Lowram: Refactor verify into per-row loop, drop polyveck w1/t1/h

Restructure mld_sign_verify_internal so that w1, t1 and h live as
single mld_poly scratch buffers instead of full mld_polyveck vectors.
Each row of A * z - c * t1 * 2^d, the use_hint correction and the
polyw1 packing are now done one polynomial at a time.

Convert mld_unpack_pk_t1 and mld_sig_unpack_hints to per-row APIs
(mld_unpack_pk_t1 takes the row index, mld_sig_unpack_hints decodes
and validates one row at a time, with the trailing-zero check folded
into the i == K-1 iteration).

Drop the now-unused mld_polyveck_{sub,shiftl,pointwise_poly_montgomery,
use_hint} helpers and their CBMC harnesses, and narrow the guards on
mld_polyveck_ntt and mld_polyveck_pack_w1 accordingly.

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

Author: mkannwischer

integration/opentitan/reduce_alloc.patch

@@ -1,7 +1,6 @@
 # Copyright (c) The mldsa-native project authors
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 diff --git a/sw/device/lib/crypto/include/mldsa.h b/sw/device/lib/crypto/include/mldsa.h
-index be11f20..9112042 100644
 --- a/sw/device/lib/crypto/include/mldsa.h
 +++ b/sw/device/lib/crypto/include/mldsa.h
 @@ -41,17 +41,17 @@ enum {
@@ -13,21 +12,21 @@ index be11f20..9112042 100644
 -  kOtcryptoMldsa44WorkBufferVerifyWords = 22464 / sizeof(uint32_t),
 +  kOtcryptoMldsa44WorkBufferKeypairWords = 13632 / sizeof(uint32_t),
 +  kOtcryptoMldsa44WorkBufferSignWords = 13120 / sizeof(uint32_t),
-+  kOtcryptoMldsa44WorkBufferVerifyWords = 13184 / sizeof(uint32_t),
++  kOtcryptoMldsa44WorkBufferVerifyWords = 9120 / sizeof(uint32_t),
 
 -  kOtcryptoMldsa65WorkBufferKeypairWords = 46304 / sizeof(uint32_t),
 -  kOtcryptoMldsa65WorkBufferSignWords = 44768 / sizeof(uint32_t),
 -  kOtcryptoMldsa65WorkBufferVerifyWords = 30720 / sizeof(uint32_t),
 +  kOtcryptoMldsa65WorkBufferKeypairWords = 19776 / sizeof(uint32_t),
 +  kOtcryptoMldsa65WorkBufferSignWords = 17248 / sizeof(uint32_t),
-+  kOtcryptoMldsa65WorkBufferVerifyWords = 18368 / sizeof(uint32_t),
++  kOtcryptoMldsa65WorkBufferVerifyWords = 10208 / sizeof(uint32_t),
 
 -  kOtcryptoMldsa87WorkBufferKeypairWords = 62688 / sizeof(uint32_t),
 -  kOtcryptoMldsa87WorkBufferSignWords = 59104 / sizeof(uint32_t),
 -  kOtcryptoMldsa87WorkBufferVerifyWords = 41216 / sizeof(uint32_t),
 +  kOtcryptoMldsa87WorkBufferKeypairWords = 25920 / sizeof(uint32_t),
 +  kOtcryptoMldsa87WorkBufferSignWords = 21344 / sizeof(uint32_t),
-+  kOtcryptoMldsa87WorkBufferVerifyWords = 24768 / sizeof(uint32_t),
++  kOtcryptoMldsa87WorkBufferVerifyWords = 12512 / sizeof(uint32_t),
  };
 
  /**

mldsa/mldsa_native.c

@@ -323,14 +323,10 @@
 #undef mld_polyveck_pack_eta
 #undef mld_polyveck_pack_t0
 #undef mld_polyveck_pack_w1
-#undef mld_polyveck_pointwise_poly_montgomery
 #undef mld_polyveck_power2round
 #undef mld_polyveck_reduce
-#undef mld_polyveck_shiftl
-#undef mld_polyveck_sub
 #undef mld_polyveck_unpack_eta
 #undef mld_polyveck_unpack_t0
-#undef mld_polyveck_use_hint
 #undef mld_polyvecl
 #undef mld_polyvecl_chknorm
 #undef mld_polyvecl_ntt

mldsa/mldsa_native.h

@@ -942,33 +942,33 @@ int MLD_API_NAMESPACE(pk_from_sk)(
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48480
 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 37056
 #define MLD_TOTAL_ALLOC_44_SIGN 44704
-#define MLD_TOTAL_ALLOC_44_VERIFY 25472
+#define MLD_TOTAL_ALLOC_44_VERIFY 24448
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 49440
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 74624
 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 60608
 #define MLD_TOTAL_ALLOC_65_SIGN 69312
-#define MLD_TOTAL_ALLOC_65_VERIFY 42944
+#define MLD_TOTAL_ALLOC_65_VERIFY 39872
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 82208
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 115488
 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 97472
 #define MLD_TOTAL_ALLOC_87_SIGN 108224
-#define MLD_TOTAL_ALLOC_87_VERIFY 73920
+#define MLD_TOTAL_ALLOC_87_VERIFY 68800
 #else /* MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM */
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 13632
-#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 16960
+#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 16896
 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 21728
 #define MLD_TOTAL_ALLOC_44_SIGN 13120
-#define MLD_TOTAL_ALLOC_44_VERIFY 13184
+#define MLD_TOTAL_ALLOC_44_VERIFY 9120
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 19776
-#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 23680
+#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 22560
 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 30944
 #define MLD_TOTAL_ALLOC_65_SIGN 17248
-#define MLD_TOTAL_ALLOC_65_VERIFY 18368
+#define MLD_TOTAL_ALLOC_65_VERIFY 10208
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 25920
-#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 32032
+#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 28608
 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 41184
 #define MLD_TOTAL_ALLOC_87_SIGN 21344
-#define MLD_TOTAL_ALLOC_87_VERIFY 24768
+#define MLD_TOTAL_ALLOC_87_VERIFY 12512
 #endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */
 /* check-magic: on */
 

mldsa/mldsa_native_asm.S

@@ -328,14 +328,10 @@
 #undef mld_polyveck_pack_eta
 #undef mld_polyveck_pack_t0
 #undef mld_polyveck_pack_w1
-#undef mld_polyveck_pointwise_poly_montgomery
 #undef mld_polyveck_power2round
 #undef mld_polyveck_reduce
-#undef mld_polyveck_shiftl
-#undef mld_polyveck_sub
 #undef mld_polyveck_unpack_eta
 #undef mld_polyveck_unpack_t0
-#undef mld_polyveck_use_hint
 #undef mld_polyvecl
 #undef mld_polyvecl_chknorm
 #undef mld_polyvecl_ntt

mldsa/src/packing.c

