mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
d3bff5e2dc
The lean/ proof library (88 files) had ~180 type-check errors across ~45 files plus 31 proof-by-assumption axiom cheats. It now type-checks cleanly under Lean 4.14.0 + Mathlib, with every theorem genuinely proven from definitions. Errors fixed: - Stale Mathlib imports: Data.Nat.Basic / Data.Int.Basic were removed this rev -> Data.Nat.Defs / Data.Int.Defs (57 files). - Shared AI/Agent/Governance/Contract/DeFi/Ecology draft files: same proof-rot as the zoo-labs sibling library (now reconciled): omega missing in-scope bounds, dead tactics after simp, simp over-reduction, doc-comment placement, reserved-word binders, deriving Repr on Finset-bearing structs, noncomputable defs over opaque primitives. - Consensus/Liveness: collapsed a 74-error cascade (undefined shared state model inlined from Safety.lean; the |>. pipe-projection vs comparison parse trap on 14 lines rewritten to explicit dot projection). - Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE), Consensus, Protocol, Warp, Trust, GPU, Compute, Network, DeFi: brought structure invariants into scope for omega, Nat-division bounds via Nat.div_le_of_le_mul / Nat.div_mul_le_self, noncomputable over opaque crypto ops, deriving Inhabited for index access. Integrity: - Removed all 31 `theorem X := X_ax` cheats (axiom asserting the identical statement) and proved each from definitions; removed the UNSOUND content_addressed axiom (hash-injectivity over a struct with free fields). - Quorum-intersection theorems (BFT/Quasar/Flare/Warp/BLS/GPU/Bridge): the draft hypothesis 3f<n is insufficient (n unbounded above makes them false); tightened to the optimal-resilience invariant n=3f+1 / 2t>n. Statement intent preserved. - Net axiom change: -35 / +1 (the one addition, honesty_static, is a fixed-validator-set modeling assumption matching sibling files). - Remaining axioms are trusted-base only: opaque crypto primitives (groups, pairings, hardness, hashes, FHE encrypt/decrypt, BLS soundness, forward secrecy, Fisher-Yates uniformity) and protocol modeling assumptions. No sorry/admit/native_decide. Verified all theorems trace to [propext, Classical.choice, Quot.sound] plus those primitives. Co-authored-by: Hanzo Dev <[email protected]>
85 lines
2.7 KiB
Lean4
85 lines
2.7 KiB
Lean4
/-
|
|
Authors: Antje Worring, Zach Kelling
|
|
|
|
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.
|
|
At the optimal node count n = 3f+1, two certificates of size 2f+1 each
|
|
together exceed n, so they must overlap.
|
|
Maps to flare.go: support >= 2*p.F+1 -/
|
|
theorem certificate_quorum_overlap
|
|
(n f : Nat)
|
|
(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 = 3f+1 nodes with f Byzantine,
|
|
any two subsets of size 2f+1 share at least one honest node.
|
|
Two such subsets together have 2(2f+1) = 4f+2 > n + f = 4f+1 members,
|
|
so their overlap exceeds the f Byzantine nodes — i.e. it is honest.
|
|
This prevents conflicting certificates. -/
|
|
theorem bft_intersection
|
|
(n f : Nat)
|
|
(hn : n = 3 * f + 1)
|
|
: 2 * (2 * f + 1) > n + f := by
|
|
omega
|
|
|
|
end Consensus.BFT
|