WIP: multi-flock-res acquire

theories/c_translation/monad.v

@@ -67,12 +67,16 @@ Section a_wp.
        ∗ ([∗ map] l ↦ _ ∈ σ, ∃ v', l ↦{1/2} v')
        ∗ ⌜correct_locks X (locked_locs σ)⌝)%I.
 
+  Definition flock_resources (γ : flock_name) (I : gmap prop_id (iProp Σ * frac)) :=
+    ([∗ map] i ↦ p ∈ I, flock_res γ i p.1 p.2)%I.
+
   Definition awp (e : expr)
       (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ :=
-    tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (π : frac) (i : prop_id) (env : val) (l : val),
+    tc_opaque (WP e {{ ev, ∀ (γ : flock_name) (env : val) (l : val) (I : gmap prop_id (iProp Σ * frac)),
       is_flock amonadN γ l -∗
-      flock_res γ i (env_inv env ∗ R) π -∗
-      WP ev env l {{ v, Φ v ∗ flock_res γ i (env_inv env ∗ R) π }}
+      flock_resources γ I -∗
+      (([∗ map] p ∈ I, p.1) ≡ (env_inv env ∗ R)) -∗
+      WP ev env l {{ v, Φ v ∗ flock_resources γ I }}
     }})%I.
 
   Global Instance elim_bupd_awp p e Φ :
@@ -107,21 +111,30 @@ Section a_wp_rules.
 
   Lemma awp_insert_res e Φ R1 R2 :
     ▷ R1 -∗
-    awp e (R1 ∗ R2) (λ v, R1 -∗ Φ v) -∗
+    awp e (R1 ∗ R2) (λ v, ▷ ▷ R1 -∗ Φ v) -∗
     awp e R2 Φ.
   Proof.
     iIntros "HR1 Hawp". rewrite /awp /=.
     iApply (wp_wand with "Hawp").
     iIntros (v) "HΦ".
-    iIntros (γ π i env l) "#Hflock Hres".
-  (*   iMod (flock_res_insert_unflocked with "Hflock Hres Hunfl HR1") *)
-  (*     as "(#Hres & Hunfl)"; first done. *)
-  (*   iApply ("HΦ" with "Hflock [Hres] Hunfl"). *)
-  (*   rewrite (comm (∗)%I R1 R2). *)
-  (*   rewrite (assoc (∗)%I _ R2 R1). *)
-  (*   by iFrame "Hres". *)
-  (* Qed. *)
-  Abort.
+    iIntros (γ env l I) "#Hflock Hres #Heq".
+    iMod (flock_res_single_alloc _ (dom (gset prop_id) I) with "Hflock HR1") as (j) "[% Hres']"; first done.
+    pose (I' := <[j:= (R1,1%Qp)]>I).
+    assert (I !! j = None) by by eapply not_elem_of_dom.
+    iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []").
+    { rewrite /flock_resources /I'.
+      rewrite big_sepM_insert; last done. iFrame. }
+    { rewrite big_sepM_insert; last done. simpl. iRewrite "Heq".
+      rewrite (assoc _ R1 _ R2).
+      rewrite (comm _ R1 (env_inv env)).
+      rewrite -(assoc _ _ R1 R2). done. }
+    iApply wp_fupd.
+    iApply (wp_wand with "HΦ").
+    iIntros (w) "[HΦ HI]". rewrite /flock_resources /I'.
+    rewrite big_sepM_insert /=; last done. iDestruct "HI" as "[HR1 $]".
+    iMod (flock_res_single_dealloc with "Hflock HR1") as (R') "[HR' Heq']"; first done.
+    iApply "HΦ". iModIntro. do 2 iNext. by iRewrite "Heq'".
+  Qed.
 
   Lemma awp_wand e (Φ Ψ : val → iProp Σ) R :
     awp e R Φ -∗
@@ -131,8 +144,8 @@ Section a_wp_rules.
     iIntros "HAWP Hv". rewrite /awp /=.
     iApply (wp_wand with "HAWP").
     iIntros (v) "HΦ".
-    iIntros (γ π i env l) "#Hflock Hres".
-    iApply (wp_wand with "[HΦ Hres]"); first by iApply "HΦ".
+    iIntros (γ env l I) "#Hflock Hres #Heq".
+    iApply (wp_wand with "[HΦ Hres]"). iApply ("HΦ" with "Hflock Hres Heq").
     iIntros (w) "[HΦ $]". by iApply "Hv".
   Qed.
 
@@ -151,7 +164,7 @@ Section a_wp_rules.
   Proof.
     iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp").
     iIntros (v) "HΦ". wp_lam.
-    iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam. iFrame.
+    iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam. iFrame.
   Qed.
 
   Lemma awp_bind (f e : expr) R Φ :
@@ -161,10 +174,10 @@ Section a_wp_rules.
   Proof.
     iIntros ([fv <-%of_to_val]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
     iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
-    iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam. wp_bind (ev env l).
-    iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
+    iIntros (γ env l I) "#Hflock Hres #Heq". do 2 wp_lam. wp_bind (ev env l).
+    iApply (wp_wand with "[Hwp Hres]"). iApply ("Hwp" with "Hflock Hres Heq").
     iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
-    iIntros (v) "H". by iApply ("H" with "[$]").
+    iIntros (v) "H". iApply ("H" with "Hflock Hres Heq").
   Qed.
 
   Lemma awp_atomic (e : expr) (ev : val) R Φ :
@@ -173,48 +186,50 @@ Section a_wp_rules.
     awp (a_atomic e) R Φ.
   Proof.
     iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic /=. wp_lam.
-    iIntros (γ π i env l) "#Hlock1 Hres". do 2 wp_let.
+    iIntros (γ env l I) "#Hlock1 Hres #Heq1". do 2 wp_let.
     wp_apply (acquire_cancel_spec with "[$]").
-    iDestruct 1 as (R') "(HR' & #Heq & Hcl)". wp_seq.
-    iAssert (▷ (env_inv env ∗ R))%I with "[HR']" as "[Henv HR]".
-    { iNext. iRewrite "Heq". done. } 
+    iIntros "[HI Hcl]". iRewrite "Heq1" in "HI".
+    iDestruct "HI" as "[Henv HR]".
     iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
+    wp_seq.
     wp_apply (newlock_cancel_spec amonadN); first done.
     iIntros (k γ') "#Hlock2".
-    iMod (flock_res_single_alloc _ _ _ (env_inv env ∗ Q)%I
-            with "Hlock2 [$Henv $HQ]") as (i') "Hres"; first done.
+    iMod (flock_res_single_alloc _ (dom (gset prop_id) I) _ _ (env_inv env ∗ Q)%I
+            with "Hlock2 [$Henv $HQ]") as (i') "[% Hres]"; first done.
     wp_let.
     wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
-    iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
-    iIntros (w) "[HR Hres]".
-    iMod (flock_res_single_dealloc with "Hlock2 Hres") as (Q') "[HQ' #HeqQ]"; first done.
-    wp_let.
-    iAssert (▷ (env_inv env ∗ Q))%I with "[HQ']" as "[Henv HQ]".
-    { iNext. by iRewrite "HeqQ". }
-    iDestruct ("HR" with "HQ") as "[HR HΦ]".
-    iAssert (▷ R')%I with "[HR Henv]" as "HR'".
-    { iNext. iRewrite -"Heq". iFrame. }
-    iMod ("Hcl" with "HR'") as "[Hflocked Hres]".
-    wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
-    iIntros "_". wp_seq. iFrame.
+    iApply (wp_wand with "[Hwp Hres]").
+    - iApply ("Hwp" $! _ _ _ {[i' := ((env_inv env ∗ Q)%I,1%Qp)]} with "Hlock2 [Hres] []").
+      + rewrite /flock_resources big_sepM_singleton //.
+      + rewrite big_sepM_singleton //.
+    - iIntros (w) "[HR Hres]".
+      rewrite /flock_resources big_sepM_singleton /=.
+      iMod (flock_res_single_dealloc with "Hlock2 Hres") as (Q') "[HQ' #Heq2]"; first done.
+      wp_let.
+      iAssert (▷ (env_inv env ∗ Q))%I with "[HQ']" as "[Henv HQ]".
+      { iNext. by iRewrite "Heq2". }
+      iDestruct ("HR" with "HQ") as "[HR HΦ]".
+      iMod ("Hcl" with "[HR Henv]") as "[Hflocked Hres]".
+      { iNext. iRewrite "Heq1". iFrame. }
+      wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
+      iIntros "_". wp_seq. iFrame.
   Qed.
 
   Lemma awp_atomic_env (e : expr) (ev : val) R Φ :
     IntoVal e ev →
-    (∀ env, ▷ env_inv env -∗ ▷ R -∗
-        WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗
+    (∀ env, env_inv env -∗ R -∗
+        WP ev env {{ w, ▷ env_inv env ∗ ▷ R ∗ ▷ Φ w }}) -∗
     awp (a_atomic_env e) R Φ.
   Proof.
     iIntros (<-%of_to_val) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam.
-    iIntros (γ π i env l) "#Hlock Hres". do 2 wp_lam.
+    iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam.
     wp_apply (acquire_cancel_spec with "[$]").
-    iDestruct 1 as (R') "(HR' & #Heq & Hcl)". wp_seq.
-    iAssert (▷ (env_inv env ∗ R))%I with "[HR']" as "[Henv HR]".
-    { iNext. iRewrite "Heq". done. }
+    iIntros "[HI Hcl]". iRewrite "Heq" in "HI".
+    iDestruct "HI" as "[Henv HR]".
     iDestruct ("Hwp" with "Henv HR") as "Hwp".
-    wp_apply (wp_wand with "Hwp").
+    wp_seq. wp_apply (wp_wand with "Hwp").
     iIntros (w) "[Henv [HR HΦ]]". wp_let.
-    iRewrite -"Heq" in "Hcl".
+    iRewrite "Heq" in "Hcl".
     iMod ("Hcl" with "[$HR $Henv]") as "[Hflocked Hres]".
     wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
     iIntros "_". wp_seq. iFrame.
@@ -231,13 +246,27 @@ Section a_wp_rules.
     iIntros (ev1) "Hwp1". wp_lam.
     wp_bind e2. iApply (wp_wand with "Hwp2").
     iIntros (ev2) "Hwp2". wp_lam.
-    iIntros (γ π i env l) "#Hlock [Hres1 Hres2]". do 2 wp_lam.
-    iApply (par_spec (λ v, Ψ1 v ∗ flock_res _ _ _ (π/2))%I
-                     (λ v, Ψ2 v ∗ flock_res _ _ _ (π/2))%I
+    iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam.
+    pose (I' := fmap (λ x, (x.1, (x.2/2)%Qp)) I).
+    iAssert (flock_resources γ I' ∗ flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
+    { rewrite /flock_resources -big_sepM_sepM.
+      rewrite /I' big_sepM_fmap /=.
+      iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl.
+      by rewrite -flock_res_op Qp_div_2. }
+    iApply (par_spec (λ v, Ψ1 v ∗ flock_resources γ I')%I
+                     (λ v, Ψ2 v ∗ flock_resources γ I')%I
       with "[Hwp1 Hres1] [Hwp2 Hres2]").
     - wp_lam. iApply ("Hwp1" with "Hlock Hres1").
+      by rewrite /I' big_sepM_fmap /=.
     - wp_lam. iApply ("Hwp2" with "Hlock Hres2").
-    - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
+      by rewrite /I' big_sepM_fmap /=.
+    - iNext. iIntros (w1 w2) "[[HΨ1 Hres1] [HΨ2 Hres2]]".
+      iAssert (flock_resources γ I)%I with "[Hres1 Hres2]" as "$".
+      { iCombine "Hres1 Hres2" as "Hres".
+        rewrite /flock_resources -big_sepM_sepM.
+        rewrite /I' big_sepM_fmap /=.
+        iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl.
+          by rewrite -flock_res_op Qp_div_2. }
       iApply ("HΦ" with "[$] [$]").
   Qed.
 End a_wp_rules.
@@ -257,17 +286,21 @@ Section a_wp_run.
     pose (amg := AMonadG Σ _ _ _ _).
     wp_apply (newlock_cancel_spec amonadN); first done.
     iIntros (k γ') "#Hlock". rewrite- wp_fupd.
-    iMod (flock_res_single_alloc _ _ _ (env_inv env ∗ R)%I
-            with "Hlock [Henv Hσ $HR]") as (i) "Hres"; first done.
+    iMod (flock_res_single_alloc _ ∅ _ _ (env_inv env ∗ R)%I
+            with "Hlock [Henv Hσ $HR]") as (i) "[_ Hres]"; first done.
     { iNext. iExists ∅, ∅. iFrame. eauto. }
     iSpecialize ("Hwp" $! amg).
     iMod (wp_value_inv with "Hwp") as "Hwp".
     wp_let. wp_bind (ev env k).    
-    iApply (wp_wand with "[Hwp Hres]"); first by iApply "Hwp".
-    iIntros (w) "[HΦ Hres]".
-    iMod (flock_res_single_dealloc with "Hlock Hres") as (R') "[HR' #Heq]"; first done.
-    wp_let.
-    iApply "HΦ". iNext. iRewrite -"Heq" in "HR'". iDestruct "HR'" as "[_ $]".
+    iApply (wp_wand with "[Hwp Hres]").
+    - iApply ("Hwp" $! _ _ _ {[i := ((env_inv env ∗ R)%I,1%Qp)]} with "Hlock [Hres] []").
+      + rewrite /flock_resources big_sepM_singleton //.
+      + rewrite big_sepM_singleton //.
+    - iIntros (w) "[HΦ Hres]".
+      rewrite /flock_resources big_sepM_singleton /=.
+      iMod (flock_res_single_dealloc with "Hlock Hres") as (R') "[HR' #Heq]"; first done.
+      wp_let.
+      iApply "HΦ". iNext. iRewrite -"Heq" in "HR'". iDestruct "HR'" as "[_ $]".
   Qed.
 End a_wp_run.
 

theories/lib/flock.v

@@ -23,13 +23,20 @@ Record flock_name := {
 Definition prop_id := positive.
 Canonical Structure gnameC := leibnizC gname.
 
+Record PropPerm := {
+  prop_perm : frac;
+  prop_saved_name : gname;
+  prop_perm_name : gname
+}.
+Canonical Structure PropPermC := leibnizC PropPerm.
+
 Class flockG Σ :=
   FlockG {
     flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
     flock_lockG  :> lockG Σ;
     flock_savedProp :> savedPropG Σ;
     flock_tokens :> inG Σ fracR;
-    flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id (prodC fracC (prodC gnameC gnameC))))));
+    flock_props_active :> inG Σ (authR (optionUR (exclR (gmapC prop_id PropPermC))));
     flock_props :> inG Σ (authR (gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC)))))
   }.
 
@@ -38,7 +45,7 @@ Definition flockΣ : gFunctors :=
    ;lockΣ
    ;savedPropΣ
    ;GFunctor fracR
-   ;GFunctor (authR (optionUR (exclR (gmapC prop_id (prodC fracC (prodC gnameC gnameC))))))
+   ;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 Σ.
@@ -48,11 +55,15 @@ Section flock.
   Context `{heapG Σ, flockG Σ}.
   Variable N : namespace.
   Definition flockN := N.@"flock".
-
+  
   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.
 
+  Definition to_props_map_ (f : gmap prop_id PropPerm)
+    : gmapUR prop_id (prodR fracR (agreeR (prodC gnameC gnameC))) :=
+    (λ x, (prop_perm x, to_agree (prop_saved_name x, prop_perm_name x))) <$> f.
+
   Lemma to_props_map_singleton_included fp i q ρ:
     {[i := (q, to_agree ρ)]} ≼ to_props_map fp → fp !! i = Some ρ.
   Proof.
@@ -62,8 +73,9 @@ Section flock.
     rewrite Hi. by destruct v'.
   Qed.
 
-  Definition from_active (f : gmap prop_id (frac * (gname * gname)))
-    : gmap prop_id (gname * gname) := fmap snd f.
+  Definition from_active (f : gmap prop_id PropPerm)
+    : gmap prop_id (gname * gname) :=
+    (λ x, (prop_saved_name x, prop_perm_name x)) <$> f.
 
   Lemma from_active_empty : from_active ∅ = ∅.
   Proof. by rewrite /from_active fmap_empty. Qed.
@@ -71,13 +83,18 @@ Section flock.
   Definition all_props (f : gmap prop_id (gname*gname)) : iProp Σ :=
     ([∗ map] i ↦ ρ ∈ f, ∃ R, saved_prop_own ρ.1 R ∗ R)%I.
 
-  Definition all_tokens (f : gmap prop_id (frac * (gname*gname))) : iProp Σ :=
-    ([∗ map] i ↦ ρ ∈ f, own ρ.2.2 ρ.1)%I.
+  Lemma all_props_to_props_map_ f f1 f2 :
+    to_props_map f = to_props_map_ f1 ⋅ to_props_map_ f2 →
+    all_props f ⊣⊢ all_props (from_active f1) ∗ all_props (from_active f2).
+  Proof. Admitted.
+
+  Definition all_tokens (f : gmap prop_id PropPerm) : iProp Σ :=
+    ([∗ map] i ↦ ρ ∈ f, own (prop_perm_name ρ) (prop_perm ρ))%I.
 
   Definition flock_inv (γ : flock_name) : iProp Σ :=
     (∃ (s : lockstate)
        (fp : gmap prop_id (gname * gname))
-       (fa : gmap prop_id (frac * (gname * gname))),
+       (fa : gmap prop_id PropPerm),
        (** fa -- active propositions, fp -- pending propositions *)
        ⌜fp ##ₘ from_active fa⌝ ∗
        own (flock_state_name γ) (● (Excl' s)) ∗
@@ -97,7 +114,7 @@ Section flock.
          (own (flock_state_name γ) (◯ (Excl' Unlocked))))%I.
 
   Definition flocked
-    (γ : flock_name) (f : gmap prop_id (frac * (gname * gname))) : iProp Σ :=
+    (γ : flock_name) (f : gmap prop_id PropPerm) : iProp Σ :=
     (own (flock_state_name γ) (◯ (Excl' Locked))
      ∗ own (flock_props_active_name γ) (● Excl' f)
      ∗ all_props (from_active f))%I.
@@ -135,18 +152,19 @@ Section flock.
     AsFractional (flock_res γ s R π) (flock_res γ s R) π.
   Proof. split. done. apply _. Qed.
 
-  Lemma flock_res_single_alloc γ lk R E :
+  Lemma flock_res_single_alloc (X : gset prop_id) γ lk R E :
     ↑flockN ⊆ E →
     is_flock γ lk -∗ ▷ R
-    ={E}=∗ ∃ s, flock_res γ s R 1.
+    ={E}=∗ ∃ s, ⌜s ∉ X⌝ ∧ flock_res γ s R 1.
   Proof.
     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.
+    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.
     { apply is_fresh. }
+    apply not_elem_of_union in Hs. destruct Hs as [Hi1 Hi2].
     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)) ]}).
@@ -156,17 +174,18 @@ Section flock.
       apply (not_elem_of_dom (to_props_map (fp ∪ from_active fa)) i (D:=gset prop_id)).
       by rewrite /to_props_map dom_fmap. }
       iDestruct "Hauth" as "[Hauth Hres]".
-      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. apply map_disjoint_insert_l_2; eauto.
-        eapply (not_elem_of_dom (D:=gset prop_id)).
-        intros Hi; apply Hs. rewrite dom_union_L elem_of_union.
-        eauto.
+      iExists i. iMod ("Hcl" with "[-Hres Hρ1 Hρ2]") as "_".
+      { iNext. iExists _,_,_. iFrame. iFrame "Hrest".
+        rewrite /all_props big_sepM_insert; last first.
+        + apply (not_elem_of_dom _ i (D:=gset prop_id)).
+          revert Hi1. rewrite dom_union_L not_elem_of_union. set_solver.
+        + iFrame "Hfp". iSplitR; last by eauto.
+          iPureIntro. apply map_disjoint_insert_l_2; eauto.
+          eapply (not_elem_of_dom (D:=gset prop_id)).
+          intros Hi; apply Hi1. rewrite dom_union_L elem_of_union.
+          eauto. }
+      iModIntro; iSplit; eauto.
+      iExists (ρ1,ρ2). iFrame "Hres Hρ1 Hρ2".
   Qed.
 
   Lemma flock_res_single_dealloc γ lk i R E :
@@ -181,7 +200,7 @@ Section flock.
       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.
+      { 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.
@@ -271,10 +290,206 @@ Section flock.
     (*     (▷ ([∗ list] (i, R, π) ∈ I, R)  *)
     (*         ={⊤}=∗ flocked γ ∅ ∗ ([∗ list] (i, R, π) ∈ I, flock_res γ i R π) }}}. *)
 
-  Lemma acquire_cancel_spec γ π lk i R :
+  Lemma extract_existential {A B C : Type} `{EqDecision A, Countable A} (I : gmap A B) (P : A -> B -> C -> iProp Σ) :
+    (([∗ map] a ↦ b ∈ I, ∃ c : C, P a b c) ⊢
+     ∃ J : gmap A (B*C), ⌜fmap fst J = I⌝ ∗ [∗ map] a ↦ bc ∈ J, P a bc.1 bc.2)%I.
+  Proof.
+    simple refine (map_ind (λ I, (([∗ map] a ↦ b ∈ I, ∃ c : C, P a b c) ⊢
+     ∃ J : gmap A (B*C), ⌜fmap fst J = I⌝ ∗ [∗ map] a ↦ bc ∈ J, P a bc.1 bc.2)) _ _ I); simpl.
+    - rewrite big_sepM_empty.
+      iIntros "_". iExists ∅. iSplit; eauto. by rewrite fmap_empty.
+    - iIntros (a b I' Ha HI') "H".
+      rewrite big_sepM_insert; auto.
+      iDestruct "H" as "[HC H]".
+      iDestruct "HC" as (c) "Habc".
+      rewrite HI'. iDestruct "H" as (J' HJ') "H".
+      iExists (<[a:=(b,c)]>J'). iSplit.
+      + iPureIntro. by rewrite fmap_insert /=HJ'.
+      + rewrite big_sepM_insert; eauto with iFrame.
+        cut (fst <$> J' !! a = None).
+        { destruct (J' !! a); eauto; inversion 1. }
+        rewrite -lookup_fmap HJ' //.
+  Qed.
+
+  Lemma big_sepM_own_frag {A B : Type} `{EqDecision A, Countable A}
+        `{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