ML-DSA: Implement hint pack functions

[marsella]

The HintBitPack and HintBitUnpack functions deal with sparse vectors and require tracking where the non-zero terms in a set of polynomials are. This kind of index-tracking functionality can be hard to express in Cryptol.

There's a version in the IPD that uses recursion but doesn't look a lot like the spec. I think it's worth exploring two avenues: try cleaning up the IPD version to see if it can be more closely mapped with some renaming and reordering; or try rewriting from scratch using a different approach (I briefly considered a recursive function that has Index as a type parameter and y as a continually-updated array).

The IPD omitted a malformed input check that was added back in the final draft. We need to make sure this gets added as well.

There are failure modes in HintBitUnpack so at the least, we should modify the existing implementation to return an Option that's None in the case of failures.

• Explore implementation approaches for HintBitPack; feel free to make a draft PR or post in the comments here with ideas to get feedback.
• Modify HintBitUnpack to return an option
• Explore implementation approaches for HintBitUnpack
• Make a property showing that unpack reverses pack.