New concurrent stack formalization

theories/concurrent_stacks/concurrent_stack1.v

-From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
-From iris.program_logic Require Export weakestpre hoare.
-From iris.heap_lang Require Export lang.
-From iris.algebra Require Import agree list.
-From iris.heap_lang Require Import assert proofmode notation.
-
-From iris_examples.concurrent_stacks Require Import spec.
-
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Import notation proofmode.
 Set Default Proof Using "Type".
 
-(** Stack 1: No helping, bag spec. *)
-
-Definition mk_stack : val :=
-  λ: "_",
-  let: "r" := ref NONEV in
-  (rec: "pop" "n" :=
-     match: !"r" with
-       NONE => NONE
-     | SOME "hd" =>
-       if: CAS "r" (SOME "hd") (Snd !"hd")
-       then SOME (Fst !"hd")
-       else "pop" "n"
-     end,
-    rec: "push" "n" :=
-       let: "r'" := !"r" in
-       let: "r''" := SOME (Alloc ("n", "r'")) in
-       if: CAS "r" "r'" "r''"
-       then #()
-       else "push" "n").
+Definition new_stack : val := λ: "_", ref NONEV.
+Definition push : val :=
+  rec: "push" "s" "v" :=
+    let: "tail" := ! "s" in
+    let: "new" := SOME (ref ("v", "tail")) in
+    if: CAS "s" "tail" "new" then #() else "push" "s" "v".
+Definition pop : val :=
+  rec: "pop" "s" :=
+    match: !"s" with
+      NONE => NONEV
+    | SOME "l" =>
+      let: "pair" := !"l" in
+      if: CAS "s" (SOME "l") (Snd "pair")
+      then SOME (Fst "pair")
+      else "pop" "s"
+    end.
 
 Section stacks.
-  Context `{!heapG Σ}.
+  Context `{!heapG Σ} (N : namespace).
   Implicit Types l : loc.
 
-  Definition oloc_to_val (h : option loc) : val :=
-    match h with
-    | None => NONEV
-    | Some l => SOMEV #l
-    end.
-  Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
-  Proof. rewrite /Inj /oloc_to_val=>??. repeat case_match; congruence. Qed.
+  Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I
+    (at level 20, format "l  ↦{-}  v") : bi_scope.
+
+  Lemma partial_mapsto_duplicable l v :
+    l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v.
+  Proof.
+    iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
+  Qed.
 
-  Definition is_stack_pre (P : val → iProp Σ) (F : option loc -c> iProp Σ) :
-     option loc -c> iProp Σ := λ v,
-    (match v with
-     | None => True
-     | Some l => ∃ q h t, l ↦{q} (h, oloc_to_val t) ∗ P h ∗ ▷ F t
-     end)%I.
+  Definition is_list_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
+     val -c> iProp Σ := λ v,
+    (v ≡ NONEV ∨ ∃ (l : loc) (h t : val), ⌜v ≡ SOMEV #l⌝ ∗ l ↦{-} (h, t)%V ∗ P h ∗ ▷ F t)%I.
 
-  Local Instance is_stack_contr (P : val → iProp Σ): Contractive (is_stack_pre P).
+  Local Instance is_list_contr (P : val → iProp Σ) : Contractive (is_list_pre P).
   Proof.
-    rewrite /is_stack_pre => n f f' Hf v.
+    rewrite /is_list_pre => n f f' Hf v.
     repeat (f_contractive || f_equiv).
     apply Hf.
   Qed.
 
-  Definition is_stack_def (P : val -> iProp Σ) := fixpoint (is_stack_pre P).
-  Definition is_stack_aux P : seal (@is_stack_def P). by eexists. Qed.
-  Definition is_stack P := unseal (is_stack_aux P).
-  Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P).
-
-  Definition stack_inv P l :=
-    (∃ ol, l ↦ oloc_to_val ol ∗ is_stack P ol)%I.
+  Definition is_list_def (P : val -> iProp Σ) := fixpoint (is_list_pre P).
+  Definition is_list_aux P : seal (@is_list_def P). by eexists. Qed.
+  Definition is_list P := unseal (is_list_aux P).
+  Definition is_list_eq P : @is_list P = @is_list_def P := seal_eq (is_list_aux P).
 
+  Lemma is_list_unfold (P : val → iProp Σ) v :
+    is_list P v ⊣⊢ is_list_pre P (is_list P) v.
+  Proof.
+    rewrite is_list_eq. apply (fixpoint_unfold (is_list_pre P)).
+  Qed.
 
