Add fast, layer-merged forward and inverse NTT code.

Adjust and move proof files accordingly.

Signed-off-by: Rod Chapman <[email protected]>

Add support for NO_INLINE attribute and its
use with CBMC.

Signed-off-by: Rod Chapman <[email protected]>

Make top-level ntt_layer*() functions NO_INLINE
to improve comprehension and review of auto-vectorization
of this code.

Signed-off-by: Rod Chapman <[email protected]>

Add first two fast Invert NTT functions

Adds
  invntt_layer7_invert_inner()
  invntt_layer7_invert()

and their proof files.

Signed-off-by: Rod Chapman <[email protected]>

Remove dummy call to invntt_layer7_invert()

Signed-off-by: Rod Chapman <[email protected]>

Add Invert NTT Layer 6 functions.

Adds
  invntt_layer6_inner()
  invntt_layer6()
functions and their proof files.

Signed-off-by: Rod Chapman <[email protected]>

Simplify Zeta tables for layers 4 and 5.

Signed-off-by: Rod Chapman <[email protected]>

Adds Inverse NTT Layer54 (marged)

Adds functions
  invntt_layer54_inner()
  invntt_layer54()

and their proof files.

Signed-off-by: Rod Chapman <[email protected]>

Use new zeta constants in ntt_layer123()

Signed-off-by: Rod Chapman <[email protected]>

Adds first full implemenation of Inverse NTT with layer merging.

Adds function invntt_layer321() and its proof.

Updates top-level poly_invntt_tomont() to call new layer-merged implementation.

Renames existing implementation as poly_invntt_tomont_ref() for now.

Signed-off-by: Rod Chapman <[email protected]>

Update proof of poly_invntt_tomont()

Signed-off-by: Rod Chapman <[email protected]>

Remove reference implementation of poly_invntt_tomont()

Also removes local function invntt_layer()
and its proof.

Signed-off-by: Rod Chapman <[email protected]>

Switch to Z3 for these proofs, which is much faster than Bitwuzla.

Signed-off-by: Rod Chapman <[email protected]>

Switch back to Z3 for proof of ntt_layer123()

Signed-off-by: Rod Chapman <[email protected]>

Rename ntt_layer45_slice() to ntt_inner45_inner()

Signed-off-by: Rod Chapman <[email protected]>

Rename proof files

Signed-off-by: Rod Chapman <[email protected]>

Further renaming of ntt_layer45_slice() to ntt_layer45_inner()

Signed-off-by: Rod Chapman <[email protected]>

Rename *_slice() to *_inner() functions - phase 1

Signed-off-by: Rod Chapman <[email protected]>

Rename *_slice() functions to *_inner() - phase 2

Signed-off-by: Rod Chapman <[email protected]>

renaming *slioce() to *inner() - phase 3

Signed-off-by: Rod Chapman <[email protected]>

Display final 4 lines of logs/result.txt after make result

Signed-off-by: Rod Chapman <[email protected]>

Rename inner to butterfly for all internal ntt functions

Signed-off-by: Rod Chapman <[email protected]>

Rename harness function source files

Signed-off-by: Rod Chapman <[email protected]>

Adjust proof Makefiles and harnesses for renaming inner to butterfly

Signed-off-by: Rod Chapman <[email protected]>

Update Makefiles for function renaming

Signed-off-by: Rod Chapman <[email protected]>

Rename all inner functions to butterfly

Signed-off-by: Rod Chapman <[email protected]>

Replace literal 255 with (MLKEM_N - 1) throughout

Signed-off-by: Rod Chapman <[email protected]>

Move declaration of Zeta tables to be as close to their
point of first use as possible.

Add and adjust comments.

Signed-off-by: Rod Chapman <[email protected]>

Align and rename Zetas tables.

Signed-off-by: Rod Chapman <[email protected]>

Zetas tables are all declared with static scope

Signed-off-by: Rod Chapman <[email protected]>

Auto-generate Zeta tables for new layer-merged NTT

Signed-off-by: Rod Chapman <[email protected]>

This proof no longer needs zetas.c as a source file

Signed-off-by: Rod Chapman <[email protected]>

Move basemul_cached() function from ntt.[hc] to poly.c

It is now local, and static within poly.c, so is amenable
to inlining and auto-vectorization within that unit.

Signed-off-by: Rod Chapman <[email protected]>

