ML-DSA x86_64: import full assembly backend from mldsa-native

Result of running importer.sh against mldsa-native
1dbd70f78583fab6fbfc46287702d6a09d5ec5e6. Imports the complete x86_64
assembly backend: adds verified .S implementations for poly_chknorm,
poly_decompose_{32,88}, poly_use_hint_{32,88}, polyz_unpack_{17,19},
rej_uniform, and rej_uniform_eta{2,4} (previously AVX2 C intrinsics,
excluded from import), plus the upstream meta.h and rej_uniform_table.c.
The remainder is the corresponding mldsa-native C-source refresh.

Generated by importer.sh; do not edit by hand.

Author: jakemas

crypto/fipsmodule/ml_dsa/META.yml

@@ -1,5 +1,5 @@
 name: mldsa-native
 source: pq-code-package/mldsa-native.git
-branch: 08d40f9403a9ca80f160118bc63e96bf36627866
-commit: 08d40f9403a9ca80f160118bc63e96bf36627866
-imported-at: 2026-06-12T17:04:44+0000
+branch: 1dbd70f78583fab6fbfc46287702d6a09d5ec5e6
+commit: 1dbd70f78583fab6fbfc46287702d6a09d5ec5e6
+imported-at: 2026-07-17T20:21:14+0000

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

@@ -27,3 +27,4 @@ Macros:
  - __loop__(x)={} do
  # Make this artifically long to force line break
  - MLD_INTERNAL_API=void abcdefghijklmnopqrstuvwabcdefghijklmnopqrstuvwabcdefg();
+ - MLD_SYSV_ABI=void abcdefghijklmnopqrstuvwabcdefghijklmnopqrstuvwabcdefg();

crypto/fipsmodule/ml_dsa/mldsa/cbmc.h

@@ -9,17 +9,28 @@
 /***************************************************
  * Basic replacements for __CPROVER_XXX contracts
  ***************************************************/
+/*
+ * The `__contract__` / `__loop__` annotation macros use a
+ * leading-double-underscore spelling in line with other CBMC macros.
+ * clang-tidy flags these as reserved identifiers; we suppress the diagnostic
+ * at each definition site (NOLINT) rather than disabling the check globally,
+ * so it stays active for the rest of the tree.
+ */
 #ifndef CBMC
 
-#define __contract__(x)
-#define __loop__(x)
+/* clang-format off */
+#define __contract__(x) /* NOLINT(bugprone-reserved-identifier,cert-dcl37-c,cert-dcl51-cpp) */
+#define __loop__(x) /* NOLINT(bugprone-reserved-identifier,cert-dcl37-c,cert-dcl51-cpp) */
+/* clang-format on */
 #define cassert(x)
 
 #else /* !CBMC */
 
 
-#define __contract__(x) x
-#define __loop__(x) x
+/* clang-format off */
+#define __contract__(x) x /* NOLINT(bugprone-reserved-identifier,cert-dcl37-c,cert-dcl51-cpp) */
+#define __loop__(x) x /* NOLINT(bugprone-reserved-identifier,cert-dcl37-c,cert-dcl51-cpp) */
+/* clang-format on */
 
 /* Conditionally expand to __VA_ARGS__ depending on MLD_CONFIG_REDUCE_RAM. */
 #if defined(MLD_CONFIG_REDUCE_RAM)

crypto/fipsmodule/ml_dsa/mldsa/common.h

@@ -129,15 +129,15 @@
 #endif
 
 #if defined(MLD_CONFIG_NO_RANDOMIZED_API) && defined(MLD_CONFIG_KEYGEN_PCT)
-#error Bad configuration: MLD_CONFIG_NO_RANDOMIZED_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires crypto_sign_signature()
+#error Bad configuration: MLD_CONFIG_NO_RANDOMIZED_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires 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()
+#error Bad configuration: MLD_CONFIG_NO_SIGN_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires 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()
+#error Bad configuration: MLD_CONFIG_NO_VERIFY_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires verify()
 #endif
 
 #if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
@@ -202,77 +202,31 @@
 #error Bad configuration: MLD_CONFIG_CUSTOM_ALLOC_FREE must be set together with MLD_CUSTOM_ALLOC and MLD_CUSTOM_FREE
 #endif
 
