Skip to content

Commit 1d4054c

Browse files
hanno-beckermkannwischer
hanno-becker
authored and
mkannwischer
committed
CBMC/x86_64: Add specs and proofs for compression routines
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent dd0b460 commit 1d4054c

39 files changed

Lines changed: 1249 additions & 49 deletions

File tree

‎dev/x86_64/src/arith_native_x86_64.h‎

Lines changed: 44 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,17 @@ __contract__(
189189
#define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2)
190190
void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],
191191
const int16_t *MLK_RESTRICT a,
192-
const uint8_t *data);
192+
const uint8_t *data)
193+
/* This must be kept in sync with the HOL-Light specification in
194+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d4.ml.
195+
*/
196+
__contract__(
197+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
198+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
199+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
200+
requires(data == mlk_compress_d4_data)
201+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
202+
);
193203

194204
#define mlk_poly_decompress_d4_avx2 MLK_NAMESPACE(poly_decompress_d4_avx2)
195205
void mlk_poly_decompress_d4_avx2(int16_t *MLK_RESTRICT r,
@@ -209,7 +219,17 @@ __contract__(
209219
#define mlk_poly_compress_d10_avx2 MLK_NAMESPACE(poly_compress_d10_avx2)
210220
void mlk_poly_compress_d10_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10],
211221
const int16_t *MLK_RESTRICT a,
212-
const uint8_t *data);
222+
const uint8_t *data)
223+
/* This must be kept in sync with the HOL-Light specification in
224+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d10.ml.
225+
*/
226+
__contract__(
227+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
228+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
229+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
230+
requires(data == mlk_compress_d10_data)
231+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
232+
);
213233

214234
#define mlk_poly_decompress_d10_avx2 MLK_NAMESPACE(poly_decompress_d10_avx2)
215235
void mlk_poly_decompress_d10_avx2(
@@ -229,7 +249,17 @@ __contract__(
229249
#define mlk_poly_compress_d5_avx2 MLK_NAMESPACE(poly_compress_d5_avx2)
230250
void mlk_poly_compress_d5_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5],
231251
const int16_t *MLK_RESTRICT a,
232-
const uint8_t *data);
252+
const uint8_t *data)
253+
/* This must be kept in sync with the HOL-Light specification in
254+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d5.ml.
255+
*/
256+
__contract__(
257+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
258+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
259+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
260+
requires(data == mlk_compress_d5_data)
261+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
262+
);
233263

234264
#define mlk_poly_decompress_d5_avx2 MLK_NAMESPACE(poly_decompress_d5_avx2)
235265
void mlk_poly_decompress_d5_avx2(int16_t *MLK_RESTRICT r,
@@ -249,7 +279,17 @@ __contract__(
249279
#define mlk_poly_compress_d11_avx2 MLK_NAMESPACE(poly_compress_d11_avx2)
250280
void mlk_poly_compress_d11_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11],
251281
const int16_t *MLK_RESTRICT a,
252-
const uint8_t *data);
282+
const uint8_t *data)
283+
/* This must be kept in sync with the HOL-Light specification in
284+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d11.ml.
285+
*/
286+
__contract__(
287+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
288+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
289+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
290+
requires(data == mlk_compress_d11_data)
291+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
292+
);
253293

