proofs/lean/Crypto/Magnetar.lean at main

mirror of https://github.com/luxfi/proofs.git synced 2026-10-30 15:21:05 +00:00

Files

T

zeekayandHanzo Dev a94116d3ff lean: Magnetar's TS-UF bound states the bound

`HardnessAdvantage` was `opaque HardnessAdvantage : Type := Unit`. In a
one-element type every advantage equals every other, so no bound of the form
`adv ≤ a + b + c + d` is expressible — which is why `MagnetarTSUFBound`
concluded `True` while its docstring described a four-way decomposition, and why
`magnetar_tsuf` and `magnetar_tsuf_n_independent` established nothing. It is now
a nonnegative quantity, ordered and additive.

`MagnetarTSUFBound fp` is the sum of the four named advantages: SHAKE collision,
SHAKE preimage, FIPS 205 EUF-CMA, and the aggregator-TCB caveat. It takes no
`ThresholdParams`, which is the substance of n-independence — that theorem now
follows from the bound's shape instead of re-wrapping its hypothesis.

`magnetar_tsuf` is an axiom rather than a theorem, because that is what an
unmechanised reduction is. `magnetar/PROOF-CLAIMS.md` §0 states "Magnetar has no
mechanized proof of any threshold property"; this corpus was claiming one, so
magnetar was the honest side of the disagreement.

`magnetar_hardness_disjoint_from_lattice` was `(h : Bound) : Bound := h` — it
returned its own hypothesis. Family disjointness quantifies over adversaries and
reductions between problems, and this model has neither; the bound's freedom
from lattice hardness is visible in its definition, so that is where it is
stated.

Three citations named `Crypto/Magnetar_MPC.lean` as the home of the mechanised
GKMM 2024/447 reduction. No such file exists in any of the three proof
repositories. They now point at `magnetar/PROOF-CLAIMS.md`, and the reference to
`threshold/study/magnetar.md`, which is also absent, is gone.

Zero Magnetar declarations are now reported as carrying no content, down from
one; corpus total 62 to 61.

Co-authored-by: Hanzo Dev <[email protected]>

2026-07-29 15:46:21 -07:00

116 lines

4.8 KiB

Lean4

