Skip to content

mldsa: Clean-up includes - #1481

Open
mkannwischer wants to merge 2 commits into
mainfrom
include-cleanup
Open

mldsa: Clean-up includes#1481
mkannwischer wants to merge 2 commits into
mainfrom
include-cleanup

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Oct 20, 2026

Copy link
Copy Markdown
Contributor

Resolves the concern raised by #1480 (comment). Turns out this was a artifact of how our autogen script worked.

@mkannwischer mkannwischer added this to the v2.1 milestone Oct 20, 2026
@oqs-bot

oqs-bot commented Oct 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 33s 7s +371%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 162s 31s +423%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 31s 5s +520%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 168s 71s +137%
Full Results (226 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1204s 1482s -18.8%
caddq LP64 z3* ✅ 3s 2s +50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 33s 7s +371%
decompose LP64 z3* ✅ 1s 4s -75%
fqmul LP64 bitwuzla* ✅ 22s 40s -45%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
intt_native_aarch64 LP64 z3* ✅ 1s 2s -50%
intt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 1s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 3s 4s -25%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 10s -40%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_finalize LP64 z3* ✅ 3s 2s +50%
keccak_init LP64 z3* ✅ 3s 4s -25%
keccak_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute LP64 z3* ✅ 2s 4s -50%
keccakf1600_permute_native LP64 z3* ✅ 1s 2s -50%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 1s +0%
keccakf1600x4_permute LP64 z3* ✅ 1s 1s +0%
keccakf1600x4_permute_native LP64 z3* ✅ 13s 22s -41%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
make_hint LP64 z3* ✅ 1s 3s -67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 162s 31s +423%
mld_check_pct LP64 z3* ✅ 4s 12s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 5s -20%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 6s -83%
ILP32 cvc5_arrays_exp ✅ 2s 6s -67%
ILP32 z3 ✅ 1s 6s -83%
LP64 bitwuzla ✅ 2s 6s -67%
LP64 cvc5_arrays_exp ✅ 1s 6s -83%
LP64 z3* ✅ 1s 6s -83%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 3s 3s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 3s 1s +200%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 4s -50%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 4s -75%
mld_ct_sel_int32 LP64 z3* ✅ 2s 2s +0%
mld_h LP64 z3* ✅ 2s 3s -33%
mld_invntt_layer LP64 bitwuzla* ✅ 54s 108s -50%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 2s 7s -71%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 10s 25s -60%
mld_ntt_layer LP64 bitwuzla* ✅ 21s 43s -51%
mld_polymat_expand_entry LP64 z3* ✅ 2s 3s -33%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 1s 4s -75%
mld_sample_pack_s1_s2 LP64 z3* ✅ 3s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 2s - new
mld_sign_attempt LP64 z3* ✅ 2s - new
mld_sign_finish LP64 z3* ✅ 1s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 1s 4s -75%
mld_value_barrier_u8 LP64 z3* ✅ 1s 1s +0%
montgomery_reduce LP64 z3* ✅ 1s 1s +0%
ntt_native_aarch64 LP64 z3* ✅ 1s 3s -67%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 3s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 3s 5s -40%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
pack_sig_c LP64 z3* ✅ 2s 3s -33%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 2s +0%
pack_sig_z LP64 z3* ✅ 4s 1s +300%
pack_sk_rho_key_tr LP64 z3* ✅ 2s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 6s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 5s -40%
pointwise_native_aarch64 LP64 z3* ✅ 3s 3s +0%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
pointwise_native_x86_64 LP64 z3* ✅ 5s 2s +150%
poly_add LP64 z3* ✅ 3s 7s -57%
poly_caddq LP64 z3* ✅ 1s 3s -67%
poly_caddq_c LP64 z3* ✅ 2s 5s -60%
poly_caddq_native LP64 z3* ✅ 3s 4s -25%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_caddq_native_x86_64 LP64 z3* ✅ 1s 1s +0%
poly_challenge LP64 z3* ✅ 5s 5s +0%
poly_chknorm LP64 z3* ✅ 3s 3s +0%
poly_chknorm_c LP64 z3* ✅ 8s 13s -38%
poly_chknorm_native LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 4s -75%
poly_decompose LP64 z3* ✅ 3s 2s +50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_decompose_c LP64 z3* ✅ 6s 8s -25%
poly_decompose_native LP64 z3* ✅ 2s 5s -60%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_invntt_tomont LP64 z3* ✅ 2s 5s -60%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 5s 10s -50%
poly_invntt_tomont_native LP64 z3* ✅ 2s 5s -60%
poly_ntt LP64 z3* ✅ 4s 2s +100%
poly_ntt_c LP64 z3_smt_only* ✅ 11s 22s -50%
poly_ntt_native LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 1s 3s -67%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery LP64 z3* ✅ 4s 2s +100%
poly_pointwise_montgomery_c LP64 z3* ✅ 63s 116s -46%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 4s -75%
poly_power2round LP64 z3* ✅ 4s 7s -43%
poly_reduce LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 z3* ✅ 2s 3s -33%
poly_sub LP64 z3* ✅ 3s 4s -25%
poly_uniform LP64 z3* ✅ 2s 2s +0%
poly_uniform_4x LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta LP64 z3* ✅ 1s 5s -80%
poly_uniform_eta_4x LP64 z3* ✅ 8s 13s -38%
poly_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 3s -67%
poly_use_hint LP64 z3* ✅ 1s 3s -67%
poly_use_hint_c LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native LP64 z3* ✅ 2s 7s -71%
poly_use_hint_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_use_hint_native_x86_64 LP64 z3* ✅ 3s - new
polyeta_pack LP64 z3* ✅ 4s 1s +300%
polyeta_unpack LP64 z3* ✅ 2s 4s -50%
polyt0_pack LP64 z3* ✅ 3s 5s -40%
polyt0_unpack LP64 z3* ✅ 6s 13s -54%
polyt1_pack LP64 z3* ✅ 1s 3s -67%
polyt1_unpack LP64 z3* ✅ 4s 3s +33%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 6s -83%
polyvec_matrix_expand_serial LP64 z3* ✅ 1s 3s -67%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 8s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 99s 201s -51%
polyveck_caddq LP64 z3* ✅ 2s 7s -71%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 3s 7s -57%
polyveck_ntt LP64 z3* ✅ 1s 4s -75%
polyveck_reduce LP64 z3* ✅ 5s 6s -17%
polyveck_unpack_eta LP64 z3* ✅ 3s 3s +0%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 1s 43s -98%
polyvecl_ntt LP64 z3* ✅ 4s 7s -43%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_uniform_gamma1 LP64 z3* ✅ 3s 4s -25%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 1s +200%
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 3s 1s +200%
polyw1_pack LP64 z3* ✅ 3s 3s +0%
polyw1_pack_32 LP64 z3* ✅ 2s 2s +0%
polyw1_pack_88 LP64 z3* ✅ 1s 3s -67%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 1s - new
polyz_pack LP64 z3* ✅ 2s 3s -33%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 3s 2s +50%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 5s -60%
polyz_unpack_c LP64 z3* ✅ 4s 9s -56%
polyz_unpack_native LP64 z3* ✅ 1s 3s -67%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 1s 2s -50%
reduce32 LP64 z3* ✅ 2s 2s +0%
rej_eta LP64 bitwuzla* ✅ 3s 5s -40%
rej_eta_c LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_native LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform LP64 z3* ✅ 5s 7s -29%
rej_uniform_c LP64 z3* ✅ 8s 16s -50%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 5s -60%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 5s -80%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 7s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 z3* ✅ 1s 6s -83%
shake128_release LP64 z3* ✅ 2s 2s +0%
shake128_squeeze LP64 bitwuzla* ✅ 1s 3s -67%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
shake256 LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 z3* ✅ 2s 4s -50%
shake256_finalize LP64 z3* ✅ 1s 1s +0%
shake256_init LP64 z3* ✅ 1s 4s -75%
shake256_release LP64 z3* ✅ 2s 3s -33%
shake256_squeeze LP64 bitwuzla* ✅ 1s 4s -75%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 4s 2s +100%
sig_unpack_hints LP64 z3* ✅ 14s 1s +1300%
sign_keypair LP64 z3* ✅ 5s 4s +25%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 17s 3s +467%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 31s 5s +520%
sign_signature LP64 z3* ✅ 4s 5s -20%
sign_signature_extmu LP64 z3* ✅ 2s 4s -50%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 6s +133%
sign_signature_pre_hash_internal LP64 z3* ✅ 4s 3s +33%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 2s 7s -71%
sign_verify LP64 z3* ✅ 4s 6s -33%
sign_verify_extmu LP64 z3* ✅ 2s 2s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 168s 71s +137%
sign_verify_pre_hash_internal LP64 z3* ✅ 2s 5s -60%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 6s -67%
sk_s1hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 2s 1s +100%
sk_t0hat_get_poly LP64 z3* ✅ 2s 1s +100%
sys_check_capability LP64 z3* ✅ 2s 1s +100%
unpack_pk_t1 LP64 z3* ✅ 1s 2s -50%
unpack_sk LP64 z3* ✅ 2s 3s -33%
unpack_sk_s1hat LP64 z3* ✅ 4s 1s +300%
unpack_sk_s2hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_t0hat LP64 z3* ✅ 4s 4s +0%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 1s 5s -80%

@oqs-bot

oqs-bot commented Oct 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 139s 19s +632%
sig_unpack_hints LP64 z3* ⚠️ 36s 2s +1700%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 28s 5s +460%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 240s 49s +390%
Full Results (226 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1329s 1364s -2.6%
caddq LP64 z3* ✅ 2s 6s -67%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
decompose LP64 z3* ✅ 2s 3s -33%
fqmul LP64 bitwuzla* ✅ 23s 39s -41%
fqscale LP64 bitwuzla* ✅ 1s 2s -50%
intt_native_aarch64 LP64 z3* ✅ 4s 3s +33%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 3s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 z3* ✅ 1s 2s -50%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 8s -38%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
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 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_finalize LP64 z3* ✅ 3s 2s +50%
keccak_init LP64 z3* ✅ 3s 3s +0%
keccak_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 3s 4s -25%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 6s -83%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
keccakf1600x4_permute_native LP64 z3* ✅ 13s 22s -41%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 5s -40%
make_hint LP64 z3* ✅ 3s 3s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 139s 19s +632%
mld_check_pct LP64 z3* ✅ 5s 15s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 6s -67%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 3s -33%
ILP32 cvc5_arrays_exp ✅ 2s 3s -33%
ILP32 z3 ✅ 3s 3s +0%
LP64 bitwuzla ✅ 3s 3s +0%
LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 2s +50%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 3s 4s -25%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 1s +0%
mld_ct_sel_int32 LP64 z3* ✅ 2s 3s -33%
mld_h LP64 z3* ✅ 3s 4s -25%
mld_invntt_layer LP64 bitwuzla* ✅ 61s 105s -42%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 2s 7s -71%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 4s -50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 3s 4s -25%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 13s 23s -43%
mld_ntt_layer LP64 bitwuzla* ✅ 24s 41s -41%
mld_polymat_expand_entry LP64 z3* ✅ 1s 2s -50%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 1s 3s -67%
mld_sample_pack_s1_s2 LP64 z3* ✅ 4s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 1s - new
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 3s - new
mld_value_barrier_i64 LP64 z3* ✅ 1s 3s -67%
mld_value_barrier_u32 LP64 z3* ✅ 2s 1s +100%
mld_value_barrier_u8 LP64 z3* ✅ 3s 4s -25%
montgomery_reduce LP64 z3* ✅ 2s 2s +0%
ntt_native_aarch64 LP64 z3* ✅ 2s 4s -50%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 4s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 3s 3s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 4s -75%
pack_sig_c LP64 z3* ✅ 1s 5s -80%
pack_sig_h LP64 z3_no_bv_extract* ✅ 4s 4s +0%
pack_sig_z LP64 z3* ✅ 2s 2s +0%
pack_sk_rho_key_tr LP64 z3* ✅ 3s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 4s -25%
pointwise_native_aarch64 LP64 z3* ✅ 1s 2s -50%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 1s 4s -75%
poly_add LP64 z3* ✅ 3s 7s -57%
poly_caddq LP64 z3* ✅ 2s 4s -50%
poly_caddq_c LP64 z3* ✅ 3s 3s +0%
poly_caddq_native LP64 z3* ✅ 4s 3s +33%
poly_caddq_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_challenge LP64 z3* ✅ 1s 6s -83%
poly_chknorm LP64 z3* ✅ 3s 3s +0%
poly_chknorm_c LP64 z3* ✅ 7s 11s -36%
poly_chknorm_native LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 z3* ✅ 1s 2s -50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_decompose_c LP64 z3* ✅ 3s 5s -40%
poly_decompose_native LP64 z3* ✅ 2s 2s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 4s 2s +100%
poly_invntt_tomont LP64 z3* ✅ 1s 2s -50%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 11s -45%
poly_invntt_tomont_native LP64 z3* ✅ 2s 3s -33%
poly_ntt LP64 z3* ✅ 4s 3s +33%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 21s -52%
poly_ntt_native LP64 z3* ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 5s -60%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery_c LP64 z3* ✅ 66s 112s -41%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 2s +0%
poly_power2round LP64 z3* ✅ 4s 4s +0%
poly_reduce LP64 z3* ✅ 3s 4s -25%
poly_shiftl LP64 z3* ✅ 1s 4s -75%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 4s 3s +33%
poly_uniform_4x LP64 z3* ✅ 3s 3s +0%
poly_uniform_eta LP64 z3* ✅ 3s 2s +50%
poly_uniform_eta_4x LP64 z3* ✅ 7s 12s -42%
poly_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 5s -60%
poly_use_hint LP64 z3* ✅ 2s 2s +0%
poly_use_hint_c LP64 z3* ✅ 5s 5s +0%
poly_use_hint_native LP64 z3* ✅ 1s 3s -67%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 6s 14s -57%
polyt0_pack LP64 z3* ✅ 1s 4s -75%
polyt0_unpack LP64 z3* ✅ 9s 12s -25%
polyt1_pack LP64 z3* ✅ 2s 3s -33%
polyt1_unpack LP64 z3* ✅ 2s 2s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 3s 3s +0%
polyvec_matrix_expand_serial LP64 z3* ✅ 3s 4s -25%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 3s 6s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 121s 149s -19%
polyveck_caddq LP64 z3* ✅ 1s 3s -67%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 2s 5s -60%
polyveck_ntt LP64 z3* ✅ 3s 2s +50%
polyveck_reduce LP64 z3* ✅ 2s 4s -50%
polyveck_unpack_eta LP64 z3* ✅ 3s 2s +50%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 3s - new
polyvecl_chknorm LP64 z3* ✅ 3s 11s -73%
polyvecl_ntt LP64 z3* ✅ 5s 3s +67%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 4s 3s +33%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 1s 4s -75%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 3s 3s +0%
polyvecl_uniform_gamma1 LP64 z3* ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 1s 2s -50%
polyvecl_unpack_eta LP64 z3* ✅ 3s 4s -25%
polyvecl_unpack_z LP64 z3* ✅ 1s 3s -67%
polyw1_pack LP64 z3* ✅ 3s 4s -25%
polyw1_pack_32 LP64 z3* ✅ 2s 3s -33%
polyw1_pack_88 LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 1s 2s -50%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_c LP64 z3* ✅ 7s 8s -12%
polyz_unpack_native LP64 z3* ✅ 2s 3s -33%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 2s 2s +0%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 3s 5s -40%
rej_eta_c LP64 bitwuzla* ✅ 1s 4s -75%
rej_eta_native LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform LP64 z3* ✅ 4s 8s -50%
rej_uniform_c LP64 z3* ✅ 10s 16s -38%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 4s 5s -20%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 9s - new
shake128_absorb LP64 z3* ✅ 4s 3s +33%
shake128_finalize LP64 z3* ✅ 3s 3s +0%
shake128_init LP64 z3* ✅ 1s 2s -50%
shake128_release LP64 z3* ✅ 1s 2s -50%
shake128_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
shake256 LP64 z3* ✅ 2s 1s +100%
shake256_absorb LP64 z3* ✅ 3s 2s +50%
shake256_finalize LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 z3* ✅ 3s 4s -25%
shake256_release LP64 z3* ✅ 1s 1s +0%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 1s +200%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
sig_unpack_hints LP64 z3* ⚠️ 36s 2s +1700%
sign_keypair LP64 z3* ✅ 5s 5s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 12s 4s +200%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 28s 5s +460%
sign_signature LP64 z3* ✅ 3s 6s -50%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 15s 4s +275%
sign_signature_pre_hash_internal LP64 z3* ✅ 4s 4s +0%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 3s 4s -25%
sign_verify LP64 z3* ✅ 1s 4s -75%
sign_verify_extmu LP64 z3* ✅ 2s 5s -60%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 240s 49s +390%
sign_verify_pre_hash_internal LP64 z3* ✅ 2s 5s -60%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 5s -60%
sk_s1hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_s2hat_get_poly LP64 z3* ✅ 2s 5s -60%
sk_t0hat_get_poly LP64 z3* ✅ 1s 1s +0%
sys_check_capability LP64 z3* ✅ 2s 2s +0%
unpack_pk_t1 LP64 z3* ✅ 2s 3s -33%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 z3* ✅ 1s 3s -67%
unpack_sk_s2hat LP64 z3* ✅ 3s 4s -25%
unpack_sk_t0hat LP64 z3* ✅ 2s 2s +0%
use_hint LP64 z3* ✅ 1s 2s -50%
yvec_get_poly LP64 z3* ✅ 1s 3s -67%
yvec_init LP64 z3* ✅ 2s 1s +100%

@oqs-bot

oqs-bot commented Oct 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87, REDUCE-RAM)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 26s 12s +117%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 160s 34s +371%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 23s 6s +283%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 208s 47s +343%
Full Results (226 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1235s 1436s -14.0%
caddq LP64 z3* ✅ 2s 3s -33%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 26s 12s +117%
decompose LP64 z3* ✅ 3s 2s +50%
fqmul LP64 bitwuzla* ✅ 21s 39s -46%
fqscale LP64 bitwuzla* ✅ 2s 1s +100%
intt_native_aarch64 LP64 z3* ✅ 2s 4s -50%
intt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 1s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 z3* ✅ 3s 4s -25%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 8s -50%
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* ✅ 4s 1s +300%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 3s -67%
keccak_finalize LP64 z3* ✅ 1s 1s +0%
keccak_init LP64 z3* ✅ 2s 1s +100%
keccak_squeeze LP64 bitwuzla* ✅ 1s 5s -80%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 3s 3s +0%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_permute LP64 z3* ✅ 1s 2s -50%
keccakf1600x4_permute_native LP64 z3* ✅ 11s 25s -56%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
make_hint LP64 z3* ✅ 3s 2s +50%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 160s 34s +371%
mld_check_pct LP64 z3* ✅ 5s 15s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 3s 6s -50%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 1s +100%
ILP32 cvc5_arrays_exp ✅ 2s 1s +100%
ILP32 z3 ✅ 1s 1s +0%
LP64 bitwuzla ✅ 3s 1s +200%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 3s 5s -40%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 1s +100%
mld_ct_sel_int32 LP64 z3* ✅ 4s 2s +100%
mld_h LP64 z3* ✅ 3s 2s +50%
mld_invntt_layer LP64 bitwuzla* ✅ 54s 111s -51%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 1s +100%
mld_keccakf1600_permute_c LP64 z3* ✅ 3s 8s -62%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 3s -33%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 1s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 23s -48%
mld_ntt_layer LP64 bitwuzla* ✅ 21s 44s -52%
mld_polymat_expand_entry LP64 z3* ✅ 2s 4s -50%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 2s 3s -33%
mld_sample_pack_s1_s2 LP64 z3* ✅ 7s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 3s - new
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 1s - new
mld_value_barrier_i64 LP64 z3* ✅ 1s 2s -50%
mld_value_barrier_u32 LP64 z3* ✅ 1s 3s -67%
mld_value_barrier_u8 LP64 z3* ✅ 2s 2s +0%
montgomery_reduce LP64 z3* ✅ 3s 2s +50%
ntt_native_aarch64 LP64 z3* ✅ 4s 4s +0%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 1s 2s -50%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
pack_sig_c LP64 z3* ✅ 3s 2s +50%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 3s -33%
pack_sig_z LP64 z3* ✅ 3s 3s +0%
pack_sk_rho_key_tr LP64 z3* ✅ 1s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 5s -40%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 8s -62%
pointwise_native_aarch64 LP64 z3* ✅ 2s 4s -50%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 3s 5s -40%
poly_add LP64 z3* ✅ 2s 8s -75%
poly_caddq LP64 z3* ✅ 2s 5s -60%
poly_caddq_c LP64 z3* ✅ 3s 3s +0%
poly_caddq_native LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_challenge LP64 z3* ✅ 5s 4s +25%
poly_chknorm LP64 z3* ✅ 1s 4s -75%
poly_chknorm_c LP64 z3* ✅ 7s 13s -46%
poly_chknorm_native LP64 z3* ✅ 2s 1s +100%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 5s -60%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_decompose LP64 z3* ✅ 1s 2s -50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_decompose_c LP64 z3* ✅ 4s 6s -33%
poly_decompose_native LP64 z3* ✅ 3s 2s +50%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_invntt_tomont LP64 z3* ✅ 1s 4s -75%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 9s -33%
poly_invntt_tomont_native LP64 z3* ✅ 3s 2s +50%
poly_ntt LP64 z3* ✅ 3s 2s +50%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 19s -47%
poly_ntt_native LP64 z3* ✅ 1s 4s -75%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 1s 2s -50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery_c LP64 z3* ✅ 65s 125s -48%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 3s -67%
poly_power2round LP64 z3* ✅ 2s 7s -71%
poly_reduce LP64 z3* ✅ 1s 4s -75%
poly_shiftl LP64 z3* ✅ 3s 4s -25%
poly_sub LP64 z3* ✅ 1s 5s -80%
poly_uniform LP64 z3* ✅ 2s 4s -50%
poly_uniform_4x LP64 z3* ✅ 2s 3s -33%
poly_uniform_eta LP64 z3* ✅ 1s 5s -80%
poly_uniform_eta_4x LP64 z3* ✅ 7s 12s -42%
poly_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 3s -67%
poly_use_hint LP64 z3* ✅ 2s 4s -50%
poly_use_hint_c LP64 z3* ✅ 3s 4s -25%
poly_use_hint_native LP64 z3* ✅ 2s 1s +100%
poly_use_hint_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 1s 3s -67%
polyeta_unpack LP64 z3* ✅ 7s 13s -46%
polyt0_pack LP64 z3* ✅ 3s 3s +0%
polyt0_unpack LP64 z3* ✅ 7s 14s -50%
polyt1_pack LP64 z3* ✅ 1s 5s -80%
polyt1_unpack LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 3s -67%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 5s 13s -62%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 79s 196s -60%
polyveck_caddq LP64 z3* ✅ 3s 8s -62%
polyveck_decompose_pack_w1 LP64 z3* ✅ 12s - new
polyveck_invntt_tomont LP64 z3* ✅ 3s 4s -25%
polyveck_ntt LP64 z3* ✅ 1s 3s -67%
polyveck_reduce LP64 z3* ✅ 4s 6s -33%
polyveck_unpack_eta LP64 z3* ✅ 2s 3s -33%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 1s 38s -97%
polyvecl_ntt LP64 z3* ✅ 2s 8s -75%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 2s -50%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_eta LP64 z3* ✅ 1s 3s -67%
polyvecl_unpack_z LP64 z3* ✅ 3s 3s +0%
polyw1_pack LP64 z3* ✅ 3s 2s +50%
polyw1_pack_32 LP64 z3* ✅ 1s 3s -67%
polyw1_pack_88 LP64 z3* ✅ 1s 2s -50%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 1s - new
polyz_pack LP64 z3* ✅ 4s 4s +0%
polyz_unpack LP64 z3* ✅ 3s 3s +0%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 3s 5s -40%
polyz_unpack_c LP64 z3* ✅ 4s 7s -43%
polyz_unpack_native LP64 z3* ✅ 3s 1s +200%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 1s 3s -67%
reduce32 LP64 z3* ✅ 3s 3s +0%
rej_eta LP64 bitwuzla* ✅ 2s 2s +0%
rej_eta_c LP64 bitwuzla* ✅ 3s 4s -25%
rej_eta_native LP64 bitwuzla* ✅ 3s 4s -25%
rej_uniform LP64 z3* ✅ 5s 7s -29%
rej_uniform_c LP64 z3* ✅ 9s 18s -50%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 2s 5s -60%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 1s 2s -50%
shake128_finalize LP64 z3* ✅ 1s 2s -50%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 3s 3s +0%
shake128_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 4s -75%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
shake256 LP64 z3* ✅ 2s 3s -33%
shake256_absorb LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 z3* ✅ 1s 3s -67%
shake256_init LP64 z3* ✅ 2s 3s -33%
shake256_release LP64 z3* ✅ 3s 5s -40%
shake256_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 5s -60%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 4s -50%
sig_unpack_hints LP64 z3* ✅ 15s 4s +275%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 23s 6s +283%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_signature LP64 z3* ✅ 2s 4s -50%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 12s 3s +300%
sign_signature_pre_hash_internal LP64 z3* ✅ 4s 2s +100%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 3s 3s +0%
sign_verify LP64 z3* ✅ 2s 2s +0%
sign_verify_extmu LP64 z3* ✅ 3s 4s -25%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 208s 47s +343%
sign_verify_pre_hash_internal LP64 z3* ✅ 2s 3s -33%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 7s -71%
sk_s1hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 z3* ✅ 2s 3s -33%
sys_check_capability LP64 z3* ✅ 1s 2s -50%
unpack_pk_t1 LP64 z3* ✅ 3s 2s +50%
unpack_sk LP64 z3* ✅ 3s 4s -25%
unpack_sk_s1hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_s2hat LP64 z3* ✅ 1s 3s -67%
unpack_sk_t0hat LP64 z3* ✅ 2s 4s -50%
use_hint LP64 z3* ✅ 3s 3s +0%
yvec_get_poly LP64 z3* ✅ 3s 2s +50%
yvec_init LP64 z3* ✅ 3s 4s -25%

@oqs-bot

oqs-bot commented Oct 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 1958s 1514s +29.3%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 87s 50s +74%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 364s 58s +528%
sig_unpack_hints LP64 z3* ⚠️ 24s 2s +1100%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 31s 5s +520%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 217s 26s +735%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 336s 114s +195%
Full Results (226 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 1958s 1514s +29.3%
caddq LP64 z3* ✅ 2s 2s +0%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 87s 50s +74%
decompose LP64 z3* ✅ 2s 2s +0%
fqmul LP64 bitwuzla* ✅ 24s 39s -38%
fqscale LP64 bitwuzla* ✅ 1s 3s -67%
intt_native_aarch64 LP64 z3* ✅ 1s 9s -89%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 3s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 z3* ✅ 2s 5s -60%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 9s -44%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 3s -67%
keccak_finalize LP64 z3* ✅ 1s 3s -67%
keccak_init LP64 z3* ✅ 1s 3s -67%
keccak_squeeze LP64 bitwuzla* ✅ 3s 1s +200%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 3s 2s +50%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
keccakf1600x4_permute_native LP64 z3* ✅ 13s 22s -41%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 3s -33%
make_hint LP64 z3* ✅ 3s 3s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 364s 58s +528%
mld_check_pct LP64 z3* ✅ 5s 14s -64%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 7s -71%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 2s +0%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 1s 2s -50%
LP64 bitwuzla ✅ 3s 2s +50%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 4s -50%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 1s +0%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 1s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mld_ct_sel_int32 LP64 z3* ✅ 3s 2s +50%
mld_h LP64 z3* ✅ 3s 4s -25%
mld_invntt_layer LP64 bitwuzla* ✅ 64s 107s -40%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600_permute_c LP64 z3* ✅ 4s 8s -50%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 3s 2s +50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 13s 23s -43%
mld_ntt_layer LP64 bitwuzla* ✅ 24s 42s -43%
mld_polymat_expand_entry LP64 z3* ✅ 3s 3s +0%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 4s 4s +0%
mld_sample_pack_s1_s2 LP64 z3* ✅ 5s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 2s - new
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 1s 2s -50%
mld_value_barrier_u8 LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 z3* ✅ 1s 3s -67%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 z3* ✅ 3s 3s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 1s +100%
pack_sig_c LP64 z3* ✅ 1s 2s -50%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 3s -33%
pack_sig_z LP64 z3* ✅ 5s 4s +25%
pack_sk_rho_key_tr LP64 z3* ✅ 2s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 2s 4s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 7s -57%
pointwise_native_aarch64 LP64 z3* ✅ 4s 5s -20%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 3s 4s -25%
poly_add LP64 z3* ✅ 6s 7s -14%
poly_caddq LP64 z3* ✅ 3s 2s +50%
poly_caddq_c LP64 z3* ✅ 2s 2s +0%
poly_caddq_native LP64 z3* ✅ 3s 5s -40%
poly_caddq_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_caddq_native_x86_64 LP64 z3* ✅ 1s 4s -75%
poly_challenge LP64 z3* ✅ 4s 3s +33%
poly_chknorm LP64 z3* ✅ 3s 4s -25%
poly_chknorm_c LP64 z3* ✅ 8s 17s -53%
poly_chknorm_native LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_x86_64 LP64 z3* ✅ 4s 2s +100%
poly_decompose LP64 z3* ✅ 1s 3s -67%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 4s 4s +0%
poly_decompose_c LP64 z3* ✅ 2s 4s -50%
poly_decompose_native LP64 z3* ✅ 2s 3s -33%
poly_decompose_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_invntt_tomont LP64 z3* ✅ 3s 4s -25%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 5s 11s -55%
poly_invntt_tomont_native LP64 z3* ✅ 2s 4s -50%
poly_ntt LP64 z3* ✅ 3s 3s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 11s 19s -42%
poly_ntt_native LP64 z3* ✅ 2s 5s -60%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 5s 4s +25%
poly_pointwise_montgomery LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery_c LP64 z3* ✅ 48s 114s -58%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 2s +50%
poly_power2round LP64 z3* ✅ 3s 4s -25%
poly_reduce LP64 z3* ✅ 6s 3s +100%
poly_shiftl LP64 z3* ✅ 1s 3s -67%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 2s 6s -67%
poly_uniform_4x LP64 z3* ✅ 7s 14s -50%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
poly_uniform_eta_4x LP64 z3* ✅ 11s 11s +0%
poly_uniform_gamma1 LP64 z3* ✅ 1s 4s -75%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 5s -60%
poly_use_hint LP64 z3* ✅ 2s 4s -50%
poly_use_hint_c LP64 z3* ✅ 1s 3s -67%
poly_use_hint_native LP64 z3* ✅ 3s 4s -25%
poly_use_hint_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 5s 14s -64%
polyt0_pack LP64 z3* ✅ 3s 2s +50%
polyt0_unpack LP64 z3* ✅ 7s 15s -53%
polyt1_pack LP64 z3* ✅ 2s 4s -50%
polyt1_unpack LP64 z3* ✅ 3s 5s -40%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 13s 28s -54%
polyvec_matrix_expand_serial LP64 z3* ✅ 5s 8s -38%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 3s 2s +50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 13s 15s -13%
polyveck_caddq LP64 z3* ✅ 3s 3s +0%
polyveck_decompose_pack_w1 LP64 z3* ✅ 2s - new
polyveck_invntt_tomont LP64 z3* ✅ 2s 5s -60%
polyveck_ntt LP64 z3* ✅ 4s 5s -20%
polyveck_reduce LP64 z3* ✅ 3s 5s -40%
polyveck_unpack_eta LP64 z3* ✅ 4s 2s +100%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 4s - new
polyvecl_chknorm LP64 z3* ✅ 5s 10s -50%
polyvecl_ntt LP64 z3* ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 130s 131s -1%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 2s -50%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 2s +50%
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 3s 2s +50%
polyw1_pack LP64 z3* ✅ 2s 3s -33%
polyw1_pack_32 LP64 z3* ✅ 3s 2s +50%
polyw1_pack_88 LP64 z3* ✅ 2s 1s +100%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 1s - new
polyw1_unpack_88 LP64 z3* ✅ 3s - new
polyz_pack LP64 z3* ✅ 3s 2s +50%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 5s -60%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 1s 5s -80%
polyz_unpack_c LP64 z3* ✅ 6s 11s -45%
polyz_unpack_native LP64 z3* ✅ 1s 2s -50%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 3s 3s +0%
reduce32 LP64 z3* ✅ 3s 2s +50%
rej_eta LP64 bitwuzla* ✅ 1s 3s -67%
rej_eta_c LP64 bitwuzla* ✅ 3s 4s -25%
rej_eta_native LP64 bitwuzla* ✅ 2s 6s -67%
rej_uniform LP64 z3* ✅ 11s 18s -39%
rej_uniform_c LP64 z3* ✅ 12s 15s -20%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 3s 4s -25%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 5s -80%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 4s 2s +100%
shake128_init LP64 z3* ✅ 2s 3s -33%
shake128_release LP64 z3* ✅ 4s 1s +300%
shake128_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
shake256 LP64 z3* ✅ 1s 1s +0%
shake256_absorb LP64 z3* ✅ 3s 3s +0%
shake256_finalize LP64 z3* ✅ 2s 2s +0%
shake256_init LP64 z3* ✅ 2s 3s -33%
shake256_release LP64 z3* ✅ 2s 2s +0%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 4s -75%
sig_unpack_hints LP64 z3* ⚠️ 24s 2s +1100%
sign_keypair LP64 z3* ✅ 5s 4s +25%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 15s 4s +275%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 31s 5s +520%
sign_signature LP64 z3* ✅ 5s 3s +67%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 217s 26s +735%
sign_signature_pre_hash_internal LP64 z3* ✅ 3s 6s -50%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 4s 3s +33%
sign_verify LP64 z3* ✅ 3s 4s -25%
sign_verify_extmu LP64 z3* ✅ 3s 3s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 336s 114s +195%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 5s -20%
sk_s1hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 z3* ✅ 2s 2s +0%
sys_check_capability LP64 z3* ✅ 2s 4s -50%
unpack_pk_t1 LP64 z3* ✅ 2s 5s -60%
unpack_sk LP64 z3* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 z3* ✅ 2s 1s +100%
unpack_sk_s2hat LP64 z3* ✅ 2s 4s -50%
unpack_sk_t0hat LP64 z3* ✅ 2s 3s -33%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 4s 3s +33%
yvec_init LP64 z3* ✅ 4s 3s +33%

@oqs-bot

oqs-bot commented Oct 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 124s 13s +854%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 182s 63s +189%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 174s 55s +216%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 399s 177s +125%
Full Results (226 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1809s 1784s +1.4%
caddq LP64 z3* ✅ 3s 3s +0%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 124s 13s +854%
decompose LP64 z3* ✅ 1s 1s +0%
fqmul LP64 bitwuzla* ✅ 23s 40s -43%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 z3* ✅ 3s 3s +0%
keccak_absorb LP64 z3* ✅ 4s 3s +33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 8s -38%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 4s -25%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_finalize LP64 z3* ✅ 1s 2s -50%
keccak_init LP64 z3* ✅ 2s 1s +100%
keccak_squeeze LP64 bitwuzla* ✅ 1s 4s -75%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 5s -60%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute LP64 z3* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 z3* ✅ 3s 3s +0%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 23s -48%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 3s -67%
make_hint LP64 z3* ✅ 1s 2s -50%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 182s 63s +189%
mld_check_pct LP64 z3* ✅ 5s 14s -64%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 7s -43%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 2s -50%
ILP32 cvc5_arrays_exp ✅ 2s 2s +0%
ILP32 z3 ✅ 1s 2s -50%
LP64 bitwuzla ✅ 4s 2s +100%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 4s -50%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 3s -33%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 3s 2s +50%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 2s -50%
mld_ct_sel_int32 LP64 z3* ✅ 1s 3s -67%
mld_h LP64 z3* ✅ 4s 2s +100%
mld_invntt_layer LP64 bitwuzla* ✅ 57s 109s -48%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 5s 1s +400%
mld_keccakf1600_permute_c LP64 z3* ✅ 2s 6s -67%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 3s -67%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 24s -50%
mld_ntt_layer LP64 bitwuzla* ✅ 22s 41s -46%
mld_polymat_expand_entry LP64 z3* ✅ 2s 4s -50%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 1s 2s -50%
mld_sample_pack_s1_s2 LP64 z3* ✅ 5s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 3s - new
mld_sign_attempt LP64 z3* ✅ 1s - new
mld_sign_finish LP64 z3* ✅ 3s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 1s 3s -67%
mld_value_barrier_u8 LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 z3* ✅ 1s 4s -75%
ntt_native_aarch64 LP64 z3* ✅ 4s 2s +100%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
pack_sig_c LP64 z3* ✅ 2s 5s -60%
pack_sig_h LP64 z3_no_bv_extract* ✅ 4s 5s -20%
pack_sig_z LP64 z3* ✅ 1s 2s -50%
pack_sk_rho_key_tr LP64 z3* ✅ 2s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 6s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 8s -62%
pointwise_native_aarch64 LP64 z3* ✅ 1s 5s -80%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 4s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_add LP64 z3* ✅ 3s 9s -67%
poly_caddq LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 z3* ✅ 4s 2s +100%
poly_caddq_native LP64 z3* ✅ 1s 2s -50%
poly_caddq_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_challenge LP64 z3* ✅ 2s 6s -67%
poly_chknorm LP64 z3* ✅ 2s 4s -50%
poly_chknorm_c LP64 z3* ✅ 5s 15s -67%
poly_chknorm_native LP64 z3* ✅ 2s 2s +0%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_decompose LP64 z3* ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 4s 1s +300%
poly_decompose_c LP64 z3* ✅ 2s 5s -60%
poly_decompose_native LP64 z3* ✅ 3s 3s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_invntt_tomont LP64 z3* ✅ 2s 3s -33%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 11s -36%
poly_invntt_tomont_native LP64 z3* ✅ 4s 2s +100%
poly_ntt LP64 z3* ✅ 3s 2s +50%
poly_ntt_c LP64 z3_smt_only* ✅ 12s 19s -37%
poly_ntt_native LP64 z3* ✅ 3s 4s -25%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 3s 4s -25%
poly_pointwise_montgomery LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery_c LP64 z3* ✅ 43s 125s -66%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 3s +0%
poly_power2round LP64 z3* ✅ 2s 4s -50%
poly_reduce LP64 z3* ✅ 4s 3s +33%
poly_shiftl LP64 z3* ✅ 3s 3s +0%
poly_sub LP64 z3* ✅ 1s 3s -67%
poly_uniform LP64 z3* ✅ 2s 4s -50%
poly_uniform_4x LP64 z3* ✅ 5s 13s -62%
poly_uniform_eta LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta_4x LP64 z3* ✅ 7s 14s -50%
poly_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 4s -50%
poly_use_hint LP64 z3* ✅ 3s 3s +0%
poly_use_hint_c LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 1s 3s -67%
polyeta_unpack LP64 z3* ✅ 2s 8s -75%
polyt0_pack LP64 z3* ✅ 3s 3s +0%
polyt0_unpack LP64 z3* ✅ 7s 16s -56%
polyt1_pack LP64 z3* ✅ 4s 3s +33%
polyt1_unpack LP64 z3* ✅ 2s 5s -60%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 71s 110s -35%
polyvec_matrix_expand_serial LP64 z3* ✅ 14s 27s -48%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 1s 1s +0%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 15s 18s -17%
polyveck_caddq LP64 z3* ✅ 2s 6s -67%
polyveck_decompose_pack_w1 LP64 z3* ✅ 6s - new
polyveck_invntt_tomont LP64 z3* ✅ 5s 8s -38%
polyveck_ntt LP64 z3* ✅ 5s 7s -29%
polyveck_reduce LP64 z3* ✅ 2s 4s -50%
polyveck_unpack_eta LP64 z3* ✅ 2s 6s -67%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 3s 7s -57%
polyvecl_ntt LP64 z3* ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 101s 210s -52%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 3s 2s +50%
polyvecl_uniform_gamma1 LP64 z3* ✅ 1s 2s -50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 3s +0%
polyvecl_unpack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_unpack_z LP64 z3* ✅ 2s 3s -33%
polyw1_pack LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 z3* ✅ 1s 4s -75%
polyw1_pack_88 LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 1s - new
polyw1_unpack_88 LP64 z3* ✅ 1s - new
polyz_pack LP64 z3* ✅ 3s 3s +0%
polyz_unpack LP64 z3* ✅ 3s 3s +0%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 1s 3s -67%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 1s 3s -67%
polyz_unpack_c LP64 z3* ✅ 3s 13s -77%
polyz_unpack_native LP64 z3* ✅ 3s 4s -25%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 2s 1s +100%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 2s 2s +0%
rej_eta_c LP64 bitwuzla* ✅ 3s 5s -40%
rej_eta_native LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform LP64 z3* ✅ 10s 18s -44%
rej_uniform_c LP64 z3* ✅ 9s 14s -36%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 4s -75%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 1s 4s -75%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 2s 1s +100%
shake128_init LP64 z3* ✅ 1s 2s -50%
shake128_release LP64 z3* ✅ 2s 3s -33%
shake128_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 3s +0%
shake256 LP64 z3* ✅ 1s 2s -50%
shake256_absorb LP64 z3* ✅ 2s 2s +0%
shake256_finalize LP64 z3* ✅ 2s 1s +100%
shake256_init LP64 z3* ✅ 2s 2s +0%
shake256_release LP64 z3* ✅ 2s 2s +0%
shake256_squeeze LP64 bitwuzla* ✅ 2s 3s -33%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
sig_unpack_hints LP64 z3* ✅ 15s 2s +650%
sign_keypair LP64 z3* ✅ 5s 3s +67%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 18s 5s +260%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_signature LP64 z3* ✅ 3s 6s -50%
sign_signature_extmu LP64 z3* ✅ 4s 2s +100%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 174s 55s +216%
sign_signature_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 3s 3s +0%
sign_verify LP64 z3* ✅ 3s 3s +0%
sign_verify_extmu LP64 z3* ✅ 1s 3s -67%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 399s 177s +125%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 5s -40%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 3s 5s -40%
sk_s1hat_get_poly LP64 z3* ✅ 2s 6s -67%
sk_s2hat_get_poly LP64 z3* ✅ 3s 2s +50%
sk_t0hat_get_poly LP64 z3* ✅ 2s 2s +0%
sys_check_capability LP64 z3* ✅ 3s 4s -25%
unpack_pk_t1 LP64 z3* ✅ 2s 5s -60%
unpack_sk LP64 z3* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 z3* ✅ 1s 2s -50%
unpack_sk_s2hat LP64 z3* ✅ 1s 4s -75%
unpack_sk_t0hat LP64 z3* ✅ 3s 5s -40%
use_hint LP64 z3* ✅ 3s 2s +50%
yvec_get_poly LP64 z3* ✅ 1s 3s -67%
yvec_init LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Oct 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2987s 2151s +38.9%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 213s 19s +1021%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 280s 55s +409%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 32s 6s +433%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 362s 42s +762%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 1135s 97s +1070%
Full Results (226 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2987s 2151s +38.9%
caddq LP64 z3* ✅ 4s 4s +0%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 213s 19s +1021%
decompose LP64 z3* ✅ 2s 3s -33%
fqmul LP64 bitwuzla* ✅ 21s 43s -51%
fqscale LP64 bitwuzla* ✅ 1s 3s -67%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 4s - new
intt_native_x86_64 LP64 z3* ✅ 1s 3s -67%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 9s -56%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 1s +200%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 1s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 4s -75%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 4s 4s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_finalize LP64 z3* ✅ 2s 1s +100%
keccak_init LP64 z3* ✅ 2s 3s -33%
keccak_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 4s 4s +0%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 3s -67%
keccakf1600_permute LP64 z3* ✅ 1s 3s -67%
keccakf1600_permute_native LP64 z3* ✅ 2s 4s -50%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_permute LP64 z3* ✅ 4s 3s +33%
keccakf1600x4_permute_native LP64 z3* ✅ 13s 23s -43%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 3s -67%
make_hint LP64 z3* ✅ 1s 3s -67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 280s 55s +409%
mld_check_pct LP64 z3* ✅ 4s 16s -75%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 8s -50%
mld_ct_abs_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* ✅ 1s 3s -67%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 4s -50%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 3s 3s +0%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
mld_ct_sel_int32 LP64 z3* ✅ 1s 3s -67%
mld_h LP64 z3* ✅ 3s 3s +0%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 115s -50%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 4s -75%
mld_keccakf1600_permute_c LP64 z3* ✅ 4s 7s -43%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 4s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 13s 24s -46%
mld_ntt_layer LP64 bitwuzla* ✅ 22s 45s -51%
mld_polymat_expand_entry LP64 z3* ✅ 2s 3s -33%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 2s 4s -50%
mld_sample_pack_s1_s2 LP64 z3* ✅ 5s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 6s - new
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 1s +100%
mld_value_barrier_u32 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u8 LP64 z3* ✅ 1s 3s -67%
montgomery_reduce LP64 z3* ✅ 3s 3s +0%
ntt_native_aarch64 LP64 z3* ✅ 2s 6s -67%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 3s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 4s 2s +100%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
pack_sig_c LP64 z3* ✅ 5s 4s +25%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 4s -50%
pack_sig_z LP64 z3* ✅ 1s 5s -80%
pack_sk_rho_key_tr LP64 z3* ✅ 1s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 6s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_native_aarch64 LP64 z3* ✅ 3s 5s -40%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_add LP64 z3* ✅ 2s 6s -67%
poly_caddq LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 z3* ✅ 1s 3s -67%
poly_caddq_native LP64 z3* ✅ 3s 4s -25%
poly_caddq_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_challenge LP64 z3* ✅ 6s 5s +20%
poly_chknorm LP64 z3* ✅ 2s 3s -33%
poly_chknorm_c LP64 z3* ✅ 7s 15s -53%
poly_chknorm_native LP64 z3* ✅ 3s 4s -25%
poly_chknorm_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 z3* ✅ 2s 3s -33%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 5s -60%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_decompose_c LP64 z3* ✅ 2s 5s -60%
poly_decompose_native LP64 z3* ✅ 2s 2s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_invntt_tomont LP64 z3* ✅ 3s 1s +200%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 12s -50%
poly_invntt_tomont_native LP64 z3* ✅ 1s 5s -80%
poly_ntt LP64 z3* ✅ 2s 3s -33%
poly_ntt_c LP64 z3_smt_only* ✅ 11s 21s -48%
poly_ntt_native LP64 z3* ✅ 1s 3s -67%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 1s 3s -67%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 5s -60%
poly_pointwise_montgomery LP64 z3* ✅ 3s 4s -25%
poly_pointwise_montgomery_c LP64 z3* ✅ 45s 144s -69%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 5s -60%
poly_power2round LP64 z3* ✅ 1s 3s -67%
poly_reduce LP64 z3* ✅ 1s 2s -50%
poly_shiftl LP64 z3* ✅ 3s 4s -25%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 1s 4s -75%
poly_uniform_4x LP64 z3* ✅ 8s 13s -38%
poly_uniform_eta LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta_4x LP64 z3* ✅ 9s 11s -18%
poly_uniform_gamma1 LP64 z3* ✅ 3s 4s -25%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 3s -33%
poly_use_hint LP64 z3* ✅ 3s 1s +200%
poly_use_hint_c LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 2s 4s -50%
polyeta_unpack LP64 z3* ✅ 6s 17s -65%
polyt0_pack LP64 z3* ✅ 2s 4s -50%
polyt0_unpack LP64 z3* ✅ 8s 14s -43%
polyt1_pack LP64 z3* ✅ 3s 3s +0%
polyt1_unpack LP64 z3* ✅ 3s 4s -25%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 100s 324s -69%
polyvec_matrix_expand_serial LP64 z3* ✅ 21s 38s -45%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 3s +33%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 13s 18s -28%
polyveck_caddq LP64 z3* ✅ 5s 8s -38%
polyveck_decompose_pack_w1 LP64 z3* ✅ 4s - new
polyveck_invntt_tomont LP64 z3* ✅ 5s 9s -44%
polyveck_ntt LP64 z3* ✅ 6s 11s -45%
polyveck_reduce LP64 z3* ✅ 2s 3s -33%
polyveck_unpack_eta LP64 z3* ✅ 1s 4s -75%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 1s 7s -86%
polyvecl_ntt LP64 z3* ✅ 4s 7s -43%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 5s -80%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 115s 353s -67%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 2s +0%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 4s -50%
polyvecl_unpack_eta LP64 z3* ✅ 2s 5s -60%
polyvecl_unpack_z LP64 z3* ✅ 3s 4s -25%
polyw1_pack LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 z3* ✅ 1s 4s -75%
polyw1_pack_88 LP64 z3* ✅ 3s 3s +0%
polyw1_unpack LP64 z3* ✅ 4s - new
polyw1_unpack_32 LP64 z3* ✅ 1s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 2s 5s -60%
polyz_unpack LP64 z3* ✅ 3s 2s +50%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_c LP64 z3* ✅ 4s 3s +33%
polyz_unpack_native LP64 z3* ✅ 2s 4s -50%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 2s 4s -50%
reduce32 LP64 z3* ✅ 3s 3s +0%
rej_eta LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_c LP64 bitwuzla* ✅ 3s 5s -40%
rej_eta_native LP64 bitwuzla* ✅ 2s 6s -67%
rej_uniform LP64 z3* ✅ 11s 15s -27%
rej_uniform_c LP64 z3* ✅ 9s 19s -53%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 5s -60%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 3s 8s -62%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 6s - new
shake128_absorb LP64 z3* ✅ 1s 4s -75%
shake128_finalize LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 z3* ✅ 2s 1s +100%
shake128_release LP64 z3* ✅ 1s 4s -75%
shake128_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 5s -60%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
shake256 LP64 z3* ✅ 1s 2s -50%
shake256_absorb LP64 z3* ✅ 1s 2s -50%
shake256_finalize LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 z3* ✅ 1s 2s -50%
shake256_release LP64 z3* ✅ 1s 3s -67%
shake256_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 4s 1s +300%
sig_unpack_hints LP64 z3* ✅ 11s 3s +267%
sign_keypair LP64 z3* ✅ 6s 4s +50%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 19s 6s +217%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 32s 6s +433%
sign_signature LP64 z3* ✅ 3s 5s -40%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 362s 42s +762%
sign_signature_pre_hash_internal LP64 z3* ✅ 2s 5s -60%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 3s 6s -50%
sign_verify LP64 z3* ✅ 3s 5s -40%
sign_verify_extmu LP64 z3* ✅ 1s 3s -67%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 1135s 97s +1070%
sign_verify_pre_hash_internal LP64 z3* ✅ 4s 3s +33%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 6s 3s +100%
sk_s1hat_get_poly LP64 z3* ✅ 4s 3s +33%
sk_s2hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_t0hat_get_poly LP64 z3* ✅ 5s 4s +25%
sys_check_capability LP64 z3* ✅ 1s 3s -67%
unpack_pk_t1 LP64 z3* ✅ 2s 1s +100%
unpack_sk LP64 z3* ✅ 3s 5s -40%
unpack_sk_s1hat LP64 z3* ✅ 2s 2s +0%
unpack_sk_s2hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_t0hat LP64 z3* ✅ 1s 7s -86%
use_hint LP64 z3* ✅ 1s 3s -67%
yvec_get_poly LP64 z3* ✅ 1s 4s -75%
yvec_init LP64 z3* ✅ 3s 4s -25%

@mkannwischer
mkannwischer marked this pull request as ready for review October 21, 2026 07:10
@mkannwischer
mkannwischer requested a review from a team as a code owner October 21, 2026 07:10
hanno-becker
hanno-becker reviewed Oct 24, 2026
View reviewed changes
Comment thread mldsa/src/fips202/fips202.c Outdated
hanno-becker
hanno-becker requested changes Oct 24, 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.

I think 48681e0 is a step back; otherwise LGTM.

hanno-becker
hanno-becker requested changes Oct 24, 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.

I think it hinders readability to mix stdlib and internal includes and prefer to keep it as is.

@mkannwischer
autogen: Format files under their own name
978869f 
clang-format identifies the main include by file name, so formatting a
temporary copy with a random name sorted it differently from lint.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
Separate standard-library from internal includes
67b656d 
Keep the internal includes of library sources in a single block,
separated from standard-library includes by a blank line, and drop the
unused <string.h> include in the x86_64 backend.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

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 Awaiting requested review from hanno-becker

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

needs-mlkem-native-port

Projects

None yet

Milestone

v2.1

Development

Successfully merging this pull request may close these issues.

3 participants

@mkannwischer @oqs-bot @hanno-becker