diff --git a/cbmc/proofs/fqmul/Makefile b/cbmc/proofs/fqmul/Makefile index f0b1dd2ae..a350c0d51 100644 --- 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 index de38a215b..d7ac86d6d 100644 --- 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 index 2b8fdd0e7..18ec83207 100644 --- 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 index 110b32f8f..1322fc353 100644 --- 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