From 7c7bc0604ed758dea61ffb00dbb16cb435d93356 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 18 Jun 2018 18:12:45 +0200 Subject: [PATCH] add abstract HoCAP-style spec and show that it implies the logically atomic one --- _CoqProject | 1 + theories/logatom_stack/hocap_spec.v | 230 ++++++++++++++++++++++++++++ theories/logatom_stack/spec.v | 4 +- theories/logatom_stack/stack.v | 57 ++++--- 4 files changed, 261 insertions(+), 31 deletions(-) create mode 100644 theories/logatom_stack/hocap_spec.v diff --git a/_CoqProject b/_CoqProject index 6668001..76e693f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -83,3 +83,4 @@ theories/hocap/parfib.v theories/logatom_stack/stack.v theories/logatom_stack/spec.v +theories/logatom_stack/hocap_spec.v diff --git a/theories/logatom_stack/hocap_spec.v b/theories/logatom_stack/hocap_spec.v new file mode 100644 index 0000000..1ef0a8b --- /dev/null +++ b/theories/logatom_stack/hocap_spec.v @@ -0,0 +1,230 @@ +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. diff --git a/theories/logatom_stack/spec.v b/theories/logatom_stack/spec.v index 263a61e..b258c3b 100644 --- a/theories/logatom_stack/spec.v +++ b/theories/logatom_stack/spec.v @@ -25,12 +25,12 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack { push_spec N γs s e v : IntoVal e v → is_stack N γs s -∗ - <<< ∀ l, stack_content γs l >>> + <<< ∀ 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, stack_content γs l >>> + <<< ∀ l : list val, stack_content γs l >>> pop s @ ⊤∖↑N <<< stack_content γs (tail l), RET match l with [] => NONEV | v :: _ => SOMEV v end >>>; diff --git a/theories/logatom_stack/stack.v b/theories/logatom_stack/stack.v index ce4ed56..94c9e61 100644 --- a/theories/logatom_stack/stack.v +++ b/theories/logatom_stack/stack.v @@ -186,25 +186,25 @@ Section stack. Lemma push_spec γs s e v : IntoVal e v → is_stack γs s -∗ - <<< ∀ l, stack_content γs l >>> + <<< ∀ l : list val, stack_content γs l >>> push (s, e) @ ⊤∖↑N <<< stack_content γs (v::l), RET #() >>>. Proof. - intros <-. iIntros "#Hinv" (Q Φ) "HQ AU". + 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 "[HQ AU]"); first by iAccu. + 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 "!> [HQ AU]". clear offer_rep l. + 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 with "[HQ]"); [by destruct stack_rep|iAccu|]. + 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↦". @@ -219,15 +219,15 @@ Section stack. 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 "Q". wp_if. by iApply "HΦ". + 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 "HQ". wp_if. + 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 with "[HQ]"); first by iAccu. + 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. @@ -238,33 +238,33 @@ Section stack. { iClear "Hoffer". iExists _, (Some (v, st_loc)), _. iFrame. rewrite /is_offer /=. iExists _, _, _. iFrame "AU_back Hoinv". done. } clear stack_rep offer_rep l. - iIntros "!> HQ". wp_let. + iIntros "!> _". wp_let. (* Retract the offer. *) - wp_proj. wp_apply (store_spec with "[HQ]"); first by iAccu. + 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. iIntros "?". iSplitR "Htok". { iClear "Hoffer". iExists _, None, _. iFrame. done. } - iIntros "!> HQ". wp_seq. + iIntros "!> _". wp_seq. clear stack_rep offer_rep l. (* See if someone took it. *) - wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. + wp_apply cas_spec; [done|iAccu|]. iAuIntro. iInv offerN as (offer_st) "[>Hst↦ Hst]". iAaccIntro with "Hst↦"; first by eauto 10 with iFrame. iIntros "Hst↦". destruct offer_st; simpl. + (* Offer was still pending, and we revoked it. Loop around and try again. *) iModIntro. iSplitR "Hst". { iNext. iExists OfferRevoked. iFrame. } - iIntros "HQ". + iIntros "_". iDestruct ("AU_back" with "Hst") as ">AU {AU_back Hoinv}". clear AU_later. - wp_if. iApply ("IH" with "HQ AU"). + wp_if. iApply ("IH" with "AU"). + (* Offer revoked by someone else? Impossible! *) iDestruct "Hst" as ">Hst". iDestruct (own_valid_2 with "Htok Hst") as %[]. + (* Offer got accepted by someone, awesome! We are done. *) iModIntro. iSplitR "Hst". { iNext. iExists OfferAcked. iFrame. } - iIntros "HQ". wp_if. by iApply "Hst". + iIntros "_". wp_if. by iApply "Hst". + (* Offer got acked by someone else? Impossible! *) iDestruct "Hst" as ">Hst". iDestruct (own_valid_2 with "Htok Hst") as %[]. @@ -277,12 +277,12 @@ Section stack. <<< stack_content γs (tail l), RET match l with [] => NONEV | v :: _ => SOMEV v end >>>. Proof. - iIntros "#Hinv" (Q Φ) "HQ AU". + iIntros "#Hinv". iApply wp_atomic_intro. iIntros (Φ) "AU". iDestruct "Hinv" as (head offer) "[% #Hinv]". subst s. iLöb as "IH". wp_let. wp_proj. (* Load the old head *) - wp_apply (load_spec with "[HQ]"); first by iAccu. + wp_apply load_spec; first by iAccu. iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)". iAaccIntro with "H↦"; first by eauto 10 with iFrame. iIntros "?". destruct l as [|v l]; simpl. @@ -294,16 +294,16 @@ Section stack. %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. iMod ("Hclose" with "Hl'") as "HΦ". iSplitR "HΦ"; first by eauto 10 with iFrame. - iIntros "!> HQ". wp_match. by iApply "HΦ". + iIntros "!> _". wp_match. by iApply "HΦ". - (* Non-empty list, let's try to pop. *) iDestruct "Hlist" as (tail q rep) "[>% [[Htail Htail2] Hlist]]". subst stack_rep. iSplitR "AU Htail"; first by eauto 15 with iFrame. clear offer_rep l. - iIntros "!> HQ". wp_match. + iIntros "!> _". wp_match. wp_apply (atomic_wp_seq $! (load_spec _) with "Htail"). iIntros "Htail". wp_let. wp_proj. wp_proj. (* CAS to change the head *) - wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. + wp_apply cas_spec; [done|iAccu|]. iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hrem)". iAaccIntro with "H↦"; first by eauto 10 with iFrame. iIntros "H↦". change (InjRV #tail) with (stack_elem_to_val (Some tail)). @@ -323,23 +323,22 @@ Section stack. { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. } iMod ("Hclose" with "Hl'") as "HΦ {Htail Htail'}". iSplitR "HΦ"; first by eauto 10 with iFrame. - iIntros "!> HQ". clear q' q offer_rep l. + iIntros "!> _". clear q' q offer_rep l. wp_if. wp_proj. by iApply "HΦ". + (* CAS failed. Go on looking for an offer. *) iSplitR "AU"; first by eauto 10 with iFrame. - iIntros "!> HQ". wp_if. clear rep stack_rep offer_rep l q tail v. + iIntros "!> _". wp_if. clear rep stack_rep offer_rep l q tail v. wp_proj. (* Load the offer pointer. *) - (* FIXME: [wp_apply (load_spec with "[HQ AU]"); first by iAccu.] here triggers an anomaly. *) - wp_apply (load_spec with "[HQ]"); first by iAccu. + wp_apply load_spec; first by iAccu. iAuIntro. iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & >Hoff↦ & #Hoff)". iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame. iIntros "Hoff↦". iSplitR "AU"; first by eauto 10 with iFrame. - iIntros "!> HQ". destruct offer_rep as [[v offer_st_loc]|]; last first. - { (* No offer, just loop. *) wp_match. iApply ("IH" with "HQ AU"). } + iIntros "!> _". destruct offer_rep as [[v offer_st_loc]|]; last first. + { (* No offer, just loop. *) wp_match. iApply ("IH" with "AU"). } clear l stack_rep. wp_match. wp_proj. (* CAS to accept the offer. *) - wp_apply (cas_spec with "[HQ]"); [done|iAccu|]. simpl. + wp_apply cas_spec; [done|iAccu|]. simpl. iAuIntro. iDestruct "Hoff" as (Poff Qoff γo) "[#Hoinv #AUoff]". iInv offerN as (offer_st) "[>Hoff↦ Hoff]". iAaccIntro with "Hoff↦"; first by eauto 10 with iFrame. @@ -347,7 +346,7 @@ Section stack. destruct (decide (#(offer_state_rep offer_st) = #0)) as [Heq|_]; last first. { (* CAS failed, we don't do a thing. *) iSplitR "AU"; first by eauto 10 with iFrame. - iIntros "!> HQ". wp_if. iApply ("IH" with "HQ AU"). } + iIntros "!> _". wp_if. iApply ("IH" with "AU"). } (* CAS succeeded! We accept and complete the offer. *) destruct offer_st; try done; []. clear Heq. iMod ("AUoff" with "Hoff") as "{AUoff IH} AUoff". @@ -366,7 +365,7 @@ Section stack. iMod ("Hclose" with "Hl'") as "HΦ". iSplitR "Hoff↦ HQoff HΦ"; first by eauto 10 with iFrame. iSplitR "HΦ". { iIntros "!> !> !>". iExists OfferAccepted. iFrame. } - iIntros "!> !> HQ". wp_if. wp_proj. by iApply "HΦ". + iIntros "!> !> _". wp_if. wp_proj. by iApply "HΦ". Qed. End stack. -- GitLab