Add Zephyr-based test platform for QEMU MPS boards

.github/workflows/all.yml

@@ -108,3 +108,9 @@ jobs:
     needs: [ base ]
     uses: ./.github/workflows/baremetal.yml
     secrets: inherit
+  zephyr:
+    name: Zephyr
+    permissions:
+      contents: 'read'
+    needs: [ base ]
+    uses: ./.github/workflows/zephyr.yml

.github/workflows/baremetal.yml

@@ -16,27 +16,6 @@ jobs:
       fail-fast: false
       matrix:
         target:
-         - runner: ubuntu-latest
-           name: 'M55-AN547'
-           makefile: test/baremetal/platform/m55-an547/platform.mk
-           nix-shell: cross-arm-embedded
-           func: true
-           kat: true
-           acvp: true
-           wycheproof: false
-           alloc: true
-           bench: true
-           opt: all
-         - runner: ubuntu-latest
-           name: 'M33-AN524'
-           makefile: test/baremetal/platform/m33-an524/platform.mk
-           nix-shell: cross-arm-embedded
-           func: true
-           kat: true
-           acvp: true
-           alloc: true
-           bench: true
-           opt: no_opt
          - runner: ubuntu-latest
            name: 'AVR ATmega128RFR2 (modified for 32K RAM)'
            makefile: test/baremetal/platform/avr/platform.mk

.github/workflows/zephyr.yml

@@ -0,0 +1,57 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: Zephyr
+permissions:
+  contents: read
+on:
+  workflow_call:
+  workflow_dispatch:
+
+jobs:
+  zephyr_tests:
+    name: Zephyr tests (${{ matrix.target.board }}, ${{ matrix.target.cpu }})
+    strategy:
+      fail-fast: false
+      matrix:
+        target:
+          - { board: mps2-an385, cpu: Cortex-M3, opt: no_opt }
+          - { board: mps2-an386, cpu: Cortex-M4, opt: no_opt }
+          - { board: mps2-an500, cpu: Cortex-M7, opt: no_opt }
+          - { board: mps2-an521, cpu: Cortex-M33, opt: no_opt }
+          - { board: mps3-an547, cpu: Cortex-M55, opt: all }
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      - name: zephyr build + test
+        uses: ./.github/actions/functest
+        env:
+          EXTRA_MAKEFILE: test/zephyr/platform.mk
+          ZEPHYR_TARGET: ${{ matrix.target.board }}
+        with:
+          nix-shell: zephyr
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          opt: ${{ matrix.target.opt }}
+          func: true
+          kat: true
+          acvp: true
+          wycheproof: false
+          examples: false
+          unit: false
+          stack: false
+          alloc: false
+          rng_fail: false
+          check_namespace: false
+          # Zephyr's CMake selects the target arch; disable the host-arch
+          # auto-detection that would otherwise leak into the forwarded CFLAGS.
+          extra_args: --no-auto
+      # Smoke only: QEMU doesn't model cycle counts (real numbers come from the
+      # FPGA); this just exercises the bench build + run.
+      - name: bench (smoke)
+        env:
+          EXTRA_MAKEFILE: test/zephyr/platform.mk
+          ZEPHYR_TARGET: ${{ matrix.target.board }}
+        run: |
+          opt=${{ matrix.target.opt == 'all' && 'opt' || 'no_opt' }}
+          nix develop .#zephyr --command ./scripts/tests bench --no-auto -c PMU --opt=$opt
+          nix develop .#zephyr --command ./scripts/tests bench --no-auto --components -c PMU --opt=$opt

dev/fips202/armv81m/mve.h

@@ -17,6 +17,7 @@
 
 #if !defined(__ASSEMBLER__)
 #include "../api.h"
+#include "src/fips202_native_armv81m.h"
 
 /*
  * Native x4 permutation
@@ -35,42 +36,27 @@ static MLK_INLINE int mlk_keccak_f1600_x4_native(uint64_t *state)
 /*
  * Native x4 XOR bytes (with on-the-fly bit interleaving)
  */
