WIP: sign stack usage: compute z incrementally

mkannwischer · mkannwischer · commit 89b07cf27c51 · 2025-12-30T19:38:48.000+08:00
Hoisted out from #791 Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c
@@ -100,15 +100,15 @@ 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_polyvecl *z,
+                  const uint8_t c[MLDSA_CTILDEBYTES],
                   const mld_polyveck *h, const unsigned int number_of_hints)
 {
   unsigned int i, j, k;
 
   mld_memcpy(sig, c, MLDSA_CTILDEBYTES);
   sig += MLDSA_CTILDEBYTES;
 
-  mld_polyvecl_pack_z(sig, z);
+  /* skip z component - packed via mld_pack_sig_z */
   sig += MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;
 
   /* Encode hints h */
@@ -168,6 +168,15 @@ void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
   }
 }
 
+MLD_INTERNAL_API
+void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
+                    unsigned i)
+{
+  sig += MLDSA_CTILDEBYTES;
+  sig += i * MLDSA_POLYZ_PACKEDBYTES;
+  mld_polyz_pack(sig, zi);
+}
+
 /*************************************************
  * Name:        mld_unpack_hints
  *
diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h
@@ -73,12 +73,12 @@ __contract__(
 /*************************************************
  * Name:        mld_pack_sig
  *
- * Description: Bit-pack signature sig = (c, z, h).
+ * Description: Bit-pack c and h component of sig = (c, z, h).
+ *              The z component is packed separately using mld_pack_sig_z.
  *
  * Arguments:   - uint8_t sig[]: output byte array
  *              - const uint8_t *c:  pointer to challenge hash length
  *                                   MLDSA_SEEDBYTES
- *              - const mld_polyvecl *z: pointer to vector z
  *              - const mld_polyveck *h: pointer to hint vector h
  *              - const unsigned int number_of_hints: total
  *                                   hints in *h
@@ -89,21 +89,41 @@ __contract__(
  **************************************************/
 MLD_INTERNAL_API
 void mld_pack_sig(uint8_t sig[MLDSA_CRYPTO_BYTES],
-                  const uint8_t c[MLDSA_CTILDEBYTES], const mld_polyvecl *z,
+                  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))
-  requires(memory_no_alias(z, sizeof(mld_polyvecl)))
   requires(memory_no_alias(h, sizeof(mld_polyveck)))
