9384     Eurydice_slice public_key,  in libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_33()  argument
9391        i < Eurydice_slice_len(public_key, uint8_t) /  in libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_33()
9396         public_key, i0 * LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT,  in libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_33()
10805 static inline void libcrux_ml_kem_ind_cpa_encrypt_60(Eurydice_slice public_key,  in libcrux_ml_kem_ind_cpa_encrypt_60()  argument
10811       Eurydice_slice_subslice_to(public_key, (size_t)1152U, uint8_t, size_t),  in libcrux_ml_kem_ind_cpa_encrypt_60()
10814       Eurydice_slice_subslice_from(public_key, (size_t)1152U, uint8_t, size_t);  in libcrux_ml_kem_ind_cpa_encrypt_60()
11085     libcrux_ml_kem_types_MlKemPublicKey_15 *public_key,  in libcrux_ml_kem_ind_cca_encapsulate_cd()  argument
11099                               libcrux_ml_kem_types_as_slice_cb_50(public_key),  in libcrux_ml_kem_ind_cca_encapsulate_cd()
11114       (size_t)1184U, libcrux_ml_kem_types_as_slice_cb_50(public_key), uint8_t);  in libcrux_ml_kem_ind_cca_encapsulate_cd()
11159     libcrux_ml_kem_types_MlKemPublicKey_15 *public_key,  in libcrux_ml_kem_ind_cca_instantiations_portable_encapsulate_c6()  argument
11161   libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key;  in libcrux_ml_kem_ind_cca_instantiations_portable_encapsulate_c6()
11176     libcrux_ml_kem_types_MlKemPublicKey_15 *public_key,  in libcrux_ml_kem_mlkem768_portable_encapsulate()  argument
11178   libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key;  in libcrux_ml_kem_mlkem768_portable_encapsulate()
11494     Eurydice_slice private_key, Eurydice_slice public_key,  in libcrux_ml_kem_ind_cca_serialize_kem_secret_key_48()  argument
11512           uu____3, uu____4, uu____5 + Eurydice_slice_len(public_key, uint8_t),  in libcrux_ml_kem_ind_cca_serialize_kem_secret_key_48()
11514       public_key, uint8_t);  in libcrux_ml_kem_ind_cca_serialize_kem_secret_key_48()
11515   pointer = pointer + Eurydice_slice_len(public_key, uint8_t);  in libcrux_ml_kem_ind_cca_serialize_kem_secret_key_48()
11519   libcrux_ml_kem_hash_functions_portable_H_f1_1a(public_key, ret0);  in libcrux_ml_kem_ind_cca_serialize_kem_secret_key_48()
11569   uint8_t public_key[1184U];  in libcrux_ml_kem_ind_cca_generate_keypair_8c()  local
11570   memcpy(public_key, uu____0.snd, (size_t)1184U * sizeof(uint8_t));  in libcrux_ml_kem_ind_cca_generate_keypair_8c()
11574       Eurydice_array_to_slice((size_t)1184U, public_key, uint8_t),  in libcrux_ml_kem_ind_cca_generate_keypair_8c()
11585   memcpy(copy_of_public_key, public_key, (size_t)1184U * sizeof(uint8_t));  in libcrux_ml_kem_ind_cca_generate_keypair_8c()
11834     libcrux_ml_kem_types_MlKemPublicKey_15 *public_key,  in libcrux_ml_kem_ind_cca_encapsulate_cd0()  argument
11848                               libcrux_ml_kem_types_as_slice_cb_50(public_key),  in libcrux_ml_kem_ind_cca_encapsulate_cd0()
11863       (size_t)1184U, libcrux_ml_kem_types_as_slice_cb_50(public_key), uint8_t);  in libcrux_ml_kem_ind_cca_encapsulate_cd0()
11912     libcrux_ml_kem_types_MlKemPublicKey_15 *public_key,  in libcrux_ml_kem_ind_cca_instantiations_portable_kyber_encapsulate_7a()  argument
11914   libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key;  in libcrux_ml_kem_ind_cca_instantiations_portable_kyber_encapsulate_7a()
11929     libcrux_ml_kem_types_MlKemPublicKey_15 *public_key,  in libcrux_ml_kem_mlkem768_portable_kyber_encapsulate()  argument
11931   libcrux_ml_kem_types_MlKemPublicKey_15 *uu____0 = public_key;  in libcrux_ml_kem_mlkem768_portable_kyber_encapsulate()
12067   uint8_t public_key[1184U];  in libcrux_ml_kem_ind_cca_generate_keypair_8c0()  local
12068   memcpy(public_key, uu____0.snd, (size_t)1184U * sizeof(uint8_t));  in libcrux_ml_kem_ind_cca_generate_keypair_8c0()
12072       Eurydice_array_to_slice((size_t)1184U, public_key, uint8_t),  in libcrux_ml_kem_ind_cca_generate_keypair_8c0()
12083   memcpy(copy_of_public_key, public_key, (size_t)1184U * sizeof(uint8_t));  in libcrux_ml_kem_ind_cca_generate_keypair_8c0()
12212     Eurydice_slice public_key,  in libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_330()  argument
12219        i < Eurydice_slice_len(public_key, uint8_t) /  in libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_330()
12224         public_key, i0 * LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT,  in libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_330()
12254     uint8_t *public_key) {  in libcrux_ml_kem_ind_cca_validate_public_key_19()  argument
12257       Eurydice_array_to_subslice_to((size_t)1184U, public_key, (size_t)1152U,  in libcrux_ml_kem_ind_cca_validate_public_key_19()
12264       Eurydice_array_to_subslice_from((size_t)1184U, public_key, (size_t)1152U,  in libcrux_ml_kem_ind_cca_validate_public_key_19()
12268       (size_t)1184U, public_key, public_key_serialized, uint8_t, uint8_t, bool);  in libcrux_ml_kem_ind_cca_validate_public_key_19()
12284     uint8_t *public_key) {  in libcrux_ml_kem_ind_cca_instantiations_portable_validate_public_key_4b()  argument
12285   return libcrux_ml_kem_ind_cca_validate_public_key_19(public_key);  in libcrux_ml_kem_ind_cca_instantiations_portable_validate_public_key_4b()
12294     libcrux_ml_kem_types_MlKemPublicKey_15 *public_key) {  in libcrux_ml_kem_mlkem768_portable_validate_public_key()  argument
12296       public_key->value);  in libcrux_ml_kem_mlkem768_portable_validate_public_key()