Skip to content

Commit 0c231fc

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #1030 from pq-code-package/cbmc-aarch64-poly2
CBMC: Prove AArch64 native API for poly_reduce, poly_mulcache_compute atop HOL-Light spec
2 parents 0843f3f + 71a40c9 commit 0c231fc

File tree

15 files changed

+223
-27
lines changed

15 files changed

+223
-27
lines changed

‎dev/aarch64_clean/src/arith_native_aarch64.h

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,14 @@ __contract__(
6262
);
6363

6464
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
65-
void mlk_poly_reduce_asm(int16_t *);
65+
void mlk_poly_reduce_asm(int16_t *p)
66+
/* This must be kept in sync with the HOL-Light specification
67+
* in proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml */
68+
__contract__(
69+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
70+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
71+
ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))
72+
);
6673

6774
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
6875
void mlk_poly_tomont_asm(int16_t *p)
@@ -75,8 +82,18 @@ __contract__(
7582
);
7683

7784
#define mlk_poly_mulcache_compute_asm MLK_NAMESPACE(poly_mulcache_compute_asm)
78-
void mlk_poly_mulcache_compute_asm(int16_t *, const int16_t *, const int16_t *,
79-
const int16_t *);
85+
void mlk_poly_mulcache_compute_asm(int16_t *cache, const int16_t *mlk_poly,
86+
const int16_t *zetas,
87+
const int16_t *zetas_twisted)
88+
/* This must be kept in sync with the HOL-Light specification
89+
* in proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml */
90+
__contract__(
91+
requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
92+
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
93+
requires(zetas == mlk_aarch64_zetas_mulcache_native)
94+
requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
95+
assigns(object_whole(cache))
96+
);
8097

8198
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
8299
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a)

‎dev/aarch64_opt/src/arith_native_aarch64.h

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,14 @@ __contract__(
6262
);
6363

6464
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
65-
void mlk_poly_reduce_asm(int16_t *);
65+
void mlk_poly_reduce_asm(int16_t *p)
66+
/* This must be kept in sync with the HOL-Light specification
67+
* in proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml */
68+
__contract__(
69+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
70+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
71+
ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))
72+
);
6673

6774
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
6875
void mlk_poly_tomont_asm(int16_t *p)
@@ -75,8 +82,18 @@ __contract__(
7582
);
7683

7784
#define mlk_poly_mulcache_compute_asm MLK_NAMESPACE(poly_mulcache_compute_asm)
78-
void mlk_poly_mulcache_compute_asm(int16_t *, const int16_t *, const int16_t *,
79-
const int16_t *);
85+
void mlk_poly_mulcache_compute_asm(int16_t *cache, const int16_t *mlk_poly,
86+
const int16_t *zetas,
87+
const int16_t *zetas_twisted)
88+
/* This must be kept in sync with the HOL-Light specification
89+
* in proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml */
90+
__contract__(
91+
requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
92+
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
93+
requires(zetas == mlk_aarch64_zetas_mulcache_native)
94+
requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
95+
assigns(object_whole(cache))
96+
);
8097

8198
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
8299
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a)

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

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,14 @@ __contract__(
6262
);
6363

6464
#define mlk_poly_reduce_asm MLK_NAMESPACE(poly_reduce_asm)
65-
void mlk_poly_reduce_asm(int16_t *);
65+
void mlk_poly_reduce_asm(int16_t *p)
66+
/* This must be kept in sync with the HOL-Light specification
67+
* in proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml */
68+
__contract__(
69+
requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
70+
assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
71+
ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))
72+
);
6673

6774
#define mlk_poly_tomont_asm MLK_NAMESPACE(poly_tomont_asm)
6875
void mlk_poly_tomont_asm(int16_t *p)
@@ -75,8 +82,18 @@ __contract__(
7582
);
7683

7784
#define mlk_poly_mulcache_compute_asm MLK_NAMESPACE(poly_mulcache_compute_asm)
78-
void mlk_poly_mulcache_compute_asm(int16_t *, const int16_t *, const int16_t *,
79-
const int16_t *);
85+
void mlk_poly_mulcache_compute_asm(int16_t *cache, const int16_t *mlk_poly,
86+
const int16_t *zetas,
87+
const int16_t *zetas_twisted)
88+
/* This must be kept in sync with the HOL-Light specification
89+
* in proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml */
90+
__contract__(
91+
requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
92+
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
93+
requires(zetas == mlk_aarch64_zetas_mulcache_native)
94+
requires(zetas_twisted == mlk_aarch64_zetas_mulcache_twisted_native)
95+
assigns(object_whole(cache))
96+
);
8097

