sign: Consolidate make_hint and pack_sig_h

Replace mld_poly_make_hint + the per-polynomial mld_pack_sig_h_poly
with a single mld_pack_sig_h that takes (w0, w1) polyvecks directly,
computes hint bits via mld_make_hint, and writes hint indices into
sig in one pass over all K rows. The function returns MLD_ERR_FAIL
if the total number of hints exceeds MLDSA_OMEGA, in which case the
caller must reject the signature.

This removes the duplicated hint counting (previously make_hint
returned the count and pack iterated the hint poly again without
re-validating), drops the temporary scratch hint polynomial from
sign.c, and lets sign.c emit a single call instead of a K-loop with
per-row tally bookkeeping.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Author: mkannwischer

mldsa/mldsa_native.c

@@ -261,7 +261,7 @@
 /* mldsa/src/packing.h */
 #undef MLD_PACKING_H
 #undef mld_pack_sig_c
-#undef mld_pack_sig_h_poly
+#undef mld_pack_sig_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk_rho_key_tr_s2
 #undef mld_pack_sk_s1
@@ -301,7 +301,6 @@
 #undef MLD_POLY_KL_H
 #undef mld_poly_challenge
 #undef mld_poly_decompose
-#undef mld_poly_make_hint
 #undef mld_poly_uniform_eta
 #undef mld_poly_uniform_eta_4x
 #undef mld_poly_uniform_gamma1

mldsa/mldsa_native_asm.S

@@ -266,7 +266,7 @@
 /* mldsa/src/packing.h */
 #undef MLD_PACKING_H
 #undef mld_pack_sig_c
-#undef mld_pack_sig_h_poly
+#undef mld_pack_sig_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk_rho_key_tr_s2
 #undef mld_pack_sk_s1
@@ -306,7 +306,6 @@
 #undef MLD_POLY_KL_H
 #undef mld_poly_challenge
 #undef mld_poly_decompose
-#undef mld_poly_make_hint
 #undef mld_poly_uniform_eta
 #undef mld_poly_uniform_eta_4x
 #undef mld_poly_uniform_gamma1

mldsa/src/packing.c

@@ -8,6 +8,7 @@
 #include "packing.h"
 #include "poly.h"
 #include "polyvec.h"
+#include "rounding.h"
 
 /* Parameter set namespacing
  * This is to facilitate building multiple instances
@@ -90,10 +91,10 @@ void mld_pack_sig_c(uint8_t sig[MLDSA_CRYPTO_BYTES],
 }
 
 MLD_INTERNAL_API
-void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h,
-                         unsigned int k, unsigned int n)
+int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
+                   const mld_polyveck *w1)
 {
-  unsigned int j;
+  unsigned int j, k, n;
 
   /* The hint section of sig[] is MLDSA_POLYVECH_PACKEDBYTES long, where
    * MLDSA_POLYVECH_PACKEDBYTES = MLDSA_OMEGA + MLDSA_K.
@@ -102,32 +103,54 @@ void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h,
    * that are not equal to 0.
    *
    * The final K bytes record a running tally of the number of hints
-   * coming from each of the K polynomials in h. */
+   * coming from each of the K polynomials. */
   uint8_t *sig_h = sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;
 
