Commit d6881996 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

gmap_view and ghost_map supports persisting the authorative element

parent 12925885
Pipeline #55773 passed with stage
in 18 minutes and 21 seconds
......@@ -9,11 +9,12 @@ Coq 8.11 is no longer supported in this version of Iris.
**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 and `ghost_map` 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
......@@ -153,11 +154,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, gmap_view, and ghost_map 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/\bghost_map_elem_frac_ne\b/ghost_map_elem_dfrac_ne/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,6 +403,10 @@ Section lemmas.
rewrite union_delete_insert //.
Qed.
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_persist k dq v :
gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
Proof.
......
......@@ -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.
......
......@@ -97,8 +97,8 @@ Section definitions.
(* The [⊆] is used to avoid assigning ghost information to the locations in
the initial heap (see [gen_heap_init]). *)
dom _ m dom (gset L) σ
ghost_map_auth (gen_heap_name hG) 1 σ
ghost_map_auth (gen_meta_name hG) 1 m.
ghost_map_auth (gen_heap_name hG) (DfracOwn 1) σ
ghost_map_auth (gen_meta_name hG) (DfracOwn 1) m.
Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
l [gen_heap_name hG]{dq} v.
......@@ -168,7 +168,7 @@ Section gen_heap.
Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
¬ (dq1 dq2) l1 {dq1} v1 - l2 {dq2} v2 - l1 l2.
Proof. rewrite mapsto_eq. apply ghost_map_elem_frac_ne. Qed.
Proof. rewrite mapsto_eq. apply ghost_map_elem_dfrac_ne. Qed.
Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 v1 - l2 {dq2} v2 - l1 l2.
Proof. rewrite mapsto_eq. apply ghost_map_elem_ne. Qed.
......
......@@ -24,8 +24,8 @@ Proof. solve_inG. Qed.
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).
Definition ghost_map_auth_def (γ : gname) (dq : dfrac) (m : gmap K V) : iProp Σ :=
own γ (gmap_view_auth (V:=leibnizO V) dq 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).
......@@ -54,7 +54,7 @@ Local Ltac unseal := rewrite
Section lemmas.
Context `{ghost_mapG Σ K V}.
Implicit Types (k : K) (v : V) (dq : dfrac) (q : Qp) (m : gmap K V).
Implicit Types (k : K) (v : V) (dp dq : dfrac) (q : Qp) (m : gmap K V).
(** * Lemmas about the map elements *)
Global Instance ghost_map_elem_timeless k γ dq v : Timeless (k [γ]{dq} v).
......@@ -104,7 +104,7 @@ Section lemmas.
unseal. iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
Qed.
Lemma ghost_map_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
Lemma ghost_map_elem_dfrac_ne γ k1 k2 dq1 dq2 v1 v2 :
¬ (dq1 dq2) k1 [γ]{dq1} v1 - k2 [γ]{dq2} v2 - k1 k2.
Proof.
iIntros (?) "H1 H2"; iIntros (->).
......@@ -112,7 +112,12 @@ Section lemmas.
Qed.
Lemma ghost_map_elem_ne γ k1 k2 dq2 v1 v2 :
k1 [γ] v1 - k2 [γ]{dq2} v2 - k1 k2.
Proof. apply ghost_map_elem_frac_ne. apply: exclusive_l. Qed.
Proof. apply ghost_map_elem_dfrac_ne. apply: exclusive_l. Qed.
(** Make an element read-only. *)
Lemma ghost_map_auth_persist γ dq m :
ghost_map_auth γ dq m == ghost_map_auth γ DfracDiscarded m.
Proof. unseal. iApply own_update. apply gmap_view_auth_persist. Qed.
(** Make an element read-only. *)
Lemma ghost_map_elem_persist k γ dq v :
......@@ -122,10 +127,10 @@ Section lemmas.
(** * Lemmas about [ghost_map_auth] *)
Lemma ghost_map_alloc_strong P m :
pred_infinite P
|==> γ, P γ⌝ ghost_map_auth γ 1 m [ map] k v m, k [γ] v.
|==> γ, P γ⌝ ghost_map_auth γ (DfracOwn 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.
......@@ -137,46 +142,46 @@ Section lemmas.
Qed.
Lemma ghost_map_alloc_strong_empty P :
pred_infinite P
|==> γ, P γ⌝ ghost_map_auth γ 1 ( : gmap K V).
|==> γ, P γ⌝ ghost_map_auth γ (DfracOwn 1) ( : gmap K V).
Proof.
intros. iMod (ghost_map_alloc_strong P ) as (γ) "(% & Hauth & _)"; eauto.
Qed.
Lemma ghost_map_alloc m :
|==> γ, ghost_map_auth γ 1 m [ map] k v m, k [γ] v.
|==> γ, ghost_map_auth γ (DfracOwn 1) m [ map] k v m, k [γ] v.
Proof.
iMod (ghost_map_alloc_strong (λ _, True) m) as (γ) "[_ Hmap]".
- by apply pred_infinite_True.
- eauto.
Qed.
Lemma ghost_map_alloc_empty :
|==> γ, ghost_map_auth γ 1 ( : gmap K V).
|==> γ, ghost_map_auth γ (DfracOwn 1) ( : gmap K V).
Proof.
intros. iMod (ghost_map_alloc ) as (γ) "(Hauth & _)"; eauto.
Qed.
Global Instance ghost_map_auth_timeless γ q m : Timeless (ghost_map_auth γ q m).
Global Instance ghost_map_auth_timeless γ dq m : Timeless (ghost_map_auth γ dq m).
Proof. unseal. apply _. Qed.
Global Instance ghost_map_auth_fractional γ m : Fractional (λ q, ghost_map_auth γ q m)%I.
Global Instance ghost_map_auth_fractional γ m : Fractional (λ q, ghost_map_auth γ (DfracOwn q) m)%I.
Proof. intros p q. unseal. rewrite -own_op gmap_view_auth_frac_op //. Qed.
Global Instance ghost_map_auth_as_fractional γ q m :
AsFractional (ghost_map_auth γ q m) (λ q, ghost_map_auth γ q m)%I q.
AsFractional (ghost_map_auth γ (DfracOwn q) m) (λ q, ghost_map_auth γ (DfracOwn q) m)%I q.
Proof. split; first done. apply _. Qed.
Lemma ghost_map_auth_valid γ q m : ghost_map_auth γ q m - q 1%Qp.
Lemma ghost_map_auth_valid γ dq m : ghost_map_auth γ dq m - dq.
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.
Lemma ghost_map_auth_valid_2 γ dq1 dq2 m1 m2 :
ghost_map_auth γ dq1 m1 - ghost_map_auth γ dq2 m2 - (dq1 dq2) 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 :
ghost_map_auth γ q1 m1 - ghost_map_auth γ q2 m2 - m1 = m2.
Lemma ghost_map_auth_agree γ dq1 dq2 m1 m2 :
ghost_map_auth γ dq1 m1 - ghost_map_auth γ dq2 m2 - m1 = m2.
Proof.
iIntros "H1 H2".
iDestruct (ghost_map_auth_valid_2 with "H1 H2") as %[_ ?].
......@@ -184,24 +189,24 @@ Section lemmas.
Qed.
(** * Lemmas about the interaction of [ghost_map_auth] with the elements *)
Lemma ghost_map_lookup {γ q m k dq v} :
ghost_map_auth γ q m - k [γ]{dq} v - m !! k = Some v.
Lemma ghost_map_lookup {γ dp m k dq v} :
ghost_map_auth γ dp 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.
Lemma ghost_map_insert {γ m} k v :
m !! k = None
ghost_map_auth γ 1 m == ghost_map_auth γ 1 (<[k := v]> m) k [γ] v.
ghost_map_auth γ (DfracOwn 1) m == ghost_map_auth γ (DfracOwn 1) (<[k := v]> m) k [γ] v.
Proof.
unseal. intros ?. rewrite -own_op.
iApply own_update. apply: gmap_view_alloc; done.
Qed.
Lemma ghost_map_insert_persist {γ m} k v :
m !! k = None
ghost_map_auth γ 1 m == ghost_map_auth γ 1 (<[k := v]> m) k [γ] v.
ghost_map_auth γ (DfracOwn 1) m == ghost_map_auth γ (DfracOwn 1) (<[k := v]> m) k [γ] v.
Proof.
iIntros (?) "Hauth".
iMod (ghost_map_insert k with "Hauth") as "[$ Helem]"; first done.
......@@ -209,22 +214,22 @@ Section lemmas.
Qed.
Lemma ghost_map_delete {γ m k v} :
ghost_map_auth γ 1 m - k [γ] v == ghost_map_auth γ 1 (delete k m).
ghost_map_auth γ (DfracOwn 1) m - k [γ] v == ghost_map_auth γ (DfracOwn 1) (delete k m).
Proof.
unseal. apply bi.wand_intro_r. rewrite -own_op.
iApply own_update. apply: gmap_view_delete.
Qed.
Lemma ghost_map_update {γ m k v} w :
ghost_map_auth γ 1 m - k [γ] v == ghost_map_auth γ 1 (<[k := w]> m) k [γ] w.
ghost_map_auth γ (DfracOwn 1) m - k [γ] v == ghost_map_auth γ (DfracOwn 1) (<[k := w]> m) k [γ] w.
Proof.
unseal. apply bi.wand_intro_r. rewrite -!own_op.
apply own_update. apply: gmap_view_update.
Qed.
(** Big-op versions of above lemmas *)
Lemma ghost_map_lookup_big {γ q m} m0 :
ghost_map_auth γ q m -
Lemma ghost_map_lookup_big {γ dq m} m0 :
ghost_map_auth γ dq m -
([ map] kv m0, k [γ] v) -
m0 m.
Proof.
......@@ -236,16 +241,16 @@ Section lemmas.
Lemma ghost_map_insert_big {γ m} m' :
m' ## m
ghost_map_auth γ 1 m ==
ghost_map_auth γ 1 (m' m) ([ map] k v m', k [γ] v).
ghost_map_auth γ (DfracOwn 1) m ==
ghost_map_auth γ (DfracOwn 1) (m' m) ([ map] k v m', k [γ] v).
Proof.
unseal. intros ?. rewrite -big_opM_own_1 -own_op.
apply own_update. apply: gmap_view_alloc_big; done.
Qed.
Lemma ghost_map_insert_persist_big {γ m} m' :
m' ## m
ghost_map_auth γ 1 m ==
ghost_map_auth γ 1 (m' m) ([ map] k v m', k [γ] v).
ghost_map_auth γ (DfracOwn 1) m ==
ghost_map_auth γ (DfracOwn 1) (m' m) ([ map] k v m', k [γ] v).
Proof.
iIntros (Hdisj) "Hauth".
iMod (ghost_map_insert_big m' with "Hauth") as "[$ Helem]"; first done.
......@@ -254,9 +259,9 @@ Section lemmas.
Qed.
Lemma ghost_map_delete_big {γ m} m0 :
ghost_map_auth γ 1 m -
ghost_map_auth γ (DfracOwn 1) m -
([ map] kv m0, k [γ] v) ==
ghost_map_auth γ 1 (m m0).
ghost_map_auth γ (DfracOwn 1) (m m0).
Proof.
iIntros "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
unseal. iApply (own_update_2 with "Hauth Hfrag").
......@@ -265,9 +270,9 @@ Section lemmas.
Theorem ghost_map_update_big {γ m} m0 m1 :
dom (gset K) m0 = dom (gset K) m1
ghost_map_auth γ 1 m -
ghost_map_auth γ (DfracOwn 1) m -
([ map] kv m0, k [γ] v) ==
ghost_map_auth γ 1 (m1 m)
ghost_map_auth γ (DfracOwn 1) (m1 m)
[ map] kv m1, k [γ] v.
Proof.
iIntros (?) "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
......
......@@ -44,7 +44,7 @@ Section definitions.
Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
R, proph_resolves_in_list R pvs
dom (gset _) R ps ghost_map_auth (proph_map_name pG) 1 R.
dom (gset _) R ps ghost_map_auth (proph_map_name pG) (DfracOwn 1) R.
Definition proph_def (p : P) (vs : list V) : iProp Σ :=
p [proph_map_name pG] vs.
......
......@@ -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))