auth.v 9.95 KB
Newer Older
1
From algebra Require Export excl.
2
From algebra Require Import functor upred.
3
Local Arguments valid _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Arguments validN _ _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
5

Robbert Krebbers's avatar
Robbert Krebbers committed
6
Record auth (A : Type) : Type := Auth { authoritative : excl A ; 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 {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Arguments own {_} _.
11
12
Notation "◯ a" := (Auth ExclUnit 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
18
Implicit Types a b : A.
Implicit Types x y : auth A.
19
20

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

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

38
Instance auth_compl : Compl (auth A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
40
Definition auth_cofe_mixin : CofeMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
Proof.
  split.
43
  - intros x y; unfold dist, auth_dist, equiv, auth_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
    rewrite !equiv_dist; naive_solver.
45
  - intros n; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
    + by intros ?; split.
    + by intros ?? [??]; split; symmetry.
48
    + intros ??? [??] [??]; split; etrans; eauto.
49
  - by intros ? [??] [??] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
  - intros n c; split. apply (conv_compl n (chain_map authoritative c)).
    apply (conv_compl n (chain_map own c)).
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Qed.
53
Canonical Structure authC := CofeT auth_cofe_mixin.
54
55
Global Instance auth_timeless (x : auth A) :
  Timeless (authoritative x)  Timeless (own x)  Timeless x.
56
Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). 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
65
Section cmra.
Context {A : cmraT}.
66
67
Implicit Types a b : A.
Implicit Types x y : auth A.
68
69

Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth  .
70
71
72
73
74
75
76
Instance auth_valid : Valid (auth A) := λ x,
  match authoritative x with
  | Excl a => own x  a   a
  | ExclUnit =>  own x
  | ExclBot => False
  end.
Global Arguments auth_valid !_ /.
77
Instance auth_validN : ValidN (auth A) := λ n x,
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  match authoritative x with
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  | Excl a => own x {n} a  {n} a
80
  | ExclUnit => {n} own x
81
  | ExclBot => False
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  end.
83
84
Global Arguments auth_validN _ !_ /.
Instance auth_unit : Unit (auth A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  Auth (unit (authoritative x)) (unit (own x)).
86
Instance auth_op : Op (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  Auth (authoritative x  authoritative y) (own x  own y).
88
Instance auth_minus : Minus (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
89
  Auth (authoritative x  authoritative y) (own x  own y).
90
Lemma auth_included (x y : auth A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
93
94
95
  x  y  authoritative x  authoritative y  own x  own y.
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.
96
Lemma auth_includedN n (x y : auth A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
99
100
101
  x {n} y  authoritative x {n} authoritative y  own x {n} own y.
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.
102
Lemma authoritative_validN n (x : auth A) : {n} x  {n} authoritative x.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Proof. by destruct x as [[]]. Qed.
104
Lemma own_validN n (x : auth A) : {n} x  {n} own x.
105
Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
106
107

Definition auth_cmra_mixin : CMRAMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
Proof.
  split.
110
111
112
  - 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'.
  - intros n [x a] [y b] [Hx Ha]; simpl in *;
113
      destruct Hx; intros ?; cofe_subst; auto.
114
  - by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
Robbert Krebbers's avatar
Robbert Krebbers committed
115
      split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
116
117
  - intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
      naive_solver eauto using O.
118
119
120
121
122
123
  - intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
  - by split; simpl; rewrite assoc.
  - by split; simpl; rewrite comm.
  - by split; simpl; rewrite ?cmra_unit_l.
  - by split; simpl; rewrite ?cmra_unit_idemp.
  - intros n ??; rewrite! auth_includedN; intros [??].
124
    by split; simpl; apply cmra_unit_preservingN.
125
  - assert ( n (a b1 b2 : A), b1  b2 {n} a  b1 {n} a).
126
    { intros n a b1 b2 <-; apply cmra_includedN_l. }
Robbert Krebbers's avatar
Robbert Krebbers committed
127
   intros n [[a1| |] b1] [[a2| |] b2];
128
     naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
129
  - by intros n ??; rewrite auth_includedN;
Robbert Krebbers's avatar
Robbert Krebbers committed
130
      intros [??]; split; simpl; apply cmra_op_minus.
131
132
133
134
135
136
  - intros n x y1 y2 ? [??]; simpl in *.
    destruct (cmra_extend n (authoritative x) (authoritative y1)
      (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
    destruct (cmra_extend n (own x) (own y1) (own y2))
      as (b&?&?&?); auto using own_validN.
    by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Qed.
138
Canonical Structure authRA : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
139

140
141
142
143
144
145
146
147
148
149
150
151
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
  (x  y)%I  (authoritative x  authoritative y  own x  own y : uPred M)%I.
Proof. done. Qed.
Lemma auth_validI {M} (x : auth A) :
  ( x)%I  (match authoritative x with
             | Excl a => ( b, a  own x  b)   a
             | ExclUnit =>  own x
             | ExclBot => False
             end : uPred M)%I.
Proof. by destruct x as [[]]. Qed.

152
153
154
155
156
(** The notations ◯ and ● only work for CMRAs with an empty element. So, in
what follows, we assume we have an empty element. *)
Context `{Empty A, !CMRAIdentity A}.

Global Instance auth_cmra_identity : CMRAIdentity authRA.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
Proof.
158
  split; simpl.
159
160
161
  - by apply (@cmra_empty_valid A _).
  - by intros x; constructor; rewrite /= left_id.
  - apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
Qed.
163
Lemma auth_frag_op a b :  (a  b)   a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof. done. Qed.
165
166
Lemma auth_both_op a b : Auth (Excl a) b   a   b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
167
168

Lemma auth_update a a' b b' :
Ralf Jung's avatar
Ralf Jung committed
169
  ( n af, {n} a  a {n} a'  af  b {n} b'  af  {n} b) 
170
   a   a' ~~>  b   b'.
171
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
  move=> Hab n [[?| |] bf1] // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
173
  destruct (Hab n (bf1  bf2)) as [Ha' ?]; auto.
174
175
  { by rewrite Ha left_id assoc. }
  split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
176
Qed.
177

178
Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
179
  Lv a   L a' 
180
   a'   a ~~>  L a'   L a.
181
Proof.
182
  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
183
  by rewrite EQ (local_updateN L) // -EQ.
184
Qed.
185
186
187
188

Lemma auth_update_op_l a a' b :
   (b  a)   a   a' ~~>  (b  a)   (b  a').
Proof. by intros; apply (auth_local_update _). Qed.
189
Lemma auth_update_op_r a a' b :
190
   (a  b)   a   a' ~~>  (a  b)   (a'  b).
191
Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed.
192

Ralf Jung's avatar
Ralf Jung committed
193
(* This does not seem to follow from auth_local_update.
194
   The trouble is that given ✓ (L a ⋅ a'), Lv a
Ralf Jung's avatar
Ralf Jung committed
195
196
   we need ✓ (a ⋅ a'). I think this should hold for every local update,
   but adding an extra axiom to local updates just for this is silly. *)
197
198
199
Lemma auth_local_update_l L `{!LocalUpdate Lv L} a a' :
  Lv a   (L a  a') 
   (a  a')   a ~~>  (L a  a')   L a.
Ralf Jung's avatar
Ralf Jung committed
200
Proof.
201
  intros. apply auth_update=>n af ? EQ; split; last by apply cmra_valid_validN.
202
  by rewrite -(local_updateN L) // EQ -(local_updateN L) // -EQ.
Ralf Jung's avatar
Ralf Jung committed
203
204
Qed.

205
206
207
End cmra.

Arguments authRA : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
208
209

(* Functor *)
210
211
212
213
214
215
216
217
218
219
220
221
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
  Auth (excl_map f (authoritative x)) (f (own x)).
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Proof. by destruct x; rewrite /auth_map excl_map_id. Qed.
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).
Proof. by destruct x; rewrite /auth_map excl_map_compose. Qed.
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.
Proof. constructor; simpl; auto using excl_map_ext. Qed.
Instance auth_map_cmra_ne {A B : cofeT} n :
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
222
Proof.
223
  intros f g Hf [??] [??] [??]; split; [by apply excl_map_cmra_ne|by apply Hf].
Robbert Krebbers's avatar
Robbert Krebbers committed
224
Qed.
225
226
227
Instance auth_map_cmra_monotone {A B : cmraT} (f : A  B) :
  ( n, Proper (dist n ==> dist n) f) 
  CMRAMonotone f  CMRAMonotone (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
Proof.
  split.
230
  - by intros n [x a] [y b]; rewrite !auth_includedN /=;
231
      intros [??]; split; simpl; apply: includedN_preserving.
232
  - intros n [[a| |] b]; rewrite /= /cmra_validN;
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
      naive_solver eauto using @includedN_preserving, @validN_preserving.
Qed.
235
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
236
  CofeMor (auth_map f).
237
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
238
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253

Program Definition authF (Σ : iFunctor) : iFunctor := {|
  ifunctor_car := authRA  Σ; ifunctor_map A B := authC_map  ifunctor_map Σ
|}.
Next Obligation.
  by intros Σ A B n f g Hfg; apply authC_map_ne, ifunctor_map_ne.
Qed.
Next Obligation.
  intros Σ A x. rewrite /= -{2}(auth_map_id x).
  apply auth_map_ext=>y; apply ifunctor_map_id.
Qed.
Next Obligation.
  intros Σ A B C f g x. rewrite /= -auth_map_compose.
  apply auth_map_ext=>y; apply ifunctor_map_compose.
Qed.