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

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 43680 cycles 43892 cycles 1.00
ML-DSA-44 sign 130377 cycles 130352 cycles 1.00
ML-DSA-44 verify 45029 cycles 45321 cycles 0.99
ML-DSA-65 keypair 75946 cycles 74796 cycles 1.02
ML-DSA-65 sign 212592 cycles 212052 cycles 1.00
ML-DSA-65 verify 74260 cycles 74687 cycles 0.99
ML-DSA-87 keypair 123762 cycles 124114 cycles 1.00
ML-DSA-87 sign 271004 cycles 271590 cycles 1.00
ML-DSA-87 verify 120269 cycles 120181 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.

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

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 91928 cycles 91784 cycles 1.00
ML-DSA-44 sign 349226 cycles 347134 cycles 1.01
ML-DSA-44 verify 99353 cycles 99097 cycles 1.00
ML-DSA-65 keypair 155553 cycles 155539 cycles 1.00
ML-DSA-65 sign 568211 cycles 568531 cycles 1.00
ML-DSA-65 verify 159741 cycles 159884 cycles 1.00
ML-DSA-87 keypair 257558 cycles 258198 cycles 1.00
ML-DSA-87 sign 720923 cycles 721227 cycles 1.00
ML-DSA-87 verify 263802 cycles 263911 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.

AMD EPYC 4th gen (c7a)

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 48013 cycles 47813 cycles 1.00
ML-DSA-44 sign 139567 cycles 139235 cycles 1.00
ML-DSA-44 verify 49580 cycles 49422 cycles 1.00
ML-DSA-65 keypair 83610 cycles 82246 cycles 1.02
ML-DSA-65 sign 227283 cycles 226854 cycles 1.00
ML-DSA-65 verify 82430 cycles 82296 cycles 1.00
ML-DSA-87 keypair 133550 cycles 143586 cycles 0.93
ML-DSA-87 sign 281368 cycles 297737 cycles 0.95
ML-DSA-87 verify 129022 cycles 135636 cycles 0.95

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.

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

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 115181 cycles 115553 cycles 1.00
ML-DSA-44 sign 420451 cycles 420266 cycles 1.00
ML-DSA-44 verify 123976 cycles 123836 cycles 1.00
ML-DSA-65 keypair 201173 cycles 195371 cycles 1.03
ML-DSA-65 sign 702261 cycles 681845 cycles 1.03
ML-DSA-65 verify 206914 cycles 199906 cycles 1.04
ML-DSA-87 keypair 327447 cycles 323445 cycles 1.01
ML-DSA-87 sign 876520 cycles 865156 cycles 1.01
ML-DSA-87 verify 332860 cycles 329502 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.

AMD EPYC 3rd gen (c6a)

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 52571 cycles 52581 cycles 1.00
ML-DSA-44 sign 156199 cycles 156021 cycles 1.00
ML-DSA-44 verify 54209 cycles 54219 cycles 1.00
ML-DSA-65 keypair 91040 cycles 90741 cycles 1.00
ML-DSA-65 sign 256089 cycles 253497 cycles 1.01
ML-DSA-65 verify 90875 cycles 89864 cycles 1.01
ML-DSA-87 keypair 145090 cycles 144894 cycles 1.00
ML-DSA-87 sign 310415 cycles 310365 cycles 1.00
ML-DSA-87 verify 138916 cycles 138533 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

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 47615 cycles 52381 cycles 0.91
ML-DSA-44 sign 161328 cycles 162344 cycles 0.99
ML-DSA-44 verify 51792 cycles 54748 cycles 0.95
ML-DSA-65 keypair 78694 cycles 91462 cycles 0.86
ML-DSA-65 sign 251056 cycles 266209 cycles 0.94
ML-DSA-65 verify 78812 cycles 89927 cycles 0.88
ML-DSA-87 keypair 133145 cycles 147757 cycles 0.90
ML-DSA-87 sign 315602 cycles 335735 cycles 0.94
ML-DSA-87 verify 131890 cycles 145717 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

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 63794 cycles 63972 cycles 1.00
ML-DSA-44 sign 193152 cycles 192594 cycles 1.00
ML-DSA-44 verify 68112 cycles 68102 cycles 1.00
ML-DSA-65 keypair 110758 cycles 110499 cycles 1.00
ML-DSA-65 sign 319862 cycles 317866 cycles 1.01
ML-DSA-65 verify 111940 cycles 111858 cycles 1.00
ML-DSA-87 keypair 174282 cycles 174451 cycles 1.00
ML-DSA-87 sign 383099 cycles 382753 cycles 1.00
ML-DSA-87 verify 173065 cycles 172460 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.

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

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 133501 cycles 133932 cycles 1.00
ML-DSA-44 sign 520671 cycles 521267 cycles 1.00
ML-DSA-44 verify 146039 cycles 146376 cycles 1.00
ML-DSA-65 keypair 224039 cycles 223907 cycles 1.00
ML-DSA-65 sign 847408 cycles 847623 cycles 1.00
ML-DSA-65 verify 234055 cycles 233902 cycles 1.00
ML-DSA-87 keypair 370647 cycles 369652 cycles 1.00
ML-DSA-87 sign 1060600 cycles 1060611 cycles 1.00
ML-DSA-87 verify 381641 cycles 381015 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.

