source: src/ASM/CostsProof.ma @ 1534

Last change on this file since 1534 was 1534, checked in by mulligan, 8 years ago

committing my changes to interpret to prevent any further conflicts

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 _ ⇒ False
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  | JMP ⇒ True (* XXX: is function pointer call *)
34  | _ ⇒ False
35  ].
36
37definition next_instruction ≝
38  λs: Status.
39  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
40    instruction.
41
42inductive trace_ends_with_ret: Type[0] ≝
43  | ends_with_ret: trace_ends_with_ret
44  | doesnt_end_with_ret: trace_ends_with_ret.
45
46definition 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
55definition current_instruction_cost ≝
56  λs: Status.
57    \snd (fetch (code_memory … s) (program_counter … s)).
58
59definition 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
68definition current_instruction ≝
69  λs: Status.
70  let pc ≝ program_counter … s in
71  \fst (\fst (fetch … (code_memory … s) pc)).
72
73definition 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
82inductive 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
95with 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
103with 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
146definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
147
148lemma 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
158let 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  ]
167and 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  ]
190and 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
202lemma 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  ]
222qed.
223
224lemma 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  ]
235qed.
236
237lemma 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  ]
257qed.
258
259include alias "arithmetics/nat.ma".
260
261lemma plus_minus_rearrangement_1:
262  ∀m, n, o: nat.
263  ∀proof_n_m: n < m.
264  ∀proof_m_o: m < o.
265    (m - n) + (o - m) = o - n.
266  #m #n #o
267  elim m
268  [1: #proof_n_m
269      cases(lt_to_not_zero … proof_n_m)
270  |2: #m' #ind_hyp
271      #proof_n_m' #proof_m_o
272      >minus_Sn_m
273      [2: normalize in proof_n_m';
274          @le_S_S_to_le
275          assumption
276      |1: >eq_minus_S_pred
277          >pred_minus_1
278          [1: >(succ_m_plus_one (m' - n))
279              >(associative_plus (m' - n) 1 (o - m' - 1))
280              <commutative_plus in match (1 + (o - m' - 1));
281              <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1);
282              [1: >ind_hyp
283                [1: %
284                |2: normalize
285                    normalize in proof_m_o;
286                    @le_S_S_to_le
287                    @(le_S ? ? proof_m_o)
288                |3: cases daemon (* XXX: problem here *)
289                ]
290              |2: normalize in proof_m_o;
291                  normalize
292                  @le_S_S_to_le
293                  @(le_S (S (S m')) o proof_m_o)
294              ]
295          |2: normalize
296              normalize in proof_m_o;
297              @le_S_S_to_le
298              @(le_S (S (S m')) o proof_m_o)
299          ]
300      ]
301  ]
302qed.
303
304axiom plus_minus_rearrangement_2:
305  ∀m, n, o: nat.
306    (m - n) + (n - o) = m - o.
307
308example set_program_counter_ignores_clock:
309  ∀s: Status.
310  ∀pc: Word.
311    clock … (set_program_counter … s pc) = clock … s.
312  #s #pc %
313qed.
314
315example set_low_internal_ram_ignores_clock:
316  ∀s: Status.
317  ∀ram: BitVectorTrie Byte 7.
318    clock … (set_low_internal_ram … s ram) = clock … s.
319  #s #ram %
320qed.
321
322example set_8051_sfr_ignores_clock:
323  ∀s: Status.
324  ∀sfr: SFR8051.
325  ∀v: Byte.
326    clock … (set_8051_sfr ? s sfr v) = clock … s.
327  #s #sfr #v %
328qed.
329
330example clock_set_clock:
331  ∀s: Status.
332  ∀v.
333    clock … (set_clock … s v) = v.
334  #s #v %
335qed.
336
337example write_at_stack_pointer_ignores_clock:
338  ∀s: Status.
339  ∀sp: Byte.
340    clock … (write_at_stack_pointer … s sp) = clock … s.
341  #s #sp
342  change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp); with (
343      let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in
344        ?);
345  normalize nodelta;
346  cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP))
347  #nu #nl normalize nodelta;
348  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
349  [ normalize nodelta; %
350  | normalize nodelta; %
351  ]
352qed.
353
354example status_execution_progresses_processor_clock:
355  ∀s: Status.
356    clock … s ≤ clock … (execute 1 s).
357  #s
358  change in match (execute 1 s) with (execute_1 s);
359  change in match (execute_1 s) with (
360    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
361                               (program_counter (BitVectorTrie Byte 16) s)
362    in 
363      execute_1_0 s instr_pc_ticks);
364  normalize nodelta;
365  whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
366     (program_counter (BitVectorTrie Byte 16) s)));
367  normalize nodelta;
368  cases (fetch (code_memory (BitVectorTrie Byte 16) s)
369           (program_counter (BitVectorTrie Byte 16) s))
370  #instruction_pc #ticks
371  normalize nodelta;
372  cases instruction_pc
373  #instruction #pc
374  cases instruction
375  [1:
376    #addr11 cases addr11 #addressing_mode
377    normalize nodelta; cases addressing_mode
378    normalize nodelta;
379    [1,2,3,4,8,9,15,16,17,19:
380      #assm whd in ⊢ (% → ?)
381      #absurd cases(absurd)
382    |5,6,7,10,11,12,13,14:
383      whd in ⊢ (% → ?)
384      #absurd cases(absurd)
385    |18:
386      #addr11 #irrelevant
387      normalize nodelta;
388      >set_program_counter_ignores_clock
389      normalize nodelta;
390      >set_program_counter_ignores_clock
391      >write_at_stack_pointer_ignores_clock
392      >set_8051_sfr_ignores_clock
393      >write_at_stack_pointer_ignores_clock
394      >set_8051_sfr_ignores_clock
395      >clock_set_clock //
396    ]
397  |2:
398    #addr16 cases addr16 #addressing_mode
399    normalize nodelta; cases addressing_mode
400    normalize nodelta;
401    [1,2,3,4,8,9,15,16,17,18:
402      #assm whd in ⊢ (% → ?)
403      #absurd cases(absurd)
404    |5,6,7,10,11,12,13,14:
405      whd in ⊢ (% → ?)
406      #absurd cases(absurd)
407    |19:
408      #addr16 #irrelevant
409      normalize nodelta;
410      >set_program_counter_ignores_clock
411      >write_at_stack_pointer_ignores_clock
412      >set_8051_sfr_ignores_clock
413      >write_at_stack_pointer_ignores_clock
414      >set_8051_sfr_ignores_clock
415      >clock_set_clock
416      >set_program_counter_ignores_clock //
417    ]
418  |3: #addr11 cases addr11 #addressing_mode
419      normalize nodelta; cases addressing_mode
420      normalize nodelta;
421      [1,2,3,4,8,9,15,16,17,19:
422        #assm whd in ⊢ (% → ?)
423        #absurd cases(absurd)
424      |5,6,7,10,11,12,13,14:
425        whd in ⊢ (% → ?)
426        #absurd cases(absurd)
427      |18:
428        #word11 #irrelevant
429        normalize nodelta;
430        >set_program_counter_ignores_clock
431        >clock_set_clock
432        >set_program_counter_ignores_clock //
433      ]
434  |4: #addr16 cases addr16 #addressing_mode
435      normalize nodelta; cases addressing_mode
436      normalize nodelta;
437      [1,2,3,4,8,9,15,16,17,18:
438        #assm whd in ⊢ (% → ?)
439        #absurd cases(absurd)
440      |5,6,7,10,11,12,13,14:
441        whd in ⊢ (% → ?)
442        #absurd cases(absurd)
443      |19:
444        #word #irrelevant
445        normalize nodelta;
446        >set_program_counter_ignores_clock
447        >clock_set_clock
448        >set_program_counter_ignores_clock //
449      ]
450  |5: #relative cases relative #addressing_mode
451      normalize nodelta; cases addressing_mode
452      normalize nodelta;
453      [1,2,3,4,8,9,15,16,18,19:
454        #assm whd in ⊢ (% → ?)
455        #absurd cases(absurd)
456      |5,6,7,10,11,12,13,14:
457        whd in ⊢ (% → ?)
458        #absurd cases(absurd)
459      |17:
460        #byte #irrelevant
461        normalize nodelta;
462        >set_program_counter_ignores_clock
463        >set_program_counter_ignores_clock
464        >clock_set_clock //
465      ]
466  |6: #indirect_dptr cases indirect_dptr #addressing_mode
467      normalize nodelta; cases addressing_mode
468      normalize nodelta;
469      [1,2,3,4,8,9,15,16,17,18,19:
470        #assm whd in ⊢ (% → ?)
471        #absurd cases(absurd)
472      |5,6,7,10,11,12,14:
473        whd in ⊢ (% → ?)
474        #absurd cases(absurd)
475      |13:
476        #irrelevant
477        normalize nodelta;
478        >set_program_counter_ignores_clock
479        >set_program_counter_ignores_clock
480        >clock_set_clock //
481      ]
482  |8: cases daemon (* XXX: my god *)
483  |7: #acc_a cases acc_a #addressing_mode
484      normalize nodelta; cases addressing_mode
485      normalize nodelta;
486      [1,2,3,4,8,9,15,16,17,18,19:
487        #assm whd in ⊢ (% → ?)
488        #absurd cases(absurd)
489      |6,7,10,11,12,13,14:
490        whd in ⊢ (% → ?)
491        #absurd cases(absurd)
492      |5:
493        #irrelevant #acc_dptr_acc_pc
494        normalize nodelta;
495        cases daemon (* XXX: my god *)
496      ]
497  ]
498qed.
499
500lemma current_instruction_cost_is_ok:
501  ∀s: Status.
502    current_instruction_cost s = clock … (execute 1 s) - clock … s.
503  #s
504  change in match (execute 1 s) with (execute_1 s);
505  change in match (execute_1 s) with (
506    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
507                               (program_counter (BitVectorTrie Byte 16) s)
508    in 
509      execute_1_0 s instr_pc_ticks);
510  change in ⊢ (??%?) with (
511    \snd (fetch (code_memory … s) (program_counter … s)));
512  normalize nodelta;
513  whd in match (
514    execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
515     (program_counter (BitVectorTrie Byte 16) s)));
516  normalize nodelta;
517  cases (fetch (code_memory (BitVectorTrie Byte 16) s)
518           (program_counter (BitVectorTrie Byte 16) s));
519  #instr_pc #ticks normalize nodelta;
520  cases (\fst instr_pc)
521  [1:
522    #addr11 normalize nodelta;
523    cases addr11 #addressing_mode
524    cases addressing_mode
525    [1,2,3,4,8,9,15,16,17,19:
526      #assm whd in ⊢ (% → ?)
527      #absurd cases(absurd)
528    |5,6,7,10,11,12,13,14:
529      whd in ⊢ (% → ?)
530      #absurd cases(absurd)
531    |18:
532      #word11 #irrelevant normalize nodelta;
533      >set_program_counter_ignores_clock
534      >write_at_stack_pointer_ignores_clock
535      >set_8051_sfr_ignores_clock
536      >write_at_stack_pointer_ignores_clock
537      >set_8051_sfr_ignores_clock
538      >clock_set_clock
539      >set_program_counter_ignores_clock
540      >commutative_plus
541      <plus_minus
542      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
543      %
544    ]
545  |2:
546    #addr16 cases addr16 #addressing_mode
547    normalize nodelta; cases addressing_mode
548    normalize nodelta;
549    [1,2,3,4,8,9,15,16,17,18:
550      #assm whd in ⊢ (% → ?)
551      #absurd cases(absurd)
552    |5,6,7,10,11,12,13,14:
553      whd in ⊢ (% → ?)
554      #absurd cases(absurd)
555    |19:
556      #addr16 #irrelevant
557      normalize nodelta;
558      >set_program_counter_ignores_clock
559      >write_at_stack_pointer_ignores_clock
560      >set_8051_sfr_ignores_clock
561      >write_at_stack_pointer_ignores_clock
562      >set_8051_sfr_ignores_clock
563      >clock_set_clock
564      >set_program_counter_ignores_clock
565      >commutative_plus
566      <plus_minus
567      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
568      %
569    ]
570  |3:
571    #addr11 cases addr11 #addressing_mode
572    normalize nodelta; cases addressing_mode
573    normalize nodelta;
574    [1,2,3,4,8,9,15,16,17,19:
575      #assm whd in ⊢ (% → ?)
576      #absurd cases(absurd)
577    |5,6,7,10,11,12,13,14:
578      whd in ⊢ (% → ?)
579      #absurd cases(absurd)
580    |18:
581      #word11 #irrelevant
582      normalize nodelta;
583      >set_program_counter_ignores_clock
584      >clock_set_clock
585      >set_program_counter_ignores_clock
586      >commutative_plus
587      <plus_minus
588      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
589      %
590    ]
591  |4:
592    #addr16 cases addr16 #addressing_mode
593    normalize nodelta; cases addressing_mode
594    normalize nodelta;
595    [1,2,3,4,8,9,15,16,17,18:
596      #assm whd in ⊢ (% → ?)
597      #absurd cases(absurd)
598    |5,6,7,10,11,12,13,14:
599      whd in ⊢ (% → ?)
600      #absurd cases(absurd)
601    |19:
602      #word #irrelevant
603      normalize nodelta;
604      >set_program_counter_ignores_clock
605      >clock_set_clock
606      >set_program_counter_ignores_clock
607      >commutative_plus
608      <plus_minus
609      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
610      %
611    ]
612  |5:
613    #relative cases relative #addressing_mode
614    normalize nodelta; cases addressing_mode
615    normalize nodelta;
616    [1,2,3,4,8,9,15,16,18,19:
617      #assm whd in ⊢ (% → ?)
618      #absurd cases(absurd)
619    |5,6,7,10,11,12,13,14:
620      whd in ⊢ (% → ?)
621      #absurd cases(absurd)
622    |17:
623      #byte #irrelevant
624      normalize nodelta;
625      >set_program_counter_ignores_clock
626      >set_program_counter_ignores_clock
627      >clock_set_clock
628      >commutative_plus
629      <plus_minus
630      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
631      %
632    ]
633  |6:
634    #indirect_dptr cases indirect_dptr #addressing_mode
635    normalize nodelta; cases addressing_mode
636    normalize nodelta;
637    [1,2,3,4,8,9,15,16,17,18,19:
638      #assm whd in ⊢ (% → ?)
639      #absurd cases(absurd)
640    |5,6,7,10,11,12,14:
641      whd in ⊢ (% → ?)
642      #absurd cases(absurd)
643    |13:
644      #irrelevant
645      normalize nodelta;
646      >set_program_counter_ignores_clock
647      >set_program_counter_ignores_clock
648      >clock_set_clock
649      >commutative_plus
650      <plus_minus
651      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
652      %
653    ]
654  |7:
655    #acc_a cases acc_a #addressing_mode
656    normalize nodelta; cases addressing_mode
657    normalize nodelta;
658    [1,2,3,4,8,9,15,16,17,18,19:
659      #assm whd in ⊢ (% → ?)
660      #absurd cases(absurd)
661    |6,7,10,11,12,13,14:
662      whd in ⊢ (% → ?)
663      #absurd cases(absurd)
664    |5:
665      #irrelevant #acc_dptr_acc_pc
666      normalize nodelta;
667      cases daemon (* XXX: todo *)
668    ]
669  |8: cases daemon (* XXX: todo *)
670  ]
671qed.
672
673let rec compute_max_trace_label_label_cost_is_ok
674  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
675    (start_status: Status) (final_status: Status)
676      (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
677      on the_trace:
678        compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
679          (clock … final_status) - (clock … start_status) ≝ ?
680and compute_max_trace_label_label_pre_cost_is_ok
681  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
682    (start_status: Status) (final_status: Status)
683      (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
684        on the_trace:
685          compute_max_trace_label_label_pre_cost cost_labels trace_ends_flag start_status final_status the_trace =
686            (clock … final_status) - (clock … start_status) ≝ ?
687and compute_max_trace_label_return_cost_is_ok
688  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
689    (the_trace: trace_label_return cost_labels start_status final_status)
690      on the_trace:
691        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
692          (clock … final_status) - (clock … start_status) ≝ ?.
693  [1:
694    cases the_trace
695    #ends_flag #start_status #end_status #label_label_pre_trace
696    #labelled_proof
697    normalize
698    @compute_max_trace_label_label_pre_cost_is_ok
699  |3:
700    cases the_trace
701    [1:
702      #status_before #status_after #trace_to_lift
703      @compute_max_trace_label_label_cost_is_ok
704    |2:
705      #status_initial #status_labelled #status_final #labelled_trace #return_trace
706      >compute_max_trace_label_return_cost_is_ok %
707    ]
708  |2: cases the_trace
709    [1: #the_status #not_return #not_jump #not_cost
710        change in ⊢ (??%?) with (current_instruction_cost the_status);
711        @current_instruction_cost_is_ok
712    |2: #the_status #is_return
713        change in ⊢ (??%?) with (current_instruction_cost the_status);
714        @current_instruction_cost_is_ok
715    |3: #the_status #is_jump #is_cost
716        change in ⊢ (??%?) with (current_instruction_cost the_status);
717        @current_instruction_cost_is_ok
718    |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
719        #next_instruction_coherence #call_trace #final_trace
720        change in ⊢ (??%?) with (
721          let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
722          let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
723          let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
724            call_trace_cost + current_instruction_cost + final_trace_cost)
725        normalize nodelta;
726        >current_instruction_cost_is_ok
727        >compute_max_trace_label_return_cost_is_ok
728        >compute_max_trace_label_label_pre_cost_is_ok
729        generalize in match next_instruction_coherence;
730        change in ⊢ (% → ?) with (
731          let size ≝ current_instruction_cost pre_fun_call in
732          let pc_before ≝ program_counter … pre_fun_call in
733          let pc_after ≝ program_counter … after_fun_call in
734          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
735            sum = pc_after)
736        normalize nodelta; #relation_pre_after_fun_call
737        >plus_minus_rearrangement_2 in match (
738          (clock (BitVectorTrie Byte 16) after_fun_call
739            -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
740          +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
741            -clock (BitVectorTrie Byte 16) pre_fun_call)));
742        >(plus_minus_rearrangement
743          (clock (BitVectorTrie Byte 16) after_fun_call)
744          (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
745          (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
746    |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
747        #is_not_jump #is_not_ret #is_not_labelled
748        change in ⊢ (??%?) with (
749          let current_instruction_cost ≝ current_instruction_cost status_pre in
750          let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
751            current_instruction_cost + tail_trace_cost)
752        normalize nodelta;
753        >compute_max_trace_label_label_pre_cost_is_ok
754        >current_instruction_cost_is_ok
755    ]
756  ]
757qed.
758       
759let rec compute_max_trace_label_ret_cost_is_ok
760  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
761    (the_trace: trace_label_return cost_labels start_status final_status)
762      on the_trace:
763        compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
764        (clock … final_status) - (clock … start_status) ≝
765  match the_trace with
766  [ tlr_base before after trace_to_lift ⇒ ?
767  | tlr_step initial pre_fun_call pre_fun_call_trace start_fun_call end_fun_call
768      fun_call_trace pre_start_fun_call_coherence ⇒ ?
769  ]
770and compute_max_trace_label_label_pre_cost_is_ok
771  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
772    (start_status: Status) (final_status: Status)
773      (the_trace: trace_label_label_pre cost_labels ends_flag start_status final_status)
774        on the_trace:
775          compute_max_trace_label_label_pre_cost cost_labels ends_flag start_status final_status the_trace =
776            (clock … final_status) - (clock … start_status) ≝
777  match the_trace with
778  [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ ?
779  | tllp_base_return the_status is_return ⇒ ?
780  | tllp_base_jump the_status cost_label is_jump is_cost ⇒ ?
781  | tllp_step_call end_flag pre_fun_call start_fun_call end_fun_call after_fun_call final
782      fun_call_trace is_call statuses_related pre_start_fun_call_coherence
783      end_after_fun_call_coherence after_fun_call_trace ⇒ ?
784  | tllp_step_default end_flag start initial end initial_end_trace not_call
785      not_jump not_return not_cost ⇒ ?
786  ]
787and compute_max_trace_label_label_cost_is_ok
788  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
789    (start_status: Status) (final_status: Status)
790      (the_trace: trace_label_label cost_labels ends_flag start_status final_status)
791        on the_trace:
792          compute_max_trace_label_label_cost cost_labels ends_flag start_status final_status the_trace =
793            (clock … final_status) - (clock … start_status) ≝
794  match the_trace with
795  [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
796  ].
797  [8: @(compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag initial final given_trace)
798  |1: @(compute_max_trace_label_label_cost_is_ok cost_labels ends_with_ret before after trace_to_lift)
799  |4: normalize
800      @minus_n_n
801  |3: normalize
802      @minus_n_n
803  |5: normalize
804      @minus_n_n
805  |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)
806      letin the_trace_cost_ok ≝ (compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag start_status final_status the_trace)
807  |*:
808  ]
809qed.
810 
811lemma compute_max_trace_label_ret_cost_is_ok:
812  ∀cost_labels: BitVectorTrie Byte 16.
813  ∀start_status: Status.
814  ∀final_status: Status.
815  ∀the_trace: trace_label_return cost_labels start_status final_status.
816    compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
817      (clock … final_status) - (clock … start_status).
818  #COST_LABELS #START_STATUS #FINAL_STATUS #THE_TRACE
819  elim THE_TRACE
820
821lemma trace_lab_rec_cost_ok:
822 ∀p: trace_lab_rec.
823  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
824
825let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
826 match p with
827 [ call ⇒ DO NOT ADD ANYTHING
828 | _ ⇒ DO ADD ].
829
830let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
831 | (call b bf tr af tl) as self ⇒
832    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
833    trace_lab_rec_cost' tl
834
835theorem main_lemma:
836 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
837
838axiom lemma1:
839 ∀p: simple_path.
840  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
841
842axiom lemma2:
843 ∀s,l,cost_map.
844  is_labelled l s →
845   traverse_cost_internal s = cost_map l.
846
847axiom main_statement:
848 ∀s.
849 ∀cost_map.
850 let p ≝ compute_simple_path0 s in
851 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
852
853axiom main_statement:
854 ∀s.
855 ∀cost_map.
856 let p ≝ compute_simple_path0 s in
857  execute' (path_length p) s = 〈s',τ〉 →
858   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.