-#define mlk_keccak_f1600_x4_state_xor_bytes \
-  MLK_NAMESPACE(keccak_f1600_x4_state_xor_bytes_asm)
-void mlk_keccak_f1600_x4_state_xor_bytes(void *state, const uint8_t *data0,
-                                         const uint8_t *data1,
-                                         const uint8_t *data2,
-                                         const uint8_t *data3, unsigned offset,
-                                         unsigned length);
-
 MLK_MUST_CHECK_RETURN_VALUE
 static MLK_INLINE int mlk_keccakf1600_xor_bytes_x4_native(
     uint64_t *state, const uint8_t *data0, const uint8_t *data1,
     const uint8_t *data2, const uint8_t *data3, unsigned offset,
     unsigned length)
 {
-  mlk_keccak_f1600_x4_state_xor_bytes(state, data0, data1, data2, data3, offset,
-                                      length);
+  mlk_keccak_f1600_x4_state_xor_bytes_asm(state, data0, data1, data2, data3,
+                                          offset, length);
   return MLK_NATIVE_FUNC_SUCCESS;
 }
 
 /*
  * Native x4 extract bytes (with on-the-fly bit de-interleaving)
  */
-#define mlk_keccak_f1600_x4_state_extract_bytes \
-  MLK_NAMESPACE(keccak_f1600_x4_state_extract_bytes_asm)
-void mlk_keccak_f1600_x4_state_extract_bytes(void *state, uint8_t *data0,
-                                             uint8_t *data1, uint8_t *data2,
-                                             uint8_t *data3, unsigned offset,
-                                             unsigned length);
-
 MLK_MUST_CHECK_RETURN_VALUE
 static MLK_INLINE int mlk_keccakf1600_extract_bytes_x4_native(
     uint64_t *state, uint8_t *data0, uint8_t *data1, uint8_t *data2,
     uint8_t *data3, unsigned offset, unsigned length)
 {
-  mlk_keccak_f1600_x4_state_extract_bytes(state, data0, data1, data2, data3,
-                                          offset, length);
+  mlk_keccak_f1600_x4_state_extract_bytes_asm(state, data0, data1, data2, data3,
+                                              offset, length);
   return MLK_NATIVE_FUNC_SUCCESS;
 }
 

flake.nix

@@ -148,15 +148,16 @@
               ++ pkgs.lib.optionals pkgs.stdenv.hostPlatform.isAarch64 [ config.packages.toolchain_x86_64 ];
           };
 
-          # arm-none-eabi-gcc + platform files from pqmx
-          devShells.cross-arm-embedded = util.mkShell {
+          # Zephyr build environment (board chosen at make time via EXTRA_MAKEFILE)
+          packages.zephyr = util.zephyr;
+          devShells.zephyr = util.mkShell {
             packages = builtins.attrValues
               {
-                inherit (util) pqmx;
-                inherit (config.packages) linters;
-                inherit (pkgs) gcc-arm-embedded qemu coreutils git;
-              };
+                inherit (util) zephyr;
+                inherit (pkgs) gcc-arm-embedded qemu cmake ninja dtc gperf coreutils git;
+              } ++ [ util.zephyrPythonEnv ];
           };
