Skip to content

Commit e4d1431

Browse files
mkannwischermkannwischer
authored
Merge pull request #1028 from pq-code-package/cbmc_basemul_aarch64
CBMC: Prove AArch64 native API for basemul atop HOL-Light spec
2 parents d3a4f76 + 610ceb0 commit e4d1431

File tree

13 files changed

+351
-42
lines changed

13 files changed

+351
-42
lines changed

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 36 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,21 +54,54 @@ void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a);
5454
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
5555
const int16_t *a,
5656
const int16_t *b,
57-
const int16_t *b_cache);
57+
const int16_t *b_cache)
58+
/* This must be kept in sync with the HOL-Light specification in
59+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
60+
*/
61+
__contract__(
62+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
63+
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
64+
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
65+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
66+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
67+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
68+
);
5869

5970
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
6071
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
6172
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
6273
const int16_t *a,
6374
const int16_t *b,
64-
const int16_t *b_cache);
75+
const int16_t *b_cache)
76+
/* This must be kept in sync with the HOL-Light specification in
77+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
78+
*/
79+
__contract__(
80+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
81+
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
82+
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
83+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
84+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
85+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
86+
);
6587

6688
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
6789
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
6890
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
6991
const int16_t *a,
7092
const int16_t *b,
71-
const int16_t *b_cache);
93+
const int16_t *b_cache)
94+
/* This must be kept in sync with the HOL-Light specification in
95+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
96+
*/
97+
__contract__(
98+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
99+
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
100+
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
101+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
102+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
103+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
104+
);
72105

73106
#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
74107
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 36 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,21 +54,54 @@ void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a);
5454
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
5555
const int16_t *a,
5656
const int16_t *b,
57-
const int16_t *b_cache);
57+
const int16_t *b_cache)
58+
/* This must be kept in sync with the HOL-Light specification in
59+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
60+
*/
61+
__contract__(
62+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
63+
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
64+
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
65+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
66+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
67+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
68+
);
5869

5970
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
6071
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
6172
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
6273
const int16_t *a,
6374
const int16_t *b,
64-
const int16_t *b_cache);
75+
const int16_t *b_cache)
76+
/* This must be kept in sync with the HOL-Light specification in
77+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
78+
*/
79+
__contract__(
80+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
81+
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
82+
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
83+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
84+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
85+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
86+
);
6587

6688
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
6789
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
6890
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
6991
const int16_t *a,
7092
const int16_t *b,
71-
const int16_t *b_cache);
93+
const int16_t *b_cache)
94+
/* This must be kept in sync with the HOL-Light specification in
95+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
96+
*/
97+
__contract__(
98+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
99+
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
100+
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
101+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
102+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
103+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
104+
);
72105

73106
#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
74107
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,

‎mlkem/native/aarch64/src/arith_native_aarch64.h‎

Lines changed: 36 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,21 +54,54 @@ void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a);
5454
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r,
5555
const int16_t *a,
5656
const int16_t *b,
57-
const int16_t *b_cache);
57+
const int16_t *b_cache)
58+
/* This must be kept in sync with the HOL-Light specification in
59+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
60+
*/
61+
__contract__(
62+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
63+
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
64+
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
65+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
66+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
67+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
68+
);
5869

5970
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
6071
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3)
6172
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r,
6273
const int16_t *a,
6374
const int16_t *b,
64-
const int16_t *b_cache);
75+
const int16_t *b_cache)
76+
/* This must be kept in sync with the HOL-Light specification in
77+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
78+
*/
79+
__contract__(
80+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
81+
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
82+
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
83+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
84+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
85+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
86+
);
6587

6688
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
6789
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4)
6890
void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r,
6991
const int16_t *a,
7092
const int16_t *b,
71-
const int16_t *b_cache);
93+
const int16_t *b_cache)
94+
/* This must be kept in sync with the HOL-Light specification in
95+
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
96+
*/
97+
__contract__(
98+
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
99+
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
100+
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
101+
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
102+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
103+
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
104+
);
72105

73106
#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
74107
uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen,

‎mlkem/native/api.h‎

Lines changed: 3 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -242,17 +242,7 @@ __contract__(
242242
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
243243
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
244244
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
245-
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
246-
* just use a single flattened array_bound(...) here.
247-
*
248-
* Once fixed, change to:
249-
* ```
250-
* requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
251-
* ```
252-
*/
253-
requires(forall(kN, 0, 2, \
254-
array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
255-
0, MLKEM_UINT12_LIMIT)))
245+
requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
256246
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
257247
);
258248
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 2 */
@@ -285,17 +275,7 @@ __contract__(
285275
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
286276
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
287277
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
288-
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
289-
* just use a single flattened array_bound(...) here.
290-
*
291-
* Once fixed, change to:
292-
* ```
293-
* requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
294-
* ```
295-
*/
296-
requires(forall(kN, 0, 3, \
297-
array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
298-
0, MLKEM_UINT12_LIMIT)))
278+
requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
299279
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
300280
);
301281
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 3 */
@@ -328,17 +308,7 @@ __contract__(
328308
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
329309
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
330310
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
331-
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
332-
* just use a single flattened array_bound(...) here.
333-
*
334-
* Once fixed, change to:
335-
* ```
336-
* requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
337-
* ```
338-
*/
339-
requires(forall(kN, 0, 4, \
340-
array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
341-
0, MLKEM_UINT12_LIMIT)))
311+
requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
342312
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
343313
);
344314
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 4 */

‎proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64/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 = polyvec_basemul_acc_montgomery_cached_k2_native_aarch64_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 = polyvec_basemul_acc_montgomery_cached_k2_native_aarch64
12+
13+
# We need to set MLK_CHECK_APIS as otherwise mlkem/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/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c
23+
24+
CHECK_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_k2_native
25+
USE_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_asm_k2
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 = polyvec_basemul_acc_montgomery_cached_k2_native_aarch64
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/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/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/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64/polyvec_basemul_acc_montgomery_cached_k2_native_aarch64_harness.c‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
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+
7+
#include "cbmc.h"
8+
#include "common.h"
9+
10+
void mlk_polyvec_basemul_acc_montgomery_cached_k2_native(
11+
int16_t r[MLKEM_N], const int16_t a[2 * MLKEM_N],
12+
const int16_t b[2 * MLKEM_N], const int16_t b_cache[2 * (MLKEM_N / 2)]);
13+
14+
void harness(void)
15+
{
16+
int16_t *r;
17+
const int16_t *a;
18+
const int16_t *b;
19+
const int16_t *b_cache;
20+
mlk_polyvec_basemul_acc_montgomery_cached_k2_native(r, a, b, b_cache);
21+
}

‎proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64/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 = polyvec_basemul_acc_montgomery_cached_k3_native_aarch64_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 = polyvec_basemul_acc_montgomery_cached_k3_native_aarch64
12+
13+
# We need to set MLK_CHECK_APIS as otherwise mlkem/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/native/aarch64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL_WITH_SHARED
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c
23+
24+
CHECK_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_k3_native
25+
USE_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_asm_k3
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 = polyvec_basemul_acc_montgomery_cached_k3_native_aarch64
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/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/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/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64/polyvec_basemul_acc_montgomery_cached_k3_native_aarch64_harness.c‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
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+
7+
#include "cbmc.h"
8+
#include "common.h"
9+
10+
void mlk_polyvec_basemul_acc_montgomery_cached_k3_native(
11+
int16_t r[MLKEM_N], const int16_t a[3 * MLKEM_N],
12+
const int16_t b[3 * MLKEM_N], const int16_t b_cache[3 * (MLKEM_N / 2)]);
13+
14+
void harness(void)
15+
{
16+
int16_t *r;
17+
const int16_t *a;
18+
const int16_t *b;
19+
const int16_t *b_cache;
20+
mlk_polyvec_basemul_acc_montgomery_cached_k3_native(r, a, b, b_cache);
21+
}

0 commit comments

Comments
 (0)