Skip to content

PPC64: Guard ABI checks with POWER8 vector support - #1943

Merged
hanno-becker merged 1 commit into
mainfrom
power8-fixes
Oct 20, 2026
Merged

PPC64: Guard ABI checks with POWER8 vector support#1943
hanno-becker merged 1 commit into
mainfrom
power8-fixes

Conversation

@hanno-becker

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

Copy link
Copy Markdown
Contributor 
The PPC64 ABI checker registered kernels whenever the target was
PPC64LE, while the kernels require POWER8 vector support. Without the
forced assembly flags, an older target could therefore refer to kernels
that were compiled out.

Add `MLK_SYS_PPC64LE_POWER8_VECTOR`, requiring `__ALTIVEC__`, `__VSX__`,
and `__POWER8_VECTOR__` on PPC64LE. Use it for the backend kernels,
constants and C wrappers, and the generated ABI checks, registry, call
stub and self-test. Name the ABI feature `POWER8_VECTOR`.

Append `MLK_SYS_CAP_PPC64LE_POWER8_VECTOR` and consult the capability
hook before calling assembly from the ABI checks or self-test.

Correct the backend READMEs from POWER9 to POWER8 and state the AltiVec
and VSX requirement. Keep the assembly instruction bodies, per-object
ISA flags, and `auto.mk` unchanged. The default capability function
still assumes enabled features are supported; runtime detection requires
a custom function.

@hanno-becker
hanno-becker requested a review from a team as a code owner October 17, 2026 09:28
@hanno-becker
hanno-becker marked this pull request as draft October 17, 2026 09:44
@oqs-bot

