Skip to content

Update to tagged build of CBMC 6.10.0#1210

Merged
mkannwischer merged 1 commit into
mainfrom
cbmc-6.10.0
Jun 26, 2026
Merged

Update to tagged build of CBMC 6.10.0#1210
mkannwischer merged 1 commit into
mainfrom
cbmc-6.10.0

Conversation

@rod-chapman

Copy link
Copy Markdown
Contributor

Fixes #1197
Fixes #1126

  1. Update NIX config for CBMC 6.10.0
  2. Revert to Z3 with default options for proof of sign_verify_internal() owing to proof performance regressions using z3_no_bv_extract following CBMC fix for Z3 soundness issue.

1. Update NIX config for CBMC 6.10.0
2. Revert to Z3 with default options for proof of sign_verify_internal()
   owing to proof performance regressions using z3_no_bv_extract following
   CBMC fix for Z3 soundness issue.

Signed-off-by: Rod Chapman <rodchap@amazon.com>
@rod-chapman rod-chapman added this to the v1.0.0 milestone Jun 26, 2026
@rod-chapman rod-chapman requested a review from mkannwischer June 26, 2026 10:34
@rod-chapman rod-chapman self-assigned this Jun 26, 2026
@rod-chapman rod-chapman requested a review from a team as a code owner June 26, 2026 10:34
@oqs-bot

