(** Cancellable locks *)
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock.
From iris.base_logic.lib Require Import cancelable_invariants auth saved_prop.
From iris.algebra Require Import auth agree excl frac gmap.
From iris.bi.lib Require Import fractional.

Inductive lockstate :=
  | Locked : frac → lockstate
  | Unlocked.
Canonical Structure lockstateC := leibnizC lockstate.

Instance lockstate_inhabited : Inhabited lockstate := populate Unlocked.

Record flock_name := {
  flock_lock_name : gname;
  flock_cinv_name : gname;
  flock_state_name : gname;
  flock_props_name : gname;
  flock_props_active_name : gname
}.

(* positive so that we have a `Fresh` instance for `gset positive` *)
Definition prop_id := positive.

Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
    flock_cinvG  :> cinvG Σ;
    flock_lockG  :> lockG Σ;
    flock_props :> authG Σ (optionUR (exclR (gmapC prop_id (iProp Σ))));
    flock_props_activeG :> authG Σ (gmapUR prop_id (agreeR (iProp Σ)))
  }.

Section cinv_lemmas.
  Context `{invG Σ, cinvG Σ}.

  Lemma cinv_alloc_strong (G : gset gname) E N (Φ : gname → iProp Σ) :
    ▷ (∀ γ, ⌜γ ∉ G⌝ → Φ γ) ={E}=∗ ∃ γ, ⌜γ ∉ G⌝ ∧ cinv N γ (Φ γ) ∗ cinv_own γ 1.
  Proof.
    iIntros "HP".
    iMod (own_alloc_strong 1%Qp G) as (γ) "[% H1]"; first done.
    iMod (inv_alloc N _ (Φ γ ∨ own γ 1%Qp)%I with "[HP]") as "#Hinv".
    - iNext. iLeft. by iApply "HP".
    - iExists γ. iModIntro. rewrite /cinv /cinv_own. iFrame "H1".
      iSplit; eauto. iExists _. iFrame "Hinv".
      iIntros "!# !>". iSplit; by iIntros "?".
  Qed.

  Lemma cinv_cancel_vs (P Q : iProp Σ) E N γ :
    ↑N ⊆ E → cinv N γ P
    -∗ (cinv_own γ 1 ∗ ▷ P ={E∖↑N}=∗ cinv_own γ 1 ∗ ▷ Q)
    -∗ cinv_own γ 1 ={E}=∗ ▷ Q.
  Proof.
    iIntros (?) "#Hinv Hvs Hγ". rewrite /cinv.
    iDestruct "Hinv" as (P') "[#HP' Hinv]".
    iInv N as "[HP|>Hγ']" "Hclose"; last first.
    - iDestruct (cinv_own_1_l with "Hγ Hγ'") as %[].
    - iMod ("Hvs" with "[$Hγ HP]") as "[Hγ HQ]".
      { by iApply "HP'". }
      iFrame. iApply "Hclose". iNext. by iRight.
  Qed.

End cinv_lemmas.

Section flock.
  Context `{heapG Σ, flockG Σ}.

  Variable N : namespace.
  Definition flockN := N.@"flock".

  Definition to_props_map (f : gmap prop_id (iProp Σ))
    : gmapUR prop_id (agreeR (iProp Σ)) := to_agree <$> f.

  Definition all_props (f : gmap prop_id (iProp Σ)) : iProp Σ :=
    ([∗ map] i ↦ R ∈ f, R)%I.

  Definition flock_inv (γ : flock_name) : iProp Σ :=
    (∃ (s : lockstate) (fp fa : gmap prop_id (iProp Σ)),
       (** fa -- active propositions, fp -- inactive propositions *)
       own (flock_state_name γ) (● (Excl' s)) ∗
       own (flock_props_name γ) (● to_props_map (fp ∪ fa)) ∗
       own (flock_props_active_name γ) (◯ Excl' fa) ∗
       match s with
       | Locked q =>
         cinv_own (flock_cinv_name γ) (q/2) ∗
         locked (flock_lock_name γ) ∗
         all_props fp
       | Unlocked => own (flock_props_active_name γ) (● Excl' fa) ∗
                     all_props fa ∗
                     ⌜fp = ∅⌝ (** all the propositions are active *)
       end)%I.

  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
    (cinv (flockN .@ "inv") (flock_cinv_name γ) (flock_inv γ) ∗
     is_lock (flockN .@ "lock") (flock_lock_name γ) lk
         (own (flock_state_name γ) (◯ (Excl' Unlocked))))%I.

  Definition unflocked (γ : flock_name) (q : frac) : iProp Σ :=
    cinv_own (flock_cinv_name γ) q.

  Definition flocked
    (γ : flock_name) (q : frac) (f : gmap prop_id (iProp Σ)) : iProp Σ :=
    (own (flock_state_name γ) (◯ (Excl' (Locked q)))
     ∗ cinv_own (flock_cinv_name γ) (q/2)
     ∗ own (flock_props_active_name γ) (● Excl' f)
     ∗ ▷ all_props f)%I.

  Definition flock_res (γ : flock_name) (R : iProp Σ) : iProp Σ :=
    (∃ f, ⌜R ≡ all_props f⌝ ∧ own (flock_props_name γ) (◯ to_props_map f))%I.

  Definition flock_res_single (γ : flock_name) (s : prop_id) (R : iProp Σ) : iProp Σ :=
    (own (flock_props_name γ) (◯ {[ s := to_agree R ]}))%I.

  (** **************************************** *)
  (** to_props_map lemmas *)
  Lemma to_props_map_insert f i P :
    to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f).
  Proof. by rewrite /to_props_map fmap_insert. Qed.

  Lemma to_props_map_lookup f i :
    to_props_map f !! i = to_agree <$> f !! i.
  Proof. by rewrite /to_props_map lookup_fmap. Qed.

  Lemma to_props_map_dom f :
    dom (gset prop_id) (to_props_map f) = dom (gset prop_id) f.
  Proof. by rewrite /to_props_map dom_fmap_L. Qed.

  Lemma to_props_map_singleton s R : to_props_map {[s := R]} = {[s := to_agree R]}.
  Proof. by rewrite /to_props_map map_fmap_singleton. Qed.

  (** all_props lemmas *)
  Lemma all_props_empty : all_props ∅.
  Proof. by rewrite /all_props big_sepM_empty. Qed.

  Lemma all_props_singleton s R : all_props {[s := R]} ≡ R.
  Proof. by rewrite /all_props big_sepM_singleton. Qed.

  Lemma all_props_insert s (R : iProp Σ) f :
    f !! s = None →
    all_props (<[s := R]>f) ≡ (R ∗ all_props f)%I.
  Proof. intros ?. rewrite /all_props big_sepM_insert //. Qed.

  Lemma all_props_union f g :
    all_props f ∗ all_props g ⊢ all_props (f ∪ g).
  Proof.
    revert g.
    simple refine (map_ind (fun f => ∀ g, all_props f ∗ all_props g -∗ all_props (f ∪ g)) _ _ f); simpl; rewrite /all_props.
    - intros g. by rewrite big_sepM_empty !left_id.
    - intros i P f' Hi IH.
      intros g. rewrite big_sepM_insert; last done.
      iIntros "[[HP Hf] Hg]".
      rewrite -insert_union_l.
      remember (g !! i) as Z. destruct Z as [R|].
      + assert (g = <[i:=R]>(delete i g)) as Hfoo.
        { rewrite insert_delete insert_id; eauto. }
        rewrite {1}Hfoo.
        rewrite big_sepM_insert; last first.
        { apply lookup_delete. }
        iDestruct "Hg" as "[HR Hg]".
        iApply (big_sepM_insert_override_2 _ _ i R P with "[-HP] [HP]"); simpl.
        { apply lookup_union_Some_raw. right. eauto. }
        * iApply (IH g).
          rewrite Hfoo big_sepM_insert; last by apply lookup_delete.
          rewrite delete_insert; last by apply lookup_delete. iFrame.
        * eauto.
      + rewrite big_sepM_insert; last first.
        { apply lookup_union_None. eauto. }
        iFrame. iApply (IH g). iFrame.
  Qed.

  Global Instance all_props_proper : Proper ((≡) ==> (≡))
    (all_props : gmapC prop_id (iProp Σ) → iProp Σ).
  Proof.
    intros f. rewrite /all_props. (* rewrite /all_props /big_opM. *)
    simple refine (map_ind (fun f => ∀ g, f ≡ g → _ ≡ _) _ _ f); simpl.
    - intros g. rewrite big_sepM_empty.
      simple refine (map_ind (fun g => ∅ ≡ g → _ ≡ _) _ _ g); simpl.
      + by rewrite big_sepM_empty.
      + intros j R g' Hj IH Hg'.
        exfalso. specialize (Hg' j). revert Hg'.
        rewrite lookup_insert lookup_empty. inversion 1.
    - intros i P f' Hi IH g Hf'.
      rewrite big_sepM_insert; last done.
      specialize (IH (delete i g)).
      assert (f' ≡ delete i g) as Hf'g.
      { by rewrite -Hf' delete_insert. }
      specialize (IH Hf'g). rewrite IH.
      assert (∃ R, g !! i = Some R ∧ P ≡ R) as [R [Hg HR]].
      { specialize (Hf' i).
        destruct (g !! i) as [R|]; last first.
        - exfalso. revert Hf'. rewrite lookup_insert. inversion 1.
        - exists R. split; auto.
          revert Hf'. rewrite lookup_insert. by inversion 1. }
      rewrite (big_sepM_delete _ g i R); eauto.
      by apply bi.sep_proper.
  Qed.

  (** **************************************** *)
  (** rules & properties of the predicates *)
  Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk).
  Proof. apply _. Qed.

  Global Instance flock_res_persistent γ R : Persistent (flock_res γ R).
  Proof. apply _. Qed.

  Global Instance flock_res_single_persistent γ s R : Persistent (flock_res_single γ s R).
  Proof. apply _. Qed.

  Global Instance flock_res_proper : Proper ((=) ==> (≡) ==> (≡)) flock_res.
  Proof.
    intros ? γ -> P R HPR. rewrite /flock_res.
    apply bi.exist_proper=>f. by rewrite HPR.
  Qed.

  Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
    unflocked γ (π1+π2) ⊣⊢ unflocked γ π1 ∗ unflocked γ π2.
  Proof. by rewrite /unflocked fractional. Qed.

  Global Instance unflocked_fractional γ : Fractional (unflocked γ).
  Proof. intros p q. apply unflocked_op. Qed.

  Global Instance unflocked_as_fractional γ π :
    AsFractional (unflocked γ π) (unflocked γ) π.
  Proof. split. done. apply _. Qed.

  Lemma flock_res_single_alloc_unflocked (X : gset prop_id) γ lk π R E :
    ↑flockN ⊆ E →
    is_flock γ lk -∗ unflocked γ π -∗ ▷ R
    ={E}=∗ ∃ s, ⌜s ∉ X⌝ ∗ flock_res_single γ s R ∗ unflocked γ π.
  Proof.
    iIntros (?) "Hl Hunfl HR". rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first solve_ndisj.
    rewrite {2}/flock_inv.
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
      pose (s := (fresh ((dom (gset prop_id) (fp ∪ fa)) ∪ X))).
      assert (s ∉ (dom (gset prop_id) (fp ∪ fa))) as Hs.
      { intros Hs.
        apply (elem_of_union_l s (dom (gset prop_id) (fp ∪ fa)) X) in Hs.
        revert Hs. apply is_fresh. }
      iMod (own_update  with "Hauth") as "Hauth".
      { apply (auth_update_alloc _ (to_props_map (<[s := R]> fp ∪ fa))
                                 {[ s := to_agree R ]}).
        rewrite -insert_union_l.
        rewrite to_props_map_insert.
        apply alloc_local_update; last done.
        apply (not_elem_of_dom (to_props_map (fp ∪ fa)) s (D:=gset prop_id)).
        rewrite to_props_map_dom. done. }
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,_,_. iFrame. iFrame "Hcown Hlocked2".
        iApply all_props_insert; last iFrame.
        apply (not_elem_of_dom _ s (D:=gset prop_id)).
        revert Hs. rewrite dom_union_L not_elem_of_union. set_solver. }
      iModIntro. iPureIntro.
      clear Hs. intros Hs.
      apply (elem_of_union_r s (dom (gset prop_id) (fp ∪ fa)) X) in Hs.
      revert Hs. apply is_fresh.
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
      pose (s := (fresh (dom (gset prop_id) fa ∪ X))).
      assert (s ∉ (dom (gset prop_id) fa)) as Hs.
      { intros Hs.
        apply (elem_of_union_l s _ X) in Hs.
        revert Hs. apply is_fresh. }
      iMod (own_update  with "Hauth") as "Hauth".
      { apply (auth_update_alloc _ (to_props_map (<[s := R]> fa))
                                 {[ s := to_agree R ]}).
        rewrite to_props_map_insert.
        apply alloc_local_update; last done.
        apply (not_elem_of_dom (to_props_map fa) s (D:=gset prop_id)).
        rewrite to_props_map_dom. done. }
      iDestruct "Hauth" as "[Hauth Hres]".
      iExists s. iFrame "Hres Hunfl".
      iMod (own_update_2 _ _ _ ((● Excl' (<[s:=R]>fa)) ⋅ (◯ Excl' (<[s:=R]>fa)))
              with "Hactive Hfactive") as "[Hactive Hfactive]".
      { by apply auth_update, option_local_update, exclusive_local_update. }
      iMod ("Hcl" with "[-]") as "_".
      { iNext. iExists _,∅,_. rewrite left_id. iFrame. iFrame "Hactive".
        iSplit; auto.
        iApply all_props_insert; last by iFrame.
        by apply (not_elem_of_dom _ s (D:=gset prop_id)). }
      iModIntro. iPureIntro.
      clear Hs. intros Hs.
      apply (elem_of_union_r s (dom (gset prop_id) fa) X) in Hs.
      revert Hs. apply is_fresh.
  Qed.

  Lemma flock_res_alloc_unflocked γ lk π R E :
    ↑flockN ⊆ E →
    is_flock γ lk -∗ unflocked γ π -∗ ▷ R
    ={E}=∗ flock_res γ R ∗ unflocked γ π.
  Proof.
    iIntros (?) "#Hlk Hunfl HR".
    iMod (flock_res_single_alloc_unflocked ∅ with "Hlk Hunfl HR")
      as (s ?) "[HR $]"; first done.
    iModIntro. iExists {[s := R]}.
    rewrite /flock_res_single to_props_map_singleton. iFrame "HR".
    iPureIntro. symmetry. apply all_props_singleton.
  Qed.

  Lemma flock_res_insert_unflocked γ lk π P R E :
    ↑flockN ⊆ E →
    is_flock γ lk -∗ flock_res γ P -∗ unflocked γ π -∗ ▷ R
    ={E}=∗ flock_res γ (P∗R) ∗ unflocked γ π.
  Proof.
    iIntros (?) "#Hlk #Hres Hunfl HR".
    iDestruct "Hres" as (f Hfeq) "Hf".
    iMod (flock_res_single_alloc_unflocked (dom (gset prop_id) f)
            with "Hlk Hunfl HR") as (s Hs) "[HR $]"; first done.
    iModIntro. iExists (<[s := R]>f).
    rewrite to_props_map_insert /flock_res_single.
    iCombine "HR Hf" as "HR".
    (* TODO this should be a lemma, somewhere in std++ *)
    rewrite /op /cmra_op /= /ucmra_op /= /gmap_op /=.
    assert ((merge op {[s := to_agree R]} (to_props_map f))
            = <[s:=to_agree R]> (to_props_map f)) as Hmerge.
    { apply map_eq=>i. rewrite lookup_merge.
      destruct (decide (s = i)) as [->|?].
      - rewrite lookup_singleton lookup_insert.
        rewrite to_props_map_lookup.
        assert (f !! i = None) as ->.
        + by rewrite -(not_elem_of_dom (D:=(gset prop_id))).
        + simpl. done.
      - rewrite lookup_singleton_ne; auto.
        rewrite lookup_insert_ne; auto.
        remember (to_props_map f !! i) as o. rewrite -Heqo.
        by destruct o. }
    rewrite Hmerge. iFrame "HR".
    iPureIntro. rewrite all_props_insert.
    - by rewrite comm Hfeq.
    - by apply (not_elem_of_dom (D:=gset prop_id)).
  Qed.

  Lemma newlock_cancel_spec :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk ∗ unflocked γ 1 }}}.
  Proof.
    iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
    iMod (own_alloc (● (Excl' Unlocked) ⋅ ◯ (Excl' Unlocked)))
      as (γ_state) "[Hauth Hfrag]"; first done.
    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. }
    iApply (newlock_spec (flockN.@"lock") (own γ_state (◯ (Excl' Unlocked))) with "Hfrag").
    iNext. iIntros (lk γ_lock) "#Hlock".
    iMod (cinv_alloc_strong ∅ _ (flockN.@"inv")
       (fun γ => flock_inv (Build_flock_name γ_lock γ γ_state γ_props γ_ac_props)) with "[-HΦ]") as (γ_cinv) "(_ & #Hcinv & Hown)".
    { iNext. rewrite /flock_inv /=. iIntros (γ _).
      iExists Unlocked, ∅, ∅. rewrite left_id. iFrame.
      iSplit; auto. iApply all_props_empty. }
    pose (γ := (Build_flock_name γ_lock γ_cinv γ_state γ_props γ_ac_props)).
    iModIntro. iApply ("HΦ" $! lk γ with "[-]"). iFrame "Hown".
    rewrite /is_flock. by iFrame "Hlock".
  Qed.

  Lemma flock_res_auth γ R fp :
    flock_res γ R -∗
    own (flock_props_name γ) (● to_props_map fp) -∗
    ⌜∃ f', all_props fp ⊣⊢ R ∗ all_props f'⌝.
  Proof.
    rewrite /flock_res. iDestruct 1 as (f Heq) "#Hf".
    iIntros "Hauth".
    iDestruct (own_valid_2 with "Hauth Hf")
      as %[Hfoo _]%auth_valid_discrete.
    iPureIntro. revert Hfoo. simpl. rewrite left_id.
    rewrite lookup_included. intros Hffp.
    exists (fp ∖ f). rewrite Heq. clear Heq. revert Hffp.
    simple refine (map_ind (fun f => (∀ i, _) → _ ≡ _) _ _ f); simpl.
    - (* TODO: this should be somewhere in std++ *)
      assert (fp ∖ ∅ = fp) as ->.
      { apply map_eq=>i. remember (fp !! i) as XX. destruct XX.
        - apply lookup_difference_Some. eauto.
        - apply lookup_difference_None. eauto. }
      intros _. iSplit; [iIntros "$" | iIntros "[_ $]"].
      iApply all_props_empty.
    - intros i P f' Hi IH Hffp. rewrite IH; last first.
      { intros j. specialize (Hffp j).
        destruct (decide (i = j)) as [->|?].
        - rewrite !to_props_map_lookup Hi. simpl.
          apply option_included. eauto.
        - revert Hffp.
          rewrite !to_props_map_lookup lookup_insert_ne; auto. }
      rewrite all_props_insert; last assumption.
      specialize (Hffp i). revert Hffp.
      rewrite !to_props_map_lookup lookup_insert; auto. simpl.
      rewrite option_included.
      intros [Hffp | [? [Q' [HP [HQ HeqQ]]]]]; first by inversion Hffp.
      simplify_eq/=. remember (fp !! i) as XX.
      destruct XX as [Q|]; simpl in HQ; last first.
      { inversion HQ. }
      simplify_eq/=.
      assert (P ≡ Q) as HPQ.
      { by destruct HeqQ as [?%to_agree_inj |?%to_agree_included]. }
      clear HeqQ.
      assert (fp = <[i:=Q]>(delete i fp)) as ->.
      { by rewrite insert_delete insert_id. }
      assert (<[i:=Q]> (delete i fp) ∖ f' = <[i:=Q]>((delete i fp) ∖ f')) as ->.
      { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
        - by rewrite lookup_insert lookup_difference_Some lookup_insert.
        - rewrite lookup_insert_ne; auto.
          unfold difference, map_difference; rewrite !lookup_difference_with.
          rewrite lookup_insert_ne; auto. }
      rewrite all_props_insert; last first.
      { apply lookup_difference_None. left. apply lookup_delete. }
      assert ((<[i:=Q]> (delete i fp) ∖ <[i:=P]> f') = (delete i fp ∖ f')) as ->.
      { apply map_eq=>j. destruct (decide (i = j)) as [->|?].
        - unfold difference, map_difference; rewrite !lookup_difference_with.
            by rewrite !lookup_insert lookup_delete Hi.
        - unfold difference, map_difference; rewrite !lookup_difference_with.
          rewrite !lookup_insert_ne; auto. }
      iSplit; rewrite {1}HPQ. iIntros "($ & $ & $)".
      iIntros "[[$ $] $]".
  Qed.

  Lemma acquire_cancel_spec γ π lk R :
    {{{ is_flock γ lk ∗ unflocked γ π ∗ flock_res γ R }}}
      acquire lk
    {{{ f, RET #(); ▷ R ∗ (▷ R -∗ flocked γ π f) }}}.
  Proof.
    iIntros (Φ) "(Hl & Hunfl & #HRres) HΦ". rewrite -wp_fupd.
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iApply (acquire_spec with "Hlk"). iNext.
    iIntros "[Hlocked Hunlk]".
    iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown & >Hlocked2 & Hfp)".
      iExFalso. iApply (locked_exclusive with "Hlocked Hlocked2").
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. rewrite left_id.
      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 "Hunfl" as "[Hunfl Hcown]".
      iDestruct (flock_res_auth with "HRres Hauth") as %Hfoo.
      destruct Hfoo as [f' Hf'].
      iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]") as "_".
      { iNext. iExists (Locked π),∅,fa. rewrite left_id. iFrame.
        iApply all_props_empty. }
      iModIntro. rewrite Hf'. iDestruct "Hfa" as "[HR Hf']".
      iApply ("HΦ" $! fa). iFrame.
      iApply bi.later_wand. iNext. iIntros "HR".
      rewrite Hf'. iFrame.
  Qed.

  (* TODO: derive this from acquire_cancel_spec *)
  Lemma acquire_single_cancel_spec γ π lk s R :
    {{{ is_flock γ lk ∗ unflocked γ π ∗ flock_res_single γ s R }}}
      acquire lk
    {{{ f, RET #(); ▷ R ∗ (▷ R -∗ flocked γ π f) }}}.
  Proof.
    iIntros (Φ) "(Hl & Hunfl & Hres) HΦ".
    rewrite /flock_res_single.
    iApply (acquire_cancel_spec with "[$Hl $Hunfl Hres]"); last done.
    iExists {[s := R]}.
    rewrite to_props_map_singleton all_props_singleton. eauto.
  Qed.

  Lemma release_cancel_spec γ π lk f :
    {{{ is_flock γ lk ∗ flocked γ π f }}}
      release lk
    {{{ RET #(); unflocked γ π }}}.
  Proof.
    iIntros (Φ) "(Hl & (Hstate' & Hflkd & Hactive & Hf)) HΦ". rewrite -fupd_wp.
    rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)".
    iMod (cinv_open with "Hcinv Hflkd") as "(Hstate & Hunfl & Hcl)"; first done.
    rewrite {2}/flock_inv.
    iDestruct "Hstate" as ([q|] fp fa) "(>Hstate & >Hauth & >Hfactive & Hrest)"; last first.
    - iDestruct "Hrest" as "(>Hactive2 & Hfa & >%)".
      iExFalso. iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
      iPureIntro. revert Hfoo.
      rewrite auth_valid_discrete /= left_id.
      intros [Hexcl _].
      apply Some_included_exclusive in Hexcl; try (done || apply _).
      simplify_eq.
    - iDestruct "Hrest" as "(>Hcown & >Hlocked & Hfp)".
      iAssert (⌜q = π⌝)%I with "[Hstate Hstate']" as  %->.
      { iDestruct (own_valid_2 with "Hstate Hstate'") as %Hfoo.
        iPureIntro. revert Hfoo.
        rewrite auth_valid_discrete /= left_id.
        intros [Hexcl _].
        apply Some_included_exclusive in Hexcl; try (done || apply _).
        by simplify_eq. }
      iMod (own_update_2 with "Hstate Hstate'") as "Hstate".
      { apply (auth_update _ _ (Excl' Unlocked) (Excl' Unlocked)).
        apply option_local_update.
        by apply exclusive_local_update. }
      iDestruct "Hstate" as "[Hstate Hstate']".
      iAssert (⌜(f : gmapC prop_id (iProp Σ)) ≡ fa⌝%I) with "[Hactive Hfactive]" as %Hfoo.
      { iDestruct (own_valid_2 with "Hactive Hfactive") as %Hfoo.
        iPureIntro. apply auth_valid_discrete_2 in Hfoo.
        destruct Hfoo as [Hfoo _].
        apply Some_included_exclusive in Hfoo; [|apply _|done].
        by apply Excl_inj. }
      rewrite {1}Hfoo.
      iMod (own_update_2 _ _ _ (● Excl' (fp ∪ fa) ⋅ ◯ Excl' (fp ∪ fa))
              with "Hactive Hfactive") as "[Hactive Hfactive]".
      { by apply auth_update, option_local_update, exclusive_local_update. }
      iMod ("Hcl" with "[Hstate Hauth Hfp Hf Hactive Hfactive]").
      { iNext. iExists Unlocked,∅,(fp∪fa). rewrite left_id. iFrame.
        rewrite Hfoo. iSplit; eauto.
        iApply all_props_union; iFrame. }
      iApply (release_spec with "[$Hlk $Hlocked $Hstate']").
      iModIntro. iNext. iIntros "_". iApply "HΦ".
      rewrite /unflocked. by iSplitL "Hcown".
  Qed.

  Lemma cancel_lock γ lk R E :
    ↑flockN ⊆ E →
    is_flock γ lk -∗ flock_res γ R -∗ unflocked γ 1 ={E}=∗ ▷ R.
  Proof.
    rewrite /is_flock /unflocked =>?.
    iDestruct 1 as "(#Hcinv & #Hislock)".
    iIntros "#Hres Hcown".
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; first solve_ndisj; eauto.
    iIntros "[Hcown Hstate]".
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. iFrame. rewrite left_id.
      iDestruct (flock_res_auth with "Hres Hauth") as %Hfoo.
      destruct Hfoo as [f' Hf'].
      iModIntro. rewrite Hf'. iDestruct "Hfa" as "[$ ?]".
  Qed.

  Lemma cancel_lock_single γ lk s R E :
    ↑flockN ⊆ E →
    is_flock γ lk -∗ flock_res_single γ s R -∗ unflocked γ 1 ={E}=∗ ▷ R.
  Proof.
    rewrite /is_flock /unflocked.
    iDestruct 1 as "(#Hcinv & #Hislock)". iIntros "#Hres Hcown".
    rewrite /flock_res.
    iMod (cinv_cancel_vs _ R with "Hcinv [] Hcown") as "$"; first solve_ndisj; eauto.
    iIntros "[Hcown Hstate]".
    iDestruct "Hstate" as ([q|] fp fa) "(Hstate & >Hauth & Hfactive & Hrest)".
    - iDestruct "Hrest" as "(>Hcown2 & >Hlocked & Hfp)".
      iDestruct (cinv_own_1_l with "Hcown Hcown2") as %[].
    - iDestruct "Hrest" as "(>Hactive & Hfa & >%)".
      simplify_eq/=. iFrame. rewrite left_id.
      iAssert (∃ R', ⌜R ≡ R' ∧ fa !! s = Some R'⌝)%I
        with "[Hres Hauth]" as %Hfoo.
      { iDestruct (own_valid_2 with "Hauth Hres")
          as %[Hfoo _]%auth_valid_discrete.
        iPureIntro. revert Hfoo.
        rewrite /= left_id singleton_included=> -[R' [Hf HR]].
        revert Hf HR.
        rewrite to_props_map_lookup fmap_Some_equiv=>-[R'' [/= Hf ->]].
        intros [?%to_agree_inj | ?%to_agree_included]%Some_included;
          simplify_eq/=; exists R''; eauto. }
      destruct Hfoo as [R' [HReq Hf]].
      rewrite /all_props {1}(big_sepM_lookup_acc _ fa s R'); last done.
      iDestruct "Hfa" as "[HR' Hfa]".
      assert ((▷ R)%I ≡ (▷ R')%I) as ->. by apply bi.later_proper.
      by iFrame.
  Qed.
End flock.