Pulsar — NIST MPTC submission package

Threshold ML-DSA — a 2-round threshold signing and DKG system whose generated signatures are verifiable by unmodified FIPS 204 ML-DSA verification. Targeting NIST MPTC Class N1 (signing) + N4 (ML keygen / DKG).

This repository is the active NIST MPTC submission package for Pulsar and the canonical home for the submission artifacts (spec, KAT vectors, reference implementation, interop harness, ct analysis, scripts). The submission tarball for NIST is cut from a tag on main at deadline — the repository itself stays active so reviewer feedback and post- submission patches land here, not in a fork.

The production Go library has split into its own stable module identity (github.com/luxfi/pulsar / github.com/luxfi/corona); this repository keeps the original github.com/luxfi/pulsar module path because that is the identifier NIST receives and reviews against.

Library identities (post-2026 split)

Pulsar is the Module-LWE threshold ML-DSA construction. The 2-round threshold protocol structure operates on ML-DSA-65's polynomial-vector- over-R_q algebra so the per-party-aggregated signature is bit-identical to a single-party FIPS 204 signature on the same message + public key.

Aggregator-honesty caveat (v0.2 vs v0.3). Bit-identity to a single-party FIPS 204 signature is achieved without master-secret reconstruction only by the v0.3 algebraic aggregator (ref/go/pkg/pulsar/threshold_v03.go::AlgebraicAggregate). The v0.2 transitional aggregator (ref/go/pkg/pulsar/threshold_v02.go::TransitionalAggregate) reconstructs the master ML-DSA secret in aggregator memory and calls mldsaSign(setup.SkBytes, …) (threshold_v02.go:1170) — output byte-equality holds but TCB at sign time includes the aggregator. The N1 submission targets the v0.3 aggregator; v0.2 is documented for protocol-evolution traceability. PULSAR-V03-1 in BLOCKERS.md tracks the v0.3 byte-equality closure (CLOSED in v1.0.20).

Repository	Module path	Role
luxfi/pulsar (this repo)	github.com/luxfi/pulsar	Active NIST MPTC submission package
luxfi/pulsar	github.com/luxfi/pulsar	Production Module-LWE Go library
luxfi/corona	github.com/luxfi/corona	Production Ring-LWE Go library (sibling kernel)

The module path inside this submission package remains github.com/luxfi/pulsar because that is the identifier NIST receives and reviews against the submitted KAT vectors and spec. Downstream consumers who want the live production library should pin github.com/luxfi/[email protected] (Module-LWE) or github.com/luxfi/[email protected] (Ring-LWE) instead.

Status: Research / Reference (not production hardened, not FIPS validated). NIST-profile vectors use SHAKE / cSHAKE / KMAC. Any BLAKE3 deltas are experimental and out-of-scope for the MPTC submission.

High-assurance headline

All local EasyCrypt theorem bodies are admit-free, per-push gates are green, threshold Jasmin CT is blocking, fuzz / KAT / interop / dudect gates are wired at documented budgets, and the extracted N1 theorem has no section-local module-contract axioms. The remaining implementation-refinement assumptions have been progressively decomposed into strictly narrower axioms with a committed proof roadmap; the Lean↔EC algebraic bridge is named, cited, and CI-guarded.

The dependency graph is acyclic and each EC file owns one concern:

Memory             → pure byte-memory model
Signature_Codec    → FIPS signature packing
Combine_Layout     → combine ABI only
Sign_Layout        → sign ABI only
Combine_Refinement → combine byte-walk only
Sign_Refinement    → sign byte-walk + ghost contract only
Combine_Wrapper    → combine wrapper bridge only
Sign_Wrapper       → sign wrapper bridge only
Extracted          → final composition theorem only

