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

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

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

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