-  requires(forall(k0, 0, MLDSA_L,
-    array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
   requires(forall(k1, 0, MLDSA_K,
     array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
   requires(number_of_hints <= MLDSA_OMEGA)
   assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
 );
 
+#define mld_pack_sig_z MLD_NAMESPACE_KL(pack_sig_z)
+/*************************************************
+ * 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.
+ *
+ * Arguments:   - uint8_t sig[]: output byte array
+ *              - const mld_poly *zi: pointer to a single polynomial in z
+ *              - const unsigned int i: index of zi in vector z
+ *
+ **************************************************/
+MLD_INTERNAL_API
+void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
+                    unsigned i)
+__contract__(
+  requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
+  requires(memory_no_alias(zi, sizeof(mld_poly)))
+  requires(i < MLDSA_L)
+  requires(array_bound(zi->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+  assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES))
+);
+
 #define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk)
 /*************************************************
  * Name:        mld_unpack_pk
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
@@ -486,7 +486,7 @@ __contract__(
           return_value == MLD_ERR_OUT_OF_MEMORY)
 )
 {
-  unsigned int n;
+  unsigned int n, i;
   uint32_t z_invalid, w0_invalid, h_invalid;
   int ret;
   /* TODO: Remove the following workaround for
@@ -495,34 +495,45 @@ __contract__(
   {
     mld_polyvecl y;
     mld_polyveck h;
-  }
-  yh_u;
+  } yh_u;
   mld_polyvecl *y;
   mld_polyveck *h;
 
+  /* TODO: Remove the following workaround for
+   * https://github.com/diffblue/cbmc/issues/8813 */
+  typedef MLK_UNION_OR_STRUCT
+  {
+    mld_polyveck w1;
+    mld_polyvecl tmp;
+  } w1tmp_u;
+  mld_polyveck *w1;
+  mld_polyvecl *tmp;
+
   MLD_ALLOC(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES);
   MLD_ALLOC(yh, yh_u, 1);
-  MLD_ALLOC(z, mld_polyvecl, 1);
-  MLD_ALLOC(w1, mld_polyveck, 1);
+  MLD_ALLOC(z, mld_poly, 1);
+  MLD_ALLOC(w1tmp, w1tmp_u, 1);
   MLD_ALLOC(w0, mld_polyveck, 1);
   MLD_ALLOC(cp, mld_poly, 1);
 
-  if (challenge_bytes == NULL || yh == NULL || z == NULL || w1 == NULL ||
+  if (challenge_bytes == NULL || yh == NULL || z == NULL || w1tmp == NULL ||
       w0 == NULL || cp == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
   y = &yh->y;
   h = &yh->h;
+  w1 = &w1tmp->w1;
+  tmp = &w1tmp->tmp;
 
   /* Sample intermediate vector y */
   mld_polyvecl_uniform_gamma1(y, rhoprime, nonce);
 
   /* Matrix-vector multiplication */
-  *z = *y;
-  mld_polyvecl_ntt(z);
-  mld_polyvec_matrix_pointwise_montgomery(w0, mat, z);
+  *tmp = *y;
+  mld_polyvecl_ntt(tmp);
+  mld_polyvec_matrix_pointwise_montgomery(w0, mat, tmp);
   mld_polyveck_reduce(w0);
   mld_polyveck_invntt_tomont(w0);
 
@@ -541,31 +552,36 @@ __contract__(
   mld_poly_challenge(cp, challenge_bytes);
   mld_poly_ntt(cp);
 
+  ret = 0;
   /* Compute z, reject if it reveals secret */
-  mld_polyvecl_pointwise_poly_montgomery(z, cp, s1);
-  mld_polyvecl_invntt_tomont(z);
-  mld_polyvecl_add(z, y);
-  mld_polyvecl_reduce(z);
-
-  z_invalid = mld_polyvecl_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.
-   * 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;
+  for (i = 0; i < MLDSA_L; i++)
+    __loop__(
+      invariant(i <= MLDSA_L))
+    {
+    mld_poly_pointwise_montgomery(z, cp, &s1->vec[i]);
+    mld_poly_invntt_tomont(z);
+    mld_poly_add(z, &y->vec[i]);
+    mld_poly_reduce(z);
+
+    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.
+     * 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;
+    }
+    /* 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));
+    mld_pack_sig_z(sig, z, i);
   }
 
-  /* 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()             */
-  mld_assert_abs_bound_2d(z->vec, MLDSA_L, MLDSA_N,
-                          (MLDSA_GAMMA1 - MLDSA_BETA));
-
   /* 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);
@@ -619,17 +635,16 @@ __contract__(
   /* Constant time: At this point it is clear that the signature is valid - it
    * can, hence, be considered public. */
   MLD_CT_TESTING_DECLASSIFY(h, sizeof(*h));
-  MLD_CT_TESTING_DECLASSIFY(z, sizeof(*z));
-  mld_pack_sig(sig, challenge_bytes, z, h, n);
+  mld_pack_sig(sig, challenge_bytes, h, n);
 
   ret = 0; /* success */
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
   MLD_FREE(cp, mld_poly, 1);
   MLD_FREE(w0, mld_polyveck, 1);
-  MLD_FREE(w1, mld_polyveck, 1);
-  MLD_FREE(z, mld_polyvecl, 1);
+  MLD_FREE(w1tmp, w1tmp_u, 1);
+  MLD_FREE(z, mld_poly, 1);
   MLD_FREE(yh, yh_u, 1);
   MLD_FREE(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES);
 
diff --git a/proofs/cbmc/attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile
@@ -31,17 +31,18 @@ USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 \
                        mld_H \
                        $(MLD_NAMESPACE)poly_challenge \
                        $(MLD_NAMESPACE)poly_ntt \
-                       $(MLD_NAMESPACE)polyvecl_pointwise_poly_montgomery \
-                       $(MLD_NAMESPACE)polyvecl_invntt_tomont \
-                       $(MLD_NAMESPACE)polyvecl_add \
-                       $(MLD_NAMESPACE)polyvecl_reduce \
+                       $(MLD_NAMESPACE)poly_pointwise_montgomery \
+                       $(MLD_NAMESPACE)poly_invntt_tomont \
+                       $(MLD_NAMESPACE)poly_add \
+                       $(MLD_NAMESPACE)poly_reduce \
                        $(MLD_NAMESPACE)polyvecl_chknorm \
                        $(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery \
                        $(MLD_NAMESPACE)polyveck_sub \
                        $(MLD_NAMESPACE)polyveck_reduce \
                        $(MLD_NAMESPACE)polyveck_chknorm \
                        $(MLD_NAMESPACE)polyveck_add \
                        $(MLD_NAMESPACE)polyveck_make_hint \
+                       $(MLD_NAMESPACE)pack_sig_z \
                        $(MLD_NAMESPACE)pack_sig
 USE_FUNCTION_CONTRACTS+=mld_zeroize
 
diff --git a/proofs/cbmc/pack_sig/Makefile b/proofs/cbmc/pack_sig/Makefile
@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig
-USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pack_z
+USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
diff --git a/proofs/cbmc/pack_sig/pack_sig_harness.c b/proofs/cbmc/pack_sig/pack_sig_harness.c
@@ -8,7 +8,6 @@ void harness(void)
 {
   uint8_t *a, *b;
   mld_polyveck *h;
-  mld_polyvecl *z;
   unsigned int nh;
-  mld_pack_sig(a, b, z, h, nh);
+  mld_pack_sig(a, b, h, nh);
 }
diff --git a/proofs/cbmc/pack_sig_z/Makefile b/proofs/cbmc/pack_sig_z/Makefile
@@ -0,0 +1,55 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = pack_sig_z_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_z
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
+
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)pack_sig_z
+USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_pack
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+CBMCFLAGS+=--slice-formula
+
+FUNCTION_NAME = pack_sig_z
+
+# 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
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 9
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/pack_sig_z/pack_sig_z_harness.c b/proofs/cbmc/pack_sig_z/pack_sig_z_harness.c
@@ -0,0 +1,13 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "packing.h"
+
+
+void harness(void)
+{
+  uint8_t *a;
+  mld_poly *zi;
+  unsigned i;
+  mld_pack_sig_z(a, zi, i);
+}

Original file line number	Diff line number	Diff line change
`@@ -8,7 +8,6 @@ void harness(void)`
`8`	`8`	`{`
`9`	`9`	`uint8_t a, b;`
`10`	`10`	`mld_polyveck *h;`
`11`		`- mld_polyvecl *z;`
`12`	`11`	`unsigned int nh;`
`13`		`- mld_pack_sig(a, b, z, h, nh);`
	`12`	`+ mld_pack_sig(a, b, h, nh);`
`14`	`13`	`}`