auth.v 13.1 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 : Proper (dist n ==> dist n ==> dist n) (@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: Proper (dist n ==> dist n) (@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 : Proper (dist n ==> dist n) (@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).
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
Proof.
  split.
42
  - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
    rewrite !equiv_dist; naive_solver.
44
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
    + by intros ?; split.
    + by intros ?? [??]; split; symmetry.
47
    + intros ??? [??] [??]; split; etrans; eauto.
48
  - by intros ? [??] [??] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
Qed.
50 51 52 53 54 55 56 57 58 59
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.
60 61 62 63 64 65

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.
66
Global Instance auth_leibniz : LeibnizEquiv A  LeibnizEquiv (auth A).
67
Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed.
68 69 70
End cofe.

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

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

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

97 98 99 100 101 102 103 104 105 106 107 108 109
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 _.

110
Lemma auth_included (x y : auth A) :
111
  x  y  authoritative x  authoritative y  auth_own x  auth_own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113 114 115
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.
116 117

Lemma authoritative_validN n x : {n} x  {n} authoritative x.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Proof. by destruct x as [[[]|]]. Qed.
119
Lemma auth_own_validN n x : {n} x  {n} auth_own x.
120 121 122 123
Proof.
  rewrite auth_validN_eq.
  destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
Qed.
124

125 126
Lemma auth_valid_discrete `{CMRADiscrete A} x :
   x  match authoritative x with
127 128
        | Excl' a => auth_own x  a   a
        | None =>  auth_own x
129 130 131
        | ExclBot' => False
        end.
Proof.
132
  rewrite auth_valid_eq. destruct x as [[[?|]|] ?]; simpl; try done.
133 134
  setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
Qed.
135 136
Lemma auth_validN_2 n a b : {n} ( a   b)  b {n} a  {n} a.
Proof. by rewrite auth_validN_eq /= left_id. Qed.
137 138
Lemma auth_valid_discrete_2 `{CMRADiscrete A} a b :  ( a   b)  b  a   a.
Proof. by rewrite auth_valid_discrete /= left_id. Qed.
139

140 141 142 143 144 145 146 147
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.

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

180
Global Instance auth_cmra_discrete : CMRADiscrete A  CMRADiscrete authR.
181 182
Proof.
  split; first apply _.
183
  intros [[[?|]|] ?]; rewrite auth_valid_eq auth_validN_eq /=; auto.
184 185 186 187
  - setoid_rewrite <-cmra_discrete_included_iff.
    rewrite -cmra_discrete_valid_iff. tauto.
  - by rewrite -cmra_discrete_valid_iff.
Qed.
188

189 190 191 192
Instance auth_empty : Empty (auth A) := Auth  .
Lemma auth_ucmra_mixin : UCMRAMixin (auth A).
Proof.
  split; simpl.
193
  - rewrite auth_valid_eq /=. apply ucmra_unit_valid.
194
  - by intros x; constructor; rewrite /= left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
  - do 2 constructor; simpl; apply (persistent_core _).
196 197
Qed.
Canonical Structure authUR :=
198
  UCMRAT (auth A) auth_ofe_mixin auth_cmra_mixin auth_ucmra_mixin.
199

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

203 204
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
205
  x  y  (authoritative x  authoritative y  auth_own x  auth_own y : uPred M).
206
Proof. by uPred.unseal. Qed.
207
Lemma auth_validI {M} (x : auth A) :
208
   x  (match authoritative x with
209 210
          | Excl' a => ( b, a  auth_own x  b)   a
          | None =>  auth_own x
211 212
          | ExclBot' => False
          end : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
214

215
Lemma auth_frag_op a b :  (a  b) =  a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
Proof. done. Qed.
217 218
Lemma auth_frag_mono a b : a  b   a   b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
219
Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
220 221 222 223
Proof. done. Qed.

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

227 228
Lemma auth_update a b a' b' :
  (a,b) ~l~> (a',b')   a   b ~~>  a'   b'.
229
Proof.
230 231 232 233 234
  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
235
Qed.
236

237 238 239 240
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.
241 242 243 244 245

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.
246 247 248 249 250 251 252
  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].
253
Qed.
254 255
End cmra.

256
Arguments authR : clear implicits.
257
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
258

259 260 261 262 263 264 265 266
(* 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
267
(* Functor *)
268
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
269
  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
270
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Proof. by destruct x as [[[]|]]. Qed.
272 273
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
274
Proof. by destruct x as [[[]|]]. Qed.
275
Lemma auth_map_ext {A B : ofeT} (f g : A  B) x :
276
  ( x, f x  g x)  auth_map f x  auth_map g x.
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278
Proof.
  constructor; simpl; auto.
279
  apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
Qed.
281
Instance auth_map_ne {A B : ofeT} n :
282
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
283
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
284 285
  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
286
Qed.
287
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A  B) :
288
  CMRAMonotone f  CMRAMonotone (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
289
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
  split; try apply _.
291
  - intros n [[[a|]|] b]; rewrite !auth_validN_eq; try
292
      naive_solver eauto using cmra_monotoneN, cmra_monotone_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
  - by intros [x a] [y b]; rewrite !auth_included /=;
294
      intros [??]; split; simpl; apply: cmra_monotone.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
Qed.
296
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
297
  CofeMor (auth_map f).
298
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
299
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
300

301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
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.

323 324 325
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
326
|}.
327
Next Obligation.
328
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
329
Qed.
Ralf Jung's avatar
Ralf Jung committed
330
Next Obligation.
331
  intros F A B x. rewrite /= -{2}(auth_map_id x).
332
  apply auth_map_ext=>y; apply urFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
333 334
Qed.
Next Obligation.
335
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
336
  apply auth_map_ext=>y; apply urFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
337
Qed.
338

339 340
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
341
Proof.
342
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
343
Qed.