Adapt to memory interface of Lem shallow embeddingmonads

Data and tags are expected to be read/written together.

8 files changed, 211 insertions, 161 deletions

diff --git a/Makefile b/Makefile
index 9f6c68f..377ed66 100644
--- a/Makefile
+++ b/Makefile
@@ -169,7 +169,7 @@ endif
 
 generated_definitions/lem/riscv.lem: $(SAIL_SRCS) Makefile
 	mkdir -p generated_definitions/lem
-	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS)
+	$(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -o riscv -lem_mwords -lem_lib Riscv_extras -auto_mono -mono_rewrites $(SAIL_LIB_DIR)/smt.sail $(SAIL_LIB_DIR)/mono_rewrites.sail $(SAIL_SRCS)
 
 generated_definitions/lem/riscv_sequential.lem: $(SAIL_SRCS) Makefile
 	mkdir -p generated_definitions/lem
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index ed572be..993ab4b 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -6,8 +6,6 @@ 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
@@ -20,12 +18,12 @@ 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
+val MEMea                            : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e
+val MEMea_release                    : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e
+val MEMea_strong_release             : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional_release        : forall 'rv 'a 'e. Size 'a => mword 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => mword '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
@@ -35,35 +33,44 @@ let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_
 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 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 addr size
-let MEMw_release addrsize size hexRAM addr                    = write_mem Write_RISCV_release addr size
-let MEMw_strong_release addrsize size hexRAM addr             = write_mem Write_RISCV_strong_release addr size
-let MEMw_conditional addrsize size hexRAM addr                = write_mem Write_RISCV_conditional addr size
-let MEMw_conditional_release addrsize size hexRAM addr        = write_mem Write_RISCV_conditional_release addr size
-let MEMw_conditional_strong_release addrsize size hexRAM addr = write_mem Write_RISCV_conditional_strong_release addr size
-
-val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
+val read_memt_bool : forall 'rv 'a 'b 'e. Size 'a, Size 'b => read_kind -> mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e
+let read_memt_bool rk addr size =
+  read_memt rk addr size >>= fun (data, tag) ->
+  maybe_fail "read_memt" (bool_of_bitU tag) >>= fun tag ->
+  return (tag, data)
+
+val ReadMemT                         : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e
+val ReadMemT_acquire                 : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e
+val ReadMemT_strong_acquire          : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e
+val ReadMemT_reserved                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e
+val ReadMemT_reserved_acquire        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e
+val ReadMemT_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> monad 'rv (bool * mword 'b) 'e
+
+let ReadMemT addr size                         = read_memt_bool Read_plain addr size
+let ReadMemT_acquire addr size                 = read_memt_bool Read_RISCV_acquire addr size
+let ReadMemT_strong_acquire addr size          = read_memt_bool Read_RISCV_strong_acquire addr size
+let ReadMemT_reserved addr size                = read_memt_bool Read_RISCV_reserved addr size
+let ReadMemT_reserved_acquire addr size        = read_memt_bool Read_RISCV_reserved_acquire addr size
+let ReadMemT_reserved_strong_acquire addr size = read_memt_bool Read_RISCV_reserved_strong_acquire addr size
+
+val write_memt_bool : forall 'rv 'a 'b 'e. Size 'a, Size 'b => write_kind -> mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e
+let write_memt_bool wk addr size tag data = write_memt wk addr size data (bitU_of_bool tag)
+
+val WriteMemT                            : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e
+val WriteMemT_release                    : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e
+val WriteMemT_strong_release             : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e
+val WriteMemT_conditional                : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e
+val WriteMemT_conditional_release        : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e
+val WriteMemT_conditional_strong_release : forall 'rv 'a 'b 'e. Size 'a, Size 'b => mword 'a -> integer -> bool -> mword 'b -> monad 'rv bool 'e
+
+let WriteMemT addr size tag data                            = write_memt_bool Write_plain addr size tag data
+let WriteMemT_release addr size tag data                    = write_memt_bool Write_RISCV_release addr size tag data
+let WriteMemT_strong_release addr size tag data             = write_memt_bool Write_RISCV_strong_release addr size tag data
+let WriteMemT_conditional addr size tag data                = write_memt_bool Write_RISCV_conditional addr size tag data
+let WriteMemT_conditional_release addr size tag data        = write_memt_bool Write_RISCV_conditional_release addr size tag data
+let WriteMemT_conditional_strong_release addr size tag data = write_memt_bool Write_RISCV_conditional_strong_release addr size tag data
+
+val load_reservation : forall 'a. Size 'a => mword 'a -> unit
 let load_reservation addr = ()
 
 let speculate_conditional_success () = excl_result ()
