Add proofs for Ind_cpa functions

[mamonet]

This PR adds spec for unpacked functions and writes full proofs for Ind_cpa functions.

Note there's a mismatch between the spec and implementation for generate_keypair function, I will confirm the right procedure and upload the changes for this function.

[mamonet]

generate_keypair calls Scheme::cpa_keygen_seed which have the following post-condition https://github.com/cryspen/libcrux/blob/Ind-cpa-proofs-refined/libcrux-ml-kem/src/variant.rs#L97-L99
However, generate_keypair spec has different parameter for v_G https://github.com/cryspen/libcrux/blob/dev/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst#L226
I modified the spec here https://github.com/cryspen/libcrux/blob/Ind-cpa-proofs-refined/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst#L238
@karthikbhargavan is the new spec supposed to be right?

[karthikbhargavan]

Good catch, FIPS 203 says: : (𝜌,𝜎) ← G(𝑑‖𝑘)
Which is what the new fix does.