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

Dan Frumin's avatar
Dan Frumin committed
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 40 41 42 43 44 45 46
(** 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:
    
        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. *)

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

Dan Frumin's avatar
Dan Frumin committed
60 61
(* Defined as `positive` so that we have a `Fresh` instance for `gset positive`.
   Doubles as an invariant name. *)
62
Definition prop_id := positive.
Dan Frumin's avatar
Dan Frumin committed
63
Canonical Structure gnameC := leibnizC gname.
64

Dan Frumin's avatar
Dan Frumin committed
65 66 67 68 69 70
(** The trick here 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 *)
Record lock_res_name := {
  flock_cinv_name : gname;
  flock_token1_name : gname;
  flock_token2_name : gname;
Dan Frumin's avatar
Dan Frumin committed
71
}.
Dan Frumin's avatar
Dan Frumin committed
72
Canonical Structure lock_res_nameC := leibnizC lock_res_name.
73

74 75 76
Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
77
    flock_lockG  :> lockG Σ;
Dan Frumin's avatar
Dan Frumin committed
78 79 80 81 82
    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);
83 84
  }.

Dan Frumin's avatar
Dan Frumin committed
85 86 87 88 89 90 91 92
Record lock_res `{flockG Σ} := {
  res_prop : iProp Σ;
  res_frac : frac;
  res_name : lock_res_name;
}.

Definition LockRes `{flockG Σ} (R : iProp Σ) (π : frac) (ρ : lock_res_name) :=
  {| res_prop := R; res_frac := π; res_name := ρ |}.
93

Dan Frumin's avatar
Dan Frumin committed
94 95 96 97 98 99 100 101 102 103 104
(* TODO: DF, finish this *)
(* Definition flockΣ : gFunctors := *)
(*   #[GFunctor (authR (optionUR (exclR lockstateC))) *)
(*    ;lockΣ *)
(*    ;savedPropΣ *)
(*    ;GFunctor fracR *)
(*    ;GFunctor (authR (optionUR (exclR (gmapC prop_id PropPermC)))) *)
(*    ;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))%CF]. *)

(* Instance subG_flockΣ Σ : subG flockΣ Σ → flockG Σ. *)
(* Proof. solve_inG. Qed. *)
105