Make basemul_cached() inline-able

Signed-off-by: Rod Chapman <[email protected]>

Add top-level explanatory comments

Signed-off-by: Rod Chapman <[email protected]>

Clarify and correct 1 typo in comment only.

Signed-off-by: Rod Chapman <[email protected]>

Move symlink from zetas.c to zetas.i

Signed-off-by: Rod Chapman <[email protected]>

Correct INVNTT_BOUND_REF for new implementation of Inverse NTT

Signed-off-by: Rod Chapman <[email protected]>

Add MLKEM_NAMESPACE to mlkem_layer7_zetas, since it is a global symbol

Signed-off-by: Rod Chapman <[email protected]>

Remove boilerplate comments from proof harness sources.

Signed-off-by: Rod Chapman <[email protected]>

Updates for namespacing of all static functions.

Signed-off-by: Rod Chapman <[email protected]>

Update this file following changes to other files

Signed-off-by: Rod Chapman <[email protected]>

Remove pc typedef and use int16_t r[MLKEM_N] instead throughout

Signed-off-by: Rod Chapman <[email protected]>

Adds namespacing to all static constant lookup tables.

In support of the monolithic build.

Signed-off-by: Rod Chapman <[email protected]>

Update auto-generates files following name-spacing of Zeta tables

Signed-off-by: Rod Chapman <[email protected]>

Remove declaration of basmul_cached() from ntt.h following rebase against PR 623

Signed-off-by: Rod Chapman <[email protected]>

Correct declaration of basemul_cached() to be static

Signed-off-by: Rod Chapman <[email protected]>

basemul_cached() is explicitly static, so does not also need MLKEM_NATIVE_INTERNAL_API

Signed-off-by: Rod Chapman <[email protected]>

remove sym link to zetas.c

Signed-off-by: Rod Chapman <[email protected]>

Add new symlink for zetas.i

Signed-off-by: Rod Chapman <[email protected]>

Add internal ct_butterfly() function and use it in ntt_layer123()

Same for other NTT layers and InvNTT is TBD.

Signed-off-by: Rod Chapman <[email protected]>

Update autogenerated file

Signed-off-by: Rod Chapman <[email protected]>

Update invariant and constants for exclusive array bounds checks.

Updates only ntt_layer123() for now to confirm effectiveness
of updates. Other functions will be updated once all is well.

Signed-off-by: Rod Chapman <[email protected]>

Update proofs for exclusive upper bound.

1. Upper bound of quantitied ranges is now exclusive
2. Upper bound of array element range constraint is now exclusive.

Signed-off-by: Rod Chapman <[email protected]>

Re-generate all auto-generated files after rebase

Signed-off-by: Rod Chapman <[email protected]>

Use inner ct_butterfly() function in all forward NTT functions.

Signed-off-by: Rod Chapman <[email protected]>

Updates for readability following review.

Introduces local gs_butterfly_reduce() and
gs_butterfly_defer() functions, which are inlined
for both compilation and proof, but significantly
simplify and improve readability of the calling
functions.

Signed-off-by: Rod Chapman <[email protected]>

Update auto-generated files after rebase

Signed-off-by: Rod Chapman <[email protected]>

Remove final STATIC_ASSERT() macro use

Signed-off-by: Rod Chapman <[email protected]>

Switch to unsigned type for loop index variables.

Signed-off-by: Rod Chapman <[email protected]>

Clarify comment on vectorization strategy

Signed-off-by: Rod Chapman <[email protected]>

Author: rod-chapman

cbmc/Makefile.common

@@ -953,6 +953,7 @@ result:
 	$(MAKE) -B _result
 	@ echo Running 'litani build'
 	$(LITANI) run-build
+	tail -4 $(LOGDIR)/result.txt
 
 _property: $(LOGDIR)/property.xml
 property:

cbmc/basemul_cached/Makefile

@@ -16,7 +16,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)basemul_cached
 USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)montgomery_reduce

cbmc/basemul_cached/basemul_cached_harness.c

@@ -6,6 +6,10 @@
 #include "ntt.h"
 #include "reduce.h"
 
