Byzantine generals problem

StructureOral-message protocol#✓fully proved

A synchronous oral-message protocol for a set \(G\) of generals, with orders in \(V\), local states in \(\sigma\) and messages in \(M\), consists of an initial state for each general in \(G\), used by the generals other than the commander; an initial state of the commander for each order in \(V\); a sending function giving, for each round \(r\), each general \(j\) in each state \(s\) and each general \(i\), the message in \(M\) that \(j\) sends to \(i\) in round \(r\); a transition function giving, for each round \(r\), each general \(i\) in each state \(s\) and each assignment of a message to every sender \(j\), the state of \(i\) after round \(r\); and a decision function giving the value in \(V\) that each general decides in each state.

The commander is not part of the protocol: it is chosen when the protocol is run. In each round every general sends its messages from its current state and then moves to the state given by the transition function on the messages it received. Only the commander's initial state depends on the order.

structure OralProtocol (G V σ M : Type*) where
  /-- The initial state of each general other than the commander. -/
  init : G → σ
  /-- The initial state of the commander, given its order. -/
  initCommander : V → σ
  /-- `send r j s i` is the message general `j`, in state `s`, sends to general `i` in round
  `r`. -/
  send : ℕ → G → σ → G → M
  /-- `recv r i s msg` is the state of general `i` after round `r`, from its state `s` and the
  message `msg j` it received from each general `j`. -/
  recv : ℕ → G → σ → (G → M) → σ
  /-- `decide i s` is the value general `i` decides in its final state `s`. -/
  decide : G → σ → V
Used by 18
Used byAgreement condition (IC1) · Decision of a general · No protocol for three generals tolerates one traitor · Messages received in a round · Initial state of a general · Initial state of a lieutenant · Initial state of the commander · No protocol for \(n\) generals tolerates \(m\) traitors when \(3 \le n \le 3m\) · No protocol for three generals solves the Byzantine generals problem with one traitor · Three generals simulating a protocol · Solving the Byzantine generals problem · Simulation reduces many generals to three · Executions of an oral-message protocol · The simulation is faithful · One round of an execution · The start of an execution · Local views determine states · Validity in the Byzantine generals problem

TheoremLocal views determine states#✓fully proved

