sts.v 18.7 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).
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 :=
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
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 !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
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.
195
Global Instance sts_unit : Unit (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_minus : Minus (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.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
  - (* (* assert (∀ T T' S s,
244
      closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247 248 249 250 251 252 253 254
    { intros S T T' s [??]. set_solver. } *)


    destruct 3; simpl in *; destruct_conjs;
      repeat match goal with H : closed _ _ |- _ => destruct H end; eauto using closed_op with sts.
split. auto with sts. 

 destruct_conjs. eauto using closed_op with sts.
admit.
eapply H. eauto. eauto. *) admit.
255
  - intros []; simpl; intros; destruct_conjs; split;
Robbert Krebbers's avatar
Robbert Krebbers committed
256
      eauto using closed_up, up_non_empty, closed_up_set, up_set_empty with sts.
257 258
  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
      setoid_subst; destruct_conjs; split_and?;
Robbert Krebbers's avatar
Robbert Krebbers committed
259 260
      rewrite disjoint_union_difference //;
      eauto using up_set_non_empty, up_non_empty, closed_up, closed_disjoint; [].
261
    eapply closed_up_set. intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
262
    eapply closed_disjoint; eauto with sts.
263 264 265 266 267 268
  - 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
    assert (S  up_set S ) by eauto using subseteq_up_set.
270
    set_solver.
271
  - intros [|S T]; constructor; auto with sts.
272
    assert (S  up_set S ); auto using subseteq_up_set with sts.
273
  - intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
274 275
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
    + rewrite (up_closed (up_set _ _));
276
        eauto using closed_up_set with sts.
277
  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x  y)); split_and?.
278
    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver.
279
    + destruct Hxz; inversion_clear Hy; simpl; split_and?;
Robbert Krebbers's avatar
Robbert Krebbers committed
280 281
        auto using closed_up_set_empty, closed_up_empty, up_non_empty; [].
      apply up_set_non_empty. set_solver.
282 283
    + destruct Hxz; inversion_clear Hy; constructor;
        repeat match goal with
284 285 286 287
        | |- 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)
288
        end; auto with sts.
289
  - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
290
      repeat match goal with
291 292 293 294
      | |- 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)
295
      end; auto with sts.
296
  - intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
Robbert Krebbers's avatar
Robbert Krebbers committed
297
      inversion Hy; clear Hy; constructor; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
298
      rewrite ?disjoint_union_difference; auto.
299
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
300
    apply intersection_greatest; [auto with sts|].
301
    intros s2; rewrite elem_of_intersection. destruct_conjs.
Robbert Krebbers's avatar
Robbert Krebbers committed
302 303
    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
304
Admitted.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 335 336 337 338
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
339
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341
  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
  by eapply to_validity_proper; try apply _; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
343 344
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
345

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

Robbert Krebbers's avatar
Robbert Krebbers committed
354 355 356
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
357

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

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

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

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

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

421 422 423 424 425 426 427 428 429 430 431 432 433
Lemma up_set_intersection S1 Sf Tf :
  closed Sf Tf  
  S1  Sf  S1  up_set (S1  Sf) Tf.
Proof.
  intros Hclf. apply (anti_symm ()).
  + move=>s [HS1 HSf]. split; first by apply HS1.
    by apply subseteq_up_set.
  + move=>s [HS1 Hscl]. split; first done.
    destruct Hscl as [s' [Hsup Hs']].
    eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
    set_solver +Hs'.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
434
(** Inclusion *)
435 436 437
(* 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
438
Lemma sts_frag_included S1 S2 T1 T2 :
439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460
  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
461
      * by apply up_set_non_empty.
462
    + constructor; last done. by rewrite -HS.
463 464
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
465
Lemma sts_frag_included' S1 S2 T :
466
  closed S2 T  closed S1 T  S2    S1    S2  S1  up_set S2  
Robbert Krebbers's avatar
Robbert Krebbers committed
467
  sts_frag S1 T  sts_frag S2 T.
468
Proof.
469 470
  intros. apply sts_frag_included; split_and?; auto.
  exists ; split_and?; done || set_solver+.
471
Qed.
472

473
End stsRA.