Added multi channels and more

theories/channel/multi_channel.v

+(** This file contains the definition of the channels, encoded as a pair of
+lock-protected buffers, and their primitive proof rules. Moreover:
+
+- It defines the connective [c ↣ prot] for ownership of channel endpoints,
+  which describes that channel endpoint [c] adheres to protocol [prot].
+- It proves Actris's specifications of [send] and [recv] w.r.t. dependent
+  separation protocols.
+
+An encoding of the usual (binary) choice connectives [prot1 <{Q1}+{Q2}> prot2]
+and [prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in
+this file.
+
+In this file we define the three message-passing connectives:
+
+- [new_chan] creates references to two empty buffers and a lock, and returns a
+  pair of endpoints, where the order of the two references determines the
+  polarity of the endpoints.
+- [send] takes an endpoint and adds an element to the first buffer.
+- [recv] performs a busy loop until there is something in the second buffer,
+  which it pops and returns, locking during each peek.
+
+It is additionaly shown that the channel ownership [c ↣ prot] is closed under
+the subprotocol relation [⊑] *)
+From iris.algebra Require Import gmap excl_auth gmap_view.
+From iris.heap_lang Require Export primitive_laws notation.
+From iris.heap_lang Require Export proofmode.
+From iris.heap_lang.lib Require Import spin_lock.
+From actris.utils Require Export llist.
+From actris.channel Require Import multi_proto_model.
+From actris.channel Require Export multi_proto.
+Set Default Proof Using "Type".
+
+(* TODO: Update new_chan definition to use pointers with offsets *)
+(** * The definition of the message-passing connectives *)
+Definition new_chan : val :=
+  λ: "n",
+    let: "l" := AllocN ("n"*"n") NONEV in
+    let: "xxs" := lnil #() in
+    (rec: "go1" "i" := if: "i" = "n" then #() else
+       let: "xs" := lnil #() in
+       (rec: "go2" "j" := if: "j" = "n" then #() else
+          lcons ("l" +ₗ ("i"*"n"+"j"), "l" +ₗ ("j"*"n"+"i")) "xs";;
+          "go2" ("j"+#1)) #0;;
+       lcons "xs" "xxs";;
+       "go1" ("i"+#1)) #0;; "xxs".
+
+Definition wait : val :=
+  rec: "go" "c" :=
+    match: !"c" with
+      NONE => #()
+    | SOME <> => "go" "c"
+    end.
+
+Definition send : val :=
+  λ: "c" "i" "v",
+    let: "len" := Fst "c" in
+    if: "i" < "len" then
+      let: "l" := Fst (! ((Snd "c") +ₗ "i")) in
+      "l" <- SOME "v";; wait "l"
+    (* OBS: Hacky *)
+    else (rec: "go" <> := "go" #())%V #().
+
+Definition recv : val :=
+  rec: "go" "c" "i" :=
+    let: "len" := Fst "c" in
+    if: "i" < "len" then
+      let: "l" := Snd (! ((Snd "c") +ₗ "i")) in
+      let: "v" := Xchg "l" NONEV in
+      match: "v" with
+        NONE => "go" "c" "i"
+      | SOME "v" => "v"
+      end
+    (* OBS: Hacky *)
+    else (rec: "go" <> := "go" #())%V #().
+
+(** * Setup of Iris's cameras *)
+Class proto_exclG Σ V :=
+  protoG_exclG ::
+    inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
+
+Definition proto_exclΣ V := #[
+  GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
+].
+
+Class chanG Σ := {
+  chanG_proto_exclG :: proto_exclG Σ val;
+  chanG_tokG :: inG Σ (exclR unitO);
+  chanG_protoG :: protoG Σ val;
+}.
+Definition chanΣ : gFunctors := #[ proto_exclΣ val; protoΣ val; GFunctor (exclR unitO) ].
+Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
+Proof. solve_inG. Qed.
+
+(** * Definition of the pointsto connective *)
+Notation iProto Σ := (iProto Σ val).
+Notation iMsg Σ := (iMsg Σ val).
+
+Definition tok `{!chanG Σ} (γ : gname) : iProp Σ := own γ (Excl ()).
+
+Definition chan_inv `{!heapGS Σ, !chanG Σ} γ γE γt i j (l:loc) : iProp Σ :=
+  (l ↦ NONEV ∗ tok γt) ∨
+  (∃ v m, l ↦ SOMEV v ∗
+            iProto_own γ i (<Send j> m)%proto ∗
+            (∃ 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) (i:nat) (p : iProto Σ) : iProp Σ :=
+  ∃ γ γE1 γE2 γt1 γt2 (l:loc) ls,
+    ⌜ c = PairV #(length ls) #l ⌝ ∗
+    inv (nroot.@"ctx") (iProto_ctx γ) ∗
+    l ↦∗ ls ∗
+    ([∗list] j ↦ v ∈ ls, 
+       ∃ (l1 l2 : loc),
+         ⌜v = PairV #l1 #l2⌝ ∗
+         inv (nroot.@"p") (chan_inv γ γE1 γt1 i j l1) ∗
+         inv (nroot.@"p") (chan_inv γ γE2 γt2 j i l2)) ∗
+    (* llist (λ l v, *)
+    (*          ∃ (j:nat) (l1 l2 : loc), *)
+    (*            ⌜l = (j,(l1,l2))⌝ ∗ ⌜v = PairV #l1 #l2⌝ ∗ *)
+    (*            inv (nroot.@"p") (chan_inv γ γE1 γt1 i j l1) ∗ *)
+    (*            inv (nroot.@"p") (chan_inv γ γE2 γt2 j i l2)) l *)
+    (*       (zip (seq 0 (length ls)) ls) ∗ *)
+    own γE1 (●E (Next p)) ∗ own γE1 (◯E (Next p)) ∗
+    iProto_own γ i p.
+Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
+Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
+Definition iProto_pointsto_eq :
+  @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
+Arguments iProto_pointsto {_ _ _} _ _ _%proto.
+Global Instance: Params (@iProto_pointsto) 4 := {}.
+Notation "c ↣{ i } p" := (iProto_pointsto c i p)
+  (at level 20, format "c  ↣{  i  }  p").
+
+Section channel.
+  Context `{!heapGS Σ, !chanG Σ}.
+  Implicit Types p : iProto Σ.
+  Implicit Types TT : tele.
+
+  Global Instance iProto_pointsto_ne c i : NonExpansive (iProto_pointsto c i).
+  Proof. rewrite iProto_pointsto_eq. solve_proper. Qed.
+  Global Instance iProto_pointsto_proper c i : Proper ((≡) ==> (≡)) (iProto_pointsto c i).
+  Proof. apply (ne_proper _). Qed.
+
+  (* Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2. *)
+  (* Proof. *)
+  (*   rewrite iProto_pointsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]". *)
+  (*   iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk". *)
+  (*   by iApply (iProto_own_le with "H"). *)
+  (* Qed. *)
+
+  (** ** Specifications of [send] and [recv] *)
+  Lemma new_chan_spec (n:nat) (ps:gmap nat (iProto Σ)) :
+    (∀ i, i < n → is_Some (ps !! i)) →
+    {{{ iProto_consistent ps }}}
+      new_chan #n
+    {{{ cs ls, RET #cs;
+        ⌜length ls = n⌝ ∗ cs ↦∗ ls ∗
+        [∗list] i ↦ l ∈ ls, l ↣{i} (ps !!! i) }}}.
+  Proof. Admitted.
+
+  Lemma own_prot_excl γ i (p1 p2 : iProto Σ) :
+    own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
+    own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p2))) -∗
+    False.
+  Proof. Admitted.
+
+  Lemma send_spec c i j v p :
+    {{{ c ↣{i} <Send j> MSG v; p }}}
+      send c #j v
+    {{{ RET #(); c ↣{i} p }}}.
+  Proof.
+    rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+    iDestruct "Hc" as
+      (γ γE1 γE2 γt1 γt2 l ls ->) "(#IH & Hl & Hls & H● & H◯ & Hown)".
+    wp_pures.
+    case_bool_decide; last first.
+    { wp_pures. iClear "IH H● H◯ Hown HΦ Hls Hl".
+      iLöb as "IH". wp_lam. iApply "IH". }
+    (* assert (is_Some ((zip (seq 0 (length ls)) ls) !! j)) as [l' HSome]. *)
+    (* { apply lookup_lt_is_Some_2. lia. } *)
+    (* wp_smart_apply (llookup_spec with "Hls"); [done|]. *)
+    assert (is_Some (ls !! j)) as [l' HSome].
+    { apply lookup_lt_is_Some_2. lia. }
+    wp_pures.
+    wp_smart_apply (wp_load_offset with "Hl").
+    { done. } 
+    iIntros "Hl". wp_pures.
+    iDestruct (big_sepL_lookup_acc with "Hls") as "[Hj Hls]"; [done|].
+    iDestruct "Hj" as (l1 l2 ->) "#[IHl1 IHl2]". 
+    iDestruct ("Hls" with "[]") as "Hls".
+    { iExists _, _. iFrame "#". done. }
+    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)".
+        wp_store.
+        rewrite /iProto_own.
+        iDestruct (own_prot_excl with "Hown Hown'") as "H". done.
+      - iDestruct "HIp" as (p') "(>Hl' & Hown' & HIp)".
+        wp_store.
+        rewrite /iProto_own.
+        iDestruct (own_prot_excl with "Hown Hown'") as "H". done. }
+    iDestruct "HIp" as "[>Hl' Htok]".
+    wp_store.
+    iMod (own_update_2 with "H● H◯") as "[H● H◯]".
+    { apply excl_auth_update. }
+    iModIntro.
+    iSplitL "Hl' H● Hown". 
+    { iRight. iLeft. iIntros "!>". iExists _, _. iFrame.
+      iExists _. iFrame. rewrite iMsg_base_eq. simpl. done. }
+    wp_pures.
+    iLöb as "HL".
+    wp_lam.
+    wp_bind (Load _).
+    iInv "IHl1" as "HIp".
+    iDestruct "HIp" as "[HIp|HIp]".
+    { 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)".
+      wp_load. iModIntro.
+      iSplitL "Hl' Hown HIp".
+      { iRight. iLeft. iExists _, _. iFrame. }
+      wp_pures. iApply ("HL" with "HΦ Hl Hls Htok H◯").
+    - iDestruct "HIp" as (p') "(>Hl' & Hown & H●)".
+      wp_load.
+      iModIntro.
+      iSplitL "Hl' Htok".
+      { iLeft. iFrame. }
+      iDestruct (own_valid_2 with "H● H◯") as "#Hagree".
+      iDestruct (excl_auth_agreeI with "Hagree") as "Hagree'".
+      wp_pures.
+      iMod (own_update_2 with "H● H◯") as "[H● H◯]".
+      { apply excl_auth_update. }
+      iModIntro.
+      iApply "HΦ".
+      iExists _, _, _, _, _, _, _.
+      iSplit; [done|]. iFrame "#∗".
+      iRewrite -"Hagree'". done.
+  Qed.
+  
+  (* Lemma send_spec_tele {TT} c (tt : TT) *)
+  (*       (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) : *)
+  (*   {{{ c ↣ (<!.. x > MSG v x {{ P x }}; p x) ∗ P tt }}} *)
+  (*     send c (v tt) *)
+  (*   {{{ RET #(); c ↣ (p tt) }}}. *)
+  (* Proof. *)
+  (*   iIntros (Φ) "[Hc HP] HΦ". *)
+  (*   iDestruct (iProto_pointsto_le _ _ (<!> MSG v tt; p tt)%proto with "Hc [HP]") *)
+  (*     as "Hc". *)
+  (*   { iIntros "!>". *)
+  (*     iApply iProto_le_trans. *)
+  (*     iApply iProto_le_texist_intro_l. *)
+  (*     by iFrame "HP". } *)
+  (*   by iApply (send_spec with "Hc"). *)
+  (* Qed. *)
+
+  Lemma recv_spec {TT} c i j (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣{i} <(Recv j) @.. x> MSG v x {{ ▷ P x }}; p x }}}
+      recv c #j
+    {{{ x, RET v x; c ↣{i} p x ∗ P x }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ". iLöb as "HL". wp_lam.
+    rewrite iProto_pointsto_eq.
+    iDestruct "Hc" as
+      (γ γE1 γE2 γt1 γt2 l ls ->) "(#IH & Hl & Hls & H● & H◯ & Hown)".
+    wp_pures.
+    case_bool_decide; last first.
+    { wp_pures. iClear "IH H● H◯ Hown HΦ Hls Hl".
+      iLöb as "IH". wp_lam. iApply "IH". }
+    wp_pures.
+    assert (is_Some (ls !! j)) as [l' HSome].
+    { apply lookup_lt_is_Some_2. lia. }
+    wp_smart_apply (wp_load_offset with "Hl").
+    { done. } 
+    iIntros "Hl". wp_pures.
+    iDestruct (big_sepL_lookup_acc with "Hls") as "[Hj Hls]"; [done|].
+    iDestruct "Hj" as (l1 l2 ->) "#[IHl1 IHl2]". 
+    iDestruct ("Hls" with "[]") as "Hls".
+    { iExists _, _. iFrame "#". done. }    
+    wp_pures.
+    wp_bind (Xchg _ _).
+    iInv "IHl2" as "HIp".
+    iDestruct "HIp" as "[HIp|HIp]".
+    { iDestruct "HIp" as ">[Hl' Htok]".
+      wp_xchg.
+      iModIntro.
+      iSplitL "Hl' Htok".
+      { iLeft. iFrame. }
+      wp_pures. iApply ("HL" with "[H● H◯ Hown Hls Hl] HΦ").
+      iExists _, _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+    iDestruct "HIp" as "[HIp|HIp]"; last first.
+    { iDestruct "HIp" as (p') "[>Hl' [Hown' H◯']]".
+      wp_xchg.
+      iModIntro.
+      iSplitL "Hl' Hown' H◯'".
+      { iRight. iRight. iExists _. iFrame. }
+      wp_pures. iApply ("HL" with "[H● H◯ Hown Hls Hl] HΦ").
+      iExists _, _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+    iDestruct "HIp" as (w m) "(>Hl' & Hown' & HIp)".
+    iDestruct "HIp" as (p') "[Hm Hp']".
+    iInv "IH" as "Hctx".
+    wp_xchg.
+    iMod (iProto_step with "Hctx Hown' Hown Hm") as
+      (p'') "(Hm & Hctx & Hown & Hown')".
+    iModIntro.
+    iSplitL "Hctx"; [done|].
+    iModIntro.
+    iSplitL "Hl' Hown Hp'".
+    { iRight. iRight. iExists _. iFrame. }
+    wp_pure _.
+    rewrite iMsg_base_eq.
+    iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
+    wp_pures.
+    iMod (own_update_2 with "H● H◯") as "[H● H◯]".
+    { apply excl_auth_update. }
+    iModIntro. iApply "HΦ".
+    iFrame.
+    iExists _, _, _, _, _, _, _. iSplit; [done|].
+    iRewrite "Hp". iFrame "#∗".
+  Qed.
+
+End channel.

theories/channel/multi_proto_consistency_examples.v

@@ -3,15 +3,15 @@ From iris.proofmode Require Import proofmode.
 From iris.base_logic Require Export lib.iprop.
 From iris.base_logic Require Import lib.own.
 From iris.program_logic Require Import language.
-From actris.channel Require Import multi_proto_model multi_proto.
+From actris.channel Require Import multi_proto_model multi_proto multi_channel.
 Set Default Proof Using "Type".
 Export action.
 
-Definition iProto_example1 {Σ V} : gmap nat (iProto Σ V) :=
+Definition iProto_example1 {Σ} : gmap nat (iProto Σ) :=
   ∅.
 
-Lemma iProto_example1_consistent {Σ V} :
-  ⊢ iProto_consistent (@iProto_example1 Σ V).
+Lemma iProto_example1_consistent {Σ} :
+  ⊢ iProto_consistent (@iProto_example1 Σ).
 Proof.
   rewrite iProto_consistent_unfold.
   iIntros (i j m1 m2) "Hi Hj".
@@ -19,13 +19,13 @@ Proof.
   by rewrite iProto_end_message_equivI.
 Qed.
 
-Definition iProto_example2 `{!invGS Σ} (P : iProp Σ) : gmap nat (iProto Σ Z) :=
-  <[0 := (<(Send 1) @ (x:Z)> MSG x {{ P }} ; END)%proto ]>
-  (<[1 := (<(Recv 0) @ (x:Z)> MSG x {{ P }} ; END)%proto ]>
+Definition iProto_example2 `{!invGS Σ} (P : iProp Σ) : gmap nat (iProto Σ) :=
+  <[0 := (<(Send 1) @ (x:Z)> MSG #x {{ P }} ; END)%proto ]>
+  (<[1 := (<(Recv 0) @ (x:Z)> MSG #x {{ P }} ; END)%proto ]>
    ∅).
 
 Lemma iProto_example2_consistent `{!invGS Σ} (P : iProp Σ) :
-  ⊢ iProto_consistent (@iProto_example2 _ Σ invGS0 P).
+  ⊢ iProto_consistent (@iProto_example2 Σ invGS0 P).
 Proof.
   rewrite iProto_consistent_unfold.
   rewrite /iProto_example2.
@@ -102,14 +102,14 @@ Proof.
     done.
 Qed.
 
-Definition iProto_example3 `{!invGS Σ}  : gmap nat (iProto Σ Z) :=
-  <[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_example3 `{!invGS Σ} : 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 ]>
     ∅)).
 
 Lemma iProto_example3_consistent `{!invGS Σ} :
-  ⊢ iProto_consistent (@iProto_example3 _ Σ invGS0).
+  ⊢ iProto_consistent (@iProto_example3 Σ invGS0).
 Proof.
   rewrite iProto_consistent_unfold.
   rewrite /iProto_example3.
@@ -157,8 +157,8 @@ Proof.
   rewrite !iMsg_exist_eq.
   iRewrite -"Hm1" in "Hm1'".
   iDestruct "Hm1'" as (x Heq) "[#Hm1' _]".
-  iSpecialize ("Hm2" $!v (Next (<Send 2> iMsg_base_def x True END)))%proto.
-  iExists (<Send 2> iMsg_base_def x True END)%proto.
+  iSpecialize ("Hm2" $!v (Next (<Send 2> iMsg_base_def #x True END)))%proto.
+  iExists (<Send 2> iMsg_base_def #x True END)%proto.
   iRewrite -"Hm2".
   simpl.
   iSplitL.
@@ -210,8 +210,8 @@ Proof.
   iSpecialize ("Hm1" $!v (Next p1)).
   iRewrite -"Hm1" in "Hm1'".
   iDestruct "Hm1'" as (Heq) "[#Hm1' _]".
-  iSpecialize ("Hm2" $!v (Next (<Send 0> iMsg_base_def x True END)))%proto.
-  iExists (<Send 0> iMsg_base_def x True END)%proto.
+  iSpecialize ("Hm2" $!v (Next (<Send 0> iMsg_base_def #x True END)))%proto.
+  iExists (<Send 0> iMsg_base_def #x True END)%proto.
   iRewrite -"Hm2".
   simpl.
   iSplitL.
@@ -291,3 +291,66 @@ Proof.
   rewrite lookup_total_empty.
   by rewrite iProto_end_message_equivI.
 Qed.
+
+Definition roundtrip_prog : val :=
+  λ: <>,
+     let: "cs" := new_chan #3 in
+     let: "c0" := ! ("cs" +ₗ #0) in 
+     let: "c1" := ! ("cs" +ₗ #1) in 
+     let: "c2" := ! ("cs" +ₗ #2) in 
+     Fork (let: "x" := recv "c1" #0 in send "c1" #2 "x");;
+     Fork (let: "x" := recv "c2" #1 in send "c2" #0 "x");;
+     send "c0" #1 #42;;
+     recv "c0" #2.
+
+Section channel.
+  Context `{!heapGS Σ, !chanG Σ}.
+  Implicit Types p : iProto Σ.
+  Implicit Types TT : tele.
+
+  Lemma roundtrip_prog_spec :
+    {{{ True }}} roundtrip_prog #() {{{ RET #42 ; True }}}.
+  Proof.
+    iIntros (Φ) "_ HΦ". wp_lam.
+    wp_pures.
+    wp_apply (new_chan_spec 3 iProto_example3 with "[]").
+    { intros i Hle. destruct i as [|[|[]]]; try set_solver. lia. }
+    { iApply iProto_example3_consistent. }
+    iIntros (cs ls) "[%Hlen [Hcs Hls]]".
+    assert (is_Some (ls !! 0)) as [c0 HSome0].
+    { apply lookup_lt_is_Some_2. lia. }
+    assert (is_Some (ls !! 1)) as [c1 HSome1].
+    { apply lookup_lt_is_Some_2. lia. }
+    assert (is_Some (ls !! 2)) as [c2 HSome2].
+    { apply lookup_lt_is_Some_2. lia. }
+    wp_smart_apply (wp_load_offset _ _ _ _ 0 with "Hcs"); [done|].
+    iIntros "Hcs".
+    wp_smart_apply (wp_load_offset _ _ _ _ 1 with "Hcs"); [done|].
+    iIntros "Hcs".
+    wp_smart_apply (wp_load_offset _ _ _ _ 2 with "Hcs"); [done|].
+    iIntros "Hcs".
+    iDestruct (big_sepL_delete' _ _ 0 with "Hls") as "[Hc0 Hls]"; [set_solver|].
+    iDestruct (big_sepL_delete' _ _ 1 with "Hls") as "[Hc1 Hls]"; [set_solver|].
+    iDestruct (big_sepL_delete' _ _ 2 with "Hls") as "[Hc2 _]"; [set_solver|].
+    iDestruct ("Hc1" with "[//]") as "Hc1".
+    iDestruct ("Hc2" with "[//] [//]") as "Hc2".
+    rewrite /iProto_example3.
+    rewrite !lookup_total_insert.
+    rewrite lookup_total_insert_ne; [|done].
+    rewrite !lookup_total_insert.
+    rewrite lookup_total_insert_ne; [|done].
+    rewrite lookup_total_insert_ne; [|done].
+    rewrite !lookup_total_insert.
+    wp_smart_apply (wp_fork with "[Hc1]").
+    { iIntros "!>". wp_pures.
+      wp_apply (recv_spec c1 _ 0 with "[Hc1]"); [admit|].
+      admit. }
+    wp_smart_apply (wp_fork with "[Hc2]").
+    { iIntros "!>". wp_pures.
+      wp_apply (recv_spec c2 _ 1 with "[Hc2]"); [admit|].
+      admit. }
+    wp_pures. wp_apply (send_spec c0 0 1 #42 with "[Hc0]"); [admit|].
+    iIntros "Hc0".
+  Admitted.
+
+End channel.