source: src/ASM/ASMCosts.ma @ 2993

Last change on this file since 2993 was 2993, checked in by sacerdot, 7 years ago
  1. performance improved: the type inference was inferring load_code_memory ... in computational positions, duplicating the work at every step of execution of the assembly code. We now force the use of the let-in-ed variable
  2. new extraction after 1)
  3. driver/printer.ml repaired
  4. the output of the intermediate passes is now printed on file
File size: 37.3 KB
Line 
1include "ASM/Interpret.ma".
2
3definition ASMRegisterRets: list [[ acc_a; direct; registr ]] ≝
4 [ DIRECT (bitvector_of_nat 8 82);       (* DPL *)
5   DIRECT (bitvector_of_nat 8 83);       (* DPH *)
6   REGISTER [[ false; false; false ]];   (* Register00 *)
7   REGISTER [[ false; false; true ]] ].  (* Register01 *)
8% qed.
9
10definition as_result_of_finaladdr: ∀T:Type[0]. ∀cm:T. PreStatus … cm → Word → option int ≝
11 λT,cm,st,finaladdr.
12  if eq_bv ? (program_counter ?? st) finaladdr then
13   let vals ≝
14    map [[acc_a;direct;registr]] ? (get_arg_8 ?? st false) (ASMRegisterRets⌈list ? ↦ ?⌉) in
15   let dummy ≝ zero ? in
16   let first_byte ≝ λl. match l with [ nil ⇒ 〈dummy,[]〉 | cons hd tl ⇒ 〈hd,tl〉] in
17   let 〈b1,tl1〉 ≝ first_byte vals in
18   let 〈b2,tl2〉 ≝ first_byte tl1 in
19   let 〈b3,tl3〉 ≝ first_byte tl2 in
20   let 〈b4,tl4〉 ≝ first_byte tl3 in
21    Some ? (b4 @@ b3 @@ b2 @@ b1)
22  else
23   None ?.
24[ @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % | % ]
25qed.
26
27definition OC_as_call_ident:
28 ∀prog:labelled_object_code.∀cm. (Σs:Status cm. OC_classify … s = cl_call) → ident
29
30 λprog,cm,s0.
31  let pc ≝ program_counter ?? (execute_1' cm s0) in
32  match lookup_opt ?? pc (symboltable prog) with
33  [ None ⇒ ⊥ | Some id ⇒ id ].
34cases daemon (*CSC: we need a specification of the symboltable for this *)
35qed.
36
37definition OC_abstract_status: labelled_object_code → abstract_status ≝
38 λprog.
39  let code_memory ≝ load_code_memory (oc prog) in
40    mk_abstract_status
41      (Status code_memory)
42      (λs1,s2. execute_1 … s1 = s2)
43      word_deqset
44      (program_counter … code_memory)
45      (OC_classify code_memory)
46      (λpc.lookup_opt … pc (costlabels prog))
47      (next_instruction_properly_relates_program_counters code_memory)
48      (λst. as_result_of_finaladdr … code_memory … st (final_pc prog))
49      (OC_as_call_ident prog code_memory)
50      ?.
51 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
52 try (#x #y #abs) try (#x #abs) try #abs destruct
53qed.
54
55definition trace_any_label_length ≝
56  λprog: labelled_object_code.
57  let code_memory ≝ load_code_memory (oc prog) in
58  λtrace_ends_flag: trace_ends_with_ret.
59  λstart_status: Status code_memory.
60  λfinal_status: Status code_memory.
61  λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
62    as_trace_any_label_length' … the_trace.
63
64let rec all_program_counter_list
65  (n: nat)
66    on n ≝
67  match n with
68  [ O ⇒ [ ]
69  | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n')
70  ].
71
72lemma all_program_counter_list_bound_eq:
73  ∀bound: nat.
74    |all_program_counter_list bound| = bound.
75  #bound elim bound try %
76  #bound' #inductive_hypothesis normalize
77  >inductive_hypothesis %
78qed.
79
80lemma mem_all_program_counter_list_lt_bound:
81  ∀bound: nat.
82  ∀bound_proof: bound ≤ 2^16.
83  ∀e: Word.
84    memb word_deqset e (all_program_counter_list bound) = true →
85      nat_of_bitvector … e < bound.
86  #bound elim bound
87  [1:
88    #bound_proof #e
89    normalize #absurd destruct(absurd)
90  |2:
91    #bound' #inductive_hypothesis
92    #bound_proof #e
93    change with (if eq_bv ??? then ? else ? = ? → ?)
94    @eq_bv_elim
95    [1:
96      #eq_assm
97      normalize nodelta destruct #_
98      >nat_of_bitvector_bitvector_of_nat_inverse try assumption
99      normalize %
100    |2:
101      #neq_assm normalize nodelta
102      #memb_assm %2 @inductive_hypothesis
103      try assumption
104      @(transitive_le bound' (S bound'))
105      try assumption %2 %
106    ]
107  ]
108qed.
109
110lemma lt_bound_mem_all_program_counter_list:
111  ∀bound: nat.
112  ∀bound_proof: bound ≤ 2^16.
113  ∀e: Word.
114    nat_of_bitvector … e < bound →
115      memb word_deqset e (all_program_counter_list bound) = true.
116  #bound elim bound
117  [1:
118    #bound_proof #e normalize
119    #absurd cases (lt_to_not_zero … absurd)
120  |2:
121    #bound' #inductive_hypothesis
122    #bound_proof #e
123    change with (? → if eq_bv ??? then ? else ? = ?)
124    #assm
125    cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
126    [1:
127      #e_lt_assm
128      @eq_bv_elim
129      [1:
130        #eq_assm normalize nodelta %
131      |2:
132        #neq_assm normalize nodelta
133        @inductive_hypothesis try assumption
134        @(transitive_le bound' (S bound')) try assumption
135        %2 %
136      ]
137    |2:
138      #relevant >eq_eq_bv normalize nodelta try %
139      destruct >bitvector_of_nat_inverse_nat_of_bitvector %
140    |3:
141      normalize in assm;
142      @le_S_S_to_le assumption
143    ]
144  ]
145qed.
146
147include alias "arithmetics/nat.ma".
148
149lemma execute_1_and_program_counter_after_other_in_lockstep00:
150  ∀code_memory: BitVectorTrie Byte 16.
151  ∀start_status: Status code_memory.
152      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
153    ASM_classify0 instruction = cl_other →
154        program_counter ? ? (execute_1 … start_status) =
155          program_counter_after_other pc instruction.
156  #code_memory #start_status
157  whd in match execute_1; normalize nodelta 
158  cases (execute_1' code_memory start_status) #the_status; * #_
159  cases (fetch ? ?); * #instruction #pc #ticks
160  #classify_assm #classify_assm0 @classify_assm assumption
161qed.
162
163lemma execute_1_and_program_counter_after_other_in_lockstep0:
164  ∀code_memory: BitVectorTrie Byte 16.
165  ∀start_status: Status code_memory.
166    OC_classify … start_status = cl_other →
167      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
168        program_counter ? ? (execute_1 … start_status) =
169          program_counter_after_other pc instruction.
170  #code_memory #start_status #classify_assm
171  whd in match execute_1; normalize nodelta
172  cases (execute_1' code_memory start_status) #the_status
173  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
174  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
175  #classify_assm #classify_assm' @classify_assm' assumption
176qed.
177
178lemma execute_1_and_program_counter_after_other_in_lockstep:
179  ∀prog: labelled_object_code.
180  let code_memory ≝ load_code_memory (oc prog) in
181  ∀start_status: Status code_memory.
182    as_classifier (OC_abstract_status prog) start_status cl_other →
183      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
184        program_counter ? ? (execute_1 … start_status) =
185          program_counter_after_other pc instruction.
186  #prog #start_status #classify_assm
187  change with (ASM_classify0 ? = ?) in classify_assm;
188  destruct (classify_assm)
189  @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
190qed. 
191
192lemma sublist_tal_pc_list_all_program_counter_list:
193  ∀prog: labelled_object_code.
194  let code_memory ≝ load_code_memory (oc prog) in
195  ∀start, final: Status code_memory.
196  ∀trace_ends_flag.
197  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
198    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
199  #prog #start #final #trace_ends_flag #the_trace
200  whd in match (sublist ???); #pc #memb_assm
201  @lt_bound_mem_all_program_counter_list try %
202  @nat_of_bitvector_lt_bound
203qed.
204
205corollary tal_pc_list_length_leq_total_program_size:
206  ∀prog: labelled_object_code.
207  let code_memory ≝ load_code_memory (oc prog) in
208  ∀start, final: Status code_memory.
209  ∀trace_ends_flag.
210  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
211  ∀unrepeating_witness: tal_unrepeating … the_trace.
212    |tal_pc_list … the_trace| ≤ 2^16.
213  #prog #start #final #trace_ends_flag #the_trace #unrepeating_witness
214  <(all_program_counter_list_bound_eq (2^16))
215  @sublist_length
216  [1:
217    @tal_unrepeating_uniqueb
218    assumption
219  |2:
220    @sublist_tal_pc_list_all_program_counter_list
221    assumption
222  ]
223qed.
224
225let rec compute_paid_trace_any_label
226  (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
227   (start_status: Status (load_code_memory (oc prog)))
228   (final_status: Status (load_code_memory (oc prog)))
229        (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
230       on the_trace: nat ≝
231  match the_trace with
232  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
233  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
234  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ _ ⇒ current_instruction_cost … pre_fun_call
235  | tal_base_tailcall pre_fun_call start_fun_call final _ _ _ ⇒ current_instruction_cost … pre_fun_call
236  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
237     _ _ _ call_trace _ final_trace ⇒
238      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
239      let final_trace_cost ≝ compute_paid_trace_any_label prog end_flag … final_trace in
240        current_instruction_cost + final_trace_cost
241  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
242      let current_instruction_cost ≝ current_instruction_cost … status_pre in
243      let tail_trace_cost ≝
244       compute_paid_trace_any_label prog end_flag
245        status_init status_end tail_trace
246      in
247        current_instruction_cost + tail_trace_cost
248  ].
249
250definition compute_paid_trace_label_label ≝
251  λprog: labelled_object_code.
252  let code_memory ≝ load_code_memory (oc prog) in
253  λtrace_ends_flag: trace_ends_with_ret.
254  λstart_status: Status code_memory.
255  λfinal_status: Status code_memory.
256  λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
257  match the_trace with
258  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
259      compute_paid_trace_any_label … given_trace
260  ].
261
262lemma trace_compute_paid_trace_cl_other:
263  ∀prog : labelled_object_code.
264  let code_memory' ≝ load_code_memory (oc prog) in
265  ∀program_counter' : Word.
266  ∀program_size' : ℕ.
267  ∀ticks : ℕ.
268  ∀instruction : instruction.
269  ∀program_counter'' : Word.
270  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
271  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
272  ∀start_status : (Status code_memory').
273  ∀final_status : (Status code_memory').
274  ∀trace_ends_flag : trace_ends_with_ret.
275  ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
276  ∀program_counter_refl : (program_counter' = program_counter … start_status).
277  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
278  ∀classify_assm: ASM_classify0 instruction = cl_other.
279  ∀pi1 : ℕ.
280   (if match lookup_opt costlabel 16 program_counter''' (costlabels prog) with 
281         [None ⇒ true
282         |Some _ ⇒ false
283         ] 
284    then
285      ∀start_status0:Status code_memory'.
286      ∀final_status0:Status code_memory'.
287      ∀trace_ends_flag0:trace_ends_with_ret.
288      ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
289        trace_any_label_length … the_trace0 ≤ program_size' →
290        program_counter''' = program_counter … start_status0 →
291                  pi1
292                    =compute_paid_trace_any_label … the_trace0
293    else (pi1=O) )
294   → ticks+pi1
295     =compute_paid_trace_any_label … the_trace.
296  #prog #program_counter' #program_size' #ticks #instruction
297  #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
298  #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
299  #recursive_assm
300  @(trace_any_label_inv_ind … the_trace)
301    [2:
302      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
303      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
304    |3:
305      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
306      #classifier_assm #after_return_assm #trace_label_return #costed_assm
307      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
308      destruct @⊥
309    |4:
310      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
311      #classifier_assm #trace_label_return
312      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
313      destruct @⊥
314    |5:
315      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
316      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
317      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
318      #final_status_refl #the_trace_refl destruct @⊥
319    |6:
320      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
321      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
322      #the_trace_refl
323      destruct
324      whd in match (trace_any_label_length … (tal_step_default …));
325      whd in match (compute_paid_trace_any_label … (tal_step_default …));
326      whd in costed_assm:(?%);
327      generalize in match costed_assm;
328      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog)));
329      whd in match (as_label ??);
330      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog))
331        in ⊢ (??%? → % → ?);
332      #lookup_assm cases lookup_assm
333      [1:
334        #None_lookup_opt_assm normalize nodelta #_
335        generalize in match recursive_assm;
336        lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
337        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
338        #None_lookup_opt_assm <None_lookup_opt_assm
339        normalize nodelta #new_recursive_assm
340        cases(new_recursive_assm (execute_1 ? status_pre) status_end
341          end_flag trace_any_label ? ?) try (>rewrite_assm %)
342        whd in match (current_instruction_cost … status_pre);
343        cut(ticks = \snd (fetch (load_code_memory (oc prog))
344           (program_counter … status_pre)))
345        [1,3:
346          <FETCH %
347        |2:
348          #ticks_refl_assm
349          >ticks_refl_assm %
350        |4:
351          #ticks_refl_assm
352          change with (S ? ≤ S ?) in size_invariant;
353          lapply (le_S_S_to_le … size_invariant) #assm
354          assumption
355        ]
356      |2:
357        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
358        #absurd
359        cases (not_Some_neq_None_to_False ?? absurd)
360      ]
361    |1:
362      #status_start #status_final #execute_assm #classifier_assm #costed_assm
363      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
364      destruct
365      whd in match (trace_any_label_length … (tal_base_not_return …));
366      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
367      whd in costed_assm;
368      generalize in match costed_assm;
369      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) ?));
370      whd in match (as_label ??);
371      generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) (costlabels prog))
372        in ⊢ (??%? → % → ?);
373      #lookup_assm cases lookup_assm
374      [1:
375        #None_lookup_opt_assm
376        #absurd @⊥ cases absurd -absurd #absurd @absurd %
377      |2:
378        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
379        generalize in match recursive_assm;
380        cases classifier_assm -classifier_assm #classifier_assm
381        [2:
382          lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
383          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
384          #Some_lookup_opt_assm <Some_lookup_opt_assm
385          normalize nodelta #new_recursive_assm >new_recursive_assm
386          cut(ticks = \snd (fetch (load_code_memory (oc prog))
387             (program_counter … status_start)))
388          [1:
389            <FETCH %
390          |2:
391            #ticks_refl_assm >ticks_refl_assm
392            <plus_n_O %
393          ]
394        |1:
395                (* JHM: wicked failure because Some prevent previous unfolding of OC_classify here *)
396                @⊥
397                (* *** (* previously: unnecessary case analysis on instruction *)
398          change with ((Some ? (ASM_classify0 ?) = ?) → ?);
399          whd in match (current_instruction code_memory' status_start);
400          <FETCH generalize in match classify_assm;
401          cases instruction
402          [8:
403            #preinstruction normalize nodelta
404            whd in match ASM_classify0; normalize nodelta
405            #contradiction >contradiction #absurd destruct(absurd)
406          ]
407          try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
408          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
409          normalize in ignore; destruct(ignore)
410                *** *)
411        ]
412      ]
413    ]
414  change with (ASM_classify0 ? = ?) in classifier_assm;
415  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
416  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
417  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
418qed.
419
420lemma trace_compute_paid_trace_cl_jump:
421  ∀prog: labelled_object_code.
422  let code_memory' ≝ load_code_memory (oc prog) in
423  ∀program_counter': Word.
424  ∀first_time_around: bool.
425  ∀program_size': ℕ.
426  ∀ticks: ℕ.
427  ∀instruction: instruction.
428  ∀program_counter'': Word.
429  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
430  ∀start_status: (Status code_memory').
431  ∀final_status: (Status code_memory').
432  ∀trace_ends_flag: trace_ends_with_ret.
433  ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
434  ∀program_counter_refl: (program_counter' = program_counter … start_status).
435  ∀classify_assm: ASM_classify0 instruction = cl_jump.
436    ticks
437     =compute_paid_trace_any_label … the_trace.
438  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #first_time_around
439  #program_size' #ticks #instruction #program_counter'' #FETCH
440  #start_status #final_status
441  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
442  @(trace_any_label_inv_ind … the_trace)
443  [6:
444    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
445    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
446    #the_trace_refl destruct @⊥
447  |1:
448    #status_start #status_final #execute_assm #classifier_assm #costed_assm
449    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
450    destruct
451    whd in match (trace_any_label_length … (tal_base_not_return …));
452    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
453    <FETCH %
454  |2:
455    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
456    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
457  |3:
458    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
459    #classifier_assm #after_return_assm #trace_label_return #costed_assm
460    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
461    destruct @⊥
462  |4:
463    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
464    #classifier_assm #trace_label_return
465    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
466    destruct @⊥
467  |5:
468    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
469    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
470    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
471    #final_status_refl #the_trace_refl destruct @⊥
472  ]
473  change with (ASM_classify0 ? = ?) in classifier_assm;
474  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
475  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
476  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
477qed.
478
479lemma trace_compute_paid_trace_cl_call:
480  ∀prog: labelled_object_code.
481  let code_memory' ≝ load_code_memory (oc prog) in
482  ∀program_counter' : Word.
483  ∀program_size' : ℕ.
484  ∀ticks : ℕ.
485  ∀instruction : instruction.
486  ∀program_counter'' : Word.
487  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
488  ∀start_status : (Status code_memory').
489  ∀final_status : (Status code_memory').
490  ∀trace_ends_flag : trace_ends_with_ret.
491  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
492  ∀program_counter_refl : (program_counter' = program_counter … start_status).
493  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
494  ∀classify_assm: ASM_classify0 instruction = cl_call.
495  (∀pi1:ℕ
496  .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
497      [None ⇒ true | Some _ ⇒ false] 
498   then (∀start_status0:Status code_memory'
499             .∀final_status0:Status code_memory'
500              .∀trace_ends_flag0:trace_ends_with_ret
501               .∀the_trace0:trace_any_label
502                                        (OC_abstract_status prog)
503                                        trace_ends_flag0 start_status0 final_status0.
504                trace_any_label_length … the_trace0
505                   ≤ program_size' →
506                program_counter''
507                 =program_counter … start_status0
508                 → pi1
509                   =compute_paid_trace_any_label … the_trace0) 
510   else (pi1=O) 
511   → ticks+pi1
512     =compute_paid_trace_any_label … the_trace).
513  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
514  #ticks #instruction #program_counter'' #FETCH
515  #start_status #final_status #trace_ends_flag
516  #the_trace #program_counter_refl #size_invariant #classify_assm
517  #recursive_block_cost #recursive_assm
518  @(trace_any_label_inv_ind … the_trace)
519  [6:
520    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
521    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
522    #the_trace_refl destruct @⊥
523  |1:
524    #status_start #status_final #execute_assm #classifier_assm #costed_assm
525    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
526    destruct @⊥
527  |2:
528    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
529    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
530  |3:
531    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
532    #classifier_assm #after_return_assm #trace_label_return #costed_assm
533    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
534    destruct
535    whd in match (trace_any_label_length … (tal_base_call …));
536    whd in match (compute_paid_trace_any_label … (tal_base_call …));
537    whd in costed_assm;
538    generalize in match costed_assm;
539    generalize in match (refl … (lookup_opt … (program_counter … status_final) (costlabels prog)));
540    whd in match (as_label ??);
541    generalize in match (lookup_opt … (program_counter … status_final) ?)
542      in ⊢ (??%? → % → ?);
543    #lookup_assm cases lookup_assm
544    [1:
545      #None_lookup_opt normalize nodelta #absurd cases absurd
546      -absurd #absurd @⊥ @absurd %
547    |2:
548      #costlabel #Some_lookup_opt normalize nodelta #ignore
549      generalize in match recursive_assm;
550      cut(program_counter'' = (program_counter … status_final))
551      [1:
552        generalize in match after_return_assm;
553        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
554      |2:
555        #program_counter_assm >program_counter_assm <Some_lookup_opt
556        normalize nodelta #new_recursive_assm >new_recursive_assm
557        cut(ticks = \snd (fetch code_memory' (program_counter … status_pre_fun_call)))
558        [1:
559          <FETCH %
560        |2:
561          #ticks_refl_assm >ticks_refl_assm
562          <plus_n_O %
563        ]
564      ]
565    ]
566  |4:
567    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
568    #classifier_assm #trace_label_return
569    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
570    destruct @⊥
571  |5:
572    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
573    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
574    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
575    #final_status_refl #the_trace_refl
576    generalize in match execute_assm; destruct #execute_assm
577    whd in match (trace_any_label_length … (tal_step_call …));
578    whd in match (compute_paid_trace_any_label … (tal_step_call …));
579    whd in costed_assm:(?%);
580    generalize in match costed_assm;
581    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) (costlabels ?)));
582    whd in match (as_label ??);
583    generalize in match (lookup_opt … (program_counter … status_after_fun_call) (costlabels prog))
584      in ⊢ (??%? → % → ?);
585    #lookup_assm cases lookup_assm
586    [1:
587      #None_lookup_opt_assm normalize nodelta #ignore
588      generalize in match recursive_assm;
589      cut(program_counter'' = program_counter … status_after_fun_call)
590      [1:
591        generalize in match after_return_assm;
592        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
593      |2:
594        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
595        normalize nodelta #new_recursive_assm
596        cases (new_recursive_assm … trace_any_label ? ?)
597        [1:
598          @plus_right_monotone whd in ⊢ (???%); <FETCH %
599        |2:
600          @le_S_S_to_le @size_invariant
601        |3:
602          %
603        ]
604      ]
605    |2:
606      #cost_label #Some_lookup_opt_assm #absurd
607      cases (not_Some_neq_None_to_False ?? absurd)
608    ]
609  ]
610  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
611  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
612  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
613  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
614  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
615  #absurd destruct(absurd)
616qed.
617
618lemma trace_compute_paid_trace_cl_return:
619  ∀prog: labelled_object_code.
620  let code_memory' ≝ load_code_memory (oc prog) in
621  ∀program_counter' : Word.
622  ∀program_size' : ℕ.
623  ∀ticks : ℕ.
624  ∀instruction : instruction.
625  ∀program_counter'' : Word.
626  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
627  ∀start_status : (Status code_memory').
628  ∀final_status : (Status code_memory').
629  ∀trace_ends_flag : trace_ends_with_ret.
630  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
631  ∀program_counter_refl : (program_counter' = program_counter … start_status).
632  ∀classify_assm: ASM_classify0 instruction = cl_return.
633    ticks
634     =compute_paid_trace_any_label … the_trace.
635  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
636  #ticks #instruction #program_counter'' #FETCH
637  #start_status #final_status #trace_ends_flag
638  #the_trace #program_counter_refl #classify_assm
639  @(trace_any_label_inv_ind … the_trace)
640  [1:
641    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
642    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
643    destruct @⊥
644  |2:
645    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
646    #start_status_refl #final_status_refl #the_trace_refl destruct
647    whd in match (trace_any_label_length … (tal_base_return …));
648    whd in match (compute_paid_trace_any_label … (tal_base_return …));
649    <FETCH %
650  |3:
651    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
652    #classifier_assm #after_return_assm #trace_label_return #costed_assm
653    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
654    destruct @⊥
655  |4:
656    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
657    #classifier_assm
658    destruct @⊥
659    change with (ASM_classify0 ? = ?) in classifier_assm;
660    cases (current_instruction ??) in classifier_assm;
661    [7: #preinstruction cases preinstruction ]
662    try(#addr1 #addr2 #absurd normalize in absurd; destruct(absurd))
663    try(#addr #absurd normalize in absurd; destruct(absurd))
664    #absurd normalize in absurd; destruct(absurd)
665  |5:
666    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
667    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
668    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
669    #final_status_refl #the_trace_refl
670    destruct @⊥
671  |6:
672    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
673    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
674    #final_status_refl #the_trace_refl destruct @⊥
675  ]
676  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
677  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
678  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
679  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
680  <FETCH in classifier_assm; >classify_assm
681  #absurd try (destruct(absurd))
682  cases absurd
683  #absurd destruct(absurd)
684qed.
685
686lemma trace_any_label_length_leq_0_to_False:
687  ∀prog: labelled_object_code.
688  let code_memory ≝ load_code_memory (oc prog) in
689  ∀trace_ends_flag: trace_ends_with_ret.
690  ∀start_status: Status code_memory.
691  ∀final_status: Status code_memory.
692  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
693   trace_any_label_length … the_trace ≤ 0 → False.
694  #prog #trace_ends_flag #start_status #final_status #the_trace
695  cases the_trace /2 by absurd/
696qed.
697     
698let rec block_cost'
699 (prog: labelled_object_code) (program_counter': Word)
700    (program_size: nat)
701      (first_time_around: bool)
702        on program_size:
703          Σcost_of_block: nat.
704          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
705            ∀start_status,final_status: Status (load_code_memory (oc prog)).
706            ∀trace_ends_flag.
707            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
708              trace_any_label_length … the_trace ≤ program_size →
709              program_counter' = program_counter … start_status →
710                cost_of_block = compute_paid_trace_any_label … the_trace
711          else
712            (cost_of_block = 0) ≝
713  let code_memory' ≝ load_code_memory (oc prog) in
714  match program_size return λx. x = program_size → ? with
715  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
716  | S program_size' ⇒ λstep_case.
717    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (load_code_memory (oc prog)) program_counter' in
718    let to_continue ≝
719      match lookup_opt … program_counter' (costlabels prog) with
720      [ None ⇒ true
721      | Some _ ⇒ first_time_around
722      ]
723    in
724      ((if to_continue then
725       pi1 … (match instruction return λx. x = instruction → ? with
726        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
727          match real_instruction return λx. x = real_instruction →
728          Σcost_of_block: nat.
729            ∀start_status,final_status: Status code_memory'.
730            ∀trace_ends_flag.
731            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
732              trace_any_label_length … the_trace ≤ S program_size' →
733              program_counter' = program_counter … start_status →
734                cost_of_block = compute_paid_trace_any_label … the_trace with
735          [ RET                    ⇒ λinstr. ticks
736          | RETI                   ⇒ λinstr. ticks
737          | JC   relative          ⇒ λinstr. ticks
738          | JNC  relative          ⇒ λinstr. ticks
739          | JB   bit_addr relative ⇒ λinstr. ticks
740          | JNB  bit_addr relative ⇒ λinstr. ticks
741          | JBC  bit_addr relative ⇒ λinstr. ticks
742          | JZ   relative          ⇒ λinstr. ticks
743          | JNZ  relative          ⇒ λinstr. ticks
744          | CJNE src_trgt relative ⇒ λinstr. ticks
745          | DJNZ src_trgt relative ⇒ λinstr. ticks
746          | JMP   addr             ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
747              ticks + block_cost' prog program_counter'' program_size' false
748          | _                      ⇒ λinstr.
749              ticks + block_cost' prog program_counter'' program_size' false
750          ] (refl …)
751        | ACALL addr     ⇒ λinstr.
752            ticks + block_cost' prog program_counter'' program_size' false
753        | AJMP  addr     ⇒ λinstr.
754          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
755            ticks + block_cost' prog jump_target program_size' false
756        | LCALL addr     ⇒ λinstr.
757            ticks + block_cost' prog program_counter'' program_size' false
758        | LJMP  addr     ⇒ λinstr.
759          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
760            ticks + block_cost' prog jump_target program_size' false
761        | SJMP  addr     ⇒ λinstr.
762          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
763            ticks + block_cost' prog jump_target program_size' false
764        | MOVC  src trgt ⇒ λinstr.
765            ticks + block_cost' prog program_counter'' program_size' false
766        ] (refl …))
767      else
768        0)
769      : Σcost_of_block: nat.
770          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
771          [ true ⇒
772            ∀start_status: Status code_memory'.
773            ∀final_status: Status code_memory'.
774            ∀trace_ends_flag.
775            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
776              trace_any_label_length … the_trace ≤ S program_size' →
777              program_counter' = program_counter … start_status →
778                cost_of_block = compute_paid_trace_any_label … the_trace
779          | false ⇒
780            (cost_of_block = 0)
781          ])
782  ] (refl …).
783  [2:
784    change with (if to_continue then ? else (? = 0))
785    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
786    @pi2
787  |1:
788    destruct
789    cases (lookup_opt ????) normalize nodelta
790    [1:
791      #start_status #final_status #trace_ends_flag #the_trace
792      #absurd
793      cases (trace_any_label_length_leq_0_to_False … absurd)
794    |2:
795      #cost cases first_time_around normalize nodelta try %
796      #start_status #final_status #trace_ends_flag #the_trace #absurd
797      cases (trace_any_label_length_leq_0_to_False … absurd)
798    ]
799  |3:
800    change with (if to_continue then ? else (0 = 0))
801    >p normalize nodelta %
802  |6,7:
803    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
804    @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl)
805    destruct %
806  |4,46,47:
807    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
808    cases(block_cost' ???) -block_cost'
809    @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
810    destruct %
811  |43,44,45: (* XXX: unconditional jumps *)
812    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
813    cases (block_cost' ???) -block_cost'
814    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
815    whd in match (program_counter_after_other ??); normalize nodelta destruct
816    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
817  |25,26,27,28,29,30,31,32,33:
818    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
819    @(trace_compute_paid_trace_cl_jump prog … first_time_around program_size' … FETCH … the_trace program_counter_refl)
820   destruct %
821  |4,33:
822  |*:
823    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
824    cases(block_cost' ???) -block_cost'
825    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)     
826    destruct #assm @assm %
827  ]
828qed.
829
830definition block_cost:
831    ∀prog: labelled_object_code.
832    ∀program_counter': Word.
833      Σcost_of_block: nat.
834        ∀start_status: Status (load_code_memory (oc prog)).
835        ∀final_status: Status (load_code_memory (oc prog)).
836        ∀trace_ends_flag.
837        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
838        ∀unrepeating_witness: tal_unrepeating … the_trace.
839          program_counter' = program_counter … start_status →
840            cost_of_block = compute_paid_trace_any_label … the_trace.
841  #prog #program_counter
842  cases(block_cost' prog program_counter (2^16) true)
843  #cost_of_block #block_cost_hyp
844  %{cost_of_block}
845  cases(lookup_opt … (costlabels prog)) in block_cost_hyp;
846  [2: #cost_label] normalize nodelta
847  #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
848  @hyp @tal_pc_list_length_leq_total_program_size try assumption
849qed.
Note: See TracBrowser for help on using the repository browser.