sign: Consolidate make_hint and pack_sig_h_poly

mldsa/mldsa_native.c

@@ -256,9 +256,9 @@
 #undef mld_memset
 /* mldsa/src/packing.h */
 #undef MLD_PACKING_H
+#undef mld_make_pack_sig_h_poly
 #undef mld_pack_pk
 #undef mld_pack_sig_c
-#undef mld_pack_sig_h_poly
 #undef mld_pack_sig_z
 #undef mld_pack_sk
 #undef mld_unpack_pk
@@ -297,7 +297,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

@@ -261,9 +261,9 @@
 #undef mld_memset
 /* mldsa/src/packing.h */
 #undef MLD_PACKING_H
+#undef mld_make_pack_sig_h_poly
 #undef mld_pack_pk
 #undef mld_pack_sig_c
-#undef mld_pack_sig_h_poly
 #undef mld_pack_sig_z
 #undef mld_pack_sk
 #undef mld_unpack_pk
@@ -302,7 +302,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
@@ -107,8 +108,9 @@ 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_make_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES],
+                             const mld_poly *a0, const mld_poly *a1,
+                             unsigned int k, unsigned int n)
 {
   unsigned int j;
 
@@ -119,11 +121,16 @@ 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 each coefficient in this 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 a0/a1 are public (see comment in sign.c
+   * before the call), so a data-dependent early return is fine. */
   for (j = 0; j < MLDSA_N; j++)
   __loop__(
     assigns(j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
@@ -132,19 +139,21 @@ void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h,
     decreases(MLDSA_N - j)
   )
   {
-    /* 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)
+    const unsigned int hint_bit = mld_make_hint(a0->coeffs[j], a1->coeffs[j]);
+    if (hint_bit)
     {
+      if (n == MLDSA_OMEGA)
+      {
+        return MLD_ERR_FAIL;
+      }
       sig_h[n] = (uint8_t)j;
       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 (int)n;
 }
 
 MLD_INTERNAL_API

mldsa/src/packing.h

@@ -87,29 +87,41 @@ __contract__(
   assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
 );
 
-#define mld_pack_sig_h_poly MLD_NAMESPACE_KL(pack_sig_h_poly)
+#define mld_make_pack_sig_h_poly MLD_NAMESPACE_KL(make_pack_sig_h_poly)
 /*************************************************
- * Name:        mld_pack_sig_h_poly
+ * Name:        mld_make_pack_sig_h_poly
  *
- * Description: Pack hints for one polynomial into the hint section of sig.
+ * Description: Compute hints for one polynomial of (w0, w1) and pack them
+ *              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.
  *
  * Arguments:   - uint8_t sig[]: byte array containing signature
- *              - const mld_poly *h: pointer to hint polynomial (0/1 coeffs)
+ *              - const mld_poly *a0: pointer to low part of input polynomial
+ *              - const mld_poly *a1: pointer to high part of input polynomial
  *              - unsigned int k: index of polynomial in vector (0..K-1)
  *              - unsigned int n: total number of hints written so far
+ *
+ * Returns:     - the updated running tally of hints (non-negative, at most
+ *                MLDSA_OMEGA) on success;
+ *              - MLD_ERR_FAIL if writing all hints for this polynomial
+ *                would exceed MLDSA_OMEGA. In this case 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_make_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES],
+                             const mld_poly *a0, const mld_poly *a1,
+                             unsigned int k, unsigned int n)
 __contract__(
   requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
-  requires(memory_no_alias(h, sizeof(mld_poly)))
+  requires(memory_no_alias(a0, sizeof(mld_poly)))
+  requires(memory_no_alias(a1, 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))
+  ensures(return_value == MLD_ERR_FAIL ||
+          (return_value >= 0 && return_value <= MLDSA_OMEGA))
 );
 
 #define mld_pack_sig_z MLD_NAMESPACE_KL(pack_sig_z)
@@ -118,7 +130,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_make_pack_sig_h_poly.
  *
  * Arguments:   - uint8_t sig[]: output byte array
  *              - const mld_poly *zi: pointer to a single polynomial in z

mldsa/src/poly_kl.c

@@ -100,30 +100,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;
-}
-
 MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *b, const mld_poly *a,
                                              const mld_poly *h)
 __contract__(

mldsa/src/poly_kl.h

@@ -43,33 +43,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))
-);
-
 #define mld_poly_use_hint MLD_NAMESPACE_KL(poly_use_hint)
 /*************************************************
  * Name:        mld_poly_use_hint

mldsa/src/sign.c

@@ -728,22 +728,18 @@ __contract__(
   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))
+    assigns(k, n, ret, memory_slice(sig, MLDSA_CRYPTO_BYTES))
     invariant(k <= MLDSA_K)
     invariant(n <= MLDSA_OMEGA)
     decreases(MLDSA_K - k)
   )
   {
-    unsigned int hints = mld_poly_make_hint(z, &w0->vec[k], &w1->vec[k]);
-    if (n + hints > MLDSA_OMEGA)
+    ret = mld_make_pack_sig_h_poly(sig, &w0->vec[k], &w1->vec[k], k, n);
+    if (ret == MLD_ERR_FAIL)
     {
-      ret = MLD_ERR_FAIL; /* reject */
       goto cleanup;
     }
-    mld_pack_sig_h_poly(sig, z, k, n);
-    n += hints;
+    n = (unsigned int)ret;
   }
 
   /* 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_make_pack_sig_h_poly
 USE_FUNCTION_CONTRACTS+=mld_zeroize
 
 APPLY_LOOP_CONTRACTS=on

proofs/cbmc/pack_sig_h_poly/Makefile → proofs/cbmc/make_pack_sig_h_poly/Makefile

@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = pack_sig_h_poly_harness
+HARNESS_FILE = make_pack_sig_h_poly_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 = make_pack_sig_h_poly
 
 DEFINES +=
 INCLUDES +=
@@ -19,8 +19,8 @@ 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_make_pack_sig_h_poly
+USE_FUNCTION_CONTRACTS=mld_make_hint
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
@@ -29,7 +29,7 @@ EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
 CBMCFLAGS+=--slice-formula
 
-FUNCTION_NAME = pack_sig_h_poly
+FUNCTION_NAME = make_pack_sig_h_poly
 
 # 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

proofs/cbmc/pack_sig_h_poly/pack_sig_h_poly_harness.c → proofs/cbmc/make_pack_sig_h_poly/make_pack_sig_h_poly_harness.c

@@ -6,7 +6,8 @@
 void harness(void)
 {
   uint8_t *sig;
-  mld_poly *h;
+  mld_poly *a0, *a1;
   unsigned int k, n;
-  mld_pack_sig_h_poly(sig, h, k, n);
+  int r;
+  r = mld_make_pack_sig_h_poly(sig, a0, a1, k, n);
 }