Commit fb14f07d by Robbert Krebbers

Another delegation example.

parent a0bc4d00
Pipeline #21278 passed with stage
in 17 minutes and 42 seconds
 ... ... @@ -41,6 +41,14 @@ Definition prog_dep_del : val := λ: <>, let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'". Definition prog_dep_del_2 : val := λ: <>, let: "c1" := start_chan (λ: "c1'", send (recv "c1'") #40;; send "c1'" #()) in let: "c2" := start_chan (λ: "c2'", let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in send "c1" "c2";; recv "c1";; recv "c2". (** Loops *) Definition prog_loop : val := λ: <>, let: "c" := start_chan (λ: "c'", ... ... @@ -94,6 +102,11 @@ Definition prot_dep_ref : iProto Σ := Definition prot_dep_del : iProto Σ := ( c : val, MSG c {{ c ↣ prot_dep }}; END)%proto. Definition prot_dep_del_2 : iProto Σ := ( c : val, MSG c {{ c ↣ prot_dep }}; MSG #() {{ c ↣ MSG #42; 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. ... ... @@ -171,6 +184,16 @@ Proof. by iApply "HΦ". Qed. Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}. Proof. iIntros (Φ) "_ HΦ". wp_lam. wp_apply (start_chan_proto_spec prot_dep_del_2); iIntros (c) "Hc". { 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 "[\$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. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment