auth.v 11.4 KB
Newer Older
1 2
From iris.algebra Require Export excl local_updates.
From iris.algebra Require Import upred updates.
3
Local Arguments valid _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Arguments validN _ _ _ !_ /.
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 16
Section cofe.
Context {A : cofeT}.
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
Instance auth_compl : Compl (auth A) := λ c,
40
  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
41
Definition auth_cofe_mixin : CofeMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
Proof.
  split.
44
  - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
    rewrite !equiv_dist; naive_solver.
46
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48
    + by intros ?; split.
    + by intros ?? [??]; split; symmetry.
49
    + intros ??? [??] [??]; split; etrans; eauto.
50
  - by intros ? [??] [??] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
52
    apply (conv_compl n (chain_map auth_own c)).
Robbert Krebbers's avatar
Robbert Krebbers committed
53
Qed.
54
Canonical Structure authC := CofeT (auth A) auth_cofe_mixin.
55 56 57 58 59 60

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

Arguments authC : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67

(* CMRA *)
68
Section cmra.
69
Context {A : ucmraT}.
70 71
Implicit Types a b : A.
Implicit Types x y : auth A.
72

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

92
Lemma auth_included (x y : auth A) :
93
  x  y  authoritative x  authoritative y  auth_own x  auth_own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96 97
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.
98 99

Lemma authoritative_validN n x : {n} x  {n} authoritative x.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Proof. by destruct x as [[[]|]]. Qed.
101
Lemma auth_own_validN n x : {n} x  {n} auth_own x.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
103

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

117 118 119 120 121 122 123 124
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.

125
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128
  apply cmra_total_mixin.
  - eauto.
129 130
  - 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
131 132 133
  - 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;
134
      naive_solver eauto using O.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  - intros n [[[]|] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
136 137
  - by split; simpl; rewrite assoc.
  - by split; simpl; rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
138 139
  - by split; simpl; rewrite ?cmra_core_l.
  - by split; simpl; rewrite ?cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  - intros ??; rewrite! auth_included; intros [??].
141
    by split; simpl; apply cmra_core_mono.
142
  - assert ( n (a b1 b2 : A), b1  b2 {n} a  b1 {n} a).
143
    { intros n a b1 b2 <-; apply cmra_includedN_l. }
Robbert Krebbers's avatar
Robbert Krebbers committed
144
   intros n [[[a1|]|] b1] [[[a2|]|] b2];
145
     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
146 147
  - intros n x y1 y2 ? [??]; simpl in *.
    destruct (cmra_extend n (authoritative x) (authoritative y1)
148
      (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
149
    destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
150 151
      as (b1&b2&?&?&?); auto using auth_own_validN.
    by exists (Auth ea1 b1), (Auth ea2 b2).
Robbert Krebbers's avatar
Robbert Krebbers committed
152
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154
Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.

155
Global Instance auth_cmra_discrete : CMRADiscrete A  CMRADiscrete authR.
156 157
Proof.
  split; first apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
  intros [[[?|]|] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
159 160 161 162
  - setoid_rewrite <-cmra_discrete_included_iff.
    rewrite -cmra_discrete_valid_iff. tauto.
  - by rewrite -cmra_discrete_valid_iff.
Qed.
163

164 165 166 167 168 169
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
170
  - do 2 constructor; simpl; apply (persistent_core _).
171 172 173 174
Qed.
Canonical Structure authUR :=
  UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.

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

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

190
Lemma auth_frag_op a b :  (a  b)   a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Proof. done. Qed.
192 193
Lemma auth_frag_mono a b : a  b   a   b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
194 195 196 197 198
Global Instance auth_frag_cmra_homomorphism : CMRAHomomorphism (Auth None).
Proof. done. Qed.

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

202
Lemma auth_update a af b :
203
  a ~l~> b @ Some af   (a  af)   a ~~>  (b  af)   b.
204
Proof.
205
  intros [Hab Hab']; apply cmra_total_update.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
207 208 209
  move: Ha; rewrite !left_id=> Hm; split; auto.
  exists bf2. rewrite -assoc.
  apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
Ralf Jung's avatar
Ralf Jung committed
210
Qed.
211

212 213 214 215 216
Lemma auth_update_no_frame a b : a ~l~> b @ Some    a   a ~~>  b   b.
Proof.
  intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
  by apply auth_update.
Qed.
217 218 219 220 221
Lemma auth_update_no_frag af b :  ~l~> b @ Some af   af ~~>  (b  af)   b.
Proof.
  intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ ( _)).
  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

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

261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
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.

283 284 285
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
286
|}.
287
Next Obligation.
288
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
289
Qed.
Ralf Jung's avatar
Ralf Jung committed
290
Next Obligation.
291
  intros F A B x. rewrite /= -{2}(auth_map_id x).
292
  apply auth_map_ext=>y; apply urFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
293 294
Qed.
Next Obligation.
295
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
296
  apply auth_map_ext=>y; apply urFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
297
Qed.
298

299 300
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
301
Proof.
302
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
303
Qed.