Library iris.algebra.sts
From iris.prelude Require Export set.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
Module sts.
Structure stsT := STS {
state : Type;
token : Type;
prim_step : relation state;
tok : state → set token;
}.
Arguments STS {_ _} _ _.
Arguments prim_step {_} _ _.
Arguments tok {_} _.
Notation states sts := (set (state sts)).
Notation tokens sts := (set (token sts)).
Structure stsT := STS {
state : Type;
token : Type;
prim_step : relation state;
tok : state → set token;
}.
Arguments STS {_ _} _ _.
Arguments prim_step {_} _ _.
Arguments tok {_} _.
Notation states sts := (set (state sts)).
Notation tokens sts := (set (token sts)).
Inductive step : relation (state sts × tokens sts) :=
| Step s1 s2 T1 T2 :
prim_step s1 s2 → tok s1 ⊥ T1 → tok s2 ⊥ T2 →
tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
Notation steps := (rtc step).
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
| Frame_step T1 T2 :
T1 ⊥ tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2.
| Step s1 s2 T1 T2 :
prim_step s1 s2 → tok s1 ⊥ T1 → tok s2 ⊥ T2 →
tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
Notation steps := (rtc step).
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
| Frame_step T1 T2 :
T1 ⊥ tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2.
Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
closed_disjoint s : s ∈ S → tok s ⊥ T;
closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
}.
Definition up (s : state sts) (T : tokens sts) : states sts :=
{[ s' | rtc (frame_step T) s s' ]}.
Definition up_set (S : states sts) (T : tokens sts) : states sts :=
S ≫= λ s, up s T.
closed_disjoint s : s ∈ S → tok s ⊥ T;
closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
}.
Definition up (s : state sts) (T : tokens sts) : states sts :=
{[ s' | rtc (frame_step T) s s' ]}.
Definition up_set (S : states sts) (T : tokens sts) : states sts :=
S ≫= λ s, up s T.
Tactic setup
Hint Resolve Step.
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.
Hint Extern 50 (_ ⊥ _) ⇒ set_solver : sts.
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.
Hint Extern 50 (_ ⊥ _) ⇒ set_solver : sts.
Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
Proof.
intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
eauto with sts; set_solver.
Qed.
Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
Proof. move⇒ ?? /collection_equiv_spec [??]; split; by apply framestep_mono. Qed.
Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.
Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
Proof.
intros s ? <- T T' HT ; apply elem_of_subseteq.
induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
eapply elem_of_mkSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
Global Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
Proof.
by move⇒ ??? ?? /collection_equiv_spec [??]; split; apply up_preserving.
Qed.
Global 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.
Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
Proof.
move⇒ S1 S2 /collection_equiv_spec [??] T1 T2 /collection_equiv_spec [??];
split; by apply up_set_preserving.
Qed.
Proof.
intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
eauto with sts; set_solver.
Qed.
Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
Proof. move⇒ ?? /collection_equiv_spec [??]; split; by apply framestep_mono. Qed.
Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.
Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
Proof.
intros s ? <- T T' HT ; apply elem_of_subseteq.
induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
eapply elem_of_mkSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
Global Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
Proof.
by move⇒ ??? ?? /collection_equiv_spec [??]; split; apply up_preserving.
Qed.
Global 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.
Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
Proof.
move⇒ S1 S2 /collection_equiv_spec [??] T1 T2 /collection_equiv_spec [??];
split; by apply up_set_preserving.
Qed.
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 :
closed S1 T1 → closed S2 T2 → closed (S1 ∩ S2) (T1 ∪ T2).
Proof.
intros [? Hstep1] [? Hstep2]; split; [set_solver|].
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.
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.
inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.
- eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
- set_solver -Hstep Hs1 Hs2.
Qed.
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 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.
Qed.
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 :
closed S1 T1 → closed S2 T2 → closed (S1 ∩ S2) (T1 ∪ T2).
Proof.
intros [? Hstep1] [? Hstep2]; split; [set_solver|].
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.
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.
inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.
- eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
- set_solver -Hstep Hs1 Hs2.
Qed.
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 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.
Qed.
Lemma elem_of_up s T : s ∈ up s T.
Proof. constructor. Qed.
Lemma subseteq_up_set S T : S ⊆ up_set S T.
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ⊥ T) → closed (up_set S T) T.
Proof.
intros HS; unfold up_set; split.
- intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
specialize (HS s' Hs'); clear Hs' S.
induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
inversion_clear Hstep; apply IH; clear IH; auto with sts.
- intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; ∃ s.
split; [eapply rtc_r|]; eauto.
Qed.
Lemma closed_up s T : tok s ⊥ T → closed (up s T) T.
Proof.
intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
apply closed_up_set; set_solver.
Qed.
Lemma closed_up_set_empty S : closed (up_set S ∅) ∅.
Proof. eauto using closed_up_set with sts. Qed.
Lemma closed_up_empty s : closed (up s ∅) ∅.
Proof. eauto using closed_up with sts. Qed.
Lemma up_set_empty S T : up_set S T ≡ ∅ → S ≡ ∅.
Proof. move:(subseteq_up_set S T). set_solver. Qed.
Lemma up_set_non_empty S T : S ≢ ∅ → up_set S T ≢ ∅.
Proof. by move=>? /up_set_empty. Qed.
Lemma up_non_empty s T : up s T ≢ ∅.
Proof. eapply non_empty_inhabited, elem_of_up. Qed.
Lemma up_closed S T : closed S T → up_set S T ≡ S.
Proof.
intros ?; apply collection_equiv_spec; split; auto using subseteq_up_set.
intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
induction Hstep; eauto using closed_step.
Qed.
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).
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 {_} _ _.
End sts.
Notation stsT := sts.stsT.
Notation STS := sts.STS.
Proof. constructor. Qed.
Lemma subseteq_up_set S T : S ⊆ up_set S T.
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ⊥ T) → closed (up_set S T) T.
Proof.
intros HS; unfold up_set; split.
- intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
specialize (HS s' Hs'); clear Hs' S.
induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
inversion_clear Hstep; apply IH; clear IH; auto with sts.
- intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; ∃ s.
split; [eapply rtc_r|]; eauto.
Qed.
Lemma closed_up s T : tok s ⊥ T → closed (up s T) T.
Proof.
intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
apply closed_up_set; set_solver.
Qed.
Lemma closed_up_set_empty S : closed (up_set S ∅) ∅.
Proof. eauto using closed_up_set with sts. Qed.
Lemma closed_up_empty s : closed (up s ∅) ∅.
Proof. eauto using closed_up with sts. Qed.
Lemma up_set_empty S T : up_set S T ≡ ∅ → S ≡ ∅.
Proof. move:(subseteq_up_set S T). set_solver. Qed.
Lemma up_set_non_empty S T : S ≢ ∅ → up_set S T ≢ ∅.
Proof. by move=>? /up_set_empty. Qed.
Lemma up_non_empty s T : up s T ≢ ∅.
Proof. eapply non_empty_inhabited, elem_of_up. Qed.
Lemma up_closed S T : closed S T → up_set S T ≡ S.
Proof.
intros ?; apply collection_equiv_spec; split; auto using subseteq_up_set.
intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
induction Hstep; eauto using closed_step.
Qed.
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).
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 {_} _ _.
End sts.
Notation stsT := sts.stsT.
Notation STS := sts.STS.
Section sts_dra.
Context (sts : stsT).
Import sts.
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,
match x with
| auth s T ⇒ tok s ⊥ T
| frag S' T ⇒ closed S' T ∧ S' ≢ ∅
end.
Instance sts_core : Core (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)
end.
Global Instance sts_step : step.Step (car sts) := λ x1 x2,
∃ s1 T1 y1 s2 T2 y2, (auth s1 T1 ⊥ y1) ∧ (x1 ≡ auth s1 T1 ⋅ y1)
∧ (auth s2 T2 ⊥ y2) ∧ (x2 ≡ auth s2 T2 ⋅ y2)
∧ (tc prim_step) s1 s2.
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.
Hint Extern 50 (_ ⊥ _) ⇒ set_solver : sts.
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)).
Proof.
split.
- by intros []; constructor.
- by destruct 1; constructor.
- destruct 1; inversion_clear 1; constructor; etrans; eauto.
Qed.
Lemma auth_disj_decomp x s1 T1 f1 s2 T2 f2:
auth s1 T1 ⊥ f1 → x ≡ auth s1 T1 ⋅ f1 → auth s2 T2 ⊥ f2 → x ≡ auth s2 T2 ⋅ f2 →
s1 = s2.
Proof.
intros Hdisj1 Heq1 Hdisj2 Heq2.
inversion Hdisj1 as [| ? ? ? Sf1 |]; subst.
inversion Hdisj2 as [| ? ? ? Sf2 |]; subst.
rewrite /op /sts_op in Heq1 Heq2.
rewrite Heq1 in Heq2 *; intro Heq_auth.
inversion Heq_auth; auto.
Qed.
Lemma sts_step_trans: Transitive (sts_step).
Proof.
intros x y z (s1 & T1 & a1 & s2 & T2 & a2 & Hdisj1 & Heqx & Hdisj2 & Heqy & Htc)
(s1' & T1' & a1' & s2' & T2' & a2' & Hdisj1' & Heqy' & Hdisj2' & Heqz & Htc').
∃ s1, T1, a1, s2', T2', a2'.
split_and?; eauto.
assert (s2 = s1') by eauto using auth_disj_decomp.
subst. eauto with ars.
Qed.
Instance sts_step_proper: Proper (equiv ==> equiv ==> impl) sts_step.
Proof.
intros x y Heq x' y' Heq' Hstep.
rewrite /step /sts_step in Hstep ×.
destruct Hstep as (s1 & T1 & y1 & s2 & T2 & y2 & Hdisj & Heqx & Hdisj' & Heqx' & Htc).
∃ s1, T1, y1, s2, T2, y2.
split_and?; rewrite -?Heq -?Heq'; eauto.
Qed.
Lemma sts_dra_mixin : DRAMixin (car sts).
Proof.
split.
- 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.
- exact sts_step_proper.
- destruct 3; simpl in *; destruct_and?; eauto using closed_op;
match goal with H : closed _ _ |- _ ⇒ destruct H end; set_solver.
- intros []; simpl; intros; destruct_conjs; split;
eauto using closed_up, up_non_empty, closed_up_set, up_set_empty with sts.
- 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.
- intros [|S T]; constructor; auto with sts.
- intros [s T|S T]; constructor; auto with sts.
+ rewrite (up_closed (up _ _)); auto using closed_up with sts.
+ rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
- intros x y. ∃ (core (x ⋅ y))=> ?? Hxy; split_and?.
+ destruct Hxy; constructor; unfold up_set; set_solver.
+ destruct Hxy; simpl; split_and?;
auto using closed_up_set_empty, closed_up_empty, up_non_empty; [].
apply up_set_non_empty. set_solver.
+ destruct Hxy; constructor;
repeat match goal with
| |- 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)
end; auto with sts.
- intros [| S T] [| S' T']; simpl.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=;
apply closed_op; rewrite ?right_id; apply closed_up; set_solver.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=.
apply closed_op; rewrite ?right_id.
× apply closed_up; set_solver.
× apply closed_up_set; set_solver.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=.
apply closed_op; rewrite ?right_id.
× apply closed_up_set; set_solver.
× apply closed_up; set_solver.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=.
apply closed_op; rewrite ?right_id.
× apply closed_up_set; set_solver.
× apply closed_up_set; set_solver.
Qed.
Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin.
End sts_dra.
Context (sts : stsT).
Import sts.
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,
match x with
| auth s T ⇒ tok s ⊥ T
| frag S' T ⇒ closed S' T ∧ S' ≢ ∅
end.
Instance sts_core : Core (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)
end.
Global Instance sts_step : step.Step (car sts) := λ x1 x2,
∃ s1 T1 y1 s2 T2 y2, (auth s1 T1 ⊥ y1) ∧ (x1 ≡ auth s1 T1 ⋅ y1)
∧ (auth s2 T2 ⊥ y2) ∧ (x2 ≡ auth s2 T2 ⋅ y2)
∧ (tc prim_step) s1 s2.
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.
Hint Extern 50 (_ ⊥ _) ⇒ set_solver : sts.
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)).
Proof.
split.
- by intros []; constructor.
- by destruct 1; constructor.
- destruct 1; inversion_clear 1; constructor; etrans; eauto.
Qed.
Lemma auth_disj_decomp x s1 T1 f1 s2 T2 f2:
auth s1 T1 ⊥ f1 → x ≡ auth s1 T1 ⋅ f1 → auth s2 T2 ⊥ f2 → x ≡ auth s2 T2 ⋅ f2 →
s1 = s2.
Proof.
intros Hdisj1 Heq1 Hdisj2 Heq2.
inversion Hdisj1 as [| ? ? ? Sf1 |]; subst.
inversion Hdisj2 as [| ? ? ? Sf2 |]; subst.
rewrite /op /sts_op in Heq1 Heq2.
rewrite Heq1 in Heq2 *; intro Heq_auth.
inversion Heq_auth; auto.
Qed.
Lemma sts_step_trans: Transitive (sts_step).
Proof.
intros x y z (s1 & T1 & a1 & s2 & T2 & a2 & Hdisj1 & Heqx & Hdisj2 & Heqy & Htc)
(s1' & T1' & a1' & s2' & T2' & a2' & Hdisj1' & Heqy' & Hdisj2' & Heqz & Htc').
∃ s1, T1, a1, s2', T2', a2'.
split_and?; eauto.
assert (s2 = s1') by eauto using auth_disj_decomp.
subst. eauto with ars.
Qed.
Instance sts_step_proper: Proper (equiv ==> equiv ==> impl) sts_step.
Proof.
intros x y Heq x' y' Heq' Hstep.
rewrite /step /sts_step in Hstep ×.
destruct Hstep as (s1 & T1 & y1 & s2 & T2 & y2 & Hdisj & Heqx & Hdisj' & Heqx' & Htc).
∃ s1, T1, y1, s2, T2, y2.
split_and?; rewrite -?Heq -?Heq'; eauto.
Qed.
Lemma sts_dra_mixin : DRAMixin (car sts).
Proof.
split.
- 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.
- exact sts_step_proper.
- destruct 3; simpl in *; destruct_and?; eauto using closed_op;
match goal with H : closed _ _ |- _ ⇒ destruct H end; set_solver.
- intros []; simpl; intros; destruct_conjs; split;
eauto using closed_up, up_non_empty, closed_up_set, up_set_empty with sts.
- 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.
- intros [|S T]; constructor; auto with sts.
- intros [s T|S T]; constructor; auto with sts.
+ rewrite (up_closed (up _ _)); auto using closed_up with sts.
+ rewrite (up_closed (up_set _ _)); eauto using closed_up_set with sts.
- intros x y. ∃ (core (x ⋅ y))=> ?? Hxy; split_and?.
+ destruct Hxy; constructor; unfold up_set; set_solver.
+ destruct Hxy; simpl; split_and?;
auto using closed_up_set_empty, closed_up_empty, up_non_empty; [].
apply up_set_non_empty. set_solver.
+ destruct Hxy; constructor;
repeat match goal with
| |- 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)
end; auto with sts.
- intros [| S T] [| S' T']; simpl.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=;
apply closed_op; rewrite ?right_id; apply closed_up; set_solver.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=.
apply closed_op; rewrite ?right_id.
× apply closed_up; set_solver.
× apply closed_up_set; set_solver.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=.
apply closed_op; rewrite ?right_id.
× apply closed_up_set; set_solver.
× apply closed_up; set_solver.
+ intros. econstructor; first set_solver+.
apply up_closed.
assert ((∅: tokens sts) ≡ ∅ ∪ ∅) as → by rewrite ?right_id //=.
apply closed_op; rewrite ?right_id.
× apply closed_up_set; set_solver.
× apply closed_up_set; set_solver.
Qed.
Canonical Structure stsDR : draT := DRAT (car sts) sts_dra_mixin.
End sts_dra.
Notation stsC sts := (validityC (stsDR sts)).
Notation stsR sts := (validityR (stsDR sts)).
Section sts_definitions.
Context {sts : stsT}.
Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
to_validity (sts.auth s T).
Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
to_validity (sts.frag S T).
Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR 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.
Arguments dra_valid _ !_/.
Notation stsR sts := (validityR (stsDR sts)).
Section sts_definitions.
Context {sts : stsT}.
Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
to_validity (sts.auth s T).
Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsR sts :=
to_validity (sts.frag S T).
Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR 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.
Arguments dra_valid _ !_/.
Setoids
Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
Proof. solve_proper. Qed.
Global Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag sts).
Proof. solve_proper. Qed.
Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
Proof. solve_proper. Qed.
Proof. solve_proper. Qed.
Global Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag sts).
Proof. solve_proper. Qed.
Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
Proof. solve_proper. Qed.
Validity
Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ⊥ T.
Proof. done. Qed.
Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ S ≢ ∅.
Proof. done. Qed.
Lemma sts_frag_up_valid s T : tok s ⊥ T → ✓ sts_frag_up s T.
Proof. intros. by apply sts_frag_valid; auto using closed_up, up_non_empty. Qed.
Lemma sts_auth_frag_valid_inv s S T1 T2 :
✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
Proof. done. Qed.
Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ S ≢ ∅.
Proof. done. Qed.
Lemma sts_frag_up_valid s T : tok s ⊥ T → ✓ sts_frag_up s T.
Proof. intros. by apply sts_frag_valid; auto using closed_up, up_non_empty. Qed.
Lemma sts_auth_frag_valid_inv s S T1 T2 :
✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.
Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
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.
intros; split; [split|constructor; set_solver]; simpl.
- intros (?&?&?); by apply closed_disjoint with S.
- intros; split_and?; last constructor; set_solver.
Qed.
Lemma sts_op_auth_frag_up s T :
sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
Proof.
intros; split; [split|constructor; set_solver]; simpl.
- intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
- intros; split_and?.
+ set_solver+.
+ by apply closed_up.
+ apply up_non_empty.
+ constructor; last set_solver. apply elem_of_up.
Qed.
Lemma sts_op_frag S1 S2 T1 T2 :
T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 →
sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
Proof.
intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.
move=>/=[??]. split_and!; [auto; set_solver..|by constructor].
Qed.
s ∈ S → closed S T → sts_auth s ∅ ⋅ sts_frag S T ≡ sts_auth s T.
Proof.
intros; split; [split|constructor; set_solver]; simpl.
- intros (?&?&?); by apply closed_disjoint with S.
- intros; split_and?; last constructor; set_solver.
Qed.
Lemma sts_op_auth_frag_up s T :
sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
Proof.
intros; split; [split|constructor; set_solver]; simpl.
- intros (?&[??]&?). by apply closed_disjoint with (up s T), elem_of_up.
- intros; split_and?.
+ set_solver+.
+ by apply closed_up.
+ apply up_non_empty.
+ constructor; last set_solver. apply elem_of_up.
Qed.
Lemma sts_op_frag S1 S2 T1 T2 :
T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 →
sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
Proof.
intros HT HS1 HS2. rewrite /sts_frag -to_validity_op //.
move=>/=[??]. split_and!; [auto; set_solver..|by constructor].
Qed.
Frame preserving updates
Lemma sts_update_auth s1 s2 T1 T2 :
steps (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
Proof.
intros ?; apply validity_update.
inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_and?.
destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
repeat (done || constructor).
Qed.
Lemma sts_update_frag S1 S2 T1 T2 :
closed S2 T2 → S1 ⊆ S2 → T2 ⊆ T1 → sts_frag S1 T1 ~~> sts_frag S2 T2.
Proof.
rewrite /sts_frag⇒ ? HS HT. apply validity_update.
inversion 3 as [|? S ? Tf|]; simplify_eq/=.
- split_and!; first done; first set_solver. constructor; set_solver.
- split_and!; first done; first set_solver. constructor; set_solver.
Qed.
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.
Proof.
intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
rewrite <-HT. eapply up_subseteq; done.
Qed.
Lemma sts_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. by apply HS1. by apply subseteq_up_set.
- move⇒s [HS1 [s' [/elem_of_mkSet Hsup Hs']]]. split; first done.
eapply closed_steps, Hsup; first done. set_solver +Hs'.
Qed.
steps (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
Proof.
intros ?; apply validity_update.
inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_and?.
destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
repeat (done || constructor).
Qed.
Lemma sts_update_frag S1 S2 T1 T2 :
closed S2 T2 → S1 ⊆ S2 → T2 ⊆ T1 → sts_frag S1 T1 ~~> sts_frag S2 T2.
Proof.
rewrite /sts_frag⇒ ? HS HT. apply validity_update.
inversion 3 as [|? S ? Tf|]; simplify_eq/=.
- split_and!; first done; first set_solver. constructor; set_solver.
- split_and!; first done; first set_solver. constructor; set_solver.
Qed.
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.
Proof.
intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
rewrite <-HT. eapply up_subseteq; done.
Qed.
Lemma sts_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. by apply HS1. by apply subseteq_up_set.
- move⇒s [HS1 [s' [/elem_of_mkSet Hsup Hs']]]. split; first done.
eapply closed_steps, Hsup; first done. set_solver +Hs'.
Qed.
Inclusion
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)).
Canonical sts_notok (sts : stsT) : sts.stsT :=
sts.STS (token:=Empty_set) (@prim_step sts) (λ _, ∅).
Section sts.
Context {sts : stsT}.
Implicit Types s : state sts.
Implicit Types S : states sts.
Notation prim_steps := (rtc prim_step).
Lemma sts_step s1 s2 :
prim_step s1 s2 → sts.step (s1, ∅) (s2, ∅).
Proof.
intros. split; set_solver.
Qed.
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.
Lemma frame_prim_step T s1 s2 :
sts.frame_step T s1 s2 → prim_step s1 s2.
Proof.
inversion 1 as [??? Hstep]. inversion_clear Hstep. done.
Qed.
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.
Lemma mk_closed S :
(∀ s1 s2, s1 ∈ S → prim_step s1 s2 → s2 ∈ S) → sts.closed S ∅.
Proof.
intros ?. constructor; first by set_solver.
intros ????. eauto using frame_prim_step.
Qed.
End sts.
Notation steps := (rtc prim_step).
End sts_notok.
Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.
Notation sts_notokT := sts_notok.stsT.
Notation STS_NoTok := sts_notok.STS.
Section sts_notokRA.
Import sts_notok.
Context {sts : sts_notokT}.
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.
End sts_notokRA.
Structure stsT := STS {
state : Type;
prim_step : relation state;
}.
Arguments STS {_} _.
Arguments prim_step {_} _ _.
Notation states sts := (set (state sts)).
Canonical sts_notok (sts : stsT) : sts.stsT :=
sts.STS (token:=Empty_set) (@prim_step sts) (λ _, ∅).
Section sts.
Context {sts : stsT}.
Implicit Types s : state sts.
Implicit Types S : states sts.
Notation prim_steps := (rtc prim_step).
Lemma sts_step s1 s2 :
prim_step s1 s2 → sts.step (s1, ∅) (s2, ∅).
Proof.
intros. split; set_solver.
Qed.
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.
Lemma frame_prim_step T s1 s2 :
sts.frame_step T s1 s2 → prim_step s1 s2.
Proof.
inversion 1 as [??? Hstep]. inversion_clear Hstep. done.
Qed.
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.
Lemma mk_closed S :
(∀ s1 s2, s1 ∈ S → prim_step s1 s2 → s2 ∈ S) → sts.closed S ∅.
Proof.
intros ?. constructor; first by set_solver.
intros ????. eauto using frame_prim_step.
Qed.
End sts.
Notation steps := (rtc prim_step).
End sts_notok.
Coercion sts_notok.sts_notok : sts_notok.stsT >-> sts.stsT.
Notation sts_notokT := sts_notok.stsT.
Notation STS_NoTok := sts_notok.STS.
Section sts_notokRA.
Import sts_notok.
Context {sts : sts_notokT}.
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.
End sts_notokRA.