sts.v 9.84 KB
Newer Older
1
Require Export iris.ra.
2
Require Import prelude.sets prelude.bsets iris.dra.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
6
7
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.

Module sts.
8
9
10
Inductive t {A B} (R : relation A) (tok : A  bset B) :=
  | auth : A  bset B  t R tok
  | frag : set A  bset B  t R tok.
11
12
Arguments auth {_ _ _ _} _ _.
Arguments frag {_ _ _ _} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14

Section sts_core.
15
Context {A B : Type} `{ x y : B, Decision (x = y)}.
16
Context (R : relation A) (tok : A  bset B).
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18

Inductive sts_equiv : Equiv (t R tok) :=
19
20
  | auth_equiv s T1 T2 : T1  T2  auth s T1  auth s T2
  | frag_equiv S1 S2 T1 T2 : T1  T2  S1  S2  frag S1 T1  frag S2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Global Existing Instance sts_equiv.
22
Inductive step : relation (A * bset B) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  | Step s1 s2 T1 T2 :
24
     R s1 s2  tok s1  T1    tok s2  T2    tok s1  T1  tok s2  T2 
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
     step (s1,T1) (s2,T2).
Hint Resolve Step.
27
Inductive frame_step (T : bset B) (s1 s2 : A) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  | Frame_step T1 T2 :
29
     T1  (tok s1  T)    step (s1,T1) (s2,T2)  frame_step T s1 s2.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Hint Resolve Frame_step.
31
Record closed (T : bset B) (S : set A) : Prop := Closed {
32
  closed_disjoint s : s  S  tok s  T  ;
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
38
  closed_step s1 s2 : s1  S  frame_step T s1 s2  s2  S
}.
Lemma closed_steps S T s1 s2 :
  closed T S  s1  S  rtc (frame_step T) s1 s2  s2  S.
Proof. induction 3; eauto using closed_step. Qed.
Global Instance sts_valid : Valid (t R tok) := λ x,
39
  match x with auth s T => tok s  T   | frag S' T => closed T S' end.
40
41
Definition up (T : bset B) (s : A) : set A := mkSet (rtc (frame_step T) s).
Definition up_set (T : bset B) (S : set A) : set A := S = up T.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
44
45
46
Global Instance sts_unit : Unit (t R tok) := λ x,
  match x with
  | frag S' _ => frag (up_set  S')  | auth s _ => frag (up  s) 
  end.
Inductive sts_disjoint : Disjoint (t R tok) :=
47
48
49
  | frag_frag_disjoint S1 S2 T1 T2 : T1  T2    frag S1 T1  frag S2 T2
  | auth_frag_disjoint s S T1 T2 : s  S  T1  T2    auth s T1  frag S T2
  | frag_auth_disjoint s S T1 T2 : s  S  T1  T2    frag S T1  auth s T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
Global Existing Instance sts_disjoint.
Global Instance sts_op : Op (t R tok) := λ x1 x2,
  match x1, x2 with
  | frag S1 T1, frag S2 T2 => frag (S1  S2) (T1  T2)
  | auth s T1, frag _ T2 => auth s (T1  T2)
  | frag _ T1, auth s T2 => auth s (T1  T2)
  | auth s T1, auth _ T2 => auth s (T1  T2) (* never happens *)
  end.
Inductive sts_included : Included (t R tok) :=
  | frag_frag_included S1 S2 T1 T2 S' :
     T1  T2  S2  S1  S'  closed (T2  T1) S'  frag S1 T1  frag S2 T2
  | frag_auth_included s S T1 T2 : s  S  T1  T2  frag S T1  auth s T2
  | auth_auth_included s T1 T2 : T1  T2  auth s T1  auth s T2.
Global Existing Instance sts_included.
Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
  match x1, x2 with
  | frag S1 T1, frag S2 T2 => frag (up_set (T1  T2) S1) (T1  T2)
  | auth s T1, frag _ T2 => auth s (T1  T2)
  | frag _ T2, auth s T1 => auth s (T1  T2) (* never happens *)
  | auth s T1, auth _ T2 => frag (up (T1  T2) s) (T1  T2)
  end.

72
Hint Extern 5 (equiv (A:=set _) _ _) => esolve_elem_of : sts.
73
Hint Extern 5 (equiv (A:=bset _) _ _) => esolve_elem_of : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76
77
78
79
80
81
82
Hint Extern 5 (_  _) => esolve_elem_of : sts.
Hint Extern 5 (_  _) => esolve_elem_of : sts.
Instance: Equivalence (() : relation (t R tok)).
Proof.
  split.
  * by intros []; constructor.
  * by destruct 1; constructor.
  * destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
Qed.
83
84
85
Instance framestep_proper : Proper (() ==> (=) ==> (=) ==> impl) frame_step.
Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor; eauto with sts. Qed.
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof.
87
88
  intros ?? HT ?? HS; destruct 1;
    constructor; intros until 0; rewrite <-?HS, <-?HT; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
90
91
Instance closed_proper : Proper (() ==> () ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Lemma closed_op T1 T2 S1 S2 :
93
  closed T1 S1  closed T2 S2  T1  T2    closed (T1  T2) (S1  S2).
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
97
98
99
100
101
102
Proof.
  intros [? Hstep1] [? Hstep2] ?; split; [esolve_elem_of|].
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T ??]; split.
  * apply Hstep1 with s3; eauto with sts.
  * apply Hstep2 with s3; eauto with sts.
Qed.
Lemma closed_all : closed  set_all.
Proof. split; auto with sts. Qed.
Hint Resolve closed_all : sts.
103
Instance up_preserving : Proper (flip () ==> (=) ==> ()) up.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
108
Proof.
  intros T T' HT s ? <-; apply elem_of_subseteq.
  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
  eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
109
110
111
112
Instance up_proper : Proper (() ==> (=) ==> ()) up.
Proof. by intros ?? [??] ???; split; apply up_preserving. Qed.
Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Proof. by intros T1 T2 HT S1 S2 HS; unfold up_set; rewrite HS, HT. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
114
115
116
Lemma elem_of_up s T : s  up T s.
Proof. constructor. Qed.
Lemma subseteq_up_set S T : S  up_set T S.
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
117
Lemma closed_up_set S T : ( s, s  S  tok s  T  )  closed T (up_set T S).
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
120
121
122
123
124
125
126
127
128
Proof.
  intros HS; unfold up_set; split.
  * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
    specialize (HS s' Hs'); clear Hs' S.
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; auto.
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
  * intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
    split; [eapply rtc_r|]; eauto.
Qed.
Lemma closed_up_set_empty S : closed  (up_set  S).
Proof. eauto using closed_up_set with sts. Qed.
129
Lemma closed_up s T : tok s  T    closed T (up T s).
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Proof.
131
  intros; rewrite <-(collection_bind_singleton (up T) s).
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
  apply closed_up_set; auto with sts.
Qed.
Lemma closed_up_empty s : closed  (up  s).
Proof. eauto using closed_up with sts. Qed.
Lemma up_closed S T : closed T S  up_set T S  S.
Proof.
  intros; split; auto using subseteq_up_set; intros s.
  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
Lemma up_set_subseteq T1 T2 S1 S2 :
  closed (T2  T1) S2  up_set (T2  T1) (S1  S2)  S2.
Proof.
  intros ? s2; unfold up_set; rewrite elem_of_bind; intros (s1&?&?).
  apply closed_steps with (T2  T1) s1; auto with sts.
Qed.
Global Instance sts_dra : DRA (t R tok).
Proof.
  split.
  * apply _.
  * by do 2 destruct 1; constructor; setoid_subst.
  * by destruct 1; constructor; setoid_subst.
  * by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
  * by do 2 destruct 1; constructor; setoid_subst.
  * by do 2 destruct 1; inversion_clear 1; econstructor; setoid_subst.
  * assert ( T T' S s,
158
      closed T S  s  S  tok s  T'    tok s  (T  T')  ).
Robbert Krebbers's avatar
Robbert Krebbers committed
159
160
161
162
163
    { intros S T T' s [??]; esolve_elem_of. }
    destruct 3; simpl in *; auto using closed_op with sts.
  * intros []; simpl; eauto using closed_up, closed_up_set with sts.
  * destruct 3; simpl in *; setoid_subst; eauto using closed_up with sts.
    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
164
  * intros [] [] []; constructor; rewrite ?(associative _); auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
  * destruct 4; inversion_clear 1; constructor; auto with sts.
  * destruct 4; inversion_clear 1; constructor; auto with sts.
  * destruct 1; constructor; auto with sts.
  * destruct 3; constructor; auto with sts.
  * intros []; constructor; auto using elem_of_up with sts.
  * intros [|S T]; constructor; auto with sts.
    assert (S  up_set  S); auto using subseteq_up_set with sts.
  * intros [s T|S T]; constructor; auto with sts.
    + by rewrite (up_closed (up _ _)) by auto using closed_up with sts.
    + by rewrite (up_closed (up_set _ _)) by auto using closed_up_set with sts.
  * destruct 3 as [S1 S2| |]; simpl;
      match goal with |- _  frag ?S _ => apply frag_frag_included with S end;
      eauto using closed_up_empty, closed_up_set_empty;
      unfold up_set; esolve_elem_of.
  * destruct 3 as [S1 S2 T1 T2| |]; econstructor; eauto with sts.
180
    by setoid_replace ((T1  T2)  T1) with T2 by esolve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
181
182
  * destruct 3; constructor; eauto using elem_of_up with sts.
  * destruct 3 as [S1 S2 T1 T2 S'| |]; constructor;
183
      rewrite ?(commutative _ (_  _)), <-?union_difference; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
185
186
187
188
    assert (S2  up_set (T2  T1) S2) by eauto using subseteq_up_set.
    assert (up_set (T2  T1) (S1  S')  S') by eauto using up_set_subseteq.
    esolve_elem_of.
Qed.
Lemma step_closed s1 s2 T1 T2 S Tf :
189
190
  step (s1,T1) (s2,T2)  closed Tf S  s1  S  T1  Tf   
  s2  S  T2  Tf    tok s2  T2  .
Robbert Krebbers's avatar
Robbert Krebbers committed
191
192
193
194
195
196
197
198
199
Proof.
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep] ??; split_ands; auto.
  * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
  * clear Hstep Hs1 Hs2; esolve_elem_of.
Qed.
End sts_core.
End sts.

Section sts_ra.
200
Context {A B : Type} `{ x y : B, Decision (x = y)}.
201
Context (R : relation A) (tok : A  bset B).
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
204
205
206
207
208

Definition sts := validity (valid : sts.t R tok  Prop).
Global Instance sts_unit : Unit sts := validity_unit _.
Global Instance sts_op : Op sts := validity_op _.
Global Instance sts_included : Included sts := validity_included _.
Global Instance sts_minus : Minus sts := validity_minus _.
Global Instance sts_ra : RA sts := validity_ra _.
209
210
Definition sts_auth (s : A) (T : bset B) : sts := to_validity (sts.auth s T).
Definition sts_frag (S : set A) (T : bset B) : sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
213
214
215
216
  to_validity (sts.frag S T).
Lemma sts_update s1 s2 T1 T2 :
  sts.step R tok (s1,T1) (s2,T2)  sts_auth s1 T1  sts_auth s2 T2.
Proof.
  intros ?; apply dra_update; inversion 3 as [|? S ? Tf|]; subst.
  destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
217
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
Qed.
End sts_ra.