Meta: Improve Specs and Reduce Annotations for ML-DSA Proofs

[karthikbhargavan]

trafficstars

While the first goal for ML-DSA verification is to get robust proofs in place, we would like to investigate and implement improvements in the style and follow them as we go forward. This issue collects such improvements, which can then be broken into separate sub-issues.

• [ ] Use &mut inputs rather than returning tuples in inner encoding functions
  • evaluate verification performance and document if doing this change would hurt perf
• [ ] Write serialization annotations (pre-/post-conditions, invariants) in Rust (not in F*)
  • Reflect bit-vector functions in Rust to make writing annotations in Rust possible
• [ ] Unroll loops in hax or in F*
  • Remove calc proofs to get more automation
• [ ] Investigate the use of SMT for these proofs
  • Are we already getting enough automation from F*->SMT?
• [ ] #783
  • Initial experiment here: https://hax-playground.cryspen.com/#fstar/3d2cbc0a9a/gist=1644de52204954e0a260187a5909403c
• [ ] Mutable arrays cannot change length, but we still need preconditions saying that the length did not change. Fix.

[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.

[franziskuskiefer]

@karthikbhargavan is this still something you plan on doing?

[karthikbhargavan]

yes. i will update with status and plans

[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.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.