Skip to content

native: Pass chknorm bound to assembly as int64_t - #1445

Merged
mkannwischer merged 2 commits into
mainfrom
hol-light-chknorm-bound-low32
Oct 6, 2026
Merged

native: Pass chknorm bound to assembly as int64_t #1445
mkannwischer merged 2 commits into
mainfrom
hol-light-chknorm-bound-low32

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

The AArch64 and x86_64 poly_chknorm HOL-Light specs state
C_ARGUMENTS [a; word_zx bound], which constrains the full 64-bit bound
register. The C prototypes declared the bound as int32_t, for which
SysV and AAPCS64 leave the upper 32 bits unspecified, so the proofs did
not cover calls through the prototype. Declare the bound as int64_t and
require 0 <= B <= INT32_MAX in the contracts so that the prototype
matches the assembly and its specification.

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 133s 19s +600%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 40s 5s +700%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 168s 49s +243%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1216s 1364s -10.9%
caddq LP64 z3* ✅ 2s 6s -67%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
decompose LP64 z3* ✅ 1s 3s -67%
fqmul LP64 bitwuzla* ✅ 23s 39s -41%
fqscale LP64 bitwuzla* ✅ 2s 2s +0%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - 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* ✅ 1s 3s -67%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_finalize LP64 z3* ✅ 5s 2s +150%
keccak_init LP64 z3* ✅ 2s 3s -33%
keccak_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 3s 4s -25%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 2s 3s -33%
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* ✅ 3s 4s -25%
keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 22s -45%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 5s -40%
make_hint LP64 z3* ✅ 1s 3s -67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 133s 19s +600%
mld_check_pct LP64 z3* ✅ 5s 15s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 6s -67%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 3s -67%
ILP32 cvc5_arrays_exp ✅ 1s 3s -67%
ILP32 z3 ✅ 2s 3s -33%
LP64 bitwuzla ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 2s +50%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 4s -50%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 1s +100%
mld_ct_sel_int32 LP64 z3* ✅ 2s 3s -33%
mld_h LP64 z3* ✅ 3s 4s -25%
mld_invntt_layer LP64 bitwuzla* ✅ 61s 105s -42%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 6s 7s -14%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 4s -75%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 4s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 10s 23s -57%
mld_ntt_layer LP64 bitwuzla* ✅ 23s 41s -44%
mld_polymat_expand_entry LP64 z3* ✅ 3s 2s +50%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 3s +0%
mld_sample_s1_s2 LP64 z3* ✅ 2s 1s +100%
mld_sample_s1_s2_serial LP64 z3* ✅ 3s 4s -25%
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 3s -33%
mld_value_barrier_u32 LP64 z3* ✅ 2s 1s +100%
mld_value_barrier_u8 LP64 z3* ✅ 3s 4s -25%
montgomery_reduce LP64 z3* ✅ 4s 2s +100%
ntt_native_aarch64 LP64 z3* ✅ 1s 4s -75%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 4s -25%
pack_sig_c LP64 z3* ✅ 4s 5s -20%
pack_sig_h LP64 z3_no_bv_extract* ✅ 1s 4s -75%
pack_sig_z LP64 z3* ✅ 2s 2s +0%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 2s 5s -60%
pack_sk_s1 LP64 z3* ✅ 1s 3s -67%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 4s -25%
pointwise_native_aarch64 LP64 z3* ✅ 3s 2s +50%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 3s 4s -25%
poly_add LP64 z3* ✅ 3s 7s -57%
poly_caddq LP64 z3* ✅ 2s 4s -50%
poly_caddq_c LP64 z3* ✅ 4s 3s +33%
poly_caddq_native LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_caddq_native_x86_64 LP64 z3* ✅ 1s 4s -75%
poly_challenge LP64 z3* ✅ 3s 6s -50%
poly_chknorm LP64 z3* ✅ 3s 3s +0%
poly_chknorm_c LP64 z3* ✅ 6s 11s -45%
poly_chknorm_native LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_decompose LP64 z3* ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_decompose_c LP64 z3* ✅ 2s 5s -60%
poly_decompose_native LP64 z3* ✅ 1s 2s -50%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont LP64 z3* ✅ 3s 2s +50%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 11s -45%
poly_invntt_tomont_native LP64 z3* ✅ 3s 3s +0%
poly_ntt LP64 z3* ✅ 1s 3s -67%
poly_ntt_c LP64 z3_smt_only* ✅ 13s 21s -38%
poly_ntt_native LP64 z3* ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 3s 5s -40%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery_c LP64 z3* ✅ 65s 112s -42%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 2s +50%
poly_power2round LP64 z3* ✅ 4s 4s +0%
poly_reduce LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 z3* ✅ 2s 4s -50%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 3s 3s +0%
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* ✅ 3s 2s +50%
poly_use_hint_c LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 1s 3s -67%
polyeta_unpack LP64 z3* ✅ 9s 14s -36%
polyt0_pack LP64 z3* ✅ 3s 4s -25%
polyt0_unpack LP64 z3* ✅ 7s 12s -42%
polyt1_pack LP64 z3* ✅ 2s 3s -33%
polyt1_unpack LP64 z3* ✅ 1s 2s -50%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 2s 3s -33%
polyvec_matrix_expand_serial LP64 z3* ✅ 1s 4s -75%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 8s 6s +33%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 94s 149s -37%
polyveck_caddq LP64 z3* ✅ 4s 3s +33%
polyveck_chknorm LP64 z3* ✅ 3s 67s -96%
polyveck_decompose_pack_w1 LP64 z3* ✅ 5s - new
polyveck_invntt_tomont LP64 z3* ✅ 1s 5s -80%
polyveck_ntt LP64 z3* ✅ 2s 2s +0%
polyveck_pack_eta LP64 z3* ✅ 1s 4s -75%
polyveck_reduce LP64 z3* ✅ 3s 4s -25%
polyveck_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_chknorm LP64 z3* ✅ 2s 11s -82%
polyvecl_ntt LP64 z3* ✅ 3s 3s +0%
polyvecl_pack_eta LP64 z3* ✅ 1s 2s -50%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_uniform_gamma1 LP64 z3* ✅ 4s 2s +100%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_eta LP64 z3* ✅ 3s 4s -25%
polyvecl_unpack_z LP64 z3* ✅ 2s 3s -33%
polyw1_pack LP64 z3* ✅ 1s 4s -75%
polyw1_pack_32 LP64 z3* ✅ 3s 3s +0%
polyw1_pack_88 LP64 z3* ✅ 3s 2s +50%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 2s 2s +0%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 3s 2s +50%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 3s 4s -25%
polyz_unpack_c LP64 z3* ✅ 6s 8s -25%
polyz_unpack_native LP64 z3* ✅ 1s 3s -67%
polyz_unpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
power2round LP64 z3* ✅ 2s 2s +0%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_c LP64 bitwuzla* ✅ 3s 4s -25%
rej_eta_native LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform LP64 z3* ✅ 3s 8s -62%
rej_uniform_c LP64 z3* ✅ 7s 16s -56%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 4s 3s +33%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 1s - new
rej_uniform_native LP64 bitwuzla* ✅ 1s 5s -80%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 5s 3s +67%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 2s 3s -33%
shake128_finalize LP64 z3* ✅ 4s 3s +33%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 2s 2s +0%
shake128_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
shake256 LP64 z3* ✅ 3s 1s +200%
shake256_absorb LP64 z3* ✅ 2s 2s +0%
shake256_finalize LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 z3* ✅ 2s 4s -50%
shake256_release LP64 z3* ✅ 1s 1s +0%
shake256_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 1s +100%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
sig_unpack_hints LP64 z3* ✅ 11s 2s +450%
sign_keypair LP64 z3* ✅ 5s 5s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 14s 4s +250%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 40s 5s +700%
sign_signature LP64 z3* ✅ 2s 6s -67%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 13s 4s +225%
sign_signature_pre_hash_internal LP64 z3* ✅ 2s 4s -50%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 4s 4s +0%
sign_verify LP64 z3* ✅ 3s 4s -25%
sign_verify_extmu LP64 z3* ✅ 2s 5s -60%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 168s 49s +243%
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* ✅ 1s 1s +0%
sys_check_capability LP64 z3* ✅ 2s 2s +0%
unpack_pk_t1 LP64 z3* ✅ 1s 3s -67%
unpack_sk LP64 z3* ✅ 2s 3s -33%
unpack_sk_s1hat LP64 z3* ✅ 3s 3s +0%
unpack_sk_s2hat LP64 z3* ✅ 1s 4s -75%
unpack_sk_t0hat LP64 z3* ✅ 2s 2s +0%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 3s 3s +0%
yvec_init LP64 z3* ✅ 1s 1s +0%

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 35s 7s +400%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 118s 31s +281%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 26s 3s +767%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 59s 5s +1080%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 193s 71s +172%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1358s 1482s -8.4%
caddq LP64 z3* ✅ 2s 2s +0%
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* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 4s 2s +100%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 z3* ✅ 1s 4s -75%
keccak_absorb LP64 z3* ✅ 3s 3s +0%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 10s -50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
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* ✅ 1s 2s -50%
keccak_finalize LP64 z3* ✅ 1s 2s -50%
keccak_init LP64 z3* ✅ 2s 4s -50%
keccak_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 3s -67%
keccakf1600_permute LP64 z3* ✅ 2s 4s -50%
keccakf1600_permute_native LP64 z3* ✅ 3s 2s +50%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_permute LP64 z3* ✅ 1s 1s +0%
keccakf1600x4_permute_native LP64 z3* ✅ 11s 22s -50%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 2s +50%
make_hint LP64 z3* ✅ 1s 3s -67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 118s 31s +281%
mld_check_pct LP64 z3* ✅ 5s 12s -58%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 5s 5s +0%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 6s -83%
ILP32 cvc5_arrays_exp ✅ 1s 6s -83%
ILP32 z3 ✅ 1s 6s -83%
LP64 bitwuzla ✅ 1s 6s -83%
LP64 cvc5_arrays_exp ✅ 1s 6s -83%
LP64 z3* ✅ 2s 6s -67%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 4s 3s +33%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 2s +50%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 1s 1s +0%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 4s -75%
mld_ct_memcmp LP64 bitwuzla* ✅ 3s 4s -25%
mld_ct_sel_int32 LP64 z3* ✅ 1s 2s -50%
mld_h LP64 z3* ✅ 2s 3s -33%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 108s -46%
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* ✅ 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 25s -52%
mld_ntt_layer LP64 bitwuzla* ✅ 21s 43s -51%
mld_polymat_expand_entry LP64 z3* ✅ 2s 3s -33%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 2s 4s -50%
mld_sample_s1_s2 LP64 z3* ✅ 4s 6s -33%
mld_sample_s1_s2_serial LP64 z3* ✅ 2s 3s -33%
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* ✅ 4s 2s +100%
mld_value_barrier_u32 LP64 z3* ✅ 3s 4s -25%
mld_value_barrier_u8 LP64 z3* ✅ 2s 1s +100%
montgomery_reduce LP64 z3* ✅ 1s 1s +0%
ntt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 5s -60%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
pack_sig_c LP64 z3* ✅ 2s 3s -33%
pack_sig_h LP64 z3_no_bv_extract* ✅ 1s 2s -50%
pack_sig_z LP64 z3* ✅ 2s 1s +100%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 3s 2s +50%
pack_sk_s1 LP64 z3* ✅ 1s 3s -67%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 2s 6s -67%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 2s 5s -60%
pointwise_native_aarch64 LP64 z3* ✅ 1s 3s -67%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_add LP64 z3* ✅ 2s 7s -71%
poly_caddq LP64 z3* ✅ 1s 3s -67%
poly_caddq_c LP64 z3* ✅ 3s 5s -40%
poly_caddq_native LP64 z3* ✅ 2s 4s -50%
poly_caddq_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 1s +100%
poly_challenge LP64 z3* ✅ 2s 5s -60%
poly_chknorm LP64 z3* ✅ 2s 3s -33%
poly_chknorm_c LP64 z3* ✅ 7s 13s -46%
poly_chknorm_native LP64 z3* ✅ 3s 4s -25%
poly_chknorm_native_aarch64 LP64 z3* ✅ 4s 2s +100%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 4s -75%
poly_decompose LP64 z3* ✅ 4s 2s +100%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 5s 2s +150%
poly_decompose_c LP64 z3* ✅ 4s 8s -50%
poly_decompose_native LP64 z3* ✅ 2s 5s -60%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont LP64 z3* ✅ 1s 5s -80%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 10s -40%
poly_invntt_tomont_native LP64 z3* ✅ 2s 5s -60%
poly_ntt LP64 z3* ✅ 2s 2s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 22s -55%
poly_ntt_native LP64 z3* ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery LP64 z3* ✅ 4s 2s +100%
poly_pointwise_montgomery_c LP64 z3* ✅ 69s 116s -41%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 4s -75%
poly_power2round LP64 z3* ✅ 4s 7s -43%
poly_reduce LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 z3* ✅ 1s 3s -67%
poly_sub LP64 z3* ✅ 3s 4s -25%
poly_uniform LP64 z3* ✅ 1s 2s -50%
poly_uniform_4x LP64 z3* ✅ 5s 4s +25%
poly_uniform_eta LP64 z3* ✅ 3s 5s -40%
poly_uniform_eta_4x LP64 z3* ✅ 6s 13s -54%
poly_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 3s -33%
poly_use_hint LP64 z3* ✅ 3s 3s +0%
poly_use_hint_c LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native LP64 z3* ✅ 2s 7s -71%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_use_hint_native_x86_64 LP64 z3* ✅ 7s - new
polyeta_pack LP64 z3* ✅ 2s 1s +100%
polyeta_unpack LP64 z3* ✅ 4s 4s +0%
polyt0_pack LP64 z3* ✅ 3s 5s -40%
polyt0_unpack LP64 z3* ✅ 6s 13s -54%
polyt1_pack LP64 z3* ✅ 1s 3s -67%
polyt1_unpack LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 2s 6s -67%
polyvec_matrix_expand_serial LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 8s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 169s 201s -16%
polyveck_caddq LP64 z3* ✅ 5s 7s -29%
polyveck_chknorm LP64 z3* ✅ 7s 36s -81%
polyveck_decompose_pack_w1 LP64 z3* ✅ 8s - new
polyveck_invntt_tomont LP64 z3* ✅ 2s 7s -71%
polyveck_ntt LP64 z3* ✅ 2s 4s -50%
polyveck_pack_eta LP64 z3* ✅ 3s 3s +0%
polyveck_reduce LP64 z3* ✅ 5s 6s -17%
polyveck_unpack_eta LP64 z3* ✅ 4s 3s +33%
polyvecl_chknorm LP64 z3* ✅ 6s 43s -86%
polyvecl_ntt LP64 z3* ✅ 6s 7s -14%
polyvecl_pack_eta LP64 z3* ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 1s 1s +0%
polyvecl_unpack_eta LP64 z3* ✅ 1s 2s -50%
polyvecl_unpack_z LP64 z3* ✅ 2s 1s +100%
polyw1_pack LP64 z3* ✅ 1s 3s -67%
polyw1_pack_32 LP64 z3* ✅ 2s 2s +0%
polyw1_pack_88 LP64 z3* ✅ 2s 3s -33%
polyw1_unpack LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 z3* ✅ 4s - new
polyw1_unpack_88 LP64 z3* ✅ 3s - new
polyz_pack LP64 z3* ✅ 2s 3s -33%
polyz_unpack LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 4s 2s +100%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 4s 5s -20%
polyz_unpack_c LP64 z3* ✅ 3s 9s -67%
polyz_unpack_native LP64 z3* ✅ 2s 3s -33%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 2s 2s +0%
reduce32 LP64 z3* ✅ 1s 2s -50%
rej_eta LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_c LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_native LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform LP64 z3* ✅ 4s 7s -43%
rej_uniform_c LP64 z3* ✅ 7s 16s -56%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 5s -60%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 5s 4s +25%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 5s -60%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 4s 2s +100%
shake128_finalize LP64 z3* ✅ 1s 2s -50%
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* ✅ 1s 4s -75%
shake256_finalize LP64 z3* ✅ 2s 1s +100%
shake256_init LP64 z3* ✅ 3s 4s -25%
shake256_release LP64 z3* ✅ 2s 3s -33%
shake256_squeeze LP64 bitwuzla* ✅ 4s 4s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
sig_unpack_hints LP64 z3* ✅ 11s 1s +1000%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 26s 3s +767%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 59s 5s +1080%
sign_signature LP64 z3* ✅ 2s 5s -60%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 12s 6s +100%
sign_signature_pre_hash_internal LP64 z3* ✅ 4s 3s +33%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 7s -29%
sign_verify LP64 z3* ✅ 2s 6s -67%
sign_verify_extmu LP64 z3* ✅ 4s 2s +100%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 193s 71s +172%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 5s -40%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 6s -33%
sk_s1hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 1s 1s +0%
sk_t0hat_get_poly LP64 z3* ✅ 2s 1s +100%
sys_check_capability LP64 z3* ✅ 3s 1s +200%
unpack_pk_t1 LP64 z3* ✅ 2s 2s +0%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 z3* ✅ 3s 1s +200%
unpack_sk_s2hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_t0hat LP64 z3* ✅ 1s 4s -75%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 1s 5s -80%

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 129s 34s +279%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 35s 6s +483%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 74s 6s +1133%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 194s 47s +313%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1327s 1436s -7.6%
caddq LP64 z3* ✅ 2s 3s -33%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
decompose LP64 z3* ✅ 3s 2s +50%
fqmul LP64 bitwuzla* ✅ 23s 39s -41%
fqscale LP64 bitwuzla* ✅ 1s 1s +0%
intt_native_aarch64 LP64 z3* ✅ 3s 4s -25%
intt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 1s 4s -75%
keccak_absorb LP64 z3* ✅ 3s 4s -25%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 8s -25%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 1s +100%
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 2s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 3s -67%
keccak_finalize LP64 z3* ✅ 3s 1s +200%
keccak_init LP64 z3* ✅ 4s 1s +300%
keccak_squeeze LP64 bitwuzla* ✅ 2s 5s -60%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 25s -52%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
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* ⚠️ 129s 34s +279%
mld_check_pct LP64 z3* ✅ 7s 15s -53%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 6s -67%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 1s +0%
ILP32 cvc5_arrays_exp ✅ 1s 1s +0%
ILP32 z3 ✅ 2s 1s +100%
LP64 bitwuzla ✅ 3s 1s +200%
LP64 cvc5_arrays_exp ✅ 2s 1s +100%
LP64 z3* ✅ 2s 1s +100%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 1s 5s -80%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 2s -50%
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 3s -67%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 1s +0%
mld_ct_sel_int32 LP64 z3* ✅ 1s 2s -50%
mld_h LP64 z3* ✅ 3s 2s +50%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 111s -48%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 1s +100%
mld_keccakf1600_permute_c LP64 z3* ✅ 5s 8s -38%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 3s -33%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 1s +100%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 23s -52%
mld_ntt_layer LP64 bitwuzla* ✅ 23s 44s -48%
mld_polymat_expand_entry LP64 z3* ✅ 1s 4s -75%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 4s 3s +33%
mld_sample_s1_s2 LP64 z3* ✅ 5s 8s -38%
mld_sample_s1_s2_serial LP64 z3* ✅ 3s 6s -50%
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* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 2s 3s -33%
mld_value_barrier_u8 LP64 z3* ✅ 1s 2s -50%
montgomery_reduce LP64 z3* ✅ 1s 2s -50%
ntt_native_aarch64 LP64 z3* ✅ 3s 4s -25%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 6s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
pack_sig_c LP64 z3* ✅ 3s 2s +50%
pack_sig_h LP64 z3_no_bv_extract* ✅ 3s 3s +0%
pack_sig_z LP64 z3* ✅ 2s 3s -33%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 1s 2s -50%
pack_sk_s1 LP64 z3* ✅ 1s 2s -50%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 6s 5s +20%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 5s 8s -38%
pointwise_native_aarch64 LP64 z3* ✅ 3s 4s -25%
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* ✅ 1s 5s -80%
poly_add LP64 z3* ✅ 3s 8s -62%
poly_caddq LP64 z3* ✅ 3s 5s -40%
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* ✅ 3s 3s +0%
poly_challenge LP64 z3* ✅ 4s 4s +0%
poly_chknorm LP64 z3* ✅ 3s 4s -25%
poly_chknorm_c LP64 z3* ✅ 7s 13s -46%
poly_chknorm_native LP64 z3* ✅ 2s 1s +100%
poly_chknorm_native_aarch64 LP64 z3* ✅ 1s 5s -80%
poly_chknorm_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_decompose LP64 z3* ✅ 2s 2s +0%
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* ✅ 6s 6s +0%
poly_decompose_native LP64 z3* ✅ 4s 2s +100%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_invntt_tomont LP64 z3* ✅ 2s 4s -50%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 5s 9s -44%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_ntt LP64 z3* ✅ 5s 2s +150%
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 3s -67%
poly_pointwise_montgomery LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery_c LP64 z3* ✅ 64s 125s -49%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 3s -67%
poly_power2round LP64 z3* ✅ 6s 7s -14%
poly_reduce LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 z3* ✅ 2s 4s -50%
poly_sub LP64 z3* ✅ 1s 5s -80%
poly_uniform LP64 z3* ✅ 1s 4s -75%
poly_uniform_4x LP64 z3* ✅ 1s 3s -67%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
poly_uniform_eta_4x LP64 z3* ✅ 9s 12s -25%
poly_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 3s -33%
poly_use_hint LP64 z3* ✅ 6s 4s +50%
poly_use_hint_c LP64 z3* ✅ 1s 4s -75%
poly_use_hint_native LP64 z3* ✅ 1s 1s +0%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 6s 13s -54%
polyt0_pack LP64 z3* ✅ 3s 3s +0%
polyt0_unpack LP64 z3* ✅ 8s 14s -43%
polyt1_pack LP64 z3* ✅ 1s 5s -80%
polyt1_unpack LP64 z3* ✅ 4s 3s +33%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 2s 3s -33%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 5s 13s -62%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 117s 196s -40%
polyveck_caddq LP64 z3* ✅ 4s 8s -50%
polyveck_chknorm LP64 z3* ✅ 3s 9s -67%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 2s 4s -50%
polyveck_ntt LP64 z3* ✅ 1s 3s -67%
polyveck_pack_eta LP64 z3* ✅ 2s 5s -60%
polyveck_reduce LP64 z3* ✅ 6s 6s +0%
polyveck_unpack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_chknorm LP64 z3* ✅ 2s 38s -95%
polyvecl_ntt LP64 z3* ✅ 4s 8s -50%
polyvecl_pack_eta LP64 z3* ✅ 4s 2s +100%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 4s 2s +100%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_eta LP64 z3* ✅ 1s 3s -67%
polyvecl_unpack_z LP64 z3* ✅ 2s 3s -33%
polyw1_pack LP64 z3* ✅ 3s 2s +50%
polyw1_pack_32 LP64 z3* ✅ 4s 3s +33%
polyw1_pack_88 LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 z3* ✅ 4s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 1s 4s -75%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 3s 5s -40%
polyz_unpack_c LP64 z3* ✅ 4s 7s -43%
polyz_unpack_native LP64 z3* ✅ 2s 1s +100%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 1s 3s -67%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 4s 2s +100%
rej_eta_c LP64 bitwuzla* ✅ 1s 4s -75%
rej_eta_native LP64 bitwuzla* ✅ 3s 4s -25%
rej_uniform LP64 z3* ✅ 3s 7s -57%
rej_uniform_c LP64 z3* ✅ 8s 18s -56%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 1s - new
rej_uniform_native LP64 bitwuzla* ✅ 3s 5s -40%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 3s 2s +50%
shake128_init LP64 z3* ✅ 1s 2s -50%
shake128_release LP64 z3* ✅ 2s 3s -33%
shake128_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 4s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
shake256 LP64 z3* ✅ 3s 3s +0%
shake256_absorb LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 z3* ✅ 1s 3s -67%
shake256_init LP64 z3* ✅ 1s 3s -67%
shake256_release LP64 z3* ✅ 1s 5s -80%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 5s -60%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 4s -50%
sig_unpack_hints LP64 z3* ✅ 13s 4s +225%
sign_keypair LP64 z3* ✅ 5s 4s +25%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 35s 6s +483%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 74s 6s +1133%
sign_signature LP64 z3* ✅ 4s 4s +0%
sign_signature_extmu LP64 z3* ✅ 4s 4s +0%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 13s 3s +333%
sign_signature_pre_hash_internal LP64 z3* ✅ 5s 2s +150%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 3s +67%
sign_verify LP64 z3* ✅ 2s 2s +0%
sign_verify_extmu LP64 z3* ✅ 2s 4s -50%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 194s 47s +313%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 3s 7s -57%
sk_s1hat_get_poly LP64 z3* ✅ 1s 3s -67%
sk_s2hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 z3* ✅ 1s 3s -67%
sys_check_capability LP64 z3* ✅ 2s 2s +0%
unpack_pk_t1 LP64 z3* ✅ 2s 2s +0%
unpack_sk LP64 z3* ✅ 1s 4s -75%
unpack_sk_s1hat LP64 z3* ✅ 1s 3s -67%
unpack_sk_s2hat LP64 z3* ✅ 3s 3s +0%
unpack_sk_t0hat LP64 z3* ✅ 1s 4s -75%
use_hint LP64 z3* ✅ 2s 3s -33%
yvec_get_poly LP64 z3* ✅ 1s 2s -50%
yvec_init LP64 z3* ✅ 1s 4s -75%

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 103s 50s +106%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 148s 58s +155%
polyveck_chknorm LP64 z3* ⚠️ 63s 5s +1160%
sig_unpack_hints LP64 z3* ⚠️ 20s 2s +900%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 37s 5s +640%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 117s 26s +350%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 305s 114s +168%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1694s 1514s +11.9%
caddq LP64 z3* ✅ 1s 2s -50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 103s 50s +106%
decompose LP64 z3* ✅ 2s 2s +0%
fqmul LP64 bitwuzla* ✅ 24s 39s -38%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
intt_native_aarch64 LP64 z3* ✅ 2s 9s -78%
intt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 z3* ✅ 4s 4s +0%
keccak_absorb LP64 z3* ✅ 4s 5s -20%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 9s -44%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 3s -33%
keccak_finalize LP64 z3* ✅ 1s 3s -67%
keccak_init LP64 z3* ✅ 2s 3s -33%
keccak_squeeze LP64 bitwuzla* ✅ 2s 1s +100%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 4s 1s +300%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_permute LP64 z3* ✅ 3s 4s -25%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 22s -45%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
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* ⚠️ 148s 58s +155%
mld_check_pct LP64 z3* ✅ 6s 14s -57%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 5s 7s -29%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 3s 2s +50%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 2s 2s +0%
LP64 bitwuzla ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 3s 2s +50%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 3s 3s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 3s 2s +50%
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* ✅ 4s 1s +300%
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* ✅ 64s 107s -40%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 2s 8s -75%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 13s 23s -43%
mld_ntt_layer LP64 bitwuzla* ✅ 23s 42s -45%
mld_polymat_expand_entry LP64 z3* ✅ 3s 3s +0%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 1s 4s -75%
mld_sample_s1_s2 LP64 z3* ✅ 1s 4s -75%
mld_sample_s1_s2_serial LP64 z3* ✅ 3s 3s +0%
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u8 LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 z3* ✅ 2s 3s -33%
ntt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 5s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 1s +200%
pack_sig_c LP64 z3* ✅ 1s 2s -50%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 3s -33%
pack_sig_z LP64 z3* ✅ 2s 4s -50%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 2s 3s -33%
pack_sk_s1 LP64 z3* ✅ 2s 2s +0%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 4s -25%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 7s -57%
pointwise_native_aarch64 LP64 z3* ✅ 2s 5s -60%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_add LP64 z3* ✅ 4s 7s -43%
poly_caddq LP64 z3* ✅ 4s 2s +100%
poly_caddq_c LP64 z3* ✅ 2s 2s +0%
poly_caddq_native LP64 z3* ✅ 2s 5s -60%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_caddq_native_x86_64 LP64 z3* ✅ 1s 4s -75%
poly_challenge LP64 z3* ✅ 1s 3s -67%
poly_chknorm LP64 z3* ✅ 1s 4s -75%
poly_chknorm_c LP64 z3* ✅ 7s 17s -59%
poly_chknorm_native LP64 z3* ✅ 3s 4s -25%
poly_chknorm_native_aarch64 LP64 z3* ✅ 3s 4s -25%
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* ✅ 2s 4s -50%
poly_decompose_native LP64 z3* ✅ 2s 3s -33%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 3s -33%
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* ✅ 5s 4s +25%
poly_ntt LP64 z3* ✅ 2s 3s -33%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 19s -47%
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* ✅ 4s 4s +0%
poly_pointwise_montgomery LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery_c LP64 z3* ✅ 48s 114s -58%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 2s +0%
poly_power2round LP64 z3* ✅ 2s 4s -50%
poly_reduce LP64 z3* ✅ 2s 3s -33%
poly_shiftl LP64 z3* ✅ 1s 3s -67%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 3s 6s -50%
poly_uniform_4x LP64 z3* ✅ 8s 14s -43%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
poly_uniform_eta_4x LP64 z3* ✅ 8s 11s -27%
poly_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 5s -80%
poly_use_hint LP64 z3* ✅ 4s 4s +0%
poly_use_hint_c LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native LP64 z3* ✅ 2s 4s -50%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 1s 3s -67%
polyeta_unpack LP64 z3* ✅ 7s 14s -50%
polyt0_pack LP64 z3* ✅ 4s 2s +100%
polyt0_unpack LP64 z3* ✅ 6s 15s -60%
polyt1_pack LP64 z3* ✅ 1s 4s -75%
polyt1_unpack LP64 z3* ✅ 3s 5s -40%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 17s 28s -39%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 8s -75%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 2s 2s +0%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 13s 15s -13%
polyveck_caddq LP64 z3* ✅ 3s 3s +0%
polyveck_chknorm LP64 z3* ⚠️ 63s 5s +1160%
polyveck_decompose_pack_w1 LP64 z3* ✅ 3s - new
polyveck_invntt_tomont LP64 z3* ✅ 3s 5s -40%
polyveck_ntt LP64 z3* ✅ 3s 5s -40%
polyveck_pack_eta LP64 z3* ✅ 3s 2s +50%
polyveck_reduce LP64 z3* ✅ 1s 5s -80%
polyveck_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_chknorm LP64 z3* ✅ 4s 10s -60%
polyvecl_ntt LP64 z3* ✅ 2s 2s +0%
polyvecl_pack_eta LP64 z3* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 4s -75%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 154s 131s +18%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 2s +50%
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 3s 2s +50%
polyw1_pack LP64 z3* ✅ 3s 3s +0%
polyw1_pack_32 LP64 z3* ✅ 2s 2s +0%
polyw1_pack_88 LP64 z3* ✅ 3s 1s +200%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 5s - new
polyw1_unpack_88 LP64 z3* ✅ 1s - new
polyz_pack LP64 z3* ✅ 1s 2s -50%
polyz_unpack LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 1s 5s -80%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 5s -60%
polyz_unpack_c LP64 z3* ✅ 6s 11s -45%
polyz_unpack_native LP64 z3* ✅ 1s 2s -50%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 1s 3s -67%
reduce32 LP64 z3* ✅ 2s 2s +0%
rej_eta LP64 bitwuzla* ✅ 1s 3s -67%
rej_eta_c LP64 bitwuzla* ✅ 3s 4s -25%
rej_eta_native LP64 bitwuzla* ✅ 3s 6s -50%
rej_uniform LP64 z3* ✅ 13s 18s -28%
rej_uniform_c LP64 z3* ✅ 10s 15s -33%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
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* ✅ 2s 5s -60%
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 3s -33%
shake128_release LP64 z3* ✅ 1s 1s +0%
shake128_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
shake256 LP64 z3* ✅ 1s 1s +0%
shake256_absorb LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 z3* ✅ 3s 2s +50%
shake256_init LP64 z3* ✅ 3s 3s +0%
shake256_release LP64 z3* ✅ 1s 2s -50%
shake256_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 3s 4s -25%
sig_unpack_hints LP64 z3* ⚠️ 20s 2s +900%
sign_keypair LP64 z3* ✅ 3s 4s -25%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 16s 4s +300%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 37s 5s +640%
sign_signature LP64 z3* ✅ 3s 3s +0%
sign_signature_extmu LP64 z3* ✅ 4s 4s +0%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 117s 26s +350%
sign_signature_pre_hash_internal LP64 z3* ✅ 4s 6s -33%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 3s +67%
sign_verify LP64 z3* ✅ 5s 4s +25%
sign_verify_extmu LP64 z3* ✅ 3s 3s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 305s 114s +168%
sign_verify_pre_hash_internal LP64 z3* ✅ 2s 3s -33%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 5s -20%
sk_s1hat_get_poly LP64 z3* ✅ 3s 3s +0%
sk_s2hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 z3* ✅ 2s 2s +0%
sys_check_capability LP64 z3* ✅ 2s 4s -50%
unpack_pk_t1 LP64 z3* ✅ 2s 5s -60%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 z3* ✅ 2s 1s +100%
unpack_sk_s2hat LP64 z3* ✅ 2s 4s -50%
unpack_sk_t0hat LP64 z3* ✅ 2s 3s -33%
use_hint LP64 z3* ✅ 3s 2s +50%
yvec_get_poly LP64 z3* ✅ 1s 3s -67%
yvec_init LP64 z3* ✅ 3s 3s +0%

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 132s 13s +915%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 208s 63s +230%
sig_unpack_hints LP64 z3* ⚠️ 29s 2s +1350%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 27s 5s +440%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 53s 6s +783%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 185s 55s +236%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 413s 177s +133%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2065s 1784s +15.8%
caddq LP64 z3* ✅ 4s 3s +33%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 132s 13s +915%
decompose LP64 z3* ✅ 1s 1s +0%
fqmul LP64 bitwuzla* ✅ 24s 40s -40%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 1s 3s -67%
intt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 3s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 4s 3s +33%
keccak_absorb LP64 z3* ✅ 3s 3s +0%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 8s -12%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 4s -75%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_finalize LP64 z3* ✅ 1s 2s -50%
keccak_init LP64 z3* ✅ 2s 1s +100%
keccak_squeeze LP64 bitwuzla* ✅ 1s 4s -75%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 5s -40%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 3s 3s +0%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 2s -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* ✅ 2s 4s -50%
keccakf1600x4_permute LP64 z3* ✅ 3s 4s -25%
keccakf1600x4_permute_native LP64 z3* ✅ 13s 23s -43%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 5s 1s +400%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 3s -33%
make_hint LP64 z3* ✅ 1s 2s -50%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 208s 63s +230%
mld_check_pct LP64 z3* ✅ 4s 14s -71%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 7s -43%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 2s -50%
ILP32 cvc5_arrays_exp ✅ 4s 2s +100%
ILP32 z3 ✅ 4s 2s +100%
LP64 bitwuzla ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 3s 2s +50%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 3s 4s -25%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 3s 3s +0%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 4s 2s +100%
mld_ct_memcmp LP64 bitwuzla* ✅ 5s 2s +150%
mld_ct_sel_int32 LP64 z3* ✅ 1s 3s -67%
mld_h LP64 z3* ✅ 3s 2s +50%
mld_invntt_layer LP64 bitwuzla* ✅ 64s 109s -41%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 1s +100%
mld_keccakf1600_permute_c LP64 z3* ✅ 3s 6s -50%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 3s -67%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 24s -54%
mld_ntt_layer LP64 bitwuzla* ✅ 26s 41s -37%
mld_polymat_expand_entry LP64 z3* ✅ 1s 4s -75%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 2s +50%
mld_sample_s1_s2 LP64 z3* ✅ 4s 6s -33%
mld_sample_s1_s2_serial LP64 z3* ✅ 2s 4s -50%
mld_sign_attempt LP64 z3* ✅ 4s - new
mld_sign_finish LP64 z3* ✅ 1s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 3s 2s +50%
mld_value_barrier_u32 LP64 z3* ✅ 4s 3s +33%
mld_value_barrier_u8 LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 z3* ✅ 3s 4s -25%
ntt_native_aarch64 LP64 z3* ✅ 3s 2s +50%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
pack_sig_c LP64 z3* ✅ 1s 5s -80%
pack_sig_h LP64 z3_no_bv_extract* ✅ 1s 5s -80%
pack_sig_z LP64 z3* ✅ 2s 2s +0%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 2s 2s +0%
pack_sk_s1 LP64 z3* ✅ 2s 5s -60%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 6s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 2s 8s -75%
pointwise_native_aarch64 LP64 z3* ✅ 2s 5s -60%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 4s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_add LP64 z3* ✅ 3s 9s -67%
poly_caddq LP64 z3* ✅ 3s 2s +50%
poly_caddq_c LP64 z3* ✅ 3s 2s +50%
poly_caddq_native LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_challenge LP64 z3* ✅ 2s 6s -67%
poly_chknorm LP64 z3* ✅ 1s 4s -75%
poly_chknorm_c LP64 z3* ✅ 7s 15s -53%
poly_chknorm_native LP64 z3* ✅ 1s 2s -50%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_decompose LP64 z3* ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 2s 1s +100%
poly_decompose_c LP64 z3* ✅ 3s 5s -40%
poly_decompose_native LP64 z3* ✅ 5s 3s +67%
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* ✅ 8s 11s -27%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_ntt LP64 z3* ✅ 3s 2s +50%
poly_ntt_c LP64 z3_smt_only* ✅ 9s 19s -53%
poly_ntt_native LP64 z3* ✅ 2s 4s -50%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 1s 2s -50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 4s -50%
poly_pointwise_montgomery LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery_c LP64 z3* ✅ 46s 125s -63%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 3s -33%
poly_power2round LP64 z3* ✅ 3s 4s -25%
poly_reduce LP64 z3* ✅ 3s 3s +0%
poly_shiftl LP64 z3* ✅ 3s 3s +0%
poly_sub LP64 z3* ✅ 6s 3s +100%
poly_uniform LP64 z3* ✅ 2s 4s -50%
poly_uniform_4x LP64 z3* ✅ 7s 13s -46%
poly_uniform_eta LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta_4x LP64 z3* ✅ 6s 14s -57%
poly_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 4s -50%
poly_use_hint LP64 z3* ✅ 2s 3s -33%
poly_use_hint_c LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 2s 3s -33%
polyeta_unpack LP64 z3* ✅ 3s 8s -62%
polyt0_pack LP64 z3* ✅ 2s 3s -33%
polyt0_unpack LP64 z3* ✅ 7s 16s -56%
polyt1_pack LP64 z3* ✅ 3s 3s +0%
polyt1_unpack LP64 z3* ✅ 1s 5s -80%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 69s 110s -37%
polyvec_matrix_expand_serial LP64 z3* ✅ 13s 27s -52%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 3s 1s +200%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 12s 18s -33%
polyveck_caddq LP64 z3* ✅ 6s 6s +0%
polyveck_chknorm LP64 z3* ✅ 3s 6s -50%
polyveck_decompose_pack_w1 LP64 z3* ✅ 4s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 8s -50%
polyveck_ntt LP64 z3* ✅ 6s 7s -14%
polyveck_pack_eta LP64 z3* ✅ 3s 4s -25%
polyveck_reduce LP64 z3* ✅ 3s 4s -25%
polyveck_unpack_eta LP64 z3* ✅ 2s 6s -67%
polyvecl_chknorm LP64 z3* ✅ 2s 7s -71%
polyvecl_ntt LP64 z3* ✅ 4s 4s +0%
polyvecl_pack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 183s 210s -13%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 3s 2s +50%
polyvecl_uniform_gamma1 LP64 z3* ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 1s 3s -67%
polyvecl_unpack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_unpack_z LP64 z3* ✅ 2s 3s -33%
polyw1_pack LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 z3* ✅ 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* ✅ 1s - new
polyz_pack LP64 z3* ✅ 3s 3s +0%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 3s -33%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 3s -33%
polyz_unpack_c LP64 z3* ✅ 2s 13s -85%
polyz_unpack_native LP64 z3* ✅ 3s 4s -25%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 2s 1s +100%
reduce32 LP64 z3* ✅ 4s 3s +33%
rej_eta LP64 bitwuzla* ✅ 3s 2s +50%
rej_eta_c LP64 bitwuzla* ✅ 3s 5s -40%
rej_eta_native LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform LP64 z3* ✅ 11s 18s -39%
rej_uniform_c LP64 z3* ✅ 12s 14s -14%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 4s -25%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 5s 4s +25%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 4s 3s +33%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 3s 2s +50%
shake128_finalize LP64 z3* ✅ 3s 1s +200%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 2s 3s -33%
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* ✅ 1s 2s -50%
shake256_finalize LP64 z3* ✅ 3s 1s +200%
shake256_init LP64 z3* ✅ 2s 2s +0%
shake256_release LP64 z3* ✅ 3s 2s +50%
shake256_squeeze LP64 bitwuzla* ✅ 3s 3s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
sig_unpack_hints LP64 z3* ⚠️ 29s 2s +1350%
sign_keypair LP64 z3* ✅ 6s 3s +100%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 27s 5s +440%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 53s 6s +783%
sign_signature LP64 z3* ✅ 4s 6s -33%
sign_signature_extmu LP64 z3* ✅ 2s 2s +0%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 185s 55s +236%
sign_signature_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 2s 3s -33%
sign_verify LP64 z3* ✅ 3s 3s +0%
sign_verify_extmu LP64 z3* ✅ 5s 3s +67%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 413s 177s +133%
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* ✅ 1s 6s -83%
sk_s2hat_get_poly LP64 z3* ✅ 4s 2s +100%
sk_t0hat_get_poly LP64 z3* ✅ 3s 2s +50%
sys_check_capability LP64 z3* ✅ 2s 4s -50%
unpack_pk_t1 LP64 z3* ✅ 1s 5s -80%
unpack_sk LP64 z3* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 z3* ✅ 3s 2s +50%
unpack_sk_s2hat LP64 z3* ✅ 2s 4s -50%
unpack_sk_t0hat LP64 z3* ✅ 3s 5s -40%
use_hint LP64 z3* ✅ 3s 2s +50%
yvec_get_poly LP64 z3* ✅ 4s 3s +33%
yvec_init LP64 z3* ✅ 1s 3s -67%

