diff --git a/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk b/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk
deleted file mode 100644
index 61543e86d..000000000
--- a/cbmc/proofs/coeff_signed_to_unsigned/desktop.mk
+++ /dev/null
@@ -1,27 +0,0 @@
-# SPDX-License-Identifier: Apache-2.0
-
-FILE = ../../../mlkem/poly
-HARNESS_FILE = coeff_signed_to_unsigned_harness
-TARGET ?= coeff_signed_to_unsigned
-
-CHECKS=--bounds-check --pointer-check \
-       --memory-cleanup-check --div-by-zero-check --signed-overflow-check \
-       --unsigned-overflow-check --pointer-overflow-check --conversion-check \
-       --undefined-shift-check --enum-range-check --pointer-primitive-check
-
-all: clean $(TARGET)
-
-coeff_signed_to_unsigned: $(FILE)_contracts.goto results_smt
-
-
-results_smt: $(FILE)_contracts.goto
-	cbmc --verbosity 6 --object-bits 8 $(CHECKS) --smt2 $<
-
-$(FILE)_contracts.goto: $(FILE).goto
-	goto-instrument --dfcc harness --apply-loop-contracts --enforce-contract $(TARGET) $< $@
-
-$(FILE).goto: $(FILE).c $(HARNESS_FILE).c
-	goto-cc --function harness -DCBMC -I../../../fips202 -I../../../mlkem -o $@ $^
-
-clean:
-	rm -f *.goto
diff --git a/cbmc/proofs/coeff_signed_to_unsigned/Makefile b/cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile
similarity index 90%
rename from cbmc/proofs/coeff_signed_to_unsigned/Makefile
rename to cbmc/proofs/scalar_signed_to_unsigned_q_16/Makefile
index 4f7f4e53e..89ed71bdd 100644
--- a/cbmc/proofs/coeff_signed_to_unsigned/Makefile
+++ b/cbmc/proofs/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/cbmc/proofs/coeff_signed_to_unsigned/README.md b/cbmc/proofs/scalar_signed_to_unsigned_q_16/README.md
similarity index 77%
rename from cbmc/proofs/coeff_signed_to_unsigned/README.md
rename to cbmc/proofs/scalar_signed_to_unsigned_q_16/README.md
index 3ee617186..e12a8d51f 100644
--- a/cbmc/proofs/coeff_signed_to_unsigned/README.md
+++ b/cbmc/proofs/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/cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt b/cbmc/proofs/scalar_signed_to_unsigned_q_16/cbmc-proof.txt
similarity index 100%
rename from cbmc/proofs/coeff_signed_to_unsigned/cbmc-proof.txt
rename to cbmc/proofs/scalar_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
new file mode 100644
index 000000000..f56a80b36
--- /dev/null
+++ 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/cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c b/cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c
similarity index 72%
rename from cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c
rename to cbmc/proofs/scalar_signed_to_unsigned_q_16/scalar_signed_to_unsigned_q_16_harness.c
index 9989182e8..1f95bad2d 100644
--- a/cbmc/proofs/coeff_signed_to_unsigned/coeff_signed_to_unsigned_harness.c
+++ b/cbmc/proofs/scalar_signed_to_unsigned_q_16/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
index 596a0ab73..288a20f4e 100644
--- 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,7 +105,7 @@ 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;
 
@@ -113,8 +113,8 @@ uint16_t coeff_signed_to_unsigned (int16_t c)
     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
index 871576a88..c7737e320 100644
--- 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