1-tolerant pseudo-consensus

This file develops the theory of pseudo-consensus algorithms that can tolerate up to 1 fault. It formalizes section 3 of [Vol04] except Theorem 1.

def Cslib.FLP.Algorithm.CanDecideWithout {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (s : State P M S) (p : P) (b : Bool) : Prop

a.CanDecideWithout s p b means that the boolean value b is decided on in a state that is reachable from s without the participation of p. In the notation of [Vol04], this is equivalent to b ∈ val(p,s).

Equations

• a.CanDecideWithout s p b = ∃ (s' : Cslib.FLP.State P M S), a.CanReachVia {p}ᶜ s s' ∧ s'.Decided b

def Cslib.FLP.Algorithm.Uniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (s : State P M S) (b : Bool) : Prop

a.Uniform s b means that for every process p, a.CanDecideWithout s p b but not a.CanDecideWithout s p !b.

Equations

• a.Uniform s b = ∀ (p : P), a.CanDecideWithout s p b ∧ ¬a.CanDecideWithout s p !b

def Cslib.FLP.Algorithm.NonUniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (s : State P M S) : Prop

a.NonUniform s means that for each boolean value b, there is a process p such that a.CanDecideWithout s p b.

Equations

• a.NonUniform s = ∀ (b : Bool), ∃ (p : P), a.CanDecideWithout s p b

theorem Cslib.FLP.OnePseudoConsensus.pseudoTermination {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] (hpc1 : a.PseudoConsensus 1) {s : State P M S} (hr : a.Reachable inp s) (p : P) : ∃ (s' : State P M S) (b : Bool), a.CanReachVia {p}ᶜ s s' ∧ s'.Decided b

Draw a consequence of a.PseudoConsensus 1.

theorem Cslib.FLP.OnePseudoConsensus.canDecideWithout_exists {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] (hpc1 : a.PseudoConsensus 1) {s : State P M S} (hr : a.Reachable inp s) (p : P) : ∃ (b : Bool), a.CanDecideWithout s p b

Assuming a.PseudoConsensus 1, for any reachable state of a and for any process p, there is a boolean value b such that a.CanDecideWithout s p b. This theorem formalizes Proposition 2(a) of [Vol04].

theorem Cslib.FLP.OnePseudoConsensus.not_uniform_and_nonUniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {s : State P M S} (b : Bool) : ¬(a.Uniform s b ∧ a.NonUniform s)

A state cannot be both uniform and non-uniform.

theorem Cslib.FLP.OnePseudoConsensus.uniform_or_nonUniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] (hpc1 : a.PseudoConsensus 1) {s : State P M S} (hr : a.Reachable inp s) : a.Uniform s false ∨ a.Uniform s true ∨ a.NonUniform s

Assuming a.PseudoConsensus 1, any reachable state of a is either uniform or non-uniform.

theorem Cslib.FLP.OnePseudoConsensus.decided_eq_canDecideWithout {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] (hpc1 : a.PseudoConsensus 1) {s : State P M S} (hr : a.Reachable inp s) {b b' : Bool} {p : P} (hd : s.Decided b) (hd' : a.CanDecideWithout s p b') : b = b'

Assuming a.PseudoConsensus 1, if a reachable state of a has decided on a boolean value b and a.CanDecideWithout s p b' for any process p, then b = b'.

theorem Cslib.FLP.OnePseudoConsensus.decided_imp_uniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] (hpc1 : a.PseudoConsensus 1) {s : State P M S} (hr : a.Reachable inp s) {b : Bool} (hd : s.Decided b) : a.Uniform s b

Assuming a.PseudoConsensus 1, if a reachable state of a has decided on a boolean value b, then s is uniform for b. This theorem formalizes Proposition 2(b) of [Vol04].

theorem Cslib.FLP.OnePseudoConsensus.canDecideWithout_dest {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {s s' : State P M S} {m : Message P M} {b : Bool} (ht : a.lts.Tr s (some m) s') (hd : a.CanDecideWithout s m.dest b) : a.CanDecideWithout s' m.dest b

For any message m, if state s' is reached from state s by receiving m, then a.CanDecideWithout s m.dest b implies a.CanDecideWithout s' m.dest b for any b. This theorem formalizes Proposition 3(b) of [Vol04].

theorem Cslib.FLP.OnePseudoConsensus.canDecideWithout_nondest {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {s s' : State P M S} {m : Message P M} {b : Bool} (ht : a.lts.Tr s (some m) s') {p : P} (hn : p ≠ m.dest) (hd' : a.CanDecideWithout s' p b) : a.CanDecideWithout s p b

For any message m, if state s' is reached from state s by receiving m, then a.CanDecideWithout s' p b implies a.CanDecideWithout s p b for any b and any p ≠ m.dest. This theorem formalizes Proposition 3(a) of [Vol04].

theorem Cslib.FLP.OnePseudoConsensus.canDecideWithout_uniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] (hpc1 : a.PseudoConsensus 1) {s s' : State P M S} {m : Message P M} {b : Bool} (hr : a.Reachable inp s) (ht : a.lts.Tr s (some m) s') {p : P} (hd : a.CanDecideWithout s p b) (hdn : ¬a.CanDecideWithout s p !b) : a.CanDecideWithout s' p b

Assuming a.PseudoConsensus 1, if any reachable state s of a is uniform for b and state s' is reached from s by receiving a message m, then a.CanDecideWithout s' p b. This theorem formalizes Proposition 3(c) of [Vol04].

theorem Cslib.FLP.OnePseudoConsensus.nonUniform_step {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] (hpc1 : a.PseudoConsensus 1) {s : State P M S} (hr : a.Reachable inp s) (hn : a.NonUniform s) (p : P) : ∃ (s' : State P M S), a.lts.CanReach s s' ∧ ∀ (b : Bool), a.CanDecideWithout s' p b

Assuming a.PseudoConsensus 1, if any reachable state s of a that is non-uniform, then for any process p, there exists a state s' reachable from s such that a.CanDecideWithout s' p b for all b. This theorem formalizes Lemma 2 of [Vol04].

def Cslib.FLP.OnePseudoConsensus.inpN {P : Type u_1} [Fintype P] (pn : P ≃ Fin (Fintype.card P)) (n : ℕ) : P → Bool

Given a numbering pn of processes and n : ℕ, inpN pn n assigns true to the processes numbered 0, ..., (n - 1) and false to the rest.

Equations

• Cslib.FLP.OnePseudoConsensus.inpN pn n p = if ↑(pn p) < n then true else false

theorem Cslib.FLP.OnePseudoConsensus.inpN_eqOn_except_singleton {P : Type u_1} [Fintype P] (pn : P ≃ Fin (Fintype.card P)) {n : ℕ} (hn0 : 0 < n) (hnc : n ≤ Fintype.card P) : InpEqOn {pn.symm ⟨n - 1, ⋯⟩}ᶜ (inpN pn (n - 1)) (inpN pn n)

Assuming 0 < n ≤ card P, the inputs inpN pn (n - 1) amd inpN pn n agree on all processes except the one that is numbered (n - 1).

theorem Cslib.FLP.OnePseudoConsensus.inpN_zero_no_true {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (pn : P ≃ Fin (Fintype.card P)) (hpc1 : a.PseudoConsensus 1) (p : P) : ¬a.CanDecideWithout (a.start (inpN pn 0)) p true

theorem Cslib.FLP.OnePseudoConsensus.inpN_zero_uniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (pn : P ≃ Fin (Fintype.card P)) (hpc1 : a.PseudoConsensus 1) (hc : Fintype.card P ≥ 1) : a.Uniform (a.start (inpN pn 0)) false

Assuming a.PseudoConsensus 1, the initial state determined by the all-false input is uniform for false.

theorem Cslib.FLP.OnePseudoConsensus.inpN_card_not_false {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (pn : P ≃ Fin (Fintype.card P)) (hpc1 : a.PseudoConsensus 1) (p : P) : ¬a.CanDecideWithout (a.start (inpN pn (Fintype.card P))) p false

theorem Cslib.FLP.OnePseudoConsensus.inpN_card_uniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (pn : P ≃ Fin (Fintype.card P)) (hpc1 : a.PseudoConsensus 1) (hc : Fintype.card P ≥ 1) : a.Uniform (a.start (inpN pn (Fintype.card P))) true

Assuming a.PseudoConsensus 1, the initial state determined by the all-true input is uniform for true.

theorem Cslib.FLP.OnePseudoConsensus.nonUniform_inp {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (hpc1 : a.PseudoConsensus 1) (hc : Fintype.card P ≥ 2) : ∃ (inp : P → Bool), a.NonUniform (a.start inp)

Assuming a.PseudoConsensus 1 and there are at least 2 processes, there must exist an input that gives rise to a non-uniform initial state. This theorem formalizes Lemma 1 of [Vol04].