From 0913705141951f4e4b07d02a7d5e899351c7ce75 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Wed, 3 Jun 2026 18:07:55 -0700 Subject: [PATCH 1/2] feat(FLP): show that distributed consensus is possible when there is no fault --- Cslib.lean | 1 + .../Distributed/FLP/Consensus.lean | 15 ++ Cslib/Computability/Distributed/FLP/README.md | 7 +- .../Distributed/FLP/ZeroConsensus.lean | 171 ++++++++++++++++++ Cslib/Foundations/Semantics/LTS/Basic.lean | 16 ++ 5 files changed, 209 insertions(+), 1 deletion(-) create mode 100644 Cslib/Computability/Distributed/FLP/ZeroConsensus.lean diff --git a/Cslib.lean b/Cslib.lean index c0269e0bb..c31318ca0 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -24,6 +24,7 @@ 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.Distributed.FLP.ZeroConsensus public import Cslib.Computability.Languages.Congruences.BuchiCongruence public import Cslib.Computability.Languages.Congruences.RightCongruence public import Cslib.Computability.Languages.ExampleEventuallyZero diff --git a/Cslib/Computability/Distributed/FLP/Consensus.lean b/Cslib/Computability/Distributed/FLP/Consensus.lean index b7209ed90..e83ee2aab 100644 --- a/Cslib/Computability/Distributed/FLP/Consensus.lean +++ b/Cslib/Computability/Distributed/FLP/Consensus.lean @@ -100,6 +100,21 @@ def Algorithm.Consensus [Fintype P] (a : Algorithm P M S) (f : ℕ) : Prop := variable {a : Algorithm P M S} {inp : P → Bool} +/-- Specialize the definition of `Algorithm.AdmissibleRun` to the case of zero fault. -/ +theorem AdmissibleRun.fault_zero [Fintype P] + {xs : ωSequence (Action P M)} {ss : ωSequence (State P M S)} : + a.AdmissibleRun inp 0 ss xs ↔ + ss 0 = a.start inp ∧ a.lts.OmegaExecution ss xs ∧ ∀ p, ProcFair p ss xs := by + constructor + · rintro ⟨_, _, _, hf⟩ + suffices ∀ p, ¬ ProcFaulty p ss xs by grind [FairRun, not_procFaulty_and_procFair] + simp (disch := toFinite_tac) [numProcFaulty, ncard_eq_zero, Set.ext_iff] at hf + assumption + · rintro ⟨hi, hr, _⟩ + use hi, hr, by grind [FairRun] + have : ∀ p, ¬ ProcFaulty p ss xs := by grind [not_procFaulty_and_procFair] + simpa (disch := toFinite_tac) [numProcFaulty, ncard_eq_zero, Set.ext_iff] + /-- 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' : ℕ} diff --git a/Cslib/Computability/Distributed/FLP/README.md b/Cslib/Computability/Distributed/FLP/README.md index 7bc8e7bd3..309a8325a 100644 --- a/Cslib/Computability/Distributed/FLP/README.md +++ b/Cslib/Computability/Distributed/FLP/README.md @@ -32,11 +32,16 @@ consensus is impossible in the presence of even a single crash fault. which doesn't contain any fault but never reaches a consensus, which then implies that there cannot be a consensus algorithm that can tolerate even a single fault. +8. `ZeroConsensus.lean` presents a simple distributed consensus algorithm and proves that it achieves + consensus if there is no fault. This file is not needed for proving the impossibility result, but is + included to show that the notion of an algorithm defined in `Algorithm.lean` is not vacuous, in the + sense that it allows a working consensus algorithm when there is no fault. + Files #1 and #2 contains materials common to both [FLP1985] and [Volzer2004]. File #3 provides proof details that are either completely omitted (in the case of `PseudoConsensus.of_consensus`) or only hinted at (in the case of `OnePseudoConsensus.fair_nonUniform`) in [Volzer2004]. -The remaining files follow the development in [Volzer2004] fairly closely, +The remaining files (except #8) follow the development in [Volzer2004] fairly closely, as is explained further in each file. ## References diff --git a/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean b/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean new file mode 100644 index 000000000..dec83d07c --- /dev/null +++ b/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean @@ -0,0 +1,171 @@ +/- +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.Consensus +public import Cslib.Foundations.Data.OmegaSequence.Temporal + +/-! # Distributed consensus in the absence of faults + +This file presents a simple distributed consensus algorithm and proves that it does achieve +consensus if there is no fault. Assume that there are `n` processes numbered 0, 1, ..., `n - 1`. +The algorithm works as follows: +(1) Process 0 receives its input value and sends that value to all processes (including itself). + All other processes ignore their inputs. +(2) Upon receiving the value sent by process 0 in the previpus step, every process (including + process 0) decides on that value. +Clearly, if there is no fault and all messages are eventually delivered, every process will +eventually decide on the same value, namely, the input value at process 0. + +The contents of this file are not needed for proving the impossibility result, but do show +that the notion of an `Algorithm` is not vacuous, in the sense that it allows a working +consensus algorithm when there is no fault. +-/ + +@[expose] public section + +namespace Cslib.FLP.ZeroFaultAlg + +open Set Sum Option Multiset ωSequence + +/-- The payload of a message is of type `Bool ⊕ Bool`, where `inl b` denotes an input value `b` +ane `inr b` denotes a value `b` sent by process 0 to all processes (including itself). -/ +abbrev M := Bool + +/-- The local state of a process is trivial. -/ +abbrev S := Unit + +variable {n : ℕ} (npos : 0 < n) + +/-- `alg` is the distributed consensus algorithm described in the main comment above. -/ +def alg : Algorithm (Fin n) M S where + init _ := () + next _ _ := () + send m _ := match m.msg with + | inl b => + if m.dest = ⟨0, npos⟩ then Multiset.map (fun p ↦ ⟨p, inr b⟩) Finset.univ.val else 0 + | inr _ => 0 + out m _ := match m.msg with + | inl _ => none + | inr b => some b + +/-- `Inv` is an invariant for `alg`. -/ +def Inv (inp : Fin n → Bool) (s : State (Fin n) M S) : Prop := + (∀ m, m ∈ s.msgs → m.msg = inl (inp m.dest) ∨ m.msg = inr (inp ⟨0, npos⟩)) ∧ + (∀ p, (s.proc p).out = none ∨ (s.proc p).out = some (inp ⟨0, npos⟩)) + +/-- `Inv` is true at any initial state. -/ +theorem inv_start (inp : Fin n → Bool) : + Inv npos inp ((alg npos).start inp) := by + simp [alg, Inv, Algorithm.start] + +/-- What happens when an `inl` message is received. -/ +theorem inv_tr_left (inp : Fin n → Bool) {s t : State (Fin n) M S} {m : Message (Fin n) M} + (hs : Inv npos inp s) (htr : (alg npos).lts.Tr s (some m) t) (hm : m.msg.isLeft) : + t.msgs = s.msgs.erase m + + ( if m.dest = ⟨0, npos⟩ then Multiset.map (fun p ↦ ⟨p, inr (inp ⟨0, npos⟩)⟩) Finset.univ.val + else 0 ) ∧ + ∀ p, (t.proc p).out = (s.proc p).out := by + simp only [alg] at htr + split_ands <;> grind [Inv, Algorithm.lts, Algorithm.recvMsg] + +/-- What happens when an `inr` message is received. -/ +theorem inv_tr_right (inp : Fin n → Bool) {s t : State (Fin n) M S} {m : Message (Fin n) M} + (hs : Inv npos inp s) (htr : (alg npos).lts.Tr s (some m) t) (hm : m.msg.isRight) : + t.msgs = s.msgs.erase m ∧ (t.proc m.dest).out = some (inp ⟨0, npos⟩) ∧ + ∀ p, p ≠ m.dest → (t.proc p).out = (s.proc p).out := by + simp only [alg] at htr + grind [Inv, Algorithm.lts, Algorithm.recvMsg] + +/-- The truth of `Inv` is preserved by every transition of `alg`. -/ +theorem trInv_inv (inp : Fin n → Bool) : (alg npos).lts.TrInv (Inv npos inp) := by + intro s x t htr hs + rcases eq_none_or_eq_some x with _ | ⟨m, rfl⟩ + · grind [Algorithm.lts] + · have h1 : m.msg = inl (inp m.dest) ∨ m.msg = inr (inp ⟨0, npos⟩) := by + grind [Inv, Algorithm.lts] + rcases h1 + · have := inv_tr_left npos inp hs htr + grind [Inv, erase_le, mem_of_le, Multiset.mem_map] + · have := inv_tr_right npos inp hs htr + grind [Inv, erase_le, mem_of_le] + +/-- `Inv` is true in all reachable state of `alg`. -/ +theorem reachable_inv (inp : Fin n → Bool) {s : State (Fin n) M S} + (hr : (alg npos).Reachable inp s) : Inv npos inp s := by + obtain ⟨xs, _⟩ := hr + have := LTS.mtrInv_of_trInv <| trInv_inv npos inp + grind [LTS.MTrInv, inv_start npos inp] + +/-- `alg` satisfies the `SafeConsensus` property. -/ +theorem safeConsensus : (alg npos).SafeConsensus := by + intro inp s hr + grind [reachable_inv npos inp hr, Inv, State.Agreed, State.Decided] + +/-- `Inv` is true at every state in an admissible run of `alg`. -/ +theorem always_inv (inp : Fin n → Bool) + {ss : ωSequence (State (Fin n) M S)} {xs : ωSequence (Action (Fin n) M)} + (ha : (alg npos).AdmissibleRun inp 0 ss xs) (k : ℕ) : Inv npos inp (ss k) := by + apply reachable_inv + apply Algorithm.reachable_stable <| Algorithm.reachable_start + use xs.extract 0 k + grind [AdmissibleRun.fault_zero, LTS.OmegaExecution.extract_mTr] + +/-- The message carrying the input value for process 0 is enabled in the initial state. -/ +theorem init_left (inp : Fin n → Bool) + {ss : ωSequence (State (Fin n) M S)} {xs : ωSequence (Action (Fin n) M)} + (ha : (alg npos).AdmissibleRun inp 0 ss xs) : + ss 0 ∈ {s | ⟨⟨0, npos⟩, inl (inp ⟨0, npos⟩)⟩ ∈ s.msgs} := by + obtain ⟨hi, _, _⟩ := AdmissibleRun.fault_zero.mp ha + simp [hi, Algorithm.start] + +/-- Whenever the message carrying the input value for process 0 is enabled in a state, +a message carrying that value is eventually sent to every process `p` by process 0. -/ +theorem left_leadsTo_right (inp : Fin n → Bool) + {ss : ωSequence (State (Fin n) M S)} {xs : ωSequence (Action (Fin n) M)} + (ha : (alg npos).AdmissibleRun inp 0 ss xs) (p : Fin n) : + ss.LeadsTo {s | ⟨⟨0, npos⟩, inl (inp ⟨0, npos⟩)⟩ ∈ s.msgs} + {s | ⟨p, inr (inp ⟨0, npos⟩)⟩ ∈ s.msgs} := by + let m : Message (Fin n) M := ⟨⟨0, npos⟩, inl (inp ⟨0, npos⟩)⟩ + intro k _ + have : m ∈ (ss k).msgs := by grind + obtain ⟨_, _, hf⟩ := AdmissibleRun.fault_zero.mp ha + obtain ⟨j, _, _⟩ : ∃ j, k ≤ j ∧ xs j = some m := by grind [hf ⟨0, npos⟩, ProcFair] + use j + 1 + have hj := always_inv npos inp ha j + have htr : (alg npos).lts.Tr (ss j) (some m) (ss (j + 1)) := by grind [LTS.OmegaExecution] + have h1 : k ≤ j + 1 := by grind + simp [h1, m, inv_tr_left npos inp hj htr rfl] + +/-- Whenever a message carrying a value sent by process 0 is enabled at a process `p`, +`p` eventually decides on that value. -/ +theorem right_leadsTo_out (inp : Fin n → Bool) + {ss : ωSequence (State (Fin n) M S)} {xs : ωSequence (Action (Fin n) M)} + (ha : (alg npos).AdmissibleRun inp 0 ss xs) (p : Fin n) : + ss.LeadsTo {s | ⟨p, inr (inp ⟨0, npos⟩)⟩ ∈ s.msgs} + {s | (s.proc p).out = some (inp ⟨0, npos⟩)} := by + let m : Message (Fin n) M := ⟨p, inr (inp ⟨0, npos⟩)⟩ + intro k _ + have : m ∈ (ss k).msgs := by grind + obtain ⟨_, _, hf⟩ := AdmissibleRun.fault_zero.mp ha + obtain ⟨j, _, _⟩ : ∃ j, k ≤ j ∧ xs j = some m := by grind [hf p, ProcFair] + use j + 1 + have hj := always_inv npos inp ha j + have htr : (alg npos).lts.Tr (ss j) (some m) (ss (j + 1)) := by grind [LTS.OmegaExecution] + grind [inv_tr_right npos inp hj htr] + +/-- `alg` is a correct consensus algorithm when there is no fault. -/ +theorem consensus_zero : (alg npos).Consensus 0 := by + use safeConsensus npos + intro inp ss xs ha p + right + have hlt1 := left_leadsTo_right npos inp ha p + have hlt2 := right_leadsTo_out npos inp ha p + have := leadsTo_trans hlt1 hlt2 0 <| init_left npos inp ha + grind + +end Cslib.FLP.ZeroFaultAlg diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 0f5686502..b273f238c 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -134,6 +134,22 @@ theorem MTr.nil_eq (h : lts.MTr s1 [] s2) : s1 = s2 := by cases h rfl +/-- Single-step invariant. -/ +@[scoped grind =] +def TrInv (p : State → Prop) : Prop := + ∀ s1 μ s2, lts.Tr s1 μ s2 → p s1 → p s2 + +/-- Multistep invariant. -/ +@[scoped grind =] +def MTrInv (p : State → Prop) : Prop := + ∀ s1 μs s2, lts.MTr s1 μs s2 → p s1 → p s2 + +/-- Any single-step invariant is also a multistep invariant. -/ +theorem mtrInv_of_trInv {lts : LTS State Label} {p : State → Prop} + (htr : lts.TrInv p) : lts.MTrInv p := by + intro s1 μs s2 h + induction h <;> grind + /-- A state `s1` can reach a state `s2` if there exists a multistep transition from `s1` to `s2`. -/ @[scoped grind =] From ed2b272e10ef4438d9e36fe301d0b8aa986d77aa Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sun, 7 Jun 2026 14:12:23 -0700 Subject: [PATCH 2/2] Incorporate Shreyas Srinivas's comment --- .../Distributed/FLP/ZeroConsensus.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean b/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean index dec83d07c..96d885a87 100644 --- a/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean +++ b/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean @@ -9,21 +9,21 @@ module public import Cslib.Computability.Distributed.FLP.Consensus public import Cslib.Foundations.Data.OmegaSequence.Temporal -/-! # Distributed consensus in the absence of faults +/-! # Asynchronous distributed consensus in the absence of faults -This file presents a simple distributed consensus algorithm and proves that it does achieve -consensus if there is no fault. Assume that there are `n` processes numbered 0, 1, ..., `n - 1`. +This file presents an asynchronous distributed consensus algorithm and proves that it does achieve +consensus when there is no fault. Assume that there are `n` processes numbered 0, 1, ..., `n - 1`. The algorithm works as follows: (1) Process 0 receives its input value and sends that value to all processes (including itself). - All other processes ignore their inputs. + All other processes ignore their inputs upon receiving them. (2) Upon receiving the value sent by process 0 in the previpus step, every process (including process 0) decides on that value. Clearly, if there is no fault and all messages are eventually delivered, every process will eventually decide on the same value, namely, the input value at process 0. -The contents of this file are not needed for proving the impossibility result, but do show +The contents of this file are not needed for proving the FLP impossibility result, but do show that the notion of an `Algorithm` is not vacuous, in the sense that it allows a working -consensus algorithm when there is no fault. +asynchronous consensus algorithm when there is no fault. -/ @[expose] public section @@ -41,7 +41,7 @@ abbrev S := Unit variable {n : ℕ} (npos : 0 < n) -/-- `alg` is the distributed consensus algorithm described in the main comment above. -/ +/-- `alg` is the asynchronous distributed consensus algorithm described above. -/ def alg : Algorithm (Fin n) M S where init _ := () next _ _ := () @@ -158,7 +158,7 @@ theorem right_leadsTo_out (inp : Fin n → Bool) have htr : (alg npos).lts.Tr (ss j) (some m) (ss (j + 1)) := by grind [LTS.OmegaExecution] grind [inv_tr_right npos inp hj htr] -/-- `alg` is a correct consensus algorithm when there is no fault. -/ +/-- `alg` is a correct asynchronous distributed consensus algorithm when there is no fault. -/ theorem consensus_zero : (alg npos).Consensus 0 := by use safeConsensus npos intro inp ss xs ha p