Skip to content

Commit 2d3d8be

Browse files
willieyzwillieyz
committed
CBMC: Add x86-64 HOL-Light-based contracts and proofs
- This commit introduces CBMC verification for several x86-64 optimized assembly functions. The contracts for these functions are derived from their corresponding HOL-Light correctness proofs. - For each assembly function, a CBMC contract has been added to `arith_native_x86_64.h`. Additionally, new proof harnesses have been creat to formally verify that the generic C implementations (`*_native`) correctly utilize these assembly backends and adhere to the top-level API contracts. - The following functions now have CBMC proofs based on their HOL-Light specifications: - polyvec_basemul_acc_montgomery_cached_asm_k2/k3/k4: - Pre-conditions: `<= &2 pow 12`(HOL_LIGHT) v.s. `MLKEM_UINT12_LIMIT + 1`(CBMC) - Adds a CBMC pre-condition: `requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT +` `1))` - ntt_avx2: - Pre-condition: `<= &8191`(HOL_LIGHT) v.s. `8191 + 1`(CBMC) - Post-condition: `<= &23594`(HOL_LIGHT) v.s. `23594 + 1`(CBMC) - Adds a CBMC pre-condition: `requires(array_abs_bound(r, 0, MLKEM_N, 8192))` - Adds a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 23595))` - intt_avx2: - Post-condition: `<= &26631` v.s. `26631 + 1`(CBMC) - Adds a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 26632))` - reduce_avx2: - Post-condition: `< &3329`(HOL_LIGHT) v.s. `3329 == MLKEM_Q`(CBMC) - Adds a CBMC post-condition: `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` - tobytes_avx2: - Pre-condition: `num_of_wordlist (MAP word_zx l:(12 word)list))`(HOL_LIGHT) v.s. `MLKEM_UINT12_LIMIT`(CBMC) - Adds a CBMC post-condition: `requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))` Signed-off-by: willieyz <willie.zhao@chelpis.com>
1 parent 90f9862 commit 2d3d8be

File tree

17 files changed

+679
-17
lines changed

17 files changed

+679
-17
lines changed

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 74 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77

88
#include "../../../common.h"
99

10-
#include <immintrin.h>
1110
#include <stdint.h>
1211
#include "consts.h"
1312

@@ -22,16 +21,44 @@ uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
2221
extern const uint8_t mlk_rej_uniform_table[];
2322

2423
#define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2)
25-
void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata);
24+
void mlk_ntt_avx2(int16_t *r, const int16_t *qdata)
25+
/* This must be kept in sync with the HOL-Light specification
26+
* in proofs/hol_light/x86/proofs/mlkem_ntt.ml */
27+
__contract__(
28+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
29+
requires(array_abs_bound(r, 0, MLKEM_N, 8192))
30+
requires(qdata == mlk_qdata)
31+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
32+
/* check-magic: off */
33+
ensures(array_abs_bound(r, 0, MLKEM_N, 23595))
34+
/* check-magic: on */
35+
);
2636

2737
#define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2)
28-
void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata);
38+
void mlk_invntt_avx2(int16_t *r, const int16_t *qdata)
39+
/* This must be kept in sync with the HOL-Light specification
40+
* in proofs/hol_light/x86/proofs/mlkem_intt.ml */
41+
__contract__(
42+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
43+
requires(qdata == mlk_qdata)
44+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
45+
/* check-magic: off */
46+
ensures(array_abs_bound(r, 0, MLKEM_N, 26632))
47+
/* check-magic: on */
48+
);
2949

3050
#define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2)
3151
void mlk_nttunpack_avx2(int16_t *r);
3252

3353
#define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2)
34-
void mlk_reduce_avx2(int16_t *r);
54+
void mlk_reduce_avx2(int16_t *r)
55+
/* This must be kept in sync with the HOL-Light specification
56+
* in proofs/hol_light/x86/proofs/mlkem_reduce.ml */
57+
__contract__(
58+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
59+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
60+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
61+
);
3562

3663
#define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
3764
void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
@@ -42,24 +69,63 @@ void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
4269
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
4370
const int16_t *a,
4471
const int16_t *b,
45-
const int16_t *b_cache);
72+
const int16_t *b_cache)
73+
/* This must be kept in sync with the HOL-Light specification in
74+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
75+
*/
76+
__contract__(
77+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
78+
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
79+
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
80+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
81+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
82+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
83+
);
4684

4785
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
4886
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
4987
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
5088
const int16_t *a,
5189
const int16_t *b,
52-
const int16_t *b_cache);
90+
const int16_t *b_cache)
91+
/* This must be kept in sync with the HOL-Light specification in
92+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
93+
*/
94+
__contract__(
95+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
96+
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
97+
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
98+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
99+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
100+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
101+
);
53102

