diff --git a/Makefile b/Makefile
index 9f284ca24..923c6a3d0 100644
--- a/Makefile
+++ b/Makefile
@@ -187,15 +187,7 @@ C_LIBS += $(SAIL_LIB_DIR)/coverage/libsail_coverage.a -lm -lpthread -ldl
 endif
 
 RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem
-# Feature detect if we are on the latest development version of Sail
-# and use an updated lem file if so. This is just until the opam
-# version catches up with changes to the barrier type.
-SAIL_LATEST := $(shell $(SAIL) -have_feature FEATURE_UNION_BARRIER 1>&2 2> /dev/null; echo $$?)
-ifeq ($(SAIL_LATEST),0)
-RISCV_EXTRAS_LEM = $(addprefix handwritten_support/0.11/,$(RISCV_EXTRAS_LEM_FILES))
-else
 RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
-endif
 
 .PHONY:
 
@@ -325,12 +317,12 @@ endif
 
 generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile
 	mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH)
-	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
+	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS)
 	echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem
 
 # sed -i isn't posix compliant, unfortunately
 generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile
-	lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
+	lem -wl ign -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \
 		$(RISCV_EXTRAS_LEM) \
 		generated_definitions/lem/$(ARCH)/riscv_types.lem \
 		generated_definitions/lem/$(ARCH)/riscv.lem
@@ -451,7 +443,7 @@ generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS)
 
 FORCE:
 
-SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard c_emulator/*.c)) $(sort $(wildcard c_emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(sort $(wildcard handwritten_support/0.11/*.lem)) $(RMEM_FILES)
+SHARE_FILES:=$(sort $(wildcard model/*.sail)) $(sort $(wildcard c_emulator/*.c)) $(sort $(wildcard c_emulator/*.h)) $(sort $(wildcard handwritten_support/*.lem)) $(sort $(wildcard handwritten_support/hgen/*.hgen)) $(RMEM_FILES)
 sail-riscv.install: FORCE
 	echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install
 	echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install
diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem
deleted file mode 100644
index 8a8c07014..000000000
--- a/handwritten_support/0.11/mem_metadata.lem
+++ /dev/null
@@ -1,16 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail2_instr_kinds
-open import Sail2_values
-open import Sail2_operators_mwords
-open import Sail2_prompt_monad
-open import Sail2_prompt
-
-val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e
-let write_ram wk addr width data meta =
-  write_mem wk () addr width data
-
-val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e
-let read_ram rk addr width read_tag =
-  read_mem rk () addr width >>= (fun (data : mword 'n) ->
-  return (data, ()))
diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem
deleted file mode 100644
index 2509057e6..000000000
--- a/handwritten_support/0.11/riscv_extras.lem
+++ /dev/null
@@ -1,172 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail2_instr_kinds
-open import Sail2_values
-open import Sail2_operators_mwords
-open import Sail2_prompt_monad
-open import Sail2_prompt
-
-type bitvector 'a = mword 'a
-
-let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ())
-let MEM_fence_r_rw  () = barrier (Barrier_RISCV_r_rw ())
-let MEM_fence_r_r   () = barrier (Barrier_RISCV_r_r ())
-let MEM_fence_rw_w  () = barrier (Barrier_RISCV_rw_w ())
-let MEM_fence_w_w   () = barrier (Barrier_RISCV_w_w ())
-let MEM_fence_w_rw  () = barrier (Barrier_RISCV_w_rw ())
-let MEM_fence_rw_r  () = barrier (Barrier_RISCV_rw_r ())
-let MEM_fence_r_w   () = barrier (Barrier_RISCV_r_w ())
-let MEM_fence_w_r   () = barrier (Barrier_RISCV_w_r ())
-let MEM_fence_tso   () = barrier (Barrier_RISCV_tso ())
-let MEM_fence_i     () = barrier (Barrier_RISCV_i ())
-
-val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_strong_release             : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional_release        : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-
-let MEMea addr size                      = write_mem_ea Write_plain () addr size
-let MEMea_release addr size              = write_mem_ea Write_RISCV_release () addr size
-let MEMea_strong_release addr size       = write_mem_ea Write_RISCV_strong_release () addr size
-let MEMea_conditional addr size          = write_mem_ea Write_RISCV_conditional () addr size
-let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_release () addr size
-let MEMea_conditional_strong_release addr size
-                                          = write_mem_ea Write_RISCV_conditional_strong_release () addr size
-
-val MEMr                         : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_acquire                 : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_strong_acquire          : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved_acquire        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-
-let MEMr addrsize size hexRAM addr                         = read_mem Read_plain addrsize addr size
-let MEMr_acquire addrsize size hexRAM addr                 = read_mem Read_RISCV_acquire addrsize addr size
-let MEMr_strong_acquire addrsize size hexRAM addr          = read_mem Read_RISCV_strong_acquire addrsize addr size
-let MEMr_reserved addrsize size hexRAM addr                = read_mem Read_RISCV_reserved addrsize addr size
-let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV_reserved_acquire addrsize addr size
-let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addrsize addr size
-
-val MEMw                            : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_release                    : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_strong_release             : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_conditional                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_conditional_release        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-
-let MEMw addrsize size hexRAM addr                            = write_mem Write_plain addrsize addr size
-let MEMw_release addrsize size hexRAM addr                    = write_mem Write_RISCV_release addrsize addr size
-let MEMw_strong_release addrsize size hexRAM addr             = write_mem Write_RISCV_strong_release addrsize addr size
-let MEMw_conditional addrsize size hexRAM addr                = write_mem Write_RISCV_conditional addrsize addr size
-let MEMw_conditional_release addrsize size hexRAM addr        = write_mem Write_RISCV_conditional_release addrsize addr size
-let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addrsize addr size
-
-val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
-let load_reservation addr = ()
-
-let speculate_conditional_success () = excl_result ()
-
-let match_reservation _ = true
-let cancel_reservation () = ()
-
-val sys_enable_writable_misa : unit -> bool
-let sys_enable_writable_misa () = true
-declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa`
-
-val sys_enable_rvc : unit -> bool
-let sys_enable_rvc () = true
-declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
-
-val sys_enable_next : unit -> bool
-let sys_enable_next () = true
-declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
-
-val sys_enable_fdext : unit -> bool
-let sys_enable_fdext () = true
-declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`
-
-val sys_enable_zfinx : unit -> bool
-let sys_enable_zfinx () = false
-declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
-
-val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_ram_base () = wordFromInteger 0
-declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
-
-val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_ram_size () = wordFromInteger 0
-declare ocaml target_rep function plat_ram_size = `Platform.dram_size`
-
-val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_rom_base () = wordFromInteger 0
-declare ocaml target_rep function plat_rom_base = `Platform.rom_base`
-
-val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_rom_size () = wordFromInteger 0
-declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
-
-val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_clint_base () = wordFromInteger 0
-declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
-
-val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_clint_size () = wordFromInteger 0
-declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
-
-val plat_enable_dirty_update : unit -> bool
-let plat_enable_dirty_update () = false
-declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`
-
-val plat_enable_misaligned_access : unit -> bool
-let plat_enable_misaligned_access () = false
-declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
-
-val plat_enable_pmp : unit -> bool
-let plat_enable_pmp () = false
-declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp`
-
-val plat_mtval_has_illegal_inst_bits : unit -> bool
-let plat_mtval_has_illegal_inst_bits () = false
-declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
-
-val plat_insns_per_tick : unit -> integer
-let plat_insns_per_tick () = 1
-declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
-
-val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_htif_tohost () = wordFromInteger 0
-declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost`
-
-val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit
-let plat_term_write _ = ()
-declare ocaml target_rep function plat_term_write = `Platform.term_write`
-
-val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_term_read () = wordFromInteger 0
-declare ocaml target_rep function plat_term_read = `Platform.term_read`
-
-val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_get_16_random_bits () = wordFromInteger 0
-declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits`
-
-val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_right v m = shiftr v (uint m)
-val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_left v m = shiftl v (uint m)
-
-val print_string : string -> string -> unit
-let print_string msg s = () (* print_endline (msg ^ s) *)
-
-val prerr_string : string -> string -> unit
-let prerr_string msg s = prerr_endline (msg ^ s)
-
-val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
-
-val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
-
-val print_dbg : string -> unit
-let print_dbg msg = ()
diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem
deleted file mode 100644
index e24a63d6a..000000000
--- a/handwritten_support/0.11/riscv_extras_fdext.lem
+++ /dev/null
@@ -1,216 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail2_instr_kinds
-open import Sail2_values
-open import Sail2_operators_mwords
-open import Sail2_prompt_monad
-open import Sail2_prompt
-
-type bitvector 'a = mword 'a
-
-(* stub functions emulating the C softfloat interface *)
-
-val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f16_add _ _ _ = ()
-
-val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f16_sub _ _ _ = ()
-
-val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f16_mul _ _ _ = ()
-
-val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f16_div _ _ _ = ()
-
-val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f32_add _ _ _ = ()
-
-val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f32_sub _ _ _ = ()
-
-val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f32_mul _ _ _ = ()
-
-val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f32_div _ _ _ = ()
-
-val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f64_add _ _ _ = ()
-
-val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f64_sub _ _ _ = ()
-
-val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f64_mul _ _ _ = ()
-
-val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
-let softfloat_f64_div _ _ _ = ()
-
-
-val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
-let softfloat_f16_muladd _ _ _ _ = ()
-
-val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
-let softfloat_f32_muladd _ _ _ _ = ()
-
-val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
-let softfloat_f64_muladd _ _ _ _ = ()
-
-
-val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f16_sqrt _ _ = ()
-
-val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f32_sqrt _ _ = ()
-
-val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f64_sqrt _ _ = ()
-
-
-val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f16_to_i32 _ _ = ()
-
-val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f16_to_ui32 _ _ = ()
-
-val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_i32_to_f16 _ _ = ()
-
-val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_ui32_to_f16 _ _ = ()
-
-val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f16_to_i64 _ _ = ()
-
-val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f16_to_ui64 _ _ = ()
-
-val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_i64_to_f16 _ _ = ()
-
-val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_ui64_to_f16 _ _ = ()
-
-
-val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f32_to_i32 _ _ = ()
-
-val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f32_to_ui32 _ _ = ()
-
-val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_i32_to_f32 _ _ = ()
-
-val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_ui32_to_f32 _ _ = ()
-
-val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f32_to_i64 _ _ = ()
-
-val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f32_to_ui64 _ _ = ()
-
-val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_i64_to_f32 _ _ = ()
-
-val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_ui64_to_f32 _ _ = ()
-
-
-val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f64_to_i32 _ _ = ()
-
-val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f64_to_ui32 _ _ = ()
-
-val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_i32_to_f64 _ _ = ()
-
-val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_ui32_to_f64 _ _ = ()
-
-val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f64_to_i64 _ _ = ()
-
-val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f64_to_ui64 _ _ = ()
-
-val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_i64_to_f64 _ _ = ()
-
-val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_ui64_to_f64 _ _ = ()
-
-
-val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f16_to_f32 _ _ = ()
-
-val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f16_to_f64 _ _ = ()
-
-val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f32_to_f64 _ _ = ()
-
-val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f32_to_f16 _ _ = ()
-
-val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f64_to_f16 _ _ = ()
-
-val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
-let softfloat_f64_to_f32 _ _ = ()
-
-
-val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f16_lt _ _ = ()
-
-val softfloat_f16_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f16_lt_quiet _ _ = ()
-
-val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f16_le _ _ = ()
-
-val softfloat_f16_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f16_le_quiet _ _ = ()
-
-val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f16_eq _ _ = ()
-
-val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f32_lt _ _ = ()
-
-val softfloat_f32_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f32_lt_quiet _ _ = ()
-
-val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f32_le _ _ = ()
-
-val softfloat_f32_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f32_le_quiet _ _ = ()
-
-val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f32_eq _ _ = ()
-
-val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f64_lt _ _ = ()
-
-val softfloat_f64_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f64_lt_quiet _ _ = ()
-
-val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f64_le _ _ = ()
-
-val softfloat_f64_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f64_le_quiet _ _ = ()
-
-val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
-let softfloat_f64_eq _ _ = ()
-
-val softfloat_f16_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit
-let softfloat_f16_round_to_int _ _ _ = ()
-
-val softfloat_f32_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit
-let softfloat_f32_round_to_int _ _ _ = ()
-
-val softfloat_f64_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit
-let softfloat_f64_round_to_int _ _ _ = ()
diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem
deleted file mode 100644
index 0c236515f..000000000
--- a/handwritten_support/0.11/riscv_extras_sequential.lem
+++ /dev/null
@@ -1,160 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail2_instr_kinds
-open import Sail2_values
-open import Sail2_operators_mwords
-open import Sail2_prompt_monad
-open import Sail2_prompt
-
-type bitvector 'a = mword 'a
-
-let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ())
-let MEM_fence_r_rw  () = barrier (Barrier_RISCV_r_rw ())
-let MEM_fence_r_r   () = barrier (Barrier_RISCV_r_r ())
-let MEM_fence_rw_w  () = barrier (Barrier_RISCV_rw_w ())
-let MEM_fence_w_w   () = barrier (Barrier_RISCV_w_w ())
-let MEM_fence_w_rw  () = barrier (Barrier_RISCV_w_rw ())
-let MEM_fence_rw_r  () = barrier (Barrier_RISCV_rw_r ())
-let MEM_fence_r_w   () = barrier (Barrier_RISCV_r_w ())
-let MEM_fence_w_r   () = barrier (Barrier_RISCV_w_r ())
-let MEM_fence_tso   () = barrier (Barrier_RISCV_tso ())
-let MEM_fence_i     () = barrier (Barrier_RISCV_i ())
-
-val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_strong_release             : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional_release        : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-
-let MEMea addr size                      = write_mem_ea Write_plain addr size
-let MEMea_release addr size              = write_mem_ea Write_RISCV_release addr size
-let MEMea_strong_release addr size       = write_mem_ea Write_RISCV_strong_release addr size
-let MEMea_conditional addr size          = write_mem_ea Write_RISCV_conditional addr size
-let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_release addr size
-let MEMea_conditional_strong_release addr size
-                                          = write_mem_ea Write_RISCV_conditional_strong_release addr size
-
-val MEMr                         : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_acquire                 : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_strong_acquire          : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved_acquire        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-
-let MEMr addrsize size hexRAM addr                         = read_mem Read_plain addr size
-let MEMr_acquire addrsize size hexRAM addr                 = read_mem Read_RISCV_acquire addr size
-let MEMr_strong_acquire addrsize size hexRAM addr          = read_mem Read_RISCV_strong_acquire addr size
-let MEMr_reserved addrsize size hexRAM addr                = read_mem Read_RISCV_reserved addr size
-let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV_reserved_acquire addr size
-let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size
-
-val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-let write_ram addrsize size hexRAM address value =
-  write_mem Write_plain address size value
-
-val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-let read_ram addrsize size hexRAM address =
-  read_mem Read_plain address size
-
-val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
-let load_reservation addr = ()
-
-let speculate_conditional_success () = excl_result ()
-
-let match_reservation _ = true
-let cancel_reservation () = ()
-
-val sys_enable_writable_misa : unit -> bool
-let sys_enable_writable_misa () = true
-declare ocaml target_rep function sys_enable_writable_misa = `Platform.enable_writable_misa`
-
-val sys_enable_rvc : unit -> bool
-let sys_enable_rvc () = true
-declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
-
-val sys_enable_zfinx : unit -> bool
-let sys_enable_zfinx () = false
-declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
-
-val sys_enable_next : unit -> bool
-let sys_enable_next () = true
-declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
-
-val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_ram_base () = wordFromInteger 0
-declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
-
-val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_ram_size () = wordFromInteger 0
-declare ocaml target_rep function plat_ram_size = `Platform.dram_size`
-
-val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_rom_base () = wordFromInteger 0
-declare ocaml target_rep function plat_rom_base = `Platform.rom_base`
-
-val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_rom_size () = wordFromInteger 0
-declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
-
-val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_clint_base () = wordFromInteger 0
-declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
-
-val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_clint_size () = wordFromInteger 0
-declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
-
-val plat_enable_dirty_update : unit -> bool
-let plat_enable_dirty_update () = false
-declare ocaml target_rep function plat_enable_dirty_update = `Platform.enable_dirty_update`
-
-val plat_enable_misaligned_access : unit -> bool
-let plat_enable_misaligned_access () = false
-declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
-
-val plat_enable_pmp : unit -> bool
-let plat_enable_pmp () = false
-declare ocaml target_rep function plat_enable_pmp = `Platform.enable_pmp`
-
-val plat_mtval_has_illegal_inst_bits : unit -> bool
-let plat_mtval_has_illegal_inst_bits () = false
-declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
-
-val plat_insns_per_tick : unit -> integer
-let plat_insns_per_tick () = 1
-declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
-
-val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_htif_tohost () = wordFromInteger 0
-declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost`
-
-val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit
-let plat_term_write _ = ()
-declare ocaml target_rep function plat_term_write = `Platform.term_write`
-
-val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_term_read () = wordFromInteger 0
-declare ocaml target_rep function plat_term_read = `Platform.term_read`
-
-val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_right v m = shiftr v (uint m)
-val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_left v m = shiftl v (uint m)
-
-val print_string : string -> string -> unit
-let print_string msg s = () (* print_endline (msg ^ s) *)
-
-val prerr_string : string -> string -> unit
-let prerr_string msg s = prerr_endline (msg ^ s)
-
-val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
-
-val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
-
-val print_dbg : string -> unit
-let print_dbg msg = ()
diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem
index eadcadad6..6ea76911a 100644
--- a/handwritten_support/mem_metadata.lem
+++ b/handwritten_support/mem_metadata.lem
@@ -72,15 +72,15 @@ open import Pervasives
 open import Pervasives_extra
 open import Sail2_instr_kinds
 open import Sail2_values
-open import Sail2_operators_mwords
+open import Sail2_operators_bitlists
 open import Sail2_prompt_monad
 open import Sail2_prompt
 
-val write_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => write_kind -> mword 'a -> integer -> mword 'n -> unit -> monad 'rv bool 'e
+val write_ram : forall 'rv 'e. write_kind -> list bitU -> integer -> list bitU -> unit -> monad 'rv bool 'e
 let write_ram wk addr width data meta =
   write_mem wk () addr width data
 
-val read_ram : forall 'rv 'e 'a 'n. Size 'a, Size 'n => read_kind -> mword 'a -> integer -> bool -> monad 'rv (mword 'n * unit) 'e
+val read_ram : forall 'rv 'e. read_kind -> list bitU -> integer -> bool -> monad 'rv (list bitU * unit) 'e
 let read_ram rk addr width read_tag =
-  read_mem rk () addr width >>= (fun (data : mword 'n) ->
+  read_mem rk () addr width >>= (fun data ->
   return (data, ()))
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index 5f92ee904..bc04c2df5 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -72,30 +72,30 @@ open import Pervasives
 open import Pervasives_extra
 open import Sail2_instr_kinds
 open import Sail2_values
-open import Sail2_operators_mwords
+open import Sail2_operators_bitlists
 open import Sail2_prompt_monad
 open import Sail2_prompt
 
-type bitvector 'a = mword 'a
-
-let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
-let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
-let MEM_fence_r_r   () = barrier Barrier_RISCV_r_r
-let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
-let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
-let MEM_fence_w_rw  () = barrier Barrier_RISCV_w_rw
-let MEM_fence_rw_r  () = barrier Barrier_RISCV_rw_r
-let MEM_fence_r_w   () = barrier Barrier_RISCV_r_w
-let MEM_fence_w_r   () = barrier Barrier_RISCV_w_r
-let MEM_fence_tso   () = barrier Barrier_RISCV_tso
-let MEM_fence_i     () = barrier Barrier_RISCV_i
-
-val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_strong_release             : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional_release        : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
-val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+type bitvector = list Sail2_values.bitU
+
+let MEM_fence_rw_rw () = barrier (Barrier_RISCV_rw_rw ())
+let MEM_fence_r_rw  () = barrier (Barrier_RISCV_r_rw ())
+let MEM_fence_r_r   () = barrier (Barrier_RISCV_r_r ())
+let MEM_fence_rw_w  () = barrier (Barrier_RISCV_rw_w ())
+let MEM_fence_w_w   () = barrier (Barrier_RISCV_w_w ())
+let MEM_fence_w_rw  () = barrier (Barrier_RISCV_w_rw ())
+let MEM_fence_rw_r  () = barrier (Barrier_RISCV_rw_r ())
+let MEM_fence_r_w   () = barrier (Barrier_RISCV_r_w ())
+let MEM_fence_w_r   () = barrier (Barrier_RISCV_w_r ())
+let MEM_fence_tso   () = barrier (Barrier_RISCV_tso ())
+let MEM_fence_i     () = barrier (Barrier_RISCV_i ())
+
+val MEMea                            : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e
+val MEMea_release                    : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e
+val MEMea_strong_release             : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e
+val MEMea_conditional                : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e
+val MEMea_conditional_release        : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e
+val MEMea_conditional_strong_release : forall 'rv 'e. bitvector -> integer -> monad 'rv unit 'e
 
 let MEMea addr size                      = write_mem_ea Write_plain () addr size
 let MEMea_release addr size              = write_mem_ea Write_RISCV_release () addr size
@@ -103,14 +103,14 @@ let MEMea_strong_release addr size       = write_mem_ea Write_RISCV_strong_relea
 let MEMea_conditional addr size          = write_mem_ea Write_RISCV_conditional () addr size
 let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_release () addr size
 let MEMea_conditional_strong_release addr size
-                                          = write_mem_ea Write_RISCV_conditional_strong_release () addr size
+                                         = write_mem_ea Write_RISCV_conditional_strong_release () addr size
 
-val MEMr                         : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_acquire                 : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_strong_acquire          : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved_acquire        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
-val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
+val MEMr                         : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e
+val MEMr_acquire                 : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e
+val MEMr_strong_acquire          : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e
+val MEMr_reserved                : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e
+val MEMr_reserved_acquire        : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e
+val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> monad 'rv bitvector 'e
 
 let MEMr addrsize size hexRAM addr                         = read_mem Read_plain addrsize addr size
 let MEMr_acquire addrsize size hexRAM addr                 = read_mem Read_RISCV_acquire addrsize addr size
@@ -119,12 +119,12 @@ let MEMr_reserved addrsize size hexRAM addr                = read_mem Read_RISCV
 let MEMr_reserved_acquire addrsize size hexRAM addr        = read_mem Read_RISCV_reserved_acquire addrsize addr size
 let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addrsize addr size
 
-val MEMw                            : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_release                    : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_strong_release             : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_conditional                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_conditional_release        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
-val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e
+val MEMw                            : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e
+val MEMw_release                    : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e
+val MEMw_strong_release             : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e
+val MEMw_conditional                : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e
+val MEMw_conditional_release        : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e
+val MEMw_conditional_strong_release : forall 'rv 'a 'b 'e. integer -> integer -> bitvector -> bitvector -> bitvector -> monad 'rv bool 'e
 
 let MEMw addrsize size hexRAM addr                            = write_mem Write_plain addrsize addr size
 let MEMw_release addrsize size hexRAM addr                    = write_mem Write_RISCV_release addrsize addr size
@@ -133,7 +133,7 @@ let MEMw_conditional addrsize size hexRAM addr                = write_mem Write_
 let MEMw_conditional_release addrsize size hexRAM addr        = write_mem Write_RISCV_conditional_release addrsize addr size
 let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addrsize addr size
 
-val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
+val load_reservation : bitvector -> unit
 let load_reservation addr = ()
 
 let speculate_conditional_success () = excl_result ()
@@ -161,32 +161,36 @@ val sys_enable_zfinx : unit -> bool
 let sys_enable_zfinx () = false
 declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
 
+val sys_enable_vext : unit -> bool
+let sys_enable_vext () = true
+declare ocaml target_rep function sys_enable_vext = `Platform.enable_vext`
+
 val sys_enable_writable_fiom : unit -> bool
 let sys_enable_writable_fiom () = true
 declare ocaml target_rep function sys_enable_writable_fiom = `Platform.enable_writable_fiom`
 
-val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_ram_base () = wordFromInteger 0
+val plat_ram_base : unit -> bitvector
+let plat_ram_base () = []
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
 
-val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_ram_size () = wordFromInteger 0
+val plat_ram_size : unit -> bitvector
+let plat_ram_size () = []
 declare ocaml target_rep function plat_ram_size = `Platform.dram_size`
 
-val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_rom_base () = wordFromInteger 0
+val plat_rom_base : unit -> bitvector
+let plat_rom_base () = []
 declare ocaml target_rep function plat_rom_base = `Platform.rom_base`
 
-val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_rom_size () = wordFromInteger 0
+val plat_rom_size : unit -> bitvector
+let plat_rom_size () = []
 declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
 
-val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_clint_base () = wordFromInteger 0
+val plat_clint_base : unit -> bitvector
+let plat_clint_base () = []
 declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
 
-val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_clint_size () = wordFromInteger 0
+val plat_clint_size : unit -> bitvector
+let plat_clint_size () = []
 declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
 
 val plat_enable_dirty_update : unit -> bool
@@ -209,25 +213,25 @@ val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
 
-val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_htif_tohost () = wordFromInteger 0
+val plat_htif_tohost : unit -> bitvector
+let plat_htif_tohost () = []
 declare ocaml target_rep function plat_htif_tohost = `Platform.htif_tohost`
 
-val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit
+val plat_term_write : bitvector -> unit
 let plat_term_write _ = ()
 declare ocaml target_rep function plat_term_write = `Platform.term_write`
 
-val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_term_read () = wordFromInteger 0
+val plat_term_read : unit -> bitvector
+let plat_term_read () = []
 declare ocaml target_rep function plat_term_read = `Platform.term_read`
 
-val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a
-let plat_get_16_random_bits () = wordFromInteger 0
+val plat_get_16_random_bits : unit -> bitvector
+let plat_get_16_random_bits () = []
 declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits`
 
-val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
+val shift_bits_right : bitvector -> bitvector -> bitvector
 let shift_bits_right v m = shiftr v (uint m)
-val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
+val shift_bits_left : bitvector -> bitvector -> bitvector
 let shift_bits_left v m = shiftl v (uint m)
 
 val print_string : string -> string -> unit
@@ -236,11 +240,11 @@ let print_string msg s = () (* print_endline (msg ^ s) *)
 val prerr_string : string -> string -> unit
 let prerr_string msg s = prerr_endline (msg ^ s)
 
-val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
+val prerr_bits : string -> bitvector -> unit
 let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
 
-val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
+val print_bits : string -> bitvector -> unit
+let print_bits msg bs = print_endline (msg ^ (show_bitlist (bits_of bs)))
 
 val print_dbg : string -> unit
 let print_dbg msg = ()
diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem
index 84e76ee47..81c6af504 100644
--- a/handwritten_support/riscv_extras_fdext.lem
+++ b/handwritten_support/riscv_extras_fdext.lem
@@ -76,193 +76,211 @@ open import Sail2_operators_mwords
 open import Sail2_prompt_monad
 open import Sail2_prompt
 
-type bitvector 'a = mword 'a
+type bitvector = list Sail2_values.bitU
 
 (* stub functions emulating the C softfloat interface *)
 
-val softfloat_f16_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f16_round_to_int : bitvector -> bitvector -> bool -> unit
+let softfloat_f16_round_to_int _ _ _ = ()
+
+val softfloat_f32_round_to_int : bitvector -> bitvector -> bool -> unit
+let softfloat_f32_round_to_int _ _ _ = ()
+
+val softfloat_f64_round_to_int : bitvector -> bitvector -> bool -> unit
+let softfloat_f64_round_to_int _ _ _ = ()
+
+val softfloat_f16_add : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f16_add _ _ _ = ()
 
-val softfloat_f16_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f16_sub : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f16_sub _ _ _ = ()
 
-val softfloat_f16_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f16_mul : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f16_mul _ _ _ = ()
 
-val softfloat_f16_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f16_div : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f16_div _ _ _ = ()
 
-val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f32_add : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f32_add _ _ _ = ()
 
-val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f32_sub : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f32_sub _ _ _ = ()
 
-val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f32_mul : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f32_mul _ _ _ = ()
 
-val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f32_div : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f32_div _ _ _ = ()
 
-val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f64_add : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f64_add _ _ _ = ()
 
-val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f64_sub : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f64_sub _ _ _ = ()
 
-val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f64_mul : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f64_mul _ _ _ = ()
 
-val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+val softfloat_f64_div : bitvector -> bitvector -> bitvector -> unit
 let softfloat_f64_div _ _ _ = ()
 
 
-val softfloat_f16_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+val softfloat_f16_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
 let softfloat_f16_muladd _ _ _ _ = ()
 
-val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+val softfloat_f32_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
 let softfloat_f32_muladd _ _ _ _ = ()
 
-val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+val softfloat_f64_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit
 let softfloat_f64_muladd _ _ _ _ = ()
 
 
-val softfloat_f16_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f16_sqrt : bitvector -> bitvector -> unit
 let softfloat_f16_sqrt _ _ = ()
 
-val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f32_sqrt : bitvector -> bitvector -> unit
 let softfloat_f32_sqrt _ _ = ()
 
-val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f64_sqrt : bitvector -> bitvector -> unit
 let softfloat_f64_sqrt _ _ = ()
 
 
-val softfloat_f16_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f16_to_i32: bitvector -> bitvector -> unit
 let softfloat_f16_to_i32 _ _ = ()
 
-val softfloat_f16_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f16_to_ui32: bitvector -> bitvector -> unit
 let softfloat_f16_to_ui32 _ _ = ()
 
-val softfloat_i32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_i32_to_f16: bitvector -> bitvector -> unit
 let softfloat_i32_to_f16 _ _ = ()
 
-val softfloat_ui32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_ui32_to_f16: bitvector -> bitvector -> unit
 let softfloat_ui32_to_f16 _ _ = ()
 
-val softfloat_f16_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f16_to_i64: bitvector -> bitvector -> unit
 let softfloat_f16_to_i64 _ _ = ()
 
-val softfloat_f16_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f16_to_ui64: bitvector -> bitvector -> unit
 let softfloat_f16_to_ui64 _ _ = ()
 
-val softfloat_i64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_i64_to_f16: bitvector -> bitvector -> unit
 let softfloat_i64_to_f16 _ _ = ()
 
-val softfloat_ui64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_ui64_to_f16: bitvector -> bitvector -> unit
 let softfloat_ui64_to_f16 _ _ = ()
 
 
-val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f32_to_i32: bitvector -> bitvector -> unit
 let softfloat_f32_to_i32 _ _ = ()
 
-val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f32_to_ui32: bitvector -> bitvector -> unit
 let softfloat_f32_to_ui32 _ _ = ()
 
-val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_i32_to_f32: bitvector -> bitvector -> unit
 let softfloat_i32_to_f32 _ _ = ()
 
-val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_ui32_to_f32: bitvector -> bitvector -> unit
 let softfloat_ui32_to_f32 _ _ = ()
 
-val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f32_to_i64: bitvector -> bitvector -> unit
 let softfloat_f32_to_i64 _ _ = ()
 
-val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f32_to_ui64: bitvector -> bitvector -> unit
 let softfloat_f32_to_ui64 _ _ = ()
 
-val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_i64_to_f32: bitvector -> bitvector -> unit
 let softfloat_i64_to_f32 _ _ = ()
 
-val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_ui64_to_f32: bitvector -> bitvector -> unit
 let softfloat_ui64_to_f32 _ _ = ()
 
 
-val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f64_to_i32: bitvector -> bitvector -> unit
 let softfloat_f64_to_i32 _ _ = ()
 
-val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f64_to_ui32: bitvector -> bitvector -> unit
 let softfloat_f64_to_ui32 _ _ = ()
 
-val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_i32_to_f64: bitvector -> bitvector -> unit
 let softfloat_i32_to_f64 _ _ = ()
 
-val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_ui32_to_f64: bitvector -> bitvector -> unit
 let softfloat_ui32_to_f64 _ _ = ()
 
-val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f64_to_i64: bitvector -> bitvector -> unit
 let softfloat_f64_to_i64 _ _ = ()
 
-val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f64_to_ui64: bitvector -> bitvector -> unit
 let softfloat_f64_to_ui64 _ _ = ()
 
-val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_i64_to_f64: bitvector -> bitvector -> unit
 let softfloat_i64_to_f64 _ _ = ()
 
-val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_ui64_to_f64: bitvector -> bitvector -> unit
 let softfloat_ui64_to_f64 _ _ = ()
 
 
-val softfloat_f16_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f16_to_f32: bitvector -> bitvector -> unit
 let softfloat_f16_to_f32 _ _ = ()
 
-val softfloat_f16_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f16_to_f64: bitvector -> bitvector -> unit
 let softfloat_f16_to_f64 _ _ = ()
 
-val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f32_to_f64: bitvector -> bitvector -> unit
 let softfloat_f32_to_f64 _ _ = ()
 
-val softfloat_f32_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f32_to_f16: bitvector -> bitvector -> unit
 let softfloat_f32_to_f16 _ _ = ()
 
-val softfloat_f64_to_f16: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f64_to_f16: bitvector -> bitvector -> unit
 let softfloat_f64_to_f16 _ _ = ()
 
-val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+val softfloat_f64_to_f32: bitvector -> bitvector -> unit
 let softfloat_f64_to_f32 _ _ = ()
 
 
-val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f16_lt : bitvector -> bitvector -> unit
 let softfloat_f16_lt _ _ = ()
 
-val softfloat_f16_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f16_lt_quiet : bitvector -> bitvector -> unit
 let softfloat_f16_lt_quiet _ _ = ()
 
-val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f16_le : bitvector -> bitvector -> unit
 let softfloat_f16_le _ _ = ()
 
-val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f16_le_quiet : bitvector -> bitvector -> unit
+let softfloat_f16_le_quiet _ _ = ()
+
+val softfloat_f16_eq : bitvector -> bitvector -> unit
 let softfloat_f16_eq _ _ = ()
 
-val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f32_lt : bitvector -> bitvector -> unit
 let softfloat_f32_lt _ _ = ()
 
-val softfloat_f32_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f32_lt_quiet : bitvector -> bitvector -> unit
 let softfloat_f32_lt_quiet _ _ = ()
 
-val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f32_le : bitvector -> bitvector -> unit
 let softfloat_f32_le _ _ = ()
 
-val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f32_le_quiet : bitvector -> bitvector -> unit
+let softfloat_f32_le_quiet _ _ = ()
+
+val softfloat_f32_eq : bitvector -> bitvector -> unit
 let softfloat_f32_eq _ _ = ()
 
-val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f64_lt : bitvector -> bitvector -> unit
 let softfloat_f64_lt _ _ = ()
 
-val softfloat_f64_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f64_lt_quiet : bitvector -> bitvector -> unit
 let softfloat_f64_lt_quiet _ _ = ()
 
-val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f64_le : bitvector -> bitvector -> unit
 let softfloat_f64_le _ _ = ()
 
-val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+val softfloat_f64_le_quiet : bitvector -> bitvector -> unit
+let softfloat_f64_le_quiet _ _ = ()
+
+val softfloat_f64_eq : bitvector -> bitvector -> unit
 let softfloat_f64_eq _ _ = ()