diff --git a/BIBLIOGRAPHY.md b/BIBLIOGRAPHY.md
index d69700bec7..388f26f74b 100644
--- a/BIBLIOGRAPHY.md
+++ b/BIBLIOGRAPHY.md
@@ -64,6 +64,17 @@ source code and documentation.
 * Referenced from:
   - [proofs/isabelle/neon_ntt/README.md](proofs/isabelle/neon_ntt/README.md)
 
+### `DilithiumMemory`
+
+* Dilithium for Memory Constrained Devices
+* Author(s):
+  - Joppe W. Bos
+  - Joost Renes
+  - Amber Sprenkels
+* URL: https://eprint.iacr.org/2022/323
+* Referenced from:
+  - [mldsa/src/sign.c](mldsa/src/sign.c)
+
 ### `FIPS140_3_IG`
 
 * Implementation Guidance for FIPS 140-3 and the Cryptographic Module Validation Program
diff --git a/BIBLIOGRAPHY.yml b/BIBLIOGRAPHY.yml
index b454402639..2c749b44c4 100644
--- a/BIBLIOGRAPHY.yml
+++ b/BIBLIOGRAPHY.yml
@@ -92,6 +92,14 @@
   author: National Institute of Standards and Technology
   url: https://csrc.nist.gov/projects/cryptographic-module-validation-program/fips-140-3-ig-announcements
 
+- id: DilithiumMemory
+  name: "Dilithium for Memory Constrained Devices"
+  author:
+  - Bos, Joppe W.
+  - Renes, Joost
+  - Sprenkels, Amber
+  url: https://eprint.iacr.org/2022/323
+
 - id: Round3_Spec
   name: "CRYSTALS-Dilithium Algorithm Specifications and Supporting Documentation (Version 3.1)"
   author:
diff --git a/integration/pavona/sign-work-buffer-size.patch b/integration/pavona/sign-work-buffer-size.patch
new file mode 100644
index 0000000000..a86f921b70
--- /dev/null
+++ b/integration/pavona/sign-work-buffer-size.patch
@@ -0,0 +1,30 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+#
+# Track the reduced signing work buffer of mldsa-native. The crypto
+# library wrapper pins the work buffer sizes and cross-checks them
+# against MLD_TOTAL_ALLOC_* with a static assertion, so the signing
+# sizes have to follow when mldsa-native allocates less.
+
+diff --git a/sw/device/lib/crypto/include/mldsa.h b/sw/device/lib/crypto/include/mldsa.h
+--- a/sw/device/lib/crypto/include/mldsa.h
++++ b/sw/device/lib/crypto/include/mldsa.h
+@@ -42,15 +42,15 @@
+ 
+   // Work buffer sizes in 32-bit words
+   kOtcryptoMldsa44WorkBufferKeypairWords = 11584 / sizeof(uint32_t),
+-  kOtcryptoMldsa44WorkBufferSignWords = 13120 / sizeof(uint32_t),
++  kOtcryptoMldsa44WorkBufferSignWords = 9792 / sizeof(uint32_t),
+   kOtcryptoMldsa44WorkBufferVerifyWords = 9120 / sizeof(uint32_t),
+ 
+   kOtcryptoMldsa65WorkBufferKeypairWords = 14656 / sizeof(uint32_t),
+-  kOtcryptoMldsa65WorkBufferSignWords = 17248 / sizeof(uint32_t),
++  kOtcryptoMldsa65WorkBufferSignWords = 11872 / sizeof(uint32_t),
+   kOtcryptoMldsa65WorkBufferVerifyWords = 10208 / sizeof(uint32_t),
+ 
+   kOtcryptoMldsa87WorkBufferKeypairWords = 18752 / sizeof(uint32_t),
+-  kOtcryptoMldsa87WorkBufferSignWords = 21344 / sizeof(uint32_t),
++  kOtcryptoMldsa87WorkBufferSignWords = 14176 / sizeof(uint32_t),
+   kOtcryptoMldsa87WorkBufferVerifyWords = 12512 / sizeof(uint32_t),
+ };
+ 
diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c
index 85e9e60f64..1491696316 100644
--- a/mldsa/mldsa_native.c
+++ b/mldsa/mldsa_native.c
@@ -274,6 +274,9 @@
 #undef MLDSA_POLYW1_PACKEDBYTES
 #undef MLDSA_POLYW1_PACKEDBYTES_32
 #undef MLDSA_POLYW1_PACKEDBYTES_88
+#undef MLDSA_POLYW1_PACKED_BITS
+#undef MLDSA_POLYW1_PACKED_BITS_32
+#undef MLDSA_POLYW1_PACKED_BITS_88
 #undef MLDSA_POLYZ_PACKEDBYTES
 #undef MLDSA_Q
 #undef MLDSA_Q_HALF
@@ -316,6 +319,7 @@
 #undef mld_polyeta_pack
 #undef mld_polyeta_unpack
 #undef mld_polyw1_pack
+#undef mld_polyw1_unpack
 #undef mld_polyz_pack
 #undef mld_polyz_unpack
 /* mldsa/src/polyvec.h */
@@ -323,11 +327,10 @@
 #undef mld_polyveck
 #undef mld_polyveck_caddq
 #undef mld_polyveck_chknorm
-#undef mld_polyveck_decompose
+#undef mld_polyveck_decompose_pack_w1
 #undef mld_polyveck_invntt_tomont
 #undef mld_polyveck_ntt
 #undef mld_polyveck_pack_eta
-#undef mld_polyveck_pack_w1
 #undef mld_polyveck_reduce
 #undef mld_polyveck_unpack_eta
 #undef mld_polyvecl
@@ -390,6 +393,9 @@
 #undef mld_yvec_init_eager
 #undef mld_yvec_init_lazy
 #undef mld_yvec_lazy
+#undef mld_yvec_scratch
+#undef mld_yvec_scratch_eager
+#undef mld_yvec_scratch_lazy
 /* mldsa/src/rounding.h */
 #undef MLD_2_POW_D
 #undef MLD_ROUNDING_H
@@ -484,6 +490,8 @@
 #undef mld_polyt1_unpack
 #undef mld_polyw1_pack_32
 #undef mld_polyw1_pack_88
+#undef mld_polyw1_unpack_32
+#undef mld_polyw1_unpack_88
 /* mldsa/src/randombytes.h */
 #undef MLD_RANDOMBYTES_H
 /* mldsa/src/reduce.h */
diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h
index a38a2c4154..c50b3db8e7 100644
--- a/mldsa/mldsa_native.h
+++ b/mldsa/mldsa_native.h
@@ -889,35 +889,35 @@ int MLD_API_NAMESPACE(pk_from_sk)(
 /* check-magic: off */
 #if !defined(MLD_CONFIG_REDUCE_RAM)
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 26912
-#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48480
+#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48224
 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 28480
-#define MLD_TOTAL_ALLOC_44_SIGN 44704
+#define MLD_TOTAL_ALLOC_44_SIGN 44448
 #define MLD_TOTAL_ALLOC_44_VERIFY 24448
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 44320
-#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 74624
+#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 73344
 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 46720
-#define MLD_TOTAL_ALLOC_65_SIGN 69312
+#define MLD_TOTAL_ALLOC_65_SIGN 68032
 #define MLD_TOTAL_ALLOC_65_VERIFY 39872
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 75040
-#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 115488
+#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 114464
 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 78272
-#define MLD_TOTAL_ALLOC_87_SIGN 108224
+#define MLD_TOTAL_ALLOC_87_SIGN 107200
 #define MLD_TOTAL_ALLOC_87_VERIFY 68800
 #else /* !MLD_CONFIG_REDUCE_RAM */
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 11584
-#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 16896
+#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 13568
 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 13152
-#define MLD_TOTAL_ALLOC_44_SIGN 13120
+#define MLD_TOTAL_ALLOC_44_SIGN 9792
 #define MLD_TOTAL_ALLOC_44_VERIFY 9120
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 14656
-#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 22560
+#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 17184
 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 17056
-#define MLD_TOTAL_ALLOC_65_SIGN 17248
+#define MLD_TOTAL_ALLOC_65_SIGN 11872
 #define MLD_TOTAL_ALLOC_65_VERIFY 10208
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 18752
-#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 28608
+#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 21440
 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 21984
-#define MLD_TOTAL_ALLOC_87_SIGN 21344
+#define MLD_TOTAL_ALLOC_87_SIGN 14176
 #define MLD_TOTAL_ALLOC_87_VERIFY 12512
 #endif /* MLD_CONFIG_REDUCE_RAM */
 /* check-magic: on */
diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S
index 61d4186a5f..7a2b330e45 100644
--- a/mldsa/mldsa_native_asm.S
+++ b/mldsa/mldsa_native_asm.S
@@ -301,6 +301,9 @@
 #undef MLDSA_POLYW1_PACKEDBYTES
 #undef MLDSA_POLYW1_PACKEDBYTES_32
 #undef MLDSA_POLYW1_PACKEDBYTES_88
+#undef MLDSA_POLYW1_PACKED_BITS
+#undef MLDSA_POLYW1_PACKED_BITS_32
+#undef MLDSA_POLYW1_PACKED_BITS_88
 #undef MLDSA_POLYZ_PACKEDBYTES
 #undef MLDSA_Q
 #undef MLDSA_Q_HALF
@@ -343,6 +346,7 @@
 #undef mld_polyeta_pack
 #undef mld_polyeta_unpack
 #undef mld_polyw1_pack
+#undef mld_polyw1_unpack
 #undef mld_polyz_pack
 #undef mld_polyz_unpack
 /* mldsa/src/polyvec.h */
@@ -350,11 +354,10 @@
 #undef mld_polyveck
 #undef mld_polyveck_caddq
 #undef mld_polyveck_chknorm
-#undef mld_polyveck_decompose
+#undef mld_polyveck_decompose_pack_w1
 #undef mld_polyveck_invntt_tomont
 #undef mld_polyveck_ntt
 #undef mld_polyveck_pack_eta
-#undef mld_polyveck_pack_w1
 #undef mld_polyveck_reduce
 #undef mld_polyveck_unpack_eta
 #undef mld_polyvecl
@@ -417,6 +420,9 @@
 #undef mld_yvec_init_eager
 #undef mld_yvec_init_lazy
 #undef mld_yvec_lazy
+#undef mld_yvec_scratch
+#undef mld_yvec_scratch_eager
+#undef mld_yvec_scratch_lazy
 /* mldsa/src/rounding.h */
 #undef MLD_2_POW_D
 #undef MLD_ROUNDING_H
@@ -511,6 +517,8 @@
 #undef mld_polyt1_unpack
 #undef mld_polyw1_pack_32
 #undef mld_polyw1_pack_88
+#undef mld_polyw1_unpack_32
+#undef mld_polyw1_unpack_88
 /* mldsa/src/randombytes.h */
 #undef MLD_RANDOMBYTES_H
 /* mldsa/src/reduce.h */
diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c
index 48e73cc65d..cef309adc2 100644
--- a/mldsa/src/packing.c
+++ b/mldsa/src/packing.c
@@ -74,7 +74,8 @@ void mld_pack_sig_c(uint8_t sig[MLDSA_CRYPTO_BYTES],
 
 MLD_INTERNAL_API
 int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
-                   const mld_polyveck *w1)
+                   const uint8_t w1_packed[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
+                   mld_poly *scratch)
 {
   unsigned int j, k, n;
 
@@ -100,11 +101,14 @@ int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
    * before the call), so a data-dependent early return is fine. */
   for (k = 0; k < MLDSA_K; k++)
   __loop__(
-    assigns(k, j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
+    assigns(k, j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES),
+            memory_slice(scratch, sizeof(mld_poly)))
     invariant(k <= MLDSA_K && n <= MLDSA_OMEGA)
     decreases(MLDSA_K - k)
   )
   {
+    mld_polyw1_unpack(scratch, w1_packed + k * MLDSA_POLYW1_PACKEDBYTES);
+
     for (j = 0; j < MLDSA_N; j++)
     __loop__(
       assigns(j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES))
@@ -113,7 +117,7 @@ int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
     )
     {
       const unsigned int hint_bit =
-          mld_make_hint(w0->vec[k].coeffs[j], w1->vec[k].coeffs[j]);
+          mld_make_hint(w0->vec[k].coeffs[j], scratch->coeffs[j]);
       if (hint_bit)
       {
         if (n == MLDSA_OMEGA)
diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h
index ec5755433f..6adcab37c3 100644
--- a/mldsa/src/packing.h
+++ b/mldsa/src/packing.h
@@ -107,9 +107,12 @@ __contract__(
  * MakeHint valid only for the values arising during signing; see the block
  * comment in mld_attempt_signature_generation (sign.c).}
  *
- * @param[in,out] sig Byte array containing signature.
- * @param[in]     w0  Pointer to low part of input vector.
- * @param[in]     w1  Pointer to high part of input vector.
+ * @param[in,out] sig       Byte array containing signature.
+ * @param[in]     w0        Pointer to low part of input vector.
+ * @param[in]     w1_packed Bit-packed high part of input vector, as produced
+ *                          by mld_polyw1_pack.
+ * @param[out]    scratch   Scratch polynomial, used to unpack one row of the
+ *                          high part at a time.
  *
  * @retval 0            Success.
  * @retval MLD_ERR_FAIL The total number of hints exceeds MLDSA_OMEGA. In this
@@ -120,12 +123,15 @@ __contract__(
 MLD_INTERNAL_API
 MLD_MUST_CHECK_RETURN_VALUE
 int mld_pack_sig_h(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_polyveck *w0,
-                   const mld_polyveck *w1)
+                   const uint8_t w1_packed[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
+                   mld_poly *scratch)
 __contract__(
   requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
   requires(memory_no_alias(w0, sizeof(mld_polyveck)))
-  requires(memory_no_alias(w1, sizeof(mld_polyveck)))
+  requires(memory_no_alias(w1_packed, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
+  requires(memory_no_alias(scratch, sizeof(mld_poly)))
   assigns(memory_slice(sig + MLDSA_SIG_H_OFFSET, MLDSA_POLYVECH_PACKEDBYTES))
+  assigns(memory_slice(scratch, sizeof(mld_poly)))
   ensures(return_value == 0 || return_value == MLD_ERR_FAIL)
 );
 
diff --git a/mldsa/src/params.h b/mldsa/src/params.h
index db3bf6c539..4765efb8eb 100644
--- a/mldsa/src/params.h
+++ b/mldsa/src/params.h
@@ -16,8 +16,12 @@
 
 #define MLDSA_GAMMA2_88 ((MLDSA_Q - 1) / 88)
 #define MLDSA_GAMMA2_32 ((MLDSA_Q - 1) / 32)
-#define MLDSA_POLYW1_PACKEDBYTES_88 192
-#define MLDSA_POLYW1_PACKEDBYTES_32 128
+/* Bits per w1 coefficient: bitlen((MLDSA_Q-1)/(2*MLDSA_GAMMA2) - 1), i.e.
+ * bitlen(43) for MLDSA_GAMMA2_88 and bitlen(15) for MLDSA_GAMMA2_32. */
+#define MLDSA_POLYW1_PACKED_BITS_88 6
+#define MLDSA_POLYW1_PACKED_BITS_32 4
+#define MLDSA_POLYW1_PACKEDBYTES_88 (MLDSA_N * MLDSA_POLYW1_PACKED_BITS_88 / 8)
+#define MLDSA_POLYW1_PACKEDBYTES_32 (MLDSA_N * MLDSA_POLYW1_PACKED_BITS_32 / 8)
 
 #if MLD_CONFIG_PARAMETER_SET == 44
 
@@ -32,6 +36,7 @@
 #define MLDSA_CTILDEBYTES 32
 #define MLDSA_POLYZ_PACKEDBYTES 576
 #define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_88
+#define MLDSA_POLYW1_PACKED_BITS MLDSA_POLYW1_PACKED_BITS_88
 #define MLDSA_POLYETA_PACKEDBYTES 96
 
 #elif MLD_CONFIG_PARAMETER_SET == 65
@@ -47,6 +52,7 @@
 #define MLDSA_CTILDEBYTES 48
 #define MLDSA_POLYZ_PACKEDBYTES 640
 #define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32
+#define MLDSA_POLYW1_PACKED_BITS MLDSA_POLYW1_PACKED_BITS_32
 #define MLDSA_POLYETA_PACKEDBYTES 128
 
 #elif MLD_CONFIG_PARAMETER_SET == 87
@@ -62,6 +68,7 @@
 #define MLDSA_CTILDEBYTES 64
 #define MLDSA_POLYZ_PACKEDBYTES 640
 #define MLDSA_POLYW1_PACKEDBYTES MLDSA_POLYW1_PACKEDBYTES_32
+#define MLDSA_POLYW1_PACKED_BITS MLDSA_POLYW1_PACKED_BITS_32
 #define MLDSA_POLYETA_PACKEDBYTES 96
 
 #endif /* MLD_CONFIG_PARAMETER_SET == 87 */
diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c
index 4d74306841..ba58474413 100644
--- a/mldsa/src/poly.c
+++ b/mldsa/src/poly.c
@@ -1057,6 +1057,57 @@ void mld_polyw1_pack_32(uint8_t r[MLDSA_POLYW1_PACKEDBYTES_32],
           || MLD_CONFIG_PARAMETER_SET == 87 */
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
 
+#if !defined(MLD_CONFIG_NO_SIGN_API)
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
+MLD_INTERNAL_API
+void mld_polyw1_unpack_88(mld_poly *r,
+                          const uint8_t a[MLDSA_POLYW1_PACKEDBYTES_88])
+{
+  unsigned int i;
+
+  for (i = 0; i < MLDSA_N / 4; ++i)
+  __loop__(
+    invariant(i <= MLDSA_N/4)
+    invariant(array_bound(r->coeffs, 0, i*4, 0, 1 << 6))
+    decreases(MLDSA_N / 4 - i))
+  {
+    r->coeffs[4 * i + 0] = a[3 * i + 0] & 0x3F;
+    r->coeffs[4 * i + 1] =
+        ((a[3 * i + 0] >> 6) | ((int32_t)a[3 * i + 1] << 2)) & 0x3F;
+    r->coeffs[4 * i + 2] =
+        ((a[3 * i + 1] >> 4) | ((int32_t)a[3 * i + 2] << 4)) & 0x3F;
+    r->coeffs[4 * i + 3] = a[3 * i + 2] >> 2;
+  }
+
+  mld_assert_bound(r->coeffs, MLDSA_N, 0, 1 << 6);
+}
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
+        */
+
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
+    (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
+MLD_INTERNAL_API
+void mld_polyw1_unpack_32(mld_poly *r,
+                          const uint8_t a[MLDSA_POLYW1_PACKEDBYTES_32])
+{
+  unsigned int i;
+
+  for (i = 0; i < MLDSA_N / 2; ++i)
+  __loop__(
+    invariant(i <= MLDSA_N/2)
+    invariant(array_bound(r->coeffs, 0, i*2, 0, 1 << 4))
+    decreases(MLDSA_N / 2 - i))
+  {
+    r->coeffs[2 * i + 0] = a[i] & 0x0F;
+    r->coeffs[2 * i + 1] = a[i] >> 4;
+  }
+
+  mld_assert_bound(r->coeffs, MLDSA_N, 0, 1 << 4);
+}
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
+          || MLD_CONFIG_PARAMETER_SET == 87 */
+#endif /* !MLD_CONFIG_NO_SIGN_API */
+
 #else  /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
 MLD_EMPTY_CU(mld_poly)
 #endif /* MLD_CONFIG_MULTILEVEL_NO_SHARED */
diff --git a/mldsa/src/poly.h b/mldsa/src/poly.h
index 2467f23798..dbdf803f27 100644
--- a/mldsa/src/poly.h
+++ b/mldsa/src/poly.h
@@ -461,4 +461,55 @@ __contract__(
           || MLD_CONFIG_PARAMETER_SET == 87 */
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
 
+#if !defined(MLD_CONFIG_NO_SIGN_API)
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
+#define mld_polyw1_unpack_88 MLD_NAMESPACE(polyw1_unpack_88)
+/**
+ * Unpack polynomial w1 packed with 6 bits per coefficient.
+ * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/88
+ * (ML-DSA-44). Inverse of mld_polyw1_pack_88.
+ *
+ * @spec{Implements @[FIPS204, Algorithm 18, SimpleBitUnpack] for b = 43.}
+ *
+ * @param[out] r Pointer to output polynomial.
+ * @param[in]  a Byte array with bit-packed polynomial.
+ */
+MLD_INTERNAL_API
+void mld_polyw1_unpack_88(mld_poly *r,
+                          const uint8_t a[MLDSA_POLYW1_PACKEDBYTES_88])
+__contract__(
+  requires(memory_no_alias(r, sizeof(mld_poly)))
+  requires(memory_no_alias(a, MLDSA_POLYW1_PACKEDBYTES_88))
+  assigns(memory_slice(r, sizeof(mld_poly)))
+  ensures(array_bound(r->coeffs, 0, MLDSA_N, 0, 1 << 6))
+);
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 44 \
+        */
+
+#if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
+    (MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
+#define mld_polyw1_unpack_32 MLD_NAMESPACE(polyw1_unpack_32)
+/**
+ * Unpack polynomial w1 packed with 4 bits per coefficient.
+ * This is the variant for parameter sets with MLDSA_GAMMA2 = (MLDSA_Q-1)/32
+ * (ML-DSA-65 and ML-DSA-87). Inverse of mld_polyw1_pack_32.
+ *
+ * @spec{Implements @[FIPS204, Algorithm 18, SimpleBitUnpack] for b = 15.}
+ *
+ * @param[out] r Pointer to output polynomial.
+ * @param[in]  a Byte array with bit-packed polynomial.
+ */
+MLD_INTERNAL_API
+void mld_polyw1_unpack_32(mld_poly *r,
+                          const uint8_t a[MLDSA_POLYW1_PACKEDBYTES_32])
+__contract__(
+  requires(memory_no_alias(r, sizeof(mld_poly)))
+  requires(memory_no_alias(a, MLDSA_POLYW1_PACKEDBYTES_32))
+  assigns(memory_slice(r, sizeof(mld_poly)))
+  ensures(array_bound(r->coeffs, 0, MLDSA_N, 0, 1 << 4))
+);
+#endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLD_CONFIG_PARAMETER_SET == 65 \
+          || MLD_CONFIG_PARAMETER_SET == 87 */
+#endif /* !MLD_CONFIG_NO_SIGN_API */
+
 #endif /* !MLD_POLY_H */
diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h
index 2dca8f17cd..e767466041 100644
--- a/mldsa/src/poly_kl.h
+++ b/mldsa/src/poly_kl.h
@@ -364,4 +364,34 @@ __contract__(
 }
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
 
+#if !defined(MLD_CONFIG_NO_SIGN_API)
+#define mld_polyw1_unpack MLD_NAMESPACE_KL(polyw1_unpack)
+/**
+ * Unpack polynomial w1. Inverse of mld_polyw1_pack; dispatches to the
+ * value-specialized variant for the selected parameter set.
+ *
+ * @spec{Implements @[FIPS204, Algorithm 18, SimpleBitUnpack] for the two
+ * values of b arising for w1: b = 43 (ML-DSA-44) and b = 15 (ML-DSA-65 and
+ * ML-DSA-87).}
+ *
+ * @param[out] r Pointer to output polynomial.
+ * @param[in]  a Byte array with bit-packed polynomial.
+ */
+static MLD_INLINE void mld_polyw1_unpack(
+    mld_poly *r, const uint8_t a[MLDSA_POLYW1_PACKEDBYTES])
+__contract__(
+  requires(memory_no_alias(r, sizeof(mld_poly)))
+  requires(memory_no_alias(a, MLDSA_POLYW1_PACKEDBYTES))
+  assigns(memory_slice(r, sizeof(mld_poly)))
+  ensures(array_bound(r->coeffs, 0, MLDSA_N, 0, 1 << MLDSA_POLYW1_PACKED_BITS))
+)
+{
+#if MLD_CONFIG_PARAMETER_SET == 44
+  mld_polyw1_unpack_88(r, a);
+#else
+  mld_polyw1_unpack_32(r, a);
+#endif
+}
+#endif /* !MLD_CONFIG_NO_SIGN_API */
+
 #endif /* !MLD_POLY_KL_H */
diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c
index 8d427a8f85..248dbef3ff 100644
--- a/mldsa/src/polyvec.c
+++ b/mldsa/src/polyvec.c
@@ -365,54 +365,34 @@ uint32_t mld_polyveck_chknorm(const mld_polyveck *v, int32_t bound)
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)
 MLD_INTERNAL_API
-void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0)
+void mld_polyveck_decompose_pack_w1(
+    uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES], mld_polyveck *v0,
+    mld_poly *scratch)
 {
   unsigned int i;
   mld_assert_bound_2d(v0->vec, MLDSA_K, MLDSA_N, 0, MLDSA_Q);
 
   for (i = 0; i < MLDSA_K; ++i)
   __loop__(
-    assigns(i, memory_slice(v0, sizeof(mld_polyveck)), memory_slice(v1, sizeof(mld_polyveck)))
+    assigns(i, memory_slice(v0, sizeof(mld_polyveck)),
+            memory_slice(scratch, sizeof(mld_poly)),
+            memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
     invariant(i <= MLDSA_K)
     invariant(forall(k1, 0, i,
-                     array_bound(v1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))))
-    invariant(forall(k2, 0, i,
-                     array_abs_bound(v0->vec[k2].coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)))
-    invariant(forall(k3, i, MLDSA_K,
-                     array_bound(v0->vec[k3].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
+                     array_abs_bound(v0->vec[k1].coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)))
+    invariant(forall(k2, i, MLDSA_K,
+                     array_bound(v0->vec[k2].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
     decreases(MLDSA_K - i)
   )
   {
-    mld_poly_decompose(&v1->vec[i], &v0->vec[i]);
+    mld_poly_decompose(scratch, &v0->vec[i]);
+    mld_polyw1_pack(&r[i * MLDSA_POLYW1_PACKEDBYTES], scratch);
   }
 
-  mld_assert_bound_2d(v1->vec, MLDSA_K, MLDSA_N, 0,
-                      (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
   mld_assert_abs_bound_2d(v0->vec, MLDSA_K, MLDSA_N, MLDSA_GAMMA2 + 1);
 }
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
-#if !defined(MLD_CONFIG_NO_SIGN_API)
-MLD_INTERNAL_API
-void mld_polyveck_pack_w1(uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
-                          const mld_polyveck *w1)
-{
-  unsigned int i;
-  mld_assert_bound_2d(w1->vec, MLDSA_K, MLDSA_N, 0,
-                      (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
-
-  for (i = 0; i < MLDSA_K; ++i)
-  __loop__(
-    assigns(i, memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
-    invariant(i <= MLDSA_K)
-    decreases(MLDSA_K - i)
-  )
-  {
-    mld_polyw1_pack(&r[i * MLDSA_POLYW1_PACKEDBYTES], &w1->vec[i]);
-  }
-}
-#endif /* !MLD_CONFIG_NO_SIGN_API */
-
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API)
 MLD_INTERNAL_API
 void mld_polyveck_pack_eta(uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES],
diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h
index 8a09c66711..7e785ba345 100644
--- a/mldsa/src/polyvec.h
+++ b/mldsa/src/polyvec.h
@@ -266,60 +266,49 @@ __contract__(
 #endif /* !MLD_CONFIG_NO_KEYPAIR_API */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)
-#define mld_polyveck_decompose MLD_NAMESPACE_KL(polyveck_decompose)
+#define mld_polyveck_decompose_pack_w1 \
+  MLD_NAMESPACE_KL(polyveck_decompose_pack_w1)
 /**
  * For all coefficients a of polynomials in vector of length MLDSA_K, compute
  * high and low bits a0, a1 such a mod^+ MLDSA_Q = a1*ALPHA + a0 with
  * -ALPHA/2 < a0 <= ALPHA/2 except a1 = (MLDSA_Q-1)/ALPHA where we set
  * a1 = 0 and -ALPHA/2 <= a0 = a mod MLDSA_Q - MLDSA_Q < 0. Assumes
- * coefficients to be standard representatives.
+ * coefficients to be standard representatives. The low bits replace the input
+ * vector, the high bits are bit-packed into r.
  *
- * @reference{The reference implementation has the input polynomial as a
- * separate argument that may be aliased with either of the outputs. Removing
- * the aliasing eases CBMC proofs.}
+ * Decomposing and packing are fused so that the high bits are never held as a
+ * vector of polynomials, saving MLDSA_K * sizeof(mld_poly) bytes. During
+ * MakeHint, a single entry of w1 is instead unpacked on demand.
  *
- * @param[out]    v1 Pointer to output vector of polynomials with
- *                   coefficients a1.
- * @param[in,out] v0 Pointer to input/output vector of polynomials. Output
- *                   polynomial has coefficients a0.
+ * @spec{Combines @[FIPS204, Algorithm 36, Decompose] with
+ * @[FIPS204, Algorithm 28, w1Encode].}
+ *
+ * @reference{The reference implementation has the Decompose input as a separate
+ * argument that may be aliased with either of the outputs. Removing the
+ * aliasing eases CBMC proofs.}
+ *
+ * @param[out]    r       Pointer to output byte array with at least
+ *                        MLDSA_K * MLDSA_POLYW1_PACKEDBYTES bytes.
+ * @param[in,out] v0      Pointer to input/output vector of polynomials. Output
+ *                        polynomials have coefficients a0.
+ * @param[out]    scratch Scratch polynomial holding the high bits of the
+ *                        polynomial currently being packed.
  */
 MLD_INTERNAL_API
-void mld_polyveck_decompose(mld_polyveck *v1, mld_polyveck *v0)
+void mld_polyveck_decompose_pack_w1(
+    uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES], mld_polyveck *v0,
+    mld_poly *scratch)
 __contract__(
-  requires(memory_no_alias(v1,  sizeof(mld_polyveck)))
+  requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
   requires(memory_no_alias(v0, sizeof(mld_polyveck)))
+  requires(memory_no_alias(scratch, sizeof(mld_poly)))
   requires(forall(k0, 0, MLDSA_K,
     array_bound(v0->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
-  assigns(memory_slice(v1, sizeof(mld_polyveck)))
+  assigns(memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
   assigns(memory_slice(v0, sizeof(mld_polyveck)))
+  assigns(memory_slice(scratch, sizeof(mld_poly)))
   ensures(forall(k1, 0, MLDSA_K,
-                 array_bound(v1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))))
-  ensures(forall(k2, 0, MLDSA_K,
-                 array_abs_bound(v0->vec[k2].coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)))
-);
-#endif /* !MLD_CONFIG_NO_SIGN_API */
-
-#if !defined(MLD_CONFIG_NO_SIGN_API)
-#define mld_polyveck_pack_w1 MLD_NAMESPACE_KL(polyveck_pack_w1)
-/**
- * Bit-pack polynomial vector w1 with coefficients in [0, 15] or [0, 43]. Input
- * coefficients are assumed to be standard representatives.
- *
- * @spec{Implements @[FIPS204, Algorithm 28, w1Encode].}
- *
- * @param[out] r  Pointer to output byte array with at least
- *                MLDSA_K * MLDSA_POLYW1_PACKEDBYTES bytes.
- * @param[in]  w1 Pointer to input polynomial vector.
- */
-MLD_INTERNAL_API
-void mld_polyveck_pack_w1(uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
-                          const mld_polyveck *w1)
-__contract__(
-  requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
-  requires(memory_no_alias(w1, sizeof(mld_polyveck)))
-  requires(forall(k1, 0, MLDSA_K,
-    array_bound(w1->vec[k1].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))))
-  assigns(memory_slice(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
+    array_abs_bound(v0->vec[k1].coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1)))
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
diff --git a/mldsa/src/polyvec_lazy.c b/mldsa/src/polyvec_lazy.c
index d85761ea03..379a43736f 100644
--- a/mldsa/src/polyvec_lazy.c
+++ b/mldsa/src/polyvec_lazy.c
@@ -157,10 +157,9 @@ void mld_polyvec_matrix_pointwise_montgomery_row_eager(mld_poly *t_row,
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)
 MLD_INTERNAL_API
-void mld_polyvec_matrix_pointwise_montgomery_yvec_eager(mld_polyveck *w,
-                                                        mld_polymat_eager *mat,
-                                                        const mld_yvec_eager *y,
-                                                        mld_polyvecl *scratch)
+void mld_polyvec_matrix_pointwise_montgomery_yvec_eager(
+    mld_polyveck *w, mld_polymat_eager *mat, const mld_yvec_eager *y,
+    mld_yvec_scratch_eager *scratch)
 {
   unsigned int i;
   *scratch = y->vec;
@@ -231,18 +230,12 @@ void mld_polyvec_matrix_pointwise_montgomery_row_lazy(mld_poly *t_row,
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)
 MLD_INTERNAL_API
-void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w,
-                                                       mld_polymat_lazy *mat,
-                                                       const mld_yvec_lazy *y,
-                                                       mld_polyvecl *scratch)
+void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(
+    mld_polyveck *w, mld_polymat_lazy *mat, const mld_yvec_lazy *y,
+    mld_yvec_scratch_lazy *scratch)
 {
   unsigned int k, l;
   MLD_ALIGN uint8_t seed_ext[MLD_ALIGN_UP(MLDSA_SEEDBYTES + 2)];
-  /* Only the first poly of the polyvecl scratch is used. The polyvecl type
-   * matches the eager variant for API uniformity; in REDUCE_RAM mode the
-   * polyvecl storage is provided "for free" by the caller's polyveck/polyvecl
-   * union. */
-  mld_poly *y_ntt = &scratch->vec[0];
 
   mld_memcpy(seed_ext, mat->rho, MLDSA_SEEDBYTES);
 
@@ -252,7 +245,7 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w,
     assigns(k, l, object_whole(seed_ext),
             memory_slice(w, sizeof(mld_polyveck)),
             memory_slice(mat, sizeof(mld_polymat_lazy)),
-            memory_slice(scratch, sizeof(mld_polyvecl)))
+            memory_slice(scratch, sizeof(mld_yvec_scratch_lazy)))
     invariant(l <= MLDSA_L)
     invariant(l == 0 ||
               forall(k0, 0, MLDSA_K,
@@ -261,8 +254,8 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w,
     decreases(MLDSA_L - l)
   )
   {
-    mld_yvec_get_poly_lazy(y_ntt, y, l);
-    mld_poly_ntt(y_ntt);
+    mld_yvec_get_poly_lazy(scratch, y, l);
+    mld_poly_ntt(scratch);
     for (k = 0; k < MLDSA_K; k++)
     __loop__(
       assigns(k, object_whole(seed_ext),
@@ -286,12 +279,12 @@ void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w,
       if (l == 0)
       {
         mld_polymat_expand_entry(&w->vec[k], seed_ext, 0, (uint8_t)k);
-        mld_poly_pointwise_montgomery(&w->vec[k], y_ntt);
+        mld_poly_pointwise_montgomery(&w->vec[k], scratch);
       }
       else
       {
         mld_polymat_expand_entry(&mat->cur, seed_ext, (uint8_t)l, (uint8_t)k);
-        mld_poly_pointwise_montgomery(&mat->cur, y_ntt);
+        mld_poly_pointwise_montgomery(&mat->cur, scratch);
         mld_poly_add(&w->vec[k], &mat->cur);
       }
     }
diff --git a/mldsa/src/polyvec_lazy.h b/mldsa/src/polyvec_lazy.h
index baecdb8226..1f18808f15 100644
--- a/mldsa/src/polyvec_lazy.h
+++ b/mldsa/src/polyvec_lazy.h
@@ -79,6 +79,9 @@
 #define mld_yvec_eager MLD_ADD_PARAM_SET(mld_yvec_eager)
 #define mld_yvec_lazy MLD_ADD_PARAM_SET(mld_yvec_lazy)
 #define mld_yvec MLD_ADD_PARAM_SET(mld_yvec)
+#define mld_yvec_scratch MLD_ADD_PARAM_SET(mld_yvec_scratch)
+#define mld_yvec_scratch_eager MLD_ADD_PARAM_SET(mld_yvec_scratch_eager)
+#define mld_yvec_scratch_lazy MLD_ADD_PARAM_SET(mld_yvec_scratch_lazy)
 #define mld_yvec_init_eager MLD_ADD_PARAM_SET(mld_yvec_init_eager)
 #define mld_yvec_init_lazy MLD_ADD_PARAM_SET(mld_yvec_init_lazy)
 #define mld_yvec_get_poly_eager MLD_ADD_PARAM_SET(mld_yvec_get_poly_eager)
@@ -127,6 +130,9 @@ typedef struct
   mld_polyvecl vec; /**< Masking vector y. */
 } mld_yvec_eager;
 
+/** Scratch for the eager matrix-vector product: holds NTT(y) in full. */
+typedef mld_polyvecl mld_yvec_scratch_eager;
+
 /** Lazy yvec: store seed and base counter kappa, regenerate y[i] on demand. */
 typedef struct
 {
@@ -134,6 +140,9 @@ typedef struct
   uint16_t kappa;          /**< Base counter; component i uses kappa + i. */
 } mld_yvec_lazy;
 
+/** Scratch for the lazy matrix-vector product: holds one column of y. */
+typedef mld_poly mld_yvec_scratch_lazy;
+
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_SIGN_API)
 /* s1vec */
 
@@ -502,21 +511,20 @@ __contract__(
  * @param[out] scratch Scratch polyvecl for NTT'd copy of y.
  */
 MLD_INTERNAL_API
-void mld_polyvec_matrix_pointwise_montgomery_yvec_eager(mld_polyveck *w,
-                                                        mld_polymat_eager *mat,
-                                                        const mld_yvec_eager *y,
-                                                        mld_polyvecl *scratch)
+void mld_polyvec_matrix_pointwise_montgomery_yvec_eager(
+    mld_polyveck *w, mld_polymat_eager *mat, const mld_yvec_eager *y,
+    mld_yvec_scratch_eager *scratch)
 __contract__(
   requires(memory_no_alias(w, sizeof(mld_polyveck)))
   requires(memory_no_alias(mat, sizeof(mld_polymat_eager)))
   requires(memory_no_alias(y, sizeof(mld_yvec_eager)))
-  requires(memory_no_alias(scratch, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(scratch, sizeof(mld_yvec_scratch_eager)))
   requires(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
     array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
   requires(forall(l2, 0, MLDSA_L,
     array_bound(y->vec.vec[l2].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
   assigns(memory_slice(w, sizeof(mld_polyveck)))
-  assigns(memory_slice(scratch, sizeof(mld_polyvecl)))
+  assigns(memory_slice(scratch, sizeof(mld_yvec_scratch_eager)))
   ensures(forall(k0, 0, MLDSA_K,
     array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND)))
 );
@@ -569,33 +577,29 @@ __contract__(
 /**
  * Compute w = invNTT(A * NTT(y)) for the signing y vector.
  *
- * The lazy variant samples one column of y at a time, NTTs it into
- * &scratch->vec[0], and accumulates the matrix-vector product
- * column-by-column with on-demand sampling of A[k][l]. Only the first poly of
- * the polyvecl scratch is used; the polyvecl type is shared with the eager
- * variant for API uniformity (the storage is provided "for free" by the
- * caller's polyveck/polyvecl union in REDUCE_RAM mode).
+ * The lazy variant samples one column of y at a time, NTTs it into scratch, and
+ * accumulates the matrix-vector product column-by-column with on-demand
+ * sampling of A[k][l].
  *
  * @param[out]    w       Pointer to output vector.
  * @param[in,out] mat     Pointer to input matrix.
  * @param[in]     y       Pointer to y seed/kappa.
- * @param[out]    scratch Scratch (only &scratch->vec[0] used).
+ * @param[out]    scratch Scratch for the NTT of the current column of y.
  */
 MLD_INTERNAL_API
-void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(mld_polyveck *w,
-                                                       mld_polymat_lazy *mat,
-                                                       const mld_yvec_lazy *y,
-                                                       mld_polyvecl *scratch)
+void mld_polyvec_matrix_pointwise_montgomery_yvec_lazy(
+    mld_polyveck *w, mld_polymat_lazy *mat, const mld_yvec_lazy *y,
+    mld_yvec_scratch_lazy *scratch)
 __contract__(
   requires(memory_no_alias(w, sizeof(mld_polyveck)))
   requires(memory_no_alias(mat, sizeof(mld_polymat_lazy)))
   requires(memory_no_alias(y, sizeof(mld_yvec_lazy)))
-  requires(memory_no_alias(scratch, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(scratch, sizeof(mld_yvec_scratch_lazy)))
   requires(memory_no_alias(y->rhoprime, MLDSA_CRHBYTES))
   requires(y->kappa <= MLD_MAX_KAPPA)
   assigns(memory_slice(w, sizeof(mld_polyveck)))
   assigns(memory_slice(mat, sizeof(mld_polymat_lazy)))
-  assigns(memory_slice(scratch, sizeof(mld_polyvecl)))
+  assigns(memory_slice(scratch, sizeof(mld_yvec_scratch_lazy)))
   ensures(forall(k0, 0, MLDSA_K,
     array_abs_bound(w->vec[k0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND)))
 );
@@ -609,6 +613,7 @@ typedef mld_sk_s2hat_lazy mld_sk_s2hat;
 typedef mld_sk_t0hat_lazy mld_sk_t0hat;
 typedef mld_polymat_lazy mld_polymat;
 typedef mld_yvec_lazy mld_yvec;
+typedef mld_yvec_scratch_lazy mld_yvec_scratch;
 #define mld_unpack_sk_s1hat mld_unpack_sk_s1hat_lazy
 #define mld_unpack_sk_s2hat mld_unpack_sk_s2hat_lazy
 #define mld_unpack_sk_t0hat mld_unpack_sk_t0hat_lazy
@@ -630,6 +635,7 @@ typedef mld_sk_s2hat_eager mld_sk_s2hat;
 typedef mld_sk_t0hat_eager mld_sk_t0hat;
 typedef mld_polymat_eager mld_polymat;
 typedef mld_yvec_eager mld_yvec;
+typedef mld_yvec_scratch_eager mld_yvec_scratch;
 #define mld_unpack_sk_s1hat mld_unpack_sk_s1hat_eager
 #define mld_unpack_sk_s2hat mld_unpack_sk_s2hat_eager
 #define mld_unpack_sk_t0hat mld_unpack_sk_t0hat_eager
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index c7e8367f6b..45ad005221 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -6,6 +6,11 @@
 /* References
  * ==========
  *
+ * - [DilithiumMemory]
+ *   Dilithium for Memory Constrained Devices
+ *   Bos, Renes, Sprenkels
+ *   https://eprint.iacr.org/2022/323
+ *
  * - [FIPS140_3_IG]
  *   Implementation Guidance for FIPS 140-3 and the Cryptographic Module
  *   Validation Program
@@ -731,28 +736,28 @@ __contract__(
 
   typedef union
   {
-    mld_polyveck w1;
-    mld_polyvecl tmp;
-  } w1tmp_u;
-  mld_polyveck *w1;
-  mld_polyvecl *tmp;
+    mld_yvec_scratch y;
+    mld_poly w;
+  } scratch_u;
+  mld_yvec_scratch *scratch_yvec;
+  mld_poly *scratch_w;
 
   MLD_ALLOC(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES, context);
   MLD_ALLOC(y, mld_yvec, 1, context);
-  MLD_ALLOC(z, mld_poly, 1, context);
-  MLD_ALLOC(w1tmp, w1tmp_u, 1, context);
+  MLD_ALLOC(scratch, scratch_u, 1, context);
+  MLD_ALLOC(w1_packed, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context);
   MLD_ALLOC(w0, mld_polyveck, 1, context);
   MLD_ALLOC(cp, mld_poly, 1, context);
   MLD_ALLOC(t, mld_poly, 1, context);
 
-  if (challenge_bytes == NULL || y == NULL || z == NULL || w1tmp == NULL ||
-      w0 == NULL || cp == NULL || t == NULL)
+  if (challenge_bytes == NULL || y == NULL || scratch == NULL ||
+      w1_packed == NULL || w0 == NULL || cp == NULL || t == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
-  w1 = &w1tmp->w1;
-  tmp = &w1tmp->tmp;
+  scratch_yvec = &scratch->y;
+  scratch_w = &scratch->w;
 
   /* @[FIPS204, Algorithm 7, line 11] y <- ExpandMask(rhoprime, kappa). */
   mld_yvec_init(y, rhoprime, kappa);
@@ -761,20 +766,19 @@ __contract__(
    * performs the whole line: it NTTs y, accumulates the pointwise product with
    * A_hat, and applies the inverse NTT. In REDUCE_RAM mode the y sampling is
    * fused into the same pass. */
-  mld_polyvec_matrix_pointwise_montgomery_yvec(w0, mat, y, tmp);
+  mld_polyvec_matrix_pointwise_montgomery_yvec(w0, mat, y, scratch_yvec);
 
   /* @[FIPS204, Algorithm 7, line 13] w1 <- HighBits(w), here together with the
-   * low part: Decompose yields w = 2*GAMMA2*w1 + w0, keeping both w1 and w0
-   * (w0 is reused below in the line-21/26 alternative, see further down). */
+   * low part: Decompose yields w = 2*GAMMA2*w1 + w0. w0 is kept in full for
+   * the line-21/26 alternative below; w1 is kept only in its w1Encode form,
+   * from which the hint computation decodes single rows on demand. Keeping w1
+   * packed for the whole signing attempt is also done in @[DilithiumMemory]. */
   mld_polyveck_caddq(w0);
-  mld_polyveck_decompose(w1, w0);
-
-  /* @[FIPS204, Algorithm 7, line 15] ctilde <- H(mu || w1Encode(w1), lambda/4).
-   * w1Encode(w1) is packed into the w1 region of sig (mld_polyveck_pack_w1),
-   * then absorbed by H together with mu. */
-  mld_polyveck_pack_w1(sig, w1);
+  mld_polyveck_decompose_pack_w1(w1_packed, w0, scratch_w);
 
-  mld_H(challenge_bytes, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, sig,
+  /* @[FIPS204, Algorithm 7, line 15] ctilde <- H(mu || w1Encode(w1),
+   * lambda/4). */
+  mld_H(challenge_bytes, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, w1_packed,
         MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
   /* Constant time: Leaking challenge_bytes does not reveal any information
    * about the secret key as H() is modelled as random oracle.
@@ -790,7 +794,7 @@ __contract__(
    * z <- y + cs1, followed by the line-23 norm check ||z||_inf >= GAMMA1 -
    * BETA. mld_compute_pack_z fuses all three per polynomial and, on success,
    * packs z into sig; it returns MLD_ERR_FAIL if the norm check rejects z. */
-  ret = mld_compute_pack_z(sig, cp, s1hat, y, t, z);
+  ret = mld_compute_pack_z(sig, cp, s1hat, y, t, scratch_w);
   if (ret != 0)
   {
     goto cleanup;
@@ -803,9 +807,9 @@ __contract__(
    * computation of h may instead be implemented "as described in Section 5.1 of
    * [6]", and that reference is @[Round3_Spec, Section 5.1].
    *
-   * The loop below builds w0 - cs2 + ct0 in place in w0; w1 is unmodified, and
-   * is HighBits(w) from line 13. Those are the inputs to the streamlined
-   * computation of MakeHint explained below.
+   * The loop below builds w0 - cs2 + ct0 in place in w0; w1_packed is
+   * unmodified, and holds w1Encode(HighBits(w)) from line 13. Those are the
+   * inputs to the streamlined computation of MakeHint explained below.
    *
    * Low-bits norm check:
    *   @[FIPS204, Algorithm 7, line 21] computes r0 = LowBits(w - cs2) and line
@@ -825,16 +829,16 @@ __contract__(
    *   (-GAMMA2, GAMMA2], or equals -GAMMA2 while the matching w1 coefficient is
    *   zero (the Decompose border case), and is set otherwise. This equivalence
    *   is precisely what mld_pack_sig_h -> mld_make_hint compute from w0
-   *   (= w0 - cs2 + ct0) and w1. The line-28 ||ct0||_inf >= GAMMA2 check is the
-   *   mld_poly_chknorm(z, GAMMA2) call on ct0 below; the weight bound is
-   *   enforced by mld_pack_sig_h.
+   *   (= w0 - cs2 + ct0) and the w1 row decoded from w1_packed. The line-28
+   *   ||ct0||_inf >= GAMMA2 check is the mld_poly_chknorm(scratch_w, GAMMA2)
+   *   call on ct0 below; the weight bound is enforced by mld_pack_sig_h.
    *
    * Building w0 per-component and checking norms incrementally also avoids
    * allocating a full polyveck for h. */
   for (k = 0; k < MLDSA_K; k++)
   __loop__(
     assigns(k,
-            object_whole(z),
+            object_whole(scratch_w),
             object_whole(w0))
     invariant(k <= MLDSA_K)
     invariant(forall(k0, k, MLDSA_K,
@@ -844,11 +848,11 @@ __contract__(
   {
     /* @[FIPS204, Algorithm 7, line 19] cs2[k] <- invNTT(c_hat o s2_hat)[k],
      * then subtract from w0[k] to form (w0 - cs2)[k]. */
-    mld_sk_s2hat_get_poly(z, s2hat, k);
-    mld_poly_pointwise_montgomery(z, cp);
-    mld_poly_invntt_tomont(z);
+    mld_sk_s2hat_get_poly(scratch_w, s2hat, k);
+    mld_poly_pointwise_montgomery(scratch_w, cp);
+    mld_poly_invntt_tomont(scratch_w);
 
-    mld_poly_sub(&w0->vec[k], z);
+    mld_poly_sub(&w0->vec[k], scratch_w);
     mld_poly_reduce(&w0->vec[k]);
 
     /* Low-bits norm check (see block comment above): the line-23 check on
@@ -863,14 +867,14 @@ __contract__(
     }
 
     /* @[FIPS204, Algorithm 7, line 25] ct0[k] <- invNTT(c_hat o t0_hat)[k]. */
-    mld_sk_t0hat_get_poly(z, t0hat, k);
-    mld_poly_pointwise_montgomery(z, cp);
-    mld_poly_invntt_tomont(z);
-    mld_poly_reduce(z);
+    mld_sk_t0hat_get_poly(scratch_w, t0hat, k);
+    mld_poly_pointwise_montgomery(scratch_w, cp);
+    mld_poly_invntt_tomont(scratch_w);
+    mld_poly_reduce(scratch_w);
 
     /* @[FIPS204, Algorithm 7, line 28] reject when ||ct0||_inf >= GAMMA2 (the
      * second part, the OMEGA weight bound, is enforced by mld_pack_sig_h). */
-    h_invalid = mld_poly_chknorm(z, MLDSA_GAMMA2);
+    h_invalid = mld_poly_chknorm(scratch_w, MLDSA_GAMMA2);
     /* Constant time: h_invalid may be leaked - see comment for z_invalid. */
     MLD_CT_TESTING_DECLASSIFY(&h_invalid, sizeof(uint32_t));
     if (h_invalid)
@@ -881,7 +885,7 @@ __contract__(
 
     /* Add ct0[k] to (w0 - cs2)[k], leaving (w0 - cs2 + ct0)[k] in w0[k] -- the
      * MakeHint input prepared for mld_pack_sig_h (see block comment above). */
-    mld_poly_add(&w0->vec[k], z);
+    mld_poly_add(&w0->vec[k], scratch_w);
   }
 
   /* Constant time: At this point all norm checks have passed and we, hence,
@@ -895,7 +899,7 @@ __contract__(
    * (see @[FIPS204, Section 6.1]).
    */
   MLD_CT_TESTING_DECLASSIFY(w0, sizeof(*w0));
-  MLD_CT_TESTING_DECLASSIFY(w1, sizeof(*w1));
+  MLD_CT_TESTING_DECLASSIFY(w1_packed, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES);
 
   /* @[FIPS204, Algorithm 7, line 33] sigEncode(ctilde, z mod+/- q, h) is split
    * across three calls: z was already packed by mld_compute_pack_z, this call
@@ -904,10 +908,11 @@ __contract__(
 
   /* @[FIPS204, Algorithm 7, line 26] h <- MakeHint(-ct0, w - cs2 + ct0),
    * computed from (w0 = w0 - cs2 + ct0, w1) as described in the block comment
-   * above, and packed as the h component of the line-33 sigEncode. Returns
-   * MLD_ERR_FAIL if h would exceed OMEGA nonzero coefficients (the remaining
-   * part of the line-28 check), in which case we reject. */
-  ret = mld_pack_sig_h(sig, w0, w1);
+   * above, and packed as the h component of the line-33 sigEncode. w1 is
+   * recovered from its encoding one polynomial at a time into scratch_w.
+   * Returns MLD_ERR_FAIL if h would exceed OMEGA nonzero coefficients (the
+   * remaining part of the line-28 check), in which case we reject. */
+  ret = mld_pack_sig_h(sig, w0, w1_packed, scratch_w);
   if (ret != 0)
   {
     goto cleanup;
@@ -923,8 +928,8 @@ __contract__(
   MLD_FREE(t, mld_poly, 1, context);
   MLD_FREE(cp, mld_poly, 1, context);
   MLD_FREE(w0, mld_polyveck, 1, context);
-  MLD_FREE(w1tmp, w1tmp_u, 1, context);
-  MLD_FREE(z, mld_poly, 1, context);
+  MLD_FREE(w1_packed, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context);
+  MLD_FREE(scratch, scratch_u, 1, context);
   MLD_FREE(y, mld_yvec, 1, context);
   MLD_FREE(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES, context);
 
diff --git a/proofs/cbmc/attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile
index 2829e198b2..9923bd0348 100644
--- a/proofs/cbmc/attempt_signature_generation/Makefile
+++ b/proofs/cbmc/attempt_signature_generation/Makefile
@@ -25,8 +25,7 @@ USE_FUNCTION_CONTRACTS+=mld_sk_s2hat_get_poly
 USE_FUNCTION_CONTRACTS+=mld_sk_t0hat_get_poly
 USE_FUNCTION_CONTRACTS+=mld_yvec_init
 USE_FUNCTION_CONTRACTS+=mld_polyveck_caddq
-USE_FUNCTION_CONTRACTS+=mld_polyveck_decompose
-USE_FUNCTION_CONTRACTS+=mld_polyveck_pack_w1
+USE_FUNCTION_CONTRACTS+=mld_polyveck_decompose_pack_w1
 USE_FUNCTION_CONTRACTS+=mld_H
 USE_FUNCTION_CONTRACTS+=mld_poly_challenge
 USE_FUNCTION_CONTRACTS+=mld_poly_ntt
diff --git a/proofs/cbmc/pack_sig_h/Makefile b/proofs/cbmc/pack_sig_h/Makefile
index e16e14641d..d7b5d69b9c 100644
--- a/proofs/cbmc/pack_sig_h/Makefile
+++ b/proofs/cbmc/pack_sig_h/Makefile
@@ -21,6 +21,7 @@ PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
 
 CHECK_FUNCTION_CONTRACTS=mld_pack_sig_h
 USE_FUNCTION_CONTRACTS=mld_make_hint
+USE_FUNCTION_CONTRACTS+=mld_polyw1_unpack
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
diff --git a/proofs/cbmc/pack_sig_h/pack_sig_h_harness.c b/proofs/cbmc/pack_sig_h/pack_sig_h_harness.c
index ddc4247f4c..9d96427913 100644
--- a/proofs/cbmc/pack_sig_h/pack_sig_h_harness.c
+++ b/proofs/cbmc/pack_sig_h/pack_sig_h_harness.c
@@ -6,7 +6,9 @@
 void harness(void)
 {
   uint8_t *sig;
-  mld_polyveck *w0, *w1;
+  mld_polyveck *w0;
+  uint8_t *w1_packed;
+  mld_poly *scratch;
   int r;
-  r = mld_pack_sig_h(sig, w0, w1);
+  r = mld_pack_sig_h(sig, w0, w1_packed, scratch);
 }
diff --git a/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/Makefile b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/Makefile
index f84c1cd01c..247e709173 100644
--- a/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/Makefile
+++ b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/Makefile
@@ -50,7 +50,11 @@ FUNCTION_NAME = polyvec_matrix_pointwise_montgomery_yvec
 # EXPENSIVE = true
 
 # This function is large enough to need...
+ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
+CBMC_OBJECT_BITS = 11
+else
 CBMC_OBJECT_BITS = 10
+endif
 
 # 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
diff --git a/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/polyvec_matrix_pointwise_montgomery_yvec_harness.c b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/polyvec_matrix_pointwise_montgomery_yvec_harness.c
index 23790814c4..b21af01f8c 100644
--- a/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/polyvec_matrix_pointwise_montgomery_yvec_harness.c
+++ b/proofs/cbmc/polyvec_matrix_pointwise_montgomery_yvec/polyvec_matrix_pointwise_montgomery_yvec_harness.c
@@ -8,6 +8,6 @@ void harness(void)
   mld_polyveck *w;
   mld_polymat *mat;
   mld_yvec *y;
-  mld_polyvecl *scratch;
+  mld_yvec_scratch *scratch;
   mld_polyvec_matrix_pointwise_montgomery_yvec(w, mat, y, scratch);
 }
diff --git a/proofs/cbmc/polyveck_decompose/Makefile b/proofs/cbmc/polyveck_decompose_pack_w1/Makefile
similarity index 89%
rename from proofs/cbmc/polyveck_decompose/Makefile
rename to proofs/cbmc/polyveck_decompose_pack_w1/Makefile
index 7500d68079..ee5d5ea125 100644
--- a/proofs/cbmc/polyveck_decompose/Makefile
+++ b/proofs/cbmc/polyveck_decompose_pack_w1/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = polyveck_decompose_harness
+HARNESS_FILE = polyveck_decompose_pack_w1_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 = polyveck_decompose
+PROOF_UID = polyveck_decompose_pack_w1
 
 DEFINES +=
 INCLUDES +=
@@ -19,8 +19,9 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
 
-CHECK_FUNCTION_CONTRACTS=mld_polyveck_decompose
+CHECK_FUNCTION_CONTRACTS=mld_polyveck_decompose_pack_w1
 USE_FUNCTION_CONTRACTS=mld_poly_decompose
+USE_FUNCTION_CONTRACTS+=mld_polyw1_pack
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
@@ -28,7 +29,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = polyveck_decompose
+FUNCTION_NAME = polyveck_decompose_pack_w1
 
 # 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
diff --git a/proofs/cbmc/polyveck_pack_w1/polyveck_pack_w1_harness.c b/proofs/cbmc/polyveck_decompose_pack_w1/polyveck_decompose_pack_w1_harness.c
similarity index 58%
rename from proofs/cbmc/polyveck_pack_w1/polyveck_pack_w1_harness.c
rename to proofs/cbmc/polyveck_decompose_pack_w1/polyveck_decompose_pack_w1_harness.c
index e2ade71a5a..6f78d0a75f 100644
--- a/proofs/cbmc/polyveck_pack_w1/polyveck_pack_w1_harness.c
+++ b/proofs/cbmc/polyveck_decompose_pack_w1/polyveck_decompose_pack_w1_harness.c
@@ -5,7 +5,8 @@
 
 void harness(void)
 {
-  mld_polyveck *a;
-  uint8_t *b;
-  mld_polyveck_pack_w1(b, a);
+  uint8_t *r;
+  mld_polyveck *v0;
+  mld_poly *scratch;
+  mld_polyveck_decompose_pack_w1(r, v0, scratch);
 }
diff --git a/proofs/cbmc/polyveck_pack_w1/Makefile b/proofs/cbmc/polyw1_unpack/Makefile
similarity index 83%
rename from proofs/cbmc/polyveck_pack_w1/Makefile
rename to proofs/cbmc/polyw1_unpack/Makefile
index 0dff07c42a..3d00190f66 100644
--- a/proofs/cbmc/polyveck_pack_w1/Makefile
+++ b/proofs/cbmc/polyw1_unpack/Makefile
@@ -4,22 +4,27 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = polyveck_pack_w1_harness
+HARNESS_FILE = polyw1_unpack_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 = polyveck_pack_w1
+PROOF_UID = polyw1_unpack
 
 DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
-
-CHECK_FUNCTION_CONTRACTS=mld_polyveck_pack_w1
-USE_FUNCTION_CONTRACTS=mld_polyw1_pack
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
+
+CHECK_FUNCTION_CONTRACTS=mld_polyw1_unpack
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+USE_FUNCTION_CONTRACTS=mld_polyw1_unpack_88
+else
+USE_FUNCTION_CONTRACTS=mld_polyw1_unpack_32
+endif
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
@@ -27,7 +32,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = polyveck_pack_w1
+FUNCTION_NAME = polyw1_unpack
 
 # 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
@@ -36,7 +41,7 @@ FUNCTION_NAME = polyveck_pack_w1
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 9
+CBMC_OBJECT_BITS = 8
 
 # 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
diff --git a/proofs/cbmc/polyveck_decompose/polyveck_decompose_harness.c b/proofs/cbmc/polyw1_unpack/polyw1_unpack_harness.c
similarity index 61%
rename from proofs/cbmc/polyveck_decompose/polyveck_decompose_harness.c
rename to proofs/cbmc/polyw1_unpack/polyw1_unpack_harness.c
index 68215df3a6..d1d88e4e68 100644
--- a/proofs/cbmc/polyveck_decompose/polyveck_decompose_harness.c
+++ b/proofs/cbmc/polyw1_unpack/polyw1_unpack_harness.c
@@ -1,10 +1,11 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "polyvec.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
-  mld_polyveck *a0, *a1;
-  mld_polyveck_decompose(a1, a0);
+  mld_poly *r;
+  uint8_t *a;
+  mld_polyw1_unpack(r, a);
 }
diff --git a/proofs/cbmc/polyw1_unpack_32/Makefile b/proofs/cbmc/polyw1_unpack_32/Makefile
new file mode 100644
index 0000000000..9f5567588d
--- /dev/null
+++ b/proofs/cbmc/polyw1_unpack_32/Makefile
@@ -0,0 +1,40 @@
+# 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 = polyw1_unpack_32_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 = polyw1_unpack_32
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
+
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+CHECK_FUNCTION_CONTRACTS=
+else
+CHECK_FUNCTION_CONTRACTS=mld_polyw1_unpack_32
+endif
+USE_FUNCTION_CONTRACTS=
+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
+
+FUNCTION_NAME = polyw1_unpack_32
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+include ../Makefile.common
diff --git a/proofs/cbmc/polyw1_unpack_32/polyw1_unpack_32_harness.c b/proofs/cbmc/polyw1_unpack_32/polyw1_unpack_32_harness.c
new file mode 100644
index 0000000000..c8bfae999c
--- /dev/null
+++ b/proofs/cbmc/polyw1_unpack_32/polyw1_unpack_32_harness.c
@@ -0,0 +1,13 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "poly.h"
+
+void harness(void)
+{
+#if MLD_CONFIG_PARAMETER_SET != 44
+  mld_poly *r;
+  uint8_t *a;
+  mld_polyw1_unpack_32(r, a);
+#endif
+}
diff --git a/proofs/cbmc/polyw1_unpack_88/Makefile b/proofs/cbmc/polyw1_unpack_88/Makefile
new file mode 100644
index 0000000000..afed3e41e3
--- /dev/null
+++ b/proofs/cbmc/polyw1_unpack_88/Makefile
@@ -0,0 +1,40 @@
+# 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 = polyw1_unpack_88_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 = polyw1_unpack_88
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly.c
+
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+CHECK_FUNCTION_CONTRACTS=mld_polyw1_unpack_88
+else
+CHECK_FUNCTION_CONTRACTS=
+endif
+USE_FUNCTION_CONTRACTS=
+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
+
+FUNCTION_NAME = polyw1_unpack_88
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+include ../Makefile.common
diff --git a/proofs/cbmc/polyw1_unpack_88/polyw1_unpack_88_harness.c b/proofs/cbmc/polyw1_unpack_88/polyw1_unpack_88_harness.c
new file mode 100644
index 0000000000..cff890c0fa
--- /dev/null
+++ b/proofs/cbmc/polyw1_unpack_88/polyw1_unpack_88_harness.c
@@ -0,0 +1,13 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include "poly.h"
+
+void harness(void)
+{
+#if MLD_CONFIG_PARAMETER_SET == 44
+  mld_poly *r;
+  uint8_t *a;
+  mld_polyw1_unpack_88(r, a);
+#endif
+}
diff --git a/proofs/cbmc/sign_verify_internal/Makefile b/proofs/cbmc/sign_verify_internal/Makefile
index 8af8698cd9..d810baf03b 100644
--- a/proofs/cbmc/sign_verify_internal/Makefile
+++ b/proofs/cbmc/sign_verify_internal/Makefile
@@ -60,7 +60,7 @@ FUNCTION_NAME = sign_verify_internal
 ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
 CBMC_OBJECT_BITS = 12
 else
-CBMC_OBJECT_BITS = 11
+CBMC_OBJECT_BITS = 10
 endif
 
 # If you require access to a file-local ("static") function or object to conduct
diff --git a/test/src/test_unit.c b/test/src/test_unit.c
index 87d3dbc2b4..f4f1d4c3da 100644
--- a/test/src/test_unit.c
+++ b/test/src/test_unit.c
@@ -1245,8 +1245,8 @@ static int test_polyvec_lazy_eager(void)
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
   MLD_ALLOC(v, mld_polyvecl, 1, NULL);
 #endif
-  MLD_ALLOC(scratch_eager, mld_polyvecl, 1, NULL);
-  MLD_ALLOC(scratch_lazy, mld_polyvecl, 1, NULL);
+  MLD_ALLOC(scratch_eager, mld_yvec_scratch_eager, 1, NULL);
+  MLD_ALLOC(scratch_lazy, mld_yvec_scratch_lazy, 1, NULL);
   MLD_ALLOC(w_eager, mld_polyveck, 1, NULL);
   MLD_ALLOC(w_lazy, mld_polyveck, 1, NULL);
 
@@ -1376,8 +1376,8 @@ static int test_polyvec_lazy_eager(void)
 cleanup:
   MLD_FREE(w_lazy, mld_polyveck, 1, NULL);
   MLD_FREE(w_eager, mld_polyveck, 1, NULL);
-  MLD_FREE(scratch_lazy, mld_polyvecl, 1, NULL);
-  MLD_FREE(scratch_eager, mld_polyvecl, 1, NULL);
+  MLD_FREE(scratch_lazy, mld_yvec_scratch_lazy, 1, NULL);
+  MLD_FREE(scratch_eager, mld_yvec_scratch_eager, 1, NULL);
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
   MLD_FREE(v, mld_polyvecl, 1, NULL);
 #endif