ML-DSA: import and enable x86_64 assembly backend from mldsa-native

crypto/fipsmodule/CMakeLists.txt

@@ -397,6 +397,24 @@ if((ARCH STREQUAL "x86_64") AND UNIX AND NOT MY_ASSEMBLER_IS_TOO_OLD_FOR_AVX)
 
 endif()
 
+# mldsa-native assembly files can be compiled on Unix platforms for x86_64 only.
+if((ARCH STREQUAL "x86_64") AND UNIX AND NOT MY_ASSEMBLER_IS_TOO_OLD_FOR_AVX)
+
+  set(MLDSA_NATIVE_DIR "${AWSLC_SOURCE_DIR}/crypto/fipsmodule/ml_dsa")
+
+  # Every .S file in this directory is imported by importer.sh and must be
+  # compiled; glob so that refreshes which add/remove files don't need a
+  # matching edit here. CONFIGURE_DEPENDS makes CMake re-run when the set of
+  # matching files changes.
+  file(GLOB MLDSA_NATIVE_X86_64_ASM_SOURCES CONFIGURE_DEPENDS
+    "${MLDSA_NATIVE_DIR}/mldsa/native/x86_64/src/*.S")
+
+  list(APPEND BCM_ASM_SOURCES ${MLDSA_NATIVE_X86_64_ASM_SOURCES})
+
+  set(S2N_BIGNUM_INCLUDE_DIR "${AWSLC_SOURCE_DIR}/third_party/s2n-bignum/s2n-bignum-imported/include")
+
+endif()
+
 
 if(FIPS_DELOCATE)
   if(FIPS_SHARED)

crypto/fipsmodule/ml_dsa/META.yml

@@ -1,5 +1,5 @@
 name: mldsa-native
 source: pq-code-package/mldsa-native.git
-branch: main
-commit: b61e84f0c73d4ed612ffcaea4282a9d682de3f46
-imported-at: 2026-01-16T13:12:01-0800
+branch: 1b47ba602b3220fb06380840fd516dde4243122e
+commit: 1b47ba602b3220fb06380840fd516dde4243122e
+imported-at: 2026-05-14T03:52:22+0000

crypto/fipsmodule/ml_dsa/importer.sh

@@ -72,22 +72,46 @@ popd
 
 echo "Pull source code from remote repository..."
 
-# Copy mldsa-native source tree -- C source only (no native backends for now)
+# Copy mldsa-native source tree -- C source
 mkdir $SRC
