auth.v 11.7 KB
Newer Older
1
2
From iris.algebra Require Export excl local_updates.
From iris.algebra Require Import upred updates.
3
From iris.proofmode Require Import class_instances.
4
Local Arguments valid _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Local Arguments validN _ _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

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

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

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

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

40
Instance auth_compl : Compl (auth A) := λ c,
41
  Auth (compl (chain_map authoritative c)) (compl (chain_map auth_own c)).
42
Definition auth_cofe_mixin : CofeMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
Proof.
  split.
45
  - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
    rewrite !equiv_dist; naive_solver.
47
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
    + by intros ?; split.
    + by intros ?? [??]; split; symmetry.
50
    + intros ??? [??] [??]; split; etrans; eauto.
51
  - by intros ? [??] [??] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
53
    apply (conv_compl n (chain_map auth_own c)).
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Qed.
55
Canonical Structure authC := CofeT (auth A) auth_cofe_mixin.
56
57
58
59
60
61

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

203
Lemma auth_update a af b :
204
  a ~l~> b @ Some af   (a  af)   a ~~>  (b  af)   b.
205
Proof.
206
  intros [Hab Hab']; apply cmra_total_update.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
  move=> n [[[?|]|] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
208
209
210
  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
211
Qed.
212

213
214
215
216
217
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.
218
219
220
221
222
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.
223
224
End cmra.

225
Arguments authR : clear implicits.
226
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
227

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

270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
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.

292
293
294
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
295
|}.
296
Next Obligation.
297
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
298
Qed.
Ralf Jung's avatar
Ralf Jung committed
299
Next Obligation.
300
  intros F A B x. rewrite /= -{2}(auth_map_id x).
301
  apply auth_map_ext=>y; apply urFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
302
303
Qed.
Next Obligation.
304
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
305
  apply auth_map_ext=>y; apply urFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
306
Qed.
307

308
309
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
310
Proof.
311
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
312
Qed.