diff --git a/multris/channel/channel.v b/multris/channel/channel.v
index 46083fd3404a9e94628bdfc0f46728904be3c34f..f7880330c1b5775e182e8a0710bae6a55292f1ce 100644
--- a/multris/channel/channel.v
+++ b/multris/channel/channel.v
@@ -91,14 +91,13 @@ Definition chan_inv `{!heapGS Σ, !chanG Σ} γ γE γt i j (l:loc) : iProp Σ :
Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
- ∃ γ (γEs : list gname) (m:val) (i:nat) (n:nat) p',
+ ∃ γ (γEs : list gname) (m:val) (i:nat) (n:nat),
⌜ c = (m,#i)%V ⌠∗
inv (nroot.@"ctx") (iProto_ctx γ n) ∗
is_matrix m n n
(λ i j l, ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j l)) ∗
- ▷ (p' ⊑ p) ∗
- own (γEs !!! i) (â—E (Next p')) ∗ own (γEs !!! i) (â—¯E (Next p')) ∗
- iProto_own γ i p'.
+ own (γEs !!! i) (â—E (Next p)) ∗ own (γEs !!! i) (â—¯E (Next p)) ∗
+ iProto_own γ i p.
Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
Definition iProto_pointsto_eq :
@@ -130,15 +129,6 @@ 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 (?????? ->) "(#IH & Hls & Hle & Hâ— & Hâ—¯ & Hown)".
- iIntros "Hle'". iExists _,_,_,_,_,p'.
- iSplit; [done|]. iFrame "#∗".
- iApply (iProto_le_trans with "Hle Hle'").
- Qed.
-
(** ** Specifications of [send] and [recv] *)
Lemma new_chan_spec (ps:list (iProto Σ)) :
0 < length ps →
@@ -206,9 +196,9 @@ Section channel.
iModIntro.
iApply "HΦ".
iSplitL "Hl".
- { rewrite iProto_pointsto_eq. iExists _, _, _, _, _, _.
+ { rewrite iProto_pointsto_eq. iExists _, _, _, _, _.
iSplit; [done|].
- iFrame. iFrame "#∗". iNext. done. }
+ iFrame. iFrame "#∗". }
iExists γp, γEs, _. iSplit; [done|].
iFrame. iFrame "#∗".
simpl.
@@ -227,14 +217,12 @@ Section channel.
Proof.
rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as
- (γ γE l i n p' ->) "(#IH & #Hls & Hle & H◠& H◯ & Hown)".
+ (γ γE l i n ->) "(#IH & #Hls & H◠& H◯ & Hown)".
wp_bind (Fst _).
iInv "IH" as "Hctx".
- iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
- iRewrite "Heq" in "Hown".
iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
- iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+ wp_pures. iModIntro. iFrame.
wp_pures.
iDestruct "Hi" as %Hi.
iDestruct "Hj" as %Hj.
@@ -255,10 +243,8 @@ Section channel.
wp_store.
iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]"; [by apply excl_auth_update|].
iModIntro.
- iSplitL "Hl' Hâ— Hown Hle".
- { iRight. iLeft. iIntros "!>". iExists _, _. iFrame.
- iDestruct (iProto_own_le with "Hown Hle") as "Hown".
- by rewrite iMsg_base_eq. }
+ iSplitL "Hl' Hâ— Hown".
+ { iRight. iLeft. iIntros "!>". iExists _, _. iFrame. }
wp_pures.
iLöb as "HL".
wp_lam.
@@ -285,24 +271,17 @@ Section channel.
{ apply excl_auth_update. }
iModIntro.
iApply "HΦ".
- iExists _, _, _, _, _, _.
+ iExists _, _, _, _, _.
iSplit; [done|]. iFrame "#∗".
- iRewrite -"Hagree'". iApply iProto_le_refl.
+ iRewrite -"Hagree'". done.
Qed.
- Lemma send_spec_tele {TT} c i (tt : TT)
+ Lemma send_spec_tele {TT} c j (tt : TT)
(v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
- {{{ c ↣ (<(Send,i) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
- send c #i (v tt)
+ {{{ c ↣ (<(Send,j) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+ send c #j (v tt)
{{{ RET #(); c ↣ (p tt) }}}.
- Proof.
- iIntros (Φ) "[Hc HP] HΦ".
- iDestruct (iProto_pointsto_le _ _ (<(Send,i)> MSG v tt; p tt)%proto
- with "Hc [HP]") as "Hc".
- { iIntros "!>". iApply iProto_le_trans. iApply iProto_le_texist_intro_l.
- by iApply iProto_le_payload_intro_l. }
- by iApply (send_spec with "Hc").
- Qed.
+ Proof. Admitted.
Lemma recv_spec {TT} c j (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
{{{ c ↣ <(Recv, j) @.. x> MSG v x {{ ▷ P x }}; p x }}}
@@ -312,15 +291,13 @@ Section channel.
iIntros (Φ) "Hc HΦ". iLöb as "HL". wp_lam.
rewrite iProto_pointsto_eq.
iDestruct "Hc" as
- (γ γE l i n p' ->) "(#IH & #Hls & Hle & H◠& H◯ & Hown)".
+ (γ γE l i n ->) "(#IH & #Hls & H◠& H◯ & Hown)".
do 5 wp_pure _.
wp_bind (Snd _).
iInv "IH" as "Hctx".
- iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
- iRewrite "Heq" in "Hown".
iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
- iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+ wp_pures. iModIntro. iFrame.
wp_pure _.
iDestruct "Hi" as %Hi.
iDestruct "Hj" as %Hj.
@@ -335,20 +312,19 @@ Section channel.
wp_xchg. iModIntro.
iSplitL "Hl' Htok".
{ iLeft. iFrame. }
- wp_pures. iApply ("HL" with "[H◠H◯ Hown Hle] HΦ").
- iExists _, _, _, _, _, _. iSplit; [done|]. 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 Hle] HΦ").
- iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+ wp_pures. iApply ("HL" with "[H◠H◯ Hown] HΦ").
+ iExists _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
iDestruct "HIp" as (w p'') "(>Hl' & Hown' & Hp')".
iInv "IH" as "Hctx".
wp_xchg.
- iDestruct (iProto_own_le with "Hown Hle") as "Hown".
iMod (iProto_step with "Hctx Hown' Hown []") as
(p''') "(Hm & Hctx & Hown & Hown')".
{ by rewrite iMsg_base_eq. }
@@ -364,7 +340,7 @@ Section channel.
iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]";
[apply (excl_auth_update _ _ (Next p'''))|].
iModIntro. iApply "HΦ". rewrite /iProto_pointsto_def. iFrame "IH Hls ∗".
- iSplit; [done|]. iRewrite "Hp". iApply iProto_le_refl.
+ iExists _. iSplit; [done|]. iRewrite "Hp". iFrame.
Qed.
End channel.
diff --git a/multris/channel/proto.v b/multris/channel/proto.v
index 56522bb410f4f5ac41da6c02117cdeccd9c6b5f4..950d5f43e8bb68f3bd8e5726d39dc10a997965c2 100644
--- a/multris/channel/proto.v
+++ b/multris/channel/proto.v
@@ -140,51 +140,51 @@ Program Definition iMsg_map {Σ V}
IMsg (λ v, λne p1', ∃ p1, iMsg_car m v (Next p1) ∗ p1' ≡ Next (rec p1))%I.
Next Obligation. solve_proper. Qed.
-Program Definition iProto_map_app_aux {Σ V}
- (f : action → action) (p2 : iProto Σ V)
- (rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p,
- proto_elim p2 (λ a m,
- proto_message (f a) (iMsg_car (iMsg_map rec (IMsg m)))) p.
-Next Obligation.
- intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a m1 m2 Hm.
- apply proto_message_ne=> v p' /=. by repeat f_equiv.
-Qed.
-
-Global Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
- Contractive (iProto_map_app_aux f p2).
-Proof.
- intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a m1 m2 Hm.
- apply proto_message_ne=> v p' /=. by repeat (f_contractive || f_equiv).
-Qed.
-
-Definition iProto_map_app {Σ V} (f : action → action)
- (p2 : iProto Σ V) : iProto Σ V -n> iProto Σ V :=
- fixpoint (iProto_map_app_aux f p2).
-
-Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
- iProto_map_app id p2 p1.
-Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
-Definition iProto_app := iProto_app_aux.(unseal).
-Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
-Arguments iProto_app {_ _} _%_proto _%_proto.
-Global Instance: Params (@iProto_app) 2 := {}.
-Infix "<++>" := iProto_app (at level 60) : proto_scope.
-Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
-
-Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V :=
- iProto_map_app action_dual proto_end p.
-Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
-Definition iProto_dual := iProto_dual_aux.(unseal).
-Definition iProto_dual_eq :
- @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
-Arguments iProto_dual {_ _} _%_proto.
-Global Instance: Params (@iProto_dual) 2 := {}.
-Notation iMsg_dual := (iMsg_map iProto_dual).
-
-Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
- if d then iProto_dual p else p.
-Arguments iProto_dual_if {_ _} _ _%_proto.
-Global Instance: Params (@iProto_dual_if) 3 := {}.
+(* Program Definition iProto_map_app_aux {Σ V} *)
+(* (f : action → action) (p2 : iProto Σ V) *)
+(* (rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p, *)
+(* proto_elim p2 (λ a m, *)
+(* proto_message (f a) (iMsg_car (iMsg_map rec (IMsg m)))) p. *)
+(* Next Obligation. *)
+(* intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a m1 m2 Hm. *)
+(* apply proto_message_ne=> v p' /=. by repeat f_equiv. *)
+(* Qed. *)
+
+(* Global Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) : *)
+(* Contractive (iProto_map_app_aux f p2). *)
+(* Proof. *)
+(* intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a m1 m2 Hm. *)
+(* apply proto_message_ne=> v p' /=. by repeat (f_contractive || f_equiv). *)
+(* Qed. *)
+
+(* Definition iProto_map_app {Σ V} (f : action → action) *)
+(* (p2 : iProto Σ V) : iProto Σ V -n> iProto Σ V := *)
+(* fixpoint (iProto_map_app_aux f p2). *)
+
+(* Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V := *)
+(* iProto_map_app id p2 p1. *)
+(* Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed. *)
+(* Definition iProto_app := iProto_app_aux.(unseal). *)
+(* Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq). *)
+(* Arguments iProto_app {_ _} _%_proto _%_proto. *)
+(* Global Instance: Params (@iProto_app) 2 := {}. *)
+(* Infix "<++>" := iProto_app (at level 60) : proto_scope. *)
+(* Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope. *)
+
+(* Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V := *)
+(* iProto_map_app action_dual proto_end p. *)
+(* Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed. *)
+(* Definition iProto_dual := iProto_dual_aux.(unseal). *)
+(* Definition iProto_dual_eq : *)
+(* @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq). *)
+(* Arguments iProto_dual {_ _} _%_proto. *)
+(* Global Instance: Params (@iProto_dual) 2 := {}. *)
+(* Notation iMsg_dual := (iMsg_map iProto_dual). *)
+
+(* Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V := *)
+(* if d then iProto_dual p else p. *)
+(* Arguments iProto_dual_if {_ _} _ _%_proto. *)
+(* Global Instance: Params (@iProto_dual_if) 3 := {}. *)
(** * Proofs *)
Section proto.
@@ -194,22 +194,22 @@ Section proto.
Implicit Types m : iMsg Σ V.
(** ** Equality *)
- Lemma iProto_case p : p ≡ END ∨ ∃ t n m, p ≡ <(t,n)> m.
- Proof.
- rewrite iProto_message_eq iProto_end_eq.
- destruct (proto_case p) as [|([a n]&m&?)]; [by left|right].
- by exists a, n, (IMsg m).
- Qed.
- Lemma iProto_message_equivI `{!BiInternalEq SPROP} a1 a2 m1 m2 :
- (<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧
+ (* Lemma iProto_case p : p ≡ END ∨ ∃ t n m, p ≡ <(t,n)> m. *)
+ (* Proof. *)
+ (* rewrite iProto_message_eq iProto_end_eq. *)
+ (* destruct (proto_case p) as [|([a n]&m&?)]; [by left|right]. *)
+ (* by exists a, n, (IMsg m). *)
+ (* Qed. *)
+ Lemma iProto_message_equivI a1 a2 m1 m2 :
+ (<a1> m1) ≡ (<a2> m2) ⊣⊢@{iProp Σ} ⌜ a1 = a2 ⌠∧
(∀ v lp, iMsg_car m1 v lp ≡ iMsg_car m2 v lp).
Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
- Lemma iProto_message_end_equivI `{!BiInternalEq SPROP} a m :
- (<a> m) ≡ END ⊢@{SPROP} False.
+ Lemma iProto_message_end_equivI a m :
+ (<a> m) ≡ END ⊢@{iProp Σ} False.
Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.
- Lemma iProto_end_message_equivI `{!BiInternalEq SPROP} a m :
- END ≡ (<a> m) ⊢@{SPROP} False.
+ Lemma iProto_end_message_equivI a m :
+ END ≡ (<a> m) ⊢@{iProp Σ} False.
Proof. by rewrite internal_eq_sym iProto_message_end_equivI. Qed.
(** ** Non-expansiveness of operators *)
@@ -316,137 +316,137 @@ Section proto.
Qed.
(** ** Dual *)
- Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
- Proof. rewrite iProto_dual_eq. solve_proper. Qed.
- Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ V).
- Proof. apply (ne_proper _). Qed.
- Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
- Proof. solve_proper. Qed.
- Global Instance iProto_dual_if_proper d :
- Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
- Proof. apply (ne_proper _). Qed.
-
- Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END.
- Proof.
- rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- by rewrite proto_elim_end.
- Qed.
- Lemma iProto_dual_message a m :
- iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m.
- Proof.
- rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
- intros a' m1 m2 Hm; f_equiv; solve_proper.
- Qed.
- Lemma iMsg_dual_base v P p :
- iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
- Proof. apply iMsg_map_base, _. Qed.
- Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) :
- iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg.
- Proof. apply iMsg_map_exist. Qed.
-
- Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
- Proof.
- intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&n&m&->)].
- { by rewrite !iProto_dual_end. }
- rewrite !iProto_dual_message involutive.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
- iApply prop_ext; iIntros "!>"; iSplit.
- - iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
- iDestruct "H" as (pdd) "[H #Hpd]".
- iApply (internal_eq_rewrite); [|done]; iIntros "!>".
- iRewrite "Hpd". by iRewrite ("IH" $! pdd).
- - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists _.
- rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
- Qed.
-
- (** ** Append *)
- Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V).
- Proof.
- intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- by rewrite proto_elim_end.
- Qed.
- Lemma iProto_app_message a m p2 : (<a> m) <++> p2 ≡ <a> m <++> p2.
- Proof.
- rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
- intros a' m1 m2 Hm. f_equiv; solve_proper.
- Qed.
-
- Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
- Proof.
- assert (∀ n, Proper (dist n ==> (=) ==> dist n) (@iProto_app Σ V)).
- { intros n p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
- assert (Proper ((≡) ==> (=) ==> (≡)) (@iProto_app Σ V)).
- { intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
- intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1.
- revert p1'. induction (lt_wf n) as [n _ IH]; intros p1.
- destruct (iProto_case p1) as [->|(a&i&m&->)].
- { by rewrite !left_id. }
- rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
- f_contractive. apply IH; eauto using dist_le with lia.
- Qed.
- Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
- Proof. apply (ne_proper_2 _). Qed.
-
- Lemma iMsg_app_base v P p1 p2 :
- ((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg.
- Proof. apply: iMsg_map_base. Qed.
- Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 :
- ((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg.
- Proof. apply iMsg_map_exist. Qed.
-
- Global Instance iProto_app_end_r : RightId (≡) END (@iProto_app Σ V).
- Proof.
- intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&i&m&->)].
- { by rewrite left_id. }
- rewrite iProto_app_message.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
- iApply prop_ext; iIntros "!>". iSplit.
- - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'".
- iApply (internal_eq_rewrite); [|done]; iIntros "!>".
- by iRewrite ("IH" $! p1').
- - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''.
- rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
- Qed.
- Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
- Proof.
- intros p1 p2 p3. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p1). destruct (iProto_case p1) as [->|(a&i&m&->)].
- { by rewrite !left_id. }
- rewrite !iProto_app_message.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
- iApply prop_ext; iIntros "!>". iSplit.
- - iDestruct 1 as (p1') "[H #Hp']".
- iExists (p1' <++> p2). iSplitL; [by auto|].
- iRewrite "Hp'". iIntros "!>". iApply "IH".
- - iDestruct 1 as (p12) "[H #Hp123]". iDestruct "H" as (p1') "[H #Hp12]".
- iExists p1'. iFrame "H". iRewrite "Hp123".
- iIntros "!>". iRewrite "Hp12". by iRewrite ("IH" $! p1').
- Qed.
-
- Lemma iProto_dual_app p1 p2 :
- iProto_dual (p1 <++> p2) ≡ iProto_dual p1 <++> iProto_dual p2.
- Proof.
- apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p1 p2). destruct (iProto_case p1) as [->|(a&i&m&->)].
- { by rewrite iProto_dual_end !left_id. }
- rewrite iProto_dual_message !iProto_app_message iProto_dual_message /=.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=".
- iApply prop_ext; iIntros "!>". iSplit.
- - iDestruct 1 as (p12d) "[H #Hp12]". iDestruct "H" as (p1') "[H #Hp12d]".
- iExists (iProto_dual p1'). iSplitL; [by auto|].
- iRewrite "Hp12". iIntros "!>". iRewrite "Hp12d". iApply "IH".
- - iDestruct 1 as (p1') "[H #Hp12]". iDestruct "H" as (p1d) "[H #Hp1']".
- iExists (p1d <++> p2). iSplitL; [by auto|].
- iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
- Qed.
+ (* Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V). *)
+ (* Proof. rewrite iProto_dual_eq. solve_proper. Qed. *)
+ (* Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ V). *)
+ (* Proof. apply (ne_proper _). Qed. *)
+ (* Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d). *)
+ (* Proof. solve_proper. Qed. *)
+ (* Global Instance iProto_dual_if_proper d : *)
+ (* Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d). *)
+ (* Proof. apply (ne_proper _). Qed. *)
+
+ (* Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END. *)
+ (* Proof. *)
+ (* rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app. *)
+ (* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
+ (* by rewrite proto_elim_end. *)
+ (* Qed. *)
+ (* Lemma iProto_dual_message a m : *)
+ (* iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m. *)
+ (* Proof. *)
+ (* rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app. *)
+ (* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
+ (* rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|]. *)
+ (* intros a' m1 m2 Hm; f_equiv; solve_proper. *)
+ (* Qed. *)
+ (* Lemma iMsg_dual_base v P p : *)
+ (* iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg. *)
+ (* Proof. apply iMsg_map_base, _. Qed. *)
+ (* Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) : *)
+ (* iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg. *)
+ (* Proof. apply iMsg_map_exist. Qed. *)
+
+ (* Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V). *)
+ (* Proof. *)
+ (* intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)). *)
+ (* iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&n&m&->)]. *)
+ (* { by rewrite !iProto_dual_end. } *)
+ (* rewrite !iProto_dual_message involutive. *)
+ (* iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=". *)
+ (* iApply prop_ext; iIntros "!>"; iSplit. *)
+ (* - iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'". *)
+ (* iDestruct "H" as (pdd) "[H #Hpd]". *)
+ (* iApply (internal_eq_rewrite); [|done]; iIntros "!>". *)
+ (* iRewrite "Hpd". by iRewrite ("IH" $! pdd). *)
+ (* - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists _. *)
+ (* rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p''). *)
+ (* Qed. *)
+
+ (* (** ** Append *) *)
+ (* Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V). *)
+ (* Proof. *)
+ (* intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app. *)
+ (* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
+ (* by rewrite proto_elim_end. *)
+ (* Qed. *)
+ (* Lemma iProto_app_message a m p2 : (<a> m) <++> p2 ≡ <a> m <++> p2. *)
+ (* Proof. *)
+ (* rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app. *)
+ (* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl. *)
+ (* rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|]. *)
+ (* intros a' m1 m2 Hm. f_equiv; solve_proper. *)
+ (* Qed. *)
+
+ (* Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V). *)
+ (* Proof. *)
+ (* assert (∀ n, Proper (dist n ==> (=) ==> dist n) (@iProto_app Σ V)). *)
+ (* { intros n p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. } *)
+ (* assert (Proper ((≡) ==> (=) ==> (≡)) (@iProto_app Σ V)). *)
+ (* { intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. } *)
+ (* intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1. *)
+ (* revert p1'. induction (lt_wf n) as [n _ IH]; intros p1. *)
+ (* destruct (iProto_case p1) as [->|(a&i&m&->)]. *)
+ (* { by rewrite !left_id. } *)
+ (* rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv. *)
+ (* f_contractive. apply IH; eauto using dist_le with lia. *)
+ (* Qed. *)
+ (* Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V). *)
+ (* Proof. apply (ne_proper_2 _). Qed. *)
+
+ (* Lemma iMsg_app_base v P p1 p2 : *)
+ (* ((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg. *)
+ (* Proof. apply: iMsg_map_base. Qed. *)
+ (* Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 : *)
+ (* ((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg. *)
+ (* Proof. apply iMsg_map_exist. Qed. *)
+
+ (* Global Instance iProto_app_end_r : RightId (≡) END (@iProto_app Σ V). *)
+ (* Proof. *)
+ (* intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)). *)
+ (* iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&i&m&->)]. *)
+ (* { by rewrite left_id. } *)
+ (* rewrite iProto_app_message. *)
+ (* iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=". *)
+ (* iApply prop_ext; iIntros "!>". iSplit. *)
+ (* - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'". *)
+ (* iApply (internal_eq_rewrite); [|done]; iIntros "!>". *)
+ (* by iRewrite ("IH" $! p1'). *)
+ (* - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''. *)
+ (* rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p''). *)
+ (* Qed. *)
+ (* Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V). *)
+ (* Proof. *)
+ (* intros p1 p2 p3. apply (uPred.internal_eq_soundness (M:=iResUR Σ)). *)
+ (* iLöb as "IH" forall (p1). destruct (iProto_case p1) as [->|(a&i&m&->)]. *)
+ (* { by rewrite !left_id. } *)
+ (* rewrite !iProto_app_message. *)
+ (* iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=". *)
+ (* iApply prop_ext; iIntros "!>". iSplit. *)
+ (* - iDestruct 1 as (p1') "[H #Hp']". *)
+ (* iExists (p1' <++> p2). iSplitL; [by auto|]. *)
+ (* iRewrite "Hp'". iIntros "!>". iApply "IH". *)
+ (* - iDestruct 1 as (p12) "[H #Hp123]". iDestruct "H" as (p1') "[H #Hp12]". *)
+ (* iExists p1'. iFrame "H". iRewrite "Hp123". *)
+ (* iIntros "!>". iRewrite "Hp12". by iRewrite ("IH" $! p1'). *)
+ (* Qed. *)
+
+ (* Lemma iProto_dual_app p1 p2 : *)
+ (* iProto_dual (p1 <++> p2) ≡ iProto_dual p1 <++> iProto_dual p2. *)
+ (* Proof. *)
+ (* apply (uPred.internal_eq_soundness (M:=iResUR Σ)). *)
+ (* iLöb as "IH" forall (p1 p2). destruct (iProto_case p1) as [->|(a&i&m&->)]. *)
+ (* { by rewrite iProto_dual_end !left_id. } *)
+ (* rewrite iProto_dual_message !iProto_app_message iProto_dual_message /=. *)
+ (* iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=". *)
+ (* iApply prop_ext; iIntros "!>". iSplit. *)
+ (* - iDestruct 1 as (p12d) "[H #Hp12]". iDestruct "H" as (p1') "[H #Hp12d]". *)
+ (* iExists (iProto_dual p1'). iSplitL; [by auto|]. *)
+ (* iRewrite "Hp12". iIntros "!>". iRewrite "Hp12d". iApply "IH". *)
+ (* - iDestruct 1 as (p1') "[H #Hp12]". iDestruct "H" as (p1d) "[H #Hp1']". *)
+ (* iExists (p1d <++> p2). iSplitL; [by auto|]. *)
+ (* iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2). *)
+ (* Qed. *)
End proto.
@@ -501,43 +501,43 @@ Proof.
apply: (fixpoint_unfold iProto_consistent_pre').
Qed.
-(** * 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,i), (Recv,j) => ⌜i = j⌠∗ ∀ v p1',
- iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ rec p1' p2' ∗ iMsg_car m2 v (Next p2')
- | (Send,i), (Send,j) => ⌜i = j⌠∗ ∀ v p2',
- iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ rec p1' p2' ∗ iMsg_car m1 v (Next p1')
- | _, _ => 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_le_pre' {Σ V}
- (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
- iProto Σ V -n> iProto Σ V -n> iPropO Σ := λne p1 p2,
- iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
-Solve Obligations with solve_proper.
-Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
-Proof.
- intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
- by repeat (f_contractive || f_equiv).
-Qed.
-Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
- fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_ _} _%_proto _%_proto.
-Global Instance: Params (@iProto_le) 2 := {}.
-Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
-
-Global Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V).
-Proof. solve_proper. Qed.
-Global Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
-Proof. solve_proper. Qed.
+(* (** * 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,i), (Recv,j) => ⌜i = j⌠∗ ∀ v p1', *)
+(* iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ rec p1' p2' ∗ iMsg_car m2 v (Next p2') *)
+(* | (Send,i), (Send,j) => ⌜i = j⌠∗ ∀ v p2', *)
+(* iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ rec p1' p2' ∗ iMsg_car m1 v (Next p1') *)
+(* | _, _ => 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_le_pre' {Σ V} *)
+(* (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) : *)
+(* iProto Σ V -n> iProto Σ V -n> iPropO Σ := λne p1 p2, *)
+(* iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2. *)
+(* Solve Obligations with solve_proper. *)
+(* Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V). *)
+(* Proof. *)
+(* intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=. *)
+(* by repeat (f_contractive || f_equiv). *)
+(* Qed. *)
+(* Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ := *)
+(* fixpoint iProto_le_pre' p1 p2. *)
+(* Arguments iProto_le {_ _} _%_proto _%_proto. *)
+(* Global Instance: Params (@iProto_le) 2 := {}. *)
+(* Notation "p ⊑ q" := (iProto_le p q) : bi_scope. *)
+
+(* Global Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V). *)
+(* Proof. solve_proper. Qed. *)
+(* Global Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V). *)
+(* Proof. solve_proper. Qed. *)
Record proto_name := ProtName { proto_names : gmap nat gname }.
Global Instance proto_name_inhabited : Inhabited proto_name :=
@@ -565,7 +565,7 @@ Definition iProto_ctx `{protoG Σ V}
(** * The connective for ownership of channel ends *)
Definition iProto_own `{!protoG Σ V}
(γ : gname) (i : nat) (p : iProto Σ V) : iProp Σ :=
- ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ i p'.
+ iProto_own_frag γ i p.
Arguments iProto_own {_ _ _} _ _ _%_proto.
Global Instance: Params (@iProto_own) 3 := {}.
@@ -607,195 +607,194 @@ Section proto.
Proof. iIntros "Hi Hj". by iDestruct (own_prot_idx with "Hi Hj") as %?. Qed.
(** ** Protocol entailment **)
- Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2.
- Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed.
-
- Lemma iProto_le_end : ⊢ END ⊑ (END : iProto Σ V).
- Proof. rewrite iProto_le_unfold. iLeft. auto 10. Qed.
-
- Lemma iProto_le_end_inv_r 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_l 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 i p1 m2 :
- p1 ⊑ (<(Send,i)> m2) -∗ ∃ m1,
- (p1 ≡ <(Send,i)> m1) ∗
- ∀ v p2', iMsg_car m2 v (Next p2') -∗
- ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
- Proof.
- rewrite iProto_le_unfold.
- iIntros "[[_ Heq]|H]".
- { by iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
- rewrite iProto_message_equivI. iDestruct "Hp2" as "[%Heq Hm2]".
- simplify_eq.
- destruct a1 as [[]]; [|done].
- iDestruct "H" as (->) "H". iExists m1. iFrame "Hp1".
- iIntros (v p2). iSpecialize ("Hm2" $! v (Next p2)). by iRewrite "Hm2".
- Qed.
-
- Lemma iProto_le_send_send_inv i m1 m2 v p2' :
- (<(Send,i)> m1) ⊑ (<(Send,i)> 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 (m1') "[Hm1 H]".
- iDestruct (iProto_message_equivI with "Hm1") as (Heq) "Hm1".
- iDestruct ("H" with "Hm2") as (p1') "[Hle Hm]".
- iRewrite -("Hm1" $! v (Next p1')) in "Hm". auto with iFrame.
- Qed.
-
- Lemma iProto_le_recv_inv_l i m1 p2 :
- (<(Recv,i)> m1) ⊑ p2 -∗ ∃ m2,
- (p2 ≡ <(Recv,i)> m2) ∗
- ∀ 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)".
- rewrite iProto_message_equivI. iDestruct "Hp1" as "[%Heq Hm1]".
- simplify_eq.
- destruct a2 as [[]]; [done|].
- iDestruct "H" as (->) "H". iExists m2. iFrame "Hp2".
- iIntros (v p1). iSpecialize ("Hm1" $! v (Next p1)). by iRewrite "Hm1".
- Qed.
-
- Lemma iProto_le_recv_inv_r i p1 m2 :
- (p1 ⊑ <(Recv,i)> m2) -∗ ∃ m1,
- (p1 ≡ <(Recv,i)> 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)".
- rewrite iProto_message_equivI.
- iDestruct "Hp2" as "[%Heq Hm2]".
- simplify_eq.
- destruct a1 as [[]]; [done|].
- iDestruct "H" as (->) "H".
- iExists m1. iFrame.
- iIntros (v p2).
- iIntros "Hm1". iDestruct ("H" with "Hm1") as (p2') "[Hle H]".
- iSpecialize ("Hm2" $! v (Next p2')).
- iExists p2'. iFrame.
- iRewrite "Hm2". iApply "H".
- Qed.
-
- Lemma iProto_le_recv_recv_inv i m1 m2 v p1' :
- (<(Recv, i)> m1) ⊑ (<(Recv, i)> 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_r 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_msg_inv_l i a m1 p2 :
- (<(a,i)> m1) ⊑ p2 -∗ ∃ m2, p2 ≡ <(a,i)> m2.
- Proof.
- rewrite iProto_le_unfold /iProto_le_pre.
- iIntros "[[Heq _]|H]".
- { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1' m2) "(Hp1 & Hp2 & H)".
- destruct a1 as [t1 ?], a2 as [t2 ?].
- destruct t1,t2; [|done|done|].
- - rewrite iProto_message_equivI.
- iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- - rewrite iProto_message_equivI.
- iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- Qed.
-
- Lemma iProto_le_msg_inv_r j a p1 m2 :
- (p1 ⊑ <(a,j)> m2) -∗ ∃ m1, p1 ≡ <(a,j)> m1.
- Proof.
- rewrite iProto_le_unfold /iProto_le_pre.
- iIntros "[[_ Heq]|H]".
- { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
- destruct a1 as [t1 ?], a2 as [t2 ?].
- destruct t1,t2; [|done|done|].
- - rewrite iProto_message_equivI.
- iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- - rewrite iProto_message_equivI.
- iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- Qed.
+ (* Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2. *)
+ (* Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed. *)
+
+ (* Lemma iProto_le_end : ⊢ END ⊑ (END : iProto Σ V). *)
+ (* Proof. rewrite iProto_le_unfold. iLeft. auto 10. Qed. *)
+
+ (* Lemma iProto_le_end_inv_r 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_l 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 i p1 m2 : *)
+ (* p1 ⊑ (<(Send,i)> m2) -∗ ∃ m1, *)
+ (* (p1 ≡ <(Send,i)> m1) ∗ *)
+ (* ∀ v p2', iMsg_car m2 v (Next p2') -∗ *)
+ (* ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1'). *)
+ (* Proof. *)
+ (* rewrite iProto_le_unfold. *)
+ (* iIntros "[[_ Heq]|H]". *)
+ (* { by iDestruct (iProto_message_end_equivI with "Heq") as %[]. } *)
+ (* iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)". *)
+ (* rewrite iProto_message_equivI. iDestruct "Hp2" as "[%Heq Hm2]". *)
+ (* simplify_eq. *)
+ (* destruct a1 as [[]]; [|done]. *)
+ (* iDestruct "H" as (->) "H". iExists m1. iFrame "Hp1". *)
+ (* iIntros (v p2). iSpecialize ("Hm2" $! v (Next p2)). by iRewrite "Hm2". *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_send_send_inv i m1 m2 v p2' : *)
+ (* (<(Send,i)> m1) ⊑ (<(Send,i)> 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 (m1') "[Hm1 H]". *)
+ (* iDestruct (iProto_message_equivI with "Hm1") as (Heq) "Hm1". *)
+ (* iDestruct ("H" with "Hm2") as (p1') "[Hle Hm]". *)
+ (* iRewrite -("Hm1" $! v (Next p1')) in "Hm". auto with iFrame. *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_recv_inv_l i m1 p2 : *)
+ (* (<(Recv,i)> m1) ⊑ p2 -∗ ∃ m2, *)
+ (* (p2 ≡ <(Recv,i)> m2) ∗ *)
+ (* ∀ 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)". *)
+ (* rewrite iProto_message_equivI. iDestruct "Hp1" as "[%Heq Hm1]". *)
+ (* simplify_eq. *)
+ (* destruct a2 as [[]]; [done|]. *)
+ (* iDestruct "H" as (->) "H". iExists m2. iFrame "Hp2". *)
+ (* iIntros (v p1). iSpecialize ("Hm1" $! v (Next p1)). by iRewrite "Hm1". *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_recv_inv_r i p1 m2 : *)
+ (* (p1 ⊑ <(Recv,i)> m2) -∗ ∃ m1, *)
+ (* (p1 ≡ <(Recv,i)> 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)". *)
+ (* rewrite iProto_message_equivI. *)
+ (* iDestruct "Hp2" as "[%Heq Hm2]". *)
+ (* simplify_eq. *)
+ (* destruct a1 as [[]]; [done|]. *)
+ (* iDestruct "H" as (->) "H". *)
+ (* iExists m1. iFrame. *)
+ (* iIntros (v p2). *)
+ (* iIntros "Hm1". iDestruct ("H" with "Hm1") as (p2') "[Hle H]". *)
+ (* iSpecialize ("Hm2" $! v (Next p2')). *)
+ (* iExists p2'. iFrame. *)
+ (* iRewrite "Hm2". iApply "H". *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_recv_recv_inv i m1 m2 v p1' : *)
+ (* (<(Recv, i)> m1) ⊑ (<(Recv, i)> 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_r 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_msg_inv_l i a m1 p2 : *)
+ (* (<(a,i)> m1) ⊑ p2 -∗ ∃ m2, p2 ≡ <(a,i)> m2. *)
+ (* Proof. *)
+ (* rewrite iProto_le_unfold /iProto_le_pre. *)
+ (* iIntros "[[Heq _]|H]". *)
+ (* { iDestruct (iProto_message_end_equivI with "Heq") as %[]. } *)
+ (* iDestruct "H" as (a1 a2 m1' m2) "(Hp1 & Hp2 & H)". *)
+ (* destruct a1 as [t1 ?], a2 as [t2 ?]. *)
+ (* destruct t1,t2; [|done|done|]. *)
+ (* - rewrite iProto_message_equivI. *)
+ (* iDestruct "Hp1" as (Heq) "Hp1". simplify_eq. *)
+ (* iDestruct "H" as (->) "H". by iExists _. *)
+ (* - rewrite iProto_message_equivI. *)
+ (* iDestruct "Hp1" as (Heq) "Hp1". simplify_eq. *)
+ (* iDestruct "H" as (->) "H". by iExists _. *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_msg_inv_r j a p1 m2 : *)
+ (* (p1 ⊑ <(a,j)> m2) -∗ ∃ m1, p1 ≡ <(a,j)> m1. *)
+ (* Proof. *)
+ (* rewrite iProto_le_unfold /iProto_le_pre. *)
+ (* iIntros "[[_ Heq]|H]". *)
+ (* { iDestruct (iProto_message_end_equivI with "Heq") as %[]. } *)
+ (* iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)". *)
+ (* destruct a1 as [t1 ?], a2 as [t2 ?]. *)
+ (* destruct t1,t2; [|done|done|]. *)
+ (* - rewrite iProto_message_equivI. *)
+ (* iDestruct "Hp2" as (Heq) "Hp2". simplify_eq. *)
+ (* iDestruct "H" as (->) "H". by iExists _. *)
+ (* - rewrite iProto_message_equivI. *)
+ (* iDestruct "Hp2" as (Heq) "Hp2". simplify_eq. *)
+ (* iDestruct "H" as (->) "H". by iExists _. *)
+ (* Qed. *)
- Lemma iProto_le_send i m1 m2 :
- (∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1',
- ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗
- (<(Send,i)> m1) ⊑ (<(Send,i)> m2).
- Proof.
- iIntros "Hle". rewrite iProto_le_unfold.
- iRight. iExists (Send, i), (Send, i), m1, m2. by eauto.
- Qed.
-
- Lemma iProto_le_recv i m1 m2 :
- (∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
- ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2')) -∗
- (<(Recv,i)> m1) ⊑ (<(Recv,i)> m2).
- Proof.
- iIntros "Hle". rewrite iProto_le_unfold.
- iRight. iExists (Recv, i), (Recv, i), m1, m2. by eauto.
- 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 as [[]].
- - 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_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ p1 ⊑ p3.
- Proof.
- iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
- destruct (iProto_case p3) as [->|([]&i&m3&->)].
- - iDestruct (iProto_le_end_inv_r with "H2") as "H2". by iRewrite "H2" in "H1".
- - iDestruct (iProto_le_send_inv with "H2") as (m2) "[Hp2 H2]".
- iRewrite "Hp2" in "H1"; clear p2.
- iDestruct (iProto_le_send_inv with "H1") as (m1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1.
- 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'").
- - iDestruct (iProto_le_recv_inv_r with "H2") as (m2) "[Hp2 H3]".
- iRewrite "Hp2" in "H1".
- iDestruct (iProto_le_recv_inv_r 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_refl p : ⊢ p ⊑ p.
- Proof.
- iLöb as "IH" forall (p). destruct (iProto_case p) as [->|([]&i&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_send i m1 m2 : *)
+ (* (∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1', *)
+ (* ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗ *)
+ (* (<(Send,i)> m1) ⊑ (<(Send,i)> m2). *)
+ (* Proof. *)
+ (* iIntros "Hle". rewrite iProto_le_unfold. *)
+ (* iRight. iExists (Send, i), (Send, i), m1, m2. by eauto. *)
+ (* Qed. *)
+
+ (* Lemma iProto_le_recv i m1 m2 : *)
+ (* (∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2', *)
+ (* ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2')) -∗ *)
+ (* (<(Recv,i)> m1) ⊑ (<(Recv,i)> m2). *)
+ (* Proof. *)
+ (* iIntros "Hle". rewrite iProto_le_unfold. *)
+ (* iRight. iExists (Recv, i), (Recv, i), m1, m2. by eauto. *)
+ (* 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 as [[]]. *)
+ (* - 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_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ p1 ⊑ p3. *)
+ (* Proof. *)
+ (* iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3). *)
+ (* destruct (iProto_case p3) as [->|([]&i&m3&->)]. *)
+ (* - iDestruct (iProto_le_end_inv_r with "H2") as "H2". by iRewrite "H2" in "H1". *)
+ (* - iDestruct (iProto_le_send_inv with "H2") as (m2) "[Hp2 H2]". *)
+ (* iRewrite "Hp2" in "H1"; clear p2. *)
+ (* iDestruct (iProto_le_send_inv with "H1") as (m1) "[Hp1 H1]". *)
+ (* iRewrite "Hp1"; clear p1. *)
+ (* 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'"). *)
+ (* - iDestruct (iProto_le_recv_inv_r with "H2") as (m2) "[Hp2 H3]". *)
+ (* iRewrite "Hp2" in "H1". *)
+ (* iDestruct (iProto_le_recv_inv_r 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_refl p : ⊢ p ⊑ p. *)
+ (* Proof. *)
+ (* iLöb as "IH" forall (p). destruct (iProto_case p) as [->|([]&i&m&->)]. *)
+ (* - iApply iProto_le_end. *)
+ (* - iApply iProto_le_send. auto 10 with iFrame. *)
+ (* - iApply iProto_le_recv. auto 10 with iFrame. *)
+ (* Qed. *)
Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
Proof. solve_proper. Qed.
@@ -865,10 +864,8 @@ Section proto.
iModIntro.
rewrite right_id_L.
rewrite -fmap_insert. iFrame.
- iSplitL "Hauth".
- - rewrite /iProto_own_auth.
- rewrite map_seq_snoc. simpl. done.
- - by iApply iProto_le_refl.
+ rewrite /iProto_own_auth.
+ rewrite map_seq_snoc. simpl. done.
Qed.
Lemma list_lookup_Some_le (ps : list $ iProto Σ V) (i : nat) (p1 : iProto Σ V) :
@@ -881,288 +878,6 @@ Section proto.
by apply lookup_lt_is_Some_1.
Qed.
- Lemma valid_target_le ps i p1 p2 :
- (∀ i' j', valid_target ps i' j') -∗
- ps !! i ≡ Some p1 -∗
- p1 ⊑ p2 -∗
- (∀ i' j', valid_target (<[i := p2]>ps) i' j') ∗ p1 ⊑ p2.
- Proof.
- iIntros "Hprot #HSome Hle".
- iDestruct (list_lookup_Some_le with "HSome") as %Hi.
- pose proof (iProto_case p1) as [Hend|Hmsg].
- { rewrite Hend. iDestruct (iProto_le_end_inv_l with "Hle") as "#H".
- iFrame "Hle".
- iIntros (i' j' a m) "Hm".
- destruct (decide (i = j')) as [->|Hneqj].
- { rewrite list_lookup_insert; [done|]. done. }
- rewrite (list_lookup_insert_ne _ i j'); [|done].
- destruct (decide (i = i')) as [->|Hneqi].
- { rewrite list_lookup_total_insert; [|done]. iRewrite "H" in "Hm".
- by iDestruct (iProto_end_message_equivI with "Hm") as "Hm". }
- rewrite list_lookup_total_insert_ne; [|done].
- by iApply "Hprot". }
- destruct Hmsg as (t & n & m & Hmsg).
- setoid_rewrite Hmsg.
- iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iFrame "Hle".
- iIntros (i' j' a m') "Hm".
- destruct (decide (i = j')) as [->|Hneqj].
- { by rewrite list_lookup_insert. }
- rewrite (list_lookup_insert_ne _ i j'); [|done].
- destruct (decide (i = i')) as [->|Hneqi].
- { rewrite list_lookup_total_insert; [|done]. iRewrite "Heq" in "Hm".
- iDestruct (iProto_message_equivI with "Hm") as (Heq) "Hm".
- simplify_eq. iApply ("Hprot" $! i').
- rewrite list_lookup_total_alt. iRewrite "HSome". done. }
- rewrite list_lookup_total_insert_ne; [|done].
- by iApply "Hprot".
- Qed.
-
- Lemma iProto_consistent_le ps i p1 p2 :
- iProto_consistent ps -∗
- ps !! i ≡ Some p1 -∗
- p1 ⊑ p2 -∗
- iProto_consistent (<[i := p2]>ps).
- Proof.
- iIntros "Hprot #HSome Hle".
- iRevert "HSome".
- iLöb as "IH" forall (p1 p2 ps).
- iIntros "#HSome".
- iDestruct (list_lookup_Some_le with "HSome") as %Hi.
- rewrite !iProto_consistent_unfold.
- iDestruct "Hprot" as "(Htar & Hprot)".
- iDestruct (valid_target_le with "Htar HSome Hle") as "[Htar Hle]".
- iFrame.
- iIntros (i' j' m1 m2) "#Hm1 #Hm2".
- destruct (decide (i = i')) as [<-|Hneq].
- { rewrite list_lookup_total_insert; [|done].
- pose proof (iProto_case p2) as [Hend|Hmsg].
- { setoid_rewrite Hend.
- rewrite !option_equivI. rewrite iProto_end_message_equivI. done. }
- destruct Hmsg as (a&?&m&Hmsg).
- setoid_rewrite Hmsg.
- destruct a; last first.
- { rewrite !option_equivI. rewrite iProto_message_equivI.
- iDestruct "Hm1" as "[%Htag Hm1]". done. }
- rewrite iProto_message_equivI.
- iDestruct "Hm1" as "[%Htag Hm1]".
- inversion Htag. simplify_eq.
- iIntros (v p) "Hm1'".
- iSpecialize ("Hm1" $! v (Next p)).
- iDestruct (iProto_le_send_inv with "Hle") as "Hle".
- iRewrite -"Hm1" in "Hm1'".
- iDestruct "Hle" as (m') "[#Heq H]".
- iDestruct ("H" with "Hm1'") as (p') "[Hle H]".
- destruct (decide (i = j')) as [<-|Hneq].
- { rewrite list_lookup_total_insert; [|done].
- rewrite iProto_message_equivI.
- iDestruct "Hm2" as "[%Heq _]". done. }
- iDestruct ("Hprot" $!i j' with "[] [] H") as "Hprot".
- { iRewrite -"Heq". iEval (rewrite list_lookup_total_alt).
- iRewrite "HSome". done. }
- { rewrite list_lookup_total_insert_ne; [|done]. done. }
- iDestruct "Hprot" as (p'') "[Hm Hprot]".
- iExists p''. iFrame.
- iNext.
- iDestruct ("IH" with "Hprot Hle [HSome]") as "HI".
- { rewrite list_lookup_insert; [done|].
- by rewrite length_insert. }
- iClear "IH Hm1 Hm2 Heq".
- rewrite list_insert_insert.
- rewrite (list_insert_commute _ j' i); [|done].
- rewrite list_insert_insert. done. }
- rewrite list_lookup_total_insert_ne; [|done].
- destruct (decide (i = j')) as [<-|Hneq'].
- { rewrite list_lookup_total_insert; [|done].
- pose proof (iProto_case p2) as [Hend|Hmsg].
- { setoid_rewrite Hend.
- rewrite !option_equivI.
- rewrite iProto_end_message_equivI. done. }
- destruct Hmsg as (a&?&m&Hmsg).
- setoid_rewrite Hmsg.
- destruct a.
- { rewrite !option_equivI.
- rewrite iProto_message_equivI.
- iDestruct "Hm2" as "[%Htag Hm2]". done. }
- rewrite iProto_message_equivI.
- iDestruct "Hm2" as "[%Htag Hm2]".
- inversion Htag. simplify_eq.
- iIntros (v p) "Hm1'".
- iDestruct (iProto_le_recv_inv_r with "Hle") as "Hle".
- iDestruct "Hle" as (m') "[#Heq Hle]".
- iDestruct ("Hprot" $!i' with "[] [] Hm1'") as "Hprot".
- { done. }
- { iEval (rewrite list_lookup_total_alt). iRewrite "HSome". done. }
- iDestruct ("Hprot") as (p') "[Hm1' Hprot]".
- iDestruct ("Hle" with "Hm1'") as (p2') "[Hle Hm']".
- iSpecialize ("Hm2" $! v (Next p2')).
- iExists p2'.
- iRewrite -"Hm2". iFrame.
- iDestruct ("IH" with "Hprot Hle []") as "HI".
- { iPureIntro. rewrite list_lookup_insert_ne; [|done].
- by rewrite list_lookup_insert. }
- rewrite list_insert_commute; [|done].
- rewrite !list_insert_insert. done. }
- rewrite list_lookup_total_insert_ne; [|done].
- iIntros (v p) "Hm1'".
- iDestruct ("Hprot" $!i' j' with "[//] [//] Hm1'") as "Hprot".
- iDestruct "Hprot" as (p') "[Hm2' Hprot]".
- iExists p'. iFrame.
- iNext.
- rewrite (list_insert_commute _ j' i); [|done].
- rewrite (list_insert_commute _ i' i); [|done].
- iApply ("IH" with "Hprot Hle []").
- rewrite list_lookup_insert_ne; [|done].
- rewrite list_lookup_insert_ne; [|done].
- done.
- 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 [->|([]&i&m1&->)].
- - iDestruct (iProto_le_end_inv_r with "H") as "H".
- iRewrite "H". iApply iProto_le_refl.
- - iDestruct (iProto_le_send_inv with "H") as (m2) "[Hp2 H]".
- iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message).
- 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.
- - iDestruct (iProto_le_recv_inv_r 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_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 [->|([]&i&m2&->)].
- - iDestruct (iProto_le_end_inv_r with "H1") as "H1".
- iRewrite "H1". by rewrite !left_id.
- - iDestruct (iProto_le_send_inv with "H1") as (m1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1. rewrite !iProto_app_message.
- 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").
- - iDestruct (iProto_le_recv_inv_r 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.
-
- Lemma iProto_le_payload_elim_l i m v P p :
- (P -∗ (<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> m)) ⊢
- (<(Recv,i)> MSG v {{ P }}; p) ⊑ <(Recv,i)> m.
- Proof.
- rewrite iMsg_base_eq. iIntros "H".
- 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 i m v P p :
- (P -∗ (<(Send, i)> m) ⊑ (<(Send, i)> MSG v; p)) ⊢
- (<(Send,i)> m) ⊑ (<(Send,i)> MSG v {{ P }}; p).
- Proof.
- rewrite iMsg_base_eq. iIntros "H".
- iApply iProto_le_send. iIntros (v' p') "(->&Hp&HP)".
- iApply (iProto_le_send_send_inv with "(H HP)"); simpl; auto.
- Qed.
- Lemma iProto_le_payload_intro_l i v P p :
- P -∗ (<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> 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 i v P p :
- P -∗ (<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> 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} i (m1 : A → iMsg Σ V) m2 :
- (∀ x, (<(Recv,i)> m1 x) ⊑ (<(Recv,i)> m2)) ⊢
- (<(Recv,i) @ x> m1 x) ⊑ (<(Recv,i)> m2).
- Proof.
- rewrite iMsg_exist_eq. iIntros "H".
- iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
- by iApply (iProto_le_recv_recv_inv with "H").
- Qed.
- Lemma iProto_le_exist_elim_r {A} i m1 (m2 : A → iMsg Σ V) :
- (∀ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x)) ⊢
- (<(Send,i)> m1) ⊑ (<(Send,i) @ x> m2 x).
- Proof.
- rewrite iMsg_exist_eq. iIntros "H".
- iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
- by iApply (iProto_le_send_send_inv with "H").
- Qed.
- Lemma iProto_le_exist_intro_l {A} i (m : A → iMsg Σ V) a :
- ⊢ (<(Send,i) @ x> m x) ⊑ (<(Send,i)> 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} i (m : A → iMsg Σ V) a :
- ⊢ (<(Recv,i)> m a) ⊑ (<(Recv,i) @ 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} i (m1 : TT → iMsg Σ V) m2 :
- (∀ x, (<(Recv,i)> m1 x) ⊑ (<(Recv,i)> m2)) ⊢
- (<(Recv,i) @.. x> m1 x) ⊑ (<(Recv,i)> 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} i m1 (m2 : TT → iMsg Σ V) :
- (∀ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x)) -∗
- (<(Send,i)> m1) ⊑ (<(Send,i) @.. 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} i (m : TT → iMsg Σ V) x :
- ⊢ (<(Send,i) @.. x> m x) ⊑ (<(Send,i)> 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} i (m : TT → iMsg Σ V) x :
- ⊢ (<(Recv,i)> m x) ⊑ (<(Recv,i) @.. 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_consistent_target ps m a i j :
iProto_consistent ps -∗
ps !! i ≡ Some (<(a, j)> m) -∗
@@ -1190,19 +905,10 @@ Section proto.
iExists p2. iFrame.
Qed.
- Lemma iProto_own_le γ s p1 p2 :
- iProto_own γ s p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ s p2.
- Proof.
- iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
- iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
- Qed.
-
Lemma iProto_own_excl γ i (p1 p2 : iProto Σ V) :
iProto_own γ i p1 -∗ iProto_own γ i p2 -∗ False.
Proof.
- rewrite /iProto_own.
- iDestruct 1 as (p1') "[_ Hp1]".
- iDestruct 1 as (p2') "[_ Hp2]".
+ rewrite /iProto_own. iIntros "Hp1 Hp2".
iDestruct (own_prot_excl with "Hp1 Hp2") as %[].
Qed.
@@ -1214,7 +920,6 @@ Section proto.
iIntros "Hctx Hown".
rewrite /iProto_ctx /iProto_own.
iDestruct "Hctx" as (ps <-) "[Hauth Hps]".
- iDestruct "Hown" as (p') "[Hle Hown]".
iDestruct (iProto_own_auth_agree_Some with "Hauth Hown") as %HSome.
iPureIntro.
by apply lookup_lt_is_Some_1.
@@ -1240,45 +945,35 @@ Section proto.
iIntros "Hctx Hi Hj Hm".
iDestruct (iProto_ctx_agree with "Hctx Hi") as %Hi.
iDestruct (iProto_ctx_agree with "Hctx Hj") as %Hij.
- iDestruct "Hi" as (pi) "[Hile Hi]".
- iDestruct "Hj" as (pj) "[Hjle Hj]".
iDestruct "Hctx" as (ps Hdom) "[Hauth Hconsistent]".
iDestruct (iProto_own_auth_agree with "Hauth Hi") as "#Hpi".
iDestruct (iProto_own_auth_agree with "Hauth Hj") as "#Hpj".
iDestruct (own_prot_idx with "Hi Hj") as %Hneq.
- iAssert (▷ (<[i:=<(Send, j)> m1]>ps !! j ≡ Some pj))%I as "Hpj'".
- { by rewrite list_lookup_insert_ne. }
- iAssert (▷ (⌜is_Some (ps !! i)⌠∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]"
- as "[Hi' Hile]".
- { iNext. iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#Heq".
- iFrame. iRewrite "Heq" in "Hpi". destruct (ps !! i); [done|].
- by rewrite option_equivI. }
- iAssert (▷ (⌜is_Some (ps !! j)⌠∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]"
- as "[Hj' Hjle]".
- { iNext. iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#Heq".
- iFrame. iRewrite "Heq" in "Hpj".
- destruct (ps !! j); [done|]. by rewrite !option_equivI. }
- iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent".
- iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent".
- iDestruct (iProto_consistent_step _ _ _ i j with "Hconsistent [] [] [Hm //]") as
+ (* iAssert (▷ (<[i:=<(Send, j)> m1]>ps !! j ≡ Some pj))%I as "Hpj'". *)
+ (* { by rewrite list_lookup_insert_ne. } *)
+ (* iAssert (▷ (⌜is_Some (ps !! i)⌠∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]" *)
+ (* as "[Hi' Hile]". *)
+ (* { iNext. iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#Heq". *)
+ (* iFrame. iRewrite "Heq" in "Hpi". destruct (ps !! i); [done|]. *)
+ (* by rewrite option_equivI. } *)
+ (* iAssert (▷ (⌜is_Some (ps !! j)⌠∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]" *)
+ (* as "[Hj' Hjle]". *)
+ (* { iNext. iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#Heq". *)
+ (* iFrame. iRewrite "Heq" in "Hpj". *)
+ (* destruct (ps !! j); [done|]. by rewrite !option_equivI. } *)
+ (* iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent". *)
+ (* iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent". *)
+ iDestruct (iProto_consistent_step _ _ _ i j with "Hconsistent Hpi Hpj [Hm //]") as
(p2) "[Hm2 Hconsistent]".
- { rewrite list_lookup_insert_ne; [|done].
- rewrite list_lookup_insert_ne; [|done].
- rewrite list_lookup_insert; [done|]. lia. }
- { rewrite list_lookup_insert_ne; [|done].
- rewrite list_lookup_insert; [done|]. rewrite length_insert. lia. }
iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
iIntros "!>!>". iExists p2. iFrame "Hm2".
- iDestruct "Hi'" as %Hi'. iDestruct "Hj'" as %Hj'.
iSplitL "Hconsistent Hauth".
{ iExists (<[i:=p1]> (<[j:=p2]> ps)).
iSplit.
{ iPureIntro. rewrite !length_insert. done. }
- iFrame. rewrite list_insert_insert.
- rewrite list_insert_commute; [|done]. rewrite list_insert_insert.
- by rewrite list_insert_commute; [|done]. }
- iSplitL "Hi"; iExists _; iFrame; iApply iProto_le_refl.
+ iFrame. }
+ iFrame.
Qed.
Lemma iProto_target γ ps_dom i a j m :
@@ -1289,89 +984,88 @@ Section proto.
iIntros "Hctx Hown".
rewrite /iProto_ctx /iProto_own.
iDestruct "Hctx" as (ps Hdom) "[Hauth Hps]".
- iDestruct "Hown" as (p') "[Hle Hown]".
+ (* iDestruct "Hown" as (p') "[Hle Hown]". *)
iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#Hi".
- iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
- iDestruct (iProto_consistent_target with "Hps []") as "#H".
- { iNext. iRewrite "Heq" in "Hi". done. }
+ (* iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq". *)
+ iDestruct (iProto_consistent_target with "Hps Hi") as "#H".
iNext. iDestruct "H" as %HSome.
iPureIntro. subst. by apply lookup_lt_is_Some_1.
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} i (m1 : A → iMsg Σ V) m2 name :
- AsIdentName m1 name →
- FromForall (iProto_message (Recv,i) (iMsg_exist m1) ⊑ (<(Recv,i)> m2))
- (λ x, (<(Recv, i)> m1 x) ⊑ (<(Recv, i)> m2))%I name | 10.
- Proof. intros _. apply iProto_le_exist_elim_l. Qed.
- Global Instance iProto_le_from_forall_r {A} i m1 (m2 : A → iMsg Σ V) name :
- AsIdentName m2 name →
- FromForall ((<(Send,i)> m1) ⊑ iProto_message (Send,i) (iMsg_exist m2))
- (λ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x))%I name | 11.
- Proof. intros _. apply iProto_le_exist_elim_r. Qed.
-
- Global Instance iProto_le_from_wand_l i m v P p :
- TCIf (TCEq P True%I) False TCTrue →
- FromWand ((<(Recv,i)> MSG v {{ P }}; p) ⊑ (<(Recv,i)> m)) P ((<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> m)) | 10.
- Proof. intros _. apply iProto_le_payload_elim_l. Qed.
- Global Instance iProto_le_from_wand_r i m v P p :
- FromWand ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v {{ P }}; p)) P ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v; p)) | 11.
- Proof. apply iProto_le_payload_elim_r. Qed.
-
- Global Instance iProto_le_from_exist_l {A} i (m : A → iMsg Σ V) p :
- FromExist ((<(Send,i) @ x> m x) ⊑ p) (λ a, (<(Send,i)> 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} i (m : A → iMsg Σ V) p :
- FromExist (p ⊑ <(Recv,i) @ x> m x) (λ a, p ⊑ (<(Recv,i)> 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 i m v P p :
- FromSep ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m)) P ((<(Send,i)> MSG v; p) ⊑ (<(Send,i)> 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 i m v P p :
- FromSep ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p)) P ((<(Recv,i)> m) ⊑ (<(Recv,i)> 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 i q m v R P Q p :
- Frame q R P Q →
- Frame q R ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m))
- ((<(Send,i)> MSG v {{ Q }}; p) ⊑ (<(Send,i)> 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 i q m v R P Q p :
- Frame q R P Q →
- Frame q R ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p))
- ((<(Recv,i)> m) ⊑ (<(Recv,i)> 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 _. iApply iProto_le_base. 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} i (m1 : A → iMsg Σ V) m2 name : *)
+ (* AsIdentName m1 name → *)
+ (* FromForall (iProto_message (Recv,i) (iMsg_exist m1) ⊑ (<(Recv,i)> m2)) *)
+ (* (λ x, (<(Recv, i)> m1 x) ⊑ (<(Recv, i)> m2))%I name | 10. *)
+ (* Proof. intros _. apply iProto_le_exist_elim_l. Qed. *)
+ (* Global Instance iProto_le_from_forall_r {A} i m1 (m2 : A → iMsg Σ V) name : *)
+ (* AsIdentName m2 name → *)
+ (* FromForall ((<(Send,i)> m1) ⊑ iProto_message (Send,i) (iMsg_exist m2)) *)
+ (* (λ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x))%I name | 11. *)
+ (* Proof. intros _. apply iProto_le_exist_elim_r. Qed. *)
+
+ (* Global Instance iProto_le_from_wand_l i m v P p : *)
+ (* TCIf (TCEq P True%I) False TCTrue → *)
+ (* FromWand ((<(Recv,i)> MSG v {{ P }}; p) ⊑ (<(Recv,i)> m)) P ((<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> m)) | 10. *)
+ (* Proof. intros _. apply iProto_le_payload_elim_l. Qed. *)
+ (* Global Instance iProto_le_from_wand_r i m v P p : *)
+ (* FromWand ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v {{ P }}; p)) P ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v; p)) | 11. *)
+ (* Proof. apply iProto_le_payload_elim_r. Qed. *)
+
+ (* Global Instance iProto_le_from_exist_l {A} i (m : A → iMsg Σ V) p : *)
+ (* FromExist ((<(Send,i) @ x> m x) ⊑ p) (λ a, (<(Send,i)> 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} i (m : A → iMsg Σ V) p : *)
+ (* FromExist (p ⊑ <(Recv,i) @ x> m x) (λ a, p ⊑ (<(Recv,i)> 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 i m v P p : *)
+ (* FromSep ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m)) P ((<(Send,i)> MSG v; p) ⊑ (<(Send,i)> 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 i m v P p : *)
+ (* FromSep ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p)) P ((<(Recv,i)> m) ⊑ (<(Recv,i)> 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 i q m v R P Q p : *)
+ (* Frame q R P Q → *)
+ (* Frame q R ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m)) *)
+ (* ((<(Send,i)> MSG v {{ Q }}; p) ⊑ (<(Send,i)> 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 i q m v R P Q p : *)
+ (* Frame q R P Q → *)
+ (* Frame q R ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p)) *)
+ (* ((<(Recv,i)> m) ⊑ (<(Recv,i)> 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 _. iApply iProto_le_base. Qed. *)
End proto.
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.
+(* 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. *)