monad.v 8.95 KB
Newer Older
Léon Gondelman's avatar
Léon Gondelman committed
1
From iris.heap_lang Require Export proofmode notation.
Dan Frumin's avatar
Dan Frumin committed
2
From iris.heap_lang Require Import adequacy spin_lock assert par.
Léon Gondelman's avatar
Léon Gondelman committed
3
From iris.algebra Require Import frac.
Dan Frumin's avatar
Dan Frumin committed
4
From iris_c.lib Require Import mset flock locking_heap.
Léon Gondelman's avatar
Léon Gondelman committed
5 6 7 8 9 10 11 12 13 14 15

(* M A := ref (list loc) → Mutex → A *)

(* A → M A *)
Definition a_ret : val := λ: "a" <> <>, "a".

(* (A → M B) → M A → M B *)
Definition a_bind : val := λ: "f" "x" "env" "l",
  let: "a" := "x" "env" "l" in
  "f" "a" "env" "l".

Robbert Krebbers's avatar
Robbert Krebbers committed
16 17
Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).

Léon Gondelman's avatar
Léon Gondelman committed
18 19
(* M A → A *)
Definition a_run : val := λ: "x",
20
  let: "env" := mset_create #() in
Léon Gondelman's avatar
Léon Gondelman committed
21 22 23 24 25 26 27
  let: "l" := newlock #() in
  "x" "env" "l".

(* M A → M A *)
Definition a_atomic : val := λ: "x" "env" "l",
  acquire "l";;
  let: "k" := newlock #() in
28
  let: "a" := "x" #() "env" "k" in
Léon Gondelman's avatar
Léon Gondelman committed
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
  release "l";;
  "a".

(* (ref (list loc) → A) → M A *)
Definition a_atomic_env : val := λ: "f" "env" "l",
  acquire "l";;
  let: "a" := "f" "env" in
  release "l";;
  "a".

(* M A → M B → M (A * B) *)
Definition a_par : val := λ: "x" "y" "env" "l",
  "x" "env" "l" ||| "y" "env" "l".

Definition amonadN := nroot .@ "amonad".

45 46 47 48 49 50 51
Class amonadG (Σ : gFunctors) := AMonadG {
  aheapG :> heapG Σ;
  aflockG :> flockG Σ;
  alocking_heapG :> locking_heapG Σ;
  aspawnG :> spawnG Σ
}.

Léon Gondelman's avatar
Léon Gondelman committed
52
Section a_wp.
53
  Context `{amonadG Σ}.
Léon Gondelman's avatar
Léon Gondelman committed
54

Dan Frumin's avatar
Dan Frumin committed
55 56
  (* X ⊆ σ^{-1}(L) *)
  Definition correct_locks (X : gset val) (preσ : gset loc) : Prop :=
57
    set_Forall (λ v,  l : loc, v = #l  l  preσ) X.
Dan Frumin's avatar
Dan Frumin committed
58 59 60 61 62 63 64

  Definition env_inv (env : val) : iProp Σ :=
    ( (X : gset val) (σ : gmap loc level),
         is_set_mut env X
        full_locking_heap σ
        ([ map] l  _  σ,  v', l {1/2} v')
        correct_locks X (locked_locs σ))%I.
65

Léon Gondelman's avatar
Léon Gondelman committed
66 67
  Definition awp (e : expr)
      (R : iProp Σ) (Φ : val  iProp Σ) : iProp Σ :=
68 69 70
    tc_opaque (WP e {{ ev,  (γ : flock_name) (π : frac) (env : val) (l : val) s,
      is_flock amonadN γ l -
      flock_res γ s (env_inv env  R) -
71
      unflocked γ π -
72
      WP ev env l {{ v, Φ v  unflocked γ π }}
Robbert Krebbers's avatar
Robbert Krebbers committed
73
    }})%I.
Dan Frumin's avatar
Dan Frumin committed
74 75 76 77 78 79 80 81 82 83 84 85

  Global Instance elim_bupd_awp p e Φ :
   ElimModal True p false (|==> P) P
     (awp e R Φ) (awp e R Φ).
  Proof.
    iIntros (P R _) "[HP HA]".
    rewrite /awp /tc_opaque.
    destruct p; simpl;
      [ iDestruct "HP" as "#HP" | ];
      iMod "HP"; by iApply "HA".
  Qed.

86 87 88
End a_wp.

Section a_wp_rules.
89
  Context `{amonadG Σ}.
Léon Gondelman's avatar
Léon Gondelman committed
90

Robbert Krebbers's avatar
Robbert Krebbers committed
91 92
  Lemma a_wp_awp R Φ Ψ e : awp e R Φ - ( v : val, awp v R Φ - Ψ v) - WP e {{ Ψ }}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    iIntros "Hwp H". rewrite /awp /=. iApply (wp_wand with "Hwp").
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96 97 98 99 100
    iIntros (v) "Hwp". iApply "H". by iApply wp_value'.
  Qed.

  Lemma wp_awp_bind R Φ K e :
    WP e {{ v, awp (fill K (of_val v)) R Φ }}  awp (fill K e) R Φ.
  Proof. by apply: wp_bind. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
