source: src/ASM/CostsProof.ma @ 1558

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

Snapshot before moving things to ASMCosts.ma.

File size: 27.8 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(*
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*)
300
301lemma plus_minus_rearrangement_1:
302  ∀m, n, o: nat.
303  ∀proof_n_m: n ≤ m.
304  ∀proof_m_o: m ≤ o.
305    (m - n) + (o - m) = o - n.
306  #m #n #o #H1 #H2
307  lapply (minus_to_plus … H1 (refl …)) #K1 >K1
308  lapply (minus_to_plus … H2 (refl …)) #K2 >K2
309  /2 by plus_minus/
310qed.
311
312lemma plus_minus_rearrangement_2:
313  ∀m, n, o: nat. n ≤ m → o ≤ n →
314    (m - n) + (n - o) = m - o.
315 /2 by plus_minus_rearrangement_1/
316qed.
317
318(*
319let rec compute_max_trace_label_label_cost_is_ok
320  (cost_labels: BitVectorTrie Byte 16)
321   (trace_ends_flag: trace_ends_with_ret)
322    (start_status: Status) (final_status: Status)
323      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
324        start_status final_status) on the_trace:
325          compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
326            (clock … final_status) - (clock … start_status) ≝ ?
327and compute_max_trace_any_label_cost_is_ok
328  (cost_labels: BitVectorTrie Byte 16)
329  (trace_ends_flag: trace_ends_with_ret)
330   (start_status: Status) (final_status: Status)
331     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
332       on the_trace:
333         compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
334           (clock … final_status) - (clock … start_status) ≝ ?
335and compute_max_trace_label_return_cost_is_ok
336  (cost_labels: BitVectorTrie Byte 16)
337  (start_status: Status) (final_status: Status)
338    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
339      on the_trace:
340        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
341          (clock … final_status) - (clock … start_status) ≝ ?.
342  [1:
343    cases the_trace
344    #ends_flag #start_status #end_status #any_label_trace #is_costed
345    normalize @compute_max_trace_any_label_cost_is_ok
346  |2:
347    cases the_trace
348    [1:
349      #start_status #final_status #is_next #is_not_return #is_costed
350      normalize nodelta;
351      change with (
352        let current_instruction_cost ≝ current_instruction_cost start_status in 
353        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in 
354        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in 
355        call_trace_cost+current_instruction_cost+final_trace_cost
356      ) in ⊢ (??%?);
357    |2:
358      #start_status #final_status #is_next #is_return
359    |3:
360      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
361      #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_trace
362      change with (
363        let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 
364        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call fun_call_trace in 
365        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final after_fun_call_trace in 
366          call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?);
367      normalize nodelta;
368      >compute_max_trace_label_return_cost_is_ok
369      >compute_max_trace_any_label_cost_is_ok
370    |4:
371    ]
372  |3:
373    cases the_trace
374    [1:
375      #status_before #status_after #trace_to_lift
376      normalize @compute_max_trace_label_label_cost_is_ok
377    |2:
378      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
379      normalize >compute_max_trace_label_label_cost_is_ok
380      >compute_max_trace_label_return_cost_is_ok
381      >plus_minus_rearrangement_1
382      [1: %
383      |2:
384      |3:
385      ]
386    ]
387  ].
388*)
389
390(* XXX: work below here: *)
391
392let rec compute_paid_trace_any_label
393  (cost_labels: BitVectorTrie costlabel 16)
394  (trace_ends_flag: trace_ends_with_ret)
395   (start_status: Status) (final_status: Status)
396     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
397       on the_trace: nat ≝
398  match the_trace with
399  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
400  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
401  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
402     _ _ _ call_trace final_trace ⇒
403      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
404      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
405        current_instruction_cost + final_trace_cost
406  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
407      let current_instruction_cost ≝ current_instruction_cost status_pre in
408      let tail_trace_cost ≝
409       compute_paid_trace_any_label cost_labels end_flag
410        status_init status_end tail_trace
411      in
412        current_instruction_cost + tail_trace_cost
413  ].
414
415definition compute_paid_trace_label_label ≝
416 λcost_labels: BitVectorTrie costlabel 16.
417  λtrace_ends_flag: trace_ends_with_ret.
418   λstart_status: Status.
419    λfinal_status: Status.
420     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
421      start_status final_status.
422  match the_trace with
423  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
424      compute_paid_trace_any_label … given_trace
425  ].
426
427let rec compute_trace_label_label_cost_using_paid
428  (cost_labels: BitVectorTrie costlabel 16)
429   (trace_ends_flag: trace_ends_with_ret)
430    (start_status: Status) (final_status: Status)
431      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
432        start_status final_status) on the_trace: nat ≝
433  match the_trace with
434  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
435      compute_paid_trace_label_label cost_labels … the_trace +
436      compute_trace_any_label_cost_using_paid … given_trace
437  ]
438and compute_trace_any_label_cost_using_paid
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_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
443       on the_trace: nat ≝
444  match the_trace with
445  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
446  | tal_base_return the_status _ _ _ ⇒ 0
447  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
448     _ _ _ call_trace final_trace ⇒
449      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
450      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cost_labels end_flag … final_trace in
451        call_trace_cost + final_trace_cost
452  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
453     compute_trace_any_label_cost_using_paid cost_labels end_flag
454      status_init status_end tail_trace
455  ]
456and compute_trace_label_return_cost_using_paid
457  (cost_labels: BitVectorTrie costlabel 16)
458  (start_status: Status) (final_status: Status)
459    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
460      on the_trace: nat ≝
461  match the_trace with
462  [ tlr_base before after trace_to_lift ⇒ compute_trace_label_label_cost_using_paid … trace_to_lift
463  | tlr_step initial labelled final labelled_trace ret_trace ⇒
464      let labelled_cost ≝ compute_trace_label_label_cost_using_paid … labelled_trace in
465      let return_cost ≝ compute_trace_label_return_cost_using_paid … ret_trace in
466        labelled_cost + return_cost
467  ].
468
469let rec compute_trace_label_label_cost_using_paid_ok
470  (cost_labels: BitVectorTrie costlabel 16)
471   (trace_ends_flag: trace_ends_with_ret)
472    (start_status: Status) (final_status: Status)
473      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
474        start_status final_status) on the_trace:
475 compute_trace_label_label_cost_using_paid cost_labels … the_trace =
476 compute_max_trace_label_label_cost … the_trace ≝ ?
477and compute_trace_any_label_cost_using_paid_ok
478  (cost_labels: BitVectorTrie costlabel 16)
479  (trace_ends_flag: trace_ends_with_ret)
480   (start_status: Status) (final_status: Status)
481     (the_trace: trace_any_label (ASM_abstract_status cost_labels)
482      trace_ends_flag start_status final_status) on the_trace:     
483  compute_paid_trace_any_label cost_labels trace_ends_flag … the_trace
484  +compute_trace_any_label_cost_using_paid cost_labels trace_ends_flag … the_trace
485  =compute_max_trace_any_label_cost cost_labels trace_ends_flag … the_trace ≝ ?
486and compute_trace_label_return_cost_using_paid_ok
487  (cost_labels: BitVectorTrie costlabel 16)
488  (start_status: Status) (final_status: Status)
489    (the_trace: trace_label_return (ASM_abstract_status cost_labels)
490     start_status final_status) on the_trace:
491 compute_trace_label_return_cost_using_paid cost_labels … the_trace =
492 compute_max_trace_label_return_cost cost_labels … the_trace ≝ ?.
493[ cases the_trace #endsf #ss #es #tr #H normalize
494  @compute_trace_any_label_cost_using_paid_ok
495| cases the_trace
496  [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O %
497  | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O %
498  | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #tr2 whd in ⊢ (??(?%%)%);
499    <compute_trace_any_label_cost_using_paid_ok
500    <compute_trace_label_return_cost_using_paid_ok
501    -compute_trace_label_label_cost_using_paid_ok
502    -compute_trace_label_return_cost_using_paid_ok
503    -compute_trace_any_label_cost_using_paid_ok
504    >commutative_plus in ⊢ (???(?%?));
505    >commutative_plus in ⊢ (??(??%)?);
506    >associative_plus >associative_plus in ⊢ (???%); @eq_f2 try %
507    <associative_plus <commutative_plus %
508  | #ef #sp #si #se #H1 #tr #H2 #H3 whd in ⊢ (??(?%%)%); >associative_plus @eq_f2
509    [ % | @compute_trace_any_label_cost_using_paid_ok ]
510  ]
511| cases the_trace
512  [ #sb #sa #tr normalize @compute_trace_label_label_cost_using_paid_ok
513  | #si #sl #sf #tr1 #tr2 normalize @eq_f2
514    [ @compute_trace_label_label_cost_using_paid_ok
515    | @compute_trace_label_return_cost_using_paid_ok ]]]
516qed.
517
518(*
519let rec compute_paid_trace_label_return
520  (cost_labels: BitVectorTrie costlabel 16)
521  (start_status: Status) (final_status: Status)
522    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
523      on the_trace: nat ≝
524 match the_trace with
525  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label … trace_to_lift
526  | tlr_step initial labelled final labelled_trace ret_trace ⇒
527      let labelled_cost ≝ compute_paid_trace_label_label … labelled_trace in
528      let return_cost ≝ compute_paid_trace_label_return … ret_trace in
529        labelled_cost + return_cost
530  ].
531*)
532
533let rec compute_cost_trace_label_label
534  (cost_labels: BitVectorTrie costlabel 16)
535   (trace_ends_flag: trace_ends_with_ret)
536    (start_status: Status) (final_status: Status)
537      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
538        start_status final_status) on the_trace: list costlabel ≝
539  match the_trace with
540  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
541     let pc ≝ program_counter … initial in
542     let label ≝
543      match lookup_opt … pc cost_labels return λx. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
544      [ None ⇒ λabs. ⊥
545      | Some l ⇒ λ_. l ] labelled_proof in
546     label::compute_cost_trace_any_label … given_trace
547  ]
548and compute_cost_trace_any_label
549  (cost_labels: BitVectorTrie costlabel 16)
550  (trace_ends_flag: trace_ends_with_ret)
551   (start_status: Status) (final_status: Status)
552     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
553       on the_trace: list costlabel ≝
554  match the_trace with
555  [ tal_base_not_return the_status _ _ _ _ ⇒ []
556  | tal_base_return the_status _ _ _ ⇒ []
557  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
558     _ _ _ call_trace final_trace ⇒
559      let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
560      let final_cost_trace ≝ compute_cost_trace_any_label cost_labels end_flag … final_trace in
561        call_cost_trace @ final_cost_trace
562  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
563       compute_cost_trace_any_label cost_labels end_flag
564        status_init status_end tail_trace
565  ]
566and compute_cost_trace_label_return
567  (cost_labels: BitVectorTrie costlabel 16)
568  (start_status: Status) (final_status: Status)
569    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
570      on the_trace: list costlabel ≝
571  match the_trace with
572  [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
573  | tlr_step initial labelled final labelled_trace ret_trace ⇒
574      let labelled_cost ≝ compute_cost_trace_label_label … labelled_trace in
575      let return_cost ≝ compute_cost_trace_label_return … ret_trace in
576        labelled_cost @ return_cost
577  ].
578//
579qed.
580
581(* ??????????????????????? *)
582axiom block_cost_static_dynamic_ok:
583 ∀cost_labels: BitVectorTrie costlabel 16.
584 ∀trace_ends_flag.
585 ∀start_status: Status.
586 ∀final_status: Status.
587 ∀the_trace:
588  trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
589   start_status final_status.
590 let mem ≝ code_memory … start_status in
591 let pc ≝ program_counter … start_status in
592 let program_size ≝ 2^16 in
593  block_cost mem cost_labels pc program_size =
594  compute_paid_trace_label_label cost_labels trace_ends_flag
595   start_status final_status the_trace.
596
597include "arithmetics/bigops.ma".
598
599lemma foo:
600 ∀cost_labels: BitVectorTrie costlabel 16.
601 ∀cost_labels_inv: identifier_map CostTag Word.
602 ∀initial,final.
603 ∀trace: trace_label_return (ASM_abstract_status cost_labels) initial final.
604  let dummy ≝ an_identifier ? one in
605  let ctrace ≝ compute_cost_trace_label_return … trace in
606  compute_max_trace_label_return_cost … trace =
607   \big [ plus, 0 ]_{ i < |ctrace| }
608    (block_cost (code_memory … initial) cost_labels
609     (lookup_present … cost_labels_inv (nth i ? ctrace dummy) ?) 2^16).
610 [2: cases daemon (* ALL LABELS MUST BE PRESENT *)
611 | #cost_labels #cost_labels_inv #initial #final #trace
612   letin dummy ≝ (an_identifier CostTag one) normalize nodelta
613   whd in match
614
615lemma
616 compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
617  final_status the_trace =
618 
619
620let rec compute_paid_trace_label_label_cost
621  (cost_labels: BitVectorTrie Byte 16)
622   (trace_ends_flag: trace_ends_with_ret)
623    (start_status: Status) (final_status: Status)
624      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
625        start_status final_status) on the_trace: nat ≝
626  match the_trace with
627  [ tll_base _ _ _ given_trace _ ⇒
628      compute_paid_trace_any_label_cost … given_trace
629  ]
630and compute_paid_trace_any_label_cost
631  (cost_labels: BitVectorTrie Byte 16)
632  (trace_ends_flag: trace_ends_with_ret)
633   (start_status: Status) (final_status: Status)
634     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
635       on the_trace: nat ≝
636  match the_trace with
637  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
638  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
639  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
640     _ _ _ call_trace final_trace ⇒
641      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
642      let final_trace_cost ≝ compute_paid_trace_any_label_cost cost_labels end_flag … final_trace in
643        current_instruction_cost + final_trace_cost
644  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
645      let current_instruction_cost ≝ current_instruction_cost status_pre in
646      let tail_trace_cost ≝
647       compute_paid_trace_any_label_cost cost_labels end_flag
648        status_init status_end tail_trace
649      in
650        current_instruction_cost + tail_trace_cost
651  ]
652and compute_paid_trace_label_return_cost
653  (cost_labels: BitVectorTrie Byte 16)
654  (start_status: Status) (final_status: Status)
655    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
656      on the_trace: nat ≝
657  match the_trace with
658  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label_cost … trace_to_lift
659  | tlr_step initial labelled final labelled_trace ret_trace ⇒
660      let labelled_cost ≝ compute_paid_trace_label_label_cost … labelled_trace in
661      let return_cost ≝ compute_paid_trace_label_return_cost … ret_trace in
662        labelled_cost + return_cost
663  ].
664
665let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
666 | (call b bf tr af tl) as self ⇒
667    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
668    trace_lab_rec_cost' tl
669
670theorem main_lemma:
671 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
672
673axiom lemma1:
674 ∀p: simple_path.
675  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
676
677axiom lemma2:
678 ∀s,l,cost_map.
679  is_labelled l s →
680   traverse_cost_internal s = cost_map l.
681
682axiom main_statement:
683 ∀s.
684 ∀cost_map.
685 let p ≝ compute_simple_path0 s in
686 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
687
688axiom main_statement:
689 ∀s.
690 ∀cost_map.
691 let p ≝ compute_simple_path0 s in
692  execute' (path_length p) s = 〈s',τ〉 →
693   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.