include "ASM/BitVector.ma".
include "common/Identifiers.ma".
include "common/CostLabel.ma".
include "common/LabelledObjects.ma".

axiom ASMTag : String.
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.

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
    ]
  | 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
  | JMP: [[indirect_dptr]] → 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
    ]
  | JMP arg ⇒
    match j with
    [ JMP 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 pseudo_instruction: Type[0] ≝
  | Instruction: preinstruction Identifier → pseudo_instruction
  | Comment: String → pseudo_instruction
  | Cost: costlabel → pseudo_instruction
  | Jmp: Identifier → pseudo_instruction
  | Call: Identifier → pseudo_instruction
  | Mov: [[dptr]] → Identifier → pseudo_instruction.

definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
definition assembly_program ≝ list instruction.
definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).

(* 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
  ].