Guarantees by Construction (Mechanization)

Jules Jacobs

From dlfactris.session_logic Require Export proofmode.
Import TImp TImp.notations.

(** From https://gitlab.mpi-sws.org/iris/actris/-/blob/master/theories/examples/basics.v *)
(** Basic *)
Definition prog : val := λ: <>,
  let: "c" := fork_chan (λ: "c'", send "c'" #42;; close "c'") in
  let: "x" := recv "c" in wait "c";; "x".

Definition prog_prot : prot :=
  <?> MSG #42 ; END?.

Lemma prog_spec : {{{ emp }}} prog #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec. iApply (wp_fork_chan prog_prot); iIntros "!> %c Hc".
  { wp_send. by wp_close. }
  wp_recv. wp_wait!. by iApply "HΦ".
Qed.

(** Tranfering References *)
Definition prog_ref : val := λ: <>,
  let: "c" := fork_chan (λ: "c'", send "c'" (Alloc #42);; close "c'") in
  let: "l" := recv "c" in let: "x" := ! "l" in Free "l";; wait "c";; "x".

Definition prot_ref : prot :=
  <? (l : loc)> MSG #l {{ l  #42 }}; END?.

Lemma prog_ref_spec : {{{ emp }}} prog_ref #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec. iApply (wp_fork_chan prot_ref); iIntros "!> %c Hc".
  { wp_alloc l as "Hl". wp_send with "[Hl//]". by wp_close. }
  wp_recv (l) as "Hl". wp_load. wp_free. wp_wait!. by iApply "HΦ".
Qed.

(** Delegation, i.e. transfering channels *)
Definition prog_del : val := λ: <>,
  let: "c1" := fork_chan (λ: "c1'",
    let: "c2" := fork_chan (λ: "c2'", send "c1'" "c2'";; close "c1'") in
    send "c2" #42;; close "c2") in
  let: "c2'" := recv "c1" in wait "c1";;
  let: "x" := recv "c2'" in wait "c2'";; "x".

Definition prot_del : prot :=
  <? c> MSG c {{ c  prog_prot }}; END?.

Lemma prog_del_spec : {{{ emp }}} prog_del #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_del); iIntros "!>" (c) "Hc".
  { iApply (wp_fork_chan (dual prog_prot) with "[Hc]"); iIntros "!>" (c2) "Hc2".
    + wp_send with "[$Hc2]". by wp_close.
    + wp_send. by wp_close. }
  wp_recv (c2) as "Hc2". wp_wait. wp_recv. wp_wait!. by iApply "HΦ".
Qed.

(** Dependent protocols *)
Definition prog_dep : val := λ: <>,
  let: "c" := fork_chan (λ: "c'",
    let: "x" := recv "c'" in send "c'" ("x" + #2);; close "c'") in
  send "c" #40;; let: "x" := recv "c" in wait "c";; "x".

Definition prot_dep : prot :=
  <! (x : Z)> MSG #x; <?> MSG #(x + 2); END?.

Lemma prog_dep_spec : {{{ emp }}} prog_dep #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_dep); iIntros "!>" (c) "Hc".
  - wp_recv (x) as "_". wp_send with "[//]". by wp_close.
  - wp_send with "[//]". wp_recv. wp_wait!. by iApply "HΦ".
Qed.

Definition prog_dep_ref : val := λ: <>,
  let: "c" := fork_chan (λ: "c'",
    let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #();; close "c'") in
  let: "l" := Alloc #40 in send "c" "l";; recv "c";;
  let: "x" := !"l" in Free "l";; wait "c";; "x".

Definition prot_dep_ref : prot :=
  <! (l : loc) (x : Z)> MSG #l {{ l  #x }};
  <?> MSG #() {{ l  #(x + 2) }};
  END?.

Lemma prog_dep_ref_spec : {{{ emp }}} prog_dep_ref #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_dep_ref); iIntros "!>" (c) "Hc".
  - wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]". by wp_close.
  - wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
    wp_free. wp_wait!. by iApply "HΦ".
Qed.

Definition prog_dep_del : val := λ: <>,
  let: "c1" := fork_chan (λ: "c1'",
    let: "cc2" := fork_chan (λ: "cc2", send "c1'" "cc2";; close "c1'") in
    let: "x" := recv "cc2" in send "cc2" ("x" + #2);; close "cc2") in
  let: "c2'" := recv "c1" in send "c2'" #40;;
  let: "x" := recv "c2'" in wait "c2'";; wait "c1";; "x".

Definition prot_dep_del : prot :=
  <? c> MSG c {{ c  prot_dep }}; END?.

Lemma prog_dep_del_spec : {{{ emp }}} prog_dep_del #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_dep_del); iIntros "!>" (c) "Hc1".
  - iApply (wp_fork_chan (dual prot_dep) with "[Hc1]"); iIntros "!>" (c2) "Hc2".
    + wp_send with "[$Hc2]". by wp_close.
    + wp_recv. wp_send. by wp_close.
  - wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv. wp_wait. wp_wait!.
    by iApply "HΦ".
Qed.

Definition prog_dep_del_2 : val := λ: <>,
  let: "c1" := fork_chan (λ: "c1'",
    let: "c2" := recv "c1'" in
    send "c2" #40;; send "c1'" #();; close "c1'") in
  let: "c2" := fork_chan (λ: "c2'",
    let: "x" := recv "c2'" in send "c2'" ("x" + #2);; close "c2'") in
  send "c1" "c2";; recv "c1";; wait "c1";; let: "x" := recv "c2" in
  wait "c2";; "x".

Definition prot_dep_del_2 : prot :=
  <! c> MSG c {{ c  prot_dep }};
  <?> MSG #() {{ c  prog_prot }};
  END?.

Lemma prog_dep_del_2_spec : {{{ emp }}} prog_dep_del_2 #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_dep_del_2); iIntros "!>" (c) "Hc".
  { wp_recv (c2) as "Hc2". wp_send. wp_send with "[$Hc2]". by wp_close. }
  iApply (wp_fork_chan prot_dep); iIntros "!>" (c2) "Hc2".
  { wp_recv. wp_send. by wp_close. }
  wp_send with "[$Hc2]". wp_recv as "Hc2". wp_wait. wp_recv. wp_wait!.
  by iApply "HΦ".
Qed.

Definition prog_dep_del_3 : val := λ: <>,
  let: "c1" := fork_chan (λ: "c1'",
    let: "c" := recv "c1'" in let: "y" := recv "c1'" in
    send "c" "y";; send "c1'" #();; close "c1'") in
  let: "c2" := fork_chan (λ: "c2'",
    let: "x" := recv "c2'" in send "c2'" ("x" + #2);; close "c2'") in
  send "c1" "c2";; send "c1" #40;;
  recv "c1";; wait "c1";;
  let: "x" := recv "c2" in wait "c2";; "x".

Definition prot_dep_del_3 : prot :=
  <! c> MSG c {{ c  prot_dep }};
  <! (y : Z)> MSG #y;
  <?> MSG #() {{ c  <?> MSG #(y + 2); END? }};
  END?.

Lemma prog_dep_del_3_spec : {{{ emp }}} prog_dep_del_3 #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_dep_del_3); iIntros "!>" (c1) "Hc1".
  { wp_recv (c2) as "Hc2". wp_recv. wp_send.
    wp_send with "[$Hc2]". by wp_close. }
  iApply (wp_fork_chan prot_dep); iIntros "!>" (c2) "Hc2".
  { wp_recv.  wp_send. by wp_close. }
  wp_send with "[$Hc2]". wp_send. wp_recv as "Hc2".
  wp_wait. wp_recv. wp_wait!. by iApply "HΦ".
Qed.

(** Loops *)
Definition prog_loop : val := λ: <>,
  let: "c" := fork_chan (rec: "go" "c'" :=
    if: recv "c'"
    then let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'"
    else wait "c'") in
  send "c" #true;;
  send "c" #18;;
  let: "x1" := recv "c" in
  send "c" #true;;
  send "c" #20;;
  let: "x2" := recv "c" in
  send "c" #false;;
  close "c";;
  "x1" + "x2".

Definition prot_loop_aux (rec : prot) : prot :=
  (<! (x : Z)> MSG #x; <?> MSG #(x + 2); rec) <+> END!.
Global Instance prot_loop_contractive : Contractive prot_loop_aux.
Proof. solve_prot_contractive. Qed.
Definition prot_loop : prot := fixpoint prot_loop_aux.
Global Instance prot_loop_unfold :
  ProtUnfold prot_loop (prot_loop_aux prot_loop).
Proof. apply prot_unfold_eq, (fixpoint_unfold _). Qed.

Lemma prog_loop_spec : {{{ emp }}} prog_loop #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_loop); iIntros "!> %c Hc".
  - iLöb as "IH". wp_recv (b). destruct b.
    + wp_recv (x). wp_send. by iApply "IH".
    + wp_pures. by wp_wait.
  - wp_send. wp_send. wp_recv. wp_send. wp_send. wp_recv. wp_send. wp_close!.
    by iApply "HΦ".
Qed.

(** Transfering higher-order functions *)
Definition prog_fun : val := λ: <>,
  let: "c" := fork_chan (λ: "c'",
    let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
  let: "r" := Alloc #40 in
  send "c" (λ: <>, !"r");;
  recv "c" #().

Definition prog_fun_del : val := λ: <>,
  let: "c1" := fork_chan (λ: "c1'",
    let: "c2" := fork_chan (λ: "c2'",
      let: "x" := recv "c2'" in send "c2'" ("x" + #2);; close "c2'") in
    let: "x" := recv "c1'" in
    send "c1'"
         (λ: <>, send "c2" "x";;
                  let: "y" := recv "c2" in wait "c2";; "y");; close "c1'") in
  send "c1" #40;; let: "f" := recv "c1" in wait "c1";; "f" #().

Definition prot_fun_del : prot :=
  <! (x : Z)> MSG #x ;
  <? f> MSG f {{ WP f #() {{ v, ⌜⌜ v = #(x + 2) ⌝⌝ }} }}; END?.

Lemma prog_fun_del_spec : {{{ emp }}} prog_fun_del #() {{{ RET #42; emp }}}.
Proof.
  iIntros (Φ) "_ HΦ". wp_rec.
  iApply (wp_fork_chan prot_fun_del); iIntros "!>" (c) "Hc".
  - iApply (wp_fork_chan prot_dep); iIntros "!>" (c2) "Hc2".
    { wp_rec. wp_recv (x). wp_send. by wp_close. }
    wp_recv (x). wp_send with "[Hc2]".
    { wp_rec. wp_send. wp_recv. by wp_wait!. }
    by wp_close.
  - wp_send. wp_recv (f) as "Hf". wp_wait!. iApply "Hf". by iApply "HΦ".
Qed.