source: src/ASM/CostsProof.ma @ 1549

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

removed cruft from costsproof.ma file so claudio can work in parallel

File size: 17.8 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4include "common/StructuredTraces.ma".
5
6definition current_instruction ≝
7  λs: Status.
8  let pc ≝ program_counter … s in
9  \fst (\fst (fetch … (code_memory … s) pc)).
10
11definition ASM_classify: Status → status_class ≝
12 λs.
13  match current_instruction s with
14   [ RealInstruction pre ⇒
15     match pre with
16      [ RET ⇒ cl_return
17      | JZ _ ⇒ cl_jump
18      | JNZ _ ⇒ cl_jump
19      | JC _ ⇒ cl_jump
20      | JNC _ ⇒ cl_jump
21      | JB _ _ ⇒ cl_jump
22      | JNB _ _ ⇒ cl_jump
23      | JBC _ _ ⇒ cl_jump
24      | CJNE _ _ ⇒ cl_jump
25      | DJNZ _ _ ⇒ cl_jump
26      | _ ⇒ cl_other
27      ]
28   | ACALL _ ⇒ cl_call
29   | LCALL _ ⇒ cl_call
30   | JMP _ ⇒ cl_call
31   | AJMP _ ⇒ cl_jump
32   | LJMP _ ⇒ cl_jump
33   | SJMP _ ⇒ cl_jump
34   | _ ⇒ cl_other
35   ].
36
37definition current_instruction_is_labelled ≝
38  λcost_labels: BitVectorTrie 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)
309   (trace_ends_flag: trace_ends_with_ret)
310    (start_status: Status) (final_status: Status)
311      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
312        start_status final_status) on the_trace:
313          compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
314            (clock … final_status) - (clock … start_status) ≝ ?
315and compute_max_trace_any_label_cost_is_ok
316  (cost_labels: BitVectorTrie Byte 16)
317  (trace_ends_flag: trace_ends_with_ret)
318   (start_status: Status) (final_status: Status)
319     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
320       on the_trace:
321         compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
322           (clock … final_status) - (clock … start_status) ≝ ?
323and compute_max_trace_label_return_cost_is_ok
324  (cost_labels: BitVectorTrie Byte 16)
325  (start_status: Status) (final_status: Status)
326    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
327      on the_trace:
328        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
329          (clock … final_status) - (clock … start_status) ≝ ?.
330  [1:
331    cases the_trace
332    #ends_flag #start_status #end_status #any_label_trace #is_costed
333    normalize @compute_max_trace_any_label_cost_is_ok
334  |2:
335  |3:
336    cases the_trace
337    [1:
338      #status_before #status_after #trace_to_lift
339      normalize @compute_max_trace_label_label_cost_is_ok
340    |2:
341      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
342      normalize >compute_max_trace_label_label_cost_is_ok
343      >compute_max_trace_label_return_cost_is_ok
344    ]
345  ].
346
347(*
348let rec compute_max_trace_label_label_cost_is_ok
349  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
350    (start_status: Status) (final_status: Status)
351      (the_trace: trace_label_label cost_labels trace_ends_flag start_status final_status)
352      on the_trace:
353        compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
354          (clock … final_status) - (clock … start_status) ≝ ?
355and compute_max_trace_any_label_pre_cost_is_ok
356  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
357    (start_status: Status) (final_status: Status)
358      (the_trace: trace_any_label cost_labels trace_ends_flag start_status final_status)
359        on the_trace:
360          compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
361            (clock … final_status) - (clock … start_status) ≝ ?
362and compute_max_trace_label_return_cost_is_ok
363  (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
364    (the_trace: trace_label_return cost_labels start_status final_status)
365      on the_trace:
366        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
367          (clock … final_status) - (clock … start_status) ≝ ?.
368  [1:
369    cases the_trace
370    #ends_flag #start_status #end_status #label_label_pre_trace
371    #labelled_proof
372    normalize
373    @compute_max_trace_label_label_pre_cost_is_ok
374  |3:
375    cases the_trace
376    [1:
377      #status_before #status_after #trace_to_lift
378      @compute_max_trace_label_label_cost_is_ok
379    |2:
380      #status_initial #status_labelled #status_final #labelled_trace #return_trace
381      >compute_max_trace_label_return_cost_is_ok %
382    ]
383  |2: cases the_trace
384    [1: #the_status #not_return #not_jump #not_cost
385        change in ⊢ (??%?) with (current_instruction_cost the_status);
386        @current_instruction_cost_is_ok
387    |2: #the_status #is_return
388        change in ⊢ (??%?) with (current_instruction_cost the_status);
389        @current_instruction_cost_is_ok
390    |3: #the_status #is_jump #is_cost
391        change in ⊢ (??%?) with (current_instruction_cost the_status);
392        @current_instruction_cost_is_ok
393    |4: #end_flag #pre_fun_call #after_fun_call #final #is_call
394        #next_instruction_coherence #call_trace #final_trace
395        change in ⊢ (??%?) with (
396          let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
397          let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels … call_trace in
398          let final_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag after_fun_call final final_trace in
399            call_trace_cost + current_instruction_cost + final_trace_cost)
400        normalize nodelta;
401        >current_instruction_cost_is_ok
402        >compute_max_trace_label_return_cost_is_ok
403        >compute_max_trace_label_label_pre_cost_is_ok
404        generalize in match next_instruction_coherence;
405        change in ⊢ (% → ?) with (
406          let size ≝ current_instruction_cost pre_fun_call in
407          let pc_before ≝ program_counter … pre_fun_call in
408          let pc_after ≝ program_counter … after_fun_call in
409          let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
410            sum = pc_after)
411        normalize nodelta; #relation_pre_after_fun_call
412        >plus_minus_rearrangement_2 in match (
413          (clock (BitVectorTrie Byte 16) after_fun_call
414            -clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
415          +(clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call)
416            -clock (BitVectorTrie Byte 16) pre_fun_call)));
417        >(plus_minus_rearrangement
418          (clock (BitVectorTrie Byte 16) after_fun_call)
419          (clock (BitVectorTrie Byte 16) (execute 1 pre_fun_call))
420          (clock (BitVectorTrie Byte 16) pre_fun_call) ? ?) in ⊢ (??%?);
421    |5: #end_flag #status_pre #status_end #tail_trace #is_not_call
422        #is_not_jump #is_not_ret #is_not_labelled
423        change in ⊢ (??%?) with (
424          let current_instruction_cost ≝ current_instruction_cost status_pre in
425          let tail_trace_cost ≝ compute_max_trace_label_label_pre_cost cost_labels end_flag (execute 1 status_pre) status_end tail_trace in
426            current_instruction_cost + tail_trace_cost)
427        normalize nodelta;
428        >compute_max_trace_label_label_pre_cost_is_ok
429        >current_instruction_cost_is_ok
430    ]
431  ]
432qed. *)
433
434(* XXX: work below here: *)
435
436let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
437 match p with
438 [ call ⇒ DO NOT ADD ANYTHING
439 | _ ⇒ DO ADD ].
440
441let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
442 | (call b bf tr af tl) as self ⇒
443    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
444    trace_lab_rec_cost' tl
445
446theorem main_lemma:
447 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
448
449axiom lemma1:
450 ∀p: simple_path.
451  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
452
453axiom lemma2:
454 ∀s,l,cost_map.
455  is_labelled l s →
456   traverse_cost_internal s = cost_map l.
457
458axiom main_statement:
459 ∀s.
460 ∀cost_map.
461 let p ≝ compute_simple_path0 s in
462 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
463
464axiom main_statement:
465 ∀s.
466 ∀cost_map.
467 let p ≝ compute_simple_path0 s in
468  execute' (path_length p) s = 〈s',τ〉 →
469   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.