diff --git a/BIBLIOGRAPHY.md b/BIBLIOGRAPHY.md
index 993ab6a91..1c362d41b 100644
--- a/BIBLIOGRAPHY.md
+++ b/BIBLIOGRAPHY.md
@@ -48,8 +48,8 @@ source code and documentation.
 * Referenced from:
   - [README.md](README.md)
   - [examples/bring_your_own_fips202/mldsa_native/mldsa_native.h](examples/bring_your_own_fips202/mldsa_native/mldsa_native.h)
-  - [examples/bring_your_own_fips202/mldsa_native/src/common.h](examples/bring_your_own_fips202/mldsa_native/src/common.h)
   - [examples/bring_your_own_fips202/mldsa_native/src/config.h](examples/bring_your_own_fips202/mldsa_native/src/config.h)
+  - [examples/bring_your_own_fips202/mldsa_native/src/ct.h](examples/bring_your_own_fips202/mldsa_native/src/ct.h)
   - [examples/bring_your_own_fips202/mldsa_native/src/ntt.h](examples/bring_your_own_fips202/mldsa_native/src/ntt.h)
   - [examples/bring_your_own_fips202/mldsa_native/src/poly.c](examples/bring_your_own_fips202/mldsa_native/src/poly.c)
   - [examples/bring_your_own_fips202/mldsa_native/src/poly_kl.c](examples/bring_your_own_fips202/mldsa_native/src/poly_kl.c)
@@ -58,8 +58,8 @@ source code and documentation.
   - [examples/bring_your_own_fips202/mldsa_native/src/sign.c](examples/bring_your_own_fips202/mldsa_native/src/sign.c)
   - [examples/bring_your_own_fips202/mldsa_native/src/sign.h](examples/bring_your_own_fips202/mldsa_native/src/sign.h)
   - [mldsa/mldsa_native.h](mldsa/mldsa_native.h)
-  - [mldsa/src/common.h](mldsa/src/common.h)
   - [mldsa/src/config.h](mldsa/src/config.h)
+  - [mldsa/src/ct.h](mldsa/src/ct.h)
   - [mldsa/src/fips202/fips202.c](mldsa/src/fips202/fips202.c)
   - [mldsa/src/fips202/fips202x4.c](mldsa/src/fips202/fips202x4.c)
   - [mldsa/src/ntt.h](mldsa/src/ntt.h)
diff --git a/examples/bring_your_own_fips202/mldsa_native/src/poly_kl.h b/examples/bring_your_own_fips202/mldsa_native/src/poly_kl.h
new file mode 120000
index 000000000..f981ad481
--- /dev/null
+++ b/examples/bring_your_own_fips202/mldsa_native/src/poly_kl.h
@@ -0,0 +1 @@
+../../../../mldsa/src/poly_kl.h
\ No newline at end of file
diff --git a/integration/liboqs/ML-DSA-44_META.yml b/integration/liboqs/ML-DSA-44_META.yml
index 89fbf63cc..b43077bbb 100644
--- a/integration/liboqs/ML-DSA-44_META.yml
+++ b/integration/liboqs/ML-DSA-44_META.yml
@@ -31,10 +31,10 @@ implementations:
   sources: integration/liboqs/config_c.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/ntt.c mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h
-    mldsa/src/params.h mldsa/src/poly.c mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c
-    mldsa/src/polyvec.h mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h
-    mldsa/src/reduce.h mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h
-    mldsa/src/sys.h mldsa/src/zetas.inc
+    mldsa/src/params.h mldsa/src/poly.c mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h
+    mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c mldsa/src/prehash.h
+    mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h mldsa/src/sign.c
+    mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
 - name: x86_64
   version: FIPS204
   folder_name: .
@@ -47,10 +47,10 @@ implementations:
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/native/api.h mldsa/src/native/meta.h mldsa/src/ntt.c
     mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h mldsa/src/params.h mldsa/src/poly.c
-    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c
-    mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h
-    mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
-    mldsa/src/native/x86_64
+    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h mldsa/src/polyvec.c mldsa/src/polyvec.h
+    mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h
+    mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h
+    mldsa/src/zetas.inc mldsa/src/native/x86_64
   supported_platforms:
   - architecture: x86_64
     operating_systems:
@@ -72,10 +72,10 @@ implementations:
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/native/api.h mldsa/src/native/meta.h mldsa/src/ntt.c
     mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h mldsa/src/params.h mldsa/src/poly.c
-    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c
-    mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h
-    mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
-    mldsa/src/native/aarch64
+    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h mldsa/src/polyvec.c mldsa/src/polyvec.h
+    mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h
+    mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h
+    mldsa/src/zetas.inc mldsa/src/native/aarch64
   supported_platforms:
   - architecture: arm_8
     operating_systems:
diff --git a/integration/liboqs/ML-DSA-65_META.yml b/integration/liboqs/ML-DSA-65_META.yml
index 885b2b98d..7933213d3 100644
--- a/integration/liboqs/ML-DSA-65_META.yml
+++ b/integration/liboqs/ML-DSA-65_META.yml
@@ -31,10 +31,10 @@ implementations:
   sources: integration/liboqs/config_c.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/ntt.c mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h
-    mldsa/src/params.h mldsa/src/poly.c mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c
-    mldsa/src/polyvec.h mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h
-    mldsa/src/reduce.h mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h
-    mldsa/src/sys.h mldsa/src/zetas.inc
+    mldsa/src/params.h mldsa/src/poly.c mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h
+    mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c mldsa/src/prehash.h
+    mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h mldsa/src/sign.c
+    mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
 - name: x86_64
   version: FIPS204
   folder_name: .
@@ -47,10 +47,10 @@ implementations:
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/native/api.h mldsa/src/native/meta.h mldsa/src/ntt.c
     mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h mldsa/src/params.h mldsa/src/poly.c
-    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c
-    mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h
-    mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
-    mldsa/src/native/x86_64
+    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h mldsa/src/polyvec.c mldsa/src/polyvec.h
+    mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h
+    mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h
+    mldsa/src/zetas.inc mldsa/src/native/x86_64
   supported_platforms:
   - architecture: x86_64
     operating_systems:
@@ -72,10 +72,10 @@ implementations:
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/native/api.h mldsa/src/native/meta.h mldsa/src/ntt.c
     mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h mldsa/src/params.h mldsa/src/poly.c
-    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c
-    mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h
-    mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
-    mldsa/src/native/aarch64
+    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h mldsa/src/polyvec.c mldsa/src/polyvec.h
+    mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h
+    mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h
+    mldsa/src/zetas.inc mldsa/src/native/aarch64
   supported_platforms:
   - architecture: arm_8
     operating_systems:
diff --git a/integration/liboqs/ML-DSA-87_META.yml b/integration/liboqs/ML-DSA-87_META.yml
index 611c5bcc4..a9ad05fa8 100644
--- a/integration/liboqs/ML-DSA-87_META.yml
+++ b/integration/liboqs/ML-DSA-87_META.yml
@@ -31,10 +31,10 @@ implementations:
   sources: integration/liboqs/config_c.h integration/liboqs/fips202_glue.h integration/liboqs/fips202x4_glue.h
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/ntt.c mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h
-    mldsa/src/params.h mldsa/src/poly.c mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c
-    mldsa/src/polyvec.h mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h
-    mldsa/src/reduce.h mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h
-    mldsa/src/sys.h mldsa/src/zetas.inc
+    mldsa/src/params.h mldsa/src/poly.c mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h
+    mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c mldsa/src/prehash.h
+    mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h mldsa/src/sign.c
+    mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
 - name: x86_64
   version: FIPS204
   folder_name: .
