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

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

(* A → M A *)
10
Definition c_ret : val := λ: "a" <> <>, "a".
Léon Gondelman's avatar
Léon Gondelman committed
11 12

(* (A → M B) → M A → M B *)
13
Definition c_bind : val := λ: "x" "f" "env" "l",
Léon Gondelman's avatar
Léon Gondelman committed
14 15 16
  let: "a" := "x" "env" "l" in
  "f" "a" "env" "l".

Robbert Krebbers's avatar
Robbert Krebbers committed
17
Notation "x ←ᶜ y ;;ᶜ z" :=
18
  (c_bind y (λ: x, z))%E
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  (at level 100, y at next level, z at level 200, right associativity) : expr_scope.
20
Notation "y ;;ᶜ z" := (c_bind y (λ: <>, z))%E
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  (at level 100, z at level 200, right associativity) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

Léon Gondelman's avatar
Léon Gondelman committed
23
(* M A → A *)
24
Definition c_run : val := λ: "x",
25
  let: "env" := mset_create #() in
Léon Gondelman's avatar
Léon Gondelman committed
26
  let: "l" := newlock #() in
Dan Frumin's avatar
Dan Frumin committed
27
  "x" "env" "l".
Léon Gondelman's avatar
Léon Gondelman committed
28 29

(* M A → M A *)
30
Definition c_atomic : val := λ: "x" "env" "l",
Léon Gondelman's avatar
Léon Gondelman committed
31 32
  acquire "l";;
  let: "k" := newlock #() in
33
  let: "a" := "x" #() "env" "k" in
Léon Gondelman's avatar
Léon Gondelman committed
34 35 36 37
  release "l";;
  "a".

(* (ref (list loc) → A) → M A *)
38
Definition c_atomic_env : val := λ: "f" "env" "l",
Léon Gondelman's avatar
Léon Gondelman committed
39 40 41 42 43 44
  acquire "l";;
  let: "a" := "f" "env" in
  release "l";;
  "a".

(* M A → M B → M (A * B) *)
45
Definition c_par : val := λ: "x" "y" "env" "l",
Léon Gondelman's avatar
Léon Gondelman committed
46
  "x" "env" "l" ||| "y" "env" "l".
47
Notation "e1 |||ᶜ e2" := (c_par e1 e2)%E (at level 50) : expr_scope.
Léon Gondelman's avatar
Léon Gondelman committed
48

49
Definition cmonadN := nroot .@ "amonad".
Léon Gondelman's avatar
Léon Gondelman committed
50

51
Class cmonadG (Σ : gFunctors) := AMonadG {
52 53 54 55 56 57
  aheapG :> heapG Σ;
  aflockG :> flockG Σ;
  alocking_heapG :> locking_heapG Σ;
  aspawnG :> spawnG Σ
}.

