mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zooqueen
506123454e
Adds two Lean 4 + Mathlib theories that replace the reconstruct-then-sign
misdirection in the Pulsar/Corona EasyCrypt byte-equality cones with the
HONEST no-leak identity, machine-checked on this host (lake build green,
0 sorry; #print axioms shows only [propext, Classical.choice, Quot.sound]
-- no sorryAx).
Crypto/Pulsar/NoLeakAggregate.lean:
- z_aggregate_no_reconstruct: the masked Lagrange z-aggregate equals
central z = (interp y).eval0 + c*f.eval0; the secret polynomial f
(master s1) is NEVER formed, only f.eval 0 inside the already-public z.
- z_aggregate_depends_only_on_secret: aggregate is a function of f.eval 0
+ public (y,c); the sharing randomness is invisible.
- hint_highbits_stable_under_hidden_shift / hint_is_fips_hint: re-exports
of the machine-checked BoundaryClearance facts -- the hint is recovered
from PUBLIC w' only, HighBits stable under the hidden c*s2 shift.
- NoLeakReduction + no_leak_under_standard_assumptions: the residual is a
STANDARD Module-LWE/Module-SIS simulation reduction, NOT a reconstruct.
Crypto/Corona/NoLeakAggregate.lean:
- pairwise_mask_telescopes: Sum_i (maskPrime_i - mask_i) = 0 by Fubini
reindex (the Corona telescoping pairwise-PRF mask cancellation).
- summed_response_is_mask_free: Sum_i z_i = Sum_i base_i (masks vanish).
- secret_aggregate_no_reconstruct: surviving c*Sum_i lambda_i*s_i = c*s
by Lagrange-at-0, master secret never formed.
- NoLeakReduction + no_leak_under_standard_assumptions: same standard
Module-LWE/Module-SIS residual.
The correctness cores depend on NO opaque assumption (the Module-LWE/MSIS
opaques are used only by the residual-reduction packaging). Both are the
machine-checked anchors for the new Pulsar_N1_NoLeak.ec / Corona_N1_NoLeak.ec
EC theories.
197 lines
3.7 KiB
Lean4
197 lines
3.7 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
|
|
]
|
|
|
|
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
|
|
]
|
|
|
|
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.dkg2,
|
|
`Crypto.Pulsar.BoundaryClearance,
|
|
`Crypto.Pulsar.NoLeakAggregate,
|
|
`Crypto.Corona.NoLeakAggregate
|
|
]
|
|
|
|
lean_lib Storage where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Storage.Replicate,
|
|
`Storage.ZapDB
|
|
]
|
|
|
|
lean_lib Warp where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Warp.Delivery,
|
|
`Warp.Ordering,
|
|
`Warp.Security
|
|
]
|
|
|
|
lean_lib Trust where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Trust.Authority,
|
|
`Trust.Vouch,
|
|
`Trust.Revocation
|
|
]
|
|
|
|
lean_lib Build where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Build.Coeffect,
|
|
`Build.Attestation,
|
|
`Build.Ecosystem,
|
|
`Build.Reproducibility
|
|
]
|
|
|
|
lean_lib Compute where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Compute.CrossChain
|
|
]
|
|
|
|
lean_lib DeFi where
|
|
srcDir := "."
|
|
roots := #[
|
|
`DeFi.OrderBook,
|
|
`DeFi.AMM,
|
|
`DeFi.HFT,
|
|
`DeFi.FeeModel,
|
|
`DeFi.LiquidStaking,
|
|
`DeFi.Router,
|
|
`DeFi.FlashLoan,
|
|
`DeFi.Governance
|
|
]
|
|
|
|
lean_lib Network where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Network.PeerDiscovery
|
|
]
|
|
|
|
lean_lib Compliance where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Compliance.ERC3643
|
|
]
|
|
|
|
lean_lib Bridge where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Bridge.Teleport,
|
|
`Bridge.FillIntegrity,
|
|
`Bridge.OmnichainRouter,
|
|
`Bridge.ShariaFilter,
|
|
`Bridge.YieldVault
|
|
]
|
|
|
|
lean_lib GPU where
|
|
srcDir := "."
|
|
roots := #[
|
|
`GPU.EVMScaling,
|
|
`GPU.FHEScaling,
|
|
`GPU.ConsensusScaling,
|
|
`GPU.DEXScaling
|
|
]
|
|
|
|
lean_lib Quasar where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Quasar.Consensus
|
|
]
|
|
|
|
lean_lib Vault where
|
|
srcDir := "."
|
|
roots := #[
|
|
`Vault.KeyIsolation
|
|
]
|
|
|
|
lean_lib StrictE2EPQ where
|
|
srcDir := "."
|
|
roots := #[
|
|
`StrictE2EPQ.Profile,
|
|
`StrictE2EPQ.Coverage
|
|
]
|
|
|
|
require mathlib from git
|
|
"https://github.com/leanprover-community/mathlib4" @ "v4.14.0"
|