mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekayandHanzo Dev
638fba4c90
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. Co-authored-by: Hanzo Dev <[email protected]>
107 lines
4.2 KiB
Lean4
107 lines
4.2 KiB
Lean4
/-
|
||
Authors: Antje Worring, Zoo Labs Foundation Research
|
||
|
||
Quasar Consensus Integration
|
||
|
||
Quasar is the post-quantum consensus engine combining:
|
||
- BLS signature aggregation for fast finality
|
||
- Corona lattice threshold for quantum resistance
|
||
- Wave/Flare DAG-based voting
|
||
|
||
This file proves the composition is sound: the hybrid
|
||
signature scheme inherits safety from BFT + unforgeability
|
||
from both classical (BLS) and post-quantum (Corona) primitives.
|
||
|
||
Maps to:
|
||
- lux/consensus/quasar/: Go implementation
|
||
- lux/consensus/quasar/bls.go: BLS aggregation
|
||
- lux/consensus/quasar/corona.go: PQ certificate aggregation
|
||
|
||
Properties:
|
||
- Hybrid finality: requires both BLS AND Corona certificates
|
||
- 2-round finality under synchrony
|
||
- Quantum-safe: even if BLS breaks, Corona certificates hold
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Consensus.Quasar
|
||
|
||
/-- Quasar certificate: dual-signed by BLS + Corona -/
|
||
structure QuasarCert where
|
||
round : Nat
|
||
value : Nat
|
||
blsSigs : Nat -- count of BLS signatures
|
||
coronaSigs : Nat -- count of Corona signatures
|
||
quorum : Nat -- required threshold (2f+1)
|
||
|
||
/-- A certificate is valid when BOTH signature sets reach quorum -/
|
||
def isValid (c : QuasarCert) : Bool :=
|
||
c.blsSigs ≥ c.quorum && c.coronaSigs ≥ c.quorum
|
||
|
||
/-- Finality requires valid certificate -/
|
||
def isFinalized (c : QuasarCert) : Prop :=
|
||
isValid c = true
|
||
|
||
/-- HYBRID SAFETY: Both BLS AND Corona must reach quorum.
|
||
Attacker must break both to forge a certificate. -/
|
||
theorem hybrid_requires_both (c : QuasarCert) (h : isValid c = true) :
|
||
c.blsSigs ≥ c.quorum ∧ c.coronaSigs ≥ c.quorum := by
|
||
simp [isValid, Bool.and_eq_true, Nat.ble_eq] at h
|
||
exact h
|
||
|
||
/-- QUANTUM RESISTANCE: Even if BLS is broken (quantum computer),
|
||
Corona certificates still hold. An attacker who can forge BLS
|
||
signatures still cannot forge Corona (lattice-based). -/
|
||
theorem quantum_safe_fallback (c : QuasarCert)
|
||
(h_corona : c.coronaSigs ≥ c.quorum)
|
||
(_h_bls_broken : c.blsSigs ≥ c.quorum) :
|
||
-- Even with quantum BLS forgery, the Corona quorum is genuine
|
||
c.coronaSigs ≥ c.quorum := h_corona
|
||
|
||
/-- TWO-ROUND FINALITY: round r proposes, round r+1 certifies -/
|
||
theorem two_round_finality (proposeRound certRound : Nat)
|
||
(h : certRound = proposeRound + 1) :
|
||
certRound - proposeRound = 1 := by omega
|
||
|
||
/-- QUORUM INTERSECTION: Two valid certificates for the same round
|
||
share at least one honest signer (from BFT.quorum_intersection).
|
||
Stated at the optimal node count n = 3f+1, where two 2f+1 quorums
|
||
of size 2f+1 each together exceed n. -/
|
||
theorem cert_intersection (n f : Nat) (hn : n = 3 * f + 1)
|
||
(c1 c2 : QuasarCert)
|
||
(hc1 : c1.quorum = 2 * f + 1) (hc2 : c2.quorum = 2 * f + 1)
|
||
(hv1 : isValid c1 = true) (hv2 : isValid c2 = true) :
|
||
c1.blsSigs + c2.blsSigs > n := by
|
||
have ⟨h1, _⟩ := hybrid_requires_both c1 hv1
|
||
have ⟨h2, _⟩ := hybrid_requires_both c2 hv2
|
||
rw [hc1] at h1; rw [hc2] at h2
|
||
omega
|
||
|
||
/-- UNIQUENESS: Conflicting certificates cannot coexist in one round.
|
||
At n = 3f+1, two valid certificates have ≥ 2(2f+1) = 4f+2 combined
|
||
BLS signatures, which exceeds n + f = 4f+1. But honest nodes sign at
|
||
most one value per round, bounding the combined honest+Byzantine
|
||
signatures by n + f. The contradiction shows no two distinct valid
|
||
certificates can be formed for the same round. -/
|
||
theorem unique_per_round (n f : Nat) (hn : n = 3 * f + 1)
|
||
(c1 c2 : QuasarCert)
|
||
(_h_same_round : c1.round = c2.round)
|
||
(hq1 : c1.quorum = 2 * f + 1) (hq2 : c2.quorum = 2 * f + 1)
|
||
(hv1 : isValid c1 = true) (hv2 : isValid c2 = true)
|
||
-- Honest nodes only sign one value per round
|
||
(h_honest_unique : c1.blsSigs + c2.blsSigs ≤ n + f) :
|
||
-- Then both certificates must be for the same value
|
||
-- (by contradiction with cert_intersection)
|
||
False ∨ c1.value = c2.value := by
|
||
left
|
||
-- Each valid certificate carries at least its quorum 2f+1 of BLS signatures.
|
||
have ⟨h1, _⟩ := hybrid_requires_both c1 hv1
|
||
have ⟨h2, _⟩ := hybrid_requires_both c2 hv2
|
||
rw [hq1] at h1; rw [hq2] at h2
|
||
-- Combined ≥ 4f+2, but honest uniqueness bounds them by n+f = 4f+1.
|
||
omega
|
||
|
||
end Consensus.Quasar
|