Skip to content

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

Merged
mkannwischer merged 2 commits into
mainfrom
port-gh-pages
Oct 26, 2026
Merged

CBMC: Push performance data to gh-pages#1961
mkannwischer merged 2 commits into
mainfrom
port-gh-pages

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Oct 25, 2026 •
edited by mkannwischer
Loading

Copy link
Copy Markdown
Contributor

@hanno-becker
CBMC: Only use name-only baselines for default configurations
814678f 
CI posts a CBMC runtime report for each pull request. report.py
compares every proof configuration, identified by its proof name, data
model, and solver, with the baseline stored on gh-pages. Older
baselines contain only one entry per proof and record the default
configuration.

classify_proof() used that name-only entry whenever it could not find an
exact configuration match. A secondary solver was therefore compared
with the default solver runtime and could be reported as a false
regression.

Use name-only entries only for results marked as default. Report other
configurations without an exact baseline as new.

Ports pq-code-package/mldsa-native#1494.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
CI: Publish CBMC baselines from merge queue runs
7fd3c04 
Pull-request reports compare CBMC runtimes with baselines on gh-pages
(dev/cbmc/mlkem-{512,768,1024}.json). report.py previously wrote them
from CI runs on main. Since 116a592 ("CI: Do not run on pushes to
main"), CBMC runs only for pull requests and merge groups, so the
baselines have not been updated since 2026-08-03 and still contain one
result per proof.

The merge queue tests the exact commit that main then receives, so its
results are the right baseline. Each CBMC job now maps k=2, 3, or 4 to
the corresponding ML-KEM name, writes the result at its gh-pages path,
and uploads that tree from merge-group runs.

Run cbmc_publish.yml on each push to main. It finds the all.yml merge
queue run for that commit, downloads all CBMC artifacts into a gh-pages
checkout, and pushes them as one commit. Rebase and retry once if the
benchmark workflow changed gh-pages first; warn and skip commits that
did not pass through the merge queue.

Remove the Contents API upload from report.py. Configured result files
no longer need to be base64-encoded into a single gh command argument.

Ports pq-code-package/mldsa-native#1494.

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 21:14
@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
mlk_indcpa_dec LP64 z3* ⚠️ 23s 10s +130%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 452s 252s +79%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 277s 7s +3857%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 71s 46s +54%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 110s 55s +100%
Full Results (379 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1937s 1645s +17.8%
intt_native_aarch64 LP64 bitwuzla ✅ 11s - new
LP64 z3* ✅ 2s 5s -60%
intt_native_x86_64 LP64 bitwuzla ✅ 11s - new
LP64 z3* ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 1s - new
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 2s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 4s - new
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 2s - new
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 4s - new
keccakf1600_permute_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 16s 21s -24%
LP64 z3 ✅ 21s - new
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s - new
kem_check_pk LP64 z3* ✅ 3s 2s +50%
kem_check_sk LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 4s 2s +100%
kem_dec LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 8s 5s +60%
kem_enc LP64 bitwuzla ✅ 35s - new
LP64 z3* ✅ 4s 2s +100%
kem_enc_derand LP64 cadical ✅ 10s - new
LP64 z3* ✅ 2s 3s -33%
kem_keypair LP64 cadical ✅ 172s - new
LP64 z3* ✅ 2s 2s +0%
kem_keypair_derand LP64 bitwuzla ✅ 10s - new
LP64 z3* ✅ 2s 2s +0%
mlk_barrett_reduce LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 4s - new
mlk_ct_cmask_neg_i16 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u16 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s 4s -75%
mlk_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 4s -50%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 3s 3s +0%
LP64 cvc5_mbqi_enum ✅ 3s - new
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 3s - new
ILP32 cvc5_arrays_exp ✅ 2s - new
ILP32 z3 ✅ 3s - new
LP64 bitwuzla* ✅ 1s 1s +0%
LP64 cvc5_arrays_exp ✅ 2s - new
LP64 z3 ✅ 1s - new
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 1s - new
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
mlk_ct_memcmp LP64 bitwuzla* ✅ 1s 4s -75%
LP64 cvc5_enum_inst ✅ 3s - new
mlk_ct_sel_int16 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 3s +33%
mlk_ct_sel_uint8 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 1s +100%
mlk_enc_getnoise_eta1_eta2 LP64 cvc5_enum_inst ✅ 12s - new
LP64 z3* ✅ 1s 3s -67%
mlk_fqmul LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 16s -75%
mlk_gen_matrix LP64 cadical ✅ 57s - new
LP64 z3* ✅ 3s 2s +50%
mlk_gen_matrix_serial LP64 cadical ✅ 59s - new
LP64 z3* ✅ 4s 2s +100%
mlk_indcpa_dec LP64 cadical ✅ 81s - new
LP64 z3* ⚠️ 23s 10s +130%
mlk_indcpa_enc LP64 z3_smt_only* ⚠️ 452s 252s +79%
mlk_indcpa_keypair_derand LP64 z3* ✅ 116s 318s -64%
mlk_invntt_layer LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 4s 4s +0%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 5s +40%
LP64 z3 ✅ 7s - new
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 8s 7s +14%
LP64 z3 ✅ 32s - new
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 8s 8s +0%
LP64 cvc5_arrays_exp ✅ 21s - new
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 28s 24s +17%
LP64 cvc5_arrays_exp ✅ 18s - new
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3 ✅ 1s - new
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 3s - new
mlk_keccakf1600_permute LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 1s 1s +0%
mlk_keccakf1600_permute_c LP64 bitwuzla ✅ 6s - new
LP64 z3* ✅ 5s 6s -17%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 3s - new
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 1s - new
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 1s - new
mlk_keccakf1600x4_extract_bytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 2s +0%
mlk_keccakf1600x4_permute LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 2s 4s -50%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s - new
mlk_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 1s +100%
mlk_keypair_getnoise_eta1 LP64 cvc5_mbqi_enum ✅ 18s - new
LP64 z3* ✅ 3s 2s +50%
mlk_matvec_mul LP64 cadical ✅ 23s - new
LP64 z3* ✅ 3s 4s -25%
mlk_montgomery_reduce LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 1s +100%
mlk_ntt_butterfly_block LP64 bitwuzla ✅ 13s - new
LP64 z3* ⚠️ 277s 7s +3857%
mlk_ntt_layer LP64 bitwuzla ✅ 32s - new
LP64 z3* ✅ 6s 29s -79%
mlk_poly_add LP64 bitwuzla ✅ 62s - new
LP64 z3* ✅ 5s 7s -29%
mlk_poly_cbd_eta1 LP64 bitwuzla ✅ 14s - new
LP64 z3* ✅ 2s 1s +100%
mlk_poly_cbd_eta2 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d10_c LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 3s 2s +50%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d11_c LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 1s - new
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 4s - new
mlk_poly_compress_d4_c LP64 bitwuzla ✅ 13s - new
LP64 z3* ✅ 2s 1s +100%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 4s 3s +33%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d5_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 1s +200%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
mlk_poly_compress_du LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 2s - new
mlk_poly_compress_dv LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
mlk_poly_decompress_d10_c LP64 bitwuzla ✅ 7s - new
LP64 z3* ✅ 4s 1s +300%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 12s 15s -20%
LP64 z3 ✅ 1s - new
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
mlk_poly_decompress_d11_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 3s +0%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 1s - new
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 1s - new
mlk_poly_decompress_d4_c LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 14s 12s +17%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 4s 2s +100%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d5_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_du LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 3s - new
mlk_poly_frombytes LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s - new
mlk_poly_frombytes_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 6s 4s +50%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 11s 8s +38%
LP64 z3 ✅ 3s - new
mlk_poly_frommsg LP64 bitwuzla ✅ 10s - new
LP64 z3* ✅ 2s 9s -78%
mlk_poly_getnoise_eta1122_4x LP64 cvc5_mbqi_enum ✅ 3s - new
LP64 z3* ✅ 2s 1s +100%
mlk_poly_getnoise_eta1122_4x_serial LP64 cvc5_enum_inst ✅ 5s - new
LP64 z3* ✅ 1s - new
mlk_poly_getnoise_eta1_4x LP64 cvc5_enum_inst ✅ 80s - new
LP64 z3* ✅ 5s 2s +150%
mlk_poly_getnoise_eta1_4x_serial LP64 cvc5_enum_inst ✅ 80s - new
LP64 z3* ✅ 4s - new
mlk_poly_getnoise_eta2 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s 2s -50%
mlk_poly_invntt_tomont LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 4s 4s +0%
mlk_poly_invntt_tomont_c LP64 bitwuzla ✅ 46s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_mulcache_compute LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_native LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s 1s +0%
mlk_poly_ntt LP64 bitwuzla* ✅ 5s 5s +0%
LP64 z3 ✅ 2s - new
mlk_poly_ntt_c LP64 bitwuzla ✅ 63s - new
LP64 z3* ✅ 3s 1s +200%
mlk_poly_reduce LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 3s - new
mlk_poly_reduce_c LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 4s 3s +33%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 34s 34s +0%
LP64 z3 ✅ 2s - new
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 34s 129s -74%
LP64 z3 ✅ 4s - new
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 7s 5s +40%
mlk_poly_sub LP64 bitwuzla ✅ 33s - new
LP64 z3* ✅ 7s 10s -30%
mlk_poly_tobytes LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s - new
mlk_poly_tobytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 1s +200%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 2s - new
mlk_poly_tomont LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 4s 1s +300%
mlk_poly_tomont_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 4s 3s +33%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 2s - new
mlk_polymat_permute_bitrev_to_custom LP64 cadical ✅ 37s - new
LP64 z3* ✅ 5s 3s +67%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 65s - new
mlk_polyvec_add LP64 cadical ✅ 84s - new
LP64 z3* ✅ 10s 12s -17%
mlk_polyvec_basemul_acc_montgomery_cached LP64 bitwuzla ✅ 20s - new
LP64 z3* ✅ 2s 4s -50%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 cadical ✅ 17s - new
LP64 z3* ⚠️ 71s 46s +54%
mlk_polyvec_compress_du LP64 cadical ✅ 7s - new
LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_decompress_du LP64 cvc5_enum_inst ✅ 6s - new
LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_frombytes LP64 cvc5_enum_inst ✅ 7s - new
LP64 z3* ✅ 1s 3s -67%
mlk_polyvec_invntt_tomont LP64 cvc5_enum_inst ✅ 6s - new
LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_mulcache_compute LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_ntt LP64 cadical ✅ 22s - new
LP64 z3* ✅ 4s 4s +0%
mlk_polyvec_reduce LP64 cvc5_enum_inst ✅ 7s - new
LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_tobytes LP64 cvc5_mbqi_enum ✅ 4s - new
LP64 z3* ✅ 1s 1s +0%
mlk_polyvec_tomont LP64 cvc5_enum_inst ✅ 6s - new
LP64 z3* ✅ 2s 1s +100%
mlk_rej_uniform LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 10s - new
mlk_rej_uniform_c LP64 bitwuzla ✅ 5s - new
LP64 z3* ✅ 155s 114s +36%
mlk_scalar_compress_d1 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 4s 2s +100%
mlk_scalar_compress_d10 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d11 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 1s +0%
mlk_scalar_compress_d4 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 2s +50%
mlk_scalar_compress_d5 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 1s +100%
mlk_scalar_decompress_d10 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d4 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d5 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 2s +50%
mlk_scalar_signed_to_unsigned_q LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s 5s -80%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 2s - new
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 2s - new
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 4s - new
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 3s - new
mlk_shake256 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
mlk_shake256x4 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 cvc5_arrays_exp ✅ 31s - new
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 1s - new
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s - new
ntt_native_aarch64 LP64 bitwuzla ✅ 20s - new
LP64 z3* ✅ 4s 3s +33%
ntt_native_x86_64 LP64 bitwuzla ✅ 21s - new
LP64 z3* ✅ 1s 3s -67%
nttunpack_native_x86_64 LP64 cvc5_enum_inst ✅ 65s - new
LP64 z3* ✅ 2s 3s -33%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3 ✅ 2s - new
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 2s - new
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 3s - new
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3 ✅ 2s - new
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 1s - new
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 4s 6s -33%
LP64 z3 ✅ 3s - new
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 4s - new
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
LP64 z3 ✅ 2s - new
poly_invntt_tomont_native LP64 bitwuzla ✅ 7s - new
LP64 z3* ✅ 4s 2s +100%
poly_mulcache_compute_native_aarch64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 6s -67%
poly_mulcache_compute_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
poly_ntt_native LP64 bitwuzla ✅ 30s - new
LP64 z3* ✅ 3s 39s -92%
poly_reduce_native_aarch64 LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 3s 2s +50%
poly_reduce_native_x86_64 LP64 bitwuzla ✅ 13s - new
LP64 z3* ✅ 2s 2s +0%
poly_tobytes_native_aarch64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 1s 1s +0%
poly_tobytes_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_aarch64 LP64 bitwuzla ✅ 11s - new
LP64 z3* ✅ 1s 1s +0%
poly_tomont_native_x86_64 LP64 bitwuzla ✅ 10s - new
LP64 z3* ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_native LP64 cadical ✅ 8s - new
LP64 z3* ✅ 15s 14s +7%
rej_uniform_native LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3_smt_only ✅ 34s - new
rej_uniform_native_aarch64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 40s 45s -11%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ⚠️ 110s 55s +100%
sys_check_capability LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
mlk_ntt_butterfly_block LP64 z3* ⚠️ 282s 9s +3033%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 z3* ⚠️ 126s 79s +59%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 112s 67s +67%
Full Results (379 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 2083s 1885s +10.5%
intt_native_aarch64 LP64 bitwuzla ✅ 10s - new
LP64 z3* ✅ 3s 3s +0%
intt_native_x86_64 LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 2s - new
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 2s - new
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 1s - new
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 1s - new
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s - new
keccakf1600_permute_native LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 19s 15s +27%
LP64 z3 ✅ 16s - new
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
kem_check_pk LP64 z3* ✅ 2s 4s -50%
kem_check_sk LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 1s 3s -67%
kem_dec LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 8s 5s +60%
kem_enc LP64 bitwuzla ✅ 70s - new
LP64 z3* ✅ 4s 2s +100%
kem_enc_derand LP64 cadical ✅ 17s - new
LP64 z3* ✅ 2s 3s -33%
kem_keypair LP64 cadical ✅ 103s - new
LP64 z3* ✅ 4s 2s +100%
kem_keypair_derand LP64 bitwuzla ✅ 49s - new
LP64 z3* ✅ 6s 1s +500%
mlk_barrett_reduce LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 2s +0%
mlk_check_pct LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
mlk_ct_cmask_neg_i16 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u16 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 1s +200%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_mbqi_enum ✅ 3s - new
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s - new
ILP32 cvc5_arrays_exp ✅ 3s - new
ILP32 z3 ✅ 2s - new
LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_arrays_exp ✅ 2s - new
LP64 z3 ✅ 1s - new
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 2s - new
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s - new
mlk_ct_memcmp LP64 bitwuzla* ✅ 4s 3s +33%
LP64 cvc5_enum_inst ✅ 3s - new
mlk_ct_sel_int16 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 4s -75%
mlk_ct_sel_uint8 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_enc_getnoise_eta1_eta2 LP64 cvc5_enum_inst ✅ 20s - new
LP64 z3* ✅ 3s 4s -25%
mlk_fqmul LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 20s -80%
mlk_gen_matrix LP64 cadical ✅ 110s - new
LP64 z3* ✅ 4s 2s +100%
mlk_gen_matrix_serial LP64 cadical ✅ 119s - new
LP64 z3* ✅ 6s 4s +50%
mlk_indcpa_dec LP64 cadical ✅ 87s - new
LP64 z3* ✅ 13s 11s +18%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 432s 402s +7%
mlk_indcpa_keypair_derand LP64 z3* ✅ 156s 176s -11%
mlk_invntt_layer LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 6s 6s +0%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 4s 4s +0%
LP64 z3 ✅ 3s - new
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 5s +40%
LP64 z3 ✅ 3s - new
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 9s 10s -10%
LP64 z3 ✅ 34s - new
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 9s 9s +0%
LP64 cvc5_arrays_exp ✅ 19s - new
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 25s 26s -4%
LP64 cvc5_arrays_exp ✅ 20s - new
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s - new
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 4s - new
mlk_keccakf1600_permute LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_keccakf1600_permute_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 5s 6s -17%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 2s - new
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 3s - new
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 4s 2s +100%
LP64 z3 ✅ 2s - new
mlk_keccakf1600x4_extract_bytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
mlk_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 5s -60%
mlk_keypair_getnoise_eta1 LP64 cvc5_mbqi_enum ✅ 16s - new
LP64 z3* ✅ 3s 5s -40%
mlk_matvec_mul LP64 cadical ✅ 35s - new
LP64 z3* ✅ 2s 5s -60%
mlk_montgomery_reduce LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 2s +0%
mlk_ntt_butterfly_block LP64 bitwuzla ✅ 13s - new
LP64 z3* ⚠️ 282s 9s +3033%
mlk_ntt_layer LP64 bitwuzla ✅ 29s - new
LP64 z3* ✅ 7s 38s -82%
mlk_poly_add LP64 bitwuzla ✅ 61s - new
LP64 z3* ✅ 5s 5s +0%
mlk_poly_cbd_eta1 LP64 bitwuzla ✅ 13s - new
LP64 z3* ✅ 1s 3s -67%
mlk_poly_cbd_eta2 LP64 bitwuzla ✅ 18s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d10_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 3s +33%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d11_c LP64 bitwuzla ✅ 8s - new
LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d4_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 4s -50%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d5_c LP64 bitwuzla ✅ 8s - new
LP64 z3* ✅ 3s 4s -25%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 4s -50%
LP64 z3 ✅ 2s - new
mlk_poly_compress_du LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 3s - new
mlk_poly_compress_dv LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
mlk_poly_decompress_d10_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_d11_c LP64 bitwuzla ✅ 8s - new
LP64 z3* ✅ 3s 2s +50%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 14s 16s -12%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d4_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 4s -50%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 4s 3s +33%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d5_c LP64 bitwuzla ✅ 10s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 12s 18s -33%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_du LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s - new
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 3s - new
mlk_poly_frombytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 3s +33%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 11s 10s +10%
LP64 z3 ✅ 1s - new
mlk_poly_frommsg LP64 bitwuzla ✅ 8s - new
LP64 z3* ✅ 2s 10s -80%
mlk_poly_getnoise_eta1122_4x LP64 cvc5_mbqi_enum ✅ 3s - new
LP64 z3* ✅ 1s 3s -67%
mlk_poly_getnoise_eta1122_4x_serial LP64 cvc5_enum_inst ✅ 2s - new
LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta1_4x LP64 cvc5_enum_inst ✅ 78s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_getnoise_eta1_4x_serial LP64 cvc5_enum_inst ✅ 85s - new
LP64 z3* ✅ 2s - new
mlk_poly_getnoise_eta2 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 1s +200%
mlk_poly_invntt_tomont LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_invntt_tomont_c LP64 bitwuzla ✅ 48s - new
LP64 z3* ✅ 4s 2s +100%
mlk_poly_mulcache_compute LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_mulcache_compute_native LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 4s 3s +33%
mlk_poly_ntt LP64 bitwuzla* ✅ 6s 8s -25%
LP64 z3 ✅ 1s - new
mlk_poly_ntt_c LP64 bitwuzla ✅ 69s - new
LP64 z3* ✅ 2s 1s +100%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 3s - new
mlk_poly_reduce_c LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 1s +100%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 35s 40s -12%
LP64 z3 ✅ 2s - new
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 36s 161s -78%
LP64 z3 ✅ 1s - new
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 8s 7s +14%
mlk_poly_sub LP64 bitwuzla ✅ 31s - new
LP64 z3* ✅ 8s 8s +0%
mlk_poly_tobytes LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s - new
mlk_poly_tobytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 4s -50%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 2s - new
mlk_poly_tomont LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 2s +100%
mlk_poly_tomont_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_tomont_native LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 2s 4s -50%
mlk_poly_tomsg LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s - new
mlk_polymat_permute_bitrev_to_custom LP64 cadical ✅ 71s - new
LP64 z3* ✅ 1s 5s -80%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 104s - new
mlk_polyvec_add LP64 cadical ✅ 111s - new
LP64 z3* ✅ 18s 18s +0%
mlk_polyvec_basemul_acc_montgomery_cached LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 cadical ✅ 23s - new
LP64 z3* ⚠️ 126s 79s +59%
mlk_polyvec_compress_du LP64 cadical ✅ 10s - new
LP64 z3* ✅ 3s 3s +0%
mlk_polyvec_decompress_du LP64 cvc5_enum_inst ✅ 7s - new
LP64 z3* ✅ 1s 2s -50%
mlk_polyvec_frombytes LP64 cvc5_enum_inst ✅ 11s - new
LP64 z3* ✅ 3s 5s -40%
mlk_polyvec_invntt_tomont LP64 cvc5_enum_inst ✅ 9s - new
LP64 z3* ✅ 4s 1s +300%
mlk_polyvec_mulcache_compute LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 4s -25%
mlk_polyvec_ntt LP64 cadical ✅ 27s - new
LP64 z3* ✅ 4s 12s -67%
mlk_polyvec_reduce LP64 cvc5_enum_inst ✅ 9s - new
LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_tobytes LP64 cvc5_mbqi_enum ✅ 6s - new
LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_tomont LP64 cvc5_enum_inst ✅ 11s - new
LP64 z3* ✅ 1s 2s -50%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 11s - new
mlk_rej_uniform_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 157s 144s +9%
mlk_scalar_compress_d1 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s 3s -67%
mlk_scalar_compress_d10 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 2s +100%
mlk_scalar_compress_d11 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 4s -50%
mlk_scalar_compress_d4 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 1s +200%
mlk_scalar_compress_d5 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 3s 4s -25%
mlk_scalar_decompress_d10 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d11 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d4 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d5 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s 2s -50%
mlk_scalar_signed_to_unsigned_q LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 3s -33%
mlk_sha3_256 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s - new
mlk_sha3_512 LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 2s - new
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 2s - new
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 1s - new
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_shake256 LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
mlk_shake256x4 LP64 bitwuzla* ✅ 4s 4s +0%
LP64 cvc5_arrays_exp ✅ 29s - new
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 1s - new
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 4s - new
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 2s - new
ntt_native_aarch64 LP64 bitwuzla ✅ 22s - new
LP64 z3* ✅ 2s 3s -33%
ntt_native_x86_64 LP64 bitwuzla ✅ 21s - new
LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 cvc5_enum_inst ✅ 69s - new
LP64 z3* ✅ 2s 2s +0%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 1s - new
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 4s 2s +100%
LP64 z3 ✅ 2s - new
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3 ✅ 2s - new
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 3s - new
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 5s 5s +0%
LP64 z3 ✅ 1s - new
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3 ✅ 2s - new
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3 ✅ 1s - new
poly_invntt_tomont_native LP64 bitwuzla ✅ 7s - new
LP64 z3* ✅ 3s 3s +0%
poly_mulcache_compute_native_aarch64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 5s -40%
poly_ntt_native LP64 bitwuzla ✅ 30s - new
LP64 z3* ✅ 4s 43s -91%
poly_reduce_native_aarch64 LP64 bitwuzla ✅ 13s - new
LP64 z3* ✅ 4s 2s +100%
poly_reduce_native_x86_64 LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 1s 3s -67%
poly_tobytes_native_aarch64 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 3s +0%
poly_tobytes_native_x86_64 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_aarch64 LP64 bitwuzla ✅ 11s - new
LP64 z3* ✅ 2s 3s -33%
poly_tomont_native_x86_64 LP64 bitwuzla ✅ 10s - new
LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_native LP64 cadical ✅ 6s - new
LP64 z3* ✅ 25s 31s -19%
rej_uniform_native LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3_smt_only ✅ 42s - new
rej_uniform_native_aarch64 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 40s 53s -25%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 1s - new
LP64 z3* ⚠️ 112s 67s +67%
sys_check_capability LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 2s +0%

@oqs-bot

oqs-bot commented Oct 25, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2161s 1614s +33.9%
mlk_indcpa_dec LP64 z3* ⚠️ 21s 14s +50%
mlk_ntt_butterfly_block LP64 z3* ⚠️ 353s 9s +3822%
rej_uniform_native_x86_64 LP64 z3* ⚠️ 139s 57s +144%
Full Results (379 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 2161s 1614s +33.9%
intt_native_aarch64 LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 3s 2s +50%
intt_native_x86_64 LP64 bitwuzla ✅ 14s - new
LP64 z3* ✅ 4s 2s +100%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 1s - new
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 4s 3s +33%
LP64 z3 ✅ 2s - new
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 3s - new
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
keccakf1600_permute_native LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 1s - new
keccakf1600x4_permute_native_x4 LP64 bitwuzla* ✅ 17s 16s +6%
LP64 z3 ✅ 16s - new
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 2s - new
kem_check_pk LP64 z3* ✅ 3s 4s -25%
kem_check_sk LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 2s +100%
kem_dec LP64 bitwuzla ✅ 6s - new
LP64 z3* ✅ 9s 5s +80%
kem_enc LP64 bitwuzla ✅ 25s - new
LP64 z3* ✅ 2s 2s +0%
kem_enc_derand LP64 cadical ✅ 12s - new
LP64 z3* ✅ 2s 3s -33%
kem_keypair LP64 cadical ✅ 97s - new
LP64 z3* ✅ 2s 4s -50%
kem_keypair_derand LP64 bitwuzla ✅ 28s - new
LP64 z3* ✅ 1s 3s -67%
mlk_barrett_reduce LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 2s +50%
mlk_check_pct LP64 bitwuzla* ✅ 4s 5s -20%
LP64 z3 ✅ 4s - new
mlk_ct_cmask_neg_i16 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 3s 3s +0%
mlk_ct_cmask_nonzero_u16 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 1s +100%
mlk_ct_cmov_zero LP64 bitwuzla* ✅ 3s 3s +0%
LP64 cvc5_mbqi_enum ✅ 3s - new
mlk_ct_get_optblocker_i32 ILP32 bitwuzla ✅ 2s - new
ILP32 cvc5_arrays_exp ✅ 1s - new
ILP32 z3 ✅ 4s - new
LP64 bitwuzla* ✅ 1s 2s -50%
LP64 cvc5_arrays_exp ✅ 1s - new
LP64 z3 ✅ 2s - new
mlk_ct_get_optblocker_u32 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
mlk_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 4s 2s +100%
LP64 z3 ✅ 1s - new
mlk_ct_memcmp LP64 bitwuzla* ✅ 2s 3s -33%
LP64 cvc5_enum_inst ✅ 4s - new
mlk_ct_sel_int16 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 1s +100%
mlk_ct_sel_uint8 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_enc_getnoise_eta1_eta2 LP64 cvc5_enum_inst ✅ 11s - new
LP64 z3* ✅ 1s 2s -50%
mlk_fqmul LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 4s 17s -76%
mlk_gen_matrix LP64 cadical ✅ 29s - new
LP64 z3* ✅ 2s 2s +0%
mlk_gen_matrix_serial LP64 cadical ✅ 25s - new
LP64 z3* ✅ 4s 3s +33%
mlk_indcpa_dec LP64 cadical ✅ 78s - new
LP64 z3* ⚠️ 21s 14s +50%
mlk_indcpa_enc LP64 z3_smt_only* ✅ 367s 255s +44%
mlk_indcpa_keypair_derand LP64 z3* ✅ 264s 213s +24%
mlk_invntt_layer LP64 bitwuzla ✅ 6s - new
LP64 z3* ✅ 7s 4s +75%
mlk_keccak_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 3s - new
mlk_keccak_absorb_once_x4 LP64 bitwuzla* ✅ 7s 5s +40%
LP64 z3 ✅ 5s - new
mlk_keccak_squeeze_once LP64 bitwuzla* ✅ 7s 8s -12%
LP64 z3 ✅ 43s - new
mlk_keccak_squeezeblocks LP64 bitwuzla* ✅ 8s 9s -11%
LP64 cvc5_arrays_exp ✅ 26s - new
mlk_keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 29s 26s +12%
LP64 cvc5_arrays_exp ✅ 22s - new
mlk_keccakf1600_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
mlk_keccakf1600_extract_bytes (big endian) LP64 bitwuzla* ✅ 2s 5s -60%
LP64 z3 ✅ 1s - new
mlk_keccakf1600_permute LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 1s 1s +0%
mlk_keccakf1600_permute_c LP64 bitwuzla ✅ 5s - new
LP64 z3* ✅ 4s 5s -20%
mlk_keccakf1600_xor_bytes LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 4s - new
mlk_keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 4s 2s +100%
LP64 z3 ✅ 3s - new
mlk_keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 1s - new
mlk_keccakf1600x4_extract_bytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
mlk_keccakf1600x4_permute LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 1s 4s -75%
mlk_keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 2s - new
mlk_keccakf1600x4_xor_bytes_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 2s +50%
mlk_keypair_getnoise_eta1 LP64 cvc5_mbqi_enum ✅ 15s - new
LP64 z3* ✅ 2s 1s +100%
mlk_matvec_mul LP64 cadical ✅ 6s - new
LP64 z3* ✅ 3s 3s +0%
mlk_montgomery_reduce LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 2s +50%
mlk_ntt_butterfly_block LP64 bitwuzla ✅ 17s - new
LP64 z3* ⚠️ 353s 9s +3822%
mlk_ntt_layer LP64 bitwuzla ✅ 37s - new
LP64 z3* ✅ 11s 32s -66%
mlk_poly_add LP64 bitwuzla ✅ 85s - new
LP64 z3* ✅ 4s 4s +0%
mlk_poly_cbd_eta1 LP64 bitwuzla ✅ 13s - new
LP64 z3* ✅ 3s 2s +50%
mlk_poly_cbd_eta2 LP64 bitwuzla ✅ 19s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d10 LP64 bitwuzla* ✅ 3s 4s -25%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d10_c LP64 bitwuzla ✅ 5s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_compress_d10_native LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d11 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
mlk_poly_compress_d11_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_poly_compress_d11_native LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 1s - new
mlk_poly_compress_d4 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 1s - new
mlk_poly_compress_d4_c LP64 bitwuzla ✅ 13s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d4_native LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d5 LP64 bitwuzla* ✅ 5s 2s +150%
LP64 z3 ✅ 3s - new
mlk_poly_compress_d5_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_compress_d5_native LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 2s - new
mlk_poly_compress_du LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s - new
mlk_poly_compress_dv LP64 bitwuzla* ✅ 4s 3s +33%
LP64 z3 ✅ 4s - new
mlk_poly_decompress_d10 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_d10_c LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 4s 4s +0%
mlk_poly_decompress_d10_native LP64 bitwuzla* ✅ 16s 15s +7%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d11 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d11_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_decompress_d11_native LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d4 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_d4_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 7s -57%
mlk_poly_decompress_d4_native LP64 bitwuzla* ✅ 14s 14s +0%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_d5 LP64 bitwuzla* ✅ 1s 1s +0%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_d5_c LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 1s +100%
mlk_poly_decompress_d5_native LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_poly_decompress_du LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 3s - new
mlk_poly_decompress_dv LP64 bitwuzla* ✅ 5s 2s +150%
LP64 z3 ✅ 3s - new
mlk_poly_frombytes LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 1s - new
mlk_poly_frombytes_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 4s +0%
mlk_poly_frombytes_native LP64 bitwuzla* ✅ 14s 8s +75%
LP64 z3 ✅ 4s - new
mlk_poly_frommsg LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 2s 10s -80%
mlk_poly_getnoise_eta1122_4x LP64 cvc5_mbqi_enum ✅ 233s - new
LP64 z3* ✅ 3s 3s +0%
mlk_poly_getnoise_eta1122_4x_serial LP64 cvc5_enum_inst ✅ 15s - new
LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta1_4x LP64 cvc5_enum_inst ✅ 101s - new
LP64 z3* ✅ 2s 5s -60%
mlk_poly_getnoise_eta1_4x_serial LP64 cvc5_enum_inst ✅ 110s - new
LP64 z3* ✅ 3s - new
mlk_poly_getnoise_eta2 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 3s +0%
mlk_poly_invntt_tomont LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_invntt_tomont_c LP64 bitwuzla ✅ 55s - new
LP64 z3* ✅ 3s 3s +0%
mlk_poly_mulcache_compute LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 2s +50%
mlk_poly_mulcache_compute_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 4s 4s +0%
mlk_poly_mulcache_compute_native LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 5s 2s +150%
mlk_poly_ntt LP64 bitwuzla* ✅ 7s 5s +40%
LP64 z3 ✅ 2s - new
mlk_poly_ntt_c LP64 bitwuzla ✅ 82s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_reduce LP64 bitwuzla* ✅ 3s 1s +200%
LP64 z3 ✅ 3s - new
mlk_poly_reduce_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 1s 3s -67%
mlk_poly_reduce_native LP64 bitwuzla* ✅ 42s 35s +20%
LP64 z3 ✅ 7s - new
mlk_poly_rej_uniform LP64 bitwuzla* ✅ 40s 150s -73%
LP64 z3 ✅ 3s - new
mlk_poly_rej_uniform_x4 LP64 z3* ✅ 8s 8s +0%
mlk_poly_sub LP64 bitwuzla ✅ 43s - new
LP64 z3* ✅ 8s 6s +33%
mlk_poly_tobytes LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 1s - new
mlk_poly_tobytes_c LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 3s -33%
mlk_poly_tobytes_native LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 2s - new
mlk_poly_tomont LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 1s +0%
mlk_poly_tomont_c LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_poly_tomont_native LP64 bitwuzla ✅ 17s - new
LP64 z3* ✅ 2s 2s +0%
mlk_poly_tomsg LP64 bitwuzla* ✅ 4s 3s +33%
LP64 z3 ✅ 2s - new
mlk_polymat_permute_bitrev_to_custom LP64 cadical ✅ 13s - new
LP64 z3* ✅ 2s 2s +0%
mlk_polymat_permute_bitrev_to_custom_native LP64 z3* ✅ 35s - new
mlk_polyvec_add LP64 cadical ✅ 66s - new
LP64 z3* ✅ 12s 11s +9%
mlk_polyvec_basemul_acc_montgomery_cached LP64 bitwuzla ✅ 22s - new
LP64 z3* ✅ 3s 1s +200%
mlk_polyvec_basemul_acc_montgomery_cached_c LP64 cadical ✅ 10s - new
LP64 z3* ✅ 78s 55s +42%
mlk_polyvec_compress_du LP64 cadical ✅ 7s - new
LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_decompress_du LP64 cvc5_enum_inst ✅ 4s - new
LP64 z3* ✅ 1s 2s -50%
mlk_polyvec_frombytes LP64 cvc5_enum_inst ✅ 5s - new
LP64 z3* ✅ 2s 2s +0%
mlk_polyvec_invntt_tomont LP64 cvc5_enum_inst ✅ 4s - new
LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_mulcache_compute LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 1s 5s -80%
mlk_polyvec_ntt LP64 cadical ✅ 14s - new
LP64 z3* ✅ 2s 1s +100%
mlk_polyvec_reduce LP64 cvc5_enum_inst ✅ 5s - new
LP64 z3* ✅ 3s 2s +50%
mlk_polyvec_tobytes LP64 cvc5_mbqi_enum ✅ 5s - new
LP64 z3* ✅ 2s 3s -33%
mlk_polyvec_tomont LP64 cvc5_enum_inst ✅ 6s - new
LP64 z3* ✅ 1s 1s +0%
mlk_rej_uniform LP64 bitwuzla* ✅ 2s 5s -60%
LP64 z3 ✅ 15s - new
mlk_rej_uniform_c LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 188s 135s +39%
mlk_scalar_compress_d1 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 2s -50%
mlk_scalar_compress_d10 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d11 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 2s +0%
mlk_scalar_compress_d4 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 4s 1s +300%
mlk_scalar_compress_d5 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 3s 2s +50%
mlk_scalar_decompress_d10 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 1s 2s -50%
mlk_scalar_decompress_d11 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 2s 2s +0%
mlk_scalar_decompress_d4 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 2s 3s -33%
mlk_scalar_decompress_d5 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 3s -33%
mlk_scalar_signed_to_unsigned_q LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 2s 1s +100%
mlk_sha3_256 LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 1s - new
mlk_sha3_512 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 3s - new
mlk_shake128_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 3s - new
mlk_shake128_squeezeblocks LP64 bitwuzla* ✅ 1s 3s -67%
LP64 z3 ✅ 2s - new
mlk_shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
LP64 z3 ✅ 3s - new
mlk_shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
mlk_shake256 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 4s - new
mlk_shake256x4 LP64 bitwuzla* ✅ 4s 5s -20%
LP64 cvc5_arrays_exp ✅ 35s - new
mlk_value_barrier_i32 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 1s - new
mlk_value_barrier_u32 LP64 bitwuzla* ✅ 2s 3s -33%
LP64 z3 ✅ 2s - new
mlk_value_barrier_u8 LP64 bitwuzla* ✅ 1s 4s -75%
LP64 z3 ✅ 2s - new
ntt_native_aarch64 LP64 bitwuzla ✅ 25s - new
LP64 z3* ✅ 2s 2s +0%
ntt_native_x86_64 LP64 bitwuzla ✅ 24s - new
LP64 z3* ✅ 3s 2s +50%
nttunpack_native_x86_64 LP64 cvc5_enum_inst ✅ 76s - new
LP64 z3* ✅ 4s 2s +100%
poly_compress_d10_native_x86_64 LP64 bitwuzla* ✅ 3s 3s +0%
LP64 z3 ✅ 2s - new
poly_compress_d11_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 4s - new
poly_compress_d4_native_x86_64 LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 3s - new
poly_compress_d5_native_x86_64 LP64 bitwuzla* ✅ 3s 2s +50%
LP64 z3 ✅ 3s - new
poly_decompress_d10_native_x86_64 LP64 bitwuzla* ✅ 4s 9s -56%
LP64 z3 ✅ 3s - new
poly_decompress_d11_native_x86_64 LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3 ✅ 2s - new
poly_decompress_d4_native_x86_64 LP64 bitwuzla* ✅ 5s 4s +25%
LP64 z3 ✅ 4s - new
poly_decompress_d5_native_x86_64 LP64 bitwuzla* ✅ 2s 2s +0%
LP64 z3 ✅ 4s - new
poly_frombytes_native_x86_64 LP64 bitwuzla* ✅ 6s 5s +20%
LP64 z3 ✅ 3s - new
poly_invntt_tomont_native LP64 bitwuzla ✅ 9s - new
LP64 z3* ✅ 2s 2s +0%
poly_mulcache_compute_native_aarch64 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 2s 3s -33%
poly_mulcache_compute_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 1s 1s +0%
poly_ntt_native LP64 bitwuzla ✅ 37s - new
LP64 z3* ✅ 2s 45s -96%
poly_reduce_native_aarch64 LP64 bitwuzla ✅ 12s - new
LP64 z3* ✅ 4s 1s +300%
poly_reduce_native_x86_64 LP64 bitwuzla ✅ 16s - new
LP64 z3* ✅ 3s 2s +50%
poly_tobytes_native_aarch64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 4s 2s +100%
poly_tobytes_native_x86_64 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 3s 1s +200%
poly_tomont_native_aarch64 LP64 bitwuzla ✅ 14s - new
LP64 z3* ✅ 1s 2s -50%
poly_tomont_native_x86_64 LP64 bitwuzla ✅ 13s - new
LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 4s 3s +33%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 LP64 bitwuzla ✅ 4s - new
LP64 z3* ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_native LP64 cadical ✅ 8s - new
LP64 z3* ✅ 10s 8s +25%
rej_uniform_native LP64 bitwuzla* ✅ 2s 1s +100%
LP64 z3_smt_only ✅ 44s - new
rej_uniform_native_aarch64 LP64 bitwuzla ✅ 1s - new
LP64 z3* ✅ 50s 43s +16%
rej_uniform_native_x86_64 LP64 bitwuzla ✅ 2s - new
LP64 z3* ⚠️ 139s 57s +144%
sys_check_capability LP64 bitwuzla ✅ 3s - new
LP64 z3* ✅ 2s 1s +100%

@mkannwischer
mkannwischer added this pull request to the merge queue Oct 26, 2026
Merged via the queue into main with commit 8ef496a Oct 26, 2026
361 checks passed
@mkannwischer
mkannwischer deleted the port-gh-pages branch October 26, 2026 06:31
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

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Port: CBMC: Push performance data to gh-pages

3 participants

@hanno-becker @oqs-bot @mkannwischer