auth.v 7.84 KB
Newer Older
1
Require Export modures.excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
Local Arguments validN _ _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

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

Robbert Krebbers's avatar
Robbert Krebbers committed
12
(* COFE *)
13
14
Section cofe.
Context {A : cofeT}.
15
16
Implicit Types a b : A.
Implicit Types x y : auth A.
17
18

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

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

36
Instance auth_compl : Compl (auth A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
38
Definition auth_cofe_mixin : CofeMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
41
42
43
44
45
46
Proof.
  split.
  * intros x y; unfold dist, auth_dist, equiv, auth_equiv.
    rewrite !equiv_dist; naive_solver.
  * intros n; split.
    + by intros ?; split.
    + by intros ?? [??]; split; symmetry.
    + intros ??? [??] [??]; split; etransitivity; eauto.
47
  * by intros ? [??] [??] [??]; split; apply dist_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
50
51
  * by split.
  * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
    apply (conv_compl (chain_map own c) n).
Qed.
52
Canonical Structure authC := CofeT auth_cofe_mixin.
53
54
Instance Auth_timeless (ea : excl A) (b : A) :
  Timeless ea  Timeless b  Timeless (Auth ea b).
55
Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
56
57
Global Instance auth_leibniz : LeibnizEquiv A  LeibnizEquiv (auth A).
Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
58
59
60
End cofe.

Arguments authC : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
62

(* CMRA *)
63
64
Section cmra.
Context {A : cmraT}.
65
66
Implicit Types a b : A.
Implicit Types x y : auth A.
67
68
69

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

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

(** 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
140
Proof.
141
142
143
144
  split; simpl.
  * by apply (@cmra_empty_valid A _).
  * by intros x; constructor; rewrite /= left_id.
  * apply Auth_timeless; apply _.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Qed.
146
Lemma auth_frag_op a b :  (a  b)   a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Proof. done. Qed.
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166

Lemma auth_update a a' b b' :
  ( n af, {n} a  a ={n}= a'  af  b ={n}= b'  af  {n} b) 
   a   a'   b   b'.
Proof.
  move=> Hab [[] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
  destruct (Hab (S n) (bf1  bf2)) as [Ha' ?]; auto.
  { by rewrite Ha left_id associative. }
  split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
Qed.
Lemma auth_update_op_l a a' b :
   (b  a)   a   a'   (b  a)   (b  a').
Proof.
  intros; apply auth_update.
  by intros n af ? Ha; split; [by rewrite Ha associative|].
Qed.
Lemma auth_update_op_r a a' b :
   (a  b)   a   a'   (a  b)   (a'  b).
Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
167
168
169
End cmra.

Arguments authRA : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
173

(* Functor *)
Instance auth_fmap : FMap auth := λ A B f x,
  Auth (f <$> authoritative x) (f (own x)).
174
175
176
177
178
179
Arguments auth_fmap _ _ _ !_ /.
Lemma auth_fmap_id {A} (x : auth A) : id <$> x = x.
Proof. by destruct x; rewrite /= excl_fmap_id. Qed.
Lemma excl_fmap_compose {A B C} (f : A  B) (g : B  C) (x : auth A) :
  g  f <$> x = g <$> f <$> x.
Proof. by destruct x; rewrite /= excl_fmap_compose. Qed.
180
Instance auth_fmap_cmra_ne {A B : cmraT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
181
182
183
184
  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
Proof.
  intros f g Hf [??] [??] [??]; split; [by apply excl_fmap_cmra_ne|by apply Hf].
Qed.
185
Instance auth_fmap_cmra_monotone {A B : cmraT} (f : A  B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
189
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone f 
  CMRAMonotone (fmap f : auth A  auth B).
Proof.
  split.
190
191
192
  * by intros n [x a] [y b]; rewrite !auth_includedN /=;
      intros [??]; split; simpl; apply: includedN_preserving.
  * intros n [[a| |] b]; rewrite /= /cmra_validN;
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
196
197
198
      naive_solver eauto using @includedN_preserving, @validN_preserving.
Qed.
Definition authRA_map {A B : cmraT} (f : A -n> B) : authRA A -n> authRA B :=
  CofeMor (fmap f : authRA A  authRA B).
Lemma authRA_map_ne A B n : Proper (dist n ==> dist n) (@authRA_map A B).
Proof. intros f f' Hf [[a| |] b]; repeat constructor; apply Hf. Qed.