-  Lemma is_stack_unfold (P : val → iProp Σ) v :
-      is_stack P v ⊣⊢ is_stack_pre P (is_stack P) v.
+  (* TODO: shouldn't have to explicitly return is_list *)
+  Lemma is_list_unboxed (P : val → iProp Σ) v :
+      is_list P v -∗ ⌜val_is_unboxed v⌝ ∗ is_list P v.
   Proof.
-    rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)).
+    iIntros "Hstack"; iSplit; last done;
+    iDestruct (is_list_unfold with "Hstack") as "[->|Hstack]";
+    last iDestruct "Hstack" as (l h t) "(-> & _)"; done.
   Qed.
 
-  Lemma is_stack_copy (P : val → iProp Σ) ol :
-      is_stack P ol -∗ is_stack P ol ∗
-           (match ol with None => True | Some l => ∃ q h t, l ↦{q} (h, oloc_to_val t) end).
+  Lemma is_list_disj (P : val → iProp Σ) v :
+    is_list P v -∗ is_list P v ∗ (⌜v ≡ NONEV⌝ ∨ ∃ (l : loc) h t, ⌜v ≡ SOMEV #l%V⌝ ∗ l ↦{-} (h, t)%V).
   Proof.
     iIntros "Hstack".
-    iDestruct (is_stack_unfold with "Hstack") as "Hstack". destruct ol; last first.
-    - iSplitL; try iApply is_stack_unfold; auto.
-    - iDestruct "Hstack" as (q h t) "[[Hl1 Hl2] [HP Hrest]]".
-      iSplitR "Hl2"; try iApply is_stack_unfold; simpl; eauto 10 with iFrame.
+    iDestruct (is_list_unfold with "Hstack") as "[%|Hstack]"; simplify_eq.
+    - rewrite is_list_unfold; iSplitR; [iLeft|]; eauto.
+    - iDestruct "Hstack" as (l h t) "(% & Hl & Hlist)".
+      iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]"; simplify_eq.
+      rewrite (is_list_unfold _ (InjRV _)); iSplitR "Hl2"; iRight; iExists _, _, _; by iFrame.
   Qed.
 
-  (* Per-element invariant (i.e., bag spec). *)
-  Theorem stack_works P Φ :
-    ▷ (∀ (f₁ f₂ : val),
-            (□ WP f₁ #() {{ v, (∃ v', v ≡ SOMEV v' ∗ P v')  ∨  v ≡ NONEV }})
-         -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }}))
-         -∗ Φ (f₁, f₂)%V)%I
-    -∗ WP mk_stack #()  {{ Φ }}.
+  Definition stack_inv P v :=
+    (∃ l v', ⌜v = #l⌝ ∗ l ↦ v' ∗ is_list P v')%I.
+
+  Definition is_stack (P : val → iProp Σ) v :=
+    inv N (stack_inv P v).
+
+  Theorem mk_stack_spec P :
+    WP new_stack #() {{ s, is_stack P s }}%I.
   Proof.
-    iIntros "HΦ".
+    iApply wp_fupd.
     wp_lam.
-    wp_alloc l as "Hl".
-    pose proof (nroot .@ "N") as N.
-    rewrite -wp_fupd.
-    iMod (inv_alloc N _ (stack_inv P l) with "[Hl]") as "#Hisstack".
-    { iExists None; iFrame; auto.
-      iApply is_stack_unfold. auto. }
-    wp_pures.
+    wp_alloc ℓ as "Hl".
+    iMod (inv_alloc N ⊤ (stack_inv P #ℓ) with "[Hl]") as "Hinv".
+    { iNext; iExists ℓ, NONEV; iFrame;
+      by iSplit; last (iApply is_list_unfold; iLeft). }
+    done.
+  Qed.
+
+  Theorem push_spec P s v :
+    {{{ is_stack P s ∗ P v }}} push s v {{{ RET #(); True }}}.
+  Proof.
+    iIntros (Φ) "[#Hstack HP] HΦ".
+    iLöb as "IH".
+    wp_lam. wp_lam. wp_bind (Load _).
+    iInv N as (ℓ v') "(>% & Hl & Hlist)" "Hclose"; subst.
+    wp_load.
+    iMod ("Hclose" with "[Hl Hlist]") as "_".
+    { iNext; iExists _, _; by iFrame. }
+    iModIntro. wp_let. wp_alloc ℓ' as "Hl'". wp_let. wp_bind (CAS _ _ _).
+    iInv N as (ℓ'' v'') "(>% & >Hl & Hlist)" "Hclose"; simplify_eq.
+    destruct (decide (v' = v'')) as [ -> |].
+    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
+      wp_cas_suc.
+      iMod ("Hclose" with "[HP Hl Hl' Hlist]") as "_".
+      { iNext; iExists _, (InjRV #ℓ'); iFrame; iSplit; first done;
+        rewrite (is_list_unfold _ (InjRV _)). iRight; iExists _, _, _; iFrame; eauto. }
+      iModIntro.
+      wp_if.
+      by iApply "HΦ".
+    - iDestruct (is_list_unboxed with "Hlist") as "[>% Hlist]".
+      wp_cas_fail.
+      iMod ("Hclose" with "[Hl Hlist]") as "_".
+      { iNext; iExists _, _; by iFrame. }
+      iModIntro.
+      wp_if.
+      iApply ("IH" with "HP HΦ").
+  Qed.
+
+  Theorem pop_works P s :
+    {{{ is_stack P s }}} pop s {{{ ov, RET ov; ⌜ov = NONEV⌝ ∨ ∃ v, ⌜ov = SOMEV v⌝ ∗ P v }}}.
+  Proof.
+    iIntros (Φ) "#Hstack HΦ".
+    iLöb as "IH".
+    wp_lam. wp_bind (Load _).
+    iInv N as (ℓ v') "(>% & Hl & Hlist)" "Hclose"; subst.
+    wp_load.
+    iDestruct (is_list_disj with "Hlist") as "[Hlist Hdisj]".
+    iMod ("Hclose" with "[Hl Hlist]") as "_".
+    { iNext; iExists _, _; by iFrame. }
     iModIntro.
-    iApply "HΦ".
-    - iIntros "!#".
-      iLöb as "IH".
-      wp_rec.
-      wp_bind (! #l)%E.
-      iInv N as "Hstack" "Hclose".
-      iDestruct "Hstack" as (v') "[Hl' Hstack]".
+    iDestruct "Hdisj" as "[-> | Heq]".
+    - wp_match.
+      iApply "HΦ"; by iLeft.
+    - iDestruct "Heq" as (l h t) "[-> Hl]".
+      wp_match. wp_bind (Load _).
+      iInv N as (ℓ' v') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
+      iDestruct "Hl" as (q) "Hl".
       wp_load.
-      destruct v' as [l'|]; simpl; last first.
-      + iMod ("Hclose" with "[Hl' Hstack]") as "_".
-        { rewrite /stack_inv. eauto with iFrame. }
-        iModIntro. wp_match. wp_pures. by iRight.
-      + iDestruct (is_stack_copy with "Hstack") as "[Hstack Hmy]".
-        iDestruct "Hmy" as (q h t) "Hl".
-        iMod ("Hclose" with "[Hl' Hstack]") as "_".
-        { rewrite /stack_inv. eauto with iFrame. }
-        iModIntro. wp_match.
-        wp_load. wp_pures.
-        wp_bind (CAS _ _ _).
-        iInv N as "Hstack" "Hclose".
-        iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
-        destruct (decide (oloc_to_val v'' = oloc_to_val (Some l'))) as [->%oloc_to_val_inj|Hne].
-        * simpl. wp_cas_suc.
-          iDestruct (is_stack_unfold with "Hstack") as "Hstack".
-          iDestruct "Hstack" as (q' h' t') "[Hl' [HP Hstack]]".
-          iDestruct (mapsto_agree with "Hl Hl'") as %[= <- <-%oloc_to_val_inj].
-          iMod ("Hclose" with "[Hl'' Hstack]").
-          { iExists _. auto with iFrame. }
-          iModIntro.
-          wp_if.
-          wp_load.
-          wp_pures.
-          eauto.
-        * simpl in Hne. wp_cas_fail.
-          iMod ("Hclose" with "[Hl'' Hstack]").
-          { iExists v''; iFrame; auto. }
-          iModIntro.
-          wp_if.
-          iApply "IH".
-    - iIntros (v) "!# HP".
-      iLöb as "IH".
-      wp_rec.
-      wp_bind (! _)%E.
-      iInv N as "Hstack" "Hclose".
-      iDestruct "Hstack" as (v') "[Hl' Hstack]".
-      wp_load.
-      iMod ("Hclose" with "[Hl' Hstack]").
-      { iExists v'. iFrame. }
+      iMod ("Hclose" with "[Hl' Hlist]") as "_".
+      { iNext; iExists _, _; by iFrame. }
       iModIntro.
-      wp_let.
-      wp_alloc r'' as "Hr''".
-      wp_pures. wp_bind (CAS _ _ _).
-      iInv N as "Hstack" "Hclose".
-      iDestruct "Hstack" as (v'') "[Hl'' Hstack]".
-      wp_cas as ->%oloc_to_val_inj|_.
-      + destruct v'; by right.
-      + iMod ("Hclose" with "[Hl'' Hr'' HP Hstack]").
-        iExists (Some r'').
-        iFrame; auto.
-        iNext.
-        iApply is_stack_unfold.
-        simpl.
-        iExists _, _, v'. iFrame.
+      wp_let. wp_proj. wp_bind (CAS _ _ _).
+      iInv N as (ℓ'' v'') "(>% & Hl' & Hlist)" "Hclose". simplify_eq.
+      destruct (decide (v'' = InjRV #l)) as [-> |].
+      * rewrite is_list_unfold.
+        iDestruct "Hlist" as "[>% | H]"; first done.
+        iDestruct "H" as (ℓ''' h' t') "(>% & Hl'' & HP & Hlist)"; simplify_eq.
+        iDestruct "Hl''" as (q') "Hl''".
+        wp_cas_suc.
+        iDestruct (mapsto_agree with "Hl'' Hl") as "%"; simplify_eq.
+        iMod ("Hclose" with "[Hl' Hlist]") as "_".
+        { iNext; iExists ℓ'', _; by iFrame. }
         iModIntro.
         wp_if.
-        done.
-      + iMod ("Hclose" with "[Hl'' Hstack]").
-        iExists v''; iFrame; auto.
+        wp_proj.
+        iApply ("HΦ" with "[HP]"); iRight; iExists h; by iFrame.
+      * wp_cas_fail.
+        iMod ("Hclose" with "[Hl' Hlist]") as "_".
+        { iNext; iExists ℓ'', _; by iFrame. }
         iModIntro.
         wp_if.
-        iApply "IH".
-        done.
+        iApply ("IH" with "HΦ").
   Qed.
 End stacks.
-
-Program Definition is_concurrent_bag `{!heapG Σ} : concurrent_bag Σ :=
-  {| spec.mk_bag := mk_stack |}.
-Next Obligation.
-  iIntros (??? P Φ) "_ HΦ". iApply stack_works.
-  iNext. iIntros (f₁ f₂) "Hpop Hpush". iApply "HΦ". iFrame.
-Qed.

theories/concurrent_stacks/concurrent_stack3.v

 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.algebra Require Import excl.
-
-From iris_examples.concurrent_stacks Require Import spec.
-
 Set Default Proof Using "Type".
 
-(** Stack 3: No helping, view-shift spec. *)
-
-Definition mk_stack : val :=
-  λ: "_",
-  let: "r" := ref NONEV in
-  (rec: "pop" "n" :=
-       (match: !"r" with
-          NONE => NONE
-        | SOME "hd" =>
-          if: CAS "r" (SOME "hd") (Snd !"hd")
-          then SOME (Fst !"hd")
-          else "pop" "n"
-        end),
-    rec: "push" "n" :=
-        let: "r'" := !"r" in
-        let: "r''" := SOME (Alloc ("n", "r'")) in
-        if: CAS "r" "r'" "r''"
-        then #()
-        else "push" "n").
+Definition mk_stack : val := λ: "_", ref NONEV.
+Definition push : val :=
+  rec: "push" "s" "v" :=
+    let: "tail" := ! "s" in
+    let: "new" := SOME (ref ("v", "tail")) in
+    if: CAS "s" "tail" "new" then #() else "push" "s" "v".
+Definition pop : val :=
+  rec: "pop" "s" :=
+    match: !"s" with
+      NONE => NONEV
+    | SOME "l" =>
+      let: "pair" := !"l" in
+      if: CAS "s" (SOME "l") (Snd "pair")
+      then SOME (Fst "pair")
+      else "pop" "s"
+    end.
 
 Section stack_works.
-  Context `{!heapG Σ}.
+  Context `{!heapG Σ} (N : namespace).
   Implicit Types l : loc.
 
-  Fixpoint is_stack xs v : iProp Σ :=
+  Local Notation "l ↦{-} v" := (∃ q, l ↦{q} v)%I
+    (at level 20, format "l  ↦{-}  v") : bi_scope.
+
+  Lemma partial_mapsto_duplicable l v :
+    l ↦{-} v -∗ l ↦{-} v ∗ l ↦{-} v.
+  Proof.
+    iIntros "H"; iDestruct "H" as (?) "[Hl Hl']"; iSplitL "Hl"; eauto.
+  Qed.
+
+  Lemma partial_mapsto_agree l v1 v2 :
+    l ↦{-} v1 -∗ l ↦{-} v2 -∗ ⌜v1 = v2⌝.
+  Proof.
+    iIntros "H1 H2".
+    iDestruct "H1" as (?) "H1".
+    iDestruct "H2" as (?) "H2".
+    iApply (mapsto_agree with "H1 H2").
+  Qed.
+
+  Fixpoint is_list xs v : iProp Σ :=
     (match xs with
      | [] => ⌜v = NONEV⌝
-     | x :: xs => ∃ q (l : loc) (t : val), ⌜v = SOMEV #l ⌝ ∗ l ↦{q} (x, t) ∗ is_stack xs t
+     | x :: xs => ∃ l (t : val), ⌜v = SOMEV #l%V⌝ ∗ l ↦{-} (x, t)%V ∗ is_list xs t
      end)%I.
 
-  Definition stack_inv P v :=
-    (∃ l v' xs, ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack xs v' ∗ P xs)%I.
-
-  Lemma is_stack_disj xs v :
-      is_stack xs v -∗ is_stack xs v ∗ (⌜v = NONEV⌝ ∨ ∃ q (l : loc) (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{q} (h, t)).
+  Lemma is_list_disj xs v :
+    is_list xs v -∗ is_list xs v ∗ (⌜v = NONEV⌝ ∨ ∃ l (h t : val), ⌜v = SOMEV #l⌝ ∗ l ↦{-} (h, t)%V).
   Proof.
-    iIntros "Hstack".
-    destruct xs.
-    - iSplit; try iLeft; auto.
-    - simpl. iDestruct "Hstack" as (q l t) "[-> [[Hl Hl'] Hstack]]".
-      iSplitR "Hl"; eauto 10 with iFrame.
+    destruct xs; auto.
+    iIntros "H"; iDestruct "H" as (l t) "(-> & Hl & Hstack)".
+    iDestruct (partial_mapsto_duplicable with "Hl") as "[Hl1 Hl2]".
+    iSplitR "Hl2"; first by (iExists _, _; iFrame). iRight; auto.
   Qed.
-  Lemma is_stack_unboxed xs v :
-    is_stack xs v -∗ ⌜val_is_unboxed v⌝.
+
+  Lemma is_list_unboxed xs v :
+      is_list xs v -∗ ⌜val_is_unboxed v⌝ ∗ is_list xs v.
   Proof.
-    iIntros "Hstack". iDestruct (is_stack_disj with "Hstack") as "[_ [->|Hdisj]]".
-    - done.
-    - iDestruct "Hdisj" as (???? ->) "_". done.
+    iIntros "Hlist"; iDestruct (is_list_disj with "Hlist") as "[$ Heq]".
+    iDestruct "Heq" as "[-> | H]"; first done; by iDestruct "H" as (? ? ?) "[-> ?]".
   Qed.
 
-  Lemma is_stack_uniq : ∀ xs ys v,
-      is_stack xs v ∗ is_stack ys v -∗ ⌜xs = ys⌝.
+  Lemma is_list_empty xs :
+    is_list xs (InjLV #()) -∗ ⌜xs = []⌝.
   Proof.
-    induction xs, ys; iIntros (v') "[Hstack1 Hstack2]"; auto.
-    - iDestruct "Hstack1" as "%".
-      iDestruct "Hstack2" as (???) "[% _]".
-      subst.
-      discriminate.
-    - iDestruct "Hstack2" as "%".
-      iDestruct "Hstack1" as (???) "[% _]".
-      subst.
-      discriminate.
-    - simpl. iDestruct "Hstack1" as (q1 l1 t) "[% [Hl1 Hstack1]]".
-      iDestruct "Hstack2" as (q2 l2 t') "[% [Hl2 Hstack2]]".
-      subst; injection H0; intros; subst; clear H0.
-      iDestruct (mapsto_agree with "Hl1 Hl2") as %[= -> ->].
-      iDestruct (IHxs with "[Hstack1 Hstack2]") as "%". by iFrame.
-      subst; auto.
+    destruct xs; iIntros "Hstack"; auto.
+    iDestruct "Hstack" as (? ?) "(% & H)"; discriminate.
   Qed.
 
-  Lemma is_stack_empty : ∀ xs,
-      is_stack xs NONEV -∗ ⌜xs = []⌝.
+  Lemma is_list_cons xs l h t :
+    l ↦{-} (h, t)%V -∗
+    is_list xs (InjRV #l) -∗
+    ∃ ys, ⌜xs = h :: ys⌝.
   Proof.
-    iIntros (xs) "Hstack".
-    destruct xs; auto.
-    iDestruct "Hstack" as (?? t) "[% rest]".
-    discriminate.
+    destruct xs; first by iIntros "? %".
+    iIntros "Hl Hstack"; iDestruct "Hstack" as (l' t') "(% & Hl' & Hrest)"; simplify_eq.
+    iDestruct (partial_mapsto_agree with "Hl Hl'") as "%"; simplify_eq; iExists _; auto.
   Qed.
-  Lemma is_stack_cons : ∀ xs l,
-      is_stack xs (SOMEV #l) -∗
-               is_stack xs (SOMEV #l) ∗ ∃ q h t ys, ⌜xs = h :: ys⌝ ∗ l ↦{q} (h, t).
+
+  Definition stack_inv P l :=
+    (∃ v xs, l ↦ v ∗ is_list xs v ∗ P xs)%I.
+
+  Definition is_stack P v :=
+    (∃ l, ⌜v = #l⌝ ∗ inv N (stack_inv P l))%I.
+
+  Theorem mk_stack_works P :
+    {{{ P [] }}} mk_stack #() {{{ v, RET v; is_stack P v }}}.
   Proof.
-    iIntros ([|x xs] l) "Hstack".
-    - iDestruct "Hstack" as "%"; discriminate.
-    - simpl. iDestruct "Hstack" as (q l' t') "[% [[Hl Hl'] Hstack]]".
-      injection H; intros; subst; clear H.
-      iSplitR "Hl'"; eauto 10 with iFrame.
+    iIntros (Φ) "HP HΦ".
+    rewrite -wp_fupd.
+    wp_let. wp_alloc l as "Hl".
+    iMod (inv_alloc N _ (stack_inv P l) with "[Hl HP]") as "#Hinv".
+    { by iNext; iExists _, []; iFrame. }
+    iModIntro; iApply "HΦ"; iExists _; auto.
   Qed.
 
-  (* Whole-stack invariant (P). However:
-     - The resources for the successful and failing pop must be disjoint.
-       Instead, there should be a normal conjunction between them.
-     Open question: How does this relate to a logically atomic spec? *)
-  Theorem stack_works ι P Q Q' Q'' (Φ : val → iProp Σ) :
-    ▷ (∀ (f₁ f₂ : val),
-        (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) ∧ (* pop *)
-            (P [] ={⊤∖↑ι}=∗ Q' ∗ P []) -∗
-            WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}}))
-         -∗ (∀ (v : val), (* push *)
-               □ ((∀ vs, P vs ={⊤∖↑ι}=∗ P (v :: vs) ∗ Q'') -∗
-                  WP f₂ v {{ v, Q'' }}))
-         -∗ Φ (f₁, f₂)%V)%I
-    -∗ P []
-    -∗ WP mk_stack #()  {{ Φ }}.
+  Theorem push_works P s v Ψ :
+    {{{ is_stack P s ∗ ∀ xs, P xs ={⊤ ∖ ↑ N}=∗ P (v :: xs) ∗ Ψ #()}}}
+      push s v
+    {{{ RET #(); Ψ #() }}}.
   Proof.
-    iIntros "HΦ HP".
-    rename ι into N.
-    wp_rec.
-    wp_alloc l as "Hl".
-    iMod (inv_alloc N _ (stack_inv P #l) with "[Hl HP]") as "#Istack".
-    { iNext; iExists l, (InjLV #()), []; iSplit; iFrame; auto. }
-    wp_pures.
+    iIntros (Φ) "[Hstack Hupd] HΦ". iDestruct "Hstack" as (l) "[-> #Hinv]".
+    iLöb as "IH".
+    wp_lam. wp_lam. wp_bind (Load _).
+    iInv N as (list xs) "(Hl & Hlist & HP)" "Hclose".
+    wp_load.
+    iMod ("Hclose" with "[Hl Hlist HP]") as "_".
+    { iNext; iExists _, _; iFrame. }