Raw Permalink Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 /-
   Magnetar — Public-DKG MPC threshold SLH-DSA (FIPS 205, hash family).
   Hash-based twin of Pulsar (FIPS 204 ML-DSA / Module-LWE).
   This file mechanises the *batch-verify* dispatcher (production today).
   The MPC-signing layer (LP-0120 slot 0x012207) is axiomatic here. There is no
   mechanised GKMM 2024/447 reduction — `magnetar/PROOF-CLAIMS.md` §0 states
   that "Magnetar has no mechanized proof of any threshold property", and this
   corpus does not add one.
   Maps to:
   - luxfi/crypto:slhdsa (gpu.go: VerifyBatch / VerifyBatchGPU)
   - luxfi/accel: LatticeOps.SLHDSAVerifyBatch (v1.1.0+)
   - luxcpp/accel: GPU SLH-DSA batch kernels — Metal / CUDA / WGSL (v0.1.1+)
   - LP-0120 §4: Magnetar at precompile 0x012207 (MPC signing)
 -/
 import Mathlib.Data.Nat.Defs
 import Mathlib.Tactic
 import Crypto.SLHDSA
 namespace Crypto.Magnetar
 open Crypto.SLHDSA (ParamSet sigSize pkSize securityBits slhdsa_sign
                     slhdsa_verify slhdsa_correctness)
 /-- Batch verification of `n` independent SLH-DSA signatures under a
     common parameter set. Accepts iff every (pk, msg, sig) triple
     verifies. GPU path: single `LatticeOps.SLHDSAVerifyBatch` call;
     CPU path: sequential loop. No aggregation-of-trust effect — any
     bad triple poisons the batch. -/
 axiom magnetar_batch_verify :
   ParamSet → List (Nat × Nat × Nat) → Bool   -- (pk, msg, sig) triples
 /-- Soundness: batch acceptance implies every triple verifies. -/
 axiom magnetar_batch_sound :
   ∀ (ps : ParamSet) (triples : List (Nat × Nat × Nat)),
     magnetar_batch_verify ps triples = true →
     ∀ (t : Nat × Nat × Nat),
       t ∈ triples →
       slhdsa_verify ps t.1 t.2.1 t.2.2 = true
 /-- Completeness: a batch of honestly-generated triples is accepted. -/
 axiom magnetar_batch_complete :
   ∀ (ps : ParamSet) (sigs : List (Nat × Nat × Nat)),
     (∀ t, t ∈ sigs → slhdsa_verify ps t.1 t.2.1 t.2.2 = true) →
     magnetar_batch_verify ps sigs = true
 /-- The empty batch is trivially accepted. -/
 axiom magnetar_batch_empty :
   ∀ (ps : ParamSet), magnetar_batch_verify ps [] = true
 /-- Singleton batch coincides with single-party verify. -/
 axiom magnetar_batch_singleton :
   ∀ (ps : ParamSet) (pk msg sig : Nat),
     magnetar_batch_verify ps [(pk, msg, sig)] = slhdsa_verify ps pk msg sig
 /-- Correctness: honestly-signed triple verifies under the batch
     dispatcher iff it verifies under the standard FIPS 205 verifier. -/
 theorem magnetar_single_sig_correctness
     (ps : ParamSet) (sk pk msg : Nat) :
     magnetar_batch_verify ps [(pk, msg, slhdsa_sign ps sk msg)] =
       slhdsa_verify ps pk msg (slhdsa_sign ps sk msg) :=
   magnetar_batch_singleton ps pk msg (slhdsa_sign ps sk msg)
 /-- Empty batch is accepted (sanity check on the soundness statement). -/
 theorem magnetar_empty_accepted (ps : ParamSet) :
     magnetar_batch_verify ps [] = true :=
   magnetar_batch_empty ps
 /- Hash-family disjointness from lattice schemes. SLH-DSA rests on
     hash collision + preimage resistance (SHA-2 / SHAKE), not on any
     lattice assumption (Module-LWE / Module-SIS, of which Ring-LWE is
     the rank-1 special case). Modelled as: a lattice oracle does not
     yield a hash oracle. This is what makes Magnetar the only true
     cross-family leg of the Polaris cert profile (Pulsar ‖ Corona ‖
     Magnetar) in LP-0120 — Pulsar and Corona are both Module-LWE, so
     Magnetar (hash) is the sole family-disjoint signature primitive.
     Family disjointness is stated here and is not axiomatised.
     Two axioms stood here, each of the shape
       ∀ (oracle : Nat → Nat), ∃ (x : Nat), oracle x ≠ x
     which the identity function refutes: it yields `∃ x, x ≠ x`, so each
     proved `False` and made every theorem in the corpus derivable. Neither
     had a user.
     `Nat → Nat` cannot express "these two problems share no reduction":
     that claim quantifies over adversaries and advantages, not over
     integers. -/
 /-- MPC threshold-signing byte-equality (axiomatic). Magnetar's
     threshold-SLH-DSA output over a Pedersen-DKG-issued group secret
     `sk` is byte-equal to the standard FIPS 205 signature on `(sk, msg)`.
     The GKMM 2024/447 reduction is not mechanised; see
     `magnetar/PROOF-CLAIMS.md` §0. Upgrading from
     per-validator individual sigs to a single threshold sig (LP-0120
 x012207) requires no verifier change. -/
 axiom magnetar_mpc_threshold_correct :
   ∀ (ps : ParamSet) (sk pk msg : Nat)
     (mpc_signature : Nat),
     -- mpc_signature is the output of the threshold protocol on (ps, sk, msg)
     slhdsa_verify ps pk msg mpc_signature =
     slhdsa_verify ps pk msg (slhdsa_sign ps sk msg)
 /-
   Shipping layers: GPU batch verify of single-party SLH-DSA (live,
   Metal + CUDA + WGSL); public-DKG + MPC threshold signing (LP-0120
 x012207). Assurance vocabulary and what is and is not proved:
   `magnetar/PROOF-CLAIMS.md`.
 -/
 end Crypto.Magnetar

116 lines 4.8 KiB Lean4 Raw Permalink Blame History Unescape Escape

116 lines

4.8 KiB

Lean4

Raw Permalink Blame History