Prove the specification for cancel

theories/lib/flock.v

@@ -321,7 +321,7 @@ Section flock.
       iApply "Hcl". iNext.
       iExists Locked,fa,(delete i fp). iFrame.
       iSplit.
-      + iPureIntro. by apply map_disjoint_delete_l.
+      + iPureIntro. solve_map_disjoint.
       + rewrite to_props_map_delete delete_union.
         rewrite (delete_notin (from_active fa)) //.
         rewrite /from_active lookup_fmap Hbar //.
@@ -347,7 +347,7 @@ Section flock.
       iApply "Hcl". iNext.
       iExists Unlocked,∅,(delete i fp). iFrame.
       iSplit.
-      + iPureIntro. by apply map_disjoint_delete_l.
+      + iPureIntro. solve_map_disjoint.
       + rewrite /from_active fmap_empty /= right_id.
         by rewrite to_props_map_delete.
   Qed.
@@ -517,7 +517,7 @@ Section flock.
       { iNext. iExists Unlocked,∅,(<[i:=ρ]>fp).
         iSplitR; eauto.
         - rewrite /from_active fmap_empty. iPureIntro.
-          apply map_disjoint_empty_r.
+          solve_map_disjoint.
         - iFrame. rewrite /from_active fmap_empty right_id /=.
           rewrite map_fmap_singleton.
           assert (fp !! i = None).
@@ -590,9 +590,159 @@ Section flock.
   Lemma acquire_flock_spec γ lk (I : gmap prop_id lock_res) :
     {{{ is_flock γ lk ∗ [∗ map] i ↦ X ∈ I, flock_res γ i X }}}
       acquire lk
-    {{{ RET #();
-        ([∗ map] i ↦ X ∈ I, ▷ (res_prop X)) ∗
-        (([∗ map] i ↦ X ∈ I, ▷ (res_prop X)) ={⊤}=∗ flocked γ I) }}}.
-  Proof. Abort.
+    {{{ 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 *)
+      iAssert (own (flock_props_name γ) (● to_props_map fp) ∗
+               own (flock_props_name γ) (◯ ∅))%I
+        with "[Haprops]"
+        as "[Haprops Hemp]".
+      { admit. }
+      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.
+
+      pose (I'' := fmap res_name I).
+      assert (∃ P', P' ##ₘ I'' ∧ fp = P' ∪ I'') as [P' HP'].
+      { subst I'' I' fa. clear H1.
+        generalize dependent fp.
+        induction I as [|i X I] using map_ind; intros fp.
+        + rewrite fmap_empty.
+          exists fp. admit.
+        + rewrite fmap_insert=>Hfp.
+          specialize (IHI (delete i fp)).
+          assert ((λ X : lock_res, (res_frac X, to_agree (res_name X))) <$> I ≼ to_props_map (delete i fp)) as HLOL.
+          { (* apply lookup_included in Hfp. *)
+            admit. }
+          specialize (IHI HLOL).
+          destruct IHI as [P [HP HU]].
+          assert (P !! i = None) as HPi.
+          { admit. }
+          exists P. rewrite !fmap_insert. split.
+          * solve_map_disjoint.
+          * rewrite -insert_union_r // -HU.
+            rewrite insert_delete.
+            symmetry. apply insert_id.
+            admit. }
+      destruct HP' as [HP' ->].
+      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.
+      iApply (big_sepM_own_frag with "[] HI").
+      admit.
+  Abort.
+
+  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.