Remove effects

Since Sail 0.15 (released Nov 2022), effects have had no effect. They now generate a deprecation warning. This commit removes all the effect annotations from the model, thus fixing the compiler warnings.

32 files changed, 189 insertions, 189 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index e51bca2..bec76d6 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -87,7 +87,7 @@ val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", l
 
 overload operator == = {eq_string, eq_anything}
 
-val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val "reg_deref" : forall ('a : Type). register('a) -> 'a
 /* sneaky deref with no effect necessary for bitfield writes */
 val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
 
diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail
index 1b27d49..3bbf437 100644
--- a/model/prelude_mem.sail
+++ b/model/prelude_mem.sail
@@ -89,7 +89,7 @@
    capabilities and SIMD / vector instructions will also need more. */
 type max_mem_access : Int = 16
 
-val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool effect {wmv, wmvt}
+val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n), bits(8 * 'n), mem_meta) -> bool
 function write_ram(wk, addr, width, data, meta) = {
   /* Write out metadata only if the value write succeeds.
    * It is assumed for now that this write always succeeds;
@@ -103,11 +103,11 @@ function write_ram(wk, addr, width, data, meta) = {
   ret
 }
 
-val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit effect {eamem}
+val write_ram_ea : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, atom('n)) -> unit
 function write_ram_ea(wk, addr, width) =
   __write_mem_ea(wk, sizeof(xlen), addr, width)
 
-val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta) effect {rmem, rmemt}
+val read_ram = {lem: "read_ram", coq: "read_ram"} : forall 'n, 0 < 'n <= max_mem_access .  (read_kind, xlenbits, atom('n), bool) -> (bits(8 * 'n), mem_meta)
 function read_ram(rk, addr, width, read_meta) =
   let meta = if read_meta then __ReadRAM_Meta(addr, width) else default_meta in
   (__read_mem(rk, sizeof(xlen), addr, width), meta)
diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail
index e714189..919cee3 100644
--- a/model/prelude_mem_metadata.sail
+++ b/model/prelude_mem_metadata.sail
@@ -76,8 +76,8 @@ type mem_meta = unit
 
 let default_meta : mem_meta = ()
 
-val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit effect {wmvt}
+val __WriteRAM_Meta : forall 'n. (xlenbits, atom('n), mem_meta) -> unit
 function __WriteRAM_Meta(addr, width, meta) = ()
 
-val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta effect {rmem}
+val __ReadRAM_Meta  : forall 'n. (xlenbits, atom('n)) -> mem_meta
 function __ReadRAM_Meta(addr, width) = ()
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index e3f8f5b..e3c1c20 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -180,13 +180,13 @@ overload to_str = {csr_name}
 /* returns whether a CSR is defined and accessible at a given address
  * and privilege
  */
-val ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg}
+val ext_is_CSR_defined : (csreg, Privilege) -> bool
 scattered function ext_is_CSR_defined
 
 /* returns the value of the CSR if it is defined */
-val ext_read_CSR : csreg -> option(xlenbits) effect {rreg}
+val ext_read_CSR : csreg -> option(xlenbits)
 scattered function ext_read_CSR
 
 /* returns new value (after legalisation) if the CSR is defined */
-val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg, escape}
+val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits)
 scattered function ext_write_CSR
diff --git a/model/riscv_decode_ext.sail b/model/riscv_decode_ext.sail
index b6b4bb8..b215109 100644
--- a/model/riscv_decode_ext.sail
+++ b/model/riscv_decode_ext.sail
@@ -73,8 +73,8 @@
   hooks, the default implementation of which is provided below.
  */
 
-val ext_decode_compressed : bits(16) -> ast effect {rreg}
+val ext_decode_compressed : bits(16) -> ast
 function ext_decode_compressed(bv) = encdec_compressed(bv)
 
-val ext_decode : bits(32) -> ast effect {rreg}
+val ext_decode : bits(32) -> ast
 function ext_decode(bv) = encdec(bv)
diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail
index 1ff956e..8568e6a 100644
--- a/model/riscv_ext_regs.sail
+++ b/model/riscv_ext_regs.sail
@@ -72,7 +72,7 @@
  * overridden by extensions.
  */
 
-val ext_init_regs : unit -> unit effect {wreg}
+val ext_init_regs : unit -> unit
 function ext_init_regs () = ()
 
 /*!
@@ -80,7 +80,7 @@ This function is called after above when running rvfi and allows the model
 to be initialised differently (e.g. CHERI cap regs are initialised
 to omnipotent instead of null).
  */
-val ext_rvfi_init : unit -> unit effect {rreg, wreg}
+val ext_rvfi_init : unit -> unit
 function ext_rvfi_init () = {
   x1 = x1 // to avoid hook being optimized out
 }
diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
index 768aede..563d600 100644
--- a/model/riscv_fdext_control.sail
+++ b/model/riscv_fdext_control.sail
@@ -77,7 +77,7 @@
 
 /* **************************************************************** */
 
-/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg} */
+/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */
 
 function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx()
 function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx()
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index f2e0fb3..6a40606 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -106,7 +106,7 @@ function nan_unbox_H   regval =
        then regval [15..0]
        else canonical_NaN_H()
 
