Skip to content

New 3-way batched Keccak-f1600 (x3) improves ML-DSA performance by 2.5 to 13.0% on Neoverse V3 - #1489

Draft
soumya2094 wants to merge 8 commits into
mainfrom
x3-hybrid-keccak-f1600
Draft

New 3-way batched Keccak-f1600 (x3) improves ML-DSA performance by 2.5 to 13.0% on Neoverse V3#1489
soumya2094 wants to merge 8 commits into
mainfrom
x3-hybrid-keccak-f1600

Conversation

@soumya2094

@soumya2094 soumya2094 commented Oct 21, 2026

Copy link
Copy Markdown

This PR adds a new 3-way Keccak-f1600 batching (x3) for Neoverse V3 cores by exploiting the optimized SHA3 hashing. It is aimed at cores that execute the Armv8.4-A SHA3 instructions on all SIMD pipes (e.g. Neoverse V3). It is off by default (MLD_CONFIG_USE_X3). The assembly and its HOL Light proof are included.

The PR also makes mldsa-native's FIPS202 AArch64 development tree structurally consistent with mlkem-native: it adds the symbolic (clean) Keccak-f1600 sources in dev/fips202/aarch64_symbolic/ and the SLOTHY recipes in dev/fips202/aarch64/src/Makefile, and enables autogen --slothy for the Keccak kernels. With this, the existing x4 kernels and the new x3 kernel can be regenerated from their symbolic sources, reproducing the committed machine code exactly.

What it adds

  • Kernel keccak_f1600_x3_v8a_v84a_scalar_hybrid_aarch64_asm: two Keccak states on Neon (SHA3 instructions), one state on scalar registers with lazy rotations, one scalar and one vector round per iteration in a single pass. Scheduled with SLOTHY (interleaving only) from the symbolic source dev/fips202/aarch64_symbolic/keccak_f1600_x3_v8a_v84a_scalar_hybrid_clean.S; the recipe is in dev/fips202/aarch64/src/Makefile (autogen --slothy keccak_f1600_x3_v8a_v84a_scalar_hybrid_aarch64_asm) and regenerates the committed kernel.
  • HOL Light proof (proofs/hol_light/aarch64/proofs/keccak_f1600_x3_v8a_v84a_scalar_hybrid_aarch64_asm.ml):
    • Correctness (_CORRECT, _SUBROUTINE_CORRECT): the kernel computes the full 24-round Keccak-f[1600] permutation on each of the three 200-byte states. Called as a C function, it also preserves all registers the calling convention requires and writes no memory other than the 600-byte state buffer and its own 224-byte stack frame.
    • _SUBROUTINE_SAFE: memory safety and secret-independent timing (mk_safety_spec), with an x3 entry sha3_keccak3_f1600_alt in subroutine_signatures.ml, named similar to the existing x4 entry sha3_keccak4_f1600_alt.
  • 3-way FIPS202 layer: x3 permute/xor/extract primitives (C fallback: 3× serial), 3-way SHAKE128/256, backend header x3_v8a_v84a_scalar.h, selection in auto.h under MLD_CONFIG_USE_X3.
  • Samplers: ExpandA, ExpandS and ExpandMask batch 3 polynomials per XOF call with MLD_CONFIG_USE_X3. Every polynomial keeps its FIPS 204 nonce, so outputs are byte-identical to the default path.
  • CBMC: proofs for the new C functions (19 proof directories), all passing for ML-DSA-44/65/87 with and without MLD_CONFIG_REDUCE_RAM.
  • Tests/benchmarks: test/configs/x3_keccak_config.h; component benchmark rows for the x3 permute and samplers, plus x4 baselines (keccakf1600x4_permute, poly_uniform_4x, poly_uniform_gamma1_4x).
  • CI: an x3-keccak config variation (native x3 on AArch64, C fallback elsewhere) and x3_v8a_v84a_scalar in the AArch64 backend matrix.

Commits (each builds and passes format / autogen / func / KAT / examples):

  1. FIPS202/AArch64: Add symbolic Keccak sources and SLOTHY Makefile (structurally consistent with mlkem-native)
  2. FIPS202: Add 3-way batched Keccak-f1600 with an AArch64 hybrid backend
  3. HOL-Light: Prove the x3 hybrid Keccak-f1600 kernel
  4. Batch ExpandA, ExpandS and ExpandMask 3-way with MLD_CONFIG_USE_X3
  5. tests: Add an x3 test configuration and x3 component benchmarks
  6. CBMC: Add proofs for the 3-way batched Keccak and x3 samplers
  7. CI: Test the 3-way batched Keccak (x3) configuration

Notes on Commit 0: FIPS202 symbolic sources and SLOTHY recipes (parity with mlkem-native)

The mldsa-native did not carry the symbolic/clean sources from which its AArch64 Keccak-f1600 kernels are generated, nor the SLOTHY recipes. The autogen --slothy had a keccak code path that could not be reached. This commit brings the FIPS202 AArch64 tree in line with mlkem-native (commit a7914d4):

  • dev/fips202/aarch64_symbolic/: keccak_f1600_x1_scalar_symbolic.S, keccak_f1600_x4_v8a_scalar_hybrid_clean.S, keccak_f1600_x4_v8a_v84a_scalar_hybrid_clean.S.
  • dev/fips202/aarch64/src/Makefile: mlkem-native's slothy-cli recipes ported over to mldsa-native.
  • scripts/autogen: the three kernels added to --slothy, similar to mlkem-native.

The shipped kernels are unchanged. Running autogen --slothy with these recipes regenerates kernels similar to the committed ones.

Testing

  • KAT, func, unit, alloc, sign_hook, rng_fail, ACVP and abicheck pass with and without MLD_CONFIG_USE_X3 on Neoverse V1, V2 and V3 (native AArch64). On x86_64, where there is no x3 assembly and the 3-way permutation falls back to three calls of the C permutation, func and KAT pass with and without MLD_CONFIG_USE_X3.
  • Default builds compile only the x4 batched path and link only the x4 kernel; MLD_CONFIG_USE_X3 builds compile only the x3 path and link only the x3 kernel.
  • scripts/lint, scripts/format, autogen --dry-run clean.

Performance (pinned to one core)

Per component (bench_components), x3 vs x4 per polynomial / per state (an x3 call handles 3, an x4 call 4; cycles per call for ML-DSA-87 in brackets, x3 vs x4). Neoverse V3: median of 5 runs; V2/V1: one run:

Component Neoverse V3 (44 / 65 / 87) Neoverse V2 (87) Neoverse V1 (87)
Keccak-f1600 permute −26.1% / −26.1% / −26.1% (531 vs 958) +48.6% (1553 vs 1393) +39.2% (1559 vs 1493)
ExpandA (poly_uniform_3x vs _4x) −10.3% / −9.8% / −9.8% (4441 vs 6565) +40.5% (9344 vs 8870) +23.9% (9629 vs 10363)
ExpandS (poly_uniform_eta_3x vs _4x) −16.1% / −14.3% / −14.1% (2180 vs 3383) +34.6% (4203 vs 4164) +20.7% (4325 vs 4779)
ExpandMask (poly_uniform_gamma1_3x vs _4x) −22.5% / −22.5% / −22.6% (3198 vs 5508) +46.2% (8448 vs 7702) +34.9% (8440 vs 8343)

End to end, x3 vs x4 (KeyGen/Verify: bench_mldsa average; Sign: change in median cycles over 20,000 signs with identical key/message/randomness in both builds, paired Wilcoxon signed-rank p < 0.001):

Core KeyGen 44 / 65 / 87 Sign 44 / 65 / 87 Verify 44 / 65 / 87
Neoverse V3 −5.3% / −13.0% / −8.9% −2.5% / −6.6% / −5.7% −6.1% / −11.6% / −6.8%
Neoverse V2 +31.2% / +25.9% / +30.8% +21.1% / +21.3% / +21.2% +22.4% / +20.8% / +28.2%
Neoverse V1 +18.9% / +13.7% / +18.0% +11.7% / +10.7% / +11.4% +14.3% / +11.5% / +17.5%

x3 only pays off where SHA3 runs on all SIMD pipes (Neoverse V3); elsewhere it is slower, hence opt-in only.

Reproduce: make bench_components_87 OPT=1 AUTO=1 CYCLES=PERF and make bench_87 …, once with the default config and once with -DMLD_CONFIG_USE_X3.

Feedback welcome

x3 is enabled with the config option MLD_CONFIG_USE_X3 (off by default). Note that the option also switches ExpandA/ExpandS/ExpandMask to 3-way batching on other platforms; on Neoverse V1 and V2 the default x4 is faster, and without a native x3 kernel the 3-way Keccak runs as three single-state permutations. Feedback on the C integration approach is welcome. The current implementation is functional, but the 3-way FIPS202 layer and samplers largely duplicate their 4-way counterparts; a single code path parameterised by the batch width (3 or 4) would be preferable, and suggestions on this proposal are welcome.

@oqs-bot

oqs-bot commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 33s 7s +371%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 166s 31s +435%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 5s +500%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 180s 71s +154%
Full Results (245 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1292s 1482s -12.8%
caddq LP64 z3* ✅ 1s 2s -50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 33s 7s +371%
decompose LP64 z3* ✅ 3s 4s -25%
fqmul LP64 bitwuzla* ✅ 22s 40s -45%
fqscale LP64 bitwuzla* ✅ 1s 3s -67%
intt_native_aarch64 LP64 z3* ✅ 3s 2s +50%
intt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 2s 4s -50%
keccak_absorb LP64 z3* ✅ 3s 3s +0%
keccak_absorb_once_x3 LP64 bitwuzla* ✅ 4s - new
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 3s 10s -70%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x3_native_aarch64_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_finalize LP64 z3* ✅ 2s 2s +0%
keccak_init LP64 z3* ✅ 5s 4s +25%
keccak_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
keccak_squeezeblocks_x3 LP64 bitwuzla* ✅ 3s - new
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 3s 3s +0%
keccakf1600_permute LP64 z3* ✅ 1s 4s -75%
keccakf1600_permute_native LP64 z3* ✅ 2s 2s +0%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x3_extract_bytes LP64 bitwuzla* ✅ 1s - new
keccakf1600x3_extract_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x3_permute LP64 z3* ✅ 3s - new
keccakf1600x3_permute_native LP64 z3* ✅ 9s - new
keccakf1600x3_xor_bytes LP64 bitwuzla* ✅ 2s - new
keccakf1600x3_xor_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 2s 1s +100%
keccakf1600x4_permute LP64 z3* ✅ 3s 1s +200%
keccakf1600x4_permute_native LP64 z3* ✅ 13s 22s -41%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
make_hint LP64 z3* ✅ 3s 3s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 166s 31s +435%
mld_check_pct LP64 z3* ✅ 4s 12s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 2s 5s -60%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 6s -83%
ILP32 cvc5_arrays_exp ✅ 2s 6s -67%
ILP32 z3 ✅ 1s 6s -83%
LP64 bitwuzla ✅ 1s 6s -83%
LP64 cvc5_arrays_exp ✅ 1s 6s -83%
LP64 z3* ✅ 1s 6s -83%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 3s 1s +200%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 2s 4s -50%
mld_ct_memcmp LP64 bitwuzla* ✅ 2s 4s -50%
mld_ct_sel_int32 LP64 z3* ✅ 2s 2s +0%
mld_h LP64 z3* ✅ 2s 3s -33%
mld_invntt_layer LP64 bitwuzla* ✅ 58s 108s -46%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 4s 7s -43%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 10s 25s -60%
mld_ntt_layer LP64 bitwuzla* ✅ 24s 43s -44%
mld_polymat_expand_entry LP64 z3* ✅ 1s 3s -67%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 4s -25%
mld_sample_pack_s1_s2 LP64 z3* ✅ 5s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 5s - new
mld_sign_attempt LP64 z3* ✅ 1s - new
mld_sign_finish LP64 z3* ✅ 4s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 4s 4s +0%
mld_value_barrier_u8 LP64 z3* ✅ 3s 1s +200%
montgomery_reduce LP64 z3* ✅ 2s 1s +100%
ntt_native_aarch64 LP64 z3* ✅ 1s 3s -67%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 4s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_x86_64 LP64 z3* ✅ 1s 5s -80%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
pack_sig_c LP64 z3* ✅ 1s 3s -67%
pack_sig_h LP64 z3_no_bv_extract* ✅ 1s 2s -50%
pack_sig_z LP64 z3* ✅ 2s 1s +100%
pack_sk_rho_key_tr LP64 z3* ✅ 2s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 6s -50%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 5s 5s +0%
pointwise_native_aarch64 LP64 z3* ✅ 1s 3s -67%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 z3* ✅ 3s 2s +50%
poly_add LP64 z3* ✅ 3s 7s -57%
poly_caddq LP64 z3* ✅ 1s 3s -67%
poly_caddq_c LP64 z3* ✅ 4s 5s -20%
poly_caddq_native LP64 z3* ✅ 1s 4s -75%
poly_caddq_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_caddq_native_x86_64 LP64 z3* ✅ 1s 1s +0%
poly_challenge LP64 z3* ✅ 1s 5s -80%
poly_chknorm LP64 z3* ✅ 2s 3s -33%
poly_chknorm_c LP64 z3* ✅ 7s 13s -46%
poly_chknorm_native LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_chknorm_native_x86_64 LP64 z3* ✅ 3s 4s -25%
poly_decompose LP64 z3* ✅ 1s 2s -50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_decompose_c LP64 z3* ✅ 4s 8s -50%
poly_decompose_native LP64 z3* ✅ 2s 5s -60%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont LP64 z3* ✅ 3s 5s -40%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 10s -30%
poly_invntt_tomont_native LP64 z3* ✅ 3s 5s -40%
poly_ntt LP64 z3* ✅ 2s 2s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 9s 22s -59%
poly_ntt_native LP64 z3* ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 2s 3s -33%
poly_pointwise_montgomery LP64 z3* ✅ 1s 2s -50%
poly_pointwise_montgomery_c LP64 z3* ✅ 68s 116s -41%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 4s -25%
poly_power2round LP64 z3* ✅ 4s 7s -43%
poly_reduce LP64 z3* ✅ 2s 4s -50%
poly_shiftl LP64 z3* ✅ 2s 3s -33%
poly_sub LP64 z3* ✅ 3s 4s -25%
poly_uniform LP64 z3* ✅ 3s 2s +50%
poly_uniform_3x LP64 z3* ✅ 2s - new
poly_uniform_4x LP64 z3* ✅ 2s 4s -50%
poly_uniform_eta LP64 z3* ✅ 1s 5s -80%
poly_uniform_eta_3x LP64 z3* ✅ 5s - new
poly_uniform_eta_4x LP64 z3* ✅ 7s 13s -46%
poly_uniform_gamma1 LP64 z3* ✅ 4s 3s +33%
poly_uniform_gamma1_3x LP64 z3* ✅ 2s - new
poly_uniform_gamma1_4x LP64 z3* ✅ 3s 3s +0%
poly_use_hint LP64 z3* ✅ 2s 3s -33%
poly_use_hint_c LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native LP64 z3* ✅ 4s 7s -43%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 4s -25%
poly_use_hint_native_x86_64 LP64 z3* ✅ 1s - new
polyeta_pack LP64 z3* ✅ 2s 1s +100%
polyeta_unpack LP64 z3* ✅ 3s 4s -25%
polyt0_pack LP64 z3* ✅ 1s 5s -80%
polyt0_unpack LP64 z3* ✅ 6s 13s -54%
polyt1_pack LP64 z3* ✅ 1s 3s -67%
polyt1_unpack LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 6s -83%
polyvec_matrix_expand_serial LP64 z3* ✅ 2s 3s -33%
polyvec_matrix_expand_x3 LP64 z3_no_bv_extract* ✅ 3s - new
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 4s 8s -50%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 102s 201s -49%
polyveck_caddq LP64 z3* ✅ 3s 7s -57%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 7s -43%
polyveck_ntt LP64 z3* ✅ 1s 4s -75%
polyveck_reduce LP64 z3* ✅ 2s 6s -67%
polyveck_unpack_eta LP64 z3* ✅ 2s 3s -33%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 1s - new
polyvecl_chknorm LP64 z3* ✅ 4s 43s -91%
polyvecl_ntt LP64 z3* ✅ 3s 7s -57%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 5s 3s +67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 1s +100%
polyvecl_uniform_gamma1_x3 LP64 z3* ✅ 1s - new
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 2s 1s +100%
polyw1_pack LP64 z3* ✅ 4s 3s +33%
polyw1_pack_32 LP64 z3* ✅ 2s 2s +0%
polyw1_pack_88 LP64 z3* ✅ 1s 3s -67%
polyw1_unpack LP64 z3* ✅ 4s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 2s 3s -33%
polyz_unpack LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 1s 5s -80%
polyz_unpack_c LP64 z3* ✅ 4s 9s -56%
polyz_unpack_native LP64 z3* ✅ 1s 3s -67%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 3s 2s +50%
reduce32 LP64 z3* ✅ 1s 2s -50%
rej_eta LP64 bitwuzla* ✅ 1s 5s -80%
rej_eta_c LP64 bitwuzla* ✅ 4s 4s +0%
rej_eta_native LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform LP64 z3* ✅ 4s 7s -43%
rej_uniform_c LP64 z3* ✅ 8s 16s -50%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 1s 5s -80%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 3s - new
rej_uniform_native LP64 bitwuzla* ✅ 1s 4s -75%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 3s 5s -40%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 9s - new
sample_pack_s1_s2_x3 LP64 z3* ✅ 3s - new
shake128_absorb LP64 z3* ✅ 1s 2s -50%
shake128_finalize LP64 z3* ✅ 2s 2s +0%
shake128_init LP64 z3* ✅ 1s 6s -83%
shake128_release LP64 z3* ✅ 1s 2s -50%
shake128_squeeze LP64 bitwuzla* ✅ 2s 3s -33%
shake128x3_absorb_once LP64 bitwuzla* ✅ 1s - new
shake128x3_squeezeblocks LP64 bitwuzla* ✅ 2s - new
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
shake256 LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 z3* ✅ 1s 4s -75%
shake256_finalize LP64 z3* ✅ 1s 1s +0%
shake256_init LP64 z3* ✅ 1s 4s -75%
shake256_release LP64 z3* ✅ 4s 3s +33%
shake256_squeeze LP64 bitwuzla* ✅ 2s 4s -50%
shake256x3_absorb_once LP64 bitwuzla* ✅ 1s - new
shake256x3_squeezeblocks LP64 bitwuzla* ✅ 3s - new
shake256x4_absorb_once LP64 bitwuzla* ✅ 2s 2s +0%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
sig_unpack_hints LP64 z3* ✅ 13s 1s +1200%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 16s 3s +433%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 5s +500%
sign_signature LP64 z3* ✅ 2s 5s -60%
sign_signature_extmu LP64 z3* ✅ 2s 4s -50%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 16s 6s +167%
sign_signature_pre_hash_internal LP64 z3* ✅ 4s 3s +33%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 4s 7s -43%
sign_verify LP64 z3* ✅ 3s 6s -50%
sign_verify_extmu LP64 z3* ✅ 3s 2s +50%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 180s 71s +154%
sign_verify_pre_hash_internal LP64 z3* ✅ 4s 5s -20%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 6s -67%
sk_s1hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 1s 1s +0%
sk_t0hat_get_poly LP64 z3* ✅ 3s 1s +200%
sys_check_capability LP64 z3* ✅ 2s 1s +100%
unpack_pk_t1 LP64 z3* ✅ 2s 2s +0%
unpack_sk LP64 z3* ✅ 2s 3s -33%
unpack_sk_s1hat LP64 z3* ✅ 3s 1s +200%
unpack_sk_s2hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_t0hat LP64 z3* ✅ 3s 4s -25%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 1s 3s -67%
yvec_init LP64 z3* ✅ 2s 5s -60%

@oqs-bot

oqs-bot commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 32s 12s +167%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 142s 19s +647%
sig_unpack_hints LP64 z3* ⚠️ 37s 2s +1750%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 5s +500%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 249s 49s +408%
Full Results (245 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1420s 1364s +4.1%
caddq LP64 z3* ✅ 2s 6s -67%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 32s 12s +167%
decompose LP64 z3* ✅ 1s 3s -67%
fqmul LP64 bitwuzla* ✅ 24s 39s -38%
fqscale LP64 bitwuzla* ✅ 1s 2s -50%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 4s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
intt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x3 LP64 bitwuzla* ✅ 5s - new
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 8s -50%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 5s 2s +150%
keccak_f1600_x3_native_aarch64_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 3s 2s +50%
keccak_finalize LP64 z3* ✅ 1s 2s -50%
keccak_init LP64 z3* ✅ 3s 3s +0%
keccak_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
keccak_squeezeblocks_x3 LP64 bitwuzla* ✅ 3s - new
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 4s -75%
keccakf1600_permute LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute_native LP64 z3* ✅ 3s 3s +0%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 6s -83%
keccakf1600x3_extract_bytes LP64 bitwuzla* ✅ 2s - new
keccakf1600x3_extract_bytes_c LP64 z3* ✅ 2s - new
keccakf1600x3_permute LP64 z3* ✅ 2s - new
keccakf1600x3_permute_native LP64 z3* ✅ 10s - new
keccakf1600x3_xor_bytes LP64 bitwuzla* ✅ 2s - new
keccakf1600x3_xor_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 4s -75%
keccakf1600x4_permute LP64 z3* ✅ 1s 4s -75%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 22s -45%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 3s 5s -40%
make_hint LP64 z3* ✅ 2s 3s -33%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 142s 19s +647%
mld_check_pct LP64 z3* ✅ 5s 15s -67%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 6s -33%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 5s 3s +67%
ILP32 cvc5_arrays_exp ✅ 1s 3s -67%
ILP32 z3 ✅ 1s 3s -67%
LP64 bitwuzla ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 1s 3s -67%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 4s -50%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 1s +0%
mld_ct_sel_int32 LP64 z3* ✅ 1s 3s -67%
mld_h LP64 z3* ✅ 4s 4s +0%
mld_invntt_layer LP64 bitwuzla* ✅ 66s 105s -37%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 2s 2s +0%
mld_keccakf1600_permute_c LP64 z3* ✅ 5s 7s -29%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 4s -75%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 1s 4s -75%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 14s 23s -39%
mld_ntt_layer LP64 bitwuzla* ✅ 24s 41s -41%
mld_polymat_expand_entry LP64 z3* ✅ 4s 2s +100%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 3s +0%
mld_sample_pack_s1_s2 LP64 z3* ✅ 3s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 2s - new
mld_sign_attempt LP64 z3* ✅ 1s - new
mld_sign_finish LP64 z3* ✅ 4s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 3s -33%
mld_value_barrier_u32 LP64 z3* ✅ 2s 1s +100%
mld_value_barrier_u8 LP64 z3* ✅ 2s 4s -50%
montgomery_reduce LP64 z3* ✅ 3s 2s +50%
ntt_native_aarch64 LP64 z3* ✅ 2s 4s -50%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 4s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 4s -50%
pack_sig_c LP64 z3* ✅ 1s 5s -80%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 4s -50%
pack_sig_z LP64 z3* ✅ 2s 2s +0%
pack_sk_rho_key_tr LP64 z3* ✅ 2s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 4s +0%
pointwise_native_aarch64 LP64 z3* ✅ 2s 2s +0%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 4s 4s +0%
poly_add LP64 z3* ✅ 3s 7s -57%
poly_caddq LP64 z3* ✅ 4s 4s +0%
poly_caddq_c LP64 z3* ✅ 5s 3s +67%
poly_caddq_native LP64 z3* ✅ 2s 3s -33%
poly_caddq_native_aarch64 LP64 z3* ✅ 1s 3s -67%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_challenge LP64 z3* ✅ 1s 6s -83%
poly_chknorm LP64 z3* ✅ 4s 3s +33%
poly_chknorm_c LP64 z3* ✅ 8s 11s -27%
poly_chknorm_native LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 z3* ✅ 1s 2s -50%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_decompose_c LP64 z3* ✅ 3s 5s -40%
poly_decompose_native LP64 z3* ✅ 1s 2s -50%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 7s 11s -36%
poly_invntt_tomont_native LP64 z3* ✅ 2s 3s -33%
poly_ntt LP64 z3* ✅ 3s 3s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 10s 21s -52%
poly_ntt_native LP64 z3* ✅ 1s 3s -67%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 5s -60%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery_c LP64 z3* ✅ 76s 112s -32%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 2s -50%
poly_power2round LP64 z3* ✅ 2s 4s -50%
poly_reduce LP64 z3* ✅ 1s 4s -75%
poly_shiftl LP64 z3* ✅ 3s 4s -25%
poly_sub LP64 z3* ✅ 1s 3s -67%
poly_uniform LP64 z3* ✅ 3s 3s +0%
poly_uniform_3x LP64 z3* ✅ 5s - new
poly_uniform_4x LP64 z3* ✅ 2s 3s -33%
poly_uniform_eta LP64 z3* ✅ 3s 2s +50%
poly_uniform_eta_3x LP64 z3* ✅ 6s - new
poly_uniform_eta_4x LP64 z3* ✅ 8s 12s -33%
poly_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
poly_uniform_gamma1_3x LP64 z3* ✅ 1s - new
poly_uniform_gamma1_4x LP64 z3* ✅ 2s 5s -60%
poly_use_hint LP64 z3* ✅ 2s 2s +0%
poly_use_hint_c LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_aarch64 LP64 z3* ✅ 4s 3s +33%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 2s 3s -33%
polyeta_unpack LP64 z3* ✅ 7s 14s -50%
polyt0_pack LP64 z3* ✅ 1s 4s -75%
polyt0_unpack LP64 z3* ✅ 8s 12s -33%
polyt1_pack LP64 z3* ✅ 3s 3s +0%
polyt1_unpack LP64 z3* ✅ 2s 2s +0%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 1s 3s -67%
polyvec_matrix_expand_serial LP64 z3* ✅ 3s 4s -25%
polyvec_matrix_expand_x3 LP64 z3_no_bv_extract* ✅ 2s - new
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 6s 6s +0%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 122s 149s -18%
polyveck_caddq LP64 z3* ✅ 2s 3s -33%
polyveck_decompose_pack_w1 LP64 z3* ✅ 6s - 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 z3* ✅ 3s 2s +50%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 2s 11s -82%
polyvecl_ntt LP64 z3* ✅ 6s 3s +100%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 1s 3s -67%
polyvecl_uniform_gamma1 LP64 z3* ✅ 1s 2s -50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 4s 2s +100%
polyvecl_uniform_gamma1_x3 LP64 z3* ✅ 2s - new
polyvecl_unpack_eta LP64 z3* ✅ 1s 4s -75%
polyvecl_unpack_z LP64 z3* ✅ 4s 3s +33%
polyw1_pack LP64 z3* ✅ 3s 4s -25%
polyw1_pack_32 LP64 z3* ✅ 2s 3s -33%
polyw1_pack_88 LP64 z3* ✅ 2s 2s +0%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 3s - new
polyw1_unpack_88 LP64 z3* ✅ 6s - new
polyz_pack LP64 z3* ✅ 4s 2s +100%
polyz_unpack LP64 z3* ✅ 3s 3s +0%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 2s +0%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_c LP64 z3* ✅ 6s 8s -25%
polyz_unpack_native LP64 z3* ✅ 3s 3s +0%
polyz_unpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
power2round LP64 z3* ✅ 1s 2s -50%
reduce32 LP64 z3* ✅ 1s 3s -67%
rej_eta LP64 bitwuzla* ✅ 3s 5s -40%
rej_eta_c LP64 bitwuzla* ✅ 4s 4s +0%
rej_eta_native LP64 bitwuzla* ✅ 4s 3s +33%
rej_uniform LP64 z3* ✅ 4s 8s -50%
rej_uniform_c LP64 z3* ✅ 10s 16s -38%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 3s -33%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 3s 5s -40%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 9s - new
sample_pack_s1_s2_x3 LP64 z3* ✅ 5s - new
shake128_absorb LP64 z3* ✅ 1s 3s -67%
shake128_finalize LP64 z3* ✅ 1s 3s -67%
shake128_init LP64 z3* ✅ 2s 2s +0%
shake128_release LP64 z3* ✅ 2s 2s +0%
shake128_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake128x3_absorb_once LP64 bitwuzla* ✅ 2s - new
shake128x3_squeezeblocks LP64 bitwuzla* ✅ 3s - new
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 2s -50%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
shake256 LP64 z3* ✅ 2s 1s +100%
shake256_absorb LP64 z3* ✅ 3s 2s +50%
shake256_finalize LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 z3* ✅ 2s 4s -50%
shake256_release LP64 z3* ✅ 1s 1s +0%
shake256_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake256x3_absorb_once LP64 bitwuzla* ✅ 3s - new
shake256x3_squeezeblocks LP64 bitwuzla* ✅ 3s - new
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 1s +0%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 2s 2s +0%
sig_unpack_hints LP64 z3* ⚠️ 37s 2s +1750%
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* ⚠️ 30s 5s +500%
sign_signature LP64 z3* ✅ 2s 6s -67%
sign_signature_extmu LP64 z3* ✅ 4s 4s +0%
sign_signature_internal LP64 z3_no_bv_extract* ✅ 14s 4s +250%
sign_signature_pre_hash_internal LP64 z3* ✅ 1s 4s -75%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 2s 4s -50%
sign_verify LP64 z3* ✅ 4s 4s +0%
sign_verify_extmu LP64 z3* ✅ 2s 5s -60%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 249s 49s +408%
sign_verify_pre_hash_internal LP64 z3* ✅ 2s 5s -60%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 4s 5s -20%
sk_s1hat_get_poly LP64 z3* ✅ 2s 2s +0%
sk_s2hat_get_poly LP64 z3* ✅ 2s 5s -60%
sk_t0hat_get_poly LP64 z3* ✅ 1s 1s +0%
sys_check_capability LP64 z3* ✅ 2s 2s +0%
unpack_pk_t1 LP64 z3* ✅ 3s 3s +0%
unpack_sk LP64 z3* ✅ 1s 3s -67%
unpack_sk_s1hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_s2hat LP64 z3* ✅ 1s 4s -75%
unpack_sk_t0hat LP64 z3* ✅ 2s 2s +0%
use_hint LP64 z3* ✅ 3s 2s +50%
yvec_get_poly LP64 z3* ✅ 1s 3s -67%
yvec_init LP64 z3* ✅ 2s 1s +100%

@oqs-bot

oqs-bot commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 80s 50s +60%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 311s 58s +436%
sig_unpack_hints LP64 z3* ⚠️ 23s 2s +1050%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 26s 5s +420%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 193s 26s +642%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 294s 114s +158%
Full Results (245 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1801s 1514s +19.0%
caddq LP64 z3* ✅ 3s 2s +50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 80s 50s +60%
decompose LP64 z3* ✅ 3s 2s +50%
fqmul LP64 bitwuzla* ✅ 23s 39s -41%
fqscale LP64 bitwuzla* ✅ 2s 3s -33%
intt_native_aarch64 LP64 z3* ✅ 2s 9s -78%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 5s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
intt_native_x86_64 LP64 z3* ✅ 3s 4s -25%
keccak_absorb LP64 z3* ✅ 3s 5s -40%
keccak_absorb_once_x3 LP64 bitwuzla* ✅ 4s - new
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 9s -56%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 3s -33%
keccak_f1600_x3_native_aarch64_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 4s 2s +100%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 3s 3s +0%
keccak_finalize LP64 z3* ✅ 2s 3s -33%
keccak_init LP64 z3* ✅ 3s 3s +0%
keccak_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
keccak_squeezeblocks_x3 LP64 bitwuzla* ✅ 2s - new
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 2s 2s +0%
keccakf1600_permute LP64 z3* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x3_extract_bytes LP64 bitwuzla* ✅ 1s - new
keccakf1600x3_extract_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x3_permute LP64 z3* ✅ 2s - new
keccakf1600x3_permute_native LP64 z3* ✅ 8s - new
keccakf1600x3_xor_bytes LP64 bitwuzla* ✅ 2s - new
keccakf1600x3_xor_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 3s +0%
keccakf1600x4_permute LP64 z3* ✅ 2s 4s -50%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 22s -45%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 3s -33%
make_hint LP64 z3* ✅ 1s 3s -67%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 311s 58s +436%
mld_check_pct LP64 z3* ✅ 7s 14s -50%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 7s -43%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 1s 2s -50%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 3s 2s +50%
LP64 bitwuzla ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 2s 2s +0%
LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 4s 3s +33%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 1s 4s -75%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 1s +0%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 1s +0%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_sel_int32 LP64 z3* ✅ 1s 2s -50%
mld_h LP64 z3* ✅ 3s 4s -25%
mld_invntt_layer LP64 bitwuzla* ✅ 57s 107s -47%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600_permute_c LP64 z3* ✅ 3s 8s -62%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 4s 2s +100%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 13s 23s -43%
mld_ntt_layer LP64 bitwuzla* ✅ 22s 42s -48%
mld_polymat_expand_entry LP64 z3* ✅ 2s 3s -33%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 4s 4s +0%
mld_sample_pack_s1_s2 LP64 z3* ✅ 2s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 2s - new
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 4s - new
mld_sign_resume LP64 z3* ✅ 1s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 3s 2s +50%
mld_value_barrier_u8 LP64 z3* ✅ 2s 3s -33%
montgomery_reduce LP64 z3* ✅ 2s 3s -33%
ntt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 1s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 3s -33%
nttunpack_native_x86_64 LP64 z3* ✅ 3s 1s +200%
pack_sig_c LP64 z3* ✅ 1s 2s -50%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 3s -33%
pack_sig_z LP64 z3* ✅ 1s 4s -75%
pack_sk_rho_key_tr LP64 z3* ✅ 1s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 3s 4s -25%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 7s -43%
pointwise_native_aarch64 LP64 z3* ✅ 3s 5s -40%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 3s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 z3* ✅ 5s 4s +25%
poly_add LP64 z3* ✅ 5s 7s -29%
poly_caddq LP64 z3* ✅ 3s 2s +50%
poly_caddq_c LP64 z3* ✅ 1s 2s -50%
poly_caddq_native LP64 z3* ✅ 3s 5s -40%
poly_caddq_native_aarch64 LP64 z3* ✅ 4s 4s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 4s -50%
poly_challenge LP64 z3* ✅ 2s 3s -33%
poly_chknorm LP64 z3* ✅ 3s 4s -25%
poly_chknorm_c LP64 z3* ✅ 6s 17s -65%
poly_chknorm_native LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 2s -50%
poly_decompose LP64 z3* ✅ 2s 3s -33%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 2s +0%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 2s 4s -50%
poly_decompose_c LP64 z3* ✅ 4s 4s +0%
poly_decompose_native LP64 z3* ✅ 3s 3s +0%
poly_decompose_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_invntt_tomont LP64 z3* ✅ 3s 4s -25%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 5s 11s -55%
poly_invntt_tomont_native LP64 z3* ✅ 2s 4s -50%
poly_ntt LP64 z3* ✅ 3s 3s +0%
poly_ntt_c LP64 z3_smt_only* ✅ 9s 19s -53%
poly_ntt_native LP64 z3* ✅ 1s 5s -80%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 1s 2s -50%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 1s 4s -75%
poly_pointwise_montgomery LP64 z3* ✅ 3s 3s +0%
poly_pointwise_montgomery_c LP64 z3* ✅ 42s 114s -63%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 2s -50%
poly_power2round LP64 z3* ✅ 3s 4s -25%
poly_reduce LP64 z3* ✅ 2s 3s -33%
poly_shiftl LP64 z3* ✅ 2s 3s -33%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 2s 6s -67%
poly_uniform_3x LP64 z3* ✅ 4s - new
poly_uniform_4x LP64 z3* ✅ 6s 14s -57%
poly_uniform_eta LP64 z3* ✅ 1s 5s -80%
poly_uniform_eta_3x LP64 z3* ✅ 4s - new
poly_uniform_eta_4x LP64 z3* ✅ 7s 11s -36%
poly_uniform_gamma1 LP64 z3* ✅ 1s 4s -75%
poly_uniform_gamma1_3x LP64 z3* ✅ 1s - new
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 5s -80%
poly_use_hint LP64 z3* ✅ 5s 4s +25%
poly_use_hint_c LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native LP64 z3* ✅ 3s 4s -25%
poly_use_hint_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 5s 14s -64%
polyt0_pack LP64 z3* ✅ 2s 2s +0%
polyt0_unpack LP64 z3* ✅ 7s 15s -53%
polyt1_pack LP64 z3* ✅ 1s 4s -75%
polyt1_unpack LP64 z3* ✅ 1s 5s -80%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 13s 28s -54%
polyvec_matrix_expand_serial LP64 z3* ✅ 3s 8s -62%
polyvec_matrix_expand_x3 LP64 z3_no_bv_extract* ✅ 15s - new
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 3s 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* ✅ 3s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 5s -20%
polyveck_ntt LP64 z3* ✅ 3s 5s -40%
polyveck_reduce LP64 z3* ✅ 2s 5s -60%
polyveck_unpack_eta LP64 z3* ✅ 3s 2s +50%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 3s 10s -70%
polyvecl_ntt LP64 z3* ✅ 1s 2s -50%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 4s -75%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 112s 131s -15%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 4s 2s +100%
polyvecl_uniform_gamma1 LP64 z3* ✅ 3s 3s +0%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 1s 2s -50%
polyvecl_uniform_gamma1_x3 LP64 z3* ✅ 1s - new
polyvecl_unpack_eta LP64 z3* ✅ 2s 2s +0%
polyvecl_unpack_z LP64 z3* ✅ 1s 2s -50%
polyw1_pack LP64 z3* ✅ 3s 3s +0%
polyw1_pack_32 LP64 z3* ✅ 1s 2s -50%
polyw1_pack_88 LP64 z3* ✅ 2s 1s +100%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 2s 2s +0%
polyz_unpack LP64 z3* ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 1s 5s -80%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 5s -60%
polyz_unpack_c LP64 z3* ✅ 4s 11s -64%
polyz_unpack_native LP64 z3* ✅ 2s 2s +0%
polyz_unpack_native_x86_64 LP64 z3* ✅ 3s 3s +0%
power2round LP64 z3* ✅ 3s 3s +0%
reduce32 LP64 z3* ✅ 2s 2s +0%
rej_eta LP64 bitwuzla* ✅ 5s 3s +67%
rej_eta_c LP64 bitwuzla* ✅ 4s 4s +0%
rej_eta_native LP64 bitwuzla* ✅ 1s 6s -83%
rej_uniform LP64 z3* ✅ 13s 18s -28%
rej_uniform_c LP64 z3* ✅ 8s 15s -47%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 1s - new
rej_uniform_native LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 2s 5s -60%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 7s - new
sample_pack_s1_s2_x3 LP64 z3* ✅ 3s - new
shake128_absorb LP64 z3* ✅ 3s 2s +50%
shake128_finalize LP64 z3* ✅ 1s 2s -50%
shake128_init LP64 z3* ✅ 1s 3s -67%
shake128_release LP64 z3* ✅ 1s 1s +0%
shake128_squeeze LP64 bitwuzla* ✅ 1s 1s +0%
shake128x3_absorb_once LP64 bitwuzla* ✅ 1s - new
shake128x3_squeezeblocks LP64 bitwuzla* ✅ 1s - new
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 3s -33%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 1s +100%
shake256 LP64 z3* ✅ 2s 1s +100%
shake256_absorb LP64 z3* ✅ 1s 3s -67%
shake256_finalize LP64 z3* ✅ 2s 2s +0%
shake256_init LP64 z3* ✅ 1s 3s -67%
shake256_release LP64 z3* ✅ 2s 2s +0%
shake256_squeeze LP64 bitwuzla* ✅ 1s 2s -50%
shake256x3_absorb_once LP64 bitwuzla* ✅ 1s - new
shake256x3_squeezeblocks LP64 bitwuzla* ✅ 3s - new
shake256x4_absorb_once LP64 bitwuzla* ✅ 3s 3s +0%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 4s -75%
sig_unpack_hints LP64 z3* ⚠️ 23s 2s +1050%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 12s 4s +200%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 26s 5s +420%
sign_signature LP64 z3* ✅ 2s 3s -33%
sign_signature_extmu LP64 z3* ✅ 3s 4s -25%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 193s 26s +642%
sign_signature_pre_hash_internal LP64 z3* ✅ 4s 6s -33%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 3s 3s +0%
sign_verify LP64 z3* ✅ 1s 4s -75%
sign_verify_extmu LP64 z3* ✅ 3s 3s +0%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 294s 114s +158%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 5s -60%
sk_s1hat_get_poly LP64 z3* ✅ 2s 3s -33%
sk_s2hat_get_poly LP64 z3* ✅ 3s 2s +50%
sk_t0hat_get_poly LP64 z3* ✅ 2s 2s +0%
sys_check_capability LP64 z3* ✅ 4s 4s +0%
unpack_pk_t1 LP64 z3* ✅ 2s 5s -60%
unpack_sk LP64 z3* ✅ 2s 3s -33%
unpack_sk_s1hat LP64 z3* ✅ 2s 1s +100%
unpack_sk_s2hat LP64 z3* ✅ 2s 4s -50%
unpack_sk_t0hat LP64 z3* ✅ 3s 3s +0%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 3s 3s +0%

@oqs-bot

oqs-bot commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 123s 13s +846%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 185s 63s +194%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 177s 55s +222%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 402s 177s +127%
Full Results (245 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ✅ 1927s 1784s +8.0%
caddq LP64 z3* ✅ 1s 3s -67%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 123s 13s +846%
decompose LP64 z3* ✅ 1s 1s +0%
fqmul LP64 bitwuzla* ✅ 23s 40s -43%
fqscale LP64 bitwuzla* ✅ 3s 3s +0%
intt_native_aarch64 LP64 z3* ✅ 3s 3s +0%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 5s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 1s - new
intt_native_x86_64 LP64 z3* ✅ 1s 3s -67%
keccak_absorb LP64 z3* ✅ 4s 3s +33%
keccak_absorb_once_x3 LP64 bitwuzla* ✅ 7s - new
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 6s 8s -25%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x3_native_aarch64_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 4s 4s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 4s 2s +100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 1s 2s -50%
keccak_finalize LP64 z3* ✅ 3s 2s +50%
keccak_init LP64 z3* ✅ 2s 1s +100%
keccak_squeeze LP64 bitwuzla* ✅ 2s 4s -50%
keccak_squeezeblocks_x3 LP64 bitwuzla* ✅ 4s - new
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 1s 5s -80%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 3s 2s +50%
keccakf1600_permute LP64 z3* ✅ 3s 2s +50%
keccakf1600_permute_native LP64 z3* ✅ 1s 3s -67%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 4s 2s +100%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 4s 2s +100%
keccakf1600x3_extract_bytes LP64 bitwuzla* ✅ 2s - new
keccakf1600x3_extract_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x3_permute LP64 z3* ✅ 1s - new
keccakf1600x3_permute_native LP64 z3* ✅ 8s - new
keccakf1600x3_xor_bytes LP64 bitwuzla* ✅ 2s - new
keccakf1600x3_xor_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 3s 4s -25%
keccakf1600x4_permute LP64 z3* ✅ 3s 4s -25%
keccakf1600x4_permute_native LP64 z3* ✅ 11s 23s -52%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 1s +0%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 3s -33%
make_hint LP64 z3* ✅ 3s 2s +50%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 185s 63s +194%
mld_check_pct LP64 z3* ✅ 5s 14s -64%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 4s 7s -43%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 2s +0%
ILP32 cvc5_arrays_exp ✅ 1s 2s -50%
ILP32 z3 ✅ 1s 2s -50%
LP64 bitwuzla ✅ 2s 2s +0%
LP64 cvc5_arrays_exp ✅ 1s 2s -50%
LP64 z3* ✅ 2s 2s +0%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 1s 2s -50%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 2s 4s -50%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 2s 2s +0%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 2s 3s -33%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 2s -50%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 2s -50%
mld_ct_sel_int32 LP64 z3* ✅ 3s 3s +0%
mld_h LP64 z3* ✅ 3s 2s +50%
mld_invntt_layer LP64 bitwuzla* ✅ 57s 109s -48%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 3s 1s +200%
mld_keccakf1600_permute_c LP64 z3* ✅ 4s 6s -33%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 3s -67%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 2s +0%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 24s -50%
mld_ntt_layer LP64 bitwuzla* ✅ 23s 41s -44%
mld_polymat_expand_entry LP64 z3* ✅ 1s 4s -75%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 3s 2s +50%
mld_sample_pack_s1_s2 LP64 z3* ✅ 4s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 3s - new
mld_sign_attempt LP64 z3* ✅ 2s - new
mld_sign_finish LP64 z3* ✅ 2s - new
mld_sign_resume LP64 z3* ✅ 1s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u32 LP64 z3* ✅ 2s 3s -33%
mld_value_barrier_u8 LP64 z3* ✅ 1s 3s -67%
montgomery_reduce LP64 z3* ✅ 2s 4s -50%
ntt_native_aarch64 LP64 z3* ✅ 2s 2s +0%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 4s - new
LP64 z3 ✅ 3s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
pack_sig_c LP64 z3* ✅ 3s 5s -40%
pack_sig_h LP64 z3_no_bv_extract* ✅ 3s 5s -40%
pack_sig_z LP64 z3* ✅ 3s 2s +50%
pack_sk_rho_key_tr LP64 z3* ✅ 3s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 8s -50%
pointwise_native_aarch64 LP64 z3* ✅ 2s 5s -60%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 4s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 2s - new
pointwise_native_x86_64 LP64 z3* ✅ 3s 3s +0%
poly_add LP64 z3* ✅ 3s 9s -67%
poly_caddq LP64 z3* ✅ 3s 2s +50%
poly_caddq_c LP64 z3* ✅ 1s 2s -50%
poly_caddq_native LP64 z3* ✅ 2s 2s +0%
poly_caddq_native_aarch64 LP64 z3* ✅ 4s 2s +100%
poly_caddq_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_challenge LP64 z3* ✅ 2s 6s -67%
poly_chknorm LP64 z3* ✅ 2s 4s -50%
poly_chknorm_c LP64 z3* ✅ 6s 15s -60%
poly_chknorm_native LP64 z3* ✅ 2s 2s +0%
poly_chknorm_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_chknorm_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_decompose LP64 z3* ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 3s 1s +200%
poly_decompose_c LP64 z3* ✅ 2s 5s -60%
poly_decompose_native LP64 z3* ✅ 1s 3s -67%
poly_decompose_native_x86_64 LP64 z3* ✅ 1s 3s -67%
poly_invntt_tomont LP64 z3* ✅ 3s 3s +0%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 11s -45%
poly_invntt_tomont_native LP64 z3* ✅ 2s 2s +0%
poly_ntt LP64 z3* ✅ 3s 2s +50%
poly_ntt_c LP64 z3_smt_only* ✅ 11s 19s -42%
poly_ntt_native LP64 z3* ✅ 3s 4s -25%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 3s 4s -25%
poly_pointwise_montgomery LP64 z3* ✅ 1s 3s -67%
poly_pointwise_montgomery_c LP64 z3* ✅ 45s 125s -64%
poly_pointwise_montgomery_native LP64 z3* ✅ 3s 3s +0%
poly_power2round LP64 z3* ✅ 2s 4s -50%
poly_reduce LP64 z3* ✅ 2s 3s -33%
poly_shiftl LP64 z3* ✅ 1s 3s -67%
poly_sub LP64 z3* ✅ 3s 3s +0%
poly_uniform LP64 z3* ✅ 1s 4s -75%
poly_uniform_3x LP64 z3* ✅ 4s - new
poly_uniform_4x LP64 z3* ✅ 5s 13s -62%
poly_uniform_eta LP64 z3* ✅ 1s 4s -75%
poly_uniform_eta_3x LP64 z3* ✅ 6s - new
poly_uniform_eta_4x LP64 z3* ✅ 8s 14s -43%
poly_uniform_gamma1 LP64 z3* ✅ 2s 3s -33%
poly_uniform_gamma1_3x LP64 z3* ✅ 2s - new
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 4s -75%
poly_use_hint LP64 z3* ✅ 2s 3s -33%
poly_use_hint_c LP64 z3* ✅ 2s 5s -60%
poly_use_hint_native LP64 z3* ✅ 2s 2s +0%
poly_use_hint_native_aarch64 LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 3s 3s +0%
polyeta_unpack LP64 z3* ✅ 3s 8s -62%
polyt0_pack LP64 z3* ✅ 3s 3s +0%
polyt0_unpack LP64 z3* ✅ 7s 16s -56%
polyt1_pack LP64 z3* ✅ 2s 3s -33%
polyt1_unpack LP64 z3* ✅ 1s 5s -80%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 66s 110s -40%
polyvec_matrix_expand_serial LP64 z3* ✅ 14s 27s -48%
polyvec_matrix_expand_x3 LP64 z3_no_bv_extract* ✅ 42s - new
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 1s 1s +0%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 15s 18s -17%
polyveck_caddq LP64 z3* ✅ 3s 6s -50%
polyveck_decompose_pack_w1 LP64 z3* ✅ 7s - new
polyveck_invntt_tomont LP64 z3* ✅ 4s 8s -50%
polyveck_ntt LP64 z3* ✅ 5s 7s -29%
polyveck_reduce LP64 z3* ✅ 1s 4s -75%
polyveck_unpack_eta LP64 z3* ✅ 2s 6s -67%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 2s - new
polyvecl_chknorm LP64 z3* ✅ 3s 7s -57%
polyvecl_ntt LP64 z3* ✅ 4s 4s +0%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 105s 210s -50%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 2s +0%
polyvecl_uniform_gamma1 LP64 z3* ✅ 2s 2s +0%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 2s 3s -33%
polyvecl_uniform_gamma1_x3 LP64 z3* ✅ 2s - new
polyvecl_unpack_eta LP64 z3* ✅ 2s 3s -33%
polyvecl_unpack_z LP64 z3* ✅ 1s 3s -67%
polyw1_pack LP64 z3* ✅ 1s 4s -75%
polyw1_pack_32 LP64 z3* ✅ 3s 4s -25%
polyw1_pack_88 LP64 z3* ✅ 5s 2s +150%
polyw1_unpack LP64 z3* ✅ 1s - new
polyw1_unpack_32 LP64 z3* ✅ 1s - new
polyw1_unpack_88 LP64 z3* ✅ 2s - new
polyz_pack LP64 z3* ✅ 1s 3s -67%
polyz_unpack LP64 z3* ✅ 2s 3s -33%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 3s 3s +0%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 3s -33%
polyz_unpack_c LP64 z3* ✅ 5s 13s -62%
polyz_unpack_native LP64 z3* ✅ 2s 4s -50%
polyz_unpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
power2round LP64 z3* ✅ 1s 1s +0%
reduce32 LP64 z3* ✅ 1s 3s -67%
rej_eta LP64 bitwuzla* ✅ 1s 2s -50%
rej_eta_c LP64 bitwuzla* ✅ 2s 5s -60%
rej_eta_native LP64 bitwuzla* ✅ 3s 3s +0%
rej_uniform LP64 z3* ✅ 10s 18s -44%
rej_uniform_c LP64 z3* ✅ 10s 14s -29%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 4s -50%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 2s - new
rej_uniform_native LP64 bitwuzla* ✅ 1s 4s -75%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 1s 3s -67%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 9s - new
sample_pack_s1_s2_x3 LP64 z3* ✅ 4s - new
shake128_absorb LP64 z3* ✅ 2s 2s +0%
shake128_finalize LP64 z3* ✅ 3s 1s +200%
shake128_init LP64 z3* ✅ 3s 2s +50%
shake128_release LP64 z3* ✅ 1s 3s -67%
shake128_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake128x3_absorb_once LP64 bitwuzla* ✅ 2s - new
shake128x3_squeezeblocks LP64 bitwuzla* ✅ 1s - new
shake128x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 2s 3s -33%
shake256 LP64 z3* ✅ 4s 2s +100%
shake256_absorb LP64 z3* ✅ 1s 2s -50%
shake256_finalize LP64 z3* ✅ 1s 1s +0%
shake256_init LP64 z3* ✅ 3s 2s +50%
shake256_release LP64 z3* ✅ 3s 2s +50%
shake256_squeeze LP64 bitwuzla* ✅ 1s 3s -67%
shake256x3_absorb_once LP64 bitwuzla* ✅ 1s - new
shake256x3_squeezeblocks LP64 bitwuzla* ✅ 2s - new
shake256x4_absorb_once LP64 bitwuzla* ✅ 1s 3s -67%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 2s -50%
sig_unpack_hints LP64 z3* ✅ 16s 2s +700%
sign_keypair LP64 z3* ✅ 5s 3s +67%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 19s 5s +280%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_signature LP64 z3* ✅ 5s 6s -17%
sign_signature_extmu LP64 z3* ✅ 2s 2s +0%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 177s 55s +222%
sign_signature_pre_hash_internal LP64 z3* ✅ 5s 3s +67%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 5s 3s +67%
sign_verify LP64 z3* ✅ 3s 3s +0%
sign_verify_extmu LP64 z3* ✅ 4s 3s +33%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 402s 177s +127%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 5s -40%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 2s 5s -60%
sk_s1hat_get_poly LP64 z3* ✅ 3s 6s -50%
sk_s2hat_get_poly LP64 z3* ✅ 1s 2s -50%
sk_t0hat_get_poly LP64 z3* ✅ 1s 2s -50%
sys_check_capability LP64 z3* ✅ 2s 4s -50%
unpack_pk_t1 LP64 z3* ✅ 3s 5s -40%
unpack_sk LP64 z3* ✅ 3s 3s +0%
unpack_sk_s1hat LP64 z3* ✅ 3s 2s +50%
unpack_sk_s2hat LP64 z3* ✅ 1s 4s -75%
unpack_sk_t0hat LP64 z3* ✅ 3s 5s -40%
use_hint LP64 z3* ✅ 2s 2s +0%
yvec_get_poly LP64 z3* ✅ 2s 3s -33%
yvec_init LP64 z3* ✅ 2s 3s -33%

@oqs-bot

oqs-bot commented Oct 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

* default.

⚠️ Attention Required

Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 3077s 2151s +43.0%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 208s 19s +995%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 279s 55s +407%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 353s 42s +740%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 1088s 97s +1022%
Full Results (245 configurations)
Proof DM Solver Status Current Previous Change
**TOTAL** - - ⚠️ 3077s 2151s +43.0%
caddq LP64 z3* ✅ 2s 4s -50%
compute_pack_t0_t1 LP64 z3_no_bv_extract* ⚠️ 208s 19s +995%
decompose LP64 z3* ✅ 2s 3s -33%
fqmul LP64 bitwuzla* ✅ 23s 43s -47%
fqscale LP64 bitwuzla* ✅ 1s 3s -67%
intt_native_aarch64 LP64 z3* ✅ 2s 3s -33%
intt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
intt_native_rv32im_slowmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 1s - new
intt_native_x86_64 LP64 z3* ✅ 5s 3s +67%
keccak_absorb LP64 z3* ✅ 2s 3s -33%
keccak_absorb_once_x3 LP64 bitwuzla* ✅ 4s - new
keccak_absorb_once_x4 LP64 bitwuzla* ✅ 4s 9s -56%
keccak_f1600_x1_native_aarch64 LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a LP64 bitwuzla* ✅ 2s 1s +100%
keccak_f1600_x3_native_aarch64_v84a_scalar_hybrid LP64 bitwuzla* ✅ 3s - new
keccak_f1600_x4_native_aarch64_v84a LP64 bitwuzla* ✅ 1s 4s -75%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid LP64 bitwuzla* ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid LP64 bitwuzla* ✅ 2s 4s -50%
keccak_f1600_x4_native_avx2 LP64 bitwuzla* ✅ 2s 2s +0%
keccak_finalize LP64 z3* ✅ 2s 1s +100%
keccak_init LP64 z3* ✅ 2s 3s -33%
keccak_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
keccak_squeezeblocks_x3 LP64 bitwuzla* ✅ 2s - new
keccak_squeezeblocks_x4 LP64 bitwuzla* ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) LP64 z3* ✅ 1s 3s -67%
keccakf1600_permute LP64 z3* ✅ 2s 3s -33%
keccakf1600_permute_native LP64 z3* ✅ 2s 4s -50%
keccakf1600_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600_xor_bytes (big endian) LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x3_extract_bytes LP64 bitwuzla* ✅ 3s - new
keccakf1600x3_extract_bytes_c LP64 z3* ✅ 3s - new
keccakf1600x3_permute LP64 z3* ✅ 2s - new
keccakf1600x3_permute_native LP64 z3* ✅ 10s - new
keccakf1600x3_xor_bytes LP64 bitwuzla* ✅ 3s - new
keccakf1600x3_xor_bytes_c LP64 z3* ✅ 1s - new
keccakf1600x4_extract_bytes LP64 bitwuzla* ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native LP64 bitwuzla* ✅ 1s 2s -50%
keccakf1600x4_permute LP64 z3* ✅ 1s 3s -67%
keccakf1600x4_permute_native LP64 z3* ✅ 12s 23s -48%
keccakf1600x4_xor_bytes LP64 bitwuzla* ✅ 1s 3s -67%
keccakf1600x4_xor_bytes_native LP64 bitwuzla* ✅ 2s 3s -33%
make_hint LP64 z3* ✅ 3s 3s +0%
mld_attempt_signature_generation LP64 z3_no_bv_extract* ⚠️ 279s 55s +407%
mld_check_pct LP64 z3* ✅ 6s 16s -62%
mld_compute_pack_z LP64 z3_no_bv_extract* ✅ 3s 8s -62%
mld_ct_abs_i32 ILP32 bitwuzla ✅ 2s 3s -33%
ILP32 cvc5_arrays_exp ✅ 3s 3s +0%
ILP32 z3 ✅ 1s 3s -67%
LP64 bitwuzla ✅ 1s 3s -67%
LP64 cvc5_arrays_exp ✅ 2s 3s -33%
LP64 z3* ✅ 1s 3s -67%
mld_ct_cmask_neg_i32 LP64 z3* ✅ 1s 4s -75%
mld_ct_cmask_nonzero_u32 LP64 z3* ✅ 4s 2s +100%
mld_ct_cmask_nonzero_u8 LP64 z3* ✅ 3s 3s +0%
mld_ct_get_optblocker_i64 LP64 z3* ✅ 3s 3s +0%
mld_ct_get_optblocker_u32 LP64 z3* ✅ 1s 2s -50%
mld_ct_get_optblocker_u8 LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_memcmp LP64 bitwuzla* ✅ 1s 3s -67%
mld_ct_sel_int32 LP64 z3* ✅ 1s 3s -67%
mld_h LP64 z3* ✅ 2s 3s -33%
mld_invntt_layer LP64 bitwuzla* ✅ 57s 115s -50%
mld_keccakf1600_extract_bytes LP64 z3* ✅ 3s 4s -25%
mld_keccakf1600_permute_c LP64 z3* ✅ 3s 7s -57%
mld_keccakf1600x4_extract_bytes_c LP64 z3* ✅ 1s 2s -50%
mld_keccakf1600x4_xor_bytes_c LP64 z3* ✅ 2s 4s -50%
mld_ntt_butterfly_block LP64 bitwuzla* ✅ 12s 24s -50%
mld_ntt_layer LP64 bitwuzla* ✅ 20s 45s -56%
mld_polymat_expand_entry LP64 z3* ✅ 2s 3s -33%
mld_prepare_domain_separation_prefix LP64 z3* ✅ 2s 4s -50%
mld_sample_pack_s1_s2 LP64 z3* ✅ 4s - new
mld_sample_pack_s1_s2_serial LP64 z3* ✅ 4s - new
mld_sign_attempt LP64 z3* ✅ 3s - new
mld_sign_finish LP64 z3* ✅ 1s - new
mld_sign_resume LP64 z3* ✅ 2s - new
mld_value_barrier_i64 LP64 z3* ✅ 2s 1s +100%
mld_value_barrier_u32 LP64 z3* ✅ 2s 2s +0%
mld_value_barrier_u8 LP64 z3* ✅ 1s 3s -67%
montgomery_reduce LP64 z3* ✅ 2s 3s -33%
ntt_native_aarch64 LP64 z3* ✅ 4s 6s -33%
ntt_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
ntt_native_rv32im_slowmul ILP32 z3* ✅ 3s - new
LP64 z3 ✅ 3s - new
ntt_native_x86_64 LP64 z3* ✅ 2s 2s +0%
nttunpack_native_x86_64 LP64 z3* ✅ 2s 3s -33%
pack_sig_c LP64 z3* ✅ 5s 4s +25%
pack_sig_h LP64 z3_no_bv_extract* ✅ 2s 4s -50%
pack_sig_z LP64 z3* ✅ 4s 5s -20%
pack_sk_rho_key_tr LP64 z3* ✅ 3s - new
pointwise_acc_native_aarch64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_acc_native_x86_64 LP64 z3_smt_only* ✅ 4s 6s -33%
pointwise_native_aarch64 LP64 z3* ✅ 2s 5s -60%
pointwise_native_rv32im_fastmul ILP32 z3* ✅ 2s - new
LP64 z3 ✅ 2s - new
pointwise_native_rv32im_slowmul ILP32 z3* ✅ 1s - new
LP64 z3 ✅ 1s - new
pointwise_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_add LP64 z3* ✅ 3s 6s -50%
poly_caddq LP64 z3* ✅ 2s 2s +0%
poly_caddq_c LP64 z3* ✅ 1s 3s -67%
poly_caddq_native LP64 z3* ✅ 2s 4s -50%
poly_caddq_native_aarch64 LP64 z3* ✅ 3s 3s +0%
poly_caddq_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_challenge LP64 z3* ✅ 1s 5s -80%
poly_chknorm LP64 z3* ✅ 1s 3s -67%
poly_chknorm_c LP64 z3* ✅ 6s 15s -60%
poly_chknorm_native LP64 z3* ✅ 2s 4s -50%
poly_chknorm_native_aarch64 LP64 z3* ✅ 1s 4s -75%
poly_chknorm_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_decompose LP64 z3* ✅ 2s 3s -33%
poly_decompose_32_native_aarch64 LP64 z3* ✅ 2s 5s -60%
poly_decompose_88_native_aarch64 LP64 z3* ✅ 1s 2s -50%
poly_decompose_c LP64 z3* ✅ 2s 5s -60%
poly_decompose_native LP64 z3* ✅ 5s 2s +150%
poly_decompose_native_x86_64 LP64 z3* ✅ 2s 2s +0%
poly_invntt_tomont LP64 z3* ✅ 1s 1s +0%
poly_invntt_tomont_c LP64 z3_smt_only* ✅ 6s 12s -50%
poly_invntt_tomont_native LP64 z3* ✅ 3s 5s -40%
poly_ntt LP64 z3* ✅ 5s 3s +67%
poly_ntt_c LP64 z3_smt_only* ✅ 8s 21s -62%
poly_ntt_native LP64 z3* ✅ 1s 3s -67%
poly_permute_bitrev_to_custom_optional LP64 z3* ✅ 1s 3s -67%
poly_permute_bitrev_to_custom_optional_native LP64 z3* ✅ 1s 5s -80%
poly_pointwise_montgomery LP64 z3* ✅ 1s 4s -75%
poly_pointwise_montgomery_c LP64 z3* ✅ 44s 144s -69%
poly_pointwise_montgomery_native LP64 z3* ✅ 1s 5s -80%
poly_power2round LP64 z3* ✅ 1s 3s -67%
poly_reduce LP64 z3* ✅ 2s 2s +0%
poly_shiftl LP64 z3* ✅ 3s 4s -25%
poly_sub LP64 z3* ✅ 2s 3s -33%
poly_uniform LP64 z3* ✅ 1s 4s -75%
poly_uniform_3x LP64 z3* ✅ 4s - new
poly_uniform_4x LP64 z3* ✅ 6s 13s -54%
poly_uniform_eta LP64 z3* ✅ 3s 4s -25%
poly_uniform_eta_3x LP64 z3* ✅ 3s - new
poly_uniform_eta_4x LP64 z3* ✅ 9s 11s -18%
poly_uniform_gamma1 LP64 z3* ✅ 2s 4s -50%
poly_uniform_gamma1_3x LP64 z3* ✅ 2s - new
poly_uniform_gamma1_4x LP64 z3* ✅ 1s 3s -67%
poly_use_hint LP64 z3* ✅ 1s 1s +0%
poly_use_hint_c LP64 z3* ✅ 1s 2s -50%
poly_use_hint_native LP64 z3* ✅ 2s 3s -33%
poly_use_hint_native_aarch64 LP64 z3* ✅ 3s 2s +50%
poly_use_hint_native_x86_64 LP64 z3* ✅ 2s - new
polyeta_pack LP64 z3* ✅ 1s 4s -75%
polyeta_unpack LP64 z3* ✅ 6s 17s -65%
polyt0_pack LP64 z3* ✅ 3s 4s -25%
polyt0_unpack LP64 z3* ✅ 6s 14s -57%
polyt1_pack LP64 z3* ✅ 2s 3s -33%
polyt1_unpack LP64 z3* ✅ 3s 4s -25%
polyvec_matrix_expand LP64 z3_no_bv_extract* ✅ 96s 324s -70%
polyvec_matrix_expand_serial LP64 z3* ✅ 20s 38s -47%
polyvec_matrix_expand_x3 LP64 z3_no_bv_extract* ✅ 120s - new
polyvec_matrix_pointwise_montgomery_row LP64 z3_no_bv_extract* ✅ 2s 3s -33%
polyvec_matrix_pointwise_montgomery_yvec LP64 z3* ✅ 15s 18s -17%
polyveck_caddq LP64 z3* ✅ 6s 8s -25%
polyveck_decompose_pack_w1 LP64 z3* ✅ 5s - new
polyveck_invntt_tomont LP64 z3* ✅ 5s 9s -44%
polyveck_ntt LP64 z3* ✅ 3s 11s -73%
polyveck_reduce LP64 z3* ✅ 2s 3s -33%
polyveck_unpack_eta LP64 z3* ✅ 3s 4s -25%
polyveck_unpack_eta_chknorm LP64 z3* ✅ 3s - new
polyvecl_chknorm LP64 z3* ✅ 3s 7s -57%
polyvecl_ntt LP64 z3* ✅ 3s 7s -57%
polyvecl_pointwise_acc_montgomery LP64 z3_smt_only* ✅ 1s 5s -80%
polyvecl_pointwise_acc_montgomery_c LP64 z3* ✅ 117s 353s -67%
polyvecl_pointwise_acc_montgomery_native LP64 z3_smt_only* ✅ 2s 3s -33%
polyvecl_uniform_gamma1 LP64 z3* ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial LP64 z3* ✅ 3s 4s -25%
polyvecl_uniform_gamma1_x3 LP64 z3* ✅ 3s - new
polyvecl_unpack_eta LP64 z3* ✅ 3s 5s -40%
polyvecl_unpack_z LP64 z3* ✅ 2s 4s -50%
polyw1_pack LP64 z3* ✅ 2s 4s -50%
polyw1_pack_32 LP64 z3* ✅ 1s 4s -75%
polyw1_pack_88 LP64 z3* ✅ 4s 3s +33%
polyw1_unpack LP64 z3* ✅ 5s - new
polyw1_unpack_32 LP64 z3* ✅ 2s - new
polyw1_unpack_88 LP64 z3* ✅ 1s - new
polyz_pack LP64 z3* ✅ 2s 5s -60%
polyz_unpack LP64 z3* ✅ 3s 2s +50%
polyz_unpack_17_native_aarch64 LP64 z3* ✅ 2s 3s -33%
polyz_unpack_19_native_aarch64 LP64 z3* ✅ 2s 4s -50%
polyz_unpack_c LP64 z3* ✅ 4s 3s +33%
polyz_unpack_native LP64 z3* ✅ 1s 4s -75%
polyz_unpack_native_x86_64 LP64 z3* ✅ 1s 3s -67%
power2round LP64 z3* ✅ 1s 4s -75%
reduce32 LP64 z3* ✅ 2s 3s -33%
rej_eta LP64 bitwuzla* ✅ 2s 4s -50%
rej_eta_c LP64 bitwuzla* ✅ 3s 5s -40%
rej_eta_native LP64 bitwuzla* ✅ 1s 6s -83%
rej_uniform LP64 z3* ✅ 11s 15s -27%
rej_uniform_c LP64 z3* ✅ 8s 19s -58%
rej_uniform_eta_native_aarch64 LP64 bitwuzla* ✅ 2s 5s -60%
rej_uniform_eta_native_x86_64 LP64 z3_smt_only* ✅ 1s - new
rej_uniform_native LP64 bitwuzla* ✅ 1s 8s -88%
rej_uniform_native_aarch64 LP64 bitwuzla* ✅ 4s 2s +100%
rej_uniform_native_x86_64 LP64 z3_smt_only* ✅ 6s - new
sample_pack_s1_s2_x3 LP64 z3* ✅ 6s - new
shake128_absorb LP64 z3* ✅ 3s 4s -25%
shake128_finalize LP64 z3* ✅ 1s 2s -50%
shake128_init LP64 z3* ✅ 3s 1s +200%
shake128_release LP64 z3* ✅ 1s 4s -75%
shake128_squeeze LP64 bitwuzla* ✅ 5s 2s +150%
shake128x3_absorb_once LP64 bitwuzla* ✅ 3s - new
shake128x3_squeezeblocks LP64 bitwuzla* ✅ 1s - new
shake128x4_absorb_once LP64 bitwuzla* ✅ 2s 5s -60%
shake128x4_squeezeblocks LP64 bitwuzla* ✅ 3s 3s +0%
shake256 LP64 z3* ✅ 2s 2s +0%
shake256_absorb LP64 z3* ✅ 1s 2s -50%
shake256_finalize LP64 z3* ✅ 1s 2s -50%
shake256_init LP64 z3* ✅ 2s 2s +0%
shake256_release LP64 z3* ✅ 2s 3s -33%
shake256_squeeze LP64 bitwuzla* ✅ 2s 2s +0%
shake256x3_absorb_once LP64 bitwuzla* ✅ 1s - new
shake256x3_squeezeblocks LP64 bitwuzla* ✅ 1s - new
shake256x4_absorb_once LP64 bitwuzla* ✅ 4s 2s +100%
shake256x4_squeezeblocks LP64 bitwuzla* ✅ 1s 1s +0%
sig_unpack_hints LP64 z3* ✅ 13s 3s +333%
sign_keypair LP64 z3* ✅ 4s 4s +0%
sign_keypair_internal LP64 z3_no_bv_extract* ✅ 18s 6s +200%
sign_pk_from_sk LP64 z3_no_bv_extract* ⚠️ 30s 6s +400%
sign_signature LP64 z3* ✅ 3s 5s -40%
sign_signature_extmu LP64 z3* ✅ 5s 4s +25%
sign_signature_internal LP64 z3_no_bv_extract* ⚠️ 353s 42s +740%
sign_signature_pre_hash_internal LP64 z3* ✅ 5s 5s +0%
sign_signature_pre_hash_shake256 LP64 z3* ✅ 4s 6s -33%
sign_verify LP64 z3* ✅ 2s 5s -60%
sign_verify_extmu LP64 z3* ✅ 1s 3s -67%
sign_verify_internal LP64 z3_no_bv_extract* ⚠️ 1088s 97s +1022%
sign_verify_pre_hash_internal LP64 z3* ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 LP64 z3* ✅ 3s 3s +0%
sk_s1hat_get_poly LP64 z3* ✅ 3s 3s +0%
sk_s2hat_get_poly LP64 z3* ✅ 3s 3s +0%
sk_t0hat_get_poly LP64 z3* ✅ 2s 4s -50%
sys_check_capability LP64 z3* ✅ 1s 3s -67%
unpack_pk_t1 LP64 z3* ✅ 1s 1s +0%
unpack_sk LP64 z3* ✅ 2s 5s -60%
unpack_sk_s1hat LP64 z3* ✅ 1s 2s -50%
unpack_sk_s2hat LP64 z3* ✅ 2s 3s -33%
unpack_sk_t0hat LP64 z3* ✅ 5s 7s -29%
use_hint LP64 z3* ✅ 1s 3s -67%
yvec_get_poly LP64 z3* ✅ 2s 4s -50%
yvec_init LP64 z3* ✅ 2s 4s -50%

@soumya2094
soumya2094 force-pushed the x3-hybrid-keccak-f1600 branch from 5197c8b to d3db6bf Compare October 22, 2026 15:51
oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Intel Xeon 4th gen (c7i)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 43944 cycles 43730 cycles 1.00
ML-DSA-44 sign 130450 cycles 129969 cycles 1.00
ML-DSA-44 verify 45010 cycles 45099 cycles 1.00
ML-DSA-65 keypair 74823 cycles 74743 cycles 1.00
ML-DSA-65 sign 212503 cycles 212343 cycles 1.00
ML-DSA-65 verify 74214 cycles 74602 cycles 0.99
ML-DSA-87 keypair 123660 cycles 123989 cycles 1.00
ML-DSA-87 sign 269982 cycles 270624 cycles 1.00
ML-DSA-87 verify 119925 cycles 120053 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Intel Xeon 4th gen (c7i) (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 91995 cycles 91828 cycles 1.00
ML-DSA-44 sign 348156 cycles 347290 cycles 1.00
ML-DSA-44 verify 99345 cycles 99167 cycles 1.00
ML-DSA-65 keypair 155589 cycles 155306 cycles 1.00
ML-DSA-65 sign 567594 cycles 568167 cycles 1.00
ML-DSA-65 verify 159576 cycles 159379 cycles 1.00
ML-DSA-87 keypair 257426 cycles 258174 cycles 1.00
ML-DSA-87 sign 721212 cycles 719356 cycles 1.00
ML-DSA-87 verify 263861 cycles 263638 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

AMD EPYC 4th gen (c7a)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 48213 cycles 47952 cycles 1.01
ML-DSA-44 sign 139478 cycles 140374 cycles 0.99
ML-DSA-44 verify 49354 cycles 49286 cycles 1.00
ML-DSA-65 keypair 83940 cycles 82656 cycles 1.02
ML-DSA-65 sign 227982 cycles 226703 cycles 1.01
ML-DSA-65 verify 83605 cycles 82393 cycles 1.01
ML-DSA-87 keypair 132436 cycles 132575 cycles 1.00
ML-DSA-87 sign 280685 cycles 279595 cycles 1.00
ML-DSA-87 verify 129529 cycles 128405 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

AMD EPYC 4th gen (c7a) (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 115293 cycles 115137 cycles 1.00
ML-DSA-44 sign 419824 cycles 420433 cycles 1.00
ML-DSA-44 verify 123722 cycles 123747 cycles 1.00
ML-DSA-65 keypair 195272 cycles 195252 cycles 1.00
ML-DSA-65 sign 683860 cycles 685019 cycles 1.00
ML-DSA-65 verify 199502 cycles 199512 cycles 1.00
ML-DSA-87 keypair 325551 cycles 324488 cycles 1.00
ML-DSA-87 sign 866667 cycles 867952 cycles 1.00
ML-DSA-87 verify 330757 cycles 330118 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

AMD EPYC 3rd gen (c6a)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 52512 cycles 52559 cycles 1.00
ML-DSA-44 sign 155862 cycles 156148 cycles 1.00
ML-DSA-44 verify 53908 cycles 54123 cycles 1.00
ML-DSA-65 keypair 89507 cycles 89889 cycles 1.00
ML-DSA-65 sign 252530 cycles 252834 cycles 1.00
ML-DSA-65 verify 89656 cycles 90026 cycles 1.00
ML-DSA-87 keypair 146722 cycles 146339 cycles 1.00
ML-DSA-87 sign 314079 cycles 312566 cycles 1.00
ML-DSA-87 verify 140128 cycles 139465 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'AMD EPYC 4th gen (c7a) (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-65 verify 206914 cycles 199906 cycles 1.04

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton5

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 47652 cycles 52381 cycles 0.91
ML-DSA-44 sign 161204 cycles 162216 cycles 0.99
ML-DSA-44 verify 51839 cycles 54836 cycles 0.95
ML-DSA-65 keypair 78734 cycles 91235 cycles 0.86
ML-DSA-65 sign 251023 cycles 266193 cycles 0.94
ML-DSA-65 verify 78921 cycles 89883 cycles 0.88
ML-DSA-87 keypair 133123 cycles 148004 cycles 0.90
ML-DSA-87 sign 315864 cycles 334857 cycles 0.94
ML-DSA-87 verify 131724 cycles 145169 cycles 0.91

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Intel Xeon 3rd gen (c6i)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 64400 cycles 63887 cycles 1.01
ML-DSA-44 sign 194919 cycles 192108 cycles 1.01
ML-DSA-44 verify 68723 cycles 68083 cycles 1.01
ML-DSA-65 keypair 110524 cycles 110095 cycles 1.00
ML-DSA-65 sign 319649 cycles 318086 cycles 1.00
ML-DSA-65 verify 112155 cycles 111442 cycles 1.01
ML-DSA-87 keypair 174729 cycles 174451 cycles 1.00
ML-DSA-87 sign 382171 cycles 382132 cycles 1.00
ML-DSA-87 verify 173153 cycles 172546 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

AMD EPYC 3rd gen (c6a) (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 133877 cycles 134010 cycles 1.00
ML-DSA-44 sign 520185 cycles 520149 cycles 1.00
ML-DSA-44 verify 145787 cycles 146079 cycles 1.00
ML-DSA-65 keypair 223966 cycles 223726 cycles 1.00
ML-DSA-65 sign 848011 cycles 847014 cycles 1.00
ML-DSA-65 verify 234233 cycles 233798 cycles 1.00
ML-DSA-87 keypair 370639 cycles 371896 cycles 1.00
ML-DSA-87 sign 1061453 cycles 1064787 cycles 1.00
ML-DSA-87 verify 381187 cycles 383120 cycles 0.99

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton5 (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 103401 cycles 102862 cycles 1.01
ML-DSA-44 sign 372867 cycles 373835 cycles 1.00
ML-DSA-44 verify 111195 cycles 111286 cycles 1.00
ML-DSA-65 keypair 176815 cycles 177304 cycles 1.00
ML-DSA-65 sign 621771 cycles 605124 cycles 1.03
ML-DSA-65 verify 180098 cycles 179404 cycles 1.00
ML-DSA-87 keypair 284840 cycles 284743 cycles 1.00
ML-DSA-87 sign 763654 cycles 771394 cycles 0.99
ML-DSA-87 verify 296496 cycles 294457 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot 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.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Graviton5 (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-65 sign 624867 cycles 605385 cycles 1.03

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Intel Xeon 3rd gen (c6i) (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 165744 cycles 165766 cycles 1.00
ML-DSA-44 sign 627417 cycles 626376 cycles 1.00
ML-DSA-44 verify 179499 cycles 181191 cycles 0.99
ML-DSA-65 keypair 282999 cycles 281493 cycles 1.01
ML-DSA-65 sign 1034327 cycles 1013590 cycles 1.02
ML-DSA-65 verify 291908 cycles 290267 cycles 1.01
ML-DSA-87 keypair 470285 cycles 462216 cycles 1.02
ML-DSA-87 sign 1316667 cycles 1264955 cycles 1.04
ML-DSA-87 verify 486758 cycles 473565 cycles 1.03

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton4

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 68290 cycles 68497 cycles 1.00
ML-DSA-44 sign 198909 cycles 198809 cycles 1.00
ML-DSA-44 verify 70367 cycles 70325 cycles 1.00
ML-DSA-65 keypair 120190 cycles 120403 cycles 1.00
ML-DSA-65 sign 325982 cycles 326041 cycles 1.00
ML-DSA-65 verify 116937 cycles 117149 cycles 1.00
ML-DSA-87 keypair 198368 cycles 198735 cycles 1.00
ML-DSA-87 sign 421947 cycles 422959 cycles 1.00
ML-DSA-87 verify 193500 cycles 193695 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Intel Xeon 3rd gen (c6i) (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-87 sign 1316667 cycles 1264955 cycles 1.04

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton4 (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 129962 cycles 129792 cycles 1.00
ML-DSA-44 sign 443899 cycles 444028 cycles 1.00
ML-DSA-44 verify 137642 cycles 137906 cycles 1.00
ML-DSA-65 keypair 226069 cycles 227248 cycles 0.99
ML-DSA-65 sign 718215 cycles 718261 cycles 1.00
ML-DSA-65 verify 223066 cycles 223008 cycles 1.00
ML-DSA-87 keypair 368346 cycles 369452 cycles 1.00
ML-DSA-87 sign 920349 cycles 923439 cycles 1.00
ML-DSA-87 verify 373062 cycles 374051 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 22, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 113419 cycles 113360 cycles 1.00
ML-DSA-44 sign 354642 cycles 354339 cycles 1.00
ML-DSA-44 verify 117343 cycles 117191 cycles 1.00
ML-DSA-65 keypair 195444 cycles 195631 cycles 1.00
ML-DSA-65 sign 583594 cycles 583538 cycles 1.00
ML-DSA-65 verify 193215 cycles 193005 cycles 1.00
ML-DSA-87 keypair 322168 cycles 322119 cycles 1.00
ML-DSA-87 sign 746821 cycles 747524 cycles 1.00
ML-DSA-87 verify 317823 cycles 317939 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton3

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 72394 cycles 72393 cycles 1.00
ML-DSA-44 sign 209931 cycles 209984 cycles 1.00
ML-DSA-44 verify 74985 cycles 74880 cycles 1.00
ML-DSA-65 keypair 126676 cycles 126759 cycles 1.00
ML-DSA-65 sign 345430 cycles 345270 cycles 1.00
ML-DSA-65 verify 124139 cycles 124136 cycles 1.00
ML-DSA-87 keypair 208322 cycles 208205 cycles 1.00
ML-DSA-87 sign 439742 cycles 439770 cycles 1.00
ML-DSA-87 verify 204460 cycles 204504 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 22, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Arm Cortex-A76 (Raspberry Pi 5) benchmarks (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 210343 cycles 210830 cycles 1.00
ML-DSA-44 sign 756586 cycles 757227 cycles 1.00
ML-DSA-44 verify 227378 cycles 227286 cycles 1.00
ML-DSA-65 keypair 373064 cycles 374699 cycles 1.00
ML-DSA-65 sign 1240518 cycles 1242073 cycles 1.00
ML-DSA-65 verify 368551 cycles 368653 cycles 1.00
ML-DSA-87 keypair 597253 cycles 597196 cycles 1.00
ML-DSA-87 sign 1576059 cycles 1579067 cycles 1.00
ML-DSA-87 verify 610647 cycles 611771 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton3 (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 140844 cycles 140675 cycles 1.00
ML-DSA-44 sign 490523 cycles 490334 cycles 1.00
ML-DSA-44 verify 151068 cycles 151249 cycles 1.00
ML-DSA-65 keypair 245989 cycles 247127 cycles 1.00
ML-DSA-65 sign 798010 cycles 797798 cycles 1.00
ML-DSA-65 verify 244924 cycles 244638 cycles 1.00
ML-DSA-87 keypair 399877 cycles 400782 cycles 1.00
ML-DSA-87 sign 1019840 cycles 1023896 cycles 1.00
ML-DSA-87 verify 407324 cycles 408361 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton2

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 113451 cycles 113704 cycles 1.00
ML-DSA-44 sign 354655 cycles 355253 cycles 1.00
ML-DSA-44 verify 117318 cycles 117688 cycles 1.00
ML-DSA-65 keypair 196454 cycles 195805 cycles 1.00
ML-DSA-65 sign 585782 cycles 584563 cycles 1.00
ML-DSA-65 verify 193793 cycles 193692 cycles 1.00
ML-DSA-87 keypair 322673 cycles 322466 cycles 1.00
ML-DSA-87 sign 748511 cycles 748282 cycles 1.00
ML-DSA-87 verify 318420 cycles 318279 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot
oqs-bot reviewed Oct 22, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Graviton2 (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 210819 cycles 210640 cycles 1.00
ML-DSA-44 sign 757985 cycles 757125 cycles 1.00
ML-DSA-44 verify 227608 cycles 228080 cycles 1.00
ML-DSA-65 keypair 374154 cycles 373760 cycles 1.00
ML-DSA-65 sign 1241755 cycles 1242290 cycles 1.00
ML-DSA-65 verify 368572 cycles 369324 cycles 1.00
ML-DSA-87 keypair 597197 cycles 598479 cycles 1.00
ML-DSA-87 sign 1600428 cycles 1597028 cycles 1.00
ML-DSA-87 verify 611960 cycles 610887 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@hanno-becker
hanno-becker self-requested a review October 23, 2026 05:18
github-actions[bot]
github-actions Bot reviewed Oct 23, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 2134310 cycles 2134310 cycles 1
ML-DSA-44 sign 17791748 cycles 17791748 cycles 1
ML-DSA-44 verify 2398890 cycles 2398890 cycles 1
ML-DSA-65 keypair 3732866 cycles 3732866 cycles 1
ML-DSA-65 sign 15034558 cycles 15034558 cycles 1
ML-DSA-65 verify 4012806 cycles 4012806 cycles 1
ML-DSA-87 keypair 6516715 cycles 6516715 cycles 1
ML-DSA-87 sign 25055900 cycles 25055900 cycles 1
ML-DSA-87 verify 6865674 cycles 6865674 cycles 1

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 23, 2026
View reviewed changes

@github-actions github-actions Bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 2332104 cycles 2332104 cycles 1
ML-DSA-44 sign 17791726 cycles 17791726 cycles 1
ML-DSA-44 verify 2398861 cycles 2398861 cycles 1
ML-DSA-65 keypair 4028005 cycles 4028005 cycles 1
ML-DSA-65 sign 15034565 cycles 15034565 cycles 1
ML-DSA-65 verify 4012799 cycles 4012799 cycles 1
ML-DSA-87 keypair 6896513 cycles 6896513 cycles 1
ML-DSA-87 sign 25049115 cycles 25049115 cycles 1
ML-DSA-87 verify 6864412 cycles 6864412 cycles 1

This comment was automatically generated by workflow using github-action-benchmark.

@soumya2094
soumya2094 force-pushed the x3-hybrid-keccak-f1600 branch from d3db6bf to a59eb86 Compare October 23, 2026 19:01
@soumya2094
FIPS202/AArch64: Add symbolic Keccak sources and SLOTHY Makefile
772e436 
Port the symbolic Keccak-f1600 sources and SLOTHY recipes from
mlkem-native, so that `autogen --slothy` regenerates the existing x1 and
x4 kernels and the SLOTHY CI job tests them.

Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
FIPS202: Add 3-way batched Keccak-f1600 with an AArch64 hybrid backend
a7b795b 
Add an opt-in 3-way Keccak-f1600 (MLD_CONFIG_USE_X3) with a C fallback
and an AArch64 kernel that runs two states on Neon with SHA3 and one on
scalar registers. It targets cores that issue SHA3 on all SIMD pipes,
such as Neoverse V3. Default builds are unchanged.

Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
HOL-Light: Prove the x3 hybrid Keccak-f1600 kernel
9905ad3 
Prove functional correctness, ABI compliance, memory safety and
constant-time behaviour of the x3 kernel, following the x4 v84a proof.

Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
Integration of the 3-way batched kernel with MLD_CONFIG_USE_X3
8d76177 
Sample three polynomials per XOF call when MLD_CONFIG_USE_X3 is set
(Batch ExpandA, ExpandS and ExpandMask). Nonces are unchanged, so
outputs match the default path.

Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
test: Add an x3 test configuration and update component benchmarks
8dc139b 
Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
CBMC: Add proofs for the 3-way batched Keccak and samplers
f71add1 
Mirror the existing proofs for the x3 primitives, samplers and callers,
built with MLD_CONFIG_USE_X3.

Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
CI: Test the x3 configuration
c2d8b2a 
Run the x3 config variation and the x3_v84a_scalar backend tests, and
test the regenerated x3 kernel in the SLOTHY job.

Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
bench: Benchmark the x3 Keccak on Graviton 5
b622325 
Use MLD_CONFIG_USE_X3 instead of MLD_SYS_AARCH64_FAST_SHA3, which would
select x2_v84a ahead of x3.

Signed-off-by: Soumya Bhattacharya <somoamz@amazon.com>
@soumya2094
soumya2094 force-pushed the x3-hybrid-keccak-f1600 branch from a59eb86 to b622325 Compare October 25, 2026 05:17
github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Mac Mini (M1, 2020) benchmarks (opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 47124 cycles 47125 cycles 1.00
ML-DSA-44 sign 131342 cycles 131417 cycles 1.00
ML-DSA-44 verify 47314 cycles 47389 cycles 1.00
ML-DSA-65 keypair 81742 cycles 81744 cycles 1.00
ML-DSA-65 sign 215162 cycles 215169 cycles 1.00
ML-DSA-65 verify 79288 cycles 79285 cycles 1.00
ML-DSA-87 keypair 133554 cycles 133554 cycles 1
ML-DSA-87 sign 277601 cycles 277736 cycles 1.00
ML-DSA-87 verify 134234 cycles 134284 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Mac Mini (M1, 2020) benchmarks (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 114120 cycles 113818 cycles 1.00
ML-DSA-44 sign 405053 cycles 404019 cycles 1.00
ML-DSA-44 verify 120713 cycles 120395 cycles 1.00
ML-DSA-65 keypair 193995 cycles 193966 cycles 1.00
ML-DSA-65 sign 653976 cycles 653692 cycles 1.00
ML-DSA-65 verify 193058 cycles 192991 cycles 1.00
ML-DSA-87 keypair 320045 cycles 320177 cycles 1.00
ML-DSA-87 sign 831241 cycles 831648 cycles 1.00
ML-DSA-87 verify 326885 cycles 326995 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A55 (Snapdragon 888) benchmarks (opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 273654 cycles 270571 cycles 1.01
ML-DSA-44 sign 823084 cycles 809712 cycles 1.02
ML-DSA-44 verify 275348 cycles 270186 cycles 1.02
ML-DSA-65 keypair 468014 cycles 463085 cycles 1.01
ML-DSA-65 sign 1331770 cycles 1323109 cycles 1.01
ML-DSA-65 verify 455497 cycles 446841 cycles 1.02
ML-DSA-87 keypair 800712 cycles 789701 cycles 1.01
ML-DSA-87 sign 1841227 cycles 1780296 cycles 1.03
ML-DSA-87 verify 774202 cycles 766029 cycles 1.01

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Arm Cortex-A55 (Snapdragon 888) benchmarks (opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-87 sign 1841227 cycles 1780296 cycles 1.03

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A55 (Snapdragon 888) benchmarks (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 461384 cycles 460388 cycles 1.00
ML-DSA-44 sign 2126110 cycles 2122332 cycles 1.00
ML-DSA-44 verify 552373 cycles 549592 cycles 1.01
ML-DSA-65 keypair 774902 cycles 772173 cycles 1.00
ML-DSA-65 sign 3476487 cycles 3460868 cycles 1.00
ML-DSA-65 verify 857005 cycles 855394 cycles 1.00
ML-DSA-87 keypair 1248658 cycles 1247284 cycles 1.00
ML-DSA-87 sign 4315667 cycles 4263921 cycles 1.01
ML-DSA-87 verify 1369497 cycles 1366794 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 214542 cycles 213756 cycles 1.00
ML-DSA-44 sign 585737 cycles 584182 cycles 1.00
ML-DSA-44 verify 211481 cycles 210896 cycles 1.00
ML-DSA-65 keypair 374245 cycles 373873 cycles 1.00
ML-DSA-65 sign 969476 cycles 962846 cycles 1.01
ML-DSA-65 verify 357454 cycles 355854 cycles 1.00
ML-DSA-87 keypair 629791 cycles 628671 cycles 1.00
ML-DSA-87 sign 1286836 cycles 1297569 cycles 0.99
ML-DSA-87 verify 607627 cycles 606774 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 293004 cycles 295318 cycles 0.99
ML-DSA-44 sign 1111099 cycles 1110298 cycles 1.00
ML-DSA-44 verify 322481 cycles 322756 cycles 1.00
ML-DSA-65 keypair 535827 cycles 536415 cycles 1.00
ML-DSA-65 sign 1816556 cycles 1817668 cycles 1.00
ML-DSA-65 verify 515271 cycles 514367 cycles 1.00
ML-DSA-87 keypair 823658 cycles 825690 cycles 1.00
ML-DSA-87 sign 2298373 cycles 2325584 cycles 0.99
ML-DSA-87 verify 850451 cycles 852301 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

github-actions[bot]
github-actions Bot reviewed Oct 25, 2026
View reviewed changes

@github-actions github-actions Bot 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.

SpacemiT K1 8 (Banana Pi F3) benchmarks (no-opt)

Details
Benchmark suite Current: b622325 Previous: 4ec47ce Ratio
ML-DSA-44 keypair 765612 cycles 764774 cycles 1.00
ML-DSA-44 sign 3142110 cycles 3144213 cycles 1.00
ML-DSA-44 verify 858484 cycles 858080 cycles 1.00
ML-DSA-65 keypair 1289359 cycles 1289582 cycles 1.00
ML-DSA-65 sign 5090080 cycles 5087169 cycles 1.00
ML-DSA-65 verify 1366208 cycles 1366024 cycles 1.00
ML-DSA-87 keypair 2122994 cycles 2122831 cycles 1.00
ML-DSA-87 sign 6370419 cycles 6356312 cycles 1.00
ML-DSA-87 verify 2224945 cycles 2225428 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

This branch has not been deployed

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

Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments
@oqs-bot oqs-bot oqs-bot left review comments
@hanno-becker hanno-becker Awaiting requested review from hanno-becker

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

benchmark

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@soumya2094 @oqs-bot @hanno-becker