Skip to content

CBMC: Push performance data to gh-pages - #1494

Merged
mkannwischer merged 2 commits into
mainfrom
gh-pages-push-fix
Oct 25, 2026
Merged

CBMC: Push performance data to gh-pages#1494
mkannwischer merged 2 commits into
mainfrom
gh-pages-push-fix

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

When we switched to using a merge queue in July, we stopped pushing CBMC performance results to Github pages. In consequence, all CBMC performance comparisons displayed in PRs since then are stale.

The reason is that the job that used to push results to gh-pages only does so when run on behalf of origin/main. With the switch to merge queues, we stopped running CI upon merge to origin/main (because the CI already ran in the merge queue, which is atop origin/main).

This PR resurrects CBMC performance data on gh-pages, as follows: Upon a successful run of the CBMC job on the merge queue, the job pushes an artifact with the performance data. Upon merge to origin/main, a new job picks up this artifact and pushes it to gh-pages. This separation is to prevent a successful CBMC job in an eventually failing merge queue run updating the gh-pages.

@hanno-becker
CBMC: Only use name-only baselines for default configurations
8882e33 
CI posts a CBMC runtime report on each PR. report.py compares the
runtime of each proof configuration (proof name, `dm`, solver) with a
baseline stored on the gh-pages branch. Baselines written before
configurations existed have a single entry per proof name, timed with
the default solver.

classify_proof() fell back to that name-only entry for every
configuration without an exact match. A secondary solver was therefore
compared with the default solver's time and flagged as a regression.
For example, poly_caddq_native with bitwuzla showed 112s against 3s,
which is the time of the default z3 configuration.

Use the name-only entry only for default configurations. Other
configurations without an exact baseline entry are now reported as
`new`.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
CI: Publish CBMC baselines from merge queue runs
de6cb3b 
PR reports compare CBMC runtimes with baselines on gh-pages
(dev/cbmc[-reduce-ram]/mldsa-{44,65,87}.json). report.py wrote them in
CI runs on main. Since 529a89d ("CI: Do not run on pushes to main"),
CI runs on PRs and in the merge queue only, and the baselines are
still those of 2026-07-03, from before per-configuration timings.

The merge queue tests the exact commit that main is then fast-forwarded
to, so its timings are the right baseline. When a batch of PRs merges
as one push, the run for the tip covers the whole batch.

- Each CBMC job writes its result file at its gh-pages path under
  $RUNNER_TEMP/cbmc-results. In merge queue runs it uploads that tree
  as artifact cbmc-results-mldsa-<set>[-reduce-ram]. A failing proof
  fails the step before the upload.
- cbmc_publish.yml runs on each push to main. It finds the merge queue
  run of all.yml for the pushed commit, downloads its artifacts into a
  gh-pages checkout, and pushes them as one commit with the workflow
  token. If bench.yml pushed first, it rebases and retries once. For a
  commit that reached main outside the merge queue, it warns and skips.

The workflow pushes with git instead of the Contents API that
push_to_gh_pages() used. A result file now has 3010 entries (215
proofs, 2 data models, 7 solver profiles), about 570 KiB. Its base64
encoding is too long for the single `-F content=...` argument of
`gh api`: Linux limits one argument to 128 KiB.

Remove push_to_gh_pages() and the refs/heads/main branch of report.py
main() that called it.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
hanno-becker requested a review from a team as a code owner October 25, 2026 14:40
mkannwischer
mkannwischer approved these changes Oct 25, 2026
View reviewed changes

@mkannwischer mkannwischer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks for fixing this @hanno-becker. LGTM (from looking at the code - let's try it out).

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

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

@mkannwischer
mkannwischer added this pull request to the merge queue Oct 25, 2026
Merged via the queue into main with commit a754991 Oct 25, 2026
410 checks passed
@mkannwischer
mkannwischer deleted the gh-pages-push-fix branch October 25, 2026 17:45
@github-actions github-actions Bot mentioned this pull request Oct 25, 2026
Closed
@hanno-becker hanno-becker mentioned this pull request Oct 25, 2026
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer approved these changes

Assignees

No one assigned

Labels

needs-mlkem-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hanno-becker @oqs-bot @mkannwischer