Verify ML-DSA

[franziskuskiefer]

trafficstars

The proofs require three levels of work:

• [x] extract F* #341
• [x] Lax-checking the F* code (also on CI)
• [ ] Verifying the platform-dependent code (simd/portable and simd/avx2)
• [ ] Verifying the generic ML-DSA code
• [ ] #585
• [ ] https://github.com/cryspen/home/issues/202

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.

---

Directory tree:

• [x] constants.rs (correctness) https://github.com/cryspen/libcrux/issues/746
• [ ] simd.rs (correctness)
  • [x] traits.rs https://github.com/cryspen/libcrux/issues/746
  • [ ] portable.rs
    • [x] vector_type.rs https://github.com/cryspen/libcrux/issues/746
    • [ ] arithmetic.rs (math) https://github.com/cryspen/libcrux/issues/744
    • [ ] encoding.rs (tactic)
      • [x] commitment.rs https://github.com/cryspen/libcrux/issues/745
      • [ ] error.rs
      • [ ] gamma1.rs
      • [ ] t0.rs
      • [ ] t1.rs
    • [ ] invntt.rs (math)
    • [ ] ntt.rs (math)
    • [ ] sample.rs
  • [ ] avx2.rs
    • [x] vector_type.rs https://github.com/cryspen/libcrux/issues/746
    • [ ] arithmetic.rs (math + simd, tactic?)
    • [ ] encoding.rs
      • [ ] commitment.rs
      • [ ] error.rs
      • [ ] gamma1.rs
      • [ ] t0.rs
      • [ ] t1.rs
    • [ ] invntt.rs
    • [ ] ntt.rs
    • [ ] rejection_sample.rs
      • [ ] less_than_eta.rs
      • [ ] less_than_field_modulus.rs
      • [ ] Shuffle_table.rs
  • [ ] tests.rs
• [ ] types.rs
• [ ] utils.rs
• [ ] arithmetic.rs (correctness)
• [ ] ntt.rs (correctness)
• [ ] polynomial.rs (correctness)
• [ ] matrix.rs (correctness)
• [ ] encoding.rs (correctness)
  • [ ] commitment.rs
  • [ ] error.rs
  • [ ] gamma1.rs
  • [ ] signature.rs
  • [ ] signing_key.rs
  • [ ] t0.rs
  • [ ] t1.rs
  • [ ] verification_key.rs
• [ ] ml_dsa_generic.rs (panic free, algorithmic correctness?)
  • [ ] instantiations
  • [ ] avx2.rs
  • [ ] instantiations.rs
  • [ ] multiplexing.rs
• [ ] hash_functions.rs (panic free)
• [ ] helper.rs (panic free)
• [ ] lib.rs (panic free)
• [ ] ml_dsa_44.rs (panic free)
• [ ] ml_dsa_65.rs (panic free)
• [ ] ml_dsa_87.rs (panic free)
• [ ] pre_hash.rs (panic free)
• [ ] sample.rs (panic free)
• [ ] samplex4.rs (panic free)

[github-actions[bot]]

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

[W95Psp]

[removed]

See https://github.com/cryspen/home/issues/274 instead.

[karthikbhargavan]

Most of our goals have been reached. It is now a matter of cleaning up and documenting what we proved which is on my plate.

[franziskuskiefer]

@karthikbhargavan a lot in here is stale. Please have a look and clean up.

[karthikbhargavan]

Yes, I'll do a round of cleanups, likely on Friday.

[karthikbhargavan]

We will close this after the meeting next week.

[karthikbhargavan]

We reached our milestone. Some TODOs and cleanups are collected here: https://github.com/cryspen/libcrux/issues/1084