diff --git a/mlkem/fips202/native/api.h b/mlkem/fips202/native/api.h index cd4149b0b..123cb9761 100644 --- a/mlkem/fips202/native/api.h +++ b/mlkem/fips202/native/api.h @@ -32,13 +32,22 @@ */ #if defined(MLKEM_USE_FIPS202_X1_NATIVE) -static INLINE void keccak_f1600_x1_native(uint64_t *state); +static INLINE void keccak_f1600_x1_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))); #endif #if defined(MLKEM_USE_FIPS202_X2_NATIVE) -static INLINE void keccak_f1600_x2_native(uint64_t *state); +static INLINE void keccak_f1600_x2_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 2)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))); #endif #if defined(MLKEM_USE_FIPS202_X4_NATIVE) -static INLINE void keccak_f1600_x4_native(uint64_t *state); +static INLINE void keccak_f1600_x4_native(uint64_t *state) +__contract__( + requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4)) + assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))); #endif #endif /* MLKEM_NATIVE_FIPS202_NATIVE_API_H */ diff --git a/mlkem/native/api.h b/mlkem/native/api.h index def32be36..fd69d4737 100644 --- a/mlkem/native/api.h +++ b/mlkem/native/api.h @@ -26,10 +26,16 @@ #include "../cbmc.h" #include "../common.h" -/* Absolute exclusive upper bound for the output of the inverse NTT */ +/* Absolute exclusive upper bound for the output of the inverse NTT + * + * NOTE: This is the same bound as in poly.h and has to be kept + * in sync. */ #define INVNTT_BOUND (8 * MLKEM_Q) -/* Absolute exclusive upper bound for the output of the forward NTT */ +/* Absolute exclusive upper bound for the output of the forward NTT + * + * NOTE: This is the same bound as in poly.h and has to be kept + * in sync. */ #define NTT_BOUND (8 * MLKEM_Q) /* diff --git a/proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c b/proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c new file mode 100644 index 000000000..87e0c15cb --- /dev/null +++ b/proofs/cbmc/KeccakF1600_StatePermute_native/KeccakF1600_StatePermute_native_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + KeccakF1600_StatePermute(s); +} diff --git a/proofs/cbmc/KeccakF1600_StatePermute_native/Makefile b/proofs/cbmc/KeccakF1600_StatePermute_native/Makefile new file mode 100644 index 000000000..103fa0cf1 --- /dev/null +++ b/proofs/cbmc/KeccakF1600_StatePermute_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = KeccakF1600_StatePermute_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = KeccakF1600_StatePermute_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_FIPS202 -DMLKEM_NATIVE_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x1.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600_StatePermute +USE_FUNCTION_CONTRACTS=keccak_f1600_x1_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = $(MLKEM_NAMESPACE)KeccakF1600_StatePermute_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StatePermute_native/cbmc-proof.txt similarity index 100% rename from proofs/cbmc/gen_matrix_native_order/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600_StatePermute_native/cbmc-proof.txt diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c new file mode 100644 index 000000000..021a10309 --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/KeccakF1600x4_StatePermute_native_x2_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + KeccakF1600x4_StatePermute(s); +} diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/Makefile b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/Makefile new file mode 100644 index 000000000..e46673cbf --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = KeccakF1600x4_StatePermute_native_x2_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = KeccakF1600x4_StatePermute_native_x2 + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_FIPS202 -DMLKEM_NATIVE_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x2.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute +USE_FUNCTION_CONTRACTS=keccak_f1600_x2_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = KeccakF1600x4_StatePermute_native_x2 + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/cbmc-proof.txt b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x2/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/KeccakF1600x4_StatePermute_native_x4_harness.c b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/KeccakF1600x4_StatePermute_native_x4_harness.c new file mode 100644 index 000000000..021a10309 --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/KeccakF1600x4_StatePermute_native_x4_harness.c @@ -0,0 +1,11 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +#include + +void harness(void) +{ + uint64_t *s; + KeccakF1600x4_StatePermute(s); +} diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/Makefile b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/Makefile new file mode 100644 index 000000000..305f0f768 --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = KeccakF1600x4_StatePermute_native_x4_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = KeccakF1600x4_StatePermute_native_x4 + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_FIPS202 -DMLKEM_NATIVE_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x4.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/keccakf1600.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)KeccakF1600x4_StatePermute +USE_FUNCTION_CONTRACTS=keccak_f1600_x4_native +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = KeccakF1600x4_StatePermute_native_x4 + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/cbmc-proof.txt b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/KeccakF1600x4_StatePermute_native_x4/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/dummy_backend_fips202_x1.h b/proofs/cbmc/dummy_backend_fips202_x1.h new file mode 100644 index 000000000..535386357 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x1.h @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#ifdef MLKEM_NATIVE_FIPS202_PROFILE_H +#error Only one MLKEM_FIPS202 assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_FIPS202_PROFILE_H + +#define MLKEM_NATIVE_FIPS202_BACKEND_NAME DUMMY_BACKEND_FIPS202_X1 + +/* Filename of the C backend implementation. + * This is not inlined here because this header is included in assembly + * files as well. */ +#define MLKEM_NATIVE_FIPS202_BACKEND_IMPL "dummy_backend_fips202_x1_impl.h" + +#endif /* MLKEM_NATIVE_FIPS202_PROFILE_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x1_impl.h b/proofs/cbmc/dummy_backend_fips202_x1_impl.h new file mode 100644 index 000000000..695f7a682 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x1_impl.h @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +/* ML-KEM arithmetic native profile for clean assembly */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H + +#define MLKEM_USE_FIPS202_X1_NATIVE + +#include "../mlkem/fips202/native/api.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x2.h b/proofs/cbmc/dummy_backend_fips202_x2.h new file mode 100644 index 000000000..1d7f340d7 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x2.h @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#ifdef MLKEM_NATIVE_FIPS202_PROFILE_H +#error Only one MLKEM_FIPS202 assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_FIPS202_PROFILE_H + +#define MLKEM_NATIVE_FIPS202_BACKEND_NAME DUMMY_BACKEND_FIPS202_X2 + +/* Filename of the C backend implementation. + * This is not inlined here because this header is included in assembly + * files as well. */ +#define MLKEM_NATIVE_FIPS202_BACKEND_IMPL "dummy_backend_fips202_x2_impl.h" + +#endif /* MLKEM_NATIVE_FIPS202_PROFILE_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x2_impl.h b/proofs/cbmc/dummy_backend_fips202_x2_impl.h new file mode 100644 index 000000000..4978ec495 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x2_impl.h @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +/* ML-KEM arithmetic native profile for clean assembly */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H + +#define MLKEM_USE_FIPS202_X2_NATIVE + +#include "../mlkem/fips202/native/api.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x4.h b/proofs/cbmc/dummy_backend_fips202_x4.h new file mode 100644 index 000000000..58994f1b9 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x4.h @@ -0,0 +1,18 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +#ifdef MLKEM_NATIVE_FIPS202_PROFILE_H +#error Only one MLKEM_FIPS202 assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_FIPS202_PROFILE_H + +#define MLKEM_NATIVE_FIPS202_BACKEND_NAME DUMMY_BACKEND_FIPS202_X2 + +/* Filename of the C backend implementation. + * This is not inlined here because this header is included in assembly + * files as well. */ +#define MLKEM_NATIVE_FIPS202_BACKEND_IMPL "dummy_backend_fips202_x4_impl.h" + +#endif /* MLKEM_NATIVE_FIPS202_PROFILE_H */ diff --git a/proofs/cbmc/dummy_backend_fips202_x4_impl.h b/proofs/cbmc/dummy_backend_fips202_x4_impl.h new file mode 100644 index 000000000..11d4ffad0 --- /dev/null +++ b/proofs/cbmc/dummy_backend_fips202_x4_impl.h @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2024 The mlkem-native project authors + * SPDX-License-Identifier: Apache-2.0 + */ + +/* ML-KEM arithmetic native profile for clean assembly */ + +#ifdef MLKEM_NATIVE_ARITH_PROFILE_IMPL_H +#error Only one MLKEM_ARITH assembly profile can be defined -- did you include multiple profiles? +#else +#define MLKEM_NATIVE_ARITH_PROFILE_IMPL_H + +#define MLKEM_USE_FIPS202_X4_NATIVE + +#include "../mlkem/fips202/native/api.h" + +#endif /* MLKEM_NATIVE_ARITH_PROFILE_IMPL_H */ diff --git a/proofs/cbmc/gen_matrix_native/Makefile b/proofs/cbmc/gen_matrix_native/Makefile new file mode 100644 index 000000000..640048d09 --- /dev/null +++ b/proofs/cbmc/gen_matrix_native/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = gen_matrix_native_harness + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = gen_matrix_native + +DEFINES += -DMLKEM_USE_NATIVE_BACKEND_ARITH -DMLKEM_NATIVE_ARITH_BACKEND_FILE="\"dummy_backend.h\"" +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += $(MLKEM_NAMESPACE)gen_matrix.0:4 $(MLKEM_NAMESPACE)gen_matrix.1:4 $(MLKEM_NAMESPACE)gen_matrix.2:4 $(MLKEM_NAMESPACE)gen_matrix.3:4 $(MLKEM_NAMESPACE)gen_matrix.4:4 + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix +USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_rej_uniform $(MLKEM_NAMESPACE)poly_rej_uniform_x4 poly_permute_bitrev_to_custom +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = $(MLKEM_NAMESPACE)gen_matrix_native + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 10 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/proofs/cbmc/gen_matrix_native_order/Makefile b/proofs/cbmc/gen_matrix_native/Makefile~ similarity index 100% rename from proofs/cbmc/gen_matrix_native_order/Makefile rename to proofs/cbmc/gen_matrix_native/Makefile~ diff --git a/proofs/cbmc/gen_matrix_native/cbmc-proof.txt b/proofs/cbmc/gen_matrix_native/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/proofs/cbmc/gen_matrix_native/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c b/proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c similarity index 100% rename from proofs/cbmc/gen_matrix_native_order/gen_matrix_native_order_harness.c rename to proofs/cbmc/gen_matrix_native/gen_matrix_native_harness.c diff --git a/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c b/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c index 77c5f2d06..e9a740d2c 100644 --- a/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c +++ b/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_frombytes(a, r); } diff --git a/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c b/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c index 77c5f2d06..e9a740d2c 100644 --- a/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c +++ b/proofs/cbmc/poly_frombytes_native/poly_frombytes_native_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_frombytes(a, r); } diff --git a/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c b/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c index 4b8f7be6a..571e75e3f 100644 --- a/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c +++ b/proofs/cbmc/poly_reduce_native/poly_reduce_native_harness.c @@ -8,6 +8,6 @@ void harness(void) { poly *a; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_reduce(a); } diff --git a/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c b/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c index de83a4d32..1c17d81e3 100644 --- a/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c +++ b/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_tobytes(r, a); } diff --git a/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c b/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c index de83a4d32..1c17d81e3 100644 --- a/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c +++ b/proofs/cbmc/poly_tobytes_native/poly_tobytes_native_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *r; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_tobytes(r, a); } diff --git a/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c b/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c index 36c56d0f5..16b66b91a 100644 --- a/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c +++ b/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c @@ -9,6 +9,6 @@ void harness(void) poly *a; uint8_t *msg; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ poly_tomsg(msg, a); } diff --git a/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c b/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c index 42fb73a8c..27c77d4b2 100644 --- a/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c +++ b/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d1(u); } diff --git a/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c b/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c index a84b36af2..708232706 100644 --- a/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c +++ b/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d10(u); } diff --git a/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c b/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c index 56dfc4913..c5b01ef5f 100644 --- a/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c +++ b/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d11(u); } diff --git a/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c b/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c index 4ac18801c..b7465fe4f 100644 --- a/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c +++ b/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d4(u); } diff --git a/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c b/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c index 6c50800ec..61c892732 100644 --- a/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c +++ b/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c @@ -8,6 +8,6 @@ void harness(void) { uint16_t u; - /* Contracts for this function are in poly.h */ + /* Contracts for this function are in compress.h */ uint32_t d = scalar_compress_d5(u); }