Commit e1571a89 authored by Dan Frumin's avatar Dan Frumin

A simpler flock API

Get rid of `prop_id`. This also simplifies the proofs.
parent 2ad958e4
......@@ -64,8 +64,9 @@ Section cwp.
is_mset env X
full_locking_heap σ)%I.
Definition flock_resources (γ : flock_name) (I : gmap prop_id lock_res) :=
([ map] i X I, flock_res cmonadN γ i X)%I.
Definition flock_resources (γ : flock_name)
(I : gmap lock_res_gname (frac*iProp Σ)) :=
([ map] ρ πR I, flock_res cmonadN γ ρ πR.1 πR.2)%I.
(** DF: The outer `WP` here is needed to be able to perform some reductions inside a heap_lang context.
Without this, the `cwp_cwp` rule is not provable.
......@@ -77,10 +78,10 @@ Section cwp.
Definition cwp_def (e : expr)
(R : iProp Σ) (Φ : val iProp Σ) : iProp Σ :=
WP e {{ ev,
(γ : flock_name) (env : val) (l : val) (I : gmap prop_id lock_res),
(γ : flock_name) (env : val) (l : val) I,
is_flock cmonadN γ l -
flock_resources γ I -
([ map] X I, res_prop X) (env_inv env R) -
([ map] πR I, πR.2) (env_inv env R) -
WP ev env l {{ v, Φ v flock_resources γ I }}
}}%I.
Definition cwp_aux : seal (@cwp_def). by eexists. Qed.
......@@ -131,9 +132,9 @@ Section cwp_rules.
iApply (wp_wand with "Hcwp").
iIntros (v) "HΦ".
iIntros (γ env l I) "#Hflock Hres #Heq".
iMod (flock_res_alloc_strong _ (dom (gset prop_id) I) with "Hflock HR1") as (j ρ) "[% Hres']"; first done.
pose (I' := <[j:= (LockRes R1 1 ρ)]>I).
assert (I !! j = None) by by eapply not_elem_of_dom.
iMod (flock_res_alloc_strong _ (dom (gset lock_res_gname) I) with "Hflock HR1") as (ρ) "[% Hres']"; first done.
pose (I' := <[ρ:=(1%Qp,R1)]>I).
assert (I !! ρ = None) by by eapply not_elem_of_dom.
iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []").
{ rewrite /flock_resources /I'.
rewrite big_sepM_insert //. iFrame. }
......@@ -224,11 +225,11 @@ Section cwp_rules.
iDestruct ("Hwp" with "HR") as (Q) "[HQ Hwp]".
wp_apply (newflock_spec cmonadN); first done.
iIntros (k γ') "#Hlock2".
iMod (flock_res_alloc_strong _ _ _ (env_inv env Q)%I with "Hlock2 [$HQ $Henv]") as (s ρ) "[_ Hres]"; first done.
iMod (flock_res_alloc_strong _ _ _ (env_inv env Q)%I with "Hlock2 [$HQ $Henv]") as (ρ) "[_ Hres]"; first done.
wp_let.
wp_apply (wp_wand with "Hwp"); iIntros (ev') "Hwp". wp_bind (ev' _ _).
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[s:=(LockRes _ 1 ρ)]} with "Hlock2 [Hres] []").
- iApply ("Hwp" $! _ _ _ {[ρ:=(1%Qp,_)]} with "Hlock2 [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
+ rewrite big_sepM_singleton //.
- iIntros (w) "[HR Hres]".
......@@ -276,7 +277,7 @@ Section cwp_rules.
wp_apply (wp_wand with "Hwp1").
iIntros (ev1) "Hwp1". wp_lam. wp_pures.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
pose (I' := fmap (λ X, LockRes (res_prop X) (res_frac X/2) (res_name X)) I).
pose (I' := fmap (λ πR, ((πR.1/2)%Qp,πR.2)) I).
iAssert (flock_resources γ I' flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
{ rewrite /flock_resources -big_sepM_sepM.
rewrite /I' big_sepM_fmap /=.
......@@ -345,12 +346,12 @@ Section cwp_run.
wp_apply (newflock_spec cmonadN); first done.
iIntros (k γ') "#Hlock". iApply wp_fupd.
iMod (flock_res_alloc_strong _ _ _ (env_inv env)%I
with "Hlock [Henv Hσ]") as (s ρ) "[_ Hres]"; first done.
with "Hlock [Henv Hσ]") as (ρ) "[_ Hres]"; first done.
{ iNext. iExists , . iFrame. iPureIntro; set_solver. }
wp_let.
iMod (wp_value_inv with "Hwp") as "Hwp".
iApply (wp_wand with "[Hwp Hres]").
- iApply ("Hwp" $! _ _ _ {[s := LockRes _ 1 ρ]} with "Hlock [Hres] []").
- iApply ("Hwp" $! _ _ _ {[ρ := (1%Qp,_)]} with "Hlock [Hres] []").
+ rewrite /flock_resources big_sepM_singleton //.
+ by rewrite big_sepM_singleton right_id.
- iIntros (w) "[HΦ Hres]".
......
......@@ -57,23 +57,28 @@ Record flock_name := {
}.
(** The data about pending and active propositions will be stored in
the maps `prop_id -> _` *)
(* `prop_id` is fefined 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 maps `lock_res_gname -> frac` *)
(** One of the tricks in this lock 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.
The `lock_res_name` datastructure contains all the ghosts names needed to manage an individual proposition.
*)
Record lock_res_name := {
Record lock_res_gname := {
flock_cinv_name : gname;
flock_token1_name : gname;
flock_token2_name : gname;
}.
Canonical Structure lock_res_nameC := leibnizC lock_res_name.
Canonical Structure lock_res_gnameC := leibnizC lock_res_gname.
Instance lock_res_gname_eq_dec : EqDecision lock_res_gname.
Proof. solve_decision. Defined.
Instance lock_res_gname_countable : Countable lock_res_gname.
Proof.
apply inj_countable' with
(f:=(λ x, (flock_cinv_name x, flock_token1_name x, flock_token2_name x)))
(g:=(λ '(γ1,γ2,γ3), Build_lock_res_gname γ1 γ2 γ3)).
intros []. reflexivity.
Defined.
(** Before we define the type of flock resources, we need to have
access to the appropriate CMRAs.
......@@ -81,11 +86,11 @@ Canonical Structure lock_res_nameC := leibnizC lock_res_name.
The totality of propositions , and the pending propositions will be
represented as a map:
`prop_id → frac * ag (flock_res_name)`,
`lock_res_gname → frac`,
so a standart ghost heap. Active propositions will be modelled by a map
`excl (prop_id → frac * ag (flock_res_name))`.
`excl (lock_res_name → frac)`.
In other words, this map will contain *exact* information of which propositions are active and with what fractions were they activated.
......@@ -96,8 +101,10 @@ Class flockG Σ :=
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_props_active :> inG Σ (authR
(optionUR (exclR (gmapC lock_res_gname fracR))));
flock_props :> inG Σ (authR
(gmapUR lock_res_gname fracR));
flock_tokens :> inG Σ (exclR unitC);
}.
......@@ -105,22 +112,12 @@ Definition flockΣ : gFunctors :=
#[GFunctor (authR (optionUR (exclR lockstateC)))
;lockΣ
;cinvΣ
;GFunctor (authR (optionUR (exclR (gmapC prop_id (prodC fracC lock_res_nameC)))))
;GFunctor (authR (gmapUR prop_id (prodR fracR (agreeR lock_res_nameC))))%CF].
;GFunctor (authR (optionUR (exclR (gmapC lock_res_gname fracC))))
;GFunctor (authR (gmapUR lock_res_gname fracR))%CF].
Instance subG_flockΣ Σ : subG flockΣ Σ flockG Σ.
Proof. solve_inG. Qed.
Record lock_res `{flockG Σ} := {
res_prop : iProp Σ;
res_frac : frac;
res_name : lock_res_name;
}.
(** A "smart constructor" for `lock_res` *)
Definition LockRes `{flockG Σ} (R : iProp Σ) (π : frac) (ρ : lock_res_name) :=
{| res_prop := R; res_frac := π; res_name := ρ |}.
Section flock.
Context `{heapG Σ, flockG Σ}.
Variable N : namespace.
......@@ -129,32 +126,40 @@ Section flock.
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 token (γ : lock_res_gname) : iProp Σ :=
own (flock_token1_name γ) (Excl ()).
Definition token (γ : lock_res_gname) : iProp Σ :=
own (flock_token2_name γ) (Excl ()).
Definition C (R : iProp Σ) (ρ : lock_res_name) : iProp Σ :=
Definition C (R : iProp Σ) (ρ : lock_res_gname) : 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.
Definition all_tokens (P : gmap lock_res_gname ()) : iProp Σ :=
([ map] ρ _ P, token ρ)%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 from_active (A : gmap lock_res_gname frac)
:= fmap (const ()) A.
(** A flock resource `s ↦ X,π,γ` contains:
- Knowledge that the `s ↦{π} γ` is in the set of propositions managed by the flock;
- There is a cancellable invariant `C X γ`;
(** A flock resource `(ρ,X,π)` contains:
- Knowledge that the `ρ ↦ π` is in the set of propositions managed by the flock;
- There is a cancellable invariant `C X ρ`;
- We have π- permissiones to access that invariant.
*)
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 N_of_ρ (ρ : lock_res_gname) :=
(flock_token1_name ρ, flock_token2_name ρ).
(* When creating a new invariant we need to pick a name that depends
_only_ on the ghost names of the tokens. We cannot depend on the
ghost name for the cancellable invariant, because that would be
circular. I mean we potentially can but that would be annoying. *)
Definition flock_res (γ : flock_name) (ρ : lock_res_gname)
(π : frac)
(P : iProp Σ) : iProp Σ :=
(own (flock_props_name γ) ( {[ρ := π]})
cinv (resN.@(N_of_ρ ρ)) (flock_cinv_name ρ) (C P ρ)
cinv_own (flock_cinv_name ρ) π)%I.
(** Basically says that the propositions from the map `A` are active.
This predicate is designed to contain enough information to deactivate those propositions.
......@@ -162,28 +167,26 @@ Section flock.
When we are deactivating the propositions we need to make sure that the set of the active propositions has not changed. That's why we need a CMRA to keep track of the exact contents of that set.
*)
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
(γ : flock_name) (A : gmap lock_res_gname (frac*iProp Σ)) : iProp Σ :=
(let fa := fmap fst A : gmap lock_res_gname frac in
(* Information we retain: the flock is locked .. *)
own (flock_state_name γ) ( (Excl' 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.
([ map] ρ πR A, token ρ
cinv (resN.@(N_of_ρ ρ)) (flock_cinv_name ρ) (C πR.2 ρ)
cinv_own (flock_cinv_name ρ) πR.1))%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 to_props_map (f : gmap lock_res_gname ())
: gmapUR lock_res_gname fracR :=
fmap (const 1%Qp) f.
(** TODO: can we actually get rid of the `to_props_map` here? *)
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),
(fa : gmap lock_res_gname frac)
(fp : gmap lock_res_gname unit), (** aka mapset lock_res_name *)
(** ... and those sets are disjoint *)
fp ## from_active fa
own (flock_state_name γ) ( (Excl' s))
......@@ -203,10 +206,10 @@ Section flock.
(** .. and we take hold of all the ghost pointsto `s ↦{π} ρ`.
This is necessary to have if we want to free the
resources. If we wish to free the resource `s ↦{1} ρ`,
resources. If we wish to free the resource `ρ ↦ 1`,
then we need to know that it is not currently active (has
not been acquired). The predicate below ensures that. *)
([ map] i πρ fa, own (flock_props_name γ) ( {[i:=(πρ.1,to_agree πρ.2)]}))
own (flock_props_name γ) ( fa)
| Unlocked =>
(** If the lock is NOT acquired, then there are no active
proposition *)
......@@ -221,24 +224,9 @@ Section flock.
(** * Lemmata **)
(** ** Basic properties of the CAPs *)
Lemma flock_res_agree (γ : flock_name) (s : prop_id) (R1 R2 : iProp Σ) ρ1 ρ2 (π1 π2 : frac) :
flock_res γ s (LockRes R1 π1 ρ1) -
flock_res γ s (LockRes R2 π2 ρ2) ==
⌜ρ1 = ρ2.
Proof.
rewrite /flock_res.
iDestruct 1 as "(Hs1 & #Hinv1 & Hρ1)".
iDestruct 1 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']. eauto.
Qed.
Lemma flock_res_op (γ : flock_name) (s : prop_id) (R : iProp Σ) ρ (π1 π2 : frac) :
flock_res γ s (LockRes R (π1+π2) ρ)
flock_res γ s (LockRes R π1 ρ) flock_res γ s (LockRes R π2 ρ).
Lemma flock_res_op (γ : flock_name) (ρ : lock_res_gname) (R : iProp Σ) (π1 π2 : frac) :
flock_res γ ρ (π1+π2) R
flock_res γ ρ π1 R flock_res γ ρ π2 R.
Proof.
rewrite /flock_res. iSplit.
- iDestruct 1 as "(Hs & #Hinv & Hρ)".
......@@ -252,21 +240,21 @@ Section flock.
rewrite /C /=. iFrame "Hinv1".
Qed.
Global Instance flock_res_fractional γ s R ρ :
Fractional (λ π, flock_res γ s (LockRes R π ρ)).
Global Instance flock_res_fractional γ i R :
Fractional (λ π, flock_res γ i π R).
Proof. intros p q. apply flock_res_op. Qed.
Global Instance flock_res_as_fractional γ s R π ρ :
AsFractional (flock_res γ s (LockRes R π ρ))
(λ π, flock_res γ s (LockRes R π ρ)) π.
Global Instance flock_res_as_fractional γ i R π :
AsFractional (flock_res γ i π R)
(λ π, flock_res γ i π 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 ρ.
Lemma to_props_map_singleton_included fp q ρ:
{[ρ := q]} to_props_map fp fp !! ρ = 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 -> //.
rewrite /to_props_map lookup_fmap fmap_Some_equiv.
move=> -[[] [Hρ _]]//.
Qed.
Lemma to_props_map_delete fp i:
......@@ -277,10 +265,10 @@ Section flock.
(** ** Spectral operations *)
Lemma flock_res_alloc_strong (X : gset prop_id) γ lk R E :
Lemma flock_res_alloc_strong (X : gset lock_res_gname) γ lk R E :
N E
is_flock γ lk -
R ={E}= s ρ, s X flock_res γ s (LockRes R 1 ρ).
R ={E}= ρ, ⌜ρ X flock_res γ ρ 1 R.
Proof.
iIntros (?) "Hl HR". rewrite /is_flock.
iDestruct "Hl" as "(#Hfl & #Hlk)".
......@@ -288,93 +276,101 @@ Section flock.
(* 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ρ]".
(* We need to guarantee that the new name
- is not in the set X,
- does not clash with the existing names in the invariant *)
set (X := collection_map flock_token1_name
X : gset gname).
set (X := collection_map flock_token2_name
(dom (gset lock_res_gname) (fp from_active fa)) : gset gname).
iMod (own_alloc_strong (Excl ()) X) as (γt Ht) "T1"; first done.
iMod (own_alloc_strong (Excl ()) X) as (γt Ht) "T2"; first done.
iMod (cinv_alloc _ (resN.@(γt,γt)) (R own γt (Excl ()) own γt (Excl ()))%I with "[HR T1]") as (γc) "[#HR Hρ]".
{ iNext. iLeft. by iFrame. }
pose (ρ :=
set (ρ :=
{| 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 ρ) ]}).
{ eapply (auth_update_alloc _
(to_props_map (<[ρ := ()]> fp from_active fa))
{[ ρ := 1%Qp ]}).
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. }
apply (not_elem_of_dom (to_props_map (fp from_active fa)) _ (D:=gset lock_res_gname)).
rewrite /to_props_map dom_fmap.
intros Hρ. apply Ht.
by apply (elem_of_map_2 flock_token2_name _ ρ).
}
iDestruct "Haprops" as "[Haprops Hi]".
iMod ("Hcl" with "[-Hi Hρ]") as "_".
{ iNext. iExists s, fa,(<[i:=ρ]>fp).
{ iNext. iExists s, fa,(<[ρ:=()]>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. }
{ apply (not_elem_of_dom _ ρ (D:=gset lock_res_gname)).
intros Hρ. apply Ht.
apply (elem_of_map_2 flock_token2_name _ ρ).
rewrite dom_union_L elem_of_union //. eauto. }
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.
eapply (not_elem_of_dom (D:=gset lock_res_gname)).
intros Hi. apply Ht.
apply (elem_of_map_2 flock_token2_name _ ρ).
rewrite dom_union_L elem_of_union. eauto. }
iModIntro; iExists ρ; iSplit; last by iFrame.
iPureIntro.
intros Hρ. apply Ht. unfold X.
by apply (elem_of_map_2 flock_token1_name X ρ).
Qed.
Lemma flock_res_dealloc γ lk i X E :
Lemma flock_res_dealloc γ lk ρ R E :
N E
res_frac X = 1%Qp
is_flock γ lk -
flock_res γ i X ={E}= (res_prop X).
flock_res γ ρ 1 R ={E}= R.
Proof.
iIntros (? HX) "Hl HR". rewrite /is_flock.
iIntros (?) "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ρ)".
iDestruct "HR" as "(Hρ & #Hiinv & Hcinv)".
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")
(* We can now show that the proposition `ρ` is *not* active *)
iDestruct (own_valid_2 with "Haprops Hρ")
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, can this proof be simplified? *)
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.
iAssert (fa !! ρ = None)%I with "[-]" as %Hbar.
{ remember (fa !! ρ) as faρ. destruct faρ as [π|]; last done.
symmetry in Heqfaρ.
iCombine "Hactives Hρ" as "H".
iDestruct (own_valid with "H") as %Hbaz.
exfalso. apply auth_own_valid in Hbaz. simpl in *.
specialize (Hbaz ρ). revert Hbaz.
rewrite lookup_op Heqfaρ lookup_singleton.
rewrite -Some_op Some_valid.
eapply exclusive_r ; eauto. apply _. }
assert (fp !! ρ = 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 ρ) //.
iMod (own_update_2 with "Haprops Hρ") as "Haprops".
{ apply auth_update_dealloc, (delete_singleton_local_update _ ρ _). }
rewrite /all_tokens (big_sepM_delete _ fp ρ) //.
iDestruct "Htokens" as "[T2 Htokens]".
iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
iMod (cinv_cancel with "Hiinv Hcinv") 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.
iExists Locked,fa,(delete ρ fp). iFrame.
iSplit.
+ iPureIntro. solve_map_disjoint.
+ rewrite to_props_map_delete delete_union.
......@@ -387,20 +383,20 @@ Section flock.
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")
iDestruct (own_valid_2 with "Haprops Hρ")
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 ρ) //.
iMod (own_update_2 with "Haprops Hρ") as "Haprops".
{ apply auth_update_dealloc, (delete_singleton_local_update _ ρ _). }
rewrite /all_tokens (big_sepM_delete _ fp ρ _) //.
iDestruct "Htokens" as "[T2 Htokens]".
iMod (cinv_cancel with "Hiinv Hρ") as "HC". solve_ndisj.
iMod (cinv_cancel with "Hiinv Hcinv") 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.
iExists Unlocked,,(delete ρ fp). iFrame.
iSplit.
+ iPureIntro. solve_map_disjoint.
+ rewrite /from_active fmap_empty /= right_id.
......@@ -408,15 +404,16 @@ Section flock.
Qed.
(** `flocked` supports invariant access just like regular invariants *)
Lemma flocked_inv_open_single E i X γ I :
Lemma flocked_inv_open_single E γ ρ πR I :
resN E
I !! i = Some X
I !! ρ = Some πR
flocked γ I ={E}=
(res_prop X) ( (res_prop X) ={E}= flocked γ I).
πR.2 ( πR.2 ={E}= flocked γ I).
Proof.
iIntros (? Hi). rewrite {1}/flocked.
iDestruct 1 as (fa ?) "(Hst & Hfa & Htokens)".
rewrite (big_sepM_lookup_acc _ I i X) //.
destruct πR as [π R].
iIntros (? Hρ). rewrite {1}/flocked.
iIntros "(Hst & Hfa & Htokens)".
rewrite (big_sepM_lookup_acc _ I ρ (π,R)) //.
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.
......@@ -429,26 +426,23 @@ Section flock.
{ 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.
iModIntro. rewrite /flocked.
iFrame "Hst Hfa". iApply "Htokens". by iFrame.
Qed.
Lemma flocked_inv_open E γ I :
resN E
flocked γ I ={E}=
([ map] s X I, res_prop X)
( ([ map] s X I, res_prop X) ={E}= flocked γ I).
([ map] ρ πR I, πR.2)
( ([ map] ρ πR I, πR.2) ={E}= flocked γ I).
Proof.
iIntros (?). rewrite {1}/flocked.
iDestruct 1 as (fa ?) "(Hst & Hfa & Htokens)".
iIntros "(Hst & Hfa & Htokens)".
rewrite !big_sepM_sepM.
iDestruct "Htokens" as "(T2s & Hinvs & Hρs)".
rewrite /flocked -(bi.exist_intro fa).
iAssert (fa = (λ X, (res_frac X, res_name X)) <$> I)%I as "$".
{ eauto. }
iFrame "Hst Hfa". subst fa.
iInduction I as [|s X I Hs] "IH" using map_ind.
rewrite /flocked.
iFrame "Hst Hfa".
iInduction I as [|ρ πR I Hs] "IH" using map_ind.
- rewrite /flocked !big_sepM_empty. eauto with iFrame.
- rewrite !big_sepM_insert //.
iDestruct "T2s" as "[T2 T2s]".
......@@ -497,16 +491,58 @@ Section flock.
rewrite /is_flock. by iFrame "Hlock".
Qed.
(** We need two additional lemmas, and they are annoying! *)
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] ix 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.
Lemma release_cancel_spec γ lk I :
{{{ is_flock γ lk flocked γ I }}}
release lk
{{{ RET #(); [ map] i X I, flock_res γ i X }}}.
{{{ RET #(); [ map] ρ πR I, flock_res γ ρ πR.1 πR.2 }}}.
Proof.