Asynchronous distributed consensus in the absence of faults

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 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 FLP impossibility result, but do show that the notion of an Algorithm is not vacuous, in the sense that it allows a working asynchronous consensus algorithm when there is no fault.

@[reducible, inline]

abbrev Cslib.FLP.ZeroFaultAlg.M : Type

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).

Equations

• Cslib.FLP.ZeroFaultAlg.M = Bool

@[reducible, inline]

abbrev Cslib.FLP.ZeroFaultAlg.S : Type

The local state of a process is trivial.

Equations

• Cslib.FLP.ZeroFaultAlg.S = Unit

def Cslib.FLP.ZeroFaultAlg.alg {n : ℕ} (npos : 0 < n) : Algorithm (Fin n) M S

alg is the asynchronous distributed consensus algorithm described above.

Equations

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

def Cslib.FLP.ZeroFaultAlg.Inv {n : ℕ} (npos : 0 < n) (inp : Fin n → Bool) (s : State (Fin n) M S) : Prop

Inv is an invariant for alg.

Equations

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

theorem Cslib.FLP.ZeroFaultAlg.inv_start {n : ℕ} (npos : 0 < n) (inp : Fin n → Bool) : Inv npos inp ((alg npos).start inp)

Inv is true at any initial state.

theorem Cslib.FLP.ZeroFaultAlg.inv_tr_left {n : ℕ} (npos : 0 < n) (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 = true) : (t.msgs = s.msgs.erase m + if m.dest = ⟨0, npos⟩ then Multiset.map (fun (p : Fin n) => { dest := p, msg := Sum.inr (inp ⟨0, npos⟩) }) Finset.univ.val else 0) ∧ ∀ (p : Fin n), (t.proc p).out = (s.proc p).out

What happens when an inl message is received.

theorem Cslib.FLP.ZeroFaultAlg.inv_tr_right {n : ℕ} (npos : 0 < n) (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 = true) : t.msgs = s.msgs.erase m ∧ (t.proc m.dest).out = some (inp ⟨0, npos⟩) ∧ ∀ (p : Fin n), p ≠ m.dest → (t.proc p).out = (s.proc p).out

What happens when an inr message is received.

theorem Cslib.FLP.ZeroFaultAlg.trInv_inv {n : ℕ} (npos : 0 < n) (inp : Fin n → Bool) : (alg npos).lts.TrInv (Inv npos inp)

The truth of Inv is preserved by every transition of alg.

theorem Cslib.FLP.ZeroFaultAlg.reachable_inv {n : ℕ} (npos : 0 < n) (inp : Fin n → Bool) {s : State (Fin n) M S} (hr : (alg npos).Reachable inp s) : Inv npos inp s

Inv is true in all reachable state of alg.

theorem Cslib.FLP.ZeroFaultAlg.safeConsensus {n : ℕ} (npos : 0 < n) : (alg npos).SafeConsensus

alg satisfies the SafeConsensus property.

theorem Cslib.FLP.ZeroFaultAlg.always_inv {n : ℕ} (npos : 0 < n) (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)

Inv is true at every state in an admissible run of alg.

theorem Cslib.FLP.ZeroFaultAlg.init_left {n : ℕ} (npos : 0 < n) (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 : State (Fin n) M S | { dest := ⟨0, npos⟩, msg := Sum.inl (inp ⟨0, npos⟩) } ∈ s.msgs}

The message carrying the input value for process 0 is enabled in the initial state.

theorem Cslib.FLP.ZeroFaultAlg.left_leadsTo_right {n : ℕ} (npos : 0 < n) (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 : State (Fin n) M S | { dest := ⟨0, npos⟩, msg := Sum.inl (inp ⟨0, npos⟩) } ∈ s.msgs} {s : State (Fin n) M S | { dest := p, msg := Sum.inr (inp ⟨0, npos⟩) } ∈ s.msgs}

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 Cslib.FLP.ZeroFaultAlg.right_leadsTo_out {n : ℕ} (npos : 0 < n) (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 : State (Fin n) M S | { dest := p, msg := Sum.inr (inp ⟨0, npos⟩) } ∈ s.msgs} {s : State (Fin n) M S | (s.proc p).out = some (inp ⟨0, npos⟩)}

Whenever a message carrying a value sent by process 0 is enabled at a process p, p eventually decides on that value.

theorem Cslib.FLP.ZeroFaultAlg.consensus_zero {n : ℕ} (npos : 0 < n) : (alg npos).Consensus 0

alg is a correct asynchronous distributed consensus algorithm when there is no fault.