Skip to content

Nix: Update CBCM to experimental branch#964

Draft
mkannwischer wants to merge 2 commits intomainfrom
cbmc-experimental
Draft

Nix: Update CBCM to experimental branch#964
mkannwischer wants to merge 2 commits intomainfrom
cbmc-experimental

Conversation

@mkannwischer
Copy link
Contributor

@mkannwischer mkannwischer force-pushed the cbmc-experimental branch 3 times, most recently from 4183c1f to 7085048 Compare February 12, 2026 01:55
@oqs-bot
Copy link
Contributor

oqs-bot commented Feb 12, 2026

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof Status Current Previous Change
polyvec_matrix_expand ⚠️ 230s 153s +50%
polyveck_shiftl ⚠️ 33s 6s +450%
Full Results (175 proofs)
Proof Status Current Previous Change
**TOTAL** 2535s 2449s +3.5%
sign_verify_internal 254s 353s -28%
mld_attempt_signature_generation 239s 227s +5%
polyvec_matrix_expand ⚠️ 230s 153s +50%
polyvecl_pointwise_acc_montgomery_c 198s 165s +20%
rej_uniform_native 154s 139s +11%
poly_pointwise_montgomery_c 144s 128s +12%
polyvec_matrix_expand_serial 112s 110s +2%
mld_ct_memcmp 84s 74s +14%
mld_invntt_layer 69s 114s -39%
mld_ntt_layer 56s 44s +27%
sign_signature_internal 54s 46s +17%
keccak_squeezeblocks_x4 41s 42s -2%
polyveck_shiftl ⚠️ 33s 6s +450%
polymat_permute_bitrev_to_custom 28s 24s +17%
mld_compute_t0_t1_tr_from_sk_components 25s 25s +0%
rej_uniform 22s 21s +5%
fqmul 20s 18s +11%
poly_chknorm_c 19s 17s +12%
poly_uniform_eta_4x 19s 17s +12%
rej_uniform_c 19s 16s +19%
polyt0_unpack 18s 17s +6%
polyveck_add 16s 13s +23%
polyveck_pointwise_poly_montgomery 15s 8s +88%
poly_uniform_4x 14s 17s -18%
polyeta_unpack 14s 13s +8%
polyvec_matrix_pointwise_montgomery 14s 12s +17%
polyveck_power2round 14s 14s +0%
keccakf1600x4_permute_native 13s 12s +8%
mld_ntt_butterfly_block 13s 13s +0%
polyveck_decompose 13s 6s +117%
keccakf1600_permute_native 11s 10s +10%
polyveck_caddq 10s 7s +43%
polyveck_use_hint 10s 9s +11%
polyvecl_ntt 10s 11s -9%
keccak_absorb_once_x4 9s 10s -10%
mld_polyvecl_permute_bitrev_to_custom_native 9s 8s +12%
polyveck_invntt_tomont 9s 10s -10%
polyveck_ntt 9s 8s +12%
rej_eta_native 9s 5s +80%
mld_check_pct 8s 7s +14%
mld_sample_s1_s2 8s 6s +33%
polyveck_chknorm 8s 6s +33%
sign 8s 7s +14%
sign_pk_from_sk 8s 9s -11%
poly_decompose_c 7s 7s +0%
poly_invntt_tomont_c 7s 9s -22%
poly_uniform_gamma1_4x 7s 6s +17%
polyveck_reduce 7s 13s -46%
polyveck_sub 7s 7s +0%
keccak_absorb 6s 7s -14%
keccakf1600_permute 6s 7s -14%
mld_compute_pack_z 6s 7s -14%
mld_sample_s1_s2_serial 6s 6s +0%
polyveck_make_hint 6s 5s +20%
polyveck_unpack_eta 6s 3s +100%
rej_eta_c 6s 4s +50%
pack_pk 5s 4s +25%
poly_add 5s 4s +25%
poly_challenge 5s 5s +0%
poly_decompose_native 5s 5s +0%
poly_invntt_tomont 5s 2s +150%
poly_power2round 5s 3s +67%
poly_uniform_eta 5s 4s +25%
polyt1_pack 5s 2s +150%
polyvecl_chknorm 5s 4s +25%
polyvecl_pointwise_acc_montgomery 5s 4s +25%
sign_keypair_internal 5s 6s -17%
sign_signature_pre_hash_shake256 5s 4s +25%
sign_verify 5s 2s +150%
unpack_hints 5s 4s +25%
keccakf1600x4_extract_bytes 4s 2s +100%
mld_h 4s 2s +100%
mld_value_barrier_u8 4s 2s +100%
pack_sig_z 4s 3s +33%
poly_caddq 4s 2s +100%
poly_decompose 4s 3s +33%
poly_ntt_native 4s 6s -33%
poly_pointwise_montgomery_native 4s 3s +33%
poly_reduce 4s 4s +0%
poly_uniform 4s 6s -33%
polyveck_pack_w1 4s 4s +0%
polyvecl_permute_bitrev_to_custom 4s 2s +100%
polyvecl_pointwise_acc_montgomery_native 4s 3s +33%
polyz_unpack_c 4s 5s -20%
shake128_squeeze 4s 5s -20%
shake128x4_squeezeblocks 4s 2s +100%
shake256_absorb 4s 3s +33%
sign_keypair 4s 3s +33%
sign_open 4s 6s -33%
sign_signature 4s 5s -20%
sign_signature_extmu 4s 5s -20%
sign_signature_pre_hash_internal 4s 5s -20%
sign_verify_extmu 4s 3s +33%
sign_verify_pre_hash_shake256 4s 4s +0%
unpack_sk 4s 6s -33%
caddq 3s 4s -25%
decompose 3s 4s -25%
fqscale 3s 5s -40%
intt_native_x86_64 3s 5s -40%
keccak_finalize 3s 2s +50%
keccak_init 3s 3s +0%
keccak_squeeze 3s 4s -25%
keccakf1600_xor_bytes 3s 2s +50%
keccakf1600x4_permute 3s 2s +50%
keccakf1600x4_xor_bytes 3s 2s +50%
make_hint 3s 5s -40%
mld_ct_cmask_neg_i32 3s 1s +200%
mld_ct_cmask_nonzero_u8 3s 3s +0%
mld_ct_get_optblocker_u8 3s 2s +50%
mld_keccakf1600_extract_bytes 3s 1s +200%
montgomery_reduce 3s 3s +0%
ntt_native_x86_64 3s 4s -25%
pack_sk 3s 3s +0%
poly_caddq_native 3s 2s +50%
poly_chknorm 3s 2s +50%
poly_chknorm_native 3s 2s +50%
poly_invntt_tomont_native 3s 2s +50%
poly_make_hint 3s 2s +50%
poly_ntt 3s 3s +0%
poly_ntt_c 3s 1s +200%
poly_pointwise_montgomery 3s 4s -25%
poly_shiftl 3s 2s +50%
poly_sub 3s 3s +0%
poly_use_hint_c 3s 4s -25%
polyt0_pack 3s 5s -40%
polyveck_pack_eta 3s 2s +50%
polyveck_unpack_t0 3s 6s -50%
polyvecl_pack_eta 3s 3s +0%
polyvecl_uniform_gamma1 3s 4s -25%
polyvecl_uniform_gamma1_serial 3s 7s -57%
polyvecl_unpack_z 3s 3s +0%
polyw1_pack 3s 2s +50%
polyz_unpack_native 3s 4s -25%
power2round 3s 4s -25%
rej_eta 3s 2s +50%
shake128_absorb 3s 2s +50%
shake128_init 3s 2s +50%
shake128_release 3s 3s +0%
shake256_finalize 3s 3s +0%
unpack_sig 3s 5s -40%
keccakf1600_extract_bytes (big endian) 2s 3s -33%
keccakf1600_xor_bytes (big endian) 2s 3s -33%
mld_ct_abs_i32 2s 2s +0%
mld_ct_cmask_nonzero_u32 2s 4s -50%
mld_ct_sel_int32 2s 2s +0%
mld_prepare_domain_separation_prefix 2s 3s -33%
mld_value_barrier_i64 2s 3s -33%
mld_value_barrier_u32 2s 2s +0%
pack_sig_c_h 2s 3s -33%
poly_caddq_c 2s 3s -33%
poly_caddq_native_aarch64 2s 3s -33%
poly_uniform_gamma1 2s 3s -33%
poly_use_hint 2s 3s -33%
poly_use_hint_native 2s 4s -50%
polyeta_pack 2s 4s -50%
polyveck_pack_t0 2s 2s +0%
polyvecl_unpack_eta 2s 3s -33%
polyz_pack 2s 2s +0%
polyz_unpack 2s 3s -33%
shake128_finalize 2s 3s -33%
shake256 2s 4s -50%
shake256_release 2s 3s -33%
shake256x4_absorb_once 2s 2s +0%
shake256x4_squeezeblocks 2s 1s +100%
sign_verify_pre_hash_internal 2s 5s -60%
sys_check_capability 2s 3s -33%
unpack_pk 2s 6s -67%
use_hint 2s 3s -33%
mld_ct_get_optblocker_i64 1s 3s -67%
mld_ct_get_optblocker_u32 1s 2s -50%
polyt1_unpack 1s 3s -67%
reduce32 1s 4s -75%
shake128x4_absorb_once 1s 4s -75%
shake256_init 1s 2s -50%
shake256_squeeze 1s 2s -50%

