source: src/ASM/ASMCosts.ma @ 1929

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

Simplified proof by removing most of the invariants on the statements all together (reachable_program_counter, good_program), and fixing the size of the total_program_size to be constantly 216.

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