Skip to content

Zeroize stack in assembly routines spilling to the stack - #1498

Draft
mkannwischer wants to merge 1 commit into
mainfrom
asm-zeroize
Draft

Zeroize stack in assembly routines spilling to the stack#1498
mkannwischer wants to merge 1 commit into
mainfrom
asm-zeroize

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

The x86_64 AVX2 Keccak-f1600x4, the aarch64 scalar/hybrid Keccak-f1600 routines, and the aarch64 rej_uniform{,_eta2,_eta4} routines left data on the stack upon return. Zeroize the used stack locals/buffers before returning, and strengthen the HOL Light specifications to state that the stack region is zero on return.

@mkannwischer
Zeroize stack in assembly routines spilling to the stack
115130b 
The x86_64 AVX2 Keccak-f1600x4, the aarch64 scalar/hybrid Keccak-f1600
routines, and the aarch64 rej_uniform{,_eta2,_eta4} routines left
data on the stack upon return. Zeroize the used stack locals/buffers
before returning, and strengthen the HOL Light specifications to
state that the stack region is zero on return.

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

oqs-bot commented Oct 25, 2026

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* ⚠️ 29s 12s +142%
intt_native_aarch64 LP64 bitwuzla ⚠️ 22s 3s +633%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 143s 19s +653%
mld_ct_memcmp LP64 z3_no_bv_extract ⚠️ 71s 1s +7000%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 20s 2s +900%
poly_caddq_native LP64 bitwuzla ⚠️ 92s 3s +2967%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 32s 3s +967%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 108s 4s +2600%
poly_challenge LP64 bitwuzla ⚠️ 23s 6s +283%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 40s 3s +1233%
poly_ntt_c LP64 bitwuzla ⚠️ 44s 21s +110%
poly_ntt_native LP64 bitwuzla ⚠️ 26s 3s +767%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 54s 2s +2600%
poly_power2round LP64 bitwuzla ⚠️ 240s 4s +5900%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 23s 2s +1050%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 90s 3s +2900%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 31s 3s +933%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 30s 4s +650%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 25s 3s +733%
polyz_unpack_native LP64 bitwuzla ⚠️ 25s 3s +733%
sig_unpack_hints LP64 bitwuzla ⚠️ 47s 2s +2250%
LP64 z3* ⚠️ 37s 2s +1750%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 5s +500%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 230s 49s +369%
Full Results (397 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1346s 1364s -1.3%
caddq LP64 bitwuzla ✅ 2s 6s -67%
LP64 z3* ✅ 3s 6s -50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 29s 12s +142%
decompose LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 4s 3s +33%
fqmul LP64 bitwuzla* ✅ 22s 39s -44%
LP64 z3_smt_only ✅ 19s 39s -51%
fqscale LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s 2s +0%
intt_native_aarch64 LP64 bitwuzla ⚠️ 22s 3s +633%
LP64 z3* ✅ 3s 3s +0%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 9s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 bitwuzla ✅ 17s 2s +750%
LP64 z3* ✅ 4s 2s +100%
keccak_absorb LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 8s -25%
LP64 cvc5_arrays_exp ✅ 7s 8s -12%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_no_bv_extract ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_smt_only ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_smt_only ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
keccak_finalize LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
keccak_init LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
keccak_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 1s 2s -50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s 3s -33%
keccakf1600_extract_bytes (big endian) LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 3s 4s -25%
keccakf1600_permute LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 3s 3s +0%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 6s -83%
LP64 z3_smt_only ✅ 2s 6s -67%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 3s 4s -25%
keccakf1600x4_permute LP64 cvc5_arrays_exp ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
keccakf1600x4_permute_native LP64 cvc5_arrays_exp ✅ 11s 22s -50%
LP64 z3* ✅ 13s 22s -41%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3_no_bv_extract ✅ 1s 5s -80%
make_hint LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 143s 19s +653%
mld_check_pct LP64 bitwuzla ✅ 5s 15s -67%
LP64 z3* ✅ 5s 15s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 6s -33%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 3s -33%
ILP32 cvc5_arrays_exp ✅ 2s 3s -33%
ILP32 z3 ✅ 1s 3s -67%
LP64 bitwuzla ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
mld_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
mld_ct_get_optblocker_u32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 4s 2s +100%
mld_ct_memcmp LP64 bitwuzla* ✅ 4s 1s +300%
LP64 z3_no_bv_extract ⚠️ 71s 1s +7000%
mld_ct_sel_int32 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
mld_h LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 2s 4s -50%
mld_invntt_layer LP64 bitwuzla* ✅ 59s 105s -44%
mld_keccakf1600_extract_bytes LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
mld_keccakf1600_permute_c LP64 cvc5_arrays_exp ✅ 5s 7s -29%
LP64 z3* ✅ 4s 7s -43%
mld_keccakf1600x4_extract_bytes_c LP64 cvc5_arrays_exp ✅ 1s 4s -75%
LP64 z3* ✅ 2s 4s -50%
mld_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 2s 4s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 23s -48%
mld_ntt_layer LP64 bitwuzla* ✅ 22s 41s -46%
LP64 z3_no_bv_extract ✅ 4s 41s -90%
mld_polymat_expand_entry LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
mld_prepare_domain_separation_prefix LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
mld_sample_pack_s1_s2 LP64 z3* ✅ 1s - new
mld_sample_pack_s1_s2_serial LP64 cvc5_mbqi_enum ✅ 87s - new
LP64 z3* ✅ 2s - new
mld_sign_attempt LP64 cvc5_arrays_exp ✅ 2s - new
LP64 z3* ✅ 2s - new
mld_sign_finish LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s - new
mld_sign_resume LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
mld_value_barrier_u32 LP64 bitwuzla ✅ 2s 1s +100%
LP64 z3* ✅ 3s 1s +200%
mld_value_barrier_u8 LP64 cvc5_arrays_exp ✅ 4s 4s +0%
LP64 z3* ✅ 2s 4s -50%
montgomery_reduce LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
ntt_native_aarch64 LP64 bitwuzla ✅ 18s 4s +350%
LP64 z3* ✅ 1s 4s -75%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 5s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 bitwuzla ✅ 18s 3s +500%
LP64 z3* ✅ 1s 3s -67%
nttunpack_native_x86_64 LP64 z3* ✅ 5s 4s +25%
pack_sig_c LP64 cvc5_arrays_exp ✅ 3s 5s -40%
LP64 z3* ✅ 3s 5s -40%
pack_sig_h LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3_no_bv_extract* ✅ 2s 4s -50%
pack_sig_z LP64 bitwuzla ✅ 5s 2s +150%
LP64 z3* ✅ 3s 2s +50%
pack_sk_rho_key_tr LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 5s 6s -17%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 4s +0%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 20s 2s +900%
LP64 z3* ✅ 3s 2s +50%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 bitwuzla ✅ 19s 4s +375%
LP64 z3* ✅ 4s 4s +0%
poly_add LP64 z3* ✅ 5s 7s -29%
poly_caddq LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 1s 4s -75%
poly_caddq_c LP64 bitwuzla ✅ 19s 3s +533%
LP64 z3* ✅ 3s 3s +0%
poly_caddq_native LP64 bitwuzla ⚠️ 92s 3s +2967%
LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 32s 3s +967%
LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 108s 4s +2600%
LP64 z3* ✅ 4s 4s +0%
poly_challenge LP64 bitwuzla ⚠️ 23s 6s +283%
LP64 z3* ✅ 2s 6s -67%
poly_chknorm LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 1s 3s -67%
poly_chknorm_c LP64 bitwuzla ✅ 8s 11s -27%
LP64 z3* ✅ 9s 11s -18%
poly_chknorm_native LP64 bitwuzla ✅ 6s 4s +50%
LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
poly_chknorm_native_x86_64 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 4s 2s +100%
poly_decompose LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 1s 2s -50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_decompose_88_native_aarch64 LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 2s 3s -33%
poly_decompose_c LP64 z3* ✅ 4s 5s -20%
poly_decompose_native LP64 z3* ✅ 2s 2s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 11s -36%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 40s 3s +1233%
LP64 z3* ✅ 2s 3s -33%
poly_ntt LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 4s 3s +33%
poly_ntt_c LP64 bitwuzla ⚠️ 44s 21s +110%
LP64 z3_smt_only* ✅ 11s 21s -48%
poly_ntt_native LP64 bitwuzla ⚠️ 26s 3s +767%
LP64 z3* ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional LP64 bitwuzla ✅ 4s 5s -20%
LP64 z3* ✅ 3s 5s -40%
poly_permute_bitrev_to_custom_optional_native LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery LP64 bitwuzla ✅ 7s 3s +133%
LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery_c LP64 z3* ✅ 73s 112s -35%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 54s 2s +2600%
LP64 z3* ✅ 1s 2s -50%
poly_power2round LP64 bitwuzla ⚠️ 240s 4s +5900%
LP64 z3* ✅ 3s 4s -25%
poly_reduce LP64 bitwuzla ✅ 7s 4s +75%
LP64 z3* ✅ 1s 4s -75%
poly_shiftl LP64 bitwuzla ✅ 12s 4s +200%
LP64 z3* ✅ 2s 4s -50%
poly_sub LP64 bitwuzla ✅ 14s 3s +367%
LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 2s 3s -33%
poly_uniform_4x LP64 z3* ✅ 2s 3s -33%
poly_uniform_eta LP64 z3* ✅ 2s 2s +0%
poly_uniform_eta_4x LP64 z3* ✅ 6s 12s -50%
poly_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
poly_uniform_gamma1_4x LP64 z3* ✅ 3s 5s -40%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 23s 2s +1050%
LP64 z3* ✅ 1s 2s -50%
poly_use_hint_c LP64 cvc5_enum_inst ✅ 10s 5s +100%
LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 90s 3s +2900%
LP64 z3* ✅ 1s 3s -67%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 31s 3s +933%
LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_x86_64 LP64 bitwuzla ✅ 29s - new
LP64 z3* ✅ 2s - new
polyeta_pack LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 2s 3s -33%
polyeta_unpack LP64 bitwuzla ✅ 2s 14s -86%
LP64 z3* ✅ 8s 14s -43%
polyt0_pack LP64 bitwuzla ✅ 5s 4s +25%
LP64 z3* ✅ 2s 4s -50%
polyt0_unpack LP64 bitwuzla ✅ 6s 12s -50%
LP64 z3* ✅ 7s 12s -42%
polyt1_pack LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 2s 3s -33%
polyt1_unpack LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 3s 2s +50%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 3s -67%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 4s -50%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 2s 6s -67%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 122s 149s -18%
polyveck_caddq LP64 z3* ✅ 2s 3s -33%
polyveck_decompose_pack_w1 LP64 z3* ✅ 8s - new
polyveck_invntt_tomont LP64 z3* ✅ 3s 5s -40%
polyveck_ntt LP64 z3* ✅ 1s 2s -50%
polyveck_reduce LP64 z3* ✅ 4s 4s +0%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
polyveck_unpack_eta_chknorm LP64 cvc5_mbqi_enum ✅ 16s - new
LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 3s 11s -73%
polyvecl_ntt LP64 z3* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery LP64 cvc5_mbqi_enum ✅ 1s 3s -67%
LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 3s 4s -25%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ✅ 4s 2s +100%
LP64 z3* ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 30s 4s +650%
LP64 z3* ✅ 2s 4s -50%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 25s 3s +733%
LP64 z3* ✅ 3s 3s +0%
polyw1_pack LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 3s 4s -25%
polyw1_pack_32 LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
polyw1_pack_88 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
polyw1_unpack LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s - new
polyw1_unpack_88 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s - new
polyz_pack LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
polyz_unpack LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 4s 2s +100%
polyz_unpack_19_native_aarch64 LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
polyz_unpack_c LP64 bitwuzla ✅ 2s 8s -75%
LP64 z3* ✅ 5s 8s -38%
polyz_unpack_native LP64 bitwuzla ⚠️ 25s 3s +733%
LP64 z3* ✅ 1s 3s -67%
polyz_unpack_native_x86_64 LP64 bitwuzla ✅ 16s 3s +433%
LP64 z3* ✅ 4s 3s +33%
power2round LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
reduce32 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 2s 5s -60%
LP64 z3_smt_only ✅ 4s 5s -20%
rej_eta_c LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3 ✅ 18s 4s +350%
rej_eta_native LP64 bitwuzla* ✅ 4s 3s +33%
LP64 z3_smt_only ✅ 11s 3s +267%
rej_uniform LP64 bitwuzla ✅ 2s 8s -75%
LP64 z3* ✅ 4s 8s -50%
rej_uniform_c LP64 bitwuzla ✅ 2s 16s -88%
LP64 z3* ✅ 7s 16s -56%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_smt_only ✅ 2s 3s -33%
rej_uniform_eta_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 5s 5s +0%
LP64 z3_smt_only ✅ 15s 5s +200%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_smt_only ✅ 1s 3s -67%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3_smt_only* ✅ 10s - new
shake128_absorb LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
shake128_finalize LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
shake128_init LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
shake128_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 1s 2s -50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3_smt_only ✅ 3s 2s +50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s 2s +0%
shake256 LP64 bitwuzla ✅ 3s 1s +200%
LP64 z3* ✅ 3s 1s +200%
shake256_absorb LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
shake256_finalize LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
shake256_release LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%
shake256_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 3s 1s +200%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 3s 2s +50%
sig_unpack_hints LP64 bitwuzla ⚠️ 47s 2s +2250%
LP64 z3* ⚠️ 37s 2s +1750%
sign_keypair LP64 z3* ✅ 3s 5s -40%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 13s 4s +225%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 5s +500%
sign_signature LP64 bitwuzla ✅ 3s 6s -50%
LP64 z3* ✅ 6s 6s +0%
sign_signature_extmu LP64 z3* ✅ 2s 4s -50%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 4s +250%
sign_signature_pre_hash_internal LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 3s 4s -25%
sign_signature_pre_hash_shake256 LP64 bitwuzla ✅ 6s 4s +50%
LP64 z3* ✅ 4s 4s +0%
sign_verify LP64 bitwuzla ✅ 5s 4s +25%
LP64 z3* ✅ 5s 4s +25%
sign_verify_extmu LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 2s 5s -60%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 230s 49s +369%
sign_verify_pre_hash_internal LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 2s 5s -60%
sign_verify_pre_hash_shake256 LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 1s 5s -80%
sk_s1hat_get_poly LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 4s 2s +100%
sk_s2hat_get_poly LP64 bitwuzla ✅ 4s 5s -20%
LP64 z3* ✅ 3s 5s -40%
sk_t0hat_get_poly LP64 bitwuzla ✅ 2s 1s +100%
LP64 z3* ✅ 3s 1s +200%
sys_check_capability LP64 cvc5_arrays_exp ✅ 4s 2s +100%
LP64 z3* ✅ 1s 2s -50%
unpack_pk_t1 LP64 bitwuzla ✅ 10s 3s +233%
LP64 z3* ✅ 1s 3s -67%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ✅ 2s 4s -50%
LP64 z3* ✅ 4s 4s +0%
unpack_sk_t0hat LP64 z3* ✅ 3s 2s +50%
use_hint LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
yvec_init LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 1971s 1514s +30.2%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 91s 50s +82%
intt_native_aarch64 LP64 bitwuzla ⚠️ 22s 9s +144%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 345s 58s +495%
mld_ct_memcmp LP64 z3_no_bv_extract ⚠️ 71s 3s +2267%
poly_caddq_c LP64 bitwuzla ⚠️ 20s 2s +900%
poly_caddq_native LP64 bitwuzla ⚠️ 102s 5s +1940%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 33s 4s +725%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 113s 4s +2725%
poly_challenge LP64 bitwuzla ⚠️ 25s 3s +733%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 44s 4s +1000%
poly_ntt_c LP64 bitwuzla ⚠️ 45s 19s +137%
poly_ntt_native LP64 bitwuzla ⚠️ 24s 5s +380%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 56s 2s +2700%
poly_power2round LP64 bitwuzla ⚠️ 280s 4s +6900%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 25s 4s +525%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 92s 4s +2200%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 30s 2s +1400%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 28s 2s +1300%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ⚠️ 38s 3s +1167%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ⚠️ 38s 2s +1800%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 32s 2s +1500%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 26s 2s +1200%
polyz_unpack_native LP64 bitwuzla ⚠️ 23s 2s +1050%
sig_unpack_hints LP64 bitwuzla ⚠️ 48s 2s +2300%
LP64 z3* ⚠️ 27s 2s +1250%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 29s 5s +480%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 232s 26s +792%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 342s 114s +200%
sk_s1hat_get_poly LP64 bitwuzla ⚠️ 29s 3s +867%
sk_s2hat_get_poly LP64 bitwuzla ⚠️ 30s 2s +1400%
sk_t0hat_get_poly LP64 bitwuzla ⚠️ 31s 2s +1450%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ⚠️ 240s 1s +23900%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ⚠️ 235s 4s +5775%
yvec_get_poly LP64 bitwuzla ⚠️ 31s 3s +933%
yvec_init LP64 bitwuzla ⚠️ 39s 3s +1200%
Full Results (397 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 1971s 1514s +30.2%
caddq LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 91s 50s +82%
decompose LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 1s 2s -50%
fqmul LP64 bitwuzla* ✅ 25s 39s -36%
LP64 z3_smt_only ✅ 20s 39s -49%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
intt_native_aarch64 LP64 bitwuzla ⚠️ 22s 9s +144%
LP64 z3* ✅ 2s 9s -78%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 1s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 8s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 bitwuzla ✅ 15s 4s +275%
LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 cvc5_arrays_exp ✅ 4s 5s -20%
LP64 z3* ✅ 3s 5s -40%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 9s -56%
LP64 cvc5_arrays_exp ✅ 8s 9s -11%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_no_bv_extract ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_smt_only ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3_smt_only ✅ 1s 1s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
keccak_finalize LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
keccak_init LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
keccak_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 3s 1s +200%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 4s 2s +100%
keccakf1600_permute LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
LP64 cvc5_arrays_exp ✅ 3s 1s +200%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 6s 4s +50%
LP64 z3_smt_only ✅ 1s 4s -75%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s 2s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 1s 3s -67%
keccakf1600x4_permute LP64 cvc5_arrays_exp ✅ 1s 4s -75%
LP64 z3* ✅ 1s 4s -75%
keccakf1600x4_permute_native LP64 cvc5_arrays_exp ✅ 13s 22s -41%
LP64 z3* ✅ 13s 22s -41%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 4s 3s +33%
LP64 z3_no_bv_extract ✅ 3s 3s +0%
make_hint LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 5s 3s +67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 345s 58s +495%
mld_check_pct LP64 bitwuzla ✅ 5s 14s -64%
LP64 z3* ✅ 7s 14s -50%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 3s 7s -57%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 2s +0%
ILP32 cvc5_arrays_exp ✅ 2s 2s +0%
ILP32 z3 ✅ 2s 2s +0%
LP64 bitwuzla ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_neg_i32 LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 5s 2s +150%
mld_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
mld_ct_get_optblocker_i64 LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 3s 4s -25%
mld_ct_get_optblocker_u32 LP64 bitwuzla ✅ 2s 1s +100%
LP64 z3* ✅ 1s 1s +0%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3_smt_only ✅ 3s 1s +200%
mld_ct_memcmp LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3_no_bv_extract ⚠️ 71s 3s +2267%
mld_ct_sel_int32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_h LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 107s -46%
mld_keccakf1600_extract_bytes LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600_permute_c LP64 cvc5_arrays_exp ✅ 3s 8s -62%
LP64 z3* ✅ 5s 8s -38%
mld_keccakf1600x4_extract_bytes_c LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 5s 2s +150%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 23s -52%
mld_ntt_layer LP64 bitwuzla* ✅ 26s 42s -38%
LP64 z3_no_bv_extract ✅ 4s 42s -90%
mld_polymat_expand_entry LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
mld_prepare_domain_separation_prefix LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 3s 4s -25%
mld_sample_pack_s1_s2 LP64 z3* ✅ 2s - new
mld_sample_pack_s1_s2_serial LP64 cvc5_mbqi_enum ✅ 88s - new
LP64 z3* ✅ 2s - new
mld_sign_attempt LP64 cvc5_arrays_exp ✅ 2s - new
LP64 z3* ✅ 2s - new
mld_sign_finish LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s - new
mld_sign_resume LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s - new
mld_value_barrier_i64 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 3s 2s +50%
mld_value_barrier_u8 LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
montgomery_reduce LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
ntt_native_aarch64 LP64 bitwuzla ✅ 19s 3s +533%
LP64 z3* ✅ 3s 3s +0%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 1s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 8s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 bitwuzla ✅ 17s 3s +467%
LP64 z3* ✅ 3s 3s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 1s +0%
pack_sig_c LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
pack_sig_h LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3_no_bv_extract* ✅ 3s 3s +0%
pack_sig_z LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 4s 4s +0%
pack_sk_rho_key_tr LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 4s -25%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 7s -43%
pointwise_native_aarch64 LP64 bitwuzla ✅ 19s 5s +280%
LP64 z3* ✅ 3s 5s -40%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 5s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 bitwuzla ✅ 19s 4s +375%
LP64 z3* ✅ 2s 4s -50%
poly_add LP64 z3* ✅ 2s 7s -71%
poly_caddq LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 bitwuzla ⚠️ 20s 2s +900%
LP64 z3* ✅ 2s 2s +0%
poly_caddq_native LP64 bitwuzla ⚠️ 102s 5s +1940%
LP64 z3* ✅ 2s 5s -60%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 33s 4s +725%
LP64 z3* ✅ 1s 4s -75%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 113s 4s +2725%
LP64 z3* ✅ 3s 4s -25%
poly_challenge LP64 bitwuzla ⚠️ 25s 3s +733%
LP64 z3* ✅ 2s 3s -33%
poly_chknorm LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 2s 4s -50%
poly_chknorm_c LP64 bitwuzla ✅ 7s 17s -59%
LP64 z3* ✅ 5s 17s -71%
poly_chknorm_native LP64 bitwuzla ✅ 6s 4s +50%
LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_x86_64 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 2s 3s -33%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_decompose_88_native_aarch64 LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 2s 4s -50%
poly_decompose_c LP64 z3* ✅ 3s 4s -25%
poly_decompose_native LP64 z3* ✅ 3s 3s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_invntt_tomont LP64 bitwuzla ✅ 7s 4s +75%
LP64 z3* ✅ 3s 4s -25%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 11s -45%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 44s 4s +1000%
LP64 z3* ✅ 2s 4s -50%
poly_ntt LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
poly_ntt_c LP64 bitwuzla ⚠️ 45s 19s +137%
LP64 z3_smt_only* ✅ 12s 19s -37%
poly_ntt_native LP64 bitwuzla ⚠️ 24s 5s +380%
LP64 z3* ✅ 3s 5s -40%
poly_permute_bitrev_to_custom_optional LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
poly_pointwise_montgomery LP64 bitwuzla ✅ 9s 3s +200%
LP64 z3* ✅ 4s 3s +33%
poly_pointwise_montgomery_c LP64 z3* ✅ 45s 114s -61%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 56s 2s +2700%
LP64 z3* ✅ 1s 2s -50%
poly_power2round LP64 bitwuzla ⚠️ 280s 4s +6900%
LP64 z3* ✅ 1s 4s -75%
poly_reduce LP64 bitwuzla ✅ 8s 3s +167%
LP64 z3* ✅ 2s 3s -33%
poly_shiftl LP64 bitwuzla ✅ 9s 3s +200%
LP64 z3* ✅ 1s 3s -67%
poly_sub LP64 bitwuzla ✅ 14s 3s +367%
LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 2s 6s -67%
poly_uniform_4x LP64 z3* ✅ 8s 14s -43%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
poly_uniform_eta_4x LP64 z3* ✅ 8s 11s -27%
poly_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
poly_uniform_gamma1_4x LP64 z3* ✅ 3s 5s -40%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 25s 4s +525%
LP64 z3* ✅ 2s 4s -50%
poly_use_hint_c LP64 cvc5_enum_inst ✅ 10s 3s +233%
LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 92s 4s +2200%
LP64 z3* ✅ 1s 4s -75%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 30s 2s +1400%
LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_x86_64 LP64 bitwuzla ✅ 32s - new
LP64 z3* ✅ 2s - new
polyeta_pack LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 bitwuzla ✅ 5s 14s -64%
LP64 z3* ✅ 5s 14s -64%
polyt0_pack LP64 bitwuzla ✅ 5s 2s +150%
LP64 z3* ✅ 2s 2s +0%
polyt0_unpack LP64 bitwuzla ✅ 5s 15s -67%
LP64 z3* ✅ 8s 15s -47%
polyt1_pack LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 4s 4s +0%
polyt1_unpack LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 1s 5s -80%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 15s 28s -46%
polyvec_matrix_expand_serial LP64 z3* ✅ 4s 8s -50%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 1s 2s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 11s 15s -27%
polyveck_caddq LP64 z3* ✅ 2s 3s -33%
polyveck_decompose_pack_w1 LP64 z3* ✅ 3s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 5s -20%
polyveck_ntt LP64 z3* ✅ 4s 5s -20%
polyveck_reduce LP64 z3* ✅ 2s 5s -60%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 28s 2s +1300%
LP64 z3* ✅ 2s 2s +0%
polyveck_unpack_eta_chknorm LP64 cvc5_mbqi_enum ✅ 15s - new
LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 5s 10s -50%
polyvecl_ntt LP64 z3* ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery LP64 cvc5_mbqi_enum ✅ 5s 4s +25%
LP64 z3_smt_only* ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 148s 131s +13%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 2s -50%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ⚠️ 38s 3s +1167%
LP64 z3* ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ⚠️ 38s 2s +1800%
LP64 z3* ✅ 1s 2s -50%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 32s 2s +1500%
LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 26s 2s +1200%
LP64 z3* ✅ 2s 2s +0%
polyw1_pack LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
polyw1_pack_32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
polyw1_pack_88 LP64 bitwuzla ✅ 5s 1s +400%
LP64 z3* ✅ 3s 1s +200%
polyw1_unpack LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 5s - new
polyz_pack LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
polyz_unpack LP64 bitwuzla ✅ 6s 3s +100%
LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 3s 5s -40%
polyz_unpack_19_native_aarch64 LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 1s 5s -80%
polyz_unpack_c LP64 bitwuzla ✅ 1s 11s -91%
LP64 z3* ✅ 6s 11s -45%
polyz_unpack_native LP64 bitwuzla ⚠️ 23s 2s +1050%
LP64 z3* ✅ 2s 2s +0%
polyz_unpack_native_x86_64 LP64 bitwuzla ✅ 14s 3s +367%
LP64 z3* ✅ 2s 3s -33%
power2round LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
reduce32 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
rej_eta LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3_smt_only ✅ 3s 3s +0%
rej_eta_c LP64 bitwuzla* ✅ 4s 4s +0%
LP64 z3 ✅ 15s 4s +275%
rej_eta_native LP64 bitwuzla* ✅ 1s 6s -83%
LP64 z3_smt_only ✅ 10s 6s +67%
rej_uniform LP64 bitwuzla ✅ 3s 18s -83%
LP64 z3* ✅ 12s 18s -33%
rej_uniform_c LP64 bitwuzla ✅ 3s 15s -80%
LP64 z3* ✅ 11s 15s -27%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3_smt_only ✅ 3s 2s +50%
rej_uniform_eta_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3_smt_only ✅ 18s 4s +350%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 5s -60%
LP64 z3_smt_only ✅ 2s 5s -60%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
shake128_finalize LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
shake128_release LP64 bitwuzla ✅ 4s 1s +300%
LP64 z3* ✅ 3s 1s +200%
shake128_squeeze LP64 bitwuzla* ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_smt_only ✅ 1s 3s -67%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 2s 1s +100%
shake256 LP64 bitwuzla ✅ 2s 1s +100%
LP64 z3* ✅ 2s 1s +100%
shake256_absorb LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
shake256_release LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 5s 4s +25%
LP64 z3_smt_only ✅ 1s 4s -75%
sig_unpack_hints LP64 bitwuzla ⚠️ 48s 2s +2300%
LP64 z3* ⚠️ 27s 2s +1250%
sign_keypair LP64 z3* ✅ 2s 4s -50%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 16s 4s +300%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 29s 5s +480%
sign_signature LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
sign_signature_extmu LP64 z3* ✅ 4s 4s +0%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 232s 26s +792%
sign_signature_pre_hash_internal LP64 bitwuzla ✅ 3s 6s -50%
LP64 z3* ✅ 2s 6s -67%
sign_signature_pre_hash_shake256 LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 4s 3s +33%
sign_verify LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 3s 4s -25%
sign_verify_extmu LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 342s 114s +200%
sign_verify_pre_hash_internal LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 3s 5s -40%
sk_s1hat_get_poly LP64 bitwuzla ⚠️ 29s 3s +867%
LP64 z3* ✅ 3s 3s +0%
sk_s2hat_get_poly LP64 bitwuzla ⚠️ 30s 2s +1400%
LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 bitwuzla ⚠️ 31s 2s +1450%
LP64 z3* ✅ 2s 2s +0%
sys_check_capability LP64 cvc5_arrays_exp ✅ 1s 4s -75%
LP64 z3* ✅ 2s 4s -50%
unpack_pk_t1 LP64 bitwuzla ✅ 11s 5s +120%
LP64 z3* ✅ 3s 5s -40%
unpack_sk LP64 z3* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ⚠️ 240s 1s +23900%
LP64 z3* ✅ 2s 1s +100%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ⚠️ 235s 4s +5775%
LP64 z3* ✅ 3s 4s -25%
unpack_sk_t0hat LP64 z3* ✅ 1s 3s -67%
use_hint LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 bitwuzla ⚠️ 31s 3s +933%
LP64 z3* ✅ 3s 3s +0%
yvec_init LP64 bitwuzla ⚠️ 39s 3s +1200%
LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Oct 25, 2026

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* ⚠️ 36s 7s +414%
intt_native_aarch64 LP64 bitwuzla ⚠️ 21s 2s +950%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 187s 31s +503%
mld_ct_memcmp LP64 z3_no_bv_extract ⚠️ 81s 4s +1925%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 20s 3s +567%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 20s 3s +567%
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 20s 2s +900%
poly_caddq_native LP64 bitwuzla ⚠️ 102s 4s +2450%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 33s 2s +1550%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 117s 1s +11600%
poly_challenge LP64 bitwuzla ⚠️ 20s 5s +300%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 42s 5s +740%
poly_ntt_c LP64 bitwuzla ⚠️ 48s 22s +118%
poly_ntt_native LP64 bitwuzla ⚠️ 26s 2s +1200%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 51s 4s +1175%
poly_power2round LP64 bitwuzla ⚠️ 279s 7s +3886%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 24s 3s +700%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 93s 7s +1229%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 28s 4s +600%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 33s 2s +1550%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 34s 1s +3300%
polyz_unpack_native LP64 bitwuzla ⚠️ 24s 3s +700%
sig_unpack_hints LP64 bitwuzla ⚠️ 1289s 1s +128800%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 33s 5s +560%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 344s 7s +4814%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 207s 71s +192%
Full Results (397 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1342s 1482s -9.4%
caddq LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 4s 2s +100%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 36s 7s +414%
decompose LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
fqmul LP64 bitwuzla* ✅ 24s 40s -40%
LP64 z3_smt_only ✅ 19s 40s -52%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
intt_native_aarch64 LP64 bitwuzla ⚠️ 21s 2s +950%
LP64 z3* ✅ 1s 2s -50%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 bitwuzla ✅ 17s 4s +325%
LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 4s 3s +33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 10s -50%
LP64 cvc5_arrays_exp ✅ 6s 10s -40%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_no_bv_extract ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_smt_only ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_smt_only ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
keccak_finalize LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
keccak_init LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
keccak_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s 2s -50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 1s 4s -75%
keccakf1600_permute_native LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 3s 4s -25%
LP64 cvc5_arrays_exp ✅ 2s 4s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 3s 2s +50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3 ✅ 3s 4s -25%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 2s 1s +100%
keccakf1600x4_permute LP64 cvc5_arrays_exp ✅ 2s 1s +100%
LP64 z3* ✅ 1s 1s +0%
keccakf1600x4_permute_native LP64 cvc5_arrays_exp ✅ 13s 22s -41%
LP64 z3* ✅ 12s 22s -45%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_no_bv_extract ✅ 1s 2s -50%
make_hint LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 187s 31s +503%
mld_check_pct LP64 bitwuzla ✅ 3s 12s -75%
LP64 z3* ✅ 5s 12s -58%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 3s 5s -40%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 6s -83%
ILP32 cvc5_arrays_exp ✅ 2s 6s -67%
ILP32 z3 ✅ 2s 6s -67%
LP64 bitwuzla ✅ 1s 6s -83%
LP64 cvc5_arrays_exp ✅ 2s 6s -67%
LP64 z3* ✅ 1s 6s -83%
mld_ct_cmask_neg_i32 LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
mld_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
mld_ct_get_optblocker_i64 LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%
mld_ct_get_optblocker_u32 LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3_smt_only ✅ 2s 4s -50%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3_no_bv_extract ⚠️ 81s 4s +1925%
mld_ct_sel_int32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_h LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
mld_invntt_layer LP64 bitwuzla* ✅ 63s 108s -42%
mld_keccakf1600_extract_bytes LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600_permute_c LP64 cvc5_arrays_exp ✅ 5s 7s -29%
LP64 z3* ✅ 3s 7s -57%
mld_keccakf1600x4_extract_bytes_c LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 4s 2s +100%
mld_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 25s -52%
mld_ntt_layer LP64 bitwuzla* ✅ 25s 43s -42%
LP64 z3_no_bv_extract ✅ 1s 43s -98%
mld_polymat_expand_entry LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
mld_prepare_domain_separation_prefix LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 5s 4s +25%
mld_sample_pack_s1_s2 LP64 z3* ✅ 4s - new
mld_sample_pack_s1_s2_serial LP64 cvc5_mbqi_enum ✅ 226s - new
LP64 z3* ✅ 4s - new
mld_sign_attempt LP64 cvc5_arrays_exp ✅ 2s - new
LP64 z3* ✅ 4s - new
mld_sign_finish LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s - new
mld_sign_resume LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s - new
mld_value_barrier_i64 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 1s 4s -75%
mld_value_barrier_u8 LP64 cvc5_arrays_exp ✅ 2s 1s +100%
LP64 z3* ✅ 2s 1s +100%
montgomery_reduce LP64 cvc5_arrays_exp ✅ 2s 1s +100%
LP64 z3* ✅ 1s 1s +0%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 20s 3s +567%
LP64 z3* ✅ 3s 3s +0%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 4s - new
LP64 cvc5_mbqi_enum ✅ 8s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 bitwuzla ✅ 16s 5s +220%
LP64 z3* ✅ 4s 5s -20%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
pack_sig_c LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
pack_sig_h LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3_no_bv_extract* ✅ 2s 2s +0%
pack_sig_z LP64 bitwuzla ✅ 2s 1s +100%
LP64 z3* ✅ 2s 1s +100%
pack_sk_rho_key_tr LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 6s 6s +0%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 6s 5s +20%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 20s 3s +567%
LP64 z3* ✅ 2s 3s -33%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 1s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 20s 2s +900%
LP64 z3* ✅ 2s 2s +0%
poly_add LP64 z3* ✅ 5s 7s -29%
poly_caddq LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 1s 3s -67%
poly_caddq_c LP64 bitwuzla ✅ 18s 5s +260%
LP64 z3* ✅ 4s 5s -20%
poly_caddq_native LP64 bitwuzla ⚠️ 102s 4s +2450%
LP64 z3* ✅ 1s 4s -75%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 33s 2s +1550%
LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 117s 1s +11600%
LP64 z3* ✅ 1s 1s +0%
poly_challenge LP64 bitwuzla ⚠️ 20s 5s +300%
LP64 z3* ✅ 4s 5s -20%
poly_chknorm LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
poly_chknorm_c LP64 bitwuzla ✅ 8s 13s -38%
LP64 z3* ✅ 5s 13s -62%
poly_chknorm_native LP64 bitwuzla ✅ 7s 4s +75%
LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_aarch64 LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 3s 2s +50%
poly_chknorm_native_x86_64 LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 2s 4s -50%
poly_decompose LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_decompose_88_native_aarch64 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
poly_decompose_c LP64 z3* ✅ 6s 8s -25%
poly_decompose_native LP64 z3* ✅ 1s 5s -80%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_invntt_tomont LP64 bitwuzla ✅ 4s 5s -20%
LP64 z3* ✅ 2s 5s -60%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 10s -30%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 42s 5s +740%
LP64 z3* ✅ 3s 5s -40%
poly_ntt LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
poly_ntt_c LP64 bitwuzla ⚠️ 48s 22s +118%
LP64 z3_smt_only* ✅ 11s 22s -50%
poly_ntt_native LP64 bitwuzla ⚠️ 26s 2s +1200%
LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery LP64 bitwuzla ✅ 9s 2s +350%
LP64 z3* ✅ 3s 2s +50%
poly_pointwise_montgomery_c LP64 z3* ✅ 74s 116s -36%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 51s 4s +1175%
LP64 z3* ✅ 5s 4s +25%
poly_power2round LP64 bitwuzla ⚠️ 279s 7s +3886%
LP64 z3* ✅ 4s 7s -43%
poly_reduce LP64 bitwuzla ✅ 9s 4s +125%
LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 bitwuzla ✅ 13s 3s +333%
LP64 z3* ✅ 2s 3s -33%
poly_sub LP64 bitwuzla ✅ 16s 4s +300%
LP64 z3* ✅ 3s 4s -25%
poly_uniform LP64 z3* ✅ 1s 2s -50%
poly_uniform_4x LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta LP64 z3* ✅ 3s 5s -40%
poly_uniform_eta_4x LP64 z3* ✅ 8s 13s -38%
poly_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 3s -33%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 24s 3s +700%
LP64 z3* ✅ 1s 3s -67%
poly_use_hint_c LP64 cvc5_enum_inst ✅ 11s 2s +450%
LP64 z3* ✅ 1s 2s -50%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 93s 7s +1229%
LP64 z3* ✅ 2s 7s -71%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 28s 4s +600%
LP64 z3* ✅ 1s 4s -75%
poly_use_hint_native_x86_64 LP64 bitwuzla ✅ 29s - new
LP64 z3* ✅ 1s - new
polyeta_pack LP64 bitwuzla ✅ 3s 1s +200%
LP64 z3* ✅ 2s 1s +100%
polyeta_unpack LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 3s 4s -25%
polyt0_pack LP64 bitwuzla ✅ 4s 5s -20%
LP64 z3* ✅ 3s 5s -40%
polyt0_unpack LP64 bitwuzla ✅ 2s 13s -85%
LP64 z3* ✅ 6s 13s -54%
polyt1_pack LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 4s 3s +33%
polyt1_unpack LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 6s -83%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 8s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 114s 201s -43%
polyveck_caddq LP64 z3* ✅ 4s 7s -43%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 5s 7s -29%
polyveck_ntt LP64 z3* ✅ 3s 4s -25%
polyveck_reduce LP64 z3* ✅ 4s 6s -33%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
polyveck_unpack_eta_chknorm LP64 cvc5_mbqi_enum ✅ 18s - new
LP64 z3* ✅ 1s - new
polyvecl_chknorm LP64 z3* ✅ 2s 43s -95%
polyvecl_ntt LP64 z3* ✅ 3s 7s -57%
polyvecl_pointwise_acc_montgomery LP64 cvc5_mbqi_enum ✅ 2s 3s -33%
LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ✅ 3s 1s +200%
LP64 z3* ✅ 2s 1s +100%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 33s 2s +1550%
LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 34s 1s +3300%
LP64 z3* ✅ 3s 1s +200%
polyw1_pack LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
polyw1_pack_32 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 1s 2s -50%
polyw1_pack_88 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
polyw1_unpack LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
polyz_pack LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
polyz_unpack LP64 bitwuzla ✅ 6s 3s +100%
LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
polyz_unpack_19_native_aarch64 LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 3s 5s -40%
polyz_unpack_c LP64 bitwuzla ✅ 1s 9s -89%
LP64 z3* ✅ 5s 9s -44%
polyz_unpack_native LP64 bitwuzla ⚠️ 24s 3s +700%
LP64 z3* ✅ 4s 3s +33%
polyz_unpack_native_x86_64 LP64 bitwuzla ✅ 14s 3s +367%
LP64 z3* ✅ 1s 3s -67%
power2round LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
reduce32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
rej_eta LP64 bitwuzla* ✅ 2s 5s -60%
LP64 z3_smt_only ✅ 3s 5s -40%
rej_eta_c LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 17s 4s +325%
rej_eta_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3_smt_only ✅ 9s 3s +200%
rej_uniform LP64 bitwuzla ✅ 2s 7s -71%
LP64 z3* ✅ 4s 7s -43%
rej_uniform_c LP64 bitwuzla ✅ 2s 16s -88%
LP64 z3* ✅ 10s 16s -38%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3_smt_only ✅ 2s 5s -60%
rej_uniform_eta_native_x86_64 LP64 bitwuzla ✅ 4s - new
LP64 z3_smt_only* ✅ 1s - new
rej_uniform_native LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3_smt_only ✅ 18s 4s +350%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3_smt_only ✅ 3s 5s -40%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 4s - new
LP64 z3_smt_only* ✅ 9s - new
shake128_absorb LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 1s 2s -50%
shake128_finalize LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 bitwuzla ✅ 3s 6s -50%
LP64 z3* ✅ 1s 6s -83%
shake128_release LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
shake128_squeeze LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 1s 3s -67%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_smt_only ✅ 1s 2s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s 2s -50%
shake256 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 4s 2s +100%
shake256_absorb LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 1s 4s -75%
shake256_finalize LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%
shake256_init LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
shake256_release LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
shake256_squeeze LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 2s 4s -50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 4s 2s +100%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 3s 2s +50%
sig_unpack_hints LP64 bitwuzla ⚠️ 1289s 1s +128800%
LP64 z3* ✅ 16s 1s +1500%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 19s 3s +533%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 33s 5s +560%
sign_signature LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 3s 5s -40%
sign_signature_extmu LP64 z3* ✅ 4s 4s +0%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 6s +133%
sign_signature_pre_hash_internal LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 1s 3s -67%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 344s 7s +4814%
LP64 z3* ✅ 4s 7s -43%
sign_verify LP64 bitwuzla ✅ 2s 6s -67%
LP64 z3* ✅ 3s 6s -50%
sign_verify_extmu LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 207s 71s +192%
sign_verify_pre_hash_internal LP64 bitwuzla ✅ 1s 5s -80%
LP64 z3* ✅ 2s 5s -60%
sign_verify_pre_hash_shake256 LP64 bitwuzla ✅ 4s 6s -33%
LP64 z3* ✅ 4s 6s -33%
sk_s1hat_get_poly LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
sk_s2hat_get_poly LP64 bitwuzla ✅ 3s 1s +200%
LP64 z3* ✅ 2s 1s +100%
sk_t0hat_get_poly LP64 bitwuzla ✅ 3s 1s +200%
LP64 z3* ✅ 1s 1s +0%
sys_check_capability LP64 cvc5_arrays_exp ✅ 3s 1s +200%
LP64 z3* ✅ 1s 1s +0%
unpack_pk_t1 LP64 bitwuzla ✅ 11s 2s +450%
LP64 z3* ✅ 2s 2s +0%
unpack_sk LP64 z3* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ✅ 3s 1s +200%
LP64 z3* ✅ 2s 1s +100%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
unpack_sk_t0hat LP64 z3* ✅ 4s 4s +0%
use_hint LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 bitwuzla ✅ 7s 3s +133%
LP64 z3* ✅ 3s 3s +0%
yvec_init LP64 bitwuzla ✅ 1s 5s -80%
LP64 z3* ✅ 2s 5s -60%

@oqs-bot

oqs-bot commented Oct 25, 2026

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* ⚠️ 30s 12s +150%
intt_native_aarch64 LP64 bitwuzla ⚠️ 24s 4s +500%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 212s 34s +524%
mld_ct_memcmp LP64 z3_no_bv_extract ⚠️ 86s 1s +8500%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 22s 4s +450%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 23s 4s +475%
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 21s 5s +320%
poly_caddq_native LP64 bitwuzla ⚠️ 115s 3s +3733%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 37s 3s +1133%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 127s 3s +4133%
poly_challenge LP64 bitwuzla ⚠️ 35s 4s +775%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 48s 2s +2300%
poly_ntt_c LP64 bitwuzla ⚠️ 49s 19s +158%
poly_ntt_native LP64 bitwuzla ⚠️ 27s 4s +575%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 55s 3s +1733%
poly_power2round LP64 bitwuzla ⚠️ 281s 7s +3914%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 23s 4s +475%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 84s 1s +8300%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 30s 3s +900%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 48s 3s +1500%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 44s 3s +1367%
polyz_unpack_native LP64 bitwuzla ⚠️ 24s 1s +2300%
rej_eta_c LP64 z3 ⚠️ 22s 4s +450%
sig_unpack_hints LP64 bitwuzla ⚠️ 24s 4s +500%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 26s 6s +333%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 36s 6s +500%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 1553s 3s +51667%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 252s 47s +436%
Full Results (397 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1449s 1436s +0.9%
caddq LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 4s 3s +33%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
decompose LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 4s 2s +100%
fqmul LP64 bitwuzla* ✅ 26s 39s -33%
LP64 z3_smt_only ✅ 20s 39s -49%
fqscale LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 3s 1s +200%
intt_native_aarch64 LP64 bitwuzla ⚠️ 24s 4s +500%
LP64 z3* ✅ 1s 4s -75%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 3s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 8s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 bitwuzla ✅ 18s 4s +350%
LP64 z3* ✅ 1s 4s -75%
keccak_absorb LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 4s 4s +0%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 8s -50%
LP64 cvc5_arrays_exp ✅ 7s 8s -12%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_no_bv_extract ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 1s 1s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_smt_only ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_smt_only ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
keccak_finalize LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3* ✅ 1s 1s +0%
keccak_init LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%
keccak_squeeze LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3 ✅ 3s 5s -40%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
LP64 cvc5_arrays_exp ✅ 2s 1s +100%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 2s 2s +0%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 1s 1s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 4s 4s +0%
LP64 z3 ✅ 2s 4s -50%
keccakf1600x4_permute LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
keccakf1600x4_permute_native LP64 cvc5_arrays_exp ✅ 12s 25s -52%
LP64 z3* ✅ 12s 25s -52%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_no_bv_extract ✅ 2s 2s +0%
make_hint LP64 cvc5_arrays_exp ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 212s 34s +524%
mld_check_pct LP64 bitwuzla ✅ 4s 15s -73%
LP64 z3* ✅ 5s 15s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 6s -33%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 1s +100%
ILP32 cvc5_arrays_exp ✅ 1s 1s +0%
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 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 cvc5_arrays_exp ✅ 2s 5s -60%
LP64 z3* ✅ 3s 5s -40%
mld_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u32 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_smt_only ✅ 4s 3s +33%
mld_ct_memcmp LP64 bitwuzla* ✅ 4s 1s +300%
LP64 z3_no_bv_extract ⚠️ 86s 1s +8500%
mld_ct_sel_int32 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
mld_h LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 3s 2s +50%
mld_invntt_layer LP64 bitwuzla* ✅ 68s 111s -39%
mld_keccakf1600_extract_bytes LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 1s 1s +0%
mld_keccakf1600_permute_c LP64 cvc5_arrays_exp ✅ 5s 8s -38%
LP64 z3* ✅ 5s 8s -38%
mld_keccakf1600x4_extract_bytes_c LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
mld_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 1s 1s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 14s 23s -39%
mld_ntt_layer LP64 bitwuzla* ✅ 26s 44s -41%
LP64 z3_no_bv_extract ✅ 3s 44s -93%
mld_polymat_expand_entry LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
mld_prepare_domain_separation_prefix LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
mld_sample_pack_s1_s2 LP64 z3* ✅ 5s - new
mld_sample_pack_s1_s2_serial LP64 cvc5_mbqi_enum ✅ 539s - new
LP64 z3* ✅ 6s - new
mld_sign_attempt LP64 cvc5_arrays_exp ✅ 4s - new
LP64 z3* ✅ 3s - new
mld_sign_finish LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s - new
mld_sign_resume LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s - new
mld_value_barrier_i64 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_value_barrier_u32 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
mld_value_barrier_u8 LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
montgomery_reduce LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 22s 4s +450%
LP64 z3* ✅ 2s 4s -50%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 1s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 bitwuzla ✅ 18s 2s +800%
LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
pack_sig_c LP64 cvc5_arrays_exp ✅ 4s 2s +100%
LP64 z3* ✅ 4s 2s +100%
pack_sig_h LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3_no_bv_extract* ✅ 3s 3s +0%
pack_sig_z LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
pack_sk_rho_key_tr LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 5s -20%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 5s 8s -38%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 23s 4s +475%
LP64 z3* ✅ 3s 4s -25%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 9s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 21s 5s +320%
LP64 z3* ✅ 3s 5s -40%
poly_add LP64 z3* ✅ 5s 8s -38%
poly_caddq LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 2s 5s -60%
poly_caddq_c LP64 bitwuzla ✅ 19s 3s +533%
LP64 z3* ✅ 2s 3s -33%
poly_caddq_native LP64 bitwuzla ⚠️ 115s 3s +3733%
LP64 z3* ✅ 3s 3s +0%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 37s 3s +1133%
LP64 z3* ✅ 1s 3s -67%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 127s 3s +4133%
LP64 z3* ✅ 2s 3s -33%
poly_challenge LP64 bitwuzla ⚠️ 35s 4s +775%
LP64 z3* ✅ 2s 4s -50%
poly_chknorm LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 2s 4s -50%
poly_chknorm_c LP64 bitwuzla ✅ 8s 13s -38%
LP64 z3* ✅ 7s 13s -46%
poly_chknorm_native LP64 bitwuzla ✅ 7s 1s +600%
LP64 z3* ✅ 2s 1s +100%
poly_chknorm_native_aarch64 LP64 bitwuzla ✅ 1s 5s -80%
LP64 z3* ✅ 2s 5s -60%
poly_chknorm_native_x86_64 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 bitwuzla ✅ 6s 2s +200%
LP64 z3* ✅ 1s 2s -50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_decompose_88_native_aarch64 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 4s 2s +100%
poly_decompose_c LP64 z3* ✅ 3s 6s -50%
poly_decompose_native LP64 z3* ✅ 2s 2s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_invntt_tomont LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 1s 4s -75%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 9s -33%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 48s 2s +2300%
LP64 z3* ✅ 2s 2s +0%
poly_ntt LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 1s 2s -50%
poly_ntt_c LP64 bitwuzla ⚠️ 49s 19s +158%
LP64 z3_smt_only* ✅ 10s 19s -47%
poly_ntt_native LP64 bitwuzla ⚠️ 27s 4s +575%
LP64 z3* ✅ 2s 4s -50%
poly_permute_bitrev_to_custom_optional LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 4s 3s +33%
poly_pointwise_montgomery LP64 bitwuzla ✅ 10s 3s +233%
LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery_c LP64 z3* ✅ 76s 125s -39%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 55s 3s +1733%
LP64 z3* ✅ 3s 3s +0%
poly_power2round LP64 bitwuzla ⚠️ 281s 7s +3914%
LP64 z3* ✅ 3s 7s -57%
poly_reduce LP64 bitwuzla ✅ 8s 4s +100%
LP64 z3* ✅ 3s 4s -25%
poly_shiftl LP64 bitwuzla ✅ 12s 4s +200%
LP64 z3* ✅ 2s 4s -50%
poly_sub LP64 bitwuzla ✅ 14s 5s +180%
LP64 z3* ✅ 2s 5s -60%
poly_uniform LP64 z3* ✅ 4s 4s +0%
poly_uniform_4x LP64 z3* ✅ 3s 3s +0%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
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 cvc5_mbqi_enum ⚠️ 23s 4s +475%
LP64 z3* ✅ 2s 4s -50%
poly_use_hint_c LP64 cvc5_enum_inst ✅ 12s 4s +200%
LP64 z3* ✅ 1s 4s -75%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 84s 1s +8300%
LP64 z3* ✅ 2s 1s +100%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 30s 3s +900%
LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_x86_64 LP64 bitwuzla ✅ 29s - new
LP64 z3* ✅ 3s - new
polyeta_pack LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 1s 3s -67%
polyeta_unpack LP64 bitwuzla ✅ 3s 13s -77%
LP64 z3* ✅ 8s 13s -38%
polyt0_pack LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 4s 3s +33%
polyt0_unpack LP64 bitwuzla ✅ 3s 14s -79%
LP64 z3* ✅ 7s 14s -50%
polyt1_pack LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 2s 5s -60%
polyt1_unpack LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 2s 3s -33%
polyvec_matrix_expand_serial LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 13s -69%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 92s 196s -53%
polyveck_caddq LP64 z3* ✅ 6s 8s -25%
polyveck_decompose_pack_w1 LP64 z3* ✅ 14s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 4s +0%
polyveck_ntt LP64 z3* ✅ 1s 3s -67%
polyveck_reduce LP64 z3* ✅ 6s 6s +0%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
polyveck_unpack_eta_chknorm LP64 cvc5_mbqi_enum ✅ 16s - new
LP64 z3* ✅ 3s - new
polyvecl_chknorm LP64 z3* ✅ 1s 38s -97%
polyvecl_ntt LP64 z3* ✅ 4s 8s -50%
polyvecl_pointwise_acc_montgomery LP64 cvc5_mbqi_enum ✅ 1s 2s -50%
LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 48s 3s +1500%
LP64 z3* ✅ 1s 3s -67%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 44s 3s +1367%
LP64 z3* ✅ 2s 3s -33%
polyw1_pack LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
polyw1_pack_32 LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
polyw1_pack_88 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s - new
polyz_pack LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 3s 4s -25%
polyz_unpack LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 3s 4s -25%
polyz_unpack_19_native_aarch64 LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 2s 5s -60%
polyz_unpack_c LP64 bitwuzla ✅ 3s 7s -57%
LP64 z3* ✅ 4s 7s -43%
polyz_unpack_native LP64 bitwuzla ⚠️ 24s 1s +2300%
LP64 z3* ✅ 3s 1s +200%
polyz_unpack_native_x86_64 LP64 bitwuzla ✅ 16s 3s +433%
LP64 z3* ✅ 1s 3s -67%
power2round LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
reduce32 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
rej_eta LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3_smt_only ✅ 2s 2s +0%
rej_eta_c LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ⚠️ 22s 4s +450%
rej_eta_native LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3_smt_only ✅ 13s 4s +225%
rej_uniform LP64 bitwuzla ✅ 3s 7s -57%
LP64 z3* ✅ 8s 7s +14%
rej_uniform_c LP64 bitwuzla ✅ 2s 18s -89%
LP64 z3* ✅ 11s 18s -39%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_smt_only ✅ 4s 3s +33%
rej_uniform_eta_native_x86_64 LP64 bitwuzla ✅ 1s - new
LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3_smt_only ✅ 19s 5s +280%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_smt_only ✅ 1s 3s -67%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3_smt_only* ✅ 9s - new
shake128_absorb LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
shake128_finalize LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
shake128_init LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
shake128_squeeze LP64 bitwuzla* ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 2s 1s +100%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3_smt_only ✅ 2s 4s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 4s 1s +300%
LP64 z3 ✅ 3s 1s +200%
shake256 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
shake256_absorb LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
shake256_init LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
shake256_release LP64 bitwuzla ✅ 5s 5s +0%
LP64 z3* ✅ 3s 5s -40%
shake256_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3 ✅ 2s 5s -60%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3_smt_only ✅ 2s 4s -50%
sig_unpack_hints LP64 bitwuzla ⚠️ 24s 4s +500%
LP64 z3* ✅ 18s 4s +350%
sign_keypair LP64 z3* ✅ 5s 4s +25%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 26s 6s +333%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 36s 6s +500%
sign_signature LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 4s 4s +0%
sign_signature_extmu LP64 z3* ✅ 5s 4s +25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 3s +367%
sign_signature_pre_hash_internal LP64 bitwuzla ✅ 5s 2s +150%
LP64 z3* ✅ 3s 2s +50%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 1553s 3s +51667%
LP64 z3* ✅ 3s 3s +0%
sign_verify LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
sign_verify_extmu LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 252s 47s +436%
sign_verify_pre_hash_internal LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
sign_verify_pre_hash_shake256 LP64 bitwuzla ✅ 3s 7s -57%
LP64 z3* ✅ 3s 7s -57%
sk_s1hat_get_poly LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
sk_t0hat_get_poly LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 1s 3s -67%
sys_check_capability LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 3s 2s +50%
unpack_pk_t1 LP64 bitwuzla ✅ 10s 2s +400%
LP64 z3* ✅ 2s 2s +0%
unpack_sk LP64 z3* ✅ 1s 4s -75%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
unpack_sk_t0hat LP64 z3* ✅ 2s 4s -50%
use_hint LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
yvec_get_poly LP64 bitwuzla ✅ 6s 2s +200%
LP64 z3* ✅ 1s 2s -50%
yvec_init LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 1s 4s -75%

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2299s 1784s +28.9%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 165s 13s +1169%
intt_native_aarch64 LP64 bitwuzla ⚠️ 26s 3s +767%
intt_native_x86_64 LP64 bitwuzla ⚠️ 20s 3s +567%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 248s 63s +294%
mld_ct_memcmp LP64 z3_no_bv_extract ⚠️ 96s 2s +4700%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 25s 2s +1150%
ntt_native_x86_64 LP64 bitwuzla ⚠️ 20s 2s +900%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 25s 5s +400%
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 23s 3s +667%
poly_caddq_c LP64 bitwuzla ⚠️ 24s 2s +1100%
poly_caddq_native LP64 bitwuzla ⚠️ 134s 2s +6600%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 37s 2s +1750%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 146s 3s +4767%
poly_challenge LP64 bitwuzla ⚠️ 25s 6s +317%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 51s 2s +2450%
poly_ntt_c LP64 bitwuzla ⚠️ 56s 19s +195%
poly_ntt_native LP64 bitwuzla ⚠️ 30s 4s +650%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 55s 3s +1733%
poly_power2round LP64 bitwuzla ⚠️ 357s 4s +8825%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 26s 3s +767%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 88s 2s +4300%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 35s 3s +1067%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 44s 6s +633%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ⚠️ 38s 2s +1800%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ⚠️ 31s 3s +933%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 35s 3s +1067%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 36s 3s +1100%
polyz_unpack_native LP64 bitwuzla ⚠️ 28s 4s +600%
rej_uniform_native LP64 z3_smt_only ⚠️ 20s 4s +400%
sig_unpack_hints LP64 bitwuzla ⚠️ 1590s 2s +79400%
LP64 z3* ⚠️ 22s 2s +1000%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 21s 5s +320%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 38s 6s +533%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 237s 55s +331%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 383s 3s +12667%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 528s 177s +198%
sk_s1hat_get_poly LP64 bitwuzla ⚠️ 42s 6s +600%
sk_s2hat_get_poly LP64 bitwuzla ⚠️ 33s 2s +1550%
sk_t0hat_get_poly LP64 bitwuzla ⚠️ 32s 2s +1500%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ⚠️ 92s 2s +4500%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ⚠️ 164s 4s +4000%
yvec_get_poly LP64 bitwuzla ⚠️ 34s 3s +1033%
Full Results (397 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2299s 1784s +28.9%
caddq LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 165s 13s +1169%
decompose LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 1s 1s +0%
fqmul LP64 bitwuzla* ✅ 25s 40s -38%
LP64 z3_smt_only ✅ 23s 40s -43%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
intt_native_aarch64 LP64 bitwuzla ⚠️ 26s 3s +767%
LP64 z3* ✅ 3s 3s +0%
intt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 9s - new
LP64 z3 ✅ 1s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 9s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 bitwuzla ⚠️ 20s 3s +567%
LP64 z3* ✅ 5s 3s +67%
keccak_absorb LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 8s -50%
LP64 cvc5_arrays_exp ✅ 8s 8s +0%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_no_bv_extract ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 2s 4s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_smt_only ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
keccak_finalize LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
keccak_init LP64 bitwuzla ✅ 2s 1s +100%
LP64 z3* ✅ 2s 1s +100%
keccak_squeeze LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 3s 4s -25%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3 ✅ 1s 5s -80%
keccakf1600_extract_bytes (big endian) LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 1s 2s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3_smt_only ✅ 1s 2s -50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 4s 4s +0%
LP64 z3 ✅ 3s 4s -25%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 1s 4s -75%
keccakf1600x4_permute LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 1s 4s -75%
keccakf1600x4_permute_native LP64 cvc5_arrays_exp ✅ 12s 23s -48%
LP64 z3* ✅ 14s 23s -39%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_no_bv_extract ✅ 3s 3s +0%
make_hint LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 1s 2s -50%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 248s 63s +294%
mld_check_pct LP64 bitwuzla ✅ 5s 14s -64%
LP64 z3* ✅ 6s 14s -57%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 3s 7s -57%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 3s 2s +50%
ILP32 cvc5_arrays_exp ✅ 2s 2s +0%
ILP32 z3 ✅ 1s 2s -50%
LP64 bitwuzla ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_neg_i32 LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 cvc5_arrays_exp ✅ 1s 4s -75%
LP64 z3* ✅ 1s 4s -75%
mld_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
mld_ct_get_optblocker_i64 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u32 LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 2s 3s -33%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_smt_only ✅ 1s 2s -50%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_no_bv_extract ⚠️ 96s 2s +4700%
mld_ct_sel_int32 LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
mld_h LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_invntt_layer LP64 bitwuzla* ✅ 75s 109s -31%
mld_keccakf1600_extract_bytes LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%
mld_keccakf1600_permute_c LP64 cvc5_arrays_exp ✅ 4s 6s -33%
LP64 z3* ✅ 4s 6s -33%
mld_keccakf1600x4_extract_bytes_c LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
mld_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 15s 24s -38%
mld_ntt_layer LP64 bitwuzla* ✅ 30s 41s -27%
LP64 z3_no_bv_extract ✅ 2s 41s -95%
mld_polymat_expand_entry LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
mld_prepare_domain_separation_prefix LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
mld_sample_pack_s1_s2 LP64 z3* ✅ 4s - new
mld_sample_pack_s1_s2_serial LP64 cvc5_mbqi_enum ✅ 239s - new
LP64 z3* ✅ 3s - new
mld_sign_attempt LP64 cvc5_arrays_exp ✅ 3s - new
LP64 z3* ✅ 2s - new
mld_sign_finish LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
mld_sign_resume LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
mld_value_barrier_u32 LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
mld_value_barrier_u8 LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 cvc5_arrays_exp ✅ 1s 4s -75%
LP64 z3* ✅ 2s 4s -50%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 25s 2s +1150%
LP64 z3* ✅ 2s 2s +0%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 1s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 3s - new
ntt_native_x86_64 LP64 bitwuzla ⚠️ 20s 2s +900%
LP64 z3* ✅ 1s 2s -50%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
pack_sig_c LP64 cvc5_arrays_exp ✅ 3s 5s -40%
LP64 z3* ✅ 2s 5s -60%
pack_sig_h LP64 bitwuzla ✅ 4s 5s -20%
LP64 z3_no_bv_extract* ✅ 4s 5s -20%
pack_sig_z LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
pack_sk_rho_key_tr LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 2s 6s -67%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 8s -50%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 25s 5s +400%
LP64 z3* ✅ 4s 5s -20%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 8s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 23s 3s +667%
LP64 z3* ✅ 1s 3s -67%
poly_add LP64 z3* ✅ 5s 9s -44%
poly_caddq LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 bitwuzla ⚠️ 24s 2s +1100%
LP64 z3* ✅ 3s 2s +50%
poly_caddq_native LP64 bitwuzla ⚠️ 134s 2s +6600%
LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 37s 2s +1750%
LP64 z3* ✅ 1s 2s -50%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 146s 3s +4767%
LP64 z3* ✅ 2s 3s -33%
poly_challenge LP64 bitwuzla ⚠️ 25s 6s +317%
LP64 z3* ✅ 5s 6s -17%
poly_chknorm LP64 bitwuzla ✅ 5s 4s +25%
LP64 z3* ✅ 3s 4s -25%
poly_chknorm_c LP64 bitwuzla ✅ 9s 15s -40%
LP64 z3* ✅ 8s 15s -47%
poly_chknorm_native LP64 bitwuzla ✅ 7s 2s +250%
LP64 z3* ✅ 2s 2s +0%
poly_chknorm_native_aarch64 LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 2s 3s -33%
poly_chknorm_native_x86_64 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 3s 3s +0%
poly_decompose LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_decompose_88_native_aarch64 LP64 bitwuzla ✅ 4s 1s +300%
LP64 z3* ✅ 3s 1s +200%
poly_decompose_c LP64 z3* ✅ 3s 5s -40%
poly_decompose_native LP64 z3* ✅ 2s 3s -33%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_invntt_tomont LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 3s 3s +0%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 9s 11s -18%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 51s 2s +2450%
LP64 z3* ✅ 1s 2s -50%
poly_ntt LP64 bitwuzla ✅ 6s 2s +200%
LP64 z3* ✅ 3s 2s +50%
poly_ntt_c LP64 bitwuzla ⚠️ 56s 19s +195%
LP64 z3_smt_only* ✅ 12s 19s -37%
poly_ntt_native LP64 bitwuzla ⚠️ 30s 4s +650%
LP64 z3* ✅ 2s 4s -50%
poly_permute_bitrev_to_custom_optional LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 4s 2s +100%
poly_permute_bitrev_to_custom_optional_native LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 2s 4s -50%
poly_pointwise_montgomery LP64 bitwuzla ✅ 9s 3s +200%
LP64 z3* ✅ 4s 3s +33%
poly_pointwise_montgomery_c LP64 z3* ✅ 56s 125s -55%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 55s 3s +1733%
LP64 z3* ✅ 7s 3s +133%
poly_power2round LP64 bitwuzla ⚠️ 357s 4s +8825%
LP64 z3* ✅ 3s 4s -25%
poly_reduce LP64 bitwuzla ✅ 8s 3s +167%
LP64 z3* ✅ 2s 3s -33%
poly_shiftl LP64 bitwuzla ✅ 15s 3s +400%
LP64 z3* ✅ 2s 3s -33%
poly_sub LP64 bitwuzla ✅ 16s 3s +433%
LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 3s 4s -25%
poly_uniform_4x LP64 z3* ✅ 10s 13s -23%
poly_uniform_eta LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta_4x LP64 z3* ✅ 8s 14s -43%
poly_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 4s -50%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 26s 3s +767%
LP64 z3* ✅ 3s 3s +0%
poly_use_hint_c LP64 cvc5_enum_inst ✅ 12s 5s +140%
LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 88s 2s +4300%
LP64 z3* ✅ 4s 2s +100%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 35s 3s +1067%
LP64 z3* ✅ 5s 3s +67%
poly_use_hint_native_x86_64 LP64 bitwuzla ✅ 33s - new
LP64 z3* ✅ 2s - new
polyeta_pack LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 2s 3s -33%
polyeta_unpack LP64 bitwuzla ✅ 1s 8s -88%
LP64 z3* ✅ 5s 8s -38%
polyt0_pack LP64 bitwuzla ✅ 7s 3s +133%
LP64 z3* ✅ 3s 3s +0%
polyt0_unpack LP64 bitwuzla ✅ 2s 16s -88%
LP64 z3* ✅ 8s 16s -50%
polyt1_pack LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
polyt1_unpack LP64 bitwuzla ✅ 4s 5s -20%
LP64 z3* ✅ 2s 5s -60%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 87s 110s -21%
polyvec_matrix_expand_serial LP64 z3* ✅ 15s 27s -44%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 3s 1s +200%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 17s 18s -6%
polyveck_caddq LP64 z3* ✅ 7s 6s +17%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 7s 8s -12%
polyveck_ntt LP64 z3* ✅ 6s 7s -14%
polyveck_reduce LP64 z3* ✅ 2s 4s -50%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 44s 6s +633%
LP64 z3* ✅ 3s 6s -50%
polyveck_unpack_eta_chknorm LP64 cvc5_mbqi_enum ✅ 20s - new
LP64 z3* ✅ 3s - new
polyvecl_chknorm LP64 z3* ✅ 2s 7s -71%
polyvecl_ntt LP64 z3* ✅ 6s 4s +50%
polyvecl_pointwise_acc_montgomery LP64 cvc5_mbqi_enum ✅ 10s 3s +233%
LP64 z3_smt_only* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 138s 210s -34%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 2s -50%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ⚠️ 38s 2s +1800%
LP64 z3* ✅ 2s 2s +0%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ⚠️ 31s 3s +933%
LP64 z3* ✅ 3s 3s +0%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 35s 3s +1067%
LP64 z3* ✅ 2s 3s -33%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 36s 3s +1100%
LP64 z3* ✅ 1s 3s -67%
polyw1_pack LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 1s 4s -75%
polyw1_pack_88 LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s - new
polyz_pack LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 4s 3s +33%
polyz_unpack LP64 bitwuzla ✅ 7s 3s +133%
LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
polyz_unpack_19_native_aarch64 LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
polyz_unpack_c LP64 bitwuzla ✅ 1s 13s -92%
LP64 z3* ✅ 2s 13s -85%
polyz_unpack_native LP64 bitwuzla ⚠️ 28s 4s +600%
LP64 z3* ✅ 1s 4s -75%
polyz_unpack_native_x86_64 LP64 bitwuzla ✅ 19s 3s +533%
LP64 z3* ✅ 2s 3s -33%
power2round LP64 bitwuzla ✅ 3s 1s +200%
LP64 z3* ✅ 2s 1s +100%
reduce32 LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 4s 2s +100%
rej_eta_c LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3 ✅ 14s 5s +180%
rej_eta_native LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_smt_only ✅ 12s 3s +300%
rej_uniform LP64 bitwuzla ✅ 3s 18s -83%
LP64 z3* ✅ 14s 18s -22%
rej_uniform_c LP64 bitwuzla ✅ 2s 14s -86%
LP64 z3* ✅ 11s 14s -21%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3_smt_only ✅ 2s 4s -50%
rej_uniform_eta_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 5s 4s +25%
LP64 z3_smt_only ⚠️ 20s 4s +400%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3_smt_only ✅ 2s 3s -33%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 5s - new
LP64 z3_smt_only* ✅ 9s - new
shake128_absorb LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 1s 2s -50%
shake128_finalize LP64 cvc5_arrays_exp ✅ 4s 1s +300%
LP64 z3* ✅ 2s 1s +100%
shake128_init LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 1s 3s -67%
shake128_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3_smt_only ✅ 3s 3s +0%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
shake256 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 3s 2s +50%
shake256_finalize LP64 cvc5_arrays_exp ✅ 2s 1s +100%
LP64 z3* ✅ 2s 1s +100%
shake256_init LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
shake256_release LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 3s 2s +50%
shake256_squeeze LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 1s 3s -67%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s 3s +0%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3_smt_only ✅ 2s 2s +0%
sig_unpack_hints LP64 bitwuzla ⚠️ 1590s 2s +79400%
LP64 z3* ⚠️ 22s 2s +1000%
sign_keypair LP64 z3* ✅ 3s 3s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 21s 5s +320%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 38s 6s +533%
sign_signature LP64 bitwuzla ✅ 4s 6s -33%
LP64 z3* ✅ 3s 6s -50%
sign_signature_extmu LP64 z3* ✅ 3s 2s +50%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 237s 55s +331%
sign_signature_pre_hash_internal LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 383s 3s +12667%
LP64 z3* ✅ 2s 3s -33%
sign_verify LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 2s 3s -33%
sign_verify_extmu LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 5s 3s +67%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 528s 177s +198%
sign_verify_pre_hash_internal LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 3s 5s -40%
sign_verify_pre_hash_shake256 LP64 bitwuzla ✅ 4s 5s -20%
LP64 z3* ✅ 5s 5s +0%
sk_s1hat_get_poly LP64 bitwuzla ⚠️ 42s 6s +600%
LP64 z3* ✅ 3s 6s -50%
sk_s2hat_get_poly LP64 bitwuzla ⚠️ 33s 2s +1550%
LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 bitwuzla ⚠️ 32s 2s +1500%
LP64 z3* ✅ 2s 2s +0%
sys_check_capability LP64 cvc5_arrays_exp ✅ 1s 4s -75%
LP64 z3* ✅ 3s 4s -25%
unpack_pk_t1 LP64 bitwuzla ✅ 16s 5s +220%
LP64 z3* ✅ 3s 5s -40%
unpack_sk LP64 z3* ✅ 2s 3s -33%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ⚠️ 92s 2s +4500%
LP64 z3* ✅ 2s 2s +0%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ⚠️ 164s 4s +4000%
LP64 z3* ✅ 4s 4s +0%
unpack_sk_t0hat LP64 z3* ✅ 3s 5s -40%
use_hint LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
yvec_get_poly LP64 bitwuzla ⚠️ 34s 3s +1033%
LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 bitwuzla ✅ 8s 3s +167%
LP64 z3* ✅ 3s 3s +0%

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 3411s 2151s +58.6%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 249s 19s +1211%
intt_native_aarch64 LP64 bitwuzla ⚠️ 22s 3s +633%
intt_native_x86_64 LP64 bitwuzla ⚠️ 20s 3s +567%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 335s 55s +509%
mld_ct_memcmp LP64 z3_no_bv_extract ⚠️ 84s 3s +2700%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 21s 6s +250%
pointwise_native_aarch64 LP64 bitwuzla ⚠️ 22s 5s +340%
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 20s 2s +900%
poly_caddq_native LP64 bitwuzla ⚠️ 105s 4s +2525%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 36s 3s +1100%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 125s 2s +6150%
poly_challenge LP64 bitwuzla ⚠️ 35s 5s +600%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 47s 5s +840%
poly_ntt_c LP64 bitwuzla ⚠️ 50s 21s +138%
poly_ntt_native LP64 bitwuzla ⚠️ 26s 3s +767%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 54s 5s +980%
poly_power2round LP64 bitwuzla ⚠️ 285s 3s +9400%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 25s 1s +2400%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 90s 3s +2900%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 30s 2s +1400%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 55s 4s +1275%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ⚠️ 75s 2s +3650%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ⚠️ 46s 4s +1050%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 43s 5s +760%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 46s 4s +1050%
polyz_unpack_native LP64 bitwuzla ⚠️ 29s 4s +625%
sig_unpack_hints LP64 bitwuzla ⚠️ 26s 3s +767%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 21s 6s +250%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 33s 6s +450%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 387s 42s +821%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 1654s 6s +27467%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 1298s 97s +1238%
sk_s1hat_get_poly LP64 bitwuzla ⚠️ 32s 3s +967%
sk_s2hat_get_poly LP64 bitwuzla ⚠️ 34s 3s +1033%
sk_t0hat_get_poly LP64 bitwuzla ⚠️ 35s 4s +775%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ⚠️ 88s 2s +4300%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ⚠️ 299s 3s +9867%
yvec_get_poly LP64 bitwuzla ⚠️ 38s 4s +850%
Full Results (397 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 3411s 2151s +58.6%
caddq LP64 bitwuzla ✅ 1s 4s -75%
LP64 z3* ✅ 1s 4s -75%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 249s 19s +1211%
decompose LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
fqmul LP64 bitwuzla* ✅ 24s 43s -44%
LP64 z3_smt_only ✅ 22s 43s -49%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s 3s +0%
intt_native_aarch64 LP64 bitwuzla ⚠️ 22s 3s +633%
LP64 z3* ✅ 2s 3s -33%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 7s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 bitwuzla ⚠️ 20s 3s +567%
LP64 z3* ✅ 5s 3s +67%
keccak_absorb LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 9s -44%
LP64 cvc5_arrays_exp ✅ 8s 9s -11%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3_no_bv_extract ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 1s +0%
LP64 cvc5_arrays_exp ✅ 2s 1s +100%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3 ✅ 2s 4s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_smt_only ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3_smt_only ✅ 3s 4s -25%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 4s 2s +100%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
keccak_finalize LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3* ✅ 4s 1s +300%
keccak_init LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
keccak_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 3s 2s +50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 1s 4s -75%
keccakf1600_extract_bytes (big endian) LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
keccakf1600_permute LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 4s 3s +33%
keccakf1600_permute_native LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 1s 4s -75%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 3s 3s +0%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3_smt_only ✅ 1s 2s -50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s 2s -50%
keccakf1600x4_permute LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
keccakf1600x4_permute_native LP64 cvc5_arrays_exp ✅ 13s 23s -43%
LP64 z3* ✅ 12s 23s -48%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3_no_bv_extract ✅ 1s 3s -67%
make_hint LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 335s 55s +509%
mld_check_pct LP64 bitwuzla ✅ 7s 16s -56%
LP64 z3* ✅ 6s 16s -62%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 6s 8s -25%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 3s -67%
ILP32 cvc5_arrays_exp ✅ 2s 3s -33%
ILP32 z3 ✅ 2s 3s -33%
LP64 bitwuzla ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
mld_ct_cmask_neg_i32 LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 3s 4s -25%
mld_ct_cmask_nonzero_u32 LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
mld_ct_get_optblocker_i64 LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
mld_ct_get_optblocker_u32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3_smt_only ✅ 2s 3s -33%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3_no_bv_extract ⚠️ 84s 3s +2700%
mld_ct_sel_int32 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 1s 3s -67%
mld_h LP64 bitwuzla ✅ 6s 3s +100%
LP64 z3* ✅ 4s 3s +33%
mld_invntt_layer LP64 bitwuzla* ✅ 64s 115s -44%
mld_keccakf1600_extract_bytes LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 1s 4s -75%
mld_keccakf1600_permute_c LP64 cvc5_arrays_exp ✅ 5s 7s -29%
LP64 z3* ✅ 4s 7s -43%
mld_keccakf1600x4_extract_bytes_c LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
mld_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 1s 4s -75%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 13s 24s -46%
mld_ntt_layer LP64 bitwuzla* ✅ 24s 45s -47%
LP64 z3_no_bv_extract ✅ 3s 45s -93%
mld_polymat_expand_entry LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
mld_prepare_domain_separation_prefix LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 4s 4s +0%
mld_sample_pack_s1_s2 LP64 z3* ✅ 7s - new
mld_sample_pack_s1_s2_serial LP64 cvc5_mbqi_enum ✅ 546s - new
LP64 z3* ✅ 4s - new
mld_sign_attempt LP64 cvc5_arrays_exp ✅ 2s - new
LP64 z3* ✅ 2s - new
mld_sign_finish LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s - new
mld_sign_resume LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 bitwuzla ✅ 2s 1s +100%
LP64 z3* ✅ 2s 1s +100%
mld_value_barrier_u32 LP64 bitwuzla ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u8 LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
montgomery_reduce LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
ntt_native_aarch64 LP64 bitwuzla ⚠️ 21s 6s +250%
LP64 z3* ✅ 2s 6s -67%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 cvc5_mbqi_enum ✅ 5s - new
LP64 z3 ✅ 1s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 bitwuzla ✅ 19s 2s +850%
LP64 z3* ✅ 6s 2s +200%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
pack_sig_c LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
pack_sig_h LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3_no_bv_extract* ✅ 1s 4s -75%
pack_sig_z LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 3s 5s -40%
pack_sk_rho_key_tr LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 3s - 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 bitwuzla ⚠️ 22s 5s +340%
LP64 z3* ✅ 2s 5s -60%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 8s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 cvc5_mbqi_enum ✅ 9s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 bitwuzla ⚠️ 20s 2s +900%
LP64 z3* ✅ 3s 2s +50%
poly_add LP64 z3* ✅ 3s 6s -50%
poly_caddq LP64 bitwuzla ✅ 4s 2s +100%
LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 bitwuzla ✅ 19s 3s +533%
LP64 z3* ✅ 2s 3s -33%
poly_caddq_native LP64 bitwuzla ⚠️ 105s 4s +2525%
LP64 z3* ✅ 3s 4s -25%
poly_caddq_native_aarch64 LP64 cvc5_mbqi_enum ⚠️ 36s 3s +1100%
LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_x86_64 LP64 bitwuzla ⚠️ 125s 2s +6150%
LP64 z3* ✅ 4s 2s +100%
poly_challenge LP64 bitwuzla ⚠️ 35s 5s +600%
LP64 z3* ✅ 2s 5s -60%
poly_chknorm LP64 bitwuzla ✅ 4s 3s +33%
LP64 z3* ✅ 3s 3s +0%
poly_chknorm_c LP64 bitwuzla ✅ 9s 15s -40%
LP64 z3* ✅ 5s 15s -67%
poly_chknorm_native LP64 bitwuzla ✅ 7s 4s +75%
LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 bitwuzla ✅ 2s 4s -50%
LP64 z3* ✅ 3s 4s -25%
poly_chknorm_native_x86_64 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 4s 2s +100%
poly_decompose LP64 bitwuzla ✅ 6s 3s +100%
LP64 z3* ✅ 3s 3s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 5s -60%
poly_decompose_88_native_aarch64 LP64 bitwuzla ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
poly_decompose_c LP64 z3* ✅ 4s 5s -20%
poly_decompose_native LP64 z3* ✅ 1s 2s -50%
poly_decompose_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_invntt_tomont LP64 bitwuzla ✅ 4s 1s +300%
LP64 z3* ✅ 3s 1s +200%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 12s -50%
poly_invntt_tomont_native LP64 bitwuzla ⚠️ 47s 5s +840%
LP64 z3* ✅ 3s 5s -40%
poly_ntt LP64 bitwuzla ✅ 6s 3s +100%
LP64 z3* ✅ 2s 3s -33%
poly_ntt_c LP64 bitwuzla ⚠️ 50s 21s +138%
LP64 z3_smt_only* ✅ 9s 21s -57%
poly_ntt_native LP64 bitwuzla ⚠️ 26s 3s +767%
LP64 z3* ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 2s 5s -60%
poly_pointwise_montgomery LP64 bitwuzla ✅ 11s 4s +175%
LP64 z3* ✅ 1s 4s -75%
poly_pointwise_montgomery_c LP64 z3* ✅ 48s 144s -67%
poly_pointwise_montgomery_native LP64 cvc5_mbqi_enum ⚠️ 54s 5s +980%
LP64 z3* ✅ 2s 5s -60%
poly_power2round LP64 bitwuzla ⚠️ 285s 3s +9400%
LP64 z3* ✅ 5s 3s +67%
poly_reduce LP64 bitwuzla ✅ 8s 2s +300%
LP64 z3* ✅ 2s 2s +0%
poly_shiftl LP64 bitwuzla ✅ 12s 4s +200%
LP64 z3* ✅ 4s 4s +0%
poly_sub LP64 bitwuzla ✅ 14s 3s +367%
LP64 z3* ✅ 5s 3s +67%
poly_uniform LP64 z3* ✅ 3s 4s -25%
poly_uniform_4x LP64 z3* ✅ 8s 13s -38%
poly_uniform_eta LP64 z3* ✅ 2s 4s -50%
poly_uniform_eta_4x LP64 z3* ✅ 8s 11s -27%
poly_uniform_gamma1 LP64 z3* ✅ 3s 4s -25%
poly_uniform_gamma1_4x LP64 z3* ✅ 4s 3s +33%
poly_use_hint LP64 cvc5_mbqi_enum ⚠️ 25s 1s +2400%
LP64 z3* ✅ 2s 1s +100%
poly_use_hint_c LP64 cvc5_enum_inst ✅ 13s 2s +550%
LP64 z3* ✅ 3s 2s +50%
poly_use_hint_native LP64 cvc5_mbqi_enum ⚠️ 90s 3s +2900%
LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_aarch64 LP64 bitwuzla ⚠️ 30s 2s +1400%
LP64 z3* ✅ 3s 2s +50%
poly_use_hint_native_x86_64 LP64 bitwuzla ✅ 30s - new
LP64 z3* ✅ 3s - new
polyeta_pack LP64 bitwuzla ✅ 5s 4s +25%
LP64 z3* ✅ 2s 4s -50%
polyeta_unpack LP64 bitwuzla ✅ 2s 17s -88%
LP64 z3* ✅ 5s 17s -71%
polyt0_pack LP64 bitwuzla ✅ 6s 4s +50%
LP64 z3* ✅ 3s 4s -25%
polyt0_unpack LP64 bitwuzla ✅ 5s 14s -64%
LP64 z3* ✅ 11s 14s -21%
polyt1_pack LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
polyt1_unpack LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 6s 4s +50%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 116s 324s -64%
polyvec_matrix_expand_serial LP64 z3* ✅ 24s 38s -37%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 14s 18s -22%
polyveck_caddq LP64 z3* ✅ 4s 8s -50%
polyveck_decompose_pack_w1 LP64 z3* ✅ 5s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 9s -56%
polyveck_ntt LP64 z3* ✅ 7s 11s -36%
polyveck_reduce LP64 z3* ✅ 1s 3s -67%
polyveck_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 55s 4s +1275%
LP64 z3* ✅ 3s 4s -25%
polyveck_unpack_eta_chknorm LP64 cvc5_mbqi_enum ✅ 19s - new
LP64 z3* ✅ 4s - new
polyvecl_chknorm LP64 z3* ✅ 5s 7s -29%
polyvecl_ntt LP64 z3* ✅ 2s 7s -71%
polyvecl_pointwise_acc_montgomery LP64 cvc5_mbqi_enum ✅ 15s 5s +200%
LP64 z3_smt_only* ✅ 2s 5s -60%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 156s 353s -56%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 4s 3s +33%
polyvecl_uniform_gamma1 LP64 cvc5_mbqi_enum ⚠️ 75s 2s +3650%
LP64 z3* ✅ 1s 2s -50%
polyvecl_uniform_gamma1_serial LP64 cvc5_mbqi_enum ⚠️ 46s 4s +1050%
LP64 z3* ✅ 2s 4s -50%
polyvecl_unpack_eta LP64 cvc5_mbqi_enum ⚠️ 43s 5s +760%
LP64 z3* ✅ 2s 5s -60%
polyvecl_unpack_z LP64 cvc5_mbqi_enum ⚠️ 46s 4s +1050%
LP64 z3* ✅ 1s 4s -75%
polyw1_pack LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 1s 4s -75%
polyw1_pack_32 LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 2s 4s -50%
polyw1_pack_88 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
polyw1_unpack LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s - new
polyz_pack LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 2s 5s -60%
polyz_unpack LP64 bitwuzla ✅ 7s 2s +250%
LP64 z3* ✅ 2s 2s +0%
polyz_unpack_17_native_aarch64 LP64 bitwuzla ✅ 3s 3s +0%
LP64 z3* ✅ 3s 3s +0%
polyz_unpack_19_native_aarch64 LP64 bitwuzla ✅ 4s 4s +0%
LP64 z3* ✅ 4s 4s +0%
polyz_unpack_c LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 5s 3s +67%
polyz_unpack_native LP64 bitwuzla ⚠️ 29s 4s +625%
LP64 z3* ✅ 4s 4s +0%
polyz_unpack_native_x86_64 LP64 bitwuzla ✅ 15s 3s +400%
LP64 z3* ✅ 2s 3s -33%
power2round LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 3s 4s -25%
reduce32 LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 4s 3s +33%
rej_eta LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3_smt_only ✅ 4s 4s +0%
rej_eta_c LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3 ✅ 17s 5s +240%
rej_eta_native LP64 bitwuzla* ✅ 2s 6s -67%
LP64 z3_smt_only ✅ 11s 6s +83%
rej_uniform LP64 bitwuzla ✅ 2s 15s -87%
LP64 z3* ✅ 13s 15s -13%
rej_uniform_c LP64 bitwuzla ✅ 4s 19s -79%
LP64 z3* ✅ 11s 19s -42%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 5s -40%
LP64 z3_smt_only ✅ 4s 5s -20%
rej_uniform_eta_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 1s 8s -88%
LP64 z3_smt_only ✅ 17s 8s +112%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 4s 2s +100%
LP64 z3_smt_only ✅ 1s 2s -50%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3_smt_only* ✅ 9s - new
shake128_absorb LP64 cvc5_arrays_exp ✅ 2s 4s -50%
LP64 z3* ✅ 2s 4s -50%
shake128_finalize LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 bitwuzla ✅ 1s 1s +0%
LP64 z3* ✅ 1s 1s +0%
shake128_release LP64 bitwuzla ✅ 3s 4s -25%
LP64 z3* ✅ 4s 4s +0%
shake128_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 5s -60%
LP64 z3_smt_only ✅ 3s 5s -40%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 1s 3s -67%
shake256 LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 bitwuzla ✅ 3s 2s +50%
LP64 z3* ✅ 3s 2s +50%
shake256_finalize LP64 cvc5_arrays_exp ✅ 4s 2s +100%
LP64 z3* ✅ 3s 2s +50%
shake256_init LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 3s 2s +50%
shake256_release LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 4s 2s +100%
shake256x4_absorb_once LP64 bitwuzla* ✅ 4s 2s +100%
LP64 z3 ✅ 1s 2s -50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3_smt_only ✅ 2s 1s +100%
sig_unpack_hints LP64 bitwuzla ⚠️ 26s 3s +767%
LP64 z3* ✅ 16s 3s +433%
sign_keypair LP64 z3* ✅ 3s 4s -25%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 21s 6s +250%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 33s 6s +450%
sign_signature LP64 bitwuzla ✅ 5s 5s +0%
LP64 z3* ✅ 4s 5s -20%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 387s 42s +821%
sign_signature_pre_hash_internal LP64 bitwuzla ✅ 2s 5s -60%
LP64 z3* ✅ 2s 5s -60%
sign_signature_pre_hash_shake256 LP64 bitwuzla ⚠️ 1654s 6s +27467%
LP64 z3* ✅ 4s 6s -33%
sign_verify LP64 bitwuzla ✅ 3s 5s -40%
LP64 z3* ✅ 2s 5s -60%
sign_verify_extmu LP64 bitwuzla ✅ 5s 3s +67%
LP64 z3* ✅ 2s 3s -33%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 1298s 97s +1238%
sign_verify_pre_hash_internal LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
sign_verify_pre_hash_shake256 LP64 bitwuzla ✅ 1s 3s -67%
LP64 z3* ✅ 5s 3s +67%
sk_s1hat_get_poly LP64 bitwuzla ⚠️ 32s 3s +967%
LP64 z3* ✅ 1s 3s -67%
sk_s2hat_get_poly LP64 bitwuzla ⚠️ 34s 3s +1033%
LP64 z3* ✅ 2s 3s -33%
sk_t0hat_get_poly LP64 bitwuzla ⚠️ 35s 4s +775%
LP64 z3* ✅ 2s 4s -50%
sys_check_capability LP64 cvc5_arrays_exp ✅ 3s 3s +0%
LP64 z3* ✅ 1s 3s -67%
unpack_pk_t1 LP64 bitwuzla ✅ 12s 1s +1100%
LP64 z3* ✅ 2s 1s +100%
unpack_sk LP64 z3* ✅ 2s 5s -60%
unpack_sk_s1hat LP64 cvc5_mbqi_enum ⚠️ 88s 2s +4300%
LP64 z3* ✅ 3s 2s +50%
unpack_sk_s2hat LP64 cvc5_mbqi_enum ⚠️ 299s 3s +9867%
LP64 z3* ✅ 3s 3s +0%
unpack_sk_t0hat LP64 z3* ✅ 3s 7s -57%
use_hint LP64 bitwuzla ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
yvec_get_poly LP64 bitwuzla ⚠️ 38s 4s +850%
LP64 z3* ✅ 2s 4s -50%
yvec_init LP64 bitwuzla ✅ 15s 4s +275%
LP64 z3* ✅ 4s 4s +0%

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Mac Mini (M1, 2020) benchmarks (opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 47850 cycles 47126 cycles 1.02
ML-DSA-44 sign 131896 cycles 131335 cycles 1.00
ML-DSA-44 verify 47860 cycles 47312 cycles 1.01
ML-DSA-65 keypair 83022 cycles 81745 cycles 1.02
ML-DSA-65 sign 216214 cycles 215190 cycles 1.00
ML-DSA-65 verify 80333 cycles 79350 cycles 1.01
ML-DSA-87 keypair 135848 cycles 133525 cycles 1.02
ML-DSA-87 sign 279803 cycles 277747 cycles 1.01
ML-DSA-87 verify 136220 cycles 134254 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Mac Mini (M1, 2020) benchmarks (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 114075 cycles 113525 cycles 1.00
ML-DSA-44 sign 404961 cycles 402727 cycles 1.01
ML-DSA-44 verify 120705 cycles 120055 cycles 1.01
ML-DSA-65 keypair 194240 cycles 193928 cycles 1.00
ML-DSA-65 sign 653484 cycles 652518 cycles 1.00
ML-DSA-65 verify 193238 cycles 192961 cycles 1.00
ML-DSA-87 keypair 320038 cycles 320038 cycles 1
ML-DSA-87 sign 831284 cycles 831271 cycles 1.00
ML-DSA-87 verify 326847 cycles 326856 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

SpacemiT K1 8 (Banana Pi F3) benchmarks (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 764872 cycles 765870 cycles 1.00
ML-DSA-44 sign 3144019 cycles 3146677 cycles 1.00
ML-DSA-44 verify 858072 cycles 859050 cycles 1.00
ML-DSA-65 keypair 1289220 cycles 1289680 cycles 1.00
ML-DSA-65 sign 5083078 cycles 5086864 cycles 1.00
ML-DSA-65 verify 1367790 cycles 1365581 cycles 1.00
ML-DSA-87 keypair 2123426 cycles 2122619 cycles 1.00
ML-DSA-87 sign 6367315 cycles 6367553 cycles 1.00
ML-DSA-87 verify 2225771 cycles 2224997 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Intel Xeon 4th gen (c7i)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 43926 cycles 43983 cycles 1.00
ML-DSA-44 sign 130809 cycles 130056 cycles 1.01
ML-DSA-44 verify 45215 cycles 45131 cycles 1.00
ML-DSA-65 keypair 75120 cycles 74720 cycles 1.01
ML-DSA-65 sign 213034 cycles 212268 cycles 1.00
ML-DSA-65 verify 74480 cycles 74545 cycles 1.00
ML-DSA-87 keypair 124120 cycles 123968 cycles 1.00
ML-DSA-87 sign 270923 cycles 270660 cycles 1.00
ML-DSA-87 verify 120447 cycles 119975 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Intel Xeon 4th gen (c7i) (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 92024 cycles 91944 cycles 1.00
ML-DSA-44 sign 347587 cycles 346827 cycles 1.00
ML-DSA-44 verify 99314 cycles 99264 cycles 1.00
ML-DSA-65 keypair 155769 cycles 155458 cycles 1.00
ML-DSA-65 sign 568913 cycles 568310 cycles 1.00
ML-DSA-65 verify 159959 cycles 159452 cycles 1.00
ML-DSA-87 keypair 257617 cycles 258097 cycles 1.00
ML-DSA-87 sign 718404 cycles 720604 cycles 1.00
ML-DSA-87 verify 263153 cycles 263959 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

AMD EPYC 4th gen (c7a)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 47893 cycles 47998 cycles 1.00
ML-DSA-44 sign 139938 cycles 139164 cycles 1.01
ML-DSA-44 verify 49735 cycles 49838 cycles 1.00
ML-DSA-65 keypair 82604 cycles 82076 cycles 1.01
ML-DSA-65 sign 227666 cycles 228277 cycles 1.00
ML-DSA-65 verify 82677 cycles 82696 cycles 1.00
ML-DSA-87 keypair 132645 cycles 132753 cycles 1.00
ML-DSA-87 sign 280709 cycles 280218 cycles 1.00
ML-DSA-87 verify 129611 cycles 128370 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton5

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 53152 cycles 52389 cycles 1.01
ML-DSA-44 sign 162730 cycles 162250 cycles 1.00
ML-DSA-44 verify 55538 cycles 54851 cycles 1.01
ML-DSA-65 keypair 92541 cycles 91248 cycles 1.01
ML-DSA-65 sign 267412 cycles 266238 cycles 1.00
ML-DSA-65 verify 91136 cycles 89892 cycles 1.01
ML-DSA-87 keypair 149816 cycles 147999 cycles 1.01
ML-DSA-87 sign 336660 cycles 334762 cycles 1.01
ML-DSA-87 verify 147217 cycles 145134 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

AMD EPYC 4th gen (c7a) (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 115305 cycles 115166 cycles 1.00
ML-DSA-44 sign 420016 cycles 420506 cycles 1.00
ML-DSA-44 verify 123860 cycles 123641 cycles 1.00
ML-DSA-65 keypair 195152 cycles 195557 cycles 1.00
ML-DSA-65 sign 680931 cycles 682193 cycles 1.00
ML-DSA-65 verify 199547 cycles 199861 cycles 1.00
ML-DSA-87 keypair 325674 cycles 325054 cycles 1.00
ML-DSA-87 sign 866429 cycles 867512 cycles 1.00
ML-DSA-87 verify 330657 cycles 330972 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

AMD EPYC 3rd gen (c6a)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 53289 cycles 52982 cycles 1.01
ML-DSA-44 sign 156537 cycles 156570 cycles 1.00
ML-DSA-44 verify 54465 cycles 54251 cycles 1.00
ML-DSA-65 keypair 91688 cycles 91220 cycles 1.01
ML-DSA-65 sign 258385 cycles 254101 cycles 1.02
ML-DSA-65 verify 92065 cycles 90192 cycles 1.02
ML-DSA-87 keypair 146897 cycles 145471 cycles 1.01
ML-DSA-87 sign 311874 cycles 312261 cycles 1.00
ML-DSA-87 verify 140010 cycles 139318 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton5 (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 102410 cycles 102853 cycles 1.00
ML-DSA-44 sign 373339 cycles 373708 cycles 1.00
ML-DSA-44 verify 111301 cycles 111244 cycles 1.00
ML-DSA-65 keypair 200362 cycles 177302 cycles 1.13
ML-DSA-65 sign 602674 cycles 605296 cycles 1.00
ML-DSA-65 verify 178157 cycles 179442 cycles 0.99
ML-DSA-87 keypair 285737 cycles 284775 cycles 1.00
ML-DSA-87 sign 767831 cycles 771818 cycles 0.99
ML-DSA-87 verify 294953 cycles 294488 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Graviton5 (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-65 keypair 200362 cycles 177302 cycles 1.13

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

AMD EPYC 3rd gen (c6a) (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 133713 cycles 134203 cycles 1.00
ML-DSA-44 sign 520337 cycles 521698 cycles 1.00
ML-DSA-44 verify 146385 cycles 146340 cycles 1.00
ML-DSA-65 keypair 223659 cycles 224038 cycles 1.00
ML-DSA-65 sign 848662 cycles 849349 cycles 1.00
ML-DSA-65 verify 234304 cycles 234185 cycles 1.00
ML-DSA-87 keypair 372428 cycles 372086 cycles 1.00
ML-DSA-87 sign 1067554 cycles 1067081 cycles 1.00
ML-DSA-87 verify 383447 cycles 383108 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Intel Xeon 3rd gen (c6i)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 64069 cycles 63585 cycles 1.01
ML-DSA-44 sign 193224 cycles 191157 cycles 1.01
ML-DSA-44 verify 68417 cycles 67816 cycles 1.01
ML-DSA-65 keypair 112045 cycles 109881 cycles 1.02
ML-DSA-65 sign 319580 cycles 317055 cycles 1.01
ML-DSA-65 verify 112706 cycles 111442 cycles 1.01
ML-DSA-87 keypair 175547 cycles 174625 cycles 1.01
ML-DSA-87 sign 383108 cycles 382174 cycles 1.00
ML-DSA-87 verify 174085 cycles 171995 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton4

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 69123 cycles 68263 cycles 1.01
ML-DSA-44 sign 199769 cycles 198874 cycles 1.00
ML-DSA-44 verify 71127 cycles 70423 cycles 1.01
ML-DSA-65 keypair 121805 cycles 120576 cycles 1.01
ML-DSA-65 sign 327197 cycles 325926 cycles 1.00
ML-DSA-65 verify 118190 cycles 117081 cycles 1.01
ML-DSA-87 keypair 200984 cycles 198541 cycles 1.01
ML-DSA-87 sign 424819 cycles 422139 cycles 1.01
ML-DSA-87 verify 195690 cycles 193754 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Intel Xeon 3rd gen (c6i) (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 166378 cycles 162954 cycles 1.02
ML-DSA-44 sign 632780 cycles 603231 cycles 1.05
ML-DSA-44 verify 181608 cycles 176562 cycles 1.03
ML-DSA-65 keypair 282836 cycles 280116 cycles 1.01
ML-DSA-65 sign 1019955 cycles 1004251 cycles 1.02
ML-DSA-65 verify 291017 cycles 288681 cycles 1.01
ML-DSA-87 keypair 465001 cycles 461083 cycles 1.01
ML-DSA-87 sign 1282007 cycles 1261358 cycles 1.02
ML-DSA-87 verify 477910 cycles 472011 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Intel Xeon 3rd gen (c6i) (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 sign 632780 cycles 603231 cycles 1.05

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 217998 cycles 212818 cycles 1.02
ML-DSA-44 sign 586363 cycles 585644 cycles 1.00
ML-DSA-44 verify 215577 cycles 210872 cycles 1.02
ML-DSA-65 keypair 380800 cycles 374559 cycles 1.02
ML-DSA-65 sign 969275 cycles 963227 cycles 1.01
ML-DSA-65 verify 364200 cycles 356092 cycles 1.02
ML-DSA-87 keypair 634936 cycles 627779 cycles 1.01
ML-DSA-87 sign 1306788 cycles 1284883 cycles 1.02
ML-DSA-87 verify 613792 cycles 604963 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton4 (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 129813 cycles 129777 cycles 1.00
ML-DSA-44 sign 443836 cycles 443954 cycles 1.00
ML-DSA-44 verify 137766 cycles 137921 cycles 1.00
ML-DSA-65 keypair 226560 cycles 227397 cycles 1.00
ML-DSA-65 sign 718936 cycles 718178 cycles 1.00
ML-DSA-65 verify 223454 cycles 223025 cycles 1.00
ML-DSA-87 keypair 368959 cycles 369597 cycles 1.00
ML-DSA-87 sign 920189 cycles 923515 cycles 1.00
ML-DSA-87 verify 373710 cycles 374365 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton3

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 73183 cycles 72389 cycles 1.01
ML-DSA-44 sign 210532 cycles 209983 cycles 1.00
ML-DSA-44 verify 75625 cycles 74897 cycles 1.01
ML-DSA-65 keypair 128073 cycles 126804 cycles 1.01
ML-DSA-65 sign 346633 cycles 345365 cycles 1.00
ML-DSA-65 verify 125438 cycles 124178 cycles 1.01
ML-DSA-87 keypair 211014 cycles 208255 cycles 1.01
ML-DSA-87 sign 442074 cycles 439799 cycles 1.01
ML-DSA-87 verify 206718 cycles 204549 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 114877 cycles 113361 cycles 1.01
ML-DSA-44 sign 355897 cycles 354336 cycles 1.00
ML-DSA-44 verify 118377 cycles 117183 cycles 1.01
ML-DSA-65 keypair 198054 cycles 195639 cycles 1.01
ML-DSA-65 sign 585933 cycles 583519 cycles 1.00
ML-DSA-65 verify 195089 cycles 193013 cycles 1.01
ML-DSA-87 keypair 327364 cycles 322098 cycles 1.02
ML-DSA-87 sign 751346 cycles 747728 cycles 1.00
ML-DSA-87 verify 322586 cycles 317955 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton3 (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 140749 cycles 140593 cycles 1.00
ML-DSA-44 sign 490389 cycles 490206 cycles 1.00
ML-DSA-44 verify 151187 cycles 151231 cycles 1.00
ML-DSA-65 keypair 245960 cycles 247009 cycles 1.00
ML-DSA-65 sign 797884 cycles 797124 cycles 1.00
ML-DSA-65 verify 244710 cycles 244478 cycles 1.00
ML-DSA-87 keypair 400337 cycles 400701 cycles 1.00
ML-DSA-87 sign 1019955 cycles 1023123 cycles 1.00
ML-DSA-87 verify 407920 cycles 408100 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 212104 cycles 210881 cycles 1.01
ML-DSA-44 sign 756832 cycles 757389 cycles 1.00
ML-DSA-44 verify 227260 cycles 227314 cycles 1.00
ML-DSA-65 keypair 373182 cycles 373516 cycles 1.00
ML-DSA-65 sign 1239793 cycles 1240832 cycles 1.00
ML-DSA-65 verify 368073 cycles 368204 cycles 1.00
ML-DSA-87 keypair 596112 cycles 596691 cycles 1.00
ML-DSA-87 sign 1575818 cycles 1577536 cycles 1.00
ML-DSA-87 verify 612270 cycles 611322 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton2

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 115018 cycles 113699 cycles 1.01
ML-DSA-44 sign 355890 cycles 355159 cycles 1.00
ML-DSA-44 verify 118451 cycles 117670 cycles 1.01
ML-DSA-65 keypair 198048 cycles 195858 cycles 1.01
ML-DSA-65 sign 586435 cycles 584711 cycles 1.00
ML-DSA-65 verify 195389 cycles 193761 cycles 1.01
ML-DSA-87 keypair 327407 cycles 322508 cycles 1.02
ML-DSA-87 sign 752891 cycles 748267 cycles 1.01
ML-DSA-87 verify 322791 cycles 318343 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 292660 cycles 294579 cycles 0.99
ML-DSA-44 sign 1107185 cycles 1107977 cycles 1.00
ML-DSA-44 verify 321757 cycles 321951 cycles 1.00
ML-DSA-65 keypair 534023 cycles 532976 cycles 1.00
ML-DSA-65 sign 1817348 cycles 1821539 cycles 1.00
ML-DSA-65 verify 515871 cycles 513495 cycles 1.00
ML-DSA-87 keypair 826823 cycles 825142 cycles 1.00
ML-DSA-87 sign 2303000 cycles 2299984 cycles 1.00
ML-DSA-87 verify 853209 cycles 849960 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 26, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

Graviton2 (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 210778 cycles 211123 cycles 1.00
ML-DSA-44 sign 757941 cycles 758997 cycles 1.00
ML-DSA-44 verify 227547 cycles 228697 cycles 0.99
ML-DSA-65 keypair 374128 cycles 373852 cycles 1.00
ML-DSA-65 sign 1241981 cycles 1242331 cycles 1.00
ML-DSA-65 verify 368468 cycles 369416 cycles 1.00
ML-DSA-87 keypair 597150 cycles 598389 cycles 1.00
ML-DSA-87 sign 1600201 cycles 1597017 cycles 1.00
ML-DSA-87 verify 611858 cycles 610902 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 2134310 cycles 2134310 cycles 1
ML-DSA-44 sign 17791748 cycles 17791748 cycles 1
ML-DSA-44 verify 2398890 cycles 2398890 cycles 1
ML-DSA-65 keypair 3732866 cycles 3732866 cycles 1
ML-DSA-65 sign 15034558 cycles 15034558 cycles 1
ML-DSA-65 verify 4012806 cycles 4012806 cycles 1
ML-DSA-87 keypair 6516715 cycles 6516715 cycles 1
ML-DSA-87 sign 25055900 cycles 25055900 cycles 1
ML-DSA-87 verify 6865674 cycles 6865674 cycles 1

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 2332104 cycles 2332104 cycles 1
ML-DSA-44 sign 17791726 cycles 17791726 cycles 1
ML-DSA-44 verify 2398861 cycles 2398861 cycles 1
ML-DSA-65 keypair 4028005 cycles 4028005 cycles 1
ML-DSA-65 sign 15034565 cycles 15034565 cycles 1
ML-DSA-65 verify 4012799 cycles 4012799 cycles 1
ML-DSA-87 keypair 6896513 cycles 6896513 cycles 1
ML-DSA-87 sign 25049115 cycles 25049115 cycles 1
ML-DSA-87 verify 6864412 cycles 6864412 cycles 1

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A55 (Snapdragon 888) benchmarks (opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 278709 cycles 273499 cycles 1.02
ML-DSA-44 sign 825586 cycles 814069 cycles 1.01
ML-DSA-44 verify 278819 cycles 273539 cycles 1.02
ML-DSA-65 keypair 479230 cycles 468000 cycles 1.02
ML-DSA-65 sign 1350929 cycles 1346928 cycles 1.00
ML-DSA-65 verify 454546 cycles 450604 cycles 1.01
ML-DSA-87 keypair 810516 cycles 803503 cycles 1.01
ML-DSA-87 sign 1876308 cycles 1840553 cycles 1.02
ML-DSA-87 verify 798479 cycles 780369 cycles 1.02

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 26, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A55 (Snapdragon 888) benchmarks (no-opt)

Details
Benchmark suite Current: 115130b Previous: a754991 Ratio
ML-DSA-44 keypair 461492 cycles 461518 cycles 1.00
ML-DSA-44 sign 2123244 cycles 2124148 cycles 1.00
ML-DSA-44 verify 550769 cycles 550884 cycles 1.00
ML-DSA-65 keypair 774992 cycles 775080 cycles 1.00
ML-DSA-65 sign 3466005 cycles 3494577 cycles 0.99
ML-DSA-65 verify 856914 cycles 858414 cycles 1.00
ML-DSA-87 keypair 1254070 cycles 1249726 cycles 1.00
ML-DSA-87 sign 4348155 cycles 4289657 cycles 1.01
ML-DSA-87 verify 1372279 cycles 1370132 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

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

@github-actions github-actions[bot] github-actions[bot] left review comments
@oqs-bot oqs-bot oqs-bot left review comments

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

Assignees

No one assigned

Labels

benchmark needs-mlkem-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mkannwischer @oqs-bot