Merge branch 'robbert/locations_meta' into 'master'

Add ghost data to locations

See merge request iris/iris!249

CHANGELOG.md

@@ -49,6 +49,7 @@ Changes in heap_lang:
   "administrative" reductions in the operational semantics of the language.
 * heap_lang now has support for allocating, accessing and reasoning about arrays
   (continuously allocated regions of memory).
+* One can now assign "meta" data to heap_lang locations.
 
 Changes in Coq:
 

_CoqProject

@@ -36,6 +36,7 @@ theories/algebra/coPset.v
 theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
+theories/algebra/namespace_map.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v

theories/algebra/namespace_map.v

+From iris.algebra Require Export gmap coPset local_updates.
+From stdpp Require Import namespaces.
+From iris.algebra Require Import updates.
+From iris.algebra Require Import proofmode_classes.
+Set Default Proof Using "Type".
+
+(** The camera [namespace_map A] over a camera [A] provides the connectives
+[namespace_map_data N a], which associates data [a : A] with a namespace [N],
+and [namespace_map_token E], which says that no data has been associated with
+the namespaces in the mask [E]. The important properties of this camera are:
+
+- The lemma [namespace_map_token_union] enables one to split [namespace_map_token]
+  w.r.t. disjoint union. That is, if we have [E1 ## E2], then we get
+  [namespace_map_token (E1 ∪ E2) = namespace_map_token E1 ⋅ namespace_map_token E2]
+- The lemma [namespace_map_alloc_update] provides a frame preserving update to
+  associate data to a namespace [namespace_map_token E ~~> namespace_map_data N a]
+  provided [↑N ⊆ E] and [✓ a]. *)
+
+Record namespace_map (A : Type) := NamespaceMap {
+  namespace_map_data_proj : gmap positive A;
+  namespace_map_token_proj : coPset_disj
+}.
+Add Printing Constructor namespace_map.
+Arguments NamespaceMap {_} _ _.
+Arguments namespace_map_data_proj {_} _.
+Arguments namespace_map_token_proj {_} _.
+Instance: Params (@NamespaceMap) 1 := {}.
+Instance: Params (@namespace_map_data_proj) 1 := {}.
+Instance: Params (@namespace_map_token_proj) 1 := {}.
+
+(** TODO: [positives_flatten] violates the namespace abstraction. *)
+Definition namespace_map_data {A : cmraT} (N : namespace) (a : A) : namespace_map A :=
+  NamespaceMap {[ positives_flatten N := a ]} ε.
+Definition namespace_map_token {A : cmraT} (E : coPset) : namespace_map A :=
+  NamespaceMap ∅ (CoPset E).
+Instance: Params (@namespace_map_data) 2 := {}.
+
+(* Ofe *)
+Section ofe.
+Context {A : ofeT}.
+Implicit Types x y : namespace_map A.
+
+Instance namespace_map_equiv : Equiv (namespace_map A) := λ x y,
+  namespace_map_data_proj x ≡ namespace_map_data_proj y ∧
+  namespace_map_token_proj x = namespace_map_token_proj y.
+Instance namespace_map_dist : Dist (namespace_map A) := λ n x y,
+  namespace_map_data_proj x ≡{n}≡ namespace_map_data_proj y ∧
+  namespace_map_token_proj x = namespace_map_token_proj y.
+
+Global Instance Awesome_ne : NonExpansive2 (@NamespaceMap A).
+Proof. by split. Qed.
+Global Instance Awesome_proper : Proper ((≡) ==> (=) ==> (≡)) (@NamespaceMap A).
+Proof. by split. Qed.
+Global Instance namespace_map_data_proj_ne: NonExpansive (@namespace_map_data_proj A).
+Proof. by destruct 1. Qed.
+Global Instance namespace_map_data_proj_proper :
+  Proper ((≡) ==> (≡)) (@namespace_map_data_proj A).
+Proof. by destruct 1. Qed.
+
+Definition namespace_map_ofe_mixin : OfeMixin (namespace_map A).
+Proof.
+  by apply (iso_ofe_mixin
+    (λ x, (namespace_map_data_proj x, namespace_map_token_proj x))).
+Qed.
+Canonical Structure namespace_mapC :=
+  OfeT (namespace_map A) namespace_map_ofe_mixin.
+
+Global Instance NamespaceMap_discrete a b :
+  Discrete a → Discrete b → Discrete (NamespaceMap a b).
+Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
+Global Instance namespace_map_ofe_discrete :
+  OfeDiscrete A → OfeDiscrete namespace_mapC.
+Proof. intros ? [??]; apply _. Qed.
+End ofe.
+
+Arguments namespace_mapC : clear implicits.
+
+(* Camera *)
+Section cmra.
+Context {A : cmraT}.
+Implicit Types a b : A.
+Implicit Types x y : namespace_map A.
+
+Global Instance namespace_map_data_ne i : NonExpansive (@namespace_map_data A i).
+Proof. solve_proper. Qed.
+Global Instance namespace_map_data_proper N :
+  Proper ((≡) ==> (≡)) (@namespace_map_data A N).
+Proof. solve_proper. Qed.
+Global Instance namespace_map_data_discrete N a :
+  Discrete a → Discrete (namespace_map_data N a).
+Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
+Global Instance namespace_map_token_discrete E : Discrete (@namespace_map_token A E).
+Proof. intros. apply NamespaceMap_discrete; apply _. Qed.
+
+Instance namespace_map_valid : Valid (namespace_map A) := λ x,
+  match namespace_map_token_proj x with
+  | CoPset E =>
+     ✓ (namespace_map_data_proj x) ∧
+     (* dom (namespace_map_data_proj x) ⊥ E *)
+     ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
+  | CoPsetBot => False
+  end.
+Global Arguments namespace_map_valid !_ /.
+Instance namespace_map_validN : ValidN (namespace_map A) := λ n x,
+  match namespace_map_token_proj x with
+  | CoPset E =>
+     ✓{n} (namespace_map_data_proj x) ∧
+     (* dom (namespace_map_data_proj x) ⊥ E *)
+     ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
+  | CoPsetBot => False
+  end.
+Global Arguments namespace_map_validN !_ /.
+Instance namespace_map_pcore : PCore (namespace_map A) := λ x,
+  Some (NamespaceMap (core (namespace_map_data_proj x)) ε).
+Instance namespace_map_op : Op (namespace_map A) := λ x y,
+  NamespaceMap (namespace_map_data_proj x ⋅ namespace_map_data_proj y)
+               (namespace_map_token_proj x ⋅ namespace_map_token_proj y).
+
+Definition namespace_map_valid_eq :
+  valid = λ x, match namespace_map_token_proj x with
+               | CoPset E =>
+                  ✓ (namespace_map_data_proj x) ∧
+                  (* dom (namespace_map_data_proj x) ⊥ E *)
+                  ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
+               | CoPsetBot => False
+               end := eq_refl _.
+Definition namespace_map_validN_eq :
+  validN = λ n x, match namespace_map_token_proj x with
+                  | CoPset E =>
+                     ✓{n} (namespace_map_data_proj x) ∧
+                     (* dom (namespace_map_data_proj x) ⊥ E *)
+                     ∀ i, namespace_map_data_proj x !! i = None ∨ i ∉ E
+                  | CoPsetBot => False
+                  end := eq_refl _.
+
+Lemma namespace_map_included x y :
+  x ≼ y ↔
+    namespace_map_data_proj x ≼ namespace_map_data_proj y ∧
+    namespace_map_token_proj x ≼ namespace_map_token_proj y.
+Proof.
+  split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
+  intros [[z1 Hz1] [z2 Hz2]]; exists (NamespaceMap z1 z2); split; auto.
+Qed.
+
+Lemma namespace_map_data_proj_validN n x : ✓{n} x → ✓{n} namespace_map_data_proj x.
+Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
+Lemma namespace_map_token_proj_validN n x : ✓{n} x → ✓{n} namespace_map_token_proj x.
+Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
+
+Lemma namespace_map_cmra_mixin : CmraMixin (namespace_map A).
+Proof.
+  apply cmra_total_mixin.
+  - eauto.
+  - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
+  - solve_proper.
+  - intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[??]; split; simplify_eq/=.
+    + by rewrite -Hm.
+    + intros i. by rewrite -(dist_None n) -Hm dist_None.
+  - intros [m [E|]]; rewrite namespace_map_valid_eq namespace_map_validN_eq /=
+      ?cmra_valid_validN; naive_solver eauto using 0.
+  - intros n [m [E|]]; rewrite namespace_map_validN_eq /=;
+      naive_solver eauto using cmra_validN_S.
+  - split; simpl; [by rewrite assoc|by rewrite assoc_L].
+  - split; simpl; [by rewrite comm|by rewrite comm_L].
+  - split; simpl; [by rewrite cmra_core_l|by rewrite left_id_L].
+  - split; simpl; [by rewrite cmra_core_idemp|done].
+  - intros ??; rewrite! namespace_map_included; intros [??].
+    by split; simpl; apply: cmra_core_mono. (* FIXME: apply cmra_core_mono. fails *)
+  - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite namespace_map_validN_eq /=.
+    rewrite {1}/op /cmra_op /=. case_decide; last done.
+    intros [Hm Hdisj]; split; first by eauto using cmra_validN_op_l.
+    intros i. move: (Hdisj i). rewrite lookup_op.
+    case: (m1 !! i)=> [a|]; last auto.
+    move=> []. by case: (m2 !! i). set_solver.
+  - intros n x y1 y2 ? [??]; simpl in *.
+    destruct (cmra_extend n (namespace_map_data_proj x)
+      (namespace_map_data_proj y1) (namespace_map_data_proj y2))
+      as (m1&m2&?&?&?); auto using namespace_map_data_proj_validN.
+    destruct (cmra_extend n (namespace_map_token_proj x)
+      (namespace_map_token_proj y1) (namespace_map_token_proj y2))
+      as (E1&E2&?&?&?); auto using namespace_map_token_proj_validN.
+    by exists (NamespaceMap m1 E1), (NamespaceMap m2 E2).
+Qed.
+Canonical Structure namespace_mapR :=
+  CmraT (namespace_map A) namespace_map_cmra_mixin.
+
+Global Instance namespace_map_cmra_discrete :
+  CmraDiscrete A → CmraDiscrete namespace_mapR.
+Proof.
+  split; first apply _.
+  intros [m [E|]]; rewrite namespace_map_validN_eq namespace_map_valid_eq //=.
+  naive_solver eauto using (cmra_discrete_valid m).
+Qed.
+
+Instance namespace_map_empty : Unit (namespace_map A) := NamespaceMap ε ε.
+Lemma namespace_map_ucmra_mixin : UcmraMixin (namespace_map A).
+Proof.
+  split; simpl.
+  - rewrite namespace_map_valid_eq /=. split. apply ucmra_unit_valid. set_solver.
+  - split; simpl; [by rewrite left_id|by rewrite left_id_L].
+  - do 2 constructor; [apply (core_id_core _)|done].
+Qed.
+Canonical Structure namespace_mapUR :=
+  UcmraT (namespace_map A) namespace_map_ucmra_mixin.
+
+Global Instance namespace_map_data_core_id N a :
+  CoreId a → CoreId (namespace_map_data N a).
+Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
+
+Lemma namespace_map_data_valid N a : ✓ (namespace_map_data N a) ↔ ✓ a.
+Proof. rewrite namespace_map_valid_eq /= singleton_valid. set_solver. Qed.
+Lemma namespace_map_token_valid E : ✓ (namespace_map_token E).
+Proof. rewrite namespace_map_valid_eq /=. split. done. by left. Qed.
+Lemma namespace_map_data_op N a b :
+  namespace_map_data N (a ⋅ b) = namespace_map_data N a ⋅ namespace_map_data N b.
+Proof.
+  by rewrite {2}/op /namespace_map_op /namespace_map_data /= -op_singleton left_id_L.
+Qed.
+Lemma namespace_map_data_mono N a b :
+  a ≼ b → namespace_map_data N a ≼ namespace_map_data N b.
+Proof. intros [c ->]. rewrite namespace_map_data_op. apply cmra_included_l. Qed.
+Global Instance is_op_namespace_map_data N a b1 b2 :
+  IsOp a b1 b2 →
+  IsOp' (namespace_map_data N a) (namespace_map_data N b1) (namespace_map_data N b2).
+Proof. rewrite /IsOp' /IsOp=> ->. by rewrite namespace_map_data_op. Qed.
+
+Lemma namespace_map_token_union E1 E2 :
+  E1 ## E2 →
+  namespace_map_token (E1 ∪ E2) = namespace_map_token E1 ⋅ namespace_map_token E2.
+Proof.
+  intros. by rewrite /op /namespace_map_op
+    /namespace_map_token /= coPset_disj_union // left_id_L.
+Qed.
+Lemma namespace_map_token_difference E1 E2 :
+  E1 ⊆ E2 →
+   namespace_map_token E2 = namespace_map_token E1 ⋅ namespace_map_token (E2 ∖ E1).
+Proof.
+  intros. rewrite -namespace_map_token_union; last set_solver.
+  by rewrite -union_difference_L.
+Qed.
+Lemma namespace_map_token_valid_op E1 E2 :
+  ✓ (namespace_map_token E1 ⋅ namespace_map_token E2) ↔ E1 ## E2.
+Proof.
+  rewrite namespace_map_valid_eq /= {1}/op /cmra_op /=. case_decide; last done.
+  split; [done|]; intros _. split.
+  - by rewrite left_id.
+  - intros i. rewrite lookup_op lookup_empty. auto.
+Qed.
+
+(** [↑N ⊆ E] is stronger than needed, just [positives_flatten N ∈ E] would be
+sufficient. However, we do not have convenient infrastructure to prove the
+latter, so we use the former. *)
+Lemma namespace_map_alloc_update E N a :
+  ↑N ⊆ E → ✓ a → namespace_map_token E ~~> namespace_map_data N a.
+Proof.
+  assert (positives_flatten N ∈ (↑N : coPset)).
+  { rewrite nclose_eq. apply elem_coPset_suffixes.
+    exists 1%positive. by rewrite left_id_L. }
+  intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
+  rewrite namespace_map_validN_eq /= {1}/op /cmra_op /=. case_decide; last done.
+  rewrite left_id_L {1}left_id. intros [Hmf Hdisj]; split.
+  - destruct (Hdisj (positives_flatten N)) as [Hmfi|]; last set_solver.
+    move: Hmfi. rewrite lookup_op lookup_empty left_id_L=> Hmfi.
+    intros j. rewrite lookup_op.
+    destruct (decide (positives_flatten N = j)) as [<-|].
+    + rewrite Hmfi lookup_singleton right_id_L. by apply cmra_valid_validN.
+    + by rewrite lookup_singleton_ne // left_id_L.
+  - intros j. destruct (decide (positives_flatten N = j)); first set_solver.
+    rewrite lookup_op lookup_singleton_ne //.
+    destruct (Hdisj j) as [Hmfi|?]; last set_solver.
+    move: Hmfi. rewrite lookup_op lookup_empty; auto.
+Qed.
+Lemma namespace_map_updateP P (Q : namespace_map A → Prop) N a :
+  a ~~>: P →
+  (∀ a', P a' → Q (namespace_map_data N a')) → namespace_map_data N a ~~>: Q.
+Proof.
+  intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
+  rewrite namespace_map_validN_eq /= left_id_L. intros [Hmf Hdisj].
+  destruct (Hup n (mf !! positives_flatten N)) as (a'&?&?).
+  { move: (Hmf (positives_flatten N)).
+    by rewrite lookup_op lookup_singleton Some_op_opM. }
+  exists (namespace_map_data N a'); split; first by eauto.
+  rewrite /= left_id_L. split.
+  - intros j. destruct (decide (positives_flatten N = j)) as [<-|].
+    + by rewrite lookup_op lookup_singleton Some_op_opM.
+    + rewrite lookup_op lookup_singleton_ne // left_id_L.
+      move: (Hmf j). rewrite lookup_op. eauto using cmra_validN_op_r.
+  - intros j. move: (Hdisj j).
+    rewrite !lookup_op !op_None !lookup_singleton_None. naive_solver.
+Qed.
+Lemma namespace_map_update N a b :
+  a ~~> b → namespace_map_data N a ~~> namespace_map_data N b.
+Proof.
+  rewrite !cmra_update_updateP. eauto using namespace_map_updateP with subst.
+Qed.
+End cmra.
+
+Arguments namespace_mapR : clear implicits.
+Arguments namespace_mapUR : clear implicits.

theories/base_logic/lib/gen_heap.v

-From iris.algebra Require Import auth gmap frac agree.
+From iris.algebra Require Import auth gmap frac agree namespace_map.
+From stdpp Require Export namespaces.
 From iris.base_logic.lib Require Export own.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 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:
+
+- 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
+  resource that denotes that no meta data has been associated with the
+  namespaces in the mask [⊤] for the location [l].
+- Meta data tokens can be split w.r.t. namespace masks, i.e.
+  [meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2] if [E1 ## E2].
+- Meta data can be set using the update [meta_token l E ==∗ meta l N x] provided
+  [↑N ⊆ E], and [x : A] for any countable [A]. The [meta l N x] connective is
+  persistent and denotes the knowledge that the meta data [x] has been
+  associated with namespace [N] to the location [l].
+
+To make the mechanism as flexible as possible, the [x : A] in [meta l N x] can
+be of any countable type [A]. This means that you can associate e.g. single
+ghost names, but also tuples of ghost names, etc.
+
+To further increase flexibility, the [meta l N x] and [meta_token l E]
+connectives are annotated with a namespace [N] and mask [E]. That way, one can
+assign a map of meta information to a location. This is particularly useful when
+building abstractions, then one can gradually assign more ghost information to a
+location instead of having to do all of this at once. We use namespaces so that
+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.
+- 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]
+  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. *)
+
 Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
   gmapUR L (prodR fracR (agreeR (leibnizC V))).
+Definition gen_metaUR (L : Type) `{Countable L} : ucmraT :=
+  gmapUR L (agreeR gnameC).
+
 Definition to_gen_heap {L V} `{Countable L} : gmap L V → gen_heapUR L V :=
   fmap (λ v, (1%Qp, to_agree (v : leibnizC V))).
+Definition to_gen_meta `{Countable L} : gmap L gname → gen_metaUR L :=
+  fmap to_agree.
 
 (** The CMRA we need. *)
 Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_inG :> inG Σ (authR (gen_heapUR L V));
-  gen_heap_name : gname
+  gen_meta_inG :> inG Σ (authR (gen_metaUR L));
+  gen_meta_data_inG :> inG Σ (namespace_mapR (agreeR positiveC));
+  gen_heap_name : gname;
+  gen_meta_name : gname
 }.
 Arguments gen_heap_name {_ _ _ _ _} _ : assert.
+Arguments gen_meta_name {_ _ _ _ _} _ : assert.
 
-Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
-  { gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
+Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V));
+  gen_meta_preG_inG :> inG Σ (authR (gen_metaUR L));
+  gen_meta_data_preG_inG :> inG Σ (namespace_mapR (agreeR positiveC));
+}.
 
-Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
-  #[GFunctor (authR (gen_heapUR L V))].
+Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
+  GFunctor (authR (gen_heapUR L V));
+  GFunctor (authR (gen_metaUR L));
+  GFunctor (namespace_mapR (agreeR positiveC))
+].
 
 Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
   subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
@@ -30,14 +97,32 @@ Proof. solve_inG. Qed.
 Section definitions.
   Context `{Countable L, hG : !gen_heapG L V Σ}.
 
-  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
-    own (gen_heap_name hG) (● (to_gen_heap σ)).
+  Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := (∃ m,
+    (* 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) (● (to_gen_heap σ)) ∗
+    own (gen_meta_name hG) (● (to_gen_meta m)))%I.
 
   Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
     own (gen_heap_name hG) (◯ {[ l := (q, to_agree (v : leibnizC V)) ]}).
   Definition mapsto_aux : seal (@mapsto_def). 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) (◯ {[ l := to_agree γm ]}) ∗
+           own γm (namespace_map_token E))%I.
+  Definition meta_token_aux : seal (@meta_token_def). 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) (◯ {[ l := to_agree γm ]}) ∗
+           own γm (namespace_map_data N (to_agree (encode x))))%I.
+  Definition meta_aux : seal (@meta_def). by eexists. Qed.
+  Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
+  Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
 End definitions.
 
 Local Notation "l ↦{ q } v" := (mapsto l q v)
@@ -51,6 +136,7 @@ Local Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 Section to_gen_heap.
   Context (L V : Type) `{Countable L}.
   Implicit Types σ : gmap L V.
+  Implicit Types m : gmap L gname.
 
   (** Conversion to heaps and back *)
   Lemma to_gen_heap_valid σ : ✓ to_gen_heap σ.
@@ -67,17 +153,25 @@ Section to_gen_heap.
   Lemma to_gen_heap_insert l v σ :
     to_gen_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizC V))]> (to_gen_heap σ).
   Proof. by rewrite /to_gen_heap fmap_insert. Qed.
-  Lemma to_gen_heap_delete l σ :
-    to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
-  Proof. by rewrite /to_gen_heap fmap_delete. Qed.
+
+  Lemma to_gen_meta_valid m : ✓ to_gen_meta m.
+  Proof. intros l. rewrite lookup_fmap. by case (m !! l). Qed.
+  Lemma lookup_to_gen_meta_None m l : m !! l = None → to_gen_meta m !! l = None.
+  Proof. by rewrite /to_gen_meta lookup_fmap=> ->. Qed.
+  Lemma to_gen_meta_insert l m γm :
+    to_gen_meta (<[l:=γm]> m) = <[l:=to_agree γm]> (to_gen_meta m).
+  Proof. by rewrite /to_gen_meta fmap_insert. Qed.
 End to_gen_heap.
 
 Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
   (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
 Proof.
-  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
+  iMod (own_alloc (● to_gen_heap σ)) as (γh) "Hh".
   { rewrite auth_auth_valid. exact: to_gen_heap_valid. }
-  iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
+  iMod (own_alloc (● to_gen_meta ∅)) as (γm) "Hm".
+  { rewrite auth_auth_valid. exact: to_gen_meta_valid. }
+  iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
+  iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
 Qed.
 
 Section gen_heap.
@@ -85,6 +179,7 @@ Section gen_heap.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
+  Implicit Types m : gmap L gname.
   Implicit Types h g : gen_heapUR L V.
   Implicit Types l : L.
   Implicit Types v : V.
@@ -131,44 +226,103 @@ Section gen_heap.
     iApply (mapsto_valid l _ v2). by iFrame.
   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.
+  Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
+  Proof. rewrite meta_eq /meta_def. 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.
+
+  Lemma meta_token_union_1 l E1 E2 :
+    E1 ## E2 → meta_token l (E1 ∪ E2) -∗ meta_token l E1 ∗ meta_token l E2.
+  Proof.
+    rewrite meta_token_eq /meta_token_def. intros ?. iDestruct 1 as (γm1) "[#Hγm Hm]".
+    rewrite namespace_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
+    iSplitL "Hm1"; eauto.
+  Qed.
+  Lemma meta_token_union_2 l E1 E2 :
+    meta_token l E1 -∗ meta_token l E2 -∗ meta_token l (E1 ∪ E2).
+  Proof.
+    rewrite meta_token_eq /meta_token_def.
+    iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
+    iAssert ⌜ γm1 = γm2 ⌝%I as %->.
+    { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
+      move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
+      rewrite singleton_valid. apply: agree_op_invL'. }
+    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.
+  Lemma meta_token_union l E1 E2 :
+    E1 ## E2 → meta_token l (E1 ∪ E2) ⊣⊢ meta_token l E1 ∗ meta_token l E2.
+  Proof.
+    intros; iSplit; first by iApply meta_token_union_1.
+    iIntros "[Hm1 Hm2]". by iApply (meta_token_union_2 with "Hm1 Hm2").
+  Qed.
+
+  Lemma meta_agree `{Countable A} l i (x1 x2 : A) :
+    meta l i x1 -∗ meta l i x2 -∗ ⌜x1 = x2⌝.
+  Proof.
+    rewrite meta_eq /meta_def.
+    iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
+    iAssert ⌜ γm1 = γm2 ⌝%I as %->.
+    { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
+      move: Hγ. rewrite -auth_frag_op op_singleton=> /auth_frag_valid /=.
+      rewrite singleton_valid. apply: agree_op_invL'. }
+    iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
+    move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
+    move=> /agree_op_invL'. naive_solver.
+  Qed.
+  Lemma meta_set `{Countable A} E l (x : A) N :
+    ↑ N ⊆ E → meta_token l E ==∗ meta l N x.
+  Proof.
+    rewrite meta_token_eq meta_eq /meta_token_def /meta_def.
+    iDestruct 1 as (γm) "[Hγm Hm]". iExists γm. iFrame "Hγm".
+    iApply (own_update with "Hm"). by apply namespace_map_alloc_update.
+  Qed.
+
+  (** Update lemmas *)
   Lemma gen_heap_alloc σ l v :
-    σ !! l = None → gen_heap_ctx σ ==∗ gen_heap_ctx (<[l:=v]>σ) ∗ l ↦ v.
+    σ !! l = None →
+    gen_heap_ctx σ ==∗ gen_heap_ctx (<[l:=v]>σ) ∗ l ↦ v ∗ meta_token l ⊤.
   Proof.
-    iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iIntros (Hσl). rewrite /gen_heap_ctx 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 auth_update_alloc,
         (alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
       by apply lookup_to_gen_heap_None. }
-    iModIntro. rewrite to_gen_heap_insert. iFrame.
+    iMod (own_alloc (namespace_map_token ⊤)) as (γm) "Hγm".
+    { apply namespace_map_token_valid. }
+    iMod (own_update with "Hm") as "[Hm Hlm]".
+    { eapply auth_update_alloc.
+      eapply (alloc_singleton_local_update _ l (to_agree γm))=> //.
+      apply lookup_to_gen_meta_None.
+      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).
+    rewrite to_gen_heap_insert to_gen_meta_insert !dom_insert_L. iFrame.
+    iPureIntro. set_solver.
   Qed.
 
   Lemma gen_heap_alloc_gen σ σ' :
-    σ' ##ₘ σ → gen_heap_ctx σ ==∗ gen_heap_ctx (σ' ∪ σ) ∗ [∗ map] l ↦ v ∈ σ', l ↦ v.
-  Proof.
-    revert σ; induction σ' as [| l v σ' Hl IHσ'] using map_ind;
-      iIntros (σ Hσdisj) "Hσ".
-    - by rewrite left_id big_opM_empty; iFrame.
-    - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_l.
-      rewrite big_opM_insert //; iFrame.
-      assert (σ !! l = None).
-      { eapply map_disjoint_Some_r; first by eauto.
-        rewrite lookup_insert //. }
-      rewrite -insert_union_l //.
-      iMod (gen_heap_alloc with "Hσ") as "[$ $]"; last done.
-      apply lookup_union_None; split; auto.
-  Qed.
-
-  Lemma gen_heap_dealloc σ l v :
-    gen_heap_ctx σ -∗ l ↦ v ==∗ gen_heap_ctx (delete l σ).
+    σ' ##ₘ σ →
+    gen_heap_ctx σ ==∗
+    gen_heap_ctx (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤).
   Proof.
-    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
-    rewrite to_gen_heap_delete. iApply (own_update_2 with "Hσ Hl").
-    eapply auth_update_dealloc, (delete_singleton_local_update _ _ _).
+    revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
+    { rewrite left_id_L. auto. }
+    iMod (IH with "Hσ") as "[Hσ'σ Hσ']"; first by eapply map_disjoint_insert_l.
+    decompose_map_disjoint.
+    rewrite !big_opM_insert // -insert_union_l //.
+    by iMod (gen_heap_alloc with "Hσ'σ") as "($ & $ & $)";
+      first by apply lookup_union_None.
   Qed.
 
   Lemma gen_heap_valid σ l q v : gen_heap_ctx σ -∗ l ↦{q} v -∗ ⌜σ !! l = Some v⌝.
   Proof.
-    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
+    rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
       as %[Hl%gen_heap_singleton_included _]%auth_both_valid; auto.
   Qed.
@@ -176,13 +330,16 @@ Section gen_heap.
   Lemma gen_heap_update σ l v1 v2 :
     gen_heap_ctx σ -∗ l ↦ v1 ==∗ gen_heap_ctx (<[l:=v2]>σ) ∗ l ↦ v2.
   Proof.
-    iIntros "Hσ Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
+    iDestruct 1 as (m Hσm) "[Hσ Hm]".
+    iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
     iDestruct (own_valid_2 with "Hσ Hl")
       as %[Hl%gen_heap_singleton_included _]%auth_both_valid.
     iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
     { eapply auth_update, singleton_local_update,
         (exclusive_local_update _ (1%Qp, to_agree (v2:leibnizC _)))=> //.
       by rewrite /to_gen_heap lookup_fmap Hl. }
-    iModIntro. rewrite to_gen_heap_insert. iFrame.
+    iModIntro. iFrame "Hl". iExists m. rewrite to_gen_heap_insert. iFrame.
+    iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
+    rewrite dom_insert_L. set_solver.
   Qed.
 End gen_heap.

theories/heap_lang/lifting.v

@@ -32,7 +32,7 @@ Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
 Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
 Definition array `{!heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
-  ([∗ list] i ↦ v ∈ vs, loc_add l i ↦ v)%I.
+  ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦ v)%I.
 Notation "l ↦∗ vs" := (array l vs)
   (at level 20, format "l  ↦∗  vs") : bi_scope.
 
@@ -218,7 +218,7 @@ Lemma array_singleton l v : l ↦∗ [v] ⊣⊢ l ↦ v.
 Proof. by rewrite /array /= right_id loc_add_0. Qed.
 
 Lemma array_app l vs ws :
-  l ↦∗ (vs ++ ws) ⊣⊢ l ↦∗ vs ∗ (loc_add l (length vs)) ↦∗ ws.
+  l ↦∗ (vs ++ ws) ⊣⊢ l ↦∗ vs ∗ (l +ₗ length vs) ↦∗ ws.
 Proof.
   rewrite /array big_sepL_app.
   setoid_rewrite Nat2Z.inj_add.
@@ -234,70 +234,82 @@ Proof.
 Qed.
 
 Lemma heap_array_to_array l vs :
-  ([∗ map] i ↦ v ∈ heap_array l vs, i ↦ v)%I -∗ l ↦∗ vs.
+  ([∗ map] l' ↦ v ∈ heap_array l vs, l' ↦ v) -∗ l ↦∗ vs.
 Proof.
-  iIntros "Hvs".
-  iInduction vs as [|v vs] "IH" forall (l); simpl.
-  { by rewrite big_opM_empty /array big_opL_nil. }
+  iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (l); simpl.
+  { by rewrite /array. }
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&?&Hjl&_)%heap_array_lookup.
-    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl;
-      apply loc_add_inj in Hjl; lia. }
+    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
   rewrite array_cons.
   rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
   by iApply "IH".
 Qed.
 
