Skip to content

Commit c1725f3

Browse files
mkannwischermkannwischer
committed
CBMC/AArch64: Add contracts and proof poly_decompose asm functions
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent ebe4c51 commit c1725f3

7 files changed

Lines changed: 251 additions & 6 deletions

File tree

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,10 +98,36 @@ uint64_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
9898

9999
#if !defined(MLD_CONFIG_NO_SIGN_API)
100100
#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
101-
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0);
101+
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0)
102+
/* This must be kept in sync with the HOL-Light specification
103+
* in proofs/hol_light/aarch64/proofs/poly_decompose_32_aarch64_asm.ml */
104+
__contract__(
105+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
106+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
107+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
108+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
109+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
110+
/* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */
111+
ensures(array_bound(a1, 0, MLDSA_N, 0, 16))
112+
/* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */
113+
ensures(array_abs_bound(a0, 0, MLDSA_N, 261889))
114+
);
102115

103116
#define mld_poly_decompose_88_asm MLD_NAMESPACE(poly_decompose_88_asm)
104-
void mld_poly_decompose_88_asm(int32_t *a1, int32_t *a0);
117+
void mld_poly_decompose_88_asm(int32_t *a1, int32_t *a0)
118+
/* This must be kept in sync with the HOL-Light specification
119+
* in proofs/hol_light/aarch64/proofs/poly_decompose_88_aarch64_asm.ml */
120+
__contract__(
121+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
122+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
123+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
124+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
125+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
126+
/* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */
127+
ensures(array_bound(a1, 0, MLDSA_N, 0, 44))
128+
/* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */
129+
ensures(array_abs_bound(a0, 0, MLDSA_N, 95233))
130+
);
105131
#endif /* !MLD_CONFIG_NO_SIGN_API */
106132

107133
#define mld_poly_caddq_asm MLD_NAMESPACE(poly_caddq_asm)

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,10 +98,36 @@ uint64_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
9898

9999
#if !defined(MLD_CONFIG_NO_SIGN_API)
100100
#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
101-
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0);
101+
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0)
102+
/* This must be kept in sync with the HOL-Light specification
103+
* in proofs/hol_light/aarch64/proofs/poly_decompose_32_aarch64_asm.ml */
104+
__contract__(
105+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
106+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
107+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
108+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
109+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
110+
/* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */
111+
ensures(array_bound(a1, 0, MLDSA_N, 0, 16))
112+
/* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */
113+
ensures(array_abs_bound(a0, 0, MLDSA_N, 261889))
114+
);
102115

103116
#define mld_poly_decompose_88_asm MLD_NAMESPACE(poly_decompose_88_asm)
104-
void mld_poly_decompose_88_asm(int32_t *a1, int32_t *a0);
117+
void mld_poly_decompose_88_asm(int32_t *a1, int32_t *a0)
118+
/* This must be kept in sync with the HOL-Light specification
119+
* in proofs/hol_light/aarch64/proofs/poly_decompose_88_aarch64_asm.ml */
120+
__contract__(
121+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
122+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
123+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
124+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
125+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
126+
/* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */
127+
ensures(array_bound(a1, 0, MLDSA_N, 0, 44))
128+
/* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */
129+
ensures(array_abs_bound(a0, 0, MLDSA_N, 95233))
130+
);
105131
#endif /* !MLD_CONFIG_NO_SIGN_API */
106132

107133
#define mld_poly_caddq_asm MLD_NAMESPACE(poly_caddq_asm)

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

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,10 +98,36 @@ uint64_t mld_rej_uniform_eta4_asm(int32_t *r, const uint8_t *buf,
9898

9999
#if !defined(MLD_CONFIG_NO_SIGN_API)
100100
#define mld_poly_decompose_32_asm MLD_NAMESPACE(poly_decompose_32_asm)
101-
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0);
101+
void mld_poly_decompose_32_asm(int32_t *a1, int32_t *a0)
102+
/* This must be kept in sync with the HOL-Light specification
103+
* in proofs/hol_light/aarch64/proofs/poly_decompose_32_aarch64_asm.ml */
104+
__contract__(
105+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
106+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
107+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
108+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
109+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
110+
/* check-magic: 16 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 32)) */
111+
ensures(array_bound(a1, 0, MLDSA_N, 0, 16))
112+
/* check-magic: 261889 == (MLDSA_Q - 1) / 32 + 1 */
113+
ensures(array_abs_bound(a0, 0, MLDSA_N, 261889))
114+
);
102115

103116
#define mld_poly_decompose_88_asm MLD_NAMESPACE(poly_decompose_88_asm)
104-
void mld_poly_decompose_88_asm(int32_t *a1, int32_t *a0);
117+
void mld_poly_decompose_88_asm(int32_t *a1, int32_t *a0)
118+
/* This must be kept in sync with the HOL-Light specification
119+
* in proofs/hol_light/aarch64/proofs/poly_decompose_88_aarch64_asm.ml */
120+
__contract__(
121+
requires(memory_no_alias(a1, sizeof(int32_t) * MLDSA_N))
122+
requires(memory_no_alias(a0, sizeof(int32_t) * MLDSA_N))
123+
requires(array_bound(a0, 0, MLDSA_N, 0, MLDSA_Q))
124+
assigns(memory_slice(a1, sizeof(int32_t) * MLDSA_N))
125+
assigns(memory_slice(a0, sizeof(int32_t) * MLDSA_N))
126+
/* check-magic: 44 == (MLDSA_Q - 1) / (2 * ((MLDSA_Q - 1) / 88)) */
127+
ensures(array_bound(a1, 0, MLDSA_N, 0, 44))
128+
/* check-magic: 95233 == (MLDSA_Q - 1) / 88 + 1 */
129+
ensures(array_abs_bound(a0, 0, MLDSA_N, 95233))
130+
);
105131
#endif /* !MLD_CONFIG_NO_SIGN_API */
106132

