Add clarrifying comment to poly_chknorm

It is a little unintuitive why in poly_chknorm it suffices to check that
the coefficients of absolute value less than B even though the inputs are NOT
canonically reduced.

The answer is:
* Specification: The definition of the infinity norm in FIPS-204 requires
*                signed canonical reduction prior to applying the bounds check.
*                However, `-B < (a mod± MLDSA_Q) < B` is equivalent to
*                `-B < a < B` under the assumption that
*                `B <= MLDSA_Q - REDUCE32_RANGE_MAX` (cf. the assertion in
*                the code). Hence, the present spec and implementation are
*                correct without reduction.

Before we were using B <= (MLDSA_Q - 1) / 8) (as it is checked in the
reference implementation), but the more natural bound is the slightly
larger MLDSA_Q - REDUCE32_RANGE_MAX.

This commits changes the pre-condition, adds a comment to poly_chknorm, and
also adds an assertion for what I said above. CBMC proves this just fine.

Resolves #504

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

mldsa/native/api.h

@@ -264,8 +264,8 @@ static MLD_INLINE void mld_poly_use_hint_88_native(int32_t *b, const int32_t *a,
  * Arguments:   - const int32_t *a: pointer to polynomial
  *              - int32_t B: norm bound
  *
- * Returns 0 if norm is strictly smaller than B <= (MLDSA_Q-1)/8 and 0xFFFFFFFF
- * otherwise.
+ * Returns 0 if the infinity norm is strictly smaller than B, and 0xFFFFFFFF
+ * otherwise. B must not be larger than MLDSA_Q - REDUCE32_RANGE_MAX.
  **************************************************/
 static MLD_INLINE uint32_t mld_poly_chknorm_native(const int32_t *a, int32_t B);
 #endif /* MLD_USE_NATIVE_POLY_CHKNORM */

mldsa/poly.c

@@ -320,6 +320,8 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
  * that it is okay to leak which coefficient violates the bound (while the
  * coefficient itself must remain secret).
  * We instead perform everything in constant-time.
+ * Also it is sufficient to check that it is smaller than
+ * MLDSA_Q - REDUCE32_RANGE_MAX > (MLDSA_Q - 1) / 8).
  */
 MLD_INTERNAL_API
 uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
@@ -341,6 +343,17 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
     invariant((t == 0) == array_abs_bound(a->coeffs, 0, i, B))
   )
   {
+    /*
+     * Since we know that -REDUCE32_RANGE_MAX <= a < REDUCE32_RANGE_MAX,
+     * and B <= MLDSA_Q - REDUCE32_RANGE_MAX, to check if
+     * -B < (a mod± MLDSA_Q) < B, it suffices to check if -B < a < B.
+     *
+     * We prove this to be true using the following CBMC assertions.
+     * a ==> b expressed as !a || b to also allow run-time assertion.
+     */
+    mld_assert(a->coeffs[i] < B || a->coeffs[i] - MLDSA_Q <= -B);
+    mld_assert(a->coeffs[i] > -B || a->coeffs[i] + MLDSA_Q >= B);
+
     /* Reference: Leaks which coefficient violates the bound via a conditional.
      * We are more conservative to reduce the number of declassifications in
      * constant-time testing.

mldsa/poly.h

@@ -307,14 +307,23 @@ __contract__(
  * Arguments:   - const mld_poly *a: pointer to polynomial
  *              - int32_t B: norm bound
  *
- * Returns 0 if norm is strictly smaller than B <= (MLDSA_Q-1)/8 and 0xFFFFFFFF
- * otherwise.
+ * Returns 0 if norm is strictly smaller than
+ * B <= (MLDSA_Q - REDUCE32_RANGE_MAX) and 0xFFFFFFFF otherwise.
+ *
+ * Specification: The definition of this FIPS-204 requires signed canonical
+ *                reduction prior to applying the bounds check.
+ *                However, `-B < (a mod± MLDSA_Q) < B` is equivalent to
+ *                `-B < a < B` under the assumption that
+ *                `B <= MLDSA_Q - REDUCE32_RANGE_MAX` (cf. the assertion in
+ *                the code). Hence, the present spec and implementation are
+ *                correct without reduction.
+ *
  **************************************************/
 MLD_INTERNAL_API
 uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
 __contract__(
   requires(memory_no_alias(a, sizeof(mld_poly)))
-  requires(0 <= B && B <= (MLDSA_Q - 1) / 8)
+  requires(0 <= B && B <= MLDSA_Q - REDUCE32_RANGE_MAX)
   requires(array_bound(a->coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))
   ensures(return_value == 0 || return_value == 0xFFFFFFFF)
   ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B))