diff --git a/flake.lock b/flake.lock index 27e6115a..bb075bd5 100644 --- a/flake.lock +++ b/flake.lock @@ -26,11 +26,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1768082582, - "narHash": "sha256-9H8ggZm5I+A4anR8jQiomkDWCo3WTqIex6ylKNhyvnw=", + "lastModified": 1768319516, + "narHash": "sha256-IXeYc6gPHx2rmtitF00ZLVsMtlNpiufr4Ts6xua2QfI=", "owner": "aeneasverif", "repo": "charon", - "rev": "6c6b93beebaf143d9a6d3ffd0f7fc0ffbf57efe4", + "rev": "051a0322504d97dea97f013be0c70a6b48811bf0", "type": "github" }, "original": { diff --git a/out/test-libcrux-no-const/internal/libcrux_core.h b/out/test-libcrux-no-const/internal/libcrux_core.h index 3e443eb8..451fce32 100644 --- a/out/test-libcrux-no-const/internal/libcrux_core.h +++ b/out/test-libcrux-no-const/internal/libcrux_core.h @@ -17,6 +17,23 @@ extern "C" { #include "../libcrux_core.h" +#define core_option_None 0 +#define core_option_Some 1 + +typedef uint8_t core_option_Option_08_tags; + +/** +A monomorphic instance of core.option.Option +with types size_t + +*/ +typedef struct core_option_Option_08_s +{ + core_option_Option_08_tags tag; + size_t f0; +} +core_option_Option_08; + static inline uint64_t core_num__u64__from_le_bytes(Eurydice_array_u8x8 x0); static inline uint64_t core_num__u64__rotate_left(uint64_t x0, uint32_t x1); @@ -1786,23 +1803,6 @@ with const generics */ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_7d(Eurydice_arr_a0 *a); -/** -A monomorphic instance of Eurydice.array_to_subslice_mut -with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t -with const generics -- N= 72 -*/ -Eurydice_mut_borrow_slice_u8 -Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r); - -/** -A monomorphic instance of Eurydice.slice_subslice_mut -with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t - -*/ -Eurydice_mut_borrow_slice_u8 -Eurydice_slice_subslice_mut_7e(Eurydice_mut_borrow_slice_u8 s, core_ops_range_Range_08 r); - /** A monomorphic instance of core.result.Result with types Eurydice_array_u8x8, core_array_TryFromSliceError @@ -1829,6 +1829,23 @@ with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError */ Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self); +/** +A monomorphic instance of Eurydice.slice_subslice_mut +with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t + +*/ +Eurydice_mut_borrow_slice_u8 +Eurydice_slice_subslice_mut_7e(Eurydice_mut_borrow_slice_u8 s, core_ops_range_Range_08 r); + +/** +A monomorphic instance of Eurydice.array_to_subslice_mut +with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t +with const generics +- N= 72 +*/ +Eurydice_mut_borrow_slice_u8 +Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r); + /** A monomorphic instance of K. with types Eurydice_arr_600, Eurydice_arr_74 diff --git a/out/test-libcrux-no-const/libcrux_core.c b/out/test-libcrux-no-const/libcrux_core.c index 87b64ccc..d473eaca 100644 --- a/out/test-libcrux-no-const/libcrux_core.c +++ b/out/test-libcrux-no-const/libcrux_core.c @@ -2454,21 +2454,24 @@ Eurydice_mut_borrow_slice_u8 Eurydice_array_to_slice_mut_7d(Eurydice_arr_a0 *a) } /** -A monomorphic instance of Eurydice.array_to_subslice_mut -with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t -with const generics -- N= 72 +This function found in impl {core::result::Result[TraitClause@0, TraitClause@1]} */ -Eurydice_mut_borrow_slice_u8 -Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r) +/** +A monomorphic instance of core.result.unwrap_26 +with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError + +*/ +Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self) { - return - ( - KRML_CLITERAL(Eurydice_mut_borrow_slice_u8){ - .ptr = a->data + r.start, - .meta = r.end - r.start - } - ); + if (self.tag == core_result_Ok) + { + return self.val.case_Ok; + } + else + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "unwrap not Ok"); + KRML_HOST_EXIT(255U); + } } /** @@ -2486,23 +2489,20 @@ Eurydice_slice_subslice_mut_7e(Eurydice_mut_borrow_slice_u8 s, core_ops_range_Ra } /** -This function found in impl {core::result::Result[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of core.result.unwrap_26 -with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError - +A monomorphic instance of Eurydice.array_to_subslice_mut +with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t +with const generics +- N= 72 */ -Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self) +Eurydice_mut_borrow_slice_u8 +Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r) { - if (self.tag == core_result_Ok) - { - return self.val.case_Ok; - } - else - { - KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "unwrap not Ok"); - KRML_HOST_EXIT(255U); - } + return + ( + KRML_CLITERAL(Eurydice_mut_borrow_slice_u8){ + .ptr = a->data + r.start, + .meta = r.end - r.start + } + ); } diff --git a/out/test-libcrux-no-const/libcrux_sha3_avx2.c b/out/test-libcrux-no-const/libcrux_sha3_avx2.c index b4861336..80258f75 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_avx2.c +++ b/out/test-libcrux-no-const/libcrux_sha3_avx2.c @@ -276,17 +276,59 @@ load_block_5b(Eurydice_arr_05 *state, Eurydice_arr_7b *blocks, size_t offset) } } +/** +A monomorphic instance of libcrux_sha3.simd.avx2.load_last +with const generics +- RATE= 136 +- DELIMITER= 31 +*/ +static KRML_MUSTINLINE void +load_last_ad(Eurydice_arr_05 *state, Eurydice_arr_7b *blocks, size_t start, size_t len) +{ + Eurydice_arr_1a + buffers = + { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; + KRML_MAYBE_FOR4(i, + (size_t)0U, + (size_t)4U, + (size_t)1U, + size_t i0 = i; + Eurydice_slice_copy(Eurydice_array_to_subslice_mut_361(&buffers.data[i0], + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), + Eurydice_slice_subslice_mut_7e(blocks->data[i0], + (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), + uint8_t); + buffers.data[i0].data[len] = 31U; + size_t uu____0 = i0; + size_t uu____1 = (size_t)136U - (size_t)1U; + buffers.data[uu____0].data[uu____1] = (uint32_t)buffers.data[uu____0].data[uu____1] | 128U;); + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_7b + lvalue = + { + .data = { + Eurydice_array_to_slice_mut_d4(buffers.data), + Eurydice_array_to_slice_mut_d4(&buffers.data[1U]), + Eurydice_array_to_slice_mut_d4(&buffers.data[2U]), + Eurydice_array_to_slice_mut_d4(&buffers.data[3U]) + } + }; + load_block_5b(state, &lvalue, (size_t)0U); +} + /** This function found in impl {libcrux_sha3::traits::Absorb<4usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::avx2::{libcrux_sha3::traits::KeccakItem<4usize> for core::core_arch::x86::__m256i}]} */ /** -A monomorphic instance of libcrux_sha3.simd.avx2.load_block_8f +A monomorphic instance of libcrux_sha3.simd.avx2.load_last_8f with const generics - RATE= 136 +- DELIMITER= 31 */ -static void load_block_8f_5b(Eurydice_arr_05 *self, Eurydice_arr_7b *input, size_t start) +static void +load_last_8f_ad(Eurydice_arr_05 *self, Eurydice_arr_7b *input, size_t start, size_t len) { - load_block_5b(self, input, start); + load_last_ad(self, input, start, len); } /** @@ -1599,24 +1641,45 @@ with const generics static KRML_MUSTINLINE void chi_80_a6(Eurydice_arr_05 *self) { Eurydice_arr_05 old = self[0U]; - KRML_MAYBE_FOR5(i0, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t i1 = i0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - set_80_a6(self, - i1, - j, - and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) + { + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + return; + } + else + { + size_t i0 = uu____0.f0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + set_80_a6(self, + i0, + j, + and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1660,78 +1723,6 @@ static KRML_MUSTINLINE void keccakf1600_80_a6(Eurydice_arr_05 *self) } } -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types core_core_arch_x86___m256i -with const generics -- N= 4 -- RATE= 136 -*/ -static KRML_MUSTINLINE void -absorb_block_80_97(Eurydice_arr_05 *self, Eurydice_arr_7b *blocks, size_t start) -{ - load_block_8f_5b(self, blocks, start); - keccakf1600_80_a6(self); -} - -/** -A monomorphic instance of libcrux_sha3.simd.avx2.load_last -with const generics -- RATE= 136 -- DELIMITER= 31 -*/ -static KRML_MUSTINLINE void -load_last_ad(Eurydice_arr_05 *state, Eurydice_arr_7b *blocks, size_t start, size_t len) -{ - Eurydice_arr_1a - buffers = - { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; - KRML_MAYBE_FOR4(i, - (size_t)0U, - (size_t)4U, - (size_t)1U, - size_t i0 = i; - Eurydice_slice_copy(Eurydice_array_to_subslice_mut_361(&buffers.data[i0], - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), - Eurydice_slice_subslice_mut_7e(blocks->data[i0], - (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), - uint8_t); - buffers.data[i0].data[len] = 31U; - size_t uu____0 = i0; - size_t uu____1 = (size_t)136U - (size_t)1U; - buffers.data[uu____0].data[uu____1] = (uint32_t)buffers.data[uu____0].data[uu____1] | 128U;); - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_7b - lvalue = - { - .data = { - Eurydice_array_to_slice_mut_d4(buffers.data), - Eurydice_array_to_slice_mut_d4(&buffers.data[1U]), - Eurydice_array_to_slice_mut_d4(&buffers.data[2U]), - Eurydice_array_to_slice_mut_d4(&buffers.data[3U]) - } - }; - load_block_5b(state, &lvalue, (size_t)0U); -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<4usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::avx2::{libcrux_sha3::traits::KeccakItem<4usize> for core::core_arch::x86::__m256i}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.avx2.load_last_8f -with const generics -- RATE= 136 -- DELIMITER= 31 -*/ -static void -load_last_8f_ad(Eurydice_arr_05 *self, Eurydice_arr_7b *input, size_t start, size_t len) -{ - load_last_ad(self, input, start, len); -} - /** This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ @@ -1767,181 +1758,222 @@ store_block_5b( ) { size_t chunks = len / (size_t)32U; - for (size_t i = (size_t)0U; i < chunks; i++) - { - size_t i4 = i; - size_t i0 = (size_t)4U * i4 / (size_t)5U; - size_t j0 = (size_t)4U * i4 % (size_t)5U; - size_t i1 = ((size_t)4U * i4 + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i4 + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i4 + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i4 + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i4 + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i4 + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v3); - } - size_t rem = len % (size_t)32U; - if (rem > (size_t)0U) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = chunks } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t start0 = start + (size_t)32U * chunks; - Eurydice_arr_60 u8s = { .data = { 0U } }; - size_t chunks8 = rem / (size_t)8U; - for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t k = i0; - size_t i = ((size_t)4U * chunks + k) / (size_t)5U; - size_t j = ((size_t)4U * chunks + k) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____0 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____0, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), - uint8_t); + size_t rem = len % (size_t)32U; + if (rem > (size_t)0U) + { + size_t start0 = start + (size_t)32U * chunks; + Eurydice_arr_60 u8s = { .data = { 0U } }; + size_t chunks8 = rem / (size_t)8U; + for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + { + size_t k = i0; + size_t i = ((size_t)4U * chunks + k) / (size_t)5U; + size_t j = ((size_t)4U * chunks + k) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), + uint8_t); + } + size_t rem8 = rem % (size_t)8U; + if (rem8 > (size_t)0U) + { + size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; + size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____2 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____2, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)8U, + .end = (size_t)8U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)16U, + .end = (size_t)16U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)24U, + .end = (size_t)24U + rem + } + )), + uint8_t); + } + return; + } + else + { + return; + } } - size_t rem8 = rem % (size_t)8U; - if (rem8 > (size_t)0U) + else { - size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; - size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)8U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)16U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)24U + rem })), - uint8_t); + v3); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1966,6 +1998,36 @@ squeeze4_17_5b( store_block_5b(self, out0, out1, out2, out3, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<4usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::avx2::{libcrux_sha3::traits::KeccakItem<4usize> for core::core_arch::x86::__m256i}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.avx2.load_block_8f +with const generics +- RATE= 136 +*/ +static void load_block_8f_5b(Eurydice_arr_05 *self, Eurydice_arr_7b *input, size_t start) +{ + load_block_5b(self, input, start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types core_core_arch_x86___m256i +with const generics +- N= 4 +- RATE= 136 +*/ +static KRML_MUSTINLINE void +absorb_block_80_97(Eurydice_arr_05 *self, Eurydice_arr_7b *blocks, size_t start) +{ + load_block_8f_5b(self, blocks, start); + keccakf1600_80_a6(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.simd256.keccak4 with const generics @@ -1983,35 +2045,61 @@ keccak4_ad( { Eurydice_arr_05 s = new_80_a6(); size_t data_len = data->data->meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)136U; i++) - { - size_t i0 = i; - absorb_block_80_97(&s, data, i0 * (size_t)136U); - } - size_t rem = data_len % (size_t)136U; - absorb_final_80_fb(&s, data, data_len - rem, rem); - size_t outlen = out0.meta; - size_t blocks = outlen / (size_t)136U; - size_t last = outlen - outlen % (size_t)136U; - if (blocks == (size_t)0U) - { - squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)136U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, (size_t)136U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - keccakf1600_80_a6(&s); - squeeze4_17_5b(&s, out0, out1, out2, out3, i0 * (size_t)136U, (size_t)136U); + size_t rem = data_len % (size_t)136U; + absorb_final_80_fb(&s, data, data_len - rem, rem); + size_t outlen = out0.meta; + size_t blocks = outlen / (size_t)136U; + size_t last = outlen - outlen % (size_t)136U; + if (blocks == (size_t)0U) + { + squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, outlen); + return; + } + else + { + squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, (size_t)136U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + keccakf1600_80_a6(&s); + squeeze4_17_5b(&s, out0, out1, out2, out3, i0 * (size_t)136U, (size_t)136U); + } + if (last < outlen) + { + keccakf1600_80_a6(&s); + squeeze4_17_5b(&s, out0, out1, out2, out3, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - keccakf1600_80_a6(&s); - squeeze4_17_5b(&s, out0, out1, out2, out3, last, outlen - last); + size_t i = uu____0.f0; + absorb_block_80_97(&s, data, i * (size_t)136U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2285,181 +2373,222 @@ store_block_3a( ) { size_t chunks = len / (size_t)32U; - for (size_t i = (size_t)0U; i < chunks; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = chunks } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i4 = i; - size_t i0 = (size_t)4U * i4 / (size_t)5U; - size_t j0 = (size_t)4U * i4 % (size_t)5U; - size_t i1 = ((size_t)4U * i4 + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i4 + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i4 + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i4 + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i4 + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i4 + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v3); - } - size_t rem = len % (size_t)32U; - if (rem > (size_t)0U) - { - size_t start0 = start + (size_t)32U * chunks; - Eurydice_arr_60 u8s = { .data = { 0U } }; - size_t chunks8 = rem / (size_t)8U; - for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t k = i0; - size_t i = ((size_t)4U * chunks + k) / (size_t)5U; - size_t j = ((size_t)4U * chunks + k) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____0 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____0, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), - uint8_t); + size_t rem = len % (size_t)32U; + if (rem > (size_t)0U) + { + size_t start0 = start + (size_t)32U * chunks; + Eurydice_arr_60 u8s = { .data = { 0U } }; + size_t chunks8 = rem / (size_t)8U; + for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + { + size_t k = i0; + size_t i = ((size_t)4U * chunks + k) / (size_t)5U; + size_t j = ((size_t)4U * chunks + k) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), + uint8_t); + } + size_t rem8 = rem % (size_t)8U; + if (rem8 > (size_t)0U) + { + size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; + size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____2 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____2, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)8U, + .end = (size_t)8U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)16U, + .end = (size_t)16U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_mut_365(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)24U, + .end = (size_t)24U + rem + } + )), + uint8_t); + } + return; + } + else + { + return; + } } - size_t rem8 = rem % (size_t)8U; - if (rem8 > (size_t)0U) + else { - size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; - size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)8U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)16U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_mut_365(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)24U + rem })), - uint8_t); + v3); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** diff --git a/out/test-libcrux-no-const/libcrux_sha3_portable.c b/out/test-libcrux-no-const/libcrux_sha3_portable.c index a571c14e..3993f003 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_portable.c +++ b/out/test-libcrux-no-const/libcrux_sha3_portable.c @@ -158,49 +158,104 @@ libcrux_sha3_simd_portable_load_block_f8( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)72U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)72U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)72U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)72U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); +} + +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_last +with const generics +- RATE= 72 +- DELIMITER= 6 +*/ +KRML_MUSTINLINE void +libcrux_sha3_simd_portable_load_last_96( + Eurydice_arr_26 *state, + Eurydice_mut_borrow_slice_u8 blocks, + size_t start, + size_t len +) +{ + Eurydice_arr_a0 buffer = { .data = { 0U } }; + Eurydice_slice_copy(Eurydice_array_to_subslice_mut_36(&buffer, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), + uint8_t); + buffer.data[len] = 6U; + size_t uu____0 = (size_t)72U - (size_t)1U; + buffer.data[uu____0] = (uint32_t)buffer.data[uu____0] | 128U; + libcrux_sha3_simd_portable_load_block_f8(state, + Eurydice_array_to_slice_mut_7d(&buffer), + (size_t)0U); } /** This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 with const generics - RATE= 72 +- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_block_a1_f8( +libcrux_sha3_simd_portable_load_last_a1_96( Eurydice_arr_26 *self, Eurydice_arr_f9 *input, - size_t start + size_t start, + size_t len ) { - libcrux_sha3_simd_portable_load_block_f8(self, input->data[0U], start); + libcrux_sha3_simd_portable_load_last_96(self, input->data[0U], start, len); } /** @@ -1510,25 +1565,46 @@ with const generics KRML_MUSTINLINE void libcrux_sha3_generic_keccak_chi_80_04(Eurydice_arr_26 *self) { Eurydice_arr_26 old = self[0U]; - KRML_MAYBE_FOR5(i0, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t i1 = i0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - libcrux_sha3_generic_keccak_set_80_04(self, - i1, - j, - libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) + { + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + return; + } + else + { + size_t i0 = uu____0.f0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + libcrux_sha3_generic_keccak_set_80_04(self, + i0, + j, + libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1572,75 +1648,6 @@ KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccakf1600_80_04(Eurydice_arr_ } } -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 72 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c6( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_f8(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); -} - -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_last -with const generics -- RATE= 72 -- DELIMITER= 6 -*/ -KRML_MUSTINLINE void -libcrux_sha3_simd_portable_load_last_96( - Eurydice_arr_26 *state, - Eurydice_mut_borrow_slice_u8 blocks, - size_t start, - size_t len -) -{ - Eurydice_arr_a0 buffer = { .data = { 0U } }; - Eurydice_slice_copy(Eurydice_array_to_subslice_mut_36(&buffer, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), - uint8_t); - buffer.data[len] = 6U; - size_t uu____0 = (size_t)72U - (size_t)1U; - buffer.data[uu____0] = (uint32_t)buffer.data[uu____0] | 128U; - libcrux_sha3_simd_portable_load_block_f8(state, - Eurydice_array_to_slice_mut_7d(&buffer), - (size_t)0U); -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 -with const generics -- RATE= 72 -- DELIMITER= 6 -*/ -void -libcrux_sha3_simd_portable_load_last_a1_96( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, - size_t start, - size_t len -) -{ - libcrux_sha3_simd_portable_load_last_96(self, input->data[0U], start, len); -} - /** This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ @@ -1742,6 +1749,45 @@ libcrux_sha3_simd_portable_squeeze_13_f8( libcrux_sha3_simd_portable_store_block_f8(self, out, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 72 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_f8( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *input, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_f8(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 72 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c6( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_f8(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -1756,39 +1802,62 @@ libcrux_sha3_generic_keccak_portable_keccak1_96( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)72U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i0 * (size_t)72U); - } - size_t rem = data_len % (size_t)72U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)72U; - size_t last = outlen - outlen % (size_t)72U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = data_len / (size_t)72U } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, (size_t)72U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, i0 * (size_t)72U, (size_t)72U); + size_t rem = data_len % (size_t)72U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)72U; + size_t last = outlen - outlen % (size_t)72U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, (size_t)72U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, i0 * (size_t)72U, (size_t)72U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i * (size_t)72U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1816,70 +1885,56 @@ libcrux_sha3_simd_portable_load_block_5b( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)136U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 136 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_5b( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_5b(self, input->data[0U], start); -} - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 136 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c60( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_5b(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2032,52 +2087,117 @@ libcrux_sha3_simd_portable_squeeze_13_5b( } /** -A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 with const generics - RATE= 136 -- DELIM= 6 */ -inline void -libcrux_sha3_generic_keccak_portable_keccak1_ad( - Eurydice_mut_borrow_slice_u8 data, - Eurydice_mut_borrow_slice_u8 out +void +libcrux_sha3_simd_portable_load_block_a1_5b( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *input, + size_t start ) { - Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); - size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)136U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i0 * (size_t)136U); - } - size_t rem = data_len % (size_t)136U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e0(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)136U; - size_t last = outlen - outlen % (size_t)136U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - } - else + libcrux_sha3_simd_portable_load_block_5b(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 136 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c60( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_5b(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + +/** +A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 +with const generics +- RATE= 136 +- DELIM= 6 +*/ +inline void +libcrux_sha3_generic_keccak_portable_keccak1_ad( + Eurydice_mut_borrow_slice_u8 data, + Eurydice_mut_borrow_slice_u8 out +) +{ + Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); + size_t data_len = data.meta; + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)136U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + size_t rem = data_len % (size_t)136U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e0(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)136U; + size_t last = outlen - outlen % (size_t)136U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2177,39 +2297,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad0( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)136U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i0 * (size_t)136U); - } - size_t rem = data_len % (size_t)136U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e1(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)136U; - size_t last = outlen - outlen % (size_t)136U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)136U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + size_t rem = data_len % (size_t)136U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e1(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)136U; + size_t last = outlen - outlen % (size_t)136U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2245,31 +2391,56 @@ libcrux_sha3_simd_portable_load_block_3a( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)168U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2544,70 +2715,56 @@ libcrux_sha3_simd_portable_load_block_2c( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)144U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)144U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)144U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)144U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 144 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_2c( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_2c(self, input->data[0U], start); -} - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 144 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c61( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_2c(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2759,6 +2916,45 @@ libcrux_sha3_simd_portable_squeeze_13_2c( libcrux_sha3_simd_portable_store_block_2c(self, out, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 144 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_2c( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *input, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_2c(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 144 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c61( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_2c(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -2773,39 +2969,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_1e( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)144U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i0 * (size_t)144U); - } - size_t rem = data_len % (size_t)144U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e3(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)144U; - size_t last = outlen - outlen % (size_t)144U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)144U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, (size_t)144U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, i0 * (size_t)144U, (size_t)144U); + size_t rem = data_len % (size_t)144U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e3(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)144U; + size_t last = outlen - outlen % (size_t)144U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, (size_t)144U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, i0 * (size_t)144U, (size_t)144U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i * (size_t)144U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2833,70 +3055,56 @@ libcrux_sha3_simd_portable_load_block_7a( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)104U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)104U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_mut_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)104U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)104U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_mut_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 104 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_7a( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_7a(self, input->data[0U], start); -} - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 104 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c62( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_7a(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -3048,6 +3256,45 @@ libcrux_sha3_simd_portable_squeeze_13_7a( libcrux_sha3_simd_portable_store_block_7a(self, out, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 104 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_7a( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *input, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_7a(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 104 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c62( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_7a(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -3062,39 +3309,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_7c( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)104U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i0 * (size_t)104U); - } - size_t rem = data_len % (size_t)104U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e4(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)104U; - size_t last = outlen - outlen % (size_t)104U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)104U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, (size_t)104U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, i0 * (size_t)104U, (size_t)104U); + size_t rem = data_len % (size_t)104U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e4(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)104U; + size_t last = outlen - outlen % (size_t)104U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, (size_t)104U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, i0 * (size_t)104U, (size_t)104U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i * (size_t)104U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -3253,39 +3526,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_c6( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)168U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i0 * (size_t)168U); - } - size_t rem = data_len % (size_t)168U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_f9 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e2(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)168U; - size_t last = outlen - outlen % (size_t)168U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)168U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, (size_t)168U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, i0 * (size_t)168U, (size_t)168U); + size_t rem = data_len % (size_t)168U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e2(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)168U; + size_t last = outlen - outlen % (size_t)168U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, (size_t)168U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, i0 * (size_t)168U, (size_t)168U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_f9 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i * (size_t)168U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** diff --git a/out/test-libcrux-no-const/libcrux_sha3_portable.h b/out/test-libcrux-no-const/libcrux_sha3_portable.h index c232de99..5557c9f8 100644 --- a/out/test-libcrux-no-const/libcrux_sha3_portable.h +++ b/out/test-libcrux-no-const/libcrux_sha3_portable.h @@ -127,19 +127,35 @@ libcrux_sha3_simd_portable_load_block_f8( size_t start ); +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_last +with const generics +- RATE= 72 +- DELIMITER= 6 +*/ +void +libcrux_sha3_simd_portable_load_last_96( + Eurydice_arr_26 *state, + Eurydice_mut_borrow_slice_u8 blocks, + size_t start, + size_t len +); + /** This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 with const generics - RATE= 72 +- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_block_a1_f8( +libcrux_sha3_simd_portable_load_last_a1_96( Eurydice_arr_26 *self, Eurydice_arr_f9 *input, - size_t start + size_t start, + size_t len ); /** @@ -875,96 +891,80 @@ void libcrux_sha3_generic_keccak_keccakf1600_80_04(Eurydice_arr_26 *self); This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_80 with types uint64_t with const generics - N= 1 - RATE= 72 +- DELIM= 6 */ void -libcrux_sha3_generic_keccak_absorb_block_80_c6( +libcrux_sha3_generic_keccak_absorb_final_80_9e( Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start + Eurydice_arr_f9 *last, + size_t start, + size_t len ); /** -A monomorphic instance of libcrux_sha3.simd.portable.load_last +A monomorphic instance of libcrux_sha3.simd.portable.store_block with const generics - RATE= 72 -- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_last_96( - Eurydice_arr_26 *state, - Eurydice_mut_borrow_slice_u8 blocks, +libcrux_sha3_simd_portable_store_block_f8( + Eurydice_arr_26 *s, + Eurydice_mut_borrow_slice_u8 out, size_t start, size_t len ); /** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +This function found in impl {libcrux_sha3::traits::Squeeze1 for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 +A monomorphic instance of libcrux_sha3.simd.portable.squeeze_13 with const generics - RATE= 72 -- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_last_a1_96( +libcrux_sha3_simd_portable_squeeze_13_f8( Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, + Eurydice_mut_borrow_slice_u8 out, size_t start, size_t len ); /** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_80 -with types uint64_t +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 with const generics -- N= 1 - RATE= 72 -- DELIM= 6 */ void -libcrux_sha3_generic_keccak_absorb_final_80_9e( +libcrux_sha3_simd_portable_load_block_a1_f8( Eurydice_arr_26 *self, - Eurydice_arr_f9 *last, - size_t start, - size_t len -); - -/** -A monomorphic instance of libcrux_sha3.simd.portable.store_block -with const generics -- RATE= 72 -*/ -void -libcrux_sha3_simd_portable_store_block_f8( - Eurydice_arr_26 *s, - Eurydice_mut_borrow_slice_u8 out, - size_t start, - size_t len + Eurydice_arr_f9 *input, + size_t start ); /** -This function found in impl {libcrux_sha3::traits::Squeeze1 for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.squeeze_13 +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t with const generics +- N= 1 - RATE= 72 */ void -libcrux_sha3_simd_portable_squeeze_13_f8( +libcrux_sha3_generic_keccak_absorb_block_80_c6( Eurydice_arr_26 *self, - Eurydice_mut_borrow_slice_u8 out, - size_t start, - size_t len + Eurydice_arr_f9 *blocks, + size_t start ); /** @@ -1000,38 +1000,6 @@ libcrux_sha3_simd_portable_load_block_5b( size_t start ); -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 136 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_5b( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, - size_t start -); - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 136 -*/ -void -libcrux_sha3_generic_keccak_absorb_block_80_c60( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start -); - /** A monomorphic instance of libcrux_sha3.simd.portable.load_last with const generics @@ -1111,6 +1079,38 @@ libcrux_sha3_simd_portable_squeeze_13_5b( size_t len ); +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 136 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_5b( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *input, + size_t start +); + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 136 +*/ +void +libcrux_sha3_generic_keccak_absorb_block_80_c60( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *blocks, + size_t start +); + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -1389,38 +1389,6 @@ libcrux_sha3_simd_portable_load_block_2c( size_t start ); -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 144 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_2c( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, - size_t start -); - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 144 -*/ -void -libcrux_sha3_generic_keccak_absorb_block_80_c61( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start -); - /** A monomorphic instance of libcrux_sha3.simd.portable.load_last with const generics @@ -1500,6 +1468,38 @@ libcrux_sha3_simd_portable_squeeze_13_2c( size_t len ); +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 144 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_2c( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *input, + size_t start +); + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 144 +*/ +void +libcrux_sha3_generic_keccak_absorb_block_80_c61( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *blocks, + size_t start +); + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -1533,38 +1533,6 @@ libcrux_sha3_simd_portable_load_block_7a( size_t start ); -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 104 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_7a( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *input, - size_t start -); - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 104 -*/ -void -libcrux_sha3_generic_keccak_absorb_block_80_c62( - Eurydice_arr_26 *self, - Eurydice_arr_f9 *blocks, - size_t start -); - /** A monomorphic instance of libcrux_sha3.simd.portable.load_last with const generics @@ -1644,6 +1612,38 @@ libcrux_sha3_simd_portable_squeeze_13_7a( size_t len ); +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 104 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_7a( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *input, + size_t start +); + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 104 +*/ +void +libcrux_sha3_generic_keccak_absorb_block_80_c62( + Eurydice_arr_26 *self, + Eurydice_arr_f9 *blocks, + size_t start +); + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics diff --git a/out/test-libcrux/internal/libcrux_core.h b/out/test-libcrux/internal/libcrux_core.h index dc9c0e79..0d37e12a 100644 --- a/out/test-libcrux/internal/libcrux_core.h +++ b/out/test-libcrux/internal/libcrux_core.h @@ -17,6 +17,23 @@ extern "C" { #include "../libcrux_core.h" +#define core_option_None 0 +#define core_option_Some 1 + +typedef uint8_t core_option_Option_08_tags; + +/** +A monomorphic instance of core.option.Option +with types size_t + +*/ +typedef struct core_option_Option_08_s +{ + core_option_Option_08_tags tag; + size_t f0; +} +core_option_Option_08; + static inline uint64_t core_num__u64__from_le_bytes(Eurydice_array_u8x8 x0); static inline uint64_t core_num__u64__rotate_left(uint64_t x0, uint32_t x1); @@ -2017,23 +2034,6 @@ with const generics */ Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_7d(const Eurydice_arr_a0 *a); -/** -A monomorphic instance of Eurydice.array_to_subslice_mut -with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t -with const generics -- N= 72 -*/ -Eurydice_mut_borrow_slice_u8 -Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r); - -/** -A monomorphic instance of Eurydice.slice_subslice_shared -with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t - -*/ -Eurydice_borrow_slice_u8 -Eurydice_slice_subslice_shared_7e(Eurydice_borrow_slice_u8 s, core_ops_range_Range_08 r); - /** A monomorphic instance of core.result.Result with types Eurydice_array_u8x8, core_array_TryFromSliceError @@ -2060,6 +2060,23 @@ with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError */ Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self); +/** +A monomorphic instance of Eurydice.slice_subslice_shared +with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t + +*/ +Eurydice_borrow_slice_u8 +Eurydice_slice_subslice_shared_7e(Eurydice_borrow_slice_u8 s, core_ops_range_Range_08 r); + +/** +A monomorphic instance of Eurydice.array_to_subslice_mut +with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t +with const generics +- N= 72 +*/ +Eurydice_mut_borrow_slice_u8 +Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r); + /** A monomorphic instance of K. with types Eurydice_arr_600, Eurydice_arr_74 diff --git a/out/test-libcrux/libcrux_core.c b/out/test-libcrux/libcrux_core.c index a79d95a2..e96433e1 100644 --- a/out/test-libcrux/libcrux_core.c +++ b/out/test-libcrux/libcrux_core.c @@ -2809,21 +2809,24 @@ Eurydice_borrow_slice_u8 Eurydice_array_to_slice_shared_7d(const Eurydice_arr_a0 } /** -A monomorphic instance of Eurydice.array_to_subslice_mut -with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t -with const generics -- N= 72 +This function found in impl {core::result::Result[TraitClause@0, TraitClause@1]} */ -Eurydice_mut_borrow_slice_u8 -Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r) +/** +A monomorphic instance of core.result.unwrap_26 +with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError + +*/ +Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self) { - return - ( - KRML_CLITERAL(Eurydice_mut_borrow_slice_u8){ - .ptr = a->data + r.start, - .meta = r.end - r.start - } - ); + if (self.tag == core_result_Ok) + { + return self.val.case_Ok; + } + else + { + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "unwrap not Ok"); + KRML_HOST_EXIT(255U); + } } /** @@ -2839,23 +2842,20 @@ Eurydice_slice_subslice_shared_7e(Eurydice_borrow_slice_u8 s, core_ops_range_Ran } /** -This function found in impl {core::result::Result[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of core.result.unwrap_26 -with types Eurydice_arr uint8_t[[$8size_t]], core_array_TryFromSliceError - +A monomorphic instance of Eurydice.array_to_subslice_mut +with types uint8_t, core_ops_range_Range size_t, Eurydice_derefed_slice uint8_t +with const generics +- N= 72 */ -Eurydice_array_u8x8 core_result_unwrap_26_ab(core_result_Result_8e self) +Eurydice_mut_borrow_slice_u8 +Eurydice_array_to_subslice_mut_36(Eurydice_arr_a0 *a, core_ops_range_Range_08 r) { - if (self.tag == core_result_Ok) - { - return self.val.case_Ok; - } - else - { - KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "unwrap not Ok"); - KRML_HOST_EXIT(255U); - } + return + ( + KRML_CLITERAL(Eurydice_mut_borrow_slice_u8){ + .ptr = a->data + r.start, + .meta = r.end - r.start + } + ); } diff --git a/out/test-libcrux/libcrux_sha3_avx2.c b/out/test-libcrux/libcrux_sha3_avx2.c index a430cff7..aa69bfe3 100644 --- a/out/test-libcrux/libcrux_sha3_avx2.c +++ b/out/test-libcrux/libcrux_sha3_avx2.c @@ -276,17 +276,59 @@ load_block_5b(Eurydice_arr_05 *state, const Eurydice_arr_cd *blocks, size_t offs } } +/** +A monomorphic instance of libcrux_sha3.simd.avx2.load_last +with const generics +- RATE= 136 +- DELIMITER= 31 +*/ +static KRML_MUSTINLINE void +load_last_ad(Eurydice_arr_05 *state, const Eurydice_arr_cd *blocks, size_t start, size_t len) +{ + Eurydice_arr_1a + buffers = + { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; + KRML_MAYBE_FOR4(i, + (size_t)0U, + (size_t)4U, + (size_t)1U, + size_t i0 = i; + Eurydice_slice_copy(Eurydice_array_to_subslice_mut_360(&buffers.data[i0], + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), + Eurydice_slice_subslice_shared_7e(blocks->data[i0], + (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), + uint8_t); + buffers.data[i0].data[len] = 31U; + size_t uu____0 = i0; + size_t uu____1 = (size_t)136U - (size_t)1U; + buffers.data[uu____0].data[uu____1] = (uint32_t)buffers.data[uu____0].data[uu____1] | 128U;); + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_cd + lvalue = + { + .data = { + Eurydice_array_to_slice_shared_d4(buffers.data), + Eurydice_array_to_slice_shared_d4(&buffers.data[1U]), + Eurydice_array_to_slice_shared_d4(&buffers.data[2U]), + Eurydice_array_to_slice_shared_d4(&buffers.data[3U]) + } + }; + load_block_5b(state, &lvalue, (size_t)0U); +} + /** This function found in impl {libcrux_sha3::traits::Absorb<4usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::avx2::{libcrux_sha3::traits::KeccakItem<4usize> for core::core_arch::x86::__m256i}]} */ /** -A monomorphic instance of libcrux_sha3.simd.avx2.load_block_8f +A monomorphic instance of libcrux_sha3.simd.avx2.load_last_8f with const generics - RATE= 136 +- DELIMITER= 31 */ -static void load_block_8f_5b(Eurydice_arr_05 *self, const Eurydice_arr_cd *input, size_t start) +static void +load_last_8f_ad(Eurydice_arr_05 *self, const Eurydice_arr_cd *input, size_t start, size_t len) { - load_block_5b(self, input, start); + load_last_ad(self, input, start, len); } /** @@ -1599,24 +1641,45 @@ with const generics static KRML_MUSTINLINE void chi_80_a6(Eurydice_arr_05 *self) { Eurydice_arr_05 old = self[0U]; - KRML_MAYBE_FOR5(i0, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t i1 = i0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - set_80_a6(self, - i1, - j, - and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - index_c2_a6(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) + { + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + return; + } + else + { + size_t i0 = uu____0.f0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + set_80_a6(self, + i0, + j, + and_not_xor_b0(index_c2_a6(self, (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + index_c2_a6(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1660,78 +1723,6 @@ static KRML_MUSTINLINE void keccakf1600_80_a6(Eurydice_arr_05 *self) } } -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types core_core_arch_x86___m256i -with const generics -- N= 4 -- RATE= 136 -*/ -static KRML_MUSTINLINE void -absorb_block_80_97(Eurydice_arr_05 *self, const Eurydice_arr_cd *blocks, size_t start) -{ - load_block_8f_5b(self, blocks, start); - keccakf1600_80_a6(self); -} - -/** -A monomorphic instance of libcrux_sha3.simd.avx2.load_last -with const generics -- RATE= 136 -- DELIMITER= 31 -*/ -static KRML_MUSTINLINE void -load_last_ad(Eurydice_arr_05 *state, const Eurydice_arr_cd *blocks, size_t start, size_t len) -{ - Eurydice_arr_1a - buffers = - { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; - KRML_MAYBE_FOR4(i, - (size_t)0U, - (size_t)4U, - (size_t)1U, - size_t i0 = i; - Eurydice_slice_copy(Eurydice_array_to_subslice_mut_360(&buffers.data[i0], - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), - Eurydice_slice_subslice_shared_7e(blocks->data[i0], - (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), - uint8_t); - buffers.data[i0].data[len] = 31U; - size_t uu____0 = i0; - size_t uu____1 = (size_t)136U - (size_t)1U; - buffers.data[uu____0].data[uu____1] = (uint32_t)buffers.data[uu____0].data[uu____1] | 128U;); - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_cd - lvalue = - { - .data = { - Eurydice_array_to_slice_shared_d4(buffers.data), - Eurydice_array_to_slice_shared_d4(&buffers.data[1U]), - Eurydice_array_to_slice_shared_d4(&buffers.data[2U]), - Eurydice_array_to_slice_shared_d4(&buffers.data[3U]) - } - }; - load_block_5b(state, &lvalue, (size_t)0U); -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<4usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::avx2::{libcrux_sha3::traits::KeccakItem<4usize> for core::core_arch::x86::__m256i}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.avx2.load_last_8f -with const generics -- RATE= 136 -- DELIMITER= 31 -*/ -static void -load_last_8f_ad(Eurydice_arr_05 *self, const Eurydice_arr_cd *input, size_t start, size_t len) -{ - load_last_ad(self, input, start, len); -} - /** This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ @@ -1772,181 +1763,222 @@ store_block_5b( ) { size_t chunks = len / (size_t)32U; - for (size_t i = (size_t)0U; i < chunks; i++) - { - size_t i4 = i; - size_t i0 = (size_t)4U * i4 / (size_t)5U; - size_t j0 = (size_t)4U * i4 % (size_t)5U; - size_t i1 = ((size_t)4U * i4 + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i4 + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i4 + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i4 + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i4 + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i4 + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v3); - } - size_t rem = len % (size_t)32U; - if (rem > (size_t)0U) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = chunks } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t start0 = start + (size_t)32U * chunks; - Eurydice_arr_60 u8s = { .data = { 0U } }; - size_t chunks8 = rem / (size_t)8U; - for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t k = i0; - size_t i = ((size_t)4U * chunks + k) / (size_t)5U; - size_t j = ((size_t)4U * chunks + k) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____0 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____0, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), - uint8_t); + size_t rem = len % (size_t)32U; + if (rem > (size_t)0U) + { + size_t start0 = start + (size_t)32U * chunks; + Eurydice_arr_60 u8s = { .data = { 0U } }; + size_t chunks8 = rem / (size_t)8U; + for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + { + size_t k = i0; + size_t i = ((size_t)4U * chunks + k) / (size_t)5U; + size_t j = ((size_t)4U * chunks + k) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), + uint8_t); + } + size_t rem8 = rem % (size_t)8U; + if (rem8 > (size_t)0U) + { + size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; + size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____2 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____2, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)8U, + .end = (size_t)8U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)16U, + .end = (size_t)16U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)24U, + .end = (size_t)24U + rem + } + )), + uint8_t); + } + return; + } + else + { + return; + } } - size_t rem8 = rem % (size_t)8U; - if (rem8 > (size_t)0U) + else { - size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; - size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)8U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)16U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)24U + rem })), - uint8_t); + v3); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1971,6 +2003,36 @@ squeeze4_17_5b( store_block_5b(self, out0, out1, out2, out3, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<4usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::avx2::{libcrux_sha3::traits::KeccakItem<4usize> for core::core_arch::x86::__m256i}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.avx2.load_block_8f +with const generics +- RATE= 136 +*/ +static void load_block_8f_5b(Eurydice_arr_05 *self, const Eurydice_arr_cd *input, size_t start) +{ + load_block_5b(self, input, start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types core_core_arch_x86___m256i +with const generics +- N= 4 +- RATE= 136 +*/ +static KRML_MUSTINLINE void +absorb_block_80_97(Eurydice_arr_05 *self, const Eurydice_arr_cd *blocks, size_t start) +{ + load_block_8f_5b(self, blocks, start); + keccakf1600_80_a6(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.simd256.keccak4 with const generics @@ -1988,35 +2050,61 @@ keccak4_ad( { Eurydice_arr_05 s = new_80_a6(); size_t data_len = data->data->meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)136U; i++) - { - size_t i0 = i; - absorb_block_80_97(&s, data, i0 * (size_t)136U); - } - size_t rem = data_len % (size_t)136U; - absorb_final_80_fb(&s, data, data_len - rem, rem); - size_t outlen = out0.meta; - size_t blocks = outlen / (size_t)136U; - size_t last = outlen - outlen % (size_t)136U; - if (blocks == (size_t)0U) - { - squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)136U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, (size_t)136U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - keccakf1600_80_a6(&s); - squeeze4_17_5b(&s, out0, out1, out2, out3, i0 * (size_t)136U, (size_t)136U); + size_t rem = data_len % (size_t)136U; + absorb_final_80_fb(&s, data, data_len - rem, rem); + size_t outlen = out0.meta; + size_t blocks = outlen / (size_t)136U; + size_t last = outlen - outlen % (size_t)136U; + if (blocks == (size_t)0U) + { + squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, outlen); + return; + } + else + { + squeeze4_17_5b(&s, out0, out1, out2, out3, (size_t)0U, (size_t)136U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + keccakf1600_80_a6(&s); + squeeze4_17_5b(&s, out0, out1, out2, out3, i0 * (size_t)136U, (size_t)136U); + } + if (last < outlen) + { + keccakf1600_80_a6(&s); + squeeze4_17_5b(&s, out0, out1, out2, out3, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - keccakf1600_80_a6(&s); - squeeze4_17_5b(&s, out0, out1, out2, out3, last, outlen - last); + size_t i = uu____0.f0; + absorb_block_80_97(&s, data, i * (size_t)136U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2295,181 +2383,222 @@ store_block_3a( ) { size_t chunks = len / (size_t)32U; - for (size_t i = (size_t)0U; i < chunks; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = chunks } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i4 = i; - size_t i0 = (size_t)4U * i4 / (size_t)5U; - size_t j0 = (size_t)4U * i4 % (size_t)5U; - size_t i1 = ((size_t)4U * i4 + (size_t)1U) / (size_t)5U; - size_t j1 = ((size_t)4U * i4 + (size_t)1U) % (size_t)5U; - size_t i2 = ((size_t)4U * i4 + (size_t)2U) / (size_t)5U; - size_t j2 = ((size_t)4U * i4 + (size_t)2U) % (size_t)5U; - size_t i3 = ((size_t)4U * i4 + (size_t)3U) / (size_t)5U; - size_t j3 = ((size_t)4U * i4 + (size_t)3U) % (size_t)5U; - __m256i - v0l = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v1h = - mm256_permute2x128_si256((int32_t)32, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i - v2l = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i0, j0)[0U], - get_ij_a6(s, i2, j2)[0U], - __m256i); - __m256i - v3h = - mm256_permute2x128_si256((int32_t)49, - get_ij_a6(s, i1, j1)[0U], - get_ij_a6(s, i3, j3)[0U], - __m256i); - __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); - __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); - __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); - __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v0); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v1); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v2); - mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start + (size_t)32U * i4, - .end = start + (size_t)32U * (i4 + (size_t)1U) - } - )), - v3); - } - size_t rem = len % (size_t)32U; - if (rem > (size_t)0U) - { - size_t start0 = start + (size_t)32U * chunks; - Eurydice_arr_60 u8s = { .data = { 0U } }; - size_t chunks8 = rem / (size_t)8U; - for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t k = i0; - size_t i = ((size_t)4U * chunks + k) / (size_t)5U; - size_t j = ((size_t)4U * chunks + k) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____0 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____0, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, - ( - KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + (size_t)8U * k, - .end = start0 + (size_t)8U * (k + (size_t)1U) - } - )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), - uint8_t); + size_t rem = len % (size_t)32U; + if (rem > (size_t)0U) + { + size_t start0 = start + (size_t)32U * chunks; + Eurydice_arr_60 u8s = { .data = { 0U } }; + size_t chunks8 = rem / (size_t)8U; + for (size_t i0 = (size_t)0U; i0 < chunks8; i0++) + { + size_t k = i0; + size_t i = ((size_t)4U * chunks + k) / (size_t)5U; + size_t j = ((size_t)4U * chunks + k) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)8U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)16U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)24U })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + (size_t)8U * k, + .end = start0 + (size_t)8U * (k + (size_t)1U) + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)32U })), + uint8_t); + } + size_t rem8 = rem % (size_t)8U; + if (rem8 > (size_t)0U) + { + size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; + size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; + Eurydice_mut_borrow_slice_u8 uu____2 = Eurydice_array_to_slice_mut_6e(&u8s); + mm256_storeu_si256_u8(uu____2, get_ij_a6(s, i, j)[0U]); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)8U, + .end = (size_t)8U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)16U, + .end = (size_t)16U + rem + } + )), + uint8_t); + Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = start0 + len - rem8, + .end = start0 + len + } + )), + Eurydice_array_to_subslice_shared_360(&u8s, + ( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)24U, + .end = (size_t)24U + rem + } + )), + uint8_t); + } + return; + } + else + { + return; + } } - size_t rem8 = rem % (size_t)8U; - if (rem8 > (size_t)0U) + else { - size_t i = ((size_t)4U * chunks + chunks8) / (size_t)5U; - size_t j = ((size_t)4U * chunks + chunks8) % (size_t)5U; - Eurydice_mut_borrow_slice_u8 uu____1 = Eurydice_array_to_slice_mut_6e(&u8s); - mm256_storeu_si256_u8(uu____1, get_ij_a6(s, i, j)[0U]); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out0, + size_t i = uu____0.f0; + size_t i0 = (size_t)4U * i / (size_t)5U; + size_t j0 = (size_t)4U * i % (size_t)5U; + size_t i1 = ((size_t)4U * i + (size_t)1U) / (size_t)5U; + size_t j1 = ((size_t)4U * i + (size_t)1U) % (size_t)5U; + size_t i2 = ((size_t)4U * i + (size_t)2U) / (size_t)5U; + size_t j2 = ((size_t)4U * i + (size_t)2U) % (size_t)5U; + size_t i3 = ((size_t)4U * i + (size_t)3U) / (size_t)5U; + size_t j3 = ((size_t)4U * i + (size_t)3U) % (size_t)5U; + __m256i + v0l = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v1h = + mm256_permute2x128_si256((int32_t)32, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i + v2l = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i0, j0)[0U], + get_ij_a6(s, i2, j2)[0U], + __m256i); + __m256i + v3h = + mm256_permute2x128_si256((int32_t)49, + get_ij_a6(s, i1, j1)[0U], + get_ij_a6(s, i3, j3)[0U], + __m256i); + __m256i v0 = mm256_unpacklo_epi64(v0l, v1h); + __m256i v1 = mm256_unpackhi_epi64(v0l, v1h); + __m256i v2 = mm256_unpacklo_epi64(v2l, v3h); + __m256i v3 = mm256_unpackhi_epi64(v2l, v3h); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out0, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out1, + v0); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out1, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)8U, .end = (size_t)8U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out2, + v1); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out2, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)16U, .end = (size_t)16U + rem })), - uint8_t); - Eurydice_slice_copy(Eurydice_slice_subslice_mut_7e(out3, + v2); + mm256_storeu_si256_u8(Eurydice_slice_subslice_mut_7e(out3, ( KRML_CLITERAL(core_ops_range_Range_08){ - .start = start0 + len - rem8, - .end = start0 + len + .start = start + (size_t)32U * i, + .end = start + (size_t)32U * (i + (size_t)1U) } )), - Eurydice_array_to_subslice_shared_360(&u8s, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)24U, .end = (size_t)24U + rem })), - uint8_t); + v3); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** diff --git a/out/test-libcrux/libcrux_sha3_portable.c b/out/test-libcrux/libcrux_sha3_portable.c index 233a9b42..7a2aa780 100644 --- a/out/test-libcrux/libcrux_sha3_portable.c +++ b/out/test-libcrux/libcrux_sha3_portable.c @@ -159,49 +159,104 @@ libcrux_sha3_simd_portable_load_block_f8( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)72U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)72U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)72U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)72U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); +} + +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_last +with const generics +- RATE= 72 +- DELIMITER= 6 +*/ +KRML_MUSTINLINE void +libcrux_sha3_simd_portable_load_last_96( + Eurydice_arr_26 *state, + Eurydice_borrow_slice_u8 blocks, + size_t start, + size_t len +) +{ + Eurydice_arr_a0 buffer = { .data = { 0U } }; + Eurydice_slice_copy(Eurydice_array_to_subslice_mut_36(&buffer, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), + uint8_t); + buffer.data[len] = 6U; + size_t uu____0 = (size_t)72U - (size_t)1U; + buffer.data[uu____0] = (uint32_t)buffer.data[uu____0] | 128U; + libcrux_sha3_simd_portable_load_block_f8(state, + Eurydice_array_to_slice_shared_7d(&buffer), + (size_t)0U); } /** This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 with const generics - RATE= 72 +- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_block_a1_f8( +libcrux_sha3_simd_portable_load_last_a1_96( Eurydice_arr_26 *self, const Eurydice_arr_06 *input, - size_t start + size_t start, + size_t len ) { - libcrux_sha3_simd_portable_load_block_f8(self, input->data[0U], start); + libcrux_sha3_simd_portable_load_last_96(self, input->data[0U], start, len); } /** @@ -1513,25 +1568,46 @@ with const generics KRML_MUSTINLINE void libcrux_sha3_generic_keccak_chi_80_04(Eurydice_arr_26 *self) { Eurydice_arr_26 old = self[0U]; - KRML_MAYBE_FOR5(i0, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t i1 = i0; - KRML_MAYBE_FOR5(i, - (size_t)0U, - (size_t)5U, - (size_t)1U, - size_t j = i; - libcrux_sha3_generic_keccak_set_80_04(self, - i1, - j, - libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = j }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], - libcrux_sha3_generic_keccak_index_c2_04(&old, - (KRML_CLITERAL(size_t_x2){ .fst = i1, .snd = (j + (size_t)1U) % (size_t)5U }))[0U])););); + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = (size_t)5U } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) + { + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + return; + } + else + { + size_t i0 = uu____0.f0; + KRML_MAYBE_FOR5(i, + (size_t)0U, + (size_t)5U, + (size_t)1U, + size_t j = i; + libcrux_sha3_generic_keccak_set_80_04(self, + i0, + j, + libcrux_sha3_simd_portable_and_not_xor_d2(libcrux_sha3_generic_keccak_index_c2_04(self, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = j }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)2U) % (size_t)5U }))[0U], + libcrux_sha3_generic_keccak_index_c2_04(&old, + (KRML_CLITERAL(size_t_x2){ .fst = i0, .snd = (j + (size_t)1U) % (size_t)5U }))[0U]));); + } + } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1575,75 +1651,6 @@ KRML_MUSTINLINE void libcrux_sha3_generic_keccak_keccakf1600_80_04(Eurydice_arr_ } } -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 72 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c6( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_f8(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); -} - -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_last -with const generics -- RATE= 72 -- DELIMITER= 6 -*/ -KRML_MUSTINLINE void -libcrux_sha3_simd_portable_load_last_96( - Eurydice_arr_26 *state, - Eurydice_borrow_slice_u8 blocks, - size_t start, - size_t len -) -{ - Eurydice_arr_a0 buffer = { .data = { 0U } }; - Eurydice_slice_copy(Eurydice_array_to_subslice_mut_36(&buffer, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = len })), - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = start, .end = start + len })), - uint8_t); - buffer.data[len] = 6U; - size_t uu____0 = (size_t)72U - (size_t)1U; - buffer.data[uu____0] = (uint32_t)buffer.data[uu____0] | 128U; - libcrux_sha3_simd_portable_load_block_f8(state, - Eurydice_array_to_slice_shared_7d(&buffer), - (size_t)0U); -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 -with const generics -- RATE= 72 -- DELIMITER= 6 -*/ -void -libcrux_sha3_simd_portable_load_last_a1_96( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, - size_t start, - size_t len -) -{ - libcrux_sha3_simd_portable_load_last_96(self, input->data[0U], start, len); -} - /** This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ @@ -1745,6 +1752,45 @@ libcrux_sha3_simd_portable_squeeze_13_f8( libcrux_sha3_simd_portable_store_block_f8(self, out, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 72 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_f8( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *input, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_f8(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 72 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c6( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_f8(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -1759,39 +1805,62 @@ libcrux_sha3_generic_keccak_portable_keccak1_96( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)72U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i0 * (size_t)72U); - } - size_t rem = data_len % (size_t)72U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)72U; - size_t last = outlen - outlen % (size_t)72U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ .start = (size_t)0U, .end = data_len / (size_t)72U } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, (size_t)72U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, i0 * (size_t)72U, (size_t)72U); + size_t rem = data_len % (size_t)72U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)72U; + size_t last = outlen - outlen % (size_t)72U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, (size_t)0U, (size_t)72U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, i0 * (size_t)72U, (size_t)72U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_f8(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c6(&s, &lvalue, i * (size_t)72U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -1819,70 +1888,56 @@ libcrux_sha3_simd_portable_load_block_5b( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)136U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)136U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 136 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_5b( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_5b(self, input->data[0U], start); -} - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 136 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c60( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_5b(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2035,52 +2090,117 @@ libcrux_sha3_simd_portable_squeeze_13_5b( } /** -A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 with const generics - RATE= 136 -- DELIM= 6 */ -inline void -libcrux_sha3_generic_keccak_portable_keccak1_ad( - Eurydice_borrow_slice_u8 data, - Eurydice_mut_borrow_slice_u8 out +void +libcrux_sha3_simd_portable_load_block_a1_5b( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *input, + size_t start ) { - Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); - size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)136U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i0 * (size_t)136U); - } - size_t rem = data_len % (size_t)136U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e0(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)136U; - size_t last = outlen - outlen % (size_t)136U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - } - else + libcrux_sha3_simd_portable_load_block_5b(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 136 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c60( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_5b(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + +/** +A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 +with const generics +- RATE= 136 +- DELIM= 6 +*/ +inline void +libcrux_sha3_generic_keccak_portable_keccak1_ad( + Eurydice_borrow_slice_u8 data, + Eurydice_mut_borrow_slice_u8 out +) +{ + Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); + size_t data_len = data.meta; + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)136U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + size_t rem = data_len % (size_t)136U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e0(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)136U; + size_t last = outlen - outlen % (size_t)136U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2180,39 +2300,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_ad0( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)136U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i0 * (size_t)136U); - } - size_t rem = data_len % (size_t)136U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e1(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)136U; - size_t last = outlen - outlen % (size_t)136U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)136U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + size_t rem = data_len % (size_t)136U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e1(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)136U; + size_t last = outlen - outlen % (size_t)136U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, (size_t)0U, (size_t)136U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, i0 * (size_t)136U, (size_t)136U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_5b(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c60(&s, &lvalue, i * (size_t)136U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2248,31 +2394,56 @@ libcrux_sha3_simd_portable_load_block_3a( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)168U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)168U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2547,70 +2718,56 @@ libcrux_sha3_simd_portable_load_block_2c( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)144U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)144U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)144U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)144U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 144 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_2c( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_2c(self, input->data[0U], start); -} - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 144 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c61( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_2c(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2762,6 +2919,45 @@ libcrux_sha3_simd_portable_squeeze_13_2c( libcrux_sha3_simd_portable_store_block_2c(self, out, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 144 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_2c( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *input, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_2c(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 144 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c61( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_2c(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -2776,39 +2972,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_1e( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)144U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i0 * (size_t)144U); - } - size_t rem = data_len % (size_t)144U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e3(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)144U; - size_t last = outlen - outlen % (size_t)144U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)144U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, (size_t)144U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, i0 * (size_t)144U, (size_t)144U); + size_t rem = data_len % (size_t)144U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e3(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)144U; + size_t last = outlen - outlen % (size_t)144U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, (size_t)0U, (size_t)144U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, i0 * (size_t)144U, (size_t)144U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_2c(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c61(&s, &lvalue, i * (size_t)144U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -2836,70 +3058,56 @@ libcrux_sha3_simd_portable_load_block_7a( ) { Eurydice_arr_26 state_flat = { .data = { 0U } }; - for (size_t i = (size_t)0U; i < (size_t)104U / (size_t)8U; i++) + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = (size_t)104U / (size_t)8U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - size_t i0 = i; - size_t offset = start + (size_t)8U * i0; - Eurydice_array_u8x8 arr; - memcpy(arr.data, - Eurydice_slice_subslice_shared_7e(blocks, - (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, - (size_t)8U * sizeof (uint8_t)); - Eurydice_array_u8x8 + core_option_Option_08 uu____0 = - core_result_unwrap_26_ab(( - KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } - )); - state_flat.data[i0] = core_num__u64__from_le_bytes(uu____0); - } - for (size_t i = (size_t)0U; i < (size_t)104U / (size_t)8U; i++) - { - size_t i0 = i; - libcrux_sha3_traits_set_ij_04(state, - i0 / (size_t)5U, - i0 % (size_t)5U, - libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ - state_flat.data[i0]); + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) + { + for (size_t i = (size_t)0U; i < (size_t)104U / (size_t)8U; i++) + { + size_t i0 = i; + libcrux_sha3_traits_set_ij_04(state, + i0 / (size_t)5U, + i0 % (size_t)5U, + libcrux_sha3_traits_get_ij_04(state, i0 / (size_t)5U, i0 % (size_t)5U)[0U] ^ + state_flat.data[i0]); + } + return; + } + else + { + size_t i = uu____0.f0; + size_t offset = start + (size_t)8U * i; + Eurydice_array_u8x8 arr; + memcpy(arr.data, + Eurydice_slice_subslice_shared_7e(blocks, + (KRML_CLITERAL(core_ops_range_Range_08){ .start = offset, .end = offset + (size_t)8U })).ptr, + (size_t)8U * sizeof (uint8_t)); + Eurydice_array_u8x8 + uu____1 = + core_result_unwrap_26_ab(( + KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } + )); + state_flat.data[i] = core_num__u64__from_le_bytes(uu____1); + } } -} - -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 104 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_7a( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_7a(self, input->data[0U], start); -} - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 104 -*/ -KRML_MUSTINLINE void -libcrux_sha3_generic_keccak_absorb_block_80_c62( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start -) -{ - libcrux_sha3_simd_portable_load_block_a1_7a(self, blocks, start); - libcrux_sha3_generic_keccak_keccakf1600_80_04(self); + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -3051,6 +3259,45 @@ libcrux_sha3_simd_portable_squeeze_13_7a( libcrux_sha3_simd_portable_store_block_7a(self, out, start, len); } +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 104 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_7a( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *input, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_7a(self, input->data[0U], start); +} + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 104 +*/ +KRML_MUSTINLINE void +libcrux_sha3_generic_keccak_absorb_block_80_c62( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start +) +{ + libcrux_sha3_simd_portable_load_block_a1_7a(self, blocks, start); + libcrux_sha3_generic_keccak_keccakf1600_80_04(self); +} + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -3065,39 +3312,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_7c( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)104U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i0 * (size_t)104U); - } - size_t rem = data_len % (size_t)104U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e4(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)104U; - size_t last = outlen - outlen % (size_t)104U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)104U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, (size_t)104U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, i0 * (size_t)104U, (size_t)104U); + size_t rem = data_len % (size_t)104U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e4(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)104U; + size_t last = outlen - outlen % (size_t)104U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, (size_t)0U, (size_t)104U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, i0 * (size_t)104U, (size_t)104U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_7a(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c62(&s, &lvalue, i * (size_t)104U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** @@ -3244,39 +3517,65 @@ libcrux_sha3_generic_keccak_portable_keccak1_c6( { Eurydice_arr_26 s = libcrux_sha3_generic_keccak_new_80_04(); size_t data_len = data.meta; - for (size_t i = (size_t)0U; i < data_len / (size_t)168U; i++) - { - size_t i0 = i; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i0 * (size_t)168U); - } - size_t rem = data_len % (size_t)168U; - /* original Rust expression is not an lvalue in C */ - Eurydice_arr_06 lvalue = { .data = { data } }; - libcrux_sha3_generic_keccak_absorb_final_80_9e2(&s, &lvalue, data_len - rem, rem); - size_t outlen = out.meta; - size_t blocks = outlen / (size_t)168U; - size_t last = outlen - outlen % (size_t)168U; - if (blocks == (size_t)0U) - { - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, outlen); - } - else + core_ops_range_Range_08 + iter = + core_iter_traits_collect__core__iter__traits__collect__IntoIterator_Clause1_Item__I__for_I__into_iter(( + KRML_CLITERAL(core_ops_range_Range_08){ + .start = (size_t)0U, + .end = data_len / (size_t)168U + } + ), + core_ops_range_Range_08, + size_t, + core_ops_range_Range_08); + while (true) { - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, (size_t)168U); - for (size_t i = (size_t)1U; i < blocks; i++) + core_option_Option_08 + uu____0 = + core_iter_range__core__iter__traits__iterator__Iterator_A__for_core__ops__range__Range_A__TraitClause_0___next(&iter, + size_t, + core_option_Option_08); + if (uu____0.tag == core_option_None) { - size_t i0 = i; - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, i0 * (size_t)168U, (size_t)168U); + size_t rem = data_len % (size_t)168U; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_final_80_9e2(&s, &lvalue, data_len - rem, rem); + size_t outlen = out.meta; + size_t blocks = outlen / (size_t)168U; + size_t last = outlen - outlen % (size_t)168U; + if (blocks == (size_t)0U) + { + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, outlen); + return; + } + else + { + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, (size_t)0U, (size_t)168U); + for (size_t i = (size_t)1U; i < blocks; i++) + { + size_t i0 = i; + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, i0 * (size_t)168U, (size_t)168U); + } + if (last < outlen) + { + libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); + libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, last, outlen - last); + } + return; + } } - if (last < outlen) + else { - libcrux_sha3_generic_keccak_keccakf1600_80_04(&s); - libcrux_sha3_simd_portable_squeeze_13_3a(&s, out, last, outlen - last); + size_t i = uu____0.f0; + /* original Rust expression is not an lvalue in C */ + Eurydice_arr_06 lvalue = { .data = { data } }; + libcrux_sha3_generic_keccak_absorb_block_80_c63(&s, &lvalue, i * (size_t)168U); } } + KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); + KRML_HOST_EXIT(255U); } /** diff --git a/out/test-libcrux/libcrux_sha3_portable.h b/out/test-libcrux/libcrux_sha3_portable.h index 7db9e271..592a0a4b 100644 --- a/out/test-libcrux/libcrux_sha3_portable.h +++ b/out/test-libcrux/libcrux_sha3_portable.h @@ -127,19 +127,35 @@ libcrux_sha3_simd_portable_load_block_f8( size_t start ); +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_last +with const generics +- RATE= 72 +- DELIMITER= 6 +*/ +void +libcrux_sha3_simd_portable_load_last_96( + Eurydice_arr_26 *state, + Eurydice_borrow_slice_u8 blocks, + size_t start, + size_t len +); + /** This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 with const generics - RATE= 72 +- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_block_a1_f8( +libcrux_sha3_simd_portable_load_last_a1_96( Eurydice_arr_26 *self, const Eurydice_arr_06 *input, - size_t start + size_t start, + size_t len ); /** @@ -877,96 +893,80 @@ void libcrux_sha3_generic_keccak_keccakf1600_80_04(Eurydice_arr_26 *self); This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_80 with types uint64_t with const generics - N= 1 - RATE= 72 +- DELIM= 6 */ void -libcrux_sha3_generic_keccak_absorb_block_80_c6( +libcrux_sha3_generic_keccak_absorb_final_80_9e( Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start + const Eurydice_arr_06 *last, + size_t start, + size_t len ); /** -A monomorphic instance of libcrux_sha3.simd.portable.load_last +A monomorphic instance of libcrux_sha3.simd.portable.store_block with const generics - RATE= 72 -- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_last_96( - Eurydice_arr_26 *state, - Eurydice_borrow_slice_u8 blocks, +libcrux_sha3_simd_portable_store_block_f8( + const Eurydice_arr_26 *s, + Eurydice_mut_borrow_slice_u8 out, size_t start, size_t len ); /** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +This function found in impl {libcrux_sha3::traits::Squeeze1 for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.load_last_a1 +A monomorphic instance of libcrux_sha3.simd.portable.squeeze_13 with const generics - RATE= 72 -- DELIMITER= 6 */ void -libcrux_sha3_simd_portable_load_last_a1_96( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, +libcrux_sha3_simd_portable_squeeze_13_f8( + const Eurydice_arr_26 *self, + Eurydice_mut_borrow_slice_u8 out, size_t start, size_t len ); /** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} */ /** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_final_80 -with types uint64_t +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 with const generics -- N= 1 - RATE= 72 -- DELIM= 6 */ void -libcrux_sha3_generic_keccak_absorb_final_80_9e( +libcrux_sha3_simd_portable_load_block_a1_f8( Eurydice_arr_26 *self, - const Eurydice_arr_06 *last, - size_t start, - size_t len -); - -/** -A monomorphic instance of libcrux_sha3.simd.portable.store_block -with const generics -- RATE= 72 -*/ -void -libcrux_sha3_simd_portable_store_block_f8( - const Eurydice_arr_26 *s, - Eurydice_mut_borrow_slice_u8 out, - size_t start, - size_t len + const Eurydice_arr_06 *input, + size_t start ); /** -This function found in impl {libcrux_sha3::traits::Squeeze1 for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} */ /** -A monomorphic instance of libcrux_sha3.simd.portable.squeeze_13 +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t with const generics +- N= 1 - RATE= 72 */ void -libcrux_sha3_simd_portable_squeeze_13_f8( - const Eurydice_arr_26 *self, - Eurydice_mut_borrow_slice_u8 out, - size_t start, - size_t len +libcrux_sha3_generic_keccak_absorb_block_80_c6( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start ); /** @@ -1002,38 +1002,6 @@ libcrux_sha3_simd_portable_load_block_5b( size_t start ); -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 136 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_5b( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, - size_t start -); - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 136 -*/ -void -libcrux_sha3_generic_keccak_absorb_block_80_c60( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start -); - /** A monomorphic instance of libcrux_sha3.simd.portable.load_last with const generics @@ -1113,6 +1081,38 @@ libcrux_sha3_simd_portable_squeeze_13_5b( size_t len ); +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 136 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_5b( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *input, + size_t start +); + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 136 +*/ +void +libcrux_sha3_generic_keccak_absorb_block_80_c60( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start +); + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -1391,38 +1391,6 @@ libcrux_sha3_simd_portable_load_block_2c( size_t start ); -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 144 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_2c( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, - size_t start -); - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 144 -*/ -void -libcrux_sha3_generic_keccak_absorb_block_80_c61( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start -); - /** A monomorphic instance of libcrux_sha3.simd.portable.load_last with const generics @@ -1502,6 +1470,38 @@ libcrux_sha3_simd_portable_squeeze_13_2c( size_t len ); +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 144 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_2c( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *input, + size_t start +); + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 144 +*/ +void +libcrux_sha3_generic_keccak_absorb_block_80_c61( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start +); + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics @@ -1535,38 +1535,6 @@ libcrux_sha3_simd_portable_load_block_7a( size_t start ); -/** -This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} -*/ -/** -A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 -with const generics -- RATE= 104 -*/ -void -libcrux_sha3_simd_portable_load_block_a1_7a( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *input, - size_t start -); - -/** -This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} -*/ -/** -A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 -with types uint64_t -with const generics -- N= 1 -- RATE= 104 -*/ -void -libcrux_sha3_generic_keccak_absorb_block_80_c62( - Eurydice_arr_26 *self, - const Eurydice_arr_06 *blocks, - size_t start -); - /** A monomorphic instance of libcrux_sha3.simd.portable.load_last with const generics @@ -1646,6 +1614,38 @@ libcrux_sha3_simd_portable_squeeze_13_7a( size_t len ); +/** +This function found in impl {libcrux_sha3::traits::Absorb<1usize> for libcrux_sha3::generic_keccak::KeccakState[core::marker::Sized, libcrux_sha3::simd::portable::{libcrux_sha3::traits::KeccakItem<1usize> for u64}]} +*/ +/** +A monomorphic instance of libcrux_sha3.simd.portable.load_block_a1 +with const generics +- RATE= 104 +*/ +void +libcrux_sha3_simd_portable_load_block_a1_7a( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *input, + size_t start +); + +/** +This function found in impl {libcrux_sha3::generic_keccak::KeccakState[TraitClause@0, TraitClause@1]} +*/ +/** +A monomorphic instance of libcrux_sha3.generic_keccak.absorb_block_80 +with types uint64_t +with const generics +- N= 1 +- RATE= 104 +*/ +void +libcrux_sha3_generic_keccak_absorb_block_80_c62( + Eurydice_arr_26 *self, + const Eurydice_arr_06 *blocks, + size_t start +); + /** A monomorphic instance of libcrux_sha3.generic_keccak.portable.keccak1 with const generics