Merge pull request #292 from pq-code-package/fqmul_proof

Strengthen spec for `montgomery_reduce()`
pq-code-package · Oct 31, 2024 · 10fd1dd · 10fd1dd
2 parents 0936b16 + b3f89d8
commit 10fd1dd
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 19 deletions.
diff --git a/cbmc/proofs/fqmul/Makefile b/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
 

diff --git a/mlkem/common.h b/mlkem/common.h
@@ -4,5 +4,6 @@
 
 #define DEFAULT_ALIGN 32
 #define ALIGN __attribute__((aligned(DEFAULT_ALIGN)))
+#define ALWAYS_INLINE __attribute__((always_inline))
 
 #endif
diff --git a/mlkem/reduce.c b/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, "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

diff --git a/mlkem/reduce.h b/mlkem/reduce.h
@@ -8,43 +8,54 @@
 #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.
  *              - int16_t b: second factor.
- *                  Must be signed canonical (abs value <|q|/2)
+ *                  Must be signed canonical (abs value <(q+1)/2)
  *
  * Returns 16-bit integer congruent to a*b*R^{-1} mod q, and
  * 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