mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zooqueen
ebf46cbba8
Corona is Lux's fork of Ringtail (ePrint 2024/1113) = two-round Module-LWE
(M=8, N=7 over R_q=Z_q[X]/(X^256+1), q=0x1000000004A01 48-bit, sigma=6.108) —
NOT Ring-LWE rank-1. Corona.lean: hardness Module-LWE; axiom corona_ring_lwe_euf_cma
-> corona_module_lwe_euf_cma; EUF-CMA reduces to Module-LWE; params corrected
(was q=2^32/sigma=13744). Corona/{OutputInterchange,Unforgeability,dkg2}, Quasar,
Magnetar, HQC, BLS, Threshold_Lagrange label fixes. 'Ring-LWE = Module-LWE rank 1'
kept only as general math remark. lake build: success.
112 lines
4.8 KiB
Lean4
112 lines
4.8 KiB
Lean4
/-
|
||
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; full
|
||
GKMM 2024/447 reduction in `proofs/lean/Crypto/Magnetar_MPC.lean`.
|
||
|
||
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. -/
|
||
axiom magnetar_hash_disjoint_from_mlwe :
|
||
∀ (mlwe_oracle : Nat → Nat),
|
||
∃ (hash_instance : Nat),
|
||
mlwe_oracle hash_instance ≠ hash_instance
|
||
|
||
/-- The same disjointness against the rank-1 (Ring-LWE) special case of
|
||
Module-LWE; retained as a general lattice statement (Corona itself
|
||
is instantiated at module rank ~7-8, i.e. Module-LWE, not rank 1). -/
|
||
axiom magnetar_hash_disjoint_from_rlwe :
|
||
∀ (rlwe_oracle : Nat → Nat),
|
||
∃ (hash_instance : Nat),
|
||
rlwe_oracle hash_instance ≠ hash_instance
|
||
|
||
/-- 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)`.
|
||
Full GKMM 2024/447 reduction mechanised in
|
||
`Crypto.Magnetar_MPC.threshold_byte_equality`. Upgrading from
|
||
per-validator individual sigs to a single threshold sig (LP-0120
|
||
0x012207) 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
|
||
0x012207; Lean reduction in `Crypto.Magnetar_MPC`). Architecture:
|
||
`~/work/lux/threshold/study/magnetar.md`.
|
||
-/
|
||
|
||
end Crypto.Magnetar
|