Lowram: Share buffers with non-overlapping lifetimes in keygen

integration/opentitan/reduce_alloc.patch

@@ -1,28 +1,28 @@
 # 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..26351ee 100644
+index be11f20..0000000 100644
 --- a/sw/device/lib/crypto/include/mldsa.h
 +++ b/sw/device/lib/crypto/include/mldsa.h
-@@ -41,16 +41,16 @@ enum {
+@@ -41,15 +41,15 @@ enum {
    kOtcryptoMldsa87SeedBytes = 32,
 
    // Work buffer sizes in 32-bit words
 -  kOtcryptoMldsa44WorkBufferKeypairWords = 32992 / sizeof(uint32_t),
 -  kOtcryptoMldsa44WorkBufferSignWords = 32448 / sizeof(uint32_t),
-+  kOtcryptoMldsa44WorkBufferKeypairWords = 28960 / sizeof(uint32_t),
++  kOtcryptoMldsa44WorkBufferKeypairWords = 16672 / sizeof(uint32_t),
 +  kOtcryptoMldsa44WorkBufferSignWords = 20256 / sizeof(uint32_t),
    kOtcryptoMldsa44WorkBufferVerifyWords = 22464 / sizeof(uint32_t),
 
 -  kOtcryptoMldsa65WorkBufferKeypairWords = 46304 / sizeof(uint32_t),
 -  kOtcryptoMldsa65WorkBufferSignWords = 44768 / sizeof(uint32_t),
-+  kOtcryptoMldsa65WorkBufferKeypairWords = 40224 / sizeof(uint32_t),
++  kOtcryptoMldsa65WorkBufferKeypairWords = 23840 / sizeof(uint32_t),
 +  kOtcryptoMldsa65WorkBufferSignWords = 26432 / sizeof(uint32_t),
    kOtcryptoMldsa65WorkBufferVerifyWords = 30720 / sizeof(uint32_t),
 
 -  kOtcryptoMldsa87WorkBufferKeypairWords = 62688 / sizeof(uint32_t),
 -  kOtcryptoMldsa87WorkBufferSignWords = 59104 / sizeof(uint32_t),
-+  kOtcryptoMldsa87WorkBufferKeypairWords = 54560 / sizeof(uint32_t),
++  kOtcryptoMldsa87WorkBufferKeypairWords = 32032 / sizeof(uint32_t),
 +  kOtcryptoMldsa87WorkBufferSignWords = 34624 / sizeof(uint32_t),
    kOtcryptoMldsa87WorkBufferVerifyWords = 41216 / sizeof(uint32_t),
  };

mldsa/mldsa_native.c

@@ -259,7 +259,8 @@
 #undef mld_pack_sig_c
 #undef mld_pack_sig_h_poly
 #undef mld_pack_sig_z
-#undef mld_pack_sk
+#undef mld_pack_sk_rho_key_tr_s2_t0
+#undef mld_pack_sk_s1
 #undef mld_unpack_pk
 #undef mld_unpack_sig
 #undef mld_unpack_sk

mldsa/mldsa_native.h

@@ -938,35 +938,35 @@ int MLD_API_NAMESPACE(pk_from_sk)(
  */
 /* check-magic: off */
 #if defined(MLD_API_LEGACY_CONFIG) || !defined(MLD_CONFIG_REDUCE_RAM)
-#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 41216
+#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 28928
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48448
-#define MLD_TOTAL_ALLOC_44_PK_FROM_SK 45248
+#define MLD_TOTAL_ALLOC_44_PK_FROM_SK 37056
 #define MLD_TOTAL_ALLOC_44_SIGN 44704
 #define MLD_TOTAL_ALLOC_44_VERIFY 34720
-#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 65792
+#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 49408
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 74592
-#define MLD_TOTAL_ALLOC_65_PK_FROM_SK 71872
+#define MLD_TOTAL_ALLOC_65_PK_FROM_SK 60608
 #define MLD_TOTAL_ALLOC_65_SIGN 69312
 #define MLD_TOTAL_ALLOC_65_VERIFY 56288
-#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 104704
+#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 82176
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 115456
-#define MLD_TOTAL_ALLOC_87_PK_FROM_SK 112832
+#define MLD_TOTAL_ALLOC_87_PK_FROM_SK 97472
 #define MLD_TOTAL_ALLOC_87_SIGN 108224
 #define MLD_TOTAL_ALLOC_87_VERIFY 91360
 #else /* MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM */
-#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 28960
-#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 28960
-#define MLD_TOTAL_ALLOC_44_PK_FROM_SK 32992
+#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 16672
+#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 26208
+#define MLD_TOTAL_ALLOC_44_PK_FROM_SK 24800
 #define MLD_TOTAL_ALLOC_44_SIGN 20256
 #define MLD_TOTAL_ALLOC_44_VERIFY 22464
-#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 40224
-#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 40224
-#define MLD_TOTAL_ALLOC_65_PK_FROM_SK 46304
+#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 23840
+#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 36000
+#define MLD_TOTAL_ALLOC_65_PK_FROM_SK 35040
 #define MLD_TOTAL_ALLOC_65_SIGN 26432
 #define MLD_TOTAL_ALLOC_65_VERIFY 30720
-#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 54560
-#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 54560
-#define MLD_TOTAL_ALLOC_87_PK_FROM_SK 62688
+#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 32032
+#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 48448
+#define MLD_TOTAL_ALLOC_87_PK_FROM_SK 47328
 #define MLD_TOTAL_ALLOC_87_SIGN 34624
 #define MLD_TOTAL_ALLOC_87_VERIFY 41216
 #endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */

mldsa/mldsa_native_asm.S

@@ -264,7 +264,8 @@
 #undef mld_pack_sig_c
 #undef mld_pack_sig_h_poly
 #undef mld_pack_sig_z
-#undef mld_pack_sk
+#undef mld_pack_sk_rho_key_tr_s2_t0
+#undef mld_pack_sk_s1
 #undef mld_unpack_pk
 #undef mld_unpack_sig
 #undef mld_unpack_sk

mldsa/src/packing.c

@@ -56,11 +56,19 @@ void mld_unpack_pk(uint8_t rho[MLDSA_SEEDBYTES], mld_polyveck *t1,
 
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API)
 MLD_INTERNAL_API
-void mld_pack_sk(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
-                 const uint8_t rho[MLDSA_SEEDBYTES],
-                 const uint8_t tr[MLDSA_TRBYTES],
-                 const uint8_t key[MLDSA_SEEDBYTES], const mld_polyveck *t0,
-                 const mld_polyvecl *s1, const mld_polyveck *s2)
+void mld_pack_sk_s1(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
+                    const mld_polyvecl *s1)
+{
+  mld_polyvecl_pack_eta(sk + 2 * MLDSA_SEEDBYTES + MLDSA_TRBYTES, s1);
+}
+
+MLD_INTERNAL_API
+void mld_pack_sk_rho_key_tr_s2_t0(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
+                                  const uint8_t rho[MLDSA_SEEDBYTES],
+                                  const uint8_t tr[MLDSA_TRBYTES],
+                                  const uint8_t key[MLDSA_SEEDBYTES],
+                                  const mld_polyveck *t0,
+                                  const mld_polyveck *s2)
 {
   mld_memcpy(sk, rho, MLDSA_SEEDBYTES);
   sk += MLDSA_SEEDBYTES;
@@ -71,7 +79,7 @@ void mld_pack_sk(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
   mld_memcpy(sk, tr, MLDSA_TRBYTES);
   sk += MLDSA_TRBYTES;
 
-  mld_polyvecl_pack_eta(sk, s1);
+  /* s1 already packed via mld_pack_sk_s1 */
   sk += MLDSA_L * MLDSA_POLYETA_PACKEDBYTES;
 
   mld_polyveck_pack_eta(sk, s2);

mldsa/src/packing.h

@@ -32,38 +32,56 @@ __contract__(
 );
 
 
-#define mld_pack_sk MLD_NAMESPACE_KL(pack_sk)
+#define mld_pack_sk_s1 MLD_NAMESPACE_KL(pack_sk_s1)
 /*************************************************
- * Name:        mld_pack_sk
+ * Name:        mld_pack_sk_s1
  *
- * Description: Bit-pack secret key sk = (rho, tr, key, t0, s1, s2).
+ * Description: Bit-pack the s1 component into the secret key.
+ *
+ * Arguments:   - uint8_t sk[]: output byte array
+ *              - const mld_polyvecl *s1: pointer to vector s1
+ **************************************************/
+MLD_INTERNAL_API
+void mld_pack_sk_s1(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
+                    const mld_polyvecl *s1)
+__contract__(
+  requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES))
+  requires(memory_no_alias(s1, sizeof(mld_polyvecl)))
+  requires(forall(k1, 0, MLDSA_L,
+    array_abs_bound(s1->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
+  assigns(memory_slice(sk, MLDSA_CRYPTO_SECRETKEYBYTES))
+);
+
+#define mld_pack_sk_rho_key_tr_s2_t0 MLD_NAMESPACE_KL(pack_sk_rho_key_tr_s2_t0)
+/*************************************************
+ * Name:        mld_pack_sk_rho_key_tr_s2_t0
+ *
+ * Description: Bit-pack rho, key, tr, s2, t0 into the secret key.
+ *              s1 must already be packed via mld_pack_sk_s1.
  *
  * Arguments:   - uint8_t sk[]: output byte array
  *              - const uint8_t rho[]: byte array containing rho
  *              - const uint8_t tr[]: byte array containing tr
  *              - const uint8_t key[]: byte array containing key
  *              - const mld_polyveck *t0: pointer to vector t0
- *              - const mld_polyvecl *s1: pointer to vector s1
  *              - const mld_polyveck *s2: pointer to vector s2
  **************************************************/
 MLD_INTERNAL_API
-void mld_pack_sk(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
-                 const uint8_t rho[MLDSA_SEEDBYTES],
-                 const uint8_t tr[MLDSA_TRBYTES],
-                 const uint8_t key[MLDSA_SEEDBYTES], const mld_polyveck *t0,
-                 const mld_polyvecl *s1, const mld_polyveck *s2)
+void mld_pack_sk_rho_key_tr_s2_t0(uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
+                                  const uint8_t rho[MLDSA_SEEDBYTES],
+                                  const uint8_t tr[MLDSA_TRBYTES],
+                                  const uint8_t key[MLDSA_SEEDBYTES],
+                                  const mld_polyveck *t0,
+                                  const mld_polyveck *s2)
 __contract__(
   requires(memory_no_alias(sk, MLDSA_CRYPTO_SECRETKEYBYTES))
   requires(memory_no_alias(rho, MLDSA_SEEDBYTES))
   requires(memory_no_alias(tr, MLDSA_TRBYTES))
   requires(memory_no_alias(key, MLDSA_SEEDBYTES))
   requires(memory_no_alias(t0, sizeof(mld_polyveck)))
-  requires(memory_no_alias(s1, sizeof(mld_polyvecl)))
   requires(memory_no_alias(s2, sizeof(mld_polyveck)))
   requires(forall(k0, 0, MLDSA_K,
     array_bound(t0->vec[k0].coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1)))
-  requires(forall(k1, 0, MLDSA_L,
-    array_abs_bound(s1->vec[k1].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
   requires(forall(k2, 0, MLDSA_K,
     array_abs_bound(s2->vec[k2].coeffs, 0, MLDSA_N, MLDSA_ETA + 1)))
   assigns(memory_slice(sk, MLDSA_CRYPTO_SECRETKEYBYTES))

mldsa/src/poly.c

@@ -516,6 +516,7 @@ void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a)
   __loop__(
     assigns(i, memory_slice(a0, sizeof(mld_poly)), memory_slice(a1, sizeof(mld_poly)))
     invariant(i <= MLDSA_N)
+    invariant(forall(k0, i, MLDSA_N, a->coeffs[k0] == loop_entry(*a).coeffs[k0]))
     invariant(array_bound(a0->coeffs, 0, i, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1))
     invariant(array_bound(a1->coeffs, 0, i, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1))
     decreases(MLDSA_N - i)

mldsa/src/poly.h

@@ -209,20 +209,22 @@ __contract__(
  * Description: For all coefficients c of the input polynomial,
  *              compute c0, c1 such that c mod MLDSA_Q = c1*2^MLDSA_D + c0
  *              with -2^{MLDSA_D-1} < c0 <= 2^{MLDSA_D-1}. Assumes coefficients
- *to be standard representatives.
+ *              to be standard representatives.
  *
  * Arguments:   - mld_poly *a1: pointer to output polynomial with coefficients
- *c1
+ *                c1
  *              - mld_poly *a0: pointer to output polynomial with coefficients
- *c0
+ *                c0; may alias the input polynomial a
  *              - const mld_poly *a: pointer to input polynomial
  **************************************************/
 MLD_INTERNAL_API
 void mld_poly_power2round(mld_poly *a1, mld_poly *a0, const mld_poly *a)
 __contract__(
   requires(memory_no_alias(a0, sizeof(mld_poly)))
   requires(memory_no_alias(a1, sizeof(mld_poly)))
-  requires(memory_no_alias(a, sizeof(mld_poly)))
+  /* The implementation does not require a0 == a, but the single call site
+   * aliases them and asserting equality simplifies the proof. */
+  requires(a0 == a)
   requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
   assigns(memory_slice(a1, sizeof(mld_poly)))
   assigns(memory_slice(a0, sizeof(mld_poly)))

mldsa/src/polyvec.c

@@ -666,6 +666,7 @@ void mld_polyveck_power2round(mld_polyveck *v1, mld_polyveck *v0,
   __loop__(
     assigns(i, memory_slice(v0, sizeof(mld_polyveck)), memory_slice(v1, sizeof(mld_polyveck)))
     invariant(i <= MLDSA_K)
+    invariant(forall(k0, i, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
     invariant(forall(k1, 0, i, array_bound(v0->vec[k1].coeffs, 0, MLDSA_N, -(MLD_2_POW_D/2)+1, (MLD_2_POW_D/2)+1)))
     invariant(forall(k2, 0, i, array_bound(v1->vec[k2].coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1)))
     decreases(MLDSA_K - i)

mldsa/src/polyvec.h

@@ -372,7 +372,7 @@ __contract__(
  * Arguments:   - mld_polyveck *v1: pointer to output vector of polynomials with
  *                              coefficients a1
  *              - mld_polyveck *v0: pointer to output vector of polynomials with
- *                              coefficients a0
+ *                              coefficients a0; may alias the input vector v
  *              - const mld_polyveck *v: pointer to input vector
  **************************************************/
 MLD_INTERNAL_API
@@ -381,7 +381,9 @@ void mld_polyveck_power2round(mld_polyveck *v1, mld_polyveck *v0,
 __contract__(
   requires(memory_no_alias(v1, sizeof(mld_polyveck)))
   requires(memory_no_alias(v0, sizeof(mld_polyveck)))
-  requires(memory_no_alias(v, sizeof(mld_polyveck)))
+  /* The implementation does not require v0 == v, but the single call site
+   * aliases them and asserting equality simplifies the proof. */
+  requires(v0 == v)
   requires(forall(k0, 0, MLDSA_K, array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
   assigns(memory_slice(v1, sizeof(mld_polyveck)))
   assigns(memory_slice(v0, sizeof(mld_polyveck)))