From c6e75b76385ad3ab7c1ef267f86057621b95253e Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Tue, 21 Jan 2025 10:35:09 +0000 Subject: [PATCH] NTT: Simplify computation of zeta index The n-th layer of the NTT needs the zeta table entries at indices `2^(n-1)..2^n-1`. Previously, the initial index was computed using a division by the `len` parameter, upholding the status of the `layer` parameter as a pure ghost variable only needed for the specification, but not the code itself. This commit gives up the status of `layer` as a ghost variable and instead uses it to compute the initial zeta index using a shift instead of a division. While `len` is not secret and there is, thus, no risk of information leakage when a `div` instruction is used, it still seems cleaner and faster to work with a shift. Suggested-by: Rod Chapman Signed-off-by: Hanno Becker --- mlkem/ntt.c | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/mlkem/ntt.c b/mlkem/ntt.c index 3651c8da9..58a97469d 100644 --- a/mlkem/ntt.c +++ b/mlkem/ntt.c @@ -104,10 +104,8 @@ __contract__( ensures(array_abs_bound(r, 0, MLKEM_N, (layer + 1) * MLKEM_Q))) { unsigned start, k; - /* `layer` is a ghost variable only needed in the CBMC specification */ - ((void)layer); - /* Twiddle factors for layer n start at index 2^(layer-1) */ - k = MLKEM_N / (2 * len); + /* Twiddle factors for layer n are at indices 2^(n-1)..2^n-1. */ + k = 1u << (layer - 1); for (start = 0; start < MLKEM_N; start += 2 * len) __loop__( invariant(start < MLKEM_N + 2 * len) @@ -172,9 +170,9 @@ __contract__( ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))) { unsigned start, k; - /* `layer` is a ghost variable used only in the specification */ - ((void)layer); - k = MLKEM_N / len - 1; + /* Twiddle factors for layer n are at indices 2^(n-1)..2^n-1. + * The inverse NTT uses them in backwards order. */ + k = (1u << layer) - 1; for (start = 0; start < MLKEM_N; start += 2 * len) __loop__( invariant(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))