Skip to content

Make the alignment configurable - #1379

Open
mkannwischer wants to merge 1 commit into
mainfrom
configurable-alignment
Open

Make the alignment configurable#1379
mkannwischer wants to merge 1 commit into
mainfrom
configurable-alignment

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

Add two experimental config options: MLD_CONFIG_ALIGN sets the alignment of large buffers and structures in bytes, MLD_CONFIG_ALIGN_ATTRIBUTE replaces the declarator prefix for compilers whose spelling mldsa-native does not know. MLD_DEFAULT_ALIGN, MLD_ALIGN and MLD_ALIGN_UP derive from them.

The x86_64 and AArch64 backends reject an alignment below what their load and store instructions require.

MLD_TOTAL_ALLOC_* is measured for the default alignment, so it is no longer defined once the alignment is customized, and the allocation test skips itself in that case.

@mkannwischer
mkannwischer force-pushed the configurable-alignment branch from 8c86285 to b64cbd8 Compare August 11, 2026 05:37
@oqs-bot

oqs-bot commented Aug 11, 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* ⚠️ 30s 7s +329%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 106s 31s +242%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 24s 3s +700%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 56s 5s +1020%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 184s 71s +159%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1286s 1482s -13.2%
caddq LP64 z3* ✅ 4s 2s +100%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 7s +329%
decompose LP64 z3* ✅ 3s 4s -25%
fqmul LP64 bitwuzla* ✅ 23s 40s -43%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 4s - new
intt_native_x86_64 LP64 z3* ✅ 1s 4s -75%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
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* ✅ 3s 3s +0%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_finalize LP64 z3* ✅ 2s 2s +0%
keccak_init LP64 z3* ✅ 2s 4s -50%
keccak_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute LP64 z3* ✅ 1s 4s -75%
keccakf1600_permute_native LP64 z3* ✅ 1s 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* ✅ 2s 4s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 4s 1s +300%
keccakf1600x4_permute LP64 z3* ✅ 3s 1s +200%
keccakf1600x4_permute_native LP64 z3* ✅ 14s 22s -36%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
make_hint LP64 z3* ✅ 2s 3s -33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 106s 31s +242%
mld_check_pct LP64 z3* ✅ 6s 12s -50%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 3s 5s -40%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 6s -67%
ILP32 cvc5_arrays_exp ✅ 2s 6s -67%
ILP32 z3 ✅ 1s 6s -83%
LP64 bitwuzla ✅ 1s 6s -83%
LP64 cvc5_arrays_exp ✅ 4s 6s -33%
LP64 z3* ✅ 1s 6s -83%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 1s 3s -67%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 2s +50%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 1s +100%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 5s 3s +67%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 4s -75%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 4s -50%
mld_ct_sel_int32 LP64 z3* ✅ 1s 2s -50%
mld_h LP64 z3* ✅ 1s 3s -67%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 108s -46%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 4s 7s -43%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 4s 2s +100%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 25s -56%
mld_ntt_layer LP64 bitwuzla* ✅ 20s 43s -53%
mld_polymat_expand_entry LP64 z3* ✅ 1s 3s -67%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 1s 4s -75%
mld_sample_s1_s2 LP64 z3* ✅ 1s 6s -83%
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* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 3s 4s -25%
mld_value_barrier_u8 LP64 z3* ✅ 1s 1s +0%
montgomery_reduce LP64 z3* ✅ 2s 1s +100%
ntt_native_aarch64 LP64 z3* ✅ 1s 3s -67%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 3s 5s -40%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
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_s2 LP64 z3* ✅ 1s 2s -50%
pack_sk_s1 LP64 z3* ✅ 4s 3s +33%
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* ✅ 2s 3s -33%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - 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* ✅ 3s 7s -57%
poly_caddq LP64 z3* ✅ 1s 3s -67%
poly_caddq_c LP64 z3* ✅ 2s 5s -60%
poly_caddq_native LP64 z3* ✅ 3s 4s -25%
poly_caddq_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 5s 1s +400%
poly_challenge LP64 z3* ✅ 1s 5s -80%
poly_chknorm LP64 z3* ✅ 2s 3s -33%
poly_chknorm_c LP64 z3* ✅ 6s 13s -54%
poly_chknorm_native LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_decompose LP64 z3* ✅ 5s 2s +150%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 3s 4s -25%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_decompose_c LP64 z3* ✅ 6s 8s -25%
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* ✅ 1s 5s -80%
poly_ntt LP64 z3* ✅ 2s 2s +0%
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* ✅ 1s 3s -67%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery LP64 z3* ✅ 4s 2s +100%
poly_pointwise_montgomery_c LP64 z3* ✅ 64s 116s -45%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 4s -75%
poly_power2round LP64 z3* ✅ 2s 7s -71%
poly_reduce LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 z3* ✅ 2s 3s -33%
poly_sub LP64 z3* ✅ 2s 4s -50%
poly_uniform LP64 z3* ✅ 2s 2s +0%
poly_uniform_4x LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta LP64 z3* ✅ 3s 5s -40%
poly_uniform_eta_4x LP64 z3* ✅ 8s 13s -38%
poly_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 3s -33%
poly_use_hint LP64 z3* ✅ 1s 3s -67%
poly_use_hint_c LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native LP64 z3* ✅ 3s 7s -57%
poly_use_hint_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 2s 1s +100%
polyeta_unpack LP64 z3* ✅ 3s 4s -25%
polyt0_pack LP64 z3* ✅ 3s 5s -40%
polyt0_unpack LP64 z3* ✅ 8s 13s -38%
polyt1_pack LP64 z3* ✅ 1s 3s -67%
polyt1_unpack LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 2s 6s -67%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 8s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 158s 201s -21%
polyveck_caddq LP64 z3* ✅ 3s 7s -57%
polyveck_chknorm LP64 z3* ✅ 5s 36s -86%
polyveck_decompose_pack_w1 LP64 z3* ✅ 5s - new
polyveck_invntt_tomont LP64 z3* ✅ 2s 7s -71%
polyveck_ntt LP64 z3* ✅ 3s 4s -25%
polyveck_pack_eta LP64 z3* ✅ 1s 3s -67%
polyveck_reduce LP64 z3* ✅ 6s 6s +0%
polyveck_unpack_eta LP64 z3* ✅ 1s 3s -67%
polyvecl_chknorm LP64 z3* ✅ 4s 43s -91%
polyvecl_ntt LP64 z3* ✅ 3s 7s -57%
polyvecl_pack_eta LP64 z3* ✅ 2s 2s +0%
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* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 1s 4s -75%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 1s +100%
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 1s 1s +0%
polyw1_pack LP64 z3* ✅ 1s 3s -67%
polyw1_pack_32 LP64 z3* ✅ 1s 2s -50%
polyw1_pack_88 LP64 z3* ✅ 2s 3s -33%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 5s - new
polyw1_unpack_88 LP64 z3* ✅ 3s - new
polyz_pack LP64 z3* ✅ 3s 3s +0%
polyz_unpack LP64 z3* ✅ 4s 3s +33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 1s 2s -50%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 3s 5s -40%
polyz_unpack_c LP64 z3* ✅ 7s 9s -22%
polyz_unpack_native LP64 z3* ✅ 1s 3s -67%
polyz_unpack_native_x86_64 LP64 z3* ✅ 4s 3s +33%
power2round LP64 z3* ✅ 1s 2s -50%
reduce32 LP64 z3* ✅ 3s 2s +50%
rej_eta LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_c LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_native LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform LP64 z3* ✅ 3s 7s -57%
rej_uniform_c LP64 z3* ✅ 8s 16s -50%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 4s 5s -20%
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* ✅ 2s 5s -60%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 9s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 1s 2s -50%
shake128_init LP64 z3* ✅ 1s 6s -83%
shake128_release LP64 z3* ✅ 2s 2s +0%
shake128_squeeze LP64 bitwuzla* ✅ 3s 3s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
shake256 LP64 z3* ✅ 1s 2s -50%
shake256_absorb LP64 z3* ✅ 3s 4s -25%
shake256_finalize LP64 z3* ✅ 1s 1s +0%
shake256_init LP64 z3* ✅ 1s 4s -75%
shake256_release LP64 z3* ✅ 2s 3s -33%
shake256_squeeze LP64 bitwuzla* ✅ 4s 4s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
sig_unpack_hints LP64 z3* ✅ 10s 1s +900%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 24s 3s +700%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 56s 5s +1020%
sign_signature LP64 z3* ✅ 6s 5s +20%
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* ✅ 3s 3s +0%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 7s -29%
sign_verify LP64 z3* ✅ 3s 6s -50%
sign_verify_extmu LP64 z3* ✅ 4s 2s +100%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 184s 71s +159%
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* ✅ 1s 3s -67%
sk_s2hat_get_poly LP64 z3* ✅ 1s 1s +0%
sk_t0hat_get_poly LP64 z3* ✅ 2s 1s +100%
sys_check_capability LP64 z3* ✅ 2s 1s +100%
unpack_pk_t1 LP64 z3* ✅ 1s 2s -50%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 z3* ✅ 3s 1s +200%
unpack_sk_s2hat LP64 z3* ✅ 1s 3s -67%
unpack_sk_t0hat LP64 z3* ✅ 2s 4s -50%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 1s 3s -67%
yvec_init LP64 z3* ✅ 4s 5s -20%

@oqs-bot

oqs-bot commented Aug 11, 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* ⚠️ 39s 12s +225%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 183s 19s +863%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 60s 5s +1100%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 226s 49s +361%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1578s 1364s +15.7%
caddq LP64 z3* ✅ 3s 6s -50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 39s 12s +225%
decompose LP64 z3* ✅ 2s 3s -33%
fqmul LP64 bitwuzla* ✅ 32s 39s -18%
fqscale LP64 bitwuzla* ✅ 2s 2s +0%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
intt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 4s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
keccak_absorb LP64 z3* ✅ 4s 3s +33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 8s -38%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 4s 2s +100%
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* ✅ 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* ✅ 1s 4s -75%
keccakf1600_permute LP64 z3* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 6s -83%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
keccakf1600x4_permute_native LP64 z3* ✅ 16s 22s -27%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 5s -60%
make_hint LP64 z3* ✅ 3s 3s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 183s 19s +863%
mld_check_pct LP64 z3* ✅ 8s 15s -47%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 6s -67%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 3s 3s +0%
ILP32 cvc5_arrays_exp ✅ 2s 3s -33%
ILP32 z3 ✅ 3s 3s +0%
LP64 bitwuzla ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 1s 3s -67%
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* ✅ 2s 2s +0%
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* ✅ 3s 4s -25%
mld_invntt_layer LP64 bitwuzla* ✅ 83s 105s -21%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 5s 7s -29%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 4s -50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 4s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 15s 23s -35%
mld_ntt_layer LP64 bitwuzla* ✅ 38s 41s -7%
mld_polymat_expand_entry LP64 z3* ✅ 4s 2s +100%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 2s 3s -33%
mld_sample_s1_s2 LP64 z3* ✅ 2s 1s +100%
mld_sample_s1_s2_serial LP64 z3* ✅ 1s 4s -75%
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* ✅ 2s 3s -33%
mld_value_barrier_u32 LP64 z3* ✅ 1s 1s +0%
mld_value_barrier_u8 LP64 z3* ✅ 2s 4s -50%
montgomery_reduce LP64 z3* ✅ 2s 2s +0%
ntt_native_aarch64 LP64 z3* ✅ 3s 4s -25%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 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* ✅ 3s 4s -25%
pack_sig_z LP64 z3* ✅ 1s 2s -50%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 2s 5s -60%
pack_sk_s1 LP64 z3* ✅ 2s 3s -33%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 5s 6s -17%
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* ✅ 2s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 z3* ✅ 3s 4s -25%
poly_add LP64 z3* ✅ 6s 7s -14%
poly_caddq LP64 z3* ✅ 1s 4s -75%
poly_caddq_c LP64 z3* ✅ 5s 3s +67%
poly_caddq_native LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_caddq_native_x86_64 LP64 z3* ✅ 3s 4s -25%
poly_challenge LP64 z3* ✅ 1s 6s -83%
poly_chknorm LP64 z3* ✅ 2s 3s -33%
poly_chknorm_c LP64 z3* ✅ 10s 11s -9%
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 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* ✅ 3s 3s +0%
poly_decompose_c LP64 z3* ✅ 4s 5s -20%
poly_decompose_native LP64 z3* ✅ 4s 2s +100%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 9s 11s -18%
poly_invntt_tomont_native LP64 z3* ✅ 5s 3s +67%
poly_ntt LP64 z3* ✅ 4s 3s +33%
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* ✅ 4s 3s +33%
poly_pointwise_montgomery_c LP64 z3* ✅ 103s 112s -8%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 2s +0%
poly_power2round LP64 z3* ✅ 5s 4s +25%
poly_reduce LP64 z3* ✅ 4s 4s +0%
poly_shiftl LP64 z3* ✅ 2s 4s -50%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 2s 3s -33%
poly_uniform_4x LP64 z3* ✅ 3s 3s +0%
poly_uniform_eta LP64 z3* ✅ 2s 2s +0%
poly_uniform_eta_4x LP64 z3* ✅ 9s 12s -25%
poly_uniform_gamma1 LP64 z3* ✅ 4s 3s +33%
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 5s -80%
poly_use_hint LP64 z3* ✅ 2s 2s +0%
poly_use_hint_c LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 5s - new
polyeta_pack LP64 z3* ✅ 2s 3s -33%
polyeta_unpack LP64 z3* ✅ 9s 14s -36%
polyt0_pack LP64 z3* ✅ 5s 4s +25%
polyt0_unpack LP64 z3* ✅ 11s 12s -8%
polyt1_pack LP64 z3* ✅ 3s 3s +0%
polyt1_unpack LP64 z3* ✅ 4s 2s +100%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 3s -67%
polyvec_matrix_expand_serial LP64 z3* ✅ 1s 4s -75%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 7s 6s +17%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 125s 149s -16%
polyveck_caddq LP64 z3* ✅ 4s 3s +33%
polyveck_chknorm LP64 z3* ✅ 3s 67s -96%
polyveck_decompose_pack_w1 LP64 z3* ✅ 4s - new
polyveck_invntt_tomont LP64 z3* ✅ 3s 5s -40%
polyveck_ntt LP64 z3* ✅ 2s 2s +0%
polyveck_pack_eta LP64 z3* ✅ 4s 4s +0%
polyveck_reduce LP64 z3* ✅ 3s 4s -25%
polyveck_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_chknorm LP64 z3* ✅ 3s 11s -73%
polyvecl_ntt LP64 z3* ✅ 2s 3s -33%
polyvecl_pack_eta LP64 z3* ✅ 4s 2s +100%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 3s 4s -25%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 5s 2s +150%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 1s 2s -50%
polyvecl_unpack_eta LP64 z3* ✅ 4s 4s +0%
polyvecl_unpack_z LP64 z3* ✅ 1s 3s -67%
polyw1_pack LP64 z3* ✅ 1s 4s -75%
polyw1_pack_32 LP64 z3* ✅ 3s 3s +0%
polyw1_pack_88 LP64 z3* ✅ 4s 2s +100%
polyw1_unpack LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - 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 2s +0%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_c LP64 z3* ✅ 9s 8s +12%
polyz_unpack_native LP64 z3* ✅ 3s 3s +0%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 2s 2s +0%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_c LP64 bitwuzla* ✅ 3s 4s -25%
rej_eta_native LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform LP64 z3* ✅ 6s 8s -25%
rej_uniform_c LP64 z3* ✅ 11s 16s -31%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 4s 5s -20%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 10s - new
shake128_absorb LP64 z3* ✅ 4s 3s +33%
shake128_finalize LP64 z3* ✅ 2s 3s -33%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 2s 2s +0%
shake128_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 4s 2s +100%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
shake256 LP64 z3* ✅ 2s 1s +100%
shake256_absorb LP64 z3* ✅ 3s 2s +50%
shake256_finalize LP64 z3* ✅ 2s 2s +0%
shake256_init LP64 z3* ✅ 2s 4s -50%
shake256_release LP64 z3* ✅ 2s 1s +100%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 1s +100%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
sig_unpack_hints LP64 z3* ✅ 19s 2s +850%
sign_keypair LP64 z3* ✅ 6s 5s +20%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 18s 4s +350%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 60s 5s +1100%
sign_signature LP64 z3* ✅ 7s 6s +17%
sign_signature_extmu LP64 z3* ✅ 4s 4s +0%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 15s 4s +275%
sign_signature_pre_hash_internal LP64 z3* ✅ 3s 4s -25%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 6s 4s +50%
sign_verify LP64 z3* ✅ 2s 4s -50%
sign_verify_extmu LP64 z3* ✅ 4s 5s -20%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 226s 49s +361%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 5s -40%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 5s -20%
sk_s1hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_s2hat_get_poly LP64 z3* ✅ 2s 5s -60%
sk_t0hat_get_poly LP64 z3* ✅ 2s 1s +100%
sys_check_capability LP64 z3* ✅ 4s 2s +100%
unpack_pk_t1 LP64 z3* ✅ 1s 3s -67%
unpack_sk LP64 z3* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_s2hat LP64 z3* ✅ 2s 4s -50%
unpack_sk_t0hat LP64 z3* ✅ 3s 2s +50%
use_hint LP64 z3* ✅ 3s 2s +50%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 3s 1s +200%