oqs-bot commented Oct 17, 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* ⚠️ 306s 9s +3300%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 131s 79s +66%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 112s 67s +67%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2113s 1885s +12.1%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 15s 15s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
kem_check_pk LP64 z3* ✅ 1s 4s -75%
kem_check_sk LP64 z3* ✅ 4s 3s +33%
kem_dec LP64 z3* ✅ 8s 5s +60%
kem_enc LP64 z3* ✅ 2s 2s +0%
kem_enc_derand LP64 z3* ✅ 1s 3s -67%
kem_keypair LP64 z3* ✅ 1s 2s -50%
kem_keypair_derand LP64 z3* ✅ 5s 1s +400%
mlk_barrett_reduce LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 3s 1s +200%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 3s 2s +50%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 4s 1s +300%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s 3s -33%
ILP32 cvc5_arrays_exp ✅ 2s 3s -33%
ILP32 z3 ✅ 2s 3s -33%
LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3 ✅ 2s 3s -33%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_ct_memcmp LP64 bitwuzla* ✅ 4s 3s +33%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 4s -50%
mlk_ct_sel_uint8 LP64 z3* ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 3s 4s -25%
mlk_fqmul LP64 z3* ✅ 3s 20s -85%
mlk_gen_matrix LP64 z3* ✅ 3s 2s +50%
mlk_gen_matrix_serial LP64 z3* ✅ 4s 4s +0%
mlk_indcpa_dec LP64 z3* ✅ 18s 11s +64%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 425s 402s +6%
mlk_indcpa_keypair_derand LP64 z3* ✅ 149s 176s -15%
mlk_invntt_layer LP64 z3* ✅ 4s 6s -33%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 4s 4s +0%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 8s 5s +60%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 8s 10s -20%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 8s 9s -11%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 26s 26s +0%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600_permute LP64 z3* ✅ 4s 2s +100%
mlk_keccakf1600_permute_c LP64 z3* ✅ 5s 6s -17%
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* ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 z3* ✅ 1s 2s -50%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 3s 5s -40%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 3s 5s -40%
mlk_matvec_mul LP64 z3* ✅ 2s 5s -60%
mlk_montgomery_reduce LP64 z3* ✅ 2s 2s +0%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 306s 9s +3300%
mlk_ntt_layer LP64 z3* ✅ 7s 38s -82%
mlk_poly_add LP64 z3* ✅ 7s 5s +40%
mlk_poly_cbd_eta1 LP64 z3* ✅ 4s 3s +33%
mlk_poly_cbd_eta2 LP64 z3* ✅ 1s 3s -67%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d10_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d4_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 2s 5s -60%
mlk_poly_compress_d5_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 3s 4s -25%
mlk_poly_compress_du LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 1s 1s +0%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d10_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d11_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 14s 16s -12%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_d5_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 14s 18s -22%
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* ✅ 3s 3s +0%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 13s 10s +30%
mlk_poly_frommsg LP64 z3* ✅ 3s 10s -70%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 3s -33%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 4s 2s +100%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 2s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 4s 1s +300%
mlk_poly_invntt_tomont LP64 z3* ✅ 3s 3s +0%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 4s 2s +100%
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* ✅ 8s 8s +0%
mlk_poly_ntt_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_reduce_c LP64 z3* ✅ 5s 1s +400%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 34s 40s -15%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 34s 161s -79%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 7s -14%
mlk_poly_sub LP64 z3* ✅ 8s 8s +0%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_tobytes_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_tomont LP64 z3* ✅ 2s 2s +0%
mlk_poly_tomont_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 z3* ✅ 2s 4s -50%
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* ✅ 102s - new
mlk_polyvec_add LP64 z3* ✅ 18s 18s +0%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 131s 79s +66%
mlk_polyvec_compress_du LP64 z3* ✅ 4s 3s +33%
mlk_polyvec_decompress_du LP64 z3* ✅ 1s 2s -50%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 5s -60%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_ntt LP64 z3* ✅ 3s 12s -75%
mlk_polyvec_reduce LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_tomont LP64 z3* ✅ 4s 2s +100%
mlk_rej_uniform LP64 bitwuzla* ✅ 4s 2s +100%
mlk_rej_uniform_c LP64 z3* ✅ 174s 144s +21%
mlk_scalar_compress_d1 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_compress_d10 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d11 LP64 z3* ✅ 2s 4s -50%
mlk_scalar_compress_d4 LP64 z3* ✅ 3s 1s +200%
mlk_scalar_compress_d5 LP64 z3* ✅ 3s 4s -25%
mlk_scalar_decompress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d5 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 3s -33%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_sha3_512 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 4s 1s +300%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake256 LP64 bitwuzla* ✅ 3s 1s +200%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 4s +25%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 2s 1s +100%
ntt_native_aarch64 LP64 z3* ✅ 1s 3s -67%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 3s +0%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 4s -50%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 1s 4s -75%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_invntt_tomont_native LP64 z3* ✅ 1s 3s -67%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 3s 5s -40%
poly_ntt_native LP64 z3* ✅ 3s 43s -93%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_reduce_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_tobytes_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_tobytes_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 1s 1s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 26s 31s -16%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
rej_uniform_native_aarch64 LP64 z3* ✅ 42s 53s -21%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 112s 67s +67%
sys_check_capability LP64 z3* ✅ 1s 2s -50%

@oqs-bot

