Strengthen specification for montgomery_reduce()

There are two uses of the generic Montgomery reduction
`montgomery_reduce()` in the code base:
- For modular multiplication with twiddles in `fqmul()`
- For Montgomery reduction after accumulation in the base
  multiplication.

Those two uses require different specifications for
`montgomery_reduce()`. However, there does not appear
to be a mechanism in CBMC to register more than one contract.

To remedy, this commit moves the previous `montgomery_reduce()`
into a static inline `montgomery_reduce_generic()`, and uses it
in the definitions of `montgomery_reduce()` and `fqmul()`. The
new `montgomery_reduce()` then makes bounds assumptions according
to the use in base multiplication, while the call to
`montgomery_reduce_generic()` provides stronger input bounds.
Accordingly, the post-condition of `montgomery_reduce()` only
guarantees coefficients < 3/2q, while `fqmul()` ensures < q.

The CBMC contracts an proofs for `montgomery_reduce()` and
`fqmul()` are adjusted accordingly.

Signed-off-by: Hanno Becker <[email protected]>

cbmc/proofs/fqmul/Makefile

@@ -18,8 +18,8 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/reduce.c
 
-CHECK_FUNCTION_CONTRACTS=fqmul
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)montgomery_reduce
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
+USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

mlkem/common.h

@@ -4,5 +4,6 @@
 
 #define DEFAULT_ALIGN 32
 #define ALIGN __attribute__((aligned(DEFAULT_ALIGN)))
+#define ALWAYS_INLINE __attribute__((always_inline))
 
 #endif

mlkem/reduce.c

@@ -33,9 +33,9 @@ static inline int16_t cast_uint16_to_int16(uint16_t x) {
 #endif
 
 /*************************************************
- * Name:        montgomery_reduce
+ * Name:        montgomery_reduce_generic
  *
- * Description: Montgomery reduction; given a 32-bit integer a, computes
+ * Description: Generic Montgomery reduction; given a 32-bit integer a, computes
  *              16-bit integer congruent to a * R^-1 mod q, where R=2^16
  *
  * Arguments:   - int32_t a: input integer to be reduced
@@ -56,7 +56,8 @@ static inline int16_t cast_uint16_to_int16(uint16_t x) {
  *                < C with a value of abs < q has absolute value
  *                < q (C/2^16 + 1/2).
  **************************************************/
-int16_t montgomery_reduce(int32_t a) {
+ALWAYS_INLINE
+static inline int16_t montgomery_reduce_generic(int32_t a) {
   // Bounds on paper
   //
   // - Case |a| < q * C, for some C
@@ -87,6 +88,24 @@ int16_t montgomery_reduce(int32_t a) {
   return (int16_t)r;
 }
 
+int16_t montgomery_reduce(int32_t a) {
+  SCALAR_BOUND(a, 2 * MLKEM_Q * 32768, "montgomery_reduce input");
+
+  int16_t res = montgomery_reduce_generic(a);
+
+  SCALAR_BOUND(res, (3 * (MLKEM_Q + 1)) / 2, "montgomery_reduce output");
+  return res;
+}
+
+int16_t fqmul(int16_t a, int16_t b) {
+  SCALAR_BOUND(b, HALF_Q + 1, "fqmul input");
+
+  int16_t res = montgomery_reduce((int32_t)a * (int32_t)b);
+
+  SCALAR_BOUND(res, MLKEM_Q, "fqmul output");
+  return res;
+}
+
 // To divide by MLKEM_Q using Barrett multiplication, the "magic number"
 // multiplier is round_to_nearest(2**26/MLKEM_Q)
 #define BPOWER 26

mlkem/reduce.h

@@ -8,26 +8,37 @@
 #include "params.h"
 
 #define MONT -1044                  // 2^16 mod q
-#define HALF_Q ((MLKEM_Q - 1) / 2)  // 1664
+#define HALF_Q ((MLKEM_Q + 1) / 2)  // 1665
 
+/*************************************************
+ * Name:        montgomery_reduce
+ *
+ * Description: Montgomery reduction
+ *
+ * Arguments:   - int32_t a: input integer to be reduced
+ *                  Must be smaller than 2 * q * 2^15 in absolute value.
+ *
+ * Returns:     integer congruent to a * R^-1 modulo q,
+ *              smaller than 3/2 q in absolute value.
+ **************************************************/
 #define montgomery_reduce MLKEM_NAMESPACE(montgomery_reduce)
 int16_t montgomery_reduce(int32_t a)
     // clang-format off
-REQUIRES(a >= INT32_MIN + (32768 * MLKEM_Q))
-REQUIRES(a <= INT32_MAX - (32768 * MLKEM_Q))
-ENSURES(RETURN_VALUE >= INT16_MIN && RETURN_VALUE <= INT16_MAX);
+REQUIRES(a > -(2 * MLKEM_Q * 32768))
+REQUIRES(a <  (2 * MLKEM_Q * 32768))
+ENSURES(RETURN_VALUE > -(3 * HALF_Q) && RETURN_VALUE < (3 * HALF_Q));
 // clang-format on
 
 #define barrett_reduce MLKEM_NAMESPACE(barrett_reduce)
 int16_t barrett_reduce(int16_t a)
     // clang-format off
-ENSURES(RETURN_VALUE >= -HALF_Q && RETURN_VALUE <= HALF_Q);
+ENSURES(RETURN_VALUE > -HALF_Q && RETURN_VALUE < HALF_Q);
 // clang-format on
 
 /*************************************************
  * Name:        fqmul
  *
- * Description: Multiplication followed by Montgomery reduction
+ * Description: Montgomery multiplication modulo q=3329
  *
  * Arguments:   - int16_t a: first factor
  *                  Can be any int16_t.
@@ -38,13 +49,13 @@ ENSURES(RETURN_VALUE >= -HALF_Q && RETURN_VALUE <= HALF_Q);
  * smaller than q in absolute value.
  *
  **************************************************/
-static inline int16_t fqmul(int16_t a, int16_t b) {
-  SCALAR_BOUND(b, HALF_Q + 1, "fqmul input");
-
-  int16_t res = montgomery_reduce((int32_t)a * (int32_t)b);
+#define fqmul MLKEM_NAMESPACE(fqmul)
+int16_t fqmul(int16_t a, int16_t b)
+    // clang-format off
+REQUIRES(b > -HALF_Q)
+REQUIRES(b < HALF_Q)
+ENSURES(RETURN_VALUE > -MLKEM_Q && RETURN_VALUE < MLKEM_Q);
+// clang-format on
 
-  SCALAR_BOUND(res, MLKEM_Q, "fqmul output");
-  return res;
-}
 
 #endif