Skip to content

abicheck: Use the native build's CPU feature flags - #1945

Open
hanno-becker wants to merge 3 commits into
mainfrom
abicheck-cflags
Open

abicheck: Use the native build's CPU feature flags#1945
hanno-becker wants to merge 3 commits into
mainfrom
abicheck-cflags

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor 
The ABI checker previously added its own CPU feature flags to assembly
objects instead of using those supplied by the test environment through
user CFLAGS or `auto.mk`.

These flags could not simply be removed while the PPC64 ABI checks
were guarded only by the target architecture: the checks could refer
to kernels omitted by the build. The previous commit aligned PPC64
backend selection, ABI checks, registry, call stub and self-test using
`MLK_SYS_PPC64LE_POWER8_VECTOR`.

This commit replaces the per-object CPU flags with source filters in
the generated `abicheck_<arch>.mk` files. Probe compiler macros using
the build's CFLAGS and `abicheck_common.h`, and omit files if a required
capability guard is absent. Use the same guards as the generated C
checks, replacing the separate SHA3 filter based on
`MK_COMPILER_SUPPORTS_SHA3`.

Retain the per-file feature lists and `aux_files` metadata, including
MVE helpers, call stubs and self-tests. The generator removes the CPU
flag metadata and object-list rules, and emits source filters instead.

Keep `ABICHECK_ASM_CFLAGS` and the full API flags so compatible kernel
variants are checked independently of library backend selection.
Guard the C self-test dispatch with `__ARM_FEATURE_MVE`, since
Armv8.1-M targets can disable MVE and omit the matching stubs.

