Skip to content

CI: gate SLOTHY and add label to trigger it - #1384

Open
L-series wants to merge 2 commits into
mainfrom
ci-slothy-path-and-label-gating
Open

CI: gate SLOTHY and add label to trigger it#1384
L-series wants to merge 2 commits into
mainfrom
ci-slothy-path-and-label-gating

Conversation

@L-series

@L-series L-series commented Aug 17, 2026

Copy link
Copy Markdown
Contributor

@L-series
L-series requested a review from a team as a code owner August 17, 2026 02:16
@L-series

Copy link
Copy Markdown
Contributor Author

Resolves: #1175

@mkannwischer

Copy link
Copy Markdown
Contributor

@L-series, please next time check if someone is already assigned to an issue. I have this half finished locally, but you can take over.

@oqs-bot

oqs-bot commented Aug 17, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 35s 7s +400%
mld_attempt_signature_generation ⚠️ 170s 31s +448%
sign_keypair_internal ⚠️ 30s 3s +900%
sign_pk_from_sk ⚠️ 61s 5s +1120%
sign_verify_internal ⚠️ 191s 71s +169%
Full Results (210 proofs)
Proof Status Current Previous Change
**TOTAL** 1500s 1482s +1.2%
sign_verify_internal ⚠️ 191s 71s +169%
mld_attempt_signature_generation ⚠️ 170s 31s +448%
polyvec_matrix_pointwise_montgomery_yvec 156s 201s -22%
poly_pointwise_montgomery_c 72s 116s -38%
mld_invntt_layer 67s 108s -38%
sign_pk_from_sk ⚠️ 61s 5s +1120%
polyvecl_chknorm 57s 43s +33%
compute_pack_t0_t1 ⚠️ 35s 7s +400%
sign_keypair_internal ⚠️ 30s 3s +900%
fqmul 25s 40s -38%
mld_ntt_layer 24s 43s -44%
keccakf1600x4_permute_native 13s 22s -41%
polyt0_unpack 13s 13s +0%
sign_signature_internal 13s 6s +117%
mld_ntt_butterfly_block 12s 25s -52%
rej_uniform_c 12s 16s -25%
rej_uniform 11s 7s +57%
rej_uniform_native_x86_64 11s - new
sig_unpack_hints 11s 1s +1000%
poly_ntt_c 9s 22s -59%
poly_uniform_eta_4x 8s 13s -38%
keccak_absorb_once_x4 6s 10s -40%
poly_invntt_tomont_c 6s 10s -40%
polyeta_unpack 6s 4s +50%
polyveck_decompose 6s 14s -57%
polyvecl_ntt 6s 7s -14%
mld_check_pct 5s 12s -58%
poly_chknorm_c 5s 13s -62%
polyvec_matrix_pointwise_montgomery_row 5s 8s -38%
polyveck_caddq 5s 7s -29%
polyveck_invntt_tomont 5s 7s -29%
polyveck_reduce 5s 6s -17%
polyvecl_pointwise_acc_montgomery_native 5s 3s +67%
polyvecl_uniform_gamma1_serial 5s 1s +400%
sign_signature_pre_hash_shake256 5s 7s -29%
yvec_init 5s 5s +0%
keccak_squeezeblocks_x4 4s 4s +0%
keccakf1600_permute_native 4s 2s +100%
mld_ct_get_optblocker_u32 4s 3s +33%
mld_ct_memcmp 4s 4s +0%
montgomery_reduce 4s 1s +300%
ntt_native_x86_64 4s 5s -20%
pack_sk_s1 4s 3s +33%
poly_decompose_c 4s 8s -50%
poly_permute_bitrev_to_custom_optional_native 4s 3s +33%
poly_power2round 4s 7s -43%
poly_use_hint_c 4s 2s +100%
polyz_unpack_17_native_aarch64 4s 2s +100%
polyz_unpack_c 4s 9s -56%
reduce32 4s 2s +100%
rej_eta 4s 5s -20%
rej_uniform_native_aarch64 4s 5s -20%
shake256 4s 2s +100%
sign_keypair 4s 4s +0%
sign_signature_extmu 4s 4s +0%
sign_verify_extmu 4s 2s +100%
unpack_pk_t1 4s 2s +100%
unpack_sk_s1hat 4s 1s +300%
intt_native_x86_64 3s 4s -25%
keccak_absorb 3s 3s +0%
keccak_f1600_x1_native_aarch64 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 3s +0%
keccak_f1600_x4_native_avx2 3s 2s +50%
keccakf1600_xor_bytes (big endian) 3s 2s +50%
keccakf1600x4_extract_bytes_native 3s 1s +200%
keccakf1600x4_xor_bytes 3s 2s +50%
make_hint 3s 3s +0%
mld_ct_abs_i32 3s 6s -50%
mld_ct_cmask_neg_i32 3s 3s +0%
mld_ct_get_optblocker_i64 3s 1s +200%
mld_keccakf1600_permute_c 3s 7s -57%
mld_prepare_domain_separation_prefix 3s 4s -25%
mld_sample_s1_s2_serial 3s 3s +0%
mld_sign_resume 3s - new
mld_value_barrier_i64 3s 2s +50%
ntt_native_aarch64 3s 3s +0%
pack_sk_rho_key_tr_s2 3s 2s +50%
pointwise_acc_native_x86_64 3s 5s -40%
pointwise_native_aarch64 3s 3s +0%
pointwise_native_x86_64 3s 2s +50%
poly_add 3s 7s -57%
poly_caddq_native_aarch64 3s 2s +50%
poly_caddq_native_x86_64 3s 1s +200%
poly_challenge 3s 5s -40%
poly_chknorm 3s 3s +0%
poly_chknorm_native_aarch64 3s 2s +50%
poly_chknorm_native_x86_64 3s 4s -25%
poly_decompose 3s 2s +50%
poly_decompose_88_native_aarch64 3s 2s +50%
poly_decompose_native 3s 5s -40%
poly_decompose_native_x86_64 3s 2s +50%
poly_invntt_tomont_native 3s 5s -40%
poly_ntt 3s 2s +50%
poly_pointwise_montgomery_native 3s 4s -25%
poly_reduce 3s 4s -25%
poly_use_hint 3s 3s +0%
polyt1_pack 3s 3s +0%
polyt1_unpack 3s 3s +0%
polyveck_pack_w1 3s 4s -25%
polyvecl_pack_eta 3s 2s +50%
polyvecl_pointwise_acc_montgomery 3s 3s +0%
polyw1_pack 3s 3s +0%
polyw1_pack_88 3s 3s +0%
polyz_pack 3s 3s +0%
polyz_unpack 3s 3s +0%
polyz_unpack_19_native_aarch64 3s 5s -40%
rej_uniform_eta_native_x86_64 3s - new
sign_signature 3s 5s -40%
sign_verify_pre_hash_internal 3s 5s -40%
sign_verify_pre_hash_shake256 3s 6s -50%
sk_s1hat_get_poly 3s 3s +0%
sk_s2hat_get_poly 3s 1s +200%
sk_t0hat_get_poly 3s 1s +200%
sys_check_capability 3s 1s +200%
unpack_sk_s2hat 3s 3s +0%
unpack_sk_t0hat 3s 4s -25%
caddq 2s 2s +0%
fqscale 2s 3s -33%
intt_native_aarch64 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 2s 3s -33%
keccak_squeeze 2s 2s +0%
keccakf1600_xor_bytes 2s 4s -50%
keccakf1600x4_extract_bytes 2s 4s -50%
keccakf1600x4_permute 2s 1s +100%
keccakf1600x4_xor_bytes_native 2s 2s +0%
mld_compute_pack_z 2s 5s -60%
mld_ct_cmask_nonzero_u8 2s 2s +0%
mld_ct_sel_int32 2s 2s +0%
mld_h 2s 3s -33%
mld_keccakf1600_extract_bytes 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c 2s 2s +0%
mld_polymat_expand_entry 2s 3s -33%
mld_sample_s1_s2 2s 6s -67%
mld_sign_finish 2s - new
mld_value_barrier_u8 2s 1s +100%
nttunpack_native_x86_64 2s 3s -33%
pack_sig_c 2s 3s -33%
pack_sig_h 2s 2s +0%
pack_sig_z 2s 1s +100%
pointwise_acc_native_aarch64 2s 6s -67%
poly_caddq 2s 3s -33%
poly_caddq_c 2s 5s -60%
poly_caddq_native 2s 4s -50%
poly_chknorm_native 2s 4s -50%
poly_decompose_32_native_aarch64 2s 4s -50%
poly_invntt_tomont 2s 5s -60%
poly_ntt_native 2s 2s +0%
poly_permute_bitrev_to_custom_optional 2s 3s -33%
poly_pointwise_montgomery 2s 2s +0%
poly_shiftl 2s 3s -33%
poly_sub 2s 4s -50%
poly_uniform 2s 2s +0%
poly_uniform_gamma1_4x 2s 3s -33%
poly_use_hint_native 2s 7s -71%
poly_use_hint_native_x86_64 2s - new
polyt0_pack 2s 5s -60%
polyvec_matrix_expand 2s 6s -67%
polyveck_pack_eta 2s 3s -33%
polyveck_unpack_eta 2s 3s -33%
polyvecl_pointwise_acc_montgomery_c 2s 3s -33%
polyvecl_unpack_eta 2s 2s +0%
polyvecl_unpack_z 2s 1s +100%
polyz_unpack_native 2s 3s -33%
polyz_unpack_native_x86_64 2s 3s -33%
rej_uniform_eta_native_aarch64 2s 5s -60%
rej_uniform_native 2s 4s -50%
shake128_init 2s 6s -67%
shake128_release 2s 2s +0%
shake128_squeeze 2s 3s -33%
shake128x4_squeezeblocks 2s 2s +0%
shake256_absorb 2s 4s -50%
shake256_finalize 2s 1s +100%
shake256_init 2s 4s -50%
shake256_release 2s 3s -33%
shake256_squeeze 2s 4s -50%
shake256x4_squeezeblocks 2s 2s +0%
sign_signature_pre_hash_internal 2s 3s -33%
unpack_sk 2s 3s -33%
yvec_get_poly 2s 3s -33%
decompose 1s 4s -75%
keccak_f1600_x1_native_aarch64_v84a 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a 1s 2s -50%
keccak_finalize 1s 2s -50%
keccak_init 1s 4s -75%
keccakf1600_extract_bytes (big endian) 1s 3s -67%
keccakf1600_permute 1s 4s -75%
mld_ct_cmask_nonzero_u32 1s 3s -67%
mld_ct_get_optblocker_u8 1s 4s -75%
mld_keccakf1600x4_extract_bytes_c 1s 2s -50%
mld_sign_attempt 1s - new
mld_value_barrier_u32 1s 4s -75%
poly_uniform_4x 1s 4s -75%
poly_uniform_eta 1s 5s -80%
poly_uniform_gamma1 1s 3s -67%
poly_use_hint_native_aarch64 1s 4s -75%
polyeta_pack 1s 1s +0%
polyvec_matrix_expand_serial 1s 3s -67%
polyveck_chknorm 1s 36s -97%
polyveck_ntt 1s 4s -75%
polyvecl_uniform_gamma1 1s 4s -75%
polyw1_pack_32 1s 2s -50%
power2round 1s 2s -50%
rej_eta_c 1s 4s -75%
rej_eta_native 1s 3s -67%
shake128_absorb 1s 2s -50%
shake128_finalize 1s 2s -50%
shake128x4_absorb_once 1s 2s -50%
shake256x4_absorb_once 1s 2s -50%
sign_verify 1s 6s -83%
use_hint 1s 2s -50%

