include "arithmetics/nat.ma".
include "basics/jmeq.ma".

include "ASM/String.ma".
include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".
include "joint/BEValues.ma".
include "ASM/BitVectorTrie.ma".

definition int_size ≝ bitvector_of_nat 8 1.
definition ptr_size ≝ bitvector_of_nat 8 2.
definition alignment ≝ None.

(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
        not further back in the translation chain.                            *)
inductive OpAccs: Type[0] ≝
  Mul: OpAccs
| DivuModu: OpAccs.

inductive Op1: Type[0] ≝
  Cmpl: Op1
| Inc: Op1
| Rl: Op1. (* TODO: implement left rotation *)

inductive Op2: Type[0] ≝
  Add: Op2
| Addc: Op2
| Sub: Op2
| And: Op2
| Or: Op2
| Xor: Op2.

(* dpm: maybe useless? *)
inductive Register: Type[0] ≝
  Register00: Register
| Register01: Register
| Register02: Register
| Register03: Register
| Register04: Register
| Register05: Register
| Register06: Register
| Register07: Register
| Register10: Register
| Register11: Register
| Register12: Register
| Register13: Register
| Register14: Register
| Register15: Register
| Register16: Register
| Register17: Register
| Register20: Register
| Register21: Register
| Register22: Register
| Register23: Register
| Register24: Register
| Register25: Register
| Register26: Register
| Register27: Register
| Register30: Register
| Register31: Register
| Register32: Register
| Register33: Register
| Register34: Register
| Register35: Register
| Register36: Register
| Register37: Register
| RegisterA: Register
| RegisterB: Register
| RegisterDPL: Register
| RegisterDPH: Register
| RegisterCarry: Register.

definition nat_of_register: Register → nat ≝
  λr: Register.
  match r with
  [ Register00 ⇒ 0
  | Register01 ⇒ 1
  | Register02 ⇒ 2
  | Register03 ⇒ 3
  | Register04 ⇒ 4
  | Register05 ⇒ 5
  | Register06 ⇒ 6
  | Register07 ⇒ 7
  | Register10 ⇒ 8
  | Register11 ⇒ 9
  | Register12 ⇒ 10
  | Register13 ⇒ 11
  | Register14 ⇒ 12
  | Register15 ⇒ 13
  | Register16 ⇒ 14
  | Register17 ⇒ 15
  | Register20 ⇒ 16
  | Register21 ⇒ 17
  | Register22 ⇒ 18
  | Register23 ⇒ 19
  | Register24 ⇒ 20
  | Register25 ⇒ 21
  | Register26 ⇒ 22
  | Register27 ⇒ 23
  | Register30 ⇒ 24
  | Register31 ⇒ 25
  | Register32 ⇒ 26
  | Register33 ⇒ 27
  | Register34 ⇒ 28
  | Register35 ⇒ 29
  | Register36 ⇒ 30
  | Register37 ⇒ 31
  | RegisterA ⇒ 32
  | RegisterB ⇒ 33
  | RegisterDPL ⇒ 34
  | RegisterDPH ⇒ 35
  | RegisterCarry ⇒ 36 (* was -1, increment as needed *)
  ].
  
definition physical_register_count ≝ 36.

definition bitvector_of_register: Register → BitVector 6 ≝
  λregister.
    bitvector_of_nat ? (nat_of_register register).

definition eq_Register: Register → Register → bool ≝
  λr, s: Register.
  let r_as_nat ≝ nat_of_register r in
  let s_as_nat ≝ nat_of_register s in
    eqb r_as_nat s_as_nat.

axiom print_register: Register → String.

(* dpm: registers for stack manipulation *)
definition RegisterSST ≝ Register10.
definition RegisterST0 ≝ Register02.
definition RegisterST1 ≝ Register03.
definition RegisterST2 ≝ Register04.
definition RegisterST3 ≝ Register05.
definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
definition RegisterSPL ≝ Register06.
definition RegisterSPH ≝ Register07.
definition RegisterParams: list Register ≝
  [ Register30; Register31; Register32; Register33;
    Register34; Register35; Register36; Register37 ].
definition Registers ≝
  [Register00; Register01; Register02; Register03; Register04;
   Register05; Register06; Register07; Register10; Register11; 
   Register12; Register13; Register14; Register15; Register16;
   Register17; Register20; Register21; Register22; Register23;
   Register24; Register25; Register26; Register27; Register30;
   Register31; Register32; Register33; Register34; Register35;
   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
   RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
   RegisterSST].
definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
definition RegisterCallerSaved ≝
  [Register00; Register01; Register02; Register03; Register04;
   Register05; Register06; Register07; Register10; Register11; 
   Register12; Register13; Register14; Register15; Register16;
   Register17; Register30; Register31; Register32; Register33;
   Register34; Register35; Register36; Register37].
definition RegisterCalleeSaved ≝
  [Register20; Register21; Register22; Register23; Register24;
   Register25; Register26; Register27].
definition RegistersForbidden ≝
  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
   RegisterST2; RegisterST3; RegisterSST].
(* registers minus forbidden *)
definition RegistersAllocatable ≝
  [Register00; Register01; Register02; Register03; Register04;
   Register05; Register06; Register07; Register10; Register11; 
   Register12; Register13; Register14; Register15; Register16;
   Register17; Register20; Register21; Register22; Register23;
   Register24; Register25; Register26; Register27; Register30;
   Register31; Register32; Register33; Register34; Register35;
   Register36; Register37].

definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  λr: Register.
    match r with
    [ Register00 ⇒ REGISTER [[ false; false; false ]]
    | Register01 ⇒ REGISTER [[ false; false; true ]]
    | Register02 ⇒ REGISTER [[ false; true; false ]]
    | Register03 ⇒ REGISTER [[ false; true; true ]]
    | Register04 ⇒ REGISTER [[ true; false; false ]]
    | Register05 ⇒ REGISTER [[ true; false; true ]]
    | Register06 ⇒ REGISTER [[ true; true; false ]]
    | Register07 ⇒ REGISTER [[ true; true; true ]]
    | RegisterA ⇒ ACC_A
    | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
    | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
    | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r)) 
    ].
    [*: normalize
        @ I
    ]
qed.

definition hw_register_env ≝ BitVectorTrie beval 6.
definition empty_hw_register_env: hw_register_env ≝ Stub ….
definition hwreg_retrieve: hw_register_env → Register → beval ≝
 λenv,r. lookup … (bitvector_of_register r) env BVundef.
definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
 λr,v,env. insert … (bitvector_of_register r) v env.
  
record Eval: Type[0] ≝
{
  opaccs: OpAccs → Byte → Byte → Byte × Byte;
  op1: Op1 → Byte → Byte;
  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
}.

axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
axiom op1_implementation: Op1 → Byte → Byte.
axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).

definition eval: Eval ≝
  mk_Eval opaccs_implementation
          op1_implementation
          op2_implementation.