Skip to content

Commit 02c8423

Browse files
rod-chapmanrod-chapman
committed
Re-baseline and introduce new fast NTT and inverse NTT code, following source re-organization in PR#674.
See comments on older PR#610. All tests, proofs, and lint OK. Signed-off-by: Rod Chapman <[email protected]> Correct list of called functions for this proof. Signed-off-by: Rod Chapman <[email protected]> Update autogenerated files aftre rebase Signed-off-by: Rod Chapman <[email protected]> Re-generate autogenerated files following rebase Signed-off-by: Rod Chapman <[email protected]> Update auto-generated files and copyright messages following rebase Signed-off-by: Rod Chapman <[email protected]> Update copyright notices for these news files Signed-off-by: Rod Chapman <[email protected]> Update one more copyright notice Signed-off-by: Rod Chapman <[email protected]> Update MLKEM_NAMESPACE to MLK_NAMESPACE for all new proofs Signed-off-by: Rod Chapman <[email protected]> Rename INLINE to MLK_INLINE for new functions here. Signed-off-by: Rod Chapman <[email protected]> rename NTT_BOUNDx macros to MLK_NTT_BOUNDx Signed-off-by: Rod Chapman <[email protected]> Remove redundant cbmc-proof.txt files following PR#794 Signed-off-by: Rod Chapman <[email protected]> Rename static functions with mlk_ prefix Signed-off-by: Rod Chapman <[email protected]> Rename proof directories accordingly Signed-off-by: Rod Chapman <[email protected]> Update Makefiles and harnesses following addition of mlk_ prefix on static functions in poly.c Signed-off-by: Rod Chapman <[email protected]> Rename directories to make lint happy Signed-off-by: Rod Chapman <[email protected]> Further adjustments to Makefiles and harnesses Signed-off-by: Rod Chapman <[email protected]>
1 parent 6a90911 commit 02c8423

26 files changed

+1077
-192
lines changed

‎mlkem/poly.c

Lines changed: 515 additions & 143 deletions
Large diffs are not rendered by default.

‎proofs/cbmc/invntt_layer321/Makefile

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = mlk_invntt_layer321_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = mlk_invntt_layer321
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.inc
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
21+
22+
CHECK_FUNCTION_CONTRACTS=mlk_invntt_layer321
23+
USE_FUNCTION_CONTRACTS=mlk_fqmul
24+
APPLY_LOOP_CONTRACTS=on
25+
USE_DYNAMIC_FRAMES=1
26+
27+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
28+
EXTERNAL_SAT_SOLVER=
29+
CBMCFLAGS=--bitwuzla
30+
31+
FUNCTION_NAME = mlk_invntt_layer321
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# This function is large enough to need...
40+
CBMC_OBJECT_BITS = 10
41+
42+
# If you require access to a file-local ("static") function or object to conduct
43+
# your proof, set the following (and do not include the original source file
44+
# ("mlkem/poly.c") in PROJECT_SOURCES).
45+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
46+
# include ../Makefile.common
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
49+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
50+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
51+
# be set before including Makefile.common, but any use of variables on the
52+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
53+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
54+
55+
include ../Makefile.common

‎proofs/cbmc/invntt_layer321/mlk_invntt_layer321_harness.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// Copyright (c) 2024-2025 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
#include <poly.h>
6+
7+
void mlk_invntt_layer321(int16_t *r);
8+
9+
/**
10+
* @brief Starting point for formal analysis
11+
*
12+
*/
13+
void harness(void)
14+
{
15+
int16_t *a;
16+
mlk_invntt_layer321(a);
17+
}

‎proofs/cbmc/invntt_layer54/Makefile

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = mlk_invntt_layer54_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = mlk_invntt_layer54
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
20+
21+
CHECK_FUNCTION_CONTRACTS=mlk_invntt_layer54
22+
USE_FUNCTION_CONTRACTS=mlk_invntt_layer54_block
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
27+
EXTERNAL_SAT_SOLVER=
28+
CBMCFLAGS=--smt2
29+
30+
FUNCTION_NAME = mlk_invntt_layer54
31+
32+
# If this proof is found to consume huge amounts of RAM, you can set the
33+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
34+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
35+
# documentation in Makefile.common under the "Job Pools" heading for details.
36+
# EXPENSIVE = true
37+
38+
# This function is large enough to need...
39+
CBMC_OBJECT_BITS = 10
40+
41+
# If you require access to a file-local ("static") function or object to conduct
42+
# your proof, set the following (and do not include the original source file
43+
# ("mlkem/poly.c") in PROJECT_SOURCES).
44+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
45+
# include ../Makefile.common
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
49+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
50+
# be set before including Makefile.common, but any use of variables on the
51+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
52+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
53+
54+
include ../Makefile.common

‎proofs/cbmc/invntt_layer/invntt_layer_harness.c renamed to ‎proofs/cbmc/invntt_layer54/mlk_invntt_layer54_harness.c

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,17 @@
22
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
33
// SPDX-License-Identifier: MIT-0
44

5-
#include <stdint.h>
6-
#include "common.h"
5+
#include <poly.h>
76

87

9-
void mlk_invntt_layer(int16_t *p, unsigned layer);
8+
void mlk_invntt_layer54(int16_t *r);
109