@@ -71,27 +78,27 @@ let speculate_conditional_success () = excl_result ()
 let match_reservation _ = true
 let cancel_reservation () = ()
 
-val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
+val plat_ram_base : forall 'a. Size 'a => unit -> mword '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
+val plat_ram_size : forall 'a. Size 'a => unit -> mword '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
+val plat_rom_base : forall 'a. Size 'a => unit -> mword '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
+val plat_rom_size : forall 'a. Size 'a => unit -> mword '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
+val plat_clint_base : forall 'a. Size 'a => unit -> mword '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
+val plat_clint_size : forall 'a. Size 'a => unit -> mword 'a
 let plat_clint_size () = wordFromInteger 0
 declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
 
@@ -111,21 +118,21 @@ 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
+val plat_htif_tohost : forall 'a. Size 'a => unit -> mword '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
+val plat_term_write : forall 'a. Size 'a => mword '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
+val plat_term_read : forall 'a. Size 'a => unit -> mword '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
+val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'b -> mword '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
+val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => mword 'a -> mword 'b -> mword 'a
 let shift_bits_left v m = shiftl v (uint m)
 
 val print_string : string -> string -> unit
@@ -134,8 +141,8 @@ let print_string msg s = () (* print_endline (msg ^ s) *)
 val prerr_string : string -> string -> unit
 let prerr_string msg s = prerr_endline (msg ^ s)
 
-val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
+val prerr_bits : forall 'a. Size 'a => string -> mword '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
+val print_bits : forall 'a. Size 'a => string -> mword 'a -> unit
 let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
diff --git a/model/cheri_insts.sail b/model/cheri_insts.sail
index 7c3cdee..2da42a7 100644
--- a/model/cheri_insts.sail
+++ b/model/cheri_insts.sail
@@ -856,7 +856,7 @@ function clause execute(CJALR(cd, cb)) =
   };
 }
 
-val handle_load_data_via_cap : (regbits, bits(6), Capability, uint64, bool, word_width) -> bool effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val handle_load_data_via_cap : (regbits, bits(6), Capability, uint64, bool, word_width) -> bool effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function handle_load_data_via_cap(rd, cs, cap_val, vaddr, is_unsigned, width) = {
   let (base, top) = getCapBounds(cap_val);
   let vaddrBits = to_bits(xlen, vaddr);
@@ -949,7 +949,7 @@ function clause execute (CLoadCapCap(rd, cs)) =
   handle_load_cap_via_cap(rd, 0b0 @ cs, cap_val, vaddr)
 }
 
-val handle_store_data_via_cap : (regbits, regbits, Capability, uint64, word_width) -> bool effect {eamem, escape, rmem, rreg, wmv, wmvt, wreg}
+val handle_store_data_via_cap : (regbits, regbits, Capability, uint64, word_width) -> bool effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function handle_store_data_via_cap(rs, cs, cap_val, vaddr, width) = {
   let (base, top) = getCapBounds(cap_val);
   let vaddrBits = to_bits(xlen, vaddr);
@@ -1012,7 +1012,7 @@ function clause execute (CStoreCap(rs, cs, width)) =
   handle_store_data_via_cap(rs, cs, cap_val, vaddr, width)
 }
 
