sts.v 19.9 KB
Newer Older
1
2
3
From iris.prelude Require Export sets.
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 :
Ralf Jung's avatar
Ralf Jung committed
29
     (* TODO: This asks for ⊥ on sets: T1 ⊥ T2 := T1 ∩ T2 ⊆ ∅. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
30
     prim_step s1 s2  tok s1  T1    tok s2  T2   
Ralf Jung's avatar
Ralf Jung committed
31
     tok s1  T1  tok s2  T2  step (s1,T1) (s2,T2).
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Notation steps := (rtc step).
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  | Frame_step T1 T2 :
35
     T1  (tok s1  T)    step (s1,T1) (s2,T2)  frame_step T s1 s2.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38

(** ** Closure under frame steps *)
Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
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 :=
43
  {[ s' | rtc (frame_step 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
54

(** ** Setoids *)
Ralf Jung's avatar
Ralf Jung committed
55
56
57
Instance framestep_mono : Proper (flip () ==> (=) ==> (=) ==> impl) frame_step.
Proof.
  intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
58
    eauto with sts; set_solver.
Ralf Jung's avatar
Ralf Jung committed
59
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Global Instance framestep_proper : Proper (() ==> (=) ==> (=) ==> iff) frame_step.
Ralf Jung's avatar
Ralf Jung committed
61
Proof. by intros ?? [??] ??????; split; apply framestep_mono. Qed.
62
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Proof.
64
  intros ?? HT ?? HS; destruct 1;
Robbert Krebbers's avatar
Robbert Krebbers committed
65
    constructor; intros until 0; rewrite -?HS -?HT; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
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
Proof. by intros ??? ?? [??]; 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
87
88
89

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

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

Notation stsT := sts.stsT.
Notation STS := sts.STS.

(** * STSs form a disjoint RA *)
(* This module should never be imported, uses the module [sts] below. *)
Module sts_dra.
Import sts.

(* 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 {_} _ _.

Section sts_dra.
Context {sts : stsT}.
Infix "≼" := dra_included.
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
Global Existing Instance sts_equiv.
Global Instance sts_valid : Valid (car sts) := λ x,
191
192
  match x with
  | auth s T => tok s  T  
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
  | frag S' T => closed S' T  S'  
  end.
Ralf Jung's avatar
Ralf Jung committed
195
Global Instance sts_core : Core (car sts) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
196
197
198
199
200
201
202
203
204
205
206
  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 :
     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.
207
208
Global Existing Instance sts_disjoint.
Global Instance sts_op : Op (car sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
209
210
211
212
213
214
  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.
215
Global Instance sts_div : Div (car sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
218
219
220
221
222
  match x1, x2 with
  | frag S1 T1, frag S2 T2 => frag (up_set S1 (T1  T2)) (T1  T2)
  | auth s T1, frag _ T2 => auth s (T1  T2)
  | frag _ T2, auth s T1 => auth s (T1  T2) (* never happens *)
  | auth s T1, auth _ T2 => frag (up s (T1  T2)) (T1  T2)
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
225
226
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.
227
Global Instance sts_equivalence: Equivalence (() : relation (car sts)).
Robbert Krebbers's avatar
Robbert Krebbers committed
228
229
Proof.
  split.
230
231
  - by intros []; constructor.
  - by destruct 1; constructor.
232
  - destruct 1; inversion_clear 1; constructor; etrans; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
233
234
Qed.
Global Instance sts_dra : DRA (car sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
Proof.
  split.
237
238
239
240
241
242
  - 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.
  - by do 2 destruct 1; constructor; 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
  - intros []; simpl; intros; destruct_and?; split;
Robbert Krebbers's avatar
Robbert Krebbers committed
246
      eauto using closed_up, up_non_empty, closed_up_set, up_set_empty with sts.
247
  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
248
      setoid_subst; destruct_and?; split_and?;
Robbert Krebbers's avatar
Robbert Krebbers committed
249
250
      rewrite disjoint_union_difference //;
      eauto using up_set_non_empty, up_non_empty, closed_up, closed_disjoint; [].
251
    eapply closed_up_set=> s ?; eapply closed_disjoint; eauto with sts.
252
253
254
255
256
257
258
259
  - 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
260
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
261
    + rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
Ralf Jung's avatar
Ralf Jung committed
262
  - intros x y ?? (z&Hy&?&Hxz); exists (core (x  y)); split_and?.
263
    + destruct Hxz; inversion_clear Hy; constructor; unfold up_set; set_solver.
264
    + destruct Hxz; inversion_clear Hy; simpl; split_and?;
Robbert Krebbers's avatar
Robbert Krebbers committed
265
266
        auto using closed_up_set_empty, closed_up_empty, up_non_empty; [].
      apply up_set_non_empty. set_solver.
267
268
    + destruct Hxz; inversion_clear Hy; constructor;
        repeat match goal with
269
270
271
272
        | |- 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)
273
        end; auto with sts.
274
  - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
275
      repeat match goal with
276
277
278
279
      | |- 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)
280
      end; auto with sts.
281
  - intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
Robbert Krebbers's avatar
Robbert Krebbers committed
282
      inversion Hy; clear Hy; constructor; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
283
      rewrite ?disjoint_union_difference; auto.
284
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
285
    apply intersection_greatest; [auto with sts|].
286
    intros s2; rewrite elem_of_intersection. destruct_and?.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
    unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
    apply closed_steps with T2 s1; auto with sts.
289
Qed.
290
Canonical Structure R : cmraT := validityR (car sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
291
292
293
294
End sts_dra. End sts_dra.

(** * The STS Resource Algebra *)
(** Finally, the general theory of STS that should be used by users *)
295
Notation stsR := (@sts_dra.R).
Robbert Krebbers's avatar
Robbert Krebbers committed
296
297
298

Section sts_definitions.
  Context {sts : stsT}.
299
  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
300
    to_validity (sts_dra.auth s T).
301
  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
302
    to_validity (sts_dra.frag S T).
303
  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
304
305
306
307
308
309
310
311
312
313
314
315
316
    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.

317
Global Instance sts_cmra_discrete : CMRADiscrete (stsR sts).
318
319
Proof. apply validity_cmra_discrete. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
320
321
322
323
324
325
326
(** Setoids *)
Global Instance sts_auth_proper s : Proper (() ==> ()) (sts_auth s).
Proof. (* this proof is horrible *)
  intros T1 T2 HT. rewrite /sts_auth.
  by eapply to_validity_proper; try apply _; constructor.
Qed.
Global Instance sts_frag_proper : Proper (() ==> () ==> ()) (@sts_frag sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
327
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
329
  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
  by eapply to_validity_proper; try apply _; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
330
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
Global Instance sts_frag_up_proper s : Proper (() ==> ()) (sts_frag_up s).
Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
333

Robbert Krebbers's avatar
Robbert Krebbers committed
334
335
(** Validity *)
Lemma sts_auth_valid s T :  sts_auth s T  tok s  T  .
336
Proof. done. Qed.
337
Lemma sts_frag_valid S T :  sts_frag S T  closed S T  S  .
338
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
Lemma sts_frag_up_valid s T : tok s  T     sts_frag_up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
340
Proof. intros. by apply sts_frag_valid; auto using closed_up, up_non_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
341

Robbert Krebbers's avatar
Robbert Krebbers committed
342
343
Lemma sts_auth_frag_valid_inv s S T1 T2 :
   (sts_auth s T1  sts_frag S T2)  s  S.
344
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
Ralf Jung's avatar
Ralf Jung committed
345

Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
348
349
(** 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.
350
  intros; split; [split|constructor; set_solver]; simpl.
351
  - intros (?&?&?); by apply closed_disjoint with S.
352
  - intros; split_and?; last constructor; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
353
354
Qed.
Lemma sts_op_auth_frag_up s T :
355
356
357
  sts_auth s   sts_frag_up s T  sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
358
  - intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
359
360
361
  - intros; split_and?.
    + set_solver+.
    + by apply closed_up.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
    + apply up_non_empty.
363
364
    + constructor; last set_solver. apply elem_of_up.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
365

Ralf Jung's avatar
Ralf Jung committed
366
Lemma sts_op_frag S1 S2 T1 T2 :
367
  T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
368
369
  sts_frag (S1  S2) (T1  T2)  sts_frag S1 T1  sts_frag S2 T2.
Proof.
370
371
  intros HT HS1 HS2. rewrite /sts_frag.
  (* FIXME why does rewrite not work?? *)
372
373
374
  etrans; last eapply to_validity_op; first done; [].
  move=>/=[??]. split_and!; [auto; set_solver..|].
  constructor; done.
Ralf Jung's avatar
Ralf Jung committed
375
376
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
377
378
(** Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
379
  steps (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
380
Proof.
381
  intros ?; apply validity_update.
382
  inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_and?.
383
  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
384
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
385
Qed.
Ralf Jung's avatar
Ralf Jung committed
386

387
388
Lemma sts_update_frag S1 S2 T1 T2 :
  closed S2 T2  S1  S2  T2  T1  sts_frag S1 T1 ~~> sts_frag S2 T2.
389
Proof.
390
  rewrite /sts_frag=> ? HS HT. apply validity_update.
391
  inversion 3 as [|? S ? Tf|]; simplify_eq/=.
392
393
  - split_and!; first done; first set_solver. constructor; set_solver.
  - split_and!; first done; first set_solver. constructor; set_solver.
394
395
Qed.

396
397
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
398
Proof.
399
400
  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
  rewrite <-HT. eapply up_subseteq; done.
Robbert Krebbers's avatar
Robbert Krebbers committed
401
402
Qed.

403
404
405
406
407
Lemma up_set_intersection S1 Sf Tf :
  closed Sf Tf  
  S1  Sf  S1  up_set (S1  Sf) Tf.
Proof.
  intros Hclf. apply (anti_symm ()).
408
409
410
  + 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.
    eapply closed_steps, Hsup; first done. set_solver +Hs'.
411
412
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
413
(** Inclusion *)
414
415
416
(* 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
417
Lemma sts_frag_included S1 S2 T1 T2 :
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
  closed S2 T2  S2   
  (sts_frag S1 T1  sts_frag S2 T2) 
  (closed S1 T1  S1     Tf, T2  T1  Tf  T1  Tf   
                                 S2  S1  up_set S2 Tf).
Proof.
  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
440
      * by apply up_set_non_empty.
441
    + constructor; last done. by rewrite -HS.
442
443
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
444
Lemma sts_frag_included' S1 S2 T :
445
  closed S2 T  closed S1 T  S2    S1    S2  S1  up_set S2  
Robbert Krebbers's avatar
Robbert Krebbers committed
446
  sts_frag S1 T  sts_frag S2 T.
447
Proof.
448
449
  intros. apply sts_frag_included; split_and?; auto.
  exists ; split_and?; done || set_solver+.
450
Qed.
451

452
End stsRA.
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
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527

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