sts.v 13.2 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 _ _ !_ /.

8
Module sts.
Ralf Jung's avatar
Ralf Jung committed
9

Robbert Krebbers's avatar
Robbert Krebbers committed
10
Record stsT := STS {
Ralf Jung's avatar
Ralf Jung committed
11 12 13 14 15
  state : Type;
  token : Type;
  trans : relation state;
  tok   : state  set token;
}.
16
Arguments STS {_ _} _ _.
Ralf Jung's avatar
Ralf Jung committed
17 18 19

(* The type of bounds we can give to the state of an STS. This is the type
   that we equip with an RA structure. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Inductive bound (sts : stsT) :=
Ralf Jung's avatar
Ralf Jung committed
21 22 23 24 25
  | bound_auth : state sts  set (token sts)  bound sts
  | bound_frag : set (state sts)  set (token sts ) bound sts.
Arguments bound_auth {_} _ _.
Arguments bound_frag {_} _ _.

Robbert Krebbers's avatar
Robbert Krebbers committed
26
Section sts_core.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Context (sts : stsT).
Robbert Krebbers's avatar
Robbert Krebbers committed
28
Infix "≼" := dra_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
29

Ralf Jung's avatar
Ralf Jung committed
30 31 32 33 34 35 36 37 38 39 40
Notation state := (state sts).
Notation token := (token sts).
Notation trans := (trans sts).
Notation tok := (tok sts).

Inductive equiv : Equiv (bound sts) :=
  | auth_equiv s T1 T2 : T1  T2  bound_auth s T1  bound_auth s T2
  | frag_equiv S1 S2 T1 T2 : T1  T2  S1  S2 
                             bound_frag S1 T1  bound_frag S2 T2.
Global Existing Instance equiv.
Inductive step : relation (state * set token) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
41
  | Step s1 s2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
42 43
     trans s1 s2  tok s1  T1    tok s2  T2   
     tok s1  T1  tok s2  T2  step (s1,T1) (s2,T2).
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Hint Resolve Step.
Ralf Jung's avatar
Ralf Jung committed
45
Inductive frame_step (T : set token) (s1 s2 : state) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  | Frame_step T1 T2 :
47
     T1  (tok s1  T)    step (s1,T1) (s2,T2)  frame_step T s1 s2.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Hint Resolve Frame_step.
Ralf Jung's avatar
Ralf Jung committed
49
Record closed (S : set state) (T : set token) : Prop := Closed {
50
  closed_ne : S  ;
51
  closed_disjoint s : s  S  tok s  T  ;
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53
  closed_step s1 s2 : s1  S  frame_step T s1 s2  s2  S
}.
54 55 56 57 58 59
Lemma closed_disjoint' S T s :
  closed S T  s  S  tok s  T  .
Proof.
  move=>Hcl Hin. move:(closed_disjoint _ _ Hcl _ Hin).
  solve_elem_of+.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Lemma closed_steps S T s1 s2 :
61
  closed S T  s1  S  rtc (frame_step T) s1 s2  s2  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Proof. induction 3; eauto using closed_step. Qed.
Ralf Jung's avatar
Ralf Jung committed
63
Global Instance valid : Valid (bound sts) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
64
  match x with
Ralf Jung's avatar
Ralf Jung committed
65
  | bound_auth s T => tok s  T   | bound_frag S' T => closed S' T
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  end.
Ralf Jung's avatar
Ralf Jung committed
67 68
Definition up (s : state) (T : set token) : set state :=
  mkSet (rtc (frame_step T) s).
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70
Definition up_set (S : set state) (T : set token) : set state :=
  S = λ s, up s T.
Ralf Jung's avatar
Ralf Jung committed
71 72 73 74 75 76
Global Instance unit : Unit (bound sts) := λ x,
  match x with
  | bound_frag S' _ => bound_frag (up_set S'  ) 
  | bound_auth s _  => bound_frag (up s ) 
  end.
