From 77ac5bce36c3ddb790e238d75818385f209d8392 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Mon, 11 Nov 2024 07:40:09 +0000 Subject: [PATCH] CBMC: Add proof for forward NTT This commit adds a spec and proof for the MLKEM forward NTT. The main difficulty in proving the forward NTT type-safe is to formalize the bounds reasoning showing that the additions and subtractions in the butterflies do not overflow. Luckily, very basic layer-to-layer bounds reasoning is sufficient to achieve an output bound of 8*q, which is enough for reason about the calling code: When moving from layer N to layer N+1, every coefficient is replaced by the addition or subtractio or a layer N coefficient with the result of a Barrett multiplication with a signed canonical twiddle factor. Since such Barrett multiplication always has absolute value < q (this could be improved significantly if we needed to), the absolute bounds increase by at most q. Spelling out the invariants in CBMC is cumbersome and rather verbose. To facilitate, and to keep runtimes down, this commit splits the NTT original NTT code into three functions, one per NTT loop: - The top-level poly_ntt() iterates over the layers, calling ntt_layer() - ntt_layer computes one NTT layer, calling ntt_butterfly_block() for each block of butterflies. - ntt_butterfly_block() actually does the modular arithmetic. While this makes the loop-and-feel of the NTT rather different from what it was, structurally it is almost the same as in the reference implementation. Previously, the NTT code included a runtime check for the tighter bound 5*q for the output of the NTT. The bound and the check are removed in this commit: While they are still true, it is confusing to runtime check for a different value than what we are proving. Instead, a comment is left. Signed-off-by: Hanno Becker --- cbmc/proofs/ntt_butterfly_block/Makefile | 54 +++++ .../proofs/ntt_butterfly_block/cbmc-proof.txt | 3 + .../ntt_butterfly_block_harness.c | 24 +++ cbmc/proofs/ntt_layer/Makefile | 54 +++++ cbmc/proofs/ntt_layer/cbmc-proof.txt | 3 + cbmc/proofs/ntt_layer/ntt_layer_harness.c | 29 +++ cbmc/proofs/poly_ntt/Makefile | 54 +++++ cbmc/proofs/poly_ntt/cbmc-proof.txt | 3 + cbmc/proofs/poly_ntt/poly_ntt_harness.c | 27 +++ mlkem/cbmc.h | 6 + mlkem/common.h | 3 + mlkem/debug/debug.h | 1 - mlkem/ntt.c | 185 +++++++++++------- mlkem/ntt.h | 42 +++- 14 files changed, 420 insertions(+), 68 deletions(-) create mode 100644 cbmc/proofs/ntt_butterfly_block/Makefile create mode 100644 cbmc/proofs/ntt_butterfly_block/cbmc-proof.txt create mode 100644 cbmc/proofs/ntt_butterfly_block/ntt_butterfly_block_harness.c create mode 100644 cbmc/proofs/ntt_layer/Makefile create mode 100644 cbmc/proofs/ntt_layer/cbmc-proof.txt create mode 100644 cbmc/proofs/ntt_layer/ntt_layer_harness.c create mode 100644 cbmc/proofs/poly_ntt/Makefile create mode 100644 cbmc/proofs/poly_ntt/cbmc-proof.txt create mode 100644 cbmc/proofs/poly_ntt/poly_ntt_harness.c diff --git a/cbmc/proofs/ntt_butterfly_block/Makefile b/cbmc/proofs/ntt_butterfly_block/Makefile new file mode 100644 index 000000000..6aeeef19c --- /dev/null +++ b/cbmc/proofs/ntt_butterfly_block/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = ntt_butterfly_block_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = ntt_butterfly_block + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c + +CHECK_FUNCTION_CONTRACTS=ntt_butterfly_block +USE_FUNCTION_CONTRACTS= $(MLKEM_NAMESPACE)fqmul +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = ntt_butterfly_block + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 9 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/ntt_butterfly_block/cbmc-proof.txt b/cbmc/proofs/ntt_butterfly_block/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/ntt_butterfly_block/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/ntt_butterfly_block/ntt_butterfly_block_harness.c b/cbmc/proofs/ntt_butterfly_block/ntt_butterfly_block_harness.c new file mode 100644 index 000000000..b8ec731ba --- /dev/null +++ b/cbmc/proofs/ntt_butterfly_block/ntt_butterfly_block_harness.c @@ -0,0 +1,24 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file ntt_butterfly_block_harness.c + * @brief Implements the proof harness for ntt_butterfly_block function. + */ +#include +void ntt_butterfly_block(int16_t *r, int16_t root, int start, int len, + int bound); + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + int16_t *r, root; + int start, stride, bound; + ntt_butterfly_block(r, root, start, stride, bound); +} diff --git a/cbmc/proofs/ntt_layer/Makefile b/cbmc/proofs/ntt_layer/Makefile new file mode 100644 index 000000000..82a30bdea --- /dev/null +++ b/cbmc/proofs/ntt_layer/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = ntt_layer_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = ntt_layer + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c + + CHECK_FUNCTION_CONTRACTS=ntt_layer +USE_FUNCTION_CONTRACTS= ntt_butterfly_block +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = ntt_layer + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/ntt_layer/cbmc-proof.txt b/cbmc/proofs/ntt_layer/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/ntt_layer/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/ntt_layer/ntt_layer_harness.c b/cbmc/proofs/ntt_layer/ntt_layer_harness.c new file mode 100644 index 000000000..54e492412 --- /dev/null +++ b/cbmc/proofs/ntt_layer/ntt_layer_harness.c @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file poly_ntt_harness.c + * @brief Implements the proof harness for poly_ntt function. + */ + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include "poly.h" +void ntt_layer(int16_t *p, int len, int layer); + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + int16_t *a; + int len, layer; + ntt_layer(a, len, layer); +} diff --git a/cbmc/proofs/poly_ntt/Makefile b/cbmc/proofs/poly_ntt/Makefile new file mode 100644 index 000000000..856a3aba2 --- /dev/null +++ b/cbmc/proofs/poly_ntt/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_ntt_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_ntt + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c + + CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_ntt +USE_FUNCTION_CONTRACTS= ntt_layer +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_ntt + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/poly_ntt/cbmc-proof.txt b/cbmc/proofs/poly_ntt/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/poly_ntt/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/poly_ntt/poly_ntt_harness.c b/cbmc/proofs/poly_ntt/poly_ntt_harness.c new file mode 100644 index 000000000..64502de15 --- /dev/null +++ b/cbmc/proofs/poly_ntt/poly_ntt_harness.c @@ -0,0 +1,27 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + +/** + * @file poly_ntt_harness.c + * @brief Implements the proof harness for poly_ntt function. + */ + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) { + poly *a; + poly_ntt(a); +} diff --git a/mlkem/cbmc.h b/mlkem/cbmc.h index c43c1bef6..6a5b2bc64 100644 --- a/mlkem/cbmc.h +++ b/mlkem/cbmc.h @@ -4,6 +4,8 @@ // Basic replacements for __CPROVER_XXX contracts /////////////////////////////////////////////////// +#include "common.h" + #ifndef CBMC #define STATIC_TESTABLE static @@ -135,4 +137,8 @@ // clang-format on +// Wrapper around ARRAY_IN_BOUNDS operating on absolute values +#define ARRAY_ABS_BOUND(arr, lb, ub, k) \ + ARRAY_IN_BOUNDS((lb), (ub), (arr), (-(k)), (k)) + #endif diff --git a/mlkem/common.h b/mlkem/common.h index d7ac86d6d..76504b88e 100644 --- a/mlkem/common.h +++ b/mlkem/common.h @@ -6,4 +6,7 @@ #define ALIGN __attribute__((aligned(DEFAULT_ALIGN))) #define ALWAYS_INLINE __attribute__((always_inline)) +#define MLKEM_CONCAT_(left, right) left##right +#define MLKEM_CONCAT(left, right) MLKEM_CONCAT_(left, right) + #endif diff --git a/mlkem/debug/debug.h b/mlkem/debug/debug.h index 13b18418c..03ede7365 100644 --- a/mlkem/debug/debug.h +++ b/mlkem/debug/debug.h @@ -144,7 +144,6 @@ void mlkem_debug_print_error(const char *file, int line, const char *msg); } while (0) // Following AWS-LC to define a C99-compliant static assert -#define MLKEM_CONCAT(left, right) left##right #define MLKEM_STATIC_ASSERT_DEFINE(cond, msg) \ typedef struct { \ unsigned int MLKEM_CONCAT(static_assertion_, msg) : (cond) ? 1 : -1; \ diff --git a/mlkem/ntt.c b/mlkem/ntt.c index ca123ff4b..62eff23c5 100644 --- a/mlkem/ntt.c +++ b/mlkem/ntt.c @@ -55,68 +55,137 @@ const int16_t zetas[128] = { -1187, -1659, -1185, -1530, -1278, 794, -1510, -854, -870, 478, -108, -308, 996, 991, 958, -1460, 1522, 1628}; -/************************************************* - * Name: poly_ntt - * - * Description: Computes negacyclic number-theoretic transform (NTT) of - * a polynomial in place. - * - * The input is assumed to be in normal order and - * coefficient-wise bound by MLKEM_Q in absolute value. - * - * The output polynomial is in bitreversed order, and - * coefficient-wise bound by NTT_BOUND in absolute value. - * - * (NOTE: Sometimes the input to the NTT is actually smaller, - * which gives better bounds.) - * - * Arguments: - poly *p: pointer to in/output polynomial - **************************************************/ #if !defined(MLKEM_USE_NATIVE_NTT) +// Computes a block CT butterflies with a fixed twiddle factor, +// using Montgomery multiplication. +// +// Parameters: +// - r: Pointer to base of polynomial (_not_ the base of butterfly block) +// - root: Twiddle factor to use for the butterfly. This must be in +// Montgomery form and signed canonical. +// - start: Offset to the beginning of the butterfly block +// - len: Index difference between coefficients subject to a butterfly +// - bound: Ghost variable describing coefficient bound: Prior to `start`, +// coefficients must be bound by `bound + MLKEM_Q`. Post `start`, +// they must be bound by `bound`. +// +// When this function returns, output coefficients in the index range +// [start, start+2*len) have bound bumped to `bound + MLKEM_Q`. +// +// Example: +// - start=8, len=4 +// This would compute the following four butterflies +// +// 8 -- 12 +// 9 -- 13 +// 10 -- 14 +// 11 -- 15 +// +// - start=4, len=2 +// This would compute the following two butterflies +// +// 4 -- 6 +// 5 -- 7 +// +STATIC_TESTABLE +void ntt_butterfly_block(int16_t r[MLKEM_N], int16_t zeta, int start, int len, + int bound) // clang-format off + REQUIRES(0 <= start && start < MLKEM_N) + REQUIRES(1 <= len && len <= MLKEM_N / 2 && start + 2 * len <= MLKEM_N) + REQUIRES(0 <= bound && bound < INT16_MAX - MLKEM_Q) + REQUIRES(-HALF_Q < zeta && zeta < HALF_Q) + REQUIRES(IS_FRESH(r, sizeof(int16_t) * MLKEM_N)) + REQUIRES(ARRAY_ABS_BOUND(r, 0, start - 1, bound + MLKEM_Q)) + REQUIRES(ARRAY_ABS_BOUND(r, start, MLKEM_N - 1, bound)) + ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) + ENSURES(ARRAY_ABS_BOUND(r, 0, start + 2*len - 1, bound + MLKEM_Q)) + ENSURES(ARRAY_ABS_BOUND(r, start + 2 * len, MLKEM_N - 1, bound)) +// clang-format on +{ + // `bound` is a ghost variable only needed in the CBMC specification + ((void)bound); + for (int j = start; j < start + len; j++) // clang-format off + ASSIGNS(j, OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) + INVARIANT(start <= j && j <= start + len) + // Coefficients are updated in strided pairs, so the bounds for the + // intermediate states alternate twice between the old and new bound + INVARIANT(ARRAY_ABS_BOUND(r, 0, j - 1, bound + MLKEM_Q)) + INVARIANT(ARRAY_ABS_BOUND(r, j, start + len - 1, bound)) + INVARIANT(ARRAY_ABS_BOUND(r, start + len, j + len - 1, bound + MLKEM_Q)) + INVARIANT(ARRAY_ABS_BOUND(r, j + len, MLKEM_N - 1, bound)) + // clang-format on + { + int16_t t; + t = fqmul(r[j + len], zeta); + r[j + len] = r[j] - t; + r[j] = r[j] + t; + } +} -// Check that the specific bound for the reference NTT implies -// the bound required by the C<->Native interface. -#define NTT_BOUND_REF (5 * MLKEM_Q) -STATIC_ASSERT(NTT_BOUND_REF <= NTT_BOUND, ntt_ref_bound) +// Compute one layer of forward NTT +// +// Parameters: +// - r: Pointer to base of polynomial +// - len: Stride of butterflies in this layer. +// - layer: Ghost variable indicating which layer is being applied. +// Must match `len` via `len == MLKEM_N >> layer`. +// +// Note: `len` could be dropped and computed in the function, but +// we are following the structure of the reference NTT from the +// official Kyber implementation here, merely adding `layer` as +// a ghost variable for the specifications. +STATIC_TESTABLE +void ntt_layer(int16_t r[MLKEM_N], int len, int layer) // clang-format off + REQUIRES(IS_FRESH(r, sizeof(int16_t) * MLKEM_N)) + REQUIRES(1 <= layer && layer <= 7 && len == (MLKEM_N >> layer)) + REQUIRES(ARRAY_ABS_BOUND(r, 0, MLKEM_N - 1, layer * MLKEM_Q - 1)) + ASSIGNS(OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) + ENSURES(ARRAY_ABS_BOUND(r, 0, MLKEM_N - 1, (layer + 1) * MLKEM_Q - 1)) +// clang-format on +{ + // `layer` is a ghost variable only needed in the specification + ((void)layer); + // Twiddle factors for layer n start at index 2^(layer-1) + int k = MLKEM_N / (2 * len); + for (int start = 0; start < MLKEM_N; start += 2 * len) // clang-format off + ASSIGNS(start, k, OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) + INVARIANT(0 <= start && start < MLKEM_N + 2 * len) + INVARIANT(0 <= k && k <= MLKEM_N / 2 && 2 * len * k == start + MLKEM_N) + INVARIANT(ARRAY_ABS_BOUND(r, 0, start - 1, (layer * MLKEM_Q - 1) + MLKEM_Q)) + INVARIANT(ARRAY_ABS_BOUND(r, start, MLKEM_N - 1, layer * MLKEM_Q - 1)) + // clang-format on + { + int16_t zeta = zetas[k++]; + ntt_butterfly_block(r, zeta, start, len, layer * MLKEM_Q - 1); + } +} +// Compute full forward NTT +// +// NOTE: This particular implementation satisfies a much tighter +// bound on the output coefficients (5*q) than the contractual one (8*q), +// but this is not needed in the calling code. Should we change the +// base multiplication strategy to require smaller NTT output bounds, +// the proof may need strengthening. +// // REF-CHANGE: Removed indirection poly_ntt -> ntt() // and integrated polynomial reduction into the NTT. void poly_ntt(poly *p) { POLY_BOUND_MSG(p, MLKEM_Q, "ref ntt input"); - - unsigned int len, start, j, k; - int16_t t, zeta; int16_t *r = p->coeffs; - k = 1; - - // Bounds reasoning: - // - There are 7 layers - // - When passing from layer N to layer N+1, each layer-N value - // is modified through the addition/subtraction of a Montgomery - // product of a twiddle of absolute value < q/2 and a layer-N value. - // - Recalling that |fqmul(a,t)| < q * (0.0254*C + 1/2) for - // |a| < C*q and |t|= 2; len >>= 1) { - for (start = 0; start < 256; start = j + len) { - zeta = zetas[k++]; - for (j = start; j < start + len; j++) { - t = fqmul(r[j + len], zeta); - r[j + len] = r[j] - t; - r[j] = r[j] + t; - } + for (int len = 128, layer = 1; len >= 2; + len >>= 1, layer++) // clang-format off + ASSIGNS(len, layer, OBJECT_UPTO(r, sizeof(int16_t) * MLKEM_N)) + INVARIANT(1 <= layer && layer <= 8 && len == (MLKEM_N >> layer)) + INVARIANT(ARRAY_ABS_BOUND(r, 0, MLKEM_N - 1, layer * MLKEM_Q - 1)) + // clang-format on + { + ntt_layer(r, len, layer); } - } // Check the stronger bound - POLY_BOUND_MSG(p, NTT_BOUND_REF, "ref ntt output"); + POLY_BOUND_MSG(p, NTT_BOUND, "ref ntt output"); } #else /* MLKEM_USE_NATIVE_NTT */ @@ -130,22 +199,6 @@ void poly_ntt(poly *p) { } #endif /* MLKEM_USE_NATIVE_NTT */ -/************************************************* - * Name: poly_invntt_tomont - * - * Description: Computes inverse of negacyclic number-theoretic transform (NTT) - * of a polynomial in place; - * inputs assumed to be in bitreversed order, output in normal - * order - * - * The input is assumed to be in bitreversed order, and can - * have arbitrary coefficients in int16_t. - * - * The output polynomial is in normal order, and - * coefficient-wise bound by INVNTT_BOUND in absolute value. - * - * Arguments: - uint16_t *a: pointer to in/output polynomial - **************************************************/ #if !defined(MLKEM_USE_NATIVE_INTT) // Check that bound for reference invNTT implies contractual bound diff --git a/mlkem/ntt.h b/mlkem/ntt.h index dc7e3c4a7..cccf2526b 100644 --- a/mlkem/ntt.h +++ b/mlkem/ntt.h @@ -4,6 +4,7 @@ #include #include "arith_native.h" +#include "cbmc.h" #include "params.h" #include "poly.h" #include "reduce.h" @@ -11,9 +12,48 @@ #define zetas MLKEM_NAMESPACE(zetas) extern const int16_t zetas[128]; +/************************************************* + * Name: poly_ntt + * + * Description: Computes negacyclic number-theoretic transform (NTT) of + * a polynomial in place. + * + * The input is assumed to be in normal order and + * coefficient-wise bound by MLKEM_Q in absolute value. + * + * The output polynomial is in bitreversed order, and + * coefficient-wise bound by NTT_BOUND in absolute value. + * + * (NOTE: Sometimes the input to the NTT is actually smaller, + * which gives better bounds.) + * + * Arguments: - poly *p: pointer to in/output polynomial + **************************************************/ + #define poly_ntt MLKEM_NAMESPACE(poly_ntt) -void poly_ntt(poly *r); +void poly_ntt(poly *r) // clang-format off +REQUIRES(IS_FRESH(r, sizeof(poly))) +REQUIRES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), MLKEM_Q - 1)) +ASSIGNS(OBJECT_UPTO(r, sizeof(poly))) +ENSURES(ARRAY_IN_BOUNDS(0, MLKEM_N - 1, r->coeffs, -(NTT_BOUND - 1), NTT_BOUND - 1)); +// clang-format on +/************************************************* + * Name: poly_invntt_tomont + * + * Description: Computes inverse of negacyclic number-theoretic transform (NTT) + * of a polynomial in place; + * inputs assumed to be in bitreversed order, output in normal + * order + * + * The input is assumed to be in bitreversed order, and can + * have arbitrary coefficients in int16_t. + * + * The output polynomial is in normal order, and + * coefficient-wise bound by INVNTT_BOUND in absolute value. + * + * Arguments: - uint16_t *a: pointer to in/output polynomial + **************************************************/ #define poly_invntt_tomont MLKEM_NAMESPACE(poly_invntt_tomont) void poly_invntt_tomont(poly *r);