diff --git a/libcrux/include/Eurydice.h b/libcrux/include/Eurydice.h deleted file mode 100644 index fdfac190..00000000 --- a/libcrux/include/Eurydice.h +++ /dev/null @@ -1,20 +0,0 @@ -/* - This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc - F* version: a32b316e - KaRaMeL version: abb38e1d - */ - -#ifndef __Eurydice_H -#define __Eurydice_H - -#include "core.h" -#include "eurydice_glue.h" - -extern uint8_t Eurydice_bitand_pv_u8(uint8_t *x, uint8_t y); - -extern uint8_t Eurydice_shr_pv_u8(uint8_t *x, int32_t y); - - -#define __Eurydice_H_DEFINED -#endif diff --git a/libcrux/include/core.h b/libcrux/include/core.h index 73918cdd..5f8eead8 100644 --- a/libcrux/include/core.h +++ b/libcrux/include/core.h @@ -1,8 +1,8 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc - F* version: a32b316e - KaRaMeL version: abb38e1d + KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc + F* version: c990b3ca + KaRaMeL version: 391b72f8 */ #ifndef __core_H @@ -10,11 +10,6 @@ #include "eurydice_glue.h" -#define core_option_None 0 -#define core_option_Some 1 - -typedef uint8_t core_option_Option__size_t_tags; - typedef struct core_ops_range_Range__size_t_s { size_t start; @@ -22,6 +17,15 @@ typedef struct core_ops_range_Range__size_t_s } core_ops_range_Range__size_t; +extern uint8_t Eurydice_bitand_pv_u8(uint8_t *x, uint8_t y); + +extern uint8_t Eurydice_shr_pv_u8(uint8_t *x, int32_t y); + +#define core_option_None 0 +#define core_option_Some 1 + +typedef uint8_t core_option_Option__size_t_tags; + #define __core_H_DEFINED #endif diff --git a/libcrux/include/eurydice_glue.h b/libcrux/include/eurydice_glue.h index edeeec63..6a215745 100644 --- a/libcrux/include/eurydice_glue.h +++ b/libcrux/include/eurydice_glue.h @@ -61,6 +61,7 @@ typedef struct } result_tryfromslice_flexible; +// See note in karamel/lib/Inlining.ml if you change this #define Eurydice_slice_to_array2(dst, src, _, t_arr, _ret_t) Eurydice_slice_to_array3((result_tryfromslice_flexible *)dst, src, sizeof(t_arr)) static inline void Eurydice_slice_to_array3(result_tryfromslice_flexible *dst, Eurydice_slice src, size_t sz) { @@ -103,6 +104,7 @@ static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) { return (*p) >> #define core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__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 Eurydice_into_iter diff --git a/libcrux/include/internal/core.h b/libcrux/include/internal/core.h index 22761ec2..753361d3 100644 --- a/libcrux/include/internal/core.h +++ b/libcrux/include/internal/core.h @@ -1,8 +1,8 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc - F* version: a32b316e - KaRaMeL version: abb38e1d + KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc + F* version: c990b3ca + KaRaMeL version: 391b72f8 */ #ifndef __internal_core_H diff --git a/libcrux/include/internal/libcrux_kyber.h b/libcrux/include/internal/libcrux_kyber.h index 1c7c5ad8..c1c738ad 100644 --- a/libcrux/include/internal/libcrux_kyber.h +++ b/libcrux/include/internal/libcrux_kyber.h @@ -1,8 +1,8 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc - F* version: a32b316e - KaRaMeL version: abb38e1d + KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc + F* version: c990b3ca + KaRaMeL version: 391b72f8 */ #ifndef __internal_libcrux_kyber_H diff --git a/libcrux/include/libcrux_digest.h b/libcrux/include/libcrux_digest.h index 1764499a..eb83dc0a 100644 --- a/libcrux/include/libcrux_digest.h +++ b/libcrux/include/libcrux_digest.h @@ -1,8 +1,8 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc - F* version: a32b316e - KaRaMeL version: abb38e1d + KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc + F* version: c990b3ca + KaRaMeL version: 391b72f8 */ #ifndef __libcrux_digest_H diff --git a/libcrux/include/libcrux_hacl_glue.h b/libcrux/include/libcrux_hacl_glue.h index 7f7ba34b..753e98eb 100644 --- a/libcrux/include/libcrux_hacl_glue.h +++ b/libcrux/include/libcrux_hacl_glue.h @@ -2,7 +2,7 @@ #pragma once -#include "Eurydice.h" +#include "eurydice_glue.h" #include #include diff --git a/libcrux/include/libcrux_kyber.h b/libcrux/include/libcrux_kyber.h index 56483138..23c7d603 100644 --- a/libcrux/include/libcrux_kyber.h +++ b/libcrux/include/libcrux_kyber.h @@ -1,14 +1,13 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config - ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: a32b316e KaRaMeL version: - abb38e1d + KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config + ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: c990b3ca KaRaMeL version: + 391b72f8 */ #ifndef __libcrux_kyber_H #define __libcrux_kyber_H -#include "Eurydice.h" #include "core.h" #include "eurydice_glue.h" #include "libcrux_digest.h" @@ -86,6 +85,25 @@ typedef struct libcrux_kyber_types_MlKemKeyPair___2400size_t_1184size_t_s libcrux_kyber_types_MlKemKeyPair___2400size_t_1184size_t libcrux_kyber_kyber768_generate_key_pair(uint8_t randomness[64U]); +typedef struct libcrux_kyber_MlKemState___3size_t_s +{ + int32_t secret_as_ntt[3U][256U]; + int32_t t_as_ntt[3U][256U]; + int32_t a_transpose[3U][3U][256U]; + uint8_t rej[32U]; + uint8_t ind_cpa_public_key_hash[32U]; +} libcrux_kyber_MlKemState___3size_t; + +typedef struct + K___libcrux_kyber_MlKemState__3size_t___libcrux_kyber_types_MlKemPublicKey__1184size_t___s +{ + libcrux_kyber_MlKemState___3size_t fst; + uint8_t snd[1184U]; +} K___libcrux_kyber_MlKemState__3size_t___libcrux_kyber_types_MlKemPublicKey__1184size_t__; + +K___libcrux_kyber_MlKemState__3size_t___libcrux_kyber_types_MlKemPublicKey__1184size_t__ +libcrux_kyber_kyber768_generate_key_pair_unpacked(uint8_t randomness[64U]); + typedef struct K___libcrux_kyber_types_MlKemCiphertext__1088size_t___uint8_t_32size_t__s { @@ -101,6 +119,12 @@ void libcrux_kyber_kyber768_decapsulate(uint8_t (*secret_key)[2400U], uint8_t (*ciphertext)[1088U], uint8_t ret[32U]); +void +libcrux_kyber_kyber768_decapsulate_unpacked( + libcrux_kyber_MlKemState___3size_t* state, + uint8_t (*ciphertext)[1088U], + uint8_t ret[32U]); + extern libcrux_digest_incremental_x4_Shake128StateX4 libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__new( void); @@ -114,7 +138,7 @@ extern void libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__absorb_final_( size_t x0, libcrux_digest_incremental_x4_Shake128StateX4* x1, - Eurydice_slice x2[3U]); + Eurydice_slice* x2); extern void libcrux_digest_incremental_x4__libcrux__digest__incremental_x4__Shake128StateX4__free_memory( diff --git a/libcrux/src/Eurydice.c b/libcrux/src/Eurydice.c deleted file mode 100644 index e1a2df79..00000000 --- a/libcrux/src/Eurydice.c +++ /dev/null @@ -1,13 +0,0 @@ -/* - This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc - F* version: a32b316e - KaRaMeL version: f1b60dfc - */ - -#include "Eurydice.h" - -typedef size_t RangeTo__size_t; - -typedef size_t RangeFrom__size_t; - diff --git a/libcrux/src/core.c b/libcrux/src/core.c index 6f2656d1..e44f3393 100644 --- a/libcrux/src/core.c +++ b/libcrux/src/core.c @@ -1,12 +1,13 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc - F* version: a32b316e - KaRaMeL version: abb38e1d + KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc + F* version: c990b3ca + KaRaMeL version: 391b72f8 */ #include "internal/core.h" +typedef size_t RangeTo__size_t; + typedef size_t RangeFrom__size_t; -typedef size_t RangeTo__size_t; diff --git a/libcrux/src/libcrux_kyber.c b/libcrux/src/libcrux_kyber.c index 5048f56b..3e4ce164 100644 --- a/libcrux/src/libcrux_kyber.c +++ b/libcrux/src/libcrux_kyber.c @@ -1,8 +1,8 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice --config - ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: a32b316e KaRaMeL version: - abb38e1d + KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config + ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: c990b3ca KaRaMeL version: + 391b72f8 */ #include "internal/libcrux_kyber.h" @@ -167,9 +167,7 @@ select_shared_secret_in_constant_time(Eurydice_slice lhs, out[i] = (uint32_t)uu____1 | ((uint32_t)uu____2[0U] & (uint32_t)~mask); } } - uint8_t uu____3[32U]; - memcpy(uu____3, out, (size_t)32U * sizeof(uint8_t)); - memcpy(ret, uu____3, (size_t)32U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)32U * sizeof(uint8_t)); } static void @@ -258,52 +256,7 @@ serialize_uncompressed_ring_element(int32_t re[256U], uint8_t ret[384U]) serialized[(size_t)3U * i + (size_t)2U] = coef3; } } - uint8_t uu____2[384U]; - memcpy(uu____2, serialized, (size_t)384U * sizeof(uint8_t)); - memcpy(ret, uu____2, (size_t)384U * sizeof(uint8_t)); -} - -static void -deserialize_to_uncompressed_ring_element(Eurydice_slice serialized, - int32_t ret[256U]) -{ - int32_t re[256U]; - memcpy(re, ZERO, (size_t)256U * sizeof(int32_t)); - core_ops_range_Range__size_t iter = - core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( - ((core_ops_range_Range__size_t){ - .start = (size_t)0U, - .end = core_slice___Slice_T___len(serialized, uint8_t, size_t) / - (size_t)3U }), - core_ops_range_Range__size_t, - core_ops_range_Range__size_t); - while (true) { - core_option_Option__size_t uu____0 = - core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( - &iter, size_t, core_option_Option__size_t); - if (uu____0.tag == core_option_None) { - break; - } else { - size_t i = uu____0.f0; - Eurydice_slice bytes = Eurydice_slice_subslice( - serialized, - ((core_ops_range_Range__size_t){ .start = i * (size_t)3U, - .end = i * (size_t)3U + (size_t)3U }), - uint8_t, - core_ops_range_Range__size_t, - Eurydice_slice); - int32_t byte1 = - (int32_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t); - int32_t byte2 = - (int32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t); - int32_t byte3 = - (int32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t); - re[(size_t)2U * i] = (byte2 & (int32_t)15) << 8U | (byte1 & (int32_t)255); - re[(size_t)2U * i + (size_t)1U] = - byte3 << 4U | (byte2 >> 4U & (int32_t)15); - } - } - memcpy(ret, re, (size_t)256U * sizeof(int32_t)); + memcpy(ret, serialized, (size_t)384U * sizeof(uint8_t)); } static void @@ -869,6 +822,53 @@ compress_coefficients_5(uint8_t coefficient2, .fst = coef1, .snd = coef2, .thd = coef3, .f3 = coef4, .f4 = coef5 }); } +static void +deserialize_to_reduced_ring_element(Eurydice_slice ring_element, + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy(re, ZERO, (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(ring_element, uint8_t, size_t) / + (size_t)3U }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____0 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) { + break; + } else { + size_t i = uu____0.f0; + Eurydice_slice bytes = Eurydice_slice_subslice( + ring_element, + ((core_ops_range_Range__size_t){ .start = i * (size_t)3U, + .end = i * (size_t)3U + (size_t)3U }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t byte1 = + (int32_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t); + int32_t byte2 = + (int32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t); + int32_t byte3 = + (int32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t); + re[(size_t)2U * i] = (byte2 & (int32_t)15) << 8U | (byte1 & (int32_t)255); + int32_t tmp = re[(size_t)2U * i] % (int32_t)3329; + re[(size_t)2U * i] = tmp; + re[(size_t)2U * i + (size_t)1U] = + byte3 << 4U | (byte2 >> 4U & (int32_t)15); + int32_t tmp0 = re[(size_t)2U * i + (size_t)1U] % (int32_t)3329; + re[(size_t)2U * i + (size_t)1U] = tmp0; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + typedef struct __int32_t_int32_t_int32_t_int32_t_s { int32_t fst; @@ -1100,6 +1100,49 @@ ntt_at_layer_3328(size_t* zeta_i, memcpy(ret, ret0, (size_t)256U * sizeof(int32_t)); } +static void +deserialize_to_uncompressed_ring_element(Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy(re, ZERO, (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(serialized, uint8_t, size_t) / + (size_t)3U }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____0 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) { + break; + } else { + size_t i = uu____0.f0; + Eurydice_slice bytes = Eurydice_slice_subslice( + serialized, + ((core_ops_range_Range__size_t){ .start = i * (size_t)3U, + .end = i * (size_t)3U + (size_t)3U }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t byte1 = + (int32_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t); + int32_t byte2 = + (int32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t); + int32_t byte3 = + (int32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t); + re[(size_t)2U * i] = (byte2 & (int32_t)15) << 8U | (byte1 & (int32_t)255); + re[(size_t)2U * i + (size_t)1U] = + byte3 << 4U | (byte2 >> 4U & (int32_t)15); + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + static __int32_t_int32_t decompress_coefficients_4(uint8_t* byte) { @@ -1295,56 +1338,7 @@ compress_then_serialize_message(int32_t re[256U], uint8_t ret[32U]) } } } - uint8_t uu____3[32U]; - memcpy(uu____3, serialized, (size_t)32U * sizeof(uint8_t)); - memcpy(ret, uu____3, (size_t)32U * sizeof(uint8_t)); -} - -static void -deserialize_to_reduced_ring_element(Eurydice_slice ring_element, - int32_t ret[256U]) -{ - int32_t re[256U]; - memcpy(re, ZERO, (size_t)256U * sizeof(int32_t)); - core_ops_range_Range__size_t iter = - core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( - ((core_ops_range_Range__size_t){ - .start = (size_t)0U, - .end = core_slice___Slice_T___len(ring_element, uint8_t, size_t) / - (size_t)3U }), - core_ops_range_Range__size_t, - core_ops_range_Range__size_t); - while (true) { - core_option_Option__size_t uu____0 = - core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( - &iter, size_t, core_option_Option__size_t); - if (uu____0.tag == core_option_None) { - break; - } else { - size_t i = uu____0.f0; - Eurydice_slice bytes = Eurydice_slice_subslice( - ring_element, - ((core_ops_range_Range__size_t){ .start = i * (size_t)3U, - .end = i * (size_t)3U + (size_t)3U }), - uint8_t, - core_ops_range_Range__size_t, - Eurydice_slice); - int32_t byte1 = - (int32_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t); - int32_t byte2 = - (int32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t); - int32_t byte3 = - (int32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t); - re[(size_t)2U * i] = (byte2 & (int32_t)15) << 8U | (byte1 & (int32_t)255); - int32_t tmp = re[(size_t)2U * i] % (int32_t)3329; - re[(size_t)2U * i] = tmp; - re[(size_t)2U * i + (size_t)1U] = - byte3 << 4U | (byte2 >> 4U & (int32_t)15); - int32_t tmp0 = re[(size_t)2U * i + (size_t)1U] % (int32_t)3329; - re[(size_t)2U * i + (size_t)1U] = tmp0; - } - } - memcpy(ret, re, (size_t)256U * sizeof(int32_t)); + memcpy(ret, serialized, (size_t)32U * sizeof(uint8_t)); } static void @@ -1385,9 +1379,7 @@ deserialize_ring_elements_reduced___1184size_t_3size_t( memcpy(deserialized_pk[i], uu____1, (size_t)256U * sizeof(int32_t)); } } - int32_t uu____2[3U][256U]; - memcpy(uu____2, deserialized_pk, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____2, (size_t)3U * sizeof(int32_t[256U])); + memcpy(ret, deserialized_pk, (size_t)3U * sizeof(int32_t[256U])); } static void @@ -1432,9 +1424,7 @@ serialize_secret_key___3size_t_1152size_t(int32_t key[3U][256U], void*); } } - uint8_t uu____2[1152U]; - memcpy(uu____2, out, (size_t)1152U * sizeof(uint8_t)); - memcpy(ret, uu____2, (size_t)1152U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)1152U * sizeof(uint8_t)); } static void @@ -1470,9 +1460,7 @@ serialize_public_key___3size_t_1152size_t_1184size_t(int32_t t_as_ntt[3U][256U], seed_for_a, uint8_t, void*); - uint8_t uu____2[1184U]; - memcpy(uu____2, public_key_serialized, (size_t)1184U * sizeof(uint8_t)); - memcpy(ret, uu____2, (size_t)1184U * sizeof(uint8_t)); + memcpy(ret, public_key_serialized, (size_t)1184U * sizeof(uint8_t)); } static bool @@ -1585,9 +1573,7 @@ squeeze_three_blocks___3size_t( memcpy(out[i], uu____1, (size_t)504U * sizeof(uint8_t)); } } - uint8_t uu____2[3U][504U]; - memcpy(uu____2, out, (size_t)3U * sizeof(uint8_t[504U])); - memcpy(ret, uu____2, (size_t)3U * sizeof(uint8_t[504U])); + memcpy(ret, out, (size_t)3U * sizeof(uint8_t[504U])); } static bool @@ -1699,9 +1685,7 @@ squeeze_block___3size_t( memcpy(out[i], uu____1, (size_t)168U * sizeof(uint8_t)); } } - uint8_t uu____2[3U][168U]; - memcpy(uu____2, out, (size_t)3U * sizeof(uint8_t[168U])); - memcpy(ret, uu____2, (size_t)3U * sizeof(uint8_t[168U])); + memcpy(ret, out, (size_t)3U * sizeof(uint8_t[168U])); } static bool @@ -1815,9 +1799,7 @@ sample_from_xof___3size_t(uint8_t seeds[3U][34U], int32_t ret[3U][256U]) uu____2, sampled_coefficients, out); } free_state(xof_state); - int32_t uu____3[3U][256U]; - memcpy(uu____3, out, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____3, (size_t)3U * sizeof(int32_t[256U])); + memcpy(ret, out, (size_t)3U * sizeof(int32_t[256U])); } static void @@ -1898,9 +1880,7 @@ sample_matrix_A___3size_t(uint8_t seed[34U], } } } - int32_t uu____5[3U][3U][256U]; - memcpy(uu____5, A_transpose, (size_t)3U * sizeof(int32_t[3U][256U])); - memcpy(ret, uu____5, (size_t)3U * sizeof(int32_t[3U][256U])); + memcpy(ret, A_transpose, (size_t)3U * sizeof(int32_t[3U][256U])); } static void @@ -1921,9 +1901,7 @@ into_padded_array___34size_t(Eurydice_slice slice, uint8_t ret[34U]) slice, uint8_t, void*); - uint8_t uu____1[34U]; - memcpy(uu____1, out, (size_t)34U * sizeof(uint8_t)); - memcpy(ret, uu____1, (size_t)34U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)34U * sizeof(uint8_t)); } static void @@ -1944,9 +1922,7 @@ into_padded_array___33size_t(Eurydice_slice slice, uint8_t ret[33U]) slice, uint8_t, void*); - uint8_t uu____1[33U]; - memcpy(uu____1, out, (size_t)33U * sizeof(uint8_t)); - memcpy(ret, uu____1, (size_t)33U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)33U * sizeof(uint8_t)); } static void @@ -2124,19 +2100,27 @@ compute_As_plus_e___3size_t(int32_t (*matrix_A)[3U][256U], } } } - int32_t uu____5[3U][256U]; - memcpy(uu____5, result, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____5, (size_t)3U * sizeof(int32_t[256U])); + memcpy(ret, result, (size_t)3U * sizeof(int32_t[256U])); } -typedef struct __uint8_t_1152size_t__uint8_t_1184size_t__s +typedef struct + __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__s { - uint8_t fst[1152U]; + int32_t fst[3U][256U]; + int32_t snd[3U][256U]; + int32_t thd[3U][3U][256U]; +} __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t_; + +typedef struct + __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__uint8_t_1184size_t__s +{ + __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t_ + fst; uint8_t snd[1184U]; -} __uint8_t_1152size_t__uint8_t_1184size_t_; +} __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__uint8_t_1184size_t_; -static __uint8_t_1152size_t__uint8_t_1184size_t_ -generate_keypair___3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t( +static __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__uint8_t_1184size_t_ +generate_keypair_unpacked___3size_t_1184size_t_1152size_t_2size_t_128size_t( Eurydice_slice key_generation_seed) { uint8_t hashed[64U]; @@ -2149,10 +2133,10 @@ generate_keypair___3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t( K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); Eurydice_slice seed_for_A = uu____0.fst; Eurydice_slice seed_for_secret_and_error = uu____0.snd; - int32_t A_transpose[3U][3U][256U]; + int32_t a_transpose[3U][3U][256U]; uint8_t ret[34U]; into_padded_array___34size_t(seed_for_A, ret); - sample_matrix_A___3size_t(ret, true, A_transpose); + sample_matrix_A___3size_t(ret, true, a_transpose); uint8_t prf_input[33U]; into_padded_array___33size_t(seed_for_secret_and_error, prf_input); uint8_t uu____1[33U]; @@ -2172,34 +2156,148 @@ generate_keypair___3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t( (size_t)3U * sizeof(int32_t[256U])); int32_t t_as_ntt[3U][256U]; compute_As_plus_e___3size_t( - A_transpose, secret_as_ntt, error_as_ntt, t_as_ntt); + a_transpose, secret_as_ntt, error_as_ntt, t_as_ntt); int32_t uu____4[3U][256U]; memcpy(uu____4, t_as_ntt, (size_t)3U * sizeof(int32_t[256U])); uint8_t public_key_serialized[1184U]; serialize_public_key___3size_t_1152size_t_1184size_t( uu____4, seed_for_A, public_key_serialized); - int32_t uu____5[3U][256U]; - memcpy(uu____5, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U])); - uint8_t secret_key_serialized[1152U]; - serialize_secret_key___3size_t_1152size_t(uu____5, secret_key_serialized); - uint8_t uu____6[1152U]; - memcpy(uu____6, secret_key_serialized, (size_t)1152U * sizeof(uint8_t)); - uint8_t uu____7[1184U]; - memcpy(uu____7, public_key_serialized, (size_t)1184U * sizeof(uint8_t)); - __uint8_t_1152size_t__uint8_t_1184size_t_ lit; - memcpy(lit.fst, uu____6, (size_t)1152U * sizeof(uint8_t)); - memcpy(lit.snd, uu____7, (size_t)1184U * sizeof(uint8_t)); + core_ops_range_Range__size_t iter0 = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)3U }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____5 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____5.tag == core_option_None) { + break; + } else { + size_t i = uu____5.f0; + core_ops_range_Range__size_t iter = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)256U }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____6 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____6.tag == core_option_None) { + break; + } else { + size_t j = uu____6.f0; + uint16_t uu____7 = to_unsigned_representative(secret_as_ntt[i][j]); + secret_as_ntt[i][j] = (int32_t)uu____7; + uint16_t uu____8 = to_unsigned_representative(t_as_ntt[i][j]); + t_as_ntt[i][j] = (int32_t)uu____8; + } + } + } + } + int32_t a_matrix[3U][3U][256U]; + memcpy(a_matrix, a_transpose, (size_t)3U * sizeof(int32_t[3U][256U])); + core_ops_range_Range__size_t iter1 = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)3U }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____9 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( + &iter1, size_t, core_option_Option__size_t); + if (uu____9.tag == core_option_None) { + break; + } else { + size_t i = uu____9.f0; + core_ops_range_Range__size_t iter = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)3U }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____10 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____10.tag == core_option_None) { + break; + } else { + size_t j = uu____10.f0; + memcpy( + a_matrix[i][j], a_transpose[j][i], (size_t)256U * sizeof(int32_t)); + } + } + } + } + int32_t uu____11[3U][256U]; + memcpy(uu____11, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U])); + int32_t uu____12[3U][256U]; + memcpy(uu____12, t_as_ntt, (size_t)3U * sizeof(int32_t[256U])); + int32_t uu____13[3U][3U][256U]; + memcpy(uu____13, a_matrix, (size_t)3U * sizeof(int32_t[3U][256U])); + __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t_ + uu____14; + memcpy(uu____14.fst, uu____11, (size_t)3U * sizeof(int32_t[256U])); + memcpy(uu____14.snd, uu____12, (size_t)3U * sizeof(int32_t[256U])); + memcpy(uu____14.thd, uu____13, (size_t)3U * sizeof(int32_t[3U][256U])); + uint8_t uu____15[1184U]; + memcpy(uu____15, public_key_serialized, (size_t)1184U * sizeof(uint8_t)); + __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__uint8_t_1184size_t_ + lit; + lit.fst = uu____14; + memcpy(lit.snd, uu____15, (size_t)1184U * sizeof(uint8_t)); return lit; } -static void -serialize_kem_secret_key___2400size_t(Eurydice_slice private_key, - Eurydice_slice public_key, - Eurydice_slice implicit_rejection_value, - uint8_t ret[2400U]) +typedef struct __uint8_t_1152size_t__uint8_t_1184size_t__s { - uint8_t out[2400U] = { 0U }; - size_t pointer = (size_t)0U; + uint8_t fst[1152U]; + uint8_t snd[1184U]; +} __uint8_t_1152size_t__uint8_t_1184size_t_; + +static __uint8_t_1152size_t__uint8_t_1184size_t_ +generate_keypair___3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t( + Eurydice_slice key_generation_seed) +{ + __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__uint8_t_1184size_t_ + uu____0 = + generate_keypair_unpacked___3size_t_1184size_t_1152size_t_2size_t_128size_t( + key_generation_seed); + int32_t secret_as_ntt[3U][256U]; + memcpy(secret_as_ntt, uu____0.fst.fst, (size_t)3U * sizeof(int32_t[256U])); + int32_t _t_as_ntt[3U][256U]; + memcpy(_t_as_ntt, uu____0.fst.snd, (size_t)3U * sizeof(int32_t[256U])); + int32_t _a_transpose[3U][3U][256U]; + memcpy(_a_transpose, uu____0.fst.thd, (size_t)3U * sizeof(int32_t[3U][256U])); + uint8_t public_key_serialized[1184U]; + memcpy(public_key_serialized, uu____0.snd, (size_t)1184U * sizeof(uint8_t)); + int32_t uu____1[3U][256U]; + memcpy(uu____1, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U])); + uint8_t secret_key_serialized[1152U]; + serialize_secret_key___3size_t_1152size_t(uu____1, secret_key_serialized); + uint8_t uu____2[1152U]; + memcpy(uu____2, secret_key_serialized, (size_t)1152U * sizeof(uint8_t)); + uint8_t uu____3[1184U]; + memcpy(uu____3, public_key_serialized, (size_t)1184U * sizeof(uint8_t)); + __uint8_t_1152size_t__uint8_t_1184size_t_ lit; + memcpy(lit.fst, uu____2, (size_t)1152U * sizeof(uint8_t)); + memcpy(lit.snd, uu____3, (size_t)1184U * sizeof(uint8_t)); + return lit; +} + +static void +serialize_kem_secret_key___2400size_t(Eurydice_slice private_key, + Eurydice_slice public_key, + Eurydice_slice implicit_rejection_value, + uint8_t ret[2400U]) +{ + uint8_t out[2400U] = { 0U }; + size_t pointer = (size_t)0U; uint8_t* uu____0 = out; size_t uu____1 = pointer; size_t uu____2 = pointer; @@ -2269,9 +2367,7 @@ serialize_kem_secret_key___2400size_t(Eurydice_slice private_key, implicit_rejection_value, uint8_t, void*); - uint8_t uu____10[2400U]; - memcpy(uu____10, out, (size_t)2400U * sizeof(uint8_t)); - memcpy(ret, uu____10, (size_t)2400U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)2400U * sizeof(uint8_t)); } typedef uint8_t MlKemPrivateKey___2400size_t[2400U]; @@ -2347,6 +2443,120 @@ libcrux_kyber_kyber768_generate_key_pair(uint8_t randomness[64U]) uu____0); } +#define Ok 0 +#define Err 1 + +typedef uint8_t Result__uint8_t_32size_t__core_array_TryFromSliceError_tags; + +typedef struct Result__uint8_t_32size_t__core_array_TryFromSliceError_s +{ + Result__uint8_t_32size_t__core_array_TryFromSliceError_tags tag; + union + { + uint8_t case_Ok[32U]; + core_array_TryFromSliceError case_Err; + } val; +} Result__uint8_t_32size_t__core_array_TryFromSliceError; + +static void +unwrap__uint8_t_32size_t__core_array_TryFromSliceError( + Result__uint8_t_32size_t__core_array_TryFromSliceError self, + uint8_t ret[32U]) +{ + if (self.tag == Ok) { + uint8_t f0[32U]; + memcpy(f0, self.val.case_Ok, (size_t)32U * sizeof(uint8_t)); + memcpy(ret, f0, (size_t)32U * sizeof(uint8_t)); + } else { + KRML_HOST_EPRINTF( + "KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "unwrap not Ok"); + KRML_HOST_EXIT(255U); + } +} + +static void +from___1184size_t(uint8_t value[1184U], uint8_t ret[1184U]) +{ + uint8_t uu____0[1184U]; + memcpy(uu____0, value, (size_t)1184U * sizeof(uint8_t)); + memcpy(ret, uu____0, (size_t)1184U * sizeof(uint8_t)); +} + +static K___libcrux_kyber_MlKemState__3size_t___libcrux_kyber_types_MlKemPublicKey__1184size_t__ +generate_keypair_unpacked___3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t( + uint8_t randomness[64U]) +{ + Eurydice_slice ind_cpa_keypair_randomness = Eurydice_array_to_subslice( + (size_t)64U, + randomness, + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = CPA_PKE_KEY_GENERATION_SEED_SIZE }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + Eurydice_slice implicit_rejection_value = + Eurydice_array_to_subslice_from((size_t)64U, + randomness, + CPA_PKE_KEY_GENERATION_SEED_SIZE, + uint8_t, + size_t, + Eurydice_slice); + __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__uint8_t_1184size_t_ + uu____0 = + generate_keypair_unpacked___3size_t_1184size_t_1152size_t_2size_t_128size_t( + ind_cpa_keypair_randomness); + int32_t secret_as_ntt[3U][256U]; + memcpy(secret_as_ntt, uu____0.fst.fst, (size_t)3U * sizeof(int32_t[256U])); + int32_t t_as_ntt[3U][256U]; + memcpy(t_as_ntt, uu____0.fst.snd, (size_t)3U * sizeof(int32_t[256U])); + int32_t a_transpose[3U][3U][256U]; + memcpy(a_transpose, uu____0.fst.thd, (size_t)3U * sizeof(int32_t[3U][256U])); + uint8_t ind_cpa_public_key[1184U]; + memcpy(ind_cpa_public_key, uu____0.snd, (size_t)1184U * sizeof(uint8_t)); + uint8_t ind_cpa_public_key_hash[32U]; + H(Eurydice_array_to_slice( + (size_t)1184U, ind_cpa_public_key, uint8_t, Eurydice_slice), + ind_cpa_public_key_hash); + uint8_t rej[32U]; + Result__uint8_t_32size_t__core_array_TryFromSliceError dst; + Eurydice_slice_to_array2( + &dst, implicit_rejection_value, Eurydice_slice, uint8_t[32U], void*); + unwrap__uint8_t_32size_t__core_array_TryFromSliceError(dst, rej); + uint8_t uu____1[1184U]; + memcpy(uu____1, ind_cpa_public_key, (size_t)1184U * sizeof(uint8_t)); + uint8_t pubkey[1184U]; + from___1184size_t(uu____1, pubkey); + int32_t uu____2[3U][256U]; + memcpy(uu____2, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U])); + int32_t uu____3[3U][256U]; + memcpy(uu____3, t_as_ntt, (size_t)3U * sizeof(int32_t[256U])); + int32_t uu____4[3U][3U][256U]; + memcpy(uu____4, a_transpose, (size_t)3U * sizeof(int32_t[3U][256U])); + uint8_t uu____5[32U]; + memcpy(uu____5, rej, (size_t)32U * sizeof(uint8_t)); + uint8_t uu____6[32U]; + memcpy(uu____6, ind_cpa_public_key_hash, (size_t)32U * sizeof(uint8_t)); + K___libcrux_kyber_MlKemState__3size_t___libcrux_kyber_types_MlKemPublicKey__1184size_t__ + lit; + memcpy(lit.fst.secret_as_ntt, uu____2, (size_t)3U * sizeof(int32_t[256U])); + memcpy(lit.fst.t_as_ntt, uu____3, (size_t)3U * sizeof(int32_t[256U])); + memcpy(lit.fst.a_transpose, uu____4, (size_t)3U * sizeof(int32_t[3U][256U])); + memcpy(lit.fst.rej, uu____5, (size_t)32U * sizeof(uint8_t)); + memcpy( + lit.fst.ind_cpa_public_key_hash, uu____6, (size_t)32U * sizeof(uint8_t)); + memcpy(lit.snd, pubkey, (size_t)1184U * sizeof(uint8_t)); + return lit; +} + +K___libcrux_kyber_MlKemState__3size_t___libcrux_kyber_types_MlKemPublicKey__1184size_t__ +libcrux_kyber_kyber768_generate_key_pair_unpacked(uint8_t randomness[64U]) +{ + uint8_t uu____0[64U]; + memcpy(uu____0, randomness, (size_t)64U * sizeof(uint8_t)); + return generate_keypair_unpacked___3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t( + uu____0); +} + static void into_padded_array___64size_t(Eurydice_slice slice, uint8_t ret[64U]) { @@ -2365,9 +2575,7 @@ into_padded_array___64size_t(Eurydice_slice slice, uint8_t ret[64U]) slice, uint8_t, void*); - uint8_t uu____1[64U]; - memcpy(uu____1, out, (size_t)64U * sizeof(uint8_t)); - memcpy(ret, uu____1, (size_t)64U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)64U * sizeof(uint8_t)); } static uint8_t* @@ -2377,12 +2585,13 @@ as_slice___1184size_t(uint8_t (*self)[1184U]) } static void -deserialize_public_key___3size_t(Eurydice_slice public_key, - int32_t ret[3U][256U]) +deserialize_ring_elements_reduced___1152size_t_3size_t( + Eurydice_slice public_key, + int32_t ret[3U][256U]) { - int32_t t_as_ntt[3U][256U]; + int32_t deserialized_pk[3U][256U]; for (size_t i = (size_t)0U; i < (size_t)3U; i++) { - memcpy(t_as_ntt[i], ZERO, (size_t)256U * sizeof(int32_t)); + memcpy(deserialized_pk[i], ZERO, (size_t)256U * sizeof(int32_t)); } core_ops_range_Range__size_t iter = core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( @@ -2400,7 +2609,7 @@ deserialize_public_key___3size_t(Eurydice_slice public_key, break; } else { size_t i = uu____0.f0; - Eurydice_slice t_as_ntt_bytes = Eurydice_slice_subslice( + Eurydice_slice ring_element = Eurydice_slice_subslice( public_key, ((core_ops_range_Range__size_t){ .start = i * BYTES_PER_RING_ELEMENT, .end = i * BYTES_PER_RING_ELEMENT + @@ -2409,13 +2618,11 @@ deserialize_public_key___3size_t(Eurydice_slice public_key, core_ops_range_Range__size_t, Eurydice_slice); int32_t uu____1[256U]; - deserialize_to_uncompressed_ring_element(t_as_ntt_bytes, uu____1); - memcpy(t_as_ntt[i], uu____1, (size_t)256U * sizeof(int32_t)); + deserialize_to_reduced_ring_element(ring_element, uu____1); + memcpy(deserialized_pk[i], uu____1, (size_t)256U * sizeof(int32_t)); } } - int32_t uu____2[3U][256U]; - memcpy(uu____2, t_as_ntt, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____2, (size_t)3U * sizeof(int32_t[256U])); + memcpy(ret, deserialized_pk, (size_t)3U * sizeof(int32_t[256U])); } static void @@ -2455,9 +2662,7 @@ sample_ring_element_cbd___3size_t_128size_t_2size_t(uint8_t* prf_input, memcpy(error_1[i], uu____1, (size_t)256U * sizeof(int32_t)); } } - int32_t uu____2[3U][256U]; - memcpy(uu____2, error_1, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____2, (size_t)3U * sizeof(int32_t[256U])); + memcpy(ret, error_1, (size_t)3U * sizeof(int32_t[256U])); } static void @@ -2572,9 +2777,7 @@ compute_vector_u___3size_t(int32_t (*a_as_ntt)[3U][256U], } } } - int32_t uu____6[3U][256U]; - memcpy(uu____6, result, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____6, (size_t)3U * sizeof(int32_t[256U])); + memcpy(ret, result, (size_t)3U * sizeof(int32_t[256U])); } static void @@ -2692,9 +2895,7 @@ compress_then_serialize_10___320size_t(int32_t re[256U], uint8_t ret[320U]) serialized[(size_t)5U * i + (size_t)4U] = coef5; } } - uint8_t uu____2[320U]; - memcpy(uu____2, serialized, (size_t)320U * sizeof(uint8_t)); - memcpy(ret, uu____2, (size_t)320U * sizeof(uint8_t)); + memcpy(ret, serialized, (size_t)320U * sizeof(uint8_t)); } static void @@ -2793,9 +2994,7 @@ compress_then_serialize_11___320size_t(int32_t re[256U], uint8_t ret[320U]) serialized[(size_t)11U * i + (size_t)10U] = coef11; } } - uint8_t uu____2[320U]; - memcpy(uu____2, serialized, (size_t)320U * sizeof(uint8_t)); - memcpy(ret, uu____2, (size_t)320U * sizeof(uint8_t)); + memcpy(ret, serialized, (size_t)320U * sizeof(uint8_t)); } static void @@ -2850,9 +3049,7 @@ compress_then_serialize_u___3size_t_960size_t_10size_t_320size_t( void*); } } - uint8_t uu____2[960U]; - memcpy(uu____2, out, (size_t)960U * sizeof(uint8_t)); - memcpy(ret, uu____2, (size_t)960U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)960U * sizeof(uint8_t)); } static void @@ -2897,9 +3094,7 @@ compress_then_serialize_4___128size_t(int32_t re[256U], uint8_t ret[128U]) serialized[i] = (uint32_t)coefficient2 << 4U | (uint32_t)coefficient1; } } - uint8_t uu____1[128U]; - memcpy(uu____1, serialized, (size_t)128U * sizeof(uint8_t)); - memcpy(ret, uu____1, (size_t)128U * sizeof(uint8_t)); + memcpy(ret, serialized, (size_t)128U * sizeof(uint8_t)); } static void @@ -2986,9 +3181,7 @@ compress_then_serialize_5___128size_t(int32_t re[256U], uint8_t ret[128U]) serialized[(size_t)5U * i + (size_t)4U] = coef5; } } - uint8_t uu____2[128U]; - memcpy(uu____2, serialized, (size_t)128U * sizeof(uint8_t)); - memcpy(ret, uu____2, (size_t)128U * sizeof(uint8_t)); + memcpy(ret, serialized, (size_t)128U * sizeof(uint8_t)); } static void @@ -3018,29 +3211,17 @@ into_padded_array___1088size_t(Eurydice_slice slice, uint8_t ret[1088U]) slice, uint8_t, void*); - uint8_t uu____1[1088U]; - memcpy(uu____1, out, (size_t)1088U * sizeof(uint8_t)); - memcpy(ret, uu____1, (size_t)1088U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)1088U * sizeof(uint8_t)); } static void -encrypt___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t( - Eurydice_slice public_key, +encrypt_unpacked___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t( + int32_t (*t_as_ntt)[256U], + int32_t (*a_transpose)[3U][256U], uint8_t message[32U], Eurydice_slice randomness, uint8_t ret[1088U]) { - int32_t t_as_ntt[3U][256U]; - deserialize_public_key___3size_t( - Eurydice_slice_subslice_to( - public_key, (size_t)1152U, uint8_t, size_t, Eurydice_slice), - t_as_ntt); - Eurydice_slice seed = Eurydice_slice_subslice_from( - public_key, (size_t)1152U, uint8_t, size_t, Eurydice_slice); - int32_t A_transpose[3U][3U][256U]; - uint8_t ret0[34U]; - into_padded_array___34size_t(seed, ret0); - sample_matrix_A___3size_t(ret0, false, A_transpose); uint8_t prf_input[33U]; into_padded_array___33size_t(randomness, prf_input); uint8_t uu____0[33U]; @@ -3063,7 +3244,7 @@ encrypt___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320 Eurydice_array_to_slice((size_t)128U, prf_output, uint8_t, Eurydice_slice), error_2); int32_t u[3U][256U]; - compute_vector_u___3size_t(A_transpose, r_as_ntt, error_1, u); + compute_vector_u___3size_t(a_transpose, r_as_ntt, error_1, u); uint8_t uu____2[32U]; memcpy(uu____2, message, (size_t)32U * sizeof(uint8_t)); int32_t message_as_ring_element[256U]; @@ -3089,9 +3270,35 @@ encrypt___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320 (size_t)128U, c2, uint8_t, Eurydice_slice), uint8_t, void*); - uint8_t uu____5[1088U]; - memcpy(uu____5, ciphertext, (size_t)1088U * sizeof(uint8_t)); - memcpy(ret, uu____5, (size_t)1088U * sizeof(uint8_t)); + memcpy(ret, ciphertext, (size_t)1088U * sizeof(uint8_t)); +} + +static void +encrypt___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t( + Eurydice_slice public_key, + uint8_t message[32U], + Eurydice_slice randomness, + uint8_t ret[1088U]) +{ + int32_t t_as_ntt[3U][256U]; + deserialize_ring_elements_reduced___1152size_t_3size_t( + Eurydice_slice_subslice_to( + public_key, (size_t)1152U, uint8_t, size_t, Eurydice_slice), + t_as_ntt); + Eurydice_slice seed = Eurydice_slice_subslice_from( + public_key, (size_t)1152U, uint8_t, size_t, Eurydice_slice); + int32_t a_transpose[3U][3U][256U]; + uint8_t ret0[34U]; + into_padded_array___34size_t(seed, ret0); + sample_matrix_A___3size_t(ret0, false, a_transpose); + int32_t(*uu____0)[256U] = t_as_ntt; + int32_t(*uu____1)[3U][256U] = a_transpose; + uint8_t uu____2[32U]; + memcpy(uu____2, message, (size_t)32U * sizeof(uint8_t)); + uint8_t ret1[1088U]; + encrypt_unpacked___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t( + uu____0, uu____1, uu____2, randomness, ret1); + memcpy(ret, ret1, (size_t)1088U * sizeof(uint8_t)); } typedef uint8_t MlKemCiphertext___1088size_t[1088U]; @@ -3176,6 +3383,46 @@ split_at___2400size_t(uint8_t (*self)[2400U], size_t mid) K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); } +static void +deserialize_secret_key___3size_t(Eurydice_slice secret_key, + int32_t ret[3U][256U]) +{ + int32_t secret_as_ntt[3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) { + memcpy(secret_as_ntt[i], ZERO, (size_t)256U * sizeof(int32_t)); + } + core_ops_range_Range__size_t iter = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(secret_key, uint8_t, size_t) / + BYTES_PER_RING_ELEMENT }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____0 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) { + break; + } else { + size_t i = uu____0.f0; + Eurydice_slice secret_bytes = Eurydice_slice_subslice( + secret_key, + ((core_ops_range_Range__size_t){ .start = i * BYTES_PER_RING_ELEMENT, + .end = i * BYTES_PER_RING_ELEMENT + + BYTES_PER_RING_ELEMENT }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t uu____1[256U]; + deserialize_to_uncompressed_ring_element(secret_bytes, uu____1); + memcpy(secret_as_ntt[i], uu____1, (size_t)256U * sizeof(int32_t)); + } + } + memcpy(ret, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U])); +} + static void deserialize_then_decompress_ring_element_u___10size_t(Eurydice_slice serialized, int32_t ret[256U]) @@ -3264,9 +3511,7 @@ deserialize_then_decompress_u___3size_t_1088size_t_10size_t( memcpy(u_as_ntt[i], uu____1, (size_t)256U * sizeof(int32_t)); } } - int32_t uu____2[3U][256U]; - memcpy(uu____2, u_as_ntt, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____2, (size_t)3U * sizeof(int32_t[256U])); + memcpy(ret, u_as_ntt, (size_t)3U * sizeof(int32_t[256U])); } static void @@ -3278,48 +3523,6 @@ deserialize_then_decompress_ring_element_v___4size_t(Eurydice_slice serialized, memcpy(ret, uu____0, (size_t)256U * sizeof(int32_t)); } -static void -deserialize_secret_key___3size_t(Eurydice_slice secret_key, - int32_t ret[3U][256U]) -{ - int32_t secret_as_ntt[3U][256U]; - for (size_t i = (size_t)0U; i < (size_t)3U; i++) { - memcpy(secret_as_ntt[i], ZERO, (size_t)256U * sizeof(int32_t)); - } - core_ops_range_Range__size_t iter = - core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter( - ((core_ops_range_Range__size_t){ - .start = (size_t)0U, - .end = core_slice___Slice_T___len(secret_key, uint8_t, size_t) / - BYTES_PER_RING_ELEMENT }), - core_ops_range_Range__size_t, - core_ops_range_Range__size_t); - while (true) { - core_option_Option__size_t uu____0 = - core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next( - &iter, size_t, core_option_Option__size_t); - if (uu____0.tag == core_option_None) { - break; - } else { - size_t i = uu____0.f0; - Eurydice_slice secret_bytes = Eurydice_slice_subslice( - secret_key, - ((core_ops_range_Range__size_t){ .start = i * BYTES_PER_RING_ELEMENT, - .end = i * BYTES_PER_RING_ELEMENT + - BYTES_PER_RING_ELEMENT }), - uint8_t, - core_ops_range_Range__size_t, - Eurydice_slice); - int32_t uu____1[256U]; - deserialize_to_uncompressed_ring_element(secret_bytes, uu____1); - memcpy(secret_as_ntt[i], uu____1, (size_t)256U * sizeof(int32_t)); - } - } - int32_t uu____2[3U][256U]; - memcpy(uu____2, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U])); - memcpy(ret, uu____2, (size_t)3U * sizeof(int32_t[256U])); -} - static void compute_message___3size_t(int32_t (*v)[256U], int32_t (*secret_as_ntt)[256U], @@ -3372,8 +3575,8 @@ compute_message___3size_t(int32_t (*v)[256U], } static void -decrypt___3size_t_1088size_t_960size_t_10size_t_4size_t( - Eurydice_slice secret_key, +decrypt_unpacked___3size_t_1088size_t_960size_t_10size_t_4size_t( + int32_t (*secret_as_ntt)[256U], uint8_t* ciphertext, uint8_t ret[32U]) { @@ -3385,8 +3588,6 @@ decrypt___3size_t_1088size_t_960size_t_10size_t_4size_t( Eurydice_array_to_subslice_from( (size_t)1088U, ciphertext, (size_t)960U, uint8_t, size_t, Eurydice_slice), v); - int32_t secret_as_ntt[3U][256U]; - deserialize_secret_key___3size_t(secret_key, secret_as_ntt); int32_t message[256U]; compute_message___3size_t(&v, secret_as_ntt, u_as_ntt, message); uint8_t ret0[32U]; @@ -3394,6 +3595,20 @@ decrypt___3size_t_1088size_t_960size_t_10size_t_4size_t( memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } +static void +decrypt___3size_t_1088size_t_960size_t_10size_t_4size_t( + Eurydice_slice secret_key, + uint8_t* ciphertext, + uint8_t ret[32U]) +{ + int32_t secret_as_ntt[3U][256U]; + deserialize_secret_key___3size_t(secret_key, secret_as_ntt); + uint8_t ret0[32U]; + decrypt_unpacked___3size_t_1088size_t_960size_t_10size_t_4size_t( + secret_as_ntt, ciphertext, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} + static void into_padded_array___1120size_t(Eurydice_slice slice, uint8_t ret[1120U]) { @@ -3412,9 +3627,7 @@ into_padded_array___1120size_t(Eurydice_slice slice, uint8_t ret[1120U]) slice, uint8_t, void*); - uint8_t uu____1[1120U]; - memcpy(uu____1, out, (size_t)1120U * sizeof(uint8_t)); - memcpy(ret, uu____1, (size_t)1120U * sizeof(uint8_t)); + memcpy(ret, out, (size_t)1120U * sizeof(uint8_t)); } static Eurydice_slice @@ -3559,3 +3772,93 @@ libcrux_kyber_kyber768_decapsulate(uint8_t (*secret_key)[2400U], secret_key, ciphertext, ret0); memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); } + +static void +decapsulate_unpacked___3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t( + libcrux_kyber_MlKemState___3size_t* state, + uint8_t (*ciphertext)[1088U], + uint8_t ret[32U]) +{ + int32_t(*secret_as_ntt)[256U] = state->secret_as_ntt; + int32_t(*t_as_ntt)[256U] = state->t_as_ntt; + int32_t(*a_transpose)[3U][256U] = state->a_transpose; + Eurydice_slice implicit_rejection_value = + Eurydice_array_to_slice((size_t)32U, state->rej, uint8_t, Eurydice_slice); + Eurydice_slice ind_cpa_public_key_hash = Eurydice_array_to_slice( + (size_t)32U, state->ind_cpa_public_key_hash, uint8_t, Eurydice_slice); + uint8_t decrypted[32U]; + decrypt_unpacked___3size_t_1088size_t_960size_t_10size_t_4size_t( + secret_as_ntt, ciphertext[0U], decrypted); + uint8_t to_hash0[64U]; + into_padded_array___64size_t( + Eurydice_array_to_slice((size_t)32U, decrypted, uint8_t, Eurydice_slice), + to_hash0); + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice_from((size_t)64U, + to_hash0, + SHARED_SECRET_SIZE, + uint8_t, + size_t, + Eurydice_slice), + ind_cpa_public_key_hash, + uint8_t, + void*); + uint8_t hashed[64U]; + G(Eurydice_array_to_slice((size_t)64U, to_hash0, uint8_t, Eurydice_slice), + hashed); + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t uu____0 = + core_slice___Slice_T___split_at( + Eurydice_array_to_slice((size_t)64U, hashed, uint8_t, Eurydice_slice), + SHARED_SECRET_SIZE, + uint8_t, + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); + Eurydice_slice shared_secret = uu____0.fst; + Eurydice_slice pseudorandomness = uu____0.snd; + uint8_t to_hash[1120U]; + into_padded_array___1120size_t(implicit_rejection_value, to_hash); + Eurydice_slice uu____1 = Eurydice_array_to_subslice_from((size_t)1120U, + to_hash, + SHARED_SECRET_SIZE, + uint8_t, + size_t, + Eurydice_slice); + core_slice___Slice_T___copy_from_slice( + uu____1, as_ref___1088size_t(ciphertext), uint8_t, void*); + uint8_t implicit_rejection_shared_secret[32U]; + PRF___32size_t( + Eurydice_array_to_slice((size_t)1120U, to_hash, uint8_t, Eurydice_slice), + implicit_rejection_shared_secret); + int32_t(*uu____2)[256U] = t_as_ntt; + int32_t(*uu____3)[3U][256U] = a_transpose; + uint8_t uu____4[32U]; + memcpy(uu____4, decrypted, (size_t)32U * sizeof(uint8_t)); + uint8_t expected_ciphertext[1088U]; + encrypt_unpacked___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t( + uu____2, uu____3, uu____4, pseudorandomness, expected_ciphertext); + Eurydice_slice uu____5 = as_ref___1088size_t(ciphertext); + uint8_t selector = compare_ciphertexts_in_constant_time___1088size_t( + uu____5, + Eurydice_array_to_slice( + (size_t)1088U, expected_ciphertext, uint8_t, Eurydice_slice)); + Eurydice_slice uu____6 = shared_secret; + uint8_t ret0[32U]; + select_shared_secret_in_constant_time( + uu____6, + Eurydice_array_to_slice( + (size_t)32U, implicit_rejection_shared_secret, uint8_t, Eurydice_slice), + selector, + ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} + +void +libcrux_kyber_kyber768_decapsulate_unpacked( + libcrux_kyber_MlKemState___3size_t* state, + uint8_t (*ciphertext)[1088U], + uint8_t ret[32U]) +{ + uint8_t ret0[32U]; + decapsulate_unpacked___3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t( + state, ciphertext, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +}