auth.v 11.8 KB
Newer Older
1
From iris.algebra Require Export excl local_updates.
2
From iris.base_logic Require Import base_logic.
3
From iris.proofmode Require Import class_instances.
4
Local Arguments valid _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Local Arguments validN _ _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
8
Add Printing Constructor auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
Arguments Auth {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Arguments authoritative {_} _.
11
Arguments auth_own {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
Notation "◯ a" := (Auth None a) (at level 20).
Notation "● a" := (Auth (Excl' a) ) (at level 20).
Robbert Krebbers's avatar
Robbert Krebbers committed
14

Robbert Krebbers's avatar
Robbert Krebbers committed
15
(* COFE *)
16
Section cofe.
17
Context {A : ofeT}.
18
Implicit Types a : excl' A.
19
Implicit Types b : A.
20
Implicit Types x y : auth A.
21 22

Instance auth_equiv : Equiv (auth A) := λ x y,
23
  authoritative x  authoritative y  auth_own x  auth_own y.
24
Instance auth_dist : Dist (auth A) := λ n x y,
25
  authoritative x {n} authoritative y  auth_own x {n} auth_own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
26

27
Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Proof. by split. Qed.
29 30
Global Instance Auth_proper : Proper (() ==> () ==> ()) (@Auth A).
Proof. by split. Qed.
31
Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Proof. by destruct 1. Qed.
33 34
Global Instance authoritative_proper : Proper (() ==> ()) (@authoritative A).
Proof. by destruct 1. Qed.
35
Global Instance own_ne : Proper (dist n ==> dist n) (@auth_own A).
Robbert Krebbers's avatar
Robbert Krebbers committed
36
Proof. by destruct 1. Qed.
37
Global Instance own_proper : Proper (() ==> ()) (@auth_own A).
38
Proof. by destruct 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
39

40
Definition auth_ofe_mixin : OfeMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42
Proof.
  split.
43
  - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
    rewrite !equiv_dist; naive_solver.
45
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47
    + by intros ?; split.
    + by intros ?? [??]; split; symmetry.
48
    + intros ??? [??] [??]; split; etrans; eauto.
49
  - by intros ? [??] [??] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
Qed.
51 52 53 54 55 56 57 58 59 60
Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.

Definition auth_compl `{Cofe A} : Compl authC := λ c,
  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
Global Program Instance auth_cofe `{Cofe A} : Cofe authC :=
  {| compl := auth_compl |}.
Next Obligation.
  intros ? n c; split. apply (conv_compl n (chain_map authoritative c)).
  apply (conv_compl n (chain_map auth_own c)).
Qed.
61 62 63 64 65 66

Global Instance Auth_timeless a b :
  Timeless a  Timeless b  Timeless (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: timeless. Qed.
Global Instance auth_discrete : Discrete A  Discrete authC.
Proof. intros ? [??]; apply _. Qed.
67
Global Instance auth_leibniz : LeibnizEquiv A  LeibnizEquiv (auth A).
68
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
69 70 71
End cofe.

Arguments authC : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73

(* CMRA *)
74
Section cmra.
75
Context {A : ucmraT}.
76 77
Implicit Types a b : A.
Implicit Types x y : auth A.
78

79 80
Instance auth_valid : Valid (auth A) := λ x,
  match authoritative x with
81 82
  | Excl' a => ( n, auth_own x {n} a)   a
  | None =>  auth_own x
Robbert Krebbers's avatar
Robbert Krebbers committed
83
  | ExclBot' => False
84 85
  end.
Global Arguments auth_valid !_ /.
86
Instance auth_validN : ValidN (auth A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  match authoritative x with
88 89
  | Excl' a => auth_own x {n} a  {n} a
  | None => {n} auth_own x
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  | ExclBot' => False
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  end.
92
Global Arguments auth_validN _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Instance auth_pcore : PCore (auth A) := λ x,
94
  Some (Auth (core (authoritative x)) (core (auth_own x))).
95
Instance auth_op : Op (auth A) := λ x y,
96
  Auth (authoritative x  authoritative y) (auth_own x  auth_own y).
97

98
Lemma auth_included (x y : auth A) :
99
  x  y  authoritative x  authoritative y  auth_own x  auth_own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
100 101 102 103
Proof.
  split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
  intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
104 105

Lemma authoritative_validN n x : {n} x  {n} authoritative x.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Proof. by destruct x as [[[]|]]. Qed.
107
Lemma auth_own_validN n x : {n} x  {n} auth_own x.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
109

110 111
Lemma auth_valid_discrete `{CMRADiscrete A} x :
   x  match authoritative x with
112 113
        | Excl' a => auth_own x  a   a
        | None =>  auth_own x
114 115 116 117 118 119
        | ExclBot' => False
        end.
Proof.
  destruct x as [[[?|]|] ?]; simpl; try done.
  setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
Qed.
120 121
Lemma auth_valid_discrete_2 `{CMRADiscrete A} a b :  ( a   b)  b  a   a.
Proof. by rewrite auth_valid_discrete /= left_id. Qed.
122

123 124 125 126 127 128 129 130
Lemma authoritative_valid  x :  x   authoritative x.
Proof. by destruct x as [[[]|]]. Qed.
Lemma auth_own_valid `{CMRADiscrete A} x :  x   auth_own x.
Proof.
  rewrite auth_valid_discrete.
  destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
Qed.

131
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134
  apply cmra_total_mixin.
  - eauto.
135 136
  - by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
  - by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139
  - intros n [x a] [y b] [Hx Ha]; simpl in *.
    destruct Hx as [?? Hx|]; first destruct Hx; intros ?; cofe_subst; auto.
  - intros [[[?|]|] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
140
      naive_solver eauto using O.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
  - intros n [[[]|] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
142 143
  - by split; simpl; rewrite assoc.
  - by split; simpl; rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
144 145
  - by split; simpl; rewrite ?cmra_core_l.
  - by split; simpl; rewrite ?cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  - intros ??; rewrite! auth_included; intros [??].
147
    by split; simpl; apply cmra_core_mono.
148
  - assert ( n (a b1 b2 : A), b1  b2 {n} a  b1 {n} a).
149
    { intros n a b1 b2 <-; apply cmra_includedN_l. }
Robbert Krebbers's avatar
Robbert Krebbers committed
150
   intros n [[[a1|]|] b1] [[[a2|]|] b2];
151
     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
152 153
  - intros n x y1 y2 ? [??]; simpl in *.
    destruct (cmra_extend n (authoritative x) (authoritative y1)
154
      (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
155
    destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
156 157
      as (b1&b2&?&?&?); auto using auth_own_validN.
    by exists (Auth ea1 b1), (Auth ea2 b2).
Robbert Krebbers's avatar
Robbert Krebbers committed
158
Qed.
159
Canonical Structure authR := CMRAT (auth A) auth_ofe_mixin auth_cmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
160

161
Global Instance auth_cmra_discrete : CMRADiscrete A  CMRADiscrete authR.
162 163
Proof.
  split; first apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
  intros [[[?|]|] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
165 166 167 168
  - setoid_rewrite <-cmra_discrete_included_iff.
    rewrite -cmra_discrete_valid_iff. tauto.
  - by rewrite -cmra_discrete_valid_iff.
Qed.
169

170 171 172 173 174 175
Instance auth_empty : Empty (auth A) := Auth  .
Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
Proof.
  split; simpl.
  - apply (@ucmra_unit_valid A).
  - by intros x; constructor; rewrite /= left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  - do 2 constructor; simpl; apply (persistent_core _).
177 178
Qed.
Canonical Structure authUR :=
179
  UCMRAT (auth A) auth_ofe_mixin auth_cmra_mixin auth_ucmra_mixin.
180

Robbert Krebbers's avatar
Robbert Krebbers committed
181 182 183
Global Instance auth_frag_persistent a : Persistent a  Persistent ( a).
Proof. do 2 constructor; simpl; auto. by apply persistent_core. Qed.

184 185
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
186
  x  y  (authoritative x  authoritative y  auth_own x  auth_own y : uPred M).
187
Proof. by uPred.unseal. Qed.
188
Lemma auth_validI {M} (x : auth A) :
189
   x  (match authoritative x with
190 191
          | Excl' a => ( b, a  auth_own x  b)   a
          | None =>  auth_own x
192 193
          | ExclBot' => False
          end : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
194
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
195

196
Lemma auth_frag_op a b :  (a  b)   a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
Proof. done. Qed.
198 199
Lemma auth_frag_mono a b : a  b   a   b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
200
Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
201 202 203 204
Proof. done. Qed.

Lemma auth_both_op a b : Auth (Excl' a) b   a   b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
205 206
Lemma auth_auth_valid a :  a   ( a).
Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
207

208 209
Lemma auth_update a b a' b' :
  (a,b) ~l~> (a',b')   a   b ~~>  a'   b'.
210
Proof.
211 212 213 214 215
  intros Hup; apply cmra_total_update.
  move=> n [[[?|]|] bf1] // [[bf2 Ha] ?]; do 2 red; simpl in *.
  move: Ha; rewrite !left_id -assoc=> Ha.
  destruct (Hup n (Some (bf1  bf2))); auto.
  split; last done. exists bf2. by rewrite -assoc.
Ralf Jung's avatar
Ralf Jung committed
216
Qed.
217

218 219 220 221
Lemma auth_update_alloc a a' b' : (a,) ~l~> (a',b')   a ~~>  a'   b'.
Proof. intros. rewrite -(right_id _ _ ( a)). by apply auth_update. Qed.
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',)   a   b ~~>  a'.
Proof. intros. rewrite -(right_id _ _ ( a')). by apply auth_update. Qed.
222 223
End cmra.

224
Arguments authR : clear implicits.
225
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
226

227 228 229 230 231 232 233 234
(* Proof mode class instances *)
Instance from_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
  FromOp a b1 b2  FromOp ( a) ( b1) ( b2).
Proof. done. Qed.
Instance into_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
  IntoOp a b1 b2  IntoOp ( a) ( b1) ( b2).
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
235
(* Functor *)
236
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
237
  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
238
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
Proof. by destruct x as [[[]|]]. Qed.
240 241
Lemma auth_map_compose {A B C} (f : A  B) (g : B  C) (x : auth A) :
  auth_map (g  f) x = auth_map g (auth_map f x).
Robbert Krebbers's avatar
Robbert Krebbers committed
242
Proof. by destruct x as [[[]|]]. Qed.
243
Lemma auth_map_ext {A B : ofeT} (f g : A  B) x :
244
  ( x, f x  g x)  auth_map f x  auth_map g x.
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247 248
Proof.
  constructor; simpl; auto.
  apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
Qed.
249
Instance auth_map_ne {A B : ofeT} n :
250
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
251
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
252 253
  intros f g Hf [??] [??] [??]; split; simpl in *; [|by apply Hf].
  apply option_fmap_ne; [|done]=> x y ?; by apply excl_map_ne.
Robbert Krebbers's avatar
Robbert Krebbers committed
254
Qed.
255
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A  B) :
256
  CMRAMonotone f  CMRAMonotone (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  split; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
  - intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
260
      naive_solver eauto using cmra_monotoneN, cmra_monotone_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
261
  - by intros [x a] [y b]; rewrite !auth_included /=;
262
      intros [??]; split; simpl; apply: cmra_monotone.
Robbert Krebbers's avatar
Robbert Krebbers committed
263
Qed.
264
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
265
  CofeMor (auth_map f).
266
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
267
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
268

269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290
Program Definition authRF (F : urFunctor) : rFunctor := {|
  rFunctor_car A B := authR (urFunctor_car F A B);
  rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
|}.
Next Obligation.
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
  intros F A B x. rewrite /= -{2}(auth_map_id x).
  apply auth_map_ext=>y; apply urFunctor_id.
Qed.
Next Obligation.
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
  apply auth_map_ext=>y; apply urFunctor_compose.
Qed.

Instance authRF_contractive F :
  urFunctorContractive F  rFunctorContractive (authRF F).
Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
Qed.

291 292 293
Program Definition authURF (F : urFunctor) : urFunctor := {|
  urFunctor_car A B := authUR (urFunctor_car F A B);
  urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
Ralf Jung's avatar
Ralf Jung committed
294
|}.
295
Next Obligation.
296
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
297
Qed.
Ralf Jung's avatar
Ralf Jung committed
298
Next Obligation.
299
  intros F A B x. rewrite /= -{2}(auth_map_id x).
300
  apply auth_map_ext=>y; apply urFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
301 302
Qed.
Next Obligation.
303
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
304
  apply auth_map_ext=>y; apply urFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
305
Qed.
306

307 308
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
309
Proof.
310
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
311
Qed.