Skip to content

sys.h: Do not depend on configuration options - #1938

Merged
mkannwischer merged 1 commit into
mainfrom
mjk/no-asm-config-order
Oct 15, 2026
Merged

sys.h: Do not depend on configuration options#1938
mkannwischer merged 1 commit into
mainfrom
mjk/no-asm-config-order

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Oct 13, 2026

Copy link
Copy Markdown
Contributor

sys.h evaluated MLK_CONFIG_NO_ASM, MLK_CONFIG_CT_TESTING_ENABLED and MLK_CONFIG_CUSTOM_CAPABILITY_FUNC when it was first included. Configuration hooks such as MLK_CONFIG_CUSTOM_ZEROIZE include sys.h, and its include guard prevents re-evaluation, so an option defined after such a hook was silently ignored or, for the capability function, caused a redefinition error. This affects the order of the config template and test/configs/no_asm_config.h: the "No ASM" configuration kept the inline-assembly value barrier and never built the volatile opt-blocker, and a late CT_TESTING_ENABLED made constant-time tests vacuous.

Move the inline-assembly decision and the CT-testing macros to common.h, after the whole configuration has been read. Move the default mlk_sys_check_capability() to a new shared header capability.h, included from common.h, so that multilevel builds still define it only once. Document in sys.h that it must not depend on configuration options.

@mkannwischer mkannwischer added bug Something isn't working needs-mldsa-native-port labels Oct 13, 2026
@mkannwischer
mkannwischer force-pushed the mjk/no-asm-config-order branch 2 times, most recently from 79b388d to 92eea31 Compare October 13, 2026 07:39
@oqs-bot

oqs-bot commented Oct 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2258s 1614s +39.9%
mlk_indcpa_dec LP64 z3* ⚠️ 23s 14s +64%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 381s 9s +4133%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 86s 55s +56%
mlk_rej_uniform_c LP64 z3* ⚠️ 213s 135s +58%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 160s 57s +181%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2258s 1614s +39.9%
intt_native_aarch64 LP64 z3* ✅ 1s 2s -50%
intt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 4s 2s +100%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 4s 3s +33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 1s +200%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 1s +200%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 17s 16s +6%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 1s +0%
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* ✅ 2s 2s +0%
kem_enc_derand LP64 z3* ✅ 4s 3s +33%
kem_keypair LP64 z3* ✅ 5s 4s +25%
kem_keypair_derand LP64 z3* ✅ 3s 3s +0%
mlk_barrett_reduce LP64 z3* ✅ 1s 2s -50%
mlk_check_pct LP64 bitwuzla* ✅ 4s 5s -20%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 1s +200%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 3s 2s +50%
ILP32 cvc5_arrays_exp ✅ 2s 2s +0%
ILP32 z3 ✅ 3s 2s +50%
LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 1s +100%
mlk_ct_sel_uint8 LP64 z3* ✅ 1s 2s -50%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_fqmul LP64 z3* ✅ 4s 17s -76%
mlk_gen_matrix LP64 z3* ✅ 2s 2s +0%
mlk_gen_matrix_serial LP64 z3* ✅ 1s 3s -67%
mlk_indcpa_dec LP64 z3* ⚠️ 23s 14s +64%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 352s 255s +38%
mlk_indcpa_keypair_derand LP64 z3* ✅ 256s 213s +20%
mlk_invntt_layer LP64 z3* ✅ 10s 4s +150%
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* ✅ 7s 8s -12%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 9s 9s +0%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 29s 26s +12%
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* ✅ 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* ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 3s 3s +0%
mlk_keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 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* ✅ 1s 3s -67%
mlk_montgomery_reduce LP64 z3* ✅ 5s 2s +150%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 381s 9s +4133%
mlk_ntt_layer LP64 z3* ✅ 9s 32s -72%
mlk_poly_add LP64 z3* ✅ 6s 4s +50%
mlk_poly_cbd_eta1 LP64 z3* ✅ 2s 2s +0%
mlk_poly_cbd_eta2 LP64 z3* ✅ 1s 3s -67%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 4s -50%
mlk_poly_compress_d10_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d4_c LP64 z3* ✅ 3s 3s +0%
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* ✅ 2s 3s -33%
mlk_poly_compress_du LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_decompress_d10_c LP64 z3* ✅ 2s 4s -50%
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* ✅ 2s 2s +0%
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* ✅ 4s 7s -43%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 16s 14s +14%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_decompress_d5_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_frombytes LP64 bitwuzla* ✅ 1s 1s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 6s 4s +50%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 14s 8s +75%
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 5s -20%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_poly_invntt_tomont LP64 z3* ✅ 1s 2s -50%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_mulcache_compute LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 3s 2s +50%
mlk_poly_ntt LP64 bitwuzla* ✅ 11s 5s +120%
mlk_poly_ntt_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_reduce_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 39s 35s +11%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 44s 150s -71%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 7s 8s -12%
mlk_poly_sub LP64 z3* ✅ 7s 6s +17%
mlk_poly_tobytes LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_tobytes_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_tomont LP64 z3* ✅ 3s 1s +200%
mlk_poly_tomont_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_tomont_native LP64 z3* ✅ 2s 2s +0%
mlk_poly_tomsg LP64 bitwuzla* ✅ 4s 3s +33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 2s 2s +0%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 33s - new
mlk_polyvec_add LP64 z3* ✅ 13s 11s +18%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 86s 55s +56%
mlk_polyvec_compress_du LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_decompress_du LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_frombytes LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 5s -40%
mlk_polyvec_ntt LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_reduce LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_tomont LP64 z3* ✅ 1s 1s +0%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 5s -60%
mlk_rej_uniform_c LP64 z3* ⚠️ 213s 135s +58%
mlk_scalar_compress_d1 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d11 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d4 LP64 z3* ✅ 3s 1s +200%
mlk_scalar_compress_d5 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d10 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 4s 3s +33%
mlk_scalar_decompress_d5 LP64 z3* ✅ 4s 3s +33%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 1s +100%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_sha3_512 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 4s 3s +33%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 1s 4s -75%
ntt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
ntt_native_x86_64 LP64 z3* ✅ 4s 2s +100%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 4s 3s +33%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 1s 1s +0%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
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* ✅ 5s 4s +25%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 1s 2s -50%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 7s 5s +40%
poly_invntt_tomont_native LP64 z3* ✅ 1s 2s -50%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 4s 3s +33%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 1s 1s +0%
poly_ntt_native LP64 z3* ✅ 3s 45s -93%
poly_reduce_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_reduce_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_tobytes_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_tobytes_native_x86_64 LP64 z3* ✅ 4s 1s +300%
poly_tomont_native_aarch64 LP64 z3* ✅ 4s 2s +100%
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* ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 2s 3s -33%
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* ✅ 5s 2s +150%
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* ⚠️ 160s 57s +181%
sys_check_capability LP64 z3* ✅ 2s 1s +100%

