flock.v 28.8 KB
Newer Older
Léon Gondelman's avatar
Léon Gondelman committed
1
From iris.heap_lang Require Export proofmode notation.
Dan Frumin's avatar
Dan Frumin committed
2 3
(* From iris.heap_lang Require Import spin_lock. *)
From iris_c.lib Require Export spin_lock.
4
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
Dan Frumin's avatar
Dan Frumin committed
5
From iris.algebra Require Import auth agree excl frac gmap gset.
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
Inductive lockstate :=
Dan Frumin's avatar
Dan Frumin committed
9
  | Locked
10 11 12
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

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

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

22 23
(* positive so that we have a `Fresh` instance for `gset positive` *)
Definition prop_id := positive.
Dan Frumin's avatar
Dan Frumin committed
24
Canonical Structure gnameC := leibnizC gname.
25

Dan Frumin's avatar
Dan Frumin committed
26 27 28 29 30 31 32
Record PropPerm := {
  prop_perm : frac;
  prop_saved_name : gname;
  prop_perm_name : gname
}.
Canonical Structure PropPermC := leibnizC PropPerm.

33 34 35
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
36
    flock_lockG  :> lockG Σ;
Dan Frumin's avatar
Dan Frumin committed
37 38
    flock_savedProp :> savedPropG Σ;
    flock_tokens :> inG Σ fracR;
Dan Frumin's avatar
Dan Frumin committed
39
    flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id PropPermC))));
Dan Frumin's avatar
Dan Frumin committed
40
    flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))
41 42
  }.

Dan Frumin's avatar
Dan Frumin committed
43 44 45 46 47
Definition flockΣ : gFunctors :=
  #[GFunctor (authR (optionUR (exclR lockstateC)))
   ;lockΣ
   ;savedPropΣ
   ;GFunctor fracR
Dan Frumin's avatar
Dan Frumin committed
48
   ;GFunctor (authR (optionUR (exclR (gmapC prop_id PropPermC))))
Dan Frumin's avatar
Dan Frumin committed
49
   ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))%CF].
50

Dan Frumin's avatar
Dan Frumin committed
51 52
Instance subG_flockΣ Σ : subG flockΣ Σ  flockG Σ.
Proof. solve_inG. Qed.
53

