Split mips.sail into three file and make use of the new -o option in preparation for adding cheri support in separate files.

3 files changed, 268 insertions, 268 deletions

diff --git a/mips/mips_epilogue.sail b/mips/mips_epilogue.sail
new file mode 100644
index 00000000..ed7d269e
--- /dev/null
+++ b/mips/mips_epilogue.sail
@@ -0,0 +1,11 @@
+
+union ast member unit RI
+function clause decode _ = Some(RI)
+function clause execute (RI) =
+      exit (SignalException (ResI))
+
+end decode
+end execute
+end ast
+
+function option<ast> supported_instructions (instr) = Some(instr)
diff --git a/mips/mips.sail b/mips/mips_insts.sail
index 75c0494c..d6288b15 100644
--- a/mips/mips.sail
+++ b/mips/mips_insts.sail
@@ -1,260 +1,3 @@
-(* bit vectors have indices decreasing from left i.e. msb is highest index *)
-default Order dec
-
-(*(* external functions *)
-val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS (* Sign extend *)
-val extern forall Nat 'n, Nat 'm. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTZ (* Zero extend *)
-*)
-register (bit[64]) PC
-register (bit[64]) nextPC
-
-(* CP0 Registers *)
-
-typedef CauseReg = register bits [ 31 : 0 ] {
-  31       : BD; (* branch delay *)
-  (*30       : Z0;*)
-  29 .. 28 : CE; (* for coprocessor enable exception *)
-  (*27 .. 24 : Z1;*)
-  23       : IV; (* special interrupt vector not supported *)
-  22       : WP; (* watchpoint exception occurred *)
-  (*21 .. 16 : Z2; *)
-  15 .. 8  : IP; (* interrupt pending bits *)
-  (*7        : Z3;*)
-  6 .. 2   : ExcCode; (* code of last exception *)
-  (*1 .. 0   : Z4;*)
-}
-register (bit[32])  CP0Compare
-register (CauseReg) CP0Cause
-register (bit[64])  CP0EPC
-register (bit[64])  CP0ErrorEPC
-register (bit[1])   CP0LLBit
-register (bit[64])  CP0LLAddr
-register (bit[64])  CP0BadVAddr
-
-typedef StatusReg = register bits [31:0] {
-  31 .. 28        : CU;  (* co-processor enable bits *)
-  (* RP/FR/RE/MX/PX not implemented *)
-  22              : BEV; (* use boot exception vectors XXX initialise to one *)
-  (* TS/SR/NMI not implemented *)
-  15 .. 8         : IM;  (* Interrupt mask *)
-  7               : KX;  (* kernel 64-bit enable *)
-  6               : SX;  (* supervisor 64-bit enable *)
-  5               : UX;  (* user 64-bit enable *)
-  4 .. 3          : KSU; (* Processor mode *)
-  2               : ERL; (* error level XXX initialise to one *)
-  1               : EXL; (* exception level *)
-  0               : IE;  (* interrupt enable *)
-}
-register (StatusReg) CP0Status
-
-(* Implementation registers -- not ISA defined *)
-register (bit[1])  branchPending      (* Set by branch instructions to implement branch delay *)
-register (bit[1])  inBranchDelay      (* Needs to be set by outside world when in branch delay slot *)
-register (bit[64]) delayedPC          (* Set by branch instructions to implement branch delay *)
-
-(* General purpose registers *)
-
-register (bit[64]) GPR00 (* should never be read or written *)
-register (bit[64]) GPR01
-register (bit[64]) GPR02
-register (bit[64]) GPR03
-register (bit[64]) GPR04
-register (bit[64]) GPR05
-register (bit[64]) GPR06
-register (bit[64]) GPR07
-register (bit[64]) GPR08
-register (bit[64]) GPR09
-register (bit[64]) GPR10
-register (bit[64]) GPR11
-register (bit[64]) GPR12
-register (bit[64]) GPR13
-register (bit[64]) GPR14
-register (bit[64]) GPR15
-register (bit[64]) GPR16
-register (bit[64]) GPR17
-register (bit[64]) GPR18
-register (bit[64]) GPR19
-register (bit[64]) GPR20
-register (bit[64]) GPR21
-register (bit[64]) GPR22
-register (bit[64]) GPR23
-register (bit[64]) GPR24
-register (bit[64]) GPR25
-register (bit[64]) GPR26
-register (bit[64]) GPR27
-register (bit[64]) GPR28
-register (bit[64]) GPR29
-register (bit[64]) GPR30
-register (bit[64]) GPR31
-
-(* Special registers For MUL/DIV *)
-register (bit[64]) HI
-register (bit[64]) LO
-
-let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
-  [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10,
-  GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20,
-  GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
-  ]
-
-(* Check whether a given 64-bit vector is a properly sign extended 32-bit word *)
-val bit[64] -> bool effect pure NotWordVal
-function bool NotWordVal (word) = 
-    (word[31] ^^ 32) != word[63..32]
-
-val bit[5] -> bit[64] effect {rreg} rGPR
-function bit[64] rGPR idx = {
-         if idx == 0 then 0 else GPR[idx]
-}
-
-val (bit[5], bit[64]) -> unit effect {wreg} wGPR
-function unit wGPR (idx, v) = {
-         if idx == 0 then () else GPR[idx] := v
-}
-
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmem } MEMw_conditional
-val extern unit -> unit effect { barr } MEM_sync
-
-typedef Exception = enumerate
-{
-   Int; Mod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E;
-   XTLBRefillL; XTLBRefillS
-}
-
-(* Return the ISA defined code for an exception condition *)
-function (bit[5]) ExceptionCode ((Exception) ex) =
-   switch (ex)
-   {
-      case Int         -> mask(0x00) (* Interrupt *)
-      case Mod         -> mask(0x01) (* TLB modification exception *)
-      case TLBL        -> mask(0x02) (* TLB exception (load or fetch) *)
-      case TLBS        -> mask(0x03) (* TLB exception (store) *)
-      case AdEL        -> mask(0x04) (* Address error (load or fetch) *)
-      case AdES        -> mask(0x05) (* Address error (store) *)
-      case Sys         -> mask(0x08) (* Syscall *)
-      case Bp          -> mask(0x09) (* Breakpoint *)
-      case ResI        -> mask(0x0a) (* Reserved instruction *)
-      case CpU         -> mask(0x0b) (* Coprocessor Unusable *)
-      case Ov          -> mask(0x0c) (* Arithmetic overflow *)
-      case Tr          -> mask(0x0d) (* Trap *)
-      case C2E         -> mask(0x12) (* C2E coprocessor 2 exception *)
-      case XTLBRefillL -> mask(0x02)
-      case XTLBRefillS -> mask(0x03)
-   }
-
-
-function unit SignalException ((Exception) ex) = 
-  {
-    (* Only update EPC and BD if not already in EXL mode *)
-    if (~ (CP0Status.EXL)) then 
-      {
-        if (inBranchDelay[0]) then
-          {
-            CP0EPC := PC - 4;
-            CP0Cause.BD := 1;
-          }
-        else
-          {
-            CP0EPC := PC;
-            CP0Cause.BD := 0;
-          }
-      };
-
-      (* choose an exception vector to branch to *)
-      vectorOffset := if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) & ~ (CP0Status.EXL) then
-                     0x080
-                  else
-                     0x180;
-      (bit[64]) vectorBase  := if CP0Status.BEV then
-                   0xFFFFFFFFBFC00200
-                else
-                   0xFFFFFFFF80000000;
-      nextPC := vectorBase + EXTS(vectorOffset);
-      CP0Cause.ExcCode      := ExceptionCode(ex);
-      CP0Status.EXL         := 1;
-  }
-
-function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
-  {
-    CP0BadVAddr := badAddr;
-    SignalException(ex);
-  }
-
-typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
-typedef AccessLevel   = enumerate {Kernel; Supervisor; User}
-function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = 
-  {
-    err := (if (accessType == StoreData) then Some(AdES) else Some(AdEL));
-    switch(vAddr[63..62]) {
-      case 0b11 -> switch(vAddr[61..31], vAddr[30..29]) { (* xkseg *)
-        case (0b1111111111111111111111111111111, 0b11) -> (err, None)  (* kseg3 mapped 32-bit compat TODO *)
-        case (0b1111111111111111111111111111111, 0b10) -> (err, None)  (* sseg  mapped 32-bit compat TODO *)
-        case (0b1111111111111111111111111111111, 0b01) -> (None, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
-        case (0b1111111111111111111111111111111, 0b00) -> (None, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
-        case (_, _) -> (err, None)  (* xkseg mapped TODO *)
-      }
-      case 0b10 -> (None, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode which we ignore *)
-      case 0b01 -> (err, None) (* xsseg - supervisor mapped TODO *)
-      case 0b00 -> (err, None) (* xuseg - user mapped TODO *)
-    }
-  }
-
-function bit[64] TranslateOrExit((bit[64]) vAddr, (MemAccessType) accessType) =
-  switch (TranslateAddress(vAddr, accessType)) {
-    case ((Some(ex)), _)    -> (exit (SignalExceptionBadAddr (ex, vAddr)))
-    case (_, (Some(pAddr))) -> pAddr
-  }
-
-typedef regno = bit[5]                      (* a register number *)
-typedef imm16 = bit[16]                     (* 16-bit immediate *)
-typedef regregreg   = (regno, regno, regno) (* a commonly used instruction format with three register operands *)
-typedef regregimm16 = (regno, regno, imm16) (* a commonly used instruction format with two register operands and 16-bit immediate *)
-typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction; illegal_instruction; internal_error }
-(* Used by branch and trap instructions *)
-typedef Comparison = enumerate { 
-  EQ; (* equal *)
-  NE; (* not equal *)
-  GE; (* signed greater than or equal *)
-  GEU;(* unsigned greater than or equal *) 
-  GT; (* signed strictly greater than *) 
-  LE; (* signed less than or equal *) 
-  LT; (* signed strictly less than *) 
-  LTU;(* unsigned less than or qual *) 
-}
-function bool compare ((Comparison)cmp, (bit[64]) valA, (bit[64]) valB) =
-  let valA65 = (0b0 : valA) in (* sail comparisons are signed so extend to 65 bits for unsigned comparisons *)
-  let valB65 = (0b0 : valB) in
-  switch(cmp) {
-    case EQ  -> valA ==   valB
-    case NE  -> valA !=   valB
-    case GE  -> valA >=   valB
-    case GEU -> valA65 >= valB65
-    case GT  -> valA >    valB
-    case LE  -> valA <=   valB
-    case LT  -> valA <    valB
-    case LTU -> valA65 <  valB65
-  }
-typedef WordType = enumerate { B; H; W; D}
-
-function forall Nat 'r, 'r IN {1,2,4,8}.[:'r:] wordWidthBytes((WordType) w) =
-  switch(w) {
-    case B -> 1
-    case H -> 2
-    case W -> 4
-    case D -> 8
-  }
-
-function bool isAddressAligned(addr, (WordType) wordType) =
-  switch (wordType) {
-    case B -> true
-    case H -> (addr[0]    == 0)
-    case W -> (addr[1..0] == 0b00)
-    case D -> (addr[2..0] == 0b000)
-  }
-
 scattered function unit execute
 scattered typedef ast = const union
 
@@ -1657,14 +1400,3 @@ function clause execute (ERET) =
 
 function clause execute (HCF) =
   () (* halt instruction actually executed by interpreter framework *)
-
-union ast member unit RI
-function clause decode _ = Some(RI)
-function clause execute (RI) =
-      exit (SignalException (ResI))
-
-end decode
-end execute
-end ast
-
-function option<ast> supported_instructions (instr) = Some(instr)
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
new file mode 100644
index 00000000..18eec9cc
--- /dev/null
+++ b/mips/mips_prelude.sail
@@ -0,0 +1,257 @@
+(* bit vectors have indices decreasing from left i.e. msb is highest index *)
+default Order dec
+
+(*(* external functions *)
+val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS (* Sign extend *)
+val extern forall Nat 'n, Nat 'm. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTZ (* Zero extend *)
+*)
+register (bit[64]) PC
+register (bit[64]) nextPC
+
+(* CP0 Registers *)
+
+typedef CauseReg = register bits [ 31 : 0 ] {
+  31       : BD; (* branch delay *)
+  (*30       : Z0;*)
+  29 .. 28 : CE; (* for coprocessor enable exception *)
+  (*27 .. 24 : Z1;*)
+  23       : IV; (* special interrupt vector not supported *)
+  22       : WP; (* watchpoint exception occurred *)
+  (*21 .. 16 : Z2; *)
+  15 .. 8  : IP; (* interrupt pending bits *)
+  (*7        : Z3;*)
+  6 .. 2   : ExcCode; (* code of last exception *)
+  (*1 .. 0   : Z4;*)
+}
+register (bit[32])  CP0Compare
+register (CauseReg) CP0Cause
+register (bit[64])  CP0EPC
+register (bit[64])  CP0ErrorEPC
+register (bit[1])   CP0LLBit
+register (bit[64])  CP0LLAddr
+register (bit[64])  CP0BadVAddr
+
+typedef StatusReg = register bits [31:0] {
+  31 .. 28        : CU;  (* co-processor enable bits *)
+  (* RP/FR/RE/MX/PX not implemented *)
+  22              : BEV; (* use boot exception vectors XXX initialise to one *)
+  (* TS/SR/NMI not implemented *)
+  15 .. 8         : IM;  (* Interrupt mask *)
+  7               : KX;  (* kernel 64-bit enable *)
+  6               : SX;  (* supervisor 64-bit enable *)
+  5               : UX;  (* user 64-bit enable *)
+  4 .. 3          : KSU; (* Processor mode *)
+  2               : ERL; (* error level XXX initialise to one *)
+  1               : EXL; (* exception level *)
+  0               : IE;  (* interrupt enable *)
+}
+register (StatusReg) CP0Status
+
+(* Implementation registers -- not ISA defined *)
+register (bit[1])  branchPending      (* Set by branch instructions to implement branch delay *)
+register (bit[1])  inBranchDelay      (* Needs to be set by outside world when in branch delay slot *)
+register (bit[64]) delayedPC          (* Set by branch instructions to implement branch delay *)
+
+(* General purpose registers *)
+
+register (bit[64]) GPR00 (* should never be read or written *)
+register (bit[64]) GPR01
+register (bit[64]) GPR02
+register (bit[64]) GPR03
+register (bit[64]) GPR04
+register (bit[64]) GPR05
+register (bit[64]) GPR06
+register (bit[64]) GPR07
+register (bit[64]) GPR08
+register (bit[64]) GPR09
+register (bit[64]) GPR10
+register (bit[64]) GPR11
+register (bit[64]) GPR12
+register (bit[64]) GPR13
+register (bit[64]) GPR14
+register (bit[64]) GPR15
+register (bit[64]) GPR16
+register (bit[64]) GPR17
+register (bit[64]) GPR18
+register (bit[64]) GPR19
+register (bit[64]) GPR20
+register (bit[64]) GPR21
+register (bit[64]) GPR22
+register (bit[64]) GPR23
+register (bit[64]) GPR24
+register (bit[64]) GPR25
+register (bit[64]) GPR26
+register (bit[64]) GPR27
+register (bit[64]) GPR28
+register (bit[64]) GPR29
+register (bit[64]) GPR30
+register (bit[64]) GPR31
+
+(* Special registers For MUL/DIV *)
+register (bit[64]) HI
+register (bit[64]) LO
+
+let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
+  [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10,
+  GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20,
+  GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
+  ]
+
+(* Check whether a given 64-bit vector is a properly sign extended 32-bit word *)
+val bit[64] -> bool effect pure NotWordVal
+function bool NotWordVal (word) = 
+    (word[31] ^^ 32) != word[63..32]
+
+val bit[5] -> bit[64] effect {rreg} rGPR
+function bit[64] rGPR idx = {
+         if idx == 0 then 0 else GPR[idx]
+}
+
+val (bit[5], bit[64]) -> unit effect {wreg} wGPR
+function unit wGPR (idx, v) = {
+         if idx == 0 then () else GPR[idx] := v
+}
+
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmem } MEMw_conditional
+val extern unit -> unit effect { barr } MEM_sync
+
+typedef Exception = enumerate
+{
+   Int; Mod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E;
+   XTLBRefillL; XTLBRefillS
+}
+
+(* Return the ISA defined code for an exception condition *)
+function (bit[5]) ExceptionCode ((Exception) ex) =
+   switch (ex)
+   {
+      case Int         -> mask(0x00) (* Interrupt *)
+      case Mod         -> mask(0x01) (* TLB modification exception *)
+      case TLBL        -> mask(0x02) (* TLB exception (load or fetch) *)
+      case TLBS        -> mask(0x03) (* TLB exception (store) *)
+      case AdEL        -> mask(0x04) (* Address error (load or fetch) *)
+      case AdES        -> mask(0x05) (* Address error (store) *)
+      case Sys         -> mask(0x08) (* Syscall *)
+      case Bp          -> mask(0x09) (* Breakpoint *)
+      case ResI        -> mask(0x0a) (* Reserved instruction *)
+      case CpU         -> mask(0x0b) (* Coprocessor Unusable *)
+      case Ov          -> mask(0x0c) (* Arithmetic overflow *)
+      case Tr          -> mask(0x0d) (* Trap *)
+      case C2E         -> mask(0x12) (* C2E coprocessor 2 exception *)
+      case XTLBRefillL -> mask(0x02)
+      case XTLBRefillS -> mask(0x03)
+   }
+
+
+function unit SignalException ((Exception) ex) = 
+  {
+    (* Only update EPC and BD if not already in EXL mode *)
+    if (~ (CP0Status.EXL)) then 
+      {
+        if (inBranchDelay[0]) then
+          {
+            CP0EPC := PC - 4;
+            CP0Cause.BD := 1;
+          }
+        else
+          {
+            CP0EPC := PC;
+            CP0Cause.BD := 0;
+          }
+      };
+
+      (* choose an exception vector to branch to *)
+      vectorOffset := if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) & ~ (CP0Status.EXL) then
+                     0x080
+                  else
+                     0x180;
+      (bit[64]) vectorBase  := if CP0Status.BEV then
+                   0xFFFFFFFFBFC00200
+                else
+                   0xFFFFFFFF80000000;
+      nextPC := vectorBase + EXTS(vectorOffset);
+      CP0Cause.ExcCode      := ExceptionCode(ex);
+      CP0Status.EXL         := 1;
+  }
+
+function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
+  {
+    CP0BadVAddr := badAddr;
+    SignalException(ex);
+  }
+
+typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
+typedef AccessLevel   = enumerate {Kernel; Supervisor; User}
+function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = 
+  {
+    err := (if (accessType == StoreData) then Some(AdES) else Some(AdEL));
+    switch(vAddr[63..62]) {
+      case 0b11 -> switch(vAddr[61..31], vAddr[30..29]) { (* xkseg *)
+        case (0b1111111111111111111111111111111, 0b11) -> (err, None)  (* kseg3 mapped 32-bit compat TODO *)
+        case (0b1111111111111111111111111111111, 0b10) -> (err, None)  (* sseg  mapped 32-bit compat TODO *)
+        case (0b1111111111111111111111111111111, 0b01) -> (None, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
+        case (0b1111111111111111111111111111111, 0b00) -> (None, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
+        case (_, _) -> (err, None)  (* xkseg mapped TODO *)
+      }
+      case 0b10 -> (None, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode which we ignore *)
+      case 0b01 -> (err, None) (* xsseg - supervisor mapped TODO *)
+      case 0b00 -> (err, None) (* xuseg - user mapped TODO *)
+    }
+  }
+
+function bit[64] TranslateOrExit((bit[64]) vAddr, (MemAccessType) accessType) =
+  switch (TranslateAddress(vAddr, accessType)) {
+    case ((Some(ex)), _)    -> (exit (SignalExceptionBadAddr (ex, vAddr)))
+    case (_, (Some(pAddr))) -> pAddr
+  }
+
+typedef regno = bit[5]                      (* a register number *)
+typedef imm16 = bit[16]                     (* 16-bit immediate *)
+typedef regregreg   = (regno, regno, regno) (* a commonly used instruction format with three register operands *)
+typedef regregimm16 = (regno, regno, imm16) (* a commonly used instruction format with two register operands and 16-bit immediate *)
+typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction; illegal_instruction; internal_error }
+(* Used by branch and trap instructions *)
+typedef Comparison = enumerate { 
+  EQ; (* equal *)
+  NE; (* not equal *)
+  GE; (* signed greater than or equal *)
+  GEU;(* unsigned greater than or equal *) 
+  GT; (* signed strictly greater than *) 
+  LE; (* signed less than or equal *) 
+  LT; (* signed strictly less than *) 
+  LTU;(* unsigned less than or qual *) 
+}
+function bool compare ((Comparison)cmp, (bit[64]) valA, (bit[64]) valB) =
+  let valA65 = (0b0 : valA) in (* sail comparisons are signed so extend to 65 bits for unsigned comparisons *)
+  let valB65 = (0b0 : valB) in
+  switch(cmp) {
+    case EQ  -> valA ==   valB
+    case NE  -> valA !=   valB
+    case GE  -> valA >=   valB
+    case GEU -> valA65 >= valB65
+    case GT  -> valA >    valB
+    case LE  -> valA <=   valB
+    case LT  -> valA <    valB
+    case LTU -> valA65 <  valB65
+  }
+typedef WordType = enumerate { B; H; W; D}
+
+function forall Nat 'r, 'r IN {1,2,4,8}.[:'r:] wordWidthBytes((WordType) w) =
+  switch(w) {
+    case B -> 1
+    case H -> 2
+    case W -> 4
+    case D -> 8
+  }
+
+function bool isAddressAligned(addr, (WordType) wordType) =
+  switch (wordType) {
+    case B -> true
+    case H -> (addr[0]    == 0)
+    case W -> (addr[1..0] == 0b00)
+    case D -> (addr[2..0] == 0b000)
+  }
+