From e8ce970ea6acc5b185244123156c44c27d5cb4ed Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Tue, 13 Oct 2026 19:46:49 +0800
Subject: [PATCH 1/7] params.h: Reject invalid MLD_CONFIG_PARAMETER_SET values

Unsupported values previously failed far downstream with unrelated
errors.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 mldsa/src/params.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/mldsa/src/params.h b/mldsa/src/params.h
index 95059ae7e6..02314338c5 100644
--- a/mldsa/src/params.h
+++ b/mldsa/src/params.h
@@ -85,7 +85,10 @@
 /* check-magic: 96 == MLDSA_N * 3 / 8 */
 #define MLDSA_POLYETA_PACKEDBYTES 96
 
-#endif /* MLD_CONFIG_PARAMETER_SET == 87 */
+#else /* MLD_CONFIG_PARAMETER_SET == 87 */
+#error Invalid value for MLD_CONFIG_PARAMETER_SET. Must be 44, 65, or 87.
+#endif /* MLD_CONFIG_PARAMETER_SET != 44 && MLD_CONFIG_PARAMETER_SET != 65 && \
+          MLD_CONFIG_PARAMETER_SET != 87 */
 
 #define MLDSA_POLYT1_PACKEDBITS 10
 /* check-magic: 320 == MLDSA_N * MLDSA_POLYT1_PACKEDBITS / 8 */

From 29f5f8ba67b824d4bebbda3a81aea811cd438d2c Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Mon, 19 Oct 2026 16:52:55 +0800
Subject: [PATCH 2/7] prepare_domain_separation_prefix: Align declaration guard
 with definition

