Move cbmc -> proofs/cbmc

This paves the way for the integration of the hol-light/s2n-bignum proofs in proofs/hol-light. Signed-off-by: Hanno Becker <[email protected]>
potsrevennil · Jan 15, 2025 · 78f99af · 78f99af
1 parent 8383b16
commit 78f99af
Show file tree

Hide file tree

Showing 291 changed files with 11 additions and 11 deletions.
diff --git 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 → proofs/cbmc/.gitignore b/cbmc/.gitignore → proofs/cbmc/.gitignore
diff --git a/...s/KeccakF1600_StateExtractBytes_harness.c → ...s/KeccakF1600_StateExtractBytes_harness.c b/...s/KeccakF1600_StateExtractBytes_harness.c → ...s/KeccakF1600_StateExtractBytes_harness.c
diff --git a/cbmc/KeccakF1600_StateExtractBytes/Makefile → ...mc/KeccakF1600_StateExtractBytes/Makefile b/cbmc/KeccakF1600_StateExtractBytes/Makefile → ...mc/KeccakF1600_StateExtractBytes/Makefile
diff --git a/...cakF1600_StateExtractBytes/cbmc-proof.txt → ...cakF1600_StateExtractBytes/cbmc-proof.txt b/...cakF1600_StateExtractBytes/cbmc-proof.txt → ...cakF1600_StateExtractBytes/cbmc-proof.txt
diff --git a/...eccakF1600_StateExtractBytes_be_harness.c → ...eccakF1600_StateExtractBytes_be_harness.c b/...eccakF1600_StateExtractBytes_be_harness.c → ...eccakF1600_StateExtractBytes_be_harness.c
diff --git a/...KeccakF1600_StateExtractBytes_BE/Makefile → ...KeccakF1600_StateExtractBytes_BE/Makefile b/...KeccakF1600_StateExtractBytes_BE/Makefile → ...KeccakF1600_StateExtractBytes_BE/Makefile
diff --git a/...F1600_StateExtractBytes_BE/cbmc-proof.txt → ...F1600_StateExtractBytes_BE/cbmc-proof.txt b/...F1600_StateExtractBytes_BE/cbmc-proof.txt → ...F1600_StateExtractBytes_BE/cbmc-proof.txt
diff --git a/...ermute/KeccakF1600_StatePermute_harness.c → ...ermute/KeccakF1600_StatePermute_harness.c b/...ermute/KeccakF1600_StatePermute_harness.c → ...ermute/KeccakF1600_StatePermute_harness.c
diff --git a/cbmc/KeccakF1600_StatePermute/Makefile → ...fs/cbmc/KeccakF1600_StatePermute/Makefile b/cbmc/KeccakF1600_StatePermute/Makefile → ...fs/cbmc/KeccakF1600_StatePermute/Makefile
diff --git a/cbmc/KeccakF1600_StatePermute/cbmc-proof.txt → ...c/KeccakF1600_StatePermute/cbmc-proof.txt b/cbmc/KeccakF1600_StatePermute/cbmc-proof.txt → ...c/KeccakF1600_StatePermute/cbmc-proof.txt
diff --git a/...Bytes/KeccakF1600_StateXORBytes_harness.c → ...Bytes/KeccakF1600_StateXORBytes_harness.c b/...Bytes/KeccakF1600_StateXORBytes_harness.c → ...Bytes/KeccakF1600_StateXORBytes_harness.c
diff --git a/cbmc/KeccakF1600_StateXORBytes/Makefile → ...s/cbmc/KeccakF1600_StateXORBytes/Makefile b/cbmc/KeccakF1600_StateXORBytes/Makefile → ...s/cbmc/KeccakF1600_StateXORBytes/Makefile
diff --git a/.../KeccakF1600_StateXORBytes/cbmc-proof.txt → .../KeccakF1600_StateXORBytes/cbmc-proof.txt b/.../KeccakF1600_StateXORBytes/cbmc-proof.txt → .../KeccakF1600_StateXORBytes/cbmc-proof.txt
diff --git a/...BE/KeccakF1600_StateXORBytes_be_harness.c → ...BE/KeccakF1600_StateXORBytes_be_harness.c b/...BE/KeccakF1600_StateXORBytes_be_harness.c → ...BE/KeccakF1600_StateXORBytes_be_harness.c
diff --git a/cbmc/KeccakF1600_StateXORBytes_BE/Makefile → ...bmc/KeccakF1600_StateXORBytes_BE/Makefile b/cbmc/KeccakF1600_StateXORBytes_BE/Makefile → ...bmc/KeccakF1600_StateXORBytes_BE/Makefile
diff --git a/...ccakF1600_StateXORBytes_BE/cbmc-proof.txt → ...ccakF1600_StateXORBytes_BE/cbmc-proof.txt b/...ccakF1600_StateXORBytes_BE/cbmc-proof.txt → ...ccakF1600_StateXORBytes_BE/cbmc-proof.txt
diff --git a/...KeccakF1600x4_StateExtractBytes_harness.c → ...KeccakF1600x4_StateExtractBytes_harness.c b/...KeccakF1600x4_StateExtractBytes_harness.c → ...KeccakF1600x4_StateExtractBytes_harness.c
diff --git a/.../KeccakF1600x4_StateExtractBytes/Makefile → .../KeccakF1600x4_StateExtractBytes/Makefile b/.../KeccakF1600x4_StateExtractBytes/Makefile → .../KeccakF1600x4_StateExtractBytes/Makefile
diff --git a/...kF1600x4_StateExtractBytes/cbmc-proof.txt → ...kF1600x4_StateExtractBytes/cbmc-proof.txt b/...kF1600x4_StateExtractBytes/cbmc-proof.txt → ...kF1600x4_StateExtractBytes/cbmc-proof.txt
diff --git a/...mute/KeccakF1600x4_StatePermute_harness.c → ...mute/KeccakF1600x4_StatePermute_harness.c b/...mute/KeccakF1600x4_StatePermute_harness.c → ...mute/KeccakF1600x4_StatePermute_harness.c
diff --git a/cbmc/KeccakF1600x4_StatePermute/Makefile → .../cbmc/KeccakF1600x4_StatePermute/Makefile b/cbmc/KeccakF1600x4_StatePermute/Makefile → .../cbmc/KeccakF1600x4_StatePermute/Makefile
diff --git a/...KeccakF1600x4_StatePermute/cbmc-proof.txt → ...KeccakF1600x4_StatePermute/cbmc-proof.txt b/...KeccakF1600x4_StatePermute/cbmc-proof.txt → ...KeccakF1600x4_StatePermute/cbmc-proof.txt
diff --git a/...tes/KeccakF1600x4_StateXORBytes_harness.c → ...tes/KeccakF1600x4_StateXORBytes_harness.c b/...tes/KeccakF1600x4_StateXORBytes_harness.c → ...tes/KeccakF1600x4_StateXORBytes_harness.c
diff --git a/cbmc/KeccakF1600x4_StateXORBytes/Makefile → ...cbmc/KeccakF1600x4_StateXORBytes/Makefile b/cbmc/KeccakF1600x4_StateXORBytes/Makefile → ...cbmc/KeccakF1600x4_StateXORBytes/Makefile
diff --git a/...eccakF1600x4_StateXORBytes/cbmc-proof.txt → ...eccakF1600x4_StateXORBytes/cbmc-proof.txt b/...eccakF1600x4_StateXORBytes/cbmc-proof.txt → ...eccakF1600x4_StateXORBytes/cbmc-proof.txt
diff --git a/cbmc/Makefile.common → proofs/cbmc/Makefile.common b/cbmc/Makefile.common → 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 → proofs/cbmc/Makefile_params.common b/cbmc/Makefile_params.common → proofs/cbmc/Makefile_params.common
diff --git a/cbmc/README.md → proofs/cbmc/README.md b/cbmc/README.md → proofs/cbmc/README.md
diff --git a/cbmc/barrett_reduce/Makefile → proofs/cbmc/barrett_reduce/Makefile b/cbmc/barrett_reduce/Makefile → proofs/cbmc/barrett_reduce/Makefile
diff --git a/cbmc/barrett_reduce/barrett_reduce_harness.c → ...c/barrett_reduce/barrett_reduce_harness.c b/cbmc/barrett_reduce/barrett_reduce_harness.c → ...c/barrett_reduce/barrett_reduce_harness.c
diff --git a/cbmc/barrett_reduce/cbmc-proof.txt → proofs/cbmc/barrett_reduce/cbmc-proof.txt b/cbmc/barrett_reduce/cbmc-proof.txt → proofs/cbmc/barrett_reduce/cbmc-proof.txt
diff --git a/cbmc/basemul_cached/Makefile → proofs/cbmc/basemul_cached/Makefile b/cbmc/basemul_cached/Makefile → proofs/cbmc/basemul_cached/Makefile
diff --git a/cbmc/basemul_cached/basemul_cached_harness.c → ...c/basemul_cached/basemul_cached_harness.c b/cbmc/basemul_cached/basemul_cached_harness.c → ...c/basemul_cached/basemul_cached_harness.c
diff --git a/cbmc/basemul_cached/cbmc-proof.txt → proofs/cbmc/basemul_cached/cbmc-proof.txt b/cbmc/basemul_cached/cbmc-proof.txt → proofs/cbmc/basemul_cached/cbmc-proof.txt
diff --git a/cbmc/crypto_kem_dec/Makefile → proofs/cbmc/crypto_kem_dec/Makefile b/cbmc/crypto_kem_dec/Makefile → proofs/cbmc/crypto_kem_dec/Makefile
diff --git a/cbmc/crypto_kem_dec/cbmc-proof.txt → proofs/cbmc/crypto_kem_dec/cbmc-proof.txt b/cbmc/crypto_kem_dec/cbmc-proof.txt → proofs/cbmc/crypto_kem_dec/cbmc-proof.txt
diff --git a/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c → ...c/crypto_kem_dec/crypto_kem_dec_harness.c b/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c → ...c/crypto_kem_dec/crypto_kem_dec_harness.c
diff --git a/cbmc/crypto_kem_enc/Makefile → proofs/cbmc/crypto_kem_enc/Makefile b/cbmc/crypto_kem_enc/Makefile → proofs/cbmc/crypto_kem_enc/Makefile
diff --git a/cbmc/crypto_kem_enc/cbmc-proof.txt → proofs/cbmc/crypto_kem_enc/cbmc-proof.txt b/cbmc/crypto_kem_enc/cbmc-proof.txt → proofs/cbmc/crypto_kem_enc/cbmc-proof.txt
diff --git a/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c → ...c/crypto_kem_enc/crypto_kem_enc_harness.c b/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c → ...c/crypto_kem_enc/crypto_kem_enc_harness.c
diff --git a/cbmc/crypto_kem_enc_derand/Makefile → proofs/cbmc/crypto_kem_enc_derand/Makefile b/cbmc/crypto_kem_enc_derand/Makefile → proofs/cbmc/crypto_kem_enc_derand/Makefile
diff --git a/cbmc/crypto_kem_enc_derand/cbmc-proof.txt → ...cbmc/crypto_kem_enc_derand/cbmc-proof.txt b/cbmc/crypto_kem_enc_derand/cbmc-proof.txt → ...cbmc/crypto_kem_enc_derand/cbmc-proof.txt
diff --git a/...nc_derand/crypto_kem_enc_derand_harness.c → ...nc_derand/crypto_kem_enc_derand_harness.c b/...nc_derand/crypto_kem_enc_derand_harness.c → ...nc_derand/crypto_kem_enc_derand_harness.c
diff --git a/cbmc/crypto_kem_keypair/Makefile → proofs/cbmc/crypto_kem_keypair/Makefile b/cbmc/crypto_kem_keypair/Makefile → proofs/cbmc/crypto_kem_keypair/Makefile
diff --git a/cbmc/crypto_kem_keypair/cbmc-proof.txt → ...fs/cbmc/crypto_kem_keypair/cbmc-proof.txt b/cbmc/crypto_kem_keypair/cbmc-proof.txt → ...fs/cbmc/crypto_kem_keypair/cbmc-proof.txt
diff --git a/..._kem_keypair/crypto_kem_keypair_harness.c → ..._kem_keypair/crypto_kem_keypair_harness.c b/..._kem_keypair/crypto_kem_keypair_harness.c → ..._kem_keypair/crypto_kem_keypair_harness.c
diff --git a/cbmc/crypto_kem_keypair_derand/Makefile → ...s/cbmc/crypto_kem_keypair_derand/Makefile b/cbmc/crypto_kem_keypair_derand/Makefile → ...s/cbmc/crypto_kem_keypair_derand/Makefile
diff --git a/.../crypto_kem_keypair_derand/cbmc-proof.txt → .../crypto_kem_keypair_derand/cbmc-proof.txt b/.../crypto_kem_keypair_derand/cbmc-proof.txt → .../crypto_kem_keypair_derand/cbmc-proof.txt
diff --git a/...erand/crypto_kem_keypair_derand_harness.c → ...erand/crypto_kem_keypair_derand_harness.c b/...erand/crypto_kem_keypair_derand_harness.c → ...erand/crypto_kem_keypair_derand_harness.c
diff --git a/cbmc/ct_cmask_neg_i16/Makefile → proofs/cbmc/ct_cmask_neg_i16/Makefile b/cbmc/ct_cmask_neg_i16/Makefile → proofs/cbmc/ct_cmask_neg_i16/Makefile
diff --git a/cbmc/ct_cmask_neg_i16/cbmc-proof.txt → proofs/cbmc/ct_cmask_neg_i16/cbmc-proof.txt b/cbmc/ct_cmask_neg_i16/cbmc-proof.txt → proofs/cbmc/ct_cmask_neg_i16/cbmc-proof.txt
diff --git a/..._cmask_neg_i16/ct_cmask_neg_i16_harness.c → ..._cmask_neg_i16/ct_cmask_neg_i16_harness.c b/..._cmask_neg_i16/ct_cmask_neg_i16_harness.c → ..._cmask_neg_i16/ct_cmask_neg_i16_harness.c
diff --git a/cbmc/ct_cmask_nonzero_u16/Makefile → proofs/cbmc/ct_cmask_nonzero_u16/Makefile b/cbmc/ct_cmask_nonzero_u16/Makefile → proofs/cbmc/ct_cmask_nonzero_u16/Makefile
diff --git a/cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt → .../cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt b/cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt → .../cbmc/ct_cmask_nonzero_u16/cbmc-proof.txt
diff --git a/...onzero_u16/ct_cmask_nonzero_u16_harness.c → ...onzero_u16/ct_cmask_nonzero_u16_harness.c b/...onzero_u16/ct_cmask_nonzero_u16_harness.c → ...onzero_u16/ct_cmask_nonzero_u16_harness.c
diff --git a/cbmc/ct_cmask_nonzero_u8/Makefile → proofs/cbmc/ct_cmask_nonzero_u8/Makefile b/cbmc/ct_cmask_nonzero_u8/Makefile → proofs/cbmc/ct_cmask_nonzero_u8/Makefile
diff --git a/cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt → ...s/cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt b/cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt → ...s/cbmc/ct_cmask_nonzero_u8/cbmc-proof.txt
diff --git a/..._nonzero_u8/ct_cmask_nonzero_u8_harness.c → ..._nonzero_u8/ct_cmask_nonzero_u8_harness.c b/..._nonzero_u8/ct_cmask_nonzero_u8_harness.c → ..._nonzero_u8/ct_cmask_nonzero_u8_harness.c
diff --git a/cbmc/ct_cmov_zero/Makefile → proofs/cbmc/ct_cmov_zero/Makefile b/cbmc/ct_cmov_zero/Makefile → proofs/cbmc/ct_cmov_zero/Makefile
diff --git a/cbmc/ct_cmov_zero/cbmc-proof.txt → proofs/cbmc/ct_cmov_zero/cbmc-proof.txt b/cbmc/ct_cmov_zero/cbmc-proof.txt → proofs/cbmc/ct_cmov_zero/cbmc-proof.txt
diff --git a/cbmc/ct_cmov_zero/ct_cmov_zero_harness.c → .../cbmc/ct_cmov_zero/ct_cmov_zero_harness.c b/cbmc/ct_cmov_zero/ct_cmov_zero_harness.c → .../cbmc/ct_cmov_zero/ct_cmov_zero_harness.c
diff --git a/cbmc/ct_memcmp/Makefile → proofs/cbmc/ct_memcmp/Makefile b/cbmc/ct_memcmp/Makefile → proofs/cbmc/ct_memcmp/Makefile
diff --git a/cbmc/ct_memcmp/cbmc-proof.txt → proofs/cbmc/ct_memcmp/cbmc-proof.txt b/cbmc/ct_memcmp/cbmc-proof.txt → proofs/cbmc/ct_memcmp/cbmc-proof.txt
diff --git a/cbmc/ct_memcmp/ct_memcmp_harness.c → proofs/cbmc/ct_memcmp/ct_memcmp_harness.c b/cbmc/ct_memcmp/ct_memcmp_harness.c → proofs/cbmc/ct_memcmp/ct_memcmp_harness.c
diff --git a/cbmc/ct_sel_int16/Makefile → proofs/cbmc/ct_sel_int16/Makefile b/cbmc/ct_sel_int16/Makefile → proofs/cbmc/ct_sel_int16/Makefile
diff --git a/cbmc/ct_sel_int16/cbmc-proof.txt → proofs/cbmc/ct_sel_int16/cbmc-proof.txt b/cbmc/ct_sel_int16/cbmc-proof.txt → proofs/cbmc/ct_sel_int16/cbmc-proof.txt
diff --git a/cbmc/ct_sel_int16/ct_sel_int16_harness.c → .../cbmc/ct_sel_int16/ct_sel_int16_harness.c b/cbmc/ct_sel_int16/ct_sel_int16_harness.c → .../cbmc/ct_sel_int16/ct_sel_int16_harness.c
diff --git a/cbmc/ct_sel_uint8/Makefile → proofs/cbmc/ct_sel_uint8/Makefile b/cbmc/ct_sel_uint8/Makefile → proofs/cbmc/ct_sel_uint8/Makefile
diff --git a/cbmc/ct_sel_uint8/cbmc-proof.txt → proofs/cbmc/ct_sel_uint8/cbmc-proof.txt b/cbmc/ct_sel_uint8/cbmc-proof.txt → proofs/cbmc/ct_sel_uint8/cbmc-proof.txt
diff --git a/cbmc/ct_sel_uint8/ct_sel_uint8_harness.c → .../cbmc/ct_sel_uint8/ct_sel_uint8_harness.c b/cbmc/ct_sel_uint8/ct_sel_uint8_harness.c → .../cbmc/ct_sel_uint8/ct_sel_uint8_harness.c
diff --git a/cbmc/fqmul/Makefile → proofs/cbmc/fqmul/Makefile b/cbmc/fqmul/Makefile → proofs/cbmc/fqmul/Makefile
diff --git a/cbmc/fqmul/cbmc-proof.txt → proofs/cbmc/fqmul/cbmc-proof.txt b/cbmc/fqmul/cbmc-proof.txt → proofs/cbmc/fqmul/cbmc-proof.txt
diff --git a/cbmc/fqmul/fqmul_harness.c → proofs/cbmc/fqmul/fqmul_harness.c b/cbmc/fqmul/fqmul_harness.c → proofs/cbmc/fqmul/fqmul_harness.c
diff --git a/cbmc/gen_matrix/Makefile → proofs/cbmc/gen_matrix/Makefile b/cbmc/gen_matrix/Makefile → proofs/cbmc/gen_matrix/Makefile
diff --git a/cbmc/gen_matrix/cbmc-proof.txt → proofs/cbmc/gen_matrix/cbmc-proof.txt b/cbmc/gen_matrix/cbmc-proof.txt → proofs/cbmc/gen_matrix/cbmc-proof.txt
diff --git a/cbmc/gen_matrix/gen_matrix_harness.c → proofs/cbmc/gen_matrix/gen_matrix_harness.c b/cbmc/gen_matrix/gen_matrix_harness.c → proofs/cbmc/gen_matrix/gen_matrix_harness.c
diff --git a/cbmc/gen_matrix_entry/Makefile → proofs/cbmc/gen_matrix_entry/Makefile b/cbmc/gen_matrix_entry/Makefile → proofs/cbmc/gen_matrix_entry/Makefile
diff --git a/cbmc/gen_matrix_entry/cbmc-proof.txt → proofs/cbmc/gen_matrix_entry/cbmc-proof.txt b/cbmc/gen_matrix_entry/cbmc-proof.txt → proofs/cbmc/gen_matrix_entry/cbmc-proof.txt
diff --git a/...n_matrix_entry/gen_matrix_entry_harness.c → ...n_matrix_entry/gen_matrix_entry_harness.c b/...n_matrix_entry/gen_matrix_entry_harness.c → ...n_matrix_entry/gen_matrix_entry_harness.c
diff --git a/cbmc/gen_matrix_entry_x4/Makefile → proofs/cbmc/gen_matrix_entry_x4/Makefile b/cbmc/gen_matrix_entry_x4/Makefile → proofs/cbmc/gen_matrix_entry_x4/Makefile
diff --git a/cbmc/gen_matrix_entry_x4/cbmc-proof.txt → ...s/cbmc/gen_matrix_entry_x4/cbmc-proof.txt b/cbmc/gen_matrix_entry_x4/cbmc-proof.txt → ...s/cbmc/gen_matrix_entry_x4/cbmc-proof.txt
diff --git a/...ix_entry_x4/gen_matrix_entry_x4_harness.c → ...ix_entry_x4/gen_matrix_entry_x4_harness.c b/...ix_entry_x4/gen_matrix_entry_x4_harness.c → ...ix_entry_x4/gen_matrix_entry_x4_harness.c
diff --git a/cbmc/indcpa_dec/Makefile → proofs/cbmc/indcpa_dec/Makefile b/cbmc/indcpa_dec/Makefile → proofs/cbmc/indcpa_dec/Makefile
diff --git a/cbmc/indcpa_dec/cbmc-proof.txt → proofs/cbmc/indcpa_dec/cbmc-proof.txt b/cbmc/indcpa_dec/cbmc-proof.txt → proofs/cbmc/indcpa_dec/cbmc-proof.txt
diff --git a/cbmc/indcpa_dec/indcpa_dec_harness.c → proofs/cbmc/indcpa_dec/indcpa_dec_harness.c b/cbmc/indcpa_dec/indcpa_dec_harness.c → proofs/cbmc/indcpa_dec/indcpa_dec_harness.c
diff --git a/cbmc/indcpa_enc/Makefile → proofs/cbmc/indcpa_enc/Makefile b/cbmc/indcpa_enc/Makefile → proofs/cbmc/indcpa_enc/Makefile
diff --git a/cbmc/indcpa_enc/cbmc-proof.txt → proofs/cbmc/indcpa_enc/cbmc-proof.txt b/cbmc/indcpa_enc/cbmc-proof.txt → proofs/cbmc/indcpa_enc/cbmc-proof.txt
diff --git a/cbmc/indcpa_enc/indcpa_enc_harness.c → proofs/cbmc/indcpa_enc/indcpa_enc_harness.c b/cbmc/indcpa_enc/indcpa_enc_harness.c → proofs/cbmc/indcpa_enc/indcpa_enc_harness.c
diff --git a/cbmc/indcpa_keypair_derand/Makefile → proofs/cbmc/indcpa_keypair_derand/Makefile b/cbmc/indcpa_keypair_derand/Makefile → proofs/cbmc/indcpa_keypair_derand/Makefile
diff --git a/cbmc/indcpa_keypair_derand/cbmc-proof.txt → ...cbmc/indcpa_keypair_derand/cbmc-proof.txt b/cbmc/indcpa_keypair_derand/cbmc-proof.txt → ...cbmc/indcpa_keypair_derand/cbmc-proof.txt
diff --git a/...ir_derand/indcpa_keypair_derand_harness.c → ...ir_derand/indcpa_keypair_derand_harness.c b/...ir_derand/indcpa_keypair_derand_harness.c → ...ir_derand/indcpa_keypair_derand_harness.c
diff --git a/cbmc/invntt_layer/Makefile → proofs/cbmc/invntt_layer/Makefile b/cbmc/invntt_layer/Makefile → proofs/cbmc/invntt_layer/Makefile
diff --git a/cbmc/invntt_layer/cbmc-proof.txt → proofs/cbmc/invntt_layer/cbmc-proof.txt b/cbmc/invntt_layer/cbmc-proof.txt → proofs/cbmc/invntt_layer/cbmc-proof.txt
diff --git a/cbmc/invntt_layer/invntt_layer_harness.c → .../cbmc/invntt_layer/invntt_layer_harness.c b/cbmc/invntt_layer/invntt_layer_harness.c → .../cbmc/invntt_layer/invntt_layer_harness.c
diff --git a/cbmc/keccak_absorb_once/Makefile → proofs/cbmc/keccak_absorb_once/Makefile b/cbmc/keccak_absorb_once/Makefile → proofs/cbmc/keccak_absorb_once/Makefile
diff --git a/cbmc/keccak_absorb_once/cbmc-proof.txt → ...fs/cbmc/keccak_absorb_once/cbmc-proof.txt b/cbmc/keccak_absorb_once/cbmc-proof.txt → ...fs/cbmc/keccak_absorb_once/cbmc-proof.txt
diff --git a/..._absorb_once/keccak_absorb_once_harness.c → ..._absorb_once/keccak_absorb_once_harness.c b/..._absorb_once/keccak_absorb_once_harness.c → ..._absorb_once/keccak_absorb_once_harness.c
diff --git a/cbmc/keccak_absorb_once_x4/Makefile → proofs/cbmc/keccak_absorb_once_x4/Makefile b/cbmc/keccak_absorb_once_x4/Makefile → proofs/cbmc/keccak_absorb_once_x4/Makefile
diff --git a/cbmc/keccak_absorb_once_x4/cbmc-proof.txt → ...cbmc/keccak_absorb_once_x4/cbmc-proof.txt b/cbmc/keccak_absorb_once_x4/cbmc-proof.txt → ...cbmc/keccak_absorb_once_x4/cbmc-proof.txt
diff --git a/...b_once_x4/keccak_absorb_once_x4_harness.c → ...b_once_x4/keccak_absorb_once_x4_harness.c b/...b_once_x4/keccak_absorb_once_x4_harness.c → ...b_once_x4/keccak_absorb_once_x4_harness.c
diff --git a/cbmc/keccak_squeeze_once/Makefile → proofs/cbmc/keccak_squeeze_once/Makefile b/cbmc/keccak_squeeze_once/Makefile → proofs/cbmc/keccak_squeeze_once/Makefile
diff --git a/cbmc/keccak_squeeze_once/cbmc-proof.txt → ...s/cbmc/keccak_squeeze_once/cbmc-proof.txt b/cbmc/keccak_squeeze_once/cbmc-proof.txt → ...s/cbmc/keccak_squeeze_once/cbmc-proof.txt
diff --git a/...queeze_once/keccak_squeeze_once_harness.c → ...queeze_once/keccak_squeeze_once_harness.c b/...queeze_once/keccak_squeeze_once_harness.c → ...queeze_once/keccak_squeeze_once_harness.c
diff --git a/cbmc/keccak_squeezeblocks/Makefile → proofs/cbmc/keccak_squeezeblocks/Makefile b/cbmc/keccak_squeezeblocks/Makefile → proofs/cbmc/keccak_squeezeblocks/Makefile
diff --git a/cbmc/keccak_squeezeblocks/cbmc-proof.txt → .../cbmc/keccak_squeezeblocks/cbmc-proof.txt b/cbmc/keccak_squeezeblocks/cbmc-proof.txt → .../cbmc/keccak_squeezeblocks/cbmc-proof.txt
diff --git a/...eezeblocks/keccak_squeezeblocks_harness.c → ...eezeblocks/keccak_squeezeblocks_harness.c b/...eezeblocks/keccak_squeezeblocks_harness.c → ...eezeblocks/keccak_squeezeblocks_harness.c
diff --git a/cbmc/keccak_squeezeblocks_x4/Makefile → proofs/cbmc/keccak_squeezeblocks_x4/Makefile b/cbmc/keccak_squeezeblocks_x4/Makefile → proofs/cbmc/keccak_squeezeblocks_x4/Makefile
diff --git a/cbmc/keccak_squeezeblocks_x4/cbmc-proof.txt → ...mc/keccak_squeezeblocks_x4/cbmc-proof.txt b/cbmc/keccak_squeezeblocks_x4/cbmc-proof.txt → ...mc/keccak_squeezeblocks_x4/cbmc-proof.txt
diff --git a/...ocks_x4/keccak_squeezeblocks_x4_harness.c → ...ocks_x4/keccak_squeezeblocks_x4_harness.c b/...ocks_x4/keccak_squeezeblocks_x4_harness.c → ...ocks_x4/keccak_squeezeblocks_x4_harness.c
diff --git a/cbmc/keccakf1600_extractbytes/Makefile → ...fs/cbmc/keccakf1600_extractbytes/Makefile b/cbmc/keccakf1600_extractbytes/Makefile → ...fs/cbmc/keccakf1600_extractbytes/Makefile
diff --git a/cbmc/keccakf1600_permute/Makefile → proofs/cbmc/keccakf1600_permute/Makefile b/cbmc/keccakf1600_permute/Makefile → proofs/cbmc/keccakf1600_permute/Makefile
diff --git a/cbmc/keccakf1600_xorbytes/Makefile → proofs/cbmc/keccakf1600_xorbytes/Makefile b/cbmc/keccakf1600_xorbytes/Makefile → proofs/cbmc/keccakf1600_xorbytes/Makefile
diff --git a/cbmc/lib/__init__.py → proofs/cbmc/lib/__init__.py b/cbmc/lib/__init__.py → proofs/cbmc/lib/__init__.py
diff --git a/cbmc/lib/print_tool_versions.py → proofs/cbmc/lib/print_tool_versions.py b/cbmc/lib/print_tool_versions.py → proofs/cbmc/lib/print_tool_versions.py
diff --git a/cbmc/lib/summarize.py → proofs/cbmc/lib/summarize.py b/cbmc/lib/summarize.py → proofs/cbmc/lib/summarize.py
diff --git a/cbmc/matvec_mul/Makefile → proofs/cbmc/matvec_mul/Makefile b/cbmc/matvec_mul/Makefile → proofs/cbmc/matvec_mul/Makefile
diff --git a/cbmc/matvec_mul/cbmc-proof.txt → proofs/cbmc/matvec_mul/cbmc-proof.txt b/cbmc/matvec_mul/cbmc-proof.txt → proofs/cbmc/matvec_mul/cbmc-proof.txt
diff --git a/cbmc/matvec_mul/matvec_mul_harness.c → proofs/cbmc/matvec_mul/matvec_mul_harness.c b/cbmc/matvec_mul/matvec_mul_harness.c → proofs/cbmc/matvec_mul/matvec_mul_harness.c
diff --git a/cbmc/montgomery_reduce/Makefile → proofs/cbmc/montgomery_reduce/Makefile b/cbmc/montgomery_reduce/Makefile → proofs/cbmc/montgomery_reduce/Makefile
diff --git a/cbmc/montgomery_reduce/cbmc-proof.txt → proofs/cbmc/montgomery_reduce/cbmc-proof.txt b/cbmc/montgomery_reduce/cbmc-proof.txt → proofs/cbmc/montgomery_reduce/cbmc-proof.txt
diff --git a/...gomery_reduce/montgomery_reduce_harness.c → ...gomery_reduce/montgomery_reduce_harness.c b/...gomery_reduce/montgomery_reduce_harness.c → ...gomery_reduce/montgomery_reduce_harness.c
diff --git a/cbmc/ntt_butterfly_block/Makefile → proofs/cbmc/ntt_butterfly_block/Makefile b/cbmc/ntt_butterfly_block/Makefile → proofs/cbmc/ntt_butterfly_block/Makefile
diff --git a/cbmc/ntt_butterfly_block/cbmc-proof.txt → ...s/cbmc/ntt_butterfly_block/cbmc-proof.txt b/cbmc/ntt_butterfly_block/cbmc-proof.txt → ...s/cbmc/ntt_butterfly_block/cbmc-proof.txt
diff --git a/...erfly_block/ntt_butterfly_block_harness.c → ...erfly_block/ntt_butterfly_block_harness.c b/...erfly_block/ntt_butterfly_block_harness.c → ...erfly_block/ntt_butterfly_block_harness.c
diff --git a/cbmc/ntt_layer/Makefile → proofs/cbmc/ntt_layer/Makefile b/cbmc/ntt_layer/Makefile → proofs/cbmc/ntt_layer/Makefile
diff --git a/cbmc/ntt_layer/cbmc-proof.txt → proofs/cbmc/ntt_layer/cbmc-proof.txt b/cbmc/ntt_layer/cbmc-proof.txt → proofs/cbmc/ntt_layer/cbmc-proof.txt
diff --git a/cbmc/ntt_layer/ntt_layer_harness.c → proofs/cbmc/ntt_layer/ntt_layer_harness.c b/cbmc/ntt_layer/ntt_layer_harness.c → proofs/cbmc/ntt_layer/ntt_layer_harness.c
diff --git a/cbmc/poly_add/Makefile → proofs/cbmc/poly_add/Makefile b/cbmc/poly_add/Makefile → proofs/cbmc/poly_add/Makefile
diff --git a/cbmc/poly_add/cbmc-proof.txt → proofs/cbmc/poly_add/cbmc-proof.txt b/cbmc/poly_add/cbmc-proof.txt → proofs/cbmc/poly_add/cbmc-proof.txt
diff --git a/cbmc/poly_add/poly_add_harness.c → proofs/cbmc/poly_add/poly_add_harness.c b/cbmc/poly_add/poly_add_harness.c → proofs/cbmc/poly_add/poly_add_harness.c
diff --git a/cbmc/poly_basemul_montgomery_cached/Makefile → ...c/poly_basemul_montgomery_cached/Makefile b/cbmc/poly_basemul_montgomery_cached/Makefile → ...c/poly_basemul_montgomery_cached/Makefile
diff --git a/..._basemul_montgomery_cached/cbmc-proof.txt → ..._basemul_montgomery_cached/cbmc-proof.txt b/..._basemul_montgomery_cached/cbmc-proof.txt → ..._basemul_montgomery_cached/cbmc-proof.txt
diff --git a/.../poly_basemul_montgomery_cached_harness.c → .../poly_basemul_montgomery_cached_harness.c b/.../poly_basemul_montgomery_cached_harness.c → .../poly_basemul_montgomery_cached_harness.c
diff --git a/cbmc/poly_cbd_eta1/Makefile → proofs/cbmc/poly_cbd_eta1/Makefile b/cbmc/poly_cbd_eta1/Makefile → proofs/cbmc/poly_cbd_eta1/Makefile
diff --git a/cbmc/poly_cbd_eta1/cbmc-proof.txt → proofs/cbmc/poly_cbd_eta1/cbmc-proof.txt b/cbmc/poly_cbd_eta1/cbmc-proof.txt → proofs/cbmc/poly_cbd_eta1/cbmc-proof.txt
diff --git a/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c → ...bmc/poly_cbd_eta1/poly_cbd_eta1_harness.c b/cbmc/poly_cbd_eta1/poly_cbd_eta1_harness.c → ...bmc/poly_cbd_eta1/poly_cbd_eta1_harness.c
diff --git a/cbmc/poly_cbd_eta2/Makefile → proofs/cbmc/poly_cbd_eta2/Makefile b/cbmc/poly_cbd_eta2/Makefile → proofs/cbmc/poly_cbd_eta2/Makefile
diff --git a/cbmc/poly_cbd_eta2/cbmc-proof.txt → proofs/cbmc/poly_cbd_eta2/cbmc-proof.txt b/cbmc/poly_cbd_eta2/cbmc-proof.txt → proofs/cbmc/poly_cbd_eta2/cbmc-proof.txt
diff --git a/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c → ...bmc/poly_cbd_eta2/poly_cbd_eta2_harness.c b/cbmc/poly_cbd_eta2/poly_cbd_eta2_harness.c → ...bmc/poly_cbd_eta2/poly_cbd_eta2_harness.c
diff --git a/cbmc/poly_compress_du/Makefile → proofs/cbmc/poly_compress_du/Makefile b/cbmc/poly_compress_du/Makefile → proofs/cbmc/poly_compress_du/Makefile
diff --git a/cbmc/poly_compress_du/cbmc-proof.txt → proofs/cbmc/poly_compress_du/cbmc-proof.txt b/cbmc/poly_compress_du/cbmc-proof.txt → proofs/cbmc/poly_compress_du/cbmc-proof.txt
diff --git a/...ly_compress_du/poly_compress_du_harness.c → ...ly_compress_du/poly_compress_du_harness.c b/...ly_compress_du/poly_compress_du_harness.c → ...ly_compress_du/poly_compress_du_harness.c
diff --git a/cbmc/poly_compress_dv/Makefile → proofs/cbmc/poly_compress_dv/Makefile b/cbmc/poly_compress_dv/Makefile → proofs/cbmc/poly_compress_dv/Makefile
diff --git a/cbmc/poly_compress_dv/cbmc-proof.txt → proofs/cbmc/poly_compress_dv/cbmc-proof.txt b/cbmc/poly_compress_dv/cbmc-proof.txt → proofs/cbmc/poly_compress_dv/cbmc-proof.txt
diff --git a/...ly_compress_dv/poly_compress_dv_harness.c → ...ly_compress_dv/poly_compress_dv_harness.c b/...ly_compress_dv/poly_compress_dv_harness.c → ...ly_compress_dv/poly_compress_dv_harness.c
diff --git a/cbmc/poly_decompress_du/Makefile → proofs/cbmc/poly_decompress_du/Makefile b/cbmc/poly_decompress_du/Makefile → proofs/cbmc/poly_decompress_du/Makefile
diff --git a/cbmc/poly_decompress_du/cbmc-proof.txt → ...fs/cbmc/poly_decompress_du/cbmc-proof.txt b/cbmc/poly_decompress_du/cbmc-proof.txt → ...fs/cbmc/poly_decompress_du/cbmc-proof.txt
diff --git a/...ecompress_du/poly_decompress_du_harness.c → ...ecompress_du/poly_decompress_du_harness.c b/...ecompress_du/poly_decompress_du_harness.c → ...ecompress_du/poly_decompress_du_harness.c
diff --git a/cbmc/poly_decompress_dv/Makefile → proofs/cbmc/poly_decompress_dv/Makefile b/cbmc/poly_decompress_dv/Makefile → proofs/cbmc/poly_decompress_dv/Makefile
diff --git a/cbmc/poly_decompress_dv/cbmc-proof.txt → ...fs/cbmc/poly_decompress_dv/cbmc-proof.txt b/cbmc/poly_decompress_dv/cbmc-proof.txt → ...fs/cbmc/poly_decompress_dv/cbmc-proof.txt
diff --git a/...ecompress_dv/poly_decompress_dv_harness.c → ...ecompress_dv/poly_decompress_dv_harness.c b/...ecompress_dv/poly_decompress_dv_harness.c → ...ecompress_dv/poly_decompress_dv_harness.c
diff --git a/cbmc/poly_frombytes/Makefile → proofs/cbmc/poly_frombytes/Makefile b/cbmc/poly_frombytes/Makefile → proofs/cbmc/poly_frombytes/Makefile
diff --git a/cbmc/poly_frombytes/cbmc-proof.txt → proofs/cbmc/poly_frombytes/cbmc-proof.txt b/cbmc/poly_frombytes/cbmc-proof.txt → proofs/cbmc/poly_frombytes/cbmc-proof.txt
diff --git a/cbmc/poly_frombytes/poly_frombytes_harness.c → ...c/poly_frombytes/poly_frombytes_harness.c b/cbmc/poly_frombytes/poly_frombytes_harness.c → ...c/poly_frombytes/poly_frombytes_harness.c
diff --git a/cbmc/poly_frommsg/Makefile → proofs/cbmc/poly_frommsg/Makefile b/cbmc/poly_frommsg/Makefile → proofs/cbmc/poly_frommsg/Makefile
diff --git a/cbmc/poly_frommsg/cbmc-proof.txt → proofs/cbmc/poly_frommsg/cbmc-proof.txt b/cbmc/poly_frommsg/cbmc-proof.txt → proofs/cbmc/poly_frommsg/cbmc-proof.txt
diff --git a/cbmc/poly_frommsg/poly_frommsg_harness.c → .../cbmc/poly_frommsg/poly_frommsg_harness.c b/cbmc/poly_frommsg/poly_frommsg_harness.c → .../cbmc/poly_frommsg/poly_frommsg_harness.c
diff --git a/cbmc/poly_getnoise_eta1122_4x/Makefile → ...fs/cbmc/poly_getnoise_eta1122_4x/Makefile b/cbmc/poly_getnoise_eta1122_4x/Makefile → ...fs/cbmc/poly_getnoise_eta1122_4x/Makefile
diff --git a/cbmc/poly_getnoise_eta1122_4x/cbmc-proof.txt → ...c/poly_getnoise_eta1122_4x/cbmc-proof.txt b/cbmc/poly_getnoise_eta1122_4x/cbmc-proof.txt → ...c/poly_getnoise_eta1122_4x/cbmc-proof.txt
diff --git a/...122_4x/poly_getnoise_eta1122_4x_harness.c → ...122_4x/poly_getnoise_eta1122_4x_harness.c b/...122_4x/poly_getnoise_eta1122_4x_harness.c → ...122_4x/poly_getnoise_eta1122_4x_harness.c
diff --git a/cbmc/poly_getnoise_eta1_4x/Makefile → proofs/cbmc/poly_getnoise_eta1_4x/Makefile b/cbmc/poly_getnoise_eta1_4x/Makefile → proofs/cbmc/poly_getnoise_eta1_4x/Makefile
diff --git a/cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt → ...cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt b/cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt → ...cbmc/poly_getnoise_eta1_4x/cbmc-proof.txt
diff --git a/...e_eta1_4x/poly_getnoise_eta1_4x_harness.c → ...e_eta1_4x/poly_getnoise_eta1_4x_harness.c b/...e_eta1_4x/poly_getnoise_eta1_4x_harness.c → ...e_eta1_4x/poly_getnoise_eta1_4x_harness.c
diff --git a/cbmc/poly_getnoise_eta2/Makefile → proofs/cbmc/poly_getnoise_eta2/Makefile b/cbmc/poly_getnoise_eta2/Makefile → proofs/cbmc/poly_getnoise_eta2/Makefile
diff --git a/cbmc/poly_getnoise_eta2/cbmc-proof.txt → ...fs/cbmc/poly_getnoise_eta2/cbmc-proof.txt b/cbmc/poly_getnoise_eta2/cbmc-proof.txt → ...fs/cbmc/poly_getnoise_eta2/cbmc-proof.txt
diff --git a/...etnoise_eta2/poly_getnoise_eta2_harness.c → ...etnoise_eta2/poly_getnoise_eta2_harness.c b/...etnoise_eta2/poly_getnoise_eta2_harness.c → ...etnoise_eta2/poly_getnoise_eta2_harness.c
diff --git a/cbmc/poly_invntt_tomont/Makefile → proofs/cbmc/poly_invntt_tomont/Makefile b/cbmc/poly_invntt_tomont/Makefile → proofs/cbmc/poly_invntt_tomont/Makefile
diff --git a/cbmc/poly_invntt_tomont/cbmc-proof.txt → ...fs/cbmc/poly_invntt_tomont/cbmc-proof.txt b/cbmc/poly_invntt_tomont/cbmc-proof.txt → ...fs/cbmc/poly_invntt_tomont/cbmc-proof.txt
diff --git a/...nvntt_tomont/poly_invntt_tomont_harness.c → ...nvntt_tomont/poly_invntt_tomont_harness.c b/...nvntt_tomont/poly_invntt_tomont_harness.c → ...nvntt_tomont/poly_invntt_tomont_harness.c
diff --git a/cbmc/poly_mulcache_compute/Makefile → proofs/cbmc/poly_mulcache_compute/Makefile b/cbmc/poly_mulcache_compute/Makefile → proofs/cbmc/poly_mulcache_compute/Makefile
diff --git a/cbmc/poly_mulcache_compute/cbmc-proof.txt → ...cbmc/poly_mulcache_compute/cbmc-proof.txt b/cbmc/poly_mulcache_compute/cbmc-proof.txt → ...cbmc/poly_mulcache_compute/cbmc-proof.txt
diff --git a/...e_compute/poly_mulcache_compute_harness.c → ...e_compute/poly_mulcache_compute_harness.c b/...e_compute/poly_mulcache_compute_harness.c → ...e_compute/poly_mulcache_compute_harness.c
diff --git a/cbmc/poly_ntt/Makefile → proofs/cbmc/poly_ntt/Makefile b/cbmc/poly_ntt/Makefile → proofs/cbmc/poly_ntt/Makefile
diff --git a/cbmc/poly_ntt/cbmc-proof.txt → proofs/cbmc/poly_ntt/cbmc-proof.txt b/cbmc/poly_ntt/cbmc-proof.txt → proofs/cbmc/poly_ntt/cbmc-proof.txt
diff --git a/cbmc/poly_ntt/poly_ntt_harness.c → proofs/cbmc/poly_ntt/poly_ntt_harness.c b/cbmc/poly_ntt/poly_ntt_harness.c → proofs/cbmc/poly_ntt/poly_ntt_harness.c
diff --git a/cbmc/poly_reduce/Makefile → proofs/cbmc/poly_reduce/Makefile b/cbmc/poly_reduce/Makefile → proofs/cbmc/poly_reduce/Makefile
diff --git a/cbmc/poly_reduce/cbmc-proof.txt → proofs/cbmc/poly_reduce/cbmc-proof.txt b/cbmc/poly_reduce/cbmc-proof.txt → proofs/cbmc/poly_reduce/cbmc-proof.txt
diff --git a/cbmc/poly_reduce/poly_reduce_harness.c → ...fs/cbmc/poly_reduce/poly_reduce_harness.c b/cbmc/poly_reduce/poly_reduce_harness.c → ...fs/cbmc/poly_reduce/poly_reduce_harness.c
diff --git a/cbmc/poly_sub/Makefile → proofs/cbmc/poly_sub/Makefile b/cbmc/poly_sub/Makefile → proofs/cbmc/poly_sub/Makefile
diff --git a/cbmc/poly_sub/cbmc-proof.txt → proofs/cbmc/poly_sub/cbmc-proof.txt b/cbmc/poly_sub/cbmc-proof.txt → proofs/cbmc/poly_sub/cbmc-proof.txt
diff --git a/cbmc/poly_sub/poly_sub_harness.c → proofs/cbmc/poly_sub/poly_sub_harness.c b/cbmc/poly_sub/poly_sub_harness.c → proofs/cbmc/poly_sub/poly_sub_harness.c
diff --git a/cbmc/poly_tobytes/Makefile → proofs/cbmc/poly_tobytes/Makefile b/cbmc/poly_tobytes/Makefile → proofs/cbmc/poly_tobytes/Makefile
diff --git a/cbmc/poly_tobytes/cbmc-proof.txt → proofs/cbmc/poly_tobytes/cbmc-proof.txt b/cbmc/poly_tobytes/cbmc-proof.txt → proofs/cbmc/poly_tobytes/cbmc-proof.txt
diff --git a/cbmc/poly_tobytes/poly_tobytes_harness.c → .../cbmc/poly_tobytes/poly_tobytes_harness.c b/cbmc/poly_tobytes/poly_tobytes_harness.c → .../cbmc/poly_tobytes/poly_tobytes_harness.c
diff --git a/cbmc/poly_tomont/Makefile → proofs/cbmc/poly_tomont/Makefile b/cbmc/poly_tomont/Makefile → proofs/cbmc/poly_tomont/Makefile
diff --git a/cbmc/poly_tomont/cbmc-proof.txt → proofs/cbmc/poly_tomont/cbmc-proof.txt b/cbmc/poly_tomont/cbmc-proof.txt → proofs/cbmc/poly_tomont/cbmc-proof.txt
diff --git a/cbmc/poly_tomont/poly_tomont_harness.c → ...fs/cbmc/poly_tomont/poly_tomont_harness.c b/cbmc/poly_tomont/poly_tomont_harness.c → ...fs/cbmc/poly_tomont/poly_tomont_harness.c
diff --git a/cbmc/poly_tomsg/Makefile → proofs/cbmc/poly_tomsg/Makefile b/cbmc/poly_tomsg/Makefile → proofs/cbmc/poly_tomsg/Makefile
diff --git a/cbmc/poly_tomsg/cbmc-proof.txt → proofs/cbmc/poly_tomsg/cbmc-proof.txt b/cbmc/poly_tomsg/cbmc-proof.txt → proofs/cbmc/poly_tomsg/cbmc-proof.txt
diff --git a/cbmc/poly_tomsg/poly_tomsg_harness.c → proofs/cbmc/poly_tomsg/poly_tomsg_harness.c b/cbmc/poly_tomsg/poly_tomsg_harness.c → proofs/cbmc/poly_tomsg/poly_tomsg_harness.c
diff --git a/cbmc/polyvec_add/Makefile → proofs/cbmc/polyvec_add/Makefile b/cbmc/polyvec_add/Makefile → proofs/cbmc/polyvec_add/Makefile
diff --git a/cbmc/polyvec_add/cbmc-proof.txt → proofs/cbmc/polyvec_add/cbmc-proof.txt b/cbmc/polyvec_add/cbmc-proof.txt → proofs/cbmc/polyvec_add/cbmc-proof.txt
diff --git a/cbmc/polyvec_add/polyvec_add_harness.c → ...fs/cbmc/polyvec_add/polyvec_add_harness.c b/cbmc/polyvec_add/polyvec_add_harness.c → ...fs/cbmc/polyvec_add/polyvec_add_harness.c
diff --git a/cbmc/polyvec_basemul_acc_montgomery/Makefile → ...c/polyvec_basemul_acc_montgomery/Makefile b/cbmc/polyvec_basemul_acc_montgomery/Makefile → ...c/polyvec_basemul_acc_montgomery/Makefile
diff --git a/...vec_basemul_acc_montgomery/cbmc-proof.txt → ...vec_basemul_acc_montgomery/cbmc-proof.txt b/...vec_basemul_acc_montgomery/cbmc-proof.txt → ...vec_basemul_acc_montgomery/cbmc-proof.txt
diff --git a/.../polyvec_basemul_acc_montgomery_harness.c → .../polyvec_basemul_acc_montgomery_harness.c b/.../polyvec_basemul_acc_montgomery_harness.c → .../polyvec_basemul_acc_montgomery_harness.c
diff --git a/...ec_basemul_acc_montgomery_cached/Makefile → ...ec_basemul_acc_montgomery_cached/Makefile b/...ec_basemul_acc_montgomery_cached/Makefile → ...ec_basemul_acc_montgomery_cached/Makefile
diff --git a/...emul_acc_montgomery_cached/cbmc-proof.txt → ...emul_acc_montgomery_cached/cbmc-proof.txt b/...emul_acc_montgomery_cached/cbmc-proof.txt → ...emul_acc_montgomery_cached/cbmc-proof.txt
diff --git a/...c_basemul_acc_montgomery_cached_harness.c → ...c_basemul_acc_montgomery_cached_harness.c b/...c_basemul_acc_montgomery_cached_harness.c → ...c_basemul_acc_montgomery_cached_harness.c
diff --git a/cbmc/polyvec_compress_du/Makefile → proofs/cbmc/polyvec_compress_du/Makefile b/cbmc/polyvec_compress_du/Makefile → proofs/cbmc/polyvec_compress_du/Makefile
diff --git a/cbmc/polyvec_compress_du/cbmc-proof.txt → ...s/cbmc/polyvec_compress_du/cbmc-proof.txt b/cbmc/polyvec_compress_du/cbmc-proof.txt → ...s/cbmc/polyvec_compress_du/cbmc-proof.txt
diff --git a/...compress_du/polyvec_compress_du_harness.c → ...compress_du/polyvec_compress_du_harness.c b/...compress_du/polyvec_compress_du_harness.c → ...compress_du/polyvec_compress_du_harness.c
diff --git a/cbmc/polyvec_decompress_du/Makefile → proofs/cbmc/polyvec_decompress_du/Makefile b/cbmc/polyvec_decompress_du/Makefile → proofs/cbmc/polyvec_decompress_du/Makefile
diff --git a/cbmc/polyvec_decompress_du/cbmc-proof.txt → ...cbmc/polyvec_decompress_du/cbmc-proof.txt b/cbmc/polyvec_decompress_du/cbmc-proof.txt → ...cbmc/polyvec_decompress_du/cbmc-proof.txt
diff --git a/...mpress_du/polyvec_decompress_du_harness.c → ...mpress_du/polyvec_decompress_du_harness.c b/...mpress_du/polyvec_decompress_du_harness.c → ...mpress_du/polyvec_decompress_du_harness.c
diff --git a/cbmc/polyvec_frombytes/Makefile → proofs/cbmc/polyvec_frombytes/Makefile b/cbmc/polyvec_frombytes/Makefile → proofs/cbmc/polyvec_frombytes/Makefile
diff --git a/cbmc/polyvec_frombytes/cbmc-proof.txt → proofs/cbmc/polyvec_frombytes/cbmc-proof.txt b/cbmc/polyvec_frombytes/cbmc-proof.txt → proofs/cbmc/polyvec_frombytes/cbmc-proof.txt
diff --git a/...vec_frombytes/polyvec_frombytes_harness.c → ...vec_frombytes/polyvec_frombytes_harness.c b/...vec_frombytes/polyvec_frombytes_harness.c → ...vec_frombytes/polyvec_frombytes_harness.c
diff --git a/cbmc/polyvec_invntt_tomont/Makefile → proofs/cbmc/polyvec_invntt_tomont/Makefile b/cbmc/polyvec_invntt_tomont/Makefile → proofs/cbmc/polyvec_invntt_tomont/Makefile
diff --git a/cbmc/polyvec_invntt_tomont/cbmc-proof.txt → ...cbmc/polyvec_invntt_tomont/cbmc-proof.txt b/cbmc/polyvec_invntt_tomont/cbmc-proof.txt → ...cbmc/polyvec_invntt_tomont/cbmc-proof.txt
diff --git a/...tt_tomont/polyvec_invntt_tomont_harness.c → ...tt_tomont/polyvec_invntt_tomont_harness.c b/...tt_tomont/polyvec_invntt_tomont_harness.c → ...tt_tomont/polyvec_invntt_tomont_harness.c
diff --git a/cbmc/polyvec_mulcache_compute/Makefile → ...fs/cbmc/polyvec_mulcache_compute/Makefile b/cbmc/polyvec_mulcache_compute/Makefile → ...fs/cbmc/polyvec_mulcache_compute/Makefile
diff --git a/cbmc/polyvec_mulcache_compute/cbmc-proof.txt → ...c/polyvec_mulcache_compute/cbmc-proof.txt b/cbmc/polyvec_mulcache_compute/cbmc-proof.txt → ...c/polyvec_mulcache_compute/cbmc-proof.txt
diff --git a/...ompute/polyvec_mulcache_compute_harness.c → ...ompute/polyvec_mulcache_compute_harness.c b/...ompute/polyvec_mulcache_compute_harness.c → ...ompute/polyvec_mulcache_compute_harness.c
diff --git a/cbmc/polyvec_ntt/Makefile → proofs/cbmc/polyvec_ntt/Makefile b/cbmc/polyvec_ntt/Makefile → proofs/cbmc/polyvec_ntt/Makefile
diff --git a/cbmc/polyvec_ntt/cbmc-proof.txt → proofs/cbmc/polyvec_ntt/cbmc-proof.txt b/cbmc/polyvec_ntt/cbmc-proof.txt → proofs/cbmc/polyvec_ntt/cbmc-proof.txt
diff --git a/cbmc/polyvec_ntt/polyvec_ntt_harness.c → ...fs/cbmc/polyvec_ntt/polyvec_ntt_harness.c b/cbmc/polyvec_ntt/polyvec_ntt_harness.c → ...fs/cbmc/polyvec_ntt/polyvec_ntt_harness.c
diff --git a/cbmc/polyvec_reduce/Makefile → proofs/cbmc/polyvec_reduce/Makefile b/cbmc/polyvec_reduce/Makefile → proofs/cbmc/polyvec_reduce/Makefile
diff --git a/cbmc/polyvec_reduce/cbmc-proof.txt → proofs/cbmc/polyvec_reduce/cbmc-proof.txt b/cbmc/polyvec_reduce/cbmc-proof.txt → proofs/cbmc/polyvec_reduce/cbmc-proof.txt
diff --git a/cbmc/polyvec_reduce/polyvec_reduce_harness.c → ...c/polyvec_reduce/polyvec_reduce_harness.c b/cbmc/polyvec_reduce/polyvec_reduce_harness.c → ...c/polyvec_reduce/polyvec_reduce_harness.c
diff --git a/cbmc/polyvec_tobytes/Makefile → proofs/cbmc/polyvec_tobytes/Makefile b/cbmc/polyvec_tobytes/Makefile → proofs/cbmc/polyvec_tobytes/Makefile
diff --git a/cbmc/polyvec_tobytes/cbmc-proof.txt → proofs/cbmc/polyvec_tobytes/cbmc-proof.txt b/cbmc/polyvec_tobytes/cbmc-proof.txt → proofs/cbmc/polyvec_tobytes/cbmc-proof.txt
diff --git a/...polyvec_tobytes/polyvec_tobytes_harness.c → ...polyvec_tobytes/polyvec_tobytes_harness.c b/...polyvec_tobytes/polyvec_tobytes_harness.c → ...polyvec_tobytes/polyvec_tobytes_harness.c
diff --git a/cbmc/polyvec_tomont/Makefile → proofs/cbmc/polyvec_tomont/Makefile b/cbmc/polyvec_tomont/Makefile → proofs/cbmc/polyvec_tomont/Makefile
diff --git a/cbmc/polyvec_tomont/cbmc-proof.txt → proofs/cbmc/polyvec_tomont/cbmc-proof.txt b/cbmc/polyvec_tomont/cbmc-proof.txt → proofs/cbmc/polyvec_tomont/cbmc-proof.txt
diff --git a/cbmc/polyvec_tomont/polyvec_tomont_harness.c → ...c/polyvec_tomont/polyvec_tomont_harness.c b/cbmc/polyvec_tomont/polyvec_tomont_harness.c → ...c/polyvec_tomont/polyvec_tomont_harness.c
diff --git a/cbmc/proof_guide.md → proofs/cbmc/proof_guide.md b/cbmc/proof_guide.md → 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 → proofs/cbmc/rej_uniform/Makefile b/cbmc/rej_uniform/Makefile → proofs/cbmc/rej_uniform/Makefile
diff --git a/cbmc/rej_uniform/cbmc-proof.txt → proofs/cbmc/rej_uniform/cbmc-proof.txt b/cbmc/rej_uniform/cbmc-proof.txt → proofs/cbmc/rej_uniform/cbmc-proof.txt
diff --git a/cbmc/rej_uniform/rej_uniform_harness.c → ...fs/cbmc/rej_uniform/rej_uniform_harness.c b/cbmc/rej_uniform/rej_uniform_harness.c → ...fs/cbmc/rej_uniform/rej_uniform_harness.c
diff --git a/cbmc/rej_uniform_scalar/Makefile → proofs/cbmc/rej_uniform_scalar/Makefile b/cbmc/rej_uniform_scalar/Makefile → proofs/cbmc/rej_uniform_scalar/Makefile
diff --git a/cbmc/rej_uniform_scalar/cbmc-proof.txt → ...fs/cbmc/rej_uniform_scalar/cbmc-proof.txt b/cbmc/rej_uniform_scalar/cbmc-proof.txt → ...fs/cbmc/rej_uniform_scalar/cbmc-proof.txt
diff --git a/...iform_scalar/rej_uniform_scalar_harness.c → ...iform_scalar/rej_uniform_scalar_harness.c b/...iform_scalar/rej_uniform_scalar_harness.c → ...iform_scalar/rej_uniform_scalar_harness.c
diff --git a/cbmc/run-cbmc-proofs.py → proofs/cbmc/run-cbmc-proofs.py b/cbmc/run-cbmc-proofs.py → proofs/cbmc/run-cbmc-proofs.py
diff --git a/cbmc/scalar_compress_d1/Makefile → proofs/cbmc/scalar_compress_d1/Makefile b/cbmc/scalar_compress_d1/Makefile → proofs/cbmc/scalar_compress_d1/Makefile
diff --git a/cbmc/scalar_compress_d1/cbmc-proof.txt → ...fs/cbmc/scalar_compress_d1/cbmc-proof.txt b/cbmc/scalar_compress_d1/cbmc-proof.txt → ...fs/cbmc/scalar_compress_d1/cbmc-proof.txt
diff --git a/..._compress_d1/scalar_compress_d1_harness.c → ..._compress_d1/scalar_compress_d1_harness.c b/..._compress_d1/scalar_compress_d1_harness.c → ..._compress_d1/scalar_compress_d1_harness.c
diff --git a/cbmc/scalar_compress_d10/Makefile → proofs/cbmc/scalar_compress_d10/Makefile b/cbmc/scalar_compress_d10/Makefile → proofs/cbmc/scalar_compress_d10/Makefile
diff --git a/cbmc/scalar_compress_d10/cbmc-proof.txt → ...s/cbmc/scalar_compress_d10/cbmc-proof.txt b/cbmc/scalar_compress_d10/cbmc-proof.txt → ...s/cbmc/scalar_compress_d10/cbmc-proof.txt
diff --git a/...ompress_d10/scalar_compress_d10_harness.c → ...ompress_d10/scalar_compress_d10_harness.c b/...ompress_d10/scalar_compress_d10_harness.c → ...ompress_d10/scalar_compress_d10_harness.c
diff --git a/cbmc/scalar_compress_d11/Makefile → proofs/cbmc/scalar_compress_d11/Makefile b/cbmc/scalar_compress_d11/Makefile → proofs/cbmc/scalar_compress_d11/Makefile
diff --git a/cbmc/scalar_compress_d11/cbmc-proof.txt → ...s/cbmc/scalar_compress_d11/cbmc-proof.txt b/cbmc/scalar_compress_d11/cbmc-proof.txt → ...s/cbmc/scalar_compress_d11/cbmc-proof.txt
diff --git a/...ompress_d11/scalar_compress_d11_harness.c → ...ompress_d11/scalar_compress_d11_harness.c b/...ompress_d11/scalar_compress_d11_harness.c → ...ompress_d11/scalar_compress_d11_harness.c
diff --git a/cbmc/scalar_compress_d4/Makefile → proofs/cbmc/scalar_compress_d4/Makefile b/cbmc/scalar_compress_d4/Makefile → proofs/cbmc/scalar_compress_d4/Makefile
diff --git a/cbmc/scalar_compress_d4/cbmc-proof.txt → ...fs/cbmc/scalar_compress_d4/cbmc-proof.txt b/cbmc/scalar_compress_d4/cbmc-proof.txt → ...fs/cbmc/scalar_compress_d4/cbmc-proof.txt
diff --git a/..._compress_d4/scalar_compress_d4_harness.c → ..._compress_d4/scalar_compress_d4_harness.c b/..._compress_d4/scalar_compress_d4_harness.c → ..._compress_d4/scalar_compress_d4_harness.c
diff --git a/cbmc/scalar_compress_d5/Makefile → proofs/cbmc/scalar_compress_d5/Makefile b/cbmc/scalar_compress_d5/Makefile → proofs/cbmc/scalar_compress_d5/Makefile
diff --git a/cbmc/scalar_compress_d5/cbmc-proof.txt → ...fs/cbmc/scalar_compress_d5/cbmc-proof.txt b/cbmc/scalar_compress_d5/cbmc-proof.txt → ...fs/cbmc/scalar_compress_d5/cbmc-proof.txt
diff --git a/..._compress_d5/scalar_compress_d5_harness.c → ..._compress_d5/scalar_compress_d5_harness.c b/..._compress_d5/scalar_compress_d5_harness.c → ..._compress_d5/scalar_compress_d5_harness.c
diff --git a/cbmc/scalar_decompress_d10/Makefile → proofs/cbmc/scalar_decompress_d10/Makefile b/cbmc/scalar_decompress_d10/Makefile → proofs/cbmc/scalar_decompress_d10/Makefile
diff --git a/cbmc/scalar_decompress_d10/cbmc-proof.txt → ...cbmc/scalar_decompress_d10/cbmc-proof.txt b/cbmc/scalar_decompress_d10/cbmc-proof.txt → ...cbmc/scalar_decompress_d10/cbmc-proof.txt
diff --git a/...press_d10/scalar_decompress_d10_harness.c → ...press_d10/scalar_decompress_d10_harness.c b/...press_d10/scalar_decompress_d10_harness.c → ...press_d10/scalar_decompress_d10_harness.c
diff --git a/cbmc/scalar_decompress_d11/Makefile → proofs/cbmc/scalar_decompress_d11/Makefile b/cbmc/scalar_decompress_d11/Makefile → proofs/cbmc/scalar_decompress_d11/Makefile
diff --git a/cbmc/scalar_decompress_d11/cbmc-proof.txt → ...cbmc/scalar_decompress_d11/cbmc-proof.txt b/cbmc/scalar_decompress_d11/cbmc-proof.txt → ...cbmc/scalar_decompress_d11/cbmc-proof.txt
diff --git a/...press_d11/scalar_decompress_d11_harness.c → ...press_d11/scalar_decompress_d11_harness.c b/...press_d11/scalar_decompress_d11_harness.c → ...press_d11/scalar_decompress_d11_harness.c
diff --git a/cbmc/scalar_decompress_d4/Makefile → proofs/cbmc/scalar_decompress_d4/Makefile b/cbmc/scalar_decompress_d4/Makefile → proofs/cbmc/scalar_decompress_d4/Makefile
diff --git a/cbmc/scalar_decompress_d4/cbmc-proof.txt → .../cbmc/scalar_decompress_d4/cbmc-proof.txt b/cbmc/scalar_decompress_d4/cbmc-proof.txt → .../cbmc/scalar_decompress_d4/cbmc-proof.txt
diff --git a/...ompress_d4/scalar_decompress_d4_harness.c → ...ompress_d4/scalar_decompress_d4_harness.c b/...ompress_d4/scalar_decompress_d4_harness.c → ...ompress_d4/scalar_decompress_d4_harness.c
diff --git a/cbmc/scalar_decompress_d5/Makefile → proofs/cbmc/scalar_decompress_d5/Makefile b/cbmc/scalar_decompress_d5/Makefile → proofs/cbmc/scalar_decompress_d5/Makefile
diff --git a/cbmc/scalar_decompress_d5/cbmc-proof.txt → .../cbmc/scalar_decompress_d5/cbmc-proof.txt b/cbmc/scalar_decompress_d5/cbmc-proof.txt → .../cbmc/scalar_decompress_d5/cbmc-proof.txt
diff --git a/...ompress_d5/scalar_decompress_d5_harness.c → ...ompress_d5/scalar_decompress_d5_harness.c b/...ompress_d5/scalar_decompress_d5_harness.c → ...ompress_d5/scalar_decompress_d5_harness.c
diff --git a/cbmc/scalar_signed_to_unsigned_q/Makefile → ...cbmc/scalar_signed_to_unsigned_q/Makefile b/cbmc/scalar_signed_to_unsigned_q/Makefile → ...cbmc/scalar_signed_to_unsigned_q/Makefile
diff --git a/...calar_signed_to_unsigned_q/cbmc-proof.txt → ...calar_signed_to_unsigned_q/cbmc-proof.txt b/...calar_signed_to_unsigned_q/cbmc-proof.txt → ...calar_signed_to_unsigned_q/cbmc-proof.txt
diff --git a/...d_q/scalar_signed_to_unsigned_q_harness.c → ...d_q/scalar_signed_to_unsigned_q_harness.c b/...d_q/scalar_signed_to_unsigned_q_harness.c → ...d_q/scalar_signed_to_unsigned_q_harness.c
diff --git a/cbmc/sha3_256/Makefile → proofs/cbmc/sha3_256/Makefile b/cbmc/sha3_256/Makefile → proofs/cbmc/sha3_256/Makefile
diff --git a/cbmc/sha3_256/cbmc-proof.txt → proofs/cbmc/sha3_256/cbmc-proof.txt b/cbmc/sha3_256/cbmc-proof.txt → proofs/cbmc/sha3_256/cbmc-proof.txt
diff --git a/cbmc/sha3_256/sha3_256_harness.c → proofs/cbmc/sha3_256/sha3_256_harness.c b/cbmc/sha3_256/sha3_256_harness.c → proofs/cbmc/sha3_256/sha3_256_harness.c
diff --git a/cbmc/sha3_512/Makefile → proofs/cbmc/sha3_512/Makefile b/cbmc/sha3_512/Makefile → proofs/cbmc/sha3_512/Makefile
diff --git a/cbmc/sha3_512/cbmc-proof.txt → proofs/cbmc/sha3_512/cbmc-proof.txt b/cbmc/sha3_512/cbmc-proof.txt → proofs/cbmc/sha3_512/cbmc-proof.txt
diff --git a/cbmc/sha3_512/sha3_512_harness.c → proofs/cbmc/sha3_512/sha3_512_harness.c b/cbmc/sha3_512/sha3_512_harness.c → proofs/cbmc/sha3_512/sha3_512_harness.c
diff --git a/cbmc/shake128_absorb_once/Makefile → proofs/cbmc/shake128_absorb_once/Makefile b/cbmc/shake128_absorb_once/Makefile → proofs/cbmc/shake128_absorb_once/Makefile
diff --git a/cbmc/shake128_absorb_once/cbmc-proof.txt → .../cbmc/shake128_absorb_once/cbmc-proof.txt b/cbmc/shake128_absorb_once/cbmc-proof.txt → .../cbmc/shake128_absorb_once/cbmc-proof.txt
diff --git a/...bsorb_once/shake128_absorb_once_harness.c → ...bsorb_once/shake128_absorb_once_harness.c b/...bsorb_once/shake128_absorb_once_harness.c → ...bsorb_once/shake128_absorb_once_harness.c
diff --git a/cbmc/shake128_squeezeblocks/Makefile → proofs/cbmc/shake128_squeezeblocks/Makefile b/cbmc/shake128_squeezeblocks/Makefile → proofs/cbmc/shake128_squeezeblocks/Makefile
diff --git a/cbmc/shake128_squeezeblocks/cbmc-proof.txt → ...bmc/shake128_squeezeblocks/cbmc-proof.txt b/cbmc/shake128_squeezeblocks/cbmc-proof.txt → ...bmc/shake128_squeezeblocks/cbmc-proof.txt
diff --git a/...zeblocks/shake128_squeezeblocks_harness.c → ...zeblocks/shake128_squeezeblocks_harness.c b/...zeblocks/shake128_squeezeblocks_harness.c → ...zeblocks/shake128_squeezeblocks_harness.c
diff --git a/cbmc/shake128x4_absorb_once/Makefile → proofs/cbmc/shake128x4_absorb_once/Makefile b/cbmc/shake128x4_absorb_once/Makefile → proofs/cbmc/shake128x4_absorb_once/Makefile
diff --git a/cbmc/shake128x4_absorb_once/cbmc-proof.txt → ...bmc/shake128x4_absorb_once/cbmc-proof.txt b/cbmc/shake128x4_absorb_once/cbmc-proof.txt → ...bmc/shake128x4_absorb_once/cbmc-proof.txt
diff --git a/...orb_once/shake128x4_absorb_once_harness.c → ...orb_once/shake128x4_absorb_once_harness.c b/...orb_once/shake128x4_absorb_once_harness.c → ...orb_once/shake128x4_absorb_once_harness.c
diff --git a/cbmc/shake128x4_squeezeblocks/Makefile → ...fs/cbmc/shake128x4_squeezeblocks/Makefile b/cbmc/shake128x4_squeezeblocks/Makefile → ...fs/cbmc/shake128x4_squeezeblocks/Makefile
diff --git a/cbmc/shake128x4_squeezeblocks/cbmc-proof.txt → ...c/shake128x4_squeezeblocks/cbmc-proof.txt b/cbmc/shake128x4_squeezeblocks/cbmc-proof.txt → ...c/shake128x4_squeezeblocks/cbmc-proof.txt
diff --git a/...blocks/shake128x4_squeezeblocks_harness.c → ...blocks/shake128x4_squeezeblocks_harness.c b/...blocks/shake128x4_squeezeblocks_harness.c → ...blocks/shake128x4_squeezeblocks_harness.c
diff --git a/cbmc/shake256/Makefile → proofs/cbmc/shake256/Makefile b/cbmc/shake256/Makefile → proofs/cbmc/shake256/Makefile
diff --git a/cbmc/shake256/cbmc-proof.txt → proofs/cbmc/shake256/cbmc-proof.txt b/cbmc/shake256/cbmc-proof.txt → proofs/cbmc/shake256/cbmc-proof.txt
diff --git a/cbmc/shake256/shake256_harness.c → proofs/cbmc/shake256/shake256_harness.c b/cbmc/shake256/shake256_harness.c → proofs/cbmc/shake256/shake256_harness.c
diff --git a/cbmc/shake256x4/Makefile → proofs/cbmc/shake256x4/Makefile b/cbmc/shake256x4/Makefile → proofs/cbmc/shake256x4/Makefile
diff --git a/cbmc/shake256x4/cbmc-proof.txt → proofs/cbmc/shake256x4/cbmc-proof.txt b/cbmc/shake256x4/cbmc-proof.txt → proofs/cbmc/shake256x4/cbmc-proof.txt
diff --git a/cbmc/shake256x4/shake256x4_harness.c → proofs/cbmc/shake256x4/shake256x4_harness.c b/cbmc/shake256x4/shake256x4_harness.c → proofs/cbmc/shake256x4/shake256x4_harness.c
diff --git 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
@@ -664,7 +664,7 @@ class Tests:
                     "--no-coverage",
                 ]
                 + self.make_j(),
-                cwd="cbmc",
+                cwd="proofs/cbmc",
                 env=os.environ.copy() | envvars,
             )
             p.communicate()