feat(MLDSA): short-secret MLWE model and the exact NMA key-swap hop

[alik-eth]

Step 2 of the #467 decomposition @dtumad proposed: the corrected short-secret MLWE model and the exact NMA key-swap hop, as a focused, purely additive PR.

Stacked on #503 (the SelfTargetMSIS binding repair) — until #503 lands, its diff shows here too; this PR's own content is the ~489 additive lines in SecurityNMA.lean + Scheme.lean. The two are independent in content (MLWE leg vs SelfTargetMSIS leg); the stacking is just to keep the decomposition ordered.

What this adds

The MLWE leg of the ML-DSA NMA reduction, modelled over the η-bounded box rather than the full ring — fixing the information-theoretically-zero-advantage issue of the earlier full-ring-uniform mldsaMLWE:

• sampleShortVec (uniform on the η-box), keygenShort/keygenShort1 (idealized key generation sampling ρ, K, and short (s₁, s₂) independently).
• validKeyPairShort (the ∃-material key relation) + identificationSchemeShort, with the satisfiability certificate keygenShort_generable (⟨hrShort, rfl⟩) — so the relation/pinning hypotheses these introduce are inhabited, not vacuous.
• mldsaMLWEShort (seed-based short-secret MLWE) and mldsaMatrixMLWE (the standard uniform-matrix form), with expandAIdealization (the named XOF-as-random-matrix assumption, computational reading disclosed) and the proven seed→matrix bridge advantage_mldsaMLWEShort_le_matrix via matrixLift.
• nma_keyswap_hop_short — the headline: the NMA-game gap between the real and uniform-t short key generators is bounded by the mldsaMLWEShort distinguishing advantage of distinguisherBShort, as an exact identity — no idealGap/hSlack statistical-slack term (the earlier honestSamplingSlack stopgap is not used).

Scope

Purely additive — no existing declaration is modified or removed. The old mldsaMLWE/nma_security chain on the base is untouched here; it is retired when the NMA headline moves over (a later step). The SelfTargetMSIS/extraction/headline development (mldsaSTMSISShort, nma_security_short/fips, ...) is not in this PR — it is steps 3–4.

Verification

Off current main (v4.32.0). lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets green. nma_keyswap_hop_short, advantage_mldsaMLWEShort_le_matrix, and keygenShort_generable all kernel-check [propext, Classical.choice, Quot.sound]. Both touched files CI-lint clean.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[github-actions]

🤖 PR Summary

Overview

This PR adds the short-secret Module-LWE (MLWE) model and an exact NMA key-swap hop for ML-DSA, the second step of a decomposition of the full NMA security proof. It is stacked on #503 (the SelfTargetMSIS binding repair), but the substantive additions are confined to SecurityNMA.lean (~489 lines) and Scheme.lean. The PR is purely additive; no existing code is modified or removed.

The core mathematical contribution is a corrected information-theoretic model for the MLWE leg of the NMA reduction, replacing the earlier full-ring-uniform mldsaMLWE with a model over the η-bounded box. This fix addresses a prior information-theoretically-zero-advantage issue.

Headline Additions

• validKeyPairShort — a noncomputable decidable predicate for key pairs built from bounded short vectors s₁, s₂ and seeds ρ, K directly, with a @[simp] equivalence theorem validKeyPairShort_eq_true_iff. This is the ∃-material analogue of the existing ∃-seed validKeyPair.
• identificationSchemeShort — reuses existing commit/respond/verify algorithms but is typed under validKeyPairShort, enabling security statements that reference an idealized scheme with material-based key relations rather than seed-derived ones.
• sampleShortVec, keygenShort / keygenShort1 — idealized key-generation procedures for the η-bounded box: keygenShort computes public key t = ExpandA(ρ)·s₁ + s₂; keygenShort1 samples uniform t.
• hrShort and keygenShort_generable — a GenerableRelation over validKeyPairShort (with generator keygenShort) and a theorem certifying its inhabitation, ensuring the relation/pinning hypotheses are non-vacuous.
• mldsaMLWEShort (seed-based short-secret MLWE) and mldsaMatrixMLWE (uniform-matrix form) — Module-LWE problem definitions for the short-secret setting.
• expandAIdealization — the named XOF-as-random-matrix assumption, stated as a property relating (ρ, ExpandA(ρ)) to (ρ, A) with uniform independent A.
• advantage_mldsaMLWEShort_le_matrix — a lemma bounding seed-based short-MLWE advantage by uniform-matrix advantage plus εA under expandAIdealization, via matrixLift.
• nma_keyswap_hop_short (the headline) — an exact identity bounding the NMA-game gap between real and uniform-t short key generators by the distinguishing advantage of distinguisherBShort against mldsaMLWEShort. This identity uses no idealGap/hSlack statistical-slack term.

Missing or Incomplete Items

• The PR body states “no existing declaration is modified or removed,” which is consistent with the code.
• The PR body notes the absence of SelfTargetMSIS/extraction/headline development (mldsaSTMSISShort, nma_security_short/fips), which is deferred to later steps—this is accurate.

Verification

lake build ToMathlib VCVio LatticeCrypto Extern HashSig Examples VCVioWidgets passes; nma_keyswap_hop_short, advantage_mldsaMLWEShort_le_matrix, and keygenShort_generable kernel-check [propext, Classical.choice, Quot.sound]. Both modified files pass CI linting.

Files by Nature

• LatticeCrypto/MLDSA/SecurityNMA.lean — the core of the change: definitions, theorems, and instances for the short-secret model, MLWE problems, NMA game, and the key-swap hop.
• LatticeCrypto/MLDSA/Scheme.lean — supporting definitions: validKeyPairShort and identificationSchemeShort.

Placeholders (sorry/admit)