@oqs-bot

oqs-bot commented Oct 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2094s 1645s +27.3%
mlk_indcpa_dec LP64 z3* ⚠️ 24s 10s +140%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 467s 252s +85%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 291s 7s +4057%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 97s 46s +111%
mlk_rej_uniform_c LP64 z3* ⚠️ 176s 114s +54%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 116s 55s +111%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2094s 1645s +27.3%
intt_native_aarch64 LP64 z3* ✅ 2s 5s -60%
intt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
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* ✅ 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* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 14s 21s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 4s 2s +100%
kem_check_pk LP64 z3* ✅ 5s 2s +150%
kem_check_sk LP64 z3* ✅ 4s 2s +100%
kem_dec LP64 z3* ✅ 7s 5s +40%
kem_enc LP64 z3* ✅ 4s 2s +100%
kem_enc_derand LP64 z3* ✅ 4s 3s +33%
kem_keypair LP64 z3* ✅ 2s 2s +0%
kem_keypair_derand LP64 z3* ✅ 2s 2s +0%
mlk_barrett_reduce LP64 z3* ✅ 3s 2s +50%
mlk_check_pct LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_cmask_neg_i16 LP64 z3* ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 LP64 z3* ✅ 5s 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 ✅ 1s 1s +0%
LP64 bitwuzla* ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 2s 1s +100%
LP64 z3 ✅ 3s 1s +200%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 3s 1s +200%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 4s -50%
mlk_ct_sel_int16 LP64 z3* ✅ 2s 3s -33%
mlk_ct_sel_uint8 LP64 z3* ✅ 1s 1s +0%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_fqmul LP64 z3* ✅ 3s 16s -81%
mlk_gen_matrix LP64 z3* ✅ 2s 2s +0%
mlk_gen_matrix_serial LP64 z3* ✅ 3s 2s +50%
mlk_indcpa_dec LP64 z3* ⚠️ 24s 10s +140%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 467s 252s +85%
mlk_indcpa_keypair_derand LP64 z3* ✅ 117s 318s -63%
mlk_invntt_layer LP64 z3* ✅ 8s 4s +100%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 4s 3s +33%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 8s 7s +14%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 8s 8s +0%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 34s 24s +42%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600_permute LP64 z3* ✅ 2s 1s +100%
mlk_keccakf1600_permute_c LP64 z3* ✅ 3s 6s -50%
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* ✅ 2s 2s +0%
mlk_keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 1s +100%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 4s 2s +100%
mlk_matvec_mul LP64 z3* ✅ 3s 4s -25%
mlk_montgomery_reduce LP64 z3* ✅ 3s 1s +200%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 291s 7s +4057%
mlk_ntt_layer LP64 z3* ✅ 10s 29s -66%
mlk_poly_add LP64 z3* ✅ 4s 7s -43%
mlk_poly_cbd_eta1 LP64 z3* ✅ 3s 1s +200%
mlk_poly_cbd_eta2 LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d10_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_compress_d11_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 4s 4s +0%
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* ✅ 1s 3s -67%
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* ✅ 3s 2s +50%
mlk_poly_compress_du LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 1s 1s +0%
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* ✅ 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* ✅ 4s 4s +0%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 15s 12s +25%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_decompress_d5_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 5s 4s +25%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 13s 8s +62%
mlk_poly_frommsg LP64 z3* ✅ 2s 9s -78%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 1s +100%
mlk_poly_getnoise_eta1122_4x_serial LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 3s 2s +50%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 4s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_poly_invntt_tomont LP64 z3* ✅ 5s 4s +25%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute LP64 z3* ✅ 4s 2s +100%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 5s 2s +150%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 2s 1s +100%
mlk_poly_ntt LP64 bitwuzla* ✅ 8s 5s +60%
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* ✅ 48s 34s +41%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 42s 129s -67%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 7s 5s +40%
mlk_poly_sub LP64 z3* ✅ 8s 10s -20%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_tobytes_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_tomont LP64 z3* ✅ 2s 1s +100%
mlk_poly_tomont_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 z3* ✅ 4s 3s +33%
mlk_poly_tomsg LP64 bitwuzla* ✅ 3s 3s +0%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 1s 3s -67%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 70s - new
mlk_polyvec_add LP64 z3* ✅ 10s 12s -17%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 97s 46s +111%
mlk_polyvec_compress_du LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_decompress_du LP64 z3* ✅ 1s 4s -75%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_ntt LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_reduce LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tobytes LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_tomont LP64 z3* ✅ 2s 1s +100%
mlk_rej_uniform LP64 bitwuzla* ✅ 1s 1s +0%
mlk_rej_uniform_c LP64 z3* ⚠️ 176s 114s +54%
mlk_scalar_compress_d1 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d10 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d11 LP64 z3* ✅ 2s 1s +100%
mlk_scalar_compress_d4 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 3s 1s +200%
mlk_scalar_decompress_d10 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_decompress_d11 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d4 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 1s 5s -80%
mlk_sha3_256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 3s -33%
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* ✅ 3s 1s +200%
mlk_shake256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 6s 3s +100%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 1s 2s -50%
ntt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
ntt_native_x86_64 LP64 z3* ✅ 3s 3s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 3s +0%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 7s 5s +40%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 1s 1s +0%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 5s 6s -17%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 6s 5s +20%
poly_invntt_tomont_native LP64 z3* ✅ 3s 2s +50%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 2s 6s -67%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_ntt_native LP64 z3* ✅ 4s 39s -90%
poly_reduce_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_reduce_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_tobytes_native_aarch64 LP64 z3* ✅ 3s 1s +200%
poly_tobytes_native_x86_64 LP64 z3* ✅ 4s 3s +33%
poly_tomont_native_aarch64 LP64 z3* ✅ 3s 1s +200%
poly_tomont_native_x86_64 LP64 z3* ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 4s 4s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 1s 2s -50%
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* ✅ 1s 2s -50%
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* ✅ 47s 45s +4%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 116s 55s +111%
sys_check_capability LP64 z3* ✅ 1s 3s -67%