@@ -47,10 +47,10 @@ implementations:
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/native/api.h mldsa/src/native/meta.h mldsa/src/ntt.c
     mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h mldsa/src/params.h mldsa/src/poly.c
-    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c
-    mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h
-    mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
-    mldsa/src/native/x86_64
+    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h mldsa/src/polyvec.c mldsa/src/polyvec.h
+    mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h
+    mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h
+    mldsa/src/zetas.inc mldsa/src/native/x86_64
   supported_platforms:
   - architecture: x86_64
     operating_systems:
@@ -71,10 +71,10 @@ implementations:
     mldsa/src/cbmc.h mldsa/src/common.h mldsa/src/ct.c mldsa/src/ct.h mldsa/src/debug.c
     mldsa/src/debug.h mldsa/src/native/api.h mldsa/src/native/meta.h mldsa/src/ntt.c
     mldsa/src/ntt.h mldsa/src/packing.c mldsa/src/packing.h mldsa/src/params.h mldsa/src/poly.c
-    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/polyvec.c mldsa/src/polyvec.h mldsa/src/prehash.c
-    mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h mldsa/src/rounding.h
-    mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h mldsa/src/zetas.inc
-    mldsa/src/native/aarch64
+    mldsa/src/poly.h mldsa/src/poly_kl.c mldsa/src/poly_kl.h mldsa/src/polyvec.c mldsa/src/polyvec.h
+    mldsa/src/prehash.c mldsa/src/prehash.h mldsa/src/randombytes.h mldsa/src/reduce.h
+    mldsa/src/rounding.h mldsa/src/sign.c mldsa/src/sign.h mldsa/src/symmetric.h mldsa/src/sys.h
+    mldsa/src/zetas.inc mldsa/src/native/aarch64
   supported_platforms:
   - architecture: arm_8
     operating_systems:
diff --git a/mldsa/src/common.h b/mldsa/src/common.h
index 9cfcf7b4c..560c3a8dd 100644
--- a/mldsa/src/common.h
+++ b/mldsa/src/common.h
@@ -3,15 +3,6 @@
  * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
  */
 
-/* References
- * ==========
- *
- * - [FIPS204]
- *   FIPS 204 Module-Lattice-Based Digital Signature Standard
- *   National Institute of Standards and Technology
- *   https://csrc.nist.gov/pubs/fips/204/final
- */
-
 #ifndef MLD_COMMON_H
 #define MLD_COMMON_H
 
@@ -104,60 +95,12 @@
  * all source files are included, even those that are not needed.
  * Those files are appropriately guarded and will be empty when unneeded.
  * The following is to avoid compilers complaining about this. */
-#define MLD_EMPTY_CU(s) extern int MLD_NAMESPACE(empty_cu_##s);
+#define MLD_EMPTY_CU(s) extern int MLD_NAMESPACE_KL(empty_cu_##s);
 
 #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202)
 #include MLD_CONFIG_FIPS202_BACKEND_FILE
 #endif
 
-#if !defined(__ASSEMBLER__)
-#include <string.h>
-
-/*************************************************
- * Name:        mld_zeroize
- *
- * Description: Force-zeroize a buffer.
- *              @[FIPS204, Section 3.6.3] Destruction of intermediate values.
- *
- * Arguments:   void *ptr: pointer to buffer to be zeroed
- *              size_t len: Amount of bytes to be zeroed
- **************************************************/
-static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
-__contract__(
-  requires(memory_no_alias(ptr, len))
-  assigns(memory_slice(ptr, len))
-);
-
-#if defined(MLD_CONFIG_CUSTOM_ZEROIZE)
-static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
-{
-  mld_zeroize_native(ptr, len);
-}
-#elif defined(MLD_SYS_WINDOWS)
-#include <windows.h>
-static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
-{
-  SecureZeroMemory(ptr, len);
-}
-#elif defined(MLD_HAVE_INLINE_ASM)
-static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
-{
-  memset(ptr, 0, len);
-  /* This follows OpenSSL and seems sufficient to prevent the compiler
-   * from optimizing away the memset.
-   *
-   * If there was a reliable way to detect availability of memset_s(),
-   * that would be preferred. */
-  __asm__ __volatile__("" : : "r"(ptr) : "memory");
-}
-#else /* !MLD_CONFIG_CUSTOM_ZEROIZE && !MLD_SYS_WINDOWS && MLD_HAVE_INLINE_ASM \
-       */
-#error No plausibly-secure implementation of mld_zeroize available. Please provide your own using MLD_CONFIG_CUSTOM_ZEROIZE.
-#endif /* !MLD_CONFIG_CUSTOM_ZEROIZE && !MLD_SYS_WINDOWS && \
-          !MLD_HAVE_INLINE_ASM */
-
-#endif /* !__ASSEMBLER__ */
-
 #if !defined(MLD_CONFIG_FIPS202_CUSTOM_HEADER)
 #define MLD_FIPS202_HEADER_FILE "fips202/fips202.h"
 #else
diff --git a/mldsa/src/ct.h b/mldsa/src/ct.h
index fd0788f6b..dc4c9b853 100644
--- a/mldsa/src/ct.h
+++ b/mldsa/src/ct.h
@@ -7,6 +7,11 @@
 /* References
  * ==========
  *
+ * - [FIPS204]
+ *   FIPS 204 Module-Lattice-Based Digital Signature Standard
+ *   National Institute of Standards and Technology
+ *   https://csrc.nist.gov/pubs/fips/204/final
+ *
  * - [libmceliece]
  *   libmceliece implementation of Classic McEliece
  *   Bernstein, Chou
@@ -232,5 +237,54 @@ __contract__(
   return mld_ct_sel_int32(-x, x, mld_ct_cmask_neg_i32(x));
 }
 
+#if !defined(__ASSEMBLER__)
+#include <string.h>
+
+/*************************************************
+ * Name:        mld_zeroize
+ *
+ * Description: Force-zeroize a buffer.
+ *              @[FIPS204, Section 3.6.3] Destruction of intermediate
+ *values.
+ *
+ * Arguments:   void *ptr: pointer to buffer to be zeroed
+ *              size_t len: Amount of bytes to be zeroed
+ **************************************************/
+static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
+__contract__(
+  requires(memory_no_alias(ptr, len))
+  assigns(memory_slice(ptr, len))
+);
+
+#if defined(MLD_CONFIG_CUSTOM_ZEROIZE)
+static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
+{
+  mld_zeroize_native(ptr, len);
+}
+#elif defined(MLD_SYS_WINDOWS)
+#include <windows.h>
+static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
+{
+  SecureZeroMemory(ptr, len);
+}
+#elif defined(MLD_HAVE_INLINE_ASM)
+static MLD_INLINE void mld_zeroize(void *ptr, size_t len)
+{
+  memset(ptr, 0, len);
+  /* This follows OpenSSL and seems sufficient to prevent the compiler
+   * from optimizing away the memset.
+   *
+   * If there was a reliable way to detect availability of memset_s(),
+   * that would be preferred. */
+  __asm__ __volatile__("" : : "r"(ptr) : "memory");
+}
+#else /* !MLD_CONFIG_CUSTOM_ZEROIZE && !MLD_SYS_WINDOWS && MLD_HAVE_INLINE_ASM \
+       */
+#error No plausibly-secure implementation of mld_zeroize available. Please provide your own using MLD_CONFIG_CUSTOM_ZEROIZE.
+#endif /* !MLD_CONFIG_CUSTOM_ZEROIZE && !MLD_SYS_WINDOWS && \
+          !MLD_HAVE_INLINE_ASM */
+
+#endif /* !__ASSEMBLER__ */
+
 
 #endif /* !MLD_CT_H */
diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c
index d3b315751..ee7f83221 100644
--- a/mldsa/src/fips202/fips202.c
+++ b/mldsa/src/fips202/fips202.c
@@ -34,8 +34,11 @@
 #include <stddef.h>
 #include <stdint.h>
 
+#include "../common.h"
+#include "../ct.h"
 #include "fips202.h"
 #include "keccakf1600.h"
+#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
 
 #define NROUNDS 24
 
@@ -259,3 +262,5 @@ void mld_shake256(uint8_t *out, size_t outlen, const uint8_t *in, size_t inlen)
   mld_shake256_squeeze(out, outlen, &state);
   mld_shake256_release(&state);
 }
+
+#endif /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
diff --git a/mldsa/src/fips202/fips202x4.c b/mldsa/src/fips202/fips202x4.c
index 3288f7e79..0fb5cd57c 100644
--- a/mldsa/src/fips202/fips202x4.c
+++ b/mldsa/src/fips202/fips202x4.c
@@ -14,8 +14,10 @@
  */
 
 #include "../common.h"
+#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
 
 #include <string.h>
+#include "../ct.h"
 #include "fips202.h"
 #include "fips202x4.h"
 #include "keccakf1600.h"
@@ -163,3 +165,5 @@ void mld_shake256x4_release(mld_shake256x4ctx *state)
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
   mld_zeroize(state, sizeof(mld_shake256x4ctx));
 }
+
+#endif /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c
index c8eafe7c3..136598543 100644
--- a/mldsa/src/packing.c
+++ b/mldsa/src/packing.c
@@ -9,6 +9,13 @@
 #include "poly.h"
 #include "polyvec.h"
 
+/* Parameter set namespacing
+ * This is to facilitate building multiple instances
+ * of mldsa-native (e.g. with varying parameter sets)
+ * within a single compilation unit. */
+#define mld_unpack_hints MLD_ADD_PARAM_SET(mld_unpack_hints)
+/* End of parameter set namespacing */
+
 MLD_INTERNAL_API
 void mld_pack_pk(uint8_t pk[CRYPTO_PUBLICKEYBYTES],
                  const uint8_t rho[MLDSA_SEEDBYTES], const mld_polyveck *t1)
diff --git a/mldsa/src/poly.h b/mldsa/src/poly.h
index 0257309e7..f42fe0df4 100644
--- a/mldsa/src/poly.h
+++ b/mldsa/src/poly.h
@@ -217,119 +217,6 @@ __contract__(
   ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, ((MLDSA_Q - 1) / MLD_2_POW_D) + 1))
 );
 