254294
#define mlk_poly_decompress_d11_avx2 MLK_NAMESPACE(poly_decompress_d11_avx2)
255295
void mlk_poly_decompress_d11_avx2(

‎mlkem/src/compress.c‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,12 @@
3535
* in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
3636
MLK_STATIC_TESTABLE void mlk_poly_compress_d4_c(
3737
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const mlk_poly *a)
38+
__contract__(
39+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
40+
requires(memory_no_alias(a, sizeof(mlk_poly)))
41+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
42+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
43+
)
3844
{
3945
unsigned i;
4046
mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
@@ -63,6 +69,12 @@ MLK_STATIC_TESTABLE void mlk_poly_compress_d4_c(
6369
MLK_INTERNAL_API
6470
void mlk_poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],
6571
const mlk_poly *a)
72+
__contract__(
73+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
74+
requires(memory_no_alias(a, sizeof(mlk_poly)))
75+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
76+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
77+
)
6678
{
6779
#if defined(MLK_USE_NATIVE_POLY_COMPRESS_D4)
6880
int ret;
@@ -85,6 +97,12 @@ void mlk_poly_compress_d4(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],
8597
* in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
8698
MLK_STATIC_TESTABLE void mlk_poly_compress_d10_c(
8799
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const mlk_poly *a)
100+
__contract__(
101+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
102+
requires(memory_no_alias(a, sizeof(mlk_poly)))
103+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
104+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
105+
)
88106
{
89107
unsigned j;
90108
mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
@@ -116,6 +134,12 @@ MLK_STATIC_TESTABLE void mlk_poly_compress_d10_c(
116134
MLK_INTERNAL_API
117135
void mlk_poly_compress_d10(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10],
118136
const mlk_poly *a)
137+
__contract__(
138+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
139+
requires(memory_no_alias(a, sizeof(mlk_poly)))
140+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
141+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
142+
)
119143
{
120144
#if defined(MLK_USE_NATIVE_POLY_COMPRESS_D10)
121145
int ret;
@@ -248,6 +272,12 @@ __contract__(
248272
* in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
249273
MLK_STATIC_TESTABLE void mlk_poly_compress_d5_c(
250274
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const mlk_poly *a)
275+
__contract__(
276+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
277+
requires(memory_no_alias(a, sizeof(mlk_poly)))
278+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
279+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
280+
)
251281
{
252282
unsigned i;
253283
mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
@@ -276,6 +306,12 @@ MLK_STATIC_TESTABLE void mlk_poly_compress_d5_c(
276306
MLK_INTERNAL_API
277307
void mlk_poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5],
278308
const mlk_poly *a)
309+
__contract__(
310+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
311+
requires(memory_no_alias(a, sizeof(mlk_poly)))
312+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
313+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
314+
)
279315
{
280316
#if defined(MLK_USE_NATIVE_POLY_COMPRESS_D5)
281317
int ret;
@@ -298,6 +334,12 @@ void mlk_poly_compress_d5(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5],
298334
* in the range (-MLKEM_Q+1,...,MLKEM_Q-1). */
299335
MLK_STATIC_TESTABLE void mlk_poly_compress_d11_c(
300336
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const mlk_poly *a)
337+
__contract__(
338+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
339+
requires(memory_no_alias(a, sizeof(mlk_poly)))
340+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
341+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
342+
)
301343
{
302344
unsigned j;
303345
mlk_assert_bound(a, MLKEM_N, 0, MLKEM_Q);
@@ -336,6 +378,12 @@ MLK_STATIC_TESTABLE void mlk_poly_compress_d11_c(
336378
MLK_INTERNAL_API
337379
void mlk_poly_compress_d11(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11],
338380
const mlk_poly *a)
381+
__contract__(
382+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
383+
requires(memory_no_alias(a, sizeof(mlk_poly)))
384+
requires(array_bound(a->coeffs, 0, MLKEM_N, 0, MLKEM_Q))
385+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
386+
)
339387
{
340388
#if defined(MLK_USE_NATIVE_POLY_COMPRESS_D11)
341389
int ret;

‎mlkem/src/native/api.h‎

Lines changed: 28 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -446,7 +446,13 @@ __contract__(
446446
**************************************************/
447447
MLK_MUST_CHECK_RETURN_VALUE
448448
static MLK_INLINE int mlk_poly_compress_d4_native(
449-
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const int16_t a[MLKEM_N]);
449+
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], const int16_t a[MLKEM_N])
450+
__contract__(
451+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
452+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
453+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
454+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
455+
ensures(return_value == MLK_NATIVE_FUNC_SUCCESS || return_value == MLK_NATIVE_FUNC_FALLBACK));
450456
#endif /* MLK_USE_NATIVE_POLY_COMPRESS_D4 */
451457

452458
#if defined(MLK_USE_NATIVE_POLY_COMPRESS_D10)
@@ -464,7 +470,13 @@ static MLK_INLINE int mlk_poly_compress_d4_native(
464470
**************************************************/
465471
MLK_MUST_CHECK_RETURN_VALUE
466472
static MLK_INLINE int mlk_poly_compress_d10_native(
467-
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const int16_t a[MLKEM_N]);
473+
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10], const int16_t a[MLKEM_N])
474+
__contract__(
475+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
476+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
477+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
478+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
479+
ensures(return_value == MLK_NATIVE_FUNC_SUCCESS || return_value == MLK_NATIVE_FUNC_FALLBACK));
468480
#endif /* MLK_USE_NATIVE_POLY_COMPRESS_D10 */
469481

470482
#if defined(MLK_USE_NATIVE_POLY_DECOMPRESS_D4)
@@ -536,7 +548,13 @@ __contract__(
536548
**************************************************/
537549
MLK_MUST_CHECK_RETURN_VALUE
538550
static MLK_INLINE int mlk_poly_compress_d5_native(
539-
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const int16_t a[MLKEM_N]);
551+
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5], const int16_t a[MLKEM_N])
552+
__contract__(
553+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
554+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
555+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
556+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
557+
ensures(return_value == MLK_NATIVE_FUNC_SUCCESS || return_value == MLK_NATIVE_FUNC_FALLBACK));
540558
#endif /* MLK_USE_NATIVE_POLY_COMPRESS_D5 */
541559

542560
#if defined(MLK_USE_NATIVE_POLY_COMPRESS_D11)
@@ -554,7 +572,13 @@ static MLK_INLINE int mlk_poly_compress_d5_native(
554572
**************************************************/
555573
MLK_MUST_CHECK_RETURN_VALUE
556574
static MLK_INLINE int mlk_poly_compress_d11_native(
557-
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const int16_t a[MLKEM_N]);
575+
uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11], const int16_t a[MLKEM_N])
576+
__contract__(
577+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
578+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
579+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
580+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
581+
ensures(return_value == MLK_NATIVE_FUNC_SUCCESS || return_value == MLK_NATIVE_FUNC_FALLBACK));
558582
#endif /* MLK_USE_NATIVE_POLY_COMPRESS_D11 */
559583

560584
#if defined(MLK_USE_NATIVE_POLY_DECOMPRESS_D5)

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

Lines changed: 44 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,17 @@ __contract__(
189189
#define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2)
190190
void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4],
191191
const int16_t *MLK_RESTRICT a,
192-
const uint8_t *data);
192+
const uint8_t *data)
193+
/* This must be kept in sync with the HOL-Light specification in
194+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d4.ml.
195+
*/
196+
__contract__(
197+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
198+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
199+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
200+
requires(data == mlk_compress_d4_data)
201+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D4))
202+
);
193203