54103
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
55104
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
56105
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
57106
const int16_t *a,
58107
const int16_t *b,
59-
const int16_t *b_cache);
108+
const int16_t *b_cache)
109+
/* This must be kept in sync with the HOL-Light specification in
110+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
111+
*/
112+
__contract__(
113+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
114+
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
115+
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
116+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
117+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
118+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
119+
);
60120

61121
#define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
62-
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a);
122+
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
123+
__contract__(
124+
requires(memory_no_alias(r, MLKEM_POLYBYTES))
125+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
126+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
127+
assigns(object_whole(r))
128+
);
63129

64130
#define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
65131
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);

‎mlkem/src/native/x86_64/src/arith_native_x86_64.h‎

Lines changed: 74 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77

88
#include "../../../common.h"
99

10-
#include <immintrin.h>
1110
#include <stdint.h>
1211
#include "consts.h"
1312

@@ -22,16 +21,44 @@ uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,
2221
extern const uint8_t mlk_rej_uniform_table[];
2322

2423
#define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2)
25-
void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata);
24+
void mlk_ntt_avx2(int16_t *r, const int16_t *qdata)
25+
/* This must be kept in sync with the HOL-Light specification
26+
* in proofs/hol_light/x86/proofs/mlkem_ntt.ml */
27+
__contract__(
28+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
29+
requires(array_abs_bound(r, 0, MLKEM_N, 8192))
30+
requires(qdata == mlk_qdata)
31+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
32+
/* check-magic: off */
33+
ensures(array_abs_bound(r, 0, MLKEM_N, 23595))
34+
/* check-magic: on */
35+
);
2636

2737
#define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2)
28-
void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata);
38+
void mlk_invntt_avx2(int16_t *r, const int16_t *qdata)
39+
/* This must be kept in sync with the HOL-Light specification
40+
* in proofs/hol_light/x86/proofs/mlkem_intt.ml */
41+
__contract__(
42+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
43+
requires(qdata == mlk_qdata)
44+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
45+
/* check-magic: off */
46+
ensures(array_abs_bound(r, 0, MLKEM_N, 26632))
47+
/* check-magic: on */
48+
);
2949

3050
#define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2)
3151
void mlk_nttunpack_avx2(int16_t *r);
3252

3353
#define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2)
34-
void mlk_reduce_avx2(int16_t *r);
54+
void mlk_reduce_avx2(int16_t *r)
55+
/* This must be kept in sync with the HOL-Light specification
56+
* in proofs/hol_light/x86/proofs/mlkem_reduce.ml */
57+
__contract__(
58+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
59+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
60+
ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
61+
);
3562

3663
#define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2)
3764
void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
@@ -42,24 +69,63 @@ void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in,
4269
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
4370
const int16_t *a,
4471
const int16_t *b,
45-
const int16_t *b_cache);
72+
const int16_t *b_cache)
73+
/* This must be kept in sync with the HOL-Light specification in
74+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
75+
*/
76+
__contract__(
77+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
78+
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
79+
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
80+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
81+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
82+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
83+
);
4684

4785
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
4886
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
4987
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
5088
const int16_t *a,
5189
const int16_t *b,
52-
const int16_t *b_cache);
90+
const int16_t *b_cache)
91+
/* This must be kept in sync with the HOL-Light specification in
92+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
93+
*/
94+
__contract__(
95+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
96+
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
97+
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
98+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
99+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
100+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
101+
);
53102

54103
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
55104
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
56105
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
57106
const int16_t *a,
58107
const int16_t *b,
59-
const int16_t *b_cache);
108+
const int16_t *b_cache)
109+
/* This must be kept in sync with the HOL-Light specification in
110+
* proofs/hol_light/x86/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
111+
*/
112+
__contract__(
113+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
114+
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
115+
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
116+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
117+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
118+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
119+
);
60120

61121
#define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2)
62-
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a);
122+
void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a)
123+
__contract__(
124+
requires(memory_no_alias(r, MLKEM_POLYBYTES))
125+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
126+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
127+
assigns(object_whole(r))
128+
);
63129

64130
#define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2)
65131
void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);

‎proofs/cbmc/intt_native_x86_64/Makefile‎

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

‎proofs/cbmc/intt_native_x86_64/intt_native_x86_64_harness.c‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// Copyright (c) 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 "cbmc.h"
7+
#include "params.h"
8+
9+
int mlk_intt_native(int16_t data[MLKEM_N]);
10+
11+
void harness(void)
12+
{
13+
int16_t *r;
14+
int t;
15+
t = mlk_intt_native(r);
16+
}

‎proofs/cbmc/ntt_native_x86_64/Makefile‎

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

‎proofs/cbmc/ntt_native_x86_64/ntt_native_x86_64_harness.c‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// Copyright (c) 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 "cbmc.h"
7+
#include "params.h"
8+
9+
int mlk_ntt_native(int16_t data[MLKEM_N]);
10+
11+
void harness(void)
12+
{
13+
int16_t *r;
14+
int t;
15+
t = mlk_ntt_native(r);
16+
}

0 commit comments

Comments
 (0)