@oqs-bot

oqs-bot commented Oct 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2461s 1885s +30.6%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 398s 9s +4322%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 158s 79s +100%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 162s 67s +142%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2461s 1885s +30.6%
intt_native_aarch64 LP64 z3* ✅ 1s 3s -67%
intt_native_x86_64 LP64 z3* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 1s +200%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 4s 2s +100%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 4s 3s +33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 18s 15s +20%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
kem_check_pk LP64 z3* ✅ 2s 4s -50%
kem_check_sk LP64 z3* ✅ 4s 3s +33%
kem_dec LP64 z3* ✅ 9s 5s +80%
kem_enc LP64 z3* ✅ 2s 2s +0%
kem_enc_derand LP64 z3* ✅ 4s 3s +33%
kem_keypair LP64 z3* ✅ 2s 2s +0%
kem_keypair_derand LP64 z3* ✅ 3s 1s +200%
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* ✅ 1s 2s -50%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 1s +100%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 1s 3s -67%
ILP32 cvc5_arrays_exp ✅ 2s 3s -33%
ILP32 z3 ✅ 3s 3s +0%
LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_ct_memcmp LP64 bitwuzla* ✅ 1s 3s -67%
mlk_ct_sel_int16 LP64 z3* ✅ 3s 4s -25%
mlk_ct_sel_uint8 LP64 z3* ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 3s 4s -25%
mlk_fqmul LP64 z3* ✅ 6s 20s -70%
mlk_gen_matrix LP64 z3* ✅ 5s 2s +150%
mlk_gen_matrix_serial LP64 z3* ✅ 5s 4s +25%
mlk_indcpa_dec LP64 z3* ✅ 18s 11s +64%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 447s 402s +11%
mlk_indcpa_keypair_derand LP64 z3* ✅ 171s 176s -3%
mlk_invntt_layer LP64 z3* ✅ 9s 6s +50%
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* ✅ 9s 10s -10%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 13s 9s +44%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 30s 26s +15%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
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* ✅ 1s 2s -50%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 z3* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 5s -60%
mlk_keypair_getnoise_eta1 LP64 z3* ✅ 4s 5s -20%
mlk_matvec_mul LP64 z3* ✅ 2s 5s -60%
mlk_montgomery_reduce LP64 z3* ✅ 3s 2s +50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 398s 9s +4322%
mlk_ntt_layer LP64 z3* ✅ 8s 38s -79%
mlk_poly_add LP64 z3* ✅ 6s 5s +20%
mlk_poly_cbd_eta1 LP64 z3* ✅ 3s 3s +0%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d10_c LP64 z3* ✅ 1s 3s -67%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_poly_compress_d11_c LP64 z3* ✅ 4s 4s +0%
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* ✅ 5s 4s +25%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 3s 5s -40%
mlk_poly_compress_d5_c LP64 z3* ✅ 1s 4s -75%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 3s 4s -25%
mlk_poly_compress_du LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
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* ✅ 4s 2s +100%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 20s 16s +25%
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* ✅ 1s 3s -67%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d5_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 20s 18s +11%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 5s 3s +67%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 14s 10s +40%
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* ✅ 2s - new
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 1s 2s -50%
mlk_poly_getnoise_eta1_4x_serial LP64 z3* ✅ 2s - new
mlk_poly_getnoise_eta2 LP64 z3* ✅ 2s 1s +100%
mlk_poly_invntt_tomont LP64 z3* ✅ 2s 3s -33%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_mulcache_compute LP64 z3* ✅ 2s 2s +0%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 1s 3s -67%
mlk_poly_ntt LP64 bitwuzla* ✅ 10s 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* ✅ 52s 40s +30%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 45s 161s -72%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 9s 7s +29%
mlk_poly_sub LP64 z3* ✅ 8s 8s +0%
mlk_poly_tobytes LP64 bitwuzla* ✅ 3s 3s +0%
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* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 z3* ✅ 2s 4s -50%
mlk_poly_tomsg LP64 bitwuzla* ✅ 3s 3s +0%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 4s 5s -20%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 112s - new
mlk_polyvec_add LP64 z3* ✅ 25s 18s +39%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 158s 79s +100%
mlk_polyvec_compress_du LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_decompress_du LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_frombytes LP64 z3* ✅ 4s 5s -20%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 4s 4s +0%
mlk_polyvec_ntt LP64 z3* ✅ 4s 12s -67%
mlk_polyvec_reduce LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_tobytes LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_tomont LP64 z3* ✅ 1s 2s -50%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 2s +0%
mlk_rej_uniform_c LP64 z3* ✅ 197s 144s +37%
mlk_scalar_compress_d1 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_compress_d10 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_compress_d11 LP64 z3* ✅ 1s 4s -75%
mlk_scalar_compress_d4 LP64 z3* ✅ 1s 1s +0%
mlk_scalar_compress_d5 LP64 z3* ✅ 2s 4s -50%
mlk_scalar_decompress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d11 LP64 z3* ✅ 2s 2s +0%
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* ✅ 1s 3s -67%
mlk_sha3_256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_sha3_512 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 5s 2s +150%
mlk_shake256 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 4s +25%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 2s 1s +100%
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* ✅ 3s 3s +0%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
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* ✅ 6s 5s +20%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_invntt_tomont_native LP64 z3* ✅ 3s 3s +0%
poly_mulcache_compute_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_mulcache_compute_native_x86_64 LP64 z3* ✅ 2s 5s -60%
poly_ntt_native LP64 z3* ✅ 2s 43s -95%
poly_reduce_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_reduce_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_tobytes_native_aarch64 LP64 z3* ✅ 4s 3s +33%
poly_tobytes_native_x86_64 LP64 z3* ✅ 5s 3s +67%
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* ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 5s 2s +150%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 31s 31s +0%
rej_uniform_native LP64 bitwuzla* ✅ 3s 1s +200%
rej_uniform_native_aarch64 LP64 z3* ✅ 45s 53s -15%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 162s 67s +142%
sys_check_capability LP64 z3* ✅ 3s 2s +50%