101 102 103 104 105 106 107 108 109 110 111 112
  Lemma wp_awp_bind_inv R Φ K e :
    awp (fill K e) R Φ  WP e {{ v, awp (fill K (of_val v)) R Φ }}.
  Proof. by apply: wp_bind_inv. Qed.

  Lemma awp_wand e (Φ Ψ : val  iProp Σ) R :
    awp e R Φ -
    ( v, Φ v - Ψ v) -
    awp e R Ψ.
  Proof.
    iIntros "HAWP Hv". rewrite /awp /=.
    iApply (wp_wand with "HAWP").
    iIntros (v) "HΦ".
113
    iIntros (γ π env l s) "#Hflock #Hres Hunfl".
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116 117 118 119 120 121 122 123 124 125 126 127
    iApply (wp_wand with "[HΦ Hunfl]"); first by iApply "HΦ".
    iIntros (w) "[HΦ $]". by iApply "Hv".
  Qed.

  Lemma awp_pure K φ e1 e2 R Φ :
    PureExec φ e1 e2 
    φ 
     awp (fill K e2) R Φ -
    awp (fill K e1) R Φ.
  Proof.
    iIntros (? Hφ) "Hawp". iApply wp_awp_bind. wp_pure _.
    by iApply wp_awp_bind_inv.
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
128 129 130
  Lemma awp_ret e R Φ :
    WP e {{ Φ }} - awp (a_ret e) R Φ.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
    iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp").
132
    iIntros (v) "HΦ". wp_lam.
