Merge branch 'ralf/gen_heap' into 'master'

clarify the intended use of gen_heap, and rename gen_heap_ctx -> gen_heap_interp

See merge request iris/iris!542

CHANGELOG.md

@@ -92,7 +92,10 @@ With this release, we dropped support for Coq 8.9.
   but should be applied to `iProp`. This avoids clients from having to push
   through the `iProp`/`iPreProp`-isomorphism themselves, which is now handled
   once and for all by the `own` construction.
-
+* Rename `gen_heap_ctx` to `gen_heap_interp`, since it is meant to be used in
+  the state interpretation of WP and since `_ctx` is elsewhere used as a suffix
+  indicating "this is a persistent assumption that clients should always have in
+  their context". Likewise, rename `proph_map_ctx` to `proph_map_interp`.
 
 **Changes in `program_logic`:**
 
@@ -113,6 +116,9 @@ s/\b(excl|frac|ufrac)_auth_agreeL/\1_auth_agree_L/g
 # auth_both_valid
 s/\bauth_both_valid\b/auth_both_valid_discrete/g
 s/\bauth_both_frac_valid\b/auth_both_frac_valid_discrete/g
+# gen_heap_ctx and proph_map_ctx
+s/\bgen_heap_ctx\b/gen_heap_interp/g
+s/\bproph_map_ctx\b/proph_map_interp/g
 EOF
 ```
 

theories/base_logic/lib/gen_heap.v

@@ -6,15 +6,23 @@ From iris.base_logic.lib Require Export own.
 From iris Require Import options.
 Import uPred.
 
-(** This file provides a generic mechanism for a point-to connective [l ↦{q} v]
-with fractional permissions (where [l : L] and [v : V] over some abstract type
-[L] for locations and [V] for values). This mechanism can be plugged into a
-language by using the heap invariant [gen_heap_ctx σ] where [σ : gmap L V]. See
-heap-lang for an example.
-
-Next to the point-to connective [l ↦{q} v], which keeps track of the value [v]
-of a location [l], this mechanism allows one to attach "meta" or "ghost" data to
-locations. This is done as follows:
+(** This file provides a generic mechanism for a language-level point-to
+connective [l ↦{q} v] reflecting the physical heap.  This library is designed to
+be used as a singleton (i.e., with only a single instance existing in any
+proof), with the [gen_heapG] typeclass providing the ghost names of that unique
+instance.  That way, [mapsto] does not need an explicit [gname] parameter.
+This mechanism can be plugged into a language and related to the physical heap
+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].
+
+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 ↦{q} v],
+which keeps track of the value [v] of a location [l], this library also provides
+a way to attach "meta" or "ghost" data to locations. This is done as follows:
 
 - When one allocates a location, in addition to the point-to connective [l ↦ v],
   one also obtains the token [meta_token l ⊤]. This token is an exclusive
@@ -40,24 +48,22 @@ these can be matched up with the invariant namespaces. *)
 
 (** To implement this mechanism, we use three resource algebras:
 
-- An authoritative RA over [gmap L (fracR * agreeR V)], which keeps track of the
-  values of locations.
-- An authoritative RA over [gmap L (agree gname)], which keeps track of the meta
-  information of locations. This RA introduces an indirection, it keeps track of
-  a ghost name for each location.
+- A [gmap_view L V], which keeps track of the values of locations.
+- A [gmap_view L gname], which keeps track of the meta information of
+  locations. More specifically, this RA introduces an indirection: it keeps
+  track of a ghost name for each location.
 - The ghost names in the aforementioned authoritative RA refer to namespace maps
   [namespace_map (agree positive)], which store the actual meta information.
   This indirection is needed because we cannot perform frame preserving updates
   in an authoritative fragment without owning the full authoritative element
-  (in other words, without the indirection [meta_set] would need [gen_heap_ctx]
+  (in other words, without the indirection [meta_set] would need [gen_heap_interp]
   as a premise).
+ *)
 
-Note that in principle we could have used one big authoritative RA to keep track
-of both values and ghost names for meta information, for example:
-[gmap L (option (fracR * agreeR V) ∗ option (agree gname)]. Due to the [option]s,
-this RA would be quite inconvenient to deal with. *)
+(** The CMRAs we need, and the global ghost names we are using.
 
-(** The CMRA we need. *)
+Typically, the adequacy theorem will use [gen_heap_init] to obtain an instance
+of this class; everything else should assume it as a premise.  *)
 Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_inG :> inG Σ (gmap_viewR L (leibnizO V));
   gen_meta_inG :> inG Σ (gmap_viewR L gnameO);
@@ -87,7 +93,7 @@ Proof. solve_inG. Qed.
 Section definitions.
   Context `{Countable L, hG : !gen_heapG L V Σ}.
 
-  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := ∃ m : gmap L gname,
+  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) σ ⌝ ∧
@@ -125,7 +131,7 @@ Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
 Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
-  ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ.
+  ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
 Proof.
   iMod (own_alloc (gmap_view_auth (σ : gmap L (leibnizO V)))) as (γh) "Hh".
   { exact: gmap_view_auth_valid. }
