source: src/ASM/CostsProof.ma @ 1522

Last change on this file since 1522 was 1522, checked in by mulligan, 10 years ago

changes to preamble and lin to asm pass, resolved conflict in interpret

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