@oqs-bot

oqs-bot commented Sep 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

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

@mkannwischer
mkannwischer marked this pull request as ready for review September 26, 2026 04:41
@mkannwischer
mkannwischer requested a review from a team as a code owner September 26, 2026 04:41
hanno-becker
hanno-becker requested changes Oct 5, 2026
View reviewed changes

@hanno-becker hanno-becker left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why don't we pass the argument in 64-bit instead, as in pq-code-package/mlkem-native#1926?

@mkannwischer
mkannwischer force-pushed the hol-light-chknorm-bound-low32 branch from e94fb52 to 39200d2 Compare October 5, 2026 09:59
@mkannwischer mkannwischer changed the title HOL-Light: Constrain only the low 32 bits of the chknorm bound native: Pass chknorm bound to assembly as int64_t Oct 5, 2026
@mkannwischer

mkannwischer commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

Why don't we pass the argument in 64-bit instead, as in pq-code-package/mlkem-native#1926?

That indeed is easier. Changed.

hanno-becker
hanno-becker requested changes Oct 6, 2026
View reviewed changes

@hanno-becker hanno-becker left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the HOL-Light spec we have

let MLDSA_POLY_CHKNORM_SUBROUTINE_CORRECT = prove(
 `!a (x:num->int32) (bound:int32) pc returnaddress.
        nonoverlapping (word pc, LENGTH mldsa_poly_chknorm_mc) (a, 1024)
        ==> ensures arm
             (\s. aligned_bytes_loaded s (word pc) mldsa_poly_chknorm_mc /\
                  read PC s = word pc /\
                  read X30 s = returnaddress /\
                  C_ARGUMENTS [a; word_zx bound] s /\
                  (!i. i < 256 ==>
                     read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                  (!i. i < 256 ==> abs(ival(x i)) < &2 pow 31))
             (\s. read PC s = returnaddress /\
                  read X0 s = word(bitval(?i. i < 256 /\ abs(ival(x i)) >= ival bound)))
             (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI)`,

There is no functional mistake here, but the use of int32 and word_zx here is still suggestive of a reliance of upper 32-bits of 32-bit arguments being cleared.

I'd suggest to switch this to int64 to have a closer alignment between the HOL and C parameters.

@mkannwischer
native: Pass chknorm bound to assembly as int64_t
d6395b5 
The AArch64 and x86_64 poly_chknorm HOL-Light specs state
C_ARGUMENTS [a; word_zx bound], which constrains the full 64-bit bound
register. The C prototypes declared the bound as int32_t, for which
SysV and AAPCS64 leave the upper 32 bits unspecified, so the proofs did
not cover calls through the prototype. Declare the bound as int64_t and
require 0 <= B <= INT32_MAX in the contracts so that the prototype
matches the assembly and its specification.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
HOL-Light: Take chknorm bound as int64 in specs
a1c60c9 
The AArch64 and x86_64 poly_chknorm specifications took the bound as
int32 and stated C_ARGUMENTS [a; word_zx bound], which suggests a
reliance on the upper 32 bits of a 32-bit argument being cleared.
Since the C prototype now passes the bound as int64_t, state the specs
over an int64 bound with C_ARGUMENTS [a; bound] and require
0 <= ival bound < 2^31, matching the CBMC contract 0 <= B <= INT32_MAX.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
mkannwischer force-pushed the hol-light-chknorm-bound-low32 branch from 39200d2 to a1c60c9 Compare October 6, 2026 05:24
@mkannwischer

mkannwischer commented Oct 6, 2026

Copy link
Copy Markdown
Contributor Author

In the HOL-Light spec we have

let MLDSA_POLY_CHKNORM_SUBROUTINE_CORRECT = prove(
 `!a (x:num->int32) (bound:int32) pc returnaddress.
        nonoverlapping (word pc, LENGTH mldsa_poly_chknorm_mc) (a, 1024)
        ==> ensures arm
             (\s. aligned_bytes_loaded s (word pc) mldsa_poly_chknorm_mc /\
                  read PC s = word pc /\
                  read X30 s = returnaddress /\
                  C_ARGUMENTS [a; word_zx bound] s /\
                  (!i. i < 256 ==>
                     read(memory :> bytes32(word_add a (word(4 * i)))) s = x i) /\
                  (!i. i < 256 ==> abs(ival(x i)) < &2 pow 31))
             (\s. read PC s = returnaddress /\
                  read X0 s = word(bitval(?i. i < 256 /\ abs(ival(x i)) >= ival bound)))
             (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI)`,

There is no functional mistake here, but the use of int32 and word_zx here is still suggestive of a reliance of upper 32-bits of 32-bit arguments being cleared.

I'd suggest to switch this to int64 to have a closer alignment between the HOL and C parameters.

Yes that's cleaner. I've changed it.

hanno-becker
hanno-becker reviewed Oct 6, 2026
View reviewed changes
Comment thread dev/aarch64_clean/src/arith_native_aarch64.h
hanno-becker
hanno-becker approved these changes Oct 6, 2026
View reviewed changes

@hanno-becker hanno-becker left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @mkannwischer!

@mkannwischer
mkannwischer enabled auto-merge October 6, 2026 09:22
@mkannwischer
mkannwischer added this pull request to the merge queue Oct 6, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Oct 6, 2026
@mkannwischer
mkannwischer added this pull request to the merge queue Oct 6, 2026
Merged via the queue into main with commit 48c075a Oct 6, 2026
445 checks passed
@mkannwischer
mkannwischer deleted the hol-light-chknorm-bound-low32 branch October 6, 2026 16:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkannwischer @oqs-bot @hanno-becker