ML-DSA on x86-64: polynomial arithmetic in SSE2 (sign −19%, verify −11% instructions)

[alex]

Stacked on #464 (the SSE2 NTT). Its base is that PR's branch, so the diff here shows only this change. Once #464 merges, I'll retarget this PR to main.

What

vg_mldsa_multiply_ntt, vg_mldsa_multiply_add_ntt, vg_mldsa_add and vg_mldsa_sub on x86-64 now process four coefficients at a time in SSE2 registers. They reuse the vector helpers from #464 (Impl/MlDsa/X86_64/Arith/Vec.lean).

• Products: two Montgomery multiplications, with pmuludq on even lanes and pshufd 0xF5 for odd lanes. The first gives f·g·2⁻³²; multiplying that by 2⁶⁴ mod q gives f·g in [0, 2q), which vcsub reduces. multiply_add then adds h and reduces again.
• add / sub: paddd/psubd, then vcsub/vcadd.

MXCSR without stack

Because of pmuludq, the multiplications have to run inside ML-KEM's withMxcsr, so Intel's MCDT mitigation holds (ci/check_mcdt.py passes). These functions have no scratch buffer, and I didn't want to give them a stack frame either. On x86-64, Exec.frameSp and the taint analysis don't support frames yet, and every ML-DSA caller relies on NoSp. So MXCSR goes through the last 8 bytes of h:

1. Set r8 = h and load the last four coefficients of h into xmm6.
2. Run withMxcsr r8 1016 (prologue; 63-iteration loop over the first 252 coefficients; the last four from registers).
3. Store the last four coefficients after MXCSR is restored, overwriting the slot.

The contracts are unchanged (no stack), and so are the proofs of sign, keygen and verify.

Proofs (untrusted)

• mul_lane / mulAdd_lane: one lane of the product, from the existing mont_mont_R2.
• Mul.step, Mul.loop_ok, Mul.last, Mul.fn_ok: the loop, the last block, and the whole function.
• withMxcsrH_ok (Proof/MlDsa/X86_64/Arith/Mxcsr.lean): withMxcsr through the end of a writable polynomial, adapted from ML-KEM's withMxcsr_ok.
• AddSub is reproven the same way.
• Constant time uses taint_decide, as before.

There are no changes to TCB or Spec.

Performance

ML-DSA-65 instructions executed (callgrind, 20 operations, #464 → this PR):

	before	after
keygen	47.3M	46.2M	−2.4%
sign	174.1M	141.2M	−18.9%
verify	52.6M	46.7M	−11.2%

Criterion timings on this shared VM were within noise (±10%), so I'm reporting instruction counts.

docs/algorithms/ml-dsa-*.toml now say "SSE2 polynomial arithmetic", and the README tables are regenerated.

Checks run

• lake build
• lake env lean --run Emit.lean --check
• check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt
• cargo fmt --check, cargo clippy --all-targets -D warnings
• cargo test --release with Wycheproof: all pass

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr

---

Generated by Claude Code