/* * SPDX-FileCopyrightText: 2026 CE Labs * * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: * Charon: e656e17bff6ca5efac8ab6919b9b74cb9a8dd8ad * Eurydice: aaa9fa657fb6f09802edb890252040d94cd93982 * Karamel: 8c19d41458ce5cbfea029ebc03334ba96d149039 * F*: 70671ffb81fa30aba09b9d6e2af275dfbccaa8f8 * Libcrux: 10066f256cec8d50d6111a4cf33ab920cfdb96cb */ #include "libcrux_mldsa_portable.h" #include "libcrux_sha3_portable.h" #include "libcrux_mldsa_core.h" #include "combined_core.h" #include "internal/libcrux_mlkem_core.h" #include "internal/libcrux_mldsa_core.h" #include "internal/combined_core.h" KRML_MUSTINLINE libcrux_ml_dsa_hash_functions_portable_Shake128X4 libcrux_ml_dsa_hash_functions_portable_init_absorb( Eurydice_borrow_slice_u8 input0, Eurydice_borrow_slice_u8 input1, Eurydice_borrow_slice_u8 input2, Eurydice_borrow_slice_u8 input3 ) { Eurydice_arr_7c state0 = libcrux_sha3_portable_incremental_shake128_init(); libcrux_sha3_portable_incremental_shake128_absorb_final(&state0, input0); Eurydice_arr_7c state1 = libcrux_sha3_portable_incremental_shake128_init(); libcrux_sha3_portable_incremental_shake128_absorb_final(&state1, input1); Eurydice_arr_7c state2 = libcrux_sha3_portable_incremental_shake128_init(); libcrux_sha3_portable_incremental_shake128_absorb_final(&state2, input2); Eurydice_arr_7c state3 = libcrux_sha3_portable_incremental_shake128_init(); libcrux_sha3_portable_incremental_shake128_absorb_final(&state3, input3); return ( KRML_CLITERAL(libcrux_ml_dsa_hash_functions_portable_Shake128X4){ .state0 = state0, .state1 = state1, .state2 = state2, .state3 = state3 } ); } KRML_MUSTINLINE Eurydice_arr_7c libcrux_ml_dsa_hash_functions_portable_init_absorb_final_shake256( Eurydice_borrow_slice_u8 input ) { Eurydice_arr_7c state = libcrux_sha3_portable_incremental_shake256_init(); libcrux_sha3_portable_incremental_shake256_absorb_final(&state, input); return state; } KRML_MUSTINLINE libcrux_ml_dsa_hash_functions_portable_Shake256X4 libcrux_ml_dsa_hash_functions_portable_init_absorb_x4( Eurydice_borrow_slice_u8 input0, Eurydice_borrow_slice_u8 input1, Eurydice_borrow_slice_u8 input2, Eurydice_borrow_slice_u8 input3 ) { Eurydice_arr_7c state0 = libcrux_sha3_portable_incremental_shake256_init(); libcrux_sha3_portable_incremental_shake256_absorb_final(&state0, input0); Eurydice_arr_7c state1 = libcrux_sha3_portable_incremental_shake256_init(); libcrux_sha3_portable_incremental_shake256_absorb_final(&state1, input1); Eurydice_arr_7c state2 = libcrux_sha3_portable_incremental_shake256_init(); libcrux_sha3_portable_incremental_shake256_absorb_final(&state2, input2); Eurydice_arr_7c state3 = libcrux_sha3_portable_incremental_shake256_init(); libcrux_sha3_portable_incremental_shake256_absorb_final(&state3, input3); return ( KRML_CLITERAL(libcrux_ml_dsa_hash_functions_portable_Shake256X4){ .state0 = state0, .state1 = state1, .state2 = state2, .state3 = state3 } ); } KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake128( Eurydice_borrow_slice_u8 input, Eurydice_mut_borrow_slice_u8 out ) { libcrux_sha3_portable_shake128(out, input); } KRML_MUSTINLINE Eurydice_arr_ff libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_shake256(Eurydice_arr_7c *state) { Eurydice_arr_ff out = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_first_block(state, Eurydice_array_to_slice_mut_58(&out)); return out; } KRML_MUSTINLINE Eurydice_arr_ff_x4 libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_x4( libcrux_ml_dsa_hash_functions_portable_Shake256X4 *state ) { Eurydice_arr_ff out0 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_first_block(&state->state0, Eurydice_array_to_slice_mut_58(&out0)); Eurydice_arr_ff out1 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_first_block(&state->state1, Eurydice_array_to_slice_mut_58(&out1)); Eurydice_arr_ff out2 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_first_block(&state->state2, Eurydice_array_to_slice_mut_58(&out2)); Eurydice_arr_ff out3 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_first_block(&state->state3, Eurydice_array_to_slice_mut_58(&out3)); return (KRML_CLITERAL(Eurydice_arr_ff_x4){ .fst = out0, .snd = out1, .thd = out2, .f3 = out3 }); } KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_squeeze_first_five_blocks( libcrux_ml_dsa_hash_functions_portable_Shake128X4 *state, Eurydice_arr_d10 *out0, Eurydice_arr_d10 *out1, Eurydice_arr_d10 *out2, Eurydice_arr_d10 *out3 ) { libcrux_sha3_portable_incremental_shake128_squeeze_first_five_blocks(&state->state0, Eurydice_array_to_slice_mut_4c(out0)); libcrux_sha3_portable_incremental_shake128_squeeze_first_five_blocks(&state->state1, Eurydice_array_to_slice_mut_4c(out1)); libcrux_sha3_portable_incremental_shake128_squeeze_first_five_blocks(&state->state2, Eurydice_array_to_slice_mut_4c(out2)); libcrux_sha3_portable_incremental_shake128_squeeze_first_five_blocks(&state->state3, Eurydice_array_to_slice_mut_4c(out3)); } KRML_MUSTINLINE Eurydice_arr_c5_x4 libcrux_ml_dsa_hash_functions_portable_squeeze_next_block( libcrux_ml_dsa_hash_functions_portable_Shake128X4 *state ) { Eurydice_arr_c5 out0 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake128_squeeze_next_block(&state->state0, Eurydice_array_to_slice_mut_2c(&out0)); Eurydice_arr_c5 out1 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake128_squeeze_next_block(&state->state1, Eurydice_array_to_slice_mut_2c(&out1)); Eurydice_arr_c5 out2 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake128_squeeze_next_block(&state->state2, Eurydice_array_to_slice_mut_2c(&out2)); Eurydice_arr_c5 out3 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake128_squeeze_next_block(&state->state3, Eurydice_array_to_slice_mut_2c(&out3)); return (KRML_CLITERAL(Eurydice_arr_c5_x4){ .fst = out0, .snd = out1, .thd = out2, .f3 = out3 }); } KRML_MUSTINLINE Eurydice_arr_ff libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_shake256(Eurydice_arr_7c *state) { Eurydice_arr_ff out = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_next_block(state, Eurydice_array_to_slice_mut_58(&out)); return out; } KRML_MUSTINLINE Eurydice_arr_ff_x4 libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_x4( libcrux_ml_dsa_hash_functions_portable_Shake256X4 *state ) { Eurydice_arr_ff out0 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_next_block(&state->state0, Eurydice_array_to_slice_mut_58(&out0)); Eurydice_arr_ff out1 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_next_block(&state->state1, Eurydice_array_to_slice_mut_58(&out1)); Eurydice_arr_ff out2 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_next_block(&state->state2, Eurydice_array_to_slice_mut_58(&out2)); Eurydice_arr_ff out3 = { .data = { 0U } }; libcrux_sha3_portable_incremental_shake256_squeeze_next_block(&state->state3, Eurydice_array_to_slice_mut_58(&out3)); return (KRML_CLITERAL(Eurydice_arr_ff_x4){ .fst = out0, .snd = out1, .thd = out2, .f3 = out3 }); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake128::Xof for libcrux_ml_dsa::hash_functions::portable::Shake128} */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake128_7b( Eurydice_borrow_slice_u8 input, Eurydice_mut_borrow_slice_u8 out ) { libcrux_ml_dsa_hash_functions_portable_shake128(input, out); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake128::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake128X4} */ KRML_MUSTINLINE libcrux_ml_dsa_hash_functions_portable_Shake128X4 libcrux_ml_dsa_hash_functions_portable_init_absorb_11( Eurydice_borrow_slice_u8 input0, Eurydice_borrow_slice_u8 input1, Eurydice_borrow_slice_u8 input2, Eurydice_borrow_slice_u8 input3 ) { return libcrux_ml_dsa_hash_functions_portable_init_absorb(input0, input1, input2, input3); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake128::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake128X4} */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_squeeze_first_five_blocks_11( libcrux_ml_dsa_hash_functions_portable_Shake128X4 *self, Eurydice_arr_d10 *out0, Eurydice_arr_d10 *out1, Eurydice_arr_d10 *out2, Eurydice_arr_d10 *out3 ) { libcrux_ml_dsa_hash_functions_portable_squeeze_first_five_blocks(self, out0, out1, out2, out3); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake128::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake128X4} */ KRML_MUSTINLINE Eurydice_arr_c5_x4 libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_11( libcrux_ml_dsa_hash_functions_portable_Shake128X4 *self ) { return libcrux_ml_dsa_hash_functions_portable_squeeze_next_block(self); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::DsaXof for libcrux_ml_dsa::hash_functions::portable::Shake256} */ KRML_MUSTINLINE Eurydice_arr_7c libcrux_ml_dsa_hash_functions_portable_init_absorb_final_61(Eurydice_borrow_slice_u8 input) { return libcrux_ml_dsa_hash_functions_portable_init_absorb_final_shake256(input); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::DsaXof for libcrux_ml_dsa::hash_functions::portable::Shake256} */ KRML_MUSTINLINE Eurydice_arr_ff libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_61(Eurydice_arr_7c *self) { return libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_shake256(self); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::DsaXof for libcrux_ml_dsa::hash_functions::portable::Shake256} */ KRML_MUSTINLINE Eurydice_arr_ff libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_61(Eurydice_arr_7c *self) { return libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_shake256(self); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::Xof for libcrux_ml_dsa::hash_functions::portable::Shake256Xof} */ void libcrux_ml_dsa_hash_functions_portable_absorb_26( libcrux_sha3_generic_keccak_xof_KeccakXofState_8d *self, Eurydice_borrow_slice_u8 input ) { libcrux_sha3_portable_incremental_absorb_42(self, input); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::Xof for libcrux_ml_dsa::hash_functions::portable::Shake256Xof} */ void libcrux_ml_dsa_hash_functions_portable_absorb_final_26( libcrux_sha3_generic_keccak_xof_KeccakXofState_8d *self, Eurydice_borrow_slice_u8 input ) { libcrux_sha3_portable_incremental_absorb_final_42(self, input); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::Xof for libcrux_ml_dsa::hash_functions::portable::Shake256Xof} */ libcrux_sha3_generic_keccak_xof_KeccakXofState_8d libcrux_ml_dsa_hash_functions_portable_init_26(void) { return libcrux_sha3_portable_incremental_new_42(); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::Xof for libcrux_ml_dsa::hash_functions::portable::Shake256Xof} */ void libcrux_ml_dsa_hash_functions_portable_squeeze_26( libcrux_sha3_generic_keccak_xof_KeccakXofState_8d *self, Eurydice_mut_borrow_slice_u8 out ) { libcrux_sha3_portable_incremental_squeeze_42(self, out); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake256X4} */ KRML_MUSTINLINE libcrux_ml_dsa_hash_functions_portable_Shake256X4 libcrux_ml_dsa_hash_functions_portable_init_absorb_x4_9b( Eurydice_borrow_slice_u8 input0, Eurydice_borrow_slice_u8 input1, Eurydice_borrow_slice_u8 input2, Eurydice_borrow_slice_u8 input3 ) { return libcrux_ml_dsa_hash_functions_portable_init_absorb_x4(input0, input1, input2, input3); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake256X4} */ KRML_MUSTINLINE Eurydice_arr_ff_x4 libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_x4_9b( libcrux_ml_dsa_hash_functions_portable_Shake256X4 *self ) { return libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_x4(self); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake256X4} */ KRML_MUSTINLINE Eurydice_arr_ff_x4 libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_x4_9b( libcrux_ml_dsa_hash_functions_portable_Shake256X4 *self ) { return libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_x4(self); } /** A monomorphic instance of libcrux_ml_dsa.sample.sample_four_error_ring_elements with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_sample_sample_four_error_ring_elements_29( libcrux_ml_dsa_constants_Eta eta, Eurydice_borrow_slice_u8 seed, uint16_t start_index, Eurydice_dst_ref_mut_44 re ) { Eurydice_arr_91 seed0 = libcrux_ml_dsa_sample_add_error_domain_separator(seed, start_index); Eurydice_arr_91 seed1 = libcrux_ml_dsa_sample_add_error_domain_separator(seed, (uint32_t)start_index + 1U); Eurydice_arr_91 seed2 = libcrux_ml_dsa_sample_add_error_domain_separator(seed, (uint32_t)start_index + 2U); Eurydice_arr_91 seed3 = libcrux_ml_dsa_sample_add_error_domain_separator(seed, (uint32_t)start_index + 3U); libcrux_ml_dsa_hash_functions_portable_Shake256X4 state = libcrux_ml_dsa_hash_functions_portable_init_absorb_x4_9b(Eurydice_array_to_slice_shared_f1(&seed0), Eurydice_array_to_slice_shared_f1(&seed1), Eurydice_array_to_slice_shared_f1(&seed2), Eurydice_array_to_slice_shared_f1(&seed3)); Eurydice_arr_ff_x4 randomnesses0 = libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_x4_9b(&state); Eurydice_arr_930 out = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; size_t sampled0 = (size_t)0U; size_t sampled1 = (size_t)0U; size_t sampled2 = (size_t)0U; size_t sampled3 = (size_t)0U; libcrux_ml_dsa_constants_Eta uu____0 = eta; bool done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____0, Eurydice_array_to_slice_shared_58(&randomnesses0.fst), &sampled0, out.data); libcrux_ml_dsa_constants_Eta uu____1 = eta; bool done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____1, Eurydice_array_to_slice_shared_58(&randomnesses0.snd), &sampled1, &out.data[1U]); libcrux_ml_dsa_constants_Eta uu____2 = eta; bool done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____2, Eurydice_array_to_slice_shared_58(&randomnesses0.thd), &sampled2, &out.data[2U]); libcrux_ml_dsa_constants_Eta uu____3 = eta; bool done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____3, Eurydice_array_to_slice_shared_58(&randomnesses0.f3), &sampled3, &out.data[3U]); while (true) { if (done0) { if (done1) { if (done2) { if (done3) { break; } else { Eurydice_arr_ff_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_x4_9b(&state); if (!done0) { libcrux_ml_dsa_constants_Eta uu____4 = eta; done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____4, Eurydice_array_to_slice_shared_58(&randomnesses.fst), &sampled0, out.data); } if (!done1) { libcrux_ml_dsa_constants_Eta uu____5 = eta; done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____5, Eurydice_array_to_slice_shared_58(&randomnesses.snd), &sampled1, &out.data[1U]); } if (!done2) { libcrux_ml_dsa_constants_Eta uu____6 = eta; done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____6, Eurydice_array_to_slice_shared_58(&randomnesses.thd), &sampled2, &out.data[2U]); } if (!done3) { libcrux_ml_dsa_constants_Eta uu____7 = eta; done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____7, Eurydice_array_to_slice_shared_58(&randomnesses.f3), &sampled3, &out.data[3U]); } } } else { Eurydice_arr_ff_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_x4_9b(&state); if (!done0) { libcrux_ml_dsa_constants_Eta uu____8 = eta; done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____8, Eurydice_array_to_slice_shared_58(&randomnesses.fst), &sampled0, out.data); } if (!done1) { libcrux_ml_dsa_constants_Eta uu____9 = eta; done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____9, Eurydice_array_to_slice_shared_58(&randomnesses.snd), &sampled1, &out.data[1U]); } if (!done2) { libcrux_ml_dsa_constants_Eta uu____10 = eta; done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____10, Eurydice_array_to_slice_shared_58(&randomnesses.thd), &sampled2, &out.data[2U]); } if (!done3) { libcrux_ml_dsa_constants_Eta uu____11 = eta; done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____11, Eurydice_array_to_slice_shared_58(&randomnesses.f3), &sampled3, &out.data[3U]); } } } else { Eurydice_arr_ff_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_x4_9b(&state); if (!done0) { libcrux_ml_dsa_constants_Eta uu____12 = eta; done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____12, Eurydice_array_to_slice_shared_58(&randomnesses.fst), &sampled0, out.data); } if (!done1) { libcrux_ml_dsa_constants_Eta uu____13 = eta; done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____13, Eurydice_array_to_slice_shared_58(&randomnesses.snd), &sampled1, &out.data[1U]); } if (!done2) { libcrux_ml_dsa_constants_Eta uu____14 = eta; done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____14, Eurydice_array_to_slice_shared_58(&randomnesses.thd), &sampled2, &out.data[2U]); } if (!done3) { libcrux_ml_dsa_constants_Eta uu____15 = eta; done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____15, Eurydice_array_to_slice_shared_58(&randomnesses.f3), &sampled3, &out.data[3U]); } } } else { Eurydice_arr_ff_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_x4_9b(&state); if (!done0) { libcrux_ml_dsa_constants_Eta uu____16 = eta; done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____16, Eurydice_array_to_slice_shared_58(&randomnesses.fst), &sampled0, out.data); } if (!done1) { libcrux_ml_dsa_constants_Eta uu____17 = eta; done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____17, Eurydice_array_to_slice_shared_58(&randomnesses.snd), &sampled1, &out.data[1U]); } if (!done2) { libcrux_ml_dsa_constants_Eta uu____18 = eta; done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____18, Eurydice_array_to_slice_shared_58(&randomnesses.thd), &sampled2, &out.data[2U]); } if (!done3) { libcrux_ml_dsa_constants_Eta uu____19 = eta; done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_eta_37(uu____19, Eurydice_array_to_slice_shared_58(&randomnesses.f3), &sampled3, &out.data[3U]); } } } size_t max0 = (size_t)(uint32_t)start_index + (size_t)4U; size_t max; if (re.meta < max0) { max = re.meta; } else { max = max0; } for (size_t i = (size_t)(uint32_t)start_index; i < max; i++) { size_t i0 = i; libcrux_ml_dsa_polynomial_from_i32_array_ff_37(Eurydice_array_to_slice_shared_2c0(&out.data[i0 % (size_t)4U]), &re.ptr[i0]); } } /** A monomorphic instance of libcrux_ml_dsa.samplex4.sample_s1_and_s2 with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_samplex4_sample_s1_and_s2_29( libcrux_ml_dsa_constants_Eta eta, Eurydice_borrow_slice_u8 seed, Eurydice_dst_ref_mut_44 s1_s2 ) { size_t len = s1_s2.meta; for (size_t i = (size_t)0U; i < len / (size_t)4U; i++) { size_t i0 = i; libcrux_ml_dsa_sample_sample_four_error_ring_elements_29(eta, seed, 4U * (uint32_t)(uint16_t)i0, s1_s2); } size_t remainder = len % (size_t)4U; if (remainder != (size_t)0U) { libcrux_ml_dsa_sample_sample_four_error_ring_elements_29(eta, seed, (uint16_t)(len - remainder), s1_s2); } } /** Sample and write out up to four ring elements. If i <= `elements_requested`, a field element with domain separated seed according to the provided index is generated in `tmp_stack[i]`. After successful rejection sampling in `tmp_stack[i]`, the ring element is written to `matrix` at the provided index in `indices[i]`. `rand_stack` is a working buffer that holds initial Shake output. */ /** A monomorphic instance of libcrux_ml_dsa.sample.sample_up_to_four_ring_elements_flat with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake128X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_sample_sample_up_to_four_ring_elements_flat_63( size_t columns, Eurydice_borrow_slice_u8 seed, Eurydice_dst_ref_mut_44 matrix, Eurydice_arr_d10 *rand_stack0, Eurydice_arr_d10 *rand_stack1, Eurydice_arr_d10 *rand_stack2, Eurydice_arr_d10 *rand_stack3, Eurydice_dst_ref_mut_33 tmp_stack, size_t start_index, size_t elements_requested ) { Eurydice_arr_31 seed0 = libcrux_ml_dsa_sample_add_domain_separator(seed, libcrux_ml_dsa_sample_sample_up_to_four_ring_elements_flat_xy(start_index, columns)); Eurydice_arr_31 seed1 = libcrux_ml_dsa_sample_add_domain_separator(seed, libcrux_ml_dsa_sample_sample_up_to_four_ring_elements_flat_xy(start_index + (size_t)1U, columns)); Eurydice_arr_31 seed2 = libcrux_ml_dsa_sample_add_domain_separator(seed, libcrux_ml_dsa_sample_sample_up_to_four_ring_elements_flat_xy(start_index + (size_t)2U, columns)); Eurydice_arr_31 seed3 = libcrux_ml_dsa_sample_add_domain_separator(seed, libcrux_ml_dsa_sample_sample_up_to_four_ring_elements_flat_xy(start_index + (size_t)3U, columns)); libcrux_ml_dsa_hash_functions_portable_Shake128X4 state = libcrux_ml_dsa_hash_functions_portable_init_absorb_11(Eurydice_array_to_slice_shared_e9(&seed0), Eurydice_array_to_slice_shared_e9(&seed1), Eurydice_array_to_slice_shared_e9(&seed2), Eurydice_array_to_slice_shared_e9(&seed3)); libcrux_ml_dsa_hash_functions_portable_squeeze_first_five_blocks_11(&state, rand_stack0, rand_stack1, rand_stack2, rand_stack3); size_t sampled0 = (size_t)0U; size_t sampled1 = (size_t)0U; size_t sampled2 = (size_t)0U; size_t sampled3 = (size_t)0U; bool done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_4c(rand_stack0), &sampled0, tmp_stack.ptr); bool done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_4c(rand_stack1), &sampled1, &tmp_stack.ptr[1U]); bool done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_4c(rand_stack2), &sampled2, &tmp_stack.ptr[2U]); bool done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_4c(rand_stack3), &sampled3, &tmp_stack.ptr[3U]); while (true) { if (done0) { if (done1) { if (done2) { if (done3) { break; } else { Eurydice_arr_c5_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_11(&state); if (!done0) { done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.fst), &sampled0, tmp_stack.ptr); } if (!done1) { done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.snd), &sampled1, &tmp_stack.ptr[1U]); } if (!done2) { done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.thd), &sampled2, &tmp_stack.ptr[2U]); } if (!done3) { done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.f3), &sampled3, &tmp_stack.ptr[3U]); } } } else { Eurydice_arr_c5_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_11(&state); if (!done0) { done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.fst), &sampled0, tmp_stack.ptr); } if (!done1) { done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.snd), &sampled1, &tmp_stack.ptr[1U]); } if (!done2) { done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.thd), &sampled2, &tmp_stack.ptr[2U]); } if (!done3) { done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.f3), &sampled3, &tmp_stack.ptr[3U]); } } } else { Eurydice_arr_c5_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_11(&state); if (!done0) { done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.fst), &sampled0, tmp_stack.ptr); } if (!done1) { done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.snd), &sampled1, &tmp_stack.ptr[1U]); } if (!done2) { done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.thd), &sampled2, &tmp_stack.ptr[2U]); } if (!done3) { done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.f3), &sampled3, &tmp_stack.ptr[3U]); } } } else { Eurydice_arr_c5_x4 randomnesses = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_11(&state); if (!done0) { done0 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.fst), &sampled0, tmp_stack.ptr); } if (!done1) { done1 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.snd), &sampled1, &tmp_stack.ptr[1U]); } if (!done2) { done2 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.thd), &sampled2, &tmp_stack.ptr[2U]); } if (!done3) { done3 = libcrux_ml_dsa_sample_rejection_sample_less_than_field_modulus_37(Eurydice_array_to_slice_shared_2c(&randomnesses.f3), &sampled3, &tmp_stack.ptr[3U]); } } } for (size_t i = (size_t)0U; i < elements_requested; i++) { size_t k = i; libcrux_ml_dsa_polynomial_from_i32_array_ff_37(Eurydice_array_to_slice_shared_2c0(&tmp_stack.ptr[k]), &matrix.ptr[start_index + k]); } } /** A monomorphic instance of libcrux_ml_dsa.samplex4.matrix_flat with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake128X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_samplex4_matrix_flat_63( size_t columns, Eurydice_borrow_slice_u8 seed, Eurydice_dst_ref_mut_44 matrix ) { Eurydice_arr_d10 rand_stack0 = { .data = { 0U } }; Eurydice_arr_d10 rand_stack1 = { .data = { 0U } }; Eurydice_arr_d10 rand_stack2 = { .data = { 0U } }; Eurydice_arr_d10 rand_stack3 = { .data = { 0U } }; Eurydice_arr_930 tmp_stack = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; for (size_t i = (size_t)0U; i < matrix.meta / (size_t)4U + (size_t)1U; i++) { size_t start_index = i; size_t start_index0 = start_index * (size_t)4U; if (start_index0 >= matrix.meta) { break; } size_t elements_requested; if (start_index0 + (size_t)4U <= matrix.meta) { elements_requested = (size_t)4U; } else { elements_requested = matrix.meta - start_index0; } libcrux_ml_dsa_sample_sample_up_to_four_ring_elements_flat_63(columns, seed, matrix, &rand_stack0, &rand_stack1, &rand_stack2, &rand_stack3, Eurydice_array_to_slice_mut_7e(&tmp_stack), start_index0, elements_requested); } } /** This function found in impl {libcrux_ml_dsa::samplex4::X4Sampler for libcrux_ml_dsa::samplex4::portable::PortableSampler} */ /** A monomorphic instance of libcrux_ml_dsa.samplex4.portable.matrix_flat_a8 with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients with const generics */ void libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37( size_t columns, Eurydice_borrow_slice_u8 seed, Eurydice_dst_ref_mut_44 matrix ) { libcrux_ml_dsa_samplex4_matrix_flat_63(columns, seed, matrix); } /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256 with const generics - OUTPUT_LENGTH= 64 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_c9( Eurydice_borrow_slice_u8 input, Eurydice_arr_c7 *out ) { libcrux_sha3_portable_shake256(Eurydice_array_to_slice_mut_17(out), input); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::DsaXof for libcrux_ml_dsa::hash_functions::portable::Shake256} */ /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256_61 with const generics - OUTPUT_LENGTH= 64 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_61_c9( Eurydice_borrow_slice_u8 input, Eurydice_arr_c7 *out ) { libcrux_ml_dsa_hash_functions_portable_shake256_c9(input, out); } /** A monomorphic instance of libcrux_ml_dsa.encoding.signing_key.generate_serialized with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake256 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_encoding_signing_key_generate_serialized_2e( libcrux_ml_dsa_constants_Eta eta, size_t error_ring_element_size, Eurydice_borrow_slice_u8 seed_matrix, Eurydice_borrow_slice_u8 seed_signing, Eurydice_borrow_slice_u8 verification_key, Eurydice_dst_ref_shared_44 s1_2, Eurydice_dst_ref_shared_44 t0, Eurydice_mut_borrow_slice_u8 signing_key_serialized ) { size_t offset = (size_t)0U; Eurydice_slice_copy(Eurydice_slice_subslice_mut_c8(signing_key_serialized, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = offset, .end = offset + LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE } )), seed_matrix, uint8_t); offset += LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE; Eurydice_slice_copy(Eurydice_slice_subslice_mut_c8(signing_key_serialized, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = offset, .end = offset + LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_SIGNING_SIZE } )), seed_signing, uint8_t); offset += LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_SIGNING_SIZE; Eurydice_arr_c7 verification_key_hash = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_61_c9(verification_key, &verification_key_hash); Eurydice_slice_copy(Eurydice_slice_subslice_mut_c8(signing_key_serialized, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = offset, .end = offset + LIBCRUX_ML_DSA_CONSTANTS_BYTES_FOR_VERIFICATION_KEY_HASH } )), Eurydice_array_to_slice_shared_17(&verification_key_hash), uint8_t); offset += LIBCRUX_ML_DSA_CONSTANTS_BYTES_FOR_VERIFICATION_KEY_HASH; for (size_t i = (size_t)0U; i < s1_2.meta; i++) { size_t i0 = i; libcrux_ml_dsa_encoding_error_serialize_37(eta, &s1_2.ptr[i0], Eurydice_slice_subslice_mut_c8(signing_key_serialized, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = offset, .end = offset + error_ring_element_size } ))); offset += error_ring_element_size; } for (size_t i = (size_t)0U; i < t0.meta; i++) { size_t _cloop_j = i; const Eurydice_arr_a3 *ring_element = &t0.ptr[_cloop_j]; libcrux_ml_dsa_encoding_t0_serialize_37(ring_element, Eurydice_slice_subslice_mut_c8(signing_key_serialized, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = offset, .end = offset + LIBCRUX_ML_DSA_CONSTANTS_RING_ELEMENT_OF_T0S_SIZE } ))); offset += LIBCRUX_ML_DSA_CONSTANTS_RING_ELEMENT_OF_T0S_SIZE; } } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.generate_key_pair with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_generate_key_pair_5a( Eurydice_arr_ec randomness, Eurydice_mut_borrow_slice_u8 signing_key, Eurydice_mut_borrow_slice_u8 verification_key ) { Eurydice_arr_89 seed_expanded0 = { .data = { 0U } }; libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_01(&randomness)); /* original Rust expression is not an lvalue in C */ Eurydice_array_u8x2 lvalue = { .data = { (uint8_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, (uint8_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A } }; libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_82(&lvalue)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_78(&seed_expanded0)); Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(Eurydice_array_to_slice_shared_78(&seed_expanded0), LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 seed_expanded = uu____0.snd; Eurydice_borrow_slice_u8_x2 uu____1 = Eurydice_slice_split_at(seed_expanded, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_ERROR_VECTORS_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_error_vectors = uu____1.fst; Eurydice_borrow_slice_u8 seed_for_signing = uu____1.snd; Eurydice_arr_8f s1_s2; Eurydice_arr_a3 repeat_expression0[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_s2.data, repeat_expression0, (size_t)8U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_sample_s1_and_s2_29(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ETA, seed_for_error_vectors, Eurydice_array_to_slice_mut_20(&s1_s2)); Eurydice_arr_9d t0; Eurydice_arr_a3 repeat_expression1[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t0.data, repeat_expression1, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_arr_2f a_as_ntt; Eurydice_arr_a3 repeat_expression2[16U]; KRML_MAYBE_FOR16(i, (size_t)0U, (size_t)16U, (size_t)1U, repeat_expression2[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(a_as_ntt.data, repeat_expression2, (size_t)16U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_200(&a_as_ntt)); Eurydice_arr_9d s1_ntt; Eurydice_arr_a3 repeat_expression3[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression3[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_ntt.data, repeat_expression3, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_slice_copy(Eurydice_array_to_slice_mut_201(&s1_ntt), Eurydice_array_to_subslice_shared_25(&s1_s2, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = (size_t)0U, .end = LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A } )), Eurydice_arr_a3); KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&s1_ntt.data[i0]);); libcrux_ml_dsa_matrix_compute_as1_plus_s2_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, Eurydice_array_to_slice_mut_200(&a_as_ntt), Eurydice_array_to_slice_shared_20(&s1_ntt), Eurydice_array_to_slice_shared_200(&s1_s2), Eurydice_array_to_slice_mut_201(&t0)); Eurydice_arr_9d t1; Eurydice_arr_a3 repeat_expression[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t1.data, repeat_expression, (size_t)4U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_arithmetic_power2round_vector_37(Eurydice_array_to_slice_mut_201(&t0), Eurydice_array_to_slice_mut_201(&t1)); libcrux_ml_dsa_encoding_verification_key_generate_serialized_37(seed_for_a, Eurydice_array_to_slice_shared_20(&t1), verification_key); libcrux_ml_dsa_encoding_signing_key_generate_serialized_2e(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_ERROR_RING_ELEMENT_SIZE, seed_for_a, seed_for_signing, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = verification_key.ptr, .meta = verification_key.meta } ), Eurydice_array_to_slice_shared_200(&s1_s2), Eurydice_array_to_slice_shared_20(&t0), signing_key); } /** Generate key pair. */ void libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_44_generate_key_pair( Eurydice_arr_ec randomness, Eurydice_arr_10 *signing_key, Eurydice_arr_02 *verification_key ) { libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_generate_key_pair_5a(randomness, Eurydice_array_to_slice_mut_34(signing_key), Eurydice_array_to_slice_mut_9f0(verification_key)); } /** This corresponds to line 6 in algorithm 7 in FIPS 204 (line 7 in algorithm 8, resp.). If `domain_separation_context` is supplied, applies domain separation and length encoding to the context string, before appending the message (in the regular variant) or the pre-hash OID as well as the pre-hashed message digest. Otherwise, it is assumed that `message` already contains domain separation information. In FIPS 204 M' is the concatenation of the domain separated context, any potential pre-hash OID and the message (or the message pre-hash). We do not explicitely construct the concatenation in memory since it is of statically unknown length, but feed its components directly into the incremental XOF. Refer to line 10 of Algorithm 2 (and line 5 of Algorithm 3, resp.) in [FIPS 204](https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.204.pdf#section.5) for details on the domain separation for regular ML-DSA. Line 23 of Algorithm 4 (and line 18 of Algorithm 5,resp.) describe domain separation for the HashMl-DSA variant. */ /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.derive_message_representative with types libcrux_ml_dsa_hash_functions_portable_Shake256Xof with const generics */ void libcrux_ml_dsa_ml_dsa_generic_derive_message_representative_43( Eurydice_borrow_slice_u8 verification_key_hash, const core_option_Option_84 *domain_separation_context, Eurydice_borrow_slice_u8 message, Eurydice_arr_c7 *message_representative ) { libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, verification_key_hash); if (domain_separation_context->tag == core_option_Some) { const libcrux_ml_dsa_pre_hash_DomainSeparationContext *domain_separation_context0 = &domain_separation_context->f0; libcrux_sha3_generic_keccak_xof_KeccakXofState_8d *uu____0 = &shake; /* original Rust expression is not an lvalue in C */ Eurydice_arr_82 lvalue0 = { .data = { (uint8_t)core_option__core__option__Option_T__TraitClause_0___is_some(libcrux_ml_dsa_pre_hash_pre_hash_oid_88(domain_separation_context0), Eurydice_arr_c9, bool) } }; libcrux_ml_dsa_hash_functions_portable_absorb_26(uu____0, Eurydice_array_to_slice_shared_79(&lvalue0)); libcrux_sha3_generic_keccak_xof_KeccakXofState_8d *uu____1 = &shake; /* original Rust expression is not an lvalue in C */ Eurydice_arr_82 lvalue = { .data = { (uint8_t)libcrux_ml_dsa_pre_hash_context_88(domain_separation_context0).meta } }; libcrux_ml_dsa_hash_functions_portable_absorb_26(uu____1, Eurydice_array_to_slice_shared_79(&lvalue)); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, libcrux_ml_dsa_pre_hash_context_88(domain_separation_context0)); const core_option_Option_57 *uu____2 = libcrux_ml_dsa_pre_hash_pre_hash_oid_88(domain_separation_context0); if (uu____2->tag == core_option_Some) { const Eurydice_arr_c9 *pre_hash_oid = &uu____2->f0; libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_2f(pre_hash_oid)); } } libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, message); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_17(message_representative)); } /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256 with const generics - OUTPUT_LENGTH= 576 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_5a( Eurydice_borrow_slice_u8 input, Eurydice_arr_220 *out ) { libcrux_sha3_portable_shake256(Eurydice_array_to_slice_mut_8a0(out), input); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake256X4} */ /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256_x4_9b with const generics - OUT_LEN= 576 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_x4_9b_5a( Eurydice_borrow_slice_u8 input0, Eurydice_borrow_slice_u8 input1, Eurydice_borrow_slice_u8 input2, Eurydice_borrow_slice_u8 input3, Eurydice_arr_220 *out0, Eurydice_arr_220 *out1, Eurydice_arr_220 *out2, Eurydice_arr_220 *out3 ) { libcrux_ml_dsa_hash_functions_portable_shake256_5a(input0, out0); libcrux_ml_dsa_hash_functions_portable_shake256_5a(input1, out1); libcrux_ml_dsa_hash_functions_portable_shake256_5a(input2, out2); libcrux_ml_dsa_hash_functions_portable_shake256_5a(input3, out3); } /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256 with const generics - OUTPUT_LENGTH= 640 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_0e( Eurydice_borrow_slice_u8 input, Eurydice_arr_20 *out ) { libcrux_sha3_portable_shake256(Eurydice_array_to_slice_mut_4f(out), input); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::XofX4 for libcrux_ml_dsa::hash_functions::portable::Shake256X4} */ /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256_x4_9b with const generics - OUT_LEN= 640 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_x4_9b_0e( Eurydice_borrow_slice_u8 input0, Eurydice_borrow_slice_u8 input1, Eurydice_borrow_slice_u8 input2, Eurydice_borrow_slice_u8 input3, Eurydice_arr_20 *out0, Eurydice_arr_20 *out1, Eurydice_arr_20 *out2, Eurydice_arr_20 *out3 ) { libcrux_ml_dsa_hash_functions_portable_shake256_0e(input0, out0); libcrux_ml_dsa_hash_functions_portable_shake256_0e(input1, out1); libcrux_ml_dsa_hash_functions_portable_shake256_0e(input2, out2); libcrux_ml_dsa_hash_functions_portable_shake256_0e(input3, out3); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::DsaXof for libcrux_ml_dsa::hash_functions::portable::Shake256} */ /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256_61 with const generics - OUTPUT_LENGTH= 640 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_61_0e( Eurydice_borrow_slice_u8 input, Eurydice_arr_20 *out ) { libcrux_ml_dsa_hash_functions_portable_shake256_0e(input, out); } /** This function found in impl {libcrux_ml_dsa::hash_functions::shake256::DsaXof for libcrux_ml_dsa::hash_functions::portable::Shake256} */ /** A monomorphic instance of libcrux_ml_dsa.hash_functions.portable.shake256_61 with const generics - OUTPUT_LENGTH= 576 */ KRML_MUSTINLINE void libcrux_ml_dsa_hash_functions_portable_shake256_61_5a( Eurydice_borrow_slice_u8 input, Eurydice_arr_220 *out ) { libcrux_ml_dsa_hash_functions_portable_shake256_5a(input, out); } /** A monomorphic instance of libcrux_ml_dsa.sample.sample_mask_ring_element with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake256 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_sample_sample_mask_ring_element_2e( const Eurydice_arr_91 *seed, Eurydice_arr_a3 *result, size_t gamma1_exponent ) { switch (gamma1_exponent) { case 17U: { break; } case 19U: { Eurydice_arr_20 out = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_61_0e(Eurydice_array_to_slice_shared_f1(seed), &out); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_4f(&out), result); return; } default: { KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); } } Eurydice_arr_220 out = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_61_5a(Eurydice_array_to_slice_shared_f1(seed), &out); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_8a0(&out), result); } /** A monomorphic instance of libcrux_ml_dsa.sample.sample_mask_vector with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_sample_sample_mask_vector_67( size_t dimension, size_t gamma1_exponent, const Eurydice_arr_c7 *seed, uint16_t *domain_separator, Eurydice_dst_ref_mut_44 mask ) { Eurydice_arr_91 seed0 = libcrux_ml_dsa_sample_add_error_domain_separator(Eurydice_array_to_slice_shared_17(seed), domain_separator[0U]); Eurydice_arr_91 seed1 = libcrux_ml_dsa_sample_add_error_domain_separator(Eurydice_array_to_slice_shared_17(seed), (uint32_t)domain_separator[0U] + 1U); Eurydice_arr_91 seed2 = libcrux_ml_dsa_sample_add_error_domain_separator(Eurydice_array_to_slice_shared_17(seed), (uint32_t)domain_separator[0U] + 2U); Eurydice_arr_91 seed3 = libcrux_ml_dsa_sample_add_error_domain_separator(Eurydice_array_to_slice_shared_17(seed), (uint32_t)domain_separator[0U] + 3U); domain_separator[0U] = (uint32_t)domain_separator[0U] + 4U; switch (gamma1_exponent) { case 17U: { Eurydice_arr_220 out0 = { .data = { 0U } }; Eurydice_arr_220 out1 = { .data = { 0U } }; Eurydice_arr_220 out2 = { .data = { 0U } }; Eurydice_arr_220 out3 = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_x4_9b_5a(Eurydice_array_to_slice_shared_f1(&seed0), Eurydice_array_to_slice_shared_f1(&seed1), Eurydice_array_to_slice_shared_f1(&seed2), Eurydice_array_to_slice_shared_f1(&seed3), &out0, &out1, &out2, &out3); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_8a0(&out0), mask.ptr); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_8a0(&out1), &mask.ptr[1U]); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_8a0(&out2), &mask.ptr[2U]); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_8a0(&out3), &mask.ptr[3U]); break; } case 19U: { Eurydice_arr_20 out0 = { .data = { 0U } }; Eurydice_arr_20 out1 = { .data = { 0U } }; Eurydice_arr_20 out2 = { .data = { 0U } }; Eurydice_arr_20 out3 = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_x4_9b_0e(Eurydice_array_to_slice_shared_f1(&seed0), Eurydice_array_to_slice_shared_f1(&seed1), Eurydice_array_to_slice_shared_f1(&seed2), Eurydice_array_to_slice_shared_f1(&seed3), &out0, &out1, &out2, &out3); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_4f(&out0), mask.ptr); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_4f(&out1), &mask.ptr[1U]); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_4f(&out2), &mask.ptr[2U]); libcrux_ml_dsa_encoding_gamma1_deserialize_37(gamma1_exponent, Eurydice_array_to_slice_shared_4f(&out3), &mask.ptr[3U]); break; } default: { KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n", __FILE__, __LINE__, "panic!"); KRML_HOST_EXIT(255U); } } for (size_t i = (size_t)4U; i < dimension; i++) { size_t i0 = i; Eurydice_arr_91 seed4 = libcrux_ml_dsa_sample_add_error_domain_separator(Eurydice_array_to_slice_shared_17(seed), domain_separator[0U]); domain_separator[0U] = (uint32_t)domain_separator[0U] + 1U; libcrux_ml_dsa_sample_sample_mask_ring_element_2e(&seed4, &mask.ptr[i0], gamma1_exponent); } } /** A monomorphic instance of libcrux_ml_dsa.sample.sample_challenge_ring_element with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_hash_functions_portable_Shake256 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_sample_sample_challenge_ring_element_2e( Eurydice_borrow_slice_u8 seed, size_t number_of_ones, Eurydice_arr_a3 *re ) { Eurydice_arr_7c state = libcrux_ml_dsa_hash_functions_portable_init_absorb_final_61(seed); Eurydice_arr_ff randomness0 = libcrux_ml_dsa_hash_functions_portable_squeeze_first_block_61(&state); Eurydice_array_u8x8 arr; memcpy(arr.data, Eurydice_array_to_subslice_shared_d4(&randomness0, (KRML_CLITERAL(core_ops_range_Range_87){ .start = (size_t)0U, .end = (size_t)8U })).ptr, (size_t)8U * sizeof (uint8_t)); uint64_t signs = core_num__u64__from_le_bytes(core_result_unwrap_26_e0(( KRML_CLITERAL(core_result_Result_8e){ .tag = core_result_Ok, .val = { .case_Ok = arr } } ))); Eurydice_arr_6c result = { .data = { 0U } }; size_t out_index = (size_t)256U - number_of_ones; bool done = libcrux_ml_dsa_sample_inside_out_shuffle(Eurydice_array_to_subslice_from_shared_5f(&randomness0, (size_t)8U), &out_index, &signs, &result); while (true) { if (done) { break; } else { Eurydice_arr_ff randomness = libcrux_ml_dsa_hash_functions_portable_squeeze_next_block_61(&state); done = libcrux_ml_dsa_sample_inside_out_shuffle(Eurydice_array_to_slice_shared_58(&randomness), &out_index, &signs, &result); } } libcrux_ml_dsa_polynomial_from_i32_array_ff_37(Eurydice_array_to_slice_shared_af(&result), re); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.sign_internal with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_internal_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, core_option_Option_84 domain_separation_context, Eurydice_arr_ec randomness, Eurydice_arr_85 *signature ) { Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(signing_key, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 remaining_serialized0 = uu____0.snd; Eurydice_borrow_slice_u8_x2 uu____1 = Eurydice_slice_split_at(remaining_serialized0, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_SIGNING_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_signing = uu____1.fst; Eurydice_borrow_slice_u8 remaining_serialized1 = uu____1.snd; Eurydice_borrow_slice_u8_x2 uu____2 = Eurydice_slice_split_at(remaining_serialized1, LIBCRUX_ML_DSA_CONSTANTS_BYTES_FOR_VERIFICATION_KEY_HASH, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 verification_key_hash = uu____2.fst; Eurydice_borrow_slice_u8 remaining_serialized2 = uu____2.snd; Eurydice_borrow_slice_u8_x2 uu____3 = Eurydice_slice_split_at(remaining_serialized2, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_ERROR_RING_ELEMENT_SIZE * LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 s1_serialized = uu____3.fst; Eurydice_borrow_slice_u8 remaining_serialized = uu____3.snd; Eurydice_borrow_slice_u8_x2 uu____4 = Eurydice_slice_split_at(remaining_serialized, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_ERROR_RING_ELEMENT_SIZE * LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 s2_serialized = uu____4.fst; Eurydice_borrow_slice_u8 t0_serialized = uu____4.snd; Eurydice_arr_9d s1_as_ntt; Eurydice_arr_a3 repeat_expression0[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_as_ntt.data, repeat_expression0, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_arr_9d s2_as_ntt; Eurydice_arr_a3 repeat_expression1[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s2_as_ntt.data, repeat_expression1, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_arr_9d t0_as_ntt; Eurydice_arr_a3 repeat_expression2[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression2[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t0_as_ntt.data, repeat_expression2, (size_t)4U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_encoding_error_deserialize_to_vector_then_ntt_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_ERROR_RING_ELEMENT_SIZE, s1_serialized, Eurydice_array_to_slice_mut_201(&s1_as_ntt)); libcrux_ml_dsa_encoding_error_deserialize_to_vector_then_ntt_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_ERROR_RING_ELEMENT_SIZE, s2_serialized, Eurydice_array_to_slice_mut_201(&s2_as_ntt)); libcrux_ml_dsa_encoding_t0_deserialize_to_vector_then_ntt_37(t0_serialized, Eurydice_array_to_slice_mut_201(&t0_as_ntt)); Eurydice_arr_2f matrix; Eurydice_arr_a3 repeat_expression3[16U]; KRML_MAYBE_FOR16(i, (size_t)0U, (size_t)16U, (size_t)1U, repeat_expression3[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(matrix.data, repeat_expression3, (size_t)16U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_200(&matrix)); Eurydice_arr_c7 message_representative = { .data = { 0U } }; libcrux_ml_dsa_ml_dsa_generic_derive_message_representative_43(verification_key_hash, &domain_separation_context, message, &message_representative); Eurydice_arr_c7 mask_seed = { .data = { 0U } }; libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake0 = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake0, seed_for_signing); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake0, Eurydice_array_to_slice_shared_01(&randomness)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake0, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake0, Eurydice_array_to_slice_mut_17(&mask_seed)); uint16_t domain_separator_for_mask = 0U; size_t attempt = (size_t)0U; core_option_Option_14 commitment_hash0 = { .tag = core_option_None }; core_option_Option_d9 signer_response0 = { .tag = core_option_None }; core_option_Option_51 hint0 = { .tag = core_option_None }; while (attempt < LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN) { attempt++; Eurydice_arr_9d mask; Eurydice_arr_a3 repeat_expression4[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression4[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(mask.data, repeat_expression4, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_arr_9d w0; Eurydice_arr_a3 repeat_expression5[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression5[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(w0.data, repeat_expression5, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_arr_9d commitment; Eurydice_arr_a3 repeat_expression6[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression6[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(commitment.data, repeat_expression6, (size_t)4U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_sample_sample_mask_vector_67(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA1_EXPONENT, &mask_seed, &domain_separator_for_mask, Eurydice_array_to_slice_mut_201(&mask)); Eurydice_arr_9d a_x_mask; Eurydice_arr_a3 repeat_expression[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(a_x_mask.data, repeat_expression, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_arr_9d mask_ntt = core_array__core__clone__Clone_for__T__N___clone((size_t)4U, &mask, Eurydice_arr_a3, Eurydice_arr_9d); KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&mask_ntt.data[i0]);); libcrux_ml_dsa_matrix_compute_matrix_x_mask_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, Eurydice_array_to_slice_shared_201(&matrix), Eurydice_array_to_slice_shared_20(&mask_ntt), Eurydice_array_to_slice_mut_201(&a_x_mask)); libcrux_ml_dsa_arithmetic_decompose_vector_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA2, Eurydice_array_to_slice_shared_20(&a_x_mask), Eurydice_array_to_slice_mut_201(&w0), Eurydice_array_to_slice_mut_201(&commitment)); Eurydice_arr_ec commitment_hash_candidate = { .data = { 0U } }; Eurydice_arr_d2 commitment_serialized = { .data = { 0U } }; libcrux_ml_dsa_encoding_commitment_serialize_vector_37(LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_COMMITMENT_RING_ELEMENT_SIZE, Eurydice_array_to_slice_shared_20(&commitment), Eurydice_array_to_slice_mut_27(&commitment_serialized)); libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_27(&commitment_serialized)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_01(&commitment_hash_candidate)); Eurydice_arr_a3 verifier_challenge = libcrux_ml_dsa_polynomial_zero_ff_37(); libcrux_ml_dsa_sample_sample_challenge_ring_element_2e(Eurydice_array_to_slice_shared_01(&commitment_hash_candidate), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ONES_IN_VERIFIER_CHALLENGE, &verifier_challenge); libcrux_ml_dsa_ntt_ntt_37(&verifier_challenge); Eurydice_arr_9d challenge_times_s1 = core_array__core__clone__Clone_for__T__N___clone((size_t)4U, &s1_as_ntt, Eurydice_arr_a3, Eurydice_arr_9d); Eurydice_arr_9d challenge_times_s2 = core_array__core__clone__Clone_for__T__N___clone((size_t)4U, &s2_as_ntt, Eurydice_arr_a3, Eurydice_arr_9d); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_201(&challenge_times_s1), &verifier_challenge); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_201(&challenge_times_s2), &verifier_challenge); libcrux_ml_dsa_matrix_add_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, Eurydice_array_to_slice_mut_201(&mask), Eurydice_array_to_slice_shared_20(&challenge_times_s1)); libcrux_ml_dsa_matrix_subtract_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, Eurydice_array_to_slice_mut_201(&w0), Eurydice_array_to_slice_shared_20(&challenge_times_s2)); if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_20(&mask), (int32_t)((uint32_t)1 << (uint32_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA1_EXPONENT) - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_BETA) ) { if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_20(&w0), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA2 - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_BETA) ) { Eurydice_arr_9d challenge_times_t0 = core_array__core__clone__Clone_for__T__N___clone((size_t)4U, &t0_as_ntt, Eurydice_arr_a3, Eurydice_arr_9d); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_201(&challenge_times_t0), &verifier_challenge); if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_20(&challenge_times_t0), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA2) ) { libcrux_ml_dsa_matrix_add_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, Eurydice_array_to_slice_mut_201(&w0), Eurydice_array_to_slice_shared_20(&challenge_times_t0)); Eurydice_arr_b7 hint_candidate = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; size_t ones_in_hint = libcrux_ml_dsa_arithmetic_make_hint_37(Eurydice_array_to_slice_shared_20(&w0), Eurydice_array_to_slice_shared_20(&commitment), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA2, Eurydice_array_to_slice_mut_86(&hint_candidate)); if (!(ones_in_hint > LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_MAX_ONES_IN_HINT)) { attempt = LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN; commitment_hash0 = ( KRML_CLITERAL(core_option_Option_14){ .tag = core_option_Some, .f0 = commitment_hash_candidate } ); signer_response0 = (KRML_CLITERAL(core_option_Option_d9){ .tag = core_option_Some, .f0 = mask }); hint0 = ( KRML_CLITERAL(core_option_Option_51){ .tag = core_option_Some, .f0 = hint_candidate } ); } } } } } core_result_Result_53 uu____5; if (commitment_hash0.tag == core_option_None) { uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } else { Eurydice_arr_ec commitment_hash = commitment_hash0.f0; Eurydice_arr_ec commitment_hash1 = commitment_hash; if (signer_response0.tag == core_option_None) { uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } else { Eurydice_arr_9d signer_response = signer_response0.f0; Eurydice_arr_9d signer_response1 = signer_response; if (!(hint0.tag == core_option_None)) { Eurydice_arr_b7 hint = hint0.f0; Eurydice_arr_b7 hint1 = hint; libcrux_ml_dsa_encoding_signature_serialize_37(Eurydice_array_to_slice_shared_01(&commitment_hash1), Eurydice_array_to_slice_shared_20(&signer_response1), Eurydice_array_to_slice_shared_86(&hint1), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COMMITMENT_HASH_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA1_EXPONENT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_GAMMA1_RING_ELEMENT_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_MAX_ONES_IN_HINT, Eurydice_array_to_slice_mut_0d(signature)); return (KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Ok }); } uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } } return uu____5; } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.sign_mut with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_mut_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness, Eurydice_arr_85 *signature ) { core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, (KRML_CLITERAL(core_option_Option_57){ .tag = core_option_None })); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_internal_5a(signing_key, message, ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), randomness, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.sign with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_48 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness ) { Eurydice_arr_85 signature = libcrux_ml_dsa_types_zero_c5_37(); core_result_Result_53 uu____0 = libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_mut_5a(signing_key, message, context, randomness, &signature); core_result_Result_48 uu____1; if (uu____0.tag == core_result_Ok) { uu____1 = ( KRML_CLITERAL(core_result_Result_48){ .tag = core_result_Ok, .val = { .case_Ok = signature } } ); } else { libcrux_ml_dsa_types_SigningError e = uu____0.f0; uu____1 = (KRML_CLITERAL(core_result_Result_48){ .tag = core_result_Err, .val = { .case_Err = e } }); } return uu____1; } /** Sign. */ core_result_Result_48 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_44_sign( const Eurydice_arr_10 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_5a(Eurydice_array_to_slice_shared_34(signing_key), message, context, randomness); } /** Sign. */ core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_44_sign_mut( const Eurydice_arr_10 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness, Eurydice_arr_85 *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_mut_5a(Eurydice_array_to_slice_shared_34(signing_key), message, context, randomness, signature); } /** This function found in impl {libcrux_ml_dsa::pre_hash::PreHash for libcrux_ml_dsa::pre_hash::SHAKE128_PH} */ /** A monomorphic instance of libcrux_ml_dsa.pre_hash.hash_30 with types libcrux_ml_dsa_hash_functions_portable_Shake128 with const generics */ void libcrux_ml_dsa_pre_hash_hash_30_83( Eurydice_borrow_slice_u8 message, Eurydice_mut_borrow_slice_u8 output ) { libcrux_ml_dsa_hash_functions_portable_shake128_7b(message, output); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.sign_pre_hashed_mut with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_pre_hashed_mut_3f( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness, Eurydice_arr_85 *signature ) { if (!(context.meta > LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN)) { libcrux_ml_dsa_pre_hash_hash_30_83(message, pre_hash_buffer); core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, ( KRML_CLITERAL(core_option_Option_57){ .tag = core_option_Some, .f0 = libcrux_ml_dsa_pre_hash_oid_30() } )); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_internal_5a(signing_key, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = pre_hash_buffer.ptr, .meta = pre_hash_buffer.meta } ), ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), randomness, signature); } return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.sign_pre_hashed with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_48 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_pre_hashed_3f( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness ) { Eurydice_arr_85 signature = libcrux_ml_dsa_types_zero_c5_37(); core_result_Result_53 uu____0 = libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_pre_hashed_mut_3f(signing_key, message, context, pre_hash_buffer, randomness, &signature); core_result_Result_48 uu____1; if (uu____0.tag == core_result_Ok) { uu____1 = ( KRML_CLITERAL(core_result_Result_48){ .tag = core_result_Ok, .val = { .case_Ok = signature } } ); } else { libcrux_ml_dsa_types_SigningError e = uu____0.f0; uu____1 = (KRML_CLITERAL(core_result_Result_48){ .tag = core_result_Err, .val = { .case_Err = e } }); } return uu____1; } /** Sign (pre-hashed). */ core_result_Result_48 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_44_sign_pre_hashed_shake128( const Eurydice_arr_10 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_sign_pre_hashed_3f(Eurydice_array_to_slice_shared_34(signing_key), message, context, pre_hash_buffer, randomness); } /** The internal verification API. If no `domain_separation_context` is supplied, it is assumed that `message` already contains the domain separation. */ /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.verify_internal with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_verify_internal_5a( const Eurydice_arr_02 *verification_key, Eurydice_borrow_slice_u8 message, core_option_Option_84 domain_separation_context, const Eurydice_arr_85 *signature_serialized ) { Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(Eurydice_array_to_slice_shared_9f(verification_key), LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 t1_serialized = uu____0.snd; Eurydice_arr_9d t1; Eurydice_arr_a3 repeat_expression0[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t1.data, repeat_expression0, (size_t)4U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_encoding_verification_key_deserialize_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_VERIFICATION_KEY_SIZE, t1_serialized, Eurydice_array_to_slice_mut_201(&t1)); Eurydice_arr_ec deserialized_commitment_hash = { .data = { 0U } }; Eurydice_arr_9d deserialized_signer_response; Eurydice_arr_a3 repeat_expression1[4U]; KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(deserialized_signer_response.data, repeat_expression1, (size_t)4U * sizeof (Eurydice_arr_a3)); Eurydice_arr_b7 deserialized_hint = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; core_result_Result_41 uu____1 = libcrux_ml_dsa_encoding_signature_deserialize_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COMMITMENT_HASH_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA1_EXPONENT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_GAMMA1_RING_ELEMENT_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_MAX_ONES_IN_HINT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_SIGNATURE_SIZE, Eurydice_array_to_slice_shared_0d(signature_serialized), Eurydice_array_to_slice_mut_01(&deserialized_commitment_hash), Eurydice_array_to_slice_mut_201(&deserialized_signer_response), Eurydice_array_to_slice_mut_86(&deserialized_hint)); core_result_Result_41 uu____2; if (uu____1.tag == core_result_Ok) { if ( libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_20(&deserialized_signer_response), (int32_t)((uint32_t)1 << (uint32_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA1_EXPONENT) - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_BETA) ) { uu____2 = ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_SignerResponseExceedsBoundError } ); } else { Eurydice_arr_2f matrix; Eurydice_arr_a3 repeat_expression[16U]; KRML_MAYBE_FOR16(i, (size_t)0U, (size_t)16U, (size_t)1U, repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(matrix.data, repeat_expression, (size_t)16U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_200(&matrix)); Eurydice_arr_c7 verification_key_hash = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_61_c9(Eurydice_array_to_slice_shared_9f(verification_key), &verification_key_hash); Eurydice_arr_c7 message_representative = { .data = { 0U } }; libcrux_ml_dsa_ml_dsa_generic_derive_message_representative_43(Eurydice_array_to_slice_shared_17(&verification_key_hash), &domain_separation_context, message, &message_representative); Eurydice_arr_a3 verifier_challenge = libcrux_ml_dsa_polynomial_zero_ff_37(); libcrux_ml_dsa_sample_sample_challenge_ring_element_2e(Eurydice_array_to_slice_shared_01(&deserialized_commitment_hash), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ONES_IN_VERIFIER_CHALLENGE, &verifier_challenge); libcrux_ml_dsa_ntt_ntt_37(&verifier_challenge); KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&deserialized_signer_response.data[i0]);); libcrux_ml_dsa_matrix_compute_w_approx_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_COLUMNS_IN_A, Eurydice_array_to_slice_shared_201(&matrix), Eurydice_array_to_slice_shared_20(&deserialized_signer_response), &verifier_challenge, Eurydice_array_to_slice_mut_201(&t1)); Eurydice_arr_ec recomputed_commitment_hash = { .data = { 0U } }; libcrux_ml_dsa_arithmetic_use_hint_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_44_GAMMA2, Eurydice_array_to_slice_shared_86(&deserialized_hint), Eurydice_array_to_slice_mut_201(&t1)); Eurydice_arr_d2 commitment_serialized = { .data = { 0U } }; libcrux_ml_dsa_encoding_commitment_serialize_vector_37(LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_44_COMMITMENT_RING_ELEMENT_SIZE, Eurydice_array_to_slice_shared_20(&t1), Eurydice_array_to_slice_mut_27(&commitment_serialized)); libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_27(&commitment_serialized)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_01(&recomputed_commitment_hash)); if ( Eurydice_array_eq((size_t)32U, &deserialized_commitment_hash, &recomputed_commitment_hash, uint8_t) ) { uu____2 = (KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Ok }); } else { uu____2 = ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_CommitmentHashesDontMatchError } ); } } } else { libcrux_ml_dsa_types_VerificationError e = uu____1.f0; uu____2 = (KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = e }); } return uu____2; } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.verify with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_verify_5a( const Eurydice_arr_02 *verification_key_serialized, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, const Eurydice_arr_85 *signature_serialized ) { core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, (KRML_CLITERAL(core_option_Option_57){ .tag = core_option_None })); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_verify_internal_5a(verification_key_serialized, message, ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), signature_serialized); } /** Verify. */ core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_44_verify( const Eurydice_arr_02 *verification_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, const Eurydice_arr_85 *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_verify_5a(verification_key, message, context, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_44.verify_pre_hashed with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_verify_pre_hashed_3f( const Eurydice_arr_02 *verification_key_serialized, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, const Eurydice_arr_85 *signature_serialized ) { libcrux_ml_dsa_pre_hash_hash_30_83(message, pre_hash_buffer); core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, ( KRML_CLITERAL(core_option_Option_57){ .tag = core_option_Some, .f0 = libcrux_ml_dsa_pre_hash_oid_30() } )); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_verify_internal_5a(verification_key_serialized, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = pre_hash_buffer.ptr, .meta = pre_hash_buffer.meta } ), ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), signature_serialized); } /** Verify (pre-hashed with SHAKE-128). */ core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_44_verify_pre_hashed_shake128( const Eurydice_arr_02 *verification_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, const Eurydice_arr_85 *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_44_verify_pre_hashed_3f(verification_key, message, context, pre_hash_buffer, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.generate_key_pair with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_generate_key_pair_5a( Eurydice_arr_ec randomness, Eurydice_mut_borrow_slice_u8 signing_key, Eurydice_mut_borrow_slice_u8 verification_key ) { Eurydice_arr_89 seed_expanded0 = { .data = { 0U } }; libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_01(&randomness)); /* original Rust expression is not an lvalue in C */ Eurydice_array_u8x2 lvalue = { .data = { (uint8_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, (uint8_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A } }; libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_82(&lvalue)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_78(&seed_expanded0)); Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(Eurydice_array_to_slice_shared_78(&seed_expanded0), LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 seed_expanded = uu____0.snd; Eurydice_borrow_slice_u8_x2 uu____1 = Eurydice_slice_split_at(seed_expanded, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_ERROR_VECTORS_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_error_vectors = uu____1.fst; Eurydice_borrow_slice_u8 seed_for_signing = uu____1.snd; Eurydice_arr_47 s1_s2; Eurydice_arr_a3 repeat_expression0[11U]; KRML_MAYBE_FOR11(i, (size_t)0U, (size_t)11U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_s2.data, repeat_expression0, (size_t)11U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_sample_s1_and_s2_29(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ETA, seed_for_error_vectors, Eurydice_array_to_slice_mut_202(&s1_s2)); Eurydice_arr_dc1 t0; Eurydice_arr_a3 repeat_expression1[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t0.data, repeat_expression1, (size_t)6U * sizeof (Eurydice_arr_a3)); Eurydice_arr_5a a_as_ntt; Eurydice_arr_a3 repeat_expression2[30U]; for (size_t i = (size_t)0U; i < (size_t)30U; i++) { repeat_expression2[i] = libcrux_ml_dsa_polynomial_zero_ff_37(); } memcpy(a_as_ntt.data, repeat_expression2, (size_t)30U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_203(&a_as_ntt)); Eurydice_arr_5d s1_ntt; Eurydice_arr_a3 repeat_expression3[5U]; KRML_MAYBE_FOR5(i, (size_t)0U, (size_t)5U, (size_t)1U, repeat_expression3[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_ntt.data, repeat_expression3, (size_t)5U * sizeof (Eurydice_arr_a3)); Eurydice_slice_copy(Eurydice_array_to_slice_mut_204(&s1_ntt), Eurydice_array_to_subslice_shared_250(&s1_s2, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = (size_t)0U, .end = LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A } )), Eurydice_arr_a3); KRML_MAYBE_FOR5(i, (size_t)0U, (size_t)5U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&s1_ntt.data[i0]);); libcrux_ml_dsa_matrix_compute_as1_plus_s2_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, Eurydice_array_to_slice_mut_203(&a_as_ntt), Eurydice_array_to_slice_shared_202(&s1_ntt), Eurydice_array_to_slice_shared_203(&s1_s2), Eurydice_array_to_slice_mut_205(&t0)); Eurydice_arr_dc1 t1; Eurydice_arr_a3 repeat_expression[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t1.data, repeat_expression, (size_t)6U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_arithmetic_power2round_vector_37(Eurydice_array_to_slice_mut_205(&t0), Eurydice_array_to_slice_mut_205(&t1)); libcrux_ml_dsa_encoding_verification_key_generate_serialized_37(seed_for_a, Eurydice_array_to_slice_shared_204(&t1), verification_key); libcrux_ml_dsa_encoding_signing_key_generate_serialized_2e(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_ERROR_RING_ELEMENT_SIZE, seed_for_a, seed_for_signing, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = verification_key.ptr, .meta = verification_key.meta } ), Eurydice_array_to_slice_shared_203(&s1_s2), Eurydice_array_to_slice_shared_204(&t0), signing_key); } /** Generate key pair. */ void libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_65_generate_key_pair( Eurydice_arr_ec randomness, Eurydice_arr_24 *signing_key, Eurydice_arr_29 *verification_key ) { libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_generate_key_pair_5a(randomness, Eurydice_array_to_slice_mut_98(signing_key), Eurydice_array_to_slice_mut_37(verification_key)); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.sign_internal with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_internal_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, core_option_Option_84 domain_separation_context, Eurydice_arr_ec randomness, Eurydice_arr_0c *signature ) { Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(signing_key, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 remaining_serialized0 = uu____0.snd; Eurydice_borrow_slice_u8_x2 uu____1 = Eurydice_slice_split_at(remaining_serialized0, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_SIGNING_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_signing = uu____1.fst; Eurydice_borrow_slice_u8 remaining_serialized1 = uu____1.snd; Eurydice_borrow_slice_u8_x2 uu____2 = Eurydice_slice_split_at(remaining_serialized1, LIBCRUX_ML_DSA_CONSTANTS_BYTES_FOR_VERIFICATION_KEY_HASH, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 verification_key_hash = uu____2.fst; Eurydice_borrow_slice_u8 remaining_serialized2 = uu____2.snd; Eurydice_borrow_slice_u8_x2 uu____3 = Eurydice_slice_split_at(remaining_serialized2, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_ERROR_RING_ELEMENT_SIZE * LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 s1_serialized = uu____3.fst; Eurydice_borrow_slice_u8 remaining_serialized = uu____3.snd; Eurydice_borrow_slice_u8_x2 uu____4 = Eurydice_slice_split_at(remaining_serialized, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_ERROR_RING_ELEMENT_SIZE * LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 s2_serialized = uu____4.fst; Eurydice_borrow_slice_u8 t0_serialized = uu____4.snd; Eurydice_arr_5d s1_as_ntt; Eurydice_arr_a3 repeat_expression0[5U]; KRML_MAYBE_FOR5(i, (size_t)0U, (size_t)5U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_as_ntt.data, repeat_expression0, (size_t)5U * sizeof (Eurydice_arr_a3)); Eurydice_arr_dc1 s2_as_ntt; Eurydice_arr_a3 repeat_expression1[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s2_as_ntt.data, repeat_expression1, (size_t)6U * sizeof (Eurydice_arr_a3)); Eurydice_arr_dc1 t0_as_ntt; Eurydice_arr_a3 repeat_expression2[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression2[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t0_as_ntt.data, repeat_expression2, (size_t)6U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_encoding_error_deserialize_to_vector_then_ntt_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_ERROR_RING_ELEMENT_SIZE, s1_serialized, Eurydice_array_to_slice_mut_204(&s1_as_ntt)); libcrux_ml_dsa_encoding_error_deserialize_to_vector_then_ntt_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_ERROR_RING_ELEMENT_SIZE, s2_serialized, Eurydice_array_to_slice_mut_205(&s2_as_ntt)); libcrux_ml_dsa_encoding_t0_deserialize_to_vector_then_ntt_37(t0_serialized, Eurydice_array_to_slice_mut_205(&t0_as_ntt)); Eurydice_arr_5a matrix; Eurydice_arr_a3 repeat_expression3[30U]; for (size_t i = (size_t)0U; i < (size_t)30U; i++) { repeat_expression3[i] = libcrux_ml_dsa_polynomial_zero_ff_37(); } memcpy(matrix.data, repeat_expression3, (size_t)30U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_203(&matrix)); Eurydice_arr_c7 message_representative = { .data = { 0U } }; libcrux_ml_dsa_ml_dsa_generic_derive_message_representative_43(verification_key_hash, &domain_separation_context, message, &message_representative); Eurydice_arr_c7 mask_seed = { .data = { 0U } }; libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake0 = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake0, seed_for_signing); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake0, Eurydice_array_to_slice_shared_01(&randomness)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake0, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake0, Eurydice_array_to_slice_mut_17(&mask_seed)); uint16_t domain_separator_for_mask = 0U; size_t attempt = (size_t)0U; core_option_Option_81 commitment_hash0 = { .tag = core_option_None }; core_option_Option_1e signer_response0 = { .tag = core_option_None }; core_option_Option_05 hint0 = { .tag = core_option_None }; while (attempt < LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN) { attempt++; Eurydice_arr_5d mask; Eurydice_arr_a3 repeat_expression4[5U]; KRML_MAYBE_FOR5(i, (size_t)0U, (size_t)5U, (size_t)1U, repeat_expression4[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(mask.data, repeat_expression4, (size_t)5U * sizeof (Eurydice_arr_a3)); Eurydice_arr_dc1 w0; Eurydice_arr_a3 repeat_expression5[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression5[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(w0.data, repeat_expression5, (size_t)6U * sizeof (Eurydice_arr_a3)); Eurydice_arr_dc1 commitment; Eurydice_arr_a3 repeat_expression6[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression6[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(commitment.data, repeat_expression6, (size_t)6U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_sample_sample_mask_vector_67(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA1_EXPONENT, &mask_seed, &domain_separator_for_mask, Eurydice_array_to_slice_mut_204(&mask)); Eurydice_arr_dc1 a_x_mask; Eurydice_arr_a3 repeat_expression[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(a_x_mask.data, repeat_expression, (size_t)6U * sizeof (Eurydice_arr_a3)); Eurydice_arr_5d mask_ntt = core_array__core__clone__Clone_for__T__N___clone((size_t)5U, &mask, Eurydice_arr_a3, Eurydice_arr_5d); KRML_MAYBE_FOR5(i, (size_t)0U, (size_t)5U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&mask_ntt.data[i0]);); libcrux_ml_dsa_matrix_compute_matrix_x_mask_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, Eurydice_array_to_slice_shared_205(&matrix), Eurydice_array_to_slice_shared_202(&mask_ntt), Eurydice_array_to_slice_mut_205(&a_x_mask)); libcrux_ml_dsa_arithmetic_decompose_vector_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA2, Eurydice_array_to_slice_shared_204(&a_x_mask), Eurydice_array_to_slice_mut_205(&w0), Eurydice_array_to_slice_mut_205(&commitment)); Eurydice_arr_65 commitment_hash_candidate = { .data = { 0U } }; Eurydice_arr_d2 commitment_serialized = { .data = { 0U } }; libcrux_ml_dsa_encoding_commitment_serialize_vector_37(LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_COMMITMENT_RING_ELEMENT_SIZE, Eurydice_array_to_slice_shared_204(&commitment), Eurydice_array_to_slice_mut_27(&commitment_serialized)); libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_27(&commitment_serialized)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_9f(&commitment_hash_candidate)); Eurydice_arr_a3 verifier_challenge = libcrux_ml_dsa_polynomial_zero_ff_37(); libcrux_ml_dsa_sample_sample_challenge_ring_element_2e(Eurydice_array_to_slice_shared_9f0(&commitment_hash_candidate), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ONES_IN_VERIFIER_CHALLENGE, &verifier_challenge); libcrux_ml_dsa_ntt_ntt_37(&verifier_challenge); Eurydice_arr_5d challenge_times_s1 = core_array__core__clone__Clone_for__T__N___clone((size_t)5U, &s1_as_ntt, Eurydice_arr_a3, Eurydice_arr_5d); Eurydice_arr_dc1 challenge_times_s2 = core_array__core__clone__Clone_for__T__N___clone((size_t)6U, &s2_as_ntt, Eurydice_arr_a3, Eurydice_arr_dc1); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_204(&challenge_times_s1), &verifier_challenge); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_205(&challenge_times_s2), &verifier_challenge); libcrux_ml_dsa_matrix_add_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, Eurydice_array_to_slice_mut_204(&mask), Eurydice_array_to_slice_shared_202(&challenge_times_s1)); libcrux_ml_dsa_matrix_subtract_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, Eurydice_array_to_slice_mut_205(&w0), Eurydice_array_to_slice_shared_204(&challenge_times_s2)); if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_202(&mask), (int32_t)((uint32_t)1 << (uint32_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA1_EXPONENT) - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_BETA) ) { if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_204(&w0), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA2 - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_BETA) ) { Eurydice_arr_dc1 challenge_times_t0 = core_array__core__clone__Clone_for__T__N___clone((size_t)6U, &t0_as_ntt, Eurydice_arr_a3, Eurydice_arr_dc1); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_205(&challenge_times_t0), &verifier_challenge); if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_204(&challenge_times_t0), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA2) ) { libcrux_ml_dsa_matrix_add_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, Eurydice_array_to_slice_mut_205(&w0), Eurydice_array_to_slice_shared_204(&challenge_times_t0)); Eurydice_arr_5d0 hint_candidate = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; size_t ones_in_hint = libcrux_ml_dsa_arithmetic_make_hint_37(Eurydice_array_to_slice_shared_204(&w0), Eurydice_array_to_slice_shared_204(&commitment), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA2, Eurydice_array_to_slice_mut_860(&hint_candidate)); if (!(ones_in_hint > LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_MAX_ONES_IN_HINT)) { attempt = LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN; commitment_hash0 = ( KRML_CLITERAL(core_option_Option_81){ .tag = core_option_Some, .f0 = commitment_hash_candidate } ); signer_response0 = (KRML_CLITERAL(core_option_Option_1e){ .tag = core_option_Some, .f0 = mask }); hint0 = ( KRML_CLITERAL(core_option_Option_05){ .tag = core_option_Some, .f0 = hint_candidate } ); } } } } } core_result_Result_53 uu____5; if (commitment_hash0.tag == core_option_None) { uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } else { Eurydice_arr_65 commitment_hash = commitment_hash0.f0; Eurydice_arr_65 commitment_hash1 = commitment_hash; if (signer_response0.tag == core_option_None) { uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } else { Eurydice_arr_5d signer_response = signer_response0.f0; Eurydice_arr_5d signer_response1 = signer_response; if (!(hint0.tag == core_option_None)) { Eurydice_arr_5d0 hint = hint0.f0; Eurydice_arr_5d0 hint1 = hint; libcrux_ml_dsa_encoding_signature_serialize_37(Eurydice_array_to_slice_shared_9f0(&commitment_hash1), Eurydice_array_to_slice_shared_202(&signer_response1), Eurydice_array_to_slice_shared_860(&hint1), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COMMITMENT_HASH_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA1_EXPONENT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_GAMMA1_RING_ELEMENT_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_MAX_ONES_IN_HINT, Eurydice_array_to_slice_mut_6b(signature)); return (KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Ok }); } uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } } return uu____5; } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.sign_mut with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_mut_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness, Eurydice_arr_0c *signature ) { core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, (KRML_CLITERAL(core_option_Option_57){ .tag = core_option_None })); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_internal_5a(signing_key, message, ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), randomness, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.sign with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_8c libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness ) { Eurydice_arr_0c signature = libcrux_ml_dsa_types_zero_c5_5c(); core_result_Result_53 uu____0 = libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_mut_5a(signing_key, message, context, randomness, &signature); core_result_Result_8c uu____1; if (uu____0.tag == core_result_Ok) { uu____1 = ( KRML_CLITERAL(core_result_Result_8c){ .tag = core_result_Ok, .val = { .case_Ok = signature } } ); } else { libcrux_ml_dsa_types_SigningError e = uu____0.f0; uu____1 = (KRML_CLITERAL(core_result_Result_8c){ .tag = core_result_Err, .val = { .case_Err = e } }); } return uu____1; } /** Sign. */ core_result_Result_8c libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_65_sign( const Eurydice_arr_24 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_5a(Eurydice_array_to_slice_shared_98(signing_key), message, context, randomness); } /** Sign. */ core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_65_sign_mut( const Eurydice_arr_24 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness, Eurydice_arr_0c *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_mut_5a(Eurydice_array_to_slice_shared_98(signing_key), message, context, randomness, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.sign_pre_hashed_mut with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_pre_hashed_mut_3f( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness, Eurydice_arr_0c *signature ) { if (!(context.meta > LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN)) { libcrux_ml_dsa_pre_hash_hash_30_83(message, pre_hash_buffer); core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, ( KRML_CLITERAL(core_option_Option_57){ .tag = core_option_Some, .f0 = libcrux_ml_dsa_pre_hash_oid_30() } )); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_internal_5a(signing_key, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = pre_hash_buffer.ptr, .meta = pre_hash_buffer.meta } ), ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), randomness, signature); } return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.sign_pre_hashed with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_8c libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_pre_hashed_3f( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness ) { Eurydice_arr_0c signature = libcrux_ml_dsa_types_zero_c5_5c(); core_result_Result_53 uu____0 = libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_pre_hashed_mut_3f(signing_key, message, context, pre_hash_buffer, randomness, &signature); core_result_Result_8c uu____1; if (uu____0.tag == core_result_Ok) { uu____1 = ( KRML_CLITERAL(core_result_Result_8c){ .tag = core_result_Ok, .val = { .case_Ok = signature } } ); } else { libcrux_ml_dsa_types_SigningError e = uu____0.f0; uu____1 = (KRML_CLITERAL(core_result_Result_8c){ .tag = core_result_Err, .val = { .case_Err = e } }); } return uu____1; } /** Sign (pre-hashed). */ core_result_Result_8c libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_65_sign_pre_hashed_shake128( const Eurydice_arr_24 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_sign_pre_hashed_3f(Eurydice_array_to_slice_shared_98(signing_key), message, context, pre_hash_buffer, randomness); } /** The internal verification API. If no `domain_separation_context` is supplied, it is assumed that `message` already contains the domain separation. */ /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.verify_internal with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_verify_internal_5a( const Eurydice_arr_29 *verification_key, Eurydice_borrow_slice_u8 message, core_option_Option_84 domain_separation_context, const Eurydice_arr_0c *signature_serialized ) { Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(Eurydice_array_to_slice_shared_37(verification_key), LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 t1_serialized = uu____0.snd; Eurydice_arr_dc1 t1; Eurydice_arr_a3 repeat_expression0[6U]; KRML_MAYBE_FOR6(i, (size_t)0U, (size_t)6U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t1.data, repeat_expression0, (size_t)6U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_encoding_verification_key_deserialize_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_VERIFICATION_KEY_SIZE, t1_serialized, Eurydice_array_to_slice_mut_205(&t1)); Eurydice_arr_65 deserialized_commitment_hash = { .data = { 0U } }; Eurydice_arr_5d deserialized_signer_response; Eurydice_arr_a3 repeat_expression1[5U]; KRML_MAYBE_FOR5(i, (size_t)0U, (size_t)5U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(deserialized_signer_response.data, repeat_expression1, (size_t)5U * sizeof (Eurydice_arr_a3)); Eurydice_arr_5d0 deserialized_hint = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; core_result_Result_41 uu____1 = libcrux_ml_dsa_encoding_signature_deserialize_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COMMITMENT_HASH_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA1_EXPONENT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_GAMMA1_RING_ELEMENT_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_MAX_ONES_IN_HINT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_SIGNATURE_SIZE, Eurydice_array_to_slice_shared_6b(signature_serialized), Eurydice_array_to_slice_mut_9f(&deserialized_commitment_hash), Eurydice_array_to_slice_mut_204(&deserialized_signer_response), Eurydice_array_to_slice_mut_860(&deserialized_hint)); core_result_Result_41 uu____2; if (uu____1.tag == core_result_Ok) { if ( libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_202(&deserialized_signer_response), (int32_t)((uint32_t)1 << (uint32_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA1_EXPONENT) - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_BETA) ) { uu____2 = ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_SignerResponseExceedsBoundError } ); } else { Eurydice_arr_5a matrix; Eurydice_arr_a3 repeat_expression[30U]; for (size_t i = (size_t)0U; i < (size_t)30U; i++) { repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37(); } memcpy(matrix.data, repeat_expression, (size_t)30U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_203(&matrix)); Eurydice_arr_c7 verification_key_hash = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_61_c9(Eurydice_array_to_slice_shared_37(verification_key), &verification_key_hash); Eurydice_arr_c7 message_representative = { .data = { 0U } }; libcrux_ml_dsa_ml_dsa_generic_derive_message_representative_43(Eurydice_array_to_slice_shared_17(&verification_key_hash), &domain_separation_context, message, &message_representative); Eurydice_arr_a3 verifier_challenge = libcrux_ml_dsa_polynomial_zero_ff_37(); libcrux_ml_dsa_sample_sample_challenge_ring_element_2e(Eurydice_array_to_slice_shared_9f0(&deserialized_commitment_hash), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ONES_IN_VERIFIER_CHALLENGE, &verifier_challenge); libcrux_ml_dsa_ntt_ntt_37(&verifier_challenge); KRML_MAYBE_FOR5(i, (size_t)0U, (size_t)5U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&deserialized_signer_response.data[i0]);); libcrux_ml_dsa_matrix_compute_w_approx_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_COLUMNS_IN_A, Eurydice_array_to_slice_shared_205(&matrix), Eurydice_array_to_slice_shared_202(&deserialized_signer_response), &verifier_challenge, Eurydice_array_to_slice_mut_205(&t1)); Eurydice_arr_65 recomputed_commitment_hash = { .data = { 0U } }; libcrux_ml_dsa_arithmetic_use_hint_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_65_GAMMA2, Eurydice_array_to_slice_shared_860(&deserialized_hint), Eurydice_array_to_slice_mut_205(&t1)); Eurydice_arr_d2 commitment_serialized = { .data = { 0U } }; libcrux_ml_dsa_encoding_commitment_serialize_vector_37(LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_65_COMMITMENT_RING_ELEMENT_SIZE, Eurydice_array_to_slice_shared_204(&t1), Eurydice_array_to_slice_mut_27(&commitment_serialized)); libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_27(&commitment_serialized)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_9f(&recomputed_commitment_hash)); if ( Eurydice_array_eq((size_t)48U, &deserialized_commitment_hash, &recomputed_commitment_hash, uint8_t) ) { uu____2 = (KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Ok }); } else { uu____2 = ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_CommitmentHashesDontMatchError } ); } } } else { libcrux_ml_dsa_types_VerificationError e = uu____1.f0; uu____2 = (KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = e }); } return uu____2; } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.verify with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_verify_5a( const Eurydice_arr_29 *verification_key_serialized, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, const Eurydice_arr_0c *signature_serialized ) { core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, (KRML_CLITERAL(core_option_Option_57){ .tag = core_option_None })); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_verify_internal_5a(verification_key_serialized, message, ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), signature_serialized); } /** Verify. */ core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_65_verify( const Eurydice_arr_29 *verification_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, const Eurydice_arr_0c *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_verify_5a(verification_key, message, context, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_65.verify_pre_hashed with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_verify_pre_hashed_3f( const Eurydice_arr_29 *verification_key_serialized, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, const Eurydice_arr_0c *signature_serialized ) { libcrux_ml_dsa_pre_hash_hash_30_83(message, pre_hash_buffer); core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, ( KRML_CLITERAL(core_option_Option_57){ .tag = core_option_Some, .f0 = libcrux_ml_dsa_pre_hash_oid_30() } )); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_verify_internal_5a(verification_key_serialized, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = pre_hash_buffer.ptr, .meta = pre_hash_buffer.meta } ), ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), signature_serialized); } /** Verify (pre-hashed with SHAKE-128). */ core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_65_verify_pre_hashed_shake128( const Eurydice_arr_29 *verification_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, const Eurydice_arr_0c *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_65_verify_pre_hashed_3f(verification_key, message, context, pre_hash_buffer, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.generate_key_pair with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE void libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_generate_key_pair_5a( Eurydice_arr_ec randomness, Eurydice_mut_borrow_slice_u8 signing_key, Eurydice_mut_borrow_slice_u8 verification_key ) { Eurydice_arr_89 seed_expanded0 = { .data = { 0U } }; libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_01(&randomness)); /* original Rust expression is not an lvalue in C */ Eurydice_array_u8x2 lvalue = { .data = { (uint8_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, (uint8_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A } }; libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_82(&lvalue)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_78(&seed_expanded0)); Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(Eurydice_array_to_slice_shared_78(&seed_expanded0), LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 seed_expanded = uu____0.snd; Eurydice_borrow_slice_u8_x2 uu____1 = Eurydice_slice_split_at(seed_expanded, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_ERROR_VECTORS_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_error_vectors = uu____1.fst; Eurydice_borrow_slice_u8 seed_for_signing = uu____1.snd; Eurydice_arr_92 s1_s2; Eurydice_arr_a3 repeat_expression0[15U]; KRML_MAYBE_FOR15(i, (size_t)0U, (size_t)15U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_s2.data, repeat_expression0, (size_t)15U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_sample_s1_and_s2_29(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ETA, seed_for_error_vectors, Eurydice_array_to_slice_mut_206(&s1_s2)); Eurydice_arr_8f t0; Eurydice_arr_a3 repeat_expression1[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t0.data, repeat_expression1, (size_t)8U * sizeof (Eurydice_arr_a3)); Eurydice_arr_0f a_as_ntt; Eurydice_arr_a3 repeat_expression2[56U]; for (size_t i = (size_t)0U; i < (size_t)56U; i++) { repeat_expression2[i] = libcrux_ml_dsa_polynomial_zero_ff_37(); } memcpy(a_as_ntt.data, repeat_expression2, (size_t)56U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_207(&a_as_ntt)); Eurydice_arr_bb s1_ntt; Eurydice_arr_a3 repeat_expression3[7U]; KRML_MAYBE_FOR7(i, (size_t)0U, (size_t)7U, (size_t)1U, repeat_expression3[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_ntt.data, repeat_expression3, (size_t)7U * sizeof (Eurydice_arr_a3)); Eurydice_slice_copy(Eurydice_array_to_slice_mut_208(&s1_ntt), Eurydice_array_to_subslice_shared_251(&s1_s2, ( KRML_CLITERAL(core_ops_range_Range_87){ .start = (size_t)0U, .end = LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A } )), Eurydice_arr_a3); KRML_MAYBE_FOR7(i, (size_t)0U, (size_t)7U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&s1_ntt.data[i0]);); libcrux_ml_dsa_matrix_compute_as1_plus_s2_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, Eurydice_array_to_slice_mut_207(&a_as_ntt), Eurydice_array_to_slice_shared_206(&s1_ntt), Eurydice_array_to_slice_shared_207(&s1_s2), Eurydice_array_to_slice_mut_20(&t0)); Eurydice_arr_8f t1; Eurydice_arr_a3 repeat_expression[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t1.data, repeat_expression, (size_t)8U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_arithmetic_power2round_vector_37(Eurydice_array_to_slice_mut_20(&t0), Eurydice_array_to_slice_mut_20(&t1)); libcrux_ml_dsa_encoding_verification_key_generate_serialized_37(seed_for_a, Eurydice_array_to_slice_shared_200(&t1), verification_key); libcrux_ml_dsa_encoding_signing_key_generate_serialized_2e(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_ERROR_RING_ELEMENT_SIZE, seed_for_a, seed_for_signing, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = verification_key.ptr, .meta = verification_key.meta } ), Eurydice_array_to_slice_shared_207(&s1_s2), Eurydice_array_to_slice_shared_200(&t0), signing_key); } /** Generate key pair. */ void libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_87_generate_key_pair( Eurydice_arr_ec randomness, Eurydice_arr_e2 *signing_key, Eurydice_arr_43 *verification_key ) { libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_generate_key_pair_5a(randomness, Eurydice_array_to_slice_mut_f7(signing_key), Eurydice_array_to_slice_mut_fc(verification_key)); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.sign_internal with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_internal_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, core_option_Option_84 domain_separation_context, Eurydice_arr_ec randomness, Eurydice_arr_93 *signature ) { Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(signing_key, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 remaining_serialized0 = uu____0.snd; Eurydice_borrow_slice_u8_x2 uu____1 = Eurydice_slice_split_at(remaining_serialized0, LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_SIGNING_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_signing = uu____1.fst; Eurydice_borrow_slice_u8 remaining_serialized1 = uu____1.snd; Eurydice_borrow_slice_u8_x2 uu____2 = Eurydice_slice_split_at(remaining_serialized1, LIBCRUX_ML_DSA_CONSTANTS_BYTES_FOR_VERIFICATION_KEY_HASH, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 verification_key_hash = uu____2.fst; Eurydice_borrow_slice_u8 remaining_serialized2 = uu____2.snd; Eurydice_borrow_slice_u8_x2 uu____3 = Eurydice_slice_split_at(remaining_serialized2, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_ERROR_RING_ELEMENT_SIZE * LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 s1_serialized = uu____3.fst; Eurydice_borrow_slice_u8 remaining_serialized = uu____3.snd; Eurydice_borrow_slice_u8_x2 uu____4 = Eurydice_slice_split_at(remaining_serialized, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_ERROR_RING_ELEMENT_SIZE * LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 s2_serialized = uu____4.fst; Eurydice_borrow_slice_u8 t0_serialized = uu____4.snd; Eurydice_arr_bb s1_as_ntt; Eurydice_arr_a3 repeat_expression0[7U]; KRML_MAYBE_FOR7(i, (size_t)0U, (size_t)7U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s1_as_ntt.data, repeat_expression0, (size_t)7U * sizeof (Eurydice_arr_a3)); Eurydice_arr_8f s2_as_ntt; Eurydice_arr_a3 repeat_expression1[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(s2_as_ntt.data, repeat_expression1, (size_t)8U * sizeof (Eurydice_arr_a3)); Eurydice_arr_8f t0_as_ntt; Eurydice_arr_a3 repeat_expression2[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression2[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t0_as_ntt.data, repeat_expression2, (size_t)8U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_encoding_error_deserialize_to_vector_then_ntt_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_ERROR_RING_ELEMENT_SIZE, s1_serialized, Eurydice_array_to_slice_mut_208(&s1_as_ntt)); libcrux_ml_dsa_encoding_error_deserialize_to_vector_then_ntt_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ETA, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_ERROR_RING_ELEMENT_SIZE, s2_serialized, Eurydice_array_to_slice_mut_20(&s2_as_ntt)); libcrux_ml_dsa_encoding_t0_deserialize_to_vector_then_ntt_37(t0_serialized, Eurydice_array_to_slice_mut_20(&t0_as_ntt)); Eurydice_arr_0f matrix; Eurydice_arr_a3 repeat_expression3[56U]; for (size_t i = (size_t)0U; i < (size_t)56U; i++) { repeat_expression3[i] = libcrux_ml_dsa_polynomial_zero_ff_37(); } memcpy(matrix.data, repeat_expression3, (size_t)56U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_207(&matrix)); Eurydice_arr_c7 message_representative = { .data = { 0U } }; libcrux_ml_dsa_ml_dsa_generic_derive_message_representative_43(verification_key_hash, &domain_separation_context, message, &message_representative); Eurydice_arr_c7 mask_seed = { .data = { 0U } }; libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake0 = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake0, seed_for_signing); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake0, Eurydice_array_to_slice_shared_01(&randomness)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake0, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake0, Eurydice_array_to_slice_mut_17(&mask_seed)); uint16_t domain_separator_for_mask = 0U; size_t attempt = (size_t)0U; core_option_Option_b2 commitment_hash0 = { .tag = core_option_None }; core_option_Option_2d signer_response0 = { .tag = core_option_None }; core_option_Option_45 hint0 = { .tag = core_option_None }; while (attempt < LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN) { attempt++; Eurydice_arr_bb mask; Eurydice_arr_a3 repeat_expression4[7U]; KRML_MAYBE_FOR7(i, (size_t)0U, (size_t)7U, (size_t)1U, repeat_expression4[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(mask.data, repeat_expression4, (size_t)7U * sizeof (Eurydice_arr_a3)); Eurydice_arr_8f w0; Eurydice_arr_a3 repeat_expression5[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression5[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(w0.data, repeat_expression5, (size_t)8U * sizeof (Eurydice_arr_a3)); Eurydice_arr_8f commitment; Eurydice_arr_a3 repeat_expression6[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression6[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(commitment.data, repeat_expression6, (size_t)8U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_sample_sample_mask_vector_67(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA1_EXPONENT, &mask_seed, &domain_separator_for_mask, Eurydice_array_to_slice_mut_208(&mask)); Eurydice_arr_8f a_x_mask; Eurydice_arr_a3 repeat_expression[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(a_x_mask.data, repeat_expression, (size_t)8U * sizeof (Eurydice_arr_a3)); Eurydice_arr_bb mask_ntt = core_array__core__clone__Clone_for__T__N___clone((size_t)7U, &mask, Eurydice_arr_a3, Eurydice_arr_bb); KRML_MAYBE_FOR7(i, (size_t)0U, (size_t)7U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&mask_ntt.data[i0]);); libcrux_ml_dsa_matrix_compute_matrix_x_mask_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, Eurydice_array_to_slice_shared_208(&matrix), Eurydice_array_to_slice_shared_206(&mask_ntt), Eurydice_array_to_slice_mut_20(&a_x_mask)); libcrux_ml_dsa_arithmetic_decompose_vector_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA2, Eurydice_array_to_slice_shared_200(&a_x_mask), Eurydice_array_to_slice_mut_20(&w0), Eurydice_array_to_slice_mut_20(&commitment)); Eurydice_arr_c7 commitment_hash_candidate = { .data = { 0U } }; Eurydice_arr_1b commitment_serialized = { .data = { 0U } }; libcrux_ml_dsa_encoding_commitment_serialize_vector_37(LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_COMMITMENT_RING_ELEMENT_SIZE, Eurydice_array_to_slice_shared_200(&commitment), Eurydice_array_to_slice_mut_68(&commitment_serialized)); libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_68(&commitment_serialized)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_17(&commitment_hash_candidate)); Eurydice_arr_a3 verifier_challenge = libcrux_ml_dsa_polynomial_zero_ff_37(); libcrux_ml_dsa_sample_sample_challenge_ring_element_2e(Eurydice_array_to_slice_shared_17(&commitment_hash_candidate), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ONES_IN_VERIFIER_CHALLENGE, &verifier_challenge); libcrux_ml_dsa_ntt_ntt_37(&verifier_challenge); Eurydice_arr_bb challenge_times_s1 = core_array__core__clone__Clone_for__T__N___clone((size_t)7U, &s1_as_ntt, Eurydice_arr_a3, Eurydice_arr_bb); Eurydice_arr_8f challenge_times_s2 = core_array__core__clone__Clone_for__T__N___clone((size_t)8U, &s2_as_ntt, Eurydice_arr_a3, Eurydice_arr_8f); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_208(&challenge_times_s1), &verifier_challenge); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_20(&challenge_times_s2), &verifier_challenge); libcrux_ml_dsa_matrix_add_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, Eurydice_array_to_slice_mut_208(&mask), Eurydice_array_to_slice_shared_206(&challenge_times_s1)); libcrux_ml_dsa_matrix_subtract_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, Eurydice_array_to_slice_mut_20(&w0), Eurydice_array_to_slice_shared_200(&challenge_times_s2)); if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_206(&mask), (int32_t)((uint32_t)1 << (uint32_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA1_EXPONENT) - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_BETA) ) { if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_200(&w0), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA2 - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_BETA) ) { Eurydice_arr_8f challenge_times_t0 = core_array__core__clone__Clone_for__T__N___clone((size_t)8U, &t0_as_ntt, Eurydice_arr_a3, Eurydice_arr_8f); libcrux_ml_dsa_matrix_vector_times_ring_element_37(Eurydice_array_to_slice_mut_20(&challenge_times_t0), &verifier_challenge); if ( !libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_200(&challenge_times_t0), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA2) ) { libcrux_ml_dsa_matrix_add_vectors_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, Eurydice_array_to_slice_mut_20(&w0), Eurydice_array_to_slice_shared_200(&challenge_times_t0)); Eurydice_arr_81 hint_candidate = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; size_t ones_in_hint = libcrux_ml_dsa_arithmetic_make_hint_37(Eurydice_array_to_slice_shared_200(&w0), Eurydice_array_to_slice_shared_200(&commitment), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA2, Eurydice_array_to_slice_mut_861(&hint_candidate)); if (!(ones_in_hint > LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_MAX_ONES_IN_HINT)) { attempt = LIBCRUX_ML_DSA_CONSTANTS_REJECTION_SAMPLE_BOUND_SIGN; commitment_hash0 = ( KRML_CLITERAL(core_option_Option_b2){ .tag = core_option_Some, .f0 = commitment_hash_candidate } ); signer_response0 = (KRML_CLITERAL(core_option_Option_2d){ .tag = core_option_Some, .f0 = mask }); hint0 = ( KRML_CLITERAL(core_option_Option_45){ .tag = core_option_Some, .f0 = hint_candidate } ); } } } } } core_result_Result_53 uu____5; if (commitment_hash0.tag == core_option_None) { uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } else { Eurydice_arr_c7 commitment_hash = commitment_hash0.f0; Eurydice_arr_c7 commitment_hash1 = commitment_hash; if (signer_response0.tag == core_option_None) { uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } else { Eurydice_arr_bb signer_response = signer_response0.f0; Eurydice_arr_bb signer_response1 = signer_response; if (!(hint0.tag == core_option_None)) { Eurydice_arr_81 hint = hint0.f0; Eurydice_arr_81 hint1 = hint; libcrux_ml_dsa_encoding_signature_serialize_37(Eurydice_array_to_slice_shared_17(&commitment_hash1), Eurydice_array_to_slice_shared_206(&signer_response1), Eurydice_array_to_slice_shared_861(&hint1), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COMMITMENT_HASH_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA1_EXPONENT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_GAMMA1_RING_ELEMENT_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_MAX_ONES_IN_HINT, Eurydice_array_to_slice_mut_11(signature)); return (KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Ok }); } uu____5 = ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_RejectionSamplingError } ); } } return uu____5; } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.sign_mut with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_mut_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness, Eurydice_arr_93 *signature ) { core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, (KRML_CLITERAL(core_option_Option_57){ .tag = core_option_None })); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_internal_5a(signing_key, message, ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), randomness, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.sign with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4 with const generics */ KRML_MUSTINLINE core_result_Result_8b libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_5a( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness ) { Eurydice_arr_93 signature = libcrux_ml_dsa_types_zero_c5_f1(); core_result_Result_53 uu____0 = libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_mut_5a(signing_key, message, context, randomness, &signature); core_result_Result_8b uu____1; if (uu____0.tag == core_result_Ok) { uu____1 = ( KRML_CLITERAL(core_result_Result_8b){ .tag = core_result_Ok, .val = { .case_Ok = signature } } ); } else { libcrux_ml_dsa_types_SigningError e = uu____0.f0; uu____1 = (KRML_CLITERAL(core_result_Result_8b){ .tag = core_result_Err, .val = { .case_Err = e } }); } return uu____1; } /** Sign. */ core_result_Result_8b libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_87_sign( const Eurydice_arr_e2 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_5a(Eurydice_array_to_slice_shared_f7(signing_key), message, context, randomness); } /** Sign. */ core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_87_sign_mut( const Eurydice_arr_e2 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_arr_ec randomness, Eurydice_arr_93 *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_mut_5a(Eurydice_array_to_slice_shared_f7(signing_key), message, context, randomness, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.sign_pre_hashed_mut with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_53 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_pre_hashed_mut_3f( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness, Eurydice_arr_93 *signature ) { if (!(context.meta > LIBCRUX_ML_DSA_CONSTANTS_CONTEXT_MAX_LEN)) { libcrux_ml_dsa_pre_hash_hash_30_83(message, pre_hash_buffer); core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, ( KRML_CLITERAL(core_option_Option_57){ .tag = core_option_Some, .f0 = libcrux_ml_dsa_pre_hash_oid_30() } )); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_internal_5a(signing_key, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = pre_hash_buffer.ptr, .meta = pre_hash_buffer.meta } ), ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), randomness, signature); } return ( KRML_CLITERAL(core_result_Result_53){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_SigningError_ContextTooLongError } ); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.sign_pre_hashed with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_hash_functions_portable_Shake256X4, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_8b libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_pre_hashed_3f( Eurydice_borrow_slice_u8 signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness ) { Eurydice_arr_93 signature = libcrux_ml_dsa_types_zero_c5_f1(); core_result_Result_53 uu____0 = libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_pre_hashed_mut_3f(signing_key, message, context, pre_hash_buffer, randomness, &signature); core_result_Result_8b uu____1; if (uu____0.tag == core_result_Ok) { uu____1 = ( KRML_CLITERAL(core_result_Result_8b){ .tag = core_result_Ok, .val = { .case_Ok = signature } } ); } else { libcrux_ml_dsa_types_SigningError e = uu____0.f0; uu____1 = (KRML_CLITERAL(core_result_Result_8b){ .tag = core_result_Err, .val = { .case_Err = e } }); } return uu____1; } /** Sign (pre-hashed). */ core_result_Result_8b libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_87_sign_pre_hashed_shake128( const Eurydice_arr_e2 *signing_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, Eurydice_arr_ec randomness ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_sign_pre_hashed_3f(Eurydice_array_to_slice_shared_f7(signing_key), message, context, pre_hash_buffer, randomness); } /** The internal verification API. If no `domain_separation_context` is supplied, it is assumed that `message` already contains the domain separation. */ /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.verify_internal with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_verify_internal_5a( const Eurydice_arr_43 *verification_key, Eurydice_borrow_slice_u8 message, core_option_Option_84 domain_separation_context, const Eurydice_arr_93 *signature_serialized ) { Eurydice_borrow_slice_u8_x2 uu____0 = Eurydice_slice_split_at(Eurydice_array_to_slice_shared_fc(verification_key), LIBCRUX_ML_DSA_CONSTANTS_SEED_FOR_A_SIZE, uint8_t, Eurydice_borrow_slice_u8_x2); Eurydice_borrow_slice_u8 seed_for_a = uu____0.fst; Eurydice_borrow_slice_u8 t1_serialized = uu____0.snd; Eurydice_arr_8f t1; Eurydice_arr_a3 repeat_expression0[8U]; KRML_MAYBE_FOR8(i, (size_t)0U, (size_t)8U, (size_t)1U, repeat_expression0[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(t1.data, repeat_expression0, (size_t)8U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_encoding_verification_key_deserialize_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_VERIFICATION_KEY_SIZE, t1_serialized, Eurydice_array_to_slice_mut_20(&t1)); Eurydice_arr_c7 deserialized_commitment_hash = { .data = { 0U } }; Eurydice_arr_bb deserialized_signer_response; Eurydice_arr_a3 repeat_expression1[7U]; KRML_MAYBE_FOR7(i, (size_t)0U, (size_t)7U, (size_t)1U, repeat_expression1[i] = libcrux_ml_dsa_polynomial_zero_ff_37();); memcpy(deserialized_signer_response.data, repeat_expression1, (size_t)7U * sizeof (Eurydice_arr_a3)); Eurydice_arr_81 deserialized_hint = { .data = { { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } }, { .data = { 0U } } } }; core_result_Result_41 uu____1 = libcrux_ml_dsa_encoding_signature_deserialize_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COMMITMENT_HASH_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA1_EXPONENT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_GAMMA1_RING_ELEMENT_SIZE, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_MAX_ONES_IN_HINT, LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_SIGNATURE_SIZE, Eurydice_array_to_slice_shared_11(signature_serialized), Eurydice_array_to_slice_mut_17(&deserialized_commitment_hash), Eurydice_array_to_slice_mut_208(&deserialized_signer_response), Eurydice_array_to_slice_mut_861(&deserialized_hint)); core_result_Result_41 uu____2; if (uu____1.tag == core_result_Ok) { if ( libcrux_ml_dsa_arithmetic_vector_infinity_norm_exceeds_37(Eurydice_array_to_slice_shared_206(&deserialized_signer_response), (int32_t)((uint32_t)1 << (uint32_t)LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA1_EXPONENT) - LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_BETA) ) { uu____2 = ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_SignerResponseExceedsBoundError } ); } else { Eurydice_arr_0f matrix; Eurydice_arr_a3 repeat_expression[56U]; for (size_t i = (size_t)0U; i < (size_t)56U; i++) { repeat_expression[i] = libcrux_ml_dsa_polynomial_zero_ff_37(); } memcpy(matrix.data, repeat_expression, (size_t)56U * sizeof (Eurydice_arr_a3)); libcrux_ml_dsa_samplex4_portable_matrix_flat_a8_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, seed_for_a, Eurydice_array_to_slice_mut_207(&matrix)); Eurydice_arr_c7 verification_key_hash = { .data = { 0U } }; libcrux_ml_dsa_hash_functions_portable_shake256_61_c9(Eurydice_array_to_slice_shared_fc(verification_key), &verification_key_hash); Eurydice_arr_c7 message_representative = { .data = { 0U } }; libcrux_ml_dsa_ml_dsa_generic_derive_message_representative_43(Eurydice_array_to_slice_shared_17(&verification_key_hash), &domain_separation_context, message, &message_representative); Eurydice_arr_a3 verifier_challenge = libcrux_ml_dsa_polynomial_zero_ff_37(); libcrux_ml_dsa_sample_sample_challenge_ring_element_2e(Eurydice_array_to_slice_shared_17(&deserialized_commitment_hash), LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ONES_IN_VERIFIER_CHALLENGE, &verifier_challenge); libcrux_ml_dsa_ntt_ntt_37(&verifier_challenge); KRML_MAYBE_FOR7(i, (size_t)0U, (size_t)7U, (size_t)1U, size_t i0 = i; libcrux_ml_dsa_ntt_ntt_37(&deserialized_signer_response.data[i0]);); libcrux_ml_dsa_matrix_compute_w_approx_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_ROWS_IN_A, LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_COLUMNS_IN_A, Eurydice_array_to_slice_shared_208(&matrix), Eurydice_array_to_slice_shared_206(&deserialized_signer_response), &verifier_challenge, Eurydice_array_to_slice_mut_20(&t1)); Eurydice_arr_c7 recomputed_commitment_hash = { .data = { 0U } }; libcrux_ml_dsa_arithmetic_use_hint_37(LIBCRUX_ML_DSA_CONSTANTS_ML_DSA_87_GAMMA2, Eurydice_array_to_slice_shared_861(&deserialized_hint), Eurydice_array_to_slice_mut_20(&t1)); Eurydice_arr_1b commitment_serialized = { .data = { 0U } }; libcrux_ml_dsa_encoding_commitment_serialize_vector_37(LIBCRUX_ML_DSA_ML_DSA_GENERIC_ML_DSA_87_COMMITMENT_RING_ELEMENT_SIZE, Eurydice_array_to_slice_shared_200(&t1), Eurydice_array_to_slice_mut_68(&commitment_serialized)); libcrux_sha3_generic_keccak_xof_KeccakXofState_8d shake = libcrux_ml_dsa_hash_functions_portable_init_26(); libcrux_ml_dsa_hash_functions_portable_absorb_26(&shake, Eurydice_array_to_slice_shared_17(&message_representative)); libcrux_ml_dsa_hash_functions_portable_absorb_final_26(&shake, Eurydice_array_to_slice_shared_68(&commitment_serialized)); libcrux_ml_dsa_hash_functions_portable_squeeze_26(&shake, Eurydice_array_to_slice_mut_17(&recomputed_commitment_hash)); if ( Eurydice_array_eq((size_t)64U, &deserialized_commitment_hash, &recomputed_commitment_hash, uint8_t) ) { uu____2 = (KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Ok }); } else { uu____2 = ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_CommitmentHashesDontMatchError } ); } } } else { libcrux_ml_dsa_types_VerificationError e = uu____1.f0; uu____2 = (KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = e }); } return uu____2; } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.verify with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_verify_5a( const Eurydice_arr_43 *verification_key_serialized, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, const Eurydice_arr_93 *signature_serialized ) { core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, (KRML_CLITERAL(core_option_Option_57){ .tag = core_option_None })); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_verify_internal_5a(verification_key_serialized, message, ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), signature_serialized); } /** Verify. */ core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_87_verify( const Eurydice_arr_43 *verification_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, const Eurydice_arr_93 *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_verify_5a(verification_key, message, context, signature); } /** A monomorphic instance of libcrux_ml_dsa.ml_dsa_generic.ml_dsa_87.verify_pre_hashed with types libcrux_ml_dsa_simd_portable_vector_type_Coefficients, libcrux_ml_dsa_samplex4_portable_PortableSampler, libcrux_ml_dsa_hash_functions_portable_Shake128, libcrux_ml_dsa_hash_functions_portable_Shake128X4, libcrux_ml_dsa_hash_functions_portable_Shake256, libcrux_ml_dsa_hash_functions_portable_Shake256Xof, libcrux_ml_dsa_pre_hash_SHAKE128_PH with const generics */ KRML_MUSTINLINE core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_verify_pre_hashed_3f( const Eurydice_arr_43 *verification_key_serialized, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, const Eurydice_arr_93 *signature_serialized ) { libcrux_ml_dsa_pre_hash_hash_30_83(message, pre_hash_buffer); core_result_Result_a8 uu____0 = libcrux_ml_dsa_pre_hash_new_88(context, ( KRML_CLITERAL(core_option_Option_57){ .tag = core_option_Some, .f0 = libcrux_ml_dsa_pre_hash_oid_30() } )); if (!(uu____0.tag == core_result_Ok)) { return ( KRML_CLITERAL(core_result_Result_41){ .tag = core_result_Err, .f0 = libcrux_ml_dsa_types_VerificationError_VerificationContextTooLongError } ); } libcrux_ml_dsa_pre_hash_DomainSeparationContext dsc = uu____0.val.case_Ok; libcrux_ml_dsa_pre_hash_DomainSeparationContext domain_separation_context = dsc; return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_verify_internal_5a(verification_key_serialized, ( KRML_CLITERAL(Eurydice_borrow_slice_u8){ .ptr = pre_hash_buffer.ptr, .meta = pre_hash_buffer.meta } ), ( KRML_CLITERAL(core_option_Option_84){ .tag = core_option_Some, .f0 = domain_separation_context } ), signature_serialized); } /** Verify (pre-hashed with SHAKE-128). */ core_result_Result_41 libcrux_ml_dsa_ml_dsa_generic_instantiations_portable_ml_dsa_87_verify_pre_hashed_shake128( const Eurydice_arr_43 *verification_key, Eurydice_borrow_slice_u8 message, Eurydice_borrow_slice_u8 context, Eurydice_mut_borrow_slice_u8 pre_hash_buffer, const Eurydice_arr_93 *signature ) { return libcrux_ml_dsa_ml_dsa_generic_ml_dsa_87_verify_pre_hashed_3f(verification_key, message, context, pre_hash_buffer, signature); }