oqs-bot commented Oct 17, 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_dec LP64 z3* ⚠️ 22s 10s +120%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 444s 252s +76%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 289s 7s +4029%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 72s 46s +57%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 115s 55s +109%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1992s 1645s +21.1%
intt_native_aarch64 LP64 z3* ✅ 3s 5s -40%
intt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 1s +200%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 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* ✅ 1s 1s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 17s 21s -19%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 2s +50%
kem_check_pk LP64 z3* ✅ 4s 2s +100%
kem_check_sk LP64 z3* ✅ 4s 2s +100%
kem_dec LP64 z3* ✅ 6s 5s +20%
kem_enc LP64 z3* ✅ 3s 2s +50%
kem_enc_derand LP64 z3* ✅ 2s 3s -33%
kem_keypair LP64 z3* ✅ 4s 2s +100%
kem_keypair_derand LP64 z3* ✅ 5s 2s +150%
mlk_barrett_reduce LP64 z3* ✅ 5s 2s +150%
mlk_check_pct LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 3s 4s -25%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 4s -50%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s 1s +100%
ILP32 cvc5_arrays_exp ✅ 1s 1s +0%
ILP32 z3 ✅ 2s 1s +100%
LP64 bitwuzla* ✅ 1s 1s +0%
LP64 cvc5_arrays_exp ✅ 2s 1s +100%
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* ✅ 1s 3s -67%
mlk_ct_sel_uint8 LP64 z3* ✅ 2s 1s +100%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_fqmul LP64 z3* ✅ 3s 16s -81%
mlk_gen_matrix LP64 z3* ✅ 3s 2s +50%
mlk_gen_matrix_serial LP64 z3* ✅ 1s 2s -50%
mlk_indcpa_dec LP64 z3* ⚠️ 22s 10s +120%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 444s 252s +76%
mlk_indcpa_keypair_derand LP64 z3* ✅ 115s 318s -64%
mlk_invntt_layer LP64 z3* ✅ 7s 4s +75%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 6s 3s +100%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 7s +0%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 12s 8s +50%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 27s 24s +12%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_permute LP64 z3* ✅ 2s 1s +100%
mlk_keccakf1600_permute_c LP64 z3* ✅ 5s 6s -17%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 3s 3s +0%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 1s +200%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 2s +0%
mlk_keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 1s +0%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 1s 2s -50%
mlk_matvec_mul LP64 z3* ✅ 4s 4s +0%
mlk_montgomery_reduce LP64 z3* ✅ 3s 1s +200%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 289s 7s +4029%
mlk_ntt_layer LP64 z3* ✅ 9s 29s -69%
mlk_poly_add LP64 z3* ✅ 5s 7s -29%
mlk_poly_cbd_eta1 LP64 z3* ✅ 1s 1s +0%
mlk_poly_cbd_eta2 LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_compress_d10_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 4s 1s +300%
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* ✅ 2s 3s -33%
mlk_poly_compress_d4_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 3s 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* ✅ 1s 1s +0%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 15s 15s +0%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_decompress_d11_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 1s 1s +0%
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* ✅ 12s 12s +0%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_decompress_d5_c LP64 z3* ✅ 1s 3s -67%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 1s 1s +0%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_frombytes_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 13s 8s +62%
mlk_poly_frommsg LP64 z3* ✅ 3s 9s -67%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 1s 1s +0%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 1s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 4s 2s +100%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 3s 2s +50%
mlk_poly_invntt_tomont LP64 z3* ✅ 1s 4s -75%
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* ✅ 2s 2s +0%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 2s 1s +100%
mlk_poly_ntt LP64 bitwuzla* ✅ 10s 5s +100%
mlk_poly_ntt_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_reduce LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_reduce_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 34s 34s +0%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 36s 129s -72%
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* ✅ 1s 1s +0%
mlk_poly_tomont_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 3s 3s +0%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 74s - new
mlk_polyvec_add LP64 z3* ✅ 12s 12s +0%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 72s 46s +57%
mlk_polyvec_compress_du LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_decompress_du LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_ntt LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_reduce LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_tobytes LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_tomont LP64 z3* ✅ 2s 1s +100%
mlk_rej_uniform LP64 bitwuzla* ✅ 4s 1s +300%
mlk_rej_uniform_c LP64 z3* ✅ 165s 114s +45%
mlk_scalar_compress_d1 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d11 LP64 z3* ✅ 4s 1s +300%
mlk_scalar_compress_d4 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 3s 1s +200%
mlk_scalar_decompress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 3s +0%
mlk_scalar_decompress_d4 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d5 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 1s 5s -80%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_sha3_512 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake256 LP64 bitwuzla* ✅ 4s 2s +100%
mlk_shake256x4 LP64 bitwuzla* ✅ 4s 3s +33%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 3s 2s +50%
ntt_native_aarch64 LP64 z3* ✅ 1s 3s -67%
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 3s 5s -40%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 1s 3s -67%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 3s +0%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 1s +200%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 4s 6s -33%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 4s -50%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_invntt_tomont_native LP64 z3* ✅ 1s 2s -50%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 6s -67%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 4s 3s +33%
poly_ntt_native LP64 z3* ✅ 3s 39s -92%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_reduce_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_tobytes_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_tobytes_native_x86_64 LP64 z3* ✅ 1s 3s -67%
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* ✅ 2s 3s -33%
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* ✅ 4s 2s +100%
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* ✅ 17s 14s +21%
rej_uniform_native LP64 bitwuzla* ✅ 3s 2s +50%
rej_uniform_native_aarch64 LP64 z3* ✅ 43s 45s -4%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 115s 55s +109%
sys_check_capability LP64 z3* ✅ 5s 3s +67%

