1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Interpret.ma". |
---|
5 | include "common/StructuredTraces.ma". |
---|
6 | |
---|
7 | definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝ |
---|
8 | λcode_memory. |
---|
9 | λcost_labels. |
---|
10 | mk_abstract_status |
---|
11 | (Status code_memory) |
---|
12 | (λs,s'. (execute_1 … s) = s') |
---|
13 | word_deqset |
---|
14 | (program_counter …) |
---|
15 | (λs. ASM_classify … s) |
---|
16 | (λpc.lookup_opt ?? pc cost_labels) |
---|
17 | (next_instruction_properly_relates_program_counters code_memory) |
---|
18 | ? |
---|
19 | ?. |
---|
20 | cases daemon (* XXX: is final predicate, call ident function *) |
---|
21 | qed. |
---|
22 | |
---|
23 | definition trace_any_label_length ≝ |
---|
24 | λcode_memory: BitVectorTrie Byte 16. |
---|
25 | λcost_labels: BitVectorTrie costlabel 16. |
---|
26 | λtrace_ends_flag: trace_ends_with_ret. |
---|
27 | λstart_status: Status code_memory. |
---|
28 | λfinal_status: Status code_memory. |
---|
29 | λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status. |
---|
30 | as_trace_any_label_length' … the_trace. |
---|
31 | |
---|
32 | let rec all_program_counter_list |
---|
33 | (n: nat) |
---|
34 | on n ≝ |
---|
35 | match n with |
---|
36 | [ O ⇒ [ ] |
---|
37 | | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n') |
---|
38 | ]. |
---|
39 | |
---|
40 | lemma all_program_counter_list_bound_eq: |
---|
41 | ∀bound: nat. |
---|
42 | |all_program_counter_list bound| = bound. |
---|
43 | #bound elim bound try % |
---|
44 | #bound' #inductive_hypothesis normalize |
---|
45 | >inductive_hypothesis % |
---|
46 | qed. |
---|
47 | |
---|
48 | lemma mem_all_program_counter_list_lt_bound: |
---|
49 | ∀bound: nat. |
---|
50 | ∀bound_proof: bound ≤ 2^16. |
---|
51 | ∀e: Word. |
---|
52 | memb word_deqset e (all_program_counter_list bound) = true → |
---|
53 | nat_of_bitvector … e < bound. |
---|
54 | #bound elim bound |
---|
55 | [1: |
---|
56 | #bound_proof #e |
---|
57 | normalize #absurd destruct(absurd) |
---|
58 | |2: |
---|
59 | #bound' #inductive_hypothesis |
---|
60 | #bound_proof #e |
---|
61 | change with (if eq_bv ??? then ? else ? = ? → ?) |
---|
62 | @eq_bv_elim |
---|
63 | [1: |
---|
64 | #eq_assm |
---|
65 | normalize nodelta destruct #_ |
---|
66 | >nat_of_bitvector_bitvector_of_nat_inverse try assumption |
---|
67 | normalize % |
---|
68 | |2: |
---|
69 | #neq_assm normalize nodelta |
---|
70 | #memb_assm %2 @inductive_hypothesis |
---|
71 | try assumption |
---|
72 | @(transitive_le bound' (S bound')) |
---|
73 | try assumption %2 % |
---|
74 | ] |
---|
75 | ] |
---|
76 | qed. |
---|
77 | |
---|
78 | lemma lt_bound_mem_all_program_counter_list: |
---|
79 | ∀bound: nat. |
---|
80 | ∀bound_proof: bound ≤ 2^16. |
---|
81 | ∀e: Word. |
---|
82 | nat_of_bitvector … e < bound → |
---|
83 | memb word_deqset e (all_program_counter_list bound) = true. |
---|
84 | #bound elim bound |
---|
85 | [1: |
---|
86 | #bound_proof #e normalize |
---|
87 | #absurd cases (lt_to_not_zero … absurd) |
---|
88 | |2: |
---|
89 | #bound' #inductive_hypothesis |
---|
90 | #bound_proof #e |
---|
91 | change with (? → if eq_bv ??? then ? else ? = ?) |
---|
92 | #assm |
---|
93 | cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?) |
---|
94 | [1: |
---|
95 | #e_lt_assm |
---|
96 | @eq_bv_elim |
---|
97 | [1: |
---|
98 | #eq_assm normalize nodelta % |
---|
99 | |2: |
---|
100 | #neq_assm normalize nodelta |
---|
101 | @inductive_hypothesis try assumption |
---|
102 | @(transitive_le bound' (S bound')) try assumption |
---|
103 | %2 % |
---|
104 | ] |
---|
105 | |2: |
---|
106 | #relevant >eq_eq_bv normalize nodelta try % |
---|
107 | destruct >bitvector_of_nat_inverse_nat_of_bitvector % |
---|
108 | |3: |
---|
109 | normalize in assm; |
---|
110 | @le_S_S_to_le assumption |
---|
111 | ] |
---|
112 | ] |
---|
113 | qed. |
---|
114 | |
---|
115 | include alias "arithmetics/nat.ma". |
---|
116 | |
---|
117 | lemma execute_1_and_program_counter_after_other_in_lockstep: |
---|
118 | ∀code_memory: BitVectorTrie Byte 16. |
---|
119 | ∀start_status: Status code_memory. |
---|
120 | ASM_classify code_memory start_status = cl_other → |
---|
121 | let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in |
---|
122 | program_counter ? ? (execute_1 … start_status) = |
---|
123 | program_counter_after_other pc instruction. |
---|
124 | #code_memory #start_status #classify_assm |
---|
125 | whd in match execute_1; normalize nodelta |
---|
126 | cases (execute_1' code_memory start_status) #the_status |
---|
127 | * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm; |
---|
128 | cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks |
---|
129 | #classify_assm #classify_assm' @classify_assm' assumption |
---|
130 | qed. |
---|
131 | |
---|
132 | lemma nat_of_bitvector_lt_bound: |
---|
133 | ∀n: nat. |
---|
134 | ∀b: BitVector n. |
---|
135 | nat_of_bitvector n b < 2^n. |
---|
136 | #n #b cases daemon |
---|
137 | qed. |
---|
138 | |
---|
139 | lemma sublist_tal_pc_list_all_program_counter_list: |
---|
140 | ∀code_memory: BitVectorTrie Byte 16. |
---|
141 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
142 | ∀start, final: Status code_memory. |
---|
143 | ∀trace_ends_flag. |
---|
144 | ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final. |
---|
145 | sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)). |
---|
146 | #code_memory #cost_labels #start #final #trace_ends_flag #the_trace |
---|
147 | whd in match (sublist ???); #pc #memb_assm |
---|
148 | @lt_bound_mem_all_program_counter_list try % |
---|
149 | @nat_of_bitvector_lt_bound |
---|
150 | qed. |
---|
151 | |
---|
152 | corollary tal_pc_list_length_leq_total_program_size: |
---|
153 | ∀code_memory: BitVectorTrie Byte 16. |
---|
154 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
155 | ∀start, final: Status code_memory. |
---|
156 | ∀trace_ends_flag. |
---|
157 | ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final. |
---|
158 | ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace. |
---|
159 | |tal_pc_list … the_trace| ≤ 2^16. |
---|
160 | #code_memory #cost_labels #start #final #trace_ends_flag #the_trace #unrepeating_witness |
---|
161 | <(all_program_counter_list_bound_eq (2^16)) |
---|
162 | @sublist_length |
---|
163 | [1: |
---|
164 | @tal_unrepeating_uniqueb |
---|
165 | assumption |
---|
166 | |2: |
---|
167 | @sublist_tal_pc_list_all_program_counter_list |
---|
168 | assumption |
---|
169 | ] |
---|
170 | qed. |
---|
171 | |
---|
172 | let rec compute_paid_trace_any_label |
---|
173 | (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
174 | (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) |
---|
175 | (final_status: Status code_memory) |
---|
176 | (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status) |
---|
177 | on the_trace: nat ≝ |
---|
178 | match the_trace with |
---|
179 | [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status |
---|
180 | | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status |
---|
181 | | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call |
---|
182 | | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final |
---|
183 | _ _ _ call_trace _ final_trace ⇒ |
---|
184 | let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in |
---|
185 | let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in |
---|
186 | current_instruction_cost + final_trace_cost |
---|
187 | | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ |
---|
188 | let current_instruction_cost ≝ current_instruction_cost … status_pre in |
---|
189 | let tail_trace_cost ≝ |
---|
190 | compute_paid_trace_any_label … cost_labels end_flag |
---|
191 | status_init status_end tail_trace |
---|
192 | in |
---|
193 | current_instruction_cost + tail_trace_cost |
---|
194 | ]. |
---|
195 | |
---|
196 | definition compute_paid_trace_label_label ≝ |
---|
197 | λcode_memory: BitVectorTrie Byte 16. |
---|
198 | λcost_labels: BitVectorTrie costlabel 16. |
---|
199 | λtrace_ends_flag: trace_ends_with_ret. |
---|
200 | λstart_status: Status code_memory. |
---|
201 | λfinal_status: Status code_memory. |
---|
202 | λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
203 | match the_trace with |
---|
204 | [ tll_base ends_flag initial final given_trace labelled_proof ⇒ |
---|
205 | compute_paid_trace_any_label … given_trace |
---|
206 | ]. |
---|
207 | |
---|
208 | lemma trace_compute_paid_trace_cl_other: |
---|
209 | ∀code_memory' : (BitVectorTrie Byte 16). |
---|
210 | ∀program_counter' : Word. |
---|
211 | ∀cost_labels : (BitVectorTrie costlabel 16). |
---|
212 | ∀program_size' : ℕ. |
---|
213 | ∀ticks : ℕ. |
---|
214 | ∀instruction : instruction. |
---|
215 | ∀program_counter'' : Word. |
---|
216 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). |
---|
217 | let program_counter''' ≝ program_counter_after_other program_counter'' instruction in |
---|
218 | ∀start_status : (Status code_memory'). |
---|
219 | ∀final_status : (Status code_memory'). |
---|
220 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
221 | ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
222 | ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
223 | ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'. |
---|
224 | ∀classify_assm: ASM_classify0 instruction = cl_other. |
---|
225 | ∀pi1 : ℕ. |
---|
226 | (if match lookup_opt costlabel 16 program_counter''' cost_labels with |
---|
227 | [None ⇒ true |
---|
228 | |Some _ ⇒ false |
---|
229 | ] |
---|
230 | then |
---|
231 | ∀start_status0:Status code_memory'. |
---|
232 | ∀final_status0:Status code_memory'. |
---|
233 | ∀trace_ends_flag0:trace_ends_with_ret. |
---|
234 | ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0. |
---|
235 | trace_any_label_length code_memory' cost_labels trace_ends_flag0 |
---|
236 | start_status0 final_status0 the_trace0 ≤ program_size' → |
---|
237 | program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 → |
---|
238 | pi1 |
---|
239 | =compute_paid_trace_any_label code_memory' cost_labels |
---|
240 | trace_ends_flag0 start_status0 final_status0 the_trace0 |
---|
241 | else (pi1=O) ) |
---|
242 | → ticks+pi1 |
---|
243 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
244 | start_status final_status the_trace. |
---|
245 | #code_memory' #program_counter' #cost_labels #program_size' #ticks #instruction |
---|
246 | #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace |
---|
247 | #program_counter_refl #size_invariant #classify_assm #recursive_block_cost |
---|
248 | #recursive_assm |
---|
249 | @(trace_any_label_inv_ind … the_trace) |
---|
250 | [5: |
---|
251 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
252 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
253 | #the_trace_refl |
---|
254 | destruct |
---|
255 | whd in match (trace_any_label_length … (tal_step_default …)); |
---|
256 | whd in match (compute_paid_trace_any_label … (tal_step_default …)); |
---|
257 | whd in costed_assm:(?%); |
---|
258 | generalize in match costed_assm; |
---|
259 | generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)); |
---|
260 | whd in match (as_label ??); |
---|
261 | generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels) |
---|
262 | in ⊢ (??%? → % → ?); |
---|
263 | #lookup_assm cases lookup_assm |
---|
264 | [1: |
---|
265 | #None_lookup_opt_assm normalize nodelta #_ |
---|
266 | generalize in match recursive_assm; |
---|
267 | lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm) |
---|
268 | <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm; |
---|
269 | #None_lookup_opt_assm <None_lookup_opt_assm |
---|
270 | normalize nodelta #new_recursive_assm |
---|
271 | cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end |
---|
272 | end_flag trace_any_label ? ?) try (>rewrite_assm %) |
---|
273 | whd in match (current_instruction_cost … status_pre); |
---|
274 | cut(ticks = \snd (fetch code_memory' |
---|
275 | (program_counter (BitVectorTrie Byte 16) code_memory' status_pre))) |
---|
276 | [1,3: |
---|
277 | <FETCH % |
---|
278 | |2: |
---|
279 | #ticks_refl_assm |
---|
280 | >ticks_refl_assm % |
---|
281 | |4: |
---|
282 | #ticks_refl_assm |
---|
283 | change with (S ? ≤ S ?) in size_invariant; |
---|
284 | lapply (le_S_S_to_le … size_invariant) #assm |
---|
285 | assumption |
---|
286 | ] |
---|
287 | |2: |
---|
288 | #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm |
---|
289 | #absurd |
---|
290 | cases (not_Some_neq_None_to_False ?? absurd) |
---|
291 | ] |
---|
292 | |1: |
---|
293 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
294 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
295 | destruct |
---|
296 | whd in match (trace_any_label_length … (tal_base_not_return …)); |
---|
297 | whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); |
---|
298 | whd in costed_assm; |
---|
299 | generalize in match costed_assm; |
---|
300 | generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels)); |
---|
301 | whd in match (as_label ??); |
---|
302 | generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels) |
---|
303 | in ⊢ (??%? → % → ?); |
---|
304 | #lookup_assm cases lookup_assm |
---|
305 | [1: |
---|
306 | #None_lookup_opt_assm |
---|
307 | #absurd @⊥ cases absurd -absurd #absurd @absurd % |
---|
308 | |2: |
---|
309 | #costlabel #Some_lookup_opt_assm normalize nodelta #ignore |
---|
310 | generalize in match recursive_assm; |
---|
311 | cases classifier_assm |
---|
312 | [1: |
---|
313 | whd in ⊢ (% → ?); |
---|
314 | whd in ⊢ (??%? → ?); |
---|
315 | whd in match (current_instruction code_memory' status_start); |
---|
316 | <FETCH generalize in match classify_assm; |
---|
317 | cases instruction |
---|
318 | [8: |
---|
319 | #preinstruction normalize nodelta |
---|
320 | whd in match ASM_classify0; normalize nodelta |
---|
321 | #contradiction >contradiction #absurd destruct(absurd) |
---|
322 | ] |
---|
323 | try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd)) |
---|
324 | try(#addr normalize nodelta #ignore #absurd destruct(absurd)) |
---|
325 | normalize in ignore; destruct(ignore) |
---|
326 | |2: |
---|
327 | -classifier_assm #classifier_assm |
---|
328 | lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm) |
---|
329 | <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm; |
---|
330 | #Some_lookup_opt_assm <Some_lookup_opt_assm |
---|
331 | normalize nodelta #new_recursive_assm >new_recursive_assm |
---|
332 | cut(ticks = \snd (fetch code_memory' |
---|
333 | (program_counter (BitVectorTrie Byte 16) code_memory' status_start))) |
---|
334 | [1: |
---|
335 | <FETCH % |
---|
336 | |2: |
---|
337 | #ticks_refl_assm >ticks_refl_assm |
---|
338 | <plus_n_O % |
---|
339 | ] |
---|
340 | ] |
---|
341 | ] |
---|
342 | |2: |
---|
343 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
344 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
345 | |3: |
---|
346 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
347 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
348 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
349 | destruct @⊥ |
---|
350 | |4: |
---|
351 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
352 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
353 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
354 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
355 | ] |
---|
356 | change with (ASM_classify0 ? = ?) in classifier_assm; |
---|
357 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
358 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
359 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) |
---|
360 | qed. |
---|
361 | |
---|
362 | lemma trace_compute_paid_trace_cl_jump: |
---|
363 | ∀code_memory': BitVectorTrie Byte 16. |
---|
364 | ∀program_counter': Word. |
---|
365 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
366 | ∀first_time_around: bool. |
---|
367 | ∀program_size': ℕ. |
---|
368 | ∀ticks: ℕ. |
---|
369 | ∀instruction: instruction. |
---|
370 | ∀program_counter'': Word. |
---|
371 | ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'. |
---|
372 | ∀start_status: (Status code_memory'). |
---|
373 | ∀final_status: (Status code_memory'). |
---|
374 | ∀trace_ends_flag: trace_ends_with_ret. |
---|
375 | ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
376 | ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
377 | ∀classify_assm: ASM_classify0 instruction = cl_jump. |
---|
378 | ticks |
---|
379 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
380 | start_status final_status the_trace. |
---|
381 | #code_memory' #program_counter' #cost_labels #first_time_around |
---|
382 | #program_size' #ticks #instruction #program_counter'' #FETCH |
---|
383 | #start_status #final_status |
---|
384 | #trace_ends_flag #the_trace #program_counter_refl #classify_assm |
---|
385 | @(trace_any_label_inv_ind … the_trace) |
---|
386 | [5: |
---|
387 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
388 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
389 | #the_trace_refl destruct @⊥ |
---|
390 | |1: |
---|
391 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
392 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
393 | destruct |
---|
394 | whd in match (trace_any_label_length … (tal_base_not_return …)); |
---|
395 | whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); |
---|
396 | <FETCH % |
---|
397 | |2: |
---|
398 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
399 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
400 | |3: |
---|
401 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
402 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
403 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
404 | destruct @⊥ |
---|
405 | |4: |
---|
406 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
407 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
408 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
409 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
410 | ] |
---|
411 | change with (ASM_classify0 ? = ?) in classifier_assm; |
---|
412 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
413 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
414 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) |
---|
415 | qed. |
---|
416 | |
---|
417 | lemma trace_compute_paid_trace_cl_call: |
---|
418 | ∀code_memory' : (BitVectorTrie Byte 16). |
---|
419 | ∀program_counter' : Word. |
---|
420 | ∀cost_labels : (BitVectorTrie costlabel 16). |
---|
421 | ∀program_size' : ℕ. |
---|
422 | ∀ticks : ℕ. |
---|
423 | ∀instruction : instruction. |
---|
424 | ∀program_counter'' : Word. |
---|
425 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). |
---|
426 | ∀start_status : (Status code_memory'). |
---|
427 | ∀final_status : (Status code_memory'). |
---|
428 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
429 | ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
430 | ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
431 | ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'. |
---|
432 | ∀classify_assm: ASM_classify0 instruction = cl_call. |
---|
433 | (∀pi1:ℕ |
---|
434 | .if match lookup_opt costlabel 16 program_counter'' cost_labels with |
---|
435 | [None ⇒ true | Some _ ⇒ false] |
---|
436 | then (∀start_status0:Status code_memory' |
---|
437 | .∀final_status0:Status code_memory' |
---|
438 | .∀trace_ends_flag0:trace_ends_with_ret |
---|
439 | .∀the_trace0:trace_any_label |
---|
440 | (ASM_abstract_status code_memory' cost_labels) |
---|
441 | trace_ends_flag0 start_status0 final_status0. |
---|
442 | trace_any_label_length code_memory' cost_labels trace_ends_flag0 |
---|
443 | start_status0 final_status0 the_trace0 |
---|
444 | ≤ program_size' → |
---|
445 | program_counter'' |
---|
446 | =program_counter (BitVectorTrie Byte 16) code_memory' start_status0 |
---|
447 | → pi1 |
---|
448 | =compute_paid_trace_any_label code_memory' cost_labels |
---|
449 | trace_ends_flag0 start_status0 final_status0 the_trace0) |
---|
450 | else (pi1=O) |
---|
451 | → ticks+pi1 |
---|
452 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
453 | start_status final_status the_trace). |
---|
454 | #code_memory' #program_counter' #cost_labels #program_size' |
---|
455 | #ticks #instruction #program_counter'' #FETCH |
---|
456 | #start_status #final_status #trace_ends_flag |
---|
457 | #the_trace #program_counter_refl #size_invariant #classify_assm |
---|
458 | #recursive_block_cost #recursive_assm |
---|
459 | @(trace_any_label_inv_ind … the_trace) |
---|
460 | [5: |
---|
461 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
462 | #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl |
---|
463 | #the_trace_refl destruct @⊥ |
---|
464 | |1: |
---|
465 | #status_start #status_final #execute_assm #classifier_assm #costed_assm |
---|
466 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
467 | destruct @⊥ |
---|
468 | |2: |
---|
469 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm |
---|
470 | #start_status_refl #final_status_refl #the_trace_assm destruct @⊥ |
---|
471 | |3: |
---|
472 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
473 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
474 | #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
475 | destruct |
---|
476 | whd in match (trace_any_label_length … (tal_base_call …)); |
---|
477 | whd in match (compute_paid_trace_any_label … (tal_base_call …)); |
---|
478 | whd in costed_assm; |
---|
479 | generalize in match costed_assm; |
---|
480 | generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels)); |
---|
481 | whd in match (as_label ??); |
---|
482 | generalize in match (lookup_opt … (program_counter … status_final) cost_labels) |
---|
483 | in ⊢ (??%? → % → ?); |
---|
484 | #lookup_assm cases lookup_assm |
---|
485 | [1: |
---|
486 | #None_lookup_opt normalize nodelta #absurd cases absurd |
---|
487 | -absurd #absurd @⊥ @absurd % |
---|
488 | |2: |
---|
489 | #costlabel #Some_lookup_opt normalize nodelta #ignore |
---|
490 | generalize in match recursive_assm; |
---|
491 | cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final)) |
---|
492 | [1: |
---|
493 | generalize in match after_return_assm; |
---|
494 | whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant % |
---|
495 | |2: |
---|
496 | #program_counter_assm >program_counter_assm <Some_lookup_opt |
---|
497 | normalize nodelta #new_recursive_assm >new_recursive_assm |
---|
498 | cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call))) |
---|
499 | [1: |
---|
500 | <FETCH % |
---|
501 | |2: |
---|
502 | #ticks_refl_assm >ticks_refl_assm |
---|
503 | <plus_n_O % |
---|
504 | ] |
---|
505 | ] |
---|
506 | ] |
---|
507 | |4: |
---|
508 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
509 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
510 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
511 | #final_status_refl #the_trace_refl |
---|
512 | generalize in match execute_assm; destruct #execute_assm |
---|
513 | whd in match (trace_any_label_length … (tal_step_call …)); |
---|
514 | whd in match (compute_paid_trace_any_label … (tal_step_call …)); |
---|
515 | whd in costed_assm:(?%); |
---|
516 | generalize in match costed_assm; |
---|
517 | generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels)); |
---|
518 | whd in match (as_label ??); |
---|
519 | generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels) |
---|
520 | in ⊢ (??%? → % → ?); |
---|
521 | #lookup_assm cases lookup_assm |
---|
522 | [1: |
---|
523 | #None_lookup_opt_assm normalize nodelta #ignore |
---|
524 | generalize in match recursive_assm; |
---|
525 | cut(program_counter'' = program_counter … status_after_fun_call) |
---|
526 | [1: |
---|
527 | generalize in match after_return_assm; |
---|
528 | whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant % |
---|
529 | |2: |
---|
530 | #program_counter_refl >program_counter_refl <None_lookup_opt_assm |
---|
531 | normalize nodelta #new_recursive_assm |
---|
532 | cases (new_recursive_assm … trace_any_label ? ?) |
---|
533 | [1: |
---|
534 | @plus_right_monotone whd in ⊢ (???%); <FETCH % |
---|
535 | |2: |
---|
536 | @le_S_S_to_le @size_invariant |
---|
537 | |3: |
---|
538 | % |
---|
539 | ] |
---|
540 | ] |
---|
541 | |2: |
---|
542 | #cost_label #Some_lookup_opt_assm #absurd |
---|
543 | cases (not_Some_neq_None_to_False ?? absurd) |
---|
544 | ] |
---|
545 | ] |
---|
546 | try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) |
---|
547 | try (change with (ASM_classify0 ? = ?) in classifier_assm;) |
---|
548 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
549 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
550 | <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd |
---|
551 | #absurd destruct(absurd) |
---|
552 | qed. |
---|
553 | |
---|
554 | lemma trace_compute_paid_trace_cl_return: |
---|
555 | ∀code_memory' : (BitVectorTrie Byte 16). |
---|
556 | ∀program_counter' : Word. |
---|
557 | ∀cost_labels : (BitVectorTrie costlabel 16). |
---|
558 | ∀program_size' : ℕ. |
---|
559 | ∀ticks : ℕ. |
---|
560 | ∀instruction : instruction. |
---|
561 | ∀program_counter'' : Word. |
---|
562 | ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter'). |
---|
563 | ∀start_status : (Status code_memory'). |
---|
564 | ∀final_status : (Status code_memory'). |
---|
565 | ∀trace_ends_flag : trace_ends_with_ret. |
---|
566 | ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status). |
---|
567 | ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status). |
---|
568 | ∀classify_assm: ASM_classify0 instruction = cl_return. |
---|
569 | ticks |
---|
570 | =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag |
---|
571 | start_status final_status the_trace. |
---|
572 | #code_memory' #program_counter' #cost_labels #program_size' |
---|
573 | #ticks #instruction #program_counter'' #FETCH |
---|
574 | #start_status #final_status #trace_ends_flag |
---|
575 | #the_trace #program_counter_refl #classify_assm |
---|
576 | @(trace_any_label_inv_ind … the_trace) |
---|
577 | [1: |
---|
578 | #start_status' #final_status' #execute_assm #classifier_assm #costed_assm |
---|
579 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
580 | destruct @⊥ |
---|
581 | |2: |
---|
582 | #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl |
---|
583 | #start_status_refl #final_status_refl #the_trace_refl destruct |
---|
584 | whd in match (trace_any_label_length … (tal_base_return …)); |
---|
585 | whd in match (compute_paid_trace_any_label … (tal_base_return …)); |
---|
586 | <FETCH % |
---|
587 | |3: |
---|
588 | #status_pre_fun_call #status_start_fun_call #status_final #execute_assm |
---|
589 | #classifier_assm #after_return_assm #trace_label_return #costed_assm |
---|
590 | #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl |
---|
591 | destruct @⊥ |
---|
592 | |4: |
---|
593 | #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call |
---|
594 | #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return |
---|
595 | #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl |
---|
596 | #final_status_refl #the_trace_refl |
---|
597 | destruct @⊥ |
---|
598 | |5: |
---|
599 | #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label |
---|
600 | #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl |
---|
601 | #final_status_refl #the_trace_refl destruct @⊥ |
---|
602 | ] |
---|
603 | try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;) |
---|
604 | try (change with (ASM_classify0 ? = ?) in classifier_assm;) |
---|
605 | whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; |
---|
606 | whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; |
---|
607 | <FETCH in classifier_assm; >classify_assm |
---|
608 | #absurd try (destruct(absurd)) |
---|
609 | cases absurd |
---|
610 | #absurd destruct(absurd) |
---|
611 | qed. |
---|
612 | |
---|
613 | lemma trace_any_label_length_leq_0_to_False: |
---|
614 | ∀code_memory: BitVectorTrie Byte 16. |
---|
615 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
616 | ∀trace_ends_flag: trace_ends_with_ret. |
---|
617 | ∀start_status: Status code_memory. |
---|
618 | ∀final_status: Status code_memory. |
---|
619 | ∀the_trace. |
---|
620 | trace_any_label_length code_memory cost_labels trace_ends_flag start_status |
---|
621 | final_status the_trace ≤ 0 → False. |
---|
622 | #code_memory #cost_labels #trace_ends_flag #start_status #final_status |
---|
623 | #the_trace |
---|
624 | cases the_trace /2/ |
---|
625 | qed. |
---|
626 | |
---|
627 | let rec block_cost' |
---|
628 | (code_memory': BitVectorTrie Byte 16) (program_counter': Word) |
---|
629 | (program_size: nat) (cost_labels: BitVectorTrie costlabel 16) |
---|
630 | (first_time_around: bool) |
---|
631 | on program_size: |
---|
632 | Σcost_of_block: nat. |
---|
633 | if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then |
---|
634 | ∀start_status: Status code_memory'. |
---|
635 | ∀final_status: Status code_memory'. |
---|
636 | ∀trace_ends_flag. |
---|
637 | ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
638 | trace_any_label_length … the_trace ≤ program_size → |
---|
639 | program_counter' = program_counter … start_status → |
---|
640 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace |
---|
641 | else |
---|
642 | (cost_of_block = 0) ≝ |
---|
643 | match program_size return λx. x = program_size → ? with |
---|
644 | [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *) |
---|
645 | | S program_size' ⇒ λstep_case. |
---|
646 | let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in |
---|
647 | let to_continue ≝ |
---|
648 | match lookup_opt … program_counter' cost_labels with |
---|
649 | [ None ⇒ true |
---|
650 | | Some _ ⇒ first_time_around |
---|
651 | ] |
---|
652 | in |
---|
653 | ((if to_continue then |
---|
654 | pi1 … (match instruction return λx. x = instruction → ? with |
---|
655 | [ RealInstruction real_instruction ⇒ λreal_instruction_refl. |
---|
656 | match real_instruction return λx. x = real_instruction → |
---|
657 | Σcost_of_block: nat. |
---|
658 | ∀start_status: Status code_memory'. |
---|
659 | ∀final_status: Status code_memory'. |
---|
660 | ∀trace_ends_flag. |
---|
661 | ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status. |
---|
662 | trace_any_label_length … the_trace ≤ S program_size' → |
---|
663 | program_counter' = program_counter … start_status → |
---|
664 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with |
---|
665 | [ RET ⇒ λinstr. ticks |
---|
666 | | RETI ⇒ λinstr. ticks |
---|
667 | | JC relative ⇒ λinstr. ticks |
---|
668 | | JNC relative ⇒ λinstr. ticks |
---|
669 | | JB bit_addr relative ⇒ λinstr. ticks |
---|
670 | | JNB bit_addr relative ⇒ λinstr. ticks |
---|
671 | | JBC bit_addr relative ⇒ λinstr. ticks |
---|
672 | | JZ relative ⇒ λinstr. ticks |
---|
673 | | JNZ relative ⇒ λinstr. ticks |
---|
674 | | CJNE src_trgt relative ⇒ λinstr. ticks |
---|
675 | | DJNZ src_trgt relative ⇒ λinstr. ticks |
---|
676 | | _ ⇒ λinstr. |
---|
677 | ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false |
---|
678 | ] (refl …) |
---|
679 | | ACALL addr ⇒ λinstr. |
---|
680 | ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false |
---|
681 | | AJMP addr ⇒ λinstr. |
---|
682 | let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in |
---|
683 | ticks + block_cost' code_memory' jump_target program_size' cost_labels false |
---|
684 | | LCALL addr ⇒ λinstr. |
---|
685 | ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false |
---|
686 | | LJMP addr ⇒ λinstr. |
---|
687 | let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in |
---|
688 | ticks + block_cost' code_memory' jump_target program_size' cost_labels false |
---|
689 | | SJMP addr ⇒ λinstr. |
---|
690 | let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in |
---|
691 | ticks + block_cost' code_memory' jump_target program_size' cost_labels false |
---|
692 | | JMP addr ⇒ λinstr. (* XXX: actually a call due to use with fptrs *) |
---|
693 | ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false |
---|
694 | | MOVC src trgt ⇒ λinstr. |
---|
695 | ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false |
---|
696 | ] (refl …)) |
---|
697 | else |
---|
698 | 0) |
---|
699 | : Σcost_of_block: nat. |
---|
700 | match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with |
---|
701 | [ true ⇒ |
---|
702 | ∀start_status: Status code_memory'. |
---|
703 | ∀final_status: Status code_memory'. |
---|
704 | ∀trace_ends_flag. |
---|
705 | ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
706 | trace_any_label_length … the_trace ≤ S program_size' → |
---|
707 | program_counter' = program_counter … start_status → |
---|
708 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace |
---|
709 | | false ⇒ |
---|
710 | (cost_of_block = 0) |
---|
711 | ]) |
---|
712 | ] (refl …). |
---|
713 | [2: |
---|
714 | change with (if to_continue then ? else (? = 0)) |
---|
715 | >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta |
---|
716 | @pi2 |
---|
717 | |1: |
---|
718 | destruct |
---|
719 | cases (lookup_opt ????) normalize nodelta |
---|
720 | [1: |
---|
721 | #start_status #final_status #trace_ends_flag #the_trace |
---|
722 | #absurd |
---|
723 | cases (trace_any_label_length_leq_0_to_False … absurd) |
---|
724 | |2: |
---|
725 | #cost cases first_time_around normalize nodelta try % |
---|
726 | #start_status #final_status #trace_ends_flag #the_trace #absurd |
---|
727 | cases (trace_any_label_length_leq_0_to_False … absurd) |
---|
728 | ] |
---|
729 | |3: |
---|
730 | change with (if to_continue then ? else (0 = 0)) |
---|
731 | >p normalize nodelta % |
---|
732 | |5,6: |
---|
733 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
734 | @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl) |
---|
735 | destruct % |
---|
736 | |42,46,47: |
---|
737 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
738 | cases(block_cost' ?????) -block_cost' |
---|
739 | @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant) |
---|
740 | destruct % |
---|
741 | |43,44,45: (* XXX: unconditional jumps *) |
---|
742 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
743 | cases (block_cost' ?????) -block_cost' |
---|
744 | lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant) |
---|
745 | whd in match (program_counter_after_other ??); normalize nodelta destruct |
---|
746 | whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm % |
---|
747 | |24,25,26,27,28,29,30,31,32: |
---|
748 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
749 | @(trace_compute_paid_trace_cl_jump … first_time_around program_size' … FETCH … the_trace program_counter_refl) |
---|
750 | destruct % |
---|
751 | |*: |
---|
752 | #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl |
---|
753 | cases(block_cost' ?????) -block_cost' |
---|
754 | lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant) |
---|
755 | destruct #assm @assm % |
---|
756 | ] |
---|
757 | qed. |
---|
758 | |
---|
759 | definition block_cost: |
---|
760 | ∀code_memory': BitVectorTrie Byte 16. |
---|
761 | ∀program_counter': Word. |
---|
762 | ∀cost_labels: BitVectorTrie costlabel 16. |
---|
763 | Σcost_of_block: nat. |
---|
764 | ∀start_status: Status code_memory'. |
---|
765 | ∀final_status: Status code_memory'. |
---|
766 | ∀trace_ends_flag. |
---|
767 | ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status. |
---|
768 | ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace. |
---|
769 | program_counter' = program_counter … start_status → |
---|
770 | cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝ |
---|
771 | λcode_memory: BitVectorTrie Byte 16. |
---|
772 | λprogram_counter: Word. |
---|
773 | λcost_labels: BitVectorTrie costlabel 16. ?. |
---|
774 | cases(block_cost' code_memory program_counter (2^16) cost_labels true) |
---|
775 | #cost_of_block #block_cost_hyp |
---|
776 | %{cost_of_block} |
---|
777 | cases(lookup_opt … cost_labels) in block_cost_hyp; |
---|
778 | [2: #cost_label] normalize nodelta |
---|
779 | #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness |
---|
780 | @hyp @tal_pc_list_length_leq_total_program_size try assumption |
---|
781 | qed. |
---|