Move poly_chknorm from poly_kl.c to poly.c

mldsa/mldsa_native.c

@@ -228,7 +228,6 @@
 #undef MLD_POLYETA_UNPACK_LOWER_BOUND
 #undef MLD_POLY_KL_H
 #undef mld_poly_challenge
-#undef mld_poly_chknorm
 #undef mld_poly_decompose
 #undef mld_poly_make_hint
 #undef mld_poly_uniform_eta_4x
@@ -327,6 +326,7 @@
 #undef MLD_POLY_H
 #undef mld_poly_add
 #undef mld_poly_caddq
+#undef mld_poly_chknorm
 #undef mld_poly_invntt_tomont
 #undef mld_poly_ntt
 #undef mld_poly_pointwise_montgomery

mldsa/src/poly.c

@@ -571,6 +571,59 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t *a)
                    (1 << (MLDSA_D - 1)) + 1);
 }
 
+/* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8).
+ * This is unnecessary as it's always a compile-time constant.
+ * We instead model it as a precondition.
+ * Checking the bound is performed using a conditional arguing
+ * 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)
+{
+#if defined(MLD_USE_NATIVE_POLY_CHKNORM)
+  /* TODO: proof */
+  mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX);
+  return mld_poly_chknorm_native(a->coeffs, B);
+#else
+  unsigned int i;
+  uint32_t t = 0;
+  mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX);
+
+
+  for (i = 0; i < MLDSA_N; ++i)
+  __loop__(
+    invariant(i <= MLDSA_N)
+    invariant(t == 0 || t == 0xFFFFFFFF)
+    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.
+     */
+
+    /* if (abs(a[i]) >= B) */
+    t |= mld_ct_cmask_neg_i32(B - 1 - mld_ct_abs_i32(a->coeffs[i]));
+  }
+
+  return t;
+#endif /* !MLD_USE_NATIVE_POLY_CHKNORM */
+}
 
 #else  /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
 MLD_EMPTY_CU(mld_poly)

mldsa/src/poly.h

@@ -351,4 +351,36 @@ __contract__(
   ensures(array_bound(r->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))
 );
 
+#define mld_poly_chknorm MLD_NAMESPACE(poly_chknorm)
+/*************************************************
+ * Name:        mld_poly_chknorm
+ *
+ * Description: Check infinity norm of polynomial against given bound.
+ *              Assumes input coefficients were reduced by mld_reduce32().
+ *
+ * Arguments:   - const mld_poly *a: pointer to polynomial
+ *              - int32_t B: norm bound
+ *
+ * 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 - 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))
+);
+
 #endif /* !MLD_POLY_H */

mldsa/src/poly_kl.c

@@ -129,61 +129,6 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
   mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
 }
 
-/* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8).
- * This is unnecessary as it's always a compile-time constant.
- * We instead model it as a precondition.
- * Checking the bound is performed using a conditional arguing
- * 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)
-{
-#if defined(MLD_USE_NATIVE_POLY_CHKNORM)
-  /* TODO: proof */
-  mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX);
-  return mld_poly_chknorm_native(a->coeffs, B);
-#else
-  unsigned int i;
-  uint32_t t = 0;
-  mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX);
-
-
-  for (i = 0; i < MLDSA_N; ++i)
-  __loop__(
-    invariant(i <= MLDSA_N)
-    invariant(t == 0 || t == 0xFFFFFFFF)
-    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.
-     */
-
-    /* if (abs(a[i]) >= B) */
-    t |= mld_ct_cmask_neg_i32(B - 1 - mld_ct_abs_i32(a->coeffs[i]));
-  }
-
-  return t;
-#endif /* !MLD_USE_NATIVE_POLY_CHKNORM */
-}
-
-
 /*************************************************
  * Name:        mld_rej_eta
  *

mldsa/src/poly_kl.h

@@ -89,38 +89,6 @@ __contract__(
   ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
 );
 
-#define mld_poly_chknorm MLD_NAMESPACE_KL(poly_chknorm)
-/*************************************************
- * Name:        mld_poly_chknorm
- *
- * Description: Check infinity norm of polynomial against given bound.
- *              Assumes input coefficients were reduced by mld_reduce32().
- *
- * Arguments:   - const mld_poly *a: pointer to polynomial
- *              - int32_t B: norm bound
- *
- * 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 - 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))
-);
-
 #define mld_poly_uniform_eta_4x MLD_NAMESPACE_KL(poly_uniform_eta_4x)
 /*************************************************
  * Name:        mld_poly_uniform_eta

proofs/cbmc/poly_chknorm/Makefile

@@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm
 USE_FUNCTION_CONTRACTS=mld_ct_abs_i32 mld_ct_cmask_neg_i32