From 6758f5c74edc70520635665f34082150e426b97f Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Tue, 24 Sep 2024 14:53:30 +0000 Subject: [PATCH] pinned versions --- libcrux-ml-kem/c/code_gen.txt | 8 +- libcrux-ml-kem/c/eurydice_glue.h | 18 + libcrux-ml-kem/c/internal/libcrux_core.h | 43 +- .../c/internal/libcrux_mlkem_avx2.h | 8 +- .../c/internal/libcrux_mlkem_portable.h | 8 +- libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h | 8 +- .../c/internal/libcrux_sha3_internal.h | 136 +++--- libcrux-ml-kem/c/libcrux_core.c | 50 ++- libcrux-ml-kem/c/libcrux_core.h | 15 +- libcrux-ml-kem/c/libcrux_mlkem1024.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c | 8 +- libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem1024_portable.c | 8 +- libcrux-ml-kem/c/libcrux_mlkem1024_portable.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem512.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem512_avx2.c | 8 +- libcrux-ml-kem/c/libcrux_mlkem512_avx2.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem512_portable.c | 8 +- libcrux-ml-kem/c/libcrux_mlkem512_portable.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem768.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem768_avx2.c | 8 +- libcrux-ml-kem/c/libcrux_mlkem768_avx2.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem768_portable.c | 8 +- libcrux-ml-kem/c/libcrux_mlkem768_portable.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem_avx2.c | 401 +++++++++--------- libcrux-ml-kem/c/libcrux_mlkem_avx2.h | 8 +- libcrux-ml-kem/c/libcrux_mlkem_portable.c | 395 ++++++++--------- libcrux-ml-kem/c/libcrux_mlkem_portable.h | 8 +- libcrux-ml-kem/c/libcrux_sha3.h | 8 +- libcrux-ml-kem/c/libcrux_sha3_avx2.c | 20 +- libcrux-ml-kem/c/libcrux_sha3_avx2.h | 8 +- libcrux-ml-kem/c/libcrux_sha3_internal.h | 48 +-- libcrux-ml-kem/c/libcrux_sha3_neon.c | 8 +- libcrux-ml-kem/c/libcrux_sha3_neon.h | 8 +- libcrux-ml-kem/cg/code_gen.txt | 6 +- libcrux-ml-kem/cg/libcrux_core.h | 6 +- libcrux-ml-kem/cg/libcrux_ct_ops.h | 6 +- libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h | 6 +- .../cg/libcrux_mlkem768_avx2_types.h | 6 +- libcrux-ml-kem/cg/libcrux_mlkem768_portable.h | 6 +- .../cg/libcrux_mlkem768_portable_types.h | 6 +- libcrux-ml-kem/cg/libcrux_sha3_avx2.h | 6 +- libcrux-ml-kem/cg/libcrux_sha3_portable.h | 6 +- 43 files changed, 716 insertions(+), 664 deletions(-) diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt index 21d1a541d..e4e28910d 100644 --- a/libcrux-ml-kem/c/code_gen.txt +++ b/libcrux-ml-kem/c/code_gen.txt @@ -1,6 +1,6 @@ This code was generated with the following revisions: -Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d -Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 -Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 +Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 +Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac +Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd -Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d +Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 diff --git a/libcrux-ml-kem/c/eurydice_glue.h b/libcrux-ml-kem/c/eurydice_glue.h index 660918c54..ad026b9e1 100644 --- a/libcrux-ml-kem/c/eurydice_glue.h +++ b/libcrux-ml-kem/c/eurydice_glue.h @@ -18,6 +18,13 @@ extern "C" { #include "krml/lowstar_endianness.h" #define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e) +#define EURYDICE_ASSERT(test, msg) \ + do { \ + if (!(test)) { \ + fprintf(stderr, "assertion \"%s\" failed: file \"%s\", line %d\n", msg, \ + __FILE__, __LINE__); \ + } \ + } while (0) // SLICES, ARRAYS, ETC. @@ -130,6 +137,10 @@ static inline void core_num__u32_8__to_be_bytes(uint32_t src, uint8_t dst[4]) { memcpy(dst, &x, 4); } +static inline void core_num__u32_8__to_le_bytes(uint32_t src, uint8_t dst[4]) { + store32_le(dst, src); +} + static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) { return load32_le(buf); } @@ -137,6 +148,7 @@ static inline uint32_t core_num__u32_8__from_le_bytes(uint8_t buf[4]) { static inline void core_num__u64_9__to_le_bytes(uint64_t v, uint8_t buf[8]) { store64_le(buf, v); } + static inline uint64_t core_num__u64_9__from_le_bytes(uint8_t buf[8]) { return load64_le(buf); } @@ -188,6 +200,9 @@ static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) { static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) { return (*p) >> v; } +static inline uint32_t Eurydice_min_u32(uint32_t x, uint32_t y) { + return x < y ? x : y; +} #define core_num_nonzero_private_NonZeroUsizeInner size_t static inline core_num_nonzero_private_NonZeroUsizeInner @@ -210,6 +225,9 @@ core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__N #define core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next \ Eurydice_range_iter_next +#define core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next \ + Eurydice_range_iter_next + // See note in karamel/lib/Inlining.ml if you change this #define Eurydice_into_iter(x, t, _ret_t) (x) #define core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter \ diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h index ea0d66fb8..4dc60c6c7 100644 --- a/libcrux-ml-kem/c/internal/libcrux_core.h +++ b/libcrux-ml-kem/c/internal/libcrux_core.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __internal_libcrux_core_H @@ -291,14 +291,15 @@ typedef struct core_result_Result_00_s { } core_result_Result_00; /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[32size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_33(core_result_Result_00 self, uint8_t ret[32U]); +void core_result_unwrap_26_33(core_result_Result_00 self, uint8_t ret[32U]); /** Pad the `slice` with `0`s at the end. @@ -382,14 +383,15 @@ typedef struct core_result_Result_6f_s { } core_result_Result_6f; /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[24size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_76(core_result_Result_6f self, uint8_t ret[24U]); +void core_result_unwrap_26_76(core_result_Result_6f self, uint8_t ret[24U]); /** A monomorphic instance of core.result.Result @@ -405,14 +407,15 @@ typedef struct core_result_Result_7a_s { } core_result_Result_7a; /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[20size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_ea(core_result_Result_7a self, uint8_t ret[20U]); +void core_result_unwrap_26_ea(core_result_Result_7a self, uint8_t ret[20U]); /** A monomorphic instance of core.result.Result @@ -428,14 +431,15 @@ typedef struct core_result_Result_cd_s { } core_result_Result_cd; /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[10size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_07(core_result_Result_cd self, uint8_t ret[10U]); +void core_result_unwrap_26_07(core_result_Result_cd self, uint8_t ret[10U]); /** A monomorphic instance of core.result.Result @@ -451,14 +455,15 @@ typedef struct core_result_Result_c0_s { } core_result_Result_c0; /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types int16_t[16size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_30(core_result_Result_c0 self, int16_t ret[16U]); +void core_result_unwrap_26_30(core_result_Result_c0 self, int16_t ret[16U]); typedef struct Eurydice_slice_uint8_t_4size_t__x2_s { Eurydice_slice fst[4U]; diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h index faf1c9b68..edc4170ea 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __internal_libcrux_mlkem_avx2_H diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h index 7d3aec1df..be78cb001 100644 --- a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __internal_libcrux_mlkem_portable_H diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h index 653268abf..354aca0c1 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __internal_libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h index 924fca293..513206ab2 100644 --- a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __internal_libcrux_sha3_internal_H @@ -29,7 +29,7 @@ typedef libcrux_sha3_generic_keccak_KeccakState_48 */ static KRML_MUSTINLINE libcrux_sha3_generic_keccak_KeccakState_48 libcrux_sha3_portable_incremental_shake128_init(void) { - return libcrux_sha3_generic_keccak_new_1e_cf(); + return libcrux_sha3_generic_keccak_new_89_cf(); } /** @@ -207,7 +207,7 @@ libcrux_sha3_portable_incremental_shake256_absorb_final( */ static KRML_MUSTINLINE libcrux_sha3_generic_keccak_KeccakState_48 libcrux_sha3_portable_incremental_shake256_init(void) { - return libcrux_sha3_generic_keccak_new_1e_cf(); + return libcrux_sha3_generic_keccak_new_89_cf(); } /** @@ -258,16 +258,16 @@ typedef libcrux_sha3_generic_keccak_KeccakXofState_4f */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.fill_buffer_9d +A monomorphic instance of libcrux_sha3.generic_keccak.fill_buffer_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 136 */ -static inline size_t libcrux_sha3_generic_keccak_fill_buffer_9d_15( +static inline size_t libcrux_sha3_generic_keccak_fill_buffer_8b_15( libcrux_sha3_generic_keccak_KeccakXofState_4f *self, Eurydice_slice inputs[1U]) { size_t input_len = Eurydice_slice_len(inputs[0U], uint8_t); @@ -292,16 +292,16 @@ static inline size_t libcrux_sha3_generic_keccak_fill_buffer_9d_15( /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_full_9d +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_full_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 136 */ -static inline size_t libcrux_sha3_generic_keccak_absorb_full_9d_7a( +static inline size_t libcrux_sha3_generic_keccak_absorb_full_8b_7a( libcrux_sha3_generic_keccak_KeccakXofState_4f *self, Eurydice_slice inputs[1U]) { libcrux_sha3_generic_keccak_KeccakXofState_4f *uu____0 = self; @@ -309,7 +309,7 @@ static inline size_t libcrux_sha3_generic_keccak_absorb_full_9d_7a( Eurydice_slice copy_of_inputs0[1U]; memcpy(copy_of_inputs0, inputs, (size_t)1U * sizeof(Eurydice_slice)); size_t input_consumed = - libcrux_sha3_generic_keccak_fill_buffer_9d_15(uu____0, copy_of_inputs0); + libcrux_sha3_generic_keccak_fill_buffer_8b_15(uu____0, copy_of_inputs0); if (input_consumed > (size_t)0U) { Eurydice_slice borrowed[1U]; { @@ -362,16 +362,16 @@ static inline size_t libcrux_sha3_generic_keccak_absorb_full_9d_7a( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_9d +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 136 */ -static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_9d_45( +static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_8b_45( libcrux_sha3_generic_keccak_KeccakXofState_4f *self, Eurydice_slice inputs[1U]) { libcrux_sha3_generic_keccak_KeccakXofState_4f *uu____0 = self; @@ -379,7 +379,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_9d_45( Eurydice_slice copy_of_inputs[1U]; memcpy(copy_of_inputs, inputs, (size_t)1U * sizeof(Eurydice_slice)); size_t input_remainder_len = - libcrux_sha3_generic_keccak_absorb_full_9d_7a(uu____0, copy_of_inputs); + libcrux_sha3_generic_keccak_absorb_full_8b_7a(uu____0, copy_of_inputs); if (input_remainder_len > (size_t)0U) { size_t input_len = Eurydice_slice_len(inputs[0U], uint8_t); { @@ -408,7 +408,7 @@ libcrux_sha3::portable::incremental::Shake256Absorb)#2} static inline void libcrux_sha3_portable_incremental_absorb_7d( libcrux_sha3_generic_keccak_KeccakXofState_4f *self, Eurydice_slice input) { Eurydice_slice buf[1U] = {input}; - libcrux_sha3_generic_keccak_absorb_9d_45(self, buf); + libcrux_sha3_generic_keccak_absorb_8b_45(self, buf); } typedef libcrux_sha3_generic_keccak_KeccakXofState_4f @@ -422,17 +422,17 @@ typedef libcrux_sha3_generic_keccak_KeccakXofState_4f */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_9d +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 136 - DELIMITER= 31 */ -static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_final_9d_b6( +static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_final_8b_b6( libcrux_sha3_generic_keccak_KeccakXofState_4f *self, Eurydice_slice inputs[1U]) { libcrux_sha3_generic_keccak_KeccakXofState_4f *uu____0 = self; @@ -440,7 +440,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_final_9d_b6( Eurydice_slice copy_of_inputs[1U]; memcpy(copy_of_inputs, inputs, (size_t)1U * sizeof(Eurydice_slice)); size_t input_remainder_len = - libcrux_sha3_generic_keccak_absorb_full_9d_7a(uu____0, copy_of_inputs); + libcrux_sha3_generic_keccak_absorb_full_8b_7a(uu____0, copy_of_inputs); size_t input_len = Eurydice_slice_len(inputs[0U], uint8_t); uint8_t blocks[1U][200U] = {{0U}}; { @@ -487,7 +487,7 @@ static inline libcrux_sha3_generic_keccak_KeccakXofState_4f libcrux_sha3_portable_incremental_absorb_final_7d( libcrux_sha3_generic_keccak_KeccakXofState_4f self, Eurydice_slice input) { Eurydice_slice buf[1U] = {input}; - libcrux_sha3_generic_keccak_absorb_final_9d_b6(&self, buf); + libcrux_sha3_generic_keccak_absorb_final_8b_b6(&self, buf); return self; } @@ -496,16 +496,16 @@ libcrux_sha3_portable_incremental_absorb_final_7d( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.zero_block_9d +A monomorphic instance of libcrux_sha3.generic_keccak.zero_block_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 136 */ -static inline void libcrux_sha3_generic_keccak_zero_block_9d_5e( +static inline void libcrux_sha3_generic_keccak_zero_block_8b_5e( uint8_t ret[136U]) { ret[0U] = 0U; ret[1U] = 0U; @@ -650,21 +650,21 @@ static inline void libcrux_sha3_generic_keccak_zero_block_9d_5e( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.new_9d +A monomorphic instance of libcrux_sha3.generic_keccak.new_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 136 */ static inline libcrux_sha3_generic_keccak_KeccakXofState_4f -libcrux_sha3_generic_keccak_new_9d_47(void) { +libcrux_sha3_generic_keccak_new_8b_47(void) { libcrux_sha3_generic_keccak_KeccakXofState_4f lit; - lit.inner = libcrux_sha3_generic_keccak_new_1e_cf(); + lit.inner = libcrux_sha3_generic_keccak_new_89_cf(); uint8_t ret[136U]; - libcrux_sha3_generic_keccak_zero_block_9d_5e(ret); + libcrux_sha3_generic_keccak_zero_block_8b_5e(ret); memcpy(lit.buf[0U], ret, (size_t)136U * sizeof(uint8_t)); lit.buf_len = (size_t)0U; lit.sponge = false; @@ -681,7 +681,7 @@ libcrux_sha3::portable::incremental::Shake256Absorb)#2} */ static inline libcrux_sha3_generic_keccak_KeccakXofState_4f libcrux_sha3_portable_incremental_new_7d(void) { - return libcrux_sha3_generic_keccak_new_9d_47(); + return libcrux_sha3_generic_keccak_new_8b_47(); } /** @@ -712,16 +712,16 @@ typedef libcrux_sha3_generic_keccak_KeccakXofState_78 */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.fill_buffer_9d +A monomorphic instance of libcrux_sha3.generic_keccak.fill_buffer_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 168 */ -static inline size_t libcrux_sha3_generic_keccak_fill_buffer_9d_150( +static inline size_t libcrux_sha3_generic_keccak_fill_buffer_8b_150( libcrux_sha3_generic_keccak_KeccakXofState_78 *self, Eurydice_slice inputs[1U]) { size_t input_len = Eurydice_slice_len(inputs[0U], uint8_t); @@ -746,16 +746,16 @@ static inline size_t libcrux_sha3_generic_keccak_fill_buffer_9d_150( /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_full_9d +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_full_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 168 */ -static inline size_t libcrux_sha3_generic_keccak_absorb_full_9d_7a0( +static inline size_t libcrux_sha3_generic_keccak_absorb_full_8b_7a0( libcrux_sha3_generic_keccak_KeccakXofState_78 *self, Eurydice_slice inputs[1U]) { libcrux_sha3_generic_keccak_KeccakXofState_78 *uu____0 = self; @@ -763,7 +763,7 @@ static inline size_t libcrux_sha3_generic_keccak_absorb_full_9d_7a0( Eurydice_slice copy_of_inputs0[1U]; memcpy(copy_of_inputs0, inputs, (size_t)1U * sizeof(Eurydice_slice)); size_t input_consumed = - libcrux_sha3_generic_keccak_fill_buffer_9d_150(uu____0, copy_of_inputs0); + libcrux_sha3_generic_keccak_fill_buffer_8b_150(uu____0, copy_of_inputs0); if (input_consumed > (size_t)0U) { Eurydice_slice borrowed[1U]; { @@ -816,16 +816,16 @@ static inline size_t libcrux_sha3_generic_keccak_absorb_full_9d_7a0( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_9d +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 168 */ -static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_9d_450( +static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_8b_450( libcrux_sha3_generic_keccak_KeccakXofState_78 *self, Eurydice_slice inputs[1U]) { libcrux_sha3_generic_keccak_KeccakXofState_78 *uu____0 = self; @@ -833,7 +833,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_9d_450( Eurydice_slice copy_of_inputs[1U]; memcpy(copy_of_inputs, inputs, (size_t)1U * sizeof(Eurydice_slice)); size_t input_remainder_len = - libcrux_sha3_generic_keccak_absorb_full_9d_7a0(uu____0, copy_of_inputs); + libcrux_sha3_generic_keccak_absorb_full_8b_7a0(uu____0, copy_of_inputs); if (input_remainder_len > (size_t)0U) { size_t input_len = Eurydice_slice_len(inputs[0U], uint8_t); { @@ -859,7 +859,7 @@ libcrux_sha3::portable::incremental::Shake128Absorb)} static inline void libcrux_sha3_portable_incremental_absorb_1c( libcrux_sha3_generic_keccak_KeccakXofState_78 *self, Eurydice_slice input) { Eurydice_slice buf[1U] = {input}; - libcrux_sha3_generic_keccak_absorb_9d_450(self, buf); + libcrux_sha3_generic_keccak_absorb_8b_450(self, buf); } typedef libcrux_sha3_generic_keccak_KeccakXofState_78 @@ -873,17 +873,17 @@ typedef libcrux_sha3_generic_keccak_KeccakXofState_78 */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_9d +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 168 - DELIMITER= 31 */ -static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_final_9d_b60( +static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_final_8b_b60( libcrux_sha3_generic_keccak_KeccakXofState_78 *self, Eurydice_slice inputs[1U]) { libcrux_sha3_generic_keccak_KeccakXofState_78 *uu____0 = self; @@ -891,7 +891,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_absorb_final_9d_b60( Eurydice_slice copy_of_inputs[1U]; memcpy(copy_of_inputs, inputs, (size_t)1U * sizeof(Eurydice_slice)); size_t input_remainder_len = - libcrux_sha3_generic_keccak_absorb_full_9d_7a0(uu____0, copy_of_inputs); + libcrux_sha3_generic_keccak_absorb_full_8b_7a0(uu____0, copy_of_inputs); size_t input_len = Eurydice_slice_len(inputs[0U], uint8_t); uint8_t blocks[1U][200U] = {{0U}}; { @@ -935,7 +935,7 @@ static inline libcrux_sha3_generic_keccak_KeccakXofState_78 libcrux_sha3_portable_incremental_absorb_final_1c( libcrux_sha3_generic_keccak_KeccakXofState_78 self, Eurydice_slice input) { Eurydice_slice buf[1U] = {input}; - libcrux_sha3_generic_keccak_absorb_final_9d_b60(&self, buf); + libcrux_sha3_generic_keccak_absorb_final_8b_b60(&self, buf); return self; } @@ -944,16 +944,16 @@ libcrux_sha3_portable_incremental_absorb_final_1c( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.zero_block_9d +A monomorphic instance of libcrux_sha3.generic_keccak.zero_block_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 168 */ -static inline void libcrux_sha3_generic_keccak_zero_block_9d_5e0( +static inline void libcrux_sha3_generic_keccak_zero_block_8b_5e0( uint8_t ret[168U]) { ret[0U] = 0U; ret[1U] = 0U; @@ -1130,21 +1130,21 @@ static inline void libcrux_sha3_generic_keccak_zero_block_9d_5e0( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.new_9d +A monomorphic instance of libcrux_sha3.generic_keccak.new_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 168 */ static inline libcrux_sha3_generic_keccak_KeccakXofState_78 -libcrux_sha3_generic_keccak_new_9d_470(void) { +libcrux_sha3_generic_keccak_new_8b_470(void) { libcrux_sha3_generic_keccak_KeccakXofState_78 lit; - lit.inner = libcrux_sha3_generic_keccak_new_1e_cf(); + lit.inner = libcrux_sha3_generic_keccak_new_89_cf(); uint8_t ret[168U]; - libcrux_sha3_generic_keccak_zero_block_9d_5e0(ret); + libcrux_sha3_generic_keccak_zero_block_8b_5e0(ret); memcpy(lit.buf[0U], ret, (size_t)168U * sizeof(uint8_t)); lit.buf_len = (size_t)0U; lit.sponge = false; @@ -1158,7 +1158,7 @@ libcrux_sha3::portable::incremental::Shake128Absorb)} */ static inline libcrux_sha3_generic_keccak_KeccakXofState_78 libcrux_sha3_portable_incremental_new_1c(void) { - return libcrux_sha3_generic_keccak_new_9d_470(); + return libcrux_sha3_generic_keccak_new_8b_470(); } /** @@ -1205,16 +1205,16 @@ static KRML_MUSTINLINE void libcrux_sha3_portable_keccak_store_5a_81( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.squeeze_9d +A monomorphic instance of libcrux_sha3.generic_keccak.squeeze_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 136 */ -static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_squeeze_9d_ba( +static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_squeeze_8b_ba( libcrux_sha3_generic_keccak_KeccakXofState_4f *self, Eurydice_slice out[1U]) { if (self->sponge) { @@ -1242,7 +1242,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_squeeze_9d_ba( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -1277,7 +1277,7 @@ libcrux_sha3::portable::incremental::Shake256Squeeze)#3} static inline void libcrux_sha3_portable_incremental_squeeze_8a( libcrux_sha3_generic_keccak_KeccakXofState_4f *self, Eurydice_slice out) { Eurydice_slice buf[1U] = {out}; - libcrux_sha3_generic_keccak_squeeze_9d_ba(self, buf); + libcrux_sha3_generic_keccak_squeeze_8b_ba(self, buf); } /** @@ -1324,16 +1324,16 @@ static KRML_MUSTINLINE void libcrux_sha3_portable_keccak_store_5a_810( */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakXofState[TraitClause@0]#2} +PARALLEL_LANES, RATE>[TraitClause@0, TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.squeeze_9d +A monomorphic instance of libcrux_sha3.generic_keccak.squeeze_8b with types uint64_t with const generics - PARALLEL_LANES= 1 - RATE= 168 */ -static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_squeeze_9d_ba0( +static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_squeeze_8b_ba0( libcrux_sha3_generic_keccak_KeccakXofState_78 *self, Eurydice_slice out[1U]) { if (self->sponge) { @@ -1361,7 +1361,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_squeeze_9d_ba0( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -1396,7 +1396,7 @@ libcrux_sha3::portable::incremental::Shake128Squeeze)#1} static inline void libcrux_sha3_portable_incremental_squeeze_10( libcrux_sha3_generic_keccak_KeccakXofState_78 *self, Eurydice_slice out) { Eurydice_slice buf[1U] = {out}; - libcrux_sha3_generic_keccak_squeeze_9d_ba0(self, buf); + libcrux_sha3_generic_keccak_squeeze_8b_ba0(self, buf); } /** diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c index c70315723..c0efed48a 100644 --- a/libcrux-ml-kem/c/libcrux_core.c +++ b/libcrux-ml-kem/c/libcrux_core.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "internal/libcrux_core.h" @@ -390,14 +390,15 @@ uint8_t *libcrux_ml_kem_types_as_slice_fd_cf( } /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[32size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_33(core_result_Result_00 self, uint8_t ret[32U]) { +void core_result_unwrap_26_33(core_result_Result_00 self, uint8_t ret[32U]) { if (self.tag == core_result_Ok) { uint8_t f0[32U]; memcpy(f0, self.val.case_Ok, (size_t)32U * sizeof(uint8_t)); @@ -519,14 +520,15 @@ void libcrux_ml_kem_utils_into_padded_array_42(Eurydice_slice slice, } /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[24size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_76(core_result_Result_6f self, uint8_t ret[24U]) { +void core_result_unwrap_26_76(core_result_Result_6f self, uint8_t ret[24U]) { if (self.tag == core_result_Ok) { uint8_t f0[24U]; memcpy(f0, self.val.case_Ok, (size_t)24U * sizeof(uint8_t)); @@ -539,14 +541,15 @@ void core_result_unwrap_41_76(core_result_Result_6f self, uint8_t ret[24U]) { } /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[20size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_ea(core_result_Result_7a self, uint8_t ret[20U]) { +void core_result_unwrap_26_ea(core_result_Result_7a self, uint8_t ret[20U]) { if (self.tag == core_result_Ok) { uint8_t f0[20U]; memcpy(f0, self.val.case_Ok, (size_t)20U * sizeof(uint8_t)); @@ -559,14 +562,15 @@ void core_result_unwrap_41_ea(core_result_Result_7a self, uint8_t ret[20U]) { } /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[10size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_07(core_result_Result_cd self, uint8_t ret[10U]) { +void core_result_unwrap_26_07(core_result_Result_cd self, uint8_t ret[10U]) { if (self.tag == core_result_Ok) { uint8_t f0[10U]; memcpy(f0, self.val.case_Ok, (size_t)10U * sizeof(uint8_t)); @@ -579,14 +583,15 @@ void core_result_unwrap_41_07(core_result_Result_cd self, uint8_t ret[10U]) { } /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types int16_t[16size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_30(core_result_Result_c0 self, int16_t ret[16U]) { +void core_result_unwrap_26_30(core_result_Result_c0 self, int16_t ret[16U]) { if (self.tag == core_result_Ok) { int16_t f0[16U]; memcpy(f0, self.val.case_Ok, (size_t)16U * sizeof(int16_t)); @@ -599,14 +604,15 @@ void core_result_unwrap_41_30(core_result_Result_c0 self, int16_t ret[16U]) { } /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[8size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_0e(core_result_Result_56 self, uint8_t ret[8U]) { +void core_result_unwrap_26_0e(core_result_Result_56 self, uint8_t ret[8U]) { if (self.tag == core_result_Ok) { uint8_t f0[8U]; memcpy(f0, self.val.case_Ok, (size_t)8U * sizeof(uint8_t)); diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h index d11c83a5a..f7265777c 100644 --- a/libcrux-ml-kem/c/libcrux_core.h +++ b/libcrux-ml-kem/c/libcrux_core.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_core_H @@ -197,14 +197,15 @@ typedef struct core_result_Result_56_s { } core_result_Result_56; /** -This function found in impl {core::result::Result} +This function found in impl {core::result::Result[TraitClause@0, +TraitClause@1]} */ /** -A monomorphic instance of core.result.unwrap_41 +A monomorphic instance of core.result.unwrap_26 with types uint8_t[8size_t], core_array_TryFromSliceError */ -void core_result_unwrap_41_0e(core_result_Result_56 self, uint8_t ret[8U]); +void core_result_unwrap_26_0e(core_result_Result_56 self, uint8_t ret[8U]); typedef struct Eurydice_slice_uint8_t_x2_s { Eurydice_slice fst; diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h index 0c4269273..0a85a746d 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem1024_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c index 291cdea74..31d8304e1 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "libcrux_mlkem1024_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h index e261044f5..8e758c512 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem1024_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c index 8589f3cb7..e8df4813a 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "libcrux_mlkem1024_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h index 5e13dac2e..fa38f9693 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem1024_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h index e2d3aeec9..2c452d78b 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem512_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c index 3147278df..a285e9e59 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "libcrux_mlkem512_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h index b8b6f8b0d..13b581872 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem512_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c index f4b93367f..25be9d68b 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "libcrux_mlkem512_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h index 7b475f089..71cbfb6fe 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem512_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h index 9d931422e..537ec47e9 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem768_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c index 067de4a91..282d5e8f3 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "libcrux_mlkem768_avx2.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h index 7a86aed30..36ab7426f 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem768_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c index fae6a874c..fae5cc397 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "libcrux_mlkem768_portable.h" diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h index 5feb24427..ff60c10cb 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem768_portable_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c index a0b9361ed..97b6fd741 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "internal/libcrux_mlkem_avx2.h" @@ -603,7 +603,7 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_4( &dst, Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)8U, uint8_t), Eurydice_slice, uint8_t[8U]); - core_result_unwrap_41_0e(dst, ret0); + core_result_unwrap_26_0e(dst, ret0); memcpy(ret, ret0, (size_t)8U * sizeof(uint8_t)); } @@ -694,7 +694,7 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_5( &dst, Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)10U, uint8_t), Eurydice_slice, uint8_t[10U]); - core_result_unwrap_41_07(dst, ret0); + core_result_unwrap_26_07(dst, ret0); memcpy(ret, ret0, (size_t)10U * sizeof(uint8_t)); } @@ -797,7 +797,7 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_10( &dst, Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)20U, uint8_t), Eurydice_slice, uint8_t[20U]); - core_result_unwrap_41_ea(dst, ret0); + core_result_unwrap_26_ea(dst, ret0); memcpy(ret, ret0, (size_t)20U * sizeof(uint8_t)); } @@ -924,7 +924,7 @@ KRML_MUSTINLINE void libcrux_ml_kem_vector_avx2_serialize_serialize_12( &dst, Eurydice_array_to_subslice2(serialized, (size_t)0U, (size_t)24U, uint8_t), Eurydice_slice, uint8_t[24U]); - core_result_unwrap_41_76(dst, ret0); + core_result_unwrap_26_76(dst, ret0); memcpy(ret, ret0, (size_t)24U * sizeof(uint8_t)); } @@ -1031,15 +1031,16 @@ inline __m256i libcrux_ml_kem_vector_avx2_clone_78(__m256i *self) { /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.ZERO_20 +A monomorphic instance of libcrux_ml_kem.polynomial.ZERO_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ -static libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ZERO_20_7d(void) { +static libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ZERO_ef_7d(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 lit; lit.coefficients[0U] = libcrux_ml_kem_vector_avx2_ZERO_09(); lit.coefficients[1U] = libcrux_ml_kem_vector_avx2_ZERO_09(); @@ -1068,7 +1069,7 @@ libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialize_to_reduced_ring_element_b8(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_ef_7d(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)24U; i++) { size_t i0 = i; @@ -1117,7 +1118,7 @@ static KRML_MUSTINLINE void deserialize_ring_elements_reduced_out_bf1( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialized_pk[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - deserialized_pk[i] = ZERO_20_7d();); + deserialized_pk[i] = ZERO_ef_7d();); deserialize_ring_elements_reduced_fb1(public_key, deserialized_pk); memcpy( ret, deserialized_pk, @@ -1341,19 +1342,19 @@ typedef struct IndCpaPrivateKeyUnpacked_a0_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPrivateKeyUnpacked[TraitClause@0])} +K>[TraitClause@0, TraitClause@1])} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_f6 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_1a with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 3 */ -static IndCpaPrivateKeyUnpacked_a0 default_f6_191(void) { +static IndCpaPrivateKeyUnpacked_a0 default_1a_191(void) { IndCpaPrivateKeyUnpacked_a0 lit; - lit.secret_as_ntt[0U] = ZERO_20_7d(); - lit.secret_as_ntt[1U] = ZERO_20_7d(); - lit.secret_as_ntt[2U] = ZERO_20_7d(); + lit.secret_as_ntt[0U] = ZERO_ef_7d(); + lit.secret_as_ntt[1U] = ZERO_ef_7d(); + lit.secret_as_ntt[2U] = ZERO_ef_7d(); return lit; } @@ -1372,33 +1373,33 @@ typedef struct IndCpaPublicKeyUnpacked_a0_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPublicKeyUnpacked[TraitClause@0])#1} +K>[TraitClause@0, TraitClause@1])#1} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_85 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_8d with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 3 */ -static IndCpaPublicKeyUnpacked_a0 default_85_801(void) { +static IndCpaPublicKeyUnpacked_a0 default_8d_801(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - uu____0[i] = ZERO_20_7d();); + uu____0[i] = ZERO_ef_7d();); uint8_t uu____1[32U] = {0U}; IndCpaPublicKeyUnpacked_a0 lit; memcpy( lit.t_as_ntt, uu____0, (size_t)3U * sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_d2)); memcpy(lit.seed_for_A, uu____1, (size_t)32U * sizeof(uint8_t)); - lit.A[0U][0U] = ZERO_20_7d(); - lit.A[0U][1U] = ZERO_20_7d(); - lit.A[0U][2U] = ZERO_20_7d(); - lit.A[1U][0U] = ZERO_20_7d(); - lit.A[1U][1U] = ZERO_20_7d(); - lit.A[1U][2U] = ZERO_20_7d(); - lit.A[2U][0U] = ZERO_20_7d(); - lit.A[2U][1U] = ZERO_20_7d(); - lit.A[2U][2U] = ZERO_20_7d(); + lit.A[0U][0U] = ZERO_ef_7d(); + lit.A[0U][1U] = ZERO_ef_7d(); + lit.A[0U][2U] = ZERO_ef_7d(); + lit.A[1U][0U] = ZERO_ef_7d(); + lit.A[1U][1U] = ZERO_ef_7d(); + lit.A[1U][2U] = ZERO_ef_7d(); + lit.A[2U][0U] = ZERO_ef_7d(); + lit.A[2U][1U] = ZERO_ef_7d(); + lit.A[2U][2U] = ZERO_ef_7d(); return lit; } @@ -1728,17 +1729,18 @@ static KRML_MUSTINLINE bool sample_from_uniform_distribution_next_744( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.from_i16_array_20 +A monomorphic instance of libcrux_ml_kem.polynomial.from_i16_array_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 -from_i16_array_20_14(Eurydice_slice a) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_20_7d(); +from_i16_array_ef_14(Eurydice_slice a) { + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_ef_7d(); for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; @@ -1757,7 +1759,7 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics */ static libcrux_ml_kem_polynomial_PolynomialRingElement_d2 closure_e41( int16_t s[272U]) { - return from_i16_array_20_14( + return from_i16_array_ef_14( Eurydice_array_to_subslice2(s, (size_t)0U, (size_t)256U, int16_t)); } @@ -1942,7 +1944,7 @@ sample_from_binomial_distribution_2_80(Eurydice_slice randomness) { sampled_i16s[(size_t)8U * chunk_number + offset] = outcome_1 - outcome_2; } } - return from_i16_array_20_14( + return from_i16_array_ef_14( Eurydice_array_to_slice((size_t)256U, sampled_i16s, int16_t)); } @@ -1986,7 +1988,7 @@ sample_from_binomial_distribution_3_05(Eurydice_slice randomness) { sampled_i16s[(size_t)4U * chunk_number + offset] = outcome_1 - outcome_2; } } - return from_i16_array_20_14( + return from_i16_array_ef_14( Eurydice_array_to_slice((size_t)256U, sampled_i16s, int16_t)); } @@ -2137,15 +2139,16 @@ static KRML_MUSTINLINE void ntt_at_layer_1_09( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.poly_barrett_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.poly_barrett_reduce_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ -static KRML_MUSTINLINE void poly_barrett_reduce_20_09( +static KRML_MUSTINLINE void poly_barrett_reduce_ef_09( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self) { for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { @@ -2171,7 +2174,7 @@ static KRML_MUSTINLINE void ntt_binomially_sampled_ring_element_5c( ntt_at_layer_3_ae(&zeta_i, re); ntt_at_layer_2_53(&zeta_i, re); ntt_at_layer_1_09(&zeta_i, re); - poly_barrett_reduce_20_09(re); + poly_barrett_reduce_ef_09(re); } /** @@ -2228,7 +2231,7 @@ static KRML_MUSTINLINE tuple_b0 sample_vector_cbd_then_ntt_out_d71( uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re_as_ntt[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - re_as_ntt[i] = ZERO_20_7d();); + re_as_ntt[i] = ZERO_ef_7d();); libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *uu____0 = re_as_ntt; uint8_t uu____1[33U]; memcpy(uu____1, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -2249,18 +2252,19 @@ static KRML_MUSTINLINE tuple_b0 sample_vector_cbd_then_ntt_out_d71( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.ntt_multiply_20 +A monomorphic instance of libcrux_ml_kem.polynomial.ntt_multiply_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 -ntt_multiply_20_63(libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, +ntt_multiply_ef_63(libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *rhs) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 out = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 out = ZERO_ef_7d(); for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; @@ -2279,15 +2283,16 @@ ntt_multiply_20_63(libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 3 */ -static KRML_MUSTINLINE void add_to_ring_element_20_311( +static KRML_MUSTINLINE void add_to_ring_element_ef_311( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *rhs) { for (size_t i = (size_t)0U; @@ -2314,15 +2319,16 @@ static __m256i to_standard_domain_c1(__m256i v) { /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_standard_error_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_standard_error_reduce_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ -static KRML_MUSTINLINE void add_standard_error_reduce_20_ba( +static KRML_MUSTINLINE void add_standard_error_reduce_ef_ba( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *error) { for (size_t i = (size_t)0U; @@ -2356,7 +2362,7 @@ static KRML_MUSTINLINE void compute_As_plus_e_671( i++) { size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *row = matrix_A[i0]; - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0 = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0 = ZERO_ef_7d(); t_as_ntt[i0] = uu____0; for (size_t i1 = (size_t)0U; i1 < Eurydice_slice_len( @@ -2369,10 +2375,10 @@ static KRML_MUSTINLINE void compute_As_plus_e_671( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *matrix_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(matrix_element, &s_as_ntt[j]); - add_to_ring_element_20_311(&t_as_ntt[i0], &product); + ntt_multiply_ef_63(matrix_element, &s_as_ntt[j]); + add_to_ring_element_ef_311(&t_as_ntt[i0], &product); } - add_standard_error_reduce_20_ba(&t_as_ntt[i0], &error_as_ntt[i0]); + add_standard_error_reduce_ef_ba(&t_as_ntt[i0], &error_as_ntt[i0]); } } @@ -2425,7 +2431,7 @@ static void generate_keypair_unpacked_4a1( uint8_t uu____5[32U]; core_result_Result_00 dst; Eurydice_slice_to_array2(&dst, seed_for_A, Eurydice_slice, uint8_t[32U]); - core_result_unwrap_41_33(dst, uu____5); + core_result_unwrap_26_33(dst, uu____5); memcpy(public_key->seed_for_A, uu____5, (size_t)32U * sizeof(uint8_t)); } @@ -2443,8 +2449,8 @@ with const generics */ static libcrux_ml_kem_utils_extraction_helper_Keypair768 generate_keypair_1e1( Eurydice_slice key_generation_seed) { - IndCpaPrivateKeyUnpacked_a0 private_key = default_f6_191(); - IndCpaPublicKeyUnpacked_a0 public_key = default_85_801(); + IndCpaPrivateKeyUnpacked_a0 private_key = default_1a_191(); + IndCpaPublicKeyUnpacked_a0 public_key = default_8d_801(); generate_keypair_unpacked_4a1(key_generation_seed, &private_key, &public_key); uint8_t public_key_serialized[1184U]; serialize_public_key_f71( @@ -2595,7 +2601,7 @@ static KRML_MUSTINLINE tuple_b0 sample_ring_element_cbd_2d1(uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 error_1[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - error_1[i] = ZERO_20_7d();); + error_1[i] = ZERO_ef_7d();); /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_prf_input[33U]; memcpy(copy_of_prf_input, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -2775,20 +2781,21 @@ static KRML_MUSTINLINE void invert_ntt_montgomery_0c1( invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)5U); invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)6U); invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)7U); - poly_barrett_reduce_20_09(re); + poly_barrett_reduce_ef_09(re); } /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_error_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_error_reduce_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ -static KRML_MUSTINLINE void add_error_reduce_20_a2( +static KRML_MUSTINLINE void add_error_reduce_ef_a2( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *error) { for (size_t i = (size_t)0U; @@ -2816,7 +2823,7 @@ static KRML_MUSTINLINE void compute_vector_u_7f1( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result0[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - result0[i] = ZERO_20_7d();); + result0[i] = ZERO_ef_7d();); for (size_t i0 = (size_t)0U; i0 < Eurydice_slice_len( Eurydice_array_to_slice( @@ -2836,11 +2843,11 @@ static KRML_MUSTINLINE void compute_vector_u_7f1( size_t j = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *a_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(a_element, &r_as_ntt[j]); - add_to_ring_element_20_311(&result0[i1], &product); + ntt_multiply_ef_63(a_element, &r_as_ntt[j]); + add_to_ring_element_ef_311(&result0[i1], &product); } invert_ntt_montgomery_0c1(&result0[i1]); - add_error_reduce_20_a2(&result0[i1], &error_1[i1]); + add_error_reduce_ef_a2(&result0[i1], &error_1[i1]); } libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result[3U]; memcpy( @@ -2872,7 +2879,7 @@ libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialize_then_decompress_message_4f(uint8_t serialized[32U]) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_ef_7d(); KRML_MAYBE_FOR16( i, (size_t)0U, (size_t)16U, (size_t)1U, size_t i0 = i; __m256i coefficient_compressed = @@ -2886,16 +2893,17 @@ deserialize_then_decompress_message_4f(uint8_t serialized[32U]) { /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_message_error_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_message_error_reduce_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 -add_message_error_reduce_20_df( +add_message_error_reduce_ef_df( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *message, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result) { @@ -2927,13 +2935,13 @@ compute_ring_element_v_ac1( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *r_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *error_2, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *message) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_ef_7d(); KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(&t_as_ntt[i0], &r_as_ntt[i0]); - add_to_ring_element_20_311(&result, &product);); + ntt_multiply_ef_63(&t_as_ntt[i0], &r_as_ntt[i0]); + add_to_ring_element_ef_311(&result, &product);); invert_ntt_montgomery_0c1(&result); - result = add_message_error_reduce_20_df(error_2, message, result); + result = add_message_error_reduce_ef_df(error_2, message, result); return result; } @@ -3391,7 +3399,7 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics */ static void encrypt_691(Eurydice_slice public_key, uint8_t message[32U], Eurydice_slice randomness, uint8_t ret[1088U]) { - IndCpaPublicKeyUnpacked_a0 unpacked_public_key = default_85_801(); + IndCpaPublicKeyUnpacked_a0 unpacked_public_key = default_8d_801(); deserialize_ring_elements_reduced_fb1( Eurydice_slice_subslice_to(public_key, (size_t)1152U, uint8_t, size_t), unpacked_public_key.t_as_ntt); @@ -3510,7 +3518,7 @@ libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialize_to_uncompressed_ring_element_59(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_ef_7d(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)24U; i++) { size_t i0 = i; @@ -3532,7 +3540,7 @@ static KRML_MUSTINLINE void deserialize_secret_key_181( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 secret_as_ntt[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - secret_as_ntt[i] = ZERO_20_7d();); + secret_as_ntt[i] = ZERO_ef_7d();); for (size_t i = (size_t)0U; i < Eurydice_slice_len(secret_key, uint8_t) / LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT; @@ -3619,7 +3627,7 @@ libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialize_then_decompress_10_3d(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_ef_7d(); LowStar_Ignore_ignore( Eurydice_slice_len( Eurydice_array_to_slice((size_t)16U, re.coefficients, __m256i), @@ -3699,7 +3707,7 @@ libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialize_then_decompress_11_1a(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_ef_7d(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)22U; i++) { size_t i0 = i; @@ -3738,7 +3746,7 @@ static KRML_MUSTINLINE void ntt_vector_u_2c0( ntt_at_layer_3_ae(&zeta_i, re); ntt_at_layer_2_53(&zeta_i, re); ntt_at_layer_1_09(&zeta_i, re); - poly_barrett_reduce_20_09(re); + poly_barrett_reduce_ef_09(re); } /** @@ -3754,7 +3762,7 @@ static KRML_MUSTINLINE void deserialize_then_decompress_u_a81( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 u_as_ntt[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - u_as_ntt[i] = ZERO_20_7d();); + u_as_ntt[i] = ZERO_ef_7d();); for (size_t i = (size_t)0U; i < Eurydice_slice_len( Eurydice_array_to_slice((size_t)1088U, ciphertext, uint8_t), @@ -3843,7 +3851,7 @@ with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialize_then_decompress_4_f1(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_ef_7d(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)8U; i++) { size_t i0 = i; @@ -3918,7 +3926,7 @@ with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialize_then_decompress_5_7e(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re = ZERO_ef_7d(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)10U; i++) { size_t i0 = i; @@ -3944,16 +3952,17 @@ deserialize_then_decompress_ring_element_v_050(Eurydice_slice serialized) { /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.subtract_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.subtract_reduce_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_d2 -subtract_reduce_20_27(libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, +subtract_reduce_ef_27(libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 b) { for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { @@ -3979,13 +3988,13 @@ compute_message_a41( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *v, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *secret_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *u_as_ntt) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_ef_7d(); KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(&secret_as_ntt[i0], &u_as_ntt[i0]); - add_to_ring_element_20_311(&result, &product);); + ntt_multiply_ef_63(&secret_as_ntt[i0], &u_as_ntt[i0]); + add_to_ring_element_ef_311(&result, &product);); invert_ntt_montgomery_0c1(&result); - result = subtract_reduce_20_27(v, result); + result = subtract_reduce_ef_27(v, result); return result; } @@ -4221,7 +4230,7 @@ static KRML_MUSTINLINE void deserialize_ring_elements_reduced_out_bf0( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialized_pk[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - deserialized_pk[i] = ZERO_20_7d();); + deserialized_pk[i] = ZERO_ef_7d();); deserialize_ring_elements_reduced_fb(public_key, deserialized_pk); memcpy( ret, deserialized_pk, @@ -4375,20 +4384,20 @@ typedef struct IndCpaPrivateKeyUnpacked_01_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPrivateKeyUnpacked[TraitClause@0])} +K>[TraitClause@0, TraitClause@1])} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_f6 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_1a with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 4 */ -static IndCpaPrivateKeyUnpacked_01 default_f6_19(void) { +static IndCpaPrivateKeyUnpacked_01 default_1a_19(void) { IndCpaPrivateKeyUnpacked_01 lit; - lit.secret_as_ntt[0U] = ZERO_20_7d(); - lit.secret_as_ntt[1U] = ZERO_20_7d(); - lit.secret_as_ntt[2U] = ZERO_20_7d(); - lit.secret_as_ntt[3U] = ZERO_20_7d(); + lit.secret_as_ntt[0U] = ZERO_ef_7d(); + lit.secret_as_ntt[1U] = ZERO_ef_7d(); + lit.secret_as_ntt[2U] = ZERO_ef_7d(); + lit.secret_as_ntt[3U] = ZERO_ef_7d(); return lit; } @@ -4407,40 +4416,40 @@ typedef struct IndCpaPublicKeyUnpacked_01_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPublicKeyUnpacked[TraitClause@0])#1} +K>[TraitClause@0, TraitClause@1])#1} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_85 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_8d with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 4 */ -static IndCpaPublicKeyUnpacked_01 default_85_80(void) { +static IndCpaPublicKeyUnpacked_01 default_8d_80(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - uu____0[i] = ZERO_20_7d();); + uu____0[i] = ZERO_ef_7d();); uint8_t uu____1[32U] = {0U}; IndCpaPublicKeyUnpacked_01 lit; memcpy( lit.t_as_ntt, uu____0, (size_t)4U * sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_d2)); memcpy(lit.seed_for_A, uu____1, (size_t)32U * sizeof(uint8_t)); - lit.A[0U][0U] = ZERO_20_7d(); - lit.A[0U][1U] = ZERO_20_7d(); - lit.A[0U][2U] = ZERO_20_7d(); - lit.A[0U][3U] = ZERO_20_7d(); - lit.A[1U][0U] = ZERO_20_7d(); - lit.A[1U][1U] = ZERO_20_7d(); - lit.A[1U][2U] = ZERO_20_7d(); - lit.A[1U][3U] = ZERO_20_7d(); - lit.A[2U][0U] = ZERO_20_7d(); - lit.A[2U][1U] = ZERO_20_7d(); - lit.A[2U][2U] = ZERO_20_7d(); - lit.A[2U][3U] = ZERO_20_7d(); - lit.A[3U][0U] = ZERO_20_7d(); - lit.A[3U][1U] = ZERO_20_7d(); - lit.A[3U][2U] = ZERO_20_7d(); - lit.A[3U][3U] = ZERO_20_7d(); + lit.A[0U][0U] = ZERO_ef_7d(); + lit.A[0U][1U] = ZERO_ef_7d(); + lit.A[0U][2U] = ZERO_ef_7d(); + lit.A[0U][3U] = ZERO_ef_7d(); + lit.A[1U][0U] = ZERO_ef_7d(); + lit.A[1U][1U] = ZERO_ef_7d(); + lit.A[1U][2U] = ZERO_ef_7d(); + lit.A[1U][3U] = ZERO_ef_7d(); + lit.A[2U][0U] = ZERO_ef_7d(); + lit.A[2U][1U] = ZERO_ef_7d(); + lit.A[2U][2U] = ZERO_ef_7d(); + lit.A[2U][3U] = ZERO_ef_7d(); + lit.A[3U][0U] = ZERO_ef_7d(); + lit.A[3U][1U] = ZERO_ef_7d(); + lit.A[3U][2U] = ZERO_ef_7d(); + lit.A[3U][3U] = ZERO_ef_7d(); return lit; } @@ -4782,7 +4791,7 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics */ static libcrux_ml_kem_polynomial_PolynomialRingElement_d2 closure_e4( int16_t s[272U]) { - return from_i16_array_20_14( + return from_i16_array_ef_14( Eurydice_array_to_subslice2(s, (size_t)0U, (size_t)256U, int16_t)); } @@ -4983,7 +4992,7 @@ static KRML_MUSTINLINE tuple_71 sample_vector_cbd_then_ntt_out_d7( uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re_as_ntt[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - re_as_ntt[i] = ZERO_20_7d();); + re_as_ntt[i] = ZERO_ef_7d();); libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *uu____0 = re_as_ntt; uint8_t uu____1[33U]; memcpy(uu____1, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -5004,15 +5013,16 @@ static KRML_MUSTINLINE tuple_71 sample_vector_cbd_then_ntt_out_d7( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 4 */ -static KRML_MUSTINLINE void add_to_ring_element_20_31( +static KRML_MUSTINLINE void add_to_ring_element_ef_31( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *rhs) { for (size_t i = (size_t)0U; @@ -5046,7 +5056,7 @@ static KRML_MUSTINLINE void compute_As_plus_e_67( i++) { size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *row = matrix_A[i0]; - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0 = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0 = ZERO_ef_7d(); t_as_ntt[i0] = uu____0; for (size_t i1 = (size_t)0U; i1 < Eurydice_slice_len( @@ -5059,10 +5069,10 @@ static KRML_MUSTINLINE void compute_As_plus_e_67( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *matrix_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(matrix_element, &s_as_ntt[j]); - add_to_ring_element_20_31(&t_as_ntt[i0], &product); + ntt_multiply_ef_63(matrix_element, &s_as_ntt[j]); + add_to_ring_element_ef_31(&t_as_ntt[i0], &product); } - add_standard_error_reduce_20_ba(&t_as_ntt[i0], &error_as_ntt[i0]); + add_standard_error_reduce_ef_ba(&t_as_ntt[i0], &error_as_ntt[i0]); } } @@ -5115,7 +5125,7 @@ static void generate_keypair_unpacked_4a( uint8_t uu____5[32U]; core_result_Result_00 dst; Eurydice_slice_to_array2(&dst, seed_for_A, Eurydice_slice, uint8_t[32U]); - core_result_unwrap_41_33(dst, uu____5); + core_result_unwrap_26_33(dst, uu____5); memcpy(public_key->seed_for_A, uu____5, (size_t)32U * sizeof(uint8_t)); } @@ -5133,8 +5143,8 @@ with const generics */ static libcrux_ml_kem_utils_extraction_helper_Keypair1024 generate_keypair_1e0( Eurydice_slice key_generation_seed) { - IndCpaPrivateKeyUnpacked_01 private_key = default_f6_19(); - IndCpaPublicKeyUnpacked_01 public_key = default_85_80(); + IndCpaPrivateKeyUnpacked_01 private_key = default_1a_19(); + IndCpaPublicKeyUnpacked_01 public_key = default_8d_80(); generate_keypair_unpacked_4a(key_generation_seed, &private_key, &public_key); uint8_t public_key_serialized[1568U]; serialize_public_key_f7( @@ -5285,7 +5295,7 @@ static KRML_MUSTINLINE tuple_71 sample_ring_element_cbd_2d(uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 error_1[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - error_1[i] = ZERO_20_7d();); + error_1[i] = ZERO_ef_7d();); /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_prf_input[33U]; memcpy(copy_of_prf_input, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -5349,7 +5359,7 @@ static KRML_MUSTINLINE void invert_ntt_montgomery_0c( invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)5U); invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)6U); invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)7U); - poly_barrett_reduce_20_09(re); + poly_barrett_reduce_ef_09(re); } /** @@ -5365,7 +5375,7 @@ static KRML_MUSTINLINE void compute_vector_u_7f( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result0[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - result0[i] = ZERO_20_7d();); + result0[i] = ZERO_ef_7d();); for (size_t i0 = (size_t)0U; i0 < Eurydice_slice_len( Eurydice_array_to_slice( @@ -5385,11 +5395,11 @@ static KRML_MUSTINLINE void compute_vector_u_7f( size_t j = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *a_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(a_element, &r_as_ntt[j]); - add_to_ring_element_20_31(&result0[i1], &product); + ntt_multiply_ef_63(a_element, &r_as_ntt[j]); + add_to_ring_element_ef_31(&result0[i1], &product); } invert_ntt_montgomery_0c(&result0[i1]); - add_error_reduce_20_a2(&result0[i1], &error_1[i1]); + add_error_reduce_ef_a2(&result0[i1], &error_1[i1]); } libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result[4U]; memcpy( @@ -5412,13 +5422,13 @@ compute_ring_element_v_ac( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *r_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *error_2, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *message) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_ef_7d(); KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(&t_as_ntt[i0], &r_as_ntt[i0]); - add_to_ring_element_20_31(&result, &product);); + ntt_multiply_ef_63(&t_as_ntt[i0], &r_as_ntt[i0]); + add_to_ring_element_ef_31(&result, &product);); invert_ntt_montgomery_0c(&result); - result = add_message_error_reduce_20_df(error_2, message, result); + result = add_message_error_reduce_ef_df(error_2, message, result); return result; } @@ -5595,7 +5605,7 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics */ static void encrypt_690(Eurydice_slice public_key, uint8_t message[32U], Eurydice_slice randomness, uint8_t ret[1568U]) { - IndCpaPublicKeyUnpacked_01 unpacked_public_key = default_85_80(); + IndCpaPublicKeyUnpacked_01 unpacked_public_key = default_8d_80(); deserialize_ring_elements_reduced_fb( Eurydice_slice_subslice_to(public_key, (size_t)1536U, uint8_t, size_t), unpacked_public_key.t_as_ntt); @@ -5717,7 +5727,7 @@ static KRML_MUSTINLINE void deserialize_secret_key_180( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 secret_as_ntt[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - secret_as_ntt[i] = ZERO_20_7d();); + secret_as_ntt[i] = ZERO_ef_7d();); for (size_t i = (size_t)0U; i < Eurydice_slice_len(secret_key, uint8_t) / LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT; @@ -5768,7 +5778,7 @@ static KRML_MUSTINLINE void ntt_vector_u_2c( ntt_at_layer_3_ae(&zeta_i, re); ntt_at_layer_2_53(&zeta_i, re); ntt_at_layer_1_09(&zeta_i, re); - poly_barrett_reduce_20_09(re); + poly_barrett_reduce_ef_09(re); } /** @@ -5784,7 +5794,7 @@ static KRML_MUSTINLINE void deserialize_then_decompress_u_a8( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 u_as_ntt[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - u_as_ntt[i] = ZERO_20_7d();); + u_as_ntt[i] = ZERO_ef_7d();); for (size_t i = (size_t)0U; i < Eurydice_slice_len( Eurydice_array_to_slice((size_t)1568U, ciphertext, uint8_t), @@ -5832,13 +5842,13 @@ compute_message_a4( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *v, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *secret_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *u_as_ntt) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_ef_7d(); KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(&secret_as_ntt[i0], &u_as_ntt[i0]); - add_to_ring_element_20_31(&result, &product);); + ntt_multiply_ef_63(&secret_as_ntt[i0], &u_as_ntt[i0]); + add_to_ring_element_ef_31(&result, &product);); invert_ntt_montgomery_0c(&result); - result = subtract_reduce_20_27(v, result); + result = subtract_reduce_ef_27(v, result); return result; } @@ -6036,7 +6046,7 @@ static KRML_MUSTINLINE void deserialize_ring_elements_reduced_out_bf( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 deserialized_pk[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - deserialized_pk[i] = ZERO_20_7d();); + deserialized_pk[i] = ZERO_ef_7d();); deserialize_ring_elements_reduced_fb0(public_key, deserialized_pk); memcpy( ret, deserialized_pk, @@ -6190,18 +6200,18 @@ typedef struct IndCpaPrivateKeyUnpacked_d6_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPrivateKeyUnpacked[TraitClause@0])} +K>[TraitClause@0, TraitClause@1])} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_f6 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_1a with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 2 */ -static IndCpaPrivateKeyUnpacked_d6 default_f6_190(void) { +static IndCpaPrivateKeyUnpacked_d6 default_1a_190(void) { IndCpaPrivateKeyUnpacked_d6 lit; - lit.secret_as_ntt[0U] = ZERO_20_7d(); - lit.secret_as_ntt[1U] = ZERO_20_7d(); + lit.secret_as_ntt[0U] = ZERO_ef_7d(); + lit.secret_as_ntt[1U] = ZERO_ef_7d(); return lit; } @@ -6220,28 +6230,28 @@ typedef struct IndCpaPublicKeyUnpacked_d6_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPublicKeyUnpacked[TraitClause@0])#1} +K>[TraitClause@0, TraitClause@1])#1} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_85 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_8d with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 2 */ -static IndCpaPublicKeyUnpacked_d6 default_85_800(void) { +static IndCpaPublicKeyUnpacked_d6 default_8d_800(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - uu____0[i] = ZERO_20_7d();); + uu____0[i] = ZERO_ef_7d();); uint8_t uu____1[32U] = {0U}; IndCpaPublicKeyUnpacked_d6 lit; memcpy( lit.t_as_ntt, uu____0, (size_t)2U * sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_d2)); memcpy(lit.seed_for_A, uu____1, (size_t)32U * sizeof(uint8_t)); - lit.A[0U][0U] = ZERO_20_7d(); - lit.A[0U][1U] = ZERO_20_7d(); - lit.A[1U][0U] = ZERO_20_7d(); - lit.A[1U][1U] = ZERO_20_7d(); + lit.A[0U][0U] = ZERO_ef_7d(); + lit.A[0U][1U] = ZERO_ef_7d(); + lit.A[1U][0U] = ZERO_ef_7d(); + lit.A[1U][1U] = ZERO_ef_7d(); return lit; } @@ -6571,7 +6581,7 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics */ static libcrux_ml_kem_polynomial_PolynomialRingElement_d2 closure_e40( int16_t s[272U]) { - return from_i16_array_20_14( + return from_i16_array_ef_14( Eurydice_array_to_subslice2(s, (size_t)0U, (size_t)256U, int16_t)); } @@ -6777,7 +6787,7 @@ static KRML_MUSTINLINE tuple_74 sample_vector_cbd_then_ntt_out_d70( uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 re_as_ntt[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - re_as_ntt[i] = ZERO_20_7d();); + re_as_ntt[i] = ZERO_ef_7d();); libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *uu____0 = re_as_ntt; uint8_t uu____1[33U]; memcpy(uu____1, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -6798,15 +6808,16 @@ static KRML_MUSTINLINE tuple_74 sample_vector_cbd_then_ntt_out_d70( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_ef with types libcrux_ml_kem_vector_avx2_SIMD256Vector with const generics - K= 2 */ -static KRML_MUSTINLINE void add_to_ring_element_20_310( +static KRML_MUSTINLINE void add_to_ring_element_ef_310( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *rhs) { for (size_t i = (size_t)0U; @@ -6840,7 +6851,7 @@ static KRML_MUSTINLINE void compute_As_plus_e_670( i++) { size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *row = matrix_A[i0]; - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0 = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 uu____0 = ZERO_ef_7d(); t_as_ntt[i0] = uu____0; for (size_t i1 = (size_t)0U; i1 < Eurydice_slice_len( @@ -6853,10 +6864,10 @@ static KRML_MUSTINLINE void compute_As_plus_e_670( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *matrix_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(matrix_element, &s_as_ntt[j]); - add_to_ring_element_20_310(&t_as_ntt[i0], &product); + ntt_multiply_ef_63(matrix_element, &s_as_ntt[j]); + add_to_ring_element_ef_310(&t_as_ntt[i0], &product); } - add_standard_error_reduce_20_ba(&t_as_ntt[i0], &error_as_ntt[i0]); + add_standard_error_reduce_ef_ba(&t_as_ntt[i0], &error_as_ntt[i0]); } } @@ -6909,7 +6920,7 @@ static void generate_keypair_unpacked_4a0( uint8_t uu____5[32U]; core_result_Result_00 dst; Eurydice_slice_to_array2(&dst, seed_for_A, Eurydice_slice, uint8_t[32U]); - core_result_unwrap_41_33(dst, uu____5); + core_result_unwrap_26_33(dst, uu____5); memcpy(public_key->seed_for_A, uu____5, (size_t)32U * sizeof(uint8_t)); } @@ -6927,8 +6938,8 @@ with const generics */ static libcrux_ml_kem_utils_extraction_helper_Keypair512 generate_keypair_1e( Eurydice_slice key_generation_seed) { - IndCpaPrivateKeyUnpacked_d6 private_key = default_f6_190(); - IndCpaPublicKeyUnpacked_d6 public_key = default_85_800(); + IndCpaPrivateKeyUnpacked_d6 private_key = default_1a_190(); + IndCpaPublicKeyUnpacked_d6 public_key = default_8d_800(); generate_keypair_unpacked_4a0(key_generation_seed, &private_key, &public_key); uint8_t public_key_serialized[800U]; serialize_public_key_f70( @@ -7125,7 +7136,7 @@ static KRML_MUSTINLINE tuple_74 sample_ring_element_cbd_2d0(uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 error_1[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - error_1[i] = ZERO_20_7d();); + error_1[i] = ZERO_ef_7d();); /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_prf_input[33U]; memcpy(copy_of_prf_input, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -7189,7 +7200,7 @@ static KRML_MUSTINLINE void invert_ntt_montgomery_0c0( invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)5U); invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)6U); invert_ntt_at_layer_4_plus_0f(&zeta_i, re, (size_t)7U); - poly_barrett_reduce_20_09(re); + poly_barrett_reduce_ef_09(re); } /** @@ -7205,7 +7216,7 @@ static KRML_MUSTINLINE void compute_vector_u_7f0( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result0[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - result0[i] = ZERO_20_7d();); + result0[i] = ZERO_ef_7d();); for (size_t i0 = (size_t)0U; i0 < Eurydice_slice_len( Eurydice_array_to_slice( @@ -7225,11 +7236,11 @@ static KRML_MUSTINLINE void compute_vector_u_7f0( size_t j = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *a_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(a_element, &r_as_ntt[j]); - add_to_ring_element_20_310(&result0[i1], &product); + ntt_multiply_ef_63(a_element, &r_as_ntt[j]); + add_to_ring_element_ef_310(&result0[i1], &product); } invert_ntt_montgomery_0c0(&result0[i1]); - add_error_reduce_20_a2(&result0[i1], &error_1[i1]); + add_error_reduce_ef_a2(&result0[i1], &error_1[i1]); } libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result[2U]; memcpy( @@ -7252,13 +7263,13 @@ compute_ring_element_v_ac0( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *r_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *error_2, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *message) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_ef_7d(); KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(&t_as_ntt[i0], &r_as_ntt[i0]); - add_to_ring_element_20_310(&result, &product);); + ntt_multiply_ef_63(&t_as_ntt[i0], &r_as_ntt[i0]); + add_to_ring_element_ef_310(&result, &product);); invert_ntt_montgomery_0c0(&result); - result = add_message_error_reduce_20_df(error_2, message, result); + result = add_message_error_reduce_ef_df(error_2, message, result); return result; } @@ -7385,7 +7396,7 @@ libcrux_ml_kem_hash_functions_avx2_Simd256Hash with const generics */ static void encrypt_69(Eurydice_slice public_key, uint8_t message[32U], Eurydice_slice randomness, uint8_t ret[768U]) { - IndCpaPublicKeyUnpacked_d6 unpacked_public_key = default_85_800(); + IndCpaPublicKeyUnpacked_d6 unpacked_public_key = default_8d_800(); deserialize_ring_elements_reduced_fb0( Eurydice_slice_subslice_to(public_key, (size_t)768U, uint8_t, size_t), unpacked_public_key.t_as_ntt); @@ -7507,7 +7518,7 @@ static KRML_MUSTINLINE void deserialize_secret_key_18( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 secret_as_ntt[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - secret_as_ntt[i] = ZERO_20_7d();); + secret_as_ntt[i] = ZERO_ef_7d();); for (size_t i = (size_t)0U; i < Eurydice_slice_len(secret_key, uint8_t) / LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT; @@ -7544,7 +7555,7 @@ static KRML_MUSTINLINE void deserialize_then_decompress_u_a80( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_d2 u_as_ntt[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - u_as_ntt[i] = ZERO_20_7d();); + u_as_ntt[i] = ZERO_ef_7d();); for (size_t i = (size_t)0U; i < Eurydice_slice_len( Eurydice_array_to_slice((size_t)768U, ciphertext, uint8_t), @@ -7581,13 +7592,13 @@ compute_message_a40( libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *v, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *secret_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_d2 *u_as_ntt) { - libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_20_7d(); + libcrux_ml_kem_polynomial_PolynomialRingElement_d2 result = ZERO_ef_7d(); KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_d2 product = - ntt_multiply_20_63(&secret_as_ntt[i0], &u_as_ntt[i0]); - add_to_ring_element_20_310(&result, &product);); + ntt_multiply_ef_63(&secret_as_ntt[i0], &u_as_ntt[i0]); + add_to_ring_element_ef_310(&result, &product);); invert_ntt_montgomery_0c0(&result); - result = subtract_reduce_20_27(v, result); + result = subtract_reduce_ef_27(v, result); return result; } diff --git a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h index b1d46ac81..705b94d1c 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_avx2.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.c b/libcrux-ml-kem/c/libcrux_mlkem_portable.c index f54504354..65f4405d5 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.c +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "internal/libcrux_mlkem_portable.h" @@ -79,7 +79,7 @@ libcrux_ml_kem_vector_portable_vector_type_from_i16_array( Eurydice_slice_to_array2( &dst, Eurydice_slice_subslice2(array, (size_t)0U, (size_t)16U, int16_t), Eurydice_slice, int16_t[16U]); - core_result_unwrap_41_30(dst, ret); + core_result_unwrap_26_30(dst, ret); memcpy(lit.elements, ret, (size_t)16U * sizeof(int16_t)); return lit; } @@ -2281,15 +2281,16 @@ libcrux_ml_kem_vector_portable_vector_type_clone_3b( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.ZERO_20 +A monomorphic instance of libcrux_ml_kem.polynomial.ZERO_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ -static libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ZERO_20_19(void) { +static libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ZERO_ef_19(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 lit; lit.coefficients[0U] = libcrux_ml_kem_vector_portable_ZERO_0d(); lit.coefficients[1U] = libcrux_ml_kem_vector_portable_ZERO_0d(); @@ -2318,7 +2319,7 @@ libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialize_to_reduced_ring_element_8a(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_ef_19(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)24U; i++) { size_t i0 = i; @@ -2369,7 +2370,7 @@ static KRML_MUSTINLINE void deserialize_ring_elements_reduced_out_611( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialized_pk[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - deserialized_pk[i] = ZERO_20_19();); + deserialized_pk[i] = ZERO_ef_19();); deserialize_ring_elements_reduced_bb(public_key, deserialized_pk); memcpy( ret, deserialized_pk, @@ -2609,20 +2610,20 @@ typedef struct IndCpaPrivateKeyUnpacked_42_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPrivateKeyUnpacked[TraitClause@0])} +K>[TraitClause@0, TraitClause@1])} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_f6 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_1a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 4 */ -static IndCpaPrivateKeyUnpacked_42 default_f6_a3(void) { +static IndCpaPrivateKeyUnpacked_42 default_1a_a3(void) { IndCpaPrivateKeyUnpacked_42 lit; - lit.secret_as_ntt[0U] = ZERO_20_19(); - lit.secret_as_ntt[1U] = ZERO_20_19(); - lit.secret_as_ntt[2U] = ZERO_20_19(); - lit.secret_as_ntt[3U] = ZERO_20_19(); + lit.secret_as_ntt[0U] = ZERO_ef_19(); + lit.secret_as_ntt[1U] = ZERO_ef_19(); + lit.secret_as_ntt[2U] = ZERO_ef_19(); + lit.secret_as_ntt[3U] = ZERO_ef_19(); return lit; } @@ -2641,40 +2642,40 @@ typedef struct IndCpaPublicKeyUnpacked_42_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPublicKeyUnpacked[TraitClause@0])#1} +K>[TraitClause@0, TraitClause@1])#1} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_85 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_8d with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 4 */ -static IndCpaPublicKeyUnpacked_42 default_85_6b(void) { +static IndCpaPublicKeyUnpacked_42 default_8d_6b(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - uu____0[i] = ZERO_20_19();); + uu____0[i] = ZERO_ef_19();); uint8_t uu____1[32U] = {0U}; IndCpaPublicKeyUnpacked_42 lit; memcpy( lit.t_as_ntt, uu____0, (size_t)4U * sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f0)); memcpy(lit.seed_for_A, uu____1, (size_t)32U * sizeof(uint8_t)); - lit.A[0U][0U] = ZERO_20_19(); - lit.A[0U][1U] = ZERO_20_19(); - lit.A[0U][2U] = ZERO_20_19(); - lit.A[0U][3U] = ZERO_20_19(); - lit.A[1U][0U] = ZERO_20_19(); - lit.A[1U][1U] = ZERO_20_19(); - lit.A[1U][2U] = ZERO_20_19(); - lit.A[1U][3U] = ZERO_20_19(); - lit.A[2U][0U] = ZERO_20_19(); - lit.A[2U][1U] = ZERO_20_19(); - lit.A[2U][2U] = ZERO_20_19(); - lit.A[2U][3U] = ZERO_20_19(); - lit.A[3U][0U] = ZERO_20_19(); - lit.A[3U][1U] = ZERO_20_19(); - lit.A[3U][2U] = ZERO_20_19(); - lit.A[3U][3U] = ZERO_20_19(); + lit.A[0U][0U] = ZERO_ef_19(); + lit.A[0U][1U] = ZERO_ef_19(); + lit.A[0U][2U] = ZERO_ef_19(); + lit.A[0U][3U] = ZERO_ef_19(); + lit.A[1U][0U] = ZERO_ef_19(); + lit.A[1U][1U] = ZERO_ef_19(); + lit.A[1U][2U] = ZERO_ef_19(); + lit.A[1U][3U] = ZERO_ef_19(); + lit.A[2U][0U] = ZERO_ef_19(); + lit.A[2U][1U] = ZERO_ef_19(); + lit.A[2U][2U] = ZERO_ef_19(); + lit.A[2U][3U] = ZERO_ef_19(); + lit.A[3U][0U] = ZERO_ef_19(); + lit.A[3U][1U] = ZERO_ef_19(); + lit.A[3U][2U] = ZERO_ef_19(); + lit.A[3U][3U] = ZERO_ef_19(); return lit; } @@ -2996,17 +2997,18 @@ static KRML_MUSTINLINE bool sample_from_uniform_distribution_next_fb0( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.from_i16_array_20 +A monomorphic instance of libcrux_ml_kem.polynomial.from_i16_array_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 -from_i16_array_20_bb(Eurydice_slice a) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_20_19(); +from_i16_array_ef_bb(Eurydice_slice a) { + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_ef_19(); for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; @@ -3028,7 +3030,7 @@ generics */ static libcrux_ml_kem_polynomial_PolynomialRingElement_f0 closure_ba( int16_t s[272U]) { - return from_i16_array_20_bb( + return from_i16_array_ef_bb( Eurydice_array_to_subslice2(s, (size_t)0U, (size_t)256U, int16_t)); } @@ -3197,7 +3199,7 @@ sample_from_binomial_distribution_2_1b(Eurydice_slice randomness) { sampled_i16s[(size_t)8U * chunk_number + offset] = outcome_1 - outcome_2; } } - return from_i16_array_20_bb( + return from_i16_array_ef_bb( Eurydice_array_to_slice((size_t)256U, sampled_i16s, int16_t)); } @@ -3241,7 +3243,7 @@ sample_from_binomial_distribution_3_ee(Eurydice_slice randomness) { sampled_i16s[(size_t)4U * chunk_number + offset] = outcome_1 - outcome_2; } } - return from_i16_array_20_bb( + return from_i16_array_ef_bb( Eurydice_array_to_slice((size_t)256U, sampled_i16s, int16_t)); } @@ -3407,15 +3409,16 @@ static KRML_MUSTINLINE void ntt_at_layer_1_21( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.poly_barrett_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.poly_barrett_reduce_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ -static KRML_MUSTINLINE void poly_barrett_reduce_20_0a( +static KRML_MUSTINLINE void poly_barrett_reduce_ef_0a( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self) { for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { @@ -3443,7 +3446,7 @@ static KRML_MUSTINLINE void ntt_binomially_sampled_ring_element_b3( ntt_at_layer_3_1b(&zeta_i, re); ntt_at_layer_2_ea(&zeta_i, re); ntt_at_layer_1_21(&zeta_i, re); - poly_barrett_reduce_20_0a(re); + poly_barrett_reduce_ef_0a(re); } /** @@ -3502,7 +3505,7 @@ static KRML_MUSTINLINE tuple_710 sample_vector_cbd_then_ntt_out_44( uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re_as_ntt[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - re_as_ntt[i] = ZERO_20_19();); + re_as_ntt[i] = ZERO_ef_19();); libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *uu____0 = re_as_ntt; uint8_t uu____1[33U]; memcpy(uu____1, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -3523,18 +3526,19 @@ static KRML_MUSTINLINE tuple_710 sample_vector_cbd_then_ntt_out_44( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.ntt_multiply_20 +A monomorphic instance of libcrux_ml_kem.polynomial.ntt_multiply_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 -ntt_multiply_20_76(libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, +ntt_multiply_ef_76(libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *rhs) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 out = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 out = ZERO_ef_19(); for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { size_t i0 = i; @@ -3555,15 +3559,16 @@ ntt_multiply_20_76(libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 4 */ -static KRML_MUSTINLINE void add_to_ring_element_20_3a( +static KRML_MUSTINLINE void add_to_ring_element_ef_3a( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *rhs) { for (size_t i = (size_t)0U; @@ -3596,15 +3601,16 @@ to_standard_domain_73( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_standard_error_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_standard_error_reduce_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ -static KRML_MUSTINLINE void add_standard_error_reduce_20_69( +static KRML_MUSTINLINE void add_standard_error_reduce_ef_69( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *error) { for (size_t i = (size_t)0U; @@ -3640,7 +3646,7 @@ static KRML_MUSTINLINE void compute_As_plus_e_f0( i++) { size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *row = matrix_A[i0]; - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0 = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0 = ZERO_ef_19(); t_as_ntt[i0] = uu____0; for (size_t i1 = (size_t)0U; i1 < Eurydice_slice_len( @@ -3653,10 +3659,10 @@ static KRML_MUSTINLINE void compute_As_plus_e_f0( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *matrix_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(matrix_element, &s_as_ntt[j]); - add_to_ring_element_20_3a(&t_as_ntt[i0], &product); + ntt_multiply_ef_76(matrix_element, &s_as_ntt[j]); + add_to_ring_element_ef_3a(&t_as_ntt[i0], &product); } - add_standard_error_reduce_20_69(&t_as_ntt[i0], &error_as_ntt[i0]); + add_standard_error_reduce_ef_69(&t_as_ntt[i0], &error_as_ntt[i0]); } } @@ -3709,7 +3715,7 @@ static void generate_keypair_unpacked_86( uint8_t uu____5[32U]; core_result_Result_00 dst; Eurydice_slice_to_array2(&dst, seed_for_A, Eurydice_slice, uint8_t[32U]); - core_result_unwrap_41_33(dst, uu____5); + core_result_unwrap_26_33(dst, uu____5); memcpy(public_key->seed_for_A, uu____5, (size_t)32U * sizeof(uint8_t)); } @@ -3727,8 +3733,8 @@ libcrux_ml_kem_variant_MlKem with const generics */ static libcrux_ml_kem_utils_extraction_helper_Keypair1024 generate_keypair_791( Eurydice_slice key_generation_seed) { - IndCpaPrivateKeyUnpacked_42 private_key = default_f6_a3(); - IndCpaPublicKeyUnpacked_42 public_key = default_85_6b(); + IndCpaPrivateKeyUnpacked_42 private_key = default_1a_a3(); + IndCpaPublicKeyUnpacked_42 public_key = default_8d_6b(); generate_keypair_unpacked_86(key_generation_seed, &private_key, &public_key); uint8_t public_key_serialized[1568U]; serialize_public_key_8c( @@ -3880,7 +3886,7 @@ static KRML_MUSTINLINE tuple_710 sample_ring_element_cbd_f9(uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 error_1[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - error_1[i] = ZERO_20_19();); + error_1[i] = ZERO_ef_19();); /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_prf_input[33U]; memcpy(copy_of_prf_input, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -4068,20 +4074,21 @@ static KRML_MUSTINLINE void invert_ntt_montgomery_45( invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)5U); invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)6U); invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)7U); - poly_barrett_reduce_20_0a(re); + poly_barrett_reduce_ef_0a(re); } /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_error_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_error_reduce_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ -static KRML_MUSTINLINE void add_error_reduce_20_bd( +static KRML_MUSTINLINE void add_error_reduce_ef_bd( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *error) { for (size_t i = (size_t)0U; @@ -4112,7 +4119,7 @@ static KRML_MUSTINLINE void compute_vector_u_cc( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result0[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - result0[i] = ZERO_20_19();); + result0[i] = ZERO_ef_19();); for (size_t i0 = (size_t)0U; i0 < Eurydice_slice_len( Eurydice_array_to_slice( @@ -4132,11 +4139,11 @@ static KRML_MUSTINLINE void compute_vector_u_cc( size_t j = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *a_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(a_element, &r_as_ntt[j]); - add_to_ring_element_20_3a(&result0[i1], &product); + ntt_multiply_ef_76(a_element, &r_as_ntt[j]); + add_to_ring_element_ef_3a(&result0[i1], &product); } invert_ntt_montgomery_45(&result0[i1]); - add_error_reduce_20_bd(&result0[i1], &error_1[i1]); + add_error_reduce_ef_bd(&result0[i1], &error_1[i1]); } libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result[4U]; memcpy( @@ -4173,7 +4180,7 @@ libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialize_then_decompress_message_52(uint8_t serialized[32U]) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_ef_19(); KRML_MAYBE_FOR16( i, (size_t)0U, (size_t)16U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_vector_portable_vector_type_PortableVector @@ -4190,16 +4197,17 @@ deserialize_then_decompress_message_52(uint8_t serialized[32U]) { /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_message_error_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_message_error_reduce_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 -add_message_error_reduce_20_42( +add_message_error_reduce_ef_42( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *message, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result) { @@ -4234,13 +4242,13 @@ compute_ring_element_v_14( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *r_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *error_2, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *message) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_ef_19(); KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(&t_as_ntt[i0], &r_as_ntt[i0]); - add_to_ring_element_20_3a(&result, &product);); + ntt_multiply_ef_76(&t_as_ntt[i0], &r_as_ntt[i0]); + add_to_ring_element_ef_3a(&result, &product);); invert_ntt_montgomery_45(&result); - result = add_message_error_reduce_20_42(error_2, message, result); + result = add_message_error_reduce_ef_42(error_2, message, result); return result; } @@ -4593,7 +4601,7 @@ generics */ static void encrypt_f41(Eurydice_slice public_key, uint8_t message[32U], Eurydice_slice randomness, uint8_t ret[1568U]) { - IndCpaPublicKeyUnpacked_42 unpacked_public_key = default_85_6b(); + IndCpaPublicKeyUnpacked_42 unpacked_public_key = default_8d_6b(); deserialize_ring_elements_reduced_bb( Eurydice_slice_subslice_to(public_key, (size_t)1536U, uint8_t, size_t), unpacked_public_key.t_as_ntt); @@ -4712,7 +4720,7 @@ libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialize_to_uncompressed_ring_element_7a(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_ef_19(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)24U; i++) { size_t i0 = i; @@ -4736,7 +4744,7 @@ static KRML_MUSTINLINE void deserialize_secret_key_a71( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 secret_as_ntt[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - secret_as_ntt[i] = ZERO_20_19();); + secret_as_ntt[i] = ZERO_ef_19();); for (size_t i = (size_t)0U; i < Eurydice_slice_len(secret_key, uint8_t) / LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT; @@ -4805,7 +4813,7 @@ libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialize_then_decompress_10_58(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_ef_19(); LowStar_Ignore_ignore( Eurydice_slice_len( Eurydice_array_to_slice( @@ -4872,7 +4880,7 @@ libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialize_then_decompress_11_5c(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_ef_19(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)22U; i++) { size_t i0 = i; @@ -4914,7 +4922,7 @@ static KRML_MUSTINLINE void ntt_vector_u_72( ntt_at_layer_3_1b(&zeta_i, re); ntt_at_layer_2_ea(&zeta_i, re); ntt_at_layer_1_21(&zeta_i, re); - poly_barrett_reduce_20_0a(re); + poly_barrett_reduce_ef_0a(re); } /** @@ -4930,7 +4938,7 @@ static KRML_MUSTINLINE void deserialize_then_decompress_u_1e( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[4U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 u_as_ntt[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, - u_as_ntt[i] = ZERO_20_19();); + u_as_ntt[i] = ZERO_ef_19();); for (size_t i = (size_t)0U; i < Eurydice_slice_len( Eurydice_array_to_slice((size_t)1568U, ciphertext, uint8_t), @@ -5001,7 +5009,7 @@ with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialize_then_decompress_4_6c(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_ef_19(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)8U; i++) { size_t i0 = i; @@ -5061,7 +5069,7 @@ with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialize_then_decompress_5_96(Eurydice_slice serialized) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re = ZERO_ef_19(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(serialized, uint8_t) / (size_t)10U; i++) { size_t i0 = i; @@ -5089,16 +5097,17 @@ deserialize_then_decompress_ring_element_v_ad(Eurydice_slice serialized) { /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.subtract_reduce_20 +A monomorphic instance of libcrux_ml_kem.polynomial.subtract_reduce_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics */ static KRML_MUSTINLINE libcrux_ml_kem_polynomial_PolynomialRingElement_f0 -subtract_reduce_20_87(libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, +subtract_reduce_ef_87(libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 b) { for (size_t i = (size_t)0U; i < LIBCRUX_ML_KEM_POLYNOMIAL_VECTORS_IN_RING_ELEMENT; i++) { @@ -5127,13 +5136,13 @@ compute_message_7e( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *v, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *secret_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *u_as_ntt) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_ef_19(); KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(&secret_as_ntt[i0], &u_as_ntt[i0]); - add_to_ring_element_20_3a(&result, &product);); + ntt_multiply_ef_76(&secret_as_ntt[i0], &u_as_ntt[i0]); + add_to_ring_element_ef_3a(&result, &product);); invert_ntt_montgomery_45(&result); - result = subtract_reduce_20_87(v, result); + result = subtract_reduce_ef_87(v, result); return result; } @@ -5371,7 +5380,7 @@ static KRML_MUSTINLINE void deserialize_ring_elements_reduced_out_610( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialized_pk[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - deserialized_pk[i] = ZERO_20_19();); + deserialized_pk[i] = ZERO_ef_19();); deserialize_ring_elements_reduced_bb0(public_key, deserialized_pk); memcpy( ret, deserialized_pk, @@ -5525,18 +5534,18 @@ typedef struct IndCpaPrivateKeyUnpacked_ae_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPrivateKeyUnpacked[TraitClause@0])} +K>[TraitClause@0, TraitClause@1])} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_f6 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_1a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 2 */ -static IndCpaPrivateKeyUnpacked_ae default_f6_a30(void) { +static IndCpaPrivateKeyUnpacked_ae default_1a_a30(void) { IndCpaPrivateKeyUnpacked_ae lit; - lit.secret_as_ntt[0U] = ZERO_20_19(); - lit.secret_as_ntt[1U] = ZERO_20_19(); + lit.secret_as_ntt[0U] = ZERO_ef_19(); + lit.secret_as_ntt[1U] = ZERO_ef_19(); return lit; } @@ -5555,28 +5564,28 @@ typedef struct IndCpaPublicKeyUnpacked_ae_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPublicKeyUnpacked[TraitClause@0])#1} +K>[TraitClause@0, TraitClause@1])#1} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_85 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_8d with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 2 */ -static IndCpaPublicKeyUnpacked_ae default_85_6b0(void) { +static IndCpaPublicKeyUnpacked_ae default_8d_6b0(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - uu____0[i] = ZERO_20_19();); + uu____0[i] = ZERO_ef_19();); uint8_t uu____1[32U] = {0U}; IndCpaPublicKeyUnpacked_ae lit; memcpy( lit.t_as_ntt, uu____0, (size_t)2U * sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f0)); memcpy(lit.seed_for_A, uu____1, (size_t)32U * sizeof(uint8_t)); - lit.A[0U][0U] = ZERO_20_19(); - lit.A[0U][1U] = ZERO_20_19(); - lit.A[1U][0U] = ZERO_20_19(); - lit.A[1U][1U] = ZERO_20_19(); + lit.A[0U][0U] = ZERO_ef_19(); + lit.A[0U][1U] = ZERO_ef_19(); + lit.A[1U][0U] = ZERO_ef_19(); + lit.A[1U][1U] = ZERO_ef_19(); return lit; } @@ -5905,7 +5914,7 @@ generics */ static libcrux_ml_kem_polynomial_PolynomialRingElement_f0 closure_ba0( int16_t s[272U]) { - return from_i16_array_20_bb( + return from_i16_array_ef_bb( Eurydice_array_to_subslice2(s, (size_t)0U, (size_t)256U, int16_t)); } @@ -6100,7 +6109,7 @@ static KRML_MUSTINLINE tuple_740 sample_vector_cbd_then_ntt_out_440( uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re_as_ntt[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - re_as_ntt[i] = ZERO_20_19();); + re_as_ntt[i] = ZERO_ef_19();); libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *uu____0 = re_as_ntt; uint8_t uu____1[33U]; memcpy(uu____1, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -6121,15 +6130,16 @@ static KRML_MUSTINLINE tuple_740 sample_vector_cbd_then_ntt_out_440( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 2 */ -static KRML_MUSTINLINE void add_to_ring_element_20_3a0( +static KRML_MUSTINLINE void add_to_ring_element_ef_3a0( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *rhs) { for (size_t i = (size_t)0U; @@ -6167,7 +6177,7 @@ static KRML_MUSTINLINE void compute_As_plus_e_f00( i++) { size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *row = matrix_A[i0]; - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0 = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0 = ZERO_ef_19(); t_as_ntt[i0] = uu____0; for (size_t i1 = (size_t)0U; i1 < Eurydice_slice_len( @@ -6180,10 +6190,10 @@ static KRML_MUSTINLINE void compute_As_plus_e_f00( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *matrix_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(matrix_element, &s_as_ntt[j]); - add_to_ring_element_20_3a0(&t_as_ntt[i0], &product); + ntt_multiply_ef_76(matrix_element, &s_as_ntt[j]); + add_to_ring_element_ef_3a0(&t_as_ntt[i0], &product); } - add_standard_error_reduce_20_69(&t_as_ntt[i0], &error_as_ntt[i0]); + add_standard_error_reduce_ef_69(&t_as_ntt[i0], &error_as_ntt[i0]); } } @@ -6236,7 +6246,7 @@ static void generate_keypair_unpacked_860( uint8_t uu____5[32U]; core_result_Result_00 dst; Eurydice_slice_to_array2(&dst, seed_for_A, Eurydice_slice, uint8_t[32U]); - core_result_unwrap_41_33(dst, uu____5); + core_result_unwrap_26_33(dst, uu____5); memcpy(public_key->seed_for_A, uu____5, (size_t)32U * sizeof(uint8_t)); } @@ -6254,8 +6264,8 @@ libcrux_ml_kem_variant_MlKem with const generics */ static libcrux_ml_kem_utils_extraction_helper_Keypair512 generate_keypair_790( Eurydice_slice key_generation_seed) { - IndCpaPrivateKeyUnpacked_ae private_key = default_f6_a30(); - IndCpaPublicKeyUnpacked_ae public_key = default_85_6b0(); + IndCpaPrivateKeyUnpacked_ae private_key = default_1a_a30(); + IndCpaPublicKeyUnpacked_ae public_key = default_8d_6b0(); generate_keypair_unpacked_860(key_generation_seed, &private_key, &public_key); uint8_t public_key_serialized[800U]; serialize_public_key_8c0( @@ -6439,7 +6449,7 @@ static KRML_MUSTINLINE tuple_740 sample_ring_element_cbd_f90(uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 error_1[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - error_1[i] = ZERO_20_19();); + error_1[i] = ZERO_ef_19();); /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_prf_input[33U]; memcpy(copy_of_prf_input, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -6503,7 +6513,7 @@ static KRML_MUSTINLINE void invert_ntt_montgomery_450( invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)5U); invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)6U); invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)7U); - poly_barrett_reduce_20_0a(re); + poly_barrett_reduce_ef_0a(re); } /** @@ -6519,7 +6529,7 @@ static KRML_MUSTINLINE void compute_vector_u_cc0( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result0[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - result0[i] = ZERO_20_19();); + result0[i] = ZERO_ef_19();); for (size_t i0 = (size_t)0U; i0 < Eurydice_slice_len( Eurydice_array_to_slice( @@ -6539,11 +6549,11 @@ static KRML_MUSTINLINE void compute_vector_u_cc0( size_t j = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *a_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(a_element, &r_as_ntt[j]); - add_to_ring_element_20_3a0(&result0[i1], &product); + ntt_multiply_ef_76(a_element, &r_as_ntt[j]); + add_to_ring_element_ef_3a0(&result0[i1], &product); } invert_ntt_montgomery_450(&result0[i1]); - add_error_reduce_20_bd(&result0[i1], &error_1[i1]); + add_error_reduce_ef_bd(&result0[i1], &error_1[i1]); } libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result[2U]; memcpy( @@ -6566,13 +6576,13 @@ compute_ring_element_v_140( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *r_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *error_2, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *message) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_ef_19(); KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(&t_as_ntt[i0], &r_as_ntt[i0]); - add_to_ring_element_20_3a0(&result, &product);); + ntt_multiply_ef_76(&t_as_ntt[i0], &r_as_ntt[i0]); + add_to_ring_element_ef_3a0(&result, &product);); invert_ntt_montgomery_450(&result); - result = add_message_error_reduce_20_42(error_2, message, result); + result = add_message_error_reduce_ef_42(error_2, message, result); return result; } @@ -6754,7 +6764,7 @@ generics */ static void encrypt_f40(Eurydice_slice public_key, uint8_t message[32U], Eurydice_slice randomness, uint8_t ret[768U]) { - IndCpaPublicKeyUnpacked_ae unpacked_public_key = default_85_6b0(); + IndCpaPublicKeyUnpacked_ae unpacked_public_key = default_8d_6b0(); deserialize_ring_elements_reduced_bb0( Eurydice_slice_subslice_to(public_key, (size_t)768U, uint8_t, size_t), unpacked_public_key.t_as_ntt); @@ -6876,7 +6886,7 @@ static KRML_MUSTINLINE void deserialize_secret_key_a70( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 secret_as_ntt[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - secret_as_ntt[i] = ZERO_20_19();); + secret_as_ntt[i] = ZERO_ef_19();); for (size_t i = (size_t)0U; i < Eurydice_slice_len(secret_key, uint8_t) / LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT; @@ -6927,7 +6937,7 @@ static KRML_MUSTINLINE void ntt_vector_u_720( ntt_at_layer_3_1b(&zeta_i, re); ntt_at_layer_2_ea(&zeta_i, re); ntt_at_layer_1_21(&zeta_i, re); - poly_barrett_reduce_20_0a(re); + poly_barrett_reduce_ef_0a(re); } /** @@ -6943,7 +6953,7 @@ static KRML_MUSTINLINE void deserialize_then_decompress_u_1e0( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[2U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 u_as_ntt[2U]; KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, - u_as_ntt[i] = ZERO_20_19();); + u_as_ntt[i] = ZERO_ef_19();); for (size_t i = (size_t)0U; i < Eurydice_slice_len( Eurydice_array_to_slice((size_t)768U, ciphertext, uint8_t), @@ -6991,13 +7001,13 @@ compute_message_7e0( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *v, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *secret_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *u_as_ntt) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_ef_19(); KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(&secret_as_ntt[i0], &u_as_ntt[i0]); - add_to_ring_element_20_3a0(&result, &product);); + ntt_multiply_ef_76(&secret_as_ntt[i0], &u_as_ntt[i0]); + add_to_ring_element_ef_3a0(&result, &product);); invert_ntt_montgomery_450(&result); - result = subtract_reduce_20_87(v, result); + result = subtract_reduce_ef_87(v, result); return result; } @@ -7195,7 +7205,7 @@ static KRML_MUSTINLINE void deserialize_ring_elements_reduced_out_61( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 deserialized_pk[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - deserialized_pk[i] = ZERO_20_19();); + deserialized_pk[i] = ZERO_ef_19();); deserialize_ring_elements_reduced_bb1(public_key, deserialized_pk); memcpy( ret, deserialized_pk, @@ -7349,19 +7359,19 @@ typedef struct IndCpaPrivateKeyUnpacked_f8_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPrivateKeyUnpacked[TraitClause@0])} +K>[TraitClause@0, TraitClause@1])} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_f6 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_1a with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 3 */ -static IndCpaPrivateKeyUnpacked_f8 default_f6_a31(void) { +static IndCpaPrivateKeyUnpacked_f8 default_1a_a31(void) { IndCpaPrivateKeyUnpacked_f8 lit; - lit.secret_as_ntt[0U] = ZERO_20_19(); - lit.secret_as_ntt[1U] = ZERO_20_19(); - lit.secret_as_ntt[2U] = ZERO_20_19(); + lit.secret_as_ntt[0U] = ZERO_ef_19(); + lit.secret_as_ntt[1U] = ZERO_ef_19(); + lit.secret_as_ntt[2U] = ZERO_ef_19(); return lit; } @@ -7380,33 +7390,33 @@ typedef struct IndCpaPublicKeyUnpacked_f8_s { /** This function found in impl {(core::default::Default for libcrux_ml_kem::ind_cpa::unpacked::IndCpaPublicKeyUnpacked[TraitClause@0])#1} +K>[TraitClause@0, TraitClause@1])#1} */ /** -A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_85 +A monomorphic instance of libcrux_ml_kem.ind_cpa.unpacked.default_8d with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 3 */ -static IndCpaPublicKeyUnpacked_f8 default_85_6b1(void) { +static IndCpaPublicKeyUnpacked_f8 default_8d_6b1(void) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - uu____0[i] = ZERO_20_19();); + uu____0[i] = ZERO_ef_19();); uint8_t uu____1[32U] = {0U}; IndCpaPublicKeyUnpacked_f8 lit; memcpy( lit.t_as_ntt, uu____0, (size_t)3U * sizeof(libcrux_ml_kem_polynomial_PolynomialRingElement_f0)); memcpy(lit.seed_for_A, uu____1, (size_t)32U * sizeof(uint8_t)); - lit.A[0U][0U] = ZERO_20_19(); - lit.A[0U][1U] = ZERO_20_19(); - lit.A[0U][2U] = ZERO_20_19(); - lit.A[1U][0U] = ZERO_20_19(); - lit.A[1U][1U] = ZERO_20_19(); - lit.A[1U][2U] = ZERO_20_19(); - lit.A[2U][0U] = ZERO_20_19(); - lit.A[2U][1U] = ZERO_20_19(); - lit.A[2U][2U] = ZERO_20_19(); + lit.A[0U][0U] = ZERO_ef_19(); + lit.A[0U][1U] = ZERO_ef_19(); + lit.A[0U][2U] = ZERO_ef_19(); + lit.A[1U][0U] = ZERO_ef_19(); + lit.A[1U][1U] = ZERO_ef_19(); + lit.A[1U][2U] = ZERO_ef_19(); + lit.A[2U][0U] = ZERO_ef_19(); + lit.A[2U][1U] = ZERO_ef_19(); + lit.A[2U][2U] = ZERO_ef_19(); return lit; } @@ -7735,7 +7745,7 @@ generics */ static libcrux_ml_kem_polynomial_PolynomialRingElement_f0 closure_ba1( int16_t s[272U]) { - return from_i16_array_20_bb( + return from_i16_array_ef_bb( Eurydice_array_to_subslice2(s, (size_t)0U, (size_t)256U, int16_t)); } @@ -7919,7 +7929,7 @@ static KRML_MUSTINLINE tuple_b00 sample_vector_cbd_then_ntt_out_441( uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 re_as_ntt[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - re_as_ntt[i] = ZERO_20_19();); + re_as_ntt[i] = ZERO_ef_19();); libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *uu____0 = re_as_ntt; uint8_t uu____1[33U]; memcpy(uu____1, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -7940,15 +7950,16 @@ static KRML_MUSTINLINE tuple_b00 sample_vector_cbd_then_ntt_out_441( /** This function found in impl -{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0]#2} +{libcrux_ml_kem::polynomial::PolynomialRingElement[TraitClause@0, +TraitClause@1]#2} */ /** -A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_20 +A monomorphic instance of libcrux_ml_kem.polynomial.add_to_ring_element_ef with types libcrux_ml_kem_vector_portable_vector_type_PortableVector with const generics - K= 3 */ -static KRML_MUSTINLINE void add_to_ring_element_20_3a1( +static KRML_MUSTINLINE void add_to_ring_element_ef_3a1( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *self, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *rhs) { for (size_t i = (size_t)0U; @@ -7986,7 +7997,7 @@ static KRML_MUSTINLINE void compute_As_plus_e_f01( i++) { size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *row = matrix_A[i0]; - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0 = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 uu____0 = ZERO_ef_19(); t_as_ntt[i0] = uu____0; for (size_t i1 = (size_t)0U; i1 < Eurydice_slice_len( @@ -7999,10 +8010,10 @@ static KRML_MUSTINLINE void compute_As_plus_e_f01( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *matrix_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(matrix_element, &s_as_ntt[j]); - add_to_ring_element_20_3a1(&t_as_ntt[i0], &product); + ntt_multiply_ef_76(matrix_element, &s_as_ntt[j]); + add_to_ring_element_ef_3a1(&t_as_ntt[i0], &product); } - add_standard_error_reduce_20_69(&t_as_ntt[i0], &error_as_ntt[i0]); + add_standard_error_reduce_ef_69(&t_as_ntt[i0], &error_as_ntt[i0]); } } @@ -8055,7 +8066,7 @@ static void generate_keypair_unpacked_861( uint8_t uu____5[32U]; core_result_Result_00 dst; Eurydice_slice_to_array2(&dst, seed_for_A, Eurydice_slice, uint8_t[32U]); - core_result_unwrap_41_33(dst, uu____5); + core_result_unwrap_26_33(dst, uu____5); memcpy(public_key->seed_for_A, uu____5, (size_t)32U * sizeof(uint8_t)); } @@ -8073,8 +8084,8 @@ libcrux_ml_kem_variant_MlKem with const generics */ static libcrux_ml_kem_utils_extraction_helper_Keypair768 generate_keypair_79( Eurydice_slice key_generation_seed) { - IndCpaPrivateKeyUnpacked_f8 private_key = default_f6_a31(); - IndCpaPublicKeyUnpacked_f8 public_key = default_85_6b1(); + IndCpaPrivateKeyUnpacked_f8 private_key = default_1a_a31(); + IndCpaPublicKeyUnpacked_f8 public_key = default_8d_6b1(); generate_keypair_unpacked_861(key_generation_seed, &private_key, &public_key); uint8_t public_key_serialized[1184U]; serialize_public_key_8c1( @@ -8226,7 +8237,7 @@ static KRML_MUSTINLINE tuple_b00 sample_ring_element_cbd_f91(uint8_t prf_input[33U], uint8_t domain_separator) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 error_1[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - error_1[i] = ZERO_20_19();); + error_1[i] = ZERO_ef_19();); /* Passing arrays by value in Rust generates a copy in C */ uint8_t copy_of_prf_input[33U]; memcpy(copy_of_prf_input, prf_input, (size_t)33U * sizeof(uint8_t)); @@ -8290,7 +8301,7 @@ static KRML_MUSTINLINE void invert_ntt_montgomery_451( invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)5U); invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)6U); invert_ntt_at_layer_4_plus_8c(&zeta_i, re, (size_t)7U); - poly_barrett_reduce_20_0a(re); + poly_barrett_reduce_ef_0a(re); } /** @@ -8306,7 +8317,7 @@ static KRML_MUSTINLINE void compute_vector_u_cc1( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result0[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - result0[i] = ZERO_20_19();); + result0[i] = ZERO_ef_19();); for (size_t i0 = (size_t)0U; i0 < Eurydice_slice_len( Eurydice_array_to_slice( @@ -8326,11 +8337,11 @@ static KRML_MUSTINLINE void compute_vector_u_cc1( size_t j = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *a_element = &row[j]; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(a_element, &r_as_ntt[j]); - add_to_ring_element_20_3a1(&result0[i1], &product); + ntt_multiply_ef_76(a_element, &r_as_ntt[j]); + add_to_ring_element_ef_3a1(&result0[i1], &product); } invert_ntt_montgomery_451(&result0[i1]); - add_error_reduce_20_bd(&result0[i1], &error_1[i1]); + add_error_reduce_ef_bd(&result0[i1], &error_1[i1]); } libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result[3U]; memcpy( @@ -8353,13 +8364,13 @@ compute_ring_element_v_141( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *r_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *error_2, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *message) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_ef_19(); KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(&t_as_ntt[i0], &r_as_ntt[i0]); - add_to_ring_element_20_3a1(&result, &product);); + ntt_multiply_ef_76(&t_as_ntt[i0], &r_as_ntt[i0]); + add_to_ring_element_ef_3a1(&result, &product);); invert_ntt_montgomery_451(&result); - result = add_message_error_reduce_20_42(error_2, message, result); + result = add_message_error_reduce_ef_42(error_2, message, result); return result; } @@ -8490,7 +8501,7 @@ generics */ static void encrypt_f4(Eurydice_slice public_key, uint8_t message[32U], Eurydice_slice randomness, uint8_t ret[1088U]) { - IndCpaPublicKeyUnpacked_f8 unpacked_public_key = default_85_6b1(); + IndCpaPublicKeyUnpacked_f8 unpacked_public_key = default_8d_6b1(); deserialize_ring_elements_reduced_bb1( Eurydice_slice_subslice_to(public_key, (size_t)1152U, uint8_t, size_t), unpacked_public_key.t_as_ntt); @@ -8612,7 +8623,7 @@ static KRML_MUSTINLINE void deserialize_secret_key_a7( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 secret_as_ntt[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - secret_as_ntt[i] = ZERO_20_19();); + secret_as_ntt[i] = ZERO_ef_19();); for (size_t i = (size_t)0U; i < Eurydice_slice_len(secret_key, uint8_t) / LIBCRUX_ML_KEM_CONSTANTS_BYTES_PER_RING_ELEMENT; @@ -8649,7 +8660,7 @@ static KRML_MUSTINLINE void deserialize_then_decompress_u_1e1( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 ret[3U]) { libcrux_ml_kem_polynomial_PolynomialRingElement_f0 u_as_ntt[3U]; KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, - u_as_ntt[i] = ZERO_20_19();); + u_as_ntt[i] = ZERO_ef_19();); for (size_t i = (size_t)0U; i < Eurydice_slice_len( Eurydice_array_to_slice((size_t)1088U, ciphertext, uint8_t), @@ -8686,13 +8697,13 @@ compute_message_7e1( libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *v, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *secret_as_ntt, libcrux_ml_kem_polynomial_PolynomialRingElement_f0 *u_as_ntt) { - libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_20_19(); + libcrux_ml_kem_polynomial_PolynomialRingElement_f0 result = ZERO_ef_19(); KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, size_t i0 = i; libcrux_ml_kem_polynomial_PolynomialRingElement_f0 product = - ntt_multiply_20_76(&secret_as_ntt[i0], &u_as_ntt[i0]); - add_to_ring_element_20_3a1(&result, &product);); + ntt_multiply_ef_76(&secret_as_ntt[i0], &u_as_ntt[i0]); + add_to_ring_element_ef_3a1(&result, &product);); invert_ntt_montgomery_451(&result); - result = subtract_reduce_20_87(v, result); + result = subtract_reduce_ef_87(v, result); return result; } diff --git a/libcrux-ml-kem/c/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/libcrux_mlkem_portable.h index 148c73ed6..850ef79ff 100644 --- a/libcrux-ml-kem/c/libcrux_mlkem_portable.h +++ b/libcrux-ml-kem/c/libcrux_mlkem_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem_portable_H diff --git a/libcrux-ml-kem/c/libcrux_sha3.h b/libcrux-ml-kem/c/libcrux_sha3.h index 7c2339260..3c9d12e58 100644 --- a/libcrux-ml-kem/c/libcrux_sha3.h +++ b/libcrux-ml-kem/c/libcrux_sha3.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_sha3_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.c b/libcrux-ml-kem/c/libcrux_sha3_avx2.c index 1ff80c854..b246030f2 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.c +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "internal/libcrux_sha3_avx2.h" @@ -167,16 +167,16 @@ split_at_mut_n_ef(Eurydice_slice a[4U], size_t mid) { */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0]#1} +N>[TraitClause@0, TraitClause@1]#1} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.new_1e +A monomorphic instance of libcrux_sha3.generic_keccak.new_89 with types core_core_arch_x86___m256i with const generics - N= 4 */ static KRML_MUSTINLINE libcrux_sha3_generic_keccak_KeccakState_29 -new_1e_71(void) { +new_89_71(void) { libcrux_sha3_generic_keccak_KeccakState_29 lit; lit.st[0U][0U] = zero_ef(); lit.st[0U][1U] = zero_ef(); @@ -1679,7 +1679,7 @@ with const generics */ static KRML_MUSTINLINE void keccak_b9(Eurydice_slice data[4U], Eurydice_slice out[4U]) { - libcrux_sha3_generic_keccak_KeccakState_29 s = new_1e_71(); + libcrux_sha3_generic_keccak_KeccakState_29 s = new_89_71(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(data[0U], uint8_t) / (size_t)136U; i++) { size_t i0 = i; @@ -1719,7 +1719,7 @@ static KRML_MUSTINLINE void keccak_b9(Eurydice_slice data[4U], .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -1757,7 +1757,7 @@ void libcrux_sha3_avx2_x4_shake256(Eurydice_slice input0, Eurydice_slice input1, */ libcrux_sha3_generic_keccak_KeccakState_29 libcrux_sha3_avx2_x4_incremental_init(void) { - return new_1e_71(); + return new_89_71(); } /** diff --git a/libcrux-ml-kem/c/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/libcrux_sha3_avx2.h index 4a83c4c39..ae63d5635 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/c/libcrux_sha3_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_sha3_avx2_H diff --git a/libcrux-ml-kem/c/libcrux_sha3_internal.h b/libcrux-ml-kem/c/libcrux_sha3_internal.h index 2986801bc..1ccb6aef7 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_internal.h +++ b/libcrux-ml-kem/c/libcrux_sha3_internal.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_sha3_internal_H @@ -192,16 +192,16 @@ typedef struct libcrux_sha3_generic_keccak_KeccakState_48_s { */ /** This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0]#1} +N>[TraitClause@0, TraitClause@1]#1} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.new_1e +A monomorphic instance of libcrux_sha3.generic_keccak.new_89 with types uint64_t with const generics - N= 1 */ static KRML_MUSTINLINE libcrux_sha3_generic_keccak_KeccakState_48 -libcrux_sha3_generic_keccak_new_1e_cf(void) { +libcrux_sha3_generic_keccak_new_89_cf(void) { libcrux_sha3_generic_keccak_KeccakState_48 lit; lit.st[0U][0U] = libcrux_sha3_portable_keccak_zero_5a(); lit.st[0U][1U] = libcrux_sha3_portable_keccak_zero_5a(); @@ -247,7 +247,7 @@ static KRML_MUSTINLINE void libcrux_sha3_portable_keccak_load_block_65( Eurydice_slice_subslice2(blocks[0U], (size_t)8U * i0, (size_t)8U * i0 + (size_t)8U, uint8_t), Eurydice_slice, uint8_t[8U]); - core_result_unwrap_41_0e(dst, uu____0); + core_result_unwrap_26_0e(dst, uu____0); size_t uu____1 = i0 / (size_t)5U; size_t uu____2 = i0 % (size_t)5U; s[uu____1][uu____2] = @@ -1465,7 +1465,7 @@ static KRML_MUSTINLINE void libcrux_sha3_portable_keccak_load_block_650( Eurydice_slice_subslice2(blocks[0U], (size_t)8U * i0, (size_t)8U * i0 + (size_t)8U, uint8_t), Eurydice_slice, uint8_t[8U]); - core_result_unwrap_41_0e(dst, uu____0); + core_result_unwrap_26_0e(dst, uu____0); size_t uu____1 = i0 / (size_t)5U; size_t uu____2 = i0 % (size_t)5U; s[uu____1][uu____2] = @@ -1740,7 +1740,7 @@ with const generics static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_064( Eurydice_slice data[1U], Eurydice_slice out[1U]) { libcrux_sha3_generic_keccak_KeccakState_48 s = - libcrux_sha3_generic_keccak_new_1e_cf(); + libcrux_sha3_generic_keccak_new_89_cf(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(data[0U], uint8_t) / (size_t)168U; i++) { size_t i0 = i; @@ -1781,7 +1781,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_064( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -1832,7 +1832,7 @@ static KRML_MUSTINLINE void libcrux_sha3_portable_keccak_load_block_653( Eurydice_slice_subslice2(blocks[0U], (size_t)8U * i0, (size_t)8U * i0 + (size_t)8U, uint8_t), Eurydice_slice, uint8_t[8U]); - core_result_unwrap_41_0e(dst, uu____0); + core_result_unwrap_26_0e(dst, uu____0); size_t uu____1 = i0 / (size_t)5U; size_t uu____2 = i0 % (size_t)5U; s[uu____1][uu____2] = @@ -2089,7 +2089,7 @@ with const generics static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_063( Eurydice_slice data[1U], Eurydice_slice out[1U]) { libcrux_sha3_generic_keccak_KeccakState_48 s = - libcrux_sha3_generic_keccak_new_1e_cf(); + libcrux_sha3_generic_keccak_new_89_cf(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(data[0U], uint8_t) / (size_t)104U; i++) { size_t i0 = i; @@ -2130,7 +2130,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_063( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -2181,7 +2181,7 @@ static KRML_MUSTINLINE void libcrux_sha3_portable_keccak_load_block_652( Eurydice_slice_subslice2(blocks[0U], (size_t)8U * i0, (size_t)8U * i0 + (size_t)8U, uint8_t), Eurydice_slice, uint8_t[8U]); - core_result_unwrap_41_0e(dst, uu____0); + core_result_unwrap_26_0e(dst, uu____0); size_t uu____1 = i0 / (size_t)5U; size_t uu____2 = i0 % (size_t)5U; s[uu____1][uu____2] = @@ -2438,7 +2438,7 @@ with const generics static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_062( Eurydice_slice data[1U], Eurydice_slice out[1U]) { libcrux_sha3_generic_keccak_KeccakState_48 s = - libcrux_sha3_generic_keccak_new_1e_cf(); + libcrux_sha3_generic_keccak_new_89_cf(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(data[0U], uint8_t) / (size_t)144U; i++) { size_t i0 = i; @@ -2479,7 +2479,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_062( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -2627,7 +2627,7 @@ with const generics static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_061( Eurydice_slice data[1U], Eurydice_slice out[1U]) { libcrux_sha3_generic_keccak_KeccakState_48 s = - libcrux_sha3_generic_keccak_new_1e_cf(); + libcrux_sha3_generic_keccak_new_89_cf(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(data[0U], uint8_t) / (size_t)136U; i++) { size_t i0 = i; @@ -2668,7 +2668,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_061( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -2745,7 +2745,7 @@ with const generics static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_060( Eurydice_slice data[1U], Eurydice_slice out[1U]) { libcrux_sha3_generic_keccak_KeccakState_48 s = - libcrux_sha3_generic_keccak_new_1e_cf(); + libcrux_sha3_generic_keccak_new_89_cf(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(data[0U], uint8_t) / (size_t)136U; i++) { size_t i0 = i; @@ -2786,7 +2786,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_060( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; @@ -2837,7 +2837,7 @@ static KRML_MUSTINLINE void libcrux_sha3_portable_keccak_load_block_651( Eurydice_slice_subslice2(blocks[0U], (size_t)8U * i0, (size_t)8U * i0 + (size_t)8U, uint8_t), Eurydice_slice, uint8_t[8U]); - core_result_unwrap_41_0e(dst, uu____0); + core_result_unwrap_26_0e(dst, uu____0); size_t uu____1 = i0 / (size_t)5U; size_t uu____2 = i0 % (size_t)5U; s[uu____1][uu____2] = @@ -3093,7 +3093,7 @@ with const generics static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_06( Eurydice_slice data[1U], Eurydice_slice out[1U]) { libcrux_sha3_generic_keccak_KeccakState_48 s = - libcrux_sha3_generic_keccak_new_1e_cf(); + libcrux_sha3_generic_keccak_new_89_cf(); for (size_t i = (size_t)0U; i < Eurydice_slice_len(data[0U], uint8_t) / (size_t)72U; i++) { size_t i0 = i; @@ -3134,7 +3134,7 @@ static KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccak_06( .end = blocks}), core_ops_range_Range_b3, core_ops_range_Range_b3); while (true) { - if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___6__next( + if (core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( &iter, size_t, core_option_Option_b3) .tag == core_option_None) { break; diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.c b/libcrux-ml-kem/c/libcrux_sha3_neon.c index ebfa2320d..e84736e6c 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.c +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.c @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #include "libcrux_sha3_neon.h" diff --git a/libcrux-ml-kem/c/libcrux_sha3_neon.h b/libcrux-ml-kem/c/libcrux_sha3_neon.h index 6756fcc4b..dcf61fdac 100644 --- a/libcrux-ml-kem/c/libcrux_sha3_neon.h +++ b/libcrux-ml-kem/c/libcrux_sha3_neon.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: b351338f6a84c7a1afc27433eb0ffdc668b3581d - * Eurydice: 7efec1624422fd5e94388ef06b9c76dfe7a48d46 - * Karamel: c96fb69d15693284644d6aecaa90afa37e4de8f0 + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 + * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 9e07b1b2962c1f8d7ad6c5cacb94bd68fd4d8a3d + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_sha3_neon_H diff --git a/libcrux-ml-kem/cg/code_gen.txt b/libcrux-ml-kem/cg/code_gen.txt index cfb1412a1..e4e28910d 100644 --- a/libcrux-ml-kem/cg/code_gen.txt +++ b/libcrux-ml-kem/cg/code_gen.txt @@ -1,6 +1,6 @@ This code was generated with the following revisions: -Charon: 1bd0af95285033fec42133810440d56977c17ade +Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac -Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 +Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd -Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 +Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 diff --git a/libcrux-ml-kem/cg/libcrux_core.h b/libcrux-ml-kem/cg/libcrux_core.h index c34810389..167e6f0ec 100644 --- a/libcrux-ml-kem/cg/libcrux_core.h +++ b/libcrux-ml-kem/cg/libcrux_core.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_core_H diff --git a/libcrux-ml-kem/cg/libcrux_ct_ops.h b/libcrux-ml-kem/cg/libcrux_ct_ops.h index 8d410ee3b..be254be76 100644 --- a/libcrux-ml-kem/cg/libcrux_ct_ops.h +++ b/libcrux-ml-kem/cg/libcrux_ct_ops.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #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 af0f83010..31e79d8fb 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem768_avx2_H diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h index 25b048abc..9d502829e 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_avx2_types.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem768_avx2_types_H diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h index ded408c91..32f0d2918 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem768_portable_H diff --git a/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h b/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h index 026ba1bf6..b8421f790 100644 --- a/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h +++ b/libcrux-ml-kem/cg/libcrux_mlkem768_portable_types.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_mlkem768_portable_types_H diff --git a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h index 4343a48cd..5b77b14b3 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_avx2.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #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 10e5c1870..eb7601a34 100644 --- a/libcrux-ml-kem/cg/libcrux_sha3_portable.h +++ b/libcrux-ml-kem/cg/libcrux_sha3_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 1bd0af95285033fec42133810440d56977c17ade + * Charon: 28d543bfacc902ba9cc2a734b76baae9583892a4 * Eurydice: 1a65dbf3758fe310833718c645a64266294a29ac - * Karamel: baec61db14d5132ae8eb4bd7a288638b7f2f1db8 + * Karamel: 15d4bce74a2d43e34a64f48f8311b7d9bcb0e152 * F*: 650b216aeb5901ec6f1c44ff275acd924e54bdbd - * Libcrux: 5971b6982c7af3edf6b84c36aa90697e599288a4 + * Libcrux: ff16b9e8164d0fd89efabd103d4a6c874df0c127 */ #ifndef __libcrux_sha3_portable_H