8198
#define mlk_poly_tobytes_asm MLK_NAMESPACE(poly_tobytes_asm)
8299
void mlk_poly_tobytes_asm(uint8_t *r, const int16_t *a)

‎mlkem/native/api.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -209,7 +209,6 @@ __contract__(
209209
requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2)))
210210
requires(memory_no_alias(mlk_poly, sizeof(int16_t) * MLKEM_N))
211211
assigns(object_whole(cache))
212-
ensures(array_abs_bound(cache, 0, MLKEM_N / 2, MLKEM_Q))
213212
);
214213
#endif /* MLK_USE_NATIVE_POLY_MULCACHE_COMPUTE */
215214

‎mlkem/poly.c

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -283,12 +283,6 @@ MLK_INTERNAL_API
283283
void mlk_poly_mulcache_compute(mlk_poly_mulcache *x, const mlk_poly *a)
284284
{
285285
mlk_poly_mulcache_compute_native(x->coeffs, a->coeffs);
286-
/*
287-
* This bound is true for the AArch64 and AVX2 implementations,
288-
* but not needed in the higher level bounds reasoning.
289-
* It is thus omitted from the spec but checked here nonetheless.
290-
*/
291-
mlk_assert_abs_bound(x, MLKEM_N / 2, MLKEM_Q);
292286
}
293287
#endif /* MLK_USE_NATIVE_POLY_MULCACHE_COMPUTE */
294288

‎proofs/cbmc/poly_mulcache_compute_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 = poly_mulcache_compute_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_mulcache_compute_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_poly_mulcache_compute_native
25+
USE_FUNCTION_CONTRACTS=mlk_poly_mulcache_compute_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 = poly_mulcache_compute_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/poly_mulcache_compute_native_aarch64/poly_mulcache_compute_native_aarch64_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+
void mlk_poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2],
10+
const int16_t mlk_poly[MLKEM_N]);
11+
12+
void harness(void)
13+
{
14+
int16_t *r, *c;
15+
mlk_poly_mulcache_compute_native(c, r);
16+
}

‎proofs/cbmc/poly_reduce_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 = poly_reduce_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_reduce_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
23+
24+
CHECK_FUNCTION_CONTRACTS=mlk_poly_reduce_native
25+
USE_FUNCTION_CONTRACTS=mlk_poly_reduce_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 = poly_reduce_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/poly_reduce_native_aarch64/poly_reduce_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_poly_reduce_native(int16_t p[MLKEM_N]);
10+
11+
void harness(void)
12+
{
13+
int16_t *r;
14+
mlk_poly_reduce_native(r);
15+
}

‎proofs/hol_light/arm/proofs/mlkem_intt.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -482,8 +482,6 @@ let intt_constants = define
482482
(* Correctness proof. *)
483483
(* ------------------------------------------------------------------------- *)
484484

