source: src/ASM/ASMCosts.ma @ 2531

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

Trivial tweaks.

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