source: src/ASM/ASMCosts.ma @ 3102

Last change on this file since 3102 was 3102, checked in by mckinna, 7 years ago

Removed redundant refs to current_instruction0,
which itself has been removed from AbstractStatus?

File size: 35.9 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 ? 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 ?? 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  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
408qed.
409
410lemma trace_compute_paid_trace_cl_jump:
411  ∀prog: labelled_object_code.
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 (cm prog) program_counter'.
419  ∀start_status: (Status (cm prog)).
420  ∀final_status: (Status (cm prog)).
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 #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  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
465qed.
466
467lemma trace_compute_paid_trace_cl_call:
468  ∀prog: labelled_object_code.
469  ∀program_counter' : Word.
470  ∀program_size' : ℕ.
471  ∀ticks : ℕ.
472  ∀instruction : instruction.
473  ∀program_counter'' : Word.
474  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
475  ∀start_status : (Status (cm prog)).
476  ∀final_status : (Status (cm prog)).
477  ∀trace_ends_flag : trace_ends_with_ret.
478  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
479  ∀program_counter_refl : (program_counter' = program_counter … start_status).
480  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
481  ∀classify_assm: ASM_classify0 instruction = cl_call.
482  (∀pi1:ℕ
483  .if match lookup_opt ?? program_counter'' (costlabels prog) with 
484      [None ⇒ true | Some _ ⇒ false] 
485   then (∀start_status0:Status (cm prog)
486             .∀final_status0:Status (cm prog)
487              .∀trace_ends_flag0:trace_ends_with_ret
488               .∀the_trace0:trace_any_label
489                                        (OC_abstract_status prog)
490                                        trace_ends_flag0 start_status0 final_status0.
491                trace_any_label_length … the_trace0
492                   ≤ program_size' →
493                program_counter''
494                 =program_counter … start_status0
495                 → pi1
496                   =compute_paid_trace_any_label … the_trace0) 
497   else (pi1=O) 
498   → ticks+pi1
499     =compute_paid_trace_any_label … the_trace).
500  #prog #program_counter' #program_size'
501  #ticks #instruction #program_counter'' #FETCH
502  #start_status #final_status #trace_ends_flag
503  #the_trace #program_counter_refl #size_invariant #classify_assm
504  #recursive_block_cost #recursive_assm
505  @(trace_any_label_inv_ind … the_trace)
506  [6:
507    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
508    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
509    #the_trace_refl destruct @⊥
510  |1:
511    #status_start #status_final #execute_assm #classifier_assm #costed_assm
512    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
513    destruct @⊥
514  |2:
515    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
516    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
517  |3:
518    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
519    #classifier_assm #after_return_assm #trace_label_return #costed_assm
520    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
521    destruct
522    whd in match (trace_any_label_length … (tal_base_call …));
523    whd in match (compute_paid_trace_any_label … (tal_base_call …));
524    whd in costed_assm;
525    generalize in match costed_assm;
526    generalize in match (refl … (lookup_opt … (program_counter … status_final) (costlabels prog)));
527    whd in match (as_label ??);
528    generalize in match (lookup_opt … (program_counter … status_final) ?)
529      in ⊢ (??%? → % → ?);
530    #lookup_assm cases lookup_assm
531    [1:
532      #None_lookup_opt normalize nodelta #absurd cases absurd
533      -absurd #absurd @⊥ @absurd %
534    |2:
535      #costlabel #Some_lookup_opt normalize nodelta #ignore
536      generalize in match recursive_assm;
537      cut(program_counter'' = (program_counter … status_final))
538      [1:
539        generalize in match after_return_assm;
540        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
541      |2:
542        #program_counter_assm >program_counter_assm <Some_lookup_opt
543        normalize nodelta #new_recursive_assm >new_recursive_assm
544        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre_fun_call)))
545        [1:
546          <FETCH %
547        |2:
548          #ticks_refl_assm >ticks_refl_assm
549          <plus_n_O %
550        ]
551      ]
552    ]
553  |4:
554    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
555    #classifier_assm #trace_label_return
556    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
557    destruct @⊥
558  |5:
559    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
560    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
561    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
562    #final_status_refl #the_trace_refl
563    generalize in match execute_assm; destruct #execute_assm
564    whd in match (trace_any_label_length … (tal_step_call …));
565    whd in match (compute_paid_trace_any_label … (tal_step_call …));
566    whd in costed_assm:(?%);
567    generalize in match costed_assm;
568    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) (costlabels ?)));
569    whd in match (as_label ??);
570    generalize in match (lookup_opt … (program_counter … status_after_fun_call) (costlabels prog))
571      in ⊢ (??%? → % → ?);
572    #lookup_assm cases lookup_assm
573    [1:
574      #None_lookup_opt_assm normalize nodelta #ignore
575      generalize in match recursive_assm;
576      cut(program_counter'' = program_counter … status_after_fun_call)
577      [1:
578        generalize in match after_return_assm;
579        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
580      |2:
581        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
582        normalize nodelta #new_recursive_assm
583        cases (new_recursive_assm … trace_any_label ? ?)
584        [1:
585          @plus_right_monotone whd in ⊢ (???%); <FETCH %
586        |2:
587          @le_S_S_to_le @size_invariant
588        |3:
589          %
590        ]
591      ]
592    |2:
593      #cost_label #Some_lookup_opt_assm #absurd
594      cases (not_Some_neq_None_to_False ?? absurd)
595    ]
596  ]
597  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
598  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
599  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
600  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
601  #absurd destruct(absurd)
602qed.
603
604lemma trace_compute_paid_trace_cl_return:
605  ∀prog: labelled_object_code.
606  ∀program_counter' : Word.
607  ∀program_size' : ℕ.
608  ∀ticks : ℕ.
609  ∀instruction : instruction.
610  ∀program_counter'' : Word.
611  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
612  ∀start_status : (Status (cm prog)).
613  ∀final_status : (Status (cm prog)).
614  ∀trace_ends_flag : trace_ends_with_ret.
615  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
616  ∀program_counter_refl : (program_counter' = program_counter … start_status).
617  ∀classify_assm: ASM_classify0 instruction = cl_return.
618    ticks
619     =compute_paid_trace_any_label … the_trace.
620  #prog #program_counter' #program_size'
621  #ticks #instruction #program_counter'' #FETCH
622  #start_status #final_status #trace_ends_flag
623  #the_trace #program_counter_refl #classify_assm
624  @(trace_any_label_inv_ind … the_trace)
625  [1:
626    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
627    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
628    destruct @⊥
629  |2:
630    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
631    #start_status_refl #final_status_refl #the_trace_refl destruct
632    whd in match (trace_any_label_length … (tal_base_return …));
633    whd in match (compute_paid_trace_any_label … (tal_base_return …));
634    <FETCH %
635  |3:
636    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
637    #classifier_assm #after_return_assm #trace_label_return #costed_assm
638    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
639    destruct @⊥
640  |4:
641    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
642    #classifier_assm
643    destruct @⊥
644    change with (ASM_classify0 ? = ?) in classifier_assm;
645    cases (current_instruction ??) in classifier_assm;
646    [7: #preinstruction cases preinstruction ]
647    try(#addr1 #addr2 #absurd normalize in absurd; destruct(absurd))
648    try(#addr #absurd normalize in absurd; destruct(absurd))
649    #absurd normalize in absurd; destruct(absurd)
650  |5:
651    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
652    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
653    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
654    #final_status_refl #the_trace_refl
655    destruct @⊥
656  |6:
657    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
658    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
659    #final_status_refl #the_trace_refl destruct @⊥
660  ]
661  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
662  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
663  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
664  <FETCH in classifier_assm; >classify_assm
665  #absurd try (destruct(absurd))
666  cases absurd
667  #absurd destruct(absurd)
668qed.
669
670lemma trace_any_label_length_leq_0_to_False:
671  ∀prog: labelled_object_code.
672  ∀trace_ends_flag: trace_ends_with_ret.
673  ∀start_status: Status (cm prog).
674  ∀final_status: Status (cm prog).
675  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
676   trace_any_label_length … the_trace ≤ 0 → False.
677  #prog #trace_ends_flag #start_status #final_status #the_trace
678  cases the_trace /2 by absurd/
679qed.
680     
681let rec block_cost'
682 (prog: labelled_object_code) (program_counter': Word)
683    (program_size: nat)
684      (first_time_around: bool)
685        on program_size:
686          Σcost_of_block: nat.
687          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
688            ∀start_status,final_status: Status (cm prog).
689            ∀trace_ends_flag.
690            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
691              trace_any_label_length … the_trace ≤ program_size →
692              program_counter' = program_counter … start_status →
693                cost_of_block = compute_paid_trace_any_label … the_trace
694          else
695            (cost_of_block = 0) ≝
696  match program_size return λx. x = program_size → ? with
697  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
698  | S program_size' ⇒ λstep_case.
699    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (cm prog) program_counter' in
700    let to_continue ≝
701      match lookup_opt … program_counter' (costlabels prog) with
702      [ None ⇒ true
703      | Some _ ⇒ first_time_around
704      ]
705    in
706      ((if to_continue then
707       pi1 … (match instruction return λx. x = instruction → ? with
708        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
709          match real_instruction return λx. x = real_instruction →
710          Σcost_of_block: nat.
711            ∀start_status,final_status: Status (cm prog).
712            ∀trace_ends_flag.
713            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
714              trace_any_label_length … the_trace ≤ S program_size' →
715              program_counter' = program_counter … start_status →
716                cost_of_block = compute_paid_trace_any_label … the_trace with
717          [ RET                    ⇒ λinstr. ticks
718          | RETI                   ⇒ λinstr. ticks
719          | JC   relative          ⇒ λinstr. ticks
720          | JNC  relative          ⇒ λinstr. ticks
721          | JB   bit_addr relative ⇒ λinstr. ticks
722          | JNB  bit_addr relative ⇒ λinstr. ticks
723          | JBC  bit_addr relative ⇒ λinstr. ticks
724          | JZ   relative          ⇒ λinstr. ticks
725          | JNZ  relative          ⇒ λinstr. ticks
726          | CJNE src_trgt relative ⇒ λinstr. ticks
727          | DJNZ src_trgt relative ⇒ λinstr. ticks
728          | JMP   addr             ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
729              ticks + block_cost' prog program_counter'' program_size' false
730          | _                      ⇒ λinstr.
731              ticks + block_cost' prog program_counter'' program_size' false
732          ] (refl …)
733        | ACALL addr     ⇒ λinstr.
734            ticks + block_cost' prog program_counter'' program_size' false
735        | AJMP  addr     ⇒ λinstr.
736          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
737            ticks + block_cost' prog jump_target program_size' false
738        | LCALL addr     ⇒ λinstr.
739            ticks + block_cost' prog program_counter'' program_size' false
740        | LJMP  addr     ⇒ λinstr.
741          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
742            ticks + block_cost' prog jump_target program_size' false
743        | SJMP  addr     ⇒ λinstr.
744          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
745            ticks + block_cost' prog jump_target program_size' false
746        | MOVC  src trgt ⇒ λinstr.
747            ticks + block_cost' prog program_counter'' program_size' false
748        ] (refl …))
749      else
750        0)
751      : Σcost_of_block: nat.
752          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
753          [ true ⇒
754            ∀start_status: Status (cm prog).
755            ∀final_status: Status (cm prog).
756            ∀trace_ends_flag.
757            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
758              trace_any_label_length … the_trace ≤ S program_size' →
759              program_counter' = program_counter … start_status →
760                cost_of_block = compute_paid_trace_any_label … the_trace
761          | false ⇒
762            (cost_of_block = 0)
763          ])
764  ] (refl …).
765  [2:
766    change with (if to_continue then ? else (? = 0))
767    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
768    @pi2
769  |1:
770    destruct
771    cases (lookup_opt ????) normalize nodelta
772    [1:
773      #start_status #final_status #trace_ends_flag #the_trace
774      #absurd
775      cases (trace_any_label_length_leq_0_to_False … absurd)
776    |2:
777      #cost cases first_time_around normalize nodelta try %
778      #start_status #final_status #trace_ends_flag #the_trace #absurd
779      cases (trace_any_label_length_leq_0_to_False … absurd)
780    ]
781  |3:
782    change with (if to_continue then ? else (0 = 0))
783    >p normalize nodelta %
784  |6,7:
785    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
786    @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl)
787    destruct %
788  |4,46,47:
789    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
790    cases(block_cost' ???) -block_cost'
791    @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
792    destruct %
793  |43,44,45: (* XXX: unconditional jumps *)
794    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
795    cases (block_cost' ???) -block_cost'
796    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
797    whd in match (program_counter_after_other ??); normalize nodelta destruct
798    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
799  |25,26,27,28,29,30,31,32,33:
800    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
801    @(trace_compute_paid_trace_cl_jump prog … first_time_around program_size' … FETCH … the_trace program_counter_refl)
802   destruct %
803  |4,33:
804  |*:
805    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
806    cases(block_cost' ???) -block_cost'
807    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)     
808    destruct #assm @assm %
809  ]
810qed.
811
812definition block_cost:
813    ∀prog: labelled_object_code.
814    ∀program_counter': Word.
815      Σcost_of_block: nat.
816        ∀start_status: Status (cm prog).
817        ∀final_status: Status (cm prog).
818        ∀trace_ends_flag.
819        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
820        ∀unrepeating_witness: tal_unrepeating … the_trace.
821          program_counter' = program_counter … start_status →
822            cost_of_block = compute_paid_trace_any_label … the_trace.
823  #prog #program_counter
824  cases(block_cost' prog program_counter (2^16) true)
825  #cost_of_block #block_cost_hyp
826  %{cost_of_block}
827  cases(lookup_opt … (costlabels prog)) in block_cost_hyp;
828  [2: #cost_label] normalize nodelta
829  #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
830  @hyp @tal_pc_list_length_leq_total_program_size try assumption
831qed.
Note: See TracBrowser for help on using the repository browser.