Guarantees by Construction (Mechanization)

Jules Jacobs

From miniactris Require Export sub.
From iris.heap_lang.lib Require Import assert.

Definition new : val := new1.                                                    (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=38eb05cd *)
Definition recv : val := recv1.                                                  (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7b052293 *)
Definition send : val := λ: "l" "v",                                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f79564b2 *)
  let: "l'" := new1 #() in
  send1 "l" ("v","l'");; "l'".
Definition wait : val := recv1.                                                  (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=50d1dd3e *)
Definition close : val := λ: "l", send1 "l" #().                                 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2211b018 *)

Section session_proofs.
  Context `{!heapGS Σ, !chanG Σ}.
  Notation prot := (prot Σ).

  (** ?x  {P}. p *)
  Definition recv_prot {A} (v : A  val) (Φ : A  iPropO Σ) (p : A  prot) : prot := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d628264e *)
    (false, λ r,  x ch', r = (v x, ch')%V  Φ x  is_chan ch' (p x))%I.
  (** !x  {P}. p *)
  Definition send_prot {A} (v : A  val) (Φ : A -d> iPropO Σ) (p : A  prot) : prot := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=40d49a14 *)
    dual (recv_prot v Φ (dual  p)).

  (** End? *)
  Definition wait_prot : prot := (false, λ r, r = #()⌝)%I.                      (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=572d1bdf *)
  (** End! *)
  Definition close_prot : prot := dual wait_prot.                                (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=aa3d152f *)

  Lemma new_spec p :                                                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9a664126 *)
    {{{ True }}} new #() {{{ ch, RET ch; is_chan ch p  is_chan ch (dual p) }}}.
  Proof. apply new1_spec. Qed.

  Lemma recv_spec {A} ch (v : A  val) Φ p :                                     (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1746e1d1 *)
    {{{ is_chan ch (recv_prot v Φ p) }}}
      recv ch
    {{{ x ch', RET (v x, ch'); is_chan ch' (p x)  Φ x }}}.
  Proof.
    iIntros (Ψ) "Hr HΨ". wp_apply (recv1_spec with "Hr").
    iIntros (ch') "(%x&%w&->&?&?)". iApply "HΨ". iFrame.
  Qed.

  Lemma send_spec {A} x ch (v : A  val) Φ p :                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a9ff067d *)
    {{{ is_chan ch (send_prot v Φ p)   Φ x }}}
      send ch (v x)
    {{{ ch', RET ch'; is_chan ch' (p x) }}}.
  Proof.
    iIntros (Ψ) "[Hs HΦ] HΨ". wp_lam. wp_smart_apply (new_spec (p x) with "[//]").
    iIntros (ch') "[H1 H2]". wp_smart_apply (send1_spec with "[$Hs HΦ H2]").
    - simpl. by eauto with iFrame.
    - iIntros "_". wp_seq. by iApply "HΨ".
  Qed.

  Lemma wait_spec ch :                                                           (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a0835460 *)
    {{{ is_chan ch wait_prot }}} wait ch {{{ RET #(); emp }}}.
  Proof.
    iIntros (Ψ) "Hch HΨ". wp_apply (recv1_spec with "Hch").
    iIntros (v') "->". by iApply "HΨ".
  Qed.

  Lemma close_spec ch :                                                          (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8333ad6a *)
    {{{ is_chan ch close_prot }}} close ch {{{ RET #(); emp }}}.
  Proof.
    iIntros (Ψ) "Hch HΨ". wp_lam.
    wp_smart_apply (send1_spec with "[$Hch]"); eauto.
  Qed.

  Lemma subprot_recv {A1 A2} (v1 : A1  val) (v2 : A2  val) Φ1 Φ2 p1 p2 :       (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2574026f *)
    (∀ x1, Φ1 x1 -  x2, v1 x1 = v2 x2  Φ2 x2   subprot (p1 x1) (p2 x2)) -
    subprot (recv_prot v1 Φ1 p1) (recv_prot v2 Φ2 p2).
  Proof.
    iIntros "H". iApply subprot_recv1. iIntros (v).
    iIntros "(%x1 & %ch & → & HΦ1 & Hch)".
    iDestruct ("H" with "HΦ1") as (x2 Heq) "[H1 H2]".
    iExists _,_. iSplit; first rewrite Heq //. iFrame.
    by iApply (subprot_is_chan with "[$]").
  Qed.

  Lemma subprot_send {A1 A2} (v1 : A1  val) (v2 : A2  val) Φ1 Φ2 p1 p2 :       (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=638b12c9 *)
    (∀ x2, Φ2 x2 -  x1, v2 x2 = v1 x1  Φ1 x1   subprot (p1 x1) (p2 x2)) -
    subprot (send_prot v1 Φ1 p1) (send_prot v2 Φ2 p2).
  Proof.
    iIntros "H". rewrite subprot_dual. iApply subprot_recv.
    by setoid_rewrite subprot_dual.
  Qed.

  Lemma subprot_frame_send {A B} (v1 : A  val) (v2 : A  B  val) Φ1 Φ2 Ψ p :   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=67df87fa *)
     subprot (send_prot v1 Φ1  x1, recv_prot (v2 x1) (Φ2 x1) (p x1)))
              (send_prot v1  x1, Φ1 x1   Ψ x1)%I  x1, recv_prot (v2 x1)  x2, Ψ x1  Φ2 x1 x2)%I (p x1))).
  Proof.
    iApply subprot_send. iIntros (x1) "[HΦ1 HΨ]".
    iExists x1. iSplit; first done. iSplitL "HΦ1"; first done.
    iApply subprot_recv. iModIntro. iIntros (x2) "HΦ2".
    iExists x2. iSplit; first done. iFrame.
    iApply subprot_refl.
  Qed.

  Lemma subprot_frame_recv {A B} (v1 : A  val) (v2 : A  B  val) Φ1 Φ2 Ψ p :   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=277cf3dd *)
     subprot (recv_prot v1  x1, Φ1 x1   Ψ x1)%I  x1, send_prot (v2 x1)  x2, Ψ x1  Φ2 x1 x2)%I (p x1)))
              (recv_prot v1 Φ1  x1, send_prot (v2 x1) (Φ2 x1) (p x1))).
  Proof.
    iApply subprot_recv. iIntros (x1) "[HΦ1 HΨ]".
    iExists x1. iSplit; first done. iSplitL "HΦ1"; first done.
    iApply subprot_send. iModIntro. iIntros (x2) "HΦ2".
    iExists x2. iSplit; first done. iFrame.
    iApply subprot_refl.
  Qed.

  Global Instance recv_prot_contractive A n :
    Proper (pointwise_relation A (dist n) ==>
            pointwise_relation A (dist n) ==>
            pointwise_relation A (dist_later n) ==> dist n) recv_prot.
  Proof.
    intros v1 v2 Hveq Φ1 Φ2 HΦeq p1 p2 Hpeq. rewrite /recv_prot.
    split; [done|]=> /= v. do 6 f_equiv; [by rewrite Hveq|done|].
    apply is_chan_contractive. apply Hpeq.
  Qed.
  Global Instance recv_prot_ne A n :
    Proper (pointwise_relation A (dist n) ==>
            pointwise_relation A (dist n) ==>
            pointwise_relation A (dist n) ==> dist n) recv_prot.
  Proof.
    intros v1 v2 Hveq Φ1 Φ2 HΦeq p1 p2 Hpeq. rewrite /recv_prot.
    split; [done|]=> /= v. do 6 f_equiv; [by rewrite Hveq|done|].
    apply is_chan_ne. apply Hpeq.
  Qed.
  Global Instance recv_prot_proper A :
    Proper (pointwise_relation A () ==>
            pointwise_relation A () ==>
            pointwise_relation A () ==> ()) recv_prot.
  Proof.
    intros v1 v2 Hveq Φ1 Φ2 HΦeq p1 p2 Hpeq. rewrite /recv_prot.
    split; [done|]=> /= v. do 6 f_equiv; [by rewrite Hveq|done|].
    apply is_chan_proper. apply Hpeq.
  Qed.

  Global Instance send_prot_contractive A n :
    Proper (pointwise_relation A (dist n) ==>
            pointwise_relation A (dist n) ==>
            pointwise_relation A (dist_later n) ==> dist n) send_prot.
  Proof.
    intros v1 v2 Hveq Φ1 Φ2 HΦeq p1 p2 Hpeq. rewrite /send_prot.
    f_equiv. split; [done|]=> /= v. do 6 f_equiv; [by rewrite Hveq|done|].
    f_contractive. f_equiv. by apply Hpeq.
  Qed.
  Global Instance send_prot_ne A n :
    Proper (pointwise_relation A (dist n) ==>
            pointwise_relation A (dist n) ==>
            pointwise_relation A (dist n) ==> dist n) send_prot.
  Proof.
    intros v1 v2 Hveq Φ1 Φ2 HΦeq p1 p2 Hpeq. rewrite /send_prot.
    f_equiv. split; [done|]=> /= v. do 6 f_equiv; [by rewrite Hveq|done|].
    apply is_chan_ne. by f_equiv.
  Qed.
  Global Instance send_prot_proper A :
    Proper (pointwise_relation A () ==>
            pointwise_relation A () ==>
            pointwise_relation A () ==> ()) send_prot.
  Proof.
    intros v1 v2 Hveq Φ1 Φ2 HΦeq p1 p2 Hpeq. rewrite /send_prot.
    f_equiv. split; [done|]=> /= v. do 6 f_equiv; [by rewrite Hveq|done|].
    apply is_chan_proper. by f_equiv.
  Qed.

  Lemma wait_prot_dual : dual wait_prot  close_prot.                            (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ce5afaf5 *)
  Proof. split; [done|]. by intros v. Qed.
  Lemma close_prot_dual : dual close_prot  wait_prot.                           (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=155d3531 *)
  Proof. split; [done|]. by intros v. Qed.
  Lemma recv_prot_dual {A} (v : A  val) Φ p :                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2f9ccadf *)
    dual (recv_prot v Φ p)  send_prot v Φ (dualp).
  Proof.
    rewrite /send_prot. f_equiv. eapply recv_prot_proper; intro; try done.
    by rewrite /= dual_dual.
  Qed.
  Lemma send_prot_dual {A} (v : A  val) Φ p :                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1e22d9d6 *)
    dual (send_prot v Φ p)  recv_prot v Φ (dualp).
  Proof. split; [done|]. intro. done. Qed.
End session_proofs.

Section session_examples.
  Context `{!heapGS Σ, !chanG Σ}.
  Notation prot := (prot Σ).

  Definition prot_add_base p : prot :=
    send_prot  (lx : loc * Z), #lx.1)  lx, lx.1  #lx.2)%I
       lx, recv_prot  (_:unit), #())  _, lx.1  #(lx.2 + 2))%I
                        _, p)).

  Instance prot_add_base_contractive : Contractive prot_add_base.
  Proof.
    unfold prot_add_base.
    repeat intro. eapply send_prot_ne; try done.
    repeat intro. eapply recv_prot_contractive; try done.
    solve_proper.
  Qed.

  Definition prog_add : val :=                                                   (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ae1e1a4d *)
    λ: "<>",
      let: "c" := new #() in
      Fork (let: "r" := recv "c" in
            Fst "r" <- ((!(Fst "r") + #2));;
            let: "c" := send (Snd "r") #() in wait "c");;
      let: "l" := ref #40 in
      let: "c" := send "c" "l" in
      let: "r" := recv "c" in
      close (Snd "r");; assert: (!"l" = #42).

  Definition prot_add : prot := prot_add_base close_prot.                        (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b1ebf472 *)

  Lemma prog_add_spec : {{{ True }}} prog_add #() {{{ RET #(); True }}}.         (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ddde3a08 *)
  Proof.
    iIntros (Φ) "_ HΦ". wp_lam.
    wp_smart_apply (new_spec prot_add); [done|].
    iIntros (ch) "[Hch1 Hch2]".
    wp_smart_apply (wp_fork with "[Hch2]").
    - iIntros "!>". wp_smart_apply (recv_spec with "Hch2").
      iIntros ([l x] ch') "[Hch2 Hl]"=> /=. rewrite recv_prot_dual.
      wp_load. wp_store. wp_smart_apply (send_spec () with "[$Hch2 $Hl]").
      iIntros (ch'') "Hch2". by wp_smart_apply (wait_spec with "Hch2").
    - wp_alloc l as "Hl". wp_smart_apply (send_spec (l,40%Z) with "[$Hch1 $Hl]").
      iIntros (ch') "Hch1". wp_smart_apply (recv_spec with "Hch1").
      iIntros (_ ?) "[Hch1 Hl]". wp_smart_apply (close_spec with "Hch1").
      iIntros "_". wp_smart_apply wp_assert. wp_load. wp_pures.
      iModIntro. iSplit; [done|]. by iApply "HΦ".
  Qed.

  Definition prog_add_rec : val :=                                               (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f6381537 *)
    λ: "<>",
      let: "c" := new #() in
      Fork ((rec: "go" "c" :=
             let: "r" := recv "c" in
             Fst "r" <- ((!(Fst "r") + #2));;
             let: "c" := send (Snd "r") #() in "go" "c") "c");;
      let: "l" := ref #38 in
      let: "c" := send "c" "l" in
      let: "r" := recv "c" in
      let: "c" := send (Snd "r") "l" in
      let: "r" := recv "c" in
      assert: (!"l" = #42);; Snd "r".

  Definition prot_add_rec := fixpoint prot_add_base.                             (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=97e941d1 *)
  Lemma prot_add_rec_unfold : prot_add_rec  prot_add_base prot_add_rec.
  Proof. rewrite /prot_add_rec. apply fixpoint_unfold. Qed.

  Lemma prog_add_rec_spec :                                                      (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3205e768 *)
    {{{ True }}}
      prog_add_rec #()
    {{{ c, RET c; is_chan c prot_add_rec }}}.
  Proof.
    iIntros (Φ) "_ HΦ". wp_lam.
    wp_smart_apply (new_spec prot_add_rec); [done|].
    iIntros (ch) "[Hch1 Hch2]".
    wp_smart_apply (wp_fork with "[Hch2]").
    - iIntros "!>". wp_pure _.
      iLöb as "IH" forall (ch).
      rewrite {2}prot_add_rec_unfold.
      wp_smart_apply (recv_spec with "Hch2").
      iIntros ([l x] ch') "[Hch2 Hl]"=> /=. rewrite recv_prot_dual.
      wp_load. wp_store. wp_smart_apply (send_spec () with "[$Hch2 $Hl]").
      iIntros (ch'') "Hch2". do 2 wp_pure. by iApply "IH".
    - rewrite {2}prot_add_rec_unfold.
      wp_alloc l as "Hl". wp_smart_apply (send_spec (l,38%Z) with "[$Hch1 $Hl]").
      iIntros (ch') "Hch1". wp_smart_apply (recv_spec with "Hch1").
      iIntros (_ ch'') "[Hch1 Hl]"=> /=.
      replace #(38 + 2) with #40; last by do 2 f_equiv; lia.
      rewrite {2}prot_add_rec_unfold.
      wp_smart_apply (send_spec (l,40%Z) with "[$Hch1 $Hl]").
      iIntros (ch''') "Hch1". wp_smart_apply (recv_spec with "Hch1").
      iIntros (_ ?) "[Hch1 Hl]". wp_smart_apply wp_assert. wp_load. wp_pures.
      replace #(40 + 2) with #42; last by do 2 f_equiv; lia.
      iModIntro. iSplit; [done|].
      iIntros "!>". wp_pures. by iApply "HΦ".
  Qed.

End session_examples.