flock.v 28.7 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
Record PropPerm := {
  prop_perm : frac;
  prop_saved_name : gname;
  prop_perm_name : gname
}.
Canonical Structure PropPermC := leibnizC PropPerm.
32

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
  Lemma to_props_map_singleton_included fp i q ρ:
    {[i := (q, to_agree ρ)]}  to_props_map fp  fp !! i = Some ρ.
69
  Proof.
Dan Frumin's avatar
Dan Frumin committed
70 71 72 73
    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'.
74 75
  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.
79

Dan Frumin's avatar
Dan Frumin committed
80 81
  Lemma from_active_empty : from_active  = .
  Proof. by rewrite /from_active fmap_empty. Qed.
82

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

Dan Frumin's avatar
Dan Frumin committed
86 87 88 89
  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.
Dan Frumin's avatar
Dan Frumin committed
90

Dan Frumin's avatar
Dan Frumin committed
91 92
  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.
Dan Frumin's avatar
Dan Frumin committed
121

Dan Frumin's avatar
Dan Frumin committed
122 123 124
  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.
Dan Frumin's avatar
Dan Frumin committed
125

Dan Frumin's avatar
Dan Frumin committed
126 127
  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.
128
  Proof.
Dan Frumin's avatar
Dan Frumin committed
129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
    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.
146 147
  Qed.

Dan Frumin's avatar
Dan Frumin committed
148 149
  Global Instance flock_res_fractional γ s R : Fractional (flock_res γ s R).
  Proof. intros p q. apply flock_res_op. Qed.
150

Dan Frumin's avatar
Dan Frumin committed
151 152
  Global Instance flock_res_as_fractional γ s R π :
    AsFractional (flock_res γ s R π) (flock_res γ s R) π.
Léon Gondelman's avatar
Léon Gondelman committed
153 154
  Proof. split. done. apply _. Qed.

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 190
  Qed.

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.
261 262 263
  Qed.

  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
  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}
Dan Frumin's avatar
Dan Frumin committed
315
        `{inG Σ (authR (gmapUR A C))} (f : B  C) (m : gmap A B) (γ : gname) :
Dan Frumin's avatar
Dan Frumin committed
316 317
    own γ ( ) -
    own γ ( (f <$> m)) - [ map] ix  m, own γ ( {[ i := f x ]}).
Dan Frumin's avatar
Dan Frumin committed
318
  Proof.
Dan Frumin's avatar
Dan Frumin committed
319
    simple refine (map_ind (λ m, _)%I _ _ m); simpl.
Dan Frumin's avatar
Dan Frumin committed
320
    - iIntros "He". rewrite fmap_empty big_sepM_empty. iSplit; eauto.
Dan Frumin's avatar
Dan Frumin committed
321
    - iIntros (i x m' Hi IH) "He".
Dan Frumin's avatar
Dan Frumin committed
322
      rewrite fmap_insert insert_union_singleton_l.
Dan Frumin's avatar
Dan Frumin committed
323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
      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".
Dan Frumin's avatar
Dan Frumin committed
343
  Qed.
Dan Frumin's avatar
Dan Frumin committed
344

Dan Frumin's avatar
Dan Frumin committed
345
  (* here it is crucial that we use a gmap:
Dan Frumin's avatar
Dan Frumin committed
346 347 348
     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 }}}
Dan Frumin's avatar
Dan Frumin committed
349
      acquire lk
Dan Frumin's avatar
Dan Frumin committed
350 351
    {{{ RET #();
        ( [ map] p  I, p.1)
Dan Frumin's avatar
Dan Frumin committed
352
      (( [ map] p  I, p.1) ={}= flocked γ 
Dan Frumin's avatar
Dan Frumin committed
353
                               [ map] i  p  I, flock_res γ i p.1 p.2) }}}.
Dan Frumin's avatar
Dan Frumin committed
354
  Proof.
Dan Frumin's avatar
Dan Frumin committed
355 356 357 358 359 360
    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
361
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
Dan Frumin's avatar
Dan Frumin committed
362 363 364 365 366 367 368 369
    - 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 *)
Dan Frumin's avatar
Dan Frumin committed
370
      iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
Dan Frumin's avatar
Dan Frumin committed
371
      { apply (auth_update _ _ (Excl' Locked) (Excl' Locked)).
Dan Frumin's avatar
Dan Frumin committed
372 373 374 375
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hflkd]".

Dan Frumin's avatar
Dan Frumin committed
376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397
      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. }
Dan Frumin's avatar
Dan Frumin committed
398

Dan Frumin's avatar
Dan Frumin committed
399 400 401 402 403 404
      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)).
Dan Frumin's avatar
Dan Frumin committed
405 406
        by apply option_local_update, exclusive_local_update. }

Dan Frumin's avatar
Dan Frumin committed
407 408 409 410 411 412 413 414 415
      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 /= //. }
Dan Frumin's avatar
Dan Frumin committed
416

Dan Frumin's avatar
Dan Frumin committed
417 418 419 420 421 422 423 424 425 426 427
      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 *) }
Dan Frumin's avatar
Dan Frumin committed
428

Dan Frumin's avatar
Dan Frumin committed
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
      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)))
Dan Frumin's avatar
Dan Frumin committed
472
                 (λ bc : iProp Σ * Qp * (gname * gname),
Dan Frumin's avatar
Dan Frumin committed
473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489
                   {|
                   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 π }}}
491
      acquire lk
Dan Frumin's avatar
Dan Frumin committed
492
    {{{ RET #();  R  ( R ={}= flocked γ   flock_res γ i R π) }}}.
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.