@@ -320,10 +320,17 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
320320 * that it is okay to leak which coefficient violates the bound (while the
321321 * coefficient itself must remain secret).
322322 * We instead perform everything in constant-time.
323+ * Also it is sufficient to check that it is smaller than
324+ * MLDSA_Q - REDUCE32_RANGE_MAX > (MLDSA_Q - 1) / 8).
323325 */
324326MLD_INTERNAL_API
325327uint32_t mld_poly_chknorm (const mld_poly * a , int32_t B )
326328{
329+ #if defined(MLD_USE_NATIVE_POLY_CHKNORM )
330+ /* TODO: proof */
331+ mld_assert_bound (a -> coeffs , MLDSA_N , - REDUCE32_RANGE_MAX , REDUCE32_RANGE_MAX );
332+ return mld_poly_chknorm_native (a -> coeffs , B );
333+ #else
327334 unsigned int i ;
328335 uint32_t t = 0 ;
329336 mld_assert_bound (a -> coeffs , MLDSA_N , - REDUCE32_RANGE_MAX , REDUCE32_RANGE_MAX );
@@ -336,6 +343,17 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
336343 invariant ((t == 0 ) == array_abs_bound (a -> coeffs , 0 , i , B ))
337344 )
338345 {
346+ /*
347+ * Since we know that -REDUCE32_RANGE_MAX <= a < REDUCE32_RANGE_MAX,
348+ * and B <= MLDSA_Q - REDUCE32_RANGE_MAX, to check if
349+ * -B < (a mod± MLDSA_Q) < B, it suffices to check if -B < a < B.
350+ *
351+ * We prove this to be true using the following CBMC assertions.
352+ * a ==> b expressed as !a || b to also allow run-time assertion.
353+ */
354+ mld_assert (a -> coeffs [i ] < B || a -> coeffs [i ] - MLDSA_Q <= - B );
355+ mld_assert (a -> coeffs [i ] > - B || a -> coeffs [i ] + MLDSA_Q >= B );
356+
339357 /* Reference: Leaks which coefficient violates the bound via a conditional.
340358 * We are more conservative to reduce the number of declassifications in
341359 * constant-time testing.
@@ -346,6 +364,7 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
346364 }
347365
348366 return t ;
367+ #endif /* !MLD_USE_NATIVE_POLY_CHKNORM */
349368}
350369
351370/*************************************************
0 commit comments