source: src/ASM/CostsProof.ma @ 1511

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

proofs, added, changes to execute_1_0 function therefore required to remove excess lets

File size: 23.7 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:
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
302example set_program_counter_ignores_clock:
303  ∀s: Status.
304  ∀pc: Word.
305    clock … (set_program_counter … s pc) = clock … s.
306  #s #pc %
307qed.
308
309example set_low_internal_ram_ignores_clock:
310  ∀s: Status.
311  ∀ram: BitVectorTrie Byte 7.
312    clock … (set_low_internal_ram … s ram) = clock … s.
313  #s #ram %
314qed.
315
316example set_8051_sfr_ignores_clock:
317  ∀s: Status.
318  ∀sfr: SFR8051.
319  ∀v: Byte.
320    clock … (set_8051_sfr ? s sfr v) = clock … s.
321  #s #sfr #v %
322qed.
323
324example clock_set_clock:
325  ∀s: Status.
326  ∀v.
327    clock … (set_clock … s v) = v.
328  #s #v %
329qed.
330
331example write_at_stack_pointer_ignores_clock:
332  ∀s: Status.
333  ∀sp: Byte.
334    clock … (write_at_stack_pointer … s sp) = clock … s.
335  #s #sp
336  change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with (
337      let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in
338        ?);
339  normalize nodelta;
340  cases(split bool 4 4 (get_8051_sfr (BitVectorTrie Byte 16) s SFR_SP))
341  #nu #nl normalize nodelta;
342  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
343  [ normalize nodelta; %
344  | normalize nodelta; %
345  ]
346qed.
347
348example status_execution_progresses_processor_clock:
349  ∀s: Status.
350    clock … s ≤ clock … (execute 1 s).
351  #s
352  change in match (execute 1 s) with (execute_1 s);
353  change in match (execute_1 s) with (
354    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
355                               (program_counter (BitVectorTrie Byte 16) s)
356    in 
357      execute_1_0 s instr_pc_ticks);
358  normalize nodelta;
359  whd in match (execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
360     (program_counter (BitVectorTrie Byte 16) s)));
361  normalize nodelta;
362  cases (fetch (code_memory (BitVectorTrie Byte 16) s)
363           (program_counter (BitVectorTrie Byte 16) s))
364  #instruction_pc #ticks
365  normalize nodelta;
366  cases instruction_pc
367  #instruction #pc
368  cases instruction
369  [1:
370    #addr11 cases addr11 #addressing_mode
371    normalize nodelta; cases addressing_mode
372    normalize nodelta;
373    [1,2,3,4,8,9,15,16,17,19:
374      #assm whd in ⊢ (% → ?)
375      #absurd cases(absurd)
376    |5,6,7,10,11,12,13,14:
377      whd in ⊢ (% → ?)
378      #absurd cases(absurd)
379    |18:
380      #addr11 #irrelevant
381      normalize nodelta;
382      >set_program_counter_ignores_clock
383      normalize nodelta;
384      >set_program_counter_ignores_clock
385      >write_at_stack_pointer_ignores_clock
386      >set_8051_sfr_ignores_clock
387      >write_at_stack_pointer_ignores_clock
388      >set_8051_sfr_ignores_clock
389      >clock_set_clock //
390    ]
391  |2:
392    #addr16 cases addr16 #addressing_mode
393    normalize nodelta; cases addressing_mode
394    normalize nodelta;
395    [1,2,3,4,8,9,15,16,17,18:
396      #assm whd in ⊢ (% → ?)
397      #absurd cases(absurd)
398    |5,6,7,10,11,12,13,14:
399      whd in ⊢ (% → ?)
400      #absurd cases(absurd)
401    |19:
402      #addr16 #irrelevant
403      normalize nodelta;
404      >set_program_counter_ignores_clock
405      >write_at_stack_pointer_ignores_clock
406      >set_8051_sfr_ignores_clock
407      >write_at_stack_pointer_ignores_clock
408      >set_8051_sfr_ignores_clock
409      >clock_set_clock
410      >set_program_counter_ignores_clock //
411    ]
412  |3: #addr11 cases addr11 #addressing_mode
413      normalize nodelta; cases addressing_mode
414      normalize nodelta;
415      [1,2,3,4,8,9,15,16,17,19:
416        #assm whd in ⊢ (% → ?)
417        #absurd cases(absurd)
418      |5,6,7,10,11,12,13,14:
419        whd in ⊢ (% → ?)
420        #absurd cases(absurd)
421      |18:
422        #word11 #irrelevant
423        normalize nodelta;
424        >set_program_counter_ignores_clock
425        >clock_set_clock
426        >set_program_counter_ignores_clock //
427      ]
428  |4: #addr16 cases addr16 #addressing_mode
429      normalize nodelta; cases addressing_mode
430      normalize nodelta;
431      [1,2,3,4,8,9,15,16,17,18:
432        #assm whd in ⊢ (% → ?)
433        #absurd cases(absurd)
434      |5,6,7,10,11,12,13,14:
435        whd in ⊢ (% → ?)
436        #absurd cases(absurd)
437      |19:
438        #word #irrelevant
439        normalize nodelta;
440        >set_program_counter_ignores_clock
441        >clock_set_clock
442        >set_program_counter_ignores_clock //
443      ]
444  |5: #relative cases relative #addressing_mode
445      normalize nodelta; cases addressing_mode
446      normalize nodelta;
447      [1,2,3,4,8,9,15,16,18,19:
448        #assm whd in ⊢ (% → ?)
449        #absurd cases(absurd)
450      |5,6,7,10,11,12,13,14:
451        whd in ⊢ (% → ?)
452        #absurd cases(absurd)
453      |17:
454        #byte #irrelevant
455        normalize nodelta;
456        >set_program_counter_ignores_clock
457        >set_program_counter_ignores_clock
458        >clock_set_clock //
459      ]
460  |6: #indirect_dptr cases indirect_dptr #addressing_mode
461      normalize nodelta; cases addressing_mode
462      normalize nodelta;
463     
464
465lemma current_instruction_cost_is_ok:
466  ∀s: Status.
467    current_instruction_cost s = clock … (execute 1 s) - clock … s.
468  #s
469  change in match (execute 1 s) with (execute_1 s);
470  change in match (execute_1 s) with (
471    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
472                               (program_counter (BitVectorTrie Byte 16) s)
473    in 
474      execute_1_0 s instr_pc_ticks);
475  change in ⊢ (??%?) with (
476    \snd (fetch (code_memory … s) (program_counter … s)));
477  normalize nodelta;
478
479let rec compute_max_trace_label_label_cost_is_ok
480  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
481    (start_status: Status) (final_status: Status)
482      (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
483      on the_trace:
484        compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
485          (clock … final_status) - (clock … start_status) ≝ ?
486and compute_max_trace_label_label_pre_cost_is_ok
487  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
488    (start_status: Status) (final_status: Status)
489      (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
490        on the_trace:
491          compute_max_trace_label_label_pre_cost cost_labels trace_ends_flag start_status final_status the_trace =
492            (clock … final_status) - (clock … start_status) ≝ ?
493and compute_max_trace_label_return_cost_is_ok
494  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
495    (the_trace: trace_label_return cost_labels start_status final_status)
496      on the_trace:
497        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
498          (clock … final_status) - (clock … start_status) ≝ ?.
499  [1:
500    cases the_trace
501    #ends_flag #start_status #end_status #label_label_pre_trace
502    #labelled_proof
503    normalize
504    @compute_max_trace_label_label_pre_cost_is_ok
505  |3:
506    cases the_trace
507    [1:
508      #status_before #status_after #trace_to_lift
509      @compute_max_trace_label_label_cost_is_ok
510    |2:
511      #status_initial #status_labelled #status_final #labelled_trace #return_trace
512      >compute_max_trace_label_return_cost_is_ok %
513    ]
514  |2: cases the_trace
515    [1: #the_status #not_return #not_jump #not_cost
516        change in ⊢ (??%?) with (current_instruction_cost the_status);
517        @current_instruction_cost_is_ok
518    |2: #the_status #is_return
519        change in ⊢ (??%?) with (current_instruction_cost the_status);
520        @current_instruction_cost_is_ok
521    |3: #the_status #is_jump #is_cost
522        change in ⊢ (??%?) with (current_instruction_cost the_status);
523        @current_instruction_cost_is_ok
524    |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
525        #next_instruction_coherence #call_trace #final_trace
526        change in ⊢ (??%?) with (
527          let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
528          let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
529          let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
530            call_trace_cost + current_instruction_cost + final_trace_cost)
531        normalize nodelta;
532        >current_instruction_cost_is_ok
533        >compute_max_trace_label_return_cost_is_ok
534        >compute_max_trace_label_label_pre_cost_is_ok
535        generalize in match next_instruction_coherence;
536        change in ⊢ (% → ?) with (
537          let size ≝ current_instruction_cost pre_fun_call in
538          let pc_before ≝ program_counter … pre_fun_call in
539          let pc_after ≝ program_counter … after_fun_call in
540          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
541            sum = pc_after)
542        normalize nodelta;
543        >(plus_minus_rearrangement
544          (clock (BitVectorTrie Byte 16) after_fun_call)
545          (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
546          (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
547    |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
548        #is_not_jump #is_not_ret #is_not_labelled
549        change in ⊢ (??%?) with (
550          let current_instruction_cost ≝ current_instruction_cost status_pre in
551          let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
552            current_instruction_cost + tail_trace_cost)
553        normalize nodelta;
554        >compute_max_trace_label_label_pre_cost_is_ok
555        >current_instruction_cost_is_ok
556    ]
557  ]
558qed.
559       
560let rec compute_max_trace_label_ret_cost_is_ok
561  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
562    (the_trace: trace_label_return cost_labels start_status final_status)
563      on the_trace:
564        compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
565        (clock … final_status) - (clock … start_status) ≝
566  match the_trace with
567  [ tlr_base before after trace_to_lift ⇒ ?
568  | tlr_step initial pre_fun_call pre_fun_call_trace start_fun_call end_fun_call
569      fun_call_trace pre_start_fun_call_coherence ⇒ ?
570  ]
571and compute_max_trace_label_label_pre_cost_is_ok
572  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
573    (start_status: Status) (final_status: Status)
574      (the_trace: trace_label_label_pre cost_labels ends_flag start_status final_status)
575        on the_trace:
576          compute_max_trace_label_label_pre_cost cost_labels ends_flag start_status final_status the_trace =
577            (clock … final_status) - (clock … start_status) ≝
578  match the_trace with
579  [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ ?
580  | tllp_base_return the_status is_return ⇒ ?
581  | tllp_base_jump the_status cost_label is_jump is_cost ⇒ ?
582  | tllp_step_call end_flag pre_fun_call start_fun_call end_fun_call after_fun_call final
583      fun_call_trace is_call statuses_related pre_start_fun_call_coherence
584      end_after_fun_call_coherence after_fun_call_trace ⇒ ?
585  | tllp_step_default end_flag start initial end initial_end_trace not_call
586      not_jump not_return not_cost ⇒ ?
587  ]
588and compute_max_trace_label_label_cost_is_ok
589  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
590    (start_status: Status) (final_status: Status)
591      (the_trace: trace_label_label cost_labels ends_flag start_status final_status)
592        on the_trace:
593          compute_max_trace_label_label_cost cost_labels ends_flag start_status final_status the_trace =
594            (clock … final_status) - (clock … start_status) ≝
595  match the_trace with
596  [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
597  ].
598  [8: @(compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag initial final given_trace)
599  |1: @(compute_max_trace_label_label_cost_is_ok cost_labels ends_with_ret before after trace_to_lift)
600  |4: normalize
601      @minus_n_n
602  |3: normalize
603      @minus_n_n
604  |5: normalize
605      @minus_n_n
606  |6: letin fun_call_cost_ok ≝ (compute_max_trace_label_ret_cost_is_ok cost_labels start_fun_call end_fun_call fun_call_trace)
607      letin the_trace_cost_ok ≝ (compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag start_status final_status the_trace)
608  |*:
609  ]
610qed.
611 
612lemma compute_max_trace_label_ret_cost_is_ok:
613  ∀cost_labels: BitVectorTrie Byte 16.
614  ∀start_status: Status.
615  ∀final_status: Status.
616  ∀the_trace: trace_label_return cost_labels start_status final_status.
617    compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
618      (clock … final_status) - (clock … start_status).
619  #COST_LABELS #START_STATUS #FINAL_STATUS #THE_TRACE
620  elim THE_TRACE
621
622lemma trace_lab_rec_cost_ok:
623 ∀p: trace_lab_rec.
624  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
625
626let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
627 match p with
628 [ call ⇒ DO NOT ADD ANYTHING
629 | _ ⇒ DO ADD ].
630
631let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
632 | (call b bf tr af tl) as self ⇒
633    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
634    trace_lab_rec_cost' tl
635
636theorem main_lemma:
637 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
638
639axiom lemma1:
640 ∀p: simple_path.
641  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
642
643axiom lemma2:
644 ∀s,l,cost_map.
645  is_labelled l s →
646   traverse_cost_internal s = cost_map l.
647
648axiom main_statement:
649 ∀s.
650 ∀cost_map.
651 let p ≝ compute_simple_path0 s in
652 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
653
654axiom main_statement:
655 ∀s.
656 ∀cost_map.
657 let p ≝ compute_simple_path0 s in
658  execute' (path_length p) s = 〈s',τ〉 →
659   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.