ML-DSA: Define HashML-DSA external functions

[marsella]

We need to add the top-level external functions for HashML-DSA. As with the other external functions (#198), these must generate randomness, perform checks, and format inputs. Unlike the other external functions, these allow the user to pass a pre-hashed message, in case the hashing step in signing / verification is prohibitively slow.

This comes with lots of additional caveats, so document those warnings carefully!

Since we can't generate randomness in cryptol, we need to pass it as an Option instead (there's an example in ML-KEM).

• Decide whether to reimplement keygen or somehow include it over from ML-DSA: Define external functions #198.
• Implement Algorithm 4 Sign
• Implement Algorithm 5 Verify
• Add additional algorithm-level warnings as needed.