Skip to content

RV32-IM: Unroll proofs to allow for later SLOTHY-fication - #1475

Draft
hanno-becker wants to merge 4 commits into
mainfrom
rv-unroll
Draft

RV32-IM: Unroll proofs to allow for later SLOTHY-fication#1475
hanno-becker wants to merge 4 commits into
mainfrom
rv-unroll

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Re-import updated s2n-bignum with better symbolic execution infrastructure. This speeds up symex so much that we can fully unroll the RV32-IM proofs.

Other proofs benefit as well, though not uniformly:


   Proof                            Baseline    PR #1475    Change                                                                                                                                                   
  ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━  ━━━━━━━━━━  ━━━━━━━━━━  ━━━━━━━━
   ARM NTT                            120:43      114:24     −5.2%
  ───────────────────────────────  ──────────  ──────────  ────────
   ARM INTT                           140:47      122:57    −12.7%
  ───────────────────────────────  ──────────  ──────────  ────────
   x86 NTT                            120:24      107:59    −10.3%
  ───────────────────────────────  ──────────  ──────────  ────────
   x86 INTT                           164:42      121:14    −26.4%
  ───────────────────────────────  ──────────  ──────────  ────────
   ARM pointwise accumulation L7       93:28       25:29    −72.7%
  ───────────────────────────────  ──────────  ──────────  ────────
   x86 pointwise accumulation L4       32:40       13:13    −59.5%
  ───────────────────────────────  ──────────  ──────────  ────────
   x86 decompose_32                    10:05       15:45    +56.2%
  ───────────────────────────────  ──────────  ──────────  ────────
   x86 polyz_unpack_17                 13:37       22:11    +62.9%

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

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

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

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

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

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

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

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

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

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

@oqs-bot

oqs-bot commented Oct 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

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

mkannwischer
mkannwischer reviewed Oct 19, 2026
View reviewed changes
Comment thread proofs/hol_light/riscv32/proofs/mldsa_ntt_rv32im_slowmul_asm.ml Outdated
@hanno-becker
hanno-becker force-pushed the rv-unroll branch 3 times, most recently from 19c5f32 to 0c59d29 Compare October 25, 2026 19:48
@hanno-becker
HOL-Light: Prepare SIMD simplifiers outside proof loops
c3c7520 
An instruction loop often applies the same arithmetic simplifier after
each step. Building SIMD_SIMPLIFY_TAC inside the instruction callback
rebuilds its rewrite conversion each time. The abbreviation variant also
rebuilt that conversion for every selected register equation.

Prepare the ARM/x86 step and SIMD tactics once before their loops. Move
conversion construction and definition selection out of the abbreviation
helper's per-fact callback. Still read local arithmetic equations from
the current context: these change during execution.

No converter-builder cache is needed. Prepared conversions capture the
basic rewrite table; prepare again if it or the arithmetic rules change.
Keep ordinary whole-context abbreviation, machine code and proof claims.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
HOL-Light: Drop unused context during integer closure
fd04909 
After the NTT output congruence has been reduced to a real polynomial,
REAL_INTEGER_TAC proves integer closure from the expression's structure.
It does not consult context facts, but its recursive subgoals still
carried the large execution context.

Discard that context immediately before the four ARM/x86 NTT and
INTT integer-closure calls. Leave instruction reasoning, congruence
rewriting, output bounds and HOL Light's tactic unchanged.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
nix: Pin the selected s2n-bignum execution speedups
c413488 
The HOL Light proofs take their shared tactics from a pinned source
package. Use the published hanno-becker revision a87e6f9f and its
unpacked source hash, so the shell needs no local checkout override.

Import independent CLARIFY_TAC facts, context rewrite reuse, faster
nonoverlap and frame handling, and guarded immutable reads. Include
opt-in frame seeding, parent snapshots and MEMOIZED_TOP_DEPTH_CONV.
Existing TOP_DEPTH_CONV callers keep their behavior.

The shared safety driver abbreviates the event-trace witness while its
saved justifications are assembled, then removes the temporary
definition. This applies unconditionally; custom drivers can still use
WITH_DEFERRED_ABBREVS_TAC explicitly. Our RV32 driver remains explicit.

The shared SIMD abbreviation helper prepares its conversion once per
prepared tactic, not per register fact. Upstream ARM/x86 SIMD loops
retain their prepared tactics; the analogous local changes precede
this pin in the history.

Also import upstream AES-GCM support and buffer-size division parsing.
These do not replace the local ML-DSA assembly or proof scripts.

Keep masked-address facts for all RISC-V instructions; do not restore
the JALR-only shortcut. Profiling, frame omission, goal-only
abbreviation and converter-builder caches remain excluded.

Change the source revision and hash. Keep HOL Light and the cross
toolchain unchanged. Full routine proofs and timings were not rerun for
this pin update.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
HOL-Light/RV32IM: Unroll all production arithmetic proofs
acf0c72 
The forward NTT, inverse NTT and pointwise Montgomery proofs used loop
invariants for fixed instruction sequences. Shared execution support now
allows each complete core to be executed symbolically. The resulting
exact output words feed the existing arithmetic theorems, which prove
the mathematical result and output bounds.

Switch all five production machine proofs in one change. Execute
9369/12439 forward NTT, 11936/15774 inverse NTT and 2821 pointwise
instructions, including branches and inverse NTT's final scaling loop.
Use scoped context rewriting and parent memory snapshots, explicit
permitted-frame seeding and guarded immutable input reads.

Prepare the scalar simplifier once per instruction loop. Fold arithmetic
expressions while expanding the output layout. Prepare one conversion
from the final context before splitting the 256 coefficient goals.
MEMOIZED_TOP_DEPTH_CONV shares equality proofs for repeated subterms
across those goals; do not cache construction of the converter itself.
A different context or basic rewrite table requires a new conversion.
Keep ordinary whole-context arithmetic abbreviations.

Use the block-based safety driver with ~defer_witness:true. A short name
stands for the complete trace function while saved instruction proofs
are assembled; WITH_DEFERRED_ABBREVS_TAC removes its defining equation
afterwards. Keep intermediate frame tracking and memory-access bounds.

Retain routine bytecode and all public core, callable and safety
claims, including the MUL/MULH timing caveat. Add helper parameter,
scoped-option and hypothesis checks. Document APIs and reproduction.
Do not add phase profiling, frame omission or goal-only abbreviations.

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

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

@mkannwischer mkannwischer mkannwischer left review comments

At least 1 approving review is required 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

@hanno-becker @oqs-bot @mkannwischer