ML-DSA: Optimize implementation

[marsella]

The version of ML-DSA that is currently being developed is very closely adherent to the spec. However, the spec is not written in a way that lends itself to fast Cryptol code. There are two particular types of slow-code that I've noticed:

• direct indexing while operating over arrays; and
• iterating + rebuilding arrays instead of using sequence-level operations (e.g. join, reverse, etc.)

In general, we don't want to delete the spec-adherent code, because spec adherence is a high-level goal of this repository. We can either make separate functions inline (e.g. BitsToBytes_fast) or make a separate module with the fast versions -- this might depend a little on the architecture decision we make in #198. In either case we need to prove equivalence between the spec version and the fast version.

Here are a few notes about things I've seen that could probably be faster:

• IntegerToBits: we could use the built-in function fromInteger, with a reverse call to get the endianness right. Similarly with BitsToInteger and probably IntegerToBytes
• BitsToBytes and BytesToBits: these should just be split and join calls.
• All the BitPack functions (Alg 16 - 19) index into an array, but they could iterate directly over it instead.

---

• Audit or benchmark the spec to identify areas for improvement (either based on Cryptol aesthetics or on some actual timing measurements). Put a list in this issue for future reference.
• Decide where to put the "fast" versions.
• Implement the optimized versions.