The public header declared the function in keygen-only builds, where
it is not defined. Use the guard of the definition.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 mldsa/mldsa_native.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h
index 77407f3247..b4c7be6964 100644
--- a/mldsa/mldsa_native.h
+++ b/mldsa/mldsa_native.h
@@ -793,6 +793,7 @@ int MLD_API_NAMESPACE(verify_pre_hash_shake256)(
 #endif /* !MLD_CONFIG_CORE_API_ONLY */
 
 #if !defined(MLD_CONFIG_CORE_API_ONLY)
+#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
 /**
  * Prepare domain separation prefix for ML-DSA signing.
  *
@@ -836,6 +837,7 @@ MLD_API_MUST_CHECK_RETURN_VALUE
 size_t MLD_API_NAMESPACE(prepare_domain_separation_prefix)(
     uint8_t prefix[MLD_DOMAIN_SEPARATION_MAX_BYTES], const uint8_t *ph,
     size_t phlen, const uint8_t *ctx, size_t ctxlen, int hashalg);
+#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
 
 #if !defined(MLD_CONFIG_NO_KEYPAIR_API)
 /**

From 2ba5308682ae9f681eb6e8dd5674764276119104 Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Mon, 19 Oct 2026 16:52:55 +0800
Subject: [PATCH 3/7] prepare_domain_separation_prefix: Cover ctxlen > 255 in
 the contract

Relax the precondition on ctxlen so that the CBMC proof covers the
documented error return for an overlong context string.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 mldsa/src/sign.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/mldsa/src/sign.h b/mldsa/src/sign.h
index dea6810ff9..e300d6a717 100644
--- a/mldsa/src/sign.h
+++ b/mldsa/src/sign.h
@@ -796,13 +796,14 @@ size_t mld_prepare_domain_separation_prefix(
     uint8_t prefix[MLD_DOMAIN_SEPARATION_MAX_BYTES], const uint8_t *ph,
     size_t phlen, const uint8_t *ctx, size_t ctxlen, int hashalg)
 __contract__(
-  requires(ctxlen <= 255)
+  requires(ctxlen <= MLD_MAX_BUFFER_SIZE)
   requires(phlen <= MLD_MAX_BUFFER_SIZE)
   requires(ctxlen == 0 || memory_no_alias(ctx, ctxlen))
   requires(hashalg == MLD_PREHASH_NONE || memory_no_alias(ph, phlen))
   requires(memory_no_alias(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES))
   assigns(memory_slice(prefix, MLD_DOMAIN_SEPARATION_MAX_BYTES))
   ensures(return_value <= MLD_DOMAIN_SEPARATION_MAX_BYTES)
+  ensures(ctxlen > 255 ==> return_value == 0)
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API */
 

From 02d6258a645a3bb05e6b4606be224d3bb2b9a659 Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Mon, 19 Oct 2026 16:52:55 +0800
Subject: [PATCH 4/7] prepare_domain_separation_prefix: Do not check ph for
 NULL

Per API-CONVENTIONS.md, mldsa-native does not check pointers for NULL,
and for HashML-DSA ph is paired with a non-zero length. Drop the NULL
check and the corresponding documented error.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 mldsa/mldsa_native.h | 4 ++--
 mldsa/src/sign.c     | 2 +-
 mldsa/src/sign.h     | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h
index b4c7be6964..a68c14cd3c 100644
--- a/mldsa/mldsa_native.h
+++ b/mldsa/mldsa_native.h
@@ -829,8 +829,8 @@ int MLD_API_NAMESPACE(verify_pre_hash_shake256)(
  * @return The total length of the formatted prefix, or 0 on error.
  *         Errors are:
  *         - The context string exceeded 255 bytes.
- *         - For HashML-DSA: hashalg was unsupported, ph was NULL, or phlen
- *           did not match the output length of hashalg.
+ *         - For HashML-DSA: hashalg was unsupported, or phlen did not match
+ *           the output length of hashalg.
  */
 MLD_API_QUALIFIER
 MLD_API_MUST_CHECK_RETURN_VALUE
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index 48dac1184b..2507b970d8 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -1648,7 +1648,7 @@ size_t mld_prepare_domain_separation_prefix(
 
   if (hashalg != MLD_PREHASH_NONE)
   {
-    if (ph == NULL || mld_validate_hash_length(hashalg, phlen) != 0)
+    if (mld_validate_hash_length(hashalg, phlen) != 0)
     {
       return 0;
     }
diff --git a/mldsa/src/sign.h b/mldsa/src/sign.h
index e300d6a717..ef2a08df4f 100644
--- a/mldsa/src/sign.h
+++ b/mldsa/src/sign.h
@@ -787,8 +787,8 @@ __contract__(
  * @return The total length of the formatted prefix, or 0 on error.
  *         Errors are:
  *         - The context string exceeded 255 bytes.
- *         - For HashML-DSA: hashalg was unsupported, ph was NULL, or phlen
- *           did not match the output length of hashalg.
+ *         - For HashML-DSA: hashalg was unsupported, or phlen did not match
+ *           the output length of hashalg.
  */
 MLD_MUST_CHECK_RETURN_VALUE
 MLD_EXTERNAL_API

From 4b0424a51422a7e40922fab67b2993a02853506d Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Wed, 14 Oct 2026 01:00:49 +0800
Subject: [PATCH 5/7] Guard helpers of pk_from_sk by MLD_CONFIG_CORE_API_ONLY

mld_sign_pk_from_sk() is not built with MLD_CONFIG_CORE_API_ONLY, but
its helpers were. With MLD_CONFIG_INTERNAL_API_QUALIFIER=static they
were unused and -Werror builds failed. Guard them by their actual
users.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 mldsa/src/poly.c    |  7 +++++++
 mldsa/src/poly.h    |  7 +++++++
 mldsa/src/polyvec.c | 22 +++++++++++++---------
 mldsa/src/polyvec.h | 20 +++++++++++++-------
 4 files changed, 40 insertions(+), 16 deletions(-)

diff --git a/mldsa/src/poly.c b/mldsa/src/poly.c
index 4153d80b8d..468def8360 100644
--- a/mldsa/src/poly.c
+++ b/mldsa/src/poly.c
@@ -918,6 +918,10 @@ void mld_polyt0_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYT0_PACKEDBYTES])
 }
 #endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */
 
+#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \
+    (!defined(MLD_CONFIG_NO_KEYPAIR_API) &&                                   \
+     !defined(MLD_CONFIG_CORE_API_ONLY)) ||                                   \
+    defined(MLD_UNIT_TEST)
 MLD_STATIC_TESTABLE uint32_t mld_poly_chknorm_c(const mld_poly *a, int32_t B)
 __contract__(
   requires(memory_no_alias(a, sizeof(mld_poly)))
@@ -1004,6 +1008,9 @@ uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
 #endif /* MLD_USE_NATIVE_POLY_CHKNORM */
   return mld_poly_chknorm_c(a, B);
 }
+#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API ||      \
+          (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
+          MLD_UNIT_TEST */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || \
diff --git a/mldsa/src/poly.h b/mldsa/src/poly.h
index 91cc426b76..d88c04eaf3 100644
--- a/mldsa/src/poly.h
+++ b/mldsa/src/poly.h
@@ -385,6 +385,10 @@ __contract__(
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */
 
+#if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \
+    (!defined(MLD_CONFIG_NO_KEYPAIR_API) &&                                   \
+     !defined(MLD_CONFIG_CORE_API_ONLY)) ||                                   \
+    defined(MLD_UNIT_TEST)
 #define mld_poly_chknorm MLD_NAMESPACE(poly_chknorm)
 /**
  * Check infinity norm of polynomial against given bound. Assumes input
@@ -413,6 +417,9 @@ __contract__(
   ensures(return_value == 0 || return_value == 0xFFFFFFFF)
   ensures((return_value == 0) == array_abs_bound(a->coeffs, 0, MLDSA_N, B))
 );
+#endif /* !MLD_CONFIG_NO_SIGN_API || !MLD_CONFIG_NO_VERIFY_API ||      \
+          (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
+          MLD_UNIT_TEST */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
 #if defined(MLD_CONFIG_MULTILEVEL_WITH_SHARED) || MLD_CONFIG_PARAMETER_SET == 44
diff --git a/mldsa/src/polyvec.c b/mldsa/src/polyvec.c
index be13ae3f91..6cef652ffa 100644
--- a/mldsa/src/polyvec.c
+++ b/mldsa/src/polyvec.c
@@ -206,8 +206,9 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
 }
 #endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */
 
-#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API) || \
-    defined(MLD_UNIT_TEST)
+#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
+     !defined(MLD_CONFIG_CORE_API_ONLY)) || \
+    !defined(MLD_CONFIG_NO_VERIFY_API) || defined(MLD_UNIT_TEST)
 MLD_INTERNAL_API
 uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound)
 {
@@ -232,8 +233,8 @@ uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound)
   }
   return t;
 }
