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