diff --git a/_CoqProject b/_CoqProject
index d5da394738d0835274ee0c7532dc628d0d882765..98b145e01d55ab2310da730b3ea5705a63ace06e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,5 @@
-Q theories actris
+-Q multi_actris multi_actris
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
@@ -17,11 +18,6 @@ theories/utils/switch.v
theories/channel/proto_model.v
theories/channel/proto.v
theories/channel/channel.v
-theories/channel/multi_proto_model.v
-theories/channel/multi_proto.v
-theories/channel/multi_channel.v
-theories/channel/multi_proofmode.v
-theories/channel/multi_proto_consistency_examples.v
theories/channel/proofmode.v
theories/examples/basics.v
theories/examples/equivalence.v
@@ -58,3 +54,10 @@ theories/logrel/examples/mapper.v
theories/logrel/examples/mapper_list.v
theories/logrel/examples/compute_service.v
theories/logrel/examples/compute_client_list.v
+
+multi_actris/utils/cofe_solver_2.v
+multi_actris/channel/proto_model.v
+multi_actris/channel/proto.v
+multi_actris/channel/channel.v
+multi_actris/channel/proofmode.v
+multi_actris/channel/proto_consistency_examples.v
diff --git a/theories/channel/multi_channel.v b/multi_actris/channel/channel.v
similarity index 99%
rename from theories/channel/multi_channel.v
rename to multi_actris/channel/channel.v
index 0b875093c71635fd66d00c7973c141af3df054c2..89937a2550979a790b45293561e19769fcebf966 100644
--- a/theories/channel/multi_channel.v
+++ b/multi_actris/channel/channel.v
@@ -24,8 +24,8 @@ the subprotocol relation [⊑] *)
From iris.algebra Require Import gmap excl_auth gmap_view.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Export primitive_laws notation proofmode.
-From actris.channel Require Import multi_proto_model.
-From actris.channel Require Export multi_proto.
+From multi_actris.channel Require Import proto_model.
+From multi_actris.channel Require Export proto.
Set Default Proof Using "Type".
(** * The definition of the message-passing connectives *)
diff --git a/theories/channel/multi_proofmode.v b/multi_actris/channel/proofmode.v
similarity index 99%
rename from theories/channel/multi_proofmode.v
rename to multi_actris/channel/proofmode.v
index ff8c57b89428fccb726e3e6fcf6e5f0579547e60..33e7d5ad860613e71515b102e0ea247185ef86cb 100644
--- a/theories/channel/multi_proofmode.v
+++ b/multi_actris/channel/proofmode.v
@@ -9,8 +9,8 @@ In addition to the tactics for symbolic execution, this file defines the tactic
recursive protocols are contractive. *)
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
From iris.heap_lang Require Export proofmode notation.
-From actris.channel Require Import multi_proto_model.
-From actris Require Export multi_channel.
+From multi_actris.channel Require Import proto_model.
+From multi_actris Require Export channel.
Export action.
(** * Tactics for proving contractiveness of protocols *)
diff --git a/theories/channel/multi_proto.v b/multi_actris/channel/proto.v
similarity index 99%
rename from theories/channel/multi_proto.v
rename to multi_actris/channel/proto.v
index e178523852dc71a5bae66aa5e1bf23507fa45546..2575c7a5ab6aca1fb4800cb0bdda83db37190dab 100644
--- a/theories/channel/multi_proto.v
+++ b/multi_actris/channel/proto.v
@@ -50,7 +50,7 @@ From iris.proofmode Require Import proofmode.
From iris.base_logic Require Export lib.iprop.
From iris.base_logic Require Import lib.own.
From iris.program_logic Require Import language.
-From actris.channel Require Import multi_proto_model.
+From multi_actris.channel Require Import proto_model.
Set Default Proof Using "Type".
Export action.
diff --git a/theories/channel/multi_proto_consistency_examples.v b/multi_actris/channel/proto_consistency_examples.v
similarity index 99%
rename from theories/channel/multi_proto_consistency_examples.v
rename to multi_actris/channel/proto_consistency_examples.v
index a52088b7d9ebe61ff432a9472e270e54964ac67b..14771d22b580641554fd0b51792767f68de5447a 100644
--- a/theories/channel/multi_proto_consistency_examples.v
+++ b/multi_actris/channel/proto_consistency_examples.v
@@ -2,9 +2,8 @@ From iris.algebra Require Import gmap excl_auth gmap_view.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Export lib.iprop.
From iris.base_logic Require Import lib.own.
-From actris.channel Require Import multi_proto_model multi_proto multi_channel multi_proofmode.
+From multi_actris.channel Require Import proofmode.
Set Default Proof Using "Type".
-Export action.
Lemma iProto_consistent_equiv_proof {Σ} (ps : gmap nat (iProto Σ)) :
(∀ i j, valid_target ps i j) ∗
diff --git a/theories/channel/multi_proto_model.v b/multi_actris/channel/proto_model.v
similarity index 99%
rename from theories/channel/multi_proto_model.v
rename to multi_actris/channel/proto_model.v
index e32bc264b0452cd3ed3b6d942deeea9dea0c1328..8bd4bd3ef6b0bd8a7c6621eebd9483a34b551166 100644
--- a/theories/channel/multi_proto_model.v
+++ b/multi_actris/channel/proto_model.v
@@ -35,7 +35,7 @@ The defined functions on the type [proto] are:
all terminations [END] in [p1] with [p2]. *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import proofmode.
-From actris.utils Require Import cofe_solver_2.
+From multi_actris.utils Require Import cofe_solver_2.
Set Default Proof Using "Type".
Module Export action.
diff --git a/multi_actris/utils/cofe_solver_2.v b/multi_actris/utils/cofe_solver_2.v
new file mode 100644
index 0000000000000000000000000000000000000000..7a2425ba1241530b55ba7d0572cb276d271f7728
--- /dev/null
+++ b/multi_actris/utils/cofe_solver_2.v
@@ -0,0 +1,88 @@
+From iris.algebra Require Import cofe_solver.
+
+(** Version of the cofe_solver for a parametrized functor. Generalize and move
+to Iris. *)
+Record solution_2 (F : ofe → oFunctor) := Solution2 {
+ solution_2_car : ∀ An `{!Cofe An} A `{!Cofe A}, ofe;
+ solution_2_cofe `{!Cofe An, !Cofe A} : Cofe (solution_2_car An A);
+ solution_2_iso `{!Cofe An, !Cofe A} :>
+ ofe_iso (oFunctor_apply (F A) (solution_2_car A An)) (solution_2_car An A);
+}.
+Arguments solution_2_car {F}.
+Global Existing Instance solution_2_cofe.
+
+Section cofe_solver_2.
+ Context (F : ofe → oFunctor).
+ Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
+ Context `{Fcofe : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
+ Context `{Finh : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
+ Notation map := (oFunctor_map (F _)).
+
+ Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=
+ oFunctor_oFunctor_compose (F A) (F An).
+
+ Definition T_result `{!Cofe An, !Cofe A} : solution (F_2 An A) := solver.result _.
+ Definition T (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : ofe :=
+ T_result (An:=An) (A:=A).
+ Instance T_cofe `{!Cofe An, !Cofe A} : Cofe (T An A) := _.
+ Instance T_inhabited `{!Cofe An, !Cofe A} : Inhabited (T An A) :=
+ populate (ofe_iso_1 T_result inhabitant).
+
+ Definition T_iso_fun_aux `{!Cofe An, !Cofe A}
+ (rec : prodO (oFunctor_apply (F An) (T An A) -n> T A An)
+ (T A An -n> oFunctor_apply (F An) (T An A))) :
+ prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An)) :=
+ (ofe_iso_1 T_result â—Ž map (rec.1,rec.2), map (rec.2,rec.1) â—Ž ofe_iso_2 T_result).
+ Instance T_iso_aux_fun_contractive `{!Cofe An, !Cofe A} :
+ Contractive (T_iso_fun_aux (An:=An) (A:=A)).
+ Proof. solve_contractive. Qed.
+
+ Definition T_iso_fun_aux_2 `{!Cofe An, !Cofe A}
+ (rec : prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An))) :
+ prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An)) :=
+ T_iso_fun_aux (T_iso_fun_aux rec).
+ Instance T_iso_fun_aux_2_contractive `{!Cofe An, !Cofe A} :
+ Contractive (T_iso_fun_aux_2 (An:=An) (A:=A)).
+ Proof.
+ intros n rec1 rec2 Hrec. rewrite /T_iso_fun_aux_2.
+ f_equiv. by apply T_iso_aux_fun_contractive.
+ Qed.
+
+ Definition T_iso_fun `{!Cofe An, !Cofe A} :
+ prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+ (T An A -n> oFunctor_apply (F A) (T A An)) :=
+ fixpoint T_iso_fun_aux_2.
+ Definition T_iso_fun_unfold_1 `{!Cofe An, !Cofe A} y :
+ T_iso_fun (An:=An) (A:=A).1 y ≡ (T_iso_fun_aux (T_iso_fun_aux T_iso_fun)).1 y.
+ Proof. apply (fixpoint_unfold T_iso_fun_aux_2). Qed.
+ Definition T_iso_fun_unfold_2 `{!Cofe An, !Cofe A} y :
+ T_iso_fun (An:=An) (A:=A).2 y ≡ (T_iso_fun_aux (T_iso_fun_aux T_iso_fun)).2 y.
+ Proof. apply (fixpoint_unfold T_iso_fun_aux_2). Qed.
+
+ Lemma result_2 : solution_2 F.
+ Proof using Fcontr Fcofe Finh.
+ apply (Solution2 F T _)=> An Hcn A Hc.
+ apply (OfeIso (T_iso_fun.1) (T_iso_fun.2)).
+ - intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
+ induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
+ rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /=.
+ rewrite -{2}(ofe_iso_12 T_result y). f_equiv.
+ rewrite -(oFunctor_map_id (F _) (ofe_iso_2 T_result y))
+ -!oFunctor_map_compose.
+ f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
+ rewrite ofe_iso_21 -{2}(oFunctor_map_id (F _) x)
+ -!oFunctor_map_compose; do 2 f_equiv; split=> z /=; auto.
+ - intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
+ induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
+ rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /= ofe_iso_21.
+ rewrite -(oFunctor_map_id (F _) y) -!oFunctor_map_compose.
+ f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
+ rewrite -{2}(ofe_iso_12 T_result x); f_equiv;
+ rewrite -{2}(oFunctor_map_id (F _) (ofe_iso_2 T_result x))
+ -!oFunctor_map_compose;
+ do 2 f_equiv; split=> z /=; auto.
+ Qed.
+End cofe_solver_2.
diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 1dbb8d8da11140fd2fe9b754f5ea0ae5ebd93625..e8d038eb646fe47d103a085ed50db99b806f82ba 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -21,85 +21,88 @@ In this file we define the three message-passing connectives:
It is additionaly shown that the channel ownership [c ↣ prot] is closed under
the subprotocol relation [⊑] *)
-From iris.algebra Require Import gmap excl_auth gmap_view.
From iris.heap_lang Require Export primitive_laws notation.
From iris.heap_lang Require Export proofmode.
From iris.heap_lang.lib Require Import spin_lock.
-From actris.utils Require Export llist.
-From actris.channel Require Import proto_model.
From actris.channel Require Export proto.
+From actris.utils Require Import llist skip.
Set Default Proof Using "Type".
+Local Existing Instance spin_lock.
+
(** * The definition of the message-passing connectives *)
Definition new_chan : val :=
- λ: <>, let: "l1" := ref NONEV in
- let: "l2" := ref NONEV in
- (("l1","l2"), ("l2","l1")).
+ λ: <>,
+ let: "l" := lnil #() in
+ let: "r" := lnil #() in
+ let: "lk" := newlock #() in
+ ((("l","r"),"lk"), (("r","l"),"lk")).
Definition fork_chan : val := λ: "f",
let: "cc" := new_chan #() in
Fork ("f" (Snd "cc"));; Fst "cc".
-Definition wait : val :=
- rec: "go" "l" :=
- match: !"l" with
- NONE => #()
- | SOME <> => "go" "l"
- end.
-
Definition send : val :=
λ: "c" "v",
- let: "l" := Fst "c" in
- "l" <- SOME "v";; wait "l".
+ let: "lk" := Snd "c" in
+ let: "l" := Fst (Fst "c") in
+ let: "r" := Snd (Fst "c") in
+ acquire "lk";;
+ lsnoc "l" "v";;
+ release "lk".
-(* Definition recv : val := *)
-(* rec: "go" "c" "i" := *)
-(* let: "l" := Snd (llookup "c" "i") in *)
-(* match: !"l" with *)
-(* NONE => "go" "c" *)
-(* | SOME "v" => "c" <- NONE;; "v" *)
-(* end. *)
+Definition try_recv : val :=
+ λ: "c",
+ let: "lk" := Snd "c" in
+ acquire "lk";;
+ let: "l" := Snd (Fst "c") in
+ let: "ret" := if: lisnil "l" then NONE else SOME (lpop "l") in
+ release "lk";; "ret".
Definition recv : val :=
rec: "go" "c" :=
- let: "l" := Snd "c" in
- let: "v" := Xchg "l" NONEV in
- match: "v" with
- NONE => "go" "c"
- | SOME "v" => "v"
+ match: try_recv "c" with
+ SOME "p" => "p"
+ | NONE => "go" "c"
end.
+(** * Setup of Iris's cameras *)
Class chanG Σ := {
- chanG_tokG :: inG Σ (exclR unitO);
+ chanG_lockG :: lockG Σ;
chanG_protoG :: protoG Σ val;
}.
-Definition chanΣ : gFunctors := #[ protoΣ val; GFunctor (exclR unitO) ].
+Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
Proof. solve_inG. Qed.
+Record chan_name := ChanName {
+ chan_lock_name : gname;
+ chan_proto_name : proto_name;
+}.
+Global Instance chan_name_inhabited : Inhabited chan_name :=
+ populate (ChanName inhabitant inhabitant).
+Global Instance chan_name_eq_dec : EqDecision chan_name.
+Proof. solve_decision. Qed.
+Global Instance chan_name_countable : Countable chan_name.
+Proof.
+ refine (inj_countable (λ '(ChanName γl γr), (γl,γr))
+ (λ '(γl, γr), Some (ChanName γl γr)) _); by intros [].
+Qed.
+
(** * Definition of the pointsto connective *)
Notation iProto Σ := (iProto Σ val).
Notation iMsg Σ := (iMsg Σ val).
-Definition tok `{!chanG Σ} (γ : gname) : iProp Σ := own γ (Excl ()).
-
-Definition chan_inv `{!heapGS Σ, !chanG Σ} γ γE γt s (l:loc) : iProp Σ :=
- (l ↦ NONEV ∗ tok γt) ∨
- (∃ v m, l ↦ SOMEV v ∗
- iProto_own γ s (<!> m)%proto ∗
- (∃ p, iMsg_car m v (Next p) ∗ own γE (â—E (Next p)))) ∨
- (∃ p, l ↦ NONEV ∗
- iProto_own γ s p ∗ own γE (â—E (Next p))).
-
Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
- ∃ γ γE1 γE2 γt1 γt2 s (l1 l2:loc),
- ⌜ c = PairV #l1 #l2 ⌠∗
- inv (nroot.@"ctx") (iProto_ctx γ) ∗
- inv (nroot.@"p") (chan_inv γ γE1 γt1 s l1) ∗
- inv (nroot.@"p") (chan_inv γ γE2 γt2 (side_dual s) l2) ∗
- own γE1 (â—E (Next p)) ∗ own γE1 (â—¯E (Next p)) ∗
- iProto_own γ s p.
+ ∃ γ s (l r : loc) (lk : val),
+ ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌠∗
+ is_lock (chan_lock_name γ) lk (∃ vsl vsr,
+ llist internal_eq l vsl ∗
+ llist internal_eq r vsr ∗
+ steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
+ iProto_ctx (chan_proto_name γ) vsl vsr) ∗
+ iProto_own (chan_proto_name γ) s p.
Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
Definition iProto_pointsto_eq :
@@ -109,6 +112,25 @@ Global Instance: Params (@iProto_pointsto) 4 := {}.
Notation "c ↣ p" := (iProto_pointsto c p)
(at level 20, format "c ↣ p").
+Global Instance iProto_pointsto_contractive `{!heapGS Σ, !chanG Σ} c :
+ Contractive (iProto_pointsto c).
+Proof. rewrite iProto_pointsto_eq. solve_contractive. Qed.
+
+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.
+Global Typeclasses Opaque iProto_choice.
+Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
+Global 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 `{!heapGS Σ, !chanG Σ}.
Implicit Types p : iProto Σ.
@@ -119,12 +141,64 @@ Section channel.
Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
Proof. apply (ne_proper _). Qed.
- (* Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2. *)
- (* Proof. *)
- (* rewrite iProto_pointsto_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. *)
+ Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
+ Proof.
+ rewrite iProto_pointsto_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_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_choice_equiv a1 a2 (P11 P12 P21 P22 : iProp Σ)
+ (p11 p12 p21 p22 : iProto Σ) :
+ ⌜a1 = a2⌠-∗ ((P11 ≡ P12):iProp Σ) -∗ (P21 ≡ P22) -∗
+ ▷ (p11 ≡ p12) -∗ ▷ (p21 ≡ p22) -∗
+ iProto_choice a1 P11 P21 p11 p21 ≡ iProto_choice a2 P12 P22 p12 p22.
+ Proof.
+ iIntros (->) "#HP1 #HP2 #Hp1 #Hp2".
+ rewrite /iProto_choice. iApply iProto_message_equiv; [ eauto | | ].
+ - iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
+ destruct b;
+ [ iRewrite -"HP1"; iFrame "H Hp1" | iRewrite -"HP2"; iFrame "H Hp2" ].
+ - iIntros "!>" (b) "H". iExists b. iSplit; [ done | ].
+ destruct b;
+ [ iRewrite "HP1"; iFrame "H Hp1" | iRewrite "HP2"; iFrame "H Hp2" ].
+ Qed.
+
+ 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_choice iProto_dual_message /= iMsg_dual_exist.
+ f_equiv; f_equiv=> -[]; by rewrite iMsg_dual_base.
+ Qed.
+
+ 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_choice iProto_app_message /= iMsg_app_exist.
+ f_equiv; f_equiv=> -[]; by rewrite iMsg_app_base.
+ Qed.
+
+ 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_choice. destruct a;
+ iIntros (b) "HP"; iExists b; destruct b;
+ iDestruct ("H" with "HP") as "[$ ?]"; by iModIntro.
+ Qed.
(** ** Specifications of [send] and [recv] *)
Lemma new_chan_spec p :
@@ -132,36 +206,19 @@ Section channel.
new_chan #()
{{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
Proof.
- iIntros (Φ _) "HΦ". wp_lam.
- wp_alloc l1 as "Hl1".
- wp_alloc l2 as "Hl2".
+ iIntros (Φ _) "HΦ". wp_lam. iMod (steps_lb_0) as "#Hlb".
+ wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
+ wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
- iMod (own_alloc (â—E (Next p) â‹… â—¯E (Next p))) as (γl) "[Hâ—l Hâ—¯l]".
- { by apply excl_auth_valid. }
- iMod (own_alloc (â—E (Next (iProto_dual p)) â‹… â—¯E (Next (iProto_dual p)))) as (γr) "[Hâ—r Hâ—¯r]".
- { by apply excl_auth_valid. }
- iMod (own_alloc (Excl ())) as (γtl) "Htokl".
- { done. }
- iMod (own_alloc (Excl ())) as (γtr) "Htokr".
- { done. }
- wp_pures.
- iMod (inv_alloc _ ⊤ (iProto_ctx γp) with "[Hctx]")
- as "#IH".
- { done. }
- iMod (inv_alloc _ ⊤ (chan_inv γp γl γtl Left l1) with "[Hl1 Htokl]")
- as "#IHl".
- { iLeft. iFrame. }
- iMod (inv_alloc _ ⊤ (chan_inv γp γr γtr Right l2) with "[Hl2 Htokr]")
- as "#IHr".
- { iLeft. iFrame. }
- iModIntro.
- iApply "HΦ".
- iSplitL "Hcl Hâ—l Hâ—¯l".
- - rewrite iProto_pointsto_eq.
- iExists _, _, _, _, _, _, _, _. eauto with iFrame.
- - rewrite iProto_pointsto_eq.
- iExists _, _, _, _, _, _, _, _.
- iSplit; [done|]. iFrame "#∗".
+ wp_smart_apply (newlock_spec (∃ vsl vsr,
+ llist internal_eq l vsl ∗ llist internal_eq r vsr ∗
+ steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
+ iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
+ { iExists [], []. iFrame "#∗". }
+ iIntros (lk γlk) "#Hlk". wp_pures. iApply "HΦ".
+ set (γ := ChanName γlk γp). iSplitL "Hcl".
+ - rewrite iProto_pointsto_eq. iExists γ, Left, l, r, lk. by iFrame "Hcl #".
+ - rewrite iProto_pointsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
Qed.
Lemma fork_chan_spec p Φ (f : val) :
@@ -176,159 +233,149 @@ Section channel.
wp_pures. iApply ("HΦ" with "Hc1").
Qed.
- Lemma own_prot_excl γ (p1 p2 : iProto Σ) :
- own γ (◯E (Next p1)) -∗ own γ (◯E (Next p2)) -∗ False.
- Proof. Admitted.
-
Lemma send_spec c v p :
{{{ c ↣ <!> MSG v; p }}}
send c v
{{{ RET #(); c ↣ p }}}.
Proof.
rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
- iDestruct "Hc" as (γ γE1 γE2 γt1 γt2 s l1 l2 ->)
- "(#IH & #IHl & #IHr & Hâ— & Hâ—¯ & Hown)".
- wp_pures.
- wp_bind (Store _ _).
- iInv "IHl" as "HIp".
- iDestruct "HIp" as "[HIp|HIp]"; last first.
- { iDestruct "HIp" as "[HIp|HIp]".
- - iDestruct "HIp" as (? m) "(>Hl & Hown' & HIp)".
- wp_store.
- rewrite /iProto_own.
- iDestruct "Hown" as (p') "[_ Hown]".
- iDestruct "Hown'" as (p'') "[_ Hown']".
- iDestruct (own_prot_excl with "Hown Hown'") as "H". done.
- - iDestruct "HIp" as (p') "(>Hl & Hown' & HIp)".
- wp_store.
- rewrite /iProto_own.
- iDestruct "Hown" as (p'') "[_ Hown]".
- iDestruct "Hown'" as (p''') "[_ Hown']".
- iDestruct (own_prot_excl with "Hown Hown'") as "H". done. }
- iDestruct "HIp" as "[>Hl Htok]".
- wp_store.
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]".
- { apply excl_auth_update. }
- iModIntro.
- iSplitL "Hl Hâ— Hown".
- { iRight. iLeft. iIntros "!>". iExists _, _. iFrame.
- iExists _. iFrame. rewrite iMsg_base_eq. simpl. done. }
- wp_pures.
- iLöb as "HL".
- wp_lam.
- wp_bind (Load _).
- iInv "IHl" as "HIp".
- iDestruct "HIp" as "[HIp|HIp]".
- { iDestruct "HIp" as ">[Hl Htok']".
- iDestruct (own_valid_2 with "Htok Htok'") as %H. done. }
- iDestruct "HIp" as "[HIp|HIp]".
- - iDestruct "HIp" as (? m) "(>Hl & Hown & HIp)".
- wp_load. iModIntro.
- iSplitL "Hl Hown HIp".
- { iRight. iLeft. iExists _, _. iFrame. }
- wp_pures. iApply ("HL" with "HΦ Htok H◯").
- - iDestruct "HIp" as (p') "(>Hl & Hown & Hâ—)".
- wp_load.
- iModIntro.
- iSplitL "Hl Htok".
- { iLeft. iFrame. }
- iDestruct (own_valid_2 with "Hâ— Hâ—¯") as "#Hagree".
- iDestruct (excl_auth_agreeI with "Hagree") as "Hagree'".
- wp_pures.
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]".
- { apply excl_auth_update. }
- iModIntro.
- iApply "HΦ".
- iExists _, _, _, _, _, _, _, _.
- iSplit; [done|]. iFrame "#∗".
- iRewrite -"Hagree'". done.
+ iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+ wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+ iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
+ destruct s; simpl.
+ - wp_pures. wp_bind (lsnoc _ _).
+ iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
+ { iApply fupd_mask_intro; [set_solver|]. simpl.
+ iIntros "Hclose !>!>".
+ iMod (iProto_send_l with "Hctx H []") as "[Hctx H]".
+ { rewrite iMsg_base_eq /=; auto. }
+ iModIntro.
+ iApply step_fupdN_intro; [done|].
+ iIntros "!>". iMod "Hclose".
+ iCombine ("Hctx H") as "H".
+ iExact "H". }
+ iApply (wp_lb_update with "Hlbl").
+ wp_smart_apply (lsnoc_spec with "[$Hl //]"); iIntros "Hl".
+ iIntros "#Hlbl' [Hctx H] !>".
+ wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+ { iExists (vsl ++ [v]), vsr.
+ rewrite app_length /=.
+ replace (length vsl + 1) with (S (length vsl)) by lia.
+ iFrame "#∗". }
+ iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
+ - wp_pures. wp_bind (lsnoc _ _).
+ iApply (wp_step_fupdN_lb with "Hlbl [Hctx H]"); [done| |].
+ { iApply fupd_mask_intro; [set_solver|]. simpl.
+ iIntros "Hclose !>!>".
+ iMod (iProto_send_r with "Hctx H []") as "[Hctx H]".
+ { rewrite iMsg_base_eq /=; auto. }
+ iModIntro.
+ iApply step_fupdN_intro; [done|].
+ iIntros "!>". iMod "Hclose".
+ iCombine ("Hctx H") as "H".
+ iExact "H". }
+ iApply (wp_lb_update with "Hlbr").
+ wp_smart_apply (lsnoc_spec with "[$Hr //]"); iIntros "Hr".
+ iIntros "#Hlbr' [Hctx H] !>".
+ wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]").
+ { iExists vsl, (vsr ++ [v]).
+ rewrite app_length /=.
+ replace (length vsr + 1) with (S (length vsr)) by lia.
+ iFrame "#∗". }
+ iIntros "_". iApply "HΦ". iExists γ, Right, l, r, lk. eauto 10 with iFrame.
+ Qed.
+
+ Lemma send_spec_tele {TT} c (tt : TT)
+ (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+ {{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+ send c (v tt)
+ {{{ RET #(); c ↣ (p tt) }}}.
+ Proof.
+ iIntros (Φ) "[Hc HP] HΦ".
+ iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]")
+ as "Hc".
+ { iIntros "!>".
+ iApply iProto_le_trans.
+ iApply iProto_le_texist_intro_l.
+ by iFrame "HP". }
+ by iApply (send_spec with "Hc").
Qed.
- (* Lemma send_spec_tele {TT} c (tt : TT) *)
- (* (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) : *)
- (* {{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}} *)
- (* send c (v tt) *)
- (* {{{ RET #(); c ↣ (p tt) }}}. *)
- (* Proof. *)
- (* iIntros (Φ) "[Hc HP] HΦ". *)
- (* iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]") *)
- (* as "Hc". *)
- (* { iIntros "!>". *)
- (* iApply iProto_le_trans. *)
- (* iApply iProto_le_texist_intro_l. *)
- (* by iFrame "HP". } *)
- (* by iApply (send_spec with "Hc"). *)
- (* Qed. *)
+ 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
+ {{{ 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.
+ rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+ iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+ wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+ iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)". destruct s; simpl.
+ - wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
+ destruct vsr as [|vr vsr]; wp_pures.
+ { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
+ iExists γ, Left, l, r, lk. eauto 10 with iFrame. }
+ wp_smart_apply (lpop_spec with "Hr"); iIntros (v') "[% Hr]"; simplify_eq/=.
+ iMod (iProto_recv_l with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
+ rewrite iMsg_base_eq.
+ iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
+ iDestruct (steps_lb_le _ (length vsr) with "Hlbr") as "#Hlbr'"; [lia|].
+ wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+ iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+ by iRewrite "Hp".
+ - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
+ destruct vsl as [|vl vsl]; wp_pures.
+ { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
+ iExists γ, Right, l, r, lk. eauto 10 with iFrame. }
+ wp_smart_apply (lpop_spec with "Hl"); iIntros (v') "[% Hl]"; simplify_eq/=.
+ iMod (iProto_recv_r with "Hctx H") as (q) "(Hctx & H & Hm)". wp_pures.
+ rewrite iMsg_base_eq.
+ iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
+ iDestruct (steps_lb_le _ (length vsl) with "Hlbl") as "#Hlbl'"; [lia|].
+ wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
+ iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
+ iFrame "HP". iExists γ, Right, l, r, lk. iSplit; [done|]. iFrame "Hlk".
+ by iRewrite "Hp".
+ Qed.
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 v x; c ↣ p x ∗ P x }}}.
Proof.
- iIntros (Φ) "Hc HΦ". iLöb as "HL". wp_lam.
- rewrite iProto_pointsto_eq.
- iDestruct "Hc" as (γ E1 γE2 γt1 γt2 s l1 l2 ->)
- "(#IH & #IHl & #IHr & Hâ— & Hâ—¯ & Hown)".
- wp_pures.
- wp_bind (Xchg _ _).
- iInv "IHr" as "HIp".
- iDestruct "HIp" as "[HIp|HIp]".
- { iDestruct "HIp" as ">[Hl Htok]".
- wp_xchg.
- iModIntro.
- iSplitL "Hl Htok".
- { iLeft. iFrame. }
- wp_pures. iApply ("HL" with "[H◠H◯ Hown] HΦ").
- iExists _, _, _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
- iDestruct "HIp" as "[HIp|HIp]"; last first.
- { iDestruct "HIp" as (p') "[>Hl [Hown' Hâ—¯']]".
- wp_xchg.
- iModIntro.
- iSplitL "Hl Hown' Hâ—¯'".
- { iRight. iRight. iExists _. iFrame. }
- wp_pures. iApply ("HL" with "[H◠H◯ Hown] HΦ").
- iExists _, _, _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
- iDestruct "HIp" as (w m) "(>Hl & Hown' & HIp)".
- iDestruct "HIp" as (p') "[Hm Hp']".
- iInv "IH" as "Hctx".
- wp_xchg.
- destruct s.
- - simpl.
- iMod (iProto_step_r with "Hctx Hown Hown' Hm") as
- (p'') "(Hm & Hctx & Hown & Hown')".
- iModIntro.
- iSplitL "Hctx"; [done|].
- iModIntro.
- iSplitL "Hl Hown' Hp'".
- { iRight. iRight. iExists _. iFrame. }
- wp_pure _.
- rewrite iMsg_base_eq.
- iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
- wp_pures.
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]".
- { apply excl_auth_update. }
- iModIntro. iApply "HΦ".
- iFrame.
- iExists _, _, _, _, _, _, _, _. iSplit; [done|].
- iRewrite "Hp". iFrame "#∗". done.
- - simpl.
- iMod (iProto_step_l with "Hctx Hown' Hown Hm") as
- (p'') "(Hm & Hctx & Hown & Hown')".
- iModIntro.
- iSplitL "Hctx"; [done|].
- iModIntro.
- iSplitL "Hl Hown Hp'".
- { iRight. iRight. iExists _. iFrame. }
- wp_pure _.
- rewrite iMsg_base_eq.
- iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
- wp_pures.
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]".
- { apply excl_auth_update. }
- iModIntro. iApply "HΦ".
- iFrame.
- iExists _, _, _, _, _, _, _, _. iSplit; [done|].
- iRewrite "Hp". iFrame "#∗". done.
+ iIntros (Φ) "Hc HΦ". iLöb as "IH". wp_lam.
+ wp_smart_apply (try_recv_spec with "Hc"); iIntros (w) "[[-> H]|H]".
+ { wp_pures. by iApply ("IH" with "[$]"). }
+ iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
+ Qed.
+
+ (** ** 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_choice. iIntros (Φ) "[Hc HP] HΦ".
+ iApply (send_spec with "[Hc HP] HΦ").
+ iApply (iProto_pointsto_le with "Hc").
+ iIntros "!>". iExists b. by iFrame "HP".
Qed.
+ Lemma branch_spec c P1 P2 p1 p2 :
+ {{{ c ↣ (p1 <{P1}&{P2}> p2) }}}
+ recv c
+ {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}.
+ Proof.
+ rewrite /iProto_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_pointsto_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/proto.v b/theories/channel/proto.v
index f7b54fe1f62e7424c567a4cd8a75c8e8692ec356..92c4c0041d3c88e7b542315014ac3a0f209ab8c9 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -245,53 +245,38 @@ Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
Arguments iProto_dual_if {_ _} _ _%proto.
Global Instance: Params (@iProto_dual_if) 3 := {}.
-Definition iProto_consistent_pre {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ)
- (pl pr : iProto Σ V) : iProp Σ :=
- (∀ a1 a2 m1 m2,
- (pl ≡ <a1> m1) -∗ (pr ≡ <a2> m2) -∗
- match a1,a2 with
- | Send,Recv => ∀ v p1, iMsg_car m1 v (Next p1) -∗
- ∃ p2, iMsg_car m2 v (Next p2) ∗ ▷ (rec p1 p2)
- | Recv,Send => ∀ v p2, iMsg_car m2 v (Next p2) -∗
- ∃ p1, iMsg_car m1 v (Next p1) ∗ ▷ (rec p1 p2)
- | _, _ => True
- end).
-
-Global Instance iProto_consistent_pre_ne {Σ V}
- (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
- NonExpansive2 (iProto_consistent_pre (λ p1 p2, rec p1 p2)).
+(** * Protocol entailment *)
+Definition iProto_le_pre {Σ V}
+ (rec : iProto Σ V → iProto Σ V → iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
+ (p1 ≡ END ∗ p2 ≡ END) ∨
+ ∃ a1 a2 m1 m2,
+ (p1 ≡ <a1> m1) ∗ (p2 ≡ <a2> m2) ∗
+ match a1, a2 with
+ | Recv, Recv => ∀ v p1',
+ iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ rec p1' p2' ∗ iMsg_car m2 v (Next p2')
+ | Send, Send => ∀ v p2',
+ iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ rec p1' p2' ∗ iMsg_car m1 v (Next p1')
+ | Recv, Send => ∀ v1 v2 p1' p2',
+ iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
+ ▷ rec p1' (<!> MSG v2; pt) ∗ ▷ rec (<?> MSG v1; pt) p2'
+ | Send, Recv => False
+ end.
+Global Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
+ NonExpansive2 (iProto_le_pre rec).
Proof. solve_proper. Qed.
-Program Definition iProto_consistent_pre' {Σ V}
- (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
- iProto Σ V -n> iProto Σ V -n> iPropO Σ :=
- λne p1 p2, iProto_consistent_pre (λ p1 p2, rec p1 p2) p1 p2.
+Program Definition iProto_le_pre' {Σ V}
+ (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
+ iProto Σ V -n> iProto Σ V -n> iPropO Σ := λne p1 p2,
+ iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
Solve Obligations with solve_proper.
-
-Local Instance iProto_consistent_pre_contractive {Σ V} : Contractive (@iProto_consistent_pre' Σ V).
+Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
Proof.
- intros n rec1 rec2 Hrec pl pr. rewrite /iProto_consistent_pre' /iProto_consistent_pre /=.
- repeat (f_contractive || f_equiv). done. done.
-Qed.
-
-Definition iProto_consistent {Σ V} (pl pr : iProto Σ V) : iProp Σ :=
- fixpoint iProto_consistent_pre' pl pr.
-
-Arguments iProto_consistent {_ _} _%proto _%proto.
-Global Instance: Params (@iProto_consistent) 2 := {}.
-
-Global Instance iProto_consistent_ne {Σ V} : NonExpansive2 (@iProto_consistent Σ V).
-Proof. solve_proper. Qed.
-Global Instance iProto_consistent_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_consistent Σ V).
-Proof. solve_proper. Qed.
-
-Lemma iProto_consistent_unfold {Σ V} (pl pr : iProto Σ V) :
- iProto_consistent pl pr ≡ (iProto_consistent_pre iProto_consistent) pl pr.
-Proof.
- apply: (fixpoint_unfold iProto_consistent_pre').
+ intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
+ by repeat (f_contractive || f_equiv).
Qed.
Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
- ∀ p3, iProto_consistent p1 p3 -∗ iProto_consistent p2 p3.
+ fixpoint iProto_le_pre' p1 p2.
Arguments iProto_le {_ _} _%proto _%proto.
Global Instance: Params (@iProto_le) 2 := {}.
Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
@@ -306,6 +291,8 @@ Fixpoint iProto_app_recvs {Σ V} (vs : list V) (p : iProto Σ V) : iProto Σ V :
| [] => p
| v :: vs => <?> MSG v; iProto_app_recvs vs p
end.
+Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
+ ∃ p, iProto_app_recvs vsr p ⊑ pl ∗ iProto_app_recvs vsl (iProto_dual p) ⊑ pr.
Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
Global Instance proto_name_inhabited : Inhabited proto_name :=
@@ -338,11 +325,11 @@ Definition iProto_own_auth `{!protoG Σ V} (γ : proto_name) (s : side)
own (side_elim s proto_l_name proto_r_name γ) (â—E (Next p)).
Definition iProto_ctx `{protoG Σ V}
- (γ : proto_name) : iProp Σ :=
+ (γ : proto_name) (vsl vsr : list V) : iProp Σ :=
∃ pl pr,
iProto_own_auth γ Left pl ∗
iProto_own_auth γ Right pr ∗
- â–· iProto_consistent pl pr.
+ â–· iProto_interp vsl vsr pl pr.
(** * The connective for ownership of channel ends *)
Definition iProto_own `{!protoG Σ V}
@@ -617,531 +604,413 @@ Section proto.
iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
Qed.
- Lemma iProto_consistent_flip p1 p2 :
- iProto_consistent p2 p1 -∗
- iProto_consistent p1 p2.
- Proof.
- iLöb as "IH" forall (p1 p2).
- iIntros "Hprot".
- rewrite iProto_consistent_unfold /iProto_consistent_pre.
- rewrite iProto_consistent_unfold /iProto_consistent_pre.
- iIntros (a1 a2 m1 m2) "Hm1 Hm2".
- iDestruct ("Hprot" with "Hm2 Hm1") as "Hprot".
- destruct a1, a2; [done| | |done].
- - iIntros (v p1') "Hm1".
- iDestruct ("Hprot" with "Hm1") as (p2') "[Hprot Hrec]".
- iExists p2'. iFrame. by iApply "IH".
+ (** ** 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.
+
+ 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', iMsg_car m2 v (Next p2') -∗ ∃ p1',
+ ▷ (p1' ⊑ p2') ∗ iMsg_car 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', iMsg_car m1 v (Next p1') -∗ ∃ p2',
+ ▷ (p1' ⊑ p2') ∗ iMsg_car 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',
+ iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
+ ▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2')) -∗
+ (<?> m1) ⊑ (<!> m2).
+ Proof. rewrite iProto_le_unfold. iIntros "H". iRight. auto 10. Qed.
+
+ Lemma iProto_le_end_inv_l p : p ⊑ END -∗ (p ≡ END).
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
+ iDestruct "H" as (a1 a2 m1 m2) "(_ & Heq & _)".
+ by iDestruct (iProto_end_message_equivI with "Heq") as %[].
+ Qed.
+
+ Lemma iProto_le_end_inv_r p : END ⊑ p -∗ (p ≡ END).
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[_ Hp]|H] //".
+ iDestruct "H" as (a1 a2 m1 m2) "(Heq & _ & _)".
+ iDestruct (iProto_end_message_equivI with "Heq") as %[].
+ Qed.
+
+ Lemma iProto_le_send_inv p1 m2 :
+ p1 ⊑ (<!> m2) -∗ ∃ a1 m1,
+ (p1 ≡ <a1> m1) ∗
+ match a1 with
+ | Send => ∀ v p2',
+ iMsg_car m2 v (Next p2') -∗ ∃ p1',
+ ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')
+ | Recv => ∀ v1 v2 p1' p2',
+ iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
+ ▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2')
+ end.
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
+ { 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".
- iDestruct ("Hprot" with "Hm2") as (p1') "[Hprot Hrec]".
- iExists p1'. iFrame. by iApply "IH".
- Qed.
-
- Lemma iProto_consistent_step m1 m2 v p1 :
- iProto_consistent (<!> m1) (<?> m2) -∗
- iMsg_car m1 v (Next p1) -∗
- ∃ p2, iMsg_car m2 v (Next p2) ∗ ▷ iProto_consistent p1 p2.
- Proof.
- iIntros "Hprot Hm1".
- rewrite iProto_consistent_unfold /iProto_consistent_pre.
- iDestruct ("Hprot" with "[//] [//] Hm1") as (p2) "[Hm2 Hprot]".
- iExists p2. iFrame.
- Qed.
-
- Lemma iProto_consistent_dual p :
- ⊢ iProto_consistent p (iProto_dual p).
- Proof.
- iLöb as "IH" forall (p).
- rewrite iProto_consistent_unfold.
- iIntros (a1 a2 m1 m2) "#Hmeq1 #Hmeq2".
- destruct a1, a2; [done| | |done].
- - iIntros (v p') "Hm1".
- iRewrite "Hmeq1" in "Hmeq2".
- rewrite iProto_dual_message. simpl.
- rewrite iProto_message_equivI.
- iDestruct "Hmeq2" as (_) "Hmeq2".
- iSpecialize ("Hmeq2" $! v (Next (iProto_dual p'))).
- iExists (iProto_dual p').
- iRewrite -"Hmeq2".
- iSplitL; [|iNext; by iApply "IH"].
- simpl. iExists p'. iFrame. done.
- - iIntros (v p') "Hm2".
- iRewrite "Hmeq1" in "Hmeq2".
- rewrite iProto_dual_message. simpl.
- rewrite iProto_message_equivI.
- iDestruct "Hmeq2" as (_) "Hmeq2".
- iSpecialize ("Hmeq2" $! v (Next p')).
- iRewrite -"Hmeq2" in "Hm2".
- simpl.
- iDestruct "Hm2" as (p'') "[Hm2 Hmeq']".
- iExists p''. iFrame.
- iNext. iRewrite "Hmeq'".
- iApply "IH".
- Qed.
-
- Lemma iProto_consistent_le_l pl pl' pr :
- iProto_consistent pl pr -∗ pl ⊑ pl' -∗ iProto_consistent pl' pr.
- Proof. iIntros "Hprot Hle". by iApply "Hle". Qed.
- Lemma iProto_consistent_le_r pl pr pr' :
- iProto_consistent pl pr -∗ pr ⊑ pr' -∗ iProto_consistent pl pr'.
- Proof.
- iIntros "H Hle". iApply iProto_consistent_flip.
- iApply "Hle". by iApply iProto_consistent_flip.
+ 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".
+ iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm".
+ iApply ("H" with "Hm1"). by iRewrite -("Hm" $! v2 (Next p2')).
+ - iDestruct (iProto_message_equivI with "Hp2") as ([=]) "_".
+ Qed.
+ Lemma iProto_le_send_send_inv m1 m2 v p2' :
+ (<!> m1) ⊑ (<!> m2) -∗
+ iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car 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".
+ iDestruct ("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) -∗
+ iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt,
+ ▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2').
+ 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_refl p : ⊢ p ⊑ p.
- Proof. iIntros (p') "$". Qed.
+ Lemma iProto_le_recv_inv p1 m2 :
+ p1 ⊑ (<?> m2) -∗ ∃ m1,
+ (p1 ≡ <?> m1) ∗
+ ∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
+ ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
+ iExists m1.
+ iDestruct (iProto_message_equivI with "Hp2") as (<-) "{Hp2} #Hm2".
+ destruct a1; [done|]. iSplit; [done|].
+ iIntros (v p1') "Hm". iDestruct ("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) -∗
+ iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car 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_end : ⊢ END ⊑ (END : iProto Σ V).
- Proof. iApply iProto_le_refl. Qed.
-
- (* Lemma iProto_le_send m1 m2 : *)
- (* (∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1', *)
- (* ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗ *)
- (* (<!> m1) ⊑ (<!> m2). *)
- (* Proof. *)
- (* iLöb as "IH" forall (m1 m2). *)
- (* iIntros "Hle". *)
- (* repeat (unfold iProto_le at 3). *)
- (* iIntros (p) "Hprot". *)
- (* repeat rewrite iProto_consistent_unfold; unfold iProto_consistent_pre. *)
- (* iSplit; [iDestruct "Hprot" as "[Hprot _]"|iDestruct "Hprot" as "[_ Hprot]"]. *)
- (* { iIntros (a m) "H". *)
- (* iDestruct (iProto_message_equivI with "H") as (Heq) "{H} #Hmeq"; subst. *)
- (* iIntros (v p') "Hm". *)
- (* iSpecialize ("Hprot" with "[//]"). *)
- (* iSpecialize ("Hmeq" $! v (Next p')). iRewrite -"Hmeq" in "Hm". *)
- (* iSpecialize ("Hle" $! _ _ with "Hm"). iDestruct "Hle" as (p'') "[Hle Hm]". *)
- (* iApply "Hle". iApply "Hprot". iApply "Hm". } *)
- (* { iIntros (a m) "H". *)
- (* iSpecialize ("Hprot" $! _ _ with "H"). *)
- (* destruct a. *)
- (* - iIntros (v p') "Hm". *)
- (* iApply ("IH" with "[Hle]"). *)
- (* { iNext. iIntros (v' p'') "Hm". *)
- (* iSpecialize ("Hle" with "Hm"). *)
- (* iDestruct "Hle" as (p''') "[Hle Hm]". *)
- (* iExists p'''. iSplitR "Hm"; [iApply "Hle" | iApply "Hm"]. } *)
- (* iApply "Hprot". iApply "Hm". *)
- (* - iIntros (v vs Heq); subst. *)
- (* iSpecialize ("Hprot" $! _ _ eq_refl). *)
- (* iDestruct "Hprot" as (p') "[Hm Hprot]". *)
- (* iExists (p'). iFrame "Hm". *)
- (* iApply ("IH" with "[Hle] [Hprot]"); [|iApply "Hprot"]. *)
- (* iNext. iIntros (v' p'') "Hm". *)
- (* iSpecialize ("Hle" with "Hm"). iDestruct "Hle" as (p''') "[Hle Hm]". *)
- (* iExists p'''; iSplitR "Hm"; [iApply "Hle" |iApply "Hm"]. } *)
- (* Qed. *)
-
- (* Lemma iProto_le_recv m1 m2 : *)
- (* (∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2', *)
- (* ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2')) -∗ *)
- (* (<?> m1) ⊑ (<?> m2). *)
- (* Proof. *)
- (* iIntros "H" (vsl vsr p) "Hprot". *)
- (* iLöb as "IH" forall (vsl vsr m2 p). *)
- (* iEval (rewrite iProto_consistent_unfold). *)
- (* rewrite /iProto_consistent_pre. *)
- (* rewrite iProto_consistent_unfold /iProto_consistent_pre. *)
- (* iSplit; last first. *)
- (* { *)
- (* iDestruct "Hprot" as "[_ Hprot]". *)
- (* iIntros ([] m) "Heq". *)
- (* { iIntros (v vs) "Hm". *)
- (* iDestruct ("Hprot" with "Heq Hm") as "Hprot". *)
- (* iIntros "!>". *)
- (* by iApply ("IH" with "H"). } *)
- (* { iIntros (v vs) "Hm". *)
- (* iDestruct ("Hprot" with "Heq Hm") as (p') "[Hm Hprot]". *)
- (* iExists p'. iFrame. *)
- (* iIntros "!>". *)
- (* by iApply ("IH" with "H"). } *)
- (* } *)
- (* destruct vsr. *)
- (* { iIntros (a m) "Heq". rewrite iProto_message_equivI. *)
- (* iDestruct "Heq" as (<-) "Heq". *)
- (* iIntros (v vs Heq). done. } *)
- (* iIntros (a m) "Heq". rewrite iProto_message_equivI. *)
- (* iDestruct "Heq" as (<-) "Heq". *)
- (* iIntros (w vs Heq). *)
- (* assert (v = w) as <- by set_solver. *)
- (* assert (vsr = vs) as <- by set_solver. *)
- (* iDestruct "Hprot" as "[Hprot _]". *)
- (* iDestruct ("Hprot" with "[//] [//]") as (p') "[Hm Hprot]". *)
- (* iDestruct ("H" with "Hm") as (p'') "[Hle H]". *)
- (* iExists p''. *)
- (* iSpecialize ("Heq" $! v (Next p'')). iRewrite -"Heq". *)
- (* iFrame. iIntros "!>". *)
- (* iApply (iProto_consistent_le_l with "Hprot Hle"). *)
- (* Qed. *)
-
- (* Lemma iProto_le_base a v P p1 p2 : *)
- (* ▷ (p1 ⊑ p2) -∗ *)
- (* (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2). *)
- (* Proof. *)
- (* 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_end_inv_l p : p ⊑ END -∗ (p ≡ END). *)
- (* Proof. *)
- (* rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //". *)
- (* iDestruct "H" as (a1 a2 m1 m2) "(_ & Heq & _)". *)
- (* by iDestruct (iProto_end_message_equivI with "Heq") as %[]. *)
- (* Qed. *)
-
- (* Lemma iProto_le_end_inv_r p : END ⊑ p -∗ (p ≡ END). *)
- (* Proof. *)
- (* rewrite iProto_le_unfold. iIntros "[[_ Hp]|H] //". *)
- (* iDestruct "H" as (a1 a2 m1 m2) "(Heq & _ & _)". *)
- (* iDestruct (iProto_end_message_equivI with "Heq") as %[]. *)
- (* Qed. *)
-
- (* Lemma iProto_le_send_inv p1 m2 : *)
- (* p1 ⊑ (<!> m2) -∗ ∃ a1 m1, *)
- (* (p1 ≡ <a1> m1) ∗ *)
- (* match a1 with *)
- (* | Send => ∀ v p2', *)
- (* iMsg_car m2 v (Next p2') -∗ ∃ p1', *)
- (* ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1') *)
- (* | Recv => ∀ v1 v2 p1' p2', *)
- (* iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt, *)
- (* ▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2') *)
- (* end. *)
- (* Proof. *)
- (* rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]". *)
- (* { 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". *)
- (* 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". *)
- (* iDestruct (iProto_message_equivI with "Hp2") as (_) "{Hp2} #Hm". *)
- (* iApply ("H" with "Hm1"). by iRewrite -("Hm" $! v2 (Next p2')). *)
- (* - iDestruct (iProto_message_equivI with "Hp2") as ([=]) "_". *)
- (* Qed. *)
- (* Lemma iProto_le_send_send_inv m1 m2 v p2' : *)
- (* (<!> m1) ⊑ (<!> m2) -∗ *)
- (* iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car 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". *)
- (* iDestruct ("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) -∗ *)
- (* iMsg_car m1 v1 (Next p1') -∗ iMsg_car m2 v2 (Next p2') -∗ ∃ pt, *)
- (* ▷ (p1' ⊑ <!> MSG v2; pt) ∗ ▷ ((<?> MSG v1; pt) ⊑ p2'). *)
- (* 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 m2 : *)
- (* p1 ⊑ (<?> m2) -∗ ∃ m1, *)
- (* (p1 ≡ <?> m1) ∗ *)
- (* ∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2', *)
- (* ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2'). *)
- (* Proof. *)
- (* rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]". *)
- (* { iDestruct (iProto_message_end_equivI with "Heq") as %[]. } *)
- (* iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)". *)
- (* iExists m1. *)
- (* iDestruct (iProto_message_equivI with "Hp2") as (<-) "{Hp2} #Hm2". *)
- (* destruct a1; [done|]. iSplit; [done|]. *)
- (* iIntros (v p1') "Hm". iDestruct ("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) -∗ *)
- (* iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car 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_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_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" (p) "Hprot".
- iApply "H2". iApply "H1". done.
- Qed.
-
- (* 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. *)
- (* 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_exist_elim_l {A} (m1 : A → iMsg Σ V) a m2 : *)
- (* (∀ x, (<?> m1 x) ⊑ (<a> m2)) -∗ *)
- (* (<? x> m1 x) ⊑ (<a> m2). *)
- (* Proof. *)
- (* 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_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p : *)
- (* (∀ x, (<?> m x) ⊑ p) -∗ *)
- (* (<? x> m x) ⊑ p. *)
- (* Proof. *)
- (* rewrite iMsg_exist_eq. iIntros "H". *)
- (* destruct (iProto_case p) as [Heq | [a [m' Heq]]]. *)
- (* - unshelve iSpecialize ("H" $!inhabitant); first by apply _. *)
- (* rewrite Heq. *)
- (* iDestruct (iProto_le_end_inv_l with "H") as "H". *)
- (* rewrite iProto_end_eq iProto_message_eq. *)
- (* iDestruct (proto_message_end_equivI with "H") as "[]". *)
- (* - iEval (rewrite Heq). destruct a. *)
- (* + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=". *)
- (* iDestruct "Hm1" as (x) "Hm1". *)
- (* iSpecialize ("H" $! x). rewrite Heq. *)
- (* iApply (iProto_le_recv_send_inv with "H Hm1 Hm2"). *)
- (* + iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm". *)
- (* iSpecialize ("H" $! x). rewrite Heq. *)
- (* 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_elim_r_inhabited `{Hinh : Inhabited A} p (m : A → iMsg Σ V) : *)
- (* (∀ x, p ⊑ (<!> m x)) -∗ *)
- (* p ⊑ (<! x> m x). *)
- (* Proof. *)
- (* rewrite iMsg_exist_eq. iIntros "H". *)
- (* destruct (iProto_case p) as [Heq | [a [m' Heq]]]. *)
- (* - unshelve iSpecialize ("H" $!inhabitant); first by apply _. *)
- (* rewrite Heq. *)
- (* iDestruct (iProto_le_end_inv_r with "H") as "H". *)
- (* rewrite iProto_end_eq iProto_message_eq. *)
- (* iDestruct (proto_message_end_equivI with "H") as "[]". *)
- (* - iEval (rewrite Heq). destruct a. *)
- (* + iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm". *)
- (* iSpecialize ("H" $! x). rewrite Heq. *)
- (* by iApply (iProto_le_send_send_inv with "H"). *)
- (* + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1". *)
- (* iDestruct 1 as (x) "Hm2". *)
- (* iSpecialize ("H" $! x). rewrite Heq. *)
- (* 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_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. *)
- (* induction x as [|T TT x xs IH] using tele_arg_ind; 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] using tele_arg_ind; simpl. *)
- (* { iApply iProto_le_refl. } *)
- (* iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH. *)
- (* Qed. *)
-
- (* Lemma iProto_le_base a v P p1 p2 : *)
- (* ▷ (p1 ⊑ p2) -∗ *)
- (* (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2). *)
- (* Proof. *)
- (* 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 {1 3}iMsg_base_eq. iApply iProto_le_swap. *)
- (* iIntros (v1' v2' p1' p2') "/= (->&#Hp1&HP1) (->&#Hp2&HP2)". iExists p. *)
- (* iSplitL "HP2". *)
- (* - iIntros "!>". iRewrite -"Hp1". by iApply iProto_le_payload_intro_l. *)
- (* - iIntros "!>". iRewrite -"Hp2". by iApply iProto_le_payload_intro_r. *)
- (* Qed. *)
-
- (* 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 (iProto_case p1) as [->|([]&m1&->)]. *)
- (* - iDestruct (iProto_le_end_inv_l 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]". *)
- (* iDestruct ("H" with "Hm1") as (p2') "[H Hm2]". *)
- (* iDestruct ("IH" with "H") as "H". iExists (iProto_dual p2'). *)
- (* iSplitL "H"; [iIntros "!>"; by iRewrite "Hp1d"|]. simpl; auto. *)
- (* + iApply iProto_le_swap. iIntros (v1 v2 p1d p2d). *)
- (* iDestruct 1 as (p1') "[Hm1 #Hp1d]". iDestruct 1 as (p2') "[Hm2 #Hp2d]". *)
- (* iDestruct ("H" with "Hm2 Hm1") as (pt) "[H1 H2]". *)
- (* iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}". *)
- (* rewrite !iProto_dual_message /=. iExists (iProto_dual pt). iSplitL "H2". *)
- (* * iIntros "!>". iRewrite "Hp1d". by rewrite -iMsg_dual_base. *)
- (* * iIntros "!>". iRewrite "Hp2d". by rewrite -iMsg_dual_base. *)
- (* - 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]". *)
- (* iDestruct ("H" with "Hm2") as (p1') "[H Hm1]". *)
- (* iDestruct ("IH" with "H") as "H". iExists (iProto_dual p1'). *)
- (* iSplitL "H"; [iIntros "!>"; by iRewrite "Hp2d"|]. simpl; auto. *)
- (* Qed. *)
-
- (* Lemma iProto_le_amber_internal (p1 p2 : iProto Σ V → iProto Σ V) *)
- (* `{Contractive p1, Contractive p2}: *)
- (* □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) -∗ *)
- (* fixpoint p1 ⊑ fixpoint p2. *)
- (* Proof. *)
- (* iIntros "#H". iLöb as "IH". *)
- (* iEval (rewrite (fixpoint_unfold p1)). *)
- (* iEval (rewrite (fixpoint_unfold p2)). *)
- (* iApply "H". iApply "IH". *)
- (* Qed. *)
- (* Lemma iProto_le_amber_external (p1 p2 : iProto Σ V → iProto Σ V) *)
- (* `{Contractive p1, Contractive p2}: *)
- (* (∀ rec1 rec2, (⊢ rec1 ⊑ rec2) → ⊢ p1 rec1 ⊑ p2 rec2) → *)
- (* ⊢ fixpoint p1 ⊑ fixpoint p2. *)
- (* Proof. *)
- (* intros IH. apply fixpoint_ind. *)
- (* - by intros p1' p2' -> ?. *)
- (* - exists (fixpoint p2). iApply iProto_le_refl. *)
- (* - intros p' ?. rewrite (fixpoint_unfold p2). by apply IH. *)
- (* - apply bi.limit_preserving_entails; [done|solve_proper]. *)
- (* Qed. *)
-
- (* 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 : 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 : *)
- (* p1 ⊑ p2 -∗ p3 ⊑ p4 -∗ p1 <++> p3 ⊑ p2 <++> p4. *)
- (* Proof. *)
- (* iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4). *)
- (* destruct (iProto_case p2) as [->|([]&m2&->)]. *)
- (* - iDestruct (iProto_le_end_inv_l 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]". *)
- (* iDestruct ("H1" with "Hm2") as (p1') "[H1 Hm1]". *)
- (* 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"). *)
- (* iDestruct "H1" as (pt) "[H1 H1']". *)
- (* iExists (pt <++> p3). iSplitL "H1". *)
- (* * iIntros "!>". iRewrite "Hp13". *)
- (* rewrite /= -iMsg_app_base -iProto_app_message. *)
- (* iApply ("IH" with "H1"). iApply iProto_le_refl. *)
- (* * iIntros "!>". iRewrite "Hp24". *)
- (* rewrite /= -iMsg_app_base -iProto_app_message. *)
- (* iApply ("IH" with "H1' H2"). *)
- (* - 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]". *)
- (* iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]". *)
- (* iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto]. *)
- (* iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1"). *)
- (* Qed. *)
+ iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
+ destruct (iProto_case p3) as [->|([]&m3&->)].
+ - iDestruct (iProto_le_end_inv_l 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 m1) "[Hp1 H1]".
+ iRewrite "Hp1"; clear p1. destruct a1.
+ * iApply iProto_le_send. iIntros (v p3') "Hm3".
+ iDestruct ("H2" with "Hm3") as (p2') "[Hle Hm2]".
+ iDestruct ("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".
+ iDestruct ("H2" with "Hm3") as (p2') "[Hle Hm2]".
+ iDestruct ("H1" with "Hm1 Hm2") as (pt) "[Hp1' Hp2']".
+ iExists pt. iIntros "{$Hp1'} !>". 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".
+ iDestruct ("H1" with "Hm1") as (p2') "[Hle Hm2]".
+ iDestruct ("H2" with "Hm2 Hm3") as (pt) "[Hp2' Hp3']".
+ iExists pt. iIntros "{$Hp3'} !>". 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 (m1) "[Hp1 H2]".
+ iRewrite "Hp1". iApply iProto_le_recv. iIntros (v p1') "Hm1".
+ iDestruct ("H2" with "Hm1") as (p2') "[Hle Hm2]".
+ iDestruct ("H3" with "Hm2") as (p3') "[Hle' Hm3]".
+ iExists p3'. iIntros "{$Hm3} !>". by iApply ("IH" with "Hle").
+ Qed.
+
+ 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.
+ 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_exist_elim_l {A} (m1 : A → iMsg Σ V) a m2 :
+ (∀ x, (<?> m1 x) ⊑ (<a> m2)) ⊢
+ (<? x> m1 x) ⊑ (<a> m2).
+ Proof.
+ 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_l_inhabited `{!Inhabited A} (m : A → iMsg Σ V) p :
+ (∀ x, (<?> m x) ⊑ p) ⊢
+ (<? x> m x) ⊑ p.
+ Proof.
+ rewrite iMsg_exist_eq. iIntros "H".
+ destruct (iProto_case p) as [Heq | [a [m' Heq]]].
+ - unshelve iSpecialize ("H" $!inhabitant); first by apply _.
+ rewrite Heq.
+ iDestruct (iProto_le_end_inv_l with "H") as "H".
+ rewrite iProto_end_eq iProto_message_eq.
+ iDestruct (proto_message_end_equivI with "H") as "[]".
+ - iEval (rewrite Heq). destruct a.
+ + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1 Hm2 /=".
+ iDestruct "Hm1" as (x) "Hm1".
+ iSpecialize ("H" $! x). rewrite Heq.
+ iApply (iProto_le_recv_send_inv with "H Hm1 Hm2").
+ + iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
+ iSpecialize ("H" $! x). rewrite Heq.
+ 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_elim_r_inhabited `{Hinh : Inhabited A} p (m : A → iMsg Σ V) :
+ (∀ x, p ⊑ (<!> m x)) ⊢
+ p ⊑ (<! x> m x).
+ Proof.
+ rewrite iMsg_exist_eq. iIntros "H".
+ destruct (iProto_case p) as [Heq | [a [m' Heq]]].
+ - unshelve iSpecialize ("H" $!inhabitant); first by apply _.
+ rewrite Heq.
+ iDestruct (iProto_le_end_inv_r with "H") as "H".
+ rewrite iProto_end_eq iProto_message_eq.
+ iDestruct (proto_message_end_equivI with "H") as "[]".
+ - iEval (rewrite Heq). destruct a.
+ + iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
+ iSpecialize ("H" $! x). rewrite Heq.
+ by iApply (iProto_le_send_send_inv with "H").
+ + iApply iProto_le_swap. iIntros (v1 v2 p1' p2') "/= Hm1".
+ iDestruct 1 as (x) "Hm2".
+ iSpecialize ("H" $! x). rewrite Heq.
+ 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_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.
+ induction x as [|T TT x xs IH] using tele_arg_ind; 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] using tele_arg_ind; simpl.
+ { iApply iProto_le_refl. }
+ iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH.
+ Qed.
+
+ Lemma iProto_le_base a v P p1 p2 :
+ ▷ (p1 ⊑ p2) ⊢
+ (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
+ Proof.
+ 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 {1 3}iMsg_base_eq. iApply iProto_le_swap.
+ iIntros (v1' v2' p1' p2') "/= (->&#Hp1&HP1) (->&#Hp2&HP2)". iExists p.
+ iSplitL "HP2".
+ - iIntros "!>". iRewrite -"Hp1". by iApply iProto_le_payload_intro_l.
+ - iIntros "!>". iRewrite -"Hp2". by iApply iProto_le_payload_intro_r.
+ Qed.
+
+ 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 (iProto_case p1) as [->|([]&m1&->)].
+ - iDestruct (iProto_le_end_inv_l 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]".
+ iDestruct ("H" with "Hm1") as (p2') "[H Hm2]".
+ iDestruct ("IH" with "H") as "H". iExists (iProto_dual p2').
+ iSplitL "H"; [iIntros "!>"; by iRewrite "Hp1d"|]. simpl; auto.
+ + iApply iProto_le_swap. iIntros (v1 v2 p1d p2d).
+ iDestruct 1 as (p1') "[Hm1 #Hp1d]". iDestruct 1 as (p2') "[Hm2 #Hp2d]".
+ iDestruct ("H" with "Hm2 Hm1") as (pt) "[H1 H2]".
+ iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
+ rewrite !iProto_dual_message /=. iExists (iProto_dual pt). iSplitL "H2".
+ * iIntros "!>". iRewrite "Hp1d". by rewrite -iMsg_dual_base.
+ * iIntros "!>". iRewrite "Hp2d". by rewrite -iMsg_dual_base.
+ - 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]".
+ iDestruct ("H" with "Hm2") as (p1') "[H Hm1]".
+ iDestruct ("IH" with "H") as "H". iExists (iProto_dual p1').
+ iSplitL "H"; [iIntros "!>"; by iRewrite "Hp2d"|]. simpl; auto.
+ Qed.
+
+ Lemma iProto_le_amber_internal (p1 p2 : iProto Σ V → iProto Σ V)
+ `{Contractive p1, Contractive p2}:
+ □ (∀ rec1 rec2, ▷ (rec1 ⊑ rec2) → p1 rec1 ⊑ p2 rec2) ⊢
+ fixpoint p1 ⊑ fixpoint p2.
+ Proof.
+ iIntros "#H". iLöb as "IH".
+ iEval (rewrite (fixpoint_unfold p1)).
+ iEval (rewrite (fixpoint_unfold p2)).
+ iApply "H". iApply "IH".
+ Qed.
+ Lemma iProto_le_amber_external (p1 p2 : iProto Σ V → iProto Σ V)
+ `{Contractive p1, Contractive p2}:
+ (∀ rec1 rec2, (⊢ rec1 ⊑ rec2) → ⊢ p1 rec1 ⊑ p2 rec2) →
+ ⊢ fixpoint p1 ⊑ fixpoint p2.
+ Proof.
+ intros IH. apply fixpoint_ind.
+ - by intros p1' p2' -> ?.
+ - exists (fixpoint p2). iApply iProto_le_refl.
+ - intros p' ?. rewrite (fixpoint_unfold p2). by apply IH.
+ - apply bi.limit_preserving_entails; [done|solve_proper].
+ Qed.
+
+ 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 : 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 :
+ p1 ⊑ p2 -∗ p3 ⊑ p4 -∗ p1 <++> p3 ⊑ p2 <++> p4.
+ Proof.
+ iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4).
+ destruct (iProto_case p2) as [->|([]&m2&->)].
+ - iDestruct (iProto_le_end_inv_l 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]".
+ iDestruct ("H1" with "Hm2") as (p1') "[H1 Hm1]".
+ 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").
+ iDestruct "H1" as (pt) "[H1 H1']".
+ iExists (pt <++> p3). iSplitL "H1".
+ * iIntros "!>". iRewrite "Hp13".
+ rewrite /= -iMsg_app_base -iProto_app_message.
+ iApply ("IH" with "H1"). iApply iProto_le_refl.
+ * iIntros "!>". iRewrite "Hp24".
+ rewrite /= -iMsg_app_base -iProto_app_message.
+ iApply ("IH" with "H1' H2").
+ - 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]".
+ iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]".
+ iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto].
+ iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1").
+ Qed.
(** ** Lemmas about the auxiliary definitions and invariants *)
Global Instance iProto_app_recvs_ne vs :
@@ -1150,6 +1019,12 @@ Section proto.
Global Instance iProto_app_recvs_proper vs :
Proper ((≡) ==> (≡)) (iProto_app_recvs (Σ:=Σ) (V:=V) vs).
Proof. induction vs; solve_proper. Qed.
+ Global Instance iProto_interp_ne vsl vsr :
+ NonExpansive2 (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
+ Proof. solve_proper. Qed.
+ Global Instance iProto_interp_proper vsl vsr :
+ Proper ((≡) ==> (≡) ==> (≡)) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
+ Proof. apply (ne_proper_2 _). Qed.
Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
Proof. solve_proper. Qed.
@@ -1157,8 +1032,8 @@ Section proto.
Lemma iProto_own_auth_agree γ s p p' :
iProto_own_auth γ s p -∗ iProto_own_frag γ s p' -∗ ▷ (p ≡ p').
Proof.
- iIntros "H◠H◯". iDestruct (own_valid_2 with "H◠H◯") as "H✓".
- iDestruct (excl_auth_agreeI with "H✓") as "H✓".
+ iIntros "H◠H◯". iCombine "H◠H◯" gives "H✓".
+ iDestruct (excl_auth_agreeI with "H✓") as "{H✓} H✓".
iApply (later_equivI_1 with "H✓").
Qed.
@@ -1171,6 +1046,67 @@ Section proto.
by rewrite own_op.
Qed.
+ Lemma iProto_interp_nil p : ⊢ iProto_interp [] [] p (iProto_dual p).
+ Proof. iExists p; simpl. iSplitL; iApply iProto_le_refl. Qed.
+
+ Lemma iProto_interp_flip vsl vsr pl pr :
+ iProto_interp vsl vsr pl pr -∗ iProto_interp vsr vsl pr pl.
+ Proof.
+ iDestruct 1 as (p) "[Hp Hdp]". iExists (iProto_dual p).
+ rewrite (involutive iProto_dual). iFrame.
+ Qed.
+
+ Lemma iProto_interp_le_l vsl vsr pl pl' pr :
+ iProto_interp vsl vsr pl pr -∗ pl ⊑ pl' -∗ iProto_interp vsl vsr pl' pr.
+ Proof.
+ iDestruct 1 as (p) "[Hp Hdp]". iIntros "Hle". iExists p.
+ iFrame "Hdp". by iApply (iProto_le_trans with "Hp").
+ Qed.
+ Lemma iProto_interp_le_r vsl vsr pl pr 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 ml vsl vsr pr pl' :
+ iProto_interp vsl vsr (<!> ml) pr -∗
+ iMsg_car ml vl (Next pl') -∗
+ â–·^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
+ Proof.
+ iDestruct 1 as (p) "[Hp Hdp] /="; iIntros "Hml".
+ iDestruct (iProto_le_trans _ _ (<!> MSG vl; pl') with "Hp [Hml]") as "Hp".
+ { iApply iProto_le_send. rewrite iMsg_base_eq. iIntros (v' p') "(->&Hp&_) /=".
+ iExists p'. iSplitR; [iApply iProto_le_refl|]. by iRewrite -"Hp". }
+ iInduction vsr as [|vr vsr] "IH" forall (pl'); simpl.
+ { iExists pl'; simpl. iSplitR; [iApply iProto_le_refl|].
+ iApply (iProto_le_trans with "[Hp] Hdp").
+ iInduction vsl as [|vl' vsl] "IH"; simpl.
+ { iApply iProto_le_dual_r. rewrite iProto_dual_message iMsg_dual_base /=.
+ by rewrite involutive. }
+ iApply iProto_le_base; iIntros "!>". by iApply "IH". }
+ iDestruct (iProto_le_recv_send_inv _ _ vr vl
+ (iProto_app_recvs vsr p) pl' with "Hp [] []") as (p') "[H1 H2]";
+ [rewrite iMsg_base_eq; by auto..|].
+ iIntros "!>". iSpecialize ("IH" with "Hdp H1"). iIntros "!>".
+ iDestruct "IH" as (p'') "[Hp'' Hdp'']". iExists p''. iFrame "Hdp''".
+ iApply (iProto_le_trans with "[Hp''] H2"); simpl. by iApply iProto_le_base.
+ Qed.
+
+ Lemma iProto_interp_recv vl vsl vsr pl mr :
+ iProto_interp (vl :: vsl) vsr pl (<?> mr) -∗
+ ∃ pr, iMsg_car mr vl (Next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
+ Proof.
+ iDestruct 1 as (p) "[Hp Hdp] /=".
+ iDestruct (iProto_le_recv_inv with "Hdp") as (m) "[#Hm Hpr]".
+ iDestruct (iProto_message_equivI with "Hm") as (_) "{Hm} #Hm".
+ iDestruct ("Hpr" $! vl (iProto_app_recvs vsl (iProto_dual p)) with "[]")
+ as (pr'') "[Hler Hpr]".
+ { iRewrite -("Hm" $! vl (Next (iProto_app_recvs vsl (iProto_dual p)))).
+ rewrite iMsg_base_eq; auto. }
+ iExists pr''. iIntros "{$Hpr} !>". iExists p. iFrame.
+ Qed.
+
Global Instance iProto_own_ne γ s : NonExpansive (iProto_own γ s).
Proof. solve_proper. Qed.
Global Instance iProto_own_proper γ s : Proper ((≡) ==> (≡)) (iProto_own γ s).
@@ -1185,7 +1121,8 @@ Section proto.
Lemma iProto_init p :
⊢ |==> ∃ γ,
- iProto_ctx γ ∗ iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
+ iProto_ctx γ [] [] ∗
+ iProto_own γ Left p ∗ iProto_own γ Right (iProto_dual p).
Proof.
iMod (own_alloc (â—E (Next p) â‹… â—¯E (Next p))) as (lγ) "[Hâ—l Hâ—¯l]".
{ by apply excl_auth_valid. }
@@ -1193,154 +1130,166 @@ Section proto.
â—¯E (Next (iProto_dual p)))) as (rγ) "[Hâ—r Hâ—¯r]".
{ by apply excl_auth_valid. }
pose (ProtName lγ rγ) as γ. iModIntro. iExists γ. iSplitL "Hâ—l Hâ—r".
- { iExists p, (iProto_dual p). iFrame. iApply iProto_consistent_dual. }
+ { iExists p, (iProto_dual p). iFrame. iApply iProto_interp_nil. }
iSplitL "Hâ—¯l"; iExists _; iFrame; iApply iProto_le_refl.
Qed.
- Definition side_dual s :=
- match s with
- | Left => Right
- | Right => Left
- end.
-
- Lemma iProto_step_l γ m1 m2 p1 v :
- iProto_ctx γ -∗ iProto_own γ Left (<!> m1) -∗ iProto_own γ Right (<?> m2) -∗
- iMsg_car m1 v (Next p1) ==∗
- ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ iProto_ctx γ ∗
- iProto_own γ Left p1 ∗ iProto_own γ Right p2.
- Proof.
- iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hconsistent)".
- iDestruct 1 as (pl') "[Hlel Hâ—¯l]".
- iDestruct 1 as (pr') "[Hler Hâ—¯r]".
- iIntros "Hm".
- iDestruct (iProto_own_auth_agree with "Hâ—l Hâ—¯l") as "#Hpl".
- iDestruct (iProto_own_auth_agree with "Hâ—r Hâ—¯r") as "#Hpr".
- iAssert (▷ (pl ⊑ <!> m1))%I
- with "[Hlel]" as "{Hpl} Hlel"; first (iNext; by iRewrite "Hpl").
- iAssert (▷ (pr ⊑ <?> m2))%I
- with "[Hler]" as "{Hpr} Hler"; first (iNext; by iRewrite "Hpr").
- iDestruct (iProto_consistent_le_l with "Hconsistent Hlel") as "Hconsistent".
- iDestruct (iProto_consistent_le_r with "Hconsistent Hler") as "Hconsistent".
- iDestruct (iProto_consistent_step with "Hconsistent [Hm //]") as
- (p2) "[Hm2 Hconsistent]".
- iMod (iProto_own_auth_update _ _ _ _ p1 with "Hâ—l Hâ—¯l") as "[Hâ—l Hâ—¯l]".
- iMod (iProto_own_auth_update _ _ _ _ p2 with "Hâ—r Hâ—¯r") as "[Hâ—r Hâ—¯r]".
- iIntros "!>!>".
- iExists p2. iFrame.
- iSplitL "Hconsistent Hâ—l Hâ—r".
- - iExists _, _. iFrame.
- - iSplitL "Hâ—¯l".
- + iExists _. iFrame. iApply iProto_le_refl.
- + iExists _. iFrame. iApply iProto_le_refl.
- Qed.
-
- Lemma iProto_step_r γ m1 m2 p2 v :
- iProto_ctx γ -∗ iProto_own γ Left (<?> m1) -∗ iProto_own γ Right (<!> m2) -∗
- iMsg_car m2 v (Next p2) ==∗
- ▷ ∃ p1, iMsg_car m1 v (Next p1) ∗ iProto_ctx γ ∗
- iProto_own γ Left p1 ∗ iProto_own γ Right p2.
- Proof.
- iDestruct 1 as (pl pr) "(Hâ—l & Hâ—r & Hconsistent)".
- iDestruct 1 as (pl') "[Hlel Hâ—¯l]".
- iDestruct 1 as (pr') "[Hler Hâ—¯r]".
- iIntros "Hm".
- iDestruct (iProto_own_auth_agree with "Hâ—l Hâ—¯l") as "#Hpl".
- iDestruct (iProto_own_auth_agree with "Hâ—r Hâ—¯r") as "#Hpr".
- iAssert (▷ (pl ⊑ <?> m1))%I
- with "[Hlel]" as "{Hpl} Hlel"; first (iNext; by iRewrite "Hpl").
- iAssert (▷ (pr ⊑ <!> m2))%I
- with "[Hler]" as "{Hpr} Hler"; first (iNext; by iRewrite "Hpr").
- iDestruct (iProto_consistent_le_l with "Hconsistent Hlel") as "Hconsistent".
- iDestruct (iProto_consistent_le_r with "Hconsistent Hler") as "Hconsistent".
- iDestruct (iProto_consistent_flip with "Hconsistent") as
- "Hconsistent".
- iDestruct (iProto_consistent_step with "Hconsistent [Hm //]") as
- (p1) "[Hm1 Hconsistent]".
- iMod (iProto_own_auth_update _ _ _ _ p1 with "Hâ—l Hâ—¯l") as "[Hâ—l Hâ—¯l]".
- iMod (iProto_own_auth_update _ _ _ _ p2 with "Hâ—r Hâ—¯r") as "[Hâ—r Hâ—¯r]".
- iIntros "!>!>".
- iExists p1. iFrame.
- iSplitL "Hconsistent Hâ—l Hâ—r".
- - iExists _, _. iFrame. iApply iProto_consistent_flip. iFrame.
- - iSplitL "Hâ—¯l".
- + iExists _. iFrame. iApply iProto_le_refl.
- + iExists _. iFrame. 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 name : *)
- (* AsIdentName m1 name → *)
- (* FromForall (iProto_message Recv (iMsg_exist m1) ⊑ (<a> m2)) *)
- (* (λ x, (<?> m1 x) ⊑ (<a> m2))%I name | 10. *)
- (* Proof. intros _. apply iProto_le_exist_elim_l. Qed. *)
- (* Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A → iMsg Σ V) name : *)
- (* AsIdentName m2 name → *)
- (* FromForall ((<a> m1) ⊑ iProto_message Send (iMsg_exist m2)) *)
- (* (λ x, (<a> m1) ⊑ (<!> m2 x))%I name | 11. *)
- (* Proof. intros _. 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 True (modality_instances.modality_laterN 1) (p1 ⊑ p2) *)
- (* ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2). *)
- (* Proof. intros _. apply iProto_le_base. Qed. *)
+ Lemma iProto_send_l γ m vsr vsl vl p :
+ iProto_ctx γ vsl vsr -∗
+ iProto_own γ Left (<!> m) -∗
+ iMsg_car m vl (Next p) ==∗
+ ▷^(length vsr) iProto_ctx γ (vsl ++ [vl]) vsr ∗
+ iProto_own γ Left p.
+ Proof.
+ 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 (▷ (pl ⊑ <!> m))%I
+ with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
+ iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
+ iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
+ iMod (iProto_own_auth_update _ _ _ _ p with "Hâ—l Hâ—¯") as "[Hâ—l Hâ—¯]".
+ iIntros "!>". iSplitR "Hâ—¯".
+ - iIntros "!>". iExists p, pr. iFrame.
+ - iExists p. iFrame. iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_send_r γ m vsr vsl vr p :
+ iProto_ctx γ vsl vsr -∗
+ iProto_own γ Right (<!> m) -∗
+ iMsg_car m vr (Next p) ==∗
+ ▷^(length vsl) iProto_ctx γ vsl (vsr ++ [vr]) ∗
+ iProto_own γ Right p.
+ Proof.
+ 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 (▷ (pr ⊑ <!> m))%I
+ with "[Hle]" as "{Hp} Hle"; first (iNext; by iRewrite "Hp").
+ iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
+ iDestruct (iProto_interp_le_l with "Hinterp Hle") as "Hinterp".
+ iDestruct (iProto_interp_send with "Hinterp [Hm //]") as "Hinterp".
+ iMod (iProto_own_auth_update _ _ _ _ p with "Hâ—r Hâ—¯") as "[Hâ—r Hâ—¯]".
+ iIntros "!>". iSplitR "Hâ—¯".
+ - iIntros "!>". iExists pl, p. iFrame. by iApply iProto_interp_flip.
+ - iExists p. iFrame. iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_recv_l γ m vr vsr vsl :
+ iProto_ctx γ vsl (vr :: vsr) -∗
+ iProto_own γ Left (<?> m) ==∗
+ ▷ ∃ p,
+ iProto_ctx γ vsl vsr ∗
+ iProto_own γ Left p ∗
+ iMsg_car m vr (Next p).
+ Proof.
+ 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_le_l with "Hinterp [Hle]") as "Hinterp".
+ { iIntros "!>". by iRewrite "Hp". }
+ iDestruct (iProto_interp_flip with "Hinterp") as "Hinterp".
+ iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
+ iMod (iProto_own_auth_update _ _ _ _ q with "Hâ—l Hâ—¯") as "[Hâ—l Hâ—¯]".
+ iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "Hâ—¯".
+ - iExists q, pr. iFrame. by iApply iProto_interp_flip.
+ - iExists q. iIntros "{$Hâ—¯} !>". iApply iProto_le_refl.
+ Qed.
+
+ Lemma iProto_recv_r γ m vl vsr vsl :
+ iProto_ctx γ (vl :: vsl) vsr -∗
+ iProto_own γ Right (<?> m) ==∗
+ ▷ ∃ p,
+ iProto_ctx γ vsl vsr ∗
+ iProto_own γ Right p ∗
+ iMsg_car m vl (Next p).
+ Proof.
+ 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_le_r with "Hinterp [Hle]") as "Hinterp".
+ { iIntros "!>". by iRewrite "Hp". }
+ iDestruct (iProto_interp_recv with "Hinterp") as (q) "[Hm Hinterp]".
+ iMod (iProto_own_auth_update _ _ _ _ q with "Hâ—r Hâ—¯") as "[Hâ—r Hâ—¯]".
+ iIntros "!> !> /=". iExists q. iFrame "Hm". iSplitR "Hâ—¯".
+ - iExists pl, q. iFrame.
+ - 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 name :
+ AsIdentName m1 name →
+ FromForall (iProto_message Recv (iMsg_exist m1) ⊑ (<a> m2))
+ (λ x, (<?> m1 x) ⊑ (<a> m2))%I name | 10.
+ Proof. intros _. apply iProto_le_exist_elim_l. Qed.
+ Global Instance iProto_le_from_forall_r {A} a m1 (m2 : A → iMsg Σ V) name :
+ AsIdentName m2 name →
+ FromForall ((<a> m1) ⊑ iProto_message Send (iMsg_exist m2))
+ (λ x, (<a> m1) ⊑ (<!> m2 x))%I name | 11.
+ Proof. intros _. 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 True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
+ ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
+ Proof. intros _. apply iProto_le_base. Qed.
End proto.
-Typeclasses Opaque iProto_ctx iProto_own.
+Global Typeclasses Opaque iProto_ctx iProto_own.
Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.