@mkannwischer
sys.h: Do not depend on configuration options
c5280f8 
sys.h evaluated MLK_CONFIG_NO_ASM, MLK_CONFIG_CT_TESTING_ENABLED and
MLK_CONFIG_CUSTOM_CAPABILITY_FUNC when it was first included.
Configuration hooks such as MLK_CONFIG_CUSTOM_ZEROIZE include sys.h,
and its include guard prevents re-evaluation, so an option defined
after such a hook was silently ignored or, for the capability function,
caused a redefinition error. This affects the order of the config
template and test/configs/no_asm_config.h: the "No ASM" configuration
kept the inline-assembly value barrier and never built the volatile
opt-blocker, and a late CT_TESTING_ENABLED made constant-time tests
vacuous.

Move the inline-assembly decision and the CT-testing macros to
common.h, after the whole configuration has been read. Move the default
mlk_sys_check_capability() to a new shared header capability.h,
included from common.h, so that multilevel builds still define it only
once. Document in sys.h that it must not depend on configuration
options.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
mkannwischer force-pushed the mjk/no-asm-config-order branch from 92eea31 to c5280f8 Compare October 13, 2026 08:56
@mkannwischer
mkannwischer marked this pull request as ready for review October 13, 2026 10:52
@mkannwischer
mkannwischer requested a review from a team as a code owner October 13, 2026 10:52
hanno-becker
hanno-becker reviewed Oct 15, 2026
View reviewed changes
Comment thread mlkem/src/sys.h Resolved
hanno-becker
hanno-becker approved these changes Oct 15, 2026
View reviewed changes

@hanno-becker hanno-becker 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.

Thank you @mkannwischer, I greatly support the disentanglement of sys.h and the config.

I'd suggest that we add a lint check to confirm that sys.h does not talk about config options; otherwise, this is good to go.

@mkannwischer mkannwischer mentioned this pull request Oct 15, 2026
Open
@mkannwischer
mkannwischer added this pull request to the merge queue Oct 15, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Oct 15, 2026
@mkannwischer
mkannwischer added this pull request to the merge queue Oct 15, 2026
Merged via the queue into main with commit 7da6bd1 Oct 15, 2026
712 of 713 checks passed
@mkannwischer
mkannwischer deleted the mjk/no-asm-config-order branch October 15, 2026 10:33
@github-actions github-actions Bot mentioned this pull request Oct 15, 2026
Open
@mkannwischer mkannwischer mentioned this pull request Oct 17, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hanno-becker hanno-becker hanno-becker approved these changes

Assignees

No one assigned

Labels

bug Something isn't working needs-mldsa-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkannwischer @oqs-bot @hanno-becker