None. The per-file summary for SecurityNMA.lean explicitly confirms that no sorry or admit statements are introduced, and this is verified by inspection of the added code.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	489
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 20 declaration(s)

LatticeCrypto/MLDSA/Scheme.lean (3)

• @[simp] theorem validKeyPairShort_eq_true_iff (pk : PublicKey p prims) (sk : SecretKey p) :
• def identificationSchemeShort
• noncomputable def validKeyPairShort (pk : PublicKey p prims) (sk : SecretKey p) : Bool

LatticeCrypto/MLDSA/SecurityNMA.lean (17)

• def expandAIdealization (p : Params) (prims : Primitives p)
• lemma advantage_mldsaMLWEShort_le_matrix {εA : ℝ}
• lemma mem_support_sampleShortVec {k b : ℕ} [SampleableType (RqVec k)] {v : RqVec k}
• lemma polyVecBounded_zero (k b : ℕ) : polyVecBounded (0 : RqVec k) b
• noncomputable def distinguisherBShort
• noncomputable def hrShort :
• noncomputable def keygenShort : ProbComp (PublicKey p prims × SecretKey p)
• noncomputable def keygenShort1 : ProbComp (PublicKey p prims × SecretKey p)
• noncomputable def matrixLift
• noncomputable def mldsaMLWEShort (p : Params) (prims : Primitives p)
• noncomputable def mldsaMatrixMLWE (p : Params)
• noncomputable def nmaAdvantageShort
• noncomputable def nmaGameShort
• noncomputable def sampleShortVec (k b : ℕ) [SampleableType (RqVec k)] : ProbComp (RqVec k)
• theorem keygenShort_generable :
• theorem nmaGameShort_eq_keygen_bind
• theorem nma_keyswap_hop_short

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• LatticeCrypto/MLDSA/Scheme.lean: Added validKeyPairShort, a noncomputable decidable predicate that holds when a key pair is built from bounded short vectors s₁, s₂ and seeds ρ, K directly (the ∃-material analogue of the existing ∃-seed validKeyPair), along with a @[simp] equivalence theorem validKeyPairShort_eq_true_iff. Also added identificationSchemeShort, which reuses the same commit/respond/verify algorithms as identificationScheme but is typed under the validKeyPairShort key relation, enabling the short-model security statements to refer to an idealized scheme where keys satisfy the material-based relation rather than the seed-derived one.
• LatticeCrypto/MLDSA/SecurityNMA.lean: This diff adds several new definitions, lemmas, and instances to SecurityNMA.lean that instantiate the "short-secret" idealized model for ML-DSA's EUF-NMA security. It introduces:

• polyVecBounded_zero: a lemma that the zero vector is b-bounded (polyVecBounded).
• sampleShortVec: a noncomputable probabilistic program that samples uniformly from the η-bounded box S_η^k.
• mem_support_sampleShortVec: a lemma that vectors in the support of sampleShortVec satisfy polyVecBounded.
• keygenShort and keygenShort1: noncomputable idealized key-generation procedures (public key t is ExpandA(ρ)·s₁ + s₂ vs. uniform, respectively).
• hrShort: a GenerableRelation over validKeyPairShort whose generator is keygenShort.
• keygenShort_generable: a theorem certifying that such a GenerableRelation is inhabited.
• nmaGameShort and nmaAdvantageShort: the EUF-NMA game and advantage over the short-key scheme (identificationSchemeShort).
• mldsaMLWEShort and mldsaMatrixMLWE: noncomputable definitions of the seed-based and uniform-matrix short-secret Module-LWE problems for ML-DSA.
• expandAIdealization: a definition of the ExpandA idealization assumption as a property (the pair (ρ, ExpandA(ρ)) is εA-indistinguishable from (ρ, A) with uniform independent A).
• distinguisherBShort: the induced short-model MLWE distinguisher.
• matrixLift: a function lifting a seed-based short-MLWE adversary to the uniform-matrix problem.
• advantage_mldsaMLWEShort_le_matrix: a lemma bounding the seed-based short-MLWE advantage by the uniform-matrix advantage plus εA under expandAIdealization.
• nmaGameShort_eq_keygen_bind and nma_keyswap_hop_short: theorems that provide an exact (no statistical slack) monadic rewrite identifying the short-model NMA-game gap with the mldsaMLWEShort distinguishing advantage of distinguisherBShort.

No sorry or admit statements are introduced by this diff.

---

Last updated: 2026-07-28 21:19 UTC.

[dtumad]

Reviewed the now-clean 489-line slice after #503 landed. The corrected model matches the relevant ML-DSA/Module-LWE semantics: s1 and s2 are sampled from the eta-bounded centered box, rather than using the information-theoretically trivial full-ring-uniform error; keygenShort and keygenShort1 differ only by replacing A·s1+s2 with uniform t; and the NMA game discards the secret key, so the proof correctly strips the independent K draw (and the now-unused short vectors on the uniform branch). The resulting key-swap is an exact game identity.

The seed-to-matrix bridge is also honestly scoped. expandAIdealization states the XOF-as-random-matrix replacement explicitly, and its docstring correctly notes that the unrestricted deterministic-function form is not a small-epsilon fact pending a cost-bounded model. matrixLift ignores the challenged matrix itself but receives its A·s+e target, which is exactly what the comparison requires.

I built LatticeCrypto from the exact post-merge head on Lean 4.32. One optional wording refinement: sampleShortVec k b is uniform over the subtype defined by the centered infinity-norm bound for every b; describing this as each coefficient uniform on the integer interval [-b,b] is literally exact only while b stays within the canonical centered residue range. That includes every intended ML-DSA eta, so it does not affect this model or any theorem. This looks safe to land once the rerun finishes.