-
Notifications
You must be signed in to change notification settings - Fork 16
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Re-baseline and introduce new fast NTT and inverse NTT code, followin…
…g source re-organization in PR#674. See comments on older PR#610. All tests, proofs, and lint OK. Signed-off-by: Rod Chapman <rodchap@amazon.com> Correct list of called functions for this proof. Signed-off-by: Rod Chapman <rodchap@amazon.com> Update autogenerated files aftre rebase Signed-off-by: Rod Chapman <rodchap@amazon.com> Re-generate autogenerated files following rebase Signed-off-by: Rod Chapman <rodchap@amazon.com> Update auto-generated files and copyright messages following rebase Signed-off-by: Rod Chapman <rodchap@amazon.com> Update copyright notices for these news files Signed-off-by: Rod Chapman <rodchap@amazon.com> Update one more copyright notice Signed-off-by: Rod Chapman <rodchap@amazon.com> Update MLKEM_NAMESPACE to MLK_NAMESPACE for all new proofs Signed-off-by: Rod Chapman <rodchap@amazon.com> Rename INLINE to MLK_INLINE for new functions here. Signed-off-by: Rod Chapman <rodchap@amazon.com> rename NTT_BOUNDx macros to MLK_NTT_BOUNDx Signed-off-by: Rod Chapman <rodchap@amazon.com>
- Loading branch information
1 parent
8582a06
commit ef16e29
Showing
34 changed files
with
1,137 additions
and
196 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
include ../Makefile_params.common | ||
|
||
HARNESS_ENTRY = 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 = invntt_layer321 | ||
|
||
DEFINES += | ||
INCLUDES += | ||
|
||
REMOVE_FUNCTION_BODY += | ||
UNWINDSET += | ||
|
||
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c | ||
|
||
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer321 | ||
USE_FUNCTION_CONTRACTS=$(MLK_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 = $(MLK_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 | ||
# 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 |
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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/poly.c | ||
|
||
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer54 | ||
USE_FUNCTION_CONTRACTS=$(MLK_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 = $(MLK_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 |
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
// Copyright (c) 2024-2025 The mlkem-native project authors | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: MIT-0 | ||
|
||
#include <poly.h> | ||
|
||
#define invntt_layer54 MLK_NAMESPACE(invntt_layer54) | ||
void invntt_layer54(int16_t *r); | ||
|
||
/** | ||
* @brief Starting point for formal analysis | ||
* | ||
*/ | ||
void harness(void) | ||
{ | ||
int16_t *a; | ||
invntt_layer54(a); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
include ../Makefile_params.common | ||
|
||
HARNESS_ENTRY = 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_layer54_butterfly | ||
|
||
DEFINES += | ||
INCLUDES += | ||
|
||
REMOVE_FUNCTION_BODY += | ||
UNWINDSET += | ||
|
||
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c | ||
|
||
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer54_butterfly | ||
USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul $(MLK_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=--smt2 | ||
|
||
FUNCTION_NAME = $(MLK_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 | ||
# 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 |
File renamed without changes.
21 changes: 21 additions & 0 deletions
21
proofs/cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
// Copyright (c) 2024-2025 The mlkem-native project authors | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: MIT-0 | ||
|
||
#include <poly.h> | ||
|
||
#define invntt_layer54_butterfly MLK_NAMESPACE(invntt_layer54_butterfly) | ||
void invntt_layer54_butterfly(int16_t r[MLKEM_N], const unsigned zeta_index, | ||
const unsigned start); | ||
|
||
/** | ||
* @brief Starting point for formal analysis | ||
* | ||
*/ | ||
void harness(void) | ||
{ | ||
int16_t *a; | ||
unsigned zi; | ||
unsigned start; | ||
invntt_layer54_butterfly(a, zi, start); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
# 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/zetas.c | ||
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c | ||
|
||
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer6 | ||
USE_FUNCTION_CONTRACTS=$(MLK_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=--smt2 | ||
|
||
FUNCTION_NAME = $(MLK_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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
# This file marks this directory as containing a CBMC proof. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
// Copyright (c) 2024-2025 The mlkem-native project authors | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: MIT-0 | ||
|
||
#include <poly.h> | ||
|
||
#define invntt_layer6 MLK_NAMESPACE(invntt_layer6) | ||
void invntt_layer6(int16_t *r); | ||
|
||
/** | ||
* @brief Starting point for formal analysis | ||
* | ||
*/ | ||
void harness(void) | ||
{ | ||
int16_t *a; | ||
invntt_layer6(a); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
# SPDX-License-Identifier: Apache-2.0 | ||
|
||
# This file marks this directory as containing a CBMC proof. |
18 changes: 18 additions & 0 deletions
18
proofs/cbmc/invntt_layer7_invert/invntt_layer7_invert_harness.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
// Copyright (c) 2024-2025 The mlkem-native project authors | ||
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
// SPDX-License-Identifier: MIT-0 | ||
|
||
#include <poly.h> | ||
|
||
#define invntt_layer7_invert MLK_NAMESPACE(invntt_layer7_invert) | ||
void invntt_layer7_invert(int16_t *r); | ||
|
||
/** | ||
* @brief Starting point for formal analysis | ||
* | ||
*/ | ||
void harness(void) | ||
{ | ||
int16_t *a; | ||
invntt_layer7_invert(a); | ||
} |
18 changes: 0 additions & 18 deletions
18
proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.