Commit b38f1529 authored by Simon Friis Vindum's avatar Simon Friis Vindum Committed by Ralf Jung
Browse files

gmap_view supports persisting the authorative element

parent 46d8457a
......@@ -73,11 +73,12 @@ Chajed, and Yusuke Matsushita. Thanks a lot to everyone involved!
**Changes in `algebra`:**
* Generalize the authorative elements of the `view`, `auth` and `gset_bij`
cameras to be parameterized by a [discardable fraction](iris/algebra/dfrac.v)
(`dfrac`) instead of a fraction (`frac`). Normal fractions are now denoted
`●{#q} a` and `●V{#q} a`. Lemmas affected by this have been renamed such that
the "frac" in their name has been changed into "dfrac". (by Simon Friis Vindum)
* Generalize the authorative elements of the `view`, `auth`, `gmap_view`, and
`gset_bij` cameras to be parameterized by a [discardable
fraction](iris/algebra/dfrac.v) (`dfrac`) instead of a fraction (`frac`).
Normal fractions are now denoted `●{#q} a` and `●V{#q} a`. Lemmas affected by
this have been renamed such that the "frac" in their name has been changed
into "dfrac". (by Simon Friis Vindum)
* Generalize `namespace_map` to `reservation_map` which enhances `gmap positive
A` with a notion of 'tokens' that enable allocating a particular name in the
map. See [algebra.reservation_map](iris/algebra/reservation_map.v) for further
......@@ -218,11 +219,13 @@ replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
```
sed -i -E -f- $(find theories -name "*.v") <<EOF
# auth and view renames from frac to dfrac
# auth, view, and gmap_view renames from frac to dfrac
s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
s/\bgmap_view_(auth|both)_frac_(op_invN|op_inv|op_inv_L|valid|op_validN|op_valid|op_valid_L)\b/gmap_view_\1_dfrac_\2/g
s/\bgmap_view_persist\b/gmap_view_frag_persist/g
# big_sepM renames
s/\bbig_sepM2_lookup_1\b/big_sepM2_lookup_l/g
s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
......
......@@ -137,8 +137,8 @@ Definition gmap_viewUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
Section definitions.
Context {K : Type} `{Countable K} {V : ofe}.
Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
V{#q} m.
Definition gmap_view_auth (dq : dfrac) (m : gmap K V) : gmap_viewR K V :=
V{dq} m.
Definition gmap_view_frag (k : K) (dq : dfrac) (v : V) : gmap_viewR K V :=
V {[k := (dq, to_agree v)]}.
End definitions.
......@@ -148,9 +148,9 @@ Section lemmas.
Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
Global Instance : Params (@gmap_view_auth) 5 := {}.
Global Instance gmap_view_auth_ne q : NonExpansive (gmap_view_auth (K:=K) (V:=V) q).
Global Instance gmap_view_auth_ne dq : NonExpansive (gmap_view_auth (K:=K) (V:=V) dq).
Proof. solve_proper. Qed.
Global Instance gmap_view_auth_proper q : Proper (() ==> ()) (gmap_view_auth (K:=K) (V:=V) q).
Global Instance gmap_view_auth_proper dq : Proper (() ==> ()) (gmap_view_auth (K:=K) (V:=V) dq).
Proof. apply ne_proper, _. Qed.
Global Instance : Params (@gmap_view_frag) 6 := {}.
......@@ -176,49 +176,54 @@ Section lemmas.
Qed.
(** Composition and validity *)
Lemma gmap_view_auth_dfrac_op dp dq m :
gmap_view_auth (dp dq) m
gmap_view_auth dp m gmap_view_auth dq m.
Proof. by rewrite /gmap_view_auth view_auth_dfrac_op. Qed.
Lemma gmap_view_auth_frac_op p q m :
gmap_view_auth (p + q) m gmap_view_auth p m gmap_view_auth q m.
Proof. by rewrite /gmap_view_auth -dfrac_op_own view_auth_dfrac_op. Qed.
Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
IsOp q q1 q2 IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
gmap_view_auth (DfracOwn (p + q)) m
gmap_view_auth (DfracOwn p) m gmap_view_auth (DfracOwn q) m.
Proof. by rewrite /gmap_view_auth view_auth_frac_op. Qed.
Global Instance gmap_view_auth_dfrac_is_op dq dq1 dq2 m :
IsOp dq dq1 dq2 IsOp' (gmap_view_auth dq m) (gmap_view_auth dq1 m) (gmap_view_auth dq2 m).
Proof. rewrite /gmap_view_auth. apply _. Qed.
Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
{n} (gmap_view_auth p m1 gmap_view_auth q m2) m1 {n} m2.
Lemma gmap_view_auth_dfrac_op_invN n dp m1 dq m2 :
{n} (gmap_view_auth dp m1 gmap_view_auth dq m2) m1 {n} m2.
Proof. apply view_auth_dfrac_op_invN. Qed.
Lemma gmap_view_auth_frac_op_inv p m1 q m2 :
(gmap_view_auth p m1 gmap_view_auth q m2) m1 m2.
Lemma gmap_view_auth_dfrac_op_inv dp m1 dq m2 :
(gmap_view_auth dp m1 gmap_view_auth dq m2) m1 m2.
Proof. apply view_auth_dfrac_op_inv. Qed.
Lemma gmap_view_auth_frac_op_inv_L `{!LeibnizEquiv V} q m1 p m2 :
(gmap_view_auth p m1 gmap_view_auth q m2) m1 = m2.
Lemma gmap_view_auth_dfrac_op_inv_L `{!LeibnizEquiv V} dq m1 dp m2 :
(gmap_view_auth dp m1 gmap_view_auth dq m2) m1 = m2.
Proof. apply view_auth_dfrac_op_inv_L, _. Qed.
Lemma gmap_view_auth_frac_valid m q : gmap_view_auth q m (q 1)%Qp.
Lemma gmap_view_auth_dfrac_valid m dq : gmap_view_auth dq m dq.
Proof.
rewrite view_auth_dfrac_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_valid m : gmap_view_auth 1 m.
Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
Lemma gmap_view_auth_valid m : gmap_view_auth (DfracOwn 1) m.
Proof. rewrite gmap_view_auth_dfrac_valid. done. Qed.
Lemma gmap_view_auth_frac_op_validN n q1 q2 m1 m2 :
{n} (gmap_view_auth q1 m1 gmap_view_auth q2 m2) (q1 + q2)%Qp m1 {n} m2.
Lemma gmap_view_auth_dfrac_op_validN n dq1 dq2 m1 m2 :
{n} (gmap_view_auth dq1 m1 gmap_view_auth dq2 m2) (dq1 dq2) m1 {n} m2.
Proof.
rewrite view_auth_dfrac_op_validN. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
(gmap_view_auth q1 m1 gmap_view_auth q2 m2) (q1 + q2 1)%Qp m1 m2.
Lemma gmap_view_auth_dfrac_op_valid dq1 dq2 m1 m2 :
(gmap_view_auth dq1 m1 gmap_view_auth dq2 m2) (dq1 dq2) m1 m2.
Proof.
rewrite view_auth_dfrac_op_valid. intuition eauto using gmap_view_rel_unit.
Qed.
Lemma gmap_view_auth_frac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
(gmap_view_auth q1 m1 gmap_view_auth q2 m2) (q1 + q2)%Qp m1 = m2.
Proof. unfold_leibniz. apply gmap_view_auth_frac_op_valid. Qed.
Lemma gmap_view_auth_dfrac_op_valid_L `{!LeibnizEquiv V} dq1 dq2 m1 m2 :
(gmap_view_auth dq1 m1 gmap_view_auth dq2 m2) (dq1 dq2) m1 = m2.
Proof. unfold_leibniz. apply gmap_view_auth_dfrac_op_valid. Qed.
Lemma gmap_view_auth_op_validN n m1 m2 :
{n} (gmap_view_auth 1 m1 gmap_view_auth 1 m2) False.
{n} (gmap_view_auth (DfracOwn 1) m1 gmap_view_auth (DfracOwn 1) m2) False.
Proof. apply view_auth_op_validN. Qed.
Lemma gmap_view_auth_op_valid m1 m2 :
(gmap_view_auth 1 m1 gmap_view_auth 1 m2) False.
(gmap_view_auth (DfracOwn 1) m1 gmap_view_auth (DfracOwn 1) m2) False.
Proof. apply view_auth_op_valid. Qed.
Lemma gmap_view_frag_validN n k dq v : {n} gmap_view_frag k dq v dq.
......@@ -260,21 +265,21 @@ Section lemmas.
(gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2) (dq1 dq2) v1 = v2.
Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
Lemma gmap_view_both_frac_validN n q m k dq v :
{n} (gmap_view_auth q m gmap_view_frag k dq v)
(q 1)%Qp dq m !! k {n} Some v.
Lemma gmap_view_both_dfrac_validN n dp m k dq v :
{n} (gmap_view_auth dp m gmap_view_frag k dq v)
dp dq m !! k {n} Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag.
rewrite view_both_dfrac_validN gmap_view_rel_lookup.
naive_solver.
Qed.
Lemma gmap_view_both_validN n m k dq v :
{n} (gmap_view_auth 1 m gmap_view_frag k dq v)
{n} (gmap_view_auth (DfracOwn 1) m gmap_view_frag k dq v)
dq m !! k {n} Some v.
Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
Lemma gmap_view_both_frac_valid q m k dq v :
(gmap_view_auth q m gmap_view_frag k dq v)
(q 1)%Qp dq m !! k Some v.
Proof. rewrite gmap_view_both_dfrac_validN. naive_solver done. Qed.
Lemma gmap_view_both_dfrac_valid dp m k dq v :
(gmap_view_auth dp m gmap_view_frag k dq v)
dp dq m !! k Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag.
rewrite view_both_dfrac_valid. setoid_rewrite gmap_view_rel_lookup.
......@@ -286,18 +291,18 @@ Section lemmas.
+ apply Hm.
+ revert n. apply equiv_dist. apply Hm.
Qed.
Lemma gmap_view_both_frac_valid_L `{!LeibnizEquiv V} q m k dq v :
(gmap_view_auth q m gmap_view_frag k dq v)
q dq m !! k = Some v.
Proof. unfold_leibniz. apply gmap_view_both_frac_valid. Qed.
Lemma gmap_view_both_dfrac_valid_L `{!LeibnizEquiv V} dp m k dq v :
(gmap_view_auth dp m gmap_view_frag k dq v)
dp dq m !! k = Some v.
Proof. unfold_leibniz. apply gmap_view_both_dfrac_valid. Qed.
Lemma gmap_view_both_valid m k dq v :
(gmap_view_auth 1 m gmap_view_frag k dq v)
(gmap_view_auth (DfracOwn 1) m gmap_view_frag k dq v)
dq m !! k Some v.
Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
Proof. rewrite gmap_view_both_dfrac_valid. naive_solver done. Qed.
(* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
have [inv_L] lemmas instead that just have an equality on the RHS. *)
Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
(gmap_view_auth 1 m gmap_view_frag k dq v)
(gmap_view_auth (DfracOwn 1) m gmap_view_frag k dq v)
dq m !! k = Some v.
Proof. unfold_leibniz. apply gmap_view_both_valid. Qed.
......@@ -305,7 +310,7 @@ Section lemmas.
Lemma gmap_view_alloc m k dq v :
m !! k = None
dq
gmap_view_auth 1 m ~~> gmap_view_auth 1 (<[k := v]> m) gmap_view_frag k dq v.
gmap_view_auth (DfracOwn 1) m ~~> gmap_view_auth (DfracOwn 1) (<[k := v]> m) gmap_view_frag k dq v.
Proof.
intros Hfresh Hdq. apply view_update_alloc=>n bf Hrel j [df va] /=.
rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
......@@ -326,8 +331,8 @@ Section lemmas.
Lemma gmap_view_alloc_big m m' dq :
m' ## m
dq
gmap_view_auth 1 m ~~>
gmap_view_auth 1 (m' m) ([^op map] kv m', gmap_view_frag k dq v).
gmap_view_auth (DfracOwn 1) m ~~>
gmap_view_auth (DfracOwn 1) (m' m) ([^op map] kv m', gmap_view_frag k dq v).
Proof.
intros. induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
{ rewrite big_opM_empty left_id_L right_id. done. }
......@@ -339,8 +344,8 @@ Section lemmas.
Qed.
Lemma gmap_view_delete m k v :
gmap_view_auth 1 m gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth 1 (delete k m).
gmap_view_auth (DfracOwn 1) m gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth (DfracOwn 1) (delete k m).
Proof.
apply view_update_dealloc=>n bf Hrel j [df va] Hbf /=.
destruct (decide (j = k)) as [->|Hne].
......@@ -354,8 +359,8 @@ Section lemmas.
Qed.
Lemma gmap_view_delete_big m m' :
gmap_view_auth 1 m ([^op map] kv m', gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth 1 (m m').
gmap_view_auth (DfracOwn 1) m ([^op map] kv m', gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth (DfracOwn 1) (m m').
Proof.
induction m' as [|k v m' ? IH] using map_ind.
{ rewrite right_id_L big_opM_empty right_id //. }
......@@ -365,8 +370,8 @@ Section lemmas.
Qed.
Lemma gmap_view_update m k v v' :
gmap_view_auth 1 m gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth 1 (<[k := v']> m) gmap_view_frag k (DfracOwn 1) v'.
gmap_view_auth (DfracOwn 1) m gmap_view_frag k (DfracOwn 1) v ~~>
gmap_view_auth (DfracOwn 1) (<[k := v']> m) gmap_view_frag k (DfracOwn 1) v'.
Proof.
rewrite gmap_view_delete.
rewrite (gmap_view_alloc _ k (DfracOwn 1) v') //; last by rewrite lookup_delete.
......@@ -375,8 +380,8 @@ Section lemmas.
Lemma gmap_view_update_big m m0 m1 :
dom (gset K) m0 = dom (gset K) m1
gmap_view_auth 1 m ([^op map] kv m0, gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth 1 (m1 m) ([^op map] kv m1, gmap_view_frag k (DfracOwn 1) v).
gmap_view_auth (DfracOwn 1) m ([^op map] kv m0, gmap_view_frag k (DfracOwn 1) v) ~~>
gmap_view_auth (DfracOwn 1) (m1 m) ([^op map] kv m1, gmap_view_frag k (DfracOwn 1) v).
Proof.
intros Hdom%eq_sym. revert m1 Hdom.
induction m0 as [|k v m0 Hnotdom IH] using map_ind; intros m1 Hdom.
......@@ -398,7 +403,11 @@ Section lemmas.
rewrite union_delete_insert //.
Qed.
Lemma gmap_view_persist k dq v :
Lemma gmap_view_auth_persist dq m :
gmap_view_auth dq m ~~> gmap_view_auth DfracDiscarded m.
Proof. apply view_update_auth_persist. Qed.
Lemma gmap_view_frag_persist k dq v :
gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
Proof.
apply view_update_frag=>m n bf Hrel j [df va] /=.
......
......@@ -244,7 +244,7 @@ Section gmap_view.
Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
Lemma gmap_view_both_validI m k dq v :
(gmap_view_auth 1 m gmap_view_frag k dq v)
(gmap_view_auth (DfracOwn 1) m gmap_view_frag k dq v)
dq m !! k Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
......
......@@ -25,7 +25,7 @@ Section definitions.
Context `{ghost_mapG Σ K V}.
Definition ghost_map_auth_def (γ : gname) (q : Qp) (m : gmap K V) : iProp Σ :=
own γ (gmap_view_auth (V:=leibnizO V) q m).
own γ (gmap_view_auth (V:=leibnizO V) (DfracOwn q) m).
Definition ghost_map_auth_aux : seal (@ghost_map_auth_def). Proof. by eexists. Qed.
Definition ghost_map_auth := ghost_map_auth_aux.(unseal).
Definition ghost_map_auth_eq : @ghost_map_auth = @ghost_map_auth_def := ghost_map_auth_aux.(seal_eq).
......@@ -117,7 +117,7 @@ Section lemmas.
(** Make an element read-only. *)
Lemma ghost_map_elem_persist k γ dq v :
k [γ]{dq} v == k [γ] v.
Proof. unseal. iApply own_update. apply gmap_view_persist. Qed.
Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
(** * Lemmas about [ghost_map_auth] *)
Lemma ghost_map_alloc_strong P m :
......@@ -125,7 +125,7 @@ Section lemmas.
|==> γ, P γ⌝ ghost_map_auth γ 1 m [ map] k v m, k [γ] v.
Proof.
unseal. intros.
iMod (own_alloc_strong (gmap_view_auth (V:=leibnizO V) 1 ) P)
iMod (own_alloc_strong (gmap_view_auth (V:=leibnizO V) (DfracOwn 1) ) P)
as (γ) "[% Hauth]"; first done.
{ apply gmap_view_auth_valid. }
iExists γ. iSplitR; first done.
......@@ -165,14 +165,14 @@ Section lemmas.
Lemma ghost_map_auth_valid γ q m : ghost_map_auth γ q m - q 1%Qp.
Proof.
unseal. iIntros "Hauth".
iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_frac_valid.
iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_dfrac_valid.
done.
Qed.
Lemma ghost_map_auth_valid_2 γ q1 q2 m1 m2 :
ghost_map_auth γ q1 m1 - ghost_map_auth γ q2 m2 - (q1 + q2 1)%Qp m1 = m2.
Proof.
unseal. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_auth_frac_op_valid_L.
iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_auth_dfrac_op_valid_L.
done.
Qed.
Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
......@@ -188,7 +188,7 @@ Section lemmas.
ghost_map_auth γ q m - k [γ]{dq} v - m !! k = Some v.
Proof.
unseal. iIntros "Hauth Hel".
iDestruct (own_valid_2 with "Hauth Hel") as %[?[??]]%gmap_view_both_frac_valid_L.
iDestruct (own_valid_2 with "Hauth Hel") as %[?[??]]%gmap_view_both_dfrac_valid_L.
eauto.
Qed.
......
......@@ -51,7 +51,7 @@ Global Instance: Params (@ownD) 3 := {}.
Definition wsat `{!invGS Σ} : iProp Σ :=
locked ( I : gmap positive (iProp Σ),
own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I))
own invariant_name (gmap_view_auth (DfracOwn 1) (invariant_unfold <$> I))
[ map] i Q I, Q ownD {[i]} ownE {[i]})%I.
Section wsat.
......@@ -103,7 +103,7 @@ Lemma ownD_singleton_twice i : ownD {[i]} ∗ ownD {[i]} ⊢ False.
Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I))
own invariant_name (gmap_view_auth (DfracOwn 1) (invariant_unfold <$> I))
own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P))
Q, I !! i = Some Q (Q P).
Proof.
......@@ -185,7 +185,7 @@ End wsat.
Lemma wsat_alloc `{!invGpreS Σ} : |==> _ : invGS Σ, wsat ownE .
Proof.
iIntros.
iMod (own_alloc (gmap_view_auth 1 )) as (γI) "HI";
iMod (own_alloc (gmap_view_auth (DfracOwn 1) )) as (γI) "HI";
first by apply gmap_view_auth_valid.
iMod (own_alloc (CoPset )) as (γE) "HE"; first done.
iMod (own_alloc (GSet )) as (γD) "HD"; first done.
......
Supports Markdown
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