Eurydice_arr_bb0
Eurydice_arr_bb0 *secret_as_ntt
static KRML_MUSTINLINE Eurydice_arr_bb0
Eurydice_arr_bb0 arr_struct;
Eurydice_arr_bb0 u_as_ntt = arr_struct;
const Eurydice_arr_bb0 *secret_as_ntt,
const Eurydice_arr_bb0 *u_as_ntt
const Eurydice_arr_bb0 *secret_key,
Eurydice_arr_bb0
Eurydice_arr_bb0 arr_struct;
Eurydice_arr_bb0 secret_key_unpacked = arr_struct;
typedef struct Eurydice_arr_c10_s { Eurydice_arr_bb0 data[3U]; } Eurydice_arr_c10;
Eurydice_arr_bb0 t_as_ntt;
Eurydice_arr_bb0 uu____0;
Eurydice_arr_bb0 repeat_expression1[3U];
Eurydice_arr_bb0 lit;
memcpy(lit0.A.data, repeat_expression1, (size_t)3U * sizeof (Eurydice_arr_bb0));
Eurydice_arr_bb0 *deserialized_pk
static KRML_MUSTINLINE Eurydice_arr_bb0
Eurydice_arr_bb0 arr_mapped_str;
Eurydice_arr_bb0 sampled = libcrux_ml_kem_sampling_sample_from_xof_91(&seeds);
Eurydice_arr_bb0 fst;
Eurydice_arr_bb0 *re_as_ntt,
Eurydice_arr_bb0 *error_1
static KRML_MUSTINLINE Eurydice_arr_bb0
const Eurydice_arr_bb0 *r_as_ntt,
const Eurydice_arr_bb0 *error_1
Eurydice_arr_bb0 arr_struct;
Eurydice_arr_bb0 result = arr_struct;
const Eurydice_arr_bb0 *row = &a_as_ntt->data[i1];
Eurydice_arr_bb0 input,
Eurydice_arr_bb0 arr_struct0;
Eurydice_arr_bb0 r_as_ntt = arr_struct0;
Eurydice_arr_bb0 arr_struct;
Eurydice_arr_bb0 error_1 = arr_struct;
Eurydice_arr_bb0 u = libcrux_ml_kem_matrix_compute_vector_u_68(matrix, &r_as_ntt, &error_1);
const Eurydice_arr_bb0 *t_as_ntt,
const Eurydice_arr_bb0 *r_as_ntt,
const Eurydice_arr_bb0 *t_as_ntt,
const Eurydice_arr_bb0 *r_as_ntt,
Eurydice_arr_bb0 r_as_ntt = uu____0.fst;
static inline Eurydice_arr_bb0 libcrux_ml_kem_ind_cpa_unpacked_default_70_68(void)
Eurydice_arr_bb0 lit;
Eurydice_arr_bb0 *t_as_ntt,
const Eurydice_arr_bb0 *s_as_ntt,
const Eurydice_arr_bb0 *error_as_ntt
const Eurydice_arr_bb0 *row = &matrix_A->data[i0];
Eurydice_arr_bb0 *private_key,
Eurydice_arr_bb0 arr_struct;
Eurydice_arr_bb0 error_as_ntt = arr_struct;
const Eurydice_arr_bb0 *key,
const Eurydice_arr_bb0 *t_as_ntt,
const Eurydice_arr_bb0 *t_as_ntt,
const Eurydice_arr_bb0 *private_key
Eurydice_arr_bb0 private_key = libcrux_ml_kem_ind_cpa_unpacked_default_70_68();
static KRML_MUSTINLINE Eurydice_arr_bb0
Eurydice_arr_bb0 arr_struct;
Eurydice_arr_bb0 deserialized_pk = arr_struct;
Eurydice_arr_bb0
Eurydice_arr_bb0 ind_cpa_private_key;
static inline Eurydice_arr_bb0
Eurydice_arr_bb0 arr_struct;
Eurydice_arr_bb0
Eurydice_arr_bb0);
Eurydice_arr_bb0,