flock.v 24 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.

Dan Frumin's avatar
Dan Frumin committed
115 116
  (** **************************************** *)
  (** to_props_map lemmas *)
117 118 119 120
  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
121 122 123 124
  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.

125 126 127 128
  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
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.

Dan Frumin's avatar
Dan Frumin committed
132 133 134 135
  (** all_props lemmas *)
  Lemma all_props_empty : all_props .
  Proof. by rewrite /all_props bi.big_sepM_empty. Qed.

Dan Frumin's avatar
Dan Frumin committed
136 137
  Lemma all_props_singleton s R : all_props {[s := R]}  R.
  Proof. by rewrite /all_props bi.big_sepM_singleton. Qed.
138

Dan Frumin's avatar
Dan Frumin committed
139 140 141 142 143
  Lemma all_props_insert s (R : iProp Σ) f :
    f !! s = None 
    all_props (<[s := R]>f)  (R  all_props f)%I.
  Proof. intros ?. rewrite /all_props bi.big_sepM_insert //. Qed.

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 187 188 189 190 191 192 193 194 195 196 197
  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.
198

Dan Frumin's avatar
Dan Frumin committed
199 200
  (** **************************************** *)
  (** rules & properties of the predicates *)
201 202 203
  Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk).
  Proof. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
204
  Global Instance flock_res_persistent γ R : Persistent (flock_res γ R).
205 206
  Proof. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
207 208 209 210 211 212 213 214 215
  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.

216
  Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
217
    unflocked γ (π1+π2)  unflocked γ π1  unflocked γ π2.
218 219
  Proof. by rewrite /unflocked fractional. Qed.

220
  Global Instance unflocked_fractional γ : Fractional (unflocked γ).
221
  Proof. intros p q. apply unflocked_op. Qed.
Dan Frumin's avatar
Dan Frumin committed
222

223 224
  Global Instance unflocked_as_fractional γ π :
    AsFractional (unflocked γ π) (unflocked γ) π.
Léon Gondelman's avatar
Léon Gondelman committed
225 226
  Proof. split. done. apply _. Qed.

Dan Frumin's avatar
Dan Frumin committed
227 228 229
  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 γ π.
230
  Proof.
231 232 233 234 235
    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
236 237 238 239 240
      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. }
241 242 243 244 245 246 247
      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
248
        rewrite to_props_map_dom. done. }
249 250
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
Dan Frumin's avatar
Dan Frumin committed
251 252
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2".
Dan Frumin's avatar
Dan Frumin committed
253
        iApply all_props_insert; last iFrame.
Dan Frumin's avatar
Dan Frumin committed
254 255 256 257 258 259
        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.
260 261
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
Dan Frumin's avatar
Dan Frumin committed
262 263 264 265 266
      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. }
267 268 269 270 271 272
      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
273
        rewrite to_props_map_dom. done. }
274 275 276 277 278
      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
279 280 281
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,,_. rewrite left_id. iFrame. iFrame "Hactive".
        iSplit; auto.
Dan Frumin's avatar
Dan Frumin committed
282
        iApply all_props_insert; last by iFrame.
Dan Frumin's avatar
Dan Frumin committed
283 284 285 286 287 288 289 290 291 292 293 294 295
        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
296
    rewrite /flock_res_single to_props_map_singleton. iFrame "HR".
Dan Frumin's avatar
Dan Frumin committed
297
    iPureIntro. symmetry. apply all_props_singleton.
Dan Frumin's avatar
Dan Frumin committed
298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
  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
318
        rewrite to_props_map_lookup.
Dan Frumin's avatar
Dan Frumin committed
319 320 321 322 323 324 325 326
        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".
Dan Frumin's avatar
Dan Frumin committed
327 328
    iPureIntro. rewrite all_props_insert.
    - by rewrite comm Hfeq.
Dan Frumin's avatar
Dan Frumin committed
329
    - by apply (not_elem_of_dom (D:=gset prop_id)).
330 331 332 333 334 335
  Qed.

  Lemma newlock_cancel_spec :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk  unflocked γ 1 }}}.
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
336 337
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
338 339 340 341 342 343 344
    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").
345
    iNext. iIntros (lk γ_lock) "#Hlock".
