auth.v 9.46 KB
Newer Older
1
From iris.algebra Require Export excl updates.
2
From iris.algebra Require Import upred.
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 [??].
Ralf Jung's avatar
Ralf Jung committed
130
    by split; simpl; apply cmra_core_preserving.
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
137
  - intros n x y1 y2 ? [??]; simpl in *.
    destruct (cmra_extend n (authoritative x) (authoritative y1)
      (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
138
139
    destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
      as (b&?&?&?); auto using auth_own_validN.
140
    by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
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
159
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.
  - apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  - do 2 constructor; simpl; apply (persistent_core _).
161
162
163
164
Qed.
Canonical Structure authUR :=
  UCMRAT (auth A) auth_cofe_mixin auth_cmra_mixin auth_ucmra_mixin.

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

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

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

194
Arguments authR : clear implicits.
195
Arguments authUR : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197

(* Functor *)
198
Definition auth_map {A B} (f : A  B) (x : auth A) : auth B :=
199
  Auth (excl_map f <$> authoritative x) (f (auth_own x)).
200
Lemma auth_map_id {A} (x : auth A) : auth_map id x = x.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
Proof. by destruct x as [[[]|]]. Qed.
202
203
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
204
Proof. by destruct x as [[[]|]]. Qed.
205
206
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
207
208
209
210
211
Proof.
  constructor; simpl; auto.
  apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
Qed.
Instance auth_map_ne {A B : cofeT} n :
212
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
214
215
  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
216
Qed.
217
Instance auth_map_cmra_monotone {A B : ucmraT} (f : A  B) :
218
  CMRAMonotone f  CMRAMonotone (auth_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
219
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  split; try apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
  - intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
224
      naive_solver eauto using includedN_preserving, validN_preserving.
  - by intros [x a] [y b]; rewrite !auth_included /=;
      intros [??]; split; simpl; apply: included_preserving.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Qed.
226
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
227
  CofeMor (auth_map f).
228
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Ralf Jung's avatar
Ralf Jung committed
230

231
232
233
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
234
|}.
235
Next Obligation.
236
  by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
237
Qed.
Ralf Jung's avatar
Ralf Jung committed
238
Next Obligation.
239
  intros F A B x. rewrite /= -{2}(auth_map_id x).
240
  apply auth_map_ext=>y; apply urFunctor_id.
Ralf Jung's avatar
Ralf Jung committed
241
242
Qed.
Next Obligation.
243
  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
244
  apply auth_map_ext=>y; apply urFunctor_compose.
Ralf Jung's avatar
Ralf Jung committed
245
Qed.
246

247
248
Instance authURF_contractive F :
  urFunctorContractive F  urFunctorContractive (authURF F).
249
Proof.
250
  by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
251
Qed.