mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zeekayandHanzo Dev
46f8ca5fa2
Zero modules are now in no library, down from three. `Contract/ZKSignature.lean` and `Crypto/ZKSignature.lean` were byte-identical and both opened `namespace Crypto.ZKSignature`, so they could not both be imported. Kept the one whose path matches its namespace; nothing imported either. `Crypto.ZKSignature` is now rooted. `Main.lean` stated eight conjuncts. Six were arithmetic facts about `Nat` presented as systems claims: `p * rate ≥ rate` as "GPU EVM linear scaling", `cpu_time / speedup ≤ cpu_time` as "GPU FHE bootstrap speedup", `pairs / cores ≤ pairs` as "GPU DEX pair parallelism", `max a b ≤ a + b` as "hybrid finality", and `t - 1 < t` as threshold secrecy. The eighth was `True`. Its header claimed a 40x FHE bootstrap speedup, which no theorem here establishes — a speedup is a measurement and belongs in a benchmark. It now imports Consensus.BFT and Governance.ZIP, and its conjuncts ARE `quorum_intersection`, `honest_majority_sufficient` and `sufficient_votes_pass`, applied rather than restated, so compilation depends on those proofs. Safety, liveness, threshold unforgeability, post-quantum hardness and FHE correctness are named as deliberately absent, with the reason. Measured after: 592 theorems queried, 566 proved outright against Lean's ambient logic, 26 resting on axioms; 23 declarations carry no content, down from 25; 0 `sorry`. Co-authored-by: Hanzo Dev <[email protected]>
214 lines
3.6 KiB
Lean4
214 lines
3.6 KiB
Lean4
import Lake
|
|
open Lake DSL
|
|
|
|
package zooFormal where
|
|
leanOptions := #[
|
|
⟨`autoImplicit, false⟩
|
|
]
|
|
|
|
-- Zoo-native proofs (AI, agents, ecology, governance)
|
|
|
|
@[default_target]
|
|
lean_lib Contract where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Contract.Bridge,
|
|
`Contract.Token,
|
|
`Contract.Staking,
|
|
`Contract.AMM
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Governance where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Governance.ZIP,
|
|
`Governance.Contribution,
|
|
`Governance.Compensation,
|
|
`Governance.Treasury,
|
|
`Governance.AgentNFT,
|
|
`Governance.DSO
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib AI where
|
|
srcDir := "."
|
|
roots := #[
|
|
`AI.DSO,
|
|
`AI.ExperienceLedger,
|
|
`AI.Gym,
|
|
`AI.Personalization,
|
|
`AI.Embedding,
|
|
`AI.FederatedWildlife,
|
|
`AI.SpeciesClassification
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Agent where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Agent.GRPO,
|
|
`Agent.NFTOwnership,
|
|
`Agent.Gym,
|
|
`Agent.EBM,
|
|
`Agent.LogicAgent,
|
|
`Agent.FunctionalAgent,
|
|
`Agent.DeltaSoup,
|
|
`Agent.RewardShaping
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Token where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Token.ExperienceLedger
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Data where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Data.Commons
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Ecology where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Ecology.Satellite
|
|
]
|
|
|
|
-- Infrastructure proofs (from Lux — shared L1 foundation)
|
|
|
|
@[default_target]
|
|
lean_lib Consensus where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Consensus.PoAI,
|
|
`Consensus.BFT,
|
|
`Consensus.Safety,
|
|
`Consensus.Liveness,
|
|
`Consensus.Finality,
|
|
`Consensus.Validator,
|
|
`Consensus.Quasar
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Crypto where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Crypto.BLS,
|
|
`Crypto.FROST,
|
|
`Crypto.Hybrid,
|
|
`Crypto.MLDSA,
|
|
`Crypto.MLKEM,
|
|
`Crypto.Corona,
|
|
`Crypto.SLHDSA,
|
|
`Crypto.VerkleTree,
|
|
`Crypto.FHE.CKKS,
|
|
`Crypto.FHE.TFHE,
|
|
`Crypto.Threshold.CGGMP21,
|
|
`Crypto.Threshold.Composition,
|
|
`Crypto.Threshold.LSS,
|
|
`Crypto.ZKSignature
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib DeFi where
|
|
srcDir := "."
|
|
roots := #[
|
|
`DeFi.AMM,
|
|
`DeFi.ImpactBonds,
|
|
`DeFi.CarbonCredits,
|
|
`DeFi.FeeModel,
|
|
`DeFi.FlashLoan,
|
|
`DeFi.Governance,
|
|
`DeFi.HFT,
|
|
`DeFi.LiquidStaking,
|
|
`DeFi.OrderBook,
|
|
`DeFi.Router
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Bridge where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Bridge.Teleport
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Build where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Build.Attestation,
|
|
`Build.Coeffect,
|
|
`Build.Ecosystem,
|
|
`Build.Reproducibility
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Compute where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Compute.CrossChain
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Network where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Network.PeerDiscovery
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Protocol where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Protocol.Field,
|
|
`Protocol.Flare,
|
|
`Protocol.Handshake,
|
|
`Protocol.Nebula,
|
|
`Protocol.Nova,
|
|
`Protocol.Photon,
|
|
`Protocol.Prism,
|
|
`Protocol.Quasar,
|
|
`Protocol.Ray,
|
|
`Protocol.Wave
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Trust where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Trust.Authority,
|
|
`Trust.Revocation,
|
|
`Trust.Vouch
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Warp where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Warp.Delivery,
|
|
`Warp.Ordering,
|
|
`Warp.Security
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Main where
|
|
srcDir := "."
|
|
roots := #[`Main]
|
|
|
|
@[default_target]
|
|
lean_lib GPU where
|
|
srcDir := "."
|
|
roots := #[
|
|
`GPU.EVMScaling,
|
|
`GPU.FHEScaling,
|
|
`GPU.ConsensusScaling,
|
|
`GPU.DEXScaling
|
|
]
|
|
|
|
require mathlib from git
|
|
"https://github.com/leanprover-community/mathlib4" @ "v4.14.0"
|