flock.v 36 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
From iris.heap_lang Require Import spin_lock.
3
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
Dan Frumin's avatar
Dan Frumin committed
4
From iris.algebra Require Import auth agree excl frac gmap gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris.bi.lib Require Import fractional.
Léon Gondelman's avatar
Léon Gondelman committed
6

7
Inductive lockstate :=
Dan Frumin's avatar
Dan Frumin committed
8
  | Locked
9
10
11
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

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

Dan Frumin's avatar
Dan Frumin committed
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
(** We need to be able to allocate resources into the lock even when
    it is in use -- for that we need to have /active/ and /pending/
    propositions. If the lock is unlocked (not acquired), then all the
    propositions are active (can be acquired); if the lock is locked
    (acquired), then some thread has the ownership of the active
    propositions, but any other thread can add a pending proposition.
    Pending propositions are thus always held by the lock.

    When a thread acquires the lock, it gets all the active
    propositions. For the whole construction to make sense, the thread
    should return exactly the same propositions once it releases the
    lock. For this to work we need to ensure that the set of active
    proposition has not changed since the lock has been acquired.
    Thus, we use ghost state to track the exact content of the set of
    active propositions.

    If we have a full access to the resource (with fraction 1), we may
    want to cancel it and get the proposition back. In order to do
    that we need to make sure that if we have the full fraction for
    accessing the resource, then this resource cannot be active. For
    that purpose we also need to store the information about the
    fractional permissions for the active propositions.

    Finally, the actual propositional content of the resources is
    shared via cancellable invariants. Each proposition (active or
    pending) is stored in a cancellable invariant associated with it:
Dan Frumin's avatar
Dan Frumin committed
40

Dan Frumin's avatar
Dan Frumin committed
41
42
43
44
45
        C(X) = X.prop ∗ X.token₁ ∨ X.token₂

    The exclusive tokens allow the thread to take out the proposition
    for the whole duration of the critical section. *)

46
Record flock_name := {
Dan Frumin's avatar
Dan Frumin committed
47
  (** ghost name for the actual spin lock invariant *)
Dan Frumin's avatar
Dan Frumin committed
48
  flock_lock_name : gname;
Dan Frumin's avatar
Dan Frumin committed
49
  (** -//- for keeping the track of the state of the flock *)
50
  flock_state_name : gname;
Dan Frumin's avatar
Dan Frumin committed
51
  (** -//- for keeping track of all propositions in the flock *)
52
  flock_props_name : gname;
53
54
  (** -//- for keeping track of the "active" propositions.
      Once you relase the lock you need to know that the set of the active propositions
Dan Frumin's avatar
Dan Frumin committed
55
      has not changed since you have acquired it *)
56
  flock_props_active_name : gname
57
58
}.

59
60
61
(** The data about pending and active propositions will be stored in
the maps `prop_id -> _` *)
(* `prop_id` is fefined as `positive` so that we have a `Fresh` instance for `gset positive`.
Dan Frumin's avatar
Dan Frumin committed
62
   Doubles as an invariant name. *)
63
Definition prop_id := positive.
Dan Frumin's avatar
Dan Frumin committed
64
Canonical Structure gnameC := leibnizC gname.
65

66
67
68
69
(** One of the tricks in this lock is to store only ghost names associated with a 'flock resource' in the flock invariant.
    If we start storing propositions, then we end up in the LATER HELL.
    The `lock_res_name` datastructure contains all the ghosts names needed to manage an individual proposition.
 *)
Dan Frumin's avatar
Dan Frumin committed
70
71
72
73
Record lock_res_name := {
  flock_cinv_name : gname;
  flock_token1_name : gname;
  flock_token2_name : gname;
Dan Frumin's avatar
Dan Frumin committed
74
}.
Dan Frumin's avatar
Dan Frumin committed
75
Canonical Structure lock_res_nameC := leibnizC lock_res_name.
76

77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92

(** Before we define the type of flock resources, we need to have
    access to the appropriate CMRAs.

   The totality of propositions , and the pending propositions will be
   represented as a map:

   `prop_id → frac * ag (flock_res_name)`,

   so a standart ghost heap. Active propositions will be modelled by a map

   `excl (prop_id → frac * ag (flock_res_name))`.

   In other words, this map will contain *exact* information of which propositions are active and with what fractions were they activated.

 *)
93
94
95
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
96
    flock_lockG  :> lockG Σ;
Dan Frumin's avatar
Dan Frumin committed
97
98
99
100
101
    flock_cinvG  :> cinvG Σ;
    (* note the difference between the two RAs here ! *)
    flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id (prodC fracC lock_res_nameC)))));
    flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR lock_res_nameC))));
    flock_tokens :> inG Σ (exclR unitC);
102
103
  }.

104
105
106
107
108
109
110
111
112
113
Definition flockΣ : gFunctors :=
  #[GFunctor (authR (optionUR (exclR lockstateC)))
   ;lockΣ
   ;cinvΣ
   ;GFunctor (authR (optionUR (exclR (gmapC prop_id (prodC fracC lock_res_nameC)))))
   ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR lock_res_nameC))))%CF].

Instance subG_flockΣ Σ : subG flockΣ Σ  flockG Σ.
Proof. solve_inG. Qed.

