source: src/ASM/ASMCosts.ma @ 1692

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

resolved conflict in asm costs this morning

File size: 64.2 KB
RevLine 
[1486]1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
[1560]5include "common/StructuredTraces.ma".
[1486]6
[1642]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  ].
[1621]23   
[1642]24definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
[1621]25  λcode_memory: BitVectorTrie Byte 16.
[1639]26  λprogram_size: nat.
[1621]27  λprogram_counter: Word.
[1642]28    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
29        nat_of_bitvector 16 program_counter < program_size.
[1639]30   
[1642]31definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
[1621]32  λcode_memory: BitVectorTrie Byte 16.
33  λtotal_program_size: nat.
[1642]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
[1621]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      | _                      ⇒
[1642]51        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
52          nat_of_bitvector … program_counter' < total_program_size
[1621]53      ]
54    | LCALL addr         ⇒
55      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
56      [ ADDR16 addr ⇒ λaddr16: True.
[1642]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
[1621]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.
[1642]65        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
[1621]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
[1642]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
[1621]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.
[1642]77        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
[1621]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
[1642]83          reachable_program_counter code_memory total_program_size new_program_counter
[1621]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.
[1642]89          reachable_program_counter code_memory total_program_size addr
[1621]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.
[1642]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
[1621]97      | _ ⇒ λother: False. ⊥
98      ] (subaddressing_modein … addr)
[1645]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
[1621]102    | MOVC  src trgt ⇒
[1642]103        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
104          nat_of_bitvector … program_counter' < total_program_size
[1621]105    ].
106  cases other
107qed.
[1648]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
[1650]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:
[1648]143  ∀n: nat.
[1650]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.
[1648]180
181lemma is_in_subvector_is_in_supervector:
[1625]182  ∀m, n: nat.
183  ∀subvector: Vector addressing_mode_tag m.
[1648]184  ∀supervector: Vector addressing_mode_tag n.
[1646]185  ∀element: addressing_mode.
[1625]186    subvector_with … eq_a subvector supervector →
187      is_in m subvector element → is_in n supervector element.
[1648]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:
[1650]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)
[1648]197    [1:
[1650]198      #is_a_true >is_a_true
[1648]199      #irrelevant
[1650]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') //
[1648]204    |2:
205      #is_a_false >is_a_false normalize nodelta
206      #assm
207      @inductive_hypothesis
208      [1:
[1650]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')
[1648]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    ]
[1650]223  ]
[1648]224qed.
[1625]225
[1622]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 ⇒
[1623]232      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
[1622]233  ].
234 
235let rec subaddressing_mode_elim_type
[1625]236  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
[1622]237    (Q: addressing_mode → T → Prop)
[1625]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
[1623]260  [ VEmpty         ⇒ λm_refl. λv_refl.
[1625]261      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
[1623]262        Q addr (
[1625]263        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
[1624]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
[1623]277        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
[1624]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
[1623]283        ] p)
284  | VCons n' hd tl ⇒ λm_refl. λv_refl.
[1625]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 ?
[1623]290    in
291    match hd return λa: addressing_mode_tag. a = hd → ? with
[1624]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
[1623]305    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
[1624]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
[1622]311    ] (refl … hd)
[1624]312  ] (refl … n) (refl_jmeq … v).
313  [20:
[1625]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  ]
[1646]325  @(is_in_subvector_is_in_supervector … proof)
[1625]326  destruct @I
[1623]327qed.
[1621]328
[1645]329lemma subaddressing_mode_elim':
[1624]330  ∀T: Type[2].
[1645]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].
[1625]349  ∀m: nat.
[1645]350  ∀n: nat.
351  ∀Q: addressing_mode → T → Prop.
[1625]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.
[1624]354  ∀v: Vector addressing_mode_tag n.
[1625]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.
[1624]358
[1658]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 ≝
[1669]365  λcode_memory.
366  λs: Status code_memory.
367    current_instruction0 code_memory (program_counter … s).
[1658]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
[1669]395definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
396  λcode_memory.
397  λs: Status code_memory.
398    ASM_classify0 (current_instruction … s).
[1658]399
400definition current_instruction_is_labelled ≝
[1669]401  λcode_memory.
[1658]402  λcost_labels: BitVectorTrie costlabel 16.
[1669]403  λs: Status code_memory.
404  let pc ≝ program_counter … code_memory s in
[1658]405    match lookup_opt … pc cost_labels with
406    [ None ⇒ False
407    | _    ⇒ True
408    ].
409
410definition next_instruction_properly_relates_program_counters ≝
[1669]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
[1658]417  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
418    sum = pc_after.
419
[1669]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).
[1658]429
430let rec trace_any_label_length
[1669]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)
[1658]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
[1669]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)
[1658]455       on the_trace: nat ≝
456  match the_trace with
[1669]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
[1658]460  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
461     _ _ _ call_trace _ final_trace ⇒
[1669]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
[1658]464        current_instruction_cost + final_trace_cost
465  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
[1669]466      let current_instruction_cost ≝ current_instruction_cost … status_pre in
[1658]467      let tail_trace_cost ≝
[1669]468       compute_paid_trace_any_label … cost_labels end_flag
[1658]469        status_init status_end tail_trace
470      in
471        current_instruction_cost + tail_trace_cost
472  ].
473
474definition compute_paid_trace_label_label ≝
[1669]475  λcode_memory: BitVectorTrie Byte 16.
476  λcost_labels: BitVectorTrie costlabel 16.
[1658]477  λtrace_ends_flag: trace_ends_with_ret.
[1669]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.
[1658]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
[1622]486include alias "arithmetics/nat.ma".
[1658]487include alias "basics/logic.ma".
[1622]488
[1663]489lemma plus_right_monotone:
490  ∀m, n, o: nat.
491    m = n → m + o = n + o.
492  #m #n #o #refl >refl %
493qed.
[1658]494
[1665]495(* XXX: indexing bug re-emerges! *)
496example fetch_half_add:
[1669]497  ∀code_memory: BitVectorTrie Byte 16.
[1665]498  ∀cost_labels: BitVectorTrie costlabel 16.
[1669]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))))).
[1665]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
[1669]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
[1684]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:
[1669]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  ∀start_status : (Status code_memory').
564  ∀final_status : (Status code_memory').
565  ∀trace_ends_flag : trace_ends_with_ret.
566  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
567  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
568  ∀classify_assm: ASM_classify0 instruction = cl_other.
569  ∀pi1 : ℕ.
570   (if match lookup_opt costlabel 16 program_counter'' cost_labels with 
571         [None ⇒ true
572         |Some _ ⇒ false
573         ] 
574    then
575      ∀start_status0:Status code_memory'.
576      ∀final_status0:Status code_memory'.
577      ∀trace_ends_flag0:trace_ends_with_ret.
578      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
579        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
580        (∃n:ℕ
581                    .trace_any_label_length code_memory' cost_labels
582                     trace_ends_flag0 start_status0 final_status0 the_trace0
583                     +S n
584                     =total_program_size)
585                   ∧pi1
586                    =compute_paid_trace_any_label code_memory' cost_labels
587                     trace_ends_flag0 start_status0 final_status0 the_trace0
588    else (pi1=O) )
589   →(∃n:ℕ
590     .trace_any_label_length code_memory' cost_labels trace_ends_flag
591      start_status final_status the_trace
592      +S n
593      =total_program_size)
594    ∧ticks+pi1
595     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
596      start_status final_status the_trace.
597  #code_memory' #program_counter' #total_program_size #cost_labels
598  #reachable_program_counter_witness #good_program_witness
599  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
[1691]600  #start_status #final_status
[1669]601  #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
[1692]602  #recursive_assm
603  @(trace_any_label_inv_ind … the_trace)
[1669]604    [5:
605      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
606      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
607      #the_trace_refl
608      destruct
609      whd in match (trace_any_label_length … (tal_step_default …));
610      whd in match (compute_paid_trace_any_label … (tal_step_default …));
611      whd in costed_assm:(?%);
612      generalize in match costed_assm;
613      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
614      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
615        in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
616      #lookup_assm cases lookup_assm
617      [1:
618        #None_lookup_opt_assm normalize nodelta #ignore
619        generalize in match recursive_assm;
620        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 code_memory' status_pre)))
621        [1:
622          <fetch_twice_fetch_execute_1 <FETCH %
623        |2:
624          #program_counter_assm >program_counter_assm <None_lookup_opt_assm
625          normalize nodelta #new_recursive_assm
626          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
627            end_flag trace_any_label ?) [2: % ]
628          #exists_assm #recursive_block_cost_assm %
629          [1:
630            cases exists_assm #exists_n #total_program_size_refl
631            <total_program_size_refl
632            %{(exists_n - current_instruction_cost … status_pre)}
[1684]633            (* XXX: Christ knows what's going on with the rewrite tactic here? *)
634            cases daemon
[1669]635          |2:
636            >recursive_block_cost_assm
637            whd in match (current_instruction_cost … status_pre);
638            cut(ticks = \snd (fetch code_memory'
639               (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
640            [1:
641              <FETCH %
642            |2:
643              #ticks_refl_assm >ticks_refl_assm %
644            ]
645          ]
646        ]
647      |2:
648        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta
649        #absurd cases absurd #absurd cases(absurd I)
650      ]
651    |1:
652      #status_start #status_final #execute_assm #classifier_assm #costed_assm
653      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
654      destruct
655      whd in match (trace_any_label_length … (tal_base_not_return …));
656      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
657      whd in costed_assm;
658      generalize in match costed_assm;
659      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
660      generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
661        in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
662      #lookup_assm cases lookup_assm
663      [1:
664        #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm
665        #absurd cases absurd
666      |2:
667        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
668        generalize in match recursive_assm;
669        cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' (execute_1 … status_start)))
670        [1:
671          <fetch_twice_fetch_execute_1 <FETCH %
672        |2:
673          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
674          normalize nodelta #new_recursive_assm >new_recursive_assm %
675          [1:
676            %{(pred total_program_size)} whd in ⊢ (??%?);
677            @S_pred
[1684]678            @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
[1669]679          |2:
680            cut(ticks = \snd (fetch code_memory'
681               (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
682            [1:
683              <FETCH %
684            |2:
685              #ticks_refl_assm >ticks_refl_assm
686              <plus_n_O %
687            ]
688          ]
689        ]
690      ]
691    |2:
692      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
693      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
694    |3:
695      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
696      #classifier_assm #after_return_assm #trace_label_return #costed_assm
697      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
698      destruct @⊥
[1684]699    |4:
700      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
701      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
702      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
703      #final_status_refl #the_trace_refl destruct @⊥
[1669]704    ]
[1684]705  change with (ASM_classify0 ? = ?) in classifier_assm;
706  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
707  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
708  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
[1669]709qed.
710
[1684]711lemma trace_compute_paid_trace_cl_jump:
712  ∀code_memory': BitVectorTrie Byte 16.
713  ∀program_counter': Word.
714  ∀total_program_size: ℕ.
715  ∀cost_labels: BitVectorTrie costlabel 16.
716  ∀reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter'.
717  ∀good_program_witness: good_program code_memory' total_program_size.
718  ∀first_time_around: bool.
719  ∀program_size': ℕ.
720  ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
721  ∀ticks: ℕ.
722  ∀instruction: instruction.
723  ∀program_counter'': Word.
724  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch code_memory' program_counter'.
725  ∀start_status: (Status code_memory').
726  ∀final_status: (Status code_memory').
727  ∀trace_ends_flag: trace_ends_with_ret.
728  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
729  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
730  ∀classify_assm: ASM_classify0 instruction = cl_jump.
[1691]731   (∃n:ℕ
[1684]732     .trace_any_label_length code_memory' cost_labels trace_ends_flag
733      start_status final_status the_trace
734      +S n
735      =total_program_size)
736    ∧ticks
737     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
[1691]738      start_status final_status the_trace.
[1684]739  #code_memory' #program_counter' #total_program_size #cost_labels
740  #reachable_program_counter_witness #good_program_witness #first_time_around
741  #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
[1691]742  #start_status #final_status
[1684]743  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
744  @(trace_any_label_inv_ind … the_trace)
[1692]745  [5:
746    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
747    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
748    #the_trace_refl destruct @⊥
749  |1:
750    #status_start #status_final #execute_assm #classifier_assm #costed_assm
[1684]751    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
752    destruct
753    whd in match (trace_any_label_length … (tal_base_not_return …));
[1692]754    whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); %
[1684]755    [1:
[1692]756      %{(pred total_program_size)} whd in ⊢ (??%?);
757      @S_pred
758      @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
[1684]759    |2:
[1692]760      <FETCH %
[1684]761    ]
762  |2:
[1692]763    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
764    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
[1684]765  |3:
766    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
767    #classifier_assm #after_return_assm #trace_label_return #costed_assm
[1692]768    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
[1684]769    destruct @⊥
770  |4:
771    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
772    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
[1692]773    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
[1684]774    #final_status_refl #the_trace_refl destruct @⊥
775  ]
776  change with (ASM_classify0 ? = ?) in classifier_assm;
777  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
778  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
779  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
780qed.
781
782lemma trace_compute_paid_trace_cl_call:
783  ∀code_memory' : (BitVectorTrie Byte 16).
784  ∀program_counter' : Word.
785  ∀total_program_size : ℕ.
786  ∀cost_labels : (BitVectorTrie costlabel 16).
787  ∀reachable_program_counter_witness : (reachable_program_counter code_memory' total_program_size program_counter').
788  ∀good_program_witness : (good_program code_memory' total_program_size).
789  ∀program_size' : ℕ.
790  ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
791  ∀ticks : ℕ.
792  ∀instruction : instruction.
793  ∀program_counter'' : Word.
794  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch code_memory' program_counter').
795  ∀start_status : (Status code_memory').
796  ∀final_status : (Status code_memory').
797  ∀trace_ends_flag : trace_ends_with_ret.
798  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
799  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
800  ∀classify_assm: ASM_classify0 instruction = cl_call.
[1692]801  (∀pi1:ℕ
802  .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
803      [None ⇒ true | Some _ ⇒ false] 
[1684]804   then (∀start_status0:Status code_memory'
805             .∀final_status0:Status code_memory'
806              .∀trace_ends_flag0:trace_ends_with_ret
807               .∀the_trace0:trace_any_label
808                                        (ASM_abstract_status code_memory' cost_labels)
809                                        trace_ends_flag0 start_status0 final_status0
810                .program_counter''
811                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
812                 →(∃n:ℕ
813                   .trace_any_label_length code_memory' cost_labels trace_ends_flag0
814                    start_status0 final_status0 the_trace0
815                    +S n
816                    =total_program_size)
817                  ∧pi1
818                   =compute_paid_trace_any_label code_memory' cost_labels
819                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
820   else (pi1=O) 
821   →(∃n:ℕ
822     .trace_any_label_length code_memory' cost_labels trace_ends_flag
823      start_status final_status the_trace
824      +S n
825      =total_program_size)
826    ∧ticks+pi1
827     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
[1692]828      start_status final_status the_trace).
[1684]829  #code_memory' #program_counter' #total_program_size #cost_labels
830  #reachable_program_counter_witness #good_program_witness #program_size'
[1691]831  #recursive_case #ticks #instruction #program_counter'' #FETCH
832  #start_status #final_status #trace_ends_flag
[1684]833  #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
834  @(trace_any_label_inv_ind … the_trace)
[1692]835  [5:
836    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
837    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
838    #the_trace_refl destruct @⊥
839  |1:
840    #status_start #status_final #execute_assm #classifier_assm #costed_assm
841    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
842    destruct @⊥
843  |2:
844    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
845    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
846  |3:
847    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
848    #classifier_assm #after_return_assm #trace_label_return #costed_assm
849    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
850    destruct
851    whd in match (trace_any_label_length … (tal_base_call …));
852    whd in match (compute_paid_trace_any_label … (tal_base_call …));
853    whd in costed_assm;
854    generalize in match costed_assm;
855    generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
856    generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
857      in ⊢ (??%? → (match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
858    #lookup_assm cases lookup_assm
859    [1:
860      #None_lookup_opt normalize nodelta #absurd cases absurd
861    |2:
862      #costlabel #Some_lookup_opt normalize nodelta #ignore
863      generalize in match recursive_assm;
864      cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
865      [1:
866        whd in after_return_assm; <after_return_assm; (* XXX: here *)
867        cases daemon
868      |2:
869        #program_counter_assm >program_counter_assm <Some_lookup_opt
870        normalize nodelta #new_recursive_assm >new_recursive_assm %
871        [1:
872          %{(pred total_program_size)} whd in ⊢ (??%?);
873          @S_pred
874          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
875        |2:
876          cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
877          [1:
878            <FETCH %
879          |2:
880            #ticks_refl_assm >ticks_refl_assm
881            <plus_n_O %
882          ]
883        ]
884      ]
885    ]
886  |4:
887    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
888    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
889    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
890    #final_status_refl #the_trace_refl destruct
891    whd in match (trace_any_label_length … (tal_step_call …));
892    whd in match (compute_paid_trace_any_label … (tal_step_call …));
893    whd in costed_assm:(?%);
894    generalize in match costed_assm;
895    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
896    generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
897      in ⊢ (??%? → ?(match % with [ _ ⇒ ? | _ ⇒ ? ]) → ?);
898    #lookup_assm cases lookup_assm
899    [1:
900      #None_lookup_opt_assm normalize nodelta #ignore
901      generalize in match recursive_assm;
902      cut(program_counter'' = program_counter … status_after_fun_call)
903      [1:
904        cases daemon
905      |2:
906        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
907        normalize nodelta #new_recursive_assm %
908        cases (new_recursive_assm … trace_any_label ?)
909        [1,3:
910          #exists_assm #recursive_block_cost_assm
911          [2:
912            >recursive_block_cost_assm
913            @plus_right_monotone
914            whd in ⊢ (???%); <FETCH %
915          |1:
916            (*
917            cases exists_assm #recursive_n #new_exists_assm
918            <new_exists_assm
919           
920            %
921            [1:
922              @(recursive_n - current_instruction_cost … status_pre_fun_call)
923            |2:
924             
925              cut(current_instruction_cost … status_pre_fun_call =
926                (nat_of_bitvector 16
927  (program_counter (BitVectorTrie Byte 16) code_memory' status_after_fun_call)
928  -nat_of_bitvector 16
929   (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
930              [1:
931              |2:
932                #eq_assm <eq_assm -eq_assm -new_exists_assm -recursive_block_cost_assm
933                <plus_n_Sm <plus_n_Sm @eq_f
934                >associative_plus in ⊢ (??%?); >commutative_plus in ⊢ (??%?);
935                >associative_plus @eq_f
936                <plus_minus_m_m [1: % ]
937              ]
938            ] *)
939            cases daemon
940          ]
941        |2,4:
942          %
943        ]
944      ]
945    |2:
946      #cost_label #Some_lookup_opt_assm normalize nodelta #absurd
947      cases absurd #absurd cases (absurd I)
948    ]
949  ]
950  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
951  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
952  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
953  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
954  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
955  #absurd destruct(absurd)
[1684]956qed.
957
[1650]958let rec block_cost'
[1658]959  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
[1621]960    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
[1658]961      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
962        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
963          on program_size:
964          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
965          Σcost_of_block: nat.
[1669]966          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
967            ∀start_status: Status code_memory'.
968            ∀final_status: Status code_memory'.
[1658]969            ∀trace_ends_flag.
[1669]970            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
971              program_counter' = program_counter … start_status →
972                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
973                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
974          else
975            (cost_of_block = 0) ≝
[1658]976  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
[1642]977  [ O ⇒ λbase_case. ⊥
[1621]978  | S program_size' ⇒ λrecursive_case.
[1663]979    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
[1650]980    let to_continue ≝
[1669]981      match lookup_opt … program_counter' cost_labels with
[1650]982      [ None ⇒ true
983      | Some _ ⇒ first_time_around
984      ]
985    in
[1669]986      ((if to_continue then
987       pi1 … (match instruction return λx. x = instruction → ? with
[1663]988        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
989          match real_instruction return λx. x = real_instruction →
990          Σcost_of_block: nat.
[1669]991            ∀start_status: Status code_memory'.
992            ∀final_status: Status code_memory'.
[1663]993            ∀trace_ends_flag.
[1669]994            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
995              program_counter' = program_counter … start_status →
996                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
997                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
[1663]998          [ RET                    ⇒ λinstr. ticks
999          | JC   relative          ⇒ λinstr. ticks
1000          | JNC  relative          ⇒ λinstr. ticks
1001          | JB   bit_addr relative ⇒ λinstr. ticks
1002          | JNB  bit_addr relative ⇒ λinstr. ticks
1003          | JBC  bit_addr relative ⇒ λinstr. ticks
1004          | JZ   relative          ⇒ λinstr. ticks
1005          | JNZ  relative          ⇒ λinstr. ticks
1006          | CJNE src_trgt relative ⇒ λinstr. ticks
1007          | DJNZ src_trgt relative ⇒ λinstr. ticks
1008          | _                      ⇒ λinstr.
[1669]1009         
[1658]1010              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]1011          ] (refl …)
1012        | ACALL addr     ⇒ λinstr.
[1658]1013            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]1014        | AJMP  addr     ⇒ λinstr. ticks
1015        | LCALL addr     ⇒ λinstr.
[1658]1016            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]1017        | LJMP  addr     ⇒ λinstr. ticks
1018        | SJMP  addr     ⇒ λinstr. ticks
1019        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
[1658]1020            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1663]1021        | MOVC  src trgt ⇒ λinstr.
[1658]1022            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
[1669]1023        ] (refl …))
[1650]1024      else
[1669]1025        0)
1026      : Σcost_of_block: nat.
1027          match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
1028          [ true ⇒
1029            ∀start_status: Status code_memory'.
1030            ∀final_status: Status code_memory'.
1031            ∀trace_ends_flag.
1032            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
1033              program_counter' = program_counter … start_status →
1034                (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
1035                  cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
1036          | false ⇒
1037            (cost_of_block = 0)
1038          ])
[1621]1039  ].
[1692]1040  cases daemon (*
[1642]1041  [1:
1042    cases reachable_program_counter_witness #_ #hyp
1043    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
1044    @(le_to_lt_to_lt … base_case hyp)
[1669]1045  |2:
[1684]1046    change with (if to_continue then ? else (? = 0))
1047    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
1048    @pi2
[1669]1049  |3:
[1684]1050    change with (if to_continue then ? else (0 = 0))
1051    >p normalize nodelta %
1052  |98,104,107:
[1669]1053    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
[1663]1054    cases(block_cost' ?????????) -block_cost'
[1691]1055    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
1056    destruct %
[1684]1057  |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,
[1691]1058   92,95:
[1684]1059    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1060    cases(block_cost' ?????????) -block_cost'
[1691]1061    @(trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
[1669]1062    destruct %
[1684]1063  |62,63,64,65,66,67,68,69,101,102,103:
[1691]1064    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1065    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
1066    destruct %
[1684]1067  |96,99:
1068    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1069    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1070    <FETCH normalize nodelta <instr normalize nodelta *
1071    #program_counter_lt' #program_counter_lt_tps' %
1072    [1,3:
1073      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1074      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1075      >(le_to_leb_true … program_counter_lt') %
1076    |2,4:
1077      assumption
1078    ]
1079  |105:
1080    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1081    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1082    <FETCH normalize nodelta <instr normalize nodelta
1083    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1084    * * * * #n'
1085    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1086    %
[1663]1087    [1:
[1684]1088      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1089      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1090      >(le_to_leb_true … program_counter_lt') %
1091    |2:
1092      assumption
1093    ]
1094  |106:
1095    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1096    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1097    <FETCH normalize nodelta <instr normalize nodelta
1098    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1099    * * * * #n'
1100    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1101    @(transitive_le
1102      total_program_size
1103      ((S program_size') + nat_of_bitvector … program_counter')
1104      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1105    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1106    >plus_n_Sm
1107    @monotonic_le_plus_r
1108    change with (
1109      nat_of_bitvector … program_counter' <
1110        nat_of_bitvector … program_counter'')
1111    assumption
1112  |108:
1113    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1114    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1115    <FETCH normalize nodelta <instr normalize nodelta
1116    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1117    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1118    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1119    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1120    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1121    %
1122    [1:
1123      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1124      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1125      >(le_to_leb_true … program_counter_lt') %
1126    |2:
1127      assumption
1128    ]
1129  |109:
1130    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1131    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1132    <FETCH normalize nodelta <instr normalize nodelta
1133    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1134    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1135    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1136    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1137    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1138    @(transitive_le
1139      total_program_size
1140      ((S program_size') + nat_of_bitvector … program_counter')
1141      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1142    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1143    >plus_n_Sm
1144    @monotonic_le_plus_r
1145    change with (
1146      nat_of_bitvector … program_counter' <
1147        nat_of_bitvector … program_counter'')
1148    assumption
1149  |5,8,12,14,15,18,20,21,24,27,30,33,36,39,42,45,48,51,54,57,60,72,75,
1150   78,81,84,87,90,93:
1151    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1152    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1153    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
1154    #program_counter_lt' #program_counter_lt_tps' %
1155    try assumption
1156    %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1157    <FETCH normalize nodelta whd in match ltb; normalize nodelta
1158    >(le_to_leb_true … program_counter_lt') %
1159  |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,
1160   94:
1161    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1162    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1163    <FETCH normalize nodelta
1164    <real_instruction_refl <instr normalize nodelta *
1165    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1166    @(transitive_le
1167      total_program_size
1168      ((S program_size') + nat_of_bitvector … program_counter')
1169      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1170    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1171    >plus_n_Sm
1172    @monotonic_le_plus_r
1173    change with (
1174      nat_of_bitvector … program_counter' <
1175        nat_of_bitvector … program_counter'')
1176    assumption
1177  |10:
1178    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1179    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
1180      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
1181    [1:
[1692]1182      #recursive_block_cost #recursive_assm
1183      @(trace_any_label_inv_ind … the_trace)
[1665]1184      [1:
[1692]1185        #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
1186        #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1187        destruct @⊥
[1665]1188      |2:
[1692]1189        #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_flag_refl
1190        #start_status_refl #final_status_refl #the_trace_refl destruct
1191        whd in match (trace_any_label_length … (tal_base_return …));
1192        whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
[1665]1193        [1:
[1692]1194          %{(pred total_program_size)} whd in ⊢ (??%?);
1195          @S_pred
1196          @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness)
[1665]1197        |2:
[1663]1198          <FETCH %
1199        ]
1200      |3:
[1692]1201        #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
1202        #classifier_assm #after_return_assm #trace_label_return #costed_assm
1203        #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
1204        destruct @⊥
1205      |4:
1206        #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
1207        #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
1208        #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
1209        #final_status_refl #the_trace_refl
1210        destruct @⊥
1211      |5:
1212        #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
1213        #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
1214        #final_status_refl #the_trace_refl destruct @⊥
[1663]1215      ]
[1692]1216      try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
1217      try (change with (ASM_classify0 ? = ?) in classifier_assm;)
[1663]1218      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
1219      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
[1692]1220      <FETCH in classifier_assm;
1221      try(whd in ⊢ ((??%?) → ?); #absurd destruct(absurd))
1222      whd in ⊢ (?(??%?)(??%?) → ?); #absurd
1223      cases absurd #absurd destruct(absurd)
1224    |2:
1225      cases daemon (* XXX: ??? *)
[1663]1226    ]
[1692]1227  |62,63,64,65,66,67,68,69,70,101,102,103:
1228    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1229    cases(block_cost' code_memory' program_counter' program_size total_program_size cost_labels
1230      reachable_program_counter_witness good_program_witness first_time_around ?) -block_cost'
1231    try (@(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl …) destruct %)
1232    cases daemon (* XXX: ???, same as above case *)
1233  |96,99:
[1642]1234    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
[1658]1235    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1692]1236    <FETCH normalize nodelta <instr normalize nodelta *
1237    #program_counter_lt' #program_counter_lt_tps' %
1238    [1,3:
1239      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1240      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1241      >(le_to_leb_true … program_counter_lt') %
1242    |2,4:
1243      assumption
1244    ]
1245  |98,104,107:
1246    #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
1247    cases(block_cost' ?????????) -block_cost'
1248    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness first_time_around … recursive_case … FETCH … the_trace program_counter_refl …)
1249    destruct %
1250  |105:
[1658]1251    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1252    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1663]1253    <FETCH normalize nodelta <instr normalize nodelta
[1692]1254    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1255    * * * * #n'
[1658]1256    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1257    %
1258    [1:
1259      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1260      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1261      >(le_to_leb_true … program_counter_lt') %
1262    |2:
1263      assumption
1264    ]
[1692]1265  |106:
[1658]1266    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1267    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1692]1268    <FETCH normalize nodelta <instr normalize nodelta
[1658]1269    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
1270    * * * * #n'
[1692]1271    #_ #_ #program_counter_lt' #program_counter_lt_tps'
[1658]1272    @(transitive_le
1273      total_program_size
1274      ((S program_size') + nat_of_bitvector … program_counter')
1275      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1276    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1277    >plus_n_Sm
1278    @monotonic_le_plus_r
1279    change with (
1280      nat_of_bitvector … program_counter' <
1281        nat_of_bitvector … program_counter'')
1282    assumption
[1692]1283  |108:
[1663]1284    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1285    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1692]1286    <FETCH normalize nodelta <instr normalize nodelta
1287    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1288    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1289    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1290    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
[1663]1291    #_ #_ #program_counter_lt' #program_counter_lt_tps'
1292    %
1293    [1:
1294      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
1295      <FETCH normalize nodelta whd in match ltb; normalize nodelta
1296      >(le_to_leb_true … program_counter_lt') %
1297    |2:
1298      assumption
1299    ]
[1692]1300  |109:
[1663]1301    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1302    lapply(good_program_witness program_counter' reachable_program_counter_witness)
1303    <FETCH normalize nodelta <instr normalize nodelta
[1692]1304    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
1305    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
1306    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
1307    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
1308    #_ #_ #program_counter_lt' #program_counter_lt_tps'
[1663]1309    @(transitive_le
1310      total_program_size
1311      ((S program_size') + nat_of_bitvector … program_counter')
1312      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1313    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1314    >plus_n_Sm
1315    @monotonic_le_plus_r
1316    change with (
1317      nat_of_bitvector … program_counter' <
1318        nat_of_bitvector … program_counter'')
1319    assumption
[1692]1320  |97,100:
[1663]1321    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
1322    lapply(good_program_witness program_counter' reachable_program_counter_witness)
[1692]1323    <FETCH normalize nodelta <instr normalize nodelta
1324    try(<real_instruction_refl <instr normalize nodelta) *
[1663]1325    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
1326    @(transitive_le
1327      total_program_size
1328      ((S program_size') + nat_of_bitvector … program_counter')
1329      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
1330    normalize in match (S program_size' + nat_of_bitvector … program_counter');
1331    >plus_n_Sm
1332    @monotonic_le_plus_r
1333    change with (
1334      nat_of_bitvector … program_counter' <
1335        nat_of_bitvector … program_counter'')
1336    assumption
[1692]1337  ] *)
[1642]1338qed.
1339
[1650]1340definition block_cost ≝
1341  λcode_memory: BitVectorTrie Byte 16.
1342  λprogram_counter: Word.
1343  λtotal_program_size: nat.
1344  λcost_labels: BitVectorTrie costlabel 16.
1345  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
1346  λgood_program_witness: good_program code_memory total_program_size.
1347    block_cost' code_memory program_counter total_program_size total_program_size cost_labels
1348      reachable_program_counter_witness good_program_witness true ?.
1349  @le_plus_n_r
1350qed.
1351
[1646]1352lemma fetch_program_counter_n_Sn:
[1645]1353  ∀instruction: instruction.
1354  ∀program_counter, program_counter': Word.
1355  ∀ticks, n: nat.
1356  ∀code_memory: BitVectorTrie Byte 16.
1357    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
1358      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
[1646]1359        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
1360          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
1361  #instruction #program_counter #program_counter' #ticks #n #code_memory
1362  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
1363  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
1364  <fetch_program_counter_n_hyp normalize nodelta
1365  <fetch_hyp normalize nodelta
1366  change with (
1367    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
1368  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
1369  >(le_to_leb_true … lt_hyp) %
1370qed.
1371
[1645]1372let rec traverse_code_internal
[1646]1373  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
1374    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
1375      (reachable_program_counter_witness:
1376          ∀lbl: costlabel.
1377          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1378            reachable_program_counter code_memory fixed_program_size program_counter)
1379        (good_program_witness: good_program code_memory fixed_program_size)
1380        on program_size: identifier_map CostTag nat ≝
1381  match program_size with
1382  [ O ⇒ empty_map …
1383  | S program_size ⇒
1384    let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
1385    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
1386    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with
1387    [ None ⇒ λlookup_refl. cost_mapping
1388    | Some lbl ⇒ λlookup_refl.
[1650]1389      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
[1645]1390        add … cost_mapping lbl cost
[1646]1391    ] (refl … (lookup_opt … program_counter cost_labels))
[1645]1392  ].
[1646]1393  [1:
1394    @(reachable_program_counter_witness lbl)
1395    assumption
1396  |2:
[1645]1397    assumption
[1642]1398  ]
[1639]1399qed.
[1486]1400
1401definition traverse_code ≝
[1645]1402  λcode_memory: BitVectorTrie Byte 16.
[1646]1403  λcost_labels: BitVectorTrie costlabel 16.
[1486]1404  λprogram_size: nat.
[1646]1405  λreachable_program_counter_witness:
1406          ∀lbl: costlabel.
1407          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
1408            reachable_program_counter code_memory program_size program_counter.
[1645]1409  λgood_program_witness: good_program code_memory program_size.
[1646]1410    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
[1648]1411 
[1486]1412definition compute_costs ≝
1413  λprogram: list Byte.
[1557]1414  λcost_labels: BitVectorTrie costlabel 16.
[1648]1415  λreachable_program_witness.
[1645]1416  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
1417    let program_size ≝ |program| + 1 in
1418    let code_memory ≝ load_code_memory program in
[1648]1419      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
[1646]1420  @good_program_witness
[1645]1421qed.
Note: See TracBrowser for help on using the repository browser.