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 :=
Robbert Krebbers's avatar
Robbert Krebbers committed
33
  | Frame_step T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
34
     T1  tok s1  T  step (s1,T1) (s2,T2)  frame_step T s1 s2.
Ralf Jung's avatar
Ralf Jung committed
35
Notation frame_steps T := (rtc (frame_step T)).
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38

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

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

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

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

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

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

175 176 177 178
Notation stsT := sts.stsT.
Notation STS := sts.STS.

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
303
(** Validity *)
Robbert Krebbers's avatar
Robbert Krebbers committed
304
Lemma sts_auth_valid s T :  sts_auth s T  tok s  T.
305
Proof. done. Qed.
306
Lemma sts_frag_valid S T :  sts_frag S T  closed S T  S  .
307
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
Lemma sts_frag_up_valid s T : tok s  T   sts_frag_up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
309
Proof. intros. by apply sts_frag_valid; auto using closed_up, up_non_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
310

Robbert Krebbers's avatar
Robbert Krebbers committed
311 312
Lemma sts_auth_frag_valid_inv s S T1 T2 :
   (sts_auth s T1  sts_frag S T2)  s  S.
313
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
Ralf Jung's avatar
Ralf Jung committed
314

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

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

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

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

362 363
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
364
Proof.
365 366
  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
  rewrite <-HT. eapply up_subseteq; done.
Robbert Krebbers's avatar
Robbert Krebbers committed
367 368
Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
413
Lemma sts_frag_included' S1 S2 T :
414
  closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ →
Robbert Krebbers's avatar
Robbert Krebbers committed
415
  sts_frag S1 T ≼ sts_frag S2 T.
416
Proof.
417 418
  intros. apply sts_frag_included; split_and?; auto.
  exists ∅; split_and?; done || set_solver+.
419
Qed. *)
420
End stsRA.
421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494

(** 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)).

Canonical sts_notok (sts : stsT) : sts.stsT :=
  sts.STS (token:=Empty_set) (@prim_step sts) (λ _, ).

Section sts.
Context {sts : stsT}.
Implicit Types s : state sts.
Implicit Types S : states sts.

Notation prim_steps := (rtc prim_step).

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

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.

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

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.

Lemma mk_closed S :
  ( s1 s2, s1  S  prim_step s1 s2  s2  S)  sts.closed S .
Proof.
  intros ?. constructor; first by set_solver.
  intros ????. eauto using frame_prim_step.
Qed.

End sts.
Notation steps := (rtc prim_step).
End sts_notok.

Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.
Notation sts_notokT := sts_notok.stsT.
Notation STS_NoTok := sts_notok.STS.

Section sts_notokRA.
Import sts_notok.
Context {sts : sts_notokT}.
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.

End sts_notokRA.