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 :
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 :
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 {
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.
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 :
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 :
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.
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.
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
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
206
207
     ( s, s  S1  S2)  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.
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.
221
Hint Extern 50 (_ ## _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
222

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
  - intros [] [] [] _ _ _ _ _; constructor; rewrite ?assoc; auto with sts.
248
249
250
251
  - 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 *)
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.
311
Lemma sts_frag_up_valid s T :  sts_frag_up s T  tok s ## T.
Ralf Jung's avatar
Ralf Jung committed
312
313
314
315
316
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 :
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
(* 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 :
354
  T1 ## T2 → sts_frag_up s (T1 ∪ T2) ≡ sts_frag_up s T1 ⋅ sts_frag_up s T2.
Ralf Jung's avatar
Ralf Jung committed
355
356
*)

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 :
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) ↔
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.