sts.v 18.1 KB
 Robbert Krebbers committed Jul 22, 2016 1 From iris.prelude Require Export set.  Robbert Krebbers committed Mar 10, 2016 2 3 From iris.algebra Require Export cmra. From iris.algebra Require Import dra.  Robbert Krebbers committed Nov 11, 2015 4 5 Local Arguments valid _ _ !_ /. Local Arguments op _ _ !_ !_ /.  Ralf Jung committed Mar 08, 2016 6 Local Arguments core _ _ !_ /.  Robbert Krebbers committed Nov 11, 2015 7   Robbert Krebbers committed Feb 16, 2016 8 (** * Definition of STSs *)  Robbert Krebbers committed Feb 01, 2016 9 Module sts.  Ralf Jung committed Feb 23, 2016 10 Structure stsT := STS {  Ralf Jung committed Feb 15, 2016 11 12  state : Type; token : Type;  Robbert Krebbers committed Feb 16, 2016 13 14  prim_step : relation state; tok : state → set token;  Ralf Jung committed Feb 15, 2016 15 }.  Ralf Jung committed Feb 16, 2016 16 Arguments STS {_ _} _ _.  Robbert Krebbers committed Feb 16, 2016 17 18 19 20 Arguments prim_step {_} _ _. Arguments tok {_} _. Notation states sts := (set (state sts)). Notation tokens sts := (set (token sts)).  Ralf Jung committed Feb 15, 2016 21   Robbert Krebbers committed Feb 16, 2016 22 23 24 (** * Theory and definitions *) Section sts. Context {sts : stsT}.  Ralf Jung committed Feb 15, 2016 25   Robbert Krebbers committed Feb 16, 2016 26 27 (** ** Step relations *) Inductive step : relation (state sts * tokens sts) :=  Robbert Krebbers committed Nov 11, 2015 28  | Step s1 s2 T1 T2 :  Robbert Krebbers committed Mar 23, 2016 29  prim_step s1 s2 → tok s1 ⊥ T1 → tok s2 ⊥ T2 →  Ralf Jung committed Feb 15, 2016 30  tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).  Robbert Krebbers committed Feb 22, 2016 31 Notation steps := (rtc step).  Robbert Krebbers committed Feb 16, 2016 32 Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=  Ralf Jung committed Aug 16, 2016 33  (* Probably equivalent definition: (\mathcal{L}(s') ⊥ T) ∧ s \rightarrow s' *)  Robbert Krebbers committed Nov 11, 2015 34  | Frame_step T1 T2 :  Robbert Krebbers committed Mar 23, 2016 35  T1 ⊥ tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2.  Ralf Jung committed Aug 09, 2016 36 Notation frame_steps T := (rtc (frame_step T)).  Robbert Krebbers committed Feb 16, 2016 37 38 39  (** ** Closure under frame steps *) Record closed (S : states sts) (T : tokens sts) : Prop := Closed {  Robbert Krebbers committed Mar 23, 2016 40  closed_disjoint s : s ∈ S → tok s ⊥ T;  Robbert Krebbers committed Nov 11, 2015 41 42  closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S }.  Robbert Krebbers committed Feb 16, 2016 43 Definition up (s : state sts) (T : tokens sts) : states sts :=  Ralf Jung committed Aug 09, 2016 44  {[ s' | frame_steps T s s' ]}.  Robbert Krebbers committed Feb 16, 2016 45 Definition up_set (S : states sts) (T : tokens sts) : states sts :=  Robbert Krebbers committed Feb 16, 2016 46  S ≫= λ s, up s T.  Robbert Krebbers committed Nov 11, 2015 47   Robbert Krebbers committed Feb 16, 2016 48 49 (** Tactic setup *) Hint Resolve Step.  50 51 52 53 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 committed Mar 23, 2016 54 Hint Extern 50 (_ ⊥ _) => set_solver : sts.  Robbert Krebbers committed Feb 16, 2016 55 56  (** ** Setoids *)  Ralf Jung committed Feb 17, 2016 57 58 59 Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step. Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor;  Robbert Krebbers committed Feb 17, 2016 60  eauto with sts; set_solver.  Ralf Jung committed Feb 17, 2016 61 Qed.  Robbert Krebbers committed Feb 16, 2016 62 Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.  Robbert Krebbers committed Jul 22, 2016 63 Proof. move=> ?? /collection_equiv_spec [??]; split; by apply framestep_mono. Qed.  Robbert Krebbers committed Nov 16, 2015 64 Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.  Robbert Krebbers committed Mar 23, 2016 65 Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.  Robbert Krebbers committed Feb 16, 2016 66 Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.  Robbert Krebbers committed Nov 16, 2015 67 Proof. by split; apply closed_proper'. Qed.  Robbert Krebbers committed Feb 16, 2016 68 Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.  Robbert Krebbers committed Nov 11, 2015 69 Proof.  70  intros s ? <- T T' HT ; apply elem_of_subseteq.  Robbert Krebbers committed Nov 11, 2015 71  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].  Robbert Krebbers committed Feb 24, 2016 72  eapply elem_of_mkSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.  Robbert Krebbers committed Nov 11, 2015 73 Qed.  Robbert Krebbers committed Feb 16, 2016 74 Global Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.  Robbert Krebbers committed Jul 22, 2016 75 76 77 Proof. by move=> ??? ?? /collection_equiv_spec [??]; split; apply up_preserving. Qed.  Robbert Krebbers committed Feb 16, 2016 78 Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.  Ralf Jung committed Feb 15, 2016 79 80 Proof. intros S1 S2 HS T1 T2 HT. rewrite /up_set.  Robbert Krebbers committed Dec 05, 2016 81  f_equiv=> // s1 s2 Hs. by apply up_preserving.  Ralf Jung committed Feb 15, 2016 82 Qed.  Robbert Krebbers committed Feb 16, 2016 83 Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.  Robbert Krebbers committed Jul 22, 2016 84 85 86 87 Proof. move=> S1 S2 /collection_equiv_spec [??] T1 T2 /collection_equiv_spec [??]; split; by apply up_set_preserving. Qed.  Robbert Krebbers committed Feb 16, 2016 88 89 90  (** ** Properties of closure under frame steps *) Lemma closed_steps S T s1 s2 :  Ralf Jung committed Aug 09, 2016 91  closed S T → s1 ∈ S → frame_steps T s1 s2 → s2 ∈ S.  Robbert Krebbers committed Feb 16, 2016 92 93 Proof. induction 3; eauto using closed_step. Qed. Lemma closed_op T1 T2 S1 S2 :  94  closed S1 T1 → closed S2 T2 → closed (S1 ∩ S2) (T1 ∪ T2).  Robbert Krebbers committed Feb 16, 2016 95 Proof.  96  intros [? Hstep1] [? Hstep2]; split; [set_solver|].  Robbert Krebbers committed Feb 16, 2016 97  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.  Robbert Krebbers committed Feb 17, 2016 98 99  - 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 committed Feb 16, 2016 100 101 Qed. Lemma step_closed s1 s2 T1 T2 S Tf :  Robbert Krebbers committed Mar 23, 2016 102 103  step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ⊥ Tf → s2 ∈ S ∧ T2 ⊥ Tf ∧ tok s2 ⊥ T2.  Robbert Krebbers committed Feb 16, 2016 104 Proof.  105  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.  Robbert Krebbers committed Feb 17, 2016 106  - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.  Robbert Krebbers committed Feb 17, 2016 107  - set_solver -Hstep Hs1 Hs2.  Robbert Krebbers committed Feb 16, 2016 108 Qed.  Ralf Jung committed Feb 20, 2016 109 Lemma steps_closed s1 s2 T1 T2 S Tf :  Robbert Krebbers committed Mar 23, 2016 110 111  steps (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ⊥ Tf → tok s1 ⊥ T1 → s2 ∈ S ∧ T2 ⊥ Tf ∧ tok s2 ⊥ T2.  Ralf Jung committed Feb 20, 2016 112 Proof.  Robbert Krebbers committed Feb 22, 2016 113 114 115 116 117  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.  Ralf Jung committed Feb 20, 2016 118 Qed.  Robbert Krebbers committed Feb 16, 2016 119 120  (** ** Properties of the closure operators *)  121 Lemma elem_of_up s T : s ∈ up s T.  Robbert Krebbers committed Nov 11, 2015 122 Proof. constructor. Qed.  123 Lemma subseteq_up_set S T : S ⊆ up_set S T.  Robbert Krebbers committed Nov 11, 2015 124 Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.  Janno committed Oct 10, 2016 125 126 Lemma elem_of_up_set S T s : s ∈ S → s ∈ up_set S T. Proof. apply subseteq_up_set. Qed.  Ralf Jung committed Feb 15, 2016 127 128 Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T. Proof. by rewrite /up_set collection_bind_singleton. Qed.  Robbert Krebbers committed Mar 23, 2016 129 Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ⊥ T) → closed (up_set S T) T.  Robbert Krebbers committed Nov 11, 2015 130 Proof.  131  intros HS; unfold up_set; split.  Robbert Krebbers committed Feb 17, 2016 132  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').  133  specialize (HS s' Hs'); clear Hs' S.  Ralf Jung committed Feb 16, 2016 134  induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.  Robbert Krebbers committed Nov 11, 2015 135  inversion_clear Hstep; apply IH; clear IH; auto with sts.  Robbert Krebbers committed Feb 24, 2016 136  - intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; exists s.  Robbert Krebbers committed Nov 11, 2015 137 138  split; [eapply rtc_r|]; eauto. Qed.  Robbert Krebbers committed Mar 23, 2016 139 Lemma closed_up s T : tok s ⊥ T → closed (up s T) T.  Robbert Krebbers committed Nov 11, 2015 140 Proof.  141  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).  Robbert Krebbers committed Feb 17, 2016 142  apply closed_up_set; set_solver.  Robbert Krebbers committed Nov 11, 2015 143 Qed.  144 145 Lemma closed_up_set_empty S : closed (up_set S ∅) ∅. Proof. eauto using closed_up_set with sts. Qed.  146 Lemma closed_up_empty s : closed (up s ∅) ∅.  Robbert Krebbers committed Nov 11, 2015 147 Proof. eauto using closed_up with sts. Qed.  148 Lemma up_closed S T : closed S T → up_set S T ≡ S.  Robbert Krebbers committed Nov 11, 2015 149 Proof.  Robbert Krebbers committed Jul 22, 2016 150 151  intros ?; apply collection_equiv_spec; split; auto using subseteq_up_set. intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).  Robbert Krebbers committed Nov 11, 2015 152 153  induction Hstep; eauto using closed_step. Qed.  Robbert Krebbers committed Feb 22, 2016 154 155 156 157 158 159 160 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).  Ralf Jung committed Aug 09, 2016 161 Notation frame_steps T := (rtc (frame_step T)).  Robbert Krebbers committed Feb 16, 2016 162 163 164 165 166 167 168 169  (* 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 {_} _ _.  Robbert Krebbers committed May 25, 2016 170 End sts.  Robbert Krebbers committed Feb 16, 2016 171   Robbert Krebbers committed May 25, 2016 172 173 174 175 Notation stsT := sts.stsT. Notation STS := sts.STS. (** * STSs form a disjoint RA *)  Robbert Krebbers committed Feb 16, 2016 176 Section sts_dra.  Robbert Krebbers committed May 25, 2016 177 178 Context (sts : stsT). Import sts.  Robbert Krebbers committed Feb 16, 2016 179 180 181 182 183 184 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.  Robbert Krebbers committed May 25, 2016 185 186 Existing Instance sts_equiv. Instance sts_valid : Valid (car sts) := λ x,  187  match x with  Robbert Krebbers committed Mar 23, 2016 188  | auth s T => tok s ⊥ T  Janno committed Oct 10, 2016 189  | frag S' T => closed S' T ∧ ∃ s, s ∈ S'  Robbert Krebbers committed Feb 22, 2016 190  end.  Robbert Krebbers committed May 25, 2016 191 Instance sts_core : Core (car sts) := λ x,  Robbert Krebbers committed Feb 16, 2016 192 193 194 195 196 197  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 :  Janno committed Oct 10, 2016 198  (∃ s, s ∈ S1 ∩ S2) → T1 ⊥ T2 → frag S1 T1 ⊥ frag S2 T2  Robbert Krebbers committed Mar 23, 2016 199 200  | 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.  Robbert Krebbers committed May 25, 2016 201 202 Existing Instance sts_disjoint. Instance sts_op : Op (car sts) := λ x1 x2,  Robbert Krebbers committed Feb 16, 2016 203 204 205 206 207 208 209  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.  Robbert Krebbers committed Feb 22, 2016 210 Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.  Janno committed Oct 10, 2016 211 Hint Extern 50 (∃ s : state sts, _) => set_solver : sts.  Robbert Krebbers committed Feb 22, 2016 212 213 Hint Extern 50 (_ ∈ _) => set_solver : sts. Hint Extern 50 (_ ⊆ _) => set_solver : sts.  Robbert Krebbers committed Mar 23, 2016 214 215 Hint Extern 50 (_ ⊥ _) => set_solver : sts.  Robbert Krebbers committed May 25, 2016 216 217 218 219 220 221 Global Instance auth_proper s : Proper ((≡) ==> (≡)) (@auth sts s). Proof. by constructor. Qed. Global Instance frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@frag sts). Proof. by constructor. Qed. Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).  Robbert Krebbers committed Feb 16, 2016 222 223 Proof. split.  Robbert Krebbers committed Feb 17, 2016 224 225  - by intros []; constructor. - by destruct 1; constructor.  Ralf Jung committed Feb 20, 2016 226  - destruct 1; inversion_clear 1; constructor; etrans; eauto.  Robbert Krebbers committed Feb 16, 2016 227 Qed.  Robbert Krebbers committed May 25, 2016 228 Lemma sts_dra_mixin : DRAMixin (car sts).  Robbert Krebbers committed Nov 11, 2015 229 230 Proof. split.  Robbert Krebbers committed Feb 17, 2016 231 232 233 234  - apply _. - by do 2 destruct 1; constructor; setoid_subst. - by destruct 1; constructor; setoid_subst. - by destruct 1; simpl; intros ?; setoid_subst.  Janno committed Oct 10, 2016 235  - by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.  Robbert Krebbers committed Mar 03, 2016 236  - destruct 3; simpl in *; destruct_and?; eauto using closed_op;  Robbert Krebbers committed Feb 22, 2016 237  match goal with H : closed _ _ |- _ => destruct H end; set_solver.  Janno committed Oct 10, 2016 238 239  - intros []; naive_solver eauto using closed_up, closed_up_set, elem_of_up, elem_of_up_set with sts.  Robbert Krebbers committed Feb 17, 2016 240 241 242 243 244  - 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.  Janno committed Oct 10, 2016 245 246  - intros []; constructor; eauto with sts. - intros []; constructor; auto with sts.  Robbert Krebbers committed Feb 17, 2016 247  - intros [s T|S T]; constructor; auto with sts.  Robbert Krebbers committed Jan 13, 2016 248  + rewrite (up_closed (up _ _)); auto using closed_up with sts.  Robbert Krebbers committed Feb 24, 2016 249  + rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.  Robbert Krebbers committed Mar 11, 2016 250 251  - intros x y. exists (core (x ⋅ y))=> ?? Hxy; split_and?. + destruct Hxy; constructor; unfold up_set; set_solver.  Janno committed Oct 10, 2016 252 253 254  + destruct Hxy; simpl; eauto using closed_up_set_empty, closed_up_empty with sts. + destruct Hxy; econstructor;  Robbert Krebbers committed Dec 08, 2015 255  repeat match goal with  256 257 258 259  | |- 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)  Robbert Krebbers committed Dec 08, 2015 260  end; auto with sts.  Robbert Krebbers committed Feb 22, 2016 261 Qed.  Robbert Krebbers committed May 25, 2016 262 263 Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin. End sts_dra.  Robbert Krebbers committed Feb 16, 2016 264 265 266  (** * The STS Resource Algebra *) (** Finally, the general theory of STS that should be used by users *)  Robbert Krebbers committed May 25, 2016 267 268 Notation stsC sts := (validityC (stsDR sts)). Notation stsR sts := (validityR (stsDR sts)).  Robbert Krebbers committed Feb 16, 2016 269 270 271  Section sts_definitions. Context {sts : stsT}.  Robbert Krebbers committed Mar 01, 2016 272  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=  Robbert Krebbers committed May 25, 2016 273  to_validity (sts.auth s T).  Robbert Krebbers committed Mar 01, 2016 274  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=  Robbert Krebbers committed May 25, 2016 275  to_validity (sts.frag S T).  Robbert Krebbers committed Mar 01, 2016 276  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=  Robbert Krebbers committed Feb 16, 2016 277 278 279 280 281 282 283 284 285 286 287 288  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.  Robbert Krebbers committed May 25, 2016 289 Arguments dra_valid _ !_/.  Robbert Krebbers committed Feb 24, 2016 290   Robbert Krebbers committed Feb 16, 2016 291 292 (** Setoids *) Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).  Robbert Krebbers committed May 25, 2016 293 Proof. solve_proper. Qed.  Robbert Krebbers committed Feb 16, 2016 294 Global Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag sts).  Robbert Krebbers committed May 25, 2016 295 Proof. solve_proper. Qed.  Robbert Krebbers committed Feb 16, 2016 296 Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).  Robbert Krebbers committed May 25, 2016 297 Proof. solve_proper. Qed.  Robbert Krebbers committed Nov 11, 2015 298   Robbert Krebbers committed Feb 16, 2016 299 (** Validity *)  Robbert Krebbers committed Mar 23, 2016 300 Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ⊥ T.  Robbert Krebbers committed Feb 24, 2016 301 Proof. done. Qed.  Janno committed Oct 10, 2016 302 Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ ∃ s, s ∈ S.  Robbert Krebbers committed Feb 24, 2016 303 Proof. done. Qed.  Robbert Krebbers committed Mar 23, 2016 304 Lemma sts_frag_up_valid s T : tok s ⊥ T → ✓ sts_frag_up s T.  Janno committed Oct 10, 2016 305 Proof. intros. apply sts_frag_valid; split. by apply closed_up. set_solver. Qed.  Robbert Krebbers committed Nov 11, 2015 306   Robbert Krebbers committed Feb 16, 2016 307 308 Lemma sts_auth_frag_valid_inv s S T1 T2 : ✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.  Robbert Krebbers committed Feb 24, 2016 309 Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.  Ralf Jung committed Feb 15, 2016 310   Robbert Krebbers committed Feb 16, 2016 311 312 313 314 (** 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.  Robbert Krebbers committed Feb 17, 2016 315  intros; split; [split|constructor; set_solver]; simpl.  316  - intros (?&?&?); by apply closed_disjoint with S.  Robbert Krebbers committed Feb 24, 2016 317  - intros; split_and?; last constructor; set_solver.  Robbert Krebbers committed Feb 16, 2016 318 319 Qed. Lemma sts_op_auth_frag_up s T :  Ralf Jung committed Feb 20, 2016 320 321 322  sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T. Proof. intros; split; [split|constructor; set_solver]; simpl.  Robbert Krebbers committed Feb 24, 2016 323  - intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.  Ralf Jung committed Feb 20, 2016 324 325 326  - intros; split_and?. + set_solver+. + by apply closed_up.  Janno committed Oct 10, 2016 327  + exists s. set_solver.  Ralf Jung committed Feb 20, 2016 328 329  + constructor; last set_solver. apply elem_of_up. Qed.  Robbert Krebbers committed Feb 16, 2016 330   Ralf Jung committed Feb 17, 2016 331 Lemma sts_op_frag S1 S2 T1 T2 :  Robbert Krebbers committed Mar 23, 2016 332  T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 →  Ralf Jung committed Feb 17, 2016 333 334  sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2. Proof.  Robbert Krebbers committed May 25, 2016 335  intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.  Janno committed Oct 10, 2016 336  move=>/=[?[? ?]]. split_and!; [set_solver..|constructor; set_solver].  Ralf Jung committed Feb 17, 2016 337 338 Qed.  Robbert Krebbers committed Feb 16, 2016 339 340 (** Frame preserving updates *) Lemma sts_update_auth s1 s2 T1 T2 :  Ralf Jung committed Feb 20, 2016 341  steps (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.  Robbert Krebbers committed Nov 11, 2015 342 Proof.  Robbert Krebbers committed Feb 22, 2016 343  intros ?; apply validity_update.  Robbert Krebbers committed Mar 03, 2016 344  inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_and?.  Ralf Jung committed Feb 20, 2016 345  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].  Robbert Krebbers committed Nov 16, 2015 346  repeat (done || constructor).  Robbert Krebbers committed Nov 11, 2015 347 Qed.  Ralf Jung committed Feb 15, 2016 348   349 350 Lemma sts_update_frag S1 S2 T1 T2 : closed S2 T2 → S1 ⊆ S2 → T2 ⊆ T1 → sts_frag S1 T1 ~~> sts_frag S2 T2.  Ralf Jung committed Feb 15, 2016 351 Proof.  352  rewrite /sts_frag=> ? HS HT. apply validity_update.  Robbert Krebbers committed Feb 17, 2016 353  inversion 3 as [|? S ? Tf|]; simplify_eq/=.  Janno committed Oct 10, 2016 354 355  - split_and!. done. set_solver. constructor; set_solver. - split_and!. done. set_solver. constructor; set_solver.  Ralf Jung committed Feb 15, 2016 356 357 Qed.  358 359 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 committed Feb 15, 2016 360 Proof.  361 362  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..]. rewrite <-HT. eapply up_subseteq; done.  Robbert Krebbers committed Feb 16, 2016 363 364 Qed.  Robbert Krebbers committed May 25, 2016 365 366 Lemma sts_up_set_intersection S1 Sf Tf : closed Sf Tf → S1 ∩ Sf ≡ S1 ∩ up_set (S1 ∩ Sf) Tf.  Ralf Jung committed Feb 21, 2016 367 368 Proof. intros Hclf. apply (anti_symm (⊆)).  Robbert Krebbers committed Jul 22, 2016 369 370  - 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.  Robbert Krebbers committed Feb 24, 2016 371  eapply closed_steps, Hsup; first done. set_solver +Hs'.  Ralf Jung committed Feb 21, 2016 372 373 Qed.  Janno committed Oct 10, 2016 374 375 376 377 378 Global Instance sts_frag_peristent S : Persistent (sts_frag S ∅). Proof. constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed. Qed.  Robbert Krebbers committed Feb 16, 2016 379 (** Inclusion *)  Ralf Jung committed Feb 21, 2016 380 381 382 (* 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. *)  Ralf Jung committed Mar 11, 2016 383 (* TODO: These have to be proven again. *)  Robbert Krebbers committed Mar 11, 2016 384 (*  Robbert Krebbers committed Feb 16, 2016 385 Lemma sts_frag_included S1 S2 T1 T2 :  Ralf Jung committed Feb 21, 2016 386 387  closed S2 T2 → S2 ≢ ∅ → (sts_frag S1 T1 ≼ sts_frag S2 T2) ↔  Robbert Krebbers committed Mar 23, 2016 388  (closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ⊥ Tf ∧  Ralf Jung committed Feb 21, 2016 389 390  S2 ≡ S1 ∩ up_set S2 Tf). Proof.  Robbert Krebbers committed Mar 11, 2016 391  intros ??; split.  Robbert Krebbers committed Mar 11, 2016 392  - intros [[???] ?].  Ralf Jung committed Feb 21, 2016 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409  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 committed Feb 22, 2016 410  * by apply up_set_non_empty.  Ralf Jung committed Feb 21, 2016 411  + constructor; last done. by rewrite -HS.  412 413 Qed.  Robbert Krebbers committed Feb 16, 2016 414 Lemma sts_frag_included' S1 S2 T :  Ralf Jung committed Feb 21, 2016 415  closed S2 T → closed S1 T → S2 ≢ ∅ → S1 ≢ ∅ → S2 ≡ S1 ∩ up_set S2 ∅ →  Robbert Krebbers committed Feb 16, 2016 416  sts_frag S1 T ≼ sts_frag S2 T.  417 Proof.  Robbert Krebbers committed Feb 19, 2016 418 419  intros. apply sts_frag_included; split_and?; auto. exists ∅; split_and?; done || set_solver+.  Robbert Krebbers committed Mar 11, 2016 420 Qed. *)  Robbert Krebbers committed Feb 01, 2016 421 End stsRA.  Ralf Jung committed Mar 07, 2016 422 423 424 425 426 427 428 429 430 431 432  (** 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)).  Robbert Krebbers committed Nov 17, 2016 433 434 Definition stsT_token := Empty_set. Definition stsT_tok {sts : stsT} (_ : state sts) : set stsT_token := ∅.  Ralf Jung committed Mar 07, 2016 435   Robbert Krebbers committed Nov 17, 2016 436 437 438 Canonical Structure sts_notok (sts : stsT) : sts.stsT := sts.STS (@prim_step sts) stsT_tok. Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.  Ralf Jung committed Mar 07, 2016 439   Robbert Krebbers committed Nov 17, 2016 440 441 442 443 Section sts. Context {sts : stsT}. Implicit Types s : state sts. Implicit Types S : states sts.  Ralf Jung committed Mar 07, 2016 444   Robbert Krebbers committed Nov 17, 2016 445  Notation prim_steps := (rtc prim_step).  Ralf Jung committed Mar 07, 2016 446   Robbert Krebbers committed Nov 17, 2016 447 448  Lemma sts_step s1 s2 : prim_step s1 s2 → sts.step (s1, ∅) (s2, ∅). Proof. intros. split; set_solver. Qed.  Ralf Jung committed Mar 07, 2016 449   Robbert Krebbers committed Nov 17, 2016 450 451  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.  Ralf Jung committed Mar 07, 2016 452   Robbert Krebbers committed Nov 17, 2016 453 454  Lemma frame_prim_step T s1 s2 : sts.frame_step T s1 s2 → prim_step s1 s2. Proof. inversion 1 as [??? Hstep]. by inversion_clear Hstep. Qed.  Ralf Jung committed Mar 07, 2016 455   Robbert Krebbers committed Nov 17, 2016 456 457 458 459 460  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.  Ralf Jung committed Mar 07, 2016 461   Robbert Krebbers committed Nov 17, 2016 462 463 464  Lemma mk_closed S : (∀ s1 s2, s1 ∈ S → prim_step s1 s2 → s2 ∈ S) → sts.closed S ∅. Proof. intros ?. constructor; [by set_solver|eauto using frame_prim_step]. Qed.  Ralf Jung committed Mar 07, 2016 465 466 467 468 469 470 471 End sts. End sts_notok. Notation sts_notokT := sts_notok.stsT. Notation STS_NoTok := sts_notok.STS. Section sts_notokRA.  Robbert Krebbers committed Nov 17, 2016 472 473 474 475 476 477 478 479  Context {sts : sts_notokT}. Import sts_notok. 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.  Ralf Jung committed Mar 07, 2016 480 End sts_notokRA.