@oqs-bot

oqs-bot commented Oct 17, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2104s 1614s +30.4%
mlk_indcpa_dec LP64 z3* ⚠️ 21s 14s +50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 345s 9s +3733%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 131s 57s +130%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2104s 1614s +30.4%
intt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
intt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 1s +200%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 18s 16s +12%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 1s +0%
kem_check_pk LP64 z3* ✅ 3s 4s -25%
kem_check_sk LP64 z3* ✅ 2s 2s +0%
kem_dec LP64 z3* ✅ 6s 5s +20%
kem_enc LP64 z3* ✅ 1s 2s -50%
kem_enc_derand LP64 z3* ✅ 4s 3s +33%
kem_keypair LP64 z3* ✅ 2s 4s -50%
kem_keypair_derand LP64 z3* ✅ 2s 3s -33%
mlk_barrett_reduce LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 4s 5s -20%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 2s 2s +0%
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 ✅ 2s 2s +0%
ILP32 cvc5_arrays_exp ✅ 2s 2s +0%
ILP32 z3 ✅ 3s 2s +50%
LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3 ✅ 1s 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* ✅ 5s 3s +67%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 1s +100%
mlk_ct_sel_uint8 LP64 z3* ✅ 3s 2s +50%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 1s 2s -50%
mlk_fqmul LP64 z3* ✅ 3s 17s -82%
mlk_gen_matrix LP64 z3* ✅ 4s 2s +100%
mlk_gen_matrix_serial LP64 z3* ✅ 2s 3s -33%
mlk_indcpa_dec LP64 z3* ⚠️ 21s 14s +50%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 354s 255s +39%
mlk_indcpa_keypair_derand LP64 z3* ✅ 249s 213s +17%
mlk_invntt_layer LP64 z3* ✅ 8s 4s +100%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 6s 3s +100%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 8s 5s +60%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 8s 8s +0%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 11s 9s +22%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 30s 26s +15%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 5s -60%
mlk_keccakf1600_permute LP64 z3* ✅ 5s 1s +400%
mlk_keccakf1600_permute_c LP64 z3* ✅ 5s 5s +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* ✅ 3s 2s +50%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 3s -67%
mlk_keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
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* ✅ 3s 3s +0%
mlk_montgomery_reduce LP64 z3* ✅ 1s 2s -50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 345s 9s +3733%
mlk_ntt_layer LP64 z3* ✅ 9s 32s -72%
mlk_poly_add LP64 z3* ✅ 5s 4s +25%
mlk_poly_cbd_eta1 LP64 z3* ✅ 1s 2s -50%
mlk_poly_cbd_eta2 LP64 z3* ✅ 1s 3s -67%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 3s 4s -25%
mlk_poly_compress_d10_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 1s 3s -67%
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* ✅ 3s 2s +50%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d5_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_du LP64 bitwuzla* ✅ 4s 3s +33%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 4s 3s +33%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_d10_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 18s 15s +20%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d4_c LP64 z3* ✅ 1s 7s -86%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 16s 14s +14%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d5_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_frombytes_c LP64 z3* ✅ 6s 4s +50%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 15s 8s +88%
mlk_poly_frommsg LP64 z3* ✅ 2s 10s -80%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 4s 3s +33%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 4s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 6s 5s +20%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 4s 3s +33%
mlk_poly_invntt_tomont LP64 z3* ✅ 4s 2s +100%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 1s 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* ✅ 1s 2s -50%
mlk_poly_ntt LP64 bitwuzla* ✅ 9s 5s +80%
mlk_poly_ntt_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_reduce_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 40s 35s +14%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 30s 150s -80%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 8s -25%
mlk_poly_sub LP64 z3* ✅ 8s 6s +33%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_tobytes_c LP64 z3* ✅ 1s 3s -67%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_tomont LP64 z3* ✅ 1s 1s +0%
mlk_poly_tomont_c LP64 z3* ✅ 4s 2s +100%
mlk_poly_tomont_native LP64 z3* ✅ 4s 2s +100%
mlk_poly_tomsg LP64 bitwuzla* ✅ 4s 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* ✅ 11s 11s +0%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ✅ 62s 55s +13%
mlk_polyvec_compress_du LP64 z3* ✅ 1s 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* ✅ 4s 5s -20%
mlk_polyvec_ntt LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_reduce LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_tomont LP64 z3* ✅ 2s 1s +100%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 5s -60%
mlk_rej_uniform_c LP64 z3* ✅ 197s 135s +46%
mlk_scalar_compress_d1 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d11 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d4 LP64 z3* ✅ 1s 1s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 1s 3s -67%
mlk_scalar_decompress_d5 LP64 z3* ✅ 1s 3s -67%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 1s +100%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 3s 3s +0%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 5s +0%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 2s 4s -50%
ntt_native_aarch64 LP64 z3* ✅ 1s 2s -50%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 4s 3s +33%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 1s 1s +0%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 1s 2s -50%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 6s 9s -33%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 1s +200%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 7s 4s +75%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_invntt_tomont_native LP64 z3* ✅ 4s 2s +100%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 3s 1s +200%
poly_ntt_native LP64 z3* ✅ 4s 45s -91%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 1s +100%
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* ✅ 2s 1s +100%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_tomont_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 2s 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* ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 9s 8s +12%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
rej_uniform_native_aarch64 LP64 z3* ✅ 49s 43s +14%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 131s 57s +130%
sys_check_capability LP64 z3* ✅ 2s 1s +100%