-  /* For each coefficient in this polynomial, record it as a hint */
-  /* if its value is not zero. */
-  for (j = 0; j < MLDSA_N; j++)
+  mld_memset(sig_h, 0, MLDSA_POLYVECH_PACKEDBYTES);
+  n = 0;
+
+  /* For each coefficient of each polynomial, compute its hint bit and, if
+   * non-zero, record the index in the hint section of sig. If recording the
+   * hint would overflow the OMEGA-sized index array, abort early and return
+   * MLD_ERR_FAIL. The caller is expected to reject the signature in that case.
+   *
+   * Constant time: At this point w0/w1 are public (see comment in sign.c
+   * before the call), so a data-dependent early return is fine. */
+  for (k = 0; k < MLDSA_K; k++)
   __loop__(
-    assigns(j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
-    invariant(j <= MLDSA_N)
-    invariant(n <= MLDSA_OMEGA)
-    decreases(MLDSA_N - j)
+    assigns(k, j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
+    invariant(k <= MLDSA_K && n <= MLDSA_OMEGA)
+    decreases(MLDSA_K - k)
   )
   {
-    /* The reference implementation implicitly relies on the total */
-    /* number of hints being less than OMEGA, assuming h is valid. */
-    /* In mldsa-native, we check this explicitly to ease proof of  */
-    /* type safety.                                                */
-    if (h->coeffs[j] != 0 && n < MLDSA_OMEGA)
+    for (j = 0; j < MLDSA_N; j++)
+    __loop__(
+      assigns(j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
+      invariant(j <= MLDSA_N && n <= MLDSA_OMEGA)
+      decreases(MLDSA_N - j)
+    )
     {
-      sig_h[n] = (uint8_t)j;
-      n++;
+      const unsigned int hint_bit =
+          mld_make_hint(w0->vec[k].coeffs[j], w1->vec[k].coeffs[j]);
+      if (hint_bit)
+      {
+        if (n == MLDSA_OMEGA)
+        {
+          return MLD_ERR_FAIL;
+        }
+        /* Safety: branch above ensures n < MLDSA_OMEGA so n is a valid index
+         * into the OMEGA-sized index array; j < MLDSA_N <= 256 fits in
+         * uint8_t. */
+        sig_h[n] = (uint8_t)j;
+        n++;
+      }
     }
+    /* Record the running tally into the correct slot for this polynomial.
+     * Safety: k < MLDSA_K, so MLDSA_OMEGA + k is a valid index into the
+     * K-byte tally tail; n <= MLDSA_OMEGA fits in uint8_t. */
+    sig_h[MLDSA_OMEGA + k] = (uint8_t)n;
   }
-  /* Record the running tally into the correct slot for this     */
-  /* polynomial in the final K bytes.                            */
-  sig_h[MLDSA_OMEGA + k] = (uint8_t)n;
+  return 0;
 }
 
 MLD_INTERNAL_API

mldsa/src/packing.h

@@ -81,29 +81,35 @@ __contract__(
   assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
 );
 
-#define mld_pack_sig_h_poly MLD_NAMESPACE_KL(pack_sig_h_poly)
+#define mld_pack_sig_h MLD_NAMESPACE_KL(pack_sig_h)
 /*************************************************
- * Name:        mld_pack_sig_h_poly
+ * Name:        mld_pack_sig_h
  *
- * Description: Pack hints for one polynomial into the hint section of sig.
- *              Must be called once per polynomial in order k = 0, ..., K-1.
- *              The hint section of sig must be zeroed before the first call.
+ * Description: Compute hints from (w0, w1) and pack them into the hint
+ *              section of sig.
  *
  * Arguments:   - uint8_t sig[]: byte array containing signature
- *              - const mld_poly *h: pointer to hint polynomial (0/1 coeffs)
- *              - unsigned int k: index of polynomial in vector (0..K-1)
- *              - unsigned int n: total number of hints written so far
+ *              - const mld_polyveck *w0: pointer to low part of input vector
+ *              - const mld_polyveck *w1: pointer to high part of input vector
+ *
+ * Returns:     - 0 on success;
+ *              - MLD_ERR_FAIL if the total number of hints exceeds
+ *                MLDSA_OMEGA. In this case the hint section of sig is
+ *                left in a partially-written state and the caller must
+ *                reject the signature.
  **************************************************/
 MLD_INTERNAL_API
-void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h,
-                         unsigned int k, unsigned int n)
+MLD_MUST_CHECK_RETURN_VALUE
+int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
+                   const mld_polyveck *w1)
 __contract__(
   requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
-  requires(memory_no_alias(h, sizeof(mld_poly)))
-  requires(k < MLDSA_K)
-  requires(n <= MLDSA_OMEGA)
-  requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
+  requires(memory_no_alias(w0, sizeof(mld_polyveck)))
+  requires(memory_no_alias(w1, sizeof(mld_polyveck)))
+  assigns(memory_slice(
+    sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES,
+    MLDSA_POLYVECH_PACKEDBYTES))
+  ensures(return_value == 0 || return_value == MLD_ERR_FAIL)
 );
 
 #define mld_pack_sig_z MLD_NAMESPACE_KL(pack_sig_z)
@@ -112,7 +118,7 @@ __contract__(
  *
  * 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_c and mld_pack_sig_h_poly.
+ *              mld_pack_sig_c and mld_pack_sig_h.
  *
  * Arguments:   - uint8_t sig[]: output byte array
  *              - const mld_poly *zi: pointer to a single polynomial in z

mldsa/src/poly_kl.c

@@ -101,29 +101,6 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0)
   mld_poly_decompose_c(a1, a0);
 }
 
-MLD_INTERNAL_API
-unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0,
-                                const mld_poly *a1)
-{
-  unsigned int i, s = 0;
-
-  for (i = 0; i < MLDSA_N; ++i)
-  __loop__(
-    invariant(i <= MLDSA_N)
-    invariant(s <= i)
-    invariant(array_bound(h->coeffs, 0, i, 0, 2))
-    decreases(MLDSA_N - i)
-  )
-  {
-    const unsigned int hint_bit = mld_make_hint(a0->coeffs[i], a1->coeffs[i]);
-    h->coeffs[i] = (int32_t)hint_bit;
-    s += hint_bit;
-  }
-
-  mld_assert(s <= MLDSA_N);
-  mld_assert_bound(h->coeffs, MLDSA_N, 0, 2);
-  return s;
-}
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)

mldsa/src/poly_kl.h

@@ -44,32 +44,6 @@ __contract__(
 );
 
 
