auth.v 10.7 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 : option (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}.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Implicit Types a : option (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
Lemma authoritative_validN n (x : auth A) : {n} x  {n} authoritative x.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Proof. by destruct x as [[[]|]]. Qed.
100
Lemma auth_own_validN n (x : auth A) : {n} x  {n} auth_own x.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
102

103
104
Lemma auth_valid_discrete `{CMRADiscrete A} x :
   x  match authoritative x with
105
106
        | Excl' a => auth_own x  a   a
        | None =>  auth_own x
107
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
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
115
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
  apply cmra_total_mixin.
  - eauto.
118
119
  - 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
120
121
122
  - 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;
123
      naive_solver eauto using O.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  - intros n [[[]|] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
125
126
  - by split; simpl; rewrite assoc.
  - by split; simpl; rewrite comm.
Ralf Jung's avatar
Ralf Jung committed
127
128
  - by split; simpl; rewrite ?cmra_core_l.
  - by split; simpl; rewrite ?cmra_core_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  - intros ??; rewrite! auth_included; intros [??].
130
    by split; simpl; apply cmra_core_mono.
131
  - assert ( n (a b1 b2 : A), b1  b2 {n} a  b1 {n} a).
132
    { intros n a b1 b2 <-; apply cmra_includedN_l. }
Robbert Krebbers's avatar
Robbert Krebbers committed
133
   intros n [[[a1|]|] b1] [[[a2|]|] b2];
134
     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
135
136
  - intros n x y1 y2 ? [??]; simpl in *.
    destruct (cmra_extend n (authoritative x) (authoritative y1)
137
      (authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
138
    destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
139
140
      as (b1&b2&?&?&?); auto using auth_own_validN.
    by exists (Auth ea1 b1), (Auth ea2 b2).
Robbert Krebbers's avatar
Robbert Krebbers committed
141
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.

144
Global Instance auth_cmra_discrete : CMRADiscrete A  CMRADiscrete authR.
145
146
Proof.
  split; first apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
  intros [[[?|]|] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
148
149
150
151
  - setoid_rewrite <-cmra_discrete_included_iff.
    rewrite -cmra_discrete_valid_iff. tauto.
  - by rewrite -cmra_discrete_valid_iff.
Qed.
152

153
154
155
156
157
158
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
159
  - do 2 constructor; simpl; apply (persistent_core _).
160
161
162
163
Qed.
Canonical Structure authUR :=
  UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.

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

167
168
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
169
  x  y  (authoritative x  authoritative y  auth_own x  auth_own y : uPred M).
170
Proof. by uPred.unseal. Qed.
171
Lemma auth_validI {M} (x : auth A) :
172
   x  (match authoritative x with
173
174
          | Excl' a => ( b, a  auth_own x  b)   a
          | None =>  auth_own x
175
176
          | ExclBot' => False
          end : uPred M).
Robbert Krebbers's avatar
Robbert Krebbers committed
177
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
178

179
Lemma auth_frag_op a b :  (a  b)   a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
Lemma auth_both_op a b : Auth (Excl' a) b   a   b.
182
Proof. by rewrite /op /auth_op /= left_id. Qed.
183

184
Lemma auth_update a af b :
185
  a ~l~> b @ Some af   (a  af)   a ~~>  (b  af)   b.
186
Proof.
187
  intros [Hab Hab']; apply cmra_total_update.
Robbert Krebbers's avatar
Robbert Krebbers committed
188
  move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
189
190
191
  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
192
Qed.
193

194
195
196
197
198
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.
199
200
201
202
203
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.
204
205
End cmra.

206
Arguments authR : clear implicits.
207
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
209

(* Functor *)
210
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
211
  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
212
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Proof. by destruct x as [[[]|]]. Qed.
214
215
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
216
Proof. by destruct x as [[[]|]]. Qed.
217
218
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
219
220
221
222
223
Proof.
  constructor; simpl; auto.
  apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
Qed.
Instance auth_map_ne {A B : cofeT} n :
224
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
227
  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
228
Qed.
229
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A  B) :
230
  CMRAMonotone f  CMRAMonotone (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
231
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
  split; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
  - intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
234
      naive_solver eauto using cmra_monotoneN, validN_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
  - by intros [x a] [y b]; rewrite !auth_included /=;
236
      intros [??]; split; simpl; apply: cmra_monotone.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
Qed.
238
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
239
  CofeMor (auth_map f).
240
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
241
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
242

243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
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.

265
266
267
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
268
|}.
269
Next Obligation.
270
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
271
Qed.
Ralf Jung's avatar
Ralf Jung committed
272
Next Obligation.
273
  intros F A B x. rewrite /= -{2}(auth_map_id x).
274
  apply auth_map_ext=>y; apply urFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
275
276
Qed.
Next Obligation.
277
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
278
  apply auth_map_ext=>y; apply urFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
279
Qed.
280

281
282
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
283
Proof.
284
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
285
Qed.