source: src/ASM/ASMCostsSplit.ma @ 1896

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

Finished horror proof

File size: 15.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
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              @(plus_lt_to_lt ? (S n') (2^16 - 1))
182              @le_plus_to_minus_r
183              change with (? < ?)
184              <plus_n_Sm <plus_n_O >plus_n_Sm assumption
185            |2:
186              #S_assm
187              @(ind_hyp … lookup_opt_assm)
188              [1:
189                @(eqb_elim (nat_of_bitvector … program_counter)
190                  (nat_of_bitvector … pc))
191                [1:
192                  #eqb_refl_assm
193                  -ind_hyp -H1 -H2
194                  lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
195                  #program_counter_refl_assm -eqb_refl_assm
196                  <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
197                  #Some_assm destruct(Some_assm)
198                  cases neq_assm #absurd_assm
199                  cases (absurd_assm (refl … k))
200                |2:
201                  #eqb_ref_assm
202                  -ind_hyp
203                  <NEW_PC' in S_assm; #relevant <relevant -relevant
204                  change with (? < ?)
205                  @le_neq_to_lt assumption
206                ]
207              |2:
208                generalize in match H2; whd in ⊢ (??% → ?);
209                >plus_n_Sm in ⊢ (% → ?);
210                cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
211                [1:
212                  <NEW_PC' %
213                |2:
214                  #new_program_counter_assm' >new_program_counter_assm'
215                  >S_assm #relevant assumption
216                ]
217              ]
218            ]
219          ]
220        ]
221      |2:
222        #k #k_pres
223        @(eq_identifier_elim … k lbl)
224        [1:
225          #eq_assm %{program_counter} #lookup_opt_assm
226          %{(reachable_program_counter_witness …)} try assumption
227          >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
228        |2:
229          #neq_assm
230          cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
231          cases ind_hyp #_ #relevant cases (relevant k ?)
232          [2:
233            @(present_add_present … present_assm) assumption
234          |1:
235            #program_counter' #ind_hyp' %{program_counter'}
236            #relevant cases (ind_hyp' relevant) #reachable_witness'
237            #ind_hyp'' %{reachable_witness'} >ind_hyp''
238            @sym_eq @lookup_present_add_miss assumption
239          ]
240        ]
241      ]
242    ]
243  |1:
244    %
245    [1:
246      #pc #k #absurd1 #absurd2
247      @⊥ lapply(lt_to_not_le … absurd2) *
248      #absurd @absurd assumption
249    |2:
250      #k #k_pres
251      @⊥ normalize in k_pres; /2/
252    ]
253  |2:
254    cases cost_mapping
255    -traverse_code_internal #cost_mapping *
256    #inductive_hypothesis1 #inductive_hypothesis2 %
257    [1:
258      #pc #k #H1 #H2
259      cases program_size_invariant
260      [1:
261        #destruct_assm @⊥ destruct
262      |2:
263        -program_size_invariant #program_size_invariant
264        inversion program_size'
265        [1:
266          #program_size_refl_0 destruct
267          #lookup_opt_Some_assm
268          >(?:pc = program_counter) in lookup_opt_Some_assm;
269          [1:
270            #absurd <lookup_refl in absurd;
271            #absurd destruct
272          |2:
273            @refl_nat_of_bitvector_to_refl
274            @le_to_le_to_eq
275            try assumption
276            change with (? ≤ ?) in H2;
277            @le_S_S_to_le
278            assumption
279          ]
280        |2:
281          #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl
282          @(inductive_hypothesis1 … pc) try assumption
283          [1:
284            @(eqb_elim … (nat_of_bitvector … program_counter)
285              (nat_of_bitvector … pc));
286            [1:
287              #eq_assm
288              lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl
289              <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd
290              destruct
291            |2:
292              #neq_assm
293              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
294              [1:
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                  @(plus_lt_to_lt ? (S n') (2^16 - 1))
300                  @le_plus_to_minus_r
301                  change with (? < ?)
302                  <plus_n_Sm <plus_n_O >plus_n_Sm assumption
303                |2:
304                  #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n
305                ]
306              |2:
307                change with (? < ?)
308                @le_neq_to_lt
309                assumption
310              ]
311            ]
312          |2:
313            destruct
314            @(transitive_le … H2)
315            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
316            [1:
317              @succ_nat_of_bitvector_half_add_1
318              @(plus_lt_to_lt ? (S n') (2^16 - 1))
319              @le_plus_to_minus_r
320              change with (? < ?)
321              <plus_n_Sm <plus_n_O >plus_n_Sm assumption
322            |2:
323              #S_assm
324              change with (S (S n' + ?) ≤ ?)
325              >plus_n_Sm @monotonic_le_plus_r >S_assm
326              <NEW_PC' @le_n
327            ]
328          ]
329        ]
330      ]
331    |2:
332      assumption
333    ]
334  |6:
335    inversion program_size'
336    [1:
337      #_ %1 %
338    |2:
339      #n' #_ #program_size_refl_Sn @or_intror
340      cases program_size_invariant
341      [1:
342        #absurd destruct
343      |2:
344        #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm
345        @eq_f >program_size_refl_Sn <plus_n_Sm
346        change with (? = (S ?) + ?) @eq_f2 try %
347        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
348        [1:
349          @succ_nat_of_bitvector_half_add_1
350          @le_plus_to_minus_r
351          @(transitive_le … fixed_program_size_limit)
352          destruct <plus_n_Sm <plus_n_Sm
353          change with (S (S ?) + ? ≤ S (S ?) + ?)
354          @monotonic_le_plus_r @le_O_n
355        |2:
356          #S_assm
357          cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
358          [1:
359            <NEW_PC' %
360          |2:
361           #new_program_counter_assm' >new_program_counter_assm'
362           cases program_size_invariant
363           [1:
364             #destruct_assm destruct
365           |2:
366             #program_size_invariant
367             <program_size_invariant <program_size_refl
368             <S_assm normalize <plus_n_Sm %
369           ]
370         ]
371      ]
372    ]
373    ]
374  ]
375qed.
376
377definition traverse_code:
378  ∀code_memory: BitVectorTrie Byte 16.
379  ∀cost_labels: BitVectorTrie costlabel 16.
380  ∀program_size: nat.
381  ∀reachable_program_counter_witness:
382    ∀lbl: costlabel.
383    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
384      reachable_program_counter code_memory program_size program_counter.
385  ∀good_program_witness: good_program code_memory program_size.
386    Σcost_map: identifier_map CostTag nat.
387      (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
388        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
389          pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
390  λcode_memory: BitVectorTrie Byte 16.
391  λcost_labels: BitVectorTrie costlabel 16.
392  λprogram_size: nat.
393  λreachable_program_counter_witness:
394          ∀lbl: costlabel.
395          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
396            reachable_program_counter code_memory program_size program_counter.
397  λgood_program_witness: good_program code_memory program_size.
398    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
399 
400definition compute_costs ≝
401  λprogram: list Byte.
402  λcost_labels: BitVectorTrie costlabel 16.
403  λreachable_program_witness.
404  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
405    let program_size ≝ |program| + 1 in
406    let code_memory ≝ load_code_memory program in
407      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
408  @good_program_witness
409qed.
Note: See TracBrowser for help on using the repository browser.