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
  Definition flock_resources (γ : flock_name) (I : gmap prop_id lock_res) :=
68
    ([ map] i  X  I, flock_res cmonadN γ i X)%I.
Dan Frumin's avatar
Dan Frumin committed
69

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

      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.
 *)
77
  Definition cwp_def (e : expr)
Léon Gondelman's avatar
Léon Gondelman committed
78
      (R : iProp Σ) (Φ : val  iProp Σ) : iProp Σ :=
79
    WP e {{ ev,
Dan Frumin's avatar
Dan Frumin committed
80
       (γ : flock_name) (env : val) (l : val) (I : gmap prop_id lock_res),
81
        is_flock cmonadN γ l -
Robbert Krebbers's avatar
Robbert Krebbers committed
82
        flock_resources γ I -
Dan Frumin's avatar
Dan Frumin committed
83
        ([ map] X  I, res_prop X)  (env_inv env  R) -
Robbert Krebbers's avatar
Robbert Krebbers committed
84
        WP ev env l {{ v, Φ v  flock_resources γ I }}
85
    }}%I.
86 87 88 89
  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.
90

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

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

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

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

115 116 117 118
  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
119

120 121 122 123
  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
124

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

152 153
  Lemma cwp_fupd_wand e Φ Ψ R :
    CWP e @ R {{ Φ }} -
154
    ( v, Φ v ={}= Ψ v) -
155
    CWP e @ R {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  Proof.
157
    iIntros "Hwp H". rewrite cwp_eq.
158 159
    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
160
    iApply (wp_wand with "[HΦ Hres]"). iApply ("HΦ" with "Hflock Hres Heq").
161 162 163
    iIntros (w) "[HΦ $]". by iApply "H".
  Qed.

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

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

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

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

191 192
  Lemma cwp_ret e R Φ :
    WP e {{ Φ }} - CWP c_ret e @ R {{ Φ }}.
Léon Gondelman's avatar
Léon Gondelman committed
193
  Proof.
194
    iIntros "Hwp". rewrite cwp_eq /cwp_def. wp_apply (wp_wand with "Hwp").
Robbert Krebbers's avatar
Robbert Krebbers committed
195 196
    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
197 198
  Qed.

199 200 201
  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
202
  Proof.
203
    iIntros "Hwp". rewrite cwp_eq /cwp_def.
Dan Frumin's avatar
Dan Frumin committed
204
    wp_apply (wp_wand with "Hwp"). iIntros (ev) "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
205 206
    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
207
    iApply (wp_wand with "[Hwp Hres]"). iApply ("Hwp" with "Hflock Hres Heq").
Dan Frumin's avatar
Dan Frumin committed
208
    iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
Dan Frumin's avatar
Dan Frumin committed
209
    iIntros (v) "H". iApply ("H" with "Hflock Hres Heq").
Léon Gondelman's avatar
Léon Gondelman committed
210 211
  Qed.

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

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

267 268 269
  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
270
     ( w1 w2, Ψ1 w1 - Ψ2 w2 -  Φ (w1,w2)%V) -
271
    CWP e1 ||| e2 @ R {{ Φ }}.
Léon Gondelman's avatar
Léon Gondelman committed
272
  Proof.
273
    iIntros "Hwp1 Hwp2 HΦ". rewrite cwp_eq /cwp_def.
Dan Frumin's avatar
Dan Frumin committed
274 275 276
    wp_apply (wp_wand with "Hwp2").
    iIntros (ev2) "Hwp2".
    wp_apply (wp_wand with "Hwp1").
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278
    iIntros (ev1) "Hwp1". wp_lam. wp_pures.
    iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
Dan Frumin's avatar
Dan Frumin committed
279
    pose (I' := fmap (λ X, LockRes (res_prop X) (res_frac X/2) (res_name X)) I).
Dan Frumin's avatar
Dan Frumin committed
280 281 282 283 284 285 286
    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
287 288
      with "[Hwp1 Hres1] [Hwp2 Hres2]").
    - wp_lam. iApply ("Hwp1" with "Hlock Hres1").
Dan Frumin's avatar
Dan Frumin committed
289
      by rewrite /I' big_sepM_fmap /=.
Dan Frumin's avatar
Dan Frumin committed
290
    - wp_lam. iApply ("Hwp2" with "Hlock Hres2").
Dan Frumin's avatar
Dan Frumin committed
291 292 293 294 295 296 297 298
      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
299 300
      iApply ("HΦ" with "[$] [$]").
  Qed.
301

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

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

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

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

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

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

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

Dan Frumin's avatar
Dan Frumin committed
362
(* Make sure that we only use the provided rules and don't break the abstraction *)
363 364
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
365

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

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

372 373
(* 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
374 375 376 377 378 379 380 381
(*   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. *)