Add input validation functions and docs to ML-KEM

[marsella]

The current implementation of ML-KEM does not quite align with the spec. The spec defines "internal" functions that run the actual computations, and "external" functions that require input validation and sample / check randomness in a specific way. We have functions whose names match the "external" functions but implementation and docs match the "internal" ones. We also don't have any of the required input validation implemented.

This is for the Encaps, Decaps, and Keygen functions in ML-KEM.

• Rename existing functions to _internal and update docs accordingly
• Make non-suffix "external" functions that (a) throw an error if the randomness is not suitable and (b) document the required input validation
• Make (public) input validation functions
  • Key pair check in 7.1
  • Encapsulation key check in 7.2
  • Decapsulation input check in 7.3
• Add properties of input validation functions (e.g. that outputs from the ml kem functions are valid)
• Make sure documentation across the board is clear about failure cases if you don't validate input. Also, add big warnings about randomness generation that Cryptol cannot do itself.