source: src/ASM/CostsProof.ma @ 1544

Last change on this file since 1544 was 1544, checked in by sacerdot, 8 years ago

StructuredTraces? inhabited for object code.

File size: 24.1 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4include "common/StructuredTraces.ma".
5
6definition current_instruction ≝
7  λs: Status.
8  let pc ≝ program_counter … s in
9  \fst (\fst (fetch … (code_memory … s) pc)).
10
11definition ASM_classify: Status → status_class ≝
12 λs.
13  match current_instruction s with
14   [ RealInstruction pre ⇒
15     match pre with
16      [ RET ⇒ cl_return
17      | JZ _ ⇒ cl_jump
18      | JNZ _ ⇒ cl_jump
19      | JC _ ⇒ cl_jump
20      | JNC _ ⇒ cl_jump
21      | JB _ _ ⇒ cl_jump
22      | JNB _ _ ⇒ cl_jump
23      | JBC _ _ ⇒ cl_jump
24      | CJNE _ _ ⇒ cl_jump
25      | DJNZ _ _ ⇒ cl_jump
26      | _ ⇒ cl_other
27      ]
28   | ACALL _ ⇒ cl_call
29   | LCALL _ ⇒ cl_call
30   | JMP _ ⇒ cl_call
31   | AJMP _ ⇒ cl_jump
32   | LJMP _ ⇒ cl_jump
33   | SJMP _ ⇒ cl_jump
34   | _ ⇒ cl_other
35   ].
36
37definition current_instruction_is_labelled ≝
38  λcost_labels: BitVectorTrie Byte 16.
39  λs: Status.
40  let pc ≝ program_counter … s in
41    match lookup_opt … pc cost_labels with
42    [ None ⇒ False
43    | _    ⇒ True
44    ].
45
46definition current_instruction_cost ≝
47  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
48
49definition next_instruction_properly_relates_program_counters ≝
50  λbefore: Status.
51  λafter : Status.
52  let size ≝ current_instruction_cost before in
53  let pc_before ≝ program_counter … before in
54  let pc_after ≝ program_counter … after in
55  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
56    sum = pc_after.
57
58definition ASM_abstract_status: BitVectorTrie Byte 16 → abstract_status ≝
59 λcost_labels.
60  mk_abstract_status
61   Status
62   (λs,s'. eject … (execute_1 s) = s')
63   (λs,class. ASM_classify s = class)
64   (current_instruction_is_labelled cost_labels)
65   next_instruction_properly_relates_program_counters.
66
67(*
68definition next_instruction_is_labelled ≝
69  λcost_labels: BitVectorTrie Byte 16.
70  λs: Status.
71  let pc ≝ program_counter … (execute_1 s) in
72    match lookup_opt … pc cost_labels with
73    [ None ⇒ False
74    | _    ⇒ True
75    ].
76
77definition current_instruction_cost ≝
78  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
79
80definition is_call_p ≝
81  λs.
82  match s with
83  [ ACALL _ ⇒ True
84  | LCALL _ ⇒ True
85  | JMP ⇒ True (* XXX: is function pointer call *)
86  | _ ⇒ False
87  ].
88
89definition next_instruction ≝
90  λs: Status.
91  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
92    instruction.
93
94inductive trace_ends_with_ret: Type[0] ≝
95  | ends_with_ret: trace_ends_with_ret
96  | doesnt_end_with_ret: trace_ends_with_ret.
97
98definition next_instruction_is_labelled ≝
99  λcost_labels: BitVectorTrie Byte 16.
100  λs: Status.
101  let pc ≝ program_counter … (execute 1 s) in
102    match lookup_opt … pc cost_labels with
103    [ None ⇒ False
104    | _    ⇒ True
105    ].
106
107definition next_instruction_properly_relates_program_counters ≝
108  λbefore: Status.
109  λafter : Status.
110  let size ≝ current_instruction_cost before in
111  let pc_before ≝ program_counter … before in
112  let pc_after ≝ program_counter … after in
113  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
114    sum = pc_after.
115
116definition current_instruction ≝
117  λs: Status.
118  let pc ≝ program_counter … s in
119  \fst (\fst (fetch … (code_memory … s) pc)).
120
121definition current_instruction_is_labelled ≝
122  λcost_labels: BitVectorTrie Byte 16.
123  λs: Status.
124  let pc ≝ program_counter … s in
125    match lookup_opt … pc cost_labels with
126    [ None ⇒ False
127    | _    ⇒ True
128    ].
129
130inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
131  | tlr_base:
132      ∀status_before: Status.
133      ∀status_after: Status.
134        trace_label_label cost_labels ends_with_ret status_before status_after →
135        trace_label_return cost_labels status_before status_after
136  | tlr_step:
137      ∀status_initial: Status.
138      ∀status_labelled: Status.
139      ∀status_final: Status.
140          trace_label_label cost_labels doesnt_end_with_ret status_initial status_labelled →
141            trace_label_return cost_labels status_labelled status_final →
142              trace_label_return cost_labels status_initial status_final
143with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
144  | tll_base:
145      ∀ends_flag: trace_ends_with_ret.
146      ∀start_status: Status.
147      ∀end_status: Status.
148        trace_label_label_pre cost_labels ends_flag start_status end_status →
149        current_instruction_is_labelled cost_labels start_status →
150        trace_label_label cost_labels ends_flag start_status end_status
151with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
152  | tllp_base_not_return:
153      ∀start_status: Status.
154        let final_status ≝ execute 1 start_status in
155        current_instruction start_status ≠ (RealInstruction … (RET [[relative]])) →
156        ¬ (is_jump_p (current_instruction start_status)) →
157        current_instruction_is_labelled cost_labels final_status →
158          trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
159  | tllp_base_return:
160      ∀start_status: Status.
161        let final_status ≝ execute 1 start_status in
162          current_instruction start_status = (RealInstruction … (RET [[relative]])) →
163            trace_label_label_pre cost_labels ends_with_ret start_status final_status
164  | tllp_base_jump:
165      ∀start_status: Status.
166        let final_status ≝ execute 1 start_status in
167          is_jump_p (current_instruction start_status) →
168            current_instruction_is_labelled cost_labels final_status →
169              trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
170  | tllp_step_call:
171      ∀end_flag: trace_ends_with_ret.
172      ∀status_pre_fun_call: Status.
173      ∀status_after_fun_call: Status.
174      ∀status_final: Status.
175        let status_start_fun_call ≝ execute 1 status_pre_fun_call in
176          is_call_p (current_instruction status_pre_fun_call) →
177          next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
178          trace_label_return cost_labels status_start_fun_call status_after_fun_call →
179          trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
180            trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
181  | tllp_step_default:
182      ∀end_flag: trace_ends_with_ret.
183      ∀status_pre: Status.
184      ∀status_end: Status.
185        let status_init ≝ execute 1 status_pre in
186          trace_label_label_pre cost_labels end_flag status_init status_end →
187          ¬ (is_call_p (current_instruction status_pre)) →
188          ¬ (is_jump_p (current_instruction status_pre)) →
189          (current_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
190          ¬ (current_instruction_is_labelled cost_labels status_init) →
191            trace_label_label_pre cost_labels end_flag status_pre status_end.
192*)
193
194(* XXX: not us
195definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
196
197lemma simple_path_ok:
198 ∀st: Status.∀H.
199 let p ≝ compute_simple_path0 st H in
200   ∀n.
201    nth_path n p = execute n st ∧
202     (execute' (path_length p) st = 〈st',τ〉 →
203      τ = cost_trace p)
204  ].
205*)
206
207let rec compute_max_trace_label_label_cost
208  (cost_labels: BitVectorTrie Byte 16)
209   (trace_ends_flag: trace_ends_with_ret)
210    (start_status: Status) (final_status: Status)
211      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
212        start_status final_status) on the_trace: nat ≝
213  match the_trace with
214  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
215      compute_max_trace_any_label_cost … given_trace
216  ]
217and compute_max_trace_any_label_cost
218  (cost_labels: BitVectorTrie Byte 16)
219  (trace_ends_flag: trace_ends_with_ret)
220   (start_status: Status) (final_status: Status)
221     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
222       on the_trace: nat ≝
223  match the_trace with
224  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
225  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
226  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
227     _ _ _ call_trace final_trace ⇒
228      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
229      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
230      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
231        call_trace_cost + current_instruction_cost + final_trace_cost
232  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
233      let current_instruction_cost ≝ current_instruction_cost status_pre in
234      let tail_trace_cost ≝
235       compute_max_trace_any_label_cost cost_labels end_flag
236        status_init status_end tail_trace
237      in
238        current_instruction_cost + tail_trace_cost
239  ]
240and compute_max_trace_label_return_cost
241  (cost_labels: BitVectorTrie Byte 16)
242  (start_status: Status) (final_status: Status)
243    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
244      on the_trace: nat ≝
245  match the_trace with
246  [ tlr_base before after trace_to_lift ⇒ compute_max_trace_label_label_cost … trace_to_lift
247  | tlr_step initial labelled final labelled_trace ret_trace ⇒
248      let labelled_cost ≝ compute_max_trace_label_label_cost … labelled_trace in
249      let return_cost ≝ compute_max_trace_label_return_cost … ret_trace in
250        labelled_cost + return_cost
251  ].
252
253(* To be moved *)
254lemma pred_minus_1:
255  ∀m, n: nat.
256  ∀proof: n < m.
257    pred (m - n) = m - n - 1.
258  #m #n
259  cases m
260  [ #proof
261    cases(lt_to_not_zero … proof)
262  | #m' #proof
263    normalize in ⊢ (???%);
264    cases n
265    [ normalize //
266    | #n' normalize
267      cases(m' - n')
268      [ %
269      | #Sm_n'
270        normalize //
271      ]
272    ]
273  ]
274qed.
275
276lemma succ_m_plus_one:
277  ∀m: nat.
278    S m = m + 1.
279 //
280qed.
281
282include alias "arithmetics/nat.ma".
283
284lemma minus_m_n_minus_minus_plus_1:
285  ∀m, n: nat.
286  ∀proof: n < m.
287    m - n = (m - n - 1) + 1.
288 /3 by lt_plus_to_minus_r, plus_minus/
289qed.
290
291lemma plus_minus_rearrangement_1:
292  ∀m, n, o: nat.
293  ∀proof_n_m: n ≤ m.
294  ∀proof_m_o: m ≤ o.
295    (m - n) + (o - m) = o - n.
296  #m #n #o #H1 #H2
297  lapply (minus_to_plus … H1 (refl …)) #K1 >K1
298  lapply (minus_to_plus … H2 (refl …)) #K2 >K2
299  /2 by plus_minus/
300qed.
301
302lemma plus_minus_rearrangement_2:
303  ∀m, n, o: nat. n ≤ m → o ≤ n →
304    (m - n) + (n - o) = m - o.
305 /2 by plus_minus_rearrangement_1/
306qed.
307
308lemma current_instruction_cost_is_ok:
309  ∀s: Status.
310    current_instruction_cost s = clock … (execute 1 s) - clock … s.
311  #s
312  change with (execute_1 s) in match (eject … (execute 1 s));
313  change with (
314    let instr_pc_ticks ≝ fetch (code_memory (BitVectorTrie Byte 16) s)
315                               (program_counter (BitVectorTrie Byte 16) s)
316    in 
317     eject … (execute_1_0 s instr_pc_ticks)) in match (eject … (execute_1 s));
318  change with (
319    \snd (fetch (code_memory … s) (program_counter … s))) in ⊢ (??%?);
320  normalize nodelta;
321  whd in match (
322    execute_1_0 s (fetch (code_memory (BitVectorTrie Byte 16) s)
323     (program_counter (BitVectorTrie Byte 16) s)));
324  normalize nodelta;
325  cases (fetch (code_memory (BitVectorTrie Byte 16) s)
326           (program_counter (BitVectorTrie Byte 16) s));
327  #instr_pc #ticks normalize nodelta;
328  cases (\fst instr_pc)
329  [1:
330    #addr11 normalize nodelta;
331    cases addr11 #addressing_mode
332    cases addressing_mode
333    [1,2,3,4,8,9,15,16,17,19:
334      #assm whd in ⊢ (% → ?)
335      #absurd cases(absurd)
336    |5,6,7,10,11,12,13,14:
337      whd in ⊢ (% → ?)
338      #absurd cases(absurd)
339    |18:
340      #word11 #irrelevant normalize nodelta;
341      >set_program_counter_ignores_clock
342      >write_at_stack_pointer_ignores_clock
343      >set_8051_sfr_ignores_clock
344      >write_at_stack_pointer_ignores_clock
345      >set_8051_sfr_ignores_clock
346      >clock_set_clock
347      >set_program_counter_ignores_clock
348      >commutative_plus
349      <plus_minus
350      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
351      %
352    ]
353  |2:
354    #addr16 cases addr16 #addressing_mode
355    normalize nodelta; cases addressing_mode
356    normalize nodelta;
357    [1,2,3,4,8,9,15,16,17,18:
358      #assm whd in ⊢ (% → ?)
359      #absurd cases(absurd)
360    |5,6,7,10,11,12,13,14:
361      whd in ⊢ (% → ?)
362      #absurd cases(absurd)
363    |19:
364      #addr16 #irrelevant
365      normalize nodelta;
366      >set_program_counter_ignores_clock
367      >write_at_stack_pointer_ignores_clock
368      >set_8051_sfr_ignores_clock
369      >write_at_stack_pointer_ignores_clock
370      >set_8051_sfr_ignores_clock
371      >clock_set_clock
372      >set_program_counter_ignores_clock
373      >commutative_plus
374      <plus_minus
375      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
376      %
377    ]
378  |3:
379    #addr11 cases addr11 #addressing_mode
380    normalize nodelta; cases addressing_mode
381    normalize nodelta;
382    [1,2,3,4,8,9,15,16,17,19:
383      #assm whd in ⊢ (% → ?)
384      #absurd cases(absurd)
385    |5,6,7,10,11,12,13,14:
386      whd in ⊢ (% → ?)
387      #absurd cases(absurd)
388    |18:
389      #word11 #irrelevant
390      normalize nodelta;
391      >set_program_counter_ignores_clock
392      >clock_set_clock
393      >set_program_counter_ignores_clock
394      >commutative_plus
395      <plus_minus
396      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
397      %
398    ]
399  |4:
400    #addr16 cases addr16 #addressing_mode
401    normalize nodelta; cases addressing_mode
402    normalize nodelta;
403    [1,2,3,4,8,9,15,16,17,18:
404      #assm whd in ⊢ (% → ?)
405      #absurd cases(absurd)
406    |5,6,7,10,11,12,13,14:
407      whd in ⊢ (% → ?)
408      #absurd cases(absurd)
409    |19:
410      #word #irrelevant
411      normalize nodelta;
412      >set_program_counter_ignores_clock
413      >clock_set_clock
414      >set_program_counter_ignores_clock
415      >commutative_plus
416      <plus_minus
417      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
418      %
419    ]
420  |5:
421    #relative cases relative #addressing_mode
422    normalize nodelta; cases addressing_mode
423    normalize nodelta;
424    [1,2,3,4,8,9,15,16,18,19:
425      #assm whd in ⊢ (% → ?)
426      #absurd cases(absurd)
427    |5,6,7,10,11,12,13,14:
428      whd in ⊢ (% → ?)
429      #absurd cases(absurd)
430    |17:
431      #byte #irrelevant
432      normalize nodelta;
433      >set_program_counter_ignores_clock
434      >set_program_counter_ignores_clock
435      >clock_set_clock
436      >commutative_plus
437      <plus_minus
438      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
439      %
440    ]
441  |6:
442    #indirect_dptr cases indirect_dptr #addressing_mode
443    normalize nodelta; cases addressing_mode
444    normalize nodelta;
445    [1,2,3,4,8,9,15,16,17,18,19:
446      #assm whd in ⊢ (% → ?)
447      #absurd cases(absurd)
448    |5,6,7,10,11,12,14:
449      whd in ⊢ (% → ?)
450      #absurd cases(absurd)
451    |13:
452      #irrelevant
453      normalize nodelta;
454      >set_program_counter_ignores_clock
455      >set_program_counter_ignores_clock
456      >clock_set_clock
457      >commutative_plus
458      <plus_minus
459      <(minus_n_n (clock (BitVectorTrie Byte 16) s))
460      %
461    ]
462  |7:
463    #acc_a cases acc_a #addressing_mode
464    normalize nodelta; cases addressing_mode
465    normalize nodelta;
466    [1,2,3,4,8,9,15,16,17,18,19:
467      #assm whd in ⊢ (% → ?)
468      #absurd cases(absurd)
469    |6,7,10,11,12,13,14:
470      whd in ⊢ (% → ?)
471      #absurd cases(absurd)
472    |5:
473      #irrelevant #acc_dptr_acc_pc
474      normalize nodelta;
475      cases daemon (* XXX: todo *)
476    ]
477  |8: cases daemon (* XXX: todo *)
478  ]
479qed.
480
481let rec compute_max_trace_label_label_cost_is_ok
482  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
483    (start_status: Status) (final_status: Status)
484      (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
485      on the_trace:
486        compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
487          (clock … final_status) - (clock … start_status) ≝ ?
488and compute_max_trace_label_label_pre_cost_is_ok
489  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
490    (start_status: Status) (final_status: Status)
491      (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
492        on the_trace:
493          compute_max_trace_label_label_pre_cost cost_labels trace_ends_flag start_status final_status the_trace =
494            (clock … final_status) - (clock … start_status) ≝ ?
495and compute_max_trace_label_return_cost_is_ok
496  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
497    (the_trace: trace_label_return cost_labels start_status final_status)
498      on the_trace:
499        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
500          (clock … final_status) - (clock … start_status) ≝ ?.
501  [1:
502    cases the_trace
503    #ends_flag #start_status #end_status #label_label_pre_trace
504    #labelled_proof
505    normalize
506    @compute_max_trace_label_label_pre_cost_is_ok
507  |3:
508    cases the_trace
509    [1:
510      #status_before #status_after #trace_to_lift
511      @compute_max_trace_label_label_cost_is_ok
512    |2:
513      #status_initial #status_labelled #status_final #labelled_trace #return_trace
514      >compute_max_trace_label_return_cost_is_ok %
515    ]
516  |2: cases the_trace
517    [1: #the_status #not_return #not_jump #not_cost
518        change in ⊢ (??%?) with (current_instruction_cost the_status);
519        @current_instruction_cost_is_ok
520    |2: #the_status #is_return
521        change in ⊢ (??%?) with (current_instruction_cost the_status);
522        @current_instruction_cost_is_ok
523    |3: #the_status #is_jump #is_cost
524        change in ⊢ (??%?) with (current_instruction_cost the_status);
525        @current_instruction_cost_is_ok
526    |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
527        #next_instruction_coherence #call_trace #final_trace
528        change in ⊢ (??%?) with (
529          let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
530          let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
531          let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
532            call_trace_cost + current_instruction_cost + final_trace_cost)
533        normalize nodelta;
534        >current_instruction_cost_is_ok
535        >compute_max_trace_label_return_cost_is_ok
536        >compute_max_trace_label_label_pre_cost_is_ok
537        generalize in match next_instruction_coherence;
538        change in ⊢ (% → ?) with (
539          let size ≝ current_instruction_cost pre_fun_call in
540          let pc_before ≝ program_counter … pre_fun_call in
541          let pc_after ≝ program_counter … after_fun_call in
542          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
543            sum = pc_after)
544        normalize nodelta; #relation_pre_after_fun_call
545        >plus_minus_rearrangement_2 in match (
546          (clock (BitVectorTrie Byte 16) after_fun_call
547            -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
548          +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
549            -clock (BitVectorTrie Byte 16) pre_fun_call)));
550        >(plus_minus_rearrangement
551          (clock (BitVectorTrie Byte 16) after_fun_call)
552          (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
553          (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
554    |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
555        #is_not_jump #is_not_ret #is_not_labelled
556        change in ⊢ (??%?) with (
557          let current_instruction_cost ≝ current_instruction_cost status_pre in
558          let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
559            current_instruction_cost + tail_trace_cost)
560        normalize nodelta;
561        >compute_max_trace_label_label_pre_cost_is_ok
562        >current_instruction_cost_is_ok
563    ]
564  ]
565qed.
566       
567let rec compute_max_trace_label_ret_cost_is_ok
568  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
569    (the_trace: trace_label_return cost_labels start_status final_status)
570      on the_trace:
571        compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
572        (clock … final_status) - (clock … start_status) ≝
573  match the_trace with
574  [ tlr_base before after trace_to_lift ⇒ ?
575  | tlr_step initial pre_fun_call pre_fun_call_trace start_fun_call end_fun_call
576      fun_call_trace pre_start_fun_call_coherence ⇒ ?
577  ]
578and compute_max_trace_label_label_pre_cost_is_ok
579  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
580    (start_status: Status) (final_status: Status)
581      (the_trace: trace_label_label_pre cost_labels ends_flag start_status final_status)
582        on the_trace:
583          compute_max_trace_label_label_pre_cost cost_labels ends_flag start_status final_status the_trace =
584            (clock … final_status) - (clock … start_status) ≝
585  match the_trace with
586  [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ ?
587  | tllp_base_return the_status is_return ⇒ ?
588  | tllp_base_jump the_status cost_label is_jump is_cost ⇒ ?
589  | tllp_step_call end_flag pre_fun_call start_fun_call end_fun_call after_fun_call final
590      fun_call_trace is_call statuses_related pre_start_fun_call_coherence
591      end_after_fun_call_coherence after_fun_call_trace ⇒ ?
592  | tllp_step_default end_flag start initial end initial_end_trace not_call
593      not_jump not_return not_cost ⇒ ?
594  ]
595and compute_max_trace_label_label_cost_is_ok
596  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
597    (start_status: Status) (final_status: Status)
598      (the_trace: trace_label_label cost_labels ends_flag start_status final_status)
599        on the_trace:
600          compute_max_trace_label_label_cost cost_labels ends_flag start_status final_status the_trace =
601            (clock … final_status) - (clock … start_status) ≝
602  match the_trace with
603  [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
604  ].
605  [8: @(compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag initial final given_trace)
606  |1: @(compute_max_trace_label_label_cost_is_ok cost_labels ends_with_ret before after trace_to_lift)
607  |4: normalize
608      @minus_n_n
609  |3: normalize
610      @minus_n_n
611  |5: normalize
612      @minus_n_n
613  |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)
614      letin the_trace_cost_ok ≝ (compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag start_status final_status the_trace)
615  |*:
616  ]
617qed.
618 
619lemma compute_max_trace_label_ret_cost_is_ok:
620  ∀cost_labels: BitVectorTrie Byte 16.
621  ∀start_status: Status.
622  ∀final_status: Status.
623  ∀the_trace: trace_label_return cost_labels start_status final_status.
624    compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
625      (clock … final_status) - (clock … start_status).
626  #COST_LABELS #START_STATUS #FINAL_STATUS #THE_TRACE
627  elim THE_TRACE
628
629lemma trace_lab_rec_cost_ok:
630 ∀p: trace_lab_rec.
631  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
632
633let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
634 match p with
635 [ call ⇒ DO NOT ADD ANYTHING
636 | _ ⇒ DO ADD ].
637
638let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
639 | (call b bf tr af tl) as self ⇒
640    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
641    trace_lab_rec_cost' tl
642
643theorem main_lemma:
644 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
645
646axiom lemma1:
647 ∀p: simple_path.
648  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
649
650axiom lemma2:
651 ∀s,l,cost_map.
652  is_labelled l s →
653   traverse_cost_internal s = cost_map l.
654
655axiom main_statement:
656 ∀s.
657 ∀cost_map.
658 let p ≝ compute_simple_path0 s in
659 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
660
661axiom main_statement:
662 ∀s.
663 ∀cost_map.
664 let p ≝ compute_simple_path0 s in
665  execute' (path_length p) s = 〈s',τ〉 →
666   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.