Merge pull request #661 from pq-code-package/cbmc_proofs

Move cbmc -> proofs/cbmc

Author: hanno-becker

README.md

@@ -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"
 

cbmc/.gitignore renamed to proofs/cbmc/.gitignore

@@ -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"

cbmc/KeccakF1600_StateExtractBytes/KeccakF1600_StateExtractBytes_harness.c renamed to proofs/cbmc/KeccakF1600_StateExtractBytes/KeccakF1600_StateExtractBytes_harness.c

@@ -664,7 +664,7 @@ class Tests:
                     "--no-coverage",
                 ]
                 + self.make_j(),
-                cwd="cbmc",
+                cwd="proofs/cbmc",
                 env=os.environ.copy() | envvars,
             )
             p.communicate()