Port: Hoist default C backend into separate functions

mldsa/mldsa_native.S

@@ -419,6 +419,7 @@
 #undef MLD_INLINE
 #undef MLD_MUST_CHECK_RETURN_VALUE
 #undef MLD_RESTRICT
+#undef MLD_STATIC_TESTABLE
 #undef MLD_SYS_AARCH64
 #undef MLD_SYS_AARCH64_EB
 #undef MLD_SYS_APPLE

mldsa/mldsa_native.c

@@ -416,6 +416,7 @@
 #undef MLD_INLINE
 #undef MLD_MUST_CHECK_RETURN_VALUE
 #undef MLD_RESTRICT
+#undef MLD_STATIC_TESTABLE
 #undef MLD_SYS_AARCH64
 #undef MLD_SYS_AARCH64_EB
 #undef MLD_SYS_APPLE

mldsa/src/poly.c

@@ -50,23 +50,17 @@ void mld_poly_reduce(mld_poly *a)
   mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX);
 }
 
-
-MLD_INTERNAL_API
-void mld_poly_caddq(mld_poly *a)
+MLD_STATIC_TESTABLE void mld_poly_caddq_c(mld_poly *a)
+__contract__(
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q))
+  assigns(memory_slice(a, sizeof(mld_poly)))
+  ensures(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
+)
 {
   unsigned int i;
   mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
-#if defined(MLD_USE_NATIVE_POLY_CADDQ)
-  {
-    int ret;
-    ret = mld_poly_caddq_native(a->coeffs);
-    if (ret == MLD_NATIVE_FUNC_SUCCESS)
-    {
-      mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
-      return;
-    }
-  }
-#endif /* MLD_USE_NATIVE_POLY_CADDQ */
+
   for (i = 0; i < MLDSA_N; ++i)
   __loop__(
     invariant(i <= MLDSA_N)
@@ -80,6 +74,22 @@ void mld_poly_caddq(mld_poly *a)
   mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
 }
 
+MLD_INTERNAL_API
+void mld_poly_caddq(mld_poly *a)
+{
+#if defined(MLD_USE_NATIVE_POLY_CADDQ)
+  int ret;
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
+  ret = mld_poly_caddq_native(a->coeffs);
+  if (ret == MLD_NATIVE_FUNC_SUCCESS)
+  {
+    mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
+    return;
+  }
+#endif /* MLD_USE_NATIVE_POLY_CADDQ */
+  mld_poly_caddq_c(a);
+}
+
 /* Reference: We use destructive version (output=first input) to avoid
  *            reasoning about aliasing in the CBMC specification */
 MLD_INTERNAL_API
@@ -142,63 +152,82 @@ void mld_poly_shiftl(mld_poly *a)
   mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
 }
 
+MLD_STATIC_TESTABLE void mld_poly_ntt_c(mld_poly *a)
+__contract__(
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q))
+  assigns(memory_slice(a, sizeof(mld_poly)))
+  ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND))
+)
+{
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
+  mld_ntt(a->coeffs);
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
+}
+
 MLD_INTERNAL_API
 void mld_poly_ntt(mld_poly *a)
 {
-  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
 #if defined(MLD_USE_NATIVE_NTT)
+  int ret;
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
+  ret = mld_ntt_native(a->coeffs);
+  if (ret == MLD_NATIVE_FUNC_SUCCESS)
   {
-    int ret;
-    ret = mld_ntt_native(a->coeffs);
-    if (ret == MLD_NATIVE_FUNC_SUCCESS)
-    {
-      mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
-      return;
-    }
+    mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
+    return;
   }
 #endif /* MLD_USE_NATIVE_NTT */
-  mld_ntt(a->coeffs);
-  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
+  mld_poly_ntt_c(a);
 }
 
+MLD_STATIC_TESTABLE void mld_poly_invntt_tomont_c(mld_poly *a)
+__contract__(
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_Q))
+  assigns(memory_slice(a, sizeof(mld_poly)))
+  ensures(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_INTT_BOUND))
+)
+{
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
+  mld_invntt_tomont(a->coeffs);
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND);
+}
+
+
 MLD_INTERNAL_API
 void mld_poly_invntt_tomont(mld_poly *a)
 {
-  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
 #if defined(MLD_USE_NATIVE_INTT)
+  int ret;
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLDSA_Q);
+  ret = mld_intt_native(a->coeffs);
+  if (ret == MLD_NATIVE_FUNC_SUCCESS)
   {
-    int ret;
-    ret = mld_intt_native(a->coeffs);
-    if (ret == MLD_NATIVE_FUNC_SUCCESS)
-    {
-      mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND);
-      return;
-    }
+    mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND);
+    return;
   }
 #endif /* MLD_USE_NATIVE_INTT */
