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