CBMC: Demonstrate use of CBMC in example of poly_compress

C code in MLKEM-C-AArch64 should be free of undefined behaviour.
The C Bounded Model Checker (CBMC) is a tool which can prove absence
of various classes of undefined behaviour.

This commit is a first step towards using CBMC to harden MLKEM-C-AArch64.

- Setup CBMC boilerplate using cbmc-starter-kit: All proof harnesses,
  scripts and Makefiles needed to run CBMC are in the `cbmc/` directory.
  Harnesses are organized by the (main) function to which they apply,
  and stored in separate directories with the name of the function.
- Demonstrate the use of CBMC in the example of the decompression funcion
  `poly_decompress`: Specify (in natural language, in a function contract,
  and in the test harness) that the coefficients in the output polynomial
  of this function are unsigned canonical.
- Guided by CBMC, make smaller changes to `poly_decompress` to avoid
  integer truncation warnings. The previous code did _not_ trigger
  undefined behaviour to my understanding (signed -> unsigned conversions
  are always defined), but it is arguably still better style to make
  truncations explicit.

To run the `poly_decompress` proofs along:

```
cd cbmc/proofs/poly_decompress
make
```

To run all CBMC tests (only `poly_decompress` so far, but more will
hopefully be added) and print a summary,

```
cd cbmc/proofs
KYBER_K={2,3,4} run-cbmc-proofs.py --summarize
```

Signed-off-by: Hanno Becker <[email protected]>

cbmc/.gitignore

@@ -0,0 +1,19 @@
+# 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,6 @@
+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,33 @@
+# -*- 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,7 @@
+# -*- 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,8 @@
+# -*- 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 @@
+
+# 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"
+