+Lemma heap_array_to_seq_meta l vs n :
+  length vs = n →
+  ([∗ map] l' ↦ _ ∈ heap_array l vs, meta_token l' ⊤) -∗
+  [∗ list] i ∈ seq 0 n, meta_token (l +ₗ (i : nat)) ⊤.
+Proof.
+  iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
+  rewrite big_opM_union; last first.
+  { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
+    intros (j&?&Hjl&_)%heap_array_lookup.
+    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
+  rewrite loc_add_0 -fmap_seq big_sepL_fmap.
+  setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
+  setoid_rewrite <-loc_add_assoc.
+  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
+Qed.
+
 (** Heap *)
 Lemma wp_allocN s E v n :
   0 < n →
   {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
-  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }}}.
+  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }}}.
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
+  iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by auto with lia.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
+  iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
   { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
-  iModIntro; iSplit; auto.
-  iFrame. iApply "HΦ".
-  by iApply heap_array_to_array.
+  iModIntro; iSplit; first done. iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
+  - by iApply heap_array_to_array.
+  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 Lemma twp_allocN s E v n :
   0 < n →
   [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
-  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }]].
+  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v ∗
+         [∗ list] i ∈ seq 0 (Z.to_nat n), meta_token (l +ₗ (i : nat)) ⊤ }]].
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
+  iMod (@gen_heap_alloc_gen with "Hσ") as "(Hσ & Hl & Hm)".
   { apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
     rewrite replicate_length Z2Nat.id; auto with lia. }
