Skip to content

Commit 227195e

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #803 from pq-code-package/contract_checker
CBMC: Add contract checker
2 parents 4010407 + 4f863ce commit 227195e

File tree

17 files changed

+579
-5
lines changed

17 files changed

+579
-5
lines changed

‎mlkem/verify.h

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -56,16 +56,26 @@
5656
#define mlk_ct_opt_blocker_u64 MLK_NAMESPACE(ct_opt_blocker_u64)
5757
extern volatile uint64_t mlk_ct_opt_blocker_u64;
5858

59-
/* Helper functions for obtaining masks of various sizes */
59+
/* Helper functions for obtaining global masks of various sizes */
60+
61+
/* This contract is not proved but treated as an axiom.
62+
*
63+
* Its validity relies on the assumption that the global opt-blocker
64+
* constant mlk_ct_opt_blocker_u64 is not modified.
65+
*/
66+
static MLK_INLINE uint64_t mlk_ct_get_optblocker_u64(void)
67+
__contract__(ensures(return_value == 0)) { return mlk_ct_opt_blocker_u64; }
68+
6069
static MLK_INLINE uint8_t mlk_ct_get_optblocker_u8(void)
61-
__contract__(ensures(return_value == 0)) { return (uint8_t)mlk_ct_opt_blocker_u64; }
70+
__contract__(ensures(return_value == 0)) { return (uint8_t)mlk_ct_get_optblocker_u64(); }
6271

6372
static MLK_INLINE uint32_t mlk_ct_get_optblocker_u32(void)
64-
__contract__(ensures(return_value == 0)) { return mlk_ct_opt_blocker_u64; }
73+
__contract__(ensures(return_value == 0)) { return (uint32_t)mlk_ct_get_optblocker_u64(); }
6574

66-
static MLK_INLINE uint32_t mlk_ct_get_optblocker_i32(void)
67-
__contract__(ensures(return_value == 0)) { return mlk_ct_opt_blocker_u64; }
75+
static MLK_INLINE int32_t mlk_ct_get_optblocker_i32(void)
76+
__contract__(ensures(return_value == 0)) { return (int32_t)mlk_ct_get_optblocker_u64(); }
6877

78+
/* Opt-blocker based implementation of value barriers */
6979
static MLK_INLINE uint32_t mlk_value_barrier_u32(uint32_t b)
7080
__contract__(ensures(return_value == b)) { return (b ^ mlk_ct_get_optblocker_u32()); }
7181

‎proofs/cbmc/ct_get_optblocker_i32/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 = ct_get_optblocker_i32_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_ct_get_optblocker_i32
11+
12+
DEFINES += -DMLK_NO_ASM_VALUE_BARRIER
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
20+
21+
CHECK_FUNCTION_CONTRACTS=mlk_ct_get_optblocker_i32
22+
USE_FUNCTION_CONTRACTS=mlk_ct_get_optblocker_u64
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=--bitwuzla
29+
30+
FUNCTION_NAME = mlk_ct_get_optblocker_i32
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 = 8
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/ct_get_optblocker_i32/ct_get_optblocker_i32_harness.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
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 AND Apache-2.0
4+
5+
#include "verify.h"
6+
7+
void harness(void) { int32_t x = mlk_ct_get_optblocker_i32(); }

‎proofs/cbmc/ct_get_optblocker_u32/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 = ct_get_optblocker_u32_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_ct_get_optblocker_u32
11+
12+
DEFINES += -DMLK_NO_ASM_VALUE_BARRIER
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
20+
21+
CHECK_FUNCTION_CONTRACTS=mlk_ct_get_optblocker_u32
22+
USE_FUNCTION_CONTRACTS=mlk_ct_get_optblocker_u64
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=--bitwuzla
29+
30+
FUNCTION_NAME = mlk_ct_get_optblocker_u32
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 = 8
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/ct_get_optblocker_u32/ct_get_optblocker_u32_harness.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
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 AND Apache-2.0
4+
5+
#include "verify.h"
6+
7+
void harness(void) { uint32_t x = mlk_ct_get_optblocker_u32(); }

