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

26 27 28
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
29
    flock_lockG  :> lockG Σ;
Dan Frumin's avatar
Dan Frumin committed
30 31 32 33
    flock_savedProp :> savedPropG Σ;
    flock_tokens :> inG Σ fracR;
    flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id (prodC fracC (prodC gnameC gnameC))))));
    flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))
34 35
  }.

Dan Frumin's avatar
Dan Frumin committed
36 37 38 39 40 41 42
Definition flockΣ : gFunctors :=
  #[GFunctor (authR (optionUR (exclR lockstateC)))
   ;lockΣ
   ;savedPropΣ
   ;GFunctor fracR
   ;GFunctor (authR (optionUR (exclR (gmapC prop_id (prodC fracC (prodC gnameC gnameC))))))
   ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))%CF].
43

Dan Frumin's avatar
Dan Frumin committed
44 45
Instance subG_flockΣ Σ : subG flockΣ Σ  flockG Σ.
Proof. solve_inG. Qed.
46

Léon Gondelman's avatar
Léon Gondelman committed
47
Section flock.
48 49
  Context `{heapG Σ, flockG Σ}.

Dan Frumin's avatar
Dan Frumin committed
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
  (* because flock_res_op is admitted, it has to go before the Variable N part *)
  Definition flock_res (γ : flock_name) (R : iProp Σ) (π : Qp) : iProp Σ :=
    ( s ρ, saved_prop_own ρ.1 R  own ρ.2 π
      own (flock_props_name γ) ( {[s := (π, to_agree ρ)]}))%I.

  Lemma flock_res_op (γ : flock_name) (R : iProp Σ) (π1 π2 : frac) :
    flock_res γ R (π1+π2)  flock_res γ R π1  flock_res γ R π2.
  Proof. rewrite /flock_res. admit. Admitted.

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

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

66
  Variable N : namespace.
67 68
  Definition flockN := N.@"flock".

Dan Frumin's avatar
Dan Frumin committed
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
  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.

  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.

  Definition from_active (f : gmap prop_id (frac * (gname * gname)))
    : gmap prop_id (gname * gname) := fmap snd f.

  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
90

Dan Frumin's avatar
Dan Frumin committed
91 92
  Definition all_tokens (f : gmap prop_id (frac * (gname*gname))) : iProp Σ :=
    ([ map] i  ρ  f, own ρ.2.2 ρ.1)%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 97 98 99
    ( (s : lockstate)
       (fp : gmap prop_id (gname * gname))
       (fa : gmap prop_id (frac * (gname * gname))),
       (** 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 118
    (γ : flock_name) (f : gmap prop_id (frac * (gname * gname))) : iProp Σ :=
    (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

122

Dan Frumin's avatar
Dan Frumin committed
123
  Lemma flock_res_single_alloc γ lk R E :
Dan Frumin's avatar
Dan Frumin committed
124
    flockN  E 
Dan Frumin's avatar
Dan Frumin committed
125 126
    is_flock γ lk -  R
    ={E}= flock_res γ R 1.
127
  Proof.
Dan Frumin's avatar
Dan Frumin committed
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142
    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".
    pose (i := (fresh ((dom (gset prop_id) (fp  from_active fa))))).
    assert (i  (dom (gset prop_id) (fp  from_active fa))) as Hs.
    { apply is_fresh. }
    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. }
143
      iDestruct "Hauth" as "[Hauth Hres]".
Dan Frumin's avatar
Dan Frumin committed
144 145 146 147 148 149 150 151 152 153 154
      iExists i, (ρ1,ρ2). iFrame "Hres Hρ1 Hρ2".
      iApply ("Hcl" with "[-]").
      iNext. iExists _,_,_. iFrame. iFrame "Hrest".
      rewrite /all_props big_sepM_insert; last first.
      + apply (not_elem_of_dom _ i (D:=gset prop_id)).
          revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. 
      + iFrame "Hfp". iSplitR; last by eauto.
        iPureIntro. admit. (* TODO: map disjoint *)
  Admitted.

  Lemma flock_res_single_dealloc γ lk R E :
Dan Frumin's avatar
Dan Frumin committed
155
    flockN  E 
Dan Frumin's avatar
Dan Frumin committed
156 157
    is_flock γ lk - flock_res γ R 1
    ={E}=  R',  R'    (R  R').
Dan Frumin's avatar
Dan Frumin committed
158
  Proof.
Dan Frumin's avatar
Dan Frumin committed
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
    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]".
      iDestruct "HR" as (i [ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.      
      iDestruct (own_valid_2 with "Hauth HR")
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.     
      iAssert (fa !! i = None)%I with "[-]" as %Hbar.
      { remember (fa !! i) as fai. destruct fai as [[π [ρ'1 ρ'2]]|]; last done.
        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.
          rewrite frac_op' in Hbaz2. exfalso. apply Hbaz2. admit. (* TODO: Qp *) }
      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.
        iSplit. admit. (* TODO: map_disjoint *)
        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.
      iDestruct "HR" as (i [ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.
      iDestruct (own_valid_2 with "Hauth HR")
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.    
      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.
  Admitted.
223 224

  Lemma newlock_cancel_spec :
Dan Frumin's avatar
Dan Frumin committed
225
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
226 227
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
228 229
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
230 231 232 233 234 235 236
    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").
237
    iNext. iIntros (lk γ_lock) "#Hlock".
Dan Frumin's avatar
Dan Frumin committed
238 239 240 241 242
    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 "[-]").
243 244
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
245

Dan Frumin's avatar
Dan Frumin committed
246
  Lemma acquire_cancel_spec γ π lk R :
Dan Frumin's avatar
Dan Frumin committed
247
    {{{ is_flock γ lk  flock_res γ R π }}}
Dan Frumin's avatar
Dan Frumin committed
248
      acquire lk
Dan Frumin's avatar
Dan Frumin committed
249
    {{{ RET #();  R', R'   (R  R')  ( R' ={}= flocked γ   flock_res γ R π) }}}.
Dan Frumin's avatar
Dan Frumin committed
250
  Proof.
Dan Frumin's avatar
Dan Frumin committed
251 252 253 254 255 256
    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
257
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
Dan Frumin's avatar
Dan Frumin committed
258 259 260 261 262 263 264 265 266
    - 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.
      iDestruct "HRres" as (i [ρ1 ρ2]) "(#Hρ1 & Hρ2 & HR)". simpl.

      (* Unlocked ~~> Locked *)
Dan Frumin's avatar
Dan Frumin committed
267
      iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
Dan Frumin's avatar
Dan Frumin committed
268
      { apply (auth_update _ _ (Excl' Locked) (Excl' Locked)).
Dan Frumin's avatar
Dan Frumin committed
269 270 271
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
272

Dan Frumin's avatar
Dan Frumin committed
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 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
      (* (i,ρ) ∈ fp *)
      iDestruct (own_valid_2 with "Hauth HR")
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.    

      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".
      
      (* move (i,ρ) to the set of active propositions *)
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
      { apply (auth_update _ _ (Excl' {[ i := (π, (ρ1, ρ2)) ]})
                               (Excl' {[ i := (π, (ρ1, ρ2)) ]})).
        apply option_local_update.
        by apply exclusive_local_update. }
      
      iMod ("Hcl" with "[-HΦ HR' Hfoo Haactive Hflkd HR]") as "_".
      { iNext. iExists Locked,(delete i fp),{[i := (π, (ρ1, ρ2))]}.
        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Φ".
      iNext. iExists R'. iFrame "HR' Hfoo". iIntros "HR'".
      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]".
        
        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. }
        
        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.
            iRewrite "Hfoo" in "Hρ1". by iFrame. }
        iModIntro. iFrame. rewrite /all_props from_active_empty big_sepM_empty.
        iSplitR; first done.
        rewrite /all_tokens big_sepM_singleton. simpl.
        iExists i, (ρ1, ρ2). by iFrame.
  Admitted.

  Lemma release_cancel_spec γ lk :
    {{{ is_flock γ lk  flocked γ  }}}
354
      release lk
Dan Frumin's avatar
Dan Frumin committed
355
    {{{ RET #(); True }}}.
356
  Proof.
Dan Frumin's avatar
Dan Frumin committed
357 358 359 360 361 362 363 364 365 366 367 368 369
    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.
    - iDestruct "Hrest" as ">[Hlocked Htokens]".        
      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".
370 371 372
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
373
      iDestruct "Hstate" as "[Hstate Hunflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
374

Dan Frumin's avatar
Dan Frumin committed
375 376 377 378 379
      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
380 381
  Qed.

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