Skip to content

Remove --slice-formula from all Makefiles and set in Makefile.common#1049

Merged
mkannwischer merged 1 commit into
mainfrom
simplify-cbmc-options2
Apr 20, 2026
Merged

Remove --slice-formula from all Makefiles and set in Makefile.common#1049
mkannwischer merged 1 commit into
mainfrom
simplify-cbmc-options2

Conversation

@rod-chapman
Copy link
Copy Markdown
Contributor

Remove --slice-formula from all Makefiles and set in Makefile.common

Also, use SMT-only Z3 tactic for proof of poly_invntt_tomont_c() which is faster with --slice-formula

Also, use SMT-only Z3 tactic for proof of poly_invntt_tomont_c() which
is faster with --slice-formula

Signed-off-by: Rod Chapman <rodchap@amazon.com>
@rod-chapman rod-chapman self-assigned this Apr 20, 2026
@rod-chapman rod-chapman requested a review from a team as a code owner April 20, 2026 17:45
@rod-chapman
Copy link
Copy Markdown
Contributor Author

Proof times on Grv4/Ubuntu, CPU user time in minutes:seconds for param sets 44,65,87:

main branch: 32:38, 36:54, 39:25
this branch: 32:06, 36:24, 38:56

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 20, 2026

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof Status Current Previous Change
polyt0_unpack ⚠️ 22s 13s +69%
Full Results (185 proofs)
Proof Status Current Previous Change
**TOTAL** 1776s 1798s -1.2%
sign_verify_internal 234s 231s +1%
rej_uniform_native 129s 142s -9%
polyvecl_pointwise_acc_montgomery_c 113s 112s +1%
poly_pointwise_montgomery_c 109s 160s -32%
mld_invntt_layer 98s 66s +48%
mld_ct_memcmp 83s 78s +6%
mld_attempt_signature_generation 48s 51s -6%
mld_ntt_layer 47s 53s -11%
fqmul 30s 21s +43%
polyvec_matrix_expand_eager 30s 30s +0%
keccakf1600x4_permute_native 23s 25s -8%
sign_keypair_internal 23s 22s +5%
polyt0_unpack ⚠️ 22s 13s +69%
rej_uniform 22s 22s +0%
sign_signature_internal 22s 23s -4%
poly_chknorm_c 19s 21s -10%
mld_ntt_butterfly_block 18s 11s +64%
sign_pk_from_sk 18s 20s -10%
rej_uniform_c 16s 15s +7%
poly_uniform_4x 12s 15s -20%
polyveck_decompose 12s 14s -14%
polyz_unpack_c 12s 13s -8%
poly_add 11s 11s +0%
poly_uniform_eta_4x 11s 17s -35%
polyvec_matrix_expand_eager_serial 11s 10s +10%
mld_check_pct 10s 9s +11%
keccak_absorb_once_x4 9s 11s -18%
poly_invntt_tomont_c 9s 6s +50%
keccakf1600_permute 8s 8s +0%
mld_compute_pack_z 8s 5s +60%
keccak_absorb 7s 10s -30%
keccakf1600_permute_native 7s 9s -22%
pointwise_acc_native_x86_64 7s 5s +40%
polyvec_matrix_pointwise_montgomery_eager 7s 7s +0%
polyveck_chknorm 7s 9s -22%
polyveck_sub 7s 7s +0%
sign 7s 5s +40%
sign_signature 7s 2s +250%
sign_signature_pre_hash_internal 7s 6s +17%
sign_verify_pre_hash_internal 7s 2s +250%
poly_power2round 6s 8s -25%
polyveck_add 6s 6s +0%
polyveck_invntt_tomont 6s 5s +20%
polyveck_power2round 6s 6s +0%
polyveck_use_hint 6s 4s +50%
polyvecl_chknorm 6s 5s +20%
polyvecl_pack_eta 6s 2s +200%
rej_eta_native 6s 8s -25%
sign_open 6s 3s +100%
unpack_sk 6s 6s +0%
keccak_squeezeblocks_x4 5s 5s +0%
keccakf1600x4_permute 5s 2s +150%
make_hint 5s 5s +0%
mld_prepare_domain_separation_prefix 5s 3s +67%
mld_sample_s1_s2_serial 5s 5s +0%
ntt_native_x86_64 5s 4s +25%
pack_pk 5s 4s +25%
pointwise_acc_native_aarch64 5s 8s -38%
pointwise_native_x86_64 5s 4s +25%
poly_caddq 5s 3s +67%
poly_decompose_c 5s 10s -50%
poly_invntt_tomont 5s 1s +400%
poly_uniform_eta 5s 5s +0%
polyveck_caddq 5s 4s +25%
polyveck_pack_w1 5s 3s +67%
polyveck_shiftl 5s 6s -17%
polyveck_unpack_eta 5s 4s +25%
polyvecl_uniform_gamma1_serial 5s 4s +25%
sign_signature_extmu 5s 4s +25%
sign_verify 5s 5s +0%
unpack_hints 5s 6s -17%
caddq 4s 3s +33%
decompose 4s 2s +100%
intt_native_x86_64 4s 3s +33%
keccak_finalize 4s 2s +100%
keccakf1600_extract_bytes (big endian) 4s 1s +300%
mld_sample_s1_s2 4s 5s -20%
montgomery_reduce 4s 4s +0%
pack_sig_h_poly 4s 4s +0%
poly_caddq_native_aarch64 4s 5s -20%
poly_challenge 4s 7s -43%
poly_pointwise_montgomery_native 4s 3s +33%
poly_reduce 4s 3s +33%
poly_shiftl 4s 4s +0%
poly_uniform_gamma1 4s 2s +100%
poly_uniform_gamma1_4x 4s 5s -20%
poly_use_hint_c 4s 5s -20%
polyeta_unpack 4s 15s -73%
polyt1_pack 4s 3s +33%
polyt1_unpack 4s 4s +0%
polyveck_ntt 4s 6s -33%
polyveck_pack_eta 4s 2s +100%
polyveck_pointwise_poly_montgomery 4s 4s +0%
polyveck_reduce 4s 4s +0%
polyvecl_pointwise_acc_montgomery_native 4s 3s +33%
reduce32 4s 4s +0%
rej_eta_c 4s 3s +33%
shake128_finalize 4s 2s +100%
shake128_squeeze 4s 3s +33%
fqscale 3s 1s +200%
keccak_f1600_x1_native_aarch64 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 5s -40%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 3s 3s +0%
keccak_init 3s 3s +0%
keccak_squeeze 3s 2s +50%
keccakf1600x4_extract_bytes 3s 4s -25%
mld_ct_abs_i32 3s 5s -40%
mld_ct_cmask_nonzero_u32 3s 6s -50%
mld_ct_get_optblocker_i64 3s 2s +50%
mld_ct_sel_int32 3s 3s +0%
mld_h 3s 5s -40%
pack_sig_c 3s 4s -25%
pack_sig_z 3s 2s +50%
pack_sk_rho_key_tr_s2_t0 3s 2s +50%
poly_caddq_c 3s 4s -25%
poly_caddq_native 3s 2s +50%
poly_chknorm_native 3s 1s +200%
poly_make_hint 3s 5s -40%
poly_ntt 3s 4s -25%
poly_ntt_c 3s 3s +0%
poly_ntt_native 3s 4s -25%
poly_permute_bitrev_to_custom_optional_native 3s 3s +0%
poly_uniform 3s 3s +0%
poly_use_hint 3s 3s +0%
polyveck_pack_t0 3s 3s +0%
polyvecl_ntt 3s 6s -50%
polyvecl_pointwise_acc_montgomery 3s 3s +0%
polyvecl_unpack_eta 3s 2s +50%
polyz_unpack 3s 2s +50%
power2round 3s 2s +50%
rej_eta 3s 3s +0%
shake128_absorb 3s 3s +0%
shake128_init 3s 3s +0%
shake128x4_squeezeblocks 3s 1s +200%
shake256_absorb 3s 2s +50%
shake256_squeeze 3s 1s +200%
shake256x4_absorb_once 3s 3s +0%
shake256x4_squeezeblocks 3s 1s +200%
sign_keypair 3s 6s -50%
sign_signature_pre_hash_shake256 3s 5s -40%
sign_verify_extmu 3s 5s -40%
sys_check_capability 3s 2s +50%
unpack_pk 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 3s -33%
keccakf1600_xor_bytes 2s 4s -50%
keccakf1600x4_xor_bytes 2s 2s +0%
mld_ct_cmask_neg_i32 2s 4s -50%
mld_ct_cmask_nonzero_u8 2s 1s +100%
mld_ct_get_optblocker_u32 2s 2s +0%
mld_value_barrier_i64 2s 3s -33%
mld_value_barrier_u8 2s 3s -33%
ntt_native_aarch64 2s 5s -60%
pack_sk_s1 2s 3s -33%
pointwise_native_aarch64 2s 4s -50%
poly_chknorm 2s 1s +100%
poly_chknorm_native_aarch64 2s 2s +0%
poly_decompose 2s 3s -33%
poly_decompose_native 2s 3s -33%
poly_invntt_tomont_native 2s 2s +0%
poly_permute_bitrev_to_custom_optional 2s 3s -33%
poly_pointwise_montgomery 2s 2s +0%
poly_sub 2s 1s +100%
poly_use_hint_native 2s 4s -50%
polyeta_pack 2s 2s +0%
polyveck_unpack_t0 2s 3s -33%
polyvecl_uniform_gamma1 2s 1s +100%
polyvecl_unpack_z 2s 2s +0%
polyw1_pack 2s 4s -50%
polyz_pack 2s 3s -33%
polyz_unpack_native 2s 3s -33%
shake128_release 2s 1s +100%
shake128x4_absorb_once 2s 2s +0%
shake256 2s 1s +100%
shake256_finalize 2s 2s +0%
shake256_init 2s 1s +100%
shake256_release 2s 2s +0%
sign_verify_pre_hash_shake256 2s 4s -50%
unpack_sig 2s 2s +0%
use_hint 2s 2s +0%
keccakf1600_xor_bytes (big endian) 1s 2s -50%
mld_ct_get_optblocker_u8 1s 1s +0%
mld_keccakf1600_extract_bytes 1s 3s -67%
mld_value_barrier_u32 1s 2s -50%
polyt0_pack 1s 4s -75%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 20, 2026

