Merge branch 'ralf/ghost-map' into 'master'

Use ghost_map in proph_map and gen_heap

See merge request iris/iris!645

iris/base_logic/lib/gen_heap.v

 From stdpp Require Export namespaces.
-From iris.algebra Require Import gmap_view namespace_map agree frac.
+From iris.algebra Require Import namespace_map agree frac.
 From iris.algebra Require Export dfrac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import ghost_map.
 From iris.prelude Require Import options.
 Import uPred.
 
@@ -17,8 +18,9 @@ by using [gen_heap_interp σ] in the state interpretation of the weakest
 precondition. See heap-lang for an example.
 
 If you are looking for a library providing "ghost heaps" independent of the
-physical state, you will likely want explicit ghost names and are thus better
-off using [algebra.lib.gmap_view] together with [base_logic.lib.own].
+physical state, you will likely want explicit ghost names to disambiguate
+multiple heaps and are thus better off using [ghost_map], or (if you need more
+flexibility), directly using the underlying [algebra.lib.gmap_view].
 
 This library is generic in the types [L] for locations and [V] for values and
 supports fractional permissions.  Next to the point-to connective [l ↦{dq} v],
@@ -64,8 +66,8 @@ these can be matched up with the invariant namespaces. *)
 (** The CMRAs we need, and the global ghost names we are using. *)
 
 Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  gen_heap_preG_inG :> inG Σ (gmap_viewR L (leibnizO V));
-  gen_meta_preG_inG :> inG Σ (gmap_viewR L gnameO);
+  gen_heap_preG_inG :> ghost_mapG Σ L V;
+  gen_meta_preG_inG :> ghost_mapG Σ L gname;
   gen_meta_data_preG_inG :> inG Σ (namespace_mapR (agreeR positiveO));
 }.
 
@@ -79,8 +81,8 @@ Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
 Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
 
 Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
-  GFunctor (gmap_viewR L (leibnizO V));
-  GFunctor (gmap_viewR L gnameO);
+  ghost_mapΣ L V;
+  ghost_mapΣ L gname;
   GFunctor (namespace_mapR (agreeR positiveO))
 ].
 
@@ -94,25 +96,24 @@ Section definitions.
   Definition gen_heap_interp (σ : gmap L V) : iProp Σ := ∃ m : gmap L gname,
     (* The [⊆] is used to avoid assigning ghost information to the locations in
     the initial heap (see [gen_heap_init]). *)
-    ⌜ dom _ m ⊆ dom (gset L) σ ⌝ ∧
-    own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V))) ∗
-    own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L gnameO)).
+    ⌜ dom _ m ⊆ dom (gset L) σ ⌝ ∗
+    ghost_map_auth (gen_heap_name hG) 1 σ ∗
+    ghost_map_auth (gen_meta_name hG) 1 m.
 
   Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
-    own (gen_heap_name hG) (gmap_view_frag l dq (v : leibnizO V)).
+    l ↪[gen_heap_name hG]{dq} v.
   Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
   Definition mapsto := mapsto_aux.(unseal).
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
 
   Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
-    ∃ γm, own (gen_meta_name hG) (gmap_view_frag l DfracDiscarded γm) ∗
-          own γm (namespace_map_token E).
+    ∃ γm, l ↪[gen_meta_name hG]□ γm ∗ own γm (namespace_map_token E).
   Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
   Definition meta_token := meta_token_aux.(unseal).
   Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
 
   Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
-    ∃ γm, own (gen_meta_name hG) (gmap_view_frag l DfracDiscarded γm) ∗
+    ∃ γm, l ↪[gen_meta_name hG]□ γm ∗
           own γm (namespace_map_data N (to_agree (encode x))).
   Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
   Definition meta := meta_aux.(unseal).
