Merge pull request #540 from Timmmm/user/timh/warnings

Fix all Sail compilation warnings

5 files changed, 124 insertions, 134 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index c924a2f..a441e3a 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -41,47 +41,37 @@ overload BitStr = {bits_str, bit_str}
 
 overload operator ^ = {xor_vec, concat_str}
 
-val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val sub_vec = pure {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
+val sub_vec_int = pure {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
 
 overload operator - = {sub_vec, sub_vec_int}
 
-val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
-val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
+val quot_round_zero = pure {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
+val rem_round_zero = pure {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
 
 /* The following defines % as euclidean modulus */
 overload operator % = {emod_int}
 
-val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_atom", c: "min_int"} : forall 'x 'y.
-  (int('x), int('y)) -> {'z, ('x <= 'y & 'z == 'x) | ('x > 'y & 'z == 'y). int('z)}
-
-val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_atom", c: "max_int"} : forall 'x 'y.
-  (int('x), int('y)) -> {'z, ('x >= 'y & 'z == 'x) | ('x < 'y & 'z == 'y). int('z)}
-
 overload min = {min_int}
-
 overload max = {max_int}
 
-val pow2 = "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
-
-val print = "print_endline" : string -> unit
-val print_string = "print_string" : (string, string) -> unit
+val print_string = pure "print_string" : (string, string) -> unit
 
-val print_instr    = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_reg      = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_mem      = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
-val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_instr    = pure {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_reg      = pure {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_mem      = pure {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit
+val print_platform = pure {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit
 
-val print_step = {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit
+val print_step = pure {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit
 
 function print_step() = ()
 
-val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
-val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
-val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
+val get_config_print_instr = pure {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool
+val get_config_print_reg = pure {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool
+val get_config_print_mem = pure {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool
 
-val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
+val get_config_print_platform = pure {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool
 // defaults for other backends
 function get_config_print_instr () = false
 function get_config_print_reg () = false
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 2dc6e75..b7a498c 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -14,13 +14,13 @@
    - it relies on externs to get platform address information and doesn't hardcode them
 */
 
-val elf_tohost = {
+val elf_tohost = pure {
   ocaml: "Elf_loader.elf_tohost",
   interpreter: "Elf_loader.elf_tohost",
   c: "elf_tohost"
 } :  unit -> int
 
-val elf_entry = {
+val elf_entry = pure {
   ocaml: "Elf_loader.elf_entry",
   interpreter: "Elf_loader.elf_entry",
   c: "elf_entry"
@@ -29,42 +29,42 @@ val elf_entry = {
 // Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096)
 // because this model performs `cbo.zero` with a single write, and the behaviour
 // with cache blocks larger than a page is not clearly defined.
-val plat_cache_block_size_exp = {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12)
+val plat_cache_block_size_exp = pure {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12)
 
 /* Main memory */
-val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
-val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
+val plat_ram_base = pure {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
+val plat_ram_size = pure {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
 
 /* whether the MMU should update dirty bits in PTEs */
-val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update",
-                                interpreter: "Platform.enable_dirty_update",
-                                c: "plat_enable_dirty_update",
-                                lem: "plat_enable_dirty_update"} : unit -> bool
+val plat_enable_dirty_update = pure {ocaml: "Platform.enable_dirty_update",
+                                     interpreter: "Platform.enable_dirty_update",
+                                     c: "plat_enable_dirty_update",
+                                     lem: "plat_enable_dirty_update"} : unit -> bool
 
 /* whether the platform supports misaligned accesses without trapping to M-mode. if false,
  * misaligned loads/stores are trapped to Machine mode.
  */
-val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access",
-                                     interpreter: "Platform.enable_misaligned_access",
-                                     c: "plat_enable_misaligned_access",
-                                     lem: "plat_enable_misaligned_access"} : unit -> bool
+val plat_enable_misaligned_access = pure {ocaml: "Platform.enable_misaligned_access",
+                                          interpreter: "Platform.enable_misaligned_access",
+                                          c: "plat_enable_misaligned_access",
+                                          lem: "plat_enable_misaligned_access"} : unit -> bool
 
 /* whether mtval stores the bits of a faulting instruction on illegal instruction exceptions */
-val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_bits",
-                                        interpreter: "Platform.mtval_has_illegal_inst_bits",
-                                        c: "plat_mtval_has_illegal_inst_bits",
-                                        lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool
+val plat_mtval_has_illegal_inst_bits = pure {ocaml: "Platform.mtval_has_illegal_inst_bits",
+                                             interpreter: "Platform.mtval_has_illegal_inst_bits",
+                                             c: "plat_mtval_has_illegal_inst_bits",
+                                             lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool
 
 /* ROM holding reset vector and device-tree DTB */
-val plat_rom_base   = {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits
-val plat_rom_size   = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits
+val plat_rom_base   = pure {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits
+val plat_rom_size   = pure {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits
 
 /* Location of clock-interface, which should match with the spec in the DTB */
-val plat_clint_base = {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits
-val plat_clint_size = {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits
+val plat_clint_base = pure {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits
+val plat_clint_size = pure {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits
 
 /* Location of HTIF ports */
-val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits
+val plat_htif_tohost = pure {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits
 function plat_htif_tohost () = to_bits(sizeof(xlen), elf_tohost ())
 // todo: fromhost
 
@@ -124,7 +124,7 @@ function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlen
 
 /* CLINT (Core Local Interruptor), based on Spike. */
 
-val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int
+val plat_insns_per_tick = pure {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int
 
 // assumes a single hart, since this typically is a vector of per-hart registers.
 register mtimecmp : bits(64)  // memory-mapped internal clint register.
@@ -284,8 +284,8 @@ function tick_clock() = {
 
 /* Basic terminal character I/O. */
 
-val plat_term_write = {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit
-val plat_term_read  = {ocaml: "Platform.term_read",  c: "plat_term_read", lem: "plat_term_read"}  : unit -> bits(8)
+val plat_term_write = impure {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit
+val plat_term_read  = impure {ocaml: "Platform.term_read",  c: "plat_term_read", lem: "plat_term_read"}  : unit -> bits(8)
 
 /* Spike's HTIF device interface, which multiplexes the above MMIO devices. */
 
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 3a673fe..79a4678 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/model/riscv_softfloat_interface.sail
@@ -47,84 +47,84 @@ register float_fflags : bits(64)
 /* **************************************************************** */
 /* 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     extern_f16Add = pure {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)
 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     extern_f16Sub = pure {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)
 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     extern_f16Mul = pure {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)
 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     extern_f16Div = pure {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)
 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     extern_f32Add = pure {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)
 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     extern_f32Sub = pure {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)
 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     extern_f32Mul = pure {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)
 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     extern_f32Div = pure {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)
 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     extern_f64Add = pure {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)
 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     extern_f64Sub = pure {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)
 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     extern_f64Mul = pure {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)
 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     extern_f64Div = pure {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)
 function riscv_f64Div (rm, v1, v2) = {
   extern_f64Div(rm, v1, v2);
@@ -134,21 +134,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     extern_f16MulAdd = pure {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)
 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     extern_f32MulAdd = pure {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)
 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     extern_f64MulAdd = pure {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)
 function riscv_f64MulAdd (rm, v1, v2, v3) = {
   extern_f64MulAdd(rm, v1, v2, v3);
@@ -158,21 +158,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     extern_f16Sqrt = pure {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)
 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     extern_f32Sqrt = pure {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)
 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     extern_f64Sqrt = pure {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)
 function riscv_f64Sqrt (rm, v) = {
   extern_f64Sqrt(rm, v);
@@ -182,56 +182,56 @@ 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     extern_f16ToI32 = pure {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)
 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     extern_f16ToUi32 = pure {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)
 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     extern_i32ToF16 = pure {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)
 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     extern_ui32ToF16 = pure {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)
 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     extern_f16ToI64 = pure {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)
 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     extern_f16ToUi64 = pure {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)
 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     extern_i64ToF16 = pure {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)
 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     extern_ui64ToF16 = pure {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)
 function riscv_ui64ToF16 (rm, v) = {
   extern_ui64ToF16(rm, v);
@@ -239,154 +239,154 @@ function riscv_ui64ToF16 (rm, v) = {
 }
 
 
-val     extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToI32 = pure {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)
 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     extern_f32ToUi32 = pure {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)
 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     extern_i32ToF32 = pure {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)
 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     extern_ui32ToF32 = pure {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)
 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     extern_f32ToI64 = pure {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)
 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     extern_f32ToUi64 = pure {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)
 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     extern_i64ToF32 = pure {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)
 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     extern_ui64ToF32 = pure {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)
 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     extern_f64ToI32 = pure {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)
 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     extern_f64ToUi32 = pure {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)
 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     extern_i32ToF64 = pure {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)
 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     extern_ui32ToF64 = pure {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)
 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     extern_f64ToI64 = pure {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)
 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     extern_f64ToUi64 = pure {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)
 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     extern_i64ToF64 = pure {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)
 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     extern_ui64ToF64 = pure {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)
 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     extern_f16ToF32 = pure {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)
 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     extern_f16ToF64 = pure {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)
 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     extern_f32ToF64 = pure {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)
 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     extern_f32ToF16 = pure {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)
 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     extern_f64ToF16 = pure {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)
 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     extern_f64ToF32 = pure {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)
 function riscv_f64ToF32 (rm, v) = {
   extern_f64ToF32(rm, v);
@@ -396,126 +396,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     extern_f16Lt = pure {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)
 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     extern_f16Lt_quiet = pure {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)
 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     extern_f16Le = pure {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)
 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     extern_f16Le_quiet = pure {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)
 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     extern_f16Eq = pure {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)
 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     extern_f32Lt = pure {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)
 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     extern_f32Lt_quiet = pure {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)
 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     extern_f32Le = pure {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)
 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     extern_f32Le_quiet = pure {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)
 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     extern_f32Eq = pure {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)
 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     extern_f64Lt = pure {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)
 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     extern_f64Lt_quiet = pure {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)
 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     extern_f64Le = pure {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)
 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     extern_f64Le_quiet = pure {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)
 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     extern_f64Eq = pure {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)
 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     extern_f16roundToInt = pure {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)
 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     extern_f32roundToInt = pure {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)
 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     extern_f64roundToInt = pure {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)
 function riscv_f64roundToInt (rm, v, exact) = {
   extern_f64roundToInt(rm, v, exact);
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 2cd5df2..f8ec00a 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -165,11 +165,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
  * where cancellation can be performed.
  */
 
-val speculate_conditional = monadic {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool
+val speculate_conditional = impure {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
-val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
+val load_reservation = impure {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
+val match_reservation = pure {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool
+val cancel_reservation = impure {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
 
 /* Exception delegation: given an exception and the privilege at which
  * it occured, returns the privilege at which it should be handled.
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 6d1afd0..295a4da 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -79,39 +79,39 @@ bitfield Misa : xlenbits = {
 register misa : Misa
 
 /* whether misa is R/W */
-val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool
+val sys_enable_writable_misa = pure {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool
 /* whether misa.c was enabled at boot */
-val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
+val sys_enable_rvc = pure {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
 /* whether misa.{f,d} were enabled at boot */
-val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
+val sys_enable_fdext = pure {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
 /* whether Svinval was enabled at boot */
-val sys_enable_svinval = {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool
+val sys_enable_svinval = pure {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool
 /* whether Zcb was enabled at boot */
-val sys_enable_zcb = {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool
+val sys_enable_zcb = pure {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool
 /* whether zfinx was enabled at boot */
-val sys_enable_zfinx = {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool
+val sys_enable_zfinx = pure {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool
 /* whether the N extension was enabled at boot */
-val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool
+val sys_enable_next = pure {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool
 /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
    supervisor mode is implemented and non-bare addressing modes are supported. */
-val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
+val sys_enable_writable_fiom = pure {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
 
 /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */
-val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64)
+val sys_pmp_count = pure {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64)
 /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g.
    G=0 -> 4 bytes, G=10 -> 4096 bytes. */
-val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63)
+val sys_pmp_grain = pure {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63)
 
 /* whether misa.v was enabled at boot */
-val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool
+val sys_enable_vext = pure {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool
 
 /* whether misa.b was enabled at boot */
-val sys_enable_bext = {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool
+val sys_enable_bext = pure {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool
 
 // CBO extensions. Zicbop cannot be enabled/disabled because it has no effect
 // at all on this model.
-val sys_enable_zicbom = {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool
-val sys_enable_zicboz = {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool
+val sys_enable_zicbom = pure {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool
+val sys_enable_zicboz = pure {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool
 
 /* This function allows an extension to veto a write to Misa
    if it would violate an alignment restriction on
@@ -733,7 +733,7 @@ mapping opst_code : seed_opst <-> bits(2) = {
  *       for this function is unavailable when it's first encountered in
  *       read_seed_csr. Hence it appears here.
  */
-val get_16_random_bits = {
+val get_16_random_bits = impure {
     ocaml: "Platform.get_16_random_bits",
     interpreter: "Platform.get_16_random_bits",
     c: "plat_get_16_random_bits",