@oqs-bot

oqs-bot commented Aug 17, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 30s 12s +150%
mld_attempt_signature_generation ⚠️ 160s 19s +742%
sign_keypair_internal ⚠️ 21s 4s +425%
sign_pk_from_sk ⚠️ 42s 5s +740%
sign_verify_internal ⚠️ 174s 49s +255%
Full Results (210 proofs)
Proof Status Current Previous Change
**TOTAL** 1300s 1364s -4.7%
sign_verify_internal ⚠️ 174s 49s +255%
mld_attempt_signature_generation ⚠️ 160s 19s +742%
polyvec_matrix_pointwise_montgomery_yvec 106s 149s -29%
poly_pointwise_montgomery_c 68s 112s -39%
mld_invntt_layer 61s 105s -42%
sign_pk_from_sk ⚠️ 42s 5s +740%
compute_pack_t0_t1 ⚠️ 30s 12s +150%
fqmul 24s 39s -38%
mld_ntt_layer 21s 41s -49%
sign_keypair_internal ⚠️ 21s 4s +425%
keccakf1600x4_permute_native 13s 22s -41%
mld_ntt_butterfly_block 13s 23s -43%
rej_uniform_c 12s 16s -25%
sig_unpack_hints 12s 2s +500%
sign_signature_internal 12s 4s +200%
poly_ntt_c 11s 21s -48%
rej_uniform 11s 8s +38%
polyt0_unpack 9s 12s -25%
rej_uniform_native_x86_64 9s - new
poly_uniform_eta_4x 8s 12s -33%
polyz_unpack_c 8s 8s +0%
poly_chknorm_c 7s 11s -36%
polyeta_unpack 7s 14s -50%
keccak_absorb 6s 3s +100%
mld_check_pct 6s 15s -60%
poly_invntt_tomont_c 6s 11s -45%
polyvec_matrix_pointwise_montgomery_row 6s 6s +0%
polyveck_decompose 6s 7s -14%
sign_keypair 6s 5s +20%
sign_signature_pre_hash_shake256 6s 4s +50%
caddq 5s 6s -17%
mld_compute_pack_z 5s 6s -17%
polyt1_unpack 5s 2s +150%
polyvecl_pointwise_acc_montgomery_c 5s 4s +25%
rej_uniform_native 5s 5s +0%
sign_signature_extmu 5s 4s +25%
fqscale 4s 2s +100%
mld_h 4s 4s +0%
mld_keccakf1600_permute_c 4s 7s -43%
mld_value_barrier_u32 4s 1s +300%
pack_sig_z 4s 2s +100%
pointwise_acc_native_aarch64 4s 6s -33%
poly_use_hint 4s 2s +100%
polyvecl_uniform_gamma1_serial 4s 2s +100%
polyw1_pack 4s 4s +0%
polyz_pack 4s 2s +100%
polyz_unpack_19_native_aarch64 4s 4s +0%
polyz_unpack_native_x86_64 4s 3s +33%
sign_verify 4s 4s +0%
sign_verify_pre_hash_shake256 4s 5s -20%
intt_native_x86_64 3s 2s +50%
keccak_absorb_once_x4 3s 8s -62%
keccak_f1600_x4_native_aarch64_v84a 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 2s +50%
keccak_finalize 3s 2s +50%
keccak_init 3s 3s +0%
keccakf1600x4_xor_bytes_native 3s 5s -40%
make_hint 3s 3s +0%
mld_ct_cmask_nonzero_u32 3s 3s +0%
mld_ct_get_optblocker_i64 3s 4s -25%
mld_keccakf1600_extract_bytes 3s 2s +50%
mld_keccakf1600x4_extract_bytes_c 3s 4s -25%
mld_sample_s1_s2 3s 1s +200%
mld_sample_s1_s2_serial 3s 4s -25%
montgomery_reduce 3s 2s +50%
ntt_native_aarch64 3s 4s -25%
pack_sk_rho_key_tr_s2 3s 5s -40%
pointwise_acc_native_x86_64 3s 4s -25%
poly_add 3s 7s -57%
poly_caddq_c 3s 3s +0%
poly_caddq_native 3s 3s +0%
poly_challenge 3s 6s -50%
poly_chknorm 3s 3s +0%
poly_chknorm_native_x86_64 3s 2s +50%
poly_decompose_32_native_aarch64 3s 4s -25%
poly_decompose_native_x86_64 3s 2s +50%
poly_ntt_native 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native 3s 3s +0%
poly_power2round 3s 4s -25%
poly_sub 3s 3s +0%
poly_uniform 3s 3s +0%
poly_uniform_eta 3s 2s +50%
poly_use_hint_c 3s 5s -40%
poly_use_hint_native_aarch64 3s 3s +0%
polyvec_matrix_expand 3s 3s +0%
polyveck_chknorm 3s 67s -96%
polyveck_reduce 3s 4s -25%
polyvecl_pack_eta 3s 2s +50%
polyvecl_uniform_gamma1 3s 2s +50%
polyz_unpack_17_native_aarch64 3s 2s +50%
rej_uniform_native_aarch64 3s 3s +0%
shake128_finalize 3s 3s +0%
shake128_release 3s 2s +50%
shake128_squeeze 3s 2s +50%
shake256_absorb 3s 2s +50%
shake256x4_absorb_once 3s 1s +200%
sign_signature 3s 6s -50%
sign_verify_extmu 3s 5s -40%
unpack_sk 3s 3s +0%
use_hint 3s 2s +50%
decompose 2s 3s -33%
intt_native_aarch64 2s 3s -33%
keccak_f1600_x4_native_avx2 2s 2s +0%
keccak_squeezeblocks_x4 2s 3s -33%
keccakf1600_extract_bytes (big endian) 2s 4s -50%
keccakf1600_permute_native 2s 3s -33%
keccakf1600_xor_bytes (big endian) 2s 6s -67%
keccakf1600x4_extract_bytes_native 2s 4s -50%
keccakf1600x4_permute 2s 4s -50%
mld_ct_abs_i32 2s 3s -33%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_cmask_nonzero_u8 2s 2s +0%
mld_ct_get_optblocker_u8 2s 2s +0%
mld_ct_memcmp 2s 1s +100%
mld_keccakf1600x4_xor_bytes_c 2s 4s -50%
mld_prepare_domain_separation_prefix 2s 3s -33%
mld_sign_attempt 2s - new
mld_sign_resume 2s - new
mld_value_barrier_u8 2s 4s -50%
ntt_native_x86_64 2s 3s -33%
nttunpack_native_x86_64 2s 4s -50%
pack_sig_c 2s 5s -60%
pack_sig_h 2s 4s -50%
pack_sk_s1 2s 3s -33%
pointwise_native_aarch64 2s 2s +0%
poly_caddq 2s 4s -50%
poly_caddq_native_x86_64 2s 4s -50%
poly_chknorm_native 2s 4s -50%
poly_chknorm_native_aarch64 2s 2s +0%
poly_decompose 2s 2s +0%
poly_decompose_c 2s 5s -60%
poly_decompose_native 2s 2s +0%
poly_invntt_tomont_native 2s 3s -33%
poly_ntt 2s 3s -33%
poly_permute_bitrev_to_custom_optional 2s 5s -60%
poly_shiftl 2s 4s -50%
poly_uniform_4x 2s 3s -33%
poly_use_hint_native_x86_64 2s - new
polyeta_pack 2s 3s -33%
polyt0_pack 2s 4s -50%
polyt1_pack 2s 3s -33%
polyvec_matrix_expand_serial 2s 4s -50%
polyveck_invntt_tomont 2s 5s -60%
polyveck_ntt 2s 2s +0%
polyveck_pack_w1 2s 3s -33%
polyvecl_chknorm 2s 11s -82%
polyvecl_ntt 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 3s -33%
polyvecl_pointwise_acc_montgomery_native 2s 3s -33%
polyvecl_unpack_eta 2s 4s -50%
polyvecl_unpack_z 2s 3s -33%
polyw1_pack_32 2s 3s -33%
polyz_unpack 2s 3s -33%
polyz_unpack_native 2s 3s -33%
reduce32 2s 3s -33%
rej_eta 2s 5s -60%
rej_eta_c 2s 4s -50%
rej_uniform_eta_native_x86_64 2s - new
shake128_absorb 2s 3s -33%
shake128x4_absorb_once 2s 2s +0%
shake128x4_squeezeblocks 2s 2s +0%
shake256 2s 1s +100%
shake256_init 2s 4s -50%
shake256_release 2s 1s +100%
shake256_squeeze 2s 2s +0%
shake256x4_squeezeblocks 2s 2s +0%
sign_signature_pre_hash_internal 2s 4s -50%
sign_verify_pre_hash_internal 2s 5s -60%
sk_s2hat_get_poly 2s 5s -60%
unpack_sk_s1hat 2s 3s -33%
unpack_sk_s2hat 2s 4s -50%
unpack_sk_t0hat 2s 2s +0%
yvec_init 2s 1s +100%
keccak_f1600_x1_native_aarch64 1s 3s -67%
keccak_f1600_x1_native_aarch64_v84a 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 1s 3s -67%
keccak_squeeze 1s 2s -50%
keccakf1600_permute 1s 2s -50%
keccakf1600_xor_bytes 1s 3s -67%
keccakf1600x4_extract_bytes 1s 2s -50%
keccakf1600x4_xor_bytes 1s 3s -67%
mld_ct_get_optblocker_u32 1s 2s -50%
mld_ct_sel_int32 1s 3s -67%
mld_polymat_expand_entry 1s 2s -50%
mld_sign_finish 1s - new
mld_value_barrier_i64 1s 3s -67%
pointwise_native_x86_64 1s 4s -75%
poly_caddq_native_aarch64 1s 3s -67%
poly_decompose_88_native_aarch64 1s 3s -67%
poly_invntt_tomont 1s 2s -50%
poly_pointwise_montgomery 1s 3s -67%
poly_pointwise_montgomery_native 1s 2s -50%
poly_reduce 1s 4s -75%
poly_uniform_gamma1 1s 3s -67%
poly_uniform_gamma1_4x 1s 5s -80%
poly_use_hint_native 1s 3s -67%
polyveck_caddq 1s 3s -67%
polyveck_pack_eta 1s 4s -75%
polyveck_unpack_eta 1s 2s -50%
polyw1_pack_88 1s 2s -50%
power2round 1s 2s -50%
rej_eta_native 1s 3s -67%
rej_uniform_eta_native_aarch64 1s 3s -67%
shake128_init 1s 2s -50%
shake256_finalize 1s 2s -50%
sk_s1hat_get_poly 1s 2s -50%
sk_t0hat_get_poly 1s 1s +0%
sys_check_capability 1s 2s -50%
unpack_pk_t1 1s 3s -67%
yvec_get_poly 1s 3s -67%

