Spec: ML-DSA's ExpandMask four polynomials at a time (vg_mldsa_expand_mask_poly4)

[alex]

Trust change (Spec only). This PR is stacked on #492, whose poly4 it reuses. Its base is #492's branch, so the diff shows only this change. It will be retargeted to main once #492 merges.

Why

With the AVX2 polynomial arithmetic (#491) and ExpandA four entries at a time (on top of #492), ExpandMask is the largest remaining Keccak cost in ML-DSA signing on x86-64. On ML-DSA-65 it is about 16–19% of the instructions per signature. Each iteration of the signing loop calls vg_mldsa_expand_mask_poly ℓ times, on independent seeds ρ″ ‖ IntegerToBytes(κ + r, 2). Those calls suit four SHAKE256 instances at once in AVX2 registers, as vg_mldsa_rej_ntt_poly4 runs four SHAKE128 instances.

What

All of this is in Spec/MlDsa/Poly.lean. It mirrors rejNTT4Sig / rejNTT4Contract / rejNTT4Api from #492, and reuses expandMaskContract's postcondition for each polynomial:

• expandMask4Sig: vg_mldsa_expand_mask_poly4(seeds: *const [u8; 264], gamma1: u32, a: *mut [u32; 1024], scratch: *mut [u64; 1024]). The 8 KiB of scratch is the same as vg_mldsa_rej_ntt_poly4's: four interleaved states, the permutation's second buffer and round-constant table, and 4 × 640 bytes of squeezed output.
• seed66: seed k is the 66 bytes from byte 66 k. Polynomial k starts at poly4 a k (byte 1024 k), as in Spec: ML-DSA's RejNTTPoly four times (vg_mldsa_rej_ntt_poly4) #492.
• expandMask4Contract:
  • Precondition: gamma1 is 2¹⁷ or 2¹⁹, as for expandMaskContract.
  • Postcondition: for each k < 4, the polynomial at poly4 a k is toRq (BitUnpack(H(seed66 seeds k, 32c), γ₁ − 1, γ₁)) and is reduced.
  • No leakage beyond the pointers and gamma1. This is the same as expandMaskContract, since the seeds hold the secret ρ″.
• expandMask4Api: the name, module, contract on every target, and documentation. It reuses ctDoc and scratchSafety.

There are no other changes: no TCB, Impl or artifacts. The implementation and its proofs come in a later PR:

• a baseline that makes four calls of vg_mldsa_expand_mask_poly;
• an AVX2 variant on the existing 4-way Keccak.

Moving signing onto it comes in that PR too.

Checks run

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

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ddof3szoTi7HB8iCsM2MCr

---

Generated by Claude Code