CBMC: Add specs and proofs for further (de)compression routines

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

cbmc/proofs/poly_compress/Makefile

@@ -0,0 +1,47 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_compress_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.
+PROOF_UID = poly_compress
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.0:9
+# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.1:33
+
+FUNCTION_NAME = $(KYBER_NAMESPACE)poly_compress
+
+USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_compress_q_16 $(KYBER_NAMESPACE)scalar_compress_q_32
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

cbmc/proofs/poly_compress/README.md

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: Apache-2.0
+
+poly_compress proof
+==============
+
+This directory contains a memory safety proof for poly_compress.
+
+To run the proof.
+-------------
+* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer.
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open `report/html/index.html` in a web browser.

cbmc/proofs/poly_compress/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/poly_compress/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "poly_compress",
+  "proof-root": "cbmc/proofs"
+}

cbmc/proofs/poly_compress/poly_compress_harness.c

@@ -0,0 +1,34 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0 AND Apache-2.0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file poly_compress_harness.c
+ * @brief Implements the proof harness for poly_compress function.
+ */
+#include "poly.h"
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+    poly r;
+    uint8_t a[KYBER_POLYCOMPRESSEDBYTES];
+
+    // *INDENT-OFF *
+    __CPROVER_assume(__CPROVER_forall {
+        unsigned i; (i < KYBER_N) ==> ( -KYBER_Q <= r.coeffs[i] && r.coeffs[i] < KYBER_Q )
+    });
+    // *INDENT-ON*
+    poly_compress(a, &r);
+}

cbmc/proofs/poly_decompress/Makefile

@@ -28,6 +28,8 @@ endif
 
 FUNCTION_NAME = $(KYBER_NAMESPACE)poly_decompress
 
+USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_decompress_q_16
+
 # TODO: I would like to comment this out to have CBMC validate the
 # function contract as annotated in the source, rather than being forced
 # to replicate it in the harness. But somehow this doesn't work...?

cbmc/proofs/scalar_compress_q_16/Makefile

@@ -0,0 +1,41 @@
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = scalar_compress_q_16_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.
+PROOF_UID = scalar_compress_q_16
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+# Disable unsigned overflow check for Barret reduction
+CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK =
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

cbmc/proofs/scalar_compress_q_16/README.md

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: Apache-2.0
+
+scalar_compress_q_16 proof
+==============
+
+This directory contains a memory safety proof for scalar_compress_q_16.
+
+To run the proof.
+-------------
+* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer.
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open `report/html/index.html` in a web browser.

cbmc/proofs/scalar_compress_q_16/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/scalar_compress_q_16/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "scalar_compress_q_16",
+  "proof-root": "cbmc/proofs"
+}

cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c

@@ -0,0 +1,32 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file scalar_compress_q_16_harness.c
+ * @brief Implements the proof harness for scalar_compress_q_16 function.
+ */
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+#include <poly.h>
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+    int32_t u;
+
+    __CPROVER_assume(0 <= u && u < KYBER_Q);
+    uint32_t d = scalar_compress_q_16(u);
+    __CPROVER_assert(d < 16, "compression bound failed");
+    __CPROVER_assert(d == (((uint32_t) u * 16 + KYBER_Q / 2) / KYBER_Q) % 16,
+                     "compression expression failed");
+}

cbmc/proofs/scalar_compress_q_32/Makefile

@@ -0,0 +1,41 @@
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = scalar_compress_q_32_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.
+PROOF_UID = scalar_compress_q_32
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+# Disable unsigned overflow check for Barret reduction
+CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK =
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

cbmc/proofs/scalar_compress_q_32/README.md

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: Apache-2.0
+
+scalar_compress_q_32 proof
+==============
+
+This directory contains a memory safety proof for scalar_compress_q_32.
+
+To run the proof.
+-------------
+* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer.
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open `report/html/index.html` in a web browser.

cbmc/proofs/scalar_compress_q_32/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/scalar_compress_q_32/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "scalar_compress_q_32",
+  "proof-root": "cbmc/proofs"
+}

cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c

@@ -0,0 +1,32 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file scalar_compress_q_32_harness.c
+ * @brief Implements the proof harness for scalar_compress_q_32 function.
+ */
+
+/*
+ * Insert project header files that
+ *   - include the declaration of the function
+ *   - include the types needed to declare function arguments
+ */
+#include <poly.h>
+
+/**
+ * @brief Starting point for formal analysis
+ *
+ */
+void harness(void) {
+    int32_t u;
+
+    __CPROVER_assume(0 <= u && u < KYBER_Q);
+    uint32_t d = scalar_compress_q_32(u);
+    __CPROVER_assert(d < 32, "compression bound failed");
+    __CPROVER_assert(d == (((uint32_t) u * 32 + KYBER_Q / 2) / KYBER_Q) % 32,
+                     "compression expression failed");
+}

cbmc/proofs/scalar_decompress_q_16/Makefile

@@ -0,0 +1,38 @@
+# SPDX-License-Identifier: Apache-2.0
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = scalar_decompress_q_16_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.
+PROOF_UID = scalar_decompress_q_16
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mlkem/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

cbmc/proofs/scalar_decompress_q_16/README.md

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: Apache-2.0
+
+scalar_decompress_q_16 proof
+==============
+
+This directory contains a memory safety proof for scalar_decompress_q_16.
+
+To run the proof.
+-------------
+* Follow these [tool installation instructions](https://github.com/awslabs/aws-templates-for-cbmc-proofs/wiki/Installation) to install cbmc and cbmc-viewer.
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path.
+* Run `make`.
+* Open `report/html/index.html` in a web browser.

cbmc/proofs/scalar_decompress_q_16/cbmc-proof.txt

@@ -0,0 +1,3 @@
+# SPDX-License-Identifier: Apache-2.0
+
+# This file marks this directory as containing a CBMC proof.

cbmc/proofs/scalar_decompress_q_16/cbmc-viewer.json

@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "scalar_decompress_q_16",
+  "proof-root": "cbmc/proofs"
+}