[SQUASH ME] Address review feedback

mkannwischer · mkannwischer · commit 5ecdabc13b75 · 2026-01-07T19:35:22.000+08:00
Signed-off-by: Matthias J. Kannwischer &lt;matthias@kannwischer.eu&gt;
diff --git a/mldsa/mldsa_native.S b/mldsa/mldsa_native.S
@@ -223,7 +223,7 @@
 /* mldsa/src/packing.h */
 #undef MLD_PACKING_H
 #undef mld_pack_pk
-#undef mld_pack_sig
+#undef mld_pack_sig_c_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk
 #undef mld_unpack_pk
diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c
@@ -219,7 +219,7 @@
 /* mldsa/src/packing.h */
 #undef MLD_PACKING_H
 #undef mld_pack_pk
-#undef mld_pack_sig
+#undef mld_pack_sig_c_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk
 #undef mld_unpack_pk
diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c
@@ -99,9 +99,9 @@ void mld_unpack_sk(uint8_t rho[MLDSA_SEEDBYTES], uint8_t tr[MLDSA_TRBYTES],
 }
 
 MLD_INTERNAL_API
-void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
-                  const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
-                  const unsigned int number_of_hints)
+void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES],
+                      const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
+                      const unsigned int number_of_hints)
 {
   unsigned int i, j, k;
 
diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h
@@ -69,9 +69,9 @@ __contract__(
 );
 
 
-#define mld_pack_sig MLD_NAMESPACE_KL(pack_sig)
+#define mld_pack_sig_c_h MLD_NAMESPACE_KL(pack_sig_c_h)
 /*************************************************
- * Name:        mld_pack_sig
+ * Name:        mld_pack_sig_c_h
  *
  * Description: Bit-pack c and h component of sig = (c, z, h).
  *              The z component is packed separately using mld_pack_sig_z.
@@ -88,9 +88,9 @@ __contract__(
  * proof of type safety.
  **************************************************/
 MLD_INTERNAL_API
-void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
-                  const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
-                  const unsigned int number_of_hints)
+void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES],
+                      const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,
+                      const unsigned int number_of_hints)
 __contract__(
   requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
   requires(memory_no_alias(c, MLDSA_CTILDEBYTES))
@@ -106,7 +106,8 @@ __contract__(
  * Name:        mld_pack_sig_z
  *
  * Description: Bit-pack single polynomial of z component of sig = (c, z, h).
- *              The c and h components are packed separately using mld_pack_sig.
+ *              The c and h components are packed separately using
+ *              mld_pack_sig_c_h.
  *
  * Arguments:   - uint8_t sig[]: output byte array
  *              - const mld_poly *zi: pointer to a single polynomial in z
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
@@ -457,34 +457,29 @@ __contract__(
 MLD_MUST_CHECK_RETURN_VALUE
 static int mld_compute_pack_z(uint8_t sig[MLDSA_CRYPTO_BYTES],
                               const mld_poly *cp, const mld_polyvecl *s1,
-                              const mld_polyvecl *y)
+                              const mld_polyvecl *y, mld_poly *z)
 __contract__(
   requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
   requires(memory_no_alias(cp, sizeof(mld_poly)))
   requires(memory_no_alias(s1, sizeof(mld_polyvecl)))
   requires(memory_no_alias(y, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(z, sizeof(mld_poly)))
   requires(array_abs_bound(cp->coeffs, 0, MLDSA_N, MLD_NTT_BOUND))
   requires(forall(k0, 0, MLDSA_L,
     array_bound(y->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
   requires(forall(k1, 0, MLDSA_L, array_abs_bound(s1->vec[k1].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
   assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
+  assigns(memory_slice(z, sizeof(mld_poly)))
   ensures(return_value == 0 || return_value == MLD_ERR_FAIL ||
           return_value == MLD_ERR_OUT_OF_MEMORY)
 )
 {
   unsigned int i;
   uint32_t z_invalid;
-  int ret;
-  MLD_ALLOC(z, mld_poly, 1);
-  if (z == NULL)
-  {
-    ret = MLD_ERR_OUT_OF_MEMORY;
-    goto cleanup;
-  }
   for (i = 0; i < MLDSA_L; i++)
   __loop__(
     assigns(i, memory_slice(z, sizeof(mld_poly)), memory_slice(sig, MLDSA_CRYPTO_BYTES))
-    invariant(i <= MLDSA_L)  
+    invariant(i <= MLDSA_L)
   )
   {
     mld_poly_pointwise_montgomery(z, cp, &s1->vec[i]);
@@ -494,38 +489,37 @@ __contract__(
 
     z_invalid = mld_poly_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA);
     /* Constant time: It is fine (and prohibitively expensive to avoid)
-     * leaking the result of the norm check. In case of rejection it
-     * would even be okay to leak which coefficient led to rejection
-     * as the candidate signature will be discarded anyway.
+     * to leak the result of the norm check and which polynomial in z caused a
+     * rejection. It would even be okay to leak which coefficient led to
+     * rejection as the candidate signature will be discarded anyway.
      * See Section 5.5 of @[Round3_Spec]. */
     MLD_CT_TESTING_DECLASSIFY(&z_invalid, sizeof(uint32_t));
     if (z_invalid)
     {
-      ret = MLD_ERR_FAIL; /* reject */
-      goto cleanup;
+      return MLD_ERR_FAIL; /* reject */
     }
-    /* If z is valid, then its coefficients are bounded by  */
-    /* MLDSA_GAMMA1 - MLDSA_BETA. This will be needed below */
-    /* to prove the pre-condition of pack_sig_z()             */
+    /* If z is valid, then its coefficients are bounded by
+     * MLDSA_GAMMA1 - MLDSA_BETA. This will be needed below
+     * to prove the pre-condition of pack_sig_z() */
     mld_assert_abs_bound(z, MLDSA_N, (MLDSA_GAMMA1 - MLDSA_BETA));
+
+    /* After the norm check, the distribution of each coefficient of z is
+     * independent of the secret key and it can, hence, be considered
+     * public. It is, hence, okay to immediately pack it into the user-provided
+     * signature buffer. */
     mld_pack_sig_z(sig, z, i);
   }
-  ret = 0;
-
-cleanup:
-  MLD_FREE(z, mld_poly, 1);
-  return ret;
+  return 0;
 }
 
-/* Reference: The reference implementation does not explicitly   */
-/* check the maximum nonce value, but instead loops indefinitely */
-/* (even when the nonce would overflow). Internally,             */
-/* sampling of y uses (nonceL), (nonceL+1), ... (nonce*L+L-1).   */
-/* Hence, there are no overflows if nonce < (UINT16_MAX - L)/L.  */
-/* Explicitly checking for this explicitly allows us to prove    */
-/* type-safety. Note that FIPS204 explicitly allows an upper-    */
-/* bound this loop of 814 (< (UINT16_MAX - L)/L) - see           */
-/* @[FIPS204, Appendix C].                                        */
+/* Reference: The reference implementation does not explicitly check the
+ * maximum nonce value, but instead loops indefinitely (even when the nonce
+ * would overflow). Internally, sampling of y uses
+ * (nonceL), (nonceL+1), ... (nonce*L+L-1).
+ * Hence, there are no overflows if nonce < (UINT16_MAX - L)/L.
+ * Explicitly checking for this explicitly allows us to prove type-safety.
+ * Note that FIPS204 explicitly allows an upper-bound this loop of
+ * 814 (< (UINT16_MAX - L)/L) - see @[FIPS204, Appendix C]. */
 #define MLD_NONCE_UB ((UINT16_MAX - MLDSA_L) / MLDSA_L)
 
 /*************************************************
@@ -608,9 +602,10 @@ __contract__(
   MLD_ALLOC(w1tmp, w1tmp_u, 1);
   MLD_ALLOC(w0, mld_polyveck, 1);
   MLD_ALLOC(cp, mld_poly, 1);
+  MLD_ALLOC(t, mld_poly, 1);
 
   if (challenge_bytes == NULL || yh == NULL || z == NULL || w1tmp == NULL ||
-      w0 == NULL || cp == NULL)
+      w0 == NULL || cp == NULL || t == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
@@ -646,13 +641,12 @@ __contract__(
   mld_poly_ntt(cp);
 
   /* Compute z, reject if it reveals secret */
-  ret = mld_compute_pack_z(sig, cp, s1, y);
+  ret = mld_compute_pack_z(sig, cp, s1, y, t);
   if (ret)
   {
     goto cleanup;
   }
 
-
   /* Check that subtracting cs2 does not change high bits of w and low bits
    * do not reveal secret information */
   mld_polyveck_pointwise_poly_montgomery(h, cp, s2);
@@ -703,14 +697,15 @@ __contract__(
   }
 
   /* All is well - write signature */
-  mld_pack_sig(sig, challenge_bytes, h, n);
+  mld_pack_sig_c_h(sig, challenge_bytes, h, n);
   /* Constant time: At this point it is clear that the signature is valid - it
    * can, hence, be considered public. */
   MLD_CT_TESTING_DECLASSIFY(sig, MLDSA_CRYPTO_BYTES);
   ret = 0; /* success */
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
+  MLD_FREE(t, mld_poly, 1);
   MLD_FREE(cp, mld_poly, 1);
   MLD_FREE(w0, mld_polyveck, 1);
   MLD_FREE(w1tmp, w1tmp_u, 1);
diff --git a/proofs/cbmc/attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile
@@ -37,7 +37,7 @@ USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 \
                        $(MLD_NAMESPACE)polyveck_chknorm \
                        $(MLD_NAMESPACE)polyveck_add \
                        $(MLD_NAMESPACE)polyveck_make_hint \
-                       $(MLD_NAMESPACE)pack_sig \
+                       $(MLD_NAMESPACE)pack_sig_c_h \
                        mld_compute_pack_z
 USE_FUNCTION_CONTRACTS+=mld_zeroize
 
diff --git a/proofs/cbmc/compute_pack_z/compute_pack_z_harness.c b/proofs/cbmc/compute_pack_z/compute_pack_z_harness.c
@@ -4,15 +4,17 @@
 #include "sign.h"
 
 int mld_compute_pack_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *cp,
-                       const mld_polyvecl *s1, const mld_polyvecl *y);
+                       const mld_polyvecl *s1, const mld_polyvecl *y,
+                       mld_poly *t);
 
 void harness(void)
 {
   uint8_t *sig;
   mld_poly *cp;
   mld_polyvecl *s1;
   mld_polyvecl *y;
+  mld_poly *t;
 
   int r;
-  r = mld_compute_pack_z(sig, cp, s1, y);
+  r = mld_compute_pack_z(sig, cp, s1, y, t);
 }
diff --git a/proofs/cbmc/pack_sig_c_h/Makefile b/proofs/cbmc/pack_sig_c_h/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = pack_sig_harness
+HARNESS_FILE = pack_sig_c_h_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 = pack_sig
+PROOF_UID = pack_sig_c_h
 
 DEFINES +=
 INCLUDES +=
@@ -18,7 +18,7 @@ REMOVE_FUNCTION_BODY +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig_c_h
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -28,7 +28,7 @@ EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 CBMCFLAGS+=--slice-formula
 
-FUNCTION_NAME = pack_sig
+FUNCTION_NAME = pack_sig_c_h
 
 # 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
diff --git a/proofs/cbmc/pack_sig_c_h/pack_sig_c_h_harness.c b/proofs/cbmc/pack_sig_c_h/pack_sig_c_h_harness.c
@@ -9,5 +9,5 @@ void harness(void)
   uint8_t *a, *b;
   mld_polyveck *h;
   unsigned int nh;
-  mld_pack_sig(a, b, h, nh);
+  mld_pack_sig_c_h(a, b, h, nh);
 }

Original file line number	Diff line number	Diff line change
`@@ -99,9 +99,9 @@ void mld_unpack_sk(uint8_t rho[MLDSA_SEEDBYTES], uint8_t tr[MLDSA_TRBYTES],`
`99`	`99`	`}`
`100`	`100`
`101`	`101`	`MLD_INTERNAL_API`
`102`		`-void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],`
`103`		`- const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,`
`104`		`- const unsigned int number_of_hints)`
	`102`	`+void mld_pack_sig_c_h(uint8_t sig[MLDSA_CRYPTO_BYTES],`
	`103`	`+ const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyveck *h,`
	`104`	`+ const unsigned int number_of_hints)`
`105`	`105`	`{`
`106`	`106`	`unsigned int i, j, k;`
`107`	`107`
Original file line number	Diff line number	Diff line change
`@@ -9,5 +9,5 @@ void harness(void)`
`9`	`9`	`uint8_t a, b;`
`10`	`10`	`mld_polyveck *h;`
`11`	`11`	`unsigned int nh;`
`12`		`- mld_pack_sig(a, b, h, nh);`
	`12`	`+ mld_pack_sig_c_h(a, b, h, nh);`
`13`	`13`	`}`