source: src/ASM/ASMCosts.ma @ 2573

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

temporary fixes to ensure {compiler,correctness}.ma recompile
after paolo's recent (r2553) changes to StructuredTraces?.ma

a number of lemmas could be made a bit more abstract
I've been quite aggressive in use of ldots to suppress verbosity;
more should be possible

previous proofs now break, either

arising from missing cases or
renumbering of cases arising from the changes to trace_* constructors

arguably, much more refactoring would be helpful here
e.g. some dependencies simplified; but more possible

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