-  mld_invntt_tomont(a->coeffs);
-  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_INTT_BOUND);
+  mld_poly_invntt_tomont_c(a);
 }
 
-MLD_INTERNAL_API
-void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a,
-                                   const mld_poly *b)
+MLD_STATIC_TESTABLE void mld_poly_pointwise_montgomery_c(mld_poly *c,
+                                                         const mld_poly *a,
+                                                         const mld_poly *b)
+__contract__(
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(memory_no_alias(b, sizeof(mld_poly)))
+  requires(memory_no_alias(c, sizeof(mld_poly)))
+  requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLD_NTT_BOUND))
+  requires(array_abs_bound(b->coeffs, 0, MLDSA_N, MLD_NTT_BOUND))
+  assigns(memory_slice(c, sizeof(mld_poly)))
+  ensures(array_abs_bound(c->coeffs, 0, MLDSA_N, MLDSA_Q))
+)
 {
   unsigned int i;
   mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
   mld_assert_abs_bound(b->coeffs, MLDSA_N, MLD_NTT_BOUND);
-#if defined(MLD_USE_NATIVE_POINTWISE_MONTGOMERY)
-  {
-    /* TODO: proof */
-    int ret;
-    ret = mld_poly_pointwise_montgomery_native(c->coeffs, a->coeffs, b->coeffs);
-    if (ret == MLD_NATIVE_FUNC_SUCCESS)
-    {
-      mld_assert_abs_bound(c->coeffs, MLDSA_N, MLDSA_Q);
-      return;
-    }
-  }
-#endif /* MLD_USE_NATIVE_POINTWISE_MONTGOMERY */
+
   for (i = 0; i < MLDSA_N; ++i)
   __loop__(
     invariant(i <= MLDSA_N)
@@ -207,10 +236,28 @@ void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a,
   {
     c->coeffs[i] = mld_montgomery_reduce((int64_t)a->coeffs[i] * b->coeffs[i]);
   }
-
   mld_assert_abs_bound(c->coeffs, MLDSA_N, MLDSA_Q);
 }
 
+MLD_INTERNAL_API
+void mld_poly_pointwise_montgomery(mld_poly *c, const mld_poly *a,
+                                   const mld_poly *b)
+{
+#if defined(MLD_USE_NATIVE_POINTWISE_MONTGOMERY)
+  /* TODO: proof */
+  int ret;
+  mld_assert_abs_bound(a->coeffs, MLDSA_N, MLD_NTT_BOUND);
+  mld_assert_abs_bound(b->coeffs, MLDSA_N, MLD_NTT_BOUND);
+  ret = mld_poly_pointwise_montgomery_native(c->coeffs, a->coeffs, b->coeffs);
+  if (ret == MLD_NATIVE_FUNC_SUCCESS)
+  {
+    mld_assert_abs_bound(c->coeffs, MLDSA_N, MLDSA_Q);
+    return;
+  }
+#endif /* MLD_USE_NATIVE_POINTWISE_MONTGOMERY */
+  mld_poly_pointwise_montgomery_c(c, a, b);
+}
+
 MLD_INTERNAL_API
 void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a)
 {
@@ -233,7 +280,57 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a)
   mld_assert_bound(a1->coeffs, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1);
 }
 
