source: src/ASM/CostsProof.ma @ 1658

Last change on this file since 1658 was 1658, checked in by mulligan, 7 years ago

asm costs changes from today

File size: 41.7 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4include "common/StructuredTraces.ma".
5include "arithmetics/bigops.ma".
6include alias "arithmetics/nat.ma".
7include alias "basics/logic.ma".
8
9definition current_instruction0 ≝
10  λcode_memory: BitVectorTrie Byte 16.
11  λprogram_counter: Word.
12    \fst (\fst (fetch … code_memory program_counter)).
13
14definition current_instruction ≝
15  λs: Status.
16    current_instruction0 (code_memory … s) (program_counter … s).
17
18definition ASM_classify0: instruction → status_class ≝
19  λi: instruction.
20  match i with
21   [ RealInstruction pre ⇒
22     match pre with
23      [ RET ⇒ cl_return
24      | JZ _ ⇒ cl_jump
25      | JNZ _ ⇒ cl_jump
26      | JC _ ⇒ cl_jump
27      | JNC _ ⇒ cl_jump
28      | JB _ _ ⇒ cl_jump
29      | JNB _ _ ⇒ cl_jump
30      | JBC _ _ ⇒ cl_jump
31      | CJNE _ _ ⇒ cl_jump
32      | DJNZ _ _ ⇒ cl_jump
33      | _ ⇒ cl_other
34      ]
35   | ACALL _ ⇒ cl_call
36   | LCALL _ ⇒ cl_call
37   | JMP _ ⇒ cl_call
38   | AJMP _ ⇒ cl_jump
39   | LJMP _ ⇒ cl_jump
40   | SJMP _ ⇒ cl_jump
41   | _ ⇒ cl_other
42   ].
43
44definition ASM_classify: Status → status_class ≝
45  λs: Status.
46    ASM_classify0 (current_instruction s).
47
48definition current_instruction_is_labelled ≝
49  λcost_labels: BitVectorTrie costlabel 16.
50  λs: Status.
51  let pc ≝ program_counter … s in
52    match lookup_opt … pc cost_labels with
53    [ None ⇒ False
54    | _    ⇒ True
55    ].
56
57definition next_instruction_properly_relates_program_counters ≝
58  λbefore: Status.
59  λafter : Status.
60  let size ≝ current_instruction_cost before in
61  let pc_before ≝ program_counter … before in
62  let pc_after ≝ program_counter … after in
63  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
64    sum = pc_after.
65
66definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
67 λcost_labels.
68  mk_abstract_status
69   Status
70   (λs,s'. (execute_1 s) = s')
71   (λs,class. ASM_classify s = class)
72   (current_instruction_is_labelled cost_labels)
73   next_instruction_properly_relates_program_counters.
74
75let rec compute_max_trace_label_label_cost
76  (cost_labels: BitVectorTrie costlabel 16)
77   (trace_ends_flag: trace_ends_with_ret)
78    (start_status: Status) (final_status: Status)
79      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
80        start_status final_status) on the_trace: nat ≝
81  match the_trace with
82  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
83      compute_max_trace_any_label_cost … given_trace
84  ]
85and compute_max_trace_any_label_cost
86  (cost_labels: BitVectorTrie costlabel 16)
87  (trace_ends_flag: trace_ends_with_ret)
88   (start_status: Status) (final_status: Status)
89     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
90       on the_trace: nat ≝
91  match the_trace with
92  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
93  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
94  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
95     _ _ _ call_trace final_trace ⇒
96      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
97      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
98      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
99        call_trace_cost + current_instruction_cost + final_trace_cost
100  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
101      let current_instruction_cost ≝ current_instruction_cost status_pre in
102      let tail_trace_cost ≝
103       compute_max_trace_any_label_cost cost_labels end_flag
104        status_init status_end tail_trace
105      in
106        current_instruction_cost + tail_trace_cost
107  ]
108and compute_max_trace_label_return_cost
109  (cost_labels: BitVectorTrie costlabel 16)
110  (start_status: Status) (final_status: Status)
111    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
112      on the_trace: nat ≝
113  match the_trace with
114  [ tlr_base before after trace_to_lift ⇒ compute_max_trace_label_label_cost … trace_to_lift
115  | tlr_step initial labelled final labelled_trace ret_trace ⇒
116      let labelled_cost ≝ compute_max_trace_label_label_cost … labelled_trace in
117      let return_cost ≝ compute_max_trace_label_return_cost … ret_trace in
118        labelled_cost + return_cost
119  ].
120
121include alias "arithmetics/nat.ma".
122
123let rec compute_max_trace_label_label_cost_is_ok
124  (cost_labels: BitVectorTrie costlabel 16)
125   (trace_ends_flag: trace_ends_with_ret)
126    (start_status: Status) (final_status: Status)
127      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
128        start_status final_status) on the_trace:
129          clock … final_status = (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
130and compute_max_trace_any_label_cost_is_ok
131  (cost_labels: BitVectorTrie costlabel 16)
132  (trace_ends_flag: trace_ends_with_ret)
133   (start_status: Status) (final_status: Status)
134     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
135       on the_trace:
136         clock … final_status = (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
137and compute_max_trace_label_return_cost_is_ok
138  (cost_labels: BitVectorTrie costlabel 16)
139  (start_status: Status) (final_status: Status)
140    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
141      on the_trace:
142        clock … final_status = (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace) + clock … start_status ≝ ?.
143  [1:
144    cases the_trace
145    #ends_flag #start_status #end_status #any_label_trace #is_costed
146    normalize @compute_max_trace_any_label_cost_is_ok
147  |2:
148    cases the_trace
149    [1,2:
150      #start_status #final_status #is_next #is_not_return try (#is_costed)
151      change with (current_instruction_cost start_status) in ⊢ (???(?%?));
152      cases(is_next) @execute_1_ok
153    |3:
154      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
155      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
156      change with (
157      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
158      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
159      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
160        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?));
161      normalize nodelta;
162      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
163          status_final final_trace)
164      >(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
165        status_after_fun_call call_trace)
166      cases(is_next) in match (clock … status_start_fun_call);
167      >(execute_1_ok status_pre_fun_call)
168      <associative_plus in ⊢ (??%?);
169      <commutative_plus in match (
170        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
171          + compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace);
172      >associative_plus in ⊢ (??%?);
173      <commutative_plus in match (
174        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
175          + (current_instruction_cost status_pre_fun_call
176              + clock (BitVectorTrie Byte 16) status_pre_fun_call));
177      >associative_plus in ⊢ (??%?);
178      <commutative_plus in match (
179         clock (BitVectorTrie Byte 16) status_pre_fun_call
180           + compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace);
181      <(associative_plus (
182         (compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace)))
183      <associative_plus in ⊢ (??%?); %
184    |4:
185      #end_flag #status_pre #status_init #status_end #is_next
186      #trace_any_label #is_other #is_not_costed
187      change with (
188      let current_instruction_cost ≝ current_instruction_cost status_pre in
189      let tail_trace_cost ≝
190       compute_max_trace_any_label_cost cost_labels end_flag
191        status_init status_end trace_any_label
192      in
193        current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?));
194      normalize nodelta;
195      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
196         status_init status_end trace_any_label)
197      cases(is_next) in match (clock … status_init);
198      >(execute_1_ok status_pre)
199      >commutative_plus >associative_plus >associative_plus @eq_f
200      @commutative_plus
201    ]
202  |3:
203    cases the_trace
204    [1:
205      #status_before #status_after #trace_to_lift
206      normalize @compute_max_trace_label_label_cost_is_ok
207    |2:
208      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
209      normalize
210      >(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
211      >(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
212      <associative_plus in ⊢ (??%?);
213      >commutative_plus in match (
214        compute_max_trace_label_return_cost cost_labels status_labelled status_final ret_trace
215          + compute_max_trace_label_label_cost cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
216      %
217    ]
218  ].
219qed.
220
221(* XXX: work below here: *)
222
223let rec compute_paid_trace_any_label
224  (cost_labels: BitVectorTrie costlabel 16)
225  (trace_ends_flag: trace_ends_with_ret)
226   (start_status: Status) (final_status: Status)
227     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
228       on the_trace: nat ≝
229  match the_trace with
230  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
231  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
232  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
233     _ _ _ call_trace final_trace ⇒
234      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
235      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
236        current_instruction_cost + final_trace_cost
237  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
238      let current_instruction_cost ≝ current_instruction_cost status_pre in
239      let tail_trace_cost ≝
240       compute_paid_trace_any_label cost_labels end_flag
241        status_init status_end tail_trace
242      in
243        current_instruction_cost + tail_trace_cost
244  ].
245
246definition compute_paid_trace_label_label ≝
247 λcost_labels: BitVectorTrie costlabel 16.
248  λtrace_ends_flag: trace_ends_with_ret.
249   λstart_status: Status.
250    λfinal_status: Status.
251     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
252      start_status final_status.
253  match the_trace with
254  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
255      compute_paid_trace_any_label … given_trace
256  ].
257
258let rec compute_trace_label_label_cost_using_paid
259  (cost_labels: BitVectorTrie costlabel 16)
260   (trace_ends_flag: trace_ends_with_ret)
261    (start_status: Status) (final_status: Status)
262      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
263        start_status final_status) on the_trace: nat ≝
264  match the_trace with
265  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
266      compute_paid_trace_label_label cost_labels … the_trace +
267      compute_trace_any_label_cost_using_paid … given_trace
268  ]
269and compute_trace_any_label_cost_using_paid
270  (cost_labels: BitVectorTrie costlabel 16)
271  (trace_ends_flag: trace_ends_with_ret)
272   (start_status: Status) (final_status: Status)
273     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
274       on the_trace: nat ≝
275  match the_trace with
276  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
277  | tal_base_return the_status _ _ _ ⇒ 0
278  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
279     _ _ _ call_trace final_trace ⇒
280      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
281      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cost_labels end_flag … final_trace in
282        call_trace_cost + final_trace_cost
283  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
284     compute_trace_any_label_cost_using_paid cost_labels end_flag
285      status_init status_end tail_trace
286  ]
287and compute_trace_label_return_cost_using_paid
288  (cost_labels: BitVectorTrie costlabel 16)
289  (start_status: Status) (final_status: Status)
290    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
291      on the_trace: nat ≝
292  match the_trace with
293  [ tlr_base before after trace_to_lift ⇒ compute_trace_label_label_cost_using_paid … trace_to_lift
294  | tlr_step initial labelled final labelled_trace ret_trace ⇒
295      let labelled_cost ≝ compute_trace_label_label_cost_using_paid … labelled_trace in
296      let return_cost ≝ compute_trace_label_return_cost_using_paid … ret_trace in
297        labelled_cost + return_cost
298  ].
299
300let rec compute_trace_label_label_cost_using_paid_ok
301  (cost_labels: BitVectorTrie costlabel 16)
302   (trace_ends_flag: trace_ends_with_ret)
303    (start_status: Status) (final_status: Status)
304      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
305        start_status final_status) on the_trace:
306 compute_trace_label_label_cost_using_paid cost_labels … the_trace =
307 compute_max_trace_label_label_cost … the_trace ≝ ?
308and compute_trace_any_label_cost_using_paid_ok
309  (cost_labels: BitVectorTrie costlabel 16)
310  (trace_ends_flag: trace_ends_with_ret)
311   (start_status: Status) (final_status: Status)
312     (the_trace: trace_any_label (ASM_abstract_status cost_labels)
313      trace_ends_flag start_status final_status) on the_trace:     
314  compute_paid_trace_any_label cost_labels trace_ends_flag … the_trace
315  +compute_trace_any_label_cost_using_paid cost_labels trace_ends_flag … the_trace
316  =compute_max_trace_any_label_cost cost_labels trace_ends_flag … the_trace ≝ ?
317and compute_trace_label_return_cost_using_paid_ok
318  (cost_labels: BitVectorTrie costlabel 16)
319  (start_status: Status) (final_status: Status)
320    (the_trace: trace_label_return (ASM_abstract_status cost_labels)
321     start_status final_status) on the_trace:
322 compute_trace_label_return_cost_using_paid cost_labels … the_trace =
323 compute_max_trace_label_return_cost cost_labels … the_trace ≝ ?.
324[ cases the_trace #endsf #ss #es #tr #H normalize
325  @compute_trace_any_label_cost_using_paid_ok
326| cases the_trace
327  [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O %
328  | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O %
329  | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #tr2 whd in ⊢ (??(?%%)%);
330    <compute_trace_any_label_cost_using_paid_ok
331    <compute_trace_label_return_cost_using_paid_ok
332    -compute_trace_label_label_cost_using_paid_ok
333    -compute_trace_label_return_cost_using_paid_ok
334    -compute_trace_any_label_cost_using_paid_ok
335    >commutative_plus in ⊢ (???(?%?));
336    >commutative_plus in ⊢ (??(??%)?);
337    >associative_plus >associative_plus in ⊢ (???%); @eq_f2 try %
338    <associative_plus <commutative_plus %
339  | #ef #sp #si #se #H1 #tr #H2 #H3 whd in ⊢ (??(?%%)%); >associative_plus @eq_f2
340    [ % | @compute_trace_any_label_cost_using_paid_ok ]
341  ]
342| cases the_trace
343  [ #sb #sa #tr normalize @compute_trace_label_label_cost_using_paid_ok
344  | #si #sl #sf #tr1 #tr2 normalize @eq_f2
345    [ @compute_trace_label_label_cost_using_paid_ok
346    | @compute_trace_label_return_cost_using_paid_ok ]]]
347qed.
348
349(*
350let rec compute_paid_trace_label_return
351  (cost_labels: BitVectorTrie costlabel 16)
352  (start_status: Status) (final_status: Status)
353    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
354      on the_trace: nat ≝
355 match the_trace with
356  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label … trace_to_lift
357  | tlr_step initial labelled final labelled_trace ret_trace ⇒
358      let labelled_cost ≝ compute_paid_trace_label_label … labelled_trace in
359      let return_cost ≝ compute_paid_trace_label_return … ret_trace in
360        labelled_cost + return_cost
361  ].
362*)
363
364let rec compute_cost_trace_label_label
365  (cost_labels: BitVectorTrie costlabel 16)
366   (trace_ends_flag: trace_ends_with_ret)
367    (start_status: Status) (final_status: Status)
368      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
369        start_status final_status) on the_trace:
370         list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
371  match the_trace with
372  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
373     let pc ≝ program_counter … initial in
374     let label ≝
375      match lookup_opt … pc cost_labels return λx. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
376      [ None ⇒ λabs. ⊥
377      | Some l ⇒ λ_. l ] labelled_proof in
378     (mk_Sig … label ?)::compute_cost_trace_any_label … given_trace
379  ]
380and compute_cost_trace_any_label
381  (cost_labels: BitVectorTrie costlabel 16)
382  (trace_ends_flag: trace_ends_with_ret)
383   (start_status: Status) (final_status: Status)
384     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
385       on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
386  match the_trace with
387  [ tal_base_not_return the_status _ _ _ _ ⇒ []
388  | tal_base_return the_status _ _ _ ⇒ []
389  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
390     _ _ _ call_trace final_trace ⇒
391      let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
392      let final_cost_trace ≝ compute_cost_trace_any_label cost_labels end_flag … final_trace in
393        call_cost_trace @ final_cost_trace
394  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
395       compute_cost_trace_any_label cost_labels end_flag
396        status_init status_end tail_trace
397  ]
398and compute_cost_trace_label_return
399  (cost_labels: BitVectorTrie costlabel 16)
400  (start_status: Status) (final_status: Status)
401    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
402      on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
403  match the_trace with
404  [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
405  | tlr_step initial labelled final labelled_trace ret_trace ⇒
406      let labelled_cost ≝ compute_cost_trace_label_label … labelled_trace in
407      let return_cost ≝ compute_cost_trace_label_return … ret_trace in
408        labelled_cost @ return_cost
409  ].
410 [ %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
411  cases (lookup_opt costlabel … pc cost_labels) normalize
412  [ #abs cases abs | // ]
413 | // ]
414qed.
415
416(* XXX: zero in base cases (where the trace is a singleton transition) because
417        we are counting until one from end
418*)
419let rec trace_any_label_length
420  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
421    (start_status: Status) (final_status: Status)
422      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
423        on the_trace: nat ≝
424  match the_trace with
425  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
426  | tal_base_return the_status _ _ _ ⇒ 0
427  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒
428      let tail_length ≝ trace_any_label_length … final_trace in
429      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
430        pc_difference + tail_length
431  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
432      let tail_length ≝ trace_any_label_length … tail_trace in
433      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
434        pc_difference + tail_length       
435  ].
436
437(* XXX: commented out in favour of above
438let rec trace_label_label_length
439  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
440    (start_status: Status) (final_status: Status)
441      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
442        on the_trace: nat ≝
443  match the_trace with
444  [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
445  ]
446and trace_any_label_length
447  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
448    (start_status: Status) (final_status: Status)
449      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
450        on the_trace: nat ≝
451  match the_trace with
452  [ tal_base_not_return the_status _ _ _ _ ⇒ ?
453  | tal_base_return the_status _ _ _ ⇒ ?
454  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace final_trace ⇒ ?
455  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ ?
456  ]
457and trace_label_return_length
458  (cost_labels: BitVectorTrie costlabel 16) (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 ⇒ ?
463  | tlr_step initial labelled final labelled_trace ret_trace ⇒ ?
464  ].
465  cases daemon
466qed.
467*)
468
469(* Experiments with block_cost first!
470lemma reachable_program_counter_to_compute_trace_any_label_length_le_program_size:
471  ∀start_status, final_status: Status.
472  ∀code_memory: BitVectorTrie Byte 16.
473  ∀program_size: nat.
474  ∀cost_labels: BitVectorTrie costlabel 16.
475  ∀trace_ends_flag: trace_ends_with_ret.
476  ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
477  let start_program_counter ≝ program_counter … start_status in
478  let final_program_counter ≝ program_counter … final_status in
479    reachable_program_counter code_memory program_size start_program_counter →
480      nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter).
481  cases daemon
482qed.
483
484lemma reachable_program_counter_to_compute_trace_label_label_length_le_program_size:
485  ∀start_status, final_status: Status.
486  ∀code_memory: BitVectorTrie Byte 16.
487  ∀program_size: nat.
488  ∀cost_labels: BitVectorTrie costlabel 16.
489  ∀trace_ends_flag: trace_ends_with_ret.
490  ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
491  let start_program_counter ≝ program_counter … start_status in
492  let final_program_counter ≝ program_counter … final_status in
493    reachable_program_counter code_memory program_size start_program_counter →
494      nat_of_bitvector … start_program_counter ≤ program_size + (nat_of_bitvector … final_program_counter).
495  #start_status #final_status #code_memory #program_size #cost_labels #trace_ends_flag #the_trace
496  cases daemon
497qed.
498
499corollary reachable_program_counter_to_compute_trace_length_le_program_size:
500  ∀start_status, final_status: Status.
501  ∀code_memory: BitVectorTrie Byte 16.
502  ∀program_size: nat.
503  ∀cost_labels: BitVectorTrie costlabel 16.
504  ∀trace_ends_flag: trace_ends_with_ret.
505  ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
506  let program_counter ≝ program_counter … start_status in
507    reachable_program_counter code_memory program_size program_counter →
508      trace_length start_status final_status ≤ program_size.
509  cases daemon
510qed. *)
511
512include alias "arithmetics/nat.ma".
513include alias "basics/logic.ma".
514
515lemma and_intro_right:
516  ∀a, b: Prop.
517    a → (a → b) → a ∧ b.
518  #a #b /3/
519qed.
520
521lemma lt_m_n_to_exists_o_plus_m_n:
522  ∀m, n: nat.
523    m < n → ∃o: nat. m + o = n.
524  #m #n
525  cases m
526  [1:
527    #irrelevant
528    %{n} %
529  |2:
530    #m' #lt_hyp
531    %{(n - S m')}
532    >commutative_plus in ⊢ (??%?);
533    <plus_minus_m_m
534    [1:
535      %
536    |2:
537      @lt_S_to_lt
538      assumption
539    ]
540  ]
541qed.
542
543lemma lt_O_n_to_S_pred_n_n:
544  ∀n: nat.
545    0 < n → S (pred n) = n.
546  #n
547  cases n
548  [1:
549    #absurd
550    cases(lt_to_not_zero 0 0 absurd)
551  |2:
552    #n' #lt_hyp %
553  ]
554qed.
555
556lemma exists_plus_m_n_to_exists_Sn:
557  ∀m, n: nat.
558    m < n → ∃p: nat. S p = n.
559  #m #n
560  cases m
561  [1:
562    #lt_hyp %{(pred n)}
563    @(lt_O_n_to_S_pred_n_n … lt_hyp)
564  |2:
565    #m' #lt_hyp %{(pred n)}
566    @(lt_O_n_to_S_pred_n_n)
567    @(transitive_le … (S m') …)
568    [1:
569      //
570    |2:
571      @lt_S_to_lt
572      assumption
573    ]
574  ]
575qed.
576   
577
578let rec block_cost_trace_any_label_static_dynamic_ok
579  (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
580    (trace_ends_flag: ?) (start_status: Status) (final_status: Status)
581      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
582        on the_trace:
583          let code_memory ≝ code_memory … start_status in
584          let program_counter ≝ program_counter … start_status in
585            ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
586            ∀good_program_witness: good_program code_memory total_program_size.
587              (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
588                block_cost code_memory program_counter total_program_size cost_labels reachable_program_counter_witness good_program_witness =
589                  compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝ ?.
590    letin code_memory ≝ (code_memory … start_status)
591    letin program_counter ≝ (program_counter … start_status)
592    #reachable_program_counter_witness #good_program_witness
593    generalize in match (refl … final_status);
594    generalize in match (refl … start_status);
595    cases the_trace in ⊢ (???% → ???% → %);
596    [1:
597      #start_status' #final_status' #execute_hyp #classifier_hyp #costed_hyp
598      #start_status_refl #final_status_refl destruct
599      whd in match (trace_any_label_length ? ? ? ? ?);
600      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
601      @and_intro_right
602      [1:
603        generalize in match reachable_program_counter_witness;
604        whd in match (reachable_program_counter code_memory total_program_size program_counter);
605        * #irrelevant #relevant
606        lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)
607        #hyp assumption
608      |2:
609        * #n #trace_length_hyp
610        whd in match block_cost; normalize nodelta
611        generalize in match reachable_program_counter_witness;
612        generalize in match good_program_witness;
613        <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);
614        -reachable_program_counter_witness #reachable_program_counter_witness
615        -good_program_witness #good_program_witness
616        whd in ⊢ (??%?); @pair_elim
617      ]
618    |2:
619      #start_status' #final_status' #execute_hyp #classified_hyp
620      #start_status_refl #final_status_refl destruct
621      whd in match (trace_any_label_length ? ? ? ? ?);
622      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
623      @and_intro_right
624      [1:
625        generalize in match reachable_program_counter_witness;
626        whd in match (reachable_program_counter code_memory total_program_size program_counter);
627        * #irrelevant #relevant
628        lapply (exists_plus_m_n_to_exists_Sn (nat_of_bitvector … program_counter) total_program_size relevant)
629        #hyp assumption
630      |2:
631        * #n #trace_length_hyp
632        whd in match block_cost; normalize nodelta
633        generalize in match reachable_program_counter_witness;
634        generalize in match good_program_witness;
635        <trace_length_hyp in ⊢ (∀_:?. ∀_:?. ??(???%??????)?);
636        -reachable_program_counter_witness #reachable_program_counter_witness
637        -good_program_witness #good_program_witness
638        whd in match (0 + S n); whd in ⊢ (??%?);
639      ]
640    |3:
641      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
642      #status_final #execute_hyp #classifier_hyp #after_return_hyp
643      #trace_label_return #trace_any_label #start_status_refl #final_status_refl
644      destruct
645      whd in match (trace_any_label_length ? ? ? ? ?);
646      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
647      @and_intro_right
648      [1:
649      |2:
650      ]
651    |4:
652      #end_flag #status_pre #status_init #status_end #execute_hyp #trace_any_label
653      #classifier_hyp #costed_hyp #start_status_refl #final_status_refl
654      destruct
655      whd in match (trace_any_label_length ? ? ? ? ?);
656      whd in match (compute_paid_trace_any_label ? ? ? ? ?);
657      @and_intro_right
658      [1:
659      |2:
660      ]
661    ]
662  ]
663 
664corollary block_cost_trace_label_labelstatic_dynamic_ok:
665  ∀program_size: nat.
666  ∀cost_labels: BitVectorTrie costlabel 16.
667  ∀trace_ends_flag.
668  ∀start_status: Status.
669  ∀final_status: Status.
670  ∀the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
671  let code_memory ≝ code_memory … start_status in
672  let program_counter ≝ program_counter … start_status in
673  ∀reachable_program_counter_witness: reachable_program_counter code_memory program_size program_counter.
674  ∀good_program_witness: good_program code_memory program_size.
675    (∃n: nat. trace_length start_status final_status + n = program_size) ∧
676      block_cost code_memory program_counter program_size program_size cost_labels reachable_program_counter_witness good_program_witness ? =
677        compute_paid_trace_label_label cost_labels trace_ends_flag start_status final_status the_trace.
678  [2:
679    @le_plus_n_r
680  |1:
681    #program_size #cost_labels #trace_ends_flag #start_status #final_status
682    #the_trace normalize nodelta
683    #reachable_program_counter_witness #good_program_witness
684    generalize in match start_status;
685qed.
686
687(*
688(* To be moved elsewhere*)
689lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m.
690 #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) //
691qed.
692*)
693
694(* This shoudl go in bigops! *)
695theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B.
696 \big[op,nil]_{i<k1+k2|p i} (f i) =
697 op \big[op,nil]_{i<k2|p (i+k1)} (f (i+k1)) \big[op,nil]_{i<k1|p i} (f i).
698 #k1 #k2 #p #B #nil #op #f >bigop_sum >commutative_plus @same_bigop #i @leb_elim normalize
699 [2,4: //
700 | #H1 #H2 <plus_minus_m_m //
701 | #H1 #H2 #H3 <plus_minus_m_m //]
702qed.
703
704(* This is taken by sigma_pi.ma that does not compile now *)
705definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
706   (λa,b,c.sym_eq ??? (associative_plus a b c)).
707
708definition natACop ≝ mk_ACop nat 0 natAop commutative_plus.
709
710definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n)))
711   distributive_times_plus.
712
713unification hint  0 ≔ ;
714   S ≟ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
715   (λa,b,c.sym_eq ??? (associative_plus a b c))
716(* ---------------------------------------- *) ⊢
717   plus ≡ op ? ? S.
718
719unification hint  0 ≔ ;
720   S ≟ mk_ACop nat 0 (mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
721   (λa,b,c.sym_eq ??? (associative_plus a b c))) commutative_plus
722(* ---------------------------------------- *) ⊢
723   plus ≡ op ? ? S.
724   
725unification hint  0 ≔ ;
726   S ≟ natDop
727(* ---------------------------------------- *) ⊢
728   plus ≡ sum ? ? S.
729
730unification hint  0 ≔ ;
731   S ≟ natDop
732(* ---------------------------------------- *) ⊢
733   times ≡ prod ? ? S.
734
735notation > "Σ_{ ident i < n } f"
736  with precedence 20
737for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
738
739notation < "Σ_{ ident i < n } f"
740  with precedence 20
741for @{'bigop $n plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f)}.
742
743axiom code_memory_ro_label_label:
744 ∀cost_labels. ∀ends_flag.
745 ∀initial,final. trace_label_label (ASM_abstract_status cost_labels) ends_flag initial final →
746  code_memory … initial = code_memory … final.
747
748(*
749axiom code_memory_ro_label_return:
750 ∀cost_labels.
751 ∀initial,final. trace_label_return (ASM_abstract_status cost_labels) initial final →
752  code_memory … initial = code_memory … final.
753*)
754
755definition tech_cost_of_label0:
756 ∀cost_labels: BitVectorTrie costlabel 16.
757 ∀cost_map: identifier_map CostTag nat.
758 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
759 ∀ctrace:list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k).
760 ∀i,p. present … cost_map (nth_safe ? i ctrace p).
761 #cost_labels #cost_map #codom_dom #ctrace #i #p
762 cases (nth_safe … i ctrace ?) normalize #id * #id_pc #K
763 lapply (codom_dom … K) #k_pres >(lookup_lookup_present … k_pres)
764 % #abs destruct (abs)
765qed.
766
767include alias "arithmetics/nat.ma".
768include alias "basics/logic.ma".
769
770lemma ltb_rect:
771 ∀P:Type[0].∀n,m. (n < m → P) → (¬ n < m → P) → P.
772 #P #n #m lapply (refl … (ltb n m)) cases (ltb n m) in ⊢ (???% → %); #E #H1 #H2
773 [ @H1 @leb_true_to_le @E | @H2 @leb_false_to_not_le @E ]
774qed.
775
776lemma same_ltb_rect:
777 ∀P,n,m,H1,H2,n',m',H1',H2'.
778  ltb n m = ltb n' m' → (∀x,y. H1 x = H1' y) → (∀x,y. H2 x = H2' y) →
779   ltb_rect P n m H1 H2 =
780   ltb_rect P n' m' H1' H2'.
781 #P #n #m #H1 #H2 #n' #m' #H1' #H2' #E #K1 #K2 whd in ⊢ (??%?);
782 cut (∀xxx,yyy,xxx',yyy'.
783   match ltb n m
784   return λx:bool.
785           eq bool (ltb n m) x
786            → (lt n m → P) → (Not (lt n m) → P) → P
787    with
788    [ true ⇒
789        λE0:eq bool (ltb n m) true.
790         λH10:lt n m → P.
791          λH20:Not (lt n m) → P. H10 (xxx E0)
792    | false ⇒
793        λE0:eq bool (ltb n m) false.
794         λH10:lt n m → P.
795          λH20:Not (lt n m) → P. H20 (yyy E0)]
796    (refl … (ltb n m)) H1 H2 =
797   match ltb n' m'
798   return λx:bool.
799           eq bool (ltb n' m') x
800            → (lt n' m' → P) → (Not (lt n' m') → P) → P
801    with
802    [ true ⇒
803        λE0:eq bool (ltb n' m') true.
804         λH10:lt n' m' → P.
805          λH20:Not (lt n' m') → P. H10 (xxx' E0)
806    | false ⇒
807        λE0:eq bool (ltb n' m') false.
808         λH10:lt n' m' → P.
809          λH20:Not (lt n' m') → P. H20 (yyy' E0)]
810    (refl … (ltb n' m')) H1' H2'
811  ) [2: #X @X]
812 >E cases (ltb n' m') #xxx #yyy #xxx' #yyy' normalize
813 [ @K1 | @K2 ]
814qed.
815
816
817definition tech_cost_of_label:
818 ∀cost_labels: BitVectorTrie costlabel 16.
819 ∀cost_map: identifier_map CostTag nat.
820 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
821 list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k) →
822 nat → nat
823≝ λcost_labels,cost_map,codom_dom,ctrace,i.
824 ltb_rect ? i (|ctrace|)
825 (λH. lookup_present ?? cost_map (nth_safe ? i ctrace H) ?)
826 (λ_.0).
827 @tech_cost_of_label0 @codom_dom
828qed.
829
830lemma shift_nth_safe:
831 ∀T,i,l2,l1,K1,K2.
832  nth_safe T i l1 K1 = nth_safe T (i+|l2|) (l2@l1) K2.
833 #T #i #l2 elim l2 normalize
834  [ #l1 #K1 <plus_n_O #K2 %
835  | #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;
836    whd in ⊢ (???%); @IH ]
837qed.
838
839lemma tech_cost_of_label_shift:
840 ∀cost_labels,cost_map,codom_dom,l1,l2,i.
841  i < |l2| →
842   tech_cost_of_label cost_labels cost_map codom_dom l2 i =
843   tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
844 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
845 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
846 [ @(ltb_rect ? i (|l2|)) @(ltb_rect ? (i+|l1|) (|l1@l2|)) #K1 #K2
847   whd in match ltb; normalize nodelta
848   [1: >le_to_leb_true try assumption applyS le_to_leb_true //
849   |4: >not_le_to_leb_false try assumption applyS not_le_to_leb_false
850       change with (¬ ? ≤ ?) in K1; applyS K1
851   |2: @⊥ @(absurd (i+|l1| < |l1@l2|)) // >length_append
852       applyS (monotonic_lt_plus_r … (|l1|)) //
853   |3: @⊥ @(absurd ?? K2) >length_append in K1; #K1 /2 by lt_plus_to_lt_l/ ]
854 | #H1 #H2
855   generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
856   <(shift_nth_safe … H1) #p %
857 | // ]
858qed.
859
860let rec compute_max_trace_label_return_cost_ok_with_trace
861 (cost_labels: BitVectorTrie costlabel 16)
862 (cost_map: identifier_map CostTag nat)
863 (initial: Status) (final: Status)
864 (trace: trace_label_return (ASM_abstract_status cost_labels) initial final)
865 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
866 on trace:
867 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
868   block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres).
869  let ctrace ≝ compute_cost_trace_label_return … trace in
870  compute_max_trace_label_return_cost … trace =
871   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
872    ≝ ?
873and compute_max_trace_label_label_cost_ok_with_trace
874 (cost_labels: BitVectorTrie costlabel 16)
875 (trace_ends_flag: trace_ends_with_ret)
876 (cost_map: identifier_map CostTag nat)
877 (initial: Status) (final: Status)
878 (trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag initial final)
879 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
880 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
881   block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres))
882 on trace:
883  let ctrace ≝ compute_cost_trace_label_label … trace in
884  compute_max_trace_label_label_cost … trace =
885   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
886    ≝ ?.
887cases trace
888[ #sb #sa #tr #dom_codom
889  @compute_max_trace_label_label_cost_ok_with_trace @dom_codom
890| #si #sl #sf #tr1 #tr2 #dom_codom whd in ⊢ (let ctrace ≝ % in ??%?);
891  change with (let ctrace ≝ ? in ? = bigop (|? @ ?|) ?????)
892  >append_length in ⊢ (let ctrace ≝ ? in ???(?%?????));
893  change with (?=?) >bigop_sum_rev >commutative_plus @eq_f2
894  [ >(compute_max_trace_label_return_cost_ok_with_trace … cost_map … codom_dom)
895    -compute_max_trace_label_return_cost_ok_with_trace     
896    [2:lapply (code_memory_ro_label_label … tr1) #E2 <E2 @dom_codom]
897    @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
898  | >(compute_max_trace_label_label_cost_ok_with_trace … cost_map … codom_dom … dom_codom)
899    @same_bigop [//] #i #H #_
900]
901(*
902lemma
903 compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
904  final_status the_trace =
905 
906
907let rec compute_paid_trace_label_label_cost
908  (cost_labels: BitVectorTrie Byte 16)
909   (trace_ends_flag: trace_ends_with_ret)
910    (start_status: Status) (final_status: Status)
911      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
912        start_status final_status) on the_trace: nat ≝
913  match the_trace with
914  [ tll_base _ _ _ given_trace _ ⇒
915      compute_paid_trace_any_label_cost … given_trace
916  ]
917and compute_paid_trace_any_label_cost
918  (cost_labels: BitVectorTrie Byte 16)
919  (trace_ends_flag: trace_ends_with_ret)
920   (start_status: Status) (final_status: Status)
921     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
922       on the_trace: nat ≝
923  match the_trace with
924  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
925  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
926  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
927     _ _ _ call_trace final_trace ⇒
928      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
929      let final_trace_cost ≝ compute_paid_trace_any_label_cost cost_labels end_flag … final_trace in
930        current_instruction_cost + final_trace_cost
931  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
932      let current_instruction_cost ≝ current_instruction_cost status_pre in
933      let tail_trace_cost ≝
934       compute_paid_trace_any_label_cost cost_labels end_flag
935        status_init status_end tail_trace
936      in
937        current_instruction_cost + tail_trace_cost
938  ]
939and compute_paid_trace_label_return_cost
940  (cost_labels: BitVectorTrie Byte 16)
941  (start_status: Status) (final_status: Status)
942    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
943      on the_trace: nat ≝
944  match the_trace with
945  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label_cost … trace_to_lift
946  | tlr_step initial labelled final labelled_trace ret_trace ⇒
947      let labelled_cost ≝ compute_paid_trace_label_label_cost … labelled_trace in
948      let return_cost ≝ compute_paid_trace_label_return_cost … ret_trace in
949        labelled_cost + return_cost
950  ].
951
952let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
953 | (call b bf tr af tl) as self ⇒
954    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
955    trace_lab_rec_cost' tl
956
957theorem main_lemma:
958 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
959
960axiom lemma1:
961 ∀p: simple_path.
962  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
963
964axiom lemma2:
965 ∀s,l,cost_map.
966  is_labelled l s →
967   traverse_cost_internal s = cost_map l.
968
969axiom main_statement:
970 ∀s.
971 ∀cost_map.
972 let p ≝ compute_simple_path0 s in
973 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
974
975axiom main_statement:
976 ∀s.
977 ∀cost_map.
978 let p ≝ compute_simple_path0 s in
979  execute' (path_length p) s = 〈s',τ〉 →
980   Timer s' - Timer s = ∑ τ cost_map. *)
Note: See TracBrowser for help on using the repository browser.