flock.v 23.5 KB
Newer Older
1
(** Cancellable locks *)
Léon Gondelman's avatar
Léon Gondelman committed
2
From iris.heap_lang Require Export proofmode notation.
3
From iris.heap_lang Require Import spin_lock.
4 5
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
From iris.algebra Require Import auth agree excl frac gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From iris.bi.lib Require Import fractional.
Léon Gondelman's avatar
Léon Gondelman committed
7

8 9 10 11 12
Inductive lockstate :=
  | Locked : frac  lockstate
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

13 14
Instance lockstate_inhabited : Inhabited lockstate := populate Unlocked.

15 16 17 18
Record flock_name := {
  flock_lock_name : gname;
  flock_cinv_name : gname;
  flock_state_name : gname;
19 20
  flock_props_name : gname;
  flock_props_active_name : gname
21 22
}.

23 24 25
(* positive so that we have a `Fresh` instance for `gset positive` *)
Definition prop_id := positive.

26 27 28
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
29 30 31 32
    flock_cinvG  :> cinvG Σ;
    flock_lockG  :> lockG Σ;
    flock_props :> authG Σ (optionUR (exclR (gmapC prop_id (iProp Σ))));
    flock_props_activeG :> authG Σ (gmapUR prop_id (agreeR (iProp Σ)))
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
  }.

Section cinv_lemmas.
  Context `{invG Σ, cinvG Σ}.

  Lemma cinv_alloc_strong (G : gset gname) E N (Φ : gname  iProp Σ) :
     ( γ, ⌜γ  G  Φ γ) ={E}=  γ, ⌜γ  G  cinv N γ (Φ γ)  cinv_own γ 1.
  Proof.
    iIntros "HP".
    iMod (own_alloc_strong 1%Qp G) as (γ) "[% H1]"; first done.
    iMod (inv_alloc N _ (Φ γ  own γ 1%Qp)%I with "[HP]") as "#Hinv".
    - iNext. iLeft. by iApply "HP".
    - iExists γ. iModIntro. rewrite /cinv /cinv_own. iFrame "H1".
      iSplit; eauto. iExists _. iFrame "Hinv".
      iIntros "!# !>". iSplit; by iIntros "?".
  Qed.

  Lemma cinv_cancel_vs (P Q : iProp Σ) E N γ :
    N  E  cinv N γ P
    - (cinv_own γ 1   P ={E∖↑N}= cinv_own γ 1   Q)
    - cinv_own γ 1 ={E}=  Q.
  Proof.
    iIntros (?) "#Hinv Hvs Hγ". rewrite /cinv.
    iDestruct "Hinv" as (P') "[#HP' Hinv]".
    iInv N as "[HP|>Hγ']" "Hclose"; last first.
    - iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
    - iMod ("Hvs" with "[$Hγ HP]") as "[Hγ HQ]".
      { by iApply "HP'". }
      iFrame. iApply "Hclose". iNext. by iRight.
  Qed.

End cinv_lemmas.

Léon Gondelman's avatar
Léon Gondelman committed
66
Section flock.
67 68 69
  Context `{heapG Σ, flockG Σ}.

  Variable N : namespace.
70 71 72 73
  Definition flockN := N.@"flock".

  Definition to_props_map (f : gmap prop_id (iProp Σ))
    : gmapUR prop_id (agreeR (iProp Σ)) := to_agree <$> f.
Dan Frumin's avatar
Dan Frumin committed
74