@hanno-becker
hanno-becker requested a review from a team as a code owner October 19, 2026 19:23
@hanno-becker hanno-becker added enhancement New feature or request testing labels Oct 19, 2026
@hanno-becker
hanno-becker marked this pull request as draft October 19, 2026 20:04
@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2053s 1614s +27.2%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 321s 9s +3467%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 161s 57s +182%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2053s 1614s +27.2%
intt_native_aarch64 LP64 z3* ✅ 3s 2s +50%
intt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 16s 16s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 1s +200%
kem_check_pk LP64 z3* ✅ 4s 4s +0%
kem_check_sk LP64 z3* ✅ 3s 2s +50%
kem_dec LP64 z3* ✅ 9s 5s +80%
kem_enc LP64 z3* ✅ 5s 2s +150%
kem_enc_derand LP64 z3* ✅ 2s 3s -33%
kem_keypair LP64 z3* ✅ 2s 4s -50%
kem_keypair_derand LP64 z3* ✅ 1s 3s -67%
mlk_barrett_reduce LP64 z3* ✅ 3s 2s +50%
mlk_check_pct LP64 bitwuzla* ✅ 2s 5s -60%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 3s 2s +50%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 1s +100%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 1s 3s -67%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 4s 2s +100%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 2s 2s +0%
LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3 ✅ 3s 2s +50%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 1s +100%
mlk_ct_sel_uint8 LP64 z3* ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_fqmul LP64 z3* ✅ 3s 17s -82%
mlk_gen_matrix LP64 z3* ✅ 3s 2s +50%
mlk_gen_matrix_serial LP64 z3* ✅ 4s 3s +33%
mlk_indcpa_dec LP64 z3* ✅ 18s 14s +29%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 343s 255s +35%
mlk_indcpa_keypair_derand LP64 z3* ✅ 240s 213s +13%
mlk_invntt_layer LP64 z3* ✅ 5s 4s +25%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 4s 3s +33%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 5s +40%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 8s -12%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 10s 9s +11%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 27s 26s +4%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 3s 5s -40%
mlk_keccakf1600_permute LP64 z3* ✅ 3s 1s +200%
mlk_keccakf1600_permute_c LP64 z3* ✅ 4s 5s -20%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 4s 2s +100%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 z3* ✅ 3s 4s -25%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 3s 1s +200%
mlk_matvec_mul LP64 z3* ✅ 2s 3s -33%
mlk_montgomery_reduce LP64 z3* ✅ 2s 2s +0%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 321s 9s +3467%
mlk_ntt_layer LP64 z3* ✅ 9s 32s -72%
mlk_poly_add LP64 z3* ✅ 3s 4s -25%
mlk_poly_cbd_eta1 LP64 z3* ✅ 3s 2s +50%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 1s 4s -75%
mlk_poly_compress_d10_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d11_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d4_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d5_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_du LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d10_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 14s 15s -7%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_decompress_d11_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 7s -71%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 14s 14s +0%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d5_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_frombytes_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 12s 8s +50%
mlk_poly_frommsg LP64 z3* ✅ 2s 10s -80%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 1s 3s -67%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 4s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 3s 5s -40%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 2s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_poly_invntt_tomont LP64 z3* ✅ 2s 2s +0%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 5s 3s +67%
mlk_poly_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 2s 2s +0%
mlk_poly_ntt LP64 bitwuzla* ✅ 6s 5s +20%
mlk_poly_ntt_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_reduce LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_reduce_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 37s 35s +6%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 36s 150s -76%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 5s 8s -38%
mlk_poly_sub LP64 z3* ✅ 7s 6s +17%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_tobytes_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_tomont LP64 z3* ✅ 4s 1s +300%
mlk_poly_tomont_c LP64 z3* ✅ 5s 2s +150%
mlk_poly_tomont_native LP64 z3* ✅ 4s 2s +100%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 1s 2s -50%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 31s - new
mlk_polyvec_add LP64 z3* ✅ 12s 11s +9%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ✅ 71s 55s +29%
mlk_polyvec_compress_du LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_decompress_du LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 3s 3s +0%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 2s 5s -60%
mlk_polyvec_ntt LP64 z3* ✅ 5s 1s +400%
mlk_polyvec_reduce LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 z3* ✅ 3s 3s +0%
mlk_polyvec_tomont LP64 z3* ✅ 5s 1s +400%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 5s -60%
mlk_rej_uniform_c LP64 z3* ✅ 162s 135s +20%
mlk_scalar_compress_d1 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d11 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_compress_d4 LP64 z3* ✅ 3s 1s +200%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 4s 3s +33%
mlk_scalar_decompress_d5 LP64 z3* ✅ 1s 3s -67%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 1s 1s +0%
mlk_sha3_256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_sha3_512 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 1s 3s -67%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake256x4 LP64 bitwuzla* ✅ 4s 5s -20%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 3s 4s -25%
ntt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
ntt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 1s +100%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 6s 9s -33%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 1s +100%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 4s 4s +0%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 6s 5s +20%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 5s 1s +400%
poly_ntt_native LP64 z3* ✅ 2s 45s -96%
poly_reduce_native_aarch64 LP64 z3* ✅ 1s 1s +0%
poly_reduce_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_tobytes_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_tobytes_native_x86_64 LP64 z3* ✅ 3s 1s +200%
poly_tomont_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_tomont_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 4s 3s +33%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 10s 8s +25%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
rej_uniform_native_aarch64 LP64 z3* ✅ 52s 43s +21%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 161s 57s +182%
sys_check_capability LP64 z3* ✅ 2s 1s +100%

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
mlk_ntt_butterfly_block LP64 z3* ⚠️ 264s 9s +2833%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 124s 79s +57%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 106s 67s +58%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2063s 1885s +9.4%
intt_native_aarch64 LP64 z3* ✅ 4s 3s +33%
intt_native_x86_64 LP64 z3* ✅ 4s 2s +100%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 4s 1s +300%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 16s 15s +7%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
kem_check_pk LP64 z3* ✅ 2s 4s -50%
kem_check_sk LP64 z3* ✅ 1s 3s -67%
kem_dec LP64 z3* ✅ 8s 5s +60%
kem_enc LP64 z3* ✅ 3s 2s +50%
kem_enc_derand LP64 z3* ✅ 2s 3s -33%
kem_keypair LP64 z3* ✅ 1s 2s -50%
kem_keypair_derand LP64 z3* ✅ 3s 1s +200%
mlk_barrett_reduce LP64 z3* ✅ 1s 2s -50%
mlk_check_pct LP64 bitwuzla* ✅ 5s 1s +400%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 1s +0%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 1s 3s -67%
ILP32 cvc5_arrays_exp ✅ 3s 3s +0%
ILP32 z3 ✅ 1s 3s -67%
LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3 ✅ 4s 3s +33%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_sel_int16 LP64 z3* ✅ 1s 4s -75%
mlk_ct_sel_uint8 LP64 z3* ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 2s 4s -50%
mlk_fqmul LP64 z3* ✅ 5s 20s -75%
mlk_gen_matrix LP64 z3* ✅ 5s 2s +150%
mlk_gen_matrix_serial LP64 z3* ✅ 5s 4s +25%
mlk_indcpa_dec LP64 z3* ✅ 14s 11s +27%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 433s 402s +8%
mlk_indcpa_keypair_derand LP64 z3* ✅ 167s 176s -5%
mlk_invntt_layer LP64 z3* ✅ 5s 6s -17%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 6s 4s +50%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 5s +40%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 10s -30%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 7s 9s -22%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 24s 26s -8%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_permute LP64 z3* ✅ 1s 2s -50%
mlk_keccakf1600_permute_c LP64 z3* ✅ 6s 6s +0%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 z3* ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 5s -60%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 1s 5s -80%
mlk_matvec_mul LP64 z3* ✅ 3s 5s -40%
mlk_montgomery_reduce LP64 z3* ✅ 1s 2s -50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 264s 9s +2833%
mlk_ntt_layer LP64 z3* ✅ 8s 38s -79%
mlk_poly_add LP64 z3* ✅ 4s 5s -20%
mlk_poly_cbd_eta1 LP64 z3* ✅ 1s 3s -67%
mlk_poly_cbd_eta2 LP64 z3* ✅ 3s 3s +0%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d10_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 3s 5s -40%
mlk_poly_compress_d5_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 4s -50%
mlk_poly_compress_du LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_d10_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d11_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 15s 16s -6%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d5_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 16s 18s -11%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 5s 3s +67%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 10s 10s +0%
mlk_poly_frommsg LP64 z3* ✅ 2s 10s -80%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 3s -33%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 1s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 5s 2s +150%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 5s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 2s 1s +100%
mlk_poly_invntt_tomont LP64 z3* ✅ 1s 3s -67%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 5s 2s +150%
mlk_poly_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 2s 3s -33%
mlk_poly_ntt LP64 bitwuzla* ✅ 6s 8s -25%
mlk_poly_ntt_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_reduce_c LP64 z3* ✅ 1s 1s +0%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 34s 40s -15%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 35s 161s -78%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 7s -14%
mlk_poly_sub LP64 z3* ✅ 7s 8s -12%
mlk_poly_tobytes LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_tobytes_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_tomont LP64 z3* ✅ 2s 2s +0%
mlk_poly_tomont_c LP64 z3* ✅ 5s 3s +67%
mlk_poly_tomont_native LP64 z3* ✅ 4s 4s +0%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 2s 5s -60%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 105s - new
mlk_polyvec_add LP64 z3* ✅ 16s 18s -11%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 124s 79s +57%
mlk_polyvec_compress_du LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_decompress_du LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 5s -60%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 1s 4s -75%
mlk_polyvec_ntt LP64 z3* ✅ 5s 12s -58%
mlk_polyvec_reduce LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_tomont LP64 z3* ✅ 2s 2s +0%
mlk_rej_uniform LP64 bitwuzla* ✅ 3s 2s +50%
mlk_rej_uniform_c LP64 z3* ✅ 163s 144s +13%
mlk_scalar_compress_d1 LP64 z3* ✅ 4s 3s +33%
mlk_scalar_compress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d11 LP64 z3* ✅ 3s 4s -25%
mlk_scalar_compress_d4 LP64 z3* ✅ 1s 1s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 1s 4s -75%
mlk_scalar_decompress_d10 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_decompress_d11 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 1s 3s -67%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 3s -33%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake256 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 6s 4s +50%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 4s 1s +300%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 1s 4s -75%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 5s -40%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 7s 5s +40%
poly_invntt_tomont_native LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 3s 5s -40%
poly_ntt_native LP64 z3* ✅ 2s 43s -95%
poly_reduce_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_reduce_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_tobytes_native_aarch64 LP64 z3* ✅ 4s 3s +33%
poly_tobytes_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 24s 31s -23%
rej_uniform_native LP64 bitwuzla* ✅ 3s 1s +200%
rej_uniform_native_aarch64 LP64 z3* ✅ 41s 53s -23%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 106s 67s +58%
sys_check_capability LP64 z3* ✅ 1s 2s -50%

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 455s 252s +81%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 267s 7s +3714%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 108s 55s +96%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1922s 1645s +16.8%
intt_native_aarch64 LP64 z3* ✅ 2s 5s -60%
intt_native_x86_64 LP64 z3* ✅ 1s 3s -67%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 1s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 4s 2s +100%
keccakf1600_permute_native LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 17s 21s -19%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
kem_check_pk LP64 z3* ✅ 3s 2s +50%
kem_check_sk LP64 z3* ✅ 3s 2s +50%
kem_dec LP64 z3* ✅ 6s 5s +20%
kem_enc LP64 z3* ✅ 3s 2s +50%
kem_enc_derand LP64 z3* ✅ 4s 3s +33%
kem_keypair LP64 z3* ✅ 2s 2s +0%
kem_keypair_derand LP64 z3* ✅ 4s 2s +100%
mlk_barrett_reduce LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 1s 4s -75%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 4s -75%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 3s 1s +200%
ILP32 cvc5_arrays_exp ✅ 3s 1s +200%
ILP32 z3 ✅ 1s 1s +0%
LP64 bitwuzla* ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3 ✅ 1s 1s +0%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 4s -50%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_sel_uint8 LP64 z3* ✅ 3s 1s +200%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_fqmul LP64 z3* ✅ 4s 16s -75%
mlk_gen_matrix LP64 z3* ✅ 2s 2s +0%
mlk_gen_matrix_serial LP64 z3* ✅ 4s 2s +100%
mlk_indcpa_dec LP64 z3* ✅ 19s 10s +90%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 455s 252s +81%
mlk_indcpa_keypair_derand LP64 z3* ✅ 116s 318s -64%
mlk_invntt_layer LP64 z3* ✅ 6s 4s +50%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 4s 3s +33%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 5s +0%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 9s 7s +29%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 8s 8s +0%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 24s 24s +0%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_permute LP64 z3* ✅ 4s 1s +300%
mlk_keccakf1600_permute_c LP64 z3* ✅ 5s 6s -17%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 1s +100%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 3s 2s +50%
mlk_keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 1s +100%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 2s 2s +0%
mlk_matvec_mul LP64 z3* ✅ 2s 4s -50%
mlk_montgomery_reduce LP64 z3* ✅ 3s 1s +200%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 267s 7s +3714%
mlk_ntt_layer LP64 z3* ✅ 8s 29s -72%
mlk_poly_add LP64 z3* ✅ 4s 7s -43%
mlk_poly_cbd_eta1 LP64 z3* ✅ 2s 1s +100%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d10_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 3s 4s -25%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d4_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 4s 3s +33%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d5_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_d10_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 14s 15s -7%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d4_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 14s 12s +17%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_decompress_d5_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 5s 2s +150%
mlk_poly_frombytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_frombytes_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 12s 8s +50%
mlk_poly_frommsg LP64 z3* ✅ 4s 9s -56%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 1s +100%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 1s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 3s 2s +50%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_poly_invntt_tomont LP64 z3* ✅ 2s 4s -50%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_mulcache_compute LP64 z3* ✅ 2s 2s +0%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 1s 1s +0%
mlk_poly_ntt LP64 bitwuzla* ✅ 7s 5s +40%
mlk_poly_ntt_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_reduce LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_reduce_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 35s 34s +3%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 37s 129s -71%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 5s +20%
mlk_poly_sub LP64 z3* ✅ 7s 10s -30%
mlk_poly_tobytes LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_tobytes_c LP64 z3* ✅ 1s 1s +0%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_tomont LP64 z3* ✅ 2s 1s +100%
mlk_poly_tomont_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_tomont_native LP64 z3* ✅ 3s 3s +0%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 68s - new
mlk_polyvec_add LP64 z3* ✅ 11s 12s -8%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ✅ 68s 46s +48%
mlk_polyvec_compress_du LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_decompress_du LP64 z3* ✅ 1s 4s -75%
mlk_polyvec_frombytes LP64 z3* ✅ 1s 3s -67%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_ntt LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_reduce LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tomont LP64 z3* ✅ 1s 1s +0%
mlk_rej_uniform LP64 bitwuzla* ✅ 3s 1s +200%
mlk_rej_uniform_c LP64 z3* ✅ 155s 114s +36%
mlk_scalar_compress_d1 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d11 LP64 z3* ✅ 1s 1s +0%
mlk_scalar_compress_d4 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 1s +100%
mlk_scalar_decompress_d10 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d4 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 3s 5s -40%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_sha3_512 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 4s 1s +300%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 4s 3s +33%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
mlk_shake256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_shake256x4 LP64 bitwuzla* ✅ 4s 3s +33%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 3s 2s +50%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_x86_64 LP64 z3* ✅ 4s 3s +33%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 6s 5s +20%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 4s 1s +300%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 6s 6s +0%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 3s 5s -40%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 6s -67%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_ntt_native LP64 z3* ✅ 3s 39s -92%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_reduce_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_tobytes_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_tobytes_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_tomont_native_x86_64 LP64 z3* ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 14s 14s +0%
rej_uniform_native LP64 bitwuzla* ✅ 3s 2s +50%
rej_uniform_native_aarch64 LP64 z3* ✅ 40s 45s -11%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 108s 55s +96%
sys_check_capability LP64 z3* ✅ 2s 3s -33%

