RISC-V spec, without implicit casts

23 files changed, 260 insertions, 253 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index c67ec3c..a8faf3d 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -50,16 +50,17 @@ overload operator & = {and_vec}
 
 overload operator | = {or_vec}
 
-val cast cast_unit_vec : bit -> bits(1)
+val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
 
-function cast_unit_vec b = match b {
-  bitzero => 0b0,
-  bitone  => 0b1
-}
+val "string_of_bits" : forall 'n. bits('n) -> string
 
-val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
+function string_of_bit(b: bit) -> string =
+  match b {
+    bitzero => "0b0",
+    bitone => "0b1"
+  }
 
-val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
+overload BitStr = {string_of_bits, string_of_bit}
 
 val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
@@ -125,10 +126,10 @@ overload zeros = {zeros_implicit}
 val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
 function ones (n) = sail_ones (n)
 
-val cast bool_to_bits : bool -> bits(1)
+val bool_to_bits : bool -> bits(1)
 function bool_to_bits x = if x then 0b1 else 0b0
 
-val cast bit_to_bool : bit -> bool
+val bit_to_bool : bit -> bool
 function bit_to_bool b = match b {
   bitone  => true,
   bitzero => false
diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
index ec8c96f..5b55e6e 100644
--- a/model/riscv_analysis.sail
+++ b/model/riscv_analysis.sail
@@ -1,11 +1,12 @@
 $include <regfp.sail>
 
 /* in reverse order because inc vectors don't seem to work (bug) */
-let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21",
+let GPRstrs : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21",
   "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x11",
   "x10", "x9", "x8", "x7", "x6", "x5", "x4", "x3", "x2", "x1", "x0"
   ]
 
+function GPRstr(i: bits(5)) -> string = GPRstrs[unsigned(i)]
 
 let CIA_fp = RFull("CIA")
 let NIA_fp = RFull("NIA")
