diff --git a/CMakeLists.txt b/CMakeLists.txt index 3ba0b0cf..752dc8a3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -367,7 +367,7 @@ endif() if(BUILD_LIBCRUX) add_library(libcrux_static STATIC ${LIBCRUX_SOURCES}) if(NOT MSVC) - target_compile_options(libcrux_static PRIVATE -g -Wall -Wextra -pedantic) + target_compile_options(libcrux_static PRIVATE -g -Wall -Wextra -pedantic -Wshadow) endif() endif() diff --git a/libcrux/include/Eurydice.h b/libcrux/include/Eurydice.h index 068068cd..d86dcc05 100644 --- a/libcrux/include/Eurydice.h +++ b/libcrux/include/Eurydice.h @@ -1,7 +1,7 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice ../libcrux_kyber.llbc - F* version: 71f2d632 + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf KaRaMeL version: 8e0595bd */ diff --git a/libcrux/include/libcrux_kyber.h b/libcrux/include/libcrux_kyber.h index f8c8d139..e0050d85 100644 --- a/libcrux/include/libcrux_kyber.h +++ b/libcrux/include/libcrux_kyber.h @@ -1,7 +1,7 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice - ../libcrux_kyber.llbc F* version: 71f2d632 KaRaMeL version: 8e0595bd + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice + ../libcrux_kyber.llbc F* version: d0aa54cf KaRaMeL version: 8e0595bd */ #ifndef __libcrux_kyber_H diff --git a/libcrux/src/Eurydice.c b/libcrux/src/Eurydice.c index 60dd8891..ce09e308 100644 --- a/libcrux/src/Eurydice.c +++ b/libcrux/src/Eurydice.c @@ -1,7 +1,7 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice ../libcrux_kyber.llbc - F* version: 71f2d632 + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf KaRaMeL version: 8e0595bd */ diff --git a/libcrux/src/LowStar_Ignore.c b/libcrux/src/LowStar_Ignore.c index 18728cc7..9dc60087 100644 --- a/libcrux/src/LowStar_Ignore.c +++ b/libcrux/src/LowStar_Ignore.c @@ -1,7 +1,7 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice ../libcrux_kyber.llbc - F* version: 71f2d632 + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice ../libcrux_kyber.llbc + F* version: d0aa54cf KaRaMeL version: 8e0595bd */ diff --git a/libcrux/src/libcrux_kyber.c b/libcrux/src/libcrux_kyber.c index 5a7a4a68..12e04b56 100644 --- a/libcrux/src/libcrux_kyber.c +++ b/libcrux/src/libcrux_kyber.c @@ -1,7 +1,7 @@ /* This file was generated by KaRaMeL - KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice - ../libcrux_kyber.llbc F* version: 71f2d632 KaRaMeL version: 8e0595bd + KaRaMeL invocation: /Users/franziskus/repos/eurydice//eurydice + ../libcrux_kyber.llbc F* version: d0aa54cf KaRaMeL version: 8e0595bd */ #include "libcrux_kyber.h" @@ -514,14 +514,14 @@ libcrux_kyber_ntt_ntt_at_layer(size_t* zeta_i, 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 iter = + 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); while (true) { core_option_Option__size_t uu____1 = - core_iter_range__core__ops__range__Range_A__3__next(&iter, size_t); + core_iter_range__core__ops__range__Range_A__3__next(&iter0, size_t); if (uu____1.tag == core_option_None) break; else { @@ -1008,14 +1008,14 @@ libcrux_kyber_ntt_invert_ntt_at_layer(size_t* zeta_i, 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 iter = + 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); while (true) { core_option_Option__size_t uu____1 = - core_iter_range__core__ops__range__Range_A__3__next(&iter, size_t); + core_iter_range__core__ops__range__Range_A__3__next(&iter0, size_t); if (uu____1.tag == core_option_None) break; else { @@ -2541,14 +2541,14 @@ libcrux_kyber_matrix_sample_matrix_A___3size_t(uint8_t seed[34U], 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 iter0 = + 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); while (true) { core_option_Option__size_t uu____2 = - core_iter_range__core__ops__range__Range_A__3__next(&iter0, size_t); + core_iter_range__core__ops__range__Range_A__3__next(&iter1, size_t); if (uu____2.tag == core_option_None) break; else { @@ -2757,12 +2757,12 @@ libcrux_kyber_matrix_compute_As_plus_e___3size_t(int32_t (*matrix_A)[3U][256U], lit.start = (size_t)0U; lit.end = core_slice___Slice_T___len( Eurydice_array_to_slice((size_t)3U, row, int32_t[256U]), int32_t[256U]); - core_ops_range_Range__size_t iter = + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter(lit, 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_iter_range__core__ops__range__Range_A__3__next(&iter0, size_t); if (uu____1.tag == core_option_None) break; else { @@ -2776,7 +2776,7 @@ libcrux_kyber_matrix_compute_As_plus_e___3size_t(int32_t (*matrix_A)[3U][256U], memcpy(result[i], uu____2, (size_t)256U * sizeof(int32_t)); } } - core_ops_range_Range__size_t iter0 = + core_ops_range_Range__size_t iter1 = core_iter_traits_collect__I__into_iter( ((core_ops_range_Range__size_t){ .start = (size_t)0U, @@ -2784,7 +2784,7 @@ libcrux_kyber_matrix_compute_As_plus_e___3size_t(int32_t (*matrix_A)[3U][256U], 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(&iter0, size_t); + core_iter_range__core__ops__range__Range_A__3__next(&iter1, size_t); if (uu____3.tag == core_option_None) break; else { @@ -2835,10 +2835,10 @@ libcrux_kyber_ind_cpa_serialize_secret_key___3size_t_1152size_t( libcrux_kyber_constants_BYTES_PER_RING_ELEMENT }), uint8_t, core_ops_range_Range__size_t); - uint8_t ret[384U]; - libcrux_kyber_serialize_serialize_uncompressed_ring_element(re, ret); + 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, ret, uint8_t), uint8_t); + uu____1, Eurydice_array_to_slice((size_t)384U, ret0, uint8_t), uint8_t); } } uint8_t uu____2[1152U]; @@ -3262,12 +3262,12 @@ libcrux_kyber_matrix_compute_vector_u___3size_t(int32_t (*a_as_ntt)[3U][256U], lit.start = (size_t)0U; lit.end = core_slice___Slice_T___len( Eurydice_array_to_slice((size_t)3U, row, int32_t[256U]), int32_t[256U]); - core_ops_range_Range__size_t iter = + core_ops_range_Range__size_t iter0 = core_iter_traits_collect__I__into_iter(lit, 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_iter_range__core__ops__range__Range_A__3__next(&iter0, size_t); if (uu____1.tag == core_option_None) break; else { @@ -3284,7 +3284,7 @@ libcrux_kyber_matrix_compute_vector_u___3size_t(int32_t (*a_as_ntt)[3U][256U], 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 iter0 = + core_ops_range_Range__size_t iter1 = core_iter_traits_collect__I__into_iter( ((core_ops_range_Range__size_t){ .start = (size_t)0U, @@ -3292,7 +3292,7 @@ libcrux_kyber_matrix_compute_vector_u___3size_t(int32_t (*a_as_ntt)[3U][256U], 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(&iter0, size_t); + core_iter_range__core__ops__range__Range_A__3__next(&iter1, size_t); if (uu____4.tag == core_option_None) break; else { @@ -3581,11 +3581,11 @@ libcrux_kyber_ind_cpa_compress_then_serialize_u___3size_t_960size_t_10size_t_320 .end = (i + (size_t)1U) * ((size_t)960U / (size_t)3U) }), uint8_t, core_ops_range_Range__size_t); - uint8_t ret[320U]; + uint8_t ret0[320U]; libcrux_kyber_serialize_compress_then_serialize_ring_element_u___10size_t_320size_t( - re, ret); + re, ret0); core_slice___Slice_T___copy_from_slice( - uu____1, Eurydice_array_to_slice((size_t)320U, ret, uint8_t), uint8_t); + uu____1, Eurydice_array_to_slice((size_t)320U, ret0, uint8_t), uint8_t); } } uint8_t uu____2[960U];