diff --git a/_CoqProject b/_CoqProject
index cda33480461f2046cc638b68e3b6f13fdb777f01..fd0c51064aa623ed614570946cdae3c6d6c50f42 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -157,6 +157,7 @@ gpfsl-examples/stack/code_na.v
 gpfsl-examples/stack/code_treiber.v
 gpfsl-examples/stack/code_elimination.v
 gpfsl-examples/stack/proof_na.v
+gpfsl-examples/stack/proof_treiber_at.v
 gpfsl-examples/stack/proof_treiber_gps.v
 gpfsl-examples/stack/proof_treiber_graph.v
 gpfsl-examples/stack/proof_treiber_history.v
diff --git a/gpfsl-examples/stack/proof_treiber_at.v b/gpfsl-examples/stack/proof_treiber_at.v
new file mode 100644
index 0000000000000000000000000000000000000000..77ef622cfca4eed5e681331823d898f87d2122dd
--- /dev/null
+++ b/gpfsl-examples/stack/proof_treiber_at.v
@@ -0,0 +1,574 @@
+From stdpp Require Import namespaces.
+From iris.proofmode Require Import proofmode.
+
+From gpfsl.base_logic Require Import frame_instances.
+From gpfsl.logic Require Import proofmode.
+From gpfsl.logic Require Import relacq new_delete atomics invariants.
+From gpfsl.examples Require Import map_seq loc_helper list_helper.
+From gpfsl.examples.stack Require Import spec_per_elem code_treiber.
+
+Require Import iris.prelude.options.
+
+Local Notation next := 0%nat (only parsing).
+Local Notation data := 1%nat (only parsing).
+
+(** Basic Treiber Stack in Release-Acquire **)
+(* This implementation is memory-leaking, as it does not care about recollecting
+   memory.
+  Furthermore, this implementation uses 0 and -1 as flags for EMPTY and
+  FAIL_RACE repsectively, so if the client should not push elements with those
+  values, otherwise they'll lose resources. *)
+
+(* Namespace for the invariant *)
+Definition tstackN (s: loc) := nroot .@ "tstackN" .@ s.
+
+Definition oloc_to_lit (on : option loc) : lit :=
+  if on is Some n then LitLoc n else LitInt 0.
+
+Global Instance oloc_to_lit_inj : Inj (=) (=) oloc_to_lit.
+Proof. intros [] []; simpl; naive_solver. Qed.
+
+Definition toHeadHist (start : time) (LVs : list (option loc * view)) : absHist :=
+  map_seqP start ((λ olv, (#(oloc_to_lit olv.1), olv.2)) <$> LVs).
+
+Lemma toHeadHist_lookup_Some t0 LVs t v V :
+  toHeadHist t0 LVs !! t = Some (v, V) ↔
+  (t0 ≤ t)%positive
+  ∧ ∃ on, v = #(oloc_to_lit on)
+  ∧ LVs !! (Pos.to_nat t - Pos.to_nat t0)%nat = Some (on, V).
+Proof.
+  rewrite lookup_map_seqP_Some. f_equiv.
+  rewrite list_lookup_fmap fmap_Some. split.
+  - intros ([] & ? & ?). simplify_eq. naive_solver.
+  - intros (on & -> & ?). exists (on, V). naive_solver.
+Qed.
+
+Lemma toHeadHist_lookup_None t0 LVs t :
+  (toHeadHist t0 LVs) !! t = None ↔
+  (t < t0)%positive ∨ (t0 +p (length LVs) ≤ t)%positive.
+Proof. by rewrite lookup_map_seqP_None fmap_length. Qed.
+
+Lemma toHeadHist_lookup_Some_is_comparable_nullable_loc LVs t0 t v V (on : option loc) :
+  toHeadHist t0 LVs !! t = Some (v, V) →
+  ∃ vl : lit, v = #vl ∧ lit_comparable (oloc_to_lit on) vl.
+Proof.
+  rewrite toHeadHist_lookup_Some. intros (? & on' & -> & _).
+  exists (oloc_to_lit on'). split; [done|].
+  destruct on, on'; constructor.
+Qed.
+
+Lemma toHeadHist_insert t0 LVs t on V  :
+  (Pos.to_nat t - Pos.to_nat t0)%nat = length LVs →
+  (1 ≤ length LVs)%nat →
+  <[t := (#(oloc_to_lit on), V)]>(toHeadHist t0 LVs) =
+  toHeadHist t0 (LVs ++ [(on, V)]).
+Proof.
+  intros Eq ?. apply map_eq.
+  intros i. case (decide (i = t)) => [->|?].
+  - rewrite lookup_insert. symmetry.
+    apply toHeadHist_lookup_Some. split; [lia|].
+    rewrite Eq !lookup_app_r // Nat.sub_diag /=. naive_solver.
+  - rewrite lookup_insert_ne; [|done].
+    destruct (toHeadHist t0 LVs !! i) as [[vi Vi]|] eqn:Eqi; rewrite Eqi; symmetry.
+    + apply toHeadHist_lookup_Some in Eqi as (Letn & on' & -> & Eq1).
+      apply toHeadHist_lookup_Some. split; [done|].
+      exists on'. split; [done|]. by apply (lookup_app_l_Some _ _ _ _ Eq1).
+    + apply toHeadHist_lookup_None.
+      apply toHeadHist_lookup_None in Eqi as [?|Eqi]; [by left|right].
+      rewrite app_length /=. move : Eqi.
+      rewrite Nat.add_1_r pos_add_succ_r_2.
+      rewrite (_: t0 +p length LVs = t); [lia|]. rewrite -Eq /pos_add_nat; lia.
+Qed.
+
+Definition next_nodes S : list (option loc) :=
+  match S with
+  | [] => []
+  | _ :: S' => (Some <$> S') ++ [None]
+  end.
+
+Lemma next_nodes_length S : length (next_nodes S) = length S.
+Proof. destruct S; [done|]. rewrite /= app_length fmap_length /=. lia. Qed.
+
+Lemma next_nodes_cons n S :
+  next_nodes (n :: S) = hd_error S :: next_nodes S.
+Proof. rewrite /=. by destruct S as [|n' S]. Qed.
+
+Section prot.
+Context `{!noprolG Σ, !atomicG Σ} (P: Z → vProp Σ).
+Local Notation vProp := (vProp Σ).
+
+Definition in_sloc (n : loc) (on' : option loc) : vProp :=
+  ∃ (v : Z),
+    (∃ q, n (* >> next *) ↦{q} #(oloc_to_lit on'))
+    ∗ (n >> data) ↦ #v
+    ∗ P v
+    ∗ ⎡ † n … 2 ⎤ (* needed for garbage collection *)
+  .
+
+Definition in_slocs S : vProp :=
+  [∗ list] n ; on' ∈ S ; (next_nodes S), in_sloc n on'.
+
+Definition all_slocs (LVs : list (option loc * view)) : vProp :=
+  (* TODO: use read-only atomic points-to [ROPtsTo] here instead of fractions. *)
+  [∗ list] onV ∈ LVs,
+    if onV is (Some n, V)
+    then (∃ q on, @{V} n (* >> next *) ↦{q} #(oloc_to_lit on))%I
+    else emp%I
+    .
+
+#[global] Instance all_slocs_objective LVs : Objective (all_slocs LVs).
+Proof. apply big_sepL_objective => _ [[n|] V]; apply _. Qed.
+#[global] Instance all_slocs_timeless LVs : Timeless (all_slocs LVs).
+Proof. apply big_sepL_timeless => _ [[n|] V]; apply _. Qed.
+
+Definition Head_inv_no_exists s γ t0 Vb Vh LVs S : vProp :=
+  let vh := (hd_error S) in
+  let LVs' := (LVs ++ [(vh,Vh)]) in
+  let ζ := (toHeadHist t0 LVs') in
+  @{Vb} s at↦{γ} ζ ∗ ⎡ † s … 1 ⎤ ∗
+  @{Vh} in_slocs S ∗
+  all_slocs LVs'.
+
+Definition Head_inv s γ : vProp :=
+  ∃ t0 Vb Vh LVs S, Head_inv_no_exists s γ t0 Vb Vh LVs S.
+
+Global Instance Head_inv_objective s γ : Objective (Head_inv s γ) := _.
+
+Definition TStack s : vProp :=
+  ∃ γ ζ, s sn⊒{γ} ζ ∗ inv (tstackN s) (Head_inv s γ).
+
+Global Instance TStack_persistent s : Persistent (TStack s) := _.
+
+Lemma all_slocs_node_next_access LVs n Vn :
+  (Some n, Vn) ∈ LVs →
+  all_slocs LVs -∗ all_slocs LVs ∗ ∃ q on, @{Vn} n ↦{q} #(oloc_to_lit on).
+Proof.
+  iIntros ([i Inn]%elem_of_list_lookup) "As".
+  rewrite {1}/all_slocs (big_sepL_lookup_acc _ _ _ _ Inn).
+  iDestruct "As" as "[Ns Close]".
+  iDestruct "Ns" as (q on) "[N1 N2]". iSplitL "N1 Close".
+  - iApply "Close". eauto with iFrame.
+  - eauto with iFrame.
+Qed.
+
+Lemma all_slocs_node_access_prim t0 LVs t (l' : loc) :
+  fst <$> toHeadHist t0 LVs !! t = Some #l' →
+  all_slocs LVs ⊢ ∃ (q' : Qp) (C' : cell), ▷ <subj> l' p↦{q'} C'.
+Proof.
+  intros ([] & Eq' & (? & on & Eq & Eq2)%toHeadHist_lookup_Some)%lookup_fmap_Some'.
+  simpl in Eq'. subst v.
+  assert (on = Some l') as ->.
+  { clear -Eq. destruct on; by inversion Eq. } clear Eq.
+  apply elem_of_list_lookup_2 in Eq2.
+  rewrite (all_slocs_node_next_access _ _ _ Eq2).
+  iIntros "[As En]". iDestruct "En" as (q' on) "En". iExists _.
+  by rewrite own_loc_na_view_at_own_loc_prim_subjectively.
+Qed.
+
+Lemma all_slocs_app LVs LVs' :
+  all_slocs (LVs ++ LVs') ⊣⊢ all_slocs LVs ∗ all_slocs LVs'.
+Proof. by rewrite /all_slocs -big_sepL_app. Qed.
+
+Lemma in_slocs_node_access S i n :
+  S !! i = Some n →
+  in_slocs S -∗
+    in_slocs S
+    ∗ ∃ on q, ⌜next_nodes S !! i = Some on ⌝ ∧ n (* >> next *) ↦{q} #(oloc_to_lit on).
+Proof.
+  iIntros (Eqn) "Is".
+  destruct (lookup_lt_is_Some_2 (next_nodes S) i) as [on Eqon].
+  { move : Eqn. rewrite next_nodes_length. by apply lookup_lt_Some. }
+  rewrite {1}/in_slocs (big_sepL2_lookup_acc _ _ _ _ _ _ Eqn Eqon).
+  iDestruct "Is" as "[Ns Close]".
+  iDestruct "Ns" as (v) "[Hn Hd]". iDestruct "Hn" as (q) "[Hn1 Hn2]".
+  iSplitR "Hn2".
+  - iApply "Close". iExists v. eauto with iFrame.
+  - eauto with iFrame.
+Qed.
+
+Lemma in_slocs_optional_head_access S :
+  in_slocs S -∗
+    in_slocs S
+    ∗ if (hd_error S) is Some n
+      then ∃ on q, ⌜ next_nodes S !! 0%nat = Some on ⌝ ∧
+                   n (* >> next *) ↦{q} #(oloc_to_lit on)
+      else emp
+    .
+Proof.
+  destruct S as [|n S]; [eauto|]. iIntros "Is".
+  by iDestruct (in_slocs_node_access _ 0%nat n with "Is") as "[$ $]".
+Qed.
+
+Lemma Head_inv_no_exists_node_next_access s γ t0 Vb Vh LVs S n Vn:
+  let vh := (hd_error S) in
+  (Some n, Vn) ∈ (LVs ++ [(vh,Vh)]) →
+  Head_inv_no_exists s γ t0 Vb Vh LVs S -∗
+    Head_inv_no_exists s γ t0 Vb Vh LVs S
+    ∗ ∃ q on, @{Vn} n ↦{q} #(oloc_to_lit on).
+Proof.
+  iIntros (vh Inn) "($ & $ & $ & As)". by iApply all_slocs_node_next_access.
+Qed.
+
+Lemma in_sloc_cons n S :
+  in_slocs (n :: S) ⊣⊢
+  in_sloc n (hd_error S) ∗ in_slocs S .
+Proof. rewrite /in_slocs next_nodes_cons big_sepL2_cons. by eauto. Qed.
+
+End prot.
+
+Section proof.
+Context `{!noprolG Σ, !atomicG Σ} (P: Z → vProp Σ).
+Local Notation vProp := (vProp Σ).
+
+Lemma new_tstack_spec tid :
+  {{{ True }}}
+      new_tstack [] @ tid; ⊤
+  {{{ (s: loc), RET #s; TStack P s }}}.
+Proof.
+  iIntros (Φ) "_ Post".
+  wp_lam.
+  (* allocate head *)
+  wp_apply wp_new; [done..|].
+  iIntros (s) "([H†|%] & Hs & Hms)"; [|done].
+  wp_let.
+  (* initialize head as 0, and create protocol *)
+  rewrite own_loc_na_vec_singleton.
+  iApply wp_fupd.
+  wp_write.
+  iMod (AtomicPtsTo_CON_from_na with "Hs") as (γ t0 V0) "(sV0 & sN & sA)".
+  iMod (inv_alloc (tstackN s) _ (Head_inv P s γ) with "[H† sA]") as "Inv".
+  { iNext. rewrite /Head_inv.
+    iDestruct (view_at_intro with "sA") as (V1) "[sV1 sA]".
+    iExists t0, V1, V0, [], []. rewrite /Head_inv_no_exists. iFrame "H†".
+    iSplitL "sA". { rewrite /toHeadHist /= insert_empty. by iFrame. }
+    iSplit.
+    - by rewrite /in_slocs /=.
+    - by rewrite /all_slocs /=. }
+  iIntros "!>". iApply ("Post"). iExists γ, _. by iFrame.
+Qed.
+
+Lemma try_push_spec s v tid :
+  {{{ TStack P s ∗ P v }}}
+      try_push [ #s; #v] @ tid; ⊤
+  {{{ (b: bool), RET #b; if b then True else P v }}}.
+Proof.
+  iIntros (Φ) "[Stack P] Post".
+  wp_lam.
+  (* allocate new node *)
+  wp_apply wp_new; [done..|].
+  iIntros (n) "([H†|%] & Hn & Hmn)"; [|done].
+  (* write data to new node *)
+  rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
+  iDestruct "Hn" as "[Hn Hd]".
+  wp_pures. wp_write. wp_lam.
+
+  iDestruct "Stack" as (γ ζs) "[#sS #sI]".
+  wp_bind (!ʳˡˣ_)%E.
+  (* read possible head of stack *)
+  (* open shared invariant *)
+  iInv (tstackN s) as (t0 Vb Vh LVs S) "[>Hs HIC]" "Close".
+  (* ready to read *)
+  iDestruct (monPred_in_bot) as "#sV0".
+  wp_apply (AtomicSeen_relaxed_read with "[$sS $Hs $sV0]"); first solve_ndisj.
+
+  iIntros (th1 vh1 V0 V1 ζh0') "(Subζ & #sV1 & _ & #sH1 & Hs)".
+  iDestruct "Subζ" as %([Subζh0 Subζh0'] & Eqth1 & _).
+  assert (Eqth1' := lookup_weaken _ _ _ _ Eqth1 Subζh0').
+
+  (* close the invariant *)
+  iMod ("Close" with "[Hs HIC]") as "_".
+  { iIntros "{#} !>". iExists _, _, _, _, _. iFrame "Hs HIC". }
+
+  (* check what we just read *)
+  assert (EqH := Eqth1').
+  apply toHeadHist_lookup_Some in EqH as (_ & on' & -> & EqLVs0).
+
+  (* set n's link to what we read from Head *)
+  iIntros "!>". wp_let. wp_op. rewrite shift_0. wp_write.
+
+  (* prepare to CAS on Head to push *)
+  clear Vb.
+  wp_bind (casʳᵉˡ(_,_,_))%E.
+  (* open the invariant *)
+  iInv (tstackN s) as (t02 Vb Vh2 LVs2 S2) "(>Hs & Hdd & Is & >As)" "Close".
+
+  iCombine "Hn Hd P" as "Hnd".
+  iDestruct (view_at_intro_incl with "Hnd sV1") as (V1') "(#sV1' & %LeV1 & Hnd)".
+
+  iDestruct (view_at_elim with "sV1 sH1") as "sH1'".
+  iDestruct (AtomicPtsTo_AtomicSeen_latest_1 with "Hs sH1'") as %Subζ0.
+
+  set Pr : vProp := all_slocs (LVs2 ++ [(hd_error S2, Vh2)])%I.
+
+  (* CAS with possible pointer comparison *)
+  wp_apply (AtomicSeen_CON_CAS _ _ _ _ _ _ _ (oloc_to_lit on') #n _ ∅ Pr
+              with "[$sH1' $Hs $sV1' $As]"); [done|done|done|solve_ndisj|..].
+  { intros t' v' NE. rewrite lookup_fmap_Some'.
+    intros ([] & <- & ?). by eapply toHeadHist_lookup_Some_is_comparable_nullable_loc. }
+  { iSplit; [done|]. iIntros "{#} !>". destruct on' as [n'|]; [|done].
+    simpl. clear -Eqth1 Subζ0. iIntros "As !>".
+    (* acquire a fraction of n' *)
+    rewrite /Pr (all_slocs_node_next_access _ n' V0); last first.
+    { eapply lookup_weaken in Eqth1; [|apply Subζ0]. simpl in Eqth1.
+      clear -Eqth1. apply toHeadHist_lookup_Some in Eqth1 as (_ & on' & Eq & Eq1).
+      destruct on' as [n''|]; [|done]. inversion Eq. subst n''.
+      move : Eq1. by apply elem_of_list_lookup_2. }
+    iDestruct "As" as "[As oN]". iDestruct "oN" as (qn' on') "oN".
+    iSplitL "oN".
+    - iExists _. by rewrite own_loc_na_view_at_own_loc_prim_subjectively.
+    - iIntros (?? (_ & ? & _)). by iApply (all_slocs_node_access_prim with "As"). }
+
+  iIntros (b t' v' Vr V2 ζ2 ζn) "(F & #sV2 & #sH2 & Hs & As & CASE)".
+  iDestruct "F" as %([Subζh02 Subζ2] & Eqt' & MAXt' & LeV1'). subst Pr.
+
+  iDestruct "CASE" as "[[F sVr]|[F sVw]]".
+  { (* fail CAS *)
+    iDestruct "F" as %(-> & NEq & ->).
+    iMod ("Close" with "[Hdd Hs As Is]") as "_".
+    { iNext. iExists _, (Vb ⊔ V2), Vh2, LVs2, _. iFrame. }
+
+    iIntros "!>". wp_if.
+    (* cleaning up *)
+    iDestruct (view_at_elim with "sV1' Hnd") as "(Hn & Hd & P)".
+    wp_apply (wp_delete _ tid 2 _ [ _; #v] with "[H† Hn Hd]"); [done|done|..].
+    { rewrite own_loc_na_vec_cons own_loc_na_vec_singleton. by iFrame. }
+    iIntros "_". wp_seq. by iApply "Post". }
+
+  (* successful CAS *)
+  iDestruct "F" as %[-> ->].
+  iDestruct "sVw" as (Vw (FRt & Eqζn & Eqt'' & LeVr & SLeVr & NLeVr & NEqV1' & LeV1w))
+                    "#[sHVw sVw]".
+
+  assert (Eqt2 := lookup_weaken _ _ _ _ Eqt' Subζ2).
+  rewrite Eqζn lookup_insert_ne in Eqt2; last by (clear; lia).
+  apply toHeadHist_lookup_Some in Eqt2 as (Let02 & on & Eqon & Eqn2).
+  assert (on = on') as ->.
+  { clear -Eqon. by destruct on, on'; inversion Eqon. } clear Eqon.
+
+  assert (EqL: (Pos.to_nat t' - Pos.to_nat t02)%nat = length LVs2).
+  { assert (LtL := lookup_lt_Some _ _ _ Eqn2).
+    clear -FRt Let02 LtL.
+    apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
+    apply : (anti_symm (le)).
+    - clear -LtL. rewrite app_length /= in LtL. lia.
+    - clear LtL. rewrite app_length /= /pos_add_nat in Let'; lia. }
+  rewrite EqL in Eqn2.
+  assert (Vh2 = Vr ∧ on' = hd_error S2) as [-> ->].
+  { clear -Eqn2. apply lookup_last_Some_2 in Eqn2. by inversion Eqn2. }
+
+  set S' := n :: S2.
+  set LVs' := (LVs2 ++ [(hd_error S2,Vr)]) ++ [(Some n, Vw)].
+  iAssert (all_slocs LVs' ∗ @{Vw} in_slocs P S')%I
+    with "[H† As Is Hnd]" as "[As Is]".
+  { iDestruct (view_at_mono_2 _ Vw with "Hnd") as "([Hn1 Hn2] & Hd & P) {#}";
+      [solve_lat|]. iSplitL "As Hn1".
+    - rewrite (all_slocs_app (_ ++ _)). iSplitL "As"; [by iFrame "As"|].
+      rewrite /all_slocs /=. iSplitL; [|done]. iExists _, (hd_error S2).
+      iFrame "Hn1".
+    - rewrite in_sloc_cons. iFrame "Is".
+      iExists v. rewrite /= /in_sloc. iFrame. iExists _. by iFrame "Hn2". }
+
+  (* re-establish the invariant *)
+  iMod ("Close" with "[-Post Hmn]") as "_".
+  { iNext. iExists t02, (Vb ⊔ V2), Vw, _, S'.
+    iFrame "Hdd Is As". rewrite Eqζn.
+    rewrite (_: toHeadHist t02 LVs' =
+      <[(t' + 1)%positive:=(#n, Vw)]> (toHeadHist t02 (LVs2 ++ [(hd_error S2, Vr)])));
+      first done.
+    symmetry. apply (toHeadHist_insert _ _ _ (Some n)).
+    - clear -Let02 EqL. rewrite app_length /=. lia.
+    - clear. rewrite app_length /=. lia. }
+
+  iIntros "!>". wp_if. by iApply "Post".
+Qed.
+
+Lemma push_spec s v tid :
+  {{{ TStack P s ∗ P v }}}
+      push_slow [ #s; #v] @ tid; ⊤
+  {{{ RET #☠; True }}}.
+Proof.
+  iIntros (Φ) "[#S P] Post".
+  iLöb as "IH". wp_rec. wp_bind (try_push _)%E.
+  iApply (try_push_spec with "[$S $P]").
+  iIntros "!>" (b) "P". destruct b; wp_if.
+  - by iApply "Post".
+  - by iApply ("IH" with "P Post").
+Qed.
+
+Lemma try_pop_spec s tid :
+  {{{ TStack P s }}}
+    try_pop [ #s] @ tid; ⊤
+  {{{ v, RET #v; ⌜v = EMPTY⌝ ∨ ⌜v = FAIL_RACE⌝ ∨ P v }}}.
+Proof.
+  iIntros (Φ) "Stack Post".
+  wp_lam.
+
+  iDestruct "Stack" as (γ ζs) "[#sS #sI]".
+  wp_bind (!ᵃᶜ_)%E.
+
+  (* read possible head of stack *)
+  (* open shared invariant *)
+  iInv (tstackN s) as (t0 Vb Vh LVs S) "[>Hs HIC]" "Close".
+  (* ready to read *)
+  iDestruct (monPred_in_bot) as "#sV0".
+  wp_apply (AtomicSeen_acquire_read with "[$sS $Hs $sV0]"); first solve_ndisj.
+
+  iIntros (th1 vh1 V1' V1 ζh0') "(Subζ & #sV1 & #sH1 & Hs)".
+  iDestruct "Subζ" as %([Subζh0 Subζh0'] & Eqth1 & MAXth1 & LeV').
+  assert (Eqth1' := lookup_weaken _ _ _ _ Eqth1 Subζh0').
+
+  (* check what we just read *)
+  assert (EqH := Eqth1').
+  apply toHeadHist_lookup_Some in EqH as (Leth0 & on & -> & EqLVs0).
+
+  iAssert (Head_inv_no_exists P s γ t0 (Vb ⊔ V1) Vh LVs S)%I
+    with "[Hs HIC]" as "HIC". { by iFrame. }
+
+  destruct on as [n|]; last first.
+  { (* EMPTY POP *)
+    (* close the invariant *)
+    iMod ("Close" with "[HIC]") as "_".
+    { iIntros "{#} !>". iExists _, _, _, _, _. by iFrame. }
+
+    iIntros "!>". wp_let.
+
+    simpl. wp_op. wp_if. iApply "Post". by iLeft. }
+
+  (* but we acquire a fraction of `n >> next` to read *)
+  iDestruct (Head_inv_no_exists_node_next_access _ _ _ _ _ _ _ _ n V1' with "HIC")
+    as "[HIC oN]".
+  { move : EqLVs0. apply elem_of_list_lookup_2. }
+
+  iMod ("Close" with "[HIC]") as "_".
+  { iIntros "{#} !>". iExists _, _, _, _, _. by iFrame. }
+
+  iIntros "!>". wp_let.
+  simpl. wp_op. wp_if. wp_op.
+
+  (* read `n >> next` non-atomically *)
+  iDestruct "oN" as (q on') "oN".
+  iDestruct (view_at_elim with "[] oN") as "oN".
+  { iApply (monPred_in_mono with "sV1"). simpl. solve_lat. }
+  rewrite shift_0. wp_read. wp_let.
+
+  clear Vb. wp_bind (casᵃᶜ(_,_,_))%E.
+
+  iMod (rel_objectively_intro (⊒∅) tid with "[]") as "HRE".
+  { iApply (objective_objectively with "sV0"). }
+
+  iDestruct (view_at_elim with "sV1 sH1") as "sH1'".
+
+  (* open the invariant *)
+  iInv (tstackN s) as (t02 Vb Vh2 LVs2 S2) "(>Hs & Hdd & Is & >As)" "Close".
+
+  set Pr : vProp :=
+    (n ↦{q} #(oloc_to_lit on') ∗ all_slocs (LVs2 ++ [(hd_error S2, Vh2)]))%I.
+  wp_apply (AtomicSeen_CON_CAS_live_loc _ _ _ _ _ _ _ n #(oloc_to_lit on') Pr _ ∅
+              with "[$sH1' $Hs $sV1 HRE $oN $As]"); [done|done|done|solve_ndisj|..].
+  { intros t v NE. rewrite lookup_fmap_Some'.
+    intros ([] & <- & ?).
+    by eapply (toHeadHist_lookup_Some_is_comparable_nullable_loc _ _ _ _ _ (Some n)). }
+  { simpl. iIntros "{# $HRE %} !> [oN As] !>". iSplitL "oN".
+    - iExists _. by rewrite own_loc_na_own_loc_prim_subjectively.
+    - iIntros (?? (_ & ? & _)). by iApply (all_slocs_node_access_prim with "As"). }
+
+  iIntros (b t' v' V2 V2' ζh2'' ζh2) "(F & #sV2' & #sH2 & Hs & [oN As] & CASE)".
+  iDestruct "F" as %([Subζh0'' Subζh2''] & Eqt' & MAXt' & LeV1). clear Pr.
+
+  iDestruct "CASE" as "[[(%&%&%) HV2]|([%%] & CASE)]".
+  { (* FAIL_RACE case *) 
+    (* COMMIT with no change *)
+    subst b ζh2.
+
+    iMod ("Close" with "[Hs Hdd As Is]") as "_".
+    { iNext. iExists t02, _, Vh2, LVs2, S2. rewrite /Head_inv_no_exists.
+      by iFrame "Hs Hdd Is As". }
+    iIntros "!>". wp_if. iApply "Post". by iRight; iLeft. }
+
+  subst b v'.
+  iDestruct "CASE" as (Vw (FRt & Eqζh2 & Eqt2 & LeV2 & _)) "[_ %LeV2']".
+  have LeV22: V2 ⊑ V2' by etrans.
+
+  have Eqt2': toHeadHist t02 (LVs2 ++ [(hd_error S2, Vh2)]) !! t' = Some (#n, V2).
+  { eapply lookup_weaken in Eqt'; [|apply Subζh2''].
+    rewrite Eqζh2 lookup_insert_ne in Eqt'; [done|lia]. }
+
+  apply toHeadHist_lookup_Some in Eqt2' as (Let02 & on & Eqon & Eqn2).
+  assert (on = Some n) as ->.
+  { clear -Eqon. by destruct on; inversion Eqon. } clear Eqon.
+
+  assert (EqL: (Pos.to_nat t' - Pos.to_nat t02)%nat = length LVs2).
+  { assert (LtL := lookup_lt_Some _ _ _ Eqn2).
+    clear -FRt Let02 LtL.
+    apply toHeadHist_lookup_None in FRt as [?|Let']; first (exfalso; lia).
+    apply : (anti_symm (le)).
+    - clear -LtL. rewrite app_length /= in LtL. lia.
+    - clear LtL.
+      rewrite app_length /= /pos_add_nat in Let'; lia. }
+  rewrite EqL in Eqn2.
+  assert (Vh2 = V2 ∧ ∃ S2', S2 = n :: S2') as (-> & S2' & ->).
+  { clear -Eqn2. apply lookup_last_Some_2 in Eqn2. inversion Eqn2 as [Eq1].
+    split; [done|]. destruct S2; inversion Eq1. by eexists. }
+
+  (* get the location *)
+  rewrite in_sloc_cons in_slocs_optional_head_access.
+  iDestruct "Is" as "(Hn & Is & HSh)".
+  iDestruct "Hn" as (vn) "(Hnn & Hnd)".
+
+  iAssert (⊒V2)%I with "[]" as "#sV2". { by iApply (monPred_in_mono with "sV2'"). }
+  iAssert (⌜on' = hd_error S2'⌝)%I with "[Hnn oN]" as %->.
+  { clear. iDestruct (view_at_elim with "sV2 Hnn") as (q') "Hnn".
+    iDestruct (own_loc_na_agree with "oN Hnn") as %Eq. iPureIntro.
+    inversion Eq as [Eq']. by apply oloc_to_lit_inj in Eq'. }
+
+  iAssert (all_slocs ((LVs2 ++ [(Some n, V2)]) ++ [(hd_error S2', Vw)]))%I
+    with "[Hnn HSh As]" as "As".
+  { rewrite {2}/all_slocs big_sepL_app big_sepL_singleton.
+    iSplitL "As"; [by iFrame|].
+    destruct S2' as [|n' S2''] eqn:Eqn'; [eauto|]; simpl.
+    iDestruct "HSh" as (on'' q' EqS) "H". iExists q', on''. by iFrame "H". }
+
+  iMod ("Close" with "[Hs Hdd As Is]") as "_".
+  { iNext. iExists t02, (Vb ⊔ V2'), Vw, _, S2'. rewrite /Head_inv_no_exists.
+    iFrame "Hdd As". iSplitR "Is"; last by iFrame "Is".
+    set LVs' := (LVs2 ++ [(Some n, V2)]).
+    rewrite (_ : toHeadHist t02 (LVs' ++ [(hd_error S2', Vw)]) = ζh2);
+      first done.
+    rewrite Eqζh2 toHeadHist_insert; [done|..].
+    - clear -EqL Let02. rewrite app_length /= -EqL. lia.
+    - clear. rewrite app_length /=. lia. }
+
+  iDestruct (view_at_elim with "sV2 Hnd") as "(Hd & P & Hn†)".
+  iIntros "!>". wp_if. wp_op.
+  (* read popped value *)
+  wp_read. iApply "Post".
+  (* TODO: leaking of n *)
+  by iRight; iRight.
+Qed.
+
+Lemma pop_spec s tid :
+  {{{ TStack P s }}}
+    pop [ #s] @ tid; ⊤
+  {{{ v, RET #v; if decide (v = 0) then True else P v }}}.
+Proof.
+  iIntros (Φ) "#S Post".
+  iLöb as "IH". wp_rec. wp_bind (try_pop _)%E.
+  iApply (try_pop_spec with "S").
+  iIntros "!>" (v) "P". wp_pures.
+  case_bool_decide.
+  - subst v. by iApply ("IH" with "Post").
+  - wp_finish. iApply "Post". case decide => ?; [done|].
+    by iDestruct "P" as "[%|[%|P]]".
+Qed.
+End proof.
+
+#[global] Typeclasses Opaque TStack.
+
+Definition TreiberStack_per_elem_instance `{!noprolG Σ, !atomicG Σ} :
+  stack_per_elem_spec Σ := {|
+    spec_per_elem.new_stack_spec := new_tstack_spec ;
+    spec_per_elem.push_spec      := push_spec ;
+    spec_per_elem.pop_spec       := pop_spec ;
+    spec_per_elem.try_push_spec  := try_push_spec ;
+    spec_per_elem.try_pop_spec   := try_pop_spec ;
+  |}.