1 | include "ASM/ASMCosts.ma". |
---|
2 | include "ASM/UtilBranch.ma". |
---|
3 | include alias "arithmetics/nat.ma". |
---|
4 | include alias "basics/logic.ma". |
---|
5 | |
---|
6 | let rec traverse_code_internal |
---|
7 | (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
8 | (program_counter: Word) (program_size: nat) |
---|
9 | (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16) |
---|
10 | on program_size: |
---|
11 | Σcost_map: identifier_map CostTag nat. |
---|
12 | (∀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) ∧ |
---|
13 | (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧ |
---|
14 | pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝ |
---|
15 | match program_size return λx. x = program_size → Σcost_map: ?. ? with |
---|
16 | [ O ⇒ λprogram_size_refl. empty_map CostTag nat |
---|
17 | | S program_size' ⇒ λprogram_size_refl. |
---|
18 | deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in |
---|
19 | let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in |
---|
20 | match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with |
---|
21 | [ None ⇒ λlookup_refl. pi1 … cost_mapping |
---|
22 | | Some lbl ⇒ λlookup_refl. |
---|
23 | let cost ≝ block_cost code_memory program_counter cost_labels in |
---|
24 | add … cost_mapping lbl cost |
---|
25 | ] (refl … (lookup_opt … program_counter cost_labels)) |
---|
26 | ] (refl … program_size). |
---|
27 | [3: |
---|
28 | cases program_size_invariant |
---|
29 | [1: |
---|
30 | #destruct_assm @⊥ -traverse_code_internal destruct |
---|
31 | |2: |
---|
32 | #program_size_invariant' |
---|
33 | % |
---|
34 | [1: |
---|
35 | #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl) |
---|
36 | [1: |
---|
37 | #eq_assm >eq_assm |
---|
38 | cases cost_mapping #cost_mapping' * #ind_hyp #_ |
---|
39 | @present_add_hit |
---|
40 | |2: |
---|
41 | #neq_assm @present_add_miss try assumption |
---|
42 | cases cost_mapping #cost_mapping' * #ind_hyp #_ |
---|
43 | inversion program_size' |
---|
44 | [1: |
---|
45 | #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm |
---|
46 | cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *) |
---|
47 | [1: |
---|
48 | #Some_assm destruct(Some_assm) % |
---|
49 | |2: |
---|
50 | #Some_assm @Some_assm <lookup_opt_assm >lookup_refl |
---|
51 | >(?:pc=program_counter) |
---|
52 | [1: |
---|
53 | % |
---|
54 | |2: |
---|
55 | @refl_nat_of_bitvector_to_refl |
---|
56 | @le_to_le_to_eq |
---|
57 | try assumption |
---|
58 | change with (? ≤ ?) in H2; |
---|
59 | @le_S_S_to_le |
---|
60 | assumption |
---|
61 | ] |
---|
62 | ] |
---|
63 | |2: |
---|
64 | #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct |
---|
65 | cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) |
---|
66 | [1: |
---|
67 | destruct |
---|
68 | @succ_nat_of_bitvector_half_add_1 |
---|
69 | @le_plus_to_minus_r |
---|
70 | change with (S ? ≤ ?) >plus_n_Sm |
---|
71 | <program_size_invariant' |
---|
72 | @monotonic_le_plus_r |
---|
73 | @le_S_S @le_S_S @le_O_n |
---|
74 | |2: |
---|
75 | #S_assm |
---|
76 | @(ind_hyp … lookup_opt_assm) |
---|
77 | [1: |
---|
78 | @(eqb_elim (nat_of_bitvector … program_counter) |
---|
79 | (nat_of_bitvector … pc)) |
---|
80 | [1: |
---|
81 | #eqb_refl_assm |
---|
82 | -ind_hyp -H1 -H2 |
---|
83 | lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm) |
---|
84 | #program_counter_refl_assm -eqb_refl_assm |
---|
85 | <program_counter_refl_assm in lookup_opt_assm; <lookup_refl |
---|
86 | #Some_assm destruct(Some_assm) |
---|
87 | cases neq_assm #absurd_assm |
---|
88 | cases (absurd_assm (refl … k)) |
---|
89 | |2: |
---|
90 | #eqb_ref_assm |
---|
91 | -ind_hyp |
---|
92 | <NEW_PC' in S_assm; #relevant <relevant -relevant |
---|
93 | change with (? < ?) |
---|
94 | @le_neq_to_lt assumption |
---|
95 | ] |
---|
96 | |2: |
---|
97 | generalize in match H2; whd in ⊢ (??% → ?); |
---|
98 | >plus_n_Sm in ⊢ (% → ?); |
---|
99 | cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) |
---|
100 | [1: |
---|
101 | <NEW_PC' % |
---|
102 | |2: |
---|
103 | #new_program_counter_assm' >new_program_counter_assm' |
---|
104 | >S_assm #relevant assumption |
---|
105 | ] |
---|
106 | ] |
---|
107 | ] |
---|
108 | ] |
---|
109 | ] |
---|
110 | |2: |
---|
111 | #k #k_pres |
---|
112 | @(eq_identifier_elim … k lbl) |
---|
113 | [1: |
---|
114 | #eq_assm %{program_counter} % |
---|
115 | [1: |
---|
116 | >eq_assm >lookup_refl % |
---|
117 | |2: |
---|
118 | >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % |
---|
119 | ] |
---|
120 | |2: |
---|
121 | #neq_assm |
---|
122 | cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm |
---|
123 | cases ind_hyp #_ #relevant cases (relevant k ?) |
---|
124 | [2: |
---|
125 | @(present_add_present … present_assm) assumption |
---|
126 | |1: |
---|
127 | #program_counter' #ind_hyp' %{program_counter'} % |
---|
128 | [1: |
---|
129 | cases ind_hyp' #assm #_ assumption |
---|
130 | |2: |
---|
131 | cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp'' |
---|
132 | @sym_eq @lookup_present_add_miss assumption |
---|
133 | ] |
---|
134 | ] |
---|
135 | ] |
---|
136 | ] |
---|
137 | ] |
---|
138 | |1: |
---|
139 | % |
---|
140 | [1: |
---|
141 | #pc #k #absurd1 #absurd2 |
---|
142 | @⊥ lapply(lt_to_not_le … absurd2) * |
---|
143 | #absurd @absurd assumption |
---|
144 | |2: |
---|
145 | #k #k_pres |
---|
146 | @⊥ normalize in k_pres; /2/ |
---|
147 | ] |
---|
148 | |2: |
---|
149 | cases cost_mapping |
---|
150 | -traverse_code_internal #cost_mapping * |
---|
151 | #inductive_hypothesis1 #inductive_hypothesis2 % |
---|
152 | [1: |
---|
153 | #pc #k #H1 #H2 |
---|
154 | cases program_size_invariant |
---|
155 | [1: |
---|
156 | #destruct_assm @⊥ destruct |
---|
157 | |2: |
---|
158 | -program_size_invariant #program_size_invariant |
---|
159 | inversion program_size' |
---|
160 | [1: |
---|
161 | #program_size_refl_0 destruct |
---|
162 | #lookup_opt_Some_assm |
---|
163 | >(?:pc = program_counter) in lookup_opt_Some_assm; |
---|
164 | [1: |
---|
165 | #absurd <lookup_refl in absurd; |
---|
166 | #absurd destruct |
---|
167 | |2: |
---|
168 | @refl_nat_of_bitvector_to_refl |
---|
169 | @le_to_le_to_eq |
---|
170 | try assumption |
---|
171 | change with (? ≤ ?) in H2; |
---|
172 | @le_S_S_to_le |
---|
173 | assumption |
---|
174 | ] |
---|
175 | |2: |
---|
176 | #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl |
---|
177 | @(inductive_hypothesis1 … pc) try assumption |
---|
178 | [1: |
---|
179 | @(eqb_elim … (nat_of_bitvector … program_counter) |
---|
180 | (nat_of_bitvector … pc)); |
---|
181 | [1: |
---|
182 | #eq_assm |
---|
183 | lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl |
---|
184 | <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd |
---|
185 | destruct |
---|
186 | |2: |
---|
187 | #neq_assm |
---|
188 | @(transitive_le ? (S (nat_of_bitvector … program_counter))) |
---|
189 | [1: |
---|
190 | cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) |
---|
191 | [1: |
---|
192 | destruct |
---|
193 | @succ_nat_of_bitvector_half_add_1 |
---|
194 | @le_plus_to_minus_r |
---|
195 | change with (S ? ≤ ?) >plus_n_Sm |
---|
196 | <program_size_invariant |
---|
197 | @monotonic_le_plus_r |
---|
198 | @le_S_S @le_S_S @le_O_n |
---|
199 | |2: |
---|
200 | #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n |
---|
201 | ] |
---|
202 | |2: |
---|
203 | change with (? < ?) |
---|
204 | @le_neq_to_lt |
---|
205 | assumption |
---|
206 | ] |
---|
207 | ] |
---|
208 | |2: |
---|
209 | destruct |
---|
210 | @(transitive_le … H2) |
---|
211 | cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) |
---|
212 | [1: |
---|
213 | destruct |
---|
214 | @succ_nat_of_bitvector_half_add_1 |
---|
215 | @le_plus_to_minus_r |
---|
216 | change with (S ? ≤ ?) >plus_n_Sm |
---|
217 | <program_size_invariant |
---|
218 | @monotonic_le_plus_r |
---|
219 | @le_S_S @le_S_S @le_O_n |
---|
220 | |2: |
---|
221 | #S_assm |
---|
222 | change with (S (S n' + ?) ≤ ?) |
---|
223 | >plus_n_Sm @monotonic_le_plus_r >S_assm |
---|
224 | <NEW_PC' @le_n |
---|
225 | ] |
---|
226 | ] |
---|
227 | ] |
---|
228 | ] |
---|
229 | |2: |
---|
230 | assumption |
---|
231 | ] |
---|
232 | |4: |
---|
233 | inversion program_size' |
---|
234 | [1: |
---|
235 | #_ %1 % |
---|
236 | |2: |
---|
237 | #n' #_ #program_size_refl_Sn @or_intror |
---|
238 | cases program_size_invariant |
---|
239 | [1: |
---|
240 | #absurd destruct |
---|
241 | |2: |
---|
242 | #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm |
---|
243 | @eq_f >program_size_refl_Sn <plus_n_Sm |
---|
244 | change with (? = (S ?) + ?) @eq_f2 try % |
---|
245 | cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) |
---|
246 | [1: |
---|
247 | destruct |
---|
248 | @succ_nat_of_bitvector_half_add_1 |
---|
249 | @le_plus_to_minus_r |
---|
250 | change with (S ? ≤ ?) >plus_n_Sm |
---|
251 | <relevant |
---|
252 | @monotonic_le_plus_r |
---|
253 | @le_S_S @le_S_S @le_O_n |
---|
254 | |2: |
---|
255 | #S_assm |
---|
256 | cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter)) |
---|
257 | [1: |
---|
258 | <NEW_PC' % |
---|
259 | |2: |
---|
260 | #new_program_counter_assm' >new_program_counter_assm' |
---|
261 | cases program_size_invariant |
---|
262 | [1: |
---|
263 | #destruct_assm destruct |
---|
264 | |2: |
---|
265 | #program_size_invariant |
---|
266 | <program_size_invariant <program_size_refl |
---|
267 | <S_assm normalize <plus_n_Sm % |
---|
268 | ] |
---|
269 | ] |
---|
270 | ] |
---|
271 | ] |
---|
272 | ] |
---|
273 | ] |
---|
274 | qed. |
---|
275 | |
---|
276 | (* XXX: |
---|
277 | * At the moment we do a full traversal of the code memory, however we could do |
---|
278 | * a fold over the domain of the cost labels map. |
---|
279 | * |
---|
280 | *) |
---|
281 | definition traverse_code: |
---|
282 | ∀code_memory: BitVectorTrie Byte 16. |
---|
283 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
284 | ∀cost_labels_injective: |
---|
285 | ∀pc, pc',l. |
---|
286 | lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → |
---|
287 | pc = pc'. |
---|
288 | Σcost_map: identifier_map CostTag nat. |
---|
289 | (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ |
---|
290 | (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → |
---|
291 | pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝ |
---|
292 | λcode_memory: BitVectorTrie Byte 16. |
---|
293 | λcost_labels: BitVectorTrie costlabel 16. |
---|
294 | λcost_labels_injective. |
---|
295 | pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?). |
---|
296 | [1: |
---|
297 | @or_intror % |
---|
298 | |2: |
---|
299 | cases (traverse_code_internal ?????) |
---|
300 | #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 % |
---|
301 | [1: |
---|
302 | #pc #k #pc_program_size_assm |
---|
303 | @inductive_hypothesis1 |
---|
304 | [1: |
---|
305 | @le_O_n |
---|
306 | |2: |
---|
307 | normalize in match (nat_of_bitvector 16 (zero 16)); |
---|
308 | <plus_n_O assumption |
---|
309 | ] |
---|
310 | |2: |
---|
311 | #k #k_pres #pc #lookup_opt_assm |
---|
312 | cases (inductive_hypothesis2 ? k_pres) |
---|
313 | #program_counter' * #lookup_opt_assm' #block_cost_assm |
---|
314 | >(cost_labels_injective … lookup_opt_assm lookup_opt_assm') |
---|
315 | assumption |
---|
316 | ] |
---|
317 | ] |
---|
318 | qed. |
---|
319 | |
---|
320 | definition compute_costs ≝ |
---|
321 | λprogram: list Byte. |
---|
322 | λcost_labels: BitVectorTrie costlabel 16. |
---|
323 | λcost_labels_injective: |
---|
324 | ∀pc, pc',l. |
---|
325 | lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → |
---|
326 | pc = pc'. |
---|
327 | let program_size ≝ |program| in |
---|
328 | let code_memory ≝ load_code_memory program in |
---|
329 | traverse_code code_memory cost_labels cost_labels_injective. |
---|