Inductive disjoint : Disjoint (bound sts) :=
77
  | frag_frag_disjoint S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
78 79 80 81 82 83 84
     S1  S2    T1  T2    bound_frag S1 T1  bound_frag S2 T2
  | auth_frag_disjoint s S T1 T2 : s  S  T1  T2   
                                   bound_auth s T1  bound_frag S T2
  | frag_auth_disjoint s S T1 T2 : s  S  T1  T2   
                                   bound_frag S T1  bound_auth s T2.
Global Existing Instance disjoint.
Global Instance op : Op (bound sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  match x1, x2 with
Ralf Jung's avatar
Ralf Jung committed
86 87 88 89 90
  | bound_frag S1 T1, bound_frag S2 T2 => bound_frag (S1  S2) (T1  T2)
  | bound_auth s T1, bound_frag _ T2 => bound_auth s (T1  T2)
  | bound_frag _ T1, bound_auth s T2 => bound_auth s (T1  T2)
  | bound_auth s T1, bound_auth _ T2 =>
    bound_auth s (T1  T2)(* never happens *)
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  end.
Ralf Jung's avatar
Ralf Jung committed
92
Global Instance minus : Minus (bound sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  match x1, x2 with
Ralf Jung's avatar
Ralf Jung committed
94 95 96 97 98 99
  | bound_frag S1 T1, bound_frag S2 T2 => bound_frag
                                            (up_set S1 (T1  T2)) (T1  T2)
  | bound_auth s T1, bound_frag _ T2 => bound_auth s (T1  T2)
  | bound_frag _ T2, bound_auth s T1 =>
    bound_auth s (T1  T2) (* never happens *)
  | bound_auth s T1, bound_auth _ T2 => bound_frag (up s (T1  T2)) (T1  T2)
Robbert Krebbers's avatar
Robbert Krebbers committed
100 101
  end.

Ralf Jung's avatar
Ralf Jung committed
102 103
Hint Extern 10 (base.equiv (A:=set _) _ _) => solve_elem_of : sts.
Hint Extern 10 (¬(base.equiv (A:=set _) _ _)) => solve_elem_of : sts.
104 105
Hint Extern 10 (_  _) => solve_elem_of : sts.
Hint Extern 10 (_  _) => solve_elem_of : sts.
Ralf Jung's avatar
Ralf Jung committed
106
Instance: Equivalence (() : relation (bound sts)).
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108 109 110 111 112
Proof.
  split.
  * by intros []; constructor.
  * by destruct 1; constructor.
  * destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
Qed.
113 114 115
Instance framestep_proper : Proper (() ==> (=) ==> (=) ==> impl) frame_step.
Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor; eauto with sts. Qed.
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Proof.
117
  intros ?? HT ?? HS; destruct 1;
Robbert Krebbers's avatar
Robbert Krebbers committed
118
    constructor; intros until 0; rewrite -?HS -?HT; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
Qed.
120 121
Instance closed_proper : Proper (() ==> () ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Lemma closed_op T1 T2 S1 S2 :
123 124
  closed S1 T1  closed S2 T2 
  T1  T2    S1  S2    closed (S1  S2) (T1  T2).
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Proof.
126
  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|].
127 128 129
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
  * 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
130
Qed.
131
Instance up_preserving : Proper ((=) ==> flip () ==> ()) up.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof.
133
  intros s ? <- T T' HT ; apply elem_of_subseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135 136
  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
  eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
137 138
Instance up_proper : Proper ((=) ==> () ==> ()) up.
Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
Ralf Jung's avatar
Ralf Jung committed
139 140 141 142 143
Instance up_set_preserving : Proper (() ==> flip () ==> ()) up_set.
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.
144
Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
146
Lemma elem_of_up s T : s  up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Proof. constructor. Qed.
148
Lemma subseteq_up_set S T : S  up_set S T.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Ralf Jung's avatar
Ralf Jung committed
150 151
Lemma up_up_set s T : up s T  up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
152
Lemma closed_up_set S T :
153
  ( s, s  S  tok s  T  )  S    closed (up_set S T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Proof.
155
  intros HS Hne; unfold up_set; split.
156
  * assert ( s, s  up s T) by eauto using elem_of_up. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
158
    specialize (HS s' Hs'); clear Hs' Hne S.
159
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161 162 163
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
  * intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
    split; [eapply rtc_r|]; eauto.
Qed.
164
Lemma closed_up_set_empty S : S    closed (up_set S ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
165
Proof. eauto using closed_up_set with sts. Qed.
166
Lemma closed_up s T : tok s  T    closed (up s T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
Proof.
168
  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
169
  apply closed_up_set; solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
Qed.
171
Lemma closed_up_empty s : closed (up s ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Proof. eauto using closed_up with sts. Qed.
173
Lemma up_closed S T : closed S T  up_set S T  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
Proof.
175
  intros; split; auto using subseteq_up_set; intros s.
Robbert Krebbers's avatar
Robbert Krebbers committed
176 177 178
  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
Ralf Jung's avatar
Ralf Jung committed
179
Global Instance dra : DRA (bound sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182 183 184 185 186 187
Proof.
  split.
  * apply _.
  * by do 2 destruct 1; constructor; setoid_subst.
  * by destruct 1; constructor; 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,
188
      closed S T  s  S  tok s  T'    tok s  (T  T')  ).
189
    { intros S T T' s [??]; solve_elem_of. }
Robbert Krebbers's avatar
Robbert Krebbers committed
190
    destruct 3; simpl in *; auto using closed_op with sts.
191
  * intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
192 193
  * intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
      rewrite ?disjoint_union_difference; auto using closed_up with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
195
  * intros [] [] []; constructor; rewrite ?assoc; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
196 197 198 199
  * 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.
200
  * intros [|S T]; constructor; auto using elem_of_up with sts.
201
    assert (S  up_set S   S  ) by eauto using subseteq_up_set, closed_ne.
202
    solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
  * intros [|S T]; constructor; auto with sts.
204
    assert (S  up_set S ); auto using subseteq_up_set with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
  * intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
206 207 208
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
    + rewrite (up_closed (up_set _ _));
        eauto using closed_up_set, closed_ne with sts.
209
  * intros x y ?? (z&Hy&?&Hxz); exists (unit (x  y)); split_ands.
210
    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of.
211 212 213 214
    + destruct Hxz; inversion_clear Hy; simpl;
        auto using closed_up_set_empty, closed_up_empty with sts.
    + destruct Hxz; inversion_clear Hy; constructor;
        repeat match goal with
215 216 217 218
        | |- 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)
219 220 221
        end; auto with sts.
  * intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
      repeat match goal with
222 223 224 225
      | |- 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)
226
      end; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
227 228
  * intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
      inversion Hy; clear Hy; constructor; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
229
      rewrite ?disjoint_union_difference; auto.
230
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
231 232 233 234
    apply intersection_greatest; [auto with sts|].
    intros s2; rewrite elem_of_intersection.
    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
235 236
Qed.
Lemma step_closed s1 s2 T1 T2 S Tf :
237
  step (s1,T1) (s2,T2)  closed S Tf  s1  S  T1  Tf   
238
  s2  S  T2  Tf    tok s2  T2  .
Robbert Krebbers's avatar
Robbert Krebbers committed
239
Proof.
240
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
  * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
242
  * solve_elem_of -Hstep Hs1 Hs2.
Robbert Krebbers's avatar
Robbert Krebbers committed
243 244 245
Qed.
End sts_core.

246
Section stsRA.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
Context (sts : stsT).
Robbert Krebbers's avatar
Robbert Krebbers committed
248

Ralf Jung's avatar
Ralf Jung committed
249 250 251 252 253
Canonical Structure RA := validityRA (bound sts).
Definition auth (s : state sts) (T : set (token sts)) : RA :=
  to_validity (bound_auth s T).
Definition frag (S : set (state sts)) (T : set (token sts)) : RA :=
  to_validity (bound_frag S T).
Ralf Jung's avatar
Ralf Jung committed
254

Ralf Jung's avatar
Ralf Jung committed
255 256
Lemma update_auth s1 s2 T1 T2 :
  step sts (s1,T1) (s2,T2)  auth s1 T1 ~~> auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
257
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
Ralf Jung's avatar
Ralf Jung committed
259
  destruct (step_closed sts s1 s2 T1 T2 S Tf) as (?&?&?); auto.
260
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
261
Qed.
Ralf Jung's avatar
Ralf Jung committed
262

Ralf Jung's avatar
Ralf Jung committed
263 264 265
Lemma sts_update_frag S1 S2 (T : set (token sts)) :
  S1  S2  closed sts S2 T 
  frag S1 T ~~> frag S2 T.
266 267 268 269 270 271
Proof.
  move=>HS Hcl. eapply validity_update; inversion 3 as [|? S ? Tf|]; subst.
  - split; first done. constructor; last done. solve_elem_of.
  - split; first done. constructor; solve_elem_of.
Qed.

Ralf Jung's avatar
Ralf Jung committed
272 273 274 275 276
Lemma frag_included S1 S2 T1 T2 :
  closed sts S2 T2 
  frag S1 T1  frag S2 T2  
  (closed sts S1 T1   Tf, T2  T1  Tf  T1  Tf   
                            S2  (S1  up_set sts S2 Tf)).
Ralf Jung's avatar
Ralf Jung committed
277
Proof.
278 279
  move=>Hcl2. split.
  - intros [xf EQ]. destruct xf as [xf vf Hvf]. destruct xf as [Sf Tf|Sf Tf].
280
    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
281
      inversion Hcl2. }
282 283 284
    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]].
285 286 287
    apply Hvf in Hclf. simpl in Hclf. clear Hvf.
    inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
    apply (anti_symm ()).
288
    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
289
      by apply sts.subseteq_up_set.
290
    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
291 292
      destruct Hscl as [s' [Hsup Hs']].
      eapply sts.closed_steps; last (hnf in Hsup; eexact Hsup); first done.
