feat(FLP): distributed algorithms for solving the consensus problem

Cslib.lean

@@ -22,6 +22,8 @@ public import Cslib.Computability.Automata.NA.Prod
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
+public import Cslib.Computability.Distributed.FLP.Algorithm
+public import Cslib.Computability.Distributed.FLP.Consensus
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero

Cslib/Computability/Distributed/FLP/Algorithm.lean

@@ -0,0 +1,239 @@
+/-
+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.Semantics.LTS.OmegaExecution
+
+/-! # Distributed algorithms for solving the consensus problem
+
+In the consensus problem, each process of a distributed algorithm is given a boolean value
+at the beginning.  Then by exchanging messages asynchronously, they are supposed to agree on
+one of the initial boolean values. This file contains a very general definition of such
+a distributed algorithm.
+
+Borrowing an idea from Leslie Lamport, we allow the LTS defined by such an algorithm to
+"stutter" at any time, in the sense of taking a dummy step without changing the
+global state of the distributed algorithm.  This idea enables us to focus on infinite
+executions alone without loss of generality, because an algorithm that has run out of
+useful steps to take can always take the stuttering step.  Pathological executions in which
+the stuttering step is taken forever when there is useful work to be done are outlawed by
+the fairness assumptions defined in `Consensus.lean`.
+
+The types `P`, `M`, and `S` below are the types of processes (more precisely, process identifiers),
+messages contents, and process states.  Eventually `P` will be assumed to be finite in the form of
+`[Fintype P]`, but that assumption will be added only where necessary.  No assumption whatsoever
+will be made about `M` and `S`.  In particular, they could be infinite.
+-/
+
+@[expose] public section
+
+namespace Cslib.FLP
+
+open Set Sum Multiset
+
+variable {P M S : Type*} [DecidableEq P] [DecidableEq M]
+
+/-- The type of messages that processes send to each other. -/
+@[ext]
+structure Message (P M : Type*) where
+  /-- The destination of a message. -/
+  dest : P
+  /-- The content of the message, where the `Bool` option is used to carry to the
+      initial boolean value to each process. -/
+  msg : Bool ⊕ M
+deriving DecidableEq
+
+/-- The type of a process's local state. -/
+structure ProcState (S : Type*) where
+  /-- The internal state of a process. -/
+  state : S
+  /-- The state component used by a process to signal the boolean value it decides on. -/
+  out : Option Bool
+
+/-- The global state of the distributed algorithm. -/
+structure State (P M S : Type*) where
+  /-- A multiset containing all messages that are in-flight (namely, they have been sent but
+  not yet received). Note that being a multiset implies that the messages are not ordered. -/
+  msgs : Multiset (Message P M)
+  /-- A map giving the local states of all processes. -/
+  proc : P → ProcState S
+
+/-- The specification of a distributed algorithm for solving the consensus problem.
+Note that each field below can depend on a process's identifier (recall that each `Message`
+contains its destination's identifier), so the algorithm is not required to be uniform
+across processes. -/
+structure Algorithm (P M S : Type*) where
+  /-- A map specifying the initial state of each process. -/
+  init : P → S
+  /-- A map specifying how a process changes its internal state upon receiving a message. -/
+  next : Message P M → ProcState S → S
+  /-- A map specifying what messages a process sends out upon receiving a message. -/
+  send : Message P M → ProcState S → Multiset (Message P M)
+  /-- A map specifying the boolean decision a process makes upon receiving a message,
+      where `none` means that no decision is made. -/
+  out : Message P M → ProcState S → Option Bool
+
+/-- The type of labels of the LTS defined by an `Algorithm`, where `some m` denotes
+the reception of message `m` and `none` denotes a stuttering step. -/
+abbrev Action (P M : Type*) := Option (Message P M)
+
+/-- `DestIn ps x` means that if `x ≠ none`, then `x = some m` with `m.dest ∈ ps`. -/
+def DestIn (ps : Set P) : Action P M → Prop
+  | some m => m.dest ∈ ps
+  | none => True
+
+/-- Given `inp : P → Bool`, the initial state of the algorithm `a` contains a single message
+carrying the boolean value `inp p` to each process `p`, where the initial internal state is
+`a.init p` and no decision has been made.  The assumption `[Fintype P]` is made because
+a multiset may contain only finitely many elements. -/
+def Algorithm.start [Fintype P] (a : Algorithm P M S) (inp : P → Bool) : State P M S where
+  msgs := Multiset.map (fun p ↦ ⟨p, inl (inp p)⟩) Finset.univ.val
+  proc := fun p ↦ ⟨a.init p, none⟩
+
+/-- The specification of how the global state of the algorithm changes when a process `p`
+receives a message `m`.  (This function will be used only when such a message `m` exists.)
+Note that once `p` has made a boolean decision in its `out` field, it is not allowed to
+"change its mind" anymore. -/
+def Algorithm.recvMsg (a : Algorithm P M S) (m : Message P M) (s : State P M S) : State P M S :=
+  let p := m.dest
+  { msgs := s.msgs.erase m + a.send m (s.proc p)
+    proc := fun q ↦
+      if q = p then
+        ⟨ a.next m (s.proc p),
+          if (s.proc p).out.isNone then a.out m (s.proc p) else (s.proc p).out ⟩
+      else s.proc q }
+
+/-- The transition relation of the LTS defined by the algorithm `a`.
+Note that the stuttering step is always allowed. -/
+def Algorithm.lts (a : Algorithm P M S) : LTS (State P M S) (Action P M) where
+  Tr s x s' := match x with
+    | some m => m ∈ s.msgs ∧ s' = a.recvMsg m s
+    | none => s' = s
+
+/-- `a.Reachable inp s` means that `s` is a reachable state of `a` given the initial `inp`. -/
+def Algorithm.Reachable [Fintype P]
+    (a : Algorithm P M S) (inp : P → Bool) (s : State P M S) : Prop :=
+  a.lts.CanReach (a.start inp) s
+
+/-- `s.ProcDecided p b` means that process `p` is decided on the boolean value `b`
+in the state `s`. -/
+abbrev State.ProcDecided (s : State P M S) (p : P) (b : Bool) : Prop :=
+  (s.proc p).out = some b
+
+/-- `s.Decided b` means that at least one process is decided on the boolean value `b`
+in the state `s`. -/
+def State.Decided (s : State P M S) (b : Bool) : Prop :=
+  ∃ p, s.ProcDecided p b
+
+/-- `s.Agreed` says that all boolean values decided on in state `s` must agree with each other. -/
+def State.Agreed (s : State P M S) : Prop :=
+  ∀ b b', s.Decided b ∧ s.Decided b' → b = b'
+
+/-- `a.SafeConsensus` says that in any reachable state of `a`, (1) all boolean values decided on
+in that state must agree with each other and (2) that boolean value (if it exists) must be
+one of the boolean values given by `inp` at the beginning.  `a.SafeConsensus` is the minimal
+correctness requirement on `a` and is a safety property (hence its name). -/
+def Algorithm.SafeConsensus [Fintype P] (a : Algorithm P M S) : Prop :=
+  ∀ inp s, a.Reachable inp s → s.Agreed ∧ ∀ b, s.Decided b → ∃ p, inp p = b
+
+namespace Algorithm
+
+variable {a : Algorithm P M S} {inp : P → Bool}
+
+/-- The stuttering step does not change the global state. -/
+theorem tr_none {s s' : State P M S} (h : a.lts.Tr s none s') : s = s' := by
+  grind [Algorithm.lts]
+
+/-- The initial state is reachable. -/
+theorem reachable_start [Fintype P] :
+    a.Reachable inp (a.start inp) := by
+  simp [Algorithm.Reachable, LTS.CanReach.refl]
+
+/-- If `s` is reachable from the initial state and `s'` is reachable from `s`,
+then `s'` is reachable from the initial state. -/
+theorem reachable_stable [Fintype P] {s s' : State P M S}
+    (hr : a.Reachable inp s) (hc : a.lts.CanReach s s') : a.Reachable inp s' := by
+  obtain ⟨xs, _⟩ := hr
+  obtain ⟨xs', _⟩ := hc
+  use xs ++ xs'
+  grind [LTS.MTr.comp]
+
+/-- If `p` is decided on the boolean value `b` in `s` and `s'` is reachable from `s`,
+then `p` is still decided on `b` in `s'`. -/
+theorem procDecided_stable {s s' : State P M S} {p : P} {b : Bool}
+    (hd : s.ProcDecided p b) (hc : a.lts.CanReach s s') : s'.ProcDecided p b := by
+  obtain ⟨xs, h_mtr⟩ := hc
+  induction h_mtr <;> grind [Algorithm.lts, Algorithm.recvMsg]
+
+/-- If at least one process is decided on the boolean value `b` in `s` and `s'` is reachable
+from `s`, then at least one process is still decided on `b` in `s'`. -/
+theorem decided_stable {s s' : State P M S} {b : Bool}
+    (hd : s.Decided b) (hc : a.lts.CanReach s s') : s'.Decided b := by
+  obtain ⟨p, _⟩ := hd
+  use p
+  grind [procDecided_stable]
+
+/-- If `m1` and `m2` are both inflight and they have different destinations,
+then receiving them in either order produces the same end state. -/
+theorem recvMsg_comm {m1 m2 : Message P M} {s : State P M S}
+    (hd : m1.dest ≠ m2.dest) (h1 : m1 ∈ s.msgs) (h2 : m2 ∈ s.msgs) :
+    m2 ∈ (a.recvMsg m1 s).msgs ∧ m1 ∈ (a.recvMsg m2 s).msgs ∧
+    a.recvMsg m2 (a.recvMsg m1 s) = a.recvMsg m1 (a.recvMsg m2 s) := by
+  rw [State.mk.injEq]
+  split_ands
+  · grind [Algorithm.recvMsg, mem_erase_of_ne]
+  · grind [Algorithm.recvMsg, mem_erase_of_ne]
+  · have he1 (x) : (s.msgs.erase m1 + x).erase m2 = (s.msgs.erase m1).erase m2 + x := by
+      grind [erase_add_left_pos, mem_erase_of_ne]
+    have he2 (x) : (s.msgs.erase m2 + x).erase m1 = (s.msgs.erase m1).erase m2 + x := by
+      grind [erase_add_left_pos, mem_erase_of_ne, erase_comm]
+    simp [Algorithm.recvMsg, hd, hd.symm, he1, he2, add_assoc]
+    grind [add_comm]
+  · ext p
+    by_cases h_p1 : p = m1.dest <;> by_cases h_p2 : p = m2.dest <;>
+      simp [Algorithm.recvMsg, h_p1, h_p2, hd, hd.symm]
+
+/-- A diamond property for the transition relation `a.lts.Tr`. -/
+theorem tr_diamond {ps : Set P} {x1 x2 : Action P M} {s s1 s2 : State P M S}
+    (hx1 : DestIn ps x1) (hs1 : a.lts.Tr s x1 s1)
+    (hx2 : DestIn psᶜ x2) (hs2 : a.lts.Tr s x2 s2) :
+    ∃ s', a.lts.Tr s1 x2 s' ∧ a.lts.Tr s2 x1 s' := by
+  cases x1 <;> cases x2 <;> try grind [Algorithm.lts]
+  case some m1 m2 =>
+    have hd : m1.dest ≠ m2.dest := by grind [DestIn]
+    obtain ⟨h_m1, rfl⟩ := hs1
+    obtain ⟨h_m2, rfl⟩ := hs2
+    simp only [Algorithm.lts, exists_eq_right_right]
+    grind [recvMsg_comm (a := a) hd h_m1 h_m2]
+
+/-- A message that is in-flight stays in-flight as long as it is not received
+(finite execution version). -/
+theorem mTr_notRcvd_enabled {s t : State P M S} {xl : List (Action P M)} {m : Message P M}
+    (hst : a.lts.MTr s xl t) (hs : m ∈ s.msgs) (hxl : ¬ some m ∈ xl) : m ∈ t.msgs := by
+  induction hst
+  case refl _ => assumption
+  case stepL s x s1 xl t h_tr h_mtr h_ind =>
+    rcases Option.eq_none_or_eq_some x <;>
+      grind [Algorithm.lts, Algorithm.recvMsg, mem_erase_of_ne]
+
+/-- A message that is in-flight stays in-flight as long as it is not received
+(infinite execution version). -/
+theorem omega_notRcvd_enabled
+    {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} {k : ℕ} {m : Message P M}
+    (he : a.lts.OmegaExecution ss xs) (hm : m ∈ (ss k).msgs) (hn : ∀ j, k ≤ j → xs j ≠ some m) :
+    ∀ j, k ≤ j → m ∈ (ss j).msgs := by
+  intro j h_j
+  obtain ⟨i, rfl⟩ : ∃ i, j = k + i := by use j - k; grind
+  induction i
+  case zero => grind
+  case succ i _ =>
+    rcases Option.eq_none_or_eq_some (xs (k + i)) <;>
+      grind [he (k + i), Algorithm.lts, Algorithm.recvMsg, mem_erase_of_ne]
+
+end Algorithm
+
+end Cslib.FLP

Cslib/Computability/Distributed/FLP/Consensus.lean

@@ -0,0 +1,144 @@
+/-
+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.FLP.Algorithm
+public import Mathlib.Data.Set.Card
+
+/-! # Fault-tolerant consensus
+
+Roughly speaking, a distributed consensus algorithm can tolerate `f` faults if up to `f`
+processes can be "faulty" and yet the non-faulty processes can still reach a consensus.
+The fault we consider here is limited to the crash fault, in which a process stops responding
+to messages from some point onward.  We do not consider Byzantine faults.
+-/
+
+@[expose] public section
+
+namespace Cslib.FLP
+
+open Function Set Multiset Fintype ωSequence
+
+variable {P M S : Type*}
+
+/-- A process `p` is faulty in an infinite execution iff there is a time `k` from which onward
+there is a message in-flight to `p` but `p` has stopped receiving messages. -/
+def ProcFaulty (p : P) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop :=
+  ∃ k, (∃ m, m ∈ (ss k).msgs ∧ m.dest = p) ∧ ∀ j, k ≤ j → ∀ m', xs j = some m' → m'.dest ≠ p
+
+/-- A process `p` is fair in an infinite execution iff every message in-flight to `p` is
+received by `p`. -/
+def ProcFair (p : P) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop :=
+  ∀ m, m.dest = p → ∀ k, m ∈ (ss k).msgs → ∃ j, k ≤ j ∧ xs j = some m
+
+/-- A process `p` cannot be both faulty and fair in an infinite execution.  Note, however, that
+it is possible for `p` to be neither faulty nor fair, because `p` can keep on receiving messages
+but at the same time keep ignoring some messages sent to it. -/
+theorem not_procFaulty_and_procFair (p : P)
+    (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) :
+    ¬ (ProcFaulty p ss xs ∧ ProcFair p ss xs) := by
+  grind [ProcFaulty, ProcFair]
+
+/-- An infinite execution is fair iff every process is either faulty or fair
+(cf. the comment for the theorem `not_procFaulty_and_procFair`). -/
+def FairRun (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop :=
+  ∀ p, ProcFaulty p ss xs ∨ ProcFair p ss xs
+
+/-- The number of faulty processes in an infinite execution. -/
+noncomputable def numProcFaulty (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : ℕ :=
+  {p | ProcFaulty p ss xs}.ncard
+
+/-- If the number of faulty processes in an infinite execution is less than the total number
+of processes, then at least one process is not faulty. -/
+theorem not_procFaulty_of_numProcFaulty [Fintype P]
+    {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)}
+    (h : numProcFaulty ss xs < card P) : ∃ p, ¬ ProcFaulty p ss xs := by
+  let nf := {p | ProcFaulty p ss xs}ᶜ
+  have h1 : 0 < nf.ncard := by
+    rw [ncard_compl]
+    grind [numProcFaulty, card_eq_nat_card]
+  obtain ⟨p, _⟩ := (ncard_pos (s := nf)).mp h1
+  grind
+
+/-- If every process in a set `ps` is fair, then the number of faulty processes is bounded by
+the total number of processes minus the cardinality of `ps`. -/
+theorem numProcFaulty_le_not_procFair [Fintype P]
+    {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} {ps : Set P}
+    (h : ∀ p, p ∈ ps → ProcFair p ss xs) : numProcFaulty ss xs ≤ card P - ps.ncard := by
+  rw [numProcFaulty, card_eq_nat_card, ← ncard_compl]
+  suffices h1 : {p | ProcFaulty p ss xs} ⊆ psᶜ by exact ncard_le_ncard h1
+  grind [not_procFaulty_and_procFair]
+
+variable [DecidableEq P] [DecidableEq M]
+
+/-- The notion of an infinite admissible execution for an algorithm `a` with input `inp`
+and containing at most `f` faulty processes. -/
+def Algorithm.AdmissibleRun [Fintype P] (a : Algorithm P M S) (inp : P → Bool) (f : ℕ)
+    (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop :=
+  ss 0 = a.start inp ∧ a.lts.OmegaExecution ss xs ∧
+  FairRun ss xs ∧ numProcFaulty ss xs ≤ f
+
+/-- A process terminates in an infinite execution iff either it crashes or it decides on
+a boolean value at some point. -/
+def ProcTermination (p : P) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop :=
+  ProcFaulty p ss xs ∨ ∃ k b, (ss k).ProcDecided p b
+
+/-- An algorithm `a` terminates with up to `f` faulty processes iff all its processes terminate
+in every infinite admissible execution containing at most `f` faulty processes. -/
+def Algorithm.Termination [Fintype P] (a : Algorithm P M S) (f : ℕ) : Prop :=
+  ∀ inp ss xs, a.AdmissibleRun inp f ss xs → ∀ p, ProcTermination p ss xs
+
+/-- An algorithm `a` is a consensus algorithm tolerating up to `f` faulty processes iff
+it both satisfies the consensus safety property `a.SafeConsensus` and terminates
+with up to `f` faulty processes. -/
+def Algorithm.Consensus [Fintype P] (a : Algorithm P M S) (f : ℕ) : Prop :=
+  a.SafeConsensus ∧ a.Termination f
+
+variable {a : Algorithm P M S} {inp : P → Bool}
+
+/-- If an infinite execution is admissible with up tp `f` faulty processes,
+then it is also admissible with with up tp `f' ≥ f` faulty processes. -/
+theorem AdmissibleRun.fault_mono [Fintype P] {f f' : ℕ}
+    {xs : ωSequence (Action P M)} {ss : ωSequence (State P M S)}
+    (hle : f ≤ f') (ha : a.AdmissibleRun inp f ss xs) : a.AdmissibleRun inp f' ss xs := by
+  grind [Algorithm.AdmissibleRun]
+
+/-- If `a` is a consensus algorithm tolerating up to `f` faulty processes,
+then it is also a consensus algorithm tolerating up to `f' ≤ f` faulty processes. -/
+theorem Consensus.fault_mono [Fintype P] {f f' : ℕ}
+    (hle : f ≥ f') (hc : a.Consensus f) : a.Consensus f' := by
+  obtain ⟨h_sc, h_f⟩ := hc
+  use h_sc
+  intro inp
+  grind [h_f inp, AdmissibleRun.fault_mono]
+
+/-- If a process `p` is not fair in an infinite execution of an algorithm `a`, then there is
+a message that is in-flight to, but never received, by `p` from some point onward. -/
+theorem Algorithm.not_fair_stay_enabled
+    {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} {p : P}
+    (he : a.lts.OmegaExecution ss xs) (hnf : ¬ ProcFair p ss xs) :
+    ∃ m, m.dest = p ∧ ∃ k, m ∈ (ss k).msgs ∧ ∀ j, k ≤ j → m ∈ (ss j).msgs ∧ (xs j) ≠ some m := by
+  simp only [ProcFair, not_forall, not_exists, not_and] at hnf
+  grind only [omega_notRcvd_enabled]
+
+/-- In an infinite execution of an algorithm `a`, a process `p` is fair iff `p` is fair in
+all suffixes of the execution. -/
+theorem Algorithm.drop_procFair_iff
+    {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)}
+    (he : a.lts.OmegaExecution ss xs) (p : P) (n : ℕ) :
+    ProcFair p (ss.drop n) (xs.drop n) ↔ ProcFair p ss xs := by
+  constructor <;> intro h
+  · by_contra h_contra
+    obtain ⟨m, h_m, k, h_k, h_ge⟩ := Algorithm.not_fair_stay_enabled he h_contra
+    have := h m h_m k
+    grind
+  · intro m h_m k h_k
+    obtain ⟨j, _, _⟩ := h m h_m (n + k) (by grind)
+    use j - n
+    grind
+
+end Cslib.FLP