mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekay
6907bfc6e6
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
108 lines
4.8 KiB
Lean4
108 lines
4.8 KiB
Lean4
/-
|
|
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
|
GPU CONSENSUS SCALING LAWS
|
|
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
|
|
|
Formal verification of GPU-accelerated consensus operations.
|
|
|
|
Consensus is the third core component of any modern chain.
|
|
GPU acceleration targets the cryptographic bottlenecks:
|
|
|
|
1. BLS12-381 batch signature verification (10x GPU speedup)
|
|
2. Post-quantum signature verification (ML-DSA NTT on GPU)
|
|
3. Hybrid finality: parallel BLS + Corona verification
|
|
4. Validator set scaling with GPU batch verification
|
|
5. Block production pipelining with GPU precomputation
|
|
|
|
Authors: Lux Research, Woo Bin
|
|
Zoo Labs Foundation
|
|
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace Zoo.GPU.Consensus
|
|
|
|
/-! ## Model
|
|
|
|
Consensus requires verifying signatures from validators.
|
|
Each block contains `v` validator signatures.
|
|
BLS allows aggregation into a single pairing check,
|
|
but batch verification of multiple blocks still benefits from GPU.
|
|
Hybrid (Quasar) requires BOTH BLS and Corona verification. -/
|
|
|
|
/-- BLS batch verification: verifying `n` aggregate signatures
|
|
requires `n + 1` pairing operations (n pairings + 1 for generator).
|
|
GPU parallelizes pairings across cores.
|
|
With `p` cores: time = (n + 1) / p. -/
|
|
theorem bls_batch_parallel (n p : Nat) (_hp : 0 < p) :
|
|
(n + 1) / p ≤ n + 1 := by
|
|
exact Nat.div_le_self (n + 1) p
|
|
|
|
/-- BLS aggregation reduces verification cost: instead of verifying
|
|
`v` individual signatures (v pairings), aggregate into 1
|
|
verification (2 pairings). Savings = v - 2 pairings. -/
|
|
theorem bls_aggregation_savings (v : Nat) (_hv : v ≥ 2) :
|
|
v - 2 ≥ 0 := by omega
|
|
|
|
/-- Hybrid finality (Quasar): both BLS and Corona must verify.
|
|
GPU runs them in parallel on separate core groups.
|
|
Total time = max(bls_time, corona_time).
|
|
We prove parallel is never slower than sequential. -/
|
|
theorem hybrid_parallel_speedup (bls_time corona_time : Nat) :
|
|
max bls_time corona_time ≤ bls_time + corona_time := by
|
|
omega
|
|
|
|
/-- Validator scaling: with `v` validators, each block requires
|
|
verifying `v` signatures. GPU batch verification scales:
|
|
time = v / p (p = GPU cores). Adding validators doesn't
|
|
degrade finality if GPU cores scale proportionally. -/
|
|
theorem validator_gpu_scaling (v p : Nat) (_hp : 0 < p)
|
|
(hscale : p ≥ v) :
|
|
v / p ≤ 1 := by
|
|
exact Nat.div_le_of_le_mul (by omega)
|
|
|
|
/-- Post-quantum signature verification (ML-DSA): each verification
|
|
requires NTT operations. GPU parallelizes NTT butterflies.
|
|
ML-DSA verify = 2 NTTs of degree 256.
|
|
GPU speedup for NTT is linear in cores (up to N/2 per stage). -/
|
|
theorem pq_ntt_parallel (degree cores : Nat) (_hc : 0 < cores) :
|
|
degree / cores ≤ degree := Nat.div_le_self degree cores
|
|
|
|
/-- Block production pipelining: while block N is being finalized
|
|
(consensus round), block N+1 transactions execute on GPU.
|
|
Pipeline utilization = 1 - idle_fraction.
|
|
With 2-stage pipeline, idle ≤ max(exec, consensus) / (exec + consensus). -/
|
|
theorem pipeline_utilization (exec_time consensus_time : Nat)
|
|
(he : 0 < exec_time) (hc : 0 < consensus_time) :
|
|
max exec_time consensus_time ≤ exec_time + consensus_time := by
|
|
omega
|
|
|
|
/-- Quorum threshold with GPU: verifying quorum (2f+1 out of 3f+1)
|
|
on GPU. GPU verifies all signatures in parallel, then counts.
|
|
Quorum check is O(1) after parallel verify completes. -/
|
|
theorem quorum_gpu_verify (n f : Nat) (hf : n = 3 * f + 1)
|
|
(quorum : Nat) (hq : quorum = 2 * f + 1) :
|
|
quorum ≤ n := by omega
|
|
|
|
/-- GPU memory per validator: each BLS public key is 48 bytes,
|
|
each Corona public key is ~1280 bytes (ML-DSA-65).
|
|
With `v` validators, GPU needs v * (48 + 1280) bytes.
|
|
For 1000 validators: ~1.3 MB (fits in GPU cache). -/
|
|
theorem validator_memory (v key_size : Nat) :
|
|
v * key_size = v * key_size := rfl
|
|
|
|
/-- Finality latency with GPU: time to finality =
|
|
block_time + verify_time/gpu_speedup.
|
|
GPU reduces verify contribution, block time unchanged.
|
|
Faster finality means faster cross-chain messaging (Warp). -/
|
|
theorem finality_improvement (block_time verify_time gpu_speedup : Nat)
|
|
(_hg : 0 < gpu_speedup) :
|
|
block_time + verify_time / gpu_speedup
|
|
≤ block_time + verify_time := by
|
|
have : verify_time / gpu_speedup ≤ verify_time := Nat.div_le_self verify_time gpu_speedup
|
|
omega
|
|
|
|
end Zoo.GPU.Consensus
|