int32_t_x2
static KRML_MUSTINLINE int32_t_x2
return (KRML_CLITERAL(int32_t_x2){ .fst = r00, .snd = r1 });
int32_t_x2
int32_t_x2 uu____0 = libcrux_ml_dsa_simd_portable_arithmetic_decompose_element(gamma2, r);
static KRML_MUSTINLINE int32_t_x2
return (KRML_CLITERAL(int32_t_x2){ .fst = t0, .snd = t1 });
int32_t_x2 uu____0 = libcrux_ml_dsa_simd_portable_arithmetic_power2round_element(t0->data[i0]);