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.