Skip to content

Commit 094b907

Browse files
willieyzmkannwischer
willieyz
authored and
mkannwischer
committed
CBMC/AArch64: Port native Keccak F1600 CBMC proofs
This commit adds the CBMC proofs for the native AArch64 Keccak routines from mlkem-native. This shows that the native contracts fulfills our API contracts. Signed-off-by: willieyz <willie.zhao@chelpis.com>
1 parent b8e62a0 commit 094b907

10 files changed

Lines changed: 350 additions & 0 deletions

File tree

‎proofs/cbmc/keccak_f1600_x1_native_aarch64/Makefile‎

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

‎proofs/cbmc/keccak_f1600_x1_native_aarch64/keccak_f1600_x1_native_aarch64_harness.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright (c) The mldsa-native project authors
3+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4+
// SPDX-License-Identifier: MIT-0
5+
6+
#include <stdint.h>
7+
8+
int mld_keccak_f1600_x1_native(uint64_t *state);
9+
10+
void harness(void)
11+
{
12+
uint64_t *s;
13+
int t = mld_keccak_f1600_x1_native(s);
14+
}

‎proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/Makefile‎

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

‎proofs/cbmc/keccak_f1600_x1_native_aarch64_v84a/keccak_f1600_x1_native_aarch64_v84a_harness.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright (c) The mldsa-native project authors
3+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4+
// SPDX-License-Identifier: MIT-0
5+
6+
#include <stdint.h>
7+
8+
int mld_keccak_f1600_x1_native(uint64_t *state);
9+
10+
void harness(void)
11+
{
12+
uint64_t *s;
13+
int t = mld_keccak_f1600_x1_native(s);
14+
}

‎proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/Makefile‎

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

‎proofs/cbmc/keccak_f1600_x4_native_aarch64_v84a/keccak_f1600_x4_native_aarch64_v84a_harness.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright (c) The mldsa-native project authors
3+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4+
// SPDX-License-Identifier: MIT-0
5+
6+
#include <stdint.h>
7+
8+
int mld_keccak_f1600_x4_native(uint64_t *state);
9+
10+
void harness(void)
11+
{
12+
uint64_t *s;
13+
int t = mld_keccak_f1600_x4_native(s);
14+
}

‎proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/Makefile‎

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

‎proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid/keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid_harness.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright (c) The mldsa-native project authors
3+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4+
// SPDX-License-Identifier: MIT-0
5+
6+
#include <stdint.h>
7+
8+
int mld_keccak_f1600_x4_native(uint64_t *state);
9+
10+
void harness(void)
11+
{
12+
uint64_t *s;
13+
int t = mld_keccak_f1600_x4_native(s);
14+
}

‎proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid/Makefile‎

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

‎proofs/cbmc/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid/keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid_harness.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright (c) The mldsa-native project authors
3+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4+
// SPDX-License-Identifier: MIT-0
5+
6+
#include <stdint.h>
7+
8+
int mld_keccak_f1600_x4_native(uint64_t *state);
9+
10+
void harness(void)
11+
{
12+
uint64_t *s;
13+
int t = mld_keccak_f1600_x4_native(s);
14+
}

0 commit comments

Comments
 (0)