diff --git a/theories/lang/steps_retag.v b/theories/lang/steps_retag.v
index 49bd4bdf3b8edd30e1df184a4a7a3d0ff299d6dc..da257628100087edf46a6d10bd64d3e85fddf25c 100644
--- a/theories/lang/steps_retag.v
+++ b/theories/lang/steps_retag.v
@@ -761,6 +761,27 @@ Proof.
       right; (split; [lia|done]).
 Qed.
 
+Lemma retag_change_tag α cids c nxtp l otag ntag rk pk T α' nxtp' :
+  retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') →
+  ntag = otag ∨
+  match ntag with
+  | Tagged t => t = nxtp ∧ nxtp' = S nxtp
+  | _ => True
+  end.
+Proof.
+  intros RT.
+  destruct (retag_change_case _ _ _ _ _ _ _ _ _ _ _ _ RT) as [[?[?[??]]]|[? Eq]].
+  - simplify_eq; by left.
+  - destruct pk.
+    + apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag.
+    + destruct rk.
+      * left. by destruct Eq as [_ []]; subst.
+      * left. by destruct Eq as [_ []]; subst.
+      * apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag.
+      * left. by destruct Eq as [_ []]; subst.
+    + apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag.
+Qed.
+
 Lemma retag_change_nxtp α cids c nxtp l otag ntag rk pk T α' nxtp' :
   retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') →
   (nxtp ≤ nxtp')%nat.
@@ -1546,3 +1567,90 @@ Proof.
     case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
     move : GR. eapply grant_head_preserving; eauto.
 Qed.
+
+Lemma grant_active_SRW stk old it cids stk' it'
+  (SRW: it.(perm) = SharedReadWrite) :
+  grant stk old it cids = Some stk' →
+  it' ∈ stk → it' ∈ stk'.
+Proof.
+  rewrite /grant. case find_granting as [[n p]|]; [|done].
+  rewrite /= SRW.
+  case find_first_write_incompatible as [n'|]; [|done].
+  rewrite /= => ?. simplify_eq.
+  destruct (item_insert_dedup_case stk it n') as [EQ|EQ]; rewrite EQ; [|done].
+  rewrite -{1}(take_drop n' stk). set_solver.
+Qed.
+
+Lemma grant_active_non_SRW stk old it cids stk' t pm c
+  (SRW: it.(perm) ≠ SharedReadWrite)
+  (Inc: c ∈ cids) :
+  grant stk old it cids = Some stk' →
+  let it' := mkItem pm t (Some c) in
+  it' ∈ stk → it' ∈ stk'.
+Proof.
+  rewrite /grant. case find_granting as [[n p]|] eqn:FR; [|done].
+  case it.(perm) eqn:Eqp; [|done|..|];
+    cbn -[item_insert_dedup];
+    (case access1 as [[n' stk1]|] eqn:ACC; [|done]);
+    cbn -[item_insert_dedup];
+    intros ?; simplify_eq;
+    move => /(access1_active_preserving _ _ _ _ _ _ ACC _ _ _ Inc);
+    (destruct (item_insert_dedup_case stk1 it O) as [EQ|EQ]; rewrite EQ; [|done]);
+    rewrite -{1}(take_drop 0 stk1); set_solver.
+Qed.
+
+Lemma grant_active_preserving stk old it cids stk' t pm c (Inc: c ∈ cids) :
+  grant stk old it cids = Some stk' →
+  let it' := mkItem pm t (Some c) in
+  it' ∈ stk → it' ∈ stk'.
+Proof.
+  case (decide (it.(perm) = SharedReadWrite)) => ?.
+  - by apply grant_active_SRW.
+  - by eapply grant_active_non_SRW.
+Qed.
+
+Lemma retag_item_active_preserving α nxtp c cids l old rk pk T new α' nxtp' :
+  retag α nxtp cids c l old rk pk T = Some (new, α', nxtp') →
+  ∀ l' stk t' c' pm,
+    α !! l' = Some stk →
+    c' ∈ cids →
+    let it' := mkItem pm t' (Some c') in
+    it' ∈ stk →
+    ∃ stk', α' !! l' = Some stk' ∧ it' ∈ stk'.
+Proof.
+  intros RT l' stk t' c' pm Eqstk Inc' it' IN.
+  destruct (retag_Some _ _ _ _ _ _ _ _ _ _ _ _ RT) as [NEQ EQ].
+  destruct (block_case l l' (tsize T)) as [?|(i & Lti & ?)].
+  { rewrite NEQ //. naive_solver. }
+  assert (∃ sz, tsize T = S sz) as [sz Eqsz].
+  { destruct (tsize T); [lia|by eexists]. }
+  subst l'.
+  move : RT. rewrite /retag /= /retag_ref Eqsz.
+  destruct pk as [[]|[]|].
+  - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR).
+    simplify_eq.
+    case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
+    exists stk2. split; [done|].
+    move : Inc' GR IN. by apply grant_active_preserving.
+  - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & b & GR).
+    simplify_eq.
+    case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
+    exists stk2. split; [done|].
+    move : Inc' GR IN. by apply grant_active_preserving.
+  - destruct rk; [by intros; simplify_eq; naive_solver..|
+                  |intros; simplify_eq; naive_solver].
+    specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq.
+    case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
+    exists stk2. split; [done|].
+    move : Inc' GR IN. by apply grant_active_preserving.
+  - destruct rk; [by intros; simplify_eq; naive_solver..|
+                  |intros; simplify_eq; naive_solver].
+    specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & b & GR). simplify_eq.
+    case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
+    exists stk2. split; [done|].
+    move : Inc' GR IN. by apply grant_active_preserving.
+  - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq.
+    case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
+    exists stk2. split; [done|].
+    move : Inc' GR IN. by apply grant_active_preserving.
+Qed.
diff --git a/theories/sim/cmra.v b/theories/sim/cmra.v
index 1195a98b7ccff81add569df699ba7f3e4bbaf74b..66ca288659019bab248c217a87565c81c6ba512e 100644
--- a/theories/sim/cmra.v
+++ b/theories/sim/cmra.v
@@ -293,6 +293,18 @@ Proof.
   by apply cmra_included_r.
 Qed.
 
+Lemma tmap_lookup_op_l_equiv_pub (pm1 pm2: tmapUR) t h1
+  (VALID: ✓ (pm1 ⋅ pm2)):
+  pm1 !! t ≡ Some (to_tgkR tkPub, h1) →
+  ∃ h2, (pm1 ⋅ pm2) !! t ≡ Some (to_tgkR tkPub, h1 ⋅ h2).
+Proof.
+  intros HL. move : (VALID t). rewrite lookup_op.
+  destruct (pm2 !! t) as [[k2 h2]|] eqn:Eqt; rewrite Eqt; rewrite -> HL.
+  - rewrite -Some_op pair_op. move => [ VL1 ?]. exists h2. simpl in VL1.
+    rewrite HL -Some_op pair_op.
+    by rewrite -(tagKindR_incl_eq (to_tgkR tkPub) _ VL1 (cmra_included_r _ _)).
+  - intros _. exists (∅: gmap loc _). by rewrite 2!right_id HL.
+Qed.
 
 Lemma tmap_lookup_op_r_equiv_pub (pm1 pm2: tmapUR) t h2
   (VALID: ✓ (pm1 ⋅ pm2)):
diff --git a/theories/sim/invariant.v b/theories/sim/invariant.v
index 557c1b9bbc8647acba528cda758befb6081a6fb2..5c7fbd78543e795efdc9be38d6fabda5456ecf95 100644
--- a/theories/sim/invariant.v
+++ b/theories/sim/invariant.v
@@ -57,7 +57,7 @@ Definition tmap_inv (r: resUR) (σs σt: state) : Prop :=
     (* If [k] ls Local, then the stack is a singleton.
       If [k] is Unique, then [t] must be Unique at the top of [stk].
       Otherwise if [k] is Pub, then [t] can be among the top SRO items. *)
-    tmap_inv_post  k t l σt.
+    tmap_inv_post k t l σt.
 
 Definition cmap_inv (r: resUR) (σ: state) : Prop :=
   ∀ (c: call_id) (T: tag_locs), r.(rcm) !! c ≡ Excl' T →
diff --git a/theories/sim/refl.v b/theories/sim/refl.v
index ee6ed26dd375a79f0b7d9ed4d2e77f00603a41e1..4a5f07054fb79978bfe8fd0a1fd43c4a56507148 100644
--- a/theories/sim/refl.v
+++ b/theories/sim/refl.v
@@ -297,8 +297,8 @@ Proof using Type*.
     sim_bind (subst_map _ e) (subst_map _ e).
     eapply sim_simple_post_mono, IHe; [|by auto..].
     intros r' n' rs rt (-> & Hrel). simpl.
-    eapply sim_simple_retag_public; eauto.
-    split; first done. constructor; done.
+    eapply sim_simple_valid_post.
+    by eapply sim_simple_retag_public; eauto.
   - (* Let *)
     move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
     eapply sim_simple_frame_core.
diff --git a/theories/sim/refl_mem_step.v b/theories/sim/refl_mem_step.v
index 61a6889d20c1f30e47cff37928c287f461c3eaaa..bdd43a0e0fcdd02eece87f474fd8df2775f82b99 100644
--- a/theories/sim/refl_mem_step.v
+++ b/theories/sim/refl_mem_step.v
@@ -1206,13 +1206,14 @@ Qed.
 (** Retag *)
 Lemma sim_body_retag_public fs ft r n ptr pk T kind σs σt Φ
   (RREL: rrel r ptr ptr) :
-  (∀ l otg ntg α' nxtp' c cids,
+  (∀ l otg ntg α' nxtp' c cids r',
     ptr = ValR [ScPtr l otg] →
     σt.(scs) = c :: cids →
     retag σt.(sst) σt.(snp) σt.(scs) c l otg kind pk T = Some (ntg, α', nxtp') →
+    vrel (r ⋅ r') [ScPtr l ntg] [ScPtr l ntg] →
     let σs' := mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc) in
     let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in
-    Φ r n (ValR [ScPtr l ntg]) σs' (ValR [ScPtr l ntg]) σt') →
+    Φ (r ⋅ r') n (ValR [ScPtr l ntg]) σs' (ValR [ScPtr l ntg]) σt') →
   r ⊨{n,fs,ft}
     (Retag ptr pk T kind, σs) ≥
     (Retag ptr pk T kind, σt) : Φ.
@@ -1250,20 +1251,65 @@ Proof.
     - rewrite Eqcs; eauto.
     - by rewrite Eqsst Eqnp Eqcs. }
 
-  exists (#[ScPtr l ntg])%V, σs', r, n. subst σt'.
+  have HNP := wsat_tmap_nxtp _ _ _ WSAT1.
+  have Eqtg := retag_change_tag _ _ _ _ _ _ _ _ _ _ _ _ EqRT.
+  set r' : resUR := if (decide (ntg = otg)) then ε else
+                    match ntg with
+                    | Tagged t => res_tag t tkPub ∅
+                    | _ => ε
+                    end.
+
+  have VALID': ✓ (r_f ⋅ r ⋅ r').
+  { rewrite /r'. case decide => ?; [by rewrite right_id|].
+    destruct Eqtg as [|Eqtg]; [by subst|].
+    destruct ntg; [destruct Eqtg; subst t|by rewrite right_id].
+    apply (local_update_discrete_valid_frame (r_f ⋅ r) ε);
+      [by rewrite right_id|]. rewrite right_id.
+    by apply res_tag_alloc_local_update. }
+  have Eqc': (r_f ⋅ r ⋅ r').(rcm)  ≡ (r_f ⋅ r).(rcm).
+  { rewrite /r'.
+    case decide => ?; [by rewrite right_id|].
+    destruct ntg; by rewrite /= right_id. }
+  have HLt: ∀ t kh, (r_f ⋅ r).(rtm) !! t ≡ Some kh →
+                    (r_f ⋅ r ⋅ r').(rtm) !! t ≡ Some kh.
+  { intros t kh Eqt. rewrite /r'.
+    case decide => ?; [by rewrite right_id|].
+    destruct Eqtg as [|Eqtg]; [by subst|].
+    destruct ntg as [t1|];
+      [destruct Eqtg; subst t1 nxtp'|by rewrite right_id].
+    rewrite lookup_op res_tag_lookup_ne.
+    - by rewrite right_id.
+    - intros ?. subst t. rewrite HNP in Eqt. inversion Eqt. }
+
+  (* unfolding rrel for place *)
+  simpl in RREL.
+  inversion RREL as [|???? AREL _]; subst; simplify_eq. clear RREL.
+
+  exists (#[ScPtr l ntg])%V, σs', (r ⋅ r'), n.
   split; last split.
   { left. by constructor. }
-  { (* unfolding rrel for place *)
-    simpl in RREL.
-    inversion RREL as [|???? AREL _]; subst; simplify_eq. clear RREL.
-
-    have Lenp: (σt.(snp) ≤ nxtp')%nat by apply retag_change_nxtp in EqRT.
+  { have Lenp: (σt.(snp) ≤ nxtp')%nat by apply retag_change_nxtp in EqRT.
     split; last split; last split; last split; last split.
     - by apply (tstep_wf _ _ _ STEPS WFS).
     - by apply (tstep_wf _ _ _ STEPT WFT).
-    - done.
+    - by rewrite cmra_assoc.
     - intros t' k' h' Eqt'.
-      specialize (PINV _ _ _ Eqt') as [Ltp PINV].
+      have Eqh': (r_f ⋅ r).(rtm) !! t' ≡ Some (to_tgkR k', h') ∨
+                 t' = σt.(snp) ∧ nxtp' = S σt.(snp) ∧ h' ≡ ∅.
+      { move : Eqt'. rewrite /r'.
+        case decide => ?; [by rewrite right_id; left|].
+        destruct Eqtg as [|Eqtg]; [by subst|].
+        destruct ntg as [t1|];
+          [destruct Eqtg; subst t1 nxtp'|by rewrite right_id; left].
+        rewrite cmra_assoc lookup_op.
+        case (decide (t' = σt.(snp))) => ?; [subst t'|].
+        - rewrite res_tag_lookup. rewrite HNP left_id fmap_empty.
+          intros [Eq1 Eq2]%Some_equiv_inj. by right.
+        - rewrite res_tag_lookup_ne // right_id. by left. }
+      destruct Eqh' as [Eqt|(?&?&Eqh')]; last first.
+      { subst t' nxtp'. split; [simpl; lia|].
+        intros l' ss st. rewrite Eqh' lookup_empty. by inversion 1. }
+      specialize (PINV _ _ _ Eqt) as [Ltp PINV].
       split; [by simpl; lia|].
       intros l1 ss st Eql1 PRE. specialize (PINV _ _ _ Eql1).
       destruct k'.
@@ -1272,7 +1318,7 @@ Proof.
         have NEq: otg ≠ Tagged t'.
         { intros ?. subst otg. simpl in AREL.
           destruct AREL as (_ & _ & ht & Eqh').
-          move : Eqt'. rewrite lookup_op Eqh'.
+          move : Eqt. rewrite lookup_op Eqh'.
           apply tagKindR_local_exclusive_r. }
         move : NEq Eqstk.
         by eapply retag_Some_local.
@@ -1293,7 +1339,7 @@ Proof.
         have NEq: Tagged t' ≠ otg.
         { intros ?. subst otg. simpl in AREL.
           destruct AREL as (_ & _ & ht & Eqh').
-          move : Eqt'. rewrite lookup_op Eqh'.
+          move : Eqt. rewrite lookup_op Eqh'.
           apply tagKindR_uniq_exclusive_r. }
         move : HTOP.
         by apply (retag_item_head_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT
@@ -1310,21 +1356,38 @@ Proof.
         have ND2 := proj2 (state_wf_stack_item _ WFT _ _ Eqstk1).
         by apply (retag_item_active_SRO_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT
                     _ _ _ _ _ ND2 Eqstk1 Eqstk' In In').
-    - intros c1 Tc Eqc. specialize (CINV _ _ Eqc) as [Ltc CINV].
+    - intros c1 Tc. rewrite cmra_assoc Eqc'. intros Eqc.
+      specialize (CINV _ _ Eqc) as [Ltc CINV].
       split; [done|].
       intros tc L EqL. specialize (CINV _ _ EqL) as [Ltp CINV].
       split; [by simpl; lia|].
       intros l1 InL. simpl.
       specialize (CINV _ InL) as (stk & pm & Eqstk & In & NDIS).
-      (* Prove that this is active (protector) preserving *)
-      (* destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ EqRT _ _ t' _ Eqstk' In')
-          as (stk & Eqstk & In); [done..|]. *)
-      admit.
-    - done. }
+      destruct (retag_item_active_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT
+                    _ _ _ _ _ Eqstk Ltc In) as (stk' & Eqstk' & In').
+      by exists stk', pm.
+    - rewrite cmra_assoc. do 4 (split; [done|]).
+      move => l' /PUBP [PB|PV].
+      + left.  move => ? /PB [? [? AREL']]. eexists. split; [done|].
+        eapply arel_mono; [done|..|exact AREL']. apply cmra_included_l.
+      + right. destruct PV as (t & k1 & h1 & Eqt & ?).
+        exists t, k1, h1. setoid_rewrite Eqc'. split; [|done].
+        by apply HLt. }
 
   left.
-  apply: sim_body_result. intros. eapply POST; eauto.
-Abort.
+  apply: sim_body_result. intros VALIDr. eapply POST; eauto.
+  constructor; [|done]. do 2 (split; [done|]).
+  destruct ntg; [|done]. destruct AREL as (_ & _ & AREL).
+  rewrite /r'.
+  case decide => ?; [subst otg|].
+  - destruct AREL as [h1 ?]. exists h1. by rewrite right_id.
+  - destruct Eqtg as [|[]]; [by subst otg|subst t].
+    destruct (tmap_lookup_op_r_equiv_pub r.(rtm)
+                (res_tag σt.(snp) tkPub ∅).(rtm) σt.(snp) (to_agree <$> ∅)).
+    + move : VALIDr. rewrite /r' decide_False // => VALIDr. apply VALIDr.
+    + apply res_tag_lookup.
+    + by eexists.
+Qed.
 
 Lemma sim_body_retag_mut_ref_default fs ft r r' rs n l told T σs σt Φ :
   (0 < tsize T)%nat →
diff --git a/theories/sim/simple.v b/theories/sim/simple.v
index 971b1b19ca302c1ba96763bdbc77d073c936d7f0..33aa272f3bd755b8c25cf09667883540bd58132d 100644
--- a/theories/sim/simple.v
+++ b/theories/sim/simple.v
@@ -385,11 +385,14 @@ Qed.
 
 Lemma sim_simple_retag_public fs ft r n (rs rt: result) pk T rk Φ :
   rrel r rs rt →
-  (Φ r n (ValR [☠%S]) (ValR [☠%S])) →
+  (∀ l old new rt, rs = ValR [ScPtr l old] →
+    vrel (r ⋅ rt) [ScPtr l new] [ScPtr l new] →
+    Φ (r ⋅ rt) n (ValR [ScPtr l new]) (ValR [ScPtr l new])) →
   r ⊨ˢ{n,fs,ft} Retag rs pk T rk ≥ Retag rt pk T rk : Φ.
 Proof.
-  intros [Hrel ?]%rrel_with_eq. simplify_eq.
-Admitted.
+  intros [Hrel ?]%rrel_with_eq HH σs σt. simplify_eq.
+  eapply sim_body_retag_public; eauto.
+Qed.
 
 (** * Pure *)
 Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 Φ :