auth.v 12.7 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 13
Instance: Params (@Auth) 1.
Instance: Params (@authoritative) 1.
Instance: Params (@auth_own) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15
Notation "◯ a" := (Auth None a) (at level 20).
Notation "● a" := (Auth (Excl' a) ) (at level 20).
Robbert Krebbers's avatar
Robbert Krebbers committed
16

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

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

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

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

46 47 48 49
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.
50
Qed.
51 52 53 54 55 56

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

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

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

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

88 89 90 91 92 93 94 95 96 97 98 99 100
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 _.

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

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

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

131 132 133 134 135 136 137 138
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.

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

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

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

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

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

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

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

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

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

229 230 231 232
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.
233 234 235 236 237

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.
238 239 240 241 242 243 244
  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].
245
Qed.
246 247
End cmra.

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

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

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

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

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

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