Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.

27 files changed, 257 insertions, 190 deletions

diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 63af1021..b839b282 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -214,52 +214,38 @@ function bool register_inaccessible((regno) r) =
   else
     false
 
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag_reserve
 
-val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag_conditional
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> unit effect { wmv } MEMval_tag
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect { wmv } MEMval_tag_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> unit effect { wmvt } MEMval_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> bool effect { wmvt } MEMval_tag_conditional
 
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
-{
   (* assumes addr is cap. aligned *)
-  let tagmem = reverse_endianness(MEMr_tag (addr, cap_size)) in
-  let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in
-  let mem = tagmem[((8 * cap_size) - 1) .. 0] in
-  (tag[0], mem)
-}
+  let (tag, data) = MEMr_tag (addr, cap_size) in
+  (tag, reverse_endianness(data))
+
 
 function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
-{
   (* assumes addr is cap. aligned *)
-  let tagmem = reverse_endianness(MEMr_tag_reserve (addr, cap_size)) in
-  let tag = tagmem[((8 * cap_size) + 7) .. (8 * cap_size)] in
-  let mem = tagmem[((8 * cap_size) - 1) .. 0] in
-  (tag[0], mem)
-}
+  let (tag, data) = MEMr_tag_reserve(addr, cap_size) in
+  (tag, reverse_endianness(data))
 
 function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
   (* assumes addr is cap. aligned *)
-  MEMea_tag(addr, cap_size);
-  MEMval_tag(addr, cap_size,  reverse_endianness(0b0000000 : [tag] : data));
+  MEMea(addr, cap_size);
+  MEMval_tag(addr, cap_size,  tag, reverse_endianness(data));
 }
 
 function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
 {
   (* assumes addr is cap. aligned *)
-  MEMea_tag_conditional(addr, cap_size);
-  MEMval_tag_conditional(addr, cap_size, reverse_endianness(0b0000000 : [tag] : data));
+  MEMea_conditional(addr, cap_size);
+  MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data));
 }
 
-function (bit[64]) align((bit[64]) addr, (nat) alignment) =
-    let remainder = unsigned(addr) mod alignment in
-    addr - remainder
-
 function unit effect {wmem} MEMw_wrapper(addr, size, data) =
   let ledata = reverse_endianness(data) in
   if (addr == 0x000000007f000000) then
@@ -269,23 +255,16 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) =
   }
   else
   {
-    (* On cheri non-capability writes must clear the corresponding tag
-       XXX this is vestigal and only works on sequential modle -- tag clearing
-       should probably be done in memory model. *)
-    TAGw(align(addr, cap_size), 0x00);
-    MEMea(addr,size);
-    MEMval(addr, size, ledata);
+    (* On cheri non-capability writes must clear the corresponding tag *)
+    MEMea(addr, size);
+    MEMval_tag(addr, size, false, ledata);
   }
 
 function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
   {
     (* On cheri non-capability writes must clear the corresponding tag*)
     MEMea_conditional(addr, size);
-    success := MEMval_conditional(addr,size,reverse_endianness(data));
-    if (success) then
-      (* XXX as above TAGw is vestigal and must die *)
-      TAGw(align(addr, cap_size), 0x00);
-    success;
+    MEMval_tag_conditional(addr,size,false,reverse_endianness(data));
   }
 
 function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index bdaa08e6..99487f49 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -34,23 +34,19 @@ let memory_parameter_transformer_option_address _mode v =
 let read_memory_functions : memory_reads =
   [ ("MEMr",             (MR Read_plain              memory_parameter_transformer));
     ("MEMr_reserve",     (MR Read_reserve            memory_parameter_transformer));
-    ("MEMr_tag",         (MR Read_tag                memory_parameter_transformer));
-    ("MEMr_tag_reserve", (MR Read_tag_reserve        memory_parameter_transformer));
+  ]
+
+let read_memory_tagged_functions : memory_read_taggeds =
+  [ ("MEMr_tag",         (MRT Read_plain             memory_parameter_transformer));
+    ("MEMr_tag_reserve", (MRT Read_reserve           memory_parameter_transformer));
   ]
 
 let memory_writes : memory_writes =
-  [ ("TAGw", (MW Write_tag (fun mode v -> let (v, regs) = extern_with_track mode extern_vector_value v in
-                                         (v, 1, regs))
-               (Just (fun (IState interp_state c) success ->
-                               let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in
-                               IState (Interp.add_answer_to_stack interp_state v) c))
-    )); ]
+  []
 
 let memory_eas : memory_write_eas =
   [ ("MEMea",                 (MEA Write_plain           memory_parameter_transformer));
     ("MEMea_conditional",     (MEA Write_conditional     memory_parameter_transformer));
-    ("MEMea_tag",             (MEA Write_tag             memory_parameter_transformer));
-    ("MEMea_tag_conditional", (MEA Write_tag_conditional memory_parameter_transformer));
   ]
 
 let memory_vals : memory_write_vals =
@@ -60,15 +56,18 @@ let memory_vals : memory_write_vals =
                            (fun (IState interp context) b -> 
                              let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
                              (IState (Interp.add_answer_to_stack interp bit) context)))));
-    ("MEMval_tag",      (MV memory_parameter_transformer_option_address Nothing));
-    ("MEMval_tag_conditional", (MV memory_parameter_transformer_option_address
+  ]
+
+let memory_vals_tagged : memory_write_vals_tagged =
+  [
+    ("MEMval_tag",      (MVT memory_parameter_transformer_option_address Nothing));
+    ("MEMval_tag_conditional", (MVT memory_parameter_transformer_option_address
                            (Just 
                            (fun (IState interp context) b -> 
                              let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in
                              (IState (Interp.add_answer_to_stack interp bit) context)))));
   ]
 
-
 let barrier_functions = [
   ("MEM_sync", Barrier_MIPS_SYNC);
   ]
diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml
index 61f34425..d4ea0681 100644
--- a/mips/mips_extras_ml.ml
+++ b/mips/mips_extras_ml.ml
@@ -11,6 +11,7 @@ module Mem = struct
     end)
 end
 
+let cap_size_shift = ref 5;; (* caps every 2**5 = 32 bytes *)
 let mem_pages = (ref Mem.empty : (Bytes.t Mem.t) ref);;
 let tag_mem = (ref Mem.empty : (bool Mem.t) ref);;
 
@@ -74,13 +75,11 @@ let _MEMval (addr, size, data) =
     tracef "MEM[%s] <- %s\n" (big_int_to_hex a) (string_of_value data);
   add_mem_bytes a buf 0 s
 
-let _MEMval_tag (addr, size, data) =
-  let tag = bit_vector_access_int data 0 in
-  let data = vector_subrange_int data (8*(int_of_big_int size) + 7) 8 in 
+let _MEMval_tag (addr, size, tag, data) =
   let addr_bi = (unsigned_big(addr)) in
   begin
     _MEMval (addr, size, data);
-    tag_mem := Mem.add addr_bi (to_bool tag) !tag_mem;
+    tag_mem := Mem.add (shift_right_big_int addr_bi !cap_size_shift) (to_bool tag) !tag_mem;
   end
 
   
@@ -88,8 +87,8 @@ let _MEMval_conditional (addr, size, data) =
     let _ = _MEMval (addr, size, data) in
     Vone
 
