pq-code-package · hanno-becker · May 13, 2026
@@ -310,7 +310,10 @@ runs:
           nix-verbose: ${{ inputs.nix-verbose }}
           gh_token: ${{ inputs.gh_token }}
           custom_shell: ${{ inputs.custom_shell }}
-          cflags: "${{ inputs.cflags }} -DMLD_FORCE_RISCV32"
+          # The RV32-IM arithmetic backend is experimental and not picked
+          # up by native/meta.h's defaults; select it explicitly here.
+          # No-op for OPT=0 builds (MLD_CONFIG_ARITH_BACKEND_FILE is unused).
+          cflags: "${{ inputs.cflags }} -DMLD_FORCE_RISCV32 -DMLD_CONFIG_ARITH_BACKEND_FILE=\\\\\\\"native/rv32im/meta.h\\\\\\\""
           ldflags: ${{ inputs.ldflags }}
           cross_prefix: riscv32-unknown-linux-gnu-
           exec_wrapper: qemu-riscv32
@@ -327,4 +330,3 @@ runs:
           rng_fail: ${{ inputs.rng_fail }}
           extra_args: ${{ inputs.extra_args }}
           extra_env: ${{ inputs.extra_env }}
-
@@ -155,8 +155,8 @@ jobs:
           check_namespace: 'false'
       - name: build + test (cross, opt)
         uses: ./.github/actions/multi-functest
-        # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests
-        if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }}
+        # There is no native code yet on PPC64LE or AArch64_be, so no point running opt tests
+        if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'aarch64_be') }}
         with:
           nix-shell: ${{ matrix.target.nix_shell }}
           nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
@@ -165,8 +165,8 @@ jobs:
           opt: 'opt'
       - name: build + test (cross, opt, +debug)
         uses: ./.github/actions/multi-functest
-        # There is no native code yet on PPC64LE, riscv32 or AArch64_be, so no point running opt tests
-        if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'riscv32' && matrix.target.arch != 'aarch64_be') }}
+        # There is no native code yet on PPC64LE or AArch64_be, so no point running opt tests
+        if: ${{ matrix.target.mode != 'native' && (matrix.target.arch != 'ppc64le' && matrix.target.arch != 'aarch64_be') }}
         with:
           nix-shell: ${{ matrix.target.nix_shell }}
           nix-cache: ${{ matrix.target.mode == 'native' && 'false' || 'true' }}
@@ -846,19 +846,19 @@ jobs:
           - system: macos-latest
             nix_cache: 'true'
             nix_shell: 'hol_light-cross-x86_64'
-            extra_args: '--force-cross'
+            extra_args: '--force-cross aarch64 x86_64'
           # TODO: autogen does not yet work on macos15-intel (#1304)
           # - system: macos-15-intel
           #   nix_cache: 'false'
           #   nix_shell: 'ci'
           - system: ubuntu-latest
             nix_shell: 'hol_light-cross-aarch64'
             nix_cache: 'true'
-            extra_args: '--force-cross'
+            extra_args: '--force-cross aarch64 x86_64'
           - system: ubuntu-24.04-arm
             nix_shell: 'hol_light-cross-x86_64'
             nix_cache: 'true'
-            extra_args: '--force-cross'
+            extra_args: '--force-cross aarch64 x86_64'
     runs-on: ${{ matrix.target.system }}
     name: Check object code in HOL-Light proofs
     steps:

@@ -23,7 +23,7 @@ mldsa-native allows developers to support ML-DSA with minimal performance and ma
 
 **Maintainability and Safety:** Memory safety, type safety and absence of various classes of timing leakage are automatically checked on every change, using a combination of static model checking (using CBMC) and dynamic instrumentation (using valgrind). This reduces review and maintenance burden and accelerates safe code delivery. See [Formal Verification](#formal-verification) and [Security](#security).
 
-**Architecture Support:** Native backends are added under a unified interface, minimizing duplicated code and reasoning. mldsa-native comes with backends for AArch64 and x86-64. See [Design](#design).
+**Architecture Support:** Native backends are added under a unified interface, minimizing duplicated code and reasoning. mldsa-native comes with backends for AArch64 and x86-64, and experimental backends for Armv8.1-M and RV32-IM. See [Design](#design).
 
 ## Quickstart for Ubuntu
 
@@ -92,6 +92,7 @@ mldsa-native currently offers the following backends:
 * 64-bit Arm backend (using Neon)
 * 64-bit Intel/AMD backend (using AVX2)
 * 32-bit Armv8.1-M backend (using Helium/MVE). This is still experimental and disabled by default.
+* 32-bit RISC-V backend (RV32-IM, base integer + M-extension only). This is still experimental and disabled by default.
 
 If you'd like contribute new backends, please reach out!
 

@@ -0,0 +1,47 @@
+/*
+ * Copyright (c) The mlkem-native project authors
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+#ifndef MLD_NATIVE_RV32IM_META_H
+#define MLD_NATIVE_RV32IM_META_H
+
+/* Set of primitives that this backend replaces */
+#define MLD_USE_NATIVE_NTT
+#define MLD_USE_NATIVE_INTT
+#define MLD_USE_NATIVE_POINTWISE_MONTGOMERY
+
+/* Identifier for this backend so that source and assembly files
+ * in the build can be appropriately guarded. */
+#define MLD_ARITH_BACKEND_RV32IM
+
+
+#if !defined(__ASSEMBLER__)
+#include "../api.h"
+#include "src/arith_native_rv32im.h"
+
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_ntt_native(int32_t data[MLDSA_N])
+{
+  mld_ntt_rv32im_asm(data, mld_rv32im_ntt_zetas);
+  return MLD_NATIVE_FUNC_SUCCESS;
+}
+
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_intt_native(int32_t data[MLDSA_N])
+{
+  mld_intt_rv32im_asm(data, mld_rv32im_ntt_zetas);
+  return MLD_NATIVE_FUNC_SUCCESS;
+}
+
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_poly_pointwise_montgomery_native(
+    int32_t a[MLDSA_N], const int32_t b[MLDSA_N])
+{
+  mld_poly_pointwise_montgomery_rv32im_asm(a, b);
+  return MLD_NATIVE_FUNC_SUCCESS;
+}
+
+#endif /* !__ASSEMBLER__ */
+#endif /* !MLD_NATIVE_RV32IM_META_H */
@@ -0,0 +1,57 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+#ifndef MLD_NATIVE_RV32IM_SRC_ARITH_NATIVE_RV32IM_H
+#define MLD_NATIVE_RV32IM_SRC_ARITH_NATIVE_RV32IM_H
+
+#include "../../../cbmc.h"
+#include "../../../common.h"
+
+#define mld_rv32im_ntt_zetas MLD_NAMESPACE(rv32im_ntt_zetas)
+
+/*
+ * Forward NTT zeta table for the RV32-IM backend.
+ *
+ * 255 logical entries, each a (zeta, zeta * QINV mod 2^32) pair, with
+ * zeta in Montgomery form (i.e. R * w^{bitrev_8(k)} mod q where R = 2^32).
+ * The order matches the consumption order of the 2+2+2+2 forward NTT.
+ */
+MLD_INTERNAL_DATA_DECLARATION const int32_t mld_rv32im_ntt_zetas[510];
+
+#define mld_ntt_rv32im_asm MLD_NAMESPACE(ntt_rv32im_asm)
+void mld_ntt_rv32im_asm(int32_t *r, const int32_t *zetas)
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
+  requires(zetas == mld_rv32im_ntt_zetas)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_abs_bound(r, 0, MLDSA_N, 9 * MLDSA_Q))
+);
+
+#define mld_intt_rv32im_asm MLD_NAMESPACE(intt_rv32im_asm)
+void mld_intt_rv32im_asm(int32_t *r, const int32_t *zetas)
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
+  requires(zetas == mld_rv32im_ntt_zetas)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
+);
+
+#define mld_poly_pointwise_montgomery_rv32im_asm \
+  MLD_NAMESPACE(poly_pointwise_montgomery_rv32im_asm)
+void mld_poly_pointwise_montgomery_rv32im_asm(int32_t *a, const int32_t *b)
+__contract__(
+  requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
+  /* check-magic: off */
+  requires(array_abs_bound(a, 0, MLDSA_N, 75423753))   /* MLD_NTT_BOUND */
+  requires(array_abs_bound(b, 0, MLDSA_N, 75423753))
+  /* check-magic: on */
+  assigns(memory_slice(a, sizeof(int32_t) * MLDSA_N))
+  ensures(array_abs_bound(a, 0, MLDSA_N, MLDSA_Q))
+);
+
+#endif /* !MLD_NATIVE_RV32IM_SRC_ARITH_NATIVE_RV32IM_H */