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

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

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

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

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

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

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

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
336
Lemma sts_op_frag S1 S2 T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
337
  T1  T2  sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
338
339
  sts_frag (S1  S2) (T1  T2)  sts_frag S1 T1  sts_frag S2 T2.
Proof.
340
341
  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
342
343
Qed.

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
419
Lemma sts_frag_included' S1 S2 T :
420
  closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ →
Robbert Krebbers's avatar
Robbert Krebbers committed
421
  sts_frag S1 T ≼ sts_frag S2 T.
422
Proof.
423
424
  intros. apply sts_frag_included; split_and?; auto.
  exists ∅; split_and?; done || set_solver+.
425
Qed. *)
426
End stsRA.
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
495
496
497
498
499
500

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