Add coeff_signed_to_unsigned() functions and its proof

cbmc/proofs/poly_compress/Makefile

@@ -17,20 +17,23 @@ UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
+PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.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
 
+# 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).

cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile

@@ -0,0 +1,51 @@
+# SPDX-License-Identifier: Apache-2.0
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = scalar_signed_to_unsigned_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_signed_to_unsigned_q_16
+
+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=$(KYBER_NAMESPACE)scalar_signed_to_unsigned_q_16
+USE_FUNCTION_CONTRACTS=
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+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_signed_to_unsigned_q_16/README.md

@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: Apache-2.0
+
+scalar_signed_to_unsigned_q_16 proof
+==============
+
+This directory contains a memory safety proof for scalar_signed_to_unsigned_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_signed_to_unsigned_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_signed_to_unsigned_q_16/cbmc-viewer.json

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

cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c

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

mlkem/poly.c

@@ -87,6 +87,36 @@ uint32_t scalar_decompress_q_32(uint32_t u)
     return ((u * KYBER_Q) + 16) / 32;
 }
 
+/************************************************************
+ * Name: scalar_signed_to_unsigned_q_16
+ *
+ * Description: converts signed polynomial coefficient
+ *              from signed (-3328 .. 3328) form to
+ *              unsigned form (0 .. 3328).
+ *
+ * Note: Cryptographic constant time implementation
+ *
+ * Examples:       0 -> 0
+ *                 1 -> 1
+ *              3328 -> 3328
+ *                -1 -> 3328
+ *                -2 -> 3327
+ *             -3328 -> 1
+ *
+ * Arguments: c: signed coefficient to be converted
+ ************************************************************/
+uint16_t scalar_signed_to_unsigned_q_16 (int16_t c)
+{
+    // Add Q if c is negative, but in constant time
+    cmov_int16(&c, c + KYBER_Q, c < 0);
+
+    __CPROVER_assert(c >= 0, "scalar_signed_to_unsigned_q_16 result lower bound");
+    __CPROVER_assert(c < KYBER_Q, "scalar_signed_to_unsigned_q_16 result upper bound");
+
+    // and therefore cast to uint16_t is safe.
+    return (uint16_t) c;
+}
+
 /*************************************************
 * Name:        poly_compress
 *
@@ -99,21 +129,20 @@ uint32_t scalar_decompress_q_32(uint32_t u)
 void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
 {
     unsigned int i, j;
-    int32_t u;
     uint8_t t[8];
 
     #if (KYBER_POLYCOMPRESSEDBYTES == 128)
     for (i = 0; i < KYBER_N / 8; i++)
-        __CPROVER_assigns(i, j, u, t, r)
+        __CPROVER_assigns(i, j, t, r)
         /* Stronger loop invariant here TBD */
     {
         for (j = 0; j < 8; j++)
-            __CPROVER_assigns(j, u, t)
+            __CPROVER_assigns(j, t)
             /* Stronger loop invariant here TBD */
         {
             // map to positive standard representatives
-            u  = a->coeffs[8 * i + j];
-            u += (u >> 15) & KYBER_Q;
+            // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
+            int32_t u = (int32_t) scalar_signed_to_unsigned_q_16(a->coeffs[8 * i + j]);
             // REF-CHANGE: Hoist scalar compression into separate function
             t[j] = scalar_compress_q_16(u);
         }
@@ -130,8 +159,8 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
         for (j = 0; j < 8; j++)
         {
             // map to positive standard representatives
-            u  = a->coeffs[8 * i + j];
-            u += (u >> 15) & KYBER_Q;
+            // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
+            int32_t u = (int32_t) scalar_signed_to_unsigned_q_16(a->coeffs[8 * i + j]);
             // REF-CHANGE: Hoist scalar compression into separate function
             t[j] = scalar_compress_q_32(u);
         }
@@ -233,10 +262,9 @@ void poly_tobytes(uint8_t r[KYBER_POLYBYTES], const poly *a)
     for (i = 0; i < KYBER_N / 2; i++)
     {
         // map to positive standard representatives
-        t0  = a->coeffs[2 * i];
-        t0 += ((int16_t)t0 >> 15) & KYBER_Q;
-        t1 = a->coeffs[2 * i + 1];
-        t1 += ((int16_t)t1 >> 15) & KYBER_Q;
+        // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
+        t0 = scalar_signed_to_unsigned_q_16(a->coeffs[2 * i]);
+        t1 = scalar_signed_to_unsigned_q_16(a->coeffs[2 * i + 1]);
         r[3 * i + 0] = (t0 >> 0);
         r[3 * i + 1] = (t0 >> 8) | (t1 << 4);
         r[3 * i + 2] = (t1 >> 4);

mlkem/poly.h

@@ -15,10 +15,11 @@ typedef struct
     int16_t coeffs[KYBER_N];
 } poly;
 
-#define scalar_compress_q_16   KYBER_NAMESPACE(scalar_compress_q_16)
-#define scalar_decompress_q_16 KYBER_NAMESPACE(scalar_decompress_q_16)
-#define scalar_compress_q_32   KYBER_NAMESPACE(scalar_compress_q_32)
-#define scalar_decompress_q_32 KYBER_NAMESPACE(scalar_decompress_q_32)
+#define scalar_compress_q_16           KYBER_NAMESPACE(scalar_compress_q_16)
+#define scalar_decompress_q_16         KYBER_NAMESPACE(scalar_decompress_q_16)
+#define scalar_compress_q_32           KYBER_NAMESPACE(scalar_compress_q_32)
+#define scalar_decompress_q_32         KYBER_NAMESPACE(scalar_decompress_q_32)
+#define scalar_signed_to_unsigned_q_16 KYBER_NAMESPACE(scalar_signed_to_unsigned_q_16)
 
 uint32_t scalar_compress_q_16   (int32_t u)
 /* INDENT-OFF */
@@ -46,6 +47,15 @@ __CPROVER_requires(0 <= u && u < 32)
 __CPROVER_ensures(__CPROVER_return_value < KYBER_Q);
 /* INDENT-ON */
 
+uint16_t scalar_signed_to_unsigned_q_16 (int16_t c)
+/* *INDENT-OFF* */
+__CPROVER_requires(c > -KYBER_Q) // c >= -3328
+__CPROVER_requires(c < KYBER_Q)  // c <= 3328
+__CPROVER_ensures(__CPROVER_return_value >= 0)
+__CPROVER_ensures(__CPROVER_return_value < KYBER_Q)
+__CPROVER_ensures(__CPROVER_return_value == (int32_t) c + (((int32_t) c < 0) * KYBER_Q));
+/* *INDENT-ON* */
+
 #define poly_compress KYBER_NAMESPACE(poly_compress)
 void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a);
 

mlkem/verify.c

@@ -64,6 +64,13 @@ void cmov(uint8_t *r, const uint8_t *x, size_t len, uint8_t b)
 **************************************************/
 void cmov_int16(int16_t *r, int16_t v, uint16_t b)
 {
+
+// CBMC issues false alarms here for the implicit conversions between
+// uint16_t and int, so disable "conversion-check" here for now.
+// Revisit this when proof of this unit with contracts is attempted.
+#pragma CPROVER check push
+#pragma CPROVER check disable "conversion"
     b = -b;
     *r ^= b & ((*r) ^ v);
+#pragma CPROVER check pop
 }