Remove double return workarounds.

libcrux-ml-dsa/src/arithmetic.rs

@@ -27,8 +27,6 @@ pub(crate) fn shift_left_then_reduce<SIMDUnit: Operations, const SHIFT_BY: i32>(
     for i in 0..re.simd_units.len() {
         SIMDUnit::shift_left_then_reduce::<SHIFT_BY>(&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: Operations>(
             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<SIMDUnit: Operations>(
             );
         }
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[inline(always)]
@@ -110,6 +104,4 @@ pub(crate) fn use_hint<SIMDUnit: Operations>(
         }
         re_vector[i] = tmp;
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }

libcrux-ml-dsa/src/encoding/commitment.rs

@@ -12,8 +12,6 @@ fn serialize<SIMDUnit: Operations>(re: &PolynomialRingElement<SIMDUnit>, seriali
             );
         }
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[inline(always)]
@@ -30,8 +28,6 @@ pub(crate) fn serialize_vector<SIMDUnit: Operations>(
             offset += ring_element_size;
         }
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[cfg(test)]

libcrux-ml-dsa/src/encoding/error.rs

@@ -21,9 +21,6 @@ pub(crate) fn serialize<SIMDUnit: Operations>(
                 );
         }
     }
-
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[inline(always)]
@@ -49,9 +46,6 @@ fn deserialize<SIMDUnit: Operations>(
             &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<SIMDUnit: Operations>(
             ntt(&mut ring_elements[i]);
         }
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[cfg(test)]

libcrux-ml-dsa/src/encoding/signature.rs

@@ -47,9 +47,6 @@ pub(crate) fn serialize<SIMDUnit: Operations>(
         }
         signature[offset + max_ones_in_hint + i] = true_hints_seen as u8;
     }
-
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[inline(always)]

libcrux-ml-dsa/src/encoding/signing_key.rs

@@ -56,7 +56,4 @@ pub(crate) fn generate_serialized<SIMDUnit: Operations, Shake256: shake256::DsaX
             offset += RING_ELEMENT_OF_T0S_SIZE;
         }
     }
-
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }

libcrux-ml-dsa/src/encoding/t0.rs

@@ -19,8 +19,6 @@ pub(crate) fn serialize<SIMDUnit: Operations>(
             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<SIMDUnit: Operations>(
             &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<SIMDUnit: Operations>(
             ntt(&mut ring_elements[i]);
         }
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[cfg(test)]

libcrux-ml-dsa/src/encoding/t1.rs

@@ -14,9 +14,6 @@ pub(crate) fn serialize<SIMDUnit: Operations>(
             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<SIMDUnit: Operations>(
@@ -30,9 +27,6 @@ pub(crate) fn deserialize<SIMDUnit: Operations>(
             &mut result.simd_units[i],
         );
     }
-
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[cfg(test)]

libcrux-ml-dsa/src/encoding/verification_key.rs

@@ -23,8 +23,6 @@ pub(crate) fn generate_serialized<SIMDUnit: Operations>(
             );
         }
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[inline(always)]
@@ -42,6 +40,4 @@ pub(crate) fn deserialize<SIMDUnit: Operations>(
             &mut t1[i],
         );
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }

libcrux-ml-dsa/src/matrix.rs

@@ -27,8 +27,6 @@ pub(crate) fn compute_as1_plus_s2<SIMDUnit: Operations>(
         invert_ntt_montgomery::<SIMDUnit>(&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<SIMDUnit: Operations>(
         }
         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<SIMDUnit: Operations>(
         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<SIMDUnit: Operations>(
     for i in 0..dimension {
         PolynomialRingElement::<SIMDUnit>::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<SIMDUnit: Operations>(
     for i in 0..dimension {
         PolynomialRingElement::<SIMDUnit>::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<SIMDUnit: Operations>(
         t1[i] = inner_result;
         invert_ntt_montgomery(&mut t1[i]);
     }
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }

libcrux-ml-dsa/src/ntt.rs

@@ -20,8 +20,6 @@ pub(crate) fn ntt_multiply_montgomery<SIMDUnit: Operations>(
     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)]

libcrux-ml-dsa/src/polynomial.rs

@@ -36,8 +36,6 @@ impl<SIMDUnit: Operations> PolynomialRingElement<SIMDUnit> {
                 &mut result.simd_units[i],
             );
         }
-        // [hax] https://github.com/hacspec/hax/issues/720
-        ()
     }
 
     #[cfg(test)]
@@ -62,16 +60,12 @@ impl<SIMDUnit: Operations> PolynomialRingElement<SIMDUnit> {
         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)]
     pub(crate) fn subtract(&mut self, rhs: &Self) {
         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
-        ()
     }
 }

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<SIMDUnit: Operations, Shake256: sh
     for i in start_index as usize..max {
         PolynomialRingElement::<SIMDUnit>::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::<SIMDUnit, Shake256>(&seed, &mut mask[i], gamma1_exponent);
     }
-
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 #[inline(always)]

libcrux-ml-dsa/src/samplex4.rs

@@ -50,9 +50,6 @@ pub(crate) fn matrix_flat<SIMDUnit: Operations, Shake128: shake128::XofX4>(
             );
         }
     }
-
-    // [hax] https://github.com/hacspec/hax/issues/720
-    ()
 }
 
 /// Portable sampling

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<const OFFSET: usize, const STEP_BY: usize, const ZETA: i32>(
             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"))]

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

libcrux-ml-dsa/src/simd/portable/arithmetic.rs

@@ -13,19 +13,13 @@ 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)]
 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,19 +54,13 @@ 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)]
 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<const SHIFT_BY: i32>(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,19 +269,13 @@ 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)]
 pub fn use_hint(gamma2: Gamma2, simd_unit: &Coefficients, hint: &mut Coefficients) {
     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)]