auth.v 6.71 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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
13
Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  authoritative x  authoritative y  own x  own y.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
Instance auth_dist `{Dist A} : Dist (auth A) := λ n x y,
  authoritative x ={n}= authoritative y  own x ={n}= own y.

Instance Auth_ne `{Dist A} : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Proof. by split. Qed.
Instance authoritative_ne `{Dist A} :
  Proper (dist n ==> dist n) (@authoritative A).
Proof. by destruct 1. Qed.
Instance own_ne `{Dist A} : Proper (dist n ==> dist n) (@own A).
Proof. by destruct 1. Qed.

Instance auth_compl `{Cofe A} : Compl (auth A) := λ c,
  Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
Local Instance auth_cofe `{Cofe A} : Cofe (auth A).
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
44
Instance Auth_timeless `{Dist A, Equiv A} (x : excl A) (y : A) :
  Timeless x  Timeless y  Timeless (Auth x y).
Proof. by intros ?? [??] [??]; split; apply (timeless _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
46
47
48
49

(* CMRA *)
Instance auth_empty `{Empty A} : Empty (auth A) := Auth  .
Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
  match authoritative x with
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
  | Excl a => own x  a   a
  | ExclUnit =>  (own x)
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
55
56
  | ExclBot => False
  end.
Arguments auth_valid _ _ _ _ !_ /.
Instance auth_validN `{Dist A, ValidN A, Op A} : ValidN (auth A) := λ n x,
  match authoritative x with
Robbert Krebbers's avatar
Robbert Krebbers committed
57
58
  | Excl a => own x {n} a  {n} a
  | ExclUnit => {n} (own x)
Robbert Krebbers's avatar
Robbert Krebbers committed
59
60
61
  | ExclBot => n = 0
  end.
Arguments auth_validN _ _ _ _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  Auth (unit (authoritative x)) (unit (own x)).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Instance auth_op `{Op A} : Op (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  Auth (authoritative x  authoritative y) (own x  own y).
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
70
71
72
73
  Auth (authoritative x  authoritative y) (own x  own y).
Lemma auth_included `{Equiv A, Op A} (x y : auth A) :
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76
77
78
79
80
Lemma auth_includedN `{Dist A, Op A} n (x y : auth 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.
Lemma authoritative_validN `{CMRA A} n (x : auth A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
81
  {n} x  {n} (authoritative x).
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof. by destruct x as [[]]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Lemma own_validN `{CMRA A} n (x : auth A) : {n} x  {n} (own x).
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed.
Instance auth_cmra `{CMRA A} : CMRA (auth A).
Robbert Krebbers's avatar
Robbert Krebbers committed
86
87
Proof.
  split.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
90
91
92
93
  * apply _.
  * 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 *;
      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
94
      split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
97
98
99
  * by intros [[] ?]; simpl.
  * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
  * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN,
      ?cmra_valid_validN; [naive_solver|naive_solver|].
    split; [done|intros Hn; discriminate (Hn 1)].
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103
  * 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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
  * intros n ??; rewrite! auth_includedN; intros [??].
    by split; simpl; apply cmra_unit_preserving.
  * assert ( n a b1 b2, b1  b2 {n} a  b1 {n} a).
    { 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.
Instance auth_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (auth A).
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.
Instance auth_ra_empty `{CMRA A, Empty A, !RAEmpty A} : RAEmpty (auth A).
Proof.
  split; [apply (ra_empty_valid (A:=A))|].
  by intros x; constructor; simpl; rewrite (left_id _ _).
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
129
130
131
132
133
134
Instance auth_frag_valid_timeless `{CMRA A} (x : A) :
  ValidTimeless x  ValidTimeless ( x).
Proof. by intros ??; apply (valid_timeless x). Qed.
Instance auth_valid_timeless `{CMRA A, Empty A, !RAEmpty A} (x : A) :
  ValidTimeless x  ValidTimeless ( x).
Proof.
  by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
Qed.
135
Lemma auth_frag_op `{CMRA A} a b :  (a  b)   a   b.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
Proof. done. Qed.

(* Functor *)
Definition authRA (A : cmraT) : cmraT := CMRAT (auth A).
Instance auth_fmap : FMap auth := λ A B f x,
  Auth (f <$> authoritative x) (f (own x)).
Instance auth_fmap_cmra_ne `{Dist A, Dist B} n :
  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.
Instance auth_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A  B) :
  ( n, Proper (dist n ==> dist n) f)  CMRAMonotone f 
  CMRAMonotone (fmap f : auth A  auth B).
Proof.
  split.
  * by intros n [x a] [y b]; rewrite !auth_includedN; simpl;
      intros [??]; split; apply includedN_preserving.
  * intros n [[a| |] b];
      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.