diff --git a/_CoqProject b/_CoqProject
index 5539986c7fa1d95c3895df822db38d233555eb3c..de64737d4ae659a03f0246cb09dba0a0764f8e08 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,12 +1,13 @@
-Q theories actris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
+theories/utils/skip.v
theories/utils/llist.v
theories/utils/compare.v
theories/utils/contribution.v
theories/utils/group.v
-theories/channel/channel.v
theories/channel/proto_model.v
-theories/channel/proto_channel.v
+theories/channel/proto.v
+theories/channel/channel.v
theories/channel/proofmode.v
theories/examples/basics.v
theories/examples/sort.v
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index a31942624d54d36d6cdb83c098467095a69a91ff..1fe1e31ab3c8ae6186b0cc4c1ab121da157afc2f 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -1,7 +1,14 @@
(** This file contains the definition of the channels, encoded as a pair of
-lock-protected buffers, and their primitive proof rules. Actris's proof rules
-for channels in terms of dependent separation protocols can be found in the file
-[theories/channel/proto_channel.v].
+lock-protected buffers, and their primitive proof rules. Moreover:
+
+- It defines the connective [c ↣ prot] for ownership of channel endpoints,
+ which describes that channel endpoint [c] adheres to protocol [prot].
+- It proves Actris's specifications of [send] and [receive] w.r.t. dependent
+ separation protocols.
+
+An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
+[prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
+file.
In this file we define the three message-passing connectives:
@@ -10,32 +17,13 @@ In this file we define the three message-passing connectives:
polarity of the endpoints.
- [send] takes an endpoint and adds an element to the first buffer.
- [recv] performs a busy loop until there is something in the second buffer,
- which it pops and returns, locking during each peek.
-
-The logically-atomic basic (i.e. non dependent separation protocol)
-proof rules [new_chan_spec], [send_spec] and [recv_spec] are defined in terms
-of the logical connectives [is_chan] and [chan_own]:
-
-- [is_chan γ v1 v2] is a persistent proposition expressing that [v1] and [v2]
- are the endpoints of a channel with logical name [γ].
-- [chan_own γ s vs] is an exclusive proposition expressing the buffer of side
- [s] ([Left] or [Right]) has contents [vs].
-
-Note that the specifications include 3 laters [â–·] to account for the three
-levels of indirection due to step-indexing in the model of dependent separation
-protocols. *)
+ which it pops and returns, locking during each peek.*)
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
-From iris.heap_lang Require Import lifting.
-From iris.algebra Require Import excl_auth list.
-From actris.utils Require Import llist.
+From actris.channel Require Export proto.
+From actris.utils Require Import llist skip.
Set Default Proof Using "Type".
-Inductive side := Left | Right.
-Instance side_inhabited : Inhabited side := populate Left.
-Definition side_elim {A} (s : side) (l r : A) : A :=
- match s with Left => l | Right => r end.
-
(** * The definition of the message-passing connectives *)
Definition new_chan : val :=
λ: <>,
@@ -44,12 +32,17 @@ Definition new_chan : val :=
let: "lk" := newlock #() in
((("l","r"),"lk"), (("r","l"),"lk")).
+Definition start_chan : val := λ: "f",
+ let: "cc" := new_chan #() in
+ Fork ("f" (Snd "cc"));; Fst "cc".
+
Definition send : val :=
λ: "c" "v",
let: "lk" := Snd "c" in
acquire "lk";;
let: "l" := Fst (Fst "c") in
lsnoc "l" "v";;
+ skipN (llength (Snd (Fst "c")));; (* Later stripping *)
release "lk".
Definition try_recv : val :=
@@ -68,156 +61,251 @@ Definition recv : val :=
end.
(** * Setup of Iris's cameras *)
+Definition chanN := nroot .@ "chan".
+
Class chanG Σ := {
chanG_lockG :> lockG Σ;
- chanG_authG :> inG Σ (excl_authR (listO valO));
+ chanG_protoG :> protoG Σ val;
}.
-Definition chanΣ : gFunctors :=
- #[ lockΣ; GFunctor (excl_authR (listO valO)) ].
+Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
Proof. solve_inG. Qed.
+Record chan_name := ChanName {
+ chan_lock_name : gname;
+ chan_proto_name : proto_name;
+}.
+
+(** * Definition of the mapsto connective *)
+Notation iProto Σ := (iProto Σ val).
+
+Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
+ (c : val) (p : iProto Σ) : iProp Σ :=
+ ∃ γ s (l r : loc) (lk : val),
+ ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌠∗
+ is_lock chanN (chan_lock_name γ) lk (∃ vsl vsr,
+ llist sbi_internal_eq l vsl ∗
+ llist sbi_internal_eq r vsr ∗
+ iProto_ctx (chan_proto_name γ) vsl vsr) ∗
+ iProto_own (chan_proto_name γ) s p.
+Definition iProto_mapsto_aux : seal (@iProto_mapsto_def). by eexists. Qed.
+Definition iProto_mapsto := iProto_mapsto_aux.(unseal).
+Definition iProto_mapsto_eq :
+ @iProto_mapsto = @iProto_mapsto_def := iProto_mapsto_aux.(seal_eq).
+Arguments iProto_mapsto {_ _ _} _ _%proto.
+Instance: Params (@iProto_mapsto) 4 := {}.
+Notation "c ↣ p" := (iProto_mapsto c p)
+ (at level 20, format "c ↣ p").
+
+Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
+ (p1 p2 : iProto Σ) : iProto Σ :=
+ (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
+Typeclasses Opaque iProto_branch.
+Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
+Instance: Params (@iProto_branch) 2 := {}.
+Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
+Infix "<{ P1 }&{ P2 }>" := (iProto_branch Receive P1 P2) (at level 85) : proto_scope.
+Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
+Infix "<&{ P2 }>" := (iProto_branch Receive True P2) (at level 85) : proto_scope.
+Infix "<{ P1 }+>" := (iProto_branch Send P1 True) (at level 85) : proto_scope.
+Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope.
+Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
+Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
+
Section channel.
- Context `{!heapG Σ, !chanG Σ} (N : namespace).
-
- Record chan_name := Chan_name {
- chan_lock_name : gname;
- chan_l_name : gname;
- chan_r_name : gname
- }.
-
- (** * The logical connectives *)
- Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
- (∃ ls rs,
- llist sbi_internal_eq l ls ∗ own (chan_l_name γ) (â—E ls) ∗
- llist sbi_internal_eq r rs ∗ own (chan_r_name γ) (â—E rs))%I.
- Typeclasses Opaque chan_inv.
-
- Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
- (∃ (l r : loc) (lk : val),
- ⌜ c1 = ((#l, #r), lk)%V ∧ c2 = ((#r, #l), lk)%V ⌠∗
- is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
-
- Global Instance is_chan_persistent : Persistent (is_chan γ c1 c2).
- Proof. by apply _. Qed.
-
- Lemma chan_inv_alt s γ l r :
- chan_inv γ l r ⊣⊢ ∃ ls rs,
- llist sbi_internal_eq (side_elim s l r) ls ∗
- own (side_elim s chan_l_name chan_r_name γ) (â—E ls) ∗
- llist sbi_internal_eq (side_elim s r l) rs ∗
- own (side_elim s chan_r_name chan_l_name γ) (â—E rs).
+ Context `{!heapG Σ, !chanG Σ}.
+ Implicit Types p : iProto Σ.
+ Implicit Types TT : tele.
+
+ Global Instance iProto_mapsto_ne c : NonExpansive (iProto_mapsto c).
+ Proof. rewrite iProto_mapsto_eq. solve_proper. Qed.
+ Global Instance iProto_mapsto_proper c : Proper ((≡) ==> (≡)) (iProto_mapsto c).
+ Proof. apply (ne_proper _). Qed.
+
+ Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ iProto_le p1 p2 -∗ c ↣ p2.
Proof.
- destruct s; rewrite /chan_inv //=.
- iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
+ rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
+ iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+ by iApply (iProto_own_le with "H").
Qed.
- Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
- own (side_elim s chan_l_name chan_r_name γ) (◯E vs)%I.
+ Global Instance iProto_branch_contractive n a :
+ Proper (dist_later n ==> dist_later n ==>
+ dist_later n ==> dist_later n ==> dist n) (@iProto_branch Σ a).
+ Proof.
+ intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
+ apply iProto_message_contractive=> /= -[] //.
+ Qed.
+ Global Instance iProto_branch_ne n a :
+ Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_branch Σ a).
+ Proof.
+ intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
+ by apply iProto_message_ne=> /= -[].
+ Qed.
+ Global Instance iProto_branch_proper a :
+ Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_branch Σ a).
+ Proof.
+ intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
+ by apply iProto_message_proper=> /= -[].
+ Qed.
- (** * The proof rules *)
- Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
- Proof. by apply _. Qed.
+ Lemma iProto_dual_branch a P1 P2 p1 p2 :
+ iProto_dual (iProto_branch a P1 P2 p1 p2)
+ ≡ iProto_branch (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
+ Proof.
+ rewrite /iProto_branch iProto_dual_message /=.
+ by apply iProto_message_proper=> /= -[].
+ Qed.
+
+ Lemma iProto_app_branch a P1 P2 p1 p2 q :
+ (iProto_branch a P1 P2 p1 p2 <++> q)%proto
+ ≡ (iProto_branch a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
+ Proof.
+ rewrite /iProto_branch iProto_app_message.
+ by apply iProto_message_proper=> /= -[].
+ Qed.
- Lemma new_chan_spec :
+ (** ** Specifications of [send] and [recv] *)
+ Lemma new_chan_spec p :
{{{ True }}}
new_chan #()
- {{{ c1 c2 γ, RET (c1,c2); is_chan γ c1 c2 ∗ chan_own γ Left [] ∗ chan_own γ Right [] }}}.
+ {{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
+ Proof.
+ iIntros (Φ _) "HΦ". wp_lam.
+ wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (l) "Hl".
+ wp_apply (lnil_spec sbi_internal_eq with "[//]"); iIntros (r) "Hr".
+ iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
+ wp_apply (newlock_spec chanN (∃ vsl vsr,
+ llist sbi_internal_eq l vsl ∗ llist sbi_internal_eq r vsr ∗
+ iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
+ { iExists [], []. iFrame. }
+ iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
+ set (γ := ChanName γlk γp). iSplitL "Hcl".
+ - rewrite iProto_mapsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
+ - rewrite iProto_mapsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
+ Qed.
+
+ Lemma start_chan_spec p Φ (f : val) :
+ ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
+ ▷ (∀ c, c ↣ p -∗ Φ c) -∗
+ WP start_chan f {{ Φ }}.
+ Proof.
+ iIntros "Hfork HΦ". wp_lam.
+ wp_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
+ wp_apply (wp_fork with "[Hfork Hc2]").
+ { iNext. wp_apply ("Hfork" with "Hc2"). }
+ wp_pures. iApply ("HΦ" with "Hc1").
+ Qed.
+
+ Lemma send_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) (x : TT) :
+ {{{ c ↣ iProto_message Send pc ∗ (pc x).1.2 }}}
+ send c (pc x).1.1
+ {{{ RET #(); c ↣ (pc x).2 }}}.
+ Proof.
+ rewrite iProto_mapsto_eq. iIntros (Φ) "[Hc Hpc] HΦ". wp_lam; wp_pures.
+ iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+ wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+ iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
+ - iMod (iProto_send_l with "Hctx H Hpc") as "[Hctx H]".
+ wp_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
+ wp_apply (llength_spec with "[$Hr //]"); iIntros "Hr".
+ wp_apply skipN_spec.
+ wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
+ - iMod (iProto_send_r with "Hctx H Hpc") as "[Hctx H]".
+ wp_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
+ wp_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
+ wp_apply skipN_spec.
+ wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+ Qed.
+
+ (** A version written without Texan triples that is more convenient to use
+ (via [iApply] in Coq. *)
+ Lemma send_spec {TT} Φ c v (pc : TT → val * iProp Σ * iProto Σ) :
+ c ↣ iProto_message Send pc -∗
+ (∃.. x : TT,
+ ⌜ v = (pc x).1.1 ⌠∗ (pc x).1.2 ∗ ▷ (c ↣ (pc x).2 -∗ Φ #())) -∗
+ WP send c v {{ Φ }}.
+ Proof.
+ iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΦ]".
+ by iApply (send_spec_packed with "[$]").
+ Qed.
+
+ Lemma try_recv_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
+ {{{ c ↣ iProto_message Receive pc }}}
+ try_recv c
+ {{{ v, RET v; (⌜v = NONEV⌠∧ c ↣ iProto_message Receive pc) ∨
+ (∃ x : TT, ⌜v = SOMEV ((pc x).1.1)⌠∗ c ↣ (pc x).2 ∗ (pc x).1.2) }}}.
+ Proof.
+ rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+ iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+ wp_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+ iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & Hctx)". destruct s; simpl.
+ - wp_apply (lisnil_spec with "Hr"); iIntros "Hr".
+ destruct vsr as [|vr vsr]; wp_pures.
+ { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
+ iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
+ wp_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
+ iMod (iProto_recv_l with "Hctx H") as "H". wp_pures.
+ iDestruct "H" as (x ->) "(Hctx & H & Hpc)".
+ wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+ iFrame "Hpc". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
+ - wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
+ destruct vsl as [|vl vsl]; wp_pures.
+ { wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iApply "HΦ". iLeft. iSplit; [done|].
+ iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
+ wp_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
+ iMod (iProto_recv_r with "Hctx H") as "H". wp_pures.
+ iDestruct "H" as (x ->) "(Hctx & H & Hpc)".
+ wp_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+ iFrame "Hpc". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+ Qed.
+
+ Lemma recv_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
+ {{{ c ↣ iProto_message Receive pc }}}
+ recv c
+ {{{ x, RET (pc x).1.1; c ↣ (pc x).2 ∗ (pc x).1.2 }}}.
Proof.
- iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
- wp_lam.
- wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
- wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
- iMod (own_alloc (â—E [] â‹… â—¯E [])) as (lsγ) "[Hls Hls']".
- { by apply excl_auth_valid. }
- iMod (own_alloc (â—E [] â‹… â—¯E [])) as (rsγ) "[Hrs Hrs']".
- { by apply excl_auth_valid. }
- wp_apply (newlock_spec N (∃ ls rs,
- llist sbi_internal_eq l ls ∗ own lsγ (â—E ls) ∗
- llist sbi_internal_eq r rs ∗ own rsγ (â—E rs))%I with "[Hl Hr Hls Hrs]").
- { eauto 10 with iFrame. }
- iIntros (lk γlk) "#Hlk". wp_pures.
- iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
- rewrite /chan_inv /=. eauto 20 with iFrame.
+ iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
+ wp_apply (try_recv_spec_packed with "Hc"); iIntros (v) "[[-> H]|H]".
+ { wp_pures. by iApply ("IH" with "[$]"). }
+ iDestruct "H" as (x ->) "[Hc Hpc]". wp_pures. iApply "HΦ". iFrame.
Qed.
- Lemma send_spec Φ E γ c1 c2 v s :
- is_chan γ c1 c2 -∗
- (|={⊤,E}=> ∃ vs,
- chan_own γ s vs ∗
- ▷ (chan_own γ s (vs ++ [v]) ={E,⊤}=∗ ▷ ▷ Φ #())) -∗
- WP send (side_elim s c1 c2) v {{ Φ }}.
+ (** A version written without Texan triples that is more convenient to use
+ (via [iApply] in Coq. *)
+ Lemma recv_spec {TT} Φ c (pc : TT → val * iProp Σ * iProto Σ) :
+ c ↣ iProto_message Receive pc -∗
+ ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Φ (pc x).1.1) -∗
+ WP recv c {{ Φ }}.
Proof.
- iIntros "Hc HΦ". wp_lam; wp_pures.
- iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
- assert (side_elim s (#l, #r, lk)%V (#r, #l, lk)%V =
- ((#(side_elim s l r), #(side_elim s r l)), lk)%V) as -> by (by destruct s).
- wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
- iDestruct (chan_inv_alt s with "Hinv") as
- (vs ws) "(Hll & Hvs & Href' & Hws)".
- wp_seq. wp_bind (Fst (_,_)%V)%E.
- iMod "HΦ" as (vs') "[Hchan HΦ]".
- iDestruct (own_valid_2 with "Hvs Hchan") as %<-%excl_auth_agreeL.
- iMod (own_update_2 _ _ _ (â—E (vs ++ [v]) â‹… _) with "Hvs Hchan") as "[Hvs Hchan]".
- { apply excl_auth_update. }
- wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
- wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
- wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
- iApply (chan_inv_alt s).
- rewrite /llist. eauto 20 with iFrame.
+ iIntros "Hc H". iApply (recv_spec_packed with "[$]").
+ iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
+ iApply ("H" with "[$] [$]").
Qed.
- Lemma try_recv_spec Φ E γ c1 c2 s :
- is_chan γ c1 c2 -∗
- ((|={⊤,E}▷=> ▷ Φ NONEV) ∧
- (|={⊤,E}=> ∃ vs,
- chan_own γ s vs ∗
- ▷ (∀ v vs', ⌜ vs = v :: vs' ⌠-∗
- chan_own γ s vs' ={E,⊤,⊤}▷=∗ ▷ Φ (SOMEV v)))) -∗
- WP try_recv (side_elim s c2 c1) {{ Φ }}.
+ (** ** Specifications for branching *)
+ Lemma select_spec c (b : bool) P1 P2 p1 p2 :
+ {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
+ send c #b
+ {{{ RET #(); c ↣ (if b then p1 else p2) }}}.
Proof.
- iIntros "Hc HΦ". wp_lam; wp_pures.
- iDestruct "Hc" as (l r lk [-> ->]) "#Hlock"; wp_pures.
- assert (side_elim s (#r, #l, lk)%V (#l, #r, lk)%V =
- ((#(side_elim s r l), #(side_elim s l r)), lk)%V) as -> by (by destruct s).
- wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
- iDestruct (chan_inv_alt s with "Hinv")
- as (vs ws) "(Hll & Hvs & Href' & Hws)".
- wp_seq. wp_bind (Fst (_,_)%V)%E. destruct vs as [|v vs]; simpl.
- - iDestruct "HΦ" as "[>HΦ _]". wp_pures. iMod "HΦ"; iModIntro.
- wp_apply (lisnil_spec with "Hll"); iIntros "Hll". wp_pures.
- wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
- { iApply (chan_inv_alt s).
- rewrite /llist. eauto 10 with iFrame. }
- iIntros (_). by wp_pures.
- - iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
- iDestruct (own_valid_2 with "Hvs Hvs'") as %<-%excl_auth_agreeL.
- iMod (own_update_2 _ _ _ (â—E vs â‹… _) with "Hvs Hvs'") as "[Hvs Hvs']".
- { apply excl_auth_update. }
- wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
- wp_apply (lisnil_spec with "Hll"); iIntros "Hll". iMod "HΦ".
- wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
- wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
- { iApply (chan_inv_alt s).
- rewrite /llist. eauto 10 with iFrame. }
- iIntros (_). by wp_pures.
+ rewrite /iProto_branch. iIntros (Φ) "[Hc HP] HΦ".
+ iApply (send_spec with "Hc"); simpl; eauto with iFrame.
Qed.
- Lemma recv_spec Φ E γ c1 c2 s :
- is_chan γ c1 c2 -∗
- (|={⊤,E}=> ∃ vs,
- chan_own γ s vs ∗
- ▷ ∀ v vs', ⌜ vs = v :: vs' ⌠-∗
- chan_own γ s vs' ={E,⊤,⊤}▷=∗ ▷ Φ v) -∗
- WP recv (side_elim s c2 c1) {{ Φ }}.
+ Lemma branch_spec c P1 P2 p1 p2 :
+ {{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
+ recv c
+ {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
Proof.
- iIntros "#Hc HΦ". iLöb as "IH". wp_lam.
- wp_apply (try_recv_spec _ E with "Hc")=> //. iSplit.
- - iMod (fupd_intro_mask' _ E) as "Hclose"; first done. iIntros "!> !>".
- iMod "Hclose" as %_; iIntros "!> !>". wp_pures. by iApply "IH".
- - iMod "HΦ" as (vs) "[Hvs HΦ]". iExists vs; iFrame "Hvs".
- iIntros "!> !>" (v vs' ->) "Hvs".
- iMod ("HΦ" with "[//] Hvs") as "HΦ". iIntros "!> !>". iMod "HΦ".
- iIntros "!> !>". by wp_pures.
+ rewrite /iProto_branch. iIntros (Φ) "Hc HΦ".
+ iApply (recv_spec with "Hc"); simpl.
+ iIntros "!>" (b) "Hc HP". iApply "HΦ". iFrame.
Qed.
End channel.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index e09ca90a7d428d0487c1ea3a2491b9d537f52dbd..2eecbbdf19bc7e496bc820c36b48315f64ec247a 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -9,7 +9,7 @@ In addition to the tactics for symbolic execution, this file defines the tactic
recursive protocols are contractive. *)
From iris.heap_lang Require Export proofmode notation.
From iris.proofmode Require Export tactics.
-From actris Require Export proto_channel.
+From actris Require Export channel.
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
(** * Tactics for proving contractiveness of protocols *)
@@ -56,7 +56,7 @@ Notation ProtoUnfold p1 p2 := (∀ d pas q,
ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
Section classes.
- Context `{!proto_chanG Σ, !heapG Σ}.
+ Context `{!chanG Σ, !heapG Σ}.
Implicit Types p : iProto Σ.
Implicit Types TT : tele.
@@ -163,7 +163,7 @@ End classes.
(** * Symbolic execution tactics *)
(* TODO: Maybe strip laters from other hypotheses in the future? *)
-Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
+Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K
c p (pc : TT → val * iProp Σ * iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (iProto_message Receive pc) →
@@ -178,7 +178,7 @@ Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
Proof.
rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
- rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_proto_spec|f_equiv].
+ rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_spec|f_equiv].
rewrite -bi.later_intro bi_tforall_forall; apply bi.forall_intro=> x.
specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl.
@@ -241,7 +241,7 @@ Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_i
simple_intropattern(x8) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
-Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
+Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
c v p (pc : TT → val * iProp Σ * iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (iProto_message Send pc) →
@@ -262,7 +262,7 @@ Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ].
rewrite envs_lookup_sound //; simpl. rewrite -Hp.
- rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_proto_spec|f_equiv].
+ rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_spec|f_equiv].
rewrite bi_texist_exist -(bi.exist_intro x).
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
@@ -337,7 +337,7 @@ Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7; eexists x8) with pat.
-Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K
+Lemma tac_wp_branch `{!chanG Σ, !heapG Σ} Δ i j K
c p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (p1 <{P1}&{P2}> p2) →
@@ -385,7 +385,7 @@ Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_in
wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" := wp_branch as %_ | %_.
-Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K
+Lemma tac_wp_select `{!chanG Σ, !heapG Σ} Δ neg i js K
c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
ProtoNormalize false p [] (p1 <{P1}+{P2}> p2) →
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
new file mode 100644
index 0000000000000000000000000000000000000000..7e62bd6e729cdbd66341f86a9c1b3ed8c5f5b196
--- /dev/null
+++ b/theories/channel/proto.v
@@ -0,0 +1,961 @@
+(** This file defines the core of the Actris logic: It defines dependent
+separation protocols and the various operations on it like dual, append, and
+branching.
+
+Dependent separation protocols are defined by instantiating the parameterized
+version in [proto_model] with type of propositions [iProp] of Iris. We define
+ways of constructing instances of the instantiated type via two constructors:
+- [iProto_end], which is identical to [proto_end].
+- [iProto_message], which takes an action and a continuation to construct
+ the corresponding message protocols.
+
+For convenience sake, we provide the following notations:
+- [END], which is simply [iProto_end].
+- [<!> x1 .. xn, MSG v; {{ P }}; prot] and [<?> x1 .. xn, MSG v; {{ P }}; prot],
+ which construct an instance of [iProto_message] with the appropriate
+ continuation.
+
+Futhermore, we define the following operations:
+- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
+- [iProto_app], which appends two protocols as described in proto_model.v
+
+Lastly, relevant type classes instances are defined for each of the above
+notions, such as contractiveness and non-expansiveness, after which the
+specifications of the message-passing primitives are defined in terms of the
+protocol connectives. *)
+From iris.algebra Require Import excl_auth.
+From iris.bi Require Import telescopes.
+From iris.program_logic Require Import language.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import lib.own.
+From actris.channel Require Import proto_model.
+Export action.
+
+(** * Setup of Iris's cameras *)
+Class protoG Σ V :=
+ protoG_authG :>
+ inG Σ (excl_authR (laterO (proto (leibnizO V) (iPrePropO Σ) (iPrePropO Σ)))).
+
+Definition protoΣ V := #[
+ GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
+].
+Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
+Proof. solve_inG. Qed.
+
+(** * Types *)
+Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
+Delimit Scope proto_scope with proto.
+Bind Scope proto_scope with iProto.
+
+(** * Operators *)
+Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
+Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
+Definition iProto_end := iProto_end_aux.(unseal).
+Definition iProto_end_eq : @iProto_end = @iProto_end_def := iProto_end_aux.(seal_eq).
+Arguments iProto_end {_ _}.
+
+Program Definition iProto_message_def {Σ V} {TT : tele} (a : action)
+ (pc : TT → V * iProp Σ * iProto Σ V) : iProto Σ V :=
+ proto_message a (λ v, λne f, ∃ x : TT,
+ (** We need the later to make [iProto_message] contractive *)
+ ⌜ v = (pc x).1.1 ⌠∗
+ ▷ (pc x).1.2 ∗
+ f (Next (pc x).2))%I.
+Next Obligation. solve_proper. Qed.
+Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
+Definition iProto_message := iProto_message_aux.(unseal).
+Definition iProto_message_eq :
+ @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
+Arguments iProto_message {_ _ _} _ _%proto.
+Instance: Params (@iProto_message) 4 := {}.
+
+Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
+ (iProto_message
+ a
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
+ (at level 20, a at level 10, x1 binder, xn binder,
+ v at level 20, P, p at level 200) : proto_scope.
+Notation "< a > x1 .. xn , 'MSG' v ; p" :=
+ (iProto_message
+ a
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
+ (at level 20, a at level 10, x1 binder, xn binder,
+ v at level 20, p at level 200) : proto_scope.
+Notation "< a > 'MSG' v {{ P } } ; p" :=
+ (iProto_message
+ a
+ (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
+ (at level 20, a at level 10, v at level 20, P, p at level 200) : proto_scope.
+Notation "< a > 'MSG' v ; p" :=
+ (iProto_message
+ a
+ (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
+ (at level 20, a at level 10, v at level 20, p at level 200) : proto_scope.
+
+Notation "<!> x1 .. xn , 'MSG' v {{ P } } ; p" :=
+ (iProto_message
+ Send
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
+ (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
+Notation "<!> x1 .. xn , 'MSG' v ; p" :=
+ (iProto_message
+ Send
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
+ (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
+Notation "<!> 'MSG' v {{ P } } ; p" :=
+ (iProto_message
+ (TT:=TeleO)
+ Send
+ (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
+ (at level 20, v at level 20, P, p at level 200) : proto_scope.
+Notation "<!> 'MSG' v ; p" :=
+ (iProto_message
+ (TT:=TeleO)
+ Send
+ (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
+ (at level 20, v at level 20, p at level 200) : proto_scope.
+
+Notation "<?> x1 .. xn , 'MSG' v {{ P } } ; p" :=
+ (iProto_message
+ Receive
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
+ (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
+Notation "<?> x1 .. xn , 'MSG' v ; p" :=
+ (iProto_message
+ Receive
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
+ (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
+Notation "<?> 'MSG' v {{ P } } ; p" :=
+ (iProto_message
+ Receive
+ (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
+ (at level 20, v at level 20, P, p at level 200) : proto_scope.
+Notation "<?> 'MSG' v ; p" :=
+ (iProto_message
+ Receive
+ (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
+ (at level 20, v at level 20, p at level 200) : proto_scope.
+
+Notation "'END'" := iProto_end : proto_scope.
+
+(** * Operations *)
+Definition iProto_dual {Σ V} (p : iProto Σ V) : iProto Σ V :=
+ proto_map action_dual cid cid p.
+Arguments iProto_dual {_ _} _%proto.
+Instance: Params (@iProto_dual) 2 := {}.
+Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
+ if d then iProto_dual p else p.
+Arguments iProto_dual_if {_ _} _ _%proto.
+Instance: Params (@iProto_dual_if) 3 := {}.
+
+Definition iProto_app {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V := proto_app p1 p2.
+Arguments iProto_app {_ _} _%proto _%proto.
+Instance: Params (@iProto_app) 2 := {}.
+Infix "<++>" := iProto_app (at level 60) : proto_scope.
+
+(** * Auxiliary definitions and invariants *)
+Definition proto_eq_next {Σ V} (p : iProto Σ V) : laterO (iProto Σ V) -n> iPropO Σ :=
+ OfeMor (sbi_internal_eq (Next p)).
+
+(*
+The definition [iProto_le] generalizes the following inductive definition
+for subtyping on session types:
+
+ p1 <: p2 p1 <: p2
+---------- ---------------- ----------------
+end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2
+
+ p1 <: !B.p3 ?A.p3 <: p2
+----------------------------
+ ?A.p1 <: !B.p2
+
+Example:
+
+!R <: !R ?Q <: ?Q ?Q <: ?Q
+------------------- --------------
+?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
+------------------------------------
+ ?P.?Q.!R <: !R.?P.?Q
+*)
+Definition iProto_le_pre {Σ V}
+ (rec : iProto Σ V → iProto Σ V→ iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
+ (p1 ≡ proto_end ∗ p2 ≡ proto_end) ∨
+ ∃ a1 a2 pc1 pc2,
+ p1 ≡ proto_message a1 pc1 ∗
+ p2 ≡ proto_message a2 pc2 ∗
+ match a1, a2 with
+ | Receive, Receive =>
+ ∀ v p1', pc1 v (proto_eq_next p1') -∗
+ ◇ ∃ p2', ▷ rec p1' p2' ∗ pc2 v (proto_eq_next p2')
+ | Send, Send =>
+ ∀ v p2', pc2 v (proto_eq_next p2') -∗
+ ◇ ∃ p1', ▷ rec p1' p2' ∗ pc1 v (proto_eq_next p1')
+ | Receive, Send =>
+ ∀ v1 v2 p1' p2',
+ pc1 v1 (proto_eq_next p1') -∗ pc2 v2 (proto_eq_next p2') -∗
+ ◇ ∃ pc1' pc2' pt,
+ ▷ rec p1' (proto_message Send pc1') ∗
+ ▷ rec (proto_message Receive pc2') p2' ∗
+ pc1' v2 (proto_eq_next pt) ∗
+ pc2' v1 (proto_eq_next pt)
+ | Send, Receive => False
+ end.
+Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
+ NonExpansive2 (iProto_le_pre rec).
+Proof. solve_proper. Qed.
+
+Program Definition iProto_le_pre' {Σ V}
+ (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
+ iProto Σ V -n> iProto Σ V -n> iPropO Σ :=
+ λne p1 p2, iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
+Solve Obligations with solve_proper.
+Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
+Proof.
+ intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
+ by repeat (f_contractive || f_equiv).
+Qed.
+Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ := fixpoint iProto_le_pre' p1 p2.
+Arguments iProto_le {_ _} _%proto _%proto.
+Instance: Params (@iProto_le) 2 := {}.
+
+Fixpoint iProto_interp_aux {Σ V} (n : nat)
+ (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
+ match n with
+ | 0 => ∃ p,
+ ⌜ vsl = [] ⌠∗
+ ⌜ vsr = [] ⌠∗
+ iProto_le p pl ∗
+ iProto_le (iProto_dual p) pr
+ | S n =>
+ (∃ vl vsl' pc p2',
+ ⌜ vsl = vl :: vsl' ⌠∗
+ iProto_le (proto_message Receive pc) pr ∗
+ pc vl (proto_eq_next p2') ∗
+ iProto_interp_aux n vsl' vsr pl p2') ∨
+ (∃ vr vsr' pc p1',
+ ⌜ vsr = vr :: vsr' ⌠∗
+ iProto_le (proto_message Receive pc) pl ∗
+ pc vr (proto_eq_next p1') ∗
+ iProto_interp_aux n vsl vsr' p1' pr)
+ end.
+Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
+ iProto_interp_aux (length vsl + length vsr) vsl vsr pl pr.
+Arguments iProto_interp {_ _} _ _ _%proto _%proto : simpl nomatch.
+
+Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
+
+Inductive side := Left | Right.
+Instance side_inhabited : Inhabited side := populate Left.
+Definition side_elim {A} (s : side) (l r : A) : A :=
+ match s with Left => l | Right => r end.
+
+Definition iProto_unfold {Σ V} (p : iProto Σ V) : proto V (iPrePropO Σ) (iPrePropO Σ) :=
+ proto_map id iProp_fold iProp_unfold p.
+Definition iProto_own_frag `{!protoG Σ V} (γ : proto_name) (s : side)
+ (p : iProto Σ V) : iProp Σ :=
+ own (side_elim s proto_l_name proto_r_name γ) (◯E (Next (iProto_unfold p))).
+Definition iProto_own_auth `{!protoG Σ V} (γ : proto_name) (s : side)
+ (p : iProto Σ V) : iProp Σ :=
+ own (side_elim s proto_l_name proto_r_name γ) (â—E (Next (iProto_unfold p))).
+
+Definition iProto_ctx `{protoG Σ V}
+ (γ : proto_name) (vsl vsr : list V) : iProp Σ :=
+ ∃ pl pr,
+ iProto_own_auth γ Left pl ∗
+ iProto_own_auth γ Right pr ∗
+ â–· iProto_interp vsl vsr pl pr.
+
+(** * The connective for ownership of channel ends *)
+Definition iProto_own `{!protoG Σ V}
+ (γ : proto_name) (s : side) (p : iProto Σ V) : iProp Σ :=
+ ∃ p', iProto_le p' p ∗ iProto_own_frag γ s p'.
+Arguments iProto_own {_ _ _} _ _%proto.
+Instance: Params (@iProto_own) 3 := {}.
+
+(** * Proofs *)
+Section proto.
+ Context `{!protoG Σ V}.
+ Implicit Types p pl pr : iProto Σ V.
+ Implicit Types TT : tele.
+
+ (** ** Non-expansiveness of operators *)
+ Lemma iProto_message_contractive {TT} a
+ (pc1 pc2 : TT → V * iProp Σ * iProto Σ V) n :
+ (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
+ (∀.. x, dist_later n ((pc1 x).1.2) ((pc2 x).1.2)) →
+ (∀.. x, dist_later n ((pc1 x).2) ((pc2 x).2)) →
+ iProto_message a pc1 ≡{n}≡ iProto_message a pc2.
+ Proof.
+ rewrite !tforall_forall=> Hv HP Hp.
+ rewrite iProto_message_eq /iProto_message_def.
+ f_equiv=> v f /=. apply bi.exist_ne=> x.
+ repeat (apply Hv || apply HP || apply Hp || f_contractive || f_equiv).
+ Qed.
+ Lemma iProto_message_ne {TT} a (pc1 pc2 : TT → V * iProp Σ * iProto Σ V) n :
+ (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
+ (∀.. x, (pc1 x).1.2 ≡{n}≡ (pc2 x).1.2) →
+ (∀.. x, (pc1 x).2 ≡{n}≡ (pc2 x).2) →
+ iProto_message a pc1 ≡{n}≡ iProto_message a pc2.
+ Proof.
+ rewrite !tforall_forall=> Hv HP Hp.
+ apply iProto_message_contractive; apply tforall_forall; eauto using dist_dist_later.
+ Qed.
+ Lemma iProto_message_proper {TT} a (pc1 pc2 : TT → V * iProp Σ * iProto Σ V) :
+ (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
+ (∀.. x, (pc1 x).1.2 ≡ (pc2 x).1.2) →
+ (∀.. x, (pc1 x).2 ≡ (pc2 x).2) →
+ iProto_message a pc1 ≡ iProto_message a pc2.
+ Proof.
+ rewrite !tforall_forall=> Hv HP Hp. apply equiv_dist => n.
+ apply iProto_message_ne; apply tforall_forall=> x; by try apply equiv_dist.
+ Qed.
+
+ (** ** Dual *)
+ Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ V).
+ Proof. apply (ne_proper _). Qed.
+ Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_dual_if_proper d : Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
+ Proof. apply (ne_proper _). Qed.
+
+ Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
+ Proof.
+ intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
+ apply: proto_map_ext=> //. by intros [].
+ Qed.
+
+ Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END%proto.
+ Proof. by rewrite iProto_end_eq /iProto_dual proto_map_end. Qed.
+
+ Lemma iProto_dual_message {TT} a (pc : TT → V * iProp Σ * iProto Σ V) :
+ iProto_dual (iProto_message a pc)
+ ≡ iProto_message (action_dual a) (prod_map id iProto_dual ∘ pc).
+ Proof.
+ rewrite /iProto_dual iProto_message_eq /iProto_message_def proto_map_message.
+ by f_equiv=> v f /=.
+ Qed.
+
+ (** Helpers for duals *)
+ Global Instance proto_eq_next_ne : NonExpansive (proto_eq_next (Σ:=Σ) (V:=V)).
+ Proof. solve_proper. Qed.
+ Global Instance proto_eq_next_proper :
+ Proper ((≡) ==> (≡)) (proto_eq_next (Σ:=Σ) (V:=V)).
+ Proof. solve_proper. Qed.
+
+ Lemma proto_eq_next_dual p :
+ ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid
+ (proto_eq_next (iProto_dual p)) ≡ proto_eq_next p.
+ Proof.
+ intros lp. iSplit; iIntros "Hlp /="; last by iRewrite -"Hlp".
+ destruct (Next_uninj lp) as [p' ->].
+ rewrite /later_map /= !bi.later_equivI. iNext.
+ rewrite -{2}(involutive iProto_dual p) -{2}(involutive iProto_dual p').
+ by iRewrite "Hlp".
+ Qed.
+
+ Lemma proto_eq_next_dual' p :
+ ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next p) ≡
+ proto_eq_next (iProto_dual p).
+ Proof.
+ rewrite -(proto_eq_next_dual (iProto_dual p))=> lp /=.
+ by rewrite involutive.
+ Qed.
+
+ (** ** Append *)
+ Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
+ Proof. apply _. Qed.
+ Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
+ Proof. apply (ne_proper_2 _). Qed.
+
+ Lemma iProto_app_message {TT} a (pc : TT → V * iProp Σ * iProto Σ V) p2 :
+ (iProto_message a pc <++> p2)%proto
+ ≡ iProto_message a (prod_map id (flip iProto_app p2) ∘ pc).
+ Proof.
+ rewrite /iProto_app iProto_message_eq /iProto_message_def proto_app_message.
+ by f_equiv=> v f /=.
+ Qed.
+
+ Global Instance iProto_app_end_l : LeftId (≡) END%proto (@iProto_app Σ V).
+ Proof.
+ intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_l.
+ Qed.
+ Global Instance iProto_app_end_r : RightId (≡) END%proto (@iProto_app Σ V).
+ Proof.
+ intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
+ Qed.
+ Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
+ Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.
+
+ Lemma iProto_dual_app p1 p2 :
+ iProto_dual (p1 <++> p2) ≡ (iProto_dual p1 <++> iProto_dual p2)%proto.
+ Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.
+
+ (** ** Protocol entailment **)
+ Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ V).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_le_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
+ Proof. solve_proper. Qed.
+
+ Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2.
+ Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed.
+
+ Lemma iProto_le_refl p : ⊢ iProto_le p p.
+ Proof.
+ iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)].
+ - rewrite iProto_le_unfold. iLeft; by auto.
+ - rewrite iProto_le_unfold. iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
+ iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
+ - rewrite iProto_le_unfold. iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
+ iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
+ Qed.
+
+ Lemma iProto_le_end_inv p : iProto_le p proto_end -∗ p ≡ proto_end.
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
+ iDestruct "H" as (a1 a2 pc1 pc2) "(_ & Heq & _)".
+ by iDestruct (proto_end_message_equivI with "Heq") as %[].
+ Qed.
+
+ Lemma iProto_le_send_inv p1 pc2 :
+ iProto_le p1 (proto_message Send pc2) -∗ ∃ a1 pc1,
+ p1 ≡ proto_message a1 pc1 ∗
+ match a1 with
+ | Send =>
+ ∀ v p2', pc2 v (proto_eq_next p2') -∗
+ ◇ ∃ p1', ▷ iProto_le p1' p2' ∗ pc1 v (proto_eq_next p1')
+ | Receive =>
+ ∀ v1 v2 p1' p2',
+ pc1 v1 (proto_eq_next p1') -∗ pc2 v2 (proto_eq_next p2') -∗
+ ◇ ∃ pc1' pc2' pt,
+ ▷ iProto_le p1' (proto_message Send pc1') ∗
+ ▷ iProto_le (proto_message Receive pc2') p2' ∗
+ pc1' v2 (proto_eq_next pt) ∗
+ pc2' v1 (proto_eq_next pt)
+ end.
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
+ { by iDestruct (proto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 pc1 pc2') "(Hp1 & Hp2 & H)".
+ iDestruct (proto_message_equivI with "Hp2") as (<-) "{Hp2} #Hpc".
+ iExists _, _; iSplit; [done|]. destruct a1.
+ - iIntros (v p2'). by iRewrite ("Hpc" $! v (proto_eq_next p2')).
+ - iIntros (v1 v2 p1' p2'). by iRewrite ("Hpc" $! v2 (proto_eq_next p2')).
+ Qed.
+
+ Lemma iProto_le_recv_inv p1 pc2 :
+ iProto_le p1 (proto_message Receive pc2) -∗ ∃ pc1,
+ p1 ≡ proto_message Receive pc1 ∗
+ ∀ v p1', pc1 v (proto_eq_next p1') -∗
+ ◇ ∃ p2', ▷ iProto_le p1' p2' ∗ pc2 v (proto_eq_next p2').
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
+ { by iDestruct (proto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 pc1 pc2') "(Hp1 & Hp2 & H)".
+ iDestruct (proto_message_equivI with "Hp2") as (<-) "{Hp2} #Hpc2".
+ destruct a1; [done|]. iExists _; iSplit; [done|].
+ iIntros (v p1') "Hpc". iDestruct ("H" with "Hpc") as (p2') ">[Hle Hpc]".
+ iExists p2'. iFrame "Hle". by iRewrite ("Hpc2" $! v (proto_eq_next p2')).
+ Qed.
+
+ Lemma iProto_le_trans p1 p2 p3 :
+ iProto_le p1 p2 -∗ iProto_le p2 p3 -∗ iProto_le p1 p3.
+ Proof.
+ iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
+ destruct (proto_case p3) as [->|([]&pc3&->)].
+ - by iRewrite (iProto_le_end_inv with "H2") in "H1".
+ - iDestruct (iProto_le_send_inv with "H2") as (a2 pc2) "[Hp2 H2]".
+ iRewrite "Hp2" in "H1"; clear p2. destruct a2.
+ + iDestruct (iProto_le_send_inv with "H1") as (a1 pc1) "[Hp1 H1]".
+ iRewrite "Hp1"; clear p1. rewrite iProto_le_unfold; iRight.
+ iExists _, _, _, _; do 2 (iSplit; [done|]). destruct a1.
+ * iIntros (v p3') "Hpc".
+ iMod ("H2" with "Hpc") as (p2') "[Hle Hpc]".
+ iMod ("H1" with "Hpc") as (p1') "[Hle' Hpc]".
+ iExists p1'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle'").
+ * iIntros (v1 v3 p1' p3') "Hpc1 Hpc3".
+ iMod ("H2" with "Hpc3") as (p2') "[Hle Hpc2]".
+ iMod ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(Hp1' & Hp2' & Hpc)".
+ iModIntro. iExists pc1', pc2', pt. iFrame "Hp1' Hpc".
+ by iApply ("IH" with "Hp2'").
+ + iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H1]".
+ iRewrite "Hp1"; clear p1. rewrite iProto_le_unfold; iRight.
+ iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
+ iIntros (v1 v3 p1' p3') "Hpc1 Hpc3".
+ iMod ("H1" with "Hpc1") as (p2') "[Hle Hpc2]".
+ iMod ("H2" with "Hpc2 Hpc3") as (pc2' pc3' pt) "(Hp2' & Hp3' & Hpc)".
+ iModIntro. iExists pc2', pc3', pt. iFrame "Hp3' Hpc".
+ by iApply ("IH" with "Hle").
+ - iDestruct (iProto_le_recv_inv with "H2") as (pc2) "[Hp2 H3]".
+ iRewrite "Hp2" in "H1".
+ iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H2]".
+ iRewrite "Hp1". rewrite iProto_le_unfold. iRight.
+ iExists _, _, _, _; do 2 (iSplit; [done|]).
+ iIntros (v p1') "Hpc".
+ iMod ("H2" with "Hpc") as (p2') "[Hle Hpc]".
+ iMod ("H3" with "Hpc") as (p3') "[Hle' Hpc]".
+ iModIntro. iExists p3'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle").
+ Qed.
+
+ Lemma iProto_le_send {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+ (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
+ (∀.. x2 : TT2, ▷ (pc2 x2).1.2 -∗ ◇ ∃.. x1 : TT1,
+ ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌠∗
+ ▷ (pc1 x1).1.2 ∗
+ ▷ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
+ iProto_le (iProto_message Send pc1) (iProto_message Send pc2).
+ Proof.
+ iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
+ iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
+ iIntros (v p2') "/=". iDestruct 1 as (x2 ->) "[Hpc #Heq]".
+ iMod ("H" with "Hpc") as (x1 ?) "[Hpc Hle]".
+ iModIntro. iExists (pc1 x1).2. iSplitL "Hle".
+ { iIntros "!>". by iRewrite "Heq". }
+ iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
+ Qed.
+ (* The following derived rule is weaker, but the positions of the laters
+ make more sense intuitively and practically. *)
+ Lemma iProto_le_send' {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+ (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
+ ▷ (∀.. x2 : TT2, (pc2 x2).1.2 -∗ ∃.. x1 : TT1,
+ ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌠∗
+ (pc1 x1).1.2 ∗
+ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
+ iProto_le (iProto_message Send pc1) (iProto_message Send pc2).
+ Proof.
+ iIntros "H". iApply iProto_le_send. iIntros (x2) "Hpc".
+ rewrite bi_tforall_forall. iDestruct ("H" with "Hpc") as "H".
+ rewrite bi_texist_exist bi.later_exist_except_0.
+ iMod "H" as (x1) "(>% & Hpc & Hle)". iExists x1. by iFrame.
+ Qed.
+
+ Lemma iProto_le_recv {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+ (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
+ (∀.. x1 : TT1, ▷ (pc1 x1).1.2 -∗ ◇ ∃.. x2 : TT2,
+ ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌠∗
+ ▷ (pc2 x2).1.2 ∗
+ ▷ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
+ iProto_le (iProto_message Receive pc1) (iProto_message Receive pc2).
+ Proof.
+ iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
+ iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
+ iIntros (v p1') "/=". iDestruct 1 as (x1 ->) "[Hpc #Heq]".
+ iMod ("H" with "Hpc") as (x2 ?) "[Hpc Hle]". iExists (pc2 x2).2. iSplitL "Hle".
+ { iIntros "!> !>". by iRewrite "Heq". }
+ iModIntro. iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
+ Qed.
+ Lemma iProto_le_recv' {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+ (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
+ ▷ (∀.. x1 : TT1, (pc1 x1).1.2 -∗ ∃.. x2 : TT2,
+ ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌠∗
+ (pc2 x2).1.2 ∗
+ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
+ iProto_le (iProto_message Receive pc1) (iProto_message Receive pc2).
+ Proof.
+ iIntros "H". iApply iProto_le_recv. iIntros (x2) "Hpc".
+ rewrite bi_tforall_forall. iDestruct ("H" with "Hpc") as "H".
+ rewrite bi_texist_exist bi.later_exist_except_0.
+ iMod "H" as (x1) "(>% & Hpc & Hle)". iExists x1. by iFrame.
+ Qed.
+
+ Lemma iProto_le_swap {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+ (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
+ (∀.. (x1 : TT1) (x2 : TT2),
+ ▷ (pc1 x1).1.2 -∗ ▷ (pc2 x2).1.2 -∗
+ ◇ ∃ {TT3 TT4} (pc3 : TT3 → V * iProp Σ * iProto Σ V)
+ (pc4 : TT4 → V * iProp Σ * iProto Σ V), ∃.. (x3 : TT3) (x4 : TT4),
+ ⌜(pc1 x1).1.1 = (pc4 x4).1.1⌠∗
+ ⌜(pc2 x2).1.1 = (pc3 x3).1.1⌠∗
+ ▷ iProto_le (pc1 x1).2 (iProto_message Send pc3) ∗
+ ▷ iProto_le (iProto_message Receive pc4) (pc2 x2).2 ∗
+ ▷ (pc3 x3).1.2 ∗ ▷ (pc4 x4).1.2 ∗
+ ▷ ((pc3 x3).2 ≡ (pc4 x4).2)) -∗
+ iProto_le (iProto_message Receive pc1) (iProto_message Send pc2).
+ Proof.
+ iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
+ iRight. iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
+ iIntros (v1 v2 p1 p2).
+ iDestruct 1 as (x1 ->) "[Hpc1 #Heq1]"; iDestruct 1 as (x2 ->) "[Hpc2 #Heq2]".
+ iMod ("H" with "Hpc1 Hpc2")
+ as (TT3 TT4 pc3 pc4 x3 x4 ??) "(H1 & H2 & Hpc1 & Hpc2 & #H)".
+ iModIntro. iExists _, _, (pc3 x3).2. iSplitL "H1"; [iNext; by iRewrite "Heq1"|].
+ iSplitL "H2"; [iNext; by iRewrite "Heq2"|]. simpl.
+ iSplitL "Hpc1"; [by auto|]. iExists x4. rewrite !bi.later_equivI. auto.
+ Qed.
+ Lemma iProto_le_swap' {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+ (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
+ ▷ (∀.. (x1 : TT1) (x2 : TT2),
+ (pc1 x1).1.2 -∗ (pc2 x2).1.2 -∗
+ ∃ {TT3 TT4} (pc3 : TT3 → V * iProp Σ * iProto Σ V)
+ (pc4 : TT4 → V * iProp Σ * iProto Σ V), ∃.. (x3 : TT3) (x4 : TT4),
+ ⌜(pc1 x1).1.1 = (pc4 x4).1.1⌠∗
+ ⌜(pc2 x2).1.1 = (pc3 x3).1.1⌠∗
+ iProto_le (pc1 x1).2 (iProto_message Send pc3) ∗
+ iProto_le (iProto_message Receive pc4) (pc2 x2).2 ∗
+ (pc3 x3).1.2 ∗ (pc4 x4).1.2 ∗
+ ((pc3 x3).2 ≡ (pc4 x4).2)) -∗
+ iProto_le (iProto_message Receive pc1) (iProto_message Send pc2).
+ Proof.
+ iIntros "H". iApply iProto_le_swap. iIntros (x1 x2) "Hpc1 Hpc2".
+ repeat setoid_rewrite bi_tforall_forall. iDestruct ("H" with "Hpc1 Hpc2") as "H".
+ iMod (bi.later_exist_except_0 with "H") as (TT3) "H".
+ iMod (bi.later_exist_except_0 with "H") as (TT4) "H".
+ iMod (bi.later_exist_except_0 with "H") as (pc3) "H".
+ iMod (bi.later_exist_except_0 with "H") as (pc4) "H".
+ rewrite bi_texist_exist bi.later_exist_except_0. iMod "H" as (x3) "H".
+ rewrite bi_texist_exist bi.later_exist_except_0. iMod "H" as (x4) "H".
+ iDestruct "H" as "(>% & >% & H1 & H2 & Hpc1 & Hpc2 & #H)".
+ iExists TT3, TT4, pc3, pc4, x3, x4. iFrame. auto.
+ Qed.
+
+ Lemma iProto_le_swap_simple {TT1 TT2} (v1 : TT1 → V) (v2 : TT2 → V)
+ (P1 : TT1 → iProp Σ) (P2 : TT2 → iProp Σ) (p : TT1 → TT2 → iProto Σ V) :
+ ⊢ iProto_le
+ (iProto_message Receive (λ x1,
+ (v1 x1, P1 x1, iProto_message Send (λ x2, (v2 x2, P2 x2, p x1 x2)))))
+ (iProto_message Send (λ x2,
+ (v2 x2, P2 x2, iProto_message Receive (λ x1, (v1 x1, P1 x1, p x1 x2))))).
+ Proof.
+ iApply iProto_le_swap. iIntros (x1 x2) "/= HP1 HP2".
+ iExists TT2, TT1, (λ x2, (v2 x2, P2 x2, p x1 x2)),
+ (λ x1, (v1 x1, P1 x1, p x1 x2)), x2, x1; simpl.
+ do 2 (iSplit; [done|]). do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
+ Qed.
+
+ Lemma iProto_le_dual p1 p2 :
+ iProto_le p2 p1 -∗ iProto_le (iProto_dual p1) (iProto_dual p2).
+ Proof.
+ iIntros "H". iLöb as "IH" forall (p1 p2).
+ destruct (proto_case p1) as [->|([]&pc1&->)].
+ - iRewrite (iProto_le_end_inv with "H"). iApply iProto_le_refl.
+ - iDestruct (iProto_le_send_inv with "H") as (a2 pc2) "[Hp2 H]".
+ iRewrite "Hp2"; clear p2. iEval (rewrite /iProto_dual !proto_map_message /=).
+ rewrite iProto_le_unfold; iRight.
+ iExists _, _, _, _; do 2 (iSplit; [done|]); simpl. destruct a2; simpl.
+ + iIntros (v p1') "Hpc". rewrite proto_eq_next_dual'.
+ iMod ("H" with "Hpc") as (p2'') "[H Hpc]".
+ iDestruct ("IH" with "H") as "H". rewrite involutive.
+ iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
+ + iIntros (v1 v2 p1' p2') "Hpc1 Hpc2". rewrite !proto_eq_next_dual'.
+ iMod ("H" with "Hpc2 Hpc1") as (pc1' pc2' pt) "(H1 & H2 & Hpc1 & Hpc2)".
+ iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
+ rewrite !involutive /iProto_dual !proto_map_message.
+ iExists _, _, (iProto_dual pt). iFrame. rewrite /= proto_eq_next_dual. iFrame.
+ - iDestruct (iProto_le_recv_inv with "H") as (pc2) "[Hp2 H]".
+ iRewrite "Hp2"; clear p2. iEval (rewrite /iProto_dual !proto_map_message /=).
+ rewrite iProto_le_unfold; iRight.
+ iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
+ iIntros (v p2') "Hpc". rewrite proto_eq_next_dual'.
+ iMod ("H" with "Hpc") as (p2'') "[H Hpc]".
+ iDestruct ("IH" with "H") as "H". rewrite involutive.
+ iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
+ Qed.
+
+ (** ** Lemmas about the auxiliary definitions and invariants *)
+ Global Instance iProto_interp_aux_ne n vsl vsr :
+ NonExpansive2 (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
+ Proof. revert vsl vsr. induction n; solve_proper. Qed.
+ Global Instance iProto_interp_aux_proper n vsl vsr :
+ Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
+ Proof. apply (ne_proper_2 _). Qed.
+ Global Instance iProto_interp_ne vsl vsr :
+ NonExpansive2 (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_interp_proper vsl vsr :
+ Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
+ Proof. apply (ne_proper_2 _). Qed.
+
+ Global Instance iProto_unfold_ne : NonExpansive (iProto_unfold (Σ:=Σ) (V:=V)).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
+ Proof. solve_proper. Qed.
+
+ Lemma iProto_own_auth_agree γ s p p' :
+ iProto_own_auth γ s p -∗ iProto_own_frag γ s p' -∗ ▷ (p ≡ p').
+ Proof.
+ iIntros "H◠H◯". iDestruct (own_valid_2 with "H◠H◯") as "H✓".
+ iDestruct (excl_auth_agreeI with "H✓") as "H✓".
+ iDestruct (bi.later_eq_1 with "H✓") as "H✓"; iNext.
+ rewrite /iProto_unfold. assert (∀ p,
+ proto_map id iProp_unfold iProp_fold (proto_map id iProp_fold iProp_unfold p) ≡ p) as help.
+ { intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
+ apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. }
+ rewrite -{2}(help p). iRewrite "H✓". by rewrite help.
+ Qed.
+
+ Lemma iProto_own_auth_update γ s p p' p'' :
+ iProto_own_auth γ s p -∗ iProto_own_frag γ s p' ==∗
+ iProto_own_auth γ s p'' ∗ iProto_own_frag γ s p''.
+ Proof.
+ iIntros "Hâ— Hâ—¯". iDestruct (own_update_2 with "Hâ— Hâ—¯") as "H".
+ { eapply (excl_auth_update _ _ (Next (iProto_unfold p''))). }
+ by rewrite own_op.
+ Qed.
+
+ (* TODO: Move somewhere else *)
+ Lemma false_disj_cong (P Q Q' : iProp Σ) :
+ (P ⊢ False) → (Q ⊣⊢ Q') → (P ∨ Q ⊣⊢ Q').
+ Proof. intros HP ->. apply (anti_symm _). by rewrite HP left_id. auto. Qed.
+
+ Lemma pure_sep_cong (φ1 φ2 : Prop) (P1 P2 : iProp Σ) :
+ (φ1 ↔ φ2) → (φ1 → φ2 → P1 ⊣⊢ P2) → (⌜φ1⌠∗ P1) ⊣⊢ (⌜φ2⌠∗ P2).
+ Proof. intros -> HP. iSplit; iDestruct 1 as (HÏ•) "H"; rewrite HP; auto. Qed.
+
+ Lemma iProto_interp_unfold vsl vsr pl pr :
+ iProto_interp vsl vsr pl pr ⊣⊢
+ (∃ p,
+ ⌜ vsl = [] ⌠∗
+ ⌜ vsr = [] ⌠∗
+ iProto_le p pl ∗
+ iProto_le (iProto_dual p) pr) ∨
+ (∃ vl vsl' pc pr',
+ ⌜ vsl = vl :: vsl' ⌠∗
+ iProto_le (proto_message Receive pc) pr ∗
+ pc vl (proto_eq_next pr') ∗
+ iProto_interp vsl' vsr pl pr') ∨
+ (∃ vr vsr' pc pl',
+ ⌜ vsr = vr :: vsr' ⌠∗
+ iProto_le (proto_message Receive pc) pl ∗
+ pc vr (proto_eq_next pl') ∗
+ iProto_interp vsl vsr' pl' pr).
+ Proof.
+ rewrite {1}/iProto_interp. destruct vsl as [|vl vsl]; simpl.
+ - destruct vsr as [|vr vsr]; simpl.
+ + iSplit; first by auto.
+ iDestruct 1 as "[H | [H | H]]"; first by auto.
+ * iDestruct "H" as (? ? ? ? [=]) "_".
+ * iDestruct "H" as (? ? ? ? [=]) "_".
+ + symmetry. apply false_disj_cong.
+ { iDestruct 1 as (? _ [=]) "_". }
+ repeat first [apply pure_sep_cong; intros; simplify_eq/= | f_equiv];
+ by rewrite ?Nat.add_succ_r.
+ - symmetry. apply false_disj_cong.
+ { iDestruct 1 as (? [=]) "_". }
+ repeat first [apply pure_sep_cong; intros; simplify_eq/= | f_equiv];
+ by rewrite ?Nat.add_succ_r.
+ Qed.
+
+ Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
+ Proof.
+ rewrite iProto_interp_unfold. iLeft. iExists p. do 2 (iSplit; [done|]).
+ iSplitL; iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_interp_flip vsl vsr pl pr :
+ iProto_interp vsl vsr pl pr -∗ iProto_interp vsr vsl pr pl.
+ Proof.
+ remember (length vsl + length vsr) as n eqn:Hn.
+ iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
+ rewrite !iProto_interp_unfold. iIntros "[H|[H|H]]".
+ - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
+ iLeft. iExists (iProto_dual p). rewrite involutive. iFrame; auto.
+ - iDestruct "H" as (vl vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
+ iRight; iRight. iExists vl, vsl', pc', pr'. iSplit; [done|]; iFrame.
+ iApply ("IH" with "[%] [//] H"); simpl; lia.
+ - iDestruct "H" as (vr vsr' pc' pl' ->) "(Hpl & Hpc' & H)".
+ iRight; iLeft. iExists vr, vsr', pc', pl'. iSplit; [done|]; iFrame.
+ iApply ("IH" with "[%] [//] H"); simpl; lia.
+ Qed.
+
+ Lemma iProto_interp_le_l vsl vsr pl pl' pr :
+ iProto_interp vsl vsr pl pr -∗ iProto_le pl pl' -∗ iProto_interp vsl vsr pl' pr.
+ Proof.
+ remember (length vsl + length vsr) as n eqn:Hn.
+ iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
+ rewrite !iProto_interp_unfold. iIntros "[H|[H|H]] Hle".
+ - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
+ iLeft. iExists p. do 2 (iSplit; [done|]). iFrame "Hp'".
+ by iApply (iProto_le_trans with "Hp").
+ - iDestruct "H" as (vl vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
+ iRight; iLeft. iExists vl, vsl', pc', pr'. iSplit; [done|]; iFrame.
+ iApply ("IH" with "[%] [//] H Hle"); simpl; lia.
+ - iClear "IH". iDestruct "H" as (vr vsr' pc' pl'' ->) "(Hpl & Hpc' & H)".
+ iRight; iRight. iExists vr, vsr', pc', pl''. iSplit; [done|]; iFrame.
+ by iApply (iProto_le_trans with "Hpl").
+ Qed.
+ Lemma iProto_interp_le_r vsl vsr pl pr pr' :
+ iProto_interp vsl vsr pl pr -∗ iProto_le pr pr' -∗ iProto_interp vsl vsr pl pr'.
+ Proof.
+ iIntros "H Hle". iApply iProto_interp_flip.
+ iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_flip.
+ Qed.
+
+ Lemma iProto_interp_send vl pcl vsl vsr pl pr pl' :
+ iProto_interp vsl vsr pl pr -∗
+ iProto_le pl (proto_message Send pcl) -∗
+ pcl vl (proto_eq_next pl') -∗
+ â–·^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
+ Proof.
+ iIntros "H Hle". iDestruct (iProto_interp_le_l with "H Hle") as "H".
+ clear pl. iIntros "Hpcl". remember (length vsl + length vsr) as n eqn:Hn.
+ iInduction (lt_wf n) as [n _] "IH" forall (pcl vsl vsr pr pl' Hn); subst.
+ rewrite {1}iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
+ - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
+ iDestruct (iProto_le_dual with "Hp") as "Hp".
+ iDestruct (iProto_le_trans with "Hp Hp'") as "Hp".
+ rewrite /iProto_dual proto_map_message /=.
+ iApply iProto_interp_unfold. iRight; iLeft.
+ iExists vl, [], _, (iProto_dual pl'). iSplit; [done|]. iFrame "Hp"; simpl.
+ rewrite proto_eq_next_dual. iFrame "Hpcl". iApply iProto_interp_nil.
+ - iDestruct "H" as (vl' vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
+ iDestruct ("IH" with "[%] [//] H Hpcl") as "H"; [simpl; lia|].
+ iNext. iApply (iProto_interp_le_r with "[-Hpr] Hpr"); clear pr.
+ iApply iProto_interp_unfold. iRight; iLeft.
+ iExists vl', (vsl' ++ [vl]), pc', pr'. iFrame.
+ iSplit; [done|]. iApply iProto_le_refl.
+ - iDestruct "H" as (vr' vsr' pc' pl'' ->) "(Hle & Hpcl' & H) /=".
+ iDestruct (iProto_le_send_inv with "Hle") as (a pcl') "[Hpc Hle]".
+ iDestruct (proto_message_equivI with "Hpc") as (<-) "Hpc".
+ iRewrite ("Hpc" $! vr' (proto_eq_next pl'')) in "Hpcl'"; clear pc'.
+ iMod ("Hle" with "Hpcl' Hpcl")
+ as (pc1 pc2 pt) "(Hpl'' & Hpl' & Hpc1 & Hpc2)".
+ iNext. iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
+ iDestruct ("IH" with "[%] [//] H Hpc1") as "H"; [simpl; lia|..].
+ iNext. iApply iProto_interp_unfold. iRight; iRight.
+ iExists vr', vsr', _, pt. iSplit; [done|]. by iFrame.
+ Qed.
+
+ Lemma iProto_interp_recv vl vsl vsr pl pr pcr :
+ iProto_interp (vl :: vsl) vsr pl pr -∗
+ iProto_le pr (proto_message Receive pcr) -∗
+ ◇ ∃ pr, pcr vl (proto_eq_next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
+ Proof.
+ iIntros "H Hle". iDestruct (iProto_interp_le_r with "H Hle") as "H".
+ clear pr. remember (length vsr) as n eqn:Hn.
+ iInduction (lt_wf n) as [n _] "IH" forall (vsr pl Hn); subst.
+ rewrite !iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
+ - iClear "IH". iDestruct "H" as (p [=]) "_".
+ - iClear "IH". iDestruct "H" as (vl' vsl' pc' pr' [= -> ->]) "(Hpr & Hpc' & Hinterp)".
+ iDestruct (iProto_le_recv_inv with "Hpr") as (pc'') "[Hpc Hpr]".
+ iDestruct (proto_message_equivI with "Hpc") as (_) "{Hpc} #Hpc".
+ iMod ("Hpr" $! vl' pr' with "[Hpc']") as (pr'') "[Hler Hpr]".
+ { by iRewrite -("Hpc" $! vl' (proto_eq_next pr')). }
+ iModIntro. iExists pr''. iFrame "Hpr".
+ by iApply (iProto_interp_le_r with "Hinterp").
+ - iDestruct "H" as (vr vsr' pc' pl'' ->) "(Hpl & Hpc' & Hinterp)".
+ iMod ("IH" with "[%] [//] Hinterp") as (pr) "[Hpc Hinterp]"; [simpl; lia|].
+ iModIntro. iExists pr. iFrame "Hpc".
+ iApply iProto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
+ Qed.
+
+ Global Instance iProto_own_ne γ s : NonExpansive (iProto_own γ s).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_own_proper γ s : Proper ((≡) ==> (≡)) (iProto_own γ s).
+ Proof. apply (ne_proper _). Qed.
+
+ Lemma iProto_own_le γ s p1 p2 :
+ iProto_own γ s p1 -∗ iProto_le p1 p2 -∗ iProto_own γ s p2.
+ Proof.
+ iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
+ iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
+ Qed.
+
+ Lemma iProto_init p :
+ ⊢ |==> ∃ γ,
+ iProto_ctx γ [] [] ∗
+ iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
+ Proof.
+ iMod (own_alloc (â—E (Next (iProto_unfold p)) â‹…
+ â—¯E (Next (iProto_unfold p)))) as (lγ) "[Hâ—l Hâ—¯l]".
+ { by apply excl_auth_valid. }
+ iMod (own_alloc (â—E (Next (iProto_unfold (iProto_dual p))) â‹…
+ â—¯E (Next (iProto_unfold (iProto_dual p))))) as (rγ) "[Hâ—r Hâ—¯r]".
+ { by apply excl_auth_valid. }
+ pose (ProtName lγ rγ) as γ. iModIntro. iExists γ. iSplitL "Hâ—l Hâ—r".
+ { iExists p, (iProto_dual p). iFrame. iApply iProto_interp_nil. }
+ iSplitL "Hâ—¯l"; iExists _; iFrame; iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_send_l {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) (x : TT) vsr vsl :
+ iProto_ctx γ vsl vsr -∗
+ iProto_own γ Left (iProto_message Send pc) -∗
+ (pc x).1.2 ==∗
+ ▷^(length vsr) iProto_ctx γ (vsl ++ [(pc x).1.1]) vsr ∗
+ iProto_own γ Left (pc x).2.
+ Proof.
+ rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ iDestruct 1 as (p) "[Hle Hâ—¯]". iIntros "Hpc".
+ iDestruct (iProto_own_auth_agree with "Hâ—l Hâ—¯") as "#Hp".
+ iAssert (â–· iProto_le pl (iProto_message_def Send pc))%I
+ with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
+ iDestruct (iProto_interp_send ((pc x).1.1) with "Hinterp Hle [Hpc]") as "Hinterp".
+ { simpl. auto. }
+ iMod (iProto_own_auth_update _ _ _ _ (pc x).2 with "Hâ—l Hâ—¯") as "[Hâ—l Hâ—¯]".
+ iIntros "!>". iSplitR "Hâ—¯".
+ - iIntros "!>". iExists (pc x).2, pr. iFrame.
+ - iExists (pc x).2. iFrame. iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_send_r {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) (x : TT) vsr vsl :
+ iProto_ctx γ vsl vsr -∗
+ iProto_own γ Right (iProto_message Send pc) -∗
+ (pc x).1.2 ==∗
+ ▷^(length vsl) iProto_ctx γ vsl (vsr ++ [(pc x).1.1]) ∗
+ iProto_own γ Right (pc x).2.
+ Proof.
+ rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ iDestruct 1 as (p) "[Hle Hâ—¯]". iIntros "Hpc".
+ iDestruct (iProto_own_auth_agree with "Hâ—r Hâ—¯") as "#Hp".
+ iAssert (â–· iProto_le pr (iProto_message_def Send pc))%I
+ with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
+ iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
+ iDestruct (iProto_interp_send ((pc x).1.1) with "Hinterp Hle [Hpc]") as "Hinterp".
+ { simpl. auto. }
+ iMod (iProto_own_auth_update _ _ _ _ (pc x).2 with "Hâ—r Hâ—¯") as "[Hâ—r Hâ—¯]".
+ iIntros "!>". iSplitR "Hâ—¯".
+ - iIntros "!>". iExists pl, (pc x).2. iFrame. by iApply iProto_interp_flip.
+ - iExists (pc x).2. iFrame. iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_recv_l {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) vr vsr vsl :
+ iProto_ctx γ vsl (vr :: vsr) -∗
+ iProto_own γ Left (iProto_message Receive pc) ==∗
+ ▷ ▷ ∃ (x : TT),
+ ⌜ vr = (pc x).1.1 ⌠∗
+ iProto_ctx γ vsl vsr ∗
+ iProto_own γ Left (pc x).2 ∗
+ (pc x).1.2.
+ Proof.
+ rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ iDestruct 1 as (p) "[Hle Hâ—¯]".
+ iDestruct (iProto_own_auth_agree with "Hâ—l Hâ—¯") as "#Hp".
+ iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
+ iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
+ { iNext. by iRewrite "Hp". }
+ iMod (iProto_own_auth_update _ _ _ _ q with "Hâ—l Hâ—¯") as "[Hâ—l Hâ—¯]".
+ iIntros "!> !>". iMod "Hinterp". iMod "Hpc" as (x ->) "[Hpc #Hq] /=".
+ iIntros "!>". iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "Hâ—¯".
+ - iExists q, pr. iFrame. by iApply iProto_interp_flip.
+ - iRewrite -"Hq". iExists q. iFrame. iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_recv_r {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) vl vsr vsl :
+ iProto_ctx γ (vl :: vsl) vsr -∗
+ iProto_own γ Right (iProto_message Receive pc) ==∗
+ ▷ ▷ ∃ (x : TT),
+ ⌜ vl = (pc x).1.1 ⌠∗
+ iProto_ctx γ vsl vsr ∗
+ iProto_own γ Right (pc x).2 ∗
+ (pc x).1.2.
+ Proof.
+ rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ iDestruct 1 as (p) "[Hle Hâ—¯]".
+ iDestruct (iProto_own_auth_agree with "Hâ—r Hâ—¯") as "#Hp".
+ iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
+ { iNext. by iRewrite "Hp". }
+ iMod (iProto_own_auth_update _ _ _ _ q with "Hâ—r Hâ—¯") as "[Hâ—r Hâ—¯]".
+ iIntros "!> !>". iMod "Hinterp". iMod "Hpc" as (x ->) "[Hpc #Hq] /=".
+ iIntros "!>". iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "Hâ—¯".
+ - iExists pl, q. iFrame.
+ - iRewrite -"Hq". iExists q. iFrame. iApply iProto_le_refl.
+ Qed.
+End proto.
+
+Typeclasses Opaque iProto_ctx iProto_own.
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
deleted file mode 100644
index 6ba63659253b0267bbf65d306dd99a8f3171b678..0000000000000000000000000000000000000000
--- a/theories/channel/proto_channel.v
+++ /dev/null
@@ -1,884 +0,0 @@
-(** This file defines the core of the Actris logic:
-
-- It defines dependent separation protocols and the various operations on it
- like dual, append, and branching.
-- It defines the connective [c ↣ prot] for ownership of channel endpoints.
-- It proves Actris's specifications of [send] and [receive] w.r.t. dependent
- separation protocols.
-
-Dependent separation protocols are defined by instantiating the parameterized
-version in [proto_model] with type of values [val] of HeapLang and the
-propositions [iProp] of Iris.
-
-In doing so we define ways of constructing instances of the instantiated type
-via two constructors:
-- [iProto_end], which is identical to [proto_end].
-- [iProto_message], which takes an action and a continuation to construct
- the corresponding message protocols.
-
-For convenience sake, we provide the following notations:
-- [END], which is simply [iProto_end].
-- [<!> x1 .. xn, MSG v; {{ P }}; prot] and [<?> x1 .. xn, MSG v; {{ P }}; prot],
- which construct an instance of [iProto_message] with the appropriate
- continuation.
-
-Futhermore, we define the following operations:
-- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
-- [iProto_app], which appends two protocols as described in proto_model.v
-
-An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
-[prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
-file.
-
-The logical connective for protocol ownership is denoted as [c ↣ prot]. It
-describes that channel endpoint [c] adheres to protocol [prot]. This connective
-is modeled using Iris invariants and ghost state along with the logical
-connectives of the channel encodings [is_chan] and [chan_own].
-
-Lastly, relevant type classes instances are defined for each of the above
-notions, such as contractiveness and non-expansiveness, after which the
-specifications of the message-passing primitives are defined in terms of the
-protocol connectives. *)
-From actris.channel Require Export channel.
-From actris.channel Require Import proto_model.
-From iris.base_logic.lib Require Import invariants.
-From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl_auth.
-Export action.
-
-Definition start_chan : val := λ: "f",
- let: "cc" := new_chan #() in
- Fork ("f" (Snd "cc"));; Fst "cc".
-
-(** * Setup of Iris's cameras *)
-Class proto_chanG Σ := {
- proto_chanG_chanG :> chanG Σ;
- proto_chanG_authG :> inG Σ (excl_authR (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))));
-}.
-
-Definition proto_chanΣ := #[
- chanΣ;
- GFunctor (authRF (optionURF (exclRF (laterOF (protoOF val idOF idOF)))))
-].
-Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ → proto_chanG Σ.
-Proof. intros [??%subG_inG]%subG_inv. constructor; apply _. Qed.
-
-(** * Types *)
-Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
-Delimit Scope proto_scope with proto.
-Bind Scope proto_scope with iProto.
-
-(** * Operators *)
-Definition iProto_end_def {Σ} : iProto Σ := proto_end.
-Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
-Definition iProto_end := iProto_end_aux.(unseal).
-Definition iProto_end_eq : @iProto_end = @iProto_end_def := iProto_end_aux.(seal_eq).
-Arguments iProto_end {_}.
-
-Program Definition iProto_message_def {Σ} {TT : tele} (a : action)
- (pc : TT → val * iProp Σ * iProto Σ) : iProto Σ :=
- proto_message a (λ v, λne f, ∃ x : TT,
- (** We need the later to make [iProto_message] contractive *)
- ⌜ v = (pc x).1.1 ⌠∗
- ▷ (pc x).1.2 ∗
- f (Next (pc x).2))%I.
-Next Obligation. solve_proper. Qed.
-Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
-Definition iProto_message := iProto_message_aux.(unseal).
-Definition iProto_message_eq :
- @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
-Arguments iProto_message {_ _} _ _%proto.
-Instance: Params (@iProto_message) 3 := {}.
-
-Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
- (iProto_message
- a
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
- (at level 20, a at level 10, x1 binder, xn binder,
- v at level 20, P, p at level 200) : proto_scope.
-Notation "< a > x1 .. xn , 'MSG' v ; p" :=
- (iProto_message
- a
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
- (at level 20, a at level 10, x1 binder, xn binder,
- v at level 20, p at level 200) : proto_scope.
-Notation "< a > 'MSG' v {{ P } } ; p" :=
- (iProto_message
- a
- (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
- (at level 20, a at level 10, v at level 20, P, p at level 200) : proto_scope.
-Notation "< a > 'MSG' v ; p" :=
- (iProto_message
- a
- (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
- (at level 20, a at level 10, v at level 20, p at level 200) : proto_scope.
-
-Notation "<!> x1 .. xn , 'MSG' v {{ P } } ; p" :=
- (iProto_message
- Send
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
- (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
-Notation "<!> x1 .. xn , 'MSG' v ; p" :=
- (iProto_message
- Send
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
- (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
-Notation "<!> 'MSG' v {{ P } } ; p" :=
- (iProto_message
- (TT:=TeleO)
- Send
- (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
- (at level 20, v at level 20, P, p at level 200) : proto_scope.
-Notation "<!> 'MSG' v ; p" :=
- (iProto_message
- (TT:=TeleO)
- Send
- (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
- (at level 20, v at level 20, p at level 200) : proto_scope.
-
-Notation "<?> x1 .. xn , 'MSG' v {{ P } } ; p" :=
- (iProto_message
- Receive
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
- (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
-Notation "<?> x1 .. xn , 'MSG' v ; p" :=
- (iProto_message
- Receive
- (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
- λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
- (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
-Notation "<?> 'MSG' v {{ P } } ; p" :=
- (iProto_message
- Receive
- (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
- (at level 20, v at level 20, P, p at level 200) : proto_scope.
-Notation "<?> 'MSG' v ; p" :=
- (iProto_message
- Receive
- (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
- (at level 20, v at level 20, p at level 200) : proto_scope.
-
-Notation "'END'" := iProto_end : proto_scope.
-
-(** * Operations *)
-Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
- proto_map action_dual cid cid p.
-Arguments iProto_dual {_} _%proto.
-Instance: Params (@iProto_dual) 1 := {}.
-Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
- if d then iProto_dual p else p.
-Arguments iProto_dual_if {_} _ _%proto.
-Instance: Params (@iProto_dual_if) 2 := {}.
-
-Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
- (p1 p2 : iProto Σ) : iProto Σ :=
- (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
-Typeclasses Opaque iProto_branch.
-Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
-Instance: Params (@iProto_branch) 2 := {}.
-Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
-Infix "<{ P1 }&{ P2 }>" := (iProto_branch Receive P1 P2) (at level 85) : proto_scope.
-Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
-Infix "<&{ P2 }>" := (iProto_branch Receive True P2) (at level 85) : proto_scope.
-Infix "<{ P1 }+>" := (iProto_branch Send P1 True) (at level 85) : proto_scope.
-Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope.
-Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
-Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
-
-Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
-Arguments iProto_app {_} _%proto _%proto.
-Instance: Params (@iProto_app) 1 := {}.
-Infix "<++>" := iProto_app (at level 60) : proto_scope.
-
-(** * Auxiliary definitions and invariants *)
-Definition proto_eq_next {Σ} (p : iProto Σ) : laterO (iProto Σ) -n> iPropO Σ :=
- OfeMor (sbi_internal_eq (Next p)).
-
-Program Definition iProto_le_aux `{invG Σ} (rec : iProto Σ -n> iProto Σ -n> iPropO Σ) :
- iProto Σ -n> iProto Σ -n> iPropO Σ := λne p1 p2,
- ((p1 ≡ proto_end ∗ p2 ≡ proto_end) ∨
- (∃ pc1 pc2,
- p1 ≡ proto_message Send pc1 ∗ p2 ≡ proto_message Send pc2 ∗
- ∀ v p2', pc2 v (proto_eq_next p2') ={⊤}=∗
- ∃ p1', ▷ rec p1' p2' ∗ pc1 v (proto_eq_next p1')) ∨
- (∃ pc1 pc2,
- p1 ≡ proto_message Receive pc1 ∗ p2 ≡ proto_message Receive pc2 ∗
- ∀ v p1', pc1 v (proto_eq_next p1') ={⊤}=∗
- ∃ p2', ▷ rec p1' p2' ∗ pc2 v (proto_eq_next p2')))%I.
-Solve Obligations with solve_proper.
-Local Instance iProto_le_aux_contractive `{invG Σ} : Contractive (@iProto_le_aux Σ _).
-Proof. solve_contractive. Qed.
-Definition iProto_le `{invG Σ} (p1 p2 : iProto Σ) : iProp Σ :=
- fixpoint iProto_le_aux p1 p2.
-Arguments iProto_le {_ _} _%proto _%proto.
-Instance: Params (@iProto_le) 2 := {}.
-
-Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
- match vs with
- | [] => iProto_dual p1 ≡ p2
- | v :: vs => ∃ pc p2',
- p2 ≡ proto_message Receive pc ∗
- pc v (proto_eq_next p2') ∗
- proto_interp vs p1 p2'
- end%I.
-Arguments proto_interp {_} _ _%proto _%proto : simpl nomatch.
-
-Record proto_name := ProtName {
- proto_c_name : chan_name;
- proto_l_name : gname;
- proto_r_name : gname
-}.
-
-Definition to_pre_proto {Σ} (p : iProto Σ) :
- proto val (iPrePropO Σ) (iPrePropO Σ) :=
- proto_map id iProp_fold iProp_unfold p.
-
-Definition proto_own_frag `{!proto_chanG Σ} (γ : proto_name) (s : side)
- (p : iProto Σ) : iProp Σ :=
- own (side_elim s proto_l_name proto_r_name γ) (◯E (Next (to_pre_proto p))).
-
-Definition proto_own_auth `{!proto_chanG Σ} (γ : proto_name) (s : side)
- (p : iProto Σ) : iProp Σ :=
- own (side_elim s proto_l_name proto_r_name γ) (â—E (Next (to_pre_proto p))).
-
-Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
- (∃ vsl vsr pl pr,
- chan_own (proto_c_name γ) Left vsl ∗
- chan_own (proto_c_name γ) Right vsr ∗
- proto_own_auth γ Left pl ∗
- proto_own_auth γ Right pr ∗
- ((⌜vsr = []⌠∗ proto_interp vsl pl pr) ∨
- (⌜vsl = []⌠∗ proto_interp vsr pr pl)))%I.
-
-Definition protoN := nroot .@ "proto".
-
-(** * The connective for ownership of channel ends *)
-Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
- (c : val) (p : iProto Σ) : iProp Σ :=
- (∃ s (c1 c2 : val) γ p',
- ⌜ c = side_elim s c1 c2 ⌠∗
- iProto_le p' p ∗
- proto_own_frag γ s p' ∗
- is_chan protoN (proto_c_name γ) c1 c2 ∗
- inv protoN (proto_inv γ))%I.
-Definition mapsto_proto_aux : seal (@mapsto_proto_def). by eexists. Qed.
-Definition mapsto_proto {Σ pΣ hΣ} := mapsto_proto_aux.(unseal) Σ pΣ hΣ.
-Definition mapsto_proto_eq :
- @mapsto_proto = @mapsto_proto_def := mapsto_proto_aux.(seal_eq).
-Arguments mapsto_proto {_ _ _} _ _%proto.
-Instance: Params (@mapsto_proto) 4 := {}.
-
-Notation "c ↣ p" := (mapsto_proto c p)
- (at level 20, format "c ↣ p").
-
-(** * Proofs *)
-Section proto.
- Context `{!proto_chanG Σ, !heapG Σ}.
- Implicit Types p : iProto Σ.
- Implicit Types TT : tele.
-
- (** ** Non-expansiveness of operators *)
- Lemma iProto_message_contractive {TT} a
- (pc1 pc2 : TT → val * iProp Σ * iProto Σ) n :
- (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
- (∀.. x, dist_later n ((pc1 x).1.2) ((pc2 x).1.2)) →
- (∀.. x, dist_later n ((pc1 x).2) ((pc2 x).2)) →
- iProto_message a pc1 ≡{n}≡ iProto_message a pc2.
- Proof.
- rewrite !tforall_forall=> Hv HP Hp.
- rewrite iProto_message_eq /iProto_message_def.
- f_equiv=> v f /=. apply bi.exist_ne=> x.
- repeat (apply Hv || apply HP || apply Hp || f_contractive || f_equiv).
- Qed.
- Lemma iProto_message_ne {TT} a
- (pc1 pc2 : TT → val * iProp Σ * iProto Σ) n :
- (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
- (∀.. x, (pc1 x).1.2 ≡{n}≡ (pc2 x).1.2) →
- (∀.. x, (pc1 x).2 ≡{n}≡ (pc2 x).2) →
- iProto_message a pc1 ≡{n}≡ iProto_message a pc2.
- Proof.
- rewrite !tforall_forall=> Hv HP Hp.
- apply iProto_message_contractive; apply tforall_forall; eauto using dist_dist_later.
- Qed.
- Lemma iProto_message_proper {TT} a
- (pc1 pc2 : TT → val * iProp Σ * iProto Σ) :
- (∀.. x, (pc1 x).1.1 = (pc2 x).1.1) →
- (∀.. x, (pc1 x).1.2 ≡ (pc2 x).1.2) →
- (∀.. x, (pc1 x).2 ≡ (pc2 x).2) →
- iProto_message a pc1 ≡ iProto_message a pc2.
- Proof.
- rewrite !tforall_forall=> Hv HP Hp. apply equiv_dist => n.
- apply iProto_message_ne; apply tforall_forall=> x; by try apply equiv_dist.
- Qed.
-
- Global Instance iProto_branch_contractive n a :
- Proper (dist_later n ==> dist_later n ==>
- dist_later n ==> dist_later n ==> dist n) (@iProto_branch Σ a).
- Proof.
- intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
- apply iProto_message_contractive=> /= -[] //.
- Qed.
- Global Instance iProto_branch_ne n a :
- Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_branch Σ a).
- Proof.
- intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
- by apply iProto_message_ne=> /= -[].
- Qed.
- Global Instance iProto_branch_proper a :
- Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_branch Σ a).
- Proof.
- intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
- by apply iProto_message_proper=> /= -[].
- Qed.
-
- (** ** Dual *)
- Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
- Proof. solve_proper. Qed.
- Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ).
- Proof. apply (ne_proper _). Qed.
- Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ d).
- Proof. solve_proper. Qed.
- Global Instance iProto_dual_if_proper d : Proper ((≡) ==> (≡)) (@iProto_dual_if Σ d).
- Proof. apply (ne_proper _). Qed.
-
- Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ).
- Proof.
- intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
- apply: proto_map_ext=> //. by intros [].
- Qed.
-
- Lemma iProto_dual_end : iProto_dual (Σ:=Σ) END ≡ END%proto.
- Proof. by rewrite iProto_end_eq /iProto_dual proto_map_end. Qed.
- Lemma iProto_dual_message {TT} a (pc : TT → val * iProp Σ * iProto Σ) :
- iProto_dual (iProto_message a pc)
- ≡ iProto_message (action_dual a) (prod_map id iProto_dual ∘ pc).
- Proof.
- rewrite /iProto_dual iProto_message_eq /iProto_message_def proto_map_message.
- by f_equiv=> v f /=.
- Qed.
-
- Lemma iProto_dual_branch a P1 P2 p1 p2 :
- iProto_dual (iProto_branch a P1 P2 p1 p2)
- ≡ iProto_branch (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
- Proof.
- rewrite /iProto_branch iProto_dual_message /=.
- by apply iProto_message_proper=> /= -[].
- Qed.
-
- (** ** Append *)
- Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ).
- Proof. apply _. Qed.
- Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ).
- Proof. apply (ne_proper_2 _). Qed.
-
- Lemma iProto_app_message {TT} a (pc : TT → val * iProp Σ * iProto Σ) p2 :
- (iProto_message a pc <++> p2)%proto
- ≡ iProto_message a (prod_map id (flip iProto_app p2) ∘ pc).
- Proof.
- rewrite /iProto_app iProto_message_eq /iProto_message_def proto_app_message.
- by f_equiv=> v f /=.
- Qed.
-
- Global Instance iProto_app_end_l : LeftId (≡) END%proto (@iProto_app Σ).
- Proof.
- intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_l.
- Qed.
- Global Instance iProto_app_end_r : RightId (≡) END%proto (@iProto_app Σ).
- Proof.
- intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
- Qed.
- Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ).
- Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.
-
- Lemma iProto_app_branch a P1 P2 p1 p2 q :
- (iProto_branch a P1 P2 p1 p2 <++> q)%proto
- ≡ (iProto_branch a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
- Proof.
- rewrite /iProto_branch iProto_app_message.
- by apply iProto_message_proper=> /= -[].
- Qed.
-
- Lemma iProto_dual_app p1 p2 :
- iProto_dual (p1 <++> p2) ≡ (iProto_dual p1 <++> iProto_dual p2)%proto.
- Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.
-
- (** ** Protocol entailment **)
- Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ _).
- Proof. solve_proper. Qed.
- Global Instance iProto_le_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ _).
- Proof. solve_proper. Qed.
-
- Lemma iProto_le_unfold p1 p2 :
- iProto_le p1 p2 ≡ iProto_le_aux (fixpoint iProto_le_aux) p1 p2.
- Proof. apply: (fixpoint_unfold iProto_le_aux). Qed.
-
- Lemma iProto_le_refl p : ⊢ iProto_le p p.
- Proof.
- iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)].
- - rewrite iProto_le_unfold. iLeft; by auto.
- - rewrite iProto_le_unfold. iRight; iLeft. iExists _, _; do 2 (iSplit; [done|]).
- iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
- - rewrite iProto_le_unfold. iRight; iRight. iExists _, _; do 2 (iSplit; [done|]).
- iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
- Qed.
-
- Lemma iProto_le_end_inv p : iProto_le p proto_end -∗ p ≡ proto_end.
- Proof.
- rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
- iDestruct "H" as "[H|H]"; iDestruct "H" as (pc1 pc2) "(_ & Heq & _)";
- by rewrite proto_end_message_equivI.
- Qed.
-
- Lemma iProto_le_send_inv p1 pc2 :
- iProto_le p1 (proto_message Send pc2) -∗ ∃ pc1,
- p1 ≡ proto_message Send pc1 ∗
- ∀ v p2', pc2 v (proto_eq_next p2') ={⊤}=∗
- ∃ p1', ▷ iProto_le p1' p2' ∗ pc1 v (proto_eq_next p1').
- Proof.
- rewrite iProto_le_unfold. iIntros "[[_ Heq]|[H|H]]".
- - by rewrite proto_message_end_equivI.
- - iDestruct "H" as (pc1 pc2') "(Hp1 & Heq & H)".
- iDestruct (proto_message_equivI with "Heq") as "[_ #Heq]".
- iExists pc1. iIntros "{$Hp1}" (v p2') "Hpc".
- iSpecialize ("Heq" $! v). iDestruct (bi.ofe_morO_equivI with "Heq") as "Heq'".
- iRewrite ("Heq'" $! (proto_eq_next p2')) in "Hpc". by iApply "H".
- - iDestruct "H" as (pc1 pc2') "(_ & Heq & _)".
- by iDestruct (proto_message_equivI with "Heq") as "[% ?]".
- Qed.
-
- Lemma iProto_le_recv_inv p1 pc2 :
- iProto_le p1 (proto_message Receive pc2) -∗ ∃ pc1,
- p1 ≡ proto_message Receive pc1 ∗
- ∀ v p1', pc1 v (proto_eq_next p1') ={⊤}=∗
- ∃ p2', ▷ iProto_le p1' p2' ∗ pc2 v (proto_eq_next p2').
- Proof.
- rewrite iProto_le_unfold. iIntros "[[_ Heq]|[H|H]]".
- - by rewrite proto_message_end_equivI.
- - iDestruct "H" as (pc1 pc2') "(_ & Heq & _)".
- by iDestruct (proto_message_equivI with "Heq") as "[% ?]".
- - iDestruct "H" as (pc1 pc2') "(Hp1 & Heq & H)".
- iDestruct (proto_message_equivI with "Heq") as "[_ #Heq]".
- iExists pc1. iIntros "{$Hp1}" (v p1') "Hpc".
- iSpecialize ("Heq" $! v). iDestruct (bi.ofe_morO_equivI with "Heq") as "Heq'".
- iMod ("H" with "Hpc") as (p2') "[Hle Hpc]". iModIntro.
- iExists p2'. iFrame "Hle". by iRewrite ("Heq'" $! (proto_eq_next p2')).
- Qed.
-
- Lemma iProto_le_trans p1 p2 p3 :
- iProto_le p1 p2 -∗ iProto_le p2 p3 -∗ iProto_le p1 p3.
- Proof.
- iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
- destruct (proto_case p3) as [->|([]&pc3&->)].
- - rewrite iProto_le_end_inv. by iRewrite "H2" in "H1".
- - iDestruct (iProto_le_send_inv with "H2") as (pc2) "[Hp2 H3]".
- iRewrite "Hp2" in "H1".
- iDestruct (iProto_le_send_inv with "H1") as (pc1) "[Hp1 H2]".
- iRewrite "Hp1". rewrite iProto_le_unfold; iRight; iLeft.
- iExists _, _; do 2 (iSplit; [done|]).
- iIntros (v p3') "Hpc".
- iMod ("H3" with "Hpc") as (p2') "[Hle Hpc]".
- iMod ("H2" with "Hpc") as (p1') "[Hle' Hpc]".
- iExists p1'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle'").
- - iDestruct (iProto_le_recv_inv with "H2") as (pc2) "[Hp2 H3]".
- iRewrite "Hp2" in "H1".
- iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H2]".
- iRewrite "Hp1". rewrite iProto_le_unfold; iRight; iRight.
- iExists _, _; do 2 (iSplit; [done|]).
- iIntros (v p1') "Hpc".
- iMod ("H2" with "Hpc") as (p2') "[Hle Hpc]".
- iMod ("H3" with "Hpc") as (p3') "[Hle' Hpc]".
- iExists p3'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle").
- Qed.
-
- Lemma iProto_send_le {TT1 TT2} (pc1 : TT1 → val * iProp Σ * iProto Σ)
- (pc2 : TT2 → val * iProp Σ * iProto Σ) :
- (∀.. x2 : TT2, ▷ (pc2 x2).1.2 ={⊤}=∗ ∃.. x1 : TT1,
- ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌠∗
- ▷ (pc1 x1).1.2 ∗
- ▷ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
- iProto_le (iProto_message Send pc1) (iProto_message Send pc2).
- Proof.
- iIntros "H". rewrite iProto_le_unfold iProto_message_eq. iRight; iLeft.
- iExists _, _; do 2 (iSplit; [done|]).
- iIntros (v p2') "/=". iDestruct 1 as (x2 ->) "[Hpc #Heq]".
- iMod ("H" with "Hpc") as (x1 ?) "[Hpc Hle]".
- iExists (pc1 x1).2. iSplitL "Hle".
- { iIntros "!> !>". change (fixpoint iProto_le_aux ?p1 ?p2) with (iProto_le p1 p2).
- by iRewrite "Heq". }
- iModIntro. iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
- Qed.
-
- Lemma iProto_recv_le {TT1 TT2} (pc1 : TT1 → val * iProp Σ * iProto Σ)
- (pc2 : TT2 → val * iProp Σ * iProto Σ) :
- (∀.. x1 : TT1, ▷ (pc1 x1).1.2 ={⊤}=∗ ∃.. x2 : TT2,
- ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌠∗
- ▷ (pc2 x2).1.2 ∗
- ▷ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
- iProto_le (iProto_message Receive pc1) (iProto_message Receive pc2).
- Proof.
- iIntros "H". rewrite iProto_le_unfold iProto_message_eq. iRight; iRight.
- iExists _, _; do 2 (iSplit; [done|]).
- iIntros (v p1') "/=". iDestruct 1 as (x1 ->) "[Hpc #Heq]".
- iMod ("H" with "Hpc") as (x2 ?) "[Hpc Hle]". iExists (pc2 x2).2. iSplitL "Hle".
- { iIntros "!> !>". change (fixpoint iProto_le_aux ?p1 ?p2) with (iProto_le p1 p2).
- by iRewrite "Heq". }
- iModIntro. iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
- Qed.
-
- Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ iProto_le p1 p2 -∗ c ↣ p2.
- Proof.
- rewrite mapsto_proto_eq. iDestruct 1 as (s c1 c2 γ p1' ->) "[Hle H]".
- iIntros "Hle'". iExists s, c1, c2, γ, p1'. iSplit; first done. iFrame "H".
- by iApply (iProto_le_trans with "Hle").
- Qed.
-
- (** ** Lemmas about the auxiliary definitions and invariants *)
- Global Instance proto_interp_ne : NonExpansive2 (proto_interp (Σ:=Σ) vs).
- Proof. induction vs; solve_proper. Qed.
- Global Instance proto_interp_proper vs :
- Proper ((≡) ==> (≡) ==> (≡)) (proto_interp (Σ:=Σ) vs).
- Proof. apply (ne_proper_2 _). Qed.
-
- Global Instance to_pre_proto_ne : NonExpansive (to_pre_proto (Σ:=Σ)).
- Proof. solve_proper. Qed.
- Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
- Proof. solve_proper. Qed.
- Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
- Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
- Global Instance mapsto_proto_proper c : Proper ((≡) ==> (≡)) (mapsto_proto c).
- Proof. apply (ne_proper _). Qed.
-
- Lemma proto_own_auth_agree γ s p p' :
- proto_own_auth γ s p -∗ proto_own_frag γ s p' -∗ ▷ (p ≡ p').
- Proof.
- iIntros "Hauth Hfrag".
- iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
- iDestruct (excl_auth_agreeI with "Hvalid") as "Hvalid".
- iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
- rewrite /to_pre_proto. assert (∀ p,
- proto_map id iProp_unfold iProp_fold (proto_map id iProp_fold iProp_unfold p) ≡ p) as help.
- { intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
- apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. }
- rewrite -{2}(help p). iRewrite "Hvalid". by rewrite help.
- Qed.
-
- Lemma proto_own_auth_update γ s p p' p'' :
- proto_own_auth γ s p -∗ proto_own_frag γ s p' ==∗
- proto_own_auth γ s p'' ∗ proto_own_frag γ s p''.
- Proof.
- iIntros "Hauth Hfrag".
- iDestruct (own_update_2 with "Hauth Hfrag") as "H".
- { eapply (excl_auth_update _ _ (Next (to_pre_proto p''))). }
- by rewrite own_op.
- Qed.
-
- Lemma proto_eq_next_dual p :
- ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next (iProto_dual p)) ≡
- proto_eq_next p.
- Proof.
- intros lp. iSplit; iIntros "Hlp /="; last by iRewrite -"Hlp".
- destruct (Next_uninj lp) as [p' ->].
- rewrite /later_map /= !bi.later_equivI. iNext.
- rewrite -{2}(involutive iProto_dual p) -{2}(involutive iProto_dual p').
- by iRewrite "Hlp".
- Qed.
-
- Lemma proto_interp_send v vs pc p1 p2 :
- proto_interp vs (proto_message Send pc) p2 -∗
- pc v (proto_eq_next p1) -∗
- proto_interp (vs ++ [v]) p1 p2.
- Proof.
- iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
- - iDestruct "Heval" as "#Heval".
- iExists _, (iProto_dual p1). iSplit.
- { iRewrite -"Heval". by rewrite /iProto_dual proto_map_message. }
- rewrite /= proto_eq_next_dual; auto.
- - iDestruct "Heval" as (pc' p2') "(Heq & Hc' & Heval)".
- iExists pc', p2'. iFrame "Heq Hc'". iApply ("IH" with "Heval Hc").
- Qed.
-
- Lemma proto_interp_recv v vs p1 pc :
- proto_interp (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2,
- pc v (proto_eq_next p2) ∗
- proto_interp vs p1 p2.
- Proof.
- simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
- iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]".
- iSpecialize ("Heq" $! v). rewrite bi.ofe_morO_equivI.
- by iRewrite ("Heq" $! (proto_eq_next p2)).
- Qed.
-
- Lemma proto_interp_False p pc v vs :
- proto_interp (v :: vs) p (proto_message Send pc) -∗ False.
- Proof.
- simpl. iDestruct 1 as (pc' p2') "[Heq _]".
- by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
- Qed.
-
- Lemma proto_interp_nil p1 p2 : proto_interp [] p1 p2 -∗ p1 ≡ iProto_dual p2.
- Proof. iIntros "#H /=". iRewrite -"H". by rewrite involutive. Qed.
-
- Arguments proto_interp : simpl never.
-
- (** ** Helper lemma for initialization of a channel *)
- Lemma proto_init E cγ c1 c2 p :
- is_chan protoN cγ c1 c2 -∗
- chan_own cγ Left [] -∗ chan_own cγ Right [] ={E}=∗
- c1 ↣ p ∗ c2 ↣ iProto_dual p.
- Proof.
- iIntros "#Hcctx Hcol Hcor".
- iMod (own_alloc (â—E (Next (to_pre_proto p)) â‹…
- ◯E (Next (to_pre_proto p)))) as (lγ) "[Hlsta Hlstf]".
- { by apply excl_auth_valid. }
- iMod (own_alloc (â—E (Next (to_pre_proto (iProto_dual p))) â‹…
- ◯E (Next (to_pre_proto (iProto_dual p))))) as (rγ) "[Hrsta Hrstf]".
- { by apply excl_auth_valid. }
- pose (ProtName cγ lγ rγ) as pγ.
- iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
- { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
- iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
- - iExists Left, c1, c2, pγ, p.
- iFrame "Hlstf Hinv Hcctx". iSplit; [done|]. iApply iProto_le_refl.
- - iExists Right, c1, c2, pγ, (iProto_dual p).
- iFrame "Hrstf Hinv Hcctx". iSplit; [done|]. iApply iProto_le_refl.
- Qed.
-
- (** ** Accessor style lemmas, used as helpers to prove the specifications of
- [send] and [recv]. *)
- Lemma proto_send_acc {TT} c (pc : TT → val * iProp Σ * iProto Σ) (x : TT) :
- c ↣ iProto_message Send pc -∗
- (pc x).1.2 -∗
- ∃ s c1 c2 γ,
- ⌜ c = side_elim s c1 c2 ⌠∗
- is_chan protoN (proto_c_name γ) c1 c2 ∗ |={⊤,⊤∖↑protoN}=> ∃ vs,
- chan_own (proto_c_name γ) s vs ∗
- ▷ (chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={⊤∖↑protoN,⊤}=∗
- c ↣ (pc x).2).
- Proof.
- rewrite {1}mapsto_proto_eq iProto_message_eq. iIntros "Hc HP".
- iDestruct "Hc" as (s c1 c2 γ p ->) "(Hle & Hst & #[Hcctx Hinv])".
- iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
- iDestruct (iProto_le_send_inv with "Hle") as (pc') "[Hp H] /=".
- iRewrite "Hp" in "Hst"; clear p.
- iMod ("H" with "[HP]") as (p1') "[Hle HP]".
- { iExists _. iFrame "HP". by iSplit. }
- iInv protoN as (l r pl pr) "(>Hcl & >Hcr & Hstla & Hstra & Hinv')" "Hclose".
- (* TODO: refactor to avoid twice nearly the same proof *)
- iModIntro. destruct s.
- - iExists _. iIntros "{$Hcl} !> Hcl".
- iDestruct (proto_own_auth_agree with "Hstla Hst") as "#Heq".
- iMod (proto_own_auth_update _ _ _ _ p1' with "Hstla Hst") as "[Hstla Hst]".
- iMod ("Hclose" with "[-Hst Hle]") as "_".
- { iNext. iExists _,_,_,_. iFrame "Hcr Hstra Hstla Hcl". iLeft.
- iRewrite "Heq" in "Hinv'".
- iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- { iSplit=> //. by iApply (proto_interp_send with "Heval [HP]"). }
- destruct r as [|vr r]; last first.
- { iDestruct (proto_interp_False with "Heval") as %[]. }
- iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
- iApply (proto_interp_send _ [] with "[//] HP"). }
- iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, p1'.
- by iFrame "Hcctx Hinv Hst Hle".
- - iExists _. iIntros "{$Hcr} !> Hcr".
- iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Heq".
- iMod (proto_own_auth_update _ _ _ _ p1' with "Hstra Hst") as "[Hstra Hst]".
- iMod ("Hclose" with "[-Hst Hle]") as "_".
- { iNext. iExists _, _, _, _. iFrame "Hcl Hstra Hstla Hcr". iRight.
- iRewrite "Heq" in "Hinv'".
- iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last first.
- { iSplit=> //. by iApply (proto_interp_send with "Heval [HP]"). }
- destruct l as [|vl l]; last first.
- { iDestruct (proto_interp_False with "Heval") as %[]. }
- iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
- iApply (proto_interp_send _ [] with "[//] HP"). }
- iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, p1'.
- by iFrame "Hcctx Hinv Hst Hle".
- Qed.
-
- Lemma proto_recv_acc {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
- c ↣ iProto_message Receive pc -∗
- ∃ s c1 c2 γ,
- ⌜ c = side_elim s c2 c1 ⌠∗
- is_chan protoN (proto_c_name γ) c1 c2 ∗ |={⊤,⊤∖↑protoN}=> ∃ vs,
- chan_own (proto_c_name γ) s vs ∗
- ▷ ((chan_own (proto_c_name γ) s vs ={⊤∖↑protoN,⊤}=∗
- c ↣ iProto_message Receive pc) ∧
- (∀ v vs',
- ⌜ vs = v :: vs' ⌠-∗
- chan_own (proto_c_name γ) s vs' ={⊤∖↑protoN,⊤,⊤}▷=∗ ▷ ∃ x : TT,
- ⌜ v = (pc x).1.1 ⌠∗ c ↣ (pc x).2 ∗ (pc x).1.2)).
- Proof.
- rewrite {1}mapsto_proto_eq iProto_message_eq.
- iDestruct 1 as (s c1 c2 γ p ->) "(Hle & Hst & #[Hcctx Hinv])".
- iDestruct (iProto_le_recv_inv with "Hle") as (pc') "[Hp Hle] /=".
- iRewrite "Hp" in "Hst". clear p.
- iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
- iFrame "Hcctx".
- iInv protoN as (l r pl pr) "(>Hcl & >Hcr & Hstla & Hstra & Hinv')" "Hclose".
- iExists (side_elim s r l). iModIntro.
- (* TODO: refactor to avoid twice nearly the same proof *)
- destruct s; simpl.
- - iIntros "{$Hcr} !>".
- iDestruct (proto_own_auth_agree with "Hstla Hst") as "#Heq".
- iSplit.
- + iIntros "Hcr".
- iMod ("Hclose" with "[-Hst Hle]") as "_".
- { iNext. iExists l, r, _, _. iFrame. }
- iModIntro. rewrite mapsto_proto_eq.
- iExists Left, c1, c2, γ, (proto_message Receive pc').
- iFrame "Hcctx Hinv Hst". iSplit; first done.
- rewrite iProto_le_unfold. iRight; auto 10.
- + iIntros (v vs ->) "Hcr".
- iDestruct "Hinv'" as "[[% _]|[-> Heval]]"; first done.
- iAssert (â–· proto_interp (v :: vs) pr (proto_message Receive pc'))%I
- with "[Heval]" as "Heval".
- { iNext. by iRewrite "Heq" in "Heval". }
- iDestruct (proto_interp_recv with "Heval") as (q) "[Hpc Heval]".
- iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hst") as "[Hstla Hst]".
- iMod ("Hclose" with "[-Hst Hpc Hle]") as %_.
- { iExists _, _,_ ,_; iFrame; eauto. }
- iIntros "!> !>". iMod ("Hle" with "Hpc") as (q') "[Hle H]".
- iDestruct "H" as (x) "(Hv & HP & #Hf) /=".
- iIntros "!> !>". iExists x. iFrame "Hv HP". iRewrite -"Hf".
- rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, q. iFrame; auto.
- - iIntros "{$Hcl} !>".
- iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Heq".
- iSplit.
- + iIntros "Hcl".
- iMod ("Hclose" with "[-Hst Hle]") as "_".
- { iNext. iExists l, r, _, _. iFrame. }
- iModIntro. rewrite mapsto_proto_eq.
- iExists Right, c1, c2, γ, (proto_message Receive pc').
- iFrame "Hcctx Hinv Hst". iSplit; first done.
- rewrite iProto_le_unfold. iRight; auto 10.
- + iIntros (v vs ->) "Hcl".
- iDestruct "Hinv'" as "[[-> Heval]|[% _]]"; last done.
- iAssert (â–· proto_interp (v :: vs) pl (proto_message Receive pc'))%I
- with "[Heval]" as "Heval".
- { iNext. by iRewrite "Heq" in "Heval". }
- iDestruct (proto_interp_recv with "Heval") as (q) "[Hpc Heval]".
- iMod (proto_own_auth_update _ _ _ _ q with "Hstra Hst") as "[Hstra Hst]".
- iMod ("Hclose" with "[-Hst Hpc Hle]") as %_.
- { iExists _, _, _, _. eauto 10 with iFrame. }
- iIntros "!> !>". iMod ("Hle" with "Hpc") as (q') "[Hle H]".
- iDestruct "H" as (x) "(Hv & HP & Hf) /=".
- iIntros "!> !>". iExists x. iFrame "Hv HP". iRewrite -"Hf".
- rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, q. iFrame; auto.
- Qed.
-
- (** ** Specifications of [send] and [recv] *)
- Lemma new_chan_proto_spec :
- {{{ True }}}
- new_chan #()
- {{{ c1 c2, RET (c1,c2); (∀ p, |={⊤}=> c1 ↣ p ∗ c2 ↣ iProto_dual p) }}}.
- Proof.
- iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
- 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) :
- ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
- ▷ (∀ c, c ↣ p -∗ Ψ c) -∗
- WP start_chan f {{ Ψ }}.
- Proof.
- iIntros "Hfork HΨ". wp_lam.
- 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").
- Qed.
-
- Lemma send_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) (x : TT) :
- {{{ c ↣ iProto_message Send pc ∗ (pc x).1.2 }}}
- send c (pc x).1.1
- {{{ RET #(); c ↣ (pc x).2 }}}.
- Proof.
- iIntros (Ψ) "[Hp HP] HΨ".
- iDestruct (proto_send_acc with "Hp HP") as (γ s c1 c2 ->) "[#Hc Hvs]".
- iApply (send_spec with "[$]"). iMod "Hvs" as (vs) "[Hch H]".
- iModIntro. iExists vs. iFrame "Hch".
- iIntros "!> Hvs". iApply "HΨ".
- iMod ("H" with "Hvs"); auto.
- Qed.
-
- (** A version written without Texan triples that is more convenient to use
- (via [iApply] in Coq. *)
- Lemma send_proto_spec {TT} Ψ c v (pc : TT → val * iProp Σ * iProto Σ) :
- c ↣ iProto_message Send pc -∗
- (∃.. x : TT,
- ⌜ v = (pc x).1.1 ⌠∗ (pc x).1.2 ∗ ▷ (c ↣ (pc x).2 -∗ Ψ #())) -∗
- WP send c v {{ Ψ }}.
- Proof.
- iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]".
- by iApply (send_proto_spec_packed with "[$]").
- Qed.
-
- Lemma try_recv_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
- {{{ c ↣ iProto_message Receive pc }}}
- try_recv c
- {{{ v, RET v; (⌜v = NONEV⌠∧ c ↣ iProto_message Receive pc) ∨
- (∃ x : TT, ⌜v = SOMEV ((pc x).1.1)⌠∗ c ↣ (pc x).2 ∗ (pc x).1.2) }}}.
- Proof.
- iIntros (Ψ) "Hp HΨ".
- iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]".
- wp_apply (try_recv_spec with "[$]"). iSplit.
- - iMod "Hvs" as (vs) "[Hch [H _]]".
- iIntros "!> !>". iMod ("H" with "Hch") as "Hch". iApply "HΨ"; auto.
- - iMod "Hvs" as (vs) "[Hch [_ H]]".
- iIntros "!>". iExists vs. iIntros "{$Hch} !>" (v vs' ->) "Hch".
- iMod ("H" with "[//] Hch") as "H". iIntros "!> !>". iMod "H".
- iIntros "!> !>". iDestruct "H" as (x ->) "H". iApply "HΨ"; auto.
- Qed.
-
- Lemma recv_proto_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
- {{{ c ↣ iProto_message Receive pc }}}
- recv c
- {{{ x, RET (pc x).1.1; c ↣ (pc x).2 ∗ (pc x).1.2 }}}.
- Proof.
- iIntros (Ψ) "Hp HΨ".
- iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]".
- wp_apply (recv_spec with "[$]"). iMod "Hvs" as (vs) "[Hch [_ H]]".
- iModIntro. iExists vs. iIntros "{$Hch} !>" (v vs' ->) "Hvs'".
- iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !>". iMod "H".
- iIntros "!> !>". iDestruct "H" as (x ->) "H". by iApply "HΨ".
- Qed.
-
- (** A version written without Texan triples that is more convenient to use
- (via [iApply] in Coq. *)
- Lemma recv_proto_spec {TT} Ψ c (pc : TT → val * iProp Σ * iProto Σ) :
- c ↣ iProto_message Receive pc -∗
- ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Ψ (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.
-
- (** ** Specifications for branching *)
- Lemma select_spec c (b : bool) P1 P2 p1 p2 :
- {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}
- send c #b
- {{{ RET #(); c ↣ (if b then p1 else p2) }}}.
- Proof.
- rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
- iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
- Qed.
-
- Lemma branch_spec c P1 P2 p1 p2 :
- {{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
- recv c
- {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
- Proof.
- rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
- iApply (recv_proto_spec with "Hc"); simpl.
- iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
- Qed.
-End proto.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 7e224b2f401ceb80214ca1ae6809ca3bccefa394..3d11b9c60adb65ee134c7f51bcd39141bc2fb360 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -1,8 +1,9 @@
-(** This file defines the model of dependent separation protocols, along with
-various operations, such as append and map.
+(** This file defines the model of dependent separation protocols as the
+solution of a recursive domain equation, along with various primitive
+operations, such as append and map.
Important: This file should not be used directly, but rather the wrappers in
-[proto_channel] should be used.
+[proto] should be used.
Dependent Separation Protocols are modeled as the solution of the following
recursive domain equation:
@@ -98,7 +99,7 @@ Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Lemma proto_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 pc1 pc2 :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 pc1 ≡ proto_message a2 pc2
- ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧ (∀ v, pc1 v ≡ pc2 v).
+ ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧ (∀ v pc', pc1 v pc' ≡ pc2 v pc').
Proof.
trans (proto_unfold (proto_message a1 pc1) ≡ proto_unfold (proto_message a2 pc2) : SPROP)%I.
{ iSplit.
@@ -106,7 +107,7 @@ Proof.
- iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
iRewrite "Heq". by rewrite proto_fold_unfold. }
rewrite /proto_message !proto_unfold_fold bi.option_equivI bi.prod_equivI /=.
- by rewrite bi.discrete_fun_equivI bi.discrete_eq.
+ rewrite bi.discrete_fun_equivI bi.discrete_eq. by setoid_rewrite bi.ofe_morO_equivI.
Qed.
Lemma proto_message_end_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a pc :
proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a pc ≡ proto_end ⊢@{SPROP} False.
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 4cbc6daf1c14d9fba460928c160fc79c43f00e74..533cb996e8c4deee5e535cacd338054da35ac8e3 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -1,7 +1,7 @@
(** This file includes basic examples that each describe a unique feature of
dependent separation protocols. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation lib.spin_lock.
+From actris.channel Require Import proofmode.
+From iris.heap_lang Require Import lib.spin_lock.
From actris.utils Require Import contribution.
(** Basic *)
@@ -87,7 +87,7 @@ Definition prog_lock : val := λ: <>,
recv "c" + recv "c".
Section proofs.
-Context `{heapG Σ, proto_chanG Σ}.
+Context `{heapG Σ, chanG Σ}.
(** Protocols for the respective programs *)
Definition prot : iProto Σ :=
@@ -146,7 +146,7 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot); iIntros (c) "Hc".
- by wp_send with "[]".
- wp_recv as "_". by iApply "HΦ".
Qed.
@@ -154,7 +154,7 @@ Qed.
Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_ref); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
- wp_alloc l as "Hl". by wp_send with "[$Hl]".
- wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
Qed.
@@ -162,17 +162,16 @@ Qed.
Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_del); iIntros (c) "Hc".
- - wp_apply (new_chan_proto_spec with "[//]").
- iIntros (c2 c2') "Hcc2". iMod ("Hcc2" $! prot) as "[Hc2 Hc2']".
- wp_send with "[$Hc2]". by wp_send with "[]".
+ wp_apply (start_chan_spec prot_del); iIntros (c) "Hc".
+ - wp_apply (new_chan_spec prot with "[//]").
+ iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_dep); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
- wp_recv (x) as "_". by wp_send with "[]".
- wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
Qed.
@@ -180,7 +179,7 @@ Qed.
Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_dep_ref); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
- wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
- wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
by iApply "HΦ".
@@ -189,9 +188,8 @@ Qed.
Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_dep_del); iIntros (c) "Hc".
- - wp_apply (new_chan_proto_spec with "[//]").
- iIntros (c2 c2') "Hcc2". iMod ("Hcc2" $! prot_dep) as "[Hc2 Hc2']".
+ wp_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
+ - wp_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
- wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
by iApply "HΦ".
@@ -200,9 +198,9 @@ Qed.
Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_dep_del_2); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
- wp_apply (start_chan_proto_spec prot_dep); iIntros (c2) "Hc2".
+ wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
Qed.
@@ -210,10 +208,10 @@ Qed.
Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_dep_del_3); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
{ wp_recv (c2) as "Hc2". wp_recv (y) as "_".
wp_send with "[//]". by wp_send with "[$Hc2]". }
- wp_apply (start_chan_proto_spec prot_dep); iIntros (c2) "Hc2".
+ wp_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
{ wp_recv (x) as "_". by wp_send with "[//]". }
wp_send with "[$Hc2]". wp_send with "[//]".
wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -222,7 +220,7 @@ Qed.
Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_loop); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
- iAssert (∀ Ψ, WP (rec: "go" <> := let: "x" := recv c in
send c ("x" + #2) ;; "go" #())%V #() {{ Ψ }})%I with "[Hc]" as "H".
{ iIntros (Ψ). iLöb as "IH". wp_recv (x) as "_". wp_send with "[//]".
@@ -235,7 +233,7 @@ Qed.
Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec prot_fun); iIntros (c) "Hc".
+ wp_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
- wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
iIntros "!>" (Ψ') "HP HΨ'". wp_apply ("Hf" with "HP"); iIntros (x) "HΨ".
wp_pures. by iApply "HΨ'".
@@ -250,8 +248,8 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
{{{ True }}} prog_lock #() {{{ RET #42; True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_apply (start_chan_proto_spec (prot_lock 2)); iIntros (c) "Hc".
- - iMod (contribution_init) as (γ) "Hs".
+ wp_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
+ - iMod contribution_init as (γ) "Hs".
iMod (alloc_client with "Hs") as "[Hs Hcl1]".
iMod (alloc_client with "Hs") as "[Hs Hcl2]".
wp_apply (newlock_spec nroot (∃ n, server γ n ε ∗
diff --git a/theories/examples/map.v b/theories/examples/map.v
index 7bd7d6ecfd8b19dc1249f1765e76da4c4c4db0e7..5a94125636cfd43d5fa10bb8a3da6cb5bc95871f 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -1,7 +1,7 @@
(** This file implements a distributed mapper service, a specification thereof,
and its proofs. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation lib.spin_lock.
+From actris.channel Require Import proofmode.
+From iris.heap_lang Require Import lib.spin_lock.
From actris.utils Require Import llist contribution.
From iris.algebra Require Import gmultiset.
@@ -60,7 +60,7 @@ Class mapG Σ A `{Countable A} := {
Section map.
Context `{Countable A} {B : Type}.
- Context `{!heapG Σ, !proto_chanG Σ, !mapG Σ A}.
+ Context `{!heapG Σ, !chanG Σ, !mapG Σ A}.
Context (IA : A → val → iProp Σ) (IB : B → val → iProp Σ) (map : A → list B).
Local Open Scope nat_scope.
Implicit Types n : nat.
@@ -202,7 +202,7 @@ Section map.
{{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌠∗ llist IB l ys }}}.
Proof.
iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
- wp_apply (start_chan_proto_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
+ wp_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
{ wp_apply (par_map_service_spec with "Hmap Hc"); auto. }
wp_pures. wp_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
wp_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 77964506070a112a902ff84c0e7d8aac2c5b3484..7e1ccfb7d51fef6fa65aebf7dd693c706b54b857 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -1,7 +1,6 @@
(** This file implements a simple distributed map-reduce function, a
specification thereof, and its proofs. *)
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
From actris.utils Require Import llist compare contribution group.
From actris.examples Require Import map sort_fg.
From iris.algebra Require Import gmultiset.
@@ -97,7 +96,7 @@ Class map_reduceG Σ A B `{Countable A, Countable B} := {
Section mapper.
Context `{Countable A, Countable B} {C : Type}.
- Context `{!heapG Σ, !proto_chanG Σ, !map_reduceG Σ A B}.
+ Context `{!heapG Σ, !chanG Σ, !map_reduceG Σ A B}.
Context (IA : A → val → iProp Σ) (IB : Z → B → val → iProp Σ) (IC : C → val → iProp Σ).
Context (map : A → list (Z * B)) (red : Z → list B → list C).
Context `{!∀ j, Proper ((≡ₚ) ==> (≡ₚ)) (red j)}.
@@ -282,10 +281,10 @@ Section mapper.
{{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌠∗ llist IC l zs }}}.
Proof.
iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
- wp_apply (start_chan_proto_spec (par_map_protocol IA IZB map n ∅));
+ wp_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
iIntros (cmap) "// Hcmap".
{ wp_pures. wp_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
- wp_apply (start_chan_proto_spec (sort_fg_protocol IZB RZB <++> END)%proto);
+ wp_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
iIntros (csort) "Hcsort".
{ wp_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
iApply RZB_cmp_spec. }
@@ -293,7 +292,7 @@ Section mapper.
wp_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
- wp_apply (start_chan_proto_spec (par_map_protocol IZBs IC (curry red) m ∅));
+ wp_apply (start_chan_spec (par_map_protocol IZBs IC (curry red) m ∅));
iIntros (cred) "// Hcred".
{ wp_pures. wp_apply (par_map_service_spec with "Hred Hcred"); auto. }
wp_branch as %_|%Hnil; last first.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 099b912a49627ffbe1318bcad8d4339e6b9bf897..d4d3b2c2efbb17fc71ef20680d63afc88ebc2ab5 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -6,8 +6,7 @@ thereof, and its proofs. There are two variants:
- [sort_service_func]: a service that only takes a channel as its argument. The
comparison function is sent over the channel. *)
From stdpp Require Import sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
From actris.utils Require Export llist compare.
Definition lmerge : val :=
@@ -43,7 +42,7 @@ Definition sort_client_func : val := λ: "cmp" "xs",
recv "c".
Section sort.
- Context `{!heapG Σ, !proto_chanG Σ}.
+ Context `{!heapG Σ, !chanG Σ}.
Definition sort_protocol {A} (I : A → val → iProp Σ) (R : A → A → Prop) : iProto Σ :=
(<!> (xs : list A) (l : loc), MSG #l {{ llist I l xs }};
@@ -106,10 +105,10 @@ Section sort.
wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
wp_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
iDestruct 1 as (->) "[Hl1 Hl2]".
- wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cy) "Hcy".
+ wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcy"); auto. }
- wp_apply (start_chan_proto_spec (sort_protocol I R)); iIntros (cz) "Hcz".
+ wp_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
{ rewrite -{2}(right_id END%proto _ (iProto_dual _)).
wp_apply ("IH" with "Hcz"); auto. }
wp_send with "[$Hl1]".
@@ -142,7 +141,7 @@ Section sort.
{{{ ys, RET #(); ⌜Sorted R ys⌠∗ ⌜ys ≡ₚ xs⌠∗ llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
- wp_apply (start_chan_proto_spec sort_protocol_func); iIntros (c) "Hc".
+ wp_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
{ rewrite -(right_id END%proto _ (iProto_dual _)).
wp_apply (sort_service_func_spec with "Hc"); auto. }
wp_send with "[$Hcmp]".
diff --git a/theories/examples/sort_br_del.v b/theories/examples/sort_br_del.v
index 7666bff72b3ce6e3b6409bc259bd599e1f632524..b5c85f43ad8e0f21643c79dd281b79fc3032b91d 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -8,8 +8,7 @@ sort, demonstrating Actris's support for delegation and branching:
- [sort_service_br_del]: a service that allows one to sort a series of list by
forking itself. *)
From stdpp Require Import sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
From actris.examples Require Import sort.
Definition sort_service_br : val :=
@@ -35,7 +34,7 @@ Definition sort_service_br_del : val :=
else #().
Section sort_service_br_del.
- Context `{!heapG Σ, !proto_chanG Σ}.
+ Context `{!heapG Σ, !chanG Σ}.
Context {A} (I : A → val → iProp Σ) (R : A → A → Prop) `{!RelDecision R, !Total R}.
Definition sort_protocol_br_aux (rec : iProto Σ) : iProto Σ :=
@@ -77,8 +76,7 @@ Section sort_service_br_del.
Proof.
iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
wp_rec. wp_branch; wp_pures.
- { wp_apply (start_chan_proto_spec (sort_protocol I R <++> END)%proto);
- iIntros (c') "Hc'".
+ { wp_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
{ wp_pures. wp_apply (sort_service_spec with "Hcmp Hc'"); auto. }
wp_send with "[$Hc']". by wp_apply ("IH" with "Hc"). }
by iApply "HΨ".
@@ -104,7 +102,7 @@ Section sort_service_br_del.
{ wp_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
wp_branch; wp_pures.
- { wp_apply (start_chan_proto_spec sort_protocol_br_del); iIntros (c') "Hc'".
+ { wp_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
{ wp_apply ("IH" with "Hc'"); auto. }
wp_send with "[$Hc']".
by wp_apply ("IH" with "Hc"). }
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index 6612052d7ded31322336d3a49a98f9edfa810a96..f7a45651b287633e0779291520d0f6dcb37ae8e4 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -3,8 +3,7 @@ specification thereof, and its proofs. We call this version fine-grained because
the lists are not transmitted using a single message, but using a series of
messages. *)
From stdpp Require Export sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
+From actris.channel Require Import proofmode.
From iris.heap_lang Require Import assert.
From actris.utils Require Import llist compare.
@@ -73,7 +72,7 @@ Definition sort_client_fg : val := λ: "cmp" "xs",
recv_all "c" "xs".
Section sort_fg.
- Context `{!heapG Σ, !proto_chanG Σ}.
+ Context `{!heapG Σ, !chanG Σ}.
Section sort_fg_inner.
Context {A} (I : A → val → iProp Σ) (R : relation A) `{!RelDecision R, !Total R}.
@@ -222,10 +221,10 @@ Section sort_fg.
wp_rec; wp_pures. wp_branch; wp_pures.
- wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
+ wp_recv (x2 v2) as "HIx2".
- wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
+ wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cy) "Hcy". wp_apply ("IH" with "Hcy"). auto. }
iIntros (cy) "Hcy".
- wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto).
+ wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
{ iIntros (cz) "Hcz". wp_apply ("IH" with "Hcz"); auto. }
iIntros (cz) "Hcz". rewrite !right_id.
wp_select. wp_send with "[$HIx1]".
@@ -241,7 +240,7 @@ Section sort_fg.
wp_select. by iApply "HΨ".
- wp_select. by iApply "HΨ".
Qed.
-
+
Lemma send_all_spec c p xs' l xs :
{{{ llist I l xs ∗ c ↣ (sort_fg_head_protocol xs' <++> p) }}}
send_all c #l
@@ -282,8 +281,7 @@ Section sort_fg.
{{{ ys, RET #(); ⌜Sorted R ys⌠∗ ⌜ys ≡ₚ xs⌠∗ llist I l ys }}}.
Proof.
iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
- wp_apply (start_chan_proto_spec (sort_fg_protocol <++> END)%proto);
- iIntros (c) "Hc".
+ wp_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
{ wp_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
wp_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
wp_select.
diff --git a/theories/utils/skip.v b/theories/utils/skip.v
new file mode 100644
index 0000000000000000000000000000000000000000..6d154ded31844ccfc1c04a9b37fc085edb4773b3
--- /dev/null
+++ b/theories/utils/skip.v
@@ -0,0 +1,11 @@
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+
+Definition skipN : val :=
+ rec: "go" "n" := if: #0 < "n" then "go" ("n" - #1) else #().
+
+Lemma skipN_spec `{heapG Σ} Φ (n : nat) : ▷^n (Φ #()) -∗ WP skipN #n {{ Φ }}.
+Proof.
+ iIntros "HΦ". iInduction n as [|n] "IH"; wp_rec; wp_pures; [done|].
+ rewrite Z.sub_1_r Nat2Z.inj_succ Z.pred_succ. by iApply "IH".
+Qed.