-/*
- * If the integration wants to provide a context parameter for use in
- * platform-specific hooks, then it should define this parameter.
- *
- * The MLD_CONTEXT_PARAMETERS_n macros are intended to be used with macros
- * defining the function names and expand to either pass or discard the context
- * argument as required by the current build.  If there is no context parameter
- * requested then these are removed from the prototypes and from all calls.
- */
-#ifdef MLD_CONFIG_CONTEXT_PARAMETER
-#define MLD_CONTEXT_PARAMETERS_0(context) (context)
-#define MLD_CONTEXT_PARAMETERS_1(arg0, context) (arg0, context)
-#define MLD_CONTEXT_PARAMETERS_2(arg0, arg1, context) (arg0, arg1, context)
-#define MLD_CONTEXT_PARAMETERS_3(arg0, arg1, arg2, context) \
-  (arg0, arg1, arg2, context)
-#define MLD_CONTEXT_PARAMETERS_4(arg0, arg1, arg2, arg3, context) \
-  (arg0, arg1, arg2, arg3, context)
-#define MLD_CONTEXT_PARAMETERS_5(arg0, arg1, arg2, arg3, arg4, context) \
-  (arg0, arg1, arg2, arg3, arg4, context)
-#define MLD_CONTEXT_PARAMETERS_6(arg0, arg1, arg2, arg3, arg4, arg5, context) \
-  (arg0, arg1, arg2, arg3, arg4, arg5, context)
-#define MLD_CONTEXT_PARAMETERS_7(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
-                                 context)                                  \
-  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, context)
-#define MLD_CONTEXT_PARAMETERS_8(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
-                                 arg7, context)                            \
-  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, context)
-#define MLD_CONTEXT_PARAMETERS_9(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
-                                 arg7, arg8, context)                      \
-  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, context)
-#else /* MLD_CONFIG_CONTEXT_PARAMETER */
-#define MLD_CONTEXT_PARAMETERS_0(context) ()
-#define MLD_CONTEXT_PARAMETERS_1(arg0, context) (arg0)
-#define MLD_CONTEXT_PARAMETERS_2(arg0, arg1, context) (arg0, arg1)
-#define MLD_CONTEXT_PARAMETERS_3(arg0, arg1, arg2, context) (arg0, arg1, arg2)
-#define MLD_CONTEXT_PARAMETERS_4(arg0, arg1, arg2, arg3, context) \
-  (arg0, arg1, arg2, arg3)
-#define MLD_CONTEXT_PARAMETERS_5(arg0, arg1, arg2, arg3, arg4, context) \
-  (arg0, arg1, arg2, arg3, arg4)
-#define MLD_CONTEXT_PARAMETERS_6(arg0, arg1, arg2, arg3, arg4, arg5, context) \
-  (arg0, arg1, arg2, arg3, arg4, arg5)
-#define MLD_CONTEXT_PARAMETERS_7(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
-                                 context)                                  \
-  (arg0, arg1, arg2, arg3, arg4, arg5, arg6)
-#define MLD_CONTEXT_PARAMETERS_8(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
-                                 arg7, context)                            \
-  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7)
-#define MLD_CONTEXT_PARAMETERS_9(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
-                                 arg7, arg8, context)                      \
-  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8)
-#endif /* !MLD_CONFIG_CONTEXT_PARAMETER */
-
-#if defined(MLD_CONFIG_CONTEXT_PARAMETER_TYPE) != \
-    defined(MLD_CONFIG_CONTEXT_PARAMETER)
-#error MLD_CONFIG_CONTEXT_PARAMETER_TYPE must be defined if and only if MLD_CONFIG_CONTEXT_PARAMETER is defined
-#endif
+/* Context-parameter machinery (MLD_CONTEXT_PARAMETERS_n and related config
+ * checks). Kept in a separate, level-generic header for readability; included
+ * here so it is available to the allocation macros below and to all consumers
+ * of common.h. */
+#include "context.h"
 
 #if !defined(MLD_CONFIG_CUSTOM_ALLOC_FREE)
 /* Default: stack allocation */
 
+/* This is a declaration macro, not an expression macro: T is a type and v is
+ * a declarator, neither of which can be wrapped in parentheses. The
+ * bugprone-macro-parentheses diagnostic is therefore a false positive here. */
 #define MLD_ALLOC(v, T, N, context) \
   MLD_ALIGN T mld_alloc_##v[N];     \
