Spec: ML-DSA's RejNTTPoly four times (vg_mldsa_rej_ntt_poly4)

[alex]

Trust change (Spec only). This is the first step towards sampling ML-DSA's matrix A four elements at a time on x86-64, with four SHAKE128 instances in AVX2 registers, as ML-KEM already does with vg_mlkem_sample_ntt4. Per CLAUDE.md, the spec goes in its own PR. The implementation, its proofs, and moving ExpandA in keygen, sign and verify onto it come in later PRs.

Why

With the AVX2 polynomial arithmetic (#491), Keccak is now the largest cost in ML-DSA on x86-64: about 38% of signing instructions, and more of keygen and verify. Most of the permutations are spent in ExpandA, which runs RejNTTPoly k·l times (30 for ML-DSA-65). Those calls are independent, so they suit the existing 4-way AVX2 Keccak (Impl/Sha3/X86_64/X4.lean).

What

All of this is in Spec/MlDsa/Poly.lean. It mirrors sampleNTT4Sig / sampleNTT4Contract / sampleNTT4Api from ML-KEM, and uses ML-DSA's own rejNTTPoly, Bounds, minBounds and leakBytes the same way rejNTTContract does.

• rejNTT4Sig: vg_mldsa_rej_ntt_poly4(seeds: *const [u8; 136], a: *mut [u32; 1024], scratch: *mut [u64; 1024]) -> u32. That is 8 KiB of scratch, the same as ML-KEM's vg_mlkem_sample_ntt4. The four interleaved states, the 4-way permutation's second buffer and its round-constant table already take 2,368 bytes before any squeezed output.
• seed4 and poly4: seed k is the 34 bytes from byte 34 k, and polynomial k starts at byte 1024 k.
• rejNTT4Contract. If it returns 1, every output polynomial is reduced and, for each k < 4, the polynomial at poly4 a k is RejNTTPoly(seed4 seeds k) for some bounds. If it returns 0, then RejNTTPoly fails within minBounds for at least one seed. It may leak the 136 seed bytes, which are public in ML-DSA (ρ and the indices). That is the same leakage as four calls to rejNTTContract.
• rejNTT4Api: name, module, contract on every target, and documentation, which reuses boundDoc and scratchSafety.

There are no other changes: no TCB, Impl or artifacts.

Checks run

• lake build +VerifiedGarbage.Spec.MlDsa.Poly
• check_lean_imports, check_lean_speed

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr