From bf293c65ac1ed8b65ded66d22551a120102ad779 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 5 Jun 2019 23:00:11 +0200
Subject: [PATCH] Namespace map RA.

---
 _CoqProject                      |   1 +
 theories/algebra/namespace_map.v | 283 +++++++++++++++++++++++++++++++
 2 files changed, 284 insertions(+)
 create mode 100644 theories/algebra/namespace_map.v

diff --git a/_CoqProject b/_CoqProject
index e88b58a5b..92912c9ec 100644
--- a/_CoqProject
+++ b/_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
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
new file mode 100644
index 000000000..f1acf06ad
--- /dev/null
+++ b/theories/algebra/namespace_map.v
@@ -0,0 +1,283 @@
+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".
+
+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) ∧ ∀ 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) ∧ ∀ 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.
-- 
GitLab