Clean up flock.v a bit

theories/c_translation/monad.v

@@ -230,7 +230,7 @@ Section a_wp_rules.
       iDestruct ("HR" with "HQ") as "[HR HΦ]".
       iMod ("Hcl" with "[HR Henv]") as "Hflocked".
       { iNext. iRewrite "Heq1". iFrame. }
-      wp_apply (release_cancel_spec' with "[$Hlock1 $Hflocked]").
+      wp_apply (release_cancel_spec with "[$Hlock1 $Hflocked]").
       iIntros "$". wp_pures. iFrame.
   Qed.
 
@@ -252,7 +252,7 @@ Section a_wp_rules.
     iIntros (w) "[Henv [HR HΦ]]". wp_pures.
     iRewrite "Heq" in "Hcl".
     iMod ("Hcl" with "[$HR $Henv]") as "Hflocked".
-    wp_apply (release_cancel_spec' with "[$Hlock $Hflocked]").
+    wp_apply (release_cancel_spec with "[$Hlock $Hflocked]").
     iIntros "$". wp_pures. iFrame.
   Qed.
 

theories/lib/flock.v

@@ -276,7 +276,8 @@ Section flock.
     by rewrite /to_props_map fmap_delete.
   Qed.
 
-  (** ** Spectral and physical operations *)
+  (** ** Spectral operations *)
+
   Lemma flock_res_alloc_strong (X : gset prop_id) γ lk R E :
     ↑N ⊆ E →
     is_flock γ lk -∗
@@ -474,6 +475,7 @@ Section flock.
       iModIntro. by iFrame.
   Qed.
 
+  (** ** Physical operations *)
   Lemma newflock_spec :
     {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
   Proof.
@@ -496,89 +498,19 @@ Section flock.
     rewrite /is_flock. by iFrame "Hlock".
   Qed.
 
-  Lemma acquire_flock_single_spec γ lk i X :
-    {{{ is_flock γ lk ∗ flock_res γ i X }}}
-      acquire lk
-    {{{ RET #(); ▷ (res_prop X) ∗ (▷ (res_prop X) ={⊤}=∗ flocked γ {[i:=X]}) }}}.
-  Proof.
-    destruct X as [R π ρ].
-    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.
-      iDestruct "HRres" as "(Hi & #Hinv & Hρ)".
-
-      (* 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]".
-
-      (* (i,ρ) ∈ fp *)
-      iDestruct (own_valid_2 with "Haprops Hi")
-        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
-
-      (* move (i,ρ) to the set of active propositions *)
-      rewrite /all_tokens (big_sepM_delete _ fp i ρ) //.
-      iDestruct "Htokens" as "[T2 Htokens]".
-
-      iMod (own_update_2 with "Haactive Hfactive") as "[Haactive Hfactive]".
-      { apply (auth_update _ _ (Excl' {[ i := (π, ρ) ]})
-                               (Excl' {[ i := (π, ρ) ]})).
-        by apply option_local_update, exclusive_local_update. }
-
-      iMod ("Hcl" with "[Haactive Hi Hlocked Haprops Htokens Hstate]") as "_".
-      { iNext. iExists Locked,{[i := (π, ρ)]},(delete i fp).
-        iFrame. iSplitR ; [ | iSplitL "Haprops"].
-        - iPureIntro.
-          rewrite /from_active map_fmap_singleton /=.
-          apply map_disjoint_singleton_r, lookup_delete.
-        - rewrite /from_active map_fmap_singleton /=.
-          rewrite -insert_union_singleton_r.
-          2: { apply lookup_delete. }
-          rewrite insert_delete insert_id //.
-        - rewrite /all_tokens big_sepM_singleton //. }
-      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 //.
-  Qed.
-
-  Lemma release_cancel_spec γ lk i X :
-    {{{ is_flock γ lk ∗ flocked γ {[i:=X]} }}}
+  Lemma release_cancel_spec γ lk I :
+    {{{ is_flock γ lk ∗ flocked γ I }}}
       release lk
-    {{{ RET #(); flock_res γ i X }}}.
+    {{{ 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)".
 
-    destruct X as [R π ρ]. rewrite /flocked /=.
+    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.
@@ -597,60 +529,32 @@ Section flock.
         by apply exclusive_local_update. }
       iDestruct "Hstate" as "[Hstate Hunflkd]".
 
-      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).
+      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 /=.
-          rewrite map_fmap_singleton.
-          assert (fp !! i = None).
-          { eapply map_disjoint_Some_r; first eassumption.
-            rewrite /from_active !map_fmap_singleton.
-            by rewrite lookup_singleton. }
-          rewrite -insert_union_singleton_r // /=. iFrame.
-          rewrite /all_tokens big_sepM_insert //.
-          iFrame.
-      }
+          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Φ".
-      by iFrame.
-  Qed.
-
-  (** 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' //.
+      rewrite /flock_res !big_sepM_sepM.
+      iFrame "Hρs Hinvs".
+      rewrite big_sepM_fmap. iFrame.
   Qed.
 
+  (** For the acquire we need two additional lemmas, and they are annoying! *)
   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 γ (◯ ∅) -∗
@@ -833,60 +737,4 @@ Section flock.
       iApply (big_sepM_own_frag with "Hemp HI").
   Qed.
 
-  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.
-
 End flock.