1 | |
---|
2 | include "ASM/ASMCosts.ma". |
---|
3 | include "ASM/WellLabeled.ma". |
---|
4 | include "ASM/Status.ma". |
---|
5 | |
---|
6 | definition is_jump_p ≝ |
---|
7 | λs. |
---|
8 | match s with |
---|
9 | [ AJMP _ ⇒ True |
---|
10 | | LJMP _ ⇒ True |
---|
11 | | SJMP _ ⇒ True |
---|
12 | | JMP _ ⇒ True |
---|
13 | | RealInstruction ri ⇒ |
---|
14 | match ri with |
---|
15 | [ JZ _ ⇒ True |
---|
16 | | JNZ _ ⇒ True |
---|
17 | | JC _ ⇒ True |
---|
18 | | JNC _ ⇒ True |
---|
19 | | JB _ _ ⇒ True |
---|
20 | | JNB _ _ ⇒ True |
---|
21 | | JBC _ _ ⇒ True |
---|
22 | | CJNE _ _ ⇒ True |
---|
23 | | DJNZ _ _ ⇒ True |
---|
24 | | _ ⇒ False |
---|
25 | ] |
---|
26 | | _ ⇒ False |
---|
27 | ]. |
---|
28 | |
---|
29 | definition is_call_p ≝ |
---|
30 | λs. |
---|
31 | match s with |
---|
32 | [ ACALL _ ⇒ True |
---|
33 | | LCALL _ ⇒ True |
---|
34 | | _ ⇒ False |
---|
35 | ]. |
---|
36 | |
---|
37 | definition next_instruction ≝ |
---|
38 | λs: Status. |
---|
39 | let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in |
---|
40 | instruction. |
---|
41 | |
---|
42 | inductive trace_ends_with_ret: Type[0] ≝ |
---|
43 | | ends_with_ret: trace_ends_with_ret |
---|
44 | | doesnt_end_with_ret: trace_ends_with_ret. |
---|
45 | |
---|
46 | definition next_instruction_is_labelled ≝ |
---|
47 | λcost_labels: BitVectorTrie Byte 16. |
---|
48 | λs: Status. |
---|
49 | let pc ≝ program_counter … (execute 1 s) in |
---|
50 | match lookup_opt … pc cost_labels with |
---|
51 | [ None ⇒ False |
---|
52 | | _ ⇒ True |
---|
53 | ]. |
---|
54 | |
---|
55 | definition current_instruction_cost ≝ |
---|
56 | λs: Status. |
---|
57 | \snd (fetch (code_memory … s) (program_counter … s)). |
---|
58 | |
---|
59 | definition next_instruction_properly_relates_program_counters ≝ |
---|
60 | λbefore: Status. |
---|
61 | λafter : Status. |
---|
62 | let size ≝ current_instruction_cost before in |
---|
63 | let pc_before ≝ program_counter … before in |
---|
64 | let pc_after ≝ program_counter … after in |
---|
65 | let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in |
---|
66 | sum = pc_after. |
---|
67 | |
---|
68 | definition current_instruction ≝ |
---|
69 | λs: Status. |
---|
70 | let pc ≝ program_counter … s in |
---|
71 | \fst (\fst (fetch … (code_memory … s) pc)). |
---|
72 | |
---|
73 | definition current_instruction_is_labelled ≝ |
---|
74 | λcost_labels: BitVectorTrie Byte 16. |
---|
75 | λs: Status. |
---|
76 | let pc ≝ program_counter … s in |
---|
77 | match lookup_opt … pc cost_labels with |
---|
78 | [ None ⇒ False |
---|
79 | | _ ⇒ True |
---|
80 | ]. |
---|
81 | |
---|
82 | inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝ |
---|
83 | | tlr_base: |
---|
84 | ∀status_before: Status. |
---|
85 | ∀status_after: Status. |
---|
86 | trace_label_label cost_labels ends_with_ret status_before status_after → |
---|
87 | trace_label_return cost_labels status_before status_after |
---|
88 | | tlr_step: |
---|
89 | ∀status_initial: Status. |
---|
90 | ∀status_labelled: Status. |
---|
91 | ∀status_final: Status. |
---|
92 | trace_label_label cost_labels doesnt_end_with_ret status_initial status_labelled → |
---|
93 | trace_label_return cost_labels status_labelled status_final → |
---|
94 | trace_label_return cost_labels status_initial status_final |
---|
95 | with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝ |
---|
96 | | tll_base: |
---|
97 | ∀ends_flag: trace_ends_with_ret. |
---|
98 | ∀start_status: Status. |
---|
99 | ∀end_status: Status. |
---|
100 | trace_label_label_pre cost_labels ends_flag start_status end_status → |
---|
101 | current_instruction_is_labelled cost_labels start_status → |
---|
102 | trace_label_label cost_labels ends_flag start_status end_status |
---|
103 | with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝ |
---|
104 | | tllp_base_not_return: |
---|
105 | ∀start_status: Status. |
---|
106 | let final_status ≝ execute 1 start_status in |
---|
107 | current_instruction start_status ≠ (RealInstruction … (RET [[relative]])) → |
---|
108 | ¬ (is_jump_p (current_instruction start_status)) → |
---|
109 | current_instruction_is_labelled cost_labels final_status → |
---|
110 | trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status |
---|
111 | | tllp_base_return: |
---|
112 | ∀start_status: Status. |
---|
113 | let final_status ≝ execute 1 start_status in |
---|
114 | current_instruction start_status = (RealInstruction … (RET [[relative]])) → |
---|
115 | trace_label_label_pre cost_labels ends_with_ret start_status final_status |
---|
116 | | tllp_base_jump: |
---|
117 | ∀start_status: Status. |
---|
118 | let final_status ≝ execute 1 start_status in |
---|
119 | is_jump_p (current_instruction start_status) → |
---|
120 | current_instruction_is_labelled cost_labels final_status → |
---|
121 | trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status |
---|
122 | | tllp_step_call: |
---|
123 | ∀end_flag: trace_ends_with_ret. |
---|
124 | ∀status_pre_fun_call: Status. |
---|
125 | ∀status_after_fun_call: Status. |
---|
126 | ∀status_final: Status. |
---|
127 | let status_start_fun_call ≝ execute 1 status_pre_fun_call in |
---|
128 | is_call_p (current_instruction status_pre_fun_call) → |
---|
129 | next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call → |
---|
130 | trace_label_return cost_labels status_start_fun_call status_after_fun_call → |
---|
131 | trace_label_label_pre cost_labels end_flag status_after_fun_call status_final → |
---|
132 | trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final |
---|
133 | | tllp_step_default: |
---|
134 | ∀end_flag: trace_ends_with_ret. |
---|
135 | ∀status_pre: Status. |
---|
136 | ∀status_end: Status. |
---|
137 | let status_init ≝ execute 1 status_pre in |
---|
138 | trace_label_label_pre cost_labels end_flag status_init status_end → |
---|
139 | ¬ (is_call_p (current_instruction status_pre)) → |
---|
140 | ¬ (is_jump_p (current_instruction status_pre)) → |
---|
141 | (current_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) → |
---|
142 | ¬ (current_instruction_is_labelled cost_labels status_init) → |
---|
143 | trace_label_label_pre cost_labels end_flag status_pre status_end. |
---|
144 | |
---|
145 | (* XXX: to do later |
---|
146 | definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ …. |
---|
147 | |
---|
148 | lemma simple_path_ok: |
---|
149 | ∀st: Status.∀H. |
---|
150 | let p ≝ compute_simple_path0 st H in |
---|
151 | ∀n. |
---|
152 | nth_path n p = execute n st ∧ |
---|
153 | (execute' (path_length p) st = 〈st',τ〉 → |
---|
154 | τ = cost_trace p) |
---|
155 | ]. |
---|
156 | *) |
---|
157 | |
---|
158 | let rec compute_max_trace_label_label_cost |
---|
159 | (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret) |
---|
160 | (start_status: Status) (final_status: Status) |
---|
161 | (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status) |
---|
162 | on the_trace: nat ≝ |
---|
163 | match the_trace with |
---|
164 | [ tll_base ends_flag initial final given_trace labelled_proof ⇒ |
---|
165 | compute_max_trace_label_label_pre_cost … given_trace |
---|
166 | ] |
---|
167 | and compute_max_trace_label_label_pre_cost |
---|
168 | (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret) |
---|
169 | (start_status: Status) (final_status: Status) |
---|
170 | (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status) |
---|
171 | on the_trace: nat ≝ |
---|
172 | match the_trace with |
---|
173 | [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ |
---|
174 | current_instruction_cost the_status |
---|
175 | | tllp_base_return the_status is_return ⇒ current_instruction_cost the_status |
---|
176 | | tllp_base_jump the_status is_jump is_cost ⇒ |
---|
177 | current_instruction_cost the_status |
---|
178 | | tllp_step_call end_flag pre_fun_call after_fun_call final is_call |
---|
179 | next_intruction_coherence call_trace final_trace ⇒ |
---|
180 | let current_instruction_cost ≝ current_instruction_cost pre_fun_call in |
---|
181 | let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in |
---|
182 | let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in |
---|
183 | call_trace_cost + current_instruction_cost + final_trace_cost |
---|
184 | | tllp_step_default end_flag status_pre status_end tail_trace is_not_call |
---|
185 | is_not_jump is_not_ret is_not_labelled ⇒ |
---|
186 | let current_instruction_cost ≝ current_instruction_cost status_pre in |
---|
187 | let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in |
---|
188 | current_instruction_cost + tail_trace_cost |
---|
189 | ] |
---|
190 | and compute_max_trace_label_return_cost |
---|
191 | (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status) |
---|
192 | (the_trace: trace_label_return cost_labels start_status final_status) |
---|
193 | on the_trace: nat ≝ |
---|
194 | match the_trace with |
---|
195 | [ tlr_base before after trace_to_lift ⇒ compute_max_trace_label_label_cost … trace_to_lift |
---|
196 | | tlr_step initial labelled final labelled_trace ret_trace ⇒ |
---|
197 | let labelled_cost ≝ compute_max_trace_label_label_cost … labelled_trace in |
---|
198 | let return_cost ≝ compute_max_trace_label_return_cost … ret_trace in |
---|
199 | labelled_cost + return_cost |
---|
200 | ]. |
---|
201 | |
---|
202 | lemma pred_minus_1: |
---|
203 | ∀m, n: nat. |
---|
204 | ∀proof: n < m. |
---|
205 | pred (m - n) = m - n - 1. |
---|
206 | #m #n |
---|
207 | cases m |
---|
208 | [ #proof |
---|
209 | cases(lt_to_not_zero … proof) |
---|
210 | | #m' #proof |
---|
211 | normalize in ⊢ (???%) |
---|
212 | cases n |
---|
213 | [ normalize // |
---|
214 | | #n' normalize |
---|
215 | cases(m' - n') |
---|
216 | [ % |
---|
217 | | #Sm_n' |
---|
218 | normalize // |
---|
219 | ] |
---|
220 | ] |
---|
221 | ] |
---|
222 | qed. |
---|
223 | |
---|
224 | lemma succ_m_plus_one: |
---|
225 | ∀m: nat. |
---|
226 | S m = m + 1. |
---|
227 | #m |
---|
228 | elim m |
---|
229 | [ % |
---|
230 | | #m' #ind_hyp |
---|
231 | normalize |
---|
232 | <ind_hyp |
---|
233 | % |
---|
234 | ] |
---|
235 | qed. |
---|
236 | |
---|
237 | lemma minus_m_n_minus_minus_plus_1: |
---|
238 | ∀m, n: nat. |
---|
239 | ∀proof: n < m. |
---|
240 | m - n = (m - n - 1) + 1. |
---|
241 | #m |
---|
242 | elim m |
---|
243 | [ #n #proof |
---|
244 | cases(lt_to_not_zero … proof) |
---|
245 | | #m' #ind_hyp #n |
---|
246 | normalize |
---|
247 | cases n |
---|
248 | [ normalize // |
---|
249 | | #n' #proof normalize |
---|
250 | <ind_hyp |
---|
251 | [ % |
---|
252 | | @le_S_S_to_le |
---|
253 | assumption |
---|
254 | ] |
---|
255 | ] |
---|
256 | ] |
---|
257 | qed. |
---|
258 | |
---|
259 | lemma plus_minus_rearrangement: |
---|
260 | ∀m, n, o: nat. |
---|
261 | ∀proof_n_m: n < m. |
---|
262 | ∀proof_m_o: m < o. |
---|
263 | (m - n) + (o - m) = o - n. |
---|
264 | #m #n #o |
---|
265 | elim m |
---|
266 | [1: #proof_n_m |
---|
267 | cases(lt_to_not_zero … proof_n_m) |
---|
268 | |2: #m' #ind_hyp |
---|
269 | #proof_n_m' #proof_m_o |
---|
270 | >minus_Sn_m |
---|
271 | [2: normalize in proof_n_m'; |
---|
272 | @le_S_S_to_le |
---|
273 | assumption |
---|
274 | |1: >eq_minus_S_pred |
---|
275 | >pred_minus_1 |
---|
276 | [1: >(succ_m_plus_one (m' - n)) |
---|
277 | >(associative_plus (m' - n) 1 (o - m' - 1)) |
---|
278 | <commutative_plus in match (1 + (o - m' - 1)); |
---|
279 | <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1) |
---|
280 | [1: >ind_hyp |
---|
281 | [1: % |
---|
282 | |2: normalize |
---|
283 | normalize in proof_m_o; |
---|
284 | @le_S_S_to_le |
---|
285 | @(le_S ? ? proof_m_o) |
---|
286 | |3: cases daemon (* XXX: problem here *) |
---|
287 | ] |
---|
288 | |2: normalize in proof_m_o; |
---|
289 | normalize |
---|
290 | @le_S_S_to_le |
---|
291 | @(le_S (S (S m')) o proof_m_o) |
---|
292 | ] |
---|
293 | |2: normalize |
---|
294 | normalize in proof_m_o; |
---|
295 | @le_S_S_to_le |
---|
296 | @(le_S (S (S m')) o proof_m_o) |
---|
297 | ] |
---|
298 | ] |
---|
299 | ] |
---|
300 | qed. |
---|
301 | |
---|
302 | example set_program_counter_ignores_clock: |
---|
303 | ∀s: Status. |
---|
304 | ∀pc: Word. |
---|
305 | clock … (set_program_counter … s pc) = clock … s. |
---|
306 | #s #pc % |
---|
307 | qed. |
---|
308 | |
---|
309 | example set_low_internal_ram_ignores_clock: |
---|
310 | ∀s: Status. |
---|
311 | ∀ram: BitVectorTrie Byte 7. |
---|
312 | clock … (set_low_internal_ram … s ram) = clock … s. |
---|
313 | #s #ram % |
---|
314 | qed. |
---|
315 | |
---|
316 | example set_8051_sfr_ignores_clock: |
---|
317 | ∀s: Status. |
---|
318 | ∀sfr: SFR8051. |
---|
319 | ∀v: Byte. |
---|
320 | clock … (set_8051_sfr ? s sfr v) = clock … s. |
---|
321 | #s #sfr #v % |
---|
322 | qed. |
---|
323 | |
---|
324 | example clock_set_clock: |
---|
325 | ∀s: Status. |
---|
326 | ∀v. |
---|
327 | clock … (set_clock … s v) = v. |
---|
328 | #s #v % |
---|
329 | qed. |
---|
330 | |
---|
331 | example write_at_stack_pointer_ignores_clock: |
---|
332 | ∀s: Status. |
---|
333 | ∀sp: Byte. |
---|
334 | clock … (write_at_stack_pointer … s sp) = clock … s. |
---|
335 | #s #sp |
---|
336 | change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with ( |
---|
337 | let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in |
---|
338 | ?); |
---|
339 | normalize nodelta; |
---|
340 | cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP)) |
---|
341 | #nu #nl normalize nodelta; |
---|
342 | cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3))) |
---|
343 | [ normalize nodelta; % |
---|
344 | | normalize nodelta; % |
---|
345 | ] |
---|
346 | qed. |
---|
347 | |
---|
348 | example status_execution_progresses_processor_clock: |
---|
349 | ∀s: Status. |
---|
350 | clock … s ≤ clock … (execute 1 s). |
---|
351 | #s |
---|
352 | change in match (execute 1 s) with (execute_1 s); |
---|
353 | change in match (execute_1 s) with ( |
---|
354 | let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) |
---|
355 | (program_counter (BitVectorTrie Byte 16) s) |
---|
356 | in |
---|
357 | execute_1_0 s instr_pc_ticks); |
---|
358 | normalize nodelta; |
---|
359 | whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s) |
---|
360 | (program_counter (BitVectorTrie Byte 16) s))); |
---|
361 | normalize nodelta; |
---|
362 | cases (fetch (code_memory (BitVectorTrie Byte 16) s) |
---|
363 | (program_counter (BitVectorTrie Byte 16) s)) |
---|
364 | #instruction_pc #ticks |
---|
365 | normalize nodelta; |
---|
366 | cases instruction_pc |
---|
367 | #instruction #pc |
---|
368 | cases instruction |
---|
369 | [1: |
---|
370 | #addr11 cases addr11 #addressing_mode |
---|
371 | normalize nodelta; cases addressing_mode |
---|
372 | normalize nodelta; |
---|
373 | [1,2,3,4,8,9,15,16,17,19: |
---|
374 | #assm whd in ⊢ (% → ?) |
---|
375 | #absurd cases(absurd) |
---|
376 | |5,6,7,10,11,12,13,14: |
---|
377 | whd in ⊢ (% → ?) |
---|
378 | #absurd cases(absurd) |
---|
379 | |18: |
---|
380 | #addr11 #irrelevant |
---|
381 | normalize nodelta; |
---|
382 | >set_program_counter_ignores_clock |
---|
383 | normalize nodelta; |
---|
384 | >set_program_counter_ignores_clock |
---|
385 | >write_at_stack_pointer_ignores_clock |
---|
386 | >set_8051_sfr_ignores_clock |
---|
387 | >write_at_stack_pointer_ignores_clock |
---|
388 | >set_8051_sfr_ignores_clock |
---|
389 | >clock_set_clock // |
---|
390 | ] |
---|
391 | |2: |
---|
392 | #addr16 cases addr16 #addressing_mode |
---|
393 | normalize nodelta; cases addressing_mode |
---|
394 | normalize nodelta; |
---|
395 | [1,2,3,4,8,9,15,16,17,18: |
---|
396 | #assm whd in ⊢ (% → ?) |
---|
397 | #absurd cases(absurd) |
---|
398 | |5,6,7,10,11,12,13,14: |
---|
399 | whd in ⊢ (% → ?) |
---|
400 | #absurd cases(absurd) |
---|
401 | |19: |
---|
402 | #addr16 #irrelevant |
---|
403 | normalize nodelta; |
---|
404 | >set_program_counter_ignores_clock |
---|
405 | >write_at_stack_pointer_ignores_clock |
---|
406 | >set_8051_sfr_ignores_clock |
---|
407 | >write_at_stack_pointer_ignores_clock |
---|
408 | >set_8051_sfr_ignores_clock |
---|
409 | >clock_set_clock |
---|
410 | >set_program_counter_ignores_clock // |
---|
411 | ] |
---|
412 | |3: #addr11 cases addr11 #addressing_mode |
---|
413 | normalize nodelta; cases addressing_mode |
---|
414 | normalize nodelta; |
---|
415 | [1,2,3,4,8,9,15,16,17,19: |
---|
416 | #assm whd in ⊢ (% → ?) |
---|
417 | #absurd cases(absurd) |
---|
418 | |5,6,7,10,11,12,13,14: |
---|
419 | whd in ⊢ (% → ?) |
---|
420 | #absurd cases(absurd) |
---|
421 | |18: |
---|
422 | #word11 #irrelevant |
---|
423 | normalize nodelta; |
---|
424 | >set_program_counter_ignores_clock |
---|
425 | >clock_set_clock |
---|
426 | >set_program_counter_ignores_clock // |
---|
427 | ] |
---|
428 | |4: #addr16 cases addr16 #addressing_mode |
---|
429 | normalize nodelta; cases addressing_mode |
---|
430 | normalize nodelta; |
---|
431 | [1,2,3,4,8,9,15,16,17,18: |
---|
432 | #assm whd in ⊢ (% → ?) |
---|
433 | #absurd cases(absurd) |
---|
434 | |5,6,7,10,11,12,13,14: |
---|
435 | whd in ⊢ (% → ?) |
---|
436 | #absurd cases(absurd) |
---|
437 | |19: |
---|
438 | #word #irrelevant |
---|
439 | normalize nodelta; |
---|
440 | >set_program_counter_ignores_clock |
---|
441 | >clock_set_clock |
---|
442 | >set_program_counter_ignores_clock // |
---|
443 | ] |
---|
444 | |5: #relative cases relative #addressing_mode |
---|
445 | normalize nodelta; cases addressing_mode |
---|
446 | normalize nodelta; |
---|
447 | [1,2,3,4,8,9,15,16,18,19: |
---|
448 | #assm whd in ⊢ (% → ?) |
---|
449 | #absurd cases(absurd) |
---|
450 | |5,6,7,10,11,12,13,14: |
---|
451 | whd in ⊢ (% → ?) |
---|
452 | #absurd cases(absurd) |
---|
453 | |17: |
---|
454 | #byte #irrelevant |
---|
455 | normalize nodelta; |
---|
456 | >set_program_counter_ignores_clock |
---|
457 | >set_program_counter_ignores_clock |
---|
458 | >clock_set_clock // |
---|
459 | ] |
---|
460 | |6: #indirect_dptr cases indirect_dptr #addressing_mode |
---|
461 | normalize nodelta; cases addressing_mode |
---|
462 | normalize nodelta; |
---|
463 | |
---|
464 | |
---|
465 | lemma current_instruction_cost_is_ok: |
---|
466 | ∀s: Status. |
---|
467 | current_instruction_cost s = clock … (execute 1 s) - clock … s. |
---|
468 | #s |
---|
469 | change in match (execute 1 s) with (execute_1 s); |
---|
470 | change in match (execute_1 s) with ( |
---|
471 | let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s) |
---|
472 | (program_counter (BitVectorTrie Byte 16) s) |
---|
473 | in |
---|
474 | execute_1_0 s instr_pc_ticks); |
---|
475 | change in ⊢ (??%?) with ( |
---|
476 | \snd (fetch (code_memory … s) (program_counter … s))); |
---|
477 | normalize nodelta; |
---|
478 | |
---|
479 | let rec compute_max_trace_label_label_cost_is_ok |
---|
480 | (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret) |
---|
481 | (start_status: Status) (final_status: Status) |
---|
482 | (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status) |
---|
483 | on the_trace: |
---|
484 | compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace = |
---|
485 | (clock … final_status) - (clock … start_status) ≝ ? |
---|
486 | and compute_max_trace_label_label_pre_cost_is_ok |
---|
487 | (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret) |
---|
488 | (start_status: Status) (final_status: Status) |
---|
489 | (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status) |
---|
490 | on the_trace: |
---|
491 | compute_max_trace_label_label_pre_cost cost_labels trace_ends_flag start_status final_status the_trace = |
---|
492 | (clock … final_status) - (clock … start_status) ≝ ? |
---|
493 | and compute_max_trace_label_return_cost_is_ok |
---|
494 | (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status) |
---|
495 | (the_trace: trace_label_return cost_labels start_status final_status) |
---|
496 | on the_trace: |
---|
497 | compute_max_trace_label_return_cost cost_labels start_status final_status the_trace = |
---|
498 | (clock … final_status) - (clock … start_status) ≝ ?. |
---|
499 | [1: |
---|
500 | cases the_trace |
---|
501 | #ends_flag #start_status #end_status #label_label_pre_trace |
---|
502 | #labelled_proof |
---|
503 | normalize |
---|
504 | @compute_max_trace_label_label_pre_cost_is_ok |
---|
505 | |3: |
---|
506 | cases the_trace |
---|
507 | [1: |
---|
508 | #status_before #status_after #trace_to_lift |
---|
509 | @compute_max_trace_label_label_cost_is_ok |
---|
510 | |2: |
---|
511 | #status_initial #status_labelled #status_final #labelled_trace #return_trace |
---|
512 | >compute_max_trace_label_return_cost_is_ok % |
---|
513 | ] |
---|
514 | |2: cases the_trace |
---|
515 | [1: #the_status #not_return #not_jump #not_cost |
---|
516 | change in ⊢ (??%?) with (current_instruction_cost the_status); |
---|
517 | @current_instruction_cost_is_ok |
---|
518 | |2: #the_status #is_return |
---|
519 | change in ⊢ (??%?) with (current_instruction_cost the_status); |
---|
520 | @current_instruction_cost_is_ok |
---|
521 | |3: #the_status #is_jump #is_cost |
---|
522 | change in ⊢ (??%?) with (current_instruction_cost the_status); |
---|
523 | @current_instruction_cost_is_ok |
---|
524 | |4: #end_flag #pre_fun_call #after_fun_call #final #is_call |
---|
525 | #next_instruction_coherence #call_trace #final_trace |
---|
526 | change in ⊢ (??%?) with ( |
---|
527 | let current_instruction_cost ≝ current_instruction_cost pre_fun_call in |
---|
528 | let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in |
---|
529 | let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in |
---|
530 | call_trace_cost + current_instruction_cost + final_trace_cost) |
---|
531 | normalize nodelta; |
---|
532 | >current_instruction_cost_is_ok |
---|
533 | >compute_max_trace_label_return_cost_is_ok |
---|
534 | >compute_max_trace_label_label_pre_cost_is_ok |
---|
535 | generalize in match next_instruction_coherence; |
---|
536 | change in ⊢ (% → ?) with ( |
---|
537 | let size ≝ current_instruction_cost pre_fun_call in |
---|
538 | let pc_before ≝ program_counter … pre_fun_call in |
---|
539 | let pc_after ≝ program_counter … after_fun_call in |
---|
540 | let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in |
---|
541 | sum = pc_after) |
---|
542 | normalize nodelta; |
---|
543 | >(plus_minus_rearrangement |
---|
544 | (clock (BitVectorTrie Byte 16) after_fun_call) |
---|
545 | (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)) |
---|
546 | (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?); |
---|
547 | |5: #end_flag #status_pre #status_end #tail_trace #is_not_call |
---|
548 | #is_not_jump #is_not_ret #is_not_labelled |
---|
549 | change in ⊢ (??%?) with ( |
---|
550 | let current_instruction_cost ≝ current_instruction_cost status_pre in |
---|
551 | let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in |
---|
552 | current_instruction_cost + tail_trace_cost) |
---|
553 | normalize nodelta; |
---|
554 | >compute_max_trace_label_label_pre_cost_is_ok |
---|
555 | >current_instruction_cost_is_ok |
---|
556 | ] |
---|
557 | ] |
---|
558 | qed. |
---|
559 | |
---|
560 | let rec compute_max_trace_label_ret_cost_is_ok |
---|
561 | (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status) |
---|
562 | (the_trace: trace_label_return cost_labels start_status final_status) |
---|
563 | on the_trace: |
---|
564 | compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace = |
---|
565 | (clock … final_status) - (clock … start_status) ≝ |
---|
566 | match the_trace with |
---|
567 | [ tlr_base before after trace_to_lift ⇒ ? |
---|
568 | | tlr_step initial pre_fun_call pre_fun_call_trace start_fun_call end_fun_call |
---|
569 | fun_call_trace pre_start_fun_call_coherence ⇒ ? |
---|
570 | ] |
---|
571 | and compute_max_trace_label_label_pre_cost_is_ok |
---|
572 | (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret) |
---|
573 | (start_status: Status) (final_status: Status) |
---|
574 | (the_trace: trace_label_label_pre cost_labels ends_flag start_status final_status) |
---|
575 | on the_trace: |
---|
576 | compute_max_trace_label_label_pre_cost cost_labels ends_flag start_status final_status the_trace = |
---|
577 | (clock … final_status) - (clock … start_status) ≝ |
---|
578 | match the_trace with |
---|
579 | [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ ? |
---|
580 | | tllp_base_return the_status is_return ⇒ ? |
---|
581 | | tllp_base_jump the_status cost_label is_jump is_cost ⇒ ? |
---|
582 | | tllp_step_call end_flag pre_fun_call start_fun_call end_fun_call after_fun_call final |
---|
583 | fun_call_trace is_call statuses_related pre_start_fun_call_coherence |
---|
584 | end_after_fun_call_coherence after_fun_call_trace ⇒ ? |
---|
585 | | tllp_step_default end_flag start initial end initial_end_trace not_call |
---|
586 | not_jump not_return not_cost ⇒ ? |
---|
587 | ] |
---|
588 | and compute_max_trace_label_label_cost_is_ok |
---|
589 | (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret) |
---|
590 | (start_status: Status) (final_status: Status) |
---|
591 | (the_trace: trace_label_label cost_labels ends_flag start_status final_status) |
---|
592 | on the_trace: |
---|
593 | compute_max_trace_label_label_cost cost_labels ends_flag start_status final_status the_trace = |
---|
594 | (clock … final_status) - (clock … start_status) ≝ |
---|
595 | match the_trace with |
---|
596 | [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ? |
---|
597 | ]. |
---|
598 | [8: @(compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag initial final given_trace) |
---|
599 | |1: @(compute_max_trace_label_label_cost_is_ok cost_labels ends_with_ret before after trace_to_lift) |
---|
600 | |4: normalize |
---|
601 | @minus_n_n |
---|
602 | |3: normalize |
---|
603 | @minus_n_n |
---|
604 | |5: normalize |
---|
605 | @minus_n_n |
---|
606 | |6: letin fun_call_cost_ok ≝ (compute_max_trace_label_ret_cost_is_ok cost_labels start_fun_call end_fun_call fun_call_trace) |
---|
607 | letin the_trace_cost_ok ≝ (compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag start_status final_status the_trace) |
---|
608 | |*: |
---|
609 | ] |
---|
610 | qed. |
---|
611 | |
---|
612 | lemma compute_max_trace_label_ret_cost_is_ok: |
---|
613 | ∀cost_labels: BitVectorTrie Byte 16. |
---|
614 | ∀start_status: Status. |
---|
615 | ∀final_status: Status. |
---|
616 | ∀the_trace: trace_label_return cost_labels start_status final_status. |
---|
617 | compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace = |
---|
618 | (clock … final_status) - (clock … start_status). |
---|
619 | #COST_LABELS #START_STATUS #FINAL_STATUS #THE_TRACE |
---|
620 | elim THE_TRACE |
---|
621 | |
---|
622 | lemma trace_lab_rec_cost_ok: |
---|
623 | ∀p: trace_lab_rec. |
---|
624 | trace_lab_rec_cost p = Timer (last p) - Timer (first p). |
---|
625 | |
---|
626 | let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝ |
---|
627 | match p with |
---|
628 | [ call ⇒ DO NOT ADD ANYTHING |
---|
629 | | _ ⇒ DO ADD ]. |
---|
630 | |
---|
631 | let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat. |
---|
632 | | (call b bf tr af tl) as self ⇒ |
---|
633 | trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr + |
---|
634 | trace_lab_rec_cost' tl |
---|
635 | |
---|
636 | theorem main_lemma: |
---|
637 | ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p. |
---|
638 | |
---|
639 | axiom lemma1: |
---|
640 | ∀p: simple_path. |
---|
641 | traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p. |
---|
642 | |
---|
643 | axiom lemma2: |
---|
644 | ∀s,l,cost_map. |
---|
645 | is_labelled l s → |
---|
646 | traverse_cost_internal s = cost_map l. |
---|
647 | |
---|
648 | axiom main_statement: |
---|
649 | ∀s. |
---|
650 | ∀cost_map. |
---|
651 | let p ≝ compute_simple_path0 s in |
---|
652 | ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p. |
---|
653 | |
---|
654 | axiom main_statement: |
---|
655 | ∀s. |
---|
656 | ∀cost_map. |
---|
657 | let p ≝ compute_simple_path0 s in |
---|
658 | execute' (path_length p) s = 〈s',τ〉 → |
---|
659 | Timer s' - Timer s = ∑ τ cost_map. |
---|