Skip to content

Commit 040738d

Browse files
rod-chapmanhanno-becker
rod-chapman
authored and
hanno-becker
committed
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]>
1 parent 2fcb52e commit 040738d

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

62 files changed

+2015
-310
lines changed

‎cbmc/Makefile.common

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -949,6 +949,7 @@ result:
949949
$(MAKE) -B _result
950950
@ echo Running 'litani build'
951951
$(LITANI) run-build
952+
tail -4 $(LOGDIR)/result.txt
952953

953954
_property: $(LOGDIR)/property.xml
954955
property:

‎cbmc/basemul_cached/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=
1717

1818
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19-
PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
2020

21-
CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)basemul_cached
21+
CHECK_FUNCTION_CONTRACTS=basemul_cached
2222
USE_FUNCTION_CONTRACTS=montgomery_reduce
2323
APPLY_LOOP_CONTRACTS=on
2424
USE_DYNAMIC_FRAMES=1

‎cbmc/basemul_cached/basemul_cached_harness.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,9 @@
66
#include "ntt.h"
77
#include "reduce.h"
88

9+
void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2],
10+
const int16_t b_cached);
11+
912
void harness(void)
1013
{
1114
int16_t *a, *b, *r, b_cached;

‎cbmc/invntt_layer/invntt_layer_harness.c

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

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

Lines changed: 6 additions & 6 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 = ntt_butterfly_block_harness
6+
HARNESS_FILE = invntt_layer321_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 = ntt_butterfly_block
10+
PROOF_UID = invntt_layer321
1111

1212
DEFINES +=
1313
INCLUDES +=
@@ -18,16 +18,16 @@ UNWINDSET +=
1818
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
1919
PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
2020

21-
CHECK_FUNCTION_CONTRACTS=ntt_butterfly_block
22-
USE_FUNCTION_CONTRACTS= fqmul
21+
CHECK_FUNCTION_CONTRACTS=invntt_layer321
22+
USE_FUNCTION_CONTRACTS=fqmul
2323
APPLY_LOOP_CONTRACTS=on
2424
USE_DYNAMIC_FRAMES=1
2525

2626
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2727
EXTERNAL_SAT_SOLVER=
2828
CBMCFLAGS=--bitwuzla
2929

30-
FUNCTION_NAME = ntt_butterfly_block
30+
FUNCTION_NAME = invntt_layer321
3131

3232
# If this proof is found to consume huge amounts of RAM, you can set the
3333
# EXPENSIVE variable. With new enough versions of the proof tools, this will
@@ -36,7 +36,7 @@ FUNCTION_NAME = ntt_butterfly_block
3636
# EXPENSIVE = true
3737

3838
# This function is large enough to need...
39-
CBMC_OBJECT_BITS = 9
39+
CBMC_OBJECT_BITS = 10
4040

4141
# If you require access to a file-local ("static") function or object to conduct
4242
# 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

File renamed without changes.

‎cbmc/invntt_layer321/invntt_layer321_harness.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// Copyright (c) 2024 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
/*
6+
* Insert copyright notice
7+
*/
8+
9+
/**
10+
* @file invntt_layer321_harness.c
11+
* @brief Implements the proof harness for invntt_layer321 function.
12+
*/
13+
14+
/*
15+
* Insert project header files that
16+
* - include the declaration of the function
17+
* - include the types needed to declare function arguments
18+
*/
19+
#include <ntt.h>
20+
void invntt_layer321(int16_t *r);
21+
22+
/**
23+
* @brief Starting point for formal analysis
24+
*
25+
*/
26+
void harness(void)
27+
{
28+
int16_t *a;
29+
invntt_layer321(a);
30+
}

‎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/ntt.c
20+
21+
CHECK_FUNCTION_CONTRACTS=invntt_layer54
22+
USE_FUNCTION_CONTRACTS=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 = 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

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

File renamed without changes.

‎cbmc/invntt_layer54/invntt_layer54_harness.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// Copyright (c) 2024 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
/*
6+
* Insert copyright notice
7+
*/
8+
9+
/**
10+
* @file invntt_layer54_harness.c
11+
* @brief Implements the proof harness for invntt_layer54 function.
12+
*/
13+
14+
/*
15+
* Insert project header files that
16+
* - include the declaration of the function
17+
* - include the types needed to declare function arguments
18+
*/
19+
#include <ntt.h>
20+
void invntt_layer54(int16_t *r);
21+
22+
/**
23+
* @brief Starting point for formal analysis
24+
*
25+
*/
26+
void harness(void)
27+
{
28+
int16_t *a;
29+
invntt_layer54(a);
30+
}

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

Lines changed: 6 additions & 6 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_layer54_butterfly_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_layer54_butterfly
1111

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

1818
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19-
PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c $(SRCDIR)/mlkem/zetas.c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/ntt.c
2020

21-
CHECK_FUNCTION_CONTRACTS=invntt_layer
21+
CHECK_FUNCTION_CONTRACTS=invntt_layer54_butterfly
2222
USE_FUNCTION_CONTRACTS=fqmul barrett_reduce
2323
APPLY_LOOP_CONTRACTS=on
2424
USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
2727
EXTERNAL_SAT_SOLVER=
2828
CBMCFLAGS=--smt2
2929

30-
FUNCTION_NAME = invntt_layer
30+
FUNCTION_NAME = invntt_layer54_butterfly
3131

3232
# If this proof is found to consume huge amounts of RAM, you can set the
3333
# EXPENSIVE variable. With new enough versions of the proof tools, this will
@@ -36,7 +36,7 @@ FUNCTION_NAME = invntt_layer
3636
# EXPENSIVE = true
3737

3838
# This function is large enough to need...
39-
CBMC_OBJECT_BITS = 8
39+
CBMC_OBJECT_BITS = 10
4040

4141
# If you require access to a file-local ("static") function or object to conduct
4242
# your proof, set the following (and do not include the original source file

‎cbmc/ntt_layer/cbmc-proof.txt renamed to ‎cbmc/invntt_layer54_butterfly/cbmc-proof.txt

File renamed without changes.

‎cbmc/invntt_layer54_butterfly/invntt_layer54_butterfly_harness.c

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
// Copyright (c) 2024 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
/*
6+
* Insert copyright notice
7+
*/
8+
9+
/**
10+
* @file invntt_layer54_butterfly_harness.c
11+
* @brief Implements the proof harness for invntt_layer54_butterfly function.
12+
*/
13+
14+
/*
15+
* Insert project header files that
16+
* - include the declaration of the function
17+
* - include the types needed to declare function arguments
18+
*/
19+
#include <ntt.h>
20+
void invntt_layer54_butterfly(int16_t *r, int zeta_index, int start);
21+
22+
/**
23+
* @brief Starting point for formal analysis
24+
*
25+
*/
26+
void harness(void)
27+
{
28+
int16_t *a;
29+
int zi;
30+
int start;
31+
invntt_layer54_butterfly(a, zi, start);
32+
}

‎cbmc/invntt_layer6/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_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/ntt.c
20+
21+
CHECK_FUNCTION_CONTRACTS=invntt_layer6
22+
USE_FUNCTION_CONTRACTS=invntt_layer6_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 = invntt_layer6
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

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

‎cbmc/invntt_layer6/invntt_layer6_harness.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// Copyright (c) 2024 The mlkem-native project authors
2+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
// SPDX-License-Identifier: MIT-0
4+
5+
/*
6+
* Insert copyright notice
7+
*/
8+
9+
/**
10+
* @file invntt_layer6_harness.c
11+
* @brief Implements the proof harness for invntt_layer6 function.
12+
*/
13+
14+
/*
15+
* Insert project header files that
16+
* - include the declaration of the function
17+
* - include the types needed to declare function arguments
18+
*/
19+
#include <ntt.h>
20+
void invntt_layer6(int16_t *r);
21+
22+
/**
23+
* @brief Starting point for formal analysis
24+
*
25+
*/
26+
void harness(void)
27+
{
28+
int16_t *a;
29+
invntt_layer6(a);
30+
}

0 commit comments

Comments
 (0)