@oqs-bot

oqs-bot commented Aug 11, 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* ⚠️ 89s 50s +78%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 131s 58s +126%
polyveck_chknorm LP64 z3* ⚠️ 51s 5s +920%
sig_unpack_hints LP64 z3* ⚠️ 20s 2s +900%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 36s 5s +620%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 100s 26s +285%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 260s 114s +128%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1552s 1514s +2.5%
caddq LP64 z3* ✅ 3s 2s +50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 89s 50s +78%
decompose LP64 z3* ✅ 3s 2s +50%
fqmul LP64 bitwuzla* ✅ 22s 39s -44%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 2s 9s -78%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 4s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 z3* ✅ 4s 5s -20%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 9s -56%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 3s -33%
keccak_finalize LP64 z3* ✅ 2s 3s -33%
keccak_init LP64 z3* ✅ 3s 3s +0%
keccak_squeeze LP64 bitwuzla* ✅ 2s 1s +100%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute LP64 z3* ✅ 3s 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 4s -75%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 3s 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* ✅ 1s 2s -50%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 3s -67%
make_hint LP64 z3* ✅ 1s 3s -67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 131s 58s +126%
mld_check_pct LP64 z3* ✅ 6s 14s -57%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 6s 7s -14%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 2s +0%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 1s 2s -50%
LP64 bitwuzla ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 4s 2s +100%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 3s 4s -25%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 2s 1s +100%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 1s +100%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_sel_int32 LP64 z3* ✅ 2s 2s +0%
mld_h LP64 z3* ✅ 1s 4s -75%
mld_invntt_layer LP64 bitwuzla* ✅ 54s 107s -50%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600_permute_c LP64 z3* ✅ 5s 8s -38%
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* ✅ 12s 23s -48%
mld_ntt_layer LP64 bitwuzla* ✅ 22s 42s -48%
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* ✅ 2s 4s -50%
mld_sample_s1_s2_serial LP64 z3* ✅ 4s 3s +33%
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* ✅ 3s 3s +0%
montgomery_reduce LP64 z3* ✅ 2s 3s -33%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 1s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 1s +200%
pack_sig_c LP64 z3* ✅ 2s 2s +0%
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* ✅ 1s 2s -50%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 4s +0%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 2s 7s -71%
pointwise_native_aarch64 LP64 z3* ✅ 4s 5s -20%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 1s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - 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 2s +0%
poly_caddq_c LP64 z3* ✅ 2s 2s +0%
poly_caddq_native LP64 z3* ✅ 2s 5s -60%
poly_caddq_native_aarch64 LP64 z3* ✅ 4s 4s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_challenge LP64 z3* ✅ 2s 3s -33%
poly_chknorm LP64 z3* ✅ 1s 4s -75%
poly_chknorm_c LP64 z3* ✅ 5s 17s -71%
poly_chknorm_native LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 z3* ✅ 3s 3s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 3s 4s -25%
poly_decompose_c LP64 z3* ✅ 1s 4s -75%
poly_decompose_native LP64 z3* ✅ 3s 3s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_invntt_tomont LP64 z3* ✅ 1s 4s -75%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 8s 11s -27%
poly_invntt_tomont_native LP64 z3* ✅ 3s 4s -25%
poly_ntt LP64 z3* ✅ 2s 3s -33%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 19s -47%
poly_ntt_native LP64 z3* ✅ 2s 5s -60%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 3s 4s -25%
poly_pointwise_montgomery LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery_c LP64 z3* ✅ 44s 114s -61%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 2s +0%
poly_power2round LP64 z3* ✅ 1s 4s -75%
poly_reduce LP64 z3* ✅ 2s 3s -33%
poly_shiftl LP64 z3* ✅ 2s 3s -33%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 2s 6s -67%
poly_uniform_4x LP64 z3* ✅ 6s 14s -57%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
poly_uniform_eta_4x LP64 z3* ✅ 7s 11s -36%
poly_uniform_gamma1 LP64 z3* ✅ 1s 4s -75%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 5s -60%
poly_use_hint LP64 z3* ✅ 2s 4s -50%
poly_use_hint_c LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native LP64 z3* ✅ 3s 4s -25%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 2s 3s -33%
polyeta_unpack LP64 z3* ✅ 5s 14s -64%
polyt0_pack LP64 z3* ✅ 1s 2s -50%
polyt0_unpack LP64 z3* ✅ 8s 15s -47%
polyt1_pack LP64 z3* ✅ 2s 4s -50%
polyt1_unpack LP64 z3* ✅ 3s 5s -40%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 16s 28s -43%
polyvec_matrix_expand_serial LP64 z3* ✅ 3s 8s -62%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 1s 2s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 12s 15s -20%
polyveck_caddq LP64 z3* ✅ 2s 3s -33%
polyveck_chknorm LP64 z3* ⚠️ 51s 5s +920%
polyveck_decompose_pack_w1 LP64 z3* ✅ 3s - new
polyveck_invntt_tomont LP64 z3* ✅ 1s 5s -80%
polyveck_ntt LP64 z3* ✅ 3s 5s -40%
polyveck_pack_eta LP64 z3* ✅ 2s 2s +0%
polyveck_reduce LP64 z3* ✅ 1s 5s -80%
polyveck_unpack_eta LP64 z3* ✅ 3s 2s +50%
polyvecl_chknorm LP64 z3* ✅ 2s 10s -80%
polyvecl_ntt LP64 z3* ✅ 2s 2s +0%
polyvecl_pack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 140s 131s +7%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 4s 2s +100%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 2s +50%
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 3s 2s +50%
polyw1_pack LP64 z3* ✅ 1s 3s -67%
polyw1_pack_32 LP64 z3* ✅ 3s 2s +50%
polyw1_pack_88 LP64 z3* ✅ 3s 1s +200%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 3s - new
polyz_pack LP64 z3* ✅ 1s 2s -50%
polyz_unpack LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 4s 5s -20%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 1s 5s -80%
polyz_unpack_c LP64 z3* ✅ 4s 11s -64%
polyz_unpack_native LP64 z3* ✅ 2s 2s +0%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 3s 3s +0%
reduce32 LP64 z3* ✅ 2s 2s +0%
rej_eta LP64 bitwuzla* ✅ 1s 3s -67%
rej_eta_c LP64 bitwuzla* ✅ 5s 4s +25%
rej_eta_native LP64 bitwuzla* ✅ 3s 6s -50%
rej_uniform LP64 z3* ✅ 10s 18s -44%
rej_uniform_c LP64 z3* ✅ 9s 15s -40%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 1s - 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* ✅ 6s - new
shake128_absorb LP64 z3* ✅ 3s 2s +50%
shake128_finalize LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 z3* ✅ 3s 3s +0%
shake128_release LP64 z3* ✅ 4s 1s +300%
shake128_squeeze LP64 bitwuzla* ✅ 2s 1s +100%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 1s +0%
shake256 LP64 z3* ✅ 1s 1s +0%
shake256_absorb LP64 z3* ✅ 3s 3s +0%
shake256_finalize LP64 z3* ✅ 2s 2s +0%
shake256_init LP64 z3* ✅ 4s 3s +33%
shake256_release LP64 z3* ✅ 2s 2s +0%
shake256_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 4s -50%
sig_unpack_hints LP64 z3* ⚠️ 20s 2s +900%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 14s 4s +250%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 36s 5s +620%
sign_signature LP64 z3* ✅ 4s 3s +33%
sign_signature_extmu LP64 z3* ✅ 2s 4s -50%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 100s 26s +285%
sign_signature_pre_hash_internal LP64 z3* ✅ 2s 6s -67%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 3s +67%
sign_verify LP64 z3* ✅ 4s 4s +0%
sign_verify_extmu LP64 z3* ✅ 2s 3s -33%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 260s 114s +128%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 3s 5s -40%
sk_s1hat_get_poly LP64 z3* ✅ 5s 3s +67%
sk_s2hat_get_poly LP64 z3* ✅ 2s 2s +0%
sk_t0hat_get_poly LP64 z3* ✅ 1s 2s -50%
sys_check_capability LP64 z3* ✅ 2s 4s -50%
unpack_pk_t1 LP64 z3* ✅ 1s 5s -80%
unpack_sk LP64 z3* ✅ 2s 3s -33%
unpack_sk_s1hat LP64 z3* ✅ 3s 1s +200%
unpack_sk_s2hat LP64 z3* ✅ 3s 4s -25%
unpack_sk_t0hat LP64 z3* ✅ 3s 3s +0%
use_hint LP64 z3* ✅ 4s 2s +100%
yvec_get_poly LP64 z3* ✅ 4s 3s +33%
yvec_init LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Aug 11, 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* ⚠️ 31s 12s +158%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 137s 34s +303%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 34s 6s +467%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 82s 6s +1267%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 200s 47s +326%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1360s 1436s -5.3%
caddq LP64 z3* ✅ 1s 3s -67%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 31s 12s +158%
decompose LP64 z3* ✅ 3s 2s +50%
fqmul LP64 bitwuzla* ✅ 23s 39s -41%
fqscale LP64 bitwuzla* ✅ 2s 1s +100%
intt_native_aarch64 LP64 z3* ✅ 2s 4s -50%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 1s 4s -75%
keccak_absorb LP64 z3* ✅ 5s 4s +25%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 8s -38%
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* ✅ 3s 1s +200%
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* ✅ 2s 3s -33%
keccak_finalize LP64 z3* ✅ 2s 1s +100%
keccak_init LP64 z3* ✅ 1s 1s +0%
keccak_squeeze LP64 bitwuzla* ✅ 2s 5s -60%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
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* ⚠️ 137s 34s +303%
mld_check_pct LP64 z3* ✅ 3s 15s -80%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 6s -67%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 4s 1s +300%
ILP32 cvc5_arrays_exp ✅ 2s 1s +100%
ILP32 z3 ✅ 1s 1s +0%
LP64 bitwuzla ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3* ✅ 3s 1s +200%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 3s 5s -40%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 4s 2s +100%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 2s +0%
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* ✅ 3s 1s +200%
mld_ct_sel_int32 LP64 z3* ✅ 3s 2s +50%
mld_h LP64 z3* ✅ 4s 2s +100%
mld_invntt_layer LP64 bitwuzla* ✅ 60s 111s -46%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 4s 1s +300%
mld_keccakf1600_permute_c LP64 z3* ✅ 3s 8s -62%
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* ✅ 21s 44s -52%
mld_polymat_expand_entry LP64 z3* ✅ 2s 4s -50%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 3s +0%
mld_sample_s1_s2 LP64 z3* ✅ 4s 8s -50%
mld_sample_s1_s2_serial LP64 z3* ✅ 3s 6s -50%
mld_sign_attempt LP64 z3* ✅ 1s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 3s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 1s 3s -67%
mld_value_barrier_u8 LP64 z3* ✅ 1s 2s -50%
montgomery_reduce LP64 z3* ✅ 2s 2s +0%
ntt_native_aarch64 LP64 z3* ✅ 2s 4s -50%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 4s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 4s 3s +33%
pack_sig_c LP64 z3* ✅ 2s 2s +0%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 3s -33%
pack_sig_z LP64 z3* ✅ 2s 3s -33%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 2s 2s +0%
pack_sk_s1 LP64 z3* ✅ 2s 2s +0%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 5s 5s +0%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 5s 8s -38%
pointwise_native_aarch64 LP64 z3* ✅ 1s 4s -75%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 z3* ✅ 3s 5s -40%
poly_add LP64 z3* ✅ 4s 8s -50%
poly_caddq LP64 z3* ✅ 1s 5s -80%
poly_caddq_c LP64 z3* ✅ 3s 3s +0%
poly_caddq_native LP64 z3* ✅ 1s 3s -67%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_challenge LP64 z3* ✅ 3s 4s -25%
poly_chknorm LP64 z3* ✅ 3s 4s -25%
poly_chknorm_c LP64 z3* ✅ 6s 13s -54%
poly_chknorm_native LP64 z3* ✅ 3s 1s +200%
poly_chknorm_native_aarch64 LP64 z3* ✅ 3s 5s -40%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 z3* ✅ 3s 2s +50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 4s 3s +33%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_decompose_c LP64 z3* ✅ 3s 6s -50%
poly_decompose_native LP64 z3* ✅ 3s 2s +50%
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* ✅ 7s 9s -22%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_ntt LP64 z3* ✅ 2s 2s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 9s 19s -53%
poly_ntt_native LP64 z3* ✅ 3s 4s -25%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery_c LP64 z3* ✅ 72s 125s -42%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 3s +0%
poly_power2round LP64 z3* ✅ 3s 7s -57%
poly_reduce LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 z3* ✅ 3s 4s -25%
poly_sub LP64 z3* ✅ 3s 5s -40%
poly_uniform LP64 z3* ✅ 3s 4s -25%
poly_uniform_4x LP64 z3* ✅ 1s 3s -67%
poly_uniform_eta LP64 z3* ✅ 3s 5s -40%
poly_uniform_eta_4x LP64 z3* ✅ 7s 12s -42%
poly_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 3s -33%
poly_use_hint LP64 z3* ✅ 1s 4s -75%
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* ✅ 3s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 8s 13s -38%
polyt0_pack LP64 z3* ✅ 1s 3s -67%
polyt0_unpack LP64 z3* ✅ 7s 14s -50%
polyt1_pack LP64 z3* ✅ 2s 5s -60%
polyt1_unpack LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 3s 3s +0%
polyvec_matrix_expand_serial LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 13s -69%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 119s 196s -39%
polyveck_caddq LP64 z3* ✅ 4s 8s -50%
polyveck_chknorm LP64 z3* ✅ 3s 9s -67%
polyveck_decompose_pack_w1 LP64 z3* ✅ 4s - 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* ✅ 4s 6s -33%
polyveck_unpack_eta LP64 z3* ✅ 1s 3s -67%
polyvecl_chknorm LP64 z3* ✅ 3s 38s -92%
polyvecl_ntt LP64 z3* ✅ 4s 8s -50%
polyvecl_pack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 3s 2s +50%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_eta LP64 z3* ✅ 2s 3s -33%
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* ✅ 4s 2s +100%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 3s - new
polyz_pack LP64 z3* ✅ 2s 4s -50%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 1s 4s -75%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 3s 5s -40%
polyz_unpack_c LP64 z3* ✅ 5s 7s -29%
polyz_unpack_native LP64 z3* ✅ 2s 1s +100%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 2s 3s -33%
reduce32 LP64 z3* ✅ 1s 3s -67%
rej_eta LP64 bitwuzla* ✅ 2s 2s +0%
rej_eta_c LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_native LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform LP64 z3* ✅ 4s 7s -43%
rej_uniform_c LP64 z3* ✅ 9s 18s -50%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 4s - 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* ✅ 10s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 1s 3s -67%
shake128_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 4s -25%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
shake256 LP64 z3* ✅ 1s 3s -67%
shake256_absorb LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 z3* ✅ 2s 3s -33%
shake256_init LP64 z3* ✅ 2s 3s -33%
shake256_release LP64 z3* ✅ 2s 5s -60%
shake256_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 5s -80%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 4s -75%
sig_unpack_hints LP64 z3* ✅ 14s 4s +250%
sign_keypair LP64 z3* ✅ 6s 4s +50%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 34s 6s +467%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 82s 6s +1267%
sign_signature LP64 z3* ✅ 2s 4s -50%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 3s +367%
sign_signature_pre_hash_internal LP64 z3* ✅ 3s 2s +50%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 3s +67%
sign_verify LP64 z3* ✅ 3s 2s +50%
sign_verify_extmu LP64 z3* ✅ 3s 4s -25%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 200s 47s +326%
sign_verify_pre_hash_internal LP64 z3* ✅ 1s 3s -67%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 7s -43%
sk_s1hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 2s 2s +0%
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* ✅ 5s 4s +25%
unpack_sk_s1hat LP64 z3* ✅ 3s 3s +0%
unpack_sk_s2hat LP64 z3* ✅ 1s 3s -67%
unpack_sk_t0hat LP64 z3* ✅ 2s 4s -50%
use_hint LP64 z3* ✅ 2s 3s -33%
yvec_get_poly LP64 z3* ✅ 3s 2s +50%
yvec_init LP64 z3* ✅ 3s 4s -25%

