From 6f1bdd8f7113b4cfaf2dc8855ea896ba2631c51f Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 2 Apr 2019 15:28:21 +0200
Subject: [PATCH] Updated receive specifications to use persistent view shift
 instead of fixpoint

---
 theories/channel.v | 23 +++++------------------
 1 file changed, 5 insertions(+), 18 deletions(-)

diff --git a/theories/channel.v b/theories/channel.v
index 130f48e..4c33c28 100644
--- a/theories/channel.v
+++ b/theories/channel.v
@@ -284,23 +284,11 @@ Section channel.
         by iApply "HΦ".
   Qed.
 
-  Definition recv_vs_rec E γ c s Φ vs :=
-    (|={⊤,E}=> ∃ ls rs,
-      is_chan γ c ls rs ∗
-        ((try_recv_upd_fail γ c ls rs s ={E,⊤}=∗ ▷ vs) ∗
-         (∀ v, try_recv_upd_succ γ c ls rs s v ={E,⊤}=∗ Φ v)))%I.
-
-  Global Instance recv_vs_rec_contractive E γ c s Φ :
-    Contractive (recv_vs_rec E γ c s Φ).
-  Proof.
-    intros n P Q Heq.
-    rewrite /recv_vs_rec.
-    do 9 f_equiv.
-    by apply later_contractive.
-  Qed.
-
   Definition recv_vs E γ c s Φ :=
-    fixpoint (recv_vs_rec E γ c s Φ).
+    (□ (|={⊤,E}=> ∃ ls rs,
+      is_chan γ c ls rs ∗
+        ((try_recv_upd_fail γ c ls rs s ={E,⊤}=∗ True) ∗
+         (∀ v, try_recv_upd_succ γ c ls rs s v ={E,⊤}=∗ Φ v))))%I.
 
   Lemma recv_spec Φ E γ c s :
     is_side s →
@@ -308,10 +296,9 @@ Section channel.
     recv_vs E γ c s Φ -∗
     WP recv c s {{ Φ }}.
   Proof.
-    iIntros (Hside) "#Hc HΦ".
+    iIntros (Hside) "#Hc #HΦ".
     rewrite /recv.
     iLöb as "IH".
-    iDestruct (fixpoint_unfold with "HΦ") as "HΦ".
     wp_apply (try_recv_spec with "Hc")=> //.
     iMod "HΦ" as (ls rs) "[Hchan [HΦfail HΦsucc]]".
     iModIntro.
-- 
GitLab