mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
de9a19550c
Zero modules are now in no library, down from ten. The seven with content are rooted — Corona's Unforgeability, Shamir and OutputInterchange, Magnetar's Unforgeability and OutputInterchange, Precompile.P3Q, Compute.AIMint — so CI type-checks them and the axiom and vacuity reports cover them for the first time. Deleted three artifacts that described things that do not exist: `pulsar/hash-suite-separation.tex` proved a separation theorem about a selectable Pulsar-SHA3 / Pulsar-BLAKE3 hash suite. `HashSuiteID` and `BLAKE3` appear nowhere in `pulsar/pkg/pulsar`, and pulsar's own DD-002 records the decision as "No BLAKE3", rationale "BLAKE3 is not on the list. Including BLAKE3 in the NIST submission profile is a strategic liability." The theorem's premise is counterfactual. `lean/Crypto/Pulsar/dkg2.lean` carried Corona's parameters — q = 0x1000000004A01, M=8, N=7, sigma_E 6.108, the `corona.dkg2.*` domain tags — under a Pulsar namespace, calling them "Pulsar production" and "Pulsar canonical ring". Pulsar's ring is pulsar-mldsa65-fips204, K=6, L=5, q = 8380417. Seven of its sixteen declarations stated `True`, including `mlwe_b_hard` and `msis_ab_hard`, so the Pedersen hiding and binding theorems reduced to nothing. It cited `pulsar/dkg2/dkg2.go`, which does not exist. `lean/Crypto/Corona/dkg2.lean` modelled `luxfi/corona/dkg2/dkg2.go`, a package deleted from corona at `2cecc08` and absent at HEAD. `Crypto/CGGMP21.lean` and `Crypto/Threshold/CGGMP21.lean` both opened `namespace Crypto.Threshold.CGGMP21`, so rooting the first broke the import of the second. The orphan at the shorter path was the larger file and a strict superset — five extra results on Paillier homomorphism, Lagrange and Shamir evaluation. Consolidated into the rooted path; one file per namespace. `Main.lean` stated four conjuncts, of which `spreadBps * volumeUSD / 10000 >= 0` holds of every `Nat` and the fourth was `True`. Its header said "if this file compiles, the following hold: consensus is safe and live under BFT assumptions" across ten libraries, while it imported only Mathlib — no consensus module, no crypto module. It now imports Consensus.BFT and its conjuncts ARE `quorum_intersection` and `honest_majority_sufficient`, applied rather than restated, so compilation depends on those proofs. Safety, liveness and post-quantum hardness are named as deliberately absent, with the reason. Measured after: 750 theorems queried, 620 proved outright against Lean's ambient logic, 130 resting on axioms; 62 declarations carry no content, down from 75; 0 `sorry`. Co-authored-by: Hanzo Dev <[email protected]>
223 lines
4.2 KiB
Lean4
223 lines
4.2 KiB
Lean4
import Lake
|
|
open Lake DSL
|
|
|
|
package luxFormal where
|
|
leanOptions := #[
|
|
⟨`autoImplicit, false⟩
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Consensus where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Consensus.Safety,
|
|
`Consensus.Liveness,
|
|
`Consensus.BFT,
|
|
`Consensus.Quasar,
|
|
`Consensus.Finality,
|
|
`Consensus.Validator,
|
|
`Consensus.ThresholdProof,
|
|
`Consensus.PreferenceStability,
|
|
`Consensus.DAGEVM,
|
|
`Consensus.DAGZChain,
|
|
`Consensus.PQZParallel
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Protocol where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Protocol.Wave,
|
|
`Protocol.Flare,
|
|
`Protocol.Ray,
|
|
`Protocol.Field,
|
|
`Protocol.Quasar,
|
|
`Protocol.Nova,
|
|
`Protocol.Nebula,
|
|
`Protocol.Photon,
|
|
`Protocol.Prism,
|
|
`Protocol.Handshake
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Crypto where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Crypto.Age,
|
|
`Crypto.BLS,
|
|
`Crypto.DEKDerivation,
|
|
`Crypto.FROST,
|
|
`Crypto.Corona,
|
|
`Crypto.MLDSA,
|
|
`Crypto.Hybrid,
|
|
`Crypto.SLHDSA,
|
|
`Crypto.MLKEM,
|
|
`Crypto.FHE.TFHE,
|
|
`Crypto.FHE.CKKS,
|
|
`Crypto.Threshold.CGGMP21,
|
|
`Crypto.Threshold.LSS,
|
|
`Crypto.Threshold.Composition,
|
|
`Crypto.VerkleTree,
|
|
`Crypto.ThresholdDecrypt,
|
|
`Crypto.NonCustodial,
|
|
`Crypto.HashChainIntegrity,
|
|
`Crypto.HSM,
|
|
`Crypto.Precompile.BLS12381,
|
|
`Crypto.Precompile.BabyJubjub,
|
|
`Crypto.Precompile.Curve25519,
|
|
`Crypto.Precompile.Pasta,
|
|
`Crypto.Precompile.X25519,
|
|
`Crypto.Precompile.XWing,
|
|
`Crypto.Precompile.AES256GCM,
|
|
`Crypto.Precompile.ChaCha20Poly1305,
|
|
`Crypto.Precompile.KZG4844,
|
|
`Crypto.Precompile.Pedersen,
|
|
`Crypto.Precompile.Poseidon2,
|
|
`Crypto.Precompile.ECIES,
|
|
`Crypto.Precompile.HPKE,
|
|
`Crypto.Precompile.Secp256r1,
|
|
`Crypto.Precompile.Ed25519,
|
|
`Crypto.Precompile.SR25519,
|
|
`Crypto.Precompile.BLAKE3,
|
|
`Crypto.Threshold.Reshare,
|
|
`Crypto.ZKSignature,
|
|
`Crypto.HQC,
|
|
`Crypto.Magnetar,
|
|
`Crypto.Threshold_Lagrange,
|
|
`Crypto.Pulsar.OutputInterchange,
|
|
`Crypto.Pulsar.Shamir,
|
|
`Crypto.Pulsar.Unforgeability,
|
|
`Crypto.Pulsar.BoundaryClearance,
|
|
`Crypto.Pulsar.NoLeakAggregate,
|
|
`Crypto.Corona.NoLeakAggregate,
|
|
`Crypto.Corona.Unforgeability,
|
|
`Crypto.Corona.Shamir,
|
|
`Crypto.Corona.OutputInterchange,
|
|
`Crypto.Magnetar.Unforgeability,
|
|
`Crypto.Magnetar.OutputInterchange,
|
|
`Crypto.Precompile.P3Q
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Storage where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Storage.Replicate,
|
|
`Storage.ZapDB
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Warp where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Warp.Delivery,
|
|
`Warp.Ordering,
|
|
`Warp.Security
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Trust where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Trust.Authority,
|
|
`Trust.Vouch,
|
|
`Trust.Revocation
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Build where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Build.Coeffect,
|
|
`Build.Attestation,
|
|
`Build.Ecosystem,
|
|
`Build.Reproducibility
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Compute where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Compute.CrossChain,
|
|
`Compute.AIMint
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib DeFi where
|
|
srcDir := "."
|
|
roots := #[
|
|
`DeFi.OrderBook,
|
|
`DeFi.AMM,
|
|
`DeFi.HFT,
|
|
`DeFi.FeeModel,
|
|
`DeFi.LiquidStaking,
|
|
`DeFi.Router,
|
|
`DeFi.FlashLoan,
|
|
`DeFi.Governance
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Network where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Network.PeerDiscovery
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Compliance where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Compliance.ERC3643
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Bridge where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Bridge.Teleport,
|
|
`Bridge.FillIntegrity,
|
|
`Bridge.OmnichainRouter,
|
|
`Bridge.ShariaFilter,
|
|
`Bridge.YieldVault
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib GPU where
|
|
srcDir := "."
|
|
roots := #[
|
|
`GPU.EVMScaling,
|
|
`GPU.FHEScaling,
|
|
`GPU.ConsensusScaling,
|
|
`GPU.DEXScaling
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Quasar where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Quasar.Consensus
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Vault where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Vault.KeyIsolation
|
|
]
|
|
|
|
@[default_target]
|
|
lean_lib Main where
|
|
srcDir := "."
|
|
roots := #[`Main]
|
|
|
|
@[default_target]
|
|
lean_lib StrictE2EPQ where
|
|
srcDir := "."
|
|
roots := #[
|
|
`StrictE2EPQ.Profile,
|
|
`StrictE2EPQ.Coverage
|
|
]
|
|
|
|
require mathlib from git
|
|
"https://github.com/leanprover-community/mathlib4" @ "v4.14.0"
|