source: src/ASM/ASMCosts.ma @ 2907

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