oqs-bot commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 2123s 1598s +32.9%
mld_ct_memcmp ⚠️ 204s 68s +200%
poly_ntt_c ⚠️ 22s 4s +450%
polyvecl_chknorm ⚠️ 38s 11s +245%
rej_uniform_native ⚠️ 184s 121s +52%
rej_uniform_native_aarch64 ⚠️ 118s 5s +2260%
sign_verify_internal ⚠️ 50s 22s +127%
Full Results (205 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 2123s 1598s +32.9%
polyvec_matrix_pointwise_montgomery_yvec 209s 152s +38%
mld_ct_memcmp ⚠️ 204s 68s +200%
mld_invntt_layer 189s 167s +13%
rej_uniform_native ⚠️ 184s 121s +52%
poly_pointwise_montgomery_c 142s 131s +8%
rej_uniform_native_aarch64 ⚠️ 118s 5s +2260%
sign_verify_internal ⚠️ 50s 22s +127%
mld_ntt_layer 49s 41s +20%
fqmul 45s 41s +10%
polyvecl_chknorm ⚠️ 38s 11s +245%
mld_attempt_signature_generation 32s 31s +3%
mld_ntt_butterfly_block 26s 20s +30%
keccakf1600x4_permute_native 23s 22s +5%
poly_ntt_c ⚠️ 22s 4s +450%
rej_uniform_c 17s 16s +6%
polyeta_unpack 15s 14s +7%
polyt0_unpack 14s 16s -12%
polyveck_chknorm 14s 4s +250%
poly_chknorm_c 13s 18s -28%
polyvec_matrix_pointwise_montgomery_row 13s 6s +117%
polyveck_decompose 13s 17s -24%
poly_invntt_tomont_c 12s 7s +71%
poly_uniform_eta_4x 12s 18s -33%
mld_check_pct 11s 15s -27%
compute_pack_t0_t1 10s 8s +25%
polyvecl_ntt 10s 8s +25%
keccak_absorb_once_x4 9s 8s +12%
polyz_unpack_c 9s 5s +80%
rej_uniform 9s 6s +50%
sign_pk_from_sk 9s 7s +29%
pointwise_acc_native_x86_64 8s 6s +33%
poly_add 8s 12s -33%
poly_decompose_c 8s 4s +100%
mld_keccakf1600_permute_c 7s 8s -12%
pointwise_acc_native_aarch64 7s 7s +0%
poly_decompose_88_native_aarch64 7s 2s +250%
polyveck_caddq 7s 4s +75%
sign 7s 6s +17%
sign_signature_internal 7s 3s +133%
mld_compute_pack_z 6s 4s +50%
mld_sample_s1_s2 6s 4s +50%
pack_sk_s1 6s 4s +50%
poly_challenge 6s 4s +50%
poly_reduce 6s 6s +0%
polyveck_reduce 6s 5s +20%
sign_verify_pre_hash_shake256 6s 7s -14%
sk_t0hat_get_poly 6s 4s +50%
use_hint 6s 4s +50%
decompose 5s 4s +25%
intt_native_x86_64 5s 4s +25%
keccak_squeezeblocks_x4 5s 6s -17%
mld_h 5s 4s +25%
mld_sample_s1_s2_serial 5s 3s +67%
montgomery_reduce 5s 3s +67%
poly_caddq_c 5s 5s +0%
poly_caddq_native_aarch64 5s 3s +67%
poly_caddq_native_x86_64 5s 2s +150%
poly_power2round 5s 7s -29%
poly_use_hint 5s 2s +150%
poly_use_hint_native 5s 3s +67%
polyt1_pack 5s 3s +67%
polyveck_invntt_tomont 5s 5s +0%
polyveck_pack_eta 5s 3s +67%
polyvecl_pointwise_acc_montgomery_c 5s 1s +400%
polyvecl_unpack_z 5s 3s +67%
polyz_unpack_19_native_aarch64 5s 4s +25%
power2round 5s 2s +150%
rej_eta_native 5s 4s +25%
sig_unpack_hints 5s 3s +67%
sign_keypair 5s 6s -17%
sign_keypair_internal 5s 6s -17%
sign_open 5s 3s +67%
sign_signature 5s 4s +25%
sign_verify 5s 4s +25%
fqscale 4s 3s +33%
keccak_absorb 4s 6s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 4s 3s +33%
keccakf1600x4_xor_bytes 4s 2s +100%
mld_keccakf1600x4_extract_bytes_c 4s 3s +33%
ntt_native_x86_64 4s 3s +33%
pointwise_native_x86_64 4s 4s +0%
poly_caddq_native 4s 4s +0%
poly_chknorm 4s 3s +33%
poly_chknorm_native 4s 3s +33%
poly_invntt_tomont 4s 2s +100%
poly_ntt 4s 1s +300%
poly_uniform 4s 4s +0%
poly_uniform_gamma1 4s 2s +100%
poly_uniform_gamma1_4x 4s 3s +33%
polyt0_pack 4s 2s +100%
polyt1_unpack 4s 1s +300%
polyveck_unpack_eta 4s 3s +33%
polyvecl_pack_eta 4s 2s +100%
polyvecl_uniform_gamma1 4s 2s +100%
polyvecl_unpack_eta 4s 3s +33%
polyw1_pack_88 4s 1s +300%
polyz_unpack_native_x86_64 4s 2s +100%
shake128_absorb 4s 2s +100%
shake128_release 4s 4s +0%
shake128x4_absorb_once 4s 3s +33%
shake256_squeeze 4s 3s +33%
shake256x4_absorb_once 4s 4s +0%
sign_signature_extmu 4s 4s +0%
sign_signature_pre_hash_internal 4s 5s -20%
sign_verify_pre_hash_internal 4s 4s +0%
intt_native_aarch64 3s 4s -25%
keccak_f1600_x1_native_aarch64_v84a 3s 2s +50%
keccak_squeeze 3s 3s +0%
keccakf1600_permute_native 3s 4s -25%
keccakf1600_xor_bytes 3s 3s +0%
keccakf1600_xor_bytes (big endian) 3s 4s -25%
keccakf1600x4_extract_bytes_native 3s 2s +50%
keccakf1600x4_xor_bytes_native 3s 5s -40%
make_hint 3s 3s +0%
mld_ct_get_optblocker_u8 3s 3s +0%
mld_prepare_domain_separation_prefix 3s 3s +0%
mld_value_barrier_u32 3s 2s +50%
ntt_native_aarch64 3s 4s -25%
nttunpack_native_x86_64 3s 2s +50%
pack_sig_h 3s 4s -25%
pack_sk_rho_key_tr_s2 3s 3s +0%
poly_chknorm_native_x86_64 3s 3s +0%
poly_decompose 3s 3s +0%
poly_decompose_32_native_aarch64 3s 3s +0%
poly_decompose_native 3s 4s -25%
poly_pointwise_montgomery 3s 3s +0%
poly_shiftl 3s 5s -40%
poly_uniform_eta 3s 4s -25%
poly_use_hint_c 3s 5s -40%
poly_use_hint_native_aarch64 3s 3s +0%
polyeta_pack 3s 2s +50%
polyvec_matrix_expand 3s 3s +0%
polyvec_matrix_expand_serial 3s 3s +0%
polyvecl_pointwise_acc_montgomery_native 3s 3s +0%
polyw1_pack_32 3s 2s +50%
polyz_unpack 3s 2s +50%
polyz_unpack_17_native_aarch64 3s 2s +50%
polyz_unpack_native 3s 2s +50%
rej_eta_c 3s 3s +0%
shake128x4_squeezeblocks 3s 3s +0%
shake256_release 3s 4s -25%
sign_signature_pre_hash_shake256 3s 4s -25%
sk_s1hat_get_poly 3s 1s +200%
sk_s2hat_get_poly 3s 4s -25%
sys_check_capability 3s 3s +0%
unpack_pk_t1 3s 3s +0%
unpack_sk_s2hat 3s 1s +200%
unpack_sk_t0hat 3s 4s -25%
yvec_get_poly 3s 5s -40%
keccak_f1600_x1_native_aarch64 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 4s -50%
keccak_finalize 2s 3s -33%
keccak_init 2s 3s -33%
keccakf1600_permute 2s 2s +0%
mld_ct_abs_i32 2s 3s -33%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_cmask_nonzero_u8 2s 1s +100%
mld_ct_get_optblocker_i64 2s 2s +0%
mld_ct_get_optblocker_u32 2s 3s -33%
mld_ct_sel_int32 2s 2s +0%
mld_keccakf1600_extract_bytes 2s 3s -33%
mld_keccakf1600x4_xor_bytes_c 2s 3s -33%
mld_polymat_expand_entry 2s 3s -33%
mld_value_barrier_i64 2s 2s +0%
mld_value_barrier_u8 2s 3s -33%
pack_sig_c 2s 6s -67%
pack_sig_z 2s 3s -33%
pointwise_native_aarch64 2s 4s -50%
poly_caddq 2s 3s -33%
poly_chknorm_native_aarch64 2s 4s -50%
poly_ntt_native 2s 3s -33%
poly_permute_bitrev_to_custom_optional 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native 2s 3s -33%
poly_pointwise_montgomery_native 2s 2s +0%
poly_uniform_4x 2s 5s -60%
polyveck_pack_w1 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 4s -50%
polyvecl_uniform_gamma1_serial 2s 1s +100%
polyw1_pack 2s 4s -50%
polyz_pack 2s 2s +0%
reduce32 2s 4s -50%
rej_eta 2s 3s -33%
rej_uniform_eta_native_aarch64 2s 5s -60%
shake128_init 2s 3s -33%
shake256_absorb 2s 2s +0%
shake256_finalize 2s 3s -33%
shake256_init 2s 2s +0%
sign_verify_extmu 2s 4s -50%
caddq 1s 4s -75%
keccak_f1600_x4_native_avx2 1s 2s -50%
keccakf1600_extract_bytes (big endian) 1s 4s -75%
keccakf1600x4_extract_bytes 1s 4s -75%
keccakf1600x4_permute 1s 2s -50%
mld_ct_cmask_nonzero_u32 1s 2s -50%
poly_invntt_tomont_native 1s 4s -75%
poly_sub 1s 3s -67%
polyveck_ntt 1s 2s -50%
shake128_finalize 1s 3s -67%
shake128_squeeze 1s 4s -75%
shake256 1s 3s -67%
shake256x4_squeezeblocks 1s 3s -67%
unpack_sk 1s 4s -75%
unpack_sk_s1hat 1s 2s -50%
yvec_init 1s 4s -75%

@oqs-bot

oqs-bot commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 2931s 1754s +67.1%
compute_pack_t0_t1 ⚠️ 56s 17s +229%
mld_ct_memcmp ⚠️ 241s 67s +260%
poly_ntt_c ⚠️ 24s 3s +700%
poly_pointwise_montgomery_c ⚠️ 167s 95s +76%
polyvecl_pointwise_acc_montgomery_c ⚠️ 656s 113s +481%
rej_uniform_native ⚠️ 219s 145s +51%
rej_uniform_native_aarch64 ⚠️ 127s 3s +4133%
sign_verify_internal ⚠️ 136s 26s +423%
Full Results (205 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 2931s 1754s +67.1%
polyvecl_pointwise_acc_montgomery_c ⚠️ 656s 113s +481%
mld_ct_memcmp ⚠️ 241s 67s +260%
mld_invntt_layer 240s 288s -17%
rej_uniform_native ⚠️ 219s 145s +51%
poly_pointwise_montgomery_c ⚠️ 167s 95s +76%
sign_verify_internal ⚠️ 136s 26s +423%
rej_uniform_native_aarch64 ⚠️ 127s 3s +4133%
mld_attempt_signature_generation 58s 59s -2%
compute_pack_t0_t1 ⚠️ 56s 17s +229%
mld_ntt_layer 50s 43s +16%
fqmul 46s 42s +10%
polyvec_matrix_expand 30s 27s +11%
mld_ntt_butterfly_block 26s 23s +13%
keccakf1600x4_permute_native 24s 24s +0%
poly_ntt_c ⚠️ 24s 3s +700%
sign_signature_internal 21s 18s +17%
polyt0_unpack 19s 16s +19%
polyeta_unpack 18s 16s +12%
rej_uniform_c 18s 14s +29%
poly_chknorm_c 17s 19s -11%
rej_uniform 17s 21s -19%
polyvec_matrix_pointwise_montgomery_yvec 16s 9s +78%
mld_check_pct 15s 14s +7%
poly_uniform_4x 15s 11s +36%
polyz_unpack_c 14s 11s +27%
poly_invntt_tomont_c 12s 7s +71%
poly_uniform_eta_4x 12s 12s +0%
polyvecl_chknorm 12s 4s +200%
keccak_absorb_once_x4 10s 8s +25%
mld_compute_pack_z 9s 9s +0%
poly_add 8s 11s -27%
polyveck_decompose 8s 9s -11%
mld_keccakf1600_permute_c 7s 6s +17%
pointwise_acc_native_aarch64 7s 4s +75%
pointwise_acc_native_x86_64 7s 4s +75%
poly_decompose_c 7s 2s +250%
polyvec_matrix_expand_serial 7s 10s -30%
polyveck_chknorm 7s 11s -36%
polyveck_invntt_tomont 7s 3s +133%
sign 7s 8s -12%
sign_keypair 7s 3s +133%
sign_pk_from_sk 7s 7s +0%
sign_verify 7s 3s +133%
keccak_squeezeblocks_x4 6s 3s +100%
mld_sample_s1_s2_serial 6s 4s +50%
poly_uniform 6s 6s +0%
polyt1_pack 6s 4s +50%
polyveck_caddq 6s 3s +100%
sign_keypair_internal 6s 4s +50%
sign_signature_pre_hash_shake256 6s 6s +0%
sign_verify_extmu 6s 3s +100%
sign_verify_pre_hash_shake256 6s 2s +200%
keccak_absorb 5s 6s -17%
nttunpack_native_x86_64 5s 3s +67%
poly_caddq 5s 2s +150%
poly_challenge 5s 3s +67%
poly_invntt_tomont 5s 3s +67%
poly_permute_bitrev_to_custom_optional 5s 3s +67%
poly_uniform_eta 5s 5s +0%
poly_uniform_gamma1_4x 5s 5s +0%
poly_use_hint_native 5s 2s +150%
polyt0_pack 5s 6s -17%
polyt1_unpack 5s 2s +150%
rej_eta_native 5s 3s +67%
sign_signature_extmu 5s 4s +25%
sign_verify_pre_hash_internal 5s 2s +150%
caddq 4s 4s +0%
keccak_f1600_x4_native_aarch64_v84a 4s 4s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 4s 2s +100%
keccakf1600_xor_bytes 4s 3s +33%
mld_ct_sel_int32 4s 3s +33%
mld_h 4s 2s +100%
mld_keccakf1600_extract_bytes 4s 3s +33%
mld_prepare_domain_separation_prefix 4s 5s -20%
mld_sample_s1_s2 4s 3s +33%
pack_sig_h 4s 4s +0%
pointwise_native_x86_64 4s 4s +0%
poly_chknorm 4s 2s +100%
poly_chknorm_native 4s 2s +100%
poly_chknorm_native_x86_64 4s 2s +100%
poly_decompose_88_native_aarch64 4s 2s +100%
poly_permute_bitrev_to_custom_optional_native 4s 2s +100%
poly_pointwise_montgomery 4s 3s +33%
poly_power2round 4s 5s -20%
poly_sub 4s 3s +33%
poly_use_hint_native_aarch64 4s 3s +33%
polyeta_pack 4s 2s +100%
polyveck_reduce 4s 5s -20%
polyveck_unpack_eta 4s 4s +0%
polyvecl_ntt 4s 5s -20%
polyvecl_pack_eta 4s 5s -20%
polyvecl_uniform_gamma1_serial 4s 3s +33%
polyw1_pack 4s 3s +33%
polyw1_pack_32 4s 2s +100%
polyz_unpack_17_native_aarch64 4s 4s +0%
polyz_unpack_native 4s 5s -20%
rej_uniform_eta_native_aarch64 4s 2s +100%
shake256 4s 2s +100%
shake256x4_absorb_once 4s 4s +0%
sign_open 4s 5s -20%
sign_signature 4s 3s +33%
sk_s2hat_get_poly 4s 4s +0%
unpack_sk 4s 3s +33%
yvec_init 4s 4s +0%
decompose 3s 5s -40%
intt_native_aarch64 3s 4s -25%
intt_native_x86_64 3s 4s -25%
keccak_finalize 3s 1s +200%
keccakf1600x4_extract_bytes 3s 4s -25%
keccakf1600x4_extract_bytes_native 3s 2s +50%
keccakf1600x4_xor_bytes 3s 2s +50%
make_hint 3s 2s +50%
mld_ct_cmask_nonzero_u8 3s 5s -40%
mld_ct_get_optblocker_i64 3s 3s +0%
mld_ct_get_optblocker_u32 3s 4s -25%
mld_polymat_expand_entry 3s 3s +0%
ntt_native_aarch64 3s 3s +0%
ntt_native_x86_64 3s 3s +0%
pack_sig_c 3s 1s +200%
pack_sk_rho_key_tr_s2 3s 3s +0%
pack_sk_s1 3s 3s +0%
pointwise_native_aarch64 3s 2s +50%
poly_caddq_native 3s 2s +50%
poly_caddq_native_x86_64 3s 3s +0%
poly_ntt 3s 4s -25%
poly_ntt_native 3s 3s +0%
poly_reduce 3s 2s +50%
poly_use_hint 3s 4s -25%
poly_use_hint_c 3s 6s -50%
polyveck_ntt 3s 5s -40%
polyveck_pack_w1 3s 2s +50%
polyvecl_unpack_eta 3s 2s +50%
polyz_unpack 3s 3s +0%
power2round 3s 4s -25%
rej_eta 3s 2s +50%
rej_eta_c 3s 4s -25%
shake128_finalize 3s 2s +50%
shake128_squeeze 3s 4s -25%
shake128x4_absorb_once 3s 4s -25%
shake256_absorb 3s 4s -25%
shake256_finalize 3s 3s +0%
sig_unpack_hints 3s 2s +50%
sign_signature_pre_hash_internal 3s 6s -50%
sk_t0hat_get_poly 3s 4s -25%
sys_check_capability 3s 2s +50%
unpack_pk_t1 3s 3s +0%
unpack_sk_s2hat 3s 3s +0%
unpack_sk_t0hat 3s 2s +50%
yvec_get_poly 3s 3s +0%
fqscale 2s 5s -60%
keccak_f1600_x1_native_aarch64 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 2s 3s -33%
keccak_f1600_x4_native_avx2 2s 2s +0%
keccak_init 2s 1s +100%
keccak_squeeze 2s 4s -50%
keccakf1600_extract_bytes (big endian) 2s 6s -67%
keccakf1600_permute 2s 2s +0%
keccakf1600_permute_native 2s 1s +100%
keccakf1600x4_permute 2s 2s +0%
keccakf1600x4_xor_bytes_native 2s 2s +0%
mld_ct_abs_i32 2s 3s -33%
mld_ct_cmask_neg_i32 2s 1s +100%
mld_ct_cmask_nonzero_u32 2s 2s +0%
mld_keccakf1600x4_extract_bytes_c 2s 2s +0%
mld_keccakf1600x4_xor_bytes_c 2s 4s -50%
mld_value_barrier_i64 2s 3s -33%
mld_value_barrier_u32 2s 1s +100%
mld_value_barrier_u8 2s 2s +0%
montgomery_reduce 2s 2s +0%
pack_sig_z 2s 3s -33%
poly_caddq_native_aarch64 2s 2s +0%
poly_chknorm_native_aarch64 2s 5s -60%
poly_decompose_32_native_aarch64 2s 3s -33%
poly_decompose_native 2s 2s +0%
poly_invntt_tomont_native 2s 3s -33%
poly_pointwise_montgomery_native 2s 3s -33%
poly_shiftl 2s 4s -50%
polyvec_matrix_pointwise_montgomery_row 2s 3s -33%
polyveck_pack_eta 2s 2s +0%
polyvecl_pointwise_acc_montgomery_native 2s 6s -67%
polyvecl_uniform_gamma1 2s 3s -33%
polyw1_pack_88 2s 6s -67%
polyz_pack 2s 4s -50%
polyz_unpack_native_x86_64 2s 4s -50%
reduce32 2s 3s -33%
shake128_absorb 2s 1s +100%
shake128_init 2s 3s -33%
shake128_release 2s 3s -33%
shake128x4_squeezeblocks 2s 2s +0%
shake256_squeeze 2s 1s +100%
shake256x4_squeezeblocks 2s 4s -50%
sk_s1hat_get_poly 2s 3s -33%
unpack_sk_s1hat 2s 3s -33%
use_hint 2s 1s +100%
keccakf1600_xor_bytes (big endian) 1s 2s -50%
mld_ct_get_optblocker_u8 1s 2s -50%
poly_caddq_c 1s 6s -83%
poly_decompose 1s 4s -75%
poly_uniform_gamma1 1s 4s -75%
polyvecl_pointwise_acc_montgomery 1s 2s -50%
polyvecl_unpack_z 1s 3s -67%
polyz_unpack_19_native_aarch64 1s 2s -50%
shake256_init 1s 2s -50%
shake256_release 1s 2s -50%

@oqs-bot

oqs-bot commented Jun 26, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

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

@mkannwischer mkannwischer merged commit 22a70aa into main Jun 26, 2026
382 checks passed
@mkannwischer mkannwischer deleted the cbmc-6.10.0 branch June 26, 2026 11:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Evaluate and adopt CBMC 6.10.0 Avoid z3 soundness issue #9550

3 participants