1
2open HolKernel boolLib bossLib Parse;
3open wordsTheory listTheory;
4
5val _ = new_theory "x64_coretypes";
6
7
8(* ---------------------------------------------------------------------------------- *>
9
10  This theory defines the types and operations over these types for the x64 model.
11
12<* ---------------------------------------------------------------------------------- *)
13
14(* used by the AST *)
15
16val _ = Hol_datatype `Zreg = RAX | RBX | RCX  | RDX  | RSP  | RBP  | RSI  | RDI  |
17                             zR8 | zR9 | zR10 | zR11 | zR12 | zR13 | zR14 | zR15 |
18                             (* nothing decodes to the ghost regsiters, it's just ghost state *)
19                             zGhost_stack_top | zGhost_stack_bottom `;
20
21val _ = Hol_datatype `Zsize = Z8 | Z16 | Z32 | Z64`;
22
23(* used elsewhere *)
24
25val _ = Hol_datatype `
26  Zeflags = Z_CF | Z_PF | Z_AF | Z_ZF | Z_SF | Z_OF `;
27
28val _ = Hol_datatype `
29  Zea =
30      Zea_i of Zsize => word64     (* constant       *)
31    | Zea_r of Zsize => Zreg       (* register name  *)
32    | Zea_m of Zsize => word64     (* memory address *) `;
33
34val _ = Hol_datatype   `iiid = <| proc : num ; program_order_index : num |>`;
35
36
37(* distinctness theorem *)
38
39val ALL_DISTINCT_Zreg = store_thm("ALL_DISTINCT_Zreg",
40  ``ALL_DISTINCT ([RAX;RCX;RDX;RBX;RSP;RBP;RSI;RDI;zR8;zR9;zR10;zR11;
41      zR12;zR13;zR14;zR15;zGhost_stack_top;zGhost_stack_bottom]:Zreg list)``,
42  SRW_TAC[][]);
43
44val _ = export_theory ();
45