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

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/importer.sh

@@ -78,22 +78,17 @@ mkdir $SRC
 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.
+# The upstream x86_64 backend is now 100% assembly — every native operation
+# (NTT, INTT, decompose, use_hint, chknorm, polyz_unpack, rej_uniform[_eta],
+# pointwise, caddq) is a verified .S file, with no AVX2 C-intrinsic .c files
+# remaining. The upstream meta.h therefore declares only assembly-backed
+# operations and is suitable as-is, so we copy the whole backend tree
+# verbatim (matching the aarch64 backend below). All imported .S files have
+# verified proofs in s2n-bignum.
 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
+cp $TMP/mldsa/src/native/x86_64/*.h $SRC/native/x86_64
+cp $TMP/mldsa/src/native/x86_64/src/* $SRC/native/x86_64/src
 
 # Copy aarch64 backend
 # Unlike x86_64, the aarch64 backend is 100% assembly — no C-intrinsic .c
@@ -141,12 +136,6 @@ 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 assembly backends to use s2n-bignum macros
 # ================================================================

crypto/fipsmodule/ml_dsa/ml_dsa.c

@@ -92,11 +92,12 @@ int ml_dsa_44_sign(const uint8_t *private_key /* IN */,
   FIPS_service_indicator_lock_state();
   boringssl_ensure_ml_dsa_self_test();
 
