auth.v 12.7 KB
Newer Older
1
From iris.algebra Require Export excl local_updates.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.base_logic Require Import base_logic proofmode_classes.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4

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

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

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

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

41
Definition auth_ofe_mixin : OfeMixin (auth A).
42
Proof. by apply (iso_ofe_mixin (λ x, (authoritative x, auth_own x))). Qed.
43 44
Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.

45 46 47 48
Global Instance auth_cofe `{Cofe A} : Cofe authC.
Proof.
  apply (iso_cofe (λ y : _ * _, Auth (y.1) (y.2))
    (λ x, (authoritative x, auth_own x))); by repeat intro.
49
Qed.
50

51 52 53
Global Instance Auth_discrete a b :
  Discrete a  Discrete b  Discrete (Auth a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
54
Global Instance auth_ofe_discrete : OfeDiscrete A  OfeDiscrete authC.
55
Proof. intros ? [??]; apply _. Qed.
56
Global Instance auth_leibniz : LeibnizEquiv A  LeibnizEquiv (auth A).
57
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
58 59 60
End cofe.

Arguments authC : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62

(* CMRA *)
63
Section cmra.
64
Context {A : ucmraT}.
65 66
Implicit Types a b : A.
Implicit Types x y : auth A.
67

68 69
Instance auth_valid : Valid (auth A) := λ x,
  match authoritative x with
70 71
  | Excl' a => ( n, auth_own x {n} a)   a
  | None =>  auth_own x
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  | ExclBot' => False
73 74
  end.
Global Arguments auth_valid !_ /.
75
Instance auth_validN : ValidN (auth A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  match authoritative x with
77 78
  | Excl' a => auth_own x {n} a  {n} a
  | None => {n} auth_own x
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  | ExclBot' => False
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  end.
81
Global Arguments auth_validN _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Instance auth_pcore : PCore (auth A) := λ x,
83
  Some (Auth (core (authoritative x)) (core (auth_own x))).
84
Instance auth_op : Op (auth A) := λ x y,
85
  Auth (authoritative x  authoritative y) (auth_own x  auth_own y).
86

87 88 89 90 91 92 93 94 95 96 97 98 99
Definition auth_valid_eq :
  valid = λ x, match authoritative x with
               | Excl' a => ( n, auth_own x {n} a)   a
               | None =>  auth_own x
               | ExclBot' => False
               end := eq_refl _.
Definition auth_validN_eq :
  validN = λ n x, match authoritative x with
                  | Excl' a => auth_own x {n} a  {n} a
                  | None => {n} auth_own x
                  | ExclBot' => False
                  end := eq_refl _.

100
Lemma auth_included (x y : auth A) :
101
  x  y  authoritative x  authoritative y  auth_own x  auth_own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103 104 105
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.
106 107

Lemma authoritative_validN n x : {n} x  {n} authoritative x.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Proof. by destruct x as [[[]|]]. Qed.
109
Lemma auth_own_validN n x : {n} x  {n} auth_own x.
110 111 112 113
Proof.
  rewrite auth_validN_eq.
  destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
Qed.
114

115
Lemma auth_valid_discrete `{CmraDiscrete A} x :
116
   x  match authoritative x with
117 118
        | Excl' a => auth_own x  a   a
        | None =>  auth_own x
119 120 121
        | ExclBot' => False
        end.
Proof.
122
  rewrite auth_valid_eq. destruct x as [[[?|]|] ?]; simpl; try done.
123 124
  setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
Qed.
125 126
Lemma auth_validN_2 n a b : {n} ( a   b)  b {n} a  {n} a.
Proof. by rewrite auth_validN_eq /= left_id. Qed.
127
Lemma auth_valid_discrete_2 `{CmraDiscrete A} a b :  ( a   b)  b  a   a.
128
Proof. by rewrite auth_valid_discrete /= left_id. Qed.
129

130 131
Lemma authoritative_valid  x :  x   authoritative x.
Proof. by destruct x as [[[]|]]. Qed.
132
Lemma auth_own_valid `{CmraDiscrete A} x :  x   auth_own x.
133 134 135 136 137
Proof.
  rewrite auth_valid_discrete.
  destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
Qed.

138
Lemma auth_cmra_mixin : CmraMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141
  apply cmra_total_mixin.
  - eauto.
142 143
  - 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'.
144
  - intros n [x a] [y b] [Hx Ha]; simpl in *. rewrite !auth_validN_eq.
145
    destruct Hx as [?? Hx|]; first destruct Hx; intros ?; ofe_subst; auto.
146 147
  - intros [[[?|]|] ?]; rewrite /= ?auth_valid_eq
      ?auth_validN_eq /= ?cmra_included_includedN ?cmra_valid_validN;
148
      naive_solver eauto using O.
149
  - intros n [[[]|] ?]; rewrite !auth_validN_eq /=;
150
      naive_solver eauto using cmra_includedN_S, cmra_validN_S.
151 152
  - by split; simpl; rewrite assoc.
  - by split; simpl; rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
153 154
  - by split; simpl; rewrite ?cmra_core_l.
  - by split; simpl; rewrite ?cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  - intros ??; rewrite! auth_included; intros [??].
156
    by split; simpl; apply cmra_core_mono.
157
  - assert ( n (a b1 b2 : A), b1  b2 {n} a  b1 {n} a).
158
    { intros n a b1 b2 <-; apply cmra_includedN_l. }
159
   intros n [[[a1|]|] b1] [[[a2|]|] b2]; rewrite auth_validN_eq;
160
     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