-
-#define mld_poly_decompose MLD_NAMESPACE(poly_decompose)
-/*************************************************
- * Name:        mld_poly_decompose
- *
- * Description: For all coefficients c of the input polynomial,
- *              compute high and low bits c0, c1 such c mod MLDSA_Q = c1*ALPHA +
- *              c0 with -ALPHA/2 < c0 <= ALPHA/2 except
- *              c1 = (MLDSA_Q-1)/ALPHA where we set
- *              c1 = 0 and -ALPHA/2 <= c0 = c mod MLDSA_Q - MLDSA_Q < 0.
- *              Assumes coefficients to be standard representatives.
- *
- * Arguments:   - mld_poly *a1: pointer to output polynomial with coefficients
- *c1
- *              - mld_poly *a0: pointer to output polynomial with coefficients
- *c0
- *              - const mld_poly *a: pointer to input polynomial
- **************************************************/
-MLD_INTERNAL_API
-void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a)
-__contract__(
-  requires(memory_no_alias(a1,  sizeof(mld_poly)))
-  requires(memory_no_alias(a0, sizeof(mld_poly)))
-  requires(memory_no_alias(a, sizeof(mld_poly)))
-  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)))
-  ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
-  ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1))
-);
-
-#define mld_poly_make_hint MLD_NAMESPACE(poly_make_hint)
-/*************************************************
- * Name:        mld_poly_make_hint
- *
- * Description: Compute hint polynomial. The coefficients of which indicate
- *              whether the low bits of the corresponding coefficient of
- *              the input polynomial overflow into the high bits.
- *
- * Arguments:   - mld_poly *h: pointer to output hint polynomial
- *              - const mld_poly *a0: pointer to low part of input polynomial
- *              - const mld_poly *a1: pointer to high part of input polynomial
- *
- * Returns number of 1 bits.
- **************************************************/
-MLD_INTERNAL_API
-unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0,
-                                const mld_poly *a1)
-__contract__(
-  requires(memory_no_alias(h,  sizeof(mld_poly)))
-  requires(memory_no_alias(a0, sizeof(mld_poly)))
-  requires(memory_no_alias(a1, sizeof(mld_poly)))
-  assigns(memory_slice(h, sizeof(mld_poly)))
-  ensures(return_value <= MLDSA_N)
-  ensures(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
-);
-
-#define mld_poly_use_hint MLD_NAMESPACE(poly_use_hint)
-/*************************************************
- * Name:        mld_poly_use_hint
- *
- * Description: Use hint polynomial to correct the high bits of a polynomial.
- *
- * Arguments:   - mld_poly *b: pointer to output polynomial with corrected high
- *bits
- *              - const mld_poly *a: pointer to input polynomial
- *              - const mld_poly *h: pointer to input hint polynomial
- **************************************************/
-MLD_INTERNAL_API
-void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
-__contract__(
-  requires(memory_no_alias(a,  sizeof(mld_poly)))
-  requires(memory_no_alias(b, sizeof(mld_poly)))
-  requires(memory_no_alias(h, sizeof(mld_poly)))
-  requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
-  requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
-  assigns(memory_slice(b, sizeof(mld_poly)))
-  ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
-);
-
-#define mld_poly_chknorm MLD_NAMESPACE(poly_chknorm)
-/*************************************************
- * Name:        mld_poly_chknorm
- *
- * Description: Check infinity norm of polynomial against given bound.
- *              Assumes input coefficients were reduced by mld_reduce32().
- *
- * Arguments:   - const mld_poly *a: pointer to polynomial
- *              - int32_t B: norm bound
- *
- * Returns 0 if norm is strictly smaller than
- * B <= (MLDSA_Q - REDUCE32_RANGE_MAX) and 0xFFFFFFFF otherwise.
- *
- * Specification: The definition of this FIPS-204 requires signed canonical
- *                reduction prior to applying the bounds check.
- *                However, `-B < (a mod± MLDSA_Q) < B` is equivalent to
- *                `-B < a < B` under the assumption that
- *                `B <= MLDSA_Q - REDUCE32_RANGE_MAX` (cf. the assertion in
- *                the code). Hence, the present spec and implementation are
- *                correct without reduction.
- *
- **************************************************/
-MLD_INTERNAL_API
-uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
-__contract__(
-  requires(memory_no_alias(a, sizeof(mld_poly)))
-  requires(0 <= B && B <= MLDSA_Q - REDUCE32_RANGE_MAX)
-  requires(array_bound(a->coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))
-  ensures(return_value == 0 || return_value == 0xFFFFFFFF)
-  ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B))
-);
-
-
 #define mld_poly_uniform MLD_NAMESPACE(poly_uniform)
 /*************************************************
  * Name:        mld_poly_uniform
@@ -385,181 +272,6 @@ __contract__(
   ensures(array_bound(vec3->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
 );
 
-#define mld_poly_uniform_eta_4x MLD_NAMESPACE_KL(poly_uniform_eta_4x)
-/*************************************************
- * Name:        mld_poly_uniform_eta
- *
- * Description: Sample four polynomials with uniformly random coefficients
- *              in [-MLDSA_ETA,MLDSA_ETA] by performing rejection sampling on
- *              the output stream from SHAKE256(seed|nonce_i)
- *
- * Arguments:   - mld_poly *r0: pointer to first output polynomial
- *              - mld_poly *r1: pointer to second output polynomial
- *              - mld_poly *r2: pointer to third output polynomial
- *              - mld_poly *r3: pointer to fourth output polynomial
- *              - const uint8_t seed[]: byte array with seed of length
- *                MLDSA_CRHBYTES
- *              - uint8_t nonce0: first nonce
- *              - uint8_t nonce1: second nonce
- *              - uint8_t nonce2: third nonce
- *              - uint8_t nonce3: fourth nonce
- **************************************************/
-MLD_INTERNAL_API
-void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
-                             mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES],
-                             uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
-                             uint8_t nonce3)
-__contract__(
-  requires(memory_no_alias(r0, sizeof(mld_poly)))
-  requires(memory_no_alias(r1, sizeof(mld_poly)))
-  requires(memory_no_alias(r2, sizeof(mld_poly)))
-  requires(memory_no_alias(r3, sizeof(mld_poly)))
-  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
-  assigns(memory_slice(r0, sizeof(mld_poly)))
-  assigns(memory_slice(r1, sizeof(mld_poly)))
-  assigns(memory_slice(r2, sizeof(mld_poly)))
-  assigns(memory_slice(r3, sizeof(mld_poly)))
-  ensures(array_abs_bound(r0->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
-  ensures(array_abs_bound(r1->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
-  ensures(array_abs_bound(r2->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
-  ensures(array_abs_bound(r3->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
-);
-
-#define mld_poly_uniform_gamma1 MLD_NAMESPACE_KL(poly_uniform_gamma1)
-/*************************************************
- * Name:        mld_poly_uniform_gamma1
- *
- * Description: Sample polynomial with uniformly random coefficients
- *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1] by unpacking output
- *              stream of SHAKE256(seed|nonce)
- *
- * Arguments:   - mld_poly *a: pointer to output polynomial
- *              - const uint8_t seed[]: byte array with seed of length
- *                MLDSA_CRHBYTES
- *              - uint16_t nonce: 16-bit nonce
- **************************************************/
-MLD_INTERNAL_API
-void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES],
-                             uint16_t nonce)
-__contract__(
-  requires(memory_no_alias(a, sizeof(mld_poly)))
-  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
-  assigns(memory_slice(a, sizeof(mld_poly)))
-  ensures(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
-);
-
-
-#define mld_poly_uniform_gamma1_4x MLD_NAMESPACE_KL(poly_uniform_gamma1_4x)
-/*************************************************
- * Name:        mld_poly_uniform_gamma1_4x
- *
- * Description: Sample polynomial with uniformly random coefficients
- *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1] by unpacking output
- *              stream of SHAKE256(seed|nonce)
- *
- * Arguments:   - mld_poly *a: pointer to output polynomial
- *              - const uint8_t seed[]: byte array with seed of length
- *                MLDSA_CRHBYTES
- *              - uint16_t nonce: 16-bit nonce
- **************************************************/
-MLD_INTERNAL_API
-void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
-                                mld_poly *r3,
-                                const uint8_t seed[MLDSA_CRHBYTES],
-                                uint16_t nonce0, uint16_t nonce1,
-                                uint16_t nonce2, uint16_t nonce3)
-__contract__(
-  requires(memory_no_alias(r0, sizeof(mld_poly)))
-  requires(memory_no_alias(r1, sizeof(mld_poly)))
-  requires(memory_no_alias(r2, sizeof(mld_poly)))
-  requires(memory_no_alias(r3, sizeof(mld_poly)))
-  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
-  assigns(memory_slice(r0, sizeof(mld_poly)))
-  assigns(memory_slice(r1, sizeof(mld_poly)))
-  assigns(memory_slice(r2, sizeof(mld_poly)))
-  assigns(memory_slice(r3, sizeof(mld_poly)))
-  ensures(array_bound(r0->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
-  ensures(array_bound(r1->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
-  ensures(array_bound(r2->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
-  ensures(array_bound(r3->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
-);
-
-
-#define mld_poly_challenge MLD_NAMESPACE_KL(poly_challenge)
-/*************************************************
- * Name:        mld_poly_challenge
- *
- * Description: Implementation of H. Samples polynomial with MLDSA_TAU nonzero
- *              coefficients in {-1,1} using the output stream of
- *              SHAKE256(seed).
- *
- * Arguments:   - mld_poly *c: pointer to output polynomial
- *              - const uint8_t mu[]: byte array containing seed of length
- *                MLDSA_CTILDEBYTES
- **************************************************/
-MLD_INTERNAL_API
-void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES])
-__contract__(
-  requires(memory_no_alias(c, sizeof(mld_poly)))
-  requires(memory_no_alias(seed, MLDSA_CTILDEBYTES))
-  assigns(memory_slice(c, sizeof(mld_poly)))
-  /* All coefficients of c are -1, 0 or +1 */
-  ensures(array_bound(c->coeffs, 0, MLDSA_N, -1, 2))
-);
-
-#define mld_polyeta_pack MLD_NAMESPACE_KL(polyeta_pack)
-/*************************************************
- * Name:        mld_polyeta_pack
- *
- * Description: Bit-pack polynomial with coefficients in [-MLDSA_ETA,MLDSA_ETA].
- *
- * Arguments:   - uint8_t *r: pointer to output byte array with at least
- *                            MLDSA_POLYETA_PACKEDBYTES bytes
- *              - const mld_poly *a: pointer to input polynomial
- **************************************************/
-MLD_INTERNAL_API
-void mld_polyeta_pack(uint8_t *r, const mld_poly *a)
-__contract__(
-  requires(memory_no_alias(r, MLDSA_POLYETA_PACKEDBYTES))
-  requires(memory_no_alias(a, sizeof(mld_poly)))
-  requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
-  assigns(memory_slice(r, MLDSA_POLYETA_PACKEDBYTES))
-);
-
-/*
- * polyeta_unpack produces coefficients in [-MLDSA_ETA,MLDSA_ETA] for
- * well-formed inputs (i.e., those produced by polyeta_pack).
- * However, when passed an arbitrary byte array, it may produce smaller values,
- * i.e, values in [MLD_POLYETA_UNPACK_LOWER_BOUND,MLDSA_ETA]
- * Even though this should never happen, we use use the bound for arbitrary
- * inputs in the CBMC proofs.
- */
-#if MLDSA_ETA == 2
-#define MLD_POLYETA_UNPACK_LOWER_BOUND (-5)
-#elif MLDSA_ETA == 4
-#define MLD_POLYETA_UNPACK_LOWER_BOUND (-11)
-#else
-#error "Invalid value of MLDSA_ETA"
-#endif
-
-#define mld_polyeta_unpack MLD_NAMESPACE_KL(polyeta_unpack)
-/*************************************************
- * Name:        mld_polyeta_unpack
- *
- * Description: Unpack polynomial with coefficients in [-MLDSA_ETA,MLDSA_ETA].
- *
- * Arguments:   - mld_poly *r: pointer to output polynomial
- *              - const uint8_t *a: byte array with bit-packed polynomial
- **************************************************/
-MLD_INTERNAL_API
-void mld_polyeta_unpack(mld_poly *r, const uint8_t *a)
-__contract__(
-  requires(memory_no_alias(r, sizeof(mld_poly)))
-  requires(memory_no_alias(a, MLDSA_POLYETA_PACKEDBYTES))
-  assigns(memory_slice(r, sizeof(mld_poly)))
-  ensures(array_bound(r->coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))
-);
-
 #define mld_polyt1_pack MLD_NAMESPACE(polyt1_pack)
 /*************************************************
  * Name:        mld_polyt1_pack
@@ -639,64 +351,4 @@ __contract__(
   ensures(array_bound(r->coeffs, 0, MLDSA_N, -(1<<(MLDSA_D-1)) + 1, (1<<(MLDSA_D-1)) + 1))
 );
 
-#define mld_polyz_pack MLD_NAMESPACE_KL(polyz_pack)
-/*************************************************
- * Name:        mld_polyz_pack
- *
- * Description: Bit-pack polynomial with coefficients
- *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1].
- *
- * Arguments:   - uint8_t *r: pointer to output byte array with at least
- *                            MLDSA_POLYZ_PACKEDBYTES bytes
- *              - const mld_poly *a: pointer to input polynomial
- **************************************************/
-MLD_INTERNAL_API
-void mld_polyz_pack(uint8_t *r, const mld_poly *a)
-__contract__(
-  requires(memory_no_alias(r, MLDSA_POLYZ_PACKEDBYTES))
-  requires(memory_no_alias(a, sizeof(mld_poly)))
-  requires(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
-  assigns(object_whole(r))
-);
-
-#define mld_polyz_unpack MLD_NAMESPACE_KL(polyz_unpack)
-/*************************************************
- * Name:        mld_polyz_unpack
- *
- * Description: Unpack polynomial z with coefficients
- *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1].
- *
- * Arguments:   - mld_poly *r: pointer to output polynomial
- *              - const uint8_t *a: byte array with bit-packed polynomial
- **************************************************/
-MLD_INTERNAL_API
-void mld_polyz_unpack(mld_poly *r, const uint8_t *a)
-__contract__(
-  requires(memory_no_alias(r, sizeof(mld_poly)))
-  requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES))
-  assigns(memory_slice(r, sizeof(mld_poly)))
-  ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
-);
-
-
-#define mld_polyw1_pack MLD_NAMESPACE_KL(polyw1_pack)
-/*************************************************
- * Name:        mld_polyw1_pack
- *
- * Description: Bit-pack polynomial w1 with coefficients in [0,15] or [0,43].
- *              Input coefficients are assumed to be standard representatives.
- *
- * Arguments:   - uint8_t *r: pointer to output byte array with at least
- *                            MLDSA_POLYW1_PACKEDBYTES bytes
- *              - const mld_poly *a: pointer to input polynomial
- **************************************************/
-MLD_INTERNAL_API
-void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
-__contract__(
-  requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES))
-  requires(memory_no_alias(a, sizeof(mld_poly)))
-  requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
-  assigns(object_whole(r))
-);
-
 #endif /* !MLD_POLY_H */
diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c
index 47031a952..1bc28607b 100644
--- a/mldsa/src/poly_kl.c
+++ b/mldsa/src/poly_kl.c
@@ -23,10 +23,16 @@
 
 #include "ct.h"
 #include "debug.h"
-#include "poly.h"
+#include "poly_kl.h"
 #include "rounding.h"
 #include "symmetric.h"
 
+/* Parameter set namespacing
+ * This is to facilitate building multiple instances
+ * of mldsa-native (e.g. with varying parameter sets)
+ * within a single compilation unit. */
+#define mld_rej_eta MLD_ADD_PARAM_SET(mld_rej_eta)
+/* End of parameter set namespacing */
 
 MLD_INTERNAL_API
 void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a)
@@ -809,3 +815,7 @@ void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
   }
 #endif /* MLD_CONFIG_PARAMETER_SET != 44 */
 }
+
+/* To facilitate single-compilation-unit (SCU) builds, undefine all macros. */
+/* TODO: autogenerate */
+#undef POLY_UNIFORM_ETA_NBLOCKS
diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h
new file mode 100644
index 000000000..ebd36b3f4
--- /dev/null
+++ b/mldsa/src/poly_kl.h
@@ -0,0 +1,357 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+#ifndef MLD_POLY_KL_H
+#define MLD_POLY_KL_H
+
+#include "cbmc.h"
+#include "common.h"
+#include "poly.h"
+
+#define mld_poly_decompose MLD_NAMESPACE_KL(poly_decompose)
+/*************************************************
+ * Name:        mld_poly_decompose
+ *
+ * Description: For all coefficients c of the input polynomial,
+ *              compute high and low bits c0, c1 such c mod MLDSA_Q = c1*ALPHA +
+ *              c0 with -ALPHA/2 < c0 <= ALPHA/2 except
+ *              c1 = (MLDSA_Q-1)/ALPHA where we set
+ *              c1 = 0 and -ALPHA/2 <= c0 = c mod MLDSA_Q - MLDSA_Q < 0.
+ *              Assumes coefficients to be standard representatives.
+ *
+ * Arguments:   - mld_poly *a1: pointer to output polynomial with coefficients
+ *c1
+ *              - mld_poly *a0: pointer to output polynomial with coefficients
+ *c0
+ *              - const mld_poly *a: pointer to input polynomial
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_decompose(mld_poly *a1, mld_poly *a0, const mld_poly *a)
+__contract__(
+  requires(memory_no_alias(a1,  sizeof(mld_poly)))
+  requires(memory_no_alias(a0, sizeof(mld_poly)))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  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)))
+  ensures(array_bound(a1->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+  ensures(array_abs_bound(a0->coeffs, 0, MLDSA_N, MLDSA_GAMMA2+1))
+);
+
+
+#define mld_poly_make_hint MLD_NAMESPACE_KL(poly_make_hint)
+/*************************************************
+ * Name:        mld_poly_make_hint
+ *
+ * Description: Compute hint polynomial. The coefficients of which indicate
+ *              whether the low bits of the corresponding coefficient of
+ *              the input polynomial overflow into the high bits.
+ *
+ * Arguments:   - mld_poly *h: pointer to output hint polynomial
+ *              - const mld_poly *a0: pointer to low part of input polynomial
+ *              - const mld_poly *a1: pointer to high part of input polynomial
+ *
+ * Returns number of 1 bits.
+ **************************************************/
+MLD_INTERNAL_API
+unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0,
+                                const mld_poly *a1)
+__contract__(
+  requires(memory_no_alias(h,  sizeof(mld_poly)))
+  requires(memory_no_alias(a0, sizeof(mld_poly)))
+  requires(memory_no_alias(a1, sizeof(mld_poly)))
+  assigns(memory_slice(h, sizeof(mld_poly)))
+  ensures(return_value <= MLDSA_N)
+  ensures(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
+);
+
+#define mld_poly_use_hint MLD_NAMESPACE_KL(poly_use_hint)
+/*************************************************
+ * Name:        mld_poly_use_hint
+ *
+ * Description: Use hint polynomial to correct the high bits of a polynomial.
+ *
+ * Arguments:   - mld_poly *b: pointer to output polynomial with corrected high
+ *bits
+ *              - const mld_poly *a: pointer to input polynomial
+ *              - const mld_poly *h: pointer to input hint polynomial
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
+__contract__(
+  requires(memory_no_alias(a,  sizeof(mld_poly)))
+  requires(memory_no_alias(b, sizeof(mld_poly)))
+  requires(memory_no_alias(h, sizeof(mld_poly)))
+  requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
+  requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
+  assigns(memory_slice(b, sizeof(mld_poly)))
+  ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+);
+
+#define mld_poly_chknorm MLD_NAMESPACE_KL(poly_chknorm)
+/*************************************************
+ * Name:        mld_poly_chknorm
+ *
+ * Description: Check infinity norm of polynomial against given bound.
+ *              Assumes input coefficients were reduced by mld_reduce32().
+ *
+ * Arguments:   - const mld_poly *a: pointer to polynomial
+ *              - int32_t B: norm bound
+ *
+ * Returns 0 if norm is strictly smaller than
+ * B <= (MLDSA_Q - REDUCE32_RANGE_MAX) and 0xFFFFFFFF otherwise.
+ *
+ * Specification: The definition of this FIPS-204 requires signed canonical
+ *                reduction prior to applying the bounds check.
+ *                However, `-B < (a mod± MLDSA_Q) < B` is equivalent to
+ *                `-B < a < B` under the assumption that
+ *                `B <= MLDSA_Q - REDUCE32_RANGE_MAX` (cf. the assertion in
+ *                the code). Hence, the present spec and implementation are
+ *                correct without reduction.
+ *
+ **************************************************/
+MLD_INTERNAL_API
+uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
+__contract__(
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(0 <= B && B <= MLDSA_Q - REDUCE32_RANGE_MAX)
+  requires(array_bound(a->coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX))
+  ensures(return_value == 0 || return_value == 0xFFFFFFFF)
+  ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B))
+);
+
+#define mld_poly_uniform_eta_4x MLD_NAMESPACE_KL(poly_uniform_eta_4x)
+/*************************************************
+ * Name:        mld_poly_uniform_eta
+ *
+ * Description: Sample four polynomials with uniformly random coefficients
+ *              in [-MLDSA_ETA,MLDSA_ETA] by performing rejection sampling on
+ *              the output stream from SHAKE256(seed|nonce_i)
+ *
+ * Arguments:   - mld_poly *r0: pointer to first output polynomial
+ *              - mld_poly *r1: pointer to second output polynomial
+ *              - mld_poly *r2: pointer to third output polynomial
+ *              - mld_poly *r3: pointer to fourth output polynomial
+ *              - const uint8_t seed[]: byte array with seed of length
+ *                MLDSA_CRHBYTES
+ *              - uint8_t nonce0: first nonce
+ *              - uint8_t nonce1: second nonce
+ *              - uint8_t nonce2: third nonce
+ *              - uint8_t nonce3: fourth nonce
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_uniform_eta_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
+                             mld_poly *r3, const uint8_t seed[MLDSA_CRHBYTES],
+                             uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
+                             uint8_t nonce3)
+__contract__(
+  requires(memory_no_alias(r0, sizeof(mld_poly)))
+  requires(memory_no_alias(r1, sizeof(mld_poly)))
+  requires(memory_no_alias(r2, sizeof(mld_poly)))
+  requires(memory_no_alias(r3, sizeof(mld_poly)))
+  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
+  assigns(memory_slice(r0, sizeof(mld_poly)))
+  assigns(memory_slice(r1, sizeof(mld_poly)))
+  assigns(memory_slice(r2, sizeof(mld_poly)))
+  assigns(memory_slice(r3, sizeof(mld_poly)))
+  ensures(array_abs_bound(r0->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
+  ensures(array_abs_bound(r1->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
+  ensures(array_abs_bound(r2->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
+  ensures(array_abs_bound(r3->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
+);
+
+#define mld_poly_uniform_gamma1 MLD_NAMESPACE_KL(poly_uniform_gamma1)
+/*************************************************
+ * Name:        mld_poly_uniform_gamma1
+ *
+ * Description: Sample polynomial with uniformly random coefficients
+ *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1] by unpacking output
+ *              stream of SHAKE256(seed|nonce)
+ *
+ * Arguments:   - mld_poly *a: pointer to output polynomial
+ *              - const uint8_t seed[]: byte array with seed of length
+ *                MLDSA_CRHBYTES
+ *              - uint16_t nonce: 16-bit nonce
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_uniform_gamma1(mld_poly *a, const uint8_t seed[MLDSA_CRHBYTES],
+                             uint16_t nonce)
+__contract__(
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
+  assigns(memory_slice(a, sizeof(mld_poly)))
+  ensures(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+);
+
+#define mld_poly_uniform_gamma1_4x MLD_NAMESPACE_KL(poly_uniform_gamma1_4x)
+/*************************************************
+ * Name:        mld_poly_uniform_gamma1_4x
+ *
+ * Description: Sample polynomial with uniformly random coefficients
+ *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1] by unpacking output
+ *              stream of SHAKE256(seed|nonce)
+ *
+ * Arguments:   - mld_poly *a: pointer to output polynomial
+ *              - const uint8_t seed[]: byte array with seed of length
+ *                MLDSA_CRHBYTES
+ *              - uint16_t nonce: 16-bit nonce
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_uniform_gamma1_4x(mld_poly *r0, mld_poly *r1, mld_poly *r2,
+                                mld_poly *r3,
+                                const uint8_t seed[MLDSA_CRHBYTES],
+                                uint16_t nonce0, uint16_t nonce1,
+                                uint16_t nonce2, uint16_t nonce3)
+__contract__(
+  requires(memory_no_alias(r0, sizeof(mld_poly)))
+  requires(memory_no_alias(r1, sizeof(mld_poly)))
+  requires(memory_no_alias(r2, sizeof(mld_poly)))
+  requires(memory_no_alias(r3, sizeof(mld_poly)))
+  requires(memory_no_alias(seed, MLDSA_CRHBYTES))
+  assigns(memory_slice(r0, sizeof(mld_poly)))
+  assigns(memory_slice(r1, sizeof(mld_poly)))
+  assigns(memory_slice(r2, sizeof(mld_poly)))
+  assigns(memory_slice(r3, sizeof(mld_poly)))
+  ensures(array_bound(r0->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+  ensures(array_bound(r1->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+  ensures(array_bound(r2->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+  ensures(array_bound(r3->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+);
+
+#define mld_poly_challenge MLD_NAMESPACE_KL(poly_challenge)
+/*************************************************
+ * Name:        mld_poly_challenge
+ *
+ * Description: Implementation of H. Samples polynomial with MLDSA_TAU nonzero
+ *              coefficients in {-1,1} using the output stream of
+ *              SHAKE256(seed).
+ *
+ * Arguments:   - mld_poly *c: pointer to output polynomial
+ *              - const uint8_t mu[]: byte array containing seed of length
+ *                MLDSA_CTILDEBYTES
+ **************************************************/
+MLD_INTERNAL_API
+void mld_poly_challenge(mld_poly *c, const uint8_t seed[MLDSA_CTILDEBYTES])
+__contract__(
+  requires(memory_no_alias(c, sizeof(mld_poly)))
+  requires(memory_no_alias(seed, MLDSA_CTILDEBYTES))
+  assigns(memory_slice(c, sizeof(mld_poly)))
+  /* All coefficients of c are -1, 0 or +1 */
+  ensures(array_bound(c->coeffs, 0, MLDSA_N, -1, 2))
+);
+
+#define mld_polyeta_pack MLD_NAMESPACE_KL(polyeta_pack)
+/*************************************************
+ * Name:        mld_polyeta_pack
+ *
+ * Description: Bit-pack polynomial with coefficients in [-MLDSA_ETA,MLDSA_ETA].
+ *
+ * Arguments:   - uint8_t *r: pointer to output byte array with at least
+ *                            MLDSA_POLYETA_PACKEDBYTES bytes
+ *              - const mld_poly *a: pointer to input polynomial
+ **************************************************/
+MLD_INTERNAL_API
+void mld_polyeta_pack(uint8_t *r, const mld_poly *a)
+__contract__(
+  requires(memory_no_alias(r, MLDSA_POLYETA_PACKEDBYTES))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_abs_bound(a->coeffs, 0, MLDSA_N, MLDSA_ETA + 1))
+  assigns(memory_slice(r, MLDSA_POLYETA_PACKEDBYTES))
+);
+
+/*
+ * polyeta_unpack produces coefficients in [-MLDSA_ETA,MLDSA_ETA] for
+ * well-formed inputs (i.e., those produced by polyeta_pack).
+ * However, when passed an arbitrary byte array, it may produce smaller values,
+ * i.e, values in [MLD_POLYETA_UNPACK_LOWER_BOUND,MLDSA_ETA]
+ * Even though this should never happen, we use use the bound for arbitrary
+ * inputs in the CBMC proofs.
+ */
+#if MLDSA_ETA == 2
+#define MLD_POLYETA_UNPACK_LOWER_BOUND (-5)
+#elif MLDSA_ETA == 4
+#define MLD_POLYETA_UNPACK_LOWER_BOUND (-11)
+#else
+#error "Invalid value of MLDSA_ETA"
+#endif
+
+#define mld_polyeta_unpack MLD_NAMESPACE_KL(polyeta_unpack)
+/*************************************************
+ * Name:        mld_polyeta_unpack
+ *
+ * Description: Unpack polynomial with coefficients in [-MLDSA_ETA,MLDSA_ETA].
+ *
+ * Arguments:   - mld_poly *r: pointer to output polynomial
+ *              - const uint8_t *a: byte array with bit-packed polynomial
+ **************************************************/
+MLD_INTERNAL_API
+void mld_polyeta_unpack(mld_poly *r, const uint8_t *a)
+__contract__(
+  requires(memory_no_alias(r, sizeof(mld_poly)))
+  requires(memory_no_alias(a, MLDSA_POLYETA_PACKEDBYTES))
+  assigns(memory_slice(r, sizeof(mld_poly)))
+  ensures(array_bound(r->coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1))
+);
+
+#define mld_polyz_pack MLD_NAMESPACE_KL(polyz_pack)
+/*************************************************
+ * Name:        mld_polyz_pack
+ *
+ * Description: Bit-pack polynomial with coefficients
+ *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1].
+ *
+ * Arguments:   - uint8_t *r: pointer to output byte array with at least
+ *                            MLDSA_POLYZ_PACKEDBYTES bytes
+ *              - const mld_poly *a: pointer to input polynomial
+ **************************************************/
+MLD_INTERNAL_API
+void mld_polyz_pack(uint8_t *r, const mld_poly *a)
+__contract__(
+  requires(memory_no_alias(r, MLDSA_POLYZ_PACKEDBYTES))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_bound(a->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+  assigns(object_whole(r))
+);
+
+
+#define mld_polyz_unpack MLD_NAMESPACE_KL(polyz_unpack)
+/*************************************************
+ * Name:        mld_polyz_unpack
+ *
+ * Description: Unpack polynomial z with coefficients
+ *              in [-(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1].
+ *
+ * Arguments:   - mld_poly *r: pointer to output polynomial
+ *              - const uint8_t *a: byte array with bit-packed polynomial
+ **************************************************/
+MLD_INTERNAL_API
+void mld_polyz_unpack(mld_poly *r, const uint8_t *a)
+__contract__(
+  requires(memory_no_alias(r, sizeof(mld_poly)))
+  requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES))
+  assigns(memory_slice(r, sizeof(mld_poly)))
+  ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
+);
+
+#define mld_polyw1_pack MLD_NAMESPACE_KL(polyw1_pack)
+/*************************************************
+ * Name:        mld_polyw1_pack
+ *
+ * Description: Bit-pack polynomial w1 with coefficients in [0,15] or [0,43].
+ *              Input coefficients are assumed to be standard representatives.
+ *
+ * Arguments:   - uint8_t *r: pointer to output byte array with at least
+ *                            MLDSA_POLYW1_PACKEDBYTES bytes
+ *              - const mld_poly *a: pointer to input polynomial
+ **************************************************/
+MLD_INTERNAL_API
+void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
+__contract__(
+  requires(memory_no_alias(r, MLDSA_POLYW1_PACKEDBYTES))
+  requires(memory_no_alias(a, sizeof(mld_poly)))
+  requires(array_bound(a->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
+  assigns(object_whole(r))
+);
+
+#endif /* !MLD_POLY_KL_H */
diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c
index d10f8166c..8469c8654 100644
--- a/mldsa/src/polyvec.c
+++ b/mldsa/src/polyvec.c
@@ -18,13 +18,14 @@
 #include "common.h"
 #include "debug.h"
 #include "poly.h"
+#include "poly_kl.h"
 #include "polyvec.h"
 
 #if !defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER)
 /* This namespacing is not done at the top to avoid a naming conflict
  * with native backends, which are currently not yet namespaced. */
 #define mld_poly_permute_bitrev_to_custom \
-  MLD_NAMESPACE(mld_poly_permute_bitrev_to_custom)
+  MLD_NAMESPACE_KL(mld_poly_permute_bitrev_to_custom)
 
 static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t data[MLDSA_N])
 {
diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h
index 2ab048f2f..06f1174ec 100644
--- a/mldsa/src/polyvec.h
+++ b/mldsa/src/polyvec.h
@@ -9,6 +9,15 @@
 #include "cbmc.h"
 #include "common.h"
 #include "poly.h"
+#include "poly_kl.h"
+
+/* Parameter set namespacing
+ * This is to facilitate building multiple instances
+ * of mldsa-native (e.g. with varying parameter sets)
+ * within a single compilation unit. */
+#define mld_polyvecl MLD_ADD_PARAM_SET(mld_polyvecl)
+#define mld_polyveck MLD_ADD_PARAM_SET(mld_polyveck)
+/* End of parameter set namespacing */
 
 /* Vectors of polynomials of length MLDSA_L */
 typedef struct
@@ -16,7 +25,6 @@ typedef struct
   mld_poly vec[MLDSA_L];
 } mld_polyvecl;
 
-#define mld_polyvecl MLD_ADD_PARAM_SET(mld_polyvecl)
 
 #define mld_polyvecl_uniform_gamma1 MLD_NAMESPACE_KL(polyvecl_uniform_gamma1)
 /*************************************************
@@ -223,8 +231,6 @@ typedef struct
   mld_poly vec[MLDSA_K];
 } mld_polyveck;
 
-#define mld_polyveck MLD_ADD_PARAM_SET(mld_polyveck)
-
 #define mld_polyveck_reduce MLD_NAMESPACE_KL(polyveck_reduce)
 /*************************************************
  * Name:        polyveck_reduce
diff --git a/mldsa/src/prehash.c b/mldsa/src/prehash.c
index 1d555a305..4eef6563b 100644
--- a/mldsa/src/prehash.c
+++ b/mldsa/src/prehash.c
@@ -6,6 +6,7 @@
 #include "prehash.h"
 #include "symmetric.h"
 
+#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
 #define MLD_PRE_HASH_OID_LEN 11
 
 /*************************************************
@@ -119,3 +120,5 @@ size_t mld_format_pre_hash_message(
   /* Return total formatted message length */
   return 2 + ctxlen + MLD_PRE_HASH_OID_LEN + phlen;
 }
+
+#endif /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
diff --git a/mldsa/src/rounding.h b/mldsa/src/rounding.h
index 9f22be16d..32b37f2b0 100644
--- a/mldsa/src/rounding.h
+++ b/mldsa/src/rounding.h
@@ -21,6 +21,16 @@
 #include "ct.h"
 #include "debug.h"
 
+/* Parameter set namespacing
+ * This is to facilitate building multiple instances
+ * of mldsa-native (e.g. with varying parameter sets)
+ * within a single compilation unit. */
+#define mld_power2round MLD_ADD_PARAM_SET(mld_power2round)
+#define mld_decompose MLD_ADD_PARAM_SET(mld_decompose)
+#define mld_make_hint MLD_ADD_PARAM_SET(mld_make_hint)
+#define mld_use_hint MLD_ADD_PARAM_SET(mld_use_hint)
+/* End of parameter set namespacing */
+
 #define MLD_2_POW_D (1 << MLDSA_D)
 
 /*************************************************
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index 763d4e01e..39dbe4bf4 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -30,12 +30,24 @@
 #include "debug.h"
 #include "packing.h"
 #include "poly.h"
+#include "poly_kl.h"
 #include "polyvec.h"
 #include "prehash.h"
 #include "randombytes.h"
 #include "sign.h"
 #include "symmetric.h"
 
+/* Parameter set namespacing
+ * This is to facilitate building multiple instances
+ * of mldsa-native (e.g. with varying parameter sets)
+ * within a single compilation unit. */
+#define mld_check_pct MLD_ADD_PARAM_SET(mld_check_pct)
+#define mld_sample_s1_s2 MLD_ADD_PARAM_SET(mld_sample_s1_s2)
+#define mld_H MLD_ADD_PARAM_SET(mld_H)
+#define mld_attempt_signature_generation \
+  MLD_ADD_PARAM_SET(mld_attempt_signature_generation)
+/* End of parameter set namespacing */
+
 
 static int mld_check_pct(uint8_t const pk[CRYPTO_PUBLICKEYBYTES],
                          uint8_t const sk[CRYPTO_SECRETKEYBYTES])
diff --git a/mldsa/src/sign.h b/mldsa/src/sign.h
index 4ff00b1ea..1fa33b395 100644
--- a/mldsa/src/sign.h
+++ b/mldsa/src/sign.h
@@ -45,6 +45,8 @@
 /*************************************************
  * Hash algorithm enumeration for pre-hash functions
  **************************************************/
+#if !defined(MLD_CONFIG_MULTILEVEL_NO_SHARED)
+/* TODO: is there a better way?*/
 typedef enum
 {
   MLD_SHA2_224,
@@ -60,6 +62,7 @@ typedef enum
   MLD_SHAKE_128,
   MLD_SHAKE_256
 } mld_hash_alg_t;
+#endif /* !MLD_CONFIG_MULTILEVEL_NO_SHARED */
 
 /*************************************************
  * Name:        crypto_sign_keypair_internal
diff --git a/proofs/cbmc/poly_challenge/poly_challenge_harness.c b/proofs/cbmc/poly_challenge/poly_challenge_harness.c
index 8cbcff4b8..2f6224194 100644
--- a/proofs/cbmc/poly_challenge/poly_challenge_harness.c
+++ b/proofs/cbmc/poly_challenge/poly_challenge_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 
 void harness(void)
diff --git a/proofs/cbmc/poly_chknorm/poly_chknorm_harness.c b/proofs/cbmc/poly_chknorm/poly_chknorm_harness.c
index 59ac869f2..890886154 100644
--- a/proofs/cbmc/poly_chknorm/poly_chknorm_harness.c
+++ b/proofs/cbmc/poly_chknorm/poly_chknorm_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 
 void harness(void)
diff --git a/proofs/cbmc/poly_decompose/poly_decompose_harness.c b/proofs/cbmc/poly_decompose/poly_decompose_harness.c
index aef542980..309afec1e 100644
--- a/proofs/cbmc/poly_decompose/poly_decompose_harness.c
+++ b/proofs/cbmc/poly_decompose/poly_decompose_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 
 void harness(void)
diff --git a/proofs/cbmc/poly_make_hint/poly_make_hint_harness.c b/proofs/cbmc/poly_make_hint/poly_make_hint_harness.c
index c8bd9c122..fc03487dc 100644
--- a/proofs/cbmc/poly_make_hint/poly_make_hint_harness.c
+++ b/proofs/cbmc/poly_make_hint/poly_make_hint_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/poly_uniform_eta_4x/poly_uniform_eta_4x_harness.c b/proofs/cbmc/poly_uniform_eta_4x/poly_uniform_eta_4x_harness.c
index bbab97217..0b847a85d 100644
--- a/proofs/cbmc/poly_uniform_eta_4x/poly_uniform_eta_4x_harness.c
+++ b/proofs/cbmc/poly_uniform_eta_4x/poly_uniform_eta_4x_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/poly_uniform_gamma1/poly_uniform_gamma1_harness.c b/proofs/cbmc/poly_uniform_gamma1/poly_uniform_gamma1_harness.c
index c9e2174e4..6c0b1fe47 100644
--- a/proofs/cbmc/poly_uniform_gamma1/poly_uniform_gamma1_harness.c
+++ b/proofs/cbmc/poly_uniform_gamma1/poly_uniform_gamma1_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/poly_uniform_gamma1_4x/poly_uniform_gamma1_4x_harness.c b/proofs/cbmc/poly_uniform_gamma1_4x/poly_uniform_gamma1_4x_harness.c
index d9bb30dc7..ed9e7070a 100644
--- a/proofs/cbmc/poly_uniform_gamma1_4x/poly_uniform_gamma1_4x_harness.c
+++ b/proofs/cbmc/poly_uniform_gamma1_4x/poly_uniform_gamma1_4x_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c b/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c
index 4912f1052..360de6d3f 100644
--- a/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c
+++ b/proofs/cbmc/poly_use_hint/poly_use_hint_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 
 void harness(void)
diff --git a/proofs/cbmc/polyeta_pack/polyeta_pack_harness.c b/proofs/cbmc/polyeta_pack/polyeta_pack_harness.c
index fc2582aaa..d2471fc4f 100644
--- a/proofs/cbmc/polyeta_pack/polyeta_pack_harness.c
+++ b/proofs/cbmc/polyeta_pack/polyeta_pack_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/polyeta_unpack/polyeta_unpack_harness.c b/proofs/cbmc/polyeta_unpack/polyeta_unpack_harness.c
index 12fa29519..3b05d0acf 100644
--- a/proofs/cbmc/polyeta_unpack/polyeta_unpack_harness.c
+++ b/proofs/cbmc/polyeta_unpack/polyeta_unpack_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/polyw1_pack/polyw1_pack_harness.c b/proofs/cbmc/polyw1_pack/polyw1_pack_harness.c
index cea1f6df9..93fe544f9 100644
--- a/proofs/cbmc/polyw1_pack/polyw1_pack_harness.c
+++ b/proofs/cbmc/polyw1_pack/polyw1_pack_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/polyz_pack/polyz_pack_harness.c b/proofs/cbmc/polyz_pack/polyz_pack_harness.c
index bcbb8147a..463d3d3a1 100644
--- a/proofs/cbmc/polyz_pack/polyz_pack_harness.c
+++ b/proofs/cbmc/polyz_pack/polyz_pack_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {
diff --git a/proofs/cbmc/polyz_unpack/polyz_unpack_harness.c b/proofs/cbmc/polyz_unpack/polyz_unpack_harness.c
index 58fce0342..0dd46b69b 100644
--- a/proofs/cbmc/polyz_unpack/polyz_unpack_harness.c
+++ b/proofs/cbmc/polyz_unpack/polyz_unpack_harness.c
@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {