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]>
Pulsar proofs
LaTeX theorem statements + proofs for Pulsar (Module-LWE), the
FIPS 204-byte-equal threshold scheme. Its sibling is Corona, a
separate Module-LWE threshold scheme (the Ringtail-derived parameter
regime; not FIPS-byte-equal). Each file is included from
~/work/lux/pulsar/spec/pulsar.tex or from a paper.
| file | claim |
|---|---|
unforgeability.tex |
TS-UF reduction to MLWE + MSIS + ML-DSA EUF-CMA |
scaling.tex |
Concrete claims at the extreme committee size N* = 1,111,111 |
output-interchangeability.tex |
Class N1 manifesto: Pulsar signatures verify under unmodified FIPS 204 |
dkg-soundness.tex |
DKG soundness + share privacy |
reshare-preservation.tex |
Reshare preserves pk, soundness, privacy under beacon-randomised quorum |
grouped-sortition.tex |
Pulsar (3,2) × Quasar sortition × P3Q rollup composition (the production 1.1M-validator stack); fully PQ end-to-end |
The Corona proofs (Module-LWE, Ringtail-derived parameter regime,
module dims M=8/N=7 over R_q = Z_q[X]/(X^256+1), q 48-bit) live with
the lean/Crypto/Corona/ tree and luxfi/corona. Do not confuse the
two: Corona has its own large parameter set and verifier and is not
FIPS-byte-equal; Pulsar (this directory) operates over R_q^k at the
FIPS 204 ML-DSA-65 parameters and verifies under the FIPS 204 verifier
verbatim. Both are Module-LWE — they differ in parameter regime and
lifecycle, not lattice family.
Mechanization status
- LaTeX statements: all five files complete.
- Lean 4:
lean/Crypto/Pulsar/skeleton in this repository. The reductions import the FIPS 204 ML-DSA EUF-CMA axiom fromlean/Crypto/MLDSA.leanand the MLWE / MSIS hardness axioms fromlean/Crypto/Pulsar/dkg2.lean. - Tamarin: out of scope (Tamarin targets the auth-permit protocol, not the threshold cryptography).
- Halmos: out of scope (Halmos targets Solidity invariants).
Reference implementation cross-check
| theorem | reference implementation gate |
|---|---|
thm:pulsar-tsuf |
ref/go/pkg/pulsar/threshold_test.go |
thm:pulsar-scales-n |
ref/go/pkg/pulsar/shamir_gfq_test.go (boundary committees) |
prop:pulsar-correct-at-N-star |
ref/go/pkg/pulsar/largeshamir_test.go:TestLargeShamir_EvalAtTargetCommitteeSize |
thm:pulsar-output-interchange |
ref/go/pkg/pulsar/kat_test.go:TestKAT_ThresholdSign_Replay |
thm:pulsar-dkg-sound |
ref/go/pkg/pulsar/dkg_test.go |
thm:pulsar-reshare-pkinv |
ref/go/pkg/pulsar/reshare_test.go |