From 8619341fcd17d5548ffae02ccc2681fed58063cb Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 15 Jan 2025 10:04:01 +0100 Subject: [PATCH] Remove double return workarounds. --- libcrux-ml-dsa/src/arithmetic.rs | 8 ------- libcrux-ml-dsa/src/encoding/commitment.rs | 4 ---- libcrux-ml-dsa/src/encoding/error.rs | 8 ------- libcrux-ml-dsa/src/encoding/signature.rs | 3 --- libcrux-ml-dsa/src/encoding/signing_key.rs | 3 --- libcrux-ml-dsa/src/encoding/t0.rs | 6 ----- libcrux-ml-dsa/src/encoding/t1.rs | 6 ----- .../src/encoding/verification_key.rs | 4 ---- libcrux-ml-dsa/src/matrix.rs | 12 ---------- libcrux-ml-dsa/src/ntt.rs | 2 -- libcrux-ml-dsa/src/polynomial.rs | 6 ----- libcrux-ml-dsa/src/sample.rs | 9 ------- libcrux-ml-dsa/src/samplex4.rs | 3 --- libcrux-ml-dsa/src/simd/avx2/invntt.rs | 6 ----- libcrux-ml-dsa/src/simd/avx2/ntt.rs | 3 --- .../src/simd/portable/arithmetic.rs | 24 ------------------- .../src/simd/portable/encoding/error.rs | 6 ----- .../src/simd/portable/encoding/gamma1.rs | 12 ---------- .../src/simd/portable/encoding/t1.rs | 6 ----- libcrux-ml-dsa/src/simd/portable/invntt.rs | 6 ----- libcrux-ml-dsa/src/simd/portable/ntt.rs | 1 - libcrux-ml-kem/src/ind_cpa.rs | 5 +--- libcrux-ml-kem/src/invert_ntt.rs | 12 ---------- libcrux-ml-kem/src/ntt.rs | 15 ------------ libcrux-ml-kem/src/polynomial.rs | 12 ---------- libcrux-ml-kem/src/serialize.rs | 6 ----- 26 files changed, 1 insertion(+), 187 deletions(-) diff --git a/libcrux-ml-dsa/src/arithmetic.rs b/libcrux-ml-dsa/src/arithmetic.rs index a86aa7752..f40580c3c 100644 --- a/libcrux-ml-dsa/src/arithmetic.rs +++ b/libcrux-ml-dsa/src/arithmetic.rs @@ -27,8 +27,6 @@ pub(crate) fn shift_left_then_reduce( for i in 0..re.simd_units.len() { SIMDUnit::shift_left_then_reduce::(&mut re.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -41,8 +39,6 @@ pub(crate) fn power2round_vector( SIMDUnit::power2round(&mut t[i].simd_units[j], &mut t1[i].simd_units[j]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -63,8 +59,6 @@ pub(crate) fn decompose_vector( ); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -110,6 +104,4 @@ pub(crate) fn use_hint( } re_vector[i] = tmp; } - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/encoding/commitment.rs b/libcrux-ml-dsa/src/encoding/commitment.rs index f123ab670..81e9d3471 100644 --- a/libcrux-ml-dsa/src/encoding/commitment.rs +++ b/libcrux-ml-dsa/src/encoding/commitment.rs @@ -12,8 +12,6 @@ fn serialize(re: &PolynomialRingElement, seriali ); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -30,8 +28,6 @@ pub(crate) fn serialize_vector( offset += ring_element_size; } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/error.rs b/libcrux-ml-dsa/src/encoding/error.rs index ad3aecbde..68e4f5a7c 100644 --- a/libcrux-ml-dsa/src/encoding/error.rs +++ b/libcrux-ml-dsa/src/encoding/error.rs @@ -21,9 +21,6 @@ pub(crate) fn serialize( ); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -49,9 +46,6 @@ fn deserialize( &mut result.simd_units[i], ); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -67,8 +61,6 @@ pub(crate) fn deserialize_to_vector_then_ntt( ntt(&mut ring_elements[i]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/signature.rs b/libcrux-ml-dsa/src/encoding/signature.rs index 34c9351fd..82b023802 100644 --- a/libcrux-ml-dsa/src/encoding/signature.rs +++ b/libcrux-ml-dsa/src/encoding/signature.rs @@ -47,9 +47,6 @@ pub(crate) fn serialize( } signature[offset + max_ones_in_hint + i] = true_hints_seen as u8; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] diff --git a/libcrux-ml-dsa/src/encoding/signing_key.rs b/libcrux-ml-dsa/src/encoding/signing_key.rs index aaee2d442..f61bbf8ab 100644 --- a/libcrux-ml-dsa/src/encoding/signing_key.rs +++ b/libcrux-ml-dsa/src/encoding/signing_key.rs @@ -56,7 +56,4 @@ pub(crate) fn generate_serialized( SIMDUnit::t0_serialize(simd_unit, &mut serialized[i * OUTPUT_BYTES_PER_SIMD_UNIT..(i + 1) * OUTPUT_BYTES_PER_SIMD_UNIT]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -34,8 +32,6 @@ fn deserialize( &mut result.simd_units[i], ); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -49,8 +45,6 @@ pub(crate) fn deserialize_to_vector_then_ntt( ntt(&mut ring_elements[i]); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/t1.rs b/libcrux-ml-dsa/src/encoding/t1.rs index 9de90bc62..815162b92 100644 --- a/libcrux-ml-dsa/src/encoding/t1.rs +++ b/libcrux-ml-dsa/src/encoding/t1.rs @@ -14,9 +14,6 @@ pub(crate) fn serialize( SIMDUnit::t1_serialize(simd_unit, &mut serialized[i * OUTPUT_BYTES_PER_SIMD_UNIT..(i + 1) * OUTPUT_BYTES_PER_SIMD_UNIT]); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } pub(crate) fn deserialize( @@ -30,9 +27,6 @@ pub(crate) fn deserialize( &mut result.simd_units[i], ); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/encoding/verification_key.rs b/libcrux-ml-dsa/src/encoding/verification_key.rs index 1dd8043f9..95b706153 100644 --- a/libcrux-ml-dsa/src/encoding/verification_key.rs +++ b/libcrux-ml-dsa/src/encoding/verification_key.rs @@ -23,8 +23,6 @@ pub(crate) fn generate_serialized( ); } } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -42,6 +40,4 @@ pub(crate) fn deserialize( &mut t1[i], ); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/matrix.rs b/libcrux-ml-dsa/src/matrix.rs index 9e0cb199f..c32d7e257 100644 --- a/libcrux-ml-dsa/src/matrix.rs +++ b/libcrux-ml-dsa/src/matrix.rs @@ -27,8 +27,6 @@ pub(crate) fn compute_as1_plus_s2( invert_ntt_montgomery::(&mut result[i]); PolynomialRingElement::add(&mut result[i], &s1_s2[columns_in_a + i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } /// Compute InvertNTT(Â ◦ ŷ) @@ -48,8 +46,6 @@ pub(crate) fn compute_matrix_x_mask( } invert_ntt_montgomery(&mut result[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -61,8 +57,6 @@ pub(crate) fn vector_times_ring_element( ntt_multiply_montgomery(&mut vector[i], ring_element); invert_ntt_montgomery(&mut vector[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -74,8 +68,6 @@ pub(crate) fn add_vectors( for i in 0..dimension { PolynomialRingElement::::add(&mut lhs[i], &rhs[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -87,8 +79,6 @@ pub(crate) fn subtract_vectors( for i in 0..dimension { PolynomialRingElement::::subtract(&mut lhs[i], &rhs[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } /// Compute InvertNTT(Â ◦ ẑ - ĉ ◦ NTT(t₁2ᵈ)) @@ -116,6 +106,4 @@ pub(crate) fn compute_w_approx( t1[i] = inner_result; invert_ntt_montgomery(&mut t1[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/ntt.rs b/libcrux-ml-dsa/src/ntt.rs index 711dc2668..2e96a67f9 100644 --- a/libcrux-ml-dsa/src/ntt.rs +++ b/libcrux-ml-dsa/src/ntt.rs @@ -20,8 +20,6 @@ pub(crate) fn ntt_multiply_montgomery( for i in 0..lhs.simd_units.len() { SIMDUnit::montgomery_multiply(&mut lhs.simd_units[i], &rhs.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/polynomial.rs b/libcrux-ml-dsa/src/polynomial.rs index 4cf104952..e212ca612 100644 --- a/libcrux-ml-dsa/src/polynomial.rs +++ b/libcrux-ml-dsa/src/polynomial.rs @@ -36,8 +36,6 @@ impl PolynomialRingElement { &mut result.simd_units[i], ); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] @@ -62,8 +60,6 @@ impl PolynomialRingElement { for i in 0..self.simd_units.len() { SIMDUnit::add(&mut self.simd_units[i], &rhs.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -71,7 +67,5 @@ impl PolynomialRingElement { for i in 0..self.simd_units.len() { SIMDUnit::subtract(&mut self.simd_units[i], &rhs.simd_units[i]); } - // [hax] https://github.com/hacspec/hax/issues/720 - () } } diff --git a/libcrux-ml-dsa/src/sample.rs b/libcrux-ml-dsa/src/sample.rs index d8883de12..8363d6313 100644 --- a/libcrux-ml-dsa/src/sample.rs +++ b/libcrux-ml-dsa/src/sample.rs @@ -164,9 +164,6 @@ pub(crate) fn sample_up_to_four_ring_elements_flat< &mut matrix[start_index + k], ); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -350,9 +347,6 @@ pub(crate) fn sample_four_error_ring_elements::from_i32_array(&out[i % 4], &mut re[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -436,9 +430,6 @@ pub(crate) fn sample_mask_vector< // TODO: For 87 we may want to do another 4 and discard 1. sample_mask_ring_element::(&seed, &mut mask[i], gamma1_exponent); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] diff --git a/libcrux-ml-dsa/src/samplex4.rs b/libcrux-ml-dsa/src/samplex4.rs index 827c8b993..504ff9bd1 100644 --- a/libcrux-ml-dsa/src/samplex4.rs +++ b/libcrux-ml-dsa/src/samplex4.rs @@ -50,9 +50,6 @@ pub(crate) fn matrix_flat( ); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } /// Portable sampling diff --git a/libcrux-ml-dsa/src/simd/avx2/invntt.rs b/libcrux-ml-dsa/src/simd/avx2/invntt.rs index f266992ac..0a6e05025 100644 --- a/libcrux-ml-dsa/src/simd/avx2/invntt.rs +++ b/libcrux-ml-dsa/src/simd/avx2/invntt.rs @@ -29,9 +29,6 @@ pub(crate) fn invert_ntt_montgomery(re: &mut AVX2RingElement) { value: arithmetic::montgomery_multiply_by_constant(re[i].value, FACTOR), }; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } unsafe { inv_inner(re) }; @@ -300,9 +297,6 @@ fn outer_3_plus( value: arithmetic::montgomery_multiply_by_constant(a_minus_b, ZETA), }; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg_attr(not(hax), target_feature(enable = "avx2"))] diff --git a/libcrux-ml-dsa/src/simd/avx2/ntt.rs b/libcrux-ml-dsa/src/simd/avx2/ntt.rs index 0f0306642..544a267bc 100644 --- a/libcrux-ml-dsa/src/simd/avx2/ntt.rs +++ b/libcrux-ml-dsa/src/simd/avx2/ntt.rs @@ -326,9 +326,6 @@ unsafe fn ntt_at_layer_5_to_3(re: &mut AVX2RingElement) { }; re[j + STEP_BY] = AVX2SIMDUnit { value: tmp }; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } // Layer 5 diff --git a/libcrux-ml-dsa/src/simd/portable/arithmetic.rs b/libcrux-ml-dsa/src/simd/portable/arithmetic.rs index 9e4df9a44..5671d8331 100644 --- a/libcrux-ml-dsa/src/simd/portable/arithmetic.rs +++ b/libcrux-ml-dsa/src/simd/portable/arithmetic.rs @@ -13,9 +13,6 @@ pub fn add(lhs: &mut Coefficients, rhs: &Coefficients) { for i in 0..lhs.values.len() { lhs.values[i] += rhs.values[i]; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -23,9 +20,6 @@ pub fn subtract(lhs: &mut Coefficients, rhs: &Coefficients) { for i in 0..lhs.values.len() { lhs.values[i] -= rhs.values[i]; } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -60,9 +54,6 @@ pub(crate) fn montgomery_multiply_by_constant(simd_unit: &mut Coefficients, c: i for i in 0..simd_unit.values.len() { simd_unit.values[i] = montgomery_reduce_element((simd_unit.values[i] as i64) * (c as i64)) } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -70,9 +61,6 @@ pub(crate) fn montgomery_multiply(lhs: &mut Coefficients, rhs: &Coefficients) { for i in 0..lhs.values.len() { lhs.values[i] = montgomery_reduce_element((lhs.values[i] as i64) * (rhs.values[i] as i64)) } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } // Splits t ∈ {0, ..., q-1} into t0 and t1 with a = t1*2ᴰ + t0 @@ -107,9 +95,6 @@ pub(super) fn power2round(t0: &mut Coefficients, t1: &mut Coefficients) { for i in 0..t0.values.len() { (t0.values[i], t1.values[i]) = power2round_element(t0.values[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } // TODO: Revisit this function when doing the range analysis and testing @@ -153,9 +138,6 @@ pub(super) fn shift_left_then_reduce(simd_unit: &mut Coeffi for i in 0..simd_unit.values.len() { simd_unit.values[i] = reduce_element(simd_unit.values[i] << SHIFT_BY); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -287,9 +269,6 @@ pub fn decompose( for i in 0..low.values.len() { (low.values[i], high.values[i]) = decompose_element(gamma2, simd_unit.values[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -297,9 +276,6 @@ pub fn use_hint(gamma2: Gamma2, simd_unit: &Coefficients, hint: &mut Coefficient for i in 0..hint.values.len() { hint.values[i] = use_one_hint(gamma2, simd_unit.values[i], hint.values[i]); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[cfg(test)] diff --git a/libcrux-ml-dsa/src/simd/portable/encoding/error.rs b/libcrux-ml-dsa/src/simd/portable/encoding/error.rs index da747fbbd..34096bb79 100644 --- a/libcrux-ml-dsa/src/simd/portable/encoding/error.rs +++ b/libcrux-ml-dsa/src/simd/portable/encoding/error.rs @@ -33,9 +33,6 @@ fn serialize_when_eta_is_4(simd_unit: &Coefficients, serialized: &mut [u8]) { serialized[i] = (coefficient1 << 4) | coefficient0; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -79,9 +76,6 @@ fn deserialize_when_eta_is_4(serialized: &[u8], simd_units: &mut Coefficients) { simd_units.values[2 * i + 1] = ETA - ((byte >> 4) as i32); } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] pub(crate) fn deserialize(eta: Eta, serialized: &[u8], out: &mut Coefficients) { diff --git a/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs b/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs index 520c8adfa..05239491a 100644 --- a/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs +++ b/libcrux-ml-dsa/src/simd/portable/encoding/gamma1.rs @@ -31,9 +31,6 @@ fn serialize_when_gamma1_is_2_pow_17(simd_unit: &Coefficients, serialized: &mut serialized[9 * i + 8] = (coefficient3 >> 10) as u8; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -55,9 +52,6 @@ fn serialize_when_gamma1_is_2_pow_19(simd_unit: &Coefficients, serialized: &mut serialized[5 * i + 4] = (coefficient1 >> 12) as u8; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -106,9 +100,6 @@ fn deserialize_when_gamma1_is_2_pow_17(serialized: &[u8], simd_unit: &mut Coeffi simd_unit.values[4 * i + 3] = GAMMA1 - coefficient3; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -135,9 +126,6 @@ fn deserialize_when_gamma1_is_2_pow_19(serialized: &[u8], simd_unit: &mut Coeffi simd_unit.values[2 * i + 1] = GAMMA1 - coefficient1; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] diff --git a/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs b/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs index f53788dd6..35e8c28cc 100644 --- a/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs +++ b/libcrux-ml-dsa/src/simd/portable/encoding/t1.rs @@ -18,9 +18,6 @@ pub fn serialize(simd_unit: &Coefficients, serialized: &mut [u8]) { serialized[5 * i + 4] = ((coefficients[3] >> 2) & 0xFF) as u8; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -43,7 +40,4 @@ pub fn deserialize(serialized: &[u8], simd_unit: &mut Coefficients) { simd_unit.values[4 * i + 3] = ((byte3 >> 6) | (byte4 << 2)) & mask; } } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/simd/portable/invntt.rs b/libcrux-ml-dsa/src/simd/portable/invntt.rs index 4ec015e60..95e1ac58b 100644 --- a/libcrux-ml-dsa/src/simd/portable/invntt.rs +++ b/libcrux-ml-dsa/src/simd/portable/invntt.rs @@ -212,9 +212,6 @@ fn outer_3_plus( re[j + STEP_BY] = a_minus_b; arithmetic::montgomery_multiply_by_constant(&mut re[j + STEP_BY], ZETA); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } #[inline(always)] @@ -301,7 +298,4 @@ pub(crate) fn invert_ntt_montgomery(re: &mut [Coefficients; SIMD_UNITS_IN_RING_E // - Convert the elements form montgomery domain to the standard domain. arithmetic::montgomery_multiply_by_constant(&mut re[i], 41_978); } - - // [hax] https://github.com/hacspec/hax/issues/720 - () } diff --git a/libcrux-ml-dsa/src/simd/portable/ntt.rs b/libcrux-ml-dsa/src/simd/portable/ntt.rs index 6e017f5a8..0b071815a 100644 --- a/libcrux-ml-dsa/src/simd/portable/ntt.rs +++ b/libcrux-ml-dsa/src/simd/portable/ntt.rs @@ -212,7 +212,6 @@ fn outer_3_plus( arithmetic::subtract(&mut re[j + STEP_BY], &tmp); arithmetic::add(&mut re[j], &tmp); } - () // Needed because of https://github.com/hacspec/hax/issues/720 } #[inline(always)] diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs index a552ba5dd..bb893aed7 100644 --- a/libcrux-ml-kem/src/ind_cpa.rs +++ b/libcrux-ml-kem/src/ind_cpa.rs @@ -649,8 +649,6 @@ fn compress_then_serialize_u< assert (v ($OUT_LEN /! $K) == v $OUT_LEN / v $K); assert (v $OUT_LEN / v $K == 32 * v $COMPRESSION_FACTOR)" ); - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 cloop! { for (i, re) in input.into_iter().enumerate() { hax_lib::loop_invariant!(|i: usize| { fstar!(r#"(v $i < v $K ==> Seq.length out == v $OUT_LEN /\ @@ -684,8 +682,7 @@ fn compress_then_serialize_u< "Lib.Sequence.eq_intro #u8 #(v $OUT_LEN) out (Spec.MLKEM.compress_then_encode_u #$K (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector $input))" - ); - () + ) } /// This function implements Algorithm 13 of the diff --git a/libcrux-ml-kem/src/invert_ntt.rs b/libcrux-ml-kem/src/invert_ntt.rs index 1d87eea97..ac197a13a 100644 --- a/libcrux-ml-kem/src/invert_ntt.rs +++ b/libcrux-ml-kem/src/invert_ntt.rs @@ -35,8 +35,6 @@ pub(crate) fn invert_ntt_at_layer_1( hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_1) (invert_ntt_re_range_1 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_2) (invert_ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -72,7 +70,6 @@ pub(crate) fn invert_ntt_at_layer_1( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -87,8 +84,6 @@ pub(crate) fn invert_ntt_at_layer_2( ) { hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_2) (invert_ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -119,7 +114,6 @@ pub(crate) fn invert_ntt_at_layer_2( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -134,8 +128,6 @@ pub(crate) fn invert_ntt_at_layer_3( ) { hax_lib::fstar!(r#"reveal_opaque (`%invert_ntt_re_range_2) (invert_ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -165,7 +157,6 @@ pub(crate) fn invert_ntt_at_layer_3( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -201,8 +192,6 @@ pub(crate) fn invert_ntt_at_layer_4_plus( ) { let step = 1 << layer; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..(128 >> layer) { *zeta_i -= 1; @@ -220,7 +209,6 @@ pub(crate) fn invert_ntt_at_layer_4_plus( re.coefficients[j + step_vec] = y; } } - () } #[inline(always)] diff --git a/libcrux-ml-kem/src/ntt.rs b/libcrux-ml-kem/src/ntt.rs index 5ea2923c3..2434eafea 100644 --- a/libcrux-ml-kem/src/ntt.rs +++ b/libcrux-ml-kem/src/ntt.rs @@ -36,8 +36,6 @@ pub(crate) fn ntt_at_layer_1( hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_2) (ntt_re_range_2 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_1) (ntt_re_range_1 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -73,7 +71,6 @@ pub(crate) fn ntt_at_layer_1( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -99,8 +96,6 @@ pub(crate) fn ntt_at_layer_2( hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_3) (ntt_re_range_3 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_2) (ntt_re_range_2 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -131,7 +126,6 @@ pub(crate) fn ntt_at_layer_2( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -157,8 +151,6 @@ pub(crate) fn ntt_at_layer_3( hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_4) (ntt_re_range_4 #$:Vector)"#); hax_lib::fstar!(r#"reveal_opaque (`%ntt_re_range_3) (ntt_re_range_3 #$:Vector)"#); let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..16 { hax_lib::loop_invariant!(|round: usize| { fstar!( @@ -187,7 +179,6 @@ pub(crate) fn ntt_at_layer_3( (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (re.f_coefficients.[ $round ])))" ); } - () } #[inline(always)] @@ -233,8 +224,6 @@ pub(crate) fn ntt_at_layer_4_plus( let step = 1 << layer; let _zeta_i_init = *zeta_i; - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for round in 0..(128 >> layer) { *zeta_i += 1; @@ -252,7 +241,6 @@ pub(crate) fn ntt_at_layer_4_plus( re.coefficients[j + step_vec] = y; } } - () } #[inline(always)] @@ -282,8 +270,6 @@ pub(crate) fn ntt_at_layer_4_plus( pub(crate) fn ntt_at_layer_7(re: &mut PolynomialRingElement) { let step = VECTORS_IN_RING_ELEMENT / 2; hax_lib::fstar!(r#"assert (v $step == 8)"#); - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..step { hax_lib::loop_invariant!(|j: usize| { fstar!( @@ -297,7 +283,6 @@ pub(crate) fn ntt_at_layer_7(re: &mut PolynomialRingElement< re.coefficients[j + step] = Vector::sub(re.coefficients[j], &t); re.coefficients[j] = Vector::add(re.coefficients[j], &t); } - () } #[inline(always)] diff --git a/libcrux-ml-kem/src/polynomial.rs b/libcrux-ml-kem/src/polynomial.rs index 5b161c355..0b97d24ac 100644 --- a/libcrux-ml-kem/src/polynomial.rs +++ b/libcrux-ml-kem/src/polynomial.rs @@ -92,24 +92,18 @@ fn add_to_ring_element( myself: &mut PolynomialRingElement, rhs: &PolynomialRingElement, ) { - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..myself.coefficients.len() { myself.coefficients[i] = Vector::add(myself.coefficients[i], &rhs.coefficients[i]); } - () } #[inline(always)] #[hax_lib::fstar::verification_status(lax)] fn poly_barrett_reduce(myself: &mut PolynomialRingElement) { // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..VECTORS_IN_RING_ELEMENT { myself.coefficients[i] = Vector::barrett_reduce(myself.coefficients[i]); } - () } #[inline(always)] @@ -172,8 +166,6 @@ fn add_error_reduce( error: &PolynomialRingElement, ) { // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..VECTORS_IN_RING_ELEMENT { let coefficient_normal_form = Vector::montgomery_multiply_by_constant(myself.coefficients[j], 1441); @@ -181,7 +173,6 @@ fn add_error_reduce( myself.coefficients[j] = Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j])); } - () } #[inline(always)] @@ -191,8 +182,6 @@ fn add_standard_error_reduce( error: &PolynomialRingElement, ) { // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..VECTORS_IN_RING_ELEMENT { // The coefficients are of the form aR^{-1} mod q, which means // calling to_montgomery_domain() on them should return a mod q. @@ -201,7 +190,6 @@ fn add_standard_error_reduce( myself.coefficients[j] = Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j])); } - () } /// Given two `KyberPolynomialRingElement`s in their NTT representations, diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs index c63bf39a4..6c496a785 100644 --- a/libcrux-ml-kem/src/serialize.rs +++ b/libcrux-ml-kem/src/serialize.rs @@ -297,8 +297,6 @@ fn compress_then_serialize_4( serialized: &mut [u8], ) { hax_lib::fstar!(r#"assert_norm (pow2 4 == 16)"#); - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..VECTORS_IN_RING_ELEMENT { // NOTE: Using `$serialized` in loop_invariant doesn't work here hax_lib::loop_invariant!(|i: usize| { @@ -317,7 +315,6 @@ fn compress_then_serialize_4( let bytes = Vector::serialize_4(coefficient); serialized[8 * i..8 * i + 8].copy_from_slice(&bytes); } - () } #[inline(always)] @@ -332,8 +329,6 @@ fn compress_then_serialize_5( re: PolynomialRingElement, serialized: &mut [u8], ) { - // The semicolon and parentheses at the end of loop are a workaround - // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..VECTORS_IN_RING_ELEMENT { let coefficients = Vector::compress::<5>(to_unsigned_representative::(re.coefficients[i])); @@ -341,7 +336,6 @@ fn compress_then_serialize_5( let bytes = Vector::serialize_5(coefficients); serialized[10 * i..10 * i + 10].copy_from_slice(&bytes); } - () } #[inline(always)]