Skip to content

Unit tests: Expose native primitives in reduced-API builds - #1422

Open
hanno-becker wants to merge 1 commit into
mainfrom
i1420
Open

Unit tests: Expose native primitives in reduced-API builds#1422
hanno-becker wants to merge 1 commit into
mainfrom
i1420

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Sep 9, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor 
Several backend unit tests were additionally guarded by the public APIs
which use the tested primitives. Reduced-API builds therefore skipped
available native implementations, while declarations and generated
backend files used different guards.

Make `MLD_UNIT_TEST` expose decomposition, hint use, `polyz`
unpacking, and eta rejection sampling throughout the core and native
backends. Simplify these tests, and the pointwise multiplication test,
to depend only on their `MLD_USE_NATIVE_*` macros. Keep keypair-only
eta helpers and `polyw1` packing under their original public API
guards.

The vector pointwise accumulator has the opposite issue: reduced-RAM
builds use the per-polynomial path, but still include its L4, L5, and
L7 native implementations. Align the AArch64 and x86_64 declarations,
wrappers, and assembly with the core `MLD_CONFIG_REDUCE_RAM` guard,
while retaining those implementations for unit tests.

Update autogen and the generated AArch64 and x86_64 files
accordingly.

@hanno-becker
hanno-becker force-pushed the i1420 branch 2 times, most recently from 35e9cb1 to 8146fca Compare September 9, 2026 14:17
@oqs-bot

