namespace_map.v 12.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 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.