mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekay
c86eec94cb
Local zoo/formal was a stale parallel checkout that pointed at
zoo-labs/formal (non-existent); the canonical remote is
zooai/proofs. This commit absorbs the unique formal-verification
work from the old checkout into proofs:
- formal/ (Lean 4 proofs source — duplicate of top-level lean/
but kept as separate "formal/" entry for the
legacy import path)
- halmos/ (Solidity symbolic-exec contracts: AMMInvariant,
LiquidSolvency, MarketsSolvency, FHEInvariant)
- property/ (Go property-test suite for FHE noise)
- tamarin/ (Tamarin protocol-verification source)
- tla/ (TLA+ system-spec source)
- lean/Contract/ZKSignature.lean (unique, not in proofs/lean)
- lean/Crypto/ZKSignature.lean (unique, not in proofs/lean)
- FORMAL_VERIFICATION.md (preserved from the old README)
- LLM-formal.md (preserved from the old LLM.md)
The duplicate folder /Users/z/work/zoo/formal is now deleted on
disk. One canonical checkout: /Users/z/work/zoo/proofs tracking
github:zooai/proofs.
95 lines
3.6 KiB
Lean4
95 lines
3.6 KiB
Lean4
/-
|
||
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) -/
|
||
theorem cert_intersection (n f : Nat) (hf : 3 * f < n) (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: At most one value can be certified per round
|
||
(follows from quorum intersection + BFT honest majority) -/
|
||
theorem unique_per_round (n f : Nat) (hf : 3 * f < n) (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 sign at most one value per round (pigeonhole on n signers)
|
||
(h_honest_unique : c1.blsSigs + c2.blsSigs ≤ n) :
|
||
-- Then both certificates must be for the same value
|
||
-- (by contradiction with cert_intersection)
|
||
False ∨ c1.value = c2.value := by
|
||
left
|
||
have h_inter := cert_intersection n f hf hn c1 c2 hq1 hq2 hv1 hv2
|
||
omega
|
||
|
||
end Consensus.Quasar
|