194204
#define mlk_poly_decompress_d4_avx2 MLK_NAMESPACE(poly_decompress_d4_avx2)
195205
void mlk_poly_decompress_d4_avx2(int16_t *MLK_RESTRICT r,
@@ -209,7 +219,17 @@ __contract__(
209219
#define mlk_poly_compress_d10_avx2 MLK_NAMESPACE(poly_compress_d10_avx2)
210220
void mlk_poly_compress_d10_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D10],
211221
const int16_t *MLK_RESTRICT a,
212-
const uint8_t *data);
222+
const uint8_t *data)
223+
/* This must be kept in sync with the HOL-Light specification in
224+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d10.ml.
225+
*/
226+
__contract__(
227+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
228+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
229+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
230+
requires(data == mlk_compress_d10_data)
231+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D10))
232+
);
213233

214234
#define mlk_poly_decompress_d10_avx2 MLK_NAMESPACE(poly_decompress_d10_avx2)
215235
void mlk_poly_decompress_d10_avx2(
@@ -229,7 +249,17 @@ __contract__(
229249
#define mlk_poly_compress_d5_avx2 MLK_NAMESPACE(poly_compress_d5_avx2)
230250
void mlk_poly_compress_d5_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D5],
231251
const int16_t *MLK_RESTRICT a,
232-
const uint8_t *data);
252+
const uint8_t *data)
253+
/* This must be kept in sync with the HOL-Light specification in
254+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d5.ml.
255+
*/
256+
__contract__(
257+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
258+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
259+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
260+
requires(data == mlk_compress_d5_data)
261+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D5))
262+
);
233263

