Make the helping stack proof abstract in the offers specs (almost?)

_CoqProject

@@ -59,7 +59,7 @@ theories/examples/coinflip.v
 
 theories/examples/par.v
 
-theories/experimental/helping/mailbox.v
+theories/experimental/helping/offers.v
 theories/experimental/helping/helping_stack.v
 
 theories/experimental/hocap/counter.v

theories/experimental/helping/helping_stack.v

@@ -8,7 +8,7 @@ of this code was written togethe witr Amin Timany around 2017 *)
 
 From iris.algebra Require Import auth gmap agree list excl.
 From iris.base_logic.lib Require Import auth.
-From reloc Require Export reloc experimental.helping.mailbox.
+From reloc Require Export reloc experimental.helping.offers.
 From reloc Require Import examples.stack.CG_stack lib.list.
 
 (** * Source code *)
@@ -65,12 +65,13 @@ Definition CG_mkstack : val := λ: <>,
 (** * Algebras needed for the refinement *)
 Canonical Structure ectx_itemO := leibnizO ectx_item.
 
-(** An offer registry associates with each offer (loc), a value that is being offered, and a potential thread (gname, nat, ectx) that accepts the offer, if it is present. *)
+(** An offer registry associates with each offer (loc), a value that
+is being offered, and a potential thread (gname, nat, ectx) that
+accepts the offer, if it is present. *)
 Definition offerReg := gmap loc (val * gname * nat * (list ectx_item)).
 
 Definition offerRegR :=
-  gmapUR loc
-         (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))).
+  gmapUR loc (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))).
 
 Class offerRegPreG Σ := OfferRegPreG {
   offerReg_inG :> authG Σ offerRegR
@@ -93,7 +94,7 @@ Qed.
 
 (** * Refinement proof *)
 Section refinement.
-  Context `{!relocG Σ, !offerRegPreG Σ, !channelG Σ}.
+  Context `{!relocG Σ, !offerRegPreG Σ, !offerG Σ}.
 
   Implicit Type A : lrel Σ.
 
@@ -111,8 +112,7 @@ Section refinement.
     iMod (own_update with "HN") as "[HN Hfrag]".
     { eapply auth_update_alloc.
       eapply (alloc_singleton_local_update _ o (to_agree (v, (γ, (j, K))))); try done.
-      by rewrite /to_offer_reg lookup_fmap HNo.
-    }
+      by rewrite /to_offer_reg lookup_fmap HNo. }
     iFrame.
     by rewrite /to_offer_reg fmap_insert.
   Qed.
@@ -186,91 +186,10 @@ Section refinement.
     by rewrite Hfoo.
   Qed.
 