@oqs-bot
Copy link
Contributor

oqs-bot commented Feb 12, 2026

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof Status Current Previous Change
poly_chknorm_c ⚠️ 20s 12s +67%
polyvec_matrix_expand ⚠️ 26s 16s +62%
Full Results (175 proofs)
Proof Status Current Previous Change
**TOTAL** 2120s 2055s +3.2%
mld_attempt_signature_generation 269s 221s +22%
sign_verify_internal 257s 254s +1%
polyvecl_pointwise_acc_montgomery_c 217s 208s +4%
rej_uniform_native 145s 144s +1%
poly_pointwise_montgomery_c 138s 143s -3%
mld_ct_memcmp 85s 82s +4%
mld_invntt_layer 67s 50s +34%
mld_ntt_layer 55s 44s +25%
keccak_squeezeblocks_x4 40s 44s -9%
polyvec_matrix_expand ⚠️ 26s 16s +62%
sign_signature_internal 25s 45s -44%
rej_uniform 23s 20s +15%
fqmul 20s 19s +5%
poly_chknorm_c ⚠️ 20s 12s +67%
poly_uniform_eta_4x 19s 19s +0%
rej_uniform_c 19s 20s -5%
poly_uniform_4x 17s 13s +31%
polymat_permute_bitrev_to_custom 17s 16s +6%
polyt0_unpack 15s 15s +0%
mld_compute_t0_t1_tr_from_sk_components 14s 15s -7%
mld_ntt_butterfly_block 14s 13s +8%
polyz_unpack_c 14s 12s +17%
polyeta_unpack 13s 12s +8%
keccakf1600x4_permute_native 12s 14s -14%
mld_polyvecl_permute_bitrev_to_custom_native 10s 14s -29%
keccak_absorb_once_x4 8s 9s -11%
mld_compute_pack_z 8s 6s +33%
polyveck_chknorm 8s 3s +167%
keccakf1600_permute 7s 8s -12%
keccakf1600_permute_native 7s 6s +17%
mld_check_pct 7s 6s +17%
poly_decompose_c 7s 5s +40%
poly_invntt_tomont_c 7s 39s -82%
poly_uniform_eta 7s 5s +40%
polyveck_add 7s 7s +0%
polyw1_pack 7s 2s +250%
rej_eta_native 7s 4s +75%
sign_keypair_internal 7s 4s +75%
caddq 6s 3s +100%
keccak_absorb 6s 8s -25%
poly_add 6s 4s +50%
poly_ntt_native 6s 2s +200%
poly_pointwise_montgomery_native 6s 3s +100%
poly_use_hint 6s 2s +200%
polyveck_decompose 6s 7s -14%
polyveck_reduce 6s 5s +20%
polyveck_shiftl 6s 5s +20%
polyvecl_ntt 6s 6s +0%
polyvecl_uniform_gamma1 6s 2s +200%
rej_eta_c 6s 4s +50%
sign 6s 5s +20%
sign_pk_from_sk 6s 6s +0%
sign_verify_extmu 6s 2s +200%
decompose 5s 3s +67%
make_hint 5s 3s +67%
mld_ct_cmask_nonzero_u8 5s 4s +25%
mld_prepare_domain_separation_prefix 5s 5s +0%
mld_value_barrier_u32 5s 4s +25%
montgomery_reduce 5s 2s +150%
poly_caddq_native_aarch64 5s 3s +67%
poly_chknorm_native 5s 6s -17%
poly_sub 5s 3s +67%
poly_uniform 5s 5s +0%
poly_use_hint_c 5s 5s +0%
polyvec_matrix_expand_serial 5s 7s -29%
polyvec_matrix_pointwise_montgomery 5s 6s -17%
polyveck_ntt 5s 4s +25%
polyveck_pointwise_poly_montgomery 5s 5s +0%
polyveck_use_hint 5s 5s +0%
polyvecl_chknorm 5s 6s -17%
polyvecl_permute_bitrev_to_custom 5s 2s +150%
polyvecl_pointwise_acc_montgomery_native 5s 3s +67%
polyz_unpack 5s 5s +0%
shake256_release 5s 3s +67%
sign_signature 5s 6s -17%
keccak_init 4s 3s +33%
keccakf1600x4_extract_bytes 4s 3s +33%
keccakf1600x4_xor_bytes 4s 2s +100%
mld_sample_s1_s2 4s 4s +0%
pack_pk 4s 3s +33%
poly_ntt_c 4s 2s +100%
poly_uniform_gamma1 4s 4s +0%
poly_use_hint_native 4s 3s +33%
polyt0_pack 4s 4s +0%
polyt1_pack 4s 1s +300%
polyt1_unpack 4s 4s +0%
polyveck_invntt_tomont 4s 6s -33%
polyveck_pack_eta 4s 3s +33%
polyveck_pack_w1 4s 4s +0%
polyveck_power2round 4s 6s -33%
polyveck_sub 4s 4s +0%
polyvecl_pointwise_acc_montgomery 4s 4s +0%
polyvecl_unpack_z 4s 5s -20%
rej_eta 4s 1s +300%
shake128_release 4s 3s +33%
sign_open 4s 6s -33%
sign_signature_pre_hash_shake256 4s 5s -20%
unpack_hints 4s 5s -20%
fqscale 3s 1s +200%
intt_native_x86_64 3s 3s +0%
keccak_finalize 3s 4s -25%
keccakf1600_extract_bytes (big endian) 3s 3s +0%
keccakf1600x4_permute 3s 3s +0%
mld_h 3s 6s -50%
mld_value_barrier_u8 3s 1s +200%
pack_sig_c_h 3s 4s -25%
pack_sig_z 3s 2s +50%
pack_sk 3s 3s +0%
poly_caddq 3s 3s +0%
poly_challenge 3s 3s +0%
poly_chknorm 3s 4s -25%
poly_decompose_native 3s 3s +0%
poly_invntt_tomont_native 3s 4s -25%
poly_make_hint 3s 4s -25%
poly_power2round 3s 5s -40%
poly_shiftl 3s 4s -25%
poly_uniform_gamma1_4x 3s 4s -25%
polyeta_pack 3s 3s +0%
polyveck_caddq 3s 8s -62%
polyveck_make_hint 3s 4s -25%
polyveck_unpack_t0 3s 4s -25%
polyvecl_unpack_eta 3s 2s +50%
polyz_pack 3s 2s +50%
polyz_unpack_native 3s 3s +0%
reduce32 3s 3s +0%
shake128_absorb 3s 1s +200%
shake256 3s 3s +0%
shake256_absorb 3s 2s +50%
shake256_init 3s 3s +0%
shake256_squeeze 3s 5s -40%
shake256x4_absorb_once 3s 4s -25%
shake256x4_squeezeblocks 3s 2s +50%
sign_keypair 3s 2s +50%
sign_verify 3s 3s +0%
sign_verify_pre_hash_shake256 3s 3s +0%
sys_check_capability 3s 4s -25%
unpack_sig 3s 3s +0%
unpack_sk 3s 4s -25%
use_hint 3s 2s +50%
keccak_squeeze 2s 5s -60%
keccakf1600_xor_bytes 2s 2s +0%
keccakf1600_xor_bytes (big endian) 2s 2s +0%
mld_ct_get_optblocker_i64 2s 2s +0%
mld_ct_get_optblocker_u32 2s 1s +100%
mld_ct_sel_int32 2s 4s -50%
mld_keccakf1600_extract_bytes 2s 6s -67%
mld_sample_s1_s2_serial 2s 3s -33%
mld_value_barrier_i64 2s 4s -50%
ntt_native_x86_64 2s 3s -33%
poly_decompose 2s 4s -50%
poly_invntt_tomont 2s 2s +0%
poly_pointwise_montgomery 2s 2s +0%
poly_reduce 2s 4s -50%
polyvecl_pack_eta 2s 3s -33%
power2round 2s 2s +0%
shake128_finalize 2s 2s +0%
shake128_init 2s 2s +0%
shake128_squeeze 2s 2s +0%
shake128x4_absorb_once 2s 4s -50%
sign_signature_extmu 2s 7s -71%
sign_signature_pre_hash_internal 2s 4s -50%
sign_verify_pre_hash_internal 2s 4s -50%
unpack_pk 2s 3s -33%
mld_ct_abs_i32 1s 2s -50%
mld_ct_cmask_neg_i32 1s 2s -50%
mld_ct_cmask_nonzero_u32 1s 2s -50%
mld_ct_get_optblocker_u8 1s 1s +0%
poly_caddq_c 1s 3s -67%
poly_caddq_native 1s 2s -50%
poly_ntt 1s 3s -67%
polyveck_pack_t0 1s 3s -67%
polyveck_unpack_eta 1s 4s -75%
polyvecl_uniform_gamma1_serial 1s 3s -67%
shake128x4_squeezeblocks 1s 2s -50%
shake256_finalize 1s 4s -75%

