Merge pull request #360 from pq-code-package/scalar_compress_cleanup

Various cleanups around scalar [de]compression, poly, polyvec

cbmc/proofs/poly_decompress/Makefile

@@ -21,11 +21,11 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress
 
-# For K = 2 or 3, the code calls scalar_decompress_q_16, so
+# For K = 2 or 3, the code calls scalar_decompress_d4, so
 ifeq ($(MLKEM_K),4)
-USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_q_32
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d5
 else
-USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_q_16
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d4
 endif
 
 APPLY_LOOP_CONTRACTS=on

cbmc/proofs/poly_reduce/Makefile

@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_reduce
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_signed_to_unsigned_q_16 $(MLKEM_NAMESPACE)barrett_reduce
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_signed_to_unsigned_q $(MLKEM_NAMESPACE)barrett_reduce
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

cbmc/proofs/scalar_compress_q_16/Makefile → cbmc/proofs/scalar_compress_d1/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = scalar_compress_q_16_harness
+HARNESS_FILE = scalar_compress_d1_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
+PROOF_UID = scalar_compress_d1
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_q_16
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d1
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_compress_q_32/cbmc-viewer.json → cbmc/proofs/scalar_compress_d1/cbmc-viewer.json

@@ -2,6 +2,6 @@
   [
 
   ],
-  "proof-name": "scalar_compress_q_32",
+  "proof-name": "scalar_compress_d1",
   "proof-root": "cbmc/proofs"
 }

cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c → cbmc/proofs/scalar_compress_d1/scalar_compress_d1_harness.c

@@ -6,8 +6,8 @@
  */
 
 /**
- * @file scalar_compress_q_32_harness.c
- * @brief Implements the proof harness for scalar_compress_q_32 function.
+ * @file scalar_compress_d1_harness.c
+ * @brief Implements the proof harness for scalar_compress_d1 function.
  */
 
 /*
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  int32_t u;
+  uint16_t u;
 
   /* Contracts for this function are in poly.h */
-  uint32_t d = scalar_compress_q_32(u);
+  uint32_t d = scalar_compress_d1(u);
 }

cbmc/proofs/scalar_compress_q_32/Makefile → cbmc/proofs/scalar_compress_d10/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = scalar_compress_q_32_harness
+HARNESS_FILE = scalar_compress_d10_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
+PROOF_UID = scalar_compress_d10
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_q_32
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d10
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_compress_d10/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-viewer.json → cbmc/proofs/scalar_compress_d10/cbmc-viewer.json

@@ -2,6 +2,6 @@
   [
 
   ],
-  "proof-name": "scalar_compress_q_16",
+  "proof-name": "scalar_compress_d10",
   "proof-root": "cbmc/proofs"
 }

cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c → cbmc/proofs/scalar_compress_d10/scalar_compress_d10_harness.c

@@ -6,8 +6,8 @@
  */
 
 /**
- * @file scalar_compress_q_16_harness.c
- * @brief Implements the proof harness for scalar_compress_q_16 function.
+ * @file scalar_compress_d10_harness.c
+ * @brief Implements the proof harness for scalar_compress_d10 function.
  */
 
 /*
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  int32_t u;
+  uint16_t u;
 
   /* Contracts for this function are in poly.h */
-  uint32_t d = scalar_compress_q_16(u);
+  uint32_t d = scalar_compress_d10(u);
 }

cbmc/proofs/scalar_decompress_q_16/Makefile → cbmc/proofs/scalar_compress_d11/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = scalar_decompress_q_16_harness
+HARNESS_FILE = scalar_compress_d11_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
+PROOF_UID = scalar_compress_d11
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_q_16
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d11
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_compress_d11/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_decompress_q_16/cbmc-viewer.json → cbmc/proofs/scalar_compress_d11/cbmc-viewer.json

@@ -2,6 +2,6 @@
   [
 
   ],
-  "proof-name": "scalar_decompress_q_16",
+  "proof-name": "scalar_compress_d11",
   "proof-root": "cbmc/proofs"
 }

cbmc/proofs/scalar_decompress_q_32/scalar_decompress_q_32_harness.c → cbmc/proofs/scalar_compress_d11/scalar_compress_d11_harness.c

@@ -6,8 +6,8 @@
  */
 
 /**
- * @file scalar_decompress_q_32_harness.c
- * @brief Implements the proof harness for scalar_decompress_q_32 function.
+ * @file scalar_compress_d11_harness.c
+ * @brief Implements the proof harness for scalar_compress_d11 function.
  */
 
 /*
@@ -22,11 +22,8 @@
  *
  */
 void harness(void) {
-  // Check that decompression followed by compression is the identity
-  uint32_t c0, c1, d;
+  uint16_t u;
 
-  d = scalar_decompress_q_32(c0);
-  c1 = scalar_compress_q_32(d);
-  __CPROVER_assert(c0 == c1,
-                   "scalar_compress_q_32 o scalar_decompress_q_32 != id");
+  /* Contracts for this function are in poly.h */
+  uint32_t d = scalar_compress_d11(u);
 }

cbmc/proofs/scalar_decompress_q_32/Makefile → cbmc/proofs/scalar_compress_d4/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = scalar_decompress_q_32_harness
+HARNESS_FILE = scalar_compress_d4_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_32
+PROOF_UID = scalar_compress_d4
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_decompress_q_32
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d4
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/scalar_compress_d4/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_decompress_q_32/cbmc-viewer.json → cbmc/proofs/scalar_compress_d4/cbmc-viewer.json

@@ -2,6 +2,6 @@
   [
 
   ],
-  "proof-name": "scalar_decompress_q_32",
+  "proof-name": "scalar_compress_d4",
   "proof-root": "cbmc/proofs"
 }

cbmc/proofs/scalar_compress_d4/scalar_compress_d4_harness.c

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file scalar_compress_d4_harness.c
+ * @brief Implements the proof harness for scalar_compress_d4 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) {
+  uint16_t u;
+
+  /* Contracts for this function are in poly.h */
+  uint32_t d = scalar_compress_d4(u);
+}

cbmc/proofs/scalar_compress_d5/Makefile

@@ -0,0 +1,52 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = scalar_compress_d5_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_d5
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d5
+USE_FUNCTION_CONTRACTS=
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# SMT backend for proving with contracts and quantifiers
+# To be re-enabled when CBMC Issue #8303 is fixed.
+# CBMCFLAGS=--smt2
+
+# Uncomment this to see what commands litani is running...
+#VERBOSE=on
+
+# 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_d5/cbmc-viewer.json

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

cbmc/proofs/scalar_compress_d5/scalar_compress_d5_harness.c

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file scalar_compress_d5_harness.c
+ * @brief Implements the proof harness for scalar_compress_d5 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) {
+  uint16_t u;
+
+  /* Contracts for this function are in poly.h */
+  uint32_t d = scalar_compress_d5(u);
+}