source: src/ASM/ASMCosts.ma @ 1696

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

finished adding russell types to the traverse_cost_* functions

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