source: src/ASM/ASMCosts.ma @ 2832

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

Added abstraction in front of cases daemon for code extraction.

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