Skip to content

Commit

Permalink
Force twiddle as second argument to fqmul()
Browse files Browse the repository at this point in the history
For bounds reasoning, we need to know that `fqmul()` is
always called with a signed canonical value in one of its
arguments.

To simplify the spec, this commit reorders arguments to `fqmul()`
so that the signed canonical twiddle is always the _second_ argument.

It checks this through a debug-only assertion, and also adds
a debug-assertion that the return value of `fqmul()` is always
of absolute value < MLKEM_Q.

Signed-off-by: Hanno Becker <[email protected]>
  • Loading branch information
hanno-becker committed Oct 31, 2024
1 parent 20dbffb commit 9692dd8
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 9 deletions.
4 changes: 2 additions & 2 deletions mlkem/ntt.c
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ void poly_ntt(poly *p) {
for (start = 0; start < 256; start = j + len) {
zeta = zetas[k++];
for (j = start; j < start + len; j++) {
t = fqmul(zeta, r[j + len]);
t = fqmul(r[j + len], zeta);
r[j + len] = r[j] - t;
r[j] = r[j] + t;
}
Expand Down Expand Up @@ -173,7 +173,7 @@ void poly_invntt_tomont(poly *p) {
t = r[j];
r[j] = barrett_reduce(t + r[j + len]); // abs < q/2
r[j + len] = r[j + len] - t;
r[j + len] = fqmul(zeta, r[j + len]); // abs < 3/4 q
r[j + len] = fqmul(r[j + len], zeta); // abs < 3/4 q
}
}
}
Expand Down
19 changes: 12 additions & 7 deletions mlkem/reduce.h
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
#include <stdint.h>
#include "cbmc.h"
#include "params.h"
#include "debug/debug.h"

#define MONT -1044 // 2^16 mod q
#define HALF_Q ((MLKEM_Q - 1) / 2) // 1664
Expand All @@ -29,17 +30,21 @@ ENSURES(RETURN_VALUE >= -HALF_Q && RETURN_VALUE <= HALF_Q);
* Description: Multiplication followed by Montgomery reduction
*
* Arguments: - int16_t a: first factor
* - int16_t b: second factor
* Can be any int16_t.
* - int16_t b: second factor.
* Must be signed canonical (abs value <|q|/2)
*
* Returns 16-bit integer congruent to a*b*R^{-1} mod q
*
* If one input is < |q|/2 in absolute value (which is given
* in the common case of multiplication with constants), the
* return value is < |q| in absolute value.
* 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) {
return montgomery_reduce((int32_t)a * (int32_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;
}

#endif

0 comments on commit 9692dd8

Please sign in to comment.