include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".
include "ASM/Fetch.ma".
include "ASM/Interpret.ma".
include "common/StructuredTraces.ma".

let rec fetch_program_counter_n
  (n: nat) (code_memory: BitVectorTrie Byte 16) (program_counter: Word)
    on n: option Word ≝
  match n with
  [ O ⇒ Some … program_counter
  | S n ⇒
    match fetch_program_counter_n n code_memory program_counter with
    [ None ⇒ None …
    | Some tail_pc ⇒
      let 〈instr, program_counter, ticks〉 ≝ fetch code_memory tail_pc in
        if ltb (nat_of_bitvector … tail_pc) (nat_of_bitvector … program_counter) then
          Some … program_counter
        else
          None Word (* XXX: overflow! *)
    ]
  ].
    
definition reachable_program_counter: BitVectorTrie Byte 16 → nat → Word → Prop ≝
  λcode_memory: BitVectorTrie Byte 16.
  λprogram_size: nat.
  λprogram_counter: Word.
    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
        nat_of_bitvector 16 program_counter < program_size.
    
definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
  λcode_memory: BitVectorTrie Byte 16.
  λtotal_program_size: nat.
  ∀program_counter: Word.
  ∀good_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
  let 〈instruction, program_counter', ticks〉 ≝ fetch code_memory program_counter in
    match instruction with
    [ RealInstruction instr ⇒
      match instr with
      [ RET                    ⇒ True
      | JC   relative          ⇒ True (* XXX: see below *)
      | JNC  relative          ⇒ True (* XXX: see below *)
      | JB   bit_addr relative ⇒ True
      | JNB  bit_addr relative ⇒ True
      | JBC  bit_addr relative ⇒ True
      | JZ   relative          ⇒ True
      | JNZ  relative          ⇒ True
      | CJNE src_trgt relative ⇒ True
      | DJNZ src_trgt relative ⇒ True
      | _                      ⇒
        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
          nat_of_bitvector … program_counter' < total_program_size
      ]
    | LCALL addr         ⇒
      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
      [ ADDR16 addr ⇒ λaddr16: True.
          reachable_program_counter code_memory total_program_size addr ∧
            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
              nat_of_bitvector … program_counter' < total_program_size
      | _ ⇒ λother: False. ⊥
      ] (subaddressing_modein … addr)
    | ACALL addr         ⇒
      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
      [ ADDR11 addr ⇒ λaddr11: True.
        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
        let 〈thr, eig〉 ≝ split … 3 8 addr in
        let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
        let new_program_counter ≝ (fiv @@ thr) @@ pc_bl in
          reachable_program_counter code_memory total_program_size new_program_counter ∧
            nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
              nat_of_bitvector … program_counter' < total_program_size
      | _ ⇒ λother: False. ⊥
      ] (subaddressing_modein … addr)
    | AJMP  addr         ⇒
      match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with
      [ ADDR11 addr ⇒ λaddr11: True.
        let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in
        let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
        let bit ≝ get_index' … O ? nl in
        let 〈relevant1, relevant2〉 ≝ split … 3 8 addr in
        let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
        let 〈carry, new_program_counter〉 ≝ half_add 16 program_counter new_addr in
          reachable_program_counter code_memory total_program_size new_program_counter
      | _ ⇒ λother: False. ⊥
      ] (subaddressing_modein … addr)
    | LJMP  addr         ⇒
      match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with
      [ ADDR16 addr ⇒ λaddr16: True.
          reachable_program_counter code_memory total_program_size addr
      | _ ⇒ λother: False. ⊥
      ] (subaddressing_modein … addr)
    | SJMP  addr     ⇒
      match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Prop with
      [ RELATIVE addr ⇒ λrelative: True.
        let 〈carry, new_program_counter〉 ≝ half_add … program_counter' (sign_extension addr) in
          reachable_program_counter code_memory total_program_size new_program_counter
      | _ ⇒ λother: False. ⊥
      ] (subaddressing_modein … addr)
    | JMP   addr     ⇒ (* XXX: JMP is used for fptrs and unconstrained *)
      nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
        nat_of_bitvector … program_counter' < total_program_size
    | MOVC  src trgt ⇒
        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧
          nat_of_bitvector … program_counter' < total_program_size
    ].
  cases other