@oqs-bot

oqs-bot commented Aug 17, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 103s 50s +106%
mld_attempt_signature_generation ⚠️ 307s 58s +429%
sig_unpack_hints ⚠️ 22s 2s +1000%
sign_keypair_internal ⚠️ 21s 4s +425%
sign_pk_from_sk ⚠️ 38s 5s +660%
sign_signature_internal ⚠️ 100s 26s +285%
sign_verify_internal ⚠️ 299s 114s +162%
Full Results (210 proofs)
Proof Status Current Previous Change
**TOTAL** 1881s 1514s +24.2%
mld_attempt_signature_generation ⚠️ 307s 58s +429%
sign_verify_internal ⚠️ 299s 114s +162%
polyvecl_pointwise_acc_montgomery_c 156s 131s +19%
poly_pointwise_montgomery_c 146s 114s +28%
compute_pack_t0_t1 ⚠️ 103s 50s +106%
sign_signature_internal ⚠️ 100s 26s +285%
mld_invntt_layer 59s 107s -45%
sign_pk_from_sk ⚠️ 38s 5s +660%
fqmul 24s 39s -38%
mld_ntt_layer 23s 42s -45%
sig_unpack_hints ⚠️ 22s 2s +1000%
sign_keypair_internal ⚠️ 21s 4s +425%
polyvec_matrix_expand 18s 28s -36%
keccakf1600x4_permute_native 12s 22s -45%
mld_ntt_butterfly_block 12s 23s -48%
polyeta_unpack 10s 14s -29%
polyt0_unpack 10s 15s -33%
rej_uniform_c 10s 15s -33%
poly_ntt_c 9s 19s -53%
poly_uniform_4x 8s 14s -43%
poly_uniform_eta_4x 8s 11s -27%
rej_uniform 8s 18s -56%
poly_chknorm_c 7s 17s -59%
polyvec_matrix_pointwise_montgomery_yvec 7s 15s -53%
rej_uniform_native_x86_64 7s - new
sign_keypair 7s 4s +75%
keccak_absorb_once_x4 6s 9s -33%
poly_invntt_tomont_c 6s 11s -45%
polyz_unpack_c 6s 11s -45%
sign_signature_pre_hash_shake256 6s 3s +100%
intt_native_x86_64 5s 4s +25%
mld_sample_s1_s2 5s 4s +25%
montgomery_reduce 5s 3s +67%
poly_caddq_native 5s 5s +0%
poly_power2round 5s 4s +25%
poly_reduce 5s 3s +67%
keccak_squeeze 4s 1s +300%
mld_check_pct 4s 14s -71%
mld_compute_pack_z 4s 7s -43%
mld_h 4s 4s +0%
pack_sig_h 4s 3s +33%
pointwise_acc_native_aarch64 4s 4s +0%
poly_add 4s 7s -43%
poly_chknorm_native_aarch64 4s 4s +0%
poly_decompose 4s 3s +33%
poly_decompose_c 4s 4s +0%
poly_invntt_tomont 4s 4s +0%
poly_ntt_native 4s 5s -20%
poly_uniform 4s 6s -33%
poly_use_hint_native 4s 4s +0%
poly_use_hint_native_x86_64 4s - new
polyeta_pack 4s 3s +33%
polyt1_unpack 4s 5s -20%
polyveck_chknorm 4s 5s -20%
polyvecl_pointwise_acc_montgomery_native 4s 2s +100%
sign_signature 4s 3s +33%
sign_signature_extmu 4s 4s +0%
sign_verify_pre_hash_shake256 4s 5s -20%
unpack_sk 4s 3s +33%
use_hint 4s 2s +100%
yvec_get_poly 4s 3s +33%
fqscale 3s 3s +0%
intt_native_aarch64 3s 9s -67%
keccak_absorb 3s 5s -40%
keccak_f1600_x4_native_aarch64_v84a 3s 2s +50%
keccak_squeezeblocks_x4 3s 4s -25%
keccakf1600x4_xor_bytes_native 3s 3s +0%
mld_ct_cmask_nonzero_u32 3s 2s +50%
mld_ct_cmask_nonzero_u8 3s 2s +50%
mld_ct_memcmp 3s 3s +0%
mld_keccakf1600_permute_c 3s 8s -62%
mld_sign_resume 3s - new
pack_sk_rho_key_tr_s2 3s 3s +0%
pointwise_acc_native_x86_64 3s 7s -57%
pointwise_native_x86_64 3s 4s -25%
poly_caddq 3s 2s +50%
poly_challenge 3s 3s +0%
poly_chknorm 3s 4s -25%
poly_chknorm_native_x86_64 3s 2s +50%
poly_decompose_32_native_aarch64 3s 2s +50%
poly_decompose_88_native_aarch64 3s 4s -25%
poly_ntt 3s 3s +0%
poly_pointwise_montgomery 3s 3s +0%
poly_uniform_eta 3s 5s -40%
poly_uniform_gamma1_4x 3s 5s -40%
polyvec_matrix_expand_serial 3s 8s -62%
polyveck_invntt_tomont 3s 5s -40%
polyvecl_chknorm 3s 10s -70%
polyw1_pack 3s 3s +0%
polyw1_pack_88 3s 1s +200%
polyz_pack 3s 2s +50%
polyz_unpack_17_native_aarch64 3s 5s -40%
rej_uniform_native_aarch64 3s 5s -40%
shake128_squeeze 3s 1s +200%
sign_verify 3s 4s -25%
sign_verify_extmu 3s 3s +0%
sk_s2hat_get_poly 3s 2s +50%
sk_t0hat_get_poly 3s 2s +50%
keccak_f1600_x1_native_aarch64 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 3s -33%
keccak_f1600_x4_native_avx2 2s 3s -33%
keccak_finalize 2s 3s -33%
keccak_init 2s 3s -33%
keccakf1600_permute_native 2s 3s -33%
keccakf1600_xor_bytes 2s 1s +100%
keccakf1600_xor_bytes (big endian) 2s 4s -50%
keccakf1600x4_extract_bytes 2s 2s +0%
keccakf1600x4_extract_bytes_native 2s 3s -33%
keccakf1600x4_permute 2s 4s -50%
keccakf1600x4_xor_bytes 2s 2s +0%
mld_ct_get_optblocker_u32 2s 1s +100%
mld_ct_get_optblocker_u8 2s 1s +100%
mld_ct_sel_int32 2s 2s +0%
mld_keccakf1600_extract_bytes 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c 2s 2s +0%
mld_prepare_domain_separation_prefix 2s 4s -50%
mld_sample_s1_s2_serial 2s 3s -33%
mld_sign_attempt 2s - new
mld_value_barrier_u8 2s 3s -33%
ntt_native_aarch64 2s 3s -33%
ntt_native_x86_64 2s 3s -33%
pack_sig_c 2s 2s +0%
pack_sig_z 2s 4s -50%
pack_sk_s1 2s 2s +0%
pointwise_native_aarch64 2s 5s -60%
poly_caddq_c 2s 2s +0%
poly_chknorm_native 2s 4s -50%
poly_decompose_native_x86_64 2s 3s -33%
poly_permute_bitrev_to_custom_optional 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native 2s 4s -50%
poly_pointwise_montgomery_native 2s 2s +0%
poly_shiftl 2s 3s -33%
poly_sub 2s 3s -33%
poly_use_hint 2s 4s -50%
polyt0_pack 2s 2s +0%
polyt1_pack 2s 4s -50%
polyvec_matrix_pointwise_montgomery_row 2s 2s +0%
polyveck_caddq 2s 3s -33%
polyveck_decompose 2s 4s -50%
polyveck_ntt 2s 5s -60%
polyveck_pack_eta 2s 2s +0%
polyveck_pack_w1 2s 1s +100%
polyvecl_pack_eta 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 4s -50%
polyvecl_uniform_gamma1_serial 2s 2s +0%
polyvecl_unpack_z 2s 2s +0%
polyw1_pack_32 2s 2s +0%
polyz_unpack 2s 3s -33%
polyz_unpack_19_native_aarch64 2s 5s -60%
power2round 2s 3s -33%
reduce32 2s 2s +0%
rej_eta_native 2s 6s -67%
rej_uniform_eta_native_aarch64 2s 2s +0%
rej_uniform_native 2s 4s -50%
shake128_absorb 2s 2s +0%
shake128_init 2s 3s -33%
shake128_release 2s 1s +100%
shake128x4_squeezeblocks 2s 1s +100%
shake256 2s 1s +100%
shake256_absorb 2s 3s -33%
shake256_finalize 2s 2s +0%
shake256_squeeze 2s 2s +0%
shake256x4_squeezeblocks 2s 4s -50%
sign_verify_pre_hash_internal 2s 3s -33%
sk_s1hat_get_poly 2s 3s -33%
sys_check_capability 2s 4s -50%
unpack_pk_t1 2s 5s -60%
unpack_sk_s2hat 2s 4s -50%
unpack_sk_t0hat 2s 3s -33%
yvec_init 2s 3s -33%
caddq 1s 2s -50%
decompose 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 1s 1s +0%
keccakf1600_extract_bytes (big endian) 1s 2s -50%
keccakf1600_permute 1s 2s -50%
make_hint 1s 3s -67%
mld_ct_abs_i32 1s 2s -50%
mld_ct_cmask_neg_i32 1s 3s -67%
mld_ct_get_optblocker_i64 1s 4s -75%
mld_keccakf1600x4_extract_bytes_c 1s 2s -50%
mld_polymat_expand_entry 1s 3s -67%
mld_sign_finish 1s - new
mld_value_barrier_i64 1s 2s -50%
mld_value_barrier_u32 1s 2s -50%
nttunpack_native_x86_64 1s 1s +0%
poly_caddq_native_aarch64 1s 4s -75%
poly_caddq_native_x86_64 1s 4s -75%
poly_decompose_native 1s 3s -67%
poly_invntt_tomont_native 1s 4s -75%
poly_uniform_gamma1 1s 4s -75%
poly_use_hint_c 1s 3s -67%
poly_use_hint_native_aarch64 1s 2s -50%
polyveck_reduce 1s 5s -80%
polyveck_unpack_eta 1s 2s -50%
polyvecl_ntt 1s 2s -50%
polyvecl_uniform_gamma1 1s 3s -67%
polyvecl_unpack_eta 1s 2s -50%
polyz_unpack_native 1s 2s -50%
polyz_unpack_native_x86_64 1s 3s -67%
rej_eta 1s 3s -67%
rej_eta_c 1s 4s -75%
rej_uniform_eta_native_x86_64 1s - new
shake128_finalize 1s 2s -50%
shake128x4_absorb_once 1s 3s -67%
shake256_init 1s 3s -67%
shake256_release 1s 2s -50%
shake256x4_absorb_once 1s 3s -67%
sign_signature_pre_hash_internal 1s 6s -83%
unpack_sk_s1hat 1s 1s +0%

