Commit 7a195a66 authored by Dan Frumin's avatar Dan Frumin

Clean up flock.v

- Reorder the lemmas
- Use to_props_map properties
parent ece2644a
...@@ -72,16 +72,63 @@ Section flock. ...@@ -72,16 +72,63 @@ Section flock.
Definition to_props_map (f : gmap prop_id (iProp Σ)) Definition to_props_map (f : gmap prop_id (iProp Σ))
: gmapUR prop_id (agreeR (iProp Σ)) := to_agree <$> f. : 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 : Lemma to_props_map_insert f i P :
to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f). to_props_map (<[i:=P]>f) = <[i:=to_agree P]>(to_props_map f).
Proof. by rewrite /to_props_map fmap_insert. Qed. 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 : Lemma to_props_map_dom f :
dom (gset prop_id) (to_props_map f) = dom (gset prop_id) f. dom (gset prop_id) (to_props_map f) = dom (gset prop_id) f.
Proof. by rewrite /to_props_map dom_fmap_L. Qed. Proof. by rewrite /to_props_map dom_fmap_L. Qed.
Definition all_props (f : gmap prop_id (iProp Σ)) : iProp Σ := Lemma to_props_map_singleton s R : to_props_map {[s := R]} = {[s := to_agree R]}.
([ map] i R f, R)%I. 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 : Lemma all_props_union f g :
all_props f all_props g all_props (f g). all_props f all_props g all_props (f g).
...@@ -138,33 +185,6 @@ Section flock. ...@@ -138,33 +185,6 @@ Section flock.
by apply bi.sep_proper. by apply bi.sep_proper.
Qed. 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). Global Instance is_flock_persistent γ lk : Persistent (is_flock γ lk).
Proof. apply _. Qed. Proof. apply _. Qed.
...@@ -180,22 +200,13 @@ Section flock. ...@@ -180,22 +200,13 @@ Section flock.
apply bi.exist_proper=>f. by rewrite HPR. apply bi.exist_proper=>f. by rewrite HPR.
Qed. 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) : Lemma unflocked_op (γ : flock_name) (π1 π2 : frac) :
unflocked γ (π1+π2) unflocked γ π1 unflocked γ π2. unflocked γ (π1+π2) unflocked γ π1 unflocked γ π2.
Proof. by rewrite /unflocked fractional. Qed. Proof. by rewrite /unflocked fractional. Qed.
Global Instance unflocked_fractional γ : Fractional (unflocked γ). Global Instance unflocked_fractional γ : Fractional (unflocked γ).
Proof. intros p q. apply unflocked_op. Qed. Proof. intros p q. apply unflocked_op. Qed.
Global Instance unflocked_as_fractional γ π : Global Instance unflocked_as_fractional γ π :
AsFractional (unflocked γ π) (unflocked γ) π. AsFractional (unflocked γ π) (unflocked γ) π.
Proof. split. done. apply _. Qed. Proof. split. done. apply _. Qed.
...@@ -269,7 +280,7 @@ Section flock. ...@@ -269,7 +280,7 @@ Section flock.
iIntros "#Hlk Hunfl HR". iIntros "#Hlk Hunfl HR".
iMod (flock_res_single_alloc_unflocked with "Hlk Hunfl HR") as (s ?) "[HR $]". iMod (flock_res_single_alloc_unflocked with "Hlk Hunfl HR") as (s ?) "[HR $]".
iModIntro. iExists {[s := R]}. 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. iPureIntro. by rewrite /all_props bi.big_sepM_singleton.
Qed. Qed.
...@@ -291,7 +302,7 @@ Section flock. ...@@ -291,7 +302,7 @@ Section flock.
{ apply map_eq=>i. rewrite lookup_merge. { apply map_eq=>i. rewrite lookup_merge.
destruct (decide (s = i)) as [->|?]. destruct (decide (s = i)) as [->|?].
- rewrite lookup_singleton lookup_insert. - rewrite lookup_singleton lookup_insert.
rewrite /to_props_map lookup_fmap. rewrite to_props_map_lookup.
assert (f !! i = None) as ->. assert (f !! i = None) as ->.
+ by rewrite -(not_elem_of_dom (D:=(gset prop_id))). + by rewrite -(not_elem_of_dom (D:=(gset prop_id))).
+ simpl. done. + simpl. done.
...@@ -351,13 +362,13 @@ Section flock. ...@@ -351,13 +362,13 @@ Section flock.
- intros i P f' Hi IH Hffp. rewrite IH; last first. - intros i P f' Hi IH Hffp. rewrite IH; last first.
{ intros j. specialize (Hffp j). { intros j. specialize (Hffp j).
destruct (decide (i = j)) as [->|?]. destruct (decide (i = j)) as [->|?].
- rewrite /to_props_map !lookup_fmap Hi. simpl. - rewrite !to_props_map_lookup Hi. simpl.
apply option_included. eauto. apply option_included. eauto.
- revert Hffp. - 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. rewrite bi.big_sepM_insert; last assumption.
specialize (Hffp i). revert Hffp. 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. rewrite option_included.
intros [Hffp | [? [Q' [HP [HQ HeqQ]]]]]; first by inversion Hffp. intros [Hffp | [? [Q' [HP [HQ HeqQ]]]]]; first by inversion Hffp.
simplify_eq/=. remember (fp !! i) as XX. simplify_eq/=. remember (fp !! i) as XX.
...@@ -426,42 +437,11 @@ Section flock. ...@@ -426,42 +437,11 @@ Section flock.
acquire lk acquire lk
{{{ f, RET #(); R ( R - flocked γ π f) }}}. {{{ f, RET #(); R ( R - flocked γ π f) }}}.
Proof. Proof.
iIntros (Φ) "(Hl & Hunfl & #HRres) HΦ". rewrite -wp_fupd. iIntros (Φ) "(Hl & Hunfl & Hres) HΦ".
rewrite /is_flock. iDestruct "Hl" as "(#Hcinv & #Hlk)". rewrite /flock_res_single.
iApply (acquire_spec with "Hlk"). iNext. iApply (acquire_cancel_spec with "[$Hl $Hunfl Hres]"); last done.
iIntros "[Hlocked Hunlk]". iExists {[s := R]}.
iMod (cinv_open with "Hcinv Hunfl") as "(Hstate & Hunfl & Hcl)"; first done. rewrite to_props_map_singleton all_props_singleton. eauto.
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.
Qed. Qed.
Lemma release_cancel_spec γ π lk f : Lemma release_cancel_spec γ π lk f :
...@@ -551,7 +531,7 @@ Section flock. ...@@ -551,7 +531,7 @@ Section flock.
iPureIntro. revert Hfoo. iPureIntro. revert Hfoo.
rewrite /= left_id singleton_included=> -[R' [Hf HR]]. rewrite /= left_id singleton_included=> -[R' [Hf HR]].
revert 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; intros [?%to_agree_inj | ?%to_agree_included]%Some_included;
simplify_eq/=; exists R''; eauto. } simplify_eq/=; exists R''; eauto. }
destruct Hfoo as [R' [HReq Hf]]. destruct Hfoo as [R' [HReq Hf]].
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment