source: src/ASM/CostsProof.ma @ 1506

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

changes to costs proof over weekend

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