234264
#define mlk_poly_decompress_d5_avx2 MLK_NAMESPACE(poly_decompress_d5_avx2)
235265
void mlk_poly_decompress_d5_avx2(int16_t *MLK_RESTRICT r,
@@ -249,7 +279,17 @@ __contract__(
249279
#define mlk_poly_compress_d11_avx2 MLK_NAMESPACE(poly_compress_d11_avx2)
250280
void mlk_poly_compress_d11_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D11],
251281
const int16_t *MLK_RESTRICT a,
252-
const uint8_t *data);
282+
const uint8_t *data)
283+
/* This must be kept in sync with the HOL-Light specification in
284+
* proofs/hol_light/x86_64/proofs/mlkem_poly_compress_d11.ml.
285+
*/
286+
__contract__(
287+
requires(memory_no_alias(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
288+
requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N))
289+
requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
290+
requires(data == mlk_compress_d11_data)
291+
assigns(memory_slice(r, MLKEM_POLYCOMPRESSEDBYTES_D11))
292+
);
253293

254294
#define mlk_poly_decompress_d11_avx2 MLK_NAMESPACE(poly_decompress_d11_avx2)
255295
void mlk_poly_decompress_d11_avx2(

‎proofs/cbmc/dummy_backend.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,10 @@
2020
#define MLK_USE_NATIVE_POLY_DECOMPRESS_D5
2121
#define MLK_USE_NATIVE_POLY_DECOMPRESS_D10
2222
#define MLK_USE_NATIVE_POLY_DECOMPRESS_D11
23+
#define MLK_USE_NATIVE_POLY_COMPRESS_D4
24+
#define MLK_USE_NATIVE_POLY_COMPRESS_D5
25+
#define MLK_USE_NATIVE_POLY_COMPRESS_D10
26+
#define MLK_USE_NATIVE_POLY_COMPRESS_D11
2327

2428
#include "../mlkem/src/native/api.h"
2529

‎proofs/cbmc/poly_compress_d10/Makefile‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
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_compress_d10_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 = mlk_poly_compress_d10
12+
13+
DEFINES +=
14+
INCLUDES +=
15+
16+
REMOVE_FUNCTION_BODY +=
17+
UNWINDSET +=
18+
19+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20+
PROJECT_SOURCES += $(SRCDIR)/mlkem/src/compress.c
21+
22+
ifneq ($(MLKEM_K),4)
23+
CHECK_FUNCTION_CONTRACTS=mlk_poly_compress_d10
24+
USE_FUNCTION_CONTRACTS=mlk_poly_compress_d10_c
25+
else
26+
CHECK_FUNCTION_CONTRACTS=
27+
USE_FUNCTION_CONTRACTS=
28+
endif
29+
APPLY_LOOP_CONTRACTS=on
30+
USE_DYNAMIC_FRAMES=1
31+
32+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
33+
EXTERNAL_SAT_SOLVER=
34+
CBMCFLAGS=--bitwuzla
35+
36+
FUNCTION_NAME = mlk_poly_compress_d10
37+
38+
# If this proof is found to consume huge amounts of RAM, you can set the
39+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
40+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
41+
# documentation in Makefile.common under the "Job Pools" heading for details.
42+
# EXPENSIVE = true
43+
44+
# This function is large enough to need...
45+
CBMC_OBJECT_BITS = 8
46+
47+
include ../Makefile.common

‎proofs/cbmc/poly_compress_d10/poly_compress_d10_harness.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
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 "compress.h"
6+
7+
void harness(void)
8+
{
9+
#if MLKEM_K != 4
10+
uint8_t *r;
11+
mlk_poly *a;
12+
mlk_poly_compress_d10(r, a);
13+
#endif
14+
}

0 commit comments

Comments
 (0)