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.

4 files changed, 461 insertions, 0 deletions

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 = ()