diff --git a/_CoqProject b/_CoqProject
index bc90218fb2771f0c20f1d1a7e13999ce890575c7..de64737d4ae659a03f0246cb09dba0a0764f8e08 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,9 +5,9 @@ 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..622e9b372d9ae6181a4f08046b91eae98b5ea40c 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_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_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_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Φ". 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_proto_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_proto_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..2ee4e79faa27d842c3ee0c8b1b688502aa524e6e 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) →
@@ -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) →
@@ -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_channel.v b/theories/channel/proto.v
similarity index 52%
rename from theories/channel/proto_channel.v
rename to theories/channel/proto.v
index ee12d19f6f74534def22d2e96ba5d93a95577da1..82b3dd00521e962e9185b66cc2237dd850bddf0e 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto.v
@@ -1,17 +1,10 @@
-(** 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.
+(** 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 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:
+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.
@@ -26,57 +19,43 @@ 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.
+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.
-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)))))
+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Σ {Σ} : subG proto_chanΣ Σ → proto_chanG Σ.
-Proof. intros [??%subG_inG]%subG_inv. constructor; apply _. Qed.
+Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
+Proof. solve_inG. Qed.
(** * Types *)
-Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
+Definition iProto Σ V := proto V (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_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 {_}.
+Arguments iProto_end {_ _}.
-Program Definition iProto_message_def {Σ} {TT : tele} (a : action)
- (pc : TT → val * iProp Σ * iProto Σ) : iProto Σ :=
+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 ⌠∗
@@ -87,8 +66,8 @@ 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 := {}.
+Arguments iProto_message {_ _ _} _ _%proto.
+Instance: Params (@iProto_message) 4 := {}.
Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
(iProto_message
@@ -166,37 +145,22 @@ Notation "<?> 'MSG' v ; p" :=
Notation "'END'" := iProto_end : proto_scope.
(** * Operations *)
-Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
+Definition iProto_dual {Σ V} (p : iProto Σ V) : iProto Σ V :=
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 Σ :=
+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) 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 := {}.
+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 {Σ} (p : iProto Σ) : laterO (iProto Σ) -n> iPropO Σ :=
+Definition proto_eq_next {Σ V} (p : iProto Σ V) : laterO (iProto Σ V) -n> iPropO Σ :=
OfeMor (sbi_internal_eq (Next p)).
(*
@@ -219,8 +183,8 @@ Example:
------------------------------------
?P.?Q.!R <: !R.?P.?Q
*)
-Definition iProto_le_pre {Σ}
- (rec : iProto Σ → iProto Σ → iProp Σ) (p1 p2 : iProto Σ) : iProp Σ :=
+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 ∗
@@ -242,25 +206,26 @@ Definition iProto_le_pre {Σ}
pc2' v1 (proto_eq_next pt)
| Send, Receive => False
end.
-Instance iProto_le_pre_ne {Σ} (rec : iProto Σ → iProto Σ → iProp Σ) :
+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' {Σ}
- (rec : iProto Σ -n> iProto Σ -n> iPropO Σ) : iProto Σ -n> iProto Σ -n> iPropO Σ :=
+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 {Σ} : Contractive (@iProto_le_pre' Σ).
+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 {Σ} (p1 p2 : iProto Σ) : iProp Σ := fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_} _%proto _%proto.
-Instance: Params (@iProto_le) 1 := {}.
+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 proto_interp_aux {Σ} (n : nat)
- (vsl vsr : list val) (pl pr : iProto Σ) : iProp Σ :=
+Fixpoint iProto_interp_aux {Σ V} (n : nat)
+ (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
match n with
| 0 => ∃ p,
⌜ vsl = [] ⌠∗
@@ -272,73 +237,56 @@ Fixpoint proto_interp_aux {Σ} (n : nat)
⌜ vsl = vl :: vsl' ⌠∗
iProto_le (proto_message Receive pc) pr ∗
pc vl (proto_eq_next p2') ∗
- proto_interp_aux n vsl' vsr pl 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') ∗
- proto_interp_aux n vsl vsr' p1' pr)
+ iProto_interp_aux n vsl vsr' p1' pr)
end.
-Definition proto_interp {Σ} (vsl vsr : list val) (pl pr : iProto Σ) : iProp Σ :=
- proto_interp_aux (length vsl + length vsr) vsl vsr pl pr.
-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 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.
-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))).
+Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
-Definition proto_inv `{!invG Σ, 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 ∗
- â–· proto_interp vsl vsr pl pr.
+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 protoN := nroot .@ "proto".
+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 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 γ).
-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").
+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 `{!proto_chanG Σ, !heapG Σ}.
- Implicit Types p pl pr : iProto Σ.
+ 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 → val * iProp Σ * iProto Σ) n :
+ (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)) →
@@ -349,8 +297,7 @@ Section proto.
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 :
+ 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) →
@@ -359,8 +306,7 @@ Section proto.
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 Σ) :
+ 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) →
@@ -370,46 +316,26 @@ Section proto.
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 Σ).
+ Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
Proof. solve_proper. Qed.
- Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ).
+ 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 Σ d).
+ 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 Σ d).
+ 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 Σ).
+ 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 (Σ:=Σ) END ≡ END%proto.
+ 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 → val * iProp Σ * iProto Σ) :
+ 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.
@@ -417,23 +343,16 @@ Section proto.
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.
-
(** Helpers for duals *)
- Global Instance proto_eq_next_ne : NonExpansive (proto_eq_next (Σ:=Σ)).
+ 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 (Σ:=Σ)).
+ 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.
+ 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' ->].
@@ -451,12 +370,12 @@ Section proto.
Qed.
(** ** Append *)
- Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ).
+ Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
Proof. apply _. Qed.
- Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ).
+ Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
Proof. apply (ne_proper_2 _). Qed.
- Lemma iProto_app_message {TT} a (pc : TT → val * iProp Σ * iProto Σ) p2 :
+ 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.
@@ -464,33 +383,25 @@ Section proto.
by f_equiv=> v f /=.
Qed.
- Global Instance iProto_app_end_l : LeftId (≡) END%proto (@iProto_app Σ).
+ 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 Σ).
+ 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 Σ).
+ Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
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 Σ).
+ Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ V).
Proof. solve_proper. Qed.
- Global Instance iProto_le_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ).
+ 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.
@@ -591,8 +502,8 @@ Section proto.
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 Σ) :
+ Lemma iProto_send_le {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 ∗
@@ -608,8 +519,8 @@ Section proto.
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 Σ) :
+ Lemma iProto_recv_le {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 ∗
@@ -624,8 +535,8 @@ Section proto.
iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
Qed.
- Lemma iProto_swap {TT1 TT2} (v1 : TT1 → val) (v2 : TT2 → val)
- (P1 : TT1 → iProp Σ) (P2 : TT2 → iProp Σ) (p : TT1 → TT2 → iProto Σ) :
+ Lemma iProto_swap {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,
@@ -670,56 +581,44 @@ Section proto.
iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
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_aux_ne n vsl vsr :
- NonExpansive2 (proto_interp_aux (Σ:=Σ) n vsl vsr).
+ 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 proto_interp_aux_proper n vsl vsr :
- Proper ((≡) ==> (≡) ==> (≡)) (proto_interp_aux (Σ:=Σ) n vsl vsr).
+ 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 proto_interp_ne vsl vsr : NonExpansive2 (proto_interp (Σ:=Σ) vsl vsr).
+ Global Instance iProto_interp_ne vsl vsr :
+ NonExpansive2 (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
Proof. solve_proper. Qed.
- Global Instance proto_interp_proper vsl vsr :
- Proper ((≡) ==> (≡) ==> (≡)) (proto_interp (Σ:=Σ) vsl vsr).
+ Global Instance iProto_interp_proper vsl vsr :
+ Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
Proof. apply (ne_proper_2 _). Qed.
- Global Instance to_pre_proto_ne : NonExpansive (to_pre_proto (Σ:=Σ)).
+ Global Instance iProto_unfold_ne : NonExpansive (iProto_unfold (Σ:=Σ) (V:=V)).
Proof. solve_proper. Qed.
- Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
+ Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_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').
+ Lemma iProto_own_auth_agree γ s p p' :
+ iProto_own_auth γ s p -∗ iProto_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,
+ 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 "Hvalid". by rewrite help.
+ rewrite -{2}(help p). iRewrite "H✓". 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''.
+ 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 "Hauth Hfrag".
- iDestruct (own_update_2 with "Hauth Hfrag") as "H".
- { eapply (excl_auth_update _ _ (Next (to_pre_proto p''))). }
+ 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.
@@ -732,8 +631,8 @@ Section proto.
(φ1 ↔ φ2) → (φ1 → φ2 → P1 ⊣⊢ P2) → (⌜φ1⌠∗ P1) ⊣⊢ (⌜φ2⌠∗ P2).
Proof. intros -> HP. iSplit; iDestruct 1 as (HÏ•) "H"; rewrite HP; auto. Qed.
- Lemma proto_interp_unfold vsl vsr pl pr :
- proto_interp vsl vsr pl pr ⊣⊢
+ Lemma iProto_interp_unfold vsl vsr pl pr :
+ iProto_interp vsl vsr pl pr ⊣⊢
(∃ p,
⌜ vsl = [] ⌠∗
⌜ vsr = [] ⌠∗
@@ -743,14 +642,14 @@ Section proto.
⌜ vsl = vl :: vsl' ⌠∗
iProto_le (proto_message Receive pc) pr ∗
pc vl (proto_eq_next pr') ∗
- proto_interp vsl' vsr pl 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') ∗
- proto_interp vsl vsr' pl' pr).
+ iProto_interp vsl vsr' pl' pr).
Proof.
- rewrite {1}/proto_interp. destruct vsl as [|vl vsl]; simpl.
+ 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.
@@ -766,18 +665,18 @@ Section proto.
by rewrite ?Nat.add_succ_r.
Qed.
- Lemma proto_interp_nil p : ⊢ proto_interp [] [] p (iProto_dual p).
+ Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
Proof.
- rewrite proto_interp_unfold. iLeft. iExists p. do 2 (iSplit; [done|]).
+ rewrite iProto_interp_unfold. iLeft. iExists p. do 2 (iSplit; [done|]).
iSplitL; iApply iProto_le_refl.
Qed.
- Lemma proto_interp_flip vsl vsr pl pr :
- proto_interp vsl vsr pl pr -∗ proto_interp vsr vsl pr pl.
+ 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 !proto_interp_unfold. iIntros "[H|[H|H]]".
+ 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)".
@@ -788,12 +687,12 @@ Section proto.
iApply ("IH" with "[%] [//] H"); simpl; lia.
Qed.
- Lemma proto_interp_le_l vsl vsr pl pl' pr :
- proto_interp vsl vsr pl pr -∗ iProto_le pl pl' -∗ proto_interp vsl vsr pl' pr.
+ 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 !proto_interp_unfold. iIntros "[H|[H|H]] Hle".
+ 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").
@@ -804,34 +703,34 @@ Section proto.
iRight; iRight. iExists vr, vsr', pc', pl''. iSplit; [done|]; iFrame.
by iApply (iProto_le_trans with "Hpl").
Qed.
- Lemma proto_interp_le_r vsl vsr pl pr pr' :
- proto_interp vsl vsr pl pr -∗ iProto_le pr pr' -∗ proto_interp vsl vsr pl pr'.
+ 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 proto_interp_flip.
- iApply (proto_interp_le_l with "[H] Hle"). by iApply proto_interp_flip.
+ iIntros "H Hle". iApply iProto_interp_flip.
+ iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_flip.
Qed.
- Lemma proto_interp_send vl pcl vsl vsr pl pr pl' :
- proto_interp vsl vsr pl pr -∗
+ 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) proto_interp (vsl ++ [vl]) vsr pl' pr.
+ â–·^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
Proof.
- iIntros "H Hle". iDestruct (proto_interp_le_l with "H Hle") as "H".
+ 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}proto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
+ rewrite {1}iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
- iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
iDestruct (iProto_dual_le with "Hp") as "Hp".
iDestruct (iProto_le_trans with "Hp Hp'") as "Hp".
rewrite /iProto_dual proto_map_message /=.
- iApply proto_interp_unfold. iRight; iLeft.
+ iApply iProto_interp_unfold. iRight; iLeft.
iExists vl, [], _, (iProto_dual pl'). iSplit; [done|]. iFrame "Hp"; simpl.
- rewrite proto_eq_next_dual. iFrame "Hpcl". iApply proto_interp_nil.
+ 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 (proto_interp_le_r with "[-Hpr] Hpr"); clear pr.
- iApply proto_interp_unfold. iRight; iLeft.
+ 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) /=".
@@ -840,271 +739,145 @@ Section proto.
iRewrite ("Hpc" $! vr' (proto_eq_next pl'')) in "Hpcl'"; clear pc'.
iDestruct ("Hle" with "Hpcl' Hpcl")
as (pc1 pc2 pt) "(Hpl'' & Hpl' & Hpc1 & Hpc2)".
- iNext. iDestruct (proto_interp_le_l with "H Hpl''") as "H".
+ iNext. iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
iDestruct ("IH" with "[%] [//] H Hpc1") as "H"; [simpl; lia|..].
- iNext. iApply proto_interp_unfold. iRight; iRight.
+ iNext. iApply iProto_interp_unfold. iRight; iRight.
iExists vr', vsr', _, pt. iSplit; [done|]. by iFrame.
Qed.
- Lemma proto_interp_recv vl vsl vsr pl pr pcr :
- proto_interp (vl :: vsl) vsr pl pr -∗
+ 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) ∗ ▷ proto_interp vsl vsr pl pr.
+ ∃ pr, pcr vl (proto_eq_next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
Proof.
- iIntros "H Hle". iDestruct (proto_interp_le_r with "H Hle") as "H".
+ 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 !proto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
+ 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".
iDestruct ("Hpr" $! vl' pr' with "[Hpc']") as (pr'') "[Hler Hpr]".
{ by iRewrite -("Hpc" $! vl' (proto_eq_next pr')). }
- iExists pr''. iFrame "Hpr". by iApply (proto_interp_le_r with "Hinterp").
+ iExists pr''. iFrame "Hpr". by iApply (iProto_interp_le_r with "Hinterp").
- iDestruct "H" as (vr vsr' pc' pl'' ->) "(Hpl & Hpc' & Hinterp)".
iDestruct ("IH" with "[%] [//] Hinterp") as (pr) "[Hpc Hinterp]"; [simpl; lia|].
iExists pr. iFrame "Hpc".
- iApply proto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
+ iApply iProto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
Qed.
- (** ** 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 "#? 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]") as "#?".
- { iNext. iExists [], [], p, (iProto_dual p). iFrame.
- iApply proto_interp_nil. }
- iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
- - iExists Left, c1, c2, pγ, p.
- iFrame "Hlstf #". iSplit; [done|]. iApply iProto_le_refl.
- - iExists Right, c1, c2, pγ, (iProto_dual p).
- iFrame "Hrstf #". 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 Hpc".
- iDestruct "Hc" as (s c1 c2 γ p ->) "(Hle & Hst & #[??])".
- iExists s, c1, c2, γ. do 2 (iSplit; [done|]).
- iInv protoN as (vsl vsr pl pr)
- "(>Hcl & >Hcr & Hstla & Hstra & Hinterp)" "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 "#Hpl".
- iAssert (â–· iProto_le pl (iProto_message_def Send pc))%I
- with "[Hle]" as "{Hpl} Hlel"; first by (iNext; iRewrite "Hpl").
- iDestruct (proto_interp_send ((pc x).1.1) with "Hinterp Hlel [Hpc]") as "Hinterp".
- { iNext. iExists x. iFrame; auto. }
- iMod (proto_own_auth_update _ _ _ _ (pc x).2 with "Hstla Hst") as "[Hstla Hst]".
- iMod ("Hclose" with "[-Hst]") as "_".
- { iNext. iExists _, _, _, _. iFrame. }
- iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, (pc x).2.
- iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
- - iExists _. iIntros "{$Hcr} !> Hcr".
- iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Hpr".
- iAssert (â–· iProto_le pr (iProto_message_def Send pc))%I
- with "[Hle]" as "{Hpr} Hler"; first by (iNext; iRewrite "Hpr").
- iDestruct (proto_interp_flip with "Hinterp") as "Hinterp".
- iDestruct (proto_interp_send ((pc x).1.1) with "Hinterp Hler [Hpc]") as "Hinterp".
- { iNext. iExists x. iFrame; auto. }
- iMod (proto_own_auth_update _ _ _ _ (pc x).2 with "Hstra Hst") as "[Hstra Hst]".
- iMod ("Hclose" with "[-Hst]") as "_".
- { iNext. iExists _, _, _, _. iFrame. by iApply proto_interp_flip. }
- iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, (pc x).2.
- iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
- 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 & #[??])".
- iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
- iSplit; [done|].
- iInv protoN as (vsl vsr pl pr)
- "(>Hcl & >Hcr & Hstla & Hstra & Hinterp)" "Hclose".
- iExists (side_elim s vsr vsl). iModIntro.
- (* TODO: refactor to avoid twice nearly the same proof *)
- destruct s; simpl.
- - iIntros "{$Hcr} !>".
- iDestruct (proto_own_auth_agree with "Hstla Hst") as "#Hpl".
- iSplit.
- + iIntros "Hcr".
- iMod ("Hclose" with "[-Hle Hst]") as "_".
- { iNext. iExists vsl, vsr, _, _. iFrame. }
- iModIntro. rewrite mapsto_proto_eq.
- iExists Left, c1, c2, γ, p. iFrame; auto.
- + iIntros (v vs ->) "Hcr".
- iDestruct (proto_interp_flip with "Hinterp") as "Hinterp".
- iDestruct (proto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
- { iNext. by iRewrite "Hpl". }
- iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hst") as "[Hstla Hst]".
- iMod ("Hclose" with "[-Hst Hpc]") as %_.
- { iNext. iExists _, _, q, _. iFrame. by iApply proto_interp_flip. }
- iIntros "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq'] /=".
- iExists x. iSplit; [done|]. iFrame "Hpc". iRewrite -"Hq'".
- rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, q.
- iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
- - iIntros "{$Hcl} !>".
- iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Hpr".
- iSplit.
- + iIntros "Hcl".
- iMod ("Hclose" with "[-Hle Hst]") as "_".
- { iNext. iExists vsl, vsr, _, _. iFrame. }
- iModIntro. rewrite mapsto_proto_eq.
- iExists Right, c1, c2, γ, p. iFrame; auto.
- + iIntros (v vs ->) "Hcl".
- iDestruct (proto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
- { iNext. by iRewrite "Hpr". }
- iMod (proto_own_auth_update _ _ _ _ q with "Hstra Hst") as "[Hstra Hst]".
- iMod ("Hclose" with "[-Hst Hpc]") as %_.
- { iNext. iExists _, _, _, q. iFrame. }
- iIntros "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq'] /=".
- iExists x. iSplit; [done|]. iFrame "Hpc". iRewrite -"Hq'".
- rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, q.
- iFrame "Hst #". iSplit; [done|]. iApply iProto_le_refl.
- 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 "!> !> !> !>".
- 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 "!> !> !> !>".
- 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.
+ 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.
- (** ** 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) }}}.
+ Lemma iProto_own_le γ s p1 p2 :
+ iProto_own γ s p1 -∗ iProto_le p1 p2 -∗ iProto_own γ s p2.
Proof.
- rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
- iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
+ iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
+ iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
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 }}}.
+ Lemma iProto_init p :
+ ⊢ |==> ∃ γ,
+ iProto_ctx γ [] [] ∗
+ iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
Proof.
- rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
- iApply (recv_proto_spec with "Hc"); simpl.
- iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
+ 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 "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq] /=".
+ 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 "!> !> !>". iDestruct "Hpc" as (x ->) "[Hpc #Hq] /=".
+ 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_model.v b/theories/channel/proto_model.v
index aa7bf60ffb72ddc8b5fa274ef155dae5b340af04..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:
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.