@hanno-becker
hanno-becker marked this pull request as ready for review October 20, 2026 05:15
@hanno-becker

hanno-becker commented Oct 20, 2026

Copy link
Copy Markdown
Contributor Author

@mkannwischer Note the slight complication in making sure we only build the backend .S files which the compiler can handle; the commit message also describes an alternative.

@hanno-becker
hanno-becker marked this pull request as draft October 20, 2026 08:03
@hanno-becker

hanno-becker commented Oct 20, 2026

Copy link
Copy Markdown
Contributor Author

@mkannwischer Note the slight complication in making sure we only build the backend .S files which the compiler can handle; the commit message also describes an alternative.

Turns out that there's another issue which basically forces the alternative of additional guards in the backend files. I'll pursue that. No need to review for now @mkannwischer

@hanno-becker
hanno-becker marked this pull request as ready for review October 20, 2026 09:43
@hanno-becker
Guard assembly with its required CPU features
9a050f3 
Backend assembly is gated by backend and parameter-set macros. The ABI
checker enables those macros for every kernel and adds CPU feature flags
so the files assemble. It cannot simply use the platform's flags while
unsupported files still contain instructions.

Guard backend assembly with the architecture and feature macros for
its instructions. Use `__ARM_FEATURE_SHA3` for the SHA3 kernels
alongside `MLK_SYS_AARCH64_NEON`. Apply matching guards to the ABI stubs
and generated checks.

