diff --git a/theories/examples/basics.v b/theories/examples/basics.v index 965c1045f71a80b9fffdca14cfbd2a7f069d8aa6..fe5ca25da5b94337972171dc62d6e384ad7b2f26 100644 --- a/theories/examples/basics.v +++ b/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.