diff --git a/.gitignore b/.gitignore index bbfe8fd8..e8d79b9e 100644 --- a/.gitignore +++ b/.gitignore @@ -27,3 +27,5 @@ rust/.c .idea cmake-build-debug +# ctags +tags diff --git a/CMakeLists.txt b/CMakeLists.txt index e7374bd9..25999e58 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -168,6 +168,11 @@ if(ENABLE_UBSAN) add_link_options(-fsanitize=undefined) endif() +if(ENABLE_MSAN) + add_compile_options(-fsanitize=memory -fsanitize-memory-track-origins) + add_link_options(-fsanitize=memory) +endif() + # Sources are written by mach.py into the following lists # - SOURCES_std: All regular files # - SOURCES_vec128: Files that require vec128 hardware @@ -335,7 +340,7 @@ configure_file(config/Config.h.in config.h) # # Dynamic library add_library(hacl SHARED ${SOURCES_std} ${VALE_OBJECTS}) if(NOT MSVC) - target_compile_options(hacl PRIVATE -Wsign-conversion -Wconversion -Wall -Wextra -pedantic) + target_compile_options(hacl PRIVATE -Wall -Wextra -pedantic) endif() if(TOOLCHAIN_CAN_COMPILE_VEC128 AND HACL_VEC128_O) @@ -362,7 +367,7 @@ endif() if(BUILD_LIBCRUX) add_library(libcrux_static STATIC ${LIBCRUX_SOURCES}) if(NOT MSVC) - target_compile_options(libcrux_static PRIVATE -Wsign-conversion -Wconversion -Wall -Wextra -pedantic) + target_compile_options(libcrux_static PRIVATE -Wall -Wextra -pedantic -Wshadow -Wunused-function) endif() endif() @@ -511,10 +516,10 @@ if(ENABLE_TESTS) add_dependencies(${TEST_NAME} hacl hacl_cpu_features) target_link_libraries(${TEST_NAME} PRIVATE gtest_main - hacl_static hacl_cpu_features nlohmann_json::nlohmann_json libcrux_static + hacl_static ) if(EXISTS ${PROJECT_SOURCE_DIR}/tests/${TEST_NAME}) @@ -596,4 +601,32 @@ if(ENABLE_BENCHMARKS) benchmark::benchmark ) endforeach() + + if(BUILD_LIBCRUX) + foreach(BENCH_FILE IN LISTS LIBCRUX_BENCHMARK_SOURCES) + get_filename_component(BENCH_NAME ${BENCH_FILE} NAME_WE) + set(BENCH_NAME ${BENCH_NAME}_benchmark) + add_executable(${BENCH_NAME} + ${BENCH_FILE} + ) + + # Use modern C++ + if(NOT MSVC) + target_compile_options(${BENCH_NAME} PRIVATE -std=c++17) + else() + # MSVC needs a modern C++ for designated initializers. + target_compile_options(${BENCH_NAME} PRIVATE /std:c++20) + endif(NOT MSVC) + + target_compile_definitions(${BENCH_NAME} PUBLIC NO_OPENSSL) + + add_dependencies(${BENCH_NAME} hacl hacl_cpu_features) + target_link_libraries(${BENCH_NAME} PRIVATE + hacl_cpu_features + benchmark::benchmark + libcrux_static + hacl_static + ) + endforeach() + endif() endif(ENABLE_BENCHMARKS) diff --git a/benchmarks/kyber.cc b/benchmarks/kyber.cc new file mode 100644 index 00000000..50e16108 --- /dev/null +++ b/benchmarks/kyber.cc @@ -0,0 +1,73 @@ +/* + * Copyright 2022 Cryspen Sarl + * + * Licensed under the Apache License, Version 2.0 or MIT. + * - http://www.apache.org/licenses/LICENSE-2.0 + * - http://opensource.org/licenses/MIT + */ + +#include "Libcrux_Kem_Kyber_Kyber768.h" +#include "util.h" + +static void +kyber768_key_generation(benchmark::State& state) +{ + uint8_t randomness[64]; + generate_random(randomness, 64); + + uint8_t public_key[KYBER768_PUBLICKEYBYTES]; + uint8_t secret_key[KYBER768_SECRETKEYBYTES]; + + for (auto _ : state) { + Libcrux_Kyber768_GenerateKeyPair(public_key, secret_key, randomness); + } +} + +static void +kyber768_encapsulation(benchmark::State& state) +{ + uint8_t randomness[32]; + generate_random(randomness, 32); + + uint8_t public_key[KYBER768_PUBLICKEYBYTES]; + uint8_t secret_key[KYBER768_SECRETKEYBYTES]; + + uint8_t ciphertext[KYBER768_CIPHERTEXTBYTES]; + uint8_t sharedSecret[KYBER768_SHAREDSECRETBYTES]; + + Libcrux_Kyber768_GenerateKeyPair(public_key, secret_key, randomness); + + for (auto _ : state) { + Libcrux_Kyber768_Encapsulate( + ciphertext, sharedSecret, &public_key, randomness); + } +} + +static void +kyber768_decapsulation(benchmark::State& state) +{ + uint8_t randomness[64]; + + uint8_t public_key[KYBER768_PUBLICKEYBYTES]; + uint8_t secret_key[KYBER768_SECRETKEYBYTES]; + + uint8_t ciphertext[KYBER768_CIPHERTEXTBYTES]; + uint8_t sharedSecret[KYBER768_SHAREDSECRETBYTES]; + + generate_random(randomness, 64); + Libcrux_Kyber768_GenerateKeyPair(public_key, secret_key, randomness); + + generate_random(randomness, 32); + Libcrux_Kyber768_Encapsulate( + ciphertext, sharedSecret, &public_key, randomness); + + for (auto _ : state) { + Libcrux_Kyber768_Decapsulate(sharedSecret, &ciphertext, &secret_key); + } +} + +BENCHMARK(kyber768_key_generation)->Setup(DoSetup); +BENCHMARK(kyber768_encapsulation)->Setup(DoSetup); +BENCHMARK(kyber768_decapsulation)->Setup(DoSetup); + +BENCHMARK_MAIN(); diff --git a/config/config.json b/config/config.json index c61544ff..63623672 100644 --- a/config/config.json +++ b/config/config.json @@ -7,7 +7,8 @@ "vale/include" ], "libcrux_include_paths": [ - "libcrux/include" + "libcrux/include", + "libcrux/eurydice" ], "hacl_sources": { "nacl": [ @@ -344,6 +345,15 @@ "kyber": [ { "file": "Libcrux_Kem_Kyber_Kyber768.c" + }, + { + "file": "libcrux_kyber.c" + }, + { + "file": "libcrux_hacl_glue.c" + }, + { + "file": "core.c" } ] }, @@ -570,5 +580,10 @@ "rsapss": [ "rsapss.cc" ] + }, + "libcrux_benchmarks": { + "kyber": [ + "kyber.cc" + ] } } diff --git a/libcrux/include/Eurydice.h b/libcrux/include/Eurydice.h new file mode 100644 index 00000000..aff0bf1a --- /dev/null +++ b/libcrux/include/Eurydice.h @@ -0,0 +1,26 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf + KaRaMeL version: 0eda808b + */ + +#ifndef __Eurydice_H +#define __Eurydice_H + +#include "eurydice_glue.h" + +typedef struct core_ops_range_Range__size_t_s +{ + size_t start; + size_t end; +} +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 __Eurydice_H_DEFINED +#endif diff --git a/libcrux/include/Libcrux_Kem_Kyber_Kyber768.h b/libcrux/include/Libcrux_Kem_Kyber_Kyber768.h index 368f22a2..f82fce7c 100644 --- a/libcrux/include/Libcrux_Kem_Kyber_Kyber768.h +++ b/libcrux/include/Libcrux_Kem_Kyber_Kyber768.h @@ -12,17 +12,18 @@ extern "C" #define KYBER768_PUBLICKEYBYTES 1184 #define KYBER768_CIPHERTEXTBYTES 1088 #define KYBER768_SHAREDSECRETBYTES 32 + void Libcrux_Kyber768_GenerateKeyPair(uint8_t* pk, + uint8_t* sk, + uint8_t randomness[64]); - int Libcrux_Kyber768_GenerateKeyPair(uint8_t* pk, - uint8_t* sk, - const uint8_t* randomness); - int Libcrux_Kyber768_Encapsulate(uint8_t* ct, - uint8_t* ss, - const uint8_t* pk, - const uint8_t* randomness); - int Libcrux_Kyber768_Decapsulate(uint8_t* ss, - const uint8_t* ct, - const uint8_t* sk); + void Libcrux_Kyber768_Encapsulate(uint8_t* ct, + uint8_t* ss, + uint8_t (*pk)[1184], + uint8_t randomness[32]); + + void Libcrux_Kyber768_Decapsulate(uint8_t ss[32U], + uint8_t (*ct)[1088U], + uint8_t (*sk)[2400U]); #if defined(__cplusplus) } diff --git a/libcrux/include/eurydice_glue.h b/libcrux/include/eurydice_glue.h new file mode 100644 index 00000000..3e3e14b0 --- /dev/null +++ b/libcrux/include/eurydice_glue.h @@ -0,0 +1,203 @@ +#pragma once + +#include +#include +#include +#include +#include + +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#define LowStar_Ignore_ignore(e, t, _ret_t) ((void)e) + +// SLICES, ARRAYS, ETC. + +// We represent a slice as a pair of an (untyped) pointer, along with the length of the slice, i.e. +// the number of elements in the slice (this is NOT the number of bytes). This design choice has two +// important consequences. +// - if you need to use `ptr`, you MUST cast it to a proper type *before* performing pointer +// arithmetic on it (remember that C desugars pointer arithmetic based on the type of the address) +// - if you need to use `len` for a C style function (e.g. memcpy, memcmp), you need to multiply it +// by sizeof t, where t is the type of the elements. +typedef struct { + void *ptr; + size_t len; +} Eurydice_slice; + +// Helper macro to create a slice out of a pointer x, a start index in x (included), and an end +// index in x (excluded). The argument x must be suitably cast to something that can decay (see +// remark above about how pointer arithmetic works in C), meaning either pointer or array type. +#define EURYDICE_SLICE(x, start, end) ((Eurydice_slice){ .ptr = (void*)(x + start), .len = end - start }) +#define EURYDICE_SLICE_LEN(s, _) s.len +#define Eurydice_slice_index(s, i, t, _ret_t) (((t*) s.ptr)[i]) +#define Eurydice_slice_subslice(s, r, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, r.start, r.end) +#define Eurydice_slice_subslice_to(s, subslice_end_pos, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, 0, subslice_end_pos) +#define Eurydice_slice_subslice_from(s, subslice_start_pos, t, _, _ret_t) EURYDICE_SLICE((t*)s.ptr, subslice_start_pos, s.len) +#define Eurydice_array_to_slice(end, x, t, _ret_t) EURYDICE_SLICE(x, 0, end) /* x is already at an array type, no need for cast */ +#define Eurydice_array_to_subslice(_arraylen, x, r, t, _, _ret_t) EURYDICE_SLICE((t*)x, r.start, r.end) +#define Eurydice_array_to_subslice_to(_size, x, r, t, _range_t, _ret_t) EURYDICE_SLICE((t*)x, 0, r) +#define Eurydice_array_to_subslice_from(size, x, r, t, _range_t, _ret_t) EURYDICE_SLICE((t*)x, r, size) +#define Eurydice_array_repeat(dst, len, init, t, _ret_t) ERROR "should've been desugared" +#define core_slice___Slice_T___len(s, t, _ret_t) EURYDICE_SLICE_LEN(s, t) +#define core_slice___Slice_T___copy_from_slice(dst, src, t, _ret_t) memcpy(dst.ptr, src.ptr, dst.len * sizeof(t)) +#define core_array___Array_T__N__23__as_slice(len_, ptr_, t, _ret_t) ((Eurydice_slice){ .ptr = ptr_, .len = len_ }) + +#define core_array_TryFromSliceError uint8_t + +#define core_array_equality___Array_A__N___eq(sz, a1, a2, t, _, _ret_t) (memcmp(a1, a2, sz * sizeof(t)) == 0) + +#define core_slice___Slice_T___split_at(slice, mid, element_type, ret_t) \ + ((ret_t){ \ + .fst = EURYDICE_SLICE((element_type*)slice.ptr, 0, mid), \ + .snd = EURYDICE_SLICE((element_type*)slice.ptr, mid, slice.len)}) + +// Can't have a flexible array as a member of a union -- this violates strict aliasing rules. +typedef struct +{ + uint8_t tag; + uint8_t case_Ok[]; +} +result_tryfromslice_flexible; + +#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) { + dst->tag = 0; + memcpy(dst->case_Ok, src.ptr, sz); +} + +// CORE STUFF (conversions, endianness, ...) + +static inline void core_num__u32_8__to_be_bytes(uint32_t src, uint8_t dst[4]) { + uint32_t x = htobe32(src); + memcpy(dst, &x, 4); +} + +static inline int64_t core_convert_num__i64_59__from(int32_t x) { return x; } +static inline int32_t core_convert_num__i32_56__from(int16_t x) { return x; } +// unsigned overflow wraparound semantics in C +static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x, uint16_t y) { return x + y; } +static inline uint8_t core_num__u8_6__wrapping_sub(uint8_t x, uint8_t y) { return x - y; } + +static inline void core_ops_arith__i32_319__add_assign(int32_t *x0, int32_t *x1) { + *x0 = *x0 + *x1; +} + +static inline uint8_t Eurydice_bitand_pv_u8(uint8_t *p, uint8_t v) { return (*p) & v; } +static inline uint8_t Eurydice_shr_pv_u8(uint8_t *p, int32_t v) { return (*p) >> v; } + +// ITERATORS + +#define core_num_nonzero_NonZeroUsize size_t +#define core_iter_range__core__ops__range__Range_A__3__next(iter_ptr, t, ret_t) ( \ + ((iter_ptr)->start == (iter_ptr)->end) ? \ + ((ret_t) { .tag = core_option_None }) : \ + ((ret_t) { .tag = core_option_Some, .f0 = (iter_ptr)->start++ }) \ + ) + +#define core_iter_traits_collect__I__into_iter(x, t, _ret_t) (x) + +typedef struct { + Eurydice_slice slice; + size_t chunk_size; +} Eurydice_chunks; + + +// Can't use macros Eurydice_slice_subslice_{to,from} because they require a type, and this static +// inline function cannot receive a type as an argument. Instead, we receive the element size and +// use it to peform manual offset computations rather than going through the macros. +static inline Eurydice_slice chunk_next(Eurydice_chunks *chunks, size_t element_size) { + size_t chunk_size = chunks->slice.len >= chunks->chunk_size ? chunks->chunk_size : chunks->slice.len; + Eurydice_slice curr_chunk = ((Eurydice_slice) { .ptr = chunks->slice.ptr, .len = chunk_size }); + chunks->slice = ((Eurydice_slice) { + .ptr = (char *)(chunks->slice.ptr) + chunk_size * element_size, + .len = chunks->slice.len - chunk_size + }); + return curr_chunk; +} + +#define core_slice___Slice_T___chunks(slice_, sz_, t, _ret_t) ((Eurydice_chunks){ .slice = slice_, .chunk_size = sz_ }) +#define core_slice___Slice_T___chunks_exact(slice_, sz_, t, _ret_t) ((Eurydice_chunks){ \ + .slice = { .ptr = slice_.ptr, .len = slice_.len - (slice_.len % sz_) }, \ + .chunk_size = sz_ }) +#define core_slice_iter_Chunks Eurydice_chunks +#define core_slice_iter_ChunksExact Eurydice_chunks +#define core_slice_iter__core__slice__iter__Chunks__a__T__70__next(iter, t, ret_t) \ + (((iter)->slice.len == 0) ? \ + ((ret_t) { .tag = core_option_None }) : \ + ((ret_t){ \ + .tag = core_option_Some, \ + .f0 = chunk_next(iter, sizeof(t)) })) +#define core_slice_iter__core__slice__iter__ChunksExact__a__T__89__next(iter, t, _ret_t) \ + core_slice_iter__core__slice__iter__Chunks__a__T__70__next(iter, t) + +typedef struct { + Eurydice_slice s; + size_t index; +} Eurydice_slice_iterator; + +#define core_slice___Slice_T___iter(x, t, _ret_t) ((Eurydice_slice_iterator){ .s = x, .index = 0 }) +#define core_slice_iter_Iter Eurydice_slice_iterator +#define core_slice_iter__core__slice__iter__Iter__a__T__181__next(iter, t, ret_t) \ + (((iter)->index == (iter)->s.len) ? \ + ((ret_t) { .tag = core_option_None }) : \ + ((ret_t){ \ + .tag = core_option_Some, \ + .f0 = ((iter)->index++, &((t*)((iter)->s.ptr))[(iter)->index-1]) })) + +// MISC + +#define core_fmt_Formatter void + + +// VECTORS + +/* For now these are passed by value -- three words. We could conceivably change + * the representation to heap-allocate this struct and only pass around the + * pointer (one word). */ +typedef struct { + void *ptr; + size_t len; /* the number of elements */ + size_t alloc_size; /* the size of the allocation, in number of BYTES */ +} Eurydice_vec_s, *Eurydice_vec; + +/* Here, we set everything to zero rather than use a non-standard GCC + * statement-expression -- this suitably initializes ptr to NULL and len and + * size to 0. */ +#define EURYDICE_VEC_NEW(_) calloc(1, sizeof(Eurydice_vec_s)) +#define EURYDICE_VEC_PUSH(v, x, t) \ + do { \ + /* Grow the vector if capacity has been reached. */ \ + if (v->len == v->alloc_size/sizeof(t)) { \ + /* Assuming that this does not exceed SIZE_MAX, because code proven \ + * correct by Aeneas. Would this even happen in practice? */ \ + size_t new_size; \ + if (v->alloc_size == 0) \ + new_size = 8 * sizeof(t); \ + else if (v->alloc_size <= SIZE_MAX/2) \ + /* TODO: discuss growth policy */ \ + new_size = 2 * v->alloc_size; \ + else \ + new_size = (SIZE_MAX/sizeof(t))*sizeof(t); \ + v->ptr = realloc(v->ptr, new_size); \ + v->alloc_size = new_size; \ + } \ + ((t*)v->ptr)[v->len] = x; \ + v->len++; \ + } while (0) + +#define EURYDICE_VEC_DROP(v, t) \ + do { \ + free(v->ptr); \ + free(v); \ + } while (0) + +#define EURYDICE_VEC_INDEX(v, i, t) &((t*) v->ptr)[i] +#define EURYDICE_VEC_LEN(v, t) (v)->len + +/* TODO: remove GCC-isms */ +#define EURYDICE_BOX_NEW(x, t) ({ t *p = malloc(sizeof(t)); *p = x; p; }) + +#define EURYDICE_REPLACE(ptr, new_v, t) ({ t old_v = *ptr; *ptr = new_v; old_v; }) + diff --git a/libcrux/include/internal/core.h b/libcrux/include/internal/core.h new file mode 100644 index 00000000..e4426c76 --- /dev/null +++ b/libcrux/include/internal/core.h @@ -0,0 +1,49 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf + KaRaMeL version: 0eda808b + */ + +#ifndef __internal_core_H +#define __internal_core_H + +#include "eurydice_glue.h" + +static inline int64_t core_convert_num__i64_59__from(int32_t x0); + +#define core_option_None 0 +#define core_option_Some 1 + +typedef uint8_t core_option_Option__size_t_tags; + +typedef struct core_option_Option__size_t_s +{ + core_option_Option__size_t_tags tag; + size_t f0; +} +core_option_Option__size_t; + +static inline uint16_t core_num__u16_7__wrapping_add(uint16_t x0, uint16_t x1); + +static inline uint8_t core_num__u8_6__wrapping_sub(uint8_t x0, uint8_t x1); + +#define CORE_NUM__U32_8__BITS (32U) + +typedef struct core_option_Option__uint32_t_s +{ + core_option_Option__size_t_tags tag; + uint32_t f0; +} +core_option_Option__uint32_t; + +typedef struct core_option_Option__int32_t_s +{ + core_option_Option__size_t_tags tag; + int32_t f0; +} +core_option_Option__int32_t; + + +#define __internal_core_H_DEFINED +#endif diff --git a/libcrux/include/libcrux_hacl_glue.h b/libcrux/include/libcrux_hacl_glue.h new file mode 100644 index 00000000..82269fd1 --- /dev/null +++ b/libcrux/include/libcrux_hacl_glue.h @@ -0,0 +1,34 @@ +#pragma once + +#include "eurydice_glue.h" + +typedef struct + __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__s +{ + uint8_t fst[840U]; + uint8_t snd[840U]; + uint8_t thd[840U]; + uint8_t f3[840U]; +} __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_; + +extern void +libcrux_digest_shake256f(size_t len, Eurydice_slice input, uint8_t* out); + +#define libcrux_digest_shake256(len, input, out, _) \ + libcrux_digest_shake256f(len, input, out) + +extern void +libcrux_digest_shake128f(size_t len, Eurydice_slice input, uint8_t* out); + +#define libcrux_digest_shake128(len, input, out, _) \ + libcrux_digest_shake128f(len, input, out) + +extern __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_ +libcrux_digest_shake128x4f(size_t len, + Eurydice_slice input0, + Eurydice_slice input1, + Eurydice_slice input2, + Eurydice_slice input3); + +#define libcrux_digest_shake128x4(len, input0, input1, input2, input3, _) \ + libcrux_digest_shake128x4f(len, input0, input1, input2, input3) diff --git a/libcrux/include/libcrux_kyber.h b/libcrux/include/libcrux_kyber.h new file mode 100644 index 00000000..43d74f3b --- /dev/null +++ b/libcrux/include/libcrux_kyber.h @@ -0,0 +1,674 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice + ../libcrux_kyber.llbc F* version: d0aa54cf KaRaMeL version: 0eda808b + */ + +#ifndef __libcrux_kyber_H +#define __libcrux_kyber_H + +#include "Eurydice.h" +#include "eurydice_glue.h" + +#define LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS ((int32_t)3329) + +#define LIBCRUX_KYBER_CONSTANTS_BITS_PER_COEFFICIENT ((size_t)12U) + +#define LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT ((size_t)256U) + +#define LIBCRUX_KYBER_CONSTANTS_BITS_PER_RING_ELEMENT \ + (LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * (size_t)12U) + +#define LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT \ + (LIBCRUX_KYBER_CONSTANTS_BITS_PER_RING_ELEMENT / (size_t)8U) + +#define LIBCRUX_KYBER_CONSTANTS_REJECTION_SAMPLING_SEED_SIZE \ + ((size_t)168U * (size_t)5U) + +#define LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE ((size_t)32U) + +#define LIBCRUX_KYBER_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE ((size_t)32U) + +#define LIBCRUX_KYBER_CONSTANTS_H_DIGEST_SIZE ((size_t)32U) + +#define LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_SHIFT (16U) + +#define LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_R \ + ((int32_t)1 << (uint32_t)LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_SHIFT) + +uint32_t +libcrux_kyber_arithmetic_get_n_least_significant_bits(uint8_t n, + uint32_t value); + +#define LIBCRUX_KYBER_ARITHMETIC_BARRETT_SHIFT ((int64_t)26) + +#define LIBCRUX_KYBER_ARITHMETIC_BARRETT_R \ + ((int64_t)1 << (uint32_t)LIBCRUX_KYBER_ARITHMETIC_BARRETT_SHIFT) + +#define LIBCRUX_KYBER_ARITHMETIC_BARRETT_MULTIPLIER ((int64_t)20159) + +int32_t +libcrux_kyber_arithmetic_barrett_reduce(int32_t value); + +#define LIBCRUX_KYBER_ARITHMETIC_INVERSE_OF_MODULUS_MOD_R (62209U) + +int32_t +libcrux_kyber_arithmetic_montgomery_reduce(int32_t value); + +int32_t +libcrux_kyber_arithmetic_montgomery_multiply_sfe_by_fer(int32_t fe, + int32_t fer); + +#define LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS \ + ((int32_t)1353) + +int32_t +libcrux_kyber_arithmetic_to_standard_domain(int32_t mfe); + +uint16_t +libcrux_kyber_arithmetic_to_unsigned_representative(int32_t fe); + +typedef int32_t libcrux_kyber_arithmetic_PolynomialRingElement[256U]; + +void + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement_1__clone( + int32_t (*self)[256U], + int32_t ret[256U]); + +extern const int32_t + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO + [256U]; + +uint8_t +libcrux_kyber_compress_compress_message_coefficient(uint16_t fe); + +int32_t +libcrux_kyber_compress_compress_ciphertext_coefficient(uint8_t coefficient_bits, + uint16_t fe); + +int32_t +libcrux_kyber_compress_decompress_message_coefficient(int32_t fe); + +int32_t +libcrux_kyber_compress_decompress_ciphertext_coefficient( + uint8_t coefficient_bits, + int32_t fe); + +uint8_t +libcrux_kyber_constant_time_ops_is_non_zero(uint8_t value); + +void +libcrux_kyber_constant_time_ops_select_shared_secret_in_constant_time( + Eurydice_slice lhs, + Eurydice_slice rhs, + uint8_t selector, + uint8_t ret[32U]); + +extern void +libcrux_digest_sha3_512(Eurydice_slice x0, uint8_t x1[64U]); + +void +libcrux_kyber_hash_functions_G(Eurydice_slice input, uint8_t ret[64U]); + +extern void +libcrux_digest_sha3_256(Eurydice_slice x0, uint8_t x1[32U]); + +void +libcrux_kyber_hash_functions_H(Eurydice_slice input, uint8_t ret[32U]); + +extern bool +libcrux_platform_simd256_support(void); + +typedef struct K___uint8_t_uint8_t_uint8_t_s +{ + uint8_t fst; + uint8_t snd; + uint8_t thd; +} K___uint8_t_uint8_t_uint8_t; + +K___uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_3(uint16_t coefficient1, + uint16_t coefficient2); + +void +libcrux_kyber_serialize_serialize_uncompressed_ring_element(int32_t re[256U], + uint8_t ret[384U]); + +void +libcrux_kyber_serialize_deserialize_to_uncompressed_ring_element( + Eurydice_slice serialized, + int32_t ret[256U]); + +void +libcrux_kyber_sampling_sample_from_binomial_distribution_2( + Eurydice_slice randomness, + int32_t ret[256U]); + +void +libcrux_kyber_sampling_sample_from_binomial_distribution_3( + Eurydice_slice randomness, + int32_t ret[256U]); + +extern const int32_t libcrux_kyber_ntt_ZETAS_TIMES_MONTGOMERY_R[128U]; + +void +libcrux_kyber_ntt_ntt_at_layer(size_t* zeta_i, + int32_t re[256U], + size_t layer, + size_t initial_coefficient_bound, + int32_t ret[256U]); + +void +libcrux_kyber_ntt_ntt_at_layer_3(size_t* zeta_i, + int32_t re[256U], + size_t layer, + int32_t ret[256U]); + +void +libcrux_kyber_ntt_ntt_binomially_sampled_ring_element(int32_t re[256U], + int32_t ret[256U]); + +void +libcrux_kyber_sampling_rejection_sampling_panic_with_diagnostic(void); + +void +libcrux_kyber_sampling_sample_from_uniform_distribution( + uint8_t randomness[840U], + int32_t ret[256U]); + +typedef struct K___int32_t_int32_t_s +{ + int32_t fst; + int32_t snd; +} K___int32_t_int32_t; + +K___int32_t_int32_t +libcrux_kyber_ntt_ntt_multiply_binomials(K___int32_t_int32_t _, + K___int32_t_int32_t _0, + int32_t zeta); + +void libcrux_kyber_ntt_ntt_multiply(int32_t (*lhs)[256U], + int32_t (*rhs)[256U], + int32_t ret[256U]); + +typedef struct K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_s +{ + uint8_t fst; + uint8_t snd; + uint8_t thd; + uint8_t f3; + uint8_t f4; +} K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t; + +K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_10(int32_t coefficient1, + int32_t coefficient2, + int32_t coefficient3, + int32_t coefficient4); + +typedef struct + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_s +{ + uint8_t fst; + uint8_t snd; + uint8_t thd; + uint8_t f3; + uint8_t f4; + uint8_t f5; + uint8_t f6; + uint8_t f7; + uint8_t f8; + uint8_t f9; + uint8_t f10; +} K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t; + +K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_11(int32_t coefficient1, + int32_t coefficient2, + int32_t coefficient3, + int32_t coefficient4, + int32_t coefficient5, + int32_t coefficient6, + int32_t coefficient7, + int32_t coefficient8); + +void +libcrux_kyber_ntt_invert_ntt_at_layer(size_t* zeta_i, + int32_t re[256U], + size_t layer, + int32_t ret[256U]); + +void +libcrux_kyber_serialize_deserialize_then_decompress_message( + uint8_t serialized[32U], + int32_t ret[256U]); + +K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_5(uint8_t coefficient2, + uint8_t coefficient1, + uint8_t coefficient4, + uint8_t coefficient3, + uint8_t coefficient5, + uint8_t coefficient7, + uint8_t coefficient6, + uint8_t coefficient8); + +typedef struct K___int32_t_int32_t_int32_t_int32_t_s +{ + int32_t fst; + int32_t snd; + int32_t thd; + int32_t f3; +} K___int32_t_int32_t_int32_t_int32_t; + +K___int32_t_int32_t_int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_10(int32_t byte2, + int32_t byte1, + int32_t byte3, + int32_t byte4, + int32_t byte5); + +void +libcrux_kyber_serialize_deserialize_then_decompress_10( + Eurydice_slice serialized, + int32_t ret[256U]); + +typedef struct + K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_s +{ + int32_t fst; + int32_t snd; + int32_t thd; + int32_t f3; + int32_t f4; + int32_t f5; + int32_t f6; + int32_t f7; +} K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t; + +K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_11(int32_t byte2, + int32_t byte1, + int32_t byte3, + int32_t byte5, + int32_t byte4, + int32_t byte6, + int32_t byte7, + int32_t byte9, + int32_t byte8, + int32_t byte10, + int32_t byte11); + +void +libcrux_kyber_serialize_deserialize_then_decompress_11( + Eurydice_slice serialized, + int32_t ret[256U]); + +void +libcrux_kyber_ntt_ntt_at_layer_3328(size_t* zeta_i, + int32_t re[256U], + size_t layer, + int32_t ret[256U]); + +K___int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_4(uint8_t* byte); + +void +libcrux_kyber_serialize_deserialize_then_decompress_4(Eurydice_slice serialized, + int32_t ret[256U]); + +K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_5(int32_t byte1, + int32_t byte2, + int32_t byte3, + int32_t byte4, + int32_t byte5); + +void +libcrux_kyber_serialize_deserialize_then_decompress_5(Eurydice_slice serialized, + int32_t ret[256U]); + +void +libcrux_kyber_serialize_compress_then_serialize_message(int32_t re[256U], + uint8_t ret[32U]); + +#define LIBCRUX_KYBER_KYBER768_RANK_768 ((size_t)3U) + +#define LIBCRUX_KYBER_KYBER768_RANKED_BYTES_PER_RING_ELEMENT_768 \ + (LIBCRUX_KYBER_KYBER768_RANK_768 * \ + LIBCRUX_KYBER_CONSTANTS_BITS_PER_RING_ELEMENT / (size_t)8U) + +#define LIBCRUX_KYBER_KYBER768_T_AS_NTT_ENCODED_SIZE_768 \ + (LIBCRUX_KYBER_KYBER768_RANK_768 * \ + LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_KYBER_CONSTANTS_BITS_PER_COEFFICIENT / (size_t)8U) + +#define LIBCRUX_KYBER_KYBER768_VECTOR_U_COMPRESSION_FACTOR_768 ((size_t)10U) + +#define LIBCRUX_KYBER_KYBER768_C1_BLOCK_SIZE_768 \ + (LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_KYBER_KYBER768_VECTOR_U_COMPRESSION_FACTOR_768 / (size_t)8U) + +#define LIBCRUX_KYBER_KYBER768_C1_SIZE_768 \ + (LIBCRUX_KYBER_KYBER768_C1_BLOCK_SIZE_768 * LIBCRUX_KYBER_KYBER768_RANK_768) + +#define LIBCRUX_KYBER_KYBER768_VECTOR_V_COMPRESSION_FACTOR_768 ((size_t)4U) + +#define LIBCRUX_KYBER_KYBER768_C2_SIZE_768 \ + (LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_KYBER_KYBER768_VECTOR_V_COMPRESSION_FACTOR_768 / (size_t)8U) + +#define LIBCRUX_KYBER_KYBER768_CPA_PKE_SECRET_KEY_SIZE_768 \ + (LIBCRUX_KYBER_KYBER768_RANK_768 * \ + LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * \ + LIBCRUX_KYBER_CONSTANTS_BITS_PER_COEFFICIENT / (size_t)8U) + +#define LIBCRUX_KYBER_KYBER768_CPA_PKE_PUBLIC_KEY_SIZE_768 \ + (LIBCRUX_KYBER_KYBER768_T_AS_NTT_ENCODED_SIZE_768 + (size_t)32U) + +#define LIBCRUX_KYBER_KYBER768_CPA_PKE_CIPHERTEXT_SIZE_768 \ + (LIBCRUX_KYBER_KYBER768_C1_SIZE_768 + LIBCRUX_KYBER_KYBER768_C2_SIZE_768) + +#define LIBCRUX_KYBER_KYBER768_SECRET_KEY_SIZE_768 \ + (LIBCRUX_KYBER_KYBER768_CPA_PKE_SECRET_KEY_SIZE_768 + \ + LIBCRUX_KYBER_KYBER768_CPA_PKE_PUBLIC_KEY_SIZE_768 + \ + LIBCRUX_KYBER_CONSTANTS_H_DIGEST_SIZE + \ + LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE) + +#define LIBCRUX_KYBER_KYBER768_ETA1 ((size_t)2U) + +#define LIBCRUX_KYBER_KYBER768_ETA1_RANDOMNESS_SIZE \ + (LIBCRUX_KYBER_KYBER768_ETA1 * (size_t)64U) + +#define LIBCRUX_KYBER_KYBER768_ETA2 ((size_t)2U) + +#define LIBCRUX_KYBER_KYBER768_ETA2_RANDOMNESS_SIZE \ + (LIBCRUX_KYBER_KYBER768_ETA2 * (size_t)64U) + +#define LIBCRUX_KYBER_KYBER768_IMPLICIT_REJECTION_HASH_INPUT_SIZE \ + (LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE + \ + LIBCRUX_KYBER_KYBER768_CPA_PKE_CIPHERTEXT_SIZE_768) + +void +libcrux_kyber_hash_functions_XOFx4___3size_t(uint8_t input[3U][34U], + uint8_t ret[3U][840U]); + +void +libcrux_kyber_matrix_sample_matrix_A___3size_t(uint8_t seed[34U], + bool transpose, + int32_t ret[3U][3U][256U]); + +void +libcrux_kyber_ind_cpa_into_padded_array___34size_t(Eurydice_slice slice, + uint8_t ret[34U]); + +void +libcrux_kyber_ind_cpa_into_padded_array___33size_t(Eurydice_slice slice, + uint8_t ret[33U]); + +void +libcrux_kyber_hash_functions_PRF___128size_t(Eurydice_slice input, + uint8_t ret[128U]); + +void +libcrux_kyber_sampling_sample_from_binomial_distribution___2size_t( + Eurydice_slice randomness, + int32_t ret[256U]); + +typedef struct + K___libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__uint8_t_s +{ + int32_t fst[3U][256U]; + uint8_t snd; +} K___libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__uint8_t; + +K___libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__uint8_t +libcrux_kyber_ind_cpa_sample_vector_cbd_then_ntt___3size_t_2size_t_128size_t( + uint8_t prf_input[33U], + uint8_t domain_separator); + +void +libcrux_kyber_arithmetic_add_to_ring_element___3size_t(int32_t lhs[256U], + int32_t (*rhs)[256U], + int32_t ret[256U]); + +void libcrux_kyber_matrix_compute_As_plus_e___3size_t( + int32_t (*matrix_A)[3U][256U], + int32_t (*s_as_ntt)[256U], + int32_t (*error_as_ntt)[256U], + int32_t ret[3U][256U]); + +void +libcrux_kyber_ind_cpa_serialize_secret_key___3size_t_1152size_t( + int32_t key[3U][256U], + uint8_t ret[1152U]); + +void +libcrux_kyber_ind_cpa_serialize_public_key___3size_t_1152size_t_1184size_t( + int32_t t_as_ntt[3U][256U], + Eurydice_slice seed_for_a, + uint8_t ret[1184U]); + +typedef struct K___uint8_t_1152size_t__uint8_t_1184size_t__s +{ + uint8_t fst[1152U]; + uint8_t snd[1184U]; +} K___uint8_t_1152size_t__uint8_t_1184size_t_; + +typedef struct K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t_s +{ + Eurydice_slice fst; + Eurydice_slice snd; +} K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t; + +K___uint8_t_1152size_t__uint8_t_1184size_t_ +libcrux_kyber_ind_cpa_generate_keypair___3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t( + Eurydice_slice key_generation_seed); + +void +libcrux_kyber_serialize_kem_secret_key___2400size_t( + Eurydice_slice private_key, + Eurydice_slice public_key, + Eurydice_slice implicit_rejection_value, + uint8_t ret[2400U]); + +typedef uint8_t libcrux_kyber_types_KyberPrivateKey___2400size_t[2400U]; + +void +libcrux_kyber_types__libcrux_kyber__types__KyberPrivateKey_SIZE__8__from___2400size_t( + uint8_t value[2400U], + uint8_t ret[2400U]); + +typedef uint8_t libcrux_kyber_types_KyberPublicKey___1184size_t[1184U]; + +typedef struct libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t_s +{ + uint8_t sk[2400U]; + uint8_t pk[1184U]; +} libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t; + +libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t +libcrux_kyber_types__libcrux_kyber__types__KyberKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t( + uint8_t sk[2400U], + uint8_t pk[1184U]); + +libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t +libcrux_kyber_generate_keypair___3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t( + uint8_t randomness[64U]); + +libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t +libcrux_kyber_kyber768_generate_key_pair_768(uint8_t randomness[64U]); + +void +libcrux_kyber_ind_cpa_into_padded_array___64size_t(Eurydice_slice slice, + uint8_t ret[64U]); + +uint8_t* + libcrux_kyber_types__libcrux_kyber__types__KyberPublicKey_SIZE__18__as_slice___1184size_t( + uint8_t (*self)[1184U]); + +void +libcrux_kyber_ind_cpa_deserialize_public_key___3size_t( + Eurydice_slice public_key, + int32_t ret[3U][256U]); + +void +libcrux_kyber_ind_cpa_sample_ring_element_cbd___3size_t_128size_t_2size_t( + uint8_t* prf_input, + uint8_t* domain_separator, + int32_t ret[3U][256U]); + +void +libcrux_kyber_ntt_invert_ntt_montgomery___3size_t(int32_t re[256U], + int32_t ret[256U]); + +void libcrux_kyber_matrix_compute_vector_u___3size_t( + int32_t (*a_as_ntt)[3U][256U], + int32_t (*r_as_ntt)[256U], + int32_t (*error_1)[256U], + int32_t ret[3U][256U]); + +void libcrux_kyber_matrix_compute_ring_element_v___3size_t( + int32_t (*t_as_ntt)[256U], + int32_t (*r_as_ntt)[256U], + int32_t (*error_2)[256U], + int32_t (*message)[256U], + int32_t ret[256U]); + +void +libcrux_kyber_serialize_compress_then_serialize_10___320size_t( + int32_t re[256U], + uint8_t ret[320U]); + +void +libcrux_kyber_serialize_compress_then_serialize_11___320size_t( + int32_t re[256U], + uint8_t ret[320U]); + +void +libcrux_kyber_serialize_compress_then_serialize_ring_element_u___10size_t_320size_t( + int32_t re[256U], + uint8_t ret[320U]); + +void +libcrux_kyber_ind_cpa_compress_then_serialize_u___3size_t_960size_t_10size_t_320size_t( + int32_t input[3U][256U], + uint8_t ret[960U]); + +void +libcrux_kyber_serialize_compress_then_serialize_4___128size_t( + int32_t re[256U], + uint8_t ret[128U]); + +void +libcrux_kyber_serialize_compress_then_serialize_5___128size_t( + int32_t re[256U], + uint8_t ret[128U]); + +void +libcrux_kyber_serialize_compress_then_serialize_ring_element_v___4size_t_128size_t( + int32_t re[256U], + uint8_t ret[128U]); + +void +libcrux_kyber_ind_cpa_into_padded_array___1088size_t(Eurydice_slice slice, + uint8_t ret[1088U]); + +void +libcrux_kyber_ind_cpa_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]); + +typedef uint8_t libcrux_kyber_types_KyberCiphertext___1088size_t[1088U]; + +typedef struct + K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t__s +{ + uint8_t fst[1088U]; + uint8_t snd[32U]; +} K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t_; + +K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t_ + libcrux_kyber_encapsulate___3size_t_1088size_t_1184size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t( + uint8_t (*public_key)[1184U], + uint8_t randomness[32U]); + +K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t_ + libcrux_kyber_kyber768_encapsulate_768(uint8_t (*public_key)[1184U], + uint8_t randomness[32U]); + +K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t + libcrux_kyber_types__libcrux_kyber__types__KyberPrivateKey_SIZE__12__split_at___2400size_t( + uint8_t (*self)[2400U], + size_t mid); + +void +libcrux_kyber_serialize_deserialize_then_decompress_ring_element_u___10size_t( + Eurydice_slice serialized, + int32_t ret[256U]); + +void +libcrux_kyber_ntt_ntt_vector_u___10size_t(int32_t re[256U], int32_t ret[256U]); + +void +libcrux_kyber_ind_cpa_deserialize_then_decompress_u___3size_t_1088size_t_10size_t( + uint8_t* ciphertext, + int32_t ret[3U][256U]); + +void +libcrux_kyber_serialize_deserialize_then_decompress_ring_element_v___4size_t( + Eurydice_slice serialized, + int32_t ret[256U]); + +void +libcrux_kyber_ind_cpa_deserialize_secret_key___3size_t( + Eurydice_slice secret_key, + int32_t ret[3U][256U]); + +void libcrux_kyber_matrix_compute_message___3size_t( + int32_t (*v)[256U], + int32_t (*secret_as_ntt)[256U], + int32_t (*u_as_ntt)[256U], + int32_t ret[256U]); + +void +libcrux_kyber_ind_cpa_decrypt___3size_t_1088size_t_960size_t_10size_t_4size_t( + Eurydice_slice secret_key, + uint8_t* ciphertext, + uint8_t ret[32U]); + +void +libcrux_kyber_ind_cpa_into_padded_array___1120size_t(Eurydice_slice slice, + uint8_t ret[1120U]); + +Eurydice_slice + libcrux_kyber_types__libcrux_kyber__types__KyberCiphertext_SIZE__1__as_ref___1088size_t( + uint8_t (*self)[1088U]); + +void +libcrux_kyber_hash_functions_PRF___32size_t(Eurydice_slice input, + uint8_t ret[32U]); + +uint8_t +libcrux_kyber_constant_time_ops_compare_ciphertexts_in_constant_time___1088size_t( + Eurydice_slice lhs, + Eurydice_slice rhs); + +void + libcrux_kyber_decapsulate___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( + uint8_t (*secret_key)[2400U], + uint8_t (*ciphertext)[1088U], + uint8_t ret[32U]); + +void libcrux_kyber_kyber768_decapsulate_768(uint8_t (*secret_key)[2400U], + uint8_t (*ciphertext)[1088U], + uint8_t ret[32U]); + +#define LIBCRUX_KYBER_KEY_GENERATION_SEED_SIZE \ + (LIBCRUX_KYBER_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE + \ + LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE) + +#define __libcrux_kyber_H_DEFINED +#endif diff --git a/libcrux/src/Eurydice.c b/libcrux/src/Eurydice.c new file mode 100644 index 00000000..884842e7 --- /dev/null +++ b/libcrux/src/Eurydice.c @@ -0,0 +1,13 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf + KaRaMeL version: 0eda808b + */ + +#include "Eurydice.h" + +typedef size_t RangeTo__size_t; + +typedef size_t RangeFrom__size_t; + diff --git a/libcrux/src/Libcrux_Kem_Kyber_Kyber768.c b/libcrux/src/Libcrux_Kem_Kyber_Kyber768.c index 05aa8d48..6713f2b1 100644 --- a/libcrux/src/Libcrux_Kem_Kyber_Kyber768.c +++ b/libcrux/src/Libcrux_Kem_Kyber_Kyber768.c @@ -1,36 +1,36 @@ #include #include "Libcrux_Kem_Kyber_Kyber768.h" +#include "libcrux_kyber.h" -int +void Libcrux_Kyber768_GenerateKeyPair(uint8_t* pk, uint8_t* sk, - const uint8_t* randomness) + uint8_t randomness[64]) { - (void)randomness; - memset(pk, 0, KYBER768_PUBLICKEYBYTES); - memset(sk, 0, KYBER768_SECRETKEYBYTES); - return 0; + libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t result = + libcrux_kyber_kyber768_generate_key_pair_768(randomness); + + memcpy(pk, result.pk, KYBER768_PUBLICKEYBYTES); + memcpy(sk, result.sk, KYBER768_SECRETKEYBYTES); } -int +void Libcrux_Kyber768_Encapsulate(uint8_t* ct, uint8_t* ss, - const uint8_t* pk, - const uint8_t* randomness) + uint8_t (*pk)[1184], + uint8_t randomness[32]) { - (void)pk; - (void)randomness; - memset(ct, 0, KYBER768_CIPHERTEXTBYTES); - memset(ss, 0, KYBER768_SHAREDSECRETBYTES); - return 0; + K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t_ + result = libcrux_kyber_kyber768_encapsulate_768(pk, randomness); + memcpy(ct, result.fst, KYBER768_CIPHERTEXTBYTES); + memcpy(ss, result.snd, KYBER768_SHAREDSECRETBYTES); } -int -Libcrux_Kyber768_Decapsulate(uint8_t* ss, const uint8_t* ct, const uint8_t* sk) +void +Libcrux_Kyber768_Decapsulate(uint8_t ss[32U], + uint8_t (*ct)[1088U], + uint8_t (*sk)[2400U]) { - (void)sk; - (void)ct; - memset(ss, 0, KYBER768_SHAREDSECRETBYTES); - return 0; + libcrux_kyber_kyber768_decapsulate_768(sk, ct, ss); } diff --git a/libcrux/src/LowStar_Ignore.c b/libcrux/src/LowStar_Ignore.c new file mode 100644 index 00000000..5048b113 --- /dev/null +++ b/libcrux/src/LowStar_Ignore.c @@ -0,0 +1,11 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf + KaRaMeL version: 1f52609c + */ + +#include "LowStar_Ignore.h" + + + diff --git a/libcrux/src/core.c b/libcrux/src/core.c new file mode 100644 index 00000000..4de8b4e5 --- /dev/null +++ b/libcrux/src/core.c @@ -0,0 +1,11 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf + KaRaMeL version: 1f52609c + */ + +#include "internal/core.h" + + + diff --git a/libcrux/src/libcrux_hacl_glue.c b/libcrux/src/libcrux_hacl_glue.c new file mode 100644 index 00000000..4346053f --- /dev/null +++ b/libcrux/src/libcrux_hacl_glue.c @@ -0,0 +1,80 @@ +#include "libcrux_hacl_glue.h" +#include "Hacl_Hash_SHA3.h" +#include "libcrux_kyber.h" + +#ifdef HACL_CAN_COMPILE_VEC256 +#include "Hacl_Hash_SHA3_Simd256.h" +#endif + +bool +libcrux_platform_simd256_support(void) +{ + // TODO: Replace this with HACL platform support. + return false; +} + +inline void +libcrux_digest_shake256f(size_t len, Eurydice_slice input, uint8_t* out) +{ + Hacl_Hash_SHA3_shake256_hacl(input.len, input.ptr, (uint32_t)len, out); +} + +inline void +libcrux_digest_shake128f(size_t len, Eurydice_slice input, uint8_t* out) +{ + Hacl_Hash_SHA3_shake128_hacl(input.len, input.ptr, (uint32_t)len, out); +} + +inline __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_ +libcrux_digest_shake128x4f(size_t len, + Eurydice_slice input0, + Eurydice_slice input1, + Eurydice_slice input2, + Eurydice_slice input3) +{ + __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_ + out = + (__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_){ + .fst = { 0 }, .snd = { 0 }, .thd = { 0 }, .f3 = { 0 } + }; +#ifdef HACL_CAN_COMPILE_VEC256 + if (libcrux_platform_simd256_support() == true) { + Hacl_Hash_SHA3_Simd256_shake128(input0.len, + input0.ptr, + input1.ptr, + input2.ptr, + input3.ptr, + (uint32_t)len, + out.fst, + out.snd, + out.thd, + out.f3); + } else { + Hacl_Hash_SHA3_shake128_hacl( + input0.len, input0.ptr, (uint32_t)len, out.fst); + Hacl_Hash_SHA3_shake128_hacl( + input1.len, input1.ptr, (uint32_t)len, out.snd); + Hacl_Hash_SHA3_shake128_hacl( + input2.len, input2.ptr, (uint32_t)len, out.thd); + Hacl_Hash_SHA3_shake128_hacl(input3.len, input3.ptr, (uint32_t)len, out.f3); + } +#else + Hacl_Hash_SHA3_shake128_hacl(input0.len, input0.ptr, (uint32_t)len, out.fst); + Hacl_Hash_SHA3_shake128_hacl(input1.len, input1.ptr, (uint32_t)len, out.snd); + Hacl_Hash_SHA3_shake128_hacl(input2.len, input2.ptr, (uint32_t)len, out.thd); + Hacl_Hash_SHA3_shake128_hacl(input3.len, input3.ptr, (uint32_t)len, out.f3); +#endif + return out; +} + +inline void +libcrux_digest_sha3_512(Eurydice_slice x0, uint8_t x1[64U]) +{ + Hacl_Hash_SHA3_sha3_512(x1, x0.ptr, (uint32_t)x0.len); +} + +inline void +libcrux_digest_sha3_256(Eurydice_slice x0, uint8_t x1[32U]) +{ + Hacl_Hash_SHA3_sha3_256(x1, x0.ptr, (uint32_t)x0.len); +} diff --git a/libcrux/src/libcrux_kyber.c b/libcrux/src/libcrux_kyber.c new file mode 100644 index 00000000..a913cbf3 --- /dev/null +++ b/libcrux/src/libcrux_kyber.c @@ -0,0 +1,4505 @@ +/* + This file was generated by KaRaMeL + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice + ../libcrux_kyber.llbc F* version: d0aa54cf KaRaMeL version: 0eda808b + */ + +#include "libcrux_kyber.h" +#include "libcrux_hacl_glue.h" + +#include "internal/core.h" + +uint32_t +libcrux_kyber_arithmetic_get_n_least_significant_bits(uint8_t n, uint32_t value) +{ + return value & ((1U << (uint32_t)n) - 1U); +} + +int32_t +libcrux_kyber_arithmetic_barrett_reduce(int32_t value) +{ + int64_t t = core_convert_num__i64_59__from(value) * + LIBCRUX_KYBER_ARITHMETIC_BARRETT_MULTIPLIER + + (LIBCRUX_KYBER_ARITHMETIC_BARRETT_R >> 1U); + int32_t quotient = + (int32_t)(t >> (uint32_t)LIBCRUX_KYBER_ARITHMETIC_BARRETT_SHIFT); + return value - quotient * LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS; +} + +int32_t +libcrux_kyber_arithmetic_montgomery_reduce(int32_t value) +{ + uint32_t t = libcrux_kyber_arithmetic_get_n_least_significant_bits( + LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_SHIFT, (uint32_t)value) * + LIBCRUX_KYBER_ARITHMETIC_INVERSE_OF_MODULUS_MOD_R; + int16_t k = (int16_t)libcrux_kyber_arithmetic_get_n_least_significant_bits( + LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_SHIFT, t); + int32_t k_times_modulus = (int32_t)k * LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS; + int32_t c = + k_times_modulus >> (uint32_t)LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_SHIFT; + int32_t value_high = + value >> (uint32_t)LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_SHIFT; + return value_high - c; +} + +int32_t +libcrux_kyber_arithmetic_montgomery_multiply_sfe_by_fer(int32_t fe, int32_t fer) +{ + return libcrux_kyber_arithmetic_montgomery_reduce(fe * fer); +} + +int32_t +libcrux_kyber_arithmetic_to_standard_domain(int32_t mfe) +{ + return libcrux_kyber_arithmetic_montgomery_reduce( + mfe * LIBCRUX_KYBER_ARITHMETIC_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS); +} + +uint16_t +libcrux_kyber_arithmetic_to_unsigned_representative(int32_t fe) +{ + return (uint16_t)(fe + (LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS & fe >> 31U)); +} + +void +libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement_1__clone( + int32_t (*self)[256U], + int32_t ret[256U]) +{ + memcpy(ret, self[0U], (size_t)256U * sizeof(int32_t)); +} + +const int32_t + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO + [256U] = { 0U }; + +uint8_t +libcrux_kyber_compress_compress_message_coefficient(uint16_t fe) +{ + int16_t shifted = (int16_t)1664 - (int16_t)fe; + int16_t mask = shifted >> 15U; + int16_t shifted_to_positive = mask ^ shifted; + int16_t shifted_positive_in_range = shifted_to_positive - (int16_t)832; + return (uint8_t)(shifted_positive_in_range >> 15U & (int16_t)1); +} + +int32_t +libcrux_kyber_compress_compress_ciphertext_coefficient(uint8_t coefficient_bits, + uint16_t fe) +{ + uint64_t compressed = (uint64_t)fe << (uint32_t)coefficient_bits; + compressed = compressed + 1664ULL; + compressed = compressed * 10321340ULL; + compressed = compressed >> 35U; + return (int32_t)libcrux_kyber_arithmetic_get_n_least_significant_bits( + coefficient_bits, (uint32_t)compressed); +} + +int32_t +libcrux_kyber_compress_decompress_message_coefficient(int32_t fe) +{ + return -fe & + (LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS + (int32_t)1) / (int32_t)2; +} + +int32_t +libcrux_kyber_compress_decompress_ciphertext_coefficient( + uint8_t coefficient_bits, + int32_t fe) +{ + uint32_t decompressed = + (uint32_t)fe * (uint32_t)LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS; + decompressed = (decompressed << 1U) + (1U << (uint32_t)coefficient_bits); + decompressed = decompressed >> (uint32_t)((uint32_t)coefficient_bits + 1U); + return (int32_t)decompressed; +} + +uint8_t +libcrux_kyber_constant_time_ops_is_non_zero(uint8_t value) +{ + uint16_t value0 = (uint16_t)value; + uint16_t uu____0 = value0; + uint16_t result = (((uint32_t)uu____0 | + (uint32_t)core_num__u16_7__wrapping_add(~value0, 1U)) & + 0xFFFFU) >> + 8U & + 1U; + return (uint8_t)result; +} + +void +libcrux_kyber_constant_time_ops_select_shared_secret_in_constant_time( + Eurydice_slice lhs, + Eurydice_slice rhs, + uint8_t selector, + uint8_t ret[32U]) +{ + uint8_t mask = core_num__u8_6__wrapping_sub( + libcrux_kyber_constant_time_ops_is_non_zero(selector), 1U); + uint8_t out[32U]; + for (size_t i = (size_t)0U; i < (size_t)32U; i++) + out[i] = 0U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE }), + 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__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; + uint8_t uu____1 = + (uint32_t)Eurydice_slice_index(lhs, i, uint8_t, uint8_t) & + (uint32_t)mask; + uint8_t* uu____2 = &Eurydice_slice_index(rhs, i, uint8_t, uint8_t); + size_t uu____3 = i; + out[uu____3] = + (uint32_t)out[uu____3] | + ((uint32_t)uu____1 | ((uint32_t)uu____2[0U] & (uint32_t)~mask)); + } + } + uint8_t uu____4[32U]; + memcpy(uu____4, out, (size_t)32U * sizeof(uint8_t)); + memcpy(ret, uu____4, (size_t)32U * sizeof(uint8_t)); +} + +void +libcrux_kyber_hash_functions_G(Eurydice_slice input, uint8_t ret[64U]) +{ + uint8_t ret0[64U]; + libcrux_digest_sha3_512(input, ret0); + memcpy(ret, ret0, (size_t)64U * sizeof(uint8_t)); +} + +void +libcrux_kyber_hash_functions_H(Eurydice_slice input, uint8_t ret[32U]) +{ + uint8_t ret0[32U]; + libcrux_digest_sha3_256(input, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} + +K___uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_3(uint16_t coefficient1, + uint16_t coefficient2) +{ + uint8_t coef1 = (uint8_t)((uint32_t)coefficient1 & 255U); + uint8_t coef2 = (uint8_t)((uint32_t)coefficient1 >> 8U | + ((uint32_t)coefficient2 & 15U) << 4U); + uint8_t coef3 = (uint8_t)((uint32_t)coefficient2 >> 4U & 255U); + return ( + (K___uint8_t_uint8_t_uint8_t){ .fst = coef1, .snd = coef2, .thd = coef3 }); +} + +void +libcrux_kyber_serialize_serialize_uncompressed_ring_element(int32_t re[256U], + uint8_t ret[384U]) +{ + uint8_t serialized[384U]; + for (size_t i = (size_t)0U; i < (size_t)384U; i++) + serialized[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = + core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)256U, re, int32_t, Eurydice_slice), + int32_t, + size_t) / + (size_t)2U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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 coefficients = Eurydice_array_to_subslice( + (size_t)256U, + re, + ((core_ops_range_Range__size_t){ .start = i * (size_t)2U, + .end = i * (size_t)2U + (size_t)2U }), + int32_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint16_t coefficient1 = + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)0U, int32_t, int32_t)); + uint16_t coefficient2 = + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)1U, int32_t, int32_t)); + K___uint8_t_uint8_t_uint8_t uu____1 = + libcrux_kyber_serialize_compress_coefficients_3(coefficient1, + coefficient2); + uint8_t coef1 = uu____1.fst; + uint8_t coef2 = uu____1.snd; + uint8_t coef3 = uu____1.thd; + serialized[(size_t)3U * i] = coef1; + serialized[(size_t)3U * i + (size_t)1U] = coef2; + 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)); +} + +void +libcrux_kyber_serialize_deserialize_to_uncompressed_ring_element( + Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy( + re, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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__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)); +} + +typedef struct Range__uint32_t_s +{ + uint32_t start; + uint32_t end; +} Range__uint32_t; + +void +libcrux_kyber_sampling_sample_from_binomial_distribution_2( + Eurydice_slice randomness, + int32_t ret[256U]) +{ + int32_t sampled[256U]; + memcpy( + sampled, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = + core_slice___Slice_T___len(randomness, uint8_t, size_t) / (size_t)4U }), + 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__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) + break; + else { + size_t chunk_number = uu____0.f0; + Eurydice_slice byte_chunk = Eurydice_slice_subslice( + randomness, + ((core_ops_range_Range__size_t){ .start = chunk_number * (size_t)4U, + .end = chunk_number * (size_t)4U + + (size_t)4U }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint32_t uu____1 = (uint32_t)Eurydice_slice_index( + byte_chunk, (size_t)0U, uint8_t, uint8_t); + uint32_t uu____2 = + uu____1 | + (uint32_t)Eurydice_slice_index(byte_chunk, (size_t)1U, uint8_t, uint8_t) + << 8U; + uint32_t uu____3 = + uu____2 | + (uint32_t)Eurydice_slice_index(byte_chunk, (size_t)2U, uint8_t, uint8_t) + << 16U; + uint32_t random_bits_as_u32 = + uu____3 | + (uint32_t)Eurydice_slice_index(byte_chunk, (size_t)3U, uint8_t, uint8_t) + << 24U; + uint32_t even_bits = random_bits_as_u32 & 1431655765U; + uint32_t odd_bits = random_bits_as_u32 >> 1U & 1431655765U; + uint32_t coin_toss_outcomes = even_bits + odd_bits; + Range__uint32_t iter = core_iter_traits_collect__I__into_iter( + ((Range__uint32_t){ .start = 0U, .end = CORE_NUM__U32_8__BITS / 4U }), + Range__uint32_t, + Range__uint32_t); + while (true) { + core_option_Option__uint32_t uu____4 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter, uint32_t, core_option_Option__uint32_t); + if (uu____4.tag == core_option_None) + break; + else { + uint32_t outcome_set = uu____4.f0; + uint32_t outcome_set0 = outcome_set * 4U; + int32_t outcome_1 = + (int32_t)(coin_toss_outcomes >> (uint32_t)outcome_set0 & 3U); + int32_t outcome_2 = + (int32_t)(coin_toss_outcomes >> (uint32_t)(outcome_set0 + 2U) & 3U); + size_t offset = (size_t)(outcome_set0 >> 2U); + sampled[(size_t)8U * chunk_number + offset] = outcome_1 - outcome_2; + } + } + } + } + memcpy(ret, sampled, (size_t)256U * sizeof(int32_t)); +} + +typedef struct Range__int32_t_s +{ + int32_t start; + int32_t end; +} Range__int32_t; + +void +libcrux_kyber_sampling_sample_from_binomial_distribution_3( + Eurydice_slice randomness, + int32_t ret[256U]) +{ + int32_t sampled[256U]; + memcpy( + sampled, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = + core_slice___Slice_T___len(randomness, 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__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) + break; + else { + size_t chunk_number = uu____0.f0; + Eurydice_slice byte_chunk = Eurydice_slice_subslice( + randomness, + ((core_ops_range_Range__size_t){ .start = chunk_number * (size_t)3U, + .end = chunk_number * (size_t)3U + + (size_t)3U }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint32_t uu____1 = (uint32_t)Eurydice_slice_index( + byte_chunk, (size_t)0U, uint8_t, uint8_t); + uint32_t uu____2 = + uu____1 | + (uint32_t)Eurydice_slice_index(byte_chunk, (size_t)1U, uint8_t, uint8_t) + << 8U; + uint32_t random_bits_as_u24 = + uu____2 | + (uint32_t)Eurydice_slice_index(byte_chunk, (size_t)2U, uint8_t, uint8_t) + << 16U; + uint32_t first_bits = random_bits_as_u24 & 2396745U; + uint32_t second_bits = random_bits_as_u24 >> 1U & 2396745U; + uint32_t third_bits = random_bits_as_u24 >> 2U & 2396745U; + uint32_t coin_toss_outcomes = first_bits + second_bits + third_bits; + Range__int32_t iter = core_iter_traits_collect__I__into_iter( + ((Range__int32_t){ .start = (int32_t)0, + .end = (int32_t)24 / (int32_t)6 }), + Range__int32_t, + Range__int32_t); + while (true) { + core_option_Option__int32_t uu____3 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter, int32_t, core_option_Option__int32_t); + if (uu____3.tag == core_option_None) + break; + else { + int32_t outcome_set = uu____3.f0; + int32_t outcome_set0 = outcome_set * (int32_t)6; + int32_t outcome_1 = + (int32_t)(coin_toss_outcomes >> (uint32_t)outcome_set0 & 7U); + int32_t outcome_2 = + (int32_t)(coin_toss_outcomes >> + (uint32_t)(outcome_set0 + (int32_t)3) & + 7U); + size_t offset = (size_t)(outcome_set0 / (int32_t)6); + sampled[(size_t)4U * chunk_number + offset] = outcome_1 - outcome_2; + } + } + } + } + memcpy(ret, sampled, (size_t)256U * sizeof(int32_t)); +} + +const int32_t libcrux_kyber_ntt_ZETAS_TIMES_MONTGOMERY_R[128U] = { + (int32_t)-1044, (int32_t)-758, (int32_t)-359, (int32_t)-1517, + (int32_t)1493, (int32_t)1422, (int32_t)287, (int32_t)202, + (int32_t)-171, (int32_t)622, (int32_t)1577, (int32_t)182, + (int32_t)962, (int32_t)-1202, (int32_t)-1474, (int32_t)1468, + (int32_t)573, (int32_t)-1325, (int32_t)264, (int32_t)383, + (int32_t)-829, (int32_t)1458, (int32_t)-1602, (int32_t)-130, + (int32_t)-681, (int32_t)1017, (int32_t)732, (int32_t)608, + (int32_t)-1542, (int32_t)411, (int32_t)-205, (int32_t)-1571, + (int32_t)1223, (int32_t)652, (int32_t)-552, (int32_t)1015, + (int32_t)-1293, (int32_t)1491, (int32_t)-282, (int32_t)-1544, + (int32_t)516, (int32_t)-8, (int32_t)-320, (int32_t)-666, + (int32_t)-1618, (int32_t)-1162, (int32_t)126, (int32_t)1469, + (int32_t)-853, (int32_t)-90, (int32_t)-271, (int32_t)830, + (int32_t)107, (int32_t)-1421, (int32_t)-247, (int32_t)-951, + (int32_t)-398, (int32_t)961, (int32_t)-1508, (int32_t)-725, + (int32_t)448, (int32_t)-1065, (int32_t)677, (int32_t)-1275, + (int32_t)-1103, (int32_t)430, (int32_t)555, (int32_t)843, + (int32_t)-1251, (int32_t)871, (int32_t)1550, (int32_t)105, + (int32_t)422, (int32_t)587, (int32_t)177, (int32_t)-235, + (int32_t)-291, (int32_t)-460, (int32_t)1574, (int32_t)1653, + (int32_t)-246, (int32_t)778, (int32_t)1159, (int32_t)-147, + (int32_t)-777, (int32_t)1483, (int32_t)-602, (int32_t)1119, + (int32_t)-1590, (int32_t)644, (int32_t)-872, (int32_t)349, + (int32_t)418, (int32_t)329, (int32_t)-156, (int32_t)-75, + (int32_t)817, (int32_t)1097, (int32_t)603, (int32_t)610, + (int32_t)1322, (int32_t)-1285, (int32_t)-1465, (int32_t)384, + (int32_t)-1215, (int32_t)-136, (int32_t)1218, (int32_t)-1335, + (int32_t)-874, (int32_t)220, (int32_t)-1187, (int32_t)-1659, + (int32_t)-1185, (int32_t)-1530, (int32_t)-1278, (int32_t)794, + (int32_t)-1510, (int32_t)-854, (int32_t)-870, (int32_t)478, + (int32_t)-108, (int32_t)-308, (int32_t)996, (int32_t)991, + (int32_t)958, (int32_t)-1460, (int32_t)1522, (int32_t)1628 +}; + +void +libcrux_kyber_ntt_ntt_at_layer(size_t* zeta_i, + int32_t re[256U], + size_t layer, + size_t initial_coefficient_bound, + int32_t ret[256U]) +{ + size_t step = (size_t)1U << (uint32_t)layer; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)128U >> (uint32_t)layer }), + 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__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 round = uu____0.f0; + zeta_i[0U] = zeta_i[0U] + (size_t)1U; + size_t offset = round * step * (size_t)2U; + core_ops_range_Range__size_t iter0 = + core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = offset, + .end = offset + step }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t j = uu____1.f0; + int32_t t = libcrux_kyber_arithmetic_montgomery_multiply_sfe_by_fer( + re[j + step], + libcrux_kyber_ntt_ZETAS_TIMES_MONTGOMERY_R[zeta_i[0U]]); + re[j + step] = re[j] - t; + re[j] = re[j] + t; + } + } + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_ntt_ntt_at_layer_3(size_t* zeta_i, + int32_t re[256U], + size_t layer, + int32_t ret[256U]) +{ + int32_t ret0[256U]; + libcrux_kyber_ntt_ntt_at_layer(zeta_i, re, layer, (size_t)3U, ret0); + memcpy(ret, ret0, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_ntt_ntt_binomially_sampled_ring_element(int32_t re[256U], + int32_t ret[256U]) +{ + size_t zeta_i = (size_t)1U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)128U }), + 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__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 j = uu____0.f0; + int32_t t = re[j + (size_t)128U] * (int32_t)-1600; + re[j + (size_t)128U] = re[j] - t; + re[j] = re[j] + t; + } + } + libcrux_kyber_ntt_ntt_at_layer_3(&zeta_i, re, (size_t)6U, re); + libcrux_kyber_ntt_ntt_at_layer_3(&zeta_i, re, (size_t)5U, re); + libcrux_kyber_ntt_ntt_at_layer_3(&zeta_i, re, (size_t)4U, re); + libcrux_kyber_ntt_ntt_at_layer_3(&zeta_i, re, (size_t)3U, re); + libcrux_kyber_ntt_ntt_at_layer_3(&zeta_i, re, (size_t)2U, re); + libcrux_kyber_ntt_ntt_at_layer_3(&zeta_i, re, (size_t)1U, re); + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t i = uu____1.f0; + int32_t uu____2 = libcrux_kyber_arithmetic_barrett_reduce(re[i]); + re[i] = uu____2; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_sampling_rejection_sampling_panic_with_diagnostic(void) +{ + KRML_HOST_EPRINTF( + "KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); +} + +typedef struct Option__Eurydice_slice_uint8_t_s +{ + core_option_Option__size_t_tags tag; + Eurydice_slice f0; +} Option__Eurydice_slice_uint8_t; + +void +libcrux_kyber_sampling_sample_from_uniform_distribution( + uint8_t randomness[840U], + int32_t ret[256U]) +{ + size_t sampled_coefficients = (size_t)0U; + int32_t out[256U]; + memcpy( + out, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + bool done = false; + core_slice_iter_Chunks iter = core_iter_traits_collect__I__into_iter( + core_slice___Slice_T___chunks( + Eurydice_array_to_slice( + (size_t)840U, randomness, uint8_t, Eurydice_slice), + (size_t)3U, + uint8_t, + core_slice_iter_Chunks), + core_slice_iter_Chunks, + core_slice_iter_Chunks); + while (true) { + Option__Eurydice_slice_uint8_t uu____0 = + core_slice_iter__core__slice__iter__Chunks__a__T__70__next( + &iter, uint8_t, Option__Eurydice_slice_uint8_t); + if (uu____0.tag == core_option_None) + break; + else { + Eurydice_slice bytes = uu____0.f0; + if (!done) { + int32_t b1 = + (int32_t)Eurydice_slice_index(bytes, (size_t)0U, uint8_t, uint8_t); + int32_t b2 = + (int32_t)Eurydice_slice_index(bytes, (size_t)1U, uint8_t, uint8_t); + int32_t b3 = + (int32_t)Eurydice_slice_index(bytes, (size_t)2U, uint8_t, uint8_t); + int32_t d1 = (b2 & (int32_t)15) << 8U | b1; + int32_t d2 = b3 << 4U | b2 >> 4U; + bool uu____1; + int32_t uu____2; + size_t uu____3; + bool uu____4; + bool uu____5; + int32_t uu____6; + bool uu____7; + size_t uu____8; + int32_t uu____9; + size_t uu____10; + bool uu____11; + size_t uu____12; + int32_t uu____13; + size_t uu____14; + size_t uu____15; + if (d1 < LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS) { + uu____1 = sampled_coefficients < + LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + if (uu____1) { + uu____2 = d1; + uu____3 = sampled_coefficients; + out[uu____3] = uu____2; + sampled_coefficients++; + uu____6 = d2; + uu____13 = LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS; + uu____5 = uu____6 < uu____13; + if (uu____5) { + uu____8 = sampled_coefficients; + uu____14 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____7 = uu____8 < uu____14; + uu____4 = uu____7; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } else { + uu____4 = false; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } + } else { + uu____6 = d2; + uu____13 = LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS; + uu____5 = uu____6 < uu____13; + if (uu____5) { + uu____8 = sampled_coefficients; + uu____14 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____7 = uu____8 < uu____14; + uu____4 = uu____7; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } else { + uu____4 = false; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } + } + } else { + uu____1 = false; + if (uu____1) { + uu____2 = d1; + uu____3 = sampled_coefficients; + out[uu____3] = uu____2; + sampled_coefficients++; + uu____6 = d2; + uu____13 = LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS; + uu____5 = uu____6 < uu____13; + if (uu____5) { + uu____8 = sampled_coefficients; + uu____14 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____7 = uu____8 < uu____14; + uu____4 = uu____7; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } else { + uu____4 = false; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } + } else { + uu____6 = d2; + uu____13 = LIBCRUX_KYBER_CONSTANTS_FIELD_MODULUS; + uu____5 = uu____6 < uu____13; + if (uu____5) { + uu____8 = sampled_coefficients; + uu____14 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____7 = uu____8 < uu____14; + uu____4 = uu____7; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } else { + uu____4 = false; + if (uu____4) { + uu____9 = d2; + uu____10 = sampled_coefficients; + out[uu____10] = uu____9; + sampled_coefficients++; + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } else { + uu____12 = sampled_coefficients; + uu____15 = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT; + uu____11 = uu____12 == uu____15; + if (uu____11) + done = true; + } + } + } + } + } + } + } + if (!done) + libcrux_kyber_sampling_rejection_sampling_panic_with_diagnostic(); + memcpy(ret, out, (size_t)256U * sizeof(int32_t)); +} + +K___int32_t_int32_t +libcrux_kyber_ntt_ntt_multiply_binomials(K___int32_t_int32_t _, + K___int32_t_int32_t _0, + int32_t zeta) +{ + int32_t a0 = _.fst; + int32_t a1 = _.snd; + int32_t b0 = _0.fst; + int32_t b1 = _0.snd; + int32_t uu____0 = a0 * b0; + int32_t uu____1 = libcrux_kyber_arithmetic_montgomery_reduce( + uu____0 + libcrux_kyber_arithmetic_montgomery_reduce(a1 * b1) * zeta); + return ((K___int32_t_int32_t){ + .fst = uu____1, + .snd = libcrux_kyber_arithmetic_montgomery_reduce(a0 * b1 + a1 * b0) }); +} + +void +libcrux_kyber_ntt_ntt_multiply(int32_t (*lhs)[256U], + int32_t (*rhs)[256U], + int32_t ret[256U]) +{ + int32_t out[256U]; + memcpy( + out, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = + LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT / (size_t)4U }), + 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__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; + K___int32_t_int32_t lit0; + lit0.fst = lhs[0U][(size_t)4U * i]; + lit0.snd = lhs[0U][(size_t)4U * i + (size_t)1U]; + K___int32_t_int32_t lit1; + lit1.fst = rhs[0U][(size_t)4U * i]; + lit1.snd = rhs[0U][(size_t)4U * i + (size_t)1U]; + K___int32_t_int32_t product = libcrux_kyber_ntt_ntt_multiply_binomials( + lit0, + lit1, + libcrux_kyber_ntt_ZETAS_TIMES_MONTGOMERY_R[(size_t)64U + i]); + out[(size_t)4U * i] = product.fst; + out[(size_t)4U * i + (size_t)1U] = product.snd; + K___int32_t_int32_t lit2; + lit2.fst = lhs[0U][(size_t)4U * i + (size_t)2U]; + lit2.snd = lhs[0U][(size_t)4U * i + (size_t)3U]; + K___int32_t_int32_t lit; + lit.fst = rhs[0U][(size_t)4U * i + (size_t)2U]; + lit.snd = rhs[0U][(size_t)4U * i + (size_t)3U]; + K___int32_t_int32_t product0 = libcrux_kyber_ntt_ntt_multiply_binomials( + lit2, + lit, + -libcrux_kyber_ntt_ZETAS_TIMES_MONTGOMERY_R[(size_t)64U + i]); + out[(size_t)4U * i + (size_t)2U] = product0.fst; + out[(size_t)4U * i + (size_t)3U] = product0.snd; + } + } + memcpy(ret, out, (size_t)256U * sizeof(int32_t)); +} + +K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_10(int32_t coefficient1, + int32_t coefficient2, + int32_t coefficient3, + int32_t coefficient4) +{ + uint8_t coef1 = (uint8_t)(coefficient1 & (int32_t)255); + uint8_t coef2 = (uint32_t)(uint8_t)(coefficient2 & (int32_t)63) << 2U | + (uint32_t)(uint8_t)(coefficient1 >> 8U & (int32_t)3); + uint8_t coef3 = (uint32_t)(uint8_t)(coefficient3 & (int32_t)15) << 4U | + (uint32_t)(uint8_t)(coefficient2 >> 6U & (int32_t)15); + uint8_t coef4 = (uint32_t)(uint8_t)(coefficient4 & (int32_t)3) << 6U | + (uint32_t)(uint8_t)(coefficient3 >> 4U & (int32_t)63); + uint8_t coef5 = (uint8_t)(coefficient4 >> 2U & (int32_t)255); + return ((K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t){ + .fst = coef1, .snd = coef2, .thd = coef3, .f3 = coef4, .f4 = coef5 }); +} + +K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_11(int32_t coefficient1, + int32_t coefficient2, + int32_t coefficient3, + int32_t coefficient4, + int32_t coefficient5, + int32_t coefficient6, + int32_t coefficient7, + int32_t coefficient8) +{ + uint8_t coef1 = (uint8_t)coefficient1; + uint8_t coef2 = (uint32_t)(uint8_t)(coefficient2 & (int32_t)31) << 3U | + (uint32_t)(uint8_t)(coefficient1 >> 8U); + uint8_t coef3 = (uint32_t)(uint8_t)(coefficient3 & (int32_t)3) << 6U | + (uint32_t)(uint8_t)(coefficient2 >> 5U); + uint8_t coef4 = (uint8_t)(coefficient3 >> 2U & (int32_t)255); + uint8_t coef5 = (uint32_t)(uint8_t)(coefficient4 & (int32_t)127) << 1U | + (uint32_t)(uint8_t)(coefficient3 >> 10U); + uint8_t coef6 = (uint32_t)(uint8_t)(coefficient5 & (int32_t)15) << 4U | + (uint32_t)(uint8_t)(coefficient4 >> 7U); + uint8_t coef7 = (uint32_t)(uint8_t)(coefficient6 & (int32_t)1) << 7U | + (uint32_t)(uint8_t)(coefficient5 >> 4U); + uint8_t coef8 = (uint8_t)(coefficient6 >> 1U & (int32_t)255); + uint8_t coef9 = (uint32_t)(uint8_t)(coefficient7 & (int32_t)63) << 2U | + (uint32_t)(uint8_t)(coefficient6 >> 9U); + uint8_t coef10 = (uint32_t)(uint8_t)(coefficient8 & (int32_t)7) << 5U | + (uint32_t)(uint8_t)(coefficient7 >> 6U); + uint8_t coef11 = (uint8_t)(coefficient8 >> 3U); + return (( + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t){ + .fst = coef1, + .snd = coef2, + .thd = coef3, + .f3 = coef4, + .f4 = coef5, + .f5 = coef6, + .f6 = coef7, + .f7 = coef8, + .f8 = coef9, + .f9 = coef10, + .f10 = coef11 }); +} + +void +libcrux_kyber_ntt_invert_ntt_at_layer(size_t* zeta_i, + int32_t re[256U], + size_t layer, + int32_t ret[256U]) +{ + size_t step = (size_t)1U << (uint32_t)layer; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)128U >> (uint32_t)layer }), + 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__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 round = uu____0.f0; + zeta_i[0U] = zeta_i[0U] - (size_t)1U; + size_t offset = round * step * (size_t)2U; + core_ops_range_Range__size_t iter0 = + core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = offset, + .end = offset + step }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t j = uu____1.f0; + int32_t a_minus_b = re[j + step] - re[j]; + re[j] = re[j] + re[j + step]; + int32_t uu____2 = libcrux_kyber_arithmetic_montgomery_reduce( + a_minus_b * libcrux_kyber_ntt_ZETAS_TIMES_MONTGOMERY_R[zeta_i[0U]]); + re[j + step] = uu____2; + } + } + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_serialize_deserialize_then_decompress_message( + uint8_t serialized[32U], + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy( + re, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)32U, serialized, uint8_t, Eurydice_slice), + uint8_t, + size_t); + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter( + lit, 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__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) + break; + else { + size_t i = uu____0.f0; + uint8_t byte = serialized[i]; + core_ops_range_Range__size_t iter = + core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)8U }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t j = uu____1.f0; + int32_t coefficient_compressed = + (int32_t)((uint32_t)byte >> (uint32_t)j & 1U); + int32_t uu____2 = + libcrux_kyber_compress_decompress_message_coefficient( + coefficient_compressed); + re[(size_t)8U * i + j] = uu____2; + } + } + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t +libcrux_kyber_serialize_compress_coefficients_5(uint8_t coefficient2, + uint8_t coefficient1, + uint8_t coefficient4, + uint8_t coefficient3, + uint8_t coefficient5, + uint8_t coefficient7, + uint8_t coefficient6, + uint8_t coefficient8) +{ + uint8_t coef1 = ((uint32_t)coefficient2 & 7U) << 5U | (uint32_t)coefficient1; + uint8_t coef2 = + (((uint32_t)coefficient4 & 1U) << 7U | (uint32_t)coefficient3 << 2U) | + (uint32_t)coefficient2 >> 3U; + uint8_t coef3 = + ((uint32_t)coefficient5 & 15U) << 4U | (uint32_t)coefficient4 >> 1U; + uint8_t coef4 = + (((uint32_t)coefficient7 & 3U) << 6U | (uint32_t)coefficient6 << 1U) | + (uint32_t)coefficient5 >> 4U; + uint8_t coef5 = (uint32_t)coefficient8 << 3U | (uint32_t)coefficient7 >> 2U; + return ((K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t){ + .fst = coef1, .snd = coef2, .thd = coef3, .f3 = coef4, .f4 = coef5 }); +} + +K___int32_t_int32_t_int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_10(int32_t byte2, + int32_t byte1, + int32_t byte3, + int32_t byte4, + int32_t byte5) +{ + int32_t coefficient1 = (byte2 & (int32_t)3) << 8U | (byte1 & (int32_t)255); + int32_t coefficient2 = (byte3 & (int32_t)15) << 6U | byte2 >> 2U; + int32_t coefficient3 = (byte4 & (int32_t)63) << 4U | byte3 >> 4U; + int32_t coefficient4 = byte5 << 2U | byte4 >> 6U; + return ((K___int32_t_int32_t_int32_t_int32_t){ .fst = coefficient1, + .snd = coefficient2, + .thd = coefficient3, + .f3 = coefficient4 }); +} + +void +libcrux_kyber_serialize_deserialize_then_decompress_10( + Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy( + re, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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)5U }), + 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__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)5U, + .end = i * (size_t)5U + (size_t)5U }), + 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); + int32_t byte4 = + (int32_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t); + int32_t byte5 = + (int32_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t); + K___int32_t_int32_t_int32_t_int32_t uu____1 = + libcrux_kyber_serialize_decompress_coefficients_10( + byte2, byte1, byte3, byte4, byte5); + int32_t coefficient1 = uu____1.fst; + int32_t coefficient2 = uu____1.snd; + int32_t coefficient3 = uu____1.thd; + int32_t coefficient4 = uu____1.f3; + int32_t uu____2 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(10U, + coefficient1); + re[(size_t)4U * i] = uu____2; + int32_t uu____3 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(10U, + coefficient2); + re[(size_t)4U * i + (size_t)1U] = uu____3; + int32_t uu____4 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(10U, + coefficient3); + re[(size_t)4U * i + (size_t)2U] = uu____4; + int32_t uu____5 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(10U, + coefficient4); + re[(size_t)4U * i + (size_t)3U] = uu____5; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_11(int32_t byte2, + int32_t byte1, + int32_t byte3, + int32_t byte5, + int32_t byte4, + int32_t byte6, + int32_t byte7, + int32_t byte9, + int32_t byte8, + int32_t byte10, + int32_t byte11) +{ + int32_t coefficient1 = (byte2 & (int32_t)7) << 8U | byte1; + int32_t coefficient2 = (byte3 & (int32_t)63) << 5U | byte2 >> 3U; + int32_t coefficient3 = + ((byte5 & (int32_t)1) << 10U | byte4 << 2U) | byte3 >> 6U; + int32_t coefficient4 = (byte6 & (int32_t)15) << 7U | byte5 >> 1U; + int32_t coefficient5 = (byte7 & (int32_t)127) << 4U | byte6 >> 4U; + int32_t coefficient6 = + ((byte9 & (int32_t)3) << 9U | byte8 << 1U) | byte7 >> 7U; + int32_t coefficient7 = (byte10 & (int32_t)31) << 6U | byte9 >> 2U; + int32_t coefficient8 = byte11 << 3U | byte10 >> 5U; + return ((K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t){ + .fst = coefficient1, + .snd = coefficient2, + .thd = coefficient3, + .f3 = coefficient4, + .f4 = coefficient5, + .f5 = coefficient6, + .f6 = coefficient7, + .f7 = coefficient8 }); +} + +void +libcrux_kyber_serialize_deserialize_then_decompress_11( + Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy( + re, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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)11U }), + 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__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)11U, .end = i * (size_t)11U + (size_t)11U }), + 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); + int32_t byte4 = + (int32_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t); + int32_t byte5 = + (int32_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t); + int32_t byte6 = + (int32_t)Eurydice_slice_index(bytes, (size_t)5U, uint8_t, uint8_t); + int32_t byte7 = + (int32_t)Eurydice_slice_index(bytes, (size_t)6U, uint8_t, uint8_t); + int32_t byte8 = + (int32_t)Eurydice_slice_index(bytes, (size_t)7U, uint8_t, uint8_t); + int32_t byte9 = + (int32_t)Eurydice_slice_index(bytes, (size_t)8U, uint8_t, uint8_t); + int32_t byte10 = + (int32_t)Eurydice_slice_index(bytes, (size_t)9U, uint8_t, uint8_t); + int32_t byte11 = + (int32_t)Eurydice_slice_index(bytes, (size_t)10U, uint8_t, uint8_t); + K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t + uu____1 = libcrux_kyber_serialize_decompress_coefficients_11(byte2, + byte1, + byte3, + byte5, + byte4, + byte6, + byte7, + byte9, + byte8, + byte10, + byte11); + int32_t coefficient1 = uu____1.fst; + int32_t coefficient2 = uu____1.snd; + int32_t coefficient3 = uu____1.thd; + int32_t coefficient4 = uu____1.f3; + int32_t coefficient5 = uu____1.f4; + int32_t coefficient6 = uu____1.f5; + int32_t coefficient7 = uu____1.f6; + int32_t coefficient8 = uu____1.f7; + int32_t uu____2 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient1); + re[(size_t)8U * i] = uu____2; + int32_t uu____3 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient2); + re[(size_t)8U * i + (size_t)1U] = uu____3; + int32_t uu____4 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient3); + re[(size_t)8U * i + (size_t)2U] = uu____4; + int32_t uu____5 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient4); + re[(size_t)8U * i + (size_t)3U] = uu____5; + int32_t uu____6 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient5); + re[(size_t)8U * i + (size_t)4U] = uu____6; + int32_t uu____7 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient6); + re[(size_t)8U * i + (size_t)5U] = uu____7; + int32_t uu____8 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient7); + re[(size_t)8U * i + (size_t)6U] = uu____8; + int32_t uu____9 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(11U, + coefficient8); + re[(size_t)8U * i + (size_t)7U] = uu____9; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_ntt_ntt_at_layer_3328(size_t* zeta_i, + int32_t re[256U], + size_t layer, + int32_t ret[256U]) +{ + int32_t ret0[256U]; + libcrux_kyber_ntt_ntt_at_layer(zeta_i, re, layer, (size_t)3328U, ret0); + memcpy(ret, ret0, (size_t)256U * sizeof(int32_t)); +} + +K___int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_4(uint8_t* byte) +{ + int32_t coefficient1 = (int32_t)Eurydice_bitand_pv_u8(byte, 15U); + int32_t coefficient2 = + (int32_t)((uint32_t)Eurydice_shr_pv_u8(byte, (int32_t)4) & 15U); + return ((K___int32_t_int32_t){ .fst = coefficient1, .snd = coefficient2 }); +} + +void +libcrux_kyber_serialize_deserialize_then_decompress_4(Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy( + re, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(serialized, uint8_t, size_t) }), + 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__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; + uint8_t* byte = &Eurydice_slice_index(serialized, i, uint8_t, uint8_t); + K___int32_t_int32_t uu____1 = + libcrux_kyber_serialize_decompress_coefficients_4(byte); + int32_t coefficient1 = uu____1.fst; + int32_t coefficient2 = uu____1.snd; + int32_t uu____2 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(4U, + coefficient1); + re[(size_t)2U * i] = uu____2; + int32_t uu____3 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(4U, + coefficient2); + re[(size_t)2U * i + (size_t)1U] = uu____3; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t +libcrux_kyber_serialize_decompress_coefficients_5(int32_t byte1, + int32_t byte2, + int32_t byte3, + int32_t byte4, + int32_t byte5) +{ + int32_t coefficient1 = byte1 & (int32_t)31; + int32_t coefficient2 = (byte2 & (int32_t)3) << 3U | byte1 >> 5U; + int32_t coefficient3 = byte2 >> 2U & (int32_t)31; + int32_t coefficient4 = (byte3 & (int32_t)15) << 1U | byte2 >> 7U; + int32_t coefficient5 = (byte4 & (int32_t)1) << 4U | byte3 >> 4U; + int32_t coefficient6 = byte4 >> 1U & (int32_t)31; + int32_t coefficient7 = (byte5 & (int32_t)7) << 2U | byte4 >> 6U; + int32_t coefficient8 = byte5 >> 3U; + return ((K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t){ + .fst = coefficient1, + .snd = coefficient2, + .thd = coefficient3, + .f3 = coefficient4, + .f4 = coefficient5, + .f5 = coefficient6, + .f6 = coefficient7, + .f7 = coefficient8 }); +} + +void +libcrux_kyber_serialize_deserialize_then_decompress_5(Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t re[256U]; + memcpy( + re, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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)5U }), + 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__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)5U, + .end = i * (size_t)5U + (size_t)5U }), + 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); + int32_t byte4 = + (int32_t)Eurydice_slice_index(bytes, (size_t)3U, uint8_t, uint8_t); + int32_t byte5 = + (int32_t)Eurydice_slice_index(bytes, (size_t)4U, uint8_t, uint8_t); + K___int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t_int32_t + uu____1 = libcrux_kyber_serialize_decompress_coefficients_5( + byte1, byte2, byte3, byte4, byte5); + int32_t coefficient1 = uu____1.fst; + int32_t coefficient2 = uu____1.snd; + int32_t coefficient3 = uu____1.thd; + int32_t coefficient4 = uu____1.f3; + int32_t coefficient5 = uu____1.f4; + int32_t coefficient6 = uu____1.f5; + int32_t coefficient7 = uu____1.f6; + int32_t coefficient8 = uu____1.f7; + int32_t uu____2 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient1); + re[(size_t)8U * i] = uu____2; + int32_t uu____3 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient2); + re[(size_t)8U * i + (size_t)1U] = uu____3; + int32_t uu____4 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient3); + re[(size_t)8U * i + (size_t)2U] = uu____4; + int32_t uu____5 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient4); + re[(size_t)8U * i + (size_t)3U] = uu____5; + int32_t uu____6 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient5); + re[(size_t)8U * i + (size_t)4U] = uu____6; + int32_t uu____7 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient6); + re[(size_t)8U * i + (size_t)5U] = uu____7; + int32_t uu____8 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient7); + re[(size_t)8U * i + (size_t)6U] = uu____8; + int32_t uu____9 = + libcrux_kyber_compress_decompress_ciphertext_coefficient(5U, + coefficient8); + re[(size_t)8U * i + (size_t)7U] = uu____9; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_serialize_compress_then_serialize_message(int32_t re[256U], + uint8_t ret[32U]) +{ + uint8_t serialized[32U]; + for (size_t i = (size_t)0U; i < (size_t)32U; i++) + serialized[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = + core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)256U, re, int32_t, Eurydice_slice), + int32_t, + size_t) / + (size_t)8U; + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter( + lit, 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__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) + break; + else { + size_t i = uu____0.f0; + Eurydice_slice coefficients = Eurydice_array_to_subslice( + (size_t)256U, + re, + ((core_ops_range_Range__size_t){ .start = i * (size_t)8U, + .end = i * (size_t)8U + (size_t)8U }), + int32_t, + core_ops_range_Range__size_t, + Eurydice_slice); + core_ops_range_Range__size_t iter = + core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(coefficients, int32_t, size_t) }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t j = uu____1.f0; + int32_t* coefficient = + &Eurydice_slice_index(coefficients, j, int32_t, int32_t); + uint16_t coefficient0 = + libcrux_kyber_arithmetic_to_unsigned_representative( + coefficient[0U]); + uint8_t coefficient_compressed = + libcrux_kyber_compress_compress_message_coefficient(coefficient0); + size_t uu____2 = i; + serialized[uu____2] = (uint32_t)serialized[uu____2] | + (uint32_t)coefficient_compressed << (uint32_t)j; + } + } + } + } + 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)); +} + +void +libcrux_kyber_hash_functions_XOFx4___3size_t(uint8_t input[3U][34U], + uint8_t ret[3U][840U]) +{ + uint8_t out[3U][840U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) { + out[i][0U] = 0U; + out[i][1U] = 0U; + out[i][2U] = 0U; + out[i][3U] = 0U; + out[i][4U] = 0U; + out[i][5U] = 0U; + out[i][6U] = 0U; + out[i][7U] = 0U; + out[i][8U] = 0U; + out[i][9U] = 0U; + out[i][10U] = 0U; + out[i][11U] = 0U; + out[i][12U] = 0U; + out[i][13U] = 0U; + out[i][14U] = 0U; + out[i][15U] = 0U; + out[i][16U] = 0U; + out[i][17U] = 0U; + out[i][18U] = 0U; + out[i][19U] = 0U; + out[i][20U] = 0U; + out[i][21U] = 0U; + out[i][22U] = 0U; + out[i][23U] = 0U; + out[i][24U] = 0U; + out[i][25U] = 0U; + out[i][26U] = 0U; + out[i][27U] = 0U; + out[i][28U] = 0U; + out[i][29U] = 0U; + out[i][30U] = 0U; + out[i][31U] = 0U; + out[i][32U] = 0U; + out[i][33U] = 0U; + out[i][34U] = 0U; + out[i][35U] = 0U; + out[i][36U] = 0U; + out[i][37U] = 0U; + out[i][38U] = 0U; + out[i][39U] = 0U; + out[i][40U] = 0U; + out[i][41U] = 0U; + out[i][42U] = 0U; + out[i][43U] = 0U; + out[i][44U] = 0U; + out[i][45U] = 0U; + out[i][46U] = 0U; + out[i][47U] = 0U; + out[i][48U] = 0U; + out[i][49U] = 0U; + out[i][50U] = 0U; + out[i][51U] = 0U; + out[i][52U] = 0U; + out[i][53U] = 0U; + out[i][54U] = 0U; + out[i][55U] = 0U; + out[i][56U] = 0U; + out[i][57U] = 0U; + out[i][58U] = 0U; + out[i][59U] = 0U; + out[i][60U] = 0U; + out[i][61U] = 0U; + out[i][62U] = 0U; + out[i][63U] = 0U; + out[i][64U] = 0U; + out[i][65U] = 0U; + out[i][66U] = 0U; + out[i][67U] = 0U; + out[i][68U] = 0U; + out[i][69U] = 0U; + out[i][70U] = 0U; + out[i][71U] = 0U; + out[i][72U] = 0U; + out[i][73U] = 0U; + out[i][74U] = 0U; + out[i][75U] = 0U; + out[i][76U] = 0U; + out[i][77U] = 0U; + out[i][78U] = 0U; + out[i][79U] = 0U; + out[i][80U] = 0U; + out[i][81U] = 0U; + out[i][82U] = 0U; + out[i][83U] = 0U; + out[i][84U] = 0U; + out[i][85U] = 0U; + out[i][86U] = 0U; + out[i][87U] = 0U; + out[i][88U] = 0U; + out[i][89U] = 0U; + out[i][90U] = 0U; + out[i][91U] = 0U; + out[i][92U] = 0U; + out[i][93U] = 0U; + out[i][94U] = 0U; + out[i][95U] = 0U; + out[i][96U] = 0U; + out[i][97U] = 0U; + out[i][98U] = 0U; + out[i][99U] = 0U; + out[i][100U] = 0U; + out[i][101U] = 0U; + out[i][102U] = 0U; + out[i][103U] = 0U; + out[i][104U] = 0U; + out[i][105U] = 0U; + out[i][106U] = 0U; + out[i][107U] = 0U; + out[i][108U] = 0U; + out[i][109U] = 0U; + out[i][110U] = 0U; + out[i][111U] = 0U; + out[i][112U] = 0U; + out[i][113U] = 0U; + out[i][114U] = 0U; + out[i][115U] = 0U; + out[i][116U] = 0U; + out[i][117U] = 0U; + out[i][118U] = 0U; + out[i][119U] = 0U; + out[i][120U] = 0U; + out[i][121U] = 0U; + out[i][122U] = 0U; + out[i][123U] = 0U; + out[i][124U] = 0U; + out[i][125U] = 0U; + out[i][126U] = 0U; + out[i][127U] = 0U; + out[i][128U] = 0U; + out[i][129U] = 0U; + out[i][130U] = 0U; + out[i][131U] = 0U; + out[i][132U] = 0U; + out[i][133U] = 0U; + out[i][134U] = 0U; + out[i][135U] = 0U; + out[i][136U] = 0U; + out[i][137U] = 0U; + out[i][138U] = 0U; + out[i][139U] = 0U; + out[i][140U] = 0U; + out[i][141U] = 0U; + out[i][142U] = 0U; + out[i][143U] = 0U; + out[i][144U] = 0U; + out[i][145U] = 0U; + out[i][146U] = 0U; + out[i][147U] = 0U; + out[i][148U] = 0U; + out[i][149U] = 0U; + out[i][150U] = 0U; + out[i][151U] = 0U; + out[i][152U] = 0U; + out[i][153U] = 0U; + out[i][154U] = 0U; + out[i][155U] = 0U; + out[i][156U] = 0U; + out[i][157U] = 0U; + out[i][158U] = 0U; + out[i][159U] = 0U; + out[i][160U] = 0U; + out[i][161U] = 0U; + out[i][162U] = 0U; + out[i][163U] = 0U; + out[i][164U] = 0U; + out[i][165U] = 0U; + out[i][166U] = 0U; + out[i][167U] = 0U; + out[i][168U] = 0U; + out[i][169U] = 0U; + out[i][170U] = 0U; + out[i][171U] = 0U; + out[i][172U] = 0U; + out[i][173U] = 0U; + out[i][174U] = 0U; + out[i][175U] = 0U; + out[i][176U] = 0U; + out[i][177U] = 0U; + out[i][178U] = 0U; + out[i][179U] = 0U; + out[i][180U] = 0U; + out[i][181U] = 0U; + out[i][182U] = 0U; + out[i][183U] = 0U; + out[i][184U] = 0U; + out[i][185U] = 0U; + out[i][186U] = 0U; + out[i][187U] = 0U; + out[i][188U] = 0U; + out[i][189U] = 0U; + out[i][190U] = 0U; + out[i][191U] = 0U; + out[i][192U] = 0U; + out[i][193U] = 0U; + out[i][194U] = 0U; + out[i][195U] = 0U; + out[i][196U] = 0U; + out[i][197U] = 0U; + out[i][198U] = 0U; + out[i][199U] = 0U; + out[i][200U] = 0U; + out[i][201U] = 0U; + out[i][202U] = 0U; + out[i][203U] = 0U; + out[i][204U] = 0U; + out[i][205U] = 0U; + out[i][206U] = 0U; + out[i][207U] = 0U; + out[i][208U] = 0U; + out[i][209U] = 0U; + out[i][210U] = 0U; + out[i][211U] = 0U; + out[i][212U] = 0U; + out[i][213U] = 0U; + out[i][214U] = 0U; + out[i][215U] = 0U; + out[i][216U] = 0U; + out[i][217U] = 0U; + out[i][218U] = 0U; + out[i][219U] = 0U; + out[i][220U] = 0U; + out[i][221U] = 0U; + out[i][222U] = 0U; + out[i][223U] = 0U; + out[i][224U] = 0U; + out[i][225U] = 0U; + out[i][226U] = 0U; + out[i][227U] = 0U; + out[i][228U] = 0U; + out[i][229U] = 0U; + out[i][230U] = 0U; + out[i][231U] = 0U; + out[i][232U] = 0U; + out[i][233U] = 0U; + out[i][234U] = 0U; + out[i][235U] = 0U; + out[i][236U] = 0U; + out[i][237U] = 0U; + out[i][238U] = 0U; + out[i][239U] = 0U; + out[i][240U] = 0U; + out[i][241U] = 0U; + out[i][242U] = 0U; + out[i][243U] = 0U; + out[i][244U] = 0U; + out[i][245U] = 0U; + out[i][246U] = 0U; + out[i][247U] = 0U; + out[i][248U] = 0U; + out[i][249U] = 0U; + out[i][250U] = 0U; + out[i][251U] = 0U; + out[i][252U] = 0U; + out[i][253U] = 0U; + out[i][254U] = 0U; + out[i][255U] = 0U; + out[i][256U] = 0U; + out[i][257U] = 0U; + out[i][258U] = 0U; + out[i][259U] = 0U; + out[i][260U] = 0U; + out[i][261U] = 0U; + out[i][262U] = 0U; + out[i][263U] = 0U; + out[i][264U] = 0U; + out[i][265U] = 0U; + out[i][266U] = 0U; + out[i][267U] = 0U; + out[i][268U] = 0U; + out[i][269U] = 0U; + out[i][270U] = 0U; + out[i][271U] = 0U; + out[i][272U] = 0U; + out[i][273U] = 0U; + out[i][274U] = 0U; + out[i][275U] = 0U; + out[i][276U] = 0U; + out[i][277U] = 0U; + out[i][278U] = 0U; + out[i][279U] = 0U; + out[i][280U] = 0U; + out[i][281U] = 0U; + out[i][282U] = 0U; + out[i][283U] = 0U; + out[i][284U] = 0U; + out[i][285U] = 0U; + out[i][286U] = 0U; + out[i][287U] = 0U; + out[i][288U] = 0U; + out[i][289U] = 0U; + out[i][290U] = 0U; + out[i][291U] = 0U; + out[i][292U] = 0U; + out[i][293U] = 0U; + out[i][294U] = 0U; + out[i][295U] = 0U; + out[i][296U] = 0U; + out[i][297U] = 0U; + out[i][298U] = 0U; + out[i][299U] = 0U; + out[i][300U] = 0U; + out[i][301U] = 0U; + out[i][302U] = 0U; + out[i][303U] = 0U; + out[i][304U] = 0U; + out[i][305U] = 0U; + out[i][306U] = 0U; + out[i][307U] = 0U; + out[i][308U] = 0U; + out[i][309U] = 0U; + out[i][310U] = 0U; + out[i][311U] = 0U; + out[i][312U] = 0U; + out[i][313U] = 0U; + out[i][314U] = 0U; + out[i][315U] = 0U; + out[i][316U] = 0U; + out[i][317U] = 0U; + out[i][318U] = 0U; + out[i][319U] = 0U; + out[i][320U] = 0U; + out[i][321U] = 0U; + out[i][322U] = 0U; + out[i][323U] = 0U; + out[i][324U] = 0U; + out[i][325U] = 0U; + out[i][326U] = 0U; + out[i][327U] = 0U; + out[i][328U] = 0U; + out[i][329U] = 0U; + out[i][330U] = 0U; + out[i][331U] = 0U; + out[i][332U] = 0U; + out[i][333U] = 0U; + out[i][334U] = 0U; + out[i][335U] = 0U; + out[i][336U] = 0U; + out[i][337U] = 0U; + out[i][338U] = 0U; + out[i][339U] = 0U; + out[i][340U] = 0U; + out[i][341U] = 0U; + out[i][342U] = 0U; + out[i][343U] = 0U; + out[i][344U] = 0U; + out[i][345U] = 0U; + out[i][346U] = 0U; + out[i][347U] = 0U; + out[i][348U] = 0U; + out[i][349U] = 0U; + out[i][350U] = 0U; + out[i][351U] = 0U; + out[i][352U] = 0U; + out[i][353U] = 0U; + out[i][354U] = 0U; + out[i][355U] = 0U; + out[i][356U] = 0U; + out[i][357U] = 0U; + out[i][358U] = 0U; + out[i][359U] = 0U; + out[i][360U] = 0U; + out[i][361U] = 0U; + out[i][362U] = 0U; + out[i][363U] = 0U; + out[i][364U] = 0U; + out[i][365U] = 0U; + out[i][366U] = 0U; + out[i][367U] = 0U; + out[i][368U] = 0U; + out[i][369U] = 0U; + out[i][370U] = 0U; + out[i][371U] = 0U; + out[i][372U] = 0U; + out[i][373U] = 0U; + out[i][374U] = 0U; + out[i][375U] = 0U; + out[i][376U] = 0U; + out[i][377U] = 0U; + out[i][378U] = 0U; + out[i][379U] = 0U; + out[i][380U] = 0U; + out[i][381U] = 0U; + out[i][382U] = 0U; + out[i][383U] = 0U; + out[i][384U] = 0U; + out[i][385U] = 0U; + out[i][386U] = 0U; + out[i][387U] = 0U; + out[i][388U] = 0U; + out[i][389U] = 0U; + out[i][390U] = 0U; + out[i][391U] = 0U; + out[i][392U] = 0U; + out[i][393U] = 0U; + out[i][394U] = 0U; + out[i][395U] = 0U; + out[i][396U] = 0U; + out[i][397U] = 0U; + out[i][398U] = 0U; + out[i][399U] = 0U; + out[i][400U] = 0U; + out[i][401U] = 0U; + out[i][402U] = 0U; + out[i][403U] = 0U; + out[i][404U] = 0U; + out[i][405U] = 0U; + out[i][406U] = 0U; + out[i][407U] = 0U; + out[i][408U] = 0U; + out[i][409U] = 0U; + out[i][410U] = 0U; + out[i][411U] = 0U; + out[i][412U] = 0U; + out[i][413U] = 0U; + out[i][414U] = 0U; + out[i][415U] = 0U; + out[i][416U] = 0U; + out[i][417U] = 0U; + out[i][418U] = 0U; + out[i][419U] = 0U; + out[i][420U] = 0U; + out[i][421U] = 0U; + out[i][422U] = 0U; + out[i][423U] = 0U; + out[i][424U] = 0U; + out[i][425U] = 0U; + out[i][426U] = 0U; + out[i][427U] = 0U; + out[i][428U] = 0U; + out[i][429U] = 0U; + out[i][430U] = 0U; + out[i][431U] = 0U; + out[i][432U] = 0U; + out[i][433U] = 0U; + out[i][434U] = 0U; + out[i][435U] = 0U; + out[i][436U] = 0U; + out[i][437U] = 0U; + out[i][438U] = 0U; + out[i][439U] = 0U; + out[i][440U] = 0U; + out[i][441U] = 0U; + out[i][442U] = 0U; + out[i][443U] = 0U; + out[i][444U] = 0U; + out[i][445U] = 0U; + out[i][446U] = 0U; + out[i][447U] = 0U; + out[i][448U] = 0U; + out[i][449U] = 0U; + out[i][450U] = 0U; + out[i][451U] = 0U; + out[i][452U] = 0U; + out[i][453U] = 0U; + out[i][454U] = 0U; + out[i][455U] = 0U; + out[i][456U] = 0U; + out[i][457U] = 0U; + out[i][458U] = 0U; + out[i][459U] = 0U; + out[i][460U] = 0U; + out[i][461U] = 0U; + out[i][462U] = 0U; + out[i][463U] = 0U; + out[i][464U] = 0U; + out[i][465U] = 0U; + out[i][466U] = 0U; + out[i][467U] = 0U; + out[i][468U] = 0U; + out[i][469U] = 0U; + out[i][470U] = 0U; + out[i][471U] = 0U; + out[i][472U] = 0U; + out[i][473U] = 0U; + out[i][474U] = 0U; + out[i][475U] = 0U; + out[i][476U] = 0U; + out[i][477U] = 0U; + out[i][478U] = 0U; + out[i][479U] = 0U; + out[i][480U] = 0U; + out[i][481U] = 0U; + out[i][482U] = 0U; + out[i][483U] = 0U; + out[i][484U] = 0U; + out[i][485U] = 0U; + out[i][486U] = 0U; + out[i][487U] = 0U; + out[i][488U] = 0U; + out[i][489U] = 0U; + out[i][490U] = 0U; + out[i][491U] = 0U; + out[i][492U] = 0U; + out[i][493U] = 0U; + out[i][494U] = 0U; + out[i][495U] = 0U; + out[i][496U] = 0U; + out[i][497U] = 0U; + out[i][498U] = 0U; + out[i][499U] = 0U; + out[i][500U] = 0U; + out[i][501U] = 0U; + out[i][502U] = 0U; + out[i][503U] = 0U; + out[i][504U] = 0U; + out[i][505U] = 0U; + out[i][506U] = 0U; + out[i][507U] = 0U; + out[i][508U] = 0U; + out[i][509U] = 0U; + out[i][510U] = 0U; + out[i][511U] = 0U; + out[i][512U] = 0U; + out[i][513U] = 0U; + out[i][514U] = 0U; + out[i][515U] = 0U; + out[i][516U] = 0U; + out[i][517U] = 0U; + out[i][518U] = 0U; + out[i][519U] = 0U; + out[i][520U] = 0U; + out[i][521U] = 0U; + out[i][522U] = 0U; + out[i][523U] = 0U; + out[i][524U] = 0U; + out[i][525U] = 0U; + out[i][526U] = 0U; + out[i][527U] = 0U; + out[i][528U] = 0U; + out[i][529U] = 0U; + out[i][530U] = 0U; + out[i][531U] = 0U; + out[i][532U] = 0U; + out[i][533U] = 0U; + out[i][534U] = 0U; + out[i][535U] = 0U; + out[i][536U] = 0U; + out[i][537U] = 0U; + out[i][538U] = 0U; + out[i][539U] = 0U; + out[i][540U] = 0U; + out[i][541U] = 0U; + out[i][542U] = 0U; + out[i][543U] = 0U; + out[i][544U] = 0U; + out[i][545U] = 0U; + out[i][546U] = 0U; + out[i][547U] = 0U; + out[i][548U] = 0U; + out[i][549U] = 0U; + out[i][550U] = 0U; + out[i][551U] = 0U; + out[i][552U] = 0U; + out[i][553U] = 0U; + out[i][554U] = 0U; + out[i][555U] = 0U; + out[i][556U] = 0U; + out[i][557U] = 0U; + out[i][558U] = 0U; + out[i][559U] = 0U; + out[i][560U] = 0U; + out[i][561U] = 0U; + out[i][562U] = 0U; + out[i][563U] = 0U; + out[i][564U] = 0U; + out[i][565U] = 0U; + out[i][566U] = 0U; + out[i][567U] = 0U; + out[i][568U] = 0U; + out[i][569U] = 0U; + out[i][570U] = 0U; + out[i][571U] = 0U; + out[i][572U] = 0U; + out[i][573U] = 0U; + out[i][574U] = 0U; + out[i][575U] = 0U; + out[i][576U] = 0U; + out[i][577U] = 0U; + out[i][578U] = 0U; + out[i][579U] = 0U; + out[i][580U] = 0U; + out[i][581U] = 0U; + out[i][582U] = 0U; + out[i][583U] = 0U; + out[i][584U] = 0U; + out[i][585U] = 0U; + out[i][586U] = 0U; + out[i][587U] = 0U; + out[i][588U] = 0U; + out[i][589U] = 0U; + out[i][590U] = 0U; + out[i][591U] = 0U; + out[i][592U] = 0U; + out[i][593U] = 0U; + out[i][594U] = 0U; + out[i][595U] = 0U; + out[i][596U] = 0U; + out[i][597U] = 0U; + out[i][598U] = 0U; + out[i][599U] = 0U; + out[i][600U] = 0U; + out[i][601U] = 0U; + out[i][602U] = 0U; + out[i][603U] = 0U; + out[i][604U] = 0U; + out[i][605U] = 0U; + out[i][606U] = 0U; + out[i][607U] = 0U; + out[i][608U] = 0U; + out[i][609U] = 0U; + out[i][610U] = 0U; + out[i][611U] = 0U; + out[i][612U] = 0U; + out[i][613U] = 0U; + out[i][614U] = 0U; + out[i][615U] = 0U; + out[i][616U] = 0U; + out[i][617U] = 0U; + out[i][618U] = 0U; + out[i][619U] = 0U; + out[i][620U] = 0U; + out[i][621U] = 0U; + out[i][622U] = 0U; + out[i][623U] = 0U; + out[i][624U] = 0U; + out[i][625U] = 0U; + out[i][626U] = 0U; + out[i][627U] = 0U; + out[i][628U] = 0U; + out[i][629U] = 0U; + out[i][630U] = 0U; + out[i][631U] = 0U; + out[i][632U] = 0U; + out[i][633U] = 0U; + out[i][634U] = 0U; + out[i][635U] = 0U; + out[i][636U] = 0U; + out[i][637U] = 0U; + out[i][638U] = 0U; + out[i][639U] = 0U; + out[i][640U] = 0U; + out[i][641U] = 0U; + out[i][642U] = 0U; + out[i][643U] = 0U; + out[i][644U] = 0U; + out[i][645U] = 0U; + out[i][646U] = 0U; + out[i][647U] = 0U; + out[i][648U] = 0U; + out[i][649U] = 0U; + out[i][650U] = 0U; + out[i][651U] = 0U; + out[i][652U] = 0U; + out[i][653U] = 0U; + out[i][654U] = 0U; + out[i][655U] = 0U; + out[i][656U] = 0U; + out[i][657U] = 0U; + out[i][658U] = 0U; + out[i][659U] = 0U; + out[i][660U] = 0U; + out[i][661U] = 0U; + out[i][662U] = 0U; + out[i][663U] = 0U; + out[i][664U] = 0U; + out[i][665U] = 0U; + out[i][666U] = 0U; + out[i][667U] = 0U; + out[i][668U] = 0U; + out[i][669U] = 0U; + out[i][670U] = 0U; + out[i][671U] = 0U; + out[i][672U] = 0U; + out[i][673U] = 0U; + out[i][674U] = 0U; + out[i][675U] = 0U; + out[i][676U] = 0U; + out[i][677U] = 0U; + out[i][678U] = 0U; + out[i][679U] = 0U; + out[i][680U] = 0U; + out[i][681U] = 0U; + out[i][682U] = 0U; + out[i][683U] = 0U; + out[i][684U] = 0U; + out[i][685U] = 0U; + out[i][686U] = 0U; + out[i][687U] = 0U; + out[i][688U] = 0U; + out[i][689U] = 0U; + out[i][690U] = 0U; + out[i][691U] = 0U; + out[i][692U] = 0U; + out[i][693U] = 0U; + out[i][694U] = 0U; + out[i][695U] = 0U; + out[i][696U] = 0U; + out[i][697U] = 0U; + out[i][698U] = 0U; + out[i][699U] = 0U; + out[i][700U] = 0U; + out[i][701U] = 0U; + out[i][702U] = 0U; + out[i][703U] = 0U; + out[i][704U] = 0U; + out[i][705U] = 0U; + out[i][706U] = 0U; + out[i][707U] = 0U; + out[i][708U] = 0U; + out[i][709U] = 0U; + out[i][710U] = 0U; + out[i][711U] = 0U; + out[i][712U] = 0U; + out[i][713U] = 0U; + out[i][714U] = 0U; + out[i][715U] = 0U; + out[i][716U] = 0U; + out[i][717U] = 0U; + out[i][718U] = 0U; + out[i][719U] = 0U; + out[i][720U] = 0U; + out[i][721U] = 0U; + out[i][722U] = 0U; + out[i][723U] = 0U; + out[i][724U] = 0U; + out[i][725U] = 0U; + out[i][726U] = 0U; + out[i][727U] = 0U; + out[i][728U] = 0U; + out[i][729U] = 0U; + out[i][730U] = 0U; + out[i][731U] = 0U; + out[i][732U] = 0U; + out[i][733U] = 0U; + out[i][734U] = 0U; + out[i][735U] = 0U; + out[i][736U] = 0U; + out[i][737U] = 0U; + out[i][738U] = 0U; + out[i][739U] = 0U; + out[i][740U] = 0U; + out[i][741U] = 0U; + out[i][742U] = 0U; + out[i][743U] = 0U; + out[i][744U] = 0U; + out[i][745U] = 0U; + out[i][746U] = 0U; + out[i][747U] = 0U; + out[i][748U] = 0U; + out[i][749U] = 0U; + out[i][750U] = 0U; + out[i][751U] = 0U; + out[i][752U] = 0U; + out[i][753U] = 0U; + out[i][754U] = 0U; + out[i][755U] = 0U; + out[i][756U] = 0U; + out[i][757U] = 0U; + out[i][758U] = 0U; + out[i][759U] = 0U; + out[i][760U] = 0U; + out[i][761U] = 0U; + out[i][762U] = 0U; + out[i][763U] = 0U; + out[i][764U] = 0U; + out[i][765U] = 0U; + out[i][766U] = 0U; + out[i][767U] = 0U; + out[i][768U] = 0U; + out[i][769U] = 0U; + out[i][770U] = 0U; + out[i][771U] = 0U; + out[i][772U] = 0U; + out[i][773U] = 0U; + out[i][774U] = 0U; + out[i][775U] = 0U; + out[i][776U] = 0U; + out[i][777U] = 0U; + out[i][778U] = 0U; + out[i][779U] = 0U; + out[i][780U] = 0U; + out[i][781U] = 0U; + out[i][782U] = 0U; + out[i][783U] = 0U; + out[i][784U] = 0U; + out[i][785U] = 0U; + out[i][786U] = 0U; + out[i][787U] = 0U; + out[i][788U] = 0U; + out[i][789U] = 0U; + out[i][790U] = 0U; + out[i][791U] = 0U; + out[i][792U] = 0U; + out[i][793U] = 0U; + out[i][794U] = 0U; + out[i][795U] = 0U; + out[i][796U] = 0U; + out[i][797U] = 0U; + out[i][798U] = 0U; + out[i][799U] = 0U; + out[i][800U] = 0U; + out[i][801U] = 0U; + out[i][802U] = 0U; + out[i][803U] = 0U; + out[i][804U] = 0U; + out[i][805U] = 0U; + out[i][806U] = 0U; + out[i][807U] = 0U; + out[i][808U] = 0U; + out[i][809U] = 0U; + out[i][810U] = 0U; + out[i][811U] = 0U; + out[i][812U] = 0U; + out[i][813U] = 0U; + out[i][814U] = 0U; + out[i][815U] = 0U; + out[i][816U] = 0U; + out[i][817U] = 0U; + out[i][818U] = 0U; + out[i][819U] = 0U; + out[i][820U] = 0U; + out[i][821U] = 0U; + out[i][822U] = 0U; + out[i][823U] = 0U; + out[i][824U] = 0U; + out[i][825U] = 0U; + out[i][826U] = 0U; + out[i][827U] = 0U; + out[i][828U] = 0U; + out[i][829U] = 0U; + out[i][830U] = 0U; + out[i][831U] = 0U; + out[i][832U] = 0U; + out[i][833U] = 0U; + out[i][834U] = 0U; + out[i][835U] = 0U; + out[i][836U] = 0U; + out[i][837U] = 0U; + out[i][838U] = 0U; + out[i][839U] = 0U; + } + bool uu____0; + if (!libcrux_platform_simd256_support()) + uu____0 = true; + else + uu____0 = !false; + if (uu____0) { + core_ops_range_Range__size_t iter = core_iter_traits_collect__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____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t i = uu____1.f0; + uint8_t uu____2[840U]; + libcrux_digest_shake128( + (size_t)840U, + Eurydice_array_to_slice( + (size_t)34U, input[i], uint8_t, Eurydice_slice), + uu____2, + void*); + memcpy(out[i], uu____2, (size_t)840U * sizeof(uint8_t)); + } + } + } else { + Eurydice_slice uu____3 = + Eurydice_array_to_slice((size_t)34U, input[0U], uint8_t, Eurydice_slice); + Eurydice_slice uu____4 = + Eurydice_array_to_slice((size_t)34U, input[1U], uint8_t, Eurydice_slice); + Eurydice_slice uu____5 = + Eurydice_array_to_slice((size_t)34U, input[2U], uint8_t, Eurydice_slice); + __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_ + uu____6 = libcrux_digest_shake128x4( + (size_t)840U, + uu____3, + uu____4, + uu____5, + Eurydice_array_to_slice( + (size_t)34U, input[0U], uint8_t, Eurydice_slice), + __uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t__uint8_t_840size_t_); + uint8_t d0[840U]; + memcpy(d0, uu____6.fst, (size_t)840U * sizeof(uint8_t)); + uint8_t d1[840U]; + memcpy(d1, uu____6.snd, (size_t)840U * sizeof(uint8_t)); + uint8_t d2[840U]; + memcpy(d2, uu____6.thd, (size_t)840U * sizeof(uint8_t)); + uint8_t uu____7[840U]; + memcpy(uu____7, d0, (size_t)840U * sizeof(uint8_t)); + memcpy(out[0U], uu____7, (size_t)840U * sizeof(uint8_t)); + uint8_t uu____8[840U]; + memcpy(uu____8, d1, (size_t)840U * sizeof(uint8_t)); + memcpy(out[1U], uu____8, (size_t)840U * sizeof(uint8_t)); + uint8_t uu____9[840U]; + memcpy(uu____9, d2, (size_t)840U * sizeof(uint8_t)); + memcpy(out[2U], uu____9, (size_t)840U * sizeof(uint8_t)); + } + uint8_t uu____10[3U][840U]; + memcpy(uu____10, out, (size_t)3U * sizeof(uint8_t[840U])); + memcpy(ret, uu____10, (size_t)3U * sizeof(uint8_t[840U])); +} + +void +libcrux_kyber_matrix_sample_matrix_A___3size_t(uint8_t seed[34U], + bool transpose, + int32_t ret[3U][3U][256U]) +{ + int32_t A_transpose[3U][3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) { + memcpy( + A_transpose[i][0U], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + memcpy( + A_transpose[i][1U], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + memcpy( + A_transpose[i][2U], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + } + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__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____0 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____0.tag == core_option_None) + break; + else { + size_t i0 = uu____0.f0; + uint8_t uu____1[34U]; + memcpy(uu____1, seed, (size_t)34U * sizeof(uint8_t)); + uint8_t seeds[3U][34U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + memcpy(seeds[i], uu____1, (size_t)34U * sizeof(uint8_t)); + core_ops_range_Range__size_t iter1 = + core_iter_traits_collect__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____2 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter1, size_t, core_option_Option__size_t); + if (uu____2.tag == core_option_None) + break; + else { + size_t j = uu____2.f0; + seeds[j][32U] = (uint8_t)i0; + seeds[j][33U] = (uint8_t)j; + } + } + uint8_t uu____3[3U][34U]; + memcpy(uu____3, seeds, (size_t)3U * sizeof(uint8_t[34U])); + uint8_t xof_bytes[3U][840U]; + libcrux_kyber_hash_functions_XOFx4___3size_t(uu____3, xof_bytes); + core_ops_range_Range__size_t iter = + core_iter_traits_collect__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____4 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter, size_t, core_option_Option__size_t); + if (uu____4.tag == core_option_None) + break; + else { + size_t j = uu____4.f0; + uint8_t uu____5[840U]; + memcpy(uu____5, xof_bytes[j], (size_t)840U * sizeof(uint8_t)); + int32_t sampled[256U]; + libcrux_kyber_sampling_sample_from_uniform_distribution(uu____5, + sampled); + if (transpose) + memcpy(A_transpose[j][i0], sampled, (size_t)256U * sizeof(int32_t)); + else + memcpy(A_transpose[i0][j], sampled, (size_t)256U * sizeof(int32_t)); + } + } + } + } + int32_t uu____6[3U][3U][256U]; + memcpy(uu____6, A_transpose, (size_t)3U * sizeof(int32_t[3U][256U])); + memcpy(ret, uu____6, (size_t)3U * sizeof(int32_t[3U][256U])); +} + +void +libcrux_kyber_ind_cpa_into_padded_array___34size_t(Eurydice_slice slice, + uint8_t ret[34U]) +{ + uint8_t out[34U]; + for (size_t i = (size_t)0U; i < (size_t)34U; i++) + out[i] = 0U; + uint8_t* uu____0 = out; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)34U, + uu____0, + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(slice, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + 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)); +} + +void +libcrux_kyber_ind_cpa_into_padded_array___33size_t(Eurydice_slice slice, + uint8_t ret[33U]) +{ + uint8_t out[33U]; + for (size_t i = (size_t)0U; i < (size_t)33U; i++) + out[i] = 0U; + uint8_t* uu____0 = out; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)33U, + uu____0, + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(slice, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + 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)); +} + +void +libcrux_kyber_hash_functions_PRF___128size_t(Eurydice_slice input, + uint8_t ret[128U]) +{ + uint8_t ret0[128U]; + libcrux_digest_shake256((size_t)128U, input, ret0, void*); + memcpy(ret, ret0, (size_t)128U * sizeof(uint8_t)); +} + +void +libcrux_kyber_sampling_sample_from_binomial_distribution___2size_t( + Eurydice_slice randomness, + int32_t ret[256U]) +{ + int32_t uu____0[256U]; + libcrux_kyber_sampling_sample_from_binomial_distribution_2(randomness, + uu____0); + memcpy(ret, uu____0, (size_t)256U * sizeof(int32_t)); +} + +K___libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__uint8_t +libcrux_kyber_ind_cpa_sample_vector_cbd_then_ntt___3size_t_2size_t_128size_t( + uint8_t prf_input[33U], + uint8_t domain_separator) +{ + int32_t re_as_ntt[3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + memcpy( + re_as_ntt[i], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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____0 = + core_iter_range__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; + prf_input[32U] = domain_separator; + domain_separator = (uint32_t)domain_separator + 1U; + uint8_t prf_output[128U]; + libcrux_kyber_hash_functions_PRF___128size_t( + Eurydice_array_to_slice( + (size_t)33U, prf_input, uint8_t, Eurydice_slice), + prf_output); + int32_t r[256U]; + libcrux_kyber_sampling_sample_from_binomial_distribution___2size_t( + Eurydice_array_to_slice( + (size_t)128U, prf_output, uint8_t, Eurydice_slice), + r); + int32_t uu____1[256U]; + libcrux_kyber_ntt_ntt_binomially_sampled_ring_element(r, uu____1); + memcpy(re_as_ntt[i], uu____1, (size_t)256U * sizeof(int32_t)); + } + } + int32_t uu____2[3U][256U]; + memcpy(uu____2, re_as_ntt, (size_t)3U * sizeof(int32_t[256U])); + K___libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__uint8_t lit; + memcpy(lit.fst, uu____2, (size_t)3U * sizeof(int32_t[256U])); + lit.snd = domain_separator; + return lit; +} + +void +libcrux_kyber_arithmetic_add_to_ring_element___3size_t(int32_t lhs[256U], + int32_t (*rhs)[256U], + int32_t ret[256U]) +{ + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)256U, lhs, int32_t, Eurydice_slice), + int32_t, + size_t); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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; + size_t uu____1 = i; + lhs[uu____1] = lhs[uu____1] + rhs[0U][i]; + } + } + memcpy(ret, lhs, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_matrix_compute_As_plus_e___3size_t(int32_t (*matrix_A)[3U][256U], + int32_t (*s_as_ntt)[256U], + int32_t (*error_as_ntt)[256U], + int32_t ret[3U][256U]) +{ + int32_t result[3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + memcpy( + result[i], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t lit0; + lit0.start = (size_t)0U; + lit0.end = core_slice___Slice_T___len( + Eurydice_array_to_slice( + (size_t)3U, matrix_A, Eurydice_error_t_cg_array, Eurydice_slice), + int32_t[3U][256U], + size_t); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit0, 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__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; + int32_t(*row)[256U] = matrix_A[i]; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)3U, row, int32_t[256U], Eurydice_slice), + int32_t[256U], + size_t); + core_ops_range_Range__size_t iter0 = + core_iter_traits_collect__I__into_iter( + lit, core_ops_range_Range__size_t, core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t j = uu____1.f0; + int32_t(*matrix_element)[256U] = &row[j]; + int32_t product[256U]; + libcrux_kyber_ntt_ntt_multiply(matrix_element, &s_as_ntt[j], product); + int32_t uu____2[256U]; + libcrux_kyber_arithmetic_add_to_ring_element___3size_t( + result[i], &product, uu____2); + memcpy(result[i], uu____2, (size_t)256U * sizeof(int32_t)); + } + } + core_ops_range_Range__size_t iter1 = + core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____3 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter1, size_t, core_option_Option__size_t); + if (uu____3.tag == core_option_None) + break; + else { + size_t j = uu____3.f0; + int32_t coefficient_normal_form = + libcrux_kyber_arithmetic_to_standard_domain(result[i][j]); + int32_t uu____4 = libcrux_kyber_arithmetic_barrett_reduce( + coefficient_normal_form + error_as_ntt[i][j]); + result[i][j] = uu____4; + } + } + } + } + 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])); +} + +void +libcrux_kyber_ind_cpa_serialize_secret_key___3size_t_1152size_t( + int32_t key[3U][256U], + uint8_t ret[1152U]) +{ + uint8_t out[1152U]; + for (size_t i = (size_t)0U; i < (size_t)1152U; i++) + out[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)3U, key, int32_t[256U], Eurydice_slice), + int32_t[256U], + size_t); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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; + int32_t re[256U]; + memcpy(re, key[i], (size_t)256U * sizeof(int32_t)); + Eurydice_slice uu____1 = Eurydice_array_to_subslice( + (size_t)1152U, + out, + ((core_ops_range_Range__size_t){ + .start = i * LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT, + .end = (i + (size_t)1U) * + LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint8_t ret0[384U]; + libcrux_kyber_serialize_serialize_uncompressed_ring_element(re, ret0); + core_slice___Slice_T___copy_from_slice( + uu____1, + Eurydice_array_to_slice((size_t)384U, ret0, uint8_t, Eurydice_slice), + uint8_t, + 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)); +} + +void +libcrux_kyber_ind_cpa_serialize_public_key___3size_t_1152size_t_1184size_t( + int32_t t_as_ntt[3U][256U], + Eurydice_slice seed_for_a, + uint8_t ret[1184U]) +{ + uint8_t public_key_serialized[1184U]; + for (size_t i = (size_t)0U; i < (size_t)1184U; i++) + public_key_serialized[i] = 0U; + Eurydice_slice uu____0 = + Eurydice_array_to_subslice((size_t)1184U, + public_key_serialized, + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, .end = (size_t)1152U }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t uu____1[3U][256U]; + memcpy(uu____1, t_as_ntt, (size_t)3U * sizeof(int32_t[256U])); + uint8_t ret0[1152U]; + libcrux_kyber_ind_cpa_serialize_secret_key___3size_t_1152size_t(uu____1, + ret0); + core_slice___Slice_T___copy_from_slice( + uu____0, + Eurydice_array_to_slice((size_t)1152U, ret0, uint8_t, Eurydice_slice), + uint8_t, + void*); + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice_from((size_t)1184U, + public_key_serialized, + (size_t)1152U, + uint8_t, + size_t, + Eurydice_slice), + 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)); +} + +K___uint8_t_1152size_t__uint8_t_1184size_t_ +libcrux_kyber_ind_cpa_generate_keypair___3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t( + Eurydice_slice key_generation_seed) +{ + uint8_t hashed[64U]; + libcrux_kyber_hash_functions_G(key_generation_seed, 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), + (size_t)32U, + uint8_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]; + uint8_t ret[34U]; + libcrux_kyber_ind_cpa_into_padded_array___34size_t(seed_for_A, ret); + libcrux_kyber_matrix_sample_matrix_A___3size_t(ret, true, A_transpose); + uint8_t prf_input[33U]; + libcrux_kyber_ind_cpa_into_padded_array___33size_t(seed_for_secret_and_error, + prf_input); + uint8_t uu____1[33U]; + memcpy(uu____1, prf_input, (size_t)33U * sizeof(uint8_t)); + K___libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__uint8_t uu____2 = + libcrux_kyber_ind_cpa_sample_vector_cbd_then_ntt___3size_t_2size_t_128size_t( + uu____1, 0U); + int32_t secret_as_ntt[3U][256U]; + memcpy(secret_as_ntt, uu____2.fst, (size_t)3U * sizeof(int32_t[256U])); + uint8_t domain_separator = uu____2.snd; + uint8_t uu____3[33U]; + memcpy(uu____3, prf_input, (size_t)33U * sizeof(uint8_t)); + int32_t error_as_ntt[3U][256U]; + memcpy( + error_as_ntt, + libcrux_kyber_ind_cpa_sample_vector_cbd_then_ntt___3size_t_2size_t_128size_t( + uu____3, domain_separator) + .fst, + (size_t)3U * sizeof(int32_t[256U])); + int32_t t_as_ntt[3U][256U]; + libcrux_kyber_matrix_compute_As_plus_e___3size_t( + 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]; + libcrux_kyber_ind_cpa_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]; + libcrux_kyber_ind_cpa_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)); + K___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)); + return lit; +} + +void +libcrux_kyber_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]; + for (size_t i = (size_t)0U; i < (size_t)2400U; i++) + out[i] = 0U; + size_t pointer = (size_t)0U; + uint8_t* uu____0 = out; + size_t uu____1 = pointer; + size_t uu____2 = pointer; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)2400U, + uu____0, + ((core_ops_range_Range__size_t){ + .start = uu____1, + .end = + uu____2 + core_slice___Slice_T___len(private_key, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + private_key, + uint8_t, + void*); + pointer = pointer + core_slice___Slice_T___len(private_key, uint8_t, size_t); + uint8_t* uu____3 = out; + size_t uu____4 = pointer; + size_t uu____5 = pointer; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)2400U, + uu____3, + ((core_ops_range_Range__size_t){ + .start = uu____4, + .end = + uu____5 + core_slice___Slice_T___len(public_key, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + public_key, + uint8_t, + void*); + pointer = pointer + core_slice___Slice_T___len(public_key, uint8_t, size_t); + Eurydice_slice uu____6 = Eurydice_array_to_subslice( + (size_t)2400U, + out, + ((core_ops_range_Range__size_t){ + .start = pointer, + .end = pointer + LIBCRUX_KYBER_CONSTANTS_H_DIGEST_SIZE }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint8_t ret0[32U]; + libcrux_kyber_hash_functions_H(public_key, ret0); + core_slice___Slice_T___copy_from_slice( + uu____6, + Eurydice_array_to_slice((size_t)32U, ret0, uint8_t, Eurydice_slice), + uint8_t, + void*); + pointer = pointer + LIBCRUX_KYBER_CONSTANTS_H_DIGEST_SIZE; + uint8_t* uu____7 = out; + size_t uu____8 = pointer; + size_t uu____9 = pointer; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)2400U, + uu____7, + ((core_ops_range_Range__size_t){ + .start = uu____8, + .end = uu____9 + core_slice___Slice_T___len( + implicit_rejection_value, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + 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)); +} + +void +libcrux_kyber_types__libcrux_kyber__types__KyberPrivateKey_SIZE__8__from___2400size_t( + uint8_t value[2400U], + uint8_t ret[2400U]) +{ + uint8_t uu____0[2400U]; + memcpy(uu____0, value, (size_t)2400U * sizeof(uint8_t)); + memcpy(ret, uu____0, (size_t)2400U * sizeof(uint8_t)); +} + +libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t +libcrux_kyber_types__libcrux_kyber__types__KyberKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t( + uint8_t sk[2400U], + uint8_t pk[1184U]) +{ + libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t lit; + memcpy(lit.sk, sk, (size_t)2400U * sizeof(uint8_t)); + memcpy(lit.pk, pk, (size_t)1184U * sizeof(uint8_t)); + return lit; +} + +libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t +libcrux_kyber_generate_keypair___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 = LIBCRUX_KYBER_CONSTANTS_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, + LIBCRUX_KYBER_CONSTANTS_CPA_PKE_KEY_GENERATION_SEED_SIZE, + uint8_t, + size_t, + Eurydice_slice); + K___uint8_t_1152size_t__uint8_t_1184size_t_ uu____0 = + libcrux_kyber_ind_cpa_generate_keypair___3size_t_1152size_t_1184size_t_1152size_t_2size_t_128size_t( + ind_cpa_keypair_randomness); + uint8_t ind_cpa_private_key[1152U]; + memcpy(ind_cpa_private_key, uu____0.fst, (size_t)1152U * sizeof(uint8_t)); + uint8_t public_key[1184U]; + memcpy(public_key, uu____0.snd, (size_t)1184U * sizeof(uint8_t)); + Eurydice_slice uu____1 = Eurydice_array_to_slice( + (size_t)1152U, ind_cpa_private_key, uint8_t, Eurydice_slice); + uint8_t secret_key_serialized[2400U]; + libcrux_kyber_serialize_kem_secret_key___2400size_t( + uu____1, + Eurydice_array_to_slice((size_t)1184U, public_key, uint8_t, Eurydice_slice), + implicit_rejection_value, + secret_key_serialized); + uint8_t uu____2[2400U]; + memcpy(uu____2, secret_key_serialized, (size_t)2400U * sizeof(uint8_t)); + uint8_t private_key[2400U]; + libcrux_kyber_types__libcrux_kyber__types__KyberPrivateKey_SIZE__8__from___2400size_t( + uu____2, private_key); + uint8_t uu____3[2400U]; + memcpy(uu____3, private_key, (size_t)2400U * sizeof(uint8_t)); + uint8_t uu____4[1184U]; + memcpy(uu____4, public_key, (size_t)1184U * sizeof(uint8_t)); + return libcrux_kyber_types__libcrux_kyber__types__KyberKeyPair_PRIVATE_KEY_SIZE__PUBLIC_KEY_SIZE___from___2400size_t_1184size_t( + uu____3, uu____4); +} + +libcrux_kyber_types_KyberKeyPair___2400size_t_1184size_t +libcrux_kyber_kyber768_generate_key_pair_768(uint8_t randomness[64U]) +{ + uint8_t uu____0[64U]; + memcpy(uu____0, randomness, (size_t)64U * sizeof(uint8_t)); + return libcrux_kyber_generate_keypair___3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t( + uu____0); +} + +void +libcrux_kyber_ind_cpa_into_padded_array___64size_t(Eurydice_slice slice, + uint8_t ret[64U]) +{ + uint8_t out[64U]; + for (size_t i = (size_t)0U; i < (size_t)64U; i++) + out[i] = 0U; + uint8_t* uu____0 = out; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)64U, + uu____0, + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(slice, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + 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)); +} + +uint8_t* +libcrux_kyber_types__libcrux_kyber__types__KyberPublicKey_SIZE__18__as_slice___1184size_t( + uint8_t (*self)[1184U]) +{ + return self[0U]; +} + +void +libcrux_kyber_ind_cpa_deserialize_public_key___3size_t( + Eurydice_slice public_key, + int32_t ret[3U][256U]) +{ + int32_t t_as_ntt[3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + memcpy( + t_as_ntt[i], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(public_key, uint8_t, size_t) / + LIBCRUX_KYBER_CONSTANTS_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__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 t_as_ntt_bytes = Eurydice_slice_subslice( + public_key, + ((core_ops_range_Range__size_t){ + .start = i * LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT, + .end = i * LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT + + LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t uu____1[256U]; + libcrux_kyber_serialize_deserialize_to_uncompressed_ring_element( + t_as_ntt_bytes, uu____1); + memcpy(t_as_ntt[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])); +} + +void +libcrux_kyber_ind_cpa_sample_ring_element_cbd___3size_t_128size_t_2size_t( + uint8_t* prf_input, + uint8_t* domain_separator, + int32_t ret[3U][256U]) +{ + int32_t error_1[3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + memcpy( + error_1[i], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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____0 = + core_iter_range__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; + prf_input[32U] = domain_separator[0U]; + domain_separator[0U] = (uint32_t)domain_separator[0U] + 1U; + uint8_t prf_output[128U]; + libcrux_kyber_hash_functions_PRF___128size_t( + Eurydice_array_to_slice( + (size_t)33U, prf_input, uint8_t, Eurydice_slice), + prf_output); + int32_t uu____1[256U]; + libcrux_kyber_sampling_sample_from_binomial_distribution___2size_t( + Eurydice_array_to_slice( + (size_t)128U, prf_output, uint8_t, Eurydice_slice), + uu____1); + 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])); +} + +void +libcrux_kyber_ntt_invert_ntt_montgomery___3size_t(int32_t re[256U], + int32_t ret[256U]) +{ + size_t zeta_i = + LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT / (size_t)2U; + libcrux_kyber_ntt_invert_ntt_at_layer(&zeta_i, re, (size_t)1U, re); + libcrux_kyber_ntt_invert_ntt_at_layer(&zeta_i, re, (size_t)2U, re); + libcrux_kyber_ntt_invert_ntt_at_layer(&zeta_i, re, (size_t)3U, re); + libcrux_kyber_ntt_invert_ntt_at_layer(&zeta_i, re, (size_t)4U, re); + libcrux_kyber_ntt_invert_ntt_at_layer(&zeta_i, re, (size_t)5U, re); + libcrux_kyber_ntt_invert_ntt_at_layer(&zeta_i, re, (size_t)6U, re); + libcrux_kyber_ntt_invert_ntt_at_layer(&zeta_i, re, (size_t)7U, re); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, .end = (size_t)2U }), + 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__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; + int32_t uu____1 = libcrux_kyber_arithmetic_barrett_reduce(re[i]); + re[i] = uu____1; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_matrix_compute_vector_u___3size_t(int32_t (*a_as_ntt)[3U][256U], + int32_t (*r_as_ntt)[256U], + int32_t (*error_1)[256U], + int32_t ret[3U][256U]) +{ + int32_t result[3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + memcpy( + result[i], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t lit0; + lit0.start = (size_t)0U; + lit0.end = core_slice___Slice_T___len( + Eurydice_array_to_slice( + (size_t)3U, a_as_ntt, Eurydice_error_t_cg_array, Eurydice_slice), + int32_t[3U][256U], + size_t); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit0, 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__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; + int32_t(*row)[256U] = a_as_ntt[i]; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)3U, row, int32_t[256U], Eurydice_slice), + int32_t[256U], + size_t); + core_ops_range_Range__size_t iter0 = + core_iter_traits_collect__I__into_iter( + lit, core_ops_range_Range__size_t, core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t j = uu____1.f0; + int32_t(*a_element)[256U] = &row[j]; + int32_t product[256U]; + libcrux_kyber_ntt_ntt_multiply(a_element, &r_as_ntt[j], product); + int32_t uu____2[256U]; + libcrux_kyber_arithmetic_add_to_ring_element___3size_t( + result[i], &product, uu____2); + memcpy(result[i], uu____2, (size_t)256U * sizeof(int32_t)); + } + } + int32_t uu____3[256U]; + libcrux_kyber_ntt_invert_ntt_montgomery___3size_t(result[i], uu____3); + memcpy(result[i], uu____3, (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter1 = + core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____4 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter1, size_t, core_option_Option__size_t); + if (uu____4.tag == core_option_None) + break; + else { + size_t j = uu____4.f0; + int32_t coefficient_normal_form = + libcrux_kyber_arithmetic_montgomery_reduce(result[i][j] * + (int32_t)1441); + int32_t uu____5 = libcrux_kyber_arithmetic_barrett_reduce( + coefficient_normal_form + error_1[i][j]); + result[i][j] = uu____5; + } + } + } + } + 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])); +} + +void +libcrux_kyber_matrix_compute_ring_element_v___3size_t(int32_t (*t_as_ntt)[256U], + int32_t (*r_as_ntt)[256U], + int32_t (*error_2)[256U], + int32_t (*message)[256U], + int32_t ret[256U]) +{ + int32_t result[256U]; + memcpy( + result, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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____0 = + core_iter_range__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; + int32_t product[256U]; + libcrux_kyber_ntt_ntt_multiply(&t_as_ntt[i], &r_as_ntt[i], product); + libcrux_kyber_arithmetic_add_to_ring_element___3size_t( + result, &product, result); + } + } + libcrux_kyber_ntt_invert_ntt_montgomery___3size_t(result, result); + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t i = uu____1.f0; + int32_t coefficient_normal_form = + libcrux_kyber_arithmetic_montgomery_reduce(result[i] * (int32_t)1441); + int32_t uu____2 = libcrux_kyber_arithmetic_barrett_reduce( + coefficient_normal_form + error_2[0U][i] + message[0U][i]); + result[i] = uu____2; + } + } + memcpy(ret, result, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_serialize_compress_then_serialize_10___320size_t( + int32_t re[256U], + uint8_t ret[320U]) +{ + uint8_t serialized[320U]; + for (size_t i = (size_t)0U; i < (size_t)320U; i++) + serialized[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = + core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)256U, re, int32_t, Eurydice_slice), + int32_t, + size_t) / + (size_t)4U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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 coefficients = Eurydice_array_to_subslice( + (size_t)256U, + re, + ((core_ops_range_Range__size_t){ .start = i * (size_t)4U, + .end = i * (size_t)4U + (size_t)4U }), + int32_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t coefficient1 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 10U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)0U, int32_t, int32_t))); + int32_t coefficient2 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 10U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)1U, int32_t, int32_t))); + int32_t coefficient3 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 10U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)2U, int32_t, int32_t))); + int32_t coefficient4 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 10U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)3U, int32_t, int32_t))); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t uu____1 = + libcrux_kyber_serialize_compress_coefficients_10( + coefficient1, coefficient2, coefficient3, coefficient4); + uint8_t coef1 = uu____1.fst; + uint8_t coef2 = uu____1.snd; + uint8_t coef3 = uu____1.thd; + uint8_t coef4 = uu____1.f3; + uint8_t coef5 = uu____1.f4; + serialized[(size_t)5U * i] = coef1; + serialized[(size_t)5U * i + (size_t)1U] = coef2; + serialized[(size_t)5U * i + (size_t)2U] = coef3; + serialized[(size_t)5U * i + (size_t)3U] = coef4; + 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)); +} + +void +libcrux_kyber_serialize_compress_then_serialize_11___320size_t( + int32_t re[256U], + uint8_t ret[320U]) +{ + uint8_t serialized[320U]; + for (size_t i = (size_t)0U; i < (size_t)320U; i++) + serialized[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = + core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)256U, re, int32_t, Eurydice_slice), + int32_t, + size_t) / + (size_t)8U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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 coefficients = Eurydice_array_to_subslice( + (size_t)256U, + re, + ((core_ops_range_Range__size_t){ .start = i * (size_t)8U, + .end = i * (size_t)8U + (size_t)8U }), + int32_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t coefficient1 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)0U, int32_t, int32_t))); + int32_t coefficient2 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)1U, int32_t, int32_t))); + int32_t coefficient3 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)2U, int32_t, int32_t))); + int32_t coefficient4 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)3U, int32_t, int32_t))); + int32_t coefficient5 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)4U, int32_t, int32_t))); + int32_t coefficient6 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)5U, int32_t, int32_t))); + int32_t coefficient7 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)6U, int32_t, int32_t))); + int32_t coefficient8 = + libcrux_kyber_compress_compress_ciphertext_coefficient( + 11U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)7U, int32_t, int32_t))); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t_uint8_t + uu____1 = + libcrux_kyber_serialize_compress_coefficients_11(coefficient1, + coefficient2, + coefficient3, + coefficient4, + coefficient5, + coefficient6, + coefficient7, + coefficient8); + uint8_t coef1 = uu____1.fst; + uint8_t coef2 = uu____1.snd; + uint8_t coef3 = uu____1.thd; + uint8_t coef4 = uu____1.f3; + uint8_t coef5 = uu____1.f4; + uint8_t coef6 = uu____1.f5; + uint8_t coef7 = uu____1.f6; + uint8_t coef8 = uu____1.f7; + uint8_t coef9 = uu____1.f8; + uint8_t coef10 = uu____1.f9; + uint8_t coef11 = uu____1.f10; + serialized[(size_t)11U * i] = coef1; + serialized[(size_t)11U * i + (size_t)1U] = coef2; + serialized[(size_t)11U * i + (size_t)2U] = coef3; + serialized[(size_t)11U * i + (size_t)3U] = coef4; + serialized[(size_t)11U * i + (size_t)4U] = coef5; + serialized[(size_t)11U * i + (size_t)5U] = coef6; + serialized[(size_t)11U * i + (size_t)6U] = coef7; + serialized[(size_t)11U * i + (size_t)7U] = coef8; + serialized[(size_t)11U * i + (size_t)8U] = coef9; + serialized[(size_t)11U * i + (size_t)9U] = coef10; + 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)); +} + +void +libcrux_kyber_serialize_compress_then_serialize_ring_element_u___10size_t_320size_t( + int32_t re[256U], + uint8_t ret[320U]) +{ + uint8_t uu____0[320U]; + libcrux_kyber_serialize_compress_then_serialize_10___320size_t(re, uu____0); + memcpy(ret, uu____0, (size_t)320U * sizeof(uint8_t)); +} + +void +libcrux_kyber_ind_cpa_compress_then_serialize_u___3size_t_960size_t_10size_t_320size_t( + int32_t input[3U][256U], + uint8_t ret[960U]) +{ + uint8_t out[960U]; + for (size_t i = (size_t)0U; i < (size_t)960U; i++) + out[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)3U, input, int32_t[256U], Eurydice_slice), + int32_t[256U], + size_t); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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; + int32_t re[256U]; + memcpy(re, input[i], (size_t)256U * sizeof(int32_t)); + Eurydice_slice uu____1 = Eurydice_array_to_subslice( + (size_t)960U, + out, + ((core_ops_range_Range__size_t){ + .start = i * ((size_t)960U / (size_t)3U), + .end = (i + (size_t)1U) * ((size_t)960U / (size_t)3U) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint8_t ret0[320U]; + libcrux_kyber_serialize_compress_then_serialize_ring_element_u___10size_t_320size_t( + re, ret0); + core_slice___Slice_T___copy_from_slice( + uu____1, + Eurydice_array_to_slice((size_t)320U, ret0, uint8_t, Eurydice_slice), + uint8_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)); +} + +void +libcrux_kyber_serialize_compress_then_serialize_4___128size_t(int32_t re[256U], + uint8_t ret[128U]) +{ + uint8_t serialized[128U]; + for (size_t i = (size_t)0U; i < (size_t)128U; i++) + serialized[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = + core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)256U, re, int32_t, Eurydice_slice), + int32_t, + size_t) / + (size_t)2U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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 coefficients = Eurydice_array_to_subslice( + (size_t)256U, + re, + ((core_ops_range_Range__size_t){ .start = i * (size_t)2U, + .end = i * (size_t)2U + (size_t)2U }), + int32_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint8_t coefficient1 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 4U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)0U, int32_t, int32_t))); + uint8_t coefficient2 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 4U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)1U, int32_t, int32_t))); + 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)); +} + +void +libcrux_kyber_serialize_compress_then_serialize_5___128size_t(int32_t re[256U], + uint8_t ret[128U]) +{ + uint8_t serialized[128U]; + for (size_t i = (size_t)0U; i < (size_t)128U; i++) + serialized[i] = 0U; + core_ops_range_Range__size_t lit; + lit.start = (size_t)0U; + lit.end = + core_slice___Slice_T___len( + Eurydice_array_to_slice((size_t)256U, re, int32_t, Eurydice_slice), + int32_t, + size_t) / + (size_t)8U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + lit, 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__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 coefficients = Eurydice_array_to_subslice( + (size_t)256U, + re, + ((core_ops_range_Range__size_t){ .start = i * (size_t)8U, + .end = i * (size_t)8U + (size_t)8U }), + int32_t, + core_ops_range_Range__size_t, + Eurydice_slice); + uint8_t coefficient1 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)0U, int32_t, int32_t))); + uint8_t coefficient2 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)1U, int32_t, int32_t))); + uint8_t coefficient3 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)2U, int32_t, int32_t))); + uint8_t coefficient4 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)3U, int32_t, int32_t))); + uint8_t coefficient5 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)4U, int32_t, int32_t))); + uint8_t coefficient6 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)5U, int32_t, int32_t))); + uint8_t coefficient7 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)6U, int32_t, int32_t))); + uint8_t coefficient8 = + (uint8_t)libcrux_kyber_compress_compress_ciphertext_coefficient( + 5U, + libcrux_kyber_arithmetic_to_unsigned_representative( + Eurydice_slice_index(coefficients, (size_t)7U, int32_t, int32_t))); + K___uint8_t_uint8_t_uint8_t_uint8_t_uint8_t uu____1 = + libcrux_kyber_serialize_compress_coefficients_5(coefficient2, + coefficient1, + coefficient4, + coefficient3, + coefficient5, + coefficient7, + coefficient6, + coefficient8); + uint8_t coef1 = uu____1.fst; + uint8_t coef2 = uu____1.snd; + uint8_t coef3 = uu____1.thd; + uint8_t coef4 = uu____1.f3; + uint8_t coef5 = uu____1.f4; + serialized[(size_t)5U * i] = coef1; + serialized[(size_t)5U * i + (size_t)1U] = coef2; + serialized[(size_t)5U * i + (size_t)2U] = coef3; + serialized[(size_t)5U * i + (size_t)3U] = coef4; + 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)); +} + +void +libcrux_kyber_serialize_compress_then_serialize_ring_element_v___4size_t_128size_t( + int32_t re[256U], + uint8_t ret[128U]) +{ + uint8_t uu____0[128U]; + libcrux_kyber_serialize_compress_then_serialize_4___128size_t(re, uu____0); + memcpy(ret, uu____0, (size_t)128U * sizeof(uint8_t)); +} + +void +libcrux_kyber_ind_cpa_into_padded_array___1088size_t(Eurydice_slice slice, + uint8_t ret[1088U]) +{ + uint8_t out[1088U]; + for (size_t i = (size_t)0U; i < (size_t)1088U; i++) + out[i] = 0U; + uint8_t* uu____0 = out; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)1088U, + uu____0, + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(slice, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + 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)); +} + +void +libcrux_kyber_ind_cpa_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]; + libcrux_kyber_ind_cpa_deserialize_public_key___3size_t(public_key, 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]; + libcrux_kyber_ind_cpa_into_padded_array___34size_t(seed, ret0); + libcrux_kyber_matrix_sample_matrix_A___3size_t(ret0, false, A_transpose); + uint8_t prf_input[33U]; + libcrux_kyber_ind_cpa_into_padded_array___33size_t(randomness, prf_input); + uint8_t uu____0[33U]; + memcpy(uu____0, prf_input, (size_t)33U * sizeof(uint8_t)); + K___libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__uint8_t uu____1 = + libcrux_kyber_ind_cpa_sample_vector_cbd_then_ntt___3size_t_2size_t_128size_t( + uu____0, 0U); + int32_t r_as_ntt[3U][256U]; + memcpy(r_as_ntt, uu____1.fst, (size_t)3U * sizeof(int32_t[256U])); + uint8_t domain_separator = uu____1.snd; + int32_t error_1[3U][256U]; + libcrux_kyber_ind_cpa_sample_ring_element_cbd___3size_t_128size_t_2size_t( + prf_input, &domain_separator, error_1); + prf_input[32U] = domain_separator; + uint8_t prf_output[128U]; + libcrux_kyber_hash_functions_PRF___128size_t( + Eurydice_array_to_slice((size_t)33U, prf_input, uint8_t, Eurydice_slice), + prf_output); + int32_t error_2[256U]; + libcrux_kyber_sampling_sample_from_binomial_distribution___2size_t( + Eurydice_array_to_slice((size_t)128U, prf_output, uint8_t, Eurydice_slice), + error_2); + int32_t u[3U][256U]; + libcrux_kyber_matrix_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]; + libcrux_kyber_serialize_deserialize_then_decompress_message( + uu____2, message_as_ring_element); + int32_t v[256U]; + libcrux_kyber_matrix_compute_ring_element_v___3size_t( + t_as_ntt, r_as_ntt, &error_2, &message_as_ring_element, v); + int32_t uu____3[3U][256U]; + memcpy(uu____3, u, (size_t)3U * sizeof(int32_t[256U])); + uint8_t c1[960U]; + libcrux_kyber_ind_cpa_compress_then_serialize_u___3size_t_960size_t_10size_t_320size_t( + uu____3, c1); + uint8_t c2[128U]; + libcrux_kyber_serialize_compress_then_serialize_ring_element_v___4size_t_128size_t( + v, c2); + uint8_t ciphertext[1088U]; + libcrux_kyber_ind_cpa_into_padded_array___1088size_t( + Eurydice_array_to_slice((size_t)960U, c1, uint8_t, Eurydice_slice), + ciphertext); + Eurydice_slice uu____4 = Eurydice_array_to_subslice_from( + (size_t)1088U, ciphertext, (size_t)960U, uint8_t, size_t, Eurydice_slice); + core_slice___Slice_T___copy_from_slice( + uu____4, + core_array___Array_T__N__23__as_slice( + (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)); +} + +#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; + +K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t_ +libcrux_kyber_encapsulate___3size_t_1088size_t_1184size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t( + uint8_t (*public_key)[1184U], + uint8_t randomness[32U]) +{ + uint8_t to_hash[64U]; + libcrux_kyber_ind_cpa_into_padded_array___64size_t( + Eurydice_array_to_slice((size_t)32U, randomness, uint8_t, Eurydice_slice), + to_hash); + Eurydice_slice uu____0 = + Eurydice_array_to_subslice_from((size_t)64U, + to_hash, + LIBCRUX_KYBER_CONSTANTS_H_DIGEST_SIZE, + uint8_t, + size_t, + Eurydice_slice); + uint8_t ret[32U]; + libcrux_kyber_hash_functions_H( + Eurydice_array_to_slice( + (size_t)1184U, + libcrux_kyber_types__libcrux_kyber__types__KyberPublicKey_SIZE__18__as_slice___1184size_t( + public_key), + uint8_t, + Eurydice_slice), + ret); + core_slice___Slice_T___copy_from_slice( + uu____0, + Eurydice_array_to_slice((size_t)32U, ret, uint8_t, Eurydice_slice), + uint8_t, + void*); + uint8_t hashed[64U]; + libcrux_kyber_hash_functions_G( + Eurydice_array_to_slice((size_t)64U, to_hash, uint8_t, Eurydice_slice), + hashed); + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t uu____1 = + core_slice___Slice_T___split_at( + Eurydice_array_to_slice((size_t)64U, hashed, uint8_t, Eurydice_slice), + LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE, + uint8_t, + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); + Eurydice_slice shared_secret0 = uu____1.fst; + Eurydice_slice pseudorandomness = uu____1.snd; + Eurydice_slice uu____2 = Eurydice_array_to_slice( + (size_t)1184U, + libcrux_kyber_types__libcrux_kyber__types__KyberPublicKey_SIZE__18__as_slice___1184size_t( + public_key), + uint8_t, + Eurydice_slice); + uint8_t uu____3[32U]; + memcpy(uu____3, randomness, (size_t)32U * sizeof(uint8_t)); + uint8_t ciphertext[1088U]; + libcrux_kyber_ind_cpa_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( + uu____2, uu____3, pseudorandomness, ciphertext); + Result__uint8_t_32size_t__core_array_TryFromSliceError dst; + Eurydice_slice_to_array2( + &dst, shared_secret0, Eurydice_slice, uint8_t[32U], void*); + Result__uint8_t_32size_t__core_array_TryFromSliceError uu____4 = dst; + if (!(uu____4.tag == Ok)) { + KRML_HOST_EPRINTF( + "KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); + } + uint8_t shared_secret1[32U]; + memcpy(shared_secret1, uu____4.val.case_Ok, (size_t)32U * sizeof(uint8_t)); + uint8_t shared_secret[32U]; + memcpy(shared_secret, shared_secret1, (size_t)32U * sizeof(uint8_t)); + uint8_t uu____5[1088U]; + memcpy(uu____5, ciphertext, (size_t)1088U * sizeof(uint8_t)); + uint8_t uu____6[1088U]; + memcpy(uu____6, uu____5, (size_t)1088U * sizeof(uint8_t)); + uint8_t uu____7[32U]; + memcpy(uu____7, shared_secret, (size_t)32U * sizeof(uint8_t)); + K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t_ lit; + memcpy(lit.fst, uu____6, (size_t)1088U * sizeof(uint8_t)); + memcpy(lit.snd, uu____7, (size_t)32U * sizeof(uint8_t)); + return lit; +} + +K___libcrux_kyber_types_KyberCiphertext__1088size_t___uint8_t_32size_t_ +libcrux_kyber_kyber768_encapsulate_768(uint8_t (*public_key)[1184U], + uint8_t randomness[32U]) +{ + uint8_t(*uu____0)[1184U] = public_key; + uint8_t uu____1[32U]; + memcpy(uu____1, randomness, (size_t)32U * sizeof(uint8_t)); + return libcrux_kyber_encapsulate___3size_t_1088size_t_1184size_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); +} + +K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t +libcrux_kyber_types__libcrux_kyber__types__KyberPrivateKey_SIZE__12__split_at___2400size_t( + uint8_t (*self)[2400U], + size_t mid) +{ + return core_slice___Slice_T___split_at( + Eurydice_array_to_slice((size_t)2400U, self[0U], uint8_t, Eurydice_slice), + mid, + uint8_t, + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); +} + +void +libcrux_kyber_serialize_deserialize_then_decompress_ring_element_u___10size_t( + Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t uu____0[256U]; + libcrux_kyber_serialize_deserialize_then_decompress_10(serialized, uu____0); + memcpy(ret, uu____0, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_ntt_ntt_vector_u___10size_t(int32_t re[256U], int32_t ret[256U]) +{ + size_t zeta_i = (size_t)0U; + libcrux_kyber_ntt_ntt_at_layer_3328(&zeta_i, re, (size_t)7U, re); + libcrux_kyber_ntt_ntt_at_layer_3328(&zeta_i, re, (size_t)6U, re); + libcrux_kyber_ntt_ntt_at_layer_3328(&zeta_i, re, (size_t)5U, re); + libcrux_kyber_ntt_ntt_at_layer_3328(&zeta_i, re, (size_t)4U, re); + libcrux_kyber_ntt_ntt_at_layer_3328(&zeta_i, re, (size_t)3U, re); + libcrux_kyber_ntt_ntt_at_layer_3328(&zeta_i, re, (size_t)2U, re); + libcrux_kyber_ntt_ntt_at_layer_3328(&zeta_i, re, (size_t)1U, re); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_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__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; + int32_t uu____1 = libcrux_kyber_arithmetic_barrett_reduce(re[i]); + re[i] = uu____1; + } + } + memcpy(ret, re, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_ind_cpa_deserialize_then_decompress_u___3size_t_1088size_t_10size_t( + uint8_t* ciphertext, + int32_t ret[3U][256U]) +{ + int32_t u_as_ntt[3U][256U]; + for (size_t i = (size_t)0U; i < (size_t)3U; i++) + memcpy( + u_as_ntt[i], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len( + Eurydice_array_to_slice( + (size_t)1088U, ciphertext, uint8_t, Eurydice_slice), + uint8_t, + size_t) / + (LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * + (size_t)10U / (size_t)8U) }), + 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__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 u_bytes = Eurydice_array_to_subslice( + (size_t)1088U, + ciphertext, + ((core_ops_range_Range__size_t){ + .start = i * (LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * + (size_t)10U / (size_t)8U), + .end = i * (LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * + (size_t)10U / (size_t)8U) + + LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT * + (size_t)10U / (size_t)8U }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t u[256U]; + libcrux_kyber_serialize_deserialize_then_decompress_ring_element_u___10size_t( + u_bytes, u); + int32_t uu____1[256U]; + libcrux_kyber_ntt_ntt_vector_u___10size_t(u, uu____1); + 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])); +} + +void +libcrux_kyber_serialize_deserialize_then_decompress_ring_element_v___4size_t( + Eurydice_slice serialized, + int32_t ret[256U]) +{ + int32_t uu____0[256U]; + libcrux_kyber_serialize_deserialize_then_decompress_4(serialized, uu____0); + memcpy(ret, uu____0, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_ind_cpa_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], + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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) / + LIBCRUX_KYBER_CONSTANTS_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__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 * LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT, + .end = i * LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT + + LIBCRUX_KYBER_CONSTANTS_BYTES_PER_RING_ELEMENT }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice); + int32_t uu____1[256U]; + libcrux_kyber_serialize_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])); +} + +void +libcrux_kyber_matrix_compute_message___3size_t(int32_t (*v)[256U], + int32_t (*secret_as_ntt)[256U], + int32_t (*u_as_ntt)[256U], + int32_t ret[256U]) +{ + int32_t result[256U]; + memcpy( + result, + libcrux_kyber_arithmetic__libcrux_kyber__arithmetic__PolynomialRingElement__ZERO, + (size_t)256U * sizeof(int32_t)); + core_ops_range_Range__size_t iter = core_iter_traits_collect__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____0 = + core_iter_range__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; + int32_t product[256U]; + libcrux_kyber_ntt_ntt_multiply(&secret_as_ntt[i], &u_as_ntt[i], product); + libcrux_kyber_arithmetic_add_to_ring_element___3size_t( + result, &product, result); + } + } + libcrux_kyber_ntt_invert_ntt_montgomery___3size_t(result, result); + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = LIBCRUX_KYBER_CONSTANTS_COEFFICIENTS_IN_RING_ELEMENT }), + core_ops_range_Range__size_t, + core_ops_range_Range__size_t); + while (true) { + core_option_Option__size_t uu____1 = + core_iter_range__core__ops__range__Range_A__3__next( + &iter0, size_t, core_option_Option__size_t); + if (uu____1.tag == core_option_None) + break; + else { + size_t i = uu____1.f0; + int32_t coefficient_normal_form = + libcrux_kyber_arithmetic_montgomery_reduce(result[i] * (int32_t)1441); + int32_t uu____2 = libcrux_kyber_arithmetic_barrett_reduce( + v[0U][i] - coefficient_normal_form); + result[i] = uu____2; + } + } + memcpy(ret, result, (size_t)256U * sizeof(int32_t)); +} + +void +libcrux_kyber_ind_cpa_decrypt___3size_t_1088size_t_960size_t_10size_t_4size_t( + Eurydice_slice secret_key, + uint8_t* ciphertext, + uint8_t ret[32U]) +{ + int32_t u_as_ntt[3U][256U]; + libcrux_kyber_ind_cpa_deserialize_then_decompress_u___3size_t_1088size_t_10size_t( + ciphertext, u_as_ntt); + int32_t v[256U]; + libcrux_kyber_serialize_deserialize_then_decompress_ring_element_v___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]; + libcrux_kyber_ind_cpa_deserialize_secret_key___3size_t(secret_key, + secret_as_ntt); + int32_t message[256U]; + libcrux_kyber_matrix_compute_message___3size_t( + &v, secret_as_ntt, u_as_ntt, message); + uint8_t ret0[32U]; + libcrux_kyber_serialize_compress_then_serialize_message(message, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} + +void +libcrux_kyber_ind_cpa_into_padded_array___1120size_t(Eurydice_slice slice, + uint8_t ret[1120U]) +{ + uint8_t out[1120U]; + for (size_t i = (size_t)0U; i < (size_t)1120U; i++) + out[i] = 0U; + uint8_t* uu____0 = out; + core_slice___Slice_T___copy_from_slice( + Eurydice_array_to_subslice( + (size_t)1120U, + uu____0, + ((core_ops_range_Range__size_t){ + .start = (size_t)0U, + .end = core_slice___Slice_T___len(slice, uint8_t, size_t) }), + uint8_t, + core_ops_range_Range__size_t, + Eurydice_slice), + 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)); +} + +Eurydice_slice +libcrux_kyber_types__libcrux_kyber__types__KyberCiphertext_SIZE__1__as_ref___1088size_t( + uint8_t (*self)[1088U]) +{ + return Eurydice_array_to_slice( + (size_t)1088U, self[0U], uint8_t, Eurydice_slice); +} + +void +libcrux_kyber_hash_functions_PRF___32size_t(Eurydice_slice input, + uint8_t ret[32U]) +{ + uint8_t ret0[32U]; + libcrux_digest_shake256((size_t)32U, input, ret0, void*); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} + +uint8_t +libcrux_kyber_constant_time_ops_compare_ciphertexts_in_constant_time___1088size_t( + Eurydice_slice lhs, + Eurydice_slice rhs) +{ + uint8_t r = 0U; + core_ops_range_Range__size_t iter = core_iter_traits_collect__I__into_iter( + ((core_ops_range_Range__size_t){ .start = (size_t)0U, + .end = (size_t)1088U }), + 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__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; + uint8_t uu____1 = Eurydice_slice_index(lhs, i, uint8_t, uint8_t); + r = (uint32_t)r | ((uint32_t)uu____1 ^ (uint32_t)Eurydice_slice_index( + rhs, i, uint8_t, uint8_t)); + } + } + return libcrux_kyber_constant_time_ops_is_non_zero(r); +} + +void +libcrux_kyber_decapsulate___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( + uint8_t (*secret_key)[2400U], + uint8_t (*ciphertext)[1088U], + uint8_t ret[32U]) +{ + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t uu____0 = + libcrux_kyber_types__libcrux_kyber__types__KyberPrivateKey_SIZE__12__split_at___2400size_t( + secret_key, (size_t)1152U); + Eurydice_slice ind_cpa_secret_key = uu____0.fst; + Eurydice_slice secret_key0 = uu____0.snd; + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t uu____1 = + core_slice___Slice_T___split_at( + secret_key0, + (size_t)1184U, + uint8_t, + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); + Eurydice_slice ind_cpa_public_key = uu____1.fst; + Eurydice_slice secret_key1 = uu____1.snd; + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t uu____2 = + core_slice___Slice_T___split_at( + secret_key1, + LIBCRUX_KYBER_CONSTANTS_H_DIGEST_SIZE, + uint8_t, + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); + Eurydice_slice ind_cpa_public_key_hash = uu____2.fst; + Eurydice_slice implicit_rejection_value = uu____2.snd; + uint8_t decrypted[32U]; + libcrux_kyber_ind_cpa_decrypt___3size_t_1088size_t_960size_t_10size_t_4size_t( + ind_cpa_secret_key, ciphertext[0U], decrypted); + uint8_t to_hash0[64U]; + libcrux_kyber_ind_cpa_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, + LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE, + uint8_t, + size_t, + Eurydice_slice), + ind_cpa_public_key_hash, + uint8_t, + void*); + uint8_t hashed[64U]; + libcrux_kyber_hash_functions_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____3 = + core_slice___Slice_T___split_at( + Eurydice_array_to_slice((size_t)64U, hashed, uint8_t, Eurydice_slice), + LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE, + uint8_t, + K___Eurydice_slice_uint8_t_Eurydice_slice_uint8_t); + Eurydice_slice shared_secret = uu____3.fst; + Eurydice_slice pseudorandomness = uu____3.snd; + uint8_t to_hash[1120U]; + libcrux_kyber_ind_cpa_into_padded_array___1120size_t(implicit_rejection_value, + to_hash); + Eurydice_slice uu____4 = + Eurydice_array_to_subslice_from((size_t)1120U, + to_hash, + LIBCRUX_KYBER_CONSTANTS_SHARED_SECRET_SIZE, + uint8_t, + size_t, + Eurydice_slice); + core_slice___Slice_T___copy_from_slice( + uu____4, + libcrux_kyber_types__libcrux_kyber__types__KyberCiphertext_SIZE__1__as_ref___1088size_t( + ciphertext), + uint8_t, + void*); + uint8_t implicit_rejection_shared_secret[32U]; + libcrux_kyber_hash_functions_PRF___32size_t( + Eurydice_array_to_slice((size_t)1120U, to_hash, uint8_t, Eurydice_slice), + implicit_rejection_shared_secret); + Eurydice_slice uu____5 = ind_cpa_public_key; + uint8_t uu____6[32U]; + memcpy(uu____6, decrypted, (size_t)32U * sizeof(uint8_t)); + uint8_t expected_ciphertext[1088U]; + libcrux_kyber_ind_cpa_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( + uu____5, uu____6, pseudorandomness, expected_ciphertext); + Eurydice_slice uu____7 = + libcrux_kyber_types__libcrux_kyber__types__KyberCiphertext_SIZE__1__as_ref___1088size_t( + ciphertext); + uint8_t selector = + libcrux_kyber_constant_time_ops_compare_ciphertexts_in_constant_time___1088size_t( + uu____7, + Eurydice_array_to_slice( + (size_t)1088U, expected_ciphertext, uint8_t, Eurydice_slice)); + Eurydice_slice uu____8 = shared_secret; + uint8_t ret0[32U]; + libcrux_kyber_constant_time_ops_select_shared_secret_in_constant_time( + uu____8, + 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_768(uint8_t (*secret_key)[2400U], + uint8_t (*ciphertext)[1088U], + uint8_t ret[32U]) +{ + uint8_t ret0[32U]; + libcrux_kyber_decapsulate___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( + secret_key, ciphertext, ret0); + memcpy(ret, ret0, (size_t)32U * sizeof(uint8_t)); +} diff --git a/mach b/mach index d5078c23..870ab2fd 100755 --- a/mach +++ b/mach @@ -172,6 +172,7 @@ def build(args): Supported sanitizers: - asan - ubsan + - msan Use an edition if you want a different build. Note that this build will use the MSVC version by default on Windows. diff --git a/tests/kyber.cc b/tests/kyber.cc index cc233186..26714288 100644 --- a/tests/kyber.cc +++ b/tests/kyber.cc @@ -10,6 +10,7 @@ #include #include +#include "Hacl_Hash_SHA3.h" #include "Libcrux_Kem_Kyber_Kyber768.h" #include "util.h" @@ -55,41 +56,173 @@ read_kats(string path) return kats; } +void modify_ciphertext(uint8_t* ciphertext, size_t ciphertext_size) { + uint8_t randomness[3]; + generate_random(randomness, 3); + + uint8_t random_byte = randomness[0]; + if (random_byte == 0) { + random_byte += 1; + } + + uint16_t random_u16 = (randomness[2] << 8) | randomness[1]; + + uint16_t random_position = random_u16 % ciphertext_size; + + ciphertext[random_position] ^= random_byte; +} + +void modify_secret_key(uint8_t* secret_key, size_t secret_key_size, bool modify_implicit_rejection_value) { + uint8_t randomness[3]; + generate_random(randomness, 3); + + uint8_t random_byte = randomness[0]; + if (random_byte == 0) { + random_byte += 1; + } + + uint16_t random_u16 = (randomness[2] << 8) | randomness[1]; + + uint16_t random_position = 0; + + if(modify_implicit_rejection_value == true) { + random_position = (secret_key_size - 32) + (random_u16 % 32); + } else { + random_position = random_u16 % (secret_key_size - 32); + } + + secret_key[random_position] ^= random_byte; +} + +uint8_t* compute_implicit_rejection_shared_secret(uint8_t* ciphertext, size_t ciphertext_size, uint8_t* secret_key, size_t secret_key_size) { + uint8_t* hashInput = new uint8_t[32 + ciphertext_size]; + uint8_t* sharedSecret = new uint8_t[32]; + + std::copy(secret_key + (secret_key_size - 32), secret_key + secret_key_size, hashInput); + std::copy(ciphertext, ciphertext + ciphertext_size, hashInput + 32); + + Hacl_Hash_SHA3_shake256_hacl(32 + ciphertext_size, hashInput, 32, sharedSecret); + + delete [] hashInput; + return sharedSecret; +} + TEST(Kyber768Test, ConsistencyTest) { - uint8_t randomness[64] = { 0 }; + uint8_t randomness[64]; uint8_t publicKey[KYBER768_PUBLICKEYBYTES]; uint8_t secretKey[KYBER768_SECRETKEYBYTES]; - int rv = Libcrux_Kyber768_GenerateKeyPair(publicKey, secretKey, randomness); - EXPECT_EQ(0, rv); + generate_random(randomness, 64); + Libcrux_Kyber768_GenerateKeyPair(publicKey, secretKey, randomness); uint8_t ciphertext[KYBER768_CIPHERTEXTBYTES]; uint8_t sharedSecret[KYBER768_SHAREDSECRETBYTES]; - rv = Libcrux_Kyber768_Encapsulate( - ciphertext, sharedSecret, publicKey, randomness); - EXPECT_EQ(0, rv); + generate_random(randomness, 32); + Libcrux_Kyber768_Encapsulate( + ciphertext, sharedSecret, &publicKey, randomness); uint8_t sharedSecret2[KYBER768_SHAREDSECRETBYTES]; - rv = Libcrux_Kyber768_Decapsulate(sharedSecret2, ciphertext, secretKey); - EXPECT_EQ(0, rv); + Libcrux_Kyber768_Decapsulate(sharedSecret2, &ciphertext, &secretKey); EXPECT_EQ(0, memcmp(sharedSecret, sharedSecret2, KYBER768_SHAREDSECRETBYTES)); } +TEST(Kyber768Test, ModifiedCiphertextTest) +{ + uint8_t randomness[64]; + uint8_t publicKey[KYBER768_PUBLICKEYBYTES]; + uint8_t secretKey[KYBER768_SECRETKEYBYTES]; + + generate_random(randomness, 64); + Libcrux_Kyber768_GenerateKeyPair(publicKey, secretKey, randomness); + + uint8_t ciphertext[KYBER768_CIPHERTEXTBYTES]; + uint8_t sharedSecret[KYBER768_SHAREDSECRETBYTES]; + + generate_random(randomness, 32); + Libcrux_Kyber768_Encapsulate( + ciphertext, sharedSecret, &publicKey, randomness); + + uint8_t sharedSecret2[KYBER768_SHAREDSECRETBYTES]; + modify_ciphertext(ciphertext, KYBER768_CIPHERTEXTBYTES); + Libcrux_Kyber768_Decapsulate(sharedSecret2, &ciphertext, &secretKey); + + EXPECT_NE(0, memcmp(sharedSecret, sharedSecret2, KYBER768_SHAREDSECRETBYTES)); + + uint8_t* implicitRejectionSharedSecret = compute_implicit_rejection_shared_secret(ciphertext, KYBER768_CIPHERTEXTBYTES, secretKey, KYBER768_SECRETKEYBYTES); + + EXPECT_EQ(0, memcmp(implicitRejectionSharedSecret, sharedSecret2, KYBER768_SHAREDSECRETBYTES)); + delete [] implicitRejectionSharedSecret; +} + +TEST(Kyber768Test, ModifiedSecretKeyTest) +{ + uint8_t randomness[64]; + uint8_t publicKey[KYBER768_PUBLICKEYBYTES]; + uint8_t secretKey[KYBER768_SECRETKEYBYTES]; + + generate_random(randomness, 64); + Libcrux_Kyber768_GenerateKeyPair(publicKey, secretKey, randomness); + + uint8_t ciphertext[KYBER768_CIPHERTEXTBYTES]; + uint8_t sharedSecret[KYBER768_SHAREDSECRETBYTES]; + + generate_random(randomness, 32); + Libcrux_Kyber768_Encapsulate( + ciphertext, sharedSecret, &publicKey, randomness); + + uint8_t sharedSecret2[KYBER768_SHAREDSECRETBYTES]; + modify_secret_key(secretKey, KYBER768_SECRETKEYBYTES, false); + Libcrux_Kyber768_Decapsulate(sharedSecret2, &ciphertext, &secretKey); + + EXPECT_NE(0, memcmp(sharedSecret, sharedSecret2, KYBER768_SHAREDSECRETBYTES)); + + modify_secret_key(secretKey, KYBER768_SECRETKEYBYTES, true); + Libcrux_Kyber768_Decapsulate(sharedSecret2, &ciphertext, &secretKey); + + uint8_t* implicitRejectionSharedSecret = compute_implicit_rejection_shared_secret(ciphertext, KYBER768_CIPHERTEXTBYTES, secretKey, KYBER768_SECRETKEYBYTES); + EXPECT_EQ(0, memcmp(implicitRejectionSharedSecret, sharedSecret2, KYBER768_SHAREDSECRETBYTES)); + delete [] implicitRejectionSharedSecret; +} + TEST(Kyber768Test, NISTKnownAnswerTest) { auto kats = read_kats("kyber768_nistkats.json"); - uint8_t randomness[64] = { 0 }; - uint8_t publicKey[KYBER768_PUBLICKEYBYTES]; uint8_t secretKey[KYBER768_SECRETKEYBYTES]; for (auto kat : kats) { - int rv = Libcrux_Kyber768_GenerateKeyPair( + Libcrux_Kyber768_GenerateKeyPair( publicKey, secretKey, kat.key_generation_seed.data()); - EXPECT_EQ(0, rv); + uint8_t pk_hash[32]; + Hacl_Hash_SHA3_sha3_256(pk_hash, publicKey, KYBER768_PUBLICKEYBYTES); + EXPECT_EQ(0, + memcmp(pk_hash, kat.sha3_256_hash_of_public_key.data(), 32)); + uint8_t sk_hash[32]; + Hacl_Hash_SHA3_sha3_256(sk_hash, secretKey, KYBER768_SECRETKEYBYTES); + EXPECT_EQ(0, + memcmp(sk_hash, kat.sha3_256_hash_of_secret_key.data(), 32)); + + uint8_t ciphertext[KYBER768_CIPHERTEXTBYTES]; + uint8_t sharedSecret[KYBER768_SHAREDSECRETBYTES]; + Libcrux_Kyber768_Encapsulate( + ciphertext, sharedSecret, &publicKey, kat.encapsulation_seed.data()); + uint8_t ct_hash[32]; + Hacl_Hash_SHA3_sha3_256(ct_hash, ciphertext, KYBER768_CIPHERTEXTBYTES); + EXPECT_EQ(0, + memcmp(ct_hash, kat.sha3_256_hash_of_ciphertext.data(), 32)); + EXPECT_EQ(0, + memcmp(sharedSecret, + kat.shared_secret.data(), + KYBER768_SHAREDSECRETBYTES)); + + uint8_t sharedSecret2[KYBER768_SHAREDSECRETBYTES]; + Libcrux_Kyber768_Decapsulate(sharedSecret2, &ciphertext, &secretKey); + + EXPECT_EQ(0, + memcmp(sharedSecret, sharedSecret2, KYBER768_SHAREDSECRETBYTES)); } } diff --git a/tests/kyber/kyber768_nistkats.json b/tests/kyber/kyber768_nistkats.json index 7b668915..6a819f80 100644 --- a/tests/kyber/kyber768_nistkats.json +++ b/tests/kyber/kyber768_nistkats.json @@ -799,4 +799,4 @@ "sha3_256_hash_of_ciphertext": "17336b9ede3a1c26abe725828a5afbe746035a73dfd4a8fbde5040fbabeb2b8d", "shared_secret": "874ac966970f29935db73c231e71a3559b2504e5446151b99c199276617b3824" } -] \ No newline at end of file +] diff --git a/tools/configure.py b/tools/configure.py index 16df4411..af899874 100644 --- a/tools/configure.py +++ b/tools/configure.py @@ -134,6 +134,7 @@ def __init__( self.tests = self.config["tests"] self.libcrux_tests = self.config["libcrux_tests"] self.benchmarks = self.config["benchmarks"] + self.libcrux_benchmarks = self.config["libcrux_benchmarks"] self.include_paths = [include_dir] # We need the config.h generated by CMake @@ -220,6 +221,11 @@ def __init__( f for files in [self.benchmarks[b] for b in self.benchmarks] for f in files ] + # Flatten benchmark sources + self.libcrux_benchmark_sources = [ + f for files in [self.libcrux_benchmarks[b] for b in self.libcrux_benchmarks] for f in files + ] + # Flatten vale files into a single list for each platform. # This is all or nothing. platforms = {} @@ -353,6 +359,16 @@ def write_cmake_config(self, cmake_config): ) ) + out.write( + "set(LIBCRUX_BENCHMARK_SOURCES\n\t%s\n)\n" + % ( + "\n\t".join( + join("${PROJECT_SOURCE_DIR}", "benchmarks", f) + for f in self.libcrux_benchmark_sources + ).replace("\\", "/") + ) + ) + for os in self.vale_files: out.write( "set(VALE_SOURCES_%s\n\t%s\n)\n"