161 162
  - intros n x y1 y2 ? [??]; simpl in *.
    destruct (cmra_extend n (authoritative x) (authoritative y1)
163
      (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
164
    destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
165 166
      as (b1&b2&?&?&?); auto using auth_own_validN.
    by exists (Auth ea1 b1), (Auth ea2 b2).
Robbert Krebbers's avatar
Robbert Krebbers committed
167
Qed.
168
Canonical Structure authR := CmraT (auth A) auth_cmra_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
169

170
Global Instance auth_cmra_discrete : CmraDiscrete A  CmraDiscrete authR.
171 172
Proof.
  split; first apply _.
173
  intros [[[?|]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
174 175 176 177
  - setoid_rewrite <-cmra_discrete_included_iff.
    rewrite -cmra_discrete_valid_iff. tauto.
  - by rewrite -cmra_discrete_valid_iff.
Qed.
178

Robbert Krebbers's avatar
Robbert Krebbers committed
179
Instance auth_empty : Unit (auth A) := Auth ε ε.
180
Lemma auth_ucmra_mixin : UcmraMixin (auth A).
181 182
Proof.
  split; simpl.
183
  - rewrite auth_valid_eq /=. apply ucmra_unit_valid.
184
  - by intros x; constructor; rewrite /= left_id.
185
  - do 2 constructor; simpl; apply (core_id_core _).
186
Qed.
187
Canonical Structure authUR := UcmraT (auth A) auth_ucmra_mixin.
188

189 190
Global Instance auth_frag_core_id a : CoreId a  CoreId ( a).
Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
191

192 193
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
194
  x  y  (authoritative x  authoritative y  auth_own x  auth_own y : uPred M).
195
Proof. by uPred.unseal. Qed.
196
Lemma auth_validI {M} (x : auth A) :
197
   x  (match authoritative x with
198 199
          | Excl' a => ( b, a  auth_own x  b)   a
          | None =>  auth_own x
200 201
          | ExclBot' => False
          end : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
202
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
203

204
Lemma auth_frag_op a b :  (a  b) =  a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
Proof. done. Qed.
206 207
Lemma auth_frag_mono a b : a  b   a   b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
208

209 210 211
Global Instance auth_frag_sep_homomorphism :
  MonoidHomomorphism op op () (Auth None).
Proof. by split; [split; try apply _|]. Qed.
212 213 214

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

218 219
Lemma auth_update a b a' b' :
  (a,b) ~l~> (a',b')   a   b ~~>  a'   b'.
220
Proof.
221 222 223 224 225
  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
226
Qed.
227

Robbert Krebbers's avatar
Robbert Krebbers committed
228
Lemma auth_update_alloc a a' b' : (a,ε) ~l~> (a',b')   a ~~>  a'   b'.
229
Proof. intros. rewrite -(right_id _ _ ( a)). by apply auth_update. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε)   a   b ~~>  a'.
231
Proof. intros. rewrite -(right_id _ _ ( a')). by apply auth_update. Qed.
232 233 234 235 236

Lemma auth_local_update (a b0 b1 a' b0' b1': A) :
  (b0, b1) ~l~> (b0', b1')  b0'  a'   a' 
  ( a   b0,  a   b1) ~l~> ( a'   b0',  a'   b1').
Proof.
237 238 239 240 241 242 243
  rewrite !local_update_unital=> Hup ? ? n /=.
  move=> [[[ac|]|] bc] /auth_validN_2 [Le Val] [] /=;
    inversion_clear 1 as [?? Ha|]; inversion_clear Ha. (* need setoid_discriminate! *)
  rewrite !left_id=> ?.
  destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN.
  rewrite -!auth_both_op auth_validN_eq /=.
  split_and!; [by apply cmra_included_includedN|by apply cmra_valid_validN|done].
244
Qed.
245 246
End cmra.

247
Arguments authR : clear implicits.
248
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
249

250
(* Proof mode class instances *)
251 252
Instance is_op_auth_frag {A : ucmraT} (a b1 b2 : A) :
  IsOp a b1 b2  IsOp' ( a) ( b1) ( b2).
253 254
Proof. done. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
255
(* Functor *)
256
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
257
  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
258
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
Proof. by destruct x as [[[]|]]. Qed.
260 261
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
262
Proof. by destruct x as [[[]|]]. Qed.
263
Lemma auth_map_ext {A B : ofeT} (f g : A  B) x :
264
  ( x, f x  g x)  auth_map f x  auth_map g x.
Robbert Krebbers's avatar
Robbert Krebbers committed
265 266
Proof.
  constructor; simpl; auto.
267
  apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
Qed.
269
Instance auth_map_ne {A B : ofeT} n :
270
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
272 273
  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
274
Qed.
275
Instance auth_map_cmra_morphism {A B : ucmraT} (f : A  B) :
276
  CmraMorphism f  CmraMorphism (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
277
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
278
  split; try apply _.
279
  - intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
280
      naive_solver eauto using cmra_morphism_monotoneN, cmra_morphism_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
281 282
  - intros [??]. apply Some_proper; rewrite /auth_map /=.
    by f_equiv; rewrite /= cmra_morphism_core.
283
  - intros [[?|]?] [[?|]?]; try apply Auth_proper=>//=; by rewrite cmra_morphism_op.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
Qed.
285
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
286
  CofeMor (auth_map f).
287 288
Lemma authC_map_ne A B : NonExpansive (@authC_map A B).
Proof. intros n f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
289

290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311
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.

312 313 314
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
315
|}.
316
Next Obligation.
317
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
318
Qed.
Ralf Jung's avatar
Ralf Jung committed
319
Next Obligation.
320
  intros F A B x. rewrite /= -{2}(auth_map_id x).
321
  apply auth_map_ext=>y; apply urFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
322 323
Qed.
Next Obligation.
324
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
325
  apply auth_map_ext=>y; apply urFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
326
Qed.
327

328 329
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
330
Proof.
331
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
332
Qed.