@@ -23,40 +24,40 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
   match instr {
      EBREAK() => (),
      UTYPE(imm, rd, op) => {
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
      },
      RISCV_JAL(imm, rd) => {
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
             let offset : bits(64) = EXTS(imm) in
             Nias = [| NIAFP_concrete_address (PC + offset) |];
             ik = IK_branch();
      },
      RISCV_JALR(imm, rs, rd) => {
-            if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
             let offset : bits(64) = EXTS(imm) in
             Nias = [| NIAFP_indirect_address() |];
             ik = IK_branch();
      },
      BTYPE(imm, rs2, rs1, op) => {
-            if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
             ik = IK_branch();
             let offset : bits(64) = EXTS(imm) in
             Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
       },
       ITYPE(imm, rs, rd, op) => {
-            if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       SHIFTIOP(imm, rs, rd, op) => {
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       RTYPE(rs2, rs1, rd, op) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       CSR(csr, rs1, rd, is_imm, op) => {
                let isWrite : bool = match op {
@@ -65,16 +66,16 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                };
                iR = RFull(csr_name(csr)) :: iR;
                if ~(is_imm) then {
-                  iR = RFull(GPRstr[rs1]) :: iR;
+                  iR = RFull(GPRstr(rs1)) :: iR;
                };
                if isWrite then {
                   oR = RFull(csr_name(csr)) :: oR;
                };
-               oR = RFull(GPRstr[rd]) :: oR;
+               oR = RFull(GPRstr(rd)) :: oR;
       },
       LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
              aR = iR;
              ik =
                match (aq, rl) {
@@ -86,9 +87,9 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                }
       },
       STORE(imm, rs2, rs1, width, aq, rl) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
              ik =
                match (aq, rl) {
                  (false, false) => IK_mem_write (Write_plain),
@@ -99,17 +100,17 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                }
       },
       ADDIW(imm, rs, rd) => {
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       SHIFTW(imm, rs, rd, op) => {
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       RTYPEW(rs2, rs1, rd, op) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       FENCE(pred, succ) => {
              ik =
@@ -141,8 +142,8 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
               ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
      },
      LOADRES(aq, rl, rs1, width, rd) => {
-            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
             aR = iR;
             ik = match (aq, rl) {
               (false, false) => IK_mem_read (Read_RISCV_reserved),
@@ -152,10 +153,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
             };
      },
      STORECON(aq, rl, rs2, rs1, width, rd) => {
-            if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-            if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+            if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
              ik = match (aq, rl) {
                (false, false) => IK_mem_write (Write_RISCV_conditional),
                (false, true)  => IK_mem_write (Write_RISCV_conditional_release),
@@ -165,10 +166,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
              };
       },
       AMO(op, aq, rl, rs2, rs1, width, rd) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
              ik = match (aq, rl) {
                (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional),
                (false, true)  => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release),
@@ -196,40 +197,40 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
   match instr {
      EBREAK() => (),
      UTYPE(imm, rd, op) => {
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+	    if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
      },
      RISCV_JAL(imm, rd) => {
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+	    if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
             let offset : bits(64) = EXTS(imm) in
             Nias = [| NIAFP_concrete_address (PC + offset) |];
             ik = IK_branch();
      },
      RISCV_JALR(imm, rs, rd) => {
-            if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
             let offset : bits(64) = EXTS(imm) in
             Nias = [| NIAFP_indirect_address() |];
             ik = IK_branch();
      },
      BTYPE(imm, rs2, rs1, op) => {
-            if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
             ik = IK_branch();
             let offset : bits(64) = EXTS(imm) in
             Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
       },
       ITYPE(imm, rs, rd, op) => {
-            if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       SHIFTIOP(imm, rs, rd, op) => {
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       RTYPE(rs2, rs1, rd, op) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       CSR(csr, rs1, rd, is_imm, op) => {
                let isWrite : bool = match op {
@@ -238,16 +239,16 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                };
                iR = RFull(csr_name(csr)) :: iR;
                if ~(is_imm) then {
-                  iR = RFull(GPRstr[rs1]) :: iR;
+                  iR = RFull(GPRstr(rs1)) :: iR;
                };
                if isWrite then {
                   oR = RFull(csr_name(csr)) :: oR;
                };
-               oR = RFull(GPRstr[rd]) :: oR;
+               oR = RFull(GPRstr(rd)) :: oR;
       },
       LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
              aR = iR;
              ik =
                match (aq, rl) {
@@ -259,9 +260,9 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                }
       },
       STORE(imm, rs2, rs1, width, aq, rl) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
              ik =
                match (aq, rl) {
                  (false, false) => IK_mem_write (Write_plain),
@@ -272,17 +273,17 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                }
       },
       ADDIW(imm, rs, rd) => {
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       SHIFTW(imm, rs, rd, op) => {
-             if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       RTYPEW(rs2, rs1, rd, op) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
       },
       FENCE(pred, succ) => {
              ik =
@@ -313,8 +314,8 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
               ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
      },
      LOADRES(aq, rl, rs1, width, rd) => {
-            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
             aR = iR;
             ik = match (aq, rl) {
               (false, false) => IK_mem_read (Read_RISCV_reserved),
@@ -324,10 +325,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
             };
      },
      STORECON(aq, rl, rs2, rs1, width, rd) => {
-            if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-            if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-            if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
-            if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+            if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
+            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
              ik = match (aq, rl) {
                (false, false) => IK_mem_write (Write_RISCV_conditional),
                (false, true)  => IK_mem_write (Write_RISCV_conditional_release),
@@ -337,10 +338,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
              };
       },
       AMO(op, aq, rl, rs2, rs1, width, rd) => {
-             if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
-             if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
-             if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
-             if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
+             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
+             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
+             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
              ik = match (aq, rl) {
                (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional),
                (false, true)  => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release),
diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail
index f611f52..395a332 100644
--- a/model/riscv_duopod.sail
+++ b/model/riscv_duopod.sail
@@ -1,14 +1,10 @@
 // This file depends on the xlen definitions in riscv_xlen.sail.
 
-type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 type regbits = bits(5)
 
 val zeros : forall 'n, 'n >= 0. atom('n) -> bits('n)
 function zeros n = replicate_bits(0b0, n)
 
-val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
-function regbits_to_regno b = let r as atom(_) = unsigned(b) in r
-
 /* Architectural state */
 
 register PC : xlenbits
@@ -17,24 +13,28 @@ register nextPC : xlenbits
 register Xs : vector(32, dec, xlenbits)
 
 /* Getters and setters for X registers (special case for zeros register, x0) */
-val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+val rX : regbits -> xlenbits effect {rreg}
 
-function rX 0 = EXTZ(0x0)
-and rX (r if r > 0) = Xs[r]
+function rX(r) =
+  match r {
+    0b00000 => EXTZ(0x0),
+    _ => Xs[unsigned(r)]
+  }
 
-val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+val wX : (regbits, xlenbits) -> unit effect {wreg}
 
 function wX (r, v) =
-  if r != 0 then {
-     Xs[r] = v;
+  if r != 0b00000 then {
+     Xs[unsigned(r)] = v;
   }
 
 overload X = {rX, wX}
 
 /* Accessors for memory */
 val MEMr = { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
-val read_mem : forall 'n, 'n >= 0. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+   (atom('m), int('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val read_mem : forall 'n, 'n >= 0. (xlenbits, int('n)) -> bits(8 * 'n) effect {rmem}
 function read_mem(addr, width) =
     MEMr(sizeof(xlen), width, EXTZ(0x0), addr)
 
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index ae8748c..c52a70d 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -12,7 +12,7 @@ function fetch() -> FetchResult =
   match ext_fetch_check_pc(PC, PC) {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
-      if   (use_pc[0] != 0b0 | (use_pc[1] != 0b0 & (~ (haveRVC()))))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & (~ (haveRVC()))))
       then F_Error(E_Fetch_Addr_Align, PC)
       else match translateAddr(use_pc, Execute) {
         TR_Failure(e)     => F_Error(e, PC),
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index cd2f069..d2cbd38 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -53,7 +53,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
             */
            match width {
              BYTE   => true,
-             HALF   => vaddr[0]    == 0b0,
+	     HALF   => vaddr[0..0] == 0b0,
              WORD   => vaddr[1..0] == 0b00,
              DOUBLE => vaddr[2..0] == 0b000
            };
@@ -112,7 +112,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
              */
             match width {
               BYTE   => true,
-              HALF   => vaddr[0]    == 0b0,
+	      HALF   => vaddr[0..0] == 0b0,
               WORD   => vaddr[1..0] == 0b00,
               DOUBLE => vaddr[2..0] == 0b000
             };
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index a435786..a0858bf 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -59,7 +59,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
     },
     Ext_ControlAddr_OK(target) => {
       /* Perform standard alignment check */
-      if   target[1] & (~ (haveRVC()))
+      if bit_to_bool(target[1]) & (~ (haveRVC()))
       then {
         handle_mem_exception(target, E_Fetch_Addr_Align);
         RETIRE_FAIL
@@ -123,7 +123,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
         RETIRE_FAIL
       },
       Ext_ControlAddr_OK(target) => {
-        if target[1] & (~ (haveRVC())) then {
+	if bit_to_bool(target[1]) & (~ (haveRVC())) then {
           handle_mem_exception(target, E_Fetch_Addr_Align);
           RETIRE_FAIL;
         } else {
@@ -167,8 +167,8 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = {
   let immext : xlenbits = EXTS(imm);
   let result : xlenbits = match op {
     RISCV_ADDI  => rs1_val + immext,
-    RISCV_SLTI  => EXTZ(rs1_val <_s immext),
-    RISCV_SLTIU => EXTZ(rs1_val <_u immext),
+    RISCV_SLTI  => EXTZ(bool_to_bits(rs1_val <_s immext)),
+    RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)),
     RISCV_ANDI  => rs1_val & immext,
     RISCV_ORI   => rs1_val | immext,
     RISCV_XORI  => rs1_val ^ immext
@@ -198,9 +198,9 @@ mapping encdec_sop : sop <-> bits(3) = {
   RISCV_SRAI <-> 0b101
 }
 
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero
 
 function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = {
   let rs1_val = X(rs1);
@@ -248,8 +248,8 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = {
   let rs2_val = X(rs2);
   let result : xlenbits = match op {
     RISCV_ADD  => rs1_val + rs2_val,
-    RISCV_SLT  => EXTZ(rs1_val <_s rs2_val),
-    RISCV_SLTU => EXTZ(rs1_val <_u rs2_val),
+    RISCV_SLT  => EXTZ(bool_to_bits(rs1_val <_s rs2_val)),
+    RISCV_SLTU => EXTZ(bool_to_bits(rs1_val <_u rs2_val)),
     RISCV_AND  => rs1_val & rs2_val,
     RISCV_OR   => rs1_val | rs2_val,
     RISCV_XOR  => rs1_val ^ rs2_val,
@@ -309,9 +309,9 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
   if   plat_enable_misaligned_access() then false
   else match width {
          BYTE   => false,
-         HALF   => vaddr[0] == true,
-         WORD   => vaddr[0] == true | vaddr[1] == true,
-         DOUBLE => vaddr[0] == true | vaddr[1] == true | vaddr[2] == true
+	 HALF   => vaddr[0] == bitone,
+	 WORD   => vaddr[0] == bitone | vaddr[1] == bitone,
+	 DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone
        }
 
 function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
@@ -731,7 +731,7 @@ mapping clause encdec = SRET()
 function clause execute SRET() = {
   match cur_privilege {
     User       => handle_illegal(),
-    Supervisor => if   (~ (haveSupMode ())) | mstatus.TSR() == true
+    Supervisor => if   (~ (haveSupMode ())) | mstatus.TSR() == 0b1
                   then handle_illegal()
                   else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)),
     Machine    => if   (~ (haveSupMode ()))
@@ -765,7 +765,7 @@ mapping clause encdec = WFI()
 function clause execute WFI() =
   match cur_privilege {
     Machine    => { platform_wfi(); RETIRE_SUCCESS },
-    Supervisor => if   mstatus.TW() == true
+    Supervisor => if   mstatus.TW() == 0b1
                   then { handle_illegal(); RETIRE_FAIL }
                   else { platform_wfi(); RETIRE_SUCCESS },
     User       => { handle_illegal(); RETIRE_FAIL }
@@ -780,13 +780,13 @@ mapping clause encdec = SFENCE_VMA(rs1, rs2)
   <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute SFENCE_VMA(rs1, rs2) = {
-  let addr : option(xlenbits) = if rs1 == 0 then None() else Some(X(rs1));
-  let asid : option(xlenbits) = if rs2 == 0 then None() else Some(X(rs2));
+  let addr : option(xlenbits) = if rs1 == 0b00000 then None() else Some(X(rs1));
+  let asid : option(xlenbits) = if rs2 == 0b00000 then None() else Some(X(rs2));
   match cur_privilege {
     User       => { handle_illegal(); RETIRE_FAIL },
     Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) {
-                    (Some(_), true)  => { handle_illegal(); RETIRE_FAIL },
-                    (Some(_), false) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
+		    (Some(_), 0b1)  => { handle_illegal(); RETIRE_FAIL },
+		    (Some(_), 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
                     (_, _)           => internal_error("unimplemented sfence architecture")
                   },
     Machine    => { flush_TLB(asid, addr); RETIRE_SUCCESS }
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index c58c636..4f3d0c6 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -400,9 +400,9 @@ mapping clause assembly = C_BNEZ(imm, rs)
 union clause ast = C_SLLI : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd)
-      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == false)
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
   <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10
-      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == false)
+      if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
 
 function clause execute (C_SLLI(shamt, rsd)) =
   execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI))
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index 5b37c78..884820f 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -15,9 +15,8 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
       RETIRE_FAIL
     },
     Ext_ControlAddr_OK(addr) => {
-      let  target = [addr with 0 = bitzero];  /* clear addr[0] */
-      if   target[1] & (~ (haveRVC()))
-      then {
+      let target = [addr with 0 = bitzero];  /* clear addr[0] */
+      if bit_to_bool(target[1]) & ~(haveRVC()) then {
         handle_mem_exception(target, E_Fetch_Addr_Align);
         RETIRE_FAIL
       } else {
diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail
index 5a3fb58..b9c9c59 100644
--- a/model/riscv_next_regs.sail
+++ b/model/riscv_next_regs.sail
@@ -55,7 +55,7 @@ function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
 /* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */
 function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
   let s : Sinterrupts = o;
-  let s = if d.USI() == true then update_USI(s, u.USI()) else s;
+  let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s;
   s
 }
 
@@ -66,9 +66,9 @@ function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterr
 /* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */
 function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
   let s : Sinterrupts = o;
-  let s = if d.UEI() == true then update_UEI(s, u.UEI()) else s;
-  let s = if d.UTI() == true then update_UTI(s, u.UTI()) else s;
-  let s = if d.USI() == true then update_USI(s, u.USI()) else s;
+  let s = if d.UEI() == 0b1 then update_UEI(s, u.UEI()) else s;
+  let s = if d.UTI() == 0b1 then update_UTI(s, u.UTI()) else s;
+  let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s;
   s
 }
 
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 52511a9..9639592 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -201,11 +201,11 @@ function clint_load(addr, width) = {
 function clint_dispatch() -> unit = {
   if   get_config_print_platform()
   then print_platform("clint::tick mtime <- " ^ BitStr(mtime));
-  mip->MTI() = false;
+  mip->MTI() = 0b0;
   if mtimecmp <=_u mtime then {
     if   get_config_print_platform()
     then print_platform(" clint timer pending at mtime " ^ BitStr(mtime));
-    mip->MTI() = true
+    mip->MTI() = 0b1
   }
 }
 
@@ -216,7 +216,7 @@ function clint_store(addr, width, data) = {
   if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
     if   get_config_print_platform()
     then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
-    mip->MSI() = data[0] == 0b1;
+    mip->MSI() = [data[0]];
     clint_dispatch();
     MemValue(true)
   } else if addr == MTIMECMP_BASE & 'n == 8 then {
@@ -308,7 +308,7 @@ function htif_store(addr, width, data) = {
     0x00 => { /* syscall-proxy */
       if   get_config_print_platform()
       then print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload()));
-      if   cmd.payload()[0] == 0b1
+      if   cmd.payload()[0] == bitone
       then {
            htif_done = true;
            htif_exit_code = (sail_zero_extend(cmd.payload(), 64) >> 1)
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 4c65f7d..233602f 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -29,10 +29,10 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
 val pmpCheckRWX: (Pmpcfg_ent, AccessType) -> bool
 function pmpCheckRWX(ent, acc) = {
   match acc {
-    Read      => ent.R() == true,
-    Write     => ent.W() == true,
-    ReadWrite => ent.R() == true & ent.W() == true,
-    Execute   => ent.X() == true
+    Read      => ent.R() == 0b1,
+    Write     => ent.W() == 0b1,
+    ReadWrite => ent.R() == 0b1 & ent.W() == 0b1,
+    Execute   => ent.X() == 0b1
   }
 }
 
@@ -40,7 +40,7 @@ function pmpCheckRWX(ent, acc) = {
 val pmpCheckPerms: (Pmpcfg_ent, AccessType, Privilege) -> bool
 function pmpCheckPerms(ent, acc, priv) = {
   match priv {
-    Machine => if   ent.L() == true
+    Machine => if   ent.L() == 0b1
                then pmpCheckRWX(ent, acc)
                else true,
     _       => pmpCheckRWX(ent, acc)
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index fcc6901..978ef18 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -2,7 +2,7 @@
 
 enum PmpAddrMatchType = {OFF, TOR, NA4, NAPOT}
 
-val cast pmpAddrMatchType_of_bits : bits(2) -> PmpAddrMatchType
+val pmpAddrMatchType_of_bits : bits(2) -> PmpAddrMatchType
 function pmpAddrMatchType_of_bits(bs) = {
   match bs {
     0b00 => OFF,
@@ -12,7 +12,7 @@ function pmpAddrMatchType_of_bits(bs) = {
   }
 }
 
-val cast pmpAddrMatchType_to_bits : PmpAddrMatchType -> bits(2)
+val pmpAddrMatchType_to_bits : PmpAddrMatchType -> bits(2)
 function pmpAddrMatchType_to_bits(bs) = {
   match bs {
     OFF   => 0b00,
@@ -87,7 +87,7 @@ function pmpReadCfgReg(n) = {
 
 /* Helper to handle locked entries */
 function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
-  if cfg.L() == true then cfg else Mk_Pmpcfg_ent(v)
+  if cfg.L() == 0b1 then cfg else Mk_Pmpcfg_ent(v)
 
 val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
 function pmpWriteCfgReg(n, v) = {
@@ -139,5 +139,5 @@ function pmpWriteCfgReg(n, v) = {
 
 function pmpWriteAddr(cfg: Pmpcfg_ent, reg: xlenbits, v: xlenbits) -> xlenbits =
   if   sizeof(xlen) == 32
-  then { if cfg.L() == true then reg else v }
-  else { if cfg.L() == true then reg else EXTZ(v[53..0]) }
+  then { if cfg.L() == 0b1 then reg else v }
+  else { if cfg.L() == 0b1 then reg else EXTZ(v[53..0]) }
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index c852677..4b4a1ea 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -139,7 +139,13 @@ function wX (r, in_v) = {
   }
 }
 
-overload X = {rX, wX}
+function rX_bits(i: bits(5)) -> xlenbits = rX(unsigned(i))
+
+function wX_bits(i: bits(5), data: xlenbits) -> unit = {
+  wX(unsigned(i)) = data
+}
+
+overload X = {rX_bits, wX_bits, rX, wX}
 
 /* register names */
 
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 4e81fe9..ed27c84 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -10,7 +10,7 @@ function step(step_no : int) -> bool = {
     match dispatchInterrupt(cur_privilege) {
       Some(intr, priv) => {
         if   get_config_print_instr()
-        then print_bits("Handling interrupt: ", intr);
+	then print_bits("Handling interrupt: ", interruptType_to_bits(intr));
         handle_interrupt(intr, priv);
         (RETIRE_FAIL, false)
       },
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index a8029a4..14e5d99 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -97,17 +97,17 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) =
   & (privLevel_to_bits(p) >=_u csrpr)      /* privilege */
 
 function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
-  ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == true)
+  ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1)
 
 function check_Counteren(csr : csreg, p : Privilege) -> bool =
   match(csr, p) {
-    (0xC00, Supervisor) => mcounteren.CY() == true,
-    (0xC01, Supervisor) => mcounteren.TM() == true,
-    (0xC02, Supervisor) => mcounteren.IR() == true,
+    (0xC00, Supervisor) => mcounteren.CY() == 0b1,
+    (0xC01, Supervisor) => mcounteren.TM() == 0b1,
+    (0xC02, Supervisor) => mcounteren.IR() == 0b1,
 
-    (0xC00, User) => mcounteren.CY() == true & ((~ (haveSupMode())) | scounteren.CY() == true),
-    (0xC01, User) => mcounteren.TM() == true & ((~ (haveSupMode())) | scounteren.TM() == true),
-    (0xC02, User) => mcounteren.IR() == true & ((~ (haveSupMode())) | scounteren.IR() == true),
+    (0xC00, User) => mcounteren.CY() == 0b1 & ((~ (haveSupMode())) | scounteren.CY() == 0b1),
+    (0xC01, User) => mcounteren.TM() == 0b1 & ((~ (haveSupMode())) | scounteren.TM() == 0b1),
+    (0xC02, User) => mcounteren.IR() == 0b1 & ((~ (haveSupMode())) | scounteren.IR() == 0b1),
 
     (_, _) => /* no HPM counters for now */
               if   0xC03 <=_u csr & csr <=_u 0xC1F
@@ -144,10 +144,10 @@ val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Pl
  */
 function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
   let idx   = num_of_ExceptionType(e);
-  let super = medeleg.bits()[idx];
+  let super = bit_to_bool(medeleg.bits()[idx]);
   /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */
   let user  = if   haveSupMode()
-              then super & haveNExt() & sedeleg.bits()[idx]
+	      then super & haveNExt() & bit_to_bool(sedeleg.bits()[idx])
               else super & haveNExt();
   let deleg = if      haveUsrMode() & user  then User
               else if haveSupMode() & super then Supervisor
@@ -162,16 +162,16 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
  */
 function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
   let ip = Mk_Minterrupts(ip);
-  if      ip.MEI() == true then Some(I_M_External)
-  else if ip.MSI() == true then Some(I_M_Software)
-  else if ip.MTI() == true then Some(I_M_Timer)
-  else if ip.SEI() == true then Some(I_S_External)
-  else if ip.SSI() == true then Some(I_S_Software)
-  else if ip.STI() == true then Some(I_S_Timer)
-  else if ip.UEI() == true then Some(I_U_External)
-  else if ip.USI() == true then Some(I_U_Software)
-  else if ip.UTI() == true then Some(I_U_Timer)
-  else                          None()
+  if      ip.MEI() == 0b1 then Some(I_M_External)
+  else if ip.MSI() == 0b1 then Some(I_M_Software)
+  else if ip.MTI() == 0b1 then Some(I_M_Timer)
+  else if ip.SEI() == 0b1 then Some(I_S_External)
+  else if ip.SSI() == 0b1 then Some(I_S_Software)
+  else if ip.STI() == 0b1 then Some(I_S_Timer)
+  else if ip.UEI() == 0b1 then Some(I_U_External)
+  else if ip.USI() == 0b1 then Some(I_U_Software)
+  else if ip.UTI() == 0b1 then Some(I_U_Timer)
+  else                         None()
 }
 
 /* Process the pending interrupts xip at a privilege according to
@@ -214,9 +214,9 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
      * while lower privileges are blocked.  An unsupported privilege is
      * considered blocked.
      */
-    let mIE = priv != Machine | (priv == Machine & mstatus.MIE() == true);
-    let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus.SIE() == true));
-    let uIE = haveNExt() & (priv == User & mstatus.UIE() == true);
+    let mIE = priv != Machine | (priv == Machine & mstatus.MIE() == 0b1);
+    let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus.SIE() == 0b1));
+    let uIE = haveNExt() & (priv == User & mstatus.UIE() == 0b1);
     match processPending(mip, mie, mideleg.bits(), mIE) {
       Ints_Empty()      => None(),
       Ints_Pending(p)   => let r = (p, Machine) in Some(r),
@@ -304,11 +304,11 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
   match (del_priv) {
     Machine => {
-       mcause->IsInterrupt() = intr;
+       mcause->IsInterrupt() = bool_to_bits(intr);
        mcause->Cause()       = EXTZ(c);
 
        mstatus->MPIE() = mstatus.MIE();
-       mstatus->MIE()  = false;
+       mstatus->MIE()  = 0b0;
        mstatus->MPP()  = privLevel_to_bits(cur_privilege);
        mtval           = tval(info);
        mepc            = pc;
@@ -325,14 +325,14 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
     Supervisor => {
        assert (haveSupMode(), "no supervisor mode present for delegation");
 
-       scause->IsInterrupt() = intr;
+       scause->IsInterrupt() = bool_to_bits(intr);
        scause->Cause()       = EXTZ(c);
 
        mstatus->SPIE() = mstatus.SIE();
-       mstatus->SIE()  = false;
-       mstatus->SPP()  = match (cur_privilege) {
-                           User => false,
-                           Supervisor => true,
+       mstatus->SIE()  = 0b0;
+       mstatus->SPP()  = match cur_privilege {
+			   User => 0b0,
+			   Supervisor => 0b1,
                            Machine => internal_error("invalid privilege for s-mode trap")
                          };
        stval           = tval(info);
@@ -350,11 +350,11 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
     User => {
        assert(haveUsrMode(), "no user mode present for delegation");
 
-       ucause->IsInterrupt() = intr;
+       ucause->IsInterrupt() = bool_to_bits(intr);
        ucause->Cause()       = EXTZ(c);
 
        mstatus->UPIE() = mstatus.UIE();
-       mstatus->UIE()  = false;
+       mstatus->UIE()  = 0b0;
        utval           = tval(info);
        uepc            = pc;
 
@@ -378,12 +378,12 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       if   get_config_print_platform()
       then print_platform("trapping from " ^ to_str(cur_priv) ^ " to " ^ to_str(del_priv)
                           ^ " to handle " ^ to_str(e.trap));
-      trap_handler(del_priv, false, e.trap, pc, e.excinfo, e.ext)
+      trap_handler(del_priv, false, exceptionType_to_bits(e.trap), pc, e.excinfo, e.ext)
     },
     (_, CTL_MRET())  => {
       let prev_priv   = cur_privilege;
       mstatus->MIE()  = mstatus.MPIE();
-      mstatus->MPIE() = true;
+      mstatus->MPIE() = 0b1;
       cur_privilege   = privLevel_of_bits(mstatus.MPP());
       mstatus->MPP()  = privLevel_to_bits(if haveUsrMode() then User else Machine);
 
@@ -398,10 +398,10 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
     (_, CTL_SRET())  => {
       let prev_priv   = cur_privilege;
       mstatus->SIE()  = mstatus.SPIE();
-      mstatus->SPIE() = true;
-      cur_privilege   = if mstatus.SPP() == true then Supervisor else User;
+      mstatus->SPIE() = 0b1;
+      cur_privilege   = if mstatus.SPP() == 0b1 then Supervisor else User;
       /* S-mode implies that U-mode is supported (issue 331 on riscv-isa-manual). */
-      mstatus->SPP()  = false;
+      mstatus->SPP()  = 0b0;
 
       if   get_config_print_reg()
       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
@@ -415,7 +415,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
     (_, CTL_URET())  => {
       let prev_priv   = cur_privilege;
       mstatus->UIE()  = mstatus.UPIE();
-      mstatus->UPIE() = true;
+      mstatus->UPIE() = 0b1;
       cur_privilege   = User;
 
       if   get_config_print_reg()
@@ -437,7 +437,7 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
 }
 
 function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
-  set_next_pc(trap_handler(del_priv, true, i, PC, None(), None()))
+  set_next_pc(trap_handler(del_priv, true, interruptType_to_bits(i), PC, None(), None()))
 
 /* state state initialization */
 
@@ -447,16 +447,16 @@ function init_sys() -> unit = {
   mhartid     = EXTZ(0b0);
 
   misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64);
-  misa->A()   = true;               /* atomics */
-  misa->C()   = sys_enable_rvc ();  /* RVC */
-  misa->I()   = true;               /* base integer ISA */
-  misa->M()   = true;               /* integer multiply/divide */
-  misa->U()   = true;               /* user-mode */
-  misa->S()   = true;               /* supervisor-mode */
+  misa->A()   = 0b1;                            /* atomics */
+  misa->C()   = bool_to_bits(sys_enable_rvc()); /* RVC */
+  misa->I()   = 0b1;                            /* base integer ISA */
+  misa->M()   = 0b1;                            /* integer multiply/divide */
+  misa->U()   = 0b1;                            /* user-mode */
+  misa->S()   = 0b1;                            /* supervisor-mode */
 
   mstatus = set_mstatus_SXL(mstatus, misa.MXL());
   mstatus = set_mstatus_UXL(mstatus, misa.MXL());
-  mstatus->SD()   = false;
+  mstatus->SD()   = 0b0;
 
   mip->bits()     = EXTZ(0b0);
   mie->bits()     = EXTZ(0b0);
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 27e0c00..25da335 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -81,7 +81,7 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
   then { /* Allow modifications to C only for now. */
          let  v = Mk_Misa(v);
          /* Suppress changing C if nextPC would become misaligned. */
-         if   v.C() == false & nextPC[1] == true
+	 if   v.C() == 0b0 & nextPC[1] == bitone
          then m
          else update_C(m, v.C())
        }
@@ -90,12 +90,12 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
 
 /* helpers to check support for various extensions. */
 /* we currently don't model 'E', so always assume 'I'. */
-function haveAtomics() -> bool = misa.A() == true
-function haveRVC()     -> bool = misa.C() == true
-function haveMulDiv()  -> bool = misa.M() == true
-function haveSupMode() -> bool = misa.S() == true
-function haveUsrMode() -> bool = misa.U() == true
-function haveNExt()    -> bool = misa.N() == true
+function haveAtomics() -> bool = misa.A() == 0b1
+function haveRVC()     -> bool = misa.C() == 0b1
+function haveMulDiv()  -> bool = misa.M() == 0b1
+function haveSupMode() -> bool = misa.S() == 0b1
+function haveUsrMode() -> bool = misa.U() == 0b1
+function haveNExt()    -> bool = misa.N() == 0b1
 
 bitfield Mstatus : xlenbits = {
   SD   : xlen - 1,
@@ -129,7 +129,7 @@ bitfield Mstatus : xlenbits = {
 register mstatus : Mstatus
 
 function effectivePrivilege(m : Mstatus, priv : Privilege) -> Privilege =
-  if   m.MPRV() == true
+  if   m.MPRV() == 0b1
   then privLevel_of_bits(mstatus.MPP())
   else cur_privilege
 
@@ -174,16 +174,16 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
    */
   // let m = update_FS(m, extStatus_to_bits(Off));
 
-  let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
-                     | extStatus_of_bits(m.XS()) == Dirty);
+  let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
+  let m = update_SD(m, bool_to_bits(dirty));
 
   /* We don't support dynamic changes to SXL and UXL. */
   let m = set_mstatus_SXL(m, get_mstatus_SXL(o));
   let m = set_mstatus_UXL(m, get_mstatus_UXL(o));
 
   /* Hardwired to zero in the absence of 'N'. */
-  let m = update_UPIE(m, false);
-  let m = update_UIE(m, false);
+  let m = update_UPIE(m, 0b0);
+  let m = update_UIE(m, 0b0);
   m
 }
 
@@ -261,9 +261,9 @@ function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = {
   /* M-mode interrupt delegation bits "should" be hardwired to 0. */
   /* FIXME: needs verification against eventual spec language. */
   let m = Mk_Minterrupts(v);
-  let m = update_MEI(m, false);
-  let m = update_MTI(m, false);
-  let m = update_MSI(m, false);
+  let m = update_MEI(m, 0b0);
+  let m = update_MTI(m, 0b0);
+  let m = update_MSI(m, 0b0);
   m
 }
 
@@ -290,7 +290,7 @@ register medeleg : Medeleg  /* Delegation to S-mode */
 function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = {
   let m = Mk_Medeleg(v);
   /* M-EnvCalls delegation is not supported */
-  let m = update_MEnvCall(m, false);
+  let m = update_MEnvCall(m, 0b0);
   m
 }
 
@@ -322,7 +322,7 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
   let base : xlenbits = m.Base() @ 0b00;
   match (trapVectorMode_of_bits(m.Mode())) {
     TV_Direct => Some(base),
-    TV_Vector => if   c.IsInterrupt() == true
+    TV_Vector => if   c.IsInterrupt() == 0b1
                  then Some(base + (EXTZ(c.Cause()) << 2))
                  else Some(base),
     TV_Reserved => None()
@@ -337,13 +337,13 @@ register mepc : xlenbits
  * When misa.C is writable, it zeroes only xepc[0].
  */
 function legalize_xepc(v : xlenbits) -> xlenbits =
-  if   sys_enable_writable_misa () | misa.C() == true
+  if   sys_enable_writable_misa () | misa.C() == 0b1
   then [v with 0 = bitzero]
   else v & EXTS(0b100)
 
 /* masking for reads to xepc */
 function pc_alignment_mask() -> xlenbits =
-  ~(EXTZ(if misa.C() == true then 0b00 else 0b10))
+  ~(EXTZ(if misa.C() == 0b1 then 0b00 else 0b10))
 
 /* auxiliary exception registers */
 
@@ -364,17 +364,17 @@ register scounteren : Counteren
 
 function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
   /* no HPM counters yet */
-  let c = update_IR(c, v[2]);
-  let c = update_TM(c, v[1]);
-  let c = update_CY(c, v[0]);
+  let c = update_IR(c, [v[2]]);
+  let c = update_TM(c, [v[1]]);
+  let c = update_CY(c, [v[0]]);
   c
 }
 
 function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
   /* no HPM counters yet */
-  let c = update_IR(c, v[2]);
-  let c = update_TM(c, v[1]);
-  let c = update_CY(c, v[0]);
+  let c = update_IR(c, [v[2]]);
+  let c = update_TM(c, [v[1]]);
+  let c = update_CY(c, [v[0]]);
   c
 }
 
@@ -462,8 +462,8 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
   let m = update_XS(m, s.XS());
   // See comment for mstatus.FS.
   let m = update_FS(m, s.FS());
-  let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
-                     | extStatus_of_bits(m.XS()) == Dirty);
+  let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
+  let m = update_SD(m, bool_to_bits(dirty));
 
   let m = update_SPP(m, s.SPP());
   let m = update_SPIE(m, s.SPIE());
@@ -535,8 +535,8 @@ function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru
   let m : Minterrupts = o;
   let m = update_SSI(m, s.SSI() & d.SSI());
   if haveNExt() then {
-    let m = if d.UEI() == true then update_UEI(m, s.UEI()) else m;
-    let m = if d.USI() == true then update_USI(m, s.USI()) else m;
+    let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m;
+    let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m;
     m
   } else m
 }
@@ -548,13 +548,13 @@ function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr
 /* Returns the new value of mie from the previous mie (o) and the written sie (s) as delegated by mideleg (d). */
 function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
   let m : Minterrupts = o;
-  let m = if d.SEI() == true then update_SEI(m, s.SEI()) else m;
-  let m = if d.STI() == true then update_STI(m, s.STI()) else m;
-  let m = if d.SSI() == true then update_SSI(m, s.SSI()) else m;
+  let m = if d.SEI() == 0b1 then update_SEI(m, s.SEI()) else m;
+  let m = if d.STI() == 0b1 then update_STI(m, s.STI()) else m;
+  let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m;
   if haveNExt() then {
-    let m = if d.UEI() == true then update_UEI(m, s.UEI()) else m;
-    let m = if d.UTI() == true then update_UTI(m, s.UTI()) else m;
-    let m = if d.USI() == true then update_USI(m, s.USI()) else m;
+    let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m;
+    let m = if d.UTI() == 0b1 then update_UTI(m, s.UTI()) else m;
+    let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m;
     m
   } else m
 }
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index a47afc3..d8d6de0 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -22,7 +22,7 @@ type csreg   = bits(12)   /* CSR addressing */
 
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 
-val cast regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
 function regidx_to_regno b = let 'r = unsigned(b) in r
 
 /* mapping RVC register indices into normal indices */
@@ -65,7 +65,7 @@ function arch_to_bits(a : Architecture) -> arch_xlen =
 type priv_level = bits(2)
 enum Privilege  = {User, Supervisor, Machine}
 
-val cast privLevel_to_bits : Privilege -> priv_level
+val privLevel_to_bits : Privilege -> priv_level
 function privLevel_to_bits (p) =
   match (p) {
     User       => 0b00,
@@ -73,7 +73,7 @@ function privLevel_to_bits (p) =
     Machine    => 0b11
   }
 
-val cast privLevel_of_bits : priv_level -> Privilege
+val privLevel_of_bits : priv_level -> Privilege
 function privLevel_of_bits (p) =
   match (p) {
     0b00 => User,
@@ -128,7 +128,7 @@ enum InterruptType = {
   I_M_External
 }
 
-val cast interruptType_to_bits : InterruptType -> exc_code
+val interruptType_to_bits : InterruptType -> exc_code
 function interruptType_to_bits (i) =
   match (i) {
     I_U_Software => 0x00,
@@ -166,7 +166,7 @@ enum ExceptionType = {
  E_CHERI
 }
 
-val cast exceptionType_to_bits : ExceptionType -> exc_code
+val exceptionType_to_bits : ExceptionType -> exc_code
 function exceptionType_to_bits(e) =
   match (e) {
     E_Fetch_Addr_Align   => 0x00,
@@ -237,7 +237,7 @@ function internal_error(s) = {
 type tv_mode = bits(2)
 enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved}
 
-val cast trapVectorMode_of_bits : tv_mode -> TrapVectorMode
+val trapVectorMode_of_bits : tv_mode -> TrapVectorMode
 function trapVectorMode_of_bits (m) =
   match (m) {
     0b00 => TV_Direct,
@@ -250,7 +250,7 @@ function trapVectorMode_of_bits (m) =
 type ext_status = bits(2)
 enum ExtStatus = {Off, Initial, Clean, Dirty}
 
-val cast extStatus_to_bits : ExtStatus -> ext_status
+val extStatus_to_bits : ExtStatus -> ext_status
 function extStatus_to_bits(e) =
   match (e) {
     Off     => 0b00,
@@ -259,7 +259,7 @@ function extStatus_to_bits(e) =
     Dirty   => 0b11
   }
 
-val cast extStatus_of_bits : ext_status -> ExtStatus
+val extStatus_of_bits : ext_status -> ExtStatus
 function extStatus_of_bits(e) =
   match (e) {
     0b00 => Off,
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index c8808f7..690a3c7 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -25,36 +25,36 @@ bitfield PTE_Bits : pteAttribs = {
 
 function isPTEPtr(p : pteAttribs) -> bool = {
   let a = Mk_PTE_Bits(p);
-  a.R() == false & a.W() == false & a.X() == false
+  a.R() == 0b0 & a.W() == 0b0 & a.X() == 0b0
 }
 
 function isInvalidPTE(p : pteAttribs) -> bool = {
   let a = Mk_PTE_Bits(p);
-  a.V() == false | (a.W() == true & a.R() == false)
+  a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
 }
 
 function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = {
   match (ac, priv) {
-    (Read,      User)       => p.U() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Write,     User)       => p.U() == true & p.W() == true,
-    (ReadWrite, User)       => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Execute,   User)       => p.U() == true & p.X() == true,
+    (Read,      User)       => p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+    (Write,     User)       => p.U() == 0b1 & p.W() == 0b1,
+    (ReadWrite, User)       => p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+    (Execute,   User)       => p.U() == 0b1 & p.X() == 0b1,
 
-    (Read,      Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)),
-    (Write,     Supervisor) => (p.U() == false | do_sum) & p.W() == true,
-    (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
-    (Execute,   Supervisor) => p.U() == false & p.X() == true,
+    (Read,      Supervisor) => (p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+    (Write,     Supervisor) => (p.U() == 0b0 | do_sum) & p.W() == 0b1,
+    (ReadWrite, Supervisor) => (p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+    (Execute,   Supervisor) => p.U() == 0b0 & p.X() == 0b1,
 
     (_,         Machine)    => internal_error("m-mode mem perm check")
   }
 }
 
 function update_PTE_Bits(p : PTE_Bits, a : AccessType) -> option(PTE_Bits) = {
-  let update_d = (a == Write | a == ReadWrite) & p.D() == false; // dirty-bit
-  let update_a = p.A() == false;                                 // accessed-bit
+  let update_d = (a == Write | a == ReadWrite) & p.D() == 0b0; // dirty-bit
+  let update_a = p.A() == 0b0;                                 // accessed-bit
   if update_d | update_a then {
-    let np = update_A(p, true);
-    let np = if update_d then update_D(np, true) else np;
+    let np = update_A(p, 0b1);
+    let np = if update_d then update_D(np, 0b1) else np;
     Some(np)
   } else None()
 }
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
index 5b640b1..02f8141 100644
--- a/model/riscv_vmem_rv32.sail
+++ b/model/riscv_vmem_rv32.sail
@@ -17,7 +17,7 @@ function translationMode(priv) = {
     match arch {
       Some(RV32) => {
         let s = Mk_Satp32(satp[31..0]);
-        if s.Mode() == false then Sbare else Sv32
+	if s.Mode() == 0b0 then Sbare else Sv32
       },
       _    => internal_error("unsupported address translation arch")
     }
@@ -32,8 +32,8 @@ function translateAddr(vAddr, ac) = {
     Execute => cur_privilege,
     _       => effectivePrivilege(mstatus, cur_privilege)
   };
-  let mxr    : bool   = mstatus.MXR() == true;
-  let do_sum : bool   = mstatus.SUM() == true;
+  let mxr    : bool   = mstatus.MXR() == 0b1;
+  let do_sum : bool   = mstatus.SUM() == 0b1;
   let mode : SATPMode = translationMode(effPriv);
 
   let asid = curAsid32(satp);
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index e3cca0b..3153983 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -24,7 +24,7 @@ function translationMode(priv) = {
       },
       Some(RV32) => {
         let s = Mk_Satp32(satp[31..0]);
-        if s.Mode() == false then Sbare else Sv32
+	if s.Mode() == 0b0 then Sbare else Sv32
       },
       _    => internal_error("unsupported address translation arch")
     }
@@ -39,8 +39,8 @@ function translateAddr(vAddr, ac) = {
     Execute => cur_privilege,
     _       => effectivePrivilege(mstatus, cur_privilege)
   };
-  let mxr    : bool   = mstatus.MXR() == true;
-  let do_sum : bool   = mstatus.SUM() == true;
+  let mxr    : bool   = mstatus.MXR() == 0b1;
+  let do_sum : bool   = mstatus.SUM() == 0b1;
   let mode : SATPMode = translationMode(effPriv);
 
   let asid = curAsid64(satp);
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index 49d7ec1..23404e3 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -25,7 +25,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
       let pte = Mk_SV32_PTE(v);
       let pbits = pte.BITS();
       let pattr = Mk_PTE_Bits(pbits);
-      let is_global = global | (pattr.G() == true);
+      let is_global = global | (pattr.G() == 0b1);
 /*    print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
             ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index a575a07..50a52f0 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -19,7 +19,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
       let pte = Mk_SV39_PTE(v);
       let pbits = pte.BITS();
       let pattr = Mk_PTE_Bits(pbits);
-      let is_global = global | (pattr.G() == true);
+      let is_global = global | (pattr.G() == 0b1);
 /*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(ptb)
             ^ " pt_ofs=" ^ BitStr(pt_ofs)
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index a898ac7..18abafd 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -19,7 +19,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
       let pte = Mk_SV48_PTE(v);
       let pbits = pte.BITS();
       let pattr = Mk_PTE_Bits(pbits);
-      let is_global = global | (pattr.G() == true);
+      let is_global = global | (pattr.G() == 0b1);
 /*    print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
             ^ " pt_base=" ^ BitStr(ptb)
             ^ " pt_ofs=" ^ BitStr(pt_ofs)