@oqs-bot

oqs-bot commented Aug 17, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 30s 12s +150%
mld_attempt_signature_generation ⚠️ 263s 34s +674%
sign_keypair_internal ⚠️ 46s 6s +667%
sign_pk_from_sk ⚠️ 65s 6s +983%
sign_verify_internal ⚠️ 330s 47s +602%
Full Results (210 proofs)
Proof Status Current Previous Change
**TOTAL** 1730s 1436s +20.5%
sign_verify_internal ⚠️ 330s 47s +602%
mld_attempt_signature_generation ⚠️ 263s 34s +674%
polyvec_matrix_pointwise_montgomery_yvec 211s 196s +8%
poly_pointwise_montgomery_c 69s 125s -45%
sign_pk_from_sk ⚠️ 65s 6s +983%
mld_invntt_layer 56s 111s -50%
sign_keypair_internal ⚠️ 46s 6s +667%
compute_pack_t0_t1 ⚠️ 30s 12s +150%
fqmul 25s 39s -36%
mld_ntt_layer 22s 44s -50%
sign_signature_internal 15s 3s +400%
keccakf1600x4_permute_native 13s 25s -48%
mld_ntt_butterfly_block 12s 23s -48%
rej_uniform_c 12s 18s -33%
sig_unpack_hints 12s 4s +200%
poly_ntt_c 10s 19s -47%
polyt0_unpack 10s 14s -29%
rej_uniform 10s 7s +43%
rej_uniform_native_x86_64 10s - new
polyeta_unpack 9s 13s -31%
polyveck_invntt_tomont 9s 4s +125%
poly_invntt_tomont_c 8s 9s -11%
mld_check_pct 7s 15s -53%
poly_uniform_eta_4x 7s 12s -42%
polyveck_decompose 7s 12s -42%
sign_keypair 7s 4s +75%
sign_signature_pre_hash_shake256 7s 3s +133%
keccak_absorb_once_x4 6s 8s -25%
mld_keccakf1600_extract_bytes 5s 1s +400%
mld_sample_s1_s2 5s 8s -38%
mld_sample_s1_s2_serial 5s 6s -17%
mld_sign_finish 5s - new
pointwise_acc_native_aarch64 5s 5s +0%
pointwise_acc_native_x86_64 5s 8s -38%
poly_chknorm_c 5s 13s -62%
poly_decompose_c 5s 6s -17%
polyz_unpack_c 5s 7s -29%
sign_verify_pre_hash_shake256 5s 7s -29%
keccak_absorb 4s 4s +0%
keccakf1600_permute_native 4s 3s +33%
keccakf1600x4_permute 4s 2s +100%
mld_compute_pack_z 4s 6s -33%
mld_ct_memcmp 4s 1s +300%
mld_keccakf1600_permute_c 4s 8s -50%
montgomery_reduce 4s 2s +100%
pack_sk_rho_key_tr_s2 4s 2s +100%
pointwise_native_x86_64 4s 5s -20%
poly_caddq_native_x86_64 4s 3s +33%
poly_chknorm_native_aarch64 4s 5s -20%
poly_decompose 4s 2s +100%
poly_decompose_88_native_aarch64 4s 2s +100%
poly_sub 4s 5s -20%
polyvec_matrix_pointwise_montgomery_row 4s 13s -69%
polyvecl_chknorm 4s 38s -89%
polyvecl_ntt 4s 8s -50%
shake256_squeeze 4s 2s +100%
sign_signature_extmu 4s 4s +0%
intt_native_x86_64 3s 4s -25%
keccak_f1600_x4_native_aarch64_v84a 3s 1s +200%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 2s +50%
keccak_squeeze 3s 5s -40%
mld_ct_abs_i32 3s 1s +200%
mld_ct_cmask_nonzero_u8 3s 2s +50%
mld_h 3s 2s +50%
mld_keccakf1600x4_extract_bytes_c 3s 3s +0%
mld_prepare_domain_separation_prefix 3s 3s +0%
mld_sign_attempt 3s - new
ntt_native_aarch64 3s 4s -25%
ntt_native_x86_64 3s 2s +50%
pack_sig_c 3s 2s +50%
pack_sk_s1 3s 2s +50%
poly_add 3s 8s -62%
poly_caddq_native 3s 3s +0%
poly_caddq_native_aarch64 3s 3s +0%
poly_challenge 3s 4s -25%
poly_chknorm_native 3s 1s +200%
poly_chknorm_native_x86_64 3s 2s +50%
poly_decompose_32_native_aarch64 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native 3s 3s +0%
poly_power2round 3s 7s -57%
poly_uniform 3s 4s -25%
poly_uniform_eta 3s 5s -40%
polyt0_pack 3s 3s +0%
polyvec_matrix_expand 3s 3s +0%
polyvec_matrix_expand_serial 3s 3s +0%
polyveck_caddq 3s 8s -62%
polyveck_reduce 3s 6s -50%
polyvecl_pointwise_acc_montgomery 3s 2s +50%
polyvecl_pointwise_acc_montgomery_c 3s 2s +50%
polyvecl_unpack_eta 3s 3s +0%
polyvecl_unpack_z 3s 3s +0%
polyw1_pack 3s 2s +50%
polyw1_pack_32 3s 3s +0%
polyz_pack 3s 4s -25%
rej_eta_c 3s 4s -25%
rej_uniform_eta_native_aarch64 3s 3s +0%
rej_uniform_eta_native_x86_64 3s - new
rej_uniform_native 3s 5s -40%
rej_uniform_native_aarch64 3s 3s +0%
shake128_finalize 3s 2s +50%
shake128x4_squeezeblocks 3s 1s +200%
shake256_absorb 3s 3s +0%
shake256x4_absorb_once 3s 5s -40%
sign_signature 3s 4s -25%
sign_signature_pre_hash_internal 3s 2s +50%
sign_verify_extmu 3s 4s -25%
sk_s1hat_get_poly 3s 3s +0%
unpack_sk_t0hat 3s 4s -25%
caddq 2s 3s -33%
decompose 2s 2s +0%
keccak_f1600_x1_native_aarch64 2s 2s +0%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_init 2s 1s +100%
keccak_squeezeblocks_x4 2s 4s -50%
keccakf1600_extract_bytes (big endian) 2s 3s -33%
keccakf1600_permute 2s 2s +0%
keccakf1600_xor_bytes (big endian) 2s 2s +0%
keccakf1600x4_extract_bytes_native 2s 4s -50%
keccakf1600x4_xor_bytes_native 2s 2s +0%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_cmask_nonzero_u32 2s 5s -60%
mld_ct_get_optblocker_i64 2s 2s +0%
mld_ct_get_optblocker_u32 2s 2s +0%
mld_ct_get_optblocker_u8 2s 3s -33%
mld_keccakf1600x4_xor_bytes_c 2s 1s +100%
mld_value_barrier_i64 2s 2s +0%
mld_value_barrier_u32 2s 3s -33%
mld_value_barrier_u8 2s 2s +0%
nttunpack_native_x86_64 2s 3s -33%
pack_sig_h 2s 3s -33%
pointwise_native_aarch64 2s 4s -50%
poly_decompose_native 2s 2s +0%
poly_decompose_native_x86_64 2s 3s -33%
poly_invntt_tomont 2s 4s -50%
poly_invntt_tomont_native 2s 2s +0%
poly_ntt 2s 2s +0%
poly_ntt_native 2s 4s -50%
poly_pointwise_montgomery 2s 3s -33%
poly_pointwise_montgomery_native 2s 3s -33%
poly_shiftl 2s 4s -50%
poly_uniform_4x 2s 3s -33%
poly_uniform_gamma1_4x 2s 3s -33%
poly_use_hint_native 2s 1s +100%
poly_use_hint_native_x86_64 2s - new
polyt1_pack 2s 5s -60%
polyt1_unpack 2s 3s -33%
polyveck_chknorm 2s 9s -78%
polyveck_ntt 2s 3s -33%
polyveck_pack_eta 2s 5s -60%
polyveck_pack_w1 2s 3s -33%
polyveck_unpack_eta 2s 3s -33%
polyvecl_pointwise_acc_montgomery_native 2s 2s +0%
polyz_unpack 2s 3s -33%
polyz_unpack_17_native_aarch64 2s 4s -50%
polyz_unpack_19_native_aarch64 2s 5s -60%
polyz_unpack_native_x86_64 2s 3s -33%
rej_eta 2s 2s +0%
shake128_absorb 2s 2s +0%
shake256_release 2s 5s -60%
sign_verify 2s 2s +0%
sign_verify_pre_hash_internal 2s 3s -33%
sk_s2hat_get_poly 2s 2s +0%
sk_t0hat_get_poly 2s 3s -33%
sys_check_capability 2s 2s +0%
unpack_pk_t1 2s 2s +0%
unpack_sk 2s 4s -50%
unpack_sk_s2hat 2s 3s -33%
yvec_get_poly 2s 2s +0%
yvec_init 2s 4s -50%
fqscale 1s 1s +0%
intt_native_aarch64 1s 4s -75%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 1s 2s -50%
keccak_f1600_x4_native_avx2 1s 3s -67%
keccak_finalize 1s 1s +0%
keccakf1600_xor_bytes 1s 1s +0%
keccakf1600x4_extract_bytes 1s 1s +0%
keccakf1600x4_xor_bytes 1s 1s +0%
make_hint 1s 2s -50%
mld_ct_sel_int32 1s 2s -50%
mld_polymat_expand_entry 1s 4s -75%
mld_sign_resume 1s - new
pack_sig_z 1s 3s -67%
poly_caddq 1s 5s -80%
poly_caddq_c 1s 3s -67%
poly_chknorm 1s 4s -75%
poly_permute_bitrev_to_custom_optional 1s 2s -50%
poly_reduce 1s 4s -75%
poly_uniform_gamma1 1s 3s -67%
poly_use_hint 1s 4s -75%
poly_use_hint_c 1s 4s -75%
poly_use_hint_native_aarch64 1s 3s -67%
polyeta_pack 1s 3s -67%
polyvecl_pack_eta 1s 2s -50%
polyvecl_uniform_gamma1 1s 3s -67%
polyvecl_uniform_gamma1_serial 1s 2s -50%
polyw1_pack_88 1s 2s -50%
polyz_unpack_native 1s 1s +0%
power2round 1s 3s -67%
reduce32 1s 3s -67%
rej_eta_native 1s 4s -75%
shake128_init 1s 2s -50%
shake128_release 1s 3s -67%
shake128_squeeze 1s 1s +0%
shake128x4_absorb_once 1s 4s -75%
shake256 1s 3s -67%
shake256_finalize 1s 3s -67%
shake256_init 1s 3s -67%
shake256x4_squeezeblocks 1s 4s -75%
unpack_sk_s1hat 1s 3s -67%
use_hint 1s 3s -67%

