source: src/ASM/ASMCosts.ma

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