1 | include "ASM/ASMCosts.ma". |
---|
2 | include alias "arithmetics/nat.ma". |
---|
3 | include alias "basics/logic.ma". |
---|
4 | |
---|
5 | |
---|
6 | (* Also extracts an equality proof (useful when not using Russell). *) |
---|
7 | notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)" |
---|
8 | with precedence 10 |
---|
9 | for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒ |
---|
10 | λ${ident E}.$s ] (refl ? $t) }. |
---|
11 | |
---|
12 | (* |
---|
13 | lemma 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 | |
---|
19 | notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" |
---|
20 | with precedence 10 |
---|
21 | for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒ |
---|
22 | λ${ident E}.$s ] (refl ? $t) }. |
---|
23 | |
---|
24 | (* |
---|
25 | notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" |
---|
26 | with precedence 10 |
---|
27 | for @{ 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 | |
---|
31 | notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" |
---|
32 | with precedence 10 |
---|
33 | for @{ 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 | |
---|
37 | notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)" |
---|
38 | with precedence 10 |
---|
39 | for @{ 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 | (* |
---|
44 | lemma 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 | |
---|
57 | lemma 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 | |
---|
71 | lemma 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 | |
---|
85 | lemma 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/ |
---|
93 | qed. |
---|
94 | |
---|
95 | lemma 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/ |
---|
103 | qed. *) |
---|
104 | |
---|
105 | |
---|
106 | let 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 | ] |
---|
375 | qed. |
---|
376 | |
---|
377 | definition 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 | |
---|
400 | definition 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 |
---|
409 | qed. |
---|