CBMC: Add script to check that contracts have proofs

This commit adds a script `scripts/check-contracts` which looks for
functions with `__contract__` annotations, and checks that a proof
for them has been given -- with a few stated exceptions.

The script is added to CI.

The approach is not perfect since we do not consider which compile-time
options may influence the behaviour of a function -- but it's a start.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

scripts/check-contracts

@@ -0,0 +1,90 @@
+#!/usr/bin/env python3
+# Copyright (c) 2024-2025 The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0
+
+#
+# Looks for CBMC contracts without proof
+#
+
+import re
+import sys
+import subprocess
+import pathlib
+
+def get_c_source_files():
+    return get_files("mlkem/**/*.c")
+
+def get_header_files():
+    return get_files("mlkem/**/*.h")
+
+def get_files(pattern):
+    return list(map(str, pathlib.Path().glob(pattern)))
+
+def gen_proofs():
+     cmd_str = ["./proofs/cbmc/list_proofs.sh"]
+     p = subprocess.run(cmd_str, capture_output=True, universal_newlines=False)
+     proofs = filter(lambda s: s.strip() != "", p.stdout.decode().split("\n"))
+     return proofs
+
+def gen_contracts():
+    files = get_c_source_files() + get_header_files()
+
+    for filename in files:
+        with open(filename, "r") as f:
+            content = f.read()
+
+        contract_pattern = r'(\w+)\s*\([^)]*\)\s*\n?\s*__contract__'
+        matches = re.finditer(contract_pattern, content)
+        for m in matches:
+            line = content.count('\n', 0, m.start())
+            yield (filename, line, m.group(1).removeprefix("mlk_"))
+
+def is_exception(funcname):
+    # The functions passing this filter are known not to have a proof
+
+    if funcname.endswith("_native"):
+        # CBMC proofs are axiomatized against contracts of the backends
+        return True
+
+    if funcname == "ct_get_optblocker_u64":
+        # As documented in the code, this contract is treated as an axiom
+        return True
+
+    if funcname in ["memcmp", "randombytes"]:
+        # External functions
+        return True
+
+    if funcname in ["zeroize"]:
+        # Implemented using inline ASM or external functions
+        return True
+
+    return False
+
+def check_contracts():
+    contracts = set(gen_contracts())
+    proofs = set(gen_proofs())
+
+    bad = []
+
+    # Print contracts without proofs
+    for (filename, line, funcname) in contracts:
+        if funcname in proofs:
+            continue
+
+        if is_exception(funcname):
+            print(f"{filename}:{line}:{funcname} has contract but no proof, "
+                  "but is listed as exception")
+            continue
+
+        print(f"{filename}:{line}:{funcname}: has contract but no proof. FAIL",
+              file=sys.stderr)
+        bad.append(funcname)
+
+    return len(bad) == 0
+
+def _main():
+    if check_contracts() != True:
+        sys.exit(1)
+
+if __name__ == "__main__":
+    _main()

scripts/lint

@@ -135,3 +135,21 @@ echo "::endgroup::"
 if ! $SUCCESS; then
   exit 1
 fi
+
+check-contracts()
+{
+  if python3 $ROOT/scripts/check-contracts >/dev/null; then
+    echo ":white_check_mark: Check contracts" >>"$GITHUB_STEP_SUMMARY"
+  else
+    echo ":x: Check contracts" >>"$GITHUB_STEP_SUMMARY"
+    SUCCESS=false
+  fi
+}
+
+echo "::group::Check contracts"
+check-contracts
+echo "::endgroup::"
+
+if ! $SUCCESS; then
+  exit 1
+fi