sts.v 19 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stdpp Require Export set.
2
3
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
7
Local Arguments core _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

Robbert Krebbers's avatar
Robbert Krebbers committed
9
(** * Definition of STSs *)
10
Module sts.
11
Structure stsT := Sts {
Ralf Jung's avatar
Ralf Jung committed
12
13
  state : Type;
  token : Type;
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
  prim_step : relation state;
  tok : state  set token;
Ralf Jung's avatar
Ralf Jung committed
16
}.
17
Arguments Sts {_ _} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
18
19
20
21
Arguments prim_step {_} _ _.
Arguments tok {_} _.
Notation states sts := (set (state sts)).
Notation tokens sts := (set (token sts)).
Ralf Jung's avatar
Ralf Jung committed
22

Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
(** * Theory and definitions *)
Section sts.
Context {sts : stsT}.
Ralf Jung's avatar
Ralf Jung committed
26

Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
(** ** Step relations *)
Inductive step : relation (state sts * tokens sts) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
29
  | Step s1 s2 T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
30
     prim_step s1 s2  tok s1  T1  tok s2  T2 
Ralf Jung's avatar
Ralf Jung committed
31
     tok s1  T1  tok s2  T2  step (s1,T1) (s2,T2).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Notation steps := (rtc step).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
34
  (* Probably equivalent definition: (\mathcal{L}(s') ⊥ T) ∧ s \rightarrow s' *)
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  | Frame_step T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
36
     T1  tok s1  T  step (s1,T1) (s2,T2)  frame_step T s1 s2.
Ralf Jung's avatar
Ralf Jung committed
37
Notation frame_steps T := (rtc (frame_step T)).
Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
40

(** ** Closure under frame steps *)
Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
Robbert Krebbers's avatar
Robbert Krebbers committed
41
  closed_disjoint s : s  S  tok s  T;
Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
  closed_step s1 s2 : s1  S  frame_step T s1 s2  s2  S
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Definition up (s : state sts) (T : tokens sts) : states sts :=
Ralf Jung's avatar
Ralf Jung committed
45
  {[ s' | frame_steps T s s' ]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Definition up_set (S : states sts) (T : tokens sts) : states sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  S = λ s, up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
48

Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
(** Tactic setup *)
Hint Resolve Step.
51
52
53
54
Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (_  _) => set_solver : sts.
Hint Extern 50 (_  _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Hint Extern 50 (_  _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57

(** ** Setoids *)
Ralf Jung's avatar
Ralf Jung committed
58
Instance frame_step_mono : Proper (flip () ==> (=) ==> (=) ==> impl) frame_step.
Ralf Jung's avatar
Ralf Jung committed
59
60
Proof.
  intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
61
    eauto with sts; set_solver.
Ralf Jung's avatar
Ralf Jung committed
62
Qed.
Ralf Jung's avatar
Ralf Jung committed
63
64
Global Instance frame_step_proper : Proper (() ==> (=) ==> (=) ==> iff) frame_step.
Proof. move=> ?? /collection_equiv_spec [??]; split; by apply frame_step_mono. Qed.
65
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Global Instance closed_proper : Proper (() ==> () ==> iff) closed.
68
Proof. by split; apply closed_proper'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Global Instance up_preserving : Proper ((=) ==> flip () ==> ()) up.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
Proof.
71
  intros s ? <- T T' HT ; apply elem_of_subseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
73
  eapply elem_of_mkSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Global Instance up_proper : Proper ((=) ==> () ==> ()) up.
76
77
78
Proof.
  by move=> ??? ?? /collection_equiv_spec [??]; split; apply up_preserving.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Global Instance up_set_preserving : Proper (() ==> flip () ==> ()) up_set.
Ralf Jung's avatar
Ralf Jung committed
80
81
Proof.
  intros S1 S2 HS T1 T2 HT. rewrite /up_set.
82
  f_equiv=> // s1 s2 Hs. by apply up_preserving.
Ralf Jung's avatar
Ralf Jung committed
83
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Global Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
85
86
87
88
Proof.
  move=> S1 S2 /collection_equiv_spec [??] T1 T2 /collection_equiv_spec [??];
    split; by apply up_set_preserving.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
90
91

(** ** Properties of closure under frame steps *)
Lemma closed_steps S T s1 s2 :
Ralf Jung's avatar
Ralf Jung committed
92
  closed S T  s1  S  frame_steps T s1 s2  s2  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
Proof. induction 3; eauto using closed_step. Qed.
Lemma closed_op T1 T2 S1 S2 :
95
  closed S1 T1  closed S2 T2  closed (S1  S2) (T1  T2).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Proof.
97
  intros [? Hstep1] [? Hstep2]; split; [set_solver|].
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
99
100
  - apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
  - apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
Qed.
Lemma step_closed s1 s2 T1 T2 S Tf :
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
  step (s1,T1) (s2,T2)  closed S Tf  s1  S  T1  Tf 
  s2  S  T2  Tf  tok s2  T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
Proof.
106
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.
107
  - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
108
  - set_solver -Hstep Hs1 Hs2.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Qed.
110
Lemma steps_closed s1 s2 T1 T2 S Tf :
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
  steps (s1,T1) (s2,T2)  closed S Tf  s1  S  T1  Tf 
  tok s1  T1  s2  S  T2  Tf  tok s2  T2.
113
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
116
117
118
  remember (s1,T1) as sT1 eqn:HsT1; remember (s2,T2) as sT2 eqn:HsT2.
  intros Hsteps; revert s1 T1 HsT1 s2 T2 HsT2.
  induction Hsteps as [?|? [s2 T2] ? Hstep Hsteps IH];
     intros s1 T1 HsT1 s2' T2' ?????; simplify_eq; first done.
  destruct (step_closed s1 s2 T1 T2 S Tf) as (?&?&?); eauto.
119
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121

(** ** Properties of the closure operators *)
122
Lemma elem_of_up s T : s  up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Proof. constructor. Qed.
124
Lemma subseteq_up_set S T : S  up_set S T.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
126
127
Lemma elem_of_up_set S T s : s  S  s  up_set S T.
Proof. apply subseteq_up_set. Qed.
Ralf Jung's avatar
Ralf Jung committed
128
129
Lemma up_up_set s T : up s T  up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Lemma closed_up_set S T : ( s, s  S  tok s  T)  closed (up_set S T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
Proof.
132
  intros HS; unfold up_set; split.
133
  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
134
    specialize (HS s' Hs'); clear Hs' S.
135
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
137
  - intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; exists s.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
    split; [eapply rtc_r|]; eauto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Lemma closed_up s T : tok s  T  closed (up s T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
Proof.
142
  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
143
  apply closed_up_set; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Qed.
145
146
Lemma closed_up_set_empty S : closed (up_set S ) .
Proof. eauto using closed_up_set with sts. Qed.
147
Lemma closed_up_empty s : closed (up s ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Proof. eauto using closed_up with sts. Qed.
149
Lemma up_closed S T : closed S T  up_set S T  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Proof.
151
152
  intros ?; apply collection_equiv_spec; split; auto using subseteq_up_set.
  intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
  induction Hstep; eauto using closed_step.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
158
Lemma up_subseteq s T S : closed S T  s  S  sts.up s T  S.
Proof. move=> ?? s' ?. eauto using closed_steps. Qed.
Lemma up_set_subseteq S1 T S2 : closed S2 T  S1  S2  sts.up_set S1 T  S2.
Proof. move=> ?? s [s' [? ?]]. eauto using closed_steps. Qed.
Ralf Jung's avatar
Ralf Jung committed
159
160
161
162
163
164
Lemma up_op s T1 T2 : up s (T1  T2)  up s T1  up s T2.
Proof. (* Notice that the other direction does not hold. *)
  intros x Hx. split; eapply elem_of_mkSet, rtc_subrel; try exact Hx.
  - intros; eapply frame_step_mono; last first; try done. set_solver+.
  - intros; eapply frame_step_mono; last first; try done. set_solver+.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
167
End sts.

Notation steps := (rtc step).
Ralf Jung's avatar
Ralf Jung committed
168
Notation frame_steps T := (rtc (frame_step T)).
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
171
172
173
174
175
176

(* The type of bounds we can give to the state of an STS. This is the type
   that we equip with an RA structure. *)
Inductive car (sts : stsT) :=
  | auth : state sts  set (token sts)  car sts
  | frag : set (state sts)  set (token sts )  car sts.
Arguments auth {_} _ _.
Arguments frag {_} _ _.
177
End sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
178

179
Notation stsT := sts.stsT.
180
Notation Sts := sts.Sts.
181
182

(** * STSs form a disjoint RA *)
Robbert Krebbers's avatar
Robbert Krebbers committed
183
Section sts_dra.
184
185
Context (sts : stsT).
Import sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
188
189
190
191
Implicit Types S : states sts.
Implicit Types T : tokens sts.

Inductive sts_equiv : Equiv (car sts) :=
  | 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.
192
193
Existing Instance sts_equiv.
Instance sts_valid : Valid (car sts) := λ x,
194
  match x with
Robbert Krebbers's avatar
Robbert Krebbers committed
195
  | auth s T => tok s  T
196
  | frag S' T => closed S' T   s, s  S'
Robbert Krebbers's avatar
Robbert Krebbers committed
197
  end.
198
Instance sts_core : Core (car sts) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
201
202
203
204
  match x with
  | frag S' _ => frag (up_set S'  ) 
  | auth s _  => frag (up s ) 
  end.
Inductive sts_disjoint : Disjoint (car sts) :=
  | frag_frag_disjoint S1 S2 T1 T2 :
205
     ( s, s  S1  S2)  T1  T2  frag S1 T1  frag S2 T2
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
  | 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.
208
209
Existing Instance sts_disjoint.
Instance sts_op : Op (car sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
212
213
214
215
216
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
217
Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
218
Hint Extern 50 ( s : state sts, _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
219
220
Hint Extern 50 (_  _) => set_solver : sts.
Hint Extern 50 (_  _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
222
Hint Extern 50 (_  _) => set_solver : sts.

223
224
225
226
227
228
Global Instance auth_proper s : Proper (() ==> ()) (@auth sts s).
Proof. by constructor. Qed.
Global Instance frag_proper : Proper (() ==> () ==> ()) (@frag sts).
Proof. by constructor. Qed.

Instance sts_equivalence: Equivalence (() : relation (car sts)).
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
Proof.
  split.
231
232
  - by intros []; constructor.
  - by destruct 1; constructor.
233
  - destruct 1; inversion_clear 1; constructor; etrans; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
234
Qed.
235
Lemma sts_dra_mixin : DraMixin (car sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
Proof.
  split.
238
239
240
241
  - apply _.
  - by do 2 destruct 1; constructor; setoid_subst.
  - by destruct 1; constructor; setoid_subst.
  - by destruct 1; simpl; intros ?; setoid_subst.
242
  - by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.
243
  - destruct 3; simpl in *; destruct_and?; eauto using closed_op;
244
      match goal with H : closed _ _ |- _ => destruct H end; set_solver.
245
246
  - intros []; naive_solver eauto using closed_up, closed_up_set,
      elem_of_up, elem_of_up_set with sts.
247
248
249
250
251
  - intros [] [] []; constructor; rewrite ?assoc; auto with sts.
  - 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.
252
253
  - intros []; constructor; eauto with sts.
  - intros []; constructor; auto with sts.
254
  - intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
255
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
256
    + rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
258
  - intros x y. exists (core (x  y))=> ?? Hxy; split_and?.
    + destruct Hxy; constructor; unfold up_set; set_solver.
259
260
261
    + destruct Hxy; simpl;
        eauto using closed_up_set_empty, closed_up_empty with sts.
    + destruct Hxy; econstructor;
262
        repeat match goal with
263
264
265
266
        | |- context [ up_set ?S ?T ] =>
           unless (S  up_set S T) by done; pose proof (subseteq_up_set S T)
        | |- context [ up ?s ?T ] =>
           unless (s  up s T) by done; pose proof (elem_of_up s T)
267
        end; auto with sts.
268
Qed.
269
Canonical Structure stsDR : draT := DraT (car sts) sts_dra_mixin.
270
End sts_dra.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
272
273

(** * The STS Resource Algebra *)
(** Finally, the general theory of STS that should be used by users *)
274
275
Notation stsC sts := (validityC (stsDR sts)).
Notation stsR sts := (validityR (stsDR sts)).
Robbert Krebbers's avatar
Robbert Krebbers committed
276
277
278

Section sts_definitions.
  Context {sts : stsT}.
279
  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
280
    to_validity (sts.auth s T).
281
  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
282
    to_validity (sts.frag S T).
283
  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
284
285
286
287
288
289
290
291
292
293
294
295
    sts_frag (sts.up s T) T.
End sts_definitions.
Instance: Params (@sts_auth) 2.
Instance: Params (@sts_frag) 1.
Instance: Params (@sts_frag_up) 2.

Section stsRA.
Import sts.
Context {sts : stsT}.
Implicit Types s : state sts.
Implicit Types S : states sts.
Implicit Types T : tokens sts.
296
Arguments dra_valid _ !_/.
297

Robbert Krebbers's avatar
Robbert Krebbers committed
298
299
(** Setoids *)
Global Instance sts_auth_proper s : Proper (() ==> ()) (sts_auth s).
300
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Global Instance sts_frag_proper : Proper (() ==> () ==> ()) (@sts_frag sts).
302
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Global Instance sts_frag_up_proper s : Proper (() ==> ()) (sts_frag_up s).
304
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
305

Robbert Krebbers's avatar
Robbert Krebbers committed
306
(** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
307
Lemma sts_auth_valid s T :  sts_auth s T  tok s  T.
308
Proof. done. Qed.
309
Lemma sts_frag_valid S T :  sts_frag S T  closed S T   s, s  S.
310
Proof. done. Qed.
Ralf Jung's avatar
Ralf Jung committed
311
312
313
314
315
316
Lemma sts_frag_up_valid s T :  sts_frag_up s T  tok s  T.
Proof.
  split.
  - move=>/sts_frag_valid [H _]. apply H, elem_of_up. 
  - intros. apply sts_frag_valid; split. by apply closed_up. set_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
317

Robbert Krebbers's avatar
Robbert Krebbers committed
318
319
Lemma sts_auth_frag_valid_inv s S T1 T2 :
   (sts_auth s T1  sts_frag S T2)  s  S.
320
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
Ralf Jung's avatar
Ralf Jung committed
321

Robbert Krebbers's avatar
Robbert Krebbers committed
322
323
324
325
(** Op *)
Lemma sts_op_auth_frag s S T :
  s  S  closed S T  sts_auth s   sts_frag S T  sts_auth s T.
Proof.
326
  intros; split; [split|constructor; set_solver]; simpl.
327
  - intros (?&?&?); by apply closed_disjoint with S.
328
  - intros; split_and?; last constructor; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
330
Qed.
Lemma sts_op_auth_frag_up s T :
331
332
333
  sts_auth s   sts_frag_up s T  sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
334
  - intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
335
336
337
  - intros; split_and?.
    + set_solver+.
    + by apply closed_up.
338
    + exists s. set_solver.
339
340
    + constructor; last set_solver. apply elem_of_up.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
341

Ralf Jung's avatar
Ralf Jung committed
342
Lemma sts_op_frag S1 S2 T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
343
  T1  T2  sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
344
345
  sts_frag (S1  S2) (T1  T2)  sts_frag S1 T1  sts_frag S2 T2.
Proof.
346
  intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.
347
  move=>/=[?[? ?]]. split_and!; [set_solver..|constructor; set_solver].
Ralf Jung's avatar
Ralf Jung committed
348
349
Qed.

Ralf Jung's avatar
Ralf Jung committed
350
351
352
353
354
355
356
(* Notice that the following does *not* hold -- the composition of the
   two closures is weaker than the closure with the itnersected token
   set.  Also see up_op.
Lemma sts_op_frag_up s T1 T2 :
  T1 ⊥ T2 → sts_frag_up s (T1 ∪ T2) ≡ sts_frag_up s T1 ⋅ sts_frag_up s T2.
*)

Robbert Krebbers's avatar
Robbert Krebbers committed
357
358
(** Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
359
  steps (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
360
Proof.
361
  intros ?; apply validity_update.
362
  inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_and?.
363
  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
364
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
365
Qed.
Ralf Jung's avatar
Ralf Jung committed
366

367
Lemma sts_update_frag S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
368
  (closed S1 T1  closed S2 T2  S1  S2  T2  T1)  sts_frag S1 T1 ~~> sts_frag S2 T2.
369
Proof.
Ralf Jung's avatar
Ralf Jung committed
370
371
372
  rewrite /sts_frag=> HC HS HT. apply validity_update.
  inversion 3 as [|? S ? Tf|]; simplify_eq/=;
    (destruct HC as (? & ? & ?); first by destruct_and?).
373
374
  - split_and!. done. set_solver. constructor; set_solver.
  - split_and!. done. set_solver. constructor; set_solver.
375
376
Qed.

377
Lemma sts_update_frag_up s1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
378
  (tok s1  T1  closed S2 T2)  s1  S2  T2  T1  sts_frag_up s1 T1 ~~> sts_frag S2 T2.
Ralf Jung's avatar
Ralf Jung committed
379
Proof.
Ralf Jung's avatar
Ralf Jung committed
380
381
382
  intros HC ? HT; apply sts_update_frag. intros HC1; split; last split; eauto using closed_steps.
  - eapply HC, HC1, elem_of_up.
  - rewrite <-HT. eapply up_subseteq; last done. apply HC, HC1, elem_of_up.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
384
Qed.

385
386
Lemma sts_up_set_intersection S1 Sf Tf :
  closed Sf Tf  S1  Sf  S1  up_set (S1  Sf) Tf.
387
388
Proof.
  intros Hclf. apply (anti_symm ()).
389
390
  - move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
  - move=>s [HS1 [s' [/elem_of_mkSet Hsup Hs']]]. split; first done.
391
    eapply closed_steps, Hsup; first done. set_solver +Hs'.
392
393
Qed.

394
Global Instance sts_frag_core_id S : CoreId (sts_frag S ).
Janno's avatar
Janno committed
395
396
397
398
Proof.
  constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
399
(** Inclusion *)
400
401
402
(* This is surprisingly different from to_validity_included. I am not sure
   whether this is because to_validity_included is non-canonical, or this
   one here is non-canonical - but I suspect both. *)
403
(* TODO: These have to be proven again. *)
404
(*
Robbert Krebbers's avatar
Robbert Krebbers committed
405
Lemma sts_frag_included S1 S2 T1 T2 :
406
407
  closed S2 T2 → S2 ≢ ∅ →
  (sts_frag S1 T1 ≼ sts_frag S2 T2) ↔
Robbert Krebbers's avatar
Robbert Krebbers committed
408
  (closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ⊥ Tf ∧
409
410
                                 S2 ≡ S1 ∩ up_set S2 Tf).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
411
  intros ??; split.
412
  - intros [[???] ?].
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
  destruct (to_validity_included (sts_dra.car sts) (sts_dra.frag S1 T1) (sts_dra.frag S2 T2)) as [Hfincl Htoincl].
  intros Hcl2 HS2ne. split.
  - intros Hincl. destruct Hfincl as ((Hcl1 & ?) & (z & EQ & Hval & Hdisj)).
    { split; last done. split; done. }
    clear Htoincl. split_and!; try done; [].
    destruct z as [sf Tf|Sf Tf].
    { exfalso. inversion_clear EQ. }
    exists Tf. inversion_clear EQ as [|? ? ? ? HT2 HS2].
    inversion_clear Hdisj as [? ? ? ? _ HTdisj | |]. split_and!; [done..|].
    rewrite HS2. apply up_set_intersection. apply Hval.
  - intros (Hcl & Hne & (Tf & HT & HTdisj & HS)). destruct Htoincl as ((Hcl' & ?) & (z & EQ)); last first.
    { exists z. exact EQ. } clear Hfincl.
    split; first (split; done). exists (sts_dra.frag (up_set S2 Tf) Tf). split_and!.
    + constructor; done.
    + simpl. split.
      * apply closed_up_set. move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
        set_solver +HT.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
      * by apply up_set_non_empty.
431
    + constructor; last done. by rewrite -HS.
432
433
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
434
Lemma sts_frag_included' S1 S2 T :
435
  closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ →
Robbert Krebbers's avatar
Robbert Krebbers committed
436
  sts_frag S1 T ≼ sts_frag S2 T.
437
Proof.
438
439
  intros. apply sts_frag_included; split_and?; auto.
  exists ∅; split_and?; done || set_solver+.
440
Qed. *)
441
End stsRA.
442
443
444

(** STSs without tokens: Some stuff is simpler *)
Module sts_notok.
445
Structure stsT := Sts {
446
447
448
  state : Type;
  prim_step : relation state;
}.
449
Arguments Sts {_} _.
450
451
452
Arguments prim_step {_} _ _.
Notation states sts := (set (state sts)).

453
454
Definition stsT_token := Empty_set.
Definition stsT_tok {sts : stsT} (_ : state sts) : set stsT_token := .
455

456
Canonical Structure sts_notok (sts : stsT) : sts.stsT :=
457
  sts.Sts (@prim_step sts) stsT_tok.
458
Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.
459

460
461
462
463
Section sts.
  Context {sts : stsT}.
  Implicit Types s : state sts.
  Implicit Types S : states sts.
464

465
  Notation prim_steps := (rtc prim_step).
466

467
468
  Lemma sts_step s1 s2 : prim_step s1 s2  sts.step (s1, ) (s2, ).
  Proof. intros. split; set_solver. Qed.
469

470
471
  Lemma sts_steps s1 s2 : prim_steps s1 s2  sts.steps (s1, ) (s2, ).
  Proof. induction 1; eauto using sts_step, rtc_refl, rtc_l. Qed.
472

473
474
  Lemma frame_prim_step T s1 s2 : sts.frame_step T s1 s2  prim_step s1 s2.
  Proof. inversion 1 as [??? Hstep]. by inversion_clear Hstep. Qed.
475

476
477
478
479
480
  Lemma prim_frame_step T s1 s2 : prim_step s1 s2  sts.frame_step T s1 s2.
  Proof.
    intros Hstep. apply sts.Frame_step with  ; first set_solver.
    by apply sts_step.
  Qed.
481

482
483
484
  Lemma mk_closed S :
    ( s1 s2, s1  S  prim_step s1 s2  s2  S)  sts.closed S .
  Proof. intros ?. constructor; [by set_solver|eauto using frame_prim_step]. Qed.
485
486
487
488
End sts.
End sts_notok.

Notation sts_notokT := sts_notok.stsT.
489
Notation Sts_NoTok := sts_notok.Sts.
490
491

Section sts_notokRA.
492
493
494
495
496
497
498
499
  Context {sts : sts_notokT}.
  Import sts_notok.
  Implicit Types s : state sts.
  Implicit Types S : states sts.

  Lemma sts_notok_update_auth s1 s2 :
    rtc prim_step s1 s2  sts_auth s1  ~~> sts_auth s2 .
  Proof. intros. by apply sts_update_auth, sts_steps. Qed.
500
End sts_notokRA.