Add ABI checker for AArch64, x86_64 (SysV), PowerPC64, Armv8.1-M+MVE

Verify that each assembly kernel preserves the callee-saved registers
its platform calling convention requires:

- AArch64 (AAPCS64):   x19-x28, x29/FP, lower 64 bits of d8-d15.
- x86_64 (System V):   rbx, rbp, r12-r15. No SIMD register callee-saved.
- PowerPC64 (ELFv2):   GPRs r14-r31, FPRs f14-f31, VRs v20-v31, CR2-CR4.
- Armv8.1-M (AAPCS32): r4-r11 plus MVE Q4-Q7 (= D8-D15).

A per-arch assembly call stub loads a random register state, calls the
kernel, and captures the result; a checker then confirms the callee-saved
set is intact. Pointer arguments are backed by correctly-sized buffers
whose layout comes from a per-kernel YAML block; scripts/autogen turns
that YAML into the per-kernel checks. A self-test of hand-written
corrupters confirms the checker actually fires before kernel verdicts
are trusted.

Run via `make run_abicheck` or `scripts/tests abicheck`. It needs no
library build, so `scripts/tests all` runs it by default.

See test/abicheck/README.md for details.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

.github/mlc_config.json

@@ -20,7 +20,12 @@
       "pattern": "^http://nvlpubs\\.nist\\.gov"
     },
     {
+      "_comment": "IACR ePrint rate-limits / 403s automated link-checks.",
       "pattern": "^https://eprint\\.iacr\\.org"
+    },
+    {
+      "_comment": "Armv8-M Architecture Reference Manual; the Arm developer site rate-limits / 403s automated link-checks.",
+      "pattern": "^https://developer\\.arm\\.com"
     }
   ]
 }

BIBLIOGRAPHY.md

@@ -7,6 +7,26 @@
 This file lists the citations made throughout the mlkem-native 
 source code and documentation.
 
+### `AAPCS32`
+
+* Procedure Call Standard for the Arm Architecture (AAPCS32)
+* Author(s):
+  - Arm Limited
+* URL: https://github.com/ARM-software/abi-aa/blob/main/aapcs32/aapcs32.rst
+* Referenced from:
+  - [test/abicheck/README.md](test/abicheck/README.md)
+  - [test/abicheck/armv81m/abicheck_armv81m.c](test/abicheck/armv81m/abicheck_armv81m.c)
+
+### `AAPCS64`
+
+* Procedure Call Standard for the Arm 64-bit Architecture (AAPCS64)
+* Author(s):
+  - Arm Limited
+* URL: https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst
+* Referenced from:
+  - [test/abicheck/README.md](test/abicheck/README.md)
+  - [test/abicheck/aarch64/abicheck_aarch64.c](test/abicheck/aarch64/abicheck_aarch64.c)
+
 ### `ACVP`
 
 * Automated Cryptographic Validation Protocol (ACVP) Server
@@ -30,6 +50,16 @@ source code and documentation.
   - [proofs/hol_light/x86_64/mlkem/intt_avx2_asm.S](proofs/hol_light/x86_64/mlkem/intt_avx2_asm.S)
   - [proofs/hol_light/x86_64/mlkem/ntt_avx2_asm.S](proofs/hol_light/x86_64/mlkem/ntt_avx2_asm.S)
 
+### `ArmARMv8M`
+
+* Armv8-M Architecture Reference Manual (DDI 0553)
+* Author(s):
+  - Arm Limited
+* URL: https://developer.arm.com/documentation/ddi0553/latest/
+* Referenced from:
+  - [test/abicheck/README.md](test/abicheck/README.md)
+  - [test/abicheck/armv81m/abicheck_armv81m.c](test/abicheck/armv81m/abicheck_armv81m.c)
+
 ### `CBMC`
 
 * C Bounded Model Checker
@@ -249,6 +279,16 @@ source code and documentation.
   - [proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.S)
   - [proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.S)
 
+### `PPC64ELFv2`
+
+* 64-Bit ELFv2 ABI Specification — Power Architecture
+* Author(s):
+  - OpenPOWER Foundation
+* URL: https://openpowerfoundation.org/specifications/64bitelfabi/
+* Referenced from:
+  - [test/abicheck/README.md](test/abicheck/README.md)
+  - [test/abicheck/ppc64le/abicheck_ppc64le.c](test/abicheck/ppc64le/abicheck_ppc64le.c)
+
 ### `REF`
 
 * CRYSTALS-Kyber C reference implementation
@@ -375,6 +415,19 @@ source code and documentation.
   - [proofs/hol_light/aarch64/mlkem/intt_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/intt_aarch64_asm.S)
   - [proofs/hol_light/aarch64/mlkem/ntt_aarch64_asm.S](proofs/hol_light/aarch64/mlkem/ntt_aarch64_asm.S)
 
+### `SysVAMD64`
+
+* System V Application Binary Interface — AMD64 Architecture Processor Supplement
+* Author(s):
+  - Michael Matz
+  - Jan Hubička
+  - Andreas Jaeger
+  - Mark Mitchell
+* URL: https://gitlab.com/x86-psABIs/x86-64-ABI
+* Referenced from:
+  - [test/abicheck/README.md](test/abicheck/README.md)
+  - [test/abicheck/x86_64/abicheck_x86_64.c](test/abicheck/x86_64/abicheck_x86_64.c)
+
 ### `clangover`
 
 * clangover

BIBLIOGRAPHY.yml

@@ -206,3 +206,37 @@
   name: tiny_sha3
   author: Saarinen, Markku-Juhani O.
   url: https://github.com/mjosaarinen/tiny_sha3
