source: src/ASM/ASMCosts.ma @ 2657

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

Ported to tailcalls (currently nothing is classified as a tailcall).

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