133
    iIntros (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
134 135
  Qed.

Robbert Krebbers's avatar
Nits.  
Robbert Krebbers committed
136 137 138
  Lemma awp_bind (f e : expr) R Φ :
    AsVal f 
    awp e R (λ ev, awp (f ev) R Φ) -
139
    awp (a_bind f e) R Φ.
Léon Gondelman's avatar
Léon Gondelman committed
140
  Proof.
Robbert Krebbers's avatar
Nits.  
Robbert Krebbers committed
141
    iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
142
    iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
143
    iIntros (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam. wp_bind (ev env l).
144
    iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
145 146
    iIntros (w) "[Hwp Hunfl]". wp_let. wp_apply (wp_wand with "Hwp").
    iIntros (v) "H". by iApply ("H" with "[$]").
Léon Gondelman's avatar
Léon Gondelman committed
147 148
  Qed.

149
  Lemma awp_atomic (e : expr) (ev : val) R Φ :
150
    IntoVal e ev 
151
    (R -  R', R'  awp (ev #()) R' (λ w, R' - R  Φ w)) -
152
    awp (a_atomic e) R Φ.
Léon Gondelman's avatar
Léon Gondelman committed
153
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
    iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
155
    iIntros (γ π env l s) "#Hlock1 #Hres Hunfl1". do 2 wp_let.
Léon Gondelman's avatar
Léon Gondelman committed
156
    wp_apply (acquire_cancel_spec with "[$]").
157 158 159
    iIntros (f) "([Henv HR] & Hcl)". wp_seq.
    iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]".    
    wp_apply (newlock_cancel_spec amonadN); first done.
160
    iIntros (k γ') "[#Hlock2 Hunfl2]". wp_let.
161 162
    iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env  R')%I
            with "Hlock2 Hunfl2 [$Henv $HR']") as (s') "[#Hres2 Hunfl2]".
163
    wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
164
    iApply (wp_wand with "[Hwp Hunfl2]"); first by iApply "Hwp".
165 166 167
    iIntros (w) "[HR Hunfl2]".
    iMod (cancel_lock with "Hlock2 Hres2 Hunfl2") as "[Henv HR']".
    wp_let.
Léon Gondelman's avatar
Léon Gondelman committed
168
    iDestruct ("HR" with "HR'") as "[HR HΦ]".
169 170
    wp_apply (release_cancel_spec with "[$Hlock1 Hcl Henv HR]").
    { iApply "Hcl". by iNext; iFrame. }
171
    iIntros "Hunfl1". wp_seq. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
172 173
  Qed.

174
  Lemma awp_atomic_env (e : expr) (ev : val) R Φ :
175
    IntoVal e ev 
Léon Gondelman's avatar
Léon Gondelman committed
176
    ( env, env_inv env - R -
177
      WP ev env {{ w, env_inv env  R  Φ w }}) -
178
    awp (a_atomic_env e) R Φ.
Léon Gondelman's avatar
Léon Gondelman committed
179
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
    iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
181
    iIntros (γ π env l s) "#Hlock #Hres Hunfl". do 2 wp_lam.
Léon Gondelman's avatar
Léon Gondelman committed
182
    wp_apply (acquire_cancel_spec with "[$]").
183
    iIntros (f) "([Henv HR] & Hcl)". wp_seq.
Léon Gondelman's avatar
Léon Gondelman committed
184 185 186
    iDestruct ("Hwp" with "Henv HR") as "Hwp".
    wp_apply (wp_wand with "Hwp").
    iIntros (w) "[Henv [HR HΦ]]". wp_let.
187 188
    wp_apply (release_cancel_spec with "[$Hlock Hcl Henv HR]").
    { iApply "Hcl". by iNext; iFrame. }
189
    iIntros "Hunfl". wp_seq. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
190 191
  Qed.

192
  Lemma awp_par (Ψ1 Ψ2 : val  iProp Σ) e1 e2 (ev1 ev2 : val) R (Φ : val  iProp Σ) :
193 194 195 196
    IntoVal e1 ev1 
    IntoVal e2 ev2 
    awp ev1 R Ψ1 -
    awp ev2 R Ψ2 -
Léon Gondelman's avatar
Léon Gondelman committed
197
     ( w1 w2, Ψ1 w1 - Ψ2 w2 -  Φ (w1,w2)%V) -
198
    awp (a_par e1 e2) R Φ.
Léon Gondelman's avatar
Léon Gondelman committed
199
  Proof.
200
    iIntros (<-%of_to_val <-%of_to_val) "Hwp1 Hwp2 HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
201
    rewrite /awp /a_par /=. do 2 wp_lam.
202
    iIntros (γ π env l s) "#Hlock #Hres [Hunfl1 Hunfl2]". do 2 wp_lam.
203 204 205
    iApply (par_spec (λ v, Ψ1 v  unflocked _ (π/2))%I
                     (λ v, Ψ2 v  unflocked _ (π/2))%I
      with "[Hwp1 Hunfl1] [Hwp2 Hunfl2]").
206 207 208 209
    - wp_lam. wp_apply (wp_wand with "Hwp1").
      iIntros (v) "Hwp1". by iApply "Hwp1".
    - wp_lam. wp_apply (wp_wand with "Hwp2").
      iIntros (v) "Hwp2". by iApply "Hwp2".
Léon Gondelman's avatar
Léon Gondelman committed
210 211 212
    - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
      iApply ("HΦ" with "[$] [$]").
  Qed.
213
End a_wp_rules.
Dan Frumin's avatar
Dan Frumin committed
214 215 216 217

Section a_wp_run.
  Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.

218 219
  Lemma awp_run (e : expr) R Φ :
    AsVal e 
220
    R - ( `{amonadG Σ}, awp e R (λ w,  R ={}= Φ w)) -
221
    WP a_run e {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
222
  Proof.
223
    iIntros ([ev <-%of_to_val]) "HR Hwp". rewrite /awp /a_run /=. wp_let.
Dan Frumin's avatar
Dan Frumin committed
224 225 226
    wp_bind (mset_create #()). iApply mset_create_spec; first done.
    iNext. iIntros (env) "Henv". wp_let.
    iMod (locking_heap_init ) as (?) "Hσ".
227
    pose (amg := AMonadG Σ _ _ _ _).
228
    wp_apply (newlock_cancel_spec amonadN); first done.
Dan Frumin's avatar
Dan Frumin committed
229
    iIntros (k γ') "[#Hlock Hunfl]". wp_let. rewrite- wp_fupd.
230 231 232
    iMod (flock_res_alloc_unflocked _ _ _ _ (env_inv env  R)%I
            with "Hlock Hunfl [Henv Hσ $HR]") as (s) "[#Hres Hunfl]".
    { iNext. iExists , . iFrame. eauto. } 
233
    iSpecialize ("Hwp" $! amg).
234 235
    wp_apply (wp_wand with "Hwp"). iIntros (v') "Hwp".
    iApply (wp_wand with "[Hwp Hunfl]"); first by iApply "Hwp".
236
    iIntros (w) "[HΦ Hunfl]".
237
    iMod (cancel_lock with "Hlock Hres Hunfl") as "[HEnv HR]". by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
238 239 240
  Qed.
End a_wp_run.

Dan Frumin's avatar
Dan Frumin committed
241 242 243
(* Make sure that we only use the provided rules and don't break the abstraction *)
Opaque a_ret a_bind (* a_run *) a_atomic a_atomic_env a_par.

Dan Frumin's avatar
Dan Frumin committed
244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
(* Definition locking_heapΣ : gFunctors := *)
(*   #[heapΣ; GFunctor (auth.authR locking_heapUR)]. *)

(* Instance subG_locking_heapG {Σ} : subG locking_heapΣ Σ → locking_heapPreG Σ. *)
(* Proof. solve_inG. Qed. *)

(* Definition awp_adequacy Σ R s v σ φ : *)
(*   (R -∗ (∀ `{locking_heapG Σ}, awp (of_val v) R (λ w, R -∗ ⌜φ w⌝)))%I → *)
(*   adequate MaybeStuck (a_run v) σ φ. *)
(*   (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) → *)
(* Proof. *)
(*   intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "". *)
(*   iMod (gen_heap_init σ) as (?) "Hh". *)
(*   iModIntro. iExists gen_heap_ctx. iFrame "Hh". *)
(*   iApply (Hwp (HeapG _ _ _)). *)
(* Qed. *)