source: src/ASM/ASMCosts.ma @ 3112

Last change on this file since 3112 was 3112, checked in by tranquil, 7 years ago

added invariant that costlabels are only assigned to NOPs (not proved
yet, assembly has a new cases daemon)

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