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

[karthikbhargavan]

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?
• Use ghost state #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.