-let _MEMval_tag_conditional (addr, size, data) =
-    let _ = _MEMval_tag (addr, size, data) in
+let _MEMval_tag_conditional (addr, size, tag, data) =
+    let _ = _MEMval_tag (addr, size, tag, data) in
     Vone
 
 let _MEMr (addr, size) = begin
@@ -112,17 +111,10 @@ let _MEMr_tag (addr, size) =
   let data = _MEMr(addr, size) in
   let addr_bi = unsigned_big(addr) in 
   let tag = try
-      Mem.find addr_bi !tag_mem 
+      Mem.find (shift_right_big_int addr_bi !cap_size_shift) !tag_mem 
     with Not_found -> false in
-  begin
-    set_start_to_length (vector_concat data (to_vec_dec_int (8, if tag then 1 else 0)))
-  end
+  (bool_to_bit tag, data)
 
 let _MEMr_tag_reserve = _MEMr_tag
 
-let _TAGw (addr, tag) = 
-  begin
-    tag_mem := Mem.add (unsigned_big addr) (to_bool (bit_vector_access_int tag 0)) !tag_mem
-  end
-
 let _MEM_sync _ = ()
diff --git a/mips/run_embed.ml b/mips/run_embed.ml
index 70dee4b6..463caffd 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -197,6 +197,7 @@ module CHERI_model : ISA_model = struct
     set_register Cheri_embed._PCC initial_cap_vec;
     set_register Cheri_embed._nextPCC initial_cap_vec;
     set_register Cheri_embed._delayedPCC initial_cap_vec;
+    cap_size_shift := 5; (* configure memory model cap_size in mips_extras_ml *)
     for i = 0 to 31 do
       set_register (vector_access_int Cheri_embed._CapRegs i) initial_cap_vec
     done
@@ -254,6 +255,7 @@ module CHERI128_model : ISA_model = struct
     set_register Cheri128_embed._PCC initial_cap_vec;
     set_register Cheri128_embed._nextPCC initial_cap_vec;
     set_register Cheri128_embed._delayedPCC initial_cap_vec;
+    cap_size_shift := 4; (* configure memory model cap_size in mips_extras_ml *)
     for i = 0 to 31 do
       set_register (vector_access_int Cheri128_embed._CapRegs i) initial_cap_vec
     done
diff --git a/src/ast.ml b/src/ast.ml
index 5eb45554..7ed991ab 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -117,9 +117,11 @@ base_effect_aux =  (* effect *)
    BE_rreg (* read register *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
+ | BE_rmemt (* read memory tagged *)
  | BE_wmem (* write memory *)
  | BE_eamem (* signal effective address for writing memory *)
  | BE_wmv (* write memory, sending only value *)
+ | BE_wmvt (* write memory, sending only value and tag *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 82cc6b7c..8f204a65 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -277,8 +277,10 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
                                | Parse_ast.BE_rreg   -> BE_rreg
                                | Parse_ast.BE_wreg   -> BE_wreg
                                | Parse_ast.BE_rmem   -> BE_rmem
+                               | Parse_ast.BE_rmemt  -> BE_rmemt
                                | Parse_ast.BE_wmem   -> BE_wmem
 			       | Parse_ast.BE_wmv    -> BE_wmv
+			       | Parse_ast.BE_wmvt   -> BE_wmvt
 			       | Parse_ast.BE_eamem  -> BE_eamem
 			       | Parse_ast.BE_depend -> BE_depend
                                | Parse_ast.BE_undef  -> BE_undef
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 24f624e3..f72bd100 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -356,9 +356,11 @@ type action =
  | Read_reg of reg_form * maybe (nat * nat)
  | Write_reg of reg_form * maybe (nat * nat) * value
  | Read_mem of id * value * maybe (nat * nat)
+ | Read_mem_tagged of id * value * maybe (nat * nat)
  | Write_mem of id * value * maybe (nat * nat) * value
  | Write_ea of id * value
  | Write_memv of id * value * value
+ | Write_memv_tagged of id * value * value * value
  | Barrier of id * value
  | Footprint of id * value
  | Nondet of list (exp tannot) * tag
@@ -2227,6 +2229,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
           let mk_thunk_frame act = (Action act (mk_thunk l annot t_level le lm), lm, le) in
           if has_rmem_effect effects 
           then mk_hole_frame (Read_mem (id_of_string name_ext) v Nothing) 
+          else if has_rmemt_effect effects 
+          then mk_hole_frame (Read_mem_tagged (id_of_string name_ext) v Nothing) 
           else if has_barr_effect effects
           then mk_thunk_frame (Barrier (id_of_string name_ext) v)
           else if has_depend_effect effects
@@ -2251,6 +2255,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                    (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved)))
                  | _ -> (v,unitv) end in
                mk_hole_frame (Write_memv (id_of_string name_ext) v wv)
+          else if has_wmvt_effect effects
+          then match v with
+               | V_tuple [addr; size; tag; data] -> 
+                  mk_hole_frame (Write_memv_tagged (id_of_string name_ext) (V_tuple([addr; size])) tag data)
+               | _ -> Assert_extra.failwith("wmvt: expected tuple of four elements") end
           else mk_hole_frame (Call_extern name_ext v) 
         | _ ->
           (Error l (String.stringAppend "Tag not empty, spec, ctor, or extern on function call " name),lm,le) end)
@@ -2384,6 +2393,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                   | (Action (Write_reg regf range value) stack) -> a
                   | (Action (Write_mem id a_ range value) stack) -> a
                   | (Action (Write_memv _ _ _) stack) -> a
+                  | (Action (Write_memv_tagged _ _ _ _) stack) -> a
                   | _ -> update_stack a (add_to_top_frame 
                                            (fun e env -> 
                                              let (ev,env') = (to_exp mode env v) in
@@ -3047,6 +3057,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
        match a with
        | Read_reg _ _ -> ((Action a s,lm,le), next_builder, Nothing)
        | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder, Nothing)
+       | Read_mem_tagged _ _ _ -> ((Action a s,lm,le), next_builder, Nothing)
        | Call_extern _ _ -> ((Action a s,lm,le), next_builder, Nothing)
        | Write_reg ((Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> 
          match in_env subregs id' with
diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem
index 64fb14b2..c65963d7 100644
--- a/src/lem_interp/interp_ast.lem
+++ b/src/lem_interp/interp_ast.lem
@@ -119,9 +119,11 @@ type base_effect_aux =  (* effect *)
  | BE_rreg (* read register *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
+ | BE_rmemt (* read memory and tag *)
  | BE_wmem (* write memory *)
  | BE_eamem (* signal effective address for writing memory *)
  | BE_wmv (* write memory, sending only value *)
+ | BE_wmvt (* write memory, sending only value and tag *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 72bf0bcc..ec747457 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -96,10 +96,7 @@ let is_bool = function
   | Bitl_unknown -> false
 end
 
-let bits_to_ibits l = List.map bit_to_ibit l
-let bitls_to_ibits l = List.map bitl_to_ibit l
-let bitls_from_ibits l = List.map 
-  (fun b -> 
+let bitl_from_ibit b = 
     let b = Interp.detaint b in
     match b with
     | Interp.V_lit (L_aux L_zero _) -> Bitl_zero
@@ -109,7 +106,11 @@ let bitls_from_ibits l = List.map
     | Interp.V_lit (L_aux L_undef _) -> Bitl_undef
     | Interp.V_vector _ _ [Interp.V_lit (L_aux L_undef _)] -> Bitl_undef
     | Interp.V_unknown -> Bitl_unknown
-    | _ -> Assert_extra.failwith ("bitls_from_ibits given unexpected " ^ (Interp.string_of_value b)) end) l
+    | _ -> Assert_extra.failwith ("bit_from_ibit given unexpected " ^ (Interp.string_of_value b)) end
+
+let bits_to_ibits l = List.map bit_to_ibit l
+let bitls_to_ibits l = List.map bitl_to_ibit l
+let bitls_from_ibits l = List.map bitl_from_ibit l
 
 let bits_from_ibits l = List.map 
   (fun b -> 
@@ -426,12 +427,16 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
         exn_seen (fun _ -> Interp.resume mode stack Nothing)
     | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Read memory request in a " ^ errk_str)), events_out)
+    | (Interp.Action (Interp.Read_mem_tagged _ _ _) _,_,_) ->
+      (Ivh_error (Interp_interface.Internal_error ("Read memory tagged request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write memory request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write ea request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_memv _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
+    | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) ->
+      (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out)
     | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
 end
 
@@ -455,7 +460,7 @@ let translate_address top_level end_flag thunk_name registers address =
   let (Address bytes i) = address in
   let mode = make_mode true false in
   let int_mode = mode.internal_mode in
-  let (Context top_env direction _ _ _ _ _ _) = top_level in
+  let (Context top_env direction _ _ _ _ _ _ _ _) = top_level in
   let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
@@ -499,7 +504,7 @@ let intern_instruction direction (name,parms) =
 let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
   let mode = make_mode true false in
   let int_mode = mode.internal_mode in
-  let (Context top_env direction _ _ _ _ _ _) = top_level in
+  let (Context top_env direction _ _ _ _ _ _ _ _) = top_level in
   let intern_val = intern_instruction direction instruction in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
@@ -584,7 +589,6 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
            (Interp.V_ctor (Id_aux (Id r) _) _ _ _) ->
             IK_mem_read (match r with
                          | "Read_plain" ->             Read_plain
-                         | "Read_tag"   ->             Read_tag
                          | "Read_reserve" ->           Read_reserve
                          | "Read_acquire" ->           Read_acquire
                          | "Read_exclusive" ->         Read_exclusive
@@ -595,7 +599,6 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
            (Interp.V_ctor (Id_aux (Id w) _) _ _ _) ->
             IK_mem_write (match w with
                          | "Write_plain" ->             Write_plain
-                         | "Write_tag"   ->             Write_tag
                          | "Write_conditional" ->       Write_conditional
                          | "Write_release" ->           Write_release
                          | "Write_exclusive" ->         Write_exclusive
@@ -641,7 +644,7 @@ end
 
 
 let interp_value_to_instr_external top_level instr = 
-  let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _) = top_level in
+  let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _ _) = top_level in
   match instr with
   | Interp.V_ctor (Id_aux (Id i) _) _ _ parm ->
      match (find_instruction i instructions) with
@@ -666,7 +669,7 @@ let interp_value_to_instr_external top_level instr =
 
 let decode_to_instruction top_level registers value : instruction_or_decode_error = 
   let mode = make_interpreter_mode true false in
-  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _) = top_level in
+  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _ _ _) = top_level in
   let intern_val = intern_opcode direction value in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
@@ -703,7 +706,7 @@ end
 
 
 let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = 
-  let (Context top_env _ _ _ _ _ _ _) = top_level in
+  let (Context top_env _ _ _ _ _ _ _ _ _) = top_level in
   match decode_to_instruction top_level registers value with
   | IDE_instr instr instrv ->
      let mode = make_interpreter_mode true false in
@@ -718,7 +721,7 @@ let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_e
 
 
 let instr_external_to_interp_value top_level instr =
-  let (Context _ direction _ _ _ _ _ _) = top_level in
+  let (Context _ direction _ _ _ _ _ _ _ _) = top_level in
   let (name,parms) = instr in
 
   let get_value (_,typ,v) = 
@@ -745,7 +748,7 @@ let instr_external_to_interp_value top_level instr =
 val instruction_to_istate : context -> instruction -> instruction_state 
 let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state  = 
   let mode = make_interpreter_mode true false in
-  let (Context top_env _ _ _ _ _ _ _) = top_level in
+  let (Context top_env _ _ _ _ _ _ _ _ _) = top_level in
   let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in
   (IState
      (Interp.Thunk_frame
@@ -755,7 +758,7 @@ let instruction_to_istate (top_level:context) (((name, parms) as instr):instruct
      top_level)
 
 let rec interp_to_outcome mode context thunk = 
-  let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in
+  let (Context _ direction mem_reads mem_reads_tagged mem_writes mem_write_eas mem_write_vals mem_write_vals_tagged barriers spec_externs) = context in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   match thunk () with
   | (Interp.Value _,lm,le) -> (Done,lm)
@@ -784,6 +787,19 @@ let rec interp_to_outcome mode context thunk =
             else Error ("Memory address on read is not 64 bits")
           | _ -> Error ("Memory function " ^ i ^ " not found")
         end  , lm)
+      | Interp.Read_mem_tagged (Id_aux (Id i) _) value slice ->
+        (match List.lookup i mem_reads_tagged with
+          | (Just (MRT read_k f)) -> 
+            let (location, length, tracking) = (f mode value) in 
+            if (List.length location) = 8
+            then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with
+              | Just bs -> Just (integer_of_byte_list bs)
+              | _ -> Nothing end in
+                Read_mem_tagged read_k (Address_lifted location address_int) length tracking 
+                  (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context)
+            else Error ("Memory address on read is not 64 bits")
+          | _ -> Error ("Memory function " ^ i ^ " not found")
+        end  , lm)
       | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
         (match List.lookup i mem_writes with
           | (Just (MW write_k f return)) -> 
@@ -832,6 +848,25 @@ let rec interp_to_outcome mode context thunk =
                     | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
                     | Just return_bool -> return_bool (IState next_state context) b end)
             | _ -> Error ("Memory function " ^ i ^ " not found") end, lm)
+        | Interp.Write_memv_tagged (Id_aux (Id i) _) address_val tag_val write_val ->
+           (match List.lookup i mem_write_vals_tagged with
+            | (Just (MVT parmf return)) -> 
+              let (value, v_tracking) = 
+                match (Interp.detaint write_val) with
+                  | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
+                  | _ -> extern_with_track mode extern_mem_value write_val end in
+               let location_opt = match parmf mode address_val with
+                  | Nothing -> Nothing
+                  | Just mv -> let address_int = match (maybe_all (List.map byte_of_byte_lifted mv)) with
+                      | Just bs -> Just (integer_of_byte_list bs)
+                      | _ -> Nothing end in Just (Address_lifted mv address_int) end
+               in
+               Write_memv_tagged location_opt ((bitl_from_ibit tag_val), value) v_tracking 
+                (fun b -> 
+                  match return with
+                    | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context)
+                    | Just return_bool -> return_bool (IState next_state context) b end)
+            | _ -> Error ("Memory function " ^ i ^ " not found") end, lm)
          | Interp.Barrier (Id_aux (Id i) _) lval ->
            (match List.lookup i barriers with
              | Just barrier -> 
@@ -899,7 +934,7 @@ end
 
 (*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*)
 let rec ie_loop mode register_values (IState interp_state context) = 
-  let (Context _ direction externs reads writes write_eas write_vals barriers) = context in
+  let (Context _ direction externs reads reads_tagged writes write_eas write_vals write_vals_tagged barriers) = context in
   let unknown_reg size =  
     <| rv_bits = (List.replicate size Bitl_unknown);
        rv_start = 0;
@@ -927,6 +962,9 @@ let rec ie_loop mode register_values (IState interp_state context) =
     | (Read_mem read_k loc length tracking i_state_fun, _) ->
       let (events,analysis_data) = ie_loop mode register_values (i_state_fun (unknown_mem length)) in
       ((E_read_mem read_k loc length tracking)::events,analysis_data)
+    | (Read_mem_tagged read_k loc length tracking i_state_fun, _) ->
+      let (events,analysis_data) = ie_loop mode register_values (i_state_fun (Bitl_unknown, (unknown_mem length))) in
+      ((E_read_memt read_k loc length tracking)::events,analysis_data)
     | (Write_mem write_k loc length tracking value v_tracking i_state_fun, _) ->
       let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
       let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
@@ -940,6 +978,11 @@ let rec ie_loop mode register_values (IState interp_state context) =
       let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
       (*TODO: consider if lm and lm should be merged*)
       ((E_write_memv opt_address value tracking)::(events++events'),analysis_data)
+    | (Write_memv_tagged opt_address value tracking i_state_fun, _) ->
+      let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in
+      let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in
+      (*TODO: consider if lm and lm should be merged*)
+      ((E_write_memvt opt_address value tracking)::(events++events'),analysis_data)
     | (Barrier barrier_k i_state, _) ->
       let (events,analysis_data) = ie_loop mode register_values i_state in
       ((E_barrier barrier_k)::events,analysis_data)
@@ -1076,9 +1119,11 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function
   | E_barrier Barrier_TM_COMMIT -> Just (IK_trans Transaction_commit)
 
   | E_read_mem rk _ _ _ -> Just (IK_mem_read rk)
+  | E_read_memt rk _ _ _ -> Just (IK_mem_read rk)
   | E_write_mem wk _ _ _ _ _  -> Just (IK_mem_write wk)
   | E_write_ea wk _ _ _ -> Just (IK_mem_write wk)
   | E_write_memv _ _ _ -> Nothing
+  | E_write_memvt _ _ _ -> Nothing
   | E_barrier bk -> Just (IK_barrier bk)
   | E_footprint -> Nothing
   | E_read_reg _ -> Nothing
@@ -1091,9 +1136,11 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function
 
 let regs_in_of_event : event -> list reg_name = function
   | E_read_mem _ _ _ _ -> []
+  | E_read_memt _ _ _ _ -> []
   | E_write_mem _ _ _ _ _ _  -> []
   | E_write_ea _ _ _ _ -> []
   | E_write_memv _ _ _ -> []
+  | E_write_memvt _ _ _ -> []
   | E_barrier _ -> []
   | E_footprint -> []
   | E_read_reg r -> [r]
@@ -1104,9 +1151,11 @@ let regs_in_of_event : event -> list reg_name = function
 
 let regs_out_of_event : event -> list reg_name = function
   | E_read_mem _ _ _ _ -> []
+  | E_read_memt _ _ _ _ -> []
   | E_write_mem _ _ _ _ _ _  -> []
   | E_write_ea _ _ _ _ -> []
   | E_write_memv _ _ _ -> []
+  | E_write_memvt _ _ _ -> []
   | E_barrier _ -> []
   | E_footprint -> []
   | E_read_reg _ -> []
@@ -1119,11 +1168,14 @@ let regs_out_of_event : event -> list reg_name = function
 let regs_feeding_memory_access_address_of_event : event -> list reg_name = function
   | E_read_mem _ _ _ (Just rs)       -> rs
   | E_read_mem _ _ _ None            -> []
+  | E_read_memt _ _ _ (Just rs)       -> rs
+  | E_read_memt _ _ _ None            -> []
   | E_write_mem _ _ _ (Just rs) _ _  -> rs
   | E_write_mem _ _ _ None _ _       -> []
   | E_write_ea wk _ _ (Just rs)      -> rs
   | E_write_ea wk _ _ None           -> []
   | E_write_memv _ _ _               -> []
+  | E_write_memvt _ _ _               -> []
   | E_barrier bk                     -> []
   | E_footprint                      -> []
   | E_read_reg _                     -> []
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 3ef6abb8..fce5b14f 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -179,17 +179,21 @@ type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value
 type optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value
 type memory_read = MR of read_kind * memory_parameter_transformer
 type memory_reads  = list (string * memory_read)
+type memory_read_tagged  = MRT of read_kind * memory_parameter_transformer
+type memory_read_taggeds = list (string * memory_read_tagged)
 type memory_write_ea = MEA of write_kind * memory_parameter_transformer
 type memory_write_eas = list (string * memory_write_ea)
 type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
 and memory_writes = list (string * memory_write)
 and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
 and memory_write_vals = list (string * memory_write_val)
+and memory_write_val_tagged = MVT of optional_memory_transformer * (maybe (instruction_state -> bool -> instruction_state))
+and memory_write_vals_tagged = list (string * memory_write_val_tagged)
 
 (* Definition information needed to run an instruction *)
 and context =
     Context of Interp.top_level * direction * 
-	memory_reads * memory_writes * memory_write_eas * memory_write_vals * barriers * external_functions
+	memory_reads * memory_read_taggeds * memory_writes * memory_write_eas * memory_write_vals * memory_write_vals_tagged * barriers * external_functions
 
 (* An instruction in flight *)
 and instruction_state = IState of interpreter_state * context
@@ -199,6 +203,7 @@ type outcome =
 (* Request to read N bytes at address *)
 (* The register list, used when mode.track_values, is those that the address depended on *)
 | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) * (memory_value -> instruction_state)
+| Read_mem_tagged of read_kind * address_lifted * nat * maybe (list reg_name) * ((bit_lifted * memory_value) -> instruction_state)
 
 (* Request to write memory *)
 | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name)
@@ -209,6 +214,7 @@ type outcome =
 
 (* Request to write memory at last signaled address. Memory value should be 8* the size given in Write_ea *)
 | Write_memv of maybe address_lifted * memory_value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_memv_tagged of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name) * (bool -> instruction_state)
 
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
@@ -248,7 +254,7 @@ type outcome =
 
 
 (* Functions to build up the initial state for interpretation *)
-val build_context : specification -> memory_reads -> memory_writes -> memory_write_eas -> memory_write_vals -> barriers -> external_functions -> context 
+val build_context : specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> external_functions -> context 
 val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 86042d61..f54fad5a 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -105,6 +105,7 @@ end
 let ~{ocaml} list_to_string format sep list = ""
 
 val has_rmem_effect : list base_effect -> bool
+val has_rmemt_effect : list base_effect -> bool
 val has_barr_effect : list base_effect -> bool
 val has_wmem_effect : list base_effect -> bool
 val has_depend_effect : list base_effect -> bool
@@ -116,8 +117,10 @@ let rec has_effect which efcts =
     | (BE_rreg,BE_rreg)     -> true 
     | (BE_wreg,BE_wreg)     -> true 
     | (BE_rmem,BE_rmem)     -> true 
+    | (BE_rmemt,BE_rmemt)   -> true 
     | (BE_wmem,BE_wmem)     -> true 
     | (BE_wmv,BE_wmv)       -> true
+    | (BE_wmvt,BE_wmvt)     -> true
     | (BE_eamem,BE_eamem)   -> true
     | (BE_barr,BE_barr)     -> true 
     | (BE_undef,BE_undef)   -> true 
@@ -128,10 +131,12 @@ let rec has_effect which efcts =
     end 
   end
 let has_rmem_effect = has_effect BE_rmem
+let has_rmemt_effect = has_effect BE_rmemt
 let has_barr_effect = has_effect BE_barr
 let has_wmem_effect = has_effect BE_wmem
 let has_eamem_effect = has_effect BE_eamem
 let has_wmv_effect = has_effect BE_wmv
+let has_wmvt_effect = has_effect BE_wmvt
 let has_depend_effect = has_effect BE_depend
 
 let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 7d182258..c9ec4e76 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -122,8 +122,10 @@ let doc_effect (BE_aux (e,_)) =
   | BE_rreg -> "rreg"
   | BE_wreg -> "wreg"
   | BE_rmem -> "rmem"
+  | BE_rmemt -> "rmemt"
   | BE_wmem -> "wmem"
   | BE_wmv  -> "wmv"
+  | BE_wmvt  -> "wmvt"
   | BE_eamem -> "eamem"
   | BE_barr -> "barr"
   | BE_depend -> "depend"
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 4922a59a..9594f238 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -425,6 +425,10 @@ let rec format_events = function
     "     Read_mem at " ^ (memory_value_to_string E_big_endian location) ^ " based on registers " ^
       format_tracking tracking ^  " for " ^ (string_of_int length) ^ " bytes \n" ^
     (format_events events)
+  | (E_read_memt(read_kind, (Address_lifted(location, _)), length, tracking))::events ->
+    "     Read_memt at " ^ (memory_value_to_string E_big_endian location) ^ " based on registers " ^
+      format_tracking tracking ^  " for " ^ (string_of_int length) ^ " bytes \n" ^
+    (format_events events)
   | (E_write_mem(write_kind,(Address_lifted (location,_)), length, tracking, value, v_tracking))::events ->
     "     Write_mem at " ^ (memory_value_to_string E_big_endian location) ^ ", based on registers " ^
       format_tracking tracking ^ ", writing " ^ (memory_value_to_string E_big_endian value) ^
@@ -438,6 +442,10 @@ let rec format_events = function
     "     Write_memv of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^
       format_tracking v_tracking ^ "\n" ^
       (format_events events)
+  | (E_write_memvt(_, (tag, value), v_tracking))::events ->
+    "     Write_memvt of " ^ (memory_value_to_string E_big_endian value) ^ ", based on registers " ^
+      format_tracking v_tracking ^ "\n" ^
+      (format_events events)
   | ((E_barrier b_kind)::events) ->
     "     Memory_barrier occurred\n" ^ 
     (format_events events)
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 8be5354a..fc78f163 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -148,7 +148,10 @@ let combine_slices (start, stop) (inner_start,inner_stop) =
 
 let unit_lit = (L_aux(L_unit,Interp_ast.Unknown))
 
-let rec perform_action ((reg, mem, tagmem) as env) = function
+let align_addr addr size = 
+  sub addr (modulus addr size)
+
+let rec perform_action ((reg, mem, tagmem) as env, cap_size) = function
  (* registers *)
  | Read_reg1(Reg(id,_,_,_), _) -> (Some(Reg.find id reg), env)
  | Read_reg1(Reg_slice(id, _, _, range), _)
@@ -170,48 +173,41 @@ let rec perform_action ((reg, mem, tagmem) as env) = function
      | Some a -> a
      | None -> assert false (*TODO remember how to report an error *)in
    let naddress = integer_of_address address in
-   (match kind with
-    | Read_tag | Read_tag_reserve ->
-      let tag = Mem.find naddress tagmem in
-      let rec reading (n : num) length = 
-        if length = 0 
-        then []
-        else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in
-      (Some (register_value_of_memory_value (tag::(reading naddress length)) !default_order), env)
-    | _ ->
-      let rec reading (n : num) length = 
-        if length = 0 
-        then []
-        else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in
-      (Some (register_value_of_memory_value (reading naddress length) !default_order), env))
+   let rec reading (n : num) length = 
+     if length = 0 
+     then []
+     else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in
+   (Some (register_value_of_memory_value (reading naddress length) !default_order), env)
+ | Read_mem_tagged0(kind,location, length, _,_) ->
+   let address = match address_of_address_lifted location with
+     | Some a -> a
+     | None -> assert false (*TODO remember how to report an error *)in
+   let naddress = integer_of_address address in
+   let tag = Mem.find (align_addr naddress cap_size) tagmem in
+   let rec reading (n : num) length = 
+     if length = 0 
+     then []
+     else (Mem.find n mem)::(reading (add n big_num_unit) (length - 1)) in
+   (Some (register_value_of_memory_value (tag::(reading naddress length)) !default_order), env)
  | Write_mem0(kind,location, length, _, bytes,_,_) ->
    let address = match address_of_address_lifted location with
      | Some a -> a
      | None -> assert false (*TODO remember how to report an error *)in
    let naddress = integer_of_address address in
-   (match kind with
-    | Write_tag | Write_tag_conditional ->
-      (match bytes with
-       | [b] -> (None,(reg,mem,Mem.add naddress b tagmem))
-       | _ -> assert false)
-   | _ -> 
-     let rec writing location length bytes mem = 
-       if length = 0
-       then mem
-       else match bytes with
+   let rec writing location length bytes mem = 
+     if length = 0
+     then mem
+     else match bytes with
          | [] -> mem
          | b::bytes -> 
            writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in
-     (None,(reg,writing naddress length bytes mem,tagmem)))
+     (None,(reg,writing naddress length bytes mem,tagmem))
  | Write_memv1(Some location, bytes, _, _) ->
    let address = match address_of_address_lifted location with
      | Some a -> a
      | _ -> failwith "Write address not known" in
    let naddress = integer_of_address address in
    let length = List.length bytes in
-   let (length,tag_mem,bytes) = if length = 17 || length = 33
-     then (length - 1, Mem.add naddress (List.hd bytes) tagmem, (List.tl bytes))
-     else (length,tagmem,bytes) in
    let rec writing location length bytes mem =
      if length = 0
      then mem
@@ -219,7 +215,22 @@ let rec perform_action ((reg, mem, tagmem) as env) = function
        | [] -> mem
        | b::bytes -> 
          writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in
-   (None, (reg,writing naddress length bytes mem, tag_mem))
+   (None, (reg,writing naddress length bytes mem, tagmem))
+ | Write_memv_tagged0(Some location, (tag, bytes), _, _) ->
+    let address = match address_of_address_lifted location with
+     | Some a -> a
+     | _ -> failwith "Write address not known" in
+    let naddress = integer_of_address address in
+    let length = List.length bytes in
+    let rec writing location length bytes mem =
+     if length = 0
+     then mem
+     else match bytes with
+       | [] -> mem
+       | b::bytes -> 
+         writing (add location big_num_unit) (length - 1) bytes (Mem.add location b mem) in
+    let tagmem = Mem.add (align_addr naddress cap_size) (Byte_lifted ([Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;Bitl_zero;tag])) tagmem in
+    (None, (reg,writing naddress length bytes mem, tagmem))
  | _ -> (None, env)
 ;;
 
@@ -245,6 +256,7 @@ let run
   reg
   mem
   tagmem
+  cap_size
   eager_eval
   track_dependencies
   mode
@@ -321,7 +333,7 @@ let run
       errorf "%s: %s: %s\n" (grey name) (red "assertion failed") "No message provided";
       (false, mode, !track_dependencies, env)
     | action ->
-      let (return,env') = perform_action env action in
+      let (return,env') = perform_action (env, cap_size) action in
       let step ?(force=false) (state: instruction_state) =
         let stack = match state with IState(stack,_) -> stack in
         let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in
@@ -356,6 +368,22 @@ let run
              let next = next_thunk (memory_value_of_register_value value) in
              (step next, env', next)
            | None -> assert false)
+        | Read_mem_tagged0(kind, (Address_lifted(location,_)), length, tracking, next_thunk) ->
+          (match return with
+           | Some(value) -> 
+             show "read_mem_tagged"
+               (memory_value_to_string !default_endian location) right
+               (register_value_to_string value);
+             (match tracking with
+              | None -> ()
+              | Some(deps) ->
+                show "read_mem address depended on" (dependencies_to_string deps) "" "");
+             let next = 
+               (match (memory_value_of_register_value value) with
+                | (Byte_lifted tag)::bytes -> next_thunk ((List.nth tag 7), bytes)
+                | _ -> assert false) in
+             (step next, env', next)
+           | None -> assert false)
         | Write_mem0(kind,(Address_lifted(location,_)), length, tracking, value, v_tracking, next_thunk) ->
           show "write_mem" (memory_value_to_string !default_endian location) left
             (memory_value_to_string !default_endian value);
@@ -374,6 +402,10 @@ let run
           show "write_mem value" (memory_value_to_string !default_endian location) left (memory_value_to_string !default_endian value);
           let next = next_thunk true in
           (step next,env',next)
+        | Write_memv_tagged0(Some(Address_lifted(location,_)),(tag, value),_,next_thunk) ->
+          show "write_mem_tagged value" (memory_value_to_string !default_endian location) left (memory_value_to_string !default_endian value);
+          let next = next_thunk true in
+          (step next,env',next)
         | Write_ea1(_,(Address_lifted(location,_)), size,_,next) ->
           show "write_announce" (memory_value_to_string !default_endian location) left ((string_of_int size) ^ " bytes");
           (step next, env, next)
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 6ce5d5e8..6920b47e 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -1214,7 +1214,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
           then resultf "\nSUCCESS program terminated after %d instructions\n" count
           else
             begin
-              match Run_interp_model.run  istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with
+              match Run_interp_model.run  istate !reg !prog_mem !tag_mem (Nat_big_num.of_int 1) !eager_eval track_dependencies mode "execute" with
               | false, _,_, _ -> errorf "FAILURE\n"; exit 1
               | true, mode, track_dependencies, (my_reg, my_mem, my_tags) ->
                 reg := my_reg;
@@ -1292,7 +1292,7 @@ let run () =
         startaddr,
         startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
 
-  let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in
+  let context = build_context isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 isa_externs in
   (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, 
           endian mode, and translate function name 
   *)
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 546fe6c8..2237d6be 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -804,9 +804,11 @@ let initial_system_state_of_elf_file name =
           
           (Cheri.defs,
            (Mips_extras.read_memory_functions,
+            Mips_extras.read_memory_tagged_functions,
             Mips_extras.memory_writes,
             Mips_extras.memory_eas,
             Mips_extras.memory_vals,
+            Mips_extras.memory_vals_tagged,
             Mips_extras.barrier_functions),
            [],
            MIPS,
@@ -1304,7 +1306,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
           then resultf "\nSUCCESS program terminated after %d instructions\n" count
           else
             begin
-              match Run_interp_model.run  istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with
+              match Run_interp_model.run  istate !reg !prog_mem !tag_mem (Nat_big_num.of_int 32) !eager_eval track_dependencies mode "execute" with
               | false, _,_, _ -> errorf "FAILURE\n"; exit 1
               | true, mode, track_dependencies, (my_reg, my_mem, my_tags) ->
                 reg := my_reg;
@@ -1377,14 +1379,14 @@ let run () =
   if !break_point then eager_eval := true;
 
   let ((isa_defs,
-       (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4),
+       (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4,isa_m5,isa_m6),
         isa_externs,
         isa_model,
         model_reg_d,
         startaddr,
         startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
 
-  let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in
+  let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 isa_externs in
   (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, 
           endian mode, and translate function name 
   *)
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 4c881b04..b34b1753 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -804,9 +804,11 @@ let initial_system_state_of_elf_file name =
           
           (Cheri128.defs,
            (Mips_extras.read_memory_functions,
+            Mips_extras.read_memory_tagged_functions,
             Mips_extras.memory_writes,
             Mips_extras.memory_eas,
             Mips_extras.memory_vals,
+            Mips_extras.memory_vals_tagged,
             Mips_extras.barrier_functions),
            [],
            MIPS,
@@ -1304,7 +1306,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
           then resultf "\nSUCCESS program terminated after %d instructions\n" count
           else
             begin
-              match Run_interp_model.run  istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with
+              match Run_interp_model.run  istate !reg !prog_mem !tag_mem (Nat_big_num.of_int 16) !eager_eval track_dependencies mode "execute" with
               | false, _,_, _ -> errorf "FAILURE\n"; exit 1
               | true, mode, track_dependencies, (my_reg, my_mem, my_tags) ->
                 reg := my_reg;
@@ -1377,14 +1379,14 @@ let run () =
   if !break_point then eager_eval := true;
 
   let ((isa_defs,
-       (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4),
+       (isa_m0, isa_m1, isa_m2, isa_m3, isa_m4, isa_m5, isa_m6),
         isa_externs,
         isa_model,
         model_reg_d,
         startaddr,
         startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
 
-  let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in
+  let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 isa_externs in
   (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, 
           endian mode, and translate function name 
   *)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 02d53896..856b90a1 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -41,7 +41,7 @@
 (*========================================================================*)
 
 open import Pervasives_extra
-            
+
 (* maybe isn't a member of type Ord - this should be in the Lem standard library*)
 instance forall 'a. Ord 'a => (Ord (maybe 'a))
   let compare = maybeCompare compare
@@ -422,7 +422,6 @@ end
 type read_kind =
   (* common reads *)
   | Read_plain
-  | Read_tag | Read_tag_reserve (*For reading the tag of tagged memory*)
   (* Power reads *)
   | Read_reserve
   (* AArch64 reads *)
@@ -431,8 +430,6 @@ type read_kind =
 instance (Show read_kind)
   let show = function
     | Read_plain -> "Read_plain"
-    | Read_tag -> "Read_tag"
-    | Read_tag_reserve -> "Read_tag_reserve"
     | Read_reserve -> "Read_reserve"
     | Read_acquire -> "Read_acquire"
     | Read_exclusive -> "Read_exclusive"
@@ -444,7 +441,6 @@ end
 type write_kind =
   (* common writes *)
   | Write_plain
-  | Write_tag | Write_tag_conditional (*For writing the tag of tagged memory*)
   (* Power writes *)
   | Write_conditional
   (* AArch64 writes *)
@@ -453,8 +449,6 @@ type write_kind =
 instance (Show write_kind)
   let show = function
     | Write_plain -> "Write_plain"
-    | Write_tag -> "Write_tag"
-    | Write_tag_conditional -> "Write_tag_conditional"
     | Write_conditional -> "Write_conditional"
     | Write_release -> "Write_release"
     | Write_exclusive -> "Write_exclusive"
@@ -536,8 +530,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_plain, Read_exclusive)         -> LT
   | (Read_plain, Read_exclusive_acquire) -> LT
   | (Read_plain, Read_stream)            -> LT
-  | (Read_plain, Read_tag)               -> LT
-  | (Read_plain, Read_tag_reserve)       -> LT
 
   | (Read_reserve, Read_plain)             -> GT
   | (Read_reserve, Read_reserve)           -> EQ
@@ -545,8 +537,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_reserve, Read_exclusive)         -> LT
   | (Read_reserve, Read_exclusive_acquire) -> LT
   | (Read_reserve, Read_stream)            -> LT
-  | (Read_reserve, Read_tag)               -> LT
-  | (Read_reserve, Read_tag_reserve)       -> LT
 
   | (Read_acquire, Read_plain)             -> GT
   | (Read_acquire, Read_reserve)           -> GT
@@ -554,8 +544,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_acquire, Read_exclusive)         -> LT
   | (Read_acquire, Read_exclusive_acquire) -> LT
   | (Read_acquire, Read_stream)            -> LT
-  | (Read_acquire, Read_tag)               -> LT
-  | (Read_acquire, Read_tag_reserve)       -> LT
 
   | (Read_exclusive, Read_plain)             -> GT
   | (Read_exclusive, Read_reserve)           -> GT
@@ -563,8 +551,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_exclusive, Read_exclusive)         -> EQ
   | (Read_exclusive, Read_exclusive_acquire) -> LT
   | (Read_exclusive, Read_stream)            -> LT
-  | (Read_exclusive, Read_tag)               -> LT
-  | (Read_exclusive, Read_tag_reserve)       -> LT
 
   | (Read_exclusive_acquire, Read_plain)             -> GT
   | (Read_exclusive_acquire, Read_reserve)           -> GT
@@ -572,8 +558,6 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_exclusive_acquire, Read_exclusive)         -> GT
   | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
   | (Read_exclusive_acquire, Read_stream)            -> GT
-  | (Read_exclusive_acquire, Read_tag)               -> LT
-  | (Read_exclusive_acquire, Read_tag_reserve)       -> LT
 
   | (Read_stream, Read_plain)             -> GT
   | (Read_stream, Read_reserve)           -> GT
@@ -581,27 +565,7 @@ let ~{ocaml} read_kindCompare rk1 rk2 =
   | (Read_stream, Read_exclusive)         -> GT
   | (Read_stream, Read_exclusive_acquire) -> GT
   | (Read_stream, Read_stream)            -> EQ
-  | (Read_stream, Read_tag)               -> LT
-  | (Read_stream, Read_tag_reserve)       -> LT
-                                               
-  | (Read_tag, Read_plain)             -> GT
-  | (Read_tag, Read_reserve)           -> GT
-  | (Read_tag, Read_acquire)           -> GT
-  | (Read_tag, Read_exclusive)         -> GT
-  | (Read_tag, Read_exclusive_acquire) -> GT
-  | (Read_tag, Read_stream)            -> GT
-  | (Read_tag, Read_tag)               -> EQ
-  | (Read_tag, Read_tag_reserve)       -> LT
-                                               
-  | (Read_tag_reserve, Read_plain)             -> GT
-  | (Read_tag_reserve, Read_reserve)           -> GT
-  | (Read_tag_reserve, Read_acquire)           -> GT
-  | (Read_tag_reserve, Read_exclusive)         -> GT
-  | (Read_tag_reserve, Read_exclusive_acquire) -> GT
-  | (Read_tag_reserve, Read_stream)            -> GT
-  | (Read_tag_reserve, Read_tag)               -> GT
-  | (Read_tag_reserve, Read_tag_reserve)       -> EQ
-  end
+end
 let inline {ocaml} read_kindCompare = defaultCompare
 
 let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
@@ -629,57 +593,31 @@ let ~{ocaml} write_kindCompare wk1 wk2 =
   | (Write_plain, Write_release)           -> LT
   | (Write_plain, Write_exclusive)         -> LT
   | (Write_plain, Write_exclusive_release) -> LT
-  | (Write_plain, Write_tag)               -> LT
-  | (Write_plain, Write_tag_conditional)   -> LT
 
   | (Write_conditional, Write_plain)             -> GT
   | (Write_conditional, Write_conditional)       -> EQ
   | (Write_conditional, Write_release)           -> LT
   | (Write_conditional, Write_exclusive)         -> LT
   | (Write_conditional, Write_exclusive_release) -> LT
-  | (Write_conditional, Write_tag)               -> LT
-  | (Write_conditional, Write_tag_conditional)   -> LT
 
   | (Write_release, Write_plain)             -> GT
   | (Write_release, Write_conditional)       -> GT
   | (Write_release, Write_release)           -> EQ
   | (Write_release, Write_exclusive)         -> LT
   | (Write_release, Write_exclusive_release) -> LT
-  | (Write_release, Write_tag)               -> LT
-  | (Write_release, Write_tag_conditional)   -> LT
 
   | (Write_exclusive, Write_plain)             -> GT
   | (Write_exclusive, Write_conditional)       -> GT
   | (Write_exclusive, Write_release)           -> GT
   | (Write_exclusive, Write_exclusive)         -> EQ
   | (Write_exclusive, Write_exclusive_release) -> LT
-  | (Write_exclusive, Write_tag)               -> LT
-  | (Write_exclusive, Write_tag_conditional)   -> LT
 
   | (Write_exclusive_release, Write_plain)             -> GT
   | (Write_exclusive_release, Write_conditional)       -> GT
   | (Write_exclusive_release, Write_release)           -> GT
   | (Write_exclusive_release, Write_exclusive)         -> GT
   | (Write_exclusive_release, Write_exclusive_release) -> EQ
-  | (Write_exclusive_release, Write_tag)               -> LT
-  | (Write_exclusive_release, Write_tag_conditional)   -> LT
-
-  | (Write_tag, Write_plain)             -> GT
-  | (Write_tag, Write_conditional)       -> GT
-  | (Write_tag, Write_release)           -> GT
-  | (Write_tag, Write_exclusive)         -> GT
-  | (Write_tag, Write_exclusive_release) -> GT
-  | (Write_tag, Write_tag)               -> EQ
-  | (Write_tag, Write_tag_conditional)   -> LT
-
-  | (Write_tag_conditional, Write_plain)             -> GT
-  | (Write_tag_conditional, Write_conditional)       -> GT
-  | (Write_tag_conditional, Write_release)           -> GT
-  | (Write_tag_conditional, Write_exclusive)         -> GT
-  | (Write_tag_conditional, Write_exclusive_release) -> GT
-  | (Write_tag_conditional, Write_tag)               -> GT
-  | (Write_tag_conditional, Write_tag_conditional)   -> EQ
-  end
+end
 let inline {ocaml} write_kindCompare = defaultCompare
 
 let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
@@ -778,9 +716,11 @@ end
 
 type event = 
 | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
+| E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name)
+| E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_footprint 
 | E_read_reg of reg_name
@@ -793,11 +733,14 @@ let eventCompare e1 e2 =
   match (e1,e2) with
   | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) ->
      compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
+  | (E_read_memt rk1 v1 i1 tr1, E_read_memt rk2 v2 i2 tr2) ->
+     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
   | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> 
     compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
   | (E_write_ea wk1 a1 i1 tr1, E_write_ea wk2 a2 i2 tr2) ->
     compare (wk1, (a1, i1, tr1)) (wk2, (a2, i2, tr2))
   | (E_write_memv _ mv1 tr1, E_write_memv _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
+  | (E_write_memvt _ mv1 tr1, E_write_memvt _ mv2 tr2) -> compare (mv1,tr1) (mv2,tr2)
   | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
   | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
   | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)
diff --git a/src/lexer.mll b/src/lexer.mll
index 98c9098d..bc8a1434 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -117,8 +117,10 @@ let kw_table =
      ("rreg",                    (fun x -> Rreg));
      ("wreg",                    (fun x -> Wreg));
      ("rmem",                    (fun x -> Rmem));
+     ("rmemt",                   (fun x -> Rmemt));
      ("wmem",                    (fun x -> Wmem));
      ("wmv",                     (fun x -> Wmv));
+     ("wmvt",                    (fun x -> Wmvt));
      ("eamem",                   (fun x -> Eamem));
      ("undef",                   (fun x -> Undef));
      ("unspec",                  (fun x -> Unspec));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 2e72761e..5b51439d 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -77,8 +77,10 @@ base_effect_aux =  (* effect *)
    BE_rreg (* read register *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
+ | BE_rmemt (* read memory tagged *)
  | BE_wmem (* write memory *)
  | BE_wmv (* write memory value *)
+ | BE_wmvt (* write memory value + tag *)
  | BE_eamem (* address for write signaled *)
  | BE_barr (* memory barrier *)
  | BE_depend (* dynmically dependent footprint *)
diff --git a/src/parser.mly b/src/parser.mly
index d172f61b..fae8d33f 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -132,7 +132,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order 
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
 %token Undefined Union With Val
-%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet Escape
+%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Undef Unspec Nondet Escape
 
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -309,10 +309,14 @@ effect:
     { efl BE_wreg }
   | Rmem
     { efl BE_rmem } 
+  | Rmemt
+    { efl BE_rmemt } 
   | Wmem
     { efl BE_wmem }
   | Wmv
     { efl BE_wmv }
+  | Wmvt
+    { efl BE_wmvt }
   | Eamem
     { efl BE_eamem }
   | Undef
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index e90d9cf1..8422ab11 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -88,8 +88,10 @@ let doc_effect (BE_aux (e,_)) =
   | BE_rreg -> "rreg"
   | BE_wreg -> "wreg"
   | BE_rmem -> "rmem"
+  | BE_rmemt -> "rmemt"
   | BE_wmem -> "wmem"
   | BE_wmv  -> "wmv"
+  | BE_wmvt  -> "wmvt"
   | BE_eamem -> "eamem"
   | BE_barr -> "barr"
   | BE_depend -> "depend"
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index b55685f4..92735f87 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -125,7 +125,7 @@ let effectful (Effect_aux (eff,_)) =
      List.exists
        (fun (BE_aux (eff,_)) ->
          match eff with
-         | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_wmv
+         | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem | BE_wmv | BE_wmvt
          | BE_barr | BE_depend | BE_nondet | BE_escape -> true
          | _ -> false)
        effs
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 03b8bdf5..54a6168e 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -181,8 +181,10 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
     | BE_rreg -> "BE_rreg"
     | BE_wreg -> "BE_wreg"
     | BE_rmem -> "BE_rmem"
+    | BE_rmemt -> "BE_rmemt"
     | BE_wmem -> "BE_wmem"
     | BE_wmv  -> "BE_wmv"
+    | BE_wmvt  -> "BE_wmvt"
     | BE_eamem -> "BE_eamem"
     | BE_barr -> "BE_barr"
     | BE_depend -> "BE_depend"
diff --git a/src/pretty_print_t_ascii.ml b/src/pretty_print_t_ascii.ml
index 79897f4b..1313fb37 100644
--- a/src/pretty_print_t_ascii.ml
+++ b/src/pretty_print_t_ascii.ml
@@ -96,8 +96,10 @@ and pp_format_base_effect_ascii (BE_aux(e,l)) =
     | BE_rreg -> "rreg"
     | BE_wreg -> "wreg"
     | BE_rmem -> "rmem"
+    | BE_rmemt -> "rmemt"
     | BE_wmem -> "wmem"
     | BE_wmv  -> "wmv"
+    | BE_wmvt  -> "wmvt"
     | BE_eamem -> "eamem"
     | BE_barr -> "barr"
     | BE_depend -> "depend"
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 2eaef407..0459c906 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -382,8 +382,10 @@ and ef_to_string (Ast.BE_aux(b,l)) =
       | Ast.BE_rreg  -> "rreg"
       | Ast.BE_wreg  -> "wreg"
       | Ast.BE_rmem  -> "rmem"
+      | Ast.BE_rmemt -> "rmemt"
       | Ast.BE_wmem  -> "wmem"
       | Ast.BE_wmv   -> "wmv"
+      | Ast.BE_wmvt  -> "wmvt"
       | Ast.BE_eamem -> "eamem"
       | Ast.BE_barr  -> "barr"
       | Ast.BE_undef -> "undef"
@@ -3075,12 +3077,18 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
   | (BE_rmem,BE_rmem) -> 0
   | (BE_rmem,_) -> -1
   | (_,BE_rmem) -> 1
+  | (BE_rmemt,BE_rmemt) -> 0
+  | (BE_rmemt,_) -> -1
+  | (_,BE_rmemt) -> 1
   | (BE_wmem,BE_wmem) -> 0
   | (BE_wmem,_) -> -1
   | (_,BE_wmem) -> 1
   | (BE_wmv,BE_wmv) -> 0
   | (BE_wmv, _ ) -> -1
   | (_,BE_wmv) -> 1
+  | (BE_wmvt,BE_wmvt) -> 0
+  | (BE_wmvt, _ ) -> -1
+  | (_,BE_wmvt) -> 1
   | (BE_eamem,BE_eamem) -> 0
   | (BE_eamem,_) -> -1
   | (_,BE_eamem) -> 1
@@ -3139,9 +3147,11 @@ let has_effect searched_for eff =
 let has_rreg_effect = has_effect (BE_aux(BE_rreg, Parse_ast.Unknown))
 let has_wreg_effect = has_effect (BE_aux(BE_wreg, Parse_ast.Unknown))
 let has_rmem_effect = has_effect (BE_aux(BE_rmem, Parse_ast.Unknown))
+let has_rmemt_effect = has_effect (BE_aux(BE_rmemt, Parse_ast.Unknown))
 let has_wmem_effect = has_effect (BE_aux(BE_wmem, Parse_ast.Unknown))
 let has_eamem_effect = has_effect (BE_aux(BE_eamem, Parse_ast.Unknown))
 let has_memv_effect = has_effect (BE_aux(BE_wmv, Parse_ast.Unknown))
+let has_memvt_effect = has_effect (BE_aux(BE_wmvt, Parse_ast.Unknown))
 let has_lret_effect = has_effect (BE_aux(BE_lret, Parse_ast.Unknown))
 
 (*Similarly to above.*)
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 4912585a..11aff1ee 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -248,9 +248,11 @@ val e_to_string : effect -> string
 val has_rreg_effect : effect -> bool
 val has_wreg_effect : effect -> bool
 val has_rmem_effect : effect -> bool
+val has_rmemt_effect : effect -> bool
 val has_wmem_effect : effect -> bool
 val has_eamem_effect : effect -> bool
 val has_memv_effect : effect -> bool
+val has_memvt_effect : effect -> bool
 val has_lret_effect : effect -> bool
   
 val initial_kind_env : kind Envmap.t