Skip to content

Commit 387f6fd

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]>
1 parent 366156b commit 387f6fd

31 files changed

+1135
-194
lines changed

‎mlkem/poly.c

Lines changed: 543 additions & 147 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 = 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 = 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.c
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
21+
22+
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer321
23+
USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)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_NAMESPACE)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/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

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

Lines changed: 8 additions & 6 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

8-
#define invntt_layer MLK_NAMESPACE(invntt_layer)
9-
void invntt_layer(int16_t *p, unsigned len, unsigned layer);
7+
#define invntt_layer321 MLK_NAMESPACE(invntt_layer321)
8+
void invntt_layer321(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 len, layer;
15-
invntt_layer(a, len, layer);
17+
invntt_layer321(a);
1618
}

‎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 = 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 = 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_NAMESPACE)invntt_layer54
22+
USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer54_butterfly
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_NAMESPACE)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_layer54/invntt_layer54_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_layer54 MLK_NAMESPACE(invntt_layer54)
8+
void invntt_layer54(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_layer54(a);
18+
}

‎proofs/cbmc/invntt_layer54_butterfly/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 = invntt_layer54_butterfly_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 = invntt_layer54_butterfly
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.c
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
21+
22+
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer54_butterfly
23+
USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul $(MLK_NAMESPACE)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_NAMESPACE)invntt_layer54_butterfly
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_butterfly/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎proofs/cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
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_layer54_butterfly MLK_NAMESPACE(invntt_layer54_butterfly)
8+
void invntt_layer54_butterfly(int16_t r[MLKEM_N], const unsigned zeta_index,
9+
const unsigned start);
10+
11+
/**
12+
* @brief Starting point for formal analysis
13+
*
14+
*/
15+
void harness(void)
16+
{
17+
int16_t *a;
18+
unsigned zi;
19+
unsigned start;
20+
invntt_layer54_butterfly(a, zi, start);
21+
}

‎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 = 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 = 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.c
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
21+
22+
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer6
23+
USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)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_NAMESPACE)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/cbmc-proof.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
# This file marks this directory as containing a CBMC proof.

‎proofs/cbmc/invntt_layer6/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_layer/Makefile renamed to ‎proofs/cbmc/invntt_layer7_invert/Makefile

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@
33
include ../Makefile_params.common
44

55
HARNESS_ENTRY = harness
6-
HARNESS_FILE = invntt_layer_harness
6+
HARNESS_FILE = invntt_layer7_invert_harness
77

88
# This should be a unique identifier for this proof, and will appear on the
99
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10-
PROOF_UID = invntt_layer
10+
PROOF_UID = invntt_layer7_invert
1111

1212
DEFINES +=
1313
INCLUDES +=
@@ -16,9 +16,10 @@ REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=
1717

1818
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/zetas.c
1920
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
2021

21-
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer
22+
CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)invntt_layer7_invert
2223
USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)fqmul $(MLK_NAMESPACE)barrett_reduce
2324
APPLY_LOOP_CONTRACTS=on
2425
USE_DYNAMIC_FRAMES=1
@@ -27,7 +28,7 @@ USE_DYNAMIC_FRAMES=1
2728
EXTERNAL_SAT_SOLVER=
2829
CBMCFLAGS=--smt2
2930

30-
FUNCTION_NAME = invntt_layer
31+
FUNCTION_NAME = invntt_layer7_invert
3132

3233
# If this proof is found to consume huge amounts of RAM, you can set the
3334
# EXPENSIVE variable. With new enough versions of the proof tools, this will

‎proofs/cbmc/invntt_layer7_invert/invntt_layer7_invert_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_layer7_invert MLK_NAMESPACE(invntt_layer7_invert)
8+
void invntt_layer7_invert(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_layer7_invert(a);
18+
}

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