Make sure everything builds correctly

Move updated 0.11 lem files from Shaked's commit into their own directory

Remove the 0.7.1 lem directory that performed a similar purpose during the prompt monad changes

Re-add model changes from Shaked's commit with a feature flag

2 files changed, 79 insertions, 45 deletions

diff --git a/handwritten_support/0.7.1/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem
index c1a52c9..f4ade26 100644
--- a/handwritten_support/0.7.1/riscv_extras.lem
+++ b/handwritten_support/0.11/riscv_extras.lem
@@ -8,17 +8,17 @@ 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
+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
@@ -27,13 +27,13 @@ val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => bitvector 'a
 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 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
+                                          = 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
@@ -42,22 +42,26 @@ val MEMr_reserved                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => inte
 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_val 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
+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 = ()
@@ -67,6 +71,14 @@ 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 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`
@@ -99,6 +111,10 @@ 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`
@@ -135,3 +151,6 @@ 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.7.1/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem
index c1a52c9..ac70ee5 100644
--- a/handwritten_support/0.7.1/riscv_extras_sequential.lem
+++ b/handwritten_support/0.11/riscv_extras_sequential.lem
@@ -8,17 +8,17 @@ 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
+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
@@ -52,7 +52,7 @@ let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV
 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_val 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
@@ -67,6 +67,14 @@ 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 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`
@@ -99,6 +107,10 @@ 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`
@@ -135,3 +147,6 @@ 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 = ()