diff --git a/theories/stacked_borrows/examples/opt1.v b/theories/stacked_borrows/examples/opt1.v
index a50bf1efb04b9d2afaa671605707fd64e46a402f..8a270ff406c6bd8872313eb32d92ae726e37debf 100644
--- a/theories/stacked_borrows/examples/opt1.v
+++ b/theories/stacked_borrows/examples/opt1.v
@@ -65,11 +65,11 @@ Proof.
   source_bind (Write _ _).
   (* gain knowledge about the length *)
   iApply source_red_irred_unless; first done. iIntros (Hsize).
-  iApply (source_write_local with "Htag Hs"); [by rewrite repeat_length | done | ].
+  iApply (source_write_local with "Htag Hs"); [by rewrite replicate_length | done | ].
   iIntros "Hs Htag". source_finish.
 
   target_bind (Write _ _).
-  iApply (target_write_local with "Htag Ht"); [ by rewrite repeat_length | lia| ].
+  iApply (target_write_local with "Htag Ht"); [ by rewrite replicate_length | lia| ].
   iIntros "Ht Htag". target_finish.
 
   sim_pures. iApply ("Hsim" with "[//] [] Htag Ht Hs").
@@ -101,11 +101,11 @@ Proof.
   { iApply source_red_irred_unless; first done. by iIntros. }
   (* gain knowledge about the length *)
   iApply source_red_irred_unless; first done. iIntros (Hsize).
-  iApply (source_write_local with "Htag Hs"); [by rewrite repeat_length | done | ].
+  iApply (source_write_local with "Htag Hs"); [by rewrite replicate_length | done | ].
   iIntros "Hs Htag". source_finish.
   iPoseProof (rrel_value_source with "Hrel") as (v_t) "(-> & #Hv)".
   iPoseProof (value_rel_length with "Hv") as "%Hlen".
-  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite repeat_length | lia| ].
+  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite replicate_length | lia| ].
   sim_pures.
 
   target_apply (Copy _) (target_copy_local with "Htag Ht") "Ht Htag"; first lia.
@@ -143,7 +143,7 @@ Proof.
   iApply (source_copy_any with "Htag_i Hi_s"); first done. iIntros (v_s') "%Hv_s' Hi_s Htag_i". source_finish.
   sim_pures.
 
-  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "". sim_pures.
+  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
   sim_val. iModIntro. destruct Hv_s' as [-> | ->]; iApply big_sepL2_singleton; done.
 Qed.
 
@@ -175,11 +175,11 @@ Proof.
   { iApply source_red_irred_unless; first done. by iIntros. }
   (* gain knowledge about the length *)
   iApply source_red_irred_unless; first done. iIntros (Hsize).
-  iApply (source_write_local with "Htag Hs"); [by rewrite repeat_length | done | ].
+  iApply (source_write_local with "Htag Hs"); [by rewrite replicate_length | done | ].
   iIntros "Hs Htag". source_finish.
   iPoseProof (rrel_value_source with "Hrel") as (v_t) "(-> & #Hv)".
   iPoseProof (value_rel_length with "Hv") as "%Hlen".
-  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite repeat_length | lia| ].
+  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite replicate_length | lia| ].
   sim_pures.
 
   target_apply (Copy _) (target_copy_local with "Htag Ht") "Ht Htag"; first lia.
@@ -221,11 +221,11 @@ Proof.
   (* resolve the deferred read in the source *)
   source_apply (Copy (Place _ _ _)) (source_copy_local with "Htag Hs") "Hs Htag"; first done.
   source_pures. source_bind (Copy _).