+#define POLY_UNIFORM_NBLOCKS \
+  ((768 + STREAM128_BLOCKBYTES - 1) / STREAM128_BLOCKBYTES)
+/* Reference: `mld_rej_uniform()` in the reference implementation @[REF].
+ *            - Our signature differs from the reference implementation
+ *              in that it adds the offset and always expects the base of the
+ *              target buffer. This avoids shifting the buffer base in the
+ *              caller, which appears tricky to reason about. */
+MLD_STATIC_TESTABLE unsigned int mld_rej_uniform_c(int32_t *a,
+                                                   unsigned int target,
+                                                   unsigned int offset,
+                                                   const uint8_t *buf,
+                                                   unsigned int buflen)
+__contract__(
+  requires(offset <= target && target <= MLDSA_N)
+  requires(buflen <= (POLY_UNIFORM_NBLOCKS * STREAM128_BLOCKBYTES) && buflen % 3 == 0)
+  requires(memory_no_alias(a, sizeof(int32_t) * target))
+  requires(memory_no_alias(buf, buflen))
+  requires(array_bound(a, 0, offset, 0, MLDSA_Q))
+  assigns(memory_slice(a, sizeof(int32_t) * target))
+  ensures(offset <= return_value && return_value <= target)
+  ensures(array_bound(a, 0, return_value, 0, MLDSA_Q))
+)
+{
+  unsigned int ctr, pos;
+  uint32_t t;
+  mld_assert_bound(a, offset, 0, MLDSA_Q);
+
+  ctr = offset;
+  pos = 0;
+  /* pos + 3 cannot overflow due to the assumption
+  buflen <= (POLY_UNIFORM_NBLOCKS * STREAM128_BLOCKBYTES) */
+  while (ctr < target && pos + 3 <= buflen)
+  __loop__(
+    invariant(offset <= ctr && ctr <= target && pos <= buflen)
+    invariant(array_bound(a, 0, ctr, 0, MLDSA_Q)))
+  {
+    t = buf[pos++];
+    t |= (uint32_t)buf[pos++] << 8;
+    t |= (uint32_t)buf[pos++] << 16;
+    t &= 0x7FFFFF;
+
+    if (t < MLDSA_Q)
+    {
+      a[ctr++] = (int32_t)t;
+    }
+  }
+
+  mld_assert_bound(a, ctr, 0, MLDSA_Q);
 
+  return ctr;
+}
 /*************************************************
  * Name:        mld_rej_uniform
  *
@@ -257,8 +354,6 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a)
  *              in that it adds the offset and always expects the base of the
  *              target buffer. This avoids shifting the buffer base in the
  *              caller, which appears tricky to reason about. */
-#define POLY_UNIFORM_NBLOCKS \
-  ((768 + STREAM128_BLOCKBYTES - 1) / STREAM128_BLOCKBYTES)
 static unsigned int mld_rej_uniform(int32_t *a, unsigned int target,
                                     unsigned int offset, const uint8_t *buf,
                                     unsigned int buflen)
@@ -273,15 +368,12 @@ __contract__(
   ensures(array_bound(a, 0, return_value, 0, MLDSA_Q))
 )
 {
-  unsigned int ctr, pos;
-  uint32_t t;
-  mld_assert_bound(a, offset, 0, MLDSA_Q);
-
 /* TODO: CBMC proof based on mld_rej_uniform_native */
 #if defined(MLD_USE_NATIVE_REJ_UNIFORM)
+  int ret;
+  mld_assert_bound(a, offset, 0, MLDSA_Q);
   if (offset == 0)
   {
-    int ret;
     ret = mld_rej_uniform_native(a, target, buf, buflen);
     if (ret != MLD_NATIVE_FUNC_FALLBACK)
     {
@@ -292,29 +384,7 @@ __contract__(
   }
 #endif /* MLD_USE_NATIVE_REJ_UNIFORM */
 
-  ctr = offset;
-  pos = 0;
-  /* pos + 3 cannot overflow due to the assumption
-  buflen <= (POLY_UNIFORM_NBLOCKS * STREAM128_BLOCKBYTES) */
-  while (ctr < target && pos + 3 <= buflen)
-  __loop__(
-    invariant(offset <= ctr && ctr <= target && pos <= buflen)
-    invariant(array_bound(a, 0, ctr, 0, MLDSA_Q)))
-  {
-    t = buf[pos++];
-    t |= (uint32_t)buf[pos++] << 8;
-    t |= (uint32_t)buf[pos++] << 16;
-    t &= 0x7FFFFF;
-
-    if (t < MLDSA_Q)
-    {
-      a[ctr++] = (int32_t)t;
-    }
-  }
-
-  mld_assert_bound(a, ctr, 0, MLDSA_Q);
-
-  return ctr;
+  return mld_rej_uniform_c(a, target, offset, buf, buflen);
 }
 
 /* Reference: poly_uniform() in the reference implementation @[REF].

mldsa/src/sys.h

@@ -135,6 +135,10 @@
 #endif /* inline */
 #endif /* !MLD_INLINE */
 
+#ifndef MLD_STATIC_TESTABLE
+#define MLD_STATIC_TESTABLE static
+#endif
+
 /*
  * C90 does not have the restrict compiler directive yet.
  * We don't use it in C90 builds.

proofs/cbmc/poly_caddq/Makefile

@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_caddq
-USE_FUNCTION_CONTRACTS=mld_caddq
+USE_FUNCTION_CONTRACTS=mld_poly_caddq_c
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1