CBMC: Consider providing functional specs for make_hint and unpack_hint

cf https://github.com/pq-code-package/mldsa-native/pull/1028#discussion_r3186069202

The current specs are enough for type-safety and memory-safety, but it seems we have an opportunity to capture (some aspect of) correctness of hint packing/unpacking as well. Investigate.