Files
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
..

Magnetar --- constant-time analysis track

Magnetar v1.0 routes ALL FIPS 205 SLH-DSA operations through cloudflare/circl/sign/slhdsa v1.6.3. CIRCL's slhdsa package is the upstream CT-audited reference; its constant-time posture is the constant-time posture inherited by both Magnetar primitives:

  • Per-validator standalone (ref/go/pkg/magnetar/standalone.go) --- ValidatorSign is a thin wrapper around slhdsa.SignDeterministic. No Magnetar-side secret-dependent branches. The CT property is the CT property of CIRCL slhdsa v1.6.3 verbatim.

  • THBS-SE (ref/go/pkg/magnetar/thbsse.go + thbsse_field.go) --- the share arithmetic surface (commit-bind, Lagrange reconstruct over GF(257), mix-to-seed, dispatch to CIRCL slhdsa) is straight-line modular arithmetic with no secret-dependent branches:

    • thbsseModInvSmall / thbsseModPowSmall operate on the PUBLIC prime exponent p-2, not on a secret exponent.
    • The Lagrange basis lambdas are functions of PUBLIC evaluation points only.
    • The per-byte share multiplication is one uint32 mul + one % 257 per byte position --- no branching on share value.
    • The commit re-derivation in Combine and deriveThbsSeCommit is a cSHAKE256 absorb, which is CT by CIRCL's golang.org/x/ crypto/sha3 implementation.

v1.0 ship status

The v0.x dudect harness has been removed --- it modeled the abandoned seed-recombine Combine and Verify API surfaces that no longer exist in the codebase. The v1.0 THBS-SE construction has a substantially smaller CT-critical surface (no DKG state, no intermediate Round1Message struct lifetime, no per-party MAC ladder), and the CIRCL slhdsa upstream covers the heavy SLH-DSA work.

v1.1 plan

The v1.1 dudect harness re-lands once the strict-atom-assembly construction lands (BLOCKERS.md::MAGNETAR-STRICT-ATOM-V11). At that point a small Magnetar-internal re-implementation of FIPS 205 sec 5/6/7/8 surfaces enters the trusted computing base, and a dudect harness over the per-atom WOTS+ chain + FORS sign step becomes the right CT analytical surface. v1.0's CT story is "inherit CIRCL"; v1.1's CT story is "inherit CIRCL for FIPS 205 sec 0--4 + dudect for the Magnetar-internal sec 5--8 surface".