Graviton5 (no-opt)

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 104029 cycles 101790 cycles 1.02
ML-DSA-44 sign 373735 cycles 372835 cycles 1.00
ML-DSA-44 verify 111277 cycles 111489 cycles 1.00
ML-DSA-65 keypair 178286 cycles 177590 cycles 1.00
ML-DSA-65 sign 624867 cycles 605385 cycles 1.03
ML-DSA-65 verify 178378 cycles 180402 cycles 0.99
ML-DSA-87 keypair 284291 cycles 286904 cycles 0.99
ML-DSA-87 sign 758407 cycles 771012 cycles 0.98
ML-DSA-87 verify 296244 cycles 296923 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 '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

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 167628 cycles 164444 cycles 1.02
ML-DSA-44 sign 637332 cycles 613041 cycles 1.04
ML-DSA-44 verify 182921 cycles 178255 cycles 1.03
ML-DSA-65 keypair 281401 cycles 276679 cycles 1.02
ML-DSA-65 sign 1025048 cycles 986251 cycles 1.04
ML-DSA-65 verify 290195 cycles 285766 cycles 1.02
ML-DSA-87 keypair 462971 cycles 465364 cycles 0.99
ML-DSA-87 sign 1273807 cycles 1272841 cycles 1.00
ML-DSA-87 verify 473739 cycles 477079 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

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 68336 cycles 68548 cycles 1.00
ML-DSA-44 sign 198908 cycles 198745 cycles 1.00
ML-DSA-44 verify 70491 cycles 70395 cycles 1.00
ML-DSA-65 keypair 120427 cycles 120272 cycles 1.00
ML-DSA-65 sign 326099 cycles 326165 cycles 1.00
ML-DSA-65 verify 117011 cycles 117105 cycles 1.00
ML-DSA-87 keypair 198499 cycles 198169 cycles 1.00
ML-DSA-87 sign 422021 cycles 421826 cycles 1.00
ML-DSA-87 verify 193723 cycles 193692 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 '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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 sign 637332 cycles 613041 cycles 1.04
ML-DSA-65 sign 1025048 cycles 986251 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

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 129797 cycles 129893 cycles 1.00
ML-DSA-44 sign 444007 cycles 444053 cycles 1.00
ML-DSA-44 verify 137962 cycles 137741 cycles 1.00
ML-DSA-65 keypair 227324 cycles 226863 cycles 1.00
ML-DSA-65 sign 718269 cycles 717850 cycles 1.00
ML-DSA-65 verify 223034 cycles 222758 cycles 1.00
ML-DSA-87 keypair 369617 cycles 368612 cycles 1.00
ML-DSA-87 sign 923542 cycles 918892 cycles 1.01
ML-DSA-87 verify 374434 cycles 373208 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

Copy link
Copy Markdown

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 113409 cycles 113367 cycles 1.00
ML-DSA-44 sign 354615 cycles 354349 cycles 1.00
ML-DSA-44 verify 117337 cycles 117187 cycles 1.00
ML-DSA-65 keypair 195445 cycles 195613 cycles 1.00
ML-DSA-65 sign 583606 cycles 583472 cycles 1.00
ML-DSA-65 verify 193220 cycles 192998 cycles 1.00
ML-DSA-87 keypair 322156 cycles 322109 cycles 1.00
ML-DSA-87 sign 746769 cycles 747503 cycles 1.00
ML-DSA-87 verify 317803 cycles 317934 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.

Graviton3

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 72327 cycles 72458 cycles 1.00
ML-DSA-44 sign 209805 cycles 210057 cycles 1.00
ML-DSA-44 verify 74806 cycles 74904 cycles 1.00
ML-DSA-65 keypair 126707 cycles 126792 cycles 1.00
ML-DSA-65 sign 345011 cycles 345502 cycles 1.00
ML-DSA-65 verify 124083 cycles 124401 cycles 1.00
ML-DSA-87 keypair 208206 cycles 207975 cycles 1.00
ML-DSA-87 sign 439777 cycles 444575 cycles 0.99
ML-DSA-87 verify 204510 cycles 204246 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

Copy link
Copy Markdown

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: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 210377 cycles 210851 cycles 1.00
ML-DSA-44 sign 756533 cycles 757357 cycles 1.00
ML-DSA-44 verify 227405 cycles 227295 cycles 1.00
ML-DSA-65 keypair 372911 cycles 373515 cycles 1.00
ML-DSA-65 sign 1240327 cycles 1240923 cycles 1.00
ML-DSA-65 verify 368410 cycles 368246 cycles 1.00
ML-DSA-87 keypair 597217 cycles 596578 cycles 1.00
ML-DSA-87 sign 1576029 cycles 1577517 cycles 1.00
ML-DSA-87 verify 610623 cycles 611193 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.

Graviton3 (no-opt)

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 140635 cycles 140841 cycles 1.00
ML-DSA-44 sign 490204 cycles 490852 cycles 1.00
ML-DSA-44 verify 151190 cycles 151175 cycles 1.00
ML-DSA-65 keypair 247166 cycles 246563 cycles 1.00
ML-DSA-65 sign 797577 cycles 796889 cycles 1.00
ML-DSA-65 verify 244622 cycles 244245 cycles 1.00
ML-DSA-87 keypair 400731 cycles 400472 cycles 1.00
ML-DSA-87 sign 1023606 cycles 1019557 cycles 1.00
ML-DSA-87 verify 408186 cycles 407941 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.

Graviton2

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 113649 cycles 113660 cycles 1.00
ML-DSA-44 sign 354617 cycles 355176 cycles 1.00
ML-DSA-44 verify 117273 cycles 117527 cycles 1.00
ML-DSA-65 keypair 195628 cycles 195686 cycles 1.00
ML-DSA-65 sign 583751 cycles 584392 cycles 1.00
ML-DSA-65 verify 193138 cycles 193432 cycles 1.00
ML-DSA-87 keypair 322592 cycles 323313 cycles 1.00
ML-DSA-87 sign 748993 cycles 747941 cycles 1.00
ML-DSA-87 verify 318836 cycles 318438 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.

Graviton2 (no-opt)

Details
Benchmark suite Current: d3db6bf Previous: d7b1b6d Ratio
ML-DSA-44 keypair 210432 cycles 210813 cycles 1.00
ML-DSA-44 sign 757046 cycles 757480 cycles 1.00
ML-DSA-44 verify 227990 cycles 227902 cycles 1.00
ML-DSA-65 keypair 373700 cycles 373594 cycles 1.00
ML-DSA-65 sign 1242366 cycles 1242050 cycles 1.00
ML-DSA-65 verify 369338 cycles 369085 cycles 1.00
ML-DSA-87 keypair 598551 cycles 597718 cycles 1.00
ML-DSA-87 sign 1597278 cycles 1577558 cycles 1.01
ML-DSA-87 verify 610865 cycles 611383 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

Copy link
Copy Markdown

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: d3db6bf Previous: d7b1b6d 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

Copy link
Copy Markdown

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: d3db6bf Previous: d7b1b6d 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

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.

2 participants

@soumya2094 @oqs-bot