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 gset.
From iris.bi.lib Require Import fractional.

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

Instance lockstate_inhabited : Inhabited lockstate := populate Unlocked.

(** 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. *)

Record flock_name := {
  (** ghost name for the actual spin lock invariant *)
  flock_lock_name : gname;
  (** -//- for keeping the track of the state of the flock *)
  flock_state_name : gname;
  (** -//- for keeping track of all propositions in the flock *)
  flock_props_name : gname;
  (** -//- 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 *)
  flock_props_active_name : gname
}.

(* Defined as `positive` so that we have a `Fresh` instance for `gset positive`.
   Doubles as an invariant name. *)
Definition prop_id := positive.
Canonical Structure gnameC := leibnizC gname.

(** 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;
}.
Canonical Structure lock_res_nameC := leibnizC lock_res_name.

Class flockG Σ :=
  FlockG {
    flock_stateG :> inG Σ (authR (optionUR (exclR lockstateC)));
    flock_lockG  :> lockG Σ;
    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);
  }.

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 := ρ |}.

(* 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. *)

Section flock.
  Context `{heapG Σ, flockG Σ}.
  Variable N : namespace.
  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.

  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.

  Definition flock_inv (γ : flock_name) : iProp Σ :=
    (∃ (s : lockstate)
       (** fa -- active propositions, fp -- pending propositions *)
       (fa : gmap prop_id (frac * lock_res_name))
       (fp : gmap prop_id lock_res_name),
       ⌜fp ##ₘ from_active fa⌝ ∗
       own (flock_state_name γ) (● (Excl' s)) ∗
       own (flock_props_name γ) (● to_props_map (fp ∪ from_active fa)) ∗
       own (flock_props_active_name γ) (● Excl' fa) ∗
       all_tokens fp ∗
       match s with
       | Locked =>
         locked (flock_lock_name γ) ∗
         ([∗ 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' ∅)
       end)%I.

  Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
    (inv invN (flock_inv γ) ∗
     is_lock lockN (flock_lock_name γ) lk
         (own (flock_state_name γ) (◯ (Excl' Unlocked))))%I.

  (** * 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 ρ.
  Proof.
    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 -> //.
  Qed.

  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.

  (** ** 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 ρ).
  Proof.
    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".
    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].

    (* 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 ρ) ]}).
      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. }
    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.
  Qed.

  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).
  Proof.
    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")
        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 [[π ρ']|]; last done.
        symmetry in Heqfai.
        rewrite (big_sepM_lookup _ fa i (π, ρ')) //.
        (* TODO: RK, please look at this! *)
        iDestruct (own_valid_2 with "Hi Hactives") as %Hbaz.
        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 _. }
      assert (fp !! i = Some ρ) as Hbaz.
      { apply lookup_union_Some in Hfoo; last done.
        destruct Hfoo as [? | Hfoo]; first done.
        exfalso. revert Hfoo. by rewrite /from_active lookup_fmap Hbar.
      }

      iMod (own_update_2 with "Haprops Hi") as "Haprops".
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
      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. solve_map_disjoint.
      + rewrite to_props_map_delete delete_union.
        rewrite (delete_notin (from_active fa)) //.
        rewrite /from_active lookup_fmap Hbar //.
    (* Unlocked *)
    - 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 (own_valid_2 with "Haprops Hi")
        as %[Hfoo%to_props_map_singleton_included _]%auth_valid_discrete_2.
      iMod (own_update_2 with "Haprops Hi") as "Haprops".
      { apply auth_update_dealloc, (delete_singleton_local_update _ i _). }
      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. solve_map_disjoint.
      + rewrite /from_active fmap_empty /= right_id.
        by rewrite to_props_map_delete.
  Qed.

  Lemma newflock_spec :
    {{{ True }}} newlock #() {{{ lk γ, RET lk; is_flock γ lk }}}.
  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 lockN (own γ_state (◯ (Excl' Unlocked))) with "Hfrag").
    iNext. iIntros (lk γ_lock) "#Hlock".
    pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
    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. }
    iModIntro. iApply ("HΦ" $! lk γ with "[-]").
    rewrite /is_flock. by iFrame "Hlock".
  Qed.

  (** `flocked` supports invariant access just like regular invariants *)
  Lemma flocked_inv_open E i X γ I :
    ↑resN ⊆ E →
    I !! i = Some X →
    flocked γ I ={E}=∗
    ▷ (res_prop X) ∗ (▷ (res_prop X) ={E}=∗ flocked γ I).
  Proof.
    iIntros (? Hi). rewrite {1}/flocked.
    iDestruct 1 as (fa ?) "(Hst & Hfa & Htokens)".
    rewrite (big_sepM_lookup_acc _ I i X) //.
    iDestruct "Htokens" as "[(T2 & #Hinv & Hρ) Htokens]".
    iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
    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. iFrame "HR". iIntros "HR".
    iMod (cinv_open with "Hinv Hρ") as "(HC & Hρ & Hcl)"; first solve_ndisj.
    iDestruct "HC" as "[[? >T1'] | >T2]".
    { iDestruct (own_valid_2 with "T1 T1'") as %?. done. }
    iMod ("Hcl" with "[T1 HR]") as "_".
    { iNext. iLeft. iFrame. }
    iModIntro. rewrite /flocked. iExists fa.
    iFrame "Hst Hfa". iSplit; first eauto.
    iApply "Htokens". by iFrame.
  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]} }}}
      release lk
    {{{ RET #(); 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 /=.
    iDestruct "H" as (fa' Hfa) "(Hflkd & Hfactive & Hfa)".
    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]".

      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).
        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.
      }
      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' //.
  Qed.

  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 γ (◯ ∅) -∗
    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.

  Lemma own_frag_empty γ X :
    own (flock_props_name γ) (● X) ==∗
    own (flock_props_name γ) (● X) ∗ own (flock_props_name γ) (◯ ∅).
  Proof.
    iIntros "H". rewrite -own_op.
    iApply (own_update with "H").
    by apply auth_update_alloc.
  Qed.

  (* THIS IS NOT TRUE *)
  Global Instance snd_cmramorphism :
    CmraMorphism (@snd Qp (agree lock_res_name)).
  Proof.
    split; first apply _.
    - move=> n [? ?] [// ?].
    - move=> [a b]/=. admit.
  Admitted.

  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 #(); 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 *)
      iMod (own_frag_empty with "Haprops") as "[Haprops #Hemp]".

      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.

      (* TODO: RK, please take a look at this horrific script *)
      (* We are going to separate the active resources I out of the fp map *)
      pose (I'' := fmap res_name I).
      assert (∃ P', P' ##ₘ I'' ∧ fp ≡ P' ∪ I'') as [P' HP'].
      { subst I'' I' fa. clear H1.
        unfold to_props_map in *.
        pose (f := (λ X, (res_frac X, to_agree (res_name X)))).
        pose (g := (λ X:lock_res_name, (1%Qp, to_agree X))).
        (* Proof idea:
          f <$> I ≼ g <$> fp
             implies
          snd <$> f <$> I ≼ snd <$> g <$> fp
          =  to_agree o res_name <$> I ≼ to_agree <$> fp *)
        assert (((snd <$> (f <$> I)) : gmapUR prop_id (agreeR lock_res_nameC)) ≼ (snd <$> (g <$> fp))) as Hbar.
        { (* TODO: this is the /proper/ proof of the statement, but
             the proof is incorrect because currently projections are
             not morphisms *)
          eapply cmra_morphism_monotone; last exact: Hfoo.
          apply gmap_fmap_cmra_morphism. apply _.
        }
        rewrite -!map_fmap_compose in Hbar.
        assert ((to_agree ∘ res_name <$> I) ≼ to_agree <$> fp) as Hbaz by exact: Hbar.
        rewrite map_fmap_compose in Hbaz.

        (* which implies the following *)
        assert (∀ i, to_agree <$> (res_name <$> (I !! i)) ≼ to_agree <$> (fp !! i)) as Hbork.
        { intros i. rewrite -!lookup_fmap. revert i.
          apply lookup_included. exact: Hbaz. }
        clear Hbaz Hbar Hfoo.

        generalize dependent fp.
        induction I as [|i X I HI IHI] using map_ind; intros fp.
        + rewrite fmap_empty.
          exists fp. rewrite right_id.
          split; first solve_map_disjoint; auto.
        + rewrite fmap_insert=>Hfp.
          specialize (IHI (delete i fp)).
          assert (∀ j, to_agree <$> (res_name <$> I !! j)
                         ≼ (to_agree <$> delete i fp !! j)) as goodboi.
          { intros j.
            destruct (decide (i = j)) as [<-|?].
            - by rewrite HI lookup_delete.
            - specialize (Hfp j).
              rewrite lookup_insert_ne in Hfp; last done.
              rewrite lookup_delete_ne //. }
          specialize (IHI goodboi). clear goodboi.
          destruct IHI as [P [HP HU]].
          assert (P !! i = None) as HPi.
          { destruct (P !! i) as [Y|] eqn:HPi; auto; simplify_eq/=.
            exfalso. unfold_leibniz.
            specialize (HU i). fold_leibniz.
            rewrite (lookup_union_Some_l _ _ _ _ HPi) in HU.
            rewrite lookup_delete in HU. done. }
          exists P. split; first solve_map_disjoint.
          rewrite -insert_union_r // -HU.
          rewrite insert_delete=> j.
          specialize (Hfp j).
          destruct (decide (i = j)) as [<-|?].
          * revert Hfp. rewrite !lookup_insert.
            intros Hfp.
            destruct (proj1( option_included _ _) Hfp)
              as [?|(a&?&Ha&Hj&Heq)]; simplify_eq/=.
            destruct (fp !! i) as [Y|] eqn:HY; simplify_eq/=.
            revert Heq. rewrite to_agree_included HY.
            intros [->%to_agree_inj | ->]; reflexivity.
          * rewrite lookup_insert_ne //. }
      fold_leibniz.

      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 "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.