Merge pull request #690 from pq-code-package/cbmc_no_verbose

CBMC: Make `tests cbmc` more convenient to use

Author: mkannwischer

proofs/cbmc/README.md

@@ -25,12 +25,12 @@ MLKEM_K={2,3,4} run-cbmc-proofs.py --summarize
 
 If `GITHUB_STEP_SUMMARY` is set, the proof summary will be appended to it.
 
-# Covered functions
-
-Each proved function has an eponymous sub-directory of its own. The shell command
+Alternatively, you can use the [tests](../../scripts/tests) script, see
 
 ```
-find . -name cbmc-proof.txt
+tests cbmc --help
 ```
 
-yields a list of the subdirectories, and thus function names, that have a proof.
+# Covered functions
+
+Each proved function has an eponymous sub-directory of its own. Use [list_proofs.sh](list_proofs.sh) to see the list of functions covered.

proofs/cbmc/gen_matrix_entry/gen_matrix_entry_harness.c

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+# Copyright (c) 2024 The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0
+#
+# This tiny script just lists the proof directories in proof/cbmc,
+# which are those containing a *harness.c file.
+
+ROOT=$(git rev-parse --show-toplevel)
+cd $ROOT
+ls -1 proofs/cbmc/**/*harness.c | cut -d '/' -f 3