ML-DSA on x86-64: NTT and NTT⁻¹ in SSE2 (sign −48%, verify −35%)

[alex]

vg_mldsa_ntt and vg_mldsa_inv_ntt on x86-64 were scalar (a Barrett reduction with three muls per butterfly) and were over half of signing's time (NTT⁻¹ alone 41%). They now compute on four coefficients at a time in SSE2 registers (baseline x86-64, so no new variant), following ML-KEM's x86-64 NTT:

• Montgomery multiplication with pmuludq (vmont, Impl/MlDsa/X86_64/Arith/Vec.lean): the even doublewords are multiplied directly; the odd ones are moved down with pshufd 0xF5 and multiplied by the odd zetas (xmm12). For each product P, m = (P mod 2³²)·(−q⁻¹) mod 2³² is two more pmuludqs, and (P + m·q)/2³² is the high doubleword of paddq: psrlq moves the even results down, and the odd results are already in place, so por merges them. The result is in [0, 2q) for any doubleword input, and vcsub/vcadd (masks from psrad) reduce.
• Layers: len ≥ 4 broadcasts one zeta per block. len = 2 gathers the halves of two blocks with punpck{l,h}qdq. len = 1 gathers four blocks with pshufd 0xD8 + punpck{l,h}qdq, and puts them back with punpck{l,h}dq. NTT⁻¹ uses the same table of ζ·2³² mod q (the prologue stores it in scratch with 128 64-bit immediates) and computes ζ·(w[j+len] − w[j]), which is −ζ·(w[j] − w[j+len]). It then scales by 256⁻¹ with vmont by 16382.
• MCDT: the multiplications run inside ML-KEM's withMxcsr (MXCSR saved through scratch + 768, which the table overwrites in between). ci/check_mcdt.py passes.

Proofs

All untrusted. No changes to TCB/ or Spec/, and the contracts are unchanged.

• VArith: dword_montV (each lane of the register is mont of the lane product, via redc_toNat), plus the conditional add/sub lemmas and butterflies lane by lane.
• VLanes: vbfly_ok, vibfly_ok on registers. Each is one vrun over the SSE-only block.
• VMem: dlanes_load, polyIs_write2, vzeta_ok.
• VLay, VLay21: adapted from ML-KEM's VLay/VLay42 to doublewords, operating on f in place.
• Ntt, NttInv: the table store (dwordTab_ok), the layer chain, vscale_ok, and mx_correct (ML-KEM's withMxcsr_ok plus abiPreserved_of_ctl).
• Signing and verification used to require that no instruction of their code (callees included) loads MXCSR. They now use ctlOk, as ML-KEM's top-level functions do. For verification, this goes through a new compositional check, ctlC (Proof/Framework/X86_64/Mxcsr.lean), so it keeps its evaluate-with-empty-primitives approach (verify_c).
• The scalar NTT's proofs (NttBfly, NttLoop, storeTab_ok) and storeTab are removed. They are now unused.

Performance

Criterion (cargo bench -- mldsa), old and new back to back on the same machine. It is a shared cloud VM, so expect ±10% noise.

	keygen	sign	verify
ML-DSA-44	157 → 140 µs	1.064 → 0.512 ms	163 → 96 µs
ML-DSA-65	276 → 248 µs	1.534 → 0.808 ms	281 → 181 µs
ML-DSA-87	426 → 357 µs	1.751 → 0.965 ms	477 → 311 µs

The README table now reads "SSE2 NTT" for ML-DSA on x86-64 (docs/algorithms/ml-dsa-*.toml, regenerated).

Checks run locally

• Full lake build (all 5527 jobs) and lake env lean --run Emit.lean. Only src/asm/x86_64/mldsa.rs changed.
• check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt, algorithms_table --check: all pass.
• cargo fmt --check and cargo clippy --all-targets -- -D warnings: clean.
• cargo test with Wycheproof, with and without cpu-features-env: all pass.

Follow-ups planned in separate PRs: SSE2 pointwise multiplication, AVX2 variants, and faster sampling.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr

---

Generated by Claude Code

[alex]

Rust (Thumb, stable) and the armv7l rust job failed in rustup toolchain install before building anything (failure removing component 'cargo-armv7-unknown-linux-gnueabihf' … share/man/man1/cargo.1, from the stable 1.99 update inside the container). That isn't caused by this PR, and it failed the same way on a re-run. Main fixed it with "Use a fresh rustup home for ARM benchmark containers" (in #460/#462), so I merged main into this branch (e49e9bb). The merge has no conflicts and touches nothing in the x86-64 ML-DSA code or the framework it uses.

---

Generated by Claude Code