qed.
        
lemma is_a_decidable:
  ∀hd.
  ∀element.
    is_a hd element = true ∨ is_a hd element = false.
  #hd #element //
qed.

lemma mem_decidable:
  ∀n: nat.
  ∀v: Vector addressing_mode_tag n.
  ∀element: addressing_mode_tag.
    mem … eq_a n v element = true ∨
      mem … eq_a … v element = false.
  #n #v #element //
qed.

lemma eq_a_elim:
  ∀tag.
  ∀hd.
  ∀P: bool → Prop.
    (tag = hd → P (true)) →
      (tag ≠ hd → P (false)) →
        P (eq_a tag hd).
  #tag #hd #P
  cases tag
  cases hd
  #true_hyp #false_hyp
  try @false_hyp
  try @true_hyp
  try %
  #absurd destruct(absurd)
qed.
  
lemma is_a_true_to_is_in:
  ∀n: nat.
  ∀x: addressing_mode.
  ∀tag: addressing_mode_tag.
  ∀supervector: Vector addressing_mode_tag n.
  mem addressing_mode_tag eq_a n supervector tag →
    is_a tag x = true →
      is_in … supervector x.
  #n #x #tag #supervector
  elim supervector
  [1:
    #absurd cases absurd
  |2:
    #n' #hd #tl #inductive_hypothesis
    whd in match (mem … eq_a (S n') (hd:::tl) tag);
    @eq_a_elim normalize nodelta
    [1:
      #tag_hd_eq #irrelevant
      whd in match (is_in (S n') (hd:::tl) x);
      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
      @I
    |2:
      #tag_hd_neq
      whd in match (is_in (S n') (hd:::tl) x);
      change with (
        mem … eq_a n' tl tag)
          in match (fold_right … n' ? false tl);
      #mem_hyp #is_a_hyp
      cases(is_a hd x)
      [1:
        normalize nodelta //
      |2:
        normalize nodelta
        @inductive_hypothesis assumption
      ]
    ]
  ]
qed.

lemma is_in_subvector_is_in_supervector:
  ∀m, n: nat.
  ∀subvector: Vector addressing_mode_tag m.
  ∀supervector: Vector addressing_mode_tag n.
  ∀element: addressing_mode.
    subvector_with … eq_a subvector supervector →
      is_in m subvector element → is_in n supervector element.
  #m #n #subvector #supervector #element
  elim subvector
  [1:
    #subvector_with_proof #is_in_proof
    cases is_in_proof
  |2:
    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
    whd in match (is_in … (hd':::tl') element);
    cases (is_a_decidable hd' element)
    [1:
      #is_a_true >is_a_true
      #irrelevant
      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
      @(is_a_true_to_is_in … is_a_true)
      lapply(subvector_with_proof)
      cases(mem … eq_a n supervector hd') //
    |2:
      #is_a_false >is_a_false normalize nodelta
      #assm
      @inductive_hypothesis
      [1:
        generalize in match subvector_with_proof;
        whd in match (subvector_with … eq_a (hd':::tl') supervector);
        cases(mem_decidable n supervector hd')
        [1:
          #mem_true >mem_true normalize nodelta
          #assm assumption
        |2:
          #mem_false >mem_false #absurd
          cases absurd
        ]
      |2:
        assumption
      ]
    ]
  ]
qed.

let rec member_addressing_mode_tag
  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
    on v: Prop ≝
  match v with
  [ VEmpty ⇒ False
  | VCons n' hd tl ⇒
      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
  ].
  
let rec subaddressing_mode_elim_type
  (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)
    (Q: addressing_mode → T → Prop)
      (p_addr11:            ∀w: Word11.      is_in m fixed_v (ADDR11 w)        → T)
      (p_addr16:            ∀w: Word.        is_in m fixed_v (ADDR16 w)        → T)
      (p_direct:            ∀w: Byte.        is_in m fixed_v (DIRECT w)        → T)
      (p_indirect:          ∀w: Bit.         is_in m fixed_v (INDIRECT w)      → T)
      (p_ext_indirect:      ∀w: Bit.         is_in m fixed_v (EXT_INDIRECT w)  → T)
      (p_acc_a:                              is_in m fixed_v ACC_A             → T)
      (p_register:          ∀w: BitVector 3. is_in m fixed_v (REGISTER w)      → T)
      (p_acc_b:                              is_in m fixed_v ACC_B             → T)
      (p_dptr:                               is_in m fixed_v DPTR              → T)
      (p_data:              ∀w: Byte.        is_in m fixed_v (DATA w)          → T)
      (p_data16:            ∀w: Word.        is_in m fixed_v (DATA16 w)        → T)
      (p_acc_dptr:                           is_in m fixed_v ACC_DPTR          → T)
      (p_acc_pc:                             is_in m fixed_v ACC_PC            → T)
      (p_ext_indirect_dptr:                  is_in m fixed_v EXT_INDIRECT_DPTR → T)
      (p_indirect_dptr:                      is_in m fixed_v INDIRECT_DPTR     → T)
      (p_carry:                              is_in m fixed_v CARRY             → T)
      (p_bit_addr:          ∀w: Byte.        is_in m fixed_v (BIT_ADDR w)      → T)
      (p_n_bit_addr:        ∀w: Byte.        is_in m fixed_v (N_BIT_ADDR w)    → T)
      (p_relative:          ∀w: Byte.        is_in m fixed_v (RELATIVE w)      → T)
        (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
      on v: Prop ≝
  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
  [ VEmpty         ⇒ λm_refl. λv_refl.
      ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.
        Q addr (
        match addr return λx: addressing_mode. is_in … fixed_v x → T with 
        [ ADDR11 x          ⇒ p_addr11 x
        | ADDR16 x          ⇒ p_addr16 x
        | DIRECT x          ⇒ p_direct x
        | INDIRECT x        ⇒ p_indirect x
        | EXT_INDIRECT x    ⇒ p_ext_indirect x
        | ACC_A             ⇒ p_acc_a
        | REGISTER x        ⇒ p_register x
        | ACC_B             ⇒ p_acc_b
        | DPTR              ⇒ p_dptr
        | DATA x            ⇒ p_data x
        | DATA16 x          ⇒ p_data16 x
        | ACC_DPTR          ⇒ p_acc_dptr
        | ACC_PC            ⇒ p_acc_pc
        | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr
        | INDIRECT_DPTR     ⇒ p_indirect_dptr
        | CARRY             ⇒ p_carry
        | BIT_ADDR x        ⇒ p_bit_addr x
        | N_BIT_ADDR x      ⇒ p_n_bit_addr x
        | RELATIVE x        ⇒ p_relative x
        ] p)
  | VCons n' hd tl ⇒ λm_refl. λv_refl.
    let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11
      p_addr16 p_direct p_indirect p_ext_indirect p_acc_a
        p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr
          p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry
            p_bit_addr p_n_bit_addr p_relative n' tl ?
    in
    match hd return λa: addressing_mode_tag. a = hd → ? with
    [ addr11            ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call
    | addr16            ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call
    | direct            ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call
    | indirect          ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call
    | ext_indirect      ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call
    | acc_a             ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call
    | registr           ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call
    | acc_b             ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call
    | dptr              ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call
    | data              ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call
    | data16            ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call
    | acc_dptr          ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call
    | acc_pc            ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call
    | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call
    | indirect_dptr     ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call
    | carry             ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call
    | bit_addr          ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call
    | n_bit_addr        ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call
    | relative          ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call
    ] (refl … hd)
  ] (refl … n) (refl_jmeq … v).
  [20:
    generalize in match proof; destruct
    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
    cases (mem … eq_a m fixed_v hd) normalize nodelta
    [1:
      whd in match (subvector_with … eq_a tl fixed_v);
      #assm assumption
    |2:
      normalize in ⊢ (% → ?);
      #absurd cases absurd
    ]
  ]
  @(is_in_subvector_is_in_supervector … proof)
  destruct @I
qed.

lemma subaddressing_mode_elim':
  ∀T: Type[2].
  ∀n: nat.
  ∀o: nat.
  ∀Q: addressing_mode → T → Prop.
  ∀fixed_v: Vector addressing_mode_tag (n + o).
  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
  ∀v1: Vector addressing_mode_tag n.
  ∀v2: Vector addressing_mode_tag o.
  ∀fixed_v_proof: fixed_v = v1 @@ v2.
  ∀subaddressing_mode_proof.
    subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7
      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.
  #T #n #o #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10
  #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #v1 #v2 #fixed_v_proof
  cases daemon
qed.

axiom subaddressing_mode_elim:
  ∀T: Type[2].
  ∀m: nat.
  ∀n: nat.
  ∀Q: addressing_mode → T → Prop.
  ∀fixed_v: Vector addressing_mode_tag m.
  ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.
  ∀v: Vector addressing_mode_tag n.
  ∀proof.
    subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
      P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.

definition current_instruction0 ≝
  λcode_memory: BitVectorTrie Byte 16.
  λprogram_counter: Word.
    \fst (\fst (fetch … code_memory program_counter)).

definition current_instruction ≝
  λs: Status.
    current_instruction0 (code_memory … s) (program_counter … s).

definition ASM_classify0: instruction → status_class ≝
  λi: instruction.
  match i with
   [ RealInstruction pre ⇒
     match pre with
      [ RET ⇒ cl_return
      | JZ _ ⇒ cl_jump
      | JNZ _ ⇒ cl_jump
      | JC _ ⇒ cl_jump
      | JNC _ ⇒ cl_jump
      | JB _ _ ⇒ cl_jump
      | JNB _ _ ⇒ cl_jump
      | JBC _ _ ⇒ cl_jump
      | CJNE _ _ ⇒ cl_jump
      | DJNZ _ _ ⇒ cl_jump
      | _ ⇒ cl_other
      ]
   | ACALL _ ⇒ cl_call
   | LCALL _ ⇒ cl_call
   | JMP _ ⇒ cl_call
   | AJMP _ ⇒ cl_jump
   | LJMP _ ⇒ cl_jump
   | SJMP _ ⇒ cl_jump
   | _ ⇒ cl_other
   ].

definition ASM_classify: Status → status_class ≝
  λs: Status.
    ASM_classify0 (current_instruction s).

definition current_instruction_is_labelled ≝
  λcost_labels: BitVectorTrie costlabel 16.
  λs: Status.
  let pc ≝ program_counter … s in
    match lookup_opt … pc cost_labels with
    [ None ⇒ False
    | _    ⇒ True
    ].

definition next_instruction_properly_relates_program_counters ≝
  λbefore: Status.
  λafter : Status.
  let size ≝ current_instruction_cost before in
  let pc_before ≝ program_counter … before in
  let pc_after ≝ program_counter … after in
  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    sum = pc_after.

definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
 λcost_labels.
  mk_abstract_status
   Status
   (λs,s'. (execute_1 s) = s')
   (λs,class. ASM_classify s = class)
   (current_instruction_is_labelled cost_labels)
   next_instruction_properly_relates_program_counters.

let rec trace_any_label_length
  (cost_labels: BitVectorTrie costlabel 16) (trace_ends_flag: trace_ends_with_ret)
    (start_status: Status) (final_status: Status)
      (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
        on the_trace: nat ≝
  match the_trace with
  [ tal_base_not_return the_status _ _ _ _ ⇒ 0
  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 0
  | tal_base_return the_status _ _ _ ⇒ 0
  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
      let tail_length ≝ trace_any_label_length … final_trace in
      let pc_difference ≝ nat_of_bitvector … (program_counter … after_fun_call) - nat_of_bitvector … (program_counter … pre_fun_call) in        
        pc_difference + tail_length
  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
      let tail_length ≝ trace_any_label_length … tail_trace in
      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
        pc_difference + tail_length        
  ].

let rec compute_paid_trace_any_label
  (cost_labels: BitVectorTrie costlabel 16)
  (trace_ends_flag: trace_ends_with_ret)
   (start_status: Status) (final_status: Status)
     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
       on the_trace: nat ≝
  match the_trace with
  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ current_instruction_cost pre_fun_call
  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     _ _ _ call_trace _ final_trace ⇒
      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
      let final_trace_cost ≝ compute_paid_trace_any_label cost_labels end_flag … final_trace in
        current_instruction_cost + final_trace_cost
  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
      let current_instruction_cost ≝ current_instruction_cost status_pre in
      let tail_trace_cost ≝
       compute_paid_trace_any_label cost_labels end_flag
        status_init status_end tail_trace
      in
        current_instruction_cost + tail_trace_cost
  ].

definition compute_paid_trace_label_label ≝
 λcost_labels: BitVectorTrie costlabel 16.
  λtrace_ends_flag: trace_ends_with_ret.
   λstart_status: Status.
    λfinal_status: Status.
     λthe_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
      start_status final_status.
  match the_trace with
  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
      compute_paid_trace_any_label … given_trace
  ].

include alias "arithmetics/nat.ma".
include alias "basics/logic.ma".

(* Bug to be fixed in the refiner! Compare the two checks
axiom T:Type[0].
axiom S:Type[0].
axiom k: S → T.
coercion k.
check (λf: T → nat. (f: S → nat))
check ((λx:T.0) : S → nat) *)
definition foo ≝ (match match 1 with [O ⇒ 0 | S n ⇒ S ?] : Σn:nat. n=n).

let rec block_cost'
  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
          on program_size:
          total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
          Σcost_of_block: nat.
            ∀start_status: Status.
            ∀final_status: Status.
            ∀trace_ends_flag.
            ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
              code_memory' = code_memory … start_status →
                program_counter' = program_counter … start_status →
                    (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) ∧
                      cost_of_block = compute_paid_trace_any_label cost_labels trace_ends_flag start_status final_status the_trace ≝
  match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
  [ O ⇒ λbase_case. ⊥
  | S program_size' ⇒ λrecursive_case.
    let 〈instruction, program_counter'', ticks〉 ≝ fetch code_memory' program_counter' in
    let to_continue ≝
      match lookup_opt … program_counter'' cost_labels with
      [ None ⇒ true
      | Some _ ⇒ first_time_around
      ]
    in
      if to_continue then
        match instruction with
        [ RealInstruction real_instruction ⇒
          match real_instruction with
          [ RET                    ⇒ ticks
          | JC   relative          ⇒ ticks
          | JNC  relative          ⇒ ticks
          | JB   bit_addr relative ⇒ ticks
          | JNB  bit_addr relative ⇒ ticks
          | JBC  bit_addr relative ⇒ ticks
          | JZ   relative          ⇒ ticks
          | JNZ  relative          ⇒ ticks
          | CJNE src_trgt relative ⇒ ticks
          | DJNZ src_trgt relative ⇒ ticks
          | _                      ⇒ 
              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
          ] 
        | ACALL addr     ⇒ 
            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
        | AJMP  addr     ⇒ ticks
        | LCALL addr     ⇒ 
            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
        | LJMP  addr     ⇒ ticks
        | SJMP  addr     ⇒ ticks
        | JMP   addr     ⇒ (* XXX: actually a call due to use with fptrs *)
            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
        | MOVC  src trgt ⇒
            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
        ]
      else
        0
  ].
  [57:
  [1:
    cases reachable_program_counter_witness #_ #hyp
    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
    @(le_to_lt_to_lt … base_case hyp)
  |2:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    <FETCH normalize nodelta >instr normalize nodelta
    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    #_ #_ #program_counter_lt' #program_counter_lt_tps'      
    @(transitive_le
      total_program_size
      ((S program_size') + nat_of_bitvector … program_counter')
      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    normalize in match (S program_size' + nat_of_bitvector … program_counter');
    >plus_n_Sm
    @monotonic_le_plus_r
    change with (
      nat_of_bitvector … program_counter' <
        nat_of_bitvector … program_counter'')
    assumption
  |3:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    <FETCH normalize nodelta >instr normalize nodelta
    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    #_ #_ #program_counter_lt' #program_counter_lt_tps'
    %
    [1:
      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
      <FETCH normalize nodelta whd in match ltb; normalize nodelta
      >(le_to_leb_true … program_counter_lt') %
    |2:
      assumption
    ]
  |4:
  |5:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter' reachable_program_counter_witness)
      <FETCH normalize nodelta >instr normalize nodelta
    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    * * * * #n'
    #_ #_ #program_counter_lt' #program_counter_lt_tps'      
    @(transitive_le
      total_program_size
      ((S program_size') + nat_of_bitvector … program_counter')
      (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    normalize in match (S program_size' + nat_of_bitvector … program_counter');
    >plus_n_Sm
    @monotonic_le_plus_r
    change with (
      nat_of_bitvector … program_counter' <
        nat_of_bitvector … program_counter'')
    assumption
  
  [1:
    #start_status #final_status #trace_ends_flag #the_trace #code_memory_refl #program_counter_refl
    cases(block_cost' ?????? ?? ?) -block_cost'
    #recursive_block_cost #recursive_assm
    @(trace_any_label_inv_ind … the_trace)
    [1:
      #start_status' #final_status' #execute_assm #classifier_assm #costed_assm
      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl destruct
      cases classifier_assm
      whd in match (as_classifier ? ? ?);
      whd in ⊢ (??%? → ?);
      whd in match current_instruction; normalize nodelta
      whd in match current_instruction0; normalize nodelta
      #absurd @⊥ >p1 in absurd; normalize nodelta
      #absurd destruct(absurd)
    |2:
      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
      #start_status_refl #final_status_refl #the_trace_assm destruct
      whd in classifier_assm;
      whd in classifier_assm:(??%?);
      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
      @⊥
      >p1 in classifier_assm; normalize nodelta
      #absurd destruct(absurd)
    |3:
      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
      #classifier_assm #after_return_assm #trace_label_return #costed_assm
      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
      destruct
      cases(recursive_assm status_pre_fun_call status_final doesnt_end_with_ret
        (tal_base_call (ASM_abstract_status cost_labels) status_pre_fun_call
          (execute_1 status_pre_fun_call) status_final
          (refl Status (execute_1 status_pre_fun_call)) classifier_assm
          after_return_assm trace_label_return costed_assm) ? ?)
      [2: %
      |3: 
      |1:
      ]
    |4:
      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
      #costed_assm #trace_any_label #trace_ends_refl #start_status_refl #final_status_refl
      #the_trace_refl destruct whd in ⊢ (??(???%)); whd in match (trace_any_label_length … (tal_step_call … trace_any_label));
    |5:
      #end_flag #status_pre #status_init #status_end #execute_assm #the_trace
      #classifier_assm #costed_assm #ends_flag_refl #start_status_refl #final_status_refl
      #the_trace_refl -the_trace_refl destruct
      whd in classifier_assm;
      whd in classifier_assm:(??%?);
      whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
      whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
      @⊥ >p1 in classifier_assm; normalize nodelta
      #absurd destruct(absurd)
    ]
  [1:
    #start_status #final_status #trace_ends_flag #the_trace
    #code_memory_refl #program_counter_refl
    cases(block_cost' ?????? ?? ?) -block_cost'
    #recursive_block_cost #recursive_assm
    @(trace_any_label_inv_ind … the_trace)
    [1:
      #start_status' #final_status' #execute_assm #not_return_assm
      #costed_assm #trace_ends_flag_assm #start_status_assm #final_status_assm
      #the_trace_assm
      cases daemon (* XXX: bug in notion of traces here *)
    |2:

    |3:
      cases daemon (* XXX *)
    |4:
    ]
  |108:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter' reachable_program_counter_witness)
    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
    #program_counter_lt' #program_counter_lt_tps' %
    try assumption
    [*:
      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
      <FETCH normalize nodelta whd in match ltb; normalize nodelta
      >(le_to_leb_true … program_counter_lt') %
    ]
  [1:
    cases reachable_program_counter_witness #_ #hyp
    @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
    @(le_to_lt_to_lt … base_case hyp)
  |2:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
      <FETCH normalize nodelta <instr normalize nodelta
    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    #_ #_ #program_counter_lt' #program_counter_lt_tps'      
    @(transitive_le
      total_program_size
      ((S program_size') + nat_of_bitvector … program_counter)
      (program_size' + nat_of_bitvector … program_counter') recursive_case)
    normalize in match (S program_size' + nat_of_bitvector … program_counter);
    >plus_n_Sm
    @monotonic_le_plus_r
    change with (
      nat_of_bitvector … program_counter <
        nat_of_bitvector … program_counter')
    assumption
  |3:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
      <FETCH normalize nodelta <instr normalize nodelta
    @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    #_ #_ #program_counter_lt' #program_counter_lt_tps'
    %
    [1:
      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
      <FETCH normalize nodelta whd in match ltb; normalize nodelta
      >(le_to_leb_true … program_counter_lt') %
    |2:
      assumption
    ]
  |4:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
      <FETCH normalize nodelta <instr normalize nodelta
    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    * * * * #n'
    #_ #_ #program_counter_lt' #program_counter_lt_tps'      
    @(transitive_le
      total_program_size
      ((S program_size') + nat_of_bitvector … program_counter)
      (program_size' + nat_of_bitvector … program_counter') recursive_case)
    normalize in match (S program_size' + nat_of_bitvector … program_counter);
    >plus_n_Sm
    @monotonic_le_plus_r
    change with (
      nat_of_bitvector … program_counter <
        nat_of_bitvector … program_counter')
    assumption
  |5:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
      <FETCH normalize nodelta <instr normalize nodelta
    @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    * * * * #n'
    #_ #_ #program_counter_lt' #program_counter_lt_tps'
    %
    [1:
      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
      <FETCH normalize nodelta whd in match ltb; normalize nodelta
      >(le_to_leb_true … program_counter_lt') %
    |2:
      assumption
    ]
  |6,8: (* JMP and MOVC *)
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
    <FETCH normalize nodelta <instr normalize nodelta
    try(<real_instruction_refl <instr normalize nodelta) *
    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    @(transitive_le
      total_program_size
      ((S program_size') + nat_of_bitvector … program_counter)
      (program_size' + nat_of_bitvector … program_counter') recursive_case)
    normalize in match (S program_size' + nat_of_bitvector … program_counter);
    >plus_n_Sm
    @monotonic_le_plus_r
    change with (
      nat_of_bitvector … program_counter <
        nat_of_bitvector … program_counter')
    assumption
  |7,9:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
    <FETCH normalize nodelta <instr normalize nodelta *
    #program_counter_lt' #program_counter_lt_tps' %
    [1,3:
      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
      <FETCH normalize nodelta whd in match ltb; normalize nodelta
      >(le_to_leb_true … program_counter_lt') %
    |2,4:
      assumption
    ]
  |11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
    55,57,59,61,63:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
    <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta *
    #program_counter_lt' #program_counter_lt_tps' %
    try assumption
    [*:
      %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta
      <FETCH normalize nodelta whd in match ltb; normalize nodelta
      >(le_to_leb_true … program_counter_lt') %
    ]
  |10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,
    54,56,58,60,62:
    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    lapply(good_program_witness program_counter reachable_program_counter_witness)
    <FETCH normalize nodelta
    <real_instruction_refl <instr normalize nodelta *
    #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    @(transitive_le
      total_program_size
      ((S program_size') + nat_of_bitvector … program_counter)
      (program_size' + nat_of_bitvector … program_counter') recursive_case)
    normalize in match (S program_size' + nat_of_bitvector … program_counter);
    >plus_n_Sm
    @monotonic_le_plus_r
    change with (
      nat_of_bitvector … program_counter <
        nat_of_bitvector … program_counter')
    assumption
  ]
qed.

definition block_cost ≝
  λcode_memory: BitVectorTrie Byte 16.
  λprogram_counter: Word.
  λtotal_program_size: nat.
  λcost_labels: BitVectorTrie costlabel 16.
  λreachable_program_counter_witness: reachable_program_counter code_memory total_program_size program_counter.
  λgood_program_witness: good_program code_memory total_program_size.
    block_cost' code_memory program_counter total_program_size total_program_size cost_labels
      reachable_program_counter_witness good_program_witness true ?.
  @le_plus_n_r
qed.

lemma fetch_program_counter_n_Sn:
  ∀instruction: instruction.
  ∀program_counter, program_counter': Word.
  ∀ticks, n: nat.
  ∀code_memory: BitVectorTrie Byte 16.
    Some … program_counter = fetch_program_counter_n n code_memory (zero 16) →
      〈instruction,program_counter',ticks〉 = fetch code_memory program_counter →
        nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' →
          Some … program_counter' = fetch_program_counter_n (S n) code_memory (zero …).
  #instruction #program_counter #program_counter' #ticks #n #code_memory
  #fetch_program_counter_n_hyp #fetch_hyp #lt_hyp
  whd in match (fetch_program_counter_n (S n) code_memory (zero …));
  <fetch_program_counter_n_hyp normalize nodelta
  <fetch_hyp normalize nodelta
  change with (
    leb (S (nat_of_bitvector … program_counter)) (nat_of_bitvector … program_counter')
  ) in match (ltb (nat_of_bitvector … program_counter) (nat_of_bitvector … program_counter'));
  >(le_to_leb_true … lt_hyp) %
qed.

let rec traverse_code_internal
  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
      (reachable_program_counter_witness:
          ∀lbl: costlabel.
          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
            reachable_program_counter code_memory fixed_program_size program_counter)
        (good_program_witness: good_program code_memory fixed_program_size)
        on program_size: identifier_map CostTag nat ≝
  match program_size with
  [ O ⇒ empty_map …
  | S program_size ⇒
    let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with
    [ None ⇒ λlookup_refl. cost_mapping
    | Some lbl ⇒ λlookup_refl.
      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
        add … cost_mapping lbl cost
    ] (refl … (lookup_opt … program_counter cost_labels))
  ].
  [1:
    @(reachable_program_counter_witness lbl)
    assumption
  |2:
    assumption
  ]
qed.

definition traverse_code ≝
  λcode_memory: BitVectorTrie Byte 16.
  λcost_labels: BitVectorTrie costlabel 16.
  λprogram_size: nat.
  λreachable_program_counter_witness:
          ∀lbl: costlabel.
          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
            reachable_program_counter code_memory program_size program_counter.
  λgood_program_witness: good_program code_memory program_size.
    traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
  
definition compute_costs ≝
  λprogram: list Byte.
  λcost_labels: BitVectorTrie costlabel 16.
  λreachable_program_witness.
  λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
    let program_size ≝ |program| + 1 in
    let code_memory ≝ load_code_memory program in
      traverse_code code_memory cost_labels program_size reachable_program_witness ?.
  @good_program_witness
qed.