CBMC Results (ML-DSA-65)

Full Results (185 proofs)
Proof Status Current Previous Change
**TOTAL** 2052s 2143s -4.2%
sign_verify_internal 232s 236s -2%
polyvecl_pointwise_acc_montgomery_c 217s 234s -7%
polyvec_matrix_expand_eager 165s 173s -5%
rej_uniform_native 119s 139s -14%
poly_pointwise_montgomery_c 104s 154s -32%
mld_invntt_layer 94s 63s +49%
mld_ct_memcmp 76s 75s +1%
mld_attempt_signature_generation 48s 52s -8%
mld_ntt_layer 43s 51s -16%
sign_keypair_internal 30s 30s +0%
sign_signature_internal 29s 30s -3%
fqmul 27s 20s +35%
polyvec_matrix_expand_eager_serial 26s 28s -7%
keccakf1600x4_permute_native 25s 24s +4%
poly_chknorm_c 22s 23s -4%
rej_uniform 21s 22s -5%
polyt0_unpack 20s 16s +25%
sign_pk_from_sk 20s 21s -5%
mld_ntt_butterfly_block 17s 10s +70%
polyveck_pointwise_poly_montgomery 16s 16s +0%
rej_uniform_c 16s 14s +14%
polyveck_power2round 15s 16s -6%
poly_uniform_eta_4x 14s 17s -18%
polyveck_add 14s 10s +40%
poly_add 13s 11s +18%
polyveck_decompose 13s 13s +0%
poly_uniform_4x 11s 14s -21%
keccak_absorb_once_x4 9s 12s -25%
mld_check_pct 9s 7s +29%
poly_invntt_tomont_c 9s 5s +80%
polyveck_use_hint 9s 11s -18%
keccakf1600_permute_native 8s 9s -11%
polyvec_matrix_pointwise_montgomery_eager 8s 7s +14%
polyveck_caddq 8s 7s +14%
polyveck_invntt_tomont 8s 9s -11%
polyveck_ntt 8s 8s +0%
sign 8s 6s +33%
pointwise_acc_native_aarch64 7s 5s +40%
pointwise_acc_native_x86_64 7s 7s +0%
poly_permute_bitrev_to_custom_optional_native 7s 3s +133%
poly_power2round 7s 8s -12%
polyvecl_ntt 7s 6s +17%
polyz_unpack_c 7s 2s +250%
sign_signature_extmu 7s 5s +40%
keccakf1600_permute 6s 10s -40%
mld_compute_pack_z 6s 7s -14%
pointwise_native_aarch64 6s 2s +200%
poly_caddq_c 6s 6s +0%
polyveck_chknorm 6s 7s -14%
polyveck_shiftl 6s 8s -25%
unpack_sk 6s 9s -33%
keccak_absorb 5s 7s -29%
keccak_f1600_x1_native_aarch64 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 5s 3s +67%
pack_sk_rho_key_tr_s2_t0 5s 2s +150%
poly_decompose_c 5s 5s +0%
poly_pointwise_montgomery 5s 3s +67%
poly_shiftl 5s 2s +150%
poly_uniform 5s 6s -17%
polyt0_pack 5s 3s +67%
polyveck_reduce 5s 6s -17%
polyveck_sub 5s 9s -44%
polyvecl_pack_eta 5s 6s -17%
shake256_absorb 5s 3s +67%
sign_open 5s 7s -29%
sign_signature 5s 3s +67%
sign_signature_pre_hash_shake256 5s 3s +67%
sign_verify 5s 4s +25%
intt_native_x86_64 4s 3s +33%
keccak_squeezeblocks_x4 4s 4s +0%
keccakf1600_extract_bytes (big endian) 4s 4s +0%
keccakf1600x4_extract_bytes 4s 4s +0%
make_hint 4s 4s +0%
mld_h 4s 3s +33%
mld_prepare_domain_separation_prefix 4s 6s -33%
mld_sample_s1_s2 4s 6s -33%
ntt_native_x86_64 4s 5s -20%
pack_pk 4s 3s +33%
pack_sig_h_poly 4s 2s +100%
pointwise_native_x86_64 4s 2s +100%
poly_challenge 4s 4s +0%
poly_chknorm 4s 4s +0%
poly_chknorm_native_aarch64 4s 3s +33%
poly_decompose 4s 4s +0%
poly_invntt_tomont 4s 3s +33%
poly_make_hint 4s 3s +33%
poly_ntt 4s 5s -20%
poly_uniform_gamma1 4s 3s +33%
poly_uniform_gamma1_4x 4s 3s +33%
poly_use_hint_native 4s 2s +100%
polyeta_pack 4s 4s +0%
polyeta_unpack 4s 8s -50%
polyveck_pack_eta 4s 3s +33%
polyveck_pack_t0 4s 4s +0%
polyveck_unpack_eta 4s 5s -20%
polyvecl_chknorm 4s 3s +33%
polyvecl_uniform_gamma1_serial 4s 3s +33%
polyvecl_unpack_z 4s 2s +100%
polyz_unpack_native 4s 5s -20%
shake128_absorb 4s 3s +33%
shake128x4_squeezeblocks 4s 3s +33%
shake256 4s 5s -20%
sign_keypair 4s 3s +33%
sign_signature_pre_hash_internal 4s 2s +100%
sign_verify_pre_hash_shake256 4s 5s -20%
unpack_sig 4s 2s +100%
caddq 3s 5s -40%
keccak_squeeze 3s 4s -25%
keccakf1600_xor_bytes 3s 5s -40%
mld_ct_abs_i32 3s 4s -25%
mld_ct_cmask_neg_i32 3s 5s -40%
mld_ct_cmask_nonzero_u32 3s 3s +0%
mld_ct_cmask_nonzero_u8 3s 2s +50%
mld_ct_get_optblocker_u32 3s 2s +50%
mld_keccakf1600_extract_bytes 3s 3s +0%
mld_sample_s1_s2_serial 3s 6s -50%
montgomery_reduce 3s 2s +50%
ntt_native_aarch64 3s 3s +0%
pack_sig_c 3s 3s +0%
pack_sig_z 3s 3s +0%
pack_sk_s1 3s 3s +0%
poly_caddq 3s 3s +0%
poly_caddq_native 3s 3s +0%
poly_caddq_native_aarch64 3s 3s +0%
poly_chknorm_native 3s 2s +50%
poly_ntt_native 3s 4s -25%
poly_permute_bitrev_to_custom_optional 3s 3s +0%
poly_sub 3s 4s -25%
poly_use_hint 3s 6s -50%
polyt1_pack 3s 4s -25%
polyveck_pack_w1 3s 2s +50%
polyvecl_pointwise_acc_montgomery 3s 4s -25%
polyvecl_pointwise_acc_montgomery_native 3s 3s +0%
polyz_pack 3s 4s -25%
power2round 3s 2s +50%
reduce32 3s 3s +0%
rej_eta 3s 2s +50%
rej_eta_c 3s 4s -25%
rej_eta_native 3s 3s +0%
shake128x4_absorb_once 3s 2s +50%
sign_verify_extmu 3s 3s +0%
sign_verify_pre_hash_internal 3s 6s -50%
sys_check_capability 3s 3s +0%
unpack_hints 3s 4s -25%
unpack_pk 3s 3s +0%
use_hint 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 2s +0%
keccak_finalize 2s 2s +0%
keccak_init 2s 3s -33%
keccakf1600_xor_bytes (big endian) 2s 4s -50%
keccakf1600x4_permute 2s 2s +0%
keccakf1600x4_xor_bytes 2s 4s -50%
mld_ct_get_optblocker_i64 2s 5s -60%
mld_ct_sel_int32 2s 2s +0%
mld_value_barrier_i64 2s 3s -33%
mld_value_barrier_u32 2s 3s -33%
mld_value_barrier_u8 2s 5s -60%
poly_decompose_native 2s 2s +0%
poly_invntt_tomont_native 2s 4s -50%
poly_ntt_c 2s 4s -50%
poly_pointwise_montgomery_native 2s 3s -33%
poly_reduce 2s 2s +0%
poly_uniform_eta 2s 5s -60%
poly_use_hint_c 2s 7s -71%
polyt1_unpack 2s 4s -50%
polyveck_unpack_t0 2s 2s +0%
polyvecl_uniform_gamma1 2s 3s -33%
polyvecl_unpack_eta 2s 3s -33%
polyw1_pack 2s 3s -33%
polyz_unpack 2s 3s -33%
shake128_finalize 2s 2s +0%
shake128_init 2s 3s -33%
shake128_release 2s 3s -33%
shake128_squeeze 2s 2s +0%
shake256_init 2s 2s +0%
shake256_release 2s 2s +0%
shake256_squeeze 2s 3s -33%
shake256x4_absorb_once 2s 1s +100%
decompose 1s 2s -50%
fqscale 1s 2s -50%
mld_ct_get_optblocker_u8 1s 1s +0%
shake256_finalize 1s 3s -67%
shake256x4_squeezeblocks 1s 4s -75%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 20, 2026

