magnetar

48 Commits 1 Branch 18 Tags

3 Commits

Include renames

Author	SHA1	Message	Date
Antje Worring	df4c537c16	magnetar: remove proof-by-rename + circular proofs; honest threshold status True no-reconstruction threshold SLH-DSA is impossible in the no-dealer / no-preprocessing model a public, leaderless, permissionless chain needs (Kondi-Kumar-Vanegas: extractable hash-based signatures cannot be thresholded by black-box hash use). Stop pretending otherwise. De-cheat: - DELETE the circular/vacuous proofs that manufactured false assurance: Magnetar_N1_Atom_Refinement.ec, Magnetar_N1_SHAKE_Expand.ec, Magnetar_N4_KeyDeriveStable.ec, lemmas/{Magnetar_CT,SLHDSA_Functional}.ec. The headline "strict-atom byte-equality" theorem was `apply <axiom that restates the theorem>`; the Lean side was `sorry`/`:= True`. - Re-open MAGNETAR-STRICT-ATOM (BLOCKERS): the public combiner DOES reconstruct the full FIPS 205 master every signature; the v1.1 "closure" only renamed identifiers. PROOF-CLAIMS / AXIOM-INVENTORY / TCB docs now say what the code does. - Re-label the name-grep "strict-atom" / "CT" checks as identifier-hygiene lint, NOT security or constant-time properties. - PVSS-DKG open-reveal (publishes the master to any observer) is gated as a TEST-ONLY path with HONEST LIMITATIONS; production does not rely on it. - Remove dead htRootCompute; staticcheck clean. Honest three-leg posture (SPEC 1.0, BLOCKERS): - Permissionless production = INDEPENDENT FIPS 205 sigs + the weighted quorum certificate (luxfi/consensus), optionally STARK/FRI-compressed (luxfi/p3q). No key sharing, no reconstruction. - Trusted-hardware custody = TEE-attested combiner (trust-relocation, NOT MPC). - THBS-SE = RESEARCH-ONLY (transient seed reconstruction at the combiner); the T-SLH-DSA-MPC track (MPC over SHAKE) is the other research escape hatch. Tests green (CGO=1, 71s). Net -923 lines.	2026-06-21 13:06:57 -07:00
Lux Magnetar	83ce56ff0f	magnetar v1.0.0: ONE construction per regime; THBS-SE permissionless threshold 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	2026-06-01 12:03:22 -07:00
Hanzo AI	d95ef9c3cb	submission: TRUSTED-COMPUTING-BASE + PROOF-CLAIMS + AXIOM-INVENTORY + FIPS-TRACEABILITY Tier A documentation shape, second cluster. Honest framing of what Magnetar v0.3.0 proves vs what remains roadmap: - TRUSTED-COMPUTING-BASE.md: enumerates the trust base. cloudflare/circl slhdsa is in TCB at the single-party FIPS 205 layer. Aggregator process is in TCB for the brief seed-reconstruction window (v0.1 reveal-and-aggregate caveat). Comparison table vs Pulsar and Corona TCBs. - PROOF-CLAIMS.md: narrow Class-N1 byte-equality claim — Magnetar threshold output is byte-identical to single-party FIPS 205 slhdsa.SignDeterministic on the reconstructed seed. §3 enumerates 7 explicit NON-claims: mechanized refinement of threshold overlay, post-quantum hardness beyond FIPS 205, byte-equality with FIPS 204/R-LWE, dudect statistical CT, covert channels, protocol-level adversarial robustness beyond reveal-and-aggregate, external Lean theorems. - AXIOM-INVENTORY.md: construction-level + implementation-level axioms. FIPS 205 SLH-DSA security inherited from NIST. Byte-wise Shamir VSS soundness over GF(257) inherited from Shamir 1979. Closure plans for EC theory shells (v0.5.0 roadmap), Lean ↔ EC bridge cross-citation to Pulsar's GF(257) bridges, dudect (v0.6.0). - FIPS-TRACEABILITY.md: FIPS 205 §10.1/10.2/10.3 → keygen/sign/ verify code map. FIPS 202 + SP 800-185 cSHAKE256/KMAC256 customisation tags pinned in transcript.go. Threshold overlay layer traces to SPEC.md §3/§4/§6 (no NIST standard exists for threshold SLH-DSA). NO fake closure language. Every "OPEN" gate is explicit; every closure plan is concrete and dated to a roadmap version.	2026-05-19 07:57:08 -07:00

Author

SHA1

Message

Date

Antje Worring

df4c537c16

