source: src/ASM/ASMCosts.ma @ 2756

Last change on this file since 2756 was 2756, checked in by sacerdot, 7 years ago

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

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