Rename coeff_signed_to_unsigned -> scalar_signed_to_unsigned_q_16

Also, uniformize file structure of proof subdirctory for scalar_signed_to_unsigned_q_16 with those of other functions. Signed-off-by: Hanno Becker <[email protected]>
pq-code-package · Jul 2, 2024 · bf75581 · bf75581
1 parent 6446621
commit bf75581
Show file tree

Hide file tree

Showing 8 changed files with 29 additions and 48 deletions.
diff --git a/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk b/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk
diff --git a/.../proofs/coeff_signed_to_unsigned/Makefile → ...s/scalar_signed_to_unsigned_q_16/Makefile b/.../proofs/coeff_signed_to_unsigned/Makefile → ...s/scalar_signed_to_unsigned_q_16/Makefile
@@ -3,11 +3,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = coeff_signed_to_unsigned_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 = coeff_signed_to_unsigned
+PROOF_UID = scalar_signed_to_unsigned_q_16
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=coeff_signed_to_unsigned
+CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)scalar_signed_to_unsigned_q_16
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

diff --git a/...proofs/coeff_signed_to_unsigned/README.md → .../scalar_signed_to_unsigned_q_16/README.md b/...proofs/coeff_signed_to_unsigned/README.md → .../scalar_signed_to_unsigned_q_16/README.md
@@ -1,9 +1,9 @@
 # SPDX-License-Identifier: Apache-2.0
 
-coeff_signed_to_unsigned proof
+scalar_signed_to_unsigned_q_16 proof
 ==============
 
-This directory contains a memory safety proof for coeff_signed_to_unsigned.
+This directory contains a memory safety proof for scalar_signed_to_unsigned_q_16.
 
 To run the proof.
 -------------

diff --git a/...s/coeff_signed_to_unsigned/cbmc-proof.txt → ...ar_signed_to_unsigned_q_16/cbmc-proof.txt b/...s/coeff_signed_to_unsigned/cbmc-proof.txt → ...ar_signed_to_unsigned_q_16/cbmc-proof.txt
diff --git a/cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-viewer.json b/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"
+}
diff --git a/...signed/coeff_signed_to_unsigned_harness.c → .../scalar_signed_to_unsigned_q_16_harness.c b/...signed/coeff_signed_to_unsigned_harness.c → .../scalar_signed_to_unsigned_q_16_harness.c
@@ -6,8 +6,8 @@
  */
 
 /**
- * @file coeff_signed_to_unsigned.c
- * @brief Implements the proof harness for coeff_signed_to_unsigned function.
+ * @file scalar_signed_to_unsigned_q_16.c
+ * @brief Implements the proof harness for scalar_signed_to_unsigned_q_16 function.
  */
 
 /*
@@ -26,5 +26,5 @@ void harness(void)
     int16_t u;
 
     /* Contracts for this function are in poly.h */
-    uint16_t d = coeff_signed_to_unsigned(u);
+    uint16_t d = scalar_signed_to_unsigned_q_16(u);
 }
diff --git a/mlkem/poly.c b/mlkem/poly.c
@@ -88,7 +88,7 @@ uint32_t scalar_decompress_q_32(uint32_t u)
 }
 
 /************************************************************
- * Name: coeff_signed_to_unsigned
+ * Name: scalar_signed_to_unsigned_q_16
  *
  * Description: converts signed polynomial coefficient
  *              from signed (-3328 .. 3328) form to
@@ -105,16 +105,16 @@ uint32_t scalar_decompress_q_32(uint32_t u)
  *
  * Arguments: c: signed coefficient to be converted
  ************************************************************/
-uint16_t coeff_signed_to_unsigned (int16_t c)
+uint16_t scalar_signed_to_unsigned_q_16 (int16_t c)
 {
     int32_t r = (int32_t) c;
 
     // Add Q if r is negative
     int32_t factor = (r < 0); // 1 if r < 0; 0 if r >= 0
     r = r + (factor * KYBER_Q);
 
-    __CPROVER_assert(r >= 0, "coeff_signed_to_unsigned result lower bound");
-    __CPROVER_assert(r < KYBER_Q, "coeff_signed_to_unsigned result upper bound");
+    __CPROVER_assert(r >= 0, "scalar_signed_to_unsigned_q_16 result lower bound");
+    __CPROVER_assert(r < KYBER_Q, "scalar_signed_to_unsigned_q_16 result upper bound");
 
     // and therefore cast to uint16_t is safe.
     return (uint16_t) r;
@@ -145,7 +145,7 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
         {
             // map to positive standard representatives
             // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
-            int32_t u = (int32_t) coeff_signed_to_unsigned(a->coeffs[8 * i + j]);
+            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);
         }
@@ -163,7 +163,7 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
         {
             // map to positive standard representatives
             // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
-            int32_t u = (int32_t) coeff_signed_to_unsigned(a->coeffs[8 * i + j]);
+            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);
         }
@@ -266,8 +266,8 @@ void poly_tobytes(uint8_t r[KYBER_POLYBYTES], const poly *a)
     {
         // map to positive standard representatives
         // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
-        t0 = coeff_signed_to_unsigned(a->coeffs[2 * i]);
-        t1 = coeff_signed_to_unsigned(a->coeffs[2 * i + 1]);
+        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);

diff --git a/mlkem/poly.h b/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,7 +47,7 @@ __CPROVER_requires(0 <= u && u < 32)
 __CPROVER_ensures(__CPROVER_return_value < KYBER_Q);
 /* INDENT-ON */
 
-uint16_t coeff_signed_to_unsigned (int16_t c)
+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