source: src/ASM/CostsProof.ma @ 1587

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

changes from today, including removing indexing of problematic function in utilities/binary/positive.ma

File size: 30.2 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4include "common/StructuredTraces.ma".
5
6let rec compute_max_trace_label_label_cost
7  (cost_labels: BitVectorTrie costlabel 16)
8   (trace_ends_flag: trace_ends_with_ret)
9    (start_status: Status) (final_status: Status)
10      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
11        start_status final_status) on the_trace: nat ≝
12  match the_trace with
13  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
14      compute_max_trace_any_label_cost … given_trace
15  ]
16and compute_max_trace_any_label_cost
17  (cost_labels: BitVectorTrie costlabel 16)
18  (trace_ends_flag: trace_ends_with_ret)
19   (start_status: Status) (final_status: Status)
20     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
21       on the_trace: nat ≝
22  match the_trace with
23  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
24  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
25  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
26     _ _ _ call_trace final_trace ⇒
27      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
28      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
29      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
30        call_trace_cost + current_instruction_cost + final_trace_cost
31  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
32      let current_instruction_cost ≝ current_instruction_cost status_pre in
33      let tail_trace_cost ≝
34       compute_max_trace_any_label_cost cost_labels end_flag
35        status_init status_end tail_trace
36      in
37        current_instruction_cost + tail_trace_cost
38  ]
39and compute_max_trace_label_return_cost
40  (cost_labels: BitVectorTrie costlabel 16)
41  (start_status: Status) (final_status: Status)
42    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
43      on the_trace: nat ≝
44  match the_trace with
45  [ tlr_base before after trace_to_lift ⇒ compute_max_trace_label_label_cost … trace_to_lift
46  | tlr_step initial labelled final labelled_trace ret_trace ⇒
47      let labelled_cost ≝ compute_max_trace_label_label_cost … labelled_trace in
48      let return_cost ≝ compute_max_trace_label_return_cost … ret_trace in
49        labelled_cost + return_cost
50  ].
51
52(*Useless now?
53(* To be moved *)
54lemma pred_minus_1:
55  ∀m, n: nat.
56  ∀proof: n < m.
57    pred (m - n) = m - n - 1.
58  #m #n
59  cases m
60  [ #proof
61    cases(lt_to_not_zero … proof)
62  | #m' #proof
63    normalize in ⊢ (???%);
64    cases n
65    [ normalize //
66    | #n' normalize
67      cases(m' - n')
68      [ %
69      | #Sm_n'
70        normalize //
71      ]
72    ]
73  ]
74qed.
75
76lemma succ_m_plus_one:
77  ∀m: nat.
78    S m = m + 1.
79 //
80qed.*)
81
82include alias "arithmetics/nat.ma".
83
84(*
85lemma minus_m_n_minus_minus_plus_1:
86  ∀m, n: nat.
87  ∀proof: n < m.
88    m - n = (m - n - 1) + 1.
89 /3 by lt_plus_to_minus_r, plus_minus/
90qed.
91
92lemma plus_minus_rearrangement_1:
93  ∀m, n, o: nat.
94  ∀proof_n_m: n ≤ m.
95  ∀proof_m_o: m ≤ o.
96    (m - n) + (o - m) = o - n.
97  #m #n #o #H1 #H2
98  lapply (minus_to_plus … H1 (refl …)) #K1 >K1
99  lapply (minus_to_plus … H2 (refl …)) #K2 >K2
100  /2 by plus_minus/
101qed.
102
103lemma plus_minus_rearrangement_2:
104  ∀m, n, o: nat. n ≤ m → o ≤ n →
105    (m - n) + (n - o) = m - o.
106 /2 by plus_minus_rearrangement_1/
107qed.
108
109lemma m_le_plus_n_m:
110  ∀m, n: nat.
111    m ≤ n + m.
112  #m #n //
113qed.
114
115lemma n_plus_m_le_o_to_m_le_o:
116  ∀m, n, o: nat.
117    n + m ≤ o → m ≤ o.
118  #m #n #o #assm /2 by le_plus_b/
119qed.
120
121lemma m_minus_n_plus_o_m_minus_n_minus_o:
122  ∀m, n, o: nat.
123    m - (n + o) = m - n - o.
124  #m #n #o /2 by /
125qed.
126*)
127
128let rec compute_max_trace_label_label_cost_is_ok
129  (cost_labels: BitVectorTrie costlabel 16)
130   (trace_ends_flag: trace_ends_with_ret)
131    (start_status: Status) (final_status: Status)
132      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
133        start_status final_status) on the_trace:
134          clock … final_status = (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
135and compute_max_trace_any_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_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
140       on the_trace:
141         clock … final_status = (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
142and compute_max_trace_label_return_cost_is_ok
143  (cost_labels: BitVectorTrie costlabel 16)
144  (start_status: Status) (final_status: Status)
145    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
146      on the_trace:
147        clock … final_status = (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace) + clock … start_status ≝ ?.
148  [1:
149    cases the_trace
150    #ends_flag #start_status #end_status #any_label_trace #is_costed
151    normalize @compute_max_trace_any_label_cost_is_ok
152  |2:
153    cases the_trace
154    [1,2:
155      #start_status #final_status #is_next #is_not_return try (#is_costed)
156      change with (current_instruction_cost start_status) in ⊢ (???(?%?));
157      cases(is_next)
158      cases(execute_1 start_status)
159      whd in match eject; normalize nodelta;
160      #the_status #assm >assm %
161    |3:
162      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
163      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
164      change with (
165      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
166      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
167      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
168        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?));
169      normalize nodelta;
170      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
171          status_final final_trace)
172      >(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
173        status_after_fun_call call_trace)
174      cases(is_next) in match (clock … status_start_fun_call);
175      cases(execute_1 status_pre_fun_call);
176      #the_status
177      whd in match eject; normalize nodelta;
178      #assm >assm
179      <associative_plus in ⊢ (??%?);
180      <commutative_plus in match (
181        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
182          + compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace);
183      >associative_plus in ⊢ (??%?);
184      <commutative_plus in match (
185        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
186          + (current_instruction_cost status_pre_fun_call
187              + clock (BitVectorTrie Byte 16) status_pre_fun_call));
188      >associative_plus in ⊢ (??%?);
189      <commutative_plus in match (
190         clock (BitVectorTrie Byte 16) status_pre_fun_call
191           + compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace);
192      <(associative_plus (
193         (compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace)))
194      <associative_plus in ⊢ (??%?); %
195    |4:
196      #end_flag #status_pre #status_init #status_end #is_next
197      #trace_any_label #is_other #is_not_costed
198      change with (
199      let current_instruction_cost ≝ current_instruction_cost status_pre in
200      let tail_trace_cost ≝
201       compute_max_trace_any_label_cost cost_labels end_flag
202        status_init status_end trace_any_label
203      in
204        current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?));
205      normalize nodelta;
206      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
207         status_init status_end trace_any_label)
208      cases(is_next) in match (clock … status_init);
209      cases(execute_1 status_pre)
210      #the_status whd in match eject; normalize nodelta;
211      #assm >assm <associative_plus in ⊢ (??%?);
212      >commutative_plus in match (
213        compute_max_trace_any_label_cost cost_labels end_flag status_init status_end trace_any_label
214          + current_instruction_cost status_pre);
215      %
216    ]
217  |3:
218    cases the_trace
219    [1:
220      #status_before #status_after #trace_to_lift
221      normalize @compute_max_trace_label_label_cost_is_ok
222    |2:
223      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
224      normalize
225      >(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
226      >(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
227      <associative_plus in ⊢ (??%?);
228      >commutative_plus in match (
229        compute_max_trace_label_return_cost cost_labels status_labelled status_final ret_trace
230          + compute_max_trace_label_label_cost cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
231      %
232    ]
233  ].
234qed.
235
236(* XXX: work below here: *)
237
238let rec compute_paid_trace_any_label
239  (cost_labels: BitVectorTrie costlabel 16)
240  (trace_ends_flag: trace_ends_with_ret)
241   (start_status: Status) (final_status: Status)
242     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
243       on the_trace: nat ≝
244  match the_trace with
245  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
246  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
247  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
248     _ _ _ call_trace final_trace ⇒
249      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
250      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
251        current_instruction_cost + final_trace_cost
252  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
253      let current_instruction_cost ≝ current_instruction_cost status_pre in
254      let tail_trace_cost ≝
255       compute_paid_trace_any_label cost_labels end_flag
256        status_init status_end tail_trace
257      in
258        current_instruction_cost + tail_trace_cost
259  ].
260
261definition compute_paid_trace_label_label ≝
262 λcost_labels: BitVectorTrie costlabel 16.
263  λtrace_ends_flag: trace_ends_with_ret.
264   λstart_status: Status.
265    λfinal_status: Status.
266     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
267      start_status final_status.
268  match the_trace with
269  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
270      compute_paid_trace_any_label … given_trace
271  ].
272
273let rec compute_trace_label_label_cost_using_paid
274  (cost_labels: BitVectorTrie costlabel 16)
275   (trace_ends_flag: trace_ends_with_ret)
276    (start_status: Status) (final_status: Status)
277      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
278        start_status final_status) on the_trace: nat ≝
279  match the_trace with
280  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
281      compute_paid_trace_label_label cost_labels … the_trace +
282      compute_trace_any_label_cost_using_paid … given_trace
283  ]
284and compute_trace_any_label_cost_using_paid
285  (cost_labels: BitVectorTrie costlabel 16)
286  (trace_ends_flag: trace_ends_with_ret)
287   (start_status: Status) (final_status: Status)
288     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
289       on the_trace: nat ≝
290  match the_trace with
291  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
292  | tal_base_return the_status _ _ _ ⇒ 0
293  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
294     _ _ _ call_trace final_trace ⇒
295      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
296      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cost_labels end_flag … final_trace in
297        call_trace_cost + final_trace_cost
298  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
299     compute_trace_any_label_cost_using_paid cost_labels end_flag
300      status_init status_end tail_trace
301  ]
302and compute_trace_label_return_cost_using_paid
303  (cost_labels: BitVectorTrie costlabel 16)
304  (start_status: Status) (final_status: Status)
305    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
306      on the_trace: nat ≝
307  match the_trace with
308  [ tlr_base before after trace_to_lift ⇒ compute_trace_label_label_cost_using_paid … trace_to_lift
309  | tlr_step initial labelled final labelled_trace ret_trace ⇒
310      let labelled_cost ≝ compute_trace_label_label_cost_using_paid … labelled_trace in
311      let return_cost ≝ compute_trace_label_return_cost_using_paid … ret_trace in
312        labelled_cost + return_cost
313  ].
314
315let rec compute_trace_label_label_cost_using_paid_ok
316  (cost_labels: BitVectorTrie costlabel 16)
317   (trace_ends_flag: trace_ends_with_ret)
318    (start_status: Status) (final_status: Status)
319      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
320        start_status final_status) on the_trace:
321 compute_trace_label_label_cost_using_paid cost_labels … the_trace =
322 compute_max_trace_label_label_cost … the_trace ≝ ?
323and compute_trace_any_label_cost_using_paid_ok
324  (cost_labels: BitVectorTrie costlabel 16)
325  (trace_ends_flag: trace_ends_with_ret)
326   (start_status: Status) (final_status: Status)
327     (the_trace: trace_any_label (ASM_abstract_status cost_labels)
328      trace_ends_flag start_status final_status) on the_trace:     
329  compute_paid_trace_any_label cost_labels trace_ends_flag … the_trace
330  +compute_trace_any_label_cost_using_paid cost_labels trace_ends_flag … the_trace
331  =compute_max_trace_any_label_cost cost_labels trace_ends_flag … the_trace ≝ ?
332and compute_trace_label_return_cost_using_paid_ok
333  (cost_labels: BitVectorTrie costlabel 16)
334  (start_status: Status) (final_status: Status)
335    (the_trace: trace_label_return (ASM_abstract_status cost_labels)
336     start_status final_status) on the_trace:
337 compute_trace_label_return_cost_using_paid cost_labels … the_trace =
338 compute_max_trace_label_return_cost cost_labels … the_trace ≝ ?.
339[ cases the_trace #endsf #ss #es #tr #H normalize
340  @compute_trace_any_label_cost_using_paid_ok
341| cases the_trace
342  [ #ss #fs #H1 #H2 #H3 whd in ⊢ (??(?%%)%); <plus_n_O %
343  | #ss #fs #H1 #H2 whd in ⊢ (??(?%%)%); <plus_n_O %
344  | #ef #spfc #ssfc #safc #sf #H1 #H2 #H3 #tr1 #tr2 whd in ⊢ (??(?%%)%);
345    <compute_trace_any_label_cost_using_paid_ok
346    <compute_trace_label_return_cost_using_paid_ok
347    -compute_trace_label_label_cost_using_paid_ok
348    -compute_trace_label_return_cost_using_paid_ok
349    -compute_trace_any_label_cost_using_paid_ok
350    >commutative_plus in ⊢ (???(?%?));
351    >commutative_plus in ⊢ (??(??%)?);
352    >associative_plus >associative_plus in ⊢ (???%); @eq_f2 try %
353    <associative_plus <commutative_plus %
354  | #ef #sp #si #se #H1 #tr #H2 #H3 whd in ⊢ (??(?%%)%); >associative_plus @eq_f2
355    [ % | @compute_trace_any_label_cost_using_paid_ok ]
356  ]
357| cases the_trace
358  [ #sb #sa #tr normalize @compute_trace_label_label_cost_using_paid_ok
359  | #si #sl #sf #tr1 #tr2 normalize @eq_f2
360    [ @compute_trace_label_label_cost_using_paid_ok
361    | @compute_trace_label_return_cost_using_paid_ok ]]]
362qed.
363
364(*
365let rec compute_paid_trace_label_return
366  (cost_labels: BitVectorTrie costlabel 16)
367  (start_status: Status) (final_status: Status)
368    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
369      on the_trace: nat ≝
370 match the_trace with
371  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label … trace_to_lift
372  | tlr_step initial labelled final labelled_trace ret_trace ⇒
373      let labelled_cost ≝ compute_paid_trace_label_label … labelled_trace in
374      let return_cost ≝ compute_paid_trace_label_return … ret_trace in
375        labelled_cost + return_cost
376  ].
377*)
378
379let rec compute_cost_trace_label_label
380  (cost_labels: BitVectorTrie costlabel 16)
381   (trace_ends_flag: trace_ends_with_ret)
382    (start_status: Status) (final_status: Status)
383      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
384        start_status final_status) on the_trace:
385         list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
386  match the_trace with
387  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
388     let pc ≝ program_counter … initial in
389     let label ≝
390      match lookup_opt … pc cost_labels return λx. match x with [None ⇒ False | Some _ ⇒ True] → costlabel with
391      [ None ⇒ λabs. ⊥
392      | Some l ⇒ λ_. l ] labelled_proof in
393     (dp … label ?)::compute_cost_trace_any_label … given_trace
394  ]
395and compute_cost_trace_any_label
396  (cost_labels: BitVectorTrie costlabel 16)
397  (trace_ends_flag: trace_ends_with_ret)
398   (start_status: Status) (final_status: Status)
399     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
400       on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
401  match the_trace with
402  [ tal_base_not_return the_status _ _ _ _ ⇒ []
403  | tal_base_return the_status _ _ _ ⇒ []
404  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
405     _ _ _ call_trace final_trace ⇒
406      let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
407      let final_cost_trace ≝ compute_cost_trace_any_label cost_labels end_flag … final_trace in
408        call_cost_trace @ final_cost_trace
409  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
410       compute_cost_trace_any_label cost_labels end_flag
411        status_init status_end tail_trace
412  ]
413and compute_cost_trace_label_return
414  (cost_labels: BitVectorTrie costlabel 16)
415  (start_status: Status) (final_status: Status)
416    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
417      on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
418  match the_trace with
419  [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
420  | tlr_step initial labelled final labelled_trace ret_trace ⇒
421      let labelled_cost ≝ compute_cost_trace_label_label … labelled_trace in
422      let return_cost ≝ compute_cost_trace_label_return … ret_trace in
423        labelled_cost @ return_cost
424  ].
425 [ %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
426  cases (lookup_opt costlabel … pc cost_labels) normalize
427  [ #abs cases abs | // ]
428 | // ]
429qed.
430
431(* ??????????????????????? *)
432axiom block_cost_static_dynamic_ok:
433 ∀cost_labels: BitVectorTrie costlabel 16.
434 ∀trace_ends_flag.
435 ∀start_status: Status.
436 ∀final_status: Status.
437 ∀the_trace:
438  trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
439   start_status final_status.
440 let mem ≝ code_memory … start_status in
441 let pc ≝ program_counter … start_status in
442 let program_size ≝ 2^16 in
443  block_cost mem cost_labels pc program_size =
444  compute_paid_trace_label_label cost_labels trace_ends_flag
445   start_status final_status the_trace.
446
447(*
448(* To be moved elsewhere*)
449lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m.
450 #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) //
451qed.
452*)
453
454include "arithmetics/bigops.ma".
455
456(* This shoudl go in bigops! *)
457theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B.
458 \big[op,nil]_{i<k1+k2|p i} (f i) =
459 op \big[op,nil]_{i<k2|p (i+k1)} (f (i+k1)) \big[op,nil]_{i<k1|p i} (f i).
460 #k1 #k2 #p #B #nil #op #f >bigop_sum >commutative_plus @same_bigop #i @leb_elim normalize
461 [2,4: //
462 | #H1 #H2 <plus_minus_m_m //
463 | #H1 #H2 #H3 <plus_minus_m_m //]
464qed.
465
466(* This is taken by sigma_pi.ma that does not compile now *)
467definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
468   (λa,b,c.sym_eq ??? (associative_plus a b c)).
469
470definition natACop ≝ mk_ACop nat 0 natAop commutative_plus.
471
472definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n)))
473   distributive_times_plus.
474
475unification hint  0 ≔ ;
476   S ≟ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
477   (λa,b,c.sym_eq ??? (associative_plus a b c))
478(* ---------------------------------------- *) ⊢
479   plus ≡ op ? ? S.
480
481unification hint  0 ≔ ;
482   S ≟ mk_ACop nat 0 (mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
483   (λa,b,c.sym_eq ??? (associative_plus a b c))) commutative_plus
484(* ---------------------------------------- *) ⊢
485   plus ≡ op ? ? S.
486   
487unification hint  0 ≔ ;
488   S ≟ natDop
489(* ---------------------------------------- *) ⊢
490   plus ≡ sum ? ? S.
491
492unification hint  0 ≔ ;
493   S ≟ natDop
494(* ---------------------------------------- *) ⊢
495   times ≡ prod ? ? S.
496
497notation "Σ_{ ident i < n } f"
498  with precedence 20
499for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
500
501axiom code_memory_ro_label_label:
502 ∀cost_labels. ∀ends_flag.
503 ∀initial,final. trace_label_label (ASM_abstract_status cost_labels) ends_flag initial final →
504  code_memory … initial = code_memory … final.
505
506(*
507axiom code_memory_ro_label_return:
508 ∀cost_labels.
509 ∀initial,final. trace_label_return (ASM_abstract_status cost_labels) initial final →
510  code_memory … initial = code_memory … final.
511*)
512
513definition tech_cost_of_label0:
514 ∀cost_labels: BitVectorTrie costlabel 16.
515 ∀cost_map: identifier_map CostTag nat.
516 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
517 ∀ctrace:list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k).
518 ∀i,p. present … cost_map (nth_safe ? i ctrace p).
519 #cost_labels #cost_map #codom_dom #ctrace #i #p
520 cases (nth_safe … i ctrace ?) normalize #id * #id_pc #K
521 lapply (codom_dom … K) #k_pres >(lookup_lookup_present … k_pres)
522 % #abs destruct (abs)
523qed.
524
525lemma ltb_rect:
526 ∀P:Type[0].∀n,m. (n < m → P) → (¬ n < m → P) → P.
527 #P #n #m lapply (refl … (ltb n m)) cases (ltb n m) in ⊢ (???% → %); #E #H1 #H2
528 [ @H1 @leb_true_to_le @E | @H2 @leb_false_to_not_le @E ]
529qed.
530
531lemma same_ltb_rect:
532 ∀P,n,m,H1,H2,n',m',H1',H2'.
533  ltb n m = ltb n' m' → (∀x,y. H1 x = H1' y) → (∀x,y. H2 x = H2' y) →
534   ltb_rect P n m H1 H2 =
535   ltb_rect P n' m' H1' H2'.
536 #P #n #m #H1 #H2 #n' #m' #H1' #H2' #E #K1 #K2 whd in ⊢ (??%?);
537 cut (∀xxx,yyy,xxx',yyy'.
538   match ltb n m
539   return λx:bool.
540           eq bool (ltb n m) x
541            → (lt n m → P) → (Not (lt n m) → P) → P
542    with
543    [ true ⇒
544        λE0:eq bool (ltb n m) true.
545         λH10:lt n m → P.
546          λH20:Not (lt n m) → P. H10 (xxx E0)
547    | false ⇒
548        λE0:eq bool (ltb n m) false.
549         λH10:lt n m → P.
550          λH20:Not (lt n m) → P. H20 (yyy E0)]
551    (refl … (ltb n m)) H1 H2 =
552   match ltb n' m'
553   return λx:bool.
554           eq bool (ltb n' m') x
555            → (lt n' m' → P) → (Not (lt n' m') → P) → P
556    with
557    [ true ⇒
558        λE0:eq bool (ltb n' m') true.
559         λH10:lt n' m' → P.
560          λH20:Not (lt n' m') → P. H10 (xxx' E0)
561    | false ⇒
562        λE0:eq bool (ltb n' m') false.
563         λH10:lt n' m' → P.
564          λH20:Not (lt n' m') → P. H20 (yyy' E0)]
565    (refl … (ltb n' m')) H1' H2'
566  ) [2: #X @X]
567 >E cases (ltb n' m') #xxx #yyy #xxx' #yyy' normalize
568 [ @K1 | @K2 ]
569qed.
570
571
572definition tech_cost_of_label:
573 ∀cost_labels: BitVectorTrie costlabel 16.
574 ∀cost_map: identifier_map CostTag nat.
575 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
576 list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k) →
577 nat → nat
578≝ λcost_labels,cost_map,codom_dom,ctrace,i.
579 ltb_rect ? i (|ctrace|)
580 (λH. lookup_present ?? cost_map (nth_safe ? i ctrace H) ?)
581 (λ_.0).
582 @tech_cost_of_label0 @codom_dom
583qed.
584
585lemma shift_nth_safe:
586 ∀T,i,l2,l1,K1,K2.
587  nth_safe T i l1 K1 = nth_safe T (i+|l2|) (l2@l1) K2.
588 #T #i #l2 elim l2 normalize
589  [ #l1 #K1 <plus_n_O #K2 %
590  | #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2;
591    whd in ⊢ (???%); @IH ]
592qed.
593
594lemma tech_cost_of_label_shift:
595 ∀cost_labels,cost_map,codom_dom,l1,l2,i.
596  i < |l1| →
597   tech_cost_of_label cost_labels cost_map codom_dom l2 i =
598   tech_cost_of_label cost_labels cost_mnth_safe ? i ctrace H) ?ap codom_dom (l1@l2) (i+|l1|).
599 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
600 cut (ltb i (|l2|) = ltb (i+|l1|) (|l1@l2|))
601 [ change with (leb ?? = leb ??); @leb_elim
602   [ #H1 change with (i < ?) in H1; >le_to_leb_true [//] change with (? < ?)
603     >append_length >commutative_plus @monotonic_lt_plus_r //
604   | #H1 change with (¬ i < ?) in H1; >not_le_to_leb_false [//]
605     >append_length >commutative_plus % #H2
606     change with (? < ?) in H2; @(absurd ?? H1) @(lt_plus_to_lt_r … H2) ]
607 | #E whd in match tech_cost_of_label; normalize nodelta
608 @same_ltb_rect [@E]
609 [ #K1 #K2 lapply (shift_nth_safe ? i l1 l2 K1 K2) #H check eq_f
610   lapply (eq_f ?? (lookup_present CostTag nat cost_Map) ?? H)
611
612   
613 
614  cut (decide_bool (ltb i (|l2|)) = decide_bool (ltb (i+(|l1|)) (|l1@l2|)))
615  whd in match tech_cost_of_label; normalize nodelta
616   
617
618let rec compute_max_trace_label_return_cost_ok_with_trace
619 (cost_labels: BitVectorTrie costlabel 16)
620 (cost_map: identifier_map CostTag nat)
621 (initial: Status) (final: Status)
622 (trace: trace_label_return (ASM_abstract_status cost_labels) initial final)
623 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
624 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
625   block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres))
626 on trace:
627  let ctrace ≝ compute_cost_trace_label_return … trace in
628  compute_max_trace_label_return_cost … trace =
629   Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)
630    ≝ ?.
631lapply (refl … initial) cases trace in ⊢ (??%? → %);
632[ #sb #sa #tr #_ whd in ⊢ (let ctrace ≝ % in ??%?);
633| #si #sl #sf #tr1 #tr2 #E whd in ⊢ (let ctrace ≝ % in ??%?);
634  change with (let ctrace ≝ ? in ? = bigop (|? @ ?|) ?????)
635  >append_length in ⊢ (let ctrace ≝ ? in ???(?%?????));
636  change with (?=?) >bigop_sum_rev >commutative_plus @eq_f2
637  [ >compute_max_trace_label_return_cost_ok_with_trace
638    -compute_max_trace_label_return_cost_ok_with_trace     
639    [3: @cost_map
640    |2: @codom_dom
641    |4:lapply (code_memory_ro_label_label … tr1) >E #E2 <E2 @dom_codom]
642    @same_bigop [//] #i #H #_ -dom_codom
643    generalize in match (compute_cost_trace_label_return cost_labels sl sf tr2); #l1
644    generalize in match (compute_cost_trace_label_label cost_labels doesnt_end_with_ret si sl tr1);
645
646i < |l1| →
647tech_cost_of_label cost_labels cost_map codom_dom l1 i =
648tech_cost_of_label cost_labels cost_map codom_dom (l2@l1) (i+|l1|)
649
650
651     whd in ⊢ (??%%);
652  |
653  ]
654]
655(*
656lemma
657 compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
658  final_status the_trace =
659 
660
661let rec compute_paid_trace_label_label_cost
662  (cost_labels: BitVectorTrie Byte 16)
663   (trace_ends_flag: trace_ends_with_ret)
664    (start_status: Status) (final_status: Status)
665      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
666        start_status final_status) on the_trace: nat ≝
667  match the_trace with
668  [ tll_base _ _ _ given_trace _ ⇒
669      compute_paid_trace_any_label_cost … given_trace
670  ]
671and compute_paid_trace_any_label_cost
672  (cost_labels: BitVectorTrie Byte 16)
673  (trace_ends_flag: trace_ends_with_ret)
674   (start_status: Status) (final_status: Status)
675     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
676       on the_trace: nat ≝
677  match the_trace with
678  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
679  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
680  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
681     _ _ _ call_trace final_trace ⇒
682      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
683      let final_trace_cost ≝ compute_paid_trace_any_label_cost cost_labels end_flag … final_trace in
684        current_instruction_cost + final_trace_cost
685  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
686      let current_instruction_cost ≝ current_instruction_cost status_pre in
687      let tail_trace_cost ≝
688       compute_paid_trace_any_label_cost cost_labels end_flag
689        status_init status_end tail_trace
690      in
691        current_instruction_cost + tail_trace_cost
692  ]
693and compute_paid_trace_label_return_cost
694  (cost_labels: BitVectorTrie Byte 16)
695  (start_status: Status) (final_status: Status)
696    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
697      on the_trace: nat ≝
698  match the_trace with
699  [ tlr_base before after trace_to_lift ⇒ compute_paid_trace_label_label_cost … trace_to_lift
700  | tlr_step initial labelled final labelled_trace ret_trace ⇒
701      let labelled_cost ≝ compute_paid_trace_label_label_cost … labelled_trace in
702      let return_cost ≝ compute_paid_trace_label_return_cost … ret_trace in
703        labelled_cost + return_cost
704  ].
705
706let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
707 | (call b bf tr af tl) as self ⇒
708    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
709    trace_lab_rec_cost' tl
710
711theorem main_lemma:
712 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
713
714axiom lemma1:
715 ∀p: simple_path.
716  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
717
718axiom lemma2:
719 ∀s,l,cost_map.
720  is_labelled l s →
721   traverse_cost_internal s = cost_map l.
722
723axiom main_statement:
724 ∀s.
725 ∀cost_map.
726 let p ≝ compute_simple_path0 s in
727 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
728
729axiom main_statement:
730 ∀s.
731 ∀cost_map.
732 let p ≝ compute_simple_path0 s in
733  execute' (path_length p) s = 〈s',τ〉 →
734   Timer s' - Timer s = ∑ τ cost_map. *)
Note: See TracBrowser for help on using the repository browser.