ctchou · Sep 23, 2026 · Sep 30, 2026 · Sep 30, 2026 · Sep 30, 2026 · Oct 1, 2026
@@ -57,6 +57,8 @@ public import Cslib.Computability.Circuit.Signature
 public import Cslib.Computability.Circuit.Simulation
 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

@@ -0,0 +1,150 @@
+/-
+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 proofs of Lemma 5.1 and 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]
+      have := (a.so_strict_total_order s).trichotomous ⟨x, h1⟩ ⟨y, h_se⟩
+      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) : a.hb ≤ TransGen a.vis := by
+  apply TransGen.mono
+  rintro x y (_ | ⟨s, _⟩)
+  · assumption
+  · apply h s
+    assumption
+
+lemma singleOrder_readMyWrites_imp_causalArbitration
+    (h1 : a.SingleOrder) (h2 : a.ReadMyWrites) : a.CausalArbitration := by
+--  intro s
+  suffices TransGen a.vis ≤ a.ar by grind [CausalArbitration, readMyWrites_imp_hb_le_trans_vis h2]
+  have h_ar : TransGen a.ar = a.ar := by exact transGen_eq_self
+  rw [← h_ar]
+  apply TransGen.mono
+  obtain ⟨_, _, _⟩ := h1
+  intro _ _ _
+  grind
+
+lemma causalVisibility_imp_readMyWrites
+    (h : a.CausalVisibility) : a.ReadMyWrites := by
+  intro s x y h_so
+  exact h x y <| TransGen.single (Or.inr ⟨s, h_so⟩)
+
+lemma causalVisibility_imp_monotonicReads
+    (h : a.CausalVisibility) : a.MonotonicReads := by
+  intro s x y z h_vis h_so
+  exact h x z <| TransGen.tail (TransGen.single (Or.inl h_vis)) (Or.inr ⟨s, h_so⟩)
+
+lemma causalVisibility_imp_noCircularCausality
+    (h : a.CausalVisibility) : a.NoCircularCausality :=
+  acyclic_le h a.vis_acyclic
+
+lemma singleOrder_readMyWrites_imp_causalVisibility
+    (h1 : a.SingleOrder) (h2 : a.ReadMyWrites) : a.CausalVisibility := by
+  suffices TransGen a.vis ≤ a.vis by grind [CausalVisibility, readMyWrites_imp_hb_le_trans_vis h2]
+  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]
+
+theorem causalConsistency_imp_basicEventualConsistency
+    (h : a.CausalConsistency d) : a.BasicEventualConsistency d := by
+  grind [CausalConsistency, BasicEventualConsistency,
+    Causality, causalVisibility_imp_noCircularCausality]
+
+end Cslib.DistributedConsistency
@@ -0,0 +1,234 @@
+/-
+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,
+
+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.
+
+NOTE: We left out the definition of quiescent consistency, for two reasons:
+* Quiescent consistency is too weak a notion to be practically useful (see the remark
+  on page 44 of [Burckhardt2014]).
+* We found during the process of formalization that the only theoretic result about
+  quiescent consistency in [Burckhardt2014], that it is implied by causal consistency,
+  is incorrect given the definitions in [Burckhardt2014].
+
+## 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, IsStrictTotalOrder {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 transitive closure of the union of the `vis` order
+and the `so s` orders for all sessions `s`. -/
+def hb (a : AbstractExecution Event Operation Value Session) : Event → Event → Prop :=
+  TransGen fun x y ↦ a.vis x y ∨ ∃ s, a.so s x y
+
+/-- `NoCircularCausality` says that the `hb` order is acyclic. -/
+def NoCircularCausality (a : AbstractExecution Event Operation Value Session) : Prop :=
+  Acyclic a.hb
+
+/-- `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 :=
+  a.hb ≤ 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 :=
+  a.hb ≤ 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
+
+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
+
+end AbstractExecution
+
+end Cslib.DistributedConsistency