@oqs-bot

oqs-bot commented Aug 17, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 128s 13s +885%
mld_attempt_signature_generation ⚠️ 246s 63s +290%
sig_unpack_hints ⚠️ 27s 2s +1250%
sign_keypair_internal ⚠️ 21s 5s +320%
sign_pk_from_sk ⚠️ 42s 6s +600%
sign_signature_internal ⚠️ 190s 55s +245%
sign_verify_internal ⚠️ 378s 177s +114%
Full Results (210 proofs)
Proof Status Current Previous Change
**TOTAL** 2107s 1784s +18.1%
sign_verify_internal ⚠️ 378s 177s +114%
mld_attempt_signature_generation ⚠️ 246s 63s +290%
sign_signature_internal ⚠️ 190s 55s +245%
polyvecl_pointwise_acc_montgomery_c 167s 210s -20%
poly_pointwise_montgomery_c 135s 125s +8%
compute_pack_t0_t1 ⚠️ 128s 13s +885%
polyvec_matrix_expand 75s 110s -32%
mld_invntt_layer 60s 109s -45%
sign_pk_from_sk ⚠️ 42s 6s +600%
sig_unpack_hints ⚠️ 27s 2s +1250%
fqmul 22s 40s -45%
mld_ntt_layer 21s 41s -49%
sign_keypair_internal ⚠️ 21s 5s +320%
polyvec_matrix_expand_serial 15s 27s -44%
polyveck_ntt 15s 7s +114%
keccakf1600x4_permute_native 12s 23s -48%
polyveck_decompose 12s 12s +0%
polyt0_unpack 11s 16s -31%
mld_ntt_butterfly_block 10s 24s -58%
poly_ntt_c 9s 19s -53%
polyvec_matrix_pointwise_montgomery_yvec 9s 18s -50%
rej_uniform_native_x86_64 9s - new
rej_uniform 8s 18s -56%
rej_uniform_c 8s 14s -43%
mld_compute_pack_z 7s 7s +0%
mld_keccakf1600_permute_c 7s 6s +17%
poly_chknorm_c 7s 15s -53%
poly_uniform_eta_4x 7s 14s -50%
pointwise_native_x86_64 6s 3s +100%
poly_decompose_c 6s 5s +20%
poly_invntt_tomont_c 6s 11s -45%
poly_uniform_4x 6s 13s -54%
pointwise_acc_native_aarch64 5s 6s -17%
poly_chknorm_native_aarch64 5s 3s +67%
poly_power2round 5s 4s +25%
polyveck_caddq 5s 6s -17%
polyveck_pack_w1 5s 3s +67%
polyvecl_ntt 5s 4s +25%
polyz_unpack_c 5s 13s -62%
sign_signature_extmu 5s 2s +150%
ntt_native_aarch64 4s 2s +100%
pointwise_acc_native_x86_64 4s 8s -50%
poly_caddq 4s 2s +100%
poly_caddq_native_x86_64 4s 3s +33%
poly_pointwise_montgomery 4s 3s +33%
poly_pointwise_montgomery_native 4s 3s +33%
poly_uniform_gamma1_4x 4s 4s +0%
poly_use_hint_native_x86_64 4s - new
polyt1_unpack 4s 5s -20%
polyvecl_uniform_gamma1_serial 4s 3s +33%
polyvecl_unpack_z 4s 3s +33%
polyz_unpack_17_native_aarch64 4s 3s +33%
rej_uniform_native 4s 4s +0%
shake128x4_squeezeblocks 4s 3s +33%
sign_keypair 4s 3s +33%
sign_signature 4s 6s -33%
sign_signature_pre_hash_shake256 4s 3s +33%
sign_verify_pre_hash_shake256 4s 5s -20%
keccak_absorb_once_x4 3s 8s -62%
keccak_f1600_x1_native_aarch64_v84a 3s 3s +0%
keccakf1600x4_permute 3s 4s -25%
mld_check_pct 3s 14s -79%
mld_ct_cmask_nonzero_u32 3s 4s -25%
mld_ct_get_optblocker_i64 3s 2s +50%
mld_ct_get_optblocker_u32 3s 3s +0%
mld_keccakf1600x4_xor_bytes_c 3s 2s +50%
mld_polymat_expand_entry 3s 4s -25%
mld_sample_s1_s2 3s 6s -50%
mld_sign_attempt 3s - new
mld_sign_finish 3s - new
mld_value_barrier_u8 3s 3s +0%
nttunpack_native_x86_64 3s 3s +0%
pack_sig_h 3s 5s -40%
pack_sig_z 3s 2s +50%
pack_sk_s1 3s 5s -40%
pointwise_native_aarch64 3s 5s -40%
poly_add 3s 9s -67%
poly_caddq_native_aarch64 3s 2s +50%
poly_chknorm_native_x86_64 3s 3s +0%
poly_decompose 3s 2s +50%
poly_decompose_32_native_aarch64 3s 3s +0%
poly_decompose_native 3s 3s +0%
poly_ntt 3s 2s +50%
poly_uniform 3s 4s -25%
poly_uniform_gamma1 3s 3s +0%
poly_use_hint_c 3s 5s -40%
poly_use_hint_native 3s 2s +50%
polyt1_pack 3s 3s +0%
polyvecl_pointwise_acc_montgomery_native 3s 2s +50%
polyvecl_uniform_gamma1 3s 2s +50%
polyvecl_unpack_eta 3s 3s +0%
polyw1_pack_32 3s 4s -25%
polyw1_pack_88 3s 2s +50%
polyz_unpack_19_native_aarch64 3s 3s +0%
polyz_unpack_native 3s 4s -25%
power2round 3s 1s +200%
rej_eta 3s 2s +50%
shake128_squeeze 3s 2s +50%
sign_signature_pre_hash_internal 3s 3s +0%
sk_s2hat_get_poly 3s 2s +50%
sk_t0hat_get_poly 3s 2s +50%
unpack_sk_s2hat 3s 4s -25%
unpack_sk_t0hat 3s 5s -40%
yvec_get_poly 3s 3s +0%
yvec_init 3s 3s +0%
caddq 2s 3s -33%
decompose 2s 1s +100%
intt_native_aarch64 2s 3s -33%
intt_native_x86_64 2s 3s -33%
keccak_absorb 2s 3s -33%
keccak_f1600_x1_native_aarch64 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 2s 2s +0%
keccak_f1600_x4_native_avx2 2s 2s +0%
keccak_squeezeblocks_x4 2s 5s -60%
keccakf1600_extract_bytes (big endian) 2s 2s +0%
keccakf1600_xor_bytes (big endian) 2s 2s +0%
keccakf1600x4_extract_bytes_native 2s 4s -50%
keccakf1600x4_xor_bytes 2s 1s +100%
keccakf1600x4_xor_bytes_native 2s 3s -33%
make_hint 2s 2s +0%
mld_ct_abs_i32 2s 2s +0%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_cmask_nonzero_u8 2s 3s -33%
mld_ct_get_optblocker_u8 2s 2s +0%
mld_ct_memcmp 2s 2s +0%
mld_h 2s 2s +0%
mld_keccakf1600x4_extract_bytes_c 2s 3s -33%
mld_sample_s1_s2_serial 2s 4s -50%
mld_sign_resume 2s - new
mld_value_barrier_i64 2s 2s +0%
mld_value_barrier_u32 2s 3s -33%
ntt_native_x86_64 2s 2s +0%
poly_caddq_c 2s 2s +0%
poly_chknorm 2s 4s -50%
poly_decompose_88_native_aarch64 2s 1s +100%
poly_decompose_native_x86_64 2s 3s -33%
poly_invntt_tomont 2s 3s -33%
poly_invntt_tomont_native 2s 2s +0%
poly_ntt_native 2s 4s -50%
poly_permute_bitrev_to_custom_optional 2s 2s +0%
poly_reduce 2s 3s -33%
poly_uniform_eta 2s 4s -50%
poly_use_hint_native_aarch64 2s 3s -33%
polyeta_pack 2s 3s -33%
polyeta_unpack 2s 8s -75%
polyt0_pack 2s 3s -33%
polyvec_matrix_pointwise_montgomery_row 2s 1s +100%
polyveck_chknorm 2s 6s -67%
polyveck_invntt_tomont 2s 8s -75%
polyveck_reduce 2s 4s -50%
polyveck_unpack_eta 2s 6s -67%
polyvecl_chknorm 2s 7s -71%
polyvecl_pack_eta 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 3s -33%
polyz_unpack 2s 3s -33%
rej_eta_c 2s 5s -60%
rej_eta_native 2s 3s -33%
rej_uniform_eta_native_aarch64 2s 4s -50%
rej_uniform_native_aarch64 2s 3s -33%
shake128_absorb 2s 2s +0%
shake256 2s 2s +0%
shake256_absorb 2s 2s +0%
shake256_finalize 2s 1s +100%
shake256_release 2s 2s +0%
shake256x4_squeezeblocks 2s 2s +0%
sign_verify 2s 3s -33%
sign_verify_extmu 2s 3s -33%
sign_verify_pre_hash_internal 2s 5s -60%
sk_s1hat_get_poly 2s 6s -67%
sys_check_capability 2s 4s -50%
unpack_pk_t1 2s 5s -60%
unpack_sk 2s 3s -33%
fqscale 1s 3s -67%
keccak_f1600_x4_native_aarch64_v84a 1s 4s -75%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 1s 2s -50%
keccak_finalize 1s 2s -50%
keccak_init 1s 1s +0%
keccak_squeeze 1s 4s -75%
keccakf1600_permute 1s 2s -50%
keccakf1600_permute_native 1s 3s -67%
keccakf1600_xor_bytes 1s 2s -50%
keccakf1600x4_extract_bytes 1s 4s -75%
mld_ct_sel_int32 1s 3s -67%
mld_keccakf1600_extract_bytes 1s 1s +0%
mld_prepare_domain_separation_prefix 1s 2s -50%
montgomery_reduce 1s 4s -75%
pack_sig_c 1s 5s -80%
pack_sk_rho_key_tr_s2 1s 2s -50%
poly_caddq_native 1s 2s -50%
poly_challenge 1s 6s -83%
poly_chknorm_native 1s 2s -50%
poly_permute_bitrev_to_custom_optional_native 1s 4s -75%
poly_shiftl 1s 3s -67%
poly_sub 1s 3s -67%
poly_use_hint 1s 3s -67%
polyveck_pack_eta 1s 4s -75%
polyw1_pack 1s 4s -75%
polyz_pack 1s 3s -67%
polyz_unpack_native_x86_64 1s 3s -67%
reduce32 1s 3s -67%
rej_uniform_eta_native_x86_64 1s - new
shake128_finalize 1s 1s +0%
shake128_init 1s 2s -50%
shake128_release 1s 3s -67%
shake128x4_absorb_once 1s 3s -67%
shake256_init 1s 2s -50%
shake256_squeeze 1s 3s -67%
shake256x4_absorb_once 1s 3s -67%
unpack_sk_s1hat 1s 2s -50%
use_hint 1s 2s -50%

