[reaperhulk]

Signing computes each row of w = NTT⁻¹(Â ∘ ŷ) with one call to a new fused function, vg_mldsa_dot_inverse{4,5,7}. Before this change, each row took ℓ multiply and multiply-add calls followed by an inverse NTT.

What's new

• New implementations: Impl/MlDsa/X86_64/Arith/Dot.lean (SSE2) and dotInvAvx2 in Arith/Montgomery.lean (AVX2, suffix _avx2).
  • The function sums the ℓ products as 64-bit values (pmuludq on the even and on the psrlq 32 odd doublewords).
  • It reduces once per coefficient, then runs the existing inverse-NTT body. That body is factored out as nttInvBody / montInvBody and shared with vg_mldsa_ntt_inverse*, so the inverse-NTT code isn't duplicated.
• Proofs:
  • The two implementations are proven against the existing Spec.MlDsa.dotInverseContract (Proof/.../Arith/Dot.lean, YDot.lean), with shared lemmas in DotCore.lean and Proof/MlDsa/Arith/DotSum.lean.
  • Constant time is proven with taint_decide.
• Backend: MlDsaArith's backend gains the three dotInv functions, and PrimsOk gains dotInv.
• Signing:
  • rowW is a single dotInvAt call.
  • The multiply-add primitive is no longer used by signing, so it was removed from Prims.

No Spec/ or TCB/ change.

Instruction counts

callgrind, sign, 32 messages, AVX2:

	main	this PR	change
ML-DSA-44	965161	927948	−3.9%
ML-DSA-65	1541430	1465172	−4.9%
ML-DSA-87	1993758	1855599	−6.9%

Verification is unchanged.

Benchmarks (x86_64, mldsa, against main 7b0c28e): https://github.com/pyca/verified-garbage/actions/runs/41016364679

---

Generated by Claude Code