source: src/ASM/CostsProof.ma @ 1692

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

resolved conflict in asm costs this morning

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