diff --git a/README.md b/README.md index bad6df3fa..d0893f0bf 100644 --- a/README.md +++ b/README.md @@ -55,7 +55,7 @@ through suitable barriers and constant-time patterns. We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to prove absence of various classes of undefined behaviour in C, including out of bounds memory accesses and integer overflows. The proofs cover all C code in [mlkem/*](mlkem) and [mlkem/fips202/*](mlkem/fips202) involved in running mlkem-native with its C backend. -See [cbmc](cbmc) for details. +See [proofs/cbmc](proofs/cbmc) for details. Experiments are underway to verify assembly using the [HOL-Light](https://hol-light.github.io/) theorem prover and the [s2n-bignum](https://github.com/awslabs/s2n-bignum) infrastructure (e.g. see diff --git a/cbmc/.gitignore b/proofs/cbmc/.gitignore similarity index 100% rename from cbmc/.gitignore rename to proofs/cbmc/.gitignore diff --git a/cbmc/KeccakF1600_StateExtractBytes/KeccakF1600_StateExtractBytes_harness.c b/proofs/cbmc/KeccakF1600_StateExtractBytes/KeccakF1600_StateExtractBytes_harness.c similarity index 100% rename from cbmc/KeccakF1600_StateExtractBytes/KeccakF1600_StateExtractBytes_harness.c rename to proofs/cbmc/KeccakF1600_StateExtractBytes/KeccakF1600_StateExtractBytes_harness.c diff --git a/cbmc/KeccakF1600_StateExtractBytes/Makefile b/proofs/cbmc/KeccakF1600_StateExtractBytes/Makefile similarity index 100% rename from cbmc/KeccakF1600_StateExtractBytes/Makefile rename to proofs/cbmc/KeccakF1600_StateExtractBytes/Makefile diff --git a/cbmc/KeccakF1600_StateExtractBytes/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StateExtractBytes/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600_StateExtractBytes/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600_StateExtractBytes/cbmc-proof.txt diff --git a/cbmc/KeccakF1600_StateExtractBytes_BE/KeccakF1600_StateExtractBytes_be_harness.c b/proofs/cbmc/KeccakF1600_StateExtractBytes_BE/KeccakF1600_StateExtractBytes_be_harness.c similarity index 100% rename from cbmc/KeccakF1600_StateExtractBytes_BE/KeccakF1600_StateExtractBytes_be_harness.c rename to proofs/cbmc/KeccakF1600_StateExtractBytes_BE/KeccakF1600_StateExtractBytes_be_harness.c diff --git a/cbmc/KeccakF1600_StateExtractBytes_BE/Makefile b/proofs/cbmc/KeccakF1600_StateExtractBytes_BE/Makefile similarity index 100% rename from cbmc/KeccakF1600_StateExtractBytes_BE/Makefile rename to proofs/cbmc/KeccakF1600_StateExtractBytes_BE/Makefile diff --git a/cbmc/KeccakF1600_StateExtractBytes_BE/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StateExtractBytes_BE/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600_StateExtractBytes_BE/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600_StateExtractBytes_BE/cbmc-proof.txt diff --git a/cbmc/KeccakF1600_StatePermute/KeccakF1600_StatePermute_harness.c b/proofs/cbmc/KeccakF1600_StatePermute/KeccakF1600_StatePermute_harness.c similarity index 100% rename from cbmc/KeccakF1600_StatePermute/KeccakF1600_StatePermute_harness.c rename to proofs/cbmc/KeccakF1600_StatePermute/KeccakF1600_StatePermute_harness.c diff --git a/cbmc/KeccakF1600_StatePermute/Makefile b/proofs/cbmc/KeccakF1600_StatePermute/Makefile similarity index 100% rename from cbmc/KeccakF1600_StatePermute/Makefile rename to proofs/cbmc/KeccakF1600_StatePermute/Makefile diff --git a/cbmc/KeccakF1600_StatePermute/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StatePermute/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600_StatePermute/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600_StatePermute/cbmc-proof.txt diff --git a/cbmc/KeccakF1600_StateXORBytes/KeccakF1600_StateXORBytes_harness.c b/proofs/cbmc/KeccakF1600_StateXORBytes/KeccakF1600_StateXORBytes_harness.c similarity index 100% rename from cbmc/KeccakF1600_StateXORBytes/KeccakF1600_StateXORBytes_harness.c rename to proofs/cbmc/KeccakF1600_StateXORBytes/KeccakF1600_StateXORBytes_harness.c diff --git a/cbmc/KeccakF1600_StateXORBytes/Makefile b/proofs/cbmc/KeccakF1600_StateXORBytes/Makefile similarity index 100% rename from cbmc/KeccakF1600_StateXORBytes/Makefile rename to proofs/cbmc/KeccakF1600_StateXORBytes/Makefile diff --git a/cbmc/KeccakF1600_StateXORBytes/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StateXORBytes/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600_StateXORBytes/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600_StateXORBytes/cbmc-proof.txt diff --git a/cbmc/KeccakF1600_StateXORBytes_BE/KeccakF1600_StateXORBytes_be_harness.c b/proofs/cbmc/KeccakF1600_StateXORBytes_BE/KeccakF1600_StateXORBytes_be_harness.c similarity index 100% rename from cbmc/KeccakF1600_StateXORBytes_BE/KeccakF1600_StateXORBytes_be_harness.c rename to proofs/cbmc/KeccakF1600_StateXORBytes_BE/KeccakF1600_StateXORBytes_be_harness.c diff --git a/cbmc/KeccakF1600_StateXORBytes_BE/Makefile b/proofs/cbmc/KeccakF1600_StateXORBytes_BE/Makefile similarity index 100% rename from cbmc/KeccakF1600_StateXORBytes_BE/Makefile rename to proofs/cbmc/KeccakF1600_StateXORBytes_BE/Makefile diff --git a/cbmc/KeccakF1600_StateXORBytes_BE/cbmc-proof.txt b/proofs/cbmc/KeccakF1600_StateXORBytes_BE/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600_StateXORBytes_BE/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600_StateXORBytes_BE/cbmc-proof.txt diff --git a/cbmc/KeccakF1600x4_StateExtractBytes/KeccakF1600x4_StateExtractBytes_harness.c b/proofs/cbmc/KeccakF1600x4_StateExtractBytes/KeccakF1600x4_StateExtractBytes_harness.c similarity index 100% rename from cbmc/KeccakF1600x4_StateExtractBytes/KeccakF1600x4_StateExtractBytes_harness.c rename to proofs/cbmc/KeccakF1600x4_StateExtractBytes/KeccakF1600x4_StateExtractBytes_harness.c diff --git a/cbmc/KeccakF1600x4_StateExtractBytes/Makefile b/proofs/cbmc/KeccakF1600x4_StateExtractBytes/Makefile similarity index 100% rename from cbmc/KeccakF1600x4_StateExtractBytes/Makefile rename to proofs/cbmc/KeccakF1600x4_StateExtractBytes/Makefile diff --git a/cbmc/KeccakF1600x4_StateExtractBytes/cbmc-proof.txt b/proofs/cbmc/KeccakF1600x4_StateExtractBytes/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600x4_StateExtractBytes/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600x4_StateExtractBytes/cbmc-proof.txt diff --git a/cbmc/KeccakF1600x4_StatePermute/KeccakF1600x4_StatePermute_harness.c b/proofs/cbmc/KeccakF1600x4_StatePermute/KeccakF1600x4_StatePermute_harness.c similarity index 100% rename from cbmc/KeccakF1600x4_StatePermute/KeccakF1600x4_StatePermute_harness.c rename to proofs/cbmc/KeccakF1600x4_StatePermute/KeccakF1600x4_StatePermute_harness.c diff --git a/cbmc/KeccakF1600x4_StatePermute/Makefile b/proofs/cbmc/KeccakF1600x4_StatePermute/Makefile similarity index 100% rename from cbmc/KeccakF1600x4_StatePermute/Makefile rename to proofs/cbmc/KeccakF1600x4_StatePermute/Makefile diff --git a/cbmc/KeccakF1600x4_StatePermute/cbmc-proof.txt b/proofs/cbmc/KeccakF1600x4_StatePermute/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600x4_StatePermute/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600x4_StatePermute/cbmc-proof.txt diff --git a/cbmc/KeccakF1600x4_StateXORBytes/KeccakF1600x4_StateXORBytes_harness.c b/proofs/cbmc/KeccakF1600x4_StateXORBytes/KeccakF1600x4_StateXORBytes_harness.c similarity index 100% rename from cbmc/KeccakF1600x4_StateXORBytes/KeccakF1600x4_StateXORBytes_harness.c rename to proofs/cbmc/KeccakF1600x4_StateXORBytes/KeccakF1600x4_StateXORBytes_harness.c diff --git a/cbmc/KeccakF1600x4_StateXORBytes/Makefile b/proofs/cbmc/KeccakF1600x4_StateXORBytes/Makefile similarity index 100% rename from cbmc/KeccakF1600x4_StateXORBytes/Makefile rename to proofs/cbmc/KeccakF1600x4_StateXORBytes/Makefile diff --git a/cbmc/KeccakF1600x4_StateXORBytes/cbmc-proof.txt b/proofs/cbmc/KeccakF1600x4_StateXORBytes/cbmc-proof.txt similarity index 100% rename from cbmc/KeccakF1600x4_StateXORBytes/cbmc-proof.txt rename to proofs/cbmc/KeccakF1600x4_StateXORBytes/cbmc-proof.txt diff --git a/cbmc/Makefile.common b/proofs/cbmc/Makefile.common similarity index 99% rename from cbmc/Makefile.common rename to proofs/cbmc/Makefile.common index 331361787..a957a5a30 100644 --- a/cbmc/Makefile.common +++ b/proofs/cbmc/Makefile.common @@ -153,7 +153,7 @@ PROOF_STUB = $(CBMC_ROOT)/stubs # selectively enable access to such symbols via each proof's Makefile. EXPORT_FILE_LOCAL_SYMBOLS = -SRCDIR ?= $(abspath $(PROOF_ROOT)/..) +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../) LITANI ?= litani PROJECT_NAME = "mlkem-native" diff --git a/cbmc/Makefile_params.common b/proofs/cbmc/Makefile_params.common similarity index 100% rename from cbmc/Makefile_params.common rename to proofs/cbmc/Makefile_params.common diff --git a/cbmc/README.md b/proofs/cbmc/README.md similarity index 100% rename from cbmc/README.md rename to proofs/cbmc/README.md diff --git a/cbmc/barrett_reduce/Makefile b/proofs/cbmc/barrett_reduce/Makefile similarity index 100% rename from cbmc/barrett_reduce/Makefile rename to proofs/cbmc/barrett_reduce/Makefile diff --git a/cbmc/barrett_reduce/barrett_reduce_harness.c b/proofs/cbmc/barrett_reduce/barrett_reduce_harness.c similarity index 100% rename from cbmc/barrett_reduce/barrett_reduce_harness.c rename to proofs/cbmc/barrett_reduce/barrett_reduce_harness.c diff --git a/cbmc/barrett_reduce/cbmc-proof.txt b/proofs/cbmc/barrett_reduce/cbmc-proof.txt similarity index 100% rename from cbmc/barrett_reduce/cbmc-proof.txt rename to proofs/cbmc/barrett_reduce/cbmc-proof.txt diff --git a/cbmc/basemul_cached/Makefile b/proofs/cbmc/basemul_cached/Makefile similarity index 100% rename from cbmc/basemul_cached/Makefile rename to proofs/cbmc/basemul_cached/Makefile diff --git a/cbmc/basemul_cached/basemul_cached_harness.c b/proofs/cbmc/basemul_cached/basemul_cached_harness.c similarity index 100% rename from cbmc/basemul_cached/basemul_cached_harness.c rename to proofs/cbmc/basemul_cached/basemul_cached_harness.c diff --git a/cbmc/basemul_cached/cbmc-proof.txt b/proofs/cbmc/basemul_cached/cbmc-proof.txt similarity index 100% rename from cbmc/basemul_cached/cbmc-proof.txt rename to proofs/cbmc/basemul_cached/cbmc-proof.txt diff --git a/cbmc/crypto_kem_dec/Makefile b/proofs/cbmc/crypto_kem_dec/Makefile similarity index 100% rename from cbmc/crypto_kem_dec/Makefile rename to proofs/cbmc/crypto_kem_dec/Makefile diff --git a/cbmc/crypto_kem_dec/cbmc-proof.txt b/proofs/cbmc/crypto_kem_dec/cbmc-proof.txt similarity index 100% rename from cbmc/crypto_kem_dec/cbmc-proof.txt rename to proofs/cbmc/crypto_kem_dec/cbmc-proof.txt diff --git a/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c b/proofs/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c similarity index 100% rename from cbmc/crypto_kem_dec/crypto_kem_dec_harness.c rename to proofs/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c diff --git a/cbmc/crypto_kem_enc/Makefile b/proofs/cbmc/crypto_kem_enc/Makefile similarity index 100% rename from cbmc/crypto_kem_enc/Makefile rename to proofs/cbmc/crypto_kem_enc/Makefile diff --git a/cbmc/crypto_kem_enc/cbmc-proof.txt b/proofs/cbmc/crypto_kem_enc/cbmc-proof.txt similarity index 100% rename from cbmc/crypto_kem_enc/cbmc-proof.txt rename to proofs/cbmc/crypto_kem_enc/cbmc-proof.txt diff --git a/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c b/proofs/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c similarity index 100% rename from cbmc/crypto_kem_enc/crypto_kem_enc_harness.c rename to proofs/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c diff --git a/cbmc/crypto_kem_enc_derand/Makefile b/proofs/cbmc/crypto_kem_enc_derand/Makefile similarity index 100% rename from cbmc/crypto_kem_enc_derand/Makefile rename to proofs/cbmc/crypto_kem_enc_derand/Makefile diff --git a/cbmc/crypto_kem_enc_derand/cbmc-proof.txt b/proofs/cbmc/crypto_kem_enc_derand/cbmc-proof.txt similarity index 100% rename from cbmc/crypto_kem_enc_derand/cbmc-proof.txt rename to proofs/cbmc/crypto_kem_enc_derand/cbmc-proof.txt diff --git a/cbmc/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c b/proofs/cbmc/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c similarity index 100% rename from cbmc/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c rename to proofs/cbmc/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c diff --git a/cbmc/crypto_kem_keypair/Makefile b/proofs/cbmc/crypto_kem_keypair/Makefile similarity index 100% rename from cbmc/crypto_kem_keypair/Makefile rename to proofs/cbmc/crypto_kem_keypair/Makefile diff --git a/cbmc/crypto_kem_keypair/cbmc-proof.txt b/proofs/cbmc/crypto_kem_keypair/cbmc-proof.txt similarity index 100% rename from cbmc/crypto_kem_keypair/cbmc-proof.txt rename to proofs/cbmc/crypto_kem_keypair/cbmc-proof.txt diff --git a/cbmc/crypto_kem_keypair/crypto_kem_keypair_harness.c b/proofs/cbmc/crypto_kem_keypair/crypto_kem_keypair_harness.c similarity index 100% rename from cbmc/crypto_kem_keypair/crypto_kem_keypair_harness.c rename to proofs/cbmc/crypto_kem_keypair/crypto_kem_keypair_harness.c diff --git a/cbmc/crypto_kem_keypair_derand/Makefile b/proofs/cbmc/crypto_kem_keypair_derand/Makefile similarity index 100% rename from cbmc/crypto_kem_keypair_derand/Makefile rename to proofs/cbmc/crypto_kem_keypair_derand/Makefile diff --git a/cbmc/crypto_kem_keypair_derand/cbmc-proof.txt b/proofs/cbmc/crypto_kem_keypair_derand/cbmc-proof.txt similarity index 100% rename from cbmc/crypto_kem_keypair_derand/cbmc-proof.txt rename to proofs/cbmc/crypto_kem_keypair_derand/cbmc-proof.txt diff --git a/cbmc/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c b/proofs/cbmc/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c similarity index 100% rename from cbmc/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c rename to proofs/cbmc/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c diff --git a/cbmc/ct_cmask_neg_i16/Makefile b/proofs/cbmc/ct_cmask_neg_i16/Makefile similarity index 100% rename from cbmc/ct_cmask_neg_i16/Makefile rename to proofs/cbmc/ct_cmask_neg_i16/Makefile diff --git a/cbmc/ct_cmask_neg_i16/cbmc-proof.txt b/proofs/cbmc/ct_cmask_neg_i16/cbmc-proof.txt similarity index 100% rename from cbmc/ct_cmask_neg_i16/cbmc-proof.txt rename to proofs/cbmc/ct_cmask_neg_i16/cbmc-proof.txt diff --git a/cbmc/ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c b/proofs/cbmc/ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c similarity index 100% rename from cbmc/ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c rename to proofs/cbmc/ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c diff --git a/cbmc/ct_cmask_nonzero_u16/Makefile b/proofs/cbmc/ct_cmask_nonzero_u16/Makefile similarity index 100% rename from cbmc/ct_cmask_nonzero_u16/Makefile rename to proofs/cbmc/ct_cmask_nonzero_u16/Makefile diff --git a/cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt b/proofs/cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt similarity index 100% rename from cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt rename to proofs/cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt diff --git a/cbmc/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c b/proofs/cbmc/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c similarity index 100% rename from cbmc/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c rename to proofs/cbmc/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c diff --git a/cbmc/ct_cmask_nonzero_u8/Makefile b/proofs/cbmc/ct_cmask_nonzero_u8/Makefile similarity index 100% rename from cbmc/ct_cmask_nonzero_u8/Makefile rename to proofs/cbmc/ct_cmask_nonzero_u8/Makefile diff --git a/cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt b/proofs/cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt similarity index 100% rename from cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt rename to proofs/cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt diff --git a/cbmc/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c b/proofs/cbmc/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c similarity index 100% rename from cbmc/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c rename to proofs/cbmc/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c diff --git a/cbmc/ct_cmov_zero/Makefile b/proofs/cbmc/ct_cmov_zero/Makefile similarity index 100% rename from cbmc/ct_cmov_zero/Makefile rename to proofs/cbmc/ct_cmov_zero/Makefile diff --git a/cbmc/ct_cmov_zero/cbmc-proof.txt b/proofs/cbmc/ct_cmov_zero/cbmc-proof.txt similarity index 100% rename from cbmc/ct_cmov_zero/cbmc-proof.txt rename to proofs/cbmc/ct_cmov_zero/cbmc-proof.txt diff --git a/cbmc/ct_cmov_zero/ct_cmov_zero_harness.c b/proofs/cbmc/ct_cmov_zero/ct_cmov_zero_harness.c similarity index 100% rename from cbmc/ct_cmov_zero/ct_cmov_zero_harness.c rename to proofs/cbmc/ct_cmov_zero/ct_cmov_zero_harness.c diff --git a/cbmc/ct_memcmp/Makefile b/proofs/cbmc/ct_memcmp/Makefile similarity index 100% rename from cbmc/ct_memcmp/Makefile rename to proofs/cbmc/ct_memcmp/Makefile diff --git a/cbmc/ct_memcmp/cbmc-proof.txt b/proofs/cbmc/ct_memcmp/cbmc-proof.txt similarity index 100% rename from cbmc/ct_memcmp/cbmc-proof.txt rename to proofs/cbmc/ct_memcmp/cbmc-proof.txt diff --git a/cbmc/ct_memcmp/ct_memcmp_harness.c b/proofs/cbmc/ct_memcmp/ct_memcmp_harness.c similarity index 100% rename from cbmc/ct_memcmp/ct_memcmp_harness.c rename to proofs/cbmc/ct_memcmp/ct_memcmp_harness.c diff --git a/cbmc/ct_sel_int16/Makefile b/proofs/cbmc/ct_sel_int16/Makefile similarity index 100% rename from cbmc/ct_sel_int16/Makefile rename to proofs/cbmc/ct_sel_int16/Makefile diff --git a/cbmc/ct_sel_int16/cbmc-proof.txt b/proofs/cbmc/ct_sel_int16/cbmc-proof.txt similarity index 100% rename from cbmc/ct_sel_int16/cbmc-proof.txt rename to proofs/cbmc/ct_sel_int16/cbmc-proof.txt diff --git a/cbmc/ct_sel_int16/ct_sel_int16_harness.c b/proofs/cbmc/ct_sel_int16/ct_sel_int16_harness.c similarity index 100% rename from cbmc/ct_sel_int16/ct_sel_int16_harness.c rename to proofs/cbmc/ct_sel_int16/ct_sel_int16_harness.c diff --git a/cbmc/ct_sel_uint8/Makefile b/proofs/cbmc/ct_sel_uint8/Makefile similarity index 100% rename from cbmc/ct_sel_uint8/Makefile rename to proofs/cbmc/ct_sel_uint8/Makefile diff --git a/cbmc/ct_sel_uint8/cbmc-proof.txt b/proofs/cbmc/ct_sel_uint8/cbmc-proof.txt similarity index 100% rename from cbmc/ct_sel_uint8/cbmc-proof.txt rename to proofs/cbmc/ct_sel_uint8/cbmc-proof.txt diff --git a/cbmc/ct_sel_uint8/ct_sel_uint8_harness.c b/proofs/cbmc/ct_sel_uint8/ct_sel_uint8_harness.c similarity index 100% rename from cbmc/ct_sel_uint8/ct_sel_uint8_harness.c rename to proofs/cbmc/ct_sel_uint8/ct_sel_uint8_harness.c diff --git a/cbmc/fqmul/Makefile b/proofs/cbmc/fqmul/Makefile similarity index 100% rename from cbmc/fqmul/Makefile rename to proofs/cbmc/fqmul/Makefile diff --git a/cbmc/fqmul/cbmc-proof.txt b/proofs/cbmc/fqmul/cbmc-proof.txt similarity index 100% rename from cbmc/fqmul/cbmc-proof.txt rename to proofs/cbmc/fqmul/cbmc-proof.txt diff --git a/cbmc/fqmul/fqmul_harness.c b/proofs/cbmc/fqmul/fqmul_harness.c similarity index 100% rename from cbmc/fqmul/fqmul_harness.c rename to proofs/cbmc/fqmul/fqmul_harness.c diff --git a/cbmc/gen_matrix/Makefile b/proofs/cbmc/gen_matrix/Makefile similarity index 100% rename from cbmc/gen_matrix/Makefile rename to proofs/cbmc/gen_matrix/Makefile diff --git a/cbmc/gen_matrix/cbmc-proof.txt b/proofs/cbmc/gen_matrix/cbmc-proof.txt similarity index 100% rename from cbmc/gen_matrix/cbmc-proof.txt rename to proofs/cbmc/gen_matrix/cbmc-proof.txt diff --git a/cbmc/gen_matrix/gen_matrix_harness.c b/proofs/cbmc/gen_matrix/gen_matrix_harness.c similarity index 100% rename from cbmc/gen_matrix/gen_matrix_harness.c rename to proofs/cbmc/gen_matrix/gen_matrix_harness.c diff --git a/cbmc/gen_matrix_entry/Makefile b/proofs/cbmc/gen_matrix_entry/Makefile similarity index 100% rename from cbmc/gen_matrix_entry/Makefile rename to proofs/cbmc/gen_matrix_entry/Makefile diff --git a/cbmc/gen_matrix_entry/cbmc-proof.txt b/proofs/cbmc/gen_matrix_entry/cbmc-proof.txt similarity index 100% rename from cbmc/gen_matrix_entry/cbmc-proof.txt rename to proofs/cbmc/gen_matrix_entry/cbmc-proof.txt diff --git a/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c b/proofs/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c similarity index 100% rename from cbmc/gen_matrix_entry/gen_matrix_entry_harness.c rename to proofs/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c diff --git a/cbmc/gen_matrix_entry_x4/Makefile b/proofs/cbmc/gen_matrix_entry_x4/Makefile similarity index 100% rename from cbmc/gen_matrix_entry_x4/Makefile rename to proofs/cbmc/gen_matrix_entry_x4/Makefile diff --git a/cbmc/gen_matrix_entry_x4/cbmc-proof.txt b/proofs/cbmc/gen_matrix_entry_x4/cbmc-proof.txt similarity index 100% rename from cbmc/gen_matrix_entry_x4/cbmc-proof.txt rename to proofs/cbmc/gen_matrix_entry_x4/cbmc-proof.txt diff --git a/cbmc/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c b/proofs/cbmc/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c similarity index 100% rename from cbmc/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c rename to proofs/cbmc/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c diff --git a/cbmc/indcpa_dec/Makefile b/proofs/cbmc/indcpa_dec/Makefile similarity index 100% rename from cbmc/indcpa_dec/Makefile rename to proofs/cbmc/indcpa_dec/Makefile diff --git a/cbmc/indcpa_dec/cbmc-proof.txt b/proofs/cbmc/indcpa_dec/cbmc-proof.txt similarity index 100% rename from cbmc/indcpa_dec/cbmc-proof.txt rename to proofs/cbmc/indcpa_dec/cbmc-proof.txt diff --git a/cbmc/indcpa_dec/indcpa_dec_harness.c b/proofs/cbmc/indcpa_dec/indcpa_dec_harness.c similarity index 100% rename from cbmc/indcpa_dec/indcpa_dec_harness.c rename to proofs/cbmc/indcpa_dec/indcpa_dec_harness.c diff --git a/cbmc/indcpa_enc/Makefile b/proofs/cbmc/indcpa_enc/Makefile similarity index 100% rename from cbmc/indcpa_enc/Makefile rename to proofs/cbmc/indcpa_enc/Makefile diff --git a/cbmc/indcpa_enc/cbmc-proof.txt b/proofs/cbmc/indcpa_enc/cbmc-proof.txt similarity index 100% rename from cbmc/indcpa_enc/cbmc-proof.txt rename to proofs/cbmc/indcpa_enc/cbmc-proof.txt diff --git a/cbmc/indcpa_enc/indcpa_enc_harness.c b/proofs/cbmc/indcpa_enc/indcpa_enc_harness.c similarity index 100% rename from cbmc/indcpa_enc/indcpa_enc_harness.c rename to proofs/cbmc/indcpa_enc/indcpa_enc_harness.c diff --git a/cbmc/indcpa_keypair_derand/Makefile b/proofs/cbmc/indcpa_keypair_derand/Makefile similarity index 100% rename from cbmc/indcpa_keypair_derand/Makefile rename to proofs/cbmc/indcpa_keypair_derand/Makefile diff --git a/cbmc/indcpa_keypair_derand/cbmc-proof.txt b/proofs/cbmc/indcpa_keypair_derand/cbmc-proof.txt similarity index 100% rename from cbmc/indcpa_keypair_derand/cbmc-proof.txt rename to proofs/cbmc/indcpa_keypair_derand/cbmc-proof.txt diff --git a/cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c b/proofs/cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c similarity index 100% rename from cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c rename to proofs/cbmc/indcpa_keypair_derand/indcpa_keypair_derand_harness.c diff --git a/cbmc/invntt_layer/Makefile b/proofs/cbmc/invntt_layer/Makefile similarity index 100% rename from cbmc/invntt_layer/Makefile rename to proofs/cbmc/invntt_layer/Makefile diff --git a/cbmc/invntt_layer/cbmc-proof.txt b/proofs/cbmc/invntt_layer/cbmc-proof.txt similarity index 100% rename from cbmc/invntt_layer/cbmc-proof.txt rename to proofs/cbmc/invntt_layer/cbmc-proof.txt diff --git a/cbmc/invntt_layer/invntt_layer_harness.c b/proofs/cbmc/invntt_layer/invntt_layer_harness.c similarity index 100% rename from cbmc/invntt_layer/invntt_layer_harness.c rename to proofs/cbmc/invntt_layer/invntt_layer_harness.c diff --git a/cbmc/keccak_absorb_once/Makefile b/proofs/cbmc/keccak_absorb_once/Makefile similarity index 100% rename from cbmc/keccak_absorb_once/Makefile rename to proofs/cbmc/keccak_absorb_once/Makefile diff --git a/cbmc/keccak_absorb_once/cbmc-proof.txt b/proofs/cbmc/keccak_absorb_once/cbmc-proof.txt similarity index 100% rename from cbmc/keccak_absorb_once/cbmc-proof.txt rename to proofs/cbmc/keccak_absorb_once/cbmc-proof.txt diff --git a/cbmc/keccak_absorb_once/keccak_absorb_once_harness.c b/proofs/cbmc/keccak_absorb_once/keccak_absorb_once_harness.c similarity index 100% rename from cbmc/keccak_absorb_once/keccak_absorb_once_harness.c rename to proofs/cbmc/keccak_absorb_once/keccak_absorb_once_harness.c diff --git a/cbmc/keccak_absorb_once_x4/Makefile b/proofs/cbmc/keccak_absorb_once_x4/Makefile similarity index 100% rename from cbmc/keccak_absorb_once_x4/Makefile rename to proofs/cbmc/keccak_absorb_once_x4/Makefile diff --git a/cbmc/keccak_absorb_once_x4/cbmc-proof.txt b/proofs/cbmc/keccak_absorb_once_x4/cbmc-proof.txt similarity index 100% rename from cbmc/keccak_absorb_once_x4/cbmc-proof.txt rename to proofs/cbmc/keccak_absorb_once_x4/cbmc-proof.txt diff --git a/cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c b/proofs/cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c similarity index 100% rename from cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c rename to proofs/cbmc/keccak_absorb_once_x4/keccak_absorb_once_x4_harness.c diff --git a/cbmc/keccak_squeeze_once/Makefile b/proofs/cbmc/keccak_squeeze_once/Makefile similarity index 100% rename from cbmc/keccak_squeeze_once/Makefile rename to proofs/cbmc/keccak_squeeze_once/Makefile diff --git a/cbmc/keccak_squeeze_once/cbmc-proof.txt b/proofs/cbmc/keccak_squeeze_once/cbmc-proof.txt similarity index 100% rename from cbmc/keccak_squeeze_once/cbmc-proof.txt rename to proofs/cbmc/keccak_squeeze_once/cbmc-proof.txt diff --git a/cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c b/proofs/cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c similarity index 100% rename from cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c rename to proofs/cbmc/keccak_squeeze_once/keccak_squeeze_once_harness.c diff --git a/cbmc/keccak_squeezeblocks/Makefile b/proofs/cbmc/keccak_squeezeblocks/Makefile similarity index 100% rename from cbmc/keccak_squeezeblocks/Makefile rename to proofs/cbmc/keccak_squeezeblocks/Makefile diff --git a/cbmc/keccak_squeezeblocks/cbmc-proof.txt b/proofs/cbmc/keccak_squeezeblocks/cbmc-proof.txt similarity index 100% rename from cbmc/keccak_squeezeblocks/cbmc-proof.txt rename to proofs/cbmc/keccak_squeezeblocks/cbmc-proof.txt diff --git a/cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c b/proofs/cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c similarity index 100% rename from cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c rename to proofs/cbmc/keccak_squeezeblocks/keccak_squeezeblocks_harness.c diff --git a/cbmc/keccak_squeezeblocks_x4/Makefile b/proofs/cbmc/keccak_squeezeblocks_x4/Makefile similarity index 100% rename from cbmc/keccak_squeezeblocks_x4/Makefile rename to proofs/cbmc/keccak_squeezeblocks_x4/Makefile diff --git a/cbmc/keccak_squeezeblocks_x4/cbmc-proof.txt b/proofs/cbmc/keccak_squeezeblocks_x4/cbmc-proof.txt similarity index 100% rename from cbmc/keccak_squeezeblocks_x4/cbmc-proof.txt rename to proofs/cbmc/keccak_squeezeblocks_x4/cbmc-proof.txt diff --git a/cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c b/proofs/cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c similarity index 100% rename from cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c rename to proofs/cbmc/keccak_squeezeblocks_x4/keccak_squeezeblocks_x4_harness.c diff --git a/cbmc/keccakf1600_extractbytes/Makefile b/proofs/cbmc/keccakf1600_extractbytes/Makefile similarity index 100% rename from cbmc/keccakf1600_extractbytes/Makefile rename to proofs/cbmc/keccakf1600_extractbytes/Makefile diff --git a/cbmc/keccakf1600_permute/Makefile b/proofs/cbmc/keccakf1600_permute/Makefile similarity index 100% rename from cbmc/keccakf1600_permute/Makefile rename to proofs/cbmc/keccakf1600_permute/Makefile diff --git a/cbmc/keccakf1600_xorbytes/Makefile b/proofs/cbmc/keccakf1600_xorbytes/Makefile similarity index 100% rename from cbmc/keccakf1600_xorbytes/Makefile rename to proofs/cbmc/keccakf1600_xorbytes/Makefile diff --git a/cbmc/lib/__init__.py b/proofs/cbmc/lib/__init__.py similarity index 100% rename from cbmc/lib/__init__.py rename to proofs/cbmc/lib/__init__.py diff --git a/cbmc/lib/print_tool_versions.py b/proofs/cbmc/lib/print_tool_versions.py similarity index 100% rename from cbmc/lib/print_tool_versions.py rename to proofs/cbmc/lib/print_tool_versions.py diff --git a/cbmc/lib/summarize.py b/proofs/cbmc/lib/summarize.py similarity index 100% rename from cbmc/lib/summarize.py rename to proofs/cbmc/lib/summarize.py diff --git a/cbmc/matvec_mul/Makefile b/proofs/cbmc/matvec_mul/Makefile similarity index 100% rename from cbmc/matvec_mul/Makefile rename to proofs/cbmc/matvec_mul/Makefile diff --git a/cbmc/matvec_mul/cbmc-proof.txt b/proofs/cbmc/matvec_mul/cbmc-proof.txt similarity index 100% rename from cbmc/matvec_mul/cbmc-proof.txt rename to proofs/cbmc/matvec_mul/cbmc-proof.txt diff --git a/cbmc/matvec_mul/matvec_mul_harness.c b/proofs/cbmc/matvec_mul/matvec_mul_harness.c similarity index 100% rename from cbmc/matvec_mul/matvec_mul_harness.c rename to proofs/cbmc/matvec_mul/matvec_mul_harness.c diff --git a/cbmc/montgomery_reduce/Makefile b/proofs/cbmc/montgomery_reduce/Makefile similarity index 100% rename from cbmc/montgomery_reduce/Makefile rename to proofs/cbmc/montgomery_reduce/Makefile diff --git a/cbmc/montgomery_reduce/cbmc-proof.txt b/proofs/cbmc/montgomery_reduce/cbmc-proof.txt similarity index 100% rename from cbmc/montgomery_reduce/cbmc-proof.txt rename to proofs/cbmc/montgomery_reduce/cbmc-proof.txt diff --git a/cbmc/montgomery_reduce/montgomery_reduce_harness.c b/proofs/cbmc/montgomery_reduce/montgomery_reduce_harness.c similarity index 100% rename from cbmc/montgomery_reduce/montgomery_reduce_harness.c rename to proofs/cbmc/montgomery_reduce/montgomery_reduce_harness.c diff --git a/cbmc/ntt_butterfly_block/Makefile b/proofs/cbmc/ntt_butterfly_block/Makefile similarity index 100% rename from cbmc/ntt_butterfly_block/Makefile rename to proofs/cbmc/ntt_butterfly_block/Makefile diff --git a/cbmc/ntt_butterfly_block/cbmc-proof.txt b/proofs/cbmc/ntt_butterfly_block/cbmc-proof.txt similarity index 100% rename from cbmc/ntt_butterfly_block/cbmc-proof.txt rename to proofs/cbmc/ntt_butterfly_block/cbmc-proof.txt diff --git a/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c b/proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c similarity index 100% rename from cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c rename to proofs/cbmc/ntt_butterfly_block/ntt_butterfly_block_harness.c diff --git a/cbmc/ntt_layer/Makefile b/proofs/cbmc/ntt_layer/Makefile similarity index 100% rename from cbmc/ntt_layer/Makefile rename to proofs/cbmc/ntt_layer/Makefile diff --git a/cbmc/ntt_layer/cbmc-proof.txt b/proofs/cbmc/ntt_layer/cbmc-proof.txt similarity index 100% rename from cbmc/ntt_layer/cbmc-proof.txt rename to proofs/cbmc/ntt_layer/cbmc-proof.txt diff --git a/cbmc/ntt_layer/ntt_layer_harness.c b/proofs/cbmc/ntt_layer/ntt_layer_harness.c similarity index 100% rename from cbmc/ntt_layer/ntt_layer_harness.c rename to proofs/cbmc/ntt_layer/ntt_layer_harness.c diff --git a/cbmc/poly_add/Makefile b/proofs/cbmc/poly_add/Makefile similarity index 100% rename from cbmc/poly_add/Makefile rename to proofs/cbmc/poly_add/Makefile diff --git a/cbmc/poly_add/cbmc-proof.txt b/proofs/cbmc/poly_add/cbmc-proof.txt similarity index 100% rename from cbmc/poly_add/cbmc-proof.txt rename to proofs/cbmc/poly_add/cbmc-proof.txt diff --git a/cbmc/poly_add/poly_add_harness.c b/proofs/cbmc/poly_add/poly_add_harness.c similarity index 100% rename from cbmc/poly_add/poly_add_harness.c rename to proofs/cbmc/poly_add/poly_add_harness.c diff --git a/cbmc/poly_basemul_montgomery_cached/Makefile b/proofs/cbmc/poly_basemul_montgomery_cached/Makefile similarity index 100% rename from cbmc/poly_basemul_montgomery_cached/Makefile rename to proofs/cbmc/poly_basemul_montgomery_cached/Makefile diff --git a/cbmc/poly_basemul_montgomery_cached/cbmc-proof.txt b/proofs/cbmc/poly_basemul_montgomery_cached/cbmc-proof.txt similarity index 100% rename from cbmc/poly_basemul_montgomery_cached/cbmc-proof.txt rename to proofs/cbmc/poly_basemul_montgomery_cached/cbmc-proof.txt diff --git a/cbmc/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c b/proofs/cbmc/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c similarity index 100% rename from cbmc/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c rename to proofs/cbmc/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c diff --git a/cbmc/poly_cbd_eta1/Makefile b/proofs/cbmc/poly_cbd_eta1/Makefile similarity index 100% rename from cbmc/poly_cbd_eta1/Makefile rename to proofs/cbmc/poly_cbd_eta1/Makefile diff --git a/cbmc/poly_cbd_eta1/cbmc-proof.txt b/proofs/cbmc/poly_cbd_eta1/cbmc-proof.txt similarity index 100% rename from cbmc/poly_cbd_eta1/cbmc-proof.txt rename to proofs/cbmc/poly_cbd_eta1/cbmc-proof.txt diff --git a/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c b/proofs/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c similarity index 100% rename from cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c rename to proofs/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c diff --git a/cbmc/poly_cbd_eta2/Makefile b/proofs/cbmc/poly_cbd_eta2/Makefile similarity index 100% rename from cbmc/poly_cbd_eta2/Makefile rename to proofs/cbmc/poly_cbd_eta2/Makefile diff --git a/cbmc/poly_cbd_eta2/cbmc-proof.txt b/proofs/cbmc/poly_cbd_eta2/cbmc-proof.txt similarity index 100% rename from cbmc/poly_cbd_eta2/cbmc-proof.txt rename to proofs/cbmc/poly_cbd_eta2/cbmc-proof.txt diff --git a/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c b/proofs/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c similarity index 100% rename from cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c rename to proofs/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c diff --git a/cbmc/poly_compress_du/Makefile b/proofs/cbmc/poly_compress_du/Makefile similarity index 100% rename from cbmc/poly_compress_du/Makefile rename to proofs/cbmc/poly_compress_du/Makefile diff --git a/cbmc/poly_compress_du/cbmc-proof.txt b/proofs/cbmc/poly_compress_du/cbmc-proof.txt similarity index 100% rename from cbmc/poly_compress_du/cbmc-proof.txt rename to proofs/cbmc/poly_compress_du/cbmc-proof.txt diff --git a/cbmc/poly_compress_du/poly_compress_du_harness.c b/proofs/cbmc/poly_compress_du/poly_compress_du_harness.c similarity index 100% rename from cbmc/poly_compress_du/poly_compress_du_harness.c rename to proofs/cbmc/poly_compress_du/poly_compress_du_harness.c diff --git a/cbmc/poly_compress_dv/Makefile b/proofs/cbmc/poly_compress_dv/Makefile similarity index 100% rename from cbmc/poly_compress_dv/Makefile rename to proofs/cbmc/poly_compress_dv/Makefile diff --git a/cbmc/poly_compress_dv/cbmc-proof.txt b/proofs/cbmc/poly_compress_dv/cbmc-proof.txt similarity index 100% rename from cbmc/poly_compress_dv/cbmc-proof.txt rename to proofs/cbmc/poly_compress_dv/cbmc-proof.txt diff --git a/cbmc/poly_compress_dv/poly_compress_dv_harness.c b/proofs/cbmc/poly_compress_dv/poly_compress_dv_harness.c similarity index 100% rename from cbmc/poly_compress_dv/poly_compress_dv_harness.c rename to proofs/cbmc/poly_compress_dv/poly_compress_dv_harness.c diff --git a/cbmc/poly_decompress_du/Makefile b/proofs/cbmc/poly_decompress_du/Makefile similarity index 100% rename from cbmc/poly_decompress_du/Makefile rename to proofs/cbmc/poly_decompress_du/Makefile diff --git a/cbmc/poly_decompress_du/cbmc-proof.txt b/proofs/cbmc/poly_decompress_du/cbmc-proof.txt similarity index 100% rename from cbmc/poly_decompress_du/cbmc-proof.txt rename to proofs/cbmc/poly_decompress_du/cbmc-proof.txt diff --git a/cbmc/poly_decompress_du/poly_decompress_du_harness.c b/proofs/cbmc/poly_decompress_du/poly_decompress_du_harness.c similarity index 100% rename from cbmc/poly_decompress_du/poly_decompress_du_harness.c rename to proofs/cbmc/poly_decompress_du/poly_decompress_du_harness.c diff --git a/cbmc/poly_decompress_dv/Makefile b/proofs/cbmc/poly_decompress_dv/Makefile similarity index 100% rename from cbmc/poly_decompress_dv/Makefile rename to proofs/cbmc/poly_decompress_dv/Makefile diff --git a/cbmc/poly_decompress_dv/cbmc-proof.txt b/proofs/cbmc/poly_decompress_dv/cbmc-proof.txt similarity index 100% rename from cbmc/poly_decompress_dv/cbmc-proof.txt rename to proofs/cbmc/poly_decompress_dv/cbmc-proof.txt diff --git a/cbmc/poly_decompress_dv/poly_decompress_dv_harness.c b/proofs/cbmc/poly_decompress_dv/poly_decompress_dv_harness.c similarity index 100% rename from cbmc/poly_decompress_dv/poly_decompress_dv_harness.c rename to proofs/cbmc/poly_decompress_dv/poly_decompress_dv_harness.c diff --git a/cbmc/poly_frombytes/Makefile b/proofs/cbmc/poly_frombytes/Makefile similarity index 100% rename from cbmc/poly_frombytes/Makefile rename to proofs/cbmc/poly_frombytes/Makefile diff --git a/cbmc/poly_frombytes/cbmc-proof.txt b/proofs/cbmc/poly_frombytes/cbmc-proof.txt similarity index 100% rename from cbmc/poly_frombytes/cbmc-proof.txt rename to proofs/cbmc/poly_frombytes/cbmc-proof.txt diff --git a/cbmc/poly_frombytes/poly_frombytes_harness.c b/proofs/cbmc/poly_frombytes/poly_frombytes_harness.c similarity index 100% rename from cbmc/poly_frombytes/poly_frombytes_harness.c rename to proofs/cbmc/poly_frombytes/poly_frombytes_harness.c diff --git a/cbmc/poly_frommsg/Makefile b/proofs/cbmc/poly_frommsg/Makefile similarity index 100% rename from cbmc/poly_frommsg/Makefile rename to proofs/cbmc/poly_frommsg/Makefile diff --git a/cbmc/poly_frommsg/cbmc-proof.txt b/proofs/cbmc/poly_frommsg/cbmc-proof.txt similarity index 100% rename from cbmc/poly_frommsg/cbmc-proof.txt rename to proofs/cbmc/poly_frommsg/cbmc-proof.txt diff --git a/cbmc/poly_frommsg/poly_frommsg_harness.c b/proofs/cbmc/poly_frommsg/poly_frommsg_harness.c similarity index 100% rename from cbmc/poly_frommsg/poly_frommsg_harness.c rename to proofs/cbmc/poly_frommsg/poly_frommsg_harness.c diff --git a/cbmc/poly_getnoise_eta1122_4x/Makefile b/proofs/cbmc/poly_getnoise_eta1122_4x/Makefile similarity index 100% rename from cbmc/poly_getnoise_eta1122_4x/Makefile rename to proofs/cbmc/poly_getnoise_eta1122_4x/Makefile diff --git a/cbmc/poly_getnoise_eta1122_4x/cbmc-proof.txt b/proofs/cbmc/poly_getnoise_eta1122_4x/cbmc-proof.txt similarity index 100% rename from cbmc/poly_getnoise_eta1122_4x/cbmc-proof.txt rename to proofs/cbmc/poly_getnoise_eta1122_4x/cbmc-proof.txt diff --git a/cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c b/proofs/cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c similarity index 100% rename from cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c rename to proofs/cbmc/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c diff --git a/cbmc/poly_getnoise_eta1_4x/Makefile b/proofs/cbmc/poly_getnoise_eta1_4x/Makefile similarity index 100% rename from cbmc/poly_getnoise_eta1_4x/Makefile rename to proofs/cbmc/poly_getnoise_eta1_4x/Makefile diff --git a/cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt b/proofs/cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt similarity index 100% rename from cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt rename to proofs/cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt diff --git a/cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c b/proofs/cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c similarity index 100% rename from cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c rename to proofs/cbmc/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c diff --git a/cbmc/poly_getnoise_eta2/Makefile b/proofs/cbmc/poly_getnoise_eta2/Makefile similarity index 100% rename from cbmc/poly_getnoise_eta2/Makefile rename to proofs/cbmc/poly_getnoise_eta2/Makefile diff --git a/cbmc/poly_getnoise_eta2/cbmc-proof.txt b/proofs/cbmc/poly_getnoise_eta2/cbmc-proof.txt similarity index 100% rename from cbmc/poly_getnoise_eta2/cbmc-proof.txt rename to proofs/cbmc/poly_getnoise_eta2/cbmc-proof.txt diff --git a/cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c b/proofs/cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c similarity index 100% rename from cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c rename to proofs/cbmc/poly_getnoise_eta2/poly_getnoise_eta2_harness.c diff --git a/cbmc/poly_invntt_tomont/Makefile b/proofs/cbmc/poly_invntt_tomont/Makefile similarity index 100% rename from cbmc/poly_invntt_tomont/Makefile rename to proofs/cbmc/poly_invntt_tomont/Makefile diff --git a/cbmc/poly_invntt_tomont/cbmc-proof.txt b/proofs/cbmc/poly_invntt_tomont/cbmc-proof.txt similarity index 100% rename from cbmc/poly_invntt_tomont/cbmc-proof.txt rename to proofs/cbmc/poly_invntt_tomont/cbmc-proof.txt diff --git a/cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c b/proofs/cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c similarity index 100% rename from cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c rename to proofs/cbmc/poly_invntt_tomont/poly_invntt_tomont_harness.c diff --git a/cbmc/poly_mulcache_compute/Makefile b/proofs/cbmc/poly_mulcache_compute/Makefile similarity index 100% rename from cbmc/poly_mulcache_compute/Makefile rename to proofs/cbmc/poly_mulcache_compute/Makefile diff --git a/cbmc/poly_mulcache_compute/cbmc-proof.txt b/proofs/cbmc/poly_mulcache_compute/cbmc-proof.txt similarity index 100% rename from cbmc/poly_mulcache_compute/cbmc-proof.txt rename to proofs/cbmc/poly_mulcache_compute/cbmc-proof.txt diff --git a/cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c b/proofs/cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c similarity index 100% rename from cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c rename to proofs/cbmc/poly_mulcache_compute/poly_mulcache_compute_harness.c diff --git a/cbmc/poly_ntt/Makefile b/proofs/cbmc/poly_ntt/Makefile similarity index 100% rename from cbmc/poly_ntt/Makefile rename to proofs/cbmc/poly_ntt/Makefile diff --git a/cbmc/poly_ntt/cbmc-proof.txt b/proofs/cbmc/poly_ntt/cbmc-proof.txt similarity index 100% rename from cbmc/poly_ntt/cbmc-proof.txt rename to proofs/cbmc/poly_ntt/cbmc-proof.txt diff --git a/cbmc/poly_ntt/poly_ntt_harness.c b/proofs/cbmc/poly_ntt/poly_ntt_harness.c similarity index 100% rename from cbmc/poly_ntt/poly_ntt_harness.c rename to proofs/cbmc/poly_ntt/poly_ntt_harness.c diff --git a/cbmc/poly_reduce/Makefile b/proofs/cbmc/poly_reduce/Makefile similarity index 100% rename from cbmc/poly_reduce/Makefile rename to proofs/cbmc/poly_reduce/Makefile diff --git a/cbmc/poly_reduce/cbmc-proof.txt b/proofs/cbmc/poly_reduce/cbmc-proof.txt similarity index 100% rename from cbmc/poly_reduce/cbmc-proof.txt rename to proofs/cbmc/poly_reduce/cbmc-proof.txt diff --git a/cbmc/poly_reduce/poly_reduce_harness.c b/proofs/cbmc/poly_reduce/poly_reduce_harness.c similarity index 100% rename from cbmc/poly_reduce/poly_reduce_harness.c rename to proofs/cbmc/poly_reduce/poly_reduce_harness.c diff --git a/cbmc/poly_sub/Makefile b/proofs/cbmc/poly_sub/Makefile similarity index 100% rename from cbmc/poly_sub/Makefile rename to proofs/cbmc/poly_sub/Makefile diff --git a/cbmc/poly_sub/cbmc-proof.txt b/proofs/cbmc/poly_sub/cbmc-proof.txt similarity index 100% rename from cbmc/poly_sub/cbmc-proof.txt rename to proofs/cbmc/poly_sub/cbmc-proof.txt diff --git a/cbmc/poly_sub/poly_sub_harness.c b/proofs/cbmc/poly_sub/poly_sub_harness.c similarity index 100% rename from cbmc/poly_sub/poly_sub_harness.c rename to proofs/cbmc/poly_sub/poly_sub_harness.c diff --git a/cbmc/poly_tobytes/Makefile b/proofs/cbmc/poly_tobytes/Makefile similarity index 100% rename from cbmc/poly_tobytes/Makefile rename to proofs/cbmc/poly_tobytes/Makefile diff --git a/cbmc/poly_tobytes/cbmc-proof.txt b/proofs/cbmc/poly_tobytes/cbmc-proof.txt similarity index 100% rename from cbmc/poly_tobytes/cbmc-proof.txt rename to proofs/cbmc/poly_tobytes/cbmc-proof.txt diff --git a/cbmc/poly_tobytes/poly_tobytes_harness.c b/proofs/cbmc/poly_tobytes/poly_tobytes_harness.c similarity index 100% rename from cbmc/poly_tobytes/poly_tobytes_harness.c rename to proofs/cbmc/poly_tobytes/poly_tobytes_harness.c diff --git a/cbmc/poly_tomont/Makefile b/proofs/cbmc/poly_tomont/Makefile similarity index 100% rename from cbmc/poly_tomont/Makefile rename to proofs/cbmc/poly_tomont/Makefile diff --git a/cbmc/poly_tomont/cbmc-proof.txt b/proofs/cbmc/poly_tomont/cbmc-proof.txt similarity index 100% rename from cbmc/poly_tomont/cbmc-proof.txt rename to proofs/cbmc/poly_tomont/cbmc-proof.txt diff --git a/cbmc/poly_tomont/poly_tomont_harness.c b/proofs/cbmc/poly_tomont/poly_tomont_harness.c similarity index 100% rename from cbmc/poly_tomont/poly_tomont_harness.c rename to proofs/cbmc/poly_tomont/poly_tomont_harness.c diff --git a/cbmc/poly_tomsg/Makefile b/proofs/cbmc/poly_tomsg/Makefile similarity index 100% rename from cbmc/poly_tomsg/Makefile rename to proofs/cbmc/poly_tomsg/Makefile diff --git a/cbmc/poly_tomsg/cbmc-proof.txt b/proofs/cbmc/poly_tomsg/cbmc-proof.txt similarity index 100% rename from cbmc/poly_tomsg/cbmc-proof.txt rename to proofs/cbmc/poly_tomsg/cbmc-proof.txt diff --git a/cbmc/poly_tomsg/poly_tomsg_harness.c b/proofs/cbmc/poly_tomsg/poly_tomsg_harness.c similarity index 100% rename from cbmc/poly_tomsg/poly_tomsg_harness.c rename to proofs/cbmc/poly_tomsg/poly_tomsg_harness.c diff --git a/cbmc/polyvec_add/Makefile b/proofs/cbmc/polyvec_add/Makefile similarity index 100% rename from cbmc/polyvec_add/Makefile rename to proofs/cbmc/polyvec_add/Makefile diff --git a/cbmc/polyvec_add/cbmc-proof.txt b/proofs/cbmc/polyvec_add/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_add/cbmc-proof.txt rename to proofs/cbmc/polyvec_add/cbmc-proof.txt diff --git a/cbmc/polyvec_add/polyvec_add_harness.c b/proofs/cbmc/polyvec_add/polyvec_add_harness.c similarity index 100% rename from cbmc/polyvec_add/polyvec_add_harness.c rename to proofs/cbmc/polyvec_add/polyvec_add_harness.c diff --git a/cbmc/polyvec_basemul_acc_montgomery/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile similarity index 100% rename from cbmc/polyvec_basemul_acc_montgomery/Makefile rename to proofs/cbmc/polyvec_basemul_acc_montgomery/Makefile diff --git a/cbmc/polyvec_basemul_acc_montgomery/cbmc-proof.txt b/proofs/cbmc/polyvec_basemul_acc_montgomery/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_basemul_acc_montgomery/cbmc-proof.txt rename to proofs/cbmc/polyvec_basemul_acc_montgomery/cbmc-proof.txt diff --git a/cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c similarity index 100% rename from cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c rename to proofs/cbmc/polyvec_basemul_acc_montgomery/polyvec_basemul_acc_montgomery_harness.c diff --git a/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile similarity index 100% rename from cbmc/polyvec_basemul_acc_montgomery_cached/Makefile rename to proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile diff --git a/cbmc/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt rename to proofs/cbmc/polyvec_basemul_acc_montgomery_cached/cbmc-proof.txt diff --git a/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c similarity index 100% rename from cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c rename to proofs/cbmc/polyvec_basemul_acc_montgomery_cached/polyvec_basemul_acc_montgomery_cached_harness.c diff --git a/cbmc/polyvec_compress_du/Makefile b/proofs/cbmc/polyvec_compress_du/Makefile similarity index 100% rename from cbmc/polyvec_compress_du/Makefile rename to proofs/cbmc/polyvec_compress_du/Makefile diff --git a/cbmc/polyvec_compress_du/cbmc-proof.txt b/proofs/cbmc/polyvec_compress_du/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_compress_du/cbmc-proof.txt rename to proofs/cbmc/polyvec_compress_du/cbmc-proof.txt diff --git a/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c b/proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c similarity index 100% rename from cbmc/polyvec_compress_du/polyvec_compress_du_harness.c rename to proofs/cbmc/polyvec_compress_du/polyvec_compress_du_harness.c diff --git a/cbmc/polyvec_decompress_du/Makefile b/proofs/cbmc/polyvec_decompress_du/Makefile similarity index 100% rename from cbmc/polyvec_decompress_du/Makefile rename to proofs/cbmc/polyvec_decompress_du/Makefile diff --git a/cbmc/polyvec_decompress_du/cbmc-proof.txt b/proofs/cbmc/polyvec_decompress_du/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_decompress_du/cbmc-proof.txt rename to proofs/cbmc/polyvec_decompress_du/cbmc-proof.txt diff --git a/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c b/proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c similarity index 100% rename from cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c rename to proofs/cbmc/polyvec_decompress_du/polyvec_decompress_du_harness.c diff --git a/cbmc/polyvec_frombytes/Makefile b/proofs/cbmc/polyvec_frombytes/Makefile similarity index 100% rename from cbmc/polyvec_frombytes/Makefile rename to proofs/cbmc/polyvec_frombytes/Makefile diff --git a/cbmc/polyvec_frombytes/cbmc-proof.txt b/proofs/cbmc/polyvec_frombytes/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_frombytes/cbmc-proof.txt rename to proofs/cbmc/polyvec_frombytes/cbmc-proof.txt diff --git a/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c b/proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c similarity index 100% rename from cbmc/polyvec_frombytes/polyvec_frombytes_harness.c rename to proofs/cbmc/polyvec_frombytes/polyvec_frombytes_harness.c diff --git a/cbmc/polyvec_invntt_tomont/Makefile b/proofs/cbmc/polyvec_invntt_tomont/Makefile similarity index 100% rename from cbmc/polyvec_invntt_tomont/Makefile rename to proofs/cbmc/polyvec_invntt_tomont/Makefile diff --git a/cbmc/polyvec_invntt_tomont/cbmc-proof.txt b/proofs/cbmc/polyvec_invntt_tomont/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_invntt_tomont/cbmc-proof.txt rename to proofs/cbmc/polyvec_invntt_tomont/cbmc-proof.txt diff --git a/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c b/proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c similarity index 100% rename from cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c rename to proofs/cbmc/polyvec_invntt_tomont/polyvec_invntt_tomont_harness.c diff --git a/cbmc/polyvec_mulcache_compute/Makefile b/proofs/cbmc/polyvec_mulcache_compute/Makefile similarity index 100% rename from cbmc/polyvec_mulcache_compute/Makefile rename to proofs/cbmc/polyvec_mulcache_compute/Makefile diff --git a/cbmc/polyvec_mulcache_compute/cbmc-proof.txt b/proofs/cbmc/polyvec_mulcache_compute/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_mulcache_compute/cbmc-proof.txt rename to proofs/cbmc/polyvec_mulcache_compute/cbmc-proof.txt diff --git a/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c b/proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c similarity index 100% rename from cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c rename to proofs/cbmc/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c diff --git a/cbmc/polyvec_ntt/Makefile b/proofs/cbmc/polyvec_ntt/Makefile similarity index 100% rename from cbmc/polyvec_ntt/Makefile rename to proofs/cbmc/polyvec_ntt/Makefile diff --git a/cbmc/polyvec_ntt/cbmc-proof.txt b/proofs/cbmc/polyvec_ntt/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_ntt/cbmc-proof.txt rename to proofs/cbmc/polyvec_ntt/cbmc-proof.txt diff --git a/cbmc/polyvec_ntt/polyvec_ntt_harness.c b/proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c similarity index 100% rename from cbmc/polyvec_ntt/polyvec_ntt_harness.c rename to proofs/cbmc/polyvec_ntt/polyvec_ntt_harness.c diff --git a/cbmc/polyvec_reduce/Makefile b/proofs/cbmc/polyvec_reduce/Makefile similarity index 100% rename from cbmc/polyvec_reduce/Makefile rename to proofs/cbmc/polyvec_reduce/Makefile diff --git a/cbmc/polyvec_reduce/cbmc-proof.txt b/proofs/cbmc/polyvec_reduce/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_reduce/cbmc-proof.txt rename to proofs/cbmc/polyvec_reduce/cbmc-proof.txt diff --git a/cbmc/polyvec_reduce/polyvec_reduce_harness.c b/proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c similarity index 100% rename from cbmc/polyvec_reduce/polyvec_reduce_harness.c rename to proofs/cbmc/polyvec_reduce/polyvec_reduce_harness.c diff --git a/cbmc/polyvec_tobytes/Makefile b/proofs/cbmc/polyvec_tobytes/Makefile similarity index 100% rename from cbmc/polyvec_tobytes/Makefile rename to proofs/cbmc/polyvec_tobytes/Makefile diff --git a/cbmc/polyvec_tobytes/cbmc-proof.txt b/proofs/cbmc/polyvec_tobytes/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_tobytes/cbmc-proof.txt rename to proofs/cbmc/polyvec_tobytes/cbmc-proof.txt diff --git a/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c b/proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c similarity index 100% rename from cbmc/polyvec_tobytes/polyvec_tobytes_harness.c rename to proofs/cbmc/polyvec_tobytes/polyvec_tobytes_harness.c diff --git a/cbmc/polyvec_tomont/Makefile b/proofs/cbmc/polyvec_tomont/Makefile similarity index 100% rename from cbmc/polyvec_tomont/Makefile rename to proofs/cbmc/polyvec_tomont/Makefile diff --git a/cbmc/polyvec_tomont/cbmc-proof.txt b/proofs/cbmc/polyvec_tomont/cbmc-proof.txt similarity index 100% rename from cbmc/polyvec_tomont/cbmc-proof.txt rename to proofs/cbmc/polyvec_tomont/cbmc-proof.txt diff --git a/cbmc/polyvec_tomont/polyvec_tomont_harness.c b/proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c similarity index 100% rename from cbmc/polyvec_tomont/polyvec_tomont_harness.c rename to proofs/cbmc/polyvec_tomont/polyvec_tomont_harness.c diff --git a/cbmc/proof_guide.md b/proofs/cbmc/proof_guide.md similarity index 98% rename from cbmc/proof_guide.md rename to proofs/cbmc/proof_guide.md index 3a26faff4..0a65b8f1c 100644 --- a/cbmc/proof_guide.md +++ b/proofs/cbmc/proof_guide.md @@ -23,7 +23,7 @@ context described by the annotations; if the annotations add further constraints function contract annotation provides contextual assumptions about a function as _preconditions_ to CBMC, and adds further _constraints_ for the program state at function return. -In mlkem-native, we use abbreviated forms of the CBMC annotations defined by macros in the [cbmc.h](../mlkem/cbmc.h). We +In mlkem-native, we use abbreviated forms of the CBMC annotations defined by macros in the [cbmc.h](../../mlkem/cbmc.h). We now list the most prominent. ### Function contracts @@ -383,7 +383,7 @@ Proof of a single function can be run from the proof directory for that function This produces `logs/result.txt` in plaintext format. -Before pushing a new proof for a new function, make sure that _all_ proofs run OK from the [cbmc](./) directory with +Before pushing a new proof for a new function, make sure that _all_ proofs run OK from the [proofs/cbmc](./) directory with ``` MLKEM_K=3 ./run-cbmc-proofs.py --summarize -j$(nproc) @@ -407,7 +407,7 @@ This section follows the recipe above, and adds actual settings, contracts and c ### Populate a proof directory -The proof directory is [cbmc/poly_tobytes](poly_tobytes). +The proof directory is [proofs/cbmc/poly_tobytes](poly_tobytes). ### Update Makefile @@ -452,7 +452,7 @@ So we need to write a requires contract to constrain the ranges of the coefficie is no constraint on the output byte array, other than it must be the right length, which is given by the function prototype. -We can use the macros in [mlkem/cbmc.h](../mlkem/cbmc.h) to help, thus: +We can use the macros in [mlkem/cbmc.h](../../mlkem/cbmc.h) to help, thus: ``` void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a) @@ -464,7 +464,7 @@ __contract__( `array_bound` is a macro that expands to a quantified expression that expresses that the elemtns of `a->coeffs` between index values `0` (inclusive) and `MLKEM_N` (exclusive) are in the range `0` through `(MLKEM_Q - 1)` (both -inclusive). See the macro definition in [mlkem/cbmc.h](../mlkem/cbmc.h) for details. +inclusive). See the macro definition in [mlkem/cbmc.h](../../mlkem/cbmc.h) for details. ### Interior contracts and loop invariants @@ -515,7 +515,7 @@ and so on for the other two statements in the loop body. With those changes, CBMC completes the proof in about 10 seconds: ``` -cd cbmc/poly_tobytes +cd proofs/cbmc/poly_tobytes make result cat logs/result.txt ``` @@ -528,7 +528,7 @@ VERIFICATION SUCCESSFUL We can also use the higher-level Python script to prove just that one function: ``` -cd cbmc +cd proofs/cbmc MLKEM_K=3 ./run-cbmc-proofs.py --summarize -j$(nproc) -p poly_tobytes ``` yields diff --git a/cbmc/rej_uniform/Makefile b/proofs/cbmc/rej_uniform/Makefile similarity index 100% rename from cbmc/rej_uniform/Makefile rename to proofs/cbmc/rej_uniform/Makefile diff --git a/cbmc/rej_uniform/cbmc-proof.txt b/proofs/cbmc/rej_uniform/cbmc-proof.txt similarity index 100% rename from cbmc/rej_uniform/cbmc-proof.txt rename to proofs/cbmc/rej_uniform/cbmc-proof.txt diff --git a/cbmc/rej_uniform/rej_uniform_harness.c b/proofs/cbmc/rej_uniform/rej_uniform_harness.c similarity index 100% rename from cbmc/rej_uniform/rej_uniform_harness.c rename to proofs/cbmc/rej_uniform/rej_uniform_harness.c diff --git a/cbmc/rej_uniform_scalar/Makefile b/proofs/cbmc/rej_uniform_scalar/Makefile similarity index 100% rename from cbmc/rej_uniform_scalar/Makefile rename to proofs/cbmc/rej_uniform_scalar/Makefile diff --git a/cbmc/rej_uniform_scalar/cbmc-proof.txt b/proofs/cbmc/rej_uniform_scalar/cbmc-proof.txt similarity index 100% rename from cbmc/rej_uniform_scalar/cbmc-proof.txt rename to proofs/cbmc/rej_uniform_scalar/cbmc-proof.txt diff --git a/cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c b/proofs/cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c similarity index 100% rename from cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c rename to proofs/cbmc/rej_uniform_scalar/rej_uniform_scalar_harness.c diff --git a/cbmc/run-cbmc-proofs.py b/proofs/cbmc/run-cbmc-proofs.py similarity index 100% rename from cbmc/run-cbmc-proofs.py rename to proofs/cbmc/run-cbmc-proofs.py diff --git a/cbmc/scalar_compress_d1/Makefile b/proofs/cbmc/scalar_compress_d1/Makefile similarity index 100% rename from cbmc/scalar_compress_d1/Makefile rename to proofs/cbmc/scalar_compress_d1/Makefile diff --git a/cbmc/scalar_compress_d1/cbmc-proof.txt b/proofs/cbmc/scalar_compress_d1/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_compress_d1/cbmc-proof.txt rename to proofs/cbmc/scalar_compress_d1/cbmc-proof.txt diff --git a/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c b/proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c similarity index 100% rename from cbmc/scalar_compress_d1/scalar_compress_d1_harness.c rename to proofs/cbmc/scalar_compress_d1/scalar_compress_d1_harness.c diff --git a/cbmc/scalar_compress_d10/Makefile b/proofs/cbmc/scalar_compress_d10/Makefile similarity index 100% rename from cbmc/scalar_compress_d10/Makefile rename to proofs/cbmc/scalar_compress_d10/Makefile diff --git a/cbmc/scalar_compress_d10/cbmc-proof.txt b/proofs/cbmc/scalar_compress_d10/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_compress_d10/cbmc-proof.txt rename to proofs/cbmc/scalar_compress_d10/cbmc-proof.txt diff --git a/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c b/proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c similarity index 100% rename from cbmc/scalar_compress_d10/scalar_compress_d10_harness.c rename to proofs/cbmc/scalar_compress_d10/scalar_compress_d10_harness.c diff --git a/cbmc/scalar_compress_d11/Makefile b/proofs/cbmc/scalar_compress_d11/Makefile similarity index 100% rename from cbmc/scalar_compress_d11/Makefile rename to proofs/cbmc/scalar_compress_d11/Makefile diff --git a/cbmc/scalar_compress_d11/cbmc-proof.txt b/proofs/cbmc/scalar_compress_d11/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_compress_d11/cbmc-proof.txt rename to proofs/cbmc/scalar_compress_d11/cbmc-proof.txt diff --git a/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c b/proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c similarity index 100% rename from cbmc/scalar_compress_d11/scalar_compress_d11_harness.c rename to proofs/cbmc/scalar_compress_d11/scalar_compress_d11_harness.c diff --git a/cbmc/scalar_compress_d4/Makefile b/proofs/cbmc/scalar_compress_d4/Makefile similarity index 100% rename from cbmc/scalar_compress_d4/Makefile rename to proofs/cbmc/scalar_compress_d4/Makefile diff --git a/cbmc/scalar_compress_d4/cbmc-proof.txt b/proofs/cbmc/scalar_compress_d4/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_compress_d4/cbmc-proof.txt rename to proofs/cbmc/scalar_compress_d4/cbmc-proof.txt diff --git a/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c b/proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c similarity index 100% rename from cbmc/scalar_compress_d4/scalar_compress_d4_harness.c rename to proofs/cbmc/scalar_compress_d4/scalar_compress_d4_harness.c diff --git a/cbmc/scalar_compress_d5/Makefile b/proofs/cbmc/scalar_compress_d5/Makefile similarity index 100% rename from cbmc/scalar_compress_d5/Makefile rename to proofs/cbmc/scalar_compress_d5/Makefile diff --git a/cbmc/scalar_compress_d5/cbmc-proof.txt b/proofs/cbmc/scalar_compress_d5/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_compress_d5/cbmc-proof.txt rename to proofs/cbmc/scalar_compress_d5/cbmc-proof.txt diff --git a/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c b/proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c similarity index 100% rename from cbmc/scalar_compress_d5/scalar_compress_d5_harness.c rename to proofs/cbmc/scalar_compress_d5/scalar_compress_d5_harness.c diff --git a/cbmc/scalar_decompress_d10/Makefile b/proofs/cbmc/scalar_decompress_d10/Makefile similarity index 100% rename from cbmc/scalar_decompress_d10/Makefile rename to proofs/cbmc/scalar_decompress_d10/Makefile diff --git a/cbmc/scalar_decompress_d10/cbmc-proof.txt b/proofs/cbmc/scalar_decompress_d10/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_decompress_d10/cbmc-proof.txt rename to proofs/cbmc/scalar_decompress_d10/cbmc-proof.txt diff --git a/cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c b/proofs/cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c similarity index 100% rename from cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c rename to proofs/cbmc/scalar_decompress_d10/scalar_decompress_d10_harness.c diff --git a/cbmc/scalar_decompress_d11/Makefile b/proofs/cbmc/scalar_decompress_d11/Makefile similarity index 100% rename from cbmc/scalar_decompress_d11/Makefile rename to proofs/cbmc/scalar_decompress_d11/Makefile diff --git a/cbmc/scalar_decompress_d11/cbmc-proof.txt b/proofs/cbmc/scalar_decompress_d11/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_decompress_d11/cbmc-proof.txt rename to proofs/cbmc/scalar_decompress_d11/cbmc-proof.txt diff --git a/cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c b/proofs/cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c similarity index 100% rename from cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c rename to proofs/cbmc/scalar_decompress_d11/scalar_decompress_d11_harness.c diff --git a/cbmc/scalar_decompress_d4/Makefile b/proofs/cbmc/scalar_decompress_d4/Makefile similarity index 100% rename from cbmc/scalar_decompress_d4/Makefile rename to proofs/cbmc/scalar_decompress_d4/Makefile diff --git a/cbmc/scalar_decompress_d4/cbmc-proof.txt b/proofs/cbmc/scalar_decompress_d4/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_decompress_d4/cbmc-proof.txt rename to proofs/cbmc/scalar_decompress_d4/cbmc-proof.txt diff --git a/cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c b/proofs/cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c similarity index 100% rename from cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c rename to proofs/cbmc/scalar_decompress_d4/scalar_decompress_d4_harness.c diff --git a/cbmc/scalar_decompress_d5/Makefile b/proofs/cbmc/scalar_decompress_d5/Makefile similarity index 100% rename from cbmc/scalar_decompress_d5/Makefile rename to proofs/cbmc/scalar_decompress_d5/Makefile diff --git a/cbmc/scalar_decompress_d5/cbmc-proof.txt b/proofs/cbmc/scalar_decompress_d5/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_decompress_d5/cbmc-proof.txt rename to proofs/cbmc/scalar_decompress_d5/cbmc-proof.txt diff --git a/cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c b/proofs/cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c similarity index 100% rename from cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c rename to proofs/cbmc/scalar_decompress_d5/scalar_decompress_d5_harness.c diff --git a/cbmc/scalar_signed_to_unsigned_q/Makefile b/proofs/cbmc/scalar_signed_to_unsigned_q/Makefile similarity index 100% rename from cbmc/scalar_signed_to_unsigned_q/Makefile rename to proofs/cbmc/scalar_signed_to_unsigned_q/Makefile diff --git a/cbmc/scalar_signed_to_unsigned_q/cbmc-proof.txt b/proofs/cbmc/scalar_signed_to_unsigned_q/cbmc-proof.txt similarity index 100% rename from cbmc/scalar_signed_to_unsigned_q/cbmc-proof.txt rename to proofs/cbmc/scalar_signed_to_unsigned_q/cbmc-proof.txt diff --git a/cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c b/proofs/cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c similarity index 100% rename from cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c rename to proofs/cbmc/scalar_signed_to_unsigned_q/scalar_signed_to_unsigned_q_harness.c diff --git a/cbmc/sha3_256/Makefile b/proofs/cbmc/sha3_256/Makefile similarity index 100% rename from cbmc/sha3_256/Makefile rename to proofs/cbmc/sha3_256/Makefile diff --git a/cbmc/sha3_256/cbmc-proof.txt b/proofs/cbmc/sha3_256/cbmc-proof.txt similarity index 100% rename from cbmc/sha3_256/cbmc-proof.txt rename to proofs/cbmc/sha3_256/cbmc-proof.txt diff --git a/cbmc/sha3_256/sha3_256_harness.c b/proofs/cbmc/sha3_256/sha3_256_harness.c similarity index 100% rename from cbmc/sha3_256/sha3_256_harness.c rename to proofs/cbmc/sha3_256/sha3_256_harness.c diff --git a/cbmc/sha3_512/Makefile b/proofs/cbmc/sha3_512/Makefile similarity index 100% rename from cbmc/sha3_512/Makefile rename to proofs/cbmc/sha3_512/Makefile diff --git a/cbmc/sha3_512/cbmc-proof.txt b/proofs/cbmc/sha3_512/cbmc-proof.txt similarity index 100% rename from cbmc/sha3_512/cbmc-proof.txt rename to proofs/cbmc/sha3_512/cbmc-proof.txt diff --git a/cbmc/sha3_512/sha3_512_harness.c b/proofs/cbmc/sha3_512/sha3_512_harness.c similarity index 100% rename from cbmc/sha3_512/sha3_512_harness.c rename to proofs/cbmc/sha3_512/sha3_512_harness.c diff --git a/cbmc/shake128_absorb_once/Makefile b/proofs/cbmc/shake128_absorb_once/Makefile similarity index 100% rename from cbmc/shake128_absorb_once/Makefile rename to proofs/cbmc/shake128_absorb_once/Makefile diff --git a/cbmc/shake128_absorb_once/cbmc-proof.txt b/proofs/cbmc/shake128_absorb_once/cbmc-proof.txt similarity index 100% rename from cbmc/shake128_absorb_once/cbmc-proof.txt rename to proofs/cbmc/shake128_absorb_once/cbmc-proof.txt diff --git a/cbmc/shake128_absorb_once/shake128_absorb_once_harness.c b/proofs/cbmc/shake128_absorb_once/shake128_absorb_once_harness.c similarity index 100% rename from cbmc/shake128_absorb_once/shake128_absorb_once_harness.c rename to proofs/cbmc/shake128_absorb_once/shake128_absorb_once_harness.c diff --git a/cbmc/shake128_squeezeblocks/Makefile b/proofs/cbmc/shake128_squeezeblocks/Makefile similarity index 100% rename from cbmc/shake128_squeezeblocks/Makefile rename to proofs/cbmc/shake128_squeezeblocks/Makefile diff --git a/cbmc/shake128_squeezeblocks/cbmc-proof.txt b/proofs/cbmc/shake128_squeezeblocks/cbmc-proof.txt similarity index 100% rename from cbmc/shake128_squeezeblocks/cbmc-proof.txt rename to proofs/cbmc/shake128_squeezeblocks/cbmc-proof.txt diff --git a/cbmc/shake128_squeezeblocks/shake128_squeezeblocks_harness.c b/proofs/cbmc/shake128_squeezeblocks/shake128_squeezeblocks_harness.c similarity index 100% rename from cbmc/shake128_squeezeblocks/shake128_squeezeblocks_harness.c rename to proofs/cbmc/shake128_squeezeblocks/shake128_squeezeblocks_harness.c diff --git a/cbmc/shake128x4_absorb_once/Makefile b/proofs/cbmc/shake128x4_absorb_once/Makefile similarity index 100% rename from cbmc/shake128x4_absorb_once/Makefile rename to proofs/cbmc/shake128x4_absorb_once/Makefile diff --git a/cbmc/shake128x4_absorb_once/cbmc-proof.txt b/proofs/cbmc/shake128x4_absorb_once/cbmc-proof.txt similarity index 100% rename from cbmc/shake128x4_absorb_once/cbmc-proof.txt rename to proofs/cbmc/shake128x4_absorb_once/cbmc-proof.txt diff --git a/cbmc/shake128x4_absorb_once/shake128x4_absorb_once_harness.c b/proofs/cbmc/shake128x4_absorb_once/shake128x4_absorb_once_harness.c similarity index 100% rename from cbmc/shake128x4_absorb_once/shake128x4_absorb_once_harness.c rename to proofs/cbmc/shake128x4_absorb_once/shake128x4_absorb_once_harness.c diff --git a/cbmc/shake128x4_squeezeblocks/Makefile b/proofs/cbmc/shake128x4_squeezeblocks/Makefile similarity index 100% rename from cbmc/shake128x4_squeezeblocks/Makefile rename to proofs/cbmc/shake128x4_squeezeblocks/Makefile diff --git a/cbmc/shake128x4_squeezeblocks/cbmc-proof.txt b/proofs/cbmc/shake128x4_squeezeblocks/cbmc-proof.txt similarity index 100% rename from cbmc/shake128x4_squeezeblocks/cbmc-proof.txt rename to proofs/cbmc/shake128x4_squeezeblocks/cbmc-proof.txt diff --git a/cbmc/shake128x4_squeezeblocks/shake128x4_squeezeblocks_harness.c b/proofs/cbmc/shake128x4_squeezeblocks/shake128x4_squeezeblocks_harness.c similarity index 100% rename from cbmc/shake128x4_squeezeblocks/shake128x4_squeezeblocks_harness.c rename to proofs/cbmc/shake128x4_squeezeblocks/shake128x4_squeezeblocks_harness.c diff --git a/cbmc/shake256/Makefile b/proofs/cbmc/shake256/Makefile similarity index 100% rename from cbmc/shake256/Makefile rename to proofs/cbmc/shake256/Makefile diff --git a/cbmc/shake256/cbmc-proof.txt b/proofs/cbmc/shake256/cbmc-proof.txt similarity index 100% rename from cbmc/shake256/cbmc-proof.txt rename to proofs/cbmc/shake256/cbmc-proof.txt diff --git a/cbmc/shake256/shake256_harness.c b/proofs/cbmc/shake256/shake256_harness.c similarity index 100% rename from cbmc/shake256/shake256_harness.c rename to proofs/cbmc/shake256/shake256_harness.c diff --git a/cbmc/shake256x4/Makefile b/proofs/cbmc/shake256x4/Makefile similarity index 100% rename from cbmc/shake256x4/Makefile rename to proofs/cbmc/shake256x4/Makefile diff --git a/cbmc/shake256x4/cbmc-proof.txt b/proofs/cbmc/shake256x4/cbmc-proof.txt similarity index 100% rename from cbmc/shake256x4/cbmc-proof.txt rename to proofs/cbmc/shake256x4/cbmc-proof.txt diff --git a/cbmc/shake256x4/shake256x4_harness.c b/proofs/cbmc/shake256x4/shake256x4_harness.c similarity index 100% rename from cbmc/shake256x4/shake256x4_harness.c rename to proofs/cbmc/shake256x4/shake256x4_harness.c diff --git a/scripts/lint b/scripts/lint index f30955927..5a01ac178 100755 --- a/scripts/lint +++ b/scripts/lint @@ -85,7 +85,7 @@ check-spdx() success=false fi done - for file in $(git ls-files -- "*.[chsS]" "*.py" ":/!cbmc/*.py" ":/!examples/bring_your_own_fips202/fips202/tiny_sha3/*" ":/!examples/custom_backend/mlkem_native/mlkem/fips202/native/custom/src/*"); do + for file in $(git ls-files -- "*.[chsS]" "*.py" ":/!proofs/cbmc/*.py" ":/!examples/bring_your_own_fips202/fips202/tiny_sha3/*" ":/!examples/custom_backend/mlkem_native/mlkem/fips202/native/custom/src/*"); do # Ignore symlinks if [[ ! -L $file && $(grep "Copyright (c) 2024 The mlkem-native project authors" $file | wc -l) == 0 ]]; then echo "::error file=$file,line=${line:-1},title=Missing copyright header error::$file is missing copyright header" diff --git a/scripts/tests b/scripts/tests index 1970191db..084b2fd57 100755 --- a/scripts/tests +++ b/scripts/tests @@ -664,7 +664,7 @@ class Tests: "--no-coverage", ] + self.make_j(), - cwd="cbmc", + cwd="proofs/cbmc", env=os.environ.copy() | envvars, ) p.communicate()