LatticeCrypto: discharging the challenge–secret norm-bound hypotheses — offering a proved no-wraparound multiplication bound

[jasonsoroko]

Several ML-DSA lemmas in LatticeCrypto currently carry the challenge–secret
product bound as a hypothesis rather than a theorem, e.g. the
h_s_bound-style binders in
MLDSA/Signature.lean
(also here and
here):

(h_s_bound : LatticeCrypto.cInfNorm ((prims.sampleInBall sig.cTilde • sk.s2).get j) ≤ p.beta)

We have a complete, sorry-free Lean 4 / Mathlib development of exactly this
fact and would like to contribute it. In your vocabulary (canonical vector
backend over ZMod q), the general lemma is:

theorem cInfNorm_mul_le_of_lt {q n} (c s : Poly (ZMod q) n)
    (h : 2 * (l1Norm c * cInfNorm s) < q) :
    cInfNorm (c * s) ≤ l1Norm c * cInfNorm s

Two points worth making explicit:

1. The size condition is essential, not an artifact. Over centered
   representatives the unconditional cInfNorm (c * s) ≤ l1Norm c * cInfNorm s
   is false — the centered lift of a product can wrap mod q. The
   2·(l1Norm c · cInfNorm s) < q guard is exactly the no-wraparound
   condition; for the FIPS 204 parameter sets it holds with 4 orders of
   magnitude to spare (2τη = 156 / 392 / 240 against q = 8380417). We
   believe this is precisely why the fact sits as a hypothesis today — it is
   a real theorem, not a one-liner.

2. The port looks direct. Since
   negacyclicMulPure_coeff
   makes your product coefficient definitionally a negacyclicConvCoeff, the
   proof reduces to (i) an integer-side bound on the negacyclic convolution
   (‖c·s‖∞ ≤ ‖c‖₁·‖s‖∞, which we have, sharp — the bound is attained), and
   (ii) the centered-lift/no-wrap argument through zmodCenteredCoeffView —
   the same uniqueness-of-small-representative fact we proved for
   ℤ_q[X]/(X^n+1), which needs only 1 < q (monicity of X^n + 1; no
   primality or field structure).

What we hold today, verified with #print axioms = [propext, Classical.choice, Quot.sound] throughout, on Lean 4.22.0 + Mathlib v4.22.0
(we would of course port to your v4.30.0 pin and house idioms per
AGENTS.md): the sharp product bound with an attainment witness; the
∃!-small-representative theorem mod q for any q > 1; and the y + c·s
no-wraparound corollary underpinning the ‖z‖∞ < γ₁ − β check (it
guarantees the centered mod-q representative of z is the faithful integer
value the check inspects), instantiated at all three FIPS 204 parameter
sets. The proof files, an axiom-audit transcript, and build instructions are
in this gist:
https://gist.github.com/jasonsoroko/79dab7c29a148f1766b2721aace8b4c1
(Full repository public with our forthcoming preprint.)

A natural follow-up we could include: l1Norm (sampleInBall x) ≤ τ appears
not to exist yet either — with it, the h_s_bound binders discharge
entirely; without it, they at least reduce to the more primitive sampler
sparsity spec.

Questions before we write any code:

1. Would you take this as a PR?
2. Preferred home and shape — a general cInfNorm_mul_le_of_lt in
   Ring/Norms.lean (possibly backend-generic via cInfNormOf/l1NormOf),
   or specialized lemmas next to their use sites in MLDSA/?
3. Is anyone already working on this among the current in-progress items?
   Happy to coordinate or stand down if so.
4. Any constraints beyond AGENTS.md, the v4.30.0 pin, and CI we should
   know about?

Disclosure: this development is human-directed and AI-assisted, with every
result kernel-checked and axiom-audited — we've read the workflow section of
the VCVio paper and aim to meet the same review bar as any other
contribution.

[jasonsoroko]

Congratulations on #479 — it lands what this issue offered, and then some: the unconditional cInfNorm_mul_le via the integer-side convolution plus the q/2 cap, the l1Norm (sampleInBall c̃) ≤ τ count by fuel induction, and the assembled concrete_sampleInBall_smul_bound discharging the Laws field for the real sampler. With those in the tree, the core of this issue is covered, and covered well.

One correction to my own point 1 above, which #479's statement exposes: I wrote that the unconditional cInfNorm (c * s) ≤ l1Norm c * cInfNorm s is false over centered representatives. As your q/2 case split shows, the capped-norm inequality is in fact unconditionally true — the wrap regime is exactly where the cap makes it trivial. The point I should have made is semantic, not boolean: 2·(l1Norm c · cInfNorm s) < q is what makes the centered representative faithful — equal to the true integer convolution — which is what the ‖z‖∞ < γ₁ − β check needs to be inspecting. Without the guard the inequality still holds but describes a wrapped value.

Three things we hold machine-checked that I don't see in the tree after #479, in case any are useful:

1. Attainment: the τ·η bound is exact — we exhibit c, s with ‖c·s‖∞ = τ·η, so β has no slack to recover (relevant to any future parameter-tightening discussion).
2. z = y + c·s faithfulness: an ∃!-small-representative theorem (any q > 1, needing only monicity of Xⁿ+1, no primality) giving that the centered representative of z is the integer the γ₁ − β check inspects, instantiated at all three FIPS 204 parameter sets — adjacent to fix(MLDSA): make Primitives.Laws inhabitable; bank the FIPS-shaped concrete witness #479's expandMask_bound correction to γ₁.
3. Rejection-sampling acceptance floors: a per-coordinate counting lower bound on the acceptance probability at δ := c·s, with concrete per-polynomial floors at the three parameter sets (e.g. ≥ 0.736 for ML-DSA-44) — possibly useful for quantitative completeness / expected-time statements over WithAbort.

Happy to open focused issues/PRs for any of these in your idiom (v4.31 noted), or to see this issue closed as addressed by #479 — either is a good outcome from where we sit. Nice work.

[dtumad]

@jasonsoroko I'm pinging @alik-eth who did most of this work, also heavily AI assisted. I'm not sure how much additional work they've done either beyond the PR. Maybe it would also make sense to have a larger tracking issue for LatticeCrypto as a whole to help coordinate overlapping external contributions?