mirror of
https://github.com/luxfi/magnetar.git
synced 2026-09-24 00:25:23 +00:00
zooqueen
135f43e531
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.
54 lines
2.0 KiB
Lean4
54 lines
2.0 KiB
Lean4
/-
|
|
Copyright (c) 2025-2026 Lux Industries Inc. All rights reserved.
|
|
Released under the same license as the rest of Magnetar.
|
|
-/
|
|
|
|
/-!
|
|
# Crypto.Magnetar.StrictAtom
|
|
|
|
SCAFFOLD: 0 mechanized content. This file proves NOTHING.
|
|
|
|
## Honest status
|
|
|
|
The earlier revision of this file declared a theorem
|
|
`strict_atom_byte_equality` whose proof body was `sorry`, and a
|
|
definition `strictAtomDisciplineSatisfied : Prop := True` with a
|
|
companion `theorem strict_atom_discipline := trivial`. A `sorry`
|
|
discharges nothing, and a `True`-valued "discipline" proves nothing
|
|
about the code. Both have been removed.
|
|
|
|
## What the code actually does
|
|
|
|
The THBS-SE Combine path
|
|
(`ref/go/pkg/magnetar/thbsse_assemble.go::assembleSignatureBytes`)
|
|
Lagrange-reconstructs the FIPS 205 master byte vector, SHAKE-expands
|
|
it into a single buffer holding `skSeed || skPrf || pkSeed`, and
|
|
emits a FIPS 205 signature. The full master is present in the public
|
|
combiner's memory for the duration of one Sign call. Renaming the
|
|
buffer to avoid the identifier `seed` does NOT establish any no-leak
|
|
property. There is nothing here for Lean to certify as confidential.
|
|
|
|
The only empirically supported property is byte-IDENTITY of the
|
|
emitted signature to `circl/slhdsa.SignDeterministic` on the
|
|
reconstructed master (a correctness/interop property), witnessed by
|
|
the Go tests `TestSlhdsaInternal_ByteEqualToCirclSign` and
|
|
`TestThbsSE_StrictAtom_Combine_ByteIdentityToCircl`. No Lean theorem
|
|
backs it.
|
|
|
|
A genuine result would require an abstract Lean model of the FIPS 205
|
|
hash-tree signing walk proven equal to the Go implementation — not a
|
|
`sorry`, and not a `True`. That work is OPEN and is tracked in
|
|
`PROOF-CLAIMS.md`.
|
|
|
|
This file intentionally declares no `theorem`, no `axiom`, no `sorry`,
|
|
and no `def`. It is a documentation stub only.
|
|
-/
|
|
|
|
namespace Crypto.Magnetar.StrictAtom
|
|
|
|
-- Intentionally empty. See the module banner: this is a 0-content
|
|
-- scaffold. It exists only to record, in the proof tree, that the
|
|
-- THBS-SE strict-atom byte-equality is NOT mechanized.
|
|
|
|
end Crypto.Magnetar.StrictAtom
|