-  int ret = mldsa44_signature(sig, sig_len, message, message_len,
+  int ret = mldsa44_signature(sig, message, message_len,
                                ctx_string, ctx_string_len, private_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
+    *sig_len = MLDSA44_SIGNATURE_BYTES;
     FIPS_service_indicator_update_state();
     return 1;
   }
@@ -113,10 +114,11 @@ int ml_dsa_extmu_44_sign(const uint8_t *private_key /* IN */,
 
   // mu_len is ignored - extmu always uses MLDSA_CRHBYTES (64 bytes)
   (void)mu_len;
-  int ret = mldsa44_signature_extmu(sig, sig_len, mu, private_key);
+  int ret = mldsa44_signature_extmu(sig, mu, private_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
+    *sig_len = MLDSA44_SIGNATURE_BYTES;
     FIPS_service_indicator_update_state();
     return 1;
   }
@@ -144,8 +146,11 @@ int ml_dsa_44_sign_internal_no_self_test(const uint8_t *private_key  /* IN */,
                                          const uint8_t *pre          /* IN */,
                                          size_t pre_len              /* IN */,
                                          const uint8_t *rnd          /* IN */) {
-  int ret = mldsa44_signature_internal(sig, sig_len, message, message_len,
+  int ret = mldsa44_signature_internal(sig, message, message_len,
                                         pre, pre_len, rnd, private_key, 0);
+  if (ret == 0) {
+    *sig_len = MLDSA44_SIGNATURE_BYTES;
+  }
   return (ret == 0) ? 1 : 0;
 }
 
@@ -158,8 +163,11 @@ int ml_dsa_extmu_44_sign_internal(const uint8_t *private_key  /* IN */,
                                   size_t pre_len              /* IN */,
                                   const uint8_t *rnd          /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa44_signature_internal(sig, sig_len, mu, mu_len,
+  int ret = mldsa44_signature_internal(sig, mu, mu_len,
                                         pre, pre_len, rnd, private_key, 1);
+  if (ret == 0) {
+    *sig_len = MLDSA44_SIGNATURE_BYTES;
+  }
   return (ret == 0) ? 1 : 0;
 }
 
@@ -173,7 +181,8 @@ int ml_dsa_44_verify(const uint8_t *public_key /* IN */,
   FIPS_service_indicator_lock_state();
   boringssl_ensure_ml_dsa_self_test();
 
-  int ret = mldsa44_verify(sig, sig_len, message, message_len,
+  (void)sig_len;
+  int ret = mldsa44_verify(sig, message, message_len,
                             ctx_string, ctx_string_len, public_key);
 
   FIPS_service_indicator_unlock_state();
@@ -194,7 +203,8 @@ int ml_dsa_extmu_44_verify(const uint8_t *public_key /* IN */,
 
   // mu_len is ignored - extmu always uses MLDSA_CRHBYTES (64 bytes)
   (void)mu_len;
-  int ret = mldsa44_verify_extmu(sig, sig_len, mu, public_key);
+  (void)sig_len;
+  int ret = mldsa44_verify_extmu(sig, mu, public_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
@@ -223,7 +233,8 @@ int ml_dsa_44_verify_internal_no_self_test(const uint8_t *public_key /* IN */,
                                            size_t message_len        /* IN */,
                                            const uint8_t *pre        /* IN */,
                                            size_t pre_len            /* IN */) {
-  int ret = mldsa44_verify_internal(sig, sig_len, message, message_len,
+  (void)sig_len;
+  int ret = mldsa44_verify_internal(sig, message, message_len,
                                      pre, pre_len, public_key, 0);
   return (ret == 0) ? 1 : 0;
 }
@@ -236,7 +247,8 @@ int ml_dsa_extmu_44_verify_internal(const uint8_t *public_key /* IN */,
                                     const uint8_t *pre        /* IN */,
                                     size_t pre_len            /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa44_verify_internal(sig, sig_len, mu, mu_len,
+  (void)sig_len;
+  int ret = mldsa44_verify_internal(sig, mu, mu_len,
                                      pre, pre_len, public_key, 1);
   return (ret == 0) ? 1 : 0;
 }
@@ -296,11 +308,12 @@ int ml_dsa_65_sign(const uint8_t *private_key /* IN */,
   FIPS_service_indicator_lock_state();
   boringssl_ensure_ml_dsa_self_test();
 
-  int ret = mldsa65_signature(sig, sig_len, message, message_len,
+  int ret = mldsa65_signature(sig, message, message_len,
                                ctx_string, ctx_string_len, private_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
+    *sig_len = MLDSA65_SIGNATURE_BYTES;
     FIPS_service_indicator_update_state();
     return 1;
   }
@@ -317,10 +330,11 @@ int ml_dsa_extmu_65_sign(const uint8_t *private_key /* IN */,
 
   // mu_len is ignored - extmu always uses MLDSA_CRHBYTES (64 bytes)
   (void)mu_len;
-  int ret = mldsa65_signature_extmu(sig, sig_len, mu, private_key);
+  int ret = mldsa65_signature_extmu(sig, mu, private_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
+    *sig_len = MLDSA65_SIGNATURE_BYTES;
     FIPS_service_indicator_update_state();
     return 1;
   }
@@ -336,8 +350,11 @@ int ml_dsa_65_sign_internal(const uint8_t *private_key  /* IN */,
                             size_t pre_len              /* IN */,
                             const uint8_t *rnd          /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa65_signature_internal(sig, sig_len, message, message_len,
+  int ret = mldsa65_signature_internal(sig, message, message_len,
                                         pre, pre_len, rnd, private_key, 0);
+  if (ret == 0) {
+    *sig_len = MLDSA65_SIGNATURE_BYTES;
+  }
   return (ret == 0) ? 1 : 0;
 }
 
@@ -350,8 +367,11 @@ int ml_dsa_extmu_65_sign_internal(const uint8_t *private_key  /* IN */,
                                   size_t pre_len              /* IN */,
                                   const uint8_t *rnd          /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa65_signature_internal(sig, sig_len, mu, mu_len,
+  int ret = mldsa65_signature_internal(sig, mu, mu_len,
                                         pre, pre_len, rnd, private_key, 1);
+  if (ret == 0) {
+    *sig_len = MLDSA65_SIGNATURE_BYTES;
+  }
   return (ret == 0) ? 1 : 0;
 }
 
@@ -365,7 +385,8 @@ int ml_dsa_65_verify(const uint8_t *public_key /* IN */,
   FIPS_service_indicator_lock_state();
   boringssl_ensure_ml_dsa_self_test();
 
-  int ret = mldsa65_verify(sig, sig_len, message, message_len,
+  (void)sig_len;
+  int ret = mldsa65_verify(sig, message, message_len,
                             ctx_string, ctx_string_len, public_key);
 
   FIPS_service_indicator_unlock_state();
@@ -386,7 +407,8 @@ int ml_dsa_extmu_65_verify(const uint8_t *public_key /* IN */,
 
   // mu_len is ignored - extmu always uses MLDSA_CRHBYTES (64 bytes)
   (void)mu_len;
-  int ret = mldsa65_verify_extmu(sig, sig_len, mu, public_key);
+  (void)sig_len;
+  int ret = mldsa65_verify_extmu(sig, mu, public_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
@@ -404,7 +426,8 @@ int ml_dsa_65_verify_internal(const uint8_t *public_key /* IN */,
                               const uint8_t *pre        /* IN */,
                               size_t pre_len            /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa65_verify_internal(sig, sig_len, message, message_len,
+  (void)sig_len;
+  int ret = mldsa65_verify_internal(sig, message, message_len,
                                      pre, pre_len, public_key, 0);
   return (ret == 0) ? 1 : 0;
 }
@@ -417,7 +440,8 @@ int ml_dsa_extmu_65_verify_internal(const uint8_t *public_key /* IN */,
                                     const uint8_t *pre        /* IN */,
                                     size_t pre_len            /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa65_verify_internal(sig, sig_len, mu, mu_len,
+  (void)sig_len;
+  int ret = mldsa65_verify_internal(sig, mu, mu_len,
                                      pre, pre_len, public_key, 1);
   return (ret == 0) ? 1 : 0;
 }
@@ -476,11 +500,12 @@ int ml_dsa_87_sign(const uint8_t *private_key /* IN */,
   FIPS_service_indicator_lock_state();
   boringssl_ensure_ml_dsa_self_test();
 
-  int ret = mldsa87_signature(sig, sig_len, message, message_len,
+  int ret = mldsa87_signature(sig, message, message_len,
                                ctx_string, ctx_string_len, private_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
+    *sig_len = MLDSA87_SIGNATURE_BYTES;
     FIPS_service_indicator_update_state();
     return 1;
   }
@@ -497,10 +522,11 @@ int ml_dsa_extmu_87_sign(const uint8_t *private_key /* IN */,
 
   // mu_len is ignored - extmu always uses MLDSA_CRHBYTES (64 bytes)
   (void)mu_len;
-  int ret = mldsa87_signature_extmu(sig, sig_len, mu, private_key);
+  int ret = mldsa87_signature_extmu(sig, mu, private_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
+    *sig_len = MLDSA87_SIGNATURE_BYTES;
     FIPS_service_indicator_update_state();
     return 1;
   }
@@ -516,8 +542,11 @@ int ml_dsa_87_sign_internal(const uint8_t *private_key  /* IN */,
                             size_t pre_len              /* IN */,
                             const uint8_t *rnd          /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa87_signature_internal(sig, sig_len, message, message_len,
+  int ret = mldsa87_signature_internal(sig, message, message_len,
                                         pre, pre_len, rnd, private_key, 0);
+  if (ret == 0) {
+    *sig_len = MLDSA87_SIGNATURE_BYTES;
+  }
   return (ret == 0) ? 1 : 0;
 }
 
@@ -530,8 +559,11 @@ int ml_dsa_extmu_87_sign_internal(const uint8_t *private_key  /* IN */,
                                   size_t pre_len              /* IN */,
                                   const uint8_t *rnd          /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa87_signature_internal(sig, sig_len, mu, mu_len,
+  int ret = mldsa87_signature_internal(sig, mu, mu_len,
                                         pre, pre_len, rnd, private_key, 1);
+  if (ret == 0) {
+    *sig_len = MLDSA87_SIGNATURE_BYTES;
+  }
   return (ret == 0) ? 1 : 0;
 }
 
@@ -545,7 +577,8 @@ int ml_dsa_87_verify(const uint8_t *public_key /* IN */,
   FIPS_service_indicator_lock_state();
   boringssl_ensure_ml_dsa_self_test();
 
-  int ret = mldsa87_verify(sig, sig_len, message, message_len,
+  (void)sig_len;
+  int ret = mldsa87_verify(sig, message, message_len,
                             ctx_string, ctx_string_len, public_key);
 
   FIPS_service_indicator_unlock_state();
@@ -566,7 +599,8 @@ int ml_dsa_extmu_87_verify(const uint8_t *public_key /* IN */,
 
   // mu_len is ignored - extmu always uses MLDSA_CRHBYTES (64 bytes)
   (void)mu_len;
-  int ret = mldsa87_verify_extmu(sig, sig_len, mu, public_key);
+  (void)sig_len;
+  int ret = mldsa87_verify_extmu(sig, mu, public_key);
 
   FIPS_service_indicator_unlock_state();
   if (ret == 0) {
@@ -584,7 +618,8 @@ int ml_dsa_87_verify_internal(const uint8_t *public_key /* IN */,
                               const uint8_t *pre        /* IN */,
                               size_t pre_len            /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa87_verify_internal(sig, sig_len, message, message_len,
+  (void)sig_len;
+  int ret = mldsa87_verify_internal(sig, message, message_len,
                                      pre, pre_len, public_key, 0);
   return (ret == 0) ? 1 : 0;
 }
@@ -597,7 +632,8 @@ int ml_dsa_extmu_87_verify_internal(const uint8_t *public_key /* IN */,
                                     const uint8_t *pre        /* IN */,
                                     size_t pre_len            /* IN */) {
   boringssl_ensure_ml_dsa_self_test();
-  int ret = mldsa87_verify_internal(sig, sig_len, mu, mu_len,
+  (void)sig_len;
+  int ret = mldsa87_verify_internal(sig, mu, mu_len,
                                      pre, pre_len, public_key, 1);
   return (ret == 0) ? 1 : 0;
 }

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)