source: src/ASM/ASMCosts.ma @ 1935

Last change on this file since 1935 was 1935, checked in by mulligan, 8 years ago

Generalized some lemma in ASM/CostsProof.ma to work on abstract statuses, moving the abstract version in to common/StructuredTraces.ma. Ported rest of proof in ASM/CostsProof.ma to use new, generalized lemma.

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