@oqs-bot

oqs-bot commented Aug 11, 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* ⚠️ 121s 13s +831%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 193s 63s +206%
sig_unpack_hints LP64 z3* ⚠️ 27s 2s +1250%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 25s 5s +400%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 47s 6s +683%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 171s 55s +211%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 378s 177s +114%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1894s 1784s +6.2%
caddq LP64 z3* ✅ 2s 3s -33%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 121s 13s +831%
decompose LP64 z3* ✅ 1s 1s +0%
fqmul LP64 bitwuzla* ✅ 22s 40s -45%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
intt_native_rv32im_fastmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 3s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
intt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
keccak_absorb LP64 z3* ✅ 4s 3s +33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 8s -38%
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* ✅ 2s 2s +0%
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* ✅ 4s 5s -20%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_permute LP64 z3* ✅ 4s 4s +0%
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* ✅ 2s 2s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 193s 63s +206%
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 ✅ 2s 2s +0%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 1s 2s -50%
LP64 bitwuzla ✅ 3s 2s +50%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 1s 4s -75%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 5s 3s +67%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 2s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 2s -50%
mld_ct_sel_int32 LP64 z3* ✅ 2s 3s -33%
mld_h LP64 z3* ✅ 2s 2s +0%
mld_invntt_layer LP64 bitwuzla* ✅ 57s 109s -48%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 1s +100%
mld_keccakf1600_permute_c LP64 z3* ✅ 4s 6s -33%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 3s -33%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 24s -54%
mld_ntt_layer LP64 bitwuzla* ✅ 23s 41s -44%
mld_polymat_expand_entry LP64 z3* ✅ 3s 4s -25%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 2s +50%
mld_sample_s1_s2 LP64 z3* ✅ 2s 6s -67%
mld_sample_s1_s2_serial LP64 z3* ✅ 2s 4s -50%
mld_sign_attempt LP64 z3* ✅ 4s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 3s - new
mld_value_barrier_i64 LP64 z3* ✅ 1s 2s -50%
mld_value_barrier_u32 LP64 z3* ✅ 1s 3s -67%
mld_value_barrier_u8 LP64 z3* ✅ 3s 3s +0%
montgomery_reduce LP64 z3* ✅ 1s 4s -75%
ntt_native_aarch64 LP64 z3* ✅ 1s 2s -50%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 5s - new
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
pack_sig_c LP64 z3* ✅ 2s 5s -60%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 5s -60%
pack_sig_z LP64 z3* ✅ 3s 2s +50%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 2s 2s +0%
pack_sk_s1 LP64 z3* ✅ 3s 5s -40%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 2s 6s -67%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 8s -62%
pointwise_native_aarch64 LP64 z3* ✅ 1s 5s -80%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_add LP64 z3* ✅ 4s 9s -56%
poly_caddq LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 z3* ✅ 2s 2s +0%
poly_caddq_native LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 4s 3s +33%
poly_challenge LP64 z3* ✅ 1s 6s -83%
poly_chknorm LP64 z3* ✅ 1s 4s -75%
poly_chknorm_c LP64 z3* ✅ 7s 15s -53%
poly_chknorm_native LP64 z3* ✅ 4s 2s +100%
poly_chknorm_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 3s -67%
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* ✅ 2s 5s -60%
poly_decompose_native LP64 z3* ✅ 2s 3s -33%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_invntt_tomont LP64 z3* ✅ 3s 3s +0%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 8s 11s -27%
poly_invntt_tomont_native LP64 z3* ✅ 3s 2s +50%
poly_ntt LP64 z3* ✅ 3s 2s +50%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 19s -47%
poly_ntt_native LP64 z3* ✅ 2s 4s -50%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 4s -50%
poly_pointwise_montgomery LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery_c LP64 z3* ✅ 45s 125s -64%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 3s -33%
poly_power2round LP64 z3* ✅ 2s 4s -50%
poly_reduce LP64 z3* ✅ 3s 3s +0%
poly_shiftl LP64 z3* ✅ 5s 3s +67%
poly_sub LP64 z3* ✅ 1s 3s -67%
poly_uniform LP64 z3* ✅ 2s 4s -50%
poly_uniform_4x LP64 z3* ✅ 6s 13s -54%
poly_uniform_eta LP64 z3* ✅ 4s 4s +0%
poly_uniform_eta_4x LP64 z3* ✅ 6s 14s -57%
poly_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 4s -50%
poly_use_hint LP64 z3* ✅ 1s 3s -67%
poly_use_hint_c LP64 z3* ✅ 1s 5s -80%
poly_use_hint_native LP64 z3* ✅ 3s 2s +50%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 2s 8s -75%
polyt0_pack LP64 z3* ✅ 1s 3s -67%
polyt0_unpack LP64 z3* ✅ 7s 16s -56%
polyt1_pack LP64 z3* ✅ 2s 3s -33%
polyt1_unpack LP64 z3* ✅ 1s 5s -80%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 63s 110s -43%
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* ✅ 12s 18s -33%
polyveck_caddq LP64 z3* ✅ 4s 6s -33%
polyveck_chknorm LP64 z3* ✅ 3s 6s -50%
polyveck_decompose_pack_w1 LP64 z3* ✅ 5s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 8s -50%
polyveck_ntt LP64 z3* ✅ 6s 7s -14%
polyveck_pack_eta LP64 z3* ✅ 2s 4s -50%
polyveck_reduce LP64 z3* ✅ 2s 4s -50%
polyveck_unpack_eta LP64 z3* ✅ 2s 6s -67%
polyvecl_chknorm LP64 z3* ✅ 8s 7s +14%
polyvecl_ntt LP64 z3* ✅ 2s 4s -50%
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* ✅ 157s 210s -25%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 3s 2s +50%
polyvecl_uniform_gamma1 LP64 z3* ✅ 4s 2s +100%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 3s +0%
polyvecl_unpack_eta LP64 z3* ✅ 4s 3s +33%
polyvecl_unpack_z LP64 z3* ✅ 2s 3s -33%
polyw1_pack LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 z3* ✅ 1s 4s -75%
polyw1_pack_88 LP64 z3* ✅ 1s 2s -50%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 1s - new
polyz_pack LP64 z3* ✅ 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* ✅ 1s 3s -67%
polyz_unpack_c LP64 z3* ✅ 3s 13s -77%
polyz_unpack_native LP64 z3* ✅ 1s 4s -75%
polyz_unpack_native_x86_64 LP64 z3* ✅ 5s 3s +67%
power2round LP64 z3* ✅ 1s 1s +0%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 2s 2s +0%
rej_eta_c LP64 bitwuzla* ✅ 1s 5s -80%
rej_eta_native LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform LP64 z3* ✅ 9s 18s -50%
rej_uniform_c LP64 z3* ✅ 8s 14s -43%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 4s -25%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 6s - new
shake128_absorb LP64 z3* ✅ 1s 2s -50%
shake128_finalize LP64 z3* ✅ 1s 1s +0%
shake128_init LP64 z3* ✅ 1s 2s -50%
shake128_release LP64 z3* ✅ 2s 3s -33%
shake128_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
shake256 LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 z3* ✅ 2s 2s +0%
shake256_finalize LP64 z3* ✅ 4s 1s +300%
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* ✅ 1s 2s -50%
sig_unpack_hints LP64 z3* ⚠️ 27s 2s +1250%
sign_keypair LP64 z3* ✅ 7s 3s +133%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 25s 5s +400%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 47s 6s +683%
sign_signature LP64 z3* ✅ 6s 6s +0%
sign_signature_extmu LP64 z3* ✅ 3s 2s +50%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 171s 55s +211%
sign_signature_pre_hash_internal LP64 z3* ✅ 2s 3s -33%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 3s 3s +0%
sign_verify LP64 z3* ✅ 5s 3s +67%
sign_verify_extmu LP64 z3* ✅ 4s 3s +33%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 378s 177s +114%
sign_verify_pre_hash_internal LP64 z3* ✅ 5s 5s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 5s -20%
sk_s1hat_get_poly LP64 z3* ✅ 2s 6s -67%
sk_s2hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 z3* ✅ 2s 2s +0%
sys_check_capability LP64 z3* ✅ 3s 4s -25%
unpack_pk_t1 LP64 z3* ✅ 1s 5s -80%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 z3* ✅ 2s 2s +0%
unpack_sk_s2hat LP64 z3* ✅ 3s 4s -25%
unpack_sk_t0hat LP64 z3* ✅ 2s 5s -60%
use_hint LP64 z3* ✅ 4s 2s +100%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Aug 11, 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* ⚠️ 338s 55s +515%
sig_unpack_hints LP64 z3* ⚠️ 27s 3s +800%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 44s 6s +633%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 49s 6s +717%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 356s 42s +748%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 592s 97s +510%
Full Results (229 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2662s 2151s +23.8%
caddq LP64 z3* ✅ 2s 4s -50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 187s 19s +884%
decompose LP64 z3* ✅ 2s 3s -33%
fqmul LP64 bitwuzla* ✅ 23s 43s -47%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 3s - new
intt_native_x86_64 LP64 z3* ✅ 3s 3s +0%
keccak_absorb LP64 z3* ✅ 3s 3s +0%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 3s 9s -67%
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* ✅ 1s 3s -67%
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* ✅ 3s 1s +200%
keccak_init LP64 z3* ✅ 2s 3s -33%
keccak_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute LP64 z3* ✅ 1s 3s -67%
keccakf1600_permute_native LP64 z3* ✅ 2s 4s -50%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_permute LP64 z3* ✅ 2s 3s -33%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 23s -48%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 4s 3s +33%
make_hint LP64 z3* ✅ 4s 3s +33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 338s 55s +515%
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 ✅ 2s 3s -33%
LP64 bitwuzla ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 4s 3s +33%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 5s 4s +25%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 5s 2s +150%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 3s -33%
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* ✅ 1s 3s -67%
mld_ct_sel_int32 LP64 z3* ✅ 2s 3s -33%
mld_h LP64 z3* ✅ 3s 3s +0%
mld_invntt_layer LP64 bitwuzla* ✅ 55s 115s -52%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 3s 4s -25%
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* ✅ 1s 4s -75%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 13s 24s -46%
mld_ntt_layer LP64 bitwuzla* ✅ 23s 45s -49%
mld_polymat_expand_entry LP64 z3* ✅ 1s 3s -67%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 2s 4s -50%
mld_sample_s1_s2 LP64 z3* ✅ 5s 6s -17%
mld_sample_s1_s2_serial LP64 z3* ✅ 3s 8s -62%
mld_sign_attempt LP64 z3* ✅ 1s - new
mld_sign_finish LP64 z3* ✅ 3s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 1s +100%
mld_value_barrier_u32 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u8 LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 z3* ✅ 3s 3s +0%
ntt_native_aarch64 LP64 z3* ✅ 2s 6s -67%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - 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 4s -25%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 4s -50%
pack_sig_z LP64 z3* ✅ 2s 5s -60%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 3s 3s +0%
pack_sk_s1 LP64 z3* ✅ 2s 1s +100%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 5s 6s -17%
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* ✅ 3s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 5s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_add LP64 z3* ✅ 2s 6s -67%
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* ✅ 2s 3s -33%
poly_caddq_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_challenge LP64 z3* ✅ 3s 5s -40%
poly_chknorm LP64 z3* ✅ 4s 3s +33%
poly_chknorm_c LP64 z3* ✅ 6s 15s -60%
poly_chknorm_native LP64 z3* ✅ 2s 4s -50%
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* ✅ 5s 5s +0%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 5s 2s +150%
poly_decompose_c LP64 z3* ✅ 3s 5s -40%
poly_decompose_native LP64 z3* ✅ 2s 2s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_invntt_tomont LP64 z3* ✅ 4s 1s +300%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 12s -42%
poly_invntt_tomont_native LP64 z3* ✅ 1s 5s -80%
poly_ntt LP64 z3* ✅ 2s 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* ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 3s 5s -40%
poly_pointwise_montgomery LP64 z3* ✅ 2s 4s -50%
poly_pointwise_montgomery_c LP64 z3* ✅ 44s 144s -69%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 5s -60%
poly_power2round LP64 z3* ✅ 3s 3s +0%
poly_reduce LP64 z3* ✅ 1s 2s -50%
poly_shiftl LP64 z3* ✅ 3s 4s -25%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 3s 4s -25%
poly_uniform_4x LP64 z3* ✅ 7s 13s -46%
poly_uniform_eta LP64 z3* ✅ 4s 4s +0%
poly_uniform_eta_4x LP64 z3* ✅ 7s 11s -36%
poly_uniform_gamma1 LP64 z3* ✅ 1s 4s -75%
poly_uniform_gamma1_4x LP64 z3* ✅ 5s 3s +67%
poly_use_hint LP64 z3* ✅ 2s 1s +100%
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* ✅ 3s 2s +50%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 3s 4s -25%
polyeta_unpack LP64 z3* ✅ 5s 17s -71%
polyt0_pack LP64 z3* ✅ 2s 4s -50%
polyt0_unpack LP64 z3* ✅ 8s 14s -43%
polyt1_pack LP64 z3* ✅ 3s 3s +0%
polyt1_unpack LP64 z3* ✅ 2s 4s -50%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 101s 324s -69%
polyvec_matrix_expand_serial LP64 z3* ✅ 16s 38s -58%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 3s 3s +0%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 11s 18s -39%
polyveck_caddq LP64 z3* ✅ 6s 8s -25%
polyveck_chknorm LP64 z3* ✅ 2s 3s -33%
polyveck_decompose_pack_w1 LP64 z3* ✅ 6s - new
polyveck_invntt_tomont LP64 z3* ✅ 5s 9s -44%
polyveck_ntt LP64 z3* ✅ 4s 11s -64%
polyveck_pack_eta LP64 z3* ✅ 3s 6s -50%
polyveck_reduce LP64 z3* ✅ 3s 3s +0%
polyveck_unpack_eta LP64 z3* ✅ 1s 4s -75%
polyvecl_chknorm LP64 z3* ✅ 3s 7s -57%
polyvecl_ntt LP64 z3* ✅ 5s 7s -29%
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* ✅ 213s 353s -40%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 2s +0%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 4s -25%
polyvecl_unpack_eta LP64 z3* ✅ 3s 5s -40%
polyvecl_unpack_z LP64 z3* ✅ 2s 4s -50%
polyw1_pack LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 z3* ✅ 3s 4s -25%
polyw1_pack_88 LP64 z3* ✅ 1s 3s -67%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 1s - new
polyw1_unpack_88 LP64 z3* ✅ 3s - new
polyz_pack LP64 z3* ✅ 1s 5s -80%
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* ✅ 5s 3s +67%
polyz_unpack_native LP64 z3* ✅ 1s 4s -75%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 2s 4s -50%
reduce32 LP64 z3* ✅ 5s 3s +67%
rej_eta LP64 bitwuzla* ✅ 1s 4s -75%
rej_eta_c LP64 bitwuzla* ✅ 4s 5s -20%
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* ✅ 3s 5s -40%
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* ✅ 3s 1s +200%
shake128_release LP64 z3* ✅ 1s 4s -75%
shake128_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 5s -60%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 3s -67%
shake256 LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 z3* ✅ 2s 2s +0%
shake256_finalize LP64 z3* ✅ 3s 2s +50%
shake256_init LP64 z3* ✅ 4s 2s +100%
shake256_release LP64 z3* ✅ 2s 3s -33%
shake256_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 1s +0%
sig_unpack_hints LP64 z3* ⚠️ 27s 3s +800%
sign_keypair LP64 z3* ✅ 5s 4s +25%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 44s 6s +633%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 49s 6s +717%
sign_signature LP64 z3* ✅ 4s 5s -20%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 356s 42s +748%
sign_signature_pre_hash_internal LP64 z3* ✅ 3s 5s -40%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 6s -17%
sign_verify LP64 z3* ✅ 2s 5s -60%
sign_verify_extmu LP64 z3* ✅ 1s 3s -67%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 592s 97s +510%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 3s 3s +0%
sk_s1hat_get_poly LP64 z3* ✅ 4s 3s +33%
sk_s2hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_t0hat_get_poly LP64 z3* ✅ 1s 4s -75%
sys_check_capability LP64 z3* ✅ 2s 3s -33%
unpack_pk_t1 LP64 z3* ✅ 2s 1s +100%
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* ✅ 4s 7s -43%
use_hint LP64 z3* ✅ 2s 3s -33%
yvec_get_poly LP64 z3* ✅ 4s 4s +0%
yvec_init LP64 z3* ✅ 2s 4s -50%

@mkannwischer
mkannwischer marked this pull request as ready for review August 11, 2026 06:37
@mkannwischer
mkannwischer requested a review from a team as a code owner August 11, 2026 06:37
hanno-becker
hanno-becker reviewed Aug 26, 2026
View reviewed changes
Comment thread mldsa/mldsa_native_config.h Outdated
hanno-becker
hanno-becker reviewed Aug 26, 2026
View reviewed changes
Comment thread mldsa/mldsa_native_config.h Outdated
hanno-becker
hanno-becker reviewed Aug 26, 2026
View reviewed changes
Comment thread mldsa/mldsa_native_config.h Outdated
hanno-becker
hanno-becker reviewed Aug 26, 2026
View reviewed changes
Comment thread mldsa/src/sys.h Outdated
hanno-becker
hanno-becker reviewed Aug 26, 2026
View reviewed changes
Comment thread mldsa/src/native/aarch64/meta.h Outdated
hanno-becker
hanno-becker reviewed Aug 26, 2026
View reviewed changes
Comment thread mldsa/src/native/x86_64/meta.h Outdated
hanno-becker
hanno-becker reviewed Aug 26, 2026
View reviewed changes
Comment thread mldsa/src/native/aarch64/meta.h Outdated
hanno-becker
hanno-becker requested changes Aug 26, 2026
View reviewed changes

@hanno-becker hanno-becker left a comment •
edited
Loading

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.

Overall this looks good, thanks @mkannwischer! Some documentation nits in comments. We should also use this opportunity to fix the pre-existing defect that if no alignment declarator is known, we silently build the backends without alignment constraints.

@mkannwischer
mkannwischer force-pushed the configurable-alignment branch from b64cbd8 to d0b1155 Compare October 1, 2026 07:04
@mkannwischer

mkannwischer commented Oct 1, 2026

Copy link
Copy Markdown
Contributor Author

Overall this looks good, thanks @mkannwischer! Some documentation nits in comments. We should also use this opportunity to fix the pre-existing defect that if no alignment declarator is known, we silently build the backends without alignment constraints.

I've addressed your comments. Apologies for the long delay, I had somehow forgotten about it. Could you take another look, please?

@mkannwischer
Make the alignment configurable
160f0a2 
Add two experimental config options: MLD_CONFIG_ALIGN sets the alignment
of large buffers and structures in bytes, MLD_CONFIG_ALIGN_ATTRIBUTE
replaces the declarator prefix for compilers supporting neither
__attribute__((aligned(N))) nor __declspec(align(N)).

MLD_DEFAULT_ALIGN is renamed to MLD_ALIGN_BYTES. MLD_ALIGN_BYTES,
MLD_ALIGN and MLD_ALIGN_UP are derived from the two options.

If no alignment declarator is known, MLD_ALIGN_BYTES is 1 and setting
MLD_CONFIG_ALIGN is an error. The x86_64 and AArch64 backends reject an
alignment below what their load and store instructions require, so they
refuse to build without alignment on such compilers.

MLD_TOTAL_ALLOC_* is measured for the default alignment, so it is not
defined once the alignment is customized, and the allocation test skips
itself in that case.

- Partially addresses #1346

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
mkannwischer force-pushed the configurable-alignment branch from d0b1155 to 160f0a2 Compare October 1, 2026 08:21

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hanno-becker hanno-becker hanno-becker requested changes

Requested changes must be addressed to merge this pull request.

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