-  iModIntro; iSplit; auto.
-  iFrame; iSplit; auto. iApply "HΦ".
-  by iApply heap_array_to_array.
+  iModIntro; do 2 (iSplit; first done). iFrame "Hσ Hκs". iApply "HΦ". iSplitL "Hl".
+  - by iApply heap_array_to_array.
+  - iApply (heap_array_to_seq_meta with "Hm"). by rewrite replicate_length.
 Qed.
 
 Lemma wp_alloc s E v :
-  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }}}.
 Proof.
-  iIntros (Φ) "_ HΦ".
-  iApply wp_allocN; auto with lia.
-  iNext; iIntros (l) "H".
-  iApply "HΦ".
-  by rewrite array_singleton.
+  iIntros (Φ) "_ HΦ". iApply wp_allocN; auto with lia.
+  iIntros "!>" (l) "/= (? & ? & _)".
+  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
 Qed.
 Lemma twp_alloc s E v :
-  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
+  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v ∗ meta_token l ⊤ }]].
 Proof.
-  iIntros (Φ) "_ HΦ".
-  iApply twp_allocN; auto with lia.
-  iIntros (l) "H".
-  iApply "HΦ".
-  by rewrite array_singleton.
+  iIntros (Φ) "_ HΦ". iApply twp_allocN; auto with lia.
+  iIntros (l) "/= (? & ? & _)".
+  rewrite array_singleton loc_add_0. iApply "HΦ"; iFrame.
 Qed.
 
 Lemma wp_load s E l q v :

theories/heap_lang/proofmode.v

@@ -189,7 +189,7 @@ Proof.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
 Qed.
 Lemma tac_twp_allocN Δ s E j K v n Φ :
   0 < n →
@@ -203,7 +203,7 @@ Proof.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
   rewrite left_id. apply forall_intro=> l.
   destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦∗ _)%I) right_id wand_elim_r.
 Qed.
 
 Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
@@ -217,7 +217,7 @@ Proof.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r.
 Qed.
 Lemma tac_twp_alloc Δ s E j K v Φ :
   (∀ l, ∃ Δ',
@@ -229,7 +229,7 @@ Proof.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
   rewrite left_id. apply forall_intro=> l.
   destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
-  by rewrite right_id HΔ'.
+  apply wand_intro_l. by rewrite (sep_elim_l (l ↦ v)%I) right_id wand_elim_r.
 Qed.
 
 Lemma tac_wp_load Δ Δ' s E i K l q v Φ :