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

Robbert Krebbers's avatar
Robbert Krebbers committed
5
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
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 "◯ x" := (Auth ExclUnit x) (at level 20).
Notation "● x" := (Auth (Excl x) ) (at level 20).
Robbert Krebbers's avatar
Robbert Krebbers committed
11

Robbert Krebbers's avatar
Robbert Krebbers committed
12
(* COFE *)
13
14
15
16
Section cofe.
Context {A : cofeT}.

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

21
Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Proof. by split. Qed.
23
Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
Robbert Krebbers's avatar
Robbert Krebbers committed
24
Proof. by destruct 1. Qed.
25
Global Instance own_ne : Proper (dist n ==> dist n) (@own A).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
Proof. by destruct 1. Qed.

28
Instance auth_compl : Compl (auth A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
30
Definition auth_cofe_mixin : CofeMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
35
36
37
38
39
40
41
42
43
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.
  * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
  * by split.
  * intros c n; split. apply (conv_compl (chain_map authoritative c) n).
    apply (conv_compl (chain_map own c) n).
Qed.
44
45
Canonical Structure authC := CofeT auth_cofe_mixin.
Instance Auth_timeless (x : excl A) (y : A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  Timeless x  Timeless y  Timeless (Auth x y).
47
48
49
50
Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
End cofe.

Arguments authC : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52

(* CMRA *)
53
54
55
56
57
Section cmra.
Context {A : cmraT}.

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

Definition auth_cmra_mixin : CMRAMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
  * 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
99
100
101
  * 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
102
      split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
  * by intros [[] ?]; simpl.
  * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
      ?cmra_valid_validN; [naive_solver|naive_solver|].
    split; [done|intros Hn; discriminate (Hn 1)].
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
110
111
  * by split; simpl; rewrite (associative _).
  * by split; simpl; rewrite (commutative _).
  * by split; simpl; rewrite ?(ra_unit_l _).
  * by split; simpl; rewrite ?(ra_unit_idempotent _).
Robbert Krebbers's avatar
Robbert Krebbers committed
112
113
  * intros n ??; rewrite! auth_includedN; intros [??].
    by split; simpl; apply cmra_unit_preserving.
114
  * assert ( n (a b1 b2 : A), b1  b2 {n} a  b1 {n} a).
Robbert Krebbers's avatar
Robbert Krebbers committed
115
116
117
118
119
120
    { intros n a b1 b2 <-; apply cmra_included_l. }
   intros n [[a1| |] b1] [[a2| |] b2];
     naive_solver eauto using cmra_valid_op_l, cmra_valid_includedN.
  * by intros n ??; rewrite auth_includedN;
      intros [??]; split; simpl; apply cmra_op_minus.
Qed.
121
Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
124
125
126
127
128
129
Proof.
  intros n x y1 y2 ? [??]; simpl in *.
  destruct (cmra_extend_op n (authoritative x) (authoritative y1)
    (authoritative y2)) as (z1&?&?&?); auto using authoritative_validN.
  destruct (cmra_extend_op n (own x) (own y1) (own y2))
    as (z2&?&?&?); auto using own_validN.
  by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
Qed.
130
131
132
Canonical Structure authRA : cmraT :=
  CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
Instance auth_ra_empty `{Empty A} : RAIdentity A  RAIdentity (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Proof.
134
  split; simpl; [apply ra_empty_valid|].
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
  by intros x; constructor; simpl; rewrite (left_id _ _).
Qed.
137
Global Instance auth_frag_valid_timeless (x : A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
  ValidTimeless x  ValidTimeless ( x).
Proof. by intros ??; apply (valid_timeless x). Qed.
140
Global Instance auth_valid_timeless `{Empty A, !RAIdentity A} (x : A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
143
144
  ValidTimeless x  ValidTimeless ( x).
Proof.
  by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
Qed.
145
Lemma auth_frag_op (a b : A) :  (a  b)   a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
146
Proof. done. Qed.
147
148
149
150
151
152
153
154
155
Lemma auth_includedN' n (x y : authC A) :
  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.
End cmra.

Arguments authRA : clear implicits.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
159

(* Functor *)
Instance auth_fmap : FMap auth := λ A B f x,
  Auth (f <$> authoritative x) (f (own x)).
160
Instance auth_fmap_cmra_ne {A B : cmraT} n :
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
163
164
  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.
165
Instance auth_fmap_cmra_monotone {A B : cmraT} (f : A  B) :
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
168
169
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone f 
  CMRAMonotone (fmap f : auth A  auth B).
Proof.
  split.
170
171
172
  * 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
173
174
175
176
177
178
      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.