diff --git a/dev/x86_64/src/arith_native_x86_64.h b/dev/x86_64/src/arith_native_x86_64.h index 53422427a1..386b630063 100644 --- a/dev/x86_64/src/arith_native_x86_64.h +++ b/dev/x86_64/src/arith_native_x86_64.h @@ -7,65 +7,179 @@ #include "../../../common.h" -#include #include #include "consts.h" #define MLK_AVX2_REJ_UNIFORM_BUFLEN \ (3 * 168) /* REJ_UNIFORM_NBLOCKS * SHAKE128_RATE */ -#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm) -uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen, - const uint8_t *table); - #define mlk_rej_uniform_table MLK_NAMESPACE(rej_uniform_table) extern const uint8_t mlk_rej_uniform_table[]; +#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm) +uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen, + const uint8_t *table) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml. */ +__contract__( + requires(buflen % 12 == 0) + requires(memory_no_alias(buf, buflen)) + requires(table == mlk_rej_uniform_table) + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(return_value <= MLKEM_N) + ensures(array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q)) +); + #define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2) -void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata); +void mlk_ntt_avx2(int16_t *r, const int16_t *qdata) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_ntt.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(array_abs_bound(r, 0, MLKEM_N, 8192)) + requires(qdata == mlk_qdata) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + /* check-magic: off */ + ensures(array_abs_bound(r, 0, MLKEM_N, 23595)) + /* check-magic: on */ +); #define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2) -void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata); +void mlk_invntt_avx2(int16_t *r, const int16_t *qdata) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_intt.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(qdata == mlk_qdata) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + /* check-magic: off */ + ensures(array_abs_bound(r, 0, MLKEM_N, 26632)) + /* check-magic: on */ +); #define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2) -void mlk_nttunpack_avx2(int16_t *r); +void mlk_nttunpack_avx2(int16_t *r) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_unpack.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q)) +); #define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2) -void mlk_reduce_avx2(int16_t *r); +void mlk_reduce_avx2(int16_t *r) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_reduce.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q)) +); #define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2) void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in, - const int16_t *mlk_qdata); + const int16_t *qdata) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml */ +__contract__( + requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2))) + requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N)) + requires(qdata == mlk_qdata) + assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2))) + ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329)) +); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2) void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r, const int16_t *a, const int16_t *b, - const int16_t *b_cache); + const int16_t *b_cache) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N)) + requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N)) + requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2))) + requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) +); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3) void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r, const int16_t *a, const int16_t *b, - const int16_t *b_cache); + const int16_t *b_cache) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N)) + requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N)) + requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2))) + requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) +); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4) void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r, const int16_t *a, const int16_t *b, - const int16_t *b_cache); + const int16_t *b_cache) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N)) + requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N)) + requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2))) + requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) +); #define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2) -void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a); +void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml. + */ +__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)) +); #define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2) -void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a); +void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml. + */ +__contract__( + requires(memory_no_alias(a, MLKEM_POLYBYTES)) + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)) +); #define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2) -void mlk_tomont_avx2(int16_t *r); +void mlk_tomont_avx2(int16_t *r) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_tomont.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, 3329)) +); #define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2) void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], diff --git a/mlkem/src/native/x86_64/src/arith_native_x86_64.h b/mlkem/src/native/x86_64/src/arith_native_x86_64.h index 0df5f021b1..47aafbd0d4 100644 --- a/mlkem/src/native/x86_64/src/arith_native_x86_64.h +++ b/mlkem/src/native/x86_64/src/arith_native_x86_64.h @@ -7,65 +7,179 @@ #include "../../../common.h" -#include #include #include "consts.h" #define MLK_AVX2_REJ_UNIFORM_BUFLEN \ (3 * 168) /* REJ_UNIFORM_NBLOCKS * SHAKE128_RATE */ -#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm) -uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen, - const uint8_t *table); - #define mlk_rej_uniform_table MLK_NAMESPACE(rej_uniform_table) extern const uint8_t mlk_rej_uniform_table[]; +#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm) +uint64_t mlk_rej_uniform_asm(int16_t *r, const uint8_t *buf, unsigned buflen, + const uint8_t *table) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml. */ +__contract__( + requires(buflen % 12 == 0) + requires(memory_no_alias(buf, buflen)) + requires(table == mlk_rej_uniform_table) + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(return_value <= MLKEM_N) + ensures(array_bound(r, 0, (unsigned) return_value, 0, MLKEM_Q)) +); + #define mlk_ntt_avx2 MLK_NAMESPACE(ntt_avx2) -void mlk_ntt_avx2(int16_t *r, const int16_t *mlk_qdata); +void mlk_ntt_avx2(int16_t *r, const int16_t *qdata) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_ntt.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(array_abs_bound(r, 0, MLKEM_N, 8192)) + requires(qdata == mlk_qdata) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + /* check-magic: off */ + ensures(array_abs_bound(r, 0, MLKEM_N, 23595)) + /* check-magic: on */ +); #define mlk_invntt_avx2 MLK_NAMESPACE(invntt_avx2) -void mlk_invntt_avx2(int16_t *r, const int16_t *mlk_qdata); +void mlk_invntt_avx2(int16_t *r, const int16_t *qdata) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_intt.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(qdata == mlk_qdata) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + /* check-magic: off */ + ensures(array_abs_bound(r, 0, MLKEM_N, 26632)) + /* check-magic: on */ +); #define mlk_nttunpack_avx2 MLK_NAMESPACE(nttunpack_avx2) -void mlk_nttunpack_avx2(int16_t *r); +void mlk_nttunpack_avx2(int16_t *r) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_unpack.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q)) +); #define mlk_reduce_avx2 MLK_NAMESPACE(reduce_avx2) -void mlk_reduce_avx2(int16_t *r); +void mlk_reduce_avx2(int16_t *r) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_reduce.ml */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q)) +); #define mlk_poly_mulcache_compute_avx2 MLK_NAMESPACE(poly_mulcache_compute_avx2) void mlk_poly_mulcache_compute_avx2(int16_t *out, const int16_t *in, - const int16_t *mlk_qdata); + const int16_t *qdata) +/* This must be kept in sync with the HOL-Light specification + * in proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml */ +__contract__( + requires(memory_no_alias(out, sizeof(int16_t) * (MLKEM_N / 2))) + requires(memory_no_alias(in, sizeof(int16_t) * MLKEM_N)) + requires(qdata == mlk_qdata) + assigns(memory_slice(out, sizeof(int16_t) * (MLKEM_N / 2))) + ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329)) +); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 \ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k2) void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(int16_t *r, const int16_t *a, const int16_t *b, - const int16_t *b_cache); + const int16_t *b_cache) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N)) + requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N)) + requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2))) + requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) +); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k3) void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(int16_t *r, const int16_t *a, const int16_t *b, - const int16_t *b_cache); + const int16_t *b_cache) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N)) + requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N)) + requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2))) + requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) +); #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \ MLK_NAMESPACE(polyvec_basemul_acc_montgomery_cached_asm_k4) void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(int16_t *r, const int16_t *a, const int16_t *b, - const int16_t *b_cache); + const int16_t *b_cache) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N)) + requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N)) + requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2))) + requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) +); #define mlk_ntttobytes_avx2 MLK_NAMESPACE(ntttobytes_avx2) -void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a); +void mlk_ntttobytes_avx2(uint8_t *r, const int16_t *a) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml. + */ +__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)) +); #define mlk_nttfrombytes_avx2 MLK_NAMESPACE(nttfrombytes_avx2) -void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a); +void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml. + */ +__contract__( + requires(memory_no_alias(a, MLKEM_POLYBYTES)) + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)) +); #define mlk_tomont_avx2 MLK_NAMESPACE(tomont_avx2) -void mlk_tomont_avx2(int16_t *r); +void mlk_tomont_avx2(int16_t *r) +/* This must be kept in sync with the HOL-Light specification in + * proofs/hol_light/x86_64/proofs/mlkem_tomont.ml. + */ +__contract__( + requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N)) + assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N)) + ensures(array_abs_bound(r, 0, MLKEM_N, 3329)) +); #define mlk_poly_compress_d4_avx2 MLK_NAMESPACE(poly_compress_d4_avx2) void mlk_poly_compress_d4_avx2(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_D4], diff --git a/proofs/cbmc/intt_native_x86_64/Makefile b/proofs/cbmc/intt_native_x86_64/Makefile new file mode 100644 index 0000000000..bd548fecd4 --- /dev/null +++ b/proofs/cbmc/intt_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = intt_native_x86_64_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 = intt_native_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly.c $(SRCDIR)/mlkem/src/native/x86_64/src/consts.c + +CHECK_FUNCTION_CONTRACTS=mlk_intt_native +USE_FUNCTION_CONTRACTS=mlk_invntt_avx2 mlk_sys_check_capability +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 = intt_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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/intt_native_x86_64/intt_native_x86_64_harness.c b/proofs/cbmc/intt_native_x86_64/intt_native_x86_64_harness.c new file mode 100644 index 0000000000..b13e673c08 --- /dev/null +++ b/proofs/cbmc/intt_native_x86_64/intt_native_x86_64_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" +#include "params.h" + +int mlk_intt_native(int16_t data[MLKEM_N]); + +void harness(void) +{ + int16_t *r; + int t; + t = mlk_intt_native(r); +} diff --git a/proofs/cbmc/ntt_native_x86_64/Makefile b/proofs/cbmc/ntt_native_x86_64/Makefile new file mode 100644 index 0000000000..f163aff9aa --- /dev/null +++ b/proofs/cbmc/ntt_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = ntt_native_x86_64_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 = ntt_native_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly.c $(SRCDIR)/mlkem/src/native/x86_64/src/consts.c + +CHECK_FUNCTION_CONTRACTS=mlk_ntt_native +USE_FUNCTION_CONTRACTS=mlk_ntt_avx2 mlk_sys_check_capability +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 = ntt_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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/ntt_native_x86_64/ntt_native_x86_64_harness.c b/proofs/cbmc/ntt_native_x86_64/ntt_native_x86_64_harness.c new file mode 100644 index 0000000000..3ebcc34701 --- /dev/null +++ b/proofs/cbmc/ntt_native_x86_64/ntt_native_x86_64_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" +#include "params.h" + +int mlk_ntt_native(int16_t data[MLKEM_N]); + +void harness(void) +{ + int16_t *r; + int t; + t = mlk_ntt_native(r); +} diff --git a/proofs/cbmc/nttunpack_native_x86_64/Makefile b/proofs/cbmc/nttunpack_native_x86_64/Makefile new file mode 100644 index 0000000000..2f6ab0aa0c --- /dev/null +++ b/proofs/cbmc/nttunpack_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = nttunpack_native_x86_64_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 = nttunpack_native_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/indcpa.c + +CHECK_FUNCTION_CONTRACTS=mlk_poly_permute_bitrev_to_custom +USE_FUNCTION_CONTRACTS=mlk_nttunpack_avx2 mlk_sys_check_capability +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 = nttunpack_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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/nttunpack_native_x86_64/nttunpack_native_x86_64_harness.c b/proofs/cbmc/nttunpack_native_x86_64/nttunpack_native_x86_64_harness.c new file mode 100644 index 0000000000..85871b8970 --- /dev/null +++ b/proofs/cbmc/nttunpack_native_x86_64/nttunpack_native_x86_64_harness.c @@ -0,0 +1,20 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include +#include "cbmc.h" +#include "params.h" + +void mlk_poly_permute_bitrev_to_custom(int16_t p[MLKEM_N]); + +void harness(void) +{ + { + /* Dummy use of `free` to work around CBMC issue #8814. */ + free(NULL); + } + int16_t *r; + mlk_poly_permute_bitrev_to_custom(r); +} diff --git a/proofs/cbmc/poly_frombytes_native_x86_64/Makefile b/proofs/cbmc/poly_frombytes_native_x86_64/Makefile new file mode 100644 index 0000000000..7205738d51 --- /dev/null +++ b/proofs/cbmc/poly_frombytes_native_x86_64/Makefile @@ -0,0 +1,55 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_frombytes_native_x86_64_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_x86_64 + +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/compress.c + +CHECK_FUNCTION_CONTRACTS=mlk_poly_frombytes_native +USE_FUNCTION_CONTRACTS=mlk_nttfrombytes_avx2 mlk_sys_check_capability +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_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_x86_64/poly_frombytes_native_x86_64_harness.c b/proofs/cbmc/poly_frombytes_native_x86_64/poly_frombytes_native_x86_64_harness.c new file mode 100644 index 0000000000..ea5eb789e5 --- /dev/null +++ b/proofs/cbmc/poly_frombytes_native_x86_64/poly_frombytes_native_x86_64_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include "compress.h" + +int mlk_poly_frombytes_native(int16_t r[MLKEM_N], + const uint8_t a[MLKEM_POLYBYTES]); + +void harness(void) +{ + uint16_t *r; + uint8_t *a; + int t; + t = mlk_poly_frombytes_native(r, a); +} diff --git a/proofs/cbmc/poly_mulcache_compute_native_x86_64/Makefile b/proofs/cbmc/poly_mulcache_compute_native_x86_64/Makefile new file mode 100644 index 0000000000..7dc78ca5ed --- /dev/null +++ b/proofs/cbmc/poly_mulcache_compute_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_mulcache_compute_native_x86_64_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_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly.c $(SRCDIR)/mlkem/src/native/x86_64/src/consts.c + +CHECK_FUNCTION_CONTRACTS=mlk_poly_mulcache_compute_native +USE_FUNCTION_CONTRACTS=mlk_poly_mulcache_compute_avx2 mlk_sys_check_capability +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_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_x86_64/poly_mulcache_compute_native_x86_64_harness.c b/proofs/cbmc/poly_mulcache_compute_native_x86_64/poly_mulcache_compute_native_x86_64_harness.c new file mode 100644 index 0000000000..8ebabb1e32 --- /dev/null +++ b/proofs/cbmc/poly_mulcache_compute_native_x86_64/poly_mulcache_compute_native_x86_64_harness.c @@ -0,0 +1,17 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" +#include "params.h" + +int mlk_poly_mulcache_compute_native(int16_t cache[MLKEM_N / 2], + const int16_t mlk_poly[MLKEM_N]); + +void harness(void) +{ + int16_t *r, *c; + int t; + t = mlk_poly_mulcache_compute_native(c, r); +} diff --git a/proofs/cbmc/poly_reduce_native_x86_64/Makefile b/proofs/cbmc/poly_reduce_native_x86_64/Makefile new file mode 100644 index 0000000000..9e2ff7e18d --- /dev/null +++ b/proofs/cbmc/poly_reduce_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_reduce_native_x86_64_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_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mlk_poly_reduce_native +USE_FUNCTION_CONTRACTS=mlk_reduce_avx2 mlk_sys_check_capability +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_reduce_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_x86_64/poly_reduce_native_x86_64_harness.c b/proofs/cbmc/poly_reduce_native_x86_64/poly_reduce_native_x86_64_harness.c new file mode 100644 index 0000000000..174c96ebfb --- /dev/null +++ b/proofs/cbmc/poly_reduce_native_x86_64/poly_reduce_native_x86_64_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" +#include "params.h" + +int mlk_poly_reduce_native(int16_t data[MLKEM_N]); + +void harness(void) +{ + int16_t *r; + int t; + t = mlk_poly_reduce_native(r); +} diff --git a/proofs/cbmc/poly_tobytes_native_x86_64/Makefile b/proofs/cbmc/poly_tobytes_native_x86_64/Makefile new file mode 100644 index 0000000000..5e2576999c --- /dev/null +++ b/proofs/cbmc/poly_tobytes_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_tobytes_native_x86_64_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_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mlk_poly_tobytes_native +USE_FUNCTION_CONTRACTS=mlk_ntttobytes_avx2 mlk_sys_check_capability +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_tobytes_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_x86_64/poly_tobytes_native_x86_64_harness.c b/proofs/cbmc/poly_tobytes_native_x86_64/poly_tobytes_native_x86_64_harness.c new file mode 100644 index 0000000000..1ca67adde2 --- /dev/null +++ b/proofs/cbmc/poly_tobytes_native_x86_64/poly_tobytes_native_x86_64_harness.c @@ -0,0 +1,18 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" +#include "params.h" + +int mlk_poly_tobytes_native(uint8_t r[MLKEM_POLYBYTES], + const int16_t a[MLKEM_N]); + +void harness(void) +{ + uint8_t *r; + int16_t *a; + int t; + t = mlk_poly_tobytes_native(r, a); +} diff --git a/proofs/cbmc/poly_tomont_native_x86_64/Makefile b/proofs/cbmc/poly_tomont_native_x86_64/Makefile new file mode 100644 index 0000000000..4f7f6b6ed5 --- /dev/null +++ b/proofs/cbmc/poly_tomont_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = poly_tomont_native_x86_64_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_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly.c + +CHECK_FUNCTION_CONTRACTS=mlk_poly_tomont_native +USE_FUNCTION_CONTRACTS=mlk_tomont_avx2 mlk_sys_check_capability +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_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_x86_64/poly_tomont_native_x86_64_harness.c b/proofs/cbmc/poly_tomont_native_x86_64/poly_tomont_native_x86_64_harness.c new file mode 100644 index 0000000000..843083a910 --- /dev/null +++ b/proofs/cbmc/poly_tomont_native_x86_64/poly_tomont_native_x86_64_harness.c @@ -0,0 +1,16 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" +#include "params.h" + +int mlk_poly_tomont_native(int16_t p[MLKEM_N]); + +void harness(void) +{ + int16_t *r; + int t; + t = mlk_poly_tomont_native(r); +} diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile new file mode 100644 index 0000000000..0ccc6dc783 --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyvec_basemul_acc_montgomery_cached_k2_native_x86_64_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_k2_native_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly_k.c + +CHECK_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_k2_native +USE_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_asm_k2 mlk_sys_check_capability +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_k2_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_k2_native_x86_64/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64_harness.c new file mode 100644 index 0000000000..6bd47ad948 --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64/polyvec_basemul_acc_montgomery_cached_k2_native_x86_64_harness.c @@ -0,0 +1,22 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +#include "cbmc.h" +#include "common.h" + +int mlk_polyvec_basemul_acc_montgomery_cached_k2_native( + int16_t r[MLKEM_N], const int16_t a[2 * MLKEM_N], + const int16_t b[2 * MLKEM_N], const int16_t b_cache[2 * (MLKEM_N / 2)]); + +void harness(void) +{ + int16_t *r; + const int16_t *a; + const int16_t *b; + const int16_t *b_cache; + int t; + t = mlk_polyvec_basemul_acc_montgomery_cached_k2_native(r, a, b, b_cache); +} diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/Makefile new file mode 100644 index 0000000000..2b593e3136 --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyvec_basemul_acc_montgomery_cached_k3_native_x86_64_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_k3_native_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly_k.c + +CHECK_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_k3_native +USE_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 mlk_sys_check_capability +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_k3_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_k3_native_x86_64/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64_harness.c new file mode 100644 index 0000000000..ae54722ba4 --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64/polyvec_basemul_acc_montgomery_cached_k3_native_x86_64_harness.c @@ -0,0 +1,21 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +#include "cbmc.h" +#include "common.h" + +int mlk_polyvec_basemul_acc_montgomery_cached_k3_native( + int16_t r[MLKEM_N], const int16_t a[3 * MLKEM_N], + const int16_t b[3 * MLKEM_N], const int16_t b_cache[3 * (MLKEM_N / 2)]); +void harness(void) +{ + int16_t *r; + const int16_t *a; + const int16_t *b; + const int16_t *b_cache; + int t; + t = mlk_polyvec_basemul_acc_montgomery_cached_k3_native(r, a, b, b_cache); +} diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/Makefile new file mode 100644 index 0000000000..ff08072fd3 --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = polyvec_basemul_acc_montgomery_cached_k4_native_x86_64_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_k4_native_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS -DMLK_CONFIG_MULTILEVEL -DMLK_CONFIG_MULTILEVEL_WITH_SHARED +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/poly_k.c + +CHECK_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_k4_native +USE_FUNCTION_CONTRACTS=mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 mlk_sys_check_capability +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_k4_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_k4_native_x86_64/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64_harness.c new file mode 100644 index 0000000000..1268b1c768 --- /dev/null +++ b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64/polyvec_basemul_acc_montgomery_cached_k4_native_x86_64_harness.c @@ -0,0 +1,22 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +#include "cbmc.h" +#include "common.h" + +int mlk_polyvec_basemul_acc_montgomery_cached_k4_native( + int16_t r[MLKEM_N], const int16_t a[4 * MLKEM_N], + const int16_t b[4 * MLKEM_N], const int16_t b_cache[4 * (MLKEM_N / 2)]); + +void harness(void) +{ + int16_t *r; + const int16_t *a; + const int16_t *b; + const int16_t *b_cache; + int t; + t = mlk_polyvec_basemul_acc_montgomery_cached_k4_native(r, a, b, b_cache); +} diff --git a/proofs/cbmc/rej_uniform_native_x86_64/Makefile b/proofs/cbmc/rej_uniform_native_x86_64/Makefile new file mode 100644 index 0000000000..50d7978999 --- /dev/null +++ b/proofs/cbmc/rej_uniform_native_x86_64/Makefile @@ -0,0 +1,57 @@ +# Copyright (c) The mlkem-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = rej_uniform_native_x86_64_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_x86_64 + +# We need to set MLK_CHECK_APIS as otherwise mlkem/src/native/api.h won't be +# included, which contains the CBMC specifications. +DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLK_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mlkem/src/native/x86_64/meta.h\"" -DMLK_CHECK_APIS +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/src/sampling.c $(SRCDIR)/mlkem/src/native/x86_64/src/rej_uniform_table.c + +CHECK_FUNCTION_CONTRACTS=mlk_rej_uniform_native +USE_FUNCTION_CONTRACTS=mlk_rej_uniform_asm mlk_sys_check_capability +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 = rej_uniform_native_x86_64 + +# 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/src/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/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_x86_64/rej_uniform_native_x86_64_harness.c b/proofs/cbmc/rej_uniform_native_x86_64/rej_uniform_native_x86_64_harness.c new file mode 100644 index 0000000000..50d08e793a --- /dev/null +++ b/proofs/cbmc/rej_uniform_native_x86_64/rej_uniform_native_x86_64_harness.c @@ -0,0 +1,20 @@ +// Copyright (c) The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include +#include "cbmc.h" + + +int mlk_rej_uniform_native(int16_t *r, unsigned len, const uint8_t *buf, + unsigned buflen); + +void harness(void) +{ + int16_t *r; + unsigned len; + const uint8_t *buf; + unsigned buflen; + + mlk_rej_uniform_native(r, len, buf, buflen); +} diff --git a/proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml b/proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml index e8c985e072..32cab4c807 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_frombytes.ml @@ -446,6 +446,9 @@ let MLKEM_FROMBYTES_NOIBT_SUBROUTINE_CORRECT = prove( MAYCHANGE [RSP] ,, MAYCHANGE [memory :> bytes(r, 512)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_frombytes_tmc MLKEM_FROMBYTES_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_FROMBYTES_SUBROUTINE_CORRECT = prove( `!r a (l:(12 word) list) pc. aligned 32 a /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_intt.ml b/proofs/hol_light/x86_64/proofs/mlkem_intt.ml index 83e7ab304a..ecff1ce758 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_intt.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_intt.ml @@ -1213,6 +1213,9 @@ let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT = prove CONV_TAC TWEAK_CONV THEN X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_intt_tmc (CONV_RULE TWEAK_CONV MLKEM_INTT_CORRECT));; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_INTT_SUBROUTINE_CORRECT = prove (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress. aligned 32 a /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml b/proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml index 5d4ee2cfcc..295b09ced8 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml @@ -267,6 +267,9 @@ let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT = prove( CONV_TAC TWEAK_CONV THEN X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_mulcache_compute_tmc (CONV_RULE TWEAK_CONV MLKEM_MULCACHE_COMPUTE_CORRECT));; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove( `!r a zetas (zetas_list:int16 list) x pc stackpointer returnaddress. aligned 32 r /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_ntt.ml b/proofs/hol_light/x86_64/proofs/mlkem_ntt.ml index c2aae4c626..9784f6c2f9 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_ntt.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_ntt.ml @@ -1222,6 +1222,9 @@ let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT = prove CONV_TAC TWEAK_CONV THEN X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_ntt_tmc (CONV_RULE TWEAK_CONV MLKEM_NTT_CORRECT));; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_NTT_SUBROUTINE_CORRECT = prove (`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress. aligned 32 a /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml index 8470f9f64b..246904936a 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml @@ -1081,6 +1081,9 @@ let MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_CORRECT = prove( MAYCHANGE [memory :> bytes(dst, 512)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k2_tmc MLKEM_BASEMUL_K2_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_BASEMUL_K2_SUBROUTINE_CORRECT = prove( `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 pc stackpointer returnaddress. aligned 32 src1 /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml index 43b31bef3d..3eac16e15f 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml @@ -1551,6 +1551,9 @@ let MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_CORRECT = prove( MAYCHANGE [memory :> bytes(dst, 512)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k3_tmc MLKEM_BASEMUL_K3_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_BASEMUL_K3_SUBROUTINE_CORRECT = prove( `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 pc stackpointer returnaddress. aligned 32 src1 /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml index bb1722ea74..85ed7c6d95 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml @@ -2028,6 +2028,9 @@ let MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_CORRECT = prove( MAYCHANGE [memory :> bytes(dst, 512)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k4_tmc MLKEM_BASEMUL_K4_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_BASEMUL_K4_SUBROUTINE_CORRECT = prove( `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 a3 b3 c3 d3 dz3 pc stackpointer returnaddress. aligned 32 src1 /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_reduce.ml b/proofs/hol_light/x86_64/proofs/mlkem_reduce.ml index 4dc859d359..3acc7357ec 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_reduce.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_reduce.ml @@ -421,6 +421,9 @@ let MLKEM_REDUCE_NOIBT_SUBROUTINE_CORRECT = prove MAYCHANGE [memory :> bytes(a, 512)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_reduce_tmc MLKEM_REDUCE_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_REDUCE_SUBROUTINE_CORRECT = prove (`!a x pc stackpointer returnaddress. aligned 32 a /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml b/proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml index 069538e2f0..96dca7af93 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_rej_uniform.ml @@ -781,6 +781,9 @@ let MLKEM_REJ_UNIFORM_NOIBT_SUBROUTINE_CORRECT = prove X86_PROMOTE_RETURN_STACK_TAC mlkem_rej_uniform_tmc (CONV_RULE TWEAK_CONV MLKEM_REJ_UNIFORM_CORRECT) `[]` 528);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_REJ_UNIFORM_SUBROUTINE_CORRECT = prove (`!res buf buflen table (inlist:(12 word)list) pc stackpointer returnaddress. 12 divides val buflen /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml b/proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml index 3fbe71b087..e7f6354f46 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_tobytes.ml @@ -404,6 +404,9 @@ let MLKEM_TOBYTES_NOIBT_SUBROUTINE_CORRECT = prove MAYCHANGE [memory :> bytes(r, 384)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_tobytes_tmc MLKEM_TOBYTES_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_TOBYTES_SUBROUTINE_CORRECT = prove (`!r a (l:int16 list) pc. aligned 32 a /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_tomont.ml b/proofs/hol_light/x86_64/proofs/mlkem_tomont.ml index 935748440d..f5033f1eb1 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_tomont.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_tomont.ml @@ -311,6 +311,9 @@ let MLKEM_TOMONT_NOIBT_SUBROUTINE_CORRECT = prove( MAYCHANGE [memory :> bytes(a,512)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_tomont_tmc MLKEM_TOMONT_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_TOMONT_SUBROUTINE_CORRECT = prove( `!a x pc stackpointer returnaddress. aligned 32 a /\ diff --git a/proofs/hol_light/x86_64/proofs/mlkem_unpack.ml b/proofs/hol_light/x86_64/proofs/mlkem_unpack.ml index 01f90b834a..975f4f7003 100644 --- a/proofs/hol_light/x86_64/proofs/mlkem_unpack.ml +++ b/proofs/hol_light/x86_64/proofs/mlkem_unpack.ml @@ -384,6 +384,9 @@ let MLKEM_UNPACK_NOIBT_SUBROUTINE_CORRECT = prove( MAYCHANGE [memory :> bytes(a, 512)])`, X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_unpack_tmc MLKEM_UNPACK_CORRECT);; +(* NOTE: This must be kept in sync with the CBMC specification + * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *) + let MLKEM_UNPACK_SUBROUTINE_CORRECT = prove( `!a (l:int16 list) pc. aligned 32 a /\ diff --git a/scripts/check-contracts b/scripts/check-contracts index cc1e7cc913..427ee8c66d 100755 --- a/scripts/check-contracts +++ b/scripts/check-contracts @@ -45,7 +45,7 @@ def is_exception(funcname): if funcname == 'poly_permute_bitrev_to_custom': return True - if funcname.endswith("_native") or funcname.endswith("_asm"): + if funcname.endswith("_native") or funcname.endswith("_asm") or funcname.endswith("avx2"): # CBMC proofs are axiomatized against contracts of the backends return True