Skip to content

CI: Run reduced CBMC configuration on pull requests - #1554

Draft
mkannwischer wants to merge 1 commit into
mainfrom
ci-cbmc-pr-default-only
Draft

CI: Run reduced CBMC configuration on pull requests#1554
mkannwischer wants to merge 1 commit into
mainfrom
ci-cbmc-pr-default-only

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Nov 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Pull requests now run CBMC only for the default (data model, solver) configuration of each proof and skip the REDUCE_RAM variants. The merge queue, manual dispatches and pull requests labeled cbmc still run all supported configurations for all six jobs. Adding the cbmc label to an open pull request triggers the full run.

The CBMC jobs no longer run functional tests, which other CI jobs already cover, and superseded pull request runs of the CI workflow are cancelled.

@mkannwischer
CI: Run reduced CBMC configuration on pull requests
d1d1c7f 
Pull requests now run CBMC only for the default (data model, solver)
configuration of each proof and skip the REDUCE_RAM variants. The merge
queue, manual dispatches and pull requests labeled `cbmc` still run all
supported configurations for all six jobs. Adding the `cbmc` label to
an open pull request triggers the full run.

The CBMC jobs no longer run functional tests, which other CI jobs
already cover, and superseded pull request runs of the CI workflow are
cancelled.

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

oqs-bot commented Nov 15, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

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

@oqs-bot

oqs-bot commented Nov 15, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

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

@mkannwischer mkannwischer mentioned this pull request Nov 15, 2026
Open
@oqs-bot

oqs-bot commented Nov 15, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

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

@hanno-becker hanno-becker mentioned this pull request Nov 15, 2026
Draft

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

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Reduce EC2 CI cost

2 participants

@mkannwischer @oqs-bot