lem: Fix issues created by vector extension

Switch to bitlist representation because the machine words
can't handle the vector code currently

Remove RMEM target from default set of targets in Makefile.
This is only interesting for RMEM maintainers. There's no reason for it
to be generated by default, and it's also broken.

While we are hacking on these files purge the duplicate versions for Sail 0.11+

8 files changed, 149 insertions, 699 deletions

diff --git a/Makefile b/Makefile
index 9f284ca..923c6a3 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 8a8c070..0000000
--- 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 2509057..0000000
--- 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 e24a63d..0000000
--- 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 0c23651..0000000
--- 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 eadcada..6ea7691 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 5f92ee9..bc04c2d 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 84e76ee..81c6af5 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 _ _ = ()