Hard boundary (counts verified against proofs/easycrypt/*.ec axiom/declare axiom declarations as of HEAD):

• 14 implementation-refinement axioms in the refinement files (counts authoritative from Pulsar_N1_{Combine,Sign}_Refinement.ec):
  • 4 stage-extraction byte-walks (combine_body_{z_via_aggregation,partial_responses}_spec, sign_body_{y,cs1}_spec)
  • 4 w-decomposition byte-walks ({combine,sign}_body_{matrix_a,mask_y}_spec; *_body_w_spec is now derived)
  • 2 w_low byte-walks for the h-stage ({combine,sign}_body_w_low_spec; *_body_h_spec derived via make_hint_of_w structural composition)
  • 4 ExternalMu codec-layout axioms (combine: 3 per-range sub-axioms over the protocol-witness buffer; sign: 1 collapsed sign_layout_m_buffer_external_mu since sign owns m_ptr/ctx_ptr in its layout)
• 1 codec-roundtrip axiom in Pulsar_N1.ec (pack_unpack_n1_signature_roundtrip)
• 5 Lean-bridged algebraic axioms, cited inline and CI-guarded (see proofs/lean-easycrypt-bridge.md: lagrange_inverse_eval, reconstruct_linear, shamir_correct, add_share_zeroR, threshold_partial_response_identity)
• 2 honest-execution no-reject post-conditions ({combine,sign}_no_reject_on_accepted_honest_layout) gated on accept_signing_attempt — protocol-level, not byte-walks
• 0 admits in any .ec file
• 0 section-local module-contract axioms in the extracted N1 corollary

See proofs/easycrypt/README.md for the per-file dashboard and proofs/lean-easycrypt-bridge.md for the Lean↔EC correspondence.

The next implementation-refinement decomposition target is combine_body_partial_responses_spec — the only remaining per-party byte-walk on the combine side over Round-2 messages. Closing it via a matrix_a/mask_y-style narrower split is the v13 roadmap.

Why

NIST FIPS 204 (ML-DSA) is the only NIST-approved post-quantum digital signature in 2026. Threshold variants of ML-DSA are not yet standardized — NIST's Multi-Party Threshold Cryptography project is collecting them now (IR 8214C, January 2026; first call package deadline expected 2026-Nov-16).

Pulsar aims to enter that process with a credible, output-interchangeable threshold ML-DSA candidate. The 2-round threshold protocol skeleton is the same one Lux ships in production for Ring-LWE (see luxfi/corona), retargeted to the Module-LWE primitives ML-DSA itself uses; the resulting per-party- aggregated signature (under the v0.3 algebraic aggregator) is bit-identical to a single-party FIPS 204 ML-DSA signature on the same message + public key.

The win, if Pulsar's Sign output is byte-equal to FIPS 204 Sign:

• Threshold-produced signatures verify under unmodified FIPS 204 verifiers.
• Existing FIPS-validated ML-DSA modules (BoringSSL FIPS, AWS-LC, OpenSSL 3.0 PQ provider) consume Pulsar certs without code changes.
• The threshold layer can be Class-N-claimed at NIST without a parallel algorithm standardization track.

Repository layout

pulsar/
├── BLOCKERS.md               open-issue tracker (currently: PULSAR-V03-1 root-cause + closure postmortem, CLOSED in v1.0.20)
├── docs/                     human-readable design notes
│   ├── threat-model.md
│   ├── nist-mptc-category.md
│   ├── design-decisions.md
│   └── patent-notes-draft.md
├── spec/                     LaTeX technical specification (MPTC package)
│   ├── pulsar.tex          main spec
│   ├── security-games.tex    EUF-CMA / TS-UF / robustness / adaptive corr.
│   ├── system-model.tex      network / setup / abort / preprocessing
│   ├── parameters.tex        concrete parameter sets, lattice-estimator
│   └── references.bib
├── ref/
│   ├── go/                   reference implementation (Go, no assembly)
│   │   ├── cmd/genkat/       KAT generator binary
│   │   └── pkg/pulsar/       single flat package: keygen, sign, DKG, reshare,
│   │                          threshold (v0.1 / v0.2 transitional / v0.3
│   │                          algebraic), large-committee path, abort tape,
│   │                          KAT replay, fuzz
│   └── c/                    conformance implementation (post-encoding-freeze)
├── vectors/                  Known Answer Tests (KATs)
│   ├── kat-v1.json           input/output vectors per MPTC §IO-Testing
│   ├── kat-v1.rsp            CAVS-style response file (compatibility)
│   └── transcripts/          full-protocol KATs (n,t sweeps)
├── bench/                    reproducible benchmark harness
├── test/                     fuzz / negative / interoperability tests
├── ct/dudect/                constant-time analysis harness
├── estimator/                lattice-estimator parameter scripts
├── jasmin/                   high-assurance Jasmin sources (initial track)
│   ├── ml-dsa-65/             libjade single-party baseline (fetched on demand)
│   └── threshold/             Pulsar threshold layer (round1 + round2 + combine implemented)
├── proofs/easycrypt/         high-assurance EasyCrypt theories
│   ├── Pulsar_N1.ec                       Class N1 protocol-level spec + generic byte-equality theorem
│   ├── Pulsar_N4.ec                       Class N4 reshare public-key preservation
│   ├── Pulsar_N1_Memory.ec                byte-memory model (0 axioms)
│   ├── Pulsar_N1_Signature_Codec.ec       FIPS 204 sig codec
│   ├── Pulsar_N1_Combine_Layout.ec        combine ABI byte layout
│   ├── Pulsar_N1_Sign_Layout.ec           libjade sign ABI byte layout
│   ├── Pulsar_N1_Combine_Refinement.ec    combine refinement scaffold
│   ├── Pulsar_N1_Sign_Refinement.ec       sign refinement scaffold + ctx/rho_rnd ghost contract
│   ├── Pulsar_N1_Combine_Wrapper.ec       combine wrapper module + bridge lemma
│   ├── Pulsar_N1_Sign_Wrapper.ec          sign wrapper module + bridge lemma
│   ├── Pulsar_N1_Extracted.ec             concrete extracted N1 byte-equality corollary
│   ├── lemmas/MLDSA65_Functional.ec       FIPS 204 functional ops
│   ├── lemmas/Pulsar_CT.ec                constant-time obligations
│   └── README.md                          trust-boundary dashboard + per-file concerns
├── proofs/lean-easycrypt-bridge.md        Lean↔EC algebraic-bridge correspondence
├── scripts/
│   ├── check-high-assurance.sh            per-push proof gate orchestrator
│   ├── test.sh                            per-push test gate orchestrator
│   ├── nightly.sh                         cron-scheduled REAL-budget gate
│   │                                        (1h fuzz + 10^9 dudect)
│   ├── check-lean-bridge.sh               Lean↔EC bridge guard
│   ├── checks/                            per-check scripts (independently runnable)
│   │   ├── jasmin.sh, ec-{admits,compile,regressions,refinement-scaffold}.sh,
│   │   ├── extraction.sh
│   │   └── test/{go-unit,no-secret-logs,kat,interop}.sh
│   └── build.sh / bench.sh / sbom.sh / gen_vectors.sh / extract-jasmin-ec.sh
└── go.mod

Quickstart

The repository is live and self-validating. A fresh clone runs the full per-push submission gate end-to-end in under 60 seconds:

git clone https://github.com/luxfi/pulsar
cd pulsar
./scripts/build.sh                  # Go ref + spec PDF (MacTeX / TeX Live)
./scripts/test.sh                   # Go unit + DD-007 linter + KAT replay
                                    # + Class N1 interop
./scripts/gen_vectors.sh            # deterministic KAT regen
./scripts/check-high-assurance.sh   # Jasmin + EasyCrypt + Lean↔EC bridge guard
                                    # (skips per-tool if not installed)
./scripts/bench.sh                  # signing / verification benchmarks

Each per-push script is an orchestrator that sequences per-check scripts under scripts/checks/ (and scripts/checks/test/). Per-check scripts are independently runnable for fast iteration:

bash scripts/checks/ec-compile.sh        # just the EC compile gate
bash scripts/checks/jasmin.sh            # just jasminc + jasmin-ct
bash scripts/checks/test/kat.sh          # just KAT replay

build.sh, test.sh, and check-high-assurance.sh exit non-zero on any failure. Reproducibility is the load-bearing CI invariant. The per-push gates run real-budget checks only — no smoke tests; the fuzz + dudect REAL-budget runs live in the nightly gate (hours, cron-scheduled):

./scripts/nightly.sh                # 1h-per-target parser fuzz
                                    # + 1h differential fuzz
                                    # + 10^9-sample dudect (per target)

NIST MPTC submission

package element	location	status
Technical Specification	spec/pulsar.{tex,pdf} (1,633-line LaTeX → 577 KB PDF)	drafted; encoding freeze 2026-Aug
Reference Implementation	ref/go/pkg/pulsar/ (83.9% statement coverage)	shipped
KAT vectors	vectors/{dkg,keygen,sign,threshold-sign,verify}.json	deterministic from seed
Class N1 E2E interop	test/interoperability/n1_class_test.go (19 subtests across TestN1_{SinglePartySignatures,ThresholdSignatures}_VerifyUnderFIPS204 + TestN1_{TamperedSignatures,WrongMessage}_Rejected, all PASS vs cloudflare/circl)	passing
Symbolic / Lean proofs	~/work/lux/proofs/lean/Crypto/Pulsar/{dkg2,OutputInterchange,Shamir,Unforgeability}.lean + Crypto/Threshold_Lagrange.lean (5 files, zero sorry)	mechanized
Constant-time analysis	ct/dudect/	harness present; results TBD
Jasmin high-assurance	jasmin/{ml-dsa-65,threshold,lib}/	libjade pinned at 9426b32; round1 + round2 + combine implemented (~2,600 lines threshold + lib)
EasyCrypt theories	proofs/easycrypt/Pulsar_{N1,N4}.ec + lemmas/Pulsar_CT.ec + per-side {Layout,Refinement,Wrapper} + Pulsar_N1_Extracted.ec	0 admits across all .ec files; 14 narrow implementation-refinement axioms + 1 codec-roundtrip + 5 Lean-bridged + 2 honest-execution post-conditions (see Hard boundary)
Report on Experimental Evaluation	bench/results/REPORT.md	TBD
Patent posture	docs/patent-notes-draft.md	drafted
License	LICENSE (Apache-2.0)	✓
Build/test/bench scripts	scripts/	shipped
SUBMISSION cover sheet	SUBMISSION.md	shipped

Target dates:

• 2026-Jul-20 preview writeup (NIST third preview deadline)
• 2026-Nov-16 package submission (NIST first call deadline; submission tag submission- cut from main)

Relationship to upstream

Scope of this submission. Pulsar is the standalone NIST MPTC submission for the Module-LWE threshold ML-DSA construction. The spec, KAT vectors, reference implementation, and proofs are self-contained. Reviewers do not need to fetch any sibling repository to evaluate the submission.

Earlier R-LWE work. The 2-round threshold construction line begins with Boschini–Kaviani–Lai–Malavolta–Takahashi–Tibouchi's Ring-LWE paper (ePrint 2024/1113). The production R-LWE library Lux deploys is luxfi/corona — same 2-round threshold algorithm retargeted at production lifecycle (Pedersen DKG over R_q with proper hiding + proactive resharing). Corona and Pulsar are independent libraries with no shared types; Pulsar is reviewable on its own merits and Corona is documented separately.

repo	role	lattice basis	hash family
luxfi/corona	production R-LWE threshold ML-DSA — Pedersen DKG over R_q + proactive resharing	Ring-LWE (R_q)	SHA-3 / cSHAKE256 (SP 800-185)
luxfi/pulsar	production M-LWE threshold ML-DSA — same protocol skeleton retargeted to ML-DSA's polynomial-vector-over-R_q^k algebra; output byte-equal to FIPS 204 ML-DSA	Module-LWE (R_q^k)	SHA-3 / cSHAKE256 (SP 800-185)
luxfi/pulsar (this repo)	NIST MPTC submission package for the M-LWE construction — frozen spec, KATs, reference impl, interop harness, proofs	Module-LWE (R_q^k)	SHA-3 / SHAKE256 (NIST profile) only

Optional layered defence on a downstream chain. A downstream consumer (e.g. Lux's primary-network QuasarCert) MAY combine Corona (Ring-LWE) and Pulsar (Module-LWE) as a Double Lattice PQ pair so a break in one lattice family does not break finality. That layered combination is the consumer's design choice and is not part of this submission. Pulsar stands alone as an MPTC Class N1 + N4 candidate.

Where the identity rollup lives

Pulsar is just the threshold sign + DKG layer. The per-validator ML-DSA-65 identity attestation that QuasarCert separately carries (MLDSARollup) is succinct via STARK / FRI through the P3Q backend — Lux's Plonky3 fork with a cSHAKE256 Merkle commitment. P3Q is post-quantum end-to-end (no Groth16/BN254 wrapper; no KZG; no pairings). The rollup statement is

∀ i ∈ [N]: ML-DSA.Verify(mldsa_pk_i, msg, mldsa_σ_i) = 1

and the resulting proof is constant in validator count. Specs: ProofPolicySTARKFRISHA3PQ (0x10) + ProofBackendP3QSTARKFRISHA3 (0x22) in github.com/luxfi/consensus/config/pq_mode.go. The historic "Z-Chain Groth16 / BN254" framing was retired alongside the classical-curve rip in 2026-Q2; any residual reference in this package's older drafts is being swept out before submission.

Security

SECURITY.md describes how to disclose vulnerabilities and what's in-scope for bug bounty.

License

Apache-2.0 — same as luxfi/pulsar and luxfi/corona. See LICENSE.