From a0084dff82e9b061693d54d7862a1cbcf69edc26 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Tue, 22 Sep 2026 20:23:25 -0700
Subject: [PATCH 1/4] feat(Distributed): formalize notions of consistency for
 replicated data types and prove their relationships

---
 Cslib.lean                                    |   2 +
 .../Distributed/Consistency/Hierarchy.lean    | 142 ++++++++++
 .../Consistency/Specification.lean            | 256 ++++++++++++++++++
 Cslib/Foundations/Relation/Basic.lean         |   4 +
 Cslib/Foundations/Relation/Defs.lean          |  30 +-
 references.bib                                |  23 ++
 6 files changed, 456 insertions(+), 1 deletion(-)
 create mode 100644 Cslib/Computability/Distributed/Consistency/Hierarchy.lean
 create mode 100644 Cslib/Computability/Distributed/Consistency/Specification.lean

diff --git a/Cslib.lean b/Cslib.lean
index 5f5b726b30..90ee786180 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -50,6 +50,8 @@ public import Cslib.Computability.Circuit.Shannon
 public import Cslib.Computability.Circuit.Signature
 public import Cslib.Computability.Circuit.Synthesis
 public import Cslib.Computability.Circuit.Wire
+public import Cslib.Computability.Distributed.Consistency.Hierarchy
+public import Cslib.Computability.Distributed.Consistency.Specification
 public import Cslib.Computability.Distributed.FLP.Algorithm
 public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