-val handle_store_cap_via_cap : (regbits, regbits, Capability, uint64) -> bool effect {eamem, escape, rmem, rreg, wmv, wreg, wmvt}
+val handle_store_cap_via_cap : (regbits, regbits, Capability, uint64) -> bool effect {eamem, escape, rmem, rmemt, rreg, wmv, wreg, wmvt}
 function handle_store_cap_via_cap(rs, cs, cap_val, vaddr) = {
   let (base, top) = getCapBounds(cap_val);
   let vaddrBits = to_bits(xlen, vaddr);
diff --git a/model/cheri_prelude_128.sail b/model/cheri_prelude_128.sail
index 4d43f7e..71dddbd 100644
--- a/model/cheri_prelude_128.sail
+++ b/model/cheri_prelude_128.sail
@@ -279,9 +279,8 @@ function getCapBounds(c) : Capability -> (uint64, CapLen) = {
   let correction_base = a_top_correction(a3, R3, B3) in
   let correction_top  = a_top_correction(a3, R3, T3) in
   let a_top = (a >> (E + 14)) in
-  let e_zeros = zeros(E) in
-  let base : bits(64) = truncate((a_top + correction_base) @ c.B @ e_zeros, 64) in
-  let top  : bits(65) = truncate((a_top + correction_top)  @ c.T @ e_zeros, 65) in
+  let base : bits(64) = truncate((a_top + correction_base) @ c.B @ zeros(E), 64) in
+  let top  : bits(65) = truncate((a_top + correction_top)  @ c.T @ zeros(E), 65) in
   (unsigned(base), unsigned(top))
 }
 
diff --git a/model/prelude.sail b/model/prelude.sail
index 0f766b4..b2731e1 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -922,74 +922,143 @@ overload min = {min_nat, min_int}
 
 overload max = {max_nat, max_int}
 
-val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+$ifndef FEATURE_IMPLICITS
 
-val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+val zeros_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
+function zeros_implicit () = sail_zeros('n)
+overload zeros = {zeros_implicit, sail_zeros}
 
-val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n)
+function ones_n n = replicate_bits (0b1, n)
 
-val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+val ones_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
+function ones_implicit () = ones_n ('n)
 
-val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm.
-  (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
+overload ones = {ones_implicit, ones_n}
+
+$else
+
+val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
+function zeros_implicit (n) = sail_zeros(n)
+overload zeros = {zeros_implicit, sail_zeros}
+
+val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n)
+function ones_n n = replicate_bits (0b1, n)
+
+val ones_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
+function ones_implicit (n) = ones_n (n)
+
+overload ones = {ones_implicit, ones_n}
+
+$endif
+
+val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
+val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
 
-val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm.
+/* XXX should derive thise form cap_size */
+val tag_align_addr : forall 'n, 4 <= 'n <= 64. bits('n) -> bits('n)
+function tag_align_addr(addr) = [addr with 3..0 = 0x0]
+
+val __WriteRAM = {_: "write_ram"} : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv}
 
-val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv}
-function __RISCV_write (addr, width, data, aq, rl, con) =
+val __WriteMemT = {lem: "WriteMemT"} : forall 'n 'm, 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bits(8 * 'n)) -> bool effect {wmv, wmvt}
+
+function __WriteMemT(addr, width, tag, data) = {
+  let tag_addr = sail_zero_extend(tag_align_addr(addr), 64);
+  MEMw_tag(tag_addr, tag);
+
+  /* If the write crosses a cap_size alignment boundary then we need to write the other tag.
+     Writes greater than cap_size that might span more than two regions are not supported. */
+  let tag_addr2 = sail_zero_extend(tag_align_addr(addr + width - 1), 64);
+  if tag_addr != tag_addr2 then MEMw_tag(tag_addr2, tag);
+
+  __WriteRAM('m, width, zeros(), addr, data);
+}
+
+val __WriteMemT_release = {lem: "WriteMemT_release"} : forall 'n 'm, 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bits(8 * 'n)) -> bool effect {wmv, wmvt}
+
+val __WriteMemT_strong_release = {lem: "WriteMemT_strong_release"} : forall 'n 'm, 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bits(8 * 'n)) -> bool effect {wmv, wmvt}
+
+val __WriteMemT_conditional = {lem: "WriteMemT_conditional"} : forall 'n 'm, 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bits(8 * 'n)) -> bool effect {wmv, wmvt}
+
+val __WriteMemT_conditional_release = {lem: "WriteMemT_conditional_release"} : forall 'n 'm, 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bits(8 * 'n)) -> bool effect {wmv, wmvt}
+
+val __WriteMemT_conditional_strong_release = {lem: "WriteMemT_conditional_strong_release"} : forall 'n 'm, 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bits(8 * 'n)) -> bool effect {wmv, wmvt}
+
+function __WriteMemT_release(addr, width, tag, data)                    = __WriteMemT(addr, width, tag, data)
+function __WriteMemT_strong_release(addr, width, tag, data)             = __WriteMemT(addr, width, tag, data)
+function __WriteMemT_conditional(addr, width, tag, data)                = __WriteMemT(addr, width, tag, data)
+function __WriteMemT_conditional_release(addr, width, tag, data)        = __WriteMemT(addr, width, tag, data)
+function __WriteMemT_conditional_strong_release(addr, width, tag, data) = __WriteMemT(addr, width, tag, data)
+
+val __RISCV_write : forall 'n 'm, 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bits(8 * 'n), bool, bool, bool) -> bool effect {wmv, wmvt}
+function __RISCV_write (addr, width, tag, data, aq, rl, con) =
   match (aq, rl, con) {
-    (false, false, false) => __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data),
-    (false, true,  false) => __WriteRAM_release(64, width, 0x0000_0000_0000_0000, addr, data),
-    (false, false, true)  => __WriteRAM_conditional(64, width, 0x0000_0000_0000_0000, addr, data),
-    (false, true,  true)  => __WriteRAM_conditional_release(64, width, 0x0000_0000_0000_0000, addr, data),
-    (true,  true,  false) => __WriteRAM_strong_release(64, width, 0x0000_0000_0000_0000, addr, data),
-    (true,  true,  true)  => __WriteRAM_conditional_strong_release(64, width, 0x0000_0000_0000_0000, addr, data),
+    (false, false, false) => __WriteMemT(addr, width, tag, data),
+    (false, true,  false) => __WriteMemT_release(addr, width, tag, data),
+    (false, false, true)  => __WriteMemT_conditional(addr, width, tag, data),
+    (false, true,  true)  => __WriteMemT_conditional_release(addr, width, tag, data),
+    (true,  true,  false) => __WriteMemT_strong_release(addr, width, tag, data),
+    (true,  true,  true)  => __WriteMemT_conditional_strong_release(addr, width, tag, data),
     (true,  false, false) => false,
     (true,  false, true)  => false
   }
 
-val __TraceMemoryWrite : forall 'n 'm.
-  (atom('n), bits('m), bits(8 * 'n)) -> unit
-
-val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val __ReadRAM = {_ : "read_ram"} : forall 'n 'm, 'n >= 0.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+val __ReadMemT = {lem: "ReadMemT"} : forall 'n 'm, 'n >= 0 & 4 <= 'm <= 64.
+  (bits('m), atom('n)) -> (bool, bits(8 * 'n)) effect {rmem, rmemt}
 
-val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+function __ReadMemT(addr, width) = {
+  let tag = MEMr_tag(sail_zero_extend(addr, 64));
+  let data = __ReadRAM('m, width, zeros(), addr);
+  (tag, data)
+}
 
-val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+val __ReadMemT_acquire = { lem: "ReadMemT_acquire" } : forall 'n 'm, 'n >= 0 & 4 <= 'm <= 64.
+  (bits('m), atom('n)) -> (bool, bits(8 * 'n)) effect {rmem, rmemt}
 
-val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+val __ReadMemT_strong_acquire = { lem: "ReadMemT_strong_acquire" } : forall 'n 'm, 'n >= 0 & 4 <= 'm <= 64.
+  (bits('m), atom('n)) -> (bool, bits(8 * 'n)) effect {rmem, rmemt}
 
-val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
-  (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+val __ReadMemT_reserved = { lem: "ReadMemT_reserved" } : forall 'n 'm, 'n >= 0 & 4 <= 'm <= 64.
+  (bits('m), atom('n)) -> (bool, bits(8 * 'n)) effect {rmem, rmemt}
+
+val __ReadMemT_reserved_acquire = { lem: "ReadMemT_reserved_acquire" } : forall 'n 'm, 'n >= 0 & 4 <= 'm <= 64.
+  (bits('m), atom('n)) -> (bool, bits(8 * 'n)) effect {rmem, rmemt}
+
+val __ReadMemT_reserved_strong_acquire = { lem: "ReadMemT_reserved_strong_acquire" } : forall 'n 'm, 'n >= 0 & 4 <= 'm <= 64.
+  (bits('m), atom('n)) -> (bool, bits(8 * 'n)) effect {rmem, rmemt}
+
+function __ReadMemT_acquire(addr, width)                 = __ReadMemT(addr, width)
+function __ReadMemT_strong_acquire(addr, width)          = __ReadMemT(addr, width)
+function __ReadMemT_reserved(addr, width)                = __ReadMemT(addr, width)
+function __ReadMemT_reserved_acquire(addr, width)        = __ReadMemT(addr, width)
+function __ReadMemT_reserved_strong_acquire(addr, width) = __ReadMemT(addr, width)
 
-val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem}
-function __RISCV_read (addr, width, aq, rl, res) =
+val __RISCV_read : forall 'n 'm, 'n >= 0 & 4 <= 'm <= 64.
+  (bits('m), atom('n), bool, bool, bool) -> option((bool, bits(8 * 'n))) effect {rmem, rmemt}
+function __RISCV_read(addr, width, aq, rl, res) =
   match (aq, rl, res) {
-    (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, false) => Some(__ReadRAM_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  false) => Some(__ReadRAM_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (false, false, true)  => Some(__ReadRAM_reserved(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  false, true)  => Some(__ReadRAM_reserved_acquire(64, width, 0x0000_0000_0000_0000, addr)),
-    (true,  true,  true)  => Some(__ReadRAM_reserved_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)),
+    (false, false, false) => Some(__ReadMemT_acquire(addr, width)),
+    (true,  false, false) => Some(__ReadMemT_acquire(addr, width)),
+    (true,  true,  false) => Some(__ReadMemT_strong_acquire(addr, width)),
+    (false, false, true)  => Some(__ReadMemT_reserved(addr, width)),
+    (true,  false, true)  => Some(__ReadMemT_reserved_acquire(addr, width)),
+    (true,  true,  true)  => Some(__ReadMemT_reserved_strong_acquire(addr, width)),
     (false, true,  false) => None(),
     (false, true,  true)  => None()
   }
 
-val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
-val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
-
 val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
 
 val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm)
@@ -1108,36 +1177,6 @@ val not = {coq:"negb", _:"not"} : bool -> bool
 val MAX : forall 'n, 'n >= 0 . atom('n) -> atom(2 ^ 'n - 1) effect pure
 function MAX(n) = pow2(n) - 1
 
-$ifndef FEATURE_IMPLICITS
-
-val zeros_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
-function zeros_implicit () = sail_zeros('n)
-overload zeros = {zeros_implicit, sail_zeros}
-
-val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n)
-function ones_n n = replicate_bits (0b1, n)
-
-val ones_implicit : forall 'n, 'n >= 0 . unit -> bits('n)
-function ones_implicit () = ones_n ('n)
-
-overload ones = {ones_implicit, ones_n}
-
-$else
-
-val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
-function zeros_implicit (n) = sail_zeros(n)
-overload zeros = {zeros_implicit, sail_zeros}
-
-val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n)
-function ones_n n = replicate_bits (0b1, n)
-
-val ones_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
-function ones_implicit (n) = ones_n (n)
-
-overload ones = {ones_implicit, ones_n}
-
-$endif
-
 val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 .  (int, atom('n)) -> range(0, 'n - 1)
 
 overload operator % = {modulus}
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 6110ab4..82cbbbc 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -8,21 +8,26 @@ function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool
   unsigned(addr) % width == 0
 
 // only used for actual memory regions, to avoid MMIO effects
-function phys_mem_read forall 'n, 'n >= 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) =
+function phys_mem_read forall 'n, 'n >= 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult((bool, bits(8 * 'n))) =
   match (t, __RISCV_read(addr, width, aq, rl, res)) {
     (Instruction, None()) => MemException(E_Fetch_Access_Fault),
     (Data, None())        => MemException(E_Load_Access_Fault),
-    (_, Some(v))          => { print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
-                               MemValue(v) }
+    (_, Some((tag, v)))   => { print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+                               MemValue((tag, v)) }
   }
 
-function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) =
+function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult((bool, bits(8 * 'n))) =
   /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
-  if   t == Data & within_mmio_readable(addr, width)
-  then mmio_read(addr, width)
-  else if within_phys_mem(addr, width)
-  then phys_mem_read(t, addr, width, aq, rl, res)
-  else MemException(E_Load_Access_Fault)
+  if t == Data & within_mmio_readable(addr, width) then {
+    match mmio_read(addr, width) {
+      MemValue(data)  => MemValue((false, data)),
+      MemException(e) => MemException(e)
+    }
+  } else if within_phys_mem(addr, width) then {
+    phys_mem_read(t, addr, width, aq, rl, res)
+  } else {
+    MemException(E_Load_Access_Fault)
+  }
 
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
 
@@ -47,9 +52,9 @@ $endif
 
 /* NOTE: The rreg effect is due to MMIO. */
 $ifdef RVFI_DII
-val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rreg, escape}
+val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {wreg, rmem, rmemt, rreg, escape}
 $else
-val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
+val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rmemt, rreg, escape}
 $endif
 
 function mem_read (addr, width, aq, rl, res) = {
@@ -59,7 +64,11 @@ function mem_read (addr, width, aq, rl, res) = {
   else match (aq, rl, res) {
     (false, true,  false) => throw(Error_not_implemented("load.rl")),
     (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
-    (_, _, _)             => checked_mem_read(Data, addr, width, aq, rl, res)
+    (_, _, _) =>
+      match checked_mem_read(Data, addr, width, aq, rl, res) {
+        MemValue((tag, data)) => MemValue(data),
+        MemException(e)       => MemException(e)
+      }
   };
  rvfi_read(addr, width, result);
  result
@@ -67,7 +76,7 @@ function mem_read (addr, width, aq, rl, res) = {
 
 val mem_read_cap : (xlenbits, bool, bool, bool) -> MemoryOpResult(Capability) effect {rmem, rmemt, rreg, escape}
 function mem_read_cap (addr, aq, rl, res) = {
-  let result : MemoryOpResult(bits(8 * 'cap_size)) =
+  let result : MemoryOpResult((bool, bits(8 * 'cap_size))) =
   if ~(is_aligned_addr(addr, cap_size))
   then MemException(E_Load_Addr_Align)
   else match (aq, rl, res) {
@@ -75,9 +84,8 @@ function mem_read_cap (addr, aq, rl, res) = {
     (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
     (_, _, _)             => checked_mem_read(Data, addr, cap_size, aq, rl, res)
   };
-  let tag = MEMr_tag(addr);
   match result {
-    MemValue(v) => MemValue(memBitsToCapability(tag, v)),
+    MemValue((tag, v)) => MemValue(memBitsToCapability(tag, v)),
     MemException(e) => MemException(e) : MemoryOpResult(Capability)
   }
 }
@@ -120,24 +128,21 @@ function mem_write_ea_cap(addr, aq, rl, con) = {
      MemValue(MEMea(addr, cap_size))
 }
 
-/* XXX should derive thise form cap_size */
-function tag_align_addr (addr : xlenbits) -> xlenbits = [addr with 3..0 = 0x0]
-
 // only used for actual memory regions, to avoid MMIO effects
 function phys_mem_write forall 'n, 'n <= 'cap_size. (addr : xlenbits, width : atom('n), tag : bool, data: bits(8 * 'n), aq : bool, rl : bool, con : bool) -> MemoryOpResult(bool) = {
-  print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  /*print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   let tag_addr = tag_align_addr(addr);
   print_mem("tag[" ^ BitStr(tag_addr) ^ "] <- " ^ (if tag then "1" else "0"));
-  MEMw_tag(tag_addr, tag);
+  MEMw_tag(tag_addr, tag);*/
 
   /* If the write crosses a cap_size alignment boundary then we need to write the other tag. 
      Writes greater than cap_size that might span more than two regions are not supported. */
-  let tag_addr2 = tag_align_addr(addr + width - 1);
+  /*let tag_addr2 = tag_align_addr(addr + width - 1);
   if tag_addr != tag_addr2 then {
       print_mem("tag[" ^ BitStr(tag_addr2) ^ "] <- " ^ (if tag then "1" else "0"));
       MEMw_tag(tag_addr2, tag);
-  };
-  MemValue(__RISCV_write(addr, width, data, aq, rl, con))
+  };*/
+  MemValue(__RISCV_write(addr, width, tag, data, aq, rl, con))
 }
 
 // dispatches to MMIO regions or physical memory regions depending on physical memory map
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index fdd20de..07cdaa8 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -10,7 +10,7 @@ union FetchResult = {
 function isRVC(h : half) -> bool =
  ~ (h[1 .. 0] == 0b11)
 
-val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function fetch() -> FetchResult = {
   /* check for legal PC */
   let abs_pc = unsigned(PC);
@@ -35,7 +35,7 @@ function fetch() -> FetchResult = {
        */
       match checked_mem_read(Instruction, ppclo, 2, false, false, false) {
         MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
-        MemValue(ilo) => {
+        MemValue((_, ilo)) => {
           if isRVC(ilo) then F_RVC(ilo)
           else if abs_pc + 4 > pcc_top then
             F_CHERI_Err (CapEx_LengthViolation, PC)
@@ -46,7 +46,7 @@ function fetch() -> FetchResult = {
               TR_Address(ppchi) => {
                 match checked_mem_read(Instruction, ppchi, 2, false, false, false) {
                   MemException(e) => F_Error(E_Fetch_Access_Fault, PChi),
-                  MemValue(ihi) => F_Base(append(ihi, ilo))
+                  MemValue((_, ihi)) => F_Base(append(ihi, ilo))
                 }
               }
             }
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
index 52cafba..1423d36 100644
--- a/model/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
@@ -139,7 +139,7 @@ union PTW_Result = {
   PTW_Failure: PTW_Error
 }
 
-val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr39, nat, bool) -> PTW_Result effect {rmem, escape}
+val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr39, nat, bool) -> PTW_Result effect {rmem, rmemt, escape}
 function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result = {
   let va = Mk_SV39_Vaddr(vaddr);
   let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
@@ -155,7 +155,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result
             ^ ": invalid pte address"); */
       PTW_Failure(PTW_Access)
     },
-    MemValue(v) => {
+    MemValue((_, v)) => {
       let pte = Mk_SV39_PTE(v);
       let pbits = pte.BITS();
       let pattr = Mk_PTE_Bits(pbits);
@@ -291,7 +291,7 @@ union TR39_Result = {
   TR39_Failure : PTW_Error
 }
 
-val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, wmvt, escape, rmem}
+val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}
 function translate39(vAddr, ac, priv, mxr, do_sum, level) = {
   let asid = curAsid64();
   match lookupTLB39(asid, vAddr) {
@@ -384,7 +384,7 @@ union TR_Result = {
 
 /* Top-level address translation dispatcher */
 
-val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rreg, wmv, wmvt, wreg}
+val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function translateAddr(vAddr, ac, rt) = {
   let effPriv : Privilege = match rt {
     Instruction => cur_privilege,