485-
(* NOTE: This must be kept in sync with the CBMC specification
486-
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
487485

488486
let MLKEM_INTT_CORRECT = prove
489487
(`!a z_12345 z_67 x pc.
@@ -578,6 +576,9 @@ let MLKEM_INTT_CORRECT = prove
578576

579577
(*** Subroutine form, somewhat messy elaboration of the usual wrapper ***)
580578

579+
(* NOTE: This must be kept in sync with the CBMC specification
580+
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
581+
581582
let MLKEM_INTT_SUBROUTINE_CORRECT = prove
582583
(`!a z_12345 z_67 x pc stackpointer returnaddress.
583584
aligned 16 stackpointer /\

‎proofs/hol_light/arm/proofs/mlkem_ntt.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -357,9 +357,6 @@ let ntt_constants = define
357357
(* Correctness proof. *)
358358
(* ------------------------------------------------------------------------- *)
359359

360-
(* NOTE: This must be kept in sync with the CBMC specification
361-
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
362-
363360
let MLKEM_NTT_CORRECT = prove
364361
(`!a z_12345 z_67 x pc.
365362
ALL (nonoverlapping (a,512))
@@ -459,6 +456,9 @@ let MLKEM_NTT_CORRECT = prove
459456

460457
(*** Subroutine form, somewhat messy elaboration of the usual wrapper ***)
461458

459+
(* NOTE: This must be kept in sync with the CBMC specification
460+
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
461+
462462
let MLKEM_NTT_SUBROUTINE_CORRECT = prove
463463
(`!a z_12345 z_67 x pc stackpointer returnaddress.
464464
aligned 16 stackpointer /\

‎proofs/hol_light/arm/proofs/mlkem_poly_mulcache_compute.ml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,9 @@ let have_mulcache_zetas = define
9595
iword (EL i mulcache_zetas_twisted))
9696
`;;
9797

98+
(* NOTE: This must be kept in sync with the CBMC specification
99+
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
100+
98101
let poly_mulcache_compute_GOAL = `forall pc src dst zetas zetas_twisted x y returnaddress.
99102
ALL (nonoverlapping (dst, 256))
100103
[(word pc, LENGTH poly_mulcache_compute_mc); (src, 512); (zetas, 256); (zetas_twisted, 256)]

‎proofs/hol_light/arm/proofs/mlkem_poly_reduce.ml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,9 @@ let MLKEM_POLY_REDUCE_CORRECT = prove
180180
ASM_REWRITE_TAC[WORD_ADD_0] THEN DISCARD_STATE_TAC "s276" THEN
181181
REWRITE_TAC[GSYM barred; overall_lemma]);;
182182

183+
(* NOTE: This must be kept in sync with the CBMC specification
184+
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
185+
183186
let MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT = prove
184187
(`!a x pc returnaddress.
185188
nonoverlapping (word pc,0x124) (a,512)

‎proofs/hol_light/arm/proofs/mlkem_poly_tobytes.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -168,9 +168,6 @@ let lemma =
168168
CONV_RULE(EXPAND_CASES_CONV THENC
169169
DEPTH_CONV (NUM_RED_CONV ORELSEC EL_CONV)) th';;
170170

171-
(* NOTE: This must be kept in sync with the CBMC specification
172-
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
173-
174171
let MLKEM_POLY_TOBYTES_CORRECT = prove
175172
(`!r a (l:int16 list) pc.
176173
ALL (nonoverlapping (r,384)) [(word pc,0x158); (a,512)]
@@ -247,6 +244,9 @@ let MLKEM_POLY_TOBYTES_CORRECT = prove
247244
REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN
248245
ABBREV_TAC `twae = &2:real` THEN REAL_ARITH_TAC);;
249246

247+
(* NOTE: This must be kept in sync with the CBMC specification
248+
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
249+
250250
let MLKEM_POLY_TOBYTES_SUBROUTINE_CORRECT = prove
251251
(`!r a (l:int16 list) pc returnaddress.
252252
ALL (nonoverlapping (r,384)) [(word pc,0x158); (a,512)]

‎proofs/hol_light/arm/proofs/mlkem_rej_uniform.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -455,9 +455,6 @@ let DIMINDEX_384 = DIMINDEX_CONV `dimindex(:384)`;;
455455
(* Now the actual proof. *)
456456
(* ------------------------------------------------------------------------- *)
457457

458-
(* NOTE: This must be kept in sync with the CBMC specification
459-
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
460-
461458
let MLKEM_REJ_UNIFORM_CORRECT = prove
462459
(`!res buf buflen table (inlist:(12 word)list) pc stackpointer.
463460
24 divides val buflen /\
@@ -1604,6 +1601,9 @@ let MLKEM_REJ_UNIFORM_CORRECT = prove
16041601
SUBST1_TAC(SYM(ASSUME `curlen + len0:num = curlen1`)) THEN
16051602
CONV_TAC WORD_RULE);;
16061603

1604+
(* NOTE: This must be kept in sync with the CBMC specification
1605+
* in mlkem/native/aarch64/src/arith_native_aarch64.h *)
1606+
16071607
let MLKEM_REJ_UNIFORM_SUBROUTINE_CORRECT = prove
16081608
(`!res buf buflen table (inlist:(12 word)list) pc stackpointer returnaddress.
16091609
24 divides val buflen /\

0 commit comments

Comments
 (0)