Skip to content

Commit 0843f3f

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #1029 from pq-code-package/cbmc-aarch64-poly
CBMC: Prove AArch64 native API for ntt, intt, poly_tobytes, poly_tomont atop HOL-Light spec
2 parents e4d1431 + 26d81ad commit 0843f3f

File tree

15 files changed

+434
-12
lines changed

15 files changed

+434
-12
lines changed

‎dev/aarch64_clean/src/arith_native_aarch64.h

Lines changed: 44 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,23 +31,63 @@ extern const int16_t mlk_aarch64_zetas_mulcache_twisted_native[];
3131
extern const uint8_t mlk_rej_uniform_table[];
3232

3333
#define mlk_ntt_asm MLK_NAMESPACE(ntt_asm)
34-
void mlk_ntt_asm(int16_t *, const int16_t *, const int16_t *);
34+
void mlk_ntt_asm(int16_t *p, const int16_t *twiddles12345,
35+
const int16_t *twiddles56)
36+
/* This must be kept in sync with the HOL-Light specification
37+
* in proofs/hol_light/arm/proofs/mlkem_ntt.ml */
38+
__contract__(
39+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
40+
requires(array_abs_bound(p, 0, MLKEM_N, 8192))
41+
requires(twiddles12345 == mlk_aarch64_ntt_zetas_layer12345)
42+
requires(twiddles56 == mlk_aarch64_ntt_zetas_layer67)
43+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
44+
/* check-magic: off */
45+
ensures(array_abs_bound(p, 0, MLKEM_N, 23595))
46+
/* check-magic: on */
47+
);
3548

3649
#define mlk_intt_asm MLK_NAMESPACE(intt_asm)
37-
void mlk_intt_asm(int16_t *, const int16_t *, const int16_t *);
50+
void mlk_intt_asm(int16_t *p, const int16_t *twiddles12345,
51+
const int16_t *twiddles56)
52+
/* This must be kept in sync with the HOL-Light specification
53+
* in proofs/hol_light/arm/proofs/mlkem_intt.ml */
54+
__contract__(
55+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
56+
requires(twiddles12345 == mlk_aarch64_invntt_zetas_layer12345)
57+
requires(twiddles56 == mlk_aarch64_invntt_zetas_layer67)
58+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
59+
/* check-magic: off */
60+
ensures(array_abs_bound(p, 0, MLKEM_N, 26625))
61+
/* check-magic: on */
62+
);
3863

3964
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
4065
void mlk_poly_reduce_asm(int16_t *);
4166

4267
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
43-
void mlk_poly_tomont_asm(int16_t *);
68+
void mlk_poly_tomont_asm(int16_t *p)
69+
/* This must be kept in sync with the HOL-Light specification
70+
* in proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml */
71+
__contract__(
72+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
73+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
74+
ensures(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q))
75+
);
4476

4577
#define mlk_poly_mulcache_compute_asm MLK_NAMESPACE(poly_mulcache_compute_asm)
4678
void mlk_poly_mulcache_compute_asm(int16_t *, const int16_t *, const int16_t *,
4779
const int16_t *);
4880

4981
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
50-
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a);
82+
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a)
83+
/* This must be kept in sync with the HOL-Light specification
84+
* in proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml */
85+
__contract__(
86+
requires(memory_no_alias(r, MLKEM_POLYBYTES))
87+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
88+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
89+
assigns(object_whole(r))
90+
);
5191

5292
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
5393
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)

‎dev/aarch64_opt/src/arith_native_aarch64.h

Lines changed: 44 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,23 +31,63 @@ extern const int16_t mlk_aarch64_zetas_mulcache_twisted_native[];
3131
extern const uint8_t mlk_rej_uniform_table[];
3232

3333
#define mlk_ntt_asm MLK_NAMESPACE(ntt_asm)
34-
void mlk_ntt_asm(int16_t *, const int16_t *, const int16_t *);
34+
void mlk_ntt_asm(int16_t *p, const int16_t *twiddles12345,
35+
const int16_t *twiddles56)
36+
/* This must be kept in sync with the HOL-Light specification
37+
* in proofs/hol_light/arm/proofs/mlkem_ntt.ml */
38+
__contract__(
39+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
40+
requires(array_abs_bound(p, 0, MLKEM_N, 8192))
41+
requires(twiddles12345 == mlk_aarch64_ntt_zetas_layer12345)
42+
requires(twiddles56 == mlk_aarch64_ntt_zetas_layer67)
43+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
44+
/* check-magic: off */
45+
ensures(array_abs_bound(p, 0, MLKEM_N, 23595))
46+
/* check-magic: on */
47+
);
3548

3649
#define mlk_intt_asm MLK_NAMESPACE(intt_asm)
37-
void mlk_intt_asm(int16_t *, const int16_t *, const int16_t *);
50+
void mlk_intt_asm(int16_t *p, const int16_t *twiddles12345,
51+
const int16_t *twiddles56)
52+
/* This must be kept in sync with the HOL-Light specification
53+
* in proofs/hol_light/arm/proofs/mlkem_intt.ml */
54+
__contract__(
55+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
56+
requires(twiddles12345 == mlk_aarch64_invntt_zetas_layer12345)
57+
requires(twiddles56 == mlk_aarch64_invntt_zetas_layer67)
58+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
59+
/* check-magic: off */
60+
ensures(array_abs_bound(p, 0, MLKEM_N, 26625))
61+
/* check-magic: on */
62+
);
3863

