diff --git a/libcrux-ml-dsa/cg/code_gen.txt b/libcrux-ml-dsa/cg/code_gen.txt index f2323957e..d60b4f857 100644 --- a/libcrux-ml-dsa/cg/code_gen.txt +++ b/libcrux-ml-dsa/cg/code_gen.txt @@ -1,6 +1,6 @@ This code was generated with the following revisions: -Charon: 0de54092afb546bf53cd8261c79499f3cae2c24b -Eurydice: 8e112cd3065d2c1eb6c023cd37111300dbf9fc9a -Karamel: f82ecfe9b99edd64642d47b4e3fb6314a8e2320b +Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25 +Eurydice: 83ab5654d49df0603797bf510475d52d67ca24d8 +Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65 F*: b0961063393215ca65927f017720cb365a193833-dirty -Libcrux: 66afce2b7d2b86febb97fb1fc5de2fbba7419d74 +Libcrux: 31e77d0e773e3d025ffeb024f3f4742d9a2b2eec diff --git a/libcrux-ml-dsa/cg/header.txt b/libcrux-ml-dsa/cg/header.txt index 635d52cd8..afb92c3b1 100644 --- a/libcrux-ml-dsa/cg/header.txt +++ b/libcrux-ml-dsa/cg/header.txt @@ -4,9 +4,9 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 0de54092afb546bf53cd8261c79499f3cae2c24b - * Eurydice: 8e112cd3065d2c1eb6c023cd37111300dbf9fc9a - * Karamel: f82ecfe9b99edd64642d47b4e3fb6314a8e2320b + * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25 + * Eurydice: 83ab5654d49df0603797bf510475d52d67ca24d8 + * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65 * F*: b0961063393215ca65927f017720cb365a193833-dirty - * Libcrux: 66afce2b7d2b86febb97fb1fc5de2fbba7419d74 + * Libcrux: 31e77d0e773e3d025ffeb024f3f4742d9a2b2eec */ diff --git a/libcrux-ml-dsa/cg/libcrux_core.h b/libcrux-ml-dsa/cg/libcrux_core.h index e3d7b8766..8b39b5b53 100644 --- a/libcrux-ml-dsa/cg/libcrux_core.h +++ b/libcrux-ml-dsa/cg/libcrux_core.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 0de54092afb546bf53cd8261c79499f3cae2c24b - * Eurydice: 8e112cd3065d2c1eb6c023cd37111300dbf9fc9a - * Karamel: f82ecfe9b99edd64642d47b4e3fb6314a8e2320b + * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25 + * Eurydice: 83ab5654d49df0603797bf510475d52d67ca24d8 + * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65 * F*: b0961063393215ca65927f017720cb365a193833-dirty - * Libcrux: 66afce2b7d2b86febb97fb1fc5de2fbba7419d74 + * Libcrux: 31e77d0e773e3d025ffeb024f3f4742d9a2b2eec */ #ifndef __libcrux_core_H diff --git a/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h b/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h index 7a3e81dab..a3d520c49 100644 --- a/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h +++ b/libcrux-ml-dsa/cg/libcrux_mldsa65_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 0de54092afb546bf53cd8261c79499f3cae2c24b - * Eurydice: 8e112cd3065d2c1eb6c023cd37111300dbf9fc9a - * Karamel: f82ecfe9b99edd64642d47b4e3fb6314a8e2320b + * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25 + * Eurydice: 83ab5654d49df0603797bf510475d52d67ca24d8 + * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65 * F*: b0961063393215ca65927f017720cb365a193833-dirty - * Libcrux: 66afce2b7d2b86febb97fb1fc5de2fbba7419d74 + * Libcrux: 31e77d0e773e3d025ffeb024f3f4742d9a2b2eec */ #ifndef __libcrux_mldsa65_avx2_H @@ -6487,184 +6487,73 @@ libcrux_ml_dsa_encoding_signature_deserialize_21( libcrux_ml_dsa_polynomial_PolynomialRingElement_4b *)); } size_t previous_true_hints_seen = (size_t)0U; - size_t i0 = (size_t)0U; - bool malformed_hint = false; + core_ops_range_Range_08 iter = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I__1__into_iter( + (CLITERAL(core_ops_range_Range_08){.start = (size_t)0U, + .end = rows_in_a}), + core_ops_range_Range_08, core_ops_range_Range_08); + Result_41 uu____2; while (true) { - if (malformed_hint) { - break; - } else if (i0 < rows_in_a) { + Option_08 uu____3 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( + &iter, size_t, Option_08); + if (uu____3.tag == None) { + for (size_t i = previous_true_hints_seen; i < max_ones_in_hint; i++) { + size_t j = i; + if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) != + 0U) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + break; + } + } + return (CLITERAL(Result_41){.tag = Ok}); + } else { + size_t i0 = uu____3.f0; size_t current_true_hints_seen = (size_t)Eurydice_slice_index( hint_serialized, max_ones_in_hint + i0, uint8_t, uint8_t *); - size_t j; - bool uu____2; - bool uu____3; - size_t uu____4; - size_t uu____5; - bool uu____6; - size_t uu____7; - size_t uu____8; - bool uu____9; - uint8_t uu____10; - size_t uu____11; - uint8_t uu____12; - size_t uu____13; - size_t uu____14; - bool uu____15; - Eurydice_slice uu____16; - size_t uu____17; - size_t uu____18; - uint8_t uu____19; - size_t uu____20; - bool uu____21; - size_t uu____22; - if (!(current_true_hints_seen < previous_true_hints_seen)) { - if (!(previous_true_hints_seen > max_ones_in_hint)) { - j = previous_true_hints_seen; - while (true) { - uu____2 = malformed_hint; - if (uu____2) { + if (current_true_hints_seen < previous_true_hints_seen) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + break; + } else if (previous_true_hints_seen > max_ones_in_hint) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + break; + } else { + for (size_t i = previous_true_hints_seen; i < current_true_hints_seen; + i++) { + size_t j = i; + if (j > previous_true_hints_seen) { + if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) <= + Eurydice_slice_index(hint_serialized, j - (size_t)1U, uint8_t, + uint8_t *)) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = + libcrux_ml_dsa_types_VerificationError_MalformedHintError}); break; } else { - uu____4 = j; - uu____5 = current_true_hints_seen; - uu____3 = uu____4 < uu____5; - if (uu____3) { - uu____7 = j; - uu____8 = previous_true_hints_seen; - uu____6 = uu____7 > uu____8; - if (uu____6) { - uu____11 = j; - uu____10 = Eurydice_slice_index(hint_serialized, uu____11, - uint8_t, uint8_t *); - uu____14 = j; - uu____13 = uu____14 - (size_t)1U; - uu____12 = Eurydice_slice_index(hint_serialized, uu____13, - uint8_t, uint8_t *); - uu____9 = uu____10 <= uu____12; - if (uu____9) { - malformed_hint = true; - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint( - uu____16, uu____17, uu____18); - j++; - } - continue; - } - } - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint(uu____16, uu____17, - uu____18); - j++; - } - } else { - break; - } - } - } - uu____21 = malformed_hint; - if (!uu____21) { - uu____22 = current_true_hints_seen; - previous_true_hints_seen = uu____22; - i0++; - } - continue; - } - } - malformed_hint = true; - j = previous_true_hints_seen; - while (true) { - uu____2 = malformed_hint; - if (uu____2) { - break; - } else { - uu____4 = j; - uu____5 = current_true_hints_seen; - uu____3 = uu____4 < uu____5; - if (uu____3) { - uu____7 = j; - uu____8 = previous_true_hints_seen; - uu____6 = uu____7 > uu____8; - if (uu____6) { - uu____11 = j; - uu____10 = Eurydice_slice_index(hint_serialized, uu____11, - uint8_t, uint8_t *); - uu____14 = j; - uu____13 = uu____14 - (size_t)1U; - uu____12 = Eurydice_slice_index(hint_serialized, uu____13, - uint8_t, uint8_t *); - uu____9 = uu____10 <= uu____12; - if (uu____9) { - malformed_hint = true; - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint(uu____16, uu____17, - uu____18); - j++; - } - continue; - } - } - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint(uu____16, uu____17, - uu____18); - j++; + libcrux_ml_dsa_encoding_signature_set_hint( + out_hint, i0, + (size_t)Eurydice_slice_index(hint_serialized, j, uint8_t, + uint8_t *)); } } else { - break; + libcrux_ml_dsa_encoding_signature_set_hint( + out_hint, i0, + (size_t)Eurydice_slice_index(hint_serialized, j, uint8_t, + uint8_t *)); } } + previous_true_hints_seen = current_true_hints_seen; } - uu____21 = malformed_hint; - if (!uu____21) { - uu____22 = current_true_hints_seen; - previous_true_hints_seen = uu____22; - i0++; - } - } else { - break; } } - i0 = previous_true_hints_seen; - for (size_t i = i0; i < max_ones_in_hint; i++) { - size_t j = i; - if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) != 0U) { - malformed_hint = true; - break; - } - } - if (!malformed_hint) { - return (CLITERAL(Result_41){.tag = Ok}); - } - return (CLITERAL(Result_41){ - .tag = Err, - .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + return uu____2; } /** diff --git a/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h b/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h index 263dd135a..57478cdd3 100644 --- a/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h +++ b/libcrux-ml-dsa/cg/libcrux_mldsa65_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 0de54092afb546bf53cd8261c79499f3cae2c24b - * Eurydice: 8e112cd3065d2c1eb6c023cd37111300dbf9fc9a - * Karamel: f82ecfe9b99edd64642d47b4e3fb6314a8e2320b + * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25 + * Eurydice: 83ab5654d49df0603797bf510475d52d67ca24d8 + * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65 * F*: b0961063393215ca65927f017720cb365a193833-dirty - * Libcrux: 66afce2b7d2b86febb97fb1fc5de2fbba7419d74 + * Libcrux: 31e77d0e773e3d025ffeb024f3f4742d9a2b2eec */ #ifndef __libcrux_mldsa65_portable_H @@ -7525,184 +7525,73 @@ libcrux_ml_dsa_encoding_signature_deserialize_5b( libcrux_ml_dsa_polynomial_PolynomialRingElement_e8 *)); } size_t previous_true_hints_seen = (size_t)0U; - size_t i0 = (size_t)0U; - bool malformed_hint = false; + core_ops_range_Range_08 iter = + core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I__1__into_iter( + (CLITERAL(core_ops_range_Range_08){.start = (size_t)0U, + .end = rows_in_a}), + core_ops_range_Range_08, core_ops_range_Range_08); + Result_41 uu____2; while (true) { - if (malformed_hint) { - break; - } else if (i0 < rows_in_a) { + Option_08 uu____3 = + core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A__TraitClause_0___6__next( + &iter, size_t, Option_08); + if (uu____3.tag == None) { + for (size_t i = previous_true_hints_seen; i < max_ones_in_hint; i++) { + size_t j = i; + if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) != + 0U) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + break; + } + } + return (CLITERAL(Result_41){.tag = Ok}); + } else { + size_t i0 = uu____3.f0; size_t current_true_hints_seen = (size_t)Eurydice_slice_index( hint_serialized, max_ones_in_hint + i0, uint8_t, uint8_t *); - size_t j; - bool uu____2; - bool uu____3; - size_t uu____4; - size_t uu____5; - bool uu____6; - size_t uu____7; - size_t uu____8; - bool uu____9; - uint8_t uu____10; - size_t uu____11; - uint8_t uu____12; - size_t uu____13; - size_t uu____14; - bool uu____15; - Eurydice_slice uu____16; - size_t uu____17; - size_t uu____18; - uint8_t uu____19; - size_t uu____20; - bool uu____21; - size_t uu____22; - if (!(current_true_hints_seen < previous_true_hints_seen)) { - if (!(previous_true_hints_seen > max_ones_in_hint)) { - j = previous_true_hints_seen; - while (true) { - uu____2 = malformed_hint; - if (uu____2) { + if (current_true_hints_seen < previous_true_hints_seen) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + break; + } else if (previous_true_hints_seen > max_ones_in_hint) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + break; + } else { + for (size_t i = previous_true_hints_seen; i < current_true_hints_seen; + i++) { + size_t j = i; + if (j > previous_true_hints_seen) { + if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) <= + Eurydice_slice_index(hint_serialized, j - (size_t)1U, uint8_t, + uint8_t *)) { + uu____2 = (CLITERAL(Result_41){ + .tag = Err, + .f0 = + libcrux_ml_dsa_types_VerificationError_MalformedHintError}); break; } else { - uu____4 = j; - uu____5 = current_true_hints_seen; - uu____3 = uu____4 < uu____5; - if (uu____3) { - uu____7 = j; - uu____8 = previous_true_hints_seen; - uu____6 = uu____7 > uu____8; - if (uu____6) { - uu____11 = j; - uu____10 = Eurydice_slice_index(hint_serialized, uu____11, - uint8_t, uint8_t *); - uu____14 = j; - uu____13 = uu____14 - (size_t)1U; - uu____12 = Eurydice_slice_index(hint_serialized, uu____13, - uint8_t, uint8_t *); - uu____9 = uu____10 <= uu____12; - if (uu____9) { - malformed_hint = true; - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint( - uu____16, uu____17, uu____18); - j++; - } - continue; - } - } - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint(uu____16, uu____17, - uu____18); - j++; - } - } else { - break; - } - } - } - uu____21 = malformed_hint; - if (!uu____21) { - uu____22 = current_true_hints_seen; - previous_true_hints_seen = uu____22; - i0++; - } - continue; - } - } - malformed_hint = true; - j = previous_true_hints_seen; - while (true) { - uu____2 = malformed_hint; - if (uu____2) { - break; - } else { - uu____4 = j; - uu____5 = current_true_hints_seen; - uu____3 = uu____4 < uu____5; - if (uu____3) { - uu____7 = j; - uu____8 = previous_true_hints_seen; - uu____6 = uu____7 > uu____8; - if (uu____6) { - uu____11 = j; - uu____10 = Eurydice_slice_index(hint_serialized, uu____11, - uint8_t, uint8_t *); - uu____14 = j; - uu____13 = uu____14 - (size_t)1U; - uu____12 = Eurydice_slice_index(hint_serialized, uu____13, - uint8_t, uint8_t *); - uu____9 = uu____10 <= uu____12; - if (uu____9) { - malformed_hint = true; - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint(uu____16, uu____17, - uu____18); - j++; - } - continue; - } - } - uu____15 = malformed_hint; - if (!uu____15) { - uu____16 = out_hint; - uu____17 = i0; - uu____20 = j; - uu____19 = Eurydice_slice_index(hint_serialized, uu____20, - uint8_t, uint8_t *); - uu____18 = (size_t)uu____19; - libcrux_ml_dsa_encoding_signature_set_hint(uu____16, uu____17, - uu____18); - j++; + libcrux_ml_dsa_encoding_signature_set_hint( + out_hint, i0, + (size_t)Eurydice_slice_index(hint_serialized, j, uint8_t, + uint8_t *)); } } else { - break; + libcrux_ml_dsa_encoding_signature_set_hint( + out_hint, i0, + (size_t)Eurydice_slice_index(hint_serialized, j, uint8_t, + uint8_t *)); } } + previous_true_hints_seen = current_true_hints_seen; } - uu____21 = malformed_hint; - if (!uu____21) { - uu____22 = current_true_hints_seen; - previous_true_hints_seen = uu____22; - i0++; - } - } else { - break; } } - i0 = previous_true_hints_seen; - for (size_t i = i0; i < max_ones_in_hint; i++) { - size_t j = i; - if (Eurydice_slice_index(hint_serialized, j, uint8_t, uint8_t *) != 0U) { - malformed_hint = true; - break; - } - } - if (!malformed_hint) { - return (CLITERAL(Result_41){.tag = Ok}); - } - return (CLITERAL(Result_41){ - .tag = Err, - .f0 = libcrux_ml_dsa_types_VerificationError_MalformedHintError}); + return uu____2; } /** diff --git a/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h b/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h index 3c48ae1a7..778d3fe10 100644 --- a/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h +++ b/libcrux-ml-dsa/cg/libcrux_sha3_avx2.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 0de54092afb546bf53cd8261c79499f3cae2c24b - * Eurydice: 8e112cd3065d2c1eb6c023cd37111300dbf9fc9a - * Karamel: f82ecfe9b99edd64642d47b4e3fb6314a8e2320b + * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25 + * Eurydice: 83ab5654d49df0603797bf510475d52d67ca24d8 + * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65 * F*: b0961063393215ca65927f017720cb365a193833-dirty - * Libcrux: 66afce2b7d2b86febb97fb1fc5de2fbba7419d74 + * Libcrux: 31e77d0e773e3d025ffeb024f3f4742d9a2b2eec */ #ifndef __libcrux_sha3_avx2_H diff --git a/libcrux-ml-dsa/cg/libcrux_sha3_portable.h b/libcrux-ml-dsa/cg/libcrux_sha3_portable.h index 672b57f1e..e606783eb 100644 --- a/libcrux-ml-dsa/cg/libcrux_sha3_portable.h +++ b/libcrux-ml-dsa/cg/libcrux_sha3_portable.h @@ -4,11 +4,11 @@ * SPDX-License-Identifier: MIT or Apache-2.0 * * This code was generated with the following revisions: - * Charon: 0de54092afb546bf53cd8261c79499f3cae2c24b - * Eurydice: 8e112cd3065d2c1eb6c023cd37111300dbf9fc9a - * Karamel: f82ecfe9b99edd64642d47b4e3fb6314a8e2320b + * Charon: db4e045d4597d06d854ce7a2c10e8dcfda6ecd25 + * Eurydice: 83ab5654d49df0603797bf510475d52d67ca24d8 + * Karamel: 3823e3d82fa0b271d799b61c59ffb4742ddc1e65 * F*: b0961063393215ca65927f017720cb365a193833-dirty - * Libcrux: 66afce2b7d2b86febb97fb1fc5de2fbba7419d74 + * Libcrux: 31e77d0e773e3d025ffeb024f3f4742d9a2b2eec */ #ifndef __libcrux_sha3_portable_H diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst index fc93a51a0..07c14734b 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst @@ -111,132 +111,247 @@ let deserialize t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)) in let previous_true_hints_seen:usize = sz 0 in - let i:usize = sz 0 in - let malformed_hint:bool = false in - let i, malformed_hint, out_hint, previous_true_hints_seen:(usize & bool & - t_Slice (t_Array i32 (sz 256)) & - usize) = - Rust_primitives.f_while_loop (fun temp_0_ -> - let i, malformed_hint, out_hint, previous_true_hints_seen:(usize & bool & - t_Slice (t_Array i32 (sz 256)) & - usize) = + match + Rust_primitives.Hax.Folds.fold_range_return (sz 0) + rows_in_a + (fun temp_0_ temp_1_ -> + let out_hint, previous_true_hints_seen:(t_Slice (t_Array i32 (sz 256)) & usize) = temp_0_ in - (~.malformed_hint <: bool) && (i <. rows_in_a <: bool)) - (i, malformed_hint, out_hint, previous_true_hints_seen - <: - (usize & bool & t_Slice (t_Array i32 (sz 256)) & usize)) - (fun temp_0_ -> - let i, malformed_hint, out_hint, previous_true_hints_seen:(usize & bool & - t_Slice (t_Array i32 (sz 256)) & - usize) = + let _:usize = temp_1_ in + true) + (out_hint, previous_true_hints_seen <: (t_Slice (t_Array i32 (sz 256)) & usize)) + (fun temp_0_ i -> + let out_hint, previous_true_hints_seen:(t_Slice (t_Array i32 (sz 256)) & usize) = temp_0_ in + let i:usize = i in let current_true_hints_seen:usize = cast (hint_serialized.[ max_ones_in_hint +! i <: usize ] <: u8) <: usize in - let malformed_hint:bool = - if - current_true_hints_seen <. previous_true_hints_seen || - previous_true_hints_seen >. max_ones_in_hint - then - let malformed_hint:bool = true in - malformed_hint - else malformed_hint - in - let j:usize = previous_true_hints_seen in - let j, malformed_hint, out_hint:(usize & bool & t_Slice (t_Array i32 (sz 256))) = - Rust_primitives.f_while_loop (fun temp_0_ -> - let j, malformed_hint, out_hint:(usize & bool & t_Slice (t_Array i32 (sz 256))) = - temp_0_ - in - (~.malformed_hint <: bool) && (j <. current_true_hints_seen <: bool)) - (j, malformed_hint, out_hint <: (usize & bool & t_Slice (t_Array i32 (sz 256)))) - (fun temp_0_ -> - let j, malformed_hint, out_hint:(usize & bool & t_Slice (t_Array i32 (sz 256))) = - temp_0_ - in - let malformed_hint:bool = - if - j >. previous_true_hints_seen && - (hint_serialized.[ j ] <: u8) <=. - (hint_serialized.[ j -! sz 1 <: usize ] <: u8) - then - let malformed_hint:bool = true in - malformed_hint - else malformed_hint - in - if ~.malformed_hint - then - let out_hint:t_Slice (t_Array i32 (sz 256)) = - set_hint out_hint i (cast (hint_serialized.[ j ] <: u8) <: usize) - in - let j:usize = j +! sz 1 in - j, malformed_hint, out_hint <: (usize & bool & t_Slice (t_Array i32 (sz 256))) - else - j, malformed_hint, out_hint <: (usize & bool & t_Slice (t_Array i32 (sz 256)))) - in - if ~.malformed_hint - then - let previous_true_hints_seen:usize = current_true_hints_seen in - let i:usize = i +! sz 1 in - i, malformed_hint, out_hint, previous_true_hints_seen - <: - (usize & bool & t_Slice (t_Array i32 (sz 256)) & usize) - else - i, malformed_hint, out_hint, previous_true_hints_seen - <: - (usize & bool & t_Slice (t_Array i32 (sz 256)) & usize)) - in - let i:usize = previous_true_hints_seen in - let malformed_hint:bool = - Rust_primitives.Hax.Folds.fold_range_cf i - max_ones_in_hint - (fun malformed_hint temp_1_ -> - let malformed_hint:bool = malformed_hint in - let _:usize = temp_1_ in - true) - malformed_hint - (fun malformed_hint j -> - let malformed_hint:bool = malformed_hint in - let j:usize = j in - if (hint_serialized.[ j ] <: u8) <>. 0uy <: bool + if + current_true_hints_seen <. previous_true_hints_seen || + previous_true_hints_seen >. max_ones_in_hint then - let malformed_hint:bool = true in - Core.Ops.Control_flow.ControlFlow_Break ((), malformed_hint <: (Prims.unit & bool)) + Core.Ops.Control_flow.ControlFlow_Break + (Core.Ops.Control_flow.ControlFlow_Break + (out_commitment_hash, + out_signer_response, + out_hint, + (Core.Result.Result_Err + (Libcrux_ml_dsa.Types.VerificationError_MalformedHintError + <: + Libcrux_ml_dsa.Types.t_VerificationError) + <: + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + <: + (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError)) + <: + Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & (t_Slice (t_Array i32 (sz 256)) & usize))) <: - Core.Ops.Control_flow.t_ControlFlow (Prims.unit & bool) bool + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & (t_Slice (t_Array i32 (sz 256)) & usize))) + (t_Slice (t_Array i32 (sz 256)) & usize) else - Core.Ops.Control_flow.ControlFlow_Continue malformed_hint - <: - Core.Ops.Control_flow.t_ControlFlow (Prims.unit & bool) bool) - in - if malformed_hint - then - out_commitment_hash, - out_signer_response, - out_hint, - (Core.Result.Result_Err - (Libcrux_ml_dsa.Types.VerificationError_MalformedHintError - <: - Libcrux_ml_dsa.Types.t_VerificationError) - <: - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + match + Rust_primitives.Hax.Folds.fold_range_return previous_true_hints_seen + current_true_hints_seen + (fun out_hint temp_1_ -> + let out_hint:t_Slice (t_Array i32 (sz 256)) = out_hint in + let _:usize = temp_1_ in + true) + out_hint + (fun out_hint j -> + let out_hint:t_Slice (t_Array i32 (sz 256)) = out_hint in + let j:usize = j in + if + (j >. previous_true_hints_seen <: bool) && + ((hint_serialized.[ j ] <: u8) <=. + (hint_serialized.[ j -! sz 1 <: usize ] <: u8) + <: + bool) + then + Core.Ops.Control_flow.ControlFlow_Break + (Core.Ops.Control_flow.ControlFlow_Break + (out_commitment_hash, + out_signer_response, + out_hint, + (Core.Result.Result_Err + (Libcrux_ml_dsa.Types.VerificationError_MalformedHintError + <: + Libcrux_ml_dsa.Types.t_VerificationError) + <: + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + ) + <: + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + )) + <: + Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + ) (Prims.unit & t_Slice (t_Array i32 (sz 256)))) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit + Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & t_Slice (t_Array i32 (sz 256)))) + (t_Slice (t_Array i32 (sz 256))) + else + Core.Ops.Control_flow.ControlFlow_Continue + (set_hint out_hint i (cast (hint_serialized.[ j ] <: u8) <: usize) + <: + t_Slice (t_Array i32 (sz 256))) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit + Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & t_Slice (t_Array i32 (sz 256)))) + (t_Slice (t_Array i32 (sz 256)))) + <: + Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (t_Slice (t_Array i32 (sz 256))) + with + | Core.Ops.Control_flow.ControlFlow_Break ret -> + Core.Ops.Control_flow.ControlFlow_Break + (Core.Ops.Control_flow.ControlFlow_Break ret + <: + Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & (t_Slice (t_Array i32 (sz 256)) & usize))) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & (t_Slice (t_Array i32 (sz 256)) & usize))) + (t_Slice (t_Array i32 (sz 256)) & usize) + | Core.Ops.Control_flow.ControlFlow_Continue out_hint -> + let previous_true_hints_seen:usize = current_true_hints_seen in + Core.Ops.Control_flow.ControlFlow_Continue + (out_hint, previous_true_hints_seen <: (t_Slice (t_Array i32 (sz 256)) & usize)) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & (t_Slice (t_Array i32 (sz 256)) & usize))) + (t_Slice (t_Array i32 (sz 256)) & usize)) <: - (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & - t_Slice (t_Array i32 (sz 256)) & - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) - else - let hax_temp_output:Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError = - Core.Result.Result_Ok (() <: Prims.unit) + Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (t_Slice (t_Array i32 (sz 256)) & usize) + with + | Core.Ops.Control_flow.ControlFlow_Break ret -> ret + | Core.Ops.Control_flow.ControlFlow_Continue (out_hint, previous_true_hints_seen) -> + match + Rust_primitives.Hax.Folds.fold_range_return previous_true_hints_seen + max_ones_in_hint + (fun temp_0_ temp_1_ -> + let _:Prims.unit = temp_0_ in + let _:usize = temp_1_ in + true) + () + (fun temp_0_ j -> + let _:Prims.unit = temp_0_ in + let j:usize = j in + if (hint_serialized.[ j ] <: u8) <>. 0uy <: bool + then + Core.Ops.Control_flow.ControlFlow_Break + (Core.Ops.Control_flow.ControlFlow_Break + (out_commitment_hash, + out_signer_response, + out_hint, + (Core.Result.Result_Err + (Libcrux_ml_dsa.Types.VerificationError_MalformedHintError + <: + Libcrux_ml_dsa.Types.t_VerificationError) + <: + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + <: + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError)) + <: + Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & Prims.unit)) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & Prims.unit)) Prims.unit + else + Core.Ops.Control_flow.ControlFlow_Continue () + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & + t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + (Prims.unit & Prims.unit)) Prims.unit) <: - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError - in - out_commitment_hash, out_signer_response, out_hint, hax_temp_output - <: - (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & - t_Slice (t_Array i32 (sz 256)) & - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) + Core.Ops.Control_flow.t_ControlFlow + (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) Prims.unit + with + | Core.Ops.Control_flow.ControlFlow_Break ret -> ret + | Core.Ops.Control_flow.ControlFlow_Continue _ -> + let hax_temp_output:Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError = + Core.Result.Result_Ok (() <: Prims.unit) + <: + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + in + out_commitment_hash, out_signer_response, out_hint, hax_temp_output + <: + (t_Slice u8 & t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) & + t_Slice (t_Array i32 (sz 256)) & + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) let serialize (#v_SIMDUnit: Type0) diff --git a/libcrux-ml-dsa/src/encoding/signature.rs b/libcrux-ml-dsa/src/encoding/signature.rs index 1d66d8ee2..34c9351fd 100644 --- a/libcrux-ml-dsa/src/encoding/signature.rs +++ b/libcrux-ml-dsa/src/encoding/signature.rs @@ -66,7 +66,6 @@ pub(crate) fn deserialize( out_signer_response: &mut [PolynomialRingElement], out_hint: &mut [[i32; COEFFICIENTS_IN_RING_ELEMENT]], ) -> Result<(), VerificationError> { - // [eurydice] generates an unused variable pointing to out_hint here. debug_assert!(serialized.len() == signature_size); let (commitment_hash, rest_of_serialized) = serialized.split_at(commitment_hash_size); @@ -88,53 +87,36 @@ pub(crate) fn deserialize( // allow only one such encoding, to ensure strong unforgeability. let mut previous_true_hints_seen = 0usize; - let mut i = 0; - let mut malformed_hint = false; - - while !malformed_hint && i < rows_in_a { + for i in 0..rows_in_a { let current_true_hints_seen = hint_serialized[max_ones_in_hint + i] as usize; if (current_true_hints_seen < previous_true_hints_seen) || (previous_true_hints_seen > max_ones_in_hint) { // the true hints seen should be increasing - malformed_hint = true; + return Err(VerificationError::MalformedHintError); } - let mut j = previous_true_hints_seen; - while !malformed_hint && j < current_true_hints_seen { + for j in previous_true_hints_seen..current_true_hints_seen { if j > previous_true_hints_seen && hint_serialized[j] <= hint_serialized[j - 1] { // indices of true hints for a specific polynomial should be // increasing - malformed_hint = true; + return Err(VerificationError::MalformedHintError); } - if !malformed_hint { - set_hint(out_hint, i, hint_serialized[j] as usize); - j += 1; - } + set_hint(out_hint, i, hint_serialized[j] as usize); } - if !malformed_hint { - previous_true_hints_seen = current_true_hints_seen; - i += 1; - } + previous_true_hints_seen = current_true_hints_seen; } - i = previous_true_hints_seen; - - for j in i..max_ones_in_hint { + for j in previous_true_hints_seen..max_ones_in_hint { if hint_serialized[j] != 0 { // ensures padding indices are zero - malformed_hint = true; - break; + return Err(VerificationError::MalformedHintError); } } - if malformed_hint { - return Err(VerificationError::MalformedHintError); - } - Ok(()) }