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

Robbert Krebbers's avatar
Robbert Krebbers committed
8
(** * Definition of STSs *)
9
Module sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
32
Definition 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 :=
Ralf Jung's avatar
Ralf Jung committed
43
  mkSet (rtc (frame_step T) 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
73
74
  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
  eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
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
80
81
Proof.
  intros S1 S2 HS T1 T2 HT. rewrite /up_set.
  f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
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
109
110
111
112
113
114
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.
  remember (s1,T1) as sT1. remember (s2,T2) as sT2. intros Hsteps.
  revert s1 T1 HeqsT1 s2 T2 HeqsT2.
  induction Hsteps as [?|? [s' T'] ? Hstep Hsteps IH]; intros; subst.
  - case: HeqsT2=>? ?. subst. done.
  - eapply step_closed in Hstep; [|done..]. destruct_conjs. eauto.
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 !elem_of_bind; 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
144
145
146
147
148
149
150
151
152
Lemma up_set_empty S T : up_set S T    S  .
Proof.
  move:(subseteq_up_set S T). set_solver.
Qed.
Lemma up_set_nonempty S T : S    up_set S T  .
Proof. by move=>? /up_set_empty. Qed.
Lemma up_nonempty s T : up s T  .
Proof.
  move:(elem_of_up s T). set_solver.
Qed.
153
Lemma up_closed S T : closed S T  up_set S T  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Proof.
155
  intros; split; auto using subseteq_up_set; intros s.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
157
158
  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
Ralf Jung's avatar
Ralf Jung committed
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' ?. eapply closed_steps; done. Qed.
Lemma up_set_subseteq S1 T S2 :
  closed S2 T  S1  S2  sts.up_set S1 T  S2.
Proof. move=>? ? s [s' [? ?]]. eapply closed_steps; by eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
End sts. End sts.

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.
Existing Instance sts_equiv.
Instance sts_valid : Valid (car sts) := λ x,
194
195
196
  match x with
  | auth s T => tok s  T  
  | frag S' T => closed S' T  S'   end.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
Instance sts_unit : Unit (car sts) := λ x,
  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.
Existing Instance sts_disjoint.
Instance sts_op : Op (car sts) := λ x1 x2,
  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.
Instance sts_minus : Minus (car sts) := λ x1 x2,
  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.

225
226
227
228
Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 10 (_  _) => set_solver : sts.
Hint Extern 10 (_  _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
Instance sts_equivalence: Equivalence (() : relation (car sts)).
Proof.
  split.
232
233
  - by intros []; constructor.
  - by destruct 1; constructor.
234
  - destruct 1; inversion_clear 1; constructor; etrans; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
235
236
Qed.
Global Instance sts_dra : DRA (car sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
Proof.
  split.
239
240
241
242
243
244
245
  - 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.
  - assert ( T T' S s,
246
      closed S T  s  S  tok s  T'    tok s  (T  T')  ).
247
    { intros S T T' s [??]; set_solver. }
248
249
250
251
252
253
254
255
256
257
258
    destruct 3; simpl in *; destruct_conjs; auto using closed_op with sts.
  - intros []; simpl; intros; destruct_conjs; split;
      eauto using closed_up, up_nonempty, closed_up_set, up_set_empty with sts.
  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
      setoid_subst; destruct_conjs; split_and?;
      (* TODO improve this. *)
      eauto using up_set_nonempty, up_nonempty;
      assert ((T1  T2)  T1  T2) as -> by set_solver;
      eauto using closed_up, closed_disjoint; [].
    eapply closed_up_set. intros.
    eapply closed_disjoint; first done. set_solver.
259
260
261
262
263
264
  - 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.
265
    simpl in *. assert (S  up_set S ) by eauto using subseteq_up_set.
266
    set_solver.
267
  - intros [|S T]; constructor; auto with sts.
268
    assert (S  up_set S ); auto using subseteq_up_set with sts.
269
  - intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
271
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
    + rewrite (up_closed (up_set _ _));
272
        eauto using closed_up_set with sts.
273
  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x  y)); split_and?.
274
    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver.
275
276
277
    + destruct Hxz; inversion_clear Hy; simpl; split_and?;
        auto using closed_up_set_empty, closed_up_empty, up_nonempty; [].
      eapply up_set_nonempty. set_solver.
278
279
    + destruct Hxz; inversion_clear Hy; constructor;
        repeat match goal with
280
281
282
283
        | |- 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)
284
        end; auto with sts.
285
  - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
286
      repeat match goal with
287
288
289
290
      | |- 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)
291
      end; auto with sts.
292
  - intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
Robbert Krebbers's avatar
Robbert Krebbers committed
293
      inversion Hy; clear Hy; constructor; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
294
      rewrite ?disjoint_union_difference; auto.
295
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
296
    apply intersection_greatest; [auto with sts|].
297
    intros s2; rewrite elem_of_intersection. destruct_conjs.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
299
    unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
    apply closed_steps with T2 s1; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
Canonical Structure RA : cmraT := validityRA (car sts).
End sts_dra. End sts_dra.

(** * The STS Resource Algebra *)
(** Finally, the general theory of STS that should be used by users *)
Notation stsRA := (@sts_dra.RA).

Section sts_definitions.
  Context {sts : stsT}.
  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
    to_validity (sts_dra.auth s T).
  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsRA sts :=
    to_validity (sts_dra.frag S T).
  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
    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.

