ML-DSA on x86-64: the norm check and MakeHint with AVX2 (sign −8% instructions)

[alex]

Stacked on #513 (HighBits and LowBits with AVX2); only the last commit is new.

This PR is an implementation only. It changes nothing in Spec/ or TCB/.

What

vg_mldsa_norm_lt_avx2 and vg_mldsa_make_hint_avx2 work on eight coefficients at a time. In each 128-bit lane they run the VEX.256 form of SSE2 code over the lane's four doublewords, the same way high_bits/low_bits do in #513.

• norm_lt
  • The public bound is clamped to q first. This branches only on the public bound and doesn't change the result, because every reduced coefficient is below q.
  • After the clamp, a - b and (q - b) - a both fit in 32 bits, and one of them is negative exactly when a coefficient is out of bounds.
  • The ORs of the two differences are ANDed into an accumulator. Its sign bits are then spread across each doubleword (vpsrad 31), and the result is (vpmovmskb + 1) >> 32.
  • There is no branch on data.
• make_hint
  • r₁ of r and of (r + z) mod q comes from hbX (from ML-DSA on x86-64: HighBits and LowBits with AVX2 (sign −4% instructions) #513), with vcsub in between. The hint is ((r₁ ^ r₁') + 63) >> 6.
  • The eight hints of each iteration are stored. Their count is the sum of the nibbles of the vpmovmskb byte mask of the hints shifted to bit 7, computed with three shift-and-adds and added to r9.

Both are added to the MlDsaArith backend as variants of vg_mldsa_norm_lt and vg_mldsa_make_hint. With AVX2, signing calls both and verification calls norm_lt. check_variants passes.

The sign and verify call lemmas for these two callees (normCall_ok/_tr, hintCall_ok/_tr) now take any callee name, as bitsAt_ok already did.

Proofs

• Round/YNorm.lean
  • the per-doubleword differences and their sign bits (nlL_msb)
  • the accumulator invariant over the loop
  • vpmovmskb of all-set sign bits giving the result
• Round/YHint.lean
  • the hint of a doubleword is makeHint (mhL_toNat)
  • the nibble count (nib_bools, decided over the 256 cases, and bsum_sp)
  • the loop invariant (stores and running count)
  • the running count equals hintOnes (csum_onesFrom)

Constant time for both uses taint_decide.

Measurements

Instructions measured with callgrind, AVX2 configuration, compared with #513:

	before	after
ML-DSA-44, 20 deterministic signatures	58.2M	53.5M	−8.0%
ML-DSA-65, 20 deterministic signatures	82.2M	75.5M	−8.2%
ML-DSA-87, 20 deterministic signatures	113.8M	106.1M	−6.8%
ML-DSA-44, 20 verifications	23.5M	23.0M	−2.0%
ML-DSA-65, 20 verifications	35.7M	35.4M	−0.8%
ML-DSA-87, 20 verifications	72.0M	70.2M	−2.4%

With VG_CPU_FEATURES=none the counts are unchanged.

Checks

Run locally, all passing:

• lake build
• Emit.lean
• check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt
• cargo fmt / clippy
• cargo test with Wycheproof, both with default features and with VG_CPU_FEATURES=none --features cpu-features-env

The README algorithm table was regenerated with ci/algorithms_table.py.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr

---

Generated by Claude Code