Multiparty synchronous list

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".