Initial; working SAIL RISC-V regs

The register definition along with read/write functions for registers
are lowered to Coq. The FIRRTL annotation does not work as expected.

41 files changed, 3438 insertions, 0 deletions

diff --git a/handwritten_support/.mem_metadata.aux b/handwritten_support/.mem_metadata.aux
new file mode 100644
index 0000000..cfce1c3
--- /dev/null
+++ b/handwritten_support/.mem_metadata.aux
@@ -0,0 +1,3 @@
+COQAUX1 693b57d74f776ae8bd215fbfc8b03df3 /home/aditya/dev/firrtl-proof/sail-riscv/handwritten_support/mem_metadata.v
+183 386 context_used ""
+0 0 vo_compile_time "0.304"
diff --git a/handwritten_support/.riscv_extras.aux b/handwritten_support/.riscv_extras.aux
new file mode 100644
index 0000000..d53d7e5
--- /dev/null
+++ b/handwritten_support/.riscv_extras.aux
@@ -0,0 +1,23 @@
+COQAUX1 9f6e940694efb436e57a7a26d0b1b3b3 /home/aditya/dev/firrtl-proof/sail-riscv/handwritten_support/riscv_extras.v
+3801 3993 context_used ""
+3994 4194 context_used ""
+4195 4402 context_used ""
+4403 4604 context_used ""
+4605 4814 context_used ""
+4815 5031 context_used ""
+7223 7331 context_used ""
+7333 7442 context_used ""
+7444 7565 context_used ""
+8744 8878 context_used ""
+9948 9983 context_used ""
+10049 10053 proof_build_time "0.017"
+0 0 euclid_modulo "0.017"
+10005 10048 context_used ""
+10049 10053 proof_check_time "0.004"
+10096 10182 context_used ""
+10183 10267 context_used ""
+11004 11008 proof_build_time "0.001"
+0 0 n_leading_spaces_fact "0.001"
+10997 11003 context_used ""
+11004 11008 proof_check_time "0.001"
+0 0 vo_compile_time "0.514"
diff --git a/handwritten_support/0.11/mem_metadata.lem b/handwritten_support/0.11/mem_metadata.lem
new file mode 100644
index 0000000..8a8c070
--- /dev/null
+++ b/handwritten_support/0.11/mem_metadata.lem
@@ -0,0 +1,16 @@
+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
new file mode 100644
index 0000000..db93001
--- /dev/null
+++ b/handwritten_support/0.11/riscv_extras.lem
@@ -0,0 +1,164 @@
+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 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/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem
new file mode 100644
index 0000000..12cfe00
--- /dev/null
+++ b/handwritten_support/0.11/riscv_extras_fdext.lem
@@ -0,0 +1,125 @@
+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_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_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_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_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_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f64 _ _ = ()
+
+val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f32 _ _ = ()
+
+
+val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_lt _ _ = ()
+
+val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_le _ _ = ()
+
+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_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_le _ _ = ()
+
+val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_eq _ _ = ()
diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem
new file mode 100644
index 0000000..827f601
--- /dev/null
+++ b/handwritten_support/0.11/riscv_extras_sequential.lem
@@ -0,0 +1,156 @@
+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_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/Holmakefile b/handwritten_support/Holmakefile
new file mode 100644
index 0000000..dd483e9
--- /dev/null
+++ b/handwritten_support/Holmakefile
@@ -0,0 +1,13 @@
+INCLUDES = $(LEM_DIR)/hol-lib $(SAIL_LIB_DIR)/hol
+
+SCRIPTS = riscv_extrasScript.sml  riscv_typesScript.sml  riscvScript.sml
+
+THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))
+
+all: $(THYS)
+.PHONY: all
+
+ifdef POLY
+BASE_HEAP = $(SAIL_LIB_DIR)/hol/sail-heap
+
+endif
diff --git a/handwritten_support/ROOT b/handwritten_support/ROOT
new file mode 100644
index 0000000..281bd26
--- /dev/null
+++ b/handwritten_support/ROOT
@@ -0,0 +1,9 @@
+session "Sail-RISC-V" = "Sail" +
+  options [document = false]
+  theories
+    "Riscv_lemmas"
+
+session "Sail-RISC-V-Duopod" = "Sail" +
+  options [document = false]
+  theories
+    "Riscv_duopod_lemmas"
diff --git a/handwritten_support/hgen/ast.hgen b/handwritten_support/hgen/ast.hgen
new file mode 100644
index 0000000..25d19a4
--- /dev/null
+++ b/handwritten_support/hgen/ast.hgen
@@ -0,0 +1,22 @@
+| `RISCVStopFetching (* this is a special instruction used by rmem to
+                        indicate the end of a litmus thread *)
+| `RISCVThreadStart  (* this instruction indicates a thread creation in ELF files *)
+
+| `RISCVUTYPE of bit20 * reg * riscvUop
+| `RISCVJAL   of bit20 * reg
+| `RISCVJALR  of bit12 * reg * reg
+| `RISCVBType of bit12 * reg * reg * riscvBop
+| `RISCVIType of bit12 * reg * reg * riscvIop
+| `RISCVShiftIop of bit6 * reg * reg * riscvSop
+| `RISCVRType of reg * reg * reg * riscvRop
+| `RISCVLoad of bit12 * reg * reg * bool * wordWidth * bool * bool
+| `RISCVStore of bit12 * reg * reg * wordWidth * bool * bool
+| `RISCVADDIW of bit12 * reg * reg
+| `RISCVSHIFTW of bit5 * reg * reg * riscvSop
+| `RISCVRTYPEW of reg * reg * reg * riscvRopw
+| `RISCVFENCE of bit4 * bit4
+| `RISCVFENCE_TSO of bit4 * bit4
+| `RISCVFENCEI
+| `RISCVLoadRes of bool * bool * reg * wordWidth * reg
+| `RISCVStoreCon of bool * bool * reg * reg * wordWidth * reg
+| `RISCVAMO of riscvAmoop * bool * bool * reg * reg * wordWidth * reg
diff --git a/handwritten_support/hgen/fold.hgen b/handwritten_support/hgen/fold.hgen
new file mode 100644
index 0000000..7f9d05c
--- /dev/null
+++ b/handwritten_support/hgen/fold.hgen
@@ -0,0 +1,21 @@
+| `RISCVThreadStart                      -> (y_reg, y_sreg)
+| `RISCVStopFetching                     -> (y_reg, y_sreg)
+
+| `RISCVUTYPE (_, r0, _)                 -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJAL (_, r0)                      -> fold_reg r0 (y_reg, y_sreg)
+| `RISCVJALR (_, r0, r1)                 -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVBType (_, r0, r1, _)             -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVIType (_, r0, r1, _)             -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVShiftIop (_, r0, r1, _)          -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRType (r0, r1, r2, _)            -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
+| `RISCVLoad (_, r0, r1, _, _, _, _)     -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVStore (_, r0, r1, _, _, _)       -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVADDIW (_, r0, r1)                -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVSHIFTW (_, r0, r1, _)            -> fold_reg r0 (fold_reg r1 (y_reg, y_sreg))
+| `RISCVRTYPEW (r0, r1, r2, _)           -> fold_reg r0 (fold_reg r1 (fold_reg r2 (y_reg, y_sreg)))
+| `RISCVFENCE (_, _)                     -> (y_reg, y_sreg)
+| `RISCVFENCE_TSO (_, _)                 -> (y_reg, y_sreg)
+| `RISCVFENCEI                           -> (y_reg, y_sreg)
+| `RISCVLoadRes (_, _, rs1, _, rd)       -> fold_reg rs1 (fold_reg rd (y_reg, y_sreg))
+| `RISCVStoreCon (_, _, rs2, rs1, _, rd) -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
+| `RISCVAMO (_, _, _, rs2, rs1, _, rd)   -> fold_reg rs2 (fold_reg rs1 (fold_reg rd (y_reg, y_sreg)))
diff --git a/handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen b/handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen
new file mode 100644
index 0000000..2ebef02
--- /dev/null
+++ b/handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen
@@ -0,0 +1,91 @@
+| `RISCVThreadStart  -> THREAD_START()
+| `RISCVStopFetching -> STOP_FETCHING()
+
+| `RISCVUTYPE(imm, rd, op) -> UTYPE(
+      translate_imm20 "imm" imm,
+      translate_reg "rd" rd,
+      translate_uop op)
+| `RISCVJAL(imm, rd) -> RISCV_JAL(
+      translate_imm21 "imm" imm,
+      translate_reg "rd" rd)
+| `RISCVJALR(imm, rs, rd) -> RISCV_JALR(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rd,
+      translate_reg "rd" rd)
+| `RISCVBType(imm, rs2, rs1, op) -> BTYPE(
+      translate_imm13 "imm" imm,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_bop op)
+| `RISCVIType(imm, rs1, rd, op) -> ITYPE(
+      translate_imm12 "imm" imm,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_iop op)
+| `RISCVShiftIop(imm, rs, rd, op) -> SHIFTIOP(
+      translate_imm6 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_sop op)
+| `RISCVRType (rs2, rs1, rd, op) -> RTYPE (
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_rop op)
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) -> LOAD(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_bool "unsigned" unsigned,
+      translate_wordWidth width,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl)
+| `RISCVStore(imm, rs, rd, width, aq, rl) -> STORE (
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_wordWidth width,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl)
+| `RISCVADDIW(imm, rs, rd) -> ADDIW(
+      translate_imm12 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd)
+| `RISCVSHIFTW(imm, rs, rd, op) -> SHIFTW(
+      translate_imm5 "imm" imm,
+      translate_reg "rs" rs,
+      translate_reg "rd" rd,
+      translate_sop op)
+| `RISCVRTYPEW(rs2, rs1, rd, op) -> RTYPEW(
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_reg "rd" rd,
+      translate_ropw op)
+| `RISCVFENCE(pred, succ) -> FENCE(
+      translate_imm4 "pred" pred,
+      translate_imm4 "succ" succ)
+| `RISCVFENCE_TSO(pred, succ) -> FENCE_TSO(
+      translate_imm4 "pred" pred,
+      translate_imm4 "succ" succ)
+| `RISCVFENCEI -> FENCEI ()
+| `RISCVLoadRes(aq, rl, rs1, width, rd) -> LOADRES(
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) -> STORECON(
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
+| `RISCVAMO (op, aq, rl, rs2, rs1, width, rd) -> AMO(
+      translate_amoop op,
+      translate_bool "aq" aq,
+      translate_bool "rl" rl,
+      translate_reg "rs2" rs2,
+      translate_reg "rs1" rs1,
+      translate_wordWidth width,
+      translate_reg "rd" rd)
diff --git a/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen b/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen
new file mode 100644
index 0000000..8bd311b
--- /dev/null
+++ b/handwritten_support/hgen/herdtools_types_to_shallow_types.hgen
@@ -0,0 +1,90 @@
+let is_inc = false
+
+let translate_reg name value =
+    Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int (reg_to_int value))
+
+let translate_uop op = match op with
+  | RISCVLUI   -> RISCV_LUI
+  | RISCVAUIPC -> RISCV_AUIPC
+
+let translate_bop op = match op with
+  | RISCVBEQ  -> RISCV_BEQ
+  | RISCVBNE  -> RISCV_BNE
+  | RISCVBLT  -> RISCV_BLT
+  | RISCVBGE  -> RISCV_BGE
+  | RISCVBLTU -> RISCV_BLTU
+  | RISCVBGEU -> RISCV_BGEU
+
+let translate_iop op = match op with
+  | RISCVADDI  -> RISCV_ADDI
+  | RISCVSLTI  -> RISCV_SLTI
+  | RISCVSLTIU -> RISCV_SLTIU
+  | RISCVXORI  -> RISCV_XORI
+  | RISCVORI   -> RISCV_ORI
+  | RISCVANDI  -> RISCV_ANDI
+
+let translate_sop op = match op with
+  | RISCVSLLI -> RISCV_SLLI
+  | RISCVSRLI -> RISCV_SRLI
+  | RISCVSRAI -> RISCV_SRAI
+
+let translate_rop op = match op with
+  | RISCVADD  -> RISCV_ADD
+  | RISCVSUB  -> RISCV_SUB
+  | RISCVSLL  -> RISCV_SLL
+  | RISCVSLT  -> RISCV_SLT
+  | RISCVSLTU -> RISCV_SLTU
+  | RISCVXOR  -> RISCV_XOR
+  | RISCVSRL  -> RISCV_SRL
+  | RISCVSRA  -> RISCV_SRA
+  | RISCVOR   -> RISCV_OR
+  | RISCVAND  -> RISCV_AND
+
+let translate_ropw op = match op with
+  | RISCVADDW -> RISCV_ADDW
+  | RISCVSUBW -> RISCV_SUBW
+  | RISCVSLLW -> RISCV_SLLW
+  | RISCVSRLW -> RISCV_SRLW
+  | RISCVSRAW -> RISCV_SRAW
+
+let translate_amoop op = match op with
+  | RISCVAMOSWAP -> AMOSWAP
+  | RISCVAMOADD  -> AMOADD
+  | RISCVAMOXOR  -> AMOXOR
+  | RISCVAMOAND  -> AMOAND
+  | RISCVAMOOR   -> AMOOR
+  | RISCVAMOMIN  -> AMOMIN
+  | RISCVAMOMAX  -> AMOMAX
+  | RISCVAMOMINU -> AMOMINU
+  | RISCVAMOMAXU -> AMOMAXU
+
+let translate_wordWidth op = match op with
+  | RISCVBYTE   -> BYTE  
+  | RISCVHALF   -> HALF  
+  | RISCVWORD   -> WORD  
+  | RISCVDOUBLE -> DOUBLE
+
+let translate_bool name b = b (* function
+   * | true -> trueSail2_values.B10
+   * | false -> false Sail2_values.B00 *)
+
+let translate_imm21 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty21_dict (Nat_big_num.of_int value)
+  
+let translate_imm20 name value = 
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty20_dict (Nat_big_num.of_int value)
+  
+let translate_imm13 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty13_dict (Nat_big_num.of_int value)
+  
+let translate_imm12 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty12_dict (Nat_big_num.of_int value)
+  
+let translate_imm6 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty6_dict (Nat_big_num.of_int value)
+  
+let translate_imm5 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty5_dict (Nat_big_num.of_int value)
+  
+let translate_imm4 name value =
+  Lem_machine_word.wordFromInteger Lem_machine_word.instance_Machine_word_Size_Machine_word_ty4_dict (Nat_big_num.of_int value)
diff --git a/handwritten_support/hgen/lexer.hgen b/handwritten_support/hgen/lexer.hgen
new file mode 100644
index 0000000..9009f33
--- /dev/null
+++ b/handwritten_support/hgen/lexer.hgen
@@ -0,0 +1,63 @@
+(** RV32I (and RV64I) ***********************************************)
+"lui"   , UTYPE { op=RISCVLUI   };
+"auipc" , UTYPE { op=RISCVAUIPC };
+
+"jal",  JAL ();
+"jalr", JALR ();
+
+"beq",  BTYPE {op=RISCVBEQ};
+"bne",  BTYPE {op=RISCVBNE};
+"blt",  BTYPE {op=RISCVBLT};
+"bge",  BTYPE {op=RISCVBGE};
+"bltu", BTYPE {op=RISCVBLTU};
+"bgeu", BTYPE {op=RISCVBGEU};
+
+"addi",  ITYPE {op=RISCVADDI};
+"stli",  ITYPE {op=RISCVSLTI};
+"sltiu", ITYPE {op=RISCVSLTIU};
+"xori",  ITYPE {op=RISCVXORI};
+"ori",   ITYPE {op=RISCVORI};
+"andi",  ITYPE {op=RISCVANDI};
+
+"add",  RTYPE {op=RISCVADD};
+"sub",  RTYPE {op=RISCVSUB};
+"sll",  RTYPE {op=RISCVSLL};
+"slt",  RTYPE {op=RISCVSLT};
+"sltu", RTYPE {op=RISCVSLT};
+"xor",  RTYPE {op=RISCVXOR};
+"srl",  RTYPE {op=RISCVSRL};
+"sra",  RTYPE {op=RISCVSRA};
+"or",   RTYPE {op=RISCVOR};
+"and",  RTYPE {op=RISCVAND};
+
+"fence",     FENCE ();
+"fence.tso", FENCETSO ();
+"fence.i",   FENCEI ();
+
+(** RV64I (in addition to RV32I) ************************************)
+
+"addiw", ADDIW ();
+
+"addw", RTYPEW {op=RISCVADDW};
+"subw", RTYPEW {op=RISCVSUBW};
+"sllw", RTYPEW {op=RISCVSLLW};
+"srlw", RTYPEW {op=RISCVSRLW};
+"sraw", RTYPEW {op=RISCVSRAW};
+
+"slli", SHIFTIOP {op=RISCVSLLI};
+"srli", SHIFTIOP {op=RISCVSRLI};
+"srai", SHIFTIOP {op=RISCVSRAI};
+
+"slliw", SHIFTW {op=RISCVSLLI};
+"srliw", SHIFTW {op=RISCVSRLI};
+"sraiw", SHIFTW {op=RISCVSRAI};
+
+(** RV32A (and RV64A) ***********************************************)
+
+"r",  FENCEOPTION Fence_R;
+"w",  FENCEOPTION Fence_W;
+"rw", FENCEOPTION Fence_RW;
+
+(** pseudo instructions *********************************************)
+
+"li", LI ()
diff --git a/handwritten_support/hgen/lexer_regexps.hgen b/handwritten_support/hgen/lexer_regexps.hgen
new file mode 100644
index 0000000..b8f3ca6
--- /dev/null
+++ b/handwritten_support/hgen/lexer_regexps.hgen
@@ -0,0 +1,131 @@
+(** RV32I (and RV64I) ***********************************************)
+
+| 'l' (('b'|'h') as width) ("u"? as u) (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = (match width with 'b' -> RISCVBYTE | 'h' -> RISCVHALF | _ -> failwith "bad width");
+              unsigned = (u = "u");
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| "lw" (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = RISCVWORD;
+              unsigned = false;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| 's' (('b'|'h'|'w') as width) (".aq"? as aq) (".rl"? as rl) as store
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ store ^ "' is not a valid instruction") else
+      STORE { width    = (match width with 'b' -> RISCVBYTE | 'h' -> RISCVHALF | 'w' -> RISCVWORD | _ -> failwith "bad width");
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+(** RV64I (in addition to RV32I) ************************************)
+
+| "lwu" (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = RISCVWORD;
+              unsigned = true;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| "ld" (".aq"? as aq) (".rl"? as rl) as load
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ load ^ "' is not a valid instruction") else
+      LOAD  { width    = RISCVDOUBLE;
+              unsigned = false;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+| "sd" (".aq"? as aq) (".rl"? as rl) as store
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ store ^ "' is not a valid instruction") else
+      STORE { width    = RISCVDOUBLE;
+              aq       = (aq = ".aq");
+              rl       = (rl = ".rl");
+            }
+    }
+
+(** RV32A (and RV64A) ***********************************************)
+
+| "lr.w" (".aq"? as aq) (".rl"? as rl) as lr
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ lr ^ "' is not a valid instruction") else
+      LOADRES { width = RISCVWORD;
+                aq    = (aq = ".aq");
+                rl    = (rl = ".rl");
+              }
+    }
+
+| "sc.w" (".aq"? as aq) (".rl"? as rl) as sc
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ sc ^ "' is not a valid instruction") else
+      STORECON  { width = RISCVWORD;
+                  aq    = (aq = ".aq");
+                  rl    = (rl = ".rl");
+                }
+    }
+
+| "amo" (("swap"|"add"|"and"|"or"|"xor"|"max"|"min"|"maxu"|"minu") as op) ".w" (".aq"? as aq) (".rl"? as rl)
+    { AMO { op    =
+              begin match op with
+              | "swap" -> RISCVAMOSWAP;
+              | "add"  -> RISCVAMOADD;
+              | "and"  -> RISCVAMOAND;
+              | "or"   -> RISCVAMOOR;
+              | "xor"  -> RISCVAMOXOR;
+              | "max"  -> RISCVAMOMAX;
+              | "min"  -> RISCVAMOMIN;
+              | "maxu" -> RISCVAMOMAXU;
+              | "minu" -> RISCVAMOMINU;
+              | _ -> failwith "bad amo"
+              end;
+            width = RISCVWORD;
+            aq    = (aq = ".aq");
+            rl    = (rl = ".rl");
+          }
+    }
+
+(** RV64A (in addition to RV32A) ************************************)
+
+| "lr.d" (".aq"? as aq) (".rl"? as rl) as lr
+    { if (rl = ".rl") && not (aq = ".aq") then failwith ("'" ^ lr ^ "' is not a valid instruction") else
+      LOADRES { width = RISCVDOUBLE;
+                aq    = (aq = ".aq");
+                rl    = (rl = ".rl");
+              }
+    }
+
+| "sc.d" (".aq"? as aq) (".rl"? as rl) as sc
+    { if (aq = ".aq") && not (rl = ".rl") then failwith ("'" ^ sc ^ "' is not a valid instruction") else
+      STORECON  { width = RISCVDOUBLE;
+                  aq    = (aq = ".aq");
+                  rl    = (rl = ".rl");
+                }
+    }
+
+| "amo" (("swap"|"add"|"and"|"or"|"xor"|"max"|"min"|"maxu"|"minu") as op) ".d" (".aq"? as aq) (".rl"? as rl)
+    { AMO { op    =
+              begin match op with
+              | "swap" -> RISCVAMOSWAP;
+              | "add"  -> RISCVAMOADD;
+              | "and"  -> RISCVAMOAND;
+              | "or"   -> RISCVAMOOR;
+              | "xor"  -> RISCVAMOXOR;
+              | "max"  -> RISCVAMOMAX;
+              | "min"  -> RISCVAMOMIN;
+              | "maxu" -> RISCVAMOMAXU;
+              | "minu" -> RISCVAMOMINU;
+              | _ -> failwith "bad amo"
+              end;
+            width = RISCVDOUBLE;
+            aq    = (aq = ".aq");
+            rl    = (rl = ".rl");
+          }
+    }
diff --git a/handwritten_support/hgen/map.hgen b/handwritten_support/hgen/map.hgen
new file mode 100644
index 0000000..aa3882e
--- /dev/null
+++ b/handwritten_support/hgen/map.hgen
@@ -0,0 +1,21 @@
+| `RISCVThreadStart                        -> `RISCVThreadStart
+| `RISCVStopFetching                       -> `RISCVStopFetching
+
+| `RISCVUTYPE (x, r0, y)                   -> `RISCVUTYPE (x, map_reg r0, y)
+| `RISCVJAL (x, r0)                        -> `RISCVJAL (x, map_reg r0)
+| `RISCVJALR (x, r0, r1)                   -> `RISCVJALR (x, map_reg r0, map_reg r1)
+| `RISCVBType (x, r0, r1, y)               -> `RISCVBType (x, map_reg r0, map_reg r1, y)
+| `RISCVIType (x, r0, r1, y)               -> `RISCVIType (x, map_reg r0, map_reg r1, y)
+| `RISCVShiftIop (x, r0, r1, y)            -> `RISCVShiftIop (x, map_reg r0, map_reg r1, y)
+| `RISCVRType (r0, r1, r2, y)              -> `RISCVRType (r0, map_reg r1, map_reg r2, y)
+| `RISCVLoad (x, r0, r1, y, z, a, b)       -> `RISCVLoad (x, map_reg r0, map_reg r1, y, z, a, b)
+| `RISCVStore (x, r0, r1, y, z, a)         -> `RISCVStore (x, map_reg r0, map_reg r1, y, z, a)
+| `RISCVADDIW (x, r0, r1)                  -> `RISCVADDIW (x, map_reg r0, map_reg r1)
+| `RISCVSHIFTW (x, r0, r1, y)              -> `RISCVSHIFTW (x, map_reg r0, map_reg r1, y)
+| `RISCVRTYPEW (r0, r1, r2, x)             -> `RISCVRTYPEW (r0, map_reg r1, map_reg r2, x)
+| `RISCVFENCE (p, s)                       -> `RISCVFENCE (p, s)
+| `RISCVFENCE_TSO (p, s)                   -> `RISCVFENCE_TSO (p, s)
+| `RISCVFENCEI                             -> `RISCVFENCEI
+| `RISCVLoadRes (aq, rl, rs1, w, rd)       -> `RISCVLoadRes (aq, rl, map_reg rs1, w, map_reg rd)
+| `RISCVStoreCon (aq, rl, rs2, rs1, w, rd) -> `RISCVStoreCon (aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
+| `RISCVAMO (op, aq, rl, rs2, rs1, w, rd)  -> `RISCVAMO (op, aq, rl, map_reg rs2, map_reg rs1, w, map_reg rd)
diff --git a/handwritten_support/hgen/parser.hgen b/handwritten_support/hgen/parser.hgen
new file mode 100644
index 0000000..a4d5c07
--- /dev/null
+++ b/handwritten_support/hgen/parser.hgen
@@ -0,0 +1,76 @@
+| UTYPE reg COMMA NUM
+  { (* it's not clear if NUM here should be before or after filling the
+      lowest 12 bits with zeros, or if it should be signed or unsigned;
+      currently assuming: NUM does not include the 12 zeros, and is unsigned *)
+    if not (iskbituimm 20 $4) then failwith "immediate is not 20bit"
+    else `RISCVUTYPE ($4, $2, $1.op) }
+| JAL reg COMMA NUM
+  { if not ($4 mod 2 = 0) then failwith "odd offset"
+    else if not (iskbitsimm 21 $4) then failwith "offset is not 21bit"
+    else `RISCVJAL ($4, $2) }
+| JALR reg COMMA reg COMMA NUM
+  { if not (iskbitsimm 12 $6) then failwith "offset is not 12bit"
+    else `RISCVJALR ($6, $4, $2) }
+| BTYPE reg COMMA reg COMMA NUM
+  { if not ($6 mod 2 = 0) then failwith "odd offset"
+    else if not (iskbitsimm 13 $6) then failwith "offset is not 13bit"
+    else `RISCVBType ($6, $4, $2, $1.op) }
+| ITYPE reg COMMA reg COMMA NUM
+  { if $1.op <> RISCVSLTIU && not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
+    else if $1.op = RISCVSLTIU && not (iskbituimm 12 $6) then failwith "unsigned immediate is not 12bit"
+    else `RISCVIType ($6, $4, $2, $1.op) }
+| ADDIW reg COMMA reg COMMA NUM
+  { if not (iskbitsimm 12 $6) then failwith "immediate is not 12bit"
+    else `RISCVADDIW ($6, $4, $2) }
+| SHIFTIOP reg COMMA reg COMMA NUM
+  { if not (iskbituimm 6 $6) then failwith "unsigned immediate is not 6bit"
+    else `RISCVShiftIop ($6, $4, $2, $1.op) }
+| SHIFTW reg COMMA reg COMMA NUM
+  { if not (iskbituimm 5 $6) then failwith "unsigned immediate is not 5bit"
+    else `RISCVSHIFTW ($6, $4, $2, $1.op) }
+| RTYPE reg COMMA reg COMMA reg
+  { `RISCVRType ($6, $4, $2, $1.op) }
+| LOAD reg COMMA NUM LPAR reg RPAR
+  { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
+    else `RISCVLoad ($4, $6, $2, $1.unsigned, $1.width, $1.aq, $1.rl) }
+| STORE reg COMMA NUM LPAR reg RPAR
+  { if not (iskbitsimm 12 $4) then failwith "offset is not 12bit"
+    else `RISCVStore ($4, $2, $6, $1.width, $1.aq, $1.rl) }
+| RTYPEW reg COMMA reg COMMA reg
+  { `RISCVRTYPEW ($6, $4, $2, $1.op) }
+| FENCE FENCEOPTION COMMA FENCEOPTION
+  { match ($2, $4) with
+    | (Fence_RW, Fence_RW) -> `RISCVFENCE (0b0011, 0b0011)
+    | (Fence_R,  Fence_RW) -> `RISCVFENCE (0b0010, 0b0011)
+    | (Fence_W,  Fence_RW) -> `RISCVFENCE (0b0001, 0b0011)
+    | (Fence_RW, Fence_R)  -> `RISCVFENCE (0b0011, 0b0010)
+    | (Fence_R,  Fence_R)  -> `RISCVFENCE (0b0010, 0b0010)
+    | (Fence_W,  Fence_R)  -> `RISCVFENCE (0b0001, 0b0010)
+    | (Fence_RW, Fence_W)  -> `RISCVFENCE (0b0011, 0b0001)
+    | (Fence_R,  Fence_W)  -> `RISCVFENCE (0b0010, 0b0001)
+    | (Fence_W,  Fence_W)  -> `RISCVFENCE (0b0001, 0b0001)
+  }
+| FENCETSO
+  { `RISCVFENCE_TSO (0b0011, 0b0011) }
+| FENCEI
+  { `RISCVFENCEI }
+| LOADRES reg COMMA LPAR reg RPAR
+  { `RISCVLoadRes ($1.aq, $1.rl, $5, $1.width, $2) }
+| LOADRES reg COMMA NUM LPAR reg RPAR
+  { if $4 <> 0 then failwith "'lr' offset must be 0" else
+    `RISCVLoadRes ($1.aq, $1.rl, $6, $1.width, $2) }
+| STORECON reg COMMA reg COMMA LPAR reg RPAR
+  { `RISCVStoreCon ($1.aq, $1.rl, $4, $7, $1.width, $2) }
+| STORECON reg COMMA reg COMMA NUM LPAR reg RPAR
+  { if $6 <> 0 then failwith "'sc' offset must be 0" else
+    `RISCVStoreCon ($1.aq, $1.rl, $4, $8, $1.width, $2) }
+| AMO reg COMMA reg COMMA LPAR reg RPAR
+  { `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $7, $1.width, $2) }
+| AMO reg COMMA reg COMMA NUM LPAR reg RPAR
+  { if $6 <> 0 then failwith "'amo<op>' offset must be 0" else
+    `RISCVAMO ($1.op, $1.aq, $1.rl, $4, $8, $1.width, $2) }
+
+/* pseudo-ops */
+| LI reg COMMA NUM
+  { if not (iskbitsimm 12 $4) then failwith "immediate is not 12bit (li is currently implemented only with small immediate)"
+    else `RISCVIType ($4, IReg R0, $2, RISCVORI) }
diff --git a/handwritten_support/hgen/pretty.hgen b/handwritten_support/hgen/pretty.hgen
new file mode 100644
index 0000000..3e6e6d1
--- /dev/null
+++ b/handwritten_support/hgen/pretty.hgen
@@ -0,0 +1,36 @@
+| `RISCVThreadStart               -> "start"
+| `RISCVStopFetching              -> "stop"
+
+| `RISCVUTYPE(imm, rd, op)        -> sprintf "%s %s, %d" (pp_riscv_uop op) (pp_reg rd) imm
+| `RISCVJAL(imm, rd)              -> sprintf "jal  %s, %d" (pp_reg rd) imm
+| `RISCVJALR(imm, rs, rd)         -> sprintf "jalr %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVBType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_bop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVIType(imm, rs2, rs1, op)  -> sprintf "%s %s, %s, %d" (pp_riscv_iop op) (pp_reg rs1) (pp_reg rs2) imm
+| `RISCVShiftIop(imm, rs, rd, op) -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRType (rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_rop op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_load_op (unsigned, width, aq, rl)) (pp_reg rd) imm (pp_reg rs)
+
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+    sprintf "%s %s, %d(%s)" (pp_riscv_store_op (width, aq, rl)) (pp_reg rs2) imm (pp_reg rs1)
+
+| `RISCVADDIW(imm, rs, rd)        -> sprintf "addiw %s, %s, %d" (pp_reg rd) (pp_reg rs) imm
+| `RISCVSHIFTW(imm, rs, rd, op)   -> sprintf "%s %s, %s, %d" (pp_riscv_sop op) (pp_reg rd) (pp_reg rs) imm
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> sprintf "%s %s, %s, %s" (pp_riscv_ropw op) (pp_reg rd) (pp_reg rs1) (pp_reg rs2)
+
+| `RISCVFENCE(pred, succ)         -> sprintf "fence %s,%s" (pp_riscv_fence_option pred) (pp_riscv_fence_option succ)
+
+| `RISCVFENCE_TSO(0b0011, 0b0011) -> sprintf "fence.tso"
+| `RISCVFENCE_TSO(_, _)           -> failwith "bad fence.tso"
+
+| `RISCVFENCEI                    -> sprintf "fence.i"
+
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+    sprintf "%s %s, (%s)" (pp_riscv_load_reserved_op (aq, rl, width)) (pp_reg rd) (pp_reg rs1)
+
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_store_conditional_op (aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
+
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+    sprintf "%s %s, %s, (%s)" (pp_riscv_amo_op (op, aq, rl, width)) (pp_reg rd) (pp_reg rs2) (pp_reg rs1)
diff --git a/handwritten_support/hgen/pretty_xml.hgen b/handwritten_support/hgen/pretty_xml.hgen
new file mode 100644
index 0000000..be080cd
--- /dev/null
+++ b/handwritten_support/hgen/pretty_xml.hgen
@@ -0,0 +1,143 @@
+| `RISCVThreadStart -> ("op_thread_start", [])
+
+| `RISCVStopFetching -> ("op_stop_fetching", [])
+
+| `RISCVUTYPE(imm, rd, op) ->
+    ("op_U_type",
+      [ ("op",   pp_riscv_uop op);
+        ("uimm", sprintf "%d" imm);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVJAL(imm, rd) ->
+    ("op_jal",
+      [ ("offset", sprintf "%d" imm);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVJALR(imm, rs1, rd) ->
+    ("op_jalr",
+      [ ("offset", sprintf "%d" imm);
+        ("base",   pp_reg rs1);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVBType(imm, rs2, rs1, op) ->
+    ("op_branch",
+      [ ("op",     pp_riscv_bop op);
+        ("offset", sprintf "%d" imm);
+        ("src2",   pp_reg rs2);
+        ("src1",   pp_reg rs1);
+      ])
+
+| `RISCVIType(imm, rs1, rd, op) ->
+    ("op_I_type",
+      [ ("op",   pp_riscv_iop op);
+        ("iimm", sprintf "%d" imm);
+        ("src",  pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVShiftIop(imm, rs1, rd, op) ->
+    ("op_IS_type",
+      [ ("op",     pp_riscv_sop op);
+        ("shamt",  sprintf "%d" imm);
+        ("src",    pp_reg rs1);
+        ("dest",   pp_reg rd);
+      ])
+
+| `RISCVSHIFTW(imm, rs1, rd, op) ->
+    ("op_ISW_type",
+      [ ("op",    pp_riscv_sop op);
+        ("shamt", sprintf "%d" imm);
+        ("src",   pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVRType (rs2, rs1, rd, op) ->
+    ("op_R_type",
+      [ ("op",   pp_riscv_rop op);
+        ("src2", pp_reg rs2);
+        ("src1", pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVLoad(imm, rs1, rd, unsigned, width, aq, rl) ->
+    ("op_load",
+      [ ("aq",       if aq then "true" else "false");
+        ("rl",       if rl then "true" else "false");
+        ("width",    pp_word_width width);
+        ("unsigned", if unsigned then "true" else "false");
+        ("base",     pp_reg rs1);
+        ("offset",   sprintf "%d" imm);
+        ("dest",     pp_reg rd);
+      ])
+
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+    ("op_store",
+      [ ("aq",       if aq then "true" else "false");
+        ("rl",       if rl then "true" else "false");
+        ("width",    pp_word_width width);
+        ("src",      pp_reg rs2);
+        ("base",     pp_reg rs1);
+        ("offset",   sprintf "%d" imm);
+      ])
+
+| `RISCVADDIW(imm, rs1, rd) ->
+    ("op_addiw",
+      [ ("iimm",  sprintf "%d" imm);
+        ("src",   pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVRTYPEW(rs2, rs1, rd, op) ->
+    ("op_RW_type",
+      [ ("op",   pp_riscv_ropw op);
+        ("src2", pp_reg rs2);
+        ("src1", pp_reg rs1);
+        ("dest", pp_reg rd);
+      ])
+
+| `RISCVFENCE(pred, succ) ->
+    ("op_fence",
+      [ ("pred", pp_riscv_fence_option pred);
+        ("succ", pp_riscv_fence_option succ);
+      ])
+
+| `RISCVFENCE_TSO(pred, succ) ->
+    ("op_fence_tso",
+      [ ("pred", pp_riscv_fence_option pred);
+        ("succ", pp_riscv_fence_option succ);
+      ])
+
+| `RISCVFENCEI -> ("op_fence_i", [])
+
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+    ("op_lr",
+      [ ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("addr",  pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+    ("op_sc",
+      [ ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("addr",  pp_reg rs1);
+        ("src",   pp_reg rs2);
+        ("dest",  pp_reg rd);
+      ])
+
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+    ("op_amo",
+      [ ("op",    pp_riscv_amo_op_part op);
+        ("aq",    if aq then "true" else "false");
+        ("rl",    if rl then "true" else "false");
+        ("width", pp_word_width width);
+        ("src",   pp_reg rs2);
+        ("addr",  pp_reg rs1);
+        ("dest",  pp_reg rd);
+      ])
diff --git a/handwritten_support/hgen/sail_trans_out.hgen b/handwritten_support/hgen/sail_trans_out.hgen
new file mode 100644
index 0000000..0ddc508
--- /dev/null
+++ b/handwritten_support/hgen/sail_trans_out.hgen
@@ -0,0 +1,27 @@
+| ("StopFetching", [])            -> `RISCVStopFetching
+| ("ThreadStart", [])             -> `RISCVThreadStart
+
+| ("UTYPE", [imm; rd; op])        -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
+| ("JAL", [imm; rd])              -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
+| ("JALR", [imm; rs; rd])         -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("BTYPE", [imm; rs2; rs1; op])  -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| ("ITYPE", [imm; rs1; rd; op])   -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
+| ("SHIFTIOP", [imm; rs; rd; op]) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| ("RTYPE", [rs2; rs1; rd; op])   -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
+| ("LOAD", [imm; rs; rd; unsigned; width; aq; rl])
+                                  -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| ("STORE", [imm; rs; rd; width; aq; rl])
+                                  -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| ("ADDIW", [imm; rs; rd])        -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| ("SHIFTW", [imm; rs; rd; op])   -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| ("RTYPEW", [rs2; rs1; rd; op])  -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
+| ("FENCE", [0; pred; succ])      -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| ("FENCE", [1; pred; succ])      -> `RISCVFENCE_TSO(translate_out_imm4 pred, translate_out_imm4 succ)
+| ("FENCE", [_; pred; succ])      -> failwith "Unknown fm_mode in sail translate out"
+| ("FENCEI", [])                  -> `RISCVFENCEI
+| ("LOADRES", [aq; rl; rs1; width; rd])
+                                  -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| ("STORECON", [aq; rl; rs2; rs1; width; rd])
+                                  -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| ("AMO", [op; aq; rl; rs2; rs1; width; rd])
+                                  -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen b/handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen
new file mode 100644
index 0000000..bea72ac
--- /dev/null
+++ b/handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen
@@ -0,0 +1,26 @@
+| STOP_FETCHING ()                -> `RISCVStopFetching
+| THREAD_START ()                 -> `RISCVThreadStart
+
+| UTYPE( imm, rd, op)         -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op)
+| RISCV_JAL( imm, rd)         -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg  rd)
+| RISCV_JALR( imm, rs, rd)    -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| BTYPE( imm, rs2, rs1, op)   -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op)
+| ITYPE( imm, rs1, rd, op)    -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op)
+| SHIFTIOP( imm, rs, rd, op)  -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| RTYPE( rs2, rs1, rd, op)    -> `RISCVRType (translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_rop op)
+| LOAD( imm, rs, rd, unsigned, width, aq, rl)
+                              -> `RISCVLoad(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_bool unsigned, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| STORE( imm, rs, rd, width, aq, rl)
+                              -> `RISCVStore(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_wordWidth width, translate_out_bool aq, translate_out_bool rl)
+| ADDIW( imm, rs, rd)         -> `RISCVADDIW(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd)
+| SHIFTW( imm, rs, rd, op)    -> `RISCVSHIFTW(translate_out_imm5 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op)
+| RTYPEW( rs2, rs1, rd, op)   -> `RISCVRTYPEW(translate_out_ireg rs2, translate_out_ireg rs1, translate_out_ireg rd, translate_out_ropw op)
+| FENCE( pred, succ)          -> `RISCVFENCE(translate_out_imm4 pred, translate_out_imm4 succ)
+| FENCE_TSO( pred, succ)      -> `RISCVFENCE_TSO(translate_out_imm4 pred, translate_out_imm4 succ)
+| FENCEI ()                   -> `RISCVFENCEI
+| LOADRES( aq, rl, rs1, width, rd)
+                              -> `RISCVLoadRes(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| STORECON( aq, rl, rs2, rs1, width, rd)
+                              -> `RISCVStoreCon(translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
+| AMO( op, aq, rl, rs2, rs1, width, rd)
+                              -> `RISCVAMO(translate_out_amoop op, translate_out_bool aq, translate_out_bool rl, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_wordWidth width, translate_out_ireg rd)
diff --git a/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen b/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen
new file mode 100644
index 0000000..f3e3856
--- /dev/null
+++ b/handwritten_support/hgen/shallow_types_to_herdtools_types.hgen
@@ -0,0 +1,87 @@
+(* let translate_out_big_bit = Sail_values.unsigned
+ * 
+ * let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+ * let translate_out_signed_int inst bits = 
+ *     let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+ *     if (i >= (1 lsl (bits - 1))) then
+ *     (i - (1 lsl bits)) else
+ *       i *)
+
+let translate_out_int i = Nat_big_num.to_int (Lem.naturalFromWord i)
+let translate_out_signed_int i = Nat_big_num.to_int (Lem.signedIntegerFromWord i)
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_uop op = match op with
+  | RISCV_LUI   -> RISCVLUI
+  | RISCV_AUIPC -> RISCVAUIPC
+
+let translate_out_bop op = match op with
+  | RISCV_BEQ  -> RISCVBEQ
+  | RISCV_BNE  -> RISCVBNE
+  | RISCV_BLT  -> RISCVBLT
+  | RISCV_BGE  -> RISCVBGE
+  | RISCV_BLTU -> RISCVBLTU
+  | RISCV_BGEU -> RISCVBGEU
+
+let translate_out_iop op = match op with
+  | RISCV_ADDI   -> RISCVADDI
+  | RISCV_SLTI   -> RISCVSLTI
+  | RISCV_SLTIU  -> RISCVSLTIU
+  | RISCV_XORI   -> RISCVXORI
+  | RISCV_ORI    -> RISCVORI
+  | RISCV_ANDI   -> RISCVANDI
+
+let translate_out_sop op = match op with
+  | RISCV_SLLI -> RISCVSLLI
+  | RISCV_SRLI -> RISCVSRLI
+  | RISCV_SRAI -> RISCVSRAI
+
+let translate_out_rop op = match op with
+  | RISCV_ADD   -> RISCVADD
+  | RISCV_SUB   -> RISCVSUB
+  | RISCV_SLL   -> RISCVSLL
+  | RISCV_SLT   -> RISCVSLT
+  | RISCV_SLTU  -> RISCVSLTU
+  | RISCV_XOR   -> RISCVXOR
+  | RISCV_SRL   -> RISCVSRL
+  | RISCV_SRA   -> RISCVSRA
+  | RISCV_OR    -> RISCVOR
+  | RISCV_AND   -> RISCVAND
+
+let translate_out_ropw op = match op with
+  | RISCV_ADDW  -> RISCVADDW
+  | RISCV_SUBW  -> RISCVSUBW
+  | RISCV_SLLW  -> RISCVSLLW
+  | RISCV_SRLW  -> RISCVSRLW
+  | RISCV_SRAW  -> RISCVSRAW
+
+let translate_out_amoop op = match op with
+  | AMOSWAP -> RISCVAMOSWAP
+  | AMOADD  -> RISCVAMOADD
+  | AMOXOR  -> RISCVAMOXOR
+  | AMOAND  -> RISCVAMOAND
+  | AMOOR   -> RISCVAMOOR
+  | AMOMIN  -> RISCVAMOMIN
+  | AMOMAX  -> RISCVAMOMAX
+  | AMOMINU -> RISCVAMOMINU
+  | AMOMAXU -> RISCVAMOMAXU
+
+let translate_out_wordWidth op = match op with
+  | BYTE   -> RISCVBYTE  
+  | HALF   -> RISCVHALF  
+  | WORD   -> RISCVWORD  
+  | DOUBLE -> RISCVDOUBLE
+
+let translate_out_bool b = b (* function
+   * | Sail_values.B1  -> true
+   * | Sail_values.B0 -> false
+   * | _ -> failwith "translate_out_bool Undef" *)
+
+let translate_out_simm21 imm = translate_out_signed_int imm (* 21 *)
+let translate_out_simm20 imm = translate_out_signed_int imm (* 20 *)
+let translate_out_simm13 imm = translate_out_signed_int imm (* 13 *)
+let translate_out_simm12 imm = translate_out_signed_int imm (* 12 *)
+let translate_out_imm6 imm = translate_out_int imm
+let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
diff --git a/handwritten_support/hgen/token_types.hgen b/handwritten_support/hgen/token_types.hgen
new file mode 100644
index 0000000..1a2895a
--- /dev/null
+++ b/handwritten_support/hgen/token_types.hgen
@@ -0,0 +1,24 @@
+type token_UTYPE    = {op : riscvUop }
+type token_JAL      = unit
+type token_JALR     = unit
+type token_BType    = {op : riscvBop }
+type token_IType    = {op : riscvIop }
+type token_ShiftIop = {op : riscvSop }
+type token_RTYPE    = {op : riscvRop }
+type token_Load     = {unsigned: bool; width : wordWidth; aq: bool; rl: bool }
+type token_Store    = {width : wordWidth; aq: bool; rl: bool }
+type token_ADDIW    = unit
+type token_SHIFTW   = {op : riscvSop }
+type token_RTYPEW   = {op : riscvRopw }
+type token_FENCE    = unit
+type token_FENCETSO = unit
+type token_FENCEI   = unit
+type token_LoadRes  = {width : wordWidth; aq: bool; rl: bool }
+type token_StoreCon = {width : wordWidth; aq: bool; rl: bool }
+type token_AMO      = {width : wordWidth; aq: bool; rl: bool; op: riscvAmoop }
+
+type token_FENCEOPTION = Fence_R | Fence_W | Fence_RW
+
+(* pseudo-ops *)
+
+type token_LI = unit
diff --git a/handwritten_support/hgen/tokens.hgen b/handwritten_support/hgen/tokens.hgen
new file mode 100644
index 0000000..37c76a2
--- /dev/null
+++ b/handwritten_support/hgen/tokens.hgen
@@ -0,0 +1,20 @@
+%token <RISCVHGenBase.token_UTYPE>    UTYPE   
+%token <RISCVHGenBase.token_JAL>      JAL     
+%token <RISCVHGenBase.token_JALR>     JALR    
+%token <RISCVHGenBase.token_BType>    BTYPE   
+%token <RISCVHGenBase.token_IType>    ITYPE   
+%token <RISCVHGenBase.token_ShiftIop> SHIFTIOP
+%token <RISCVHGenBase.token_RTYPE>    RTYPE   
+%token <RISCVHGenBase.token_Load>     LOAD    
+%token <RISCVHGenBase.token_Store>    STORE   
+%token <RISCVHGenBase.token_ADDIW>    ADDIW   
+%token <RISCVHGenBase.token_SHIFTW>   SHIFTW  
+%token <RISCVHGenBase.token_RTYPEW>   RTYPEW  
+%token <RISCVHGenBase.token_FENCE>    FENCE
+%token <RISCVHGenBase.token_FENCEOPTION> FENCEOPTION
+%token <RISCVHGenBase.token_FENCETSO> FENCETSO
+%token <RISCVHGenBase.token_FENCEI>   FENCEI
+%token <RISCVHGenBase.token_LoadRes>  LOADRES
+%token <RISCVHGenBase.token_StoreCon> STORECON
+%token <RISCVHGenBase.token_AMO>      AMO
+%token <RISCVHGenBase.token_LI>       LI
diff --git a/handwritten_support/hgen/trans_sail.hgen b/handwritten_support/hgen/trans_sail.hgen
new file mode 100644
index 0000000..aceaee7
--- /dev/null
+++ b/handwritten_support/hgen/trans_sail.hgen
@@ -0,0 +1,162 @@
+| `RISCVStopFetching -> ("StopFetching", [], [])
+| `RISCVThreadStart  -> ("ThreadStart", [], [])
+
+| `RISCVUTYPE(imm, rd, op) -> 
+    ("UTYPE",
+      [
+      translate_imm20 "imm" imm;
+      translate_reg "rd" rd;
+      translate_uop "op" op;
+       ],
+      [])
+| `RISCVJAL(imm, rd) -> 
+   ("JAL",
+    [
+      translate_imm21 "imm" imm;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVJALR(imm, rs, rd) -> 
+   ("JALR",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rd;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVBType(imm, rs2, rs1, op)  -> 
+   ("BTYPE",
+    [
+      translate_imm13 "imm" imm;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_bop "op" op;
+    ],
+    [])
+| `RISCVIType(imm, rs1, rd, op)  -> 
+   ("ITYPE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_iop "op" op;
+    ],
+    [])
+| `RISCVShiftIop(imm, rs, rd, op) -> 
+   ("SHIFTIOP",
+    [
+      translate_imm6 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRType (rs2, rs1, rd, op)  -> 
+   ("RTYPE",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_rop "op" op;
+    ],
+    [])
+| `RISCVLoad(imm, rs, rd, unsigned, width, aq, rl) ->
+   ("LOAD",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_bool "unsigned" unsigned;
+      translate_width "width" width;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+    ],
+    [])
+| `RISCVStore(imm, rs2, rs1, width, aq, rl) ->
+   ("STORE",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+    ],
+    [])
+| `RISCVADDIW(imm, rs, rd)        -> 
+   ("ADDIW",
+    [
+      translate_imm12 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVSHIFTW(imm, rs, rd, op)   -> 
+   ("SHIFTW",
+    [
+      translate_imm5 "imm" imm;
+      translate_reg "rs" rs;
+      translate_reg "rd" rd;
+      translate_sop "op" op;
+    ],
+    [])
+| `RISCVRTYPEW(rs2, rs1, rd, op)  -> 
+   ("RTYPEW",
+    [
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_reg "rd" rd;
+      translate_ropw "op" op;
+    ],
+    [])
+| `RISCVFENCE(pred, succ) ->
+  ("FENCE", 
+  [
+     translate_imm4 "pred" pred;
+     translate_imm4 "succ" succ;
+  ], 
+  [])
+| `RISCVFENCE_TSO(pred, succ) ->
+  ("FENCE_TSO",
+  [
+     translate_imm4 "pred" pred;
+     translate_imm4 "succ" succ;
+  ],
+  [])
+| `RISCVFENCEI ->
+  ("FENCEI",
+  [],
+  [])
+| `RISCVLoadRes(aq, rl, rs1, width, rd) ->
+   ("LOADRES",
+    [
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVStoreCon(aq, rl, rs2, rs1, width, rd) ->
+   ("STORECON",
+    [
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
+| `RISCVAMO(op, aq, rl, rs2, rs1, width, rd) ->
+   ("AMO",
+    [
+      translate_amoop "op" op;
+      translate_bool "aq" aq;
+      translate_bool "rl" rl;
+      translate_reg "rs2" rs2;
+      translate_reg "rs1" rs1;
+      translate_width "width" width;
+      translate_reg "rd" rd;
+    ],
+    [])
diff --git a/handwritten_support/hgen/types.hgen b/handwritten_support/hgen/types.hgen
new file mode 100644
index 0000000..a0b7560
--- /dev/null
+++ b/handwritten_support/hgen/types.hgen
@@ -0,0 +1,172 @@
+type bit20 = int
+type bit12 = int
+type bit6  = int
+type bit5  = int
+type bit4  = int
+
+type riscvUop =  (* upper immediate ops *)
+| RISCVLUI
+| RISCVAUIPC
+
+let pp_riscv_uop = function
+| RISCVLUI   -> "lui"
+| RISCVAUIPC -> "auipc"
+
+
+type riscvBop =  (* branch ops *)
+| RISCVBEQ 
+| RISCVBNE
+| RISCVBLT
+| RISCVBGE
+| RISCVBLTU
+| RISCVBGEU
+
+let pp_riscv_bop = function
+| RISCVBEQ  -> "beq"
+| RISCVBNE  -> "bne"
+| RISCVBLT  -> "blt"
+| RISCVBGE  -> "bge"
+| RISCVBLTU -> "bltu"
+| RISCVBGEU -> "bgeu"
+
+type riscvIop = (* immediate ops *)
+| RISCVADDI
+| RISCVSLTI
+| RISCVSLTIU
+| RISCVXORI
+| RISCVORI
+| RISCVANDI
+
+let pp_riscv_iop = function
+| RISCVADDI  -> "addi"
+| RISCVSLTI  -> "slti"
+| RISCVSLTIU -> "sltiu"
+| RISCVXORI  -> "xori"
+| RISCVORI   -> "ori"
+| RISCVANDI  -> "andi"
+
+type riscvSop = (* shift ops *)
+| RISCVSLLI
+| RISCVSRLI
+| RISCVSRAI
+
+let pp_riscv_sop = function
+| RISCVSLLI -> "slli"
+| RISCVSRLI -> "srli"
+| RISCVSRAI -> "srai"
+
+type riscvRop = (* reg-reg ops *)
+| RISCVADD
+| RISCVSUB
+| RISCVSLL
+| RISCVSLT 
+| RISCVSLTU
+| RISCVXOR
+| RISCVSRL
+| RISCVSRA
+| RISCVOR
+| RISCVAND
+
+let pp_riscv_rop = function
+| RISCVADD  -> "add"
+| RISCVSUB  -> "sub"
+| RISCVSLL  -> "sll"
+| RISCVSLT  -> "slt"
+| RISCVSLTU -> "sltu"
+| RISCVXOR  -> "xor"
+| RISCVSRL  -> "srl"
+| RISCVSRA  -> "sra"
+| RISCVOR   -> "or"
+| RISCVAND  -> "and"
+
+type riscvRopw = (* reg-reg 32-bit ops *)
+| RISCVADDW
+| RISCVSUBW
+| RISCVSLLW
+| RISCVSRLW
+| RISCVSRAW
+
+let pp_riscv_ropw = function
+| RISCVADDW -> "addw"
+| RISCVSUBW -> "subw"
+| RISCVSLLW -> "sllw"
+| RISCVSRLW -> "srlw"
+| RISCVSRAW -> "sraw"
+
+type wordWidth = 
+  | RISCVBYTE
+  | RISCVHALF
+  | RISCVWORD
+  | RISCVDOUBLE
+
+let pp_word_width width : string =
+  begin match width with
+  | RISCVBYTE   -> "b"
+  | RISCVHALF   -> "h"
+  | RISCVWORD   -> "w"
+  | RISCVDOUBLE -> "d"
+  end
+
+let pp_riscv_load_op (unsigned, width, aq, rl) =
+  "l" ^
+  (pp_word_width width) ^
+  (if unsigned then "u" else "") ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_store_op (width, aq, rl) =
+  "s" ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_load_reserved_op (aq, rl, width) =
+  "lr." ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_store_conditional_op (aq, rl, width) =
+  "sc." ^
+  (pp_word_width width) ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+type riscvAmoop =
+  | RISCVAMOSWAP
+  | RISCVAMOADD
+  | RISCVAMOXOR
+  | RISCVAMOAND
+  | RISCVAMOOR
+  | RISCVAMOMIN
+  | RISCVAMOMAX
+  | RISCVAMOMINU
+  | RISCVAMOMAXU
+
+let pp_riscv_amo_op_part = function
+  | RISCVAMOSWAP -> "swap"
+  | RISCVAMOADD  -> "add"
+  | RISCVAMOXOR  -> "xor"
+  | RISCVAMOAND  -> "and"
+  | RISCVAMOOR   -> "or"
+  | RISCVAMOMIN  -> "min"
+  | RISCVAMOMAX  -> "max"
+  | RISCVAMOMINU -> "minu"
+  | RISCVAMOMAXU -> "maxu"
+
+let pp_riscv_amo_op (op, aq, rl, width) =
+  "amo" ^
+  pp_riscv_amo_op_part op ^
+  begin match width with
+  | RISCVWORD   -> ".w"
+  | RISCVDOUBLE -> ".d"
+  | _ -> assert false
+  end ^
+  (if aq then ".aq" else "") ^
+  (if rl then ".rl" else "")
+
+let pp_riscv_fence_option = function
+  | 0b0011 -> "rw"
+  | 0b0010 -> "r"
+  | 0b0001 -> "w"
+  | _ -> failwith "unexpected fence option"
diff --git a/handwritten_support/hgen/types_sail_trans_out.hgen b/handwritten_support/hgen/types_sail_trans_out.hgen
new file mode 100644
index 0000000..66a2020
--- /dev/null
+++ b/handwritten_support/hgen/types_sail_trans_out.hgen
@@ -0,0 +1,98 @@
+let translate_out_big_bit = function
+  | (name, Bvector _, bits) -> IInt.integer_of_bit_list bits
+  | _ -> assert false
+
+let translate_out_int inst = (Nat_big_num.to_int (translate_out_big_bit inst))
+let translate_out_signed_int inst bits = 
+    let i = (Nat_big_num.to_int (translate_out_big_bit inst)) in
+    if (i >= (1 lsl (bits - 1))) then
+    (i - (1 lsl bits)) else
+    i
+
+let translate_out_ireg ireg = IReg (int_to_ireg (translate_out_int ireg))
+
+let translate_out_simm21 imm = translate_out_signed_int imm 21
+let translate_out_simm20 imm = translate_out_signed_int imm 20
+let translate_out_simm13 imm = translate_out_signed_int imm 13
+let translate_out_simm12 imm = translate_out_signed_int imm 12
+let translate_out_imm6 imm = translate_out_int imm
+let translate_out_imm5 imm = translate_out_int imm
+let translate_out_imm4 imm = translate_out_int imm
+
+let translate_out_bool = function
+  | (name, Bit, [Bitc_one])  -> true
+  | (name, Bit, [Bitc_zero]) -> false
+  | _ -> assert false
+
+let translate_out_enum (name,_,bits) =
+    Nat_big_num.to_int (IInt.integer_of_bit_list bits)
+
+let translate_out_wordWidth w = 
+    match translate_out_enum w with
+    | 0 -> RISCVBYTE
+    | 1 -> RISCVHALF
+    | 2 -> RISCVWORD
+    | 3 -> RISCVDOUBLE
+    | _ -> failwith "Unknown wordWidth in sail translate out"
+
+let translate_out_uop op = match translate_out_enum op with
+    | 0 -> RISCVLUI
+    | 1 -> RISCVAUIPC
+    | _ -> failwith "Unknown uop in sail translate out"
+
+let translate_out_bop op = match translate_out_enum op with
+| 0 -> RISCVBEQ 
+| 1 -> RISCVBNE 
+| 2 -> RISCVBLT 
+| 3 -> RISCVBGE 
+| 4 -> RISCVBLTU
+| 5 -> RISCVBGEU
+| _ -> failwith "Unknown bop in sail translate out"
+
+let translate_out_iop op = match translate_out_enum op with
+| 0 -> RISCVADDI 
+| 1 -> RISCVSLTI 
+| 2 -> RISCVSLTIU
+| 3 -> RISCVXORI 
+| 4 -> RISCVORI  
+| 5 -> RISCVANDI 
+| _ -> failwith "Unknown iop in sail translate out"
+
+let translate_out_sop op = match translate_out_enum op with 
+| 0 -> RISCVSLLI
+| 1 -> RISCVSRLI
+| 2 -> RISCVSRAI
+| _ -> failwith "Unknown sop in sail translate out"
+
+let translate_out_rop op = match translate_out_enum op with
+| 0 -> RISCVADD 
+| 1 -> RISCVSUB 
+| 2 -> RISCVSLL 
+| 3 -> RISCVSLT 
+| 4 -> RISCVSLTU
+| 5 -> RISCVXOR 
+| 6 -> RISCVSRL 
+| 7 -> RISCVSRA 
+| 8 -> RISCVOR  
+| 9 -> RISCVAND 
+| _ -> failwith "Unknown rop in sail translate out"
+
+let translate_out_ropw op = match translate_out_enum op with
+| 0 -> RISCVADDW
+| 1 -> RISCVSUBW
+| 2 -> RISCVSLLW
+| 3 -> RISCVSRLW
+| 4 -> RISCVSRAW
+| _ -> failwith "Unknown ropw in sail translate out"
+
+let translate_out_amoop op = match translate_out_enum op with
+| 0 -> RISCVAMOSWAP
+| 1 -> RISCVAMOADD
+| 2 -> RISCVAMOXOR
+| 3 -> RISCVAMOAND
+| 4 -> RISCVAMOOR
+| 5 -> RISCVAMOMIN
+| 6 -> RISCVAMOMAX
+| 7 -> RISCVAMOMINU
+| 8 -> RISCVAMOMAXU
+| _ -> failwith "Unknown amoop in sail translate out"
diff --git a/handwritten_support/hgen/types_trans_sail.hgen b/handwritten_support/hgen/types_trans_sail.hgen
new file mode 100644
index 0000000..238c7e5
--- /dev/null
+++ b/handwritten_support/hgen/types_trans_sail.hgen
@@ -0,0 +1,57 @@
+let translate_enum enum_values name value =
+  let rec bit_count n =
+    if n = 0 then 0
+    else 1 + (bit_count (n lsr 1)) in
+  let rec find_index element = function
+    | h::tail -> if h = element then 0 else 1 + (find_index element tail)
+    | _ -> failwith "translate_enum could not find value"
+    in
+  let size = bit_count (List.length enum_values) in
+  let index = find_index value enum_values in
+  (name, Range0 (Some size),  IInt.bit_list_of_integer size (Nat_big_num.of_int index))
+
+let translate_uop = translate_enum [RISCVLUI; RISCVAUIPC]
+
+let translate_bop = translate_enum [RISCVBEQ; RISCVBNE; RISCVBLT; RISCVBGE; RISCVBLTU; RISCVBGEU] (* branch ops *)
+
+let translate_iop = translate_enum [RISCVADDI; RISCVSLTI; RISCVSLTIU; RISCVXORI; RISCVORI; RISCVANDI] (* immediate ops *)
+
+let translate_sop = translate_enum [RISCVSLLI; RISCVSRLI; RISCVSRAI] (* shift ops *)
+
+let translate_rop = translate_enum [RISCVADD; RISCVSUB; RISCVSLL; RISCVSLT; RISCVSLTU; RISCVXOR; RISCVSRL; RISCVSRA; RISCVOR; RISCVAND] (* reg-reg ops *)
+
+let translate_ropw = translate_enum [RISCVADDW; RISCVSUBW; RISCVSLLW; RISCVSRLW; RISCVSRAW] (* reg-reg 32-bit ops *)
+
+let translate_amoop = translate_enum [RISCVAMOSWAP; RISCVAMOADD; RISCVAMOXOR; RISCVAMOAND; RISCVAMOOR; RISCVAMOMIN; RISCVAMOMAX; RISCVAMOMINU; RISCVAMOMAXU]
+
+let translate_width = translate_enum [RISCVBYTE; RISCVHALF; RISCVWORD; RISCVDOUBLE] 
+
+let translate_reg name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int (reg_to_int value)))
+
+let translate_imm21 name value = 
+    (name, Bvector (Some 21), bit_list_of_integer 21 (Nat_big_num.of_int value))
+
+let translate_imm20 name value = 
+    (name, Bvector (Some 20), bit_list_of_integer 20 (Nat_big_num.of_int value))
+
+let translate_imm16 name value = 
+    (name, Bvector (Some 16), bit_list_of_integer 16 (Nat_big_num.of_int value))
+
+let translate_imm13 name value = 
+    (name, Bvector (Some 13), bit_list_of_integer 13 (Nat_big_num.of_int value))
+
+let translate_imm12 name value = 
+    (name, Bvector (Some 12), bit_list_of_integer 12 (Nat_big_num.of_int value))
+
+let translate_imm6 name value = 
+    (name, Bvector (Some 6), bit_list_of_integer 6 (Nat_big_num.of_int value))
+
+let translate_imm5 name value = 
+    (name, Bvector (Some 5), bit_list_of_integer 5 (Nat_big_num.of_int value))
+
+let translate_imm4 name value = 
+    (name, Bvector (Some 4), bit_list_of_integer 4 (Nat_big_num.of_int value))
+
+let translate_bool name value =
+  (name, Bit, [if value then Bitc_one else Bitc_zero])
diff --git a/handwritten_support/mem_metadata.glob b/handwritten_support/mem_metadata.glob
new file mode 100644
index 0000000..c2d0ccd
--- /dev/null
+++ b/handwritten_support/mem_metadata.glob
@@ -0,0 +1,64 @@
+DIGEST 693b57d74f776ae8bd215fbfc8b03df3
+Fmem_metadata
+R15:23 Sail.Base <> <> lib
+def 52:60 <> write_ram
+binder 63:64 <> rv:1
+binder 66:66 <> e:2
+binder 68:68 <> a:3
+binder 71:72 <> wk:4
+R82:86 Sail.Values <> mword def
+R88:88 mem_metadata <> a:3 var
+binder 75:78 <> addr:5
+binder 91:94 <> size:6
+R101:105 Sail.Values <> mword def
+R109:111 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R112:115 mem_metadata <> size:6 var
+binder 97:97 <> v:7
+R127:130 Coq.Init.Datatypes <> unit ind
+binder 120:123 <> meta:8
+R135:139 Sail.Prompt_monad <> monad ind
+R141:142 mem_metadata <> rv:1 var
+R144:147 Coq.Init.Datatypes <> bool ind
+R149:149 mem_metadata <> e:2 var
+R154:162 Sail.Prompt_monad <> write_mem def
+R179:179 mem_metadata <> v:7 var
+R174:177 mem_metadata <> size:6 var
+R169:172 mem_metadata <> addr:5 var
+R167:167 mem_metadata <> a:3 var
+R164:165 mem_metadata <> wk:4 var
+def 194:201 <> read_ram
+binder 204:205 <> rv:9
+binder 207:207 <> e:10
+binder 209:209 <> a:11
+binder 212:213 <> rk:12
+R223:227 Sail.Values <> mword def
+R229:229 mem_metadata <> a:11 var
+binder 216:219 <> addr:13
+binder 232:235 <> size:14
+R249:252 Coq.Init.Datatypes <> bool ind
+binder 238:245 <> read_tag:15
+R257:265 Sail.Values <> ArithFact class
+R272:276 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R268:271 mem_metadata <> size:14 var
+binder 257:278 <> H:16
+R283:287 Sail.Prompt_monad <> monad ind
+R289:290 mem_metadata <> rv:9 var
+R309:311 Coq.Init.Datatypes <> ::type_scope:x_'*'_x not
+R293:297 Sail.Values <> mword def
+R301:303 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R304:307 mem_metadata <> size:14 var
+R312:315 Coq.Init.Datatypes <> unit ind
+R318:318 mem_metadata <> e:10 var
+R348:352 Sail.Prompt_monad <> :::x_'>>='_x not
+R325:332 Sail.Prompt_monad <> read_mem def
+R344:347 mem_metadata <> size:14 var
+R339:342 mem_metadata <> addr:13 var
+R337:337 mem_metadata <> a:11 var
+R334:335 mem_metadata <> rk:12 var
+binder 357:360 <> data:17
+R367:373 Sail.Prompt_monad <> returnm def
+R375:375 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
+R380:381 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
+R384:384 Coq.Init.Datatypes <> ::core_scope:'('_x_','_x_','_'..'_','_x_')' not
+R376:379 mem_metadata <> data:17 var
+R382:383 Coq.Init.Datatypes <> tt constr
diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem
new file mode 100644
index 0000000..8a8c070
--- /dev/null
+++ b/handwritten_support/mem_metadata.lem
@@ -0,0 +1,16 @@
+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/mem_metadata.v b/handwritten_support/mem_metadata.v
new file mode 100644
index 0000000..bbfc856
--- /dev/null
+++ b/handwritten_support/mem_metadata.v
@@ -0,0 +1,8 @@
+Require Import Sail.Base.
+Open Scope Z.
+
+Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v.
+
+Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size) * unit) e :=
+  read_mem rk a addr size >>= fun data =>
+  returnm (data, tt).
diff --git a/handwritten_support/mem_metadata.vo b/handwritten_support/mem_metadata.vo
new file mode 100644
index 0000000..76f5087
--- /dev/null
+++ b/handwritten_support/mem_metadata.vo
diff --git a/handwritten_support/mem_metadata.vok b/handwritten_support/mem_metadata.vok
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/handwritten_support/mem_metadata.vok
diff --git a/handwritten_support/mem_metadata.vos b/handwritten_support/mem_metadata.vos
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/handwritten_support/mem_metadata.vos
diff --git a/handwritten_support/riscv_extras.glob b/handwritten_support/riscv_extras.glob
new file mode 100644
index 0000000..980acb4
--- /dev/null
+++ b/handwritten_support/riscv_extras.glob
@@ -0,0 +1,875 @@
+DIGEST 9f6e940694efb436e57a7a26d0b1b3b3
+Friscv_extras
+R15:23 Sail.Base <> <> lib
+R41:46 Coq.Strings.String <> <> lib
+R64:67 Coq.Lists.List <> <> lib
+def 123:137 <> MEM_fence_rw_rw
+binder 140:141 <> rv:1
+binder 143:143 <> e:2
+R149:152 Coq.Init.Datatypes <> unit ind
+R157:161 Sail.Prompt_monad <> monad ind
+R163:164 riscv_extras <> rv:1 var
+R166:169 Coq.Init.Datatypes <> unit ind
+R171:171 riscv_extras <> e:2 var
+R176:182 Sail.Prompt_monad <> barrier def
+R185:203 Sail.Instr_kinds <> Barrier_RISCV_rw_rw constr
+R205:206 Coq.Init.Datatypes <> tt constr
+def 221:234 <> MEM_fence_r_rw
+binder 238:239 <> rv:3
+binder 241:241 <> e:4
+R247:250 Coq.Init.Datatypes <> unit ind
+R255:259 Sail.Prompt_monad <> monad ind
+R261:262 riscv_extras <> rv:3 var
+R264:267 Coq.Init.Datatypes <> unit ind
+R269:269 riscv_extras <> e:4 var
+R274:280 Sail.Prompt_monad <> barrier def
+R283:300 Sail.Instr_kinds <> Barrier_RISCV_r_rw constr
+R302:303 Coq.Init.Datatypes <> tt constr
+def 318:330 <> MEM_fence_r_r
+binder 335:336 <> rv:5
+binder 338:338 <> e:6
+R344:347 Coq.Init.Datatypes <> unit ind
+R352:356 Sail.Prompt_monad <> monad ind
+R358:359 riscv_extras <> rv:5 var
+R361:364 Coq.Init.Datatypes <> unit ind
+R366:366 riscv_extras <> e:6 var
+R371:377 Sail.Prompt_monad <> barrier def
+R380:396 Sail.Instr_kinds <> Barrier_RISCV_r_r constr
+R398:399 Coq.Init.Datatypes <> tt constr
+def 414:427 <> MEM_fence_rw_w
+binder 431:432 <> rv:7
+binder 434:434 <> e:8
+R440:443 Coq.Init.Datatypes <> unit ind
+R448:452 Sail.Prompt_monad <> monad ind
+R454:455 riscv_extras <> rv:7 var
+R457:460 Coq.Init.Datatypes <> unit ind
+R462:462 riscv_extras <> e:8 var
+R467:473 Sail.Prompt_monad <> barrier def
+R476:493 Sail.Instr_kinds <> Barrier_RISCV_rw_w constr
+R495:496 Coq.Init.Datatypes <> tt constr
+def 511:523 <> MEM_fence_w_w
+binder 528:529 <> rv:9
+binder 531:531 <> e:10
+R537:540 Coq.Init.Datatypes <> unit ind
+R545:549 Sail.Prompt_monad <> monad ind
+R551:552 riscv_extras <> rv:9 var
+R554:557 Coq.Init.Datatypes <> unit ind
+R559:559 riscv_extras <> e:10 var
+R564:570 Sail.Prompt_monad <> barrier def
+R573:589 Sail.Instr_kinds <> Barrier_RISCV_w_w constr
+R591:592 Coq.Init.Datatypes <> tt constr
+def 607:620 <> MEM_fence_w_rw
+binder 624:625 <> rv:11
+binder 627:627 <> e:12
+R633:636 Coq.Init.Datatypes <> unit ind
+R641:645 Sail.Prompt_monad <> monad ind
+R647:648 riscv_extras <> rv:11 var
+R650:653 Coq.Init.Datatypes <> unit ind
+R655:655 riscv_extras <> e:12 var
+R660:666 Sail.Prompt_monad <> barrier def
+R669:686 Sail.Instr_kinds <> Barrier_RISCV_w_rw constr
+R688:689 Coq.Init.Datatypes <> tt constr
+def 704:717 <> MEM_fence_rw_r
+binder 721:722 <> rv:13
+binder 724:724 <> e:14
+R730:733 Coq.Init.Datatypes <> unit ind
+R738:742 Sail.Prompt_monad <> monad ind
+R744:745 riscv_extras <> rv:13 var
+R747:750 Coq.Init.Datatypes <> unit ind
+R752:752 riscv_extras <> e:14 var
+R757:763 Sail.Prompt_monad <> barrier def
+R766:783 Sail.Instr_kinds <> Barrier_RISCV_rw_r constr
+R785:786 Coq.Init.Datatypes <> tt constr
+def 801:813 <> MEM_fence_r_w
+binder 818:819 <> rv:15
+binder 821:821 <> e:16
+R827:830 Coq.Init.Datatypes <> unit ind
+R835:839 Sail.Prompt_monad <> monad ind
+R841:842 riscv_extras <> rv:15 var
+R844:847 Coq.Init.Datatypes <> unit ind
+R849:849 riscv_extras <> e:16 var
+R854:860 Sail.Prompt_monad <> barrier def
+R863:879 Sail.Instr_kinds <> Barrier_RISCV_r_w constr
+R881:882 Coq.Init.Datatypes <> tt constr
+def 897:909 <> MEM_fence_w_r
+binder 914:915 <> rv:17
+binder 917:917 <> e:18
+R923:926 Coq.Init.Datatypes <> unit ind
+R931:935 Sail.Prompt_monad <> monad ind
+R937:938 riscv_extras <> rv:17 var
+R940:943 Coq.Init.Datatypes <> unit ind
+R945:945 riscv_extras <> e:18 var
+R950:956 Sail.Prompt_monad <> barrier def
+R959:975 Sail.Instr_kinds <> Barrier_RISCV_w_r constr
+R977:978 Coq.Init.Datatypes <> tt constr
+def 993:1005 <> MEM_fence_tso
+binder 1010:1011 <> rv:19
+binder 1013:1013 <> e:20
+R1019:1022 Coq.Init.Datatypes <> unit ind
+R1027:1031 Sail.Prompt_monad <> monad ind
+R1033:1034 riscv_extras <> rv:19 var
+R1036:1039 Coq.Init.Datatypes <> unit ind
+R1041:1041 riscv_extras <> e:20 var
+R1046:1052 Sail.Prompt_monad <> barrier def
+R1055:1071 Sail.Instr_kinds <> Barrier_RISCV_tso constr
+R1073:1074 Coq.Init.Datatypes <> tt constr
+def 1089:1099 <> MEM_fence_i
+binder 1106:1107 <> rv:21
+binder 1109:1109 <> e:22
+R1115:1118 Coq.Init.Datatypes <> unit ind
+R1123:1127 Sail.Prompt_monad <> monad ind
+R1129:1130 riscv_extras <> rv:21 var
+R1132:1135 Coq.Init.Datatypes <> unit ind
+R1137:1137 riscv_extras <> e:22 var
+R1142:1148 Sail.Prompt_monad <> barrier def
+R1151:1165 Sail.Instr_kinds <> Barrier_RISCV_i constr
+R1167:1168 Coq.Init.Datatypes <> tt constr
+def 1867:1871 <> MEMea
+binder 1874:1875 <> rv:23
+binder 1877:1877 <> a:24
+binder 1879:1879 <> e:25
+binder 1882:1889 <> addrsize:26
+R1899:1903 Sail.Values <> mword def
+R1905:1905 riscv_extras <> a:24 var
+binder 1892:1895 <> addr:27
+binder 1908:1911 <> size:28
+R1935:1939 Sail.Prompt_monad <> monad ind
+R1941:1942 riscv_extras <> rv:23 var
+R1944:1947 Coq.Init.Datatypes <> unit ind
+R1949:1949 riscv_extras <> e:25 var
+R1954:1965 Sail.Prompt_monad <> write_mem_ea def
+R1993:1996 riscv_extras <> size:28 var
+R1988:1991 riscv_extras <> addr:27 var
+R1979:1986 riscv_extras <> addrsize:26 var
+R1967:1977 Sail.Instr_kinds <> Write_plain constr
+def 2010:2022 <> MEMea_release
+binder 2025:2026 <> rv:29
+binder 2028:2028 <> a:30
+binder 2030:2030 <> e:31
+binder 2033:2040 <> addrsize:32
+R2050:2054 Sail.Values <> mword def
+R2056:2056 riscv_extras <> a:30 var
+binder 2043:2046 <> addr:33
+binder 2059:2062 <> size:34
+R2078:2082 Sail.Prompt_monad <> monad ind
+R2084:2085 riscv_extras <> rv:29 var
+R2087:2090 Coq.Init.Datatypes <> unit ind
+R2092:2092 riscv_extras <> e:31 var
+R2097:2108 Sail.Prompt_monad <> write_mem_ea def
+R2144:2147 riscv_extras <> size:34 var
+R2139:2142 riscv_extras <> addr:33 var
+R2130:2137 riscv_extras <> addrsize:32 var
+R2110:2128 Sail.Instr_kinds <> Write_RISCV_release constr
+def 2161:2180 <> MEMea_strong_release
+binder 2183:2184 <> rv:35
+binder 2186:2186 <> a:36
+binder 2188:2188 <> e:37
+binder 2191:2198 <> addrsize:38
+R2208:2212 Sail.Values <> mword def
+R2214:2214 riscv_extras <> a:36 var
+binder 2201:2204 <> addr:39
+binder 2217:2220 <> size:40
+R2229:2233 Sail.Prompt_monad <> monad ind
+R2235:2236 riscv_extras <> rv:35 var
+R2238:2241 Coq.Init.Datatypes <> unit ind
+R2243:2243 riscv_extras <> e:37 var
+R2248:2259 Sail.Prompt_monad <> write_mem_ea def
+R2302:2305 riscv_extras <> size:40 var
+R2297:2300 riscv_extras <> addr:39 var
+R2288:2295 riscv_extras <> addrsize:38 var
+R2261:2286 Sail.Instr_kinds <> Write_RISCV_strong_release constr
+def 2319:2335 <> MEMea_conditional
+binder 2338:2339 <> rv:41
+binder 2341:2341 <> a:42
+binder 2343:2343 <> e:43
+binder 2346:2353 <> addrsize:44
+R2363:2367 Sail.Values <> mword def
+R2369:2369 riscv_extras <> a:42 var
+binder 2356:2359 <> addr:45
+binder 2372:2375 <> size:46
+R2387:2391 Sail.Prompt_monad <> monad ind
+R2393:2394 riscv_extras <> rv:41 var
+R2396:2399 Coq.Init.Datatypes <> unit ind
+R2401:2401 riscv_extras <> e:43 var
+R2406:2417 Sail.Prompt_monad <> write_mem_ea def
+R2457:2460 riscv_extras <> size:46 var
+R2452:2455 riscv_extras <> addr:45 var
+R2443:2450 riscv_extras <> addrsize:44 var
+R2419:2441 Sail.Instr_kinds <> Write_RISCV_conditional constr
+def 2474:2498 <> MEMea_conditional_release
+binder 2501:2502 <> rv:47
+binder 2504:2504 <> a:48
+binder 2506:2506 <> e:49
+binder 2509:2516 <> addrsize:50
+R2526:2530 Sail.Values <> mword def
+R2532:2532 riscv_extras <> a:48 var
+binder 2519:2522 <> addr:51
+binder 2535:2538 <> size:52
+R2542:2546 Sail.Prompt_monad <> monad ind
+R2548:2549 riscv_extras <> rv:47 var
+R2551:2554 Coq.Init.Datatypes <> unit ind
+R2556:2556 riscv_extras <> e:49 var
+R2561:2572 Sail.Prompt_monad <> write_mem_ea def
+R2620:2623 riscv_extras <> size:52 var
+R2615:2618 riscv_extras <> addr:51 var
+R2606:2613 riscv_extras <> addrsize:50 var
+R2574:2604 Sail.Instr_kinds <> Write_RISCV_conditional_release constr
+def 2637:2668 <> MEMea_conditional_strong_release
+binder 2671:2672 <> rv:53
+binder 2674:2674 <> a:54
+binder 2676:2676 <> e:55
+binder 2679:2686 <> addrsize:56
+R2696:2700 Sail.Values <> mword def
+R2702:2702 riscv_extras <> a:54 var
+binder 2689:2692 <> addr:57
+binder 2705:2708 <> size:58
+R2712:2716 Sail.Prompt_monad <> monad ind
+R2718:2719 riscv_extras <> rv:53 var
+R2721:2724 Coq.Init.Datatypes <> unit ind
+R2726:2726 riscv_extras <> e:55 var
+R2773:2784 Sail.Prompt_monad <> write_mem_ea def
+R2839:2842 riscv_extras <> size:58 var
+R2834:2837 riscv_extras <> addr:57 var
+R2825:2832 riscv_extras <> addrsize:56 var
+R2786:2823 Sail.Instr_kinds <> Write_RISCV_conditional_strong_release constr
+def 3812:3815 <> MEMr
+binder 3818:3819 <> rv:59
+binder 3821:3821 <> e:60
+binder 3824:3831 <> addrsize:61
+binder 3833:3836 <> size:62
+R3853:3857 Sail.Values <> mword def
+R3859:3866 riscv_extras <> addrsize:61 var
+binder 3839:3844 <> hexRAM:63
+binder 3846:3849 <> addr:64
+R3895:3903 Sail.Values <> ArithFact class
+R3910:3914 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R3906:3909 riscv_extras <> size:62 var
+binder 3895:3916 <> H:65
+R3921:3925 Sail.Prompt_monad <> monad ind
+R3927:3928 riscv_extras <> rv:59 var
+R3931:3935 Sail.Values <> mword def
+R3939:3941 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R3942:3945 riscv_extras <> size:62 var
+R3949:3949 riscv_extras <> e:60 var
+R3954:3961 Sail.Prompt_monad <> read_mem def
+R3988:3991 riscv_extras <> size:62 var
+R3983:3986 riscv_extras <> addr:64 var
+R3974:3981 riscv_extras <> addrsize:61 var
+R3963:3972 Sail.Instr_kinds <> Read_plain constr
+def 4005:4016 <> MEMr_acquire
+binder 4019:4020 <> rv:66
+binder 4022:4022 <> e:67
+binder 4025:4032 <> addrsize:68
+binder 4034:4037 <> size:69
+R4054:4058 Sail.Values <> mword def
+R4060:4067 riscv_extras <> addrsize:68 var
+binder 4040:4045 <> hexRAM:70
+binder 4047:4050 <> addr:71
+R4088:4096 Sail.Values <> ArithFact class
+R4103:4107 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R4099:4102 riscv_extras <> size:69 var
+binder 4088:4109 <> H:72
+R4114:4118 Sail.Prompt_monad <> monad ind
+R4120:4121 riscv_extras <> rv:66 var
+R4124:4128 Sail.Values <> mword def
+R4132:4134 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R4135:4138 riscv_extras <> size:69 var
+R4142:4142 riscv_extras <> e:67 var
+R4147:4154 Sail.Prompt_monad <> read_mem def
+R4189:4192 riscv_extras <> size:69 var
+R4184:4187 riscv_extras <> addr:71 var
+R4175:4182 riscv_extras <> addrsize:68 var
+R4156:4173 Sail.Instr_kinds <> Read_RISCV_acquire constr
+def 4206:4224 <> MEMr_strong_acquire
+binder 4227:4228 <> rv:73
+binder 4230:4230 <> e:74
+binder 4233:4240 <> addrsize:75
+binder 4242:4245 <> size:76
+R4262:4266 Sail.Values <> mword def
+R4268:4275 riscv_extras <> addrsize:75 var
+binder 4248:4253 <> hexRAM:77
+binder 4255:4258 <> addr:78
+R4289:4297 Sail.Values <> ArithFact class
+R4304:4308 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R4300:4303 riscv_extras <> size:76 var
+binder 4289:4310 <> H:79
+R4315:4319 Sail.Prompt_monad <> monad ind
+R4321:4322 riscv_extras <> rv:73 var
+R4325:4329 Sail.Values <> mword def
+R4333:4335 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R4336:4339 riscv_extras <> size:76 var
+R4343:4343 riscv_extras <> e:74 var
+R4348:4355 Sail.Prompt_monad <> read_mem def
+R4397:4400 riscv_extras <> size:76 var
+R4392:4395 riscv_extras <> addr:78 var
+R4383:4390 riscv_extras <> addrsize:75 var
+R4357:4381 Sail.Instr_kinds <> Read_RISCV_strong_acquire constr
+def 4414:4426 <> MEMr_reserved
+binder 4429:4430 <> rv:80
+binder 4432:4432 <> e:81
+binder 4435:4442 <> addrsize:82
+binder 4444:4447 <> size:83
+R4464:4468 Sail.Values <> mword def
+R4470:4477 riscv_extras <> addrsize:82 var
+binder 4450:4455 <> hexRAM:84
+binder 4457:4460 <> addr:85
+R4497:4505 Sail.Values <> ArithFact class
+R4512:4516 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R4508:4511 riscv_extras <> size:83 var
+binder 4497:4518 <> H:86
+R4523:4527 Sail.Prompt_monad <> monad ind
+R4529:4530 riscv_extras <> rv:80 var
+R4533:4537 Sail.Values <> mword def
+R4541:4543 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R4544:4547 riscv_extras <> size:83 var
+R4551:4551 riscv_extras <> e:81 var
+R4556:4563 Sail.Prompt_monad <> read_mem def
+R4599:4602 riscv_extras <> size:83 var
+R4594:4597 riscv_extras <> addr:85 var
+R4585:4592 riscv_extras <> addrsize:82 var
+R4565:4583 Sail.Instr_kinds <> Read_RISCV_reserved constr
+def 4616:4636 <> MEMr_reserved_acquire
+binder 4639:4640 <> rv:87
+binder 4642:4642 <> e:88
+binder 4645:4652 <> addrsize:89
+binder 4654:4657 <> size:90
+R4674:4678 Sail.Values <> mword def
+R4680:4687 riscv_extras <> addrsize:89 var
+binder 4660:4665 <> hexRAM:91
+binder 4667:4670 <> addr:92
+R4699:4707 Sail.Values <> ArithFact class
+R4714:4718 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R4710:4713 riscv_extras <> size:90 var
+binder 4699:4720 <> H:93
+R4725:4729 Sail.Prompt_monad <> monad ind
+R4731:4732 riscv_extras <> rv:87 var
+R4735:4739 Sail.Values <> mword def
+R4743:4745 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R4746:4749 riscv_extras <> size:90 var
+R4753:4753 riscv_extras <> e:88 var
+R4758:4765 Sail.Prompt_monad <> read_mem def
+R4809:4812 riscv_extras <> size:90 var
+R4804:4807 riscv_extras <> addr:92 var
+R4795:4802 riscv_extras <> addrsize:89 var
+R4767:4793 Sail.Instr_kinds <> Read_RISCV_reserved_acquire constr
+def 4826:4853 <> MEMr_reserved_strong_acquire
+binder 4856:4857 <> rv:94
+binder 4859:4859 <> e:95
+binder 4862:4869 <> addrsize:96
+binder 4871:4874 <> size:97
+R4891:4895 Sail.Values <> mword def
+R4897:4904 riscv_extras <> addrsize:96 var
+binder 4877:4882 <> hexRAM:98
+binder 4884:4887 <> addr:99
+R4909:4917 Sail.Values <> ArithFact class
+R4924:4928 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R4920:4923 riscv_extras <> size:97 var
+binder 4909:4930 <> H:100
+R4935:4939 Sail.Prompt_monad <> monad ind
+R4941:4942 riscv_extras <> rv:94 var
+R4945:4949 Sail.Values <> mword def
+R4953:4955 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R4956:4959 riscv_extras <> size:97 var
+R4963:4963 riscv_extras <> e:95 var
+R4968:4975 Sail.Prompt_monad <> read_mem def
+R5026:5029 riscv_extras <> size:97 var
+R5021:5024 riscv_extras <> addr:99 var
+R5012:5019 riscv_extras <> addrsize:96 var
+R4977:5010 Sail.Instr_kinds <> Read_RISCV_reserved_strong_acquire constr
+def 6053:6056 <> MEMw
+binder 6059:6060 <> rv:101
+binder 6062:6062 <> e:102
+binder 6065:6072 <> addrsize:103
+binder 6074:6077 <> size:104
+R6094:6098 Sail.Values <> mword def
+R6100:6107 riscv_extras <> addrsize:103 var
+binder 6080:6085 <> hexRAM:105
+binder 6087:6090 <> addr:106
+R6115:6119 Sail.Values <> mword def
+R6123:6125 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R6126:6129 riscv_extras <> size:104 var
+binder 6111:6111 <> v:107
+R6162:6166 Sail.Prompt_monad <> monad ind
+R6168:6169 riscv_extras <> rv:101 var
+R6171:6174 Coq.Init.Datatypes <> bool ind
+R6176:6176 riscv_extras <> e:102 var
+R6181:6189 Sail.Prompt_monad <> write_mem def
+R6222:6222 riscv_extras <> v:107 var
+R6217:6220 riscv_extras <> size:104 var
+R6212:6215 riscv_extras <> addr:106 var
+R6203:6210 riscv_extras <> addrsize:103 var
+R6191:6201 Sail.Instr_kinds <> Write_plain constr
+def 6236:6247 <> MEMw_release
+binder 6250:6251 <> rv:108
+binder 6253:6253 <> e:109
+binder 6256:6263 <> addrsize:110
+binder 6265:6268 <> size:111
+R6285:6289 Sail.Values <> mword def
+R6291:6298 riscv_extras <> addrsize:110 var
+binder 6271:6276 <> hexRAM:112
+binder 6278:6281 <> addr:113
+R6306:6310 Sail.Values <> mword def
+R6314:6316 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R6317:6320 riscv_extras <> size:111 var
+binder 6302:6302 <> v:114
+R6345:6349 Sail.Prompt_monad <> monad ind
+R6351:6352 riscv_extras <> rv:108 var
+R6354:6357 Coq.Init.Datatypes <> bool ind
+R6359:6359 riscv_extras <> e:109 var
+R6364:6372 Sail.Prompt_monad <> write_mem def
+R6413:6413 riscv_extras <> v:114 var
+R6408:6411 riscv_extras <> size:111 var
+R6403:6406 riscv_extras <> addr:113 var
+R6394:6401 riscv_extras <> addrsize:110 var
+R6374:6392 Sail.Instr_kinds <> Write_RISCV_release constr
+def 6427:6445 <> MEMw_strong_release
+binder 6448:6449 <> rv:115
+binder 6451:6451 <> e:116
+binder 6454:6461 <> addrsize:117
+binder 6463:6466 <> size:118
+R6483:6487 Sail.Values <> mword def
+R6489:6496 riscv_extras <> addrsize:117 var
+binder 6469:6474 <> hexRAM:119
+binder 6476:6479 <> addr:120
+R6504:6508 Sail.Values <> mword def
+R6512:6514 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R6515:6518 riscv_extras <> size:118 var
+binder 6500:6500 <> v:121
+R6536:6540 Sail.Prompt_monad <> monad ind
+R6542:6543 riscv_extras <> rv:115 var
+R6545:6548 Coq.Init.Datatypes <> bool ind
+R6550:6550 riscv_extras <> e:116 var
+R6555:6563 Sail.Prompt_monad <> write_mem def
+R6611:6611 riscv_extras <> v:121 var
+R6606:6609 riscv_extras <> size:118 var
+R6601:6604 riscv_extras <> addr:120 var
+R6592:6599 riscv_extras <> addrsize:117 var
+R6565:6590 Sail.Instr_kinds <> Write_RISCV_strong_release constr
+def 6625:6640 <> MEMw_conditional
+binder 6643:6644 <> rv:122
+binder 6646:6646 <> e:123
+binder 6649:6656 <> addrsize:124
+binder 6658:6661 <> size:125
+R6678:6682 Sail.Values <> mword def
+R6684:6691 riscv_extras <> addrsize:124 var
+binder 6664:6669 <> hexRAM:126
+binder 6671:6674 <> addr:127
+R6699:6703 Sail.Values <> mword def
+R6707:6709 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R6710:6713 riscv_extras <> size:125 var
+binder 6695:6695 <> v:128
+R6734:6738 Sail.Prompt_monad <> monad ind
+R6740:6741 riscv_extras <> rv:122 var
+R6743:6746 Coq.Init.Datatypes <> bool ind
+R6748:6748 riscv_extras <> e:123 var
+R6753:6761 Sail.Prompt_monad <> write_mem def
+R6806:6806 riscv_extras <> v:128 var
+R6801:6804 riscv_extras <> size:125 var
+R6796:6799 riscv_extras <> addr:127 var
+R6787:6794 riscv_extras <> addrsize:124 var
+R6763:6785 Sail.Instr_kinds <> Write_RISCV_conditional constr
+def 6820:6843 <> MEMw_conditional_release
+binder 6846:6847 <> rv:129
+binder 6849:6849 <> e:130
+binder 6852:6859 <> addrsize:131
+binder 6861:6864 <> size:132
+R6881:6885 Sail.Values <> mword def
+R6887:6894 riscv_extras <> addrsize:131 var
+binder 6867:6872 <> hexRAM:133
+binder 6874:6877 <> addr:134
+R6902:6906 Sail.Values <> mword def
+R6910:6912 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R6913:6916 riscv_extras <> size:132 var
+binder 6898:6898 <> v:135
+R6929:6933 Sail.Prompt_monad <> monad ind
+R6935:6936 riscv_extras <> rv:129 var
+R6938:6941 Coq.Init.Datatypes <> bool ind
+R6943:6943 riscv_extras <> e:130 var
+R6948:6956 Sail.Prompt_monad <> write_mem def
+R7009:7009 riscv_extras <> v:135 var
+R7004:7007 riscv_extras <> size:132 var
+R6999:7002 riscv_extras <> addr:134 var
+R6990:6997 riscv_extras <> addrsize:131 var
+R6958:6988 Sail.Instr_kinds <> Write_RISCV_conditional_release constr
+def 7023:7053 <> MEMw_conditional_strong_release
+binder 7056:7057 <> rv:136
+binder 7059:7059 <> e:137
+binder 7062:7069 <> addrsize:138
+binder 7071:7074 <> size:139
+R7091:7095 Sail.Values <> mword def
+R7097:7104 riscv_extras <> addrsize:138 var
+binder 7077:7082 <> hexRAM:140
+binder 7084:7087 <> addr:141
+R7112:7116 Sail.Values <> mword def
+R7120:7122 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R7123:7126 riscv_extras <> size:139 var
+binder 7108:7108 <> v:142
+R7132:7136 Sail.Prompt_monad <> monad ind
+R7138:7139 riscv_extras <> rv:136 var
+R7141:7144 Coq.Init.Datatypes <> bool ind
+R7146:7146 riscv_extras <> e:137 var
+R7151:7159 Sail.Prompt_monad <> write_mem def
+R7219:7219 riscv_extras <> v:142 var
+R7214:7217 riscv_extras <> size:139 var
+R7209:7212 riscv_extras <> addr:141 var
+R7200:7207 riscv_extras <> addrsize:138 var
+R7161:7198 Sail.Instr_kinds <> Write_RISCV_conditional_strong_release constr
+def 7234:7248 <> shift_bits_left
+binder 7251:7251 <> a:143
+binder 7253:7253 <> b:144
+R7261:7265 Sail.Values <> mword def
+R7267:7267 riscv_extras <> a:143 var
+binder 7257:7257 <> v:145
+R7275:7279 Sail.Values <> mword def
+R7281:7281 riscv_extras <> b:144 var
+binder 7271:7271 <> n:146
+R7286:7290 Sail.Values <> mword def
+R7292:7292 riscv_extras <> a:143 var
+R7299:7304 Sail.Operators_mwords <> shiftl def
+R7309:7320 Sail.Values <> int_of_mword def
+R7328:7328 riscv_extras <> n:146 var
+R7322:7326 Coq.Init.Datatypes <> false constr
+R7306:7306 riscv_extras <> v:145 var
+def 7344:7359 <> shift_bits_right
+binder 7362:7362 <> a:147
+binder 7364:7364 <> b:148
+R7372:7376 Sail.Values <> mword def
+R7378:7378 riscv_extras <> a:147 var
+binder 7368:7368 <> v:149
+R7386:7390 Sail.Values <> mword def
+R7392:7392 riscv_extras <> b:148 var
+binder 7382:7382 <> n:150
+R7397:7401 Sail.Values <> mword def
+R7403:7403 riscv_extras <> a:147 var
+R7410:7415 Sail.Operators_mwords <> shiftr def
+R7420:7431 Sail.Values <> int_of_mword def
+R7439:7439 riscv_extras <> n:150 var
+R7433:7437 Coq.Init.Datatypes <> false constr
+R7417:7417 riscv_extras <> v:149 var
+def 7455:7476 <> shift_bits_right_arith
+binder 7479:7479 <> a:151
+binder 7481:7481 <> b:152
+R7489:7493 Sail.Values <> mword def
+R7495:7495 riscv_extras <> a:151 var
+binder 7485:7485 <> v:153
+R7503:7507 Sail.Values <> mword def
+R7509:7509 riscv_extras <> b:152 var
+binder 7499:7499 <> n:154
+R7514:7518 Sail.Values <> mword def
+R7520:7520 riscv_extras <> a:151 var
+R7527:7538 Sail.Operators_mwords <> arith_shiftr def
+R7543:7554 Sail.Values <> int_of_mword def
+R7562:7562 riscv_extras <> n:154 var
+R7556:7560 Coq.Init.Datatypes <> false constr
+R7540:7540 riscv_extras <> v:153 var
+def 7627:7639 <> internal_pick
+binder 7642:7643 <> rv:155
+binder 7645:7645 <> a:156
+binder 7647:7647 <> e:157
+R7656:7659 Coq.Init.Datatypes <> list ind
+R7661:7661 riscv_extras <> a:156 var
+binder 7651:7652 <> vs:158
+R7666:7670 Sail.Prompt_monad <> monad ind
+R7672:7673 riscv_extras <> rv:155 var
+R7675:7675 riscv_extras <> a:156 var
+R7677:7677 riscv_extras <> e:157 var
+R7688:7689 riscv_extras <> vs:158 var
+R7700:7701 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
+R7708:7714 Sail.Prompt_monad <> returnm def
+R7725:7728 Sail.Prompt_monad <> Fail constr
+def 7776:7791 <> undefined_string
+binder 7794:7795 <> rv:160
+binder 7797:7797 <> e:161
+R7803:7806 Coq.Init.Datatypes <> unit ind
+R7811:7815 Sail.Prompt_monad <> monad ind
+R7817:7818 riscv_extras <> rv:160 var
+R7820:7825 Coq.Strings.String <> string ind
+R7827:7827 riscv_extras <> e:161 var
+R7832:7838 Sail.Prompt_monad <> returnm def
+def 7862:7875 <> undefined_unit
+binder 7878:7879 <> rv:162
+binder 7881:7881 <> e:163
+R7887:7890 Coq.Init.Datatypes <> unit ind
+R7895:7899 Sail.Prompt_monad <> monad ind
+R7901:7902 riscv_extras <> rv:162 var
+R7904:7907 Coq.Init.Datatypes <> unit ind
+R7909:7909 riscv_extras <> e:163 var
+R7914:7920 Sail.Prompt_monad <> returnm def
+R7922:7923 Coq.Init.Datatypes <> tt constr
+def 7937:7949 <> undefined_int
+binder 7952:7953 <> rv:164
+binder 7955:7955 <> e:165
+R7961:7964 Coq.Init.Datatypes <> unit ind
+R7969:7973 Sail.Prompt_monad <> monad ind
+R7975:7976 riscv_extras <> rv:164 var
+R7978:7978 Coq.Numbers.BinNums <> Z ind
+R7980:7980 riscv_extras <> e:165 var
+R7985:7991 Sail.Prompt_monad <> returnm def
+R7996:7997 Sail.Values <> ii def
+def 8097:8112 <> undefined_vector
+binder 8115:8116 <> rv:166
+binder 8118:8118 <> a:167
+binder 8120:8120 <> e:168
+binder 8123:8125 <> len:169
+R8132:8132 riscv_extras <> a:167 var
+binder 8128:8128 <> u:170
+R8137:8145 Sail.Values <> ArithFact class
+R8151:8155 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R8148:8150 riscv_extras <> len:169 var
+binder 8137:8157 <> H:171
+R8162:8166 Sail.Prompt_monad <> monad ind
+R8168:8169 riscv_extras <> rv:166 var
+R8172:8174 Sail.Values <> vec def
+R8176:8176 riscv_extras <> a:167 var
+R8178:8180 riscv_extras <> len:169 var
+R8183:8183 riscv_extras <> e:168 var
+R8188:8194 Sail.Prompt_monad <> returnm def
+R8197:8204 Sail.Values <> vec_init def
+R8208:8210 riscv_extras <> len:169 var
+R8206:8206 riscv_extras <> u:170 var
+def 8316:8334 <> undefined_bitvector
+binder 8337:8338 <> rv:172
+binder 8340:8340 <> e:173
+binder 8343:8345 <> len:174
+R8349:8357 Sail.Values <> ArithFact class
+R8363:8367 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R8360:8362 riscv_extras <> len:174 var
+binder 8349:8369 <> H:175
+R8374:8378 Sail.Prompt_monad <> monad ind
+R8380:8381 riscv_extras <> rv:172 var
+R8384:8388 Sail.Values <> mword def
+R8390:8392 riscv_extras <> len:174 var
+R8395:8395 riscv_extras <> e:173 var
+R8400:8406 Sail.Prompt_monad <> returnm def
+R8409:8420 Sail.Values <> mword_of_int def
+def 8523:8536 <> undefined_bits
+binder 8539:8540 <> rv:176
+binder 8542:8542 <> e:177
+R8549:8567 riscv_extras <> undefined_bitvector def
+R8569:8570 riscv_extras <> rv:176 var
+R8572:8572 riscv_extras <> e:177 var
+def 8586:8598 <> undefined_bit
+binder 8601:8602 <> rv:178
+binder 8604:8604 <> e:179
+R8610:8613 Coq.Init.Datatypes <> unit ind
+R8618:8622 Sail.Prompt_monad <> monad ind
+R8624:8625 riscv_extras <> rv:178 var
+R8627:8630 Sail.Values <> bitU ind
+R8632:8632 riscv_extras <> e:179 var
+R8637:8643 Sail.Prompt_monad <> returnm def
+R8645:8646 Sail.Values <> BU constr
+def 8755:8769 <> undefined_range
+binder 8772:8773 <> rv:180
+binder 8775:8775 <> e:181
+binder 8778:8778 <> i:182
+binder 8780:8780 <> j:183
+R8784:8792 Sail.Values <> ArithFact class
+R8796:8800 Coq.ZArith.BinInt <> ::Z_scope:x_'<=?'_x not
+R8795:8795 riscv_extras <> i:182 var
+R8801:8801 riscv_extras <> j:183 var
+binder 8784:8802 <> H:184
+R8807:8811 Sail.Prompt_monad <> monad ind
+R8813:8814 riscv_extras <> rv:180 var
+R8816:8816 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R8818:8820 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R8822:8824 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R8850:8850 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R8821:8821 Coq.Numbers.BinNums <> Z ind
+binder 8817:8817 <> z:185
+R8825:8833 Sail.Values <> ArithFact class
+R8837:8841 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
+R8843:8847 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
+R8836:8836 riscv_extras <> i:182 var
+R8842:8842 riscv_extras <> z:185 var
+R8842:8842 riscv_extras <> z:185 var
+R8848:8848 riscv_extras <> j:183 var
+R8852:8852 riscv_extras <> e:181 var
+R8857:8863 Sail.Prompt_monad <> returnm def
+R8866:8873 Sail.Values <> build_ex def
+R8875:8875 riscv_extras <> i:182 var
+def 8890:8903 <> undefined_atom
+binder 8906:8907 <> rv:186
+binder 8909:8909 <> e:187
+binder 8912:8912 <> i:188
+R8916:8920 Sail.Prompt_monad <> monad ind
+R8922:8923 riscv_extras <> rv:186 var
+R8925:8925 Coq.Numbers.BinNums <> Z ind
+R8927:8927 riscv_extras <> e:187 var
+R8932:8938 Sail.Prompt_monad <> returnm def
+R8940:8940 riscv_extras <> i:188 var
+def 8954:8966 <> undefined_nat
+binder 8969:8970 <> rv:189
+binder 8972:8972 <> e:190
+R8978:8981 Coq.Init.Datatypes <> unit ind
+R8986:8990 Sail.Prompt_monad <> monad ind
+R8992:8993 riscv_extras <> rv:189 var
+R8995:8995 Coq.Numbers.BinNums <> Z ind
+R8997:8997 riscv_extras <> e:190 var
+R9002:9008 Sail.Prompt_monad <> returnm def
+R9013:9014 Sail.Values <> ii def
+def 9030:9033 <> skip
+binder 9036:9037 <> rv:191
+binder 9039:9039 <> e:192
+R9045:9048 Coq.Init.Datatypes <> unit ind
+R9053:9057 Sail.Prompt_monad <> monad ind
+R9059:9060 riscv_extras <> rv:191 var
+R9062:9065 Coq.Init.Datatypes <> unit ind
+R9067:9067 riscv_extras <> e:192 var
+R9072:9078 Sail.Prompt_monad <> returnm def
+R9080:9081 Coq.Init.Datatypes <> tt constr
+def 9132:9140 <> elf_entry
+R9145:9148 Coq.Init.Datatypes <> unit ind
+R9153:9153 Coq.Numbers.BinNums <> Z ind
+def 9247:9256 <> print_bits
+binder 9259:9259 <> n:193
+binder 9262:9264 <> msg:194
+R9272:9276 Sail.Values <> mword def
+R9278:9278 riscv_extras <> n:193 var
+binder 9267:9268 <> bs:195
+R9284:9296 Sail.Values <> prerr_endline def
+R9302:9306 Coq.Strings.String <> ::string_scope:x_'++'_x not
+R9324:9324 Coq.Strings.String <> ::string_scope:x_'++'_x not
+R9299:9301 riscv_extras <> msg:194 var
+R9307:9320 Sail.Operators_mwords <> string_of_bits def
+R9322:9323 riscv_extras <> bs:195 var
+def 9378:9388 <> get_time_ns
+R9393:9396 Coq.Init.Datatypes <> unit ind
+R9401:9401 Coq.Numbers.BinNums <> Z ind
+def 9548:9553 <> eq_bit
+R9560:9563 Sail.Values <> bitU ind
+binder 9556:9556 <> x:196
+R9571:9574 Sail.Values <> bitU ind
+binder 9567:9567 <> y:197
+R9579:9582 Coq.Init.Datatypes <> bool ind
+R9598:9598 riscv_extras <> y:197 var
+R9595:9595 riscv_extras <> x:196 var
+R9609:9610 Sail.Values <> B0 constr
+R9613:9614 Sail.Values <> B0 constr
+R9619:9622 Coq.Init.Datatypes <> true constr
+R9628:9629 Sail.Values <> B1 constr
+R9632:9633 Sail.Values <> B1 constr
+R9638:9641 Coq.Init.Datatypes <> true constr
+R9647:9648 Sail.Values <> BU constr
+R9651:9652 Sail.Values <> BU constr
+R9657:9660 Coq.Init.Datatypes <> true constr
+R9673:9677 Coq.Init.Datatypes <> false constr
+R9702:9708 Coq.ZArith.Zeuclid <> <> lib
+def 9722:9734 <> euclid_modulo
+R9743:9743 Coq.Numbers.BinNums <> Z ind
+binder 9737:9737 <> m:200
+binder 9739:9739 <> n:201
+R9748:9756 Sail.Values <> ArithFact class
+R9760:9763 Coq.ZArith.BinInt <> ::Z_scope:x_'>?'_x not
+R9759:9759 riscv_extras <> n:201 var
+binder 9748:9765 <> H:202
+R9770:9770 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R9772:9774 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R9776:9778 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R9806:9806 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R9775:9775 Coq.Numbers.BinNums <> Z ind
+binder 9771:9771 <> z:203
+R9779:9787 Sail.Values <> ArithFact class
+R9791:9795 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
+R9797:9801 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
+R9796:9796 riscv_extras <> z:203 var
+R9796:9796 riscv_extras <> z:203 var
+R9803:9803 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not
+R9802:9802 riscv_extras <> n:201 var
+R9833:9846 Coq.ZArith.Zeuclid ZEuclid modulo def
+R9815:9820 Coq.Init.Specif <> existT constr
+R9833:9846 Coq.ZArith.Zeuclid ZEuclid modulo def
+R9815:9820 Coq.Init.Specif <> existT constr
+R9939:9941 Coq.Init.Logic <> ::type_scope:x_'='_x not
+R9932:9936 Coq.ZArith.BinInt Z abs def
+R9939:9941 Coq.Init.Logic <> ::type_scope:x_'='_x not
+R9932:9936 Coq.ZArith.BinInt Z abs def
+R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
+R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
+R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
+R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
+R10013:10034 Coq.ZArith.Zeuclid ZEuclid mod_always_pos thm
+R10013:10034 Coq.ZArith.Zeuclid ZEuclid mod_always_pos thm
+def 10107:10115 <> mults_vec
+binder 10118:10118 <> n:204
+R10126:10130 Sail.Values <> mword def
+R10132:10132 riscv_extras <> n:204 var
+binder 10122:10122 <> l:205
+R10140:10144 Sail.Values <> mword def
+R10146:10146 riscv_extras <> n:204 var
+binder 10136:10136 <> r:206
+R10151:10155 Sail.Values <> mword def
+R10159:10161 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R10162:10162 riscv_extras <> n:204 var
+R10168:10176 Sail.Operators_mwords <> mults_vec def
+R10180:10180 riscv_extras <> r:206 var
+R10178:10178 riscv_extras <> l:205 var
+def 10194:10201 <> mult_vec
+binder 10204:10204 <> n:207
+R10212:10216 Sail.Values <> mword def
+R10218:10218 riscv_extras <> n:207 var
+binder 10208:10208 <> l:208
+R10226:10230 Sail.Values <> mword def
+R10232:10232 riscv_extras <> n:207 var
+binder 10222:10222 <> r:209
+R10237:10241 Sail.Values <> mword def
+R10245:10247 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
+R10248:10248 riscv_extras <> n:207 var
+R10254:10261 Sail.Operators_mwords <> mult_vec def
+R10265:10265 riscv_extras <> r:209 var
+R10263:10263 riscv_extras <> l:208 var
+def 10281:10293 <> print_endline
+R10298:10303 Coq.Strings.String <> string ind
+R10308:10311 Coq.Init.Datatypes <> unit ind
+R10316:10317 Coq.Init.Datatypes <> tt constr
+def 10331:10343 <> prerr_endline
+R10348:10353 Coq.Strings.String <> string ind
+R10358:10361 Coq.Init.Datatypes <> unit ind
+R10366:10367 Coq.Init.Datatypes <> tt constr
+def 10381:10392 <> prerr_string
+R10397:10402 Coq.Strings.String <> string ind
+R10407:10410 Coq.Init.Datatypes <> unit ind
+R10415:10416 Coq.Init.Datatypes <> tt constr
+def 10430:10436 <> putchar
+binder 10439:10439 <> T:210
+R10445:10445 riscv_extras <> T:210 var
+R10450:10453 Coq.Init.Datatypes <> unit ind
+R10458:10459 Coq.Init.Datatypes <> tt constr
+R10470:10482 Coq.Numbers.DecimalString <> <> lib
+def 10496:10508 <> string_of_int
+binder 10510:10510 <> z:211
+R10515:10549 Coq.Numbers.DecimalString NilZero string_of_int def
+R10552:10559 Coq.ZArith.BinInt Z to_int def
+R10561:10561 riscv_extras <> z:211 var
+ax 10572:10595 <> sys_enable_writable_misa
+R10603:10606 Coq.Init.Logic <> ::type_scope:x_'->'_x not
+R10599:10602 Coq.Init.Datatypes <> unit ind
+R10607:10610 Coq.Init.Datatypes <> bool ind
+ax 10619:10632 <> sys_enable_rvc
+R10640:10643 Coq.Init.Logic <> ::type_scope:x_'->'_x not
+R10636:10639 Coq.Init.Datatypes <> unit ind
+R10644:10647 Coq.Init.Datatypes <> bool ind
+ax 10656:10671 <> sys_enable_fdext
+R10679:10682 Coq.Init.Logic <> ::type_scope:x_'->'_x not
+R10675:10678 Coq.Init.Datatypes <> unit ind
+R10683:10686 Coq.Init.Datatypes <> bool ind
+ax 10695:10709 <> sys_enable_next
+R10717:10720 Coq.Init.Logic <> ::type_scope:x_'->'_x not
+R10713:10716 Coq.Init.Datatypes <> unit ind
+R10721:10724 Coq.Init.Datatypes <> bool ind
+prf 10868:10888 <> n_leading_spaces_fact
+binder 10891:10894 <> w__0:216
+R10910:10913 Coq.Init.Logic <> ::type_scope:x_'->'_x not
+R10905:10908 Coq.ZArith.BinInt <> ::Z_scope:x_'>='_x not
+R10901:10904 riscv_extras <> w__0:216 var
+R10914:10920 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
+R10933:10934 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
+R10932:10932 Coq.Numbers.BinNums <> Z ind
+binder 10921:10928 <> ex17629_:217
+R10958:10961 Coq.Init.Logic <> ::type_scope:x_'/\'_x not
+R10943:10945 Coq.Init.Logic <> ::type_scope:x_'='_x not
+R10936:10938 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not
+R10939:10942 riscv_extras <> w__0:216 var
+R10947:10949 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not
+R10950:10957 riscv_extras <> ex17629_:217 var
+R10963:10966 Coq.ZArith.BinInt <> ::Z_scope:x_'<='_x not
+R10967:10974 riscv_extras <> ex17629_:217 var
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
new file mode 100644
index 0000000..15ac8c7
--- /dev/null
+++ b/handwritten_support/riscv_extras.lem
@@ -0,0 +1,164 @@
+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 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/riscv_extras.v b/handwritten_support/riscv_extras.v
new file mode 100644
index 0000000..4b069ec
--- /dev/null
+++ b/handwritten_support/riscv_extras.v
@@ -0,0 +1,154 @@
+Require Import Sail.Base.
+Require Import String.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z.
+
+Definition MEM_fence_rw_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_rw tt).
+Definition MEM_fence_r_rw  {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_rw tt).
+Definition MEM_fence_r_r   {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_r tt).
+Definition MEM_fence_rw_w  {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_w tt).
+Definition MEM_fence_w_w   {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_w tt).
+Definition MEM_fence_w_rw  {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_rw tt).
+Definition MEM_fence_rw_r  {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_r tt).
+Definition MEM_fence_r_w   {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_w tt).
+Definition MEM_fence_w_r   {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_r tt).
+Definition MEM_fence_tso   {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_tso tt).
+Definition MEM_fence_i     {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_i tt).
+(*
+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
+*)
+Definition MEMea {rv a e} addrsize (addr : mword a) size                     : monad rv unit e := write_mem_ea Write_plain addrsize addr size.
+Definition MEMea_release {rv a e} addrsize (addr : mword a) size             : monad rv unit e := write_mem_ea Write_RISCV_release addrsize addr size.
+Definition MEMea_strong_release {rv a e} addrsize (addr : mword a) size      : monad rv unit e := write_mem_ea Write_RISCV_strong_release addrsize addr size.
+Definition MEMea_conditional {rv a e} addrsize (addr : mword a) size         : monad rv unit e := write_mem_ea Write_RISCV_conditional addrsize addr size.
+Definition MEMea_conditional_release {rv a e} addrsize (addr : mword a) size : monad rv unit e := write_mem_ea Write_RISCV_conditional_release addrsize addr size.
+Definition MEMea_conditional_strong_release {rv a e} addrsize (addr : mword a) size : monad rv unit e
+                                          := write_mem_ea Write_RISCV_conditional_strong_release addrsize 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
+*)
+
+Definition MEMr {rv e} addrsize size (hexRAM addr : mword addrsize)                         `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_plain addrsize addr size.
+Definition MEMr_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)                 `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_acquire addrsize addr size.
+Definition MEMr_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)          `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_strong_acquire addrsize addr size.
+Definition MEMr_reserved {rv e} addrsize size (hexRAM addr : mword addrsize)                `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved addrsize addr size.
+Definition MEMr_reserved_acquire {rv e} addrsize size (hexRAM addr : mword addrsize)        `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := read_mem Read_RISCV_reserved_acquire addrsize addr size.
+Definition MEMr_reserved_strong_acquire {rv e} addrsize size (hexRAM addr : mword addrsize) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size)) e := 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
+*)
+
+Definition MEMw {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size))                            : monad rv bool e := write_mem Write_plain addrsize addr size v.
+Definition MEMw_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size))                    : monad rv bool e := write_mem Write_RISCV_release addrsize addr size v.
+Definition MEMw_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size))             : monad rv bool e := write_mem Write_RISCV_strong_release addrsize addr size v.
+Definition MEMw_conditional {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size))                : monad rv bool e := write_mem Write_RISCV_conditional addrsize addr size v.
+Definition MEMw_conditional_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size))        : monad rv bool e := write_mem Write_RISCV_conditional_release addrsize addr size v.
+Definition MEMw_conditional_strong_release {rv e} addrsize size (hexRAM addr : mword addrsize) (v : mword (8 * size)) : monad rv bool e := write_mem Write_RISCV_conditional_strong_release addrsize addr size v.
+
+Definition shift_bits_left {a b} (v : mword a) (n : mword b) : mword a :=
+  shiftl v (int_of_mword false n).
+
+Definition shift_bits_right {a b} (v : mword a) (n : mword b) : mword a :=
+  shiftr v (int_of_mword false n).
+
+Definition shift_bits_right_arith {a b} (v : mword a) (n : mword b) : mword a :=
+  arith_shiftr v (int_of_mword false n).
+
+(* Use constants for undefined values for now *)
+Definition internal_pick {rv a e} (vs : list a) : monad rv a e :=
+match vs with
+| (h::_) => returnm h
+| _ => Fail "empty list in internal_pick"
+end.
+Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string.
+Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
+Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
+(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
+Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >=? 0)} : monad rv (vec a len) e := returnm (vec_init u len).
+(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
+Definition undefined_bitvector {rv e} len `{ArithFact (len >=? 0)} : monad rv (mword len) e := returnm (mword_of_int 0).
+(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
+Definition undefined_bits {rv e} := @undefined_bitvector rv e.
+Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU.
+(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*)
+Definition undefined_range {rv e} i j `{ArithFact (i <=? j)} : monad rv {z : Z & ArithFact (i <=? z <=? j)} e := returnm (build_ex i).
+Definition undefined_atom {rv e} i : monad rv Z e := returnm i.
+Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
+
+Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt.
+
+(*val elf_entry : unit -> integer*)
+Definition elf_entry (_:unit) : Z := 0.
+(*declare ocaml target_rep function elf_entry := `Elf_loader.elf_entry`*)
+
+Definition print_bits {n} msg (bs : mword n) := prerr_endline (msg ++ (string_of_bits bs)).
+
+(*val get_time_ns : unit -> integer*)
+Definition get_time_ns (_:unit) : Z := 0.
+(*declare ocaml target_rep function get_time_ns := `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))`*)
+
+Definition eq_bit (x : bitU) (y : bitU) : bool :=
+  match x, y with
+  | B0, B0 => true
+  | B1, B1 => true
+  | BU, BU => true
+  | _,_ => false
+  end.
+
+Require Import Zeuclid.
+Definition euclid_modulo (m n : Z) `{ArithFact (n >? 0)} : {z : Z & ArithFact (0 <=? z <=? n-1)}.
+apply existT with (x := ZEuclid.modulo m n).
+constructor.
+destruct H.
+unbool_comparisons.
+unbool_comparisons_goal.
+assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. }
+rewrite <- H at 3.
+lapply (ZEuclid.mod_always_pos m n); omega.
+Qed.
+
+(* Override the more general version *)
+
+Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r.
+Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r.
+
+
+Definition print_endline (_:string) : unit := tt.
+Definition prerr_endline (_:string) : unit := tt.
+Definition prerr_string (_:string) : unit := tt.
+Definition putchar {T} (_:T) : unit := tt.
+Require DecimalString.
+Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
+
+Axiom sys_enable_writable_misa : unit -> bool.
+Axiom sys_enable_rvc : unit -> bool.
+Axiom sys_enable_fdext : unit -> bool.
+Axiom sys_enable_next : unit -> bool.
+
+(* The constraint solver can do this itself, but a Coq bug puts
+   anonymous_subproof into the term instead of an actual subproof. *)
+Lemma n_leading_spaces_fact {w__0} :
+  w__0 >= 0 -> exists ex17629_ : Z, 1 + w__0 = 1 + ex17629_ /\ 0 <= ex17629_.
+intro.
+exists w__0.
+omega.
+Qed.
+Hint Resolve n_leading_spaces_fact : sail.
diff --git a/handwritten_support/riscv_extras.vo b/handwritten_support/riscv_extras.vo
new file mode 100644
index 0000000..995df56
--- /dev/null
+++ b/handwritten_support/riscv_extras.vo
diff --git a/handwritten_support/riscv_extras.vok b/handwritten_support/riscv_extras.vok
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/handwritten_support/riscv_extras.vok
diff --git a/handwritten_support/riscv_extras.vos b/handwritten_support/riscv_extras.vos
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/handwritten_support/riscv_extras.vos
diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem
new file mode 100644
index 0000000..12cfe00
--- /dev/null
+++ b/handwritten_support/riscv_extras_fdext.lem
@@ -0,0 +1,125 @@
+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_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_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_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_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_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f64 _ _ = ()
+
+val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f32 _ _ = ()
+
+
+val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_lt _ _ = ()
+
+val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_le _ _ = ()
+
+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_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_le _ _ = ()
+
+val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_eq _ _ = ()
diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem
new file mode 100644
index 0000000..c1c99ed
--- /dev/null
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -0,0 +1,156 @@
+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_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 = ()