-val nan_box_S : bits(32) -> flenbits effect {escape}
+val nan_box_S : bits(32) -> flenbits
 function nan_box_S val_32b = {
   assert(sys_enable_fdext());
   if (sizeof(flen) == 32)
@@ -114,7 +114,7 @@ function nan_box_S val_32b = {
   else 0x_FFFF_FFFF @ val_32b
 }
 
-val nan_unbox_S : flenbits -> bits(32) effect {escape}
+val nan_unbox_S : flenbits -> bits(32)
 function nan_unbox_S regval = {
   assert(sys_enable_fdext());
   if (sizeof(flen) == 32)
@@ -174,7 +174,7 @@ function dirty_fd_context_if_present() -> unit = {
   if sys_enable_fdext() then dirty_fd_context()
 }
 
-val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits effect {rreg, escape}
+val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits
 function rF r = {
   assert(sys_enable_fdext());
   let v : fregtype =
@@ -216,7 +216,7 @@ function rF r = {
   fregval_from_freg(v)
 }
 
-val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit effect {wreg, escape}
+val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit
 function wF (r, in_v) = {
   assert(sys_enable_fdext());
   let v = fregval_into_freg(in_v);
@@ -272,42 +272,42 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {
 
 overload F = {rF_bits, wF_bits, rF, wF}
 
-val rF_H : bits(5) -> bits(16) effect {escape, rreg}
+val rF_H : bits(5) -> bits(16)
 function rF_H(i) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   nan_unbox(F(i))
 }
 
-val wF_H : (bits(5), bits(16)) -> unit effect {escape, wreg}
+val wF_H : (bits(5), bits(16)) -> unit
 function wF_H(i, data) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   F(i) = nan_box(data)
 }
 
-val rF_S : bits(5) -> bits(32) effect {escape, rreg}
+val rF_S : bits(5) -> bits(32)
 function rF_S(i) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   nan_unbox(F(i))
 }
 
-val wF_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
+val wF_S : (bits(5), bits(32)) -> unit
 function wF_S(i, data) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   F(i) = nan_box(data)
 }
 
-val rF_D : bits(5) -> bits(64) effect {escape, rreg}
+val rF_D : bits(5) -> bits(64)
 function rF_D(i) = {
   assert(sizeof(flen) >= 64);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
   F(i)
 }
 
-val wF_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
+val wF_D : (bits(5), bits(64)) -> unit
 function wF_D(i, data) = {
   assert(sizeof(flen) >= 64);
   assert(sys_enable_fdext() & not(sys_enable_zfinx()));
@@ -318,7 +318,7 @@ overload F_H = { rF_H, wF_H }
 overload F_S = { rF_S, wF_S }
 overload F_D = { rF_D, wF_D }
 
-val rF_or_X_H : bits(5) -> bits(16) effect {escape, rreg}
+val rF_or_X_H : bits(5) -> bits(16)
 function rF_or_X_H(i) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -327,7 +327,7 @@ function rF_or_X_H(i) = {
   else X(i)[15..0]
 }
 
-val rF_or_X_S : bits(5) -> bits(32) effect {escape, rreg}
+val rF_or_X_S : bits(5) -> bits(32)
 function rF_or_X_S(i) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -336,7 +336,7 @@ function rF_or_X_S(i) = {
   else X(i)[31..0]
 }
 
-val rF_or_X_D : bits(5) -> bits(64) effect {escape, rreg}
+val rF_or_X_D : bits(5) -> bits(64)
 function rF_or_X_D(i) = {
   assert(sizeof(flen) >= 64);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -350,7 +350,7 @@ function rF_or_X_D(i) = {
   }
 }
 
-val wF_or_X_H : (bits(5), bits(16)) -> unit effect {escape, wreg}
+val wF_or_X_H : (bits(5), bits(16)) -> unit
 function wF_or_X_H(i, data) = {
   assert(sizeof(flen) >= 16);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -359,7 +359,7 @@ function wF_or_X_H(i, data) = {
   else X(i) = sign_extend(data)
 }
 
-val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
+val wF_or_X_S : (bits(5), bits(32)) -> unit
 function wF_or_X_S(i, data) = {
   assert(sizeof(flen) >= 32);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -368,7 +368,7 @@ function wF_or_X_S(i, data) = {
   else X(i) = sign_extend(data)
 }
 
-val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
+val wF_or_X_D : (bits(5), bits(64)) -> unit
 function wF_or_X_D(i, data) = {
   assert (sizeof(flen) >= 64);
   assert(sys_enable_fdext() != sys_enable_zfinx());
@@ -474,7 +474,7 @@ mapping freg_or_reg_name = {
   reg if sys_enable_zfinx() <-> reg_name(reg)  if sys_enable_zfinx()
 }
 
-val init_fdext_regs : unit -> unit effect {wreg}
+val init_fdext_regs : unit -> unit
 function init_fdext_regs () = {
   f0  = zero_freg;
   f1  = zero_freg;
@@ -524,7 +524,7 @@ bitfield Fcsr : bits(32) = {
 
 register fcsr : Fcsr
 
-val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg, escape}
+val ext_write_fcsr : (bits(3), bits(5)) -> unit
 function ext_write_fcsr (frm, fflags) = {
   fcsr->FRM()    = frm;      /* Note: frm can be an illegal value, 101, 110, 111 */
   fcsr->FFLAGS() = fflags;
@@ -533,7 +533,7 @@ function ext_write_fcsr (frm, fflags) = {
 }
 
 /* called for softfloat paths (softfloat flags are consistent) */
-val write_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
+val write_fflags : (bits(5)) -> unit
 function write_fflags(fflags) = {
   if   fcsr.FFLAGS() != fflags
   then dirty_fd_context_if_present();
@@ -541,7 +541,7 @@ function write_fflags(fflags) = {
 }
 
 /* called for non-softfloat paths (softfloat flags need updating) */
-val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
+val accrue_fflags : (bits(5)) -> unit
 function accrue_fflags(flags) = {
   let f = fcsr.FFLAGS() | flags;
   if  fcsr.FFLAGS() != f
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index 7a083a7..4c54ccc 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -74,7 +74,7 @@
 
 function isRVC(h : half) -> bool = not(h[1 .. 0] == 0b11)
 
-val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+val fetch : unit -> FetchResult
 function fetch() -> FetchResult =
   /* fetch PC check for extensions: extensions return a transformed PC to fetch,
    * but any exceptions use the untransformed PC.
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index b1bfcef..6915f28 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -115,7 +115,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if amo_width_valid(size)
  * call to load_reservation in LR and cancel_reservation in SC.
  */
 
-val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg}
+val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
 function process_loadres(rd, addr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
     MemValue(result) => { load_reservation(addr); X(rd) = result; RETIRE_SUCCESS },
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index d68e7a3..b5e699e 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -368,7 +368,7 @@ function extend_value(is_unsigned, value) = match (value) {
   MemException(e) => MemException(e)
 }
 
-val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired effect {escape, rreg, wreg}
+val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> Retired
 function process_load(rd, vaddr, value, is_unsigned) =
   match extend_value(is_unsigned, value) {
     MemValue(result) => { X(rd) = result; RETIRE_SUCCESS },
diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail
index fae285c..dd7865f 100644
--- a/model/riscv_insts_begin.sail
+++ b/model/riscv_insts_begin.sail
@@ -76,16 +76,16 @@
 scattered union ast
 
 /* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> Retired effect {escape, wreg, rreg, wmv, wmvt, eamem, rmem, rmemt, barr, exmem, undef}
+val execute : ast -> Retired
 scattered function execute
 
 val assembly : ast <-> string
 scattered mapping assembly
 
-val encdec : ast <-> bits(32) effect {rreg}
+val encdec : ast <-> bits(32)
 scattered mapping encdec
 
-val encdec_compressed : ast <-> bits(16) effect {rreg}
+val encdec_compressed : ast <-> bits(16)
 scattered mapping encdec_compressed
 
 /*
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index e60b96b..67f34a7 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -108,7 +108,7 @@ mapping frm_mnemonic : rounding_mode <-> string = {
 val      valid_rounding_mode : bits(3) -> bool
 function valid_rounding_mode rm = (rm != 0b101 & rm != 0b110)
 
-val      select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode) effect {rreg}
+val      select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode)
 function select_instr_or_fcsr_rm instr_rm =
   if (instr_rm == RM_DYN)
   then {
@@ -345,7 +345,7 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE)        if haveDExt()
 /* Execution semantics ================================ */
 
 val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64)))
-                      -> Retired effect {escape, rreg, wreg}
+                      -> Retired
 function process_fload64(rd, addr, value) =
   if   sizeof(flen) == 64
   then match value {
@@ -358,7 +358,7 @@ function process_fload64(rd, addr, value) =
   }
 
 val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32)))
-                      -> Retired effect {escape, rreg, wreg}
+                      -> Retired
 function process_fload32(rd, addr, value) =
   match value {
     MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
@@ -366,7 +366,7 @@ function process_fload32(rd, addr, value) =
   }
 
 val process_fload16 : (regidx, xlenbits, MemoryOpResult(bits(16)))
-                      -> Retired effect {escape, rreg, wreg}
+                      -> Retired
 function process_fload16(rd, addr, value) =
   match value {
     MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS },
@@ -430,7 +430,7 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE)
 
 /* Execution semantics ================================ */
 
-val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired effect {escape, rreg, wreg}
+val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired
 function process_fstore(vaddr, value) =
   match value {
     MemValue(true)  => { RETIRE_SUCCESS },
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 1472589..0f36dee 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -156,7 +156,7 @@ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
 
 $ifdef RVFI_DII
-val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit effect {wreg}
+val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit
 function rvfi_read (addr, width, result) = {
   rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr);
   rvfi_mem_data_present = true;
@@ -176,15 +176,15 @@ $endif
 
 /* NOTE: The rreg effect is due to MMIO. */
 $ifdef RVFI_DII
-val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {wreg, rmem, rmemt, rreg, escape}
-val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {wreg, rmem, rmemt, rreg, escape}
-val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
-val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {wreg, rmem, rmemt, rreg, escape}
+val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))
+val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
+val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
 $else
-val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {rmem, rmemt, rreg, escape}
-val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))             effect {rmem, rmemt, rreg, escape}
-val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
-val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) effect {rmem, rmemt, rreg, escape}
+val mem_read      : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))
+val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool)       -> MemoryOpResult(bits(8 * 'n))
+val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
+val mem_read_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, atom('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta))
 $endif
 
 /* The most generic memory read operation */
@@ -212,7 +212,7 @@ function mem_read_priv (typ, priv, paddr, width, aq, rl, res) =
 function mem_read (typ, paddr, width, aq, rel, res) =
   mem_read_priv(typ, effectivePrivilege(typ, mstatus, cur_privilege), paddr, width, aq, rel, res)
 
-val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
+val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit)
 
 function mem_write_ea (addr, width, aq, rl, con) = {
   if (rl | con) & not(is_aligned_addr(addr, width))
@@ -230,7 +230,7 @@ function mem_write_ea (addr, width, aq, rl, con) = {
 }
 
 $ifdef RVFI_DII
-val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit effect {wreg}
+val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit
 function rvfi_write (addr, width, value, meta, result) = {
   rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr);
   rvfi_mem_data_present = true;
@@ -288,7 +288,7 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, pa
  * data.
  * NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime.
  */
-val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool)
 function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl, con) = {
   if (rl | con) & not(is_aligned_addr(paddr, width))
   then MemException(E_SAMO_Addr_Align())
@@ -311,12 +311,12 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl
 }
 
 /* Memory write with explicit Privilege, implicit AccessType and metadata */
-val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+val mem_write_value_priv : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), Privilege, bool, bool, bool) -> MemoryOpResult(bool)
 function mem_write_value_priv (paddr, width, value, priv, aq, rl, con) =
   mem_write_value_priv_meta(paddr, width, value, Write(default_write_acc), priv, default_meta, aq, rl, con)
 
 /* Memory write with explicit metadata and AccessType, implicit and Privilege */
