mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
81 lines
2.4 KiB
Lean4
81 lines
2.4 KiB
Lean4
/-
|
|
Byzantine Fault Tolerance Threshold Proof
|
|
|
|
Theorem: Safety and liveness hold when f < n/3 nodes are Byzantine.
|
|
|
|
This is the structural argument that connects the BFT assumption
|
|
to the threshold voting mechanism.
|
|
|
|
Maps to Go code:
|
|
- core/dag/horizon.go: Params{N, F int} where F < N/3
|
|
- core/dag/flare.go: HasCertificate requires 2*F+1 support
|
|
- protocol/wave/wave.go: alpha threshold derived from honest majority
|
|
- protocol/quasar/quasar.go: BLS aggregation with 2f+1 threshold
|
|
|
|
Core argument:
|
|
Given n = 3f + 1 nodes (optimal), honest = n - f = 2f + 1.
|
|
Any k-sample of size k from n nodes contains at most f Byzantine.
|
|
So honest votes in sample >= k - f.
|
|
If alpha = ceil(2k/3), then honest majority in sample suffices.
|
|
Two conflicting values cannot both achieve alpha in the same sample
|
|
because that would require 2*alpha > 2*(2k/3) = 4k/3 > k total votes.
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Consensus.BFT
|
|
|
|
/-- The quorum intersection lemma:
|
|
Two quorums of size > 2n/3 must share at least one honest node. -/
|
|
theorem quorum_intersection
|
|
(n f : Nat)
|
|
(hf : f < n / 3)
|
|
(q1 q2 : Nat)
|
|
(hq1 : q1 > 2 * n / 3)
|
|
(hq2 : q2 > 2 * n / 3)
|
|
: q1 + q2 > n + f := by
|
|
omega
|
|
|
|
/-- With n = 3f+1 nodes, honest count = 2f+1 which exceeds 2n/3. -/
|
|
theorem honest_majority_sufficient
|
|
(f : Nat)
|
|
(hf : 0 < f)
|
|
: 2 * f + 1 > 2 * (3 * f + 1) / 3 := by
|
|
omega
|
|
|
|
/-- Two alpha-quorums cannot both be satisfied by different values
|
|
when alpha > 2k/3, because total votes would exceed k. -/
|
|
theorem unique_alpha_threshold
|
|
(k alpha : Nat)
|
|
(halpha : alpha > 2 * k / 3)
|
|
(v1_votes v2_votes : Nat)
|
|
(hv1 : v1_votes ≥ alpha)
|
|
(hv2 : v2_votes ≥ alpha)
|
|
: v1_votes + v2_votes > k := by
|
|
omega
|
|
|
|
/-- The certificate threshold (2f+1 out of n) ensures quorum intersection.
|
|
Maps to flare.go: support >= 2*p.F+1 -/
|
|
theorem certificate_quorum_overlap
|
|
(n f : Nat)
|
|
(hf : 3 * f < n)
|
|
(hn : n ≤ 3 * f + 1)
|
|
(cert1 cert2 : Nat)
|
|
(hc1 : cert1 ≥ 2 * f + 1)
|
|
(hc2 : cert2 ≥ 2 * f + 1)
|
|
: cert1 + cert2 > n := by
|
|
omega
|
|
|
|
/-- Key BFT property: in a set of n nodes with f Byzantine,
|
|
any two subsets of size 2f+1 share at least one honest node.
|
|
This prevents conflicting certificates. -/
|
|
theorem bft_intersection
|
|
(n f : Nat)
|
|
(hf : 3 * f < n)
|
|
(hn : n ≤ 3 * f + 1)
|
|
: 2 * (2 * f + 1) > n + f := by
|
|
omega
|
|
|
|
end Consensus.BFT
|