Guarantees by Construction (Mechanization)

Jules Jacobs

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
From iris.algebra Require Import excl.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang.lib Require Import assert.

Definition new1 : val := λ: <>, ref NONE.                                        (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=85bb86b3 *)
Definition recv1 : val :=                                                        (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7ea0b4e1 *)
  rec: "recv1" "l" :=
    match: !"l" with
      NONE => "recv1" "l"
    | SOME "v" => Free "l";; "v"
    end.
Definition send1 : val := λ: "l" "v",                                            (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7e49444e *)
    "l" <- SOME ("v").

Class chanG Σ := LockG { chan_tokG : inG Σ (exclR unitO) }.
Local Existing Instance chan_tokG.
Definition chanΣ : gFunctors := #[GFunctor (exclR unitO)].
Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
Proof. solve_inG. Qed.

Definition prot Σ : ofe := prodO boolO (val -d> iPropO Σ).                       (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=dd594332 *)

Section proof_base.
  Context `{!heapGS Σ, !chanG Σ}.
  Let N := nroot .@ "chan".
  Notation prot := (prot Σ).

  Definition tok (γ : gname) : iProp Σ := own γ (Excl ()).

  Definition chan_inv (γ1 γ2 : gname) (l : loc)                                  (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3a3f805f *)
                      (Φ : val → iProp Σ) : iProp Σ :=
    (l ↦ NONEV) ∨
    (∃ v, l ↦ SOMEV v ∗ tok γ1 ∗ Φ v) ∨
    (tok γ1 ∗ tok γ2).

  Definition is_chan0 (ch : val) (p : prot) : iProp Σ :=                         (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=13efbb1e *)
    ∃ γ1 γ2 (l : loc),
      ▷ ⌜ch = #l⌝ ∗ inv N (chan_inv γ1 γ2 l p.2) ∗ ▷ tok (if p.1 then γ1 else γ2).

  Definition dual (p : prot) : prot := (negb p.1, p.2).                          (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=11bdcaec *)

  Lemma pointsto_to_chan l p :
    l ↦ NONEV -∗ |={⊤}=> is_chan0 #l p ∗ is_chan0 #l (dual p).
  Proof.
    iIntros "Hl".
    iMod (own_alloc (Excl ())) as (γ1) "Hγ1"; first done.
    iMod (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
    iMod (inv_alloc N _ (chan_inv γ1 γ2 l p.2) with "[Hl]") as "#?"; [by iLeft|].
    destruct p as [[]?]; [iSplitL "Hγ1"|iSplitL "Hγ2"];
      iExists _, _; by eauto with iFrame.
  Qed.

  Lemma new1_spec0 p :                                                           (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9ad64e64 *)
    {{{ True }}} new1 #() {{{ ch, RET ch; is_chan0 ch p ∗ is_chan0 ch (dual p) }}}.
  Proof.
    iIntros (Ψ) "_ HΨ". wp_lam. wp_alloc l as "Hl".
    iMod (pointsto_to_chan with "Hl") as "[H1 H2]".
    iApply "HΨ". by eauto with iFrame.
  Qed.

  Lemma send1_spec0 ch P v :                                                     (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c9e07dff *)
    {{{ is_chan0 ch (true,P) ∗ ▷ P v }}} send1 ch v {{{ RET #(); True }}}.
  Proof.
    iIntros (φ) "[(%γ1 & %γ2 & %l & >-> & #Hinv & >Htok) HP] Hφ /=".
    wp_lam; wp_pures.
    iInv N as "[Hl|[(%w & Hl & >Htok' & HΦ')|>[Htok' Htok'']]]";
      [|iDestruct (own_valid_2 with "Htok Htok'") as %[]..].
    wp_store. iSplitR "Hφ"; last by iApply "Hφ".
    rewrite /chan_inv; eauto 10 with iFrame.
  Qed.

  Lemma recv1_spec0 ch P :                                                       (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=08836b00 *)
    {{{ is_chan0 ch (false,P) }}} recv1 ch {{{ v, RET v; P v }}}.
  Proof.
    iIntros (φ) "(%γ1 & %γ2 & %l & >-> & #Hinv & >Htok) Hφ /=".
    iLöb as "IH". wp_rec. wp_bind (Load _).
    iInv N as "[Hl|[(%w & Hl & Htok' & HΦ')|>[Htok' Htok'']]]".
    - wp_load. iModIntro. iSplitL "Hl"; [iNext; by iLeft|].
      wp_match. iApply ("IH" with "Htok Hφ").
    - wp_load. iModIntro. iSplitL "Htok Htok'".
      + rewrite /chan_inv. by eauto with iFrame.
      + wp_match. wp_free. wp_seq. iModIntro. by iApply "Hφ".
    - iDestruct (own_valid_2 with "Htok Htok''") as %[].
  Qed.

  Lemma dual_dual p : dual (dual p) = p.                                         (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8b0ded24 *)
  Proof. by destruct p as [[] ?]. Qed.
  Global Instance dual_ne : NonExpansive dual.
  Proof. solve_proper. Qed.
  Global Instance dual_proper : Proper ((≡) ==> (≡)) dual.
  Proof. solve_proper. Qed.

  Global Instance chan_inv_ne γ1 γ2 l n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (chan_inv γ1 γ2 l).
  Proof. solve_proper. Qed.
  Global Instance chan_inv_proper γ1 γ2 l :
    Proper (pointwise_relation _ (≡) ==> (≡)) (chan_inv γ1 γ2 l).
  Proof. solve_proper. Qed.

  Global Instance is_chan0_is_except_0 ch p : IsExcept0 (is_chan0 ch p).
  Proof.
    rewrite /IsExcept0 /is_chan0. repeat (setoid_rewrite bi.except_0_exist).
    do 6 f_equiv. rewrite !bi.except_0_sep !bi.except_0_later.
    by rewrite except_0_inv.
  Qed.
  Global Instance is_chan0_contractive ch : Contractive (is_chan0 ch).           (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9465a0c1 *)
  Proof.
    intros n [??] [??] Hpair; solve_proper_prepare.
    repeat first [f_contractive; destruct Hpair; simplify_eq/=| f_equiv].
  Qed.
  Global Instance is_chan0_ne ch : NonExpansive (is_chan0 ch).
  Proof. solve_proper. Qed.
  Global Instance is_chan0_proper ch : Proper ((≡) ==> (≡)) (is_chan0 ch).
  Proof. solve_proper. Qed.
End proof_base.

Global Typeclasses Opaque is_chan0.

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

  Definition prog_single : val :=                                                (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f17e4e44 *)
    λ: "<>",
      let: "c" := new1 #() in
      Fork (let: "l" := ref #42 in send1 "c" "l");;
      let: "l" := recv1 "c" in assert: (!"l" = #42).

  Definition prot_single : prot :=                                               (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=62e0c0bd *)
    (false, λ (v:val), ∃ (l:loc), ⌜v = #l⌝ ∗ l ↦ #42)%I.

  Lemma prog_add_spec : {{{ True }}} prog_single #() {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "_ HΦ". wp_lam.
    wp_smart_apply (new1_spec0 prot_single); [done|].
    iIntros (ch) "[Hch1 Hch2]".
    wp_smart_apply (wp_fork with "[Hch2]").
    - iIntros "!>". wp_alloc l as "Hl".
      wp_smart_apply (send1_spec0 with "[$Hch2 Hl]"); [|done].
      iIntros "!>". iExists _. by iFrame.
    - wp_smart_apply (recv1_spec0 with "Hch1").
      iIntros (v) "Hl". iDestruct "Hl" as (l ->) "Hl".
      wp_smart_apply wp_assert. wp_load. wp_pures.
      iModIntro. iSplit; [done|]. by iApply "HΦ".
  Qed.

End base_examples.