source: src/ASM/ASMCosts.ma @ 1684

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

changes from the past week

File size: 87.0 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7let rec fetch_program_counter_n
8  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
9    on n: option Word ≝
10  match n with
11  [ O ⇒ Some … program_counter
12  | S n ⇒
13    match fetch_program_counter_n n code_memory program_counter with
14    [ None ⇒ None …
15    | Some tail_pc ⇒
16      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
17        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
18          Some … program_counter
19        else
20          None Word (* XXX: overflow! *)
21    ]
22  ].
23   
24definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
25  λcode_memory: BitVectorTrie Byte 16.
26  λprogram_size: nat.
27  λprogram_counter: Word.
28    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
29        nat_of_bitvector 16 program_counter < program_size.
30   
31definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
32  λcode_memory: BitVectorTrie Byte 16.
33  λtotal_program_size: nat.
34  ∀program_counter: Word.
35  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
36  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
37    match instruction with
38    [ RealInstruction instr ⇒
39      match instr with
40      [ RET                    ⇒ True
41      | JC   relative          ⇒ True (* XXX: see below *)
42      | JNC  relative          ⇒ True (* XXX: see below *)
43      | JB   bit_addr relative ⇒ True
44      | JNB  bit_addr relative ⇒ True
45      | JBC  bit_addr relative ⇒ True
46      | JZ   relative          ⇒ True
47      | JNZ  relative          ⇒ True
48      | CJNE src_trgt relative ⇒ True
49      | DJNZ src_trgt relative ⇒ True
50      | _                      ⇒
51        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
52          nat_of_bitvector … program_counter' < total_program_size
53      ]
54    | LCALL addr         ⇒
55      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
56      [ ADDR16 addr ⇒ λaddr16: True.
57          reachable_program_counter code_memory total_program_size addr ∧
58            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
59              nat_of_bitvector … program_counter' < total_program_size
60      | _ ⇒ λother: False. ⊥
61      ] (subaddressing_modein … addr)
62    | ACALL addr         ⇒
63      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
64      [ ADDR11 addr ⇒ λaddr11: True.
65        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
66        let 〈thr, eig〉 ≝ split … 3 8 addr in
67        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
68        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
69          reachable_program_counter code_memory total_program_size new_program_counter ∧
70            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
71              nat_of_bitvector … program_counter' < total_program_size
72      | _ ⇒ λother: False. ⊥
73      ] (subaddressing_modein … addr)
74    | AJMP  addr         ⇒
75      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
76      [ ADDR11 addr ⇒ λaddr11: True.
77        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
78        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
79        let bit ≝ get_index' … O ? nl in
80        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
81        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
82        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
83          reachable_program_counter code_memory total_program_size new_program_counter
84      | _ ⇒ λother: False. ⊥
85      ] (subaddressing_modein … addr)
86    | LJMP  addr         ⇒
87      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
88      [ ADDR16 addr ⇒ λaddr16: True.
89          reachable_program_counter code_memory total_program_size addr
90      | _ ⇒ λother: False. ⊥
91      ] (subaddressing_modein … addr)
92    | SJMP  addr     ⇒
93      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
94      [ RELATIVE addr ⇒ λrelative: True.
95        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
96          reachable_program_counter code_memory total_program_size new_program_counter
97      | _ ⇒ λother: False. ⊥
98      ] (subaddressing_modein … addr)
99    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
100      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
101        nat_of_bitvector … program_counter' < total_program_size
102    | MOVC  src trgt ⇒
103        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
104          nat_of_bitvector … program_counter' < total_program_size
105    ].
106  cases other
107qed.
108       
109lemma is_a_decidable:
110  ∀hd.
111  ∀element.
112    is_a hd element = true ∨ is_a hd element = false.
113  #hd #element //
114qed.
115
116lemma mem_decidable:
117  ∀n: nat.
118  ∀v: Vector addressing_mode_tag n.
119  ∀element: addressing_mode_tag.
120    mem … eq_a n v element = true ∨
121      mem … eq_a … v element = false.
122  #n #v #element //
123qed.
124
125lemma eq_a_elim:
126  ∀tag.
127  ∀hd.
128  ∀P: bool → Prop.
129    (tag = hd → P (true)) →
130      (tag ≠ hd → P (false)) →
131        P (eq_a tag hd).
132  #tag #hd #P
133  cases tag
134  cases hd
135  #true_hyp #false_hyp
136  try @false_hyp
137  try @true_hyp
138  try %
139  #absurd destruct(absurd)
140qed.
141 
142lemma is_a_true_to_is_in:
143  ∀n: nat.
144  ∀x: addressing_mode.
145  ∀tag: addressing_mode_tag.
146  ∀supervector: Vector addressing_mode_tag n.
147  mem addressing_mode_tag eq_a n supervector tag →
148    is_a tag x = true →
149      is_in … supervector x.
150  #n #x #tag #supervector
151  elim supervector
152  [1:
153    #absurd cases absurd
154  |2:
155    #n' #hd #tl #inductive_hypothesis
156    whd in match (mem … eq_a (S n') (hd:::tl) tag);
157    @eq_a_elim normalize nodelta
158    [1:
159      #tag_hd_eq #irrelevant
160      whd in match (is_in (S n') (hd:::tl) x);
161      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
162      @I
163    |2:
164      #tag_hd_neq
165      whd in match (is_in (S n') (hd:::tl) x);
166      change with (
167        mem … eq_a n' tl tag)
168          in match (fold_right … n' ? false tl);
169      #mem_hyp #is_a_hyp
170      cases(is_a hd x)
171      [1:
172        normalize nodelta //
173      |2:
174        normalize nodelta
175        @inductive_hypothesis assumption
176      ]
177    ]
178  ]
179qed.
180
181lemma is_in_subvector_is_in_supervector:
182  ∀m, n: nat.
183  ∀subvector: Vector addressing_mode_tag m.
184  ∀supervector: Vector addressing_mode_tag n.
185  ∀element: addressing_mode.
186    subvector_with … eq_a subvector supervector →
187      is_in m subvector element → is_in n supervector element.
188  #m #n #subvector #supervector #element
189  elim subvector
190  [1:
191    #subvector_with_proof #is_in_proof
192    cases is_in_proof
193  |2:
194    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
195    whd in match (is_in … (hd':::tl') element);
196    cases (is_a_decidable hd' element)
197    [1:
198      #is_a_true >is_a_true
199      #irrelevant
200      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
201      @(is_a_true_to_is_in … is_a_true)
202      lapply(subvector_with_proof)
203      cases(mem … eq_a n supervector hd') //
204    |2:
205      #is_a_false >is_a_false normalize nodelta
206      #assm
207      @inductive_hypothesis
208      [1:
209        generalize in match subvector_with_proof;
210        whd in match (subvector_with … eq_a (hd':::tl') supervector);
211        cases(mem_decidable n supervector hd')
212        [1:
213          #mem_true >mem_true normalize nodelta
214          #assm assumption
215        |2:
216          #mem_false >mem_false #absurd
217          cases absurd
218        ]
219      |2:
220        assumption
221      ]
222    ]
223  ]
224qed.
225
226let rec member_addressing_mode_tag
227  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
228    on v: Prop ≝
229  match v with
230  [ VEmpty ⇒ False
231  | VCons n' hd tl ⇒
232      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
233  ].
234 
235let rec subaddressing_mode_elim_type
236  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
237    (Q: addressing_mode → T → Prop)
238      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
239      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
240      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
241      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
242      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
243      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
244      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
245      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
246      (p_dptr:                               is_in m fixed_v DPTR              → T)
247      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
248      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
249      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
250      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
251      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
252      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
253      (p_carry:                              is_in m fixed_v CARRY             → T)
254      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
255      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
256      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
257        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
258      on v: Prop ≝
259  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
260  [ VEmpty         ⇒ λm_refl. λv_refl.
261      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
262        Q addr (
263        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
264        [ ADDR11 x          ⇒ p_addr11 x
265        | ADDR16 x          ⇒ p_addr16 x
266        | DIRECT x          ⇒ p_direct x
267        | INDIRECT x        ⇒ p_indirect x
268        | EXT_INDIRECT x    ⇒ p_ext_indirect x
269        | ACC_A             ⇒ p_acc_a
270        | REGISTER x        ⇒ p_register x
271        | ACC_B             ⇒ p_acc_b
272        | DPTR              ⇒ p_dptr
273        | DATA x            ⇒ p_data x
274        | DATA16 x          ⇒ p_data16 x
275        | ACC_DPTR          ⇒ p_acc_dptr
276        | ACC_PC            ⇒ p_acc_pc
277        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
278        | INDIRECT_DPTR     ⇒ p_indirect_dptr
279        | CARRY             ⇒ p_carry
280        | BIT_ADDR x        ⇒ p_bit_addr x
281        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
282        | RELATIVE x        ⇒ p_relative x
283        ] p)
284  | VCons n' hd tl ⇒ λm_refl. λv_refl.
285    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
286      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
287        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
288          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
289            p_bit_addr p_n_bit_addr p_relative n' tl ?
290    in
291    match hd return λa: addressing_mode_tag. a = hd → ? with
292    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
293    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
294    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
295    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
296    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
297    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
298    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
299    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
300    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
301    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
302    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
303    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
304    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
305    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
306    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
307    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
308    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
309    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
310    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
311    ] (refl … hd)
312  ] (refl … n) (refl_jmeq … v).
313  [20:
314    generalize in match proof; destruct
315    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
316    cases (mem … eq_a m fixed_v hd) normalize nodelta
317    [1:
318      whd in match (subvector_with … eq_a tl fixed_v);
319      #assm assumption
320    |2:
321      normalize in ⊢ (% → ?);
322      #absurd cases absurd
323    ]
324  ]
325  @(is_in_subvector_is_in_supervector … proof)
326  destruct @I
327qed.
328
329lemma subaddressing_mode_elim':
330  ∀T: Type[2].
331  ∀n: nat.
332  ∀o: nat.
333  ∀Q: addressing_mode → T → Prop.
334  ∀fixed_v: Vector addressing_mode_tag (n + o).
335  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
336  ∀v1: Vector addressing_mode_tag n.
337  ∀v2: Vector addressing_mode_tag o.
338  ∀fixed_v_proof: fixed_v = v1 @@ v2.
339  ∀subaddressing_mode_proof.
340    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
341      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
342  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
343  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
344  cases daemon
345qed.
346
347axiom subaddressing_mode_elim:
348  ∀T: Type[2].
349  ∀m: nat.
350  ∀n: nat.
351  ∀Q: addressing_mode → T → Prop.
352  ∀fixed_v: Vector addressing_mode_tag m.
353  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
354  ∀v: Vector addressing_mode_tag n.
355  ∀proof.
356    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
357      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
358
359definition current_instruction0 ≝
360  λcode_memory: BitVectorTrie Byte 16.
361  λprogram_counter: Word.
362    \fst (\fst (fetch … code_memory program_counter)).
363
364definition current_instruction ≝
365  λcode_memory.
366  λs: Status code_memory.
367    current_instruction0 code_memory (program_counter … s).
368
369definition ASM_classify0: instruction → status_class ≝
370  λi: instruction.
371  match i with
372   [ RealInstruction pre ⇒
373     match pre with
374      [ RET ⇒ cl_return
375      | JZ _ ⇒ cl_jump
376      | JNZ _ ⇒ cl_jump
377      | JC _ ⇒ cl_jump
378      | JNC _ ⇒ cl_jump
379      | JB _ _ ⇒ cl_jump
380      | JNB _ _ ⇒ cl_jump
381      | JBC _ _ ⇒ cl_jump
382      | CJNE _ _ ⇒ cl_jump
383      | DJNZ _ _ ⇒ cl_jump
384      | _ ⇒ cl_other
385      ]
386   | ACALL _ ⇒ cl_call
387   | LCALL _ ⇒ cl_call
388   | JMP _ ⇒ cl_call
389   | AJMP _ ⇒ cl_jump
390   | LJMP _ ⇒ cl_jump
391   | SJMP _ ⇒ cl_jump
392   | _ ⇒ cl_other
393   ].
394
395definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
396  λcode_memory.
397  λs: Status code_memory.
398    ASM_classify0 (current_instruction … s).
399
400definition current_instruction_is_labelled ≝
401  λcode_memory.
402  λcost_labels: BitVectorTrie costlabel 16.
403  λs: Status code_memory.
404  let pc ≝ program_counter … code_memory s in
405    match lookup_opt … pc cost_labels with
406    [ None ⇒ False
407    | _    ⇒ True
408    ].
409
410definition next_instruction_properly_relates_program_counters ≝
411  λcode_memory.
412  λbefore: Status code_memory.
413  λafter : Status code_memory.
414  let size ≝ current_instruction_cost code_memory before in
415  let pc_before ≝ program_counter … code_memory before in
416  let pc_after ≝ program_counter … code_memory after in
417  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
418    sum = pc_after.
419
420definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
421  λcode_memory.
422  λcost_labels.
423    mk_abstract_status
424      (Status code_memory)
425      (λs,s'. (execute_1 … s) = s')
426      (λs,class. ASM_classify … s = class)
427      (current_instruction_is_labelled … cost_labels)
428      (next_instruction_properly_relates_program_counters code_memory).
429
430let rec trace_any_label_length
431  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
432    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
433      (final_status: Status code_memory)
434      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
435        on the_trace: nat ≝
436  match the_trace with
437  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
438  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0
439  | tal_base_return the_status _ _ _ ⇒ 0
440  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
441      let tail_length ≝ trace_any_label_length … final_trace in
442      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in       
443        pc_difference + tail_length
444  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
445      let tail_length ≝ trace_any_label_length … tail_trace in
446      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
447        pc_difference + tail_length       
448  ].
449
450let rec compute_paid_trace_any_label
451  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
452    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
453      (final_status: Status code_memory)
454        (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
455       on the_trace: nat ≝
456  match the_trace with
457  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
458  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
459  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost … pre_fun_call
460  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
461     _ _ _ call_trace _ final_trace ⇒
462      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
463      let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
464        current_instruction_cost + final_trace_cost
465  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
466      let current_instruction_cost ≝ current_instruction_cost … status_pre in
467      let tail_trace_cost ≝
468       compute_paid_trace_any_label … cost_labels end_flag
469        status_init status_end tail_trace
470      in
471        current_instruction_cost + tail_trace_cost
472  ].
473
474definition compute_paid_trace_label_label ≝
475  λcode_memory: BitVectorTrie Byte 16.
476  λcost_labels: BitVectorTrie costlabel 16.
477  λtrace_ends_flag: trace_ends_with_ret.
478  λstart_status: Status code_memory.
479  λfinal_status: Status code_memory.
480  λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
481  match the_trace with
482  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
483      compute_paid_trace_any_label … given_trace
484  ].
485
486include alias "arithmetics/nat.ma".
487include alias "basics/logic.ma".
488
489lemma plus_right_monotone:
490  ∀m, n, o: nat.
491    m = n → m + o = n + o.
492  #m #n #o #refl >refl %
493qed.
494
495(* XXX: indexing bug re-emerges! *)
496example fetch_half_add:
497  ∀code_memory: BitVectorTrie Byte 16.
498  ∀cost_labels: BitVectorTrie costlabel 16.
499  ∀the_status : ASM_abstract_status code_memory cost_labels.
500    \snd (\fst (fetch code_memory (program_counter … the_status))) =
501      \snd (half_add 16 (program_counter … the_status)
502        (bitvector_of_nat … (\snd (fetch code_memory (program_counter … the_status))))).
503  cases daemon
504qed.
505
506axiom half_add_minus_right:
507  ∀size : nat.
508  ∀left : BitVector size.
509  ∀right: nat.
510  nat_of_bitvector … (\snd (half_add … left (bitvector_of_nat … right))) -
511    nat_of_bitvector … left = right.
512
513lemma minus_plus_cancel:
514  ∀m, n : nat.
515  ∀proof: n ≤ m.
516    (m - n) + n = m.
517  #m #n #proof /2 by plus_minus/
518qed.
519
520(* XXX: indexing bug *)
521example fetch_twice_fetch_execute_1:
522  ∀code_memory: BitVectorTrie Byte 16.
523  ∀start_status: Status code_memory.
524    \snd (\fst (fetch code_memory (program_counter … start_status))) =
525      program_counter … (execute_1 … start_status).
526  cases daemon
527qed. (*
528  #code_memory #start_status
529  whd in match (execute_1 code_memory start_status);
530  whd in match (execute_1' code_memory start_status); normalize nodelta
531  cases (fetch code_memory (program_counter … start_status)) #instruction_pc #ticks
532  cases instruction_pc #instruction #pc normalize nodelta *)
533
534lemma reachable_program_counter_to_0_lt_total_program_size:
535  ∀code_memory: BitVectorTrie Byte 16.
536  ∀program_counter: Word.
537  ∀total_program_size: nat.
538    reachable_program_counter code_memory total_program_size program_counter →
539      0 < total_program_size.
540  #code_memory #program_counter #total_program_size
541  whd in match reachable_program_counter; normalize nodelta * * #some_n
542  #_ cases (nat_of_bitvector 16 program_counter)
543  [1:
544    #assm assumption
545  |2:
546    #new_pc @ltn_to_ltO
547  ]
548qed.
549
550lemma trace_compute_paid_trace_cl_other:
551  ∀code_memory' : (BitVectorTrie Byte 16).
552  ∀program_counter' : Word.
553  ∀total_program_size : ℕ.
554  ∀cost_labels : (BitVectorTrie costlabel 16).
555  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
556  ∀good_program_witness : (good_program code_memory' total_program_size).
557  ∀program_size' : ℕ.
558  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
559  ∀ticks : ℕ.
560  ∀instruction : instruction.
561  ∀program_counter'' : Word.
562  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
563  ∀real_instruction : (preinstruction [[relative]]).
564  ∀real_instruction_refl : (RealInstruction … real_instruction = instruction).
565  ∀start_status : (Status code_memory').
566  ∀final_status : (Status code_memory').
567  ∀trace_ends_flag : trace_ends_with_ret.
568  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
569  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
570  ∀classify_assm: ASM_classify0 instruction = cl_other.
571  ∀pi1 : ℕ.
572   (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
573         [None ⇒ true
574         |Some _ ⇒ false
575         ] 
576    then
577      ∀start_status0:Status code_memory'.
578      ∀final_status0:Status code_memory'.
579      ∀trace_ends_flag0:trace_ends_with_ret.
580      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
581        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
582        (∃n:ℕ
583                    .trace_any_label_length code_memory' cost_labels
584                     trace_ends_flag0 start_status0 final_status0 the_trace0
585                     +S n
586                     =total_program_size)
587                   ∧pi1
588                    =compute_paid_trace_any_label code_memory' cost_labels
589                     trace_ends_flag0 start_status0 final_status0 the_trace0
590    else (pi1=O) )
591   →(∃n:ℕ
592     .trace_any_label_length code_memory' cost_labels trace_ends_flag
593      start_status final_status the_trace
594      +S n
595      =total_program_size)
596    ∧ticks+pi1
597     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
598      start_status final_status the_trace.
599  #code_memory' #program_counter' #total_program_size #cost_labels
600  #reachable_program_counter_witness #good_program_witness
601  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
602  #real_instruction #real_instruction_refl #start_status #final_status
603  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
604  #recursive_assm @(trace_any_label_inv_ind … the_trace)
605    [5:
606      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
607      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
608      #the_trace_refl
609      destruct
610      whd in match (trace_any_label_length … (tal_step_default …));
611      whd in match (compute_paid_trace_any_label … (tal_step_default …));
612      whd in costed_assm:(?%);
613      generalize in match costed_assm;
614      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
615      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
616        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
617      #lookup_assm cases lookup_assm
618      [1:
619        #None_lookup_opt_assm normalize nodelta #ignore
620        generalize in match recursive_assm;
621        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
622        [1:
623          <fetch_twice_fetch_execute_1 <FETCH %
624        |2:
625          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
626          normalize nodelta #new_recursive_assm
627          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
628            end_flag trace_any_label ?) [2: % ]
629          #exists_assm #recursive_block_cost_assm %
630          [1:
631            cases exists_assm #exists_n #total_program_size_refl
632            <total_program_size_refl
633            %{(exists_n - current_instruction_cost … status_pre)}
634            (* XXX: Christ knows what's going on with the rewrite tactic here? *)
635            cases daemon
636          |2:
637            >recursive_block_cost_assm
638            whd in match (current_instruction_cost … status_pre);
639            cut(ticks = \snd (fetch code_memory'
640               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
641            [1:
642              <FETCH %
643            |2:
644              #ticks_refl_assm >ticks_refl_assm %
645            ]
646          ]
647        ]
648      |2:
649        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
650        #absurd cases absurd #absurd cases(absurd I)
651      ]
652    |1:
653      #status_start #status_final #execute_assm #classifier_assm #costed_assm
654      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
655      destruct
656      whd in match (trace_any_label_length … (tal_base_not_return …));
657      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
658      whd in costed_assm;
659      generalize in match costed_assm;
660      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
661      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
662        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
663      #lookup_assm cases lookup_assm
664      [1:
665        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
666        #absurd cases absurd
667      |2:
668        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
669        generalize in match recursive_assm;
670        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
671        [1:
672          <fetch_twice_fetch_execute_1 <FETCH %
673        |2:
674          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
675          normalize nodelta #new_recursive_assm >new_recursive_assm %
676          [1:
677            %{(pred total_program_size)} whd in ⊢ (??%?);
678            @S_pred
679            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
680          |2:
681            cut(ticks = \snd (fetch code_memory'
682               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
683            [1:
684              <FETCH %
685            |2:
686              #ticks_refl_assm >ticks_refl_assm
687              <plus_n_O %
688            ]
689          ]
690        ]
691      ]
692    |2:
693      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
694      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
695    |3:
696      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
697      #classifier_assm #after_return_assm #trace_label_return #costed_assm
698      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
699      destruct @⊥
700    |4:
701      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
702      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
703      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
704      #final_status_refl #the_trace_refl destruct @⊥
705    ]
706  change with (ASM_classify0 ? = ?) in classifier_assm;
707  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
708  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
709  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
710qed.
711
712lemma trace_compute_paid_trace_cl_jump:
713  ∀code_memory': BitVectorTrie Byte 16.
714  ∀program_counter': Word.
715  ∀total_program_size: ℕ.
716  ∀cost_labels: BitVectorTrie costlabel 16.
717  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
718  ∀good_program_witness: good_program code_memory' total_program_size.
719  ∀first_time_around: bool.
720  ∀program_size': ℕ.
721  ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
722  ∀ticks: ℕ.
723  ∀instruction: instruction.
724  ∀program_counter'': Word.
725  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
726  ∀real_instruction: (preinstruction [[relative]]).
727  ∀real_instruction_refl: (RealInstruction … real_instruction = instruction).
728  ∀start_status: (Status code_memory').
729  ∀final_status: (Status code_memory').
730  ∀trace_ends_flag: trace_ends_with_ret.
731  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
732  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
733  ∀classify_assm: ASM_classify0 instruction = cl_jump.
734 (∀pi1:ℕ
735  .if match lookup_opt costlabel 16 program_counter' cost_labels with 
736        [None⇒true|Some _ ⇒first_time_around] 
737   then (∀start_status0:Status code_memory'
738             .∀final_status0:Status code_memory'
739              .∀trace_ends_flag0:trace_ends_with_ret
740               .∀the_trace0:trace_any_label
741                                        (ASM_abstract_status code_memory' cost_labels)
742                                        trace_ends_flag0 start_status0 final_status0
743                .program_counter'
744                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
745                 →(∃n:ℕ
746                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
747                    start_status0 final_status0 the_trace0
748                    +S n
749                    =total_program_size)
750                  ∧pi1
751                   =compute_paid_trace_any_label code_memory' cost_labels
752                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
753   else (pi1=O) 
754   →(∃n:ℕ
755     .trace_any_label_length code_memory' cost_labels trace_ends_flag
756      start_status final_status the_trace
757      +S n
758      =total_program_size)
759    ∧ticks
760     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
761      start_status final_status the_trace).
762  #code_memory' #program_counter' #total_program_size #cost_labels
763  #reachable_program_counter_witness #good_program_witness #first_time_around
764  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
765  #real_instruction #real_instruction_refl #start_status #final_status
766  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
767  #recursive_block_cost #recursive_assm
768  @(trace_any_label_inv_ind … the_trace)
769  [1:
770    #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
771    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
772    destruct
773    whd in match (trace_any_label_length … (tal_base_not_return …));
774    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
775    whd in costed_assm;
776    generalize in match costed_assm;
777    generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … start_status')) cost_labels));
778    generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' start_status')) cost_labels)
779      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
780    #lookup_assm cases lookup_assm
781    [1:
782      #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
783      #absurd cases absurd
784    |2:
785      #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
786      generalize in match recursive_assm;
787      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … start_status')))
788      [1:
789        <fetch_twice_fetch_execute_1 <FETCH %
790      |2:
791        cases daemon
792      ]
793    ]
794  |2:
795    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
796    #start_status_refl #final_status_refl #the_trace_refl destruct @⊥
797  |3:
798    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
799    #classifier_assm #after_return_assm #trace_label_return #costed_assm
800    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
801    destruct @⊥
802  |4:
803    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
804    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
805    #costed_assm #trace_any_label_return #trace_ends_flag_refl #start_status_refl
806    #final_status_refl #the_trace_refl destruct @⊥
807  |5:
808    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
809    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
810    #final_status_refl #the_trace_refl destruct @⊥
811  ]
812  change with (ASM_classify0 ? = ?) in classifier_assm;
813  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
814  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
815  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
816qed.
817
818lemma trace_compute_paid_trace_cl_call:
819  ∀code_memory' : (BitVectorTrie Byte 16).
820  ∀program_counter' : Word.
821  ∀total_program_size : ℕ.
822  ∀cost_labels : (BitVectorTrie costlabel 16).
823  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
824  ∀good_program_witness : (good_program code_memory' total_program_size).
825  ∀program_size' : ℕ.
826  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
827  ∀ticks : ℕ.
828  ∀instruction : instruction.
829  ∀program_counter'' : Word.
830  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
831  ∀real_instruction : (preinstruction [[relative]]).
832  ∀real_instruction_refl : (RealInstruction … real_instruction = instruction).
833  ∀start_status : (Status code_memory').
834  ∀final_status : (Status code_memory').
835  ∀trace_ends_flag : trace_ends_with_ret.
836  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
837  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
838  ∀classify_assm: ASM_classify0 instruction = cl_call.
839  ∀pi1 : ℕ.
840  if match lookup_opt costlabel 16 program_counter'' cost_labels with 
841        [None ⇒ true|Some _ ⇒ false] 
842   then (∀start_status0:Status code_memory'
843             .∀final_status0:Status code_memory'
844              .∀trace_ends_flag0:trace_ends_with_ret
845               .∀the_trace0:trace_any_label
846                                        (ASM_abstract_status code_memory' cost_labels)
847                                        trace_ends_flag0 start_status0 final_status0
848                .program_counter''
849                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
850                 →(∃n:ℕ
851                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
852                    start_status0 final_status0 the_trace0
853                    +S n
854                    =total_program_size)
855                  ∧pi1
856                   =compute_paid_trace_any_label code_memory' cost_labels
857                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
858   else (pi1=O) 
859   →(∃n:ℕ
860     .trace_any_label_length code_memory' cost_labels trace_ends_flag
861      start_status final_status the_trace
862      +S n
863      =total_program_size)
864    ∧ticks+pi1
865     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
866      start_status final_status the_trace.
867  #code_memory' #program_counter' #total_program_size #cost_labels
868  #reachable_program_counter_witness #good_program_witness #program_size'
869  #recursive_case #ticks #instruction #program_counter'' #FETCH #real_instruction
870  #real_instruction_refl #start_status #final_status #trace_ends_flag
871  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
872  @(trace_any_label_inv_ind … the_trace)
873  cases daemon
874qed.
875
876let rec block_cost'
877  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
878    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
879      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
880        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
881          on program_size:
882          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
883          Σcost_of_block: nat.
884          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
885            ∀start_status: Status code_memory'.
886            ∀final_status: Status code_memory'.
887            ∀trace_ends_flag.
888            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
889              program_counter' = program_counter … start_status →
890                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
891                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
892          else
893            (cost_of_block = 0) ≝
894  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
895  [ O ⇒ λbase_case. ⊥
896  | S program_size' ⇒ λrecursive_case.
897    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
898    let to_continue ≝
899      match lookup_opt … program_counter' cost_labels with
900      [ None ⇒ true
901      | Some _ ⇒ first_time_around
902      ]
903    in
904      ((if to_continue then
905       pi1 … (match instruction return λx. x = instruction → ? with
906        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
907          match real_instruction return λx. x = real_instruction →
908          Σcost_of_block: nat.
909            ∀start_status: Status code_memory'.
910            ∀final_status: Status code_memory'.
911            ∀trace_ends_flag.
912            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
913              program_counter' = program_counter … start_status →
914                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
915                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
916          [ RET                    ⇒ λinstr. ticks
917          | JC   relative          ⇒ λinstr. ticks
918          | JNC  relative          ⇒ λinstr. ticks
919          | JB   bit_addr relative ⇒ λinstr. ticks
920          | JNB  bit_addr relative ⇒ λinstr. ticks
921          | JBC  bit_addr relative ⇒ λinstr. ticks
922          | JZ   relative          ⇒ λinstr. ticks
923          | JNZ  relative          ⇒ λinstr. ticks
924          | CJNE src_trgt relative ⇒ λinstr. ticks
925          | DJNZ src_trgt relative ⇒ λinstr. ticks
926          | _                      ⇒ λinstr.
927         
928              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
929          ] (refl …)
930        | ACALL addr     ⇒ λinstr.
931            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
932        | AJMP  addr     ⇒ λinstr. ticks
933        | LCALL addr     ⇒ λinstr.
934            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
935        | LJMP  addr     ⇒ λinstr. ticks
936        | SJMP  addr     ⇒ λinstr. ticks
937        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
938            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
939        | MOVC  src trgt ⇒ λinstr.
940            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
941        ] (refl …))
942      else
943        0)
944      : Σcost_of_block: nat.
945          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
946          [ true ⇒
947            ∀start_status: Status code_memory'.
948            ∀final_status: Status code_memory'.
949            ∀trace_ends_flag.
950            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
951              program_counter' = program_counter … start_status →
952                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
953                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
954          | false ⇒
955            (cost_of_block = 0)
956          ])
957  ].
958  [1:
959    cases reachable_program_counter_witness #_ #hyp
960    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
961    @(le_to_lt_to_lt … base_case hyp)
962  |2:
963    change with (if to_continue then ? else (? = 0))
964    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
965    @pi2
966  |3:
967    change with (if to_continue then ? else (0 = 0))
968    >p normalize nodelta %
969  |98,104,107:
970    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
971    cases(block_cost' ?????????) -block_cost'
972    #recursive_block_cost #recursive_assm
973    @(trace_any_label_inv_ind … the_trace)
974    [1,6,11:
975      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
976      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
977      destruct @⊥
978    |2,7,12:
979      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
980      #start_status_refl #final_status_refl #the_trace_refl
981      destruct @⊥
982    |3,8,13:
983      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
984      #classifier_assm #after_return_assm #trace_label_return #costed_assm
985      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
986      destruct
987      whd in match (trace_any_label_length … (tal_base_call …));
988      whd in match (compute_paid_trace_any_label … (tal_base_call …));
989      whd in costed_assm;
990      generalize in match costed_assm;
991      generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
992      [1:
993        generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
994          in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
995      |2:
996        generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
997          in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
998      |3:
999        generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
1000          in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
1001      ] (* XXX: matita bug here: generalize in match ... above works OK on each
1002                individual goal, but fails when you try to do it across multiple goals
1003                with a delifting error. *)
1004      #lookup_assm cases lookup_assm
1005      [1,3,5:
1006        #None_lookup_opt normalize nodelta #absurd cases absurd
1007      |2,4,6:
1008        #costlabel #Some_lookup_opt normalize nodelta #ignore
1009        generalize in match recursive_assm;
1010        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_pre_fun_call)))
1011        [1,3,5:
1012          <fetch_twice_fetch_execute_1 <FETCH %
1013        |2,4,6: (* XXX: got to here *)
1014          #program_counter_assm >program_counter_assm <Some_lookup_opt
1015          normalize nodelta #new_recursive_assm >new_recursive_assm %
1016          [1:
1017            %{(pred total_program_size)} whd in ⊢ (??%?);
1018            @S_pred
1019            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
1020          |2:
1021            cut(ticks = \snd (fetch code_memory'
1022               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
1023            [1:
1024              <FETCH %
1025            |2:
1026              #ticks_refl_assm >ticks_refl_assm
1027              <plus_n_O %
1028            ]
1029          ]
1030        ]
1031      ]
1032    |4,9,14:
1033      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1034      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1035      #not_costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
1036      #final_status_refl #the_trace_refl
1037      destruct (* XXX: relevant *) cases daemon
1038    |5,10,15:
1039      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
1040      #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
1041      #final_status_refl #the_trace_refl
1042      destruct @⊥
1043    ]
1044    try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
1045    try (change with (ASM_classify0 ? = ?) in classifier_assm;)
1046    whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1047    whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1048    <FETCH in classifier_assm;
1049    try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd))
1050    whd in ⊢ (?(??%?)(??%?) → ?); #absurd
1051    cases absurd #absurd destruct(absurd)
1052  |4,7,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,71,74,77,80,83,86,89,
1053   92:
1054    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1055    cases(block_cost' ?????????) -block_cost'
1056    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … real_instruction_refl … the_trace program_counter_refl …)
1057    destruct %
1058  |95:
1059    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1060    cases(block_cost' ?????????) -block_cost'
1061    #recursive_block_cost #recursive_assm
1062    @(trace_any_label_inv_ind … the_trace)
1063    [5:
1064      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
1065      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
1066      #the_trace_refl
1067      destruct
1068      whd in match (trace_any_label_length … (tal_step_default …));
1069      whd in match (compute_paid_trace_any_label … (tal_step_default …));
1070      whd in costed_assm:(?%);
1071      generalize in match costed_assm;
1072      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
1073      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
1074        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
1075      #lookup_assm cases lookup_assm
1076      [1:
1077        #None_lookup_opt_assm normalize nodelta #ignore
1078        generalize in match recursive_assm;
1079        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
1080        [1:
1081          <fetch_twice_fetch_execute_1 <FETCH %
1082        |2:
1083          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
1084          normalize nodelta #new_recursive_assm
1085          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
1086            end_flag trace_any_label ?) [2: % ]
1087          #exists_assm #recursive_block_cost_assm %
1088          [1:
1089            cases exists_assm #exists_n #total_program_size_refl
1090            <total_program_size_refl
1091            %{(exists_n - current_instruction_cost … status_pre)}
1092            (* XXX: Christ knows what's going on with the rewrite tactic here? *)
1093            cases daemon
1094          |2:
1095            >recursive_block_cost_assm
1096            whd in match (current_instruction_cost … status_pre);
1097            cut(ticks = \snd (fetch code_memory'
1098               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
1099            [1:
1100              <FETCH %
1101            |2:
1102              #ticks_refl_assm >ticks_refl_assm %
1103            ]
1104          ]
1105        ]
1106      |2:
1107        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
1108        #absurd cases absurd #absurd cases(absurd I)
1109      ]
1110    |1:
1111      #status_start #status_final #execute_assm #classifier_assm #costed_assm
1112      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1113      destruct
1114      whd in match (trace_any_label_length … (tal_base_not_return …));
1115      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
1116      whd in costed_assm;
1117      generalize in match costed_assm;
1118      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
1119      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
1120        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
1121      #lookup_assm cases lookup_assm
1122      [1:
1123        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
1124        #absurd cases absurd
1125      |2:
1126        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
1127        generalize in match recursive_assm;
1128        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
1129        [1:
1130          <fetch_twice_fetch_execute_1 <FETCH %
1131        |2:
1132          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
1133          normalize nodelta #new_recursive_assm >new_recursive_assm %
1134          [1:
1135            %{(pred total_program_size)} whd in ⊢ (??%?);
1136            @S_pred
1137            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
1138          |2:
1139            cut(ticks = \snd (fetch code_memory'
1140               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
1141            [1:
1142              <FETCH %
1143            |2:
1144              #ticks_refl_assm >ticks_refl_assm
1145              <plus_n_O %
1146            ]
1147          ]
1148        ]
1149      ]
1150    |2:
1151      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
1152      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
1153    |3:
1154      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1155      #classifier_assm #after_return_assm #trace_label_return #costed_assm
1156      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1157      destruct @⊥
1158    |4:
1159      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1160      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1161      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
1162      #final_status_refl #the_trace_refl destruct @⊥
1163    ]
1164    change with (ASM_classify0 ? = ?) in classifier_assm;
1165    whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1166    whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1167    <FETCH in classifier_assm; whd in ⊢ ((??%?) → ?); #absurd destruct(absurd)
1168  |62,63,64,65,66,67,68,69,101,102,103:
1169    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1170    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
1171      reachable_program_counter_witness good_program_witness first_time_around ?)
1172    try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … real_instruction_refl … the_trace program_counter_refl …) destruct %)
1173    |2:
1174    ]
1175    cases daemon
1176  |96,99:
1177    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1178    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1179    <FETCH normalize nodelta <instr normalize nodelta *
1180    #program_counter_lt' #program_counter_lt_tps' %
1181    [1,3:
1182      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1183      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1184      >(le_to_leb_true … program_counter_lt') %
1185    |2,4:
1186      assumption
1187    ]
1188  |105:
1189    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1190    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1191    <FETCH normalize nodelta <instr normalize nodelta
1192    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1193    * * * * #n'
1194    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1195    %
1196    [1:
1197      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1198      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1199      >(le_to_leb_true … program_counter_lt') %
1200    |2:
1201      assumption
1202    ]
1203  |106:
1204    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1205    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1206    <FETCH normalize nodelta <instr normalize nodelta
1207    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1208    * * * * #n'
1209    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1210    @(transitive_le
1211      total_program_size
1212      ((S program_size') + nat_of_bitvector … program_counter')
1213      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1214    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1215    >plus_n_Sm
1216    @monotonic_le_plus_r
1217    change with (
1218      nat_of_bitvector … program_counter' <
1219        nat_of_bitvector … program_counter'')
1220    assumption
1221  |108:
1222    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1223    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1224    <FETCH normalize nodelta <instr normalize nodelta
1225    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1226    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1227    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1228    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1229    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1230    %
1231    [1:
1232      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1233      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1234      >(le_to_leb_true … program_counter_lt') %
1235    |2:
1236      assumption
1237    ]
1238  |109:
1239    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1240    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1241    <FETCH normalize nodelta <instr normalize nodelta
1242    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1243    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1244    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1245    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1246    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1247    @(transitive_le
1248      total_program_size
1249      ((S program_size') + nat_of_bitvector … program_counter')
1250      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1251    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1252    >plus_n_Sm
1253    @monotonic_le_plus_r
1254    change with (
1255      nat_of_bitvector … program_counter' <
1256        nat_of_bitvector … program_counter'')
1257    assumption
1258  |5,8,12,14,15,18,20,21,24,27,30,33,36,39,42,45,48,51,54,57,60,72,75,
1259   78,81,84,87,90,93:
1260    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1261    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1262    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1263    #program_counter_lt' #program_counter_lt_tps' %
1264    try assumption
1265    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1266    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1267    >(le_to_leb_true … program_counter_lt') %
1268  |97,100:
1269    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1270    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1271    <FETCH normalize nodelta <instr normalize nodelta
1272    try(<real_instruction_refl <instr normalize nodelta) *
1273    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1274    @(transitive_le
1275      total_program_size
1276      ((S program_size') + nat_of_bitvector … program_counter')
1277      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1278    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1279    >plus_n_Sm
1280    @monotonic_le_plus_r
1281    change with (
1282      nat_of_bitvector … program_counter' <
1283        nat_of_bitvector … program_counter'')
1284    assumption
1285  |6,9,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,73,76,79,82,85,88,91,
1286   94:
1287    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1288    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1289    <FETCH normalize nodelta
1290    <real_instruction_refl <instr normalize nodelta *
1291    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1292    @(transitive_le
1293      total_program_size
1294      ((S program_size') + nat_of_bitvector … program_counter')
1295      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1296    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1297    >plus_n_Sm
1298    @monotonic_le_plus_r
1299    change with (
1300      nat_of_bitvector … program_counter' <
1301        nat_of_bitvector … program_counter'')
1302    assumption
1303  |10:
1304    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1305    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
1306      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
1307    [1:
1308      @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness …
1309        recursive_case … instruction program_counter' … FETCH)
1310    |2:
1311    ]
1312  ]
1313qed.
1314 
1315 
1316 
1317 
1318    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1319    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1320    <FETCH normalize nodelta
1321    <real_instruction_refl <instr normalize nodelta *
1322    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1323    @(transitive_le
1324      total_program_size
1325      ((S program_size') + nat_of_bitvector … program_counter')
1326      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1327    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1328    >plus_n_Sm
1329    @monotonic_le_plus_r
1330    change with (
1331      nat_of_bitvector … program_counter' <
1332        nat_of_bitvector … program_counter'')
1333    assumption
1334  |4:
1335    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1336    cases(block_cost' ??? ? ?????) -block_cost'
1337    #recursive_block_cost #recursive_assm
1338    @(trace_any_label_inv_ind … the_trace)
1339    [1:
1340      #status_start #status_final #execute_assm #classifier_assm #costed_assm
1341      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1342      destruct
1343      whd in match (trace_any_label_length … (tal_base_not_return …));
1344      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
1345      whd in costed_assm;
1346    |2:
1347      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
1348      #start_status_refl #final_status_refl #the_trace_assm destruct
1349      whd in classifier_assm;
1350      whd in classifier_assm:(??%?);
1351      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1352      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1353      @⊥ <FETCH in classifier_assm; normalize nodelta
1354      #absurd destruct(absurd)
1355    |3:
1356      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1357      #classifier_assm #after_return_assm #trace_label_return #costed_assm
1358      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1359      destruct
1360      whd in classifier_assm;
1361      whd in classifier_assm:(??%?);
1362      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1363      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1364      @⊥ <FETCH in classifier_assm; normalize nodelta
1365      #absurd destruct(absurd)
1366    |4:
1367      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1368      #status_final #execute_assm #classifier_assm #after_return_assm
1369      #trace_label_return #costed_assm #trace_any_label #ends_flag_refl
1370      #start_status_refl #final_status_refl #the_trace_refl
1371      destruct
1372      whd in classifier_assm;
1373      whd in classifier_assm:(??%?);
1374      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1375      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1376      @⊥ <FETCH in classifier_assm; normalize nodelta
1377      #absurd destruct(absurd)
1378    ]
1379   
1380   
1381   
1382   
1383   
1384   
1385   
1386   
1387   
1388   
1389   
1390   
1391   
1392   
1393   
1394   
1395   
1396   
1397   
1398   
1399   
1400   
1401   
1402   
1403   
1404   
1405   
1406   
1407   
1408    |3:
1409      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1410      #classifier_assm #after_return_assm #trace_label_return #costed_assm
1411      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1412      destruct
1413      whd in match (compute_paid_trace_any_label … (tal_base_call …));
1414      whd in match (trace_any_label_length … (tal_base_call …));
1415      cases(recursive_assm …
1416        (tal_base_call (ASM_abstract_status code_memory' cost_labels)
1417         status_pre_fun_call (execute_1 … status_pre_fun_call) status_final (refl …)
1418         classifier_assm after_return_assm trace_label_return costed_assm) ?)
1419      [1:
1420        * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
1421        [1:
1422          %{(pred total_program_size)}
1423          whd in ⊢ (??%?);
1424          >S_pred [1: % ]
1425          <recursive_trace_total
1426          @lt_O_S
1427        |2:
1428          >recursive_block_cost_assm
1429          whd in ⊢ (??(??%)?); <FETCH
1430          (* XXX: ??? *)
1431        ]
1432      |2:
1433        cut(program_counter'' = \snd (\fst (fetch code_memory' (program_counter … status_pre_fun_call))))
1434        [1:
1435          cases FETCH %
1436        |2:
1437          #program_counter_hyp'' >program_counter_hyp''
1438          whd in after_return_assm; <after_return_assm
1439          whd in match (current_instruction_cost status_pre_fun_call);
1440          @fetch_half_add
1441        ]
1442      ]
1443    |4:
1444      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1445      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1446      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
1447      #final_status_refl #the_trace_refl
1448      generalize in match execute_assm; destruct #execute_assm
1449      whd in match (compute_paid_trace_any_label … (tal_step_call …));
1450      whd in match (trace_any_label_length … (tal_step_call …));
1451      cases(recursive_assm status_after_fun_call status_final end_flag trace_any_label ? ?)
1452      [1:
1453        * #recursive_n #recursive_trace_total #recursive_block_cost_assm %
1454        [1:
1455          <recursive_trace_total %
1456          [1:
1457            @(recursive_n - (current_instruction_cost status_pre_fun_call))
1458          |2:
1459            whd in after_return_assm; cases after_return_assm
1460            >half_add_minus_right in ⊢ (??%?);
1461            >commutative_plus in ⊢ (???%);
1462            >commutative_plus in ⊢ (??%?);
1463            <associative_plus in ⊢ (??%?);
1464            @plus_right_monotone
1465            cut(current_instruction_cost status_pre_fun_call ≤ recursive_n)
1466            [1:
1467              (* XXX: ??? *)
1468            |2:
1469              #current_instruction_cost_assm
1470              <minus_Sn_m in ⊢ (??%?); [2: assumption ]
1471              >minus_plus_cancel [1: % ]
1472              @le_S assumption
1473            ]
1474          ]
1475        |2:
1476          >recursive_block_cost_assm
1477          @plus_right_monotone
1478          whd in match (current_instruction_cost status_pre_fun_call);
1479          <FETCH %
1480        ]
1481     
1482      |2:
1483        lapply (trace_label_return_preserves_code_memory … (execute_1 status_pre_fun_call) status_after_fun_call)
1484        #hyp cases (hyp trace_label_return)
1485        @as_execute_preserves_code_memory whd %
1486      |3:
1487        cut(program_counter'' = \snd (\fst (fetch (code_memory … status_pre_fun_call) (program_counter … status_pre_fun_call))))
1488        [1:
1489          cases FETCH %
1490        |2:
1491          #program_counter_hyp'' >program_counter_hyp''
1492          whd in after_return_assm; <after_return_assm
1493          whd in match (current_instruction_cost status_pre_fun_call);
1494          @fetch_half_add
1495        ]
1496      ]
1497    |5:
1498      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace'
1499      #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
1500      #final_status_refl #trace_refl
1501      generalize in match the_trace; destruct #the_trace
1502      whd in classifier_assm;
1503      whd in classifier_assm:(??%?);
1504      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1505      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1506      @⊥ <FETCH in classifier_assm; normalize nodelta
1507      #absurd destruct(absurd)
1508    ]
1509  |7,8,9,10,13,16,19,22,25,28,31,34,37,40,41,42,43,44,45,46,47,48,49,52,55,58,61,
1510    64,67,70,73,76,79,82,85,88,91,94,97,100,101,104,108,107:
1511    cases daemon (* XXX: massive terms *)
1512  |2:
1513    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1514    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1515    <FETCH normalize nodelta <instr normalize nodelta
1516    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1517    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1518    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1519    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1520    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1521    @(transitive_le
1522      total_program_size
1523      ((S program_size') + nat_of_bitvector … program_counter')
1524      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1525    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1526    >plus_n_Sm
1527    @monotonic_le_plus_r
1528    change with (
1529      nat_of_bitvector … program_counter' <
1530        nat_of_bitvector … program_counter'')
1531    assumption
1532  |3:
1533    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1534    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1535    <FETCH normalize nodelta <instr normalize nodelta
1536    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1537    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1538    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1539    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1540    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1541    %
1542    [1:
1543      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1544      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1545      >(le_to_leb_true … program_counter_lt') %
1546    |2:
1547      assumption
1548    ]
1549  |5:
1550    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1551    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1552      <FETCH normalize nodelta <instr normalize nodelta
1553    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1554    * * * * #n'
1555    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1556    @(transitive_le
1557      total_program_size
1558      ((S program_size') + nat_of_bitvector … program_counter')
1559      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1560    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1561    >plus_n_Sm
1562    @monotonic_le_plus_r
1563    change with (
1564      nat_of_bitvector … program_counter' <
1565        nat_of_bitvector … program_counter'')
1566    assumption
1567  |6:
1568    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1569    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1570      <FETCH normalize nodelta <instr normalize nodelta
1571    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1572    * * * * #n'
1573    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1574    %
1575    [1:
1576      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1577      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1578      >(le_to_leb_true … program_counter_lt') %
1579    |2:
1580      assumption
1581    ]
1582  |11,14: (* JMP and MOVC *)
1583    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1584    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1585    <FETCH normalize nodelta <instr normalize nodelta
1586    try(<real_instruction_refl <instr normalize nodelta) *
1587    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1588    @(transitive_le
1589      total_program_size
1590      ((S program_size') + nat_of_bitvector … program_counter')
1591      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1592    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1593    >plus_n_Sm
1594    @monotonic_le_plus_r
1595    change with (
1596      nat_of_bitvector … program_counter' <
1597        nat_of_bitvector … program_counter'')
1598    assumption
1599  |12,15:
1600    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1601    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1602    <FETCH normalize nodelta <instr normalize nodelta *
1603    #program_counter_lt' #program_counter_lt_tps' %
1604    [1,3:
1605      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1606      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1607      >(le_to_leb_true … program_counter_lt') %
1608    |2,4:
1609      assumption
1610    ]
1611  |17,20,23,26,29,32,35,38,50,53,56,59,62,65,68,71,74,77,80,83,86,89,92,95,98,
1612   102,105:
1613    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1614    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1615    <FETCH normalize nodelta
1616    <real_instruction_refl <instr normalize nodelta *
1617    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1618    @(transitive_le
1619      total_program_size
1620      ((S program_size') + nat_of_bitvector … program_counter')
1621      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1622    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1623    >plus_n_Sm
1624    @monotonic_le_plus_r
1625    change with (
1626      nat_of_bitvector … program_counter' <
1627        nat_of_bitvector … program_counter'')
1628    assumption
1629  |18,21,24,27,30,33,36,39,51,54,57,60,63,66,69,72,75,78,
1630    81,84,87,90,93,96,99,103,106:
1631    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1632    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1633    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1634    #program_counter_lt' #program_counter_lt_tps' %
1635    try assumption
1636    [*:
1637      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1638      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1639      >(le_to_leb_true … program_counter_lt') %
1640    ]
1641  [1:
1642    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
1643    cases(block_cost' ?????? ?? ?) -block_cost'
1644    #recursive_block_cost #recursive_assm
1645    @(trace_any_label_inv_ind … the_trace)
1646    [1:
1647      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
1648      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
1649      cases classifier_assm
1650      whd in match (as_classifier ? ? ?);
1651      whd in ⊢ (??%? → ?);
1652      whd in match current_instruction; normalize nodelta
1653      whd in match current_instruction0; normalize nodelta
1654      #absurd @⊥ >p1 in absurd; normalize nodelta
1655      #absurd destruct(absurd)
1656    |2:
1657      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
1658      #start_status_refl #final_status_refl #the_trace_assm destruct
1659      whd in classifier_assm;
1660      whd in classifier_assm:(??%?);
1661      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1662      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1663      @⊥
1664      >p1 in classifier_assm; normalize nodelta
1665      #absurd destruct(absurd)
1666    |3:
1667      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1668      #classifier_assm #after_return_assm #trace_label_return #costed_assm
1669      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1670      destruct
1671      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
1672        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
1673          (execute_1 status_pre_fun_call) status_final
1674          (refl Status (execute_1 status_pre_fun_call)) classifier_assm
1675          after_return_assm trace_label_return costed_assm) ? ?)
1676      [2: %
1677      |3:
1678      |1:
1679      ]
1680    |4:
1681      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1682      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1683      #costed_assm #trace_any_label #trace_ends_refl #start_status_refl #final_status_refl
1684      #the_trace_refl destruct whd in ⊢ (??(???%)); whd in match (trace_any_label_length … (tal_step_call … trace_any_label));
1685    |5:
1686      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace
1687      #classifier_assm #costed_assm #ends_flag_refl #start_status_refl #final_status_refl
1688      #the_trace_refl -the_trace_refl destruct
1689      whd in classifier_assm;
1690      whd in classifier_assm:(??%?);
1691      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1692      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
1693      @⊥ >p1 in classifier_assm; normalize nodelta
1694      #absurd destruct(absurd)
1695    ]
1696  [1:
1697    #start_status #final_status #trace_ends_flag #the_trace
1698    #code_memory_refl #program_counter_refl
1699    cases(block_cost' ?????? ?? ?) -block_cost'
1700    #recursive_block_cost #recursive_assm
1701    @(trace_any_label_inv_ind … the_trace)
1702    [1:
1703      #start_status' #final_status' #execute_assm #not_return_assm
1704      #costed_assm #trace_ends_flag_assm #start_status_assm #final_status_assm
1705      #the_trace_assm
1706      cases daemon (* XXX: bug in notion of traces here *)
1707    |2:
1708
1709    |3:
1710      cases daemon (* XXX *)
1711    |4:
1712    ]
1713  |108:
1714    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1715    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1716    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1717    #program_counter_lt' #program_counter_lt_tps' %
1718    try assumption
1719    [*:
1720      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1721      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1722      >(le_to_leb_true … program_counter_lt') %
1723    ]
1724  [1:
1725    cases reachable_program_counter_witness #_ #hyp
1726    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
1727    @(le_to_lt_to_lt … base_case hyp)
1728  |2:
1729    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1730    lapply(good_program_witness program_counter reachable_program_counter_witness)
1731      <FETCH normalize nodelta <instr normalize nodelta
1732    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1733    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
1734    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1735    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1736    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1737    @(transitive_le
1738      total_program_size
1739      ((S program_size') + nat_of_bitvector … program_counter)
1740      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1741    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1742    >plus_n_Sm
1743    @monotonic_le_plus_r
1744    change with (
1745      nat_of_bitvector … program_counter <
1746        nat_of_bitvector … program_counter')
1747    assumption
1748  |3:
1749    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1750    lapply(good_program_witness program_counter reachable_program_counter_witness)
1751      <FETCH normalize nodelta <instr normalize nodelta
1752    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1753    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
1754    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1755    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1756    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1757    %
1758    [1:
1759      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1760      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1761      >(le_to_leb_true … program_counter_lt') %
1762    |2:
1763      assumption
1764    ]
1765  |4:
1766    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1767    lapply(good_program_witness program_counter reachable_program_counter_witness)
1768      <FETCH normalize nodelta <instr normalize nodelta
1769    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1770    * * * * #n'
1771    #_ #_ #program_counter_lt' #program_counter_lt_tps'     
1772    @(transitive_le
1773      total_program_size
1774      ((S program_size') + nat_of_bitvector … program_counter)
1775      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1776    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1777    >plus_n_Sm
1778    @monotonic_le_plus_r
1779    change with (
1780      nat_of_bitvector … program_counter <
1781        nat_of_bitvector … program_counter')
1782    assumption
1783  |5:
1784    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1785    lapply(good_program_witness program_counter reachable_program_counter_witness)
1786      <FETCH normalize nodelta <instr normalize nodelta
1787    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1788    * * * * #n'
1789    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1790    %
1791    [1:
1792      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1793      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1794      >(le_to_leb_true … program_counter_lt') %
1795    |2:
1796      assumption
1797    ]
1798  |6,8: (* JMP and MOVC *)
1799    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1800    lapply(good_program_witness program_counter reachable_program_counter_witness)
1801    <FETCH normalize nodelta <instr normalize nodelta
1802    try(<real_instruction_refl <instr normalize nodelta) *
1803    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1804    @(transitive_le
1805      total_program_size
1806      ((S program_size') + nat_of_bitvector … program_counter)
1807      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1808    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1809    >plus_n_Sm
1810    @monotonic_le_plus_r
1811    change with (
1812      nat_of_bitvector … program_counter <
1813        nat_of_bitvector … program_counter')
1814    assumption
1815  |7,9:
1816    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1817    lapply(good_program_witness program_counter reachable_program_counter_witness)
1818    <FETCH normalize nodelta <instr normalize nodelta *
1819    #program_counter_lt' #program_counter_lt_tps' %
1820    [1,3:
1821      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1822      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1823      >(le_to_leb_true … program_counter_lt') %
1824    |2,4:
1825      assumption
1826    ]
1827  |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
1828    55,57,59,61,63:
1829    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1830    lapply(good_program_witness program_counter reachable_program_counter_witness)
1831    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1832    #program_counter_lt' #program_counter_lt_tps' %
1833    try assumption
1834    [*:
1835      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1836      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1837      >(le_to_leb_true … program_counter_lt') %
1838    ]
1839  |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
1840    54,56,58,60,62:
1841    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1842    lapply(good_program_witness program_counter reachable_program_counter_witness)
1843    <FETCH normalize nodelta
1844    <real_instruction_refl <instr normalize nodelta *
1845    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1846    @(transitive_le
1847      total_program_size
1848      ((S program_size') + nat_of_bitvector … program_counter)
1849      (program_size' + nat_of_bitvector … program_counter') recursive_case)
1850    normalize in match (S program_size' + nat_of_bitvector … program_counter);
1851    >plus_n_Sm
1852    @monotonic_le_plus_r
1853    change with (
1854      nat_of_bitvector … program_counter <
1855        nat_of_bitvector … program_counter')
1856    assumption
1857  ]
1858qed.
1859
1860definition block_cost ≝
1861  λcode_memory: BitVectorTrie Byte 16.
1862  λprogram_counter: Word.
1863  λtotal_program_size: nat.
1864  λcost_labels: BitVectorTrie costlabel 16.
1865  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1866  λgood_program_witness: good_program code_memory total_program_size.
1867    block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1868      reachable_program_counter_witness good_program_witness true ?.
1869  @le_plus_n_r
1870qed.
1871
1872lemma fetch_program_counter_n_Sn:
1873  ∀instruction: instruction.
1874  ∀program_counter, program_counter': Word.
1875  ∀ticks, n: nat.
1876  ∀code_memory: BitVectorTrie Byte 16.
1877    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
1878      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
1879        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
1880          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
1881  #instruction #program_counter #program_counter' #ticks #n #code_memory
1882  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
1883  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
1884  <fetch_program_counter_n_hyp normalize nodelta
1885  <fetch_hyp normalize nodelta
1886  change with (
1887    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
1888  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
1889  >(le_to_leb_true … lt_hyp) %
1890qed.
1891
1892let rec traverse_code_internal
1893  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
1894    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
1895      (reachable_program_counter_witness:
1896          ∀lbl: costlabel.
1897          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1898            reachable_program_counter code_memory fixed_program_size program_counter)
1899        (good_program_witness: good_program code_memory fixed_program_size)
1900        on program_size: identifier_map CostTag nat ≝
1901  match program_size with
1902  [ O ⇒ empty_map …
1903  | S program_size ⇒
1904    let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
1905    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
1906    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with
1907    [ None ⇒ λlookup_refl. cost_mapping
1908    | Some lbl ⇒ λlookup_refl.
1909      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
1910        add … cost_mapping lbl cost
1911    ] (refl … (lookup_opt … program_counter cost_labels))
1912  ].
1913  [1:
1914    @(reachable_program_counter_witness lbl)
1915    assumption
1916  |2:
1917    assumption
1918  ]
1919qed.
1920
1921definition traverse_code ≝
1922  λcode_memory: BitVectorTrie Byte 16.
1923  λcost_labels: BitVectorTrie costlabel 16.
1924  λprogram_size: nat.
1925  λreachable_program_counter_witness:
1926          ∀lbl: costlabel.
1927          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1928            reachable_program_counter code_memory program_size program_counter.
1929  λgood_program_witness: good_program code_memory program_size.
1930    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
1931 
1932definition compute_costs ≝
1933  λprogram: list Byte.
1934  λcost_labels: BitVectorTrie costlabel 16.
1935  λreachable_program_witness.
1936  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
1937    let program_size ≝ |program| + 1 in
1938    let code_memory ≝ load_code_memory program in
1939      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
1940  @good_program_witness
1941qed.
Note: See TracBrowser for help on using the repository browser.