Skip to content

CI: Add clang23 tests and constant-time tests - #1916

Queued
mkannwischer wants to merge 1 commit into
mainfrom
clang23
Queued

CI: Add clang23 tests and constant-time tests#1916
mkannwischer wants to merge 1 commit into
mainfrom
clang23

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Sep 25, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
mlk_ntt_butterfly_block LP64 z3* ⚠️ 274s 9s +2944%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 113s 57s +98%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1888s 1614s +17.0%
intt_native_aarch64 LP64 z3* ✅ 1s 2s -50%
intt_native_x86_64 LP64 z3* ✅ 4s 2s +100%
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* ✅ 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* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 1s +200%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 4s 1s +300%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 16s 16s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 1s +0%
kem_check_pk LP64 z3* ✅ 6s 4s +50%
kem_check_sk LP64 z3* ✅ 2s 2s +0%
kem_dec LP64 z3* ✅ 7s 5s +40%
kem_enc LP64 z3* ✅ 2s 2s +0%
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* ✅ 3s 5s -40%
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* ✅ 3s 1s +200%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 1s 2s -50%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 3s 2s +50%
LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_sel_int16 LP64 z3* ✅ 1s 1s +0%
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* ✅ 2s 2s +0%
mlk_gen_matrix_serial LP64 z3* ✅ 1s 3s -67%
mlk_indcpa_dec LP64 z3* ✅ 19s 14s +36%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 319s 255s +25%
mlk_indcpa_keypair_derand LP64 z3* ✅ 228s 213s +7%
mlk_invntt_layer LP64 z3* ✅ 7s 4s +75%
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* ✅ 9s 9s +0%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 24s 26s -8%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 4s 5s -20%
mlk_keccakf1600_permute LP64 z3* ✅ 2s 1s +100%
mlk_keccakf1600_permute_c LP64 z3* ✅ 5s 5s +0%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 3s 3s +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* ✅ 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* ⚠️ 274s 9s +2944%
mlk_ntt_layer LP64 z3* ✅ 9s 32s -72%
mlk_poly_add LP64 z3* ✅ 5s 4s +25%
mlk_poly_cbd_eta1 LP64 z3* ✅ 2s 2s +0%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 3s -33%
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* ✅ 1s 1s +0%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_compress_d11_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 5s 3s +67%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
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* ✅ 1s 3s -67%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 4s 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* ✅ 3s 4s -25%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 15s 15s +0%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11_c LP64 z3* ✅ 4s 2s +100%
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* ✅ 2s 7s -71%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 14s 14s +0%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 1s 1s +0%
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* ✅ 2s 2s +0%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 1s 1s +0%
mlk_poly_frombytes_c LP64 z3* ✅ 5s 4s +25%
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_eta1_4x LP64 z3* ✅ 2s 5s -60%
mlk_poly_getnoise_eta1_4x_native LP64 z3* ✅ 3s 2s +50%
mlk_poly_getnoise_eta2 LP64 z3* ✅ 3s 3s +0%
mlk_poly_invntt_tomont LP64 z3* ✅ 3s 2s +50%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_mulcache_compute LP64 z3* ✅ 4s 2s +100%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 4s 4s +0%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 3s 2s +50%
mlk_poly_ntt LP64 bitwuzla* ✅ 8s 5s +60%
mlk_poly_ntt_c LP64 z3* ✅ 1s 2s -50%
mlk_poly_reduce LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_reduce_c LP64 z3* ✅ 3s 3s +0%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 34s 35s -3%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 37s 150s -75%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 8s 8s +0%
mlk_poly_sub LP64 z3* ✅ 5s 6s -17%
mlk_poly_tobytes LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_tobytes_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_tomont LP64 z3* ✅ 1s 1s +0%
mlk_poly_tomont_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_tomont_native LP64 z3* ✅ 4s 2s +100%
mlk_poly_tomsg LP64 bitwuzla* ✅ 3s 3s +0%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 3s 2s +50%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 28s - new
mlk_polyvec_add LP64 z3* ✅ 11s 11s +0%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ✅ 62s 55s +13%
mlk_polyvec_compress_du LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_decompress_du LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 1s 3s -67%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 5s -40%
mlk_polyvec_ntt LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_reduce LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 z3* ✅ 1s 3s -67%
mlk_polyvec_tomont LP64 z3* ✅ 4s 1s +300%
mlk_rej_uniform LP64 bitwuzla* ✅ 3s 5s -40%
mlk_rej_uniform_c LP64 z3* ✅ 153s 135s +13%
mlk_scalar_compress_d1 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d10 LP64 z3* ✅ 1s 2s -50%
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* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_decompress_d4 LP64 z3* ✅ 3s 3s +0%
mlk_scalar_decompress_d5 LP64 z3* ✅ 2s 3s -33%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 1s +100%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_sha3_512 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 1s 3s -67%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 4s 1s +300%
mlk_shake256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 6s 5s +20%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 3s 4s -25%
ntt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 2s +0%
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* ✅ 3s 1s +200%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 5s 2s +150%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 7s 9s -22%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 1s +200%
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* ✅ 5s 5s +0%
poly_getnoise_eta1122_4x_native LP64 z3* ✅ 3s 1s +200%
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* ✅ 4s 1s +300%
poly_ntt_native LP64 z3* ✅ 3s 45s -93%
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* ✅ 4s 2s +100%
poly_tobytes_native_x86_64 LP64 z3* ✅ 4s 1s +300%
poly_tomont_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_tomont_native_x86_64 LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 3s 3s +0%
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* ✅ 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* ✅ 40s 43s -7%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 113s 57s +98%
sys_check_capability LP64 z3* ✅ 4s 1s +300%

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2313s 1645s +40.6%
mlk_indcpa_dec LP64 z3* ⚠️ 31s 10s +210%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 468s 252s +86%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 323s 7s +4514%
mlk_poly_decompress_d4_native LP64 bitwuzla* ⚠️ 21s 12s +75%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 105s 46s +128%
mlk_rej_uniform_c LP64 z3* ⚠️ 182s 114s +60%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 142s 55s +158%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2313s 1645s +40.6%
intt_native_aarch64 LP64 z3* ✅ 2s 5s -60%
intt_native_x86_64 LP64 z3* ✅ 5s 3s +67%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 4s 2s +100%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 4s 1s +300%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 16s 21s -24%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
kem_check_pk LP64 z3* ✅ 4s 2s +100%
kem_check_sk LP64 z3* ✅ 3s 2s +50%
kem_dec LP64 z3* ✅ 8s 5s +60%
kem_enc LP64 z3* ✅ 5s 2s +150%
kem_enc_derand LP64 z3* ✅ 3s 3s +0%
kem_keypair LP64 z3* ✅ 3s 2s +50%
kem_keypair_derand LP64 z3* ✅ 2s 2s +0%
mlk_barrett_reduce LP64 z3* ✅ 3s 2s +50%
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* ✅ 2s 4s -50%
mlk_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 4s -75%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 6s 3s +100%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s 1s +100%
ILP32 cvc5_arrays_exp ✅ 2s 1s +100%
ILP32 z3 ✅ 2s 1s +100%
LP64 bitwuzla* ✅ 1s 1s +0%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3 ✅ 2s 1s +100%
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* ✅ 3s 3s +0%
mlk_ct_sel_uint8 LP64 z3* ✅ 3s 1s +200%
mlk_enc_getnoise_eta1_eta2 LP64 z3* ✅ 3s 3s +0%
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* ⚠️ 31s 10s +210%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 468s 252s +86%
mlk_indcpa_keypair_derand LP64 z3* ✅ 151s 318s -53%
mlk_invntt_layer LP64 z3* ✅ 9s 4s +125%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 7s 3s +133%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 8s 5s +60%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 9s 7s +29%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 12s 8s +50%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 34s 24s +42%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
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* ✅ 4s 2s +100%
mlk_keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
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* ✅ 4s 2s +100%
mlk_matvec_mul LP64 z3* ✅ 2s 4s -50%
mlk_montgomery_reduce LP64 z3* ✅ 3s 1s +200%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 323s 7s +4514%
mlk_ntt_layer LP64 z3* ✅ 8s 29s -72%
mlk_poly_add LP64 z3* ✅ 5s 7s -29%
mlk_poly_cbd_eta1 LP64 z3* ✅ 3s 1s +200%
mlk_poly_cbd_eta2 LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_compress_d10_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 7s 2s +250%
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* ✅ 5s 4s +25%
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d4_c LP64 z3* ✅ 1s 1s +0%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d5_c LP64 z3* ✅ 4s 1s +300%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_du LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_compress_dv LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_decompress_d10_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 22s 15s +47%
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_decompress_d11_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 3s 1s +200%
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* ⚠️ 21s 12s +75%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_poly_decompress_d5_c LP64 z3* ✅ 5s 3s +67%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_frombytes_c LP64 z3* ✅ 3s 4s -25%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 18s 8s +125%
mlk_poly_frommsg LP64 z3* ✅ 4s 9s -56%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 1s +100%
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 4s 2s +100%
mlk_poly_getnoise_eta1_4x_native LP64 z3* ✅ 3s 3s +0%
mlk_poly_getnoise_eta2 LP64 z3* ✅ 3s 2s +50%
mlk_poly_invntt_tomont LP64 z3* ✅ 3s 4s -25%
mlk_poly_invntt_tomont_c LP64 z3* ✅ 2s 2s +0%
mlk_poly_mulcache_compute LP64 z3* ✅ 1s 2s -50%
mlk_poly_mulcache_compute_c LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_native LP64 z3* ✅ 3s 1s +200%
mlk_poly_ntt LP64 bitwuzla* ✅ 8s 5s +60%
mlk_poly_ntt_c LP64 z3* ✅ 4s 1s +300%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_reduce_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 50s 34s +47%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 38s 129s -71%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 6s 5s +20%
mlk_poly_sub LP64 z3* ✅ 8s 10s -20%
mlk_poly_tobytes LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_tobytes_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 3s 1s +200%
mlk_poly_tomont LP64 z3* ✅ 1s 1s +0%
mlk_poly_tomont_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 z3* ✅ 5s 3s +67%
mlk_poly_tomsg LP64 bitwuzla* ✅ 4s 3s +33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 3s 3s +0%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 70s - new
mlk_polyvec_add LP64 z3* ✅ 14s 12s +17%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 105s 46s +128%
mlk_polyvec_compress_du LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_decompress_du LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_frombytes LP64 z3* ✅ 3s 3s +0%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_ntt LP64 z3* ✅ 5s 4s +25%
mlk_polyvec_reduce LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tobytes LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_tomont LP64 z3* ✅ 1s 1s +0%
mlk_rej_uniform LP64 bitwuzla* ✅ 1s 1s +0%
mlk_rej_uniform_c LP64 z3* ⚠️ 182s 114s +60%
mlk_scalar_compress_d1 LP64 z3* ✅ 2s 2s +0%
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* ✅ 4s 1s +300%
mlk_scalar_decompress_d10 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 z3* ✅ 4s 3s +33%
mlk_scalar_decompress_d4 LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d5 LP64 z3* ✅ 4s 2s +100%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 5s -60%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_sha3_512 LP64 bitwuzla* ✅ 6s 3s +100%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 1s 3s -67%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
mlk_shake256 LP64 bitwuzla* ✅ 3s 2s +50%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 3s +67%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 4s 2s +100%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 2s 2s +0%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 5s -60%
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 5s 3s +67%
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 1s 2s -50%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 8s 5s +60%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 1s +100%
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* ✅ 9s 5s +80%
poly_getnoise_eta1122_4x_native LP64 z3* ✅ 2s 1s +100%
poly_invntt_tomont_native LP64 z3* ✅ 4s 2s +100%
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* ✅ 2s 39s -95%
poly_reduce_native_aarch64 LP64 z3* ✅ 4s 2s +100%
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* ✅ 3s 3s +0%
poly_tomont_native_aarch64 LP64 z3* ✅ 4s 1s +300%
poly_tomont_native_x86_64 LP64 z3* ✅ 2s 1s +100%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 z3* ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 4s 4s +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* ✅ 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* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 20s 14s +43%
rej_uniform_native LP64 bitwuzla* ✅ 3s 2s +50%
rej_uniform_native_aarch64 LP64 z3* ✅ 57s 45s +27%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 142s 55s +158%
sys_check_capability LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2722s 1885s +44.4%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 445s 9s +4844%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 214s 79s +171%
mlk_rej_uniform_c LP64 z3* ⚠️ 242s 144s +68%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 197s 67s +194%
Full Results (195 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2722s 1885s +44.4%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
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* ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 6s 3s +100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 4s 2s +100%
keccakf1600_permute_native LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 17s 15s +13%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 4s 2s +100%
kem_check_pk LP64 z3* ✅ 4s 4s +0%
kem_check_sk LP64 z3* ✅ 4s 3s +33%
kem_dec LP64 z3* ✅ 10s 5s +100%
kem_enc LP64 z3* ✅ 4s 2s +100%
kem_enc_derand LP64 z3* ✅ 5s 3s +67%
kem_keypair LP64 z3* ✅ 2s 2s +0%
kem_keypair_derand LP64 z3* ✅ 4s 1s +300%
mlk_barrett_reduce LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 2s 1s +100%
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* ✅ 2s 1s +100%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 3s 3s +0%
ILP32 cvc5_arrays_exp ✅ 3s 3s +0%
ILP32 z3 ✅ 2s 3s -33%
LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 4s 3s +33%
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
mlk_ct_memcmp LP64 bitwuzla* ✅ 3s 3s +0%
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* ✅ 4s 4s +0%
mlk_fqmul LP64 z3* ✅ 3s 20s -85%
mlk_gen_matrix LP64 z3* ✅ 5s 2s +150%
mlk_gen_matrix_serial LP64 z3* ✅ 6s 4s +50%
mlk_indcpa_dec LP64 z3* ✅ 18s 11s +64%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 475s 402s +18%
mlk_indcpa_keypair_derand LP64 z3* ✅ 181s 176s +3%
mlk_invntt_layer LP64 z3* ✅ 7s 6s +17%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 6s 4s +50%
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 8s 5s +60%
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 10s -30%
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 10s 9s +11%
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 32s 26s +23%
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
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* ✅ 5s 6s -17%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 3s 1s +200%
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* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 z3* ✅ 1s 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* ✅ 4s 5s -20%
mlk_montgomery_reduce LP64 z3* ✅ 1s 2s -50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 445s 9s +4844%
mlk_ntt_layer LP64 z3* ✅ 8s 38s -79%
mlk_poly_add LP64 z3* ✅ 7s 5s +40%
mlk_poly_cbd_eta1 LP64 z3* ✅ 2s 3s -33%
mlk_poly_cbd_eta2 LP64 z3* ✅ 4s 3s +33%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_poly_compress_d10_c LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 3s 3s +0%
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* ✅ 1s 3s -67%
mlk_poly_compress_d4_c LP64 z3* ✅ 3s 4s -25%
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* ✅ 3s 4s -25%
mlk_poly_compress_du LP64 bitwuzla* ✅ 4s 2s +100%
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 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* ✅ 19s 16s +19%
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d4_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 4s 3s +33%
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_poly_decompress_d5_c LP64 z3* ✅ 4s 2s +100%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 17s 18s -6%
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_frombytes LP64 bitwuzla* ✅ 3s 2s +50%
mlk_poly_frombytes_c LP64 z3* ✅ 4s 3s +33%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 17s 10s +70%
mlk_poly_frommsg LP64 z3* ✅ 4s 10s -60%
mlk_poly_getnoise_eta1122_4x LP64 z3* ✅ 2s 3s -33%
mlk_poly_getnoise_eta1_4x LP64 z3* ✅ 6s 2s +200%
mlk_poly_getnoise_eta1_4x_native LP64 z3* ✅ 5s 3s +67%
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* ✅ 2s 2s +0%
mlk_poly_mulcache_compute LP64 z3* ✅ 1s 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* ✅ 9s 8s +12%
mlk_poly_ntt_c LP64 z3* ✅ 3s 1s +200%
mlk_poly_reduce LP64 bitwuzla* ✅ 4s 2s +100%
mlk_poly_reduce_c LP64 z3* ✅ 2s 1s +100%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 48s 40s +20%
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 43s 161s -73%
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 7s 7s +0%
mlk_poly_sub LP64 z3* ✅ 8s 8s +0%
mlk_poly_tobytes LP64 bitwuzla* ✅ 1s 3s -67%
mlk_poly_tobytes_c LP64 z3* ✅ 2s 4s -50%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 4s 1s +300%
mlk_poly_tomont LP64 z3* ✅ 3s 2s +50%
mlk_poly_tomont_c LP64 z3* ✅ 5s 3s +67%
mlk_poly_tomont_native LP64 z3* ✅ 2s 4s -50%
mlk_poly_tomsg LP64 bitwuzla* ✅ 4s 3s +33%
mlk_polymat_permute_bitrev_to_custom LP64 z3* ✅ 4s 5s -20%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 120s - new
mlk_polyvec_add LP64 z3* ✅ 24s 18s +33%
mlk_polyvec_basemul_acc_montgomery_cached LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 214s 79s +171%
mlk_polyvec_compress_du LP64 z3* ✅ 1s 3s -67%
mlk_polyvec_decompress_du LP64 z3* ✅ 1s 2s -50%
mlk_polyvec_frombytes LP64 z3* ✅ 2s 5s -60%
mlk_polyvec_invntt_tomont LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_mulcache_compute LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_ntt LP64 z3* ✅ 3s 12s -75%
mlk_polyvec_reduce LP64 z3* ✅ 4s 2s +100%
mlk_polyvec_tobytes LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tomont LP64 z3* ✅ 5s 2s +150%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 2s +0%
mlk_rej_uniform_c LP64 z3* ⚠️ 242s 144s +68%
mlk_scalar_compress_d1 LP64 z3* ✅ 3s 3s +0%
mlk_scalar_compress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d11 LP64 z3* ✅ 4s 4s +0%
mlk_scalar_compress_d4 LP64 z3* ✅ 2s 1s +100%
mlk_scalar_compress_d5 LP64 z3* ✅ 1s 4s -75%
mlk_scalar_decompress_d10 LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d11 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d4 LP64 z3* ✅ 3s 3s +0%
mlk_scalar_decompress_d5 LP64 z3* ✅ 3s 2s +50%
mlk_scalar_signed_to_unsigned_q LP64 z3* ✅ 2s 3s -33%
mlk_sha3_256 LP64 bitwuzla* ✅ 2s 2s +0%
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 1s +100%
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
mlk_shake256 LP64 bitwuzla* ✅ 1s 1s +0%
mlk_shake256x4 LP64 bitwuzla* ✅ 5s 4s +25%
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 2s 3s -33%
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 3s 3s +0%
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 3s 1s +200%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_x86_64 LP64 z3* ✅ 1s 2s -50%
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* ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 4s 4s +0%
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 7s 5s +40%
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 1s 2s -50%
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
poly_getnoise_eta1122_4x_native LP64 z3* ✅ 2s 3s -33%
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* ✅ 3s 43s -93%
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* ✅ 2s 3s -33%
poly_tobytes_native_x86_64 LP64 z3* ✅ 4s 3s +33%
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* ✅ 4s 1s +300%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 z3* ✅ 5s 2s +150%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 z3* ✅ 5s 2s +150%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 z3* ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_native LP64 z3* ✅ 31s 31s +0%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
rej_uniform_native_aarch64 LP64 z3* ✅ 51s 53s -4%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 197s 67s +194%
sys_check_capability LP64 z3* ✅ 2s 2s +0%

@mkannwischer

mkannwischer commented Oct 1, 2026

Copy link
Copy Markdown
Contributor Author

clang23 is now fixed in nixpkgs-unstable, but unfortuantely CBMC broke in the meantime. I'll fix that in nixpkgs and then update.

@mkannwischer
CI: Add clang23 tests and constant-time tests
d41f111 
Signed-off-by: Matthias J. Kannwischer <[email protected]>
@mkannwischer

mkannwischer commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

clang23 is now fixed in nixpkgs-unstable, but unfortuantely CBMC broke in the meantime. I'll fix that in nixpkgs and then update.

It has been fixed in NixOS/nixpkgs#568925 which is now in nixpkgs-unstable.
That hopefully fixes it for us.

@mkannwischer mkannwischer added the legacy-compiler-tests Triggers legacy compiler tests in CI label Oct 5, 2026
@mkannwischer
mkannwischer marked this pull request as ready for review October 5, 2026 08:17
@mkannwischer
mkannwischer requested a review from a team as a code owner October 5, 2026 08:17
hanno-becker
hanno-becker reviewed Oct 5, 2026
View reviewed changes
Comment thread .github/workflows/ct-tests.yml
@hanno-becker
hanno-becker added this pull request to the merge queue Oct 5, 2026
Any commits made after this event will not be merged.

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

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

Assignees

No one assigned

Labels

legacy-compiler-tests Triggers legacy compiler tests in CI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkannwischer @oqs-bot @hanno-becker