293
      solve_elem_of +HS Hs'.
Ralf Jung's avatar
Ralf Jung committed
294 295
  - intros (Hcl1 & Tf & Htk & Hf & Hs).
    exists (frag (up_set sts S2 Tf) Tf).
296 297 298
    split; first split; simpl;[|done|].
    + intros _. split_ands; first done.
      * apply sts.closed_up_set; last by eapply sts.closed_ne.
Ralf Jung's avatar
Ralf Jung committed
299
        move=>s Hs2. move:(closed_disjoint sts _ _ Hcl2 _ Hs2).
Ralf Jung's avatar
Ralf Jung committed
300
        solve_elem_of +Htk.
301 302 303 304
      * constructor; last done. rewrite -Hs. by eapply sts.closed_ne.
    + intros _. constructor; [ solve_elem_of +Htk | done].
Qed.

Ralf Jung's avatar
Ralf Jung committed
305 306
Lemma frag_included' S1 S2 T :
  closed sts S2 T  closed sts S1 T 
Robbert Krebbers's avatar
Robbert Krebbers committed
307
  S2  S1  sts.up_set sts S2  
Ralf Jung's avatar
Ralf Jung committed
308
  frag S1 T  frag S2 T.
309
Proof.
Ralf Jung's avatar
Ralf Jung committed
310
  intros. apply frag_included; first done.
311 312
  split; first done. exists . split_ands; done || solve_elem_of+.
Qed.
Ralf Jung's avatar
Ralf Jung committed
313

314
End stsRA.
Ralf Jung's avatar
Ralf Jung committed
315 316

End sts.