Merge branch 'logatom_stack' into 'master'

Logically atomic stack

See merge request FP/iris-examples!9

Makefile.coq.local

@@ -19,3 +19,6 @@ logrel: $(filter theories/logrel/%,$(VOFILES))
 
 hocap: $(filter theories/hocap/%,$(VOFILES))
 .PHONY: hocap
+
+logatom_stack: $(filter theories/logatom_stack/%,$(VOFILES))
+.PHONY: logrel

_CoqProject

@@ -80,3 +80,7 @@ theories/hocap/contrib_bag.v
 theories/hocap/lib/oneshot.v
 theories/hocap/concurrent_runners.v
 theories/hocap/parfib.v
+
+theories/logatom_stack/stack.v
+theories/logatom_stack/spec.v
+theories/logatom_stack/hocap_spec.v

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2018-07-13.0.cbf73155") | (= "dev") }
+  "coq-iris" { (= "dev.2018-07-13.2.af5611c8") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/logatom_stack/hocap_spec.v

+From stdpp Require Import namespaces.
+From iris.algebra Require Import excl auth list.
+From iris.heap_lang Require Export lifting notation.
+From iris.base_logic.lib Require Import invariants.
+From iris.program_logic Require Import atomic.
+From iris.heap_lang Require Import proofmode atomic_heap.
+From iris_examples.logatom_stack Require spec.
+Set Default Proof Using "Type".
+
+Module logatom := logatom_stack.spec.
+
+(** A general HoCAP-style interface for a stack, modeled after the spec in
+[hocap/abstract_bag.v].  There are two differences:
+- We split [bag_contents] into an authoritative part and a fragment as this
+  slightly strnegthens the spec: The logically atomic spec only requires
+  [stack_content ∗ stack_content] to derive a contradiction, the abstract bag
+  spec requires to get *three* pieces which is only possible when actually
+  calling a bag operation.
+- We also slightly weaken the spec by adding [make_laterable], which is needed
+  because logical atomicity can only capture laterable resources, which is
+  needed when implementing e.g. the elimination stack on top of an abstract
+  logically atomic heap. *)
+Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
+  (* -- operations -- *)
+  new_stack : val;
+  push : val;
+  pop : val;
+  (* -- other data -- *)
+  name : Type;
+  (* -- predicates -- *)
+  is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
+  stack_content_frag (γs : name) (l : list val) : iProp Σ;
+  stack_content_auth (γs : name) (l : list val) : iProp Σ;
+  (* -- predicate properties -- *)
+  is_stack_persistent N γs v : Persistent (is_stack N γs v);
+  stack_content_frag_timeless γs l : Timeless (stack_content_frag γs l);
+  stack_content_auth_timeless γs l : Timeless (stack_content_auth γs l);
+  stack_content_frag_exclusive γs l1 l2 :
+    stack_content_frag γs l1 -∗ stack_content_frag γs l2 -∗ False;
+  stack_content_auth_exclusive γs l1 l2 :
+    stack_content_auth γs l1 -∗ stack_content_auth γs l2 -∗ False;
+  stack_content_agree γs l1 l2 :
+    stack_content_frag γs l1 -∗ stack_content_auth γs l2 -∗ ⌜l1 = l2⌝;
+  stack_content_update γs l l' :
+    stack_content_frag γs l -∗
+    stack_content_auth γs l -∗
+    |==> stack_content_frag γs l' ∗ stack_content_auth γs l';
+  (* -- operation specs -- *)
+  new_stack_spec N :
+    {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content_frag γs [] }}};
+  push_spec N γs s e v (Φ : val → iProp Σ) :
+    IntoVal e v →
+    is_stack N γs s -∗
+    make_laterable (∀ l, stack_content_auth γs l ={⊤∖↑N}=∗ stack_content_auth γs (v::l) ∗ Φ #()) -∗
+    WP push (s, e) {{ Φ }};
+  pop_spec N γs s (Φ : val → iProp Σ) :
+    is_stack N γs s -∗
+    make_laterable (∀ l, stack_content_auth γs l ={⊤∖↑N}=∗
+          match l with [] => stack_content_auth γs [] ∗ Φ NONEV
+                | v :: l' => stack_content_auth γs l' ∗ Φ (SOMEV v) end) -∗
+    WP pop s {{ Φ }};
+}.
+Arguments hocap_stack _ {_}.
+
+Existing Instance is_stack_persistent.
+Existing Instance stack_content_frag_timeless.
+Existing Instance stack_content_auth_timeless.
+
+(** Show that our way of writing the [pop_spec] is equivalent to what is done in
+[concurrent_stack.spec].  IOW, the conjunction-vs-match doesn't matter.  Fixing
+the postcondition (the [Q] in [concurrent_stack.spec]) still matters. *)
+Section pop_equiv.
+  Context `{invG Σ} (T : Type).
+
+  Lemma pop_equiv E (I : list T → iProp Σ) (Φemp : iProp Σ) (Φret : T → iProp Σ) :
+    (∀ l, I l ={E}=∗
+       match l with [] => I [] ∗ Φemp | v :: l' => I l' ∗ Φret v end)
+    ⊣⊢
+    (∀ v vs, I (v :: vs) ={E}=∗ Φret v ∗ I vs)
+    ∧ (I [] ={E}=∗ Φemp ∗ I []).
+  Proof.
+    iSplit.
+    - iIntros "HΦ". iSplit.
+      + iIntros (??) "HI". iMod ("HΦ" with "HI") as "[$ $]". done.
+      + iIntros "HI". iMod ("HΦ" with "HI") as "[$ $]". done.
+    - iIntros "HΦ" (l) "HI". destruct l; rewrite [(I _ ∗ _)%I]bi.sep_comm; by iApply "HΦ".
+  Qed.
+End pop_equiv.
+
+(** From a HoCAP stack we can directly implement the logically atomic
+interface. *)
+Section hocap_logatom.
+  Context `{!heapG Σ} (stack: hocap_stack Σ).
+
+  Lemma logatom_push N γs s e v :
+    IntoVal e v →
+    stack.(is_stack) N γs s -∗
+    <<< ∀ l : list val, stack.(stack_content_frag) γs l >>>
+      stack.(push) (s, e) @ ⊤∖↑N
+    <<< stack.(stack_content_frag) γs (v::l), RET #() >>>.
+  Proof.
+    iIntros (?) "Hstack". iApply wp_atomic_intro. iIntros (Φ) "HΦ".
+    iApply (push_spec with "Hstack").
+    iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
+    iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
+    iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
+    iMod (stack_content_update with "Hfrag Hauth") as "[Hfrag $]".
+    iMod ("Hclose" with "Hfrag") as "HΦ". done.
+  Qed.
+
+  Lemma logatom_pop N γs (s : val) :
+    stack.(is_stack) N γs s -∗
+    <<< ∀ l : list val, stack.(stack_content_frag) γs l >>>
+      stack.(pop) s @ ⊤∖↑N
+    <<< stack.(stack_content_frag) γs (tail l),
+        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
+  Proof.
+    iIntros "Hstack". iApply wp_atomic_intro. iIntros (Φ) "HΦ".
+    iApply (pop_spec with "Hstack").
+    iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
+    iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
+    iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
+    destruct l;
+    iMod (stack_content_update with "Hfrag Hauth") as "[Hfrag $]";
+    iMod ("Hclose" with "Hfrag") as "HΦ"; done.
+  Qed.
+
+  Definition hocap_logatom : logatom.atomic_stack Σ :=
+    {| logatom.new_stack_spec := stack.(new_stack_spec);
+       logatom.push_spec := logatom_push;
+       logatom.pop_spec := logatom_pop;
+       logatom.stack_content_exclusive := stack.(stack_content_frag_exclusive) |}.
+
+End hocap_logatom.
+
+(** From a logically atomic stack, we can implement a HoCAP stack by adding an
+auth invariant. *)
+
+(** The CMRA & functor we need. *)
+Class hocapG Σ := HocapG {
+  hocap_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
+}.
+Definition hocapΣ : gFunctors :=
+  #[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
+
+Instance subG_hocapΣ {Σ} : subG hocapΣ Σ → hocapG Σ.
+Proof. solve_inG. Qed.
+
+Section logatom_hocap.
+  Context `{!heapG Σ} `{!hocapG Σ} (stack: logatom.atomic_stack Σ).
+
+  Definition hocap_name : Type := stack.(logatom.name) * gname.
+  Implicit Types γs : hocap_name.
+
+  Definition hocap_stack_content_auth γs l : iProp Σ := own γs.2 (● Excl' l).
+  Definition hocap_stack_content_frag γs l : iProp Σ := own γs.2 (◯ Excl' l).
+
+  Definition hocap_is_stack N γs v : iProp Σ :=
+    (stack.(logatom.is_stack) (N .@ "stack") γs.1 v ∗
+     inv (N .@ "wrapper") (∃ l, stack.(logatom.stack_content) γs.1 l ∗ hocap_stack_content_auth γs l))%I.
+
+  Lemma hocap_new_stack N :
+    {{{ True }}}
+      stack.(logatom.new_stack) #()
+    {{{ γs s, RET s; hocap_is_stack N γs s ∗ hocap_stack_content_frag γs [] }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". iApply wp_fupd. iApply logatom.new_stack_spec; first done.
+    iIntros "!>" (γs s) "[Hstack Hcont]".
+    iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γw) "[Hs● Hs◯]".
+    { apply auth_valid_discrete_2. split; done. }
+    iApply ("HΦ" $! (γs, γw)). rewrite /hocap_is_stack. iFrame.
+    iApply inv_alloc. eauto with iFrame.
+  Qed.
+
+  Lemma hocap_push N γs s e v (Φ : val → iProp Σ) :
+    IntoVal e v →
+    hocap_is_stack N γs s -∗
+    make_laterable (∀ l, hocap_stack_content_auth γs l ={⊤∖↑N}=∗ hocap_stack_content_auth γs (v::l) ∗ Φ #()) -∗
+    WP stack.(logatom.push) (s, e) {{ Φ }}.
+  Proof using Type*.
+    iIntros (?) "#[Hstack Hwrap] Hupd". iApply (logatom.push_spec with "Hstack"); first iAccu.
+    iAuIntro. iInv "Hwrap" as (l) "[>Hcont >H●]".
+    iAaccIntro with "Hcont"; first by eauto 10 with iFrame.
+    iIntros "Hcont".
+    iMod fupd_intro_mask' as "Hclose";
+      last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
+    iMod "Hclose" as "_". iIntros "!>".
+    eauto with iFrame.
+  Qed.
+
+  Lemma hocap_pop N γs s (Φ : val → iProp Σ) :
+    hocap_is_stack N γs s -∗
+    make_laterable (∀ l, hocap_stack_content_auth γs l ={⊤∖↑N}=∗
+          match l with [] => hocap_stack_content_auth γs [] ∗ Φ NONEV
+                | v :: l' => hocap_stack_content_auth γs l' ∗ Φ (SOMEV v) end) -∗
+    WP stack.(logatom.pop) s {{ Φ }}.
+  Proof using Type*.
+    iIntros "#[Hstack Hwrap] Hupd". iApply (logatom.pop_spec with "Hstack"); first iAccu.
+    iAuIntro. iInv "Hwrap" as (l) "[>Hcont >H●]".
+    iAaccIntro with "Hcont"; first by eauto 10 with iFrame.
+    iIntros "Hcont". destruct l.
+    - iMod fupd_intro_mask' as "Hclose";
+        last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
+       iMod "Hclose" as "_". iIntros "!>"; eauto with iFrame.
+    - iMod fupd_intro_mask' as "Hclose";
+        last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
+       iMod "Hclose" as "_". iIntros "!>"; eauto with iFrame.
+  Qed.
+
+  Program Definition logatom_hocap : hocap_stack Σ :=
+    {| new_stack_spec := hocap_new_stack;
+       push_spec := hocap_push;
+       pop_spec := hocap_pop |}.
+  Next Obligation.
+    iIntros (???) "Hf1 Hf2". iDestruct (own_valid_2 with "Hf1 Hf2") as %[].
+  Qed.
+  Next Obligation.
+    iIntros (???) "Ha1 Ha2". iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
+  Qed.
+  Next Obligation.
+    iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
+      %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. done.
+  Qed.
+  Next Obligation.
+    iIntros (???) "Hf Ha". iMod (own_update_2 with "Ha Hf") as "[? ?]".
+    { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
+    by iFrame.
+  Qed.
+
+End logatom_hocap.

theories/logatom_stack/spec.v

+From stdpp Require Import namespaces.
+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+Set Default Proof Using "Type".
+
+(** A general logically atomic interface for a stack. *)
+Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
+  (* -- operations -- *)
+  new_stack : val;
+  push : val;
+  pop : val;
+  (* -- other data -- *)
+  name : Type;
+  (* -- predicates -- *)
+  is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
+  stack_content (γs : name) (l : list val) : iProp Σ;
+  (* -- predicate properties -- *)
+  is_stack_persistent N γs v : Persistent (is_stack N γs v);
+  stack_content_timeless γs l : Timeless (stack_content γs l);
+  stack_content_exclusive γs l1 l2 :
+    stack_content γs l1 -∗ stack_content γs l2 -∗ False;
+  (* -- operation specs -- *)
+  new_stack_spec N :
+    {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s ∗ stack_content γs [] }}};
+  push_spec N γs s e v :
+    IntoVal e v →
+    is_stack N γs s -∗
+    <<< ∀ l : list val, stack_content γs l >>>
+      push (s, e) @ ⊤∖↑N
+    <<< stack_content γs (v::l), RET #() >>>;
+  pop_spec N γs s :
+    is_stack N γs s -∗
+    <<< ∀ l : list val, stack_content γs l >>>
+      pop s @ ⊤∖↑N
+    <<< stack_content γs (tail l),
+        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>;
+}.
+Arguments atomic_stack _ {_}.
+
+Existing Instance is_stack_persistent.
+Existing Instance stack_content_timeless.

theories/logatom_stack/stack.v

+From iris.algebra Require Import excl auth list.
+From iris.base_logic.lib Require Import invariants.
+From iris.program_logic Require Import atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode atomic_heap.
+From iris.bi.lib Require Import fractional.
+From iris_examples.logatom_stack Require Import spec.
+Set Default Proof Using "Type".
+
+(** * Implement a concurrent stack with helping on top of an arbitrary atomic
+heap. *)
+
+(** The CMRA & functor we need. *)
+(* Not bundling heapG, as it may be shared with other users. *)
+Class stackG Σ := StackG {
+  stack_tokG :> inG Σ (exclR unitC);
+  stack_stateG :> inG Σ (authR (optionUR $ exclR (listC valC)));
+ }.
+Definition stackΣ : gFunctors :=
+  #[GFunctor (exclR unitC); GFunctor (authR (optionUR $ exclR (listC valC)))].
+
+Instance subG_stackΣ {Σ} : subG stackΣ Σ → stackG Σ.
+Proof. solve_inG. Qed.
+
+Section stack.
+  Context `{!heapG Σ, stackG Σ} {aheap: atomic_heap Σ} (N : namespace).
+  Notation iProp := (iProp Σ).
+
+  Let offerN := N .@ "offer".
+  Let stackN := N .@ "stack".
+
+  Import atomic_heap.notation.
+
+  (** Code. A stack is a pair of two pointers-to-option-pointers, one for the
+  head element (if the stack is non-empty) and for the current offer (if it
+  exists).  A stack element is a pair of a value an an optional pointer to the
+  next element. *)
+  Definition new_stack : val :=
+    λ: <>,
+      let: "head" := ref NONE in
+      let: "offer" := ref NONE in
+      ("head", "offer").
+
+  Definition push : val :=
+    rec: "push" "args" :=
+      let: "stack" := Fst "args" in
+      let: "val" := Snd "args" in
+      let: "head_old" := !(Fst "stack") in
+      let: "head_new" := ref ("val", "head_old") in
+      if: CAS (Fst "stack") "head_old" (SOME "head_new") then #() else
+      (* the CAS failed due to a race, let's try an offer on the side-channel *)
+      let: "state" := ref #0 in
+      let: "offer" := ("val", "state") in
+      (Snd "stack") <- SOME "offer" ;;
+      (* wait to see if anyone takes it *)
+      (* okay, enough waiting *)
+      (Snd "stack") <- NONE ;;
+      if: CAS "state" #0 #2 then
+        (* We retracted the offer. Just try the entire thing again. *)
+        "push" "args"
+      else
+        (* Someone took the offer. We are done. *)
+        #().
+
+  Definition pop : val :=
+    rec: "pop" "stack" :=
+      match: !(Fst "stack") with
+        NONE => NONE (* stack empty *)
+      | SOME "head_old" =>
+        let: "head_old_data" := !"head_old" in
+        (* See if we can change the master head pointer *)
+        if: CAS (Fst "stack") (SOME "head_old") (Snd "head_old_data") then
+          (* That worked! We are done. Return the value. *)
+          SOME (Fst "head_old_data")
+        else
+          (* See if there is an offer on the side-channel *)
+          match: !(Snd "stack") with
+            NONE =>
+            (* Nope, no offer. Just try again. *)
+            "pop" "stack"
+          | SOME "offer" =>
+            (* Try to accept the offer. *)
+            if: CAS (Snd "offer") #0 #1 then
+              (* Success! We are done. Return the offered value. *)
+              SOME (Fst "offer")
+            else
+              (* Someone else was faster. Just try again. *)
+              "pop" "stack"
+          end
+      end.
+
+  (** Invariant and protocol. *)
+  Definition stack_content (γs : gname) (l : list val) : iProp :=
+    (own γs (◯ Excl' l))%I.
+  Global Instance stack_content_timeless γs l : Timeless (stack_content γs l) := _.
+
+  Lemma stack_content_exclusive γs l1 l2 :
+    stack_content γs l1 -∗ stack_content γs l2 -∗ False.
+  Proof.
+    iIntros "Hl1 Hl2". iDestruct (own_valid_2 with "Hl1 Hl2") as %[].
+  Qed.
+
+  Definition stack_elem_to_val (stack_rep : option loc) : val :=
+    match stack_rep with
+    | None => NONEV
+    | Some l => SOMEV #l
+    end.
+  Local Instance stack_elem_to_val_inj : Inj (=) (=) stack_elem_to_val.
+  Proof. rewrite /Inj /stack_elem_to_val=>??. repeat case_match; congruence. Qed.
+
+  Fixpoint list_inv (l : list val) (rep : option loc) : iProp :=
+    match l with
+    | nil => ⌜rep = None⌝
+    | v::l => ∃ (ℓ : loc) q (rep' : option loc), ⌜rep = Some ℓ⌝ ∗
+                              ℓ ↦{q} (v, stack_elem_to_val rep') ∗ list_inv l rep'
+    end%I.
+
+  Local Hint Extern 0 (environments.envs_entails _ (list_inv (_::_) _)) => simpl.
+
+  Inductive offer_state := OfferPending | OfferRevoked | OfferAccepted | OfferAcked.
+
+  Local Instance: Inhabited offer_state := populate OfferPending.
+
+  Definition offer_state_rep (st : offer_state) : Z :=
+    match st with
+    | OfferPending => 0
+    | OfferRevoked => 2
+    | OfferAccepted => 1
+    | OfferAcked => 1
+    end.
+
+  Definition offer_inv (st_loc : loc) (γo : gname) (P Q : iProp) : iProp :=
+    (∃ st : offer_state, st_loc ↦ #(offer_state_rep st) ∗
+      match st with
+      | OfferPending => P
+      | OfferAccepted => Q
+      | _ => own γo (Excl ())
+      end)%I.
+
+  Local Hint Extern 0 (environments.envs_entails _ (offer_inv _ _ _ _)) => unfold offer_inv.
+
+  Definition is_offer (γs : gname) (offer_rep : option (val * loc)) :=
+    match offer_rep with
+    | None => True
+    | Some (v, st_loc) =>
+      ∃ P Q γo, inv offerN (offer_inv st_loc γo P Q) ∗
+                (* The persistent part of the Laterable AU *)
+                □ (▷ P -∗ ◇ AU << ∀ l, stack_content γs l >> @ ⊤∖↑N, ∅
+                               << stack_content γs (v::l), COMM Q >>)
+    end%I.
+
+  Local Instance is_offer_persistent γs offer_rep : Persistent (is_offer γs offer_rep).
+  Proof. destruct offer_rep as [[??]|]; apply _. Qed.
+
+  Definition offer_to_val (offer_rep : option (val * loc)) : val :=
+    match offer_rep with
+    | None => NONEV
+    | Some (v, l) => SOMEV (v, #l)
+    end.
+
+  Definition stack_inv (γs : gname) (head : loc) (offer : loc) : iProp :=
+    (∃ stack_rep offer_rep l, own γs (● Excl' l) ∗
+       head ↦ stack_elem_to_val stack_rep ∗ list_inv l stack_rep ∗
+       offer ↦ offer_to_val offer_rep ∗ is_offer γs offer_rep)%I.
+
+  Local Hint Extern 0 (environments.envs_entails _ (stack_inv _ _ _)) => unfold stack_inv.
+
+  Definition is_stack (γs : gname) (s : val) : iProp :=
+    (∃ head offer : loc, ⌜s = (#head, #offer)%V⌝ ∗ inv stackN (stack_inv γs head offer))%I.
+  Global Instance is_stack_persistent γs s : Persistent (is_stack γs s) := _.
+
+  (** Proofs. *)
+  Lemma new_stack_spec :
+    {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack γs s ∗ stack_content γs [] }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam.
+    wp_apply alloc_spec; first done. iIntros (head) "Hhead". wp_let.
+    wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
+    iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γs) "[Hs● Hs◯]".
+    { apply auth_valid_discrete_2. split; done. }
+    iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
+    { iNext. iExists None, None, _. iFrame. done. }
+    iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
+  Qed.
+
+  Lemma push_spec γs s e v :
+    IntoVal e v →
+    is_stack γs s -∗
+    <<< ∀ l : list val, stack_content γs l >>>
+      push (s, e) @ ⊤∖↑N
+    <<< stack_content γs (v::l), RET #() >>>.
+  Proof.
+    iIntros (<-) "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "AU".
+    iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s.
+    iLöb as "IH".
+    wp_let. wp_proj. wp_let. wp_proj. wp_let. wp_proj.
+    (* Load the old head. *)
+    wp_apply (load_spec with "[AU]"); first by iAccu.
+    iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hrem)".
+    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
+    iIntros "?". iSplitL; first by eauto 10 with iFrame.
+    iIntros "!> AU". clear offer_rep l.
+    (* Go on. *)
+    wp_let. wp_apply alloc_spec; first done. iIntros (head_new) "Hhead_new".
+    wp_let. wp_proj.
+    (* CAS to change the head. *)
+    wp_apply cas_spec; [by destruct stack_rep|iAccu|].
+    iAuIntro. iInv stackN as (stack_rep' offer_rep l) "(>Hs● & >H↦ & Hlist & Hoffer)".
+    iAaccIntro with "H↦"; first by eauto 10 with iFrame.
+    iIntros "H↦".
+    destruct (decide (stack_elem_to_val stack_rep' = stack_elem_to_val stack_rep)) as
+      [->%stack_elem_to_val_inj|_].
+    - (* The CAS succeeded. Update everything accordingly. *)
+      iMod "AU" as (l') "[Hl' [_ Hclose]]".
+      iDestruct (own_valid_2 with "Hs● Hl'") as
+        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+      iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
+      { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
+      iMod ("Hclose" with "Hl'") as "HΦ". iModIntro.
+      change (InjRV #head_new) with (stack_elem_to_val (Some head_new)).
+      iSplitR "HΦ"; first by eauto 12 with iFrame.
+      iIntros "_". wp_if. by iApply "HΦ".
+    - (* The CAS failed, go on making an offer. *)
+      iModIntro. iSplitR "AU"; first by eauto 8 with iFrame.
+      clear stack_rep stack_rep' offer_rep l head_new.
+      iIntros "H". wp_if.
+      wp_apply alloc_spec; first done. iIntros (st_loc) "Hoffer_st".
+      wp_let. wp_let. wp_proj.
+      (* Make the offer *)
+      wp_apply store_spec; first by iAccu.
+      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
+      iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.
+      iMod (own_alloc (Excl ())) as (γo) "Htok"; first done.
+      iDestruct (laterable with "AU") as (AU_later) "[AU #AU_back]".
+      iMod (inv_alloc offerN _ (offer_inv st_loc γo AU_later _)  with "[AU Hoffer_st]") as "#Hoinv".
+      { iNext. iExists OfferPending. iFrame. }
+      iIntros "?". iSplitR "Htok".
+      { iClear "Hoffer". iExists _, (Some (v, st_loc)), _. iFrame.
+        rewrite /is_offer /=. iExists _, _, _. iFrame "AU_back Hoinv". done. }
+      clear stack_rep offer_rep l.
+      iIntros "!> _". wp_let.
+      (* Retract the offer. *)
+      wp_proj. wp_apply store_spec; first by iAccu.
+      iAuIntro. iInv stackN as (stack_rep offer_rep l) "(Hs● & >H↦ & Hlist & >Hoffer↦ & Hoffer)".
+      iAaccIntro with "Hoffer↦"; first by eauto 10 with iFrame.