bft-proposal

BFT with Leader Proposal

Extends bft-voting by adding a leader who proposes values. Demonstrates why BFT protocols need leaders and what happens when leaders are faulty.

Protocol Overview

Leader                           Nodes
  |                                |
  |-- propose(value) -----------> N2    (correct leader: same value to all)
  |-- propose(value) -----------> N3
  |-- propose(value) -----------> N4
  |                                |
  |   OR (faulty leader)           |
  |                                |
  |-- propose(A) ---------------> N2    (faulty leader: different values)
  |-- propose(B) ---------------> N3
  |-- propose(A) ---------------> N4
  |                                |
  |                           nodes vote for received proposal
  |                                |
  |                           value commits at 2f+1 votes

Running

make test SPEC=bft-proposal
make run SPEC=bft-proposal
make verify SPEC=bft-proposal

State Variables

Variable	Type	Description
status	Node -> Status	Which nodes are faulty
leader	Node	Current round's leader
proposal	Node -> Value	What each node received from leader
votes	Node -> Set[Value]	Votes cast by each node
committed	Set[Value]	Values that reached quorum

Actions

correctLeaderPropose(value)

Correct leader proposes the same value to all nodes.

Precondition: Leader is correct, no proposals sent yet

Effect: All nodes receive the same proposal

---

faultyLeaderPropose(node, value)

Faulty leader sends a proposal to one node.

Precondition: Leader is faulty, node hasn't received proposal

Effect: Node receives proposal (may differ from other nodes)

---

correctVote(node)

Correct node votes for the value it received.

Precondition: Node is correct, has proposal, hasn't voted

Effect: Vote recorded for proposed value

---

faultyVote(node, value)

Faulty node votes for any value.

Precondition: Node is faulty

Effect: Vote recorded (can accumulate)

Safety Properties

agreement

At most one value commits.

committed.size() <= 1

integrity

Committed values were voted for by some correct node.

Key Insights

Why leaders? Without a leader, correct nodes might vote for different values and nothing commits. The leader coordinates.

Faulty leader equivocation: A faulty leader can propose A to some nodes and B to others. But agreement still holds because:

• At most f nodes are faulty
• Quorum is 2f+1
• Two quorums overlap by at least f+1 (one correct node)
• That correct node voted for only one value

Tests

correctLeaderTest

Correct leader proposes A, all correct nodes vote A, A commits.

faultyLeaderEquivocationTest

Faulty leader sends A to N2/N4, B to N3. Shows only one value commits.

faultyLeaderBothValuesTest

Faulty leader tries to help both values. Agreement holds.

Next Steps

• bft-locking/ - Add locks across multiple rounds
• pbft/ - Full 3-phase protocol

References

• bft-voting/ - BFT quorum voting (prerequisite)
• PBFT - Castro, Liskov (1999)