sts.v 18.1 KB
Newer Older
1
From iris.prelude Require Export set.
2 3
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Ralf Jung's avatar
Ralf Jung committed
6
Local Arguments core _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
(** Tactic setup *)
Hint Resolve Step.
50 51 52 53
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
54
Hint Extern 50 (_  _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56

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

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

(** ** Properties of the closure operators *)
121
Lemma elem_of_up s T : s  up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof. constructor. Qed.
123
Lemma subseteq_up_set S T : S  up_set S T.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
125 126
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
127 128
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
129
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
130
Proof.
131
  intros HS; unfold up_set; split.
132
  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
133
    specialize (HS s' Hs'); clear Hs' S.
134
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
136
  - intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; exists s.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
    split; [eapply rtc_r|]; eauto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Lemma closed_up s T : tok s  T  closed (up s T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Proof.
141
  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
142
  apply closed_up_set; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
Qed.
144 145
Lemma closed_up_set_empty S : closed (up_set S ) .
Proof. eauto using closed_up_set with sts. Qed.
146
Lemma closed_up_empty s : closed (up s ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Proof. eauto using closed_up with sts. Qed.
148
Lemma up_closed S T : closed S T  up_set S T  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Proof.
150 151
  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
152 153
  induction Hstep; eauto using closed_step.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156 157 158 159 160
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.
End sts.

Notation steps := (rtc step).
Ralf Jung's avatar
Ralf Jung committed
161
Notation frame_steps T := (rtc (frame_step T)).
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163 164 165 166 167 168 169

(* 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 {_} _ _.
170
End sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
171

172 173 174 175
Notation stsT := sts.stsT.
Notation STS := sts.STS.

(** * STSs form a disjoint RA *)
Robbert Krebbers's avatar
Robbert Krebbers committed
176
Section sts_dra.
177 178
Context (sts : stsT).
Import sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
179 180 181 182 183 184
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.
185 186
Existing Instance sts_equiv.
Instance sts_valid : Valid (car sts) := λ x,
187
  match x with
Robbert Krebbers's avatar
Robbert Krebbers committed
188
  | auth s T => tok s  T
189
  | frag S' T => closed S' T   s, s  S'
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  end.
191
Instance sts_core : Core (car sts) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
192 193 194 195 196 197
  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 :
198
     ( s, s  S1  S2)  T1  T2  frag S1 T1  frag S2 T2
Robbert Krebbers's avatar
Robbert Krebbers committed
199 200
  | 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.
201 202
Existing Instance sts_disjoint.
Instance sts_op : Op (car sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205 206 207 208 209
  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
210
Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
211
Hint Extern 50 ( s : state sts, _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
212 213
Hint Extern 50 (_  _) => set_solver : sts.
Hint Extern 50 (_  _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
214 215
Hint Extern 50 (_  _) => set_solver : sts.

216 217 218 219 220 221
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
222 223
Proof.
  split.
224 225
  - by intros []; constructor.
  - by destruct 1; constructor.
226
  - destruct 1; inversion_clear 1; constructor; etrans; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
Qed.
228
Lemma sts_dra_mixin : DRAMixin (car sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230
Proof.
  split.
231 232 233 234
  - apply _.
  - by do 2 destruct 1; constructor; setoid_subst.
  - by destruct 1; constructor; setoid_subst.
  - by destruct 1; simpl; intros ?; setoid_subst.
235
  - by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.
236
  - destruct 3; simpl in *; destruct_and?; eauto using closed_op;
237
      match goal with H : closed _ _ |- _ => destruct H end; set_solver.
238 239
  - intros []; naive_solver eauto using closed_up, closed_up_set,
      elem_of_up, elem_of_up_set with sts.
240 241 242 243 244
  - 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.
245 246
  - intros []; constructor; eauto with sts.
  - intros []; constructor; auto with sts.
247
  - intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
248
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
249
    + rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251
  - intros x y. exists (core (x  y))=> ?? Hxy; split_and?.
    + destruct Hxy; constructor; unfold up_set; set_solver.
252 253 254
    + destruct Hxy; simpl;
        eauto using closed_up_set_empty, closed_up_empty with sts.
    + destruct Hxy; econstructor;
255
        repeat match goal with
256 257 258 259
        | |- 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)
260
        end; auto with sts.
261
Qed.
262 263
Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin.
End sts_dra.
Robbert Krebbers's avatar
Robbert Krebbers committed
264 265 266

(** * The STS Resource Algebra *)
(** Finally, the general theory of STS that should be used by users *)
267 268
Notation stsC sts := (validityC (stsDR sts)).
Notation stsR sts := (validityR (stsDR sts)).
Robbert Krebbers's avatar
Robbert Krebbers committed
269 270 271

Section sts_definitions.
  Context {sts : stsT}.
272
  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
273
    to_validity (sts.auth s T).
274
  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
275
    to_validity (sts.frag S T).
276
  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
277 278 279 280 281 282 283 284 285 286 287 288
    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.
289
Arguments dra_valid _ !_/.
290

Robbert Krebbers's avatar
Robbert Krebbers committed
291 292
(** Setoids *)
Global Instance sts_auth_proper s : Proper (() ==> ()) (sts_auth s).
293
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
Global Instance sts_frag_proper : Proper (() ==> () ==> ()) (@sts_frag sts).
295
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
296
Global Instance sts_frag_up_proper s : Proper (() ==> ()) (sts_frag_up s).
297
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298

Robbert Krebbers's avatar
Robbert Krebbers committed
299
(** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Lemma sts_auth_valid s T :  sts_auth s T  tok s  T.
301
Proof. done. Qed.
302
Lemma sts_frag_valid S T :  sts_frag S T  closed S T   s, s  S.
303
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
Lemma sts_frag_up_valid s T : tok s  T   sts_frag_up s T.
305
Proof. intros. apply sts_frag_valid; split. by apply closed_up. set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
306

Robbert Krebbers's avatar
Robbert Krebbers committed
307 308
Lemma sts_auth_frag_valid_inv s S T1 T2 :
   (sts_auth s T1  sts_frag S T2)  s  S.
309
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
Ralf Jung's avatar
Ralf Jung committed
310

Robbert Krebbers's avatar
Robbert Krebbers committed
311 312 313 314
(** 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.
315
  intros; split; [split|constructor; set_solver]; simpl.
316
  - intros (?&?&?); by apply closed_disjoint with S.
317
  - intros; split_and?; last constructor; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
318 319
Qed.
Lemma sts_op_auth_frag_up s T :
320 321 322
  sts_auth s   sts_frag_up s T  sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
323
  - intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
324 325 326
  - intros; split_and?.
    + set_solver+.
    + by apply closed_up.
327
    + exists s. set_solver.
328 329
    + constructor; last set_solver. apply elem_of_up.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
330

Ralf Jung's avatar
Ralf Jung committed
331
Lemma sts_op_frag S1 S2 T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
332
  T1  T2  sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
333 334
  sts_frag (S1  S2) (T1  T2)  sts_frag S1 T1  sts_frag S2 T2.
Proof.
335
  intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.
336
  move=>/=[?[? ?]]. split_and!; [set_solver..|constructor; set_solver].
Ralf Jung's avatar
Ralf Jung committed
337 338
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
339 340
(** Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
341
  steps (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
Proof.
343
  intros ?; apply validity_update.
344
  inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_and?.
345
  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
346
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
347
Qed.
Ralf Jung's avatar
Ralf Jung committed
348

349 350
Lemma sts_update_frag S1 S2 T1 T2 :
  closed S2 T2  S1  S2  T2  T1  sts_frag S1 T1 ~~> sts_frag S2 T2.
351
Proof.
352
  rewrite /sts_frag=> ? HS HT. apply validity_update.
353
  inversion 3 as [|? S ? Tf|]; simplify_eq/=.
354 355
  - split_and!. done. set_solver. constructor; set_solver.
  - split_and!. done. set_solver. constructor; set_solver.
356 357
Qed.

358 359
Lemma sts_update_frag_up s1 S2 T1 T2 :
  closed S2 T2  s1  S2  T2  T1  sts_frag_up s1 T1 ~~> sts_frag S2 T2.
Ralf Jung's avatar
Ralf Jung committed
360
Proof.
361 362
  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
  rewrite <-HT. eapply up_subseteq; done.
Robbert Krebbers's avatar
Robbert Krebbers committed
363 364
Qed.

365 366
Lemma sts_up_set_intersection S1 Sf Tf :
  closed Sf Tf  S1  Sf  S1  up_set (S1  Sf) Tf.
367 368
Proof.
  intros Hclf. apply (anti_symm ()).
369 370
  - 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.
371
    eapply closed_steps, Hsup; first done. set_solver +Hs'.
372 373
Qed.

Janno's avatar
Janno committed
374 375 376 377 378
Global Instance sts_frag_peristent S : Persistent (sts_frag S ).
Proof.
  constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
379
(** Inclusion *)
380 381 382
(* 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. *)
383
(* TODO: These have to be proven again. *)
384
(*
Robbert Krebbers's avatar
Robbert Krebbers committed
385
Lemma sts_frag_included S1 S2 T1 T2 :
386 387
  closed S2 T2 → S2 ≢ ∅ →
  (sts_frag S1 T1 ≼ sts_frag S2 T2) ↔
Robbert Krebbers's avatar
Robbert Krebbers committed
388
  (closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ⊥ Tf ∧
389 390
                                 S2 ≡ S1 ∩ up_set S2 Tf).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
391
  intros ??; split.
392
  - intros [[???] ?].
393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409
  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
410
      * by apply up_set_non_empty.
411
    + constructor; last done. by rewrite -HS.
412 413
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
414
Lemma sts_frag_included' S1 S2 T :
415
  closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ →
Robbert Krebbers's avatar
Robbert Krebbers committed
416
  sts_frag S1 T ≼ sts_frag S2 T.
417
Proof.
418 419
  intros. apply sts_frag_included; split_and?; auto.
  exists ∅; split_and?; done || set_solver+.
420
Qed. *)
421
End stsRA.
422 423 424 425 426 427 428 429 430 431 432

(** STSs without tokens: Some stuff is simpler *)
Module sts_notok.
Structure stsT := STS {
  state : Type;
  prim_step : relation state;
}.
Arguments STS {_} _.
Arguments prim_step {_} _ _.
Notation states sts := (set (state sts)).

433 434
Definition stsT_token := Empty_set.
Definition stsT_tok {sts : stsT} (_ : state sts) : set stsT_token := .
435

436 437 438
Canonical Structure sts_notok (sts : stsT) : sts.stsT :=
  sts.STS (@prim_step sts) stsT_tok.
Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.
439

440 441 442 443
Section sts.
  Context {sts : stsT}.
  Implicit Types s : state sts.
  Implicit Types S : states sts.
444

445
  Notation prim_steps := (rtc prim_step).
446

447 448
  Lemma sts_step s1 s2 : prim_step s1 s2  sts.step (s1, ) (s2, ).
  Proof. intros. split; set_solver. Qed.
449

450 451
  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.
452

453 454
  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.
455

456 457 458 459 460
  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.
461

462 463 464
  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.
465 466 467 468 469 470 471
End sts.
End sts_notok.

Notation sts_notokT := sts_notok.stsT.
Notation STS_NoTok := sts_notok.STS.

Section sts_notokRA.
472 473 474 475 476 477 478 479
  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.
480
End sts_notokRA.