-#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API || \
-          MLD_UNIT_TEST */
+#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
+          !MLD_CONFIG_NO_VERIFY_API || MLD_UNIT_TEST */
 
 /**************************************************************/
 /************ Vectors of polynomials of length MLDSA_K **************/
@@ -334,7 +335,7 @@ void mld_polyveck_invntt_tomont(mld_polyveck *v)
 }
 #endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */
 
-#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
+#if !defined(MLD_CONFIG_NO_KEYPAIR_API) && !defined(MLD_CONFIG_CORE_API_ONLY)
 MLD_INTERNAL_API
 uint32_t mld_polyveck_unpack_eta_chknorm(
     const uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES], int32_t bound,
@@ -362,7 +363,7 @@ uint32_t mld_polyveck_unpack_eta_chknorm(
   return t;
 }
 
-#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
+#endif /* !MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)
 MLD_INTERNAL_API
@@ -394,8 +395,10 @@ void mld_polyveck_decompose_pack_w1(
 }
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
-#if !defined(MLD_CONFIG_NO_KEYPAIR_API) ||                                  \
-    (!defined(MLD_CONFIG_NO_SIGN_API) &&                                    \
+#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) &&  \
+     !defined(MLD_CONFIG_CORE_API_ONLY)) ||  \
+    ((!defined(MLD_CONFIG_NO_KEYPAIR_API) || \
+      !defined(MLD_CONFIG_NO_SIGN_API)) &&   \
      (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)))
 MLD_INTERNAL_API
 void mld_polyvecl_unpack_eta(
@@ -410,7 +413,8 @@ void mld_polyvecl_unpack_eta(
   mld_assert_bound_2d(p->vec, MLDSA_L, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND,
                       MLDSA_ETA + 1);
 }
-#endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_SIGN_API && \
+#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
+          ((!MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_SIGN_API) &&  \
           (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) */
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
diff --git a/mldsa/src/polyvec.h b/mldsa/src/polyvec.h
index dfb64526dc..3187558cd2 100644
--- a/mldsa/src/polyvec.h
+++ b/mldsa/src/polyvec.h
@@ -124,7 +124,9 @@ __contract__(
 );
 #endif /* !MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST */
 
-#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || !defined(MLD_CONFIG_NO_VERIFY_API)
+#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) && \
+     !defined(MLD_CONFIG_CORE_API_ONLY)) || \
+    !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_polyvecl_chknorm MLD_NAMESPACE_KL(polyvecl_chknorm)
 /**
  * Check infinity norm of polynomials in vector of length MLDSA_L. Assumes
@@ -147,7 +149,8 @@ __contract__(
   ensures(return_value == 0 || return_value == 0xFFFFFFFF)
   ensures((return_value == 0) == forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, B)))
 );
-#endif /* !MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_VERIFY_API */
+#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
+          !MLD_CONFIG_NO_VERIFY_API */
 
 /** Vector of MLDSA_K polynomials. */
 typedef struct
@@ -238,7 +241,7 @@ __contract__(
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API || MLD_UNIT_TEST */
 
-#if !defined(MLD_CONFIG_NO_KEYPAIR_API)
+#if !defined(MLD_CONFIG_NO_KEYPAIR_API) && !defined(MLD_CONFIG_CORE_API_ONLY)
 #define mld_polyveck_unpack_eta_chknorm \
   MLD_NAMESPACE_KL(polyveck_unpack_eta_chknorm)
 /**
@@ -266,7 +269,7 @@ __contract__(
   ensures(return_value == 0 || return_value == 0xFFFFFFFF)
 );
 
-#endif /* !MLD_CONFIG_NO_KEYPAIR_API */
+#endif /* !MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)
 #define mld_polyveck_decompose_pack_w1 \
@@ -315,8 +318,10 @@ __contract__(
 );
 #endif /* !MLD_CONFIG_NO_SIGN_API */
 
-#if !defined(MLD_CONFIG_NO_KEYPAIR_API) || \
-    (!defined(MLD_CONFIG_NO_SIGN_API) &&   \
+#if (!defined(MLD_CONFIG_NO_KEYPAIR_API) &&  \
+     !defined(MLD_CONFIG_CORE_API_ONLY)) ||  \
+    ((!defined(MLD_CONFIG_NO_KEYPAIR_API) || \
+      !defined(MLD_CONFIG_NO_SIGN_API)) &&   \
      (!defined(MLD_CONFIG_REDUCE_RAM) || defined(MLD_UNIT_TEST)))
 #define mld_polyvecl_unpack_eta MLD_NAMESPACE_KL(polyvecl_unpack_eta)
 /**
@@ -335,7 +340,8 @@ __contract__(
   ensures(forall(k1, 0, MLDSA_L,
     array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)))
 );
-#endif /* !MLD_CONFIG_NO_KEYPAIR_API || (!MLD_CONFIG_NO_SIGN_API && \
+#endif /* (!MLD_CONFIG_NO_KEYPAIR_API && !MLD_CONFIG_CORE_API_ONLY) || \
+          ((!MLD_CONFIG_NO_KEYPAIR_API || !MLD_CONFIG_NO_SIGN_API) &&  \
           (!MLD_CONFIG_REDUCE_RAM || MLD_UNIT_TEST)) */
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)

From e2e5cb39e100c60ea76fdd9bc932966be2ddade2 Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Tue, 13 Oct 2026 23:30:57 +0800
Subject: [PATCH 6/7] rv32im: Reject the backend on targets other than RV32
 with M

Selecting the backend through MLD_CONFIG_ARITH_BACKEND_FILE bypassed
the check in native/meta.h; on RV64 it built but computed wrong
results. The CBMC proofs of the C wrappers run on the host and now
define MLD_SYS_RISCV32_M.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 dev/riscv32/fastmul.h                                | 4 ++++
 dev/riscv32/slowmul.h                                | 4 ++++
 mldsa/src/native/rv32im/fastmul.h                    | 4 ++++
 mldsa/src/native/rv32im/slowmul.h                    | 4 ++++
 proofs/cbmc/intt_native_rv32im_fastmul/Makefile      | 1 +
 proofs/cbmc/intt_native_rv32im_slowmul/Makefile      | 1 +
 proofs/cbmc/ntt_native_rv32im_fastmul/Makefile       | 1 +
 proofs/cbmc/ntt_native_rv32im_slowmul/Makefile       | 1 +
 proofs/cbmc/pointwise_native_rv32im_fastmul/Makefile | 1 +
 proofs/cbmc/pointwise_native_rv32im_slowmul/Makefile | 1 +
 10 files changed, 22 insertions(+)

diff --git a/dev/riscv32/fastmul.h b/dev/riscv32/fastmul.h
index 6eb72a3f93..432bf4dc7c 100644
--- a/dev/riscv32/fastmul.h
+++ b/dev/riscv32/fastmul.h
@@ -7,6 +7,10 @@
 #ifndef MLD_DEV_RISCV32_FASTMUL_H
 #define MLD_DEV_RISCV32_FASTMUL_H
 
+#if !defined(MLD_SYS_RISCV32_M)
+#error This backend can only be used on RV32 targets with the M extension.
+#endif
+
 /*
  * Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
  * ILP32D family of ABIs. This is the default arithmetic backend selected by
diff --git a/dev/riscv32/slowmul.h b/dev/riscv32/slowmul.h
index eaae64d793..06fa72a102 100644
--- a/dev/riscv32/slowmul.h
+++ b/dev/riscv32/slowmul.h
@@ -7,6 +7,10 @@
 #ifndef MLD_DEV_RISCV32_SLOWMUL_H
 #define MLD_DEV_RISCV32_SLOWMUL_H
 
+#if !defined(MLD_SYS_RISCV32_M)
+#error This backend can only be used on RV32 targets with the M extension.
+#endif
+
 /*
  * Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
  * ILP32D family of ABIs. Select this profile explicitly through
diff --git a/mldsa/src/native/rv32im/fastmul.h b/mldsa/src/native/rv32im/fastmul.h
index 3b4dad6a08..3925e1144d 100644
--- a/mldsa/src/native/rv32im/fastmul.h
+++ b/mldsa/src/native/rv32im/fastmul.h
@@ -7,6 +7,10 @@
 #ifndef MLD_NATIVE_RV32IM_FASTMUL_H
 #define MLD_NATIVE_RV32IM_FASTMUL_H
 
+#if !defined(MLD_SYS_RISCV32_M)
+#error This backend can only be used on RV32 targets with the M extension.
+#endif
+
 /*
  * Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
  * ILP32D family of ABIs. This is the default arithmetic backend selected by
diff --git a/mldsa/src/native/rv32im/slowmul.h b/mldsa/src/native/rv32im/slowmul.h
index 72d26d1625..9ada6d0f9c 100644
--- a/mldsa/src/native/rv32im/slowmul.h
+++ b/mldsa/src/native/rv32im/slowmul.h
@@ -7,6 +7,10 @@
 #ifndef MLD_NATIVE_RV32IM_SLOWMUL_H
 #define MLD_NATIVE_RV32IM_SLOWMUL_H
 
+#if !defined(MLD_SYS_RISCV32_M)
+#error This backend can only be used on RV32 targets with the M extension.
+#endif
+
 /*
  * Arithmetic backend for the RISC-V RV32-IM ISA and the ILP32, ILP32F, and
  * ILP32D family of ABIs. Select this profile explicitly through
diff --git a/proofs/cbmc/intt_native_rv32im_fastmul/Makefile b/proofs/cbmc/intt_native_rv32im_fastmul/Makefile
index 767dbaecc6..45e256a018 100644
--- a/proofs/cbmc/intt_native_rv32im_fastmul/Makefile
+++ b/proofs/cbmc/intt_native_rv32im_fastmul/Makefile
@@ -8,6 +8,7 @@ HARNESS_FILE = intt_native_rv32im_fastmul_harness
 PROOF_UID = intt_native_rv32im_fastmul
 
 DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+DEFINES += -DMLD_SYS_RISCV32_M
 DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/fastmul.h\""
 DEFINES += -DMLD_CHECK_APIS
 
diff --git a/proofs/cbmc/intt_native_rv32im_slowmul/Makefile b/proofs/cbmc/intt_native_rv32im_slowmul/Makefile
index f7c085a6c0..2d197a26fe 100644
--- a/proofs/cbmc/intt_native_rv32im_slowmul/Makefile
+++ b/proofs/cbmc/intt_native_rv32im_slowmul/Makefile
@@ -8,6 +8,7 @@ HARNESS_FILE = intt_native_rv32im_slowmul_harness
 PROOF_UID = intt_native_rv32im_slowmul
 
 DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+DEFINES += -DMLD_SYS_RISCV32_M
 DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/slowmul.h\""
 DEFINES += -DMLD_CHECK_APIS
 
diff --git a/proofs/cbmc/ntt_native_rv32im_fastmul/Makefile b/proofs/cbmc/ntt_native_rv32im_fastmul/Makefile
index 12515fa957..d86aa9aefb 100644
--- a/proofs/cbmc/ntt_native_rv32im_fastmul/Makefile
+++ b/proofs/cbmc/ntt_native_rv32im_fastmul/Makefile
@@ -8,6 +8,7 @@ HARNESS_FILE = ntt_native_rv32im_fastmul_harness
 PROOF_UID = ntt_native_rv32im_fastmul
 
 DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+DEFINES += -DMLD_SYS_RISCV32_M
 DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/fastmul.h\""
 DEFINES += -DMLD_CHECK_APIS
 
diff --git a/proofs/cbmc/ntt_native_rv32im_slowmul/Makefile b/proofs/cbmc/ntt_native_rv32im_slowmul/Makefile
index c779541010..3ec77a6f25 100644
--- a/proofs/cbmc/ntt_native_rv32im_slowmul/Makefile
+++ b/proofs/cbmc/ntt_native_rv32im_slowmul/Makefile
@@ -8,6 +8,7 @@ HARNESS_FILE = ntt_native_rv32im_slowmul_harness
 PROOF_UID = ntt_native_rv32im_slowmul
 
 DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+DEFINES += -DMLD_SYS_RISCV32_M
 DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/slowmul.h\""
 DEFINES += -DMLD_CHECK_APIS
 
diff --git a/proofs/cbmc/pointwise_native_rv32im_fastmul/Makefile b/proofs/cbmc/pointwise_native_rv32im_fastmul/Makefile
index cc991a4e6d..0c4cd0bdeb 100644
--- a/proofs/cbmc/pointwise_native_rv32im_fastmul/Makefile
+++ b/proofs/cbmc/pointwise_native_rv32im_fastmul/Makefile
@@ -8,6 +8,7 @@ HARNESS_FILE = pointwise_native_rv32im_fastmul_harness
 PROOF_UID = pointwise_native_rv32im_fastmul
 
 DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+DEFINES += -DMLD_SYS_RISCV32_M
 DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/fastmul.h\""
 DEFINES += -DMLD_CHECK_APIS
 
diff --git a/proofs/cbmc/pointwise_native_rv32im_slowmul/Makefile b/proofs/cbmc/pointwise_native_rv32im_slowmul/Makefile
index ca0ff1459a..82f0f90b05 100644
--- a/proofs/cbmc/pointwise_native_rv32im_slowmul/Makefile
+++ b/proofs/cbmc/pointwise_native_rv32im_slowmul/Makefile
@@ -8,6 +8,7 @@ HARNESS_FILE = pointwise_native_rv32im_slowmul_harness
 PROOF_UID = pointwise_native_rv32im_slowmul
 
 DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+DEFINES += -DMLD_SYS_RISCV32_M
 DEFINES += -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/rv32im/slowmul.h\""
 DEFINES += -DMLD_CHECK_APIS
 

From a238db9f39e7042267cb607436a14cf1c48222e8 Mon Sep 17 00:00:00 2001
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
Date: Tue, 13 Oct 2026 19:46:49 +0800
Subject: [PATCH 7/7] armv81m: Check the MVE capability in the x4 Keccak
 backend

A custom capability function could not disable the backend. Check
MLD_SYS_CAP_ARMV81M_MVE in all three entry points so that they fall
back together, as the state is kept bit-interleaved.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
---
 dev/fips202/armv81m/mve.h              | 12 ++++++++++++
 mldsa/src/fips202/native/armv81m/mve.h | 12 ++++++++++++
 2 files changed, 24 insertions(+)

diff --git a/dev/fips202/armv81m/mve.h b/dev/fips202/armv81m/mve.h
index d09310e9ad..f1baa2d32a 100644
--- a/dev/fips202/armv81m/mve.h
+++ b/dev/fips202/armv81m/mve.h
@@ -32,6 +32,10 @@ int mld_keccak_f1600_x4_native_impl(uint64_t *state);
 MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state)
 {
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
   return mld_keccak_f1600_x4_native_impl(state);
 }
 
@@ -44,6 +48,10 @@ static MLD_INLINE int mld_keccakf1600_xor_bytes_x4_native(
     const uint8_t *data2, const uint8_t *data3, unsigned offset,
     unsigned length)
 {
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
   mld_keccak_f1600_x4_state_xor_bytes_asm(state, data0, data1, data2, data3,
                                           offset, length);
   return MLD_NATIVE_FUNC_SUCCESS;
@@ -57,6 +65,10 @@ static MLD_INLINE int mld_keccakf1600_extract_bytes_x4_native(
     uint64_t *state, uint8_t *data0, uint8_t *data1, uint8_t *data2,
     uint8_t *data3, unsigned offset, unsigned length)
 {
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
   mld_keccak_f1600_x4_state_extract_bytes_asm(state, data0, data1, data2, data3,
                                               offset, length);
   return MLD_NATIVE_FUNC_SUCCESS;
diff --git a/mldsa/src/fips202/native/armv81m/mve.h b/mldsa/src/fips202/native/armv81m/mve.h
index e3b87dc75d..4caf0f5b1a 100644
--- a/mldsa/src/fips202/native/armv81m/mve.h
+++ b/mldsa/src/fips202/native/armv81m/mve.h
@@ -32,6 +32,10 @@ int mld_keccak_f1600_x4_native_impl(uint64_t *state);
 MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int mld_keccak_f1600_x4_native(uint64_t *state)
 {
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
   return mld_keccak_f1600_x4_native_impl(state);
 }
 
@@ -44,6 +48,10 @@ static MLD_INLINE int mld_keccakf1600_xor_bytes_x4_native(
     const uint8_t *data2, const uint8_t *data3, unsigned offset,
     unsigned length)
 {
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
   mld_keccak_f1600_x4_state_xor_bytes_asm(state, data0, data1, data2, data3,
                                           offset, length);
   return MLD_NATIVE_FUNC_SUCCESS;
@@ -57,6 +65,10 @@ static MLD_INLINE int mld_keccakf1600_extract_bytes_x4_native(
     uint64_t *state, uint8_t *data0, uint8_t *data1, uint8_t *data2,
     uint8_t *data3, unsigned offset, unsigned length)
 {
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
   mld_keccak_f1600_x4_state_extract_bytes_asm(state, data0, data1, data2, data3,
                                               offset, length);
   return MLD_NATIVE_FUNC_SUCCESS;