@oqs-bot
Copy link
Contributor

oqs-bot commented Feb 12, 2026

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof Status Current Previous Change
sign_verify_internal ⚠️ 368s 177s +108%
Full Results (175 proofs)
Proof Status Current Previous Change
**TOTAL** 2589s 2286s +13.3%
sign_verify_internal ⚠️ 368s 177s +108%
polyvecl_pointwise_acc_montgomery_c 295s 226s +31%
mld_attempt_signature_generation 243s 197s +23%
poly_pointwise_montgomery_c 169s 138s +22%
rej_uniform_native 165s 144s +15%
polyvec_matrix_expand 123s 145s -15%
mld_ct_memcmp 95s 79s +20%
mld_invntt_layer 72s 117s -38%
polyvec_matrix_expand_serial 72s 65s +11%
mld_ntt_layer 60s 44s +36%
keccak_squeezeblocks_x4 40s 42s -5%
sign_signature_internal 34s 50s -32%
mld_compute_t0_t1_tr_from_sk_components 29s 27s +7%
fqmul 23s 18s +28%
rej_uniform 23s 21s +10%
polymat_permute_bitrev_to_custom 21s 18s +17%
poly_chknorm_c 20s 16s +25%
rej_uniform_c 20s 19s +5%
polyvec_matrix_pointwise_montgomery 18s 14s +29%
polyveck_decompose 17s 16s +6%
mld_ntt_butterfly_block 16s 13s +23%
poly_uniform_4x 16s 13s +23%
poly_uniform_eta_4x 16s 17s -6%
polyt0_unpack 16s 17s -6%
polyveck_add 13s 9s +44%
keccakf1600x4_permute_native 12s 14s -14%
polyveck_sub 11s 7s +57%
mld_polyvecl_permute_bitrev_to_custom_native 10s 14s -29%
polyveck_caddq 10s 8s +25%
polyveck_invntt_tomont 10s 8s +25%
polyveck_power2round 10s 11s -9%
keccak_absorb 9s 5s +80%
keccak_absorb_once_x4 9s 10s -10%
keccakf1600_permute_native 9s 9s +0%
mld_check_pct 9s 9s +0%
polyveck_pointwise_poly_montgomery 9s 6s +50%
poly_caddq_c 8s 3s +167%
poly_invntt_tomont_c 8s 8s +0%
polyz_unpack_c 8s 5s +60%
sign 8s 9s -11%
keccakf1600_permute 7s 9s -22%
mld_compute_pack_z 7s 7s +0%
ntt_native_x86_64 7s 3s +133%
polyeta_unpack 7s 7s +0%
polyveck_ntt 7s 6s +17%
polyveck_reduce 7s 9s -22%
polyveck_shiftl 7s 8s -12%
sign_pk_from_sk 7s 8s -12%
sign_verify_pre_hash_internal 7s 3s +133%
mld_prepare_domain_separation_prefix 6s 5s +20%
mld_sample_s1_s2 6s 4s +50%
poly_challenge 6s 4s +50%
poly_pointwise_montgomery_native 6s 2s +200%
poly_uniform 6s 4s +50%
polyvecl_ntt 6s 8s -25%
keccak_squeeze 5s 2s +150%
mld_h 5s 3s +67%
mld_sample_s1_s2_serial 5s 6s -17%
poly_add 5s 4s +25%
poly_decompose_c 5s 7s -29%
poly_invntt_tomont 5s 6s -17%
poly_make_hint 5s 3s +67%
poly_ntt 5s 5s +0%
poly_sub 5s 5s +0%
poly_use_hint_c 5s 7s -29%
polyveck_chknorm 5s 5s +0%
polyveck_use_hint 5s 14s -64%
polyvecl_pointwise_acc_montgomery_native 5s 5s +0%
polyvecl_unpack_z 5s 2s +150%
sign_signature_pre_hash_internal 5s 6s -17%
sign_signature_pre_hash_shake256 5s 4s +25%
decompose 4s 5s -20%
fqscale 4s 4s +0%
keccakf1600x4_xor_bytes 4s 2s +100%
mld_keccakf1600_extract_bytes 4s 2s +100%
pack_pk 4s 3s +33%
pack_sk 4s 2s +100%
poly_decompose_native 4s 3s +33%
poly_ntt_c 4s 2s +100%
poly_ntt_native 4s 3s +33%
poly_uniform_gamma1 4s 5s -20%
poly_use_hint 4s 3s +33%
poly_use_hint_native 4s 4s +0%
polyt0_pack 4s 4s +0%
polyt1_unpack 4s 6s -33%
polyveck_make_hint 4s 5s -20%
polyveck_unpack_eta 4s 4s +0%
polyveck_unpack_t0 4s 3s +33%
polyvecl_uniform_gamma1_serial 4s 4s +0%
rej_eta_native 4s 4s +0%
shake128_init 4s 1s +300%
sign_open 4s 5s -20%
sign_signature 4s 4s +0%
sign_signature_extmu 4s 4s +0%
sign_verify 4s 4s +0%
sign_verify_pre_hash_shake256 4s 6s -33%
unpack_hints 4s 5s -20%
unpack_sk 4s 5s -20%
use_hint 4s 2s +100%
caddq 3s 3s +0%
keccakf1600_extract_bytes (big endian) 3s 3s +0%
mld_ct_get_optblocker_u8 3s 2s +50%
mld_value_barrier_i64 3s 2s +50%
mld_value_barrier_u8 3s 3s +0%
montgomery_reduce 3s 2s +50%
poly_caddq 3s 3s +0%
poly_caddq_native 3s 4s -25%
poly_invntt_tomont_native 3s 7s -57%
poly_pointwise_montgomery 3s 5s -40%
poly_power2round 3s 5s -40%
poly_reduce 3s 5s -40%
poly_shiftl 3s 2s +50%
poly_uniform_eta 3s 3s +0%
poly_uniform_gamma1_4x 3s 6s -50%
polyveck_pack_eta 3s 4s -25%
polyveck_pack_w1 3s 6s -50%
polyvecl_chknorm 3s 5s -40%
polyvecl_pack_eta 3s 4s -25%
polyvecl_uniform_gamma1 3s 5s -40%
polyvecl_unpack_eta 3s 5s -40%
polyz_unpack 3s 2s +50%
polyz_unpack_native 3s 3s +0%
power2round 3s 2s +50%
rej_eta 3s 4s -25%
rej_eta_c 3s 3s +0%
shake256_absorb 3s 5s -40%
shake256_init 3s 2s +50%
shake256_squeeze 3s 2s +50%
sign_keypair 3s 3s +0%
sign_keypair_internal 3s 6s -50%
sign_verify_extmu 3s 4s -25%
sys_check_capability 3s 3s +0%
unpack_pk 3s 3s +0%
intt_native_x86_64 2s 3s -33%
keccakf1600_xor_bytes 2s 3s -33%
keccakf1600_xor_bytes (big endian) 2s 3s -33%
keccakf1600x4_extract_bytes 2s 1s +100%
keccakf1600x4_permute 2s 1s +100%
mld_ct_abs_i32 2s 4s -50%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_cmask_nonzero_u32 2s 2s +0%
mld_ct_cmask_nonzero_u8 2s 2s +0%
mld_value_barrier_u32 2s 3s -33%
pack_sig_c_h 2s 2s +0%
pack_sig_z 2s 2s +0%
poly_caddq_native_aarch64 2s 6s -67%
poly_chknorm 2s 3s -33%
poly_chknorm_native 2s 4s -50%
poly_decompose 2s 3s -33%
polyeta_pack 2s 2s +0%
polyt1_pack 2s 2s +0%
polyveck_pack_t0 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 5s -60%
polyw1_pack 2s 1s +100%
polyz_pack 2s 4s -50%
reduce32 2s 3s -33%
shake128_absorb 2s 2s +0%
shake128_finalize 2s 3s -33%
shake128_release 2s 3s -33%
shake128_squeeze 2s 2s +0%
shake128x4_squeezeblocks 2s 1s +100%
shake256_release 2s 1s +100%
unpack_sig 2s 4s -50%
keccak_finalize 1s 2s -50%
keccak_init 1s 3s -67%
make_hint 1s 3s -67%
mld_ct_get_optblocker_i64 1s 1s +0%
mld_ct_get_optblocker_u32 1s 4s -75%
mld_ct_sel_int32 1s 3s -67%
polyvecl_permute_bitrev_to_custom 1s 3s -67%
shake128x4_absorb_once 1s 4s -75%
shake256 1s 2s -50%
shake256_finalize 1s 5s -80%
shake256x4_absorb_once 1s 4s -75%
shake256x4_squeezeblocks 1s 3s -67%

@rod-chapman
Copy link
Contributor

Proof performance for parameter sets 44,65,87 on r7g/Ubuntu with 64 cores: 4m52s, 6m3s, 4m32s respectively. Looking good.

mkannwischer and others added 2 commits February 23, 2026 09:38
See diffblue/cbmc#8830

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Rod Chapman <rodchap@amazon.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants