diff --git a/theories/lib/flock.v b/theories/lib/flock.v index 2338a259f28cadd84af1c61b8600062ada4d22e2..533272179af19ea9ab0294d62074e3a3cf973d2d 100644 --- a/theories/lib/flock.v +++ b/theories/lib/flock.v @@ -72,16 +72,63 @@ Section 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. + 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. - Definition all_props (f : gmap prop_id (iProp Σ)) : iProp Σ := - ([∗ map] i ↦ R ∈ f, R)%I. + 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. + + Lemma all_props_singleton s R : all_props {[s := R]} ≡ R. + Proof. by rewrite /all_props bi.big_sepM_singleton. Qed. Lemma all_props_union f g : all_props f ∗ all_props g ⊢ all_props (f ∪ g). @@ -138,33 +185,6 @@ Section flock. by apply bi.sep_proper. Qed. - 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 = ∅⌝ - 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 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. - Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk). Proof. apply _. Qed. @@ -180,22 +200,13 @@ Section flock. apply bi.exist_proper=>f. by rewrite HPR. Qed. - 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. - 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. @@ -269,7 +280,7 @@ Section flock. iIntros "#Hlk Hunfl HR". iMod (flock_res_single_alloc_unflocked ∅ with "Hlk Hunfl HR") as (s ?) "[HR $]". iModIntro. iExists {[s := R]}. - rewrite /flock_res_single /to_props_map map_fmap_singleton. iFrame "HR". + rewrite /flock_res_single to_props_map_singleton. iFrame "HR". iPureIntro. by rewrite /all_props bi.big_sepM_singleton. Qed. @@ -291,7 +302,7 @@ Section flock. { apply map_eq=>i. rewrite lookup_merge. destruct (decide (s = i)) as [->|?]. - rewrite lookup_singleton lookup_insert. - rewrite /to_props_map lookup_fmap. + rewrite to_props_map_lookup. assert (f !! i = None) as ->. + by rewrite -(not_elem_of_dom (D:=(gset prop_id))). + simpl. done. @@ -351,13 +362,13 @@ Section flock. - 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_fmap Hi. simpl. + - rewrite !to_props_map_lookup Hi. simpl. apply option_included. eauto. - revert Hffp. - rewrite /to_props_map !lookup_fmap lookup_insert_ne; auto. } + rewrite !to_props_map_lookup lookup_insert_ne; auto. } rewrite bi.big_sepM_insert; last assumption. specialize (Hffp i). revert Hffp. - rewrite /to_props_map !lookup_fmap lookup_insert; auto. simpl. + 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. @@ -426,42 +437,11 @@ Section flock. 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]". - iAssert (∃ R', ⌜R ≡ R' ∧ fa !! s = Some R'⌝)%I - with "[HRres Hauth]" as %Hfoo. - { iDestruct (own_valid_2 with "Hauth HRres") - 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 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}(bi.big_sepM_lookup_acc _ fa s R'); last done. - iDestruct "Hfa" as "[HR' Hfa]". - iMod ("Hcl" with "[Hstate Hcown Hlocked Hauth Hfactive]"). - { iNext. iExists (Locked π),∅,fa. rewrite left_id. iFrame. - by rewrite /all_props bi.big_sepM_empty. } - iModIntro. - iApply ("HΦ" $! fa). rewrite -HReq. iFrame. - by iApply bi.later_wand. + 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 : @@ -551,7 +531,7 @@ Section flock. iPureIntro. revert Hfoo. rewrite /= left_id singleton_included=> -[R' [Hf HR]]. revert Hf HR. - rewrite /to_props_map lookup_fmap fmap_Some_equiv=>-[R'' [/= Hf ->]]. + 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]].