@@ -38,17 +38,11 @@ void mld_pack_pk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 MLD_INTERNAL_API
-void mld_unpack_pk_t1(mld_polyveck *t1,
-                      const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES])
+void mld_unpack_pk_t1(mld_poly *t1,
+                      const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
+                      unsigned int i)
 {
-  unsigned int i;
-
-  pk += MLDSA_SEEDBYTES;
-
-  for (i = 0; i < MLDSA_K; ++i)
-  {
-    mld_polyt1_unpack(&t1->vec[i], pk + i * MLDSA_POLYT1_PACKEDBYTES);
-  }
+  mld_polyt1_unpack(t1, pk + MLDSA_SEEDBYTES + i * MLDSA_POLYT1_PACKEDBYTES);
 }
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
@@ -172,75 +166,52 @@ void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 MLD_INTERNAL_API
-int mld_sig_unpack_hints(mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
+int mld_sig_unpack_hints(mld_poly *h, const uint8_t sig[MLDSA_CRYPTO_BYTES],
+                         unsigned int i)
 {
   const uint8_t *packed_hints =
       sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;
-  unsigned int i, j;
-  unsigned int old_hint_count;
+  const unsigned int old_hint_count =
+      (i == 0) ? 0 : packed_hints[MLDSA_OMEGA + i - 1];
+  const unsigned int new_hint_count = packed_hints[MLDSA_OMEGA + i];
+  unsigned int j;
 
-  /* Set all coefficients of all polynomials to 0.    */
-  /* Only those that are actually non-zero hints will */
-  /* be overwritten below.                            */
-  mld_memset(h, 0, sizeof(mld_polyveck));
+  if (new_hint_count < old_hint_count || new_hint_count > MLDSA_OMEGA)
+  {
+    return MLD_ERR_FAIL;
+  }
 
-  old_hint_count = 0;
-  for (i = 0; i < MLDSA_K; ++i)
+  mld_memset(h, 0, sizeof(mld_poly));
+
+  for (j = old_hint_count; j < new_hint_count; ++j)
   __loop__(
-    invariant(i <= MLDSA_K)
-    /* Maintain the post-condition */
-    invariant(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
-    decreases(MLDSA_K - i)
+    invariant(j >= old_hint_count && j <= new_hint_count &&
+              new_hint_count <= MLDSA_OMEGA)
+    invariant(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
+    decreases(new_hint_count - j)
   )
   {
-    /* Grab the hint count for the i'th polynomial */
-    const unsigned int new_hint_count = packed_hints[MLDSA_OMEGA + i];
-
-    /* new_hint_count must increase or stay the same, but also remain */
-    /* less than or equal to MLDSA_OMEGA                              */
-    if (new_hint_count < old_hint_count || new_hint_count > MLDSA_OMEGA)
+    if (j > old_hint_count && packed_hints[j] <= packed_hints[j - 1])
     {
-      /* Error - new_hint_count is invalid */
-      return 1;
+      return MLD_ERR_FAIL;
     }
+    /* Safety: packed_hints[j] is uint8_t (<= 255) and MLDSA_N == 256. */
+    h->coeffs[packed_hints[j]] = 1;
+  }
 
-    /* If new_hint_count == old_hint_count, then this polynomial has */
-    /* zero hints, so this loop executes zero times and we move      */
-    /* straight on to the next polynomial.                           */
-    for (j = old_hint_count; j < new_hint_count; ++j)
+  /* On the last row, also verify that the trailing index slots are zero. */
+  if (i == MLDSA_K - 1)
+  {
+    for (j = new_hint_count; j < MLDSA_OMEGA; ++j)
     __loop__(
-        invariant(i <= MLDSA_K)
-        /* Maintain the post-condition */
-        invariant(j <= new_hint_count && new_hint_count <= MLDSA_OMEGA)
-        invariant(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
-        decreases(new_hint_count - j)
-      )
+      invariant(j <= MLDSA_OMEGA)
+      decreases(MLDSA_OMEGA - j)
+    )
     {
-      const uint8_t this_hint_index = packed_hints[j];
-
-      /* Coefficients must be ordered for strong unforgeability */
-      if (j > old_hint_count && this_hint_index <= packed_hints[j - 1])
+      if (packed_hints[j] != 0)
       {
-        return 1;
+        return MLD_ERR_FAIL;
       }
-      h->vec[i].coeffs[this_hint_index] = 1;
-    }
-
-    old_hint_count = new_hint_count;
-  }
-
-  /* Extra indices must be zero for strong unforgeability */
-  for (j = old_hint_count; j < MLDSA_OMEGA; ++j)
-  __loop__(
-    invariant(j <= MLDSA_OMEGA)
-    /* Maintain the post-condition */
-    invariant(forall(k1, 0, MLDSA_K, array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
-    decreases(MLDSA_OMEGA - j)
-  )
-  {
-    if (packed_hints[j] != 0)
-    {
-      return 1;
     }
   }
 

mldsa/src/packing.h

@@ -163,20 +163,23 @@ __contract__(
 /*************************************************
  * Name:        mld_unpack_pk_t1
  *
- * Description: Unpack the t1 component of a public key pk = (rho, t1).
+ * Description: Unpack a single polynomial of the t1 component of a public
+ *              key pk = (rho, t1).
  *
- * Arguments:   - mld_polyveck *t1: pointer to output vector t1
+ * Arguments:   - mld_poly *t1: pointer to output polynomial t1[i]
  *              - uint8_t pk[]: byte array containing bit-packed pk
+ *              - unsigned int i: row index, must be < MLDSA_K
  **************************************************/
 MLD_INTERNAL_API
-void mld_unpack_pk_t1(mld_polyveck *t1,
-                      const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES])
+void mld_unpack_pk_t1(mld_poly *t1,
+                      const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
+                      unsigned int i)
 __contract__(
   requires(memory_no_alias(pk, MLDSA_CRYPTO_PUBLICKEYBYTES))
-  requires(memory_no_alias(t1, sizeof(mld_polyveck)))
-  assigns(memory_slice(t1, sizeof(mld_polyveck)))
-  ensures(forall(k0, 0, MLDSA_K,
-    array_bound(t1->vec[k0].coeffs, 0, MLDSA_N, 0, 1 << 10)))
+  requires(memory_no_alias(t1, sizeof(mld_poly)))
+  requires(i < MLDSA_K)
+  assigns(memory_slice(t1, sizeof(mld_poly)))
+  ensures(array_bound(t1->coeffs, 0, MLDSA_N, 0, 1 << 10))
 );
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
@@ -240,25 +243,38 @@ __contract__(
 /*************************************************
  * Name:        mld_sig_unpack_hints
  *
- * Description: Unpack hint vector h from a signature buffer.
+ * Description: Decode and validate a single row of the hint vector h
+ *              from a signature buffer. The hint encoding is shared
+ *              across all rows (a count array followed by a single
+ *              index list), so this function performs the validation
+ *              relevant to row i:
+ *                - the i'th hint count is non-decreasing and bounded
+ *                  by MLDSA_OMEGA;
+ *                - the indices for row i are strictly ascending;
+ *                - on i == MLDSA_K - 1, the trailing index slots are
+ *                  zero.
+ *              Callers must invoke this for every
+ *              i in {0, 1, ..., MLDSA_K - 1}; if any call returns
+ *              MLD_ERR_FAIL the encoding is malformed and the signature
+ *              must be rejected.
  *
- * Arguments:   - mld_polyveck *h: pointer to output hint vector
+ * Arguments:   - mld_poly *h: pointer to output polynomial h[i]
  *              - const uint8_t sig[]: signature buffer
- *                (MLDSA_CRYPTO_BYTES); the hint bytes are read from
- *                the trailing MLDSA_POLYVECH_PACKEDBYTES.
+ *              - unsigned int i: row index, must be < MLDSA_K
  *
- * Returns 1 in case of malformed hints; otherwise 0.
+ * Returns MLD_ERR_FAIL in case of malformed hints; otherwise 0.
  **************************************************/
 MLD_INTERNAL_API
 MLD_MUST_CHECK_RETURN_VALUE
-int mld_sig_unpack_hints(mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
+int mld_sig_unpack_hints(mld_poly *h, const uint8_t sig[MLDSA_CRYPTO_BYTES],
+                         unsigned int i)
 __contract__(
   requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
-  requires(memory_no_alias(h, sizeof(mld_polyveck)))
-  assigns(memory_slice(h, sizeof(mld_polyveck)))
-  ensures(forall(k1, 0, MLDSA_K,
-    array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
-  ensures(return_value >= 0 && return_value <= 1)
+  requires(memory_no_alias(h, sizeof(mld_poly)))
+  requires(i < MLDSA_K)
+  assigns(memory_slice(h, sizeof(mld_poly)))
+  ensures(return_value == 0 || return_value == MLD_ERR_FAIL)
+  ensures(return_value == 0 ==> array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
 );
 #endif /* !MLD_CONFIG_NO_VERIFY_API */