Merge branch 'master' of bitbucket.org:Peter_Sewell/sail

# Conflicts:
#	src/lem_interp/interp.lem
#	src/lem_interp/interp_inter_imp.lem
#	src/lem_interp/interp_interface.lem
#	src/parser.mly
#	src/pretty_print_lem.ml

24 files changed, 225 insertions, 148 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 186d7f9a..c923ae3f 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -117,10 +117,12 @@ 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_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | 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/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index a0b8e514..e2ddd3e9 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -577,18 +577,9 @@ let minus_big = arith_op sub_big_int
 let multiply_big = arith_op mult_big_int
 let min_big = arith_op min_big_int
 let max_big = arith_op max_big_int
- (* this implements truncation towards zero like C and unlike ocaml (consider r < 0) *)
-let quot_big (l, r) =
-  let q = div_big_int (abs_big_int l) (abs_big_int r) in
-  let lneg = lt_big_int l zero_big_int in
-  let rneg = lt_big_int r zero_big_int in
-  if (lneg <> rneg) then
-    minus_big_int q
-  else
-    q
-let modulo_big (l, r) = (* calculate mod given above quot *)
-  let q = quot_big (l, r) in
-  sub_big_int l (mult_big_int q r)
+(* NB Z.div is what we want because it does truncation towards zero unlike Big_int_Z.div_big_int == Z.ediv *)
+let quot_big = arith_op (Z.div)
+let modulo_big = arith_op (Z.rem)
 
 let power_big = arith_op power_big
 
@@ -597,17 +588,7 @@ let add_signed_int = arith_op (+)
 let minus_int = arith_op (-)
 let multiply_int = arith_op ( * )
 let modulo_int = arith_op (mod)
-let quot_int (l, r) = 
-  let q = (abs l) / (abs r) in
-  let lneg = l < 0 in
-  let rneg = r < 0 in
-  if (lneg <> rneg) then
-    -q
-  else
-    q
-let modulo_int (l, r) = 
-  let q = quot_int (l, r) in
-  l - (r * q)
+let quot_int = arith_op (/)
 
 let power_int = arith_op power_int
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index a0d4d312..0e37b418 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_exmem  -> BE_exmem
 			       | Parse_ast.BE_depend -> BE_depend
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 4de1e869..23e2160b 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -356,10 +356,12 @@ 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
  | Excl_res of id * value
+ | Write_memv_tagged of id * value * value * value
  | Barrier of id * value
  | Footprint of id * value
  | Nondet of list (exp tannot) * tag
@@ -2228,6 +2230,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
@@ -2254,6 +2258,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)
@@ -2387,6 +2396,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
@@ -3050,6 +3060,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 6091e8b1..b706d3aa 100644
--- a/src/lem_interp/interp_ast.lem
+++ b/src/lem_interp/interp_ast.lem
@@ -119,10 +119,12 @@ 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_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | 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 3e71ba37..280b1097 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,6 +427,8 @@ 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 _ _) _,_,_) ->
@@ -434,6 +437,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
       (Ivh_error (Interp_interface.Internal_error ("Exclusive result 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
 
@@ -457,7 +462,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
@@ -501,7 +506,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
@@ -586,7 +591,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
@@ -597,7 +601,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
@@ -643,7 +646,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
@@ -668,7 +671,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
@@ -705,7 +708,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
@@ -720,7 +723,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) = 
@@ -747,7 +750,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
@@ -757,7 +760,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 excl_res 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 excl_res 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)
@@ -786,6 +789,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)) -> 
@@ -842,6 +858,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 -> 
@@ -909,7 +944,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 excl_res) = context in
+  let (Context _ direction externs reads reads_tagged writes write_eas write_vals write_vals_tagged barriers excl_res) = context in
   let unknown_reg size =  
     <| rv_bits = (List.replicate size Bitl_unknown);
        rv_start = 0;