Léon Gondelman's avatar
Léon Gondelman committed
106
Section flock.
107 108
  Context `{heapG Σ, flockG Σ}.
  Variable N : namespace.
Dan Frumin's avatar
Dan Frumin committed
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
  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' (X : lock_res) : iProp Σ := *)
  (*   (res_prop X ∗ token₁ (res_name X) ∨ token₂ (res_name X))%I. *)

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

  (* Tokens that allow you to get all the propositions from `A` out of the invariants *)
  Definition all_tokens (P : gmap prop_id lock_res_name) : iProp Σ :=
    ([ map] i  X  P, token X)%I.
  
  (** 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.
  
  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.
137

Dan Frumin's avatar
Dan Frumin committed
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
  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
154 155

  Definition flock_inv (γ : flock_name) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
156 157
    ( (s : lockstate)
       (** fa -- active propositions, fp -- pending propositions *)
Dan Frumin's avatar
Dan Frumin committed
158 159
       (fa : gmap prop_id (frac * lock_res_name))
       (fp : gmap prop_id lock_res_name),
Dan Frumin's avatar
Dan Frumin committed
160
       fp ## from_active fa 
Dan Frumin's avatar
Dan Frumin committed
161
       own (flock_state_name γ) ( (Excl' s)) 
Dan Frumin's avatar
Dan Frumin committed
162
       own (flock_props_name γ) ( to_props_map (fp  from_active fa)) 
Dan Frumin's avatar
Dan Frumin committed
163 164
       own (flock_props_active_name γ) ( Excl' fa) 
       all_tokens fp 
Dan Frumin's avatar
Dan Frumin committed
165
       match s with
Dan Frumin's avatar
Dan Frumin committed
166
       | Locked =>
Dan Frumin's avatar
Dan Frumin committed
167
         locked (flock_lock_name γ) 
Dan Frumin's avatar
Dan Frumin committed
168 169 170 171
         ([ map] i  πX  fa, own (flock_props_name γ) ( {[i:=(πX.1,to_agree πX.2)]}))
       | Unlocked =>
         (* there are no active proposition *)
         own (flock_props_active_name γ) ( Excl' )
Dan Frumin's avatar
Dan Frumin committed
172 173 174
       end)%I.

  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
Dan Frumin's avatar
Dan Frumin committed
175 176
    (inv invN (flock_inv γ) 
     is_lock lockN (flock_lock_name γ) lk
Dan Frumin's avatar
Dan Frumin committed
177 178
         (own (flock_state_name γ) ( (Excl' Unlocked))))%I.

Dan Frumin's avatar
Dan Frumin committed
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
  (** * Lemmata **)

  (** ** Basic properties of the CAPs *)
  (* Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) (π1 π2 : frac) : *)
  (*   flock_res γ s R (π1+π2) ⊣⊢ flock_res γ s R π1 ∗ flock_res γ s R π2. *)
  (* Proof. *)
  (*   rewrite /flock_res. iSplit. *)
  (*   - iDestruct 1 as (ρ) "(Hs & #Hinv & Hρ)". *)
  (*     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 (ρ) "(Hs1 & #Hinv1 & Hρ1)". *)
  (*     iDestruct "H2" 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']. *)
  (*     fold_leibniz. rewrite -!Hfoo. *)
  (*     iCombine "Hρ1 Hρ2" as "Hρ". *)
  (*     rewrite !frac_op' agree_idemp. *)
  (*     iExists ρ. by iFrame. *)
  (* Qed. *)

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

  (* Global Instance flock_res_as_fractional γ s R π : *)
  (*   AsFractional (flock_res γ s R π) (flock_res γ s R) π. *)
  (* Proof. split. done. apply _. Qed. *)
  
  Lemma to_props_map_singleton_included fp i q ρ:
    {[i := (q, to_agree ρ)]}  to_props_map fp  fp !! i = Some ρ.
213
  Proof.
Dan Frumin's avatar
Dan Frumin committed
214 215 216
    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 -> //.
217 218
  Qed.

Dan Frumin's avatar
Dan Frumin committed
219 220 221 222 223
  Lemma to_props_map_delete fp i:
    delete i (to_props_map fp) = to_props_map (delete i fp).
  Proof.
    by rewrite /to_props_map fmap_delete. 
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
224

Dan Frumin's avatar
Dan Frumin committed
225 226 227 228 229
  (** ** 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 ρ).
230
  Proof.
Dan Frumin's avatar
Dan Frumin committed
231 232 233 234 235 236
    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
237 238
    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
239
    { apply is_fresh. }    
Dan Frumin's avatar
Dan Frumin committed
240
    apply not_elem_of_union in Hs. destruct Hs as [Hi1 Hi2].
Dan Frumin's avatar
Dan Frumin committed
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255

    (* 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 |}).
    
    (* 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
256 257 258 259 260
      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
261 262 263 264 265 266 267 268 269 270 271 272 273 274
    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.
      eapply (not_elem_of_dom (D:=gset prop_id)).        
      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
275 276
  Qed.

Dan Frumin's avatar
Dan Frumin committed
277 278 279 280 281
  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
282
  Proof.
Dan Frumin's avatar
Dan Frumin committed
283 284 285 286 287 288 289 290 291 292 293
    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
294
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
295
      iAssert (fa !! i = None)%I with "[-]" as %Hbar.
Dan Frumin's avatar
Dan Frumin committed
296 297 298
      { 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
299
        (* TODO: RK, please look at this! *)
Dan Frumin's avatar
Dan Frumin committed
300
        iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz.
Dan Frumin's avatar
Dan Frumin committed
301 302 303 304 305
        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
306
      assert (fp !! i = Some ρ) as Hbaz.
Dan Frumin's avatar
Dan Frumin committed
307 308
      { apply lookup_union_Some in Hfoo; last done.
        destruct Hfoo as [? | Hfoo]; first done.
Dan Frumin's avatar
Dan Frumin committed
309 310 311 312
        exfalso. revert Hfoo. by rewrite /from_active lookup_fmap Hbar.
      } 
      
      iMod (own_update_2 with "Haprops Hi") as "Haprops".
Dan Frumin's avatar
Dan Frumin committed
313
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
Dan Frumin's avatar
Dan Frumin committed
314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330
      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 Locked,fa,(delete i fp). iFrame.
      iSplit.
      + iPureIntro. by apply map_disjoint_delete_l.
      + 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
331 332 333 334
      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
335 336
      rewrite /from_active fmap_empty /= right_id.
      iDestruct (own_valid_2 with "Haprops Hi")
Dan Frumin's avatar
Dan Frumin committed
337
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
338
      iMod (own_update_2 with "Haprops Hi") as "Haprops".
Dan Frumin's avatar
Dan Frumin committed
339
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
Dan Frumin's avatar
Dan Frumin committed
340 341 342 343 344 345 346 347 348 349 350 351 352 353
      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.
      + iPureIntro. by apply map_disjoint_delete_l.
      + rewrite /from_active fmap_empty /= right_id.
        by rewrite to_props_map_delete.
Dan Frumin's avatar
Dan Frumin committed
354
  Qed.
355

Dan Frumin's avatar
Dan Frumin committed
356
  Lemma newflock_spec :
Dan Frumin's avatar
Dan Frumin committed
357
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
358 359
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
360 361
    iMod (own_alloc ( (Excl' Unlocked)   (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
362 363 364 365 366 367
    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
368
    iApply (newlock_spec lockN (own γ_state ( (Excl' Unlocked))) with "Hfrag").
369
    iNext. iIntros (lk γ_lock) "#Hlock".
Dan Frumin's avatar
Dan Frumin committed
370
    pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
Dan Frumin's avatar
Dan Frumin committed
371 372 373
    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
374
    iModIntro. iApply ("HΦ" $! lk γ with "[-]").
375 376
    rewrite /is_flock. by iFrame "Hlock".
  Qed.
Léon Gondelman's avatar
Léon Gondelman committed
377

Dan Frumin's avatar
Dan Frumin committed
378 379
  Lemma acquire_flock_single_spec γ lk i X :
    {{{ is_flock γ lk  flock_res γ i X }}}
380
      acquire lk
Dan Frumin's avatar
Dan Frumin committed
381
    {{{ RET #();  (res_prop X)  ( (res_prop X) ={}= flocked γ {[i:=X]}) }}}.
382
  Proof.
Dan Frumin's avatar
Dan Frumin committed
383
    destruct X as [R π ρ].
Dan Frumin's avatar
Dan Frumin committed
384
    iIntros (Φ) "(Hl & HRres) HΦ".
Dan Frumin's avatar
Dan Frumin committed
385 386
    rewrite /is_flock. iDestruct "Hl" as "(#Hfl & #Hlk)".
    iApply wp_fupd.
Dan Frumin's avatar
Dan Frumin committed
387 388
    iApply (acquire_spec with "Hlk").
    iNext. iIntros "[Hlocked Hunlk]".
Dan Frumin's avatar
Dan Frumin committed
389 390 391
    iInv invN as ([|] fa fp) 
      "(>% & >Hstate & >Haprops & >Haactive & >Htokens & Hst)" "Hcl".
    - iDestruct "Hst" as "(>Hlocked2 & ?)".
Dan Frumin's avatar
Dan Frumin committed
392
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
Dan Frumin's avatar
Dan Frumin committed
393
    - iDestruct "Hst" as ">Hfactive".
Dan Frumin's avatar
Dan Frumin committed
394 395 396 397
      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
398 399
      rewrite /from_active fmap_empty /= right_id.
      iDestruct "HRres" as "(Hi & #Hinv & Hρ)".
Dan Frumin's avatar
Dan Frumin committed
400 401

      (* Unlocked ~~> Locked *)
Dan Frumin's avatar
Dan Frumin committed
402
      iMod (own_update_2 with "Hstate Hunlk") as "Hstate".
Dan Frumin's avatar
Dan Frumin committed
403
      { apply (auth_update _ _ (Excl' Locked) (Excl' Locked)).
Dan Frumin's avatar
Dan Frumin committed
404 405 406
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
407

Dan Frumin's avatar
Dan Frumin committed
408
      (* (i,ρ) ∈ fp *)
Dan Frumin's avatar
Dan Frumin committed
409
      iDestruct (own_valid_2 with "Haprops Hi")
Dan Frumin's avatar
Dan Frumin committed
410
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
Dan Frumin's avatar
Dan Frumin committed
411 412

      (* move (i,ρ) to the set of active propositions *)
Dan Frumin's avatar
Dan Frumin committed
413 414 415
      rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
      iDestruct "Htokens" as "[T2 Htokens]".
      
Dan Frumin's avatar
Dan Frumin committed
416
      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
Dan Frumin's avatar
Dan Frumin committed
417 418
      { apply (auth_update _ _ (Excl' {[ i := (π, ρ) ]})
                               (Excl' {[ i := (π, ρ) ]})).
Dan Frumin's avatar
Dan Frumin committed
419
        by apply option_local_update, exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
420

Dan Frumin's avatar
Dan Frumin committed
421 422 423
      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
424 425
        - iPureIntro.
          rewrite /from_active map_fmap_singleton /=.
Dan Frumin's avatar
Dan Frumin committed
426
          apply map_disjoint_singleton_r, lookup_delete.
Dan Frumin's avatar
Dan Frumin committed
427
        - rewrite /from_active map_fmap_singleton /=.
Dan Frumin's avatar
Dan Frumin committed
428 429 430
          rewrite -insert_union_singleton_r.
          2: { apply lookup_delete. }
          rewrite insert_delete insert_id //.
Dan Frumin's avatar
Dan Frumin committed
431
        - rewrite /all_tokens big_sepM_singleton //. }
Dan Frumin's avatar
Dan Frumin committed
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448
      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
449
  Qed.
Dan Frumin's avatar
Dan Frumin committed
450

Dan Frumin's avatar
Dan Frumin committed
451 452
  Lemma release_cancel_spec γ lk i X :
    {{{ is_flock γ lk  flocked γ {[i:=X]} }}}
453
      release lk
Dan Frumin's avatar
Dan Frumin committed
454
    {{{ RET #(); flock_res γ i X }}}.
455
  Proof.
Dan Frumin's avatar
Dan Frumin committed
456
    iIntros (Φ) "(#Hl & H) HΦ". rewrite -fupd_wp.
Dan Frumin's avatar
Dan Frumin committed
457
    rewrite /is_flock. iDestruct "Hl" as "(#Hinv & #Hlk)".
Dan Frumin's avatar
Dan Frumin committed
458 459 460 461 462 463

    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
464 465 466
    - 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
467
    - iDestruct "Hst" as ">[Hlocked Hactives]".
Dan Frumin's avatar
Dan Frumin committed
468 469 470 471 472 473
      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".
474 475 476
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
Dan Frumin's avatar
Dan Frumin committed
477
      iDestruct "Hstate" as "[Hstate Hunflkd]".
Léon Gondelman's avatar
Léon Gondelman committed
478

Dan Frumin's avatar
Dan Frumin committed
479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502
      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. }

      (* Get the tokens out of cinvs *)
      iDestruct "Hfa" as "(T2 & #Hiinv & Hρ)".
      iMod (cinv_open with "Hiinv Hρ") as "(HC & Hρ & Hcl2)". solve_ndisj.
      iDestruct "HC" as "[[HR >T1] | >T2']"; last first.
      { iDestruct (own_valid_2 with "T2' T2") as %?. done. }
      iMod ("Hcl2" with "[HR T1]") as "_".
      { iNext. iLeft. iFrame. }

      iMod ("Hcl" with "[-HΦ Hlocked Hactives Hunflkd Hρ]") as "_".
      { iNext. iExists Unlocked,,(<[i:=ρ]>fp).
        iSplitR; eauto.
        - rewrite /from_active fmap_empty. iPureIntro.
          apply map_disjoint_empty_r.
        - iFrame. rewrite /from_active fmap_empty right_id /=.
          rewrite map_fmap_singleton.
Dan Frumin's avatar
Dan Frumin committed
503 504 505 506
          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
507 508 509 510
          rewrite -insert_union_singleton_r // /=. iFrame.
          rewrite /all_tokens big_sepM_insert //.
          iFrame.
      }
Dan Frumin's avatar
Dan Frumin committed
511
      iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
Dan Frumin's avatar
Dan Frumin committed
512 513
      iModIntro. iNext. iIntros "_". iApply "HΦ".
      by iFrame.
Dan Frumin's avatar
Dan Frumin committed
514
  Qed.
Dan Frumin's avatar
Dan Frumin committed
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536

  (** 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
537 538
  Qed.

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 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 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 644 645 646 647 648 649 650 651 652 653 654 655 656 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 705 706 707 708 709 710 711 712
  (* Lemma big_sepM_own_frag {A B : Type} `{EqDecision A, Countable A} *)
  (*       `{inG Σ (authR (gmapUR A C))} (f : B → C) (m : gmap A B) (γ : gname) : *)
  (*   own γ (◯ ∅) -∗ *)
  (*   own γ (◯ (f <$> m)) ∗-∗ [∗ map] i↦x ∈ m, own γ (◯ {[ i := f x ]}). *)
  (* Proof. *)
  (*   simple refine (map_ind (λ m, _)%I _ _ m); simpl. *)
  (*   - iIntros "He". rewrite fmap_empty big_sepM_empty. iSplit; eauto. *)
  (*   - iIntros (i x m' Hi IH) "He". *)
  (*     rewrite fmap_insert insert_union_singleton_l. *)
  (*     assert (({[i := f x]} ∪ (f <$> m')) = {[i := f x]} ⋅ (f <$> m')) as ->. *)
  (*     { rewrite /op /cmra_op /= /gmap_op. *)
  (*       apply map_eq. intros j. destruct (decide (i = j)) as [->|?]. *)
  (*       - etransitivity. eapply lookup_union_Some_l. apply lookup_insert. *)
  (*         symmetry. rewrite lookup_merge lookup_insert. *)
  (*         rewrite lookup_fmap Hi /=. done. *)
  (*       - remember (m' !! j) as mj. *)
  (*         destruct mj; simplify_eq/=. *)
  (*         + etransitivity. apply lookup_union_Some_raw. *)
  (*           right. split; first by rewrite lookup_insert_ne. *)
  (*           by rewrite lookup_fmap -Heqmj. *)
  (*           symmetry. rewrite lookup_merge lookup_singleton_ne; eauto. *)
  (*           rewrite lookup_fmap -Heqmj. done. *)
  (*         + etransitivity. apply lookup_union_None. *)
  (*           split; first by rewrite lookup_singleton_ne. *)
  (*           rewrite lookup_fmap -Heqmj //. *)
  (*           symmetry. *)
  (*           rewrite lookup_merge lookup_singleton_ne // lookup_fmap -Heqmj //. } *)
  (*     rewrite auth_frag_op own_op IH big_sepM_insert; last eauto. *)
  (*     iSplit; iIntros "[$ Hm']"; by iApply "He". *)
  (* Qed. *)

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

  (*     (* Unlocked ~~> Locked *) *)
  (*     iMod (own_update_2 with "Hstate Hunlk") as "Hstate". *)
  (*     { apply (auth_update _ _ (Excl' Locked) (Excl' Locked)). *)
  (*       apply option_local_update. *)
  (*       by apply exclusive_local_update. } *)
  (*     iDestruct "Hstate" as "[Hstate Hflkd]". *)

  (*     iDestruct (extract_existential with "HRres") as (J HJ) "HRres". *)

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

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

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

  (*     assert (∃ fo : gmap prop_id PropPerm, *)
  (*                to_props_map fp = to_props_map_ fs ⋅ to_props_map_ fo) *)
  (*       as [fo Hfo]. *)
  (*     { admit. } *)

  (*     rewrite (all_props_to_props_map_ fp fs fo); last done. *)
  (*     iDestruct "Hfp" as "[Hfs_props Hfo]". *)

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

  (*     rewrite (big_sepM_sepM _ _ J). *)
  (*     iDestruct "HJ" as "[#HJ Htokens]". *)

  (*     iMod ("Hcl" with "[-HΦ Haactive Hflkd Hfs_props Hfs HJ]") as "_". *)
  (*     { iNext. iExists Locked,(from_active fo),fs. *)
  (*       iFrame. iSplitR. admit. (* TODO: map_disjoint *) *)
  (*       iSplitL "Hauth". *)
  (*       - admit. (* fp = from_active fo ∪ from_active fs *) *)
  (*       - rewrite /all_tokens /fs big_sepM_fmap /= //. } *)

  (*     iAssert (▷▷ [∗ map] p ∈ I, p.1)%I with "[Hfs_props]" as "Hfs_props". *)
  (*     { iNext. rewrite /all_props /fs -HJ !big_sepM_fmap big_sepM_later /=. *)
  (*       (* TODO: why is big_sepM_mono not formulated with the persistence modality? *) *)
  (*       iCombine "HJ Hfs_props" as "Hfs". *)
  (*       rewrite -big_sepM_sepM. *)
  (*       iApply (big_sepM_mono with "Hfs"). *)
  (*       iIntros (k ρ Hk) "[#Hsaved HR]". *)
  (*       iDestruct "HR" as (R') "[Hsaved' HR']". *)
  (*       iDestruct (saved_prop_agree with "Hsaved Hsaved'") as "#Hfoo". *)
  (*       iNext. iRewrite -"Hfoo" in "HR'". done. *)
  (*       (* TODO: iRewrite "Hfoo" didn't work *) } *)

  (*     iModIntro. iApply "HΦ". *)
  (*     iNext. iFrame "Hfs_props". iIntros "Hfs_props". *)
  (*     clear Hfoo H1 Hfo fp. rewrite /flocked /flock_res. *)
  (*     iInv (flockN.@"inv") as ([|] fp fa) "(>% & >Hstate & >Hauth & >Hfactive & Hfp & Hrest)" "Hcl"; last first. *)
  (*     + iDestruct (own_valid_2 with "Hstate Hflkd") *)
  (*         as %[Hfoo%Excl_included _]%auth_valid_discrete_2. *)
  (*       fold_leibniz. inversion Hfoo. *)
  (*     + iDestruct "Hrest" as ">[Hlocked Htokens]". *)

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

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

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

  (*       iMod (own_update _ _ (● to_props_map _ ⋅ ◯ ∅) with "Hauth") as "[Hauth He]". *)
  (*       { by apply auth_update_alloc. } *)

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

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