diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt index 835226d4d..e73598e22 100644 --- a/libcrux-ml-kem/cg/code_gen.txt +++ b/libcrux-ml-kem/cg/code_gen.txt @@ -1,5 +1,5 @@ This code was generated with the following tools: Charon: 0f1b5e50fa4e96ed9e650d8334e1afbf2bf319b1 Eurydice: e888878c640c71e2cd0456ed51d70c9b054470e6 -Karamel: f13006e27305a378b68d3686425a096e9bc05f86 +Karamel: 65aab550cf3ba36d52ae6ad1ad962bb573406395 F*: 07b5a2101c86f81d9a2d31ca68eb855ee361bacc diff --git a/libcrux-ml-kem/cg/eurydice_glue.h b/libcrux-ml-kem/cg/eurydice_glue.h index 48455c2d7..4f3e2d5f4 100644 --- a/libcrux-ml-kem/cg/eurydice_glue.h +++ b/libcrux-ml-kem/cg/eurydice_glue.h @@ -120,6 +120,12 @@ static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t buf[8]) { return v; } +static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) { + uint32_t v; + memcpy(&v, buf, sizeof(v)); + return v; +} + static inline uint32_t core_num__u8_6__count_ones(uint8_t x0) { #ifdef _MSC_VER return __popcnt(x0); diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h index a3018698d..fbde3222b 100644 --- a/libcrux-ml-kem/cg/libcrux_core.h +++ b/libcrux-ml-kem/cg/libcrux_core.h @@ -2,7 +2,7 @@ This file was generated by KaRaMeL KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../cg.yaml -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: - 07b5a210 KaRaMeL version: f13006e2 + 07b5a210 KaRaMeL version: 65aab550 */ #ifndef __libcrux_core_H @@ -37,6 +37,8 @@ static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x0, uint16_t x1); #define CORE_NUM__U32_8__BITS (32U) +static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t x0[4U]); + static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t x0[8U]); static inline void core_num__u64_9__to_le_bytes(uint64_t x0, uint8_t x1[8U]); @@ -314,6 +316,30 @@ static KRML_MUSTINLINE void libcrux_ml_kem_utils_into_padded_array___64size_t( memcpy(ret, out, (size_t)64U * sizeof(uint8_t)); } +typedef struct + core_result_Result__uint8_t_4size_t__core_array_TryFromSliceError_s { + core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError_tags tag; + union { + uint8_t case_Ok[4U]; + core_array_TryFromSliceError case_Err; + } val; +} core_result_Result__uint8_t_4size_t__core_array_TryFromSliceError; + +static inline void +core_result__core__result__Result_T__E___unwrap__uint8_t_4size_t__core_array_TryFromSliceError( + core_result_Result__uint8_t_4size_t__core_array_TryFromSliceError self, + uint8_t ret[4U]) { + if (self.tag == core_result_Ok) { + uint8_t f0[4U]; + memcpy(f0, self.val.case_Ok, (size_t)4U * sizeof(uint8_t)); + memcpy(ret, f0, (size_t)4U * sizeof(uint8_t)); + } else { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, + "unwrap not Ok"); + KRML_HOST_EXIT(255U); + } +} + typedef struct core_result_Result__int16_t_16size_t__core_array_TryFromSliceError_s { core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError_tags tag; diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h index 4eeae547d..834933d26 100644 --- a/libcrux-ml-kem/cg/libcrux_ct_ops.h +++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h @@ -2,7 +2,7 @@ This file was generated by KaRaMeL KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../cg.yaml -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: - 07b5a210 KaRaMeL version: f13006e2 + 07b5a210 KaRaMeL version: 65aab550 */ #ifndef __libcrux_ct_ops_H diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h index ffb5199b9..5edf102f4 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h @@ -2,7 +2,7 @@ This file was generated by KaRaMeL KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../cg.yaml -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: - 07b5a210 KaRaMeL version: f13006e2 + 07b5a210 KaRaMeL version: 65aab550 */ #ifndef __libcrux_mlkem768_avx2_H @@ -19,6 +19,26 @@ extern "C" { #include "libcrux_sha3_avx2.h" #include "libcrux_sha3_portable.h" +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_avx2_G( + Eurydice_slice input, uint8_t ret[64U]) { + uint8_t digest[64U] = {0U}; + libcrux_sha3_portable_sha512( + Eurydice_array_to_slice((size_t)64U, digest, uint8_t, Eurydice_slice), + input); + memcpy(ret, digest, (size_t)64U * sizeof(uint8_t)); +} + +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_avx2_H( + Eurydice_slice input, uint8_t ret[32U]) { + uint8_t digest[32U] = {0U}; + libcrux_sha3_portable_sha256( + Eurydice_array_to_slice((size_t)32U, digest, uint8_t, Eurydice_slice), + input); + memcpy(ret, digest, (size_t)32U * sizeof(uint8_t)); +} + typedef core_core_arch_x86___m256i libcrux_ml_kem_vector_avx2_SIMD256Vector; KRML_ATTRIBUTE_TARGET("avx2") @@ -47,6 +67,24 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc return libcrux_ml_kem_vector_avx2_from_i16_array(array); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_to_i16_array( + core_core_arch_x86___m256i v, int16_t ret[16U]) { + int16_t output[16U] = {0U}; + libcrux_intrinsics_avx2_mm256_storeu_si256_i16( + Eurydice_array_to_slice((size_t)16U, output, int16_t, Eurydice_slice), v); + memcpy(ret, output, (size_t)16U * sizeof(int16_t)); +} + +KRML_ATTRIBUTE_TARGET("avx2") +static inline void +libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__avx2__SIMD256Vector___to_i16_array( + core_core_arch_x86___m256i x, int16_t ret[16U]) { + int16_t ret0[16U]; + libcrux_ml_kem_vector_avx2_to_i16_array(x, ret0); + memcpy(ret, ret0, (size_t)16U * sizeof(int16_t)); +} + KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE core_core_arch_x86___m256i libcrux_ml_kem_vector_avx2_arithmetic_add(core_core_arch_x86___m256i lhs, @@ -1112,99 +1150,19 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc return libcrux_ml_kem_vector_avx2_serialize_deserialize_10(bytes); } -KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_to_i16_array( - core_core_arch_x86___m256i v, int16_t ret[16U]) { - int16_t output[16U] = {0U}; - libcrux_intrinsics_avx2_mm256_storeu_si256_i16( - Eurydice_array_to_slice((size_t)16U, output, int16_t, Eurydice_slice), v); - memcpy(ret, output, (size_t)16U * sizeof(int16_t)); -} - -typedef struct libcrux_ml_kem_vector_avx2_portable_PortableVector_s { - int16_t elements[16U]; -} libcrux_ml_kem_vector_avx2_portable_PortableVector; - -KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE libcrux_ml_kem_vector_avx2_portable_PortableVector -libcrux_ml_kem_vector_avx2_portable_from_i16_array(int16_t array[16U]) { - int16_t uu____0[16U]; - memcpy(uu____0, array, (size_t)16U * sizeof(int16_t)); - libcrux_ml_kem_vector_avx2_portable_PortableVector lit; - memcpy(lit.elements, uu____0, (size_t)16U * sizeof(int16_t)); - return lit; -} - -KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_portable_serialize_11( - libcrux_ml_kem_vector_avx2_portable_PortableVector v, uint8_t ret[22U]) { - uint8_t result[22U] = {0U}; - result[0U] = (uint8_t)v.elements[0U]; - result[1U] = (uint32_t)(uint8_t)(v.elements[1U] & (int16_t)31) << 3U | - (uint32_t)(uint8_t)(v.elements[0U] >> 8U); - result[2U] = (uint32_t)(uint8_t)(v.elements[2U] & (int16_t)3) << 6U | - (uint32_t)(uint8_t)(v.elements[1U] >> 5U); - result[3U] = (uint8_t)(v.elements[2U] >> 2U & (int16_t)255); - result[4U] = (uint32_t)(uint8_t)(v.elements[3U] & (int16_t)127) << 1U | - (uint32_t)(uint8_t)(v.elements[2U] >> 10U); - result[5U] = (uint32_t)(uint8_t)(v.elements[4U] & (int16_t)15) << 4U | - (uint32_t)(uint8_t)(v.elements[3U] >> 7U); - result[6U] = (uint32_t)(uint8_t)(v.elements[5U] & (int16_t)1) << 7U | - (uint32_t)(uint8_t)(v.elements[4U] >> 4U); - result[7U] = (uint8_t)(v.elements[5U] >> 1U & (int16_t)255); - result[8U] = (uint32_t)(uint8_t)(v.elements[6U] & (int16_t)63) << 2U | - (uint32_t)(uint8_t)(v.elements[5U] >> 9U); - result[9U] = (uint32_t)(uint8_t)(v.elements[7U] & (int16_t)7) << 5U | - (uint32_t)(uint8_t)(v.elements[6U] >> 6U); - result[10U] = (uint8_t)(v.elements[7U] >> 3U); - result[11U] = (uint8_t)v.elements[(size_t)8U + (size_t)0U]; - result[12U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)1U] & (int16_t)31) - << 3U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)0U] >> 8U); - result[13U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)2U] & (int16_t)3) - << 6U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)1U] >> 5U); - result[14U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)2U] >> 2U & (int16_t)255); - result[15U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)3U] & (int16_t)127) - << 1U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)2U] >> 10U); - result[16U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)4U] & (int16_t)15) - << 4U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)3U] >> 7U); - result[17U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)5U] & (int16_t)1) - << 7U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)4U] >> 4U); - result[18U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)5U] >> 1U & (int16_t)255); - result[19U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)6U] & (int16_t)63) - << 2U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)5U] >> 9U); - result[20U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)7U] & (int16_t)7) - << 5U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)6U] >> 6U); - result[21U] = (uint8_t)(v.elements[(size_t)8U + (size_t)7U] >> 3U); - memcpy(ret, result, (size_t)22U * sizeof(uint8_t)); -} - KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_11( core_core_arch_x86___m256i vector, uint8_t ret[22U]) { - int16_t array[16U]; - libcrux_ml_kem_vector_avx2_to_i16_array(vector, array); - int16_t uu____0[16U]; - memcpy(uu____0, array, (size_t)16U * sizeof(int16_t)); - libcrux_ml_kem_vector_avx2_portable_PortableVector input = - libcrux_ml_kem_vector_avx2_portable_from_i16_array(uu____0); + int16_t array[16U] = {0U}; + libcrux_intrinsics_avx2_mm256_storeu_si256_i16( + Eurydice_array_to_slice((size_t)16U, array, int16_t, Eurydice_slice), + vector); + libcrux_ml_kem_vector_portable_vector_type_PortableVector input = + libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___from_i16_array( + Eurydice_array_to_slice((size_t)16U, array, int16_t, Eurydice_slice)); uint8_t ret0[22U]; - libcrux_ml_kem_vector_avx2_portable_serialize_11(input, ret0); + libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___serialize_11( + input, ret0); memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t)); } @@ -1217,186 +1175,17 @@ libcrux_ml_kem_vector_avx2___libcrux_ml_kem__vector__traits__Operations_for_libc memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t)); } -KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE libcrux_ml_kem_vector_avx2_portable_PortableVector -libcrux_ml_kem_vector_avx2_portable_zero(void) { - libcrux_ml_kem_vector_avx2_portable_PortableVector lit; - lit.elements[0U] = (int16_t)0; - lit.elements[1U] = (int16_t)0; - lit.elements[2U] = (int16_t)0; - lit.elements[3U] = (int16_t)0; - lit.elements[4U] = (int16_t)0; - lit.elements[5U] = (int16_t)0; - lit.elements[6U] = (int16_t)0; - lit.elements[7U] = (int16_t)0; - lit.elements[8U] = (int16_t)0; - lit.elements[9U] = (int16_t)0; - lit.elements[10U] = (int16_t)0; - lit.elements[11U] = (int16_t)0; - lit.elements[12U] = (int16_t)0; - lit.elements[13U] = (int16_t)0; - lit.elements[14U] = (int16_t)0; - lit.elements[15U] = (int16_t)0; - return lit; -} - -KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE libcrux_ml_kem_vector_avx2_portable_PortableVector -libcrux_ml_kem_vector_avx2_portable_deserialize_11(Eurydice_slice bytes) { - libcrux_ml_kem_vector_avx2_portable_PortableVector result = - libcrux_ml_kem_vector_avx2_portable_zero(); - int16_t uu____0 = ((int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)7) - << 8U; - uint8_t *uu____1 = - &Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); - result.elements[0U] = uu____0 | (int16_t)uu____1[0U]; - int16_t uu____2 = ((int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)63) - << 5U; - uint8_t *uu____3 = - &Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); - result.elements[1U] = uu____2 | (int16_t)uu____3[0U] >> 3U; - int16_t uu____4 = ((int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)1) - << 10U; - int16_t uu____5 = - uu____4 | (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, - uint8_t *, uint8_t) - << 2U; - uint8_t *uu____6 = - &Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t); - result.elements[2U] = uu____5 | (int16_t)uu____6[0U] >> 6U; - int16_t uu____7 = ((int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)15) - << 7U; - uint8_t *uu____8 = - &Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t); - result.elements[3U] = uu____7 | (int16_t)uu____8[0U] >> 1U; - int16_t uu____9 = ((int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)127) - << 4U; - uint8_t *uu____10 = - &Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *, uint8_t); - result.elements[4U] = uu____9 | (int16_t)uu____10[0U] >> 4U; - int16_t uu____11 = ((int16_t)Eurydice_slice_index(bytes, (size_t)8U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)3) - << 9U; - int16_t uu____12 = - uu____11 | (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, - uint8_t *, uint8_t) - << 1U; - uint8_t *uu____13 = - &Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t); - result.elements[5U] = uu____12 | (int16_t)uu____13[0U] >> 7U; - int16_t uu____14 = ((int16_t)Eurydice_slice_index(bytes, (size_t)9U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)31) - << 6U; - uint8_t *uu____15 = - &Eurydice_slice_index(bytes, (size_t)8U, uint8_t, uint8_t *, uint8_t); - result.elements[6U] = uu____14 | (int16_t)uu____15[0U] >> 2U; - int16_t uu____16 = (int16_t)Eurydice_slice_index(bytes, (size_t)10U, uint8_t, - uint8_t *, uint8_t) - << 3U; - uint8_t *uu____17 = - &Eurydice_slice_index(bytes, (size_t)9U, uint8_t, uint8_t *, uint8_t); - result.elements[7U] = uu____16 | (int16_t)uu____17[0U] >> 5U; - int16_t uu____18 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)1U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)7) - << 8U; - uint8_t *uu____19 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)0U, - uint8_t, uint8_t *, uint8_t); - result.elements[8U] = uu____18 | (int16_t)uu____19[0U]; - int16_t uu____20 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)2U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)63) - << 5U; - uint8_t *uu____21 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)1U, - uint8_t, uint8_t *, uint8_t); - result.elements[9U] = uu____20 | (int16_t)uu____21[0U] >> 3U; - int16_t uu____22 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)4U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)1) - << 10U; - int16_t uu____23 = - uu____22 | (int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)3U, - uint8_t, uint8_t *, uint8_t) - << 2U; - uint8_t *uu____24 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)2U, - uint8_t, uint8_t *, uint8_t); - result.elements[10U] = uu____23 | (int16_t)uu____24[0U] >> 6U; - int16_t uu____25 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)5U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)15) - << 7U; - uint8_t *uu____26 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)4U, - uint8_t, uint8_t *, uint8_t); - result.elements[11U] = uu____25 | (int16_t)uu____26[0U] >> 1U; - int16_t uu____27 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)6U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)127) - << 4U; - uint8_t *uu____28 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)5U, - uint8_t, uint8_t *, uint8_t); - result.elements[12U] = uu____27 | (int16_t)uu____28[0U] >> 4U; - int16_t uu____29 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)8U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)3) - << 9U; - int16_t uu____30 = - uu____29 | (int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)7U, - uint8_t, uint8_t *, uint8_t) - << 1U; - uint8_t *uu____31 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)6U, - uint8_t, uint8_t *, uint8_t); - result.elements[13U] = uu____30 | (int16_t)uu____31[0U] >> 7U; - int16_t uu____32 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)9U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)31) - << 6U; - uint8_t *uu____33 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)8U, - uint8_t, uint8_t *, uint8_t); - result.elements[14U] = uu____32 | (int16_t)uu____33[0U] >> 2U; - int16_t uu____34 = - (int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)10U, uint8_t, - uint8_t *, uint8_t) - << 3U; - uint8_t *uu____35 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)9U, - uint8_t, uint8_t *, uint8_t); - result.elements[15U] = uu____34 | (int16_t)uu____35[0U] >> 5U; - return result; -} - -KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_portable_to_i16_array( - libcrux_ml_kem_vector_avx2_portable_PortableVector v, int16_t ret[16U]) { - memcpy(ret, v.elements, (size_t)16U * sizeof(int16_t)); -} - KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE core_core_arch_x86___m256i libcrux_ml_kem_vector_avx2_serialize_deserialize_11(Eurydice_slice bytes) { - libcrux_ml_kem_vector_avx2_portable_PortableVector output = - libcrux_ml_kem_vector_avx2_portable_deserialize_11(bytes); - int16_t ret[16U]; - libcrux_ml_kem_vector_avx2_portable_to_i16_array(output, ret); - return libcrux_ml_kem_vector_avx2_from_i16_array( - Eurydice_array_to_slice((size_t)16U, ret, int16_t, Eurydice_slice)); + libcrux_ml_kem_vector_portable_vector_type_PortableVector output = + libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___deserialize_11( + bytes); + int16_t array[16U]; + libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___to_i16_array( + output, array); + return libcrux_intrinsics_avx2_mm256_loadu_si256_i16( + Eurydice_array_to_slice((size_t)16U, array, int16_t, Eurydice_slice)); } KRML_ATTRIBUTE_TARGET("avx2") @@ -2709,16 +2498,13 @@ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___G___3size_t( Eurydice_slice input, uint8_t ret[64U]) { - uint8_t digest[64U] = {0U}; - libcrux_sha3_portable_sha512( - Eurydice_array_to_slice((size_t)64U, digest, uint8_t, Eurydice_slice), - input); - memcpy(ret, digest, (size_t)64U * sizeof(uint8_t)); + uint8_t ret0[64U]; + libcrux_ml_kem_hash_functions_avx2_G(input, ret0); + memcpy(ret, ret0, (size_t)64U * sizeof(uint8_t)); } KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRF___3size_t_32size_t( +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_avx2_PRF___32size_t( Eurydice_slice input, uint8_t ret[32U]) { uint8_t digest[32U] = {0U}; libcrux_sha3_portable_shake256( @@ -2727,6 +2513,15 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for memcpy(ret, digest, (size_t)32U * sizeof(uint8_t)); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRF___3size_t_32size_t( + Eurydice_slice input, uint8_t ret[32U]) { + uint8_t ret0[32U]; + libcrux_ml_kem_hash_functions_avx2_PRF___32size_t(input, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} + KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_1152size_t_3size_t( @@ -2831,7 +2626,7 @@ typedef libcrux_sha3_avx2_x4_incremental_KeccakState KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE libcrux_sha3_avx2_x4_incremental_KeccakState -libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_init_absorb___3size_t( +libcrux_ml_kem_hash_functions_avx2_shake128_init_absorb___3size_t( uint8_t input[3U][34U]) { libcrux_sha3_generic_keccak_KeccakState__core_core_arch_x86___m256i__4size_t state = libcrux_sha3_avx2_x4_incremental_shake128_init(); @@ -2844,18 +2639,27 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for return state; } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE libcrux_sha3_avx2_x4_incremental_KeccakState +libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_init_absorb___3size_t( + uint8_t input[3U][34U]) { + uint8_t uu____0[3U][34U]; + memcpy(uu____0, input, (size_t)3U * sizeof(uint8_t[34U])); + return libcrux_ml_kem_hash_functions_avx2_shake128_init_absorb___3size_t( + uu____0); +} + KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_squeeze_three_blocks___3size_t( - libcrux_sha3_avx2_x4_incremental_KeccakState *self, uint8_t ret[3U][504U]) { +libcrux_ml_kem_hash_functions_avx2_shake128_squeeze_three_blocks___3size_t( + libcrux_sha3_avx2_x4_incremental_KeccakState *st, uint8_t ret[3U][504U]) { uint8_t out[3U][504U] = {{0U}}; uint8_t out0[504U] = {0U}; uint8_t out1[504U] = {0U}; uint8_t out2[504U] = {0U}; uint8_t out3[504U] = {0U}; libcrux_sha3_avx2_x4_incremental_shake128_squeeze_first_three_blocks( - self, - Eurydice_array_to_slice((size_t)504U, out0, uint8_t, Eurydice_slice), + st, Eurydice_array_to_slice((size_t)504U, out0, uint8_t, Eurydice_slice), Eurydice_array_to_slice((size_t)504U, out1, uint8_t, Eurydice_slice), Eurydice_array_to_slice((size_t)504U, out2, uint8_t, Eurydice_slice), Eurydice_array_to_slice((size_t)504U, out3, uint8_t, Eurydice_slice)); @@ -2871,6 +2675,16 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for memcpy(ret, out, (size_t)3U * sizeof(uint8_t[504U])); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_squeeze_three_blocks___3size_t( + libcrux_sha3_avx2_x4_incremental_KeccakState *self, uint8_t ret[3U][504U]) { + uint8_t ret0[3U][504U]; + libcrux_ml_kem_hash_functions_avx2_shake128_squeeze_three_blocks___3size_t( + self, ret0); + memcpy(ret, ret0, (size_t)3U * sizeof(uint8_t[504U])); +} + KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE bool libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_504size_t( @@ -2918,16 +2732,15 @@ libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_ve KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_squeeze_block___3size_t( - libcrux_sha3_avx2_x4_incremental_KeccakState *self, uint8_t ret[3U][168U]) { +libcrux_ml_kem_hash_functions_avx2_shake128_squeeze_block___3size_t( + libcrux_sha3_avx2_x4_incremental_KeccakState *st, uint8_t ret[3U][168U]) { uint8_t out[3U][168U] = {{0U}}; uint8_t out0[168U] = {0U}; uint8_t out1[168U] = {0U}; uint8_t out2[168U] = {0U}; uint8_t out3[168U] = {0U}; libcrux_sha3_avx2_x4_incremental_shake128_squeeze_next_block( - self, - Eurydice_array_to_slice((size_t)168U, out0, uint8_t, Eurydice_slice), + st, Eurydice_array_to_slice((size_t)168U, out0, uint8_t, Eurydice_slice), Eurydice_array_to_slice((size_t)168U, out1, uint8_t, Eurydice_slice), Eurydice_array_to_slice((size_t)168U, out2, uint8_t, Eurydice_slice), Eurydice_array_to_slice((size_t)168U, out3, uint8_t, Eurydice_slice)); @@ -2943,6 +2756,16 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for memcpy(ret, out, (size_t)3U * sizeof(uint8_t[168U])); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___shake128_squeeze_block___3size_t( + libcrux_sha3_avx2_x4_incremental_KeccakState *self, uint8_t ret[3U][168U]) { + uint8_t ret0[3U][168U]; + libcrux_ml_kem_hash_functions_avx2_shake128_squeeze_block___3size_t(self, + ret0); + memcpy(ret, ret0, (size_t)3U * sizeof(uint8_t[168U])); +} + KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE bool libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t_168size_t( @@ -3160,7 +2983,7 @@ libcrux_ml_kem_ind_cpa_sample_vector_cbd_then_ntt_closure__libcrux_ml_kem_vector KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRFxN___3size_t_128size_t( +libcrux_ml_kem_hash_functions_avx2_PRFxN___3size_t_128size_t( uint8_t (*input)[33U], uint8_t ret[3U][128U]) { uint8_t out[3U][128U] = {{0U}}; uint8_t out0[128U] = {0U}; @@ -3188,6 +3011,15 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for memcpy(ret, out, (size_t)3U * sizeof(uint8_t[128U])); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRFxN___3size_t_128size_t( + uint8_t (*input)[33U], uint8_t ret[3U][128U]) { + uint8_t ret0[3U][128U]; + libcrux_ml_kem_hash_functions_avx2_PRFxN___3size_t_128size_t(input, ret0); + memcpy(ret, ret0, (size_t)3U * sizeof(uint8_t[128U])); +} + KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector @@ -3459,8 +3291,7 @@ static KRML_MUSTINLINE } KRML_ATTRIBUTE_TARGET("avx2") -static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRF___3size_t_128size_t( +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_avx2_PRF___128size_t( Eurydice_slice input, uint8_t ret[128U]) { uint8_t digest[128U] = {0U}; libcrux_sha3_portable_shake256( @@ -3469,6 +3300,15 @@ libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for memcpy(ret, digest, (size_t)128U * sizeof(uint8_t)); } +KRML_ATTRIBUTE_TARGET("avx2") +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___PRF___3size_t_128size_t( + Eurydice_slice input, uint8_t ret[128U]) { + uint8_t ret0[128U]; + libcrux_ml_kem_hash_functions_avx2_PRF___128size_t(input, ret0); + memcpy(ret, ret0, (size_t)128U * sizeof(uint8_t)); +} + KRML_ATTRIBUTE_TARGET("avx2") static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_avx2_SIMD256Vector libcrux_ml_kem_matrix_compute_vector_u_closure__libcrux_ml_kem_vector_avx2_SIMD256Vector_3size_t( @@ -4511,11 +4351,9 @@ KRML_ATTRIBUTE_TARGET("avx2") static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_avx2___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__avx2__Simd256Hash___H___3size_t( Eurydice_slice input, uint8_t ret[32U]) { - uint8_t digest[32U] = {0U}; - libcrux_sha3_portable_sha256( - Eurydice_array_to_slice((size_t)32U, digest, uint8_t, Eurydice_slice), - input); - memcpy(ret, digest, (size_t)32U * sizeof(uint8_t)); + uint8_t ret0[32U]; + libcrux_ml_kem_hash_functions_avx2_H(input, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } KRML_ATTRIBUTE_TARGET("avx2") @@ -5403,13 +5241,6 @@ libcrux_ml_kem_mlkem768_avx2_validate_public_key( return uu____0; } -KRML_ATTRIBUTE_TARGET("avx2") -static inline libcrux_ml_kem_vector_avx2_portable_PortableVector -libcrux_ml_kem_vector_avx2_portable___core__clone__Clone_for_libcrux_ml_kem__vector__avx2__portable__PortableVector___clone( - libcrux_ml_kem_vector_avx2_portable_PortableVector *self) { - return self[0U]; -} - KRML_ATTRIBUTE_TARGET("avx2") static inline core_core_arch_x86___m256i libcrux_ml_kem_vector_avx2___core__clone__Clone_for_libcrux_ml_kem__vector__avx2__SIMD256Vector__1__clone( @@ -5417,8 +5248,6 @@ libcrux_ml_kem_vector_avx2___core__clone__Clone_for_libcrux_ml_kem__vector__avx2 return self[0U]; } -typedef int16_t libcrux_ml_kem_vector_avx2_portable_FieldElement; - #if defined(__cplusplus) } #endif diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h index 9bfb0ef0f..42f208793 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h @@ -2,7 +2,7 @@ This file was generated by KaRaMeL KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../cg.yaml -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: - 07b5a210 KaRaMeL version: f13006e2 + 07b5a210 KaRaMeL version: 65aab550 */ #ifndef __libcrux_mlkem768_portable_H @@ -22,10 +22,46 @@ extern "C" { #define LIBCRUX_ML_KEM_HASH_FUNCTIONS_THREE_BLOCKS \ (LIBCRUX_ML_KEM_HASH_FUNCTIONS_BLOCK_SIZE * (size_t)3U) +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_neon_G( + Eurydice_slice input, uint8_t ret[64U]) { + uint8_t digest[64U] = {0U}; + libcrux_sha3_neon_sha512( + Eurydice_array_to_slice((size_t)64U, digest, uint8_t, Eurydice_slice), + input); + memcpy(ret, digest, (size_t)64U * sizeof(uint8_t)); +} + +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_neon_H( + Eurydice_slice input, uint8_t ret[32U]) { + uint8_t digest[32U] = {0U}; + libcrux_sha3_neon_sha256( + Eurydice_array_to_slice((size_t)32U, digest, uint8_t, Eurydice_slice), + input); + memcpy(ret, digest, (size_t)32U * sizeof(uint8_t)); +} + typedef struct libcrux_ml_kem_hash_functions_neon_Simd128Hash_s { libcrux_sha3_neon_x2_incremental_KeccakState shake128_state[2U]; } libcrux_ml_kem_hash_functions_neon_Simd128Hash; +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_portable_G( + Eurydice_slice input, uint8_t ret[64U]) { + uint8_t digest[64U] = {0U}; + libcrux_sha3_portable_sha512( + Eurydice_array_to_slice((size_t)64U, digest, uint8_t, Eurydice_slice), + input); + memcpy(ret, digest, (size_t)64U * sizeof(uint8_t)); +} + +static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_portable_H( + Eurydice_slice input, uint8_t ret[32U]) { + uint8_t digest[32U] = {0U}; + libcrux_sha3_portable_sha256( + Eurydice_array_to_slice((size_t)32U, digest, uint8_t, Eurydice_slice), + input); + memcpy(ret, digest, (size_t)32U * sizeof(uint8_t)); +} + #define LIBCRUX_ML_KEM_IND_CCA_ENCAPS_SEED_SIZE \ (LIBCRUX_ML_KEM_CONSTANTS_SHARED_SECRET_SIZE) @@ -83,6 +119,370 @@ static const int16_t libcrux_ml_kem_polynomial_ZETAS_TIMES_MONTGOMERY_R[128U] = #define LIBCRUX_ML_KEM_VECTOR_TRAITS_INVERSE_OF_MODULUS_MOD_MONTGOMERY_R \ (62209U) +typedef struct libcrux_ml_kem_vector_portable_vector_type_PortableVector_s { + int16_t elements[16U]; +} libcrux_ml_kem_vector_portable_vector_type_PortableVector; + +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_vector_type_from_i16_array( + Eurydice_slice array) { + libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; + int16_t ret[16U]; + core_result_Result__int16_t_16size_t__core_array_TryFromSliceError dst; + Eurydice_slice_to_array2( + &dst, + Eurydice_slice_subslice(array, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = (size_t)16U}), + int16_t, core_ops_range_Range__size_t, + Eurydice_slice), + Eurydice_slice, int16_t[16U], void *); + core_result__core__result__Result_T__E___unwrap__int16_t_16size_t__core_array_TryFromSliceError( + dst, ret); + memcpy(lit.elements, ret, (size_t)16U * sizeof(int16_t)); + return lit; +} + +static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___from_i16_array( + Eurydice_slice array) { + return libcrux_ml_kem_vector_portable_vector_type_from_i16_array(array); +} + +typedef struct + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_s { + uint8_t fst; + uint8_t snd; + uint8_t thd; + uint8_t f3; + uint8_t f4; + uint8_t f5; + uint8_t f6; + uint8_t f7; + uint8_t f8; + uint8_t f9; + uint8_t f10; +} K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t; + +static KRML_MUSTINLINE + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t + libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_slice v) { + uint8_t r0 = + (uint8_t)Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *, int16_t); + uint8_t uu____0 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *, int16_t) & + (int16_t)31) + << 3U; + uint8_t r1 = (uint32_t)uu____0 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, + int16_t *, int16_t) >> + 8U); + uint8_t uu____1 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *, int16_t) & + (int16_t)3) + << 6U; + uint8_t r2 = (uint32_t)uu____1 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *, int16_t) >> + 5U); + uint8_t r3 = (uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *, + int16_t) >> + 2U & + (int16_t)255); + uint8_t uu____2 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, + int16_t *, int16_t) & + (int16_t)127) + << 1U; + uint8_t r4 = (uint32_t)uu____2 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *, int16_t) >> + 10U); + uint8_t uu____3 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, + int16_t *, int16_t) & + (int16_t)15) + << 4U; + uint8_t r5 = (uint32_t)uu____3 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, + int16_t *, int16_t) >> + 7U); + uint8_t uu____4 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, + int16_t *, int16_t) & + (int16_t)1) + << 7U; + uint8_t r6 = (uint32_t)uu____4 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)4U, int16_t, + int16_t *, int16_t) >> + 4U); + uint8_t r7 = (uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *, + int16_t) >> + 1U & + (int16_t)255); + uint8_t uu____5 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, + int16_t *, int16_t) & + (int16_t)63) + << 2U; + uint8_t r8 = (uint32_t)uu____5 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)5U, int16_t, + int16_t *, int16_t) >> + 9U); + uint8_t uu____6 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, + int16_t *, int16_t) & + (int16_t)7) + << 5U; + uint8_t r9 = (uint32_t)uu____6 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)6U, int16_t, + int16_t *, int16_t) >> + 6U); + uint8_t r10 = (uint8_t)(Eurydice_slice_index(v, (size_t)7U, int16_t, + int16_t *, int16_t) >> + 3U); + return (CLITERAL( + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t){ + .fst = r0, + .snd = r1, + .thd = r2, + .f3 = r3, + .f4 = r4, + .f5 = r5, + .f6 = r6, + .f7 = r7, + .f8 = r8, + .f9 = r9, + .f10 = r10}); +} + +static KRML_MUSTINLINE void +libcrux_ml_kem_vector_portable_serialize_serialize_11( + libcrux_ml_kem_vector_portable_vector_type_PortableVector v, + uint8_t ret[22U]) { + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t + r0_10 = libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)0U, + .end = (size_t)8U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t + r11_21 = libcrux_ml_kem_vector_portable_serialize_serialize_11_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)8U, + .end = (size_t)16U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + uint8_t result[22U] = {0U}; + result[0U] = r0_10.fst; + result[1U] = r0_10.snd; + result[2U] = r0_10.thd; + result[3U] = r0_10.f3; + result[4U] = r0_10.f4; + result[5U] = r0_10.f5; + result[6U] = r0_10.f6; + result[7U] = r0_10.f7; + result[8U] = r0_10.f8; + result[9U] = r0_10.f9; + result[10U] = r0_10.f10; + result[11U] = r11_21.fst; + result[12U] = r11_21.snd; + result[13U] = r11_21.thd; + result[14U] = r11_21.f3; + result[15U] = r11_21.f4; + result[16U] = r11_21.f5; + result[17U] = r11_21.f6; + result[18U] = r11_21.f7; + result[19U] = r11_21.f8; + result[20U] = r11_21.f9; + result[21U] = r11_21.f10; + memcpy(ret, result, (size_t)22U * sizeof(uint8_t)); +} + +static inline void +libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___serialize_11( + libcrux_ml_kem_vector_portable_vector_type_PortableVector a, + uint8_t ret[22U]) { + uint8_t ret0[22U]; + libcrux_ml_kem_vector_portable_serialize_serialize_11(a, ret0); + memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t)); +} + +typedef struct + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_s { + int16_t fst; + int16_t snd; + int16_t thd; + int16_t f3; + int16_t f4; + int16_t f5; + int16_t f6; + int16_t f7; +} K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t; + +static KRML_MUSTINLINE + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t + libcrux_ml_kem_vector_portable_serialize_deserialize_11_int( + Eurydice_slice bytes) { + int16_t uu____0 = ((int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, + uint8_t *, uint8_t) & + (int16_t)7) + << 8U; + int16_t r0 = uu____0 | (int16_t)Eurydice_slice_index( + bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); + int16_t uu____1 = ((int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, + uint8_t *, uint8_t) & + (int16_t)63) + << 5U; + int16_t r1 = uu____1 | (int16_t)Eurydice_slice_index( + bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t) >> + 3U; + int16_t uu____2 = ((int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, + uint8_t *, uint8_t) & + (int16_t)1) + << 10U; + int16_t uu____3 = + uu____2 | (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, + uint8_t *, uint8_t) + << 2U; + int16_t r2 = uu____3 | (int16_t)Eurydice_slice_index( + bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t) >> + 6U; + int16_t uu____4 = ((int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, + uint8_t *, uint8_t) & + (int16_t)15) + << 7U; + int16_t r3 = uu____4 | (int16_t)Eurydice_slice_index( + bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t) >> + 1U; + int16_t uu____5 = ((int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, + uint8_t *, uint8_t) & + (int16_t)127) + << 4U; + int16_t r4 = uu____5 | (int16_t)Eurydice_slice_index( + bytes, (size_t)5U, uint8_t, uint8_t *, uint8_t) >> + 4U; + int16_t uu____6 = ((int16_t)Eurydice_slice_index(bytes, (size_t)8U, uint8_t, + uint8_t *, uint8_t) & + (int16_t)3) + << 9U; + int16_t uu____7 = + uu____6 | (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, + uint8_t *, uint8_t) + << 1U; + int16_t r5 = uu____7 | (int16_t)Eurydice_slice_index( + bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t) >> + 7U; + int16_t uu____8 = ((int16_t)Eurydice_slice_index(bytes, (size_t)9U, uint8_t, + uint8_t *, uint8_t) & + (int16_t)31) + << 6U; + int16_t r6 = uu____8 | (int16_t)Eurydice_slice_index( + bytes, (size_t)8U, uint8_t, uint8_t *, uint8_t) >> + 2U; + int16_t uu____9 = (int16_t)Eurydice_slice_index(bytes, (size_t)10U, uint8_t, + uint8_t *, uint8_t) + << 3U; + int16_t r7 = uu____9 | (int16_t)Eurydice_slice_index( + bytes, (size_t)9U, uint8_t, uint8_t *, uint8_t) >> + 5U; + return (CLITERAL( + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t){ + .fst = r0, + .snd = r1, + .thd = r2, + .f3 = r3, + .f4 = r4, + .f5 = r5, + .f6 = r6, + .f7 = r7}); +} + +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_vector_type_zero(void) { + libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; + lit.elements[0U] = (int16_t)0; + lit.elements[1U] = (int16_t)0; + lit.elements[2U] = (int16_t)0; + lit.elements[3U] = (int16_t)0; + lit.elements[4U] = (int16_t)0; + lit.elements[5U] = (int16_t)0; + lit.elements[6U] = (int16_t)0; + lit.elements[7U] = (int16_t)0; + lit.elements[8U] = (int16_t)0; + lit.elements[9U] = (int16_t)0; + lit.elements[10U] = (int16_t)0; + lit.elements[11U] = (int16_t)0; + lit.elements[12U] = (int16_t)0; + lit.elements[13U] = (int16_t)0; + lit.elements[14U] = (int16_t)0; + lit.elements[15U] = (int16_t)0; + return lit; +} + +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_serialize_deserialize_11(Eurydice_slice bytes) { + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v0_7 = + libcrux_ml_kem_vector_portable_serialize_deserialize_11_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = (size_t)11U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v8_15 = + libcrux_ml_kem_vector_portable_serialize_deserialize_11_int( + Eurydice_slice_subslice( + bytes, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)11U, + .end = (size_t)22U}), + uint8_t, core_ops_range_Range__size_t, Eurydice_slice)); + libcrux_ml_kem_vector_portable_vector_type_PortableVector v = + libcrux_ml_kem_vector_portable_vector_type_zero(); + v.elements[0U] = v0_7.fst; + v.elements[1U] = v0_7.snd; + v.elements[2U] = v0_7.thd; + v.elements[3U] = v0_7.f3; + v.elements[4U] = v0_7.f4; + v.elements[5U] = v0_7.f5; + v.elements[6U] = v0_7.f6; + v.elements[7U] = v0_7.f7; + v.elements[8U] = v8_15.fst; + v.elements[9U] = v8_15.snd; + v.elements[10U] = v8_15.thd; + v.elements[11U] = v8_15.f3; + v.elements[12U] = v8_15.f4; + v.elements[13U] = v8_15.f5; + v.elements[14U] = v8_15.f6; + v.elements[15U] = v8_15.f7; + return v; +} + +static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___deserialize_11( + Eurydice_slice a) { + return libcrux_ml_kem_vector_portable_serialize_deserialize_11(a); +} + +static KRML_MUSTINLINE void +libcrux_ml_kem_vector_portable_vector_type_to_i16_array( + libcrux_ml_kem_vector_portable_vector_type_PortableVector x, + int16_t ret[16U]) { + memcpy(ret, x.elements, (size_t)16U * sizeof(int16_t)); +} + +static inline void +libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___to_i16_array( + libcrux_ml_kem_vector_portable_vector_type_PortableVector x, + int16_t ret[16U]) { + int16_t ret0[16U]; + libcrux_ml_kem_vector_portable_vector_type_to_i16_array(x, ret0); + memcpy(ret, ret0, (size_t)16U * sizeof(int16_t)); +} + static const uint8_t libcrux_ml_kem_vector_rej_sample_table_REJECTION_SAMPLE_SHUFFLE_TABLE [256U][16U] = {{255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, @@ -598,64 +998,12 @@ static const uint8_t {0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U}}; -typedef struct libcrux_ml_kem_vector_portable_vector_type_PortableVector_s { - int16_t elements[16U]; -} libcrux_ml_kem_vector_portable_vector_type_PortableVector; - -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_vector_type_zero(void) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; - lit.elements[0U] = (int16_t)0; - lit.elements[1U] = (int16_t)0; - lit.elements[2U] = (int16_t)0; - lit.elements[3U] = (int16_t)0; - lit.elements[4U] = (int16_t)0; - lit.elements[5U] = (int16_t)0; - lit.elements[6U] = (int16_t)0; - lit.elements[7U] = (int16_t)0; - lit.elements[8U] = (int16_t)0; - lit.elements[9U] = (int16_t)0; - lit.elements[10U] = (int16_t)0; - lit.elements[11U] = (int16_t)0; - lit.elements[12U] = (int16_t)0; - lit.elements[13U] = (int16_t)0; - lit.elements[14U] = (int16_t)0; - lit.elements[15U] = (int16_t)0; - return lit; -} - static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___ZERO( void) { return libcrux_ml_kem_vector_portable_vector_type_zero(); } -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_vector_type_from_i16_array( - Eurydice_slice array) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector lit; - int16_t ret[16U]; - core_result_Result__int16_t_16size_t__core_array_TryFromSliceError dst; - Eurydice_slice_to_array2( - &dst, - Eurydice_slice_subslice(array, - (CLITERAL(core_ops_range_Range__size_t){ - .start = (size_t)0U, .end = (size_t)16U}), - int16_t, core_ops_range_Range__size_t, - Eurydice_slice), - Eurydice_slice, int16_t[16U], void *); - core_result__core__result__Result_T__E___unwrap__int16_t_16size_t__core_array_TryFromSliceError( - dst, ret); - memcpy(lit.elements, ret, (size_t)16U * sizeof(int16_t)); - return lit; -} - -static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___from_i16_array( - Eurydice_slice array) { - return libcrux_ml_kem_vector_portable_vector_type_from_i16_array(array); -} - static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_arithmetic_add( libcrux_ml_kem_vector_portable_vector_type_PortableVector lhs, @@ -907,58 +1255,36 @@ libcrux_ml_kem_vector_portable_compress_compress_ciphertext_coefficient( coefficient_bits, (uint32_t)compressed); } +static KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_ntt_ntt_step( + libcrux_ml_kem_vector_portable_vector_type_PortableVector *v, int16_t zeta, + size_t i, size_t j) { + int16_t t = + libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( + v->elements[j], zeta); + v->elements[j] = v->elements[i] - t; + v->elements[i] = v->elements[i] + t; +} + static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_ntt_ntt_layer_1_step( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, int16_t zeta1, int16_t zeta2, int16_t zeta3) { - int16_t t = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[2U], zeta0); - v.elements[2U] = v.elements[0U] - t; - v.elements[0U] = v.elements[0U] + t; - int16_t t0 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[3U], zeta0); - v.elements[3U] = v.elements[1U] - t0; - v.elements[1U] = v.elements[1U] + t0; - int16_t t1 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[6U], zeta1); - v.elements[6U] = v.elements[4U] - t1; - v.elements[4U] = v.elements[4U] + t1; - int16_t t2 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[7U], zeta1); - v.elements[7U] = v.elements[5U] - t2; - v.elements[5U] = v.elements[5U] + t2; - int16_t t3 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)2U], zeta2); - v.elements[(size_t)8U + (size_t)2U] = - v.elements[(size_t)8U + (size_t)0U] - t3; - v.elements[(size_t)8U + (size_t)0U] = - v.elements[(size_t)8U + (size_t)0U] + t3; - int16_t t4 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)3U], zeta2); - v.elements[(size_t)8U + (size_t)3U] = - v.elements[(size_t)8U + (size_t)1U] - t4; - v.elements[(size_t)8U + (size_t)1U] = - v.elements[(size_t)8U + (size_t)1U] + t4; - int16_t t5 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)6U], zeta3); - v.elements[(size_t)8U + (size_t)6U] = - v.elements[(size_t)8U + (size_t)4U] - t5; - v.elements[(size_t)8U + (size_t)4U] = - v.elements[(size_t)8U + (size_t)4U] + t5; - int16_t t6 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)7U], zeta3); - v.elements[(size_t)8U + (size_t)7U] = - v.elements[(size_t)8U + (size_t)5U] - t6; - v.elements[(size_t)8U + (size_t)5U] = - v.elements[(size_t)8U + (size_t)5U] + t6; + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)0U, + (size_t)2U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)1U, + (size_t)3U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)4U, + (size_t)6U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)5U, + (size_t)7U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta2, (size_t)8U, + (size_t)10U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta2, (size_t)9U, + (size_t)11U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta3, (size_t)12U, + (size_t)14U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta3, (size_t)13U, + (size_t)15U); return v; } @@ -974,54 +1300,22 @@ static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_ntt_ntt_layer_2_step( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, int16_t zeta1) { - int16_t t = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[4U], zeta0); - v.elements[4U] = v.elements[0U] - t; - v.elements[0U] = v.elements[0U] + t; - int16_t t0 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[5U], zeta0); - v.elements[5U] = v.elements[1U] - t0; - v.elements[1U] = v.elements[1U] + t0; - int16_t t1 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[6U], zeta0); - v.elements[6U] = v.elements[2U] - t1; - v.elements[2U] = v.elements[2U] + t1; - int16_t t2 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[7U], zeta0); - v.elements[7U] = v.elements[3U] - t2; - v.elements[3U] = v.elements[3U] + t2; - int16_t t3 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)4U], zeta1); - v.elements[(size_t)8U + (size_t)4U] = - v.elements[(size_t)8U + (size_t)0U] - t3; - v.elements[(size_t)8U + (size_t)0U] = - v.elements[(size_t)8U + (size_t)0U] + t3; - int16_t t4 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)5U], zeta1); - v.elements[(size_t)8U + (size_t)5U] = - v.elements[(size_t)8U + (size_t)1U] - t4; - v.elements[(size_t)8U + (size_t)1U] = - v.elements[(size_t)8U + (size_t)1U] + t4; - int16_t t5 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)6U], zeta1); - v.elements[(size_t)8U + (size_t)6U] = - v.elements[(size_t)8U + (size_t)2U] - t5; - v.elements[(size_t)8U + (size_t)2U] = - v.elements[(size_t)8U + (size_t)2U] + t5; - int16_t t6 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[(size_t)8U + (size_t)7U], zeta1); - v.elements[(size_t)8U + (size_t)7U] = - v.elements[(size_t)8U + (size_t)3U] - t6; - v.elements[(size_t)8U + (size_t)3U] = - v.elements[(size_t)8U + (size_t)3U] + t6; + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)0U, + (size_t)4U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)1U, + (size_t)5U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)2U, + (size_t)6U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta0, (size_t)3U, + (size_t)7U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)8U, + (size_t)12U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)9U, + (size_t)13U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)10U, + (size_t)14U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta1, (size_t)11U, + (size_t)15U); return v; } @@ -1035,46 +1329,20 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta) { - int16_t t = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[8U], zeta); - v.elements[8U] = v.elements[0U] - t; - v.elements[0U] = v.elements[0U] + t; - int16_t t0 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[9U], zeta); - v.elements[9U] = v.elements[1U] - t0; - v.elements[1U] = v.elements[1U] + t0; - int16_t t1 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[10U], zeta); - v.elements[10U] = v.elements[2U] - t1; - v.elements[2U] = v.elements[2U] + t1; - int16_t t2 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[11U], zeta); - v.elements[11U] = v.elements[3U] - t2; - v.elements[3U] = v.elements[3U] + t2; - int16_t t3 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[12U], zeta); - v.elements[12U] = v.elements[4U] - t3; - v.elements[4U] = v.elements[4U] + t3; - int16_t t4 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[13U], zeta); - v.elements[13U] = v.elements[5U] - t4; - v.elements[5U] = v.elements[5U] + t4; - int16_t t5 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[14U], zeta); - v.elements[14U] = v.elements[6U] - t5; - v.elements[6U] = v.elements[6U] + t5; - int16_t t6 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - v.elements[15U], zeta); - v.elements[15U] = v.elements[7U] - t6; - v.elements[7U] = v.elements[7U] + t6; + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)0U, (size_t)8U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)1U, (size_t)9U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)2U, + (size_t)10U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)3U, + (size_t)11U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)4U, + (size_t)12U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)5U, + (size_t)13U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)6U, + (size_t)14U); + libcrux_ml_kem_vector_portable_ntt_ntt_step(&v, zeta, (size_t)7U, + (size_t)15U); return v; } @@ -1084,161 +1352,71 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ return libcrux_ml_kem_vector_portable_ntt_ntt_layer_3_step(a, zeta); } -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step( - libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, - int16_t zeta1, int16_t zeta2, int16_t zeta3) { - int16_t a_minus_b = v.elements[2U] - v.elements[0U]; +static KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_ntt_inv_ntt_step( + libcrux_ml_kem_vector_portable_vector_type_PortableVector *v, int16_t zeta, + size_t i, size_t j) { + int16_t a_minus_b = v->elements[j] - v->elements[i]; int16_t uu____0 = libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[0U] + v.elements[2U]); - v.elements[0U] = uu____0; + v->elements[i] + v->elements[j]); + v->elements[i] = uu____0; int16_t uu____1 = libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b, zeta0); - v.elements[2U] = uu____1; - int16_t a_minus_b0 = v.elements[3U] - v.elements[1U]; - int16_t uu____2 = - libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[1U] + v.elements[3U]); - v.elements[1U] = uu____2; - int16_t uu____3 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b0, zeta0); - v.elements[3U] = uu____3; - int16_t a_minus_b1 = v.elements[6U] - v.elements[4U]; - int16_t uu____4 = - libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[4U] + v.elements[6U]); - v.elements[4U] = uu____4; - int16_t uu____5 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b1, zeta1); - v.elements[6U] = uu____5; - int16_t a_minus_b2 = v.elements[7U] - v.elements[5U]; - int16_t uu____6 = - libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[5U] + v.elements[7U]); - v.elements[5U] = uu____6; - int16_t uu____7 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b2, zeta1); - v.elements[7U] = uu____7; - int16_t a_minus_b3 = - v.elements[(size_t)8U + (size_t)2U] - v.elements[(size_t)8U + (size_t)0U]; - int16_t uu____8 = - libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[(size_t)8U + (size_t)0U] + - v.elements[(size_t)8U + (size_t)2U]); - v.elements[(size_t)8U + (size_t)0U] = uu____8; - int16_t uu____9 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b3, zeta2); - v.elements[(size_t)8U + (size_t)2U] = uu____9; - int16_t a_minus_b4 = - v.elements[(size_t)8U + (size_t)3U] - v.elements[(size_t)8U + (size_t)1U]; - int16_t uu____10 = - libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[(size_t)8U + (size_t)1U] + - v.elements[(size_t)8U + (size_t)3U]); - v.elements[(size_t)8U + (size_t)1U] = uu____10; - int16_t uu____11 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b4, zeta2); - v.elements[(size_t)8U + (size_t)3U] = uu____11; - int16_t a_minus_b5 = - v.elements[(size_t)8U + (size_t)6U] - v.elements[(size_t)8U + (size_t)4U]; - int16_t uu____12 = - libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[(size_t)8U + (size_t)4U] + - v.elements[(size_t)8U + (size_t)6U]); - v.elements[(size_t)8U + (size_t)4U] = uu____12; - int16_t uu____13 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b5, zeta3); - v.elements[(size_t)8U + (size_t)6U] = uu____13; - int16_t a_minus_b6 = - v.elements[(size_t)8U + (size_t)7U] - v.elements[(size_t)8U + (size_t)5U]; - int16_t uu____14 = - libcrux_ml_kem_vector_portable_arithmetic_barrett_reduce_element( - v.elements[(size_t)8U + (size_t)5U] + - v.elements[(size_t)8U + (size_t)7U]); - v.elements[(size_t)8U + (size_t)5U] = uu____14; - int16_t uu____15 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b6, zeta3); - v.elements[(size_t)8U + (size_t)7U] = uu____15; - return v; -} - -static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___inv_ntt_layer_1_step( - libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta0, - int16_t zeta1, int16_t zeta2, int16_t zeta3) { - return libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step( - a, zeta0, zeta1, zeta2, zeta3); + a_minus_b, zeta); + v->elements[j] = uu____1; } static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step( +libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, - int16_t zeta1) { - int16_t a_minus_b = v.elements[4U] - v.elements[0U]; - v.elements[0U] = v.elements[0U] + v.elements[4U]; - int16_t uu____0 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b, zeta0); - v.elements[4U] = uu____0; - int16_t a_minus_b0 = v.elements[5U] - v.elements[1U]; - v.elements[1U] = v.elements[1U] + v.elements[5U]; - int16_t uu____1 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b0, zeta0); - v.elements[5U] = uu____1; - int16_t a_minus_b1 = v.elements[6U] - v.elements[2U]; - v.elements[2U] = v.elements[2U] + v.elements[6U]; - int16_t uu____2 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b1, zeta0); - v.elements[6U] = uu____2; - int16_t a_minus_b2 = v.elements[7U] - v.elements[3U]; - v.elements[3U] = v.elements[3U] + v.elements[7U]; - int16_t uu____3 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b2, zeta0); - v.elements[7U] = uu____3; - int16_t a_minus_b3 = - v.elements[(size_t)8U + (size_t)4U] - v.elements[(size_t)8U + (size_t)0U]; - v.elements[(size_t)8U + (size_t)0U] = - v.elements[(size_t)8U + (size_t)0U] + v.elements[(size_t)8U + (size_t)4U]; - int16_t uu____4 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b3, zeta1); - v.elements[(size_t)8U + (size_t)4U] = uu____4; - int16_t a_minus_b4 = - v.elements[(size_t)8U + (size_t)5U] - v.elements[(size_t)8U + (size_t)1U]; - v.elements[(size_t)8U + (size_t)1U] = - v.elements[(size_t)8U + (size_t)1U] + v.elements[(size_t)8U + (size_t)5U]; - int16_t uu____5 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b4, zeta1); - v.elements[(size_t)8U + (size_t)5U] = uu____5; - int16_t a_minus_b5 = - v.elements[(size_t)8U + (size_t)6U] - v.elements[(size_t)8U + (size_t)2U]; - v.elements[(size_t)8U + (size_t)2U] = - v.elements[(size_t)8U + (size_t)2U] + v.elements[(size_t)8U + (size_t)6U]; - int16_t uu____6 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b5, zeta1); - v.elements[(size_t)8U + (size_t)6U] = uu____6; - int16_t a_minus_b6 = - v.elements[(size_t)8U + (size_t)7U] - v.elements[(size_t)8U + (size_t)3U]; - v.elements[(size_t)8U + (size_t)3U] = - v.elements[(size_t)8U + (size_t)3U] + v.elements[(size_t)8U + (size_t)7U]; - int16_t uu____7 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b6, zeta1); - v.elements[(size_t)8U + (size_t)7U] = uu____7; + int16_t zeta1, int16_t zeta2, int16_t zeta3) { + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)0U, + (size_t)2U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)1U, + (size_t)3U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)4U, + (size_t)6U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)5U, + (size_t)7U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta2, (size_t)8U, + (size_t)10U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta2, (size_t)9U, + (size_t)11U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta3, (size_t)12U, + (size_t)14U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta3, (size_t)13U, + (size_t)15U); + return v; +} + +static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___inv_ntt_layer_1_step( + libcrux_ml_kem_vector_portable_vector_type_PortableVector a, int16_t zeta0, + int16_t zeta1, int16_t zeta2, int16_t zeta3) { + return libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_1_step( + a, zeta0, zeta1, zeta2, zeta3); +} + +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_2_step( + libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta0, + int16_t zeta1) { + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)0U, + (size_t)4U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)1U, + (size_t)5U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)2U, + (size_t)6U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta0, (size_t)3U, + (size_t)7U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)8U, + (size_t)12U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)9U, + (size_t)13U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)10U, + (size_t)14U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta1, (size_t)11U, + (size_t)15U); return v; } @@ -1253,54 +1431,22 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, int16_t zeta) { - int16_t a_minus_b = v.elements[8U] - v.elements[0U]; - v.elements[0U] = v.elements[0U] + v.elements[8U]; - int16_t uu____0 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b, zeta); - v.elements[8U] = uu____0; - int16_t a_minus_b0 = v.elements[9U] - v.elements[1U]; - v.elements[1U] = v.elements[1U] + v.elements[9U]; - int16_t uu____1 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b0, zeta); - v.elements[9U] = uu____1; - int16_t a_minus_b1 = v.elements[10U] - v.elements[2U]; - v.elements[2U] = v.elements[2U] + v.elements[10U]; - int16_t uu____2 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b1, zeta); - v.elements[10U] = uu____2; - int16_t a_minus_b2 = v.elements[11U] - v.elements[3U]; - v.elements[3U] = v.elements[3U] + v.elements[11U]; - int16_t uu____3 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b2, zeta); - v.elements[11U] = uu____3; - int16_t a_minus_b3 = v.elements[12U] - v.elements[4U]; - v.elements[4U] = v.elements[4U] + v.elements[12U]; - int16_t uu____4 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b3, zeta); - v.elements[12U] = uu____4; - int16_t a_minus_b4 = v.elements[13U] - v.elements[5U]; - v.elements[5U] = v.elements[5U] + v.elements[13U]; - int16_t uu____5 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b4, zeta); - v.elements[13U] = uu____5; - int16_t a_minus_b5 = v.elements[14U] - v.elements[6U]; - v.elements[6U] = v.elements[6U] + v.elements[14U]; - int16_t uu____6 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b5, zeta); - v.elements[14U] = uu____6; - int16_t a_minus_b6 = v.elements[15U] - v.elements[7U]; - v.elements[7U] = v.elements[7U] + v.elements[15U]; - int16_t uu____7 = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_multiply_fe_by_fer( - a_minus_b6, zeta); - v.elements[15U] = uu____7; + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)0U, + (size_t)8U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)1U, + (size_t)9U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)2U, + (size_t)10U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)3U, + (size_t)11U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)4U, + (size_t)12U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)5U, + (size_t)13U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)6U, + (size_t)14U); + libcrux_ml_kem_vector_portable_ntt_inv_ntt_step(&v, zeta, (size_t)7U, + (size_t)15U); return v; } @@ -1310,31 +1456,25 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ return libcrux_ml_kem_vector_portable_ntt_inv_ntt_layer_3_step(a, zeta); } -typedef struct K___int16_t_int16_t_s { - int16_t fst; - int16_t snd; -} K___int16_t_int16_t; - -static KRML_MUSTINLINE K___int16_t_int16_t +static KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( - K___int16_t_int16_t _, K___int16_t_int16_t _0, int16_t zeta) { - int16_t a0 = _.fst; - int16_t a1 = _.snd; - int16_t b0 = _0.fst; - int16_t b1 = _0.snd; - int32_t uu____0 = (int32_t)a0 * (int32_t)b0; - int16_t uu____1 = + libcrux_ml_kem_vector_portable_vector_type_PortableVector *a, + libcrux_ml_kem_vector_portable_vector_type_PortableVector *b, int16_t zeta, + size_t i, size_t j, + libcrux_ml_kem_vector_portable_vector_type_PortableVector *out) { + int32_t uu____0 = (int32_t)a->elements[i] * (int32_t)b->elements[i]; + int16_t o0 = libcrux_ml_kem_vector_portable_arithmetic_montgomery_reduce_element( + uu____0 + + (int32_t) + libcrux_ml_kem_vector_portable_arithmetic_montgomery_reduce_element( + (int32_t)a->elements[j] * (int32_t)b->elements[j]) * + (int32_t)zeta); + int16_t o1 = libcrux_ml_kem_vector_portable_arithmetic_montgomery_reduce_element( - uu____0 + - (int32_t) - libcrux_ml_kem_vector_portable_arithmetic_montgomery_reduce_element( - (int32_t)a1 * (int32_t)b1) * - (int32_t)zeta); - return (CLITERAL(K___int16_t_int16_t){ - .fst = uu____1, - .snd = - libcrux_ml_kem_vector_portable_arithmetic_montgomery_reduce_element( - (int32_t)a0 * (int32_t)b1 + (int32_t)a1 * (int32_t)b0)}); + (int32_t)a->elements[i] * (int32_t)b->elements[j] + + (int32_t)a->elements[j] * (int32_t)b->elements[i]); + out->elements[i] = o0; + out->elements[j] = o1; } static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector @@ -1344,94 +1484,22 @@ libcrux_ml_kem_vector_portable_ntt_ntt_multiply( int16_t zeta0, int16_t zeta1, int16_t zeta2, int16_t zeta3) { libcrux_ml_kem_vector_portable_vector_type_PortableVector out = libcrux_ml_kem_vector_portable_vector_type_zero(); - K___int16_t_int16_t lit0; - lit0.fst = lhs->elements[0U]; - lit0.snd = lhs->elements[1U]; - K___int16_t_int16_t lit1; - lit1.fst = rhs->elements[0U]; - lit1.snd = rhs->elements[1U]; - K___int16_t_int16_t product = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit0, lit1, - zeta0); - out.elements[0U] = product.fst; - out.elements[1U] = product.snd; - K___int16_t_int16_t lit2; - lit2.fst = lhs->elements[2U]; - lit2.snd = lhs->elements[3U]; - K___int16_t_int16_t lit3; - lit3.fst = rhs->elements[2U]; - lit3.snd = rhs->elements[3U]; - K___int16_t_int16_t product0 = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit2, lit3, - -zeta0); - out.elements[2U] = product0.fst; - out.elements[3U] = product0.snd; - K___int16_t_int16_t lit4; - lit4.fst = lhs->elements[4U]; - lit4.snd = lhs->elements[5U]; - K___int16_t_int16_t lit5; - lit5.fst = rhs->elements[4U]; - lit5.snd = rhs->elements[5U]; - K___int16_t_int16_t product1 = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit4, lit5, - zeta1); - out.elements[4U] = product1.fst; - out.elements[5U] = product1.snd; - K___int16_t_int16_t lit6; - lit6.fst = lhs->elements[6U]; - lit6.snd = lhs->elements[7U]; - K___int16_t_int16_t lit7; - lit7.fst = rhs->elements[6U]; - lit7.snd = rhs->elements[7U]; - K___int16_t_int16_t product2 = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit6, lit7, - -zeta1); - out.elements[6U] = product2.fst; - out.elements[7U] = product2.snd; - K___int16_t_int16_t lit8; - lit8.fst = lhs->elements[(size_t)8U + (size_t)0U]; - lit8.snd = lhs->elements[(size_t)8U + (size_t)1U]; - K___int16_t_int16_t lit9; - lit9.fst = rhs->elements[(size_t)8U + (size_t)0U]; - lit9.snd = rhs->elements[(size_t)8U + (size_t)1U]; - K___int16_t_int16_t product3 = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit8, lit9, - zeta2); - out.elements[(size_t)8U + (size_t)0U] = product3.fst; - out.elements[(size_t)8U + (size_t)1U] = product3.snd; - K___int16_t_int16_t lit10; - lit10.fst = lhs->elements[(size_t)8U + (size_t)2U]; - lit10.snd = lhs->elements[(size_t)8U + (size_t)3U]; - K___int16_t_int16_t lit11; - lit11.fst = rhs->elements[(size_t)8U + (size_t)2U]; - lit11.snd = rhs->elements[(size_t)8U + (size_t)3U]; - K___int16_t_int16_t product4 = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit10, lit11, - -zeta2); - out.elements[(size_t)8U + (size_t)2U] = product4.fst; - out.elements[(size_t)8U + (size_t)3U] = product4.snd; - K___int16_t_int16_t lit12; - lit12.fst = lhs->elements[(size_t)8U + (size_t)4U]; - lit12.snd = lhs->elements[(size_t)8U + (size_t)5U]; - K___int16_t_int16_t lit13; - lit13.fst = rhs->elements[(size_t)8U + (size_t)4U]; - lit13.snd = rhs->elements[(size_t)8U + (size_t)5U]; - K___int16_t_int16_t product5 = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit12, lit13, - zeta3); - out.elements[(size_t)8U + (size_t)4U] = product5.fst; - out.elements[(size_t)8U + (size_t)5U] = product5.snd; - K___int16_t_int16_t lit14; - lit14.fst = lhs->elements[(size_t)8U + (size_t)6U]; - lit14.snd = lhs->elements[(size_t)8U + (size_t)7U]; - K___int16_t_int16_t lit; - lit.fst = rhs->elements[(size_t)8U + (size_t)6U]; - lit.snd = rhs->elements[(size_t)8U + (size_t)7U]; - K___int16_t_int16_t product6 = - libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials(lit14, lit, - -zeta3); - out.elements[(size_t)8U + (size_t)6U] = product6.fst; - out.elements[(size_t)8U + (size_t)7U] = product6.snd; + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, zeta0, (size_t)0U, (size_t)1U, &out); + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, -zeta0, (size_t)2U, (size_t)3U, &out); + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, zeta1, (size_t)4U, (size_t)5U, &out); + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, -zeta1, (size_t)6U, (size_t)7U, &out); + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, zeta2, (size_t)8U, (size_t)9U, &out); + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, -zeta2, (size_t)10U, (size_t)11U, &out); + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, zeta3, (size_t)12U, (size_t)13U, &out); + libcrux_ml_kem_vector_portable_ntt_ntt_multiply_binomials( + lhs, rhs, -zeta3, (size_t)14U, (size_t)15U, &out); return out; } @@ -1501,27 +1569,70 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ return libcrux_ml_kem_vector_portable_serialize_deserialize_1(a); } +typedef struct K___uint8_t_uint8_t_uint8_t_uint8_t_s { + uint8_t fst; + uint8_t snd; + uint8_t thd; + uint8_t f3; +} K___uint8_t_uint8_t_uint8_t_uint8_t; + +static KRML_MUSTINLINE K___uint8_t_uint8_t_uint8_t_uint8_t +libcrux_ml_kem_vector_portable_serialize_serialize_4_int(Eurydice_slice v) { + uint8_t uu____0 = (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)1U, int16_t, int16_t *, int16_t) + << 4U; + uint8_t result0 = + (uint32_t)uu____0 | (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)0U, int16_t, int16_t *, int16_t); + uint8_t uu____1 = (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)3U, int16_t, int16_t *, int16_t) + << 4U; + uint8_t result1 = + (uint32_t)uu____1 | (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)2U, int16_t, int16_t *, int16_t); + uint8_t uu____2 = (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)5U, int16_t, int16_t *, int16_t) + << 4U; + uint8_t result2 = + (uint32_t)uu____2 | (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)4U, int16_t, int16_t *, int16_t); + uint8_t uu____3 = (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)7U, int16_t, int16_t *, int16_t) + << 4U; + uint8_t result3 = + (uint32_t)uu____3 | (uint32_t)(uint8_t)Eurydice_slice_index( + v, (size_t)6U, int16_t, int16_t *, int16_t); + return (CLITERAL(K___uint8_t_uint8_t_uint8_t_uint8_t){ + .fst = result0, .snd = result1, .thd = result2, .f3 = result3}); +} + static KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_serialize_serialize_4( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, uint8_t ret[8U]) { + K___uint8_t_uint8_t_uint8_t_uint8_t result0_3 = + libcrux_ml_kem_vector_portable_serialize_serialize_4_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)0U, + .end = (size_t)8U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t_uint8_t result4_7 = + libcrux_ml_kem_vector_portable_serialize_serialize_4_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)8U, + .end = (size_t)16U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); uint8_t result[8U] = {0U}; - result[0U] = (uint32_t)(uint8_t)v.elements[1U] << 4U | - (uint32_t)(uint8_t)v.elements[0U]; - result[1U] = (uint32_t)(uint8_t)v.elements[3U] << 4U | - (uint32_t)(uint8_t)v.elements[2U]; - result[2U] = (uint32_t)(uint8_t)v.elements[5U] << 4U | - (uint32_t)(uint8_t)v.elements[4U]; - result[3U] = (uint32_t)(uint8_t)v.elements[7U] << 4U | - (uint32_t)(uint8_t)v.elements[6U]; - result[4U] = (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)1U] << 4U | - (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)0U]; - result[5U] = (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)3U] << 4U | - (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)2U]; - result[6U] = (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)5U] << 4U | - (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)4U]; - result[7U] = (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)7U] << 4U | - (uint32_t)(uint8_t)v.elements[(size_t)8U + (size_t)6U]; + result[0U] = result0_3.fst; + result[1U] = result0_3.snd; + result[2U] = result0_3.thd; + result[3U] = result0_3.f3; + result[4U] = result4_7.fst; + result[5U] = result4_7.snd; + result[6U] = result4_7.thd; + result[7U] = result4_7.f3; memcpy(ret, result, (size_t)8U * sizeof(uint8_t)); } @@ -1534,58 +1645,70 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ memcpy(ret, ret0, (size_t)8U * sizeof(uint8_t)); } +static KRML_MUSTINLINE + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t + libcrux_ml_kem_vector_portable_serialize_deserialize_4_int( + Eurydice_slice bytes) { + uint8_t ret[4U]; + core_result_Result__uint8_t_4size_t__core_array_TryFromSliceError dst; + Eurydice_slice_to_array2(&dst, bytes, Eurydice_slice, uint8_t[4U], void *); + core_result__core__result__Result_T__E___unwrap__uint8_t_4size_t__core_array_TryFromSliceError( + dst, ret); + uint32_t input = core_num__u32_8__from_le_bytes(ret); + int16_t v0 = (int16_t)(input & 15U); + int16_t v1 = (int16_t)(input >> 4U & 15U); + int16_t v2 = (int16_t)(input >> 8U & 15U); + int16_t v3 = (int16_t)(input >> 12U & 15U); + int16_t v4 = (int16_t)(input >> 16U & 15U); + int16_t v5 = (int16_t)(input >> 20U & 15U); + int16_t v6 = (int16_t)(input >> 24U & 15U); + int16_t v7 = (int16_t)(input >> 28U & 15U); + return (CLITERAL( + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t){ + .fst = v0, + .snd = v1, + .thd = v2, + .f3 = v3, + .f4 = v4, + .f5 = v5, + .f6 = v6, + .f7 = v7}); +} + static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_vector_portable_serialize_deserialize_4(Eurydice_slice bytes) { + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v0_7 = + libcrux_ml_kem_vector_portable_serialize_deserialize_4_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = (size_t)4U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v8_15 = + libcrux_ml_kem_vector_portable_serialize_deserialize_4_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)4U, .end = (size_t)8U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); libcrux_ml_kem_vector_portable_vector_type_PortableVector v = libcrux_ml_kem_vector_portable_vector_type_zero(); - uint8_t *uu____0 = - &Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); - v.elements[0U] = (int16_t)((uint32_t)uu____0[0U] & 15U); - uint8_t *uu____1 = - &Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); - v.elements[1U] = (int16_t)((uint32_t)uu____1[0U] >> 4U & 15U); - uint8_t *uu____2 = - &Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); - v.elements[2U] = (int16_t)((uint32_t)uu____2[0U] & 15U); - uint8_t *uu____3 = - &Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); - v.elements[3U] = (int16_t)((uint32_t)uu____3[0U] >> 4U & 15U); - uint8_t *uu____4 = - &Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t); - v.elements[4U] = (int16_t)((uint32_t)uu____4[0U] & 15U); - uint8_t *uu____5 = - &Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t); - v.elements[5U] = (int16_t)((uint32_t)uu____5[0U] >> 4U & 15U); - uint8_t *uu____6 = - &Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t); - v.elements[6U] = (int16_t)((uint32_t)uu____6[0U] & 15U); - uint8_t *uu____7 = - &Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t); - v.elements[7U] = (int16_t)((uint32_t)uu____7[0U] >> 4U & 15U); - uint8_t *uu____8 = - &Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t); - v.elements[8U] = (int16_t)((uint32_t)uu____8[0U] & 15U); - uint8_t *uu____9 = - &Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t); - v.elements[9U] = (int16_t)((uint32_t)uu____9[0U] >> 4U & 15U); - uint8_t *uu____10 = - &Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *, uint8_t); - v.elements[10U] = (int16_t)((uint32_t)uu____10[0U] & 15U); - uint8_t *uu____11 = - &Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *, uint8_t); - v.elements[11U] = (int16_t)((uint32_t)uu____11[0U] >> 4U & 15U); - uint8_t *uu____12 = - &Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t); - v.elements[12U] = (int16_t)((uint32_t)uu____12[0U] & 15U); - uint8_t *uu____13 = - &Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t); - v.elements[13U] = (int16_t)((uint32_t)uu____13[0U] >> 4U & 15U); - uint8_t *uu____14 = - &Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *, uint8_t); - v.elements[14U] = (int16_t)((uint32_t)uu____14[0U] & 15U); - uint8_t *uu____15 = - &Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *, uint8_t); - v.elements[15U] = (int16_t)((uint32_t)uu____15[0U] >> 4U & 15U); + v.elements[0U] = v0_7.fst; + v.elements[1U] = v0_7.snd; + v.elements[2U] = v0_7.thd; + v.elements[3U] = v0_7.f3; + v.elements[4U] = v0_7.f4; + v.elements[5U] = v0_7.f5; + v.elements[6U] = v0_7.f6; + v.elements[7U] = v0_7.f7; + v.elements[8U] = v8_15.fst; + v.elements[9U] = v8_15.snd; + v.elements[10U] = v8_15.thd; + v.elements[11U] = v8_15.f3; + v.elements[12U] = v8_15.f4; + v.elements[13U] = v8_15.f5; + v.elements[14U] = v8_15.f6; + v.elements[15U] = v8_15.f7; return v; } @@ -1595,37 +1718,85 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ return libcrux_ml_kem_vector_portable_serialize_deserialize_4(a); } +typedef struct K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_s { + uint8_t fst; + uint8_t snd; + uint8_t thd; + uint8_t f3; + uint8_t f4; +} K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t; + +static KRML_MUSTINLINE K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_ml_kem_vector_portable_serialize_serialize_5_int(Eurydice_slice v) { + int16_t uu____0 = + Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *, int16_t); + uint8_t r0 = + (uint8_t)(uu____0 | + Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *, int16_t) + << 5U); + int16_t uu____1 = + Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *, int16_t) >> 3U; + int16_t uu____2 = + uu____1 | Eurydice_slice_index(v, (size_t)2U, int16_t, int16_t *, int16_t) + << 2U; + uint8_t r1 = + (uint8_t)(uu____2 | + Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *, int16_t) + << 7U); + int16_t uu____3 = + Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *, int16_t) >> 1U; + uint8_t r2 = + (uint8_t)(uu____3 | + Eurydice_slice_index(v, (size_t)4U, int16_t, int16_t *, int16_t) + << 4U); + int16_t uu____4 = + Eurydice_slice_index(v, (size_t)4U, int16_t, int16_t *, int16_t) >> 4U; + int16_t uu____5 = + uu____4 | Eurydice_slice_index(v, (size_t)5U, int16_t, int16_t *, int16_t) + << 1U; + uint8_t r3 = + (uint8_t)(uu____5 | + Eurydice_slice_index(v, (size_t)6U, int16_t, int16_t *, int16_t) + << 6U); + int16_t uu____6 = + Eurydice_slice_index(v, (size_t)6U, int16_t, int16_t *, int16_t) >> 2U; + uint8_t r4 = + (uint8_t)(uu____6 | + Eurydice_slice_index(v, (size_t)7U, int16_t, int16_t *, int16_t) + << 3U); + return (CLITERAL(K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t){ + .fst = r0, .snd = r1, .thd = r2, .f3 = r3, .f4 = r4}); +} + static KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_serialize_serialize_5( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, uint8_t ret[10U]) { + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t r0_4 = + libcrux_ml_kem_vector_portable_serialize_serialize_5_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)0U, + .end = (size_t)8U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t r5_9 = + libcrux_ml_kem_vector_portable_serialize_serialize_5_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)8U, + .end = (size_t)16U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); uint8_t result[10U] = {0U}; - result[0U] = (uint8_t)((v.elements[1U] & (int16_t)7) << 5U | v.elements[0U]); - result[1U] = - (uint8_t)(((v.elements[3U] & (int16_t)1) << 7U | v.elements[2U] << 2U) | - v.elements[1U] >> 3U); - result[2U] = - (uint8_t)((v.elements[4U] & (int16_t)15) << 4U | v.elements[3U] >> 1U); - result[3U] = - (uint8_t)(((v.elements[6U] & (int16_t)3) << 6U | v.elements[5U] << 1U) | - v.elements[4U] >> 4U); - result[4U] = (uint8_t)(v.elements[7U] << 3U | v.elements[6U] >> 2U); - result[5U] = - (uint8_t)((v.elements[(size_t)8U + (size_t)1U] & (int16_t)7) << 5U | - v.elements[(size_t)8U + (size_t)0U]); - result[6U] = - (uint8_t)(((v.elements[(size_t)8U + (size_t)3U] & (int16_t)1) << 7U | - v.elements[(size_t)8U + (size_t)2U] << 2U) | - v.elements[(size_t)8U + (size_t)1U] >> 3U); - result[7U] = - (uint8_t)((v.elements[(size_t)8U + (size_t)4U] & (int16_t)15) << 4U | - v.elements[(size_t)8U + (size_t)3U] >> 1U); - result[8U] = - (uint8_t)(((v.elements[(size_t)8U + (size_t)6U] & (int16_t)3) << 6U | - v.elements[(size_t)8U + (size_t)5U] << 1U) | - v.elements[(size_t)8U + (size_t)4U] >> 4U); - result[9U] = (uint8_t)(v.elements[(size_t)8U + (size_t)7U] << 3U | - v.elements[(size_t)8U + (size_t)6U] >> 2U); + result[0U] = r0_4.fst; + result[1U] = r0_4.snd; + result[2U] = r0_4.thd; + result[3U] = r0_4.f3; + result[4U] = r0_4.f4; + result[5U] = r5_9.fst; + result[6U] = r5_9.snd; + result[7U] = r5_9.thd; + result[8U] = r5_9.f3; + result[9U] = r5_9.f4; memcpy(ret, result, (size_t)10U * sizeof(uint8_t)); } @@ -1638,97 +1809,102 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ memcpy(ret, ret0, (size_t)10U * sizeof(uint8_t)); } -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_serialize_deserialize_5(Eurydice_slice bytes) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector v = - libcrux_ml_kem_vector_portable_vector_type_zero(); - uint8_t *uu____0 = - &Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); - v.elements[0U] = (int16_t)((uint32_t)uu____0[0U] & 31U); - uint8_t uu____1 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, +static KRML_MUSTINLINE + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t + libcrux_ml_kem_vector_portable_serialize_deserialize_5_int( + Eurydice_slice bytes) { + int16_t v0 = (int16_t)((uint32_t)Eurydice_slice_index( + bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t) & + 31U); + uint8_t uu____0 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t) & 3U) << 3U; - uint8_t *uu____2 = - &Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); - v.elements[1U] = (int16_t)((uint32_t)uu____1 | (uint32_t)uu____2[0U] >> 5U); - uint8_t *uu____3 = - &Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); - v.elements[2U] = (int16_t)((uint32_t)uu____3[0U] >> 2U & 31U); - uint8_t uu____4 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, + int16_t v1 = (int16_t)((uint32_t)uu____0 | + (uint32_t)Eurydice_slice_index( + bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t) >> + 5U); + int16_t v2 = (int16_t)((uint32_t)Eurydice_slice_index( + bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t) >> + 2U & + 31U); + uint8_t uu____1 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t) & 15U) << 1U; - uint8_t *uu____5 = - &Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); - v.elements[3U] = (int16_t)((uint32_t)uu____4 | (uint32_t)uu____5[0U] >> 7U); - uint8_t uu____6 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, + int16_t v3 = (int16_t)((uint32_t)uu____1 | + (uint32_t)Eurydice_slice_index( + bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t) >> + 7U); + uint8_t uu____2 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t) & 1U) << 4U; - uint8_t *uu____7 = - &Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t); - v.elements[4U] = (int16_t)((uint32_t)uu____6 | (uint32_t)uu____7[0U] >> 4U); - uint8_t *uu____8 = - &Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t); - v.elements[5U] = (int16_t)((uint32_t)uu____8[0U] >> 1U & 31U); - uint8_t uu____9 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, + int16_t v4 = (int16_t)((uint32_t)uu____2 | + (uint32_t)Eurydice_slice_index( + bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t) >> + 4U); + int16_t v5 = (int16_t)((uint32_t)Eurydice_slice_index( + bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t) >> + 1U & + 31U); + uint8_t uu____3 = ((uint32_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t) & 7U) << 2U; - uint8_t *uu____10 = - &Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t); - v.elements[6U] = (int16_t)((uint32_t)uu____9 | (uint32_t)uu____10[0U] >> 6U); - uint8_t *uu____11 = - &Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t); - v.elements[7U] = (int16_t)((uint32_t)uu____11[0U] >> 3U); - uint8_t *uu____12 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)0U, - uint8_t, uint8_t *, uint8_t); - v.elements[8U] = (int16_t)((uint32_t)uu____12[0U] & 31U); - uint8_t uu____13 = - ((uint32_t)Eurydice_slice_index(bytes, (size_t)5U + (size_t)1U, uint8_t, - uint8_t *, uint8_t) & - 3U) - << 3U; - uint8_t *uu____14 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)0U, - uint8_t, uint8_t *, uint8_t); - v.elements[9U] = (int16_t)((uint32_t)uu____13 | (uint32_t)uu____14[0U] >> 5U); - uint8_t *uu____15 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)1U, - uint8_t, uint8_t *, uint8_t); - v.elements[10U] = (int16_t)((uint32_t)uu____15[0U] >> 2U & 31U); - uint8_t uu____16 = - ((uint32_t)Eurydice_slice_index(bytes, (size_t)5U + (size_t)2U, uint8_t, - uint8_t *, uint8_t) & - 15U) - << 1U; - uint8_t *uu____17 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)1U, - uint8_t, uint8_t *, uint8_t); - v.elements[11U] = - (int16_t)((uint32_t)uu____16 | (uint32_t)uu____17[0U] >> 7U); - uint8_t uu____18 = - ((uint32_t)Eurydice_slice_index(bytes, (size_t)5U + (size_t)3U, uint8_t, - uint8_t *, uint8_t) & - 1U) - << 4U; - uint8_t *uu____19 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)2U, - uint8_t, uint8_t *, uint8_t); - v.elements[12U] = - (int16_t)((uint32_t)uu____18 | (uint32_t)uu____19[0U] >> 4U); - uint8_t *uu____20 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)3U, - uint8_t, uint8_t *, uint8_t); - v.elements[13U] = (int16_t)((uint32_t)uu____20[0U] >> 1U & 31U); - uint8_t uu____21 = - ((uint32_t)Eurydice_slice_index(bytes, (size_t)5U + (size_t)4U, uint8_t, - uint8_t *, uint8_t) & - 7U) - << 2U; - uint8_t *uu____22 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)3U, - uint8_t, uint8_t *, uint8_t); - v.elements[14U] = - (int16_t)((uint32_t)uu____21 | (uint32_t)uu____22[0U] >> 6U); - uint8_t *uu____23 = &Eurydice_slice_index(bytes, (size_t)5U + (size_t)4U, - uint8_t, uint8_t *, uint8_t); - v.elements[15U] = (int16_t)((uint32_t)uu____23[0U] >> 3U); + int16_t v6 = (int16_t)((uint32_t)uu____3 | + (uint32_t)Eurydice_slice_index( + bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t) >> + 6U); + int16_t v7 = (int16_t)((uint32_t)Eurydice_slice_index( + bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t) >> + 3U); + return (CLITERAL( + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t){ + .fst = v0, + .snd = v1, + .thd = v2, + .f3 = v3, + .f4 = v4, + .f5 = v5, + .f6 = v6, + .f7 = v7}); +} + +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_serialize_deserialize_5(Eurydice_slice bytes) { + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v0_7 = + libcrux_ml_kem_vector_portable_serialize_deserialize_5_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = (size_t)5U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v8_15 = + libcrux_ml_kem_vector_portable_serialize_deserialize_5_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)5U, .end = (size_t)10U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + libcrux_ml_kem_vector_portable_vector_type_PortableVector v = + libcrux_ml_kem_vector_portable_vector_type_zero(); + v.elements[0U] = v0_7.fst; + v.elements[1U] = v0_7.snd; + v.elements[2U] = v0_7.thd; + v.elements[3U] = v0_7.f3; + v.elements[4U] = v0_7.f4; + v.elements[5U] = v0_7.f5; + v.elements[6U] = v0_7.f6; + v.elements[7U] = v0_7.f7; + v.elements[8U] = v8_15.fst; + v.elements[9U] = v8_15.snd; + v.elements[10U] = v8_15.thd; + v.elements[11U] = v8_15.f3; + v.elements[12U] = v8_15.f4; + v.elements[13U] = v8_15.f5; + v.elements[14U] = v8_15.f6; + v.elements[15U] = v8_15.f7; return v; } @@ -1738,63 +1914,102 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ return libcrux_ml_kem_vector_portable_serialize_deserialize_5(a); } +static KRML_MUSTINLINE K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_ml_kem_vector_portable_serialize_serialize_10_int(Eurydice_slice v) { + uint8_t r0 = (uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *, + int16_t) & + (int16_t)255); + uint8_t uu____0 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *, int16_t) & + (int16_t)63) + << 2U; + uint8_t r1 = (uint32_t)uu____0 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, + int16_t *, int16_t) >> + 8U & + (int16_t)3); + uint8_t uu____1 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *, int16_t) & + (int16_t)15) + << 4U; + uint8_t r2 = (uint32_t)uu____1 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *, int16_t) >> + 6U & + (int16_t)15); + uint8_t uu____2 = + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, + int16_t *, int16_t) & + (int16_t)3) + << 6U; + uint8_t r3 = (uint32_t)uu____2 | + (uint32_t)(uint8_t)(Eurydice_slice_index(v, (size_t)2U, int16_t, + int16_t *, int16_t) >> + 4U & + (int16_t)63); + uint8_t r4 = (uint8_t)(Eurydice_slice_index(v, (size_t)3U, int16_t, int16_t *, + int16_t) >> + 2U & + (int16_t)255); + return (CLITERAL(K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t){ + .fst = r0, .snd = r1, .thd = r2, .f3 = r3, .f4 = r4}); +} + static KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_serialize_serialize_10( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, uint8_t ret[20U]) { + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t r0_4 = + libcrux_ml_kem_vector_portable_serialize_serialize_10_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)0U, + .end = (size_t)4U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t r5_9 = + libcrux_ml_kem_vector_portable_serialize_serialize_10_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)4U, + .end = (size_t)8U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t r10_14 = + libcrux_ml_kem_vector_portable_serialize_serialize_10_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)8U, + .end = (size_t)12U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t r15_19 = + libcrux_ml_kem_vector_portable_serialize_serialize_10_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)12U, + .end = (size_t)16U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); uint8_t result[20U] = {0U}; - result[0U] = (uint8_t)(v.elements[0U] & (int16_t)255); - result[1U] = (uint32_t)(uint8_t)(v.elements[1U] & (int16_t)63) << 2U | - (uint32_t)(uint8_t)(v.elements[0U] >> 8U & (int16_t)3); - result[2U] = (uint32_t)(uint8_t)(v.elements[2U] & (int16_t)15) << 4U | - (uint32_t)(uint8_t)(v.elements[1U] >> 6U & (int16_t)15); - result[3U] = (uint32_t)(uint8_t)(v.elements[3U] & (int16_t)3) << 6U | - (uint32_t)(uint8_t)(v.elements[2U] >> 4U & (int16_t)63); - result[4U] = (uint8_t)(v.elements[3U] >> 2U & (int16_t)255); - result[5U] = (uint8_t)(v.elements[4U] & (int16_t)255); - result[6U] = (uint32_t)(uint8_t)(v.elements[5U] & (int16_t)63) << 2U | - (uint32_t)(uint8_t)(v.elements[4U] >> 8U & (int16_t)3); - result[7U] = (uint32_t)(uint8_t)(v.elements[6U] & (int16_t)15) << 4U | - (uint32_t)(uint8_t)(v.elements[5U] >> 6U & (int16_t)15); - result[8U] = (uint32_t)(uint8_t)(v.elements[7U] & (int16_t)3) << 6U | - (uint32_t)(uint8_t)(v.elements[6U] >> 4U & (int16_t)63); - result[9U] = (uint8_t)(v.elements[7U] >> 2U & (int16_t)255); - result[10U] = (uint8_t)(v.elements[(size_t)8U + (size_t)0U] & (int16_t)255); - result[11U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)1U] & (int16_t)63) - << 2U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)0U] >> 8U & - (int16_t)3); - result[12U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)2U] & (int16_t)15) - << 4U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)1U] >> 6U & - (int16_t)15); - result[13U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)3U] & (int16_t)3) - << 6U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)2U] >> 4U & - (int16_t)63); - result[14U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)3U] >> 2U & (int16_t)255); - result[15U] = (uint8_t)(v.elements[(size_t)8U + (size_t)4U] & (int16_t)255); - result[16U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)5U] & (int16_t)63) - << 2U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)4U] >> 8U & - (int16_t)3); - result[17U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)6U] & (int16_t)15) - << 4U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)5U] >> 6U & - (int16_t)15); - result[18U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)7U] & (int16_t)3) - << 6U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)6U] >> 4U & - (int16_t)63); - result[19U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)7U] >> 2U & (int16_t)255); + result[0U] = r0_4.fst; + result[1U] = r0_4.snd; + result[2U] = r0_4.thd; + result[3U] = r0_4.f3; + result[4U] = r0_4.f4; + result[5U] = r5_9.fst; + result[6U] = r5_9.snd; + result[7U] = r5_9.thd; + result[8U] = r5_9.f3; + result[9U] = r5_9.f4; + result[10U] = r10_14.fst; + result[11U] = r10_14.snd; + result[12U] = r10_14.thd; + result[13U] = r10_14.f3; + result[14U] = r10_14.f4; + result[15U] = r15_19.fst; + result[16U] = r15_19.snd; + result[17U] = r15_19.thd; + result[18U] = r15_19.f3; + result[19U] = r15_19.f4; memcpy(ret, result, (size_t)20U * sizeof(uint8_t)); } @@ -1807,396 +2022,229 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ memcpy(ret, ret0, (size_t)20U * sizeof(uint8_t)); } -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_serialize_deserialize_10(Eurydice_slice bytes) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector result = - libcrux_ml_kem_vector_portable_vector_type_zero(); +static KRML_MUSTINLINE + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t + libcrux_ml_kem_vector_portable_serialize_deserialize_10_int( + Eurydice_slice bytes) { int16_t uu____0 = ((int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t) & (int16_t)3) << 8U; - uint8_t *uu____1 = - &Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); - result.elements[0U] = uu____0 | ((int16_t)uu____1[0U] & (int16_t)255); - int16_t uu____2 = ((int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, + int16_t r0 = uu____0 | ((int16_t)Eurydice_slice_index( + bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t) & + (int16_t)255); + int16_t uu____1 = ((int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t) & (int16_t)15) << 6U; - uint8_t *uu____3 = - &Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); - result.elements[1U] = uu____2 | (int16_t)uu____3[0U] >> 2U; - int16_t uu____4 = ((int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, + int16_t r1 = uu____1 | (int16_t)Eurydice_slice_index( + bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t) >> + 2U; + int16_t uu____2 = ((int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t) & (int16_t)63) << 4U; - uint8_t *uu____5 = - &Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t); - result.elements[2U] = uu____4 | (int16_t)uu____5[0U] >> 4U; - int16_t uu____6 = (int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, + int16_t r2 = uu____2 | (int16_t)Eurydice_slice_index( + bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t) >> + 4U; + int16_t uu____3 = (int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t) << 2U; - uint8_t *uu____7 = - &Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t); - result.elements[3U] = uu____6 | (int16_t)uu____7[0U] >> 6U; - int16_t uu____8 = ((int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, + int16_t r3 = uu____3 | (int16_t)Eurydice_slice_index( + bytes, (size_t)3U, uint8_t, uint8_t *, uint8_t) >> + 6U; + int16_t uu____4 = ((int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t) & (int16_t)3) << 8U; - uint8_t *uu____9 = - &Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *, uint8_t); - result.elements[4U] = uu____8 | ((int16_t)uu____9[0U] & (int16_t)255); - int16_t uu____10 = ((int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)15) - << 6U; - uint8_t *uu____11 = - &Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t); - result.elements[5U] = uu____10 | (int16_t)uu____11[0U] >> 2U; - int16_t uu____12 = ((int16_t)Eurydice_slice_index(bytes, (size_t)8U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)63) - << 4U; - uint8_t *uu____13 = - &Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *, uint8_t); - result.elements[6U] = uu____12 | (int16_t)uu____13[0U] >> 4U; - int16_t uu____14 = (int16_t)Eurydice_slice_index(bytes, (size_t)9U, uint8_t, - uint8_t *, uint8_t) - << 2U; - uint8_t *uu____15 = - &Eurydice_slice_index(bytes, (size_t)8U, uint8_t, uint8_t *, uint8_t); - result.elements[7U] = uu____14 | (int16_t)uu____15[0U] >> 6U; - int16_t uu____16 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)1U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)3) - << 8U; - uint8_t *uu____17 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)0U, - uint8_t, uint8_t *, uint8_t); - result.elements[8U] = uu____16 | ((int16_t)uu____17[0U] & (int16_t)255); - int16_t uu____18 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)2U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)15) - << 6U; - uint8_t *uu____19 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)1U, - uint8_t, uint8_t *, uint8_t); - result.elements[9U] = uu____18 | (int16_t)uu____19[0U] >> 2U; - int16_t uu____20 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)3U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)63) - << 4U; - uint8_t *uu____21 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)2U, - uint8_t, uint8_t *, uint8_t); - result.elements[10U] = uu____20 | (int16_t)uu____21[0U] >> 4U; - int16_t uu____22 = - (int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)4U, uint8_t, - uint8_t *, uint8_t) - << 2U; - uint8_t *uu____23 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)3U, - uint8_t, uint8_t *, uint8_t); - result.elements[11U] = uu____22 | (int16_t)uu____23[0U] >> 6U; - int16_t uu____24 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)6U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)3) - << 8U; - uint8_t *uu____25 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)5U, - uint8_t, uint8_t *, uint8_t); - result.elements[12U] = uu____24 | ((int16_t)uu____25[0U] & (int16_t)255); - int16_t uu____26 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)7U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)15) - << 6U; - uint8_t *uu____27 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)6U, - uint8_t, uint8_t *, uint8_t); - result.elements[13U] = uu____26 | (int16_t)uu____27[0U] >> 2U; - int16_t uu____28 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)8U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)63) - << 4U; - uint8_t *uu____29 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)7U, - uint8_t, uint8_t *, uint8_t); - result.elements[14U] = uu____28 | (int16_t)uu____29[0U] >> 4U; - int16_t uu____30 = - (int16_t)Eurydice_slice_index(bytes, (size_t)10U + (size_t)9U, uint8_t, - uint8_t *, uint8_t) - << 2U; - uint8_t *uu____31 = &Eurydice_slice_index(bytes, (size_t)10U + (size_t)8U, - uint8_t, uint8_t *, uint8_t); - result.elements[15U] = uu____30 | (int16_t)uu____31[0U] >> 6U; - return result; -} - -static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___deserialize_10( - Eurydice_slice a) { - return libcrux_ml_kem_vector_portable_serialize_deserialize_10(a); -} - -static KRML_MUSTINLINE void -libcrux_ml_kem_vector_portable_serialize_serialize_11( - libcrux_ml_kem_vector_portable_vector_type_PortableVector v, - uint8_t ret[22U]) { - uint8_t result[22U] = {0U}; - result[0U] = (uint8_t)v.elements[0U]; - result[1U] = (uint32_t)(uint8_t)(v.elements[1U] & (int16_t)31) << 3U | - (uint32_t)(uint8_t)(v.elements[0U] >> 8U); - result[2U] = (uint32_t)(uint8_t)(v.elements[2U] & (int16_t)3) << 6U | - (uint32_t)(uint8_t)(v.elements[1U] >> 5U); - result[3U] = (uint8_t)(v.elements[2U] >> 2U & (int16_t)255); - result[4U] = (uint32_t)(uint8_t)(v.elements[3U] & (int16_t)127) << 1U | - (uint32_t)(uint8_t)(v.elements[2U] >> 10U); - result[5U] = (uint32_t)(uint8_t)(v.elements[4U] & (int16_t)15) << 4U | - (uint32_t)(uint8_t)(v.elements[3U] >> 7U); - result[6U] = (uint32_t)(uint8_t)(v.elements[5U] & (int16_t)1) << 7U | - (uint32_t)(uint8_t)(v.elements[4U] >> 4U); - result[7U] = (uint8_t)(v.elements[5U] >> 1U & (int16_t)255); - result[8U] = (uint32_t)(uint8_t)(v.elements[6U] & (int16_t)63) << 2U | - (uint32_t)(uint8_t)(v.elements[5U] >> 9U); - result[9U] = (uint32_t)(uint8_t)(v.elements[7U] & (int16_t)7) << 5U | - (uint32_t)(uint8_t)(v.elements[6U] >> 6U); - result[10U] = (uint8_t)(v.elements[7U] >> 3U); - result[11U] = (uint8_t)v.elements[(size_t)8U + (size_t)0U]; - result[12U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)1U] & (int16_t)31) - << 3U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)0U] >> 8U); - result[13U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)2U] & (int16_t)3) - << 6U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)1U] >> 5U); - result[14U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)2U] >> 2U & (int16_t)255); - result[15U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)3U] & (int16_t)127) - << 1U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)2U] >> 10U); - result[16U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)4U] & (int16_t)15) - << 4U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)3U] >> 7U); - result[17U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)5U] & (int16_t)1) - << 7U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)4U] >> 4U); - result[18U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)5U] >> 1U & (int16_t)255); - result[19U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)6U] & (int16_t)63) - << 2U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)5U] >> 9U); - result[20U] = - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)7U] & (int16_t)7) - << 5U | - (uint32_t)(uint8_t)(v.elements[(size_t)8U + (size_t)6U] >> 6U); - result[21U] = (uint8_t)(v.elements[(size_t)8U + (size_t)7U] >> 3U); - memcpy(ret, result, (size_t)22U * sizeof(uint8_t)); -} - -static inline void -libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___serialize_11( - libcrux_ml_kem_vector_portable_vector_type_PortableVector a, - uint8_t ret[22U]) { - uint8_t ret0[22U]; - libcrux_ml_kem_vector_portable_serialize_serialize_11(a, ret0); - memcpy(ret, ret0, (size_t)22U * sizeof(uint8_t)); -} - -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_serialize_deserialize_11(Eurydice_slice bytes) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector result = - libcrux_ml_kem_vector_portable_vector_type_zero(); - int16_t uu____0 = ((int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)7) - << 8U; - uint8_t *uu____1 = - &Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); - result.elements[0U] = uu____0 | (int16_t)uu____1[0U]; - int16_t uu____2 = ((int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)63) - << 5U; - uint8_t *uu____3 = - &Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); - result.elements[1U] = uu____2 | (int16_t)uu____3[0U] >> 3U; - int16_t uu____4 = ((int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)1) - << 10U; - int16_t uu____5 = - uu____4 | (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, - uint8_t *, uint8_t) - << 2U; - uint8_t *uu____6 = - &Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t); - result.elements[2U] = uu____5 | (int16_t)uu____6[0U] >> 6U; - int16_t uu____7 = ((int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, + int16_t r4 = uu____4 | ((int16_t)Eurydice_slice_index( + bytes, (size_t)5U, uint8_t, uint8_t *, uint8_t) & + (int16_t)255); + int16_t uu____5 = ((int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t *, uint8_t) & (int16_t)15) - << 7U; - uint8_t *uu____8 = - &Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t *, uint8_t); - result.elements[3U] = uu____7 | (int16_t)uu____8[0U] >> 1U; - int16_t uu____9 = ((int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, + << 6U; + int16_t r5 = uu____5 | (int16_t)Eurydice_slice_index( + bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t) >> + 2U; + int16_t uu____6 = ((int16_t)Eurydice_slice_index(bytes, (size_t)8U, uint8_t, uint8_t *, uint8_t) & - (int16_t)127) + (int16_t)63) << 4U; - uint8_t *uu____10 = - &Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t *, uint8_t); - result.elements[4U] = uu____9 | (int16_t)uu____10[0U] >> 4U; - int16_t uu____11 = ((int16_t)Eurydice_slice_index(bytes, (size_t)8U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)3) - << 9U; - int16_t uu____12 = - uu____11 | (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, - uint8_t *, uint8_t) - << 1U; - uint8_t *uu____13 = - &Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t *, uint8_t); - result.elements[5U] = uu____12 | (int16_t)uu____13[0U] >> 7U; - int16_t uu____14 = ((int16_t)Eurydice_slice_index(bytes, (size_t)9U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)31) - << 6U; - uint8_t *uu____15 = - &Eurydice_slice_index(bytes, (size_t)8U, uint8_t, uint8_t *, uint8_t); - result.elements[6U] = uu____14 | (int16_t)uu____15[0U] >> 2U; - int16_t uu____16 = (int16_t)Eurydice_slice_index(bytes, (size_t)10U, uint8_t, - uint8_t *, uint8_t) - << 3U; - uint8_t *uu____17 = - &Eurydice_slice_index(bytes, (size_t)9U, uint8_t, uint8_t *, uint8_t); - result.elements[7U] = uu____16 | (int16_t)uu____17[0U] >> 5U; - int16_t uu____18 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)1U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)7) - << 8U; - uint8_t *uu____19 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)0U, - uint8_t, uint8_t *, uint8_t); - result.elements[8U] = uu____18 | (int16_t)uu____19[0U]; - int16_t uu____20 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)2U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)63) - << 5U; - uint8_t *uu____21 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)1U, - uint8_t, uint8_t *, uint8_t); - result.elements[9U] = uu____20 | (int16_t)uu____21[0U] >> 3U; - int16_t uu____22 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)4U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)1) - << 10U; - int16_t uu____23 = - uu____22 | (int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)3U, - uint8_t, uint8_t *, uint8_t) - << 2U; - uint8_t *uu____24 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)2U, - uint8_t, uint8_t *, uint8_t); - result.elements[10U] = uu____23 | (int16_t)uu____24[0U] >> 6U; - int16_t uu____25 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)5U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)15) - << 7U; - uint8_t *uu____26 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)4U, - uint8_t, uint8_t *, uint8_t); - result.elements[11U] = uu____25 | (int16_t)uu____26[0U] >> 1U; - int16_t uu____27 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)6U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)127) - << 4U; - uint8_t *uu____28 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)5U, - uint8_t, uint8_t *, uint8_t); - result.elements[12U] = uu____27 | (int16_t)uu____28[0U] >> 4U; - int16_t uu____29 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)8U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)3) - << 9U; - int16_t uu____30 = - uu____29 | (int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)7U, - uint8_t, uint8_t *, uint8_t) - << 1U; - uint8_t *uu____31 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)6U, - uint8_t, uint8_t *, uint8_t); - result.elements[13U] = uu____30 | (int16_t)uu____31[0U] >> 7U; - int16_t uu____32 = - ((int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)9U, uint8_t, - uint8_t *, uint8_t) & - (int16_t)31) - << 6U; - uint8_t *uu____33 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)8U, - uint8_t, uint8_t *, uint8_t); - result.elements[14U] = uu____32 | (int16_t)uu____33[0U] >> 2U; - int16_t uu____34 = - (int16_t)Eurydice_slice_index(bytes, (size_t)11U + (size_t)10U, uint8_t, - uint8_t *, uint8_t) - << 3U; - uint8_t *uu____35 = &Eurydice_slice_index(bytes, (size_t)11U + (size_t)9U, - uint8_t, uint8_t *, uint8_t); - result.elements[15U] = uu____34 | (int16_t)uu____35[0U] >> 5U; - return result; + int16_t r6 = uu____6 | (int16_t)Eurydice_slice_index( + bytes, (size_t)7U, uint8_t, uint8_t *, uint8_t) >> + 4U; + int16_t uu____7 = (int16_t)Eurydice_slice_index(bytes, (size_t)9U, uint8_t, + uint8_t *, uint8_t) + << 2U; + int16_t r7 = uu____7 | (int16_t)Eurydice_slice_index( + bytes, (size_t)8U, uint8_t, uint8_t *, uint8_t) >> + 6U; + return (CLITERAL( + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t){ + .fst = r0, + .snd = r1, + .thd = r2, + .f3 = r3, + .f4 = r4, + .f5 = r5, + .f6 = r6, + .f7 = r7}); +} + +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_serialize_deserialize_10(Eurydice_slice bytes) { + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v0_7 = + libcrux_ml_kem_vector_portable_serialize_deserialize_10_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = (size_t)10U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t_int16_t v8_15 = + libcrux_ml_kem_vector_portable_serialize_deserialize_10_int( + Eurydice_slice_subslice( + bytes, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)10U, + .end = (size_t)20U}), + uint8_t, core_ops_range_Range__size_t, Eurydice_slice)); + libcrux_ml_kem_vector_portable_vector_type_PortableVector v = + libcrux_ml_kem_vector_portable_vector_type_zero(); + v.elements[0U] = v0_7.fst; + v.elements[1U] = v0_7.snd; + v.elements[2U] = v0_7.thd; + v.elements[3U] = v0_7.f3; + v.elements[4U] = v0_7.f4; + v.elements[5U] = v0_7.f5; + v.elements[6U] = v0_7.f6; + v.elements[7U] = v0_7.f7; + v.elements[8U] = v8_15.fst; + v.elements[9U] = v8_15.snd; + v.elements[10U] = v8_15.thd; + v.elements[11U] = v8_15.f3; + v.elements[12U] = v8_15.f4; + v.elements[13U] = v8_15.f5; + v.elements[14U] = v8_15.f6; + v.elements[15U] = v8_15.f7; + return v; } static inline libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___deserialize_11( +libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_libcrux_ml_kem__vector__portable__vector_type__PortableVector___deserialize_10( Eurydice_slice a) { - return libcrux_ml_kem_vector_portable_serialize_deserialize_11(a); + return libcrux_ml_kem_vector_portable_serialize_deserialize_10(a); +} + +typedef struct K___uint8_t_uint8_t_uint8_t_s { + uint8_t fst; + uint8_t snd; + uint8_t thd; +} K___uint8_t_uint8_t_uint8_t; + +static KRML_MUSTINLINE K___uint8_t_uint8_t_uint8_t +libcrux_ml_kem_vector_portable_serialize_serialize_12_int(Eurydice_slice v) { + uint8_t r0 = (uint8_t)(Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *, + int16_t) & + (int16_t)255); + int16_t uu____0 = + Eurydice_slice_index(v, (size_t)0U, int16_t, int16_t *, int16_t) >> 8U; + uint8_t r1 = (uint8_t)(uu____0 | (Eurydice_slice_index(v, (size_t)1U, int16_t, + int16_t *, int16_t) & + (int16_t)15) + << 4U); + uint8_t r2 = (uint8_t)(Eurydice_slice_index(v, (size_t)1U, int16_t, int16_t *, + int16_t) >> + 4U & + (int16_t)255); + return ( + CLITERAL(K___uint8_t_uint8_t_uint8_t){.fst = r0, .snd = r1, .thd = r2}); } static KRML_MUSTINLINE void libcrux_ml_kem_vector_portable_serialize_serialize_12( libcrux_ml_kem_vector_portable_vector_type_PortableVector v, uint8_t ret[24U]) { + K___uint8_t_uint8_t_uint8_t r0_2 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)0U, + .end = (size_t)2U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t r3_5 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)2U, + .end = (size_t)4U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t r6_8 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)4U, + .end = (size_t)6U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t r9_11 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)6U, + .end = (size_t)8U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t r12_14 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)8U, + .end = (size_t)10U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t r15_17 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)10U, + .end = (size_t)12U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t r18_20 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)12U, + .end = (size_t)14U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___uint8_t_uint8_t_uint8_t r21_23 = + libcrux_ml_kem_vector_portable_serialize_serialize_12_int( + Eurydice_array_to_subslice( + (size_t)16U, v.elements, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)14U, + .end = (size_t)16U}), + int16_t, core_ops_range_Range__size_t, Eurydice_slice)); uint8_t result[24U] = {0U}; - result[0U] = (uint8_t)(v.elements[0U] & (int16_t)255); - result[1U] = - (uint8_t)(v.elements[0U] >> 8U | (v.elements[1U] & (int16_t)15) << 4U); - result[2U] = (uint8_t)(v.elements[1U] >> 4U & (int16_t)255); - result[3U] = (uint8_t)(v.elements[2U] & (int16_t)255); - result[4U] = - (uint8_t)(v.elements[2U] >> 8U | (v.elements[3U] & (int16_t)15) << 4U); - result[5U] = (uint8_t)(v.elements[3U] >> 4U & (int16_t)255); - result[6U] = (uint8_t)(v.elements[4U] & (int16_t)255); - result[7U] = - (uint8_t)(v.elements[4U] >> 8U | (v.elements[5U] & (int16_t)15) << 4U); - result[8U] = (uint8_t)(v.elements[5U] >> 4U & (int16_t)255); - result[9U] = (uint8_t)(v.elements[6U] & (int16_t)255); - result[10U] = - (uint8_t)(v.elements[6U] >> 8U | (v.elements[7U] & (int16_t)15) << 4U); - result[11U] = (uint8_t)(v.elements[7U] >> 4U & (int16_t)255); - result[12U] = (uint8_t)(v.elements[(size_t)8U + (size_t)0U] & (int16_t)255); - result[13U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)0U] >> 8U | - (v.elements[(size_t)8U + (size_t)1U] & (int16_t)15) << 4U); - result[14U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)1U] >> 4U & (int16_t)255); - result[15U] = (uint8_t)(v.elements[(size_t)8U + (size_t)2U] & (int16_t)255); - result[16U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)2U] >> 8U | - (v.elements[(size_t)8U + (size_t)3U] & (int16_t)15) << 4U); - result[17U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)3U] >> 4U & (int16_t)255); - result[18U] = (uint8_t)(v.elements[(size_t)8U + (size_t)4U] & (int16_t)255); - result[19U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)4U] >> 8U | - (v.elements[(size_t)8U + (size_t)5U] & (int16_t)15) << 4U); - result[20U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)5U] >> 4U & (int16_t)255); - result[21U] = (uint8_t)(v.elements[(size_t)8U + (size_t)6U] & (int16_t)255); - result[22U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)6U] >> 8U | - (v.elements[(size_t)8U + (size_t)7U] & (int16_t)15) << 4U); - result[23U] = - (uint8_t)(v.elements[(size_t)8U + (size_t)7U] >> 4U & (int16_t)255); + result[0U] = r0_2.fst; + result[1U] = r0_2.snd; + result[2U] = r0_2.thd; + result[3U] = r3_5.fst; + result[4U] = r3_5.snd; + result[5U] = r3_5.thd; + result[6U] = r6_8.fst; + result[7U] = r6_8.snd; + result[8U] = r6_8.thd; + result[9U] = r9_11.fst; + result[10U] = r9_11.snd; + result[11U] = r9_11.thd; + result[12U] = r12_14.fst; + result[13U] = r12_14.snd; + result[14U] = r12_14.thd; + result[15U] = r15_17.fst; + result[16U] = r15_17.snd; + result[17U] = r15_17.thd; + result[18U] = r18_20.fst; + result[19U] = r18_20.snd; + result[20U] = r18_20.thd; + result[21U] = r21_23.fst; + result[22U] = r21_23.snd; + result[23U] = r21_23.thd; memcpy(ret, result, (size_t)24U * sizeof(uint8_t)); } @@ -2209,74 +2257,101 @@ libcrux_ml_kem_vector_portable___libcrux_ml_kem__vector__traits__Operations_for_ memcpy(ret, ret0, (size_t)24U * sizeof(uint8_t)); } -static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector -libcrux_ml_kem_vector_portable_serialize_deserialize_12(Eurydice_slice bytes) { - libcrux_ml_kem_vector_portable_vector_type_PortableVector re = - libcrux_ml_kem_vector_portable_vector_type_zero(); +typedef struct K___int16_t_int16_t_s { + int16_t fst; + int16_t snd; +} K___int16_t_int16_t; + +static KRML_MUSTINLINE K___int16_t_int16_t +libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice bytes) { int16_t byte0 = (int16_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t *, uint8_t); int16_t byte1 = (int16_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t *, uint8_t); int16_t byte2 = (int16_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t *, uint8_t); - int16_t byte3 = (int16_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, - uint8_t *, uint8_t); - int16_t byte4 = (int16_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, - uint8_t *, uint8_t); - int16_t byte5 = (int16_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, - uint8_t *, uint8_t); - int16_t byte6 = (int16_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, - uint8_t *, uint8_t); - int16_t byte7 = (int16_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, - uint8_t *, uint8_t); - int16_t byte8 = (int16_t)Eurydice_slice_index(bytes, (size_t)8U, uint8_t, - uint8_t *, uint8_t); - int16_t byte9 = (int16_t)Eurydice_slice_index(bytes, (size_t)9U, uint8_t, - uint8_t *, uint8_t); - int16_t byte10 = (int16_t)Eurydice_slice_index(bytes, (size_t)10U, uint8_t, - uint8_t *, uint8_t); - int16_t byte11 = (int16_t)Eurydice_slice_index(bytes, (size_t)11U, uint8_t, - uint8_t *, uint8_t); - re.elements[0U] = (byte1 & (int16_t)15) << 8U | (byte0 & (int16_t)255); - re.elements[1U] = byte2 << 4U | (byte1 >> 4U & (int16_t)15); - re.elements[2U] = (byte4 & (int16_t)15) << 8U | (byte3 & (int16_t)255); - re.elements[3U] = byte5 << 4U | (byte4 >> 4U & (int16_t)15); - re.elements[4U] = (byte7 & (int16_t)15) << 8U | (byte6 & (int16_t)255); - re.elements[5U] = byte8 << 4U | (byte7 >> 4U & (int16_t)15); - re.elements[6U] = (byte10 & (int16_t)15) << 8U | (byte9 & (int16_t)255); - re.elements[7U] = byte11 << 4U | (byte10 >> 4U & (int16_t)15); - int16_t byte12 = (int16_t)Eurydice_slice_index(bytes, (size_t)12U, uint8_t, - uint8_t *, uint8_t); - int16_t byte13 = (int16_t)Eurydice_slice_index(bytes, (size_t)13U, uint8_t, - uint8_t *, uint8_t); - int16_t byte14 = (int16_t)Eurydice_slice_index(bytes, (size_t)14U, uint8_t, - uint8_t *, uint8_t); - int16_t byte15 = (int16_t)Eurydice_slice_index(bytes, (size_t)15U, uint8_t, - uint8_t *, uint8_t); - int16_t byte16 = (int16_t)Eurydice_slice_index(bytes, (size_t)16U, uint8_t, - uint8_t *, uint8_t); - int16_t byte17 = (int16_t)Eurydice_slice_index(bytes, (size_t)17U, uint8_t, - uint8_t *, uint8_t); - int16_t byte18 = (int16_t)Eurydice_slice_index(bytes, (size_t)18U, uint8_t, - uint8_t *, uint8_t); - int16_t byte19 = (int16_t)Eurydice_slice_index(bytes, (size_t)19U, uint8_t, - uint8_t *, uint8_t); - int16_t byte20 = (int16_t)Eurydice_slice_index(bytes, (size_t)20U, uint8_t, - uint8_t *, uint8_t); - int16_t byte21 = (int16_t)Eurydice_slice_index(bytes, (size_t)21U, uint8_t, - uint8_t *, uint8_t); - int16_t byte22 = (int16_t)Eurydice_slice_index(bytes, (size_t)22U, uint8_t, - uint8_t *, uint8_t); - int16_t byte23 = (int16_t)Eurydice_slice_index(bytes, (size_t)23U, uint8_t, - uint8_t *, uint8_t); - re.elements[8U] = (byte13 & (int16_t)15) << 8U | (byte12 & (int16_t)255); - re.elements[9U] = byte14 << 4U | (byte13 >> 4U & (int16_t)15); - re.elements[10U] = (byte16 & (int16_t)15) << 8U | (byte15 & (int16_t)255); - re.elements[11U] = byte17 << 4U | (byte16 >> 4U & (int16_t)15); - re.elements[12U] = (byte19 & (int16_t)15) << 8U | (byte18 & (int16_t)255); - re.elements[13U] = byte20 << 4U | (byte19 >> 4U & (int16_t)15); - re.elements[14U] = (byte22 & (int16_t)15) << 8U | (byte21 & (int16_t)255); - re.elements[15U] = byte23 << 4U | (byte22 >> 4U & (int16_t)15); + int16_t r0 = (byte1 & (int16_t)15) << 8U | (byte0 & (int16_t)255); + int16_t r1 = byte2 << 4U | (byte1 >> 4U & (int16_t)15); + return (CLITERAL(K___int16_t_int16_t){.fst = r0, .snd = r1}); +} + +static KRML_MUSTINLINE libcrux_ml_kem_vector_portable_vector_type_PortableVector +libcrux_ml_kem_vector_portable_serialize_deserialize_12(Eurydice_slice bytes) { + K___int16_t_int16_t v0_1 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = (size_t)3U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t v2_3 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)3U, .end = (size_t)6U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t v4_5 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)6U, .end = (size_t)9U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t v6_7 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice(bytes, + (CLITERAL(core_ops_range_Range__size_t){ + .start = (size_t)9U, .end = (size_t)12U}), + uint8_t, core_ops_range_Range__size_t, + Eurydice_slice)); + K___int16_t_int16_t v8_9 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice( + bytes, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)12U, + .end = (size_t)15U}), + uint8_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___int16_t_int16_t v10_11 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice( + bytes, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)15U, + .end = (size_t)18U}), + uint8_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___int16_t_int16_t v12_13 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice( + bytes, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)18U, + .end = (size_t)21U}), + uint8_t, core_ops_range_Range__size_t, Eurydice_slice)); + K___int16_t_int16_t v14_15 = + libcrux_ml_kem_vector_portable_serialize_deserialize_12_int( + Eurydice_slice_subslice( + bytes, + (CLITERAL(core_ops_range_Range__size_t){.start = (size_t)21U, + .end = (size_t)24U}), + uint8_t, core_ops_range_Range__size_t, Eurydice_slice)); + libcrux_ml_kem_vector_portable_vector_type_PortableVector re = + libcrux_ml_kem_vector_portable_vector_type_zero(); + re.elements[0U] = v0_1.fst; + re.elements[1U] = v0_1.snd; + re.elements[2U] = v2_3.fst; + re.elements[3U] = v2_3.snd; + re.elements[4U] = v4_5.fst; + re.elements[5U] = v4_5.snd; + re.elements[6U] = v6_7.fst; + re.elements[7U] = v6_7.snd; + re.elements[8U] = v8_9.fst; + re.elements[9U] = v8_9.snd; + re.elements[10U] = v10_11.fst; + re.elements[11U] = v10_11.snd; + re.elements[12U] = v12_13.fst; + re.elements[13U] = v12_13.snd; + re.elements[14U] = v14_15.fst; + re.elements[15U] = v14_15.snd; return re; } @@ -3328,16 +3403,14 @@ libcrux_ml_kem_ind_cpa_decrypt__libcrux_ml_kem_vector_portable_vector_type_Porta static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____G___3size_t( Eurydice_slice input, uint8_t ret[64U]) { - uint8_t digest[64U] = {0U}; - libcrux_sha3_portable_sha512( - Eurydice_array_to_slice((size_t)64U, digest, uint8_t, Eurydice_slice), - input); - memcpy(ret, digest, (size_t)64U * sizeof(uint8_t)); + uint8_t ret0[64U]; + libcrux_ml_kem_hash_functions_portable_G(input, ret0); + memcpy(ret, ret0, (size_t)64U * sizeof(uint8_t)); } static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____PRF___3size_t_32size_t( - Eurydice_slice input, uint8_t ret[32U]) { +libcrux_ml_kem_hash_functions_portable_PRF___32size_t(Eurydice_slice input, + uint8_t ret[32U]) { uint8_t digest[32U] = {0U}; libcrux_sha3_portable_shake256( Eurydice_array_to_slice((size_t)32U, digest, uint8_t, Eurydice_slice), @@ -3345,6 +3418,14 @@ libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K_ memcpy(ret, digest, (size_t)32U * sizeof(uint8_t)); } +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____PRF___3size_t_32size_t( + Eurydice_slice input, uint8_t ret[32U]) { + uint8_t ret0[32U]; + libcrux_ml_kem_hash_functions_portable_PRF___32size_t(input, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} + static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_serialize_deserialize_ring_elements_reduced_closure__libcrux_ml_kem_vector_portable_vector_type_PortableVector_1152size_t_3size_t( size_t _i) { @@ -3444,22 +3525,23 @@ typedef struct libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t shake128_state[3U]; } libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t; -static KRML_MUSTINLINE libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t -libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____shake128_init_absorb___3size_t( - uint8_t input[3U][34U]) { - libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t state[3U]; +static KRML_MUSTINLINE + libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t + libcrux_ml_kem_hash_functions_portable_shake128_init_absorb___3size_t( + uint8_t input[3U][34U]) { + libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t shake128_state[3U]; for (size_t i = (size_t)0U; i < (size_t)3U; i++) { - state[i] = libcrux_sha3_portable_incremental_shake128_init(); + shake128_state[i] = libcrux_sha3_portable_incremental_shake128_init(); } for (size_t i = (size_t)0U; i < (size_t)3U; i++) { size_t i0 = i; libcrux_sha3_portable_incremental_shake128_absorb_final( - &state[i0], Eurydice_array_to_slice((size_t)34U, input[i0], uint8_t, - Eurydice_slice)); + &shake128_state[i0], Eurydice_array_to_slice((size_t)34U, input[i0], + uint8_t, Eurydice_slice)); } libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t uu____0[3U]; memcpy( - uu____0, state, + uu____0, shake128_state, (size_t)3U * sizeof(libcrux_sha3_generic_keccak_KeccakState__uint64_t__1size_t)); libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t lit; @@ -3470,21 +3552,40 @@ libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K_ return lit; } +static KRML_MUSTINLINE libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t +libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____shake128_init_absorb___3size_t( + uint8_t input[3U][34U]) { + uint8_t uu____0[3U][34U]; + memcpy(uu____0, input, (size_t)3U * sizeof(uint8_t[34U])); + return libcrux_ml_kem_hash_functions_portable_shake128_init_absorb___3size_t( + uu____0); +} + static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____shake128_squeeze_three_blocks___3size_t( - libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t *self, +libcrux_ml_kem_hash_functions_portable_shake128_squeeze_three_blocks___3size_t( + libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t *st, uint8_t ret[3U][504U]) { uint8_t out[3U][504U] = {{0U}}; for (size_t i = (size_t)0U; i < (size_t)3U; i++) { size_t i0 = i; libcrux_sha3_portable_incremental_shake128_squeeze_first_three_blocks( - &self->shake128_state[i0], + &st->shake128_state[i0], Eurydice_array_to_slice((size_t)504U, out[i0], uint8_t, Eurydice_slice)); } memcpy(ret, out, (size_t)3U * sizeof(uint8_t[504U])); } +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____shake128_squeeze_three_blocks___3size_t( + libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t *self, + uint8_t ret[3U][504U]) { + uint8_t ret0[3U][504U]; + libcrux_ml_kem_hash_functions_portable_shake128_squeeze_three_blocks___3size_t( + self, ret0); + memcpy(ret, ret0, (size_t)3U * sizeof(uint8_t[504U])); +} + static KRML_MUSTINLINE bool libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_vector_portable_vector_type_PortableVector_3size_t_504size_t( uint8_t randomness[3U][504U], size_t *sampled_coefficients, @@ -3530,20 +3631,30 @@ libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_ve } static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____shake128_squeeze_block___3size_t( - libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t *self, +libcrux_ml_kem_hash_functions_portable_shake128_squeeze_block___3size_t( + libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t *st, uint8_t ret[3U][168U]) { uint8_t out[3U][168U] = {{0U}}; for (size_t i = (size_t)0U; i < (size_t)3U; i++) { size_t i0 = i; libcrux_sha3_portable_incremental_shake128_squeeze_next_block( - &self->shake128_state[i0], + &st->shake128_state[i0], Eurydice_array_to_slice((size_t)168U, out[i0], uint8_t, Eurydice_slice)); } memcpy(ret, out, (size_t)3U * sizeof(uint8_t[168U])); } +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____shake128_squeeze_block___3size_t( + libcrux_ml_kem_hash_functions_portable_PortableHash____3size_t *self, + uint8_t ret[3U][168U]) { + uint8_t ret0[3U][168U]; + libcrux_ml_kem_hash_functions_portable_shake128_squeeze_block___3size_t(self, + ret0); + memcpy(ret, ret0, (size_t)3U * sizeof(uint8_t[168U])); +} + static KRML_MUSTINLINE bool libcrux_ml_kem_sampling_sample_from_uniform_distribution_next__libcrux_ml_kem_vector_portable_vector_type_PortableVector_3size_t_168size_t( uint8_t randomness[3U][168U], size_t *sampled_coefficients, @@ -3754,7 +3865,7 @@ libcrux_ml_kem_ind_cpa_sample_vector_cbd_then_ntt_closure__libcrux_ml_kem_vector } static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____PRFxN___3size_t_128size_t( +libcrux_ml_kem_hash_functions_portable_PRFxN___3size_t_128size_t( uint8_t (*input)[33U], uint8_t ret[3U][128U]) { uint8_t out[3U][128U] = {{0U}}; for (size_t i = (size_t)0U; i < (size_t)3U; i++) { @@ -3767,6 +3878,14 @@ libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K_ memcpy(ret, out, (size_t)3U * sizeof(uint8_t[128U])); } +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____PRFxN___3size_t_128size_t( + uint8_t (*input)[33U], uint8_t ret[3U][128U]) { + uint8_t ret0[3U][128U]; + libcrux_ml_kem_hash_functions_portable_PRFxN___3size_t_128size_t(input, ret0); + memcpy(ret, ret0, (size_t)3U * sizeof(uint8_t[128U])); +} + static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_sampling_sample_from_binomial_distribution_2__libcrux_ml_kem_vector_portable_vector_type_PortableVector( @@ -4030,8 +4149,8 @@ static KRML_MUSTINLINE } static KRML_MUSTINLINE void -libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____PRF___3size_t_128size_t( - Eurydice_slice input, uint8_t ret[128U]) { +libcrux_ml_kem_hash_functions_portable_PRF___128size_t(Eurydice_slice input, + uint8_t ret[128U]) { uint8_t digest[128U] = {0U}; libcrux_sha3_portable_shake256( Eurydice_array_to_slice((size_t)128U, digest, uint8_t, Eurydice_slice), @@ -4039,6 +4158,14 @@ libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K_ memcpy(ret, digest, (size_t)128U * sizeof(uint8_t)); } +static KRML_MUSTINLINE void +libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____PRF___3size_t_128size_t( + Eurydice_slice input, uint8_t ret[128U]) { + uint8_t ret0[128U]; + libcrux_ml_kem_hash_functions_portable_PRF___128size_t(input, ret0); + memcpy(ret, ret0, (size_t)128U * sizeof(uint8_t)); +} + static inline libcrux_ml_kem_polynomial_PolynomialRingElement__libcrux_ml_kem_vector_portable_vector_type_PortableVector libcrux_ml_kem_matrix_compute_vector_u_closure__libcrux_ml_kem_vector_portable_vector_type_PortableVector_3size_t( size_t _i) { @@ -4871,11 +4998,9 @@ libcrux_ml_kem_ind_cca___libcrux_ml_kem__ind_cca__Variant_for_libcrux_ml_kem__in static KRML_MUSTINLINE void libcrux_ml_kem_hash_functions_portable___libcrux_ml_kem__hash_functions__Hash_K__for_libcrux_ml_kem__hash_functions__portable__PortableHash_K____H___3size_t( Eurydice_slice input, uint8_t ret[32U]) { - uint8_t digest[32U] = {0U}; - libcrux_sha3_portable_sha256( - Eurydice_array_to_slice((size_t)32U, digest, uint8_t, Eurydice_slice), - input); - memcpy(ret, digest, (size_t)32U * sizeof(uint8_t)); + uint8_t ret0[32U]; + libcrux_ml_kem_hash_functions_portable_H(input, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } static inline K___libcrux_ml_kem_types_MlKemCiphertext___1088size_t___uint8_t_32size_t_ diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h index 372cc7359..a348595dd 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h @@ -2,7 +2,7 @@ This file was generated by KaRaMeL KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../cg.yaml -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: - 07b5a210 KaRaMeL version: f13006e2 + 07b5a210 KaRaMeL version: 65aab550 */ #ifndef __libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/cg/libcrux_sha3_portable.h b/libcrux-ml-kem/cg/libcrux_sha3_portable.h index bc699c56e..d2428ffc0 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h @@ -2,7 +2,7 @@ This file was generated by KaRaMeL KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../cg.yaml -funroll-loops 0 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: - 07b5a210 KaRaMeL version: f13006e2 + 07b5a210 KaRaMeL version: 65aab550 */ #ifndef __libcrux_sha3_portable_H