Merge pull request #435 from pq-code-package/polyvec-compress-split

Hoist `poly_{,de}compress_du` out of `polyvec_{,de}compress`

cbmc/proofs/indcpa_dec/Makefile

@@ -26,8 +26,8 @@ USED_FUNCTIONS += poly_invntt_tomont
 USED_FUNCTIONS += poly_sub
 USED_FUNCTIONS += poly_reduce
 USED_FUNCTIONS += poly_tomsg
-USED_FUNCTIONS += polyvec_decompress
-USED_FUNCTIONS += poly_decompress
+USED_FUNCTIONS += polyvec_decompress_du
+USED_FUNCTIONS += poly_decompress_dv
 USED_FUNCTIONS += polyvec_frombytes
 USED_FUNCTIONS += polyvec_reduce
 USE_FUNCTION_CONTRACTS=$(addprefix $(MLKEM_NAMESPACE),$(USED_FUNCTIONS))

cbmc/proofs/indcpa_enc/Makefile

@@ -41,8 +41,8 @@ USED_FUNCTIONS += polyvec_add
 USED_FUNCTIONS += poly_add
 USED_FUNCTIONS += polyvec_reduce
 USED_FUNCTIONS += poly_reduce
-USED_FUNCTIONS += polyvec_compress
-USED_FUNCTIONS += poly_compress
+USED_FUNCTIONS += polyvec_compress_du
+USED_FUNCTIONS += poly_compress_dv
 USED_FUNCTIONS += polyvec_frombytes
 
 USE_FUNCTION_CONTRACTS=matvec_mul $(addprefix $(MLKEM_NAMESPACE),$(USED_FUNCTIONS))

cbmc/proofs/poly_compress_du/Makefile

@@ -0,0 +1,61 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_compress_du_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_du
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du
+# For K = 2 or 3, the code calls scalar_compress_d10, so
+ifeq ($(MLKEM_K),4)
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d11
+else
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_compress_d10
+endif
+
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_compress_du
+
+# 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
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 10
+
+# 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/poly_compress_harness.c → cbmc/proofs/poly_compress_du/poly_compress_du_harness.c

@@ -6,8 +6,8 @@
  */
 
 /**
- * @file poly_compress_harness.c
- * @brief Implements the proof harness for poly_compress function.
+ * @file poly_compress_du_harness.c
+ * @brief Implements the proof harness for poly_compress_du function.
  */
 #include "poly.h"
 
@@ -25,5 +25,5 @@ void harness(void) {
   poly *r;
   uint8_t *a;
 
-  poly_compress(a, r);
+  poly_compress_du(a, r);
 }

cbmc/proofs/poly_compress/Makefile → cbmc/proofs/poly_compress_dv/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = poly_compress_harness
+HARNESS_FILE = poly_compress_dv_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
+PROOF_UID = poly_compress_dv
 
 DEFINES +=
 INCLUDES +=
@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_dv
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -28,7 +28,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_compress
+FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_compress_dv
 
 # 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

cbmc/proofs/poly_decompress/poly_decompress_harness.c → cbmc/proofs/poly_compress_dv/poly_compress_dv_harness.c

@@ -6,16 +6,16 @@
  */
 
 /**
- * @file poly_decompress_harness.c
- * @brief Implements the proof harness for poly_decompress function.
+ * @file poly_compress_dv_harness.c
+ * @brief Implements the proof harness for poly_compress_dv function.
  */
+#include "poly.h"
 
 /*
  * 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
@@ -25,5 +25,5 @@ void harness(void) {
   poly *r;
   uint8_t *a;
 
-  poly_decompress(r, a);
+  poly_compress_dv(a, r);
 }

cbmc/proofs/poly_decompress_du/Makefile

@@ -0,0 +1,62 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = poly_decompress_du_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_decompress_du
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du
+
+# For K = 2 or 3, the code calls scalar_decompress_d10, so
+ifeq ($(MLKEM_K),4)
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d11
+else
+USE_FUNCTION_CONTRACTS = $(MLKEM_NAMESPACE)scalar_decompress_d10
+endif
+
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_decompress_du
+
+# 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
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 12
+
+# 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_decompress_du/poly_decompress_du_harness.c

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0 AND Apache-2.0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file poly_decompress_du_harness.c
+ * @brief Implements the proof harness for poly_decompress_du 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) {
+  poly *r;
+  uint8_t *a;
+
+  poly_decompress_du(r, a);
+}

cbmc/proofs/poly_decompress/Makefile → cbmc/proofs/poly_decompress_dv/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = poly_decompress_harness
+HARNESS_FILE = poly_decompress_dv_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_decompress
+PROOF_UID = poly_decompress_dv
 
 DEFINES +=
 INCLUDES +=
@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_dv
 
 # For K = 2 or 3, the code calls scalar_decompress_d4, so
 ifeq ($(MLKEM_K),4)
@@ -35,7 +35,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_decompress
+FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_decompress_dv
 
 # 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

cbmc/proofs/poly_decompress_dv/poly_decompress_dv_harness.c

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: MIT-0 AND Apache-2.0
+
+/*
+ * Insert copyright notice
+ */
+
+/**
+ * @file poly_decompress_dv_harness.c
+ * @brief Implements the proof harness for poly_decompress_dv 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) {
+  poly *r;
+  uint8_t *a;
+
+  poly_decompress_dv(r, a);
+}

cbmc/proofs/poly_getnoise_eta1122_4x/Makefile

@@ -43,7 +43,7 @@ FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_getnoise_eta1122_4x
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 9
 
 # 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

cbmc/proofs/polyvec_compress/Makefile → cbmc/proofs/polyvec_compress_du/Makefile

@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = polyvec_compress_harness
+HARNESS_FILE = polyvec_compress_du_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 = polyvec_compress
+PROOF_UID = polyvec_compress_du
 
 DEFINES +=
 INCLUDES +=
@@ -18,16 +18,16 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/polyvec.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_compress
-USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_compress_d10 $(MLKEM_NAMESPACE)scalar_compress_d11
+CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)polyvec_compress_du
+USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_compress
+FUNCTION_NAME = $(MLKEM_NAMESPACE)polyvec_compress_du
 
 # 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

cbmc/proofs/polyvec_compress_du/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/polyvec_compress/polyvec_compress_harness.c → cbmc/proofs/polyvec_compress_du/polyvec_compress_du_harness.c

@@ -6,8 +6,8 @@
  */
 
 /**
- * @file polyvec_compress_harness.c
- * @brief Implements the proof harness for polyvec_compress function.
+ * @file polyvec_compress_du_harness.c
+ * @brief Implements the proof harness for polyvec_compress_du function.
  */
 #include "poly.h"
 #include "polyvec.h"
@@ -26,5 +26,5 @@ void harness(void) {
   polyvec *r;
   uint8_t *a;
 
-  polyvec_compress(a, r);
+  polyvec_compress_du(a, r);
 }