CBMC Results (ML-DSA-87)

Full Results (185 proofs)
Proof Status Current Previous Change
**TOTAL** 2271s 2433s -6.7%
polyvecl_pointwise_acc_montgomery_c 279s 321s -13%
sign_verify_internal 277s 294s -6%
polyvec_matrix_expand_eager 138s 145s -5%
rej_uniform_native 125s 143s -13%
poly_pointwise_montgomery_c 115s 177s -35%
mld_invntt_layer 99s 68s +46%
mld_attempt_signature_generation 81s 81s +0%
mld_ct_memcmp 78s 82s -5%
polyvec_matrix_expand_eager_serial 62s 65s -5%
sign_keypair_internal 46s 52s -12%
mld_ntt_layer 43s 54s -20%
fqmul 29s 20s +45%
sign_signature_internal 26s 26s +0%
keccakf1600x4_permute_native 25s 24s +4%
sign_pk_from_sk 25s 28s -11%
rej_uniform 20s 23s -13%
polyt0_unpack 19s 13s +46%
poly_chknorm_c 18s 23s -22%
polyveck_sub 18s 7s +157%
polyveck_chknorm 17s 19s -11%
mld_compute_pack_z 16s 9s +78%
polyveck_decompose 16s 16s +0%
rej_uniform_c 16s 15s +7%
mld_ntt_butterfly_block 15s 12s +25%
poly_uniform_eta_4x 15s 18s -17%
poly_add 12s 11s +9%
poly_uniform_4x 12s 13s -8%
polyvec_matrix_pointwise_montgomery_eager 12s 15s -20%
polyveck_add 12s 12s +0%
polyvecl_ntt 10s 8s +25%
keccak_absorb_once_x4 9s 11s -18%
mld_check_pct 9s 10s -10%
pointwise_acc_native_x86_64 9s 8s +12%
polyveck_power2round 9s 8s +12%
keccakf1600_permute_native 8s 8s +0%
poly_decompose_c 8s 7s +14%
keccak_absorb 7s 7s +0%
keccakf1600_permute 7s 8s -12%
mld_sample_s1_s2 7s 8s -12%
poly_invntt_tomont_c 7s 6s +17%
poly_power2round 7s 5s +40%
poly_shiftl 7s 5s +40%
polyveck_caddq 7s 10s -30%
polyveck_invntt_tomont 7s 8s -12%
polyveck_ntt 7s 8s -12%
polyveck_pointwise_poly_montgomery 7s 9s -22%
polyveck_reduce 7s 8s -12%
shake128x4_squeezeblocks 7s 3s +133%
sign 7s 5s +40%
unpack_hints 7s 5s +40%
mld_ct_cmask_nonzero_u8 6s 2s +200%
pointwise_acc_native_aarch64 6s 6s +0%
poly_uniform 6s 4s +50%
polyveck_use_hint 6s 10s -40%
polyvecl_unpack_eta 6s 5s +20%
sign_signature 6s 6s +0%
sign_verify_pre_hash_internal 6s 4s +50%
unpack_sk 6s 10s -40%
keccakf1600x4_xor_bytes 5s 3s +67%
make_hint 5s 3s +67%
mld_prepare_domain_separation_prefix 5s 4s +25%
mld_sample_s1_s2_serial 5s 5s +0%
ntt_native_x86_64 5s 4s +25%
poly_challenge 5s 4s +25%
poly_chknorm_native_aarch64 5s 3s +67%
poly_reduce 5s 3s +67%
polyeta_unpack 5s 14s -64%
polyt0_pack 5s 3s +67%
polyveck_shiftl 5s 9s -44%
polyvecl_chknorm 5s 4s +25%
polyvecl_uniform_gamma1 5s 5s +0%
polyz_unpack_native 5s 3s +67%
rej_eta_c 5s 4s +25%
shake256x4_absorb_once 5s 2s +150%
sign_open 5s 5s +0%
sign_signature_pre_hash_shake256 5s 3s +67%
unpack_sig 5s 4s +25%
use_hint 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 4s 3s +33%
keccak_squeeze 4s 3s +33%
mld_ct_sel_int32 4s 2s +100%
mld_h 4s 4s +0%
mld_keccakf1600_extract_bytes 4s 4s +0%
pointwise_native_aarch64 4s 4s +0%
poly_caddq_c 4s 7s -43%
poly_caddq_native_aarch64 4s 4s +0%
poly_invntt_tomont_native 4s 4s +0%
poly_permute_bitrev_to_custom_optional_native 4s 5s -20%
poly_use_hint_c 4s 3s +33%
poly_use_hint_native 4s 1s +300%
polyeta_pack 4s 3s +33%
polyveck_pack_w1 4s 2s +100%
polyveck_unpack_eta 4s 3s +33%
polyveck_unpack_t0 4s 4s +0%
polyvecl_pointwise_acc_montgomery_native 4s 3s +33%
polyz_unpack 4s 5s -20%
polyz_unpack_c 4s 9s -56%
power2round 4s 3s +33%
reduce32 4s 4s +0%
sign_signature_extmu 4s 6s -33%
sign_signature_pre_hash_internal 4s 4s +0%
sign_verify_extmu 4s 6s -33%
sign_verify_pre_hash_shake256 4s 4s +0%
caddq 3s 1s +200%
decompose 3s 3s +0%
intt_native_x86_64 3s 5s -40%
keccak_squeezeblocks_x4 3s 7s -57%
keccakf1600x4_extract_bytes 3s 2s +50%
mld_ct_get_optblocker_i64 3s 2s +50%
mld_ct_get_optblocker_u32 3s 4s -25%
mld_ct_get_optblocker_u8 3s 4s -25%
mld_value_barrier_i64 3s 2s +50%
mld_value_barrier_u8 3s 2s +50%
ntt_native_aarch64 3s 4s -25%
pack_pk 3s 2s +50%
pack_sig_z 3s 3s +0%
pack_sk_s1 3s 3s +0%
pointwise_native_x86_64 3s 4s -25%
poly_caddq 3s 4s -25%
poly_caddq_native 3s 4s -25%
poly_chknorm_native 3s 2s +50%
poly_decompose 3s 4s -25%
poly_make_hint 3s 3s +0%
poly_permute_bitrev_to_custom_optional 3s 2s +50%
poly_pointwise_montgomery 3s 2s +50%
poly_sub 3s 2s +50%
poly_uniform_eta 3s 3s +0%
poly_uniform_gamma1 3s 3s +0%
polyveck_pack_eta 3s 3s +0%
polyvecl_pack_eta 3s 5s -40%
polyvecl_pointwise_acc_montgomery 3s 4s -25%
polyvecl_uniform_gamma1_serial 3s 4s -25%
polyvecl_unpack_z 3s 2s +50%
rej_eta 3s 4s -25%
rej_eta_native 3s 8s -62%
shake128_init 3s 2s +50%
shake256 3s 4s -25%
shake256_absorb 3s 2s +50%
shake256_squeeze 3s 3s +0%
shake256x4_squeezeblocks 3s 3s +0%
sys_check_capability 3s 4s -25%
unpack_pk 3s 5s -40%
fqscale 2s 2s +0%
keccak_f1600_x1_native_aarch64 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 3s -33%
keccak_finalize 2s 4s -50%
keccak_init 2s 4s -50%
keccakf1600_xor_bytes 2s 2s +0%
keccakf1600_xor_bytes (big endian) 2s 3s -33%
keccakf1600x4_permute 2s 3s -33%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_value_barrier_u32 2s 2s +0%
montgomery_reduce 2s 3s -33%
pack_sig_c 2s 3s -33%
pack_sig_h_poly 2s 3s -33%
poly_chknorm 2s 3s -33%
poly_decompose_native 2s 2s +0%
poly_invntt_tomont 2s 3s -33%
poly_ntt 2s 4s -50%
poly_ntt_c 2s 6s -67%
poly_pointwise_montgomery_native 2s 4s -50%
poly_uniform_gamma1_4x 2s 2s +0%
poly_use_hint 2s 3s -33%
polyt1_pack 2s 3s -33%
polyt1_unpack 2s 4s -50%
polyveck_pack_t0 2s 2s +0%
polyw1_pack 2s 6s -67%
polyz_pack 2s 4s -50%
shake128_absorb 2s 2s +0%
shake128_finalize 2s 2s +0%
shake128_release 2s 3s -33%
shake128_squeeze 2s 3s -33%
shake128x4_absorb_once 2s 1s +100%
shake256_finalize 2s 3s -33%
shake256_init 2s 5s -60%
shake256_release 2s 2s +0%
sign_keypair 2s 3s -33%
sign_verify 2s 4s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 1s 4s -75%
keccakf1600_extract_bytes (big endian) 1s 3s -67%
mld_ct_abs_i32 1s 1s +0%
mld_ct_cmask_nonzero_u32 1s 2s -50%
pack_sk_rho_key_tr_s2_t0 1s 4s -75%
poly_ntt_native 1s 2s -50%

Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

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

Thanks @rod-chapman. LGTM. Performance improved slightly.

@mkannwischer mkannwischer merged commit e446794 into main Apr 20, 2026
405 checks passed
@mkannwischer mkannwischer deleted the simplify-cbmc-options2 branch April 20, 2026 23:55
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.

3 participants