Skip to content

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

Open
mkannwischer wants to merge 1 commit into
mainfrom
port-sys-h
Open

sys.h: Do not depend on configuration options#1472
mkannwischer wants to merge 1 commit into
mainfrom
port-sys-h

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

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

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

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

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

 - Ports pq-code-package/mlkem-native#1938.
 - Resolves #1469.

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

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

@oqs-bot

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

@oqs-bot

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

@oqs-bot

oqs-bot commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 17, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

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

@mkannwischer
mkannwischer marked this pull request as ready for review October 19, 2026 09:18
@mkannwischer
mkannwischer requested a review from a team as a code owner October 19, 2026 09:18
@mkannwischer mkannwischer added this to the v2.1 milestone Oct 19, 2026

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

v2.1

Development

Successfully merging this pull request may close these issues.

Port: sys.h: Do not depend on configuration options

2 participants

@mkannwischer @oqs-bot