58 59
Section cwp.
  Context `{cmonadG Σ}.
Léon Gondelman's avatar
Léon Gondelman committed
60

Dan Frumin's avatar
Dan Frumin committed
61
  Definition env_inv (env : val) : iProp Σ :=
62
    ( (X : gset val) (σ : gmap cloc (lvl * val)),
Robbert Krebbers's avatar
Robbert Krebbers committed
63
        v, v  X   cl, cloc_of_val (SOMEV v) = Some cl  cl  locked_locs σ  
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65
      is_mset env X 
      full_locking_heap σ)%I.
66

Dan Frumin's avatar
Dan Frumin committed
67 68 69
  Definition flock_resources (γ : flock_name)
             (I : gmap lock_res_gname (frac*iProp Σ)) :=
    ([ map] ρ  πR  I, flock_res cmonadN γ ρ πR.1 πR.2)%I.
Dan Frumin's avatar
Dan Frumin committed
70

71
  (** DF: The outer `WP` here is needed to be able to perform some reductions inside a heap_lang context.
72
      Without this, the `cwp_cwp` rule is not provable.
Dan Frumin's avatar
Dan Frumin committed
73 74 75 76 77

      My intuitive explanation: we want to preform some reductions to `e` until it is actually a value that is a monadic computation.
      In some sense it is a form of CPSing on a logical level.
      But I still cannot precisely state why is it needed.
 *)
78
  Definition cwp_def (e : expr)
Léon Gondelman's avatar
Léon Gondelman committed
79
      (R : iProp Σ) (Φ : val  iProp Σ) : iProp Σ :=
80
    WP e {{ ev,
Dan Frumin's avatar
Dan Frumin committed
81
       (γ : flock_name) (env : val) (l : val) I,
82
        is_flock cmonadN γ l -
Robbert Krebbers's avatar
Robbert Krebbers committed
83
        flock_resources γ I -
Dan Frumin's avatar
Dan Frumin committed
84
        ([ map] πR  I, πR.2)  (env_inv env  R) -
Robbert Krebbers's avatar
Robbert Krebbers committed
85
        WP ev env l {{ v, Φ v  flock_resources γ I }}
86
    }}%I.
87 88 89 90
  Definition cwp_aux : seal (@cwp_def). by eexists. Qed.
  Definition cwp := unseal cwp_aux.
  Definition cwp_eq : @cwp = @cwp_def := seal_eq cwp_aux.
End cwp.
91

92
Notation "'CWP' e @ R {{ Φ } }" := (cwp e%E R%I Φ)
93
  (at level 20, e, Φ at level 200, only parsing) : bi_scope.
94
Notation "'CWP' e {{ Φ } }" := (cwp e%E True%I Φ)
95 96
  (at level 20, e, Φ at level 200, only parsing) : bi_scope.

97
Notation "'CWP' e @ R {{ v , Q } }" := (cwp e%E R%I (λ v, Q))
98
  (at level 20, e, Q at level 200,
99 100
   format "'[' 'CWP'  e  '/' '[          ' @  R  {{  v ,  Q  } } ']' ']'") : bi_scope.
Notation "'CWP' e {{ v , Q } }" := (cwp e%E True%I (λ v, Q))
101
  (at level 20, e, Q at level 200,
102
   format "'[' 'CWP'  e  '/' '[   ' {{  v ,  Q  } } ']' ']'") : bi_scope.
103

104 105
Section cwp_rules.
  Context `{cmonadG Σ}.
Léon Gondelman's avatar
Léon Gondelman committed
106

107 108 109
  Lemma cwp_wp R Φ Ψ e :
    CWP e @ R {{ Φ }} -
    ( v : val, CWP v @ R {{ Φ }} - Ψ v) -