diff --git a/Cslib/Computability/Distributed/Consistency/Hierarchy.lean b/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
new file mode 100644
index 0000000000..220a7f8f44
--- /dev/null
+++ b/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
@@ -0,0 +1,142 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Computability.Distributed.Consistency.Specification
+public import Cslib.Foundations.Relation.Basic
+public import Mathlib.Data.Set.Finite.Basic
+
+/-! # Consistency hierarchy
+
+We prove a number of results about the various notions of consistency for replicated data types.
+In paricular, we prove that:
+
+  Linearizability → SequentialConsistency → CausalConsistency → BasicEventualConsistency
+
+Our proofs follow closely the proof of Proposition 5.1 of [Burckhardt2014].
+
+## References
+
+* [*Principles of Eventual Consistency*][Burckhardt2014]
+-/
+
+@[expose] public section
+
+namespace Cslib.DistributedConsistency
+
+open Relation AbstractExecution
+
+variable {Event Operation Value Session : Type*}
+  {d : ReplicatedDataType Event Operation Value}
+  {a : AbstractExecution Event Operation Value Session}
+
+instance isTrans_ar : IsTrans Event a.ar :=
+  ⟨a.ar_strict_total_order.trans⟩
+
+lemma so_iff_se_rb (s : Session) (x y : Event) :
+    a.so s x y ↔ a.se x = s ∧ a.se y = s ∧ a.rb x y := by
+  simp only [BaseHistory.so, restrict]
+  grind
+
+lemma so_le_rb (s : Session) : a.so s ≤ a.rb := by
+  intro x y
+  simp [so_iff_se_rb]
+
+lemma se_rval_eq_none {s : Session} {x : Event} (h1 : a.se x = s) (h2 : a.rval x = none) :
+    {y | a.se y = s} = {y | a.se y = s ∧ a.rb y x } ∪ {x} := by
+  ext y
+  apply Iff.intro
+  · intro h_se
+    by_cases x = y
+    · grind
+    · by_contra h_contra
+      suffices a.rb x y by grind [a.rb_rval_ne_none]
+      obtain ⟨_, h_tri⟩ := a.so_strict_total_order s
+      specialize h_tri x y
+      grind [so_iff_se_rb]
+  · grind
+
+lemma singleOrder_vis_ar_rval_ne_none (h : a.SingleOrder) (x y : Event) :
+    (a.vis x y → a.ar x y) ∧ (a.ar x y → a.rval x ≠ none → a.vis x y) := by
+  obtain ⟨_, _, _⟩ := h
+  grind
+
+lemma singleOrder_realTime_imp_readMyWrites
+    (h1 : a.SingleOrder) (h2 : a.RealTime) : a.ReadMyWrites := by
+  rintro s x y h_so
+  have h_so_ar : a.so s ≤ a.ar := by grind [RealTime, so_le_rb]
+  grind [singleOrder_vis_ar_rval_ne_none, a.rb_rval_ne_none,
+    so_le_rb s x y h_so, h_so_ar x y h_so]
+
+theorem linearizability_imp_sequentialConsistency
+    (h : a.Linearizability d) : a.SequentialConsistency d := by
+  grind [Linearizability, SequentialConsistency, singleOrder_realTime_imp_readMyWrites]
+
+lemma readMyWrites_imp_hb_le_trans_vis
+    (h : a.ReadMyWrites) (s : Session) : a.hb s ≤ TransGen a.vis := by
+  apply TransGen.mono
+  rintro x y (h1 | h2)
+  · exact h s x y h1
+  · exact h2
+
+lemma singleOrder_readMyWrites_imp_causalArbitration
+    (h1 : a.SingleOrder) (h2 : a.ReadMyWrites) : a.CausalArbitration := by
+  intro s
+  suffices TransGen a.vis ≤ a.ar by grind [readMyWrites_imp_hb_le_trans_vis h2 s]
+  have h_ar : TransGen a.ar = a.ar := by exact transGen_eq_self
+  rw [← h_ar]
+  apply TransGen.mono
+  obtain ⟨_, _, _⟩ := h1
+  intro _ _ _
+  grind
+
+lemma singleOrder_readMyWrites_imp_causalVisibility
+    (h1 : a.SingleOrder) (h2 : a.ReadMyWrites) : a.CausalVisibility := by
+  intro s
+  suffices TransGen a.vis ≤ a.vis by grind [readMyWrites_imp_hb_le_trans_vis h2 s]
+  suffices IsTrans Event a.vis by grind
+  obtain ⟨_, _, _⟩ := h1
+  grind [IsTrans, isTrans_ar]
+
+lemma singleOrder_imp_eventualVisibility
+    (h : a.SingleOrder) : a.EventualVisibility := by
+  intro x s
+  by_cases a.rval x = none
+  · have h_rb : ∀ y, ¬ a.rb x y := by grind [a.rb_rval_ne_none]
+    simp [nonVisibleEvents, h_rb]
+  · by_cases h_y : ∃ y, a.se y = s ∧ a.rval y = none
+    · obtain ⟨y, h_y1, h_y2⟩ := h_y
+      have h_ss1 : a.nonVisibleEvents x s ⊆ {z | a.se z = s} := by grind [nonVisibleEvents]
+      refine Set.Finite.subset ?_ h_ss1
+      simp only [se_rval_eq_none h_y1 h_y2, Set.union_singleton, Set.finite_insert]
+      have h_ss2 : {z | a.se z = s ∧ a.rb z y} ⊆ predecessors a.rb y := by simp
+      exact Set.Finite.subset (a.rb_pred_finite y) h_ss2
+    · simp only [not_exists, not_and] at h_y
+      suffices h_ss : a.nonVisibleEvents x s ⊆ predecessors a.vis x by
+        exact Set.Finite.subset (a.vis_pred_finite x) h_ss
+      rintro y ⟨_, _, _⟩
+      have : x ≠ y := by grind [a.rb_strict_order.irrefl]
+      have : ¬ a.ar x y := by grind [singleOrder_vis_ar_rval_ne_none]
+      have : a.ar y x := by grind [a.ar_strict_total_order.trichotomous]
+      grind [singleOrder_vis_ar_rval_ne_none]
+
+theorem sequentialConsistency_imp_causalConsistency
+    (h : a.SequentialConsistency d) : a.CausalConsistency d := by
+  grind [SequentialConsistency, CausalConsistency, Causality, singleOrder_imp_eventualVisibility,
+    singleOrder_readMyWrites_imp_causalArbitration, singleOrder_readMyWrites_imp_causalVisibility]
+
+lemma causality_imp_noCircularCausality
+    (h : a.Causality) : a.NoCircularCausality := by
+  intro s
+  have : a.hb s ≤ a.vis := by grind [Causality, CausalVisibility]
+  grind [a.vis_acyclic, acyclic_le]
+
+theorem causalConsistency_imp_basicEventualConsistency
+    (h : a.CausalConsistency d) : a.BasicEventualConsistency d := by
+  grind [CausalConsistency, BasicEventualConsistency, causality_imp_noCircularCausality]
+
+end Cslib.DistributedConsistency
diff --git a/Cslib/Computability/Distributed/Consistency/Specification.lean b/Cslib/Computability/Distributed/Consistency/Specification.lean
new file mode 100644
index 0000000000..922aa9aae3
--- /dev/null
+++ b/Cslib/Computability/Distributed/Consistency/Specification.lean
@@ -0,0 +1,256 @@
+/-
+Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+module
+
+public import Cslib.Foundations.Relation.Defs
+public import Mathlib.Basic.Finite.Defs
+
+/-! # Consistency specifications
+
+We formalize several notions of consistency for replicated data types defined in [Burckhardt2014],
+listed below in decreasing order of strength:
+* Linearizability,
+* Sequential consistency.
+* Causal consistency,
+* Basic eventual consistency,
+* Quiescent consistency.
+
+We follow [Burckhardt2014] closely in the formalization except for one detail:
+instead of using an equivalence relation "same-session" to model the notion of sessions,
+we use a map `se : Event → Session` and regard two events `x` and `y` to belong to the
+same session iff `se x = se y`.  These two approaches are clearly equivalent and `se` is
+chosen because it is easier to work with.
+
+## References
+
+* [*Principles of Eventual Consistency*][Burckhardt2014]
+-/
+
+@[expose] public section
+
+namespace Cslib.DistributedConsistency
+
+open Set Relation
+
+variable {Event Operation Value Session : Type*}
+
+/-- `BaseHistory` is an auxiliary definition containing all data fields of `History` below. -/
+structure BaseHistory (Event Operation Value Session : Type*) where
+  /-- `op` assigns each event its operation. -/
+  op : Event → Operation
+  /-- `se` assigns each event its session. -/
+  se : Event → Session
+  /-- `rval` assigns each event its return value, where `none` indicates that
+  the event never returns. -/
+  rval : Event → Option Value
+  /-- `rb` is the "returns before" order on events. -/
+  rb : Event → Event → Prop
+
+/-- `so` (for "session order") is `rb` restricted to a single session. -/
+def BaseHistory.so (h : BaseHistory Event Operation Value Session) (s : Session) :=
+  restrict h.rb {x | h.se x = s}
+
+/-- `History` extends `BaseHistory` with well-formedness conditions. -/
+structure History (Event Operation Value Session : Type*)
+    extends bh : BaseHistory Event Operation Value Session where
+  /-- `rb` is a strict order on events (namely, it is irreflexive and transitive). -/
+  rb_strict_order : IsStrictOrder Event rb
+  /-- Each event has only a finite number of predecessors in the `rb` order. -/
+  rb_pred_finite : ∀ x, (predecessors rb x).Finite
+  /-- The `rb` order is an interval order. -/
+  rb_interval_order : IsIntervalOrder rb
+  /-- If an event `x` returns before another event `y`, then `x` cannot return `none`. -/
+  rb_rval_ne_none : ∀ x y, rb x y → rval x ≠ none
+  /-- The `so` order is a strict total order of the events of each session. -/
+  so_strict_total_order : ∀ s, IsStrictTotalOrderOn {x | se x = s} (bh.so s)
+
+/-- `AbstractExecution` extends `History` with two more orders and additional
+well-formedness conditions. -/
+structure AbstractExecution (Event Operation Value Session : Type*)
+    extends History Event Operation Value Session where
+  /-- `vis x y` means that `x` is visible to `y`. -/
+  vis : Event → Event → Prop
+  /-- `ar` is the arbitration order of the whole system. -/
+  ar : Event → Event → Prop
+  /-- The visibility order `vis` is acyclic. -/
+  vis_acyclic : Acyclic vis
+  /-- Each event has only a finite number of predecessors in the `vis` order. -/
+  vis_pred_finite : ∀ x, (predecessors vis x).Finite
+  /-- The arbitration order is a strict total order of all events. -/
+  ar_strict_total_order : IsStrictTotalOrder Event ar
+
+/-- A history satisfies a predicte `p` on abstract executions iff it can be extended
+to an abstract execution satisfying `p`. -/
+def History.Satisfies (h : History Event Operation Value Session)
+    (p : AbstractExecution Event Operation Value Session → Prop) : Prop :=
+  ∃ a : AbstractExecution Event Operation Value Session, a.toHistory = h ∧ p a
+
+namespace AbstractExecution
+
+/-- `ReadMyWrites` says that if two events are ordered by `so`,
+then they are also ordered by `vis`. -/
+def ReadMyWrites (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∀ s, a.so s ≤ a.vis
+
+/-- `MonotonicReads` says that if `x` is visible to `y`, then `x` is also visible to all
+successors of `y` under the `so` order. -/
+def MonotonicReads (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∀ s x y z, a.vis x y → a.so s y z → a.vis x z
+
+/-- `ConsistentPrefix` says that if `x` is visible to `y` in a different session,
+then all predecessors of `x` in the arbitration order are also visible to `y`. -/
+def ConsistentPrefix (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∀ x y, a.se x ≠ a.se y → a.vis x y → ∀ z, a.ar z x → a.vis z y
+
+/-- The `happens before` order is the per-session transitive closure of the union of
+the `so` and `vis` orders. -/
+def hb (a : AbstractExecution Event Operation Value Session)
+    (s : Session) : Event → Event → Prop :=
+  TransGen fun x y ↦ a.so s x y ∨ a.vis x y
+
+/-- `NoCircularCausality` says that the `hb` order is acyclic. -/
+def NoCircularCausality (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∀ s, Acyclic (a.hb s)
+
+/-- `CausalArbitration` says that if two events are ordered by `hb`,
+then they are also ordered by `ar`. -/
+def CausalArbitration (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∀ s, a.hb s ≤ a.ar
+
+/-- `CausalVisibility` says that if two events are ordered by `hb`,
+then they are also ordered by `vis`. -/
+def CausalVisibility (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∀ s, a.hb s ≤ a.vis
+
+/-- `Causality` is the conjunction of `CausalArbitration` and `CausalVisibility`. -/
+def Causality (a : AbstractExecution Event Operation Value Session) : Prop :=
+  a.CausalArbitration ∧ a.CausalVisibility
+
+/-- `SingleOrder` says that `vis` and `ar` are the same order except that there may be
+a set of events which never returns and are not visible. -/
+def SingleOrder (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∃ xs : Set Event, (∀ x, x ∈ xs → a.rval x = none) ∧
+    ∀ x y, a.vis x y ↔ a.ar x y ∧ ¬ x ∈ xs
+
+/-- `RealTime` says that if two events are ordered by `rb`, then they are also ordered by `ar`. -/
+def RealTime (a : AbstractExecution Event Operation Value Session) : Prop :=
+  a.rb ≤ a.ar
+
+/-- `a.nonVisibleEvents x s` is the set of events in session `s` which returns after `x`
+but does not see `x`. -/
+def nonVisibleEvents (a : AbstractExecution Event Operation Value Session)
+    (x : Event) (s : Session) : Set Event :=
+  { y | a.se y = s ∧ a.rb x y ∧ ¬ a.vis x y }
+
+/-- `EventualVisibility` says that for any event `x` and any session `s`, there can be at most
+finitely many events in `s` that return after `x` and do not see `x`.
+-/
+def EventualVisibility (a : AbstractExecution Event Operation Value Session) : Prop :=
+  ∀ x : Event, ∀ s : Session, (a.nonVisibleEvents x s).Finite
+
+end AbstractExecution
+
+/-- An `OperationContext` is the data used by a replicated data type to determine the
+return value of an operation.  It is an abstraction of the notion of states. -/
+structure OperationContext (Event Operation : Type*) where
+  /-- The set of events in the operation context. -/
+  events : Set Event
+  /-- Operation labeling of events. -/
+  op : Event → Operation
+  /-- Visibility order. -/
+  vis : Event → Event → Prop
+  /-- Arbitration order. -/
+  ar : Event → Event → Prop
+
+/-- The notion of equivalence on `OperationContext`, which is essentially an isomorphism
+that ignores the identities of events and the behavior of `op`, `vis`, and `ar` outside
+the set of events in the operation context. -/
+structure OperationContext.Equiv (c1 c2 : OperationContext Event Operation) where
+  /-- A bijection from `c1`'s events to `c2`'s events. -/
+  equiv : { x // x ∈ c1.events } ≃ { x // x ∈ c2.events }
+  /-- `op` is preserved by the bijection. -/
+  op_equiv : ∀ x, c1.op x.val = c2.op (equiv x).val
+  /-- `vis` is preserved by the bijection. -/
+  vis_equiv : ∀ x y, c1.vis x.val y.val ↔ c2.vis (equiv x).val (equiv y).val
+  /-- `ar` is preserved by the bijection. -/
+  ar_equiv : ∀ x y, c1.ar x.val y.val ↔ c2.ar (equiv x).val (equiv y).val
+
+/-- The notion of a replicated data type. -/
+structure ReplicatedDataType (Event Operation Value : Type*) where
+  /-- `rval` takes an operation and an operation context and returns a value. -/
+  rval : Operation → OperationContext Event Operation → Option Value
+  /-- For any operation, `rval` must returns the same value on equivalent operation contexts. -/
+  rval_equiv : ∀ o c1 c2, ∀ _ : c1.Equiv c2, rval o c1 = rval o c2
+
+/-- For a replicated data type `d`, an operation `o` is read-only iff an event with operation `o`
+can be removed from any operation context without affecting the behavior of `d`. -/
+def ReplicatedDataType.ReadOnlyOp (d : ReplicatedDataType Event Operation Value)
+    (o : Operation) : Prop :=
+  ∀ c : OperationContext Event Operation, ∀ x ∈ c.events,
+    c.op x = o → ∀ o' : Operation, d.rval o' c = d.rval o' {c with events := c.events \ {x}}
+
+namespace AbstractExecution
+
+/-- `a.context xs` is the operation context obtained by restricting `a` to `xs`. -/
+def context (a : AbstractExecution Event Operation Value Session)
+    (xs : Set Event) : OperationContext Event Operation where
+  events := xs
+  op := a.op
+  vis := a.vis
+  ar := a.ar
+
+/-- `a.RVal d` says that the return value of any event in the abstract execution `a` is
+the same as the value returned by the replicated data type `d` in the context consisting of
+the predecessors of the event. -/
+def RVal (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value) : Prop :=
+  ∀ x, a.rval x = d.rval (a.op x) (a.context (predecessors a.vis x))
+
+/-- `Linearizability` is the conjunction of `SingleOrder`, `RealTime`, and `RVal`. -/
+def Linearizability (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value) : Prop :=
+  a.SingleOrder ∧ a.RealTime ∧ a.RVal d
+
+/-- `SequentialConsistency` is the conjunction of `SingleOrder`, `ReadMyWrites`, and `RVal`. -/
+def SequentialConsistency (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value) : Prop :=
+  a.SingleOrder ∧ a.ReadMyWrites ∧ a.RVal d
+
+/-- `CausalConsistency` is the conjunction of `EventualVisibility`, `Causality`, and `RVal`. -/
+def CausalConsistency (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value) : Prop :=
+  a.EventualVisibility ∧ a.Causality ∧ a.RVal d
+
+/-- `BasicEventualConsistency` is the conjunction of `EventualVisibility`, `NoCircularCausality`,
+and `RVal`. -/
+def BasicEventualConsistency (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value) : Prop :=
+  a.EventualVisibility ∧ a.NoCircularCausality ∧ a.RVal d
+
+/-- `a.updateEvents d` is the set of events in `a` whose operations are not read-only in `d` -/
+def updateEvents (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value) : Set Event :=
+  { x | ¬ d.ReadOnlyOp (a.op x) }
+
+/-- `a.nonRvalEvents d c s` is the set of events in `a` of session `s` whose return value
+does not agree with the value returned by `d` in the context `c`. -/
+def nonRvalEvents (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value)
+    (c : OperationContext Event Operation) (s : Session) : Set Event :=
+  { x | a.se x = s ∧ d.rval (a.op x) c ≠ a.rval x }
+
+/-- `a.QuiescentConsistency d` says that if the set of update events is finite, then there exists
+a context `c` such that for any session, there is at most a finite set of events for which
+the return values in the abstract execution `a` do not agree with the values returned by the
+replicated data type `d` in the context `c`. -/
+def QuiescentConsistency (a : AbstractExecution Event Operation Value Session)
+    (d : ReplicatedDataType Event Operation Value) : Prop :=
+  (a.updateEvents d).Finite → ∃ c, ∀ s, (a.nonRvalEvents d c s).Finite
+
+end AbstractExecution
+
+end Cslib.DistributedConsistency
diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean
index 9369e346cf..1cb81de567 100644
--- a/Cslib/Foundations/Relation/Basic.lean
+++ b/Cslib/Foundations/Relation/Basic.lean
@@ -177,4 +177,8 @@ theorem join_inl_reflTransGen (r₁_ab : ReflTransGen r₁ a b) : ReflTransGen (
 theorem join_inr_reflTransGen (r₂_ab : ReflTransGen r₂ a b) : ReflTransGen (r₁ ⊔ r₂) a b :=
   ReflTransGen.mono le_sup_right _ _ r₂_ab
 
+theorem acyclic_le {r s : α → α → Prop}
+    (hle : r ≤ s) (ha : Acyclic s) : Acyclic r := by
+  grind [irrefl_iff_le_ne, TransGen.mono hle]
+
 end Relation
diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean
index 07a6980e14..9486008df8 100644
--- a/Cslib/Foundations/Relation/Defs.lean
+++ b/Cslib/Foundations/Relation/Defs.lean
@@ -16,11 +16,13 @@ public import Mathlib.Logic.Relation
 
 * [*Term Rewriting and All That*][Baader1998]
 * [*Simple Laws about Nonprominent Properties of Binary Relations*][Burghardt2018]
-
+* [*Applied Combinatorics*][KellerTrotter2017]
 -/
 
 @[expose] public section
 
+variable {α β : Type*}
+
 namespace Relation
 
 /-! ### Operations on relations -/
@@ -137,6 +139,32 @@ class LeftEuclidean (r : α → α → Prop) where
 class Serial (r : α → α → Prop) where
   serial : Relator.LeftTotal r
 
+/-! ### Relations and sets in the underlying types -/
+
+/-- The set of successors of an element `a` in a relation `r`. -/
+abbrev successors (r : α → β → Prop) (a : α) : Set β := {b | r a b}
+
+/-- The set of predecessors of an element `b` in a relation `r`. -/
+abbrev predecessors (r : α → β → Prop) (b : β) : Set α := {a | r a b}
+
+/-- The restriction of a relation `r` to a set `s`. -/
+def restrict (r : α → α → Prop) (s : Set α) : α → α → Prop :=
+  fun a b ↦ a ∈ s ∧ b ∈ s ∧ r a b
+
+/-- `IsStrictTotalOrderOn s r` means that `r` is a strict total order on the set `s`. -/
+def IsStrictTotalOrderOn (s : Set α) (r : α → α → Prop) : Prop :=
+  IsStrictOrder α r ∧
+  ∀ a b, a ∈ s → b ∈ s → a = b ∨ r a b ∨ r b a
+
+/-! ### Interval order -/
+
+/-- Fishburn's theorem (see sections 6.6 and 6.7 of [KellerTrotter2017]) shows that
+the definition below is a sufficient and necessary condition for a relation `r` to have
+a representation by closed intervals on the real line such that `r i1 i2` iff the right
+endpoint of `i1` is less than the left endpoint of `i2`. -/
+def IsIntervalOrder (r : α → α → Prop) : Prop :=
+  ∀ a1 b1 a2 b2, r a1 b1 ∧ r a2 b2 → r a1 b2 ∨ r a2 b1
+
 end Relation
 
 /-! ### Properties of relations on restrictions of their (co)domain -/
diff --git a/references.bib b/references.bib
index afbe3d9b02..81e399a22e 100644
--- a/references.bib
+++ b/references.bib
@@ -80,6 +80,19 @@ @misc{BonehShoup2023
   url          = {https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf}
 }
 
+@book{Burckhardt2014,
+  author  = {Burckhardt, Sebastian},
+  title   = {Principles of Eventual Consistency},
+  series  = {Foundations and Trends in Programming Languages},
+  year    = {2014},
+  volume  = {1},
+  number  = {1-2},
+  pages   = {1--150},
+  doi     = {10.1561/2500000011},
+  publisher = {Now Publishers},
+  url = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/final-printversion-10-5-14.pdf}
+}
+
 @misc{Burghardt2018,
 	title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}},
 	url = {https://arxiv.org/abs/1806.05036v2},
@@ -275,6 +288,16 @@ @book{             KatzLindell2020
   isbn         = {9780815354369}
 }
 
+@book{KellerTrotter2017,
+  author    = {Keller, Mitchel T. and Trotter, William T.},
+  title     = {Applied Combinatorics},
+  year      = {2017},
+  isbn      = {978-1973702719},
+  publisher = {Self-published},
+  url       = {https://appliedcombinatorics.org},
+  note      = {Approved open textbook by the American Institute of Mathematics}
+}
+
 @article{         Shamir1979,
   author       = {Adi Shamir},
   title        = {How to Share a Secret},

From 65868f547c53ad9eb9156f5545b4dbd79703be91 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Tue, 29 Sep 2026 20:57:54 -0700
Subject: [PATCH 2/4] add some results corresponding to Lemma 5.1 in
 Burckhardt's book

---
 .../Distributed/Consistency/Hierarchy.lean    | 25 +++++++++++++------
 1 file changed, 18 insertions(+), 7 deletions(-)

diff --git a/Cslib/Computability/Distributed/Consistency/Hierarchy.lean b/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
index 220a7f8f44..2ce1fc1e67 100644
--- a/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
+++ b/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
@@ -94,6 +94,22 @@ lemma singleOrder_readMyWrites_imp_causalArbitration
   intro _ _ _
   grind
 
+lemma causalVisibility_imp_readMyWrites
+    (h : a.CausalVisibility) : a.ReadMyWrites := by
+  intro s x y h_so
+  exact h s x y <| TransGen.single (Or.inl h_so)
+
+lemma causalVisibility_imp_monotonicReads
+    (h : a.CausalVisibility) : a.MonotonicReads := by
+  intro s x y z h_vis h_so
+  exact h s x z <| TransGen.tail (TransGen.single (Or.inr h_vis)) (Or.inl h_so)
+
+lemma causalVisibility_imp_noCircularCausality
+    (h : a.CausalVisibility) : a.NoCircularCausality := by
+  intro s
+  have : a.hb s ≤ a.vis := by grind [CausalVisibility]
+  grind [a.vis_acyclic, acyclic_le]
+
 lemma singleOrder_readMyWrites_imp_causalVisibility
     (h1 : a.SingleOrder) (h2 : a.ReadMyWrites) : a.CausalVisibility := by
   intro s
@@ -129,14 +145,9 @@ theorem sequentialConsistency_imp_causalConsistency
   grind [SequentialConsistency, CausalConsistency, Causality, singleOrder_imp_eventualVisibility,
     singleOrder_readMyWrites_imp_causalArbitration, singleOrder_readMyWrites_imp_causalVisibility]
 
-lemma causality_imp_noCircularCausality
-    (h : a.Causality) : a.NoCircularCausality := by
-  intro s
-  have : a.hb s ≤ a.vis := by grind [Causality, CausalVisibility]
-  grind [a.vis_acyclic, acyclic_le]
-
 theorem causalConsistency_imp_basicEventualConsistency
     (h : a.CausalConsistency d) : a.BasicEventualConsistency d := by
-  grind [CausalConsistency, BasicEventualConsistency, causality_imp_noCircularCausality]
+  grind [CausalConsistency, BasicEventualConsistency,
+    Causality, causalVisibility_imp_noCircularCausality]
 
 end Cslib.DistributedConsistency

From 41d4a1d88615559154e923b28f1950cbcaafeab0 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Tue, 29 Sep 2026 21:00:34 -0700
Subject: [PATCH 3/4] fix a comment

---
 Cslib/Computability/Distributed/Consistency/Hierarchy.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/Distributed/Consistency/Hierarchy.lean b/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
index 2ce1fc1e67..9a515b8812 100644
--- a/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
+++ b/Cslib/Computability/Distributed/Consistency/Hierarchy.lean
@@ -17,7 +17,7 @@ In paricular, we prove that:
 
   Linearizability → SequentialConsistency → CausalConsistency → BasicEventualConsistency
 
-Our proofs follow closely the proof of Proposition 5.1 of [Burckhardt2014].
+Our proofs follow closely the proofs of Lemma 5.1 and Proposition 5.1 of [Burckhardt2014].
 
 ## References
 

From ece9331209a0ac3215f08b82500c88bb442eb480 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Thu, 1 Oct 2026 15:37:16 -0700
Subject: [PATCH 4/4] fix the definition of IsIntervalOrder

---
 Cslib/Foundations/Relation/Defs.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean
index 9486008df8..d53827dfc4 100644
--- a/Cslib/Foundations/Relation/Defs.lean
+++ b/Cslib/Foundations/Relation/Defs.lean
@@ -163,6 +163,7 @@ the definition below is a sufficient and necessary condition for a relation `r`
 a representation by closed intervals on the real line such that `r i1 i2` iff the right
 endpoint of `i1` is less than the left endpoint of `i2`. -/
 def IsIntervalOrder (r : α → α → Prop) : Prop :=
+  IsStrictOrder α r ∧
   ∀ a1 b1 a2 b2, r a1 b1 ∧ r a2 b2 → r a1 b2 ∨ r a2 b1
 
 end Relation