From 46799c39706a498968c17df7d5977747eee8b7a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Jul 2019 15:39:01 +0200
Subject: [PATCH] More powerful rule for allocation of channels.

---
 theories/channel/proto_channel.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index ab8ca5d..0326743 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -697,15 +697,14 @@ Section proto.
   Qed.
 
   (** Specifications of send and receive *)
-  Lemma new_chan_proto_spec p :
+  Lemma new_chan_proto_spec :
     {{{ True }}}
       new_chan #()
-    {{{ c1 c2, RET (c1,c2); c1 ↣ p @ N ∗ c2 ↣ iProto_dual p @ N }}}.
+    {{{ c1 c2, RET (c1,c2); (∀ p, |={⊤}=> c1 ↣ p @ N ∗ c2 ↣ iProto_dual p @ N) }}}.
   Proof.
     iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
-    iIntros (c1 c2 γ) "(Hc & Hl & Hr)".
-    iMod (proto_init ⊤ γ c1 c2 p with "Hc Hl Hr") as "[Hp Hdp]".
-    iApply "HΨ". by iFrame.
+    iIntros (c1 c2 γ) "(Hc & Hl & Hr)". iApply "HΨ"; iIntros "!>" (p).
+    iApply (proto_init ⊤ γ c1 c2 p with "Hc Hl Hr").
   Qed.
 
   Lemma start_chan_proto_spec p Ψ (f : val) :
@@ -714,7 +713,8 @@ Section proto.
     WP start_chan f {{ Ψ }}.
   Proof.
     iIntros "Hfork HΨ". wp_lam.
-    wp_apply (new_chan_proto_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
+    wp_apply (new_chan_proto_spec with "[//]"); iIntros (c1 c2) "Hc".
+    iMod ("Hc" $! p) as "[Hc1 Hc2]".
     wp_apply (wp_fork with "[Hfork Hc2]").
     { iNext. wp_apply ("Hfork" with "Hc2"). }
     wp_pures. iApply ("HΨ" with "Hc1").
-- 
GitLab