-#define mld_poly_make_hint MLD_NAMESPACE_KL(poly_make_hint)
-/*************************************************
- * Name:        mld_poly_make_hint
- *
- * Description: Compute hint polynomial. The coefficients of which indicate
- *              whether the low bits of the corresponding coefficient of
- *              the input polynomial overflow into the high bits.
- *
- * Arguments:   - mld_poly *h: pointer to output hint polynomial
- *              - const mld_poly *a0: pointer to low part of input polynomial
- *              - const mld_poly *a1: pointer to high part of input polynomial
- *
- * Returns number of 1 bits.
- **************************************************/
-MLD_INTERNAL_API
-MLD_MUST_CHECK_RETURN_VALUE
-unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0,
-                                const mld_poly *a1)
-__contract__(
-  requires(memory_no_alias(h,  sizeof(mld_poly)))
-  requires(memory_no_alias(a0, sizeof(mld_poly)))
-  requires(memory_no_alias(a1, sizeof(mld_poly)))
-  assigns(memory_slice(h, sizeof(mld_poly)))
-  ensures(return_value <= MLDSA_N)
-  ensures(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
-);
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)

mldsa/src/sign.c

@@ -681,7 +681,7 @@ __contract__(
           return_value == MLD_ERR_OUT_OF_MEMORY)
 )
 {
-  unsigned int k, n;
+  unsigned int k;
   uint32_t w0_invalid, h_invalid;
   int ret;
 
@@ -808,31 +808,13 @@ __contract__(
   MLD_CT_TESTING_DECLASSIFY(w0, sizeof(*w0));
   MLD_CT_TESTING_DECLASSIFY(w1, sizeof(*w1));
 
-  /* Pack challenge bytes and initialize hint section */
+  /* Pack challenge bytes and hints. */
   mld_pack_sig_c(sig, challenge_bytes);
-  mld_memset(sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES, 0,
-             MLDSA_POLYVECH_PACKEDBYTES);
 
-  /* Compute hints per-component and pack incrementally */
-  n = 0;
-  for (k = 0; k < MLDSA_K; k++)
-  __loop__(
-    assigns(k, n,
-            memory_slice(z, sizeof(mld_poly)),
-            memory_slice(sig, MLDSA_CRYPTO_BYTES))
-    invariant(k <= MLDSA_K)
-    invariant(n <= MLDSA_OMEGA)
-    decreases(MLDSA_K - k)
-  )
+  ret = mld_pack_sig_h(sig, w0, w1);
+  if (ret != 0)
   {
-    unsigned int hints = mld_poly_make_hint(z, &w0->vec[k], &w1->vec[k]);
-    if (n + hints > MLDSA_OMEGA)
-    {
-      ret = MLD_ERR_FAIL; /* reject */
-      goto cleanup;
-    }
-    mld_pack_sig_h_poly(sig, z, k, n);
-    n += hints;
+    goto cleanup;
   }
 
   /* Constant time: At this point it is clear that the signature is valid - it

proofs/cbmc/attempt_signature_generation/Makefile

@@ -37,9 +37,8 @@ USE_FUNCTION_CONTRACTS+=mld_poly_sub
 USE_FUNCTION_CONTRACTS+=mld_poly_reduce
 USE_FUNCTION_CONTRACTS+=mld_poly_chknorm
 USE_FUNCTION_CONTRACTS+=mld_poly_add
-USE_FUNCTION_CONTRACTS+=mld_poly_make_hint
 USE_FUNCTION_CONTRACTS+=mld_pack_sig_c
-USE_FUNCTION_CONTRACTS+=mld_pack_sig_h_poly
+USE_FUNCTION_CONTRACTS+=mld_pack_sig_h
 USE_FUNCTION_CONTRACTS+=mld_zeroize
 
 APPLY_LOOP_CONTRACTS=on

proofs/cbmc/pack_sig_h_poly/Makefile proofs/cbmc/pack_sig_h/Makefileproofs/cbmc/pack_sig_h_poly/Makefile renamed to proofs/cbmc/pack_sig_h/Makefile

@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = pack_sig_h_poly_harness
+HARNESS_FILE = pack_sig_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_h_poly
+PROOF_UID = pack_sig_h
 
 DEFINES +=
 INCLUDES +=
@@ -19,16 +19,16 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
 
-CHECK_FUNCTION_CONTRACTS=mld_pack_sig_h_poly
-USE_FUNCTION_CONTRACTS=
+CHECK_FUNCTION_CONTRACTS=mld_pack_sig_h
+USE_FUNCTION_CONTRACTS=mld_make_hint
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
 
-FUNCTION_NAME = pack_sig_h_poly
+FUNCTION_NAME = pack_sig_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

…ack_sig_h_poly/pack_sig_h_poly_harness.c …ofs/cbmc/pack_sig_h/pack_sig_h_harness.cproofs/cbmc/pack_sig_h_poly/pack_sig_h_poly_harness.c renamed to proofs/cbmc/pack_sig_h/pack_sig_h_harness.c proofs/cbmc/pack_sig_h_poly/pack_sig_h_poly_harness.c renamed to proofs/cbmc/pack_sig_h/pack_sig_h_harness.c

@@ -6,7 +6,7 @@
 void harness(void)
 {
   uint8_t *sig;
-  mld_poly *h;
-  unsigned int k, n;
-  mld_pack_sig_h_poly(sig, h, k, n);
+  mld_polyveck *w0, *w1;
+  int r;
+  r = mld_pack_sig_h(sig, w0, w1);
 }