The stack with helping refinement

theories/examples/stack/helping.v

 (* Stack with helping *)
 From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth gmap agree list.
+From iris.base_logic Require Export gen_heap invariants lib.auth.
+From iris_logrel.examples.stack Require Import CG_stack.
 From iris_logrel Require Export logrel examples.stack.mailbox.
 
 Definition LIST τ :=
@@ -42,179 +45,584 @@ Definition mk_stack : val :=  λ: "_",
   (pop_st "r" (λ: <>, "get" "mb"),
    push_st "r" (λ: "n", "put" "mb" "n")).
 
-Section stack_works.
-  Context `{!heapG Σ}.
-  Implicit Types l : loc.
+Section refinement.
+  Context `{!logrelG Σ}.
+  Definition CG_mkstack : val :=
+    Λ: let: "l" := ref #false in
+       let: "st" := ref Nile in
+       (CG_locked_pop "st" "l", CG_locked_push "st" "l").
 
-  Definition is_stack_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
-     val -c> iProp Σ := λ v,
-    (v ≡ FoldV NONEV ∨ ∃ (h t : val), v ≡ FoldV (SOMEV (h, t))%V ∗ P h ∗ ▷ F t)%I.
+  Canonical Structure ectx_itemC := leibnizC ectx_item.
+  Canonical Structure locC := leibnizC loc.
+  Canonical Structure gnameC := leibnizC gname.
 
