Demonstrate use of CBMC in example of (de)compression routines

.github/workflows/build.yml

@@ -11,6 +11,8 @@ jobs:
     runs-on: macos-latest
     steps:
       - uses: actions/checkout@v4
+      - name: install native dependencies
+        run: brew install litani cbmc cbmc-viewer
       - name: Setup nix
         uses: ./.github/actions/setup-nix
         with:
@@ -20,6 +22,9 @@ jobs:
               Architecture: $(uname -m)
               - $(nix --version)
               - $(astyle --version)
+              - $(cbmc --version)
+              - $(litani --version)
+              - $(cadical --version)
               - $(${{ matrix.cross_prefix }}gcc --version | grep -m1 "")
               - $(bash --version | grep -m1 "")
             EOF
@@ -55,3 +60,10 @@ jobs:
             $(checksum ./test/gen_NISTKAT768  21b4a1e1ea34a13c26a9da5eeb9325afb5ca11596ca6f3704c3f2637e3ea7524)
             $(checksum ./test/gen_NISTKAT1024 6471398b0a728ee1ef39e93bb89b526fbf59587a3662edadbcfc6c88a512cd71)
           EOF
+      - name: Run CBMC proofs
+        shell: nix develop .#ci -c bash -e {0}
+        run: |
+          cd cbmc/proofs;
+          KYBER_K=2 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=3 ./run-cbmc-proofs.py --summarize;
+          KYBER_K=4 ./run-cbmc-proofs.py --summarize;

cbmc/.gitignore

@@ -0,0 +1,21 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# Emitted when running CBMC proofs
+proofs/**/logs
+proofs/**/gotos
+proofs/**/report
+proofs/**/html
+proofs/output
+
+# Emitted by CBMC Viewer
+TAGS-*
+
+# Emitted by litani
+.ninja_deps
+.ninja_log
+.litani_cache_dir
+
+# These files should be overwritten whenever prepare.py runs
+cbmc-batch.yaml
+
+__pycache__/

cbmc/include/README.md

@@ -0,0 +1,8 @@
+# SPDX-License-Identifier: Apache-2.0
+
+CBMC proof include files
+========================
+
+This directory contains include files written for CBMC proof.  It is
+common to write some code to model aspects of the system under test,
+and the header files for this code go here.

cbmc/proofs/Makefile-project-defines

@@ -0,0 +1,35 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+################################################################
+# Use this file to give project-specific definitions of the command
+# line arguments to pass to CBMC tools like goto-cc to build the goto
+# binaries and cbmc to do the property and coverage checking.
+#
+# Use this file to override most default definitions of variables in
+# Makefile.common.
+################################################################
+
+# Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
+# COMPILE_FLAGS =
+
+# Flags to pass to goto-cc for linking (typically those passed to gcc)
+# LINK_FLAGS =
+
+# Flag to pass to goto-cc to make all static symbols globally visible. Leave it
+# unset or set it to --export-file-local-symbols to enable this behavior. Else,
+# selectively enable access to such symbols via each proof's Makefile.
+EXPORT_FILE_LOCAL_SYMBOLS =
+
+# Preprocessor include paths -I...
+# Consider adding
+#     INCLUDES += -I$(CBMC_ROOT)/include
+# You will want to decide what order that comes in relative to the other
+# include directories in your project.
+#
+# INCLUDES =
+
+# Preprocessor definitions -D...
+# DEFINES =

cbmc/proofs/Makefile-project-targets

@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+################################################################
+# Use this file to give project-specific targets, including targets
+# that may depend on targets defined in Makefile.common.
+################################################################

cbmc/proofs/Makefile-project-testing

@@ -0,0 +1,10 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# -*- mode: makefile -*-
+# The first line sets the emacs major mode to Makefile
+
+################################################################
+# Use this file to define project-specific targets and definitions for
+# unit testing or continuous integration that may depend on targets
+# defined in Makefile.common
+################################################################

cbmc/proofs/Makefile-template-defines

@@ -0,0 +1,20 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# Absolute path to the root of the source tree.
+#
+SRCDIR ?= $(abspath $(PROOF_ROOT)/../..)
+
+
+# How to invoke litani.
+# Use "litani" when litani is present in PATH.
+#
+LITANI ?= litani
+
+
+# Name of this proof project, displayed in proof reports. For example,
+# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots,
+# this may be overridden on the command-line to Make, for example
+#
+#         make PROJECT_NAME="FreeRTOS MQTT" report
+#
+PROJECT_NAME = "mlkem-c-aarch64"