source: src/ASM/CostsProof.ma @ 1522

Last change on this file since 1522 was 1522, checked in by mulligan, 8 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.