-  Local Instance is_stack_contr (P : val → iProp Σ): Contractive (is_stack_pre P).
+  Definition offerReg := gmap loc (val * gname * nat * (list ectx_item)).
+  Definition offerRegR :=
+    gmapUR loc
+      (agreeR (prodC valC (prodC gnameC (prodC natC (listC ectx_itemC))))).
+  Class offerRegPreG Σ := OfferRegPreG
+  { offerReg_inG :> authG Σ offerRegR }.
+  Definition offerize (x : (val * gname * nat * (list ectx_item))) :
+    (agreeR (prodC valC (prodC gnameC (prodC natC (listC ectx_itemC))))) :=
+    match x with
+    | (v, γ, n, K) => to_agree (v, (γ, (n, K)))
+    end.
+  Definition to_offer_reg : offerReg -> offerRegR := fmap offerize.
+  Lemma to_offer_reg_valid N : ✓ to_offer_reg N.
+  Proof. intros l. rewrite lookup_fmap. case (N !! l); simpl; try done.
+         intros [[[v γ] n] K]; simpl. done. Qed.
+
+  Context `{!offerRegPreG Σ, !channelG Σ}.
+
+  Definition stackN := nroot .@ "stacked".
+
+  Definition offerInv (N : offerReg) (st' lc : loc) : iProp Σ :=
+    ([∗ map] l ↦ w ∈ N,
+     match w with
+     | (v,γ,j,K) => ∃ (c : nat),
+       l ↦ᵢ #c ∗
+        (⌜c = 0⌝ ∗ j ⤇ fill K (CG_locked_push $/ LitV (Loc st') $/ LitV (Loc lc) $/ v)%E
+       ∨ ⌜c = 1⌝ ∗ (j ⤇ fill K #() ∨ own γ (Excl ()))
+       ∨ ⌜c = 2⌝ ∗ own γ (Excl ()))
+     end)%I.
+
+  Lemma offerInv_empty (st' lc : loc) :
+    offerInv ∅ st' lc.
+  Proof. by rewrite /offerInv big_sepM_empty. Qed.
+
+  Lemma offerInv_excl (N : offerReg) (st' lc : loc) (o : loc) (v : val) :
+    offerInv N st' lc -∗ o ↦ᵢ v -∗ ⌜N !! o = None⌝.
   Proof.
-    rewrite /is_stack_pre  => n f f' Hf v.
-    repeat (f_contractive || f_equiv).
-    apply Hf.
+    rewrite /offerInv.
+    iIntros "HN Ho".
+    iAssert (⌜is_Some (N !! o)⌝ → False)%I as %Hbaz.
+    {
+      iIntros ([[[[? ?] ?] ?] HNo]).
+      rewrite (big_sepM_lookup _ N o _ HNo).
+      iDestruct "HN" as (c) "[HNo ?]".
+      iDestruct (mapsto_valid_2 o with "Ho HNo") as %Hfoo.
+      compute in Hfoo. contradiction.
+    }
+    iPureIntro.
+    destruct (N !! o); eauto. exfalso. apply Hbaz; eauto.
   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).
+  Lemma offerReg_alloc (o : loc) (v : val) (γ : gname)
+    (j : nat) (K : list ectx_item) (γo : gname) (N : offerReg)  :
+    N !! o = None →
+    own γo (● to_offer_reg N)
+    ==∗ own γo (● to_offer_reg (<[o:=(v, γ, j, K)]> N))
+      ∗ own γo (◯ {[o := to_agree (v, (γ, (j, K)))]}).
+  Proof.
+    iIntros (HNo) "HN".
+    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.
+    }
+    iFrame.
+    by rewrite /to_offer_reg fmap_insert.
+  Qed.
 
-  Definition stack_inv P v :=
-    (∃ l v', ⌜v = # l⌝ ∗ l ↦ᵢ v' ∗ is_stack P v')%I.
+  Lemma offerReg_frag_lookup (o : loc) (v : val) (γ : gname)
+    (j : nat) (K : list ectx_item) (γo : gname) (N : offerReg)  :
+    own γo (● to_offer_reg N)
+    -∗ own γo (◯ {[o := to_agree (v, (γ, (j, K)))]})
+    -∗ ⌜N !! o = Some (v, γ, j, K)⌝.
+  Proof.
+    iIntros "HN Hfrag".
+    iDestruct (own_valid_2 with "HN Hfrag") as %Hfoo.
+    apply auth_valid_discrete in Hfoo.
+    simpl in Hfoo. destruct Hfoo as [Hfoo _].
+    iAssert (⌜✓ ((to_offer_reg N) !! o)⌝)%I as %Hvalid.
+    { iDestruct (own_valid with "HN") as %HNvalid.
+      rewrite auth_valid_eq /= in HNvalid.
+      destruct HNvalid as [_ HNvalid].
+      done. }
+    iPureIntro.
+    revert Hfoo.
+    rewrite left_id.
+    rewrite singleton_included=> -[av []].
+    revert Hvalid.
+    rewrite /to_offer_reg !lookup_fmap.
+    case: (N !! o)=> [av'|] Hvalid; last by inversion 1.
+    intros Hav.
+    rewrite -(inj Some _ _ Hav).
+    rewrite Some_included_total.
+    destruct av' as [[[??]?]?]. simpl.
+    rewrite to_agree_included.
+    fold_leibniz.
+    intros. by simplify_eq.
+  Qed.
 
-  Lemma is_stack_unfold (P : val → iProp Σ) v :
-      is_stack P v ⊣⊢ is_stack_pre P (is_stack P) v.
+  Lemma offerReg_lookup_frag (o : loc) (v : val) (γ : gname)
+    (j : nat) (K : list ectx_item) (γo : gname) (N : offerReg) :
+    N !! o = Some (v, γ, j, K) →
+    own γo (● to_offer_reg N)
+    ==∗ own γo (◯ {[o := to_agree (v, (γ, (j, K)))]})
+      ∗ own γo (● to_offer_reg N).
   Proof.
-    rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)).
+    iIntros (HNo) "Hown".
+    iMod (own_update with "[Hown]") as "Hown".
+    { eapply (auth_update (to_offer_reg N) ∅).
+      eapply (op_local_update_discrete _ ∅ {[o := to_agree (v, (γ, (j, K)))]}).
+      intros. intros i. destruct (decide (i = o)); subst; rewrite lookup_op.
+      + rewrite lookup_singleton lookup_fmap HNo.
+        rewrite -Some_op.
+        rewrite Some_valid.
+        rewrite agree_idemp. done.
+      + rewrite lookup_singleton_ne; eauto.
+        rewrite left_id.
+        done.
+    }
+    { rewrite right_id. iFrame "Hown". }
+    iDestruct "Hown" as "[Ho Hown]".
+    rewrite right_id. iFrame.
+    assert ({[o := to_agree (v, (γ, (j, K)))]} ⋅ to_offer_reg N ≡ to_offer_reg N) as Hfoo.
+    { intro i.
+      rewrite /to_offer_reg lookup_merge !lookup_fmap.
+      destruct (decide (i = o)); subst.
+      + rewrite HNo lookup_singleton /=.
+        rewrite -Some_op.
+        apply Some_proper.
+        symmetry. apply agree_included.
+        by apply to_agree_included.
+      + rewrite lookup_singleton_ne; eauto.
+        by rewrite left_id. }
+    by rewrite Hfoo.
   Qed.
 
-  Lemma is_stack_disj (P : val → iProp Σ) v :
-      is_stack P v -∗ is_stack P v ∗ (v ≡ FoldV NONEV ∨ ∃ (h t : val), v ≡ FoldV (SOMEV (h, t))%V).
+  Definition stackRel (v1 v2 : val) : iProp Σ :=
+    ⟦ LIST TNat ⟧ [] (v1, v2).
+  Instance stackRel_persistent v1 v2 : PersistentP (stackRel v1 v2).
+  Proof. apply _. Qed.
+  Lemma stackRel_empty : stackRel (FoldV (InjLV #())) (FoldV (InjLV #())).
+  Proof.
+    rewrite /stackRel /= fixpoint_unfold /=.
+    iExists (_,_). iSplit; eauto.
+    iNext. iLeft. iExists (_,_); eauto.
+  Qed.
+  Hint Resolve stackRel_empty.
+  Lemma stackRel_cons (n : nat) t1 t2 :
+    ▷ stackRel t1 t2 -∗ stackRel (FoldV (InjRV (#n, t1))) (FoldV (InjRV (#n, t2))).
   Proof.
-    iIntros "Hstack".
-    iDestruct (is_stack_unfold with "Hstack") as "[#Hstack|Hstack]".
-    - iSplit; try iApply is_stack_unfold; iLeft; auto.
-    - iDestruct "Hstack" as (h t) "[#Heq rest]".
-      iSplitL; try iApply is_stack_unfold; iRight; auto.
+    iIntros "#Hs".
+    rewrite /stackRel /=.
+    rewrite {2}fixpoint_unfold /=.
+    iExists (_,_). iSplit; eauto.
+    iNext. iRight. iExists (_, _). iSplit; eauto.
+    iExists (_,_), (_,_). iSplit; eauto.
+  Qed.
+  Lemma stackRel_unfold v1 v2 :
+    stackRel v1 v2
+         ⊣⊢
+    (∃ w1 w2, (⌜v1 = FoldV w1⌝ ∧ ⌜v2 = FoldV w2⌝)
+    ∧ ▷ ((⌜w1 = (InjLV #())⌝ ∧ ⌜w2 = (InjLV #())⌝)
+      ∨ ∃ (n : nat) t1 t2, ⌜v1 = FoldV (InjRV (#n, t1))⌝
+                         ∧ ⌜v2 = FoldV (InjRV (#n, t2))⌝
+                         ∧ stackRel t1 t2))%I.
+  Proof.
+    rewrite /stackRel /= {1}fixpoint_unfold /=.
+    iSplit.
+    - iDestruct 1 as ([? ?]) "[% R]". simplify_eq.
+      iExists _, _. iSplit; eauto.
+      iNext.
+      iDestruct "R" as "[R | R]"; [iLeft | iRight].
+      + iDestruct "R" as ([? ?]) "[% [% %]]"; simplify_eq/=.
+        done.
+      + iDestruct "R" as ([? ?]) "[% R]"; simplify_eq/=.
+        iDestruct "R" as ([? ?] [? ?]) "[% [Rn #R]]"; simplify_eq/=.
+        iDestruct "Rn" as (n) "[% %]"; simplify_eq/=.
+        iExists n, _, _. iSplit; eauto.
+    - iDestruct 1 as (? ?) "[[% %] R]". simplify_eq/=.
+      iExists (_, _). iSplit; eauto.
+      iNext.
+      iDestruct "R" as "[[% %] | R]"; [iLeft | iRight]; simplify_eq/=.
+      + iExists (_,_); eauto.
+      + iDestruct "R" as (n ? ?) "[% [% #R]]". simplify_eq/=.
+        iExists (_,_); iSplit; eauto.
+        iExists (_,_), (_,_). iSplit; eauto.
+  Qed.
+
+  Definition stackInv oname (st st' mb lc : loc) : iProp Σ :=
+    (∃ v1 v2 (N : offerReg), lc ↦ₛ #false ∗ st ↦ᵢ v1 ∗ st' ↦ₛ v2 ∗ stackRel v1 v2
+     ∗ (mb ↦ᵢ NONEV
+        ∨ (∃ (l : loc) (n : nat) γ j K, mb ↦ᵢ SOMEV (#n, #l) ∗ ⌜N !! l = Some (#n, γ, j, K)⌝))
+     ∗ own oname (● to_offer_reg N)
+     ∗ offerInv N st' lc)%I.
+
+  Definition pull_no_offer (st mb : loc) : expr :=
+    match: Unfold ! #st with
+      InjL <> => InjL #()
+    | InjR "hd" =>
+      if: CAS #st (Fold (InjR "hd")) (Snd "hd") then InjR (Fst "hd")
+      else (rec: "pop" <> :=
+              match: #() ;;
+                      let: "r" := #mb in
+                      match: ! "r" with
+                        InjL <> => InjL #()
+                      | InjR "x" => take_offer "x"
+                      end with
+                InjL <> =>
+                match: Unfold ! #st with
+                  InjL <> => InjL #()
+                | InjR "hd" =>
+                  if: CAS #st (Fold (InjR "hd")) (Snd "hd") then
+                    InjR (Fst "hd") else "pop" #()
+                end
+              | InjR "x" => InjR "x"
+              end) #()
+    end.
+
+  Lemma stack_pull_no_offer Δ Γ γo st st' mb l' :
+    inv stackN (stackInv γo st st' mb l') -∗
+    ▷ ({⊤,⊤;Δ;Γ} ⊨ (rec: "pop" <> :=
+              match: #() ;;
+                      let: "r" := #mb in
+                      match: ! "r" with
+                        InjL <> => InjL #()
+                      | InjR "x" => take_offer "x"
+                      end with
+                InjL <> =>
+                match: Unfold ! #st with
+                  InjL <> => InjL #()
+                | InjR "hd" =>
+                  if: CAS #st (Fold (InjR "hd")) (Snd "hd") then
+                    InjR (Fst "hd") else "pop" #()
+                end
+              | InjR "x" => InjR "x"
+              end) #() ≤log≤
+              ((CG_locked_pop $/ LitV st' $/ LitV l') #()) :
+      TSum TUnit TNat) -∗
+        {⊤,⊤;Δ;Γ} ⊨
+              pull_no_offer st mb
+              ≤log≤
+              ((CG_locked_pop $/ LitV st' $/ LitV l') #()) :
+      TSum TUnit TNat.
+  Proof.
+    iIntros "#Hinv IH".
+    unfold pull_no_offer.
+    rel_load_l_atomic.
+    iInv stackN as (s1 s2 N) "(Hl & Hst1 & Hst2 & Hrel & >Hmb & HNown & HN)" "Hcl".
+    iModIntro. iExists _; iFrame. iNext. iIntros "Hst1".
+    rewrite stackRel_unfold.
+    iDestruct "Hrel" as (w1 w2) "[[% %] #Hrel]"; simplify_eq/=.
+    iApply fupd_logrel'.
+    iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq; iModIntro; rel_fold_l.
+    - rel_case_l.
+      rel_seq_l.
+      rel_apply_r (CG_pop_fail_r with "Hst2 Hl").
+      { solve_ndisj. }
+      iIntros "Hst' Hl".
+      iMod ("Hcl" with "[-]").
+      { iNext. iExists _,_,_. iFrame.
+        rewrite stackRel_unfold.
+        iExists _,_; iSplit; eauto. }
+      rel_vals. iLeft. iModIntro. iExists (_,_). eauto.
+    - iApply fupd_logrel'.
+      iDestruct "Hrel" as (n t1 t2) "(>% & >% & Hrel)". simplify_eq/=.
+      iModIntro.
+      rel_case_l.
+      rel_let_l.
+      iMod ("Hcl" with "[-IH]").
+      { iNext. iExists _,_,_. iFrame.
+        rewrite (stackRel_unfold (FoldV (InjRV (#n, t1))) (FoldV (InjRV (#n, t2)))).
+        iExists _,_; iSplit; eauto.
+        iNext. iRight. iExists _,_,_; eauto. }
+      rel_proj_l.
+      rel_cas_l_atomic.
+      iClear "Hrel".
+      iInv stackN as (s1 s2 N') "(Hl & Hst1 & Hst2 & Hrel & >Hmb & HNown & HN)" "Hcl".
+      iModIntro. iExists _; iFrame.
+      destruct (decide (s1 = FoldV (InjRV (#n, t1)))); subst.
+      + (* Going to succeed *)
+        iSplitR.
+        { iIntros "%"; congruence. }
+        iIntros (?). iNext. iIntros "Hst1".
+        rel_if_true_l.
+        rewrite stackRel_unfold.
+        iApply fupd_logrel'.
+        iDestruct "Hrel" as (??) "[[% %] Hrel]"; simplify_eq/=.
+        iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq.
+        iDestruct "Hrel" as (???) "(>% & >% & Hrel)"; simplify_eq/=.
+        iModIntro.
+        rel_apply_r (CG_pop_suc_r with "Hst2 Hl").
+        { solve_ndisj. }
+        iIntros "Hst' Hl".
+        rel_fst_l.
+        iMod ("Hcl" with "[-IH]").
+        { iNext. iExists _,_,_. iFrame. }
+        rel_vals. iRight. iExists (_,_). eauto.
+      + (* Going to retry *)
+        iSplitL; last first.
+        { iIntros "%". congruence. }
+        iIntros "%". iNext. iIntros "Hst".
+        rel_if_false_l.
+        iMod ("Hcl" with "[-IH]").
+        { iNext. iExists _,_,_. iFrame. }
+        iApply "IH".
   Qed.
 
-  Theorem stack_works {channelG0 : channelG Σ} P Φ :
-    (∀ (f₁ f₂ : val),
-            (□ WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ P v')  ∨ v ≡ NONEV }})
-         -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }}))
-         -∗ Φ (f₁, f₂)%V)%I
-    -∗ WP mk_stack #()  {{ Φ }}.
+  Lemma refinement Γ :
+    Γ ⊨ mk_stack #() ≤log≤ TApp CG_mkstack :
+      (TProd (TArrow TUnit (MAYBE TNat))
+             (TArrow TNat TUnit)).
   Proof.
-    iIntros "HΦ".
+    iIntros (Δ).
+    unlock CG_mkstack.
+    assert (Closed (dom (gset string) Γ) (mk_stack #())).
+    { eapply Closed_mono with ∅; eauto. set_solver. }
+    assert (Closed (dom (gset string) Γ) (let: "l" := ref #false in
+      let: "st" := ref Nile in
+      ((CG_locked_pop "st") "l", (CG_locked_push "st") "l"))).
+    { eapply Closed_mono with ∅; eauto. set_solver. }
+    rel_tlam_r.
+    rel_alloc_r as l' "Hl'". rel_let_r.
+    rel_alloc_r as st' "Hst'". rel_let_r.
     unlock mk_stack.
-    wp_rec.
-    wp_pack.
-    wp_let.
-    repeat wp_proj; wp_let.
-    repeat wp_proj; wp_let.
-    repeat wp_proj; wp_let.
-    wp_bind (new_mb _).
-    iApply (new_mb_works P).
-    iIntros (mb Nmb) "#Hinv".
-    wp_let.
-    wp_alloc r as "Hr".
-    wp_let.
-    pose proof (nroot .@ "N") as N.
-    iMod (inv_alloc N _ (stack_inv P #r) with "[Hr]") as "#Hisstack".
-    { iExists r, (FoldV NONEV); iFrame; iSplit; auto. iApply is_stack_unfold; iLeft; done. }
-    unlock pop_st. do 2 wp_rec.
-    unlock push_st. do 2 wp_rec.
-    wp_value; last first.
-    (* TODO: solve_to_val. either doesn't work or too slow *)
-    { rewrite /IntoVal /= ?decide_left.
-      simpl. done. }
-    iApply "HΦ".
-    (* The verification of pop *)
-    - iIntros "!#".
-      iLöb as "IH".
-      wp_rec.
-      wp_rec.
-      wp_bind (get_mail _).
-      iApply (get_mail_works P with "Hinv").
-      iIntros (v) "Hv".
-      iDestruct "Hv" as "[H | H]".
-      + iDestruct "H" as (v') "[% HP]".
-        subst.
-        simpl. wp_case_inr. (* TODO: we require a simpl here *)
-        wp_let.
-        iApply wp_value.
-        iLeft; iExists v'; auto.
-      + iDestruct "H" as "%"; subst.
-        wp_case.
-        wp_seq.
-        wp_bind (! #r)%E.
-        iInv N as "Hstack" "Hclose".
-        iDestruct "Hstack" as (l'' v'') "[>% [Hl' Hstack]]". simplify_eq/=.
-        wp_load.
-        iDestruct (is_stack_disj with "Hstack") as "[Hstack #Heq]".
-        iMod ("Hclose" with "[Hl' Hstack]").
-        { iExists l'', v''; iFrame; auto. }
+    rel_rec_l.
+    rel_pack_l.
+    repeat (rel_rec_l; repeat rel_proj_l).
+    unlock new_mb. simpl_subst/=.
+    rel_alloc_l as mb "Hmb". rel_let_l.
+    rel_alloc_l as st "Hst". rel_let_l.
+    unlock pop_st. rel_rec_l. rel_let_l.
+    unlock push_st. rel_rec_l. rel_let_l.
+    unlock CG_locked_pop. rel_rec_r. rel_let_r.
+    unlock CG_locked_push. rel_rec_r. rel_let_r.
+    iApply fupd_logrel.
+    iMod (own_alloc (● to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor".
+    { apply auth_auth_valid. apply to_offer_reg_valid. }
+    iMod (inv_alloc stackN _ (stackInv γo st st' mb l') with "[-]") as "#Hinv".
+    { iNext. unfold stackInv.
+      iExists _, _, _. iFrame.
+      iSplit; eauto. iApply stackRel_empty.
+      iSplitL; first eauto.
+      iApply offerInv_empty. }
+    iModIntro.
+    iApply bin_log_related_pair; last first.
+  (* * Push refinement *)
+  { iApply bin_log_related_arrow_val; eauto.
+    iAlways. iIntros (h1 h2) "#Hh"; simplify_eq/=.
+    iDestruct "Hh" as (n) "[% %]"; simplify_eq/=.
+    rel_rec_r.
+    iLöb as "IH".
+    rel_rec_l.
+    rel_let_l.
+    unlock put_mail. repeat rel_rec_l.
+    unlock mk_offer.
+    (* rel_rec_l. (* TODO: picks the wrong "reduct" *) *)
+    rel_bind_l (App _ #n).
+    rel_rec_l.
+    rel_alloc_l as o "Ho".
+    rel_let_l.
+    rel_store_l_atomic.
+    iInv stackN as (s1 s2 N) "(Hl & Hst1 & Hst2 & Hrel & >Hmb & HNown & HN)" "Hcl".
+    iModIntro.
+    iAssert (∃ v, ▷ mb ↦ᵢ v)%I with "[Hmb]" as (v) "Hmb".
+    { iDestruct "Hmb" as "[Hmb | Hmb]".
+      - iExists (InjLV #()); eauto.
+      - iDestruct "Hmb" as (l m γ j K) "[Hmb ?]".
+        iExists (InjRV (#m, #l)); eauto. }
+    iExists _; iFrame; iNext.
+    iIntros "Hmb".
+    rel_rec_l.
+    unlock revoke_offer. rel_rec_l.
+    rewrite {2}bin_log_related_eq /bin_log_related_def.
+    iIntros (vvs ρ) "#Hs #HΓ".
+    iIntros (j K) "Hj". cbn[snd fst].
+    rewrite {2}/env_subst Closed_subst_p_id.
+    iDestruct (offerInv_excl with "HN Ho") as %Hbaz.
+    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+    iMod (offerReg_alloc o #n γ j K with "HNown") as "[HNown Hfrag]"; eauto.
+    iMod ("Hcl" with "[-Hfrag Hγ]") as "_".
+    { iNext. iExists _,_,_; iFrame.
+      iSplitL "Hmb".
+      - iRight. iExists _, _; iFrame "Hmb".
+        iPureIntro. do 3 eexists. by rewrite lookup_insert.
+      - rewrite /offerInv big_sepM_insert; eauto.
+        iFrame.
+        iExists 0. iFrame "Ho".
+        iLeft. unlock CG_locked_push.
+        rewrite /env_subst !Closed_subst_p_id.
+        simpl_subst/=. eauto. }
+    iModIntro. wp_proj.
+    wp_bind (CAS _ _ _).
+    iInv stackN as (s1' s2' N') "(Hl & Hst1 & Hst2 & Hrel & >Hmb & >HNown & HN)" "Hcl".
+    iDestruct (offerReg_frag_lookup with "HNown Hfrag") as %Hfoo.
+    rewrite /offerInv.
+    rewrite (big_sepM_lookup_acc _ N'); eauto.
+    iDestruct "HN" as "[HoN HN]".
+    iDestruct "HoN" as (c) ">[Ho Hc]".
+    destruct (decide (c = 0)); subst.
+    * wp_cas_suc.
+      iDestruct "Hc" as "[[% Hj] | [[% Hc] | [% Hc]]]"; [ | congruence..].
+      iMod ("Hcl" with "[-Hj Hfrag]").
+      { iNext. iExists _,_,_; iFrame.
+        iApply "HN".
+        iExists _; iFrame; eauto. }
+      iModIntro.
+      wp_if.
+      wp_proj.
+      wp_case.
+      wp_let.
+      clear.
+      wp_bind (! #st)%E.
+      iInv stackN as (s1 s2 N) "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
+      wp_load.
+      iMod ("Hcl" with "[-Hj Hfrag]") as "_".
+      { iNext. iExists _,_,_; iFrame. }
+      iModIntro. repeat (wp_pure _).
+      wp_bind (CAS _ _ _).
+      clear N.
+      iInv stackN as (s1' s2' N) "(>Hl & >Hst1 & >Hst2 & Hrel & Hmb & HNown & HN)" "Hcl"; simplify_eq.
+      destruct (decide (s1 = s1')).
+      ** (* CAS/push succeeds *)
+        wp_cas_suc.
+        unlock {1}CG_locked_push. simpl_subst/=.
+        unlock {2}acquire {2}release.
+        tp_rec j.
+        tp_cas_suc j. simpl.
+        repeat (tp_pure j _). simpl.
+        unlock CG_push.
+        repeat (tp_pure j _; simpl). simpl.
+        repeat (tp_rec j).
+        tp_load j; simpl.
+        tp_store j; simpl.
+        tp_seq j; simpl.
+        tp_rec j; simpl.
+        tp_store j; simpl.
+        iDestruct (stackRel_cons n with "Hrel") as "Hrel".
+        iMod ("Hcl" with "[-Hj]").
+        { iNext. iExists _,_,_; subst; iFrame; eauto. }
         iModIntro.
-        iDestruct "Heq" as "[H | H]".
-        * iRewrite "H".
-          wp_unfold.
-          wp_case. wp_seq. iApply wp_value.
-          iRight; auto.
-        * iDestruct "H" as (h t) "H"; iRewrite "H".
-          simpl. wp_unfold.
-          simpl. wp_case_inr. (* TODO: same comment *)
-          wp_let.
-          wp_proj.
-          wp_bind (CAS _ _ _).
-          iInv N as "Hstack" "Hclose".
-          iDestruct "Hstack" as (l''' v''') "[>% [Hl'' Hstack]]". simplify_eq/=.
-          destruct (decide (v''' = FoldV (InjRV (h, t))%V)) as [Heq | Heq]; subst.
-          ++ (* If nothing has changed, the cas succeeds *)
-            wp_cas_suc.
-            iDestruct (is_stack_unfold with "Hstack") as "[Hstack | Hstack]".
-            { iDestruct "Hstack" as "%"; discriminate. }
-            iDestruct "Hstack" as (h' t') "[% [HP Hstack]]". simplify_eq/=.
-            iMod ("Hclose" with "[Hl'' Hstack]").
-            { iExists l''', t'; iFrame; auto. }
-            iModIntro.
-            wp_if. 
-            wp_proj. 
-            iApply wp_value. iLeft; auto.
-          ++ (* The case in which we fail *)
-            wp_cas_fail.
-            iMod ("Hclose" with "[Hl'' Hstack]").
-            iExists l''', v'''; iFrame; auto.
-            iModIntro.
-            wp_if.
-            (* Now we use our IH to loop *)
-            iApply "IH".
-    (* The verification of push. This is actually markedly simpler. *)
-    - iIntros (v) "!# HP /=".
-      (* We grab an IH to be used in the case that we loop *)
-      iLöb as "IH" forall (v).
-      wp_rec.
-      wp_rec.
-      wp_bind (put_mail _ _).
-      iApply (put_mail_works P with "Hinv HP").
-      iIntros (v') "Hv'".
-      iDestruct "Hv'" as "[H | H]".
-      * iDestruct "H" as (v'') "[% HP]"; subst.
-        simpl. wp_case. (* TODO: same comment here *)
-        wp_let.
-        wp_bind (! _)%E.
-        iInv N as "Hstack" "Hclose".
-        iDestruct "Hstack" as (l'' v') "[>% [Hl' Hstack]]". simplify_eq/=.
-        wp_load.
-        iMod ("Hclose" with "[Hl' Hstack]").
-        { by (iExists l'', v'; iFrame). }
+        wp_if. iApply