libcrux_ml_kem_vector_portable_serialize_deserialize_4_int
int16_t_x8 v0_7 = libcrux_ml_kem_vector_portable_serialize_deserialize_4_int(
int16_t_x8 v8_15 = libcrux_ml_kem_vector_portable_serialize_deserialize_4_int(