Define `MLK_SYS_ARMV81M_MVE` only when `__ARM_FEATURE_MVE` is present:
Armv8.1-M architecture support alone does not enable MVE. GCC exposes
the feature macro only with a softfp or hard float ABI, so use
`-mfloat-abi=hard` when autogen regenerates MVE assembly.

The AWS-LC importer replaces `common.h` with s2n-bignum headers after
running `unifdef`. Add a pre-import patch that resolves the NEON and
AVX2 guards for the selected assembly, so imported files do not depend
on mlkem-native's system macros.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
abicheck: Use the platform's CPU feature flags
300af76 
The ABI checker adds CPU feature flags to individual assembly objects.
This can enable kernels which the platform disabled and leaves Make
responsible for compiler capabilities that a custom build, such as
Zephyr, determines itself.

The preceding commit guards assembly with the same architecture and
feature checks as the generated C tests. Compile the fixed source list
with the platform's flags and let those guards omit unsupported kernels.
Remove the generated feature makefiles and the separate SHA3 source
filter.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
CI: Enable ABI checks in the Zig 0.17 jobs
9ff7f2e 
The Zig 0.17 jobs skip ABI checks because the checker previously added
AArch64 `-march` flags which Zig parses as CPU names. The checker now
uses the platform's CPU flags, so that restriction no longer applies.

Remove `--no-abicheck` from the Extended compiler matrix and the Linux
and macOS legacy matrices. Drop the comments about the old `-march`
flags.

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

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer Awaiting requested review from mkannwischer

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

enhancement New feature or request testing

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hanno-becker @oqs-bot