From 47c3fa6ed2659a9c7621bd14b96b78cf56d23f93 Mon Sep 17 00:00:00 2001 From: Becker Date: Wed, 22 Jan 2025 15:01:20 +0000 Subject: [PATCH 1/4] CBMC: Add contracts to native backend So far, the CBMC proofs covered the combination of C frontend and C backend. While most native backend functions are drop-in replacements of functions in the default C backend and should thus inherit their specification, there are minor differences in signature (in particular since #675) or functionality (e.g. the native implementation of rej_uniform may reject certain inputs, and the frontend uses fallback logic which is not present with the C backend) that merit explicit contract annotations for all functions in the arithmetic and FIPS202 backend, and proofs against those specs. This commit takes a step in this direction by adding CBMC contracts for all functions in the native arithmetic backend, except for `rej_uniform_native`, and proving that their call-sites still uphold their spec when the respective MLKEM_USE_NATIVE_XXX option is set. This is largely trivial, but it is still worth doing for (a) documentation purposes, and since (b) the native backends operate on raw arrays, while their call-sites operate in terms of the `poly_xxx` structs. The case of `rej_uniform` is more complicated and will be handled separately. Signed-off-by: Hanno Becker --- mlkem/native/api.h | 88 +++++++++++++++++-- proofs/cbmc/Makefile.common | 1 + proofs/cbmc/dummy_backend.h | 18 ++++ proofs/cbmc/dummy_backend_impl.h | 26 ++++++ proofs/cbmc/gen_matrix_native_order/Makefile | 54 ++++++++++++ .../gen_matrix_native_order/cbmc-proof.txt | 3 + .../gen_matrix_native_order_harness.c | 14 +++ proofs/cbmc/poly_frombytes_native/Makefile | 54 ++++++++++++ .../cbmc/poly_frombytes_native/cbmc-proof.txt | 3 + .../poly_frombytes_native_harness.c | 14 +++ .../cbmc/poly_invntt_tomont_native/Makefile | 54 ++++++++++++ .../poly_invntt_tomont_native/cbmc-proof.txt | 3 + .../poly_invntt_tomont_native_harness.c | 11 +++ .../poly_mulcache_compute_native/Makefile | 54 ++++++++++++ .../cbmc-proof.txt | 3 + .../poly_mulcache_compute_native_harness.c | 13 +++ proofs/cbmc/poly_ntt_native/Makefile | 54 ++++++++++++ proofs/cbmc/poly_ntt_native/cbmc-proof.txt | 3 + .../poly_ntt_native/poly_ntt_native_harness.c | 11 +++ proofs/cbmc/poly_reduce_native/Makefile | 54 ++++++++++++ proofs/cbmc/poly_reduce_native/cbmc-proof.txt | 3 + .../poly_reduce_native_harness.c | 13 +++ proofs/cbmc/poly_tobytes_native/Makefile | 54 ++++++++++++ .../cbmc/poly_tobytes_native/cbmc-proof.txt | 3 + .../poly_tobytes_native_harness.c | 14 +++ proofs/cbmc/poly_tomont_native/Makefile | 54 ++++++++++++ proofs/cbmc/poly_tomont_native/cbmc-proof.txt | 3 + .../poly_tomont_native_harness.c | 12 +++ .../Makefile | 54 ++++++++++++ .../cbmc-proof.txt | 3 + ...mul_acc_montgomery_cached_native_harness.c | 14 +++ 31 files changed, 753 insertions(+), 9 deletions(-) create mode 100644 proofs/cbmc/dummy_backend.h create mode 100644 proofs/cbmc/dummy_backend_impl.h create mode 100644 proofs/cbmc/gen_matrix_native_order/Makefile create mode 100644 proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt create mode 100644 proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c create mode 100644 proofs/cbmc/poly_frombytes_native/Makefile create mode 100644 proofs/cbmc/poly_frombytes_native/cbmc-proof.txt create mode 100644 proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c create mode 100644 proofs/cbmc/poly_invntt_tomont_native/Makefile create mode 100644 proofs/cbmc/poly_invntt_tomont_native/cbmc-proof.txt create mode 100644 proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c create mode 100644 proofs/cbmc/poly_mulcache_compute_native/Makefile create mode 100644 proofs/cbmc/poly_mulcache_compute_native/cbmc-proof.txt create mode 100644 proofs/cbmc/poly_mulcache_compute_native/poly_mulcache_compute_native_harness.c create mode 100644 proofs/cbmc/poly_ntt_native/Makefile create mode 100644 proofs/cbmc/poly_ntt_native/cbmc-proof.txt create mode 100644 proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c create mode 100644 proofs/cbmc/poly_reduce_native/Makefile create mode 100644 proofs/cbmc/poly_reduce_native/cbmc-proof.txt create mode 100644 proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c create mode 100644 proofs/cbmc/poly_tobytes_native/Makefile create mode 100644 proofs/cbmc/poly_tobytes_native/cbmc-proof.txt create mode 100644 proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c create mode 100644 proofs/cbmc/poly_tomont_native/Makefile create mode 100644 proofs/cbmc/poly_tomont_native/cbmc-proof.txt create mode 100644 proofs/cbmc/poly_tomont_native/poly_tomont_native_harness.c create mode 100644 proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/Makefile create mode 100644 proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/cbmc-proof.txt create mode 100644 proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c diff --git a/mlkem/native/api.h b/mlkem/native/api.h index 0704f9dcd..c39f63211 100644 --- a/mlkem/native/api.h +++ b/mlkem/native/api.h @@ -23,8 +23,15 @@ #define MLKEM_NATIVE_ARITH_NATIVE_API_H #include +#include "../cbmc.h" #include "../common.h" +/* Absolute exclusive upper bound for the output of the inverse NTT */ +#define INVNTT_BOUND (8 * MLKEM_Q) + +/* Absolute exclusive upper bound for the output of the forward NTT */ +#define NTT_BOUND (8 * MLKEM_Q) + /* * This is the C<->native interface allowing for the drop-in of * native code for performance critical arithmetic components of ML-KEM. @@ -66,7 +73,13 @@ * * Arguments: - int16_t p[MLKEM_N]: pointer to in/output polynomial **************************************************/ -static INLINE void ntt_native(int16_t p[MLKEM_N]); +static INLINE void ntt_native(int16_t p[MLKEM_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N)) + requires(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q)) + assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(p, 0, MLKEM_N, NTT_BOUND)) +); #endif /* MLKEM_USE_NATIVE_NTT */ #if defined(MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER) @@ -98,7 +111,14 @@ and to/from bytes conversions." * Arguments: - int16_t p[MLKEM_N]: pointer to in/output polynomial * **************************************************/ -static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]); +static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]) +__contract__( + /* We don't specify that this should be a permutation, but only + * that it does not change the bound established at the end of gen_matrix. */ + requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N)) + requires(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q))); #endif /* MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER */ #if defined(MLKEM_USE_NATIVE_INTT) @@ -116,7 +136,12 @@ static INLINE void poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]); * * Arguments: - uint16_t *a: pointer to in/output polynomial **************************************************/ -static INLINE void intt_native(int16_t p[MLKEM_N]); +static INLINE void intt_native(int16_t p[MLKEM_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(p, 0, MLKEM_N, INVNTT_BOUND)) +); #endif /* MLKEM_USE_NATIVE_INTT */ #if defined(MLKEM_USE_NATIVE_POLY_REDUCE) @@ -127,7 +152,12 @@ static INLINE void intt_native(int16_t p[MLKEM_N]); * * Arguments: - int16_t r[MLKEM_N]: pointer to input/output polynomial **************************************************/ -static INLINE void poly_reduce_native(int16_t p[MLKEM_N]); +static INLINE void poly_reduce_native(int16_t p[MLKEM_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(p, 0, MLKEM_N, 0, MLKEM_Q)) +); #endif /* MLKEM_USE_NATIVE_POLY_REDUCE */ #if defined(MLKEM_USE_NATIVE_POLY_TOMONT) @@ -139,7 +169,12 @@ static INLINE void poly_reduce_native(int16_t p[MLKEM_N]); * * Arguments: - int16_t r[MLKEM_N]: pointer to input/output polynomial **************************************************/ -static INLINE void poly_tomont_native(int16_t p[MLKEM_N]); +static INLINE void poly_tomont_native(int16_t p[MLKEM_N]) +__contract__( + requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(p, 0, MLKEM_N, MLKEM_Q)) +); #endif /* MLKEM_USE_NATIVE_POLY_TOMONT */ #if defined(MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE) @@ -165,7 +200,12 @@ static INLINE void poly_tomont_native(int16_t p[MLKEM_N]); * - cache: pointer to multiplication cache **************************************************/ static INLINE void poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2], - const int16_t poly[MLKEM_N]); + const int16_t poly[MLKEM_N]) +__contract__( + requires(memory_no_alias(cache, sizeof(int16_t) * (MLKEM_N / 2))) + requires(memory_no_alias(poly, sizeof(int16_t) * MLKEM_N)) + assigns(object_whole(cache)) +); #endif /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */ #if defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED) @@ -190,7 +230,25 @@ static INLINE void poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2], static INLINE void polyvec_basemul_acc_montgomery_cached_native( int16_t r[MLKEM_N], const int16_t a[MLKEM_K * MLKEM_N], const int16_t b[MLKEM_K * MLKEM_N], - const int16_t b_cache[MLKEM_K * (MLKEM_N / 2)]); + const int16_t b_cache[MLKEM_K * (MLKEM_N / 2)]) +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_K * MLKEM_N)) + requires(memory_no_alias(b, sizeof(int16_t) * MLKEM_K * MLKEM_N)) + requires(memory_no_alias(b_cache, sizeof(int16_t) * MLKEM_K * (MLKEM_N / 2))) + /* Because of https://github.com/diffblue/cbmc/issues/8570, we can't + * just use a single flattened array_bound(...) here. + * + * Once fixed, change to: + * ``` + * requires(array_bound(a, 0, MLKEM_K * MLKEM_N, 0, UINT12_LIMIT)) + * ``` + */ + requires(forall(kN, 0, MLKEM_K, \ + array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \ + 0, UINT12_LIMIT))) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) +); #endif #if defined(MLKEM_USE_NATIVE_POLY_TOBYTES) @@ -209,7 +267,13 @@ static INLINE void polyvec_basemul_acc_montgomery_cached_native( * (of MLKEM_POLYBYTES bytes) **************************************************/ static INLINE void poly_tobytes_native(uint8_t r[MLKEM_POLYBYTES], - const int16_t a[MLKEM_N]); + const int16_t a[MLKEM_N]) +__contract__( + requires(memory_no_alias(r, MLKEM_POLYBYTES)) + requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N)) + requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(object_whole(r)) +); #endif /* MLKEM_USE_NATIVE_POLY_TOBYTES */ #if defined(MLKEM_USE_NATIVE_POLY_FROMBYTES) @@ -227,7 +291,13 @@ static INLINE void poly_tobytes_native(uint8_t r[MLKEM_POLYBYTES], * (of MLKEM_POLYBYTES bytes) **************************************************/ static INLINE void poly_frombytes_native(int16_t a[MLKEM_N], - const uint8_t r[MLKEM_POLYBYTES]); + const uint8_t r[MLKEM_POLYBYTES]) +__contract__( + requires(memory_no_alias(r, MLKEM_POLYBYTES)) + requires(memory_no_alias(a, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(a, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(a, 0, MLKEM_N, 0, UINT12_LIMIT)) +); #endif /* MLKEM_USE_NATIVE_POLY_FROMBYTES */ #if defined(MLKEM_USE_NATIVE_REJ_UNIFORM) diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common index e9a2c3051..1dcd5fcfd 100644 --- a/proofs/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -321,6 +321,7 @@ ADD_LIBRARY_FLAG := --add-library # Preprocessor include paths -I... INCLUDES ?= INCLUDES += -I$(PROOFDIR) +INCLUDES += -I$(SRCDIR)/proofs/cbmc INCLUDES += -I$(SRCDIR)/mlkem INCLUDES += -I$(SRCDIR)/mlkem/fips202 diff --git a/proofs/cbmc/dummy_backend.h b/proofs/cbmc/dummy_backend.h new file mode 100644 index 000000000..76bf137c5 --- /dev/null +++ b/proofs/cbmc/dummy_backend.h @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_H + +#define MLKEM_NATIVE_ARITH_BACKEND_NAME DUMMY_BACKEND + +/* Filename of the C backend implementation. + * This is not inlined here because this header is included in assembly + * files as well. */ +#define MLKEM_NATIVE_ARITH_BACKEND_IMPL "dummy_backend_impl.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_H */ diff --git a/proofs/cbmc/dummy_backend_impl.h b/proofs/cbmc/dummy_backend_impl.h new file mode 100644 index 000000000..92485da2b --- /dev/null +++ b/proofs/cbmc/dummy_backend_impl.h @@ -0,0 +1,26 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +/* ML-KEM arithmetic native profile for clean assembly */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H + +#define MLKEM_USE_NATIVE_REJ_UNIFORM +#define MLKEM_USE_NATIVE_NTT +#define MLKEM_USE_NATIVE_INTT +#define MLKEM_USE_NATIVE_POLY_REDUCE +#define MLKEM_USE_NATIVE_POLY_TOMONT +#define MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED +#define MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE +#define MLKEM_USE_NATIVE_POLY_TOBYTES +#define MLKEM_USE_NATIVE_POLY_FROMBYTES +#define MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER + +#include "../mlkem/native/api.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */ diff --git a/proofs/cbmc/gen_matrix_native_order/Makefile b/proofs/cbmc/gen_matrix_native_order/Makefile new file mode 100644 index 000000000..17afb1133 --- /dev/null +++ b/proofs/cbmc/gen_matrix_native_order/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = gen_matrix_native_order_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = gen_matrix_native_order + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += $(MLKEM_NAMESPACE)gen_matrix.0:4 $(MLKEM_NAMESPACE)gen_matrix.1:4 $(MLKEM_NAMESPACE)gen_matrix.2:4 $(MLKEM_NAMESPACE)gen_matrix.3:4 $(MLKEM_NAMESPACE)gen_matrix.4:4 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform $(MLKEM_NAMESPACE)poly_rej_uniform_x4 poly_permute_bitrev_to_custom +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = $(MLKEM_NAMESPACE)gen_matrix_native_order + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt b/proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c b/proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c new file mode 100644 index 000000000..bef383b86 --- /dev/null +++ b/proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "indcpa.h" + +void harness(void) +{ + polyvec *a; + uint8_t *seed; + int transposed; + gen_matrix(a, seed, transposed); +} diff --git a/proofs/cbmc/poly_frombytes_native/Makefile b/proofs/cbmc/poly_frombytes_native/Makefile new file mode 100644 index 000000000..07ac7fe35 --- /dev/null +++ b/proofs/cbmc/poly_frombytes_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_frombytes_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_frombytes_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_frombytes +USE_FUNCTION_CONTRACTS=poly_frombytes_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = poly_frombytes_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_frombytes_native/cbmc-proof.txt b/proofs/cbmc/poly_frombytes_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/poly_frombytes_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c b/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c new file mode 100644 index 000000000..77c5f2d06 --- /dev/null +++ b/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include "compress.h" + +void harness(void) +{ + poly *a; + uint8_t *r; + + /* Contracts for this function are in poly.h */ + poly_frombytes(a, r); +} diff --git a/proofs/cbmc/poly_invntt_tomont_native/Makefile b/proofs/cbmc/poly_invntt_tomont_native/Makefile new file mode 100644 index 000000000..a72a91940 --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_invntt_tomont_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_invntt_tomont_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_invntt_tomont +USE_FUNCTION_CONTRACTS=intt_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_invntt_tomont_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 12 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_invntt_tomont_native/cbmc-proof.txt b/proofs/cbmc/poly_invntt_tomont_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c b/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c new file mode 100644 index 000000000..5d48b3eae --- /dev/null +++ b/proofs/cbmc/poly_invntt_tomont_native/poly_invntt_tomont_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include "poly.h" + +void harness(void) +{ + poly *p; + poly_invntt_tomont(p); +} diff --git a/proofs/cbmc/poly_mulcache_compute_native/Makefile b/proofs/cbmc/poly_mulcache_compute_native/Makefile new file mode 100644 index 000000000..642dbbaf9 --- /dev/null +++ b/proofs/cbmc/poly_mulcache_compute_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_mulcache_compute_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_mulcache_compute_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c $(SRCDIR)/mlkem/zetas.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_mulcache_compute +USE_FUNCTION_CONTRACTS=poly_mulcache_compute_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_mulcache_compute_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_mulcache_compute_native/cbmc-proof.txt b/proofs/cbmc/poly_mulcache_compute_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/poly_mulcache_compute_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/poly_mulcache_compute_native/poly_mulcache_compute_native_harness.c b/proofs/cbmc/poly_mulcache_compute_native/poly_mulcache_compute_native_harness.c new file mode 100644 index 000000000..7a90ed537 --- /dev/null +++ b/proofs/cbmc/poly_mulcache_compute_native/poly_mulcache_compute_native_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include "poly.h" + +void harness(void) +{ + poly_mulcache *x; + poly *a; + + poly_mulcache_compute(x, a); +} diff --git a/proofs/cbmc/poly_ntt_native/Makefile b/proofs/cbmc/poly_ntt_native/Makefile new file mode 100644 index 000000000..2f75237b3 --- /dev/null +++ b/proofs/cbmc/poly_ntt_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_ntt_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_ntt_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_ntt +USE_FUNCTION_CONTRACTS=ntt_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = poly_ntt + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_ntt_native/cbmc-proof.txt b/proofs/cbmc/poly_ntt_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/poly_ntt_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c b/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c new file mode 100644 index 000000000..333d34f63 --- /dev/null +++ b/proofs/cbmc/poly_ntt_native/poly_ntt_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + poly *a; + poly_ntt(a); +} diff --git a/proofs/cbmc/poly_reduce_native/Makefile b/proofs/cbmc/poly_reduce_native/Makefile new file mode 100644 index 000000000..89f341e5e --- /dev/null +++ b/proofs/cbmc/poly_reduce_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_reduce_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_reduce_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_reduce +USE_FUNCTION_CONTRACTS=poly_reduce_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = poly_reduce_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_reduce_native/cbmc-proof.txt b/proofs/cbmc/poly_reduce_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/poly_reduce_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c b/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c new file mode 100644 index 000000000..4b8f7be6a --- /dev/null +++ b/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c @@ -0,0 +1,13 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + poly *a; + + /* Contracts for this function are in poly.h */ + poly_reduce(a); +} diff --git a/proofs/cbmc/poly_tobytes_native/Makefile b/proofs/cbmc/poly_tobytes_native/Makefile new file mode 100644 index 000000000..7b9422450 --- /dev/null +++ b/proofs/cbmc/poly_tobytes_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_tobytes_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_tobytes_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/compress.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tobytes +USE_FUNCTION_CONTRACTS=poly_tobytes_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = poly_tobytes_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_tobytes_native/cbmc-proof.txt b/proofs/cbmc/poly_tobytes_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/poly_tobytes_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c b/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c new file mode 100644 index 000000000..de83a4d32 --- /dev/null +++ b/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include "compress.h" + +void harness(void) +{ + poly *a; + uint8_t *r; + + /* Contracts for this function are in poly.h */ + poly_tobytes(r, a); +} diff --git a/proofs/cbmc/poly_tomont_native/Makefile b/proofs/cbmc/poly_tomont_native/Makefile new file mode 100644 index 000000000..62cda6ce9 --- /dev/null +++ b/proofs/cbmc/poly_tomont_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_tomont_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = poly_tomont_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_tomont +USE_FUNCTION_CONTRACTS=poly_tomont_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = poly_tomont_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/poly_tomont_native/cbmc-proof.txt b/proofs/cbmc/poly_tomont_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/poly_tomont_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/poly_tomont_native/poly_tomont_native_harness.c b/proofs/cbmc/poly_tomont_native/poly_tomont_native_harness.c new file mode 100644 index 000000000..ee3acbd62 --- /dev/null +++ b/proofs/cbmc/poly_tomont_native/poly_tomont_native_harness.c @@ -0,0 +1,12 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include "poly.h" + +void harness(void) +{ + poly *a; + + poly_tomont(a); +} diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/Makefile new file mode 100644 index 000000000..5bf1e7697 --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyvec_basemul_acc_montgomery_cached_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = polyvec_basemul_acc_montgomery_cached_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly_k.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_basemul_acc_montgomery_cached +USE_FUNCTION_CONTRACTS=polyvec_basemul_acc_montgomery_cached_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = polyvec_basemul_acc_montgomery_cached_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 9 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/cbmc-proof.txt b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c new file mode 100644 index 000000000..3eb072c4e --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_native/polyvec_basemul_acc_montgomery_cached_native_harness.c @@ -0,0 +1,14 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +#include "poly_k.h" + +void harness(void) +{ + poly *r; + polyvec *a, *b; + polyvec_mulcache *b_cached; + + polyvec_basemul_acc_montgomery_cached(r, a, b, b_cached); +} From 1b2db0cc7b761330b23abc01e69cf48971b3c921 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 23 Jan 2025 04:29:25 +0000 Subject: [PATCH 2/4] Sampling: Change fallback logic to native implementation From a perspective of the native backend, the rejection sampling routine `rej_uniform` is special in that it is not expected to be replaced by native code in its entirety, but only in special cases. Outside of those special cases, the default C implementation is used. Previously, this fallback logic was implemented as follows: First, the native backend would be called. Upon success, the function would return immediately. Otherwise, it would fall back to the default implementation. Success/Failure would be communicated through a special return value -1. There are two problems with this logic: - It appears very difficult to reason about in CBMC: Specifically, when we call the native backend, we shift the input buffer by the amount of data that has already been successfully sampled, and CBMC struggles reasoning about that. - We call the native backend with a potentially unaligned buffer, which seems unnatural. This is not an issue for the existing backends, because their bounds checks ensure that the native implementation only takes effect at the beginning of rejection sampling, where the output buffer is aligned; yet, alignment is not guaranteed in general. This commit simplifies the fallback logic by invoking the native backend only upon the first call to `rej_uniform`, when no coefficients have yet been sampled. This solves both issues above. Signed-off-by: Hanno Becker --- mlkem/sampling.c | 37 +++++++++++++++---------------------- 1 file changed, 15 insertions(+), 22 deletions(-) diff --git a/mlkem/sampling.c b/mlkem/sampling.c index b448c24c3..caf822528 100644 --- a/mlkem/sampling.c +++ b/mlkem/sampling.c @@ -29,10 +29,10 @@ __contract__( requires(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0) requires(memory_no_alias(r, sizeof(int16_t) * target)) requires(memory_no_alias(buf, buflen)) - requires(offset > 0 ==> array_bound(r, 0, offset, 0, MLKEM_Q)) + requires(array_bound(r, 0, offset, 0, MLKEM_Q)) assigns(memory_slice(r, sizeof(int16_t) * target)) ensures(offset <= return_value && return_value <= target) - ensures(return_value > 0 ==> array_bound(r, 0, return_value, 0, MLKEM_Q)) + ensures(array_bound(r, 0, return_value, 0, MLKEM_Q)) ) { unsigned int ctr, pos; @@ -66,7 +66,6 @@ __contract__( return ctr; } -#if !defined(MLKEM_USE_NATIVE_REJ_UNIFORM) /************************************************* * Name: rej_uniform * @@ -87,7 +86,7 @@ __contract__( * Must be a multiple of 3. * * Note: Strictly speaking, only a few values of buflen near UINT_MAX need - * excluding. The limit of 4096 is somewhat arbitary but sufficient for all + * excluding. The limit of 128 is somewhat arbitary but sufficient for all * uses of this function. Similarly, the actual limit for target is UINT_MAX/2. * * Returns the new offset of sampled 16-bit integers, at most target, @@ -110,33 +109,27 @@ __contract__( requires(offset <= target && target <= 4096 && buflen <= 4096 && buflen % 3 == 0) requires(memory_no_alias(r, sizeof(int16_t) * target)) requires(memory_no_alias(buf, buflen)) - requires(offset > 0 ==> array_bound(r, 0, offset, 0, MLKEM_Q)) + requires(array_bound(r, 0, offset, 0, MLKEM_Q)) assigns(memory_slice(r, sizeof(int16_t) * target)) ensures(offset <= return_value && return_value <= target) - ensures(return_value > 0 ==> array_bound(r, 0, return_value, 0, MLKEM_Q)) + ensures(array_bound(r, 0, return_value, 0, MLKEM_Q)) ) { - return rej_uniform_scalar(r, target, offset, buf, buflen); -} -#else /* MLKEM_USE_NATIVE_REJ_UNIFORM */ -static unsigned int rej_uniform(int16_t *r, unsigned int target, - unsigned int offset, const uint8_t *buf, - unsigned int buflen) -{ - int ret; - - /* Sample from large buffer with full lane as much as possible. */ - ret = rej_uniform_native(r + offset, target - offset, buf, buflen); - if (ret != -1) +#if defined(MLKEM_USE_NATIVE_REJ_UNIFORM) + if (offset == 0) { - unsigned res = offset + (unsigned)ret; - debug_assert_bound(r, res, 0, MLKEM_Q); - return res; + int ret = rej_uniform_native(r, target, buf, buflen); + if (ret != -1) + { + unsigned res = (unsigned)ret; + debug_assert_bound(r, res, 0, MLKEM_Q); + return res; + } } +#endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */ return rej_uniform_scalar(r, target, offset, buf, buflen); } -#endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */ #ifndef MLKEM_GEN_MATRIX_NBLOCKS #define MLKEM_GEN_MATRIX_NBLOCKS \ From 801ac7833564125a53b7f528f7b983d323bbffae Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 23 Jan 2025 04:36:57 +0000 Subject: [PATCH 3/4] CBMC: Add contract for native `rej_uniform` and prove fallback logic This commit adds a contract for the rejection sampling backend and proves the C implementation correct on the basis of that contract. Signed-off-by: Hanno Becker --- mlkem/native/api.h | 10 +++- proofs/cbmc/rej_uniform_native/Makefile | 56 +++++++++++++++++++ proofs/cbmc/rej_uniform_native/cbmc-proof.txt | 3 + .../rej_uniform_native_harness.c | 19 +++++++ 4 files changed, 87 insertions(+), 1 deletion(-) create mode 100644 proofs/cbmc/rej_uniform_native/Makefile create mode 100644 proofs/cbmc/rej_uniform_native/cbmc-proof.txt create mode 100644 proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c diff --git a/mlkem/native/api.h b/mlkem/native/api.h index c39f63211..def32be36 100644 --- a/mlkem/native/api.h +++ b/mlkem/native/api.h @@ -319,7 +319,15 @@ __contract__( * len). **************************************************/ static INLINE int rej_uniform_native(int16_t *r, unsigned int len, - const uint8_t *buf, unsigned int buflen); + const uint8_t *buf, unsigned int buflen) +__contract__( + requires(len <= 4096 && buflen <= 4096 && buflen % 3 == 0) + requires(memory_no_alias(r, sizeof(int16_t) * len)) + requires(memory_no_alias(buf, buflen)) + assigns(memory_slice(r, sizeof(int16_t) * len)) + ensures(return_value == -1 || (0 <= return_value && return_value <= len)) + ensures(return_value != -1 ==> array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q)) +); #endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */ #endif /* MLKEM_NATIVE_ARITH_NATIVE_API_H */ diff --git a/proofs/cbmc/rej_uniform_native/Makefile b/proofs/cbmc/rej_uniform_native/Makefile new file mode 100644 index 000000000..013c1bc6c --- /dev/null +++ b/proofs/cbmc/rej_uniform_native/Makefile @@ -0,0 +1,56 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = rej_uniform_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = rej_uniform_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/sampling.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)rej_uniform +USE_FUNCTION_CONTRACTS=rej_uniform_native $(MLKEM_NAMESPACE)rej_uniform_scalar +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +#CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula + +FUNCTION_NAME = rej_uniform_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/rej_uniform_native/cbmc-proof.txt b/proofs/cbmc/rej_uniform_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/rej_uniform_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c b/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c new file mode 100644 index 000000000..eccac7a54 --- /dev/null +++ b/proofs/cbmc/rej_uniform_native/rej_uniform_native_harness.c @@ -0,0 +1,19 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" + +#define rej_uniform MLKEM_NAMESPACE(rej_uniform) +unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset, + const uint8_t *buf, unsigned int buflen); + +void harness(void) +{ + unsigned int target, offset, inlen; + int16_t *r; + uint8_t *buf; + + rej_uniform(r, target, offset, buf, inlen); +} From 1d4fc1f9841df485a5e5c14718ef6431c835c2e9 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 23 Jan 2025 05:01:07 +0000 Subject: [PATCH 4/4] CBMC: Add KeccakF1600[x4]_StatePermute proofs based on native code This commit adds CBMC specifications to the FIPS202 backend API and proves the functions depending on it -- KeccakF1600_StatePermute and KeccakF1600x4_StatePermute -- memory-safe with respect to those specifications. Since the logic implementing KeccakF1600x4_StatePermute in the presence of a FIPS202 backend depends on whether x1/x2/x4-batched Keccak is present in the native backend, we provide 3 dummy FIPS202 backends for each case. Signed-off-by: Hanno Becker --- mlkem/fips202/native/api.h | 15 ++++-- mlkem/native/api.h | 10 +++- .../KeccakF1600_StatePermute_native_harness.c | 11 ++++ .../KeccakF1600_StatePermute_native/Makefile | 54 +++++++++++++++++++ .../cbmc-proof.txt | 0 ...akF1600x4_StatePermute_native_x2_harness.c | 11 ++++ .../Makefile | 54 +++++++++++++++++++ .../cbmc-proof.txt | 3 ++ ...akF1600x4_StatePermute_native_x4_harness.c | 11 ++++ .../Makefile | 54 +++++++++++++++++++ .../cbmc-proof.txt | 3 ++ proofs/cbmc/dummy_backend_fips202_x1.h | 18 +++++++ proofs/cbmc/dummy_backend_fips202_x1_impl.h | 17 ++++++ proofs/cbmc/dummy_backend_fips202_x2.h | 18 +++++++ proofs/cbmc/dummy_backend_fips202_x2_impl.h | 17 ++++++ proofs/cbmc/dummy_backend_fips202_x4.h | 18 +++++++ proofs/cbmc/dummy_backend_fips202_x4_impl.h | 17 ++++++ proofs/cbmc/gen_matrix_native/Makefile | 54 +++++++++++++++++++ .../Makefile => gen_matrix_native/Makefile~} | 0 proofs/cbmc/gen_matrix_native/cbmc-proof.txt | 3 ++ .../gen_matrix_native_harness.c} | 0 .../poly_frombytes/poly_frombytes_harness.c | 2 +- .../poly_frombytes_native_harness.c | 2 +- .../poly_reduce_native_harness.c | 2 +- .../cbmc/poly_tobytes/poly_tobytes_harness.c | 2 +- .../poly_tobytes_native_harness.c | 2 +- proofs/cbmc/poly_tomsg/poly_tomsg_harness.c | 2 +- .../scalar_compress_d1_harness.c | 2 +- .../scalar_compress_d10_harness.c | 2 +- .../scalar_compress_d11_harness.c | 2 +- .../scalar_compress_d4_harness.c | 2 +- .../scalar_compress_d5_harness.c | 2 +- 32 files changed, 394 insertions(+), 16 deletions(-) create mode 100644 proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c create mode 100644 proofs/cbmc/KeccakF1600_StatePermute_native/Makefile rename proofs/cbmc/{gen_matrix_native_order => KeccakF1600_StatePermute_native}/cbmc-proof.txt (100%) create mode 100644 proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c create mode 100644 proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/Makefile create mode 100644 proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/cbmc-proof.txt create mode 100644 proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/KeccakF1600x4_StatePermute_native_x4_harness.c create mode 100644 proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/Makefile create mode 100644 proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/cbmc-proof.txt create mode 100644 proofs/cbmc/dummy_backend_fips202_x1.h create mode 100644 proofs/cbmc/dummy_backend_fips202_x1_impl.h create mode 100644 proofs/cbmc/dummy_backend_fips202_x2.h create mode 100644 proofs/cbmc/dummy_backend_fips202_x2_impl.h create mode 100644 proofs/cbmc/dummy_backend_fips202_x4.h create mode 100644 proofs/cbmc/dummy_backend_fips202_x4_impl.h create mode 100644 proofs/cbmc/gen_matrix_native/Makefile rename proofs/cbmc/{gen_matrix_native_order/Makefile => gen_matrix_native/Makefile~} (100%) create mode 100644 proofs/cbmc/gen_matrix_native/cbmc-proof.txt rename proofs/cbmc/{gen_matrix_native_order/gen_matrix_native_order_harness.c => gen_matrix_native/gen_matrix_native_harness.c} (100%) diff --git a/mlkem/fips202/native/api.h b/mlkem/fips202/native/api.h index cd4149b0b..123cb9761 100644 --- a/mlkem/fips202/native/api.h +++ b/mlkem/fips202/native/api.h @@ -32,13 +32,22 @@ */ #if defined(MLKEM_USE_FIPS202_X1_NATIVE) -static INLINE void keccak_f1600_x1_native(uint64_t *state); +static INLINE void keccak_f1600_x1_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))); #endif #if defined(MLKEM_USE_FIPS202_X2_NATIVE) -static INLINE void keccak_f1600_x2_native(uint64_t *state); +static INLINE void keccak_f1600_x2_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))); #endif #if defined(MLKEM_USE_FIPS202_X4_NATIVE) -static INLINE void keccak_f1600_x4_native(uint64_t *state); +static INLINE void keccak_f1600_x4_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))); #endif #endif /* MLKEM_NATIVE_FIPS202_NATIVE_API_H */ diff --git a/mlkem/native/api.h b/mlkem/native/api.h index def32be36..fd69d4737 100644 --- a/mlkem/native/api.h +++ b/mlkem/native/api.h @@ -26,10 +26,16 @@ #include "../cbmc.h" #include "../common.h" -/* Absolute exclusive upper bound for the output of the inverse NTT */ +/* Absolute exclusive upper bound for the output of the inverse NTT + * + * NOTE: This is the same bound as in poly.h and has to be kept + * in sync. */ #define INVNTT_BOUND (8 * MLKEM_Q) -/* Absolute exclusive upper bound for the output of the forward NTT */ +/* Absolute exclusive upper bound for the output of the forward NTT + * + * NOTE: This is the same bound as in poly.h and has to be kept + * in sync. */ #define NTT_BOUND (8 * MLKEM_Q) /* diff --git a/proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c b/proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c new file mode 100644 index 000000000..87e0c15cb --- /dev/null +++ b/proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + KeccakF1600_StatePermute(s); +} diff --git a/proofs/cbmc/KeccakF1600_StatePermute_native/Makefile b/proofs/cbmc/KeccakF1600_StatePermute_native/Makefile new file mode 100644 index 000000000..103fa0cf1 --- /dev/null +++ b/proofs/cbmc/KeccakF1600_StatePermute_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = KeccakF1600_StatePermute_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = KeccakF1600_StatePermute_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_FIPS202 -DMLKEM_NATIVE_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x1.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StatePermute +USE_FUNCTION_CONTRACTS=keccak_f1600_x1_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StatePermute_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StatePermute_native/cbmc-proof.txt similarity index 100% rename from proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600_StatePermute_native/cbmc-proof.txt diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c new file mode 100644 index 000000000..021a10309 --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + KeccakF1600x4_StatePermute(s); +} diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/Makefile b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/Makefile new file mode 100644 index 000000000..e46673cbf --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = KeccakF1600x4_StatePermute_native_x2_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = KeccakF1600x4_StatePermute_native_x2 + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_FIPS202 -DMLKEM_NATIVE_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x2.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute +USE_FUNCTION_CONTRACTS=keccak_f1600_x2_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = KeccakF1600x4_StatePermute_native_x2 + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/cbmc-proof.txt b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/KeccakF1600x4_StatePermute_native_x4_harness.c b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/KeccakF1600x4_StatePermute_native_x4_harness.c new file mode 100644 index 000000000..021a10309 --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/KeccakF1600x4_StatePermute_native_x4_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + KeccakF1600x4_StatePermute(s); +} diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/Makefile b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/Makefile new file mode 100644 index 000000000..305f0f768 --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = KeccakF1600x4_StatePermute_native_x4_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = KeccakF1600x4_StatePermute_native_x4 + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_FIPS202 -DMLKEM_NATIVE_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x4.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute +USE_FUNCTION_CONTRACTS=keccak_f1600_x4_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = KeccakF1600x4_StatePermute_native_x4 + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/cbmc-proof.txt b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/dummy_backend_fips202_x1.h b/proofs/cbmc/dummy_backend_fips202_x1.h new file mode 100644 index 000000000..535386357 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x1.h @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#ifdef MLKEM_NATIVE_FIPS202_PROFILE_H +#error Only one MLKEM_FIPS202 assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_FIPS202_PROFILE_H + +#define MLKEM_NATIVE_FIPS202_BACKEND_NAME DUMMY_BACKEND_FIPS202_X1 + +/* Filename of the C backend implementation. + * This is not inlined here because this header is included in assembly + * files as well. */ +#define MLKEM_NATIVE_FIPS202_BACKEND_IMPL "dummy_backend_fips202_x1_impl.h" + +#endif /* MLKEM_NATIVE_FIPS202_PROFILE_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x1_impl.h b/proofs/cbmc/dummy_backend_fips202_x1_impl.h new file mode 100644 index 000000000..695f7a682 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x1_impl.h @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +/* ML-KEM arithmetic native profile for clean assembly */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H + +#define MLKEM_USE_FIPS202_X1_NATIVE + +#include "../mlkem/fips202/native/api.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x2.h b/proofs/cbmc/dummy_backend_fips202_x2.h new file mode 100644 index 000000000..1d7f340d7 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x2.h @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#ifdef MLKEM_NATIVE_FIPS202_PROFILE_H +#error Only one MLKEM_FIPS202 assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_FIPS202_PROFILE_H + +#define MLKEM_NATIVE_FIPS202_BACKEND_NAME DUMMY_BACKEND_FIPS202_X2 + +/* Filename of the C backend implementation. + * This is not inlined here because this header is included in assembly + * files as well. */ +#define MLKEM_NATIVE_FIPS202_BACKEND_IMPL "dummy_backend_fips202_x2_impl.h" + +#endif /* MLKEM_NATIVE_FIPS202_PROFILE_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x2_impl.h b/proofs/cbmc/dummy_backend_fips202_x2_impl.h new file mode 100644 index 000000000..4978ec495 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x2_impl.h @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +/* ML-KEM arithmetic native profile for clean assembly */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H + +#define MLKEM_USE_FIPS202_X2_NATIVE + +#include "../mlkem/fips202/native/api.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x4.h b/proofs/cbmc/dummy_backend_fips202_x4.h new file mode 100644 index 000000000..58994f1b9 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x4.h @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#ifdef MLKEM_NATIVE_FIPS202_PROFILE_H +#error Only one MLKEM_FIPS202 assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_FIPS202_PROFILE_H + +#define MLKEM_NATIVE_FIPS202_BACKEND_NAME DUMMY_BACKEND_FIPS202_X2 + +/* Filename of the C backend implementation. + * This is not inlined here because this header is included in assembly + * files as well. */ +#define MLKEM_NATIVE_FIPS202_BACKEND_IMPL "dummy_backend_fips202_x4_impl.h" + +#endif /* MLKEM_NATIVE_FIPS202_PROFILE_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x4_impl.h b/proofs/cbmc/dummy_backend_fips202_x4_impl.h new file mode 100644 index 000000000..11d4ffad0 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x4_impl.h @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +/* ML-KEM arithmetic native profile for clean assembly */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H + +#define MLKEM_USE_FIPS202_X4_NATIVE + +#include "../mlkem/fips202/native/api.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */ diff --git a/proofs/cbmc/gen_matrix_native/Makefile b/proofs/cbmc/gen_matrix_native/Makefile new file mode 100644 index 000000000..640048d09 --- /dev/null +++ b/proofs/cbmc/gen_matrix_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = gen_matrix_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = gen_matrix_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += $(MLKEM_NAMESPACE)gen_matrix.0:4 $(MLKEM_NAMESPACE)gen_matrix.1:4 $(MLKEM_NAMESPACE)gen_matrix.2:4 $(MLKEM_NAMESPACE)gen_matrix.3:4 $(MLKEM_NAMESPACE)gen_matrix.4:4 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform $(MLKEM_NAMESPACE)poly_rej_uniform_x4 poly_permute_bitrev_to_custom +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = $(MLKEM_NAMESPACE)gen_matrix_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/gen_matrix_native_order/Makefile b/proofs/cbmc/gen_matrix_native/Makefile~ similarity index 100% rename from proofs/cbmc/gen_matrix_native_order/Makefile rename to proofs/cbmc/gen_matrix_native/Makefile~ diff --git a/proofs/cbmc/gen_matrix_native/cbmc-proof.txt b/proofs/cbmc/gen_matrix_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/gen_matrix_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c b/proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c similarity index 100% rename from proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c rename to proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c diff --git a/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c b/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c index 77c5f2d06..e9a740d2c 100644 --- a/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c +++ b/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_frombytes(a, r); } diff --git a/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c b/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c index 77c5f2d06..e9a740d2c 100644 --- a/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c +++ b/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_frombytes(a, r); } diff --git a/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c b/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c index 4b8f7be6a..571e75e3f 100644 --- a/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c +++ b/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c @@ -8,6 +8,6 @@ void harness(void) { poly *a; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_reduce(a); } diff --git a/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c b/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c index de83a4d32..1c17d81e3 100644 --- a/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c +++ b/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_tobytes(r, a); } diff --git a/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c b/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c index de83a4d32..1c17d81e3 100644 --- a/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c +++ b/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_tobytes(r, a); } diff --git a/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c b/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c index 36c56d0f5..16b66b91a 100644 --- a/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c +++ b/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *msg; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_tomsg(msg, a); } diff --git a/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c b/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c index 42fb73a8c..27c77d4b2 100644 --- a/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c +++ b/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d1(u); } diff --git a/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c b/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c index a84b36af2..708232706 100644 --- a/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c +++ b/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d10(u); } diff --git a/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c b/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c index 56dfc4913..c5b01ef5f 100644 --- a/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c +++ b/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d11(u); } diff --git a/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c b/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c index 4ac18801c..b7465fe4f 100644 --- a/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c +++ b/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d4(u); } diff --git a/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c b/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c index 6c50800ec..61c892732 100644 --- a/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c +++ b/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d5(u); }