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: costlabel_map) |
---|
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 | let new_program_counter' ≝ 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 | cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? 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 (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 | <S_assm |
---|
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' = add 16 (bitvector_of_nat 16 1) program_counter) |
---|
100 | [1: % |
---|
101 | |2: |
---|
102 | #new_program_counter_assm' >new_program_counter_assm' |
---|
103 | >S_assm #relevant assumption |
---|
104 | ] |
---|
105 | ] |
---|
106 | ] |
---|
107 | ] |
---|
108 | ] |
---|
109 | |2: |
---|
110 | #k #k_pres |
---|
111 | @(eq_identifier_elim … k lbl) |
---|
112 | [1: |
---|
113 | #eq_assm %{program_counter} % |
---|
114 | [1: |
---|
115 | >eq_assm >lookup_refl % |
---|
116 | |2: |
---|
117 | >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % |
---|
118 | ] |
---|
119 | |2: |
---|
120 | #neq_assm |
---|
121 | cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm |
---|
122 | cases ind_hyp #_ #relevant cases (relevant k ?) |
---|
123 | [2: |
---|
124 | @(present_add_present … present_assm) assumption |
---|
125 | |1: |
---|
126 | #program_counter' #ind_hyp' %{program_counter'} % |
---|
127 | [1: |
---|
128 | cases ind_hyp' #assm #_ assumption |
---|
129 | |2: |
---|
130 | cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp'' |
---|
131 | @sym_eq @lookup_present_add_miss assumption |
---|
132 | ] |
---|
133 | ] |
---|
134 | ] |
---|
135 | ] |
---|
136 | ] |
---|
137 | |1: |
---|
138 | % |
---|
139 | [1: |
---|
140 | #pc #k #absurd1 #absurd2 |
---|
141 | @⊥ lapply(lt_to_not_le … absurd2) * |
---|
142 | #absurd @absurd assumption |
---|
143 | |2: |
---|
144 | #k #k_pres |
---|
145 | @⊥ normalize in k_pres; /2/ |
---|
146 | ] |
---|
147 | |2: |
---|
148 | cases cost_mapping |
---|
149 | -traverse_code_internal #cost_mapping * |
---|
150 | #inductive_hypothesis1 #inductive_hypothesis2 % |
---|
151 | [1: |
---|
152 | #pc #k #H1 #H2 |
---|
153 | cases program_size_invariant |
---|
154 | [1: |
---|
155 | #destruct_assm @⊥ destruct |
---|
156 | |2: |
---|
157 | -program_size_invariant #program_size_invariant |
---|
158 | inversion program_size' |
---|
159 | [1: |
---|
160 | #program_size_refl_0 destruct |
---|
161 | #lookup_opt_Some_assm |
---|
162 | >(?:pc = program_counter) in lookup_opt_Some_assm; |
---|
163 | [1: |
---|
164 | #absurd <lookup_refl in absurd; |
---|
165 | #absurd destruct |
---|
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 | |2: |
---|
175 | #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl |
---|
176 | @(inductive_hypothesis1 … pc) try assumption |
---|
177 | [1: |
---|
178 | @(eqb_elim … (nat_of_bitvector … program_counter) |
---|
179 | (nat_of_bitvector … pc)); |
---|
180 | [1: |
---|
181 | #eq_assm |
---|
182 | lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl |
---|
183 | <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd |
---|
184 | destruct |
---|
185 | |2: |
---|
186 | #neq_assm |
---|
187 | @(transitive_le ? (S (nat_of_bitvector … program_counter))) |
---|
188 | [1: |
---|
189 | cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter)) |
---|
190 | [1: |
---|
191 | destruct |
---|
192 | @succ_nat_of_bitvector_half_add_1 |
---|
193 | @le_plus_to_minus_r |
---|
194 | change with (S ? ≤ ?) >plus_n_Sm |
---|
195 | <program_size_invariant |
---|
196 | @monotonic_le_plus_r |
---|
197 | @le_S_S @le_S_S @le_O_n |
---|
198 | |2: |
---|
199 | #Sn_refl_assm >Sn_refl_assm @le_n |
---|
200 | ] |
---|
201 | |2: |
---|
202 | change with (? < ?) |
---|
203 | @le_neq_to_lt |
---|
204 | assumption |
---|
205 | ] |
---|
206 | ] |
---|
207 | |2: |
---|
208 | destruct |
---|
209 | @(transitive_le … H2) |
---|
210 | cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter)) |
---|
211 | [1: |
---|
212 | destruct |
---|
213 | @succ_nat_of_bitvector_half_add_1 |
---|
214 | @le_plus_to_minus_r |
---|
215 | change with (S ? ≤ ?) >plus_n_Sm |
---|
216 | <program_size_invariant |
---|
217 | @monotonic_le_plus_r |
---|
218 | @le_S_S @le_S_S @le_O_n |
---|
219 | |2: |
---|
220 | #S_assm |
---|
221 | change with (S (S n' + ?) ≤ ?) |
---|
222 | >plus_n_Sm @monotonic_le_plus_r >S_assm |
---|
223 | @le_n |
---|
224 | ] |
---|
225 | ] |
---|
226 | ] |
---|
227 | ] |
---|
228 | |2: |
---|
229 | assumption |
---|
230 | ] |
---|
231 | |4: |
---|
232 | inversion program_size' |
---|
233 | [1: |
---|
234 | #_ %1 % |
---|
235 | |2: |
---|
236 | #n' #_ #program_size_refl_Sn @or_intror |
---|
237 | cases program_size_invariant |
---|
238 | [1: |
---|
239 | #absurd destruct |
---|
240 | |2: |
---|
241 | #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm |
---|
242 | @eq_f >program_size_refl_Sn <plus_n_Sm |
---|
243 | change with (? = (S ?) + ?) @eq_f2 try % |
---|
244 | cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter)) |
---|
245 | [1: |
---|
246 | destruct |
---|
247 | @succ_nat_of_bitvector_half_add_1 |
---|
248 | @le_plus_to_minus_r |
---|
249 | change with (S ? ≤ ?) >plus_n_Sm |
---|
250 | <relevant |
---|
251 | @monotonic_le_plus_r |
---|
252 | @le_S_S @le_S_S @le_O_n |
---|
253 | |2: |
---|
254 | #S_assm |
---|
255 | cut(new_program_counter' = add … (bitvector_of_nat … 1) program_counter) |
---|
256 | [1: % |
---|
257 | |2: |
---|
258 | #new_program_counter_assm' >new_program_counter_assm' |
---|
259 | cases program_size_invariant |
---|
260 | [1: |
---|
261 | #destruct_assm @⊥ >destruct_assm in program_size_refl; #abs destruct(abs) |
---|
262 | |2: |
---|
263 | #program_size_invariant |
---|
264 | <program_size_invariant <program_size_refl |
---|
265 | <S_assm normalize <plus_n_Sm % |
---|
266 | ] |
---|
267 | ] |
---|
268 | ] |
---|
269 | ] |
---|
270 | ] |
---|
271 | ] |
---|
272 | qed. |
---|
273 | |
---|
274 | (* XXX: |
---|
275 | * At the moment we do a full traversal of the code memory, however we could do |
---|
276 | * a fold over the domain of the cost labels map. |
---|
277 | * |
---|
278 | *) |
---|
279 | definition traverse_code: |
---|
280 | ∀code_memory: BitVectorTrie Byte 16. |
---|
281 | ∀cost_labels: costlabel_map. |
---|
282 | ∀cost_labels_injective: |
---|
283 | ∀pc, pc',l. |
---|
284 | lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → |
---|
285 | pc = pc'. |
---|
286 | Σcost_map: identifier_map CostTag nat. |
---|
287 | (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ |
---|
288 | (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k → |
---|
289 | pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝ |
---|
290 | λcode_memory: BitVectorTrie Byte 16. |
---|
291 | λcost_labels: costlabel_map. |
---|
292 | λcost_labels_injective. |
---|
293 | pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?). |
---|
294 | [1: |
---|
295 | @or_intror % |
---|
296 | |2: |
---|
297 | cases (traverse_code_internal ?????) |
---|
298 | #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 % |
---|
299 | [1: |
---|
300 | #pc #k #pc_program_size_assm |
---|
301 | @inductive_hypothesis1 |
---|
302 | [1: |
---|
303 | @le_O_n |
---|
304 | |2: |
---|
305 | normalize in match (nat_of_bitvector 16 (zero 16)); |
---|
306 | <plus_n_O assumption |
---|
307 | ] |
---|
308 | |2: |
---|
309 | #k #k_pres #pc #lookup_opt_assm |
---|
310 | cases (inductive_hypothesis2 ? k_pres) |
---|
311 | #program_counter' * #lookup_opt_assm' #block_cost_assm |
---|
312 | >(cost_labels_injective … lookup_opt_assm lookup_opt_assm') |
---|
313 | assumption |
---|
314 | ] |
---|
315 | ] |
---|
316 | qed. |
---|
317 | |
---|
318 | definition compute_costs ≝ |
---|
319 | λprogram: list Byte. |
---|
320 | λcost_labels: costlabel_map. |
---|
321 | λcost_labels_injective: |
---|
322 | ∀pc, pc',l. |
---|
323 | lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l → |
---|
324 | pc = pc'. |
---|
325 | let program_size ≝ |program| in |
---|
326 | let code_memory ≝ load_code_memory program in |
---|
327 | traverse_code code_memory cost_labels cost_labels_injective. |
---|
328 | |
---|
329 | (* definition object_code ≝ list Byte. *) |
---|
330 | |
---|
331 | (* use of this defn in ASM/CostsProof.ma is ill-typed *) |
---|
332 | definition ASM_cost_map : |
---|
333 | ∀p.let code_memory ≝ load_code_memory (\fst p) in |
---|
334 | ? → as_cost_map (ASM_abstract_status code_memory (\snd p)) ≝ |
---|
335 | λp : object_code × costlabel_map. |
---|
336 | λcost_labels_injective. |
---|
337 | let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in |
---|
338 | λl_sig. |
---|
339 | lookup_present … cost_map l_sig ?. |
---|
340 | cases cost_map |
---|
341 | #m * #prf #_ cases l_sig cases daemon (*bla bla*) |
---|
342 | qed. |
---|