-  T *v = mld_alloc_##v
+  T *v = mld_alloc_##v /* NOLINT(bugprone-macro-parentheses) */
 
-/* TODO: This leads to a circular dependency between common and ct.h
- * It just works out before we're at the end of the file, but it's still
- * prone to issues in the future. */
-#include "ct.h"
+/* The MLD_FREE macro body references mld_zeroize(), which is declared in
+ * ct.h. We deliberately do NOT include ct.h here: doing so would create a
+ * circular dependency (ct.h includes common.h), and common.h itself never
+ * calls mld_zeroize() -- only the macro expansion does. Each translation
+ * unit that uses MLD_FREE therefore includes ct.h directly. */
 #define MLD_FREE(v, T, N, context)                     \
   do                                                   \
   {                                                    \
+    MLD_CONTEXT_UNUSED(context);                       \
     mld_zeroize(mld_alloc_##v, sizeof(mld_alloc_##v)); \
     (v) = NULL;                                        \
   } while (0)
@@ -305,27 +259,33 @@
 /****************************** Error codes ***********************************/
 
 /* Generic failure condition */
-#define MLD_ERR_FAIL -1
+#define MLD_ERR_FAIL (-1)
 /* An allocation failed. This can only happen if MLD_CONFIG_CUSTOM_ALLOC_FREE
  * is defined and the provided MLD_CUSTOM_ALLOC can fail. */
-#define MLD_ERR_OUT_OF_MEMORY -2
+#define MLD_ERR_OUT_OF_MEMORY (-2)
 /* An rng failure occured. Might be due to insufficient entropy or
  * system misconfiguration. */
-#define MLD_ERR_RNG_FAIL -3
+#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
+#define MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED (-4)
+/* Signing was paused before completing, at the request of a caller-provided
+ * MLD_CONFIG_SIGN_HOOK_ATTEMPT hook (see mldsa_native_config.h). The caller
+ * resumes by re-invoking signing with the same inputs; the attempt hook,
+ * together with MLD_CONFIG_SIGN_HOOK_RESUME, decides where to continue. */
+#define MLD_ERR_SIGNING_PAUSED (-5)
 
 /* Disjunction over the full set of MLD_ERR_XXX failure codes.
  *
  * Intended for use in top-level `ensures` clauses that admit every
  * possible error. Narrower contracts should enumerate only the
  * specific errors they can actually return. */
-#define MLD_ANY_ERROR(err)                                    \
-  ((err) == MLD_ERR_FAIL || (err) == MLD_ERR_OUT_OF_MEMORY || \
-   (err) == MLD_ERR_RNG_FAIL || (err) == MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED)
+#define MLD_ANY_ERROR(err)                                                  \
+  ((err) == MLD_ERR_FAIL || (err) == MLD_ERR_OUT_OF_MEMORY ||               \
+   (err) == MLD_ERR_RNG_FAIL || (err) == MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED || \
+   (err) == MLD_ERR_SIGNING_PAUSED)
 
 
 #endif /* !__ASSEMBLER__ */

crypto/fipsmodule/ml_dsa/mldsa/context.h

@@ -0,0 +1,152 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+#ifndef MLD_CONTEXT_H
+#define MLD_CONTEXT_H
+
+/* This header is included by common.h once the configuration has been pulled
+ * in; it is not meant to be included directly. */
+#if !defined(__ASSEMBLER__)
+
+#include <stdint.h>
+#include "cbmc.h"
+#include "sys.h"
+
+/*
+ * If the integration wants to provide a context parameter for use in
+ * platform-specific hooks, then it should define this parameter.
+ *
+ * The MLD_CONTEXT_PARAMETERS_n macros are intended to be used with macros
+ * defining the function names and expand to either pass or discard the context
+ * argument as required by the current build.  If there is no context parameter
+ * requested then these are removed from the prototypes and from all calls.
+ */
+#ifdef MLD_CONFIG_CONTEXT_PARAMETER
+#define MLD_CONTEXT_PARAMETERS_0(context) (context)
+#define MLD_CONTEXT_PARAMETERS_1(arg0, context) (arg0, context)
+#define MLD_CONTEXT_PARAMETERS_2(arg0, arg1, context) (arg0, arg1, context)
+#define MLD_CONTEXT_PARAMETERS_3(arg0, arg1, arg2, context) \
+  (arg0, arg1, arg2, context)
+#define MLD_CONTEXT_PARAMETERS_4(arg0, arg1, arg2, arg3, context) \
+  (arg0, arg1, arg2, arg3, context)
+#define MLD_CONTEXT_PARAMETERS_5(arg0, arg1, arg2, arg3, arg4, context) \
+  (arg0, arg1, arg2, arg3, arg4, context)
+#define MLD_CONTEXT_PARAMETERS_6(arg0, arg1, arg2, arg3, arg4, arg5, context) \
+  (arg0, arg1, arg2, arg3, arg4, arg5, context)
+#define MLD_CONTEXT_PARAMETERS_7(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
+                                 context)                                  \
+  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, context)
+#define MLD_CONTEXT_PARAMETERS_8(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
+                                 arg7, context)                            \
+  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, context)
+#define MLD_CONTEXT_PARAMETERS_9(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
+                                 arg7, arg8, context)                      \
+  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, context)
+#else /* MLD_CONFIG_CONTEXT_PARAMETER */
+#define MLD_CONTEXT_PARAMETERS_0(context) ()
+#define MLD_CONTEXT_PARAMETERS_1(arg0, context) (arg0)
+#define MLD_CONTEXT_PARAMETERS_2(arg0, arg1, context) (arg0, arg1)
+#define MLD_CONTEXT_PARAMETERS_3(arg0, arg1, arg2, context) (arg0, arg1, arg2)
+#define MLD_CONTEXT_PARAMETERS_4(arg0, arg1, arg2, arg3, context) \
+  (arg0, arg1, arg2, arg3)
+#define MLD_CONTEXT_PARAMETERS_5(arg0, arg1, arg2, arg3, arg4, context) \
+  (arg0, arg1, arg2, arg3, arg4)
+#define MLD_CONTEXT_PARAMETERS_6(arg0, arg1, arg2, arg3, arg4, arg5, context) \
+  (arg0, arg1, arg2, arg3, arg4, arg5)
+#define MLD_CONTEXT_PARAMETERS_7(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
+                                 context)                                  \
+  (arg0, arg1, arg2, arg3, arg4, arg5, arg6)
+#define MLD_CONTEXT_PARAMETERS_8(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
+                                 arg7, context)                            \
+  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7)
+#define MLD_CONTEXT_PARAMETERS_9(arg0, arg1, arg2, arg3, arg4, arg5, arg6, \
+                                 arg7, arg8, context)                      \
+  (arg0, arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8)
+#endif /* !MLD_CONFIG_CONTEXT_PARAMETER */
+
+/* Consume a context parameter carried only for the integration's benefit,
+ * avoiding -Wunused-parameter; expands to nothing when no context is
+ * configured. */
+#if defined(MLD_CONFIG_CONTEXT_PARAMETER)
+#define MLD_CONTEXT_UNUSED(context) ((void)(context))
+#else
+#define MLD_CONTEXT_UNUSED(context) ((void)0)
+#endif
+
+#if defined(MLD_CONFIG_CONTEXT_PARAMETER_TYPE) != \
+    defined(MLD_CONFIG_CONTEXT_PARAMETER)
+#error MLD_CONFIG_CONTEXT_PARAMETER_TYPE must be defined if and only if MLD_CONFIG_CONTEXT_PARAMETER is defined
+#endif
+
+/* The signing hooks tie into the rejection-sampling loop. A pausing attempt
+ * hook only reproduces the uninterrupted signature if the randomness is fixed
+ * across calls, and thus requires the deterministic API.
+ * For now we impose that requirement on all three hooks uniformly: enabling any
+ * of them requires MLD_CONFIG_NO_RANDOMIZED_API. This also rules out
+ * MLD_CONFIG_KEYGEN_PCT (whose PCT needs the randomized signature(), see
+ * common.h).
+ *
+ * A logging-only use (attempt always returns 0; resume/finish merely observe)
+ * would be safe with the randomized API too, but the restriction is applied
+ * uniformly for now. */
+#if (defined(MLD_CONFIG_SIGN_HOOK_RESUME) ||  \
+     defined(MLD_CONFIG_SIGN_HOOK_ATTEMPT) || \
+     defined(MLD_CONFIG_SIGN_HOOK_FINISH)) && \
+    !defined(MLD_CONFIG_NO_RANDOMIZED_API)
+#error Signing hooks (MLD_CONFIG_SIGN_HOOK_RESUME / _ATTEMPT / _FINISH) require MLD_CONFIG_NO_RANDOMIZED_API
+#endif /* (MLD_CONFIG_SIGN_HOOK_RESUME || MLD_CONFIG_SIGN_HOOK_ATTEMPT || \
+          MLD_CONFIG_SIGN_HOOK_FINISH) && !MLD_CONFIG_NO_RANDOMIZED_API */
+
+/* Signing hooks (MLD_CONFIG_SIGN_HOOK_RESUME / _ATTEMPT / _FINISH; documented
+ * in mldsa_native_config.h). The following macros route the call sites to
+ * mld_sign_hook_*, appending or dropping the context argument; each unset hook
+ * uses the dummy below. */
+#define mld_sign_resume mld_sign_hook_resume MLD_CONTEXT_PARAMETERS_0
+#define mld_sign_attempt mld_sign_hook_attempt MLD_CONTEXT_PARAMETERS_1
+#define mld_sign_finish mld_sign_hook_finish MLD_CONTEXT_PARAMETERS_1
+
+/* We don't use mld_sign_resume here because MLD_CONTEXT_PARAMETERS_0 is
+ * unsuitable for function declarations: it misses `void` as the placeholder
+ * argument. */
+#if !defined(MLD_CONFIG_SIGN_HOOK_RESUME)
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE uint16_t mld_sign_hook_resume(
+#if defined(MLD_CONFIG_CONTEXT_PARAMETER)
+    MLD_CONFIG_CONTEXT_PARAMETER_TYPE context
+#else
+    void
+#endif
+)
+__contract__(assigns() ensures(1))
+{
+  MLD_CONTEXT_UNUSED(context);
+  return 0;
+}
+#endif /* !MLD_CONFIG_SIGN_HOOK_RESUME */
+
+#if !defined(MLD_CONFIG_SIGN_HOOK_ATTEMPT)
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_sign_attempt(
+    uint16_t attempt, MLD_CONFIG_CONTEXT_PARAMETER_TYPE context)
+__contract__(assigns() ensures(1))
+{
+  ((void)attempt);
+  MLD_CONTEXT_UNUSED(context);
+  return 0;
+}
+#endif /* !MLD_CONFIG_SIGN_HOOK_ATTEMPT */
+
+#if !defined(MLD_CONFIG_SIGN_HOOK_FINISH)
+static MLD_INLINE void mld_sign_finish(
+    uint16_t attempt, MLD_CONFIG_CONTEXT_PARAMETER_TYPE context)
+__contract__(assigns() ensures(1))
+{
+  ((void)attempt);
+  MLD_CONTEXT_UNUSED(context);
+}
+#endif /* !MLD_CONFIG_SIGN_HOOK_FINISH */
+
+#endif /* !__ASSEMBLER__ */
+
+#endif /* !MLD_CONTEXT_H */

crypto/fipsmodule/ml_dsa/mldsa/ct.h

@@ -230,6 +230,12 @@ static MLD_INLINE uint32_t mld_ct_cmask_nonzero_u32(uint32_t x)
 __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFFFFFFFF)))
 {
   int64_t tmp = mld_value_barrier_i64(-((int64_t)x));
+  /*
+   * PORTABILITY: Right-shift on a signed integer is
+   * implementation-defined for negative left argument.
+   * Here, we assume it's sign-preserving "arithmetic" shift right.
+   * See (C99 6.5.7 (5))
+   */
   tmp >>= 32;
   return mld_cast_int64_to_uint32(tmp);
 }
@@ -259,6 +265,12 @@ __contract__(
 )
 {
   int64_t tmp = mld_value_barrier_i64((int64_t)x);
+  /*
+   * PORTABILITY: Right-shift on a signed integer is
+   * implementation-defined for negative left argument.
+   * Here, we assume it's sign-preserving "arithmetic" shift right.
+   * See (C99 6.5.7 (5))
+   */
   tmp >>= 31;
   return mld_cast_int64_to_uint32(tmp);
 }