auth.v 12.6 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 classes.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5

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

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

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

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

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

43 44 45 46
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.
47
Qed.
48 49 50 51 52 53

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.
54
Global Instance auth_leibniz : LeibnizEquiv A  LeibnizEquiv (auth A).
55
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
56 57 58
End cofe.

Arguments authC : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60

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

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

85 86 87 88 89 90 91 92 93 94 95 96 97
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 _.

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.
108 109 110 111
Proof.
  rewrite auth_validN_eq.
  destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
Qed.
112

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

128 129 130 131 132 133 134 135
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.

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

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

177 178 179 180
Instance auth_empty : Empty (auth A) := Auth  .
Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
Proof.
  split; simpl.
181
  - rewrite auth_valid_eq /=. apply ucmra_unit_valid.
182
  - by intros x; constructor; rewrite /= left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
183
  - do 2 constructor; simpl; apply (persistent_core _).
184
Qed.
185
Canonical Structure authUR := UCMRAT (auth A) auth_ucmra_mixin.
186

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

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

202
Lemma auth_frag_op a b :  (a  b) =  a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
Proof. done. Qed.
204 205
Lemma auth_frag_mono a b : a  b   a   b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
206
Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
207 208 209 210
Proof. done. Qed.

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

214 215
Lemma auth_update a b a' b' :
  (a,b) ~l~> (a',b')   a   b ~~>  a'   b'.
216
Proof.
217 218 219 220 221
  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
222
Qed.
223

224 225 226 227
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.
228 229 230 231 232

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.
233 234 235 236 237 238 239
  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].
240
Qed.
241 242
End cmra.

243
Arguments authR : clear implicits.
244
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
245

246 247 248 249 250 251 252 253
(* 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
254
(* Functor *)
255
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
256
  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
257
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Proof. by destruct x as [[[]|]]. Qed.
259 260
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
261
Proof. by destruct x as [[[]|]]. Qed.
262
Lemma auth_map_ext {A B : ofeT} (f g : A  B) x :
263
  ( x, f x  g x)  auth_map f x  auth_map g x.
Robbert Krebbers's avatar
Robbert Krebbers committed
264 265
Proof.
  constructor; simpl; auto.
266
  apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
Qed.
268
Instance auth_map_ne {A B : ofeT} n :
269
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
270
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
271 272
  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
273
Qed.
274
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A  B) :
275
  CMRAMonotone f  CMRAMonotone (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
276
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
277
  split; try apply _.
278
  - intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
279
      naive_solver eauto using cmra_monotoneN, cmra_monotone_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
  - by intros [x a] [y b]; rewrite !auth_included /=;
281
      intros [??]; split; simpl; apply: cmra_monotone.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
Qed.
283
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
284
  CofeMor (auth_map f).
285 286
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
287

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

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

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