@@ -937,6 +972,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
@@ -955,6 +993,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)
@@ -1093,10 +1136,12 @@ 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_excl_res -> Nothing
   | E_write_memv _ _ _ -> Nothing
+  | E_write_memvt _ _ _ -> Nothing
   | E_barrier bk -> Just (IK_barrier bk)
   | E_footprint -> Nothing
   | E_read_reg _ -> Nothing
@@ -1109,10 +1154,12 @@ 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_excl_res -> []
   | E_write_memv _ _ _ -> []
+  | E_write_memvt _ _ _ -> []
   | E_barrier _ -> []
   | E_footprint -> []
   | E_read_reg r -> [r]
@@ -1123,10 +1170,12 @@ 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_excl_res -> []
   | E_write_memv _ _ _ -> []
+  | E_write_memvt _ _ _ -> []
   | E_barrier _ -> []
   | E_footprint -> []
   | E_read_reg _ -> []
@@ -1139,12 +1188,15 @@ 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_excl_res                       -> []
   | 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 77572de9..0ce7b43a 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -179,6 +179,8 @@ 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))
@@ -187,11 +189,13 @@ and memory_write_val = MV of optional_memory_transformer * (maybe (instruction_s
 and memory_write_vals = list (string * memory_write_val)
 and excl_res_t = ER of maybe (instruction_state -> bool -> instruction_state)
 and excl_res = maybe (string * excl_res_t)
+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 * excl_res * external_functions
+	memory_reads * memory_read_taggeds * memory_writes * memory_write_eas * memory_write_vals * memory_write_vals_tagged * barriers * excl_res * external_functions
 
 (* An instruction in flight *)
 and instruction_state = IState of interpreter_state * context
@@ -201,6 +205,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)
@@ -214,6 +219,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
@@ -253,7 +259,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 -> excl_res -> 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 -> excl_res -> 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 2c338ff7..4e8c1111 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_exmem,BE_exmem)   -> true
     | (BE_barr,BE_barr)     -> true 
@@ -129,11 +132,13 @@ 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_exmem_effect = has_effect BE_exmem
 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 855658b4..b019fb53 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_exmem -> "exmem"
   | BE_barr -> "barr"
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 01c828dd..f0c0d392 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) ^
@@ -440,6 +444,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 600699ec..d6f6e30c 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 fad04a51..0cdeb414 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,10 +716,12 @@ 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_excl_res
 | 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
@@ -794,12 +734,15 @@ 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_excl_res, E_excl_res) -> EQ
   | (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 921be112..7f11355f 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));
      ("exmem",                   (fun x -> Exmem));
      ("undef",                   (fun x -> Undef));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 68ebbf9b..e069462a 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_exmem (* determine if a store-exclusive (ARM) is going to succeed *)
  | BE_barr (* memory barrier *)
diff --git a/src/parser.mly b/src/parser.mly
index fce6ff9d..bd68cfdc 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 Exmem Undef Unspec Nondet Escape
+%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem 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 }
   | Exmem
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 51cf070b..3699e1ac 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_exmem -> "exmem"
   | BE_barr -> "barr"
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a436cf90..673c286b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -125,8 +125,9 @@ 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_exmem
-         | BE_wmv | BE_barr | BE_depend | BE_nondet | BE_escape -> true
+         | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem
+         | BE_exmem | 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 268aeb2f..ef7a8b95 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_exmem -> "BE_exmem"
     | BE_barr -> "BE_barr"
diff --git a/src/pretty_print_t_ascii.ml b/src/pretty_print_t_ascii.ml
index 1494ca0a..273ceb29 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_exmem -> "exmem"
     | BE_barr -> "barr"
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 45630d3e..2932cf33 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_exmem -> "exmem"
       | Ast.BE_barr  -> "barr"
@@ -3076,12 +3078,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
@@ -3143,10 +3151,12 @@ 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_exmem_effect = has_effect (BE_aux(BE_exmem, 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 f6f196a9..ee2e3988 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -248,10 +248,12 @@ 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_exmem_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