source: src/ASM/CostsProof.ma @ 1554

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

Major progress in the proof.

File size: 25.5 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 costlabel 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 label_of_current_instruction:
47 BitVectorTrie costlabel 16 → Status → list costlabel
48 ≝
49  λcost_labels,s.
50  let pc ≝ program_counter … s in
51    match lookup_opt … pc cost_labels with
52    [ None ⇒ []
53    | Some l ⇒ [l]
54    ].
55
56definition next_instruction_properly_relates_program_counters ≝
57  λbefore: Status.
58  λafter : Status.
59  let size ≝ current_instruction_cost before in
60  let pc_before ≝ program_counter … before in
61  let pc_after ≝ program_counter … after in
62  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
63    sum = pc_after.
64
65definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
66 λcost_labels.
67  mk_abstract_status
68   Status
69   (λs,s'. eject … (execute_1 s) = s')
70   (λs,class. ASM_classify s = class)
71   (current_instruction_is_labelled cost_labels)
72   next_instruction_properly_relates_program_counters.
73
74(*
75definition next_instruction_is_labelled ≝
76  λcost_labels: BitVectorTrie Byte 16.
77  λs: Status.
78  let pc ≝ program_counter … (execute_1 s) in
79    match lookup_opt … pc cost_labels with
80    [ None ⇒ False
81    | _    ⇒ True
82    ].
83
84definition current_instruction_cost ≝
85  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
86
87definition is_call_p ≝
88  λs.
89  match s with
90  [ ACALL _ ⇒ True
91  | LCALL _ ⇒ True
92  | JMP ⇒ True (* XXX: is function pointer call *)
93  | _ ⇒ False
94  ].
95
96definition next_instruction ≝
97  λs: Status.
98  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
99    instruction.
100
101inductive trace_ends_with_ret: Type[0] ≝
102  | ends_with_ret: trace_ends_with_ret
103  | doesnt_end_with_ret: trace_ends_with_ret.
104
105definition next_instruction_is_labelled ≝
106  λcost_labels: BitVectorTrie Byte 16.
107  λs: Status.
108  let pc ≝ program_counter … (execute 1 s) in
109    match lookup_opt … pc cost_labels with
110    [ None ⇒ False
111    | _    ⇒ True
112    ].
113
114definition next_instruction_properly_relates_program_counters ≝
115  λbefore: Status.
116  λafter : Status.
117  let size ≝ current_instruction_cost before in
118  let pc_before ≝ program_counter … before in
119  let pc_after ≝ program_counter … after in
120  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
121    sum = pc_after.
122
123definition current_instruction ≝
124  λs: Status.
125  let pc ≝ program_counter … s in
126  \fst (\fst (fetch … (code_memory … s) pc)).
127
128definition current_instruction_is_labelled ≝
129  λcost_labels: BitVectorTrie Byte 16.
130  λs: Status.
131  let pc ≝ program_counter … s in
132    match lookup_opt … pc cost_labels with
133    [ None ⇒ False
134    | _    ⇒ True
135    ].
136
137inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
138  | tlr_base:
139      ∀status_before: Status.
140      ∀status_after: Status.
141        trace_label_label cost_labels ends_with_ret status_before status_after →
142        trace_label_return cost_labels status_before status_after
143  | tlr_step:
144      ∀status_initial: Status.
145      ∀status_labelled: Status.
146      ∀status_final: Status.
147          trace_label_label cost_labels doesnt_end_with_ret status_initial status_labelled →
148            trace_label_return cost_labels status_labelled status_final →
149              trace_label_return cost_labels status_initial status_final
150with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
151  | tll_base:
152      ∀ends_flag: trace_ends_with_ret.
153      ∀start_status: Status.
154      ∀end_status: Status.
155        trace_label_label_pre cost_labels ends_flag start_status end_status →
156        current_instruction_is_labelled cost_labels start_status →
157        trace_label_label cost_labels ends_flag start_status end_status
158with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
159  | tllp_base_not_return:
160      ∀start_status: Status.
161        let final_status ≝ execute 1 start_status in
162        current_instruction start_status ≠ (RealInstruction … (RET [[relative]])) →
163        ¬ (is_jump_p (current_instruction start_status)) →
164        current_instruction_is_labelled cost_labels final_status →
165          trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
166  | tllp_base_return:
167      ∀start_status: Status.
168        let final_status ≝ execute 1 start_status in
169          current_instruction start_status = (RealInstruction … (RET [[relative]])) →
170            trace_label_label_pre cost_labels ends_with_ret start_status final_status
171  | tllp_base_jump:
172      ∀start_status: Status.
173        let final_status ≝ execute 1 start_status in
174          is_jump_p (current_instruction start_status) →
175            current_instruction_is_labelled cost_labels final_status →
176              trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
177  | tllp_step_call:
178      ∀end_flag: trace_ends_with_ret.
179      ∀status_pre_fun_call: Status.
180      ∀status_after_fun_call: Status.
181      ∀status_final: Status.
182        let status_start_fun_call ≝ execute 1 status_pre_fun_call in
183          is_call_p (current_instruction status_pre_fun_call) →
184          next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
185          trace_label_return cost_labels status_start_fun_call status_after_fun_call →
186          trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
187            trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
188  | tllp_step_default:
189      ∀end_flag: trace_ends_with_ret.
190      ∀status_pre: Status.
191      ∀status_end: Status.
192        let status_init ≝ execute 1 status_pre in
193          trace_label_label_pre cost_labels end_flag status_init status_end →
194          ¬ (is_call_p (current_instruction status_pre)) →
195          ¬ (is_jump_p (current_instruction status_pre)) →
196          (current_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
197          ¬ (current_instruction_is_labelled cost_labels status_init) →
198            trace_label_label_pre cost_labels end_flag status_pre status_end.
199*)
200
201(* XXX: not us
202definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
203
204lemma simple_path_ok:
205 ∀st: Status.∀H.
206 let p ≝ compute_simple_path0 st H in
207   ∀n.
208    nth_path n p = execute n st ∧
209     (execute' (path_length p) st = 〈st',τ〉 →
210      τ = cost_trace p)
211  ].
212*)
213
214let rec compute_max_trace_label_label_cost
215  (cost_labels: BitVectorTrie costlabel 16)
216   (trace_ends_flag: trace_ends_with_ret)
217    (start_status: Status) (final_status: Status)
218      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
219        start_status final_status) on the_trace: nat ≝
220  match the_trace with
221  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
222      compute_max_trace_any_label_cost … given_trace
223  ]
224and compute_max_trace_any_label_cost
225  (cost_labels: BitVectorTrie costlabel 16)
226  (trace_ends_flag: trace_ends_with_ret)
227   (start_status: Status) (final_status: Status)
228     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
229       on the_trace: nat ≝
230  match the_trace with
231  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
232  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
233  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
234     _ _ _ call_trace final_trace ⇒
235      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
236      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
237      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
238        call_trace_cost + current_instruction_cost + final_trace_cost
239  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
240      let current_instruction_cost ≝ current_instruction_cost status_pre in
241      let tail_trace_cost ≝
242       compute_max_trace_any_label_cost cost_labels end_flag
243        status_init status_end tail_trace
244      in
245        current_instruction_cost + tail_trace_cost
246  ]
247and compute_max_trace_label_return_cost
248  (cost_labels: BitVectorTrie costlabel 16)
249  (start_status: Status) (final_status: Status)
250    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
251      on the_trace: nat ≝
252  match the_trace with
253  [ tlr_base before after trace_to_lift ⇒ compute_max_trace_label_label_cost … trace_to_lift
254  | tlr_step initial labelled final labelled_trace ret_trace ⇒
255      let labelled_cost ≝ compute_max_trace_label_label_cost … labelled_trace in
256      let return_cost ≝ compute_max_trace_label_return_cost … ret_trace in
257        labelled_cost + return_cost
258  ].
259
260(*Useless now?
261(* To be moved *)
262lemma pred_minus_1:
263  ∀m, n: nat.
264  ∀proof: n < m.
265    pred (m - n) = m - n - 1.
266  #m #n
267  cases m
268  [ #proof
269    cases(lt_to_not_zero … proof)
270  | #m' #proof
271    normalize in ⊢ (???%);
272    cases n
273    [ normalize //
274    | #n' normalize
275      cases(m' - n')
276      [ %
277      | #Sm_n'
278        normalize //
279      ]
280    ]
281  ]
282qed.
283
284lemma succ_m_plus_one:
285  ∀m: nat.
286    S m = m + 1.
287 //
288qed.*)
289
290include alias "arithmetics/nat.ma".
291
292(*Useless now?
293lemma minus_m_n_minus_minus_plus_1:
294  ∀m, n: nat.
295  ∀proof: n < m.
296    m - n = (m - n - 1) + 1.
297 /3 by lt_plus_to_minus_r, plus_minus/
298qed.
299
300lemma plus_minus_rearrangement_1:
301  ∀m, n, o: nat.
302  ∀proof_n_m: n ≤ m.
303  ∀proof_m_o: m ≤ o.
304    (m - n) + (o - m) = o - n.
305  #m #n #o #H1 #H2
306  lapply (minus_to_plus … H1 (refl …)) #K1 >K1
307  lapply (minus_to_plus … H2 (refl …)) #K2 >K2
308  /2 by plus_minus/
309qed.
310
311lemma plus_minus_rearrangement_2:
312  ∀m, n, o: nat. n ≤ m → o ≤ n →
313    (m - n) + (n - o) = m - o.
314 /2 by plus_minus_rearrangement_1/
315qed.*)
316
317(*
318let rec compute_max_trace_label_label_cost_is_ok
319  (cost_labels: BitVectorTrie Byte 16)
320   (trace_ends_flag: trace_ends_with_ret)
321    (start_status: Status) (final_status: Status)
322      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
323        start_status final_status) on the_trace:
324          compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
325            (clock … final_status) - (clock … start_status) ≝ ?
326and compute_max_trace_any_label_cost_is_ok
327  (cost_labels: BitVectorTrie Byte 16)
328  (trace_ends_flag: trace_ends_with_ret)
329   (start_status: Status) (final_status: Status)
330     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
331       on the_trace:
332         compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
333           (clock … final_status) - (clock … start_status) ≝ ?
334and compute_max_trace_label_return_cost_is_ok
335  (cost_labels: BitVectorTrie Byte 16)
336  (start_status: Status) (final_status: Status)
337    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
338      on the_trace:
339        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
340          (clock … final_status) - (clock … start_status) ≝ ?.
341  [1:
342    cases the_trace
343    #ends_flag #start_status #end_status #any_label_trace #is_costed
344    normalize @compute_max_trace_any_label_cost_is_ok
345  |2:
346  |3:
347    cases the_trace
348    [1:
349      #status_before #status_after #trace_to_lift
350      normalize @compute_max_trace_label_label_cost_is_ok
351    |2:
352      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
353      normalize >compute_max_trace_label_label_cost_is_ok
354      >compute_max_trace_label_return_cost_is_ok
355    ]
356  ].
357*)
358
359(* XXX: work below here: *)
360
361let rec compute_paid_trace_any_label
362  (cost_labels: BitVectorTrie costlabel 16)
363  (trace_ends_flag: trace_ends_with_ret)
364   (start_status: Status) (final_status: Status)
365     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
366       on the_trace: nat ≝
367  match the_trace with
368  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
369  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
370  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
371     _ _ _ call_trace final_trace ⇒
372      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
373      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
374        current_instruction_cost + final_trace_cost
375  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
376      let current_instruction_cost ≝ current_instruction_cost status_pre in
377      let tail_trace_cost ≝
378       compute_paid_trace_any_label cost_labels end_flag
379        status_init status_end tail_trace
380      in
381        current_instruction_cost + tail_trace_cost
382  ].
383
384definition compute_paid_trace_label_label ≝
385 λcost_labels: BitVectorTrie costlabel 16.
386  λtrace_ends_flag: trace_ends_with_ret.
387   λstart_status: Status.
388    λfinal_status: Status.
389     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
390      start_status final_status.
391  match the_trace with
392  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
393      compute_paid_trace_any_label … given_trace
394  ].
395
396let rec compute_trace_label_label_cost_using_paid
397  (cost_labels: BitVectorTrie costlabel 16)
398   (trace_ends_flag: trace_ends_with_ret)
399    (start_status: Status) (final_status: Status)
400      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
401        start_status final_status) on the_trace: nat ≝
402  match the_trace with
403  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
404      compute_paid_trace_label_label cost_labels … the_trace +
405      compute_trace_any_label_cost_using_paid … given_trace
406  ]
407and compute_trace_any_label_cost_using_paid
408  (cost_labels: BitVectorTrie costlabel 16)
409  (trace_ends_flag: trace_ends_with_ret)
410   (start_status: Status) (final_status: Status)
411     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
412       on the_trace: nat ≝
413  match the_trace with
414  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
415  | tal_base_return the_status _ _ _ ⇒ 0
416  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
417     _ _ _ call_trace final_trace ⇒
418      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
419      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cost_labels end_flag … final_trace in
420        call_trace_cost + final_trace_cost
421  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
422     compute_trace_any_label_cost_using_paid cost_labels end_flag
423      status_init status_end tail_trace
424  ]
425and compute_trace_label_return_cost_using_paid
426  (cost_labels: BitVectorTrie costlabel 16)
427  (start_status: Status) (final_status: Status)
428    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
429      on the_trace: nat ≝
430  match the_trace with
431  [ tlr_base before after trace_to_lift ⇒ compute_trace_label_label_cost_using_paid … trace_to_lift
432  | tlr_step initial labelled final labelled_trace ret_trace ⇒
433      let labelled_cost ≝ compute_trace_label_label_cost_using_paid … labelled_trace in
434      let return_cost ≝ compute_trace_label_return_cost_using_paid … ret_trace in
435        labelled_cost + return_cost
436  ].
437
438let rec compute_trace_label_label_cost_using_paid_ok
439  (cost_labels: BitVectorTrie costlabel 16)
440   (trace_ends_flag: trace_ends_with_ret)
441    (start_status: Status) (final_status: Status)
442      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
443        start_status final_status) on the_trace:
444 compute_trace_label_label_cost_using_paid cost_labels … the_trace =
445 compute_max_trace_label_label_cost … the_trace ≝ ?
446and compute_trace_any_label_cost_using_paid_ok
447  (cost_labels: BitVectorTrie costlabel 16)
448  (trace_ends_flag: trace_ends_with_ret)
449   (start_status: Status) (final_status: Status)
450     (the_trace: trace_any_label (ASM_abstract_status cost_labels)
451      trace_ends_flag start_status final_status) on the_trace:     
452  compute_paid_trace_any_label cost_labels trace_ends_flag … the_trace
453  +compute_trace_any_label_cost_using_paid cost_labels trace_ends_flag … the_trace
454  =compute_max_trace_any_label_cost cost_labels trace_ends_flag … the_trace ≝ ?
455and compute_trace_label_return_cost_using_paid_ok
456  (cost_labels: BitVectorTrie costlabel 16)
457  (start_status: Status) (final_status: Status)
458    (the_trace: trace_label_return (ASM_abstract_status cost_labels)
459     start_status final_status) on the_trace:
460 compute_trace_label_return_cost_using_paid cost_labels … the_trace =
461 compute_max_trace_label_return_cost cost_labels … the_trace ≝ ?.
462[ cases the_trace #endsf #ss #es #tr #H normalize
463  @compute_trace_any_label_cost_using_paid_ok
464| cases the_trace
465  [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O %
466  | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O %
467  | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #tr2 whd in ⊢ (??(?%%)%);
468    <compute_trace_any_label_cost_using_paid_ok
469    <compute_trace_label_return_cost_using_paid_ok
470    -compute_trace_label_label_cost_using_paid_ok
471    -compute_trace_label_return_cost_using_paid_ok
472    -compute_trace_any_label_cost_using_paid_ok
473    >commutative_plus in ⊢ (???(?%?));
474    >commutative_plus in ⊢ (??(??%)?);
475    >associative_plus >associative_plus in ⊢ (???%); @eq_f2 try %
476    <associative_plus <commutative_plus %
477  | #ef #sp #si #se #H1 #tr #H2 #H3 whd in ⊢ (??(?%%)%); >associative_plus @eq_f2
478    [ % | @compute_trace_any_label_cost_using_paid_ok ]
479  ]
480| cases the_trace
481  [ #sb #sa #tr normalize @compute_trace_label_label_cost_using_paid_ok
482  | #si #sl #sf #tr1 #tr2 normalize @eq_f2
483    [ @compute_trace_label_label_cost_using_paid_ok
484    | @compute_trace_label_return_cost_using_paid_ok ]]]
485qed.
486
487(*
488let rec compute_paid_trace_label_return
489  (cost_labels: BitVectorTrie costlabel 16)
490  (start_status: Status) (final_status: Status)
491    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
492      on the_trace: nat ≝
493 match the_trace with
494  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label … trace_to_lift
495  | tlr_step initial labelled final labelled_trace ret_trace ⇒
496      let labelled_cost ≝ compute_paid_trace_label_label … labelled_trace in
497      let return_cost ≝ compute_paid_trace_label_return … ret_trace in
498        labelled_cost + return_cost
499  ].
500*)
501
502let rec compute_cost_trace_label_label
503  (cost_labels: BitVectorTrie costlabel 16)
504   (trace_ends_flag: trace_ends_with_ret)
505    (start_status: Status) (final_status: Status)
506      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
507        start_status final_status) on the_trace: list costlabel ≝
508  match the_trace with
509  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
510     let pc ≝ program_counter … initial in
511     let label ≝
512      match lookup_opt … pc cost_labels return λx. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
513      [ None ⇒ λabs. ⊥
514      | Some l ⇒ λ_. l ] labelled_proof in
515     label::compute_cost_trace_any_label … given_trace
516  ]
517and compute_cost_trace_any_label
518  (cost_labels: BitVectorTrie costlabel 16)
519  (trace_ends_flag: trace_ends_with_ret)
520   (start_status: Status) (final_status: Status)
521     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
522       on the_trace: list costlabel ≝
523  match the_trace with
524  [ tal_base_not_return the_status _ _ _ _ ⇒ []
525  | tal_base_return the_status _ _ _ ⇒ []
526  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
527     _ _ _ call_trace final_trace ⇒
528      let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
529      let final_cost_trace ≝ compute_cost_trace_any_label cost_labels end_flag … final_trace in
530        call_cost_trace @ final_cost_trace
531  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
532       compute_cost_trace_any_label cost_labels end_flag
533        status_init status_end tail_trace
534  ]
535and compute_cost_trace_label_return
536  (cost_labels: BitVectorTrie costlabel 16)
537  (start_status: Status) (final_status: Status)
538    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
539      on the_trace: list costlabel ≝
540  match the_trace with
541  [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
542  | tlr_step initial labelled final labelled_trace ret_trace ⇒
543      let labelled_cost ≝ compute_cost_trace_label_label … labelled_trace in
544      let return_cost ≝ compute_cost_trace_label_return … ret_trace in
545        labelled_cost @ return_cost
546  ].
547//
548qed.
549
550include "arithmetics/bigops.ma".
551
552lemma foo:
553 ∀cost_label: BitVectorTrie costlabel 16.
554 ∀initial,final.
555 ∀trace: trace_label_return (ASM_abstract_status cost_label) initial final.
556  let ctrace ≝ compute_cost_trace_label_return … trace in
557  compute_max_trace_label_return_cost … trace =
558   \big [ plus, 0 ]_{ i < |ctrace| } (? (nth i ? ctrace ?)).
559 
560  compute_cost_trace_label_return trace =
561 
562 
563
564
565lemma
566 compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
567  final_status the_trace =
568 
569
570let rec compute_paid_trace_label_label_cost
571  (cost_labels: BitVectorTrie Byte 16)
572   (trace_ends_flag: trace_ends_with_ret)
573    (start_status: Status) (final_status: Status)
574      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
575        start_status final_status) on the_trace: nat ≝
576  match the_trace with
577  [ tll_base _ _ _ given_trace _ ⇒
578      compute_paid_trace_any_label_cost … given_trace
579  ]
580and compute_paid_trace_any_label_cost
581  (cost_labels: BitVectorTrie Byte 16)
582  (trace_ends_flag: trace_ends_with_ret)
583   (start_status: Status) (final_status: Status)
584     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
585       on the_trace: nat ≝
586  match the_trace with
587  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
588  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
589  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
590     _ _ _ call_trace final_trace ⇒
591      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
592      let final_trace_cost ≝ compute_paid_trace_any_label_cost cost_labels end_flag … final_trace in
593        current_instruction_cost + final_trace_cost
594  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
595      let current_instruction_cost ≝ current_instruction_cost status_pre in
596      let tail_trace_cost ≝
597       compute_paid_trace_any_label_cost cost_labels end_flag
598        status_init status_end tail_trace
599      in
600        current_instruction_cost + tail_trace_cost
601  ]
602and compute_paid_trace_label_return_cost
603  (cost_labels: BitVectorTrie Byte 16)
604  (start_status: Status) (final_status: Status)
605    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
606      on the_trace: nat ≝
607  match the_trace with
608  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label_cost … trace_to_lift
609  | tlr_step initial labelled final labelled_trace ret_trace ⇒
610      let labelled_cost ≝ compute_paid_trace_label_label_cost … labelled_trace in
611      let return_cost ≝ compute_paid_trace_label_return_cost … ret_trace in
612        labelled_cost + return_cost
613  ].
614
615let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
616 | (call b bf tr af tl) as self ⇒
617    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
618    trace_lab_rec_cost' tl
619
620theorem main_lemma:
621 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
622
623axiom lemma1:
624 ∀p: simple_path.
625  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
626
627axiom lemma2:
628 ∀s,l,cost_map.
629  is_labelled l s →
630   traverse_cost_internal s = cost_map l.
631
632axiom main_statement:
633 ∀s.
634 ∀cost_map.
635 let p ≝ compute_simple_path0 s in
636 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
637
638axiom main_statement:
639 ∀s.
640 ∀cost_map.
641 let p ≝ compute_simple_path0 s in
642  execute' (path_length p) s = 〈s',τ〉 →
643   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.