10+
/**
11+
* @brief Starting point for formal analysis
12+
*
13+
*/
1114
void harness(void)
1215
{
1316
int16_t *a;
14-
unsigned layer;
15-
mlk_invntt_layer(a, layer);
17+
mlk_invntt_layer54(a);
1618
}

‎proofs/cbmc/invntt_layer54_block/Makefile

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = mlk_invntt_layer54_block_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = mlk_invntt_layer54_block
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.inc
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
21+
22+
CHECK_FUNCTION_CONTRACTS=mlk_invntt_layer54_block
23+
USE_FUNCTION_CONTRACTS=mlk_fqmul mlk_barrett_reduce
24+
APPLY_LOOP_CONTRACTS=on
25+
USE_DYNAMIC_FRAMES=1
26+
27+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
28+
EXTERNAL_SAT_SOLVER=
29+
CBMCFLAGS=--smt2
30+
31+
FUNCTION_NAME = mlk_invntt_layer54_block
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# This function is large enough to need...
40+
CBMC_OBJECT_BITS = 10
41+
42+
# If you require access to a file-local ("static") function or object to conduct
43+
# your proof, set the following (and do not include the original source file
44+
# ("mlkem/poly.c") in PROJECT_SOURCES).
45+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
46+
# include ../Makefile.common
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
49+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
50+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
51+
# be set before including Makefile.common, but any use of variables on the
52+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
53+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
54+
55+
include ../Makefile.common

‎proofs/cbmc/invntt_layer54_block/mlk_invntt_layer54_block_harness.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Copyright (c) 2024-2025 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
#include <poly.h>
6+
7+
void mlk_invntt_layer54_block(int16_t r[MLKEM_N], const unsigned zeta_index,
8+
const unsigned start);
9+
10+
/**
11+
* @brief Starting point for formal analysis
12+
*
13+
*/
14+
void harness(void)
15+
{
16+
int16_t *a;
17+
unsigned zi;
18+
unsigned start;
19+
mlk_invntt_layer54_block(a, zi, start);
20+
}

‎proofs/cbmc/invntt_layer6/Makefile

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = mlk_invntt_layer6_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = mlk_invntt_layer6
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.inc
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
21+
22+
CHECK_FUNCTION_CONTRACTS=mlk_invntt_layer6
23+
USE_FUNCTION_CONTRACTS=mlk_fqmul
24+
APPLY_LOOP_CONTRACTS=on
25+
USE_DYNAMIC_FRAMES=1
26+
27+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
28+
EXTERNAL_SAT_SOLVER=
29+
CBMCFLAGS=--smt2
30+
31+
FUNCTION_NAME = mlk_invntt_layer6
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# This function is large enough to need...
40+
CBMC_OBJECT_BITS = 10
41+
42+
# If you require access to a file-local ("static") function or object to conduct
43+
# your proof, set the following (and do not include the original source file
44+
# ("mlkem/poly.c") in PROJECT_SOURCES).
45+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
46+
# include ../Makefile.common
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
49+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
50+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
51+
# be set before including Makefile.common, but any use of variables on the
52+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
53+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
54+
55+
include ../Makefile.common

‎proofs/cbmc/invntt_layer6/mlk_invntt_layer6_harness.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// Copyright (c) 2024-2025 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
#include <poly.h>
6+
7+
#define invntt_layer6 MLK_NAMESPACE(invntt_layer6)
8+
void invntt_layer6(int16_t *r);
9+
10+
/**
11+
* @brief Starting point for formal analysis
12+
*
13+
*/
14+
void harness(void)
15+
{
16+
int16_t *a;
17+
invntt_layer6(a);
18+
}

‎proofs/cbmc/invntt_layer7_invert/Makefile

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = mlk_invntt_layer7_invert_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = mlk_invntt_layer7_invert
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.inc
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
21+
22+
CHECK_FUNCTION_CONTRACTS=mlk_invntt_layer7_invert
23+
USE_FUNCTION_CONTRACTS=mlk_fqmul mlk_barrett_reduce
24+
APPLY_LOOP_CONTRACTS=on
25+
USE_DYNAMIC_FRAMES=1
26+
27+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
28+
EXTERNAL_SAT_SOLVER=
29+
CBMCFLAGS=--smt2
30+
31+
FUNCTION_NAME = mlk_invntt_layer7_invert
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# This function is large enough to need...
40+
CBMC_OBJECT_BITS = 10
41+
42+
# If you require access to a file-local ("static") function or object to conduct
43+
# your proof, set the following (and do not include the original source file
44+
# ("mlkem/poly.c") in PROJECT_SOURCES).
45+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
46+
# include ../Makefile.common
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
49+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
50+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
51+
# be set before including Makefile.common, but any use of variables on the
52+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
53+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
54+
55+
include ../Makefile.common

‎proofs/cbmc/invntt_layer7_invert/mlk_invntt_layer7_invert_harness.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// Copyright (c) 2024-2025 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
#include <poly.h>
6+
7+
void mlk_invntt_layer7_invert(int16_t *r);
8+
9+
/**
10+
* @brief Starting point for formal analysis
11+
*
12+
*/
13+
void harness(void)
14+
{
15+
int16_t *a;
16+
mlk_invntt_layer7_invert(a);
17+
}

‎proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c

Lines changed: 0 additions & 18 deletions
This file was deleted.

0 commit comments

Comments
 (0)