Merge pull request #410 from pq-code-package/inline2

Inline rounding.c and reduce.c

Author: mkannwischer

mldsa/reduce.c

@@ -8,6 +8,7 @@
 #include <stdint.h>
 #include "cbmc.h"
 #include "common.h"
+#include "ct.h"
 
 #define MONT -4186625 /* 2^32 % MLDSA_Q */
 
@@ -24,7 +25,35 @@
 #define MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX ((int64_t)INT32_MIN * -MLDSA_Q)
 
 
-#define mld_montgomery_reduce MLD_NAMESPACE(montgomery_reduce)
+
+/*************************************************
+ * Name:        mld_cast_uint32_to_int32
+ *
+ * Description: Cast uint32 value to int32
+ *
+ * Returns:
+ *   input x in     0 .. 2^31-1: returns value unchanged
+ *   input x in  2^31 .. 2^32-1: returns (x - 2^32)
+ **************************************************/
+#ifdef CBMC
+#pragma CPROVER check push
+#pragma CPROVER check disable "conversion"
+#endif
+static MLD_INLINE int32_t mld_cast_uint32_to_int32(uint32_t x)
+{
+  /*
+   * PORTABILITY: This relies on uint32_t -> int32_t
+   * being implemented as the inverse of int32_t -> uint32_t,
+   * which is implementation-defined (C99 6.3.1.3 (3))
+   * CBMC (correctly) fails to prove this conversion is OK,
+   * so we have to suppress that check here
+   */
+  return (int32_t)x;
+}
+#ifdef CBMC
+#pragma CPROVER check pop
+#endif
+
 /*************************************************
  * Name:        mld_montgomery_reduce
  *
@@ -46,17 +75,39 @@
  *
  * Returns r.
  **************************************************/
-int32_t mld_montgomery_reduce(int64_t a)
+static MLD_INLINE int32_t mld_montgomery_reduce(int64_t a)
 __contract__(
   requires(a >= -MONTGOMERY_REDUCE_DOMAIN_MAX && a <= MONTGOMERY_REDUCE_DOMAIN_MAX)
   ensures(return_value >= INT32_MIN && return_value < REDUCE32_DOMAIN_MAX)
 
   /* Special case - for stronger input bounds, we can ensure stronger bounds on the output */
   ensures((a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX) ==>
           (return_value > -MLDSA_Q && return_value < MLDSA_Q))
-);
+)
+{
+  /* check-magic: 58728449 == unsigned_mod(pow(MLDSA_Q, -1, 2^32), 2^32) */
+  const uint64_t QINV = 58728449;
+
+  /*  Compute a*q^{-1} mod 2^32 in unsigned representatives */
+  const uint32_t a_reduced = a & UINT32_MAX;
+  const uint32_t a_inverted = (a_reduced * QINV) & UINT32_MAX;
+
+  /* Lift to signed canonical representative mod 2^32. */
+  const int32_t t = mld_cast_uint32_to_int32(a_inverted);
+
+  int64_t r;
+
+  r = a - ((int64_t)t * MLDSA_Q);
+
+  /*
+   * PORTABILITY: Right-shift on a signed integer is, strictly-speaking,
+   * implementation-defined for negative left argument. Here,
+   * we assume it's sign-preserving "arithmetic" shift right. (C99 6.5.7 (5))
+   */
+  r = r >> 32;
+  return (int32_t)r;
+}
 
-#define mld_reduce32 MLD_NAMESPACE(reduce32)
 /*************************************************
  * Name:        mld_reduce32
  *
@@ -68,14 +119,21 @@ __contract__(
  *
  * Returns r.
  **************************************************/
-int32_t mld_reduce32(int32_t a)
+static MLD_INLINE int32_t mld_reduce32(int32_t a)
 __contract__(
   requires(a <= REDUCE32_DOMAIN_MAX)
   ensures(return_value >= -REDUCE32_RANGE_MAX)
   ensures(return_value <   REDUCE32_RANGE_MAX)
-);
+)
+{
+  int32_t t;
+
+  t = (a + (1 << 22)) >> 23;
+  t = a - t * MLDSA_Q;
+  cassert((t - a) % MLDSA_Q == 0);
+  return t;
+}
 
-#define mld_caddq MLD_NAMESPACE(caddq)
 /*************************************************
  * Name:        mld_caddq
  *
@@ -85,14 +143,17 @@ __contract__(
  *
  * Returns r.
  **************************************************/
-int32_t mld_caddq(int32_t a)
+static MLD_INLINE int32_t mld_caddq(int32_t a)
 __contract__(
   requires(a > -MLDSA_Q)
   requires(a < MLDSA_Q)
   ensures(return_value >= 0)
   ensures(return_value < MLDSA_Q)
   ensures(return_value == (a >= 0) ? a : (a + MLDSA_Q))
-);
+)
+{
+  return mld_ct_sel_int32(a + MLDSA_Q, a, mld_ct_cmask_neg_i32(a));
+}
 
 
 #endif /* !MLD_REDUCE_H */