From 72cce691fdf72047f028c2f6297864f58ed2cd82 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Mon, 17 Mar 2025 21:14:48 +0100
Subject: [PATCH] Closed non-mixed choice lemmas for mixed choice model
---
multris/channel/channel.v | 70 ++-
multris/channel/proofmode.v | 182 ++++--
multris/channel/proto.v | 1144 ++++++++++++++++++++++++-----------
multris/examples/basics.v | 9 +-
4 files changed, 980 insertions(+), 425 deletions(-)
diff --git a/multris/channel/channel.v b/multris/channel/channel.v
index f788033..d3caf09 100644
--- a/multris/channel/channel.v
+++ b/multris/channel/channel.v
@@ -91,13 +91,14 @@ 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),
+ ∃ γ (γEs : list gname) (m:val) (i:nat) (n:nat) p',
⌜ 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)) ∗
- own (γEs !!! i) (â—E (Next p)) ∗ own (γEs !!! i) (â—¯E (Next p)) ∗
- iProto_own γ i p.
+ ▷ (p' ⊑ 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 :
@@ -129,6 +130,15 @@ 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 →
@@ -196,9 +206,9 @@ Section channel.
iModIntro.
iApply "HΦ".
iSplitL "Hl".
- { rewrite iProto_pointsto_eq. iExists _, _, _, _, _.
+ { rewrite iProto_pointsto_eq. iExists _, _, _, _, _, _.
iSplit; [done|].
- iFrame. iFrame "#∗". }
+ iFrame. iFrame "#∗". iNext. done. }
iExists γp, γEs, _. iSplit; [done|].
iFrame. iFrame "#∗".
simpl.
@@ -217,12 +227,14 @@ Section channel.
Proof.
rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
iDestruct "Hc" as
- (γ γE l i n ->) "(#IH & #Hls & H◠& H◯ & Hown)".
+ (γ γE l i n p' ->) "(#IH & #Hls & Hle & 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".
- wp_pures. iModIntro. iFrame.
+ iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
wp_pures.
iDestruct "Hi" as %Hi.
iDestruct "Hj" as %Hj.
@@ -243,8 +255,10 @@ Section channel.
wp_store.
iMod (own_update_2 with "Hâ— Hâ—¯") as "[Hâ— Hâ—¯]"; [by apply excl_auth_update|].
iModIntro.
- iSplitL "Hl' Hâ— Hown".
- { iRight. iLeft. iIntros "!>". iExists _, _. iFrame. }
+ iSplitL "Hl' Hâ— Hown Hle".
+ { iRight. iLeft. iIntros "!>". iExists _, _. iFrame.
+ iDestruct (iProto_own_le with "Hown Hle") as "Hown".
+ by rewrite iMsg_base_eq. }
wp_pures.
iLöb as "HL".
wp_lam.
@@ -271,18 +285,25 @@ Section channel.
{ apply excl_auth_update. }
iModIntro.
iApply "HΦ".
- iExists _, _, _, _, _.
+ iExists _, _, _, _, _, _.
iSplit; [done|]. iFrame "#∗".
- iRewrite -"Hagree'". done.
+ iRewrite -"Hagree'". iApply iProto_le_refl.
Qed.
- Lemma send_spec_tele {TT} c j (tt : TT)
+ Lemma send_spec_tele {TT} c i (tt : TT)
(v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
- {{{ c ↣ (<(Send,j) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
- send c #j (v tt)
+ {{{ c ↣ (<(Send,i) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+ send c #i (v tt)
{{{ RET #(); c ↣ (p tt) }}}.
- Proof. Admitted.
-
+ 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.
+
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 }}}
recv c #j
@@ -291,13 +312,15 @@ Section channel.
iIntros (Φ) "Hc HΦ". iLöb as "HL". wp_lam.
rewrite iProto_pointsto_eq.
iDestruct "Hc" as
- (γ γE l i n ->) "(#IH & #Hls & H◠& H◯ & Hown)".
+ (γ γE l i n p' ->) "(#IH & #Hls & Hle & 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".
- wp_pures. iModIntro. iFrame.
+ iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
wp_pure _.
iDestruct "Hi" as %Hi.
iDestruct "Hj" as %Hj.
@@ -312,19 +335,20 @@ Section channel.
wp_xchg. iModIntro.
iSplitL "Hl' Htok".
{ iLeft. iFrame. }
- wp_pures. iApply ("HL" with "[H◠H◯ Hown] HΦ").
- iExists _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+ wp_pures. iApply ("HL" with "[H◠H◯ Hown Hle] 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 "#∗". }
+ wp_pures. iApply ("HL" with "[H◠H◯ Hown Hle] 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. }
@@ -340,7 +364,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 ∗".
- iExists _. iSplit; [done|]. iRewrite "Hp". iFrame.
+ iSplit; [done|]. iRewrite "Hp". iApply iProto_le_refl.
Qed.
End channel.
diff --git a/multris/channel/proofmode.v b/multris/channel/proofmode.v
index d3da00d..484e641 100644
--- a/multris/channel/proofmode.v
+++ b/multris/channel/proofmode.v
@@ -61,27 +61,27 @@ Section classes.
Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
Proof. rewrite /ProtoNormalize=> Hp d pas q. by rewrite Hp. Qed.
- Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
- Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
- Global Instance proto_normalize_done_dual p :
- ProtoNormalize true p [] (iProto_dual p) | 0.
- Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
- Global Instance proto_normalize_done_dual_end :
- ProtoNormalize (Σ:=Σ) true END [] END | 0.
- Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. auto. Qed.
-
- Global Instance proto_normalize_dual d p pas q :
- ProtoNormalize (negb d) p pas q →
- ProtoNormalize d (iProto_dual p) pas q.
- Proof. rewrite /ProtoNormalize. by destruct d; rewrite /= ?involutive. Qed.
-
- Global Instance proto_normalize_app_l d p1 p2 pas q :
- ProtoNormalize d p1 ((d,p2) :: pas) q →
- ProtoNormalize d (p1 <++> p2) pas q.
- Proof.
- rewrite /ProtoNormalize /=. rewrite assoc.
- by destruct d; by rewrite /= ?iProto_dual_app.
- Qed.
+ (* Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0. *)
+ (* Proof. rewrite /ProtoNormalize /= right_id. auto. Qed. *)
+ (* Global Instance proto_normalize_done_dual p : *)
+ (* ProtoNormalize true p [] (iProto_dual p) | 0. *)
+ (* Proof. rewrite /ProtoNormalize /= right_id. auto. Qed. *)
+ (* Global Instance proto_normalize_done_dual_end : *)
+ (* ProtoNormalize (Σ:=Σ) true END [] END | 0. *)
+ (* Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. auto. Qed. *)
+
+ (* Global Instance proto_normalize_dual d p pas q : *)
+ (* ProtoNormalize (negb d) p pas q → *)
+ (* ProtoNormalize d (iProto_dual p) pas q. *)
+ (* Proof. rewrite /ProtoNormalize. by destruct d; rewrite /= ?involutive. Qed. *)
+
+ (* Global Instance proto_normalize_app_l d p1 p2 pas q : *)
+ (* ProtoNormalize d p1 ((d,p2) :: pas) q → *)
+ (* ProtoNormalize d (p1 <++> p2) pas q. *)
+ (* Proof. *)
+ (* rewrite /ProtoNormalize /=. rewrite assoc. *)
+ (* by destruct d; by rewrite /= ?iProto_dual_app. *)
+ (* Qed. *)
Global Instance proto_normalize_end d d' p pas q :
ProtoNormalize d p pas q →
@@ -91,15 +91,15 @@ Section classes.
destruct d'; by rewrite /= ?iProto_dual_end left_id.
Qed.
- Global Instance proto_normalize_app_r d p1 p2 pas q :
- ProtoNormalize d p2 pas q →
- ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0.
- Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
+ (* Global Instance proto_normalize_app_r d p1 p2 pas q : *)
+ (* ProtoNormalize d p2 pas q → *)
+ (* ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0. *)
+ (* Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed. *)
- Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
- ProtoNormalize d p2 pas q →
- ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0.
- Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
+ (* Global Instance proto_normalize_app_r_dual d p1 p2 pas q : *)
+ (* ProtoNormalize d p2 pas q → *)
+ (* ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0. *)
+ (* Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed. *)
Global Instance msg_normalize_base d v P p q pas :
ProtoNormalize d p pas q →
@@ -131,22 +131,22 @@ Section classes.
(** Automatically perform normalization of protocols in the proof mode when
using [iAssumption] and [iFrame]. *)
- Global Instance pointsto_proto_from_assumption q c p1 p2 :
- ProtoNormalize false p1 [] p2 →
- FromAssumption q (c ↣ p1) (c ↣ p2).
- Proof.
- rewrite /FromAssumption /ProtoNormalize /= right_id.
- rewrite bi.intuitionistically_if_elim.
- iIntros (?) "H". by iApply (iProto_pointsto_le with "H").
- Qed.
- Global Instance pointsto_proto_from_frame q c p1 p2 :
- ProtoNormalize false p1 [] p2 →
- Frame q (c ↣ p1) (c ↣ p2) True.
- Proof.
- rewrite /Frame /ProtoNormalize /= right_id.
- rewrite bi.intuitionistically_if_elim.
- iIntros (?) "[H _]". by iApply (iProto_pointsto_le with "H").
- Qed.
+ (* Global Instance pointsto_proto_from_assumption q c p1 p2 : *)
+ (* ProtoNormalize false p1 [] p2 → *)
+ (* FromAssumption q (c ↣ p1) (c ↣ p2). *)
+ (* Proof. *)
+ (* rewrite /FromAssumption /ProtoNormalize /= right_id. *)
+ (* rewrite bi.intuitionistically_if_elim. *)
+ (* iIntros (?) "H". by iApply (iProto_pointsto_le with "H"). *)
+ (* Qed. *)
+ (* Global Instance pointsto_proto_from_frame q c p1 p2 : *)
+ (* ProtoNormalize false p1 [] p2 → *)
+ (* Frame q (c ↣ p1) (c ↣ p2) True. *)
+ (* Proof. *)
+ (* rewrite /Frame /ProtoNormalize /= right_id. *)
+ (* rewrite bi.intuitionistically_if_elim. *)
+ (* iIntros (?) "[H _]". by iApply (iProto_pointsto_le with "H"). *)
+ (* Qed. *)
End classes.
(** * Symbolic execution tactics *)
@@ -154,7 +154,8 @@ End classes.
Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K v (n:nat) c p m tv tP tP' tp Φ :
v = #n →
envs_lookup i Δ = Some (false, c ↣ p)%I →
- ProtoNormalize false p [] (<(Recv,n)> m) →
+ (* ProtoNormalize false p [] (<(Recv,n)> m) → *)
+ p ≡ (<(Recv,n)> m)%proto →
MsgTele m tv tP tp →
(∀.. x, MaybeIntoLaterN false 1 (tele_app tP x) (tele_app tP' x)) →
let Δ' := envs_delete false i false Δ in
@@ -168,12 +169,12 @@ Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K v (n:nat) c p m
Proof.
intros ->.
rewrite envs_entails_unseal /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
- rewrite !tforall_forall right_id.
+ rewrite !tforall_forall.
intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
assert (c ↣ p ⊢ c ↣ <(Recv,n) @.. x>
MSG tele_app tv x {{ â–· tele_app tP' x }}; tele_app tp x) as ->.
{ iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>".
- iApply iProto_le_trans; [iApply Hp|rewrite Hm].
+ iApply iProto_le_trans; [rewrite Hp; iApply iProto_le_refl|rewrite Hm].
iApply iProto_le_texist_elim_l; iIntros (x).
iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ _ x)]; simpl.
iIntros "H". by iDestruct (HP with "H") as "$". }
@@ -184,6 +185,41 @@ Proof.
rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
Qed.
+(* (** * Symbolic execution tactics *) *)
+(* (* TODO: Maybe strip laters from other hypotheses in the future? *) *)
+(* Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K v (n:nat) c p m tv tP tP' tp Φ : *)
+(* v = #n → *)
+(* envs_lookup i Δ = Some (false, c ↣ p)%I → *)
+(* ProtoNormalize false p [] (<(Recv,n)> m) → *)
+(* MsgTele m tv tP tp → *)
+(* (∀.. x, MaybeIntoLaterN false 1 (tele_app tP x) (tele_app tP' x)) → *)
+(* let Δ' := envs_delete false i false Δ in *)
+(* (∀.. x : TT, *)
+(* match envs_app false *)
+(* (Esnoc (Esnoc Enil j (tele_app tP' x)) i (c ↣ tele_app tp x)) Δ' with *)
+(* | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (tele_app tv x)) {{ Φ }}) *)
+(* | None => False *)
+(* end) → *)
+(* envs_entails Δ (WP fill K (recv c v) {{ Φ }}). *)
+(* Proof. *)
+(* intros ->. *)
+(* rewrite envs_entails_unseal /ProtoNormalize /MsgTele /MaybeIntoLaterN /=. *)
+(* rewrite !tforall_forall right_id. *)
+(* intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl. *)
+(* assert (c ↣ p ⊢ c ↣ <(Recv,n) @.. x> *)
+(* MSG tele_app tv x {{ â–· tele_app tP' x }}; tele_app tp x) as ->. *)
+(* { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>". *)
+(* iApply iProto_le_trans; [iApply Hp|rewrite Hm]. *)
+(* iApply iProto_le_texist_elim_l; iIntros (x). *)
+(* iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ _ x)]; simpl. *)
+(* iIntros "H". by iDestruct (HP with "H") as "$". } *)
+(* rewrite -wp_bind. eapply bi.wand_apply; *)
+(* [by eapply bi.wand_entails, (recv_spec _ n (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done]. *)
+(* rewrite -bi.later_intro; apply bi.forall_intro=> x. *)
+(* specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //. *)
+(* rewrite envs_app_sound //; simpl. by rewrite right_id HΦ. *)
+(* Qed. *)
+
Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
@@ -196,7 +232,8 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
|fail 1 "wp_recv: cannot find 'recv' in" e];
[|solve_pointsto ()
- |tc_solve || fail 1 "wp_recv: protocol not of the shape <?>"
+ |done || fail 1 "wp_recv: protocol not of the shape <?>"
+ (* |tc_solve || fail 1 "wp_recv: protocol not of the shape <?>" *)
|tc_solve || fail 1 "wp_recv: cannot convert to telescope"
|tc_solve
|pm_reduce; simpl; tac_intros;
@@ -213,11 +250,12 @@ Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as"
"(" ne_simple_intropattern_list(ys) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => _iDestructHyp H ys pat).
-
+
Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K (n:nat) w c v p m tv tP tp Φ :
w = #n →
envs_lookup i Δ = Some (false, c ↣ p)%I →
- ProtoNormalize false p [] (<(Send,n)> m) →
+ (* ProtoNormalize false p [] (<(Send,n)> m) → *)
+ p ≡ (<(Send,n)> m)%proto →
MsgTele m tv tP tp →
let Δ' := envs_delete false i false Δ in
(∃.. x : TT,
@@ -235,7 +273,7 @@ Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K (n:nat) w c
envs_entails Δ (WP fill K (send c w v) {{ Φ }}).
Proof.
intros ->.
- rewrite envs_entails_unseal /ProtoNormalize /MsgTele /= right_id texist_exist.
+ rewrite envs_entails_unseal /MsgTele /= texist_exist.
intros ? Hp Hm [x HΦ]. rewrite envs_lookup_sound //; simpl.
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
@@ -244,11 +282,46 @@ Proof.
assert (c ↣ p ⊢
c ↣ <(Send,n) @.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
{ iIntros "Hc". iApply (iProto_pointsto_le with "Hc"); iIntros "!>".
- iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
+ rewrite Hp. iApply iProto_le_trans; [iApply iProto_le_refl|]. by rewrite Hm. }
eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|].
by rewrite -bi.later_intro.
Qed.
+(* Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K (n:nat) w c v p m tv tP tp Φ : *)
+(* w = #n → *)
+(* envs_lookup i Δ = Some (false, c ↣ p)%I → *)
+(* ProtoNormalize false p [] (<(Send,n)> m) → *)
+(* MsgTele m tv tP tp → *)
+(* let Δ' := envs_delete false i false Δ in *)
+(* (∃.. x : TT, *)
+(* match envs_split (if neg is true then base.Right else base.Left) js Δ' with *)
+(* | Some (Δ1,Δ2) => *)
+(* match envs_app false (Esnoc Enil i (c ↣ tele_app tp x)) Δ2 with *)
+(* | Some Δ2' => *)
+(* v = tele_app tv x ∧ *)
+(* envs_entails Δ1 (tele_app tP x) ∧ *)
+(* envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }}) *)
+(* | None => False *)
+(* end *)
+(* | None => False *)
+(* end) → *)
+(* envs_entails Δ (WP fill K (send c w v) {{ Φ }}). *)
+(* Proof. *)
+(* intros ->. *)
+(* rewrite envs_entails_unseal /ProtoNormalize /MsgTele /= right_id texist_exist. *)
+(* intros ? Hp Hm [x HΦ]. rewrite envs_lookup_sound //; simpl. *)
+(* destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //. *)
+(* destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //. *)
+(* rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl. *)
+(* destruct HΦ as (-> & -> & ->). rewrite right_id assoc. *)
+(* assert (c ↣ p ⊢ *)
+(* c ↣ <(Send,n) @.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->. *)
+(* { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"); iIntros "!>". *)
+(* iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. } *)
+(* eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|]. *)
+(* by rewrite -bi.later_intro. *)
+(* Qed. *)
+
Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
let solve_pointsto _ :=
let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
@@ -271,7 +344,8 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
[reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
|fail 1 "wp_send: cannot find 'send' in" e];
[|solve_pointsto ()
- |tc_solve || fail 1 "wp_send: protocol not of the shape <!>"
+ |done || fail 1 "wp_send: protocol not of the shape <!>"
+ (* |tc_solve || fail 1 "wp_send: protocol not of the shape <!>" *)
|tc_solve || fail 1 "wp_send: cannot convert to telescope"
|pm_reduce; simpl; tac_exist;
repeat lazymatch goal with
diff --git a/multris/channel/proto.v b/multris/channel/proto.v
index 8849b59..67501de 100644
--- a/multris/channel/proto.v
+++ b/multris/channel/proto.v
@@ -138,7 +138,7 @@ Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m)
(at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
format "< a @.. x1 .. xn > m") : proto_scope.
-Infix "<+>'" := iProto_union (at level 20) : proto_scope.
+Infix "<+>" := iProto_union (at level 20) : proto_scope.
Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
(tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
@@ -217,8 +217,15 @@ Qed.
Lemma proto_elim_union {V} `{!Cofe PROPn, !Cofe PROP} {A : ofe}
(x y : A) (f : A → action → (V → laterO (proto V PROP PROPn) -n> PROP) → A) p1 p2 :
(Proper ((≡) ==> (=) ==> (pointwise_relation _ (≡)) ==> (≡)) f) →
+ p1 ≠[] → p2 ≠[] →
proto_elim x y f (proto_union p1 p2) ≡ proto_elim x (proto_elim x y f p1) f p2 .
-Proof. Admitted.
+Proof.
+ intros Hf Hp1 Hp2. rewrite /proto_elim /proto_message /=.
+ rewrite /proto_union.
+ destruct p1, p2=> /=; try done.
+ rewrite fold_left_app.
+ solve_proper.
+Qed.
Program Definition iProto_map_app_aux {Σ V}
(f : action → action)
@@ -290,18 +297,9 @@ Section proto.
(** ** Equality *)
Lemma iProto_case p : p ≡ END ∨ ∃ t n m ps, p ≡ proto_union (iProto_message (t, n) m) ps.
Proof.
- (* rewrite iProto_end_eq. destruct p. left. done. right. *)
- (* eexists _, (IMsg <$> p). done. *)
- (* done. done. *)
destruct (proto_case p) as [|([t n] & m & ps & Hps)]; [left; by rewrite iProto_end_eq|].
right. exists t, n, (IMsg m), ps. rewrite iProto_message_eq. done.
Qed.
- (* 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]. *)
- (* 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).
@@ -481,44 +479,65 @@ Section proto.
intros p1 p2 Hp a1 a2 Ha m1 m2 Hm. f_equiv; [|solve_proper].
f_equiv; [done|]. solve_proper.
Qed.
- Lemma iProto_app_union p1 p2 p :
- p1 ≠END → p2 ≠END →
- (proto_union p1 p2) <++> p ≡ proto_union (p1 <++> p) (p2 <++> p).
- Proof. Admitted.
- (* rewrite iProto_app_eq /iProto_app_def /iProto_map_app. *)
+ (* Lemma iProto_app_union p1 p2 p : *)
+ (* p1 ≠END → p2 ≠END → *)
+ (* (proto_union p1 p2) <++> p ≡ proto_union (p1 <++> p) (p2 <++> p). *)
+ (* Proof. *)
+ (* intros Hp1 Hp2. *)
+ (* rewrite !iProto_app_unfold. *)
(* (* rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app. *) *)
- (* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]. *)
- (* simpl. *)
- (* rewrite ->proto_elim_union. *)
- (* { rewrite /proto_elim. induction p2; [simpl|]. *)
- (* { rewrite /proto_union. } *)
- (* intros p1' p2' Hp a1 a2 Ha m1 m2 Hm. f_equiv; [|solve_proper]. *)
- (* f_equiv; [done|]. solve_proper. *)
- (* Qed. *)
+ (* (* etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]. *) *)
+ (* rewrite iProto_end_eq in Hp1,Hp2. *)
+ (* rewrite /iProto_end_def in Hp1,Hp2. *)
+ (* rewrite /proto_end in Hp1,Hp2. *)
+ (* simpl in *. *)
+ (* rewrite ->proto_elim_union; [| |done|done]; last first. *)
+ (* { intros p1' p2' Hp a1 a2 Ha m1 m2 Hm. f_equiv; [|solve_proper]. *)
+ (* f_equiv; [done|]. solve_proper. } *)
+ (* rewrite /proto_union. *)
+ (* induction p1. *)
+ (* { simpl. done. } *)
+ (* destruct p1; [simpl|]. *)
+ (* Admitted. *)
- 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.
- Admitted.
+ (* 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. *)
+ (* Admitted. *)
(* 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.
+ (* 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.
+ (* 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&ps&->)]. *)
+ (* { 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_end_r : RightId (≡) END (@iProto_app Σ V). *)
(* Proof. *)
@@ -583,6 +602,14 @@ Definition can_step {Σ V} (rec : list (iProto Σ V) → iProp Σ)
Definition valid_target {Σ V} (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
∀ a m, (ps !!! i ≡ (<(a, j)> m)) -∗ ⌜is_Some (ps !! j)âŒ.
+Global Instance valid_target_ne {Σ V} n :
+ Proper ((dist n) ==> (=) ==> (=) ==> (dist n)) (valid_target (Σ:=Σ) (V:=V)).
+Proof. rewrite /valid_target. intros ps1 ps2 Hs ??-> ??->. do 6 f_equiv; by rewrite Hs. Qed.
+
+Global Instance valid_target_proper {Σ V} :
+ Proper ((≡) ==> (=) ==> (=) ==> (≡)) (valid_target (Σ:=Σ) (V:=V)).
+Proof. rewrite /valid_target. intros ps1 ps2 Hs ??-> ??->. do 6 f_equiv; by rewrite Hs. Qed.
+
Definition iProto_consistent_pre {Σ V} (rec : list (iProto Σ V) → iProp Σ)
(ps : list (iProto Σ V)) : iProp Σ :=
(∀ i j, valid_target ps i j) ∗ (∀ i j, can_step rec ps i j).
@@ -620,43 +647,79 @@ Proof.
apply: (fixpoint_unfold iProto_consistent_pre').
Qed.
-(* (** * Protocol entailment *) *)
+(** * 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. *)
+(* (rec : iProto Σ V → iProto Σ V → iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ := *)
+(* match p1, p2 with *)
+(* | [], [] => p1 ≡ END ∗ p2 ≡ END *)
+(* | p1::ps1, p2::ps2 => *)
+(* (∃ 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) *)
+(* | _ , _ => False *)
+(* end. *)
+
+(* Fixpoint iProto_le_pre {Σ V} *)
+(* (rec : iProto Σ V → iProto Σ V → iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ := *)
+(* match p1, p2 with *)
+(* | [], [] => p1 ≡ END ∗ p2 ≡ END *)
+(* | p1::ps1, p2::ps2 => *)
+(* (∃ 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) ∗ iProto_le_pre rec ps1 ps2 *)
+(* | _ , _ => False *)
+(* end. *)
+
+(** * 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) ∨
+ (p1 ≡ p2).
+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 :=
@@ -684,7 +747,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 Σ :=
- iProto_own_frag γ i p.
+ ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ i p'.
Arguments iProto_own {_ _ _} _ _ _%_proto.
Global Instance: Params (@iProto_own) 3 := {}.
@@ -726,195 +789,258 @@ 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_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 /iProto_le_pre !iProto_end_eq=> /=.
+ iLeft. done.
+ 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 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. iLeft. iExists (Send, i), (Send, i), m1, m2. by eauto.
+ 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 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. iLeft. iExists (Recv, i), (Recv, i), m1, m2. by eauto.
+ Qed.
+
+ Lemma iProto_le_refl p : ⊢ p ⊑ p.
+ Proof.
+ iLöb as "IH" forall (p). rewrite iProto_le_unfold. iRight. iRight. done.
+ 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_end_inv_r p : p ⊑ END -∗ (p ≡ END).
+ Proof.
+ rewrite iProto_le_unfold.
+ iIntros "[[Hp _]|[H|H]] //".
+ iDestruct "H" as (a1 a2 m1 m2) "(_ & Heq & _)".
+ by iDestruct (iProto_end_message_equivI with "Heq") as %[].
+ 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_end_inv_l p : END ⊑ p -∗ (p ≡ END).
+ Proof.
+ rewrite iProto_le_unfold. iIntros "[[_ Hp]|[H|H]] //"; [|by iRewrite "H"].
+ iDestruct "H" as (a1 a2 m1 m2) "(Heq & _ & _)".
+ iDestruct (iProto_end_message_equivI with "Heq") as %[].
+ 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_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|H]]".
+ { by iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ 2: { iExists _. iFrame. iIntros (??) "?". iExists _. iFrame. iApply iProto_le_refl. }
+ 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_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_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_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_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|H]]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ 2: { iExists _. iRewrite -"H". iSplit; [done|].
+ iIntros (??) "?". iExists _. iFrame. iApply iProto_le_refl. }
+ 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 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_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|H]]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ 2: { iExists _. iFrame. iIntros (??) "?". iExists _. iFrame. iApply iProto_le_refl. }
+ 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_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_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_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_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|H]]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ 2: { iExists _. iRewrite -"H". done. }
+ 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_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_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|H]]".
+ { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
+ 2: { iExists _. iRewrite "H". done. }
+ 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_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_union_inv_l a m p1 p2:
+ proto_union (<a>m) p1 ⊑ p2 -∗ (p1 ≡ END) ∨ (p2 ≡ proto_union (<a>m) p1).
+ Proof.
+ iIntros "Hle".
+ destruct p1; [iLeft|iRight].
+ { by rewrite iProto_end_eq. }
+ rewrite iProto_le_unfold /iProto_le_pre.
+ iDestruct "Hle" as "[Hle|[Hle|Hle]]".
+ - iDestruct "Hle" as "[Hend _]".
+ rewrite /proto_union iProto_end_eq /iProto_end_def /proto_end. simpl in *.
+ rewrite list_equivI.
+ iSpecialize ("Hend" $!0).
+ simpl. rewrite option_equivI.
+ rewrite iProto_message_eq. simpl. done.
+ - iDestruct "Hle" as (a1 a2 m1 m2) "[Hmsg _]".
+ rewrite /proto_union.
+ rewrite list_equivI.
+ iSpecialize ("Hmsg" $!1).
+ simpl. rewrite option_equivI.
+ rewrite iProto_message_eq. simpl. done.
+ - by iRewrite "Hle".
+ Qed.
+ Lemma iProto_le_union_inv_r a m p1 p2:
+ p1 ⊑ proto_union (<a>m) p2 -∗ (p2 ≡ END) ∨ (p1 ≡ proto_union (<a>m) p2).
+ Proof.
+ iIntros "Hle".
+ destruct p2; [iLeft|iRight].
+ { by rewrite iProto_end_eq. }
+ rewrite iProto_le_unfold /iProto_le_pre.
+ iDestruct "Hle" as "[Hle|[Hle|Hle]]".
+ - iDestruct "Hle" as "[_ Hend]".
+ rewrite /proto_union iProto_end_eq /iProto_end_def /proto_end. simpl in *.
+ rewrite list_equivI.
+ iSpecialize ("Hend" $!0).
+ simpl. rewrite option_equivI.
+ rewrite iProto_message_eq. simpl. done.
+ - iDestruct "Hle" as (a1 a2 m1 m2) "[_ [Hmsg _]]".
+ rewrite /proto_union.
+ rewrite list_equivI.
+ iSpecialize ("Hmsg" $!1).
+ simpl. rewrite option_equivI.
+ rewrite iProto_message_eq. simpl. done.
+ - by iRewrite "Hle".
+ 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 [->|([]&n&m&ps&->)].
+ - iDestruct (iProto_le_end_inv_r with "H2") as "H2". by iRewrite "H2" in "H1".
+ -
+ iDestruct (iProto_le_union_inv_r with "H2") as "#[Heq|Heq]"; last first.
+ { by iRewrite -"Heq". }
+ iRewrite "Heq" in "H2".
+ iRewrite "Heq".
+ rewrite !/proto_union iProto_end_eq right_id.
+ 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_union_inv_r with "H2") as "#[Heq|Heq]"; last first.
+ { by iRewrite -"Heq". }
+ iRewrite "Heq" in "H2".
+ iRewrite "Heq".
+ rewrite !/proto_union iProto_end_eq right_id.
+ 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.
+
Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
Proof. solve_proper. Qed.
@@ -984,7 +1110,7 @@ Section proto.
rewrite right_id_L.
rewrite -fmap_insert. iFrame.
rewrite /iProto_own_auth.
- rewrite map_seq_snoc. simpl. done.
+ rewrite map_seq_snoc. simpl. iFrame. iApply iProto_le_refl.
Qed.
Lemma list_lookup_Some_le (ps : list $ iProto Σ V) (i : nat) (p1 : iProto Σ V) :
@@ -997,6 +1123,311 @@ Section proto.
by apply lookup_lt_is_Some_1.
Qed.
+ (* Lemma list_lookup_id (ps : list $ iProto Σ V) (i : nat) (p1 : iProto Σ V) : *)
+ (* ⊢@{iProp Σ} ps !! i ≡ Some p1 -∗ ⌜ps = <[i := p1]> ps âŒ. *)
+ (* Proof. *)
+ (* iIntros "HSome". *)
+ (* rewrite option_equivI. *)
+ (* destruct (ps !! i) eqn:Heqn; [|done]. *)
+ (* iPureIntro. *)
+ (* rewrite list_insert_id. *)
+ (* Qed. *)
+
+ (* Lemma list_insert_id {A:ofe} (l : list A) i (x:A) : l !! i ≡ Some x → <[i:=x]>l ≡ l. *)
+ (* Proof. intros ?. *)
+ (* rewrite list_equivI. *)
+ (* apply option_equivI in H. *)
+ (* rewrite list_insert_id; [done|]. *)
+
+ (* by apply list_insert_id'. 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 & ps' & Hmsg).
+ setoid_rewrite Hmsg.
+ iDestruct (iProto_le_union_inv_l with "Hle") as "#[H|H]"; last first.
+ { iRewrite -"H". iRewrite -"H" in "Hle". iRewrite -"H" in "HSome". iFrame.
+ (* OBS: Breaking abstraction here; need more lemmas about [valid_target] *)
+ iAssert (<[i := p2]>ps ≡ ps)%I as "Heq".
+ { rewrite list_equivI.
+ rewrite option_equivI.
+ iIntros (j). destruct (decide (i = j)) as [->|Hneq].
+ - rewrite list_lookup_insert; [|done].
+ destruct (ps !! j); [|done]. by iRewrite "HSome".
+ - by rewrite list_lookup_insert_ne. }
+ iIntros (??). iSpecialize ("Hprot" $! i' j'). iRewrite "Heq". done. }
+ iRewrite "H". iRewrite "H" in "HSome". iRewrite "H" in "Hle".
+ rewrite /proto_union iProto_end_eq. rewrite right_id.
+ 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&ps'&Hmsg).
+ setoid_rewrite Hmsg.
+ destruct a; last first.
+ { rewrite !option_equivI.
+ iDestruct (iProto_le_union_inv_r with "Hle") as "[Heq|Heq]".
+ { iRewrite "Heq" in "Hm1".
+ rewrite /proto_union iProto_end_eq right_id.
+ rewrite iProto_message_equivI.
+ iDestruct "Hm1" as "[%Htag Hm1]". done. }
+ rewrite /proto_union.
+ destruct ps'.
+ { rewrite right_id.
+ rewrite iProto_message_equivI.
+ iDestruct "Hm1" as "[%Htag Hm1]". done. }
+ (* TODO: Clean up *)
+ rewrite list_equivI.
+ iSpecialize ("Hm1" $!0).
+ rewrite iProto_message_eq. simpl. rewrite option_equivI.
+ rewrite prod_equivI. iDestruct "Hm1" as "[%Hm1 _]".
+ simpl in *. done. }
+ iAssert (ps' ≡ END)%I as "#Heq'".
+ { (* TODO: Clean up *)
+ rewrite /proto_union. rewrite iProto_end_eq. destruct ps'; [done|].
+ rewrite list_equivI.
+ iSpecialize ("Hm1" $!1).
+ rewrite iProto_message_eq.
+ by rewrite !option_equivI. }
+ iRewrite "Heq'" in "Hm1". rewrite /proto_union iProto_end_eq right_id.
+ iRewrite "Heq'" in "Hle". rewrite right_id.
+ iRewrite "Heq'" in "Hm2". rewrite right_id.
+ 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&ps'&Hmsg).
+ setoid_rewrite Hmsg.
+ destruct a.
+ { rewrite !option_equivI.
+ iDestruct (iProto_le_union_inv_r with "Hle") as "[Heq|Heq]".
+ { iRewrite "Heq" in "Hm2".
+ rewrite /proto_union iProto_end_eq right_id.
+ rewrite iProto_message_equivI.
+ iDestruct "Hm2" as "[%Htag Hm2]". done. }
+ rewrite /proto_union.
+ destruct ps'.
+ { rewrite right_id.
+ rewrite iProto_message_equivI.
+ iDestruct "Hm2" as "[%Htag Hm2]". done. }
+ (* TODO: Clean up *)
+ rewrite !list_equivI.
+ iSpecialize ("Hm2" $!0).
+ rewrite iProto_message_eq. simpl. rewrite option_equivI.
+ rewrite prod_equivI. iDestruct "Hm2" as "[%Hm2 _]".
+ simpl in *. done. }
+ iAssert (ps' ≡ END)%I as "#Heq'".
+ { (* TODO: Clean up *)
+ rewrite /proto_union. rewrite iProto_end_eq. destruct ps'; [done|].
+ rewrite !list_equivI.
+ iSpecialize ("Hm2" $!1).
+ rewrite iProto_message_eq.
+ by rewrite !option_equivI. }
+ iRewrite "Heq'" in "Hm2". rewrite /proto_union iProto_end_eq right_id.
+ iRewrite "Heq'" in "Hle". rewrite right_id.
+ 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_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) -∗
@@ -1024,10 +1455,19 @@ 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. iIntros "Hp1 Hp2".
+ rewrite /iProto_own.
+ iDestruct 1 as (p1') "[_ Hp1]".
+ iDestruct 1 as (p2') "[_ Hp2]".
iDestruct (own_prot_excl with "Hp1 Hp2") as %[].
Qed.
@@ -1039,6 +1479,7 @@ 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.
@@ -1064,35 +1505,45 @@ 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 Hpi Hpj [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 [] [] [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. }
- iFrame.
+ 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.
Qed.
Lemma iProto_target γ ps_dom i a j m :
@@ -1103,88 +1554,89 @@ 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 Hi") as "#H".
+ 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. }
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. *)
+ (* (** 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_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_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. *)
+ 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.
diff --git a/multris/examples/basics.v b/multris/examples/basics.v
index 53ad44a..70ee013 100644
--- a/multris/examples/basics.v
+++ b/multris/examples/basics.v
@@ -203,13 +203,18 @@ Section roundtrip_ref_rec.
as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
wp_smart_apply (wp_fork with "[Hc1]").
{ iIntros "!>". wp_pure _. iLöb as "IH".
+ rewrite {2}iProto_roundtrip_ref_rec2_unfold. rewrite /iProto_roundtrip_ref_rec2_aux.
wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
do 2 wp_pure _. by iApply "IH". }
wp_smart_apply (wp_fork with "[Hc2]").
{ iIntros "!>". wp_pure _. iLöb as "IH".
+ rewrite {2}iProto_roundtrip_ref_rec3_unfold. rewrite /iProto_roundtrip_ref_rec3_aux.
wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
do 2 wp_pure _. by iApply "IH". }
- wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl".
+ wp_alloc l as "Hl".
+ rewrite iProto_roundtrip_ref_rec1_unfold. rewrite /iProto_roundtrip_ref_rec1_aux.
+ wp_send with "[$Hl]". wp_recv as "Hl".
+ rewrite iProto_roundtrip_ref_rec1_unfold. rewrite /iProto_roundtrip_ref_rec1_aux.
wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
by iApply "HΦ".
Qed.
@@ -407,7 +412,7 @@ Section forwarder_rec.
iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
iNext.
iEval (rewrite iProto_forwarder_rec_1_unfold).
- iEval (rewrite iProto_forwarder_rec_n_unfold).
+ iEval (rewrite {2}iProto_forwarder_rec_n_unfold).
iProto_consistent_take_step.
iIntros "_". iSplit; [done|]. iSplit; [done|].
iEval (rewrite -iProto_forwarder_rec_1_unfold).
--
GitLab