source: src/ASM/ASMCosts.ma @ 1928

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

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File size: 51.3 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7(* XXX: alternative approach:
8 * R : Word → Prop
9 * TPS ≝ |R|
10 * GP : ∀a. R(a) → R(next(a))
11 *)
12
13let rec fetch_program_counter_n
14  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
15    on n: option Word ≝
16  match n with
17  [ O ⇒ Some … program_counter
18  | S n ⇒
19    match fetch_program_counter_n n code_memory program_counter with
20    [ None ⇒ None …
21    | Some tail_pc ⇒
22      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
23        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
24          Some … program_counter
25        else
26          None Word (* XXX: overflow! *)
27    ]
28  ].
29   
30definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
31  λcode_memory: BitVectorTrie Byte 16.
32  λprogram_size: nat.
33  λprogram_counter: Word.
34    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
35        nat_of_bitvector 16 program_counter < program_size.
36   
37definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝
38  λcost_labels.
39    injective … (λx. lookup_opt … x cost_labels).
40   
41definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
42  λcode_memory: BitVectorTrie Byte 16.
43  λtotal_program_size: nat.
44  ∀program_counter: Word.
45  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
46  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
47    match instruction with
48    [ RealInstruction instr ⇒
49      match instr with
50      [ RET                    ⇒ True
51      | JC   relative          ⇒ True (* XXX: see below *)
52      | JNC  relative          ⇒ True (* XXX: see below *)
53      | JB   bit_addr relative ⇒ True
54      | JNB  bit_addr relative ⇒ True
55      | JBC  bit_addr relative ⇒ True
56      | JZ   relative          ⇒ True
57      | JNZ  relative          ⇒ True
58      | CJNE src_trgt relative ⇒ True
59      | DJNZ src_trgt relative ⇒ True
60      | _                      ⇒
61        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
62          nat_of_bitvector … program_counter' < total_program_size
63      ]
64    | LCALL addr         ⇒
65      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
66        nat_of_bitvector … program_counter' < total_program_size
67    | ACALL addr         ⇒
68      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
69        nat_of_bitvector … program_counter' < total_program_size
70    | AJMP  addr         ⇒
71      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
72        reachable_program_counter code_memory total_program_size jump_target
73    | LJMP  addr         ⇒
74      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
75        reachable_program_counter code_memory total_program_size jump_target
76    | SJMP  addr     ⇒
77      let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in
78        reachable_program_counter code_memory total_program_size jump_target
79    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
80      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
81        nat_of_bitvector … program_counter' < total_program_size
82    | MOVC  src trgt ⇒
83        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
84          nat_of_bitvector … program_counter' < total_program_size
85    ].
86
87definition current_instruction_label ≝
88  λcode_memory.
89  λcost_labels: BitVectorTrie costlabel 16.
90  λs: Status code_memory.
91  let pc ≝ program_counter … code_memory s in
92    lookup_opt … pc cost_labels.
93
94definition next_instruction_properly_relates_program_counters ≝
95  λcode_memory.
96  λbefore: Status code_memory.
97  λafter : Status code_memory.
98    let program_counter_before ≝ program_counter ? code_memory before in
99    let 〈instruction, program_counter_after, ticks〉 ≝ fetch code_memory program_counter_before in
100      program_counter ? code_memory after = program_counter_after.
101
102definition word_deqset: DeqSet ≝
103  mk_DeqSet Word (eq_bv 16) ?.
104  @refl_iff_eq_bv_true
105qed.
106
107definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
108  λcode_memory.
109  λcost_labels.
110    mk_abstract_status
111      (Status code_memory)
112      (λs,s'. (execute_1 … s) = s')
113      word_deqset
114      (program_counter …)
115      (λs,class. ASM_classify … s = class)
116      (current_instruction_label code_memory cost_labels)
117      (next_instruction_properly_relates_program_counters code_memory)
118      ?.
119  cases daemon (* XXX: is final predicate *)
120qed.
121
122let rec trace_any_label_length
123  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
124    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
125      (final_status: Status code_memory)
126      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
127        on the_trace: nat ≝
128  match the_trace with
129  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
130  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 0
131  | tal_base_return the_status _ _ _ ⇒ 0
132  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
133      let tail_length ≝ trace_any_label_length … final_trace in
134      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
135        pc_difference + tail_length
136  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
137      let tail_length ≝ trace_any_label_length … tail_trace in
138      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
139        pc_difference + tail_length       
140  ].
141
142definition trace_any_label_length' ≝
143  λcode_memory: BitVectorTrie Byte 16.
144  λcost_labels: BitVectorTrie costlabel 16.
145  λtrace_ends_flag: trace_ends_with_ret.
146  λstart_status: Status code_memory.
147  λfinal_status: Status code_memory.
148  λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status.
149    as_trace_any_label_length' … the_trace.
150
151let rec all_program_counter_list
152  (n: nat)
153    on n ≝
154  match n with
155  [ O ⇒ [ ]
156  | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n')
157  ].
158
159lemma all_program_counter_list_bound_eq:
160  ∀bound: nat.
161    |all_program_counter_list bound| = bound.
162  #bound elim bound try %
163  #bound' #inductive_hypothesis normalize
164  >inductive_hypothesis %
165qed.
166
167lemma mem_all_program_counter_list_lt_bound:
168  ∀bound: nat.
169  ∀bound_proof: bound ≤ 2^16.
170  ∀e: Word.
171    memb word_deqset e (all_program_counter_list bound) = true →
172      nat_of_bitvector … e < bound.
173  #bound elim bound
174  [1:
175    #bound_proof #e
176    normalize #absurd destruct(absurd)
177  |2:
178    #bound' #inductive_hypothesis
179    #bound_proof #e
180    change with (if eq_bv ??? then ? else ? = ? → ?)
181    @eq_bv_elim
182    [1:
183      #eq_assm
184      normalize nodelta destruct #_
185      >nat_of_bitvector_bitvector_of_nat_inverse try assumption
186      normalize %
187    |2:
188      #neq_assm normalize nodelta
189      #memb_assm %2 @inductive_hypothesis
190      try assumption
191      @(transitive_le bound' (S bound'))
192      try assumption %2 %
193    ]
194  ]
195qed.
196
197lemma lt_bound_mem_all_program_counter_list:
198  ∀bound: nat.
199  ∀bound_proof: bound ≤ 2^16.
200  ∀e: Word.
201    nat_of_bitvector … e < bound →
202      memb word_deqset e (all_program_counter_list bound) = true.
203  #bound elim bound
204  [1:
205    #bound_proof #e normalize
206    #absurd cases (lt_to_not_zero … absurd)
207  |2:
208    #bound' #inductive_hypothesis
209    #bound_proof #e
210    change with (? → if eq_bv ??? then ? else ? = ?)
211    #assm
212    cases (le_to_or_lt_eq … (nat_of_bitvector 16 e) bound' ?)
213    [1:
214      #e_lt_assm
215      @eq_bv_elim
216      [1:
217        #eq_assm normalize nodelta %
218      |2:
219        #neq_assm normalize nodelta
220        @inductive_hypothesis try assumption
221        @(transitive_le bound' (S bound')) try assumption
222        %2 %
223      ]
224    |2:
225      #relevant >eq_eq_bv normalize nodelta try %
226      destruct >bitvector_of_nat_inverse_nat_of_bitvector %
227    |3:
228      normalize in assm;
229      @le_S_S_to_le assumption
230    ]
231  ]
232qed.
233
234include alias "arithmetics/nat.ma".
235
236lemma fetch_program_counter_n_Sn:
237  ∀instruction: instruction.
238  ∀program_counter, program_counter': Word.
239  ∀ticks, n: nat.
240  ∀code_memory: BitVectorTrie Byte 16.
241    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
242      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
243        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
244          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
245  #instruction #program_counter #program_counter' #ticks #n #code_memory
246  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
247  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
248  <fetch_program_counter_n_hyp normalize nodelta
249  <fetch_hyp normalize nodelta
250  change with (
251    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
252  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
253  >(le_to_leb_true … lt_hyp) %
254qed.
255
256(* XXX: indexing bug *)
257lemma execute_1_and_program_counter_after_other_in_lockstep:
258  ∀code_memory: BitVectorTrie Byte 16.
259  ∀start_status: Status code_memory.
260    ASM_classify code_memory start_status = cl_other →
261      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
262        program_counter ? ? (execute_1 … start_status) =
263          program_counter_after_other pc instruction.
264  #code_memory #start_status #classify_assm
265  whd in match execute_1; normalize nodelta
266  cases (execute_1' code_memory start_status) #the_status
267  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
268  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
269  #classify_assm #classify_assm' @classify_assm' assumption
270qed-.
271
272let rec tal_pc_list_lt_total_program_size
273  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
274    (total_program_size: nat) (total_program_size_invariant: total_program_size ≤ 2^16)
275      (good_program_witness: good_program code_memory total_program_size)
276        (start: Status code_memory) (final: Status code_memory) (trace_ends_flag: trace_ends_with_ret)
277          (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final)
278            (pc: as_pc (ASM_abstract_status code_memory cost_labels))
279              on the_trace:
280  reachable_program_counter code_memory total_program_size (program_counter … start) →
281    memb word_deqset pc (tal_pc_list (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace) = true →
282      nat_of_bitvector 16 pc<total_program_size ≝
283  match the_trace with
284  [ tal_base_not_return the_status _ _ _ _ ⇒ ?
285  | tal_base_return the_status _ _ _ ⇒ ?
286  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ ?
287  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
288     _ classifier after_return call_trace _ final_trace ⇒ ?
289  | tal_step_default end_flag status_pre status_init status_end execute tail_trace classifier _ ⇒ ?
290  ].
291  #reachable_program_counter_witness
292  whd in ⊢ (??%? → ?); @(bool_inv_ind … (pc==as_pc_of (ASM_abstract_status code_memory cost_labels) ?))
293  normalize nodelta #eq_assm cases reachable_program_counter_witness
294  [1,3,5,7,9:
295    >(eq_bv_eq … eq_assm) #_ #relevant #_
296    assumption
297  |2,4,6:
298    #_ #_ #absurd
299    normalize in absurd; destruct(absurd)
300  |8:
301    #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption
302    whd in after_return;
303    lapply after_return
304    @pair_elim * normalize nodelta #instruction #pc' #ticks
305    #fetch_eq #pc_assm' >pc_assm'
306    lapply (good_program_witness ? reachable_program_counter_witness)
307    whd in classifier; whd in classifier:(??%?);
308    whd in match (current_instruction ??) in classifier;
309    whd in match current_instruction0 in classifier;
310    >fetch_eq in classifier;
311    normalize nodelta cases instruction
312    normalize nodelta -tal_pc_list_lt_total_program_size
313    [8:
314      #preinstruction elim preinstruction
315      normalize in match (? = cl_call);
316    ]
317    try (#assm1 #assm2 #absurd destruct(absurd) @I)
318    try (#assm1 #absurd destruct(absurd) @I)
319    try (#absurd destruct(absurd) @I)
320    #_ #_ * #relevant #pc_tps_assm'
321    whd cases reachable_program_counter_witness * #n
322    #Some_assm #_ % try assumption
323    %{(S n)}
324    @(fetch_program_counter_n_Sn … Some_assm (sym_eq … fetch_eq))
325    assumption
326  |10:
327    #Some_assm #tps_lt_assm @tal_pc_list_lt_total_program_size try assumption -tal_pc_list_lt_total_program_size
328    lapply (execute_1_and_program_counter_after_other_in_lockstep … status_pre classifier)
329    @pair_elim * #instruction #pc #ticks normalize nodelta
330    #fetch_eq whd in match program_counter_after_other; normalize nodelta
331    lapply (good_program_witness … reachable_program_counter_witness)
332    whd in classifier; whd in classifier:(??%?);
333    whd in match (current_instruction ??) in classifier;
334    whd in match current_instruction0 in classifier;
335    >fetch_eq in classifier; normalize nodelta cases instruction
336    normalize nodelta
337    [8:
338      #preinstruction elim preinstruction
339      normalize in match (? = cl_other);
340    ]
341    try (#assm1 #assm2 #absurd destruct(absurd) @I)
342    try (#assm1 #absurd destruct(absurd) @I)
343    try (#absurd destruct(absurd) @I) normalize nodelta
344    [27,28,29:
345      #addr #_ #reachable
346      #program_counter_execute_1_refl
347      whd in execute; <execute
348      >program_counter_execute_1_refl assumption
349    |*:
350      try (#assm1 #assm2 #_ * #relevant #pc_lt_assm)
351      try (#assm1 #_ * #relevant #pc_lt_assm)
352      try (#_ * #relevant #pc_lt_assm) #pc_refl
353      cases reachable_program_counter_witness * #n
354      #Some_assm #tps_lt_assm
355      whd in match reachable_program_counter; normalize nodelta %
356      try %{(S n)}
357      whd in execute; <execute
358      try (@(fetch_program_counter_n_Sn instruction ?? ticks ?? Some_assm ?) >execute >fetch_eq <pc_refl >execute try %)
359      <pc_refl in relevant; <execute #assm
360      >pc_refl >pc_refl in assm; #assm assumption
361    ]
362  ]
363qed.
364
365lemma sublist_tal_pc_list_all_program_counter_list:
366  ∀code_memory: BitVectorTrie Byte 16.
367  ∀cost_labels: BitVectorTrie costlabel 16.
368  ∀total_program_size: nat.
369  ∀total_program_size_invariant: total_program_size ≤ 2^16.
370  ∀good_program_witness: good_program code_memory total_program_size.
371  ∀start, final: Status code_memory.
372  ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
373    (program_counter (BitVectorTrie Byte 16) code_memory start).
374  ∀trace_ends_flag.
375  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
376    sublist ? (tal_pc_list … the_trace) (all_program_counter_list total_program_size).
377  #code_memory #cost_labels #total_program_size #total_program_size_invariant
378  #good_program_witness #start #final #reachable_program_counter_witness
379  #trace_ends_flag #the_trace
380  whd in match (sublist ???); #pc #memb_assm
381  @lt_bound_mem_all_program_counter_list
382  try assumption destruct
383  lapply memb_assm -memb_assm
384  @tal_pc_list_lt_total_program_size
385  assumption
386qed.
387
388corollary tal_pc_list_length_leq_total_program_size:
389  ∀code_memory: BitVectorTrie Byte 16.
390  ∀cost_labels: BitVectorTrie costlabel 16.
391  ∀total_program_size: nat.
392  ∀total_program_size_invariant: total_program_size ≤ 2^16.
393  ∀good_program_witness: good_program code_memory total_program_size.
394  ∀start, final: Status code_memory.
395  ∀reachable_program_counter_witness: reachable_program_counter code_memory total_program_size
396    (program_counter (BitVectorTrie Byte 16) code_memory start).
397  ∀trace_ends_flag.
398  ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
399  ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace.
400    |tal_pc_list … the_trace| ≤ total_program_size.
401  #code_memory #cost_labels #total_program_size #total_program_size_invariant
402  #good_program_witness #start #final #reachable_program_counter_witness
403  #trace_ends_flag #the_trace #unrepeating_witness
404  <(all_program_counter_list_bound_eq total_program_size)
405  @sublist_length
406  [1:
407    @tal_unrepeating_uniqueb
408    assumption
409  |2:
410    @sublist_tal_pc_list_all_program_counter_list
411    assumption
412  ]
413qed.
414
415let rec compute_paid_trace_any_label
416  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
417    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
418      (final_status: Status code_memory)
419        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
420       on the_trace: nat ≝
421  match the_trace with
422  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
423  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
424  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ current_instruction_cost … pre_fun_call
425  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
426     _ _ _ call_trace _ final_trace ⇒
427      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
428      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
429        current_instruction_cost + final_trace_cost
430  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
431      let current_instruction_cost ≝ current_instruction_cost … status_pre in
432      let tail_trace_cost ≝
433       compute_paid_trace_any_label … cost_labels end_flag
434        status_init status_end tail_trace
435      in
436        current_instruction_cost + tail_trace_cost
437  ].
438
439definition compute_paid_trace_label_label ≝
440  λcode_memory: BitVectorTrie Byte 16.
441  λcost_labels: BitVectorTrie costlabel 16.
442  λtrace_ends_flag: trace_ends_with_ret.
443  λstart_status: Status code_memory.
444  λfinal_status: Status code_memory.
445  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
446  match the_trace with
447  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
448      compute_paid_trace_any_label … given_trace
449  ].
450
451lemma reachable_program_counter_to_0_lt_total_program_size:
452  ∀code_memory: BitVectorTrie Byte 16.
453  ∀program_counter: Word.
454  ∀total_program_size: nat.
455    reachable_program_counter code_memory total_program_size program_counter →
456      0 < total_program_size.
457  #code_memory #program_counter #total_program_size
458  whd in match reachable_program_counter; normalize nodelta * * #some_n
459  #_ cases (nat_of_bitvector 16 program_counter)
460  [1:
461    #assm assumption
462  |2:
463    #new_pc @ltn_to_ltO
464  ]
465qed.
466
467lemma trace_compute_paid_trace_cl_other:
468  ∀code_memory' : (BitVectorTrie Byte 16).
469  ∀program_counter' : Word.
470  ∀total_program_size : ℕ.
471  ∀cost_labels : (BitVectorTrie costlabel 16).
472  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
473  ∀good_program_witness : (good_program code_memory' total_program_size).
474  ∀program_size' : ℕ.
475  ∀ticks : ℕ.
476  ∀instruction : instruction.
477  ∀program_counter'' : Word.
478  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
479  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
480  ∀start_status : (Status code_memory').
481  ∀final_status : (Status code_memory').
482  ∀trace_ends_flag : trace_ends_with_ret.
483  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
484  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
485  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
486  ∀classify_assm: ASM_classify0 instruction = cl_other.
487  ∀pi1 : ℕ.
488   (if match lookup_opt costlabel 16 program_counter''' cost_labels with 
489         [None ⇒ true
490         |Some _ ⇒ false
491         ] 
492    then
493      ∀start_status0:Status code_memory'.
494      ∀final_status0:Status code_memory'.
495      ∀trace_ends_flag0:trace_ends_with_ret.
496      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
497        trace_any_label_length' code_memory' cost_labels trace_ends_flag0
498          start_status0 final_status0 the_trace0 ≤ program_size' →
499        program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
500                  pi1
501                    =compute_paid_trace_any_label code_memory' cost_labels
502                     trace_ends_flag0 start_status0 final_status0 the_trace0
503    else (pi1=O) )
504   → ticks+pi1
505     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
506      start_status final_status the_trace.
507  #code_memory' #program_counter' #total_program_size #cost_labels
508  #reachable_program_counter_witness #good_program_witness
509  #program_size' #ticks #instruction #program_counter'' #FETCH
510  #start_status #final_status
511  #trace_ends_flag #the_trace #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
512  #recursive_assm
513  @(trace_any_label_inv_ind … the_trace)
514    [5:
515      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
516      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
517      #the_trace_refl
518      destruct
519      whd in match (trace_any_label_length … (tal_step_default …));
520      whd in match (compute_paid_trace_any_label … (tal_step_default …));
521      whd in costed_assm:(?%);
522      generalize in match costed_assm;
523      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
524      whd in match (as_label ??);
525      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
526        in ⊢ (??%? → % → ?);
527      #lookup_assm cases lookup_assm
528      [1:
529        #None_lookup_opt_assm normalize nodelta #_
530        generalize in match recursive_assm;
531        lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
532        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
533        #None_lookup_opt_assm <None_lookup_opt_assm
534        normalize nodelta #new_recursive_assm
535        cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
536          end_flag trace_any_label ? ?) try %
537        whd in match (current_instruction_cost … status_pre);
538        cut(ticks = \snd (fetch code_memory'
539           (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
540        [1,3,5:
541          <FETCH %
542        |2:
543          #ticks_refl_assm
544          >ticks_refl_assm %
545        |4:
546          #ticks_refl_assm
547          change with (S ? ≤ S ?) in size_invariant;
548          lapply (le_S_S_to_le … size_invariant) #assm
549          assumption
550        |6:
551          #ticks_refl_assm
552          <rewrite_assm %
553        ]
554      |2:
555        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
556        #absurd
557        cases (not_Some_neq_None_to_False ?? absurd)
558      ]
559    |1:
560      #status_start #status_final #execute_assm #classifier_assm #costed_assm
561      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
562      destruct
563      whd in match (trace_any_label_length … (tal_base_not_return …));
564      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
565      whd in costed_assm;
566      generalize in match costed_assm;
567      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
568      whd in match (as_label ??);
569      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
570        in ⊢ (??%? → % → ?);
571      #lookup_assm cases lookup_assm
572      [1:
573        #None_lookup_opt_assm
574        #absurd @⊥ cases absurd -absurd #absurd @absurd %
575      |2:
576        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
577        generalize in match recursive_assm;
578        cases classifier_assm
579        [1:
580          whd in ⊢ (% → ?);
581          whd in ⊢ (??%? → ?);
582          whd in match (current_instruction code_memory' status_start);
583          <FETCH generalize in match classify_assm;
584          cases instruction
585          [8:
586            #preinstruction normalize nodelta
587            whd in match ASM_classify0; normalize nodelta
588            #contradiction >contradiction #absurd destruct(absurd)
589          ]
590          try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
591          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
592          normalize in ignore; destruct(ignore)
593        |2:
594          -classifier_assm #classifier_assm
595          lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
596          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
597          #Some_lookup_opt_assm <Some_lookup_opt_assm
598          normalize nodelta #new_recursive_assm >new_recursive_assm
599          cut(ticks = \snd (fetch code_memory'
600             (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
601          [1:
602            <FETCH %
603          |2:
604            #ticks_refl_assm >ticks_refl_assm
605            <plus_n_O %
606          ]
607        ]
608      ]
609    |2:
610      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
611      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
612    |3:
613      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
614      #classifier_assm #after_return_assm #trace_label_return #costed_assm
615      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
616      destruct @⊥
617    |4:
618      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
619      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
620      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
621      #final_status_refl #the_trace_refl destruct @⊥
622    ]
623  change with (ASM_classify0 ? = ?) in classifier_assm;
624  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
625  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
626  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
627qed.
628
629lemma trace_compute_paid_trace_cl_jump:
630  ∀code_memory': BitVectorTrie Byte 16.
631  ∀program_counter': Word.
632  ∀total_program_size: ℕ.
633  ∀cost_labels: BitVectorTrie costlabel 16.
634  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
635  ∀good_program_witness: good_program code_memory' total_program_size.
636  ∀first_time_around: bool.
637  ∀program_size': ℕ.
638  ∀ticks: ℕ.
639  ∀instruction: instruction.
640  ∀program_counter'': Word.
641  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
642  ∀start_status: (Status code_memory').
643  ∀final_status: (Status code_memory').
644  ∀trace_ends_flag: trace_ends_with_ret.
645  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
646  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
647  ∀classify_assm: ASM_classify0 instruction = cl_jump.
648    ticks
649     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
650      start_status final_status the_trace.
651  #code_memory' #program_counter' #total_program_size #cost_labels
652  #reachable_program_counter_witness #good_program_witness #first_time_around
653  #program_size' #ticks #instruction #program_counter'' #FETCH
654  #start_status #final_status
655  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
656  @(trace_any_label_inv_ind … the_trace)
657  [5:
658    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
659    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
660    #the_trace_refl destruct @⊥
661  |1:
662    #status_start #status_final #execute_assm #classifier_assm #costed_assm
663    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
664    destruct
665    whd in match (trace_any_label_length … (tal_base_not_return …));
666    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
667    <FETCH %
668  |2:
669    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
670    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
671  |3:
672    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
673    #classifier_assm #after_return_assm #trace_label_return #costed_assm
674    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
675    destruct @⊥
676  |4:
677    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
678    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
679    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
680    #final_status_refl #the_trace_refl destruct @⊥
681  ]
682  change with (ASM_classify0 ? = ?) in classifier_assm;
683  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
684  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
685  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
686qed.
687
688lemma trace_compute_paid_trace_cl_call:
689  ∀code_memory' : (BitVectorTrie Byte 16).
690  ∀program_counter' : Word.
691  ∀total_program_size : ℕ.
692  ∀cost_labels : (BitVectorTrie costlabel 16).
693  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
694  ∀good_program_witness : (good_program code_memory' total_program_size).
695  ∀program_size' : ℕ.
696  ∀ticks : ℕ.
697  ∀instruction : instruction.
698  ∀program_counter'' : Word.
699  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
700  ∀start_status : (Status code_memory').
701  ∀final_status : (Status code_memory').
702  ∀trace_ends_flag : trace_ends_with_ret.
703  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
704  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
705  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
706  ∀classify_assm: ASM_classify0 instruction = cl_call.
707  (∀pi1:ℕ
708  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
709      [None ⇒ true | Some _ ⇒ false] 
710   then (∀start_status0:Status code_memory'
711             .∀final_status0:Status code_memory'
712              .∀trace_ends_flag0:trace_ends_with_ret
713               .∀the_trace0:trace_any_label
714                                        (ASM_abstract_status code_memory' cost_labels)
715                                        trace_ends_flag0 start_status0 final_status0.
716                trace_any_label_length' code_memory' cost_labels trace_ends_flag0
717                  start_status0 final_status0 the_trace0
718                   ≤ program_size' →
719                program_counter''
720                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
721                 → pi1
722                   =compute_paid_trace_any_label code_memory' cost_labels
723                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
724   else (pi1=O) 
725   → ticks+pi1
726     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
727      start_status final_status the_trace).
728  #code_memory' #program_counter' #total_program_size #cost_labels
729  #reachable_program_counter_witness #good_program_witness #program_size'
730  #ticks #instruction #program_counter'' #FETCH
731  #start_status #final_status #trace_ends_flag
732  #the_trace #program_counter_refl #size_invariant #classify_assm
733  #recursive_block_cost #recursive_assm
734  @(trace_any_label_inv_ind … the_trace)
735  [5:
736    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
737    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
738    #the_trace_refl destruct @⊥
739  |1:
740    #status_start #status_final #execute_assm #classifier_assm #costed_assm
741    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
742    destruct @⊥
743  |2:
744    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
745    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
746  |3:
747    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
748    #classifier_assm #after_return_assm #trace_label_return #costed_assm
749    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
750    destruct
751    whd in match (trace_any_label_length … (tal_base_call …));
752    whd in match (compute_paid_trace_any_label … (tal_base_call …));
753    whd in costed_assm;
754    generalize in match costed_assm;
755    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
756    whd in match (as_label ??);
757    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
758      in ⊢ (??%? → % → ?);
759    #lookup_assm cases lookup_assm
760    [1:
761      #None_lookup_opt normalize nodelta #absurd cases absurd
762      -absurd #absurd @⊥ @absurd %
763    |2:
764      #costlabel #Some_lookup_opt normalize nodelta #ignore
765      generalize in match recursive_assm;
766      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
767      [1:
768        generalize in match after_return_assm;
769        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
770      |2:
771        #program_counter_assm >program_counter_assm <Some_lookup_opt
772        normalize nodelta #new_recursive_assm >new_recursive_assm
773        cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
774        [1:
775          <FETCH %
776        |2:
777          #ticks_refl_assm >ticks_refl_assm
778          <plus_n_O %
779        ]
780      ]
781    ]
782  |4:
783    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
784    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
785    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
786    #final_status_refl #the_trace_refl
787    generalize in match execute_assm; destruct #execute_assm
788    whd in match (trace_any_label_length … (tal_step_call …));
789    whd in match (compute_paid_trace_any_label … (tal_step_call …));
790    whd in costed_assm:(?%);
791    generalize in match costed_assm;
792    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
793    whd in match (as_label ??);
794    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
795      in ⊢ (??%? → % → ?);
796    #lookup_assm cases lookup_assm
797    [1:
798      #None_lookup_opt_assm normalize nodelta #ignore
799      generalize in match recursive_assm;
800      cut(program_counter'' = program_counter … status_after_fun_call)
801      [1:
802        generalize in match after_return_assm;
803        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
804      |2:
805        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
806        normalize nodelta #new_recursive_assm
807        cases (new_recursive_assm … trace_any_label ? ?)
808        [1:
809          @plus_right_monotone whd in ⊢ (???%); <FETCH %
810        |2:
811          @le_S_S_to_le @size_invariant
812        |3:
813          %
814        ]
815      ]
816    |2:
817      #cost_label #Some_lookup_opt_assm #absurd
818      cases (not_Some_neq_None_to_False ?? absurd)
819    ]
820  ]
821  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
822  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
823  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
824  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
825  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
826  #absurd destruct(absurd)
827qed.
828
829lemma trace_compute_paid_trace_cl_return:
830  ∀code_memory' : (BitVectorTrie Byte 16).
831  ∀program_counter' : Word.
832  ∀total_program_size : ℕ.
833  ∀cost_labels : (BitVectorTrie costlabel 16).
834  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
835  ∀good_program_witness : (good_program code_memory' total_program_size).
836  ∀program_size' : ℕ.
837  ∀ticks : ℕ.
838  ∀instruction : instruction.
839  ∀program_counter'' : Word.
840  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
841  ∀start_status : (Status code_memory').
842  ∀final_status : (Status code_memory').
843  ∀trace_ends_flag : trace_ends_with_ret.
844  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
845  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
846  ∀classify_assm: ASM_classify0 instruction = cl_return.
847    ticks
848     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
849      start_status final_status the_trace.
850  #code_memory' #program_counter' #total_program_size #cost_labels
851  #reachable_program_counter_witness #good_program_witness #program_size'
852  #ticks #instruction #program_counter'' #FETCH
853  #start_status #final_status #trace_ends_flag
854  #the_trace #program_counter_refl #classify_assm
855  @(trace_any_label_inv_ind … the_trace)
856  [1:
857    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
858    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
859    destruct @⊥
860  |2:
861    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
862    #start_status_refl #final_status_refl #the_trace_refl destruct
863    whd in match (trace_any_label_length … (tal_base_return …));
864    whd in match (compute_paid_trace_any_label … (tal_base_return …));
865    <FETCH %
866  |3:
867    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
868    #classifier_assm #after_return_assm #trace_label_return #costed_assm
869    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
870    destruct @⊥
871  |4:
872    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
873    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
874    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
875    #final_status_refl #the_trace_refl
876    destruct @⊥
877  |5:
878    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
879    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
880    #final_status_refl #the_trace_refl destruct @⊥
881  ]
882  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
883  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
884  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
885  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
886  <FETCH in classifier_assm; >classify_assm
887  #absurd try (destruct(absurd))
888  cases absurd
889  #absurd destruct(absurd)
890qed.
891
892lemma trace_any_label_length_leq_0_to_False:
893  ∀code_memory: BitVectorTrie Byte 16.
894  ∀cost_labels: BitVectorTrie costlabel 16.
895  ∀trace_ends_flag: trace_ends_with_ret.
896  ∀start_status: Status code_memory.
897  ∀final_status: Status code_memory.
898  ∀the_trace.
899  trace_any_label_length' code_memory cost_labels trace_ends_flag start_status
900    final_status the_trace ≤ 0 → False.
901  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
902  #the_trace
903  cases the_trace /2/
904qed.
905     
906let rec block_cost'
907  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
908    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
909      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
910        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
911          on program_size:
912          Σcost_of_block: nat.
913          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
914            ∀start_status: Status code_memory'.
915            ∀final_status: Status code_memory'.
916            ∀trace_ends_flag.
917            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
918              trace_any_label_length' … the_trace ≤ program_size →
919              program_counter' = program_counter … start_status →
920                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
921          else
922            (cost_of_block = 0) ≝
923  match program_size return λx. x = program_size → ? with
924  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
925  | S program_size' ⇒ λstep_case.
926    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
927    let to_continue ≝
928      match lookup_opt … program_counter' cost_labels with
929      [ None ⇒ true
930      | Some _ ⇒ first_time_around
931      ]
932    in
933      ((if to_continue then
934       pi1 … (match instruction return λx. x = instruction → ? with
935        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
936          match real_instruction return λx. x = real_instruction →
937          Σcost_of_block: nat.
938            ∀start_status: Status code_memory'.
939            ∀final_status: Status code_memory'.
940            ∀trace_ends_flag.
941            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
942              trace_any_label_length' … the_trace ≤ S program_size' →
943              program_counter' = program_counter … start_status →
944                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
945          [ RET                    ⇒ λinstr. ticks
946          | RETI                   ⇒ λinstr. ticks
947          | JC   relative          ⇒ λinstr. ticks
948          | JNC  relative          ⇒ λinstr. ticks
949          | JB   bit_addr relative ⇒ λinstr. ticks
950          | JNB  bit_addr relative ⇒ λinstr. ticks
951          | JBC  bit_addr relative ⇒ λinstr. ticks
952          | JZ   relative          ⇒ λinstr. ticks
953          | JNZ  relative          ⇒ λinstr. ticks
954          | CJNE src_trgt relative ⇒ λinstr. ticks
955          | DJNZ src_trgt relative ⇒ λinstr. ticks
956          | _                      ⇒ λinstr.
957              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
958          ] (refl …)
959        | ACALL addr     ⇒ λinstr.
960            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
961        | AJMP  addr     ⇒ λinstr.
962          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
963            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
964        | LCALL addr     ⇒ λinstr.
965            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
966        | LJMP  addr     ⇒ λinstr.
967          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
968            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
969        | SJMP  addr     ⇒ λinstr.
970          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
971            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
972        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
973            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
974        | MOVC  src trgt ⇒ λinstr.
975            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
976        ] (refl …))
977      else
978        0)
979      : Σcost_of_block: nat.
980          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
981          [ true ⇒
982            ∀start_status: Status code_memory'.
983            ∀final_status: Status code_memory'.
984            ∀trace_ends_flag.
985            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
986              trace_any_label_length' … the_trace ≤ S program_size' →
987              program_counter' = program_counter … start_status →
988                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
989          | false ⇒
990            (cost_of_block = 0)
991          ])
992  ] (refl …).
993  [2:
994    change with (if to_continue then ? else (? = 0))
995    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
996    @pi2
997  |1:
998    destruct
999    cases (lookup_opt ????) normalize nodelta
1000    [1:
1001      #start_status #final_status #trace_ends_flag #the_trace
1002      #absurd
1003      cases (trace_any_label_length_leq_0_to_False … absurd)
1004    |2:
1005      #cost cases first_time_around normalize nodelta try %
1006      #start_status #final_status #trace_ends_flag #the_trace #absurd
1007      cases (trace_any_label_length_leq_0_to_False … absurd)
1008    ]
1009  |3:
1010    change with (if to_continue then ? else (0 = 0))
1011    >p normalize nodelta %
1012  |6,7:
1013    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1014    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl)
1015    destruct %
1016  |69,77,79:
1017    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1018    cases(block_cost' ????????) -block_cost'
1019    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
1020    destruct %
1021  |4,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,51,53,55,57,59,61,63,65,
1022    67:
1023    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1024    cases(block_cost' ????????) -block_cost'
1025    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)     
1026    destruct #assm @assm %
1027  |42,43,44,45,46,47,48,49,50:
1028    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1029    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … FETCH … the_trace program_counter_refl)
1030    destruct %
1031  |71,73,75: (* XXX: unconditional jumps *)
1032    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
1033    cases (block_cost' ????????) -block_cost'
1034    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
1035    whd in match (program_counter_after_other ??); normalize nodelta destruct
1036    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
1037  ]
1038  -block_cost'
1039  [29,30,31: (* XXX: unconditional jumps *)
1040    normalize nodelta
1041    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1042    lapply (good_program_witness program_counter' reachable_program_counter_witness)
1043    <FETCH normalize nodelta <instr normalize nodelta #assm assumption
1044  |*:
1045    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1046    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1047    <FETCH normalize nodelta destruct normalize nodelta
1048    * #program_counter_lt' #program_counter_lt_tps'
1049    % try assumption
1050    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1051    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1052    >(le_to_leb_true … program_counter_lt') %
1053  ]
1054qed.
1055
1056definition block_cost:
1057    ∀code_memory': BitVectorTrie Byte 16.
1058    ∀program_counter': Word.
1059    ∀total_program_size: nat.
1060    ∀total_program_size_invariant: total_program_size ≤ 2^16.
1061    ∀cost_labels: BitVectorTrie costlabel 16.
1062    ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
1063    ∀good_program_witness: good_program code_memory' total_program_size.
1064      Σcost_of_block: nat.
1065        ∀start_status: Status code_memory'.
1066        ∀final_status: Status code_memory'.
1067        ∀trace_ends_flag.
1068        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1069        ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size (program_counter (BitVectorTrie Byte 16) code_memory' start_status).
1070        ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace.
1071          program_counter' = program_counter … start_status →
1072            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
1073  λcode_memory: BitVectorTrie Byte 16.
1074  λprogram_counter: Word.
1075  λtotal_program_size: nat.
1076  λtotal_program_size_invariant: total_program_size ≤ 2^16.
1077  λcost_labels: BitVectorTrie costlabel 16.
1078  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1079  λgood_program_witness: good_program code_memory total_program_size. ?.
1080  cases(block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1081    reachable_program_counter_witness good_program_witness true)
1082  #cost_of_block #block_cost_hyp
1083  %{cost_of_block}
1084  cases(lookup_opt … cost_labels) in block_cost_hyp;
1085  [2: #cost_label] normalize nodelta
1086  #hyp #start_status #final_status #trace_ends_flag #the_trace
1087  #reachable_program_counter_witness #unrepeating_witness
1088  @hyp @tal_pc_list_length_leq_total_program_size try assumption
1089qed.
Note: See TracBrowser for help on using the repository browser.