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

New Camera dyn_reservation_map and generalize namespace_map → reservation_map

See merge request iris/iris!646

CHANGELOG.md

@@ -12,6 +12,16 @@ lemma.
   (`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".
+* 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
+  information.
+* Add `dyn_reservation_map` which further extends `reservation_map` with the
+  ability to dynamically allocate an infinite set of tokens. This is useful to
+  perform synchronized allocation of the same name in two maps/APIs without
+  dedicated support from one of the involved maps/APIs. See
+  [algebra.dyn_reservation_map](iris/algebra/dyn_reservation_map.v) for further
+  information.
 
 **Changes in `base_logic`:**
 

_CoqProject

@@ -45,7 +45,8 @@ iris/algebra/gmultiset.v
 iris/algebra/coPset.v
 iris/algebra/proofmode_classes.v
 iris/algebra/ufrac.v
-iris/algebra/namespace_map.v
+iris/algebra/reservation_map.v
+iris/algebra/dyn_reservation_map.v
 iris/algebra/lib/excl_auth.v
 iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v

iris/algebra/dyn_reservation_map.v

+From iris.algebra Require Export gmap coPset local_updates.
+From iris.algebra Require Import reservation_map updates proofmode_classes.
+From iris.prelude Require Import options.
+
+(** The camera [dyn_reservation_map A] over a camera [A] extends [gmap positive
+A] with a notion of "reservation tokens" for a (potentially infinite) set [E :
+coPset] which represent the right to allocate a map entry at any position [k ∈
+E].  Unlike [reservation_map], [dyn_reservation_map] supports dynamically
+allocating these tokens, including infinite sets of them.  This is useful when
+syncing the keys of this map with another API that dynamically allocates names:
+we can first reserve a fresh infinite set [E] of tokens here, then allocate a
+new name *in [E]* with the other API (assuming it offers the usual "allocate a
+fresh name in an infinite set" API), and then use our tokens to allocate the
+same name here.  In effect, we have performed synchronized allocation of the
+same name across two maps, without the other API having to have dedicated
+support for this.
+
+The key connectives are [dyn_reservation_map_data k a] (the "points-to"
+assertion of this map), which associates data [a : A] with a key [k : positive],
+and [dyn_reservation_map_token E] (the reservation token), which says
+that no data has been associated with the indices in the mask [E]. The important
+properties of this camera are:
+
+- The lemma [dyn_reservation_map_reserve] provides a frame-preserving update to
+  obtain ownership of [dyn_reservation_map_token E] for some fresh infinite [E].
+- The lemma [dyn_reservation_map_alloc] provides a frame preserving update to
+  associate data to a key: [dyn_reservation_map_token E ~~> dyn_reservation_map_data k a]
+  provided [k ∈ E] and [✓ a].
+
+In the future, it could be interesting to generalize this map to arbitrary key
+types instead of hard-coding [positive]. *)
+
+Record dyn_reservation_map (A : Type) := DynReservationMap {
+  dyn_reservation_map_data_proj : gmap positive A;
+  dyn_reservation_map_token_proj : coPset_disj
+}.
+Add Printing Constructor dyn_reservation_map.
+Global Arguments DynReservationMap {_} _ _.
+Global Arguments dyn_reservation_map_data_proj {_} _.
+Global Arguments dyn_reservation_map_token_proj {_} _.
+Global Instance: Params (@DynReservationMap) 1 := {}.
+Global Instance: Params (@dyn_reservation_map_data_proj) 1 := {}.
+Global Instance: Params (@dyn_reservation_map_token_proj) 1 := {}.
+
+Definition dyn_reservation_map_data {A : cmra} (k : positive) (a : A) : dyn_reservation_map A :=
+  DynReservationMap {[ k := a ]} ε.
+Definition dyn_reservation_map_token {A : cmra} (E : coPset) : dyn_reservation_map A :=
+  DynReservationMap ∅ (CoPset E).
+Global Instance: Params (@dyn_reservation_map_data) 2 := {}.
+
+(** We consruct the OFE and CMRA structure via an isomorphism with
+[reservation_map]. *)
+
+Section ofe.
+  Context {A : ofe}.
+  Implicit Types x y : dyn_reservation_map A.
+
+  Local Definition to_reservation_map x : reservation_map A :=
+    ReservationMap (dyn_reservation_map_data_proj x) (dyn_reservation_map_token_proj x).
+  Local Definition from_reservation_map (x : reservation_map A) : dyn_reservation_map A :=
+    DynReservationMap (reservation_map_data_proj x) (reservation_map_token_proj x).
+
+  Local Instance dyn_reservation_map_equiv : Equiv (dyn_reservation_map A) := λ x y,
+    dyn_reservation_map_data_proj x ≡ dyn_reservation_map_data_proj y ∧
+    dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.
+  Local Instance dyn_reservation_map_dist : Dist (dyn_reservation_map A) := λ n x y,
+    dyn_reservation_map_data_proj x ≡{n}≡ dyn_reservation_map_data_proj y ∧
+    dyn_reservation_map_token_proj x = dyn_reservation_map_token_proj y.
+
+  Global Instance DynReservationMap_ne :
+    NonExpansive2 (@DynReservationMap A).
+  Proof. by split. Qed.
+  Global Instance DynReservationMap_proper :
+    Proper ((≡) ==> (=) ==> (≡)) (@DynReservationMap A).
+  Proof. by split. Qed.
+  Global Instance dyn_reservation_map_data_proj_ne :
+    NonExpansive (@dyn_reservation_map_data_proj A).
+  Proof. by destruct 1. Qed.
+  Global Instance dyn_reservation_map_data_proj_proper :
+    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data_proj A).
+  Proof. by destruct 1. Qed.
+
+  Definition dyn_reservation_map_ofe_mixin : OfeMixin (dyn_reservation_map A).
+  Proof.
+    by apply (iso_ofe_mixin to_reservation_map).
+  Qed.
+  Canonical Structure dyn_reservation_mapO :=
+    Ofe (dyn_reservation_map A) dyn_reservation_map_ofe_mixin.
+
+  Global Instance DynReservationMap_discrete a b :
+    Discrete a → Discrete b → Discrete (DynReservationMap a b).
+  Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
+  Global Instance dyn_reservation_map_ofe_discrete :
+    OfeDiscrete A → OfeDiscrete dyn_reservation_mapO.
+  Proof. intros ? [??]; apply _. Qed.
+End ofe.
+
+Global Arguments dyn_reservation_mapO : clear implicits.
+
+Section cmra.
+  Context {A : cmra}.
+  Implicit Types a b : A.
+  Implicit Types x y : dyn_reservation_map A.
+  Implicit Types k : positive.
+
+  Global Instance dyn_reservation_map_data_ne i : NonExpansive (@dyn_reservation_map_data A i).
+  Proof. intros ? ???. rewrite /dyn_reservation_map_data. solve_proper. Qed.
+  Global Instance dyn_reservation_map_data_proper N :
+    Proper ((≡) ==> (≡)) (@dyn_reservation_map_data A N).
+  Proof. solve_proper. Qed.
+  Global Instance dyn_reservation_map_data_discrete N a :
+    Discrete a → Discrete (dyn_reservation_map_data N a).
+  Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
+  Global Instance dyn_reservation_map_token_discrete E : Discrete (@dyn_reservation_map_token A E).
+  Proof. intros. apply DynReservationMap_discrete; apply _. Qed.
+
+  Local Instance dyn_reservation_map_valid_instance : Valid (dyn_reservation_map A) := λ x,
+    match dyn_reservation_map_token_proj x with
+    | CoPset E =>
+      ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
+      (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
+      (∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E)
+    | CoPsetBot => False
+    end.
+  Global Arguments dyn_reservation_map_valid_instance !_ /.
+  Local Instance dyn_reservation_map_validN_instance : ValidN (dyn_reservation_map A) := λ n x,
+    match dyn_reservation_map_token_proj x with
+    | CoPset E =>
+      ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
+      (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
+      (∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E)
+    | CoPsetBot => False
+    end.
+  Global Arguments dyn_reservation_map_validN_instance !_ /.
+  Local Instance dyn_reservation_map_pcore_instance : PCore (dyn_reservation_map A) := λ x,
+    Some (DynReservationMap (core (dyn_reservation_map_data_proj x)) ε).
+  Local Instance dyn_reservation_map_op_instance : Op (dyn_reservation_map A) := λ x y,
+    DynReservationMap (dyn_reservation_map_data_proj x ⋅ dyn_reservation_map_data_proj y)
+                   (dyn_reservation_map_token_proj x ⋅ dyn_reservation_map_token_proj y).
+
+  Definition dyn_reservation_map_valid_eq :
+    valid = λ x, match dyn_reservation_map_token_proj x with
+                 | CoPset E =>
+                   ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
+                   (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
+                   ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
+                 | CoPsetBot => False
+                 end := eq_refl _.
+  Definition dyn_reservation_map_validN_eq :
+    validN = λ n x, match dyn_reservation_map_token_proj x with
+                    | CoPset E =>
+                      ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
+                      (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
+                      ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
+                    | CoPsetBot => False
+                    end := eq_refl _.
+
+  Lemma dyn_reservation_map_included x y :
+    x ≼ y ↔
+      dyn_reservation_map_data_proj x ≼ dyn_reservation_map_data_proj y ∧
+      dyn_reservation_map_token_proj x ≼ dyn_reservation_map_token_proj y.
+  Proof.
+    split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
+    intros [[z1 Hz1] [z2 Hz2]]; exists (DynReservationMap z1 z2); split; auto.
+  Qed.
+
+  Lemma dyn_reservation_map_data_proj_validN n x : ✓{n} x → ✓{n} dyn_reservation_map_data_proj x.
+  Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
+  Lemma dyn_reservation_map_token_proj_validN n x : ✓{n} x → ✓{n} dyn_reservation_map_token_proj x.
+  Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
+
+  Lemma dyn_reservation_map_cmra_mixin : CmraMixin (dyn_reservation_map A).
+  Proof.
+    apply (iso_cmra_mixin_restrict from_reservation_map to_reservation_map); try done.
+    - intros n [m [E|]];
+        rewrite dyn_reservation_map_validN_eq reservation_map_validN_eq /=;
+        naive_solver.
+    - intros n [m1 [E1|]] [m2 [E2|]] [Hm ?]=> // -[?[??]]; split; simplify_eq/=.
+      + by rewrite -Hm.
+      + split; first done. intros i. by rewrite -(dist_None n) -Hm dist_None.
+    - intros [m [E|]]; rewrite dyn_reservation_map_valid_eq dyn_reservation_map_validN_eq /=
+        ?cmra_valid_validN; naive_solver eauto using O.
+    - intros n [m [E|]]; rewrite dyn_reservation_map_validN_eq /=;
+        naive_solver eauto using cmra_validN_S.
+    - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite dyn_reservation_map_validN_eq /=.
+      rewrite {1}/op /cmra_op /=. case_decide; last done.
+      intros [Hm [Hinf Hdisj]]; split; first by eauto using cmra_validN_op_l.
+      split.
+      + rewrite ->difference_union_distr_r_L in Hinf.
+        eapply set_infinite_subseteq, Hinf. set_solver.
+      + intros i. move: (Hdisj i). rewrite lookup_op.
+        case: (m1 !! i); case: (m2 !! i); set_solver.
+  Qed.
+
+  Canonical Structure dyn_reservation_mapR :=
+    Cmra (dyn_reservation_map A) dyn_reservation_map_cmra_mixin.
+
+  Global Instance dyn_reservation_map_cmra_discrete :
+    CmraDiscrete A → CmraDiscrete dyn_reservation_mapR.
+  Proof.
+    split; first apply _.
+    intros [m [E|]]; rewrite dyn_reservation_map_validN_eq dyn_reservation_map_valid_eq //=.
+      by intros [?%cmra_discrete_valid ?].
+  Qed.
+
+  Local Instance dyn_reservation_map_empty_instance : Unit (dyn_reservation_map A) :=
+    DynReservationMap ε ε.
+  Lemma dyn_reservation_map_ucmra_mixin : UcmraMixin (dyn_reservation_map A).
+  Proof.
+    split; simpl.
+    - rewrite dyn_reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. split.
+      + rewrite difference_empty_L. apply top_infinite.
+      + set_solver.
+    - split; simpl; [by rewrite left_id|by rewrite left_id_L].
+    - do 2 constructor; [apply (core_id_core _)|done].
+  Qed.
+  Canonical Structure dyn_reservation_mapUR :=
+    Ucmra (dyn_reservation_map A) dyn_reservation_map_ucmra_mixin.
+
+  Global Instance dyn_reservation_map_data_core_id N a :
+    CoreId a → CoreId (dyn_reservation_map_data N a).
+  Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
+
+  Lemma dyn_reservation_map_data_valid N a :
+    ✓ (dyn_reservation_map_data N a) ↔ ✓ a.
+  Proof.
+    rewrite dyn_reservation_map_valid_eq /= singleton_valid.
+    split; first naive_solver. intros Ha.
+    split; first done. split; last set_solver.
+    rewrite difference_empty_L. apply top_infinite.
+  Qed.
+  Lemma dyn_reservation_map_token_valid E :
+    ✓ (dyn_reservation_map_token E) ↔ set_infinite (⊤ ∖ E).
+  Proof.
+    rewrite dyn_reservation_map_valid_eq /=. split; first naive_solver.
+    intros Hinf. do 2 (split; first done). by left.
+  Qed.
+  Lemma dyn_reservation_map_data_op N a b :
+    dyn_reservation_map_data N (a ⋅ b) = dyn_reservation_map_data N a ⋅ dyn_reservation_map_data N b.
+  Proof.
+      by rewrite {2}/op /dyn_reservation_map_op_instance /dyn_reservation_map_data /= singleton_op left_id_L.
+  Qed.
+  Lemma dyn_reservation_map_data_mono N a b :
+    a ≼ b → dyn_reservation_map_data N a ≼ dyn_reservation_map_data N b.
+  Proof. intros [c ->]. rewrite dyn_reservation_map_data_op. apply cmra_included_l. Qed.
+  Global Instance dyn_reservation_map_data_is_op N a b1 b2 :
+    IsOp a b1 b2 →
+    IsOp' (dyn_reservation_map_data N a) (dyn_reservation_map_data N b1) (dyn_reservation_map_data N b2).
+  Proof. rewrite /IsOp' /IsOp=> ->. by rewrite dyn_reservation_map_data_op. Qed.
+
+  Lemma dyn_reservation_map_token_union E1 E2 :
+    E1 ## E2 →
+    dyn_reservation_map_token (E1 ∪ E2) = dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token E2.
+  Proof.
+    intros. by rewrite /op /dyn_reservation_map_op_instance
+      /dyn_reservation_map_token /= coPset_disj_union // left_id_L.
+  Qed.
+  Lemma dyn_reservation_map_token_difference E1 E2 :
+    E1 ⊆ E2 →
+    dyn_reservation_map_token E2 = dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token (E2 ∖ E1).
+  Proof.
+    intros. rewrite -dyn_reservation_map_token_union; last set_solver.
+    by rewrite -union_difference_L.
+  Qed.
+  Lemma dyn_reservation_map_token_valid_op E1 E2 :
+    ✓ (dyn_reservation_map_token E1 ⋅ dyn_reservation_map_token E2) ↔
+      E1 ## E2 ∧ set_infinite (⊤ ∖ (E1 ∪ E2)).
+  Proof.
+    split.
+    - rewrite dyn_reservation_map_valid_eq /= {1}/op /cmra_op /=. case_decide; last done.
+      naive_solver.
+    - intros [Hdisj Hinf]. rewrite -dyn_reservation_map_token_union //.
+      apply dyn_reservation_map_token_valid. done.
+  Qed.
+
+  Lemma dyn_reservation_map_reserve (Q : dyn_reservation_map A → Prop) :
+    (∀ E, set_infinite E → Q (dyn_reservation_map_token E)) →
+    ε ~~>: Q.
+  Proof.
+    intros HQ. apply cmra_total_updateP=> n [mf [Ef|]];
+      rewrite left_id {1}dyn_reservation_map_validN_eq /=; last done.
+    intros [Hmap [Hinf Hdisj]].
+    (* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf],
+       such that both that set [E1] and the remainder [E2] are infinite. *)
+    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ dom coPset mf))) as
+        (E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf).
+    { rewrite -difference_difference_L.
+        by apply difference_infinite, dom_finite. }
+    exists (dyn_reservation_map_token E1).
+    split; first by apply HQ. clear HQ.
+    rewrite dyn_reservation_map_validN_eq /=.
+    rewrite coPset_disj_union; last set_solver.
+    split; first by rewrite left_id_L. split.
+    - eapply set_infinite_subseteq, HE2inf. set_solver.
+    - intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
+      destruct (mf !! i) as [p|] eqn:Hp; last by left.
+      apply (elem_of_dom_2 (D:=coPset)) in Hp. right. set_solver.
+  Qed.
+  Lemma dyn_reservation_map_reserve' :
+    ε ~~>: (λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E).
+  Proof. eauto using dyn_reservation_map_reserve. Qed.
+
+  Lemma dyn_reservation_map_alloc E k a :
+    k ∈ E → ✓ a → dyn_reservation_map_token E ~~> dyn_reservation_map_data k a.
+  Proof.
+    intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
+    rewrite dyn_reservation_map_validN_eq /= {1}/op /cmra_op /=. case_decide; last done.
+    rewrite left_id_L {1}left_id. intros [Hmf [Hinf Hdisj]]; split; last split.
+    - destruct (Hdisj k) as [Hmfi|]; last set_solver.
+      move: Hmfi. rewrite lookup_op lookup_empty left_id_L=> Hmfi.
+      intros j. rewrite lookup_op.
+      destruct (decide (k = j)) as [<-|].
+      + rewrite Hmfi lookup_singleton right_id_L. by apply cmra_valid_validN.
+      + by rewrite lookup_singleton_ne // left_id_L.
+    - eapply set_infinite_subseteq, Hinf. set_solver.
+    - intros j. destruct (decide (k = 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 dyn_reservation_map_updateP P (Q : dyn_reservation_map A → Prop) k a :
+    a ~~>: P →
+    (∀ a', P a' → Q (dyn_reservation_map_data k a')) →
+    dyn_reservation_map_data k a ~~>: Q.
+  Proof.
+    intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
+    rewrite dyn_reservation_map_validN_eq /= left_id_L. intros [Hmf [Hinf Hdisj]].
+    destruct (Hup n (mf !! k)) as (a'&?&?).
+    { move: (Hmf (k)).
+      by rewrite lookup_op lookup_singleton Some_op_opM. }
+    exists (dyn_reservation_map_data k a'); split; first by eauto.
+    rewrite /= left_id_L. split; last split.
+    - intros j. destruct (decide (k = 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.
+    - done.
+    - intros j. move: (Hdisj j).
+      rewrite !lookup_op !op_None !lookup_singleton_None. naive_solver.
+  Qed.
+  Lemma dyn_reservation_map_update k a b :
+    a ~~> b →
+    dyn_reservation_map_data k a ~~> dyn_reservation_map_data k b.
+  Proof.
+    rewrite !cmra_update_updateP. eauto using dyn_reservation_map_updateP with subst.
+  Qed.
+End cmra.
+
+Global Arguments dyn_reservation_mapR : clear implicits.
+Global Arguments dyn_reservation_mapUR : clear implicits.

iris/algebra/namespace_map.v

-From stdpp Require Import namespaces.
-From iris.algebra Require Export gmap coPset local_updates.
-From iris.algebra Require Import updates proofmode_classes.
-From iris.prelude Require Import options.
-
-(** 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.
-Global Arguments NamespaceMap {_} _ _.
-Global Arguments namespace_map_data_proj {_} _.
-Global Arguments namespace_map_token_proj {_} _.
-Global Instance: Params (@NamespaceMap) 1 := {}.
-Global Instance: Params (@namespace_map_data_proj) 1 := {}.
-Global Instance: Params (@namespace_map_token_proj) 1 := {}.
-
-(** TODO: [positives_flatten] violates the namespace abstraction. *)
-Definition namespace_map_data {A : cmra} (N : namespace) (a : A) : namespace_map A :=
-  NamespaceMap {[ positives_flatten N := a ]} ε.
-Definition namespace_map_token {A : cmra} (E : coPset) : namespace_map A :=
-  NamespaceMap ∅ (CoPset E).
-Global Instance: Params (@namespace_map_data) 2 := {}.
-
-(* Ofe *)
-Section ofe.
-Context {A : ofe}.
-Implicit Types x y : namespace_map A.
-
-Local 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.
-Local 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 NamespaceMap_ne : NonExpansive2 (@NamespaceMap A).
-Proof. by split. Qed.
-Global Instance NamespaceMap_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_mapO :=
-  Ofe (namespace_map A) namespace_map_ofe_mixin.
-
-Global Instance NamespaceMap_discrete a b :
-  Discrete a → Discrete b → Discrete (NamespaceMap a b).
-Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
-Global Instance namespace_map_ofe_discrete :
-  OfeDiscrete A → OfeDiscrete namespace_mapO.
-Proof. intros ? [??]; apply _. Qed.
-End ofe.
-
-Global Arguments namespace_mapO : clear implicits.
-
-(* Camera *)
-Section cmra.
-Context {A : cmra}.
-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.
-
-Local Instance namespace_map_valid_instance : 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 !_ /.
-Local Instance namespace_map_validN_instance : 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 !_ /.
-Local Instance namespace_map_pcore_instance : PCore (namespace_map A) := λ x,
-  Some (NamespaceMap (core (namespace_map_data_proj x)) ε).
-Local Instance namespace_map_op_instance : 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 O.
-  - 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: FIXME(Coq #6294): needs new unification *)
-  - 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 :=
-  Cmra (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 //=.
-  by intros [?%cmra_discrete_valid ?].
-Qed.
-
-Local Instance namespace_map_empty_instance : 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 :=
-  Ucmra (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; first 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_instance /namespace_map_data /= singleton_op 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 namespace_map_data_is_op 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_instance
-    /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.
-
-Global Arguments namespace_mapR : clear implicits.
-Global Arguments namespace_mapUR : clear implicits.

iris/algebra/reservation_map.v

+From iris.algebra Require Export gmap coPset local_updates.
+From iris.algebra Require Import updates proofmode_classes.
+From iris.prelude Require Import options.
+
+(** The camera [reservation_map A] over a camera [A] extends [gmap positive A]
+with a notion of "reservation tokens" for a (potentially infinite) set
+[E : coPset] which represent the right to allocate a map entry at any position
+[k ∈ E].  The key connectives are [reservation_map_data k a] (the "points-to"
+assertion of this map), which associates data [a : A] with a key [k : positive],
+and [reservation_map_token E] (the reservation token), which says
+that no data has been associated with the indices in the mask [E]. The important
+properties of this camera are:
+
+- The lemma [reservation_map_token_union] enables one to split [reservation_map_token]
+  w.r.t. disjoint union. That is, if we have [E1 ## E2], then we get
+  [reservation_map_token (E1 ∪ E2) = reservation_map_token E1 ⋅ reservation_map_token E2].
+- The lemma [reservation_map_alloc] provides a frame preserving update to
+  associate data to a key: [reservation_map_token E ~~> reservation_map_data k a]
+  provided [k ∈ E] and [✓ a].
+
+In the future, it could be interesting to generalize this map to arbitrary key
+types instead of hard-coding [positive]. *)
+
+Record reservation_map (A : Type) := ReservationMap {
+  reservation_map_data_proj : gmap positive A;
+  reservation_map_token_proj : coPset_disj
+}.
+Add Printing Constructor reservation_map.
+Global Arguments ReservationMap {_} _ _.
+Global Arguments reservation_map_data_proj {_} _.
+Global Arguments reservation_map_token_proj {_} _.
+Global Instance: Params (@ReservationMap) 1 := {}.
+Global Instance: Params (@reservation_map_data_proj) 1 := {}.
+Global Instance: Params (@reservation_map_token_proj) 1 := {}.
+
+Definition reservation_map_data {A : cmra} (k : positive) (a : A) : reservation_map A :=
+  ReservationMap {[ k := a ]} ε.
+Definition reservation_map_token {A : cmra} (E : coPset) : reservation_map A :=
+  ReservationMap ∅ (CoPset E).
+Global Instance: Params (@reservation_map_data) 2 := {}.
+
+(* Ofe *)
+Section ofe.
+  Context {A : ofe}.
+  Implicit Types x y : reservation_map A.
+
+  Local Instance reservation_map_equiv : Equiv (reservation_map A) := λ x y,
+    reservation_map_data_proj x ≡ reservation_map_data_proj y ∧
+    reservation_map_token_proj x = reservation_map_token_proj y.
+  Local Instance reservation_map_dist : Dist (reservation_map A) := λ n x y,
+    reservation_map_data_proj x ≡{n}≡ reservation_map_data_proj y ∧
+    reservation_map_token_proj x = reservation_map_token_proj y.
+
+  Global Instance ReservationMap_ne :
+    NonExpansive2 (@ReservationMap A).
+  Proof. by split. Qed.
+  Global Instance ReservationMap_proper :
+    Proper ((≡) ==> (=) ==> (≡)) (@ReservationMap A).
+  Proof. by split. Qed.
+  Global Instance reservation_map_data_proj_ne :
+    NonExpansive (@reservation_map_data_proj A).
+  Proof. by destruct 1. Qed.
+  Global Instance reservation_map_data_proj_proper :
+    Proper ((≡) ==> (≡)) (@reservation_map_data_proj A).
+  Proof. by destruct 1. Qed.
+
+  Definition reservation_map_ofe_mixin : OfeMixin (reservation_map A).
+  Proof.
+    by apply (iso_ofe_mixin
+      (λ x, (reservation_map_data_proj x, reservation_map_token_proj x))).
+  Qed.
+  Canonical Structure reservation_mapO :=
+    Ofe (reservation_map A) reservation_map_ofe_mixin.
+
+  Global Instance ReservationMap_discrete a b :
+    Discrete a → Discrete b → Discrete (ReservationMap a b).
+  Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
+  Global Instance reservation_map_ofe_discrete :
+    OfeDiscrete A → OfeDiscrete reservation_mapO.
+  Proof. intros ? [??]; apply _. Qed.
+End ofe.
+
+Global Arguments reservation_mapO : clear implicits.
+
+(* Camera *)
+Section cmra.
+  Context {A : cmra}.
+  Implicit Types a b : A.
+  Implicit Types x y : reservation_map A.
+  Implicit Types k : positive.
+
+  Global Instance reservation_map_data_ne i : NonExpansive (@reservation_map_data A i).
+  Proof. solve_proper. Qed.
+  Global Instance reservation_map_data_proper N :
+    Proper ((≡) ==> (≡)) (@reservation_map_data A N).
+  Proof. solve_proper. Qed.
+  Global Instance reservation_map_data_discrete N a :
+    Discrete a → Discrete (reservation_map_data N a).
+  Proof. intros. apply ReservationMap_discrete; apply _. Qed.
+  Global Instance reservation_map_token_discrete E : Discrete (@reservation_map_token A E).
+  Proof. intros. apply ReservationMap_discrete; apply _. Qed.
+
+  Local Instance reservation_map_valid_instance : Valid (reservation_map A) := λ x,
+    match reservation_map_token_proj x with
+    | CoPset E =>
+      ✓ (reservation_map_data_proj x) ∧
+      (* dom (reservation_map_data_proj x) ⊥ E *)
+      ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
+    | CoPsetBot => False
+    end.
+  Global Arguments reservation_map_valid_instance !_ /.
+  Local Instance reservation_map_validN_instance : ValidN (reservation_map A) := λ n x,
+    match reservation_map_token_proj x with
+    | CoPset E =>
+      ✓{n} (reservation_map_data_proj x) ∧
+      (* dom (reservation_map_data_proj x) ⊥ E *)
+      ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
+    | CoPsetBot => False
+    end.
+  Global Arguments reservation_map_validN_instance !_ /.
+  Local Instance reservation_map_pcore_instance : PCore (reservation_map A) := λ x,
+    Some (ReservationMap (core (reservation_map_data_proj x)) ε).
+  Local Instance reservation_map_op_instance : Op (reservation_map A) := λ x y,
+    ReservationMap (reservation_map_data_proj x ⋅ reservation_map_data_proj y)
+                   (reservation_map_token_proj x ⋅ reservation_map_token_proj y).
+
+  Definition reservation_map_valid_eq :
+    valid = λ x, match reservation_map_token_proj x with
+                 | CoPset E =>
+                   ✓ (reservation_map_data_proj x) ∧
+                   (* dom (reservation_map_data_proj x) ⊥ E *)
+                   ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
+                 | CoPsetBot => False
+                 end := eq_refl _.
+  Definition reservation_map_validN_eq :
+    validN = λ n x, match reservation_map_token_proj x with
+                    | CoPset E =>
+                      ✓{n} (reservation_map_data_proj x) ∧
+                      (* dom (reservation_map_data_proj x) ⊥ E *)
+                      ∀ i, reservation_map_data_proj x !! i = None ∨ i ∉ E
+                    | CoPsetBot => False
+                    end := eq_refl _.
+
+  Lemma reservation_map_included x y :
+    x ≼ y ↔
+      reservation_map_data_proj x ≼ reservation_map_data_proj y ∧
+      reservation_map_token_proj x ≼ reservation_map_token_proj y.
+  Proof.
+    split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
+    intros [[z1 Hz1] [z2 Hz2]]; exists (ReservationMap z1 z2); split; auto.
+  Qed.
+  
+  Lemma reservation_map_data_proj_validN n x : ✓{n} x → ✓{n} reservation_map_data_proj x.
+  Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
+  Lemma reservation_map_token_proj_validN n x : ✓{n} x → ✓{n} reservation_map_token_proj x.
+  Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
+  
+  Lemma reservation_map_cmra_mixin : CmraMixin (reservation_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 reservation_map_valid_eq reservation_map_validN_eq /=
+        ?cmra_valid_validN; naive_solver eauto using O.
+    - intros n [m [E|]]; rewrite reservation_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! reservation_map_included; intros [??].
+      by split; simpl; apply: cmra_core_mono. (* FIXME: FIXME(Coq #6294): needs new unification *)
+    - intros n [m1 [E1|]] [m2 [E2|]]=> //=; rewrite reservation_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); case: (m2 !! i); set_solver.
+    - intros n x y1 y2 ? [??]; simpl in *.
+      destruct (cmra_extend n (reservation_map_data_proj x)
+          (reservation_map_data_proj y1) (reservation_map_data_proj y2))
+        as (m1&m2&?&?&?); auto using reservation_map_data_proj_validN.
+      destruct (cmra_extend n (reservation_map_token_proj x)
+          (reservation_map_token_proj y1) (reservation_map_token_proj y2))
+        as (E1&E2&?&?&?); auto using reservation_map_token_proj_validN.
+      by exists (ReservationMap m1 E1), (ReservationMap m2 E2).
+  Qed.
+  Canonical Structure reservation_mapR :=
+    Cmra (reservation_map A) reservation_map_cmra_mixin.
+
+  Global Instance reservation_map_cmra_discrete :
+    CmraDiscrete A → CmraDiscrete reservation_mapR.
+  Proof.
+    split; first apply _.
+    intros [m [E|]]; rewrite reservation_map_validN_eq reservation_map_valid_eq //=.
+      by intros [?%cmra_discrete_valid ?].
+  Qed.
+
+  Local Instance reservation_map_empty_instance : Unit (reservation_map A) := ReservationMap ε ε.
+  Lemma reservation_map_ucmra_mixin : UcmraMixin (reservation_map A).
+  Proof.
+    split; simpl.
+    - rewrite reservation_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 reservation_mapUR :=
+    Ucmra (reservation_map A) reservation_map_ucmra_mixin.
+
+  Global Instance reservation_map_data_core_id N a :
+    CoreId a → CoreId (reservation_map_data N a).
+  Proof. do 2 constructor; simpl; auto. apply core_id_core, _. Qed.
+
+  Lemma reservation_map_data_valid N a : ✓ (reservation_map_data N a) ↔ ✓ a.
+  Proof. rewrite reservation_map_valid_eq /= singleton_valid. set_solver. Qed.
+  Lemma reservation_map_token_valid E : ✓ (reservation_map_token E).
+  Proof. rewrite reservation_map_valid_eq /=. split; first done. by left. Qed.
+  Lemma reservation_map_data_op N a b :
+    reservation_map_data N (a ⋅ b) = reservation_map_data N a ⋅ reservation_map_data N b.
+  Proof.
+      by rewrite {2}/op /reservation_map_op_instance /reservation_map_data /= singleton_op left_id_L.
+  Qed.
+  Lemma reservation_map_data_mono N a b :
+    a ≼ b → reservation_map_data N a ≼ reservation_map_data N b.
+  Proof. intros [c ->]. rewrite reservation_map_data_op. apply cmra_included_l. Qed.
+  Global Instance reservation_map_data_is_op N a b1 b2 :
+    IsOp a b1 b2 →
+    IsOp' (reservation_map_data N a) (reservation_map_data N b1) (reservation_map_data N b2).
+  Proof. rewrite /IsOp' /IsOp=> ->. by rewrite reservation_map_data_op. Qed.
+
+  Lemma reservation_map_token_union E1 E2 :
+    E1 ## E2 →
+    reservation_map_token (E1 ∪ E2) = reservation_map_token E1 ⋅ reservation_map_token E2.
+  Proof.
+    intros. by rewrite /op /reservation_map_op_instance
+      /reservation_map_token /= coPset_disj_union // left_id_L.
+  Qed.
+  Lemma reservation_map_token_difference E1 E2 :
+    E1 ⊆ E2 →
+    reservation_map_token E2 = reservation_map_token E1 ⋅ reservation_map_token (E2 ∖ E1).
+  Proof.
+    intros. rewrite -reservation_map_token_union; last set_solver.
+      by rewrite -union_difference_L.
+  Qed.
+  Lemma reservation_map_token_valid_op E1 E2 :
+    ✓ (reservation_map_token E1 ⋅ reservation_map_token E2) ↔ E1 ## E2.
+  Proof.
+    rewrite reservation_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.
+
+  Lemma reservation_map_alloc E k a :
+    k ∈ E → ✓ a → reservation_map_token E ~~> reservation_map_data k a.
+  Proof.
+    intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
+    rewrite reservation_map_validN_eq /= {1}/op /cmra_op /=. case_decide; last done.
+    rewrite left_id_L {1}left_id. intros [Hmf Hdisj]; split.
+    - destruct (Hdisj k) as [Hmfi|]; last set_solver.
+      move: Hmfi. rewrite lookup_op lookup_empty left_id_L=> Hmfi.
+      intros j. rewrite lookup_op.
+      destruct (decide (k = 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 (k = 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 reservation_map_updateP P (Q : reservation_map A → Prop) k a :
+    a ~~>: P →
+    (∀ a', P a' → Q (reservation_map_data k a')) →
+    reservation_map_data k a ~~>: Q.
+  Proof.
+    intros Hup HP. apply cmra_total_updateP=> n [mf [Ef|]] //.
+    rewrite reservation_map_validN_eq /= left_id_L. intros [Hmf Hdisj].
+    destruct (Hup n (mf !! k)) as (a'&?&?).
+    { move: (Hmf (k)).
+      by rewrite lookup_op lookup_singleton Some_op_opM. }
+    exists (reservation_map_data k a'); split; first by eauto.
+    rewrite /= left_id_L. split.
+    - intros j. destruct (decide (k = 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 reservation_map_update k a b :
+    a ~~> b →
+    reservation_map_data k a ~~> reservation_map_data k b.
+  Proof.
+    rewrite !cmra_update_updateP. eauto using reservation_map_updateP with subst.
+  Qed.
+End cmra.
+
+Global Arguments reservation_mapR : clear implicits.
+Global Arguments reservation_mapUR : clear implicits.

iris/base_logic/lib/gen_heap.v

 From stdpp Require Export namespaces.
-From iris.algebra Require Import namespace_map agree frac.
+From iris.algebra Require Import reservation_map agree frac.
 From iris.algebra Require Export dfrac.
 From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
@@ -56,7 +56,7 @@ these can be matched up with the invariant namespaces. *)
   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.
+  [reservation_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_interp]
@@ -68,7 +68,7 @@ these can be matched up with the invariant namespaces. *)
 Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
   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));
+  gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
 }.
 
 Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
@@ -83,7 +83,7 @@ Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
 Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
   ghost_mapΣ L V;
   ghost_mapΣ L gname;
-  GFunctor (namespace_mapR (agreeR positiveO))
+  GFunctor (reservation_mapR (agreeR positiveO))
 ].
 
 Global Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
@@ -107,14 +107,16 @@ Section definitions.
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
 
   Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
-    ∃ γm, l ↪[gen_meta_name hG]□ γm ∗ own γm (namespace_map_token E).
+    ∃ γm, l ↪[gen_meta_name hG]□ γm ∗ own γm (reservation_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).
 
+  (** TODO: The use of [positives_flatten] violates the namespace abstraction
+  (see the proof of [meta_set]. *)
   Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
     ∃ γm, l ↪[gen_meta_name hG]□ γm ∗
-          own γm (namespace_map_data N (to_agree (encode x))).
+          own γm (reservation_map_data (positives_flatten N) (to_agree (encode x))).
   Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
   Definition meta := meta_aux.(unseal).
   Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
@@ -187,7 +189,7 @@ Section gen_heap.
     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]".
+    rewrite reservation_map_token_union //. iDestruct "Hm" as "[Hm1 Hm2]".
     iSplitL "Hm1"; eauto.
   Qed.
   Lemma meta_token_union_2 l E1 E2 :
@@ -196,8 +198,8 @@ Section gen_heap.
     rewrite meta_token_eq /meta_token_def.
     iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
     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".
+    iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
+    iExists γm2. iFrame "Hγm2". rewrite reservation_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.
@@ -220,7 +222,7 @@ Section gen_heap.
     iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
     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: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
     move=> /to_agree_op_inv_L. naive_solver.
   Qed.
   Lemma meta_set `{Countable A} E l (x : A) N :
@@ -228,7 +230,11 @@ Section gen_heap.
   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.
+    iApply (own_update with "Hm").
+    apply reservation_map_alloc; last done.
+    cut (positives_flatten N ∈@{coPset} ↑N); first by set_solver.
+    rewrite nclose_eq. apply elem_coPset_suffixes.
+    exists 1%positive. by rewrite left_id_L.
   Qed.
 
   (** Update lemmas *)
@@ -239,8 +245,8 @@ Section gen_heap.
     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 (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_alloc (reservation_map_token ⊤)) as (γm) "Hγm".
+    { apply reservation_map_token_valid. }
     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.