346 347
    iMod (cinv_alloc_strong  _ (flockN.@"inv")
       (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state γ_props γ_ac_props)) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
348
    { iNext. rewrite /flock_inv /=. iIntros (γ _).
349
      iExists Unlocked, , . rewrite left_id. iFrame.
Dan Frumin's avatar
Dan Frumin committed
350
      iSplit; auto. iApply all_props_empty. }
351 352
    pose (γ := (Build_flock_name γ_lock γ_cinv γ_state γ_props γ_ac_props)).
    iModIntro. iApply ("HΦ" $! lk γ with "[-]"). iFrame "Hown".
353 354
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
355

Dan Frumin's avatar
Dan Frumin committed
356 357 358 359 360 361 362 363 364 365 366
  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.
Dan Frumin's avatar
Dan Frumin committed
367
    exists (fp  f). rewrite Heq. clear Heq. revert Hffp.
Dan Frumin's avatar
Dan Frumin committed
368 369 370 371 372 373
    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. }
Dan Frumin's avatar
Dan Frumin committed
374 375
      intros _. iSplit; [iIntros "$" | iIntros "[_ $]"].
      iApply all_props_empty.
Dan Frumin's avatar
Dan Frumin committed
376 377 378
    - 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
379
        - rewrite !to_props_map_lookup Hi. simpl.
Dan Frumin's avatar
Dan Frumin committed
380 381
          apply option_included. eauto.
        - revert Hffp.
Dan Frumin's avatar
Dan Frumin committed
382
          rewrite !to_props_map_lookup lookup_insert_ne; auto. }
Dan Frumin's avatar
Dan Frumin committed
383
      rewrite all_props_insert; last assumption.
Dan Frumin's avatar
Dan Frumin committed
384
      specialize (Hffp i). revert Hffp.
Dan Frumin's avatar
Dan Frumin committed
385
      rewrite !to_props_map_lookup lookup_insert; auto. simpl.
Dan Frumin's avatar
Dan Frumin committed
386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402
      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. }
Dan Frumin's avatar
Dan Frumin committed
403
      rewrite all_props_insert; last first.
Dan Frumin's avatar
Dan Frumin committed
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 437 438 439 440
      { 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.
Dan Frumin's avatar
Dan Frumin committed
441
        iApply all_props_empty. }
Dan Frumin's avatar
Dan Frumin committed
442 443 444 445 446 447 448 449 450
      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 }}}
451
      acquire lk
452
    {{{ f, RET #();  R  ( R - flocked γ π f) }}}.
453
  Proof.
Dan Frumin's avatar
Dan Frumin committed
454 455 456 457 458
    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.
459
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
460

461 462
  Lemma release_cancel_spec γ π lk f :
    {{{ is_flock γ lk  flocked γ π f }}}
463 464 465
      release lk
    {{{ RET #(); unflocked γ π }}}.
  Proof.
466
    iIntros (Φ) "(Hl & (Hstate' & Hflkd & Hactive & Hf)) HΦ". rewrite -fupd_wp.
467 468 469
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
470 471
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)"; last first.
    - iDestruct "Hrest" as "(>Hactive2 & Hfa & >%)".
472 473 474 475 476 477
      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.
478
    - iDestruct "Hrest" as "(>Hcown & >Hlocked & Hfp)".
479 480 481 482 483 484 485 486 487 488 489 490
      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']".
491 492 493 494 495 496 497 498 499 500 501 502 503 504
      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. }
505 506
      iApply (release_spec with "[$Hlk $Hlocked $Hstate']").
      iModIntro. iNext. iIntros "_". iApply "HΦ".
507
      rewrite /unflocked. by iSplitL "Hcown".
508
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
509

Dan Frumin's avatar
Dan Frumin committed
510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529
  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.
530 531
  Proof.
    rewrite /is_flock /unflocked.
532 533
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown".
    rewrite /flock_res.
534
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; eauto.
535
    iIntros "[Hcown Hstate]".
536 537
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
538
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
539 540 541 542 543 544 545 546 547
    - 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
548
        rewrite to_props_map_lookup fmap_Some_equiv=>-[R'' [/= Hf ->]].
549 550 551 552 553 554 555
        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.
556
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
557
End flock.