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);