Merge branch 'ralf/sts' into 'master'

remove DRA layer, implement STS directly as an RA

Closes #378

See merge request iris/iris!693

_CoqProject

@@ -28,7 +28,6 @@ iris/algebra/view.v
 iris/algebra/auth.v
 iris/algebra/gmap.v
 iris/algebra/ofe.v
-iris/algebra/dra.v
 iris/algebra/cofe_solver.v
 iris/algebra/agree.v
 iris/algebra/excl.v

iris/algebra/dra.v

-From iris.algebra Require Export cmra updates.
-From iris.prelude Require Import options.
-
-Record DraMixin A `{Equiv A, PCore A, Disjoint A, Op A, Valid A} := {
-  (* setoids *)
-  mixin_dra_equivalence : Equivalence (≡@{A});
-  mixin_dra_op_proper : Proper ((≡@{A}) ==> (≡) ==> (≡)) (⋅);
-  mixin_dra_core_proper : Proper ((≡@{A}) ==> (≡)) core;
-  mixin_dra_valid_proper : Proper ((≡@{A}) ==> impl) valid;
-  mixin_dra_disjoint_proper (x : A) : Proper ((≡) ==> impl) (disjoint x);
-  (* validity *)
-  mixin_dra_op_valid (x y : A) : ✓ x → ✓ y → x ## y → ✓ (x ⋅ y);
-  mixin_dra_core_valid (x : A) : ✓ x → ✓ core x;
-  (* monoid *)
-  mixin_dra_assoc (x y z : A) :
-    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z;
-  mixin_dra_disjoint_ll (x y z :  A) :
-    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## z;
-  mixin_dra_disjoint_move_l (x y z : A) :
-    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## y ⋅ z;
-  mixin_dra_symmetric : Symmetric (@disjoint A _);
-  mixin_dra_comm (x y : A) : ✓ x → ✓ y → x ## y → x ⋅ y ≡ y ⋅ x;
-  mixin_dra_core_disjoint_l (x : A) : ✓ x → core x ## x;
-  mixin_dra_core_l (x : A) : ✓ x → core x ⋅ x ≡ x;
-  mixin_dra_core_idemp (x : A) : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_mono (x y : A) :
-    ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z
-}.
-Structure draT := DraT {
-  dra_car :> Type;
-  dra_equiv : Equiv dra_car;
-  dra_pcore : PCore dra_car;
-  dra_disjoint : Disjoint dra_car;
-  dra_op : Op dra_car;
-  dra_valid : Valid dra_car;
-  dra_mixin : DraMixin dra_car
-}.
-Global Arguments DraT _ {_ _ _ _ _} _.
-Global Arguments dra_car : simpl never.
-Global Arguments dra_equiv : simpl never.
-Global Arguments dra_pcore : simpl never.
-Global Arguments dra_disjoint : simpl never.
-Global Arguments dra_op : simpl never.
-Global Arguments dra_valid : simpl never.
-Global Arguments dra_mixin : simpl never.
-Add Printing Constructor draT.
-(* FIXME: Should some of these be [Global]? *)
-Local Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
-
-(** Lifting properties from the mixin *)
-Section dra_mixin.
-  Context {A : draT}.
-  Implicit Types x y : A.
-  Global Instance dra_equivalence : Equivalence ((≡) : relation A).
-  Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
-  Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
-  Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
-  Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _).
-  Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x).
-  Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
-  Lemma dra_op_valid x y : ✓ x → ✓ y → x ## y → ✓ (x ⋅ y).
-  Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
-  Lemma dra_core_valid x : ✓ x → ✓ core x.
-  Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
-  Lemma dra_assoc x y z :
-    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z.
-  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
-  Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## z.
-  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
-  Lemma dra_disjoint_move_l x y z :
-    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## y ⋅ z.
-  Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
-  Global Instance  dra_symmetric : Symmetric (@disjoint A _).
-  Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
-  Lemma dra_comm x y : ✓ x → ✓ y → x ## y → x ⋅ y ≡ y ⋅ x.
-  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
-  Lemma dra_core_disjoint_l x : ✓ x → core x ## x.
-  Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
-  Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x.
-  Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
-  Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
-  Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_mono x y :
-    ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z.
-  Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
-End dra_mixin.
-
-Record validity (A : draT) := Validity {
-  validity_car : A;
-  validity_is_valid : Prop;
-  validity_prf : validity_is_valid → valid validity_car
-}.
-Add Printing Constructor validity.
-Global Arguments Validity {_} _ _ _.
-Global Arguments validity_car {_} _.
-Global Arguments validity_is_valid {_} _.
-
-Definition to_validity {A : draT} (x : A) : validity A :=
-  Validity x (valid x) id.
-
-(* The actual construction *)
-Section dra.
-Context (A : draT).
-Implicit Types a b : A.
-Implicit Types x y z : validity A.
-Local Arguments valid _ _ !_ /.
-
-Local Instance validity_valid_instance : Valid (validity A) := validity_is_valid.
-Local Instance validity_equiv : Equiv (validity A) := λ x y,
-  (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
-Local Instance validity_equivalence : Equivalence (@equiv (validity A) _).
-Proof.
-  split; unfold equiv, validity_equiv.
-  - by intros [x px ?]; simpl.
-  - intros [x px ?] [y py ?]; naive_solver.
-  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
-    split; [|intros; trans y]; tauto.
-Qed.
-Canonical Structure validityO : ofe := discreteO (validity A).
-
-Local Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
-Proof. by split; apply: dra_valid_proper. Qed.
-Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
-Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
-Local Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
-Proof.
-  intros x1 x2 Hx y1 y2 Hy; split.
-  - by rewrite Hy (symmetry_iff (##) x1) (symmetry_iff (##) x2) Hx.
-  - by rewrite -Hy (symmetry_iff (##) x2) (symmetry_iff (##) x1) -Hx.
-Qed.
-
-Lemma dra_disjoint_rl a b c : ✓ a → ✓ b → ✓ c → b ## c → a ## b ⋅ c → a ## b.
-Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ## b → a ⋅ b ## c → b ## c.
-Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_move_r a b c :
-  ✓ a → ✓ b → ✓ c → b ## c → a ## b ⋅ c → a ⋅ b ## c.
-Proof.
-  intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
-  apply dra_disjoint_move_l; auto; by rewrite dra_comm.
-Qed.
-Local Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
-
-Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
-Proof. apply validity_prf. Qed.
-Local Hint Resolve validity_valid_car_valid : core.
-Local Program Instance validity_pcore_instance : PCore (validity A) := λ x,
-  Some (Validity (core (validity_car x)) (✓ x) _).
-Solve Obligations with naive_solver eauto using dra_core_valid.
-Local Program Instance validity_op_instance : Op (validity A) := λ x y,
-  Validity (validity_car x ⋅ validity_car y)
-           (✓ x ∧ ✓ y ∧ validity_car x ## validity_car y) _.
-Solve Obligations with naive_solver eauto using dra_op_valid.
-
-Definition validity_ra_mixin : RAMixin (validity A).
-Proof.
-  apply ra_total_mixin; first eauto.
-  - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
-    split; intros (?&?&?); split_and!;
-      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
-  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
-  - intros ?? [??]; naive_solver.
-  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
-      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |intuition eauto using dra_assoc, dra_disjoint_rl].
-  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
-  - intros [x px ?]; split;
-      naive_solver eauto using dra_core_l, dra_core_disjoint_l.
-  - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
-  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
-    destruct (dra_core_mono x z) as (z'&Hz').
-    unshelve eexists (Validity z' (px ∧ py ∧ pz) _).
-    { intros (?&?&?); apply Hz'; tauto. }
-    split; simpl; first tauto.
-    intros. rewrite Hy //. tauto.
-  - by intros [x px ?] [y py ?] (?&?&?).
-Qed.
-Canonical Structure validityR : cmra :=
-  discreteR (validity A) validity_ra_mixin.
-
-Global Instance validity_disrete_cmra : CmraDiscrete validityR.
-Proof. apply discrete_cmra_discrete. Qed.
-Global Instance validity_cmra_total : CmraTotal validityR.
-Proof. rewrite /CmraTotal; eauto. Qed.
-
-Lemma validity_update x y :
-  (∀ c, ✓ x → ✓ c → validity_car x ## c → ✓ y ∧ validity_car y ## c) → x ~~> y.
-Proof.
-  intros Hxy; apply cmra_discrete_update=> z [?[??]].
-  split_and!; try eapply Hxy; eauto.
-Qed.
-
-Lemma to_validity_op a b :
-  (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ## b) →
-  to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b.
-Proof. split; naive_solver eauto using dra_op_valid. Qed.
-
-(* TODO: This has to be proven again. *)
-(*
-Lemma to_validity_included x y:
-  (✓ y ∧ to_validity x ≼ to_validity y)%stdpp ↔ (✓ x ∧ x ≼ y).
-Proof.
-  split.
-  - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
-    destruct Hvl' as [? [? ?]]; split; first done.
-    exists (validity_car z); eauto.
-  - intros (Hvl & z & EQ & ? & ?).
-    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
-    split; first done. exists (to_validity z). split; first split.
-    + intros _. simpl. by split_and!.
-    + intros _. setoid_subst. by apply dra_op_valid.
-    + intros _. rewrite /= EQ //.
-Qed.
-*)
-End dra.

iris/algebra/sts.v

+(**
+This file formalizes the STS construction from the original Iris paper (POPL15).
+
+DISCLAIMER: The definition of STSs is included in the Iris development for
+historical purposes. If you plan to mechanize an Iris proof in Coq, it is
+usually better to use a more direct encoding of the ghost state you need as a
+resource algebra (camera). STSs are very painful to use in Coq, and they are
+therefore barely used in practice.
+
+The type [stsT] describes state-transition systems: a type of states, a type of
+tokens, a step relation between states, and a token assignment function. Then
+[sts_resR sts], for [sts: stsT], is the resource algebra of "STS resources",
+which can be fragments ("we are in one of these states", where the set of states
+needs to be closed under transitions performed without the locally owned
+tokens), or authoritative ("we are exactly in this state").
+
+The construction is performed via an intermediate internal type, [sts.car]. The
+reason for this intermediate step is that composition of two STS resources is
+defined only if their token sets are disjoint and the state sets are not
+disjoint (i.e., they have at least one element in common). This condition is not
+decidable, so we cannot use the usual approach (used e.g. in [gset_disj]) of
+just composing those pairs to a dedicated "invalid" element. Instead, [sts_res]
+consists of an [sts.car] element (fragment or authoritative), together with a
+[Prop] defining whether this element is valid. That way we can "defer" the
+validity check from composition to RA validity.
+*)
+
 From stdpp Require Export propset.
-From iris.algebra Require Export cmra.
-From iris.algebra Require Import dra.
+From iris.algebra Require Export cmra updates.
 From iris.prelude Require Import options.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
 
-(** DISCLAIMER: The definition of STSs is included in the Iris development for
-historical purposes. If you plan to mechanize an Iris proof in Coq, it is
-usually better to use a more direct encoding of the ghost state you need as a
-resource algebra (camera). STSs are very painful to use in Coq, and they are
-therefore barely used in practice. *)
-
 (** * Definition of STSs *)
 Module sts.
 Structure stsT := Sts {
@@ -174,8 +194,9 @@ End sts.
 Notation steps := (rtc step).
 Notation frame_steps T := (rtc (frame_step T)).
 
-(* The type of bounds we can give to the state of an STS. This is the type
-   that we equip with an RA structure. *)
+(* The type of bounds we can give to the state of an STS. On paper, this is the
+   type that we equip with an RA structure. In Coq we have to do some work to
+   model composition only being defined under some non-computable conditions. *)
 Inductive car (sts : stsT) :=
   | auth : state sts → propset (token sts) → car sts
   | frag : propset (state sts) → propset (token sts) → car sts.
@@ -186,39 +207,39 @@ End sts.
 Notation stsT := sts.stsT.
 Notation Sts := sts.Sts.
 
-(** * STSs form a disjoint RA *)
-Section sts_dra.
-Context (sts : stsT).
+(** * STSs form an RA *)
+Section sts_res.
+Context {sts : stsT}.
 Import sts.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
 
-Inductive sts_equiv : Equiv (car sts) :=
+Inductive sts_car_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.
-Local Existing Instance sts_equiv.
-Local Instance sts_valid_instance : Valid (car sts) := λ x,
+Local Existing Instance sts_car_equiv.
+Local Instance sts_car_valid_instance : Valid (car sts) := λ x,
   match x with
   | auth s T => tok s ## T
   | frag S' T => closed S' T ∧ ∃ s, s ∈ S'
   end.
-Local Instance sts_core_instance : PCore (car sts) := λ x,
+Local Instance sts_car_core_instance : PCore (car sts) := λ x,
   Some match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
   | auth s _  => frag (up s ∅) ∅
   end.
-Inductive sts_disjoint : Disjoint (car sts) :=
+Inductive sts_car_disjoint_instance : Disjoint (car sts) :=
   | frag_frag_disjoint S1 S2 T1 T2 :
      (∃ s, s ∈ 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.
-Local Existing Instance sts_disjoint.
+Local Existing Instance sts_car_disjoint_instance.
 Local Instance sts_op_instance : 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)(* never happens *)
+  | auth s T1, auth _ T2 => auth s (T1 ∪ T2) (* never happens *)
   end.
 
 Local Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
@@ -232,62 +253,199 @@ Proof. by constructor. Qed.
 Global Instance frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@frag sts).
 Proof. by constructor. Qed.
 
-Local Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
+Local Instance sts_car_equivalence: Equivalence ((≡) : relation (car sts)).
 Proof.
   split.
   - by intros []; constructor.
   - by destruct 1; constructor.
   - destruct 1; inversion_clear 1; constructor; etrans; eauto.
 Qed.
-Lemma sts_dra_mixin : DraMixin (car sts).
+Local Instance sts_car_op_proper : Proper ((≡@{car sts}) ==> (≡) ==> (≡)) (⋅).
+Proof. by do 2 destruct 1; constructor; setoid_subst. Qed.
+Local Instance sts_car_core_proper : Proper ((≡@{car sts}) ==> (≡)) core.
+Proof. by destruct 1; constructor; setoid_subst. Qed.
+Local Instance sts_car_valid_proper : Proper ((≡@{car sts}) ==> impl) valid.
+Proof. by destruct 1; simpl; intros ?; setoid_subst. Qed.
+Local Instance sts_car_valid_proper' : Proper ((≡@{car sts}) ==> iff) valid.
+Proof. by split; apply: sts_car_valid_proper. Qed.
+Local Instance sts_car_disjoint_proper (x : car sts) :
+  Proper ((≡) ==> impl) (disjoint x).
 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; econstructor; setoid_subst.
-  - destruct 3; simpl in *; destruct_and?; eauto using closed_op;
-      select (closed _ _) (fun H => destruct H); set_solver.
-  - intros []; naive_solver eauto using closed_up, closed_up_set,
+  by intros ? [|]; destruct 1; inversion_clear 1; econstructor; setoid_subst.
+Qed.
+
+Local Instance sts_car_disjoint_symmetric : Symmetric (@disjoint (car sts) _).
+Proof. destruct 1; constructor; auto with sts. Qed.
+Local Instance sts_car_disjoint_proper' :
+  Proper ((≡@{car sts}) ==> (≡) ==> iff) disjoint.
+Proof.
+  intros x1 x2 Hx y1 y2 Hy; split.
+  - by rewrite Hy (symmetry_iff (##) x1) (symmetry_iff (##) x2) Hx.
+  - by rewrite -Hy (symmetry_iff (##) x2) (symmetry_iff (##) x1) -Hx.
+Qed.
+
+Local Lemma sts_car_core_valid (x : car sts) :
+  ✓ x → ✓ core x.
+Proof.
+  destruct x; naive_solver eauto using closed_up, closed_up_set,
       elem_of_up, elem_of_up_set 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 []; constructor; eauto with sts.
-  - intros []; 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. exists (core (x ⋅ y))=> ?? Hxy; split_and?.
-    + destruct Hxy; constructor; unfold up_set; set_solver.
-    + destruct Hxy; simpl;
-        eauto using closed_up_set_empty, closed_up_empty with sts.
-    + destruct Hxy; econstructor;
-        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.
-Qed.
-Canonical Structure stsDR : draT := DraT (car sts) sts_dra_mixin.
-End sts_dra.
-
-(** * The STS Resource Algebra *)
+Qed.
+Local Lemma sts_car_op_valid (x y : car sts) :
+  ✓ x → ✓ y → x ## y → ✓ (x ⋅ y).
+Proof.
+  destruct 3; simpl in *; destruct_and?; eauto using closed_op;
+      select (closed _ _) (fun H => destruct H); set_solver.
+Qed.
+Local Lemma sts_car_op_assoc (x y z : car sts) :
+  ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z.
+Proof.
+  destruct x, y, z; intros _ _ _ _ _; constructor; rewrite ?assoc; auto with sts.
+Qed.
+Local Lemma sts_car_op_comm (x y : car sts) :
+  ✓ x → ✓ y → x ## y → x ⋅ y ≡ y ⋅ x.
+Proof. destruct 3; constructor; auto with sts. Qed.
+
+Local Lemma sts_car_disjoint_ll (x y z : car sts) :
+  ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## z.
+Proof.
+  destruct 4; inversion_clear 1; constructor; auto with sts.
+Qed.
+Local Lemma sts_car_disjoint_rl (x y z : car sts) :
+  ✓ x → ✓ y → ✓ z → y ## z → x ## y ⋅ z → x ## y.
+Proof. intros ???. rewrite !(symmetry_iff _ x). by apply sts_car_disjoint_ll. Qed.
+Local Lemma sts_car_disjoint_lr (x y z : car sts) :
+  ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → y ## z.
+Proof. intros ????. rewrite sts_car_op_comm //. by apply sts_car_disjoint_ll. Qed.
+Local Lemma sts_car_disjoint_move_l (x y z : car sts) :
+    ✓ x → ✓ y → ✓ z → x ## y → x ⋅ y ## z → x ## y ⋅ z.
+Proof. destruct 4; inversion_clear 1; constructor; auto with sts. Qed.
+Local Lemma sts_car_disjoint_move_r (a b c : car sts) :
+  ✓ a → ✓ b → ✓ c → b ## c → a ## b ⋅ c → a ⋅ b ## c.
+Proof.
+  intros; symmetry; rewrite sts_car_op_comm; eauto using sts_car_disjoint_rl.
+  apply sts_car_disjoint_move_l; auto; by rewrite sts_car_op_comm.
+Qed.
+Local Hint Immediate sts_car_disjoint_move_l sts_car_disjoint_move_r : core.
+
+Local Lemma sts_car_core_disjoint_l (x : car sts) : ✓ x → core x ## x.
+Proof. destruct x; constructor; eauto with sts. Qed. 
+Local Lemma sts_car_core_l (x : car sts) : ✓ x → core x ⋅ x ≡ x.
+Proof. destruct x; constructor; eauto with sts. Qed.
+Local Lemma sts_car_core_idemp (x : car sts) : ✓ x → core (core x) ≡ core x.
+Proof.
+  destruct x as [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.
+Qed.
+Local Lemma sts_car_core_mono (x y : car sts) :
+  ∃ z, ✓ x → ✓ y → x ## y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ## z.
+Proof.
+  exists (core (x ⋅ y))=> ?? Hxy; split_and?.
+  + destruct Hxy; constructor; unfold up_set; set_solver.
+  + destruct Hxy; simpl;
+      eauto using closed_up_set_empty, closed_up_empty with sts.
+  + destruct Hxy; econstructor;
+      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.
+Qed.
+
+(** The resource type for [sts]. *)
+Record sts_res := StsRes {
+  (** The underlying STS carrier element, storing the actual data. *)
+  sts_car : car sts;
+  (** Defines whether this element is valid. *)
+  sts_valid : Prop;
+  (** Valid elements must have a valid carrier element. *)
+  sts_valid_prf : sts_valid → ✓ sts_car
+}.
+Add Printing Constructor sts_res.
+Global Arguments StsRes _ _ {_}.
+
+(** Setoid and OFE for [sts_res]. *)
+Local Instance sts_equiv : Equiv sts_res := λ x y,
+  (sts_valid x ↔ sts_valid y) ∧ (sts_valid x → sts_car x ≡ sts_car y).
+Local Instance sts_equivalence : Equivalence (@equiv sts_res _).
+Proof.
+  split; unfold equiv, sts_equiv.
+  - by intros [x px ?]; simpl.
+  - intros [x px ?] [y py ?]; naive_solver.
+  - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
+    split; [|intros; trans y]; tauto.
+Qed.
+Canonical Structure sts_resO : ofe := discreteO sts_res.
+
+(** RA for [sts_res]. *)
+Local Instance sts_res_valid_instance : Valid sts_res := sts_valid.
+Local Program Instance sts_res_pcore_instance : PCore sts_res := λ x,
+  Some (StsRes (core (sts_car x)) (✓ x)).
+Next Obligation.
+  intros []; naive_solver eauto using sts_car_core_valid.
+Qed.
+Local Program Instance sts_res_op_instance : Op sts_res := λ x y,
+  StsRes (sts_car x ⋅ sts_car y)
+           (✓ x ∧ ✓ y ∧ sts_car x ## sts_car y).
+Next Obligation.
+  intros [] []; naive_solver eauto using sts_car_op_valid.
+Qed.
+
+Definition sts_res_ra_mixin : RAMixin sts_res.
+Proof.
+  apply ra_total_mixin; first eauto.
+  - intros ??? [? Heq]; split; simpl; [|intros (?&?&?); by rewrite Heq].
+    split; intros (?&?&?); split_and!;
+      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
+  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
+  - intros ?? [??]; naive_solver.
+  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
+      [intuition eauto 2 using sts_car_disjoint_lr, sts_car_disjoint_rl
+      |intuition eauto using sts_car_op_assoc, sts_car_disjoint_rl].
+  - intros [x px ?] [y py ?]; split; naive_solver eauto using sts_car_op_comm.
+  - intros [x px ?]; split;
+      naive_solver eauto using sts_car_core_l, sts_car_core_disjoint_l.
+  - intros [x px ?]; split; naive_solver eauto using sts_car_core_idemp.
+  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
+    destruct (sts_car_core_mono x z) as (z'&Hz').
+    unshelve eexists (StsRes z' (px ∧ py ∧ pz)).
+    { intros (?&?&?); apply Hz'; tauto. }
+    split; simpl; first tauto.
+    intros. rewrite Hy //. tauto.
+  - by intros [x px ?] [y py ?] (?&?&?).
+Qed.
+Canonical Structure sts_resR : cmra :=
+  discreteR sts_res sts_res_ra_mixin.
+
+Global Instance sts_res_disrete_cmra : CmraDiscrete sts_resR.
+Proof. apply discrete_cmra_discrete. Qed.
+Global Instance sts_res_cmra_total : CmraTotal sts_resR.
+Proof. rewrite /CmraTotal; eauto. Qed.
+
+Local Definition to_sts_res (x : car sts) : sts_res :=
+  @StsRes x (valid x) id.
+Global Instance to_sts_res_proper : Proper ((≡) ==> (≡)) to_sts_res.
+Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
+
+Lemma to_sts_res_op a b :
+  (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ## b) →
+  to_sts_res (a ⋅ b) ≡ to_sts_res a ⋅ to_sts_res b.
+Proof. split; naive_solver eauto using sts_car_op_valid. Qed.
+
+End sts_res.
+
+Global Arguments sts_resR : clear implicits.
+
 (** Finally, the general theory of STS that should be used by users *)
-Notation stsC sts := (validityO (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 :=
+  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : sts_resR sts :=
+    to_sts_res (sts.auth s T).
+  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : sts_resR sts :=
+    to_sts_res (sts.frag S T).
+  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : sts_resR sts :=
     sts_frag (sts.up s T) T.
 End sts_definitions.
 Global Instance: Params (@sts_auth) 2 := {}.
@@ -300,7 +458,7 @@ Context {sts : stsT}.
 Implicit Types s : state sts.
 Implicit Types S : states sts.
 Implicit Types T : tokens sts.
-Local Arguments dra_valid _ !_/.
+Local Arguments cmra_valid _ !_/.
 
 (** Setoids *)
 Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
@@ -352,7 +510,7 @@ Lemma sts_frag_op 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 //.
+  intros HT HS1 HS2. rewrite /sts_frag -to_sts_res_op //.
   move=>/=[?[? ?]]. split_and!; [set_solver..|constructor; set_solver].
 Qed.
 
@@ -367,8 +525,10 @@ Lemma sts_frag_up_op s T1 T2 :
 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?.
+  intros ?. apply cmra_discrete_update.
+  intros [x x_val Hx_val]; simpl. intros (Htok & Hval & Hdisj).
+  specialize (Hx_val Hval).
+  inversion Hdisj as [|? S ? Tf|]; simplify_eq/=; destruct_and?.
   destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
   repeat (done || constructor).
 Qed.
@@ -376,14 +536,18 @@ Qed.
 Lemma sts_update_frag S1 S2 T1 T2 :
   (closed S1 T1 → closed S2 T2 ∧ S1 ⊆ S2 ∧ T2 ⊆ T1) → sts_frag S1 T1 ~~> sts_frag S2 T2.
 Proof.
-  rewrite /sts_frag=> HC HS HT. apply validity_update.
-  inversion 3 as [|? S ? Tf|]; simplify_eq/=;
+  rewrite /sts_frag=> HC HS HT. apply cmra_discrete_update.
+  intros [x x_val Hx_val]; simpl. intros (Htok & Hval & Hdisj).
+  specialize (Hx_val Hval).
+  inversion Hdisj as [|? S ? Tf|]; simplify_eq/=;
     (destruct HC as (? & ? & ?); first by destruct_and?).
   - split_and!; first done.
     + set_solver.
+    + done.
     + constructor; set_solver.
   - split_and!; first done.
     + set_solver.
+    + done.
     + constructor; set_solver.
 Qed.
 
@@ -408,7 +572,9 @@ Qed.
 
 Global Instance sts_frag_core_id S : CoreId (sts_frag S ∅).
 Proof.
-  constructor; split=> //= [[??]]. by rewrite /dra.dra_pcore /= sts.up_closed.
+  constructor; split=> //= [[??]].
+  (* FIXME: rewriting with [sts.up_closed] for some reason fails here. *)
+  f_equiv. by rewrite sts.up_closed.
 Qed.
 
 (** Inclusion *)

iris_deprecated/base_logic/sts.v

@@ -10,11 +10,11 @@ Import uPred.
 
 (** The CMRA we need. *)
 Class stsG Σ (sts : stsT) := StsG {
-  sts_inG :> inG Σ (stsR sts);
+  sts_inG :> inG Σ (sts_resR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
 
-Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (stsR sts) ].
+Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (sts_resR sts) ].
 Global Instance subG_stsΣ Σ sts :
   subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
 Proof. solve_inG. Qed.