110
    WP e {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  Proof.
112
    iIntros "Hwp H". rewrite cwp_eq /=. iApply (wp_wand with "Hwp").
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115
    iIntros (v) "Hwp". iApply "H". by iApply wp_value'.
  Qed.

116 117 118 119
  Lemma wp_cwp_bind R Φ K e :
    WP e {{ v, CWP (fill K (of_val v)) @ R {{ Φ }} }} -
    CWP fill K e @ R {{ Φ }}.
  Proof. rewrite cwp_eq. by apply: wp_bind. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
120

121 122 123 124
  Lemma wp_cwp_bind_inv R Φ K e :
    CWP fill K e @ R {{ Φ }} -
    WP e {{ v, CWP fill K (of_val v) @ R {{ Φ }} }}.
  Proof. rewrite cwp_eq. by apply: wp_bind_inv. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
125

126
  Lemma cwp_insert_res e Φ R1 R2 :
Dan Frumin's avatar
Dan Frumin committed
127
     R1 -
128 129
    CWP e @ (R1  R2) {{ v,  R1 ={}= Φ v }} -
    CWP e @ R2 {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
130
  Proof.
131 132
    iIntros "HR1 Hcwp". rewrite cwp_eq.
    iApply (wp_wand with "Hcwp").
Dan Frumin's avatar
Dan Frumin committed
133
    iIntros (v) "HΦ".
Dan Frumin's avatar
Dan Frumin committed
134
    iIntros (γ env l I) "#Hflock Hres #Heq".
Dan Frumin's avatar
Dan Frumin committed
135 136 137
    iMod (flock_res_alloc_strong _ (dom (gset lock_res_gname) I) with "Hflock HR1") as (ρ) "[% Hres']"; first done.
    pose (I' := <[ρ:=(1%Qp,R1)]>I).
    assert (I !! ρ = None) by by eapply not_elem_of_dom.
Dan Frumin's avatar
Dan Frumin committed
138 139
    iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []").
    { rewrite /flock_resources /I'.
Dan Frumin's avatar
Dan Frumin committed
140 141
      rewrite big_sepM_insert //. iFrame. }
    { rewrite big_sepM_insert // /=. iRewrite "Heq".
Dan Frumin's avatar
Dan Frumin committed
142 143 144 145 146 147 148
      rewrite (assoc _ R1 _ R2).
      rewrite (comm _ R1 (env_inv env)).
      rewrite -(assoc _ _ R1 R2). done. }
    iApply wp_fupd.
    iApply (wp_wand with "HΦ").
    iIntros (w) "[HΦ HI]". rewrite /flock_resources /I'.
    rewrite big_sepM_insert /=; last done. iDestruct "HI" as "[HR1 $]".
Dan Frumin's avatar
Dan Frumin committed
149 150
    iMod (flock_res_dealloc with "Hflock HR1") as "HR"; try done.
    by iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
151 152
  Qed.

153 154
  Lemma cwp_fupd_wand e Φ Ψ R :
    CWP e @ R {{ Φ }} -
155
    ( v, Φ v ={}= Ψ v) -
156
    CWP e @ R {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  Proof.
158
    iIntros "Hwp H". rewrite cwp_eq.
159 160
    iApply (wp_wand with "Hwp"); iIntros (v) "HΦ".
    iIntros (γ env l I) "#Hflock Hres #Heq". iApply wp_fupd.
Dan Frumin's avatar
Dan Frumin committed
161
    iApply (wp_wand with "[HΦ Hres]"). iApply ("HΦ" with "Hflock Hres Heq").
162 163 164
    iIntros (w) "[HΦ $]". by iApply "H".
  Qed.

165 166 167
  Lemma cwp_fupd e Φ R :
    CWP e @ R {{ v, |={}=> Φ v }} - CWP e @ R {{ Φ }}.
  Proof. iIntros "Hwp". iApply (cwp_fupd_wand with "Hwp"); auto. Qed.
168

169 170 171
  Lemma fupd_cwp e Φ R :
    (|={}=> CWP e @ R {{ v, Φ v }}) - CWP e @ R {{ Φ }}.
  Proof. rewrite cwp_eq. by iIntros ">Hwp". Qed.
172

173 174
  Lemma cwp_wand e Φ Ψ R :
    CWP e @ R {{ Φ }} -
175
    ( v, Φ v - Ψ v) -
176
    CWP e @ R {{ Ψ }}.
177
  Proof.
178
    iIntros "Hwp H". iApply (cwp_fupd_wand with "Hwp"); iIntros (v) "HΦ !>".
179
    by iApply "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181
  Qed.

182
  Lemma cwp_pure K φ n e1 e2 R Φ :
Dan Frumin's avatar
Dan Frumin committed
183
    PureExec φ n e1 e2 
Robbert Krebbers's avatar
Robbert Krebbers committed
184
    φ 
185 186
    ^n CWP (fill K e2) @ R {{ Φ }} -
    CWP (fill K e1) @ R {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
187
  Proof.
188 189
    iIntros (? Hφ) "Hcwp". iApply wp_cwp_bind. wp_pure _.
    by iApply wp_cwp_bind_inv.
Robbert Krebbers's avatar
Robbert Krebbers committed
190 191
  Qed.

192 193
  Lemma cwp_ret e R Φ :
    WP e {{ Φ }} - CWP c_ret e @ R {{ Φ }}.
Léon Gondelman's avatar
Léon Gondelman committed
194
  Proof.
195
    iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_apply (wp_wand with "Hwp").
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197
    iIntros (v) "HΦ". wp_lam. wp_pures.
    iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
198 199
  Qed.

200 201 202
  Lemma cwp_bind (f : val) (e : expr) R Φ :
    CWP e @ R {{ ev, CWP f ev @ R {{ Φ }} }} -
    CWP c_bind e f @ R {{ Φ }}.
Léon Gondelman's avatar
Léon Gondelman committed
203
  Proof.
204
    iIntros "Hwp". rewrite cwp_eq /cwp_def.
Dan Frumin's avatar
Dan Frumin committed
205
    wp_apply (wp_wand with "Hwp"). iIntros (ev) "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207
    wp_lam. wp_pures.
    iIntros (γ env l I) "#Hflock Hres #Heq". wp_pures. wp_bind (ev env l).
Dan Frumin's avatar
Dan Frumin committed
208
    iApply (wp_wand with "[Hwp Hres]"). iApply ("Hwp" with "Hflock Hres Heq").
Dan Frumin's avatar
Dan Frumin committed
209
    iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
Dan Frumin's avatar
Dan Frumin committed
210
    iIntros (v) "H". iApply ("H" with "Hflock Hres Heq").
Léon Gondelman's avatar
Léon Gondelman committed
211 212
  Qed.

213 214 215
  Lemma cwp_atomic (ev : val) R Φ :
    (R -   R', R'  CWP ev #() @ R' {{ w, R' - R  Φ w }}) -
    CWP c_atomic ev @ R {{ Φ }}.
Léon Gondelman's avatar
Léon Gondelman committed
216
  Proof.
217
    iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_lam. wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
    iIntros (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
Dan Frumin's avatar
Dan Frumin committed
219 220 221 222
    wp_apply (acquire_flock_spec with "[$]").
    iIntros "Hfl".
    iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
    iRewrite "Heq1" in "HI".
Dan Frumin's avatar
Dan Frumin committed
223
    iDestruct "HI" as "[Henv HR]".
Dan Frumin's avatar
Dan Frumin committed
224
    wp_pures; simpl.
Dan Frumin's avatar
Dan Frumin committed
225
    iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
226
    wp_apply (newflock_spec cmonadN); first done.
Dan Frumin's avatar
Dan Frumin committed
227
    iIntros (k γ') "#Hlock2".
Dan Frumin's avatar
Dan Frumin committed
228
    iMod (flock_res_alloc_strong _  _ _ (env_inv env  Q)%I with "Hlock2 [$HQ $Henv]") as (ρ) "[_ Hres]"; first done.
229
    wp_let.
230
    wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
Dan Frumin's avatar
Dan Frumin committed
231
    iApply (wp_wand with "[Hwp Hres]").
Dan Frumin's avatar
Dan Frumin committed
232
    - iApply ("Hwp" $! _ _ _ {[ρ:=(1%Qp,_)]}  with "Hlock2 [Hres] []").
Dan Frumin's avatar
Dan Frumin committed
233 234 235 236
      + rewrite /flock_resources big_sepM_singleton //.
      + rewrite big_sepM_singleton //.
    - iIntros (w) "[HR Hres]".
      rewrite /flock_resources big_sepM_singleton /=.
Dan Frumin's avatar
Dan Frumin committed
237
      iMod (flock_res_dealloc with "Hlock2 Hres") as "[Henv HQ]"; try done.
Dan Frumin's avatar
Dan Frumin committed
238 239
      wp_let.
      iDestruct ("HR" with "HQ") as "[HR HΦ]".
Dan Frumin's avatar
Dan Frumin committed
240
      iMod ("Hcl" with "[HR Henv]") as "Hflocked".
Dan Frumin's avatar
Dan Frumin committed
241
      { iNext. iRewrite "Heq1". iFrame. }
Dan Frumin's avatar
Dan Frumin committed
242
      wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
Dan Frumin's avatar
Dan Frumin committed
243
      iIntros "$". wp_pures. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
244 245
  Qed.

246
  Lemma cwp_atomic_env (ev : val) R Φ :
Léon Gondelman's avatar
Léon Gondelman committed
247
    ( env, env_inv env - R -
Robbert Krebbers's avatar
Robbert Krebbers committed
248
      WP ev env {{ w,  (env_inv env  R  Φ w) }}) -
249
    CWP c_atomic_env ev @ R {{ Φ }}.
Léon Gondelman's avatar
Léon Gondelman committed
250
  Proof.
251
    iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_lam. wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
    iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
Dan Frumin's avatar
Dan Frumin committed
253 254 255 256
    wp_apply (acquire_flock_spec with "[$]").
    iIntros "Hfl".
    iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
    iRewrite "Heq" in "HI".
Dan Frumin's avatar
Dan Frumin committed
257
    iDestruct "HI" as "[Henv HR]".
Dan Frumin's avatar
Dan Frumin committed
258 259
    wp_pures; simpl.
    iSpecialize ("Hwp" with "Henv HR").
Robbert Krebbers's avatar
Robbert Krebbers committed
260 261
    wp_apply (wp_wand with "Hwp").
    iIntros (w) "[Henv [HR HΦ]]". wp_pures.
Dan Frumin's avatar
Dan Frumin committed
262
    iRewrite "Heq" in "Hcl".
Dan Frumin's avatar
Dan Frumin committed
263
    iMod ("Hcl" with "[$HR $Henv]") as "Hflocked".
Dan Frumin's avatar
Dan Frumin committed
264
    wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
Dan Frumin's avatar
Dan Frumin committed
265
    iIntros "$". wp_pures. iFrame.
Léon Gondelman's avatar
Léon Gondelman committed
266 267
  Qed.

268 269 270
  Lemma cwp_par Ψ1 Ψ2 e1 e2 R Φ :
    CWP e1 @ R {{ Ψ1 }} -
    CWP e2 @ R {{ Ψ2 }} -
Léon Gondelman's avatar
Léon Gondelman committed
271
     ( w1 w2, Ψ1 w1 - Ψ2 w2 -  Φ (w1,w2)%V) -
272
    CWP e1 ||| e2 @ R {{ Φ }}.
Léon Gondelman's avatar
Léon Gondelman committed
273
  Proof.
274
    iIntros "Hwp1 Hwp2 HΦ". rewrite cwp_eq /cwp_def.
Dan Frumin's avatar
Dan Frumin committed
275 276 277
    wp_apply (wp_wand with "Hwp2").
    iIntros (ev2) "Hwp2".
    wp_apply (wp_wand with "Hwp1").
Robbert Krebbers's avatar
Robbert Krebbers committed
278 279
    iIntros (ev1) "Hwp1". wp_lam. wp_pures.
    iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
Dan Frumin's avatar
Dan Frumin committed
280
    pose (I' := fmap (λ πR, ((πR.1/2)%Qp,πR.2)) I).
Dan Frumin's avatar
Dan Frumin committed
281 282 283 284 285 286 287
    iAssert (flock_resources γ I'  flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
    { rewrite /flock_resources -big_sepM_sepM.
      rewrite /I' big_sepM_fmap /=.
      iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl.
      by rewrite -flock_res_op Qp_div_2. }
    iApply (par_spec (λ v, Ψ1 v  flock_resources γ I')%I
                     (λ v, Ψ2 v  flock_resources γ I')%I
Dan Frumin's avatar
Dan Frumin committed
288 289
      with "[Hwp1 Hres1] [Hwp2 Hres2]").
    - wp_lam. iApply ("Hwp1" with "Hlock Hres1").
Dan Frumin's avatar
Dan Frumin committed
290
      by rewrite /I' big_sepM_fmap /=.
Dan Frumin's avatar
Dan Frumin committed
291
    - wp_lam. iApply ("Hwp2" with "Hlock Hres2").
Dan Frumin's avatar
Dan Frumin committed
292 293 294 295 296 297 298 299
      by rewrite /I' big_sepM_fmap /=.
    - iNext. iIntros (w1 w2) "[[HΨ1 Hres1] [HΨ2 Hres2]]".
      iAssert (flock_resources γ I)%I with "[Hres1 Hres2]" as "$".
      { iCombine "Hres1 Hres2" as "Hres".
        rewrite /flock_resources -big_sepM_sepM.
        rewrite /I' big_sepM_fmap /=.
        iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl.
          by rewrite -flock_res_op Qp_div_2. }
Léon Gondelman's avatar
Léon Gondelman committed
300 301
      iApply ("HΦ" with "[$] [$]").
  Qed.
302

303
  Global Instance frame_cwp p R' e R Φ Ψ :
304
    ( v, Frame p R (Φ v) (Ψ v)) 
305
    Frame p R (CWP e @ R' {{ Φ }}) (CWP e @ R' {{ Ψ }}).
306
  Proof.
307
    rewrite /Frame. iIntros (HR) "[HR H]". iApply (cwp_wand with "H").
308 309 310
    iIntros (v) "H". iApply HR; iFrame.
  Qed.

311 312
  Global Instance is_except_0_cwp R e Φ : IsExcept0 (CWP e @ R {{ Φ }}).
  Proof. rewrite /IsExcept0. iIntros "H". iApply fupd_cwp. by iMod "H". Qed.
313

314 315
  Global Instance elim_modal_bupd_cwp p R e P Φ :
    ElimModal True p false (|==> P) P (CWP e @ R {{ Φ }}) (CWP e @ R {{ Φ }}).
316 317
  Proof.
    rewrite /ElimModal bi.intuitionistically_if_elim; iIntros (_) "[HP HR]".
318
    iApply fupd_cwp. iMod "HP". by iApply "HR".
319 320 321
  Qed.

  Global Instance elim_modal_fupd_wp p R e P Φ :
322
    ElimModal True p false (|={}=> P) P (CWP e @ R {{ Φ }}) (CWP e @ R {{ Φ }}).
323 324
  Proof.
    rewrite /ElimModal bi.intuitionistically_if_elim; iIntros (_) "[HP HR]".
325
    iApply fupd_cwp. iMod "HP". by iApply "HR".
326 327 328
  Qed.

  Global Instance add_modal_fupd_wp R e P Φ :
329
    AddModal (|={}=> P) P (CWP e @ R {{ Φ }}).
330
  Proof. rewrite /AddModal. iIntros "[>HP H]". by iApply "H". Qed.
331
End cwp_rules.
Dan Frumin's avatar
Dan Frumin committed
332

333
Section cwp_run.
Dan Frumin's avatar
Dan Frumin committed
334 335
  Context `{heapG Σ, flockG Σ, spawnG Σ, locking_heapPreG Σ}.

336 337 338
  Lemma cwp_run (ev : val) Φ :
    ( `{cmonadG Σ}, CWP ev {{ w, Φ w }}) -
    WP c_run ev {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
339
  Proof.
340
    iIntros "Hwp". wp_lam.
Dan Frumin's avatar
Dan Frumin committed
341 342
    wp_bind (mset_create #()). iApply mset_create_spec; first done.
    iNext. iIntros (env) "Henv". wp_let.
343
    iMod locking_heap_init as (?) "Hσ".
344
    pose (amg := AMonadG Σ _ _ _ _).
345 346
    iSpecialize ("Hwp" $! amg). rewrite cwp_eq /cwp_def.
    wp_apply (newflock_spec cmonadN); first done.
Dan Frumin's avatar
Dan Frumin committed
347
    iIntros (k γ') "#Hlock". iApply wp_fupd.
348
    iMod (flock_res_alloc_strong _  _ _ (env_inv env)%I
Dan Frumin's avatar
Dan Frumin committed
349
        with "Hlock [Henv Hσ]") as (ρ) "[_ Hres]"; first done.
Dan Frumin's avatar
Dan Frumin committed
350 351
    { iNext. iExists , . iFrame. iPureIntro; set_solver. }
    wp_let.
Dan Frumin's avatar
Dan Frumin committed
352
    iMod (wp_value_inv with "Hwp") as "Hwp".
Dan Frumin's avatar
Dan Frumin committed
353
    iApply (wp_wand with "[Hwp Hres]").
Dan Frumin's avatar
Dan Frumin committed
354
    - iApply ("Hwp" $! _ _ _ {[ρ := (1%Qp,_)]} with "Hlock [Hres] []").
Dan Frumin's avatar
Dan Frumin committed
355
      + rewrite /flock_resources big_sepM_singleton //.
356
      + by rewrite big_sepM_singleton right_id.
Dan Frumin's avatar
Dan Frumin committed
357 358
    - iIntros (w) "[HΦ Hres]".
      rewrite /flock_resources big_sepM_singleton /=.
359
      by iMod (flock_res_dealloc with "Hlock Hres") as "Henv".
Dan Frumin's avatar
Dan Frumin committed
360
  Qed.
361
End cwp_run.
Dan Frumin's avatar
Dan Frumin committed
362

Dan Frumin's avatar
Dan Frumin committed
363
(* Make sure that we only use the provided rules and don't break the abstraction *)
364 365
Typeclasses Opaque c_ret c_bind c_run c_atomic c_atomic_env c_par.
Opaque c_ret c_bind c_run c_atomic c_atomic_env c_par.
Dan Frumin's avatar
Dan Frumin committed
366

Dan Frumin's avatar
Dan Frumin committed
367 368 369 370 371 372
(* Definition locking_heapΣ : gFunctors := *)
(*   #[heapΣ; GFunctor (auth.authR locking_heapUR)]. *)

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

373 374
(* Definition cwp_adequacy Σ R s v σ φ : *)
(*   (R -∗ (∀ `{locking_heapG Σ}, cwp (of_val v) R (λ w, R -∗ ⌜φ w⌝)))%I → *)
Dan Frumin's avatar
Dan Frumin committed
375 376 377 378 379 380 381 382
(*   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. *)