‎proofs/cbmc/ct_get_optblocker_u8/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 = ct_get_optblocker_u8_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_ct_get_optblocker_u8
11+
12+
DEFINES += -DMLK_NO_ASM_VALUE_BARRIER
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
20+
21+
CHECK_FUNCTION_CONTRACTS=mlk_ct_get_optblocker_u8
22+
USE_FUNCTION_CONTRACTS=mlk_ct_get_optblocker_u64
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=--bitwuzla
29+
30+
FUNCTION_NAME = mlk_ct_get_optblocker_u8
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 = 8
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/ct_get_optblocker_u8/ct_get_optblocker_u8_harness.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
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 AND Apache-2.0
4+
5+
#include "verify.h"
6+
7+
void harness(void) { uint8_t x = mlk_ct_get_optblocker_u8(); }

‎proofs/cbmc/poly_permute_bitrev_to_custom/Makefile

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = poly_permute_bitrev_to_custom_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_poly_permute_bitrev_to_custom
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
17+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
18+
PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c
19+
20+
CHECK_FUNCTION_CONTRACTS=mlk_poly_permute_bitrev_to_custom
21+
USE_FUNCTION_CONTRACTS=
22+
APPLY_LOOP_CONTRACTS=on
23+
USE_DYNAMIC_FRAMES=1
24+
25+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
26+
EXTERNAL_SAT_SOLVER=
27+
CBMCFLAGS=--smt2
28+
29+
# For this proof we tell CBMC to
30+
# 1. not decompose arrays into their individual cells
31+
# 2. to model arrays directly as SMT-lib arrays
32+
# 3. to slice constraints that are not in the cone of influence of the proof obligations
33+
# These options simplify them modelling of arrays and produce much more compact
34+
# SMT files, leaving all array-type reasoning to the SMT solver.
35+
#
36+
# For functions that use large and multi-dimensional arrays, this yields
37+
# a substantial improvement in proof performance.
38+
CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
39+
40+
FUNCTION_NAME = mlk_poly_permute_bitrev_to_custom
41+
42+
# If this proof is found to consume huge amounts of RAM, you can set the
43+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
44+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
45+
# documentation in Makefile.common under the "Job Pools" heading for details.
46+
# EXPENSIVE = true
47+
48+
# This function is large enough to need...
49+
CBMC_OBJECT_BITS = 8
50+
51+
# If you require access to a file-local ("static") function or object to conduct
52+
# your proof, set the following (and do not include the original source file
53+
# ("mlkem/poly.c") in PROJECT_SOURCES).
54+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
55+
# include ../Makefile.common
56+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
57+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
58+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
59+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
60+
# be set before including Makefile.common, but any use of variables on the
61+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
62+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
63+
64+
include ../Makefile.common

‎proofs/cbmc/poly_permute_bitrev_to_custom/poly_permute_bitrev_to_custom_harness.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
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 <stdint.h>
6+
#include "params.h"
7+
8+
void mlk_poly_permute_bitrev_to_custom(int16_t data[MLKEM_N]);
9+
10+
void harness(void)
11+
{
12+
int16_t data[MLKEM_N];
13+
mlk_poly_permute_bitrev_to_custom(data);
14+
}

‎proofs/cbmc/value_barrier_i32/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 = value_barrier_i32_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_value_barrier_i32
11+
12+
DEFINES += -DMLK_NO_ASM_VALUE_BARRIER
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_value_barrier_i32
22+
USE_FUNCTION_CONTRACTS=mlk_ct_get_optblocker_i32
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=--bitwuzla
29+
30+
FUNCTION_NAME = mlk_value_barrier_i32
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 = 8
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/value_barrier_i32/value_barrier_i32_harness.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
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 AND Apache-2.0
4+
5+
#include "verify.h"
6+
7+
void harness(void)
8+
{
9+
int32_t x, y;
10+
y = mlk_value_barrier_i32(x);
11+
}

0 commit comments

Comments
 (0)