source: src/ASM/ASMCostsSplit.ma @ 1897

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

Changes to proof, and pushed through those changes to rest of the file.

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