Armv8.1-M: add pqmx MVE inverse NTT

BIBLIOGRAPHY.md

@@ -36,6 +36,17 @@ source code and documentation.
 * Referenced from:
   - [README.md](README.md)
 
+### `ADOMNICAI23`
+
+* An update on Keccak performance on ARMv7-M
+* Author(s):
+  - Alexandre Adomnicai
+* URL: https://eprint.iacr.org/2023/773
+* Referenced from:
+  - [dev/fips202/armv81m_clean/src/keccak_f1600_x1_armv81m.S](dev/fips202/armv81m_clean/src/keccak_f1600_x1_armv81m.S)
+  - [dev/fips202/armv81m_opt/src/keccak_f1600_x1_armv7m_opt_m55.S](dev/fips202/armv81m_opt/src/keccak_f1600_x1_armv7m_opt_m55.S)
+  - [mldsa/src/fips202/native/armv81m/src/keccak_f1600_x1_armv7m_opt_m55.S](mldsa/src/fips202/native/armv81m/src/keccak_f1600_x1_armv7m_opt_m55.S)
+
 ### `ArmARMv8M`
 
 * Armv8-M Architecture Reference Manual (DDI 0553)
@@ -371,6 +382,19 @@ source code and documentation.
   - [mldsa/src/sign.c](mldsa/src/sign.c)
   - [proofs/hol_light/README.md](proofs/hol_light/README.md)
 
+### `SLOTHYM7`
+
+* Enabling Microarchitectural Agility: Taking ML-KEM and ML-DSA from Cortex-M4 to M7 with SLOTHY
+* Author(s):
+  - Amin Abdulrahman
+  - Matthias J. Kannwischer
+  - Joel Lim
+* URL: https://eprint.iacr.org/2025/366
+* Referenced from:
+  - [dev/fips202/armv81m_clean/src/keccak_f1600_x1_armv81m.S](dev/fips202/armv81m_clean/src/keccak_f1600_x1_armv81m.S)
+  - [dev/fips202/armv81m_opt/src/keccak_f1600_x1_armv7m_opt_m55.S](dev/fips202/armv81m_opt/src/keccak_f1600_x1_armv7m_opt_m55.S)
+  - [mldsa/src/fips202/native/armv81m/src/keccak_f1600_x1_armv7m_opt_m55.S](mldsa/src/fips202/native/armv81m/src/keccak_f1600_x1_armv7m_opt_m55.S)
+
 ### `SLOTHY_Paper`
 
 * Fast and Clean: Auditable high-performance assembly via constraint solving
@@ -404,6 +428,21 @@ source code and documentation.
   - [test/abicheck/README.md](test/abicheck/README.md)
   - [test/abicheck/x86_64/abicheck_x86_64.c](test/abicheck/x86_64/abicheck_x86_64.c)
 
+### `XKCP`
+
+* eXtended Keccak Code Package
+* Author(s):
+  - Guido Bertoni
+  - Joan Daemen
+  - Michaël Peeters
+  - Gilles Van Assche
+  - Ronny Van Keer
+* URL: https://github.com/XKCP/XKCP
+* Referenced from:
+  - [dev/fips202/armv81m_clean/src/keccak_f1600_x1_armv81m.S](dev/fips202/armv81m_clean/src/keccak_f1600_x1_armv81m.S)
+  - [dev/fips202/armv81m_opt/src/keccak_f1600_x1_armv7m_opt_m55.S](dev/fips202/armv81m_opt/src/keccak_f1600_x1_armv7m_opt_m55.S)
+  - [mldsa/src/fips202/native/armv81m/src/keccak_f1600_x1_armv7m_opt_m55.S](mldsa/src/fips202/native/armv81m/src/keccak_f1600_x1_armv7m_opt_m55.S)
+
 ### `libmceliece`
 
 * libmceliece implementation of Classic McEliece

BIBLIOGRAPHY.yml

@@ -109,6 +109,29 @@
   - Klein, Fabien
   url: https://eprint.iacr.org/2022/1303
 
+- id: ADOMNICAI23
+  name: "An update on Keccak performance on ARMv7-M"
+  author: Adomnicai, Alexandre
+  url: https://eprint.iacr.org/2023/773
+
+- id: SLOTHYM7
+  name: "Enabling Microarchitectural Agility: Taking ML-KEM and ML-DSA from Cortex-M4 to M7 with SLOTHY"
+  author:
+  - Abdulrahman, Amin
+  - Kannwischer, Matthias J.
+  - Lim, Joel
+  url: https://eprint.iacr.org/2025/366
+
+- id: XKCP
+  name: eXtended Keccak Code Package
+  author:
+  - Bertoni, Guido
+  - Daemen, Joan
+  - Peeters, Michaël
+  - Van Assche, Gilles
+  - Van Keer, Ronny
+  url: https://github.com/XKCP/XKCP
+
 - id: NeonNTT
   name: "Neon NTT: Faster Dilithium, Kyber, and Saber on Cortex-A72 and Apple M1"
   year: 2022

LICENSE

@@ -14,11 +14,17 @@ It is only used for testing purposes.
 The benchmarking code in test/hal/hal.c carries the
 MIT license. It is only used for testing purposes.
 
