From 543b9218e4a5e98b502a12d9ed6560fe2ca00533 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 6 Mar 2021 13:19:40 +0100
Subject: [PATCH] port gen_heap to ghost_map

---
 iris/base_logic/lib/gen_heap.v | 99 +++++++++++++---------------------
 1 file changed, 37 insertions(+), 62 deletions(-)

diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 51ecbe6ee..4f59ad506 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -1,9 +1,10 @@
 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. }
-- 
GitLab