sts.v 13 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 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24

Record Sts := {
  state : Type;
  token : Type;
  trans : relation state;
  tok   : state  set token;
}.

(* 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 bound (sts : Sts) :=
  | 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
25
Section sts_core.
Ralf Jung's avatar
Ralf Jung committed
26
Context (sts : Sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Infix "≼" := dra_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
28

Ralf Jung's avatar
Ralf Jung committed
29 30 31 32 33 34 35 36 37 38 39
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
40
  | Step s1 s2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
41 42
     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
43
Hint Resolve Step.
Ralf Jung's avatar
Ralf Jung committed
44
Inductive frame_step (T : set token) (s1 s2 : state) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  | Frame_step T1 T2 :
46
     T1  (tok s1  T)    step (s1,T1) (s2,T2)  frame_step T s1 s2.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Hint Resolve Frame_step.
Ralf Jung's avatar
Ralf Jung committed
48
Record closed (S : set state) (T : set token) : Prop := Closed {
49
  closed_ne : S  ;
50
  closed_disjoint s : s  S  tok s  T  ;
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53
  closed_step s1 s2 : s1  S  frame_step T s1 s2  s2  S
}.
Lemma closed_steps S T s1 s2 :
54
  closed S T  s1  S  rtc (frame_step T) s1 s2  s2  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Proof. induction 3; eauto using closed_step. Qed.
Ralf Jung's avatar
Ralf Jung committed
56
Global Instance valid : Valid (bound sts) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  match x with
Ralf Jung's avatar
Ralf Jung committed
58
  | bound_auth s T => tok s  T   | bound_frag S' T => closed S' T
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  end.
Ralf Jung's avatar
Ralf Jung committed
60 61 62 63 64 65 66 67 68 69
Definition up (s : state) (T : set token) : set state :=
  mkSet (rtc (frame_step T) s).
Definition up_set (S : set state) (T : set token) : set state
  := S = λ s, up s T.
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) :=
70
  | frag_frag_disjoint S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
71 72 73 74 75 76 77
     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
78
  match x1, x2 with
Ralf Jung's avatar
Ralf Jung committed
79 80 81 82 83
  | 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
84
  end.
Ralf Jung's avatar
Ralf Jung committed
85
Global Instance minus : Minus (bound sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
86
  match x1, x2 with
Ralf Jung's avatar
Ralf Jung committed
87 88 89 90 91 92
  | 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
93 94
  end.

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

241
Section stsRA.
Ralf Jung's avatar
Ralf Jung committed
242
Context (sts : Sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
243

Ralf Jung's avatar
Ralf Jung committed
244 245 246 247 248
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
249

Ralf Jung's avatar
Ralf Jung committed
250 251
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
252
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
253
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
Ralf Jung's avatar
Ralf Jung committed
254
  destruct (step_closed sts s1 s2 T1 T2 S Tf) as (?&?&?); auto.
255
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
256
Qed.
Ralf Jung's avatar
Ralf Jung committed
257

Ralf Jung's avatar
Ralf Jung committed
258 259 260
Lemma sts_update_frag S1 S2 (T : set (token sts)) :
  S1  S2  closed sts S2 T 
  frag S1 T ~~> frag S2 T.
261 262 263 264 265 266
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
267 268 269 270 271
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
272
Proof.
273 274
  move=>Hcl2. split.
  - intros [xf EQ]. destruct xf as [xf vf Hvf]. destruct xf as [Sf Tf|Sf Tf].
275
    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
276
      inversion Hcl2. }
277 278 279
    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]].
280 281 282
    apply Hvf in Hclf. simpl in Hclf. clear Hvf.
    inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
    apply (anti_symm ()).
283
    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
284
      by apply sts.subseteq_up_set.
285
    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
286 287
      destruct Hscl as [s' [Hsup Hs']].
      eapply sts.closed_steps; last (hnf in Hsup; eexact Hsup); first done.
288
      solve_elem_of +HS Hs'.
Ralf Jung's avatar
Ralf Jung committed
289 290
  - intros (Hcl1 & Tf & Htk & Hf & Hs).
    exists (frag (up_set sts S2 Tf) Tf).
291 292 293
    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
294
        move=>s Hs2. move:(closed_disjoint sts _ _ Hcl2 _ Hs2).
Ralf Jung's avatar
Ralf Jung committed
295
        solve_elem_of +Htk.
296 297 298 299
      * 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
300 301 302 303
Lemma frag_included' S1 S2 T :
  closed sts S2 T  closed sts S1 T 
  S2  (S1  sts.up_set sts S2 ) 
  frag S1 T  frag S2 T.
304
Proof.
Ralf Jung's avatar
Ralf Jung committed
305
  intros. apply frag_included; first done.
306 307
  split; first done. exists . split_ands; done || solve_elem_of+.
Qed.
Ralf Jung's avatar
Ralf Jung committed
308

309
End stsRA.
Ralf Jung's avatar
Ralf Jung committed
310 311

End sts.