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

crypto/fipsmodule/CMakeLists.txt

@@ -397,6 +397,39 @@ 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
+# and aarch64.
+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((ARCH STREQUAL "aarch64") AND UNIX)
+
+  set(MLDSA_NATIVE_DIR "${AWSLC_SOURCE_DIR}/crypto/fipsmodule/ml_dsa")
+
+  # See x86_64 comment above; same glob-based convention.
+  file(GLOB MLDSA_NATIVE_AARCH64_ASM_SOURCES CONFIGURE_DEPENDS
+    "${MLDSA_NATIVE_DIR}/mldsa/native/aarch64/src/*.S")
+
+  list(APPEND BCM_ASM_SOURCES ${MLDSA_NATIVE_AARCH64_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
+commit: 45ba4b3e87aba0e6681f256a3e5f90e01b0e3af1
+imported-at: 2026-05-05T21:10:53+0000

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 */

crypto/fipsmodule/ml_dsa/mldsa/ct.h

@@ -26,7 +26,6 @@
 #ifndef MLD_CT_H
 #define MLD_CT_H
 
-#include <stdint.h>
 #include "cbmc.h"
 #include "common.h"
 
@@ -83,44 +82,54 @@ extern volatile uint64_t mld_ct_opt_blocker_u64;
  * Its validity relies on the assumption that the global opt-blocker
  * constant mld_ct_opt_blocker_u64 is not modified.
  */
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint64_t mld_ct_get_optblocker_u64(void)
 __contract__(ensures(return_value == 0)) { return mld_ct_opt_blocker_u64; }
 
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int64_t mld_ct_get_optblocker_i64(void)
 __contract__(ensures(return_value == 0)) { return (int64_t)mld_ct_get_optblocker_u64(); }
 
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint32_t mld_ct_get_optblocker_u32(void)
 __contract__(ensures(return_value == 0)) { return (uint32_t)mld_ct_get_optblocker_u64(); }
 
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint8_t mld_ct_get_optblocker_u8(void)
 __contract__(ensures(return_value == 0)) { return (uint8_t)mld_ct_get_optblocker_u64(); }
 
 /* Opt-blocker based implementation of value barriers */
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int64_t mld_value_barrier_i64(int64_t b)
 __contract__(ensures(return_value == b)) { return (b ^ mld_ct_get_optblocker_i64()); }
 
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint32_t mld_value_barrier_u32(uint32_t b)
 __contract__(ensures(return_value == b)) { return (b ^ mld_ct_get_optblocker_u32()); }
 
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint8_t mld_value_barrier_u8(uint8_t b)
 __contract__(ensures(return_value == b)) { return (b ^ mld_ct_get_optblocker_u8()); }
 
 
 #else  /* !MLD_USE_ASM_VALUE_BARRIER */
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int64_t mld_value_barrier_i64(int64_t b)
 __contract__(ensures(return_value == b))
 {
   __asm__ volatile("" : "+r"(b));
   return b;
 }
 
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint32_t mld_value_barrier_u32(uint32_t b)
 __contract__(ensures(return_value == b))
 {
   __asm__ volatile("" : "+r"(b));
   return b;
 }
 
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint8_t mld_value_barrier_u8(uint8_t b)
 __contract__(ensures(return_value == b))
 {
@@ -147,6 +156,7 @@ __contract__(ensures(return_value == b))
  *              - x >= 2^31: returns x - 2^31
  *
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_ALWAYS_INLINE int32_t mld_cast_uint32_to_int32(uint32_t x)
 {
   /*
@@ -172,6 +182,7 @@ static MLD_ALWAYS_INLINE int32_t mld_cast_uint32_to_int32(uint32_t x)
  * Returns:     For int64_t x, the unique y in uint32_t
  *              so that x == y mod 2^32.
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_ALWAYS_INLINE uint32_t mld_cast_int64_to_uint32(int64_t x)
 {
   return (uint32_t)(x & (int64_t)UINT32_MAX);
@@ -185,6 +196,7 @@ static MLD_ALWAYS_INLINE uint32_t mld_cast_int64_to_uint32(int64_t x)
  * Returns:     For int32_t x, the unique y in uint32_t
  *              so that x == y mod 2^32.
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_ALWAYS_INLINE uint32_t mld_cast_int32_to_uint32(int32_t x)
 {
   return mld_cast_int64_to_uint32((int64_t)x);
@@ -203,6 +215,7 @@ static MLD_ALWAYS_INLINE uint32_t mld_cast_int32_to_uint32(int32_t x)
  *
  *
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int32_t mld_ct_sel_int32(int32_t a, int32_t b, uint32_t cond)
 __contract__(
   requires(cond == 0x0 || cond == 0xFFFFFFFF)
@@ -223,6 +236,7 @@ __contract__(
  * Arguments:   uint32_t x: Value to be converted into a mask
  *
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint32_t mld_ct_cmask_nonzero_u32(uint32_t x)
 __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFFFFFFFF)))
 {
@@ -239,6 +253,7 @@ __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFFFFFFFF)))
  * Arguments:   uint8_t x: Value to be converted into a mask
  *
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint8_t mld_ct_cmask_nonzero_u8(uint8_t x)
 __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFF)))
 {
@@ -254,6 +269,7 @@ __contract__(ensures(return_value == ((x == 0) ? 0 : 0xFF)))
  * Arguments:   int32_t x: Value to be converted into a mask
  *
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint32_t mld_ct_cmask_neg_i32(int32_t x)
 __contract__(
   ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0))
@@ -272,6 +288,7 @@ __contract__(
  * Arguments:   int32_t x: Input value
  *
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE int32_t mld_ct_abs_i32(int32_t x)
 __contract__(
   requires(x >= -INT32_MAX)
@@ -294,6 +311,7 @@ __contract__(
  *
  * Returns 0 if the byte arrays are equal, 0xFF otherwise.
  **************************************************/
+MLD_MUST_CHECK_RETURN_VALUE
 static MLD_INLINE uint8_t mld_ct_memcmp(const uint8_t *a, const uint8_t *b,
                                         const size_t len)
 __contract__(
@@ -309,7 +327,8 @@ __contract__(
   for (i = 0; i < len; i++)
   __loop__(
     invariant(i <= len)
-    invariant((r == 0) == (forall(k, 0, i, (a[k] == b[k])))))
+    invariant((r == 0) == (forall(k, 0, i, (a[k] == b[k]))))
+    decreases(len - i))
   {
     r |= a[i] ^ b[i];
     /* s is useless, but prevents the loop from being aborted once r=0xff. */

crypto/fipsmodule/ml_dsa/mldsa/debug.h

@@ -8,7 +8,6 @@
 #include "common.h"
 
 #if defined(MLDSA_DEBUG)
-#include <stdint.h>
 
 /*************************************************
  * Name:        mld_assert
@@ -91,14 +90,14 @@ void mld_debug_check_bounds(const char *file, int line, const int32_t *ptr,
 
 /* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
  * just use a single flattened array_bound(...) here. */
-#define mld_assert_bound_2d(ptr, M, N, value_lb, value_ub)             \
-  cassert(forall(kN, 0, (M),                                           \
-                 array_bound(&((int32_t(*)[(N)])(ptr))[kN][0], 0, (N), \
+#define mld_assert_bound_2d(ptr, M, N, value_lb, value_ub)              \
+  cassert(forall(kN, 0, (M),                                            \
+                 array_bound(&((int32_t (*)[(N)])(ptr))[kN][0], 0, (N), \
                              (value_lb), (value_ub))))
 
-#define mld_assert_abs_bound_2d(ptr, M, N, value_abs_bd)                   \
-  cassert(forall(kN, 0, (M),                                               \
-                 array_abs_bound(&((int32_t(*)[(N)])(ptr))[kN][0], 0, (N), \
+#define mld_assert_abs_bound_2d(ptr, M, N, value_abs_bd)                    \
+  cassert(forall(kN, 0, (M),                                                \
+                 array_abs_bound(&((int32_t (*)[(N)])(ptr))[kN][0], 0, (N), \
                                  (value_abs_bd))))
 
 #else /* !MLDSA_DEBUG && CBMC */