107133
#define mld_poly_caddq_asm MLD_NAMESPACE(poly_caddq_asm)

‎proofs/cbmc/poly_decompose_32_native_aarch64/Makefile‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
# Copyright (c) The mldsa-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 = poly_decompose_32_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 = poly_decompose_32_native_aarch64
12+
13+
# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
14+
# included, which contains the CBMC specifications.
15+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/aarch64/meta.h\"" -DMLD_CHECK_APIS
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
23+
24+
# poly_decompose_32 is only used with ML-DSA-65 and ML-DSA-87
25+
ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
26+
CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_32_native
27+
USE_FUNCTION_CONTRACTS = mld_poly_decompose_32_asm
28+
else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
29+
CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_32_native
30+
USE_FUNCTION_CONTRACTS = mld_poly_decompose_32_asm
31+
else
32+
CHECK_FUNCTION_CONTRACTS=
33+
USE_FUNCTION_CONTRACTS =
34+
endif
35+
APPLY_LOOP_CONTRACTS=on
36+
USE_DYNAMIC_FRAMES=1
37+
38+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
39+
EXTERNAL_SAT_SOLVER=
40+
CBMCFLAGS=--smt2
41+
42+
FUNCTION_NAME = poly_decompose_32_native_aarch64
43+
44+
# If this proof is found to consume huge amounts of RAM, you can set the
45+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
46+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
47+
# documentation in Makefile.common under the "Job Pools" heading for details.
48+
# EXPENSIVE = true
49+
50+
# This function is large enough to need...
51+
CBMC_OBJECT_BITS = 8
52+
53+
# If you require access to a file-local ("static") function or object to conduct
54+
# your proof, set the following (and do not include the original source file
55+
# ("mldsa/poly_kl.c") in PROJECT_SOURCES).
56+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
57+
# include ../Makefile.common
58+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly_kl.c
59+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
60+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
61+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
62+
# be set before including Makefile.common, but any use of variables on the
63+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
64+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
65+
66+
include ../Makefile.common

‎proofs/cbmc/poly_decompose_32_native_aarch64/poly_decompose_32_native_aarch64_harness.c‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include <stdint.h>
5+
#include "cbmc.h"
6+
#include "params.h"
7+
8+
int mld_poly_decompose_32_native(int32_t *a1, int32_t *a0);
9+
10+
void harness(void)
11+
{
12+
/* mld_poly_decompose_32_native is only defined for ML-DSA-65 and ML-DSA-87 */
13+
#if MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87
14+
int32_t *a1;
15+
int32_t *a0;
16+
int t;
17+
t = mld_poly_decompose_32_native(a1, a0);
18+
#endif /* MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87 */
19+
}

‎proofs/cbmc/poly_decompose_88_native_aarch64/Makefile‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
# Copyright (c) The mldsa-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 = poly_decompose_88_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 = poly_decompose_88_native_aarch64
12+
13+
# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
14+
# included, which contains the CBMC specifications.
15+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/aarch64/meta.h\"" -DMLD_CHECK_APIS
16+
INCLUDES +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
UNWINDSET +=
20+
21+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
22+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
23+
24+
# poly_decompose_88 is only used with ML-DSA-44
25+
ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
26+
CHECK_FUNCTION_CONTRACTS=mld_poly_decompose_88_native
27+
USE_FUNCTION_CONTRACTS = mld_poly_decompose_88_asm
28+
else
29+
CHECK_FUNCTION_CONTRACTS=
30+
USE_FUNCTION_CONTRACTS =
31+
endif
32+
APPLY_LOOP_CONTRACTS=on
33+
USE_DYNAMIC_FRAMES=1
34+
35+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
36+
EXTERNAL_SAT_SOLVER=
37+
CBMCFLAGS=--smt2
38+
39+
FUNCTION_NAME = poly_decompose_88_native_aarch64
40+
41+
# If this proof is found to consume huge amounts of RAM, you can set the
42+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
43+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
44+
# documentation in Makefile.common under the "Job Pools" heading for details.
45+
# EXPENSIVE = true
46+
47+
# This function is large enough to need...
48+
CBMC_OBJECT_BITS = 8
49+
50+
# If you require access to a file-local ("static") function or object to conduct
51+
# your proof, set the following (and do not include the original source file
52+
# ("mldsa/poly_kl.c") in PROJECT_SOURCES).
53+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
54+
# include ../Makefile.common
55+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly_kl.c
56+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
57+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
58+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
59+
# be set before including Makefile.common, but any use of variables on the
60+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
61+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
62+
63+
include ../Makefile.common

‎proofs/cbmc/poly_decompose_88_native_aarch64/poly_decompose_88_native_aarch64_harness.c‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include <stdint.h>
5+
#include "cbmc.h"
6+
#include "params.h"
7+
8+
int mld_poly_decompose_88_native(int32_t *a1, int32_t *a0);
9+
10+
void harness(void)
11+
{
12+
/* mld_poly_decompose_88_native is only defined for ML-DSA-44 */
13+
#if MLD_CONFIG_PARAMETER_SET == 44
14+
int32_t *a1;
15+
int32_t *a0;
16+
int t;
17+
t = mld_poly_decompose_88_native(a1, a0);
18+
#endif /* MLD_CONFIG_PARAMETER_SET == 44 */
19+
}

0 commit comments

Comments
 (0)