source: src/ASM/ASMCostsSplit.ma @ 1919

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

Fixes to get everything compiling again

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