@@ -144,64 +145,43 @@ Section gen_heap.
   Global Instance mapsto_timeless l dq v : Timeless (l ↦{dq} v).
   Proof. rewrite mapsto_eq. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{#q} v)%I.
-  Proof.
-    intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_add //.
-  Qed.
+  Proof. rewrite mapsto_eq. apply _. Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
-  Proof. split; [done|]. apply _. Qed.
+  Proof. rewrite mapsto_eq. apply _. Qed.
   Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
   Proof. rewrite mapsto_eq. apply _. Qed.
 
   Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
-  Proof.
-    rewrite mapsto_eq. iIntros "Hl".
-    iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
-  Qed.
+  Proof. rewrite mapsto_eq. apply ghost_map_elem_valid. Qed.
   Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
-  Proof.
-    rewrite mapsto_eq. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
-    auto.
-  Qed.
+  Proof. rewrite mapsto_eq. apply ghost_map_elem_valid_2. Qed.
   (** Almost all the time, this is all you really need. *)
   Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-  Proof.
-    iIntros "H1 H2".
-    iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?].
-    done.
-  Qed.
+  Proof. rewrite mapsto_eq. apply ghost_map_elem_agree. Qed.
 
   Lemma mapsto_combine l dq1 dq2 v1 v2 :
     l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
-  Proof.
-    iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
-    iCombine "Hl1 Hl2" as "Hl".
-    rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_op.
-    auto.
-  Qed.
+  Proof. rewrite mapsto_eq. apply ghost_map_elem_combine. Qed.
 
   Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
     ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
-  Proof.
-    iIntros (?) "Hl1 Hl2"; iIntros (->).
-    by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
-  Qed.
+  Proof. rewrite mapsto_eq. apply ghost_map_elem_frac_ne. Qed.
   Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
-  Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
+  Proof. rewrite mapsto_eq. apply ghost_map_elem_ne. Qed.
 
   (** Permanently turn any points-to predicate into a persistent
       points-to predicate. *)
   Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
-  Proof. rewrite mapsto_eq. apply own_update, gmap_view_persist. Qed.
+  Proof. rewrite mapsto_eq. apply ghost_map_elem_persist. Qed.
 
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
-  Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.
+  Proof. rewrite meta_token_eq. apply _. Qed.
   Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
-  Proof. rewrite meta_eq /meta_def. apply _. Qed.
+  Proof. rewrite meta_eq. apply _. Qed.
   Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
-  Proof. rewrite meta_eq /meta_def. apply _. Qed.
+  Proof. rewrite meta_eq. apply _. Qed.
 
   Lemma meta_token_union_1 l E1 E2 :
     E1 ## E2 → meta_token l (E1 ∪ E2) -∗ meta_token l E1 ∗ meta_token l E2.
@@ -215,7 +195,7 @@ Section gen_heap.
   Proof.
     rewrite meta_token_eq /meta_token_def.
     iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
-    iDestruct (own_valid_2 with "Hγm1 Hγm2") as %[_ ->]%gmap_view_frag_op_valid_L.
+    iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
     iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op.
     iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1".
   Qed.
@@ -238,7 +218,7 @@ Section gen_heap.
   Proof.
     rewrite meta_eq /meta_def.
     iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
-    iDestruct (own_valid_2 with "Hγm1 Hγm2") as %[_ ->]%gmap_view_frag_op_valid_L.
+    iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
     move=> /to_agree_op_inv_L. naive_solver.
@@ -258,13 +238,11 @@ Section gen_heap.
   Proof.
     iIntros (Hσl). rewrite /gen_heap_interp mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
     iDestruct 1 as (m Hσm) "[Hσ Hm]".
-    iMod (own_update with "Hσ") as "[Hσ Hl]".
-    { eapply (gmap_view_alloc _ l (DfracOwn 1)); done. }
+    iMod (ghost_map_insert l with "Hσ") as "[Hσ Hl]"; first done.
     iMod (own_alloc (namespace_map_token ⊤)) as (γm) "Hγm".
     { apply namespace_map_token_valid. }
