From deb6d9e522976541b4434417c936cf4d99b823b3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Apr 2020 17:35:38 +0200
Subject: [PATCH] Large refactoring.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
- Protocols are no longer contractive in the message
- New type `iMsg` for messages to avoid telescopes in protocols
- Better rules for subprotocols that do not involve telescopes, but allow introduction
and elimination of quantifiers and the payload
- Better notations for protocols
- Notation ⊑ for subprotocols
- Make ⊑ except-0 so one can strip laters when proving a ⊑
- Restore recursive domain equation to push later inwards to support protocols
that are not contractive in the mssage.
- Proofmode support for easy manipulation of ⊑
---
theories/channel/channel.v | 191 ++---
theories/channel/proofmode.v | 247 +++---
theories/channel/proto.v | 1223 +++++++++++++++++------------
theories/channel/proto_model.v | 73 +-
theories/examples/basics.v | 34 +-
theories/examples/map.v | 4 +-
theories/examples/sort.v | 8 +-
theories/examples/sort_br_del.v | 4 +-
theories/examples/sort_fg.v | 8 +-
theories/logrel/examples/double.v | 17 +-
theories/logrel/model.v | 4 +-
theories/logrel/session_types.v | 25 +-
theories/logrel/subtyping_rules.v | 220 ++----
13 files changed, 1051 insertions(+), 1007 deletions(-)
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 1beb11c..4e518e2 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -6,7 +6,7 @@ lock-protected buffers, and their primitive proof rules. Moreover:
- It proves Actris's specifications of [send] and [recv] w.r.t. dependent
separation protocols.
-An encoding of the usual branching connectives [prot1 <{Q1}+{Q2}> prot2] and
+An encoding of the usual choice connectives [prot1 <{Q1}+{Q2}> prot2] and
[prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
file.
@@ -86,6 +86,7 @@ Qed.
(** * Definition of the mapsto connective *)
Notation iProto Σ := (iProto Σ val).
+Notation iMsg Σ := (iMsg Σ val).
Definition iProto_mapsto_def `{!heapG Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
@@ -105,20 +106,20 @@ 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 Σ)
+Definition iProto_choice {Σ} (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 Recv P1 P2) (at level 85) : proto_scope.
-Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
-Infix "<&{ P2 }>" := (iProto_branch Recv True P2) (at level 85) : proto_scope.
-Infix "<{ P1 }+>" := (iProto_branch Send P1 True) (at level 85) : proto_scope.
-Infix "<{ P1 }&>" := (iProto_branch Recv P1 True) (at level 85) : proto_scope.
-Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
-Infix "<&>" := (iProto_branch Recv True True) (at level 85) : proto_scope.
+ (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
+Typeclasses Opaque iProto_choice.
+Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
+Instance: Params (@iProto_choice) 2 := {}.
+Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
+Infix "<{ P1 }&{ P2 }>" := (iProto_choice Recv P1 P2) (at level 85) : proto_scope.
+Infix "<+{ P2 }>" := (iProto_choice Send True P2) (at level 85) : proto_scope.
+Infix "<&{ P2 }>" := (iProto_choice Recv True P2) (at level 85) : proto_scope.
+Infix "<{ P1 }+>" := (iProto_choice Send P1 True) (at level 85) : proto_scope.
+Infix "<{ P1 }&>" := (iProto_choice Recv P1 True) (at level 85) : proto_scope.
+Infix "<+>" := (iProto_choice Send True True) (at level 85) : proto_scope.
+Infix "<&>" := (iProto_choice Recv True True) (at level 85) : proto_scope.
Section channel.
Context `{!heapG Σ, !chanG Σ}.
@@ -130,62 +131,47 @@ Section channel.
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.
+ Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
Proof.
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.
- 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.
+ Global Instance iProto_choice_contractive n a :
+ Proper (dist n ==> dist n ==>
+ dist_later n ==> dist_later n ==> dist n) (@iProto_choice Σ a).
+ Proof. solve_contractive. Qed.
+ Global Instance iProto_choice_ne n a :
+ Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_choice Σ a).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_choice_proper a :
+ Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) (@iProto_choice Σ a).
+ Proof. solve_proper. 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).
+ Lemma iProto_dual_choice a P1 P2 p1 p2 :
+ iProto_dual (iProto_choice a P1 P2 p1 p2)
+ ≡ iProto_choice (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
Proof.
- rewrite /iProto_branch iProto_dual_message /=.
- by apply iProto_message_proper=> /= -[].
+ rewrite /iProto_choice iProto_dual_message /= iMsg_dual_exist.
+ f_equiv; f_equiv=> -[]; by rewrite iMsg_dual_base.
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.
+ Lemma iProto_app_choice a P1 P2 p1 p2 q :
+ (iProto_choice a P1 P2 p1 p2 <++> q)%proto
+ ≡ (iProto_choice a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
Proof.
- rewrite /iProto_branch iProto_app_message.
- by apply iProto_message_proper=> /= -[].
+ rewrite /iProto_choice iProto_app_message /= iMsg_app_exist.
+ f_equiv; f_equiv=> -[]; by rewrite iMsg_app_base.
Qed.
- Lemma iProto_le_branch a P1 P2 p1 p2 p1' p2' :
- ▷ (P1 -∗ P1 ∗ iProto_le p1 p1') ∧ ▷ (P2 -∗ P2 ∗ iProto_le p2 p2') -∗
- iProto_le (iProto_branch a P1 P2 p1 p2) (iProto_branch a P1 P2 p1' p2').
+ Lemma iProto_le_choice a P1 P2 p1 p2 p1' p2' :
+ (P1 -∗ P1 ∗ ▷ (p1 ⊑ p1')) ∧ (P2 -∗ P2 ∗ ▷ (p2 ⊑ p2')) -∗
+ iProto_choice a P1 P2 p1 p2 ⊑ iProto_choice a P1 P2 p1' p2'.
Proof.
- iIntros "H". rewrite /iProto_branch. destruct a.
- - iApply iProto_le_send; iIntros "!>" (b) "HP /=".
- iExists b; iSplit; [done|]. destruct b.
- + iDestruct "H" as "[H _]". by iApply "H".
- + iDestruct "H" as "[_ H]". by iApply "H".
- - iApply iProto_le_recv; iIntros "!>" (b) "HP /=".
- iExists b; iSplit; [done|]. destruct b.
- + iDestruct "H" as "[H _]". by iApply "H".
- + iDestruct "H" as "[_ H]". by iApply "H".
+ iIntros "H". rewrite /iProto_choice. destruct a;
+ iIntros (b) "HP"; iExists b; destruct b;
+ iDestruct ("H" with "HP") as "[$ ?]"; by iModIntro.
Qed.
(** ** Specifications of [send] and [recv] *)
@@ -220,22 +206,24 @@ Section channel.
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 }}}.
+ Lemma send_spec c v p :
+ {{{ c ↣ <!> MSG v; p }}}
+ send c v
+ {{{ RET #(); c ↣ p }}}.
Proof.
- rewrite iProto_mapsto_eq. iIntros (Φ) "[Hc Hpc] HΦ". wp_lam; wp_pures.
+ 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.
- - iMod (iProto_send_l with "Hctx H Hpc") as "[Hctx H]".
+ - iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
+ { rewrite iMsg_base_eq /=; auto. }
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]".
+ - iMod (iProto_send_r with "Hctx H []") as "[Hctx H]".
+ { rewrite iMsg_base_eq /=; auto. }
wp_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
wp_apply (llength_spec with "[$Hl //]"); iIntros "Hl".
wp_apply skipN_spec.
@@ -243,24 +231,16 @@ Section channel.
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 Recv pc }}}
+ Lemma try_recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+ {{{ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x }}}
try_recv c
- {{{ v, RET v; (⌜v = NONEV⌠∧ c ↣ iProto_message Recv pc) ∨
- (∃ x : TT, ⌜v = SOMEV ((pc x).1.1)⌠∗ c ↣ (pc x).2 ∗ (pc x).1.2) }}}.
+ {{{ w, RET w; (⌜w = NONEV⌠∗ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x) ∨
+ (∃.. x, ⌜w = SOMEV (v x)⌠∗ c ↣ p x ∗ P x) }}}.
Proof.
+ assert (∀ w lp (m : TT → iMsg Σ),
+ (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, m x w lp)) as iMsg_texist.
+ { intros w lp m. clear v P p. rewrite /iMsg_texist iMsg_exist_eq.
+ induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH. }
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]".
@@ -272,10 +252,12 @@ Section channel.
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.
- iMod "H" as (x ->) "(Hctx & H & Hpc)".
+ iMod "H" as (q) "(Hctx & H & Hm)".
+ rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
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.
+ iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+ by iRewrite "Hp".
- 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|].
@@ -283,43 +265,35 @@ Section channel.
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.
- iMod "H" as (x ->) "(Hctx & H & Hpc)".
+ iMod "H" as (q) "(Hctx & H & Hm)".
+ rewrite iMsg_base_eq. iDestruct (iMsg_texist with "Hm") as (x <-) "[Hp HP]".
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.
+ iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+ by iRewrite "Hp".
Qed.
- Lemma recv_spec_packed {TT} c (pc : TT → val * iProp Σ * iProto Σ) :
- {{{ c ↣ iProto_message Recv pc }}}
+ Lemma recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+ {{{ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x }}}
recv c
- {{{ x, RET (pc x).1.1; c ↣ (pc x).2 ∗ (pc x).1.2 }}}.
+ {{{ x, RET v x; c ↣ p x ∗ P x }}}.
Proof.
iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
- wp_apply (try_recv_spec_packed with "Hc"); iIntros (v) "[[-> H]|H]".
+ wp_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
{ wp_pures. by iApply ("IH" with "[$]"). }
- iDestruct "H" as (x ->) "[Hc Hpc]". wp_pures. iApply "HΦ". iFrame.
- Qed.
-
- (** 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 Recv pc -∗
- ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Φ (pc x).1.1) -∗
- WP recv c {{ Φ }}.
- Proof.
- iIntros "Hc H". iApply (recv_spec_packed with "[$]").
- iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
- iApply ("H" with "[$] [$]").
+ iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". iFrame.
Qed.
- (** ** Specifications for branching *)
+ (** ** Specifications for choice *)
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_spec with "Hc"); simpl; eauto with iFrame.
+ rewrite /iProto_choice. iIntros (Φ) "[Hc HP] HΦ".
+ iApply (send_spec with "[Hc HP] HΦ").
+ iApply (iProto_mapsto_le with "Hc").
+ iIntros "!>". iExists b. by iFrame "HP".
Qed.
Lemma branch_spec c P1 P2 p1 p2 :
@@ -327,8 +301,13 @@ Section channel.
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_spec with "Hc"); simpl.
- iIntros "!>" (b) "Hc HP". iApply "HΦ". iFrame.
+ rewrite /iProto_choice. iIntros (Φ) "Hc HΦ".
+ iApply (recv_spec _ (tele_app _)
+ (tele_app (TT:=[tele _ : bool]) (λ b, if b then P1 else P2))%I
+ (tele_app _) with "[Hc]").
+ { iApply (iProto_mapsto_le with "Hc").
+ iIntros "!> /=" (b) "HP". iExists b. by iSplitL. }
+ rewrite -bi_tforall_forall.
+ iIntros "!>" (x) "[Hc H]". iApply "HΦ". iFrame.
Qed.
End channel.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 7652a62..90e2817 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -12,22 +12,22 @@ From iris.proofmode Require Export tactics.
From actris Require Export channel.
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
-(** * Tactics for proving contractiveness of protocols *)
-Ltac f_proto_contractive :=
+-(** * Tactics for proving contractiveness of protocols *)
+Ltac f_dist_le :=
match goal with
- | _ => apply iProto_branch_contractive
- | _ => apply iProto_message_contractive; simpl; intros; [reflexivity|..]
| H : _ ≡{?n}≡ _ |- _ ≡{?n'}≡ _ => apply (dist_le n); [apply H|lia]
- end;
- try match goal with
- | |- @dist_later ?A _ ?n ?x ?y =>
- destruct n as [|n]; simpl in *; [exact Logic.I|change (@dist A _ n x y)]
end.
Ltac solve_proto_contractive :=
- solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]).
+ solve_proper_core ltac:(fun _ =>
+ first [f_contractive; simpl in * | f_equiv | f_dist_le]).
(** * Normalization of protocols *)
+Class MsgTele {Σ} {TT : tele} (m : iMsg Σ)
+ (tv : TT -t> val) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ) :=
+ msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
+Hint Mode MsgTele ! - ! - - - : typeclass_instances.
+
Class ActionDualIf (d : bool) (a1 a2 : action) :=
dual_action_if : a2 = if d then action_dual a1 else a1.
Hint Mode ActionDualIf ! ! - : typeclass_instances.
@@ -39,38 +39,47 @@ Instance action_dual_if_true_recv : ActionDualIf true Recv Send := eq_refl.
Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
(pas : list (bool * iProto Σ)) (q : iProto Σ) :=
proto_normalize :
- ⊢ iProto_le (iProto_dual_if d p <++>
- foldr (iProto_app ∘ curry iProto_dual_if) END pas)%proto q.
+ ⊢ iProto_dual_if d p <++>
+ foldr (iProto_app ∘ curry iProto_dual_if) END%proto pas ⊑ q.
Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
-Class ProtoContNormalize {Σ TT} (d : bool) (pc : TT → val * iProp Σ * iProto Σ)
- (pas : list (bool * iProto Σ)) (qc : TT → val * iProp Σ * iProto Σ) :=
- proto_cont_normalize x :
- (pc x).1.1 = (qc x).1.1 ∧
- (pc x).1.2 ≡ (qc x).1.2 ∧
- ProtoNormalize d ((pc x).2) pas ((qc x).2).
-Hint Mode ProtoContNormalize ! ! ! ! ! - : typeclass_instances.
-
Notation ProtoUnfold p1 p2 := (∀ d pas q,
ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
+Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
+ (pas : list (bool * iProto Σ)) (m2 : iMsg Σ) :=
+ msg_normalize a :
+ ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
+Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
+Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
+
Section classes.
Context `{!chanG Σ, !heapG Σ}.
- Implicit Types p : iProto Σ.
Implicit Types TT : tele.
+ Implicit Types p : iProto Σ.
+ Implicit Types m : iMsg Σ.
+ Implicit Types P : iProp Σ.
+
+ Global Instance msg_tele_base v P p :
+ MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
+ Proof. done. Qed.
+ Global Instance msg_tele_exist {A} {TT : A → tele} (m : A → iMsg Σ) tv tP tp :
+ (∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) →
+ MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
+ Proof. intros Hm. rewrite /MsgTele /=. f_equiv=> x. apply Hm. Qed.
Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
Proof. rewrite /ProtoNormalize=> Hp d pas q. by rewrite Hp. Qed.
Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
- Proof. rewrite /ProtoNormalize /= right_id. iApply iProto_le_refl. Qed.
+ Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
Global Instance proto_normalize_done_dual p :
ProtoNormalize true p [] (iProto_dual p) | 0.
- Proof. rewrite /ProtoNormalize /= right_id. iApply iProto_le_refl. Qed.
+ Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
Global Instance proto_normalize_done_dual_end :
ProtoNormalize (Σ:=Σ) true END [] END | 0.
- Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. iApply iProto_le_refl. Qed.
+ Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. auto. Qed.
Global Instance proto_normalize_dual d p pas q :
ProtoNormalize (negb d) p pas q →
@@ -96,101 +105,75 @@ Section classes.
Global Instance proto_normalize_app_r d p1 p2 pas q :
ProtoNormalize d p2 pas q →
ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0.
- Proof.
- rewrite /ProtoNormalize /= => H.
- iApply iProto_le_app; [iApply iProto_le_refl|done].
- Qed.
+ Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
ProtoNormalize d p2 pas q →
ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0.
- Proof.
- rewrite /ProtoNormalize /= => H.
- iApply iProto_le_app; [iApply iProto_le_refl|done].
- Qed.
+ Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
- Global Instance proto_cont_normalize_O d v P p q pas :
+ Global Instance msg_normalize_base d v P p q pas :
ProtoNormalize d p pas q →
- ProtoContNormalize d (tele_app (TT:=TeleO) (v,P,p)) pas
- (tele_app (TT:=TeleO) (v,P,q)).
- Proof. rewrite /ProtoContNormalize=> ?. by apply tforall_forall. Qed.
-
- Global Instance proto_cont_normalize_S {A} {TT : A → tele} d
- (pc qc : ∀ a, TT a -t> val * iProp Σ * iProto Σ) pas :
- (∀ a, ProtoContNormalize d (tele_app (pc a)) pas (tele_app (qc a))) →
- ProtoContNormalize d (tele_app (TT:=TeleS TT) pc) pas (tele_app (TT:=TeleS TT) qc).
+ MsgNormalize d (MSG v {{ P }}; p) pas (MSG v {{ P }}; q).
Proof.
- rewrite /ProtoContNormalize=> H. apply tforall_forall=> /= x.
- apply tforall_forall, (H x).
+ rewrite /MsgNormalize /ProtoNormalize=> H a.
+ iApply iProto_le_trans; [|by iApply iProto_le_base].
+ destruct d; by rewrite /= ?iProto_dual_message ?iMsg_dual_base
+ iProto_app_message iMsg_app_base.
Qed.
- Global Instance proto_normalize_message {TT} d a1 a2
- (pc qc : TT → val * iProp Σ * iProto Σ) pas :
- ActionDualIf d a1 a2 →
- ProtoContNormalize d pc pas qc →
- ProtoNormalize d (iProto_message a1 pc) pas
- (iProto_message a2 qc).
+ Global Instance msg_normalize_exist {A} d (m1 m2 : A → iMsg Σ) pas :
+ (∀ x, MsgNormalize d (m1 x) pas (m2 x)) →
+ MsgNormalize d (∃ x, m1 x) pas (∃ x, m2 x).
Proof.
- rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize=> -> H.
- destruct d; simpl.
- - rewrite iProto_dual_message iProto_app_message. destruct a1; simpl.
- + iApply iProto_le_recv; iIntros "!>" (x) "/= Hpc". iExists x.
- destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
- + iApply iProto_le_send; iIntros "!>" (x) "/= Hpc". iExists x.
- destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
- - rewrite iProto_app_message. destruct a1; simpl.
- + iApply iProto_le_send; iIntros "!>" (x) "/= Hpc". iExists x.
- destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
- + iApply iProto_le_recv; iIntros "!>" (x) "/= Hpc". iExists x.
- destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
+ rewrite /MsgNormalize /ProtoNormalize=> H a.
+ destruct d, a; simpl in *; rewrite ?iProto_dual_message ?iMsg_dual_exist
+ ?iProto_app_message ?iMsg_app_exist /=; iIntros (x); iExists x; first
+ [move: (H x Send); by rewrite ?iProto_dual_message ?iProto_app_message
+ |move: (H x Recv); by rewrite ?iProto_dual_message ?iProto_app_message].
Qed.
- Global Instance proto_normalize_swap {TT1 TT2} d a1
- (pc1 : TT1 → val * iProp Σ * iProto Σ)
- (vP1 : TT1 -t> val * iProp Σ) (vP2 : TT2 -t> val * iProp Σ)
- (pc12 : TT1 -t> TT2 -t> iProto Σ)
- (pc2 : TT2 -t> val * iProp Σ * iProto Σ) pas :
- ActionDualIf d a1 Recv →
- ProtoContNormalize d pc1 pas (λ.. x1,
- (tele_app vP1 x1, iProto_message Send (λ.. x2,
- (tele_app vP2 x2, tele_app (tele_app pc12 x1) x2)))) →
- (∀.. x2, TCEq (tele_app vP2 x2, iProto_message Recv (λ.. x1,
- (tele_app vP1 x1, tele_app (tele_app pc12 x1) x2)))
- (tele_app pc2 x2)) →
- ProtoNormalize d (iProto_message a1 pc1) pas
- (iProto_message Send (tele_app pc2)).
+ Global Instance proto_normalize_message d a1 a2 m1 m2 pas :
+ ActionDualIf d a1 a2 →
+ MsgNormalize d m1 pas m2 →
+ ProtoNormalize d (<a1> m1) pas (<a2> m2).
+ Proof. by rewrite /ActionDualIf /MsgNormalize /ProtoNormalize=> ->. Qed.
+
+ Global Instance proto_normalize_swap {TT1 TT2} d a m m'
+ (tv1 : TT1 -t> val) (tP1 : TT1 -t> iProp Σ) (tm1 : TT1 -t> iMsg Σ)
+ (tv2 : TT2 -t> val) (tP2 : TT2 -t> iProp Σ)
+ (tp : TT1 -t> TT2 -t> iProto Σ) pas :
+ ActionDualIf d a Recv →
+ MsgNormalize d m pas m' →
+ MsgTele m' tv1 tP1 (tele_bind (λ.. x1, <!> tele_app tm1 x1))%proto →
+ (∀.. x1, MsgTele (tele_app tm1 x1) tv2 tP2 (tele_app tp x1)) →
+ ProtoNormalize d (<a> m) pas (<!.. x2> MSG tele_app tv2 x2 {{ tele_app tP2 x2 }};
+ <?.. x1> MSG tele_app tv1 x1 {{ tele_app tP1 x1 }};
+ tele_app (tele_app tp x1) x2).
Proof.
- (** TODO: This proof contains twice the same subproof. Refactor. *)
- rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize.
- rewrite tforall_forall=> ? Hpc1 Hpc2. destruct d, a1; simplify_eq/=.
- - rewrite iProto_dual_message iProto_app_message /=.
- iApply iProto_le_swap. iIntros "!>" (x1 x2) "/= Hpc1 Hpc2".
- move: (Hpc1 x1); rewrite {Hpc1} !tele_app_bind /=; intros (->&->&Hpc).
- move: (Hpc2 x2); rewrite {Hpc2} TCEq_eq; intros Hpc2.
- iExists TT2, TT1, (λ.. x2, (tele_app vP2 x2, tele_app (tele_app pc12 x1) x2)),
- (λ.. x1, (tele_app vP1 x1, tele_app (tele_app pc12 x1) x2)), x2, x1.
- rewrite /= !tele_app_bind /= -!Hpc2 /=. do 2 (iSplit; [done|]). iFrame.
- iSplitR; [done|]. iSplitR; [iApply iProto_le_refl|]. done.
- - rewrite iProto_app_message /=.
- iApply iProto_le_swap. iIntros "!>" (x1 x2) "/= Hpc1 Hpc2".
- move: (Hpc1 x1); rewrite {Hpc1} !tele_app_bind /=; intros (->&->&Hpc).
- move: (Hpc2 x2); rewrite {Hpc2} TCEq_eq; intros Hpc2.
- iExists TT2, TT1, (λ.. x2, (tele_app vP2 x2, tele_app (tele_app pc12 x1) x2)),
- (λ.. x1, (tele_app vP1 x1, tele_app (tele_app pc12 x1) x2)), x2, x1.
- rewrite /= !tele_app_bind /= -!Hpc2 /=. do 2 (iSplit; [done|]). iFrame.
- iSplitR; [done|]. iSplitR; [iApply iProto_le_refl|]. done.
+ rewrite /ActionDualIf /MsgNormalize /ProtoNormalize /MsgTele.
+ rewrite tforall_forall=> Ha Hm Hm' Hm''.
+ iApply iProto_le_trans; [iApply Hm|]. rewrite Hm' -Ha. clear Ha Hm Hm'.
+ iApply iProto_le_texist_elim_l; iIntros (x1).
+ iApply iProto_le_texist_elim_r; iIntros (x2).
+ rewrite !tele_app_bind Hm'' {Hm''}.
+ iApply iProto_le_trans;
+ [iApply iProto_le_base; iApply (iProto_le_texist_intro_l _ x2)|].
+ iApply iProto_le_trans;
+ [|iApply iProto_le_base; iApply (iProto_le_texist_intro_r _ x1)]; simpl.
+ iApply iProto_le_base_swap.
Qed.
- Global Instance proto_normalize_branch d a1 a2 P1 P2 p1 p2 q1 q2 pas :
+ Global Instance proto_normalize_choice d a1 a2 P1 P2 p1 p2 q1 q2 pas :
ActionDualIf d a1 a2 →
ProtoNormalize d p1 pas q1 → ProtoNormalize d p2 pas q2 →
- ProtoNormalize d (iProto_branch a1 P1 P2 p1 p2) pas
- (iProto_branch a2 P1 P2 q1 q2).
+ ProtoNormalize d (iProto_choice a1 P1 P2 p1 p2) pas
+ (iProto_choice a2 P1 P2 q1 q2).
Proof.
rewrite /ActionDualIf /ProtoNormalize=> -> H1 H2. destruct d; simpl.
- - rewrite !iProto_dual_branch !iProto_app_branch.
- iApply iProto_le_branch; iSplit; by iIntros "!> $".
- - rewrite !iProto_app_branch. iApply iProto_le_branch; iSplit; by iIntros "!> $".
+ - rewrite !iProto_dual_choice !iProto_app_choice.
+ iApply iProto_le_choice; iSplit; by iIntros "$".
+ - rewrite !iProto_app_choice. iApply iProto_le_choice; iSplit; by iIntros "$".
Qed.
(** Automatically perform normalization of protocols in the proof mode when
@@ -215,27 +198,35 @@ End classes.
(** * Symbolic execution tactics *)
(* TODO: Maybe strip laters from other hypotheses in the future? *)
-Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K
- c p (pc : TT → val * iProp Σ * iProto Σ) Φ :
+Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K c p m tv tP tP' tp Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
- ProtoNormalize false p [] (iProto_message Recv pc) →
+ ProtoNormalize false p [] (<?> m) →
+ MsgTele m tv tP tp →
+ (∀.. x, MaybeIntoLaterN false 1 (tele_app tP x) (tele_app tP' x)) →
let Δ' := envs_delete false i false Δ in
(∀.. x : TT,
match envs_app false
- (Esnoc (Esnoc Enil j ((pc x).1.2)) i (c ↣ (pc x).2)) Δ' with
- | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (pc x).1.1) {{ Φ }})
+ (Esnoc (Esnoc Enil j (tele_app tP' x)) i (c ↣ tele_app tp x)) Δ' with
+ | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (tele_app tv x)) {{ Φ }})
| None => False
end) →
envs_entails Δ (WP fill K (recv c) {{ Φ }}).
Proof.
- rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ.
- rewrite envs_lookup_sound //; simpl.
- rewrite (iProto_mapsto_le _ _ (iProto_message Recv pc)) -bi.later_intro -Hp left_id.
- 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.
+ rewrite envs_entails_eq /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
+ rewrite !tforall_forall right_id.
+ intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
+ assert (c ↣ p ⊢ c ↣ <?.. x>
+ MSG tele_app tv x {{ â–· tele_app tP' x }}; tele_app tp x) as ->.
+ { iIntros "Hc". iApply (iProto_mapsto_le with "Hc"). iIntros "!>".
+ iApply iProto_le_trans; [iApply Hp|rewrite Hm].
+ iApply iProto_le_texist_elim_l; iIntros (x).
+ iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ x)]; simpl.
+ iIntros "H". by iDestruct (HP with "H") as "$". }
+ rewrite -wp_bind. eapply bi.wand_apply;
+ [by eapply (recv_spec _ (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv].
+ rewrite -bi.later_intro; apply bi.forall_intro=> x.
specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
- rewrite envs_app_sound //; simpl.
- by rewrite right_id HΦ bi.wand_curry.
+ rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
Qed.
Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
@@ -251,6 +242,8 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
|fail 1 "wp_recv: cannot find 'recv' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <?>"
+ |iSolveTC || fail 1 "wp_send: cannot convert to telescope"
+ |iSolveTC
|pm_reduce; simpl; tac_intros;
tac Hnew;
wp_finish]
@@ -294,18 +287,18 @@ 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 `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
- c v p (pc : TT → val * iProp Σ * iProto Σ) Φ :
+Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K c v p m tv tP tp Φ :
envs_lookup i Δ = Some (false, c ↣ p)%I →
- ProtoNormalize false p [] (iProto_message Send pc) →
+ ProtoNormalize false p [] (<!> m) →
+ MsgTele m tv tP tp →
let Δ' := envs_delete false i false Δ in
(∃.. x : TT,
match envs_split (if neg is true then Right else Left) js Δ' with
| Some (Δ1,Δ2) =>
- match envs_app false (Esnoc Enil i (c ↣ (pc x).2)) Δ2 with
+ match envs_app false (Esnoc Enil i (c ↣ tele_app tp x)) Δ2 with
| Some Δ2' =>
- v = (pc x).1.1 ∧
- envs_entails Δ1 (pc x).1.2 ∧
+ v = tele_app tv x ∧
+ envs_entails Δ1 (tele_app tP x) ∧
envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
| None => False
end
@@ -313,16 +306,19 @@ Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
end) →
envs_entails Δ (WP fill K (send c v) {{ Φ }}).
Proof.
- rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ].
- rewrite envs_lookup_sound //; simpl.
- rewrite (iProto_mapsto_le _ _ (iProto_message Send pc)) -bi.later_intro -Hp left_id.
- rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_spec|f_equiv].
- rewrite bi_texist_exist -(bi.exist_intro x).
+ rewrite envs_entails_eq /ProtoNormalize /MsgTele /= right_id texist_exist.
+ intros ? Hp Hm [x HΦ]. rewrite envs_lookup_sound //; simpl.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
- destruct HΦ as (-> & -> & ->). rewrite bi.pure_True // left_id.
- by rewrite -bi.later_intro right_id.
+ destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
+ assert (c ↣ p ∗ tele_app tP x ⊢
+ c ↣ <!> MSG tele_app tv x; tele_app tp x) as ->.
+ { iIntros "[Hc Hm]". iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
+ iApply iProto_le_trans; [iApply Hp|]. rewrite Hm.
+ iApply iProto_le_trans; [iApply iProto_le_texist_intro_l|]. by iFrame. }
+ eapply bi.wand_apply; [rewrite -wp_bind; by eapply send_spec|].
+ by rewrite -bi.later_intro.
Qed.
Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
@@ -348,6 +344,7 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
|fail 1 "wp_send: cannot find 'send' in" e];
[solve_mapsto ()
|iSolveTC || fail 1 "wp_send: protocol not of the shape <!>"
+ |iSolveTC || fail 1 "wp_send: cannot convert to telescope"
|pm_reduce; simpl; tac_exist;
repeat lazymatch goal with
| |- ∃ _, _ => eexists _
@@ -437,7 +434,7 @@ Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" constr(pat2)
Tactic Notation "wp_branch" "as" constr(pat1) "|" "%" simple_intropattern(pat2) :=
wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_intropattern(pat2) :=
- wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
+ 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 `{!chanG Σ, !heapG Σ} Δ neg i js K
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index ca61dcf..8dc4451 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -24,7 +24,6 @@ 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.proofmode Require Import tactics.
From iris.base_logic Require Export lib.iprop.
From iris.base_logic Require Import lib.own.
@@ -48,6 +47,81 @@ Proof. solve_inG. Qed.
Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto.
+Local Open Scope proto.
+
+(** * Messages *)
+Section iMsg.
+ Set Primitive Projections.
+ Record iMsg Σ V := IMsg { iMsg_car :> V → laterO (iProto Σ V) -n> iPropO Σ }.
+End iMsg.
+Arguments IMsg {_ _} _.
+Arguments iMsg_car {_ _} _.
+
+Delimit Scope msg_scope with msg.
+Bind Scope msg_scope with iMsg.
+Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
+
+Section imsg_ofe.
+ Context {Σ : gFunctors} {V : Type}.
+
+ Instance iMsg_equiv : Equiv (iMsg Σ V) := λ m1 m2,
+ ∀ w p, iMsg_car m1 w p ≡ iMsg_car m2 w p.
+ Instance iMsg_dist : Dist (iMsg Σ V) := λ n m1 m2,
+ ∀ w p, iMsg_car m1 w p ≡{n}≡ iMsg_car m2 w p.
+
+ Lemma iMsg_ofe_mixin : OfeMixin (iMsg Σ V).
+ Proof. by apply (iso_ofe_mixin (iMsg_car : _ → V -d> _ -n> _)). Qed.
+ Canonical Structure iMsgO := OfeT (iMsg Σ V) iMsg_ofe_mixin.
+
+ Global Instance iMsg_cofe : Cofe iMsgO.
+ Proof. by apply (iso_cofe (IMsg : (V -d> _ -n> _) → _) iMsg_car). Qed.
+
+ Global Instance iMsg_car_ne n : Proper (dist n ==> (=) ==> dist n) iMsg_car.
+ Proof. by intros m m' ? w ? <- p. Qed.
+ Global Instance iMsg_car_proper : Proper ((≡) ==> (=) ==> (≡)) iMsg_car.
+ Proof. by intros m m' ? w ? <- p. Qed.
+
+ Global Instance IMsg_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) IMsg.
+ Proof. by intros ???. Qed.
+ Global Instance IMsg_proper : Proper (pointwise_relation _ (≡) ==> (≡)) IMsg.
+ Proof. by intros ???. Qed.
+End imsg_ofe.
+
+Program Definition iMsg_base_def {Σ V}
+ (v : V) (P : iProp Σ) (p : iProto Σ V) : iMsg Σ V :=
+ IMsg (λ v', λne p', ⌜ v = v' ⌠∗ Next p ≡ p' ∗ P)%I.
+Next Obligation. solve_proper. Qed.
+Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
+Definition iMsg_base := iMsg_base_aux.(unseal).
+Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
+Arguments iMsg_base {_ _} _%V _%I _%proto.
+Instance: Params (@iMsg_base) 3 := {}.
+
+Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
+ IMsg (λ v', λne p', ∃ x, m x v' p')%I.
+Next Obligation. solve_proper. Qed.
+Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
+Definition iMsg_exist := iMsg_exist_aux.(unseal).
+Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
+Arguments iMsg_exist {_ _ _} _%msg.
+Instance: Params (@iMsg_exist) 3 := {}.
+
+Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
+ tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
+Arguments iMsg_texist {_ _ !_} _%msg /.
+
+Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
+ (at level 200, v at level 20, right associativity,
+ format "MSG v {{ P } } ; p") : msg_scope.
+Notation "'MSG' v ; p" := (iMsg_base v True p)
+ (at level 200, v at level 20, right associativity,
+ format "MSG v ; p") : msg_scope.
+Notation "∃ x .. y , m" :=
+ (iMsg_exist (λ x, .. (iMsg_exist (λ y, m)) ..)%msg) : msg_scope.
+Notation "'∃..' x .. y , m" :=
+ (iMsg_texist (λ x, .. (iMsg_texist (λ y, m)) .. )%msg)
+ (at level 200, x binder, y binder, right associativity,
+ format "∃.. x .. y , m") : msg_scope.
(** * Operators *)
Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
@@ -56,119 +130,64 @@ 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 p', ∃ x : TT,
- ⌜ v = (pc x).1.1 ⌠∗
- (pc x).1.2 ∗
- p' ≡ (pc x).2)%I.
-Next Obligation. solve_proper. Qed.
+Definition iProto_message_def {Σ V} (a : action) (m : iMsg Σ V) : iProto Σ V :=
+ proto_message a m.
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
- Recv
- (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
- Recv
- (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
- Recv
- (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
- Recv
- (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
- (at level 20, v at level 20, p at level 200) : proto_scope.
+Arguments iProto_message {_ _} _ _%msg.
+Instance: Params (@iProto_message) 3 := {}.
Notation "'END'" := iProto_end : proto_scope.
+Notation "< a > m" := (iProto_message a m)
+ (at level 200, a at level 10, m at level 200,
+ format "< a > m") : proto_scope.
+Notation "< a @ x1 .. xn > m" := (iProto_message a (∃ x1, .. (∃ xn, m) ..))
+ (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
+ format "< a @ x1 .. xn > m") : proto_scope.
+Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m) ..))
+ (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
+ format "< a @.. x1 .. xn > m") : proto_scope.
+
+Notation "<!> m" := (<Send> m) (at level 200, m at level 200) : proto_scope.
+Notation "<! x1 .. xn > m" := (<!> ∃ x1, .. (∃ xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<! x1 .. xn > m") : proto_scope.
+Notation "<!.. x1 .. xn > m" := (<!> ∃.. x1, .. (∃.. xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<!.. x1 .. xn > m") : proto_scope.
+
+Notation "<?> m" := (<Recv> m) (at level 200, m at level 200) : proto_scope.
+Notation "<? x1 .. xn > m" := (<?> ∃ x1, .. (∃ xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<? x1 .. xn > m") : proto_scope.
+Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
+ (at level 200, x1 closed binder, xn closed binder, m at level 200,
+ format "<?.. x1 .. xn > m") : proto_scope.
+
(** * Operations *)
-Program Definition iProto_map_app_cont {Σ V}
- (rec : iProto Σ V → iProto Σ V) (pc : iProto Σ V -n> iPropO Σ) :
- iProto Σ V -n> iPropO Σ :=
- λne p1', (∃ p1, pc p1 ∗ p1' ≡ rec p1)%I.
+Program Definition iMsg_map {Σ V}
+ (rec : iProto Σ V → iProto Σ V) (m : iMsg Σ V) : iMsg Σ V :=
+ IMsg (λ v, λne p1', ∃ p1, m v (Next p1) ∗ p1' ≡ Next (rec p1))%I.
Next Obligation. solve_proper. Qed.
Program Definition iProto_map_app_aux {Σ V}
(f : action → action) (p2 : iProto Σ V)
(rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p,
- proto_elim p2 (λ a pc,
- proto_message (f a) (iProto_map_app_cont rec ∘ pc)) p.
+ proto_elim p2 (λ a m,
+ proto_message (f a) (iMsg_map rec (IMsg m))) p.
Next Obligation.
- intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a pc1 pc2 Hpc.
- apply proto_message_contractive; destruct n as [|n]=> // v p'; simpl in *.
- by repeat f_equiv.
+ intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a m1 m2 Hm.
+ apply proto_message_ne=> v p' /=. by repeat f_equiv.
Qed.
Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
Contractive (iProto_map_app_aux f p2).
Proof.
- intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a pc1 pc2 Hpc.
- apply proto_message_contractive; destruct n as [|n]=> // v p'; simpl in *.
- by repeat f_equiv.
+ intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a m1 m2 Hm.
+ apply proto_message_ne=> v p' /=. by repeat (f_contractive || f_equiv).
Qed.
Definition iProto_map_app {Σ V} (f : action → action)
@@ -183,6 +202,7 @@ Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal
Arguments iProto_app {_ _} _%proto _%proto.
Instance: Params (@iProto_app) 2 := {}.
Infix "<++>" := iProto_app (at level 60) : proto_scope.
+Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V :=
iProto_map_app action_dual proto_end p.
@@ -192,6 +212,8 @@ Definition iProto_dual_eq :
@iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
Arguments iProto_dual {_ _} _%proto.
Instance: Params (@iProto_dual) 2 := {}.
+Notation iMsg_dual := (iMsg_map iProto_dual).
+
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.
@@ -219,19 +241,16 @@ Example:
*)
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 ∗
+ ◇ (p1 ≡ END ∗ p2 ≡ END) ∨
+ ∃ a1 a2 m1 m2,
+ ◇ (p1 ≡ <a1> m1) ∗ ◇ (p2 ≡ <a2> m2) ∗
match a1, a2 with
- | Recv, Recv => ▷ ∀ v p1', pc1 v p1' -∗ ∃ p2', rec p1' p2' ∗ pc2 v p2'
- | Send, Send => ▷ ∀ v p2', pc2 v p2' -∗ ∃ p1', rec p1' p2' ∗ pc1 v p1'
- | Recv, Send => ▷ ∀ v1 v2 p1' p2',
- pc1 v1 p1' -∗ pc2 v2 p2' -∗ ∃ pc1' pc2' pt,
- rec p1' (proto_message Send pc1') ∗
- rec (proto_message Recv pc2') p2' ∗
- pc1' v2 pt ∗
- pc2' v1 pt
+ | Recv, Recv => ∀ v p1', m1 v (Next p1') -∗ ◇ ∃ p2', ▷ rec p1' p2' ∗ m2 v (Next p2')
+ | Send, Send => ∀ v p2', m2 v (Next p2') -∗ ◇ ∃ p1', ▷ rec p1' p2' ∗ m1 v (Next p1')
+ | Recv, Send => ∀ v1 v2 p1' p2',
+ m1 v1 (Next p1') -∗ m2 v2 (Next p2') -∗ ◇ ∃ m1' m2' pt,
+ ▷ rec p1' (<!> m1') ∗ ▷ rec (<?> m2') p2' ∗
+ m1' v2 (Next pt) ∗ m2' v1 (Next pt)
| Send, Recv => False
end.
Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
@@ -252,6 +271,7 @@ 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 := {}.
+Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
Fixpoint iProto_interp_aux {Σ V} (n : nat)
(vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
@@ -259,18 +279,18 @@ Fixpoint iProto_interp_aux {Σ V} (n : nat)
| 0 => ∃ p,
⌜ vsl = [] ⌠∗
⌜ vsr = [] ⌠∗
- iProto_le p pl ∗
- iProto_le (iProto_dual p) pr
+ p ⊑ pl ∗
+ iProto_dual p ⊑ pr
| S n =>
- (∃ vl vsl' pc p2',
+ (∃ vl vsl' m p2',
⌜ vsl = vl :: vsl' ⌠∗
- iProto_le (proto_message Recv pc) pr ∗
- pc vl p2' ∗
+ (<?> m) ⊑ pr ∗
+ m vl (Next p2') ∗
iProto_interp_aux n vsl' vsr pl p2') ∨
- (∃ vr vsr' pc p1',
+ (∃ vr vsr' m p1',
⌜ vsr = vr :: vsr' ⌠∗
- iProto_le (proto_message Recv pc) pl ∗
- pc vr p1' ∗
+ (<?> m) ⊑ pl ∗
+ m vr (Next p1') ∗
iProto_interp_aux n vsl vsr' p1' pr)
end.
Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
@@ -319,46 +339,72 @@ Definition iProto_ctx `{protoG Σ V}
(** * 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'.
+ ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ s p'.
Arguments iProto_own {_ _ _} _ _%proto.
Instance: Params (@iProto_own) 3 := {}.
(** * Proofs *)
Section proto.
Context `{!protoG Σ V}.
+ Implicit Types v : V.
Implicit Types p pl pr : iProto Σ V.
- Implicit Types TT : tele.
+ Implicit Types m : iMsg Σ V.
- (** ** 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.
+ (** ** Equality *)
+ Lemma iProto_case p : p ≡ END ∨ ∃ a m, p ≡ <a> m.
Proof.
- rewrite !tforall_forall=> Hv HP Hp.
- rewrite iProto_message_eq /iProto_message_def.
- apply proto_message_contractive; destruct n as [|n]=> // v f /=.
- repeat (apply Hv || apply HP || apply Hp || f_contractive || f_equiv).
+ rewrite iProto_message_eq iProto_end_eq.
+ destruct (proto_case p) as [|(a&m&?)]; [by left|right].
+ by exists a, (IMsg m).
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.
+ Lemma iProto_message_equivI {SPROP : sbi} a1 a2 m1 m2 :
+ (<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧ (∀ v lp, m1 v lp ≡ m2 v lp).
+ Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
+ Lemma iProto_message_end_equivI {SPROP : sbi} a m : (<a> m) ≡ END ⊢@{SPROP} False.
+ Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.
+ Lemma iProto_end_message_equivI {SPROP : sbi} a m : END ≡ (<a> m) ⊢@{SPROP} False.
+ Proof. by rewrite bi.internal_eq_sym iProto_message_end_equivI. Qed.
+
+ (** ** Non-expansiveness of operators *)
+ Global Instance iMsg_contractive v n :
+ Proper (dist n ==> dist_later n ==> dist n) (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. rewrite iMsg_base_eq. solve_proper. Qed.
+ Global Instance iMsg_ne v : NonExpansive2 (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. rewrite iMsg_base_eq. solve_proper. Qed.
+ Global Instance iMsg_proper v :
+ Proper ((≡) ==> (≡) ==> (≡)) (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. apply (ne_proper_2 _). Qed.
+
+ Global Instance iMsg_exist_ne A n :
+ Proper (pointwise_relation _ (dist n) ==> (dist n)) (@iMsg_exist Σ V A).
+ Proof. rewrite iMsg_exist_eq. solve_proper. Qed.
+ Global Instance iMsg_exist_proper A :
+ Proper (pointwise_relation _ (≡) ==> (≡)) (@iMsg_exist Σ V A).
+ Proof. rewrite iMsg_exist_eq. solve_proper. Qed.
+
+ Global Instance iProto_message_ne a :
+ NonExpansive (iProto_message (Σ:=Σ) (V:=V) a).
+ Proof. rewrite iProto_message_eq. solve_proper. Qed.
+ Global Instance iProto_message_proper a :
+ Proper ((≡) ==> (≡)) (iProto_message (Σ:=Σ) (V:=V) a).
+ Proof. apply (ne_proper _). Qed.
+
+ (** Helpers *)
+ Lemma iMsg_map_base f v P p :
+ NonExpansive f →
+ iMsg_map f (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; f p)%msg.
Proof.
- rewrite !tforall_forall=> Hv HP Hp.
- apply iProto_message_contractive; apply tforall_forall; eauto using dist_dist_later.
+ rewrite iMsg_base_eq. intros ? v' p'; simpl. iSplit.
+ - iDestruct 1 as (p'') "[(->&Hp&$) Hp']". iSplit; [done|].
+ iRewrite "Hp'". iIntros "!>". by iRewrite "Hp".
+ - iIntros "(->&Hp'&$)". iExists p. iRewrite -"Hp'". auto.
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.
+ Lemma iMsg_map_exist {A} f (m : A → iMsg Σ V) :
+ iMsg_map f (∃ x, m x) ≡ (∃ x, iMsg_map f (m x))%msg.
Proof.
- rewrite !tforall_forall=> Hv HP Hp. apply equiv_dist => n.
- apply iProto_message_ne; apply tforall_forall=> x; by try apply equiv_dist.
+ rewrite iMsg_exist_eq. intros v' p'; simpl. iSplit.
+ - iDestruct 1 as (p'') "[H Hp']". iDestruct "H" as (x) "H"; auto.
+ - iDestruct 1 as (x p'') "[Hm Hp']". auto.
Qed.
(** ** Dual *)
@@ -372,71 +418,54 @@ Section proto.
Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
Proof. apply (ne_proper _). Qed.
- Lemma iProto_dual_end' : iProto_dual (Σ:=Σ) (V:=V) proto_end ≡ proto_end.
+ Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END.
Proof.
- rewrite iProto_dual_eq /iProto_dual_def /iProto_map_app.
+ rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
by rewrite proto_elim_end.
Qed.
- Lemma iProto_dual_message' a pc :
- iProto_dual (Σ:=Σ) (V:=V) (proto_message a pc)
- ≡ proto_message (action_dual a) (iProto_map_app_cont iProto_dual ∘ pc).
+ Lemma iProto_dual_message a m :
+ iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m.
Proof.
- rewrite iProto_dual_eq /iProto_dual_def /iProto_map_app.
+ rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- apply: proto_elim_message=> a' pc1 pc2 Hpc; f_equiv; solve_proper.
- Qed.
-
- Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END%proto.
- Proof. rewrite iProto_end_eq. apply iProto_dual_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_message_eq /iProto_message_def iProto_dual_message' /=.
- do 2 f_equiv; intros p'; simpl. iSplit.
- - iDestruct 1 as (pd) "[H Hp']". iDestruct "H" as (x ->) "[Hpc Hpd]".
- iExists x. iSplit; [done|]; iFrame. iRewrite "Hp'". by iRewrite "Hpd".
- - iDestruct 1 as (x ->) "[Hpc Hpd]"; auto 10.
- Qed.
-
- Lemma iProto_dual_message_tele {TT} a (pc : TT -t> V * iProp Σ * iProto Σ V) :
- iProto_dual (iProto_message a (tele_app pc))
- ≡ iProto_message (action_dual a) (tele_app (tele_map (prod_map id iProto_dual) pc)).
- Proof.
- rewrite iProto_dual_message.
- apply iProto_message_proper; apply tforall_forall=> x; by rewrite /=?tele_map_app.
+ apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
Qed.
+ Lemma iMsg_dual_base v P p :
+ iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
+ Proof. apply iMsg_map_base, _. Qed.
+ Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) :
+ iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg.
+ Proof. apply iMsg_map_exist. Qed.
Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
Proof.
intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p). destruct (proto_case p) as [->|(a&pc&->)].
- { by rewrite !iProto_dual_end'. }
- rewrite !iProto_dual_message' involutive.
- iApply proto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
- iIntros "!>"; iApply prop_ext; iIntros "!>"; iSplit.
+ iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&m&->)].
+ { by rewrite !iProto_dual_end. }
+ rewrite !iProto_dual_message involutive.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
+ iApply prop_ext; iIntros "!>"; iSplit.
- iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
- iDestruct "H" as (pdd) "[H Hpd]". iRewrite "Hpd". by iRewrite ("IH" $! pdd).
- - iIntros "H". iExists (iProto_dual p').
- iSplitL; [by auto|]. by iRewrite ("IH" $! p').
+ iDestruct "H" as (pdd) "[H #Hpd]".
+ iApply (bi.internal_eq_rewrite); [|done]; iIntros "!>".
+ iRewrite "Hpd". by iRewrite ("IH" $! pdd).
+ - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists _.
+ rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
Qed.
(** ** Append *)
- Lemma iProto_app_end' p : (proto_end <++> p)%proto ≡ p.
+ Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V).
Proof.
- rewrite iProto_app_eq /iProto_app_def /iProto_map_app.
+ intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
by rewrite proto_elim_end.
Qed.
- Lemma iProto_app_message' a pc p2 :
- (proto_message a pc <++> p2)%proto
- ≡ proto_message a (iProto_map_app_cont (flip iProto_app p2) ∘ pc).
+ Lemma iProto_app_message a m p2 : (<a> m) <++> p2 ≡ <a> m <++> p2.
Proof.
- rewrite iProto_app_eq /iProto_app_def /iProto_map_app.
+ rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- apply: proto_elim_message => a' pc1 pc2 Hpc. f_equiv; solve_proper.
+ apply: proto_elim_message=> a' m1 m2 Hm. f_equiv; solve_proper.
Qed.
Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
@@ -447,326 +476,411 @@ Section proto.
{ intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1.
revert p1'. induction (lt_wf n) as [n _ IH]; intros p1.
- destruct (proto_case p1) as [->|(a&pc&->)].
- { by rewrite !iProto_app_end'. }
- rewrite !iProto_app_message'.
- apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
- do 4 f_equiv. apply IH; eauto using dist_le with lia.
+ destruct (iProto_case p1) as [->|(a&m&->)].
+ { by rewrite !left_id. }
+ rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
+ f_contractive. apply IH; eauto using dist_le with lia.
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_message_eq /iProto_message_def iProto_app_message' /=.
- f_equiv=> v ps /=. iSplit.
- - iDestruct 1 as (p1') "[H Hps]". iDestruct "H" as (x ->) "[Hpc #Hp1']".
- iExists x. iSplit; [done|]. iFrame. iRewrite "Hps". by iRewrite "Hp1'".
- - iDestruct 1 as (x ->) "[Hpc Hps]". auto 10.
- Qed.
-
- Lemma iProto_app_message_tele {TT} a (pc : TT -t> V * iProp Σ * iProto Σ V) p2 :
- (iProto_message a (tele_app pc) <++> p2)%proto
- ≡ iProto_message a (tele_app (tele_map (prod_map id (flip iProto_app p2)) pc)).
- Proof.
- rewrite iProto_app_message.
- apply iProto_message_proper; apply tforall_forall=> x; by rewrite /=?tele_map_app.
- Qed.
+ Lemma iMsg_app_base v P p1 p2 :
+ ((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg.
+ Proof. apply: iMsg_map_base. Qed.
+ Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 :
+ ((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg.
+ Proof. apply iMsg_map_exist. 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_end'. Qed.
- Global Instance iProto_app_end_r : RightId (≡) END%proto (@iProto_app Σ V).
+ Global Instance iProto_app_end_r : RightId (≡) END (@iProto_app Σ V).
Proof.
- rewrite iProto_end_eq /iProto_end_def.
intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p). destruct (proto_case p) as [->|(a&pc&->)].
- { by rewrite iProto_app_end'. }
- rewrite iProto_app_message'.
- iApply proto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
- iIntros "!>". iApply prop_ext; iIntros "!>". iSplit.
- - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'". by iRewrite ("IH" $! p1').
- - iIntros "H". iExists p'. iFrame "H". by iRewrite ("IH" $! p').
+ iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&m&->)].
+ { by rewrite left_id. }
+ rewrite iProto_app_message.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
+ iApply prop_ext; iIntros "!>". iSplit.
+ - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'".
+ iApply (bi.internal_eq_rewrite); [|done]; iIntros "!>".
+ by iRewrite ("IH" $! p1').
+ - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''.
+ rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
Qed.
Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
Proof.
intros p1 p2 p3. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p1). destruct (proto_case p1) as [->|(a&pc&->)].
- { by rewrite !iProto_app_end'. }
- rewrite !iProto_app_message'.
- iApply proto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
- iIntros "!>". iApply prop_ext; iIntros "!>". iSplit.
+ iLöb as "IH" forall (p1). destruct (iProto_case p1) as [->|(a&m&->)].
+ { by rewrite !left_id. }
+ rewrite !iProto_app_message.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
+ iApply prop_ext; iIntros "!>". iSplit.
- iDestruct 1 as (p1') "[H #Hp']".
- iExists (p1' <++> p2)%proto. iSplitL; [by auto|].
- iRewrite "Hp'". iApply "IH".
+ iExists (p1' <++> p2). iSplitL; [by auto|].
+ iRewrite "Hp'". iIntros "!>". iApply "IH".
- iDestruct 1 as (p12) "[H #Hp123]". iDestruct "H" as (p1') "[H #Hp12]".
iExists p1'. iFrame "H". iRewrite "Hp123".
- iRewrite "Hp12". by iRewrite ("IH" $! p1').
+ iIntros "!>". iRewrite "Hp12". by iRewrite ("IH" $! p1').
Qed.
Lemma iProto_dual_app p1 p2 :
- iProto_dual (p1 <++> p2) ≡ (iProto_dual p1 <++> iProto_dual p2)%proto.
+ iProto_dual (p1 <++> p2) ≡ iProto_dual p1 <++> iProto_dual p2.
Proof.
apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p1 p2). destruct (proto_case p1) as [->|(a&pc&->)].
- { by rewrite iProto_dual_end' !iProto_app_end'. }
- rewrite iProto_dual_message' !iProto_app_message' iProto_dual_message' /=.
- iApply proto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=".
- iIntros "!>"; iApply prop_ext; iIntros "!>". iSplit.
+ iLöb as "IH" forall (p1 p2). destruct (iProto_case p1) as [->|(a&m&->)].
+ { by rewrite iProto_dual_end !left_id. }
+ rewrite iProto_dual_message !iProto_app_message iProto_dual_message /=.
+ iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=".
+ iApply prop_ext; iIntros "!>". iSplit.
- iDestruct 1 as (p12d) "[H #Hp12]". iDestruct "H" as (p1') "[H #Hp12d]".
iExists (iProto_dual p1'). iSplitL; [by auto|].
- iRewrite "Hp12". iRewrite "Hp12d". iApply "IH".
+ iRewrite "Hp12". iIntros "!>". iRewrite "Hp12d". iApply "IH".
- iDestruct 1 as (p1') "[H #Hp12]". iDestruct "H" as (p1d) "[H #Hp1']".
- iExists (p1d <++> p2)%proto. iSplitL; [by auto|].
- iRewrite "Hp12". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
+ iExists (p1d <++> p2). iSplitL; [by auto|].
+ iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
Qed.
(** ** Protocol entailment **)
+ 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.
+
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.
+ Global Instance iProto_le_is_except_0 p1 p2 : IsExcept0 (p1 ⊑ p2).
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'. iFrame "Hpc". iApply "IH".
- - rewrite iProto_le_unfold. iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
- iIntros "!>" (v p') "Hpc". iExists p'. iFrame "Hpc". iApply "IH".
+ rewrite /IsExcept0 /sbi_except_0. iIntros "[H|$]".
+ rewrite iProto_le_unfold /iProto_le_pre. iLeft. by iMod "H".
Qed.
- Lemma iProto_le_end_inv p : iProto_le p proto_end -∗ p ≡ proto_end.
+ Lemma iProto_le_end : ⊢ END ⊑ (END : iProto Σ V).
+ Proof. rewrite iProto_le_unfold. iLeft. auto 10. Qed.
+
+ Lemma iProto_le_send m1 m2 :
+ (∀ v p2', m2 v (Next p2') -∗ ◇ ∃ p1', ▷ (p1' ⊑ p2') ∗ m1 v (Next p1')) -∗
+ (<!> m1) ⊑ (<!> m2).
+ Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
+ Lemma iProto_le_recv m1 m2 :
+ (∀ v p1', m1 v (Next p1') -∗ ◇ ∃ p2', ▷ (p1' ⊑ p2') ∗ m2 v (Next p2')) -∗
+ (<?> m1) ⊑ (<?> m2).
+ Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
+ Lemma iProto_le_swap m1 m2 :
+ (∀ v1 v2 p1' p2',
+ m1 v1 (Next p1') -∗ m2 v2 (Next p2') -∗ ◇ ∃ m1' m2' pt,
+ ▷ (p1' ⊑ <!> m1') ∗ ▷ ((<?> m2') ⊑ p2') ∗
+ m1' v2 (Next pt) ∗ m2' v1 (Next pt)) -∗
+ (<?> m1) ⊑ (<!> m2).
+ Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
+
+ Lemma iProto_le_end_inv p : p ⊑ END -∗ ◇ (p ≡ 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 %[].
+ iDestruct "H" as (a1 a2 m1 m2) "(_ & >Heq & _)".
+ by iDestruct (iProto_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 ∗
+ Lemma iProto_le_send_inv p1 m2 :
+ p1 ⊑ (<!> m2) -∗ ∃ a1 m1,
+ ◇ (p1 ≡ <a1> m1) ∗
match a1 with
- | Send => ▷ ∀ v p2', pc2 v p2' -∗ ∃ p1', iProto_le p1' p2' ∗ pc1 v p1'
- | Recv => ▷ ∀ v1 v2 p1' p2',
- pc1 v1 p1' -∗ pc2 v2 p2' -∗ ∃ pc1' pc2' pt,
- iProto_le p1' (proto_message Send pc1') ∗
- iProto_le (proto_message Recv pc2') p2' ∗
- pc1' v2 pt ∗
- pc2' v1 pt
+ | Send => ∀ v p2',
+ m2 v (Next p2') -∗ ◇ ∃ p1', ▷ (p1' ⊑ p2') ∗ m1 v (Next p1')
+ | Recv => ∀ v1 v2 p1' p2',
+ m1 v1 (Next p1') -∗ m2 v2 (Next p2') -∗ ◇ ∃ m1' m2' pt,
+ ▷ (p1' ⊑ <!> m1') ∗ ▷ ((<?> m2') ⊑ p2') ∗
+ m1' v2 (Next pt) ∗ m2' v1 (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 p2').
- - iIntros "!>" (v1 v2 p1' p2'). by iRewrite ("Hpc" $! v2 p2').
+ { iExists inhabitant, inhabitant.
+ iSplit; [|destruct inhabitant];
+ iMod "Heq"; iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
+ iExists _, _; iSplit; [done|]. destruct a1, a2.
+ - iIntros (v p2') "Hm2". iMod "Hp1". iMod "Hp2".
+ iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm".
+ iApply "H". by iRewrite -("Hm" $! v (Next p2')).
+ - done.
+ - iIntros (v1 v2 p1' p2') "Hm1 Hm2". iMod "Hp1". iMod "Hp2".
+ iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm".
+ iApply ("H" with "Hm1"). by iRewrite -("Hm" $! v2 (Next p2')).
+ - iMod "Hp2". iDestruct (iProto_message_equivI with "Hp2") as ([=]) "_".
+ Qed.
+ Lemma iProto_le_send_send_inv m1 m2 v p2' :
+ (<!> m1) ⊑ (<!> m2) -∗
+ m2 v (Next p2') -∗ ◇ ∃ p1', ▷ (p1' ⊑ p2') ∗ m1 v (Next p1').
+ Proof.
+ iIntros "H Hm2". iDestruct (iProto_le_send_inv with "H") as (a m1') "[>Hm1 H]".
+ iDestruct (iProto_message_equivI with "Hm1") as (<-) "Hm1".
+ iMod ("H" with "Hm2") as (p1') "[Hle Hm]".
+ iRewrite -("Hm1" $! v (Next p1')) in "Hm". auto with iFrame.
+ Qed.
+ Lemma iProto_le_recv_send_inv m1 m2 v1 v2 p1' p2' :
+ (<?> m1) ⊑ (<!> m2) -∗
+ m1 v1 (Next p1') -∗ m2 v2 (Next p2') -∗ ◇ ∃ m1' m2' pt,
+ ▷ (p1' ⊑ <!> m1') ∗ ▷ ((<?> m2') ⊑ p2') ∗
+ m1' v2 (Next pt) ∗ m2' v1 (Next pt).
+ Proof.
+ iIntros "H Hm1 Hm2". iDestruct (iProto_le_send_inv with "H") as (a m1') "[>Hm H]".
+ iDestruct (iProto_message_equivI with "Hm") as (<-) "{Hm} #Hm".
+ iApply ("H" with "[Hm1] Hm2"). by iRewrite -("Hm" $! v1 (Next p1')).
Qed.
- Lemma iProto_le_recv_inv p1 pc2 :
- iProto_le p1 (proto_message Recv pc2) -∗ ∃ pc1,
- p1 ≡ proto_message Recv pc1 ∗
- ▷ ∀ v p1', pc1 v p1' -∗ ∃ p2', iProto_le p1' p2' ∗ pc2 v p2'.
+ Lemma iProto_le_recv_inv p1 m2 :
+ p1 ⊑ (<?> m2) -∗ ∃ m1,
+ ◇ (p1 ≡ <?> m1) ∗
+ ∀ v p1', m1 v (Next p1') -∗ ◇ ∃ p2', ▷ (p1' ⊑ p2') ∗ m2 v (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 p2').
+ { iExists inhabitant.
+ iSplit; iMod "Heq"; iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
+ iExists m1. iSplit; iMod "Hp1"; iMod "Hp2";
+ iDestruct (iProto_message_equivI with "Hp2") as (<-) "{Hp2} #Hm2";
+ destruct a1; try done.
+ iIntros (v p1') "Hm". iMod ("H" with "Hm") as (p2') "[Hle Hm]".
+ iExists p2'. iIntros "{$Hle}". by iRewrite ("Hm2" $! v (Next p2')).
+ Qed.
+ Lemma iProto_le_recv_recv_inv m1 m2 v p1' :
+ (<?> m1) ⊑ (<?> m2) -∗
+ m1 v (Next p1') -∗ ◇ ∃ p2', ▷ (p1' ⊑ p2') ∗ m2 v (Next p2').
+ Proof.
+ iIntros "H Hm2". iDestruct (iProto_le_recv_inv with "H") as (m1') "[>Hm1 H]".
+ iApply "H". iDestruct (iProto_message_equivI with "Hm1") as (_) "Hm1".
+ by iRewrite -("Hm1" $! v (Next p1')).
Qed.
- Lemma iProto_le_trans p1 p2 p3 :
- iProto_le p1 p2 -∗ iProto_le p2 p3 -∗ iProto_le p1 p3.
+ Lemma iProto_le_refl p : ⊢ p ⊑ p.
+ Proof.
+ iLöb as "IH" forall (p). destruct (iProto_case p) as [->|([]&m&->)].
+ - iApply iProto_le_end.
+ - iApply iProto_le_send. auto 10 with iFrame.
+ - iApply iProto_le_recv. auto 10 with iFrame.
+ Qed.
+
+ Lemma iProto_le_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ 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]".
+ destruct (iProto_case p3) as [->|([]&m3&->)].
+ - iMod (iProto_le_end_inv with "H2") as "H2". by iRewrite "H2" in "H1".
+ - iDestruct (iProto_le_send_inv with "H2") as (a2 m2) "[>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".
- iDestruct ("H2" with "Hpc") as (p2') "[Hle Hpc]".
- iDestruct ("H1" with "Hpc") as (p1') "[Hle' Hpc]".
- iExists p1'. iFrame "Hpc". by iApply ("IH" with "Hle'").
- * iIntros "!>" (v1 v3 p1' p3') "Hpc1 Hpc3".
- iDestruct ("H2" with "Hpc3") as (p2') "[Hle Hpc2]".
- iDestruct ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(Hp1' & Hp2' & Hpc)".
- 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".
- iDestruct ("H1" with "Hpc1") as (p2') "[Hle Hpc2]".
- iDestruct ("H2" with "Hpc2 Hpc3") as (pc2' pc3' pt) "(Hp2' & Hp3' & Hpc)".
- iExists pc2', pc3', pt. iFrame "Hp3' Hpc". by iApply ("IH" with "Hle").
- - iDestruct (iProto_le_recv_inv with "H2") as (pc2) "[Hp2 H3]".
+ + iDestruct (iProto_le_send_inv with "H1") as (a1 m1) "[>Hp1 H1]".
+ iRewrite "Hp1"; clear p1. destruct a1.
+ * iApply iProto_le_send. iIntros (v p3') "Hm3".
+ iMod ("H2" with "Hm3") as (p2') "[Hle Hm2]".
+ iMod ("H1" with "Hm2") as (p1') "[Hle' Hm1]".
+ iExists p1'. iIntros "{$Hm1} !>". by iApply ("IH" with "Hle'").
+ * iApply iProto_le_swap. iIntros (v1 v3 p1' p3') "Hm1 Hm3".
+ iMod ("H2" with "Hm3") as (p2') "[Hle Hm2]".
+ iMod ("H1" with "Hm1 Hm2") as (m1' m2' pt) "(Hp1' & Hp2' & Hm)".
+ iExists m1', m2', pt. iIntros "{$Hp1' $Hm} !>". by iApply ("IH" with "Hp2'").
+ + iDestruct (iProto_le_recv_inv with "H1") as (m1) "[>Hp1 H1]".
+ iRewrite "Hp1"; clear p1. iApply iProto_le_swap.
+ iIntros (v1 v3 p1' p3') "Hm1 Hm3".
+ iMod ("H1" with "Hm1") as (p2') "[Hle Hm2]".
+ iMod ("H2" with "Hm2 Hm3") as (m2' m3' pt) "(Hp2' & Hp3' & Hm)".
+ iExists m2', m3', pt. iIntros "{$Hp3' $Hm} !>". by iApply ("IH" with "Hle").
+ - iDestruct (iProto_le_recv_inv with "H2") as (m2) "[>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".
- iDestruct ("H2" with "Hpc") as (p2') "[Hle Hpc]".
- iDestruct ("H3" with "Hpc") as (p3') "[Hle' Hpc]".
- iExists p3'. iFrame "Hpc". by iApply ("IH" with "Hle").
+ iDestruct (iProto_le_recv_inv with "H1") as (m1) "[>Hp1 H2]".
+ iRewrite "Hp1". iApply iProto_le_recv. iIntros (v p1') "Hm1".
+ iMod ("H2" with "Hm1") as (p2') "[Hle Hm2]".
+ iMod ("H3" with "Hm2") as (p3') "[Hle' Hm3]".
+ iExists p3'. iIntros "{$Hm3} !>". 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).
+ Lemma iProto_le_base a v P p1 p2 :
+ ▷ (p1 ⊑ p2) -∗
+ (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
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]".
- iDestruct ("H" with "Hpc") as (x1 ?) "[Hpc Hle]".
- iExists (pc1 x1).2. iSplitL "Hle"; [by iRewrite "Heq"|].
- iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
+ rewrite iMsg_base_eq. iIntros "H". destruct a.
+ - iApply iProto_le_send. iIntros (v' p') "(->&Hp&$) !>".
+ iExists p1. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
+ - iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$) !>".
+ iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
+ Qed.
+ Lemma iProto_le_base_swap v1 v2 P1 P2 p :
+ ⊢ (<?> MSG v1 {{ P1 }}; <!> MSG v2 {{ P2 }}; p)
+ ⊑ (<!> MSG v2 {{ P2 }}; <?> MSG v1 {{ P1 }}; p).
+ Proof.
+ rewrite iMsg_base_eq. iApply iProto_le_swap.
+ iIntros (v1' v2' p1' p2') "/= (->&#Hp1&HP1) (->&#Hp2&HP2) !>". iExists _, _, p.
+ iSplitR; [iIntros "!>"; iRewrite -"Hp1"; iApply iProto_le_refl|].
+ iSplitR; [iIntros "!>"; iRewrite -"Hp2"; iApply iProto_le_refl|].
+ simpl; auto with 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 Recv pc1) (iProto_message Recv pc2).
+ Lemma iProto_le_payload_elim_l a m v P p :
+ (P -∗ (<?> MSG v; p) ⊑ (<a> m)) -∗
+ (<?> MSG v {{ P }}; p) ⊑ (<a> m).
+ Proof.
+ rewrite iMsg_base_eq. iIntros "H". destruct a.
+ - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= (#?&#?&HP) Hm2 /=".
+ iApply (iProto_le_recv_send_inv with "(H HP)"); simpl; auto.
+ - iApply iProto_le_recv. iIntros (v' p') "(->&Hp&HP)".
+ iApply (iProto_le_recv_recv_inv with "(H HP)"); simpl; auto.
+ Qed.
+ Lemma iProto_le_payload_elim_r a m v P p :
+ (P -∗ (<a> m) ⊑ (<!> MSG v; p)) -∗
+ (<a> m) ⊑ (<!> MSG v {{ P }}; p).
+ Proof.
+ rewrite iMsg_base_eq. iIntros "H". destruct a.
+ - iApply iProto_le_send. iIntros (v' p') "(->&Hp&HP)".
+ iApply (iProto_le_send_send_inv with "(H HP)"); simpl; auto.
+ - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 (->&#?&HP) /=".
+ iApply (iProto_le_recv_send_inv with "(H HP) Hm1"); simpl; auto.
+ Qed.
+ Lemma iProto_le_payload_intro_l v P p :
+ P -∗ (<!> MSG v {{ P }}; p) ⊑ (<!> MSG v; p).
+ Proof.
+ rewrite iMsg_base_eq.
+ iIntros "HP". iApply iProto_le_send. iIntros (v' p') "(->&Hp&_) !> /=".
+ iExists p'. iSplitR; [iApply iProto_le_refl|]. auto.
+ Qed.
+ Lemma iProto_le_payload_intro_r v P p :
+ P -∗ (<?> MSG v; p) ⊑ (<?> MSG v {{ P }}; p).
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]".
- iDestruct ("H" with "Hpc") as (x2 ?) "[Hpc Hle]".
- iExists (pc2 x2).2. iSplitL "Hle"; [by iRewrite "Heq"|].
- iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
+ rewrite iMsg_base_eq.
+ iIntros "HP". iApply iProto_le_recv. iIntros (v' p') "(->&Hp&_) !> /=".
+ iExists p'. iSplitR; [iApply iProto_le_refl|]. 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 Recv pc4) (pc2 x2).2 ∗
- (pc3 x3).1.2 ∗ (pc4 x4).1.2 ∗
- ((pc3 x3).2 ≡ (pc4 x4).2)) -∗
- iProto_le (iProto_message Recv pc1) (iProto_message Send pc2).
+ Lemma iProto_le_exist_elim_l {A} (m1 : A → iMsg Σ V) a m2 :
+ (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗
+ (<? x> m1 x) ⊑ (<a> m2).
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]".
- iDestruct ("H" with "Hpc1 Hpc2")
- as (TT3 TT4 pc3 pc4 x3 x4 ??) "(H1 & H2 & Hpc1 & Hpc2 & #H)".
- iExists _, _, (pc3 x3).2. iSplitL "H1"; [by iRewrite "Heq1"|].
- iSplitL "H2"; [by iRewrite "Heq2"|]. simpl. iSplitL "Hpc1"; eauto.
+ rewrite iMsg_exist_eq. iIntros "H". destruct a.
+ - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=".
+ iDestruct "Hm1" as (x) "Hm1".
+ iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
+ - iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
+ by iApply (iProto_le_recv_recv_inv with "H").
+ Qed.
+ Lemma iProto_le_exist_elim_r {A} a m1 (m2 : A → iMsg Σ V) :
+ (∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗
+ (<a> m1) ⊑ (<! x> m2 x).
+ Proof.
+ rewrite iMsg_exist_eq. iIntros "H". destruct a.
+ - iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
+ by iApply (iProto_le_send_send_inv with "H").
+ - iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1".
+ iDestruct 1 as (x) "Hm2".
+ iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
+ Qed.
+ Lemma iProto_le_exist_intro_l {A} (m : A → iMsg Σ V) a :
+ ⊢ (<! x> m x) ⊑ (<!> m a).
+ Proof.
+ rewrite iMsg_exist_eq. iApply iProto_le_send. iIntros (v p') "Hm !> /=".
+ iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
+ Qed.
+ Lemma iProto_le_exist_intro_r {A} (m : A → iMsg Σ V) a :
+ ⊢ (<?> m a) ⊑ (<? x> m x).
+ Proof.
+ rewrite iMsg_exist_eq. iApply iProto_le_recv. iIntros (v p') "Hm !> /=".
+ iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
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 Recv (λ 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 Recv (λ x1, (v1 x1, P1 x1, p x1 x2))))).
+ Lemma iProto_le_texist_elim_l {TT : tele} (m1 : TT → iMsg Σ V) a m2 :
+ (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗
+ (<?.. x> m1 x) ⊑ (<a> m2).
+ Proof.
+ iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
+ iApply iProto_le_exist_elim_l; iIntros (x).
+ iApply "IH". iIntros (xs). iApply "H".
+ Qed.
+ Lemma iProto_le_texist_elim_r {TT : tele} a m1 (m2 : TT → iMsg Σ V) :
+ (∀ x, (<a> m1) ⊑ (<!> m2 x)) -∗
+ (<a> m1) ⊑ (<!.. x> m2 x).
+ Proof.
+ iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
+ iApply iProto_le_exist_elim_r; iIntros (x).
+ iApply "IH". iIntros (xs). iApply "H".
+ Qed.
+ Lemma iProto_le_texist_intro_l {TT : tele} (m : TT → iMsg Σ V) x :
+ ⊢ (<!.. x> m x) ⊑ (<!> m x).
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.
+ induction x as [|T TT x xs IH]; simpl; [iApply iProto_le_refl|].
+ iApply iProto_le_trans; [by iApply iProto_le_exist_intro_l|]. iApply IH.
+ Qed.
+ Lemma iProto_le_texist_intro_r {TT : tele} (m : TT → iMsg Σ V) x :
+ ⊢ (<?> m x) ⊑ (<?.. x> m x).
+ Proof.
+ induction x as [|T TT x xs IH]; simpl; [iApply iProto_le_refl|].
+ iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH.
Qed.
- Lemma iProto_le_dual p1 p2 :
- iProto_le p2 p1 -∗ iProto_le (iProto_dual p1) (iProto_dual p2).
+ Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ 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_message').
- rewrite iProto_le_unfold; iRight.
- iExists _, _, _, _; do 2 (iSplit; [done|]); simpl. destruct a2; simpl.
- + iIntros "!>" (v p1d). iDestruct 1 as (p1') "[Hpc #Hp1d]".
- iDestruct ("H" with "Hpc") as (p2') "[H Hpc]".
- iDestruct ("IH" with "H") as "H".
- iExists (iProto_dual p2'). iSplitR "Hpc"; [|by auto]. by iRewrite "Hp1d".
- + iIntros "!>" (v1 v2 p1d p2d).
- iDestruct 1 as (p1') "[Hpc1 #Hp1d]". iDestruct 1 as (p2') "[Hpc2 #Hp2d]".
- iDestruct ("H" with "Hpc2 Hpc1") as (pc1' pc2' pt) "(H1 & H2 & Hpc1 & Hpc2)".
+ destruct (iProto_case p1) as [->|([]&m1&->)].
+ - iMod (iProto_le_end_inv with "H") as "H".
+ iRewrite "H". iApply iProto_le_refl.
+ - iDestruct (iProto_le_send_inv with "H") as (a2 m2) "[>Hp2 H]".
+ iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message).
+ destruct a2; simpl.
+ + iApply iProto_le_recv. iIntros (v p1d).
+ iDestruct 1 as (p1') "[Hm1 #Hp1d]".
+ iMod ("H" with "Hm1") as (p2') "[H Hm2]".
+ iDestruct ("IH" with "H") as "H". iIntros "!>". iExists (iProto_dual p2').
+ iSplitL "H"; [iIntros "!>"; by iRewrite "Hp1d"|]. simpl; auto.
+ + iApply iProto_le_swap. iIntros (v1 p1d v2 p2d).
+ iDestruct 1 as (p1') "[Hm1 #Hp1d]". iDestruct 1 as (p2') "[Hm2 #Hp2d]".
+ iMod ("H" with "Hm2 Hm1") as (m1' m2' pt) "(H1 & H2 & Hm1 & Hm2)".
iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
- rewrite !iProto_dual_message' /=. iExists _, _, (iProto_dual pt).
- iSplitL "H2"; [by iRewrite "Hp1d"|]. iSplitL "H1"; [by iRewrite "Hp2d"|].
- iSplitL "Hpc2"; simpl; auto.
- - iDestruct (iProto_le_recv_inv with "H") as (pc2) "[Hp2 H]".
- iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message' /=).
- rewrite iProto_le_unfold; iRight.
- iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
- iIntros "!>" (v p2d). iDestruct 1 as (p2') "[Hpc #Hp2d]".
- iDestruct ("H" with "Hpc") as (p1') "[H Hpc]".
- iDestruct ("IH" with "H") as "H".
- iExists (iProto_dual p1'). iSplitR "Hpc"; [|by auto]. by iRewrite "Hp2d".
+ rewrite !iProto_dual_message /=. iIntros "!>". iExists _, _, (iProto_dual pt).
+ iSplitL "H2"; [iIntros "!>"; by iRewrite "Hp1d"|].
+ iSplitL "H1"; [iIntros "!>"; by iRewrite "Hp2d"|].
+ iSplitL "Hm2"; simpl; auto.
+ - iDestruct (iProto_le_recv_inv with "H") as (m2) "[>Hp2 H]".
+ iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message /=).
+ iApply iProto_le_send. iIntros (v p2d).
+ iDestruct 1 as (p2') "[Hm2 #Hp2d]".
+ iMod ("H" with "Hm2") as (p1') "[H Hm1]".
+ iDestruct ("IH" with "H") as "H". iIntros "!>". iExists (iProto_dual p1').
+ iSplitL "H"; [iIntros "!>"; by iRewrite "Hp2d"|]. simpl; auto.
Qed.
- Lemma iProto_le_dual_l p1 p2 :
- iProto_le (iProto_dual p2) p1 -∗ iProto_le (iProto_dual p1) p2.
+ Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 -∗ iProto_dual p1 ⊑ p2.
Proof.
iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
by iApply iProto_le_dual.
Qed.
- Lemma iProto_le_dual_r p1 p2 :
- iProto_le p2 (iProto_dual p1) -∗ iProto_le p1 (iProto_dual p2).
+ Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 -∗ p1 ⊑ iProto_dual p2.
Proof.
iIntros "H". iEval (rewrite -(involutive iProto_dual p1)).
by iApply iProto_le_dual.
Qed.
Lemma iProto_le_app p1 p2 p3 p4 :
- iProto_le p1 p2 -∗ iProto_le p3 p4 -∗ iProto_le (p1 <++> p3) (p2 <++> p4).
+ p1 ⊑ p2 -∗ p3 ⊑ p4 -∗ p1 <++> p3 ⊑ p2 <++> p4.
Proof.
iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4).
- destruct (proto_case p2) as [->|([]&pc2&->)].
- - iRewrite (iProto_le_end_inv with "H1"). by rewrite !iProto_app_end'.
- - iDestruct (iProto_le_send_inv with "H1") as (a1 pc1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1.
- rewrite !iProto_app_message'. iEval (rewrite iProto_le_unfold).
- iRight. iExists _, _, _, _; do 2 (iSplit; [done|]). destruct a1; simpl.
- + iIntros "!>" (v p24). iDestruct 1 as (p2') "[Hpc #Hp24]".
- iDestruct ("H1" with "Hpc") as (p1') "[H1 Hpc]".
- iExists (p1' <++> p3)%proto. iSplitR "Hpc"; [|eauto].
- iRewrite "Hp24". by iApply ("IH" with "H1").
- + iIntros "!>" (v1 v2 p13 p24).
- iDestruct 1 as (p1') "[Hpc1 #Hp13]"; iDestruct 1 as (p2') "[Hpc2 #Hp24]".
- iDestruct ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(H1 & H1' & Hpc1 & Hpc2)".
- iExists (iProto_map_app_cont (flip iProto_app p3) ∘ pc1'),
- (iProto_map_app_cont (flip iProto_app p3) ∘ pc2'), (pt <++> p3)%proto.
- rewrite -!iProto_app_message' /=. iSplitL "H1".
- { iRewrite "Hp13". iApply ("IH" with "H1"). iApply iProto_le_refl. }
+ destruct (iProto_case p2) as [->|([]&m2&->)].
+ - iMod (iProto_le_end_inv with "H1") as "H1".
+ iRewrite "H1". by rewrite !left_id.
+ - iDestruct (iProto_le_send_inv with "H1") as (a1 m1) "[>Hp1 H1]".
+ iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. destruct a1; simpl.
+ + iApply iProto_le_send. iIntros (v p24).
+ iDestruct 1 as (p2') "[Hm2 #Hp24]".
+ iMod ("H1" with "Hm2") as (p1') "[H1 Hm1]".
+ iIntros "!>". iExists (p1' <++> p3). iSplitR "Hm1"; [|by simpl; eauto].
+ iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1").
+ + iApply iProto_le_swap. iIntros (v1 v2 p13 p24).
+ iDestruct 1 as (p1') "[Hm1 #Hp13]". iDestruct 1 as (p2') "[Hm2 #Hp24]".
+ iSpecialize ("H1" with "Hm1 Hm2").
+ iMod "H1" as (m1' m2' pt) "(H1 & H1' & Hm1 & Hm2)".
+ iIntros "!>". iExists (m1' <++> p3)%msg, (m2' <++> p3)%msg, (pt <++> p3).
+ rewrite -!iProto_app_message /=. iSplitL "H1".
+ { iIntros "!>". iRewrite "Hp13". iApply ("IH" with "H1"). iApply iProto_le_refl. }
iSplitL "H2 H1'".
- { iRewrite "Hp24". iApply ("IH" with "H1' H2"). }
- iSplitL "Hpc1"; auto.
- - iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1.
- rewrite !iProto_app_message'. iEval (rewrite iProto_le_unfold).
- iRight. iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
- iIntros "!>" (v p13). iDestruct 1 as (p1') "[Hpc #Hp13]".
- iDestruct ("H1" with "Hpc") as (p2'') "[H1 Hpc]".
- iExists (p2'' <++> p4)%proto. iSplitR "Hpc"; [|eauto].
- iRewrite "Hp13". by iApply ("IH" with "H1").
+ { iIntros "!>". iRewrite "Hp24". iApply ("IH" with "H1' H2"). }
+ iSplitL "Hm1"; auto.
+ - iDestruct (iProto_le_recv_inv with "H1") as (m1) "[>Hp1 H1]".
+ iRewrite "Hp1"; clear p1. rewrite !iProto_app_message. iApply iProto_le_recv.
+ iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]".
+ iMod ("H1" with "Hm1") as (p2'') "[H1 Hm2]".
+ iIntros "!>". iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto].
+ iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1").
Qed.
(** ** Lemmas about the auxiliary definitions and invariants *)
@@ -797,7 +911,7 @@ Section proto.
rewrite /iProto_unfold. assert (∀ p, proto_map iProp_unfold iProp_fold
(proto_map 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. }
+ apply proto_map_ext=> // m /=; by rewrite iProp_fold_unfold. }
rewrite -{2}(help p). iRewrite "H✓". by rewrite help.
Qed.
@@ -824,17 +938,17 @@ Section proto.
(∃ p,
⌜ vsl = [] ⌠∗
⌜ vsr = [] ⌠∗
- iProto_le p pl ∗
- iProto_le (iProto_dual p) pr) ∨
- (∃ vl vsl' pc pr',
+ p ⊑ pl ∗
+ iProto_dual p ⊑ pr) ∨
+ (∃ vl vsl' m pr',
⌜ vsl = vl :: vsl' ⌠∗
- iProto_le (proto_message Recv pc) pr ∗
- pc vl pr' ∗
+ (<?> m) ⊑ pr ∗
+ m vl (Next pr') ∗
iProto_interp vsl' vsr pl pr') ∨
- (∃ vr vsr' pc pl',
+ (∃ vr vsr' m pl',
⌜ vsr = vr :: vsr' ⌠∗
- iProto_le (proto_message Recv pc) pl ∗
- pc vr pl' ∗
+ (<?> m) ⊑ pl ∗
+ m vr (Next pl') ∗
iProto_interp vsl vsr' pl' pr).
Proof.
rewrite {1}/iProto_interp. destruct vsl as [|vl vsl]; simpl.
@@ -867,16 +981,16 @@ Section proto.
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.
+ - iDestruct "H" as (vl vsl' m' pr' ->) "(Hpr & Hm' & H)".
+ iRight; iRight. iExists vl, vsl', m', 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.
+ - iDestruct "H" as (vr vsr' m' pl' ->) "(Hpl & Hm' & H)".
+ iRight; iLeft. iExists vr, vsr', m', 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.
+ iProto_interp vsl vsr pl pr -∗ 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.
@@ -884,76 +998,75 @@ Section proto.
- 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.
+ - iDestruct "H" as (vl vsl' m' pr' ->) "(Hpr & Hm' & H)".
+ iRight; iLeft. iExists vl, vsl', m', 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.
+ - iClear "IH". iDestruct "H" as (vr vsr' m' pl'' ->) "(Hpl & Hm' & H)".
+ iRight; iRight. iExists vr, vsr', m', 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'.
+ iProto_interp vsl vsr pl pr -∗ 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' :
+ Lemma iProto_interp_send vl ml vsl vsr pl pr pl' :
iProto_interp vsl vsr pl pr -∗
- iProto_le pl (proto_message Send pcl) -∗
- pcl vl pl' -∗
+ pl ⊑ (<!> ml) -∗
+ ml vl (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.
+ clear pl. iIntros "Hml". remember (length vsl + length vsr) as n eqn:Hn.
+ iInduction (lt_wf n) as [n _] "IH" forall (ml 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_message' /=.
+ rewrite iProto_dual_message /=.
iApply iProto_interp_unfold. iRight; iLeft.
iExists vl, [], _, (iProto_dual pl'). iSplit; [done|]. iFrame "Hp"; simpl.
iSplitL; [by auto|]. iApply iProto_interp_nil.
- - iDestruct "H" as (vl' vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
- iDestruct ("IH" with "[%] [//] H Hpcl") as "H"; [simpl; lia|].
+ - iDestruct "H" as (vl' vsl' m' pr' ->) "(Hpr & Hm' & H)".
+ iDestruct ("IH" with "[%] [//] H Hml") 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.
+ iExists vl', (vsl' ++ [vl]), m', 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".
- iIntros "!>". iRewrite ("Hpc" $! vr' pl'') in "Hpcl'"; clear pc'.
- iDestruct ("Hle" with "Hpcl' Hpcl")
- as (pc1 pc2 pt) "(Hpl'' & Hpl' & Hpc1 & Hpc2)".
+ - iDestruct "H" as (vr' vsr' m' pl'' ->) "(Hle & Hml' & H) /=".
+ iDestruct (iProto_le_send_inv with "Hle") as (a ml') "[>Hm Hle]".
+ iDestruct (iProto_message_equivI with "Hm") as (<-) "Hm".
+ iSpecialize ("Hle" with "[Hml' Hm] Hml").
+ { by iRewrite ("Hm" $! vr' (Next pl'')) in "Hml'". }
+ iMod "Hle" as (m1 m2 pt) "(Hpl'' & Hpl' & Hm1 & Hm2)". iIntros "!>".
iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
- iDestruct ("IH" with "[%] [//] H Hpc1") as "H"; [simpl; lia|..].
+ iDestruct ("IH" with "[%] [//] H Hm1") 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 :
+ Lemma iProto_interp_recv vl vsl vsr pl pr mr :
iProto_interp (vl :: vsl) vsr pl pr -∗
- iProto_le pr (proto_message Recv pcr) -∗
- ▷ ∃ pr, pcr vl pr ∗ iProto_interp vsl vsr pl pr.
+ pr ⊑ (<?> mr) -∗
+ ◇ ∃ pr, mr vl (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".
- iIntros "!>".
- iDestruct ("Hpr" $! vl' pr' with "[Hpc']") as (pr'') "[Hler Hpr]".
- { by iRewrite -("Hpc" $! vl' pr'). }
- 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|].
- iIntros "!>". iExists pr. iFrame "Hpc".
+ - iClear "IH". iDestruct "H" as (vl' vsl' m' pr' [= -> ->]) "(Hpr & Hm' & H)".
+ iDestruct (iProto_le_recv_inv with "Hpr") as (m'') "[>Hm Hpr]".
+ iDestruct (iProto_message_equivI with "Hm") as (_) "{Hm} #Hm".
+ iMod ("Hpr" $! vl' pr' with "[Hm']") as (pr'') "[Hler Hpr]".
+ { by iRewrite -("Hm" $! vl' (Next pr')). }
+ iIntros "!>". iExists pr''. iFrame "Hpr".
+ by iApply (iProto_interp_le_r with "H").
+ - iDestruct "H" as (vr vsr' m' pl'' ->) "(Hpl & Hm' & H)".
+ iMod ("IH" with "[%] [//] H") as (pr) "[Hm H]"; [simpl; lia|].
+ iIntros "!>". iExists pr. iFrame "Hm".
iApply iProto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
Qed.
@@ -963,7 +1076,7 @@ Section proto.
Proof. apply (ne_proper _). Qed.
Lemma iProto_own_le γ s p1 p2 :
- iProto_own γ s p1 -∗ ▷ iProto_le p1 p2 -∗ iProto_own γ s p2.
+ iProto_own γ s p1 -∗ ▷ (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").
@@ -985,91 +1098,157 @@ Section proto.
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 :
+ Lemma iProto_send_l γ m vsr vsl vl p :
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.
+ iProto_own γ Left (<!> m) -∗
+ m vl (Next p) ==∗
+ ▷^(length vsr) iProto_ctx γ (vsl ++ [vl]) vsr ∗
+ iProto_own γ Left p.
Proof.
- rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
- iDestruct 1 as (p) "[Hle Hâ—¯]". iIntros "Hpc".
+ iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ iDestruct 1 as (pl') "[Hle Hâ—¯]". iIntros "Hm".
iDestruct (iProto_own_auth_agree with "Hâ—l Hâ—¯") as "#Hp".
- iAssert (â–· iProto_le pl (iProto_message_def Send pc))%I
+ iAssert (▷ (pl ⊑ <!> m))%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".
+ iDestruct (iProto_interp_send with "Hinterp Hle [Hm]") as "Hinterp".
{ simpl. auto. }
- iMod (iProto_own_auth_update _ _ _ _ (pc x).2 with "Hâ—l Hâ—¯") as "[Hâ—l Hâ—¯]".
+ iMod (iProto_own_auth_update _ _ _ _ p 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.
+ - iIntros "!>". iExists p, pr. iFrame.
+ - iExists p. iFrame. iApply iProto_le_refl.
Qed.
- Lemma iProto_send_r {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) (x : TT) vsr vsl :
+ Lemma iProto_send_r γ m vsr vsl vr p :
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.
+ iProto_own γ Right (<!> m) -∗
+ m vr (Next p) ==∗
+ ▷^(length vsl) iProto_ctx γ vsl (vsr ++ [vr]) ∗
+ iProto_own γ Right p.
Proof.
- rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
- iDestruct 1 as (p) "[Hle Hâ—¯]". iIntros "Hpc".
+ iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ iDestruct 1 as (pr') "[Hle Hâ—¯]". iIntros "Hm".
iDestruct (iProto_own_auth_agree with "Hâ—r Hâ—¯") as "#Hp".
- iAssert (â–· iProto_le pr (iProto_message_def Send pc))%I
+ iAssert (▷ (pr ⊑ <!> m))%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".
+ iDestruct (iProto_interp_send with "Hinterp Hle [Hm]") as "Hinterp".
{ simpl. auto. }
- iMod (iProto_own_auth_update _ _ _ _ (pc x).2 with "Hâ—r Hâ—¯") as "[Hâ—r Hâ—¯]".
+ iMod (iProto_own_auth_update _ _ _ _ p 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.
+ - iIntros "!>". iExists pl, p. iFrame. by iApply iProto_interp_flip.
+ - iExists p. iFrame. iApply iProto_le_refl.
Qed.
- Lemma iProto_recv_l {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) vr vsr vsl :
+ Lemma iProto_recv_l γ m vr vsr vsl :
iProto_ctx γ vsl (vr :: vsr) -∗
- iProto_own γ Left (iProto_message Recv pc) ==∗
- ▷ ◇ ∃ (x : TT),
- ⌜ vr = (pc x).1.1 ⌠∗
+ iProto_own γ Left (<?> m) ==∗
+ ▷ ◇ ∃ p,
iProto_ctx γ vsl vsr ∗
- iProto_own γ Left (pc x).2 ∗
- â–· (pc x).1.2.
+ iProto_own γ Left p ∗
+ m vr (Next p).
Proof.
- rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ 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]".
+ iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hm Hinterp]".
{ iNext. by iRewrite "Hp". }
iMod (iProto_own_auth_update _ _ _ _ q with "Hâ—l Hâ—¯") as "[Hâ—l Hâ—¯]".
- iIntros "!> !> /=".
- iMod (bi.later_exist_except_0 with "Hpc") as (x) "(>-> & Hpc & #Hq)".
- iIntros "!>". iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "Hâ—¯".
+ iIntros "!> !> /=". iMod "Hm"; iMod "Hinterp". iIntros "!>".
+ iExists q. iFrame "Hm". iSplitR "Hâ—¯".
- iExists q, pr. iFrame. by iApply iProto_interp_flip.
- - iExists q. iIntros "{$Hâ—¯} !>". iRewrite "Hq". iApply iProto_le_refl.
+ - iExists q. iIntros "{$Hâ—¯} !>". iApply iProto_le_refl.
Qed.
- Lemma iProto_recv_r {TT} γ (pc : TT → V * iProp Σ * iProto Σ V) vl vsr vsl :
+ Lemma iProto_recv_r γ m vl vsr vsl :
iProto_ctx γ (vl :: vsl) vsr -∗
- iProto_own γ Right (iProto_message Recv pc) ==∗
- ▷ ◇ ∃ (x : TT),
- ⌜ vl = (pc x).1.1 ⌠∗
+ iProto_own γ Right (<?> m) ==∗
+ ▷ ◇ ∃ p,
iProto_ctx γ vsl vsr ∗
- iProto_own γ Right (pc x).2 ∗
- â–· (pc x).1.2.
+ iProto_own γ Right p ∗
+ m vl (Next p).
Proof.
- rewrite iProto_message_eq. iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hinterp)".
+ 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]".
+ iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hm Hinterp]".
{ iNext. by iRewrite "Hp". }
iMod (iProto_own_auth_update _ _ _ _ q with "Hâ—r Hâ—¯") as "[Hâ—r Hâ—¯]".
- iIntros "!> !> /=".
- iMod (bi.later_exist_except_0 with "Hpc") as (x) "(>-> & Hpc & #Hq)".
- iIntros "!>". iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "Hâ—¯".
+ iIntros "!> !> /=". iMod "Hm"; iMod "Hinterp". iIntros "!>".
+ iExists q. iFrame "Hm". iSplitR "Hâ—¯".
- iExists pl, q. iFrame.
- - iExists q. iIntros "{$Hâ—¯} !>". iRewrite "Hq". iApply iProto_le_refl.
+ - iExists q. iIntros "{$Hâ—¯} !>". iApply iProto_le_refl.
+ Qed.
+
+ (** The instances below make it possible to use the tactics [iIntros],
+ [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [iProto_le] goals. *)
+ Global Instance iProto_le_from_forall_l {A} a (m1 : A → iMsg Σ V) m2 :
+ FromForall ((<? x> m1 x) ⊑ (<a> m2)) (λ x, (<?> m1 x) ⊑ (<a> m2))%I | 10.
+ Proof. apply iProto_le_exist_elim_l. Qed.
+ Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A → iMsg Σ V) :
+ FromForall ((<a> m1) ⊑ (<! x> m2 x)) (λ x, (<a> m1) ⊑ (<!> m2 x))%I | 11.
+ Proof. apply iProto_le_exist_elim_r. Qed.
+
+ Global Instance iProto_le_from_wand_l a m v P p :
+ TCIf (TCEq P True%I) False TCTrue →
+ FromWand ((<?> MSG v {{ P }}; p) ⊑ (<a> m)) P ((<?> MSG v; p) ⊑ (<a> m)) | 10.
+ Proof. intros _. apply iProto_le_payload_elim_l. Qed.
+ Global Instance iProto_le_from_wand_r a m v P p :
+ FromWand ((<a> m) ⊑ (<!> MSG v {{ P }}; p)) P ((<a> m) ⊑ (<!> MSG v; p)) | 11.
+ Proof. apply iProto_le_payload_elim_r. Qed.
+
+ Global Instance iProto_le_from_exist_l {A} (m : A → iMsg Σ V) p :
+ FromExist ((<! x> m x) ⊑ p) (λ a, (<!> m a) ⊑ p)%I | 10.
+ Proof.
+ rewrite /FromExist. iDestruct 1 as (x) "H".
+ iApply (iProto_le_trans with "[] H"). iApply iProto_le_exist_intro_l.
+ Qed.
+ Global Instance iProto_le_from_exist_r {A} (m : A → iMsg Σ V) p :
+ FromExist (p ⊑ <? x> m x) (λ a, p ⊑ (<?> m a))%I | 11.
+ Proof.
+ rewrite /FromExist. iDestruct 1 as (x) "H".
+ iApply (iProto_le_trans with "H"). iApply iProto_le_exist_intro_r.
+ Qed.
+
+ Global Instance iProto_le_from_sep_l m v P p :
+ FromSep ((<!> MSG v {{ P }}; p) ⊑ (<!> m)) P ((<!> MSG v; p) ⊑ (<!> m)) | 10.
+ Proof.
+ rewrite /FromSep. iIntros "[HP H]".
+ iApply (iProto_le_trans with "[HP] H"). by iApply iProto_le_payload_intro_l.
Qed.
+ Global Instance iProto_le_from_sep_r m v P p :
+ FromSep ((<?> m) ⊑ (<?> MSG v {{ P }}; p)) P ((<?> m) ⊑ (<?> MSG v; p)) | 11.
+ Proof.
+ rewrite /FromSep. iIntros "[HP H]".
+ iApply (iProto_le_trans with "H"). by iApply iProto_le_payload_intro_r.
+ Qed.
+
+ Global Instance iProto_le_frame_l q m v R P Q p :
+ Frame q R P Q →
+ Frame q R ((<!> MSG v {{ P }}; p) ⊑ (<!> m))
+ ((<!> MSG v {{ Q }}; p) ⊑ (<!> m)) | 10.
+ Proof.
+ rewrite /Frame /=. iIntros (HP) "[HR H]".
+ iApply (iProto_le_trans with "[HR] H"). iApply iProto_le_payload_elim_r.
+ iIntros "HQ". iApply iProto_le_payload_intro_l. iApply HP; iFrame.
+ Qed.
+ Global Instance iProto_le_frame_r q m v R P Q p :
+ Frame q R P Q →
+ Frame q R ((<?> m) ⊑ (<?> MSG v {{ P }}; p))
+ ((<?> m) ⊑ (<?> MSG v {{ Q }}; p)) | 11.
+ Proof.
+ rewrite /Frame /=. iIntros (HP) "[HR H]".
+ iApply (iProto_le_trans with "H"). iApply iProto_le_payload_elim_l.
+ iIntros "HQ". iApply iProto_le_payload_intro_r. iApply HP; iFrame.
+ Qed.
+
+ Global Instance iProto_le_from_modal a v p1 p2 :
+ FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+ ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
+ Proof. apply iProto_le_base. Qed.
End proto.
Typeclasses Opaque iProto_ctx iProto_own.
+
+Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
+ first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 0a0a5cc..b21f06e 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -8,7 +8,7 @@ Important: This file should not be used directly, but rather the wrappers in
Dependent Separation Protocols are modeled as the solution of the following
recursive domain equation:
-[proto = 1 + (action * ▶ (V → proto → PROP))]
+[proto = 1 + (action * (V → ▶ proto → PROP))]
Here, the left-hand side of the sum is used for the terminated process, while
the right-hand side is used for the communication constructors. The type
@@ -16,7 +16,7 @@ the right-hand side is used for the communication constructors. The type
[Recv]. Compared to having an additional sum in [proto], this makes it
possible to factorize the code in a better way.
-The remainder [▶ (V → proto → PROP)] is a predicate that ranges over the
+The remainder [V → ▶ proto → PROP] is a predicate that ranges over the
communicated value [V] and the tail protocol [proto]. Note that to solve this
recursive domain equation using Iris's COFE solver, the recursive occurrence
of [proto] appear under the later [â–¶].
@@ -49,9 +49,9 @@ Module Export action.
End action.
Definition proto_auxO (V : Type) (PROP : ofeT) (A : ofeT) : ofeT :=
- optionO (prodO actionO (laterO (V -d> A -n> PROP))).
+ optionO (prodO actionO (V -d> laterO A -n> PROP)).
Definition proto_auxOF (V : Type) (PROP : ofeT) : oFunctor :=
- optionOF (actionO * ▶ (V -d> ∙ -n> PROP)).
+ optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
Definition proto_result (V : Type) := result_2 (proto_auxOF V).
Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
@@ -77,23 +77,13 @@ Proof. apply (ofe_iso_21 proto_iso). Qed.
Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
proto_fold None.
Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
- (pc : V → proto V PROP PROPn -n> PROP) : proto V PROPn PROP :=
- proto_fold (Some (a, Next pc)).
+ (pc : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
+ proto_fold (Some (a, pc)).
-Instance proto_message_contractive {V} `{!Cofe PROPn, !Cofe PROP} a n :
- Proper (pointwise_relation V (dist_later n) ==> dist n)
- (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
-Proof.
- intros c1 c2 Hc. rewrite /proto_message. f_equiv. do 2 constructor=>//=.
- apply Next_contractive. by destruct n.
-Qed.
Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
Proper (pointwise_relation V (dist n) ==> dist n)
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
-Proof.
- intros c1 c2 Hc. apply proto_message_contractive=> v.
- by destruct n; [|apply dist_S].
-Qed.
+Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
Proper (pointwise_relation V (≡) ==> (≡))
(proto_message (PROPn:=PROPn) (PROP:=PROP) a).
@@ -104,15 +94,14 @@ Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
Proof.
destruct (proto_unfold p) as [[a pc]|] eqn:E; simpl in *; last first.
- left. by rewrite -(proto_fold_unfold p) E.
- - right. destruct (Next_uninj pc) as [pc' Hpc]. exists a, pc'.
- by rewrite /proto_message -Hpc -E proto_fold_unfold.
+ - right. exists a, pc. by rewrite /proto_message -E proto_fold_unfold.
Qed.
Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
Inhabited (proto V PROPn PROP) := populate proto_end.
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 p', pc1 v p' ≡ pc2 v p').
+ ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧ (∀ v p', pc1 v p' ≡ pc2 v p').
Proof.
trans (proto_unfold (proto_message a1 pc1) ≡ proto_unfold (proto_message a2 pc2) : SPROP)%I.
{ iSplit.
@@ -120,7 +109,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 /=.
- rewrite bi.discrete_eq bi.later_equivI bi.discrete_fun_equivI.
+ rewrite bi.discrete_eq bi.discrete_fun_equivI.
by setoid_rewrite bi.ofe_morO_equivI.
Qed.
Lemma proto_message_end_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a pc :
@@ -137,13 +126,13 @@ Proof. by rewrite bi.internal_eq_sym proto_message_end_equivI. Qed.
(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
is contractive *)
Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
- (x : A) (f : action → (V → proto V PROP PROPn -n> PROP) → A)
+ (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
(p : proto V PROPn PROP) : A :=
- match proto_unfold p with None => x | Some (a, pc) => f a (later_car pc) end.
+ match proto_unfold p with None => x | Some (a, pc) => f a pc end.
Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
- (x : A) (f1 f2 : action → (V → proto V PROP PROPn -n> PROP) → A) p1 p2 n :
- (∀ a pc1 pc2, (∀ v, dist_later n (pc1 v) (pc2 v)) → f1 a pc1 ≡{n}≡ f2 a pc2) →
+ (x : A) (f1 f2 : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 n :
+ (∀ a pc1 pc2, (∀ v, pc1 v ≡{n}≡ pc2 v) → f1 a pc1 ≡{n}≡ f2 a pc2) →
p1 ≡{n}≡ p2 →
proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2.
Proof.
@@ -154,7 +143,7 @@ Proof.
Qed.
Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
- (x : A) (f : action → (V → proto V PROP PROPn -n> PROP) → A) :
+ (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) :
proto_elim x f proto_end ≡ x.
Proof.
rewrite /proto_elim /proto_end.
@@ -162,14 +151,14 @@ Proof.
by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
Qed.
Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
- (x : A) (f : action → (V → proto V PROP PROPn -n> PROP) → A)
+ (x : A) (f : action → (V → laterO (proto V PROP PROPn) -n> PROP) → A)
`{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a pc :
proto_elim x f (proto_message a pc) ≡ f a pc.
Proof.
rewrite /proto_elim /proto_message /=.
pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
- (PROP:=PROP) (Some (a, Next pc))) as Hfold.
- destruct (proto_unfold (proto_fold (Some (a, Next pc))))
+ (PROP:=PROP) (Some (a, pc))) as Hfold.
+ destruct (proto_unfold (proto_fold (Some (a, pc))))
as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
by f_equiv=> v.
Qed.
@@ -178,12 +167,10 @@ Qed.
Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
- proto_elim proto_end (λ a pc, proto_message a (λ v, g ◎ pc v ◎ rec)) p.
+ proto_elim proto_end (λ a pc, proto_message a (λ v, g ◎ pc v ◎ laterO_map rec)) p.
Next Obligation.
intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
- apply proto_elim_ne=> // a pc1 pc2 Hpc.
- apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
- do 2 f_equiv. apply Hpc.
+ apply proto_elim_ne=> // a pc1 pc2 Hpc. by repeat f_equiv.
Qed.
Instance proto_map_aux_contractive {V}
@@ -191,8 +178,8 @@ Instance proto_map_aux_contractive {V}
Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
Proof.
intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a pc1 pc2 Hpc.
- apply proto_message_contractive; destruct n as [|n]=> // v p'; simpl in *.
- by rewrite (Hrec p') (Hpc _ (rec2 _)).
+ f_equiv=> v p' /=. do 2 f_equiv; [done|].
+ apply Next_contractive; destruct n as [|n]=> //=.
Qed.
Definition proto_map_aux_2 {V}
@@ -234,7 +221,7 @@ Proof. by rewrite proto_map_unfold /proto_map_aux /= proto_elim_end. Qed.
Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a pc :
proto_map (V:=V) gn g (proto_message a pc)
- ≡ proto_message a (λ v, g ◎ pc v ◎ proto_map g gn).
+ ≡ proto_message a (λ v, g ◎ pc v ◎ laterO_map (proto_map g gn)).
Proof.
rewrite proto_map_unfold /proto_map_aux /=.
apply: proto_elim_message=> a' pc1 pc2 Hpc; f_equiv; solve_proper.
@@ -251,8 +238,8 @@ Proof.
PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
destruct (proto_case p) as [->|(a & pc & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
- apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
- rewrite (dist_S _ _ _ (Hg _)) IH //; auto using dist_S with lia.
+ apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
+ apply Next_contractive; destruct n as [|n]=> //=; auto using dist_S with lia.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
@@ -267,9 +254,8 @@ Proof.
apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
destruct (proto_case p) as [->|(a & pc & ->)]; [by rewrite !proto_map_end|].
- rewrite !proto_map_message /=.
- apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
- by rewrite IH; last lia.
+ rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=. f_equiv.
+ apply Next_contractive; destruct n as [|n]=> //=; auto.
Qed.
Lemma proto_map_compose {V}
`{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
@@ -283,9 +269,8 @@ Proof.
induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
- rewrite !proto_map_message /=.
- apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
- by rewrite IH; last lia.
+ rewrite !proto_map_message /=. apply proto_message_ne=> // v p' /=.
+ do 3 f_equiv. apply Next_contractive; destruct n as [|n]=> //=; auto.
Qed.
Program Definition protoOF (V : Type) (Fn F : oFunctor)
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index 2ad65fe..e45362d 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -112,34 +112,34 @@ Definition prot : iProto Σ :=
(<?> MSG #42; END)%proto.
Definition prot_ref : iProto Σ :=
- (<?> l : loc, MSG #l {{ l ↦ #42 }}; END)%proto.
+ (<? (l : loc)> MSG #l {{ l ↦ #42 }}; END)%proto.
Definition prot_del : iProto Σ :=
- (<?> c : val, MSG c {{ c ↣ prot }}; END)%proto.
+ (<? c> MSG c {{ c ↣ prot }}; END)%proto.
Definition prot_dep : iProto Σ :=
- (<!> x : Z, MSG #x; <?> MSG #(x + 2); END)%proto.
+ (<! (x : Z)> MSG #x; <?> MSG #(x + 2); END)%proto.
Definition prot_dep_ref : iProto Σ :=
- (<!> (l : loc) (x : Z), MSG #l {{ l ↦ #x }};
+ (<! (l : loc) (x : Z)> MSG #l {{ l ↦ #x }};
<?> MSG #() {{ l ↦ #(x + 2) }};
END)%proto.
Definition prot_dep_del : iProto Σ :=
- (<?> c : val, MSG c {{ c ↣ prot_dep }}; END)%proto.
+ (<? c> MSG c {{ c ↣ prot_dep }}; END)%proto.
Definition prot_dep_del_2 : iProto Σ :=
- (<!> c : val, MSG c {{ c ↣ prot_dep }};
+ (<! c> MSG c {{ c ↣ prot_dep }};
<?> MSG #() {{ c ↣ <?> MSG #42; END }};
END)%proto.
Definition prot_dep_del_3 : iProto Σ :=
- (<!> c : val, MSG c {{ c ↣ prot_dep }};
- <!> y : Z, MSG #y; <?> MSG #() {{ c ↣ <?> MSG #(y + 2); END }};
+ (<! c> MSG c {{ c ↣ prot_dep }};
+ <! (y : Z)> MSG #y; <?> MSG #() {{ c ↣ <?> MSG #(y + 2); END }};
END)%proto.
Definition prot_loop_aux (rec : iProto Σ) : iProto Σ :=
- (<!> x : Z, MSG #x; <?> MSG #(x + 2); rec)%proto.
+ (<! (x : Z)> MSG #x; <?> MSG #(x + 2); rec)%proto.
Instance prot_loop_contractive : Contractive prot_loop_aux.
Proof. solve_proto_contractive. Qed.
Definition prot_loop : iProto Σ := fixpoint prot_loop_aux.
@@ -148,9 +148,9 @@ Global Instance prot_loop_unfold :
Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
Definition prot_fun : iProto Σ :=
- (<!> (P : iProp Σ) (Φ : Z → iProp Σ) (vf : val),
+ (<! (P : iProp Σ) (Φ : Z → iProp Σ) (vf : val)>
MSG vf {{ {{{ P }}} vf #() {{{ x, RET #x; Φ x }}} }};
- <?> (vg : val),
+ <? (vg : val)>
MSG vg {{ {{{ P }}} vg #() {{{ x, RET #(x + 2); Φ x }}} }};
END)%proto.
@@ -161,13 +161,13 @@ Fixpoint prot_lock (n : nat) : iProto Σ :=
end%proto.
Definition prot_swap : iProto Σ :=
- (<!> x : Z, MSG #x;
+ (<! (x : Z)> MSG #x;
<?> MSG #20;
<?> MSG #x; END)%proto.
Definition prot_swap_twice : iProto Σ :=
- (<!> x : Z, MSG #x;
- <!> y : Z, MSG #y;
+ (<! (x : Z)> MSG #x;
+ <! (y : Z)> MSG #y;
<?> MSG #20;
<?> MSG #(x+y); END)%proto.
@@ -285,9 +285,9 @@ Proof.
c ↣ iProto_dual (prot_lock n))%I
with "[Hc Hs]"); first by eauto with iFrame.
iIntros (lk γlk) "#Hlk".
- iAssert (□ (client γ ε -∗
- WP acquire lk;; send c #21;; release lk {{ _, True }}))%I as "#Hhelp".
- { iIntros "!> Hcl".
+ iAssert (client γ ε -∗
+ WP acquire lk;; send c #21;; release lk {{ _, True }})%I with "[]" as "#Hhelp".
+ { iIntros "Hcl".
wp_apply (acquire_spec with "[$]"); iIntros "[Hl H]".
iDestruct "H" as (n) "[Hs Hc]".
iDestruct (server_agree with "Hs Hcl") as %[? _].
diff --git a/theories/examples/map.v b/theories/examples/map.v
index 42ca8c1..807535a 100644
--- a/theories/examples/map.v
+++ b/theories/examples/map.v
@@ -72,11 +72,11 @@ Section map.
nat -d> gmultiset A -d> iProto Σ := λ i X,
let rec : nat → gmultiset A → iProto Σ := rec in
(if i is 0 then END else
- ((<!> x v, MSG v {{ IA x v }}; rec i (X ⊎ {[ x ]}))
+ ((<! x v> MSG v {{ IA x v }}; rec i (X ⊎ {[ x ]}))
<+>
rec (pred i) X
) <{⌜ i ≠1 ∨ X = ∅ âŒ}&>
- <?> x (l : loc), MSG #l {{ ⌜ x ∈ X ⌠∗ llist IB l (map x) }};
+ <? x (l : loc)> MSG #l {{ ⌜ x ∈ X ⌠∗ llist IB l (map x) }};
rec i (X ∖ {[ x ]}))%proto.
Instance par_map_protocol_aux_contractive : Contractive par_map_protocol_aux.
Proof. solve_proper_prepare. f_equiv. solve_proto_contractive. Qed.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index d4d3b2c..d8affb6 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -45,13 +45,13 @@ Section sort.
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 }};
- <?> (xs' : list A), MSG #() {{ ⌜ Sorted R xs' ⌠∗ ⌜ xs' ≡ₚ xs ⌠∗ llist I l xs' }};
+ (<! (xs : list A) (l : loc)> MSG #l {{ llist I l xs }};
+ <? (xs' : list A)> MSG #() {{ ⌜ Sorted R xs' ⌠∗ ⌜ xs' ≡ₚ xs ⌠∗ llist I l xs' }};
END)%proto.
Definition sort_protocol_func : iProto Σ :=
- (<!> A (I : A → val → iProp Σ) (R : A → A → Prop)
- `{!RelDecision R, !Total R} (cmp : val),
+ (<! A (I : A → val → iProp Σ) (R : A → A → Prop)
+ `{!RelDecision R, !Total R} (cmp : val)>
MSG cmp {{ cmp_spec I R cmp }};
sort_protocol I R)%proto.
diff --git a/theories/examples/sort_br_del.v b/theories/examples/sort_br_del.v
index b5c85f4..c153b98 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -60,7 +60,7 @@ Section sort_service_br_del.
Qed.
Definition sort_protocol_del_aux (rec : iProto Σ) : iProto Σ :=
- ((<?> c, MSG c {{ c ↣ sort_protocol I R }}; rec) <+> END)%proto.
+ ((<? c> MSG c {{ c ↣ sort_protocol I R }}; rec) <+> END)%proto.
Instance sort_protocol_del_aux_contractive : Contractive sort_protocol_del_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_del : iProto Σ := fixpoint sort_protocol_del_aux.
@@ -83,7 +83,7 @@ Section sort_service_br_del.
Qed.
Definition sort_protocol_br_del_aux (rec : iProto Σ) : iProto Σ :=
- ((sort_protocol I R <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec }}; rec) <+> END))%proto.
+ ((sort_protocol I R <++> rec) <+> ((<? c> MSG c {{ c ↣ rec }}; rec) <+> END))%proto.
Instance sort_protocol_br_del_aux_contractive : Contractive sort_protocol_br_del_aux.
Proof. solve_proto_contractive. Qed.
Definition sort_protocol_br_del : iProto Σ := fixpoint sort_protocol_br_del_aux.
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index f7a4565..f2ef96e 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -79,7 +79,7 @@ Section sort_fg.
Definition sort_fg_tail_protocol_aux (xs : list A)
(rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ ys,
- ((<?> y v, MSG v {{ ⌜ TlRel R y ys ⌠∗ I y v }}; (rec : _ → iProto Σ) (ys ++ [y]))
+ ((<? y v> MSG v {{ ⌜ TlRel R y ys ⌠∗ I y v }}; rec (ys ++ [y]))
<&{⌜ ys ≡ₚ xs âŒ}> END)%proto.
Instance sort_fg_tail_protocol_aux_contractive xs :
@@ -94,7 +94,7 @@ Section sort_fg.
Definition sort_fg_head_protocol_aux
(rec : list A -d> iProto Σ) : list A -d> iProto Σ := λ xs,
- ((<!> x v, MSG v {{ I x v }}; (rec : _ → iProto Σ) (xs ++ [x]))
+ ((<! x v > MSG v {{ I x v }}; (rec : _ → iProto Σ) (xs ++ [x]))
<+> sort_fg_tail_protocol xs [])%proto.
Instance sort_fg_head_protocol_aux_contractive :
@@ -293,8 +293,8 @@ Section sort_fg.
End sort_fg_inner.
Definition sort_fg_func_protocol : iProto Σ :=
- (<!> A (I : A → val → iProp Σ) (R : A → A → Prop)
- `{!RelDecision R, !Total R} (cmp : val),
+ (<! A (I : A → val → iProp Σ) (R : A → A → Prop)
+ `{!RelDecision R, !Total R} (cmp : val)>
MSG cmp {{ cmp_spec I R cmp }};
sort_fg_head_protocol I R [])%proto.
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index e3b76c8..1d8a927 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -22,14 +22,14 @@ Section double.
Context `{heapG Σ, chanG Σ, inG Σ fracR, spawnG Σ}.
Definition prog_prot : iProto Σ :=
- (<?> (x : Z), MSG #x; <?> (y : Z), MSG #y; END)%proto.
+ (<? (x : Z)> MSG #x; <? (y : Z)> MSG #y; END)%proto.
Definition chan_inv (c : val) (γ : gname) : iProp Σ :=
- ((c ↣ prog_prot) ∨
- (own γ (1/2)%Qp ∗ c ↣ (<?> (x : Z), MSG #x; END)%proto) ∨
+ (c ↣ prog_prot ∨
+ (own γ (1/2)%Qp ∗ c ↣ <? (x : Z)> MSG #x; END) ∨
(own γ 1%Qp ∗ c ↣ END))%I.
- Lemma wp_prog (c : val):
+ Lemma wp_prog c :
{{{ ▷ c ↣ prog_prot }}}
prog c
{{{ (k1 k2 : Z), RET (#k1, #k2); True }}}.
@@ -93,13 +93,8 @@ Section double.
iIntros (c) "Hc".
iApply (wp_prog with "[Hc]").
{ iApply (iProto_mapsto_le _ (lsty_car (<??> lty_int; <??> lty_int; END)) with "Hc").
- iApply iProto_le_recv.
- iIntros "!> !> !>" (? [x ->]).
- iExists _. do 2 (iSplit; [done|]).
- iApply iProto_le_recv.
- iIntros "!>" (? [y ->]).
- iExists _. do 2 (iSplit; [done|]).
- iApply iProto_le_refl. }
+ iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists x1.
+ iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists x2. auto. }
iIntros "!>" (k1 k2 _).
iExists _, _. iSplit; first done. eauto.
Qed.
diff --git a/theories/logrel/model.v b/theories/logrel/model.v
index b5d1e71..a44e55e 100644
--- a/theories/logrel/model.v
+++ b/theories/logrel/model.v
@@ -46,13 +46,13 @@ Section lty_ofe.
| lty_kind => λ n S T, lsty_car S ≡{n}≡ lsty_car T
end.
- Lemma lty_mixin k : OfeMixin (lty Σ k).
+ Lemma lty_ofe_mixin k : OfeMixin (lty Σ k).
Proof.
destruct k.
- by apply (iso_ofe_mixin (ltty_car : _ → val -d> _)).
- by apply (iso_ofe_mixin (lsty_car : _ → iProto _)).
Qed.
- Canonical Structure ltyO k := OfeT (lty Σ k) (lty_mixin k).
+ Canonical Structure ltyO k := OfeT (lty Σ k) (lty_ofe_mixin k).
Global Instance lty_cofe k : Cofe (ltyO k).
Proof.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index dec1ee5..9ba6d36 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -5,10 +5,10 @@ From actris.channel Require Export channel.
Definition lty_end {Σ} : lsty Σ := Lsty END.
Definition lty_message {Σ} (a : action) (A : ltty Σ) (S : lsty Σ) : lsty Σ :=
- Lsty (<a> v, MSG v {{ ltty_car A v }}; lsty_car S).
+ Lsty (<a@v> MSG v {{ â–· ltty_car A v }}; lsty_car S).
Definition lty_choice {Σ} (a : action) (Ss : gmap Z (lsty Σ)) : lsty Σ :=
- Lsty (<a> x : Z, MSG #x {{ ⌜is_Some (Ss !! x)⌠}}; lsty_car (Ss !!! x)).
+ Lsty (<a@(x : Z)> MSG #x {{ ⌜is_Some (Ss !! x)⌠}}; lsty_car (Ss !!! x)).
Definition lty_dual {Σ} (S : lsty Σ) : lsty Σ :=
Lsty (iProto_dual (lsty_car S)).
@@ -35,29 +35,22 @@ Section session_types.
Context {Σ : gFunctors}.
Global Instance lty_message_ne a : NonExpansive2 (@lty_message Σ a).
- Proof. intros n A A' ? S S' ?. by apply iProto_message_ne; simpl. Qed.
+ Proof. solve_proper. Qed.
Global Instance lty_message_proper a :
Proper ((≡) ==> (≡) ==> (≡)) (@lty_message Σ a).
Proof. apply ne_proper_2, _. Qed.
Global Instance lty_message_contractive n a :
Proper (dist_later n ==> dist_later n ==> dist n) (@lty_message Σ a).
- Proof.
- intros A A' ? S S' ?.
- apply iProto_message_contractive; simpl; done || by destruct n.
- Qed.
+ Proof. solve_contractive. Qed.
Global Instance lty_choice_ne a : NonExpansive (@lty_choice Σ a).
- Proof.
- intros n Ss1 Ss2 Pseq. apply iProto_message_ne; simpl; solve_proper.
- Qed.
+ Proof. solve_proper. Qed.
Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
- Proof. apply ne_proper. apply _. Qed.
+ Proof. apply ne_proper, _. Qed.
+(* FIXME
Global Instance lty_choice_contractive a : Contractive (@lty_choice Σ a).
- Proof.
- intros ? Ss1 Ss2 ?.
- apply iProto_message_contractive; destruct n; simpl; done || solve_proper.
- Qed.
-
+ Proof. solve_contractive. Qed.
+*)
Global Instance lty_dual_ne : NonExpansive (@lty_dual Σ).
Proof. solve_proper. Qed.
Global Instance lty_dual_proper : Proper ((≡) ==> (≡)) (@lty_dual Σ).
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index fb10025..1a7342a 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -10,11 +10,7 @@ Section subtyping_rules.
(** Generic rules *)
Lemma lty_le_refl {k} (M : lty Σ k) : ⊢ M <: M.
- Proof.
- destruct k.
- - by iIntros (v) "!> H".
- - iModIntro. iApply iProto_le_refl.
- Qed.
+ Proof. destruct k. by iIntros (v) "!> H". by iModIntro. Qed.
Lemma lty_le_trans {k} (M1 M2 M3 : lty Σ k) : M1 <: M2 -∗ M2 <: M3 -∗ M1 <: M3.
Proof.
destruct k.
@@ -254,143 +250,93 @@ Section subtyping_rules.
▷ (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
(<!!> A1 ; S1) <: (<!!> A2 ; S2).
Proof.
- iIntros "#HAle #HSle !>". iApply iProto_le_send; iIntros "!> /=" (x) "H".
- iDestruct ("HAle" with "H") as "H".
- eauto with iFrame.
+ iIntros "#HAle #HSle !>" (v) "H". iExists v.
+ iDestruct ("HAle" with "H") as "$". by iModIntro.
Qed.
Lemma lty_le_recv A1 A2 S1 S2 :
▷ (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
(<??> A1 ; S1) <: (<??> A2 ; S2).
Proof.
- iIntros "#HAle #HSle !>". iApply iProto_le_recv; iIntros "!> /=" (x) "H".
- iDestruct ("HAle" with "H") as "H".
- eauto with iFrame.
+ iIntros "#HAle #HSle !>" (v) "H". iExists v.
+ iDestruct ("HAle" with "H") as "$". by iModIntro.
Qed.
Lemma lty_le_swap_recv_send A1 A2 S :
⊢ (<??> A1; <!!> A2; S) <: (<!!> A2; <??> A1; S).
Proof.
- iIntros "!>". iApply iProto_le_swap. iIntros "!>" (v1 v2) "/= HS1 HS2".
- iExists _, _,
- (tele_app (TT:=[tele _]) (λ v2, (v2, ltty_car A2 v2, lsty_car S))),
- (tele_app (TT:=[tele _]) (λ v1, (v1, ltty_car A1 v1, lsty_car S))),
- v2, v1; simpl.
- do 2 (iSplit; [done|]).
- iFrame "HS1 HS2".
- do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
+ iIntros "!>" (v1 v2).
+ iApply iProto_le_trans;
+ [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ v2)|].
+ iApply iProto_le_trans;
+ [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ v1)]; simpl.
+ iApply iProto_le_base_swap.
Qed.
Lemma lty_le_swap_recv_select A Ss :
- ⊢ (<??> A; lty_select Ss) <: (lty_select ((λ S, <??> A ; S)%lty <$> Ss)).
- Proof.
- iIntros "!>". iApply iProto_le_swap. iIntros "!>" (v1 v2) "/=".
- iIntros "HS1" (HS2).
- iExists _, _,
- (tele_app (TT:=[tele _]) (λ (v2 : Z),(#v2, ⌜is_Some (((λ S : lsty Σ, (<??> A; S)%lty) <$> Ss) !! v2)âŒ%I, lsty_car (Ss !!! v2)))),
- (tele_app (TT:=[tele _]) (λ v1, (v1, ltty_car A v1, lsty_car (Ss !!! v2)))),
- v2, v1; simpl.
- do 2 (iSplit; [done|]).
- iFrame "HS1".
- iSplitL.
- - iApply iProto_le_send=> /=.
- iIntros "!>" (x HSsx). iExists _.
- rewrite lookup_fmap in HSsx.
- apply fmap_is_Some in HSsx.
- do 2 (iSplit; first done).
- iApply iProto_le_refl.
- - iSplit; last done.
- destruct HS2 as [x HS2].
- rewrite !lookup_total_alt !lookup_fmap /=.
- rewrite lookup_fmap in HS2.
- destruct (Ss !! v2); inversion HS2.
- iApply iProto_le_recv=> /=.
- iIntros "!>" (y) "H". iExists _.
- iFrame. iSplit; first done.
- iApply iProto_le_refl.
+ ⊢ (<??> A; lty_select Ss) <: lty_select ((λ S, <??> A; S) <$> Ss)%lty.
+ Proof.
+ iIntros "!>" (v1 x2).
+ iApply iProto_le_trans;
+ [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
+ iApply iProto_le_payload_elim_r.
+ rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
+ iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
+ iModIntro. by iExists v1.
Qed.
Lemma lty_le_swap_branch_send A Ss :
- ⊢ lty_branch ((λ S, <!!> A ; S)%lty <$> Ss) <: (<!!> A ; lty_branch Ss).
- Proof.
- iIntros "!>". iApply iProto_le_swap. iIntros "!>" (v1 v2) "/=".
- iIntros (HS1) "HS2".
- iExists _, _,
- (tele_app (TT:=[tele _]) (λ v2, (v2, ltty_car A v2, lsty_car (Ss !!! v1)))),
- (tele_app (TT:=[tele _]) (λ (v1 : Z),(#v1, ⌜is_Some (((λ S : lsty Σ, (<!!> A; S)%lty) <$> Ss) !! v1)âŒ%I, lsty_car (Ss !!! v1)))),
- v2, v1; simpl.
- do 2 (iSplit; [done|]).
- iFrame "HS2".
- iSplitL.
- - destruct HS1 as [x HS1].
- rewrite !lookup_total_alt !lookup_fmap /=.
- rewrite lookup_fmap in HS1.
- destruct (Ss !! v1); inversion HS1.
- iApply iProto_le_send=> /=.
- iIntros "!>" (y) "H". iExists _.
- iFrame. iSplit; first done.
- iApply iProto_le_refl.
- - iSplit; last done.
- iApply iProto_le_recv=> /=.
- iIntros "!>" (y HSsy). iExists _.
- rewrite lookup_fmap in HSsy.
- apply fmap_is_Some in HSsy.
- do 2 (iSplit; first done).
- iApply iProto_le_refl.
+ ⊢ lty_branch ((λ S, <!!> A; S) <$> Ss)%lty <: (<!!> A; lty_branch Ss).
+ Proof.
+ iIntros "!>" (x1 v2).
+ iApply iProto_le_trans;
+ [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
+ iApply iProto_le_payload_elim_l.
+ rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
+ iApply iProto_le_trans; [|iApply iProto_le_base_swap]. iSplitL; [by eauto|].
+ iModIntro. by iExists v2.
Qed.
Lemma lty_le_select (Ss1 Ss2 : gmap Z (lsty Σ)) :
▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
lty_select Ss1 <: lty_select Ss2.
Proof.
- iIntros "#H1 !>". iApply iProto_le_send; iIntros "!>" (x Hsome).
- iExists x. iSplit; first done. iSplit.
- - iDestruct (big_sepM2_forall with "H1") as "[% _]".
- iPureIntro. naive_solver.
- - iDestruct (big_sepM2_forall with "H1") as "[% H]".
- iApply ("H" with "[] []").
- + iPureIntro. apply lookup_lookup_total; naive_solver.
- + iPureIntro. by apply lookup_lookup_total.
+ iIntros "#H !>" (x); iDestruct 1 as %[S2 HSs2]. iExists x.
+ iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
+ assert (is_Some (Ss1 !! x)) as [S1 HSs1] by naive_solver.
+ rewrite HSs1. iSplitR; [by eauto|].
+ iIntros "!>". rewrite !lookup_total_alt HSs1 HSs2 /=.
+ by iApply ("H" with "[] []").
Qed.
Lemma lty_le_select_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
Ss2 ⊆ Ss1 →
⊢ lty_select Ss1 <: lty_select Ss2.
Proof.
- iIntros (Hle) "!>". iApply iProto_le_send; iIntros "!>" (x Hsome).
- iExists _. iSplit; first done. iSplit.
- { iPureIntro. by eapply lookup_weaken_is_Some. }
- destruct Hsome as [P H1].
- assert (Ss1 !! x = Some P) by eauto using lookup_weaken.
- rewrite (lookup_total_correct Ss1 x P) //.
- rewrite (lookup_total_correct Ss2 x P) //.
- iApply iProto_le_refl.
+ intros; iIntros "!>" (x); iDestruct 1 as %[S HSs2]. iExists x.
+ assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
+ rewrite HSs1. iSplitR; [by eauto|].
+ iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
Qed.
Lemma lty_le_branch (Ss1 Ss2 : gmap Z (lsty Σ)) :
▷ ([∗ map] S1;S2 ∈ Ss1; Ss2, S1 <: S2) -∗
lty_branch Ss1 <: lty_branch Ss2.
Proof.
- iIntros "#H1 !>". iApply iProto_le_recv; iIntros "!>" (x Hsome).
- iExists x. iSplit; first done. iSplit.
- - iDestruct (big_sepM2_forall with "H1") as "[% _]".
- iPureIntro. by naive_solver.
- - iDestruct (big_sepM2_forall with "H1") as "[% H]".
- iApply ("H" with "[] []").
- + iPureIntro. by apply lookup_lookup_total.
- + iPureIntro. by apply lookup_lookup_total; naive_solver.
+ iIntros "#H !>" (x); iDestruct 1 as %[S1 HSs1]. iExists x.
+ iDestruct (big_sepM2_forall with "H") as "{H} [>% H]".
+ assert (is_Some (Ss2 !! x)) as [S2 HSs2] by naive_solver.
+ rewrite HSs2. iSplitR; [by eauto|].
+ iIntros "!>". rewrite !lookup_total_alt HSs1 HSs2 /=.
+ by iApply ("H" with "[] []").
Qed.
Lemma lty_le_branch_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
Ss1 ⊆ Ss2 →
⊢ lty_branch Ss1 <: lty_branch Ss2.
Proof.
- iIntros (Hle) "!>". iApply iProto_le_recv; iIntros "!>" (x Hsome).
- iExists _. iSplit; first done. iSplit.
- { iPureIntro. by eapply lookup_weaken_is_Some. }
- destruct Hsome as [P ?].
- assert (Ss2 !! x = Some P) by eauto using lookup_weaken.
- rewrite (lookup_total_correct Ss1 x P) //.
- rewrite (lookup_total_correct Ss2 x P) //.
- iApply iProto_le_refl.
+ intros; iIntros "!>" (x); iDestruct 1 as %[S HSs1]. iExists x.
+ assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
+ rewrite HSs2. iSplitR; [by eauto|].
+ iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
Qed.
(** Algebraic laws *)
@@ -400,47 +346,32 @@ Section subtyping_rules.
Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
Lemma lty_le_app_id_l S : ⊢ (END <++> S) <:> S.
- Proof. rewrite /lty_app left_id. iSplit; iModIntro; iApply iProto_le_refl. Qed.
+ Proof. rewrite /lty_app left_id. iSplit; by iModIntro. Qed.
Lemma lty_le_app_id_r S : ⊢ (S <++> END) <:> S.
- Proof. rewrite /lty_app right_id. iSplit; iModIntro; iApply iProto_le_refl. Qed.
+ Proof. rewrite /lty_app right_id. iSplit; by iModIntro. Qed.
Lemma lty_le_app_assoc S1 S2 S3 :
⊢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
- Proof. rewrite /lty_app assoc. iSplit; iModIntro; iApply iProto_le_refl. Qed.
+ Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
Lemma lty_le_app_send A S1 S2 : ⊢ (<!!> A; S1) <++> S2 <:> (<!!> A; S1 <++> S2).
Proof.
- rewrite /lty_app iProto_app_message_tele.
- iSplit; iIntros "!>"; iApply iProto_le_refl.
+ rewrite /lty_app iProto_app_message iMsg_app_exist.
+ setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
Qed.
Lemma lty_le_app_recv A S1 S2 : ⊢ (<??> A; S1) <++> S2 <:> (<??> A; S1 <++> S2).
Proof.
- rewrite /lty_app iProto_app_message_tele.
- iSplit; iIntros "!>"; iApply iProto_le_refl.
+ rewrite /lty_app iProto_app_message iMsg_app_exist.
+ setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
Qed.
Lemma lty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
⊢ lty_choice a Ss <++> S2 <:> lty_choice a ((.<++> S2) <$> Ss)%lty.
Proof.
- destruct a.
- - rewrite /lty_app iProto_app_message_tele. iSplit; iIntros "!> /=".
- + iApply iProto_le_send; iIntros "!>" (x [S HSs]); simpl in *.
- move: HSs; rewrite lookup_fmap fmap_Some; intros (S'&HSs&->).
- iExists _; do 2 (iSplit; [by eauto|]).
- rewrite !lookup_total_alt lookup_fmap !HSs /=. iApply iProto_le_refl.
- + iApply iProto_le_send; iIntros "!>" (x [S HSs]); simpl in *.
- iExists _; iSplit; [by eauto|].
- rewrite !lookup_total_alt lookup_fmap !HSs /=.
- iSplit; [by eauto|]. iApply iProto_le_refl.
- - rewrite /lty_app iProto_app_message_tele. iSplit; iIntros "!> /=".
- + iApply iProto_le_recv; iIntros "!>" (x [S HSs]); simpl in *.
- iExists _; iSplit; [by eauto|].
- rewrite !lookup_total_alt lookup_fmap !HSs /=.
- iSplit; [by eauto|]. iApply iProto_le_refl.
- + iApply iProto_le_recv; iIntros "!>" (x [S HSs]); simpl in *.
- move: HSs; rewrite lookup_fmap fmap_Some; intros (S'&HSs&->).
- iExists _; iSplit; [by eauto|].
- rewrite !lookup_total_alt lookup_fmap !HSs /=.
- iSplit; [by eauto|]. iApply iProto_le_refl.
+ rewrite /lty_app /lty_choice iProto_app_message iMsg_app_exist;
+ setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
+ setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
+ iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
+ iDestruct 1 as %[S ->]; iSplitR; eauto.
Qed.
Lemma lty_le_app_select A Ss S2 :
⊢ lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
@@ -462,8 +393,8 @@ Section subtyping_rules.
Lemma lty_le_dual_message a A S :
⊢ lty_dual (lty_message a A S) <:> lty_message (action_dual a) A (lty_dual S).
Proof.
- iSplit; iIntros "!>"; rewrite /lty_dual iProto_dual_message_tele;
- iApply iProto_le_refl.
+ rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
+ setoid_rewrite iMsg_dual_base. iSplit; by iIntros "!> /=".
Qed.
Lemma lty_le_dual_send A S : ⊢ lty_dual (<!!> A; S) <:> (<??> A; lty_dual S).
Proof. apply lty_le_dual_message. Qed.
@@ -473,26 +404,11 @@ Section subtyping_rules.
Lemma lty_le_dual_choice a (Ss : gmap Z (lsty Σ)) :
⊢ lty_dual (lty_choice a Ss) <:> lty_choice (action_dual a) (lty_dual <$> Ss).
Proof.
- destruct a.
- - rewrite /lty_dual iProto_dual_message_tele. iSplit; iIntros "!> /=".
- + iApply iProto_le_recv; iIntros "!>" (x [S HSs]); simpl in *.
- iExists _; iSplit; [by eauto|].
- rewrite !lookup_total_alt lookup_fmap !HSs /=.
- iSplit; [by eauto|]. iApply iProto_le_refl.
- + iApply iProto_le_recv; iIntros "!>" (x [S HSs]); simpl in *.
- move: HSs; rewrite lookup_fmap fmap_Some; intros (S'&HSs&->).
- iExists _; iSplit; [by eauto|].
- rewrite !lookup_total_alt lookup_fmap !HSs /=.
- iSplit; [by eauto|]. iApply iProto_le_refl.
- - rewrite /lty_dual iProto_dual_message_tele. iSplit; iIntros "!> /=".
- + iApply iProto_le_send; iIntros "!>" (x [S HSs]); simpl in *.
- move: HSs; rewrite lookup_fmap fmap_Some; intros (S'&HSs&->).
- iExists _; do 2 (iSplit; [by eauto|]).
- rewrite !lookup_total_alt lookup_fmap !HSs /=. iApply iProto_le_refl.
- + iApply iProto_le_send; iIntros "!>" (x [S HSs]); simpl in *.
- iExists _; iSplit; [by eauto|].
- rewrite !lookup_total_alt lookup_fmap !HSs /=.
- iSplit; [by eauto|]. iApply iProto_le_refl.
+ rewrite /lty_dual /lty_choice iProto_dual_message iMsg_dual_exist;
+ setoid_rewrite iMsg_dual_base; setoid_rewrite lookup_total_alt;
+ setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
+ iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
+ iDestruct 1 as %[S ->]; iSplitR; eauto.
Qed.
Lemma lty_le_dual_select (Ss : gmap Z (lsty Σ)) :
--
GitLab