-val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+val mem_write_value_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), ext_access_type, mem_meta, bool, bool, bool) -> MemoryOpResult(bool)
 function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con) = {
   let typ = Write(ext_acc);
   let ep = effectivePrivilege(typ, mstatus, cur_privilege);
@@ -324,7 +324,7 @@ function mem_write_value_meta (paddr, width, value, ext_acc, meta, aq, rl, con)
 }
 
 /* Memory write with default AccessType, Privilege, and metadata */
-val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
+val mem_write_value : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool)
 function mem_write_value (paddr, width, value, aq, rl, con) = {
   mem_write_value_meta(paddr, width, value, default_write_acc, default_meta, aq, rl, con)
 }
diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail
index 9c3c742..dee566a 100644
--- a/model/riscv_pc_access.sail
+++ b/model/riscv_pc_access.sail
@@ -76,18 +76,18 @@
   The value in the PC register is the absolute virtual address of the instruction
   to fetch.
  */
-val get_arch_pc : unit -> xlenbits effect {rreg}
+val get_arch_pc : unit -> xlenbits
 function get_arch_pc() = PC
 
-val get_next_pc : unit -> xlenbits effect {rreg}
+val get_next_pc : unit -> xlenbits
 function get_next_pc() = nextPC
 
-val set_next_pc : xlenbits -> unit effect {wreg}
+val set_next_pc : xlenbits -> unit
 function set_next_pc(pc) = {
   nextPC = pc
 }
 
