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]>