mirror of https://github.com/luxfi/magnetar.git synced 2026-07-27 02:53:47 +00:00

Files

T

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

3.5 KiB

Raw Permalink Blame History

Magnetar --- proof track (HONEST: there is no mechanized proof)

There is currently no mechanized proof of any Magnetar threshold property. This directory contains SCAFFOLDS only. Read this before treating anything here as assurance.

What is actually here

File	Content
`easycrypt/Magnetar_N1_StrictAtom.ec`	SCAFFOLD. 0 mechanized content. Records that THBS-SE Combine byte-equality is NOT proven and explains why the prior "proof" (a theorem `apply`-ing an axiom that restated it) was circular.
`easycrypt/Magnetar_N5_PVSS_DKG.ec`	SCAFFOLD. 0 mechanized content. Records that PVSS-DKG secrecy is NOT proven, and that the prior secrecy "theorem" was both vacuous (`conclusion = true`) and false for the open-reveal code it modeled.
`lean/Crypto/Magnetar/StrictAtom.lean`	SCAFFOLD. 0 mechanized content. The prior `sorry`-bodied theorem and `:= True` discipline have been removed.

Each file declares no axiom, no admit, no sorry, no theorem, and no lemma. The only occurrences of those words are inside prose comments that describe what was removed.

What was deleted, and why

The following files were deleted because every result in them was vacuous (X = X by rewrite, or conclusion = true by trivial) or a black-box axiom feeding nothing real. They manufactured the appearance of a "proof track" with a nonzero theorem count and a small "admit budget" while proving nothing about the construction:

Magnetar_N1_SHAKE_Expand.ec --- only non-axiom lemma was shake_expand m s = shake_expand m s rewritten from s = s.
Magnetar_N1_Atom_Refinement.ec --- a single restate-as-axiom.
Magnetar_N4_KeyDeriveStable.ec --- s = s' => f s = f s', i.e. "this function is a function". Content-free.
lemmas/Magnetar_CT.ec --- strict_atom_combine_is_ct discharged by admit; the comment itself called the abstract level "vacuous". Constant-time was also the wrong property to claim: the Combine path reconstructs the FIPS 205 master, so there is no secret to protect from a timing side-channel that is not already in plaintext in the combiner's buffer.
lemmas/SLHDSA_Functional.ec --- legitimate black-box FIPS 205 functional-spec axioms, but they fed only the deleted files.

Honest summary of the actual evidence base

Magnetar's correctness/interop evidence is empirical, not mechanized:

Per-validator standalone (standalone.go) emits single-party FIPS 205 signatures; TestMagnetar_Wire_FIPS205Verifiable.
THBS-SE Combine emits FIPS 205 signatures byte-identical to circl/slhdsa.SignDeterministic on the reconstructed master; TestSlhdsaInternal_ByteEqualToCirclSign, TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl.
KAT determinism via ref/go/cmd/genkat.

These are tests. They establish that the threshold output is a valid FIPS 205 signature. They do NOT establish any confidentiality / no-leak property, and there is no mechanized refinement.

See PROOF-CLAIMS.md for the per-property proven/asserted/open breakdown.

Open work (tracked, not done)

A genuine mechanized result would require an abstract slh_sign model (EasyCrypt or Lean) of the FIPS 205 sec 5--sec 8 hash-tree signing walk, proven equal to the Go implementation — not to circl, and not to a restatement of the conclusion. That is multi-week work and is OPEN.

There is no mechanized no-leak result to target for THBS-SE, because THBS-SE in the permissionless model reconstructs the master at the public combiner (research-grade; see BLOCKERS.md).

3.5 KiB Raw Permalink Blame History