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 0704f9dcd..fd69d4737 100644 --- a/mlkem/native/api.h +++ b/mlkem/native/api.h @@ -23,8 +23,21 @@ #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 + * + * 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 + * + * NOTE: This is the same bound as in poly.h and has to be kept + * in sync. */ +#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 +79,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 +117,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 +142,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 +158,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 +175,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 +206,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 +236,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 +273,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 +297,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) @@ -249,7 +325,15 @@ static INLINE void poly_frombytes_native(int16_t a[MLKEM_N], * 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/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 \ 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/KeccakF1600_StatePermute_native/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StatePermute_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/KeccakF1600_StatePermute_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/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/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_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/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/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/Makefile~ b/proofs/cbmc/gen_matrix_native/Makefile~ new file mode 100644 index 000000000..17afb1133 --- /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_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/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/gen_matrix_native_harness.c b/proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c new file mode 100644 index 000000000..bef383b86 --- /dev/null +++ b/proofs/cbmc/gen_matrix_native/gen_matrix_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 +#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/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/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..e9a740d2c --- /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 compress.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..571e75e3f --- /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 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/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..1c17d81e3 --- /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 compress.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/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/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); +} 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); +} 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); }