-cp $TMP/mldsa/src/* $SRC
+# Copy only files (not subdirectories like native/ and fips202/)
+find $TMP/mldsa/src -maxdepth 1 -type f -exec cp {} $SRC \;
+
+# Copy x86_64 backend
+# We import all assembly (.S) files and shared headers/constants from the
+# upstream x86_64 backend. The AVX2 C-intrinsic .c files (rej_uniform,
+# decompose, use_hint, chknorm, polyz_unpack) are excluded — their includes
+# are stripped from the BCM below.
+#
+# The upstream meta.h advertises both assembly and C-intrinsic operations.
+# Rather than modify it, we keep a hand-maintained replacement in
+# ../mldsa_x86_64_meta.h (referenced via MLD_CONFIG_ARITH_BACKEND_FILE) that
+# declares only the assembly-backed subset. Upstream meta.h is not copied.
+mkdir -p $SRC/native/x86_64/src
+cp $TMP/mldsa/src/native/api.h $SRC/native
+cp $TMP/mldsa/src/native/x86_64/src/arith_native_x86_64.h $SRC/native/x86_64/src
+cp $TMP/mldsa/src/native/x86_64/src/consts.h $SRC/native/x86_64/src
+cp $TMP/mldsa/src/native/x86_64/src/consts.c $SRC/native/x86_64/src
+# NOTE: all imported .S files must have verified proofs in s2n-bignum.
+cp $TMP/mldsa/src/native/x86_64/src/*.S $SRC/native/x86_64/src
 
 # We use the custom `mldsa_native_config.h`, so can remove the default one
-rm $SRC/config.h
+rm -f $SRC/config.h
 
 # Copy formatting file
 cp $TMP/.clang-format $SRC
 
+# ================================================================
+# Process mldsa_native_bcm.c
+# ================================================================
+
 # Copy and statically simplify BCM file
 # The static simplification is not necessary, but improves readability
 # by removing directives related to the FIPS-202 backend that we provide
 # via our own glue layer.
 unifdef -DMLD_CONFIG_FIPS202_CUSTOM_HEADER                             \
         -UMLD_CONFIG_USE_NATIVE_BACKEND_FIPS202                        \
+        -UMLD_SYS_AARCH64                                              \
         $TMP/mldsa/mldsa_native.c                                      \
         > $SRC/mldsa_native_bcm.c
 
@@ -110,6 +134,40 @@ cp $TMP/mldsa/mldsa_native.h $SRC
 echo "Fixup include paths"
 sed "${SED_I[@]}" 's/#include "src\/\([^"]*\)"/#include "\1"/' $SRC/mldsa_native_bcm.c
 
+# Drop #include directives for the C-intrinsic .c files we did not import.
+# Only consts.c (shared with the assembly backend) is kept.
+echo "Strip C-intrinsic includes from mldsa_native_bcm.c"
+BCM=$SRC/mldsa_native_bcm.c
+sed "${SED_I[@]}" '/^#include "native\/x86_64\/src\/[^"]*\.c"/{/consts\.c/!d;}' "$BCM"
+
+# ================================================================
+# Fixup x86_64 assembly backend to use s2n-bignum macros
+# ================================================================
+
+echo "Fixup x86_64 assembly backend to use s2n-bignum macros"
+for file in $SRC/native/x86_64/src/*.S; do
+  echo "Processing $file"
+  tmp_file=$(mktemp)
+
+  backend_define="MLD_ARITH_BACKEND_X86_64_DEFAULT"
+
+  # Flatten multiline preprocessor directives, then process with unifdef
+  sed -e ':a' -e 'N' -e '$!ba' -e 's/\\\n/ /g' "$file" | \
+    unifdef -D$backend_define -UMLD_CONFIG_MULTILEVEL_NO_SHARED -DMLD_CONFIG_MULTILEVEL_WITH_SHARED > "$tmp_file"
+  mv "$tmp_file" "$file"
+
+  # Replace common.h include and assembly macros
+  s2n_header="_internal_s2n_bignum_x86_att.h"
+  sed "${SED_I[@]}" "s/#include \"\.\.\/\.\.\/\.\.\/common\.h\"/#include \"$s2n_header\"/" "$file"
+
+  func_name=$(grep -o '\.global MLD_ASM_NAMESPACE(\([^)]*\))' "$file" | sed 's/\.global MLD_ASM_NAMESPACE(\([^)]*\))/\1/')
+  if [ -n "$func_name" ]; then
+    sed "${SED_I[@]}" "s/\.global MLD_ASM_NAMESPACE($func_name)/        S2N_BN_SYM_VISIBILITY_DIRECTIVE(mldsa_$func_name)\n        S2N_BN_SYM_PRIVACY_DIRECTIVE(mldsa_$func_name)/" "$file"
+    sed "${SED_I[@]}" "s/MLD_ASM_FN_SYMBOL($func_name)/S2N_BN_SYMBOL(mldsa_$func_name):/" "$file"
+    sed "${SED_I[@]}" "s/MLD_ASM_FN_SIZE($func_name)/S2N_BN_SIZE_DIRECTIVE(mldsa_$func_name)/" "$file"
+  fi
+done
+
 echo "Remove temporary artifacts ..."
 rm -rf $TMP
 

crypto/fipsmodule/ml_dsa/mldsa/.clang-format

@@ -26,4 +26,4 @@ Macros:
  - __contract__(x)={ void a; void b; void c; void d; void e; void f; } void abcdefghijklmnopqrstuvw()
  - __loop__(x)={} do
  # Make this artifically long to force line break
- - MLK_INTERNAL_API=void abcdefghijklmnopqrstuvwabcdefghijklmnopqrstuvwabcdefg();
+ - MLD_INTERNAL_API=void abcdefghijklmnopqrstuvwabcdefghijklmnopqrstuvwabcdefg();

crypto/fipsmodule/ml_dsa/mldsa/cbmc.h

@@ -5,6 +5,7 @@
 
 #ifndef MLD_CBMC_H
 #define MLD_CBMC_H
+
 /***************************************************
  * Basic replacements for __CPROVER_XXX contracts
  ***************************************************/