Let \(P\) be an oral-message protocol for the generals \(G\) with states \(\sigma\) and messages \(M\). Let \(N\) be a type of nodes, node \(k\) running the code of the general \(\rho(k) \in G\), and let \(L\) be a property of nodes. For each round \(r\) and node \(k\), let \(s_r(k), s'_r(k) \in \sigma\) be two states and \(\mu_r(k), \mu'_r(k) : G \to M\) two families of received messages. Suppose that for every \(r\) and every node \(k\) satisfying \(L\), \(s_{r+1}(k)\) is the state to which general \(\rho(k)\) of \(P\) moves in round \(r\) from \(s_r(k)\) on the messages \(\mu_r(k)\), and \(s'_{r+1}(k)\) the one to which it moves from \(s'_r(k)\) on \(\mu'_r(k)\); that \(s_0(k) = s'_0(k)\) for every \(k\) satisfying \(L\); and that for every \(r\), if \(s_r(k) = s'_r(k)\) for all \(k\) satisfying \(L\), then \(\mu_r(k) = \mu'_r(k)\) for all \(k\) satisfying \(L\). Then \(s_r(k) = s'_r(k)\) for every \(r\) and every \(k\) satisfying \(L\).

theorem states_eq_of_inbox_eq {N : Type*} (role : N → G) (L : N → Prop) (s s' : ℕ → N → σ)
    (inb inb' : ℕ → N → G → M)
    (hs : ∀ r k, L k → s (r + 1) k = P.recv r (role k) (s r k) (inb r k))
    (hs' : ∀ r k, L k → s' (r + 1) k = P.recv r (role k) (s' r k) (inb' r k))
    (h0 : ∀ k, L k → s 0 k = s' 0 k)
    (hinb : ∀ r, (∀ k, L k → s r k = s' r k) → ∀ k, L k → inb r k = inb' r k) :
    ∀ r k, L k → s r k = s' r k
Uses 1 · Used by 3
Statement usesOral-message protocol
Used byNo protocol for three generals tolerates one traitor · No protocol for three generals solves the Byzantine generals problem with one traitor · The simulation is faithful

DefinitionInitial state of a general#✓fully proved

When the commander \(c\) has order \(v\), the initial state of general \(i\) is the initial state that the protocol assigns to a commander with order \(v\) if \(i = c\), and the initial state that the protocol assigns to \(i\) as a general other than the commander if \(i \ne c\).

def initState (c : G) (v : V) (i : G) : σ :=
  if i = c then P.initCommander v else P.init i
Uses 1 · Used by 8
Statement usesOral-message protocol
Used byNo protocol for three generals tolerates one traitor · Initial state of a lieutenant · Initial state of the commander · No protocol for three generals solves the Byzantine generals problem with one traitor · Three generals simulating a protocol · Executions of an oral-message protocol · The simulation is faithful · The start of an execution

TheoremInitial state of the commander#✓fully proved

When the commander \(c\) has order \(v\), the initial state of \(c\) is the initial state that the protocol assigns to a commander with order \(v\).

theorem initState_self (c : G) (v : V) : P.initState c v c = P.initCommander v
Uses 2
Statement usesOral-message protocol · Initial state of a general

TheoremInitial state of a lieutenant#✓fully proved

If general \(i\) is not the commander \(c\), then the initial state of \(i\) when \(c\) has order \(v\) is the initial state that the protocol assigns to \(i\) as a general other than the commander; in particular, it does not depend on \(v\).

theorem initState_of_ne {c i : G} (v : V) (h : i ≠ c) : P.initState c v i = P.init i
Uses 2 · Used by 2
Statement usesOral-message protocol · Initial state of a general
Used byNo protocol for three generals tolerates one traitor · No protocol for three generals solves the Byzantine generals problem with one traitor

DefinitionExecutions of an oral-message protocol#✓fully proved

Let \(P\) be an oral-message protocol for the generals \(G\), let \(c \in G\) be the commander, \(v\) its order and \(S \subseteq G\) a finite set of traitors, and let \(a_r(j, i)\) be the message a traitor \(j\) sends general \(i\) in round \(r\). The state of general \(i\) after \(r\) rounds is defined by recursion on \(r\). After \(0\) rounds it is the initial state of \(i\) for commander \(c\) and order \(v\). After \(r + 1\) rounds it is the state to which \(i\) moves by its code for round \(r\) from its state after \(r\) rounds, on receiving \(a_r(j, i)\) from each traitor \(j \in S\) and, from each other general \(j\), the message that \(P\) has \(j\) send to \(i\) in round \(r\) from the state of \(j\) after \(r\) rounds.

def state (c : G) (v : V) (traitors : Finset G) (adv : ℕ → G → G → M) : ℕ → G → σ
  | 0, i => P.initState c v i
  | r + 1, i => P.recv r i (state c v traitors adv r i) fun j =>
      if j ∈ traitors then adv r j i else P.send r j (state c v traitors adv r j) i
Uses 2 · Used by 8
Statement usesOral-message protocol · Initial state of a general
Used byDecision of a general · No protocol for three generals tolerates one traitor · Messages received in a round · No protocol for three generals solves the Byzantine generals problem with one traitor · Simulation reduces many generals to three · The simulation is faithful · One round of an execution · The start of an execution

DefinitionMessages received in a round#✓fully proved

In the execution of a protocol \(P\) with commander \(c\), order \(v\), a set of traitors and a behaviour \(\mathrm{adv}\) of the traitors, the messages that general \(i\) receives in round \(r\) form the function of the sender \(j\) whose value is \(\mathrm{adv}(r, j, i)\) if \(j\) is a traitor, and otherwise the message that \(P\) has \(j\) send to \(i\) in round \(r\) from the state of \(j\) after \(r\) rounds.

def inbox (c : G) (v : V) (traitors : Finset G) (adv : ℕ → G → G → M) (r : ℕ) (i : G) :
    G → M := fun j =>
  if j ∈ traitors then adv r j i else P.send r j (P.state c v traitors adv r j) i
Uses 2 · Used by 4
Statement usesOral-message protocol · Executions of an oral-message protocol
Used byNo protocol for three generals tolerates one traitor · No protocol for three generals solves the Byzantine generals problem with one traitor · The simulation is faithful · One round of an execution

TheoremThe start of an execution#✓fully proved

In the execution of an oral-message protocol \(P\) with commander \(c\), order \(v\), any set of traitors and any traitor behaviour, every general is in its initial state after \(0\) rounds: the commander in the initial state given by the order \(v\), and every other general in its order-independent initial state.

theorem state_zero : P.state c v traitors adv 0 = P.initState c v
Uses 3
Statement usesOral-message protocol · Initial state of a general · Executions of an oral-message protocol

TheoremOne round of an execution#✓fully proved

In the execution of an oral-message protocol \(P\) with a given commander, order, set of traitors and traitor behaviour, for every round \(r\) and every general \(i\), the state of \(i\) after \(r + 1\) rounds is the state to which \(i\) moves by its code for round \(r\) from its state after \(r\) rounds on the messages it receives in round \(r\).

theorem state_succ (r : ℕ) (i : G) :
    P.state c v traitors adv (r + 1) i =
      P.recv r i (P.state c v traitors adv r i) (P.inbox c v traitors adv r i)
Uses 3 · Used by 3
Statement usesOral-message protocol · Messages received in a round · Executions of an oral-message protocol
Used byNo protocol for three generals tolerates one traitor · No protocol for three generals solves the Byzantine generals problem with one traitor · The simulation is faithful

DefinitionDecision of a general#✓fully proved

In the execution of a protocol \(P\) with commander \(c\), order \(v\), a set of traitors and a behaviour of the traitors, the decision of general \(i\) after \(T\) rounds is the value that the decision function of \(P\) assigns to \(i\) in its state after \(T\) rounds.

def decision (T : ℕ) (i : G) : V := P.decide i (P.state c v traitors adv T i)
Uses 2 · Used by 5
Statement usesOral-message protocol · Executions of an oral-message protocol
Used byAgreement condition (IC1) · No protocol for three generals tolerates one traitor · No protocol for three generals solves the Byzantine generals problem with one traitor · Simulation reduces many generals to three · Validity in the Byzantine generals problem

DefinitionAgreement condition (IC1)#✓fully proved

Consider the execution of a protocol \(P\) with commander \(c\), order \(v\), a set of traitors and a behaviour of the traitors. Condition IC1 holds after \(T\) rounds when any two generals \(i\) and \(j\), neither of which is the commander or a traitor, decide the same value after \(T\) rounds of this execution.

def Agreement (T : ℕ) : Prop :=
  ∀ i j, i ≠ c → j ≠ c → i ∉ traitors → j ∉ traitors →
    P.decision c v traitors adv T i = P.decision c v traitors adv T j
Uses 2 · Used by 4
Statement usesOral-message protocol · Decision of a general
Used byNo protocol for three generals tolerates one traitor · No protocol for three generals solves the Byzantine generals problem with one traitor · Solving the Byzantine generals problem · Simulation reduces many generals to three

DefinitionValidity in the Byzantine generals problem#✓fully proved

In the execution of an oral-message protocol with commander \(c\), order \(v\), a set of traitors and a traitor behaviour, condition IC2 (validity) holds after \(T\) rounds if, provided the commander is loyal, every loyal general other than the commander decides \(v\) after \(T\) rounds.

def Validity (T : ℕ) : Prop :=
  c ∉ traitors → ∀ i, i ≠ c → i ∉ traitors → P.decision c v traitors adv T i = v
Uses 2 · Used by 4
Statement usesOral-message protocol · Decision of a general
Used byNo protocol for three generals tolerates one traitor · No protocol for three generals solves the Byzantine generals problem with one traitor · Solving the Byzantine generals problem · Simulation reduces many generals to three

DefinitionSolving the Byzantine generals problem#✓fully proved

An oral-message protocol \(P\) for the generals \(G\) solves the Byzantine generals problem with commander \(c \in G\) and at most \(m\) traitors in \(T\) rounds if, for every order \(v\), every set of at most \(m\) traitors and every behaviour of the traitors (the message each traitor sends to each general in each round), conditions IC1 (agreement) and IC2 (validity) hold after \(T\) rounds.

def Solves (c : G) (m T : ℕ) : Prop :=
  ∀ (v : V) (traitors : Finset G), traitors.card ≤ m → ∀ adv : ℕ → G → G → M,
    P.Agreement c v traitors adv T ∧ P.Validity c v traitors adv T
Uses 3 · Used by 3
Statement usesOral-message protocol · Agreement condition (IC1) · Validity in the Byzantine generals problem
Used byNo protocol for \(n\) generals tolerates \(m\) traitors when \(3 \le n \le 3m\) · No protocol for three generals solves the Byzantine generals problem with one traitor · Simulation reduces many generals to three

TheoremNo protocol for three generals tolerates one traitor#✓fully proved

Suppose there are at least two possible orders. For every oral-message protocol for three generals \(0\), \(1\), \(2\) with commander \(0\) and every number of rounds \(T\), there are an order \(v\), a general \(t\) and a behaviour of \(t\) such that, in the execution with order \(v\) in which \(t\) is the only traitor, the agreement condition (IC1) or the validity condition (IC2) fails after \(T\) rounds.

This is the theorem of Pease, Shostak and Lamport, proved here by a commander version of the hexagon argument of Fischer, Lynch and Merritt.

theorem exists_violation_three [Nontrivial V] (P : OralProtocol (Fin 3) V σ M) (T : ℕ) :
    ∃ (v : V) (t : Fin 3) (adv : ℕ → Fin 3 → Fin 3 → M),
      ¬ (P.Agreement 0 v {t} adv T ∧ P.Validity 0 v {t} adv T)
Uses 10
Statement usesOral-message protocol · Agreement condition (IC1) · Validity in the Byzantine generals problem
Proof usesDecision of a general · Messages received in a round · Initial state of a general · Initial state of a lieutenant · Executions of an oral-message protocol · One round of an execution · Local views determine states

TheoremNo protocol for three generals solves the Byzantine generals problem with one traitor#✓fully proved

No protocol for three generals solves the Byzantine generals problem with one traitor. Suppose there are at least two possible orders. For every oral-message protocol for three generals \(0\), \(1\), \(2\) with commander \(0\) and every number of rounds \(T\), the protocol does not solve the Byzantine generals problem with commander \(0\) and at most one traitor in \(T\) rounds.

theorem not_solves_three [Nontrivial V] (P : OralProtocol (Fin 3) V σ M) (T : ℕ) :
    ¬ P.Solves 0 1 T
Uses 11 · Used by 1
Statement usesOral-message protocol · Solving the Byzantine generals problem
Proof usesAgreement condition (IC1) · Validity in the Byzantine generals problem · Decision of a general · Messages received in a round · Initial state of a general · Initial state of a lieutenant · Executions of an oral-message protocol · One round of an execution · Local views determine states
Used byNo protocol for \(n\) generals tolerates \(m\) traitors when \(3 \le n \le 3m\)

DefinitionThree generals simulating a protocol#✓fully proved

Let \(P\) be an oral-message protocol for the generals \(G\) with orders in \(V\), states \(\sigma\) and messages \(M\), let \(c \in G\), let \(\mathrm{grp} : G \to \{0, 1, 2\}\) split the generals into three groups and let \(\mathrm{rep} : \{0, 1, 2\} \to G\). The simulation of \(P\) with \(c\), \(\mathrm{grp}\) and \(\mathrm{rep}\) is the oral-message protocol for the generals \(\{0, 1, 2\}\) with orders in \(V\), whose states are families \((s(i))_{i \in G}\) of states of \(\sigma\) and whose messages are families \((\mu(j, i))_{j, i \in G}\) of messages of \(M\), defined as follows. A general other than the commander starts from the family of the initial states that \(P\) gives each general of \(G\) as a non-commander; the commander, with order \(v\), starts from the family of the initial states of the generals of \(G\) in \(P\) when \(c\) is the commander with order \(v\). In round \(r\), a general in state \(s\) sends every general the family whose entry \((j, i)\) is the message that general \(j\) of \(P\), in state \(s(j)\), sends to general \(i\) in round \(r\). In round \(r\), general \(g\) in state \(s\), having received \(\mu_h\) from each general \(h\), moves to the family that keeps \(s(i)\) for each \(i\) with \(\mathrm{grp}(i) \ne g\) and, for each \(i\) with \(\mathrm{grp}(i) = g\), holds the state to which general \(i\) of \(P\) moves in round \(r\) from \(s(i)\) on receiving \(\mu_{\mathrm{grp}(j)}(j, i)\) from each \(j \in G\). General \(g\) in final state \(s\) decides what general \(\mathrm{rep}(g)\) of \(P\) decides in state \(s(\mathrm{rep}(g))\).

def simulate (c : G) (grp : G → Fin 3) (rep : Fin 3 → G) :
    OralProtocol (Fin 3) V (G → σ) (G → G → M) where
  init _ := P.init
  initCommander v := P.initState c v
  send r _ s _ j i := P.send r j (s j) i
  recv r g s msg i := if grp i = g then P.recv r i (s i) (fun j => msg (grp j) j i) else s i
  decide g s := P.decide (rep g) (s (rep g))
Uses 2 · Used by 3
Statement usesOral-message protocol · Initial state of a general
Used byNo protocol for \(n\) generals tolerates \(m\) traitors when \(3 \le n \le 3m\) · Simulation reduces many generals to three · The simulation is faithful

TheoremThe simulation is faithful#✓fully proved

Let \(P\) be an oral-message protocol for a finite set \(G\) of generals with messages \(M\), let \(c \in G\), and let \(\mathrm{grp} : G \to \{0, 1, 2\}\) and \(\mathrm{rep} : \{0, 1, 2\} \to G\) with \(\mathrm{grp}(c) = 0\). Fix an order \(v\), a set \(S \subseteq \{0, 1, 2\}\) of traitors and a traitor behaviour \(a\) for the simulation of \(P\) with \(c\), \(\mathrm{grp}\) and \(\mathrm{rep}\): in round \(r\) a traitor \(h\) sends general \(g\) the family \((a_r(h, g)(j, i))_{j, i \in G}\) of messages of \(M\). Compare the execution of the simulation with commander \(0\), order \(v\), traitors \(S\) and behaviour \(a\) with the execution of \(P\) with commander \(c\), order \(v\) and traitors \(\{j \in G : \mathrm{grp}(j) \in S\}\), in which a traitor \(j\) sends general \(i\) the message \(a_r(\mathrm{grp}(j), \mathrm{grp}(i))(j, i)\) in round \(r\). Then for every \(r \in \mathbb{N}\) and every \(i \in G\) with \(\mathrm{grp}(i) \notin S\), the entry at \(i\) of the state of general \(\mathrm{grp}(i)\) after \(r\) rounds of the first execution equals the state of general \(i\) after \(r\) rounds of the second.

theorem state_simulate (c : G) (grp : G → Fin 3) (rep : Fin 3 → G) (hc : grp c = 0) (v : V)
    (traitors : Finset (Fin 3)) (adv : ℕ → Fin 3 → Fin 3 → G → G → M) (r : ℕ) (i : G)
    (hi : grp i ∉ traitors) :
    (P.simulate c grp rep).state 0 v traitors adv r (grp i) i =
      P.state c v {j | grp j ∈ traitors} (fun r j i => adv r (grp j) (grp i) j i) r i
Uses 7 · Used by 1
Statement usesOral-message protocol · Three generals simulating a protocol · Executions of an oral-message protocol
Proof usesMessages received in a round · Initial state of a general · One round of an execution · Local views determine states
Used bySimulation reduces many generals to three

TheoremSimulation reduces many generals to three#✓fully proved

Let \(P\) be an oral-message protocol for a finite set \(G\) of generals, let \(c \in G\) and \(m, T \in \mathbb{N}\), and suppose that \(P\) solves the Byzantine generals problem with commander \(c\) and at most \(m\) traitors in \(T\) rounds. Let \(\mathrm{grp} : G \to \{0, 1, 2\}\) and \(\mathrm{rep} : \{0, 1, 2\} \to G\) satisfy \(\mathrm{grp}(c) = 0\), \(\mathrm{grp}(\mathrm{rep}(g)) = g\) for every \(g \ne 0\), and \(|\{i \in G : \mathrm{grp}(i) = g\}| \le m\) for every \(g\). Then the simulation of \(P\) with \(c\), \(\mathrm{grp}\) and \(\mathrm{rep}\) solves the Byzantine generals problem for the generals \(\{0, 1, 2\}\) with commander \(0\) and at most one traitor in \(T\) rounds.

theorem solves_simulate {c : G} {m T : ℕ} (hP : P.Solves c m T) (grp : G → Fin 3)
    (rep : Fin 3 → G) (hc : grp c = 0) (hrep : ∀ g, g ≠ 0 → grp (rep g) = g)
    (hcard : ∀ g, ({i | grp i = g} : Finset G).card ≤ m) :
    (P.simulate c grp rep).Solves 0 1 T
Uses 8 · Used by 1
Statement usesOral-message protocol · Solving the Byzantine generals problem · Three generals simulating a protocol
Proof usesAgreement condition (IC1) · Validity in the Byzantine generals problem · Decision of a general · Executions of an oral-message protocol · The simulation is faithful
Used byNo protocol for \(n\) generals tolerates \(m\) traitors when \(3 \le n \le 3m\)

TheoremNo protocol for \(n\) generals tolerates \(m\) traitors when \(3 \le n \le 3m\)#✓fully proved

Suppose there are at least two possible orders and the set of generals is finite with \(n\) elements, where \(3 \le n \le 3m\). Then for every oral-message protocol, every commander \(c\) and every number of rounds \(T\), the protocol does not solve the Byzantine generals problem with commander \(c\) and at most \(m\) traitors in \(T\) rounds: there are an order, a set of at most \(m\) traitors and a behaviour of the traitors for which the agreement condition (IC1) or the validity condition (IC2) fails after \(T\) rounds.

This is the theorem of Lamport, Shostak and Pease, proved by reduction to three generals.

theorem not_solves_of_card_le_three_mul [Nontrivial V] (c : G) {m : ℕ}
    (h3 : 3 ≤ Fintype.card G) (hm : Fintype.card G ≤ 3 * m) (T : ℕ) : ¬ P.Solves c m T
Uses 5
Statement usesOral-message protocol · Solving the Byzantine generals problem
Proof usesNo protocol for three generals solves the Byzantine generals problem with one traitor · Three generals simulating a protocol · Simulation reduces many generals to three

DefinitionMajority of a multiset#✓fully proved

The majority of a finite multiset \(s\) of values is the value \(x\) such that more than half of the elements of \(s\) are equal to \(x\) (counted with multiplicity), if there is one (there is at most one), and a fixed default value (retreat) otherwise.

def majority (s : Multiset V) : V :=
  haveI := Multiset.decidableExistsMultiset (m := s) (p := fun x ↦ Multiset.card s < 2 * s.count x)
  if h : ∃ x ∈ s, Multiset.card s < 2 * s.count x then
    s.choose (fun x ↦ Multiset.card s < 2 * s.count x) (by
      obtain ⟨x, hx, hc⟩ := h
      refine ⟨x, ⟨hx, hc⟩, fun y ⟨_, hy⟩ ↦ ?_⟩
      by_contra hyx
      have := count_add_count_le (s := s) hyx
      omega)
  else default
Used by 5
Used byMajority falls back to the default value · A value filling more than half of a multiset is its majority · The oral messages algorithm · Agreement under oral messages (IC1) · A loyal commander is obeyed under oral messages

TheoremA value filling more than half of a multiset is its majority#✓fully proved

If more than half of the elements of a multiset \(s\) of values are equal to \(x\) (counted with multiplicity), then the majority of \(s\) is \(x\).

theorem majority_eq_of_lt_count {s : Multiset V} {x : V} (h : Multiset.card s < 2 * s.count x) :
    majority s = x
Uses 1 · Used by 1
Statement usesMajority of a multiset
Used byA loyal commander is obeyed under oral messages

TheoremMajority falls back to the default value#✓fully proved

If, for every value \(x\), at most half of the elements of a multiset \(s\) of values are equal to \(x\) (counted with multiplicity), then the majority of \(s\) is the default value (retreat).

theorem majority_eq_default {s : Multiset V} (h : ∀ x, 2 * s.count x ≤ Multiset.card s) :
    majority s = default
Uses 1
Statement usesMajority of a multiset

DefinitionValue received from a commander#✓fully proved

Fix a predicate saying which generals are loyal and an adversary \(\mathrm{adv}\) that assigns a value to each pair of a finite sequence of generals and a recipient. The value that lieutenant \(p\) receives from commander \(c\), who holds the value \(v\) and whose superiors form the sequence \(\sigma\), is \(v\) if \(c\) is loyal, and is \(\mathrm{adv}(\sigma c, p)\) if \(c\) is a traitor, where \(\sigma c\) is \(\sigma\) followed by \(c\).

def received (c : G) (v : V) (path : List G) (p : G) : V :=
  if loyal c then v else adv (path ++ [c]) p
Used by 5
Used byThe oral messages algorithm · Agreement under oral messages (IC1) · A loyal commander is obeyed under oral messages · A loyal commander sends its value · A traitorous commander sends the adversary's value

DefinitionThe oral messages algorithm#✓fully proved

Fix which generals are loyal and a strategy for the traitors, which assigns a value to each list of generals and each recipient. Let \(c\) be a commander holding the value \(v\), let \(\sigma\) be the list of the commanders above \(c\), and let \(S\) be a finite set of lieutenants. For a general \(q\), let \(r_q\) be the value \(q\) receives from \(c\): \(v\) if \(c\) is loyal, and otherwise the value the strategy assigns to the list \(\sigma c\) (\(\sigma\) followed by \(c\)) and the recipient \(q\). The value that a general \(p\) decides under \(\mathrm{OM}(m)\) is defined by recursion on \(m\). Under \(\mathrm{OM}(0)\), \(p\) decides \(r_p\). Under \(\mathrm{OM}(m + 1)\), \(p\) decides the majority of the multiset of values \(w_q\) for \(q \in S\), where \(w_p = r_p\) and, for \(q \ne p\), \(w_q\) is the value \(p\) decides under \(\mathrm{OM}(m)\) when \(q\), holding \(r_q\) with the superiors \(\sigma c\), sends it to the lieutenants \(S \setminus \{q\}\).

def om : ℕ → G → Finset G → V → List G → G → V
  | 0, c, _, v, path, p => received loyal adv c v path p
  | m + 1, c, S, v, path, p => majority (S.val.map fun q ↦
      if q = p then received loyal adv c v path p
      else om m q (S.erase q) (received loyal adv c v path q) (path ++ [c]) p)
Uses 2 · Used by 5
Statement usesMajority of a multiset · Value received from a commander
Used byThe oral messages algorithm solves the Byzantine generals problem · Agreement under oral messages (IC1) · A loyal commander is obeyed under oral messages · Oral messages achieve interactive consistency · Validity under oral messages (IC2)

TheoremA loyal commander sends its value#✓fully proved

If the commander \(c\) is loyal, then for every value \(v\), every list of superiors of \(c\) and every general \(p\), the value \(p\) receives from \(c\) is \(v\).

@[simp]
theorem received_of_loyal {c : G} (hc : loyal c) (v : V) (path : List G) (p : G) :
    received loyal adv c v path p = v
Uses 1
Statement usesValue received from a commander

TheoremA traitorous commander sends the adversary's value#✓fully proved

Fix which generals are loyal and an adversary \(\mathrm{adv}\) that assigns a value to each pair of a list of generals and a recipient. If the commander \(c\) is a traitor, then for every value \(v\), every list \(\sigma\) of superiors of \(c\) and every general \(p\), the value \(p\) receives from \(c\) is \(\mathrm{adv}(\sigma c, p)\), where \(\sigma c\) is \(\sigma\) followed by \(c\).

@[simp]
theorem received_of_not_loyal {c : G} (hc : ¬ loyal c) (v : V) (path : List G) (p : G) :
    received loyal adv c v path p = adv (path ++ [c]) p
Uses 1
Statement usesValue received from a commander

TheoremA loyal commander is obeyed under oral messages#✓fully proved

Let \(m\) and \(k\) be natural numbers, and let a loyal commander \(c\) run \(\mathrm{OM}(m)\) with a value \(v\) and any list of superiors, sending to a finite set \(S\) of lieutenants. If \(2k + m < |S| + 1\) (more than \(2k + m\) generals when \(c \notin S\)) and at most \(k\) of the generals in \(S \cup \{c\}\) are traitors, then, whatever the traitors send, every loyal lieutenant \(p \in S\) decides \(v\).

This is Lemma 1 of Lamport–Shostak–Pease.

theorem om_eq_of_loyal {m k : ℕ} {c : G} {S : Finset G} (v : V) (path : List G)
    (hc : loyal c) (hS : 2 * k + m < S.card + 1)
    (hk : ((insert c S).filter (¬ loyal ·)).card ≤ k) {p : G} (hp : p ∈ S) (hpl : loyal p) :
    om loyal adv m c S v path p = v
Uses 4 · Used by 2
Statement usesThe oral messages algorithm
Proof usesMajority of a multiset · A value filling more than half of a multiset is its majority · Value received from a commander
Used byAgreement under oral messages (IC1) · Validity under oral messages (IC2)

TheoremValidity under oral messages (IC2)#✓fully proved

Let a loyal commander \(c\) run \(\mathrm{OM}(m)\) with a value \(v\) and any list of superiors, sending to a finite set \(S\) of lieutenants. If \(3m < |S| + 1\) (more than \(3m\) generals when \(c \notin S\)) and at most \(m\) of the generals in \(S \cup \{c\}\) are traitors, then, whatever the traitors send, every loyal lieutenant \(p \in S\) decides \(v\).

This is condition IC2 of Theorem 1 of Lamport–Shostak–Pease.

theorem om_valid {m : ℕ} {c : G} {S : Finset G} (v : V) (path : List G)
    (hS : 3 * m < S.card + 1) (hm : ((insert c S).filter (¬ loyal ·)).card ≤ m)
    (hc : loyal c) {p : G} (hp : p ∈ S) (hpl : loyal p) :
    om loyal adv m c S v path p = v
Uses 2 · Used by 2
Statement usesThe oral messages algorithm
Proof usesA loyal commander is obeyed under oral messages
Used byAgreement under oral messages (IC1) · Oral messages achieve interactive consistency

TheoremAgreement under oral messages (IC1)#✓fully proved

Let a commander \(c\) run \(\mathrm{OM}(m)\) with a value \(v\) and any list of superiors, sending to a finite set \(S\) of lieutenants with \(c \notin S\). If there are more than \(3m\) generals, that is \(3m < |S| + 1\), and at most \(m\) of the generals in \(S \cup \{c\}\) are traitors, then, whatever the traitors send, any two loyal lieutenants \(p, p' \in S\) decide the same value.

This is condition IC1 of Theorem 1 of Lamport–Shostak–Pease.

theorem om_agree {m : ℕ} {c : G} {S : Finset G} (v : V) (path : List G) (hcS : c ∉ S)
    (hS : 3 * m < S.card + 1) (hm : ((insert c S).filter (¬ loyal ·)).card ≤ m)
    {p p' : G} (hp : p ∈ S) (hp' : p' ∈ S) (hpl : loyal p) (hpl' : loyal p') :
    om loyal adv m c S v path p = om loyal adv m c S v path p'
Uses 5 · Used by 1
Statement usesThe oral messages algorithm
Proof usesMajority of a multiset · A loyal commander is obeyed under oral messages · Validity under oral messages (IC2) · Value received from a commander
Used byOral messages achieve interactive consistency

TheoremOral messages achieve interactive consistency#✓fully proved

Let a commander \(c\) run \(\mathrm{OM}(m)\) with a value \(v\) and any list of superiors, sending to a finite set \(S\) of lieutenants with \(c \notin S\). If there are more than \(3m\) generals, that is \(3m < |S| + 1\), and at most \(m\) of the generals in \(S \cup \{c\}\) are traitors, then, whatever the traitors send, any two loyal lieutenants in \(S\) decide the same value (IC1), and if \(c\) is loyal, every loyal lieutenant in \(S\) decides \(v\) (IC2).

This is Theorem 1 of Lamport–Shostak–Pease.

theorem om_interactive_consistency {m : ℕ} {c : G} {S : Finset G} (v : V) (path : List G)
    (hcS : c ∉ S) (hS : 3 * m < S.card + 1)
    (hm : ((insert c S).filter (¬ loyal ·)).card ≤ m) :
    (∀ p ∈ S, ∀ p' ∈ S, loyal p → loyal p' →
        om loyal adv m c S v path p = om loyal adv m c S v path p') ∧
      (loyal c → ∀ p ∈ S, loyal p → om loyal adv m c S v path p = v)
Uses 3 · Used by 1
Statement usesThe oral messages algorithm
Proof usesAgreement under oral messages (IC1) · Validity under oral messages (IC2)
Used byThe oral messages algorithm solves the Byzantine generals problem

TheoremThe oral messages algorithm solves the Byzantine generals problem#✓fully proved

Let \(G\) be a finite set of more than \(3m\) generals, at most \(m\) of whom are traitors, and let the commander \(c \in G\) run \(\mathrm{OM}(m)\) with the value \(v\), with no superiors and with all the other generals as lieutenants. Then, whatever the traitors send, any two loyal lieutenants decide the same value, and if \(c\) is loyal, every loyal lieutenant decides \(v\).

This is Theorem 1 of Lamport–Shostak–Pease, applied to all the generals.

theorem byzantine_generals [Fintype G] {m : ℕ} (c : G) (v : V) (hG : 3 * m < Fintype.card G)
    (hm : (Finset.univ.filter (¬ loyal ·)).card ≤ m) :
    (∀ p p', p ≠ c → p' ≠ c → loyal p → loyal p' →
        om loyal adv m c (Finset.univ.erase c) v [] p =
          om loyal adv m c (Finset.univ.erase c) v [] p') ∧
      (loyal c → ∀ p, p ≠ c → loyal p → om loyal adv m c (Finset.univ.erase c) v [] p = v)
Uses 2
Statement usesThe oral messages algorithm
Proof usesOral messages achieve interactive consistency
31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.