Added another example for channel delegation

theories/examples/basics.v

@@ -49,6 +49,14 @@ Definition prog_dep_del_2 : val := λ: <>,
     let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
   send "c1" "c2";; recv "c1";; recv "c2".
 
+Definition prog_dep_del_3 : val := λ: <>,
+  let: "c1" := start_chan (λ: "c1'",
+    send (recv "c1'") (recv "c1'");;
+    send "c1'" #()) in
+  let: "c2" := start_chan (λ: "c2'",
+    let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
+  send "c1" #40;; send "c1" "c2";; recv "c1";; recv "c2".
+
 (** Loops *)
 Definition prog_loop : val := λ: <>,
   let: "c" := start_chan (λ: "c'",
@@ -107,6 +115,12 @@ Definition prot_dep_del_2 : iProto Σ :=
    <?> MSG #() {{ c ↣ <?> MSG #42; END }};
    END)%proto.
 
+Definition prot_dep_del_3 : iProto Σ :=
+  (<!> x : Z, MSG #x {{ True }};
+   <!> c : val, MSG c {{ c ↣ prot_dep }};
+   <?> MSG #() {{ c ↣ <?> MSG #(x+2); END }};
+   END)%proto.
+
 Definition prot_loop_aux (rec : iProto Σ) : iProto Σ :=
   (<!> x : Z, MSG #x; <?> MSG #(x + 2); rec)%proto.
 Instance prot_loop_contractive : Contractive prot_loop_aux.
@@ -194,6 +208,16 @@ Proof.
   wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
 
+Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  wp_apply (start_chan_proto_spec prot_dep_del_3); iIntros (c) "Hc".
+  { wp_recv (x) as "_". wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
+  wp_apply (start_chan_proto_spec prot_dep); iIntros (c2) "Hc2".
+  { wp_recv (x) as "_". by wp_send with "[//]". }
+  wp_send with "[//]". wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
+Qed.
+
 Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.