+
           devShells.cross-aarch64-embedded = util.mkShell {
             packages = builtins.attrValues
               {

mlkem/mlkem_native.c

@@ -508,8 +508,6 @@
 #undef MLK_USE_FIPS202_X4_NATIVE
 #undef MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE
 #undef mlk_keccak_f1600_x4_native_impl
-#undef mlk_keccak_f1600_x4_state_extract_bytes
-#undef mlk_keccak_f1600_x4_state_xor_bytes
 /* mlkem/src/fips202/native/armv81m/src/fips202_native_armv81m.h */
 #undef MLK_FIPS202_NATIVE_ARMV81M_SRC_FIPS202_NATIVE_ARMV81M_H
 #undef mlk_keccak_f1600_x4_mve_asm

mlkem/mlkem_native_asm.S

@@ -532,8 +532,6 @@
 #undef MLK_USE_FIPS202_X4_NATIVE
 #undef MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE
 #undef mlk_keccak_f1600_x4_native_impl
-#undef mlk_keccak_f1600_x4_state_extract_bytes
-#undef mlk_keccak_f1600_x4_state_xor_bytes
 /* mlkem/src/fips202/native/armv81m/src/fips202_native_armv81m.h */
 #undef MLK_FIPS202_NATIVE_ARMV81M_SRC_FIPS202_NATIVE_ARMV81M_H
 #undef mlk_keccak_f1600_x4_mve_asm

mlkem/src/fips202/native/armv81m/mve.h

@@ -17,6 +17,7 @@
 
 #if !defined(__ASSEMBLER__)
 #include "../api.h"
+#include "src/fips202_native_armv81m.h"
 
 /*
  * Native x4 permutation
@@ -35,42 +36,27 @@ static MLK_INLINE int mlk_keccak_f1600_x4_native(uint64_t *state)
 /*
  * Native x4 XOR bytes (with on-the-fly bit interleaving)
  */
-#define mlk_keccak_f1600_x4_state_xor_bytes \
-  MLK_NAMESPACE(keccak_f1600_x4_state_xor_bytes_asm)
-void mlk_keccak_f1600_x4_state_xor_bytes(void *state, const uint8_t *data0,
-                                         const uint8_t *data1,
-                                         const uint8_t *data2,
-                                         const uint8_t *data3, unsigned offset,
-                                         unsigned length);
-
 MLK_MUST_CHECK_RETURN_VALUE
 static MLK_INLINE int mlk_keccakf1600_xor_bytes_x4_native(
     uint64_t *state, const uint8_t *data0, const uint8_t *data1,
     const uint8_t *data2, const uint8_t *data3, unsigned offset,
     unsigned length)
 {
-  mlk_keccak_f1600_x4_state_xor_bytes(state, data0, data1, data2, data3, offset,
-                                      length);
+  mlk_keccak_f1600_x4_state_xor_bytes_asm(state, data0, data1, data2, data3,
+                                          offset, length);
   return MLK_NATIVE_FUNC_SUCCESS;
 }
 
 /*
  * Native x4 extract bytes (with on-the-fly bit de-interleaving)
  */
-#define mlk_keccak_f1600_x4_state_extract_bytes \
-  MLK_NAMESPACE(keccak_f1600_x4_state_extract_bytes_asm)
-void mlk_keccak_f1600_x4_state_extract_bytes(void *state, uint8_t *data0,
-                                             uint8_t *data1, uint8_t *data2,
-                                             uint8_t *data3, unsigned offset,
-                                             unsigned length);
-
 MLK_MUST_CHECK_RETURN_VALUE
 static MLK_INLINE int mlk_keccakf1600_extract_bytes_x4_native(
     uint64_t *state, uint8_t *data0, uint8_t *data1, uint8_t *data2,
     uint8_t *data3, unsigned offset, unsigned length)
 {
-  mlk_keccak_f1600_x4_state_extract_bytes(state, data0, data1, data2, data3,
-                                          offset, length);
+  mlk_keccak_f1600_x4_state_extract_bytes_asm(state, data0, data1, data2, data3,
+                                              offset, length);
   return MLK_NATIVE_FUNC_SUCCESS;
 }
 

nix/util.nix

@@ -107,7 +107,17 @@ rec {
   hol_server = pkgs.callPackage ./hol_light/hol_server.nix { inherit hol_light'; };
   s2n_bignum = pkgs.callPackage ./s2n_bignum { };
   slothy = pkgs.callPackage ./slothy { };
-  pqmx = pkgs.callPackage ./pqmx { };
+  zephyr = pkgs.callPackage ./zephyr { };
+  zephyrPythonEnv = pkgs.python3.withPackages (ps: with ps; [
+    pyelftools
+    pyyaml
+    packaging
+    pykwalify
+    jsonschema
+    anytree
+    intelhex
+    colorama
+  ]);
   avr-toolchain = pkgs.callPackage ./avr { };
 
   # Helper function to build individual cross toolchains

nix/zephyr/default.nix

@@ -0,0 +1,53 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+{ stdenvNoCC
+, fetchFromGitHub
+, gcc-arm-embedded
+, writeText
+}:
+
+# Board-agnostic Zephyr build environment: a pinned Zephyr tree plus the
+# modules needed by the boards we target, exposed via a setup hook so a plain
+# `cmake` build works with no west workspace. CMSIS-6 covers the Cortex-M
+# boards; add further modules here as more boards are wired up.
+let
+  zephyr = fetchFromGitHub {
+    owner = "zephyrproject-rtos";
+    repo = "zephyr";
+    rev = "v4.4.1";
+    hash = "sha256-8bzykJs6fFGiofCxRKh8M9jdXr5R8FM0lAbA28yanGk=";
+  };
+
+  # Revision pinned by the Zephyr v4.4.1 manifest (west.yml).
+  cmsis_6 = fetchFromGitHub {
+    owner = "zephyrproject-rtos";
+    repo = "CMSIS_6";
+    rev = "30a859f44ef8ab4dc8f84b03ed586fd16ccf9d74";
+    hash = "sha256-nTehISN0pu9gnOZMpGaBQ3DFmNxAqAZPGpvbKfEM35o=";
+  };
+in
+stdenvNoCC.mkDerivation {
+  pname = "mlkem-native-zephyr";
+  version = "4.4.1";
+
+  dontUnpack = true;
+
+  installPhase = ''
+    mkdir -p $out
+    ln -s ${zephyr} $out/zephyr
+    ln -s ${cmsis_6} $out/cmsis_6
+  '';
+
+  setupHook = writeText "setup-hook.sh" ''
+    export ZEPHYR_BASE="$1/zephyr"
+    export ZEPHYR_MODULES="$1/cmsis_6"
+    export ZEPHYR_TOOLCHAIN_VARIANT=gnuarmemb
+    export GNUARMEMB_TOOLCHAIN_PATH=${gcc-arm-embedded}
+  '';
+
+  meta = {
+    description = "Pinned Zephyr tree and modules for the Zephyr-based test flows";
+    homepage = "https://www.zephyrproject.org/";
+  };
+}

scripts/lint

@@ -268,7 +268,7 @@ gh_group_end
 
 check-tabs()
 {
-  for file in $(git ls-files -- ":/" ":/!:Makefile" ":/!:**/Makefile" ":/!:**/Makefile.*" ":/!:Makefile.*" ":/!:*.mk" ":/!:*.patch" ":/!:*.S" ":/!:*.inc" ":/!:nix/valgrind/*.txt"); do
+  for file in $(git ls-files -- ":/" ":/!:Makefile" ":/!:**/Makefile" ":/!:**/Makefile.*" ":/!:Makefile.*" ":/!:**/Kconfig" ":/!:*.mk" ":/!:*.patch" ":/!:*.S" ":/!:*.inc" ":/!:nix/valgrind/*.txt"); do
     if [[ ! -L $file ]] && grep -Pq '\t' "$file"; then
       l=$(grep -Pn '\t' "$file" | head -1 | cut -d: -f1)
       echo "$file $l"

test/acvp/acvp_mlkem.c

@@ -192,6 +192,11 @@ static MLK_NOINLINE void acvp_mlkem_keyGen_AFT(
   print_hex("dk", dk, sizeof(dk));
 }
 
+/* Ensure main has a prototype even if re-#define'd, avoiding
+ * -Wmissing-prototypes failure */
+#if defined(main)
+int main(int argc, char *argv[]);
+#endif
 int main(int argc, char *argv[])
 {
   acvp_mode mode;