Port check-constracts script from mlkem-native and adjust proof names

proofs/cbmc/mld_h/Makefile → proofs/cbmc/H/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_h_harness
+HARNESS_FILE = H_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.
@@ -18,7 +18,6 @@ UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
-USE_FUNCTION_CONTRACTS+=mld_zeroize
 
 CHECK_FUNCTION_CONTRACTS=mld_H
 USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_squeeze $(FIPS202_NAMESPACE)shake256_finalize

proofs/cbmc/mld_attempt_signature_generation/Makefile → proofs/cbmc/attempt_signature_generation/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_attempt_signature_generation_harness
+HARNESS_FILE = attempt_signature_generation_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_ct_abs_i32/Makefile → proofs/cbmc/ct_abs_i32/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_ct_abs_i32_harness
+HARNESS_FILE = ct_abs_i32_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_ct_cmask_neg_i32/Makefile → proofs/cbmc/ct_cmask_neg_i32/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_ct_cmask_neg_i32_harness
+HARNESS_FILE = ct_cmask_neg_i32_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_ct_get_optblocker_i64/Makefile → proofs/cbmc/ct_get_optblocker_i64/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_ct_get_optblocker_i64_harness
+HARNESS_FILE = ct_get_optblocker_i64_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_ct_get_optblocker_u32/Makefile → proofs/cbmc/ct_get_optblocker_u32/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_ct_get_optblocker_u32_harness
+HARNESS_FILE = ct_get_optblocker_u32_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_ct_sel_int32/Makefile → proofs/cbmc/ct_sel_int32/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_ct_sel_int32_harness
+HARNESS_FILE = ct_sel_int32_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_sample_s1_s2/Makefile → proofs/cbmc/sample_s1_s2/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_sample_s1_s2_harness
+HARNESS_FILE = sample_s1_s2_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_value_barrier_i64/Makefile → proofs/cbmc/value_barrier_i64/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_value_barrier_i64_harness
+HARNESS_FILE = value_barrier_i64_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

proofs/cbmc/mld_value_barrier_u32/Makefile → proofs/cbmc/value_barrier_u32/Makefile

@@ -4,7 +4,7 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = mld_value_barrier_u32_harness
+HARNESS_FILE = value_barrier_u32_harness
 
 # This should be a unique identifier for this proof, and will appear on the
 # Litani dashboard. It can be human-readable and contain spaces if you wish.

scripts/check-contracts

@@ -0,0 +1,91 @@
+#!/usr/bin/env python3
+# Copyright (c) The mlkem-native project authors
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#
+# Looks for CBMC contracts without proof
+#
+
+import re
+import sys
+import subprocess
+import pathlib
+
+def get_c_source_files():
+    return get_files("mldsa/**/*.c")
+
+def get_header_files():
+    return get_files("mldsa/**/*.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("mld_"))
+
+def is_exception(funcname):
+    # The functions passing this filter are known not to have a proof
+
+    if funcname.endswith("_native") or funcname.endswith("_asm"):
+        # 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

@@ -163,6 +163,19 @@ check-spdx()
       success=false
     fi
   done
+  # For source files in dev/* and mldsa/*, we enforce `Apache-2.0 OR ISC OR MIT`
+  for file in $(git ls-files -- "*.[chsSi]" | grep "^dev/\|^mldsa/"); do
+    # TODO: Temporarily exclude AArch64 (i)NTT pending license resolution (see issue #381)
+    if [[ $file == "mldsa/native/aarch64/src/ntt.S" ]] ||
+      [[ $file == "mldsa/native/aarch64/src/intt.S" ]]; then
+      continue
+    fi
+    # Ignore symlinks
+    if [[ ! -L $file && $(grep "SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT" $file | wc -l) == 0 ]]; then
+      gh_error "$file" "${line:-1}" "Missing license header error" "$file is not licensed under 'Apache-2.0 OR ISC OR MIT'"
+      success=false
+    fi
+  done
 
   if $success; then
     info "Check SPDX + Copyright"
@@ -196,3 +209,23 @@ gh_group_end
 if ! $SUCCESS; then
   exit 1
 fi
+
+check-contracts()
+{
+  if python3 $ROOT/scripts/check-contracts >/dev/null; then
+    info "Check contracts"
+    gh_summary_success "Check contracts"
+  else
+    error "Check contracts"
+    gh_summary_failure "Check contracts"
+    SUCCESS=false
+  fi
+}
+
+gh_group_start "Check contracts"
+check-contracts
+gh_group_end
+
+if ! $SUCCESS; then
+  exit 1
+fi