source: src/ASM/CostsProof.ma @ 1548

Last change on this file since 1548 was 1548, checked in by sacerdot, 9 years ago

...

File size: 19.2 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4include "common/StructuredTraces.ma".
5
6definition current_instruction ≝
7  λs: Status.
8  let pc ≝ program_counter … s in
9  \fst (\fst (fetch … (code_memory … s) pc)).
10
11definition ASM_classify: Status → status_class ≝
12 λs.
13  match current_instruction s with
14   [ RealInstruction pre ⇒
15     match pre with
16      [ RET ⇒ cl_return
17      | JZ _ ⇒ cl_jump
18      | JNZ _ ⇒ cl_jump
19      | JC _ ⇒ cl_jump
20      | JNC _ ⇒ cl_jump
21      | JB _ _ ⇒ cl_jump
22      | JNB _ _ ⇒ cl_jump
23      | JBC _ _ ⇒ cl_jump
24      | CJNE _ _ ⇒ cl_jump
25      | DJNZ _ _ ⇒ cl_jump
26      | _ ⇒ cl_other
27      ]
28   | ACALL _ ⇒ cl_call
29   | LCALL _ ⇒ cl_call
30   | JMP _ ⇒ cl_call
31   | AJMP _ ⇒ cl_jump
32   | LJMP _ ⇒ cl_jump
33   | SJMP _ ⇒ cl_jump
34   | _ ⇒ cl_other
35   ].
36
37definition current_instruction_is_labelled ≝
38  λcost_labels: BitVectorTrie Byte 16.
39  λs: Status.
40  let pc ≝ program_counter … s in
41    match lookup_opt … pc cost_labels with
42    [ None ⇒ False
43    | _    ⇒ True
44    ].
45
46definition next_instruction_properly_relates_program_counters ≝
47  λbefore: Status.
48  λafter : Status.
49  let size ≝ current_instruction_cost before in
50  let pc_before ≝ program_counter … before in
51  let pc_after ≝ program_counter … after in
52  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
53    sum = pc_after.
54
55definition ASM_abstract_status: BitVectorTrie Byte 16 → abstract_status ≝
56 λcost_labels.
57  mk_abstract_status
58   Status
59   (λs,s'. eject … (execute_1 s) = s')
60   (λs,class. ASM_classify s = class)
61   (current_instruction_is_labelled cost_labels)
62   next_instruction_properly_relates_program_counters.
63
64(*
65definition next_instruction_is_labelled ≝
66  λcost_labels: BitVectorTrie Byte 16.
67  λs: Status.
68  let pc ≝ program_counter … (execute_1 s) in
69    match lookup_opt … pc cost_labels with
70    [ None ⇒ False
71    | _    ⇒ True
72    ].
73
74definition current_instruction_cost ≝
75  λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
76
77definition is_call_p ≝
78  λs.
79  match s with
80  [ ACALL _ ⇒ True
81  | LCALL _ ⇒ True
82  | JMP ⇒ True (* XXX: is function pointer call *)
83  | _ ⇒ False
84  ].
85
86definition next_instruction ≝
87  λs: Status.
88  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
89    instruction.
90
91inductive trace_ends_with_ret: Type[0] ≝
92  | ends_with_ret: trace_ends_with_ret
93  | doesnt_end_with_ret: trace_ends_with_ret.
94
95definition next_instruction_is_labelled ≝
96  λcost_labels: BitVectorTrie Byte 16.
97  λs: Status.
98  let pc ≝ program_counter … (execute 1 s) in
99    match lookup_opt … pc cost_labels with
100    [ None ⇒ False
101    | _    ⇒ True
102    ].
103
104definition next_instruction_properly_relates_program_counters ≝
105  λbefore: Status.
106  λafter : Status.
107  let size ≝ current_instruction_cost before in
108  let pc_before ≝ program_counter … before in
109  let pc_after ≝ program_counter … after in
110  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
111    sum = pc_after.
112
113definition current_instruction ≝
114  λs: Status.
115  let pc ≝ program_counter … s in
116  \fst (\fst (fetch … (code_memory … s) pc)).
117
118definition current_instruction_is_labelled ≝
119  λcost_labels: BitVectorTrie Byte 16.
120  λs: Status.
121  let pc ≝ program_counter … s in
122    match lookup_opt … pc cost_labels with
123    [ None ⇒ False
124    | _    ⇒ True
125    ].
126
127inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
128  | tlr_base:
129      ∀status_before: Status.
130      ∀status_after: Status.
131        trace_label_label cost_labels ends_with_ret status_before status_after →
132        trace_label_return cost_labels status_before status_after
133  | tlr_step:
134      ∀status_initial: Status.
135      ∀status_labelled: Status.
136      ∀status_final: Status.
137          trace_label_label cost_labels doesnt_end_with_ret status_initial status_labelled →
138            trace_label_return cost_labels status_labelled status_final →
139              trace_label_return cost_labels status_initial status_final
140with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
141  | tll_base:
142      ∀ends_flag: trace_ends_with_ret.
143      ∀start_status: Status.
144      ∀end_status: Status.
145        trace_label_label_pre cost_labels ends_flag start_status end_status →
146        current_instruction_is_labelled cost_labels start_status →
147        trace_label_label cost_labels ends_flag start_status end_status
148with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
149  | tllp_base_not_return:
150      ∀start_status: Status.
151        let final_status ≝ execute 1 start_status in
152        current_instruction start_status ≠ (RealInstruction … (RET [[relative]])) →
153        ¬ (is_jump_p (current_instruction start_status)) →
154        current_instruction_is_labelled cost_labels final_status →
155          trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
156  | tllp_base_return:
157      ∀start_status: Status.
158        let final_status ≝ execute 1 start_status in
159          current_instruction start_status = (RealInstruction … (RET [[relative]])) →
160            trace_label_label_pre cost_labels ends_with_ret start_status final_status
161  | tllp_base_jump:
162      ∀start_status: Status.
163        let final_status ≝ execute 1 start_status in
164          is_jump_p (current_instruction start_status) →
165            current_instruction_is_labelled cost_labels final_status →
166              trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
167  | tllp_step_call:
168      ∀end_flag: trace_ends_with_ret.
169      ∀status_pre_fun_call: Status.
170      ∀status_after_fun_call: Status.
171      ∀status_final: Status.
172        let status_start_fun_call ≝ execute 1 status_pre_fun_call in
173          is_call_p (current_instruction status_pre_fun_call) →
174          next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
175          trace_label_return cost_labels status_start_fun_call status_after_fun_call →
176          trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
177            trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
178  | tllp_step_default:
179      ∀end_flag: trace_ends_with_ret.
180      ∀status_pre: Status.
181      ∀status_end: Status.
182        let status_init ≝ execute 1 status_pre in
183          trace_label_label_pre cost_labels end_flag status_init status_end →
184          ¬ (is_call_p (current_instruction status_pre)) →
185          ¬ (is_jump_p (current_instruction status_pre)) →
186          (current_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
187          ¬ (current_instruction_is_labelled cost_labels status_init) →
188            trace_label_label_pre cost_labels end_flag status_pre status_end.
189*)
190
191(* XXX: not us
192definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
193
194lemma simple_path_ok:
195 ∀st: Status.∀H.
196 let p ≝ compute_simple_path0 st H in
197   ∀n.
198    nth_path n p = execute n st ∧
199     (execute' (path_length p) st = 〈st',τ〉 →
200      τ = cost_trace p)
201  ].
202*)
203
204let rec compute_max_trace_label_label_cost
205  (cost_labels: BitVectorTrie Byte 16)
206   (trace_ends_flag: trace_ends_with_ret)
207    (start_status: Status) (final_status: Status)
208      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
209        start_status final_status) on the_trace: nat ≝
210  match the_trace with
211  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
212      compute_max_trace_any_label_cost … given_trace
213  ]
214and compute_max_trace_any_label_cost
215  (cost_labels: BitVectorTrie Byte 16)
216  (trace_ends_flag: trace_ends_with_ret)
217   (start_status: Status) (final_status: Status)
218     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
219       on the_trace: nat ≝
220  match the_trace with
221  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
222  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
223  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
224     _ _ _ call_trace final_trace ⇒
225      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
226      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
227      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
228        call_trace_cost + current_instruction_cost + final_trace_cost
229  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
230      let current_instruction_cost ≝ current_instruction_cost status_pre in
231      let tail_trace_cost ≝
232       compute_max_trace_any_label_cost cost_labels end_flag
233        status_init status_end tail_trace
234      in
235        current_instruction_cost + tail_trace_cost
236  ]
237and compute_max_trace_label_return_cost
238  (cost_labels: BitVectorTrie Byte 16)
239  (start_status: Status) (final_status: Status)
240    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
241      on the_trace: nat ≝
242  match the_trace with
243  [ tlr_base before after trace_to_lift ⇒ compute_max_trace_label_label_cost … trace_to_lift
244  | tlr_step initial labelled final labelled_trace ret_trace ⇒
245      let labelled_cost ≝ compute_max_trace_label_label_cost … labelled_trace in
246      let return_cost ≝ compute_max_trace_label_return_cost … ret_trace in
247        labelled_cost + return_cost
248  ].
249
250(*Useless now?
251(* To be moved *)
252lemma pred_minus_1:
253  ∀m, n: nat.
254  ∀proof: n < m.
255    pred (m - n) = m - n - 1.
256  #m #n
257  cases m
258  [ #proof
259    cases(lt_to_not_zero … proof)
260  | #m' #proof
261    normalize in ⊢ (???%);
262    cases n
263    [ normalize //
264    | #n' normalize
265      cases(m' - n')
266      [ %
267      | #Sm_n'
268        normalize //
269      ]
270    ]
271  ]
272qed.
273
274lemma succ_m_plus_one:
275  ∀m: nat.
276    S m = m + 1.
277 //
278qed.*)
279
280include alias "arithmetics/nat.ma".
281
282(*Useless now?
283lemma minus_m_n_minus_minus_plus_1:
284  ∀m, n: nat.
285  ∀proof: n < m.
286    m - n = (m - n - 1) + 1.
287 /3 by lt_plus_to_minus_r, plus_minus/
288qed.
289
290lemma plus_minus_rearrangement_1:
291  ∀m, n, o: nat.
292  ∀proof_n_m: n ≤ m.
293  ∀proof_m_o: m ≤ o.
294    (m - n) + (o - m) = o - n.
295  #m #n #o #H1 #H2
296  lapply (minus_to_plus … H1 (refl …)) #K1 >K1
297  lapply (minus_to_plus … H2 (refl …)) #K2 >K2
298  /2 by plus_minus/
299qed.
300
301lemma plus_minus_rearrangement_2:
302  ∀m, n, o: nat. n ≤ m → o ≤ n →
303    (m - n) + (n - o) = m - o.
304 /2 by plus_minus_rearrangement_1/
305qed.*)
306
307let rec compute_max_trace_label_label_cost_is_ok
308  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
309    (start_status: Status) (final_status: Status)
310      (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
311      on the_trace:
312        compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
313          (clock … final_status) - (clock … start_status) ≝ ?
314and compute_max_trace_label_label_pre_cost_is_ok
315  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
316    (start_status: Status) (final_status: Status)
317      (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
318        on the_trace:
319          compute_max_trace_label_label_pre_cost cost_labels trace_ends_flag start_status final_status the_trace =
320            (clock … final_status) - (clock … start_status) ≝ ?
321and compute_max_trace_label_return_cost_is_ok
322  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
323    (the_trace: trace_label_return cost_labels start_status final_status)
324      on the_trace:
325        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
326          (clock … final_status) - (clock … start_status) ≝ ?.
327  [1:
328    cases the_trace
329    #ends_flag #start_status #end_status #label_label_pre_trace
330    #labelled_proof
331    normalize
332    @compute_max_trace_label_label_pre_cost_is_ok
333  |3:
334    cases the_trace
335    [1:
336      #status_before #status_after #trace_to_lift
337      @compute_max_trace_label_label_cost_is_ok
338    |2:
339      #status_initial #status_labelled #status_final #labelled_trace #return_trace
340      >compute_max_trace_label_return_cost_is_ok %
341    ]
342  |2: cases the_trace
343    [1: #the_status #not_return #not_jump #not_cost
344        change in ⊢ (??%?) with (current_instruction_cost the_status);
345        @current_instruction_cost_is_ok
346    |2: #the_status #is_return
347        change in ⊢ (??%?) with (current_instruction_cost the_status);
348        @current_instruction_cost_is_ok
349    |3: #the_status #is_jump #is_cost
350        change in ⊢ (??%?) with (current_instruction_cost the_status);
351        @current_instruction_cost_is_ok
352    |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
353        #next_instruction_coherence #call_trace #final_trace
354        change in ⊢ (??%?) with (
355          let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
356          let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
357          let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
358            call_trace_cost + current_instruction_cost + final_trace_cost)
359        normalize nodelta;
360        >current_instruction_cost_is_ok
361        >compute_max_trace_label_return_cost_is_ok
362        >compute_max_trace_label_label_pre_cost_is_ok
363        generalize in match next_instruction_coherence;
364        change in ⊢ (% → ?) with (
365          let size ≝ current_instruction_cost pre_fun_call in
366          let pc_before ≝ program_counter … pre_fun_call in
367          let pc_after ≝ program_counter … after_fun_call in
368          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
369            sum = pc_after)
370        normalize nodelta; #relation_pre_after_fun_call
371        >plus_minus_rearrangement_2 in match (
372          (clock (BitVectorTrie Byte 16) after_fun_call
373            -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
374          +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
375            -clock (BitVectorTrie Byte 16) pre_fun_call)));
376        >(plus_minus_rearrangement
377          (clock (BitVectorTrie Byte 16) after_fun_call)
378          (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
379          (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
380    |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
381        #is_not_jump #is_not_ret #is_not_labelled
382        change in ⊢ (??%?) with (
383          let current_instruction_cost ≝ current_instruction_cost status_pre in
384          let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
385            current_instruction_cost + tail_trace_cost)
386        normalize nodelta;
387        >compute_max_trace_label_label_pre_cost_is_ok
388        >current_instruction_cost_is_ok
389    ]
390  ]
391qed.
392       
393let rec compute_max_trace_label_ret_cost_is_ok
394  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
395    (the_trace: trace_label_return cost_labels start_status final_status)
396      on the_trace:
397        compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
398        (clock … final_status) - (clock … start_status) ≝
399  match the_trace with
400  [ tlr_base before after trace_to_lift ⇒ ?
401  | tlr_step initial pre_fun_call pre_fun_call_trace start_fun_call end_fun_call
402      fun_call_trace pre_start_fun_call_coherence ⇒ ?
403  ]
404and compute_max_trace_label_label_pre_cost_is_ok
405  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
406    (start_status: Status) (final_status: Status)
407      (the_trace: trace_label_label_pre cost_labels ends_flag start_status final_status)
408        on the_trace:
409          compute_max_trace_label_label_pre_cost cost_labels ends_flag start_status final_status the_trace =
410            (clock … final_status) - (clock … start_status) ≝
411  match the_trace with
412  [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ ?
413  | tllp_base_return the_status is_return ⇒ ?
414  | tllp_base_jump the_status cost_label is_jump is_cost ⇒ ?
415  | tllp_step_call end_flag pre_fun_call start_fun_call end_fun_call after_fun_call final
416      fun_call_trace is_call statuses_related pre_start_fun_call_coherence
417      end_after_fun_call_coherence after_fun_call_trace ⇒ ?
418  | tllp_step_default end_flag start initial end initial_end_trace not_call
419      not_jump not_return not_cost ⇒ ?
420  ]
421and compute_max_trace_label_label_cost_is_ok
422  (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
423    (start_status: Status) (final_status: Status)
424      (the_trace: trace_label_label cost_labels ends_flag start_status final_status)
425        on the_trace:
426          compute_max_trace_label_label_cost cost_labels ends_flag start_status final_status the_trace =
427            (clock … final_status) - (clock … start_status) ≝
428  match the_trace with
429  [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
430  ].
431  [8: @(compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag initial final given_trace)
432  |1: @(compute_max_trace_label_label_cost_is_ok cost_labels ends_with_ret before after trace_to_lift)
433  |4: normalize
434      @minus_n_n
435  |3: normalize
436      @minus_n_n
437  |5: normalize
438      @minus_n_n
439  |6: letin fun_call_cost_ok ≝ (compute_max_trace_label_ret_cost_is_ok cost_labels start_fun_call end_fun_call fun_call_trace)
440      letin the_trace_cost_ok ≝ (compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag start_status final_status the_trace)
441  |*:
442  ]
443qed.
444 
445lemma compute_max_trace_label_ret_cost_is_ok:
446  ∀cost_labels: BitVectorTrie Byte 16.
447  ∀start_status: Status.
448  ∀final_status: Status.
449  ∀the_trace: trace_label_return cost_labels start_status final_status.
450    compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
451      (clock … final_status) - (clock … start_status).
452  #COST_LABELS #START_STATUS #FINAL_STATUS #THE_TRACE
453  elim THE_TRACE
454
455lemma trace_lab_rec_cost_ok:
456 ∀p: trace_lab_rec.
457  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
458
459let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
460 match p with
461 [ call ⇒ DO NOT ADD ANYTHING
462 | _ ⇒ DO ADD ].
463
464let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
465 | (call b bf tr af tl) as self ⇒
466    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
467    trace_lab_rec_cost' tl
468
469theorem main_lemma:
470 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
471
472axiom lemma1:
473 ∀p: simple_path.
474  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
475
476axiom lemma2:
477 ∀s,l,cost_map.
478  is_labelled l s →
479   traverse_cost_internal s = cost_map l.
480
481axiom main_statement:
482 ∀s.
483 ∀cost_map.
484 let p ≝ compute_simple_path0 s in
485 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
486
487axiom main_statement:
488 ∀s.
489 ∀cost_map.
490 let p ≝ compute_simple_path0 s in
491  execute' (path_length p) s = 〈s',τ〉 →
492   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.