+
+- id: AAPCS64
+  short: AAPCS64
+  name: "Procedure Call Standard for the Arm 64-bit Architecture (AAPCS64)"
+  author: Arm Limited
+  url: https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst
+
+- id: AAPCS32
+  short: AAPCS32
+  name: "Procedure Call Standard for the Arm Architecture (AAPCS32)"
+  author: Arm Limited
+  url: https://github.com/ARM-software/abi-aa/blob/main/aapcs32/aapcs32.rst
+
+- id: SysVAMD64
+  short: System V AMD64 psABI
+  name: "System V Application Binary Interface — AMD64 Architecture Processor Supplement"
+  author:
+  - Matz, Michael
+  - Hubička, Jan
+  - Jaeger, Andreas
+  - Mitchell, Mark
+  url: https://gitlab.com/x86-psABIs/x86-64-ABI
+
+- id: PPC64ELFv2
+  short: PPC64 ELFv2
+  name: "64-Bit ELFv2 ABI Specification — Power Architecture"
+  author: OpenPOWER Foundation
+  url: https://openpowerfoundation.org/specifications/64bitelfabi/
+
+- id: ArmARMv8M
+  short: Armv8-M ARM
+  name: "Armv8-M Architecture Reference Manual (DDI 0553)"
+  author: Arm Limited
+  url: https://developer.arm.com/documentation/ddi0553/latest/

Makefile

@@ -17,7 +17,7 @@
 	clean quickcheck check-defined-CYCLES \
 	size_512 size_768 size_1024 size \
 	run_size_512 run_size_768 run_size_1024 run_size \
-	host_info
+	host_info abicheck run_abicheck
 
 SHELL := /usr/bin/env bash
 .DEFAULT_GOAL := build
@@ -46,7 +46,7 @@ quickcheck: test
 build: func kat acvp wycheproof
 	$(Q)echo "  Everything builds fine!"
 
-test: run_kat run_func run_acvp run_wycheproof run_unit run_alloc run_rng_fail
+test: run_kat run_func run_acvp run_wycheproof run_unit run_alloc run_rng_fail run_abicheck
 	$(Q)echo "  Everything checks fine!"
 
 run_kat_512: kat_512
@@ -245,6 +245,21 @@ run_size: \
 	run_size_768 \
 	run_size_1024
 
+# OPT=0: no-op (native asm only built with OPT=1).
+# Per-arch gating lives in the sources; x86_64 is also gated on
+# MLK_SYSV_ABI_SUPPORTED because the call stub is hand-written SysV asm.
+# Unsupported targets get an empty registry and exit success, so this builds
+# and runs cleanly on every arch (e.g. riscv64) with no explicit allowlist.
+ifeq ($(OPT),1)
+abicheck: $(ABICHECK_DIR)/bin/abicheck
+
+run_abicheck: abicheck
+	$(W) $(ABICHECK_DIR)/bin/abicheck
+else
+abicheck:
+run_abicheck:
+endif
+
 # Display host and compiler feature detection information
 # Shows which architectural features are supported by both the compiler and host CPU
 # Usage: make host_info [AUTO=0|1] [CROSS_PREFIX=...]

dev/aarch64_clean/src/intt_aarch64_asm.S

@@ -24,6 +24,8 @@
   Description: AArch64 ML-KEM inverse NTT following @[NeonNTT] and @[SLOTHY_Paper]
   Signature: void mlk_intt_aarch64_asm(int16_t p[256], const int16_t twiddles12345[80], const int16_t twiddles56[384])
   ABI:
+    Architecture: aarch64
+    CallingConvention: AAPCS64
     x0:
       type: buffer
       size_bytes: 512

dev/aarch64_clean/src/ntt_aarch64_asm.S

@@ -24,6 +24,8 @@
   Description: AArch64 ML-KEM forward NTT following @[NeonNTT] and @[SLOTHY_Paper]
   Signature: void mlk_ntt_aarch64_asm(int16_t p[256], const int16_t twiddles12345[80], const int16_t twiddles56[384])
   ABI:
+    Architecture: aarch64
+    CallingConvention: AAPCS64
     x0:
       type: buffer
       size_bytes: 512

dev/aarch64_clean/src/poly_mulcache_compute_aarch64_asm.S

@@ -8,6 +8,8 @@
   Description: Compute multiplication cache for polynomial
   Signature: void mlk_poly_mulcache_compute_aarch64_asm(int16_t cache[128], const int16_t mlk_poly[256], const int16_t zetas[128], const int16_t zetas_twisted[128])
   ABI:
+    Architecture: aarch64
+    CallingConvention: AAPCS64
     x0:
       type: buffer
       size_bytes: 256

dev/aarch64_clean/src/poly_reduce_aarch64_asm.S

@@ -8,6 +8,8 @@
   Description: Barrett reduction of polynomial coefficients
   Signature: void mlk_poly_reduce_aarch64_asm(int16_t p[256])
   ABI:
+    Architecture: aarch64
+    CallingConvention: AAPCS64
     x0:
       type: buffer
       size_bytes: 512

dev/aarch64_clean/src/poly_tobytes_aarch64_asm.S

@@ -8,6 +8,8 @@
   Description: Convert polynomial to byte representation
   Signature: void mlk_poly_tobytes_aarch64_asm(uint8_t r[384], const int16_t a[256])
   ABI:
+    Architecture: aarch64
+    CallingConvention: AAPCS64
     x0:
       type: buffer
       size_bytes: 384

dev/aarch64_clean/src/poly_tomont_aarch64_asm.S

@@ -8,6 +8,8 @@
   Description: Convert polynomial to Montgomery domain
   Signature: void mlk_poly_tomont_aarch64_asm(int16_t p[256])
   ABI:
+    Architecture: aarch64
+    CallingConvention: AAPCS64
     x0:
       type: buffer
       size_bytes: 512