source: src/ASM/ASMCosts.ma @ 2708

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

Further tweak to Brian's changes: no normalization reqd at all!

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