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 <[email protected]>

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

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.

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 <stdint.h>
+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);
+}

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

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.

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

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

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.

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 <ntt.h>
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+  poly *a;
+  poly_ntt(a);
+}

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

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

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