-val tick_pc : unit -> unit effect {rreg, wreg}
+val tick_pc : unit -> unit
 function tick_pc() = {
   PC = nextPC
 }
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 6194b8f..579a118 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -212,7 +212,7 @@ let MTIMECMP_BASE_HI : xlenbits = zero_extend(0x04004)
 let MTIME_BASE       : xlenbits = zero_extend(0x0bff8)
 let MTIME_BASE_HI    : xlenbits = zero_extend(0x0bffc)
 
-val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
+val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
 function clint_load(t, addr, width) = {
   let addr = addr - plat_clint_base ();
   /* FIXME: For now, only allow exact aligned access. */
@@ -284,7 +284,7 @@ function clint_dispatch() -> unit = {
 }
 
 /* The rreg effect is due to checking mtime. */
-val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg}
+val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool)
 function clint_store(addr, width, data) = {
   let addr = addr - plat_clint_base ();
   if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
@@ -318,7 +318,7 @@ function clint_store(addr, width, data) = {
   }
 }
 
-val tick_clock : unit -> unit effect {rreg, wreg}
+val tick_clock : unit -> unit
 function tick_clock() = {
   if   mcountinhibit.CY() == 0b0
   then mcycle = mcycle + 1;
@@ -367,7 +367,7 @@ function reset_htif () -> unit = {
  * dispatched the address.
  */
 
-val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
+val htif_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
 function htif_load(t, paddr, width) = {
   if   get_config_print_platform()
   then print_platform("htif[" ^ BitStr(paddr) ^ "] -> " ^ BitStr(htif_tohost));
@@ -386,7 +386,7 @@ function htif_load(t, paddr, width) = {
 }
 
 /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */
-val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg}
+val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool)
 function htif_store(paddr, width, data) = {
   if   get_config_print_platform()
   then print_platform("htif[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data));
@@ -444,7 +444,7 @@ function htif_store(paddr, width, data) = {
   MemValue(true)
 }
 
-val htif_tick : unit -> unit effect {rreg, wreg}
+val htif_tick : unit -> unit
 function htif_tick() = {
   if   get_config_print_platform()
   then print_platform("htif::tick " ^ BitStr(htif_tohost));
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index d022006..9b6355c 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -140,7 +140,7 @@ register pmpaddr15 : xlenbits
 
 /* Packing and unpacking pmpcfg regs for xlen-width accesses */
 
-val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits effect {rreg}
+val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits
 function pmpReadCfgReg(n) = {
   if   sizeof(xlen) == 32
   then match n {
@@ -168,7 +168,7 @@ function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
   if pmpLocked(cfg) then cfg
   else Mk_Pmpcfg_ent(v & 0x9f)  // Bits 5 and 6 are zero.
 
-val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
+val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit
 function pmpWriteCfgReg(n, v) = {
   if   sizeof(xlen) == 32
   then match n {
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index ec4a2c6..15e7613 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -110,7 +110,7 @@ register x29 : regtype
 register x30 : regtype
 register x31 : regtype
 
-val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg, escape}
+val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits
 function rX r = {
   let v : regtype =
     match r {
@@ -152,7 +152,7 @@ function rX r = {
 }
 
 $ifdef RVFI_DII
-val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit
 function rvfi_wX (r,v) = {
   rvfi_int_data->rvfi_rd_wdata() = zero_extend(v);
   rvfi_int_data->rvfi_rd_addr() = to_bits(8,r);
@@ -163,7 +163,7 @@ val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit
 function rvfi_wX (r,v) = ()
 $endif
 
-val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg, escape}
+val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit
 function wX (r, in_v) = {
   let v = regval_into_reg(in_v);
   match r {
@@ -308,7 +308,7 @@ mapping creg_name : bits(3) <-> string = {
   0b111 <-> "a5"
 }
 
-val init_base_regs : unit -> unit effect {wreg}
+val init_base_regs : unit -> unit
 function init_base_regs () = {
   x1  = zero_reg;
   x2  = zero_reg;
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 3be28c8..b98c444 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/model/riscv_softfloat_interface.sail
@@ -107,7 +107,7 @@ register float_result : bits(64)
 register float_fflags : bits(64)
 
 /* updater to keep the flags in sync with fcsr.fflags */
-val update_softfloat_fflags : bits(5) -> unit effect {wreg}
+val update_softfloat_fflags : bits(5) -> unit
 function update_softfloat_fflags(flags) = {
   float_fflags = sail_zero_extend(flags, 64);
 }
@@ -116,84 +116,84 @@ function update_softfloat_fflags(flags) = {
 /* ADD/SUB/MUL/DIV                                                  */
 
 val     extern_f16Add = {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit
-val      riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Add (rm, v1, v2) = {
   extern_f16Add(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f16Sub = {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit
-val      riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Sub (rm, v1, v2) = {
   extern_f16Sub(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f16Mul = {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit
-val      riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Mul (rm, v1, v2) = {
   extern_f16Mul(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f16Div = {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit
-val      riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Div (rm, v1, v2) = {
   extern_f16Div(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit
-val      riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Add (rm, v1, v2) = {
   extern_f32Add(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit
-val      riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Sub (rm, v1, v2) = {
   extern_f32Sub(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit
-val      riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Mul (rm, v1, v2) = {
   extern_f32Mul(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit
-val      riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Div (rm, v1, v2) = {
   extern_f32Div(rm, v1, v2);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit
-val      riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Add (rm, v1, v2) = {
   extern_f64Add(rm, v1, v2);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit
-val      riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Sub (rm, v1, v2) = {
   extern_f64Sub(rm, v1, v2);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit
-val      riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Mul (rm, v1, v2) = {
   extern_f64Mul(rm, v1, v2);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit
-val      riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Div (rm, v1, v2) = {
   extern_f64Div(rm, v1, v2);
   (float_fflags[4 .. 0], float_result)
@@ -203,21 +203,21 @@ function riscv_f64Div (rm, v1, v2) = {
 /* MULTIPLY-ADD                                                     */
 
 val     extern_f16MulAdd = {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit
-val      riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16MulAdd (rm, v1, v2, v3) = {
   extern_f16MulAdd(rm, v1, v2, v3);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit
-val      riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32MulAdd (rm, v1, v2, v3) = {
   extern_f32MulAdd(rm, v1, v2, v3);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit
-val      riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64MulAdd (rm, v1, v2, v3) = {
   extern_f64MulAdd(rm, v1, v2, v3);
   (float_fflags[4 .. 0], float_result)
@@ -227,21 +227,21 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = {
 /* SQUARE ROOT                                                      */
 
 val     extern_f16Sqrt = {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit
-val      riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Sqrt (rm, v) = {
   extern_f16Sqrt(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit
-val      riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Sqrt (rm, v) = {
   extern_f32Sqrt(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit
-val      riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Sqrt (rm, v) = {
   extern_f64Sqrt(rm, v);
   (float_fflags[4 .. 0], float_result)
@@ -251,210 +251,210 @@ function riscv_f64Sqrt (rm, v) = {
 /* CONVERSIONS                                                      */
 
 val     extern_f16ToI32 = {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit
-val      riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W) effect {rreg}
+val      riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W)
 function riscv_f16ToI32 (rm, v) = {
   extern_f16ToI32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f16ToUi32 = {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit
-val      riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU) effect {rreg}
+val      riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU)
 function riscv_f16ToUi32 (rm, v) = {
   extern_f16ToUi32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_i32ToF16 = {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit
-val      riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H)
 function riscv_i32ToF16 (rm, v) = {
   extern_i32ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_ui32ToF16 = {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit
-val      riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H)
 function riscv_ui32ToF16 (rm, v) = {
   extern_ui32ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f16ToI64 = {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit
-val      riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L) effect {rreg}
+val      riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L)
 function riscv_f16ToI64 (rm, v) = {
   extern_f16ToI64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f16ToUi64 = {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit
-val      riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU) effect {rreg}
+val      riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU)
 function riscv_f16ToUi64 (rm, v) = {
   extern_f16ToUi64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_i64ToF16 = {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit
-val      riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H)
 function riscv_i64ToF16 (rm, v) = {
   extern_i64ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_ui64ToF16 = {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit
-val      riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H)
 function riscv_ui64ToF16 (rm, v) = {
   extern_ui64ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit
-val      riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W) effect {rreg}
+val      riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W)
 function riscv_f32ToI32 (rm, v) = {
   extern_f32ToI32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit
-val      riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU) effect {rreg}
+val      riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU)
 function riscv_f32ToUi32 (rm, v) = {
   extern_f32ToUi32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit
-val      riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S)
 function riscv_i32ToF32 (rm, v) = {
   extern_i32ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit
-val      riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S)
 function riscv_ui32ToF32 (rm, v) = {
   extern_ui32ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit
-val      riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L) effect {rreg}
+val      riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L)
 function riscv_f32ToI64 (rm, v) = {
   extern_f32ToI64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit
-val      riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU) effect {rreg}
+val      riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU)
 function riscv_f32ToUi64 (rm, v) = {
   extern_f32ToUi64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit
-val      riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S)
 function riscv_i64ToF32 (rm, v) = {
   extern_i64ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit
-val      riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S)
 function riscv_ui64ToF32 (rm, v) = {
   extern_ui64ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit
-val      riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W) effect {rreg}
+val      riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W)
 function riscv_f64ToI32 (rm, v) = {
   extern_f64ToI32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit
-val      riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU) effect {rreg}
+val      riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU)
 function riscv_f64ToUi32 (rm, v) = {
   extern_f64ToUi32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit
-val      riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D)
 function riscv_i32ToF64 (rm, v) = {
   extern_i32ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit
-val      riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D)
 function riscv_ui32ToF64 (rm, v) = {
   extern_ui32ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit
-val      riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L) effect {rreg}
+val      riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L)
 function riscv_f64ToI64 (rm, v) = {
   extern_f64ToI64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit
-val      riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU) effect {rreg}
+val      riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU)
 function riscv_f64ToUi64 (rm, v) = {
   extern_f64ToUi64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit
-val      riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D)
 function riscv_i64ToF64 (rm, v) = {
   extern_i64ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit
-val      riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D)
 function riscv_ui64ToF64 (rm, v) = {
   extern_ui64ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit
-val      riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S)
 function riscv_f16ToF32 (rm, v) = {
   extern_f16ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f16ToF64 = {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit
-val      riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D)
 function riscv_f16ToF64 (rm, v) = {
   extern_f16ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit
-val      riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D)
 function riscv_f32ToF64 (rm, v) = {
   extern_f32ToF64(rm, v);
   (float_fflags[4 .. 0], float_result)
 }
 
 val     extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit
-val      riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H)
 function riscv_f32ToF16 (rm, v) = {
   extern_f32ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit
-val      riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H)
 function riscv_f64ToF16 (rm, v) = {
   extern_f64ToF16(rm, v);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit
-val      riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S)
 function riscv_f64ToF32 (rm, v) = {
   extern_f64ToF32(rm, v);
   (float_fflags[4 .. 0], float_result[31 .. 0])
@@ -464,126 +464,126 @@ function riscv_f64ToF32 (rm, v) = {
 /* COMPARISONS                                                      */
 
 val     extern_f16Lt = {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit
-val      riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Lt (v1, v2) = {
   extern_f16Lt(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit
-val      riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Lt_quiet (v1, v2) = {
   extern_f16Lt_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit
-val      riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Le (v1, v2) = {
   extern_f16Le(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit
-val      riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Le_quiet (v1, v2) = {
   extern_f16Le_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit
-val      riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Eq (v1, v2) = {
   extern_f16Eq(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit
-val      riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Lt (v1, v2) = {
   extern_f32Lt(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit
-val      riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Lt_quiet (v1, v2) = {
   extern_f32Lt_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit
-val      riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Le (v1, v2) = {
   extern_f32Le(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit
-val      riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Le_quiet (v1, v2) = {
   extern_f32Le_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit
-val      riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Eq (v1, v2) = {
   extern_f32Eq(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit
-val      riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Lt (v1, v2) = {
   extern_f64Lt(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit
-val      riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Lt_quiet (v1, v2) = {
   extern_f64Lt_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit
-val      riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Le (v1, v2) = {
   extern_f64Le(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit
-val      riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Le_quiet (v1, v2) = {
   extern_f64Le_quiet(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit
-val      riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg}
+val      riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Eq (v1, v2) = {
   extern_f64Eq(v1, v2);
   (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
 }
 
 val     extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit
-val      riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) effect {rreg}
+val      riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H)
 function riscv_f16roundToInt (rm, v, exact) = {
   extern_f16roundToInt(rm, v, exact);
   (float_fflags[4 .. 0], float_result[15 .. 0])
 }
 
 val     extern_f32roundToInt = {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit
-val      riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S) effect {rreg}
+val      riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S)
 function riscv_f32roundToInt (rm, v, exact) = {
   extern_f32roundToInt(rm, v, exact);
   (float_fflags[4 .. 0], float_result[31 .. 0])
 }
 
 val     extern_f64roundToInt = {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit
-val      riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D) effect {rreg}
+val      riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D)
 function riscv_f64roundToInt (rm, v, exact) = {
   extern_f64roundToInt(rm, v, exact);
   (float_fflags[4 .. 0], float_result)
diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail
index c266e6b..d23a679 100644
--- a/model/riscv_step_rvfi.sail
+++ b/model/riscv_step_rvfi.sail
@@ -79,7 +79,7 @@ function ext_post_step_hook() -> unit = {
   rvfi_pc_data->rvfi_pc_wdata() = zero_extend(get_arch_pc())
 }
 
-val ext_init : unit -> unit effect {wreg}
+val ext_init : unit -> unit
 function ext_init() = {
   init_base_regs();
   init_fdext_regs();
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index b854053..cf0a488 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -228,7 +228,7 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
  * where cancellation can be performed.
  */
 
-val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool effect {exmem}
+val speculate_conditional = {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool
 
 val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
 val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool
@@ -377,7 +377,7 @@ function tval(excinfo : option(xlenbits)) -> xlenbits = {
 }
 
 $ifdef RVFI_DII
-val rvfi_trap : unit -> unit effect {wreg}
+val rvfi_trap : unit -> unit
 // TODO: record rvfi_trap_data
 function rvfi_trap () =
   rvfi_inst_data->rvfi_trap() = 0x01
diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail
index a4fc8f0..14cc05c 100644
--- a/model/riscv_sys_exceptions.sail
+++ b/model/riscv_sys_exceptions.sail
@@ -99,7 +99,7 @@ function prepare_trap_vector(p : Privilege, cause : Mcause) -> xlenbits = {
  * prepare_xret_target: used to get the value for control transfer to the xret target
  */
 
-val get_xret_target : Privilege -> xlenbits effect {rreg}
+val get_xret_target : Privilege -> xlenbits
 function get_xret_target(p) =
   match p {
     Machine    => mepc,
@@ -107,7 +107,7 @@ function get_xret_target(p) =
     User       => uepc
   }
 
-val set_xret_target : (Privilege, xlenbits) -> xlenbits effect {rreg, wreg}
+val set_xret_target : (Privilege, xlenbits) -> xlenbits
 function set_xret_target(p, value) = {
   let target = legalize_xepc(value);
   match p {
@@ -118,7 +118,7 @@ function set_xret_target(p, value) = {
   target
 }
 
-val prepare_xret_target : (Privilege) -> xlenbits effect {rreg, wreg}
+val prepare_xret_target : (Privilege) -> xlenbits
 function prepare_xret_target(p) =
   get_xret_target(p)
 
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 251df5a..4774469 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -154,7 +154,7 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "
 /* This function allows an extension to veto a write to Misa
    if it would violate an alignment restriction on
    unsetting C. If it returns true the write will have no effect. */
-val ext_veto_disable_C : unit -> bool effect {rreg}
+val ext_veto_disable_C : unit -> bool
 
 function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
   let  v = Mk_Misa(v);
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index 728c1d2..b940286 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -138,10 +138,10 @@ union exception = {
   Error_internal_error  : unit
 }
 
-val not_implemented : forall ('a : Type). string -> 'a effect {escape}
+val not_implemented : forall ('a : Type). string -> 'a
 function not_implemented message = throw(Error_not_implemented(message))
 
-val internal_error : forall ('a : Type). (string, int, string) -> 'a effect {escape}
+val internal_error : forall ('a : Type). (string, int, string) -> 'a
 function internal_error(file, line, s) = {
     assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s);
     throw Error_internal_error()
@@ -464,7 +464,7 @@ function word_width_bytes width = match width {
  * should be unreachable. See https://github.com/riscv/sail-riscv/issues/194
  * and https://github.com/riscv/sail-riscv/pull/197 .
  */
-val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a effect {escape}
+val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a
 function report_invalid_width(f , l, w, k) -> 'a = {
   /*
    * Ideally we would call internal_error here but this triggers a Sail bug,
diff --git a/model/riscv_types_kext.sail b/model/riscv_types_kext.sail
index ef03d9b..9f9892f 100644
--- a/model/riscv_types_kext.sail
+++ b/model/riscv_types_kext.sail
@@ -144,7 +144,7 @@ function aes_mixcolumn_inv(x) = {
    do not decode to the AES64KS1I instruction. The 0xA case is used
    specifically for the AES-256 KeySchedule, and this function is never
    called in that case. */
-val aes_decode_rcon : bits(4) -> bits(32) effect {escape}
+val aes_decode_rcon : bits(4) -> bits(32)
 function aes_decode_rcon(r) = {
   assert(r <_u 0xA);
   match r {
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
index ba29332..3478be4 100644
--- a/model/riscv_vmem_rv32.sail
+++ b/model/riscv_vmem_rv32.sail
@@ -79,7 +79,7 @@ function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits
 
 /* Compute the address translation mode. */
 
-val translationMode : (Privilege) -> SATPMode effect {rreg, escape}
+val translationMode : (Privilege) -> SATPMode
 function translationMode(priv) = {
   if priv == Machine then Sbare
   else {
@@ -96,7 +96,7 @@ function translationMode(priv) = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType)
 function translateAddr_priv(vAddr, ac, effPriv) = {
   let mxr    : bool   = mstatus.MXR() == 0b1;
   let do_sum : bool   = mstatus.SUM() == 0b1;
@@ -118,11 +118,11 @@ function translateAddr_priv(vAddr, ac, effPriv) = {
   }
 }
 
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType)
 function translateAddr(vAddr, ac) =
   translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege))
 
-val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit effect {rreg, wreg}
+val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit
 function flush_TLB(asid_xlen, addr_xlen) -> unit = {
   let asid : option(asid32) =
     match (asid_xlen) {
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index 10b2067..18d0991 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -93,7 +93,7 @@ function isValidSv48Addr(vAddr : xlenbits) -> bool = {
 
 /* Compute the address translation mode. */
 
-val translationMode : (Privilege) -> SATPMode effect {rreg, escape}
+val translationMode : (Privilege) -> SATPMode
 function translationMode(priv) = {
   if priv == Machine then Sbare
   else {
@@ -117,7 +117,7 @@ function translationMode(priv) = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType)
 function translateAddr_priv(vAddr, ac, effPriv) = {
   let mxr    : bool   = mstatus.MXR() == 0b1;
   let do_sum : bool   = mstatus.SUM() == 0b1;
@@ -149,11 +149,11 @@ function translateAddr_priv(vAddr, ac, effPriv) = {
   }
 }
 
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType)
 function translateAddr(vAddr, ac) =
   translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege))
 
-val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit effect {rreg, wreg}
+val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit
 function flush_TLB(asid_xlen, addr_xlen) -> unit = {
   /* Flush both Sv39 and Sv48 TLBs. */
   let (addr39, addr48) : (option(vaddr39), option(vaddr48)) =
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index e8365c3..72def15 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -76,7 +76,7 @@
 
 function to_phys_addr(a : paddr32) -> xlenbits = a[31..0]
 
-val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rmemt, rreg, escape}
+val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE)
 function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let va = Mk_SV32_Vaddr(vaddr);
   let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]),
@@ -158,14 +158,14 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
 type TLB32_Entry = TLB_Entry(9, 32, 34, 32)
 register tlb32 : option(TLB32_Entry)
 
-val lookup_TLB32 : (asid32, vaddr32) -> option((nat, TLB32_Entry)) effect {rreg}
+val lookup_TLB32 : (asid32, vaddr32) -> option((nat, TLB32_Entry))
 function lookup_TLB32(asid, vaddr) =
   match tlb32 {
     None()  => None(),
     Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None()
   }
 
-val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit effect {wreg, rreg}
+val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit
 function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
   let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV32_LEVEL_BITS);
   tlb32 = Some(ent)
@@ -174,7 +174,7 @@ function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
 function write_TLB32(idx : nat, ent : TLB32_Entry) -> unit =
   tlb32 = Some(ent)
 
-val flush_TLB32 : (option(asid32), option(vaddr32)) -> unit effect {rreg, wreg}
+val flush_TLB32 : (option(asid32), option(vaddr32)) -> unit
 function flush_TLB32(asid, addr) =
   match (tlb32) {
     None()  => (),
@@ -185,7 +185,7 @@ function flush_TLB32(asid, addr) =
 
 /* address translation */
 
-val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
+val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error)
 function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
   match lookup_TLB32(asid, vAddr) {
     Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index 384b6ec..25378a8 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -70,7 +70,7 @@
 
 /* Sv39 address translation for RV64. */
 
-val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rmemt, rreg, escape}
+val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE)
 function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let va = Mk_SV39_Vaddr(vaddr);
   let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
@@ -152,14 +152,14 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
 type TLB39_Entry = TLB_Entry(16, 39, 56, 64)
 register tlb39 : option(TLB39_Entry)
 
-val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry)) effect {rreg}
+val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry))
 function lookup_TLB39(asid, vaddr) =
   match tlb39 {
     None()  => None(),
     Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None()
   }
 
-val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit effect {wreg, rreg}
+val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit
 function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
   let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV39_LEVEL_BITS);
   tlb39 = Some(ent)
@@ -168,7 +168,7 @@ function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
 function write_TLB39(idx : nat, ent : TLB39_Entry) -> unit =
   tlb39 = Some(ent)
 
-val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg}
+val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit
 function flush_TLB39(asid, addr) =
   match (tlb39) {
     None()  => (),
@@ -179,7 +179,7 @@ function flush_TLB39(asid, addr) =
 
 /* address translation */
 
-val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
+val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error)
 function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
   match lookup_TLB39(asid, vAddr) {
     Some(idx, ent) => {
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index 729a701..64c7a54 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -70,7 +70,7 @@
 
 /* Sv48 address translation for RV64. */
 
-val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rmemt, rreg, escape}
+val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE)
 function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let va = Mk_SV48_Vaddr(vaddr);
   let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
@@ -152,14 +152,14 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
 type TLB48_Entry = TLB_Entry(16, 48, 56, 64)
 register tlb48 : option(TLB48_Entry)
 
-val lookup_TLB48 : (asid64, vaddr48) -> option((nat, TLB48_Entry)) effect {rreg}
+val lookup_TLB48 : (asid64, vaddr48) -> option((nat, TLB48_Entry))
 function lookup_TLB48(asid, vaddr) =
   match tlb48 {
     None()  => None(),
     Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None()
   }
 
-val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit effect {wreg, rreg}
+val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit
 function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
   let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV48_LEVEL_BITS);
   tlb48 = Some(ent)
@@ -168,7 +168,7 @@ function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
 function write_TLB48(idx : nat, ent : TLB48_Entry) -> unit =
   tlb48 = Some(ent)
 
-val flush_TLB48 : (option(asid64), option(vaddr48)) -> unit effect {rreg, wreg}
+val flush_TLB48 : (option(asid64), option(vaddr48)) -> unit
 function flush_TLB48(asid, addr) =
   match (tlb48) {
     None()  => (),
@@ -179,7 +179,7 @@ function flush_TLB48(asid, addr) =
 
 /* address translation */
 
-val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
+val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error)
 function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
   match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) {
     PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),
diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail
index ae24815..27b63ba 100644
--- a/model/riscv_vmem_tlb.sail
+++ b/model/riscv_vmem_tlb.sail
@@ -85,7 +85,7 @@ struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int) = {
 
 val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, 'valen > 0.
   (bits('asidlen), bool, bits('valen), bits('palen), bits('ptelen), nat, bits('palen), nat)
-  -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen) effect {rreg}
+  -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen)
 function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBitSize) = {
   let shift : nat = PAGESIZE_BITS + (level * levelBitSize);
   /* fixme hack: use a better idiom for masks */
diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail
index 5c87465..e1007bb 100644
--- a/model/rvfi_dii.sail
+++ b/model/rvfi_dii.sail
@@ -86,16 +86,16 @@ bitfield RVFI_DII_Instruction_Packet : bits(64) = {
 
 register rvfi_instruction : RVFI_DII_Instruction_Packet
 
-val rvfi_set_instr_packet : bits(64) -> unit effect {wreg}
+val rvfi_set_instr_packet : bits(64) -> unit
 
 function rvfi_set_instr_packet(p) =
   rvfi_instruction = Mk_RVFI_DII_Instruction_Packet(p)
 
-val rvfi_get_cmd : unit -> bits(8) effect {rreg}
+val rvfi_get_cmd : unit -> bits(8)
 
 function rvfi_get_cmd () = rvfi_instruction.rvfi_cmd()
 
-val rvfi_get_insn : unit -> bits(32) effect {rreg}
+val rvfi_get_insn : unit -> bits(32)
 
 function rvfi_get_insn () = rvfi_instruction.rvfi_insn()
 
@@ -261,7 +261,7 @@ register rvfi_mem_data : RVFI_DII_Execution_Packet_Ext_MemAccess
 register rvfi_mem_data_present : bool
 
 // Reset the trace
-val rvfi_zero_exec_packet : unit -> unit effect {wreg}
+val rvfi_zero_exec_packet : unit -> unit
 
 function rvfi_zero_exec_packet () = {
   rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zero_extend(0b0));
@@ -278,7 +278,7 @@ function rvfi_zero_exec_packet () = {
 
 // FIXME: most of these will no longer be necessary once we use the c2 sail backend.
 
-val rvfi_halt_exec_packet : unit -> unit effect {wreg}
+val rvfi_halt_exec_packet : unit -> unit
 
 function rvfi_halt_exec_packet () =
   rvfi_inst_data->rvfi_halt() = 0x01
@@ -294,7 +294,7 @@ function rvfi_get_v2_support_packet () = {
   return rvfi_exec.bits();
 }
 
-val rvfi_get_exec_packet_v1 : unit -> bits(704) effect {rreg}
+val rvfi_get_exec_packet_v1 : unit -> bits(704)
 function rvfi_get_exec_packet_v1 () = {
   let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0));
   // Convert the v2 packet to a v1 packet
@@ -323,7 +323,7 @@ function rvfi_get_exec_packet_v1 () = {
   return v1_packet.bits();
 }
 
-val rvfi_get_v2_trace_size : unit -> bits(64) effect {rreg}
+val rvfi_get_v2_trace_size : unit -> bits(64)
 function rvfi_get_v2_trace_size () = {
   let trace_size : bits(64) = to_bits(64, 512);
   let trace_size = if (rvfi_int_data_present) then trace_size + 320 else trace_size;
@@ -331,7 +331,7 @@ function rvfi_get_v2_trace_size () = {
   return trace_size >> 3; // we have to return bytes not bits
 }
 
-val rvfi_get_exec_packet_v2 : unit -> bits(512) effect {rreg}
+val rvfi_get_exec_packet_v2 : unit -> bits(512)
 function rvfi_get_exec_packet_v2 () = {
   // TODO: add the other data
   // TODO: find a way to return a variable-length bitvector
@@ -348,13 +348,13 @@ function rvfi_get_exec_packet_v2 () = {
   return packet.bits();
 }
 
-val rvfi_get_int_data : unit -> bits(320) effect {rreg}
+val rvfi_get_int_data : unit -> bits(320)
 function rvfi_get_int_data () = {
   assert(rvfi_int_data_present, "reading uninitialized data");
   return rvfi_int_data.bits();
 }
 
-val rvfi_get_mem_data : unit -> bits(704) effect {rreg}
+val rvfi_get_mem_data : unit -> bits(704)
 function rvfi_get_mem_data () = {
   assert(rvfi_mem_data_present, "reading uninitialized data");
   return rvfi_mem_data.bits();
@@ -365,7 +365,7 @@ val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. atom('n) -> bits(32)
 function rvfi_encode_width_mask(width) =
   (0xFFFFFFFF >> (32 - width))
 
-val print_rvfi_exec : unit -> unit effect {rreg}
+val print_rvfi_exec : unit -> unit
 
 function print_rvfi_exec () = {
   print_bits("rvfi_intr     : ", rvfi_inst_data.rvfi_intr());