source: src/ASM/ASMCosts.ma @ 2475

Last change on this file since 2475 was 2475, checked in by campbell, 7 years ago

Get compiler.ma and correctness.ma checking again. Note that the back-end
is in a state of flux at the moment, so is axiomatised out.

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