source: src/ASM/ASMCosts.ma @ 3034

Last change on this file since 3034 was 3028, checked in by sacerdot, 7 years ago

Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should have
been 0x82 and 0x83!

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