diff --git a/theories/channel/multi_proto_consistency_examples.v b/theories/channel/multi_proto_consistency_examples.v
index 2813020852a367a2b8f5f099d08f1e34eefd9380..c3c37431b180d58c8bbdd19b2804b2f0518e6571 100644
--- a/theories/channel/multi_proto_consistency_examples.v
+++ b/theories/channel/multi_proto_consistency_examples.v
@@ -372,3 +372,304 @@ Section channel.
   Qed.
 
 End channel.
+
+Section example4.
+  Context `{!heapGS Σ}.
+
+  Definition iProto_example4 : 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]>
+            ∅)).
+
+  Lemma iProto_example4_consistent :
+    ⊢ iProto_consistent (iProto_example4).
+  Proof.
+    rewrite iProto_consistent_unfold.
+    rewrite /iProto_example4.
+    iIntros (i j m1 m2) "Hm1 Hm2".
+    destruct i; last first.
+    { destruct i.
+      { rewrite lookup_total_insert_ne; [|done].
+        rewrite !lookup_total_insert.
+        rewrite !iProto_message_equivI.
+        by iDestruct "Hm1" as (Hieq) "#Hm1". }
+      destruct i.
+      { rewrite lookup_total_insert_ne; [|done].
+        rewrite lookup_total_insert_ne; [|done].
+        rewrite !iProto_message_equivI.
+        by iDestruct "Hm1" as (Hieq) "#Hm1". }
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_empty=> /=.
+      by rewrite iProto_end_message_equivI. }
+    destruct j.
+    { rewrite !lookup_total_insert.
+      rewrite !iProto_message_equivI.
+      by iDestruct "Hm2" as (Hjeq) "#Hm2". }
+    destruct j; last first.
+    { rewrite !lookup_total_insert.
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_insert_ne; [|done].
+      destruct j.
+      { rewrite !lookup_total_insert.
+        rewrite !iProto_message_equivI.
+        by iDestruct "Hm2" as (Hjeq) "#Hm2". }
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_empty=> /=.
+      by rewrite iProto_end_message_equivI. }
+    rewrite !lookup_total_insert.
+    rewrite lookup_total_insert_ne; [|done].
+    rewrite !lookup_total_insert.
+    rewrite !iProto_message_equivI.
+    iDestruct "Hm1" as (Hieq) "#Hm1".
+    iDestruct "Hm2" as (Hjeq) "#Hm2".
+    iIntros (v p1) "Hm1'".
+    iSpecialize ("Hm1" $!v (Next p1)).
+    rewrite !iMsg_base_eq.
+    rewrite !iMsg_exist_eq.
+    iRewrite -"Hm1" in "Hm1'".
+    iDestruct "Hm1'" as (l x <-) "[#Hm1' Hl]". simpl.
+    iSpecialize ("Hm2" $!#l (Next (<Send 2> iMsg_base_def #l
+                                                          (l ↦ #(x+1)) END)))%proto.
+    Unshelve. 2-4: apply _.     (* Why is this needed? *)
+    iExists (<Send 2> iMsg_base_def #l (l ↦ #(x+1)) END)%proto.
+    simpl.
+    iSplitL.
+    { iRewrite -"Hm2". iExists l, x. iSplit; [done|]. iFrame. done. }
+    iNext.
+    rewrite iProto_consistent_unfold.
+    rewrite insert_commute; [|done].
+    rewrite insert_insert.
+    rewrite insert_commute; [|done].
+    rewrite insert_insert.
+    iRewrite -"Hm1'".
+    iClear (m1 m2 Hieq Hjeq p1) "Hm1 Hm2 Hm1'".
+    iIntros (i j m1 m2) "Hm1 Hm2".
+    destruct i.
+    { rewrite !lookup_total_insert.
+      rewrite !iProto_message_equivI.
+      by iDestruct "Hm1" as (Hieq) "#Hm1". }
+    rewrite lookup_total_insert_ne; [|done].
+    destruct i; last first.
+    { destruct i.
+      { rewrite lookup_total_insert_ne; [|done].
+        rewrite lookup_total_insert.
+        rewrite !iProto_message_equivI.
+        by iDestruct "Hm1" as (Hieq) "#Hm1". }
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_empty=> /=.
+      by rewrite iProto_end_message_equivI. }
+    rewrite lookup_total_insert.
+    destruct j.
+    { rewrite lookup_total_insert.
+      rewrite !iProto_message_equivI.
+      by iDestruct "Hm2" as (Hjeq) "#Hm2". }
+    rewrite lookup_total_insert_ne; [|done].
+    destruct j.
+    { rewrite lookup_total_insert.
+      rewrite !iProto_message_equivI.
+      by iDestruct "Hm2" as (Hjeq) "#Hm2". }
+    rewrite lookup_total_insert_ne; [|done].
+    destruct j; last first.
+    { rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_empty.
+      by rewrite iProto_end_message_equivI. }
+    rewrite lookup_total_insert.
+    rewrite !iProto_message_equivI.
+    iDestruct "Hm1" as (Hieq) "#Hm1".
+    iDestruct "Hm2" as (Hjeq) "#Hm2".
+    iIntros (v p1) "Hm1'".
+    iSpecialize ("Hm1" $!v (Next p1)).
+    iRewrite -"Hm1" in "Hm1'".
+    iDestruct "Hm1'" as (<-) "[#Hm1' Hl]".
+    simpl.
+    iSpecialize ("Hm2" $!#l (Next (<Send 0> iMsg_base_def #() (l ↦ #(x+1+1)) END)))%proto.
+    iExists (<Send 0> iMsg_base_def #() (l ↦ #(x+1+1)) END)%proto.
+    Unshelve. 2-4: apply _.    
+    iRewrite -"Hm2".
+    simpl.
+    iSplitL.
+    { iExists l, (x+1)%Z. iSplit; [done|]. iFrame. done. }
+    iNext.
+    rewrite iProto_consistent_unfold.
+    rewrite (insert_commute _ 1 2); [|done].
+    rewrite (insert_commute _ 1 0); [|done].
+    rewrite insert_insert.
+    rewrite (insert_commute _ 2 0); [|done].
+    rewrite (insert_commute _ 2 1); [|done].
+    rewrite insert_insert.
+    iRewrite -"Hm1'".
+    iClear (m1 m2 Hieq Hjeq p1) "Hm1 Hm2 Hm1'".
+    iIntros (i j m1 m2) "Hm1 Hm2".
+    destruct i.
+    { rewrite !lookup_total_insert.
+      rewrite !iProto_message_equivI.
+      by iDestruct "Hm1" as (Hieq) "#Hm1". }
+    rewrite lookup_total_insert_ne; [|done].
+    destruct i.
+    { rewrite lookup_total_insert.
+      by rewrite iProto_end_message_equivI. }
+    rewrite lookup_total_insert_ne; [|done].
+    destruct i; last first.
+    { rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_empty.
+      by rewrite iProto_end_message_equivI. }
+    rewrite lookup_total_insert.
+    destruct j; last first.
+    { rewrite lookup_total_insert_ne; [|done].
+      destruct j.
+      { rewrite lookup_total_insert.
+        by rewrite iProto_end_message_equivI. }
+      rewrite lookup_total_insert_ne; [|done].
+      destruct j.
+      { rewrite lookup_total_insert.
+        rewrite !iProto_message_equivI.
+        by iDestruct "Hm2" as (Hjeq) "#Hm2". }
+      rewrite lookup_total_insert_ne; [|done].
+      rewrite lookup_total_empty.
+      by rewrite iProto_end_message_equivI. }
+    rewrite lookup_total_insert.
+    rewrite !iProto_message_equivI.
+    iDestruct "Hm1" as (Hieq) "#Hm1".
+    iDestruct "Hm2" as (Hjeq) "#Hm2".
+    iIntros (v p1) "Hm1'".
+    iSpecialize ("Hm1" $!v (Next p1)).
+    iRewrite -"Hm1" in "Hm1'".
+    iDestruct "Hm1'" as (<-) "[#Hm1' Hl]".
+    iSpecialize ("Hm2" $!#() (Next END))%proto.
+    iExists END%proto.
+    iRewrite -"Hm2".
+    simpl.
+    replace (x + 1 + 1)%Z with (x+2)%Z by lia.
+    iSplitL; [iFrame;done|].
+    rewrite insert_insert.
+    rewrite insert_commute; [|done].
+    rewrite (insert_commute _ 2 1); [|done].
+    rewrite insert_insert.
+    iNext.
+    iRewrite -"Hm1'".
+    rewrite iProto_consistent_unfold.
+    iClear (m1 m2 Hieq Hjeq p1) "Hm1 Hm2 Hm1'".
+    iIntros (i j m1 m2) "Hm1 Hm2".
+    destruct i.
+    { rewrite lookup_total_insert.
+      by rewrite !iProto_end_message_equivI. }
+    rewrite lookup_total_insert_ne; [|done].
+    destruct i.
+    { rewrite lookup_total_insert.
+      by rewrite !iProto_end_message_equivI. }
+    rewrite lookup_total_insert_ne; [|done].
+    destruct i.
+    { rewrite lookup_total_insert.
+      by rewrite !iProto_end_message_equivI. }
+    rewrite lookup_total_insert_ne; [|done].
+    rewrite lookup_total_empty.
+    by rewrite iProto_end_message_equivI.
+  Qed.
+
+End example4.
+
+Definition roundtrip_ref_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: "l" := recv "c1" #0 in "l" <- !"l" + #1;; send "c1" #2 "l");;
+     Fork (let: "l" := recv "c2" #1 in "l" <- !"l" + #1;; send "c2" #0 #());;
+     let: "l" := ref #40 in send "c0" #1 "l";; recv "c0" #2;; !"l".
+
+Section proof.
+  Context `{!heapGS Σ, !chanG Σ}.
+  Implicit Types p : iProto Σ.
+  Implicit Types TT : tele.
+
+  Lemma roundtrip_ref_prog_spec :
+    {{{ True }}} roundtrip_ref_prog #() {{{ RET #42 ; True }}}.
+  Proof using chanG0.
+    iIntros (Φ) "_ HΦ". wp_lam.
+    wp_smart_apply (new_chan_spec 3 iProto_example4 with "[]").
+    { intros i Hle. destruct i as [|[|[]]]; try set_solver. lia. }
+    { iApply iProto_example4_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_example4.
+    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_smart_apply
+        (recv_spec (TT:=[tele loc Z]) c1 0
+                   (tele_app (λ (l : loc) (x:Z), #l))
+                   (tele_app (λ (l : loc) (x:Z), l ↦ #x)%I)
+                   (tele_app (λ (l : loc) (x:Z), _))
+          with "Hc1").
+      iIntros (x') "[Hc1 Hl]".
+      epose proof (tele_arg_S_inv x') as [l [y' ->]]. simpl.
+      epose proof (tele_arg_S_inv y') as [x [[] ->]]. simpl.
+      wp_load. wp_store.
+      wp_smart_apply (send_spec_tele (TT:=[tele]) c1 2
+                                     ([tele_arg])
+                                     (λ _, #l)
+                                     (λ _, l ↦ #(x+1))%I
+                                     (λ _, _) with "[$Hc1 $Hl]").
+      by iIntros "_". }
+    wp_smart_apply (wp_fork with "[Hc2]").
+    { iIntros "!>".
+      wp_smart_apply
+        (recv_spec (TT:=[tele loc Z]) c2 1
+                   (tele_app (λ (l : loc) (x:Z), #l))
+                   (tele_app (λ (l : loc) (x:Z), l ↦ #x)%I)
+                   (tele_app (λ (l : loc) (x:Z), _))
+          with "Hc2").
+      iIntros (x') "[Hc2 Hl]".
+      epose proof (tele_arg_S_inv x') as [l [y' ->]]. simpl.
+      epose proof (tele_arg_S_inv y') as [x [[] ->]]. simpl.
+      wp_load. wp_store.
+      wp_smart_apply (send_spec_tele (TT:=[tele]) c2 0
+                                     ([tele_arg])
+                                     (λ _, #())
+                                     (λ _, l ↦ #(x+1))%I
+                                     (λ _, _) with "[$Hc2 $Hl]").
+      by iIntros "_". }
+    wp_alloc l as "Hl".
+    wp_smart_apply
+      (send_spec_tele (TT:=[tele l Z]) c0 1 ([tele_arg l ; 40%Z])
+                      (tele_app (λ (l:loc) (x:Z), #l))
+                      (tele_app (λ (l:loc) (x:Z), l ↦ #x)%I)
+                      (tele_app (λ (l:loc) (x:Z), _))
+                   with "[$Hc0 $Hl]").
+    iIntros "Hc0".
+    wp_smart_apply (recv_spec (TT:=[tele]) c0 2
+                              (λ _, #()) (λ _, l ↦ #(40 + 2))%I (λ _, _)
+                      with "Hc0").
+    iIntros (_) "[Hc0 Hl]". wp_load. by iApply "HΦ".
+  Qed.
+
+End proof.