Dan Frumin's avatar
Dan Frumin committed
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
  Definition all_props (f : gmap prop_id (iProp Σ)) : iProp Σ :=
    ([ map] i  R  f, R)%I.

  Definition flock_inv (γ : flock_name) : iProp Σ :=
    ( (s : lockstate) (fp fa : gmap prop_id (iProp Σ)),
       (** fa -- active propositions, fp -- inactive propositions *)
       own (flock_state_name γ) ( (Excl' s)) 
       own (flock_props_name γ) ( to_props_map (fp  fa)) 
       own (flock_props_active_name γ) ( Excl' fa) 
       match s with
       | Locked q =>
         cinv_own (flock_cinv_name γ) (q/2) 
         locked (flock_lock_name γ) 
         all_props fp
       | Unlocked => own (flock_props_active_name γ) ( Excl' fa) 
                     all_props fa 
                     fp = ∅⌝ (** all the propositions are active *)
       end)%I.

  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
    (cinv (flockN .@ "inv") (flock_cinv_name γ) (flock_inv γ) 
     is_lock (flockN .@ "lock") (flock_lock_name γ) lk
         (own (flock_state_name γ) ( (Excl' Unlocked))))%I.

  Definition unflocked (γ : flock_name) (q : frac) : iProp Σ :=
    cinv_own (flock_cinv_name γ) q.

  Definition flocked
    (γ : flock_name) (q : frac) (f : gmap prop_id (iProp Σ)) : iProp Σ :=
    (own (flock_state_name γ) ( (Excl' (Locked q)))
      cinv_own (flock_cinv_name γ) (q/2)
      own (flock_props_active_name γ) ( Excl' f)
       all_props f)%I.

  Definition flock_res (γ : flock_name) (R : iProp Σ) : iProp Σ :=
    ( f, R  all_props f  own (flock_props_name γ) ( to_props_map f))%I.

  Definition flock_res_single (γ : flock_name) (s : prop_id) (R : iProp Σ) : iProp Σ :=
    (own (flock_props_name γ) ( {[ s := to_agree R ]}))%I.

115 116 117 118
  Lemma to_props_map_insert f i P :
    to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f).
  Proof. by rewrite /to_props_map fmap_insert. Qed.

Dan Frumin's avatar
Dan Frumin committed
119 120 121 122
  Lemma to_props_map_lookup f i :
    to_props_map f !! i = to_agree <$> f !! i.
  Proof. by rewrite /to_props_map lookup_fmap. Qed.

123 124 125 126
  Lemma to_props_map_dom f :
    dom (gset prop_id) (to_props_map f) = dom (gset prop_id) f.
  Proof. by rewrite /to_props_map dom_fmap_L. Qed.

Dan Frumin's avatar
Dan Frumin committed
127 128 129 130 131
  Lemma to_props_map_singleton s R : to_props_map {[s := R]} = {[s := to_agree R]}.
  Proof. by rewrite /to_props_map map_fmap_singleton. Qed.

  Lemma all_props_singleton s R : all_props {[s := R]}  R.
  Proof. by rewrite /all_props bi.big_sepM_singleton. Qed.
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186

  Lemma all_props_union f g :
    all_props f  all_props g  all_props (f  g).
  Proof.
    revert g.
    simple refine (map_ind (fun f =>  g, all_props f  all_props g - all_props (f  g)) _ _ f); simpl; rewrite /all_props.
    - intros g. by rewrite bi.big_sepM_empty !left_id.
    - intros i P f' Hi IH.
      intros g. rewrite bi.big_sepM_insert; last done.
      iIntros "[[HP Hf] Hg]".
      rewrite -insert_union_l.
      remember (g !! i) as Z. destruct Z as [R|].
      + assert (g = <[i:=R]>(delete i g)) as Hfoo.
        { rewrite insert_delete insert_id; eauto. }
        rewrite {1}Hfoo.
        rewrite bi.big_sepM_insert; last first.
        { apply lookup_delete. }
        iDestruct "Hg" as "[HR Hg]".
        iApply (bi.big_sepM_insert_override_2 _ _ i R P with "[-HP] [HP]"); simpl.
        { apply lookup_union_Some_raw. right. eauto. }
        * iApply (IH g).
          rewrite Hfoo bi.big_sepM_insert; last by apply lookup_delete.
          rewrite delete_insert; last by apply lookup_delete. iFrame.
        * eauto.
      + rewrite bi.big_sepM_insert; last first.
        { apply lookup_union_None. eauto. }
        iFrame. iApply (IH g). iFrame.
  Qed.

  Global Instance all_props_proper : Proper (() ==> ())
    (all_props : gmapC prop_id (iProp Σ)  iProp Σ).
  Proof.
    intros f. rewrite /all_props. (* rewrite /all_props /big_opM. *)
    simple refine (map_ind (fun f =>  g, f  g  _  _) _ _ f); simpl.
    - intros g. rewrite bi.big_sepM_empty.
      simple refine (map_ind (fun g =>   g  _  _) _ _ g); simpl.
      + by rewrite bi.big_sepM_empty.
      + intros j R g' Hj IH Hg'.
        exfalso. specialize (Hg' j). revert Hg'.
        rewrite lookup_insert lookup_empty. inversion 1.
    - intros i P f' Hi IH g Hf'.
      rewrite bi.big_sepM_insert; last done.
      specialize (IH (delete i g)).
      assert (f'  delete i g) as Hf'g.
      { by rewrite -Hf' delete_insert. }
      specialize (IH Hf'g). rewrite IH.
      assert ( R, g !! i = Some R  P  R) as [R [Hg HR]].
      { specialize (Hf' i).
        destruct (g !! i) as [R|]; last first.
        - exfalso. revert Hf'. rewrite lookup_insert. inversion 1.
        - exists R. split; auto.
          revert Hf'. rewrite lookup_insert. by inversion 1. }
      rewrite (bi.big_sepM_delete _ g i R); eauto.
      by apply bi.sep_proper.
  Qed.
187

188 189 190
  Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk).
  Proof. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
191
  Global Instance flock_res_persistent γ R : Persistent (flock_res γ R).
192 193
  Proof. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
194 195 196 197 198 199 200 201 202
  Global Instance flock_res_single_persistent γ s R : Persistent (flock_res_single γ s R).
  Proof. apply _. Qed.

  Global Instance flock_res_proper : Proper ((=) ==> () ==> ()) flock_res.
  Proof.
    intros ? γ -> P R HPR. rewrite /flock_res.
    apply bi.exist_proper=>f. by rewrite HPR.
  Qed.

203
  Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
204
    unflocked γ (π1+π2)  unflocked γ π1  unflocked γ π2.
205 206
  Proof. by rewrite /unflocked fractional. Qed.

207
  Global Instance unflocked_fractional γ : Fractional (unflocked γ).
208
  Proof. intros p q. apply unflocked_op. Qed.
Dan Frumin's avatar
Dan Frumin committed
209

210 211
  Global Instance unflocked_as_fractional γ π :
    AsFractional (unflocked γ π) (unflocked γ) π.
Léon Gondelman's avatar
Léon Gondelman committed
212 213
  Proof. split. done. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
214 215 216
  Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R :
    is_flock γ lk - unflocked γ π -  R
    ={}=  s, s  X  flock_res_single γ s R  unflocked γ π.
217
  Proof.
218 219 220 221 222
    iIntros "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
Dan Frumin's avatar
Dan Frumin committed
223 224 225 226 227
      pose (s := (fresh ((dom (gset prop_id) (fp  fa))  X))).
      assert (s  (dom (gset prop_id) (fp  fa))) as Hs.
      { intros Hs.
        apply (elem_of_union_l s (dom (gset prop_id) (fp  fa)) X) in Hs.
        revert Hs. apply is_fresh. }
228 229 230 231 232 233 234
      iMod (own_update  with "Hauth") as "Hauth".
      { apply (auth_update_alloc _ (to_props_map (<[s := R]> fp  fa))
                                 {[ s := to_agree R ]}).
        rewrite -insert_union_l.
        rewrite to_props_map_insert.
        apply alloc_local_update; last done.
        apply (not_elem_of_dom (to_props_map (fp  fa)) s (D:=gset prop_id)).
Dan Frumin's avatar
Dan Frumin committed
235
        rewrite to_props_map_dom. done. }
236 237
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
Dan Frumin's avatar
Dan Frumin committed
238 239 240 241 242 243 244 245 246
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2".
        rewrite /all_props bi.big_sepM_insert. iFrame.
        apply (not_elem_of_dom _ s (D:=gset prop_id)).
        revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. }
      iModIntro. iPureIntro.
      clear Hs. intros Hs.
      apply (elem_of_union_r s (dom (gset prop_id) (fp  fa)) X) in Hs.
      revert Hs. apply is_fresh.
247 248
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
Dan Frumin's avatar
Dan Frumin committed
249 250 251 252 253
      pose (s := (fresh (dom (gset prop_id) fa  X))).
      assert (s  (dom (gset prop_id) fa)) as Hs.
      { intros Hs.
        apply (elem_of_union_l s _ X) in Hs.
        revert Hs. apply is_fresh. }
254 255 256 257 258 259
      iMod (own_update  with "Hauth") as "Hauth".
      { apply (auth_update_alloc _ (to_props_map (<[s := R]> fa))
                                 {[ s := to_agree R ]}).
        rewrite to_props_map_insert.
        apply alloc_local_update; last done.
        apply (not_elem_of_dom (to_props_map fa) s (D:=gset prop_id)).
Dan Frumin's avatar
Dan Frumin committed
260
        rewrite to_props_map_dom. done. }
261 262 263 264 265
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
      iMod (own_update_2 _ _ _ (( Excl' (<[s:=R]>fa))  ( Excl' (<[s:=R]>fa)))
              with "Hactive Hfactive") as "[Hactive Hfactive]".
      { by apply auth_update, option_local_update, exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,,_. rewrite left_id. iFrame. iFrame "Hactive".
        iSplit; auto.
        rewrite /all_props bi.big_sepM_insert. iFrame.
        by apply (not_elem_of_dom _ s (D:=gset prop_id)). }
      iModIntro. iPureIntro.
      clear Hs. intros Hs.
      apply (elem_of_union_r s (dom (gset prop_id) fa) X) in Hs.
      revert Hs. apply is_fresh.
  Qed.

  Lemma flock_res_alloc_unflocked γ lk π R :
    is_flock γ lk - unflocked γ π -  R ={}= flock_res γ R  unflocked γ π.
  Proof.
    iIntros "#Hlk Hunfl HR".
    iMod (flock_res_single_alloc_unflocked  with "Hlk Hunfl HR") as (s ?) "[HR $]".
    iModIntro. iExists {[s := R]}.
Dan Frumin's avatar
Dan Frumin committed
283
    rewrite /flock_res_single to_props_map_singleton. iFrame "HR".
Dan Frumin's avatar
Dan Frumin committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304
    iPureIntro. by rewrite /all_props bi.big_sepM_singleton.
  Qed.

  Lemma flock_res_insert_unflocked γ lk π P R :
    is_flock γ lk - flock_res γ P - unflocked γ π -  R
    ={}= flock_res γ (PR)  unflocked γ π.
  Proof.
    iIntros "#Hlk #Hres Hunfl HR".
    iDestruct "Hres" as (f Hfeq) "Hf".
    iMod (flock_res_single_alloc_unflocked (dom (gset prop_id) f)
            with "Hlk Hunfl HR") as (s Hs) "[HR $]".
    iModIntro. iExists (<[s := R]>f).
    rewrite to_props_map_insert /flock_res_single.
    iCombine "HR Hf" as "HR".
    (* TODO this should be a lemma, somewhere in std++ *)
    rewrite /op /cmra_op /= /ucmra_op /= /gmap_op /=.
    assert ((merge op {[s := to_agree R]} (to_props_map f))
            = <[s:=to_agree R]> (to_props_map f)) as Hmerge.
    { apply map_eq=>i. rewrite lookup_merge.
      destruct (decide (s = i)) as [->|?].
      - rewrite lookup_singleton lookup_insert.
Dan Frumin's avatar
Dan Frumin committed
305
        rewrite to_props_map_lookup.
Dan Frumin's avatar
Dan Frumin committed
306 307 308 309 310 311 312 313 314 315 316
        assert (f !! i = None) as ->.
        + by rewrite -(not_elem_of_dom (D:=(gset prop_id))).
        + simpl. done.
      - rewrite lookup_singleton_ne; auto.
        rewrite lookup_insert_ne; auto.
        remember (to_props_map f !! i) as o. rewrite -Heqo.
        by destruct o. }
    rewrite Hmerge. iFrame "HR".
    iPureIntro. rewrite /all_props bi.big_sepM_insert; last first.
    - by apply (not_elem_of_dom (D:=gset prop_id)).
    - rewrite comm Hfeq /all_props. reflexivity.
317 318 319 320 321 322
  Qed.

  Lemma newlock_cancel_spec :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk  unflocked γ 1 }}}.
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
323 324
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
325 326 327 328 329 330 331
    iMod (own_alloc ( to_props_map )) as (γ_props) "Hprops".
    { apply auth_valid_discrete. simpl.
      split; last done. apply ucmra_unit_least. }
    iMod (own_alloc (( Excl' )  ( Excl' ))) as (γ_ac_props) "[Hacprops1 Hacprops2]".
    { apply auth_valid_discrete. simpl.
      split; last done. by rewrite left_id. }
    iApply (newlock_spec (flockN.@"lock") (own γ_state ( (Excl' Unlocked))) with "Hfrag").
332
    iNext. iIntros (lk γ_lock) "#Hlock".
333 334
    iMod (cinv_alloc_strong  _ (flockN.@"inv")
       (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state γ_props γ_ac_props)) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
335
    { iNext. rewrite /flock_inv /=. iIntros (γ _).
336 337 338 339
      iExists Unlocked, , . rewrite left_id. iFrame.
      by rewrite /all_props !bi.big_sepM_empty. }
    pose (γ := (Build_flock_name γ_lock γ_cinv γ_state γ_props γ_ac_props)).
    iModIntro. iApply ("HΦ" $! lk γ with "[-]"). iFrame "Hown".
340 341
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
342

Dan Frumin's avatar
Dan Frumin committed
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364
  Lemma flock_res_auth γ R fp :
    flock_res γ R -
    own (flock_props_name γ) ( to_props_map fp) -
     f', all_props fp  R  all_props f'.
  Proof.
    rewrite /flock_res. iDestruct 1 as (f Heq) "#Hf".
    iIntros "Hauth".
    iDestruct (own_valid_2 with "Hauth Hf")
      as %[Hfoo _]%auth_valid_discrete.
    iPureIntro. revert Hfoo. simpl. rewrite left_id.
    rewrite lookup_included. intros Hffp.
    exists (fp  f). rewrite Heq /all_props. revert Hffp.
    simple refine (map_ind (fun f => ( i, _)  _  _) _ _ f); simpl.
    - (* TODO: this should be somewhere in std++ *)
      assert (fp   = fp) as ->.
      { apply map_eq=>i. remember (fp !! i) as XX. destruct XX.
        - apply lookup_difference_Some. eauto.
        - apply lookup_difference_None. eauto. }
      by rewrite bi.big_sepM_empty left_id.
    - intros i P f' Hi IH Hffp. rewrite IH; last first.
      { intros j. specialize (Hffp j).
        destruct (decide (i = j)) as [->|?].
Dan Frumin's avatar
Dan Frumin committed
365
        - rewrite !to_props_map_lookup Hi. simpl.
Dan Frumin's avatar
Dan Frumin committed
366 367
          apply option_included. eauto.
        - revert Hffp.
Dan Frumin's avatar
Dan Frumin committed
368
          rewrite !to_props_map_lookup lookup_insert_ne; auto. }
Dan Frumin's avatar
Dan Frumin committed
369 370
      rewrite bi.big_sepM_insert; last assumption.
      specialize (Hffp i). revert Hffp.
Dan Frumin's avatar
Dan Frumin committed
371
      rewrite !to_props_map_lookup lookup_insert; auto. simpl.
Dan Frumin's avatar
Dan Frumin committed
372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436
      rewrite option_included.
      intros [Hffp | [? [Q' [HP [HQ HeqQ]]]]]; first by inversion Hffp.
      simplify_eq/=. remember (fp !! i) as XX.
      destruct XX as [Q|]; simpl in HQ; last first.
      { inversion HQ. }
      simplify_eq/=.
      assert (P  Q) as HPQ.
      { by destruct HeqQ as [?%to_agree_inj |?%to_agree_included]. }
      clear HeqQ.
      assert (fp = <[i:=Q]>(delete i fp)) as ->.
      { by rewrite insert_delete insert_id. }
      assert (<[i:=Q]> (delete i fp)  f' = <[i:=Q]>((delete i fp)  f')) as ->.
      { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
        - by rewrite lookup_insert lookup_difference_Some lookup_insert.
        - rewrite lookup_insert_ne; auto.
          unfold difference, map_difference; rewrite !lookup_difference_with.
          rewrite lookup_insert_ne; auto. }
      rewrite bi.big_sepM_insert; last first.
      { apply lookup_difference_None. left. apply lookup_delete. }
      assert ((<[i:=Q]> (delete i fp)  <[i:=P]> f') = (delete i fp  f')) as ->.
      { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
        - unfold difference, map_difference; rewrite !lookup_difference_with.
            by rewrite !lookup_insert lookup_delete Hi.
        - unfold difference, map_difference; rewrite !lookup_difference_with.
          rewrite !lookup_insert_ne; auto. }
      iSplit; rewrite {1}HPQ. iIntros "($ & $ & $)".
      iIntros "[[$ $] $]".
  Qed.

  Lemma acquire_cancel_spec γ π lk R :
    {{{ is_flock γ lk  unflocked γ π  flock_res γ R }}}
      acquire lk
    {{{ f, RET #();  R  ( R - flocked γ π f) }}}.
  Proof.
    iIntros (Φ) "(Hl & Hunfl & #HRres) HΦ". rewrite -wp_fupd.
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iApply (acquire_spec with "Hlk"). iNext.
    iIntros "[Hlocked Hunlk]".
    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
      iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
      { apply (auth_update _ _ (Excl' (Locked π)) (Excl' (Locked π))).
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hflkd]".
      iDestruct "Hunfl" as "[Hunfl Hcown]".
      iDestruct (flock_res_auth with "HRres Hauth") as %Hfoo.
      destruct Hfoo as [f' Hf'].
      iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]") as "_".
      { iNext. iExists (Locked π),,fa. rewrite left_id. iFrame.
        by rewrite /all_props bi.big_sepM_empty. }
      iModIntro. rewrite Hf'. iDestruct "Hfa" as "[HR Hf']".
      iApply ("HΦ" $! fa). iFrame.
      iApply bi.later_wand. iNext. iIntros "HR".
      rewrite Hf'. iFrame.
  Qed.

  (* TODO: derive this from acquire_cancel_spec *)
  Lemma acquire_single_cancel_spec γ π lk s R :
    {{{ is_flock γ lk  unflocked γ π  flock_res_single γ s R }}}
437
      acquire lk
438
    {{{ f, RET #();  R  ( R - flocked γ π f) }}}.
439
  Proof.
Dan Frumin's avatar
Dan Frumin committed
440 441 442 443 444
    iIntros (Φ) "(Hl & Hunfl & Hres) HΦ".
    rewrite /flock_res_single.
    iApply (acquire_cancel_spec with "[$Hl $Hunfl Hres]"); last done.
    iExists {[s := R]}.
    rewrite to_props_map_singleton all_props_singleton. eauto.
445
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
446

447 448
  Lemma release_cancel_spec γ π lk f :
    {{{ is_flock γ lk  flocked γ π f }}}
449 450 451
      release lk
    {{{ RET #(); unflocked γ π }}}.
  Proof.
452
    iIntros (Φ) "(Hl & (Hstate' & Hflkd & Hactive & Hf)) HΦ". rewrite -fupd_wp.
453 454 455
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
456 457
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)"; last first.
    - iDestruct "Hrest" as "(>Hactive2 & Hfa & >%)".
458 459 460 461 462 463
      iExFalso. iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
      iPureIntro. revert Hfoo.
      rewrite auth_valid_discrete /= left_id.
      intros [Hexcl _].
      apply Some_included_exclusive in Hexcl; try (done || apply _).
      simplify_eq.
464
    - iDestruct "Hrest" as "(>Hcown & >Hlocked & Hfp)".
465 466 467 468 469 470 471 472 473 474 475 476
      iAssert (q = π⌝)%I with "[Hstate Hstate']" as  %->.
      { iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
        iPureIntro. revert Hfoo.
        rewrite auth_valid_discrete /= left_id.
        intros [Hexcl _].
        apply Some_included_exclusive in Hexcl; try (done || apply _).
        by simplify_eq. }
      iMod (own_update_2 with "Hstate Hstate'") as "Hstate".
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hstate']".
477 478 479 480 481 482 483 484 485 486 487 488 489 490
      iAssert ((f : gmapC prop_id (iProp Σ))  fa%I) with "[Hactive Hfactive]" as %Hfoo.
      { iDestruct (own_valid_2 with "Hactive Hfactive") as %Hfoo.
        iPureIntro. apply auth_valid_discrete_2 in Hfoo.
        destruct Hfoo as [Hfoo _].
        apply Some_included_exclusive in Hfoo; [|apply _|done].
        by apply Excl_inj. }
      rewrite {1}Hfoo.
      iMod (own_update_2 _ _ _ ( Excl' (fp  fa)   Excl' (fp  fa))
              with "Hactive Hfactive") as "[Hactive Hfactive]".
      { by apply auth_update, option_local_update, exclusive_local_update. }
      iMod ("Hcl" with "[Hstate Hauth Hfp Hf Hactive Hfactive]").
      { iNext. iExists Unlocked,,(fpfa). rewrite left_id. iFrame.
        rewrite Hfoo. iSplit; eauto.
        iApply all_props_union; iFrame. }
491 492
      iApply (release_spec with "[$Hlk $Hlocked $Hstate']").
      iModIntro. iNext. iIntros "_". iApply "HΦ".
493
      rewrite /unflocked. by iSplitL "Hcown".
494
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
495

Dan Frumin's avatar
Dan Frumin committed
496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515
  Lemma cancel_lock γ lk R :
    is_flock γ lk - flock_res γ R - unflocked γ 1 ={}=  R.
  Proof.
    rewrite /is_flock /unflocked.
    iDestruct 1 as "(#Hcinv & #Hislock)".
    iIntros "#Hres Hcown".
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
    iIntros "[Hcown Hstate]".
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. iFrame. rewrite left_id.
      iDestruct (flock_res_auth with "Hres Hauth") as %Hfoo.
      destruct Hfoo as [f' Hf'].
      iModIntro. rewrite Hf'. iDestruct "Hfa" as "[$ ?]".
  Qed.

  Lemma cancel_lock_single γ lk s R :
    is_flock γ lk - flock_res_single γ s R - unflocked γ 1 ={}=  R.
516 517
  Proof.
    rewrite /is_flock /unflocked.
518 519
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown".
    rewrite /flock_res.
520
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
521
    iIntros "[Hcown Hstate]".
522 523
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
524
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
525 526 527 528 529 530 531 532 533
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. iFrame. rewrite left_id.
      iAssert ( R', R  R'  fa !! s = Some R')%I
        with "[Hres Hauth]" as %Hfoo.
      { iDestruct (own_valid_2 with "Hauth Hres")
          as %[Hfoo _]%auth_valid_discrete.
        iPureIntro. revert Hfoo.
        rewrite /= left_id singleton_included=> -[R' [Hf HR]].
        revert Hf HR.
Dan Frumin's avatar
Dan Frumin committed
534
        rewrite to_props_map_lookup fmap_Some_equiv=>-[R'' [/= Hf ->]].
535 536 537 538 539 540 541
        intros [?%to_agree_inj | ?%to_agree_included]%Some_included;
          simplify_eq/=; exists R''; eauto. }
      destruct Hfoo as [R' [HReq Hf]].
      rewrite /all_props {1}(bi.big_sepM_lookup_acc _ fa s R'); last done.
      iDestruct "Hfa" as "[HR' Hfa]".
      assert (( R)%I  ( R')%I) as ->. by apply bi.later_proper.
      by iFrame.
542
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
543
End flock.