source: src/ASM/CostsProof.ma @ 1514

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

changes from today. matita keeps dieing

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