flock.v 24.1 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
  (** all_props lemmas *)
  Lemma all_props_empty : all_props .
134
  Proof. by rewrite /all_props big_sepM_empty. Qed.
Dan Frumin's avatar
Dan Frumin committed
135

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

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

144 145 146 147 148
  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.
149
    - intros g. by rewrite big_sepM_empty !left_id.
150
    - intros i P f' Hi IH.
151
      intros g. rewrite big_sepM_insert; last done.
152 153 154 155 156 157
      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.
158
        rewrite big_sepM_insert; last first.
159 160
        { apply lookup_delete. }
        iDestruct "Hg" as "[HR Hg]".
161
        iApply (big_sepM_insert_override_2 _ _ i R P with "[-HP] [HP]"); simpl.
162 163
        { apply lookup_union_Some_raw. right. eauto. }
        * iApply (IH g).
164
          rewrite Hfoo big_sepM_insert; last by apply lookup_delete.
165 166
          rewrite delete_insert; last by apply lookup_delete. iFrame.
        * eauto.
167
      + rewrite big_sepM_insert; last first.
168 169 170 171 172 173 174 175 176
        { 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.
177
    - intros g. rewrite big_sepM_empty.
178
      simple refine (map_ind (fun g =>   g  _  _) _ _ g); simpl.
179
      + by rewrite big_sepM_empty.
180 181 182 183
      + 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'.
184
      rewrite big_sepM_insert; last done.
185 186 187 188 189 190 191 192 193 194
      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. }
195
      rewrite (big_sepM_delete _ g i R); eauto.
196 197
      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
  Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R E :
    flockN  E 
Dan Frumin's avatar
Dan Frumin committed
229
    is_flock γ lk - unflocked γ π -  R
Dan Frumin's avatar
Dan Frumin committed
230
    ={E}=  s, s  X  flock_res_single γ s R  unflocked γ π.
231
  Proof.
Dan Frumin's avatar
Dan Frumin committed
232 233
    iIntros (?) "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first solve_ndisj.
234 235 236
    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
237 238 239 240 241
      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. }
242 243 244 245 246 247 248
      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
249
        rewrite to_props_map_dom. done. }
250 251
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
Dan Frumin's avatar
Dan Frumin committed
252 253
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2".
Dan Frumin's avatar
Dan Frumin committed
254
        iApply all_props_insert; last iFrame.
Dan Frumin's avatar
Dan Frumin committed
255 256 257 258 259 260
        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.
261 262
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
Dan Frumin's avatar
Dan Frumin committed
263 264 265 266 267
      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. }
268 269 270 271 272 273
      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
274
        rewrite to_props_map_dom. done. }
275 276 277 278 279
      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
280 281 282
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,,_. rewrite left_id. iFrame. iFrame "Hactive".
        iSplit; auto.
Dan Frumin's avatar
Dan Frumin committed
283
        iApply all_props_insert; last by iFrame.
Dan Frumin's avatar
Dan Frumin committed
284 285 286 287 288 289 290
        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.

Dan Frumin's avatar
Dan Frumin committed
291 292 293 294
  Lemma flock_res_alloc_unflocked γ lk π R E :
    flockN  E 
    is_flock γ lk - unflocked γ π -  R
    ={E}= flock_res γ R  unflocked γ π.
Dan Frumin's avatar
Dan Frumin committed
295
  Proof.
Dan Frumin's avatar
Dan Frumin committed
296 297 298
    iIntros (?) "#Hlk Hunfl HR".
    iMod (flock_res_single_alloc_unflocked  with "Hlk Hunfl HR")
      as (s ?) "[HR $]"; first done.
Dan Frumin's avatar
Dan Frumin committed
299
    iModIntro. iExists {[s := R]}.
Dan Frumin's avatar
Dan Frumin committed
300
    rewrite /flock_res_single to_props_map_singleton. iFrame "HR".
Dan Frumin's avatar
Dan Frumin committed
301
    iPureIntro. symmetry. apply all_props_singleton.
Dan Frumin's avatar
Dan Frumin committed
302 303
  Qed.

Dan Frumin's avatar
Dan Frumin committed
304 305
  Lemma flock_res_insert_unflocked γ lk π P R E :
    flockN  E 
Dan Frumin's avatar
Dan Frumin committed
306
    is_flock γ lk - flock_res γ P - unflocked γ π -  R
Dan Frumin's avatar
Dan Frumin committed
307
    ={E}= flock_res γ (PR)  unflocked γ π.
Dan Frumin's avatar
Dan Frumin committed
308
  Proof.
Dan Frumin's avatar
Dan Frumin committed
309
    iIntros (?) "#Hlk #Hres Hunfl HR".
Dan Frumin's avatar
Dan Frumin committed
310 311
    iDestruct "Hres" as (f Hfeq) "Hf".
    iMod (flock_res_single_alloc_unflocked (dom (gset prop_id) f)
Dan Frumin's avatar
Dan Frumin committed
312
            with "Hlk Hunfl HR") as (s Hs) "[HR $]"; first done.
Dan Frumin's avatar
Dan Frumin committed
313 314 315 316 317 318 319 320 321 322
    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
323
        rewrite to_props_map_lookup.
Dan Frumin's avatar
Dan Frumin committed
324 325 326 327 328 329 330 331
        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
332 333
    iPureIntro. rewrite all_props_insert.
    - by rewrite comm Hfeq.
Dan Frumin's avatar
Dan Frumin committed
334
    - by apply (not_elem_of_dom (D:=gset prop_id)).
335 336 337 338 339 340
  Qed.

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

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

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

Dan Frumin's avatar
Dan Frumin committed
515 516 517
  Lemma cancel_lock γ lk R E :
    flockN  E 
    is_flock γ lk - flock_res γ R - unflocked γ 1 ={E}=  R.
Dan Frumin's avatar
Dan Frumin committed
518
  Proof.
Dan Frumin's avatar
Dan Frumin committed
519
    rewrite /is_flock /unflocked =>?.
Dan Frumin's avatar
Dan Frumin committed
520 521
    iDestruct 1 as "(#Hcinv & #Hislock)".
    iIntros "#Hres Hcown".
Dan Frumin's avatar
Dan Frumin committed
522
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; first solve_ndisj; eauto.
Dan Frumin's avatar
Dan Frumin committed
523 524 525 526 527 528 529 530 531 532 533
    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.

Dan Frumin's avatar
Dan Frumin committed
534 535 536
  Lemma cancel_lock_single γ lk s R E :
    flockN  E 
    is_flock γ lk - flock_res_single γ s R - unflocked γ 1 ={E}=  R.
537 538
  Proof.
    rewrite /is_flock /unflocked.
539 540
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown".
    rewrite /flock_res.
Dan Frumin's avatar
Dan Frumin committed
541
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; first solve_ndisj; eauto.
542
    iIntros "[Hcown Hstate]".
543 544
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
545
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
546 547 548 549 550 551 552 553 554
    - 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
555
        rewrite to_props_map_lookup fmap_Some_equiv=>-[R'' [/= Hf ->]].
556 557 558
        intros [?%to_agree_inj | ?%to_agree_included]%Some_included;
          simplify_eq/=; exists R''; eauto. }
      destruct Hfoo as [R' [HReq Hf]].
559
      rewrite /all_props {1}(big_sepM_lookup_acc _ fa s R'); last done.
560 561 562
      iDestruct "Hfa" as "[HR' Hfa]".
      assert (( R)%I  ( R')%I) as ->. by apply bi.later_proper.
      by iFrame.
563
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
564
End flock.