source: src/ASM/ASMCostsSplit.ma @ 1899

Last change on this file since 1899 was 1899, checked in by mulligan, 8 years ago

Changes to statements of theorems

File size: 16.9 KB
Line 
1include "ASM/ASMCosts.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5
6(* Also extracts an equality proof (useful when not using Russell). *)
7notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
8 with precedence 10
9for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
10        λ${ident E}.$s ] (refl ? $t) }.
11
12(*
13lemma test:
14  ∀c: nat × nat.
15    Σx: nat. ∃y: nat. c = 〈x, y〉 ≝
16  λc: nat × nat. let 〈left, right〉 as T return Σx: ?. ? ≝ c in left.
17*)
18
19notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
20 with precedence 10
21for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
22        λ${ident E}.$s ] (refl ? $t) }.
23
24(*
25notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
26 with precedence 10
27for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
28       match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
29        λ${ident E}.$s ] ] (refl ? $t) }. *)
30
31notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
32 with precedence 10
33for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
34       match ${fresh xy} return λx.∀${ident E}:? = $t. Σu: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
35        λ${ident E}.$s ] ] (refl ? $t) }.
36
37notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
38 with precedence 10
39for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
40       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
41        λ${ident E}.$s ] ] (refl ? $t) }.
42
43let rec traverse_code_internal
44  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
45    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
46      (reachable_program_counter_witness:
47          ∀lbl: costlabel.
48          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
49            reachable_program_counter code_memory fixed_program_size program_counter)
50        (good_program_witness: good_program code_memory fixed_program_size)
51        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
52        (fixed_program_size_limit: fixed_program_size ≤ 2^16)
53        on program_size:
54          Σcost_map: identifier_map CostTag nat.
55            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
56            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
57              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
58                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
59  match program_size return λx. x = program_size → Σcost_map: ?. ? with
60  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
61  | S program_size' ⇒ λprogram_size_refl.
62    deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
63    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' fixed_program_size program_size' ? good_program_witness ? fixed_program_size_limit in
64    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
65    [ None ⇒ λlookup_refl. pi1 … cost_mapping
66    | Some lbl ⇒ λlookup_refl.
67      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
68        add … cost_mapping lbl cost
69    ] (refl … (lookup_opt … program_counter cost_labels))
70  ] (refl … program_size).
71  [5:
72    assumption
73  |4:
74    @(reachable_program_counter_witness lbl)
75    @lookup_refl
76  |3:
77    cases program_size_invariant
78    [1:
79      #destruct_assm @⊥ -traverse_code_internal destruct
80    |2:
81      #program_size_invariant'
82      %
83      [1:
84        #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
85        [1:
86          #eq_assm >eq_assm
87          cases cost_mapping #cost_mapping' * #ind_hyp #_
88          @present_add_hit
89        |2:
90          #neq_assm @present_add_miss try assumption
91          cases cost_mapping #cost_mapping' * #ind_hyp #_
92          inversion program_size'
93          [1:
94            #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm
95            cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *)
96            [1:
97              #Some_assm destruct(Some_assm) %
98            |2:
99              #Some_assm @Some_assm <lookup_opt_assm >lookup_refl
100              >(?:pc=program_counter)
101              [1:
102                %
103              |2:
104                @refl_nat_of_bitvector_to_refl
105                @le_to_le_to_eq
106                try assumption
107                change with (? ≤ ?) in H2;
108                @le_S_S_to_le
109                assumption
110              ]
111            ]
112          |2:
113            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
114            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
115            [1:
116              destruct
117              @succ_nat_of_bitvector_half_add_1
118              @le_plus_to_minus_r
119              @(transitive_le … fixed_program_size_limit)
120              change with (S ? ≤ ?) >plus_n_Sm
121              @monotonic_le_plus_r
122              @le_S_S @le_S_S @le_O_n
123            |2:
124              #S_assm
125              @(ind_hyp … lookup_opt_assm)
126              [1:
127                @(eqb_elim (nat_of_bitvector … program_counter)
128                  (nat_of_bitvector … pc))
129                [1:
130                  #eqb_refl_assm
131                  -ind_hyp -H1 -H2
132                  lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
133                  #program_counter_refl_assm -eqb_refl_assm
134                  <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
135                  #Some_assm destruct(Some_assm)
136                  cases neq_assm #absurd_assm
137                  cases (absurd_assm (refl … k))
138                |2:
139                  #eqb_ref_assm
140                  -ind_hyp
141                  <NEW_PC' in S_assm; #relevant <relevant -relevant
142                  change with (? < ?)
143                  @le_neq_to_lt assumption
144                ]
145              |2:
146                generalize in match H2; whd in ⊢ (??% → ?);
147                >plus_n_Sm in ⊢ (% → ?);
148                cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
149                [1:
150                  <NEW_PC' %
151                |2:
152                  #new_program_counter_assm' >new_program_counter_assm'
153                  >S_assm #relevant assumption
154                ]
155              ]
156            ]
157          ]
158        ]
159      |2:
160        #k #k_pres
161        @(eq_identifier_elim … k lbl)
162        [1:
163          #eq_assm %{program_counter} %
164          [1:
165            >eq_assm >lookup_refl %
166          |2:
167            %{(reachable_program_counter_witness …)} try assumption
168            >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
169          ]
170        |2:
171          #neq_assm
172          cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
173          cases ind_hyp #_ #relevant cases (relevant k ?)
174          [2:
175            @(present_add_present … present_assm) assumption
176          |1:
177            #program_counter' #ind_hyp' %{program_counter'} %
178            [1:
179              cases ind_hyp' #assm #_ assumption
180            |2:
181              cases ind_hyp' #lookup_opt_assm * #reachable_witness'
182              #ind_hyp'' %{reachable_witness'} >ind_hyp''
183              @sym_eq @lookup_present_add_miss assumption
184            ]
185          ]
186        ]
187      ]
188    ]
189  |1:
190    %
191    [1:
192      #pc #k #absurd1 #absurd2
193      @⊥ lapply(lt_to_not_le … absurd2) *
194      #absurd @absurd assumption
195    |2:
196      #k #k_pres
197      @⊥ normalize in k_pres; /2/
198    ]
199  |2:
200    cases cost_mapping
201    -traverse_code_internal #cost_mapping *
202    #inductive_hypothesis1 #inductive_hypothesis2 %
203    [1:
204      #pc #k #H1 #H2
205      cases program_size_invariant
206      [1:
207        #destruct_assm @⊥ destruct
208      |2:
209        -program_size_invariant #program_size_invariant
210        inversion program_size'
211        [1:
212          #program_size_refl_0 destruct
213          #lookup_opt_Some_assm
214          >(?:pc = program_counter) in lookup_opt_Some_assm;
215          [1:
216            #absurd <lookup_refl in absurd;
217            #absurd destruct
218          |2:
219            @refl_nat_of_bitvector_to_refl
220            @le_to_le_to_eq
221            try assumption
222            change with (? ≤ ?) in H2;
223            @le_S_S_to_le
224            assumption
225          ]
226        |2:
227          #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl
228          @(inductive_hypothesis1 … pc) try assumption
229          [1:
230            @(eqb_elim … (nat_of_bitvector … program_counter)
231              (nat_of_bitvector … pc));
232            [1:
233              #eq_assm
234              lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl
235              <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd
236              destruct
237            |2:
238              #neq_assm
239              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
240              [1:
241                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
242                [1:
243                  destruct
244                  @succ_nat_of_bitvector_half_add_1
245                  @le_plus_to_minus_r
246                  @(transitive_le … fixed_program_size_limit)
247                  change with (S ? ≤ ?) >plus_n_Sm
248                  @monotonic_le_plus_r
249                  @le_S_S @le_S_S @le_O_n
250                |2:
251                  #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n
252                ]
253              |2:
254                change with (? < ?)
255                @le_neq_to_lt
256                assumption
257              ]
258            ]
259          |2:
260            destruct
261            @(transitive_le … H2)
262            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
263            [1:
264              destruct
265              @succ_nat_of_bitvector_half_add_1
266              @le_plus_to_minus_r
267              @(transitive_le … fixed_program_size_limit)
268              change with (S ? ≤ ?) >plus_n_Sm
269              @monotonic_le_plus_r
270              @le_S_S @le_S_S @le_O_n
271            |2:
272              #S_assm
273              change with (S (S n' + ?) ≤ ?)
274              >plus_n_Sm @monotonic_le_plus_r >S_assm
275              <NEW_PC' @le_n
276            ]
277          ]
278        ]
279      ]
280    |2:
281      assumption
282    ]
283  |6:
284    inversion program_size'
285    [1:
286      #_ %1 %
287    |2:
288      #n' #_ #program_size_refl_Sn @or_intror
289      cases program_size_invariant
290      [1:
291        #absurd destruct
292      |2:
293        #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm
294        @eq_f >program_size_refl_Sn <plus_n_Sm
295        change with (? = (S ?) + ?) @eq_f2 try %
296        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
297        [1:
298          destruct
299          @succ_nat_of_bitvector_half_add_1
300          @le_plus_to_minus_r
301          @(transitive_le … fixed_program_size_limit)
302          change with (S ? ≤ ?) >plus_n_Sm
303          @monotonic_le_plus_r
304          @le_S_S @le_S_S @le_O_n
305        |2:
306          #S_assm
307          cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
308          [1:
309            <NEW_PC' %
310          |2:
311           #new_program_counter_assm' >new_program_counter_assm'
312           cases program_size_invariant
313           [1:
314             #destruct_assm destruct
315           |2:
316             #program_size_invariant
317             <program_size_invariant <program_size_refl
318             <S_assm normalize <plus_n_Sm %
319           ]
320         ]
321      ]
322    ]
323    ]
324  ]
325qed.
326
327(*
328let rec traverse_code_internal
329  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
330    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
331      (reachable_program_counter_witness:
332          ∀lbl: costlabel.
333          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
334            reachable_program_counter code_memory fixed_program_size program_counter)
335        (good_program_witness: good_program code_memory fixed_program_size)
336        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
337        (fixed_program_size_limit: fixed_program_size < 2^16)
338        on program_size:
339          Σcost_map: identifier_map CostTag nat.
340            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
341            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
342              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
343                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
344*)
345
346definition traverse_code:
347  ∀code_memory: BitVectorTrie Byte 16.
348  ∀cost_labels: BitVectorTrie costlabel 16.
349  ∀cost_labels_injective:
350    ∀pc, pc',l.
351      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
352        pc = pc'.
353  ∀program_size: nat.
354  ∀program_size_limit: program_size ≤ 2^16.
355  ∀reachable_program_counter_witness:
356    ∀lbl: costlabel.
357    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
358      reachable_program_counter code_memory program_size program_counter.
359  ∀good_program_witness: good_program code_memory program_size.
360    Σcost_map: identifier_map CostTag nat.
361      (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
362      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
363        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
364          pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
365  λcode_memory: BitVectorTrie Byte 16.
366  λcost_labels: BitVectorTrie costlabel 16.
367  λcost_labels_injective.
368  λprogram_size: nat.
369  λprogram_size_limit: program_size ≤ 2^16.
370  λreachable_program_counter_witness:
371          ∀lbl: costlabel.
372          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
373            reachable_program_counter code_memory program_size program_counter.
374  λgood_program_witness: good_program code_memory program_size.
375    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness ? program_size_limit).
376  [1:
377    @or_intror %
378  |2:
379    cases (traverse_code_internal ? ? ? ? ? ? ? ? ?)
380    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
381    [1:
382      #pc #k #pc_program_size_assm
383      @inductive_hypothesis1
384      [1:
385        @le_O_n
386      |2:
387        normalize in match (nat_of_bitvector 16 (zero 16));
388        <plus_n_O assumption
389      ]
390    |2:
391      #k #k_pres #pc #lookup_opt_assm
392      cases (inductive_hypothesis2 ? k_pres)
393      #program_counter' * #lookup_opt_assm' * #reachable_witness
394      #block_cost_assm
395      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
396      %{reachable_witness} assumption
397    ]
398  ]
399qed.
400   
401definition compute_costs ≝
402  λprogram: list Byte.
403  λcost_labels: BitVectorTrie costlabel 16.
404  λcost_labels_injective:
405    ∀pc, pc',l.
406      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
407        pc = pc'.
408  λreachable_program_witness.
409  λgood_program_witness: good_program (load_code_memory program) (|program|).
410  λprogram_size_limit: |program| ≤ 2^16.
411    let program_size ≝ |program| in
412    let code_memory ≝ load_code_memory program in
413      traverse_code code_memory cost_labels cost_labels_injective program_size program_size_limit reachable_program_witness good_program_witness.
Note: See TracBrowser for help on using the repository browser.