Verify ML-DSA

[franziskuskiefer]

The proofs require three levels of work:

• extract F* ML-DSA: Refactor code to so that Hax can process it. #341
• Lax-checking the F* code (also on CI)
• Verifying the platform-dependent code (simd/portable and simd/avx2)
• Verifying the generic ML-DSA code

We will begin with simd/portable in the second half of September,
wait for an optimized simd/avx2, and then move to the generic code.

---

• Add ML-DSA verification to CI #585
• Port Arithmetic proofs from ML-KEM to ML-DSA #583

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[karthikbhargavan]

The plan for the ML-DSA proofs are as follows:

1. Prove the arithmetic code (by porting them from ML-KEM where possible)
2. Prove the serialization code (by adapting and reusing the tactic from ML-KEM)
3. Prove the portable NTT code
4. Prove the optimized AVX2 NTT code
5. Set the pre- and post-conditions for the SIMD trait
6. Prove the generic algorithms