flocked accessor

theories/lib/flock.v

@@ -374,6 +374,33 @@ Section flock.
     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