Fault-tolerant pseudo-consensus

A central idea of [Vol04] is the notion of pseudo-consensus, which weakens the notion of consensus by replacing the requirement of termination, which is stated in terms of infinite executions, by that of pseudo-termination, which is stated in terms of finite executions. This makes the notion of pseudo-consensus easier to work with than consensus. This file defines pseudo-consensus and proves that it is implied by consensus. This result is intuitively obvious and is stated without proof in [Vol04], but it turns out to require quite a bit of formal machinery to prove.

def Cslib.FLP.Algorithm.PseudoTermination {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (f : ℕ) : Prop

An algorithm a satisfies f-tolerant pseudo-termination iff for every reachable state s of a and every ps of at least card P - f processes, there exists a state s' reachable from s using only messages with destinations in ps which has decided on a boolean value. In other words, from any reachable state of a, a decision can be made without the participation of at most f processes.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.FLP.Algorithm.PseudoConsensus {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (f : ℕ) : Prop

An algorithm a is a pseudo-consensus algorithm tolerating up to f faults iff it satisfies both the consensus safety property a.SafeConsensus and f-tolerant pseudo-termination.

Equations

• a.PseudoConsensus f = (a.SafeConsensus ∧ a.PseudoTermination f)

noncomputable def Cslib.FLP.Algorithm.simpleDeliver {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (ps : Set P) : DeliverMsg P M S

a.simpleDeliver ps delivers any message that is in-flight and has its destination in ps.

Equations

• a.simpleDeliver ps s m = if m ∈ s.msgs ∧ m.dest ∈ ps then ([some m], a.recvMsg m s) else ([], s)

theorem Cslib.FLP.PseudoConsensus.simpleDeliver_fair {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} (ps : Set P) : a.FairDeliverMsg (a.simpleDeliver ps) ps fun (x : State P M S) => True

theorem Cslib.FLP.PseudoConsensus.simpleDeliver_forallActions {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} (ps : Set P) : (a.simpleDeliver ps).ForallActions (DestIn ps)

theorem Cslib.FLP.PseudoConsensus.of_consensus {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (f : ℕ) (hf : f < Fintype.card P) (hc : a.Consensus f) : a.PseudoConsensus f

If an algorithm a is a consensus algorithm tolerating up to f faults, then a is also a pseudo-consensus algorithm tolerating up to f faults. The main difficulty in the proof of this theorem is that we need to construct an infinite admissible execution starting from any reachable state of a using any subset of non-faulty processes. This is achieved using the fair scheduler developed in FairSchedular.lean.