include "common/CostLabel.ma".
include "common/LabelledObjects.ma".
include "common/AST.ma".
include "joint/String.ma".
include "ASM/BitVectorTrie.ma".

definition Identifier ≝ identifier ASMTag.
definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].

inductive addressing_mode: Type[0] ≝
  DIRECT: Byte → addressing_mode
| INDIRECT: Bit → addressing_mode
| EXT_INDIRECT: Bit → addressing_mode
| REGISTER: BitVector 3 → addressing_mode
| ACC_A: addressing_mode
| ACC_B: addressing_mode
| DPTR: addressing_mode
| DATA: Byte → addressing_mode
| DATA16: Word → addressing_mode
| ACC_DPTR: addressing_mode
| ACC_PC: addressing_mode
| EXT_INDIRECT_DPTR: addressing_mode
| INDIRECT_DPTR: addressing_mode
| CARRY: addressing_mode
| BIT_ADDR: Byte → addressing_mode
| N_BIT_ADDR: Byte → addressing_mode
| RELATIVE: Byte → addressing_mode
| ADDR11: Word11 → addressing_mode
| ADDR16: Word → addressing_mode.

definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
  λa, b: addressing_mode.
  match a with
  [ DIRECT d ⇒
    match b with
    [ DIRECT e ⇒ eq_bv ? d e
    | _ ⇒ false
    ]
  | INDIRECT b' ⇒
    match b with
    [ INDIRECT e ⇒ eq_b b' e
    | _ ⇒ false
    ]
  | EXT_INDIRECT b' ⇒
    match b with
    [ EXT_INDIRECT e ⇒ eq_b b' e
    | _ ⇒ false
    ]
  | REGISTER bv ⇒
    match b with
    [ REGISTER bv' ⇒ eq_bv ? bv bv'
    | _ ⇒ false
    ]
  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
  | DATA b' ⇒
    match b with
    [ DATA e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | DATA16 w ⇒ 
    match b with
    [ DATA16 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
  | BIT_ADDR b' ⇒
    match b with
    [ BIT_ADDR e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | N_BIT_ADDR b' ⇒ 
    match b with
    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | RELATIVE n ⇒
    match b with
    [ RELATIVE e ⇒ eq_bv ? n e
    | _ ⇒ false
    ]
  | ADDR11 w ⇒
    match b with
    [ ADDR11 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  | ADDR16 w ⇒
    match b with
    [ ADDR16 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  ].

lemma eq_addressing_mode_refl:
  ∀a. eq_addressing_mode a a = true.
  #a
  cases a try #arg1 try #arg2
  try @eq_bv_refl try @eq_b_refl
  try normalize %
qed.

(* dpm: renamed register to registr to avoid clash with brian's types *)
inductive addressing_mode_tag : Type[0] ≝
  direct: addressing_mode_tag
| indirect: addressing_mode_tag
| ext_indirect: addressing_mode_tag
| registr: addressing_mode_tag
| acc_a: addressing_mode_tag
| acc_b: addressing_mode_tag
| dptr: addressing_mode_tag
| data: addressing_mode_tag
| data16: addressing_mode_tag
| acc_dptr: addressing_mode_tag
| acc_pc: addressing_mode_tag
| ext_indirect_dptr: addressing_mode_tag
| indirect_dptr: addressing_mode_tag
| carry: addressing_mode_tag
| bit_addr: addressing_mode_tag
| n_bit_addr: addressing_mode_tag
| relative: addressing_mode_tag
| addr11: addressing_mode_tag
| addr16: addressing_mode_tag.

definition eq_a ≝
  λa, b: addressing_mode_tag.
    match a with
      [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
      | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
      | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
      | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
      | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
      | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
      | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
      | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
      | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
      | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
      | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
      | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
      | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
      | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
      ].

lemma eq_a_to_eq:
  ∀a,b.
    eq_a a b = true → a = b.
 #a #b
 cases a cases b
 #K
 try cases (eq_true_false K)
 %
qed.

lemma eq_a_reflexive:
  ∀a. eq_a a a = true.
  #a cases a %
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
  ].

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.

(* to avoid expansion... *)
let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
  match d with
   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]
   ].

lemma is_a_decidable:
  ∀hd.
  ∀element.
    is_a hd element = true ∨ is_a hd element = false.
  #hd #element //
qed.

let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
 match l return λm.λ_:Vector addressing_mode_tag m.bool with
  [ VEmpty ⇒ false
  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
     is_a he A ∨ is_in ? tl A ].

definition is_in_cons_elim:
 ∀len.∀hd,tl.∀m:addressing_mode
  .is_in (S len) (hd:::tl) m →
    (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
 cases (is_a hd am) in ISIN; /2/
qed.

lemma is_in_monotonic_wrt_append:
  ∀m, n: nat.
  ∀p: Vector addressing_mode_tag m.
  ∀q: Vector addressing_mode_tag n.
  ∀to_search: addressing_mode.
    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
  #m #n #p #q #to_search #assm
  elim q try assumption
  #n' #hd #tl #inductive_hypothesis
  normalize
  cases (is_a ??) try @I
  >inductive_hypothesis @I
qed.

corollary is_in_hd_tl:
  ∀to_search: addressing_mode.
  ∀hd: addressing_mode_tag.
  ∀n: nat.
  ∀v: Vector addressing_mode_tag n.
    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
  #to_search #hd #n #v
  elim v
  [1:
    #absurd
    normalize in absurd; cases absurd
  |2:
    #n' #hd' #tl #inductive_hypothesis #assm
    >vector_cons_append >(vector_cons_append … hd' tl)
    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
    assumption
  ]
qed.

lemma is_a_to_mem_to_is_in:
 ∀he,a,m,q.
   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
 #he #a #m #q
 elim q
 [1:
   #_ #K assumption
 |2:
   #m' #t #q' #II #H1 #H2
   normalize
   change with (orb ??) in H2:(??%?);
   cases (inclusive_disjunction_true … H2)
   [1:
     #K
     <(eq_a_to_eq … K) >H1 %
   |2:
     #K
     >II
     try assumption
     cases (is_a t a)
     normalize
     %
   ]
 ]
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.

record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
{
  subaddressing_modeel:> addressing_mode;
  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
}.

coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].

coercion mk_subaddressing_mode :
 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.

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.

(* XXX: move back into ASM.ma *)
lemma subvector_with_to_subvector_with_tl:
  ∀n: nat.
  ∀m: nat.
  ∀v.
  ∀fixed_v.
  ∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v).
  ∀n': nat.
  ∀hd: addressing_mode_tag.
  ∀tl: Vector addressing_mode_tag n'.
  ∀m_refl: S n'=n.
  ∀v_refl: v≃hd:::tl.
   subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v.
  #n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl
  generalize in match proof; destruct
  whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
  cases (mem … eq_a ? fixed_v hd) normalize nodelta
  [1:
    whd in match (subvector_with … eq_a tl fixed_v);
    #assm assumption
  |2:
    normalize in ⊢ (% → ?);
    #absurd cases absurd
  ]
qed.

let rec subaddressing_mode_elim_type
  (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v)
    (Q: fixed_v → Prop)
     (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. Q origaddr
  | VCons n' hd tl ⇒ λm_refl. λv_refl.
    let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ?
    in
    match hd return λa: addressing_mode_tag. a = hd → ? with
    [ addr11            ⇒ λhd_refl. (∀w: Word11.      Q (ADDR11 w)) → tail_call
    | addr16            ⇒ λhd_refl. (∀w: Word.        Q (ADDR16 w)) → tail_call
    | direct            ⇒ λhd_refl. (∀w: Byte.        Q (DIRECT w)) → tail_call
    | indirect          ⇒ λhd_refl. (∀w: Bit.         Q (INDIRECT w)) → tail_call
    | ext_indirect      ⇒ λhd_refl. (∀w: Bit.         Q (EXT_INDIRECT w)) → tail_call
    | acc_a             ⇒ λhd_refl.                  Q ACC_A → tail_call
    | registr           ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call
    | acc_b             ⇒ λhd_refl.                  Q ACC_B → tail_call
    | dptr              ⇒ λhd_refl.                  Q DPTR → tail_call
    | data              ⇒ λhd_refl. (∀w: Byte.        Q (DATA w))  → tail_call
    | data16            ⇒ λhd_refl. (∀w: Word.        Q (DATA16 w)) → tail_call 
    | acc_dptr          ⇒ λhd_refl.                  Q ACC_DPTR → tail_call 
    | acc_pc            ⇒ λhd_refl.                  Q ACC_PC → tail_call
    | ext_indirect_dptr ⇒ λhd_refl.                  Q EXT_INDIRECT_DPTR → tail_call
    | indirect_dptr     ⇒ λhd_refl.                  Q INDIRECT_DPTR → tail_call
    | carry             ⇒ λhd_refl.                  Q CARRY → tail_call
    | bit_addr          ⇒ λhd_refl. (∀w: Byte.        Q (BIT_ADDR w)) → tail_call
    | n_bit_addr        ⇒ λhd_refl. (∀w: Byte.        Q (N_BIT_ADDR w)) → tail_call
    | relative          ⇒ λhd_refl. (∀w: Byte.        Q (RELATIVE w)) → tail_call
    ] (refl … hd)
  ] (refl … n) (refl_jmeq … v).
  [20:
    @(subvector_with_to_subvector_with_tl … proof … m_refl v_refl)
  ]
  @(is_in_subvector_is_in_supervector … proof)
  destruct @I
qed.

lemma subaddressing_mode_elim0:
  ∀n: nat.
  ∀v: Vector addressing_mode_tag (S n).
  ∀addr: v.
  ∀Q: v → Prop.
  ∀m,w,H.
  (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) → 
   subaddressing_mode_elim_type n v addr Q m w H.
  #n #v #addr #Q #m #w elim w
  [1:
    /2/
  |2:
    #n' #hd #tl #IH cases hd #H
    #INV whd #PO @IH #xaddr cases xaddr *
    try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
    @ALREADYSEEN
  ]
qed.

lemma subaddressing_mode_elim:
  ∀n: nat.
  ∀v: Vector addressing_mode_tag (S n).
  ∀addr: v.
  ∀Q: v → Prop.
   subaddressing_mode_elim_type n v addr Q (S n) v ?.
  [1:
    #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
  |2:
    @subvector_with_refl @eq_a_reflexive
  ]
qed.
 
inductive preinstruction (A: Type[0]) : Type[0] ≝
  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
| DA: [[acc_a]] → preinstruction A

(* conditional jumps *)
| JC: A → preinstruction A
| JNC: A → preinstruction A
| JB: [[bit_addr]] → A → preinstruction A
| JNB: [[bit_addr]] → A → preinstruction A
| JBC: [[bit_addr]] → A → preinstruction A
| JZ: A → preinstruction A
| JNZ: A → preinstruction A
| CJNE:
   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
| DJNZ: [[registr ; direct]] → A → preinstruction A
 (* logical operations *)
| ANL:
   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
   [[direct]] × [[ acc_a ; data ]] ⊎
   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
| ORL:
   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
   [[direct]] × [[ acc_a ; data ]] ⊎
   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
| XRL:
   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
   [[direct]] × [[ acc_a ; data ]] → preinstruction A
| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
| RL: [[acc_a]] → preinstruction A
| RLC: [[acc_a]] → preinstruction A
| RR: [[acc_a]] → preinstruction A
| RRC: [[acc_a]] → preinstruction A
| SWAP: [[acc_a]] → preinstruction A

 (* data transfer *)
| MOV:
    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
    [[dptr]] × [[data16]] ⊎
    [[carry]] × [[bit_addr]] ⊎
    [[bit_addr]] × [[carry]] → preinstruction A
| MOVX: 
    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
| SETB: [[ carry ; bit_addr ]] → preinstruction A
| PUSH: [[direct]] → preinstruction A
| POP: [[direct]] → preinstruction A
| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
| XCHD: [[acc_a]] → [[indirect]] → preinstruction A

 (* program branching *)
| RET: preinstruction A
| RETI: preinstruction A
| NOP: preinstruction A
| JMP: [[acc_dptr]] → preinstruction A.

definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
  λi, j.
  match i with
  [ ADD arg1 arg2 ⇒
    match j with
    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | ADDC arg1 arg2 ⇒
    match j with
    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | SUBB arg1 arg2 ⇒
    match j with
    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | INC arg ⇒
    match j with
    [ INC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | DEC arg ⇒
    match j with
    [ DEC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | MUL arg1 arg2 ⇒
    match j with
    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DIV arg1 arg2 ⇒
    match j with
    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DA arg ⇒
    match j with
    [ DA arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JC arg ⇒
    match j with
    [ JC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JNC arg ⇒
    match j with
    [ JNC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JB arg1 arg2 ⇒
    match j with
    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JNB arg1 arg2 ⇒
    match j with
    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JBC arg1 arg2 ⇒
    match j with
    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JZ arg ⇒
    match j with
    [ JZ arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JNZ arg ⇒
    match j with
    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JMP arg ⇒
    match j with
    [ JMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | CJNE arg1 arg2 ⇒
    match j with
    [ CJNE arg1' arg2' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DJNZ arg1 arg2 ⇒
    match j with
    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | CLR arg ⇒
    match j with
    [ CLR arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | CPL arg ⇒
    match j with
    [ CPL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RL arg ⇒
    match j with
    [ RL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RLC arg ⇒
    match j with
    [ RLC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RR arg ⇒
    match j with
    [ RR arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RRC arg ⇒
    match j with
    [ RRC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SWAP arg ⇒
    match j with
    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SETB arg ⇒
    match j with
    [ SETB arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | PUSH arg ⇒
    match j with
    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | POP arg ⇒
    match j with
    [ POP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | XCH arg1 arg2 ⇒
    match j with
    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | XCHD arg1 arg2 ⇒
    match j with
    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
  | MOVX arg ⇒
    match j with
    [ MOVX arg' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | XRL arg ⇒
    match j with
    [ XRL arg' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | ORL arg ⇒
    match j with
    [ ORL arg' ⇒
      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | ANL arg ⇒
    match j with
    [ ANL arg' ⇒
      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | MOV arg ⇒
    match j with
    [ MOV arg' ⇒
      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
        sum_eq_5 arg arg'
    | _ ⇒ false
    ]
  ].

lemma eq_preinstruction_refl:
  ∀i.
    eq_preinstruction i i = true.
  #i cases i try #arg1 try #arg2
  try @eq_addressing_mode_refl
  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    whd in ⊢ (??%?); try %
    >eq_addressing_mode_refl
    >eq_addressing_mode_refl %
  |13,15:
    whd in ⊢ (??%?);
    cases arg1
    [*:
      #arg1_left normalize nodelta
      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
    ]
  |11,12:
    whd in ⊢ (??%?);
    cases arg1
    [1:
      #arg1_left normalize nodelta 
      >(eq_sum_refl …)
      [1: % | 2,3: #arg @eq_prod_refl ]
      @eq_addressing_mode_refl
    |2:
      #arg1_left normalize nodelta
      @eq_prod_refl [*: @eq_addressing_mode_refl ]
    |3:
      #arg1_left normalize nodelta
      >(eq_sum_refl …)
      [1:
        %
      |2,3:
        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
      ]
    |4:
      #arg1_left normalize nodelta
      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
    ]
  |14:
    whd in ⊢ (??%?);
    cases arg1
    [1:
      #arg1_left normalize nodelta
      @eq_sum_refl
      [1:
        #arg @eq_sum_refl
        [1:
          #arg @eq_sum_refl
          [1:
            #arg @eq_sum_refl
            [1:
              #arg @eq_prod_refl
              [*:
                @eq_addressing_mode_refl
              ]
            |2:
              #arg @eq_prod_refl
              [*:
                #arg @eq_addressing_mode_refl
              ]
            ]
          |2:
            #arg @eq_prod_refl
            [*:
              #arg @eq_addressing_mode_refl
            ]
          ]
        |2:
          #arg @eq_prod_refl
          [*:
            #arg @eq_addressing_mode_refl
          ]
        ]
      |2:
        #arg @eq_prod_refl
        [*:
          #arg @eq_addressing_mode_refl
        ]
      ]
    |2:
      #arg1_right normalize nodelta
      @eq_prod_refl
      [*:
        #arg @eq_addressing_mode_refl
      ]
    ]
  |*:
    whd in ⊢ (??%?);
    cases arg1
    [*:
      #arg1 >eq_sum_refl
      [1,4:
        @eq_addressing_mode_refl
      |2,3,5,6:
        #arg @eq_prod_refl
        [*:
          #arg @eq_addressing_mode_refl
        ]
      ]
    ]
  ]
qed.

inductive instruction: Type[0] ≝
  | ACALL: [[addr11]] → instruction
  | LCALL: [[addr16]] → instruction
  | AJMP: [[addr11]] → instruction
  | LJMP: [[addr16]] → instruction
  | SJMP: [[relative]] → instruction
  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
  | RealInstruction: preinstruction [[ relative ]] → instruction.
  
coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
  RealInstruction on _p: preinstruction ? to instruction.

definition eq_instruction: instruction → instruction → bool ≝
  λi, j.
  match i with
  [ ACALL arg ⇒
    match j with
    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | LCALL arg ⇒
    match j with
    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | AJMP arg ⇒ 
    match j with
    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | LJMP arg ⇒
    match j with
    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SJMP arg ⇒ 
    match j with
    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | MOVC arg1 arg2 ⇒
    match j with
    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | RealInstruction instr ⇒
    match j with
    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
    | _ ⇒ false
    ]
  ].
  
lemma eq_instruction_refl:
  ∀i. eq_instruction i i = true.
  #i cases i [*: #arg1 ]
  try @eq_addressing_mode_refl
  try @eq_preinstruction_refl
  #arg2 whd in ⊢ (??%?);
  >eq_addressing_mode_refl >eq_addressing_mode_refl %
qed.

lemma eq_instruction_to_eq:
  ∀i1, i2: instruction.
    eq_instruction i1 i2 = true → i1 ≃ i2.
  #i1 #i2
  cases i1 cases i2 cases daemon (* easy but tedious
  [1,10,19,28,37,46:
    #arg1 #arg2
    whd in match (eq_instruction ??);
    cases arg1 #subaddressing_mode
    cases subaddressing_mode
    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
    #word11 #irrelevant
    cases arg2 #subaddressing_mode
    cases subaddressing_mode
    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
    #word11' #irrelevant normalize nodelta
    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
qed.

inductive word_side : Type[0] ≝ HIGH : word_side | LOW : word_side.

inductive pseudo_instruction: Type[0] ≝
  | Instruction: preinstruction Identifier → pseudo_instruction
  | Comment: String → pseudo_instruction
  | Cost: costlabel → pseudo_instruction
  | Jmp: Identifier → pseudo_instruction
  | Jnz : [[acc_a]] → Identifier → Identifier → pseudo_instruction
  | Call: Identifier → pseudo_instruction
  | Mov: ([[dptr]] ⊎ ([[ acc_a ; direct ; registr ]] × word_side)) →
    Identifier → Word → pseudo_instruction.

definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.

definition assembly_program ≝ list instruction.

definition fetch_pseudo_instruction:
 ∀code_mem:list labelled_instruction. ∀pc:Word.
  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
  λcode_mem.
  λpc: Word.
  λpc_ok.
    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
      〈instr, new_pc〉.

lemma snd_fetch_pseudo_instruction:
 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
 #lft #rgt #_ %
qed.

lemma fetch_pseudo_instruction_vsplit:
 ∀instr_list,ppc,ppc_ok.
  ∃pre,suff,lbl.
   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
#EQ %{lbl0} @EQ
qed.

lemma fetch_pseudo_instruction_append:
 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
 cut (|l1| + nat_of_bitvector … ppc < 2^16)
 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] 
 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
 #lbl #instr normalize nodelta >add_associative %
qed.

(* labels & instructions *)
definition instruction_has_label ≝ 
  λid: Identifier.
  λi.
  match i with
  [ Jmp j ⇒ j = id
  | Call j ⇒ j = id
  | Instruction instr ⇒
    match instr with
    [ JC j ⇒ j = id
    | JNC j ⇒ j = id
    | JZ j ⇒ j = id
    | JNZ j ⇒ j = id
    | JB _ j ⇒ j = id
    | JNB _ j ⇒ j = id
    | JBC _ j ⇒ j = id
    | DJNZ _ j ⇒ j = id
    | CJNE _ j ⇒ j = id
    | _ ⇒ False
    ]
  | _ ⇒ False
  ].

(* If instruction i is a jump, then there will be something in the policy at
 * position i *)
definition is_jump' ≝
  λx:preinstruction Identifier.
  match x with
  [ JC _ ⇒ true
  | JNC _ ⇒ true
  | JZ _ ⇒ true
  | JNZ _ ⇒ true
  | JB _ _ ⇒ true
  | JNB _ _ ⇒ true
  | JBC _ _ ⇒ true
  | CJNE _ _ ⇒ true
  | DJNZ _ _ ⇒ true
  | _ ⇒ false
  ].

definition is_relative_jump ≝
  λinstr:pseudo_instruction.
  match instr with
  [ Instruction i ⇒ is_jump' i
  | _             ⇒ false
  ].
    
definition is_jump ≝
  λinstr:pseudo_instruction.
  match instr with
  [ Instruction i   ⇒ is_jump' i
  | Call _ ⇒ true
  | Jmp _ ⇒ true
  | _ ⇒ false
  ].

definition is_call ≝
  λinstr:pseudo_instruction.
  match instr with
  [ Call _ ⇒ true
  | _ ⇒ false
  ].
  
definition is_jump_to ≝
  λx:pseudo_instruction.λd:Identifier.
  match x with
  [ Instruction i ⇒ match i with
    [ JC j ⇒ d = j
    | JNC j ⇒ d = j
    | JZ j ⇒ d = j
    | JNZ j ⇒ d = j
    | JB _ j ⇒ d = j
    | JNB _ j ⇒ d = j
    | JBC _ j ⇒ d = j
    | CJNE _ j ⇒ d = j
    | DJNZ _ j ⇒ d = j
    | _ ⇒ False
    ]
  | Call c ⇒ d = c
  | Jmp j ⇒ d = j
  | _ ⇒ False
  ].

definition is_well_labelled_p ≝
  λinstr_list.
  ∀id: Identifier.
  ∀ppc.
  ∀ppc_ok.
  ∀i.
    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
      (instruction_has_label id i →
        occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
      (is_jump_to i id →
        occurs_exactly_once ASMTag pseudo_instruction id instr_list).

definition asm_cost_label : ∀mem : list labelled_instruction.
  (Σw : Word.nat_of_bitvector … w < |mem|) → option costlabel ≝
λmem,w_prf.
match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with
[ Cost c ⇒ Some ? c
| _ ⇒ None ?
].

(* XXX JHM: avoid magic numbers! *)
definition ADDRESS_WIDTH ≝ 16. 
definition MAX_CODE_SIZE ≝ 2^ADDRESS_WIDTH. 

definition code_size_p : list labelled_instruction → Prop ≝ 
  λcode. S (|code|) < MAX_CODE_SIZE. 
  
definition code_size_opt : ∀code. option (code_size_p code) ≝ 
  λcode. nat_bound_opt MAX_CODE_SIZE (S (|code|)). 

(* The first associative list assigns symbol names to addresses in data memory.
   The second associative list assigns to Identifiers meant to be entry points
   of functions the name of the function (that lives in a different namespace) *)

record pseudo_assembly_program : Type[0] ≝
{ preamble : list (Identifier × Word)
; code : list labelled_instruction
; code_size_ok: code_size_p code
; renamed_symbols : list (Identifier × ident)
; final_label : Identifier
(* properties *)
; asm_injective_costlabels :
  partial_injection … (asm_cost_label code)
; well_labelled_p : is_well_labelled_p code
}.

definition object_code ≝ list Byte.

include alias "ASM/BitVectorTrie.ma".
include alias "ASM/Arithmetic.ma".

definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
  λpmem: BitVectorTrie Byte 16.
  λpc: Word.
    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.

definition load_code_memory0:
 ∀program: object_code. Σres: BitVectorTrie Byte 16.
  let program_size ≝ |program| in
   program_size ≤ 2^16 →
    ∀pc. ∀pc_ok: pc < program_size.
     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
≝
 λprogram. \snd
  (foldl_strong ?
   (λprefix.
     Σres: nat × Word × (BitVectorTrie Byte 16).
      let 〈i,bvi,mem〉 ≝ res in
      i = |prefix| ∧ bvi = bitvector_of_nat … i ∧
      (i ≤ 2^16 →
        ∀pc. ∀pc_ok: pc < |prefix|.
         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
   program 
   (λprefix,v,tl,prf,i_mem.
     let 〈i,bvi,mem〉 ≝ i_mem in
      〈S i,increment … bvi,insert … bvi v mem〉)
  〈0,zero ?,Stub Byte 16〉).
[3: cases (foldl_strong ? (λprefix.Σres.?) ???) ** #i #bvi #mem ** #H1 #H3 >H1 #H2 @H2
| % // % // (*#_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))*)
| cases i_mem in p; ** #i' #bvi' #mem' normalize nodelta #H #EQ destruct(EQ)
  cases H -H * #H1 #H3 #H2 destruct (p1) %
  [ % [ >length_append >H1 normalize //
      | >increment_zero_bitvector_of_nat_1 >H3 <add_bitvector_of_nat % ]
  | #LE #pc #pc_ok
    cases (le_to_or_lt_eq … pc_ok)
    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
      <H1 <plus_n_O whd in ⊢ (???%); //
    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix
      [2: /2 by lt_plus_to_lt_l/]
      >H2 [2: @(transitive_le … LE) //]
      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false % >H3
      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
qed.

definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
 λprogram.load_code_memory0 program.

lemma load_code_memory_ok:
 ∀program: object_code.
  let program_size ≝ |program| in
   program_size ≤ 2^16 →
    ∀pc. ∀pc_ok: pc < program_size.
     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
whd in match load_code_memory; normalize nodelta #program @pi2
qed.


definition costlabel_map ≝ BitVectorTrie costlabel 16. (* XXX *)
definition symboltable_type ≝ BitVectorTrie ident 16.  (* XXX *)
record labelled_object_code : Type[0] ≝
{ oc : object_code
; cm: BitVectorTrie Byte 16
; cm_def: cm = load_code_memory oc
; costlabels : costlabel_map
; symboltable : symboltable_type
; final_pc : Word
(* properties *)
; oc_injective_costlabels :
  partial_injection … (λpc.lookup_opt … pc costlabels)
; oc_costlabels_are_zero : (* this will imply that cost labels are only assigned to nops *)
  ∀ppc,l.lookup_opt … ppc costlabels = Some ? l →
  lookup … ppc cm (zero …) = zero …
}.