Dan Frumin's avatar
Dan Frumin committed
114
115
116
117
118
119
Record lock_res `{flockG Σ} := {
  res_prop : iProp Σ;
  res_frac : frac;
  res_name : lock_res_name;
}.

120
(** A "smart constructor" for `lock_res` *)
Dan Frumin's avatar
Dan Frumin committed
121
122
Definition LockRes `{flockG Σ} (R : iProp Σ) (π : frac) (ρ : lock_res_name) :=
  {| res_prop := R; res_frac := π; res_name := ρ |}.
123

Léon Gondelman's avatar
Léon Gondelman committed
124
Section flock.
125
126
  Context `{heapG Σ, flockG Σ}.
  Variable N : namespace.
Dan Frumin's avatar
Dan Frumin committed
127
128
129
130
131
132
133
134
135
136
137
138
139
  Definition invN := N.@"flock_inv".
  Definition lockN := N.@"flock_lock".
  Definition resN := N.@"flock_res".

  (** * Definitions **)
  Definition token (ρ : lock_res_name) : iProp Σ :=
    own (flock_token1_name ρ) (Excl ()).
  Definition token (ρ : lock_res_name) : iProp Σ :=
    own (flock_token2_name ρ) (Excl ()).

  Definition C (R : iProp Σ) (ρ : lock_res_name) : iProp Σ :=
    (R  token ρ  token ρ)%I.

140
  (** Tokens that allow you to get all the propositions from `A` out of the invariants *)
Dan Frumin's avatar
Dan Frumin committed
141
142
  Definition all_tokens (P : gmap prop_id lock_res_name) : iProp Σ :=
    ([ map] i  X  P, token X)%I.
Dan Frumin's avatar
Dan Frumin committed
143

Dan Frumin's avatar
Dan Frumin committed
144
145
146
  (** For active propositions we also need to know the fraction which was used to access it *)
  Definition from_active (A : gmap prop_id (frac * lock_res_name))
    := fmap snd A.
Dan Frumin's avatar
Dan Frumin committed
147

148
149
150
151
152
153

  (** A flock resource `s ↦ X,π,γ` contains:
      - Knowledge that the `s ↦{π} γ` is in the set of propositions managed by the flock;
      - There is a cancellable invariant `C X γ`;
      - We have π- permissiones to access that invariant.
   *)
Dan Frumin's avatar
Dan Frumin committed
154
155
156
157
  Definition flock_res (γ : flock_name) (s : prop_id) (X : lock_res) : iProp Σ :=
    (own (flock_props_name γ) ( {[s := (res_frac X, to_agree (res_name X))]})
     cinv (resN.@s) (flock_cinv_name (res_name X)) (C (res_prop X) (res_name X))
     cinv_own (flock_cinv_name (res_name X)) (res_frac X))%I.
158

159
160
161
162
163
  (** Basically says that the propositions from the map `A` are active.
      This predicate is designed to contain enough information to deactivate those propositions.

      When we are deactivating the propositions we need to make sure that the set of the active propositions has not changed. That's why we need a CMRA to keep track of the exact contents of that set.
 *)
Dan Frumin's avatar
Dan Frumin committed
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
  Definition flocked
    (γ : flock_name) (A : gmap prop_id lock_res) : iProp Σ :=
    ( fa : gmap prop_id (frac * lock_res_name),
         fa = fmap (λ X, (res_frac X, res_name X)) A
       (* Information we retain: the flock is locked .. *)
        own (flock_state_name γ) ( (Excl' Locked))
       (* What are the exact propositions that we have activated.. *)
        own (flock_props_active_name γ) ( (Excl' fa))
       (* Tokens and permissions for closing the active propositions .. *)
        ([ map] i  X  A, token (res_name X)
                   cinv (resN.@i) (flock_cinv_name (res_name X)) (C (res_prop X) (res_name X))
                   cinv_own (flock_cinv_name (res_name X)) (res_frac X)))%I.

  Definition to_props_map (f : gmap prop_id lock_res_name)
    : gmapUR prop_id (prodR fracR (agreeR lock_res_nameC)) :=
    fmap (λ X, (1%Qp, to_agree X)) f.
Dan Frumin's avatar
Dan Frumin committed
180

181
  (** TODO: can we actually get rid of the `to_props_map` here? *)
Dan Frumin's avatar
Dan Frumin committed
182
  Definition flock_inv (γ : flock_name) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
183
184
    ( (s : lockstate)
       (** fa -- active propositions, fp -- pending propositions *)
Dan Frumin's avatar
Dan Frumin committed
185
186
       (fa : gmap prop_id (frac * lock_res_name))
       (fp : gmap prop_id lock_res_name),
187
       (** ... and those sets are disjoint *)
Dan Frumin's avatar
Dan Frumin committed
188
       fp ## from_active fa 
Dan Frumin's avatar
Dan Frumin committed
189
       own (flock_state_name γ) ( (Excl' s)) 
190
       (** the totality of resources: fp ∪ fa *)
Dan Frumin's avatar
Dan Frumin committed
191
       own (flock_props_name γ) ( to_props_map (fp  from_active fa)) 
192
       (** but we also need to know the exact contents of fa *)
Dan Frumin's avatar
Dan Frumin committed
193
       own (flock_props_active_name γ) ( Excl' fa) 
194
195
196
197
       (** the invariant keeps track of the tokens (token₂) for the
           pending resource; when we activate a resource, we transfer
           this token to the client, which uses it to open the
           cinvariant and get the actual proposition. *)
Dan Frumin's avatar
Dan Frumin committed
198
       all_tokens fp 
Dan Frumin's avatar
Dan Frumin committed
199
       match s with
Dan Frumin's avatar
Dan Frumin committed
200
       | Locked =>
201
         (** If the lock is acuired, then we hold on to the token from the "old" specification *)
Dan Frumin's avatar
Dan Frumin committed
202
         locked (flock_lock_name γ) 
203
204
205
206
207
208
209
         (** .. and we take hold of all the ghost pointsto `s ↦{π} ρ`.

             This is necessary to have if we want to free the
             resources. If we wish to free the resource `s ↦{1} ρ`,
             then we need to know that it is not currently active (has
             not been acquired). The predicate below ensures that. *)
         ([ map] i  πρ  fa, own (flock_props_name γ) ( {[i:=(πρ.1,to_agree πρ.2)]}))
Dan Frumin's avatar
Dan Frumin committed
210
       | Unlocked =>
211
212
         (** If the lock is NOT acquired, then there are no active
         proposition *)
Dan Frumin's avatar
Dan Frumin committed
213
         own (flock_props_active_name γ) ( Excl' )
Dan Frumin's avatar
Dan Frumin committed
214
215
216
       end)%I.

  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
217
218
    (inv invN (flock_inv γ) 
     is_lock lockN (flock_lock_name γ) lk
Dan Frumin's avatar
Dan Frumin committed
219
220
         (own (flock_state_name γ) ( (Excl' Unlocked))))%I.

Dan Frumin's avatar
Dan Frumin committed
221
222
223
  (** * Lemmata **)

  (** ** Basic properties of the CAPs *)
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
  (* TODO, we only have this for the "smart constructor" *)
  Lemma flock_res_agree (γ : flock_name) (s : prop_id) (R1 R2 : iProp Σ) ρ1 ρ2 (π1 π2 : frac) :
    flock_res γ s (LockRes R1 π1 ρ1) -
    flock_res γ s (LockRes R2 π2 ρ2) ==
    ⌜ρ1 = ρ2.
  Proof.
    rewrite /flock_res.
    iDestruct 1 as "(Hs1 & #Hinv1 & Hρ1)".
    iDestruct 1 as "(Hs2 & #Hinv2 & Hρ2)".
    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']. eauto.
  Qed.

  Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) ρ (π1 π2 : frac) :
    flock_res γ s (LockRes R (π1+π2) ρ)
  flock_res γ s (LockRes R π1 ρ)  flock_res γ s (LockRes R π2 ρ).
  Proof.
    rewrite /flock_res. iSplit.
    - iDestruct 1 as "(Hs & #Hinv & Hρ)".
      iDestruct "Hρ" as "[Hρ1 Hρ2]".
      iDestruct "Hs" as "[Hs1 Hs2]".
      iSplitL "Hρ1 Hs1"; by iFrame.
    - iIntros "[H1 H2]".
      iDestruct "H1" as "(Hs1 & #Hinv1 & Hρ1)".
      iDestruct "H2" as "(Hs2 & #Hinv2 & Hρ2)".
      iCombine "Hs1 Hs2" as "Hs". iFrame.
      rewrite /C /=. iFrame "Hinv1".
  Qed.

  Global Instance flock_res_fractional γ s R ρ :
    Fractional (λ π, flock_res γ s (LockRes R π ρ)).
  Proof. intros p q. apply flock_res_op. Qed.

  Global Instance flock_res_as_fractional γ s R π ρ :
    AsFractional (flock_res γ s (LockRes R π ρ))
                 (λ π, flock_res γ s (LockRes R π ρ)) π.
  Proof. split. done. apply _. Qed.
Dan Frumin's avatar
Dan Frumin committed
264

Dan Frumin's avatar
Dan Frumin committed
265
266
  Lemma to_props_map_singleton_included fp i q ρ:
    {[i := (q, to_agree ρ)]}  to_props_map fp  fp !! i = Some ρ.
267
  Proof.
Dan Frumin's avatar
Dan Frumin committed
268
269
270
    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 -> //.
271
272
  Qed.

Dan Frumin's avatar
Dan Frumin committed
273
274
275
  Lemma to_props_map_delete fp i:
    delete i (to_props_map fp) = to_props_map (delete i fp).
  Proof.
Dan Frumin's avatar
Dan Frumin committed
276
    by rewrite /to_props_map fmap_delete.
Dan Frumin's avatar
Dan Frumin committed
277
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
278

Dan Frumin's avatar
Dan Frumin committed
279
280
281
282
283
  (** ** Spectral and physical operations *)
  Lemma flock_res_alloc_strong (X : gset prop_id) γ lk R E :
    N  E 
    is_flock γ lk -
     R ={E}=  s ρ, s  X  flock_res γ s (LockRes R 1 ρ).
284
  Proof.
Dan Frumin's avatar
Dan Frumin committed
285
286
287
288
289
290
    iIntros (?) "Hl HR". rewrite /is_flock.
    iDestruct "Hl" as "(#Hfl & #Hlk)".

    (* Pick a fresh name *)
    iInv invN as (s fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
Dan Frumin's avatar
Dan Frumin committed
291
292
    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
293
    { apply is_fresh. }
Dan Frumin's avatar
Dan Frumin committed
294
    apply not_elem_of_union in Hs. destruct Hs as [Hi1 Hi2].
Dan Frumin's avatar
Dan Frumin committed
295
296
297
298
299
300
301
302
303
304

    (* Alloc all the data for the resource *)
    iMod (own_alloc (Excl ())) as (γt) "T1"; first done.
    iMod (own_alloc (Excl ())) as (γt) "T2"; first done.
    iMod (cinv_alloc _ (resN.@i) (R  own γt (Excl ())  own γt (Excl ()))%I with "[HR T1]") as (γc) "[#HR Hρ]".
    { iNext. iLeft. by iFrame. }
    pose (ρ :=
            {| flock_cinv_name := γc;
               flock_token1_name := γt;
               flock_token2_name := γt |}).
Dan Frumin's avatar
Dan Frumin committed
305

Dan Frumin's avatar
Dan Frumin committed
306
307
308
309
    (* Put it in the map of flock resources *)
    iMod (own_update  with "Haprops") as "Haprops".
    { apply (auth_update_alloc _ (to_props_map (<[i := ρ]> fp  from_active fa))
                               {[ i := (1%Qp, to_agree ρ) ]}).
Dan Frumin's avatar
Dan Frumin committed
310
311
312
313
314
      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. }
Dan Frumin's avatar
Dan Frumin committed
315
316
317
318
319
320
321
322
323
    iDestruct "Haprops" as "[Haprops Hi]".
    iMod ("Hcl" with "[-Hi Hρ]") as "_".
    { iNext. iExists s, fa,(<[i:=ρ]>fp).
      iFrame. rewrite /all_tokens 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. iPureIntro.
      apply map_disjoint_insert_l_2; eauto.
Dan Frumin's avatar
Dan Frumin committed
324
      eapply (not_elem_of_dom (D:=gset prop_id)).
Dan Frumin's avatar
Dan Frumin committed
325
326
327
328
      intros Hi; apply Hi1. rewrite dom_union_L elem_of_union. eauto.
    }
    iModIntro; iExists i, ρ; iSplit; eauto.
    by iFrame.
Dan Frumin's avatar
Dan Frumin committed
329
330
  Qed.

Dan Frumin's avatar
Dan Frumin committed
331
332
333
334
335
  Lemma flock_res_dealloc γ lk i X E :
    N  E 
    res_frac X = 1%Qp 
    is_flock γ lk -
    flock_res γ i X ={E}=  (res_prop X).
Dan Frumin's avatar
Dan Frumin committed
336
  Proof.
Dan Frumin's avatar
Dan Frumin committed
337
338
339
340
341
342
343
344
345
346
347
    iIntros (? HX) "Hl HR". rewrite /is_flock.
    iDestruct "Hl" as "(#Hfl & #Hlk)".
    destruct X as [R ? ρ]. simpl in HX. rewrite HX; clear HX.
    iDestruct "HR" as "(Hi & #Hiinv & Hρ)".

    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
    (* Locked *)
    - iDestruct "Hst" as ">[Hlocked Hactives]".
      (* We can now show that the proposition `i` is *not* active *)
      iDestruct (own_valid_2 with "Haprops Hi")
Dan Frumin's avatar
Dan Frumin committed
348
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
349
      iAssert (fa !! i = None)%I with "[-]" as %Hbar.
Dan Frumin's avatar
Dan Frumin committed
350
351
352
      { remember (fa !! i) as fai. destruct fai as [[π ρ']|]; last done.
        symmetry in Heqfai.
        rewrite (big_sepM_lookup _ fa i (π, ρ')) //.
Dan Frumin's avatar
Dan Frumin committed
353
        (* TODO: RK, please look at this! *)
Dan Frumin's avatar
Dan Frumin committed
354
        iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz.
Dan Frumin's avatar
Dan Frumin committed
355
356
357
358
359
        exfalso. revert Hbaz.
        rewrite -auth_frag_op /=. intros Hbaz%auth_own_valid.
        revert Hbaz. simpl. rewrite op_singleton pair_op /=.
        rewrite singleton_valid. intros [Hlol _]. simpl in *.
        eapply exclusive_l ; eauto. apply _. }
Dan Frumin's avatar
Dan Frumin committed
360
      assert (fp !! i = Some ρ) as Hbaz.
Dan Frumin's avatar
Dan Frumin committed
361
362
      { apply lookup_union_Some in Hfoo; last done.
        destruct Hfoo as [? | Hfoo]; first done.
Dan Frumin's avatar
Dan Frumin committed
363
        exfalso. revert Hfoo. by rewrite /from_active lookup_fmap Hbar.
Dan Frumin's avatar
Dan Frumin committed
364
365
      }

Dan Frumin's avatar
Dan Frumin committed
366
      iMod (own_update_2 with "Haprops Hi") as "Haprops".
Dan Frumin's avatar
Dan Frumin committed
367
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
Dan Frumin's avatar
Dan Frumin committed
368
369
370
371
372
373
      rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
      iDestruct "Htokens" as "[T2 Htokens]".
      iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
      rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
      { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
      iFrame "HR".
Dan Frumin's avatar
Dan Frumin committed
374

Dan Frumin's avatar
Dan Frumin committed
375
376
377
378
      (* Now that the resource is cancelled we close the flock invariant *)
      iApply "Hcl". iNext.
      iExists Locked,fa,(delete i fp). iFrame.
      iSplit.
379
      + iPureIntro. solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
380
381
382
383
384
      + rewrite to_props_map_delete delete_union.
        rewrite (delete_notin (from_active fa)) //.
        rewrite /from_active lookup_fmap Hbar //.
    (* Unlocked *)
    - iDestruct "Hst" as ">Hfactive".
Dan Frumin's avatar
Dan Frumin committed
385
386
387
388
      iAssert (fa = ∅⌝)%I with "[-]" as %->.
      { iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        iPureIntro. by unfold_leibniz. }
Dan Frumin's avatar
Dan Frumin committed
389
390
      rewrite /from_active fmap_empty /= right_id.
      iDestruct (own_valid_2 with "Haprops Hi")
Dan Frumin's avatar
Dan Frumin committed
391
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
392
      iMod (own_update_2 with "Haprops Hi") as "Haprops".
Dan Frumin's avatar
Dan Frumin committed
393
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
Dan Frumin's avatar
Dan Frumin committed
394
395
396
397
398
399
400
401
402
403
404
      rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
      iDestruct "Htokens" as "[T2 Htokens]".
      iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
      rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
      { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
      iFrame "HR".

      (* Now that the resource is cancelled we close the flock invariant *)
      iApply "Hcl". iNext.
      iExists Unlocked,,(delete i fp). iFrame.
      iSplit.
405
      + iPureIntro. solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
406
407
      + rewrite /from_active fmap_empty /= right_id.
        by rewrite to_props_map_delete.
Dan Frumin's avatar
Dan Frumin committed
408
  Qed.
409

Dan Frumin's avatar
Dan Frumin committed
410
  Lemma newflock_spec :
Dan Frumin's avatar
Dan Frumin committed
411
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
412
413
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
414
415
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
416
417
418
419
420
421
    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. }
Dan Frumin's avatar
Dan Frumin committed
422
    iApply (newlock_spec lockN (own γ_state ( (Excl' Unlocked))) with "Hfrag").
423
    iNext. iIntros (lk γ_lock) "#Hlock".
Dan Frumin's avatar
Dan Frumin committed
424
    pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
Dan Frumin's avatar
Dan Frumin committed
425
426
427
    iMod (inv_alloc invN _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
    { iNext. iExists Unlocked, , . rewrite /from_active fmap_empty right_id. iFrame.
      iSplit; eauto. by rewrite /all_tokens big_sepM_empty. }
Dan Frumin's avatar
Dan Frumin committed
428
    iModIntro. iApply ("HΦ" $! lk γ with "[-]").
429
430
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
431

Dan Frumin's avatar
Dan Frumin committed
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
  (** `flocked` supports invariant access just like regular invariants *)
  Lemma flocked_inv_open E i X γ I :
    resN  E 
    I !! i = Some X 
    flocked γ I ={E}=
     (res_prop X)  ( (res_prop X) ={E}= flocked γ I).
  Proof.
    iIntros (? Hi). rewrite {1}/flocked.
    iDestruct 1 as (fa ?) "(Hst & Hfa & Htokens)".
    rewrite (big_sepM_lookup_acc _ I i X) //.
    iDestruct "Htokens" as "[(T2 & #Hinv & Hρ) Htokens]".
    iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
    rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
    { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
    iMod ("Hcl" with "[T2]") as "_".
    { iNext. iRight. done. }
    iModIntro. iFrame "HR". iIntros "HR".
    iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
    iDestruct "HC" as "[[? >T1'] | >T2]".
    { iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
    iMod ("Hcl" with "[T1 HR]") as "_".
    { iNext. iLeft. iFrame. }
    iModIntro. rewrite /flocked. iExists fa.
    iFrame "Hst Hfa". iSplit; first eauto.
    iApply "Htokens". by iFrame.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
459
460
  Lemma acquire_flock_single_spec γ lk i X :
    {{{ is_flock γ lk  flock_res γ i X }}}
461
      acquire lk
Dan Frumin's avatar
Dan Frumin committed
462
    {{{ RET #();  (res_prop X)  ( (res_prop X) ={}= flocked γ {[i:=X]}) }}}.
463
  Proof.
Dan Frumin's avatar
Dan Frumin committed
464
    destruct X as [R π ρ].
Dan Frumin's avatar
Dan Frumin committed
465
    iIntros (Φ) "(Hl & HRres) HΦ".
Dan Frumin's avatar
Dan Frumin committed
466
467
    rewrite /is_flock. iDestruct "Hl" as "(#Hfl & #Hlk)".
    iApply wp_fupd.
Dan Frumin's avatar
Dan Frumin committed
468
469
    iApply (acquire_spec with "Hlk").
    iNext. iIntros "[Hlocked Hunlk]".
Dan Frumin's avatar
Dan Frumin committed
470
    iInv invN as ([|] fa fp)
Dan Frumin's avatar
Dan Frumin committed
471
472
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
    - iDestruct "Hst" as "(>Hlocked2 & ?)".
Dan Frumin's avatar
Dan Frumin committed
473
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
Dan Frumin's avatar
Dan Frumin committed
474
    - iDestruct "Hst" as ">Hfactive".
Dan Frumin's avatar
Dan Frumin committed
475
476
477
478
      iAssert (fa = ∅⌝)%I with "[-]" as %->.
      { iDestruct (own_valid_2 with "Haactive Hfactive")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
        iPureIntro. by unfold_leibniz. }
Dan Frumin's avatar
Dan Frumin committed
479
480
      rewrite /from_active fmap_empty /= right_id.
      iDestruct "HRres" as "(Hi & #Hinv & Hρ)".
Dan Frumin's avatar
Dan Frumin committed
481
482

      (* Unlocked ~~> Locked *)
Dan Frumin's avatar
Dan Frumin committed
483
      iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
Dan Frumin's avatar
Dan Frumin committed
484
      { apply (auth_update _ _ (Excl' Locked) (Excl' Locked)).
Dan Frumin's avatar
Dan Frumin committed
485
486
487
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
488

Dan Frumin's avatar
Dan Frumin committed
489
      (* (i,ρ) ∈ fp *)
Dan Frumin's avatar
Dan Frumin committed
490
      iDestruct (own_valid_2 with "Haprops Hi")
Dan Frumin's avatar
Dan Frumin committed
491
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
492
493

      (* move (i,ρ) to the set of active propositions *)
Dan Frumin's avatar
Dan Frumin committed
494
495
      rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
      iDestruct "Htokens" as "[T2 Htokens]".
Dan Frumin's avatar
Dan Frumin committed
496

Dan Frumin's avatar
Dan Frumin committed
497
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
Dan Frumin's avatar
Dan Frumin committed
498
499
      { apply (auth_update _ _ (Excl' {[ i := (π, ρ) ]})
                               (Excl' {[ i := (π, ρ) ]})).
Dan Frumin's avatar
Dan Frumin committed
500
        by apply option_local_update, exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
501

Dan Frumin's avatar
Dan Frumin committed
502
503
504
      iMod ("Hcl" with "[Haactive Hi Hlocked Haprops Htokens Hstate]") as "_".
      { iNext. iExists Locked,{[i := (π, ρ)]},(delete i fp).
        iFrame. iSplitR ; [ | iSplitL "Haprops"].
Dan Frumin's avatar
Dan Frumin committed
505
506
        - iPureIntro.
          rewrite /from_active map_fmap_singleton /=.
Dan Frumin's avatar
Dan Frumin committed
507
          apply map_disjoint_singleton_r, lookup_delete.
Dan Frumin's avatar
Dan Frumin committed
508
        - rewrite /from_active map_fmap_singleton /=.
Dan Frumin's avatar
Dan Frumin committed
509
510
511
          rewrite -insert_union_singleton_r.
          2: { apply lookup_delete. }
          rewrite insert_delete insert_id //.
Dan Frumin's avatar
Dan Frumin committed
512
        - rewrite /all_tokens big_sepM_singleton //. }
Dan Frumin's avatar
Dan Frumin committed
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
      iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first done.
      rewrite /C /=. iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
      { iDestruct (own_valid_2 with "T2 T2'") as %?. done. }
      iMod ("Hcl" with "[T2]") as "_".
      { iNext. iRight. done. }
      iModIntro.
      iApply "HΦ". iFrame "HR". iIntros "HR".
      rewrite /flocked. iExists ({[i:=(π,ρ)]}).
      iFrame "Hflkd Hfactive".
      rewrite big_sepM_singleton /=.
      iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first done.
      iDestruct "HC" as "[[? >T1'] | >T2]".
      { iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
      iFrame "T2 Hρ Hinv".
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iLeft. iFrame. }
      iModIntro. iPureIntro. rewrite map_fmap_singleton //.
Dan Frumin's avatar
Dan Frumin committed
530
  Qed.
Dan Frumin's avatar
Dan Frumin committed
531

Dan Frumin's avatar
Dan Frumin committed
532
533
  Lemma release_cancel_spec γ lk i X :
    {{{ is_flock γ lk  flocked γ {[i:=X]} }}}
534
      release lk
Dan Frumin's avatar
Dan Frumin committed
535
    {{{ RET #(); flock_res γ i X }}}.
536
  Proof.
Dan Frumin's avatar
Dan Frumin committed
537
    iIntros (Φ) "(#Hl & H) HΦ". rewrite -fupd_wp.
Dan Frumin's avatar
Dan Frumin committed
538
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
Dan Frumin's avatar
Dan Frumin committed
539
540
541
542
543
544

    destruct X as [R π ρ]. rewrite /flocked /=.
    iDestruct "H" as (fa' Hfa) "(Hflkd & Hfactive & Hfa)".
    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl";
      last first.
Dan Frumin's avatar
Dan Frumin committed
545
546
547
    - 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
548
    - iDestruct "Hst" as ">[Hlocked Hactives]".
Dan Frumin's avatar
Dan Frumin committed
549
550
551
552
553
554
      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".
555
556
557
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
558
      iDestruct "Hstate" as "[Hstate Hunflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
559

Dan Frumin's avatar
Dan Frumin committed
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
      rewrite !map_fmap_singleton /=.
      rewrite !big_sepM_singleton /=.

      (* Empty up the set of active propositions *)
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
      { apply (auth_update _ _ (Excl' )
                               (Excl' )).
        by apply option_local_update, exclusive_local_update. }

      iDestruct "Hfa" as "(T2 & #Hiinv & Hρ)".

      iMod ("Hcl" with "[-HΦ Hlocked Hactives Hunflkd Hρ]") as "_".
      { iNext. iExists Unlocked,,(<[i:=ρ]>fp).
        iSplitR; eauto.
        - rewrite /from_active fmap_empty. iPureIntro.
575
          solve_map_disjoint.
Dan Frumin's avatar
Dan Frumin committed
576
577
        - iFrame. rewrite /from_active fmap_empty right_id /=.
          rewrite map_fmap_singleton.
Dan Frumin's avatar
Dan Frumin committed
578
579
580
581
          assert (fp !! i = None).
          { eapply map_disjoint_Some_r; first eassumption.
            rewrite /from_active !map_fmap_singleton.
            by rewrite lookup_singleton. }
Dan Frumin's avatar
Dan Frumin committed
582
583
584
585
          rewrite -insert_union_singleton_r // /=. iFrame.
          rewrite /all_tokens big_sepM_insert //.
          iFrame.
      }
Dan Frumin's avatar
Dan Frumin committed
586
      iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
Dan Frumin's avatar
Dan Frumin committed
587
588
      iModIntro. iNext. iIntros "_". iApply "HΦ".
      by iFrame.
Dan Frumin's avatar
Dan Frumin committed
589
  Qed.
Dan Frumin's avatar
Dan Frumin committed
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611

  (** LULZ *)

  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' //.
Dan Frumin's avatar
Dan Frumin committed
612
613
  Qed.

Dan Frumin's avatar
Dan Frumin committed
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
  Lemma big_sepM_own_frag {A B : Type} {C} `{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.
Dan Frumin's avatar
Dan Frumin committed
644

Dan Frumin's avatar
Dan Frumin committed
645
646
647
648
649
650
651
652
653
  Lemma own_frag_empty γ X :
    own (flock_props_name γ) ( X) ==
    own (flock_props_name γ) ( X)  own (flock_props_name γ) ( ).
  Proof.
    iIntros "H". rewrite -own_op.
    iApply (own_update with "H").
    by apply auth_update_alloc.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
654
655
656
  Lemma acquire_flock_spec γ lk (I : gmap prop_id lock_res) :
    {{{ is_flock γ lk  [ map] i  X  I, flock_res γ i X }}}
      acquire lk
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
    {{{ RET #(); flocked γ I }}}.
  Proof.
    iIntros (Φ) "(Hl & HRres) HΦ".
    rewrite /is_flock. iDestruct "Hl" as "(#Hfl & #Hlk)".
    iApply wp_fupd.
    iApply (acquire_spec with "Hlk").
    iNext. iIntros "[Hlocked Hunlk]".
    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
    - iDestruct "Hst" as "(>Hlocked2 & ?)".
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
    - iDestruct "Hst" as ">Hfactive".
      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 fmap_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]".

      iApply "HΦ". rewrite /flocked.
      iFrame "Hflkd".

      (* Designate the propositions from I as active *)
      pose (fa := fmap (λ X, (res_frac X, res_name X)) I).
      iExists fa.
      iAssert (fa = (λ X, (res_frac X, res_name X)) <$> I)%I as "$".
      { eauto. }

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

      rewrite /flock_res. rewrite !big_sepM_sepM.
      iDestruct "HRres" as "(HI & #Hinvs & Hρs)".
      iFrame "Hinvs Hρs".

      (* this is going to be annoying .. *)
      (* show that I ⊆ fp, or, better fp = fp' ∪ I *)

      (* first obtain the empty fragment for big_sepM_own_frag *)
Dan Frumin's avatar
Dan Frumin committed
705
706
      iMod (own_frag_empty with "Haprops") as "[Haprops #Hemp]".

707
708
709
710
711
712
713
714
715
      pose (I' := (fmap (λ X, (res_frac X, to_agree (res_name X))) I)).
      iAssert (own (flock_props_name γ) ( I'))
        with "[HI Hemp]" as "HI".
      { by iApply (big_sepM_own_frag with "Hemp"). }

      (* I' ≼ fp *)
      iDestruct (own_valid_2 with "Haprops HI")
        as %[Hfoo _]%auth_valid_discrete_2.

Dan Frumin's avatar
Dan Frumin committed
716
717
      (* TODO: RK, please take a look at this horrific script *)
      (* We are going to separate the active resources I out of the fp map *)
718
      pose (I'' := fmap res_name I).
Dan Frumin's avatar
Dan Frumin committed
719
      assert ( P', P' ## I''  fp  P'  I'') as [P' HP'].
720
      { subst I'' I' fa. clear H1.
Dan Frumin's avatar
Dan Frumin committed
721
722
723
724
725
726
727
728
729
        unfold to_props_map in *.
        pose (f := (λ X, (res_frac X, to_agree (res_name X)))).
        pose (g := (λ X:lock_res_name, (1%Qp, to_agree X))).
        (* Proof idea:
          f <$> I ≼ g <$> fp
             implies
          snd <$> f <$> I ≼ snd <$> g <$> fp
          =  to_agree o res_name <$> I ≼ to_agree <$> fp *)
        assert (((snd <$> (f <$> I)) : gmapUR prop_id (agreeR lock_res_nameC))  (snd <$> (g <$> fp))) as Hbar.
730
731
732
733
734
        { (* TODO DOESN"T  WORK SAD *)
          (* Check (gmap_fmap_mono snd (f <$> I) (g <$> fp)). *)
          admit.
          (* eapply cmra_morphism_monotone; last exact: Hfoo. *)
          (* apply gmap_fmap_cmra_morphism. apply _. *)
Dan Frumin's avatar
Dan Frumin committed
735
736
737
738
739
740
741
742
743
744
745
        }
        rewrite -!map_fmap_compose in Hbar.
        assert ((to_agree  res_name <$> I)  to_agree <$> fp) as Hbaz by exact: Hbar.
        rewrite map_fmap_compose in Hbaz.

        (* which implies the following *)
        assert ( i, to_agree <$> (res_name <$> (I !! i))  to_agree <$> (fp !! i)) as Hbork.
        { intros i. rewrite -!lookup_fmap. revert i.
          apply lookup_included. exact: Hbaz. }
        clear Hbaz Hbar Hfoo.

746
        generalize dependent fp.
Dan Frumin's avatar
Dan Frumin committed
747
        induction I as [|i X I HI IHI] using map_ind; intros fp.
748
        + rewrite fmap_empty.
Dan Frumin's avatar
Dan Frumin committed
749
750
          exists fp. rewrite right_id.
          split; first solve_map_disjoint; auto.
751
752
        + rewrite fmap_insert=>Hfp.
          specialize (IHI (delete i fp)).
Dan Frumin's avatar
Dan Frumin committed
753
754
755
756
757
758
759
760
761
          assert ( j, to_agree <$> (res_name <$> I !! j)
                          (to_agree <$> delete i fp !! j)) as goodboi.
          { intros j.
            destruct (decide (i = j)) as [<-|?].
            - by rewrite HI lookup_delete.
            - specialize (Hfp j).
              rewrite lookup_insert_ne in Hfp; last done.
              rewrite lookup_delete_ne //. }
          specialize (IHI goodboi). clear goodboi.
762
763
          destruct IHI as [P [HP HU]].
          assert (P !! i = None) as HPi.
Dan Frumin's avatar
Dan Frumin committed
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
          { destruct (P !! i) as [Y|] eqn:HPi; auto; simplify_eq/=.
            exfalso. unfold_leibniz.
            specialize (HU i). fold_leibniz.
            rewrite (lookup_union_Some_l _ _ _ _ HPi) in HU.
            rewrite lookup_delete in HU. done. }
          exists P. split; first solve_map_disjoint.
          rewrite -insert_union_r // -HU.
          rewrite insert_delete=> j.
          specialize (Hfp j).
          destruct (decide (i = j)) as [<-|?].
          * revert Hfp. rewrite !lookup_insert.
            intros Hfp.
            destruct (proj1( option_included _ _) Hfp)
              as [?|(a&?&Ha&Hj&Heq)]; simplify_eq/=.
            destruct (fp !! i) as [Y|] eqn:HY; simplify_eq/=.
            revert Heq. rewrite to_agree_included HY.
            intros [->%to_agree_inj | ->]; reflexivity.
          * rewrite lookup_insert_ne //. }
      fold_leibniz.

784
      destruct HP' as [HP' ->].
Dan Frumin's avatar
Dan Frumin committed
785

786
787
788
789
790
791
792
793
794
795
      rewrite /all_tokens big_sepM_union //.
      iDestruct "Htokens" as "[Htokens H]".
      rewrite /I'' big_sepM_fmap. iFrame.
      iApply "Hcl".
      iNext. iExists Locked, fa, P'.
      assert (res_name <$> I = from_active fa) as <-.
      { rewrite /from_active -map_fmap_compose.
        apply map_eq=> k. by rewrite lookup_fmap. }
      iFrame. iSplit; eauto.
      rewrite big_sepM_fmap.
Dan Frumin's avatar
Dan Frumin committed
796
      iApply (big_sepM_own_frag with "Hemp HI").
797
  Admitted.
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853

  Lemma release_cancel_spec' γ lk I :
    {{{ is_flock γ lk  flocked γ I }}}
      release lk
    {{{ RET #(); [ map] i  X  I, flock_res γ i X }}}.
  Proof.
    iIntros (Φ) "(#Hl & H) HΦ". rewrite -fupd_wp.
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".

    rewrite {1}/flocked /=.
    iDestruct "H" as (fa' Hfa) "(Hflkd & Hfactive & Hfa)".
    do 2 rewrite big_sepM_sepM.
    iDestruct "Hfa" as "(HT2s & #Hinvs & Hρs)".

    iInv invN as ([|] fa fp)
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl";
      last first.
    - iDestruct (own_valid_2 with "Hstate Hflkd")
          as %[Hfoo%Excl_included _]%auth_valid_discrete_2.
      fold_leibniz. inversion Hfoo.
    - iDestruct "Hst" as ">[Hlocked Hactives]".
      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".
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hunflkd]".

      (* Empty up the set of active propositions *)
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
      { apply (auth_update _ _ (Excl' )
                               (Excl' )).
        by apply option_local_update, exclusive_local_update. }


      pose (fa := ((λ X : lock_res, (res_frac X, res_name X)) <$> I)).
      iMod ("Hcl" with "[-HΦ Hlocked Hactives Hunflkd Hρs]") as "_".
      { iNext. iExists Unlocked,,(fp  from_active fa).
        iSplitR; eauto.
        - rewrite /from_active fmap_empty. iPureIntro.
          solve_map_disjoint.
        - iFrame. rewrite /from_active fmap_empty right_id /=.
          iFrame "Haprops".
          rewrite /all_tokens.
          rewrite big_sepM_union // -map_fmap_compose.
          rewrite big_sepM_fmap. by iFrame. }
      iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
      iModIntro. iNext. iIntros "_". iApply "HΦ".
      rewrite /flock_res !big_sepM_sepM.
      iFrame "Hρs Hinvs".
      rewrite big_sepM_fmap. iFrame.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
854

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