@@ -16,11 +17,19 @@
 
 #else /* !CBMC */
 
-#include <stdint.h>
 
 #define __contract__(x) x
 #define __loop__(x) x
 
+/* Conditionally expand to __VA_ARGS__ depending on MLD_CONFIG_REDUCE_RAM. */
+#if defined(MLD_CONFIG_REDUCE_RAM)
+#define MLD_IF_REDUCE_RAM(...) __VA_ARGS__
+#define MLD_IF_NOT_REDUCE_RAM(...)
+#else
+#define MLD_IF_REDUCE_RAM(...)
+#define MLD_IF_NOT_REDUCE_RAM(...) __VA_ARGS__
+#endif
+
 /* https://diffblue.github.io/cbmc/contracts-assigns.html */
 #define assigns(...) __CPROVER_assigns(__VA_ARGS__)
 
@@ -97,7 +106,7 @@
     ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate)   \
   }
 
-#define exists(qvar, qvar_lb, qvar_ub, predicate)         \
+#define exists(qvar, qvar_lb, qvar_ub, predicate)               \
   __CPROVER_exists                                              \
   {                                                             \
     unsigned qvar;                                              \
@@ -121,30 +130,30 @@
   {                                                                    \
     unsigned qvar;                                                     \
     ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
-        (((int)(value_lb) <= ((array_var)[(qvar)])) &&		       \
-         (((array_var)[(qvar)]) < (int)(value_ub)))		       \
+        (((int)(value_lb) <= ((array_var)[(qvar)])) &&                 \
+         (((array_var)[(qvar)]) < (int)(value_ub)))                    \
   }
 
 #define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
-  array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb),      \
+  array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb),   \
       (qvar_ub), (array_var), (value_lb), (value_ub))
 