+The Armv8.1-M Keccak implementation contains portions adapted from SLOTHY
+examples distributed under the MIT license. The applicable SLOTHY copyright
+notices are included below.
+
 ```
 Copyright (c) The mldsa-native project authors
 Copyright (c) The mlkem-native project authors
 Copyright (c) 2020 Dougall Johnson
 Copyright (c) 2022 Arm Limited
+Copyright (c) 2022 Hanno Becker
+Copyright (c) 2023 Amin Abdulrahman, Matthias Kannwischer
 SPDX-License-Identifier: MIT
 
 Permission is hereby granted, free of charge, to any person obtaining a copy

dev/armv81m_clean/README.md

@@ -0,0 +1,10 @@
+[//]: # (SPDX-License-Identifier: CC-BY-4.0)
+
+# Armv8.1-M pqmx NTT/iNTT: clean inputs
+
+This directory contains the regular, readable pqmx forward- and inverse-NTT
+inputs for the Cortex-M55. The matching files under `../armv81m_opt/src/` hold
+the selected SLOTHY schedules. The inverse schedule follows pqmx's selected
+output with its temporary whole-buffer reduction passes omitted. See that
+directory's README for provenance, generation commands, and the custom-order
+contract.

dev/armv81m_clean/meta.h

@@ -0,0 +1,105 @@
+/*
+ * 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_ARMV81M_META_H
+#define MLD_NATIVE_ARMV81M_META_H
+
+/* MVE-only backend; otherwise, leave the C NTT selected. */
+#if defined(__ARM_FEATURE_MVE)
+
+/* Identifier for this backend so its assembly is only emitted when selected. */
+#define MLD_ARITH_BACKEND_ARMV81M_PQMX
+#define MLD_USE_NATIVE_NTT_CUSTOM_ORDER
+#define MLD_USE_NATIVE_NTT
+#define MLD_USE_NATIVE_INTT
+
+#if !defined(__ASSEMBLER__)
+#include <stddef.h>
+#include "../../reduce.h"
+#include "../api.h"
+#include "src/arith_native_armv81m.h"
+
+/*
+ * pqmx's forward kernel produces, and its inverse kernel consumes, a 4-by-4
+ * transposed layout in every 16-coefficient block. The transpose is
+ * self-inverse.
+ */
+static MLD_INLINE void mld_armv81m_pqmx_transpose_4x4(int32_t data[MLDSA_N])
+{
+  unsigned int block;
+
+  for (block = 0; block < MLDSA_N; block += 16)
+  {
+    int32_t tmp[16];
+    unsigned int row, col;
+
+    for (row = 0; row < 16; row++)
+    {
+      tmp[row] = data[block + row];
+    }
+    for (row = 0; row < 4; row++)
+    {
+      for (col = 0; col < 4; col++)
+      {
+        data[block + 4 * row + col] = tmp[4 * col + row];
+      }
+    }
+  }
+}
+
+static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t data[MLDSA_N])
+{
+  if (mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    mld_armv81m_pqmx_transpose_4x4(data);
+  }
+}
+
+/*
+ * The plain pqmx iNTT omits ML-DSA's final Montgomery-domain scale. Keep the
+ * existing scalar 41978 = R^2 / 256 (mod q) step separate in this issue.
+ */
+static MLD_INLINE void mld_armv81m_pqmx_intt_tomont_scale(int32_t data[MLDSA_N])
+{
+  /* check-magic: 41978 == pow(2,64-8,MLDSA_Q) */
+  const int32_t f = 41978;
+  unsigned int i;
+
+  for (i = 0; i < MLDSA_N; i++)
+  {
+    data[i] = mld_montgomery_reduce((int64_t)data[i] * f);
+  }
+}
+
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_ntt_native(int32_t data[MLDSA_N])
+{
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
+
+  mld_ntt_armv81m_asm(data);
+  return MLD_NATIVE_FUNC_SUCCESS;
+}
+
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_intt_native(int32_t data[MLDSA_N])
+{
+  if (!mld_sys_check_capability(MLD_SYS_CAP_ARMV81M_MVE))
+  {
+    return MLD_NATIVE_FUNC_FALLBACK;
+  }
+
+  mld_intt_armv81m_asm(data);
+  mld_armv81m_pqmx_intt_tomont_scale(data);
+  return MLD_NATIVE_FUNC_SUCCESS;
+}
+#endif /* !__ASSEMBLER__ */
+
+#endif /* __ARM_FEATURE_MVE */
+
+#endif /* !MLD_NATIVE_ARMV81M_META_H */

dev/armv81m_clean/src/arith_native_armv81m.h

@@ -0,0 +1,33 @@
+/*
+ * 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_ARMV81M_SRC_ARITH_NATIVE_ARMV81M_H
+#define MLD_NATIVE_ARMV81M_SRC_ARITH_NATIVE_ARMV81M_H
+
+#include "../../../cbmc.h"
+#include "../../../common.h"
+
+#define mld_ntt_armv81m_asm MLD_NAMESPACE(ntt_armv81m_asm)
+void mld_ntt_armv81m_asm(int32_t r[MLDSA_N])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_abs_bound(r, 0, MLDSA_N, MLD_NTT_BOUND))
+);
+
+#define mld_intt_armv81m_asm MLD_NAMESPACE(intt_armv81m_asm)
+void mld_intt_armv81m_asm(int32_t r[MLDSA_N])
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(array_abs_bound(r, 0, MLDSA_N, MLDSA_Q))
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  /* The assembly returns the unscaled inverse transform. The wrapper applies
+   * the established 41978 ToMont scale before returning to the frontend. */
+  ensures(array_abs_bound(r, 0, MLDSA_N, MLDSA_N * MLDSA_Q))
+);
+
+#endif /* !MLD_NATIVE_ARMV81M_SRC_ARITH_NATIVE_ARMV81M_H */