diff --git a/_CoqProject b/_CoqProject
index 4489ccb2876733d2156d6e1c85882966758f62ea..496c210bafd16545c1169b4bf22789ac8fcb2f9a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -61,3 +61,4 @@ multi_actris/channel/proto.v
multi_actris/channel/channel.v
multi_actris/channel/proofmode.v
multi_actris/examples/basics.v
+multi_actris/examples/leader_election.v
diff --git a/multi_actris/channel/channel.v b/multi_actris/channel/channel.v
index 89937a2550979a790b45293561e19769fcebf966..11c498bcd9e20d10594e75f0d081d2e0c8376ae0 100644
--- a/multi_actris/channel/channel.v
+++ b/multi_actris/channel/channel.v
@@ -93,23 +93,21 @@ Definition tok `{!chanG Σ} (γ : gname) : iProp Σ := own γ (Excl ()).
Definition chan_inv `{!heapGS Σ, !chanG Σ} γ γE γt i j (l:loc) : iProp Σ :=
(l ↦ NONEV ∗ tok γt)%I ∨
- (∃ v m, l ↦ SOMEV v ∗
+ (∃ v m p, l ↦ SOMEV v ∗
iProto_own γ i (<(Send, j)> m)%proto ∗
- (∃ p, iMsg_car m v (Next p) ∗ own γE (â—E (Next p)))) ∨
+ iMsg_car m v (Next p) ∗ own γE (â—E (Next p))) ∨
(∃ p, l ↦ NONEV ∗
iProto_own γ i p ∗ own γE (â—E (Next p))).
Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
(c : val) (p : iProto Σ) : iProp Σ :=
- ∃ γ γE1 (l:loc) (i:nat) (n:nat) p',
+ ∃ γ (γEs : list gname) (l:loc) (i:nat) (n:nat) p',
⌜ c = (#l,#n,#i)%V ⌠∗
- inv (nroot.@"ctx") (iProto_ctx γ (set_seq 0 n)) ∗
- ([∗list] j ↦ _ ∈ replicate n (),
- ∃ γE2 γt1 γt2,
- inv (nroot.@"p") (chan_inv γ γE1 γt1 i j (l +ₗ (pos n i j))) ∗
- inv (nroot.@"p") (chan_inv γ γE2 γt2 j i (l +ₗ (pos n j i)))) ∗
+ inv (nroot.@"ctx") (iProto_ctx γ n) ∗
+ (∀ i j, ⌜i < n ⌠-∗ ⌜j < n⌠-∗
+ ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j (l +ₗ (pos n i j)))) ∗
▷ (p' ⊑ p) ∗
- own γE1 (â—E (Next p')) ∗ own γE1 (â—¯E (Next 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).
@@ -121,19 +119,17 @@ Notation "c ↣ p" := (iProto_pointsto c p)
(at level 20, format "c ↣ p").
Definition chan_pool `{!heapGS Σ, !chanG Σ}
- (cs : val) (ps : gmap nat (iProto Σ)) : iProp Σ :=
- ∃ γ (γEs : list gname) (l:loc) (n:nat),
- ⌜cs = (#l,#n)%V⌠∗ ⌜∀ i, is_Some (ps !! i) → i < n⌠∗
- inv (nroot.@"ctx") (iProto_ctx γ (set_seq 0 n)) ∗
+ (cs : val) (i':nat) (ps : list (iProto Σ)) : iProp Σ :=
+ ∃ γ (γEs : list gname) (n:nat) (l:loc),
+ ⌜cs = (#l,#n)%V⌠∗ ⌜(i' + length ps = n)%nat⌠∗
+ inv (nroot.@"ctx") (iProto_ctx γ n) ∗
+ (∀ i j, ⌜i < n ⌠-∗ ⌜j < n⌠-∗
+ ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j (l +ₗ (pos n i j)))) ∗
[∗ list] i ↦ _ ∈ replicate n (),
- (∀ p, ⌜ps !! i = Some p⌠-∗
+ (∀ p, ⌜i' <= i⌠-∗ ⌜ps !! (i - i') = Some p⌠-∗
own (γEs !!! i) (â—E (Next p)) ∗
own (γEs !!! i) (◯E (Next p)) ∗
- iProto_own γ i p) ∗
- [∗ list] j ↦ _ ∈ replicate n (),
- ∃ γt1 γt2,
- inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt1 i j (l +ₗ (pos n i j))) ∗
- inv (nroot.@"p") (chan_inv γ (γEs !!! j) γt2 j i (l +ₗ (pos n j i))).
+ iProto_own γ i p).
Section channel.
Context `{!heapGS Σ, !chanG Σ}.
@@ -203,63 +199,53 @@ Section channel.
Qed.
(** ** Specifications of [send] and [recv] *)
- Lemma new_chan_spec (n:nat) (ps:gmap nat (iProto Σ)) :
- 0 < n →
- dom ps = set_seq 0 n →
+ Lemma new_chan_spec (ps:list (iProto Σ)) :
+ 0 < length ps →
{{{ iProto_consistent ps }}}
- new_chan #n
- {{{ cs, RET cs; chan_pool cs ps }}}.
+ new_chan #(length ps)
+ {{{ cs, RET cs; chan_pool cs 0 ps }}}.
Proof.
- iIntros (Hle Hdom Φ) "Hps HΦ". wp_lam.
+ iIntros (Hle Φ) "Hps HΦ". wp_lam.
wp_smart_apply wp_allocN; [lia|done|].
iIntros (l) "[Hl _]".
iMod (iProto_init with "Hps") as (γ) "[Hps Hps']".
wp_pures. iApply "HΦ".
iAssert (|==> ∃ (γEs : list gname),
- ⌜length γEs = n⌠∗
- [∗ list] i ↦ _ ∈ replicate n (),
+ ⌜length γEs = length ps⌠∗
+ [∗ list] i ↦ _ ∈ replicate (length ps) (),
own (γEs !!! i) (â—E (Next (ps !!! i))) ∗
own (γEs !!! i) (◯E (Next (ps !!! i))) ∗
iProto_own γ i (ps !!! i))%I with "[Hps']" as "H".
{ clear Hle.
- iInduction n as [|n] "IHn" forall (ps Hdom).
+ iInduction ps as [|p ps] "IHn" using rev_ind.
{ iExists []. iModIntro. simpl. done. }
- assert (is_Some (ps !! n)) as [p HSome].
- { apply elem_of_dom. rewrite Hdom. apply elem_of_set_seq. lia. }
- iDestruct (big_sepM_delete _ _ n with "Hps'") as "[Hp Hps']"; [done|].
+ iDestruct "Hps'" as "[Hps' Hp]".
iMod (own_alloc (â—E (Next p) â‹… â—¯E (Next p))) as (γE) "[Hauth Hfrag]".
{ apply excl_auth_valid. }
- iMod ("IHn" with "[] Hps'") as (γEs Hlen) "H".
- { iPureIntro.
- rewrite dom_delete_L Hdom.
- replace (S n) with (n + 1) by lia.
- rewrite set_seq_add_L /= right_id_L difference_union_distr_l_L
- difference_diag_L right_id_L.
- assert (n ∉ (set_seq 0 n:gset _)); [|set_solver].
- intros Hin%elem_of_set_seq. lia. }
+ iMod ("IHn" with "Hps'") as (γEs Hlen) "H".
iModIntro. iExists (γEs++[γE]).
- replace (S n) with (n + 1) by lia.
- rewrite replicate_add big_sepL_app app_length Hlen.
- iSplit; [done|]=> /=.
+ rewrite !app_length Hlen.
+ iSplit; [iPureIntro=>/=;lia|]=> /=.
+ rewrite replicate_add.
iSplitL "H".
{ iApply (big_sepL_impl with "H").
iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
- assert (i < n) as Hle.
+ assert (i < length ps) as Hle.
{ by apply lookup_replicate_1 in HSome' as [??]. }
- assert (delete n ps !!! i = ps !!! i) as Heq'.
- { apply lookup_total_delete_ne. lia. }
- rewrite Heq'. iFrame.
- rewrite lookup_total_app_l; [|lia]. iFrame. }
+ rewrite !lookup_total_app_l; [|lia..]. iFrame. }
rewrite replicate_length Nat.add_0_r.
- rewrite list_lookup_total_middle; [|done].
- rewrite lookup_total_alt HSome. by iFrame. }
+ simpl. rewrite right_id_L.
+ rewrite !lookup_total_app_r; [|lia..]. rewrite !Hlen.
+ rewrite Nat.sub_diag. simpl. iFrame.
+ iDestruct "Hp" as "[$ _]". }
iMod "H" as (γEs Hlen) "H".
+ set n := length ps.
iAssert (|={⊤}=>
- [∗ list] i ↦ _ ∈ replicate n (),
- [∗ list] j ↦ _ ∈ replicate n (),
+ [∗ list] i ↦ _ ∈ replicate (length ps) (),
+ [∗ list] j ↦ _ ∈ replicate (length ps) (),
∃ γt,
inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j
- (l +â‚— (pos n i j))))%I with "[Hl]" as "IH".
+ (l +â‚— (pos (length ps) i j))))%I with "[Hl]" as "IH".
{ replace (Z.to_nat (Z.of_nat n * Z.of_nat n)) with (n*n) by lia.
iDestruct (array_to_matrix with "Hl") as "Hl".
iApply big_sepL_fupd.
@@ -273,72 +259,77 @@ Section channel.
iMod "IH" as "#IH".
iMod (inv_alloc with "Hps") as "#IHp".
iExists _,_,_,_.
- iModIntro. iSplit; [done|].
+ iModIntro.
+ iSplit.
+ { iPureIntro. done. }
iSplit.
- { iPureIntro. intros i HSome.
- apply elem_of_dom in HSome.
- rewrite Hdom in HSome.
- apply elem_of_set_seq in HSome. lia. }
- rewrite Hdom. iFrame "IHp".
+ { done. }
+ iFrame "IHp".
+ iSplit.
+ { iIntros (i j Hi Hj).
+ rewrite (big_sepL_lookup _ _ i); [|by rewrite lookup_replicate].
+ rewrite (big_sepL_lookup _ _ j); [|by rewrite lookup_replicate].
+ iApply "IH". }
iApply (big_sepL_impl with "H").
iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
- iSplitL.
- { iIntros (p HSome'').
- rewrite lookup_total_alt. rewrite HSome''.
- iFrame. }
- iApply big_sepL_intro.
- iIntros "!>" (j ? HSome'').
- assert (i < n) as Hle'.
- { apply lookup_replicate in HSome' as [_ Hle']. done. }
- assert (j < n) as Hle''.
- { apply lookup_replicate in HSome'' as [_ Hle'']. done. }
- iDestruct (big_sepL_lookup _ _ i () with "IH") as "IH'";
- [by rewrite lookup_replicate|].
- iDestruct (big_sepL_lookup _ _ j () with "IH'") as "IH''";
- [by rewrite lookup_replicate|].
- iDestruct (big_sepL_lookup _ _ j () with "IH") as "H";
- [by rewrite lookup_replicate|].
- iDestruct (big_sepL_lookup _ _ i () with "H") as "H'";
- [by rewrite lookup_replicate|].
- iDestruct "IH''" as (γ1) "?".
- iDestruct "H'" as (γ2) "?".
- iExists _, _. iFrame "#".
+ iIntros (p Hle' HSome'').
+ iFrame. rewrite right_id_L in HSome''.
+ rewrite (list_lookup_total_alt ps).
+ rewrite HSome''. simpl. iFrame.
Qed.
- Lemma get_chan_spec cs (i:nat) ps p :
- ps !! i = Some p →
- {{{ chan_pool cs ps }}}
+ Lemma get_chan_spec cs i ps p :
+ {{{ chan_pool cs i (p::ps) }}}
get_chan cs #i
- {{{ c, RET c; c ↣ p ∗ chan_pool cs (delete i ps) }}}.
+ {{{ c, RET c; c ↣ p ∗ chan_pool cs (i+1) ps }}}.
Proof.
- iIntros (HSome Φ) "Hcs HΦ".
- iDestruct "Hcs" as (γp γEs l n -> Hle) "[#IHp Hl]".
- wp_lam. wp_pures.
- assert (i < n); [by apply Hle|].
- iDestruct (big_sepL_delete _ _ i () with "Hl") as "[[Hi #IHs] H]";
- [by apply lookup_replicate|].
- iDestruct ("Hi" with "[//]") as "(Hauth & Hown & Hp)".
+ iIntros (Φ) "Hcs HΦ".
+ iDestruct "Hcs" as (γp γEs n l -> <-) "(#IHp & #IHl & Hl)".
+ wp_lam. wp_pures.
+ rewrite replicate_add. simpl.
+ iDestruct "Hl" as "[Hl1 [Hi Hl3]]".
+ iDestruct ("Hi" with "[] []") as "(Hauth & Hown & Hp)".
+ { rewrite right_id_L. rewrite replicate_length. iPureIntro. lia. }
+ { rewrite right_id_L. rewrite replicate_length.
+ rewrite Nat.sub_diag. simpl. done. }
iModIntro.
iApply "HΦ".
- iSplitR "H".
+ iSplitR "Hl1 Hl3".
{ rewrite iProto_pointsto_eq. iExists _, _, _, _, _, _.
- iSplit; [done|]. iFrame "#∗". iSplit; [|iNext; done].
- iApply (big_sepL_impl with "IHs").
- iIntros "!>" (???). iDestruct 1 as (γt1 γt2) "[??]".
- iExists _,_,_. iFrame. }
- iExists _, _, _, _. iSplit; [done|].
+ iSplit; [done|].
+ rewrite replicate_length. rewrite right_id_L.
+ iFrame. iFrame "#∗". iNext. done. }
+ iExists γp, γEs, _, _. iSplit; [done|].
iSplit.
- { iPureIntro. intros i' HSome'. apply Hle.
- assert (i ≠i').
- { intros ->. rewrite lookup_delete in HSome'. by inversion HSome'. }
- by rewrite lookup_delete_ne in HSome'. }
+ { iPureIntro. lia. }
+ iFrame. iFrame "#∗".
+ rewrite replicate_add.
+ simpl.
+ iSplitL "Hl1".
+ { iApply (big_sepL_impl with "Hl1").
+ iIntros "!>" (i' ? HSome'').
+ assert (i' < i).
+ { rewrite lookup_replicate in HSome''. lia. }
+ iIntros "H" (p' Hle'). lia. }
+ simpl.
iFrame "#∗".
- iApply (big_sepL_impl with "H").
+ iSplitR.
+ { iIntros (p' Hle'). rewrite right_id_L in Hle'.
+ rewrite replicate_length in Hle'. lia. }
+ iApply (big_sepL_impl with "Hl3").
iIntros "!>" (i' ? HSome'').
- case_decide.
- { simplify_eq. iFrame "#".
- iIntros "_" (p' Hin). simplify_eq. by rewrite lookup_delete in Hin. }
- rewrite lookup_delete_ne; [|done]. by eauto.
+ assert (i' < length ps).
+ { rewrite lookup_replicate in HSome''. lia. }
+ iIntros "H" (p' Hle' HSome).
+ iApply "H".
+ { iPureIntro. lia. }
+ iPureIntro.
+ rewrite replicate_length.
+ rewrite replicate_length in HSome.
+ replace (i + S i' - i) with (S i') by lia.
+ simpl.
+ replace (i + S i' - (i+1)) with (i') in HSome by lia.
+ done.
Qed.
Lemma vpos_spec (n i j : nat) :
@@ -359,44 +350,42 @@ Section channel.
iDestruct "Hc" as
(γ γE l i n p' ->) "(#IH & #Hls & Hle & H◠& H◯ & Hown)".
wp_bind (Fst _).
- iInv "IH" as "HI".
+ iInv "IH" as "Hctx".
iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
iRewrite "Heq" in "Hown".
+ iAssert (▷ (⌜i < n⌠∗ iProto_own γ i (<(Send, j)> m') ∗
+ iProto_ctx γ n))%I with "[Hctx Hown]"
+ as "[Hi [Hown Hctx]]".
+ { iNext. iDestruct (iProto_ctx_agree with "Hctx Hown") as %Hi.
+ iFrame. done. }
iAssert (▷ (▷ ⌜j < n⌠∗ iProto_own γ i (<(Send, j)> m') ∗
- iProto_ctx γ (set_seq 0 n)))%I with "[HI Hown]"
- as "[HI [Hown Hctx]]".
- { iNext. iDestruct (iProto_target with "HI Hown") as "[Hin [$ $]]".
- iFrame. iNext. iDestruct "Hin" as %Hin. by set_solver. }
+ iProto_ctx γ n))%I with "[Hctx Hown]"
+ as "[Hj [Hown Hctx]]".
+ { iNext. iDestruct (iProto_target with "Hctx Hown") as "[Hin [$ $]]".
+ iFrame. }
iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
wp_smart_apply (vpos_spec); [done|]; iIntros "_".
- iDestruct "HI" as %Hle.
- iDestruct (big_sepL_lookup_acc with "Hls") as "[Hj _]";
- [by apply lookup_replicate_2|].
- iDestruct "Hj" as (γE' γt γt') "#[IHl1 IHl2]".
+ iDestruct "Hi" as %Hi.
+ iDestruct "Hj" as %Hj.
+ iDestruct ("Hls" $! i j with "[//] [//]") as (γt) "IHl1".
wp_pures. wp_bind (Store _ _).
iInv "IHl1" as "HIp".
iDestruct "HIp" as "[HIp|HIp]"; last first.
{ iDestruct "HIp" as "[HIp|HIp]".
- - iDestruct "HIp" as (? m) "(>Hl & Hown' & HIp)".
+ - iDestruct "HIp" as (? m p'') "(>Hl & Hown' & HIp)".
wp_store.
- rewrite /iProto_own.
- iDestruct "Hown" as (p'') "[Hle' Hown]".
- iDestruct "Hown'" as (p''') "[Hle'' Hown']".
- iDestruct (own_prot_excl with "Hown Hown'") as "H". done.
+ iDestruct (iProto_own_excl with "Hown Hown'") as %[].
- iDestruct "HIp" as (p'') "(>Hl' & Hown' & HIp)".
wp_store.
- rewrite /iProto_own.
- iDestruct "Hown" as (p''') "[Hle' Hown]".
- iDestruct "Hown'" as (p'''') "[Hle'' Hown']".
- iDestruct (own_prot_excl with "Hown Hown'") as "H". done. }
+ iDestruct (iProto_own_excl with "Hown Hown'") as %[]. }
iDestruct "HIp" as "[>Hl' Htok]".
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.
+ { iRight. iLeft. iIntros "!>". iExists _, _, _. iFrame.
iSplitL "Hown Hle"; [by iApply (iProto_own_le with "Hown Hle")|].
- iExists _. iFrame. by rewrite iMsg_base_eq. }
+ by rewrite iMsg_base_eq. }
wp_pures.
iLöb as "HL".
wp_lam.
@@ -406,10 +395,10 @@ Section channel.
{ iDestruct "HIp" as ">[Hl' Htok']".
iDestruct (own_valid_2 with "Htok Htok'") as %[]. }
iDestruct "HIp" as "[HIp|HIp]".
- - iDestruct "HIp" as (? m) "(>Hl' & Hown & HIp)".
+ - iDestruct "HIp" as (? m p'') "(>Hl' & Hown & HIp)".
wp_load. iModIntro.
iSplitL "Hl' Hown HIp".
- { iRight. iLeft. iExists _, _. iFrame. }
+ { iRight. iLeft. iExists _, _,_. iFrame. }
wp_pures. iApply ("HL" with "HΦ Htok H◯").
- iDestruct "HIp" as (p'') "(>Hl' & Hown & Hâ—)".
wp_load.
@@ -452,19 +441,23 @@ Section channel.
iDestruct "Hc" as
(γ γE l i n p' ->) "(#IH & #Hls & Hle & H◠& H◯ & Hown)".
do 6 wp_pure _. wp_bind (Fst _). wp_pure _.
- iInv "IH" as "HI".
+ iInv "IH" as "Hctx".
iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
iRewrite "Heq" in "Hown".
+ iAssert (▷ (⌜i < n⌠∗ iProto_own γ i (<(Recv, j)> m') ∗
+ iProto_ctx γ n))%I with "[Hctx Hown]"
+ as "[Hi [Hown Hctx]]".
+ { iNext. iDestruct (iProto_ctx_agree with "Hctx Hown") as %Hi.
+ iFrame. done. }
iAssert (▷ (▷ ⌜j < n⌠∗ iProto_own γ i (<(Recv, j)> m') ∗
- iProto_ctx γ (set_seq 0 n)))%I with "[HI Hown]" as "[HI [Hown Hctx]]".
- { iNext. iDestruct (iProto_target with "HI Hown") as "[Hin [$$]]".
- iFrame. iNext. iDestruct "Hin" as %Hin. by set_solver. }
+ iProto_ctx γ n))%I with "[Hctx Hown]" as "[Hj [Hown Hctx]]".
+ { iNext. iDestruct (iProto_target with "Hctx Hown") as "[Hin [$$]]".
+ iFrame. }
iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
wp_smart_apply (vpos_spec); [done|]; iIntros "_".
- iDestruct "HI" as %Hle.
- iDestruct (big_sepL_lookup_acc with "Hls") as "[Hj _]";
- [by apply lookup_replicate_2|].
- iDestruct "Hj" as (γE' γt γt') "#[IHl1 IHl2]".
+ iDestruct "Hi" as %Hi.
+ iDestruct "Hj" as %Hj.
+ iDestruct ("Hls" $! j i with "[//] [//]") as (γt) "IHl2".
wp_pures.
wp_bind (Xchg _ _).
iInv "IHl2" as "HIp".
@@ -483,8 +476,7 @@ Section channel.
{ iRight. iRight. iExists _. iFrame. }
wp_pures. iApply ("HL" with "[H◠H◯ Hown Hle] HΦ").
iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
- iDestruct "HIp" as (w m) "(>Hl' & Hown' & HIp)".
- iDestruct "HIp" as (p'') "[Hm Hp']".
+ iDestruct "HIp" as (w m p'') "(>Hl' & Hown' & Hm & Hp')".
iInv "IH" as "Hctx".
wp_xchg.
iDestruct (iProto_own_le with "Hown Hle") as "Hown".
diff --git a/multi_actris/channel/proofmode.v b/multi_actris/channel/proofmode.v
index 07c044920f750bd14e942c5043f7cc2e6ba20891..5f9d7b8fb105122ee7dc64e208c6ecb50395aef1 100644
--- a/multi_actris/channel/proofmode.v
+++ b/multi_actris/channel/proofmode.v
@@ -205,42 +205,14 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
| _ => fail "wp_recv: not a 'wp'"
end.
+
Tactic Notation "wp_recv" "as" constr(pat) :=
wp_recv_core (idtac) as (fun H => iDestructHyp H as pat).
-
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
- constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) ")" constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
- constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) ")" constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
- constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
- simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
- simple_intropattern(x8) ")" constr(pat) :=
- wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+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 →
@@ -318,33 +290,10 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
Tactic Notation "wp_send" "with" constr(pat) :=
wp_send_core (idtac) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) ")" "with" constr(pat) :=
- wp_send_core (eexists x1) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) ")" "with" constr(pat) :=
- wp_send_core (eexists x1; eexists x2) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) ")"
- "with" constr(pat) :=
- wp_send_core (eexists x1; eexists x2; eexists x3) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
- "with" constr(pat) :=
- wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4)
- uconstr(x5) ")" "with" constr(pat) :=
- wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
- uconstr(x5) uconstr(x6) ")" "with" constr(pat) :=
- wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
- eexists x6) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
- uconstr(x5) uconstr(x6) uconstr(x7) ")" "with" constr(pat) :=
- wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
- eexists x6; eexists x7) with pat.
-Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")"
- uconstr(x5) uconstr(x6) uconstr(x7) uconstr(x8) ")" "with" constr(pat) :=
- wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
- eexists x6; eexists x7; eexists x8) with pat.
-
-Lemma iProto_consistent_equiv_proof {Σ} (ps : gmap nat (iProto Σ)) :
+Tactic Notation "wp_send" "(" ne_uconstr_list(xs) ")" "with" constr(pat) :=
+ wp_send_core (ltac1_list_iter ltac:(fun x => eexists x) xs) with pat.
+
+Lemma iProto_consistent_equiv_proof {Σ} (ps : list (iProto Σ)) :
(∀ i j, valid_target ps i j) ∗
(∀ i j m1 m2,
(ps !!! i ≡ (<(Send, j)> m1)%proto) -∗
@@ -396,56 +345,31 @@ Tactic Notation "iProto_consistent_take_step_step" :=
let m1 := fresh in
let m2 := fresh in
iIntros (i j m1 m2) "#Hm1 #Hm2";
- repeat (destruct i as [|i];
- [repeat (rewrite lookup_total_insert_ne; [|lia]);
- try (by rewrite lookup_total_empty iProto_end_message_equivI);
- try (rewrite lookup_total_insert;
- try (by rewrite iProto_end_message_equivI);
- iDestruct (iProto_message_equivI with "Hm1")
- as "[%Heq1 Hm1']";simplify_eq)|
- repeat (rewrite lookup_total_insert_ne; [|lia]);
- try (by rewrite lookup_total_empty iProto_end_message_equivI)]);
- repeat (rewrite lookup_total_insert_ne; [|lia]);
- try rewrite lookup_total_empty;
- try (by iProto_end_message_equivI);
- rewrite lookup_total_insert;
+ repeat (destruct i as [|i]=> /=;
+ [try (by rewrite iProto_end_message_equivI);
+ iDestruct (iProto_message_equivI with "Hm1")
+ as "[%Heq1 Hm1']";simplify_eq=> /=|
+ try (by rewrite iProto_end_message_equivI)]);
+ try (by rewrite iProto_end_message_equivI);
iDestruct (iProto_message_equivI with "Hm2")
- as "[%Heq2 Hm2']";simplify_eq;
+ as "[%Heq2 Hm2']";simplify_eq=> /=;
try (iClear "Hm1' Hm2'";
iExists _,_,_,_,_,_,_,_,_,_;
iSplitL "Hm1"; [iFrame "#"|];
iSplitL "Hm2"; [iFrame "#"|];
iSplit; [iPureIntro; tc_solve|];
iSplit; [iPureIntro; tc_solve|];
- simpl; iClear "Hm1 Hm2"; clear m1 m2);
- try (repeat (rewrite (insert_commute _ _ i); [|done]);
- rewrite insert_insert;
- repeat (rewrite (insert_commute _ _ j); [|done]);
- rewrite insert_insert).
+ simpl; iClear "Hm1 Hm2"; clear m1 m2).
Tactic Notation "iProto_consistent_take_step_target" :=
let i := fresh in
iIntros (i j a m); rewrite /valid_target;
- iIntros "#Hm";
- repeat (destruct i as [|i];
- [repeat (rewrite lookup_total_insert_ne; [|lia]);
- try (by rewrite lookup_total_empty iProto_end_message_equivI);
- try (rewrite lookup_total_insert;
- try (by rewrite iProto_end_message_equivI);
- iDestruct (iProto_message_equivI with "Hm1")
- as "[%Heq1 Hm1']";simplify_eq)|
- repeat (rewrite lookup_total_insert_ne; [|lia]);
- try (by rewrite lookup_total_empty iProto_end_message_equivI)]);
- repeat (rewrite lookup_total_insert_ne; [|lia]);
- try rewrite lookup_total_empty;
- try (by iProto_end_message_equivI);
- rewrite lookup_total_insert;
- iDestruct (iProto_message_equivI with "Hm")
- as "[%Heq Hm']";simplify_eq;
- repeat (try rewrite lookup_empty;
- try rewrite lookup_insert;
- rewrite lookup_insert_ne; [|lia]);
- try rewrite lookup_insert; try done.
+ iIntros "#Hm1";
+ repeat (destruct i as [|i]=> /=;
+ [try (by rewrite iProto_end_message_equivI);
+ by iDestruct (iProto_message_equivI with "Hm1")
+ as "[%Heq1 _]" ; simplify_eq=> /=|
+ try (by rewrite iProto_end_message_equivI)]).
Tactic Notation "iProto_consistent_take_step" :=
try iNext;
@@ -453,13 +377,30 @@ Tactic Notation "iProto_consistent_take_step" :=
iSplitR; [iProto_consistent_take_step_target|
iProto_consistent_take_step_step].
-Tactic Notation "clean_map" constr(i) :=
- iEval (repeat (rewrite (insert_commute _ _ i); [|done]));
- rewrite (insert_insert _ i).
-
Tactic Notation "iProto_consistent_resolve_step" :=
repeat iIntros (?); repeat iIntros "?";
repeat iExists _; repeat (iSplit; [done|]); try iFrame.
Tactic Notation "iProto_consistent_take_steps" :=
repeat (iProto_consistent_take_step; iProto_consistent_resolve_step).
+
+Tactic Notation "wp_get_chan" "(" simple_intropattern(c) ")" constr(pat) :=
+ wp_smart_apply (get_chan_spec with "[$]"); iIntros (c) "[_TMP ?]";
+ iRevert "_TMP"; iIntros pat.
+
+Ltac ltac1_list_iter2 tac l1 l2 :=
+ let go := ltac2:(tac l1 l2 |- List.iter2 (ltac1:(tac x y |- tac x y) tac)
+ (of_ltac1_list l1) (of_ltac1_list l2)) in
+ go tac l1 l2.
+
+Tactic Notation "wp_new_chan" constr(prot) "as"
+ "(" simple_intropattern_list(xs) ")" constr_list(pats) :=
+ wp_smart_apply (new_chan_spec prot);
+ [set_solver| |iIntros (?) "?"];
+ [|ltac1_list_iter2 ltac:(fun x y => wp_get_chan (x) y) xs pats].
+
+Tactic Notation "wp_new_chan" constr(prot) "with" constr(lem) "as"
+ "(" simple_intropattern_list(xs) ")" constr_list(pats) :=
+ wp_smart_apply (new_chan_spec prot);
+ [set_solver|by iApply lem|iIntros (?) "?"];
+ ltac1_list_iter2 ltac:(fun x y => wp_get_chan (x) y) xs pats.
diff --git a/multi_actris/channel/proto.v b/multi_actris/channel/proto.v
index dbb1b16e265bc573133ee6d5180461709e85f43b..aa0826a901447c221041396c7a8b895ac871a5e1 100644
--- a/multi_actris/channel/proto.v
+++ b/multi_actris/channel/proto.v
@@ -173,22 +173,6 @@ Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m)
(at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
format "< a @.. x1 .. xn > m") : proto_scope.
-Notation "<!> m" := (<Send> m) (at level 200, m at level 200) : proto_scope.
-Notation "<! x1 .. xn > m" := (<!> ∃ x1, .. (∃ xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<! x1 .. xn > m") : proto_scope.
-Notation "<!.. x1 .. xn > m" := (<!> ∃.. x1, .. (∃.. xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<!.. x1 .. xn > m") : proto_scope.
-
-Notation "<?> m" := (<Recv> m) (at level 200, m at level 200) : proto_scope.
-Notation "<? x1 .. xn > m" := (<?> ∃ x1, .. (∃ xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<? x1 .. xn > m") : proto_scope.
-Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
- (at level 200, x1 closed binder, xn closed binder, m at level 200,
- format "<?.. x1 .. xn > m") : proto_scope.
-
Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
(tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
@@ -512,30 +496,30 @@ End proto.
Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
-Definition can_step {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
- (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
+Definition can_step {Σ V} (rec : list (iProto Σ V) → iProp Σ)
+ (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
∀ m1 m2,
- (ps !!! i ≡ <(Send, j)> m1) -∗
- (ps !!! j ≡ <(Recv, i)> m2) -∗
+ (ps !!! i ≡ (<(Send, j)> m1)) -∗
+ (ps !!! j ≡ (<(Recv, i)> m2)) -∗
∀ v p1, iMsg_car m1 v (Next p1) -∗
∃ p2, iMsg_car m2 v (Next p2) ∗
â–· (rec (<[i:=p1]>(<[j:=p2]>ps))).
-Definition valid_target {Σ V} (ps : gmap nat (iProto Σ V)) (i j : nat) : iProp Σ :=
- ∀ a m, (ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)âŒ.
+Definition valid_target {Σ V} (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
+ ∀ a m, (ps !!! i ≡ (<(a, j)> m)) -∗ ⌜is_Some (ps !! j)âŒ.
-Definition iProto_consistent_pre {Σ V} (rec : gmap nat (iProto Σ V) → iProp Σ)
- (ps : gmap nat (iProto Σ V)) : iProp Σ :=
+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).
Global Instance iProto_consistent_pre_ne {Σ V}
- (rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
NonExpansive (iProto_consistent_pre rec).
Proof. rewrite /iProto_consistent_pre /can_step /valid_target. solve_proper. Qed.
Program Definition iProto_consistent_pre' {Σ V}
- (rec : gmapO natO (iProto Σ V) -n> iPropO Σ) :
- gmapO natO (iProto Σ V) -n> iPropO Σ :=
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
+ listO (iProto Σ V) -n> iPropO Σ :=
λne ps, iProto_consistent_pre (λ ps, rec ps) ps.
Local Instance iProto_consistent_pre_contractive {Σ V} : Contractive (@iProto_consistent_pre' Σ V).
@@ -544,7 +528,7 @@ Proof.
solve_contractive.
Qed.
-Definition iProto_consistent {Σ V} (ps : gmap nat (iProto Σ V)) : iProp Σ :=
+Definition iProto_consistent {Σ V} (ps : list (iProto Σ V)) : iProp Σ :=
fixpoint iProto_consistent_pre' ps.
Arguments iProto_consistent {_ _} _%proto.
@@ -555,7 +539,7 @@ Proof. solve_proper. Qed.
Global Instance iProto_consistent_proper {Σ V} : Proper ((≡) ==> (⊣⊢)) (@iProto_consistent Σ V).
Proof. solve_proper. Qed.
-Lemma iProto_consistent_unfold {Σ V} (ps : gmap nat (iProto Σ V)) :
+Lemma iProto_consistent_unfold {Σ V} (ps : list (iProto Σ V)) :
iProto_consistent ps ≡ (iProto_consistent_pre iProto_consistent) ps.
Proof.
apply: (fixpoint_unfold iProto_consistent_pre').
@@ -615,12 +599,12 @@ Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p))).
Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
- (ps : gmap nat (iProto Σ V)) : iProp Σ :=
- own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$> ps) : gmap _ _)).
+ (ps : list (iProto Σ V)) : iProp Σ :=
+ own γ (gmap_view_auth (DfracOwn 1) ((λ p, Excl' (Next p)) <$> map_seq 0 ps)).
Definition iProto_ctx `{protoG Σ V}
- (γ : gname) (ps_dom : gset nat) : iProp Σ :=
- ∃ ps, ⌜dom ps = ps_dom⌠∗ iProto_own_auth γ ps ∗ ▷ iProto_consistent ps.
+ (γ : gname) (ps_len : nat) : iProp Σ :=
+ ∃ ps, ⌜length ps = ps_len⌠∗ iProto_own_auth γ ps ∗ ▷ iProto_consistent ps.
(** * The connective for ownership of channel ends *)
Definition iProto_own `{!protoG Σ V}
@@ -796,44 +780,191 @@ Section proto.
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.
+
+
+ Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
+ Proof. solve_proper. Qed.
+
+ Lemma iProto_own_auth_agree γ ps i p :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ▷ (ps !! i ≡ Some p).
+ Proof.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (own_valid_2 with "H◠H◯") as "H✓".
+ rewrite gmap_view_both_validI.
+ iDestruct "H✓" as "[_ [H1 H2]]".
+ rewrite lookup_fmap.
+ simpl.
+ rewrite lookup_map_seq_0.
+ destruct (ps !! i) eqn:Heqn; last first.
+ { rewrite Heqn. rewrite !option_equivI. done. }
+ rewrite Heqn.
+ simpl. rewrite !option_equivI excl_equivI. by iNext.
+ Qed.
+
+ Lemma iProto_own_auth_agree_Some γ ps i p :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ⌜is_Some (ps !! i)âŒ.
+ Proof.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (own_valid_2 with "H◠H◯") as "H✓".
+ rewrite gmap_view_both_validI.
+ iDestruct "H✓" as "[_ [H1 H2]]".
+ rewrite lookup_fmap.
+ simpl.
+ rewrite lookup_map_seq_0.
+ destruct (ps !! i) eqn:Heqn; last first.
+ { rewrite Heqn. rewrite !option_equivI. done. }
+ rewrite Heqn.
+ simpl. rewrite !option_equivI excl_equivI. done.
+ Qed.
+
+ Lemma iProto_own_auth_update γ ps i p p' :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p ==∗
+ iProto_own_auth γ (<[i := p']>ps) ∗ iProto_own_frag γ i p'.
+ Proof.
+ iIntros "Hâ— Hâ—¯".
+ iDestruct (iProto_own_auth_agree_Some with "Hâ— Hâ—¯") as %HSome.
+ iMod (own_update_2 with "Hâ— Hâ—¯") as "[H1 H2]"; [|iModIntro].
+ { eapply (gmap_view_replace _ _ _ (Excl' (Next p'))). done. }
+ iFrame. rewrite -fmap_insert.
+ rewrite /iProto_own_auth.
+ rewrite insert_map_seq_0; [done|].
+ by apply lookup_lt_is_Some_1.
+ Qed.
+
+ Lemma iProto_own_auth_alloc ps :
+ ⊢ |==> ∃ γ, iProto_own_auth γ ps ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
+ Proof.
+ iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γ) "Hauth".
+ { apply gmap_view_auth_valid. }
+ iExists γ.
+ iInduction ps as [|p ps] "IH" using rev_ind.
+ { iModIntro. iFrame. done. }
+ iMod ("IH" with "Hauth") as "[Hauth Hfrags]".
+ iFrame "Hfrags".
+ iMod (own_update with "Hauth") as "[Hauth Hfrag]".
+ { apply (gmap_view_alloc _ (length ps) (DfracOwn 1) (Excl' (Next p))); [|done|done].
+ rewrite fmap_map_seq.
+ rewrite lookup_map_seq_0.
+ apply lookup_ge_None_2. rewrite fmap_length. done. }
+ simpl.
+ iModIntro.
+ rewrite right_id_L.
+ rewrite -fmap_insert. iFrame.
+ iSplitL "Hauth".
+ - rewrite /iProto_own_auth.
+ rewrite map_seq_snoc. simpl. done.
+ - iSplit; [|done].
+ iExists _. iFrame. by iApply iProto_le_refl.
+ Qed.
+
+ Lemma list_lookup_Some_le (ps : list $ iProto Σ V) (i : nat) (p1 : iProto Σ V) :
+ ⊢@{iProp Σ} ps !! i ≡ Some p1 -∗ ⌜i < length psâŒ.
+ Proof.
+ iIntros "HSome".
+ rewrite option_equivI.
+ destruct (ps !! i) eqn:Heqn; [|done].
+ iPureIntro.
+ 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 ≡ p1 -∗
+ 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].
- { by rewrite lookup_insert. }
- rewrite lookup_insert_ne; [|done].
+ { rewrite list_lookup_insert; [done|]. done. }
+ rewrite (list_lookup_insert_ne _ i j'); [|done].
destruct (decide (i = i')) as [->|Hneqi].
- { rewrite lookup_total_insert. iRewrite "H" in "Hm".
+ { rewrite list_lookup_total_insert; [|done]. iRewrite "H" in "Hm".
by iDestruct (iProto_end_message_equivI with "Hm") as "Hm". }
- rewrite lookup_total_insert_ne; [|done].
+ 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].
- { rewrite lookup_insert. done. }
- rewrite lookup_insert_ne; [|done].
+ { by rewrite list_lookup_insert. }
+ rewrite (list_lookup_insert_ne _ i j'); [|done].
destruct (decide (i = i')) as [->|Hneqi].
- { rewrite lookup_total_insert. iRewrite "Heq" in "Hm".
+ { rewrite list_lookup_total_insert; [|done]. iRewrite "Heq" in "Hm".
iDestruct (iProto_message_equivI with "Hm") as (Heq) "Hm".
- simplify_eq. by iApply "Hprot". }
- rewrite lookup_total_insert_ne; [|done].
+ 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 ≡ p1 -∗
+ ps !! i ≡ Some p1 -∗
p1 ⊑ p2 -∗
iProto_consistent (<[i := p2]>ps).
Proof.
@@ -841,19 +972,21 @@ Section proto.
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 lookup_total_insert.
+ { rewrite list_lookup_total_insert; [|done].
pose proof (iProto_case p2) as [Hend|Hmsg].
- { setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
+ { 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 iProto_message_equivI.
+ { rewrite !option_equivI. rewrite iProto_message_equivI.
iDestruct "Hm1" as "[%Htag Hm1]". done. }
rewrite iProto_message_equivI.
iDestruct "Hm1" as "[%Htag Hm1]".
@@ -865,29 +998,35 @@ Section proto.
iDestruct "Hle" as (m') "[#Heq H]".
iDestruct ("H" with "Hm1'") as (p') "[Hle H]".
destruct (decide (i = j')) as [<-|Hneq].
- { rewrite lookup_total_insert. rewrite iProto_message_equivI.
+ { 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". rewrite !lookup_total_alt. iRewrite "HSome". done. }
- { rewrite lookup_total_insert_ne; [|done]. done. }
+ { 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".
- { by rewrite lookup_total_insert. }
+ { rewrite list_lookup_insert; [done|].
+ by rewrite insert_length. }
iClear "IH Hm1 Hm2 Heq".
- rewrite insert_insert.
- rewrite (insert_commute _ j' i); [|done].
- rewrite insert_insert. done. }
- rewrite lookup_total_insert_ne; [|done].
+ 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 lookup_total_insert.
+ { rewrite list_lookup_total_insert; [|done].
pose proof (iProto_case p2) as [Hend|Hmsg].
- { setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
+ { setoid_rewrite Hend.
+ rewrite !option_equivI.
+ rewrite iProto_end_message_equivI. done. }
destruct Hmsg as (a&?&m&Hmsg).
setoid_rewrite Hmsg.
destruct a.
- { rewrite iProto_message_equivI.
+ { rewrite !option_equivI.
+ rewrite iProto_message_equivI.
iDestruct "Hm2" as "[%Htag Hm2]". done. }
rewrite iProto_message_equivI.
iDestruct "Hm2" as "[%Htag Hm2]".
@@ -897,90 +1036,31 @@ Section proto.
iDestruct "Hle" as (m') "[#Heq Hle]".
iDestruct ("Hprot" $!i' with "[] [] Hm1'") as "Hprot".
{ done. }
- { rewrite !lookup_total_alt. iRewrite "HSome". 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 lookup_total_insert_ne; [|done].
- rewrite lookup_total_insert. done. }
- rewrite insert_commute; [|done].
- rewrite !insert_insert. done. }
- rewrite lookup_total_insert_ne; [|done].
+ { 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 (insert_commute _ j' i); [|done].
- rewrite (insert_commute _ i' i); [|done].
+ rewrite (list_insert_commute _ j' i); [|done].
+ rewrite (list_insert_commute _ i' i); [|done].
iApply ("IH" with "Hprot Hle []").
- rewrite lookup_total_insert_ne; [|done].
- rewrite lookup_total_insert_ne; [|done].
+ rewrite list_lookup_insert_ne; [|done].
+ rewrite list_lookup_insert_ne; [|done].
done.
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_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
Proof.
iIntros "H". iLöb as "IH" forall (p1 p2).
@@ -1130,16 +1210,18 @@ Section proto.
Lemma iProto_consistent_target ps m a i j :
iProto_consistent ps -∗
- ps !!! i ≡ (<(a, j)> m) -∗
+ ps !! i ≡ Some (<(a, j)> m) -∗
⌜is_Some (ps !! j)âŒ.
Proof.
- rewrite iProto_consistent_unfold. iDestruct 1 as "[Htar _]". iApply "Htar".
+ rewrite iProto_consistent_unfold. iDestruct 1 as "[Htar _]".
+ iIntros "H". iApply ("Htar" $! i).
+ rewrite list_lookup_total_alt. iRewrite "H". done.
Qed.
Lemma iProto_consistent_step ps m1 m2 i j v p1 :
iProto_consistent ps -∗
- ps !!! i ≡ (<(Send, j)> m1) -∗
- ps !!! j ≡ (<(Recv, i)> m2) -∗
+ ps !! i ≡ Some (<(Send, j)> m1) -∗
+ ps !! j ≡ Some (<(Recv, i)> m2) -∗
iMsg_car m1 v (Next p1) -∗
∃ p2, iMsg_car m2 v (Next p2) ∗
â–· iProto_consistent (<[i := p1]>(<[j := p2]>ps)).
@@ -1147,70 +1229,51 @@ Section proto.
iIntros "Hprot #Hi #Hj Hm1".
rewrite iProto_consistent_unfold /iProto_consistent_pre.
iDestruct "Hprot" as "[_ Hprot]".
- iDestruct ("Hprot" with "Hi Hj Hm1") as (p2) "[Hm2 Hprot]".
+ iDestruct ("Hprot" $! i j with "[Hi] [Hj] Hm1") as (p2) "[Hm2 Hprot]".
+ { rewrite list_lookup_total_alt. iRewrite "Hi". done. }
+ { rewrite list_lookup_total_alt. iRewrite "Hj". done. }
iExists p2. iFrame.
Qed.
- Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
- Proof. solve_proper. Qed.
-
- Lemma iProto_own_auth_agree γ ps i p :
- iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ▷ (ps !!! i ≡ p).
- Proof.
- iIntros "Hâ— Hâ—¯".
- iDestruct (own_valid_2 with "H◠H◯") as "H✓".
- rewrite gmap_view_both_validI.
- iDestruct "H✓" as "[_ [H1 H2]]".
- rewrite lookup_total_alt lookup_fmap.
- destruct (ps !! i); last first.
- { by rewrite !option_equivI. }
- simpl. rewrite !option_equivI excl_equivI. by iNext.
- Qed.
-
- Lemma iProto_own_auth_update γ ps i p p' :
- iProto_own_auth γ ps -∗ iProto_own_frag γ i p ==∗
- iProto_own_auth γ (<[i := p']>ps) ∗ iProto_own_frag γ i p'.
+ Lemma iProto_own_le γ s p1 p2 :
+ iProto_own γ s p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ s p2.
Proof.
- iIntros "Hâ— Hâ—¯".
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[H1 H2]"; [|iModIntro].
- { eapply (gmap_view_replace _ _ _ (Excl' (Next p'))). done. }
- iFrame. rewrite -fmap_insert. done.
+ iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
+ iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
Qed.
- Lemma iProto_own_auth_alloc ps :
- ⊢ |==> ∃ γ, iProto_own_auth γ ps ∗ [∗ map] i ↦p ∈ ps, iProto_own γ i p.
+ Lemma iProto_own_excl γ i (p1 p2 : iProto Σ V) :
+ iProto_own γ i p1 -∗ iProto_own γ i p2 -∗ False.
Proof.
- iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γ) "Hauth".
- { apply gmap_view_auth_valid. }
- iExists γ.
- iInduction ps as [|i p ps Hin] "IH" using map_ind.
- { iModIntro. iFrame. by iApply big_sepM_empty. }
- iMod ("IH" with "Hauth") as "[Hauth Hfrags]".
- rewrite big_sepM_insert; [|done]. iFrame "Hfrags".
- iMod (own_update with "Hauth") as "[Hauth Hfrag]".
- { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))); [|done|done].
- by rewrite lookup_fmap Hin. }
- iModIntro. rewrite -fmap_insert. iFrame.
- iExists _. iFrame. iApply iProto_le_refl.
+ rewrite /iProto_own.
+ iDestruct 1 as (p1') "[_ Hp1]".
+ iDestruct 1 as (p2') "[_ Hp2]".
+ iDestruct (own_prot_excl with "Hp1 Hp2") as %[].
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").
+ Lemma iProto_ctx_agree γ n i p :
+ iProto_ctx γ n -∗
+ iProto_own γ i p -∗
+ ⌜i < nâŒ.
+ Proof.
+ 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.
Qed.
Lemma iProto_init ps :
▷ iProto_consistent ps -∗
- |==> ∃ γ, iProto_ctx γ (dom ps) ∗ [∗ map] i ↦p ∈ ps, iProto_own γ i p.
+ |==> ∃ γ, iProto_ctx γ (length ps) ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
Proof.
iIntros "Hconsistent".
iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
iExists γ. iFrame. iExists _. by iFrame.
Qed.
-
Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
iProto_ctx γ ps_dom -∗
iProto_own γ i (<(Send, j)> m1) -∗
@@ -1220,53 +1283,53 @@ Section proto.
iProto_own γ i p1 ∗ iProto_own γ j p2.
Proof.
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 ≡ pj))%I as "Hpj'".
- { by rewrite lookup_total_insert_ne. }
+ 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". rewrite lookup_total_alt.
- destruct (ps !! i); [done|].
- iDestruct (iProto_end_message_equivI with "Hpi") as "[]". }
+ 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". rewrite !lookup_total_alt.
- destruct (ps !! j); [done|].
- iDestruct (iProto_end_message_equivI with "Hpj") as "[]". }
+ 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 lookup_total_insert_ne; [|done].
- rewrite lookup_total_insert_ne; [|done].
- by rewrite lookup_total_insert. }
- { rewrite lookup_total_insert_ne; [|done].
- by rewrite lookup_total_insert. }
+ { 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 insert_length. 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.
+ iDestruct "Hi'" as %Hi'. iDestruct "Hj'" as %Hj'.
iSplitL "Hconsistent Hauth".
{ iExists (<[i:=p1]> (<[j:=p2]> ps)).
iSplit.
- { rewrite !dom_insert_lookup_L; [done..|by rewrite lookup_insert_ne]. }
- iFrame. rewrite insert_insert.
- rewrite insert_commute; [|done]. rewrite insert_insert.
- by rewrite insert_commute; [|done]. }
+ { iPureIntro. rewrite !insert_length. 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.
Qed.
Lemma iProto_target γ ps_dom i a j m :
iProto_ctx γ ps_dom -∗
iProto_own γ i (<(a, j)> m) -∗
- â–· (⌜j ∈ ps_domâŒ) ∗ iProto_ctx γ ps_dom ∗ iProto_own γ i (<(a, j)> m).
+ â–· (⌜j < ps_domâŒ) ∗ iProto_ctx γ ps_dom ∗ iProto_own γ i (<(a, j)> m).
Proof.
iIntros "Hctx Hown".
rewrite /iProto_ctx /iProto_own.
@@ -1280,7 +1343,7 @@ Section proto.
iDestruct (iProto_consistent_target with "Hps Hi") as "#$". by iFrame. }
iSplitL "HSome".
{ iNext. iDestruct "HSome" as %Heq.
- iPureIntro. simplify_eq. by apply elem_of_dom. }
+ iPureIntro. simplify_eq. by apply lookup_lt_is_Some_1. }
iSplitL "Hauth Hps"; iExists _; by iFrame.
Qed.
diff --git a/multi_actris/channel/proto_alt.v b/multi_actris/channel/proto_alt.v
new file mode 100644
index 0000000000000000000000000000000000000000..8e27dbf061d0f1612e55ca9c01fa5fd45deaae76
--- /dev/null
+++ b/multi_actris/channel/proto_alt.v
@@ -0,0 +1,1417 @@
+(** This file defines the core of the Actris logic: It defines dependent
+separation protocols and the various operations on it like dual, append, and
+branching.
+
+Dependent separation protocols [iProto] are defined by instantiating the
+parameterized version in [proto_model] with the type of propositions [iProp] of Iris.
+We define ways of constructing instances of the instantiated type via two
+constructors:
+- [iProto_end], which is identical to [proto_end].
+- [iProto_message], which takes an [action] and an [iMsg]. The type [iMsg] is a
+ sequence of binders [iMsg_exist], terminated by the payload constructed with
+ [iMsg_base] based on arguments [v], [P] and [prot], which are the value, the
+ carried proposition and the [iProto] tail, respectively.
+
+For convenience sake, we provide the following notations:
+- [END], which is simply [iProto_end].
+- [∃ x, m], which is [iMsg_exist] with argument [m].
+- [MSG v {{ P }}; prot], which is [iMsg_Base] with arguments [v], [P] and [prot].
+- [<a> m], which is [iProto_message] with arguments [a] and [m].
+
+We also include custom notation to more easily construct complete constructions:
+- [<a x1 .. xn> m], which is [<a> ∃ x1, .. ∃ xn, m].
+- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol.
+
+Futhermore, we define the following operations:
+- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa.
+- [iProto_app], which appends two protocols.
+
+In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
+the following inductive definition for asynchronous subtyping on session types:
+
+ p1 <: p2 p1 <: p2 p1 <: !B.p3 ?A.p3 <: p2
+---------- ---------------- ---------------- ----------------------------
+end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2 ?A.p1 <: !B.p2
+
+Example:
+
+!R <: !R ?Q <: ?Q ?Q <: ?Q
+------------------- --------------
+?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
+------------------------------------
+ ?P.?Q.!R <: !R.?P.?Q
+
+Lastly, relevant type classes instances are defined for each of the above
+notions, such as contractiveness and non-expansiveness, after which the
+specifications of the message-passing primitives are defined in terms of the
+protocol connectives. *)
+From iris.algebra Require Import gmap excl_auth gmap_view.
+From iris.proofmode Require Import proofmode.
+From iris.base_logic Require Export lib.iprop.
+From iris.base_logic Require Import lib.own.
+From iris.program_logic Require Import language.
+From multi_actris.channel Require Import proto_model.
+Set Default Proof Using "Type".
+Export action.
+
+(** * Setup of Iris's cameras *)
+Class protoG Σ V :=
+ protoG_authG ::
+ inG Σ (gmap_viewR natO
+ (optionUR (exclR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))))).
+
+Definition protoΣ V := #[
+ GFunctor ((gmap_viewRF natO (optionRF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF))))))
+].
+Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
+Proof. solve_inG. Qed.
+
+(** * Types *)
+Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
+Declare Scope proto_scope.
+Delimit Scope proto_scope with proto.
+Bind Scope proto_scope with iProto.
+Local Open Scope proto.
+
+(** * Messages *)
+Section iMsg.
+ Set Primitive Projections.
+ Record iMsg Σ V := IMsg { iMsg_car : V → laterO (iProto Σ V) -n> iPropO Σ }.
+End iMsg.
+Arguments IMsg {_ _} _.
+Arguments iMsg_car {_ _} _.
+
+Declare Scope msg_scope.
+Delimit Scope msg_scope with msg.
+Bind Scope msg_scope with iMsg.
+Global Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
+
+Section imsg_ofe.
+ Context {Σ : gFunctors} {V : Type}.
+
+ Instance iMsg_equiv : Equiv (iMsg Σ V) := λ m1 m2,
+ ∀ w p, iMsg_car m1 w p ≡ iMsg_car m2 w p.
+ Instance iMsg_dist : Dist (iMsg Σ V) := λ n m1 m2,
+ ∀ w p, iMsg_car m1 w p ≡{n}≡ iMsg_car m2 w p.
+
+ Lemma iMsg_ofe_mixin : OfeMixin (iMsg Σ V).
+ Proof. by apply (iso_ofe_mixin (iMsg_car : _ → V -d> _ -n> _)). Qed.
+ Canonical Structure iMsgO := Ofe (iMsg Σ V) iMsg_ofe_mixin.
+
+ Global Instance iMsg_cofe : Cofe iMsgO.
+ Proof. by apply (iso_cofe (IMsg : (V -d> _ -n> _) → _) iMsg_car). Qed.
+End imsg_ofe.
+
+Program Definition iMsg_base_def {Σ V}
+ (v : V) (P : iProp Σ) (p : iProto Σ V) : iMsg Σ V :=
+ IMsg (λ v', λne p', ⌜ v = v' ⌠∗ Next p ≡ p' ∗ P)%I.
+Next Obligation. solve_proper. Qed.
+Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
+Definition iMsg_base := iMsg_base_aux.(unseal).
+Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
+Arguments iMsg_base {_ _} _%V _%I _%proto.
+Global Instance: Params (@iMsg_base) 3 := {}.
+
+Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
+ IMsg (λ v', λne p', ∃ x, iMsg_car (m x) v' p')%I.
+Next Obligation. solve_proper. Qed.
+Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
+Definition iMsg_exist := iMsg_exist_aux.(unseal).
+Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
+Arguments iMsg_exist {_ _ _} _%msg.
+Global Instance: Params (@iMsg_exist) 3 := {}.
+
+Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
+ tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
+Arguments iMsg_texist {_ _ !_} _%msg /.
+
+Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
+ (at level 200, v at level 20, right associativity,
+ format "MSG v {{ P } } ; p") : msg_scope.
+Notation "'MSG' v ; p" := (iMsg_base v True p)
+ (at level 200, v at level 20, right associativity,
+ format "MSG v ; p") : msg_scope.
+Notation "∃ x .. y , m" :=
+ (iMsg_exist (λ x, .. (iMsg_exist (λ y, m)) ..)%msg) : msg_scope.
+Notation "'∃..' x .. y , m" :=
+ (iMsg_texist (λ x, .. (iMsg_texist (λ y, m)) .. )%msg)
+ (at level 200, x binder, y binder, right associativity,
+ format "∃.. x .. y , m") : msg_scope.
+
+Lemma iMsg_texist_exist {Σ V} {TT : tele} w lp (m : TT → iMsg Σ V) :
+ iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp).
+Proof.
+ rewrite /iMsg_texist iMsg_exist_eq.
+ induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH.
+Qed.
+
+(** * Operators *)
+Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
+Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
+Definition iProto_end := iProto_end_aux.(unseal).
+Definition iProto_end_eq : @iProto_end = @iProto_end_def := iProto_end_aux.(seal_eq).
+Arguments iProto_end {_ _}.
+
+Definition iProto_message_def {Σ V} (a : action) (m : iMsg Σ V) : iProto Σ V :=
+ proto_message a (iMsg_car m).
+Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
+Definition iProto_message := iProto_message_aux.(unseal).
+Definition iProto_message_eq :
+ @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
+Arguments iProto_message {_ _} _ _%msg.
+Global Instance: Params (@iProto_message) 3 := {}.
+
+Notation "'END'" := iProto_end : proto_scope.
+
+Notation "< a > m" := (iProto_message a m)
+ (at level 200, a at level 10, m at level 200,
+ format "< a > m") : proto_scope.
+Notation "< a @ x1 .. xn > m" := (iProto_message a (∃ x1, .. (∃ xn, m) ..))
+ (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
+ format "< a @ x1 .. xn > m") : proto_scope.
+Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m) ..))
+ (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
+ format "< a @.. x1 .. xn > m") : proto_scope.
+
+Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
+ (tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
+ msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
+Global Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
+
+(** * Operations *)
+Program Definition iMsg_map {Σ V}
+ (rec : iProto Σ V → iProto Σ V) (m : iMsg Σ V) : iMsg Σ 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 := {}.
+
+(** * Proofs *)
+Section proto.
+ Context `{!protoG Σ V}.
+ Implicit Types v : V.
+ Implicit Types p pl pr : iProto Σ V.
+ 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 ⌠∧
+ (∀ 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.
+ 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.
+ Proof. by rewrite internal_eq_sym iProto_message_end_equivI. Qed.
+
+ (** ** Non-expansiveness of operators *)
+ Global Instance iMsg_car_proper :
+ Proper (iMsg_equiv ==> (=) ==> (≡) ==> (≡)) (iMsg_car (Σ:=Σ) (V:=V)).
+ Proof.
+ intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+ f_equiv; [ by f_equiv | done ].
+ Qed.
+ Global Instance iMsg_car_ne n :
+ Proper (iMsg_dist n ==> (=) ==> (dist n) ==> (dist n)) (iMsg_car (Σ:=Σ) (V:=V)).
+ Proof.
+ intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+ f_equiv; [ by f_equiv | done ].
+ Qed.
+
+ Global Instance iMsg_contractive v n :
+ Proper (dist n ==> dist_later n ==> dist n) (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_contractive. Qed.
+ Global Instance iMsg_ne v : NonExpansive2 (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_proper. Qed.
+ Global Instance iMsg_proper v :
+ Proper ((≡) ==> (≡) ==> (≡)) (iMsg_base (Σ:=Σ) (V:=V) v).
+ Proof. apply (ne_proper_2 _). Qed.
+
+ Global Instance iMsg_exist_ne A n :
+ Proper (pointwise_relation _ (dist n) ==> (dist n)) (@iMsg_exist Σ V A).
+ Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
+ Global Instance iMsg_exist_proper A :
+ Proper (pointwise_relation _ (≡) ==> (≡)) (@iMsg_exist Σ V A).
+ Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
+
+ Global Instance msg_tele_base (v:V) (P : iProp Σ) (p : iProto Σ V) :
+ MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
+ Proof. done. Qed.
+ Global Instance msg_tele_exist {A} {TT : A → tele} (m : A → iMsg Σ V) tv tP tp :
+ (∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) →
+ MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
+ Proof. intros Hm. rewrite /MsgTele /=. f_equiv=> x. apply Hm. Qed.
+
+ Global Instance iProto_message_ne a :
+ NonExpansive (iProto_message (Σ:=Σ) (V:=V) a).
+ Proof. rewrite iProto_message_eq. solve_proper. Qed.
+ Global Instance iProto_message_proper a :
+ Proper ((≡) ==> (≡)) (iProto_message (Σ:=Σ) (V:=V) a).
+ Proof. apply (ne_proper _). Qed.
+
+ Lemma iProto_message_equiv {TT1 TT2 : tele} a1 a2
+ (m1 m2 : iMsg Σ V)
+ (v1 : TT1 -t> V) (v2 : TT2 -t> V)
+ (P1 : TT1 -t> iProp Σ) (P2 : TT2 -t> iProp Σ)
+ (prot1 : TT1 -t> iProto Σ V) (prot2 : TT2 -t> iProto Σ V) :
+ MsgTele m1 v1 P1 prot1 →
+ MsgTele m2 v2 P2 prot2 →
+ ⌜ a1 = a2 ⌠-∗
+ (■∀.. (xs1 : TT1), tele_app P1 xs1 -∗
+ ∃.. (xs2 : TT2), ⌜tele_app v1 xs1 = tele_app v2 xs2⌠∗
+ ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
+ tele_app P2 xs2) -∗
+ (■∀.. (xs2 : TT2), tele_app P2 xs2 -∗
+ ∃.. (xs1 : TT1), ⌜tele_app v1 xs1 = tele_app v2 xs2⌠∗
+ ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
+ tele_app P1 xs1) -∗
+ (<a1> m1) ≡ (<a2> m2).
+ Proof.
+ iIntros (Hm1 Hm2 Heq) "#Heq1 #Heq2".
+ unfold MsgTele in Hm1. rewrite Hm1. clear Hm1.
+ unfold MsgTele in Hm2. rewrite Hm2. clear Hm2.
+ rewrite iProto_message_eq proto_message_equivI.
+ iSplit; [ done | ].
+ iIntros (v p').
+ do 2 rewrite iMsg_texist_exist.
+ rewrite iMsg_base_eq /=.
+ iApply prop_ext.
+ iIntros "!>". iSplit.
+ - iDestruct 1 as (xs1 Hveq1) "[Hrec1 HP1]".
+ iDestruct ("Heq1" with "HP1") as (xs2 Hveq2) "[Hrec2 HP2]".
+ iExists xs2. rewrite -Hveq1 Hveq2.
+ iSplitR; [ done | ]. iSplitR "HP2"; [ | done ].
+ iRewrite -"Hrec1". iApply later_equivI. iIntros "!>". by iRewrite "Hrec2".
+ - iDestruct 1 as (xs2 Hveq2) "[Hrec2 HP2]".
+ iDestruct ("Heq2" with "HP2") as (xs1 Hveq1) "[Hrec1 HP1]".
+ iExists xs1. rewrite -Hveq2 Hveq1.
+ iSplitR; [ done | ]. iSplitR "HP1"; [ | done ].
+ iRewrite -"Hrec2". iApply later_equivI. iIntros "!>". by iRewrite "Hrec1".
+ Qed.
+
+ (** Helpers *)
+ Lemma iMsg_map_base f v P p :
+ NonExpansive f →
+ iMsg_map f (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; f p)%msg.
+ Proof.
+ rewrite iMsg_base_eq. intros ? v' p'; simpl. iSplit.
+ - iDestruct 1 as (p'') "[(->&Hp&$) Hp']". iSplit; [done|].
+ iRewrite "Hp'". iIntros "!>". by iRewrite "Hp".
+ - iIntros "(->&Hp'&$)". iExists p. iRewrite -"Hp'". auto.
+ Qed.
+ Lemma iMsg_map_exist {A} f (m : A → iMsg Σ V) :
+ iMsg_map f (∃ x, m x) ≡ (∃ x, iMsg_map f (m x))%msg.
+ Proof.
+ rewrite iMsg_exist_eq. intros v' p'; simpl. iSplit.
+ - iDestruct 1 as (p'') "[H Hp']". iDestruct "H" as (x) "H"; auto.
+ - iDestruct 1 as (x p'') "[Hm Hp']". auto.
+ Qed.
+
+ (** ** Dual *)
+ 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.
+
+Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
+
+Program Definition iProto_elim {Σ V A}
+ (x : A) (f : action → iMsg Σ V -> A) (p : iProto Σ V) : A :=
+ proto_elim x (λ a m, f a (IMsg (λ v, λne p, m v p)))%I p.
+Next Obligation. solve_proper. Qed.
+
+Lemma iProto_elim_message {Σ V} {A:ofe}
+ (x : A) (f : action → iMsg Σ V -> A) a m
+ `{Hf : ∀ a, Proper ((≡) ==> (≡)) (f a)} :
+ iProto_elim x f (iProto_message a m) ≡ f a m.
+ Proof.
+ rewrite /iProto_elim iProto_message_eq /iProto_message_def /=.
+ setoid_rewrite proto_elim_message.
+ { apply Hf. done. }
+ intros a' f1 f2 Hf'. apply Hf=> v p /=. apply Hf'.
+Qed.
+
+Lemma iProto_elim_message' {Σ V} {A:ofe}
+ (x : A) (f : action → iMsg Σ V -> A) a m
+ `{Hf : ∀ a, Proper ((≡) ==> (≡)) (f a)} :
+ iProto_elim x f (iProto_message a m) ≡ f a m.
+Proof.
+ rewrite /iProto_elim.
+ rewrite iProto_message_eq /iProto_message_def. simpl.
+ setoid_rewrite proto_elim_message.
+ { f_equiv. done. }
+ intros a'.
+ intros f1 f2 Hf'. f_equiv. done.
+Qed.
+
+Definition nat_beq := Eval compute in Nat.eqb.
+
+Definition find_recv {Σ V} (i:nat) (j:nat) (ps : list (iProto Σ V)) :
+ option $ iMsg Σ V :=
+ iProto_elim None (λ a m,
+ match a with
+ | (Recv, i') => if nat_beq i i' then Some m else None
+ | (Send, _) => None
+ end) (ps !!! j).
+
+Fixpoint sync_pairs_aux {Σ V} (i : nat) (ps_full ps : list (iProto Σ V)) :
+ list (nat * nat * iMsg Σ V * iMsg Σ V) :=
+ match ps with
+ | [] => []
+ | p :: ps =>
+ iProto_elim (sync_pairs_aux (S i) ps_full ps)
+ (λ a mi, match a with
+ | (Recv,_) => sync_pairs_aux (S i) ps_full ps
+ | (Send,j) => match find_recv i j ps_full with
+ | None => sync_pairs_aux (S i) ps_full ps
+ | Some mj => (i,j,mi,mj) ::
+ sync_pairs_aux (S i) ps_full ps
+ end
+ end) p
+ end.
+
+Notation sync_pairs ps := (sync_pairs_aux 0 ps ps).
+
+Definition can_step {Σ V} (rec : list (iProto Σ V) → iProp Σ)
+ (ps : list (iProto Σ V)) : iProp Σ :=
+ [∧ list] '(i,j,m1,m2) ∈ sync_pairs ps,
+ ∀ v p1, iMsg_car m1 v (Next p1) -∗
+ ∃ p2, iMsg_car m2 v (Next p2) ∗
+ â–· (rec (<[i:=p1]>(<[j:=p2]>ps))).
+
+From iris.heap_lang Require Import notation.
+
+Definition iProto_binary `{!heapGS Σ} : list (iProto Σ val) :=
+ [(<(Send, 1) @ (x:Z)> MSG #x ; END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ; END)%proto].
+
+Lemma iProto_binary_consistent `{!heapGS Σ} :
+ ⊢ can_step (λ _, True) (@iProto_binary _ Σ heapGS).
+Proof. rewrite /iProto_binary /can_step /iProto_elim. simpl.
+ rewrite /find_recv. simpl.
+ Fail rewrite iProto_elim_message.
+ (* OBS: Break here *)
+
+
+Definition valid_target {Σ V} (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
+ ∀ a m, (ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)âŒ.
+
+Definition iProto_consistent_pre {Σ V} (rec : list (iProto Σ V) → iProp Σ)
+ (ps : list (iProto Σ V)) : iProp Σ :=
+ (∀ i j, valid_target ps i j) ∗ (can_step rec ps).
+
+Global Instance iProto_consistent_pre_ne {Σ V}
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
+ NonExpansive (iProto_consistent_pre rec).
+Proof. rewrite /iProto_consistent_pre /can_step /valid_target. solve_proper. Qed.
+
+Program Definition iProto_consistent_pre' {Σ V}
+ (rec : listO (iProto Σ V) -n> iPropO Σ) :
+ listO (iProto Σ V) -n> iPropO Σ :=
+ λne ps, iProto_consistent_pre (λ ps, rec ps) ps.
+
+Local Instance iProto_consistent_pre_contractive {Σ V} : Contractive (@iProto_consistent_pre' Σ V).
+Proof.
+ rewrite /iProto_consistent_pre' /iProto_consistent_pre /can_step.
+ solve_contractive.
+Qed.
+
+Definition iProto_consistent {Σ V} (ps : list (iProto Σ V)) : iProp Σ :=
+ fixpoint iProto_consistent_pre' ps.
+
+Arguments iProto_consistent {_ _} _%proto.
+Global Instance: Params (@iProto_consistent) 1 := {}.
+
+Global Instance iProto_consistent_ne {Σ V} : NonExpansive (@iProto_consistent Σ V).
+Proof. solve_proper. Qed.
+Global Instance iProto_consistent_proper {Σ V} : Proper ((≡) ==> (⊣⊢)) (@iProto_consistent Σ V).
+Proof. solve_proper. Qed.
+
+Lemma iProto_consistent_unfold {Σ V} (ps : list (iProto Σ V)) :
+ iProto_consistent ps ≡ (iProto_consistent_pre iProto_consistent) ps.
+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.
+
+Record proto_name := ProtName { proto_names : gmap nat gname }.
+Global Instance proto_name_inhabited : Inhabited proto_name :=
+ populate (ProtName inhabitant).
+Global Instance proto_name_eq_dec : EqDecision proto_name.
+Proof. solve_decision. Qed.
+Global Instance proto_name_countable : Countable proto_name.
+Proof.
+ refine (inj_countable (λ '(ProtName γs), (γs))
+ (λ '(γs), Some (ProtName γs)) _); by intros [].
+Qed.
+
+Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
+ (i : nat) (p : iProto Σ V) : iProp Σ :=
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p))).
+
+Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
+ (ps : list (iProto Σ V)) : iProp Σ :=
+ own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$>
+ (list_to_map (zip (seq 0 (length ps)) ps))) : gmap _ _)).
+
+Definition iProto_ctx `{protoG Σ V}
+ (γ : gname) (ps_len : nat) : iProp Σ :=
+ ∃ ps, ⌜length ps = ps_len⌠∗ iProto_own_auth γ ps ∗ ▷ iProto_consistent ps.
+
+(** * 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'.
+Arguments iProto_own {_ _ _} _ _ _%proto.
+Global Instance: Params (@iProto_own) 3 := {}.
+
+Global Instance iProto_own_frag_contractive `{protoG Σ V} γ i :
+ Contractive (iProto_own_frag γ i).
+Proof. solve_contractive. Qed.
+
+Global Instance iProto_own_contractive `{protoG Σ V} γ i :
+ Contractive (iProto_own γ i).
+Proof. solve_contractive. Qed.
+Global Instance iProto_own_ne `{protoG Σ V} γ s : NonExpansive (iProto_own γ s).
+Proof. solve_proper. Qed.
+Global Instance iProto_own_proper `{protoG Σ V} γ s :
+ Proper ((≡) ==> (≡)) (iProto_own γ s).
+Proof. apply (ne_proper _). Qed.
+
+(** * Proofs *)
+Section proto.
+ Context `{!protoG Σ V}.
+ Implicit Types v : V.
+ Implicit Types p pl pr : iProto Σ V.
+ Implicit Types m : iMsg Σ V.
+
+ Lemma own_prot_idx γ i j (p1 p2 : iProto Σ V) :
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
+ own γ (gmap_view_frag j (DfracOwn 1) (Excl' (Next p2))) -∗
+ ⌜i ≠jâŒ.
+ Proof.
+ iIntros "Hown Hown'" (->).
+ iDestruct (own_valid_2 with "Hown Hown'") as "H".
+ rewrite uPred.cmra_valid_elim.
+ by iDestruct "H" as %[]%gmap_view_frag_op_validN.
+ Qed.
+
+ Lemma own_prot_excl γ i (p1 p2 : iProto Σ V) :
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
+ own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p2))) -∗
+ False.
+ 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 valid_target_le ps i p1 p2 :
+ (∀ i' j', valid_target ps i' j') -∗
+ ps !!! i ≡ p1 -∗
+ p1 ⊑ p2 -∗
+ (∀ i' j', valid_target (<[i := p2]>ps) i' j') ∗ p1 ⊑ p2.
+ Proof. Admitted.
+ (* iIntros "Hprot #HSome Hle". *)
+ (* 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]. *)
+ (* { Search list_lookup_total insert. rewrite list_lookup_total_insert. ; [done|]. lia. done. } *)
+ (* rewrite lookup_insert_ne; [|done]. *)
+ (* destruct (decide (i = i')) as [->|Hneqi]. *)
+ (* { rewrite lookup_total_insert. iRewrite "H" in "Hm". *)
+ (* by iDestruct (iProto_end_message_equivI with "Hm") as "Hm". } *)
+ (* rewrite 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]. *)
+ (* { rewrite lookup_insert. done. } *)
+ (* rewrite lookup_insert_ne; [|done]. *)
+ (* destruct (decide (i = i')) as [->|Hneqi]. *)
+ (* { rewrite lookup_total_insert. iRewrite "Heq" in "Hm". *)
+ (* iDestruct (iProto_message_equivI with "Hm") as (Heq) "Hm". *)
+ (* simplify_eq. by iApply "Hprot". } *)
+ (* rewrite lookup_total_insert_ne; [|done]. *)
+ (* by iApply "Hprot". *)
+ (* Qed. *)
+
+ Lemma iProto_consistent_le ps i p1 p2 :
+ iProto_consistent ps -∗
+ ps !!! i ≡ 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".
+ 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; [|admit].
+ pose proof (iProto_case p2) as [Hend|Hmsg].
+ { setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
+ destruct Hmsg as (a&?&m&Hmsg).
+ setoid_rewrite Hmsg.
+ destruct a; last first.
+ { 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. rewrite iProto_message_equivI.
+ iDestruct "Hm2" as "[%Heq _]". done. admit. }
+ iDestruct ("Hprot" $!i j' with "[] [] H") as "Hprot".
+ { iRewrite -"Heq". 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_total_insert; [done|]. admit. }
+ 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.
+ pose proof (iProto_case p2) as [Hend|Hmsg].
+ { setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
+ destruct Hmsg as (a&?&m&Hmsg).
+ setoid_rewrite Hmsg.
+ destruct a.
+ { 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. }
+ { 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_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert. done. admit. }
+ rewrite list_insert_commute; [|done].
+ rewrite !list_insert_insert. done. admit. }
+ 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_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert_ne; [|done].
+ done.
+ Admitted.
+
+ 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_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 ≡ (<(a, j)> m) -∗
+ ⌜is_Some (ps !! j)âŒ.
+ Proof.
+ rewrite iProto_consistent_unfold. iDestruct 1 as "[Htar _]". iApply "Htar".
+ Qed.
+
+ Lemma iProto_consistent_step ps m1 m2 i j v p1 :
+ iProto_consistent ps -∗
+ ps !!! i ≡ (<(Send, j)> m1) -∗
+ ps !!! j ≡ (<(Recv, i)> m2) -∗
+ iMsg_car m1 v (Next p1) -∗
+ ∃ p2, iMsg_car m2 v (Next p2) ∗
+ â–· iProto_consistent (<[i := p1]>(<[j := p2]>ps)).
+ Proof.
+ iIntros "Hprot #Hi #Hj Hm1".
+ rewrite iProto_consistent_unfold /iProto_consistent_pre.
+ iDestruct "Hprot" as "[_ Hprot]".
+ iDestruct ("Hprot" with "Hi Hj Hm1") as (p2) "[Hm2 Hprot]".
+ iExists p2. iFrame.
+ Qed.
+
+ Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
+ Proof. solve_proper. Qed.
+
+ Lemma iProto_own_auth_agree γ ps i p :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ▷ (ps !!! i ≡ p).
+ Proof. Admitted.
+ (* iIntros "Hâ— Hâ—¯". *)
+ (* iDestruct (own_valid_2 with "H◠H◯") as "H✓". *)
+ (* rewrite gmap_view_both_validI. *)
+ (* iDestruct "H✓" as "[_ [H1 H2]]". *)
+ (* rewrite list_lookup_total_alt lookup_fmap. *)
+ (* destruct (ps !! i); last first. *)
+ (* { rewrite !option_equivI. } *)
+ (* simpl. rewrite !option_equivI excl_equivI. by iNext. *)
+ (* Qed. *)
+
+ Lemma iProto_own_auth_update γ ps i p p' :
+ iProto_own_auth γ ps -∗ iProto_own_frag γ i p ==∗
+ iProto_own_auth γ (<[i := p']>ps) ∗ iProto_own_frag γ i p'.
+ Proof.
+ iIntros "Hâ— Hâ—¯".
+ iMod (own_update_2 with "Hâ— Hâ—¯") as "[H1 H2]"; [|iModIntro].
+ { eapply (gmap_view_replace _ _ _ (Excl' (Next p'))). done. }
+ iFrame. rewrite -fmap_insert. Admitted.
+
+ Lemma iProto_own_auth_alloc ps :
+ ⊢ |==> ∃ γ, iProto_own_auth γ ps ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
+ Proof. Admitted.
+ (* iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γ) "Hauth". *)
+ (* { apply gmap_view_auth_valid. } *)
+ (* iExists γ. *)
+ (* iInduction ps as [|i p ps Hin] "IH" using map_ind. *)
+ (* { iModIntro. iFrame. by iApply big_sepM_empty. } *)
+ (* iMod ("IH" with "Hauth") as "[Hauth Hfrags]". *)
+ (* rewrite big_sepM_insert; [|done]. iFrame "Hfrags". *)
+ (* iMod (own_update with "Hauth") as "[Hauth Hfrag]". *)
+ (* { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))); [|done|done]. *)
+ (* by rewrite lookup_fmap Hin. } *)
+ (* iModIntro. rewrite -fmap_insert. iFrame. *)
+ (* iExists _. iFrame. iApply iProto_le_refl. *)
+ (* 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_init ps :
+ ▷ iProto_consistent ps -∗
+ |==> ∃ γ, iProto_ctx γ (length ps) ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
+ Proof.
+ iIntros "Hconsistent".
+ iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
+ iExists γ. iFrame. iExists _. by iFrame.
+ Qed.
+
+
+ Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
+ iProto_ctx γ ps_dom -∗
+ iProto_own γ i (<(Send, j)> m1) -∗
+ iProto_own γ j (<(Recv, i)> m2) -∗
+ iMsg_car m1 v (Next p1) ==∗
+ ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ iProto_ctx γ ps_dom ∗
+ iProto_own γ i p1 ∗ iProto_own γ j p2.
+ Proof.
+ iIntros "Hctx Hi Hj Hm".
+ 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 ≡ pj))%I as "Hpj'".
+ { by rewrite list_lookup_total_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". rewrite list_lookup_total_alt.
+ destruct (ps !! i); [done|].
+ iDestruct (iProto_end_message_equivI with "Hpi") as "[]". }
+ 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". rewrite !list_lookup_total_alt.
+ destruct (ps !! j); [done|].
+ iDestruct (iProto_end_message_equivI with "Hpj") as "[]". }
+ 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_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert; [done|]. admit. }
+ { rewrite list_lookup_total_insert_ne; [|done].
+ rewrite list_lookup_total_insert; [done|]. admit. }
+ 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.
+ { admit.
+ (* rewrite !dom_insert_lookup_L; [done..|by rewrite lookup_insert_ne]. *)}
+ 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.
+ Admitted.
+
+ Lemma iProto_target γ ps_dom i a j m :
+ iProto_ctx γ ps_dom -∗
+ iProto_own γ i (<(a, j)> m) -∗
+ â–· (⌜j < ps_domâŒ) ∗ iProto_ctx γ ps_dom ∗ iProto_own γ i (<(a, j)> m).
+ Proof.
+ iIntros "Hctx Hown".
+ rewrite /iProto_ctx /iProto_own.
+ iDestruct "Hctx" as (ps Hdom) "[Hauth Hps]".
+ 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".
+ iAssert (▷ (⌜is_Some (ps !! j)⌠∗ iProto_consistent ps))%I
+ with "[Hps]" as "[HSome Hps]".
+ { iNext. iRewrite "Heq" in "Hi".
+ iDestruct (iProto_consistent_target with "Hps Hi") as "#$". by iFrame. }
+ iSplitL "HSome".
+ { iNext. iDestruct "HSome" as %Heq.
+ iPureIntro. simplify_eq. admit. }
+ iSplitL "Hauth Hps"; iExists _; by iFrame.
+ Admitted.
+
+ (* (** 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.
+
+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.
diff --git a/multi_actris/examples/basics.v b/multi_actris/examples/basics.v
index 9efa72bdd741c8aa00e88c4fc95c0bb39f38d361..36c500f5638399b41d1f224f642729436330879d 100644
--- a/multi_actris/examples/basics.v
+++ b/multi_actris/examples/basics.v
@@ -1,16 +1,15 @@
From multi_actris.channel Require Import proofmode.
Set Default Proof Using "Type".
-Definition iProto_empty {Σ} : gmap nat (iProto Σ) := ∅.
+Definition iProto_empty {Σ} : list (iProto Σ) := [].
Lemma iProto_consistent_empty {Σ} :
⊢ iProto_consistent (@iProto_empty Σ).
-Proof. iProto_consistent_take_step. Qed.
+Proof. iProto_consistent_take_steps. Qed.
-Definition iProto_binary `{!heapGS Σ} : gmap nat (iProto Σ) :=
- <[0 := (<(Send, 1) @ (x:Z)> MSG #x ; END)%proto ]>
- (<[1 := (<(Recv, 0) @ (x:Z)> MSG #x ; END)%proto ]>
- ∅).
+Definition iProto_binary `{!heapGS Σ} : list (iProto Σ) :=
+ [(<(Send, 1) @ (x:Z)> MSG #x ; END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ; END)%proto].
Lemma iProto_binary_consistent `{!heapGS Σ} :
⊢ iProto_consistent iProto_binary.
@@ -29,10 +28,10 @@ Definition roundtrip_prog : val :=
Section channel.
Context `{!heapGS Σ, !chanG Σ}.
- Definition iProto_roundtrip : gmap nat (iProto Σ) :=
- <[0 := (<(Send, 1) @ (x:Z)> MSG #x ; <(Recv, 2)> MSG #x; END)%proto ]>
- (<[1 := (<(Recv, 0) @ (x:Z)> MSG #x ; <(Send, 2)> MSG #x; END)%proto ]>
- (<[2 := (<(Recv, 1) @ (x:Z)> MSG #x ; <(Send, 0)> MSG #x; END)%proto ]> ∅)).
+ Definition iProto_roundtrip : list (iProto Σ) :=
+ [(<(Send, 1) @ (x:Z)> MSG #x ; <(Recv, 2)> MSG #x; END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ; <(Send, 2)> MSG #x; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ; <(Send, 0)> MSG #x; END)%proto].
Lemma iProto_roundtrip_consistent :
⊢ iProto_consistent iProto_roundtrip.
@@ -43,15 +42,8 @@ Section channel.
{{{ True }}} roundtrip_prog #() {{{ RET #42 ; True }}}.
Proof using chanG0 heapGS0 Σ.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_smart_apply (new_chan_spec 3 iProto_roundtrip);
- [lia|set_solver|iApply iProto_roundtrip_consistent|].
- iIntros (cs) "Hcs".
- wp_smart_apply (get_chan_spec _ 0 with "Hcs"); [set_solver|].
- iIntros (c0) "[Hc0 Hcs]".
- wp_smart_apply (get_chan_spec _ 1 with "Hcs"); [set_solver|].
- iIntros (c1) "[Hc1 Hcs]".
- wp_smart_apply (get_chan_spec _ 2 with "Hcs"); [set_solver|].
- iIntros (c2) "[Hc2 Hcs]".
+ wp_new_chan iProto_roundtrip with iProto_roundtrip_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
wp_smart_apply (wp_fork with "[Hc1]").
{ iIntros "!>". wp_recv (x) as "_". wp_send with "[//]". done. }
wp_smart_apply (wp_fork with "[Hc2]").
@@ -74,13 +66,13 @@ Definition roundtrip_ref_prog : val :=
Section roundtrip_ref.
Context `{!heapGS Σ, !chanG Σ}.
- Definition iProto_roundtrip_ref : gmap nat (iProto Σ) :=
- <[0 := (<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
- <(Recv, 2)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto]>
- (<[1 := (<(Recv, 0) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
- <(Send, 2)> MSG #l {{ l ↦ #(x+1) }}; END)%proto]>
- (<[2 := (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
- <(Send, 0)> MSG #() {{ l ↦ #(x+1) }}; END)%proto]> ∅)).
+ Definition iProto_roundtrip_ref : list (iProto Σ) :=
+ [(<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Recv, 2)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto;
+ (<(Recv, 0) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Send, 2)> MSG #l {{ l ↦ #(x+1) }}; END)%proto;
+ (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ (l ↦ #x)%I }} ;
+ <(Send, 0)> MSG #() {{ l ↦ #(x+1) }}; END)%proto].
Lemma iProto_roundtrip_ref_consistent :
⊢ iProto_consistent iProto_roundtrip_ref.
@@ -95,17 +87,8 @@ Section roundtrip_ref.
{{{ True }}} roundtrip_ref_prog #() {{{ RET #42 ; True }}}.
Proof using chanG0.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_smart_apply (new_chan_spec 3 iProto_roundtrip_ref with "[]").
- { lia. }
- { set_solver. }
- { iApply iProto_roundtrip_ref_consistent. }
- iIntros (cs) "Hcs".
- wp_smart_apply (get_chan_spec _ 0 with "Hcs"); [set_solver|].
- iIntros (c0) "[Hc0 Hcs]".
- wp_smart_apply (get_chan_spec _ 1 with "Hcs"); [set_solver|].
- iIntros (c1) "[Hc1 Hcs]".
- wp_smart_apply (get_chan_spec _ 2 with "Hcs"); [set_solver|].
- iIntros (c2) "[Hc2 Hcs]".
+ wp_new_chan iProto_roundtrip_ref with iProto_roundtrip_ref_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
wp_smart_apply (wp_fork with "[Hc1]").
{ iIntros "!>".
wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[$Hl]". }
@@ -188,10 +171,10 @@ Section roundtrip_ref_rec.
(iProto_roundtrip_ref_rec3_aux iProto_roundtrip_ref_rec3).
Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
- Definition iProto_roundtrip_ref_rec : gmap nat (iProto Σ) :=
- <[0 := iProto_roundtrip_ref_rec1]>
- (<[1 := iProto_roundtrip_ref_rec2]>
- (<[2 := iProto_roundtrip_ref_rec3]> ∅)).
+ Definition iProto_roundtrip_ref_rec : list (iProto Σ) :=
+ [iProto_roundtrip_ref_rec1;
+ iProto_roundtrip_ref_rec2;
+ iProto_roundtrip_ref_rec3].
Lemma iProto_roundtrip_ref_rec_consistent :
⊢ iProto_consistent iProto_roundtrip_ref_rec.
@@ -210,7 +193,6 @@ Section roundtrip_ref_rec.
iIntros "Hloc". iSplit; [done|].
replace (x + 1 + 1)%Z with (x+2)%Z by lia. iFrame.
rewrite -iProto_roundtrip_ref_rec2_unfold.
- do 2 clean_map 0. do 2 clean_map 1. do 2 clean_map 2.
iApply "IH".
Qed.
@@ -218,17 +200,8 @@ Section roundtrip_ref_rec.
{{{ True }}} roundtrip_ref_rec_prog #() {{{ RET #42 ; True }}}.
Proof using chanG0.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_smart_apply (new_chan_spec 3 iProto_roundtrip_ref_rec with "[]").
- { lia. }
- { set_solver. }
- { iApply iProto_roundtrip_ref_rec_consistent. }
- iIntros (cs) "Hcs".
- wp_smart_apply (get_chan_spec _ 0 with "Hcs"); [set_solver|].
- iIntros (c0) "[Hc0 Hcs]".
- wp_smart_apply (get_chan_spec _ 1 with "Hcs"); [set_solver|].
- iIntros (c1) "[Hc1 Hcs]".
- wp_smart_apply (get_chan_spec _ 2 with "Hcs"); [set_solver|].
- iIntros (c2) "[Hc2 Hcs]".
+ wp_new_chan iProto_roundtrip_ref_rec with iProto_roundtrip_ref_rec_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
wp_smart_apply (wp_fork with "[Hc1]").
{ iIntros "!>". wp_pure _. iLöb as "IH".
wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
@@ -258,13 +231,13 @@ Definition smuggle_ref_prog : val :=
Section smuggle_ref.
Context `{!heapGS Σ, !chanG Σ}.
- Definition iProto_smuggle_ref : gmap nat (iProto Σ) :=
- <[0 := (<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ l ↦ #x }} ;
- <(Recv,1)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto]>
- (<[1 := (<(Recv, 0) @ (v:val)> MSG v ; <(Send,2)> MSG v ;
- <(Recv, 2)> MSG #(); <(Send,0)> MSG #() ; END)%proto]>
- (<[2 := (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ l ↦ #x }} ;
- <(Send,1)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto]> ∅)).
+ Definition iProto_smuggle_ref : list (iProto Σ) :=
+ [(<(Send, 1) @ (l:loc) (x:Z)> MSG #l {{ l ↦ #x }} ;
+ <(Recv,1)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto;
+ (<(Recv, 0) @ (v:val)> MSG v ; <(Send,2)> MSG v ;
+ <(Recv, 2)> MSG #(); <(Send,0)> MSG #() ; END)%proto;
+ (<(Recv, 1) @ (l:loc) (x:Z)> MSG #l {{ l ↦ #x }} ;
+ <(Send,1)> MSG #() {{ l ↦ #(x+2) }} ; END)%proto].
Lemma iProto_smuggle_ref_consistent :
⊢ iProto_consistent iProto_smuggle_ref.
@@ -274,18 +247,8 @@ Section smuggle_ref.
{{{ True }}} smuggle_ref_prog #() {{{ RET #42 ; True }}}.
Proof using chanG0 heapGS0 Σ.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_smart_apply (new_chan_spec 3 iProto_smuggle_ref with "[]").
- { lia. }
- { set_solver. }
- { iApply iProto_smuggle_ref_consistent. }
- iIntros (cs) "Hcs".
- wp_pures.
- wp_smart_apply (get_chan_spec _ 0 with "Hcs"); [set_solver|].
- iIntros (c0) "[Hc0 Hcs]".
- wp_smart_apply (get_chan_spec _ 1 with "Hcs"); [set_solver|].
- iIntros (c1) "[Hc1 Hcs]".
- wp_smart_apply (get_chan_spec _ 2 with "Hcs"); [set_solver|].
- iIntros (c2) "[Hc2 Hcs]".
+ wp_new_chan iProto_smuggle_ref with iProto_smuggle_ref_consistent
+ as (c0 c1 c2) "Hc0" "Hc1" "Hc2".
wp_smart_apply (wp_fork with "[Hc1]").
{ iIntros "!>". wp_recv (v) as "_". wp_send with "[//]".
wp_recv as "_". by wp_send with "[//]". }
@@ -311,149 +274,57 @@ Section parallel.
0
*)
- Definition iProto_parallel : gmap nat (iProto Σ) :=
- <[0 := (<(Send, 1) @ (x1:Z)> MSG #x1 ;
+ Definition iProto_parallel : list (iProto Σ) :=
+ [(<(Send, 1) @ (x1:Z)> MSG #x1 ;
<(Send, 2) @ (x2:Z)> MSG #x2 ;
<(Recv, 3) @ (y1:Z)> MSG #(x1+y1);
- <(Recv, 4) @ (y2:Z)> MSG #(x2+y2); END)%proto]>
- (<[1 := (<(Recv, 0) @ (x:Z)> MSG #x ;
- <(Send, 3) @ (y:Z)> MSG #(x+y); END)%proto]>
- (<[2 := (<(Recv, 0) @ (x:Z)> MSG #x ;
- <(Send, 4) @ (y:Z)> MSG #(x+y) ; END)%proto]>
- (<[3 := (<(Recv, 1) @ (x:Z)> MSG #x ;
- <(Send, 0)> MSG #x; END)%proto]>
- (<[4 := (<(Recv, 2) @ (x:Z)> MSG #x ;
- <(Send, 0)> MSG #x ; END)%proto]> ∅)))).
+ <(Recv, 4) @ (y2:Z)> MSG #(x2+y2); END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ;
+ <(Send, 3) @ (y:Z)> MSG #(x+y); END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ;
+ <(Send, 4) @ (y:Z)> MSG #(x+y) ; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x; END)%proto;
+ (<(Recv, 2) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x ; END)%proto].
Lemma iProto_parallel_consistent :
⊢ iProto_consistent iProto_parallel.
- Proof.
- rewrite /iProto_parallel.
- iProto_consistent_take_step.
- iIntros (x1) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 1.
- iProto_consistent_take_step.
- - iIntros (x2) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 2.
- iProto_consistent_take_step.
- + iIntros (y1) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 1. clean_map 3.
- iProto_consistent_take_step.
- * iIntros (y2) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 4.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 3.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- iProto_consistent_take_step.
- * iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 3. clean_map 0.
- iProto_consistent_take_step.
- iIntros (y2) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 4.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 4. clean_map 0.
- iProto_consistent_take_step.
- + iIntros (y1) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 4.
- iProto_consistent_take_step.
- iIntros (y2) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 1. clean_map 3.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 3. clean_map 0.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 4. clean_map 0.
- iProto_consistent_take_step.
- - iIntros (y1) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 1. clean_map 3.
- iProto_consistent_take_step.
- iIntros (x2) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 2.
- iProto_consistent_take_step.
- + iIntros (y2) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 4.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 3. clean_map 0.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 4. clean_map 0.
- iProto_consistent_take_step.
- + iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 3. clean_map 0.
- iProto_consistent_take_step.
- iIntros (z) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 4.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 4. clean_map 0.
- iProto_consistent_take_step.
- Qed.
+ Proof. rewrite /iProto_parallel. iProto_consistent_take_steps. Qed.
End parallel.
Section two_buyer.
Context `{!heapGS Σ}.
- Definition two_buyer_prot : gmap nat (iProto Σ) :=
- <[0 := (<(Send, 1) @ (title:Z)> MSG #title ;
+ Definition two_buyer_prot : list (iProto Σ) :=
+ [(<(Send, 1) @ (title:Z)> MSG #title ;
<(Recv, 1) @ (quote:Z)> MSG #quote ;
- <(Send, 2) @ (contrib:Z)> MSG #contrib ; END)%proto]>
- (<[1 := (<(Recv, 0) @ (title:Z)> MSG #title ;
+ <(Send, 2) @ (contrib:Z)> MSG #contrib ; END)%proto;
+ (<(Recv, 0) @ (title:Z)> MSG #title ;
<(Send, 0) @ (quote:Z)> MSG #quote ;
<(Send, 2)> MSG #quote ;
<(Recv, 2) @ (b:bool)> MSG #b ;
if b then
<(Recv, 2) @ (address:Z)> MSG #address ;
<(Send, 2) @ (date:Z)> MSG #date ; END
- else END)%proto]>
- (<[2 := (<(Recv, 1) @ (quote:Z)> MSG #quote ;
+ else END)%proto;
+ (<(Recv, 1) @ (quote:Z)> MSG #quote ;
<(Recv, 0) @ (contrib:Z)> MSG #contrib ;
if bool_decide (contrib >= quote/2)%Z then
<(Send, 1)> MSG #true ;
<(Send, 1) @ (address:Z)> MSG #address ;
<(Recv, 1) @ (date:Z)> MSG #date ; END
else
- <(Send, 1)> MSG #false ; END)%proto]>
- ∅)).
+ <(Send, 1)> MSG #false ; END)%proto].
Lemma two_buyer_prot_consistent :
⊢ iProto_consistent two_buyer_prot.
Proof.
- rewrite /two_buyer_prot.
- iProto_consistent_take_step.
- iIntros (title) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 1.
- iProto_consistent_take_step.
- iIntros (quote) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 1.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 1. clean_map 2.
- iProto_consistent_take_step.
- iIntros (contrib) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 2.
- case_bool_decide.
- - iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 1.
- iProto_consistent_take_step.
- iIntros (address) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 1.
- iProto_consistent_take_step.
- iIntros (date) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 1.
- iProto_consistent_take_step.
- - iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 2. clean_map 1.
- iProto_consistent_take_step.
+ rewrite /two_buyer_prot. iProto_consistent_take_steps.
+ case_bool_decide; iProto_consistent_take_steps.
Qed.
-
+
End two_buyer.
Section two_buyer_ref.
@@ -493,47 +364,21 @@ Section two_buyer_ref.
END
else END)%proto.
- Definition two_buyer_ref_prot : gmap nat (iProto Σ) :=
- <[0 := two_buyer_ref_b1_prot]>
- (<[1 := two_buyer_ref_s_prot]>
- (<[2 := two_buyer_ref_b2_prot]>
- ∅)).
+ Definition two_buyer_ref_prot : list (iProto Σ) :=
+ [two_buyer_ref_b1_prot;
+ two_buyer_ref_s_prot;
+ two_buyer_ref_b2_prot].
+ (* TODO: Anonymous variable in this is unsatisfactory *)
Lemma two_buyer_ref_prot_consistent :
⊢ iProto_consistent two_buyer_ref_prot.
Proof.
- rewrite /two_buyer_prot.
- iProto_consistent_take_step.
- iIntros (title) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 1.
- iProto_consistent_take_step.
- iIntros (quote) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 0. clean_map 1.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 1. clean_map 2.
- iProto_consistent_take_step.
- iIntros (l1 amount1 contrib) "Hl1". iExists _,_,_. iSplit; [done|]. iFrame.
- clean_map 0. clean_map 2.
- iProto_consistent_take_step.
- iIntros (b) "Hl1". iExists _. iSplit; [done|]. iFrame.
- clean_map 0. clean_map 2.
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- clean_map 1. clean_map 2.
- destruct b.
- - iProto_consistent_take_step.
- iIntros (l2 amount2 address) "Hl2". iExists _,_,_. iSplit; [done|]. iFrame.
- clean_map 2. clean_map 1.
- iProto_consistent_take_step.
- iIntros (date) "Hl2". iExists _. iSplit; [done|]. iFrame.
- iProto_consistent_take_step.
- - iProto_consistent_take_step.
+ rewrite /two_buyer_prot. iProto_consistent_take_steps.
+ iNext. destruct x4; iProto_consistent_take_steps.
Qed.
End two_buyer_ref.
-
Section forwarder.
Context `{!heapGS Σ}.
@@ -548,36 +393,25 @@ Section forwarder.
*)
- Definition iProto_forwarder : gmap nat (iProto Σ) :=
- <[0 := (<(Send, 1) @ (x:Z)> MSG #x ;
+ Definition iProto_forwarder : list (iProto Σ) :=
+ [(<(Send, 1) @ (x:Z)> MSG #x ;
<(Send, 1) @ (b:bool)> MSG #b ;
- <(Recv, if b then 2 else 3) > MSG #x ; END)%proto]>
- (<[1 := (<(Recv, 0) @ (x:Z)> MSG #x ;
+ <(Recv, if b then 2 else 3) > MSG #x ; END)%proto;
+ (<(Recv, 0) @ (x:Z)> MSG #x ;
<(Recv, 0) @ (b:bool)> MSG #b;
- <(Send, if b then 2 else 3)> MSG #x ; END)%proto]>
- (<[2 := (<(Recv, 1) @ (x:Z)> MSG #x ;
- <(Send, 0)> MSG #x ; END)%proto]>
- (<[3 := (<(Recv, 1) @ (x:Z)> MSG #x ;
- <(Send, 0)> MSG #x ; END)%proto]> ∅))).
+ <(Send, if b then 2 else 3)> MSG #x ; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x ; END)%proto;
+ (<(Recv, 1) @ (x:Z)> MSG #x ;
+ <(Send, 0)> MSG #x ; END)%proto].
+ (* TODO: Anonymous variable in this is unsatisfactory *)
Lemma iProto_forwarder_consistent :
⊢ iProto_consistent iProto_forwarder.
Proof.
rewrite /iProto_forwarder.
- iProto_consistent_take_step.
- iIntros (x) "_". iExists _. iSplit; [done|]. iSplit; [done|].
- iProto_consistent_take_step.
- iIntros ([]) "_".
- - iExists _. iSplit; [done|]. iSplit; [done|].
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- repeat clean_map 0. repeat clean_map 1.
- iProto_consistent_take_steps.
- - iExists _. iSplit; [done|]. iSplit; [done|].
- iProto_consistent_take_step.
- iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- repeat clean_map 0. repeat clean_map 1.
- iProto_consistent_take_steps.
+ iProto_consistent_take_steps.
+ destruct x0; iProto_consistent_take_steps.
Qed.
End forwarder.
@@ -637,11 +471,11 @@ Section forwarder_rec.
(iProto_forwarder_rec_n_aux iProto_forwarder_rec_n).
Proof. apply (fixpoint_unfold _). Qed.
- Definition iProto_forwarder_rec : gmap nat (iProto Σ) :=
- <[0 := iProto_forwarder_rec_0]>
- (<[1 := iProto_forwarder_rec_1]>
- (<[2 := iProto_forwarder_rec_n]>
- (<[3 := iProto_forwarder_rec_n]>∅))).
+ Definition iProto_forwarder_rec : list (iProto Σ) :=
+ [iProto_forwarder_rec_0;
+ iProto_forwarder_rec_1;
+ iProto_forwarder_rec_n;
+ iProto_forwarder_rec_n].
Lemma iProto_forwarder_rec_consistent :
⊢ iProto_consistent iProto_forwarder_rec.
@@ -658,14 +492,11 @@ Section forwarder_rec.
- iExists _. iSplit; [done|]. iSplit; [done|].
iProto_consistent_take_step.
iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- repeat clean_map 1. repeat clean_map 2. repeat clean_map 0.
iNext.
iEval (rewrite iProto_forwarder_rec_1_unfold).
iEval (rewrite iProto_forwarder_rec_n_unfold).
iProto_consistent_take_step.
iIntros "_". iSplit; [done|]. iSplit; [done|].
- repeat clean_map 1. repeat clean_map 2. repeat clean_map 0.
- rewrite (insert_commute _ 2 1); [|done].
iEval (rewrite -iProto_forwarder_rec_1_unfold).
iEval (rewrite -iProto_forwarder_rec_n_unfold).
iEval (rewrite -iProto_forwarder_rec_n_unfold).
@@ -673,14 +504,11 @@ Section forwarder_rec.
- iExists _. iSplit; [done|]. iSplit; [done|].
iProto_consistent_take_step.
iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
- repeat clean_map 1. repeat clean_map 2. repeat clean_map 0.
iNext.
iEval (rewrite iProto_forwarder_rec_1_unfold).
iEval (rewrite iProto_forwarder_rec_n_unfold).
iProto_consistent_take_step.
iIntros "_". iSplit; [done|]. iSplit; [done|].
- repeat clean_map 1. repeat clean_map 3. repeat clean_map 0.
- rewrite (insert_commute _ 3 1); [|done].
iEval (rewrite -iProto_forwarder_rec_1_unfold).
iEval (rewrite -iProto_forwarder_rec_n_unfold).
iEval (rewrite -iProto_forwarder_rec_n_unfold).
diff --git a/multi_actris/examples/leader_election.v b/multi_actris/examples/leader_election.v
index cb21e823d4d481ec63a2fefc575d85f1000644e5..e8810fc0605da0134e8550368a32012fd103daf3 100644
--- a/multi_actris/examples/leader_election.v
+++ b/multi_actris/examples/leader_election.v
@@ -133,98 +133,49 @@ Section ring_leader_election_example.
Definition prot_tail (i_max : nat) : iProto Σ :=
(<(Send,0)> MSG #i_max; END)%proto.
- Definition pre_prot_pool id_max : gmap nat (iProto Σ) :=
- <[0 := (<(Recv,1) @ (id_max : nat)> MSG #id_max ;
+ Definition pre_prot_pool id_max : list (iProto Σ) :=
+ [(<(Recv,1) @ (id_max : nat)> MSG #id_max ;
<(Recv,2)> MSG #id_max ;
<(Recv,3)> MSG #id_max ;
- END)%proto ]>
- (<[1 := prot_tail id_max ]>
- (<[2 := prot_tail id_max ]>
- (<[3 := prot_tail id_max ]> ∅))).
+ END)%proto;
+ prot_tail id_max;
+ prot_tail id_max;
+ prot_tail id_max].
Lemma pre_prot_pool_consistent id_max :
⊢ iProto_consistent (pre_prot_pool id_max).
Proof. rewrite /pre_prot_pool. iProto_consistent_take_steps. Qed.
- Definition prot_pool : gmap nat (iProto Σ) :=
- <[0 := (<(Recv,1) @ (id_max : nat)> MSG #id_max ;
+ Definition prot_pool : list (iProto Σ) :=
+ [(<(Recv,1) @ (id_max : nat)> MSG #id_max ;
<(Recv,2)> MSG #id_max ;
<(Recv,3)> MSG #id_max ;
- END)%proto ]>
- (<[1 := rle_preprot 3 1 2 prot_tail ]>
- (<[2 := rle_prot 1 2 3 prot_tail false ]>
- (<[3 := rle_preprot 2 3 1 prot_tail ]> ∅))).
+ END)%proto;
+ rle_preprot 3 1 2 prot_tail;
+ rle_prot 1 2 3 prot_tail false;
+ rle_preprot 2 3 1 prot_tail].
Lemma prot_pool_consistent : ⊢ iProto_consistent prot_pool.
Proof.
rewrite /prot_pool /rle_preprot.
rewrite !rle_prot_unfold'.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- repeat clean_map 0. repeat clean_map 1.
- repeat clean_map 2. repeat clean_map 3.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- repeat clean_map 0. repeat clean_map 1.
- repeat clean_map 2. repeat clean_map 3.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ case_bool_decide; try lia.
rewrite !rle_prot_unfold'.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- repeat clean_map 0. repeat clean_map 1.
- repeat clean_map 2. repeat clean_map 3.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- repeat clean_map 0. repeat clean_map 1.
- repeat clean_map 2. repeat clean_map 3.
+ iProto_consistent_take_steps.
+ case_bool_decide; try lia.
+ case_bool_decide; try lia.
rewrite !rle_prot_unfold'.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- repeat clean_map 0. repeat clean_map 1.
- repeat clean_map 2. repeat clean_map 3.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- repeat clean_map 0. repeat clean_map 1.
- repeat clean_map 2. repeat clean_map 3.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- iProto_consistent_take_step.
- iProto_consistent_resolve_step.
- repeat clean_map 0. repeat clean_map 1.
- repeat clean_map 2. repeat clean_map 3.
- repeat (rewrite (insert_commute _ _ 3); [|lia]).
- repeat (rewrite (insert_commute _ _ 2); [|lia]).
- repeat (rewrite (insert_commute _ _ 1); [|lia]).
- repeat (rewrite (insert_commute _ _ 0); [|lia]).
- iApply pre_prot_pool_consistent.
+ iProto_consistent_take_steps.
Qed.
Lemma program_spec :
{{{ True }}} program #() {{{ RET #(); True }}}.
Proof.
iIntros (Φ) "_ HΦ". wp_lam.
- wp_smart_apply (new_chan_spec 4 prot_pool);
- [lia|set_solver|iApply prot_pool_consistent|].
- iIntros (cs) "Hcs".
- wp_smart_apply (get_chan_spec _ 0 with "Hcs"); [done|].
- iIntros (c0) "[Hc0 Hcs]".
- wp_smart_apply (get_chan_spec _ 1 with "Hcs"); [done|].
- iIntros (c1) "[Hc1 Hcs]".
- wp_smart_apply (get_chan_spec _ 2 with "Hcs"); [done|].
- iIntros (c2) "[Hc2 Hcs]".
- wp_smart_apply (get_chan_spec _ 3 with "Hcs"); [done|].
- iIntros (c3) "[Hc3 Hcs]".
+ wp_new_chan prot_pool with prot_pool_consistent
+ as (c0 c1 c2 c3) "Hc0" "Hc1" "Hc2" "Hc3".
wp_smart_apply (wp_fork with "[Hc1]").
{ iIntros "!>". wp_smart_apply (init_spec with "Hc1").
iIntros (i') "Hc1". by wp_send with "[//]". }