-#define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var)        \
-  __CPROVER_forall                                                     \
-  {                                                                    \
-    unsigned qvar;                                                     \
-    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
+#define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var)                   \
+  __CPROVER_forall                                                                \
+  {                                                                               \
+    unsigned qvar;                                                                \
+    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                               \
     ((array_var)[(qvar)]) == (old(* (int32_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
   }
 
 #define array_unchanged(array_var, N) \
     array_unchanged_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), 0, (N), (array_var))
 
-#define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var)        \
-  __CPROVER_forall                                                     \
-  {                                                                    \
-    unsigned qvar;                                                     \
-    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
+#define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var)                \
+  __CPROVER_forall                                                                 \
+  {                                                                                \
+    unsigned qvar;                                                                 \
+    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                                \
     ((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
   }
 

crypto/fipsmodule/ml_dsa/mldsa/common.h

@@ -6,6 +6,11 @@
 #ifndef MLD_COMMON_H
 #define MLD_COMMON_H
 
+#ifndef __ASSEMBLER__
+#include <stdint.h>
+#endif
+
+
 #define MLD_BUILD_INTERNAL
 
 #if defined(MLD_CONFIG_FILE)
@@ -21,8 +26,12 @@
  * this can be overwritten by the user, e.g. for single-CU builds. */
 #if !defined(MLD_CONFIG_INTERNAL_API_QUALIFIER)
 #define MLD_INTERNAL_API
+#define MLD_INTERNAL_DATA_DECLARATION extern
+#define MLD_INTERNAL_DATA_DEFINITION
 #else
 #define MLD_INTERNAL_API MLD_CONFIG_INTERNAL_API_QUALIFIER
+#define MLD_INTERNAL_DATA_DECLARATION MLD_CONFIG_INTERNAL_API_QUALIFIER
+#define MLD_INTERNAL_DATA_DEFINITION MLD_CONFIG_INTERNAL_API_QUALIFIER
 #endif
 
 #if !defined(MLD_CONFIG_EXTERNAL_API_QUALIFIER)
@@ -77,8 +86,24 @@
  */
 #if defined(MLD_SYS_X86_64)
 #define MLD_ASM_FN_SYMBOL(sym) MLD_ASM_NAMESPACE(sym) : MLD_CET_ENDBR
-#else
+#elif defined(MLD_SYS_ARMV81M_MVE)
+/* clang-format off */
+#define MLD_ASM_FN_SYMBOL(sym) \
+  .type MLD_ASM_NAMESPACE(sym), %function; \
+  MLD_ASM_NAMESPACE(sym) :
+/* clang-format on */
+#else /* !MLD_SYS_X86_64 && MLD_SYS_ARMV81M_MVE */
 #define MLD_ASM_FN_SYMBOL(sym) MLD_ASM_NAMESPACE(sym) :
+#endif /* !MLD_SYS_X86_64 && !MLD_SYS_ARMV81M_MVE */
+
+/*
+ * Output the size of an assembly function.
+ */
+#if defined(__ELF__)
+#define MLD_ASM_FN_SIZE(sym) \
+  .size MLD_ASM_NAMESPACE(sym), .- MLD_ASM_NAMESPACE(sym)
+#else
+#define MLD_ASM_FN_SIZE(sym)
 #endif
 
 /* We aim to simplify the user's life by supporting builds where
@@ -107,6 +132,14 @@
 #error Bad configuration: MLD_CONFIG_NO_RANDOMIZED_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires crypto_sign_signature()
 #endif
 
+#if defined(MLD_CONFIG_NO_SIGN_API) && defined(MLD_CONFIG_KEYGEN_PCT)
+#error Bad configuration: MLD_CONFIG_NO_SIGN_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires crypto_sign_signature()
+#endif
+
+#if defined(MLD_CONFIG_NO_VERIFY_API) && defined(MLD_CONFIG_KEYGEN_PCT)
+#error Bad configuration: MLD_CONFIG_NO_VERIFY_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires crypto_sign_verify()
+#endif
+
 #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
 #include MLD_CONFIG_ARITH_BACKEND_FILE
 /* Include to enforce consistency of API and implementation,
@@ -269,20 +302,6 @@
 
 #endif /* MLD_CONFIG_CUSTOM_ALLOC_FREE */
 
-/*
- * We are facing severe CBMC performance issues when using unions.
- * As a temporary workaround, we use unions only when MLD_CONFIG_REDUCE_RAM is
- * set.
- * TODO: Remove the workaround once
- * https://github.com/diffblue/cbmc/issues/8813
- * is resolved
- */
-#if defined(MLD_CONFIG_REDUCE_RAM)
-#define MLK_UNION_OR_STRUCT union
-#else
-#define MLK_UNION_OR_STRUCT struct
-#endif
-
 /****************************** Error codes ***********************************/
 
 /* Generic failure condition */
@@ -293,6 +312,11 @@
 /* An rng failure occured. Might be due to insufficient entropy or
  * system misconfiguration. */
 #define MLD_ERR_RNG_FAIL -3
+/* The signing rejection-sampling loop exceeded
+ * MLD_CONFIG_MAX_SIGNING_ATTEMPTS iterations without producing a valid
+ * signature. With a FIPS 204 Appendix C compliant bound (>= 814) this
+ * has probability < 2^-256. */
+#define MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED -4
 
 
 #endif /* !__ASSEMBLER__ */