-  (** ** The offer invariant *)
-  (* TODO: abstract away from the concrete representation of offers *)
-  Definition is_offer γ (l : loc) (P Q : iProp Σ) :=
-    (∃ (c : nat),
-       l ↦ #c ∗
-        (⌜c = 0⌝ ∗ P
-       ∨ ⌜c = 1⌝ ∗ (Q ∨ own γ (Excl ()))
-       ∨ ⌜c = 2⌝ ∗ own γ (Excl ()))%nat)%I.
-
-  Definition offer_token γ := own γ (Excl ()).
-
- (* this is kinda useless *)
-  Lemma mk_offer_l P Q K (v : val) t A :
-    P -∗
-    (∀ γ l, is_offer γ l P Q -∗ offer_token γ -∗ REL fill K (of_val (v, #l)) << t : A) -∗
-    REL fill K (mk_offer v) << t : A.
-  Proof.
-    iIntros "HP Hcont". rel_rec_l. rel_alloc_l l as "Hl".
-    iMod (own_alloc (Excl ())) as (γ) "Hγ". done.
-    rel_pures_l.
-    iApply ("Hcont" $! γ l with "[HP Hl] Hγ").
-    iExists 0. iFrame. iLeft. eauto.
-  Qed.
-
-  Lemma take_offer_l γ E (l : loc) v t A K P Q :
-    (|={⊤, E}=> ▷ is_offer γ l P Q ∗
-         ▷ ((is_offer γ l P Q -∗ REL fill K (of_val NONEV) << t @ E : A)
-            ∧ (P -∗ (Q -∗ is_offer γ l P Q) -∗ REL fill K (of_val $ SOMEV v) << t @ E : A))) -∗
-    REL fill K (take_offer (v, #l)%V) << t : A.
-  Proof.
-    iIntros "Hlog". rel_rec_l. rel_pures_l.
-    rel_cmpxchg_l_atomic.
-    iMod "Hlog" as "(Hoff & Hcont)".
-    rewrite {1}/is_offer. iDestruct "Hoff" as (c) "[Hl Hoff]".
-    iModIntro. iExists _. iFrame "Hl". iSplit.
-    - iIntros (?). iNext.
-      iDestruct "Hcont" as "[Hcont _]".
-      iIntros "Hl".
-      rel_pures_l. iApply ("Hcont" with "[-]").
-      iExists _; iFrame.
-    - iIntros (?). simplify_eq/=.
-      assert (c = 0%nat) as -> by lia. (* :) *)
-      iNext. iIntros "Hl".
-      iDestruct "Hoff" as "[[% HP] | [[% ?] | [% ?]]]"; [| congruence..].
-      rel_pures_l.
-      iDestruct "Hcont" as "[_ Hcont]".
-      iApply ("Hcont" with "HP [-]").
-      iIntros "HQ". rewrite /is_offer. iExists 1.
-      iFrame. iRight. iLeft. iSplit; eauto.
-  Qed.
-
-  Lemma wp_revoke_offer γ l E P Q (v : val) Φ :
-    offer_token γ -∗
-    ▷ (|={⊤, E}=> ▷ is_offer γ l P Q ∗
-        ▷ ((is_offer γ l P Q -∗ Q ={E, ⊤}=∗ Φ NONEV)
-           ∧ (is_offer γ l P Q -∗ P ={E, ⊤}=∗ Φ (SOMEV v)))) -∗
-    WP (revoke_offer (of_val (v, #l))) {{ Φ }}.
-  Proof.
-    iIntros "Hγ Hlog". wp_rec. wp_pures.
-    wp_bind (CmpXchg _ _ _). iApply wp_atomic.
-    iMod "Hlog" as "(Hoff & Hcont)".
-    rewrite {1}/is_offer. iDestruct "Hoff" as (c) "[Hl Hoff]".
-    iModIntro. iDestruct "Hoff" as "[(>-> & HP)|[(>-> & HQ) | (>-> & Htok)]]".
-    - wp_cmpxchg_suc; first fast_done.
-      iDestruct "Hcont" as "[_ Hcont]".
-      iMod ("Hcont" with "[-HP] HP") as "HΦ".
-      { iExists 2. iFrame "Hl". iRight. iRight. eauto. }
-      iModIntro. by wp_pures.
-    - wp_cmpxchg_fail; first done.
-      iDestruct "Hcont" as "[Hcont _]".
-      iDestruct "HQ" as "[HQ | Htok]"; last first.
-      { iDestruct (own_valid_2 with "Hγ Htok") as %Hbar.
-        inversion Hbar. }
-      iMod ("Hcont" with "[-HQ] HQ") as "HΦ".
-      { iExists 1. iFrame "Hl". iRight. iLeft. eauto. }
-      iModIntro. by wp_pures.
-    - wp_cmpxchg_fail; first done.
-      iDestruct (own_valid_2 with "Hγ Htok") as %Hbar.
-      inversion Hbar.
-  Qed.
-
   (* We have the revoke_offer symbolic execution rule specialized for helping *)
   Lemma revoke_offer_l γ off E K (v : val) e1 e2 A :
     offer_token γ -∗
-    off ↦ #0 -∗
+    (∀ j K', (j ⤇ fill K' e1) -∗ is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2)) -∗
     (∀ j K', is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2) ={E, ⊤, E}▷=∗
       ▷ is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2) ∗
       ▷ (is_offer γ off (j ⤇ fill K' e1) (j ⤇ fill K' e2) -∗
@@ -281,8 +200,8 @@ Section refinement.
     iIntros "Hγ Hoff Hlog".
     rewrite {3}refines_eq /refines_def.
     iIntros (j K') "#Hs Hj".
-    iMod ("Hlog" with "[Hoff Hj]") as "Hlog".
-    { iExists 0. iFrame "Hoff". iLeft. eauto. }
+    iSpecialize ("Hoff" with "Hj").
+    iMod ("Hlog" with "Hoff") as "Hlog".
     iModIntro. iApply wp_bind. (* TODO: why do we have to use wp_bind here? *)
     wp_apply (wp_revoke_offer with "Hγ [-]").
     iNext. iMod "Hlog" as "[Hoff Hcont]". iModIntro.
@@ -293,8 +212,6 @@ Section refinement.
       rewrite refines_eq. by iApply "Hcont".
   Qed.
 
-  Opaque is_offer mk_offer take_offer revoke_offer.
-
   Definition offerInv (N : offerReg) (st' : val) : iProp Σ :=
     ([∗ map] l ↦ w ∈ N,
      match w with
@@ -307,23 +224,17 @@ Section refinement.
     ⊢ offerInv ∅ st'.
   Proof. by rewrite /offerInv big_sepM_empty. Qed.
 
-  Lemma offerInv_excl (N : offerReg) (st' : val) (o : loc) (v : val) :
-    offerInv N st' -∗ o ↦ v -∗ ⌜N !! o = None⌝.
+  Lemma offerInv_excl (N : offerReg) (st' : val) (o : loc) γ P Q :
+    offerInv N st' -∗ is_offer γ o P Q -∗ ⌜N !! o = None⌝.
   Proof.
-    rewrite /offerInv.
-    iIntros "HN Ho".
+    rewrite /offerInv. iIntros "HN Ho".
     iAssert (⌜is_Some (N !! o)⌝ → False)%I as %Hbaz.
     {
       iIntros ([[[[? ?] ?] ?] HNo]).
       rewrite (big_sepM_lookup _ N o _ HNo).
-      Transparent is_offer.
-      iDestruct "HN" as (c) "[HNo ?]".
-      iDestruct (gen_heap.mapsto_valid_2 with "Ho HNo") as %Hfoo.
-      compute in Hfoo. contradiction.
-      Opaque is_offer.
+      iApply (is_offer_exclusive with "HN Ho").
     }
-    iPureIntro.
-    destruct (N !! o); eauto. exfalso. apply Hbaz; eauto.
+    iPureIntro. revert Hbaz. case: (N !! o)=> [av'|]; naive_solver.
   Qed.
 
   (** Linking two contents of the two stacks together. *)
@@ -579,11 +490,8 @@ Section refinement.
     iLöb as "IH".
     rel_rec_l.
     rel_pures_l.
-
-    Transparent mk_offer.
-
-    rel_rec_l. rel_pures_l.
-    rel_alloc_l off as "Hoff". rel_pures_l.
+    rel_apply_l mk_offer_l. iIntros (γ off) "Hoff Htok".
+    rel_pures_l.
     rel_store_l_atomic. (* we update the mailbox and store the offer in the registry *)
     iInv stackN as (s1 s2 N) "(Hl & Hst1 & Hst2 & Hrel & Hmb & HNown & HN)" "Hcl".
     iModIntro.
@@ -591,18 +499,18 @@ Section refinement.
     iAssert (∃ v, ▷ mb ↦ v)%I with "[Hmb]" as (v) "Hmb".
     { iDestruct "Hmb" as "[Hmb | Hmb]".
       - iExists NONEV; eauto.
-      - iDestruct "Hmb" as (l m1 m2 γ j K) "(Hm & Hmb & ?)".
+      - iDestruct "Hmb" as (l m1 m2 γ' j K) "(Hm & Hmb & ?)".
         iExists (SOMEV (m1, #l)); eauto. }
     iExists _; iFrame; iNext.
     iIntros "Hmb".
 
 
     rel_pures_l.
-    iDestruct (offerInv_excl with "HN Hoff") as %Hbaz.
-    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+    rel_apply_l (revoke_offer_l with "Htok [Hoff]").
+    { iIntros (j K') "Hj". iApply ("Hoff" with "Hj"). }
 
-    rel_apply_l (revoke_offer_l with "Hγ Hoff").
     iIntros (j K') "Hoff".
+    iDestruct (offerInv_excl with "HN Hoff") as %?.
     iMod (offerReg_alloc off h2 γ j K' with "HNown") as "[HNown #Hfrag]"; eauto.
     iMod ("Hcl" with "[-]") as "_".
     { iNext. iExists _,_,_; iFrame.

theories/experimental/helping/mailbox.v

-(* ReLoC -- Relational logic for fine-grained concurrency *)
-(** A "mailbox" datastructure for helping.
-Based on the case study <https://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf> *)
-From iris.proofmode Require Import tactics.
-From iris.algebra Require Import excl.
-From reloc Require Export reloc.
-
-Definition mk_offer : val :=
-  λ: "v", ("v", ref #0).
-Definition revoke_offer : val :=
-  λ: "v", if: CAS (Snd "v") #0 #2 then SOME (Fst "v") else NONE.
-Definition take_offer : val :=
-  λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE.
-
-Definition put_mail : val := λ: "r" "v",
-  let: "off" := mk_offer "v" in
-  "r" <- SOME "off";;
-  revoke_offer "off".
-Definition get_mail : val := λ: "r",
-  match: !"r" with
-    NONE => NONE
-  | SOME "x" => take_offer "x"
-  end.
-Definition new_mb : val := λ: <>, ref NONE.
-Definition mailbox : val :=
-  (new_mb, put_mail, get_mail).
-
-
-Definition channelR := exclR unitR.
-Class channelG Σ := { channel_inG :> inG Σ channelR }.
-Definition channelΣ : gFunctors := #[GFunctor channelR].
-Instance subG_channelΣ {Σ} : subG channelΣ Σ → channelG Σ.
-Proof. solve_inG. Qed.
-
-Section side_channel.
-  Context `{!heapG Σ, !channelG Σ}.
-  Implicit Types l : loc.
-
-  Definition stages γ (P : val → iProp Σ) l v :=
-    ((l ↦ #0 ∗ P v)
-     ∨ (l ↦ #1)
-     ∨ (l ↦ #2 ∗ own γ (Excl ())))%I.
-
-  Definition is_offer γ (P : val → iProp Σ) (v : val) : iProp Σ :=
-    (∃ v' l, ⌜v = (v', # l)%V⌝ ∗ ∃ ι, inv ι (stages γ P l v'))%I.
-
-  (* A partial specification for revoke that will be useful later *)
-  Lemma revoke_works γ P v :
-    is_offer γ P v ∗ own γ (Excl ()) -∗
-    WP revoke_offer v
-      {{ v', (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}.
-  Proof.
-    iIntros "[#Hinv Hγ]".
-    rewrite /is_offer.
-    iDestruct "Hinv" as (v' l) "[% Hinv]"; simplify_eq.
-    iDestruct "Hinv" as (N) "#Hinv".
-    unlock revoke_offer.
-    wp_pures.
-    wp_bind (CmpXchg _ _ _).
-    iInv N as "Hstages" "Hclose".
-    iDestruct "Hstages" as "[H | [H | H]]".
-    - iDestruct "H" as "[Hl HP]".
-      wp_cmpxchg_suc.
-      iMod ("Hclose" with "[Hl Hγ]").
-      iRight; iRight; iFrame.
-      iModIntro. wp_pures.
-      iLeft. iExists v'; iSplit; auto.
-    - wp_cmpxchg_fail.
-      iMod ("Hclose" with "[H]").
-      iRight; iLeft; auto.
-      iModIntro. wp_pures.
-      iRight; auto.
-    - iDestruct "H" as "[Hl H]".
-      wp_cmpxchg_fail.
-      by iDestruct (own_valid_2 with "H Hγ") as %?.
-  Qed.
-
-  (* A partial specification for take that will be useful later *)
-  Lemma take_works γ N P v l :
-    inv N (stages γ P l v) -∗
-    WP take_offer (v, LitV l)%V
-      {{ v', (∃ v'' : val, ⌜v' = InjRV v''⌝ ∗ P v'') ∨ ⌜v' = InjLV #()⌝ }}.
-  Proof.
-    iIntros "#Hinv".
-    wp_rec. wp_pures.
-    wp_bind (CmpXchg _ _ _).
-    iInv N as "Hstages" "Hclose".
-    iDestruct "Hstages" as "[H | [H | H]]".
-    - iDestruct "H" as "[H HP]".
-      wp_cmpxchg_suc.
-      iMod ("Hclose" with "[H]").
-      iRight; iLeft; done.
-      iModIntro. wp_pures.
-      iLeft; auto.
-    - wp_cmpxchg_fail.
-      iMod ("Hclose" with "[H]").
-      iRight; iLeft; done.
-      iModIntro. wp_pures; eauto.
-    - iDestruct "H" as "[Hl Hγ]".
-      wp_cmpxchg_fail.
-      iMod ("Hclose" with "[Hl Hγ]").
-      iRight; iRight; iFrame.
-      iModIntro. wp_pures; eauto.
-  Qed.
-
-  Lemma mk_offer_works P (v : val) :
-    P v -∗
-    WP mk_offer v {{ v', ∃ γ, own γ (Excl ()) ∗ is_offer γ P v' }}.
-  Proof.
-    iIntros "HP".
-    wp_rec.
-    wp_alloc l as "Hl".
-    iApply wp_fupd.
-    wp_pures.
-    pose proof (nroot .@ "N'") as N'.
-    iMod (own_alloc (Excl ())) as (γ) "Hγ". done.
-    iMod (inv_alloc N' _ (stages γ P l v) with "[HP Hl]") as "#Hinv'".
-    { iNext. rewrite /stages. iLeft. iFrame. }
-    iModIntro.
-    iExists γ; iFrame.
-    unfold is_offer.
-    iExists _, _; iSplitR; eauto.
-  Qed.
-
-End side_channel.
-
-Section mailbox.
-  Context `{!heapG Σ, !channelG Σ}.
-  Implicit Types l : loc.
-
-  Definition mailbox_inv (P : val → iProp Σ) (v : val) : iProp Σ :=
-    (∃ l : loc, ⌜v = # l⌝ ∗ (l ↦ NONEV ∨ (∃ v' γ, l ↦ SOMEV v' ∗ is_offer γ P v')))%I.
-
-  Theorem new_mb_works (P : val → iProp Σ) (Φ : val → iProp Σ) :
-    (∀ v N, inv N (mailbox_inv P v) -∗ Φ v)
-    -∗ WP new_mb #() {{ Φ }}.
-  Proof.
-    iIntros "HΦ".
-    unlock new_mb.
-    wp_rec.
-    iApply wp_fupd.
-    wp_alloc r as "Hr".
-    pose proof (nroot .@ "N") as N.
-    iMod (inv_alloc N _ (mailbox_inv P (# r)) with "[Hr]") as "#Hinv".
-    { iExists r; iSplit; try iLeft; auto. }
-    iModIntro.
-    by iApply "HΦ".
-  Qed.
-
-  Theorem put_mail_works (P : val → iProp Σ) (Φ : val → iProp Σ) N (mb v : val) :
-    inv N (mailbox_inv P mb) -∗
-    P v -∗
-    (∀ v', ((∃ v'', ⌜v' = SOMEV v''⌝ ∗ P v'') ∨ ⌜v' = NONEV⌝) -∗ Φ v')
-    -∗ WP put_mail mb v {{ Φ }}.
-  Proof.
-    iIntros "#Hinv HP HΦ".
-    wp_rec.
-    wp_pures.
-    wp_bind (mk_offer v).
-    iApply (wp_wand with "[HP]").
-    { iApply (mk_offer_works with "HP"). }
-    iIntros (off). iDestruct 1 as (γ) "[Hγ #Hoffer]".
-    wp_let.
-    wp_bind (mb <- _)%E. wp_pures.
-    iInv N as "Hmailbox" "Hclose".
-    iDestruct "Hmailbox" as (l) "[>% Hl]". simplify_eq/=.
-    iDestruct "Hl" as "[>Hl | Hl]";
-      [ | iDestruct "Hl" as (off' γ') "[Hl Hoff']"]; (* off' - already existing offer *)
-      wp_store;
-      [iMod ("Hclose" with "[Hl]") | iMod ("Hclose" with "[Hl Hoff']")];
-      try (iExists _; iNext; iSplit; eauto);
-      iModIntro;
-      wp_pures;
-      iApply (wp_wand with "[Hγ Hoffer] HΦ");
-      iApply (revoke_works with "[$]").
-  Qed.
-
-  Theorem get_mail_works (P : val → iProp Σ) (Φ : val → iProp Σ) N (mb : val) :
-    inv N (mailbox_inv P mb) -∗
-    (∀ v', ((∃ v'', ⌜v' = SOMEV v''⌝ ∗ P v'') ∨ ⌜v' = NONEV⌝) -∗ Φ v')
-    -∗ WP get_mail mb {{ Φ }}.
-  Proof.
-    iIntros "#Hinv HΦ".
-    unlock get_mail.
-    wp_rec.
-    wp_bind (! _)%E.
-    iInv N as "Hmailbox" "Hclose".
-    iDestruct "Hmailbox" as (l') "[>% H]"; simplify_eq/=.
-    iDestruct "H" as "[H | H]".
-    + wp_load.
-      iMod ("Hclose" with "[H]").
-      iExists l'; iSplit; auto.
-      iModIntro.
-      wp_pures. iApply "HΦ"; auto.
-    + iDestruct "H" as (v' γ) "[Hl' #Hoffer]".
-      wp_load.
-      iMod ("Hclose" with "[Hl' Hoffer]").
-      { iExists l'; iSplit; auto.
-        iRight; iExists v', γ; by iSplit. }
-      iModIntro.
-      wp_pures.
-      iDestruct "Hoffer" as (v'' l'') "[% Hoffer]"; simplify_eq.
-      iDestruct "Hoffer" as (ι) "Hinv'".
-      iApply (wp_wand with "[] HΦ").
-      iApply take_works; auto.
-  Qed.
-
-End mailbox.

theories/experimental/helping/offers.v

+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Offers used to implement the stack with helping
+Based on the case study <https://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf> *)
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import excl.
+From reloc Require Export reloc.
+
+Definition mk_offer : val :=
+  λ: "v", ("v", ref #0).
+Definition revoke_offer : val :=
+  λ: "v", if: CAS (Snd "v") #0 #2 then SOME (Fst "v") else NONE.
+Definition take_offer : val :=
+  λ: "v", if: CAS (Snd "v") #0 #1 then SOME (Fst "v") else NONE.
+
+Definition offerR := exclR unitR.
+Class offerG Σ := { offer_inG :> inG Σ offerR }.
+Definition offerΣ : gFunctors := #[GFunctor offerR].
+Instance subG_offerΣ {Σ} : subG offerΣ Σ → offerG Σ.
+Proof. solve_inG. Qed.
+
+Section rules.
+  Context `{!relocG Σ, !offerG Σ}.
+
+  Definition offer_token γ := own γ (Excl ()).
+
+  Lemma offer_token_exclusive γ : offer_token γ -∗ offer_token γ -∗ False.
+  Proof. iIntros "H1 H2". iDestruct (own_valid_2 with "H1 H2") as %[]. Qed.
+
+  (** The offer invariant *)
+  Definition is_offer γ (l : loc) (P Q : iProp Σ) :=
+    (∃ (c : nat), l ↦ #c ∗
+        (⌜c = 0⌝ ∗ P
+       ∨ ⌜c = 1⌝ ∗ (Q ∨ offer_token γ)
+       ∨ ⌜c = 2⌝ ∗ offer_token γ))%I.
+
+  Lemma is_offer_exclusive γ1 γ2 l P1 Q1 P2 Q2 :
+    is_offer γ1 l P1 Q1 -∗ is_offer γ2 l P2 Q2 -∗ False.
+  Proof.
+    iDestruct 1 as (?) "[Hl1 _]". iDestruct 1 as (?) "[Hl2 _]".
+    iDestruct (gen_heap.mapsto_valid_2 with "Hl1 Hl2") as %?. contradiction.
+  Qed.
+
+  Lemma make_is_offer γ l P Q : l ↦ #0 -∗ P -∗ is_offer γ l P Q.
+  Proof. iIntros "Hl HP". iExists 0; by eauto with iFrame. Qed.
+
+  Lemma mk_offer_l K (v : val) t A :
+    (∀ γ l, (∀ P Q, P -∗ is_offer γ l P Q) -∗ offer_token γ -∗ REL fill K (of_val (v, #l)) << t : A) -∗
+    REL fill K (mk_offer v) << t : A.
+  Proof.
+    iIntros "Hcont". rel_rec_l. rel_alloc_l l as "Hl".
+    iMod (own_alloc (Excl ())) as (γ) "Hγ". done.
+    rel_pures_l. iApply ("Hcont" with "[Hl] Hγ").
+    iIntros (P Q) "HP". iExists 0; eauto with iFrame.
+  Qed.
+
+  Lemma take_offer_l γ E o v t A K P Q :
+    (|={⊤, E}=> ▷ is_offer γ o P Q ∗
+         ▷ ((is_offer γ o P Q -∗ REL fill K (of_val NONEV) << t @ E : A)
+            ∧ (P -∗ (Q -∗ is_offer γ o P Q) -∗ REL fill K (of_val $ SOMEV v) << t @ E : A))) -∗
+    REL fill K (take_offer (v, #o)%V) << t : A.
+  Proof.
+    iIntros "Hlog". rel_rec_l. rel_pures_l.
+    rel_cmpxchg_l_atomic.
+    iMod "Hlog" as "(Hoff & Hcont)".
+    rewrite {1}/is_offer. iDestruct "Hoff" as (c) "[Hl Hoff]".
+    iModIntro. iExists _. iFrame "Hl". iSplit.
+    - iIntros (?). iNext.
+      iDestruct "Hcont" as "[Hcont _]".
+      iIntros "Hl".
+      rel_pures_l. iApply ("Hcont" with "[-]").
+      iExists _; iFrame.
+    - iIntros (?). simplify_eq/=.
+      assert (c = 0%nat) as -> by lia. (* :) *)
+      iNext. iIntros "Hl".
+      iDestruct "Hoff" as "[[% HP] | [[% ?] | [% ?]]]"; [| congruence..].
+      rel_pures_l.
+      iDestruct "Hcont" as "[_ Hcont]".
+      iApply ("Hcont" with "HP [-]").
+      iIntros "HQ". rewrite /is_offer. iExists 1.
+      iFrame. iRight. iLeft. iSplit; eauto.
+  Qed.
+
+  Lemma wp_revoke_offer γ l E P Q (v : val) Φ :
+    offer_token γ -∗
+    ▷ (|={⊤, E}=> ▷ is_offer γ l P Q ∗
+        ▷ ((is_offer γ l P Q -∗ Q ={E, ⊤}=∗ Φ NONEV)
+           ∧ (is_offer γ l P Q -∗ P ={E, ⊤}=∗ Φ (SOMEV v)))) -∗
+    WP (revoke_offer (of_val (v, #l))) {{ Φ }}.
+  Proof.
+    iIntros "Hγ Hlog". wp_rec. wp_pures.
+    wp_bind (CmpXchg _ _ _). iApply wp_atomic.
+    iMod "Hlog" as "(Hoff & Hcont)".
+    rewrite {1}/is_offer. iDestruct "Hoff" as (c) "[Hl Hoff]".
+    iModIntro. iDestruct "Hoff" as "[(>-> & HP)|[(>-> & HQ) | (>-> & Htok)]]".
+    - wp_cmpxchg_suc; first fast_done.
+      iDestruct "Hcont" as "[_ Hcont]".
+      iMod ("Hcont" with "[-HP] HP") as "HΦ".
+      { iExists 2. iFrame "Hl". iRight. iRight. eauto. }
+      iModIntro. by wp_pures.
+    - wp_cmpxchg_fail; first done.
+      iDestruct "Hcont" as "[Hcont _]".
+      iDestruct "HQ" as "[HQ | Htok]"; last first.
+      { iExFalso. iApply (offer_token_exclusive with "Hγ Htok"). }
+      iMod ("Hcont" with "[-HQ] HQ") as "HΦ".
+      { iExists 1. iFrame "Hl". iRight. iLeft. eauto. }
+      iModIntro. by wp_pures.
+    - wp_cmpxchg_fail; first done.
+      iExFalso. iApply (offer_token_exclusive with "Hγ Htok").
+  Qed.
+
+End rules.
+
+Global Opaque offer_token is_offer revoke_offer take_offer mk_offer.