-  iApply (source_copy_resolve_deferred with "Htag_i Hi_s Hdeferred"); first done. 
-  { iApply big_sepL2_singleton. done. } 
+  iApply (source_copy_resolve_deferred with "Htag_i Hi_s Hdeferred"); first done.
+  { iApply big_sepL2_singleton. done. }
   iIntros (v_s') "Hv' Hi_s Htag_i". source_finish.
   sim_pures.
 
-  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "". sim_pures.
+  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
   sim_val. iModIntro. done.
 Qed.
diff --git a/theories/stacked_borrows/examples/opt1_down.v b/theories/stacked_borrows/examples/opt1_down.v
index 4f5314bcf7f8225882be362f2c81b77598e9a603..2e622c47c0958e998c9325a6b4aa5e7a772887bf 100644
--- a/theories/stacked_borrows/examples/opt1_down.v
+++ b/theories/stacked_borrows/examples/opt1_down.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 (* Assuming x : &mut i32 *)
 Definition ex1_down_unopt : ectx :=
   λ: "i",
-    let: "c" := InitCall in 
+    let: "c" := InitCall in
     (* "x" is the local variable that stores the pointer value "i" *)
     let: "x" := new_place (&mut int) "i" in
 
@@ -32,7 +32,7 @@ Definition ex1_down_unopt : ectx :=
 
 Definition ex1_down_opt : ectx :=
   λ: "i",
-    let: "c" := InitCall in 
+    let: "c" := InitCall in
     let: "x" := new_place (&mut int) "i" in
     retag_place "x" (RefPtr Mutable) int FnEntry "c";;
     Call #[ScFnPtr "f"] #[] ;;
@@ -75,7 +75,7 @@ Proof.
   iApply sim_irred_unless; first done.
   iIntros ((_ & ot & i & -> & _)).
   iPoseProof (value_rel_singleton_source with "Hv") as (sc_t) "[-> Hscrel]".
-  iPoseProof (sc_rel_ptr_source with "Hscrel") as "[-> Htagged]". 
+  iPoseProof (sc_rel_ptr_source with "Hscrel") as "[-> Htagged]".
   iApply (sim_retag_fnentry with "Hscrel Hcall"); [cbn; lia| done | ].
   iIntros (t_i v_t v_s Hlen_t Hlen_s) "#Hvrel Hcall Htag_i Hi_t Hi_s _".
   iApply sim_expr_base.
@@ -85,7 +85,7 @@ Proof.
 
   (* do the source load *)
   source_apply (Copy (Place _ _ _)) (source_copy_local with "Htag Hs") "Hs Htag"; first done.
-  source_pures. source_bind (Copy _).  
+  source_pures. source_bind (Copy _).
   iApply (source_copy_any with "Htag_i Hi_s"); first done. iIntros (v_s' Hv_s') "Hi_s Htag_i". source_finish.
   sim_pures.
 
@@ -95,31 +95,24 @@ Proof.
   (* do the target load *)
   target_apply (Copy (Place _ _ _)) (target_copy_local with "Htag Ht") "Ht Htag"; first done.
   target_pures. target_apply (Copy _) (target_copy_protected with "Hcall Htag_i Hi_t") "Hi_t Hcall Htag_i"; first done.
-  { simpl. intros i0 Hi0. assert (i0 = O) as -> by lia. eexists. split; first apply lookup_insert.  set_solver. } 
-  sim_pures. 
+  { simpl. intros i0 Hi0. assert (i0 = O) as -> by lia. eexists. split; first apply lookup_insert.  set_solver. }
+  sim_pures.
 
   (* cleanup: remove the protector ghost state, make the external locations public, free the local locations*)
-  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "". sim_pures.
+  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
   iApply (sim_protected_unprotectN with "Hcall Htag_i Hi_t Hi_s Hvrel"); [ | apply lookup_insert | ].
-  { simpl. cbn in Hlen_t. intros i' Hi'. replace i' with O by lia. rewrite elem_of_union elem_of_singleton. eauto. } 
+  { simpl. cbn in Hlen_t. intros i' Hi'. replace i' with O by lia. rewrite elem_of_union elem_of_singleton. eauto. }
   iIntros "Hcall Htag_i Hi_t Hi_s".
-  iApply (sim_remove_empty_calls _ t_i with "Hcall"). 
-  { rewrite lookup_insert. done. } 
-  { rewrite Hlen_t. set_solver. } 
+  iApply (sim_remove_empty_calls _ t_i with "Hcall").
+  { rewrite lookup_insert. done. }
+  { rewrite Hlen_t. set_solver. }
   iIntros "Hcall".
   sim_apply (EndCall _) (EndCall _) (sim_endcall with "[Hcall]") "".
-  { replace (delete t_i _) with (∅ : gmap ptr_id (gset loc)); first done. 
+  { replace (delete t_i _) with (∅ : gmap ptr_id (gset loc)); first done.
     apply map_eq. intros t'. rewrite delete_insert_delete delete_insert; done.
-  } 
-  sim_pures. 
-  sim_val. iModIntro. destruct Hv_s' as [-> | ->]; first done. 
-  iApply big_sepL2_forall. iSplit. { rewrite replicate_length. iPureIntro. lia. } 
-  iIntros (k sc_t sc_s). rewrite lookup_replicate. iIntros "Hsc (-> & _)". 
-  (* TODO: fix the pointer refined by poison thing in the relation *)
-  (*destruct sc_t; done.*)
-  
-  (*iApply big_sepL2_singleton; done.*)
-
-Abort.
-
-
+  }
+  sim_pures.
+  sim_val. iModIntro. destruct Hv_s' as [-> | ->]; first done.
+  iApply big_sepL2_forall. iSplit. { rewrite replicate_length. iPureIntro. lia. }
+  iIntros (k sc_t sc_s). rewrite lookup_replicate. iIntros "Hsc (-> & _)". destruct sc_t;done.
+Qed.
diff --git a/theories/stacked_borrows/examples/opt2.v b/theories/stacked_borrows/examples/opt2.v
index d07227c20d69710452f4561dc6da76c2617f1e25..6f3f1f51505c556a37d192ef9fa9420dd61eb189 100644
--- a/theories/stacked_borrows/examples/opt2.v
+++ b/theories/stacked_borrows/examples/opt2.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 (** Moving read of shared ref up across code that *may* use that ref. *)
 
-(** This is a variant using protectors. 
+(** This is a variant using protectors.
   See below for the original optimization without protectors and with deferred UB.
  *)
 
@@ -65,11 +65,11 @@ Proof.
   { iApply source_red_irred_unless; first done. by iIntros. }
   (* gain knowledge about the length *)
   iApply source_red_irred_unless; first done. iIntros (Hsize).
-  iApply (source_write_local with "Htag Hs"); [by rewrite repeat_length | done | ].
+  iApply (source_write_local with "Htag Hs"); [by rewrite replicate_length | done | ].
   iIntros "Hs Htag". source_finish.
   iPoseProof (rrel_value_source with "Hrel") as (v_t) "(-> & #Hv)".
   iPoseProof (value_rel_length with "Hv") as "%Hlen".
-  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite repeat_length | lia| ].
+  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite replicate_length | lia| ].
   sim_pures.
 
   target_apply (Copy _) (target_copy_local with "Htag Ht") "Ht Htag"; first lia.
@@ -104,22 +104,22 @@ Proof.
   source_pures. source_bind (Copy _). iApply (source_copy_any with "Htag_i Hi_s"); first done.
   iIntros (v_s' Hv_s') "Hi_s Htag_i". source_finish. sim_pures.
 
-  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "". sim_pures.
+  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
   iApply (sim_protected_unprotectN with "Hcall Htag_i Hi_t Hi_s Hvrel"); [ | apply lookup_insert | ].
-  { simpl. cbn in Hlen_t. intros i' Hi'. replace i' with O by lia. rewrite elem_of_union elem_of_singleton. eauto. } 
+  { simpl. cbn in Hlen_t. intros i' Hi'. replace i' with O by lia. rewrite elem_of_union elem_of_singleton. eauto. }
   iIntros "Hcall Htag_i Hi_t Hi_s".
-  iApply (sim_remove_empty_calls _ t_i with "Hcall"). 
-  { rewrite lookup_insert. done. } 
-  { rewrite Hlen_t. set_solver. } 
+  iApply (sim_remove_empty_calls _ t_i with "Hcall").
+  { rewrite lookup_insert. done. }
+  { rewrite Hlen_t. set_solver. }
   iIntros "Hcall".
   sim_apply (EndCall _) (EndCall _) (sim_endcall with "[Hcall]") "".
-  { replace (delete t_i _) with (∅ : gmap ptr_id (gset loc)); first done. 
+  { replace (delete t_i _) with (∅ : gmap ptr_id (gset loc)); first done.
     apply map_eq. intros t'. rewrite delete_insert_delete delete_insert; done.
-  } 
-  sim_pures. 
-  sim_val. iModIntro. destruct Hv_s' as [-> | ->]; first done. 
-  iApply big_sepL2_forall. iSplit. { rewrite replicate_length. iPureIntro. lia. } 
-  iIntros (k sc_t sc_s). rewrite lookup_replicate. iIntros "Hsc (-> & _)". 
+  }
+  sim_pures.
+  sim_val. iModIntro. destruct Hv_s' as [-> | ->]; first done.
+  iApply big_sepL2_forall. iSplit. { rewrite replicate_length. iPureIntro. lia. }
+  iIntros (k sc_t sc_s). rewrite lookup_replicate. iIntros "Hsc (-> & _)".
   destruct sc_t; done.
 Qed.
 
@@ -175,11 +175,11 @@ Proof.
   { iApply source_red_irred_unless; first done. by iIntros. }
   (* gain knowledge about the length *)
   iApply source_red_irred_unless; first done. iIntros (Hsize).
-  iApply (source_write_local with "Htag Hs"); [by rewrite repeat_length | done | ].
+  iApply (source_write_local with "Htag Hs"); [by rewrite replicate_length | done | ].
   iIntros "Hs Htag". source_finish.
   iPoseProof (rrel_value_source with "Hrel") as (v_t) "(-> & #Hv)".
   iPoseProof (value_rel_length with "Hv") as "%Hlen".
-  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite repeat_length | lia| ].
+  target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag"; [ by rewrite replicate_length | lia| ].
   sim_pures.
 
   target_apply (Copy _) (target_copy_local with "Htag Ht") "Ht Htag"; first lia.
@@ -217,10 +217,7 @@ Proof.
   iIntros (v_s') "Hv' Hi_s Htag_i". source_finish.
   sim_pures.
 
-  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "". sim_pures.
-   
+  sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
+
   sim_val. iModIntro. done.
 Qed.
-
-
-
diff --git a/theories/stacked_borrows/heap.v b/theories/stacked_borrows/heap.v
index e9901dd81d4a89a19775985fa72b5ef93c82b3ba..133b1476e67dbfe3298b3f64fefe215c2c1fd334 100644
--- a/theories/stacked_borrows/heap.v
+++ b/theories/stacked_borrows/heap.v
@@ -674,6 +674,19 @@ Section tainted_tags.
     - right; right. eapply (Ht t it); done.
     - left. simpl. lia.
   Qed.
+
+  Lemma tag_tainted_interp_alloc σ l n :
+    let nt := Tagged σ.(snp) in
+    tag_tainted_interp σ -∗ tag_tainted_interp (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n nt) σ.(scs) (S σ.(snp)) σ.(snc)).
+  Proof.
+    intros nt. iIntros "Htainted".
+    iApply (tag_tainted_interp_preserve σ with "Htainted"). { simpl. lia. }
+    intros l' stk' Hstk' it Hit.
+    specialize (init_stacks_lookup_case _ _ _ _ _ _ Hstk') as [(Hstk'' & Hi) | (i & Hi & ->)].
+    + right. right. eauto.
+    + left. simpl. move : Hstk'. rewrite (proj1 (init_stacks_lookup _ _ _ _)); last done.
+      intros [= <-]. move : Hit. rewrite elem_of_list_singleton => -> /=. lia.
+  Qed.
 End tainted_tags.
 
 
@@ -769,6 +782,28 @@ Proof.
       by replace (Z.of_nat (S i)) with (1 + i) by lia.
 Qed.
 
+Lemma array_tag_map_lookup_None t t' l v :
+  t ≠ t' → ∀ l', array_tag_map l t v !! (t', l') = None.
+Proof.
+  intros Hneq l'. destruct (array_tag_map l t v !! (t', l')) eqn:Harr; last done.
+  specialize (array_tag_map_lookup1 l t v t' l' ltac:(eauto)) as [Heq _]; congruence.
+Qed.
+
+Lemma array_tag_map_lookup_None' l t v l' : 
+  (∀ i:nat, (i < length v)%nat → l +ₗ i ≠ l') →
+  array_tag_map l t v !! (t, l') = None.
+Proof. 
+  intros Hneq. destruct (array_tag_map _ _ _ !! _) eqn:Heq; last done. exfalso.
+  specialize (array_tag_map_lookup2 l t v t l' ltac:(eauto)) as [_ (i & Hi & ->)].
+  eapply Hneq; last reflexivity. done. 
+Qed.
+
+Lemma array_tag_map_lookup_None2 l t t' v l' :
+  array_tag_map l t v !! (t', l') = None →
+  t ≠ t' ∨ (∀ i: nat, (i < length v)%nat → l +ₗ i ≠ l'). 
+Proof.
+Admitted.
+
 Lemma ghost_map_array_tag_lookup `{!bor_stateG Σ} (γh : gname) (q : Qp) (M : gmap (ptr_id * loc) scalar) (scs : list scalar) (t : ptr_id) (l : loc) dq :
   ghost_map_auth γh q M -∗
   ([∗ list] i ↦ sc ∈ scs, ghost_map_elem γh (t, l +ₗ i) dq sc) -∗
@@ -792,6 +827,7 @@ Lemma ghost_map_array_tag_update `{!bor_stateG Σ} (γh : gname) (M : gmap (ptr_
   ([∗ list] i ↦ sc' ∈ v', ghost_map_elem γh (t, l +ₗ i) (DfracOwn 1) sc') ∗
   ghost_map_auth γh 1 (array_tag_map l t v' ∪ M).
 Proof.
+
 Admitted.
 
 Lemma ghost_map_array_tag_insert `{!bor_stateG Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v : list scalar) (t : ptr_id) (l : loc) :
@@ -802,6 +838,26 @@ Lemma ghost_map_array_tag_insert `{!bor_stateG Σ} (γh : gname) (M : gmap (ptr_
 Proof.
 Admitted.
 
+Lemma ghost_map_array_tag_delete `{!bor_stateG Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v : list scalar) (t : ptr_id) (l : loc) :
+  ghost_map_auth γh 1 M -∗
+  ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) (DfracOwn 1) sc) ==∗
+  ghost_map_auth γh 1 (M ∖ array_tag_map l t v).
+Proof.
+  iIntros "Hauth Helems". 
+  iApply (ghost_map_delete_big (array_tag_map l t v) with "Hauth [Helems]"). 
+  iInduction v as [ | sc v] "IH" forall (l); first done. 
+  simpl. iApply big_sepM_insert. 
+  { destruct (_ !! _) eqn:Heq; last done. 
+    specialize (array_tag_map_lookup2 (l +ₗ 1) t v t l ltac:(eauto)) as [_ (i & _ & Hl)].
+    destruct l. injection Hl. lia. 
+  } 
+  rewrite shift_loc_0_nat. iDestruct "Helems" as "[$ Helems]".  
+  iApply "IH". iApply (big_sepL_mono with "Helems"). 
+  iIntros (i sc' Hi). simpl. 
+  rewrite shift_loc_assoc. replace (Z.of_nat (S i)) with (1 + i) by lia; done.
+Qed.
+
+
 Lemma ghost_map_array_tag_tk `{!bor_stateG Σ} (γh : gname) (v : list scalar) (t : ptr_id) (l : loc) tk :
   ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) (DfracOwn 1) sc) ==∗
   ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +ₗ i) (tk_to_frac tk) sc).
@@ -819,38 +875,459 @@ Proof.
 Qed.
 
 
+Lemma lookup_union_Some_l' `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) (v : V) :
+  (M1 ∪ M2) !! k = Some v → M2 !! k = None → M1 !! k = Some v.
+Proof.
+  destruct (M1 !! k) as [ v' | ] eqn:Hv'.
+  - specialize (lookup_union_Some_l M1 M2 _ _ Hv') as ->. move => [= ->]. done.
+  - rewrite lookup_union_r; last done. congruence.
+Qed.
+Lemma lookup_union_is_Some `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) :
+  is_Some ((M1 ∪ M2) !! k) ↔ is_Some (M1 !! k) ∨ is_Some (M2 !! k).
+Proof.
+  split.
+  - intros (v & Hv). destruct (M1 !! k) eqn:HM1; first by eauto.
+    right. erewrite <-lookup_union_r; eauto.
+  - intros [(v & HM1) | (v & HM2)].
+    + rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto.
+    + destruct (M1 !! k) eqn:HM1. { rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto. }
+      rewrite lookup_union_r; eauto.
+Qed.
+
+Lemma dom_agree_on_tag_union M1_t M1_s M2_t M2_s t :
+  dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t →
+  dom_agree_on_tag (M1_t ∪ M2_t) (M1_s ∪ M2_s) t.
+Proof.
+  intros [H1a H1b] [H2a H2b]. split; intros l; rewrite !lookup_union_is_Some; naive_solver.
+Qed.
+
+Lemma dom_agree_on_tag_array_tag_map l t v_t v_s :
+  length v_t = length v_s →
+  dom_agree_on_tag (array_tag_map l t v_t) (array_tag_map l t v_s) t.
+Proof.
+  intros Hlen. split; intros l'.
+  - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia.
+    apply lookup_lt_is_Some_2. lia.
+  - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia.
+    apply lookup_lt_is_Some_2. lia.
+Qed.
+
+
+Lemma dom_agree_on_tag_not_elem M_t M_s t :
+  (∀ l, M_t !! (t, l) = None) → (∀ l, M_s !! (t, l) = None) →
+  dom_agree_on_tag M_t M_s t.
+Proof. intros Ht Hs. split; intros l; rewrite Ht Hs; congruence. Qed.
+
+(* TODO: move somewhere? *)
+Lemma lookup_difference_is_Some `{Countable K} (V : Type) (M1 M2 : gmap K V) (k : K) : 
+  is_Some ((M1 ∖ M2) !! k) ↔ is_Some (M1 !! k) ∧ M2 !! k = None.
+Proof. rewrite /is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed.
+
+Lemma dom_agree_on_tag_difference M1_t M1_s M2_t M2_s t :
+  dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t →
+  dom_agree_on_tag (M1_t ∖ M2_t) (M1_s ∖ M2_s) t.
+Proof.
+  intros [H1a H1b] [H2a H2b]. split; intros l. 
+  all: rewrite !lookup_difference_is_Some !eq_None_not_Some; naive_solver.
+Qed.
+
+
+Section val_rel.
+  Context {Σ} `{bor_stateG Σ}.
+  Definition sc_rel (sc1 sc2 : scalar) : iProp Σ :=
+    match sc1, sc2 with
+    | ScInt z1, ScInt z2 => ⌜z1 = z2⌝
+    | ScFnPtr f1, ScFnPtr f2 => ⌜f1  = f2⌝
+    | ScPtr l1 p1, ScPtr l2 p2 =>
+        (* through srel: the stacks are the same, the allocation size is the same, and the locations are related (i.e.: if tagged, then it is public) *)
+        ⌜l1 = l2⌝ ∗
+        (⌜p1 = Untagged⌝ ∗ ⌜p2 = Untagged⌝ ∨
+        (∃ t1 t2, ⌜p1 = Tagged t1⌝ ∗ ⌜p2 = Tagged t2⌝ ∗
+        (* may want to generalize that properly when we have a proper bijection on tags*)
+        ⌜t1 = t2⌝ ∗
+        t1 $$ tk_pub))
+        (* note: we do not have any assertion about the value as viewed by the tag here -- we don't really care about it, we need to do a retag anyways. what the tk_pub gives us is that the locations store related values *)
+    | ScCallId c, ScCallId c' => ⌜c = c'⌝
+    | ScPtr l t, ScPoison => True
+    | ScInt z, ScPoison => True
+    | ScPoison, ScPoison => True
+    | ScFnPtr fn, ScPoison => True
+    | ScCallId c, ScPoison => True
+    | _, _ => False
+    end.
+
+  Definition value_rel (v1 v2 : value) : iProp Σ := [∗ list] sc_t; sc_s ∈ v1; v2, sc_rel sc_t sc_s.
+
+  Definition rrel (r1 r2 : result) : iProp Σ :=
+    match r1, r2 with
+    | ValR v1, ValR v2 => value_rel v1 v2
+    | PlaceR l1 bor1 T1, PlaceR l2 bor2 T2 =>
+      (* places must be related in a similar way as pointers: either untagged or public. Types should be equal. *)
+      sc_rel (ScPtr l1 bor1) (ScPtr l2 bor2) ∧ ⌜T1 = T2⌝
+    | _, _ => False
+    end.
+
+  Global Instance sc_rel_persistent sc_t sc_s : Persistent (sc_rel sc_t sc_s).
+  Proof. destruct sc_t, sc_s; apply _. Qed.
+  Global Instance value_rel_persistent v_t v_s : Persistent (value_rel v_t v_s).
+  Proof. apply _. Qed.
+  Global Instance rrel_persistent r_t r_s : Persistent (rrel r_t r_s).
+  Proof. destruct r_t, r_s; apply _. Qed.
+
+  (* Inversion lemmas *)
+  Lemma sc_rel_ptr_source sc_t l_s t_s :
+    sc_rel sc_t (ScPtr l_s t_s) -∗ ⌜sc_t = ScPtr l_s t_s⌝ ∗ (if t_s is Tagged t then t $$ tk_pub else True).
+  Proof.
+    iIntros "Hrel". destruct sc_t; [done | done | | done | done ].
+    iDestruct "Hrel" as "(-> & [[-> ->] | (% & %t & -> & -> & -> & ?)])"; iFrame; done.
+  Qed.
+  Lemma sc_rel_fnptr_source sc_t fn :
+    sc_rel sc_t (ScFnPtr fn) -∗ ⌜sc_t = ScFnPtr fn⌝.
+  Proof.
+    iIntros "Hrel". destruct sc_t; [done | done | done | | done].
+    by iDestruct "Hrel" as "->".
+  Qed.
+  Lemma sc_rel_int_source sc_t z :
+    sc_rel sc_t (ScInt z) -∗ ⌜sc_t = ScInt z⌝.
+  Proof.
+    iIntros "Hrel". destruct sc_t; [ done | | done..].
+    by iDestruct "Hrel" as "->".
+  Qed.
+  Lemma sc_rel_cid_source sc_t c :
+    sc_rel sc_t (ScCallId c) -∗ ⌜sc_t = ScCallId c⌝.
+  Proof. iIntros "Hrel"; destruct sc_t; [done.. | ]. by iDestruct "Hrel" as "->". Qed.
+
+  Lemma sc_rel_poison_target sc_s :
+    sc_rel (ScPoison) sc_s -∗ ⌜sc_s = ScPoison⌝.
+  Proof. iIntros "Hrel". destruct sc_s; done. Qed.
+
+  Lemma rrel_place_source r_t l_s t_s T :
+    rrel r_t (PlaceR l_s t_s T) -∗
+    ∃ l_t, ⌜r_t = PlaceR l_t t_s T⌝ ∗ (if t_s is Tagged t then t $$ tk_pub else True).
+  Proof.
+    iIntros "Hrel".
+    destruct r_t as [ | l_t t' T']; first done. iDestruct "Hrel" as "(#H & ->)".
+    iDestruct (sc_rel_ptr_source with "H") as "[%Heq Htag]".
+    injection Heq as [= -> ->]. iExists l_s. eauto.
+  Qed.
+  Lemma rrel_value_source r_t v_s :
+    rrel r_t (ValR v_s) -∗
+    ∃ v_t, ⌜r_t = ValR v_t⌝ ∗ value_rel v_t v_s.
+  Proof.
+    iIntros "Hrel". destruct r_t as [ v_t | ]; last done.
+    iExists v_t. iFrame "Hrel". done.
+  Qed.
+
+  Lemma value_rel_length v_t v_s :
+    value_rel v_t v_s -∗ ⌜length v_t = length v_s⌝.
+  Proof. iApply big_sepL2_length. Qed.
+  Lemma value_rel_empty :
+    ⊢ value_rel [] [].
+  Proof. by iApply big_sepL2_nil. Qed.
+
+  Lemma value_rel_singleton_source v_t sc_s :
+    value_rel v_t [sc_s] -∗ ∃ sc_t, ⌜v_t = [sc_t]⌝ ∗ sc_rel sc_t sc_s.
+  Proof.
+    iIntros "Hv". iPoseProof (value_rel_length with "Hv") as "%Hlen".
+    destruct v_t as [ | sc_t []]; [done | | done ].
+    iExists sc_t. iSplitR "Hv"; first done. iRevert "Hv". rewrite /value_rel big_sepL2_singleton. eauto.
+  Qed.
+
+
+  Lemma value_rel_lookup v_t v_s (i : nat) :
+    i < length v_t →
+    value_rel v_t v_s -∗
+    ∃ sc_t sc_s, ⌜v_t !! i = Some sc_t⌝ ∗ ⌜v_s !! i = Some sc_s⌝ ∗ sc_rel sc_t sc_s.
+  Proof.
+    iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall.
+    iDestruct "Hvrel" as "[%Hlen Hvrel]".
+    iSpecialize ("Hvrel" $! i (v_t !!! i) (v_s !!! i)). iExists (v_t !!! i), (v_s !!! i).
+    assert (v_t !! i = Some (v_t !!! i)) as Heq.
+    { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. }
+    assert (v_s !! i = Some (v_s !!! i)) as Heq'.
+    { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. }
+    iSplit; first done. iSplit; first done. iApply "Hvrel"; done.
+  Qed.
+
+  Lemma value_rel_lookup_total (v_t v_s : list scalar) (i : nat) :
+    i < length v_t → value_rel v_t v_s -∗ sc_rel (v_t !!! i) (v_s !!! i).
+  Proof.
+    iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall.
+    iDestruct "Hvrel" as "[%Hlen Hvrel]".
+    iApply ("Hvrel" $! i (v_t !!! i) (v_s !!! i)).
+    all: iPureIntro; apply list_lookup_lookup_total; apply lookup_lt_is_Some_2; lia.
+  Qed.
+
+  Lemma tag_values_included_iff v t :
+    tag_values_included v t ↔ (∀ i, (i < length v)%nat → wf_scalar t (v !!! i)).
+  Proof.
+    rewrite /tag_values_included /wf_scalar. split.
+    - intros Hin i Hi t' l Hvi. eapply (Hin l). rewrite -Hvi. by apply elem_of_list_lookup_total_2.
+    - intros Hs l tg (i & Hi & Hl)%elem_of_list_lookup_total_1. by eapply Hs.
+  Qed.
+
+  Lemma tag_values_included_cons sc v t :
+    tag_values_included (sc :: v) t ↔ wf_scalar t sc ∧ tag_values_included v t.
+  Proof.
+    rewrite !tag_values_included_iff. split.
+    - intros Ha. split.
+      + apply (Ha O). cbn. lia.
+      + intros i Hi. apply (Ha (S i)). cbn. lia.
+    - intros [Hwf Ha]. intros [ | i] Hi; first done. apply Ha. cbn in Hi. lia.
+  Qed.
+
+End val_rel.
+
+Class sborG (Σ: gFunctors) := SBorG {
+  sborG_gen_progG :> gen_sim_progGS string ectx ectx Σ;
+  sborG_stateG :> bor_stateG Σ;
+}.
+
+Global Program Instance sborG_simulirisG `{!sborG Σ} : simulirisG (iPropI Σ) bor_lang := {
+  state_interp P_t σ_t P_s σ_s T_s :=
+    (gen_prog_interp (hG := gen_prog_inG_target) P_t ∗
+     gen_prog_interp (hG := gen_prog_inG_source) P_s ∗
+     bor_interp sc_rel σ_t σ_s
+    )%I;
+}.
+Next Obligation.
+Admitted.
+
+
+
+
+
 (** Lemmas / Accessors *)
 Add Printing Constructor state item.
 Section lemmas.
-  Context `{bor_stateG Σ} (sc_rel : scalar → scalar → iProp Σ)
-    (sc_rel_pers : ∀ sc_t sc_s, Persistent (sc_rel sc_t sc_s)).
+  Context `{bor_stateG Σ}.
   Local Notation bor_interp := (bor_interp sc_rel).
 
   Implicit Types
     (l : loc) (sc : scalar).
 
+  Lemma init_mem_dom_L l n h :
+    dom (gset loc) (init_mem l n h) = dom (gset loc) h ∪ dom (gset loc) (init_mem l n ∅).
+  Proof. apply set_eq. intros l'. rewrite init_mem_dom. done. Qed.
+
+  Lemma fresh_block_not_elem_dom h i :
+    (fresh_block h, i) ∉ dom (gset loc) h.
+  Proof.
+    rewrite /fresh_block.
+    rewrite -elem_of_elements.
+  Admitted.
+
+  Lemma fresh_block_det σ_s σ_t :
+    dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp) →
+    fresh_block σ_s.(shp) = fresh_block σ_t.(shp).
+  Proof. rewrite /fresh_block. intros ->. done. Qed.
+
+  Lemma free_mem_dom σ_t σ_s l n :
+    dom (gset loc) σ_t.(shp) = dom (gset loc) σ_s.(shp) →
+    dom (gset loc) (free_mem l n σ_t.(shp)) = dom (gset loc) (free_mem l n σ_s.(shp)).
+  Proof.
+    intros Hdom. induction n as [ | n IH] in l |-*; first done.
+    simpl. rewrite !dom_delete_L IH. done.
+  Qed.
+
+
+
+  Lemma init_stack_preserve σ n :
+    let l := (fresh_block σ.(shp), 0) in
+    let nt := σ.(snp) in
+    let α' := init_stacks σ.(sst) l n (Tagged nt) in
+    state_wf σ →
+    ∀ l' stk, σ.(sst) !! l' = Some stk → α' !! l' = Some stk.
+  Proof.
+    intros l nt α' Hwf l' stk Hl'.
+    rewrite (proj2 (init_stacks_lookup _ _ _ _) l'); first done.
+    intros i Hi ->.
+    specialize (elem_of_dom σ.(sst) ((fresh_block (shp σ), 0) +ₗ i)).
+    rewrite Hl'. intros (_ &Ha). specialize (Ha ltac:(eauto)).
+    move : Ha. rewrite -state_wf_dom; last done.
+    apply fresh_block_not_elem_dom.
+  Qed.
+
+  Lemma init_mem_preserve σ n :
+    let l := (fresh_block σ.(shp), 0) in
+    let nt := σ.(snp) in
+    let h' := init_mem l n σ.(shp) in
+    ∀ l' sc, σ.(shp) !! l' = Some sc → h' !! l' = Some sc.
+  Proof.
+    intros l nt h' l' sc Hsc.
+    rewrite (proj2 (init_mem_lookup _ _ _) l'); first done.
+    intros i Hi ->.
+    specialize (elem_of_dom σ.(shp) ((fresh_block (shp σ), 0) +ₗ i)).
+    rewrite Hsc. intros (_ &Ha). specialize (Ha ltac:(eauto)).
+    move : Ha. apply fresh_block_not_elem_dom.
+  Qed.
+
+  Lemma loc_controlled_alloc_update σ l' n (t : ptr_id) (tk : tag_kind) sc :
+    let l := (fresh_block σ.(shp), 0) in
+    let nt := σ.(snp) in
+    let α' := init_stacks σ.(sst) l n (Tagged nt) in
+    state_wf σ →
+    nt ≠ t →
+    loc_controlled l' t tk sc σ →
+    loc_controlled l' t tk sc (mkState (init_mem l n σ.(shp)) α' σ.(scs) (S σ.(snp)) σ.(snc)).
+  Proof.
+    intros l nt α' Hwf Hne Hcontrolled Hpre.
+    assert (∀ l' stk, α' !! l' = Some stk → stk = init_stack (Tagged nt) ∨ σ.(sst) !! l' = Some stk) as Hα'.
+    { intros l'' stk Hl'.
+      specialize (init_stacks_lookup_case _ _ _ _ _ _ Hl') as [(Hstk & _) | (i & Hi & ->)]; first by eauto.
+      left. rewrite (proj1 (init_stacks_lookup _ _ _ _) i Hi) in Hl'.
+      injection Hl' as [= <-]. done.
+    }
+    assert (bor_state_pre l' t tk σ) as [Hown Hmem]%Hcontrolled.
+    { destruct tk; last done.
+      all: destruct Hpre as (stk & pm & opro & [-> | Hstk]%Hα' & Hit & ?); simpl in *; last by eauto 8.
+      all: exfalso; move : Hit; rewrite elem_of_list_singleton; injection 1; congruence.
+    }
+    simpl. split.
+    - destruct tk.
+      + destruct Hown as (stk & Hstk & ?). exists stk. split; last done. apply init_stack_preserve; done.
+      + destruct Hown as (stk & Hstk & ?). exists stk. split; last done. apply init_stack_preserve; done.
+      + apply init_stack_preserve; done.
+    - apply init_mem_preserve. done.
+  Qed.
+
+  Lemma sim_alloc_state_rel_update σ_t σ_s M_tag M_t M_t' M_call l n tk :
+    let nt := σ_t.(snp) in
+    (∀ t, is_Some (M_tag !! t) → t ≠ nt) →
+    state_rel sc_rel M_tag M_t M_call σ_t σ_s -∗
+    state_rel sc_rel (<[nt := (tk, ())]> M_tag) (M_t' ∪ M_t) M_call
+      (mkState (init_mem l n (shp σ_t)) (init_stacks (sst σ_t) l n (Tagged nt)) (scs σ_t) (S σ_t.(snp)) (snc σ_t))
+      (mkState (init_mem l n (shp σ_s)) (init_stacks (sst σ_s) l n (Tagged nt)) (scs σ_s) (S (snp σ_s)) (snc σ_s)).
+  Proof.
+    intros nt Hneq. iIntros "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hstate)".
+    iSplitR. { simpl. rewrite !(init_mem_dom_L _ _ (shp _)) Hdom_eq. iPureIntro. set_solver. }
+    simpl. rewrite Hsst_eq. iSplitR; first done.
+    iSplitR; first by rewrite Hsnp_eq. do 2 (iSplitR; first done).
+    iIntros (l' (s & [(Heq & Hi) | (i & Hi & ->)]%init_mem_lookup_case)).
+    + (* old location *)
+      iDestruct ("Hstate" $! l' with "[]") as "[Hpub | (%t & %Hpriv)]".
+      { eauto. }
+      * iLeft. simpl. iIntros (sc_t Hsc_t). simpl in Hsc_t.
+        rewrite (proj2 (init_mem_lookup _ n _) l' Hi) in Hsc_t. simplify_eq.
+        iDestruct ("Hpub" $! s with "[//]") as (sc_s Hsc_s) "Hscrel".
+        iExists sc_s. iSplit; last done. iPureIntro.
+        by rewrite (proj2 (init_mem_lookup _ n _) l' Hi).
+      * iRight. iPureIntro. exists t.
+        destruct Hpriv as (tk' & Htk & Hs & ?). exists tk'. split_and!; [ | | done].
+        { rewrite lookup_insert_ne; first done. specialize (Hneq t ltac:(eauto)). done. }
+        rewrite lookup_union_is_Some. eauto.
+    + (* new location *)
+      iLeft. rewrite /pub_loc /=. rewrite !(proj1 (init_mem_lookup _ _ _)); [ | done | done].
+      iIntros (? [= <-]). iExists ☠%S. iSplit; done.
+  Qed.
+
+  Lemma sim_alloc_call_set_interp_update σ n M_call :
+    state_wf σ →
+    let nt := σ.(snp) in
+    let l := (fresh_block σ.(shp), 0) in
+    call_set_interp M_call σ →
+    call_set_interp M_call (mkState (init_mem l n (shp σ)) (init_stacks (sst σ) l n (Tagged nt)) (scs σ) (S σ.(snp)) (snc σ)).
+  Proof.
+    intros Hwf nt l Hcall_interp c M' [? HM']%Hcall_interp. simpl. split; first done.
+    intros t L HL. specialize (HM' _ _ HL) as (?& HL'). split; first lia. intros l' Hl'.
+    specialize (HL' l' Hl') as (stk & pm & Hstk & Hit & ?).
+    exists stk, pm. split_and!; [ | done..].
+    apply init_stack_preserve; done.
+  Qed.
+
+  Lemma local_alloc_loc_controlled σ l nt n l' sc :
+    array_tag_map l nt (replicate n ScPoison) !! (nt, l') = Some sc →
+    loc_controlled l' nt tk_local sc (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n (Tagged nt)) σ.(scs) (S σ.(snp)) σ.(snc)).
+  Proof.
+    intros Hsc.
+    specialize (array_tag_map_lookup2 l nt _ nt l' ltac:(eauto)) as [_ (i & Hi & ->)].
+    intros _.
+    rewrite array_tag_map_lookup_Some in Hsc; last done.
+    apply lookup_replicate in Hsc as [-> Hi']. split.
+    * simpl. rewrite (proj1 (init_stacks_lookup _ _ _ _)); done.
+    * simpl. rewrite (proj1 (init_mem_lookup _ _ _ )); done.
+  Qed.
+
   Lemma heap_local_alloc σ_t σ_s T :
-    bor_interp σ_t σ_s ==∗
     let l_t := (fresh_block σ_t.(shp), 0) in
     let l_s := (fresh_block σ_s.(shp), 0) in
-    let t := σ_t.(snp) in
+    let nt := σ_t.(snp) in
+    state_wf (mkState (init_mem l_t (tsize T) σ_t.(shp)) (init_stacks σ_t.(sst) l_t (tsize T) (Tagged nt)) σ_t.(scs) (S σ_t.(snp)) σ_t.(snc)) →
+    state_wf (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged nt)) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)) →
+    bor_interp σ_t σ_s ==∗
     bor_interp
-      (mkState (init_mem l_t (tsize T) σ_t.(shp)) (init_stacks σ_t.(sst) l_t (tsize T) (Tagged σ_t.(snp))) σ_t.(scs) (S σ_t.(snp)) σ_t.(snc))
-      (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged σ_s.(snp))) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)) ∗
-      t $$ tk_local ∗
-      l_t ↦t∗[tk_local]{t} repeat ScPoison (tsize T) ∗
-      l_s ↦s∗[tk_local]{t} repeat ScPoison (tsize T).
+      (mkState (init_mem l_t (tsize T) σ_t.(shp)) (init_stacks σ_t.(sst) l_t (tsize T) (Tagged nt)) σ_t.(scs) (S σ_t.(snp)) σ_t.(snc))
+      (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged nt)) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)) ∗
+      nt $$ tk_local ∗
+      l_t ↦t∗[tk_local]{nt} replicate (tsize T) ScPoison ∗
+      l_s ↦s∗[tk_local]{nt} replicate (tsize T) ScPoison.
   Proof.
-    iIntros "(% & % & % & % & ? & Hstate & ? & Htag & %Hwf_s & %Hwf_t)".
-    (* 1. allocate new local locations
-       2. profit
-    *)
-    (*iDestruct "Hheap_s" as (Mheap_s) "(Hheap_s_auth & %Hheap_s)".*)
-    (*iDestruct "Hheap_t" as (Mheap_t) "(Hheap_t_auth & %Hheap_t)".*)
-
-    (* TODO: need notion of array maps, see HeapLang *)
-    (*iMod (ghost_map_insert_big with "Hheap_s_auth") as "(Hheap_s_auth & Hloc_s)".*)
-  Admitted.
+    intros l_t l_s nt Hwf_t' Hwf_s'.
+    iIntros "(% & % & % & % & (Hcall_auth & Htag_auth & Ht_auth & Hs_auth) & Htainted & #Hstate & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)".
+    destruct Htag_interp as (Htag_interp & Ht_dom& Hs_dom).
+    assert (M_tag !! nt = None) as M_tag_none.
+    { destruct (M_tag !! nt) as [[? []] | ]eqn:Hs; last done.
+      apply Htag_interp in Hs as (? & ? & _). lia.
+    }
+    assert (∀ l, M_t !! (nt, l) = None).
+    { intros l. destruct (M_t !! (nt, l)) eqn:Hl; last done.
+      specialize (Ht_dom nt l ltac:(eauto)) as (? & ?); congruence.
+    }
+    assert (∀ l, M_s !! (nt, l) = None).
+    { intros l. destruct (M_s !! (nt, l)) eqn:Hl; last done.
+      specialize (Hs_dom nt l ltac:(eauto)) as (? & ?); congruence.
+    }
+    (* update ghost state *)
+    iMod (ghost_map_array_tag_insert _ _ (replicate (tsize T) ScPoison ) nt l_t with "Ht_auth") as "[Ht_mem Ht_auth]"; first done.
+    iMod (ghost_map_array_tag_insert _ _ (replicate (tsize T) ScPoison ) nt l_s with "Hs_auth") as "[Hs_mem Hs_auth]"; first done.
+    iMod (tkmap_insert tk_local nt () with "Htag_auth") as "[Htag_auth Hnt]"; first done.
+    iModIntro.
+
+    iFrame "Hnt Hs_mem Ht_mem".
+    iExists _, _, _, _. iFrame "Htag_auth Ht_auth Hs_auth Hcall_auth". simpl.
+    iPoseProof (state_rel_get_pure with "Hstate") as "%Hp".
+    iPoseProof (state_rel_dom_eq with "Hstate") as "%Hdom_eq".
+    destruct Hp as (Hsst_eq & Hsnp_eq & Hsnc_eq & Hscs_eq).
+    assert (l_s = l_t) as Hl_eq.
+    { subst l_s l_t. rewrite (fresh_block_det _ _ Hdom_eq). done. }
+    iSplitL "Htainted". { subst nt. rewrite -Hsnp_eq. by iApply tag_tainted_interp_alloc. }
+    iSplitL.
+    { (* state rel *)
+      rewrite Hl_eq. iApply sim_alloc_state_rel_update; last done.
+      intros t ([?[]] & Hs). specialize (Htag_interp _ _ Hs) as (? & ? & _). lia.
+    }
+    iSplitL.
+    { iPureIntro. apply sim_alloc_call_set_interp_update; done. }
+    iSplitL.
+    { (* tag interp *)
+      iPureIntro. split_and!.
+      { simpl. intros t tk. rewrite lookup_insert_Some. intros [[<- [= <-]] | [Hneq Hsome]].
+        - (* new tag: under local control *)
+          split_and!; [ lia | lia | | |].
+          + intros l' sc_t Hsc_t%lookup_union_Some_l'; last done. by apply local_alloc_loc_controlled.
+          + intros l' sc_t Hsc_s%lookup_union_Some_l'; last done. by apply local_alloc_loc_controlled.
+          + apply dom_agree_on_tag_union; first last.
+            { apply dom_agree_on_tag_not_elem; done. }
+            rewrite Hl_eq. apply dom_agree_on_tag_array_tag_map.
+            by rewrite replicate_length.
+        - (* old tag *)
+          specialize (Htag_interp _ _ Hsome) as (? & ? & Hcontrol_t & Hcontrol_s & Hag).
+          split_and!; [lia | lia | .. ].
+          + intros l' sc_t Hsc_t. apply loc_controlled_alloc_update; [done | done| ].
+            rewrite lookup_union_r in Hsc_t; first by apply Hcontrol_t.
+            apply array_tag_map_lookup_None. lia.
+          + intros l' sc_s Hsc_s. subst nt. rewrite -Hsnp_eq. apply loc_controlled_alloc_update; [done | lia | ].
+            rewrite lookup_union_r in Hsc_s; first by apply Hcontrol_s.
+            apply array_tag_map_lookup_None. lia.
+          + apply dom_agree_on_tag_union; last done.
+            rewrite Hl_eq. apply dom_agree_on_tag_not_elem.
+            all: intros l; rewrite array_tag_map_lookup_None; done.
+      }
+      all: intros t l'; rewrite lookup_insert_is_Some' lookup_union_is_Some;
+        intros [[-> _]%array_tag_map_lookup2 | ?]; eauto.
+    }
+    eauto.
+  Qed.
 
   Lemma state_wf_upd_mem σ l sc :
     is_Some (σ.(shp) !! l) →
@@ -858,17 +1335,11 @@ Section lemmas.
     state_wf (state_upd_mem (<[l := sc]>) σ).
   Proof.
     intros Hs []. constructor; try done.
-    - rewrite dom_insert //.
-      have ->: {[l]} ∪ dom (gset loc) (shp σ) ≡ dom (gset loc) (shp σ); last done.
-      split; rewrite elem_of_union; last by eauto.
-      intros [ ->%elem_of_singleton_1 | ]; last done.
-      by apply elem_of_dom.
-    (*- intros l' l'' pid Hsome.*)
-      (*destruct (decide (l = l')) as [<- | Hne].*)
-      (*+ move : Hsome. rewrite lookup_insert => [= Heq].*)
-        (*subst sc. specialize (Hwf _ _ eq_refl). apply Hwf.*)
-      (*+ rewrite lookup_insert_ne in Hsome; last done.*)
-        (*eapply state_wf_mem_tag; done.*)
+    rewrite dom_insert //.
+    have ->: {[l]} ∪ dom (gset loc) (shp σ) ≡ dom (gset loc) (shp σ); last done.
+    split; rewrite elem_of_union; last by eauto.
+    intros [ ->%elem_of_singleton_1 | ]; last done.
+    by apply elem_of_dom.
     Qed.
 
   Lemma heap_local_write_target σ_t σ_s (t : ptr_id) l sc sc' :
@@ -928,21 +1399,12 @@ Section lemmas.
     - done.
   Qed.
 
-
-  Lemma tag_values_included_iff v t :
-    tag_values_included v t ↔ (∀ i, (i < length v)%nat → wf_scalar t (v !!! i)).
-  Proof.
-    rewrite /tag_values_included /wf_scalar. split.
-    - intros Hin i Hi t' l Hvi. eapply (Hin l). rewrite -Hvi. by apply elem_of_list_lookup_total_2.
-    - intros Hs l tg (i & Hi & Hl)%elem_of_list_lookup_total_1. by eapply Hs.
-  Qed.
   Lemma heap_local_readN_target σ_t σ_s (t : ptr_id) l scs :
     bor_interp σ_t σ_s -∗
     l ↦t∗[tk_local]{t} scs -∗
     t $$ tk_local -∗
     ⌜∀ i : nat, (i < length scs)%nat → σ_t.(shp) !! (l +ₗ i) = scs !! i⌝ ∗
     ⌜∀ i:nat, (i < length scs)%nat → bor_state_own (l +ₗ i) t tk_local σ_t⌝.
-    (*∗ ⌜scs <<t σ_t.(snp)⌝.*)
   Proof.
     iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & ? & Hsrel & ? & %Htag_interp & %Hwf_s & %Hwf_t)".
     iIntros "Hp Htag".
@@ -1113,6 +1575,45 @@ Section lemmas.
   Proof.
   Admitted.
 
+  Lemma loc_controlled_dealloc_update σ l l' (bor : tag) n (α' : stacks) (t : ptr_id) (tk : tag_kind) sc :
+    memory_deallocated σ.(sst) σ.(scs) l bor n = Some α' →
+    state_wf σ →
+    (bor = Tagged t ∧ (∃ i:nat, l' = l +ₗ i ∧ (i < n)%nat) → tk = tk_pub) →
+    loc_controlled l' t tk sc σ →
+    loc_controlled l' t tk sc (mkState (free_mem l n σ.(shp)) α' σ.(scs) σ.(snp) σ.(snc)).
+  Proof.
+    intros Hdealloc Hwf Hpub Hcontrol Hpre. 
+    destruct tk. 
+    - (* public *)
+      destruct Hpre as (stk & pm & opro & Hstk & Hit & Hpm). simpl in *.
+      destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Hdealloc _ _ Hstk) as [Hneq Hstk'].
+      destruct Hcontrol as [Hown Hshp]. { exists stk, pm, opro. done. }
+      destruct Hown as (stk' & Hstk'' & Hsro). 
+      split. 
+      + simplify_eq. exists stk. done.
+      + destruct (free_mem_lookup_case l' l n σ.(shp)) as [(_ & ->) | (i & Hi & -> & _)]; first done.
+        specialize (Hneq i Hi). congruence. 
+    - (* unique *)
+      destruct Hpre as (stk & pm & opro & Hstk & Hit & Hpm). simpl in *.
+      destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Hdealloc _ _ Hstk) as [Hneq Hstk'].
+      destruct Hcontrol as [Hown Hshp]. { exists stk, pm, opro. done. }
+      destruct Hown as (stk' & Hstk'' & (opro' & ? & ->)). 
+      split. 
+      + simplify_eq. exists stk. split; first done. rewrite Hstk' in Hstk''. 
+        injection Hstk'' as ->. eauto.
+      + destruct (free_mem_lookup_case l' l n σ.(shp)) as [(_ & ->) | (i & Hi & -> & _)]; first done.
+        specialize (Hneq i Hi). congruence. 
+    - (* local *) clear Hpre. destruct Hcontrol as [Hown Hshp]; first done. simpl. 
+      destruct (free_mem_lookup_case l' l n σ.(shp)) as [(Hi & ->) | (i & Hi & -> & Hfree)]. 
+      + split; last done. destruct (for_each_dealloc_lookup _ _ _ _ _ Hdealloc) as (_ & Heq). 
+        rewrite Heq; done.
+      + exfalso. destruct (for_each_true_lookup_case_2 _ _ _ _ _ Hdealloc) as [Heq _].
+        specialize (Heq _ Hi) as (stk & stk' & Hstk & Hstk' & Hd1). 
+        rewrite Hown in Hstk. injection Hstk as <-.
+        destruct (dealloc1 _ _ _) eqn:Heq; [ | done].
+        destruct (dealloc1_singleton_Some _ _ _ ltac:(eauto)) as (<- & _).
+        enough (tk_local = tk_pub) by congruence. apply Hpub. eauto.
+  Qed. 
 End lemmas.
 
 (* accessing a local location is only possible with the same tag, retaining the same stack for the access *)
@@ -1223,167 +1724,6 @@ Proof.
 Qed.
 
 
-(* NOTE: might need to generalize that with the bijection a bit when we want to do cool things, e.g., pass parts of an object to a function (but for just obtaining a reflexivity thm, it should be fine) *)
-Section val_rel.
-  Context {Σ} `{bor_stateG Σ}.
-  Definition sc_rel (sc1 sc2 : scalar) : iProp Σ :=
-    match sc1, sc2 with
-    | ScInt z1, ScInt z2 => ⌜z1 = z2⌝
-    | ScFnPtr f1, ScFnPtr f2 => ⌜f1  = f2⌝
-    | ScPtr l1 p1, ScPtr l2 p2 =>
-        (* through srel: the stacks are the same, the allocation size is the same, and the locations are related (i.e.: if tagged, then it is public) *)
-        ⌜l1 = l2⌝ ∗
-        (⌜p1 = Untagged⌝ ∗ ⌜p2 = Untagged⌝ ∨
-        (∃ t1 t2, ⌜p1 = Tagged t1⌝ ∗ ⌜p2 = Tagged t2⌝ ∗
-        (* may want to generalize that properly when we have a proper bijection on tags*)
-        ⌜t1 = t2⌝ ∗
-        t1 $$ tk_pub))
-        (* note: we do not have any assertion about the value as viewed by the tag here -- we don't really care about it, we need to do a retag anyways. what the tk_pub gives us is that the locations store related values *)
-    | ScCallId c, ScCallId c' => ⌜c = c'⌝
-    | ScPtr l t, ScPoison => True
-    | ScInt z, ScPoison => True
-    | ScPoison, ScPoison => True
-    | ScFnPtr fn, ScPoison => True
-    | ScCallId c, ScPoison => True
-    | _, _ => False
-    end.
-
-  Definition value_rel (v1 v2 : value) : iProp Σ := [∗ list] sc_t; sc_s ∈ v1; v2, sc_rel sc_t sc_s.
-
-  Definition rrel (r1 r2 : result) : iProp Σ :=
-    match r1, r2 with
-    | ValR v1, ValR v2 => value_rel v1 v2
-    | PlaceR l1 bor1 T1, PlaceR l2 bor2 T2 =>
-      (* places must be related in a similar way as pointers: either untagged or public. Types should be equal. *)
-      sc_rel (ScPtr l1 bor1) (ScPtr l2 bor2) ∧ ⌜T1 = T2⌝
-    | _, _ => False
-    end.
-
-  Global Instance sc_rel_persistent sc_t sc_s : Persistent (sc_rel sc_t sc_s).
-  Proof. destruct sc_t, sc_s; apply _. Qed.
-  Global Instance value_rel_persistent v_t v_s : Persistent (value_rel v_t v_s).
-  Proof. apply _. Qed.
-  Global Instance rrel_persistent r_t r_s : Persistent (rrel r_t r_s).
-  Proof. destruct r_t, r_s; apply _. Qed.
-
-  Lemma sc_rel_public_ptr_inv σ_t σ_s t1 t2 l1 l2 :
-    bor_interp sc_rel σ_t σ_s -∗
-    sc_rel (ScPtr l1 (Tagged t1)) (ScPtr l2 (Tagged t2)) -∗
-    ⌜l1 = l2 ∧ t1 = t2⌝ ∗
-    ∀ sc_s, ⌜σ_s.(shp) !! l1 = Some sc_s⌝ → ∃ sc_t, ⌜σ_t.(shp) !! l2 = Some sc_t⌝ ∗ sc_rel sc_t sc_s.
-  Proof.
-  Abort.
-
-  (* Inversion lemmas *)
-  Lemma sc_rel_ptr_source sc_t l_s t_s :
-    sc_rel sc_t (ScPtr l_s t_s) -∗ ⌜sc_t = ScPtr l_s t_s⌝ ∗ (if t_s is Tagged t then t $$ tk_pub else True).
-  Proof.
-    iIntros "Hrel". destruct sc_t; [done | done | | done | done ].
-    iDestruct "Hrel" as "(-> & [[-> ->] | (% & %t & -> & -> & -> & ?)])"; iFrame; done.
-  Qed.
-  Lemma sc_rel_fnptr_source sc_t fn :
-    sc_rel sc_t (ScFnPtr fn) -∗ ⌜sc_t = ScFnPtr fn⌝.
-  Proof.
-    iIntros "Hrel". destruct sc_t; [done | done | done | | done].
-    by iDestruct "Hrel" as "->".
-  Qed.
-  Lemma sc_rel_int_source sc_t z :
-    sc_rel sc_t (ScInt z) -∗ ⌜sc_t = ScInt z⌝.
-  Proof.
-    iIntros "Hrel". destruct sc_t; [ done | | done..].
-    by iDestruct "Hrel" as "->".
-  Qed.
-  Lemma sc_rel_cid_source sc_t c :
-    sc_rel sc_t (ScCallId c) -∗ ⌜sc_t = ScCallId c⌝.
-  Proof. iIntros "Hrel"; destruct sc_t; [done.. | ]. by iDestruct "Hrel" as "->". Qed.
-
-  Lemma sc_rel_poison_target sc_s :
-    sc_rel (ScPoison) sc_s -∗ ⌜sc_s = ScPoison⌝.
-  Proof. iIntros "Hrel". destruct sc_s; done. Qed.
-
-  Lemma rrel_place_source r_t l_s t_s T :
-    rrel r_t (PlaceR l_s t_s T) -∗
-    ∃ l_t, ⌜r_t = PlaceR l_t t_s T⌝ ∗ (if t_s is Tagged t then t $$ tk_pub else True).
-  Proof.
-    iIntros "Hrel".
-    destruct r_t as [ | l_t t' T']; first done. iDestruct "Hrel" as "(#H & ->)".
-    iDestruct (sc_rel_ptr_source with "H") as "[%Heq Htag]".
-    injection Heq as [= -> ->]. iExists l_s. eauto.
-  Qed.
-  Lemma rrel_value_source r_t v_s :
-    rrel r_t (ValR v_s) -∗
-    ∃ v_t, ⌜r_t = ValR v_t⌝ ∗ value_rel v_t v_s.
-  Proof.
-    iIntros "Hrel". destruct r_t as [ v_t | ]; last done.
-    iExists v_t. iFrame "Hrel". done.
-  Qed.
-
-  Lemma value_rel_length v_t v_s :
-    value_rel v_t v_s -∗ ⌜length v_t = length v_s⌝.
-  Proof. iApply big_sepL2_length. Qed.
-  Lemma value_rel_empty :
-    ⊢ value_rel [] [].
-  Proof. by iApply big_sepL2_nil. Qed.
-
-  Lemma value_rel_singleton_source v_t sc_s :
-    value_rel v_t [sc_s] -∗ ∃ sc_t, ⌜v_t = [sc_t]⌝ ∗ sc_rel sc_t sc_s.
-  Proof.
-    iIntros "Hv". iPoseProof (value_rel_length with "Hv") as "%Hlen".
-    destruct v_t as [ | sc_t []]; [done | | done ].
-    iExists sc_t. iSplitR "Hv"; first done. iRevert "Hv". rewrite /value_rel big_sepL2_singleton. eauto.
-  Qed.
-
-
-  Lemma value_rel_lookup v_t v_s (i : nat) :
-    i < length v_t →
-    value_rel v_t v_s -∗
-    ∃ sc_t sc_s, ⌜v_t !! i = Some sc_t⌝ ∗ ⌜v_s !! i = Some sc_s⌝ ∗ sc_rel sc_t sc_s.
-  Proof.
-    iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall.
-    iDestruct "Hvrel" as "[%Hlen Hvrel]".
-    iSpecialize ("Hvrel" $! i (v_t !!! i) (v_s !!! i)). iExists (v_t !!! i), (v_s !!! i).
-    assert (v_t !! i = Some (v_t !!! i)) as Heq.
-    { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. }
-    assert (v_s !! i = Some (v_s !!! i)) as Heq'.
-    { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. }
-    iSplit; first done. iSplit; first done. iApply "Hvrel"; done.
-  Qed.
-
-  Lemma value_rel_lookup_total (v_t v_s : list scalar) (i : nat) :
-    i < length v_t → value_rel v_t v_s -∗ sc_rel (v_t !!! i) (v_s !!! i).
-  Proof.
-    iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall.
-    iDestruct "Hvrel" as "[%Hlen Hvrel]".
-    iApply ("Hvrel" $! i (v_t !!! i) (v_s !!! i)).
-    all: iPureIntro; apply list_lookup_lookup_total; apply lookup_lt_is_Some_2; lia.
-  Qed.
-
-  Lemma tag_values_included_cons sc v t :
-    tag_values_included (sc :: v) t ↔ wf_scalar t sc ∧ tag_values_included v t.
-  Proof.
-    rewrite !tag_values_included_iff. split.
-    - intros Ha. split.
-      + apply (Ha O). cbn. lia.
-      + intros i Hi. apply (Ha (S i)). cbn. lia.
-    - intros [Hwf Ha]. intros [ | i] Hi; first done. apply Ha. cbn in Hi. lia.
-  Qed.
-
-End val_rel.
-
-Class sborG (Σ: gFunctors) := SBorG {
-  sborG_gen_progG :> gen_sim_progGS string ectx ectx Σ;
-  sborG_stateG :> bor_stateG Σ;
-}.
-
-Global Program Instance sborG_simulirisG `{!sborG Σ} : simulirisG (iPropI Σ) bor_lang := {
-  state_interp P_t σ_t P_s σ_s T_s :=
-    (gen_prog_interp (hG := gen_prog_inG_target) P_t ∗
-     gen_prog_interp (hG := gen_prog_inG_source) P_s ∗
-     bor_interp sc_rel σ_t σ_s
-    )%I;
-}.
-Next Obligation.
-Admitted.
 
 Fixpoint seq_loc_set (l : loc) (n : nat) : gset loc :=
   match n with
@@ -1401,11 +1741,6 @@ Proof.
       right. apply IH. exists i. split; [lia | done].
 Qed.
 
-Lemma fresh_block_det σ_s σ_t :
-  dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp) →
-  fresh_block σ_s.(shp) = fresh_block σ_t.(shp).
-Proof. rewrite /fresh_block. intros ->. done. Qed.
-
 (** TODO: these lemmas need a new home *)
 Section lemmas.
 Context `{!sborG Σ}.
@@ -1441,56 +1776,6 @@ Proof.
   rewrite insert_id; last done. apply IH. intros i Hi. apply Hacc1. lia.
 Qed.
 
-
-Lemma lookup_union_Some_l' `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) (v : V) :
-  (M1 ∪ M2) !! k = Some v → M2 !! k = None → M1 !! k = Some v.
-Proof.
-  destruct (M1 !! k) as [ v' | ] eqn:Hv'.
-  - specialize (lookup_union_Some_l M1 M2 _ _ Hv') as ->. move => [= ->]. done.
-  - rewrite lookup_union_r; last done. congruence.
-Qed.
-Lemma lookup_union_is_Some `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) :
-  is_Some ((M1 ∪ M2) !! k) ↔ is_Some (M1 !! k) ∨ is_Some (M2 !! k).
-Proof.
-  split.
-  - intros (v & Hv). destruct (M1 !! k) eqn:HM1; first by eauto.
-    right. erewrite <-lookup_union_r; eauto.
-  - intros [(v & HM1) | (v & HM2)].
-    + rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto.
-    + destruct (M1 !! k) eqn:HM1. { rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto. }
-      rewrite lookup_union_r; eauto.
-Qed.
-
-Lemma dom_agree_on_tag_union M1_t M1_s M2_t M2_s t :
-  dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t →
-  dom_agree_on_tag (M1_t ∪ M2_t) (M1_s ∪ M2_s) t.
-Proof.
-  intros [H1a H1b] [H2a H2b]. split; intros l; rewrite !lookup_union_is_Some; naive_solver.
-Qed.
-
-Lemma dom_agree_on_tag_array_tag_map l t v_t v_s :
-  length v_t = length v_s →
-  dom_agree_on_tag (array_tag_map l t v_t) (array_tag_map l t v_s) t.
-Proof.
-  intros Hlen. split; intros l'.
-  - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia.
-    apply lookup_lt_is_Some_2. lia.
-  - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia.
-    apply lookup_lt_is_Some_2. lia.
-Qed.
-
-Lemma array_tag_map_lookup_None t t' l v :
-  t ≠ t' → ∀ l', array_tag_map l t v !! (t', l') = None.
-Proof.
-  intros Hneq l'. destruct (array_tag_map l t v !! (t', l')) eqn:Harr; last done.
-  specialize (array_tag_map_lookup1 l t v t' l' ltac:(eauto)) as [Heq _]; congruence.
-Qed.
-
-Lemma dom_agree_on_tag_not_elem M_t M_s t :
-  (∀ l, M_t !! (t, l) = None) → (∀ l, M_s !! (t, l) = None) →
-  dom_agree_on_tag M_t M_s t.
-Proof. intros Ht Hs. split; intros l; rewrite Ht Hs; congruence. Qed.
-
 Lemma retag_mut_loc_controlled σ c l ot T mut α' rk i sc :
   let nt := σ.(snp) in
   let pk := RefPtr mut in
diff --git a/theories/stacked_borrows/steps_inv.v b/theories/stacked_borrows/steps_inv.v
index ded6fac8ec8c8c49c1fe9321fefa3c79d7332636..602b260295caa1afd66542455a69f95c9ab702fe 100644
--- a/theories/stacked_borrows/steps_inv.v
+++ b/theories/stacked_borrows/steps_inv.v
@@ -2,24 +2,24 @@ From simuliris.stacked_borrows Require Export notation defs.
 From simuliris.stacked_borrows Require Import steps_progress steps_retag.
 From iris.prelude Require Import options.
 
-Lemma head_free_inv (P : prog) l bor T σ σ' e' efs : 
+Lemma head_free_inv (P : prog) l bor T σ σ' e' efs :
   head_step P (Free (PlaceR l bor T)) σ e' σ' efs →
-  ∃ α', 
+  ∃ α',
     memory_deallocated σ.(sst) σ.(scs) l bor (tsize T) = Some α' ∧
     (∀ m : Z, is_Some (shp σ !! (l +ₗ m)) ↔ 0 ≤ m < tsize T) ∧
-    e' = #[☠]%E ∧ 
+    e' = #[☠]%E ∧
     σ' = mkState (free_mem l (tsize T) σ.(shp)) α' σ.(scs) σ.(snp) σ.(snc) ∧
     efs = [].
 Proof. intros Hhead. inv_head_step. eauto 8. Qed.
 
 Lemma head_copy_inv (P : prog) l t T σ e σ' efs :
   head_step P (Copy (PlaceR l t T)) σ e σ' efs →
-  efs = [] ∧ 
+  efs = [] ∧
   ((∃ v α', read_mem l (tsize T) (shp σ) = Some v ∧
   memory_read (sst σ) (scs σ) l t (tsize T) = Some α' ∧
   (*v <<t snp σ ∧*)
   σ' = mkState (shp σ) α' (scs σ) (snp σ) (snc σ) ∧
-  e = (ValR v)) ∨ 
+  e = (ValR v)) ∨
   e = ValR (replicate (tsize T) ScPoison) ∧ memory_read (sst σ) (scs σ) l t (tsize T) = None ∧ σ' = σ).
 Proof. intros Hhead. inv_head_step; first by eauto 10. destruct σ; eauto 10. Qed.
 
@@ -60,3 +60,11 @@ Lemma head_end_call_inv (P : prog) e' σ σ' efs c :
   e' = (#[☠])%E ∧
   σ' = state_upd_calls (.∖ {[ c ]}) σ.
 Proof. intros Hhead. inv_head_step. eauto. Qed.
+
+Lemma head_alloc_inv (P : prog) T σ σ' e' efs :
+  head_step P (Alloc T) σ e' σ' efs →
+  let l := (fresh_block σ.(shp), 0) in
+  efs = [] ∧
+  e' = Place l (Tagged σ.(snp)) T ∧
+  σ' = mkState (init_mem l (tsize T) σ.(shp)) (init_stacks σ.(sst) l (tsize T) (Tagged σ.(snp))) σ.(scs) (S σ.(snp)) σ.(snc).
+Proof. intros Hhead. inv_head_step. eauto. Qed.
diff --git a/theories/stacked_borrows/steps_opt.v b/theories/stacked_borrows/steps_opt.v
index ebfc534bd895a1a38916b0d222d35e8a6170314f..5bed884a5524021b3b2e901668055363930ef9de 100644
--- a/theories/stacked_borrows/steps_opt.v
+++ b/theories/stacked_borrows/steps_opt.v
@@ -1019,37 +1019,172 @@ Qed.
 (** Alloc *)
 Lemma sim_alloc_local T Φ π :
   (∀ t l, t $$ tk_local -∗
-    l ↦t∗[tk_local]{t} repeat ScPoison (tsize T) -∗
-    l ↦s∗[tk_local]{t} repeat ScPoison (tsize T) -∗
+    l ↦t∗[tk_local]{t} replicate (tsize T) ScPoison -∗
+    l ↦s∗[tk_local]{t} replicate (tsize T) ScPoison -∗
     Place l (Tagged t) T ⪯{π, Ω} Place l (Tagged t) T [{ Φ }]) -∗
   Alloc T ⪯{π, Ω} Alloc T [{ Φ }].
 Proof.
   iIntros "Hsim".
   iApply sim_lift_head_step_both. iIntros (??????) "[(HP_t & HP_s & Hbor) %Hsafe]".
   iPoseProof (bor_interp_get_pure with "Hbor") as "%Hp".
+  iPoseProof (bor_interp_get_state_wf with "Hbor") as "%Hwf".
   iModIntro. iSplitR.
   { iPureIntro. do 3 eexists. econstructor 2; econstructor. }
-  iIntros (e_t' efs_t σ_t') "%Hhead".
-  inv_head_step.
+  iIntros (e_t' efs_t σ_t') "%Hhead_t".
+  specialize (head_alloc_inv _ _ _ _ _ _ Hhead_t) as (-> & -> & ->).
   set (l_s := (fresh_block σ_s.(shp), 0)).
-  iMod (heap_local_alloc _ _ _ T with "Hbor") as "(Hbor & Htag & Htarget & Hsource)".
+  set (σ_s' := (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged σ_t.(snp))) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc))).
+  assert (Hhead_s : language.head_step P_s (Alloc T) σ_s (Place l_s (Tagged σ_t.(snp)) T) σ_s' []). 
+  { subst σ_s'. destruct Hp as (_ & <- & _). econstructor 2; econstructor. }
+  iMod (heap_local_alloc _ _ T with "Hbor") as "(Hbor & Htag & Htarget & Hsource)".
+  { eapply head_step_wf; [ apply Hhead_t | apply Hwf]. }
+  { eapply head_step_wf; last apply (proj2 Hwf). apply Hhead_s. } 
   iModIntro.
-  iExists (Place l_s (Tagged (σ_t.(snp))) T), [], (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged σ_s.(snp))) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)).
-  iFrame. iSplitR.
-  { iPureIntro. destruct Hp as (_ & <- & _).  econstructor 2; econstructor. }
+  iExists (Place l_s (Tagged (σ_t.(snp))) T), [], σ_s'.
+  iFrame. iSplitR; first done.
   iSplitL; last by iApply big_sepL2_nil.
-  subst l l_s. rewrite (fresh_block_det σ_s σ_t); last apply Hp.
+  subst l_s. rewrite (fresh_block_det σ_s σ_t); last apply Hp.
   iApply ("Hsim" with "Htag Htarget Hsource").
 Qed.
 
+
+Lemma bor_interp_free_local t v_t v_s l σ_t σ_s α' n : 
+  memory_deallocated (sst σ_t) (scs σ_t) l (Tagged t) n = Some α' →
+  memory_deallocated (sst σ_s) (scs σ_s) l (Tagged t) n = Some α' →
+  length v_t = n →
+  length v_s = n →
+  let σ_t' := mkState (free_mem l n σ_t.(shp)) α' σ_t.(scs) σ_t.(snp) σ_t.(snc) in
+  let σ_s' := mkState (free_mem l n σ_s.(shp)) α' σ_s.(scs) σ_s.(snp) σ_s.(snc) in
+  state_wf σ_t' →
+  state_wf σ_s' →
+  t $$ tk_local -∗ 
+  l ↦t∗[tk_local]{t} v_t -∗
+  l ↦s∗[tk_local]{t} v_s -∗
+  bor_interp sc_rel σ_t σ_s ==∗
+  t $$ tk_local ∗
+  bor_interp sc_rel σ_t' σ_s'.
+Proof. 
+  intros Hstack_t Hstack_s Hlen_t Hlen_s σ_t' σ_s' Hwf_t' Hwf_s'.
+  iIntros "Htag Ht Hs Hbor". 
+  iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htaint_interp & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)".
+  iMod (ghost_map_array_tag_delete with "Htag_t_auth Ht") as "Htag_t_auth". 
+  iMod (ghost_map_array_tag_delete with "Htag_s_auth Hs") as "Htag_s_auth".
+  iModIntro. iFrame "Htag". 
+  iExists M_call, M_tag, (M_t ∖ array_tag_map l t v_t), (M_s ∖ array_tag_map l t v_s).
+  iFrame.
+  iSplitL. 
+  { (* tainted *)
+    iApply (tag_tainted_interp_preserve σ_s with "Htaint_interp"). { simpl. lia. } 
+    intros l' stk' Hstk' it Hit. right. right. 
+    specialize (for_each_dealloc_lookup_Some _ _ _ _ _ Hstack_s _ _ Hstk') as (_ & Hstk). eauto.
+  } 
+  iSplitL. 
+  { (* state rel *)
+    (* TODO: partially duplicated from the refl lemma. prove more general lemma? *)
+    iDestruct "Hsrel" as "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hsrel)". 
+    iSplitR. { iPureIntro. simpl. apply free_mem_dom. done. } 
+    simpl. do 4 (iSplitR; first done). 
+    iIntros (l' (sc & Hsome)). 
+    destruct (free_mem_lookup_case l' l n σ_t.(shp)) as [[Hi Heq] | (i & _ & -> & ?)]; last congruence. 
+    rewrite Heq in Hsome. iDestruct ("Hsrel" $! l' with "[]") as "[Hpubl | (%t' & %Hprivl)]"; first by eauto.
+    + iLeft. iIntros (sc_t Hsc_t). simpl in *. 
+      rewrite Heq in Hsc_t. rewrite Hsome in Hsc_t. injection Hsc_t as <-.
+      iDestruct ("Hpubl" $! sc Hsome) as (sc_s) "[%Hsc_s Hscr]".
+      iExists sc_s. iSplitR; last done.
+      iPureIntro. 
+      destruct (free_mem_lookup_case l' l n σ_s.(shp)) as [[_ Heq'] | (i' & Hi' & -> & _)].
+      2: { specialize (Hi i' Hi'). congruence. }
+      rewrite Heq' Hsc_s. done. 
+    + iRight. iPureIntro. exists t'. 
+      destruct Hprivl as (tk & Htk & (s & Hs) & Hpriv). exists tk. split_and!; [done | | done].
+      exists s. apply lookup_difference_Some. split; first done.
+      destruct (decide (t = t')) as [<- | Hneq]; last by apply array_tag_map_lookup_None.
+      apply array_tag_map_lookup_None'. intros i Hi'. rewrite Hlen_t in Hi'. 
+      specialize (Hi i Hi'); done.
+  } 
+  iSplitL. 
+  { (* call interp *)
+    (* TODO: duplicated with the refl lemma *)
+    iPureIntro. iIntros (c M' Hc). 
+    destruct (Hcall_interp c M' Hc) as (? & HM'). split; first done. 
+    intros t' L Ht'. specialize (HM' t' L Ht') as (? & HL). split; first done.
+    intros l' (stk & pm & Hstk & Hit & Hpm)%HL. exists stk, pm. split_and!; [ | done..].
+    destruct (for_each_true_lookup_case_2 _ _ _ _ _ Hstack_t) as [EQ1 EQ2].
+    (* from Hstack_s, l cannot be in the affected range because it is protected by c,
+      so α' !! l = σt.(sst) !! l. *)
+    destruct (block_case l l' n) as [Hneq|(i & Hi & ->)].
+    + rewrite EQ2//. 
+    + exfalso. clear EQ2.
+      specialize (EQ1 _ Hi) as (stk1 & stk' & Eqstk1 & Eqstk' & Hdealloc).
+      rewrite Eqstk1 in Hstk. simplify_eq.
+      move : Hdealloc. destruct (dealloc1 stk (Tagged t) σ_t.(scs)) eqn:Eqd; last done. 
+      intros _.
+      destruct (dealloc1_Some stk (Tagged t) σ_t.(scs)) as (it & Eqit & ? & FA & GR).
+      { by eexists. }
+      rewrite ->Forall_forall in FA. apply (FA _ Hit).
+      rewrite /is_active_protector /= /is_active bool_decide_true //.
+  } 
+  iSplitL. 
+  { (* tag interp *)
+    destruct Htag_interp as (Htag_interp & Hdom_t & Hdom_s).
+    iPureIntro. split_and!.
+    { intros t' tk Ht. simpl. specialize (Htag_interp _ _ Ht) as (? & ? & Hcontrol_t & Hcontrol_s & Hag).
+      split_and!; [done | done | | | ].
+      + intros l' sc_t. 
+        rewrite lookup_difference_Some. intros [Hsc_t%Hcontrol_t Hnotin%array_tag_map_lookup_None2].
+        eapply loc_controlled_dealloc_update; [ apply Hstack_t | done | | done].
+        intros [[= <-] (i & -> & Hi)]. 
+        destruct Hnotin as [? | Hi']; first congruence. 
+        rewrite Hlen_t in Hi'. apply Hi' in Hi. congruence. 
+      + intros l' sc_s. 
+        rewrite lookup_difference_Some. intros [Hsc_t%Hcontrol_s Hnotin%array_tag_map_lookup_None2].
+        eapply loc_controlled_dealloc_update; [ apply Hstack_s | done | | done].
+        intros [[= <-] (i & -> & Hi)]. 
+        destruct Hnotin as [? | Hi']; first congruence. 
+        rewrite Hlen_s in Hi'. apply Hi' in Hi. congruence. 
+      + apply dom_agree_on_tag_difference; first done.
+        destruct (decide (t = t')) as [<- | Hneq].
+        * apply dom_agree_on_tag_array_tag_map. lia. 
+        * apply dom_agree_on_tag_not_elem; apply array_tag_map_lookup_None; done.
+    } 
+    all: intros t' l'; rewrite lookup_difference_is_Some; intros [? _]; eauto.
+  } 
+  eauto.
+Qed.
+
 (* local ownership makes strong assertions: we also have to deallocate the corresponding ghost state. *)
 Lemma sim_free_local l t T v_t v_s Φ π : 
+  length v_t = tsize T → 
+  length v_s = tsize T →
   t $$ tk_local -∗ 
   l ↦t∗[tk_local]{t} v_t -∗
   l ↦s∗[tk_local]{t} v_s -∗ 
-  #[☠] ⪯{π, Ω} #[☠] [{ Φ }] -∗
+  (t $$ tk_local -∗ #[☠] ⪯{π, Ω} #[☠] [{ Φ }]) -∗
   Free (Place l (Tagged t) T) ⪯{π, Ω} Free (Place l (Tagged t) T) [{ Φ }].
 Proof. 
-Admitted.
+  iIntros (Hlen_t Hlen_s) "Htag Ht Hs Hsim". 
+  iApply sim_lift_head_step_both. iIntros (??????) "[(HP_t & HP_s & Hbor) %Hsafe]".
+  destruct Hsafe as [Hthread Hsafe].
+  specialize (pool_safe_irred _ _ _ _ _ _ _ Hsafe Hthread ltac:(done)) as (Hmem_s & (α' & Hstack_s)).
+
+  iPoseProof (bor_interp_get_pure with "Hbor") as "%Hp".
+  destruct Hp as (Hsst_eq & Hsnp_eq & Hsnc_eq & Hscs_eq & Hwf_s & Hwf_t & Hdom_eq).
+  iModIntro. 
+  iSplitR.
+  { iPureIntro. eexists _, _, _. eapply dealloc_head_step'; first apply Hwf_t. 
+    - intros i. rewrite -Hmem_s. rewrite -!elem_of_dom Hdom_eq. done. 
+    - erewrite <-Hstack_s. rewrite Hsst_eq Hscs_eq. done. 
+  }
+  iIntros (e_t' efs_t σ_t' Hhead_t).
+  specialize (head_free_inv _ _ _ _ _ _ _ _ Hhead_t) as (α'_t & Hstack_t & Hmem_t & -> & -> & ->). 
+  assert (α'_t = α') as ->.
+  { move : Hstack_t Hstack_s. rewrite Hsst_eq Hscs_eq => -> [= ->] //. }
+  iMod (bor_interp_free_local with "Htag Ht Hs Hbor") as "[Htag Hbor]"; [done | done | done | done | ..].
+  { eapply head_step_wf; done. } 
+  { eapply head_step_wf; [eapply (dealloc_head_step' P_s); done | done ]. }
+  iModIntro. iExists _, _, _. 
+  iSplitR. { iPureIntro. eapply dealloc_head_step'; done. }
+  iFrame. iSplitL; last done. by iApply "Hsim".
+Qed.
 
 End lifting.
diff --git a/theories/stacked_borrows/steps_refl.v b/theories/stacked_borrows/steps_refl.v
index 69880f792deb9a2b8cc2aea3594440e225436ca8..04b21ee35d72eded51b493c451289700e19298bf 100644
--- a/theories/stacked_borrows/steps_refl.v
+++ b/theories/stacked_borrows/steps_refl.v
@@ -21,14 +21,83 @@ Implicit Types f : fname.
 
 Context (Ω : result → result → iProp Σ).
 
-
 Lemma sim_alloc_public T Φ π :
   (∀ t l, t $$ tk_pub -∗
     rrel (PlaceR l (Tagged t) T) (PlaceR l (Tagged t) T) -∗
     Place l (Tagged t) T ⪯{π, Ω} Place l (Tagged t) T [{ Φ }]) -∗
   Alloc T ⪯{π, Ω} Alloc T [{ Φ }].
 Proof.
-Admitted.
+  iIntros "Hsim".
+  iApply sim_lift_head_step_both. iIntros (??????) "[(HP_t & HP_s & Hbor) %Hsafe]".
+  iModIntro.
+  destruct Hsafe as [Hpool Hsafe].
+  iPoseProof (bor_interp_get_pure with "Hbor") as "%Hp".
+  destruct Hp as (Hsst_eq & Hsnp_eq & Hsnc_eq & Hscs_eq & Hwf_s & Hwf_t & Hdom_eq).
+  iSplitR. { iPureIntro. do 3 eexists. eapply alloc_head_step. }
+  iIntros (e_t' efs_t σ_t') "%Hhead_t".
+  specialize (head_alloc_inv _ _ _ _ _ _ Hhead_t) as (-> & -> & ->).
+
+  (* allocate tag *)
+  iDestruct "Hbor" as "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & #Hsrel & %Hcall_interp & %Htag_interp & _ & _)".
+  assert (M_tag !! σ_t.(snp) = None).
+  { destruct (M_tag !! σ_t.(snp)) as [[tk' []] | ] eqn:Hs; last done. exfalso.
+    apply Htag_interp in Hs as (_ & ? & _); lia.
+  }
+  iMod (tkmap_insert tk_pub σ_t.(snp) () ltac:(done) with "Htag_auth") as "[Htag_auth #Ht]".
+  iModIntro.
+  pose (l := (fresh_block σ_t.(shp), 0)). pose (nt := σ_t.(snp)).
+  pose (α' := init_stacks σ_t.(sst) l (tsize T) (Tagged nt)).
+  pose (σ_s' := (mkState (init_mem l (tsize T) σ_s.(shp)) α' σ_s.(scs) (S σ_s.(snp)) σ_s.(snc))).
+  assert (Hhead_s : head_step P_s (Alloc T) σ_s (Place l (Tagged nt) T) σ_s' []).
+  { subst σ_s' nt α' l. rewrite -Hsst_eq -Hsnp_eq. rewrite -(fresh_block_det σ_s σ_t); last done.
+    eapply alloc_head_step.
+  }
+  iExists _, [], _. iSplitR; first done. simpl. iFrame "HP_t HP_s".
+  iSplitR "Hsim Ht"; first last.
+  { iSplitL; last done. iApply ("Hsim" with "Ht"). iSplit; last done.
+    iSplitR; first done. iRight. iExists nt, nt. iFrame "Ht". eauto.
+  }
+  (* re-establish the invariants *)
+  iExists M_call, (<[nt := (tk_pub, ())]> M_tag), M_t, M_s.
+  iFrame "Hc Htag_auth Htag_t_auth Htag_s_auth".
+  iSplit; last iSplit; last iSplit; last iSplit; last iSplit.
+  - (* tainted *)
+    subst σ_s' α' nt. rewrite -Hsst_eq -Hsnp_eq.
+    by iApply tag_tainted_interp_alloc.
+  - (* state rel *)
+    rewrite -{2}(map_empty_union M_t).
+    subst σ_s' α' nt. rewrite -{2}Hsst_eq.
+    iApply sim_alloc_state_rel_update; last done.
+    intros t (s & Hs) ->. congruence.
+  - (* call interp *)
+    iPureIntro. apply sim_alloc_call_set_interp_update; done.
+  - (* tag interp *)
+    iPureIntro. destruct Htag_interp as (Htag_interp & Hdom_t & Hdom_s). split_and!.
+    { simpl. intros t tk. rewrite lookup_insert_Some. intros [[<- [= <-]] | [Hneq Hsome]].
+      - (* new tag: as these are public, the locations under this tag are not directly controlled *)
+        split_and!; [ lia | lia | | |].
+        + intros l' sc_t Hsc_t. exfalso. specialize (Hdom_t nt l' ltac:(eauto)) as (? &?). subst nt. congruence.
+        + intros l' sc_t Hsc_t. exfalso. specialize (Hdom_s nt l' ltac:(eauto)) as (? &?). subst nt. congruence.
+        + apply dom_agree_on_tag_not_elem.
+          * intros l'. destruct (M_t !! (nt, l')) eqn:Hs; last done.
+            destruct (Hdom_t nt l' ltac:(eauto)) as (? & ?).
+            subst nt. congruence.
+          * intros l'. destruct (M_s !! (nt, l')) eqn:Hs; last done.
+            destruct (Hdom_s nt l' ltac:(eauto)) as (? & ?).
+            subst nt. congruence.
+      - (* old tag *)
+        specialize (Htag_interp _ _ Hsome) as (? & ? & Hcontrol_t & Hcontrol_s & Hag).
+        split_and!; [lia | lia | .. | done].
+        + intros l' sc_t Hcontrol%Hcontrol_t. eapply loc_controlled_alloc_update; done.
+        + intros l' sc_s Hcontrol%Hcontrol_s. subst α' nt σ_s' l.
+          rewrite -Hsnp_eq -Hsst_eq -(fresh_block_det _ _ Hdom_eq).
+          eapply loc_controlled_alloc_update; [ done | lia | done].
+    }
+    { intros t l'. rewrite lookup_insert_is_Some'. eauto. }
+    { intros t l'. rewrite lookup_insert_is_Some'. eauto. }
+  - iPureIntro. by eapply head_step_wf.
+  - iPureIntro. by eapply head_step_wf.
+Qed.
 
 Lemma sim_free_public T_t T_s l_t l_s bor_t bor_s Φ π :
   rrel (PlaceR l_t bor_t T_t) (PlaceR l_s bor_s T_s) -∗
@@ -81,15 +150,54 @@ Proof.
     specialize (for_each_dealloc_lookup_Some _ _ _ _ _ Hstack_s _ _ Hstk') as (_ & Hstk).
     right. right. eauto.
   - (* re-establish the state relation *)
-    admit.
+    iDestruct "Hsrel" as "(_ & _ & _ & _ & _ & Hsrel)".
+    iSplitR. { iPureIntro. simpl. apply free_mem_dom. done. }
+    simpl. do 4 (iSplitR; first done).
+    iIntros (l (sc & Hsome)).
+    destruct (free_mem_lookup_case l l_s (tsize T_s) σ_t.(shp)) as [[Hi Heq] | (i & _ & -> & ?)]; last congruence.
+    rewrite Heq in Hsome. iDestruct ("Hsrel" $! l with "[]") as "[Hpubl | Hprivl]"; first by eauto.
+    + iLeft. iIntros (sc_t Hsc_t). simpl in *.
+      rewrite Heq in Hsc_t. simplify_eq.
+      iDestruct ("Hpubl" $! sc Hsome) as (sc_s) "[%Hsc_s Hscr]".
+      iExists sc_s. iSplitR; last done.
+      iPureIntro.
+      destruct (free_mem_lookup_case l l_s (tsize T_s) σ_s.(shp)) as [[_ Heq'] | (i' & Hi' & -> & _)].
+      2: { specialize (Hi i' Hi'). congruence. }
+      rewrite Heq' Hsc_s. done.
+    + iRight. done.
   - (* re-establish the call set interpretation *)
-    admit.
+    iPureIntro.
+    iIntros (c M' Hc). simpl. specialize (Hcall_interp _ _ Hc) as (? & HM'). split; first done.
+    intros t L HL. specialize (HM' _ _ HL) as (? & HM'). split; first done.
+    intros l Hl. specialize (HM' l Hl) as (stk & pm & Hstk & Hit & Hpm).
+    destruct (for_each_true_lookup_case_2 _ _ _ _ _ Hstack_t) as [EQ1 EQ2].
+    (* from Hstack_s, l cannot be in the affected range because it is protected by c,
+      so α' !! l = σt.(sst) !! l. *)
+    destruct (block_case l_s l (tsize T_s)) as [Hneq|(i & Hi & ->)].
+    + rewrite EQ2//. eauto.
+    + exfalso. clear EQ2.
+      specialize (EQ1 _ Hi) as (stk1 & stk' & Eqstk1 & Eqstk' & Hdealloc).
+      rewrite Eqstk1 in Hstk. simplify_eq.
+      move : Hdealloc. destruct (dealloc1 stk bor_s σ_t.(scs)) eqn:Eqd; last done.
+      intros _.
+      destruct (dealloc1_Some stk bor_s σ_t.(scs)) as (it & Eqit & ? & FA & GR).
+      { by eexists. }
+      rewrite ->Forall_forall in FA. apply (FA _ Hit).
+      rewrite /is_active_protector /= /is_active bool_decide_true //.
   - (* re-establish the tag interpretation *)
-    admit.
+    destruct Htag_interp as (Htag_interp & Hdom_t & Hdom_s).
+    iPureIntro. split_and!; [ | done | done].
+    intros t tk Ht. simpl. specialize (Htag_interp _ _ Ht) as (? & ? & Hcontrol_t & Hcontrol_s & Hag).
+    split_and!; [done | done | | | done].
+    + intros l sc_t Hsc_t%Hcontrol_t.
+      eapply loc_controlled_dealloc_update; [ apply Hstack_t | done | | done].
+      intros [-> _]. rewrite Hpub in Ht. congruence.
+    + intros l sc_s Hsc_s%Hcontrol_s.
+      eapply loc_controlled_dealloc_update; [apply Hstack_s | done | | done].
+      intros [-> _]. rewrite Hpub in Ht. congruence.
   - iPureIntro. by eapply head_step_wf.
   - iPureIntro. by eapply head_step_wf.
-Admitted.
-
+Qed.
 
 Lemma sim_copy_public_controlled_update σ l l' (bor : tag) (T : type) (α' : stacks) (t : ptr_id) (tk : tag_kind) sc :
   memory_read σ.(sst) σ.(scs) l bor (tsize T) = Some α' →