oqs-bot commented Sep 9, 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* ⚠️ 128s 19s +574%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 42s 5s +740%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 164s 49s +235%
Full Results (217 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1193s 1364s -12.5%
caddq LP64 z3* ✅ 2s 6s -67%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 30s 12s +150%
decompose LP64 z3* ✅ 3s 3s +0%
fqmul LP64 bitwuzla* ✅ 22s 39s -44%
fqscale LP64 bitwuzla* ✅ 2s 2s +0%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_x86_64 LP64 z3* ✅ 1s 2s -50%
keccak_absorb LP64 z3* ✅ 4s 3s +33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 8s -25%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_finalize LP64 z3* ✅ 1s 2s -50%
keccak_init LP64 z3* ✅ 3s 3s +0%
keccak_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 4s -50%
keccakf1600_permute LP64 z3* ✅ 1s 2s -50%
keccakf1600_permute_native LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 6s -83%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
keccakf1600x4_permute_native LP64 z3* ✅ 13s 22s -41%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 5s -60%
make_hint LP64 z3* ✅ 2s 3s -33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 128s 19s +574%
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 ✅ 3s 3s +0%
ILP32 cvc5_arrays_exp ✅ 2s 3s -33%
ILP32 z3 ✅ 1s 3s -67%
LP64 bitwuzla ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 1s 3s -67%
LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 3s 3s +0%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 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* ✅ 2s 2s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 1s +100%
mld_ct_sel_int32 LP64 z3* ✅ 1s 3s -67%
mld_h LP64 z3* ✅ 2s 4s -50%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 105s -45%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600_permute_c LP64 z3* ✅ 4s 7s -43%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 4s -50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 4s -75%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 10s 23s -57%
mld_ntt_layer LP64 bitwuzla* ✅ 22s 41s -46%
mld_polymat_expand_entry LP64 z3* ✅ 2s 2s +0%
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* ✅ 3s 4s -25%
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 3s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 3s 3s +0%
mld_value_barrier_u32 LP64 z3* ✅ 2s 1s +100%
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_x86_64 LP64 z3* ✅ 1s 3s -67%
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* ✅ 1s 4s -75%
pack_sig_z LP64 z3* ✅ 2s 2s +0%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 3s 5s -40%
pack_sk_s1 LP64 z3* ✅ 4s 3s +33%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 6s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 4s +0%
pointwise_native_aarch64 LP64 z3* ✅ 2s 2s +0%
pointwise_native_x86_64 LP64 z3* ✅ 4s 4s +0%
poly_add LP64 z3* ✅ 2s 7s -71%
poly_caddq LP64 z3* ✅ 3s 4s -25%
poly_caddq_c LP64 z3* ✅ 3s 3s +0%
poly_caddq_native LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_challenge LP64 z3* ✅ 1s 6s -83%
poly_chknorm LP64 z3* ✅ 3s 3s +0%
poly_chknorm_c LP64 z3* ✅ 5s 11s -55%
poly_chknorm_native LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_chknorm_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_decompose LP64 z3* ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 4s 4s +0%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_decompose_c LP64 z3* ✅ 3s 5s -40%
poly_decompose_native LP64 z3* ✅ 1s 2s -50%
poly_decompose_native_x86_64 LP64 z3* ✅ 4s 2s +100%
poly_invntt_tomont LP64 z3* ✅ 1s 2s -50%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 11s -36%
poly_invntt_tomont_native LP64 z3* ✅ 2s 3s -33%
poly_ntt LP64 z3* ✅ 4s 3s +33%
poly_ntt_c LP64 z3_smt_only* ✅ 9s 21s -57%
poly_ntt_native LP64 z3* ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 5s -60%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery_c LP64 z3* ✅ 66s 112s -41%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 2s -50%
poly_power2round LP64 z3* ✅ 3s 4s -25%
poly_reduce LP64 z3* ✅ 3s 4s -25%
poly_shiftl LP64 z3* ✅ 2s 4s -50%
poly_sub LP64 z3* ✅ 1s 3s -67%
poly_uniform LP64 z3* ✅ 1s 3s -67%
poly_uniform_4x LP64 z3* ✅ 3s 3s +0%
poly_uniform_eta LP64 z3* ✅ 2s 2s +0%
poly_uniform_eta_4x LP64 z3* ✅ 6s 12s -50%
poly_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 5s -60%
poly_use_hint LP64 z3* ✅ 2s 2s +0%
poly_use_hint_c LP64 z3* ✅ 3s 5s -40%
poly_use_hint_native LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_aarch64 LP64 z3* ✅ 4s 3s +33%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 8s 14s -43%
polyt0_pack LP64 z3* ✅ 2s 4s -50%
polyt0_unpack LP64 z3* ✅ 9s 12s -25%
polyt1_pack LP64 z3* ✅ 3s 3s +0%
polyt1_unpack LP64 z3* ✅ 1s 2s -50%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 3s 3s +0%
polyvec_matrix_expand_serial LP64 z3* ✅ 4s 4s +0%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 5s 6s -17%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 92s 149s -38%
polyveck_caddq LP64 z3* ✅ 3s 3s +0%
polyveck_chknorm LP64 z3* ✅ 4s 67s -94%
polyveck_decompose_pack_w1 LP64 z3* ✅ 3s - new
polyveck_invntt_tomont LP64 z3* ✅ 2s 5s -60%
polyveck_ntt LP64 z3* ✅ 1s 2s -50%
polyveck_pack_eta LP64 z3* ✅ 3s 4s -25%
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* ✅ 2s 3s -33%
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* ✅ 3s 4s -25%
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 2s +50%
polyvecl_unpack_eta LP64 z3* ✅ 2s 4s -50%
polyvecl_unpack_z LP64 z3* ✅ 1s 3s -67%
polyw1_pack LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 z3* ✅ 2s 3s -33%
polyw1_pack_88 LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 5s - new
polyz_pack LP64 z3* ✅ 2s 2s +0%
polyz_unpack LP64 z3* ✅ 2s 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* ✅ 6s 8s -25%
polyz_unpack_native LP64 z3* ✅ 3s 3s +0%
polyz_unpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
power2round LP64 z3* ✅ 1s 2s -50%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 1s 5s -80%
rej_eta_c LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_native LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform LP64 z3* ✅ 4s 8s -50%
rej_uniform_c LP64 z3* ✅ 7s 16s -56%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 3s 5s -40%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 11s - new
shake128_absorb LP64 z3* ✅ 2s 3s -33%
shake128_finalize LP64 z3* ✅ 1s 3s -67%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 3s 2s +50%
shake128_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
shake256 LP64 z3* ✅ 4s 1s +300%
shake256_absorb LP64 z3* ✅ 1s 2s -50%
shake256_finalize LP64 z3* ✅ 2s 2s +0%
shake256_init LP64 z3* ✅ 1s 4s -75%
shake256_release LP64 z3* ✅ 3s 1s +200%
shake256_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 1s +0%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
sig_unpack_hints LP64 z3* ✅ 10s 2s +400%
sign_keypair LP64 z3* ✅ 5s 5s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 16s 4s +300%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 42s 5s +740%
sign_signature LP64 z3* ✅ 5s 6s -17%
sign_signature_extmu LP64 z3* ✅ 2s 4s -50%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 4s +250%
sign_signature_pre_hash_internal LP64 z3* ✅ 1s 4s -75%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 4s 4s +0%
sign_verify LP64 z3* ✅ 4s 4s +0%
sign_verify_extmu LP64 z3* ✅ 3s 5s -40%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 164s 49s +235%
sign_verify_pre_hash_internal LP64 z3* ✅ 2s 5s -60%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 5s -60%
sk_s1hat_get_poly LP64 z3* ✅ 2s 2s +0%
sk_s2hat_get_poly LP64 z3* ✅ 2s 5s -60%
sk_t0hat_get_poly LP64 z3* ✅ 3s 1s +200%
sys_check_capability LP64 z3* ✅ 1s 2s -50%
unpack_pk_t1 LP64 z3* ✅ 3s 3s +0%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_s2hat LP64 z3* ✅ 3s 4s -25%
unpack_sk_t0hat LP64 z3* ✅ 2s 2s +0%
use_hint LP64 z3* ✅ 3s 2s +50%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 2s 1s +100%

@oqs-bot

oqs-bot commented Sep 9, 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* ⚠️ 31s 7s +343%
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* ⚠️ 180s 71s +154%
Full Results (217 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1224s 1482s -17.4%
caddq LP64 z3* ✅ 3s 2s +50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 31s 7s +343%
decompose LP64 z3* ✅ 2s 4s -50%
fqmul LP64 bitwuzla* ✅ 23s 40s -43%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
intt_native_aarch64 LP64 z3* ✅ 3s 2s +50%
intt_native_x86_64 LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 3s 10s -70%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_finalize LP64 z3* ✅ 3s 2s +50%
keccak_init LP64 z3* ✅ 1s 4s -75%
keccak_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 3s -67%
keccakf1600_permute LP64 z3* ✅ 2s 4s -50%
keccakf1600_permute_native LP64 z3* ✅ 1s 2s -50%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 1s +200%
keccakf1600x4_permute LP64 z3* ✅ 1s 1s +0%
keccakf1600x4_permute_native LP64 z3* ✅ 11s 22s -50%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
make_hint LP64 z3* ✅ 2s 3s -33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 106s 31s +242%
mld_check_pct LP64 z3* ✅ 5s 12s -58%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 3s 5s -40%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 3s 6s -50%
ILP32 cvc5_arrays_exp ✅ 2s 6s -67%
ILP32 z3 ✅ 3s 6s -50%
LP64 bitwuzla ✅ 2s 6s -67%
LP64 cvc5_arrays_exp ✅ 3s 6s -50%
LP64 z3* ✅ 1s 6s -83%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 1s 3s -67%
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* ✅ 1s 3s -67%
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* ✅ 1s 3s -67%
mld_invntt_layer LP64 bitwuzla* ✅ 53s 108s -51%
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* ✅ 3s 2s +50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 25s -56%
mld_ntt_layer LP64 bitwuzla* ✅ 21s 43s -51%
mld_polymat_expand_entry LP64 z3* ✅ 2s 3s -33%
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* ✅ 5s 3s +67%
mld_sign_attempt LP64 z3* ✅ 1s - new
mld_sign_finish LP64 z3* ✅ 1s - new
mld_sign_resume LP64 z3* ✅ 1s - new
mld_value_barrier_i64 LP64 z3* ✅ 1s 2s -50%
mld_value_barrier_u32 LP64 z3* ✅ 2s 4s -50%
mld_value_barrier_u8 LP64 z3* ✅ 1s 1s +0%
montgomery_reduce LP64 z3* ✅ 3s 1s +200%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_x86_64 LP64 z3* ✅ 2s 5s -60%
nttunpack_native_x86_64 LP64 z3* ✅ 5s 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* ✅ 1s 1s +0%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 1s 2s -50%
pack_sk_s1 LP64 z3* ✅ 2s 3s -33%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 5s -40%
pointwise_native_aarch64 LP64 z3* ✅ 2s 3s -33%
pointwise_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_add LP64 z3* ✅ 4s 7s -43%
poly_caddq LP64 z3* ✅ 4s 3s +33%
poly_caddq_c LP64 z3* ✅ 5s 5s +0%
poly_caddq_native LP64 z3* ✅ 2s 4s -50%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_caddq_native_x86_64 LP64 z3* ✅ 5s 1s +400%
poly_challenge LP64 z3* ✅ 1s 5s -80%
poly_chknorm LP64 z3* ✅ 1s 3s -67%
poly_chknorm_c LP64 z3* ✅ 6s 13s -54%
poly_chknorm_native LP64 z3* ✅ 3s 4s -25%
poly_chknorm_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 4s -75%
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 2s +0%
poly_decompose_c LP64 z3* ✅ 3s 8s -62%
poly_decompose_native LP64 z3* ✅ 1s 5s -80%
poly_decompose_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_invntt_tomont LP64 z3* ✅ 2s 5s -60%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 5s 10s -50%
poly_invntt_tomont_native LP64 z3* ✅ 1s 5s -80%
poly_ntt LP64 z3* ✅ 3s 2s +50%
poly_ntt_c LP64 z3_smt_only* ✅ 9s 22s -59%
poly_ntt_native LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery LP64 z3* ✅ 3s 2s +50%
poly_pointwise_montgomery_c LP64 z3* ✅ 63s 116s -46%
poly_pointwise_montgomery_native LP64 z3* ✅ 4s 4s +0%
poly_power2round LP64 z3* ✅ 6s 7s -14%
poly_reduce LP64 z3* ✅ 1s 4s -75%
poly_shiftl LP64 z3* ✅ 3s 3s +0%
poly_sub LP64 z3* ✅ 2s 4s -50%
poly_uniform LP64 z3* ✅ 1s 2s -50%
poly_uniform_4x LP64 z3* ✅ 4s 4s +0%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
poly_uniform_eta_4x LP64 z3* ✅ 9s 13s -31%
poly_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
poly_uniform_gamma1_4x LP64 z3* ✅ 3s 3s +0%
poly_use_hint LP64 z3* ✅ 4s 3s +33%
poly_use_hint_c LP64 z3* ✅ 4s 2s +100%
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* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 1s 1s +0%
polyeta_unpack LP64 z3* ✅ 2s 4s -50%
polyt0_pack LP64 z3* ✅ 2s 5s -60%
polyt0_unpack LP64 z3* ✅ 9s 13s -31%
polyt1_pack LP64 z3* ✅ 3s 3s +0%
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* ✅ 2s 8s -75%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 146s 201s -27%
polyveck_caddq LP64 z3* ✅ 2s 7s -71%
polyveck_chknorm LP64 z3* ✅ 6s 36s -83%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 2s 7s -71%
polyveck_ntt LP64 z3* ✅ 1s 4s -75%
polyveck_pack_eta LP64 z3* ✅ 3s 3s +0%
polyveck_reduce LP64 z3* ✅ 5s 6s -17%
polyveck_unpack_eta LP64 z3* ✅ 3s 3s +0%
polyvecl_chknorm LP64 z3* ✅ 4s 43s -91%
polyvecl_ntt LP64 z3* ✅ 4s 7s -43%
polyvecl_pack_eta LP64 z3* ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
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* ✅ 2s 3s -33%
polyw1_pack_32 LP64 z3* ✅ 2s 2s +0%
polyw1_pack_88 LP64 z3* ✅ 3s 3s +0%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 3s 3s +0%
polyz_unpack LP64 z3* ✅ 1s 3s -67%
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* ✅ 3s 9s -67%
polyz_unpack_native LP64 z3* ✅ 2s 3s -33%
polyz_unpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
power2round LP64 z3* ✅ 2s 2s +0%
reduce32 LP64 z3* ✅ 1s 2s -50%
rej_eta LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_c LP64 bitwuzla* ✅ 1s 4s -75%
rej_eta_native LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform LP64 z3* ✅ 4s 7s -43%
rej_uniform_c LP64 z3* ✅ 6s 16s -62%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 5s -80%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 3s - 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* ✅ 1s 2s -50%
shake128_finalize LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 z3* ✅ 2s 6s -67%
shake128_release LP64 z3* ✅ 1s 2s -50%
shake128_squeeze LP64 bitwuzla* ✅ 2s 3s -33%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
shake256 LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 z3* ✅ 2s 4s -50%
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* ✅ 2s 4s -50%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
sig_unpack_hints LP64 z3* ✅ 10s 1s +900%
sign_keypair LP64 z3* ✅ 5s 4s +25%
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* ✅ 3s 5s -40%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 6s +133%
sign_signature_pre_hash_internal LP64 z3* ✅ 5s 3s +67%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 4s 7s -43%
sign_verify LP64 z3* ✅ 3s 6s -50%
sign_verify_extmu LP64 z3* ✅ 3s 2s +50%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 180s 71s +154%
sign_verify_pre_hash_internal LP64 z3* ✅ 1s 5s -80%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 6s -67%
sk_s1hat_get_poly LP64 z3* ✅ 1s 3s -67%
sk_s2hat_get_poly LP64 z3* ✅ 2s 1s +100%
sk_t0hat_get_poly LP64 z3* ✅ 2s 1s +100%
sys_check_capability LP64 z3* ✅ 2s 1s +100%
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* ✅ 1s 3s -67%
unpack_sk_t0hat LP64 z3* ✅ 1s 4s -75%
use_hint LP64 z3* ✅ 3s 2s +50%
yvec_get_poly LP64 z3* ✅ 1s 3s -67%
yvec_init LP64 z3* ✅ 1s 5s -80%

@oqs-bot

oqs-bot commented Sep 9, 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* ⚠️ 26s 12s +117%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 125s 34s +268%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 33s 6s +450%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 73s 6s +1117%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 178s 47s +279%
Full Results (217 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1254s 1436s -12.7%
caddq LP64 z3* ✅ 3s 3s +0%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 26s 12s +117%
decompose LP64 z3* ✅ 2s 2s +0%
fqmul LP64 bitwuzla* ✅ 22s 39s -44%
fqscale LP64 bitwuzla* ✅ 2s 1s +100%
intt_native_aarch64 LP64 z3* ✅ 3s 4s -25%
intt_native_x86_64 LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 z3* ✅ 3s 4s -25%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 8s -25%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 5s 2s +150%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 1s +100%
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 2s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 3s -67%
keccak_finalize LP64 z3* ✅ 1s 1s +0%
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* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 1s +0%
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* ✅ 1s 1s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
make_hint LP64 z3* ✅ 3s 2s +50%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 125s 34s +268%
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 ✅ 2s 1s +100%
ILP32 z3 ✅ 2s 1s +100%
LP64 bitwuzla ✅ 2s 1s +100%
LP64 cvc5_arrays_exp ✅ 1s 1s +0%
LP64 z3* ✅ 2s 1s +100%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 3s 2s +50%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 5s -60%
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* ✅ 2s 2s +0%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_memcmp LP64 bitwuzla* ✅ 3s 1s +200%
mld_ct_sel_int32 LP64 z3* ✅ 1s 2s -50%
mld_h LP64 z3* ✅ 1s 2s -50%
mld_invntt_layer LP64 bitwuzla* ✅ 54s 111s -51%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 1s +100%
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* ✅ 4s 1s +300%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 23s -52%
mld_ntt_layer LP64 bitwuzla* ✅ 22s 44s -50%
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* ✅ 5s - new
mld_sign_resume LP64 z3* ✅ 1s - 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* ✅ 1s 2s -50%
montgomery_reduce LP64 z3* ✅ 5s 2s +150%
ntt_native_aarch64 LP64 z3* ✅ 3s 4s -25%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
pack_sig_c LP64 z3* ✅ 1s 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* ✅ 3s 2s +50%
pack_sk_s1 LP64 z3* ✅ 1s 2s -50%
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 5s -20%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 5s 8s -38%
pointwise_native_aarch64 LP64 z3* ✅ 3s 4s -25%
pointwise_native_x86_64 LP64 z3* ✅ 2s 5s -60%
poly_add LP64 z3* ✅ 3s 8s -62%
poly_caddq LP64 z3* ✅ 1s 5s -80%
poly_caddq_c LP64 z3* ✅ 3s 3s +0%
poly_caddq_native LP64 z3* ✅ 4s 3s +33%
poly_caddq_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_challenge LP64 z3* ✅ 2s 4s -50%
poly_chknorm LP64 z3* ✅ 2s 4s -50%
poly_chknorm_c LP64 z3* ✅ 7s 13s -46%
poly_chknorm_native LP64 z3* ✅ 1s 1s +0%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 5s -60%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 z3* ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_decompose_c LP64 z3* ✅ 4s 6s -33%
poly_decompose_native LP64 z3* ✅ 3s 2s +50%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_invntt_tomont LP64 z3* ✅ 1s 4s -75%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 5s 9s -44%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_ntt LP64 z3* ✅ 2s 2s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 8s 19s -58%
poly_ntt_native LP64 z3* ✅ 1s 4s -75%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 1s 2s -50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery_c LP64 z3* ✅ 65s 125s -48%
poly_pointwise_montgomery_native LP64 z3* ✅ 2s 3s -33%
poly_power2round LP64 z3* ✅ 2s 7s -71%
poly_reduce LP64 z3* ✅ 1s 4s -75%
poly_shiftl LP64 z3* ✅ 2s 4s -50%
poly_sub LP64 z3* ✅ 2s 5s -60%
poly_uniform LP64 z3* ✅ 3s 4s -25%
poly_uniform_4x LP64 z3* ✅ 2s 3s -33%
poly_uniform_eta LP64 z3* ✅ 2s 5s -60%
poly_uniform_eta_4x LP64 z3* ✅ 8s 12s -33%
poly_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 3s -33%
poly_use_hint LP64 z3* ✅ 2s 4s -50%
poly_use_hint_c LP64 z3* ✅ 1s 4s -75%
poly_use_hint_native LP64 z3* ✅ 2s 1s +100%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 3s - new
polyeta_pack LP64 z3* ✅ 1s 3s -67%
polyeta_unpack LP64 z3* ✅ 9s 13s -31%
polyt0_pack LP64 z3* ✅ 3s 3s +0%
polyt0_unpack LP64 z3* ✅ 7s 14s -50%
polyt1_pack LP64 z3* ✅ 3s 5s -40%
polyt1_unpack LP64 z3* ✅ 3s 3s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 3s -67%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 6s 13s -54%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 112s 196s -43%
polyveck_caddq LP64 z3* ✅ 4s 8s -50%
polyveck_chknorm LP64 z3* ✅ 1s 9s -89%
polyveck_decompose_pack_w1 LP64 z3* ✅ 3s - new
polyveck_invntt_tomont LP64 z3* ✅ 3s 4s -25%
polyveck_ntt LP64 z3* ✅ 2s 3s -33%
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* ✅ 1s 38s -97%
polyvecl_ntt LP64 z3* ✅ 5s 8s -38%
polyvecl_pack_eta LP64 z3* ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_uniform_gamma1 LP64 z3* ✅ 1s 3s -67%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_eta LP64 z3* ✅ 3s 3s +0%
polyvecl_unpack_z LP64 z3* ✅ 1s 3s -67%
polyw1_pack LP64 z3* ✅ 1s 2s -50%
polyw1_pack_32 LP64 z3* ✅ 3s 3s +0%
polyw1_pack_88 LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 z3* ✅ 2s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 3s 4s -25%
polyz_unpack LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 1s 5s -80%
polyz_unpack_c LP64 z3* ✅ 4s 7s -43%
polyz_unpack_native LP64 z3* ✅ 1s 1s +0%
polyz_unpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 2s 3s -33%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 3s 2s +50%
rej_eta_c LP64 bitwuzla* ✅ 4s 4s +0%
rej_eta_native LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform LP64 z3* ✅ 4s 7s -43%
rej_uniform_c LP64 z3* ✅ 7s 18s -61%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 1s - new
rej_uniform_native LP64 bitwuzla* ✅ 4s 5s -20%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 6s - new
shake128_absorb LP64 z3* ✅ 3s 2s +50%
shake128_finalize LP64 z3* ✅ 1s 2s -50%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 2s 3s -33%
shake128_squeeze LP64 bitwuzla* ✅ 2s 1s +100%
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 4s -75%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 1s +0%
shake256 LP64 z3* ✅ 3s 3s +0%
shake256_absorb LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 z3* ✅ 1s 3s -67%
shake256_init LP64 z3* ✅ 2s 3s -33%
shake256_release LP64 z3* ✅ 1s 5s -80%
shake256_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
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* ✅ 7s 4s +75%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 33s 6s +450%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 73s 6s +1117%
sign_signature LP64 z3* ✅ 2s 4s -50%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 15s 3s +400%
sign_signature_pre_hash_internal LP64 z3* ✅ 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* ✅ 2s 4s -50%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 178s 47s +279%
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* ✅ 3s 2s +50%
sk_t0hat_get_poly LP64 z3* ✅ 2s 3s -33%
sys_check_capability LP64 z3* ✅ 1s 2s -50%
unpack_pk_t1 LP64 z3* ✅ 1s 2s -50%
unpack_sk LP64 z3* ✅ 2s 4s -50%
unpack_sk_s1hat LP64 z3* ✅ 3s 3s +0%
unpack_sk_s2hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_t0hat LP64 z3* ✅ 3s 4s -25%
use_hint LP64 z3* ✅ 2s 3s -33%
yvec_get_poly LP64 z3* ✅ 1s 2s -50%
yvec_init LP64 z3* ✅ 3s 4s -25%

@oqs-bot

oqs-bot commented Sep 9, 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* ⚠️ 94s 50s +88%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 133s 58s +129%
polyveck_chknorm LP64 z3* ⚠️ 52s 5s +940%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 37s 5s +640%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 105s 26s +304%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 268s 114s +135%
Full Results (217 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1562s 1514s +3.2%
caddq LP64 z3* ✅ 2s 2s +0%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 94s 50s +88%
decompose LP64 z3* ✅ 3s 2s +50%
fqmul LP64 bitwuzla* ✅ 22s 39s -44%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 3s 9s -67%
intt_native_x86_64 LP64 z3* ✅ 3s 4s -25%
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* ✅ 1s 3s -67%
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* ✅ 1s 3s -67%
keccak_finalize LP64 z3* ✅ 2s 3s -33%
keccak_init LP64 z3* ✅ 2s 3s -33%
keccak_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 2s +0%
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 4s -50%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 4s 3s +33%
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* ✅ 2s 3s -33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 133s 58s +129%
mld_check_pct LP64 z3* ✅ 4s 14s -71%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 6s 7s -14%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 2s -50%
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* ✅ 1s 3s -67%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 6s 2s +200%
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* ✅ 4s 1s +300%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 1s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 3s 3s +0%
mld_ct_sel_int32 LP64 z3* ✅ 1s 2s -50%
mld_h LP64 z3* ✅ 2s 4s -50%
mld_invntt_layer LP64 bitwuzla* ✅ 55s 107s -49%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600_permute_c LP64 z3* ✅ 3s 8s -62%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 6s 2s +200%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 11s 23s -52%
mld_ntt_layer LP64 bitwuzla* ✅ 19s 42s -55%
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* ✅ 2s 4s -50%
mld_sample_s1_s2_serial LP64 z3* ✅ 2s 3s -33%
mld_sign_attempt LP64 z3* ✅ 3s - 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* ✅ 3s 2s +50%
mld_value_barrier_u8 LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 z3* ✅ 3s 3s +0%
ntt_native_aarch64 LP64 z3* ✅ 4s 3s +33%
ntt_native_x86_64 LP64 z3* ✅ 4s 3s +33%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 1s +100%
pack_sig_c LP64 z3* ✅ 2s 2s +0%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 3s -33%
pack_sig_z LP64 z3* ✅ 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* ✅ 2s 4s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 3s 7s -57%
pointwise_native_aarch64 LP64 z3* ✅ 1s 5s -80%
pointwise_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_add LP64 z3* ✅ 2s 7s -71%
poly_caddq LP64 z3* ✅ 1s 2s -50%
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* ✅ 2s 3s -33%
poly_chknorm LP64 z3* ✅ 2s 4s -50%
poly_chknorm_c LP64 z3* ✅ 5s 17s -71%
poly_chknorm_native LP64 z3* ✅ 3s 4s -25%
poly_chknorm_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_decompose LP64 z3* ✅ 1s 3s -67%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 4s 2s +100%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 3s 4s -25%
poly_decompose_c LP64 z3* ✅ 5s 4s +25%
poly_decompose_native LP64 z3* ✅ 3s 3s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_invntt_tomont LP64 z3* ✅ 2s 4s -50%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 5s 11s -55%
poly_invntt_tomont_native LP64 z3* ✅ 3s 4s -25%
poly_ntt LP64 z3* ✅ 3s 3s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 19s -47%
poly_ntt_native LP64 z3* ✅ 2s 5s -60%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 1s 4s -75%
poly_pointwise_montgomery LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery_c LP64 z3* ✅ 42s 114s -63%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 2s +50%
poly_power2round LP64 z3* ✅ 2s 4s -50%
poly_reduce LP64 z3* ✅ 2s 3s -33%
poly_shiftl LP64 z3* ✅ 3s 3s +0%
poly_sub LP64 z3* ✅ 1s 3s -67%
poly_uniform LP64 z3* ✅ 5s 6s -17%
poly_uniform_4x LP64 z3* ✅ 6s 14s -57%
poly_uniform_eta LP64 z3* ✅ 4s 5s -20%
poly_uniform_eta_4x LP64 z3* ✅ 8s 11s -27%
poly_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 5s -60%
poly_use_hint LP64 z3* ✅ 2s 4s -50%
poly_use_hint_c LP64 z3* ✅ 1s 3s -67%
poly_use_hint_native LP64 z3* ✅ 2s 4s -50%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 1s 3s -67%
polyeta_unpack LP64 z3* ✅ 6s 14s -57%
polyt0_pack LP64 z3* ✅ 1s 2s -50%
polyt0_unpack LP64 z3* ✅ 6s 15s -60%
polyt1_pack LP64 z3* ✅ 1s 4s -75%
polyt1_unpack LP64 z3* ✅ 1s 5s -80%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 16s 28s -43%
polyvec_matrix_expand_serial LP64 z3* ✅ 5s 8s -38%
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* ✅ 2s 3s -33%
polyveck_chknorm LP64 z3* ⚠️ 52s 5s +940%
polyveck_decompose_pack_w1 LP64 z3* ✅ 3s - new
polyveck_invntt_tomont LP64 z3* ✅ 1s 5s -80%
polyveck_ntt LP64 z3* ✅ 2s 5s -60%
polyveck_pack_eta LP64 z3* ✅ 2s 2s +0%
polyveck_reduce LP64 z3* ✅ 4s 5s -20%
polyveck_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_chknorm LP64 z3* ✅ 5s 10s -50%
polyvecl_ntt LP64 z3* ✅ 1s 2s -50%
polyvecl_pack_eta LP64 z3* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 3s 4s -25%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 136s 131s +4%
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* ✅ 3s 2s +50%
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 4s 2s +100%
polyw1_pack LP64 z3* ✅ 1s 3s -67%
polyw1_pack_32 LP64 z3* ✅ 1s 2s -50%
polyw1_pack_88 LP64 z3* ✅ 2s 1s +100%
polyw1_unpack LP64 z3* ✅ 3s - new
polyw1_unpack_32 LP64 z3* ✅ 1s - new
polyw1_unpack_88 LP64 z3* ✅ 3s - new
polyz_pack LP64 z3* ✅ 2s 2s +0%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 5s 5s +0%
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* ✅ 2s 3s -33%
power2round LP64 z3* ✅ 1s 3s -67%
reduce32 LP64 z3* ✅ 5s 2s +150%
rej_eta LP64 bitwuzla* ✅ 2s 3s -33%
rej_eta_c LP64 bitwuzla* ✅ 1s 4s -75%
rej_eta_native LP64 bitwuzla* ✅ 4s 6s -33%
rej_uniform LP64 z3* ✅ 10s 18s -44%
rej_uniform_c LP64 z3* ✅ 11s 15s -27%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - 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* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 3s 2s +50%
shake128_init LP64 z3* ✅ 1s 3s -67%
shake128_release LP64 z3* ✅ 2s 1s +100%
shake128_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 1s +200%
shake256 LP64 z3* ✅ 1s 1s +0%
shake256_absorb LP64 z3* ✅ 2s 3s -33%
shake256_finalize LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 z3* ✅ 2s 3s -33%
shake256_release LP64 z3* ✅ 2s 2s +0%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 5s 3s +67%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 4s -75%
sig_unpack_hints LP64 z3* ✅ 19s 2s +850%
sign_keypair LP64 z3* ✅ 5s 4s +25%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 17s 4s +325%
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* ⚠️ 105s 26s +304%
sign_signature_pre_hash_internal LP64 z3* ✅ 5s 6s -17%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 2s 3s -33%
sign_verify LP64 z3* ✅ 5s 4s +25%
sign_verify_extmu LP64 z3* ✅ 3s 3s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 268s 114s +135%
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* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 z3* ✅ 4s 2s +100%
sys_check_capability LP64 z3* ✅ 2s 4s -50%
unpack_pk_t1 LP64 z3* ✅ 2s 5s -60%
unpack_sk LP64 z3* ✅ 2s 3s -33%
unpack_sk_s1hat LP64 z3* ✅ 1s 1s +0%
unpack_sk_s2hat LP64 z3* ✅ 3s 4s -25%
unpack_sk_t0hat LP64 z3* ✅ 2s 3s -33%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 3s 3s +0%
yvec_init LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Sep 9, 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* ⚠️ 127s 13s +877%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 204s 63s +224%
sig_unpack_hints LP64 z3* ⚠️ 26s 2s +1200%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 28s 5s +460%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 52s 6s +767%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 181s 55s +229%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 397s 177s +124%
Full Results (217 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2014s 1784s +12.9%
caddq LP64 z3* ✅ 3s 3s +0%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 127s 13s +877%
decompose LP64 z3* ✅ 1s 1s +0%
fqmul LP64 bitwuzla* ✅ 23s 40s -43%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
intt_native_x86_64 LP64 z3* ✅ 3s 3s +0%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 8s -50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 4s 4s +0%
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 2s +0%
keccak_finalize LP64 z3* ✅ 2s 2s +0%
keccak_init LP64 z3* ✅ 3s 1s +200%
keccak_squeeze LP64 bitwuzla* ✅ 1s 4s -75%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 5s -40%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 2s 3s -33%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
keccakf1600x4_permute_native LP64 z3* ✅ 14s 23s -39%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 4s 3s +33%
make_hint LP64 z3* ✅ 2s 2s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 204s 63s +224%
mld_check_pct LP64 z3* ✅ 6s 14s -57%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 7s -71%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 2s +0%
ILP32 cvc5_arrays_exp ✅ 3s 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* ✅ 1s 2s -50%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 4s 4s +0%
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* ✅ 1s 2s -50%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 2s +0%
mld_ct_sel_int32 LP64 z3* ✅ 3s 3s +0%
mld_h LP64 z3* ✅ 3s 2s +50%
mld_invntt_layer LP64 bitwuzla* ✅ 59s 109s -46%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 3s 1s +200%
mld_keccakf1600_permute_c LP64 z3* ✅ 3s 6s -50%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 4s 3s +33%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 24s -50%
mld_ntt_layer LP64 bitwuzla* ✅ 25s 41s -39%
mld_polymat_expand_entry LP64 z3* ✅ 4s 4s +0%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 1s 2s -50%
mld_sample_s1_s2 LP64 z3* ✅ 2s 6s -67%
mld_sample_s1_s2_serial LP64 z3* ✅ 3s 4s -25%
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* ✅ 1s 2s -50%
mld_value_barrier_u32 LP64 z3* ✅ 1s 3s -67%
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_x86_64 LP64 z3* ✅ 1s 2s -50%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
pack_sig_c LP64 z3* ✅ 3s 5s -40%
pack_sig_h LP64 z3_no_bv_extract* ✅ 3s 5s -40%
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* ✅ 6s 8s -25%
pointwise_native_aarch64 LP64 z3* ✅ 2s 5s -60%
pointwise_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_add LP64 z3* ✅ 5s 9s -44%
poly_caddq LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 z3* ✅ 4s 2s +100%
poly_caddq_native LP64 z3* ✅ 3s 2s +50%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 3s -33%
poly_challenge LP64 z3* ✅ 2s 6s -67%
poly_chknorm LP64 z3* ✅ 2s 4s -50%
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* ✅ 5s 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* ✅ 3s 1s +200%
poly_decompose_c LP64 z3* ✅ 4s 5s -20%
poly_decompose_native LP64 z3* ✅ 2s 3s -33%
poly_decompose_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_invntt_tomont LP64 z3* ✅ 2s 3s -33%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 11s -36%
poly_invntt_tomont_native LP64 z3* ✅ 3s 2s +50%
poly_ntt LP64 z3* ✅ 2s 2s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 19s -47%
poly_ntt_native LP64 z3* ✅ 4s 4s +0%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 4s -50%
poly_pointwise_montgomery LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery_c LP64 z3* ✅ 45s 125s -64%
poly_pointwise_montgomery_native LP64 z3* ✅ 4s 3s +33%
poly_power2round LP64 z3* ✅ 4s 4s +0%
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* ✅ 1s 4s -75%
poly_uniform_4x LP64 z3* ✅ 8s 13s -38%
poly_uniform_eta LP64 z3* ✅ 4s 4s +0%
poly_uniform_eta_4x LP64 z3* ✅ 8s 14s -43%
poly_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 4s -50%
poly_use_hint LP64 z3* ✅ 2s 3s -33%
poly_use_hint_c LP64 z3* ✅ 5s 5s +0%
poly_use_hint_native LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 2s 3s -33%
polyeta_unpack LP64 z3* ✅ 6s 8s -25%
polyt0_pack LP64 z3* ✅ 2s 3s -33%
polyt0_unpack LP64 z3* ✅ 7s 16s -56%
polyt1_pack LP64 z3* ✅ 1s 3s -67%
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* ✅ 5s 6s -17%
polyveck_chknorm LP64 z3* ✅ 5s 6s -17%
polyveck_decompose_pack_w1 LP64 z3* ✅ 4s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 8s -50%
polyveck_ntt LP64 z3* ✅ 4s 7s -43%
polyveck_pack_eta LP64 z3* ✅ 4s 4s +0%
polyveck_reduce LP64 z3* ✅ 4s 4s +0%
polyveck_unpack_eta LP64 z3* ✅ 1s 6s -83%
polyvecl_chknorm LP64 z3* ✅ 4s 7s -43%
polyvecl_ntt LP64 z3* ✅ 4s 4s +0%
polyvecl_pack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 174s 210s -17%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 3s 2s +50%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 2s +0%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 3s -33%
polyvecl_unpack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_unpack_z LP64 z3* ✅ 2s 3s -33%
polyw1_pack LP64 z3* ✅ 5s 4s +25%
polyw1_pack_32 LP64 z3* ✅ 3s 4s -25%
polyw1_pack_88 LP64 z3* ✅ 1s 2s -50%
polyw1_unpack LP64 z3* ✅ 4s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - 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* ✅ 2s 3s -33%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 3s -33%
polyz_unpack_c LP64 z3* ✅ 3s 13s -77%
polyz_unpack_native LP64 z3* ✅ 1s 4s -75%
polyz_unpack_native_x86_64 LP64 z3* ✅ 4s 3s +33%
power2round LP64 z3* ✅ 3s 1s +200%
reduce32 LP64 z3* ✅ 1s 3s -67%
rej_eta LP64 bitwuzla* ✅ 2s 2s +0%
rej_eta_c LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_native LP64 bitwuzla* ✅ 4s 3s +33%
rej_uniform LP64 z3* ✅ 10s 18s -44%
rej_uniform_c LP64 z3* ✅ 10s 14s -29%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 1s 1s +0%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 2s 3s -33%
shake128_squeeze LP64 bitwuzla* ✅ 3s 2s +50%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 3s +0%
shake256 LP64 z3* ✅ 1s 2s -50%
shake256_absorb LP64 z3* ✅ 1s 2s -50%
shake256_finalize LP64 z3* ✅ 2s 1s +100%
shake256_init LP64 z3* ✅ 2s 2s +0%
shake256_release LP64 z3* ✅ 1s 2s -50%
shake256_squeeze LP64 bitwuzla* ✅ 2s 3s -33%
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 3s 2s +50%
sig_unpack_hints LP64 z3* ⚠️ 26s 2s +1200%
sign_keypair LP64 z3* ✅ 5s 3s +67%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 28s 5s +460%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 52s 6s +767%
sign_signature LP64 z3* ✅ 4s 6s -33%
sign_signature_extmu LP64 z3* ✅ 6s 2s +200%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 181s 55s +229%
sign_signature_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 6s 3s +100%
sign_verify LP64 z3* ✅ 3s 3s +0%
sign_verify_extmu LP64 z3* ✅ 3s 3s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 397s 177s +124%
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* ✅ 2s 6s -67%
sk_s2hat_get_poly LP64 z3* ✅ 2s 2s +0%
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* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 z3* ✅ 2s 2s +0%
unpack_sk_s2hat LP64 z3* ✅ 4s 4s +0%
unpack_sk_t0hat LP64 z3* ✅ 4s 5s -20%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 3s 3s +0%

@oqs-bot

oqs-bot commented Sep 9, 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* ⚠️ 186s 19s +879%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 352s 55s +540%
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* ⚠️ 53s 6s +783%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 362s 42s +762%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 617s 97s +536%
Full Results (217 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2680s 2151s +24.6%
caddq LP64 z3* ✅ 2s 4s -50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 186s 19s +879%
decompose LP64 z3* ✅ 3s 3s +0%
fqmul LP64 bitwuzla* ✅ 24s 43s -44%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
intt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
keccak_absorb LP64 z3* ✅ 5s 3s +67%
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 5s 9s -44%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 1s 1s +0%
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* ✅ 2s 3s -33%
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* ✅ 3s 1s +200%
keccak_init LP64 z3* ✅ 1s 3s -67%
keccak_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 3s 3s +0%
keccakf1600_permute LP64 z3* ✅ 3s 3s +0%
keccakf1600_permute_native LP64 z3* ✅ 1s 4s -75%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 4s 2s +100%
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_permute LP64 z3* ✅ 1s 3s -67%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 23s -48%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
make_hint LP64 z3* ✅ 2s 3s -33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 352s 55s +540%
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 ✅ 2s 3s -33%
ILP32 cvc5_arrays_exp ✅ 1s 3s -67%
ILP32 z3 ✅ 1s 3s -67%
LP64 bitwuzla ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 3s 3s +0%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 1s 4s -75%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 4s 3s +33%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_sel_int32 LP64 z3* ✅ 3s 3s +0%
mld_h LP64 z3* ✅ 2s 3s -33%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 115s -50%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 4s -50%
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* ✅ 13s 24s -46%
mld_ntt_layer LP64 bitwuzla* ✅ 20s 45s -56%
mld_polymat_expand_entry LP64 z3* ✅ 1s 3s -67%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 4s -25%
mld_sample_s1_s2 LP64 z3* ✅ 3s 6s -50%
mld_sample_s1_s2_serial LP64 z3* ✅ 1s 8s -88%
mld_sign_attempt LP64 z3* ✅ 2s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 3s - new
mld_value_barrier_i64 LP64 z3* ✅ 1s 1s +0%
mld_value_barrier_u32 LP64 z3* ✅ 3s 2s +50%
mld_value_barrier_u8 LP64 z3* ✅ 1s 3s -67%
montgomery_reduce LP64 z3* ✅ 1s 3s -67%
ntt_native_aarch64 LP64 z3* ✅ 2s 6s -67%
ntt_native_x86_64 LP64 z3* ✅ 3s 2s +50%
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* ✅ 2s 4s -50%
pack_sig_z LP64 z3* ✅ 1s 5s -80%
pack_sk_rho_key_tr_s2 LP64 z3* ✅ 2s 3s -33%
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* ✅ 2s 5s -60%
pointwise_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_add LP64 z3* ✅ 3s 6s -50%
poly_caddq LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 z3* ✅ 3s 3s +0%
poly_caddq_native LP64 z3* ✅ 2s 4s -50%
poly_caddq_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 4s 2s +100%
poly_challenge LP64 z3* ✅ 3s 5s -40%
poly_chknorm LP64 z3* ✅ 3s 3s +0%
poly_chknorm_c LP64 z3* ✅ 6s 15s -60%
poly_chknorm_native LP64 z3* ✅ 3s 4s -25%
poly_chknorm_native_aarch64 LP64 z3* ✅ 4s 4s +0%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_decompose LP64 z3* ✅ 1s 3s -67%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 5s -60%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_decompose_c LP64 z3* ✅ 3s 5s -40%
poly_decompose_native LP64 z3* ✅ 4s 2s +100%
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* ✅ 5s 12s -58%
poly_invntt_tomont_native LP64 z3* ✅ 2s 5s -60%
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* ✅ 3s 4s -25%
poly_pointwise_montgomery_c LP64 z3* ✅ 43s 144s -70%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 5s -40%
poly_power2round LP64 z3* ✅ 5s 3s +67%
poly_reduce LP64 z3* ✅ 3s 2s +50%
poly_shiftl LP64 z3* ✅ 4s 4s +0%
poly_sub LP64 z3* ✅ 1s 3s -67%
poly_uniform LP64 z3* ✅ 3s 4s -25%
poly_uniform_4x LP64 z3* ✅ 5s 13s -62%
poly_uniform_eta LP64 z3* ✅ 4s 4s +0%
poly_uniform_eta_4x LP64 z3* ✅ 8s 11s -27%
poly_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 3s -67%
poly_use_hint LP64 z3* ✅ 2s 1s +100%
poly_use_hint_c LP64 z3* ✅ 4s 2s +100%
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* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 2s 4s -50%
polyeta_unpack LP64 z3* ✅ 5s 17s -71%
polyt0_pack LP64 z3* ✅ 3s 4s -25%
polyt0_unpack LP64 z3* ✅ 8s 14s -43%
polyt1_pack LP64 z3* ✅ 1s 3s -67%
polyt1_unpack LP64 z3* ✅ 1s 4s -75%
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* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 12s 18s -33%
polyveck_caddq LP64 z3* ✅ 5s 8s -38%
polyveck_chknorm LP64 z3* ✅ 3s 3s +0%
polyveck_decompose_pack_w1 LP64 z3* ✅ 6s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 9s -56%
polyveck_ntt LP64 z3* ✅ 3s 11s -73%
polyveck_pack_eta LP64 z3* ✅ 2s 6s -67%
polyveck_reduce LP64 z3* ✅ 3s 3s +0%
polyveck_unpack_eta LP64 z3* ✅ 2s 4s -50%
polyvecl_chknorm LP64 z3* ✅ 3s 7s -57%
polyvecl_ntt LP64 z3* ✅ 4s 7s -43%
polyvecl_pack_eta LP64 z3* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 2s 5s -60%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 222s 353s -37%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 1s 2s -50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 1s 4s -75%
polyvecl_unpack_eta LP64 z3* ✅ 1s 5s -80%
polyvecl_unpack_z LP64 z3* ✅ 2s 4s -50%
polyw1_pack LP64 z3* ✅ 3s 4s -25%
polyw1_pack_32 LP64 z3* ✅ 1s 4s -75%
polyw1_pack_88 LP64 z3* ✅ 2s 3s -33%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 2s 5s -60%
polyz_unpack LP64 z3* ✅ 1s 2s -50%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 1s 3s -67%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 1s 4s -75%
polyz_unpack_c LP64 z3* ✅ 3s 3s +0%
polyz_unpack_native LP64 z3* ✅ 1s 4s -75%
polyz_unpack_native_x86_64 LP64 z3* ✅ 5s 3s +67%
power2round LP64 z3* ✅ 2s 4s -50%
reduce32 LP64 z3* ✅ 1s 3s -67%
rej_eta LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_c LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_native LP64 bitwuzla* ✅ 3s 6s -50%
rej_uniform LP64 z3* ✅ 10s 15s -33%
rej_uniform_c LP64 z3* ✅ 7s 19s -63%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 3s 5s -40%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 1s - new
rej_uniform_native LP64 bitwuzla* ✅ 4s 8s -50%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 2s -50%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 8s - new
shake128_absorb LP64 z3* ✅ 1s 4s -75%
shake128_finalize LP64 z3* ✅ 3s 2s +50%
shake128_init LP64 z3* ✅ 2s 1s +100%
shake128_release LP64 z3* ✅ 2s 4s -50%
shake128_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 5s -60%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
shake256 LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 z3* ✅ 1s 2s -50%
shake256_finalize LP64 z3* ✅ 2s 2s +0%
shake256_init LP64 z3* ✅ 2s 2s +0%
shake256_release LP64 z3* ✅ 3s 3s +0%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
sig_unpack_hints LP64 z3* ⚠️ 29s 3s +867%
sign_keypair LP64 z3* ✅ 5s 4s +25%
sign_keypair_internal LP64 z3_no_bv_extract* ⚠️ 45s 6s +650%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 53s 6s +783%
sign_signature LP64 z3* ✅ 2s 5s -60%
sign_signature_extmu LP64 z3* ✅ 6s 4s +50%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 362s 42s +762%
sign_signature_pre_hash_internal LP64 z3* ✅ 2s 5s -60%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 4s 6s -33%
sign_verify LP64 z3* ✅ 2s 5s -60%
sign_verify_extmu LP64 z3* ✅ 3s 3s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 617s 97s +536%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 3s +33%
sk_s1hat_get_poly LP64 z3* ✅ 4s 3s +33%
sk_s2hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_t0hat_get_poly LP64 z3* ✅ 2s 4s -50%
sys_check_capability LP64 z3* ✅ 3s 3s +0%
unpack_pk_t1 LP64 z3* ✅ 2s 1s +100%
unpack_sk LP64 z3* ✅ 1s 5s -80%
unpack_sk_s1hat LP64 z3* ✅ 3s 2s +50%
unpack_sk_s2hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_t0hat LP64 z3* ✅ 6s 7s -14%
use_hint LP64 z3* ✅ 2s 3s -33%
yvec_get_poly LP64 z3* ✅ 1s 4s -75%
yvec_init LP64 z3* ✅ 1s 4s -75%

@hanno-becker Hanno Becker
Unit tests: Expose native primitives in reduced-API builds
1f9391c 
Several backend unit tests were additionally guarded by the public APIs
which use the tested primitives. Reduced-API builds therefore skipped
available native implementations, while declarations and generated
backend files used different guards.

Make `MLD_UNIT_TEST` expose decomposition, hint use, `polyz`
unpacking, and eta rejection sampling throughout the core and native
backends. Simplify these tests, and the pointwise multiplication test,
to depend only on their `MLD_USE_NATIVE_*` macros. Keep keypair-only
eta helpers and `polyw1` packing under their original public API
guards.

Update autogen and the generated AArch64 and x86_64 files
accordingly.

Fixes #1420

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker

hanno-becker commented Sep 13, 2026

Copy link
Copy Markdown
Contributor Author

@mkannwischer This works, but the hierarchy of #ifdefs is just a huge mess. I wonder if rather than piling more on -- even if for the sake of consistency -- we should rethink our approach and simplify.

@hanno-becker
hanno-becker marked this pull request as ready for review September 13, 2026 06:50
@hanno-becker
hanno-becker requested a review from a team as a code owner September 13, 2026 06:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hanno-becker @oqs-bot