@hanno-becker hanno-becker mentioned this pull request Oct 19, 2026
Merged
@hanno-becker
hanno-becker marked this pull request as ready for review October 19, 2026 19:25
@hanno-becker
PPC64: Align backend selection and ABI feature guards
b26e10d 
The PPC64 ABI checker registered kernels whenever the target was
PPC64LE, while the kernels require POWER8 vector support. Removing the
checker's forced assembly flags would leave checks referring to kernels
omitted by the build's CPU flags.

Add `MLK_SYS_PPC64LE_POWER8_VECTOR`, requiring `__ALTIVEC__`, `__VSX__`,
and `__POWER8_VECTOR__` on PPC64LE. Use it to select the default PPC64
backend in `native/meta.h`, as for the NEON and AVX2 backends.
Unsupported targets then use portable C without selecting the native
wrappers.

Remove the per-kernel and constant-table `__POWER8_VECTOR__` guards and
the wrappers' compile-time fallback branches. Explicitly selecting the
PPC64 backend now requires a target with its documented features,
matching the other backends.

The PPC64 wrappers previously checked only `__POWER8_VECTOR__` at
compile time, so a custom capability function could not disable them at
runtime. Append `MLK_SYS_CAP_PPC64LE_POWER8_VECTOR` and have all four
wrappers consult the capability hook before calling assembly. Return
`MLK_NATIVE_FUNC_FALLBACK` without modifying the input if it rejects
POWER8 vector support.

Use the same feature macro for the generated ABI checks, registry, call
stub and self-test. Name the ABI feature `POWER8_VECTOR` and consult the
capability hook before calling assembly from ABI checks or the
self-test.

Correct the backend READMEs from POWER9 to POWER8 and state the AltiVec
and VSX requirement. The default capability hook assumes compile-time
features are supported; runtime detection requires a custom function.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
mkannwischer
mkannwischer approved these changes Oct 20, 2026
View reviewed changes

@mkannwischer mkannwischer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @hanno-becker. This LGTM - just one nit.

Comment thread test/abicheck/ppc64le/checks/check_intt_ppc_asm.c
@hanno-becker
hanno-becker added this pull request to the merge queue Oct 20, 2026
Merged via the queue into main with commit b955018 Oct 20, 2026
363 checks passed
@hanno-becker
hanno-becker deleted the power8-fixes branch October 20, 2026 17:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer approved these changes

Assignees

No one assigned

Labels

enhancement New feature or request ppc64le testing

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hanno-becker @oqs-bot @mkannwischer