+#define basemul_cached MLKEM_NAMESPACE(basemul_cached)
+void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2],
+                    const int16_t b_cached);
+
 void harness(void)
 {
   int16_t *a, *b, *r, b_cached;

cbmc/ntt_butterfly_block/Makefile renamed to cbmc/invntt_layer321/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = ntt_butterfly_block_harness
+HARNESS_FILE = invntt_layer321_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
+PROOF_UID = invntt_layer321
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ntt_butterfly_block
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer321
 USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = ntt_butterfly_block
+FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer321
 
 # 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
@@ -36,7 +36,7 @@ FUNCTION_NAME = ntt_butterfly_block
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 9
+CBMC_OBJECT_BITS = 10
 
 # 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

cbmc/invntt_layer/cbmc-proof.txt renamed to cbmc/invntt_layer321/cbmc-proof.txt

@@ -2,15 +2,17 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: MIT-0
 
-#include <stdint.h>
-#include "common.h"
+#include <ntt.h>
 
-#define invntt_layer MLKEM_NAMESPACE(invntt_layer)
-void invntt_layer(int16_t *p, int len, int layer);
+#define invntt_layer321 MLKEM_NAMESPACE(invntt_layer321)
+void invntt_layer321(int16_t *r);
 
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
 void harness(void)
 {
   int16_t *a;
-  int len, layer;
-  invntt_layer(a, len, layer);
+  invntt_layer321(a);
 }

cbmc/invntt_layer/invntt_layer_harness.c renamed to cbmc/invntt_layer321/invntt_layer321_harness.c

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = invntt_layer54_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 = invntt_layer54
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer54
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer54_butterfly
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer54
+
+# 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 = 10
+
+# 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/invntt_layer54/Makefile

@@ -0,0 +1,18 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <ntt.h>
+
+#define invntt_layer54 MLKEM_NAMESPACE(invntt_layer54)
+void invntt_layer54(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  invntt_layer54(a);
+}

cbmc/ntt_butterfly_block/cbmc-proof.txt renamed to cbmc/invntt_layer54/cbmc-proof.txt

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = invntt_layer_harness
+HARNESS_FILE = invntt_layer54_butterfly_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 = invntt_layer
+PROOF_UID = invntt_layer54_butterfly
 
 DEFINES +=
 INCLUDES +=
@@ -16,9 +16,9 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c $(SRCDIR)/mlkem/zetas.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer54_butterfly
 USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul $(MLKEM_NAMESPACE)barrett_reduce
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = invntt_layer
+FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer54_butterfly
 
 # 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
@@ -36,7 +36,7 @@ FUNCTION_NAME = invntt_layer
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 10
 
 # 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

cbmc/invntt_layer54/invntt_layer54_harness.c

@@ -0,0 +1,20 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <ntt.h>
+
+#define invntt_layer54_butterfly MLKEM_NAMESPACE(invntt_layer54_butterfly)
+void invntt_layer54_butterfly(int16_t *r, int zeta_index, int start);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  int zi;
+  int start;
+  invntt_layer54_butterfly(a, zi, start);
+}

cbmc/invntt_layer/Makefile renamed to cbmc/invntt_layer54_butterfly/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = invntt_layer6_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 = invntt_layer6
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer6
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer6_butterfly
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)invntt_layer6
+
+# 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 = 10
+
+# 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/ntt_layer/cbmc-proof.txt renamed to cbmc/invntt_layer54_butterfly/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c

@@ -0,0 +1,18 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <ntt.h>
+
+#define invntt_layer6 MLKEM_NAMESPACE(invntt_layer6)
+void invntt_layer6(int16_t *r);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  invntt_layer6(a);
+}

cbmc/invntt_layer6/Makefile

@@ -0,0 +1,54 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = invntt_layer6_butterfly_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 = invntt_layer6_butterfly
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)invntt_layer6_butterfly
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul $(MLKEM_NAMESPACE)barrett_reduce
+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)invntt_layer6_butterfly
+
+# 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 = 10
+
+# 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/invntt_layer6/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/invntt_layer6/invntt_layer6_harness.c

@@ -0,0 +1,20 @@
+// Copyright (c) 2024 The mlkem-native project authors
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+#include <ntt.h>
+
+#define invntt_layer6_butterfly MLKEM_NAMESPACE(invntt_layer6_butterfly)
+void invntt_layer6_butterfly(int16_t *r, int zeta_index, int start);
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void)
+{
+  int16_t *a;
+  int zi;
+  int start;
+  invntt_layer6_butterfly(a, zi, start);
+}