source: src/ASM/ASMCosts.ma @ 3051

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

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

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