From 8369282388809237fcaa3aba142481f69deaf658 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 21 Jun 2019 13:35:43 +0200
Subject: [PATCH] Restore branching.

Also weaken some specs by adding laters.
---
 _CoqProject                      |  1 -
 theories/channel/branching.v     | 78 --------------------------------
 theories/channel/proto_channel.v | 41 +++++++++++++++--
 theories/examples/list_sort.v    |  8 ++--
 4 files changed, 42 insertions(+), 86 deletions(-)
 delete mode 100644 theories/channel/branching.v

diff --git a/_CoqProject b/_CoqProject
index 86b78cf..4ce4b8b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,7 +6,6 @@ theories/utils/list.v
 theories/channel/channel.v
 theories/channel/proto_model.v
 theories/channel/proto_channel.v
-theories/channel/branching.v
 theories/examples/proofs_enc.v
 theories/examples/branching_proofs.v
 theories/examples/list_sort.v
diff --git a/theories/channel/branching.v b/theories/channel/branching.v
deleted file mode 100644
index d278168..0000000
--- a/theories/channel/branching.v
+++ /dev/null
@@ -1,78 +0,0 @@
-From iris.heap_lang Require Import proofmode notation.
-From osiris.channel Require Export proto_channel.
-
-Definition TSB {PROP : bi} (a : action)
-    (prot1 prot2 : proto val PROP) : proto val PROP :=
-  TSR' a (λ _, True)%I (λ v, if v : bool then prot1 else prot2).
-Global Typeclasses Opaque TSB.
-Infix "<+>" := (TSB Send) (at level 85) : proto_scope.
-Infix "<&>" := (TSB Receive) (at level 85) : proto_scope.
-
-Definition select : val := λ: "c" "s" "b", send "c" "s" "b".
-Definition branch : val := λ: "c" "s" "b1" "b2",
-  if: recv "c" "s" then "b1" else "b2".
-(* TODO: This notation should be fixed *)
-Notation "'branch:' c @ s 'left' e1 'right' e2" :=
-  (branch c s (λ: <>, e1)%E (λ: <>, e2)%E #())
-    (at level 200, c, s, e1, e2 at level 200) : expr_scope.
-
-Global Instance is_dual_tsb {PROP : bi} a1 a2
-    (proto1 proto1' proto2 proto2' : proto val PROP) :
-  IsDualAction a1 a2 →
-  IsDualProto proto1 proto1' → IsDualProto proto2 proto2' →
-  IsDualProto (TSB a1 proto1 proto2) (TSB a2 proto1' proto2').
-Proof.
-  rewrite /IsDualAction.
-  rewrite /IsDualProto.
-  intros Ha Hst1 Hst2.
-  destruct a1.
-  - simpl.
-    simpl in Ha. rewrite -Ha.
-    rewrite -(proto_force_eq (dual_proto _)).
-    constructor.
-    f_equiv.
-    f_equiv.
-    destruct (val_decode a).
-    by destruct b. apply is_dual_end.
-  - simpl.
-    simpl in Ha. rewrite -Ha.
-    rewrite -(proto_force_eq (dual_proto _)).
-    constructor.
-    f_equiv.
-    f_equiv.
-    destruct (val_decode a).
-    by destruct b.
-    apply is_dual_end.
-Qed.
-
-Section branching_specs.
-  Context `{!heapG Σ, !logrelG val Σ} (N : namespace).
-
-  Lemma select_st_spec proto1 proto2 γ c s (b : side) :
-    {{{ ⟦ c @ s : proto1 <+> proto2 ⟧{N,γ} }}}
-      select c #s #b
-    {{{ RET #(); ⟦ c @ s : (if b then proto1 else proto2) ⟧{N,γ} }}}.
-  Proof.
-    iIntros (Φ) "Hproto HΦ".
-    wp_pures. wp_lam.
-    wp_pures. rewrite /TSB.
-    wp_apply (send_st_spec (A:=bool) with "[$Hproto //]"); iIntros "Hstl".
-    iApply "HΦ". by destruct b.
-  Qed.
-
-  Lemma branch_st_spec proto1 proto2 γ c s (b1 b2 : val) :
-    {{{ ⟦ c @ s : proto1 <&> proto2 ⟧{N,γ} }}}
-      branch c #s b1 b2
-    {{{ v, RET v; (⌜v = b1%V⌝ ∧ ⟦ c @ s : proto1 ⟧{N,γ}) ∨
-                  (⌜v = b2%V⌝ ∧ ⟦ c @ s : proto2 ⟧{N,γ})}}}.
-  Proof.
-    iIntros (Φ').
-    iIntros "Hproto HΦ'".
-    wp_pures.
-    wp_lam. rewrite /TSB. simpl.
-    wp_apply (recv_st_spec (A:=bool) with "[$Hproto //]").
-    iIntros ([]) "[Hstl _]".
-    - wp_pures. iApply ("HΦ'"). eauto with iFrame.
-    - wp_pures. iApply ("HΦ'"). eauto with iFrame.
-  Qed.
-End branching_specs.
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 2450756..3e2292c 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -53,6 +53,7 @@ Notation "'MSG' v {{ P }}; p" :=
 Notation "'MSG' v ; p" :=
   (proto_payload v True p) (at level 20, v at level 20, p at level 200) : proto_cont_scope.
 
+(** Dual *)
 Definition proto_dual {Σ} (p : iProto Σ) : iProto Σ :=
   proto_map action_dual cid cid p.
 Arguments proto_dual {_} _%proto.
@@ -68,6 +69,13 @@ Class IsProtoDual {Σ} (p1 p2 : iProto Σ) :=
 Class IsProtoContDual {Σ X} (pc1 pc2 : iProto_cont Σ X) :=
   is_dual_proto_cont x : prod_map id proto_dual (tele_app pc1 x) ≡ tele_app pc2 x.
 
+(** Branching *)
+Definition iProto_branch {Σ} (a : action)(p1 p2 : iProto Σ) : iProto Σ :=
+  iProto_message a (∃ b : bool, MSG #b {{ True }}; if b then p1 else p2).
+Typeclasses Opaque iProto_branch.
+Infix "<+>" := (iProto_branch Send) (at level 85) : proto_scope.
+Infix "<&>" := (iProto_branch Receive) (at level 85) : proto_scope.
+
 (** Invariants *)
 Fixpoint proto_eval `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
   match vs with
@@ -167,6 +175,14 @@ Section proto.
     apply tforall_forall. apply Hpc.
   Qed.
 
+  Global Instance is_proto_dual_branch a1 a2 (p1 p2 p1' p2' : iProto Σ) :
+    IsActionDual a1 a2 → IsProtoDual p1 p1' → IsProtoDual p2 p2' →
+    IsProtoDual (iProto_branch a1 p1 p2) (iProto_branch a2 p1' p2').
+  Proof.
+    intros. apply is_proto_dual_message,
+      is_proto_cont_dual_exist; last (intros []); apply _.
+  Qed.
+
   Global Instance proto_eval_ne : NonExpansive2 (proto_eval vs).
   Proof. induction vs; solve_proper. Qed.
   Global Instance proto_eval_proper vs : Proper ((≡) ==> (≡) ==> (≡)) (proto_eval vs).
@@ -423,7 +439,7 @@ Section proto.
     (∃.. x : X,
       ⌜ v = (tele_app pc x).1.1 ⌝ ∗
       (tele_app pc x).1.2 ∗
-      (c ↣ (tele_app pc x).2 @ N -∗ Ψ #())) -∗
+      ▷ (c ↣ (tele_app pc x).2 @ N -∗ Ψ #())) -∗
     WP send c v {{ Ψ }}.
   Proof.
     iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]".
@@ -464,12 +480,31 @@ Section proto.
 
   Lemma recv_proto_spec {X} Ψ c (pc : iProto_cont Σ X) :
     c ↣ <?> pc @ N -∗
-    (∀.. x : X, c ↣ (tele_app pc x).2 @ N -∗
-                (tele_app pc x).1.2 -∗ Ψ (tele_app pc x).1.1) -∗
+    ▷ (∀.. x : X, c ↣ (tele_app pc x).2 @ N -∗
+                  (tele_app pc x).1.2 -∗ Ψ (tele_app pc x).1.1) -∗
     WP recv c {{ Ψ }}.
   Proof.
     iIntros "Hc H". iApply (recv_proto_spec_packed with "[$]").
     iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
     iApply ("H" with "[$] [$]").
   Qed.
+
+  Lemma select_spec c b p1 p2 :
+    {{{ c ↣ p1 <+> p2 @ N }}}
+      send c #b
+    {{{ RET #(); c ↣ (if b : bool then p1 else p2) @ N }}}.
+  Proof.
+    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
+    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
+  Qed.
+
+  Lemma branch_spec c p1 p2  :
+    {{{ c ↣ p1 <&> p2 @ N }}}
+      recv c
+    {{{ b, RET #b; c ↣ if b : bool then p1 else p2 @ N }}}.
+  Proof.
+    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
+    iApply (recv_proto_spec with "Hc"); simpl.
+    iIntros "!>" (b) "Hc _". by iApply "HΨ".
+  Qed.
 End proto. 
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 7aafed1..ad3f9c6 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -123,13 +123,13 @@ Section list_sort.
     wp_apply (wp_fork with "[Hcz1]").
     { iNext. wp_apply ("IH" with "Hcz1"); auto. }
     wp_apply (send_proto_spec with "Hcy2"); simpl.
-    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} Hcy2".
+    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcy2".
     wp_apply (send_proto_spec with "Hcy2"); simpl.
-    iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} Hcy2".
+    iExists xs1, l1, vs1. iSplit; first done. iIntros "{$Hl1 $HI1} !> Hcy2".
     wp_apply (send_proto_spec with "Hcz2"); simpl.
-    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} Hcz2".
+    iExists _, I, R, _, _, cmp. iSplit; first done. iIntros "{$Hcmp} !> Hcz2".
     wp_apply (send_proto_spec with "Hcz2"); simpl.
-    iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} Hcz2".
+    iExists xs2, l2, vs2. iSplit; first done. iIntros "{$Hl2 $HI2} !> Hcz2".
     wp_apply (recv_proto_spec with "Hcy2"); simpl.
     iIntros (ys1 ws1) "_". iDestruct 1 as (??) "[Hl1 HI1]".
     wp_apply (recv_proto_spec with "Hcz2"); simpl.
-- 
GitLab