-    iMod (own_update with "Hm") as "[Hm Hlm]".
-    { eapply (gmap_view_alloc _ l DfracDiscarded); last done.
-      move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
+    iMod (ghost_map_insert_persist l with "Hm") as "[Hm Hlm]".
+    { move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
     iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
     iExists (<[l:=γm]> m). iFrame. iPureIntro.
     rewrite !dom_insert_L. set_solver.
@@ -288,7 +266,7 @@ Section gen_heap.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
     rewrite /gen_heap_interp mapsto_eq.
-    by iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
+    by iDestruct (ghost_map_lookup with "Hσ Hl") as %?.
   Qed.
 
   Lemma gen_heap_update σ l v1 v2 :
@@ -296,9 +274,8 @@ Section gen_heap.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ Hm]".
     iIntros "Hl". rewrite /gen_heap_interp mapsto_eq /mapsto_def.
-    iDestruct (own_valid_2 with "Hσ Hl") as %[_ Hl]%gmap_view_both_valid_L.
-    iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
-    { eapply gmap_view_update. }
+    iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl.
+    iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
     iModIntro. iFrame "Hl". iExists m. iFrame.
     iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
     rewrite dom_insert_L. set_solver.
@@ -314,10 +291,8 @@ Lemma gen_heap_init_names `{Countable L, !gen_heapPreG L V Σ} σ :
     let hG := GenHeapG L V Σ γh γm in
     gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
 Proof.
-  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (leibnizO V)))) as (γh) "Hh".
-  { exact: gmap_view_auth_valid. }
-  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L gnameO))) as (γm) "Hm".
-  { exact: gmap_view_auth_valid. }
+  iMod (ghost_map_alloc_empty (V:=V)) as (γh) "Hh".
+  iMod (ghost_map_alloc_empty (V:=gname)) as (γm) "Hm".
   iExists γh, γm.
   iAssert (gen_heap_interp (hG:=GenHeapG _ _ _ γh γm) ∅) with "[Hh Hm]" as "Hinterp".
   { iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }

iris/base_logic/lib/ghost_map.v

@@ -95,23 +95,20 @@ Section lemmas.
     unseal. iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
   Qed.
 
-  Lemma ghost_map_elem_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
+  Lemma ghost_map_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
     ¬ ✓ (dq1 ⋅ dq2) → k1 ↪[γ]{dq1} v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
   Proof.
     iIntros (?) "H1 H2"; iIntros (->).
     by iDestruct (ghost_map_elem_valid_2 with "H1 H2") as %[??].
   Qed.
-  Lemma ghost_map_elem_elem_ne γ k1 k2 dq2 v1 v2 :
+  Lemma ghost_map_elem_ne γ k1 k2 dq2 v1 v2 :
     k1 ↪[γ] v1 -∗ k2 ↪[γ]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
-  Proof. apply ghost_map_elem_elem_frac_ne. apply: exclusive_l. Qed.
+  Proof. apply ghost_map_elem_frac_ne. apply: exclusive_l. Qed.
 
   (** Make an element read-only. *)
-  Lemma ghost_map_elem_persist k γ q v :
-    k ↪[γ]{#q} v ==∗ k ↪[γ]□ v.
-  Proof.
-    unseal. iApply own_update.
-    apply gmap_view_persist.
-  Qed.
+  Lemma ghost_map_elem_persist k γ dq v :
+    k ↪[γ]{dq} v ==∗ k ↪[γ]□ v.
+  Proof. unseal. iApply own_update. apply gmap_view_persist. Qed.
 
   (** * Lemmas about [ghost_map_auth] *)
   Lemma ghost_map_alloc_strong P m :
@@ -193,6 +190,14 @@ Section lemmas.
     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.
+  Proof.
+    iIntros (?) "Hauth".
+    iMod (ghost_map_insert k with "Hauth") as "[$ Helem]"; first done.
+    iApply ghost_map_elem_persist. done.
+  Qed.
 
   Lemma ghost_map_delete {γ m k v} :
     ghost_map_auth γ 1 m -∗ k ↪[γ] v ==∗ ghost_map_auth γ 1 (delete k m).

iris/base_logic/lib/proph_map.v

 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import gmap_view list.
 From iris.base_logic.lib Require Export own.
+From iris.base_logic.lib Require Import ghost_map.
 From iris.prelude Require Import options.
 Import uPred.
 
@@ -9,7 +9,7 @@ Definition proph_val_list (P V : Type) := list (P * V).
 
 (** The CMRA we need. *)
 Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} := {
-  proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V))
+  proph_map_preG_inG :> ghost_mapG Σ P (list V)
 }.
 
 Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
@@ -19,7 +19,7 @@ Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
 Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
 
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
-  #[GFunctor (gmap_viewR P (listO $ leibnizO V))].
+  #[ghost_mapΣ P (list V)].
 
 Global Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
   subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
@@ -44,11 +44,10 @@ Section definitions.
 
   Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
     (∃ R, ⌜proph_resolves_in_list R pvs ∧
-          dom (gset _) R ⊆ ps⌝ ∗
-          own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO V) 1 R))%I.
+          dom (gset _) R ⊆ ps⌝ ∗ ghost_map_auth (proph_map_name pG) 1 R)%I.
 
   Definition proph_def (p : P) (vs : list V) : iProp Σ :=
-    own (proph_map_name pG) (gmap_view_frag (V:=listO $ leibnizO V) p (DfracOwn 1) vs).
+    p ↪[proph_map_name pG] vs.
 
   Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
   Definition proph := proph_aux.(unseal).
@@ -76,8 +75,7 @@ End list_resolves.
 Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
   ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_interp pvs ps.
 Proof.
-  iMod (own_alloc (gmap_view_auth 1 ∅)) as (γ) "Hh".
-  { apply gmap_view_auth_valid. }
+  iMod (ghost_map_alloc_empty) as (γ) "Hh".
   iModIntro. iExists (ProphMapG P V PVS _ _ _ γ), ∅. iSplit; last by iFrame.
   iPureIntro. done.
 Qed.
@@ -98,9 +96,7 @@ Section proph_map.
     proph p vs1 -∗ proph p vs2 -∗ False.
   Proof.
     rewrite proph_eq /proph_def. iIntros "Hp1 Hp2".
-    iCombine "Hp1 Hp2" as "Hp".
-    iDestruct (own_valid with "Hp") as %[Hp _]%gmap_view_frag_op_valid_L.
-    done.
+    by iDestruct (ghost_map_elem_ne with "Hp1 Hp2") as %?.
   Qed.
 
   Lemma proph_map_new_proph p ps pvs :
@@ -110,9 +106,8 @@ Section proph_map.
   Proof.
     iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
     rewrite proph_eq /proph_def.
-    iMod (own_update with "H●") as "[H● H◯]".
-    { eapply (gmap_view_alloc _ p (DfracOwn 1)); last done.
-      apply (not_elem_of_dom (D:=gset P)). set_solver. }
+    iMod (ghost_map_insert p (proph_list_resolves pvs p) with "H●") as "[H● H◯]".
+    { apply (not_elem_of_dom (D:=gset P)). set_solver. }
     iModIntro. iFrame.
     iExists (<[p := proph_list_resolves pvs p]> R).
     iFrame. iPureIntro. split.
@@ -126,11 +121,10 @@ Section proph_map.
   Proof.
     iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
     rewrite /proph_map_interp proph_eq /proph_def.
-    iDestruct (own_valid_2 with "H● Hp") as %[_ HR]%gmap_view_both_valid_L.
+    iDestruct (ghost_map_lookup with "H● Hp") as %HR.
     assert (vs = v :: proph_list_resolves pvs p) as ->.
     { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
-    iMod (own_update_2 with "H● Hp") as "[H● H◯]".
-    { eapply gmap_view_update. }
+    iMod (ghost_map_update (proph_list_resolves pvs p) with "H● Hp") as "[H● H◯]".
     iModIntro. iExists (proph_list_resolves pvs p). iFrame. iSplitR.
     - iPureIntro. done.
     - iExists _. iFrame. iPureIntro. split.