Lux Magnetar
83ce56ff0f
Magnetar v1.0.0 closes the permissionless-threshold story at ONE
construction --- THBS-SE (Threshold Hash-Based Signatures with
Selected-Element Reconstruction) --- and removes every legacy
seed-recombine path from the codebase.
The two production primitives at v1.0:
1. Per-validator standalone (standalone.go, unchanged from v0.5.x) ---
the public-BFT primary primitive. Each validator holds its own FIPS
205 keypair, signs independently, consensus collects N signatures
into a ValidatorAggregateCert.
2. THBS-SE (thbsse.go + thbsse_field.go) --- the permissionless
threshold companion. t-of-n committee, slot-bound commit-and-reveal,
PUBLIC COMBINER role (anyone-can-combine, no host in TCB at sign
time), slashable equivocation and malformed-share evidence.
Both emit byte-identical FIPS 205 signatures that unmodified verifiers
accept (TestMagnetar_Wire_FIPS205Verifiable +
TestThbsSE_Wire_FIPS205Verifiable across all 3 SHAKE modes).
Hard invariant (THBS-SE): a revealed value is allowed only if it is
also present in the final SLH-DSA signature. Forbidden reveals:
SK.seed in any party-local persistent form, SK.prf, future-slot share
material. The slot guard refuses any same-slot re-emission.
v1.0 honest open item: the strict "no transient seed at any moment"
invariant requires a v1.1 strict-atom-assembly path
(BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11) that re-implements FIPS 205
sec 5/6/7/8 internally. v1.0 ships a PUBLIC COMBINER that holds the
seed for one slhdsa.SignDeterministic call and zeroizes; materially
stronger than TEE-attested privileged-aggregator constructions,
materially weaker than the strict refinement.
8 test gates + 2 bonus correctness checks:
- TestThbsSE_Wire_FIPS205Verifiable (3 modes) -- byte identity
- TestThbsSE_RejectSeedReveal
- TestThbsSE_RejectUnselectedFORS
- TestThbsSE_RejectUnselectedWOTS
- TestThbsSE_SlotReuseRejected
- TestThbsSE_OverselectedCommittee
- TestThbsSE_SlotBindingDomainSeparation
- BenchmarkThbsSE_Sign_5of7
- TestThbsSE_PublicCombiner_Determinism (bonus)
- TestKAT_ThbsSe (n=7, t=4, 3 modes, 3 messages)
Removed (legacy seed-recombine path + the proofs/CT scaffolding that
modeled it):
- ref/go/pkg/magnetar/{threshold,aggregate,combine,shamir,dkg}.go
+ tests
- ref/go/pkg/magnetar/{e2e,fuzz,n1_byte_equality}_test.go
- ref/go/pkg/thbs/ (entire subtree including dkg2/ PVSS skeleton)
- vectors/{threshold-sign,dkg}.json
- jasmin/{threshold,lib}/ (legacy seed-recombine model)
- proofs/easycrypt/ (entire tree; v1.1 ports to THBS-SE)
- ct/dudect/ (entire tree; v1.1 lands with strict-atom path)
- scripts/{check-lean-bridge,checks/ec-*,checks/jasmin,checks/extraction}.sh
Added:
- ref/go/pkg/magnetar/thbsse.go (1054 LOC; the THBS-SE construction)
- ref/go/pkg/magnetar/thbsse_field.go (GF(257) internal share math)
- ref/go/pkg/magnetar/thbsse_test.go (8 gates + 2 bonus)
- vectors/thbsse-sign.json (deterministic (n=7,t=4) KAT)
- v1.0 supersede notices on v0.x archival docs
Verification:
- GOWORK=off go build ./... && go vet ./...: clean
- go test -count=1 -short: PASS (all gates)
- go test -count=1 -race -short: PASS
- grep "reveal-and-aggregate|seed.*recombin|THBS over.*seed|aggregator.*reconstruct.*seed" *.go: 0 matches
- find ref/go/pkg -type d -name thbs: empty
Magnetar --- machine-checked proof track
Magnetar v1.0 ships two primitives:
-
Per-validator standalone --- routes through
cloudflare/circl/sign/slhdsav1.6.3 in production. The single-party FIPS 205 functional + constant-time analysis tracks the formosa-cryptolibjade-SLH-DSAupstream when it lands. Until then, the trust model relies on CIRCL's upstream review and the NIST FIPS 205 reference. -
THBS-SE (Threshold Hash-Based Signatures with Selected-Element Reconstruction) --- permissionless t-of-n threshold signing that produces a byte-identical FIPS 205-shaped signature. See
ref/go/pkg/magnetar/thbsse.gofor the construction, andTHBS-SPEC.mdfor the normative spec.
What the proof track covers in v1.0
For v1.0 the machine-checked proof effort is scoped to the algebraic identities the THBS-SE share arithmetic relies on, plus the byte-identity claim that ties THBS-SE Combine output to single-party FIPS 205 SignDeterministic.
The legacy EasyCrypt scaffolding that modeled the abandoned v0.x
seed-recombine path has been removed (it modeled combine.go and
threshold.go, files that are no longer in the codebase). The
v1.0 proof track is being rebuilt against the THBS-SE construction
shape (commit-bind, byte-wise Shamir over GF(257), Lagrange
reconstruct, FIPS 205 dispatch) and lands in v1.1 alongside the
strict-atom-assembly construction.
What ships in v1.0
The Go reference implementation under
ref/go/pkg/magnetar/thbsse.go and thbsse_field.go is the
load-bearing artifact for v1.0. The 8 test gates listed in the
v1.0 sign-off (TestThbsSE_Wire_FIPS205Verifiable,
TestThbsSE_RejectSeedReveal, TestThbsSE_RejectUnselectedFORS,
TestThbsSE_RejectUnselectedWOTS, TestThbsSE_SlotReuseRejected,
TestThbsSE_OverselectedCommittee,
TestThbsSE_SlotBindingDomainSeparation,
BenchmarkThbsSE_Sign_5of7) pin the byte-identity, slot-binding, and
slashing-evidence properties end-to-end against unmodified
cloudflare/circl/sign/slhdsa.Verify. The KAT replay
(TestKAT_ThbsSe) pins deterministic vectors at (n=7, t=4) across
all three SLH-DSA modes and three messages.
What lands in v1.1
The v1.1 proof track plan:
-
EasyCrypt theory shells for THBS-SE: the commit-bind ladder, the byte-wise Shamir over GF(257), the Lagrange interpolation at x=0, and the byte-identity step that ties the final SLH-DSA bytes to single-party FIPS 205 SignDeterministic on the reconstructed seed (or, in the strict-atom v1.1 path, on the directly-assembled FIPS 205 signature atoms).
-
Lean bridge for the algebraic content (Shamir reconstruction identity, Lagrange basis uniqueness over finite fields, polynomial interpolation existence) mirroring Pulsar's
~/work/lux/proofs/lean/Crypto/setup. -
Jasmin track for the strict-atom path (Magnetar-internal FIPS 205 sec 5/6/7/8 surface), once that construction lands at v1.1.
See BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11 for the v1.1 roadmap.