Léon Gondelman's avatar
Léon Gondelman committed
54
Section flock.
55 56
  Context `{heapG Σ, flockG Σ}.
  Variable N : namespace.
57
  Definition flockN := N.@"flock".
Dan Frumin's avatar
Dan Frumin committed
58
  
Dan Frumin's avatar
Dan Frumin committed
59 60 61 62
  Definition to_props_map (f : gmap prop_id (gname * gname))
    : gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))) :=
    (λ x, (1%Qp, to_agree (x.1, x.2))) <$> f.

Dan Frumin's avatar
Dan Frumin committed
63 64 65 66
  Definition to_props_map_ (f : gmap prop_id PropPerm)
    : gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))) :=
    (λ x, (prop_perm x, to_agree (prop_saved_name x, prop_perm_name x))) <$> f.

Dan Frumin's avatar
Dan Frumin committed
67 68 69 70 71 72 73 74 75
  Lemma to_props_map_singleton_included fp i q ρ:
    {[i := (q, to_agree ρ)]}  to_props_map fp  fp !! i = Some ρ.
  Proof.
    rewrite singleton_included=> -[[q' av] []].
    rewrite /to_props_map lookup_fmap fmap_Some_equiv => -[v' [Hi [/= -> ->]]].
    move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
    rewrite Hi. by destruct v'.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
76 77 78
  Definition from_active (f : gmap prop_id PropPerm)
    : gmap prop_id (gname * gname) :=
    (λ x, (prop_saved_name x, prop_perm_name x)) <$> f.
Dan Frumin's avatar
Dan Frumin committed
79 80 81 82 83 84

  Lemma from_active_empty : from_active  = .
  Proof. by rewrite /from_active fmap_empty. Qed.

  Definition all_props (f : gmap prop_id (gname*gname)) : iProp Σ :=
    ([ map] i  ρ  f,  R, saved_prop_own ρ.1 R  R)%I.
Dan Frumin's avatar
Dan Frumin committed
85

Dan Frumin's avatar
Dan Frumin committed
86 87 88 89 90 91 92
  Lemma all_props_to_props_map_ f f1 f2 :
    to_props_map f = to_props_map_ f1  to_props_map_ f2 
    all_props f  all_props (from_active f1)  all_props (from_active f2).
  Proof. Admitted.

  Definition all_tokens (f : gmap prop_id PropPerm) : iProp Σ :=
    ([ map] i  ρ  f, own (prop_perm_name ρ) (prop_perm ρ))%I.
Dan Frumin's avatar
Dan Frumin committed
93 94

  Definition flock_inv (γ : flock_name) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
95 96
    ( (s : lockstate)
       (fp : gmap prop_id (gname * gname))
Dan Frumin's avatar
Dan Frumin committed
97
       (fa : gmap prop_id PropPerm),
Dan Frumin's avatar
Dan Frumin committed
98 99
       (** fa -- active propositions, fp -- pending propositions *)
       fp ## from_active fa 
Dan Frumin's avatar
Dan Frumin committed
100
       own (flock_state_name γ) ( (Excl' s)) 
Dan Frumin's avatar
Dan Frumin committed
101
       own (flock_props_name γ) ( to_props_map (fp  from_active fa)) 
Dan Frumin's avatar
Dan Frumin committed
102
       own (flock_props_active_name γ) ( Excl' fa) 
Dan Frumin's avatar
Dan Frumin committed
103
       all_props fp 
Dan Frumin's avatar
Dan Frumin committed
104
       match s with
Dan Frumin's avatar
Dan Frumin committed
105
       | Locked =>
Dan Frumin's avatar
Dan Frumin committed
106
         locked (flock_lock_name γ) 
Dan Frumin's avatar
Dan Frumin committed
107 108
         all_tokens fa
       | Unlocked => own (flock_props_active_name γ) ( Excl' )
Dan Frumin's avatar
Dan Frumin committed
109 110 111
       end)%I.

  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
112
    (inv (flockN .@ "inv") (flock_inv γ) 
Dan Frumin's avatar
Dan Frumin committed
113 114 115 116
     is_lock (flockN .@ "lock") (flock_lock_name γ) lk
         (own (flock_state_name γ) ( (Excl' Unlocked))))%I.

  Definition flocked
Dan Frumin's avatar
Dan Frumin committed
117
    (γ : flock_name) (f : gmap prop_id PropPerm) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
118
    (own (flock_state_name γ) ( (Excl' Locked))
Dan Frumin's avatar
Dan Frumin committed
119
      own (flock_props_active_name γ) ( Excl' f)
Dan Frumin's avatar
Dan Frumin committed
120
      all_props (from_active f))%I.
121

Dan Frumin's avatar
Dan Frumin committed
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
  Definition flock_res (γ : flock_name) (s : prop_id) (R : iProp Σ) (π : Qp) : iProp Σ :=
    ( ρ, saved_prop_own ρ.1 R  own ρ.2 π
      own (flock_props_name γ) ( {[s := (π, to_agree ρ)]}))%I.

  Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) (π1 π2 : frac) :
    flock_res γ s R (π1+π2)  flock_res γ s R π1  flock_res γ s R π2.
  Proof.
    rewrite /flock_res. iSplit.
    - iDestruct 1 as (ρ) "(#Hsaved & Hρ & Hs)".
      iDestruct "Hρ" as "[Hρ1 Hρ2]".
      iDestruct "Hs" as "[Hs1 Hs2]".
      iSplitL "Hρ1 Hs1"; iExists _; by iFrame.
    - iIntros "[H1 H2]".
      iDestruct "H1" as (ρ) "(#Hsaved & Hρ1 & Hs1)".
      iDestruct "H2" as (ρ') "(_ & Hρ2 & Hs2)".
      iCombine "Hs1 Hs2" as "Hs".
      iDestruct (own_valid with "Hs")
        as %Hfoo%auth_valid_discrete.
      simpl in Hfoo. apply singleton_valid in Hfoo.
      destruct Hfoo as [_ Hfoo%agree_op_inv'].
      fold_leibniz. rewrite -!Hfoo.
      iCombine "Hρ1 Hρ2" as "Hρ".
      rewrite !frac_op' agree_idemp.
      iExists ρ. by iFrame.
  Qed.

  Global Instance flock_res_fractional γ s R : Fractional (flock_res γ s R).
  Proof. intros p q. apply flock_res_op. Qed.

  Global Instance flock_res_as_fractional γ s R π :
    AsFractional (flock_res γ s R π) (flock_res γ s R) π.
  Proof. split. done. apply _. Qed.
154

Dan Frumin's avatar
Dan Frumin committed
155
  Lemma flock_res_single_alloc (X : gset prop_id) γ lk R E :
Dan Frumin's avatar
Dan Frumin committed
156
    flockN  E 
Dan Frumin's avatar
Dan Frumin committed
157
    is_flock γ lk -  R
Dan Frumin's avatar
Dan Frumin committed
158
    ={E}=  s, s  X  flock_res γ s R 1.
159
  Proof.
Dan Frumin's avatar
Dan Frumin committed
160 161 162 163
    iIntros (?) "Hl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (saved_prop_alloc R) as (ρ1) "#Hρ1".
    iMod (own_alloc 1%Qp) as (ρ2) "Hρ2"; first done.
    iInv (flockN.@"inv") as (s fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl".
Dan Frumin's avatar
Dan Frumin committed
164 165
    pose (i := (fresh ((dom (gset prop_id) (fp  from_active fa))  X))).
    assert (i  (dom (gset prop_id) (fp  from_active fa))  X) as Hs.
Dan Frumin's avatar
Dan Frumin committed
166
    { apply is_fresh. }
Dan Frumin's avatar
Dan Frumin committed
167
    apply not_elem_of_union in Hs. destruct Hs as [Hi1 Hi2].
Dan Frumin's avatar
Dan Frumin committed
168 169 170 171 172 173 174 175
    iMod (own_update  with "Hauth") as "Hauth".
    { apply (auth_update_alloc _ (to_props_map (<[i := (ρ1,ρ2)]> fp  from_active fa))
                               {[ i := (1%Qp, to_agree (ρ1, ρ2)) ]}).
      rewrite -insert_union_l.
      rewrite /to_props_map /= fmap_insert.
      apply alloc_local_update; last done.
      apply (not_elem_of_dom (to_props_map (fp  from_active fa)) i (D:=gset prop_id)).
      by rewrite /to_props_map dom_fmap. }
176
      iDestruct "Hauth" as "[Hauth Hres]".
Dan Frumin's avatar
Dan Frumin committed
177 178 179 180 181 182 183 184 185 186 187 188
      iExists i. iMod ("Hcl" with "[-Hres Hρ1 Hρ2]") as "_".
      { iNext. iExists _,_,_. iFrame. iFrame "Hrest".
        rewrite /all_props big_sepM_insert; last first.
        + apply (not_elem_of_dom _ i (D:=gset prop_id)).
          revert Hi1. rewrite dom_union_L not_elem_of_union. set_solver.
        + iFrame "Hfp". iSplitR; last by eauto.
          iPureIntro. apply map_disjoint_insert_l_2; eauto.
          eapply (not_elem_of_dom (D:=gset prop_id)).
          intros Hi; apply Hi1. rewrite dom_union_L elem_of_union.
          eauto. }
      iModIntro; iSplit; eauto.
      iExists (ρ1,ρ2). iFrame "Hres Hρ1 Hρ2".
Dan Frumin's avatar
Dan Frumin committed
189
  Qed.
Dan Frumin's avatar
Dan Frumin committed
190

Dan Frumin's avatar
Dan Frumin committed
191
  Lemma flock_res_single_dealloc γ lk i R E :
Dan Frumin's avatar
Dan Frumin committed
192
    flockN  E 
Dan Frumin's avatar
Dan Frumin committed
193
    is_flock γ lk - flock_res γ i R 1
Dan Frumin's avatar
Dan Frumin committed
194
    ={E}=  R',  R'    (R  R').
Dan Frumin's avatar
Dan Frumin committed
195
  Proof.
Dan Frumin's avatar
Dan Frumin committed
196 197 198
    iIntros (?) "Hl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl".
    - iDestruct "Hrest" as ">[Hlocked Htokens]".
Dan Frumin's avatar
Dan Frumin committed
199
      iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
Dan Frumin's avatar
Dan Frumin committed
200
      iDestruct (own_valid_2 with "Hauth HR")
Dan Frumin's avatar
Dan Frumin committed
201
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
202
      iAssert (fa !! i = None)%I with "[-]" as %Hbar.
Dan Frumin's avatar
Dan Frumin committed
203
      { remember (fa !! i) as fai. destruct fai as [[π ρ'1 ρ'2]|]; last done.
Dan Frumin's avatar
Dan Frumin committed
204 205 206 207 208 209 210 211 212 213 214 215 216 217
        iExFalso.
        assert (fp !! i = None) as Hbar.
        { apply lookup_union_Some_raw in Hfoo.
          destruct Hfoo as [Hfoo | [? ?]]; last done.
          specialize (H2 i). revert H2. rewrite Hfoo.
          rewrite /from_active lookup_fmap -Heqfai /=. done. }
        apply lookup_union_Some in Hfoo; last done.
        destruct Hfoo as [Hfoo | Hfa].
        - exfalso. rewrite Hfoo in Hbar. inversion Hbar.
        - revert Hfa. rewrite /from_active lookup_fmap -Heqfai /= =>Hfa.
          rewrite /all_tokens (big_sepM_lookup _ fa i); last done.
          simplify_eq/=.
          iDestruct (own_valid with "Htokens") as %Hbaz1%frac_valid'.
          iDestruct (own_valid_2 with "Hρ2 Htokens") as %Hbaz2.
Dan Frumin's avatar
Dan Frumin committed
218 219
          rewrite frac_op' in Hbaz2. exfalso.
          eapply Qp_not_plus_q_ge_1. apply Hbaz2. }
Dan Frumin's avatar
Dan Frumin committed
220 221 222 223 224 225 226 227 228 229 230 231 232 233
      assert (fp !! i = Some (ρ1, ρ2)) as Hbaz.
      { apply lookup_union_Some in Hfoo; last done.
        destruct Hfoo as [? | Hfoo]; first done.
        exfalso. revert Hfoo. rewrite  /from_active lookup_fmap Hbar. done. }

      iMod (own_update_2 with "Hauth HR") as "Hauth".
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }

      rewrite /all_props (big_sepM_delete _ fp i (ρ1,ρ2)); last done.
      iDestruct "Hfp" as "[HR' Hfp]".
      iDestruct "HR'" as (R') "[Hsaved HR']".
      iDestruct (saved_prop_agree with "Hρ1 Hsaved") as "Hfoo".
      iMod ("Hcl" with "[-HR' Hfoo Hρ2]") as "_".
      { iNext. iExists Locked, (delete i fp),fa. iFrame.
Dan Frumin's avatar
Dan Frumin committed
234 235
        iSplit.
        { iPureIntro. by apply map_disjoint_delete_l. }
Dan Frumin's avatar
Dan Frumin committed
236 237 238 239 240 241 242 243 244 245
        rewrite /to_props_map -fmap_delete.
        rewrite delete_union (delete_notin (from_active fa)); first iFrame.
        by rewrite /from_active lookup_fmap Hbar. }
      iModIntro. iExists R'. iFrame.
    - iDestruct "Hrest" as ">Haactive".
      iAssert (fa = ∅⌝)%I with "[-]" as %->.
      { iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        iPureIntro. by unfold_leibniz. }
      rewrite from_active_empty right_id.
Dan Frumin's avatar
Dan Frumin committed
246
      iDestruct "HR" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
Dan Frumin's avatar
Dan Frumin committed
247
      iDestruct (own_valid_2 with "Hauth HR")
Dan Frumin's avatar
Dan Frumin committed
248
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
249 250 251 252 253 254 255 256 257 258 259 260
      iMod (own_update_2 with "Hauth HR") as "Hauth".
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
      rewrite /all_props (big_sepM_delete _ fp i (ρ1,ρ2)); last done.
      iDestruct "Hfp" as "[HR' Hfp]".
      iDestruct "HR'" as (R') "[Hsaved HR']".
      iDestruct (saved_prop_agree with "Hρ1 Hsaved") as "Hfoo".
      iMod ("Hcl" with "[-HR' Hfoo Hρ2]") as "_".
      { iNext. iExists Unlocked, (delete i fp),. iFrame.
        rewrite !from_active_empty right_id.
        rewrite /to_props_map fmap_delete. iFrame "Hauth".
        iPureIntro. apply map_disjoint_empty_r. }
      iModIntro. iExists R'. iFrame.
Dan Frumin's avatar
Dan Frumin committed
261
  Qed.
262 263

  Lemma newlock_cancel_spec :
Dan Frumin's avatar
Dan Frumin committed
264
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
265 266
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
267 268
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
269 270 271 272 273 274 275
    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").
276
    iNext. iIntros (lk γ_lock) "#Hlock".
Dan Frumin's avatar
Dan Frumin committed
277 278 279 280 281
    pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
    iMod (inv_alloc (flockN.@"inv") _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
    { iNext. iExists Unlocked, , . rewrite from_active_empty right_id. iFrame.
      iSplit; eauto. by rewrite /all_props big_sepM_empty. }
    iModIntro. iApply ("HΦ" $! lk γ with "[-]").
282 283
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
284

Dan Frumin's avatar
Dan Frumin committed
285 286 287 288 289 290 291 292
    (* {{{ is_flock γ lk ∗ *)
    (*     ([∗ list] (i, R, π) ∈ I, flock_res γ i R π) }}} *)
    (*   acquire lk *)
    (* {{{ RET #(); *)
    (*     ▷ ▷ ([∗ list] (i, R, π) ∈ I, R) ∗ *)
    (*     (▷ ([∗ list] (i, R, π) ∈ I, R)  *)
    (*         ={⊤}=∗ flocked γ ∅ ∗ ([∗ list] (i, R, π) ∈ I, flock_res γ i R π) }}}. *)

Dan Frumin's avatar
Dan Frumin committed
293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 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 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489
  Lemma extract_existential {A B C : Type} `{EqDecision A, Countable A} (I : gmap A B) (P : A -> B -> C -> iProp Σ) :
    (([ map] a  b  I,  c : C, P a b c) 
      J : gmap A (B*C), fmap fst J = I  [ map] a  bc  J, P a bc.1 bc.2)%I.
  Proof.
    simple refine (map_ind (λ I, (([ map] a  b  I,  c : C, P a b c) 
      J : gmap A (B*C), fmap fst J = I  [ map] a  bc  J, P a bc.1 bc.2)) _ _ I); simpl.
    - rewrite big_sepM_empty.
      iIntros "_". iExists . iSplit; eauto. by rewrite fmap_empty.
    - iIntros (a b I' Ha HI') "H".
      rewrite big_sepM_insert; auto.
      iDestruct "H" as "[HC H]".
      iDestruct "HC" as (c) "Habc".
      rewrite HI'. iDestruct "H" as (J' HJ') "H".
      iExists (<[a:=(b,c)]>J'). iSplit.
      + iPureIntro. by rewrite fmap_insert /=HJ'.
      + rewrite big_sepM_insert; eauto with iFrame.
        cut (fst <$> J' !! a = None).
        { destruct (J' !! a); eauto; inversion 1. }
        rewrite -lookup_fmap HJ' //.
  Qed.

  Lemma big_sepM_own_frag {A B : Type} `{EqDecision A, Countable A}
        `{inG Σ (authR (gmapUR A C))} (f : B  C) (m : gmap A B) (γ : gname) : 
    own γ ( ) -
    own γ ( (f <$> m)) - [ map] ix  m, own γ ( {[ i := f x ]}).
  Proof.
    simple refine (map_ind (λ m, _)%I _ _ m); simpl.
    - iIntros "He". rewrite fmap_empty big_sepM_empty. iSplit; eauto.
    - iIntros (i x m' Hi IH) "He".
      rewrite fmap_insert insert_union_singleton_l.
      assert (({[i := f x]}  (f <$> m')) = {[i := f x]}  (f <$> m')) as ->.
      { rewrite /op /cmra_op /= /gmap_op.
        apply map_eq. intros j. destruct (decide (i = j)) as [->|?].
        - etransitivity. eapply lookup_union_Some_l. apply lookup_insert.
          symmetry. rewrite lookup_merge lookup_insert.
          rewrite lookup_fmap Hi /=. done.
        - remember (m' !! j) as mj.
          destruct mj; simplify_eq/=.
          + etransitivity. apply lookup_union_Some_raw.
            right. split; first by rewrite lookup_insert_ne.
            by rewrite lookup_fmap -Heqmj.
            symmetry. rewrite lookup_merge lookup_singleton_ne; eauto.
            rewrite lookup_fmap -Heqmj. done.
          + etransitivity. apply lookup_union_None.
            split; first by rewrite lookup_singleton_ne.
            rewrite lookup_fmap -Heqmj //.
            symmetry.
            rewrite lookup_merge lookup_singleton_ne // lookup_fmap -Heqmj //. }
      rewrite auth_frag_op own_op IH big_sepM_insert; last eauto.
      iSplit; iIntros "[$ Hm']"; by iApply "He".
  Qed.

(* here it is crucial that we use a gmap:
     that way there is at most one flock_res associated with a prop_id *)
  Lemma acquire_cancel_spec γ lk (I : gmap prop_id (iProp Σ * frac)) :
    {{{ is_flock γ lk  [ map] i  p  I, flock_res γ i p.1 p.2 }}}
      acquire lk
    {{{ RET #();
        ( [ map] p  I, p.1)
      (( [ map] p  I, p.1) ={}= flocked γ  
                               [ map] i  p  I, flock_res γ i p.1 p.2) }}}.
  Proof.
    iIntros (Φ) "(Hl & HRres) HΦ".
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
    iApply (acquire_spec with "Hlk").
    iNext. iIntros "[Hlocked Hunlk]".
    iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl".
    - iDestruct "Hrest" as "(>Hlocked2 & Htokens)".
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
    - iDestruct "Hrest" as ">Haactive".
      iAssert (fa = ∅⌝)%I with "[-]" as %->.
      { iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        iPureIntro. by unfold_leibniz. }
      rewrite from_active_empty right_id.

      (* Unlocked ~~> Locked *)
      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 (extract_existential with "HRres") as (J HJ) "HRres".

      iAssert (([ map] abc  J, own (flock_props_name γ) ( {[a := (bc.1.2, to_agree bc.2)]}))  ([ map] abc  J, saved_prop_own bc.2.1 bc.1.1  own bc.2.2 bc.1.2))%I with "[HRres]" as "[Hfs HJ]".
      { rewrite -big_sepM_sepM. iApply (big_sepM_mono with "HRres").
        iIntros (k x Hk) "(? & ? & ?)". eauto with iFrame. }
      pose (fs := fmap (λ bc, {| prop_perm := bc.1.2; prop_saved_name := bc.2.1; prop_perm_name := bc.2.2 |}) J).

      iMod (own_update _ _ ( to_props_map fp   ) with "Hauth") as "[Hauth He]".
      { by apply auth_update_alloc. }
      iAssert (own (flock_props_name γ) ( to_props_map_ fs))%I with "[Hfs He]" as "Hfs".
      { unfold fs. iApply (big_sepM_own_frag with "He").
        rewrite big_sepM_fmap /=. iApply (big_sepM_mono with "Hfs").
        iIntros (k x Hk) "H /=". by destruct (x.2). }

      (* fs ≤ fp *)
      iDestruct (own_valid_2 with "Hauth Hfs")
        as %[Hfoo _]%auth_valid_discrete_2.

      assert ( fo : gmap prop_id PropPerm,
                 to_props_map fp = to_props_map_ fs  to_props_map_ fo)
        as [fo Hfo].
      { admit. }
      
      rewrite (all_props_to_props_map_ fp fs fo); last done.
      iDestruct "Hfp" as "[Hfs_props Hfo]".

      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
      { apply (auth_update _ _ (Excl' fs)
                               (Excl' fs)).
        by apply option_local_update, exclusive_local_update. }      
     
      rewrite (big_sepM_sepM _ _ J).
      iDestruct "HJ" as "[#HJ Htokens]".

      iMod ("Hcl" with "[-HΦ Haactive Hflkd Hfs_props Hfs HJ]") as "_".
      { iNext. iExists Locked,(from_active fo),fs.
        iFrame. iSplitR. admit. (* TODO: map_disjoint *)
        iSplitL "Hauth".
        - admit. (* fp = from_active fo ∪ from_active fs *)
        - rewrite /all_tokens /fs big_sepM_fmap /= //. }
      
      iAssert (▷▷ [ map] p  I, p.1)%I with "[Hfs_props]" as "Hfs_props".
      { iNext. rewrite /all_props /fs -HJ !big_sepM_fmap big_sepM_later /=.
        (* TODO: why is big_sepM_mono not formulated with the persistence modality? *)
        iCombine "HJ Hfs_props" as "Hfs".
        rewrite -big_sepM_sepM.
        iApply (big_sepM_mono with "Hfs").
        iIntros (k ρ Hk) "[#Hsaved HR]".
        iDestruct "HR" as (R') "[Hsaved' HR']".
        iDestruct (saved_prop_agree with "Hsaved Hsaved'") as "#Hfoo".
        iNext. iRewrite -"Hfoo" in "HR'". done.
        (* TODO: iRewrite "Hfoo" didn't work *) }
        
      iModIntro. iApply "HΦ".
      iNext. iFrame "Hfs_props". iIntros "Hfs_props".
      clear Hfoo H1 Hfo fp. rewrite /flocked /flock_res.
      iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl"; last first.
      + iDestruct (own_valid_2 with "Hstate Hflkd")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        fold_leibniz. inversion Hfoo.
      + iDestruct "Hrest" as ">[Hlocked Htokens]".

        iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        fold_leibniz. simplify_eq/=.

        iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
        { apply (auth_update _ _ (Excl' ) (Excl' )).
          by apply option_local_update, exclusive_local_update. }

        (* fs ≤ fp *)
        iDestruct (own_valid_2 with "Hauth Hfs")
          as %[Hfoo _]%auth_valid_discrete_2.

        iMod (own_update _ _ ( to_props_map _   ) with "Hauth") as "[Hauth He]".
        { by apply auth_update_alloc. }

        iMod ("Hcl" with "[Hlocked Hstate Hauth Hfactive Hfp Hfs_props]") as "_".
        { iNext. iExists Locked,(fp  from_active fs),. iFrame.
          iSplitR.
          { rewrite from_active_empty. iPureIntro. apply map_disjoint_empty_r. }
          iSplitL "Hauth".
          - by rewrite from_active_empty right_id.
          - iSplitL; last first.
            { by rewrite /all_tokens big_sepM_empty. }
            rewrite big_sepM_fmap.
            rewrite /fs /from_active.
            (* TODO: need all_props union lemma *)
            admit. }
        iModIntro. iFrame. rewrite /all_props from_active_empty big_sepM_empty.
        iSplitR; first done. rewrite /all_tokens big_sepM_fmap.
        rewrite {1}/fs /to_props_map_ -map_fmap_compose /=.
        iAssert ([ map] ky  J, own (flock_props_name γ) ( {[k := (y.1.2, to_agree y.2)]}))%I with "[Hfs He]" as "Hfs".
        { iApply (big_sepM_own_frag with "He"); simpl.
          assert (((λ y, (y.1.2, to_agree y.2)) <$> J) = ((λ x : PropPerm, (prop_perm x,
                                 to_agree (prop_saved_name x, prop_perm_name x)))
                 (λ bc : iProp Σ * Qp * (gname * gname), 
                   {|
                   prop_perm := bc.1.2;
                   prop_saved_name := bc.2.1;
                   prop_perm_name := bc.2.2 |}) <$> J)) as Hh.
          { apply map_eq=>i /=. rewrite !lookup_fmap /=.
            destruct (J !! i);eauto. simpl. by destruct (p.2). }
          rewrite Hh. done. }
        iCombine "Hfs Htokens" as "Hm".
        rewrite /fs big_sepM_fmap -big_sepM_sepM.
        iCombine "HJ Hm" as "Hm". rewrite -big_sepM_sepM.
        iApply (big_sepM_mono with "Hm").
        iIntros (k x Hk) "(Hsaved & Hx & Hperm)". simpl.
        iExists x.2. iFrame.
  Admitted.


  Lemma acquire_single_cancel_spec γ π lk i R :
Dan Frumin's avatar
Dan Frumin committed
490
    {{{ is_flock γ lk  flock_res γ i R π }}}
Dan Frumin's avatar
Dan Frumin committed
491
      acquire lk
Dan Frumin's avatar
Dan Frumin committed
492
    {{{ RET #();  R  ( R ={}= flocked γ   flock_res γ i R π) }}}.
Dan Frumin's avatar
Dan Frumin committed
493
  Proof.
Dan Frumin's avatar
Dan Frumin committed
494 495 496 497 498 499
    iIntros (Φ) "(Hl & HRres) HΦ".
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
    iApply (acquire_spec with "Hlk").
    iNext. iIntros "[Hlocked Hunlk]".
    iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl".
    - iDestruct "Hrest" as "(>Hlocked2 & Htokens)".
Dan Frumin's avatar
Dan Frumin committed
500
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
Dan Frumin's avatar
Dan Frumin committed
501 502 503 504 505 506
    - iDestruct "Hrest" as ">Haactive".
      iAssert (fa = ∅⌝)%I with "[-]" as %->.
      { iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        iPureIntro. by unfold_leibniz. }
      rewrite from_active_empty right_id.
Dan Frumin's avatar
Dan Frumin committed
507
      iDestruct "HRres" as ([ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
Dan Frumin's avatar
Dan Frumin committed
508 509

      (* Unlocked ~~> Locked *)
Dan Frumin's avatar
Dan Frumin committed
510
      iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
Dan Frumin's avatar
Dan Frumin committed
511
      { apply (auth_update _ _ (Excl' Locked) (Excl' Locked)).
Dan Frumin's avatar
Dan Frumin committed
512 513 514
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
515

Dan Frumin's avatar
Dan Frumin committed
516 517
      (* (i,ρ) ∈ fp *)
      iDestruct (own_valid_2 with "Hauth HR")
Dan Frumin's avatar
Dan Frumin committed
518
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
519 520 521 522 523

      rewrite /all_props (big_sepM_delete _ fp i (ρ1,ρ2)); last done.
      iDestruct "Hfp" as "[HR' Hfp]".
      iDestruct "HR'" as (R') "[Hsaved HR']".
      iDestruct (saved_prop_agree with "Hρ1 Hsaved") as "#Hfoo".
Dan Frumin's avatar
Dan Frumin committed
524

Dan Frumin's avatar
Dan Frumin committed
525 526
      (* move (i,ρ) to the set of active propositions *)
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
Dan Frumin's avatar
Dan Frumin committed
527 528 529 530 531 532 533
      { apply (auth_update _ _ (Excl' {[ i := {| prop_perm := π;
                                                 prop_saved_name := ρ1;
                                                 prop_perm_name := ρ2 |} ]})
                               (Excl' {[ i := {| prop_perm := π;
                                                 prop_saved_name := ρ1;
                                                 prop_perm_name := ρ2 |} ]})).
        by apply option_local_update, exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
534

Dan Frumin's avatar
Dan Frumin committed
535
      iMod ("Hcl" with "[-HΦ HR' Hfoo Haactive Hflkd HR]") as "_".
Dan Frumin's avatar
Dan Frumin committed
536 537 538
      { iNext. iExists Locked,(delete i fp),{[i := {| prop_perm := π;
                                                      prop_saved_name := ρ1;
                                                      prop_perm_name := ρ2 |}]}.
Dan Frumin's avatar
Dan Frumin committed
539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559
        iFrame. iSplitR. admit. (* TODO: map_disjoint *)
        iSplitL "Hauth".
        - rewrite /from_active map_fmap_singleton /=.
          assert (fp = (delete i fp  {[i := (ρ1, ρ2)]})) as <-.
          { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
            - remember (fp !! j) as fpj. destruct fpj.
              + symmetry. apply lookup_union_Some.
                admit. (* TODO map disjoint *)
                right. simplify_eq/=. apply lookup_singleton.
              + symmetry. apply lookup_union_None. naive_solver.
            - remember (fp !! j) as fpj. destruct fpj.
              + symmetry. apply lookup_union_Some.
                admit. (* TODO map disjoint *)
                left. simplify_eq/=. rewrite lookup_delete_ne; eauto.
              + symmetry. apply lookup_union_None. split; eauto.
                * rewrite lookup_delete_ne; eauto.
                * rewrite lookup_singleton_ne; eauto. }
          iFrame.
        - rewrite /all_tokens big_sepM_singleton //. }
      iModIntro. (* iApply ("HΦ" $! {[ i := (π, (ρ1, ρ2)) ]}). *)
      iApply "HΦ".
Dan Frumin's avatar
Dan Frumin committed
560 561 562
      iNext. iAssert ( R)%I with "[HR']" as "HR'".
      { iNext. by iRewrite "Hfoo". }
      iFrame "HR'". iIntros "HR'".
Dan Frumin's avatar
Dan Frumin committed
563 564 565 566 567 568
      clear Hfoo H1 fp. rewrite /flocked /flock_res.
      iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl"; last first.
      + iDestruct (own_valid_2 with "Hstate Hflkd")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        fold_leibniz. inversion Hfoo.
      + iDestruct "Hrest" as ">[Hlocked Htokens]".
Dan Frumin's avatar
Dan Frumin committed
569

Dan Frumin's avatar
Dan Frumin committed
570 571 572 573 574 575 576 577 578 579 580 581 582
        iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        fold_leibniz. simplify_eq/=.

        iAssert (fp !! i = None)%I with "[-]" as %Hbar.
        { remember (fp !! i) as fpi. destruct fpi as [[ρ'1 ρ'2]|]; last done.
          exfalso. specialize (H1 i). revert H1. rewrite -Heqfpi.
          rewrite /from_active lookup_fmap lookup_singleton. done. }

        iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
        { apply (auth_update _ _ (Excl' )
                                 (Excl' )).
          apply option_local_update. by apply exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
583

Dan Frumin's avatar
Dan Frumin committed
584 585 586 587 588 589 590 591 592 593 594
        iMod ("Hcl" with "[HR' Hlocked Hstate Hauth Hfactive Hfp]") as "_".
        { iNext. iExists Locked,(<[i := (ρ1,ρ2)]>fp),.
          iSplitR.
          { rewrite from_active_empty. iPureIntro. apply map_disjoint_empty_r. }
          iFrame "Hstate Hfactive Hlocked".
          iSplitL "Hauth".
          - rewrite from_active_empty right_id /from_active map_fmap_singleton.
            rewrite insert_union_singleton_r; done.
          - rewrite /all_tokens /all_props big_sepM_empty. iSplitL; last done.
            rewrite big_sepM_insert; last done.
            iFrame "Hfp". iExists R'. iFrame. simpl.
Dan Frumin's avatar
Dan Frumin committed
595
            iRewrite "Hfoo" in "Hρ1". iRewrite "Hfoo" in "HR'". by iFrame. }
Dan Frumin's avatar
Dan Frumin committed
596 597 598
        iModIntro. iFrame. rewrite /all_props from_active_empty big_sepM_empty.
        iSplitR; first done.
        rewrite /all_tokens big_sepM_singleton. simpl.
Dan Frumin's avatar
Dan Frumin committed
599
        iExists (ρ1, ρ2). by iFrame.
Dan Frumin's avatar
Dan Frumin committed
600 601 602 603
  Admitted.

  Lemma release_cancel_spec γ lk :
    {{{ is_flock γ lk  flocked γ  }}}
604
      release lk
Dan Frumin's avatar
Dan Frumin committed
605
    {{{ RET #(); True }}}.
606
  Proof.
Dan Frumin's avatar
Dan Frumin committed
607 608 609 610 611 612
    iIntros (Φ) "(#Hl & (Hflkd & Haactive & Hfa)) HΦ". rewrite -fupd_wp.
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
    iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl"; last first.
    - iDestruct (own_valid_2 with "Hstate Hflkd")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
      fold_leibniz. inversion Hfoo.
Dan Frumin's avatar
Dan Frumin committed
613
    - iDestruct "Hrest" as ">[Hlocked Htokens]".
Dan Frumin's avatar
Dan Frumin committed
614 615 616 617 618 619
      iDestruct (own_valid_2 with "Haactive Hfactive")
        as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
      fold_leibniz. simplify_eq/=.

      (* Locked ~~> Unlocked *)
      iMod (own_update_2 with "Hstate Hflkd") as "Hstate".
620 621 622
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
623
      iDestruct "Hstate" as "[Hstate Hunflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
624

Dan Frumin's avatar
Dan Frumin committed
625 626 627 628 629
      iMod ("Hcl" with "[Hstate Hauth Haactive Hfactive Hfp]") as "_".
      { iNext. iExists Unlocked,fp,.
        iSplitR; eauto. iFrame. }
      iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
      done.
Dan Frumin's avatar
Dan Frumin committed
630 631
  Qed.

Léon Gondelman's avatar
Léon Gondelman committed
632
End flock.