fix(LatticeCrypto): bind SelfTargetMSIS solutions to their hashed preimage

[alik-eth]

Extracts the generic SelfTargetMSIS binding repair as a small, self-contained PR — step 1 of the decomposition @dtumad proposed on #467/#479. It is independently necessary (it closes a soundness gap in the tailored ML-DSA self-target problem) and it unblocks a sound review of #479.

The soundness gap

SelfTargetMSIS.Problem.isValid received only Challenge → Target → HashOutput → Response, never the RO preimage the experiment looks up. So mldsaSTMSIS.isValid recomputed a commitment w' from (pk, c̃, (z, h)) and verified against that same recomputed value, without ever requiring the commitment component of the hashed pair (msg, w) to equal w'. The relevant equality closed as X = X. That makes the tailored problem strictly easier than the literature relation — a zero-response / zero-hint solution wins after querying an unrelated commitment, subject only to the verifier norm gates.

The repair

• Generic (ShortIntegerSolution.lean): isValid : Challenge → Target → HashInput → HashOutput → Response → Bool, and experiment now passes the cache-consistent hashInput (the same preimage it already looks up) into isValid. The structure's type parameters are unchanged, so abstract references to SelfTargetMSIS.Problem … elsewhere are unaffected.
• ML-DSA binding (SecurityNMA.lean): mldsaSTMSIS.isValid now additionally requires hashInput.2 = w' — the recovered commitment must equal the commitment component of the hashed preimage. On the accepting path the forger's own returned (msg, w') is the queried preimage, so the extraction proof discharges the binding for free (it reduces to w' = w'); the read-back proof (stmsis_tail_le) is updated accordingly.
• Characterization (mldsaSTMSIS_isValid_eq_true_iff): acceptance is exactly verifier acceptance ∧ the binding conjunct, stated explicitly so the self-target requirement stays visible — an instantiation that silently dropped the preimage would fail this lemma, making the regression hard to reintroduce.

Scope (deliberately narrow)

This PR fixes only the SelfTargetMSIS binding. The other items from the #467 review are separate, larger pieces and are not in this PR:

• the short-secret MLWE model / exact short-key swap (the full-ring-uniform MLWE issue) — a focused model PR;
• the explicit reduction from this tailored verifier relation to the standard-STMSIS normal form (H([I_m | A]·y, μ) with the challenge as y's final coefficient block) — the endpoint bridge;
• the generic CMA-to-NMA engine.

The characterization lemma here is the lightweight binding statement, not the full algebraic normal-form bridge (that lives with the standard-STMSIS reduction).

Verification

Off current main. lake build LatticeCrypto (and the full CI library set) green on Lean v4.32.0; mldsaSTMSIS_isValid_eq_true_iff and the affected nmaAdvantage_keygen1_le_stmsis extraction kernel-check [propext, Classical.choice, Quot.sound]. No statement outside the three touched declarations changes.

https://claude.ai/code/session_01DaNGD9nDo3Grwk58nsjS77

[github-actions]

🤖 PR Summary

PR Overview: Bind SelfTargetMSIS solutions to their hashed preimage

This PR closes a soundness gap in the ML-DSA tailored SelfTargetMSIS problem by requiring isValid to check the hash preimage's commitment component against the recovered commitment. The change is concentrated in two files; no public API surface beyond the SelfTargetMSIS.Problem structure's isValid signature changes.

Mathematical Formalization

• LatticeCrypto/HardnessAssumptions/ShortIntegerSolution.lean: The generic SelfTargetMSIS problem definition is updated.

  • SelfTargetMSIS.Problem structure
    • Changed field isValid from type Challenge → Target → HashOutput → Response → Bool to Challenge → Target → HashInput → HashOutput → Response → Bool.
  • The experiment function now passes the hashInput (the same preimage it looks up in its cache) as the third argument to problem.isValid.
  • Module-level comment and Problem docstring updated to reflect the new binding requirement.

• LatticeCrypto/MLDSA/SecurityNMA.lean: The ML-DSA specific instance is repaired.

  • mldsaSTMSIS.isValid: Extended with a conjunct hashInput.2 = w' (the recovered commitment must equal the commitment component of the hashed preimage), implemented via decide and &&.
  • New theorem mldsaSTMSIS_isValid_eq_true_iff: Characterizes isValid = true as the conjunction of the generic binding condition and the identification scheme's verify returning true. This makes the self-target binding requirement explicit and hard to silently drop in future instantiations.
  • Private theorem stmsis_tail_le: Updated proof to pass the full hashInput = (msg, w') to isValid and adapted body accordingly.

Proof Completion (sorries removed)

No sorry or admit placeholders were added or removed. All changes are complete and verified by lake build LatticeCrypto.

Refactoring

The SelfTargetMSIS.Problem structure's isValid signature change is the only breaking API change. Abstract references to SelfTargetMSIS.Problem … elsewhere in the library are type-parameter-preserving and unaffected. The PR is deliberately scoped to this binding repair; the items from the #467 review (short-secret MLWE model, standard-STMSIS normal form reduction, generic CMA-to-NMA engine) are deferred to separate PRs.

Scope

• Core change: ShortIntegerSolution.lean and SecurityNMA.lean as described above.
• No other files touched; no statements outside mldsaSTMSIS_isValid_eq_true_iff, stmsis_tail_le, and the isValid definitions are altered.

Note on PR Body Accuracy

• The PR body's description of the change is accurate. The per-file summaries confirm the isValid signature change in ShortIntegerSolution.lean and the binding conjunct addition and characterization lemma in SecurityNMA.lean.
• The body's statement that "abstract references to SelfTargetMSIS.Problem … elsewhere are unaffected" is correct because only the isValid field's signature changed, not the structure's type parameters.
• No discrepancies between the PR body and the actual code changes were found.

No other headers apply: This PR does not touch Protocols, Soundness (beyond the soundness repair itself), Infrastructure/CI, Documentation, or Refactoring (beyond the minimal signature change).

Key Files

1. LatticeCrypto/HardnessAssumptions/ShortIntegerSolution.lean
2. LatticeCrypto/MLDSA/SecurityNMA.lean

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	48
❌ Lines Removed	17

---

Lean Declarations

✏️ Added: 1 declaration(s)

LatticeCrypto/MLDSA/SecurityNMA.lean (1)

• theorem mldsaSTMSIS_isValid_eq_true_iff (aHat : TqMatrix p.k p.l) (pk : PublicKey p prims)

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

No findings.

---

📄 **Per-File Summaries**

• LatticeCrypto/HardnessAssumptions/ShortIntegerSolution.lean: The file LatticeCrypto/HardnessAssumptions/ShortIntegerSolution.lean updates the SelfTargetMSIS problem definition to require the isValid predicate to take the adversary's hash preimage (HashInput) in addition to the hash output (HashOutput). The SelfTargetMSIS.Problem structure's isValid field signature changed from Challenge → Target → HashOutput → Response → Bool to Challenge → Target → HashInput → HashOutput → Response → Bool. The experiment's call to problem.isValid now passes hashInput as the third argument. The module-level comment and the Problem structure's docstring were updated to describe this
• LatticeCrypto/MLDSA/SecurityNMA.lean: The diff modifies mldsaSTMSIS's isValid field to additionally check that the hash preimage's commitment component (hashInput.2) equals the recovered commitment w' (using decide and &&), making the self-target binding explicit in the relation. It adds a new theorem mldsaSTMSIS_isValid_eq_true_iff that characterizes isValid = true as the conjunction of this binding condition and the identification scheme's verify returning true. The private theorem stmsis_tail_le is updated to pass the full hashInput (now (msg, w')) to isValid and its proof is adapted accordingly.

---

Last updated: 2026-07-28 10:16 UTC.

[dtumad]

Reviewed the exact head against the generic experiment, the ML-DSA extraction, and the standard self-target shape used in the Dilithium literature. This is the focused soundness repair the stack needs: the experiment still enforces RO consistency through the cache, but now also makes that exact preimage available to validity; the ML-DSA instance uses it to require the hashed commitment to equal the commitment recovered from the response. The characterization theorem exposes that conjunct directly, and the NMA extractor preserves it by querying and returning the same (message, commitment) pair.

The scope is appropriately narrow: this fixes the previously trivial tailored relation without claiming that the tailored UseHint/HighBits relation has already been reduced to standard [I | A]-form SelfTargetMSIS. I also built LatticeCrypto from this exact head on Lean 4.32. This looks safe to land as the dependency root for #504/#506.