@@ -257,9 +263,9 @@ Section gen_heap.
   (** Update lemmas *)
   Lemma gen_heap_alloc σ l v :
     σ !! l = None →
-    gen_heap_ctx σ ==∗ gen_heap_ctx (<[l:=v]>σ) ∗ l ↦ v ∗ meta_token l ⊤.
+    gen_heap_interp σ ==∗ gen_heap_interp (<[l:=v]>σ) ∗ l ↦ v ∗ meta_token l ⊤.
   Proof.
-    iIntros (Hσl). rewrite /gen_heap_ctx mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
+    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. }
@@ -275,8 +281,8 @@ Section gen_heap.
 
   Lemma gen_heap_alloc_gen σ σ' :
     σ' ##ₘ σ →
-    gen_heap_ctx σ ==∗
-    gen_heap_ctx (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤).
+    gen_heap_interp σ ==∗
+    gen_heap_interp (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤).
   Proof.
     revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
     { rewrite left_id_L. auto. }
@@ -287,19 +293,19 @@ Section gen_heap.
       first by apply lookup_union_None.
   Qed.
 
-  Lemma gen_heap_valid σ l q v : gen_heap_ctx σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
+  Lemma gen_heap_valid σ l q v : gen_heap_interp σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
-    rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    rewrite /gen_heap_interp mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
     iPureIntro. done.
   Qed.
 
   Lemma gen_heap_update σ l v1 v2 :
-    gen_heap_ctx σ -∗ l ↦ v1 ==∗ gen_heap_ctx (<[l:=v2]>σ) ∗ l ↦ v2.
+    gen_heap_interp σ -∗ l ↦ v1 ==∗ gen_heap_interp (<[l:=v2]>σ) ∗ l ↦ v2.
   Proof.
     iDestruct 1 as (m Hσm) "[Hσ Hm]".
-    iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    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. }

theories/base_logic/lib/proph_map.v

@@ -41,7 +41,7 @@ Section definitions.
   Definition proph_resolves_in_list R pvs :=
     map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
 
-  Definition proph_map_ctx pvs (ps : gset P) : iProp Σ :=
+  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) R))%I.
@@ -73,7 +73,7 @@ Section list_resolves.
 End list_resolves.
 
 Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
-  ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps.
+  ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_interp pvs ps.
 Proof.
   iMod (own_alloc (gmap_view_auth ∅)) as (γ) "Hh".
   { apply gmap_view_auth_valid. }
@@ -104,8 +104,8 @@ Section proph_map.
 
   Lemma proph_map_new_proph p ps pvs :
     p ∉ ps →
-    proph_map_ctx pvs ps ==∗
-    proph_map_ctx pvs ({[p]} ∪ ps) ∗ proph p (proph_list_resolves pvs p).
+    proph_map_interp pvs ps ==∗
+    proph_map_interp pvs ({[p]} ∪ ps) ∗ proph p (proph_list_resolves pvs p).
   Proof.
     iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
     rewrite proph_eq /proph_def.
@@ -120,11 +120,11 @@ Section proph_map.
   Qed.
 
   Lemma proph_map_resolve_proph p v pvs ps vs :
-    proph_map_ctx ((p,v) :: pvs) ps ∗ proph p vs ==∗
-    ∃vs', ⌜vs = v::vs'⌝ ∗ proph_map_ctx pvs ps ∗ proph p vs'.
+    proph_map_interp ((p,v) :: pvs) ps ∗ proph p vs ==∗
+    ∃vs', ⌜vs = v::vs'⌝ ∗ proph_map_interp pvs ps ∗ proph p vs'.
   Proof.
     iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
-    rewrite /proph_map_ctx proph_eq /proph_def.
+    rewrite /proph_map_interp proph_eq /proph_def.
     iDestruct (own_valid_2 with "H● Hp") as %[_ HR]%gmap_view_both_valid_L.
     assert (vs = v :: proph_list_resolves pvs p) as ->.
     { rewrite (Hres p vs HR). simpl. by rewrite decide_True. }

theories/heap_lang/adequacy.v

@@ -25,7 +25,7 @@ Proof.
   iMod (inv_heap_init loc (option val)) as (?) ">Hi".
   iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
   iModIntro. iExists
-    (λ σ κs, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
+    (λ σ κs, (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I),
     (λ _, True%I).
   iFrame. iApply (Hwp (HeapG _ _ _ _ _)). done.
 Qed.

theories/heap_lang/primitive_laws.v

@@ -22,7 +22,7 @@ Class heapG Σ := HeapG {
 Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
   iris_invG := heapG_invG;
   state_interp σ κs _ :=
-    (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I;
+    (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I;
   fork_post _ := True%I;
 }.
 

theories/heap_lang/total_adequacy.v

@@ -14,7 +14,7 @@ Proof.
   iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
   iModIntro.
   iExists
-    (λ σ κs _, (gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
+    (λ σ κs _, (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I),
     (λ _, True%I); iFrame.
   iApply (Hwp (HeapG _ _ _ _ _)). done.
 Qed.