@oqs-bot

oqs-bot commented Aug 17, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 3272s 2151s +52.1%
compute_pack_t0_t1 ⚠️ 221s 19s +1063%
mld_attempt_signature_generation ⚠️ 346s 55s +529%
sig_unpack_hints ⚠️ 34s 3s +1033%
sign_keypair_internal ⚠️ 66s 6s +1000%
sign_pk_from_sk ⚠️ 54s 6s +800%
sign_signature_internal ⚠️ 364s 42s +767%
sign_verify_internal ⚠️ 877s 97s +804%
Full Results (210 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 3272s 2151s +52.1%
sign_verify_internal ⚠️ 877s 97s +804%
sign_signature_internal ⚠️ 364s 42s +767%
mld_attempt_signature_generation ⚠️ 346s 55s +529%
polyvecl_pointwise_acc_montgomery_c 293s 353s -17%
compute_pack_t0_t1 ⚠️ 221s 19s +1063%
poly_pointwise_montgomery_c 173s 144s +20%
polyvec_matrix_expand 100s 324s -69%
mld_invntt_layer 71s 115s -38%
sign_keypair_internal ⚠️ 66s 6s +1000%
sign_pk_from_sk ⚠️ 54s 6s +800%
sig_unpack_hints ⚠️ 34s 3s +1033%
fqmul 27s 43s -37%
mld_ntt_layer 27s 45s -40%
polyvec_matrix_expand_serial 24s 38s -37%
mld_ntt_butterfly_block 13s 24s -46%
keccakf1600x4_permute_native 12s 23s -48%
polyvec_matrix_pointwise_montgomery_yvec 12s 18s -33%
rej_uniform_native_x86_64 12s - new
polyt0_unpack 10s 14s -29%
poly_ntt_c 9s 21s -57%
rej_uniform 9s 15s -40%
poly_invntt_tomont_c 8s 12s -33%
poly_uniform_eta_4x 8s 11s -27%
polyeta_unpack 8s 17s -53%
polyveck_decompose 8s 13s -38%
poly_chknorm_c 7s 15s -53%
poly_uniform_4x 7s 13s -46%
rej_uniform_c 7s 19s -63%
sign_keypair 7s 4s +75%
poly_use_hint_c 6s 2s +200%
polyveck_invntt_tomont 6s 9s -33%
polyveck_ntt 6s 11s -45%
intt_native_aarch64 5s 3s +67%
mld_check_pct 5s 16s -69%
mld_compute_pack_z 5s 8s -38%
pointwise_acc_native_aarch64 5s 6s -17%
pointwise_native_aarch64 5s 5s +0%
poly_caddq_native 5s 4s +25%
poly_chknorm_native 5s 4s +25%
polyvecl_chknorm 5s 7s -29%
shake128x4_absorb_once 5s 5s +0%
keccak_absorb 4s 3s +33%
keccak_absorb_once_x4 4s 9s -56%
keccakf1600_xor_bytes 4s 3s +33%
keccakf1600_xor_bytes (big endian) 4s 2s +100%
mld_ct_abs_i32 4s 3s +33%
mld_keccakf1600_permute_c 4s 7s -43%
mld_sample_s1_s2 4s 6s -33%
pack_sk_rho_key_tr_s2 4s 3s +33%
pointwise_acc_native_x86_64 4s 6s -33%
poly_add 4s 6s -33%
poly_decompose_88_native_aarch64 4s 2s +100%
poly_uniform 4s 4s +0%
polyeta_pack 4s 4s +0%
polyveck_caddq 4s 8s -50%
polyveck_chknorm 4s 3s +33%
polyveck_pack_w1 4s 3s +33%
polyvecl_ntt 4s 7s -43%
polyvecl_pointwise_acc_montgomery_native 4s 3s +33%
polyvecl_uniform_gamma1_serial 4s 4s +0%
polyz_unpack_c 4s 3s +33%
rej_eta_native 4s 6s -33%
rej_uniform_eta_native_x86_64 4s - new
shake128_squeeze 4s 2s +100%
sign_signature_extmu 4s 4s +0%
sign_signature_pre_hash_internal 4s 5s -20%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 3s 4s -25%
keccak_init 3s 3s +0%
keccakf1600_extract_bytes (big endian) 3s 3s +0%
keccakf1600_permute 3s 3s +0%
keccakf1600x4_extract_bytes 3s 2s +50%
mld_ct_cmask_neg_i32 3s 4s -25%
mld_ct_cmask_nonzero_u32 3s 2s +50%
mld_ct_cmask_nonzero_u8 3s 3s +0%
mld_keccakf1600x4_extract_bytes_c 3s 2s +50%
mld_sample_s1_s2_serial 3s 8s -62%
pack_sig_c 3s 4s -25%
pack_sig_h 3s 4s -25%
pack_sig_z 3s 5s -40%
poly_caddq_native_aarch64 3s 3s +0%
poly_caddq_native_x86_64 3s 2s +50%
poly_chknorm 3s 3s +0%
poly_invntt_tomont 3s 1s +200%
poly_ntt_native 3s 3s +0%
poly_pointwise_montgomery_native 3s 5s -40%
poly_power2round 3s 3s +0%
poly_sub 3s 3s +0%
poly_uniform_gamma1_4x 3s 3s +0%
poly_use_hint_native 3s 3s +0%
polyt1_pack 3s 3s +0%
polyvec_matrix_pointwise_montgomery_row 3s 3s +0%
polyveck_pack_eta 3s 6s -50%
polyveck_unpack_eta 3s 4s -25%
polyvecl_pointwise_acc_montgomery 3s 5s -40%
polyvecl_uniform_gamma1 3s 2s +50%
polyz_pack 3s 5s -40%
polyz_unpack_19_native_aarch64 3s 4s -25%
polyz_unpack_native 3s 4s -25%
rej_eta 3s 4s -25%
rej_eta_c 3s 5s -40%
rej_uniform_eta_native_aarch64 3s 5s -40%
rej_uniform_native 3s 8s -62%
shake256_absorb 3s 2s +50%
sign_signature 3s 5s -40%
sign_signature_pre_hash_shake256 3s 6s -50%
sign_verify 3s 5s -40%
sign_verify_pre_hash_shake256 3s 3s +0%
sk_s1hat_get_poly 3s 3s +0%
sk_s2hat_get_poly 3s 3s +0%
sys_check_capability 3s 3s +0%
unpack_sk_t0hat 3s 7s -57%
use_hint 3s 3s +0%
yvec_get_poly 3s 4s -25%
decompose 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 3s -33%
keccak_f1600_x4_native_avx2 2s 2s +0%
keccak_squeeze 2s 2s +0%
keccak_squeezeblocks_x4 2s 4s -50%
keccakf1600_permute_native 2s 4s -50%
keccakf1600x4_extract_bytes_native 2s 2s +0%
keccakf1600x4_permute 2s 3s -33%
keccakf1600x4_xor_bytes 2s 3s -33%
keccakf1600x4_xor_bytes_native 2s 3s -33%
make_hint 2s 3s -33%
mld_ct_get_optblocker_u32 2s 2s +0%
mld_ct_memcmp 2s 3s -33%
mld_ct_sel_int32 2s 3s -33%
mld_h 2s 3s -33%
mld_polymat_expand_entry 2s 3s -33%
mld_prepare_domain_separation_prefix 2s 4s -50%
mld_sign_finish 2s - new
mld_sign_resume 2s - new
ntt_native_aarch64 2s 6s -67%
pointwise_native_x86_64 2s 2s +0%
poly_challenge 2s 5s -60%
poly_chknorm_native_aarch64 2s 4s -50%
poly_chknorm_native_x86_64 2s 2s +0%
poly_decompose 2s 3s -33%
poly_decompose_32_native_aarch64 2s 5s -60%
poly_decompose_c 2s 5s -60%
poly_decompose_native 2s 2s +0%
poly_decompose_native_x86_64 2s 2s +0%
poly_invntt_tomont_native 2s 5s -60%
poly_permute_bitrev_to_custom_optional 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native 2s 5s -60%
poly_pointwise_montgomery 2s 4s -50%
poly_uniform_eta 2s 4s -50%
poly_use_hint 2s 1s +100%
polyt0_pack 2s 4s -50%
polyt1_unpack 2s 4s -50%
polyvecl_pack_eta 2s 3s -33%
polyw1_pack_32 2s 4s -50%
polyz_unpack 2s 2s +0%
polyz_unpack_native_x86_64 2s 3s -33%
power2round 2s 4s -50%
reduce32 2s 3s -33%
rej_uniform_native_aarch64 2s 2s +0%
shake128_finalize 2s 2s +0%
shake128_release 2s 4s -50%
shake256 2s 2s +0%
shake256_finalize 2s 2s +0%
shake256x4_absorb_once 2s 2s +0%
shake256x4_squeezeblocks 2s 1s +100%
sign_verify_pre_hash_internal 2s 3s -33%
sk_t0hat_get_poly 2s 4s -50%
unpack_pk_t1 2s 1s +100%
unpack_sk 2s 5s -60%
unpack_sk_s1hat 2s 2s +0%
unpack_sk_s2hat 2s 3s -33%
yvec_init 2s 4s -50%
caddq 1s 4s -75%
fqscale 1s 3s -67%
intt_native_x86_64 1s 3s -67%
keccak_f1600_x1_native_aarch64 1s 1s +0%
keccak_f1600_x1_native_aarch64_v84a 1s 1s +0%
keccak_f1600_x4_native_aarch64_v84a 1s 4s -75%
keccak_finalize 1s 1s +0%
mld_ct_get_optblocker_i64 1s 3s -67%
mld_ct_get_optblocker_u8 1s 3s -67%
mld_keccakf1600_extract_bytes 1s 4s -75%
mld_keccakf1600x4_xor_bytes_c 1s 4s -75%
mld_sign_attempt 1s - new
mld_value_barrier_i64 1s 1s +0%
mld_value_barrier_u32 1s 2s -50%
mld_value_barrier_u8 1s 3s -67%
montgomery_reduce 1s 3s -67%
ntt_native_x86_64 1s 2s -50%
nttunpack_native_x86_64 1s 3s -67%
pack_sk_s1 1s 1s +0%
poly_caddq 1s 2s -50%
poly_caddq_c 1s 3s -67%
poly_ntt 1s 3s -67%
poly_reduce 1s 2s -50%
poly_shiftl 1s 4s -75%
poly_uniform_gamma1 1s 4s -75%
poly_use_hint_native_aarch64 1s 2s -50%
poly_use_hint_native_x86_64 1s - new
polyveck_reduce 1s 3s -67%
polyvecl_unpack_eta 1s 5s -80%
polyvecl_unpack_z 1s 4s -75%
polyw1_pack 1s 4s -75%
polyw1_pack_88 1s 3s -67%
polyz_unpack_17_native_aarch64 1s 3s -67%
shake128_absorb 1s 4s -75%
shake128_init 1s 1s +0%
shake128x4_squeezeblocks 1s 3s -67%
shake256_init 1s 2s -50%
shake256_release 1s 3s -67%
shake256_squeeze 1s 2s -50%
sign_verify_extmu 1s 3s -67%

@L-series

Copy link
Copy Markdown
Contributor Author

@mkannwischer apologies, its late and i completely glossed over the assignee tab.. Won't do that again.

On the topic of SLOTHY however, what do you think of the addition of a per-file gate? I see that most of the time is spent optimizing NTT and iNTT, and so it might make sense to just have a finer grain gate for these two routines (i.e if any other routine is modified, only re-optimize what has been affected)

@mkannwischer

Copy link
Copy Markdown
Contributor

@mkannwischer apologies, its late and i completely glossed over the assignee tab.. Won't do that again.

No worries! Thank you for your contributions.

On the topic of SLOTHY however, what do you think of the addition of a per-file gate? I see that most of the time is spent optimizing NTT and iNTT, and so it might make sense to just have a finer grain gate for these two routines (i.e if any other routine is modified, only re-optimize what has been affected)

We are not planning many more asm changes at this point, so the vast majority of re-runs will be triggered by nix flake changes, I believe. For those we have to re-run for all files anyway. I prefer to keep it simple for now.

@mkannwischer mkannwischer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks @L-series. This looks great.
I think we can afford to keep running on main. Could you add that, please? Sorry I realized I had a typo in my original issue that suggested otherwise.

SLOTHY starts a c8g.8xlarge for every PR push and merge_group run,
regardless of what changed. Gate it on a changed-files job, as in
hol_light.yml.

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
This commit introduces a slothy-tests label for PR's which can manually
trigger SLOTHY upon addition.

 - Resolves #1175

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
@L-series
L-series force-pushed the ci-slothy-path-and-label-gating branch from 083ca4d to 25bd632 Compare August 31, 2026 15:38
@L-series

Copy link
Copy Markdown
Contributor Author

Thanks @L-series. This looks great. I think we can afford to keep running on main. Could you add that, please? Sorry I realized I had a typo in my original issue that suggested otherwise.

No worries! I added a:

    push:
    branches: ["main"]

and
${{ github.event_name == 'push' || which will run slothy on push to main unconditionally.

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

CI: Only run SLOTHY in main and when relevant files change

3 participants