3964
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
4065
void mlk_poly_reduce_asm(int16_t *);
4166

4267
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
43-
void mlk_poly_tomont_asm(int16_t *);
68+
void mlk_poly_tomont_asm(int16_t *p)
69+
/* This must be kept in sync with the HOL-Light specification
70+
* in proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml */
71+
__contract__(
72+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
73+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
74+
ensures(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q))
75+
);
4476

4577
#define mlk_poly_mulcache_compute_asm MLK_NAMESPACE(poly_mulcache_compute_asm)
4678
void mlk_poly_mulcache_compute_asm(int16_t *, const int16_t *, const int16_t *,
4779
const int16_t *);
4880

4981
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
50-
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a);
82+
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a)
83+
/* This must be kept in sync with the HOL-Light specification
84+
* in proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml */
85+
__contract__(
86+
requires(memory_no_alias(r, MLKEM_POLYBYTES))
87+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
88+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
89+
assigns(object_whole(r))
90+
);
5191

5292
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
5393
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)

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

Lines changed: 44 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,23 +31,63 @@ extern const int16_t mlk_aarch64_zetas_mulcache_twisted_native[];
3131
extern const uint8_t mlk_rej_uniform_table[];
3232

3333
#define mlk_ntt_asm MLK_NAMESPACE(ntt_asm)
34-
void mlk_ntt_asm(int16_t *, const int16_t *, const int16_t *);
34+
void mlk_ntt_asm(int16_t *p, const int16_t *twiddles12345,
35+
const int16_t *twiddles56)
36+
/* This must be kept in sync with the HOL-Light specification
37+
* in proofs/hol_light/arm/proofs/mlkem_ntt.ml */
38+
__contract__(
39+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
40+
requires(array_abs_bound(p, 0, MLKEM_N, 8192))
41+
requires(twiddles12345 == mlk_aarch64_ntt_zetas_layer12345)
42+
requires(twiddles56 == mlk_aarch64_ntt_zetas_layer67)
43+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
44+
/* check-magic: off */
45+
ensures(array_abs_bound(p, 0, MLKEM_N, 23595))
46+
/* check-magic: on */
47+
);
3548

3649
#define mlk_intt_asm MLK_NAMESPACE(intt_asm)
37-
void mlk_intt_asm(int16_t *, const int16_t *, const int16_t *);
50+
void mlk_intt_asm(int16_t *p, const int16_t *twiddles12345,
51+
const int16_t *twiddles56)
52+
/* This must be kept in sync with the HOL-Light specification
53+
* in proofs/hol_light/arm/proofs/mlkem_intt.ml */
54+
__contract__(
55+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
56+
requires(twiddles12345 == mlk_aarch64_invntt_zetas_layer12345)
57+
requires(twiddles56 == mlk_aarch64_invntt_zetas_layer67)
58+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
59+
/* check-magic: off */
60+
ensures(array_abs_bound(p, 0, MLKEM_N, 26625))
61+
/* check-magic: on */
62+
);
3863

3964
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
4065
void mlk_poly_reduce_asm(int16_t *);
4166

4267
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
43-
void mlk_poly_tomont_asm(int16_t *);
68+
void mlk_poly_tomont_asm(int16_t *p)
69+
/* This must be kept in sync with the HOL-Light specification
70+
* in proofs/hol_light/arm/proofs/mlkem_poly_tomont.ml */
71+
__contract__(
72+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
73+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
74+
ensures(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q))
75+
);
4476

4577
#define mlk_poly_mulcache_compute_asm MLK_NAMESPACE(poly_mulcache_compute_asm)
4678
void mlk_poly_mulcache_compute_asm(int16_t *, const int16_t *, const int16_t *,
4779
const int16_t *);
4880

4981
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
50-
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a);
82+
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a)
83+
/* This must be kept in sync with the HOL-Light specification
84+
* in proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml */
85+
__contract__(
86+
requires(memory_no_alias(r, MLKEM_POLYBYTES))
87+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
88+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
89+
assigns(object_whole(r))
90+
);
5191

5292
#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \
5393
MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2)

‎proofs/cbmc/intt_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 = intt_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 = intt_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
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/native/aarch64/src/aarch64_zetas.c
23+
24+
CHECK_FUNCTION_CONTRACTS=mlk_intt_native
25+
USE_FUNCTION_CONTRACTS=mlk_intt_asm
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_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/intt_native_aarch64/intt_native_aarch64_harness.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
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+
void mlk_intt_native(int16_t data[MLKEM_N]);
10+
11+
void harness(void)
12+
{
13+
int16_t *r;
14+
mlk_intt_native(r);
15+
}

‎proofs/cbmc/ntt_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 = ntt_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 = ntt_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
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/native/aarch64/src/aarch64_zetas.c
23+
24+
CHECK_FUNCTION_CONTRACTS=mlk_ntt_native
25+
USE_FUNCTION_CONTRACTS=mlk_ntt_asm
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_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/ntt_native_aarch64/ntt_native_aarch64_harness.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
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+
void mlk_ntt_native(int16_t data[MLKEM_N]);
10+
11+
void harness(void)
12+
{
13+
int16_t *r;
14+
mlk_ntt_native(r);
15+
}

0 commit comments

Comments
 (0)