(** 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
335
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
337
  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
  by eapply to_validity_proper; try apply _; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
339
340
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
341

Robbert Krebbers's avatar
Robbert Krebbers committed
342
343
344
(** Validity *)
Lemma sts_auth_valid s T :  sts_auth s T  tok s  T  .
Proof. split. by move=> /(_ 0). by intros ??. Qed.
345
Lemma sts_frag_valid S T :  sts_frag S T  closed S T  S  .
Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
Proof. split. by move=> /(_ 0). by intros ??. Qed.
Lemma sts_frag_up_valid s T : tok s  T     sts_frag_up s T.
348
Proof. intros. by apply sts_frag_valid; auto using closed_up, up_nonempty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349

Robbert Krebbers's avatar
Robbert Krebbers committed
350
351
352
Lemma sts_auth_frag_valid_inv s S T1 T2 :
   (sts_auth s T1  sts_frag S T2)  s  S.
Proof. by move=> /(_ 0) [? [? Hdisj]]; inversion Hdisj. Qed.
Ralf Jung's avatar
Ralf Jung committed
353

Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
356
357
(** 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.
358
  intros; split; [split|constructor; set_solver]; simpl.
359
  - intros (?&?&?); by apply closed_disjoint with S.
360
361
362
  - intros; split_and?.
    + set_solver+.
    + done.
363
    + set_solver.
364
    + constructor; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
365
366
Qed.
Lemma sts_op_auth_frag_up s T :
367
368
369
  sts_auth s   sts_frag_up s T  sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
370
371
  - intros (?&?&?). destruct_conjs.
    apply closed_disjoint with (up s T); first done.
372
373
374
375
    apply elem_of_up.
  - intros; split_and?.
    + set_solver+.
    + by apply closed_up.
376
    + apply up_nonempty.
377
378
    + constructor; last set_solver. apply elem_of_up.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
379

Ralf Jung's avatar
Ralf Jung committed
380
Lemma sts_op_frag S1 S2 T1 T2 :
381
  T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
382
383
  sts_frag (S1  S2) (T1  T2)  sts_frag S1 T1  sts_frag S2 T2.
Proof.
384
385
  intros HT HS1 HS2. rewrite /sts_frag.
  (* FIXME why does rewrite not work?? *)
386
387
388
  etrans; last eapply to_validity_op; first done; [].
  move=>/=[??]. split_and!; [auto; set_solver..|].
  constructor; done.
Ralf Jung's avatar
Ralf Jung committed
389
390
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
391
392
(** Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
393
  steps (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
394
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
396
  simpl in *. destruct_conjs.
397
  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
398
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
399
Qed.
Ralf Jung's avatar
Ralf Jung committed
400

401
402
Lemma sts_update_frag S1 S2 T1 T2 :
  closed S2 T2  S1  S2  T2  T1  sts_frag S1 T1 ~~> sts_frag S2 T2.
403
Proof.
404
  rewrite /sts_frag=> ? HS HT. apply validity_update.
405
  inversion 3 as [|? S ? Tf|]; simplify_eq/=.
406
407
  - split_and!; first done; first set_solver. constructor; set_solver.
  - split_and!; first done; first set_solver. constructor; set_solver.
408
409
Qed.

410
411
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
412
Proof.
413
414
  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
  rewrite <-HT. eapply up_subseteq; done.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
416
417
Qed.

(** Inclusion *)
418
(*
Robbert Krebbers's avatar
Robbert Krebbers committed
419
Lemma sts_frag_included S1 S2 T1 T2 :
420
  closed S2 T2 → S2 ≢ ∅
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
423
424
  sts_frag S1 T1 ≼ sts_frag S2 T2 ↔
  (closed S1 T1 ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ∩ Tf ≡ ∅ ∧ S2 ≡ S1 ∩ up_set S2 Tf).
Proof. (* This should use some general properties of DRAs. To be improved
when we have RAs back *)
425
  move=>Hcl2. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
  - intros [[[Sf Tf|Sf Tf] vf Hvf] EQ].
427
    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
428
      inversion Hcl2. }
429
430
431
    inversion_clear EQ as [Hv EQ'].
    move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS].
    destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1  [Hclf Hdisj]].
432
    apply Hvf in Hclf. simpl in Hclf. clear Hvf.
433
    inversion_clear Hdisj. split; last (exists Tf; split_and?); [done..|].
434
    apply (anti_symm (⊆)).
435
    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
Robbert Krebbers's avatar
Robbert Krebbers committed
436
      by apply subseteq_up_set.
437
    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
438
      destruct Hscl as [s' [Hsup Hs']].
Robbert Krebbers's avatar
Robbert Krebbers committed
439
      eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
440
      set_solver +HS Hs'.
Ralf Jung's avatar
Ralf Jung committed
441
  - intros (Hcl1 & Tf & Htk & Hf & Hs).
Robbert Krebbers's avatar
Robbert Krebbers committed
442
    exists (sts_frag (up_set S2 Tf) Tf).
443
    split; first split; simpl;[|done|].
444
    + intros _. split_and?; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
445
446
      * apply closed_up_set; last by eapply closed_ne.
        move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
447
        set_solver +Htk.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
      * constructor; last done. rewrite -Hs. by eapply closed_ne.
449
    + intros _. constructor; [ set_solver +Htk | done].
450
451
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
452
453
454
Lemma sts_frag_included' S1 S2 T :
  closed S2 T → closed S1 T → S2 ≡ S1 ∩ up_set S2 ∅ →
  sts_frag S1 T ≼ sts_frag S2 T.
455
Proof.
456
457
  intros. apply sts_frag_included; split_and?; auto.
  exists ∅; split_and?; done || set_solver+.
458
Qed.
459
*)
460
End stsRA.