magnetar: remove proof-by-rename + circular proofs; honest threshold status

True no-reconstruction threshold SLH-DSA is impossible in the no-dealer /
no-preprocessing model a public, leaderless, permissionless chain needs
(Kondi-Kumar-Vanegas: extractable hash-based signatures cannot be thresholded
by black-box hash use). Stop pretending otherwise.

De-cheat:
  - DELETE the circular/vacuous proofs that manufactured false assurance:
    Magnetar_N1_Atom_Refinement.ec, Magnetar_N1_SHAKE_Expand.ec,
    Magnetar_N4_KeyDeriveStable.ec, lemmas/{Magnetar_CT,SLHDSA_Functional}.ec.
    The headline "strict-atom byte-equality" theorem was `apply <axiom that
    restates the theorem>`; the Lean side was `sorry`/`:= True`.
  - Re-open MAGNETAR-STRICT-ATOM (BLOCKERS): the public combiner DOES
    reconstruct the full FIPS 205 master every signature; the v1.1 "closure"
    only renamed identifiers. PROOF-CLAIMS / AXIOM-INVENTORY / TCB docs now say
    what the code does.
  - Re-label the name-grep "strict-atom" / "CT" checks as identifier-hygiene
    lint, NOT security or constant-time properties.
  - PVSS-DKG open-reveal (publishes the master to any observer) is gated as a
    TEST-ONLY path with HONEST LIMITATIONS; production does not rely on it.
  - Remove dead htRootCompute; staticcheck clean.

Honest three-leg posture (SPEC 1.0, BLOCKERS):
  - Permissionless production = INDEPENDENT FIPS 205 sigs + the weighted quorum
    certificate (luxfi/consensus), optionally STARK/FRI-compressed (luxfi/p3q).
    No key sharing, no reconstruction.
  - Trusted-hardware custody = TEE-attested combiner (trust-relocation, NOT MPC).
  - THBS-SE = RESEARCH-ONLY (transient seed reconstruction at the combiner);
    the T-SLH-DSA-MPC track (MPC over SHAKE) is the other research escape hatch.

Tests green (CGO=1, 71s). Net -923 lines.

2026-06-21 13:06:57 -07:00

Lux Magnetar

83ce56ff0f

magnetar v1.0.0: ONE construction per regime; THBS-SE permissionless threshold

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

2026-06-01 12:03:22 -07:00

Hanzo AI

d95ef9c3cb

submission: TRUSTED-COMPUTING-BASE + PROOF-CLAIMS + AXIOM-INVENTORY + FIPS-TRACEABILITY

Tier A documentation shape, second cluster. Honest framing of what
Magnetar v0.3.0 proves vs what remains roadmap:

- TRUSTED-COMPUTING-BASE.md: enumerates the trust base.
  cloudflare/circl slhdsa is in TCB at the single-party FIPS 205
  layer. Aggregator process is in TCB for the brief
  seed-reconstruction window (v0.1 reveal-and-aggregate caveat).
  Comparison table vs Pulsar and Corona TCBs.

- PROOF-CLAIMS.md: narrow Class-N1 byte-equality claim — Magnetar
  threshold output is byte-identical to single-party FIPS 205
  slhdsa.SignDeterministic on the reconstructed seed.
  §3 enumerates 7 explicit NON-claims: mechanized refinement of
  threshold overlay, post-quantum hardness beyond FIPS 205,
  byte-equality with FIPS 204/R-LWE, dudect statistical CT,
  covert channels, protocol-level adversarial robustness beyond
  reveal-and-aggregate, external Lean theorems.

- AXIOM-INVENTORY.md: construction-level + implementation-level
  axioms. FIPS 205 SLH-DSA security inherited from NIST. Byte-wise
  Shamir VSS soundness over GF(257) inherited from Shamir 1979.
  Closure plans for EC theory shells (v0.5.0 roadmap), Lean ↔ EC
  bridge cross-citation to Pulsar's GF(257) bridges, dudect (v0.6.0).

- FIPS-TRACEABILITY.md: FIPS 205 §10.1/10.2/10.3 → keygen/sign/
  verify code map. FIPS 202 + SP 800-185 cSHAKE256/KMAC256
  customisation tags pinned in transcript.go. Threshold overlay
  layer traces to SPEC.md §3/§4/§6 (no NIST standard exists for
  threshold SLH-DSA).

NO fake closure language. Every "OPEN" gate is explicit;
every closure plan is concrete and dated to a roadmap version.

2026-05-19 07:57:08 -07:00