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