source: src/ASM/CostsProof.ma @ 1509

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

i hate subtraction over the nats

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