Skip to content

CBMC: Update to v6.9.0#1041

Merged
mkannwischer merged 1 commit intomainfrom
cbmc69
Apr 15, 2026
Merged

CBMC: Update to v6.9.0#1041
mkannwischer merged 1 commit intomainfrom
cbmc69

Conversation

@hanno-becker
Copy link
Copy Markdown
Contributor

@hanno-becker hanno-becker commented Apr 15, 2026

This hopefully enables the use of unions (cf #1016 #826), but this is left for a follow-up PR. Here, we merely update the version in nix.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker hanno-becker requested a review from a team as a code owner April 15, 2026 04:18
@hanno-becker hanno-becker changed the title CBMC: Update to v6.9 CBMC: Update to v6.9.0 Apr 15, 2026
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 15, 2026

CBMC Results (ML-DSA-44)

Full Results (186 proofs)
Proof Status Current Previous Change
**TOTAL** 1879s 2114s -11.1%
sign_verify_internal 215s 162s +33%
polyvecl_pointwise_acc_montgomery_c 155s 168s -8%
poly_pointwise_montgomery_c 144s 153s -6%
rej_uniform_native 135s 146s -8%
mld_attempt_signature_generation 122s 281s -57%
mld_ct_memcmp 73s 76s -4%
mld_invntt_layer 64s 108s -41%
mld_ntt_layer 51s 55s -7%
polyvec_matrix_expand 27s 23s +17%
polymat_permute_bitrev_to_custom 26s 27s -4%
rej_uniform 23s 25s -8%
fqmul 21s 21s +0%
sign_signature_internal 21s 21s +0%
poly_chknorm_c 20s 20s +0%
poly_uniform_eta_4x 16s 16s +0%
poly_uniform_4x 15s 13s +15%
polyeta_unpack 15s 17s -12%
rej_uniform_c 15s 16s -6%
keccakf1600x4_permute_native 13s 13s +0%
mld_compute_t0_t1_tr_from_sk_components 13s 12s +8%
polyt0_unpack 13s 19s -32%
poly_add 12s 11s +9%
polyz_unpack_c 12s 12s +0%
mld_ntt_butterfly_block 10s 14s -29%
polyveck_decompose 10s 7s +43%
keccak_absorb_once_x4 9s 12s -25%
mld_check_pct 9s 13s -31%
polyveck_add 9s 4s +125%
keccak_absorb 8s 7s +14%
keccakf1600_permute_native 8s 7s +14%
poly_decompose_c 8s 3s +167%
sign 8s 8s +0%
pointwise_acc_native_aarch64 7s 8s -12%
pointwise_acc_native_x86_64 7s 4s +75%
polyvec_matrix_expand_serial 7s 21s -67%
polyvec_matrix_pointwise_montgomery 7s 9s -22%
polyveck_pointwise_poly_montgomery 7s 4s +75%
polyveck_sub 7s 6s +17%
polyvecl_chknorm 7s 4s +75%
sign_pk_from_sk 7s 10s -30%
unpack_sk 7s 8s -12%
keccakf1600_permute 6s 7s -14%
mld_ct_abs_i32 6s 1s +500%
mld_sample_s1_s2 6s 5s +20%
pack_sig_z 6s 2s +200%
poly_invntt_tomont_c 6s 26s -77%
poly_ntt_c 6s 4s +50%
poly_use_hint_c 6s 4s +50%
polyveck_ntt 6s 4s +50%
polyveck_power2round 6s 4s +50%
polyveck_shiftl 6s 6s +0%
polyvecl_uniform_gamma1 6s 4s +50%
rej_eta_native 6s 8s -25%
sign_open 6s 5s +20%
sign_signature 6s 3s +100%
sign_signature_pre_hash_shake256 6s 4s +50%
unpack_hints 6s 6s +0%
mld_compute_pack_z 5s 7s -29%
mld_ct_get_optblocker_u8 5s 3s +67%
pack_sk 5s 3s +67%
poly_caddq 5s 2s +150%
poly_challenge 5s 4s +25%
poly_power2round 5s 9s -44%
poly_sub 5s 3s +67%
poly_uniform 5s 2s +150%
polyt0_pack 5s 5s +0%
polyt1_unpack 5s 2s +150%
polyveck_chknorm 5s 6s -17%
polyveck_invntt_tomont 5s 2s +150%
polyveck_reduce 5s 5s +0%
polyvecl_pointwise_acc_montgomery_native 5s 2s +150%
polyvecl_uniform_gamma1_serial 5s 3s +67%
polyvecl_unpack_eta 5s 2s +150%
polyvecl_unpack_z 5s 4s +25%
rej_eta_c 5s 4s +25%
sign_keypair_internal 5s 4s +25%
sign_signature_extmu 5s 3s +67%
sign_verify 5s 3s +67%
sign_verify_extmu 5s 7s -29%
sign_verify_pre_hash_shake256 5s 4s +25%
keccak_squeezeblocks_x4 4s 5s -20%
mld_ct_cmask_nonzero_u32 4s 3s +33%
mld_ct_cmask_nonzero_u8 4s 5s -20%
montgomery_reduce 4s 4s +0%
ntt_native_x86_64 4s 3s +33%
pack_sig_h_poly 4s 3s +33%
pointwise_native_x86_64 4s 5s -20%
poly_caddq_c 4s 5s -20%
poly_chknorm_native_aarch64 4s 3s +33%
poly_reduce 4s 4s +0%
poly_uniform_gamma1 4s 3s +33%
poly_uniform_gamma1_4x 4s 3s +33%
poly_use_hint 4s 3s +33%
polyeta_pack 4s 3s +33%
polyveck_caddq 4s 4s +0%
polyveck_pack_eta 4s 3s +33%
polyveck_use_hint 4s 6s -33%
polyvecl_ntt 4s 5s -20%
polyvecl_pack_eta 4s 3s +33%
polyvecl_permute_bitrev_to_custom 4s 5s -20%
polyw1_pack 4s 3s +33%
polyz_pack 4s 3s +33%
polyz_unpack 4s 5s -20%
polyz_unpack_native 4s 2s +100%
shake256_init 4s 3s +33%
shake256x4_squeezeblocks 4s 1s +300%
sign_keypair 4s 5s -20%
decompose 3s 3s +0%
keccak_f1600_x1_native_aarch64 3s 6s -50%
keccak_f1600_x1_native_aarch64_v84a 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 3s 4s -25%
keccakf1600_xor_bytes 3s 2s +50%
keccakf1600x4_permute 3s 3s +0%
keccakf1600x4_xor_bytes 3s 2s +50%
mld_ct_cmask_neg_i32 3s 3s +0%
mld_h 3s 3s +0%
mld_keccakf1600_extract_bytes 3s 2s +50%
mld_polyvecl_permute_bitrev_to_custom_native 3s 10s -70%
mld_prepare_domain_separation_prefix 3s 2s +50%
mld_value_barrier_u32 3s 2s +50%
ntt_native_aarch64 3s 3s +0%
pack_pk 3s 4s -25%
pack_sig_c 3s 2s +50%
poly_caddq_native 3s 3s +0%
poly_caddq_native_aarch64 3s 4s -25%
poly_chknorm 3s 5s -40%
poly_chknorm_native 3s 3s +0%
poly_invntt_tomont_native 3s 4s -25%
poly_pointwise_montgomery 3s 2s +50%
poly_pointwise_montgomery_native 3s 1s +200%
poly_shiftl 3s 3s +0%
poly_uniform_eta 3s 5s -40%
poly_use_hint_native 3s 4s -25%
polyveck_pack_t0 3s 4s -25%
polyveck_pack_w1 3s 5s -40%
polyveck_unpack_eta 3s 3s +0%
polyveck_unpack_t0 3s 4s -25%
power2round 3s 3s +0%
reduce32 3s 3s +0%
shake128_squeeze 3s 4s -25%
shake128x4_absorb_once 3s 3s +0%
shake128x4_squeezeblocks 3s 2s +50%
shake256_squeeze 3s 3s +0%
sign_verify_pre_hash_internal 3s 3s +0%
sys_check_capability 3s 5s -40%
unpack_pk 3s 2s +50%
unpack_sig 3s 3s +0%
caddq 2s 4s -50%
fqscale 2s 4s -50%
intt_native_x86_64 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 2s +0%
keccak_finalize 2s 4s -50%
keccak_init 2s 3s -33%
keccak_squeeze 2s 1s +100%
keccakf1600_extract_bytes (big endian) 2s 3s -33%
keccakf1600_xor_bytes (big endian) 2s 2s +0%
keccakf1600x4_extract_bytes 2s 3s -33%
make_hint 2s 3s -33%
mld_ct_get_optblocker_i64 2s 5s -60%
mld_ct_get_optblocker_u32 2s 1s +100%
mld_ct_sel_int32 2s 3s -33%
mld_sample_s1_s2_serial 2s 5s -60%
mld_value_barrier_i64 2s 3s -33%
mld_value_barrier_u8 2s 4s -50%
pointwise_native_aarch64 2s 5s -60%
poly_decompose 2s 4s -50%
poly_decompose_native 2s 6s -67%
poly_invntt_tomont 2s 3s -33%
poly_make_hint 2s 2s +0%
poly_ntt 2s 1s +100%
poly_ntt_native 2s 4s -50%
polyt1_pack 2s 5s -60%
polyvecl_pointwise_acc_montgomery 2s 2s +0%
rej_eta 2s 6s -67%
shake128_absorb 2s 3s -33%
shake128_finalize 2s 5s -60%
shake128_init 2s 5s -60%
shake128_release 2s 3s -33%
shake256 2s 4s -50%
shake256_absorb 2s 4s -50%
shake256_release 2s 3s -33%
shake256x4_absorb_once 2s 3s -33%
sign_signature_pre_hash_internal 2s 5s -60%
use_hint 2s 3s -33%
shake256_finalize 1s 2s -50%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 15, 2026

CBMC Results (ML-DSA-65)

Full Results (186 proofs)
Proof Status Current Previous Change
**TOTAL** 2324s 2682s -13.3%
polyvecl_pointwise_acc_montgomery_c 510s 540s -6%
sign_verify_internal 246s 304s -19%
rej_uniform_native 133s 138s -4%
poly_pointwise_montgomery_c 131s 236s -44%
polyvec_matrix_expand 80s 108s -26%
mld_attempt_signature_generation 79s 113s -30%
mld_ct_memcmp 71s 74s -4%
mld_invntt_layer 62s 95s -35%
mld_ntt_layer 49s 54s -9%
polyvec_matrix_expand_serial 45s 82s -45%
polymat_permute_bitrev_to_custom 33s 34s -3%
sign_signature_internal 29s 24s +21%
mld_compute_t0_t1_tr_from_sk_components 25s 27s -7%
rej_uniform 22s 21s +5%
fqmul 20s 21s -5%
poly_chknorm_c 20s 19s +5%
polyveck_decompose 18s 18s +0%
poly_uniform_eta_4x 16s 15s +7%
polyt0_unpack 15s 13s +15%
poly_uniform_4x 14s 14s +0%
polyveck_power2round 14s 12s +17%
rej_uniform_c 14s 16s -12%
keccakf1600x4_permute_native 13s 13s +0%
mld_check_pct 12s 11s +9%
polyvec_matrix_pointwise_montgomery 12s 12s +0%
polyveck_add 12s 8s +50%
keccak_absorb_once_x4 11s 9s +22%
poly_add 11s 12s -8%
polyveck_caddq 11s 8s +38%
keccakf1600_permute_native 9s 8s +12%
mld_compute_pack_z 9s 11s -18%
mld_ntt_butterfly_block 9s 13s -31%
pointwise_acc_native_x86_64 9s 6s +50%
polyveck_use_hint 9s 24s -62%
sign_pk_from_sk 9s 7s +29%
keccakf1600_permute 8s 8s +0%
polyvecl_ntt 8s 6s +33%
keccak_absorb 7s 8s -12%
mld_sample_s1_s2 7s 6s +17%
polyveck_ntt 7s 9s -22%
polyveck_pointwise_poly_montgomery 7s 7s +0%
polyveck_shiftl 7s 9s -22%
polyveck_sub 7s 6s +17%
sign 7s 7s +0%
sign_open 7s 7s +0%
unpack_sk 7s 10s -30%
fqscale 6s 3s +100%
mld_sample_s1_s2_serial 6s 4s +50%
ntt_native_x86_64 6s 3s +100%
poly_caddq_c 6s 6s +0%
poly_decompose_c 6s 6s +0%
poly_decompose_native 6s 2s +200%
poly_invntt_tomont_c 6s 9s -33%
poly_uniform_eta 6s 4s +50%
polyt0_pack 6s 4s +50%
reduce32 6s 2s +200%
sign_keypair_internal 6s 5s +20%
decompose 5s 3s +67%
keccak_squeezeblocks_x4 5s 8s -38%
mld_h 5s 6s -17%
pack_sig_z 5s 5s +0%
pointwise_acc_native_aarch64 5s 6s -17%
poly_caddq 5s 2s +150%
poly_pointwise_montgomery_native 5s 2s +150%
poly_shiftl 5s 3s +67%
poly_uniform 5s 3s +67%
poly_uniform_gamma1 5s 2s +150%
poly_use_hint_c 5s 6s -17%
polyeta_unpack 5s 4s +25%
polyveck_reduce 5s 6s -17%
polyveck_unpack_t0 5s 3s +67%
polyvecl_uniform_gamma1_serial 5s 2s +150%
polyz_unpack 5s 5s +0%
sign_keypair 5s 4s +25%
sign_verify 5s 5s +0%
caddq 4s 3s +33%
intt_native_x86_64 4s 3s +33%
keccak_finalize 4s 5s -20%
keccak_squeeze 4s 2s +100%
mld_polyvecl_permute_bitrev_to_custom_native 4s 10s -60%
mld_value_barrier_u8 4s 2s +100%
pack_sig_c 4s 2s +100%
poly_caddq_native_aarch64 4s 2s +100%
poly_chknorm 4s 2s +100%
poly_chknorm_native_aarch64 4s 2s +100%
poly_decompose 4s 3s +33%
poly_ntt 4s 4s +0%
poly_ntt_native 4s 3s +33%
poly_power2round 4s 5s -20%
poly_uniform_gamma1_4x 4s 6s -33%
polyeta_pack 4s 3s +33%
polyveck_invntt_tomont 4s 7s -43%
polyveck_pack_w1 4s 1s +300%
polyvecl_chknorm 4s 4s +0%
polyvecl_unpack_eta 4s 4s +0%
rej_eta_c 4s 4s +0%
shake256_absorb 4s 1s +300%
sign_signature_pre_hash_internal 4s 3s +33%
sign_signature_pre_hash_shake256 4s 4s +0%
sign_verify_pre_hash_internal 4s 5s -20%
sign_verify_pre_hash_shake256 4s 6s -33%
unpack_hints 4s 7s -43%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 2s +50%
keccak_init 3s 2s +50%
keccakf1600_xor_bytes 3s 3s +0%
keccakf1600x4_permute 3s 2s +50%
mld_ct_abs_i32 3s 2s +50%
mld_ct_cmask_nonzero_u8 3s 2s +50%
mld_ct_get_optblocker_i64 3s 3s +0%
mld_prepare_domain_separation_prefix 3s 5s -40%
montgomery_reduce 3s 3s +0%
ntt_native_aarch64 3s 3s +0%
pack_pk 3s 2s +50%
pointwise_native_x86_64 3s 3s +0%
poly_challenge 3s 4s -25%
poly_chknorm_native 3s 3s +0%
poly_invntt_tomont 3s 4s -25%
poly_invntt_tomont_native 3s 4s -25%
poly_pointwise_montgomery 3s 2s +50%
poly_reduce 3s 1s +200%
poly_use_hint 3s 1s +200%
poly_use_hint_native 3s 2s +50%
polyveck_chknorm 3s 8s -62%
polyvecl_permute_bitrev_to_custom 3s 4s -25%
polyvecl_pointwise_acc_montgomery_native 3s 3s +0%
polyvecl_uniform_gamma1 3s 4s -25%
polyz_pack 3s 4s -25%
polyz_unpack_c 3s 1s +200%
polyz_unpack_native 3s 3s +0%
power2round 3s 2s +50%
rej_eta 3s 2s +50%
shake128_absorb 3s 2s +50%
shake128_init 3s 2s +50%
shake128x4_absorb_once 3s 2s +50%
shake256_init 3s 1s +200%
shake256_release 3s 2s +50%
shake256_squeeze 3s 3s +0%
shake256x4_absorb_once 3s 2s +50%
sign_signature 3s 3s +0%
sign_signature_extmu 3s 3s +0%
sign_verify_extmu 3s 5s -40%
unpack_sig 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 3s -33%
keccakf1600_xor_bytes (big endian) 2s 2s +0%
keccakf1600x4_extract_bytes 2s 3s -33%
keccakf1600x4_xor_bytes 2s 3s -33%
make_hint 2s 4s -50%
mld_ct_cmask_neg_i32 2s 3s -33%
mld_ct_get_optblocker_u32 2s 3s -33%
mld_ct_get_optblocker_u8 2s 4s -50%
mld_ct_sel_int32 2s 2s +0%
mld_keccakf1600_extract_bytes 2s 1s +100%
mld_value_barrier_i64 2s 2s +0%
mld_value_barrier_u32 2s 2s +0%
pack_sig_h_poly 2s 6s -67%
pointwise_native_aarch64 2s 5s -60%
poly_caddq_native 2s 4s -50%
poly_make_hint 2s 5s -60%
poly_ntt_c 2s 3s -33%
polyt1_pack 2s 3s -33%
polyt1_unpack 2s 3s -33%
polyveck_pack_eta 2s 3s -33%
polyveck_unpack_eta 2s 4s -50%
polyvecl_pack_eta 2s 4s -50%
polyvecl_pointwise_acc_montgomery 2s 4s -50%
polyvecl_unpack_z 2s 6s -67%
polyw1_pack 2s 2s +0%
rej_eta_native 2s 3s -33%
shake128_finalize 2s 3s -33%
shake128_squeeze 2s 2s +0%
shake128x4_squeezeblocks 2s 3s -33%
shake256 2s 3s -33%
shake256x4_squeezeblocks 2s 2s +0%
sys_check_capability 2s 5s -60%
unpack_pk 2s 3s -33%
use_hint 2s 3s -33%
keccak_f1600_x1_native_aarch64 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 1s 5s -80%
keccakf1600_extract_bytes (big endian) 1s 3s -67%
mld_ct_cmask_nonzero_u32 1s 2s -50%
pack_sk 1s 2s -50%
poly_sub 1s 2s -50%
polyveck_pack_t0 1s 5s -80%
shake128_release 1s 4s -75%
shake256_finalize 1s 2s -50%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 15, 2026

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof Status Current Previous Change
polyveck_invntt_tomont ⚠️ 27s 9s +200%
sign_verify_internal ⚠️ 171s 107s +60%
Full Results (186 proofs)
Proof Status Current Previous Change
**TOTAL** 3460s 3454s +0.2%
polyvecl_pointwise_acc_montgomery_c 1248s 1161s +7%
mld_attempt_signature_generation 244s 201s +21%
polyvec_matrix_expand 180s 243s -26%
poly_pointwise_montgomery_c 171s 257s -33%
sign_verify_internal ⚠️ 171s 107s +60%
rej_uniform_native 146s 150s -3%
polyvec_matrix_expand_serial 124s 85s +46%
mld_ct_memcmp 79s 79s +0%
mld_invntt_layer 68s 104s -35%
mld_ntt_layer 54s 56s -4%
sign_signature_internal 37s 43s -14%
polymat_permute_bitrev_to_custom 27s 27s +0%
polyveck_invntt_tomont ⚠️ 27s 9s +200%
mld_compute_t0_t1_tr_from_sk_components 24s 24s +0%
fqmul 22s 20s +10%
poly_chknorm_c 21s 20s +5%
rej_uniform 21s 21s +0%
poly_uniform_eta_4x 20s 18s +11%
polyeta_unpack 16s 20s -20%
rej_uniform_c 15s 14s +7%
keccakf1600x4_permute_native 14s 14s +0%
polyt0_unpack 14s 15s -7%
polyveck_decompose 14s 14s +0%
poly_uniform_4x 13s 17s -24%
polyveck_add 13s 9s +44%
mld_check_pct 12s 16s -25%
keccak_absorb_once_x4 11s 13s -15%
mld_ntt_butterfly_block 11s 13s -15%
polyveck_power2round 11s 18s -39%
sign_pk_from_sk 11s 9s +22%
poly_add 10s 9s +11%
unpack_sk 10s 9s +11%
keccakf1600_permute 9s 10s -10%
mld_sample_s1_s2_serial 9s 6s +50%
polyvec_matrix_pointwise_montgomery 9s 10s -10%
polyveck_caddq 9s 4s +125%
polyveck_reduce 9s 7s +29%
polyz_unpack_c 9s 9s +0%
keccak_squeezeblocks_x4 8s 7s +14%
mld_compute_pack_z 8s 7s +14%
mld_polyvecl_permute_bitrev_to_custom_native 8s 11s -27%
keccak_absorb 7s 9s -22%
keccakf1600_permute_native 7s 7s +0%
mld_ct_cmask_nonzero_u8 7s 5s +40%
mld_sample_s1_s2 7s 7s +0%
pointwise_acc_native_aarch64 7s 5s +40%
pointwise_acc_native_x86_64 7s 9s -22%
poly_decompose_c 7s 8s -12%
polyveck_ntt 7s 9s -22%
polyvecl_ntt 7s 10s -30%
sign 7s 7s +0%
sign_keypair_internal 7s 8s -12%
sign_signature_pre_hash_shake256 7s 4s +75%
unpack_hints 7s 6s +17%
mld_h 6s 6s +0%
poly_invntt_tomont_c 6s 11s -45%
poly_invntt_tomont_native 6s 3s +100%
polyveck_pointwise_poly_montgomery 6s 10s -40%
polyveck_shiftl 6s 7s -14%
polyveck_sub 6s 6s +0%
polyveck_use_hint 6s 12s -50%
polyvecl_pointwise_acc_montgomery_native 6s 2s +200%
rej_eta_native 6s 5s +20%
shake128_finalize 6s 3s +100%
shake256_absorb 6s 4s +50%
shake256_finalize 6s 3s +100%
intt_native_x86_64 5s 3s +67%
keccakf1600_xor_bytes (big endian) 5s 2s +150%
poly_ntt_native 5s 2s +150%
poly_uniform_eta 5s 5s +0%
poly_use_hint 5s 3s +67%
polyt0_pack 5s 4s +25%
polyveck_chknorm 5s 6s -17%
polyveck_unpack_t0 5s 2s +150%
polyvecl_chknorm 5s 5s +0%
polyvecl_unpack_z 5s 4s +25%
rej_eta_c 5s 6s -17%
sign_signature 5s 4s +25%
sign_signature_pre_hash_internal 5s 4s +25%
sign_verify 5s 2s +150%
unpack_sig 5s 3s +67%
caddq 4s 4s +0%
mld_ct_cmask_neg_i32 4s 1s +300%
mld_ct_cmask_nonzero_u32 4s 2s +100%
ntt_native_x86_64 4s 2s +100%
pack_pk 4s 5s -20%
pack_sk 4s 3s +33%
poly_caddq_c 4s 5s -20%
poly_chknorm_native_aarch64 4s 3s +33%
poly_power2round 4s 6s -33%
poly_reduce 4s 3s +33%
poly_sub 4s 4s +0%
poly_uniform 4s 5s -20%
poly_uniform_gamma1_4x 4s 3s +33%
polyt1_pack 4s 3s +33%
polyveck_unpack_eta 4s 4s +0%
polyvecl_uniform_gamma1 4s 7s -43%
polyvecl_unpack_eta 4s 3s +33%
polyz_unpack_native 4s 3s +33%
shake256_release 4s 2s +100%
shake256x4_absorb_once 4s 2s +100%
sign_keypair 4s 6s -33%
sign_open 4s 3s +33%
sign_verify_extmu 4s 4s +0%
fqscale 3s 4s -25%
keccak_f1600_x1_native_aarch64_v84a 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 3s 2s +50%
keccakf1600x4_extract_bytes 3s 3s +0%
keccakf1600x4_permute 3s 2s +50%
keccakf1600x4_xor_bytes 3s 4s -25%
mld_ct_abs_i32 3s 4s -25%
mld_ct_get_optblocker_i64 3s 1s +200%
mld_ct_get_optblocker_u32 3s 4s -25%
mld_prepare_domain_separation_prefix 3s 5s -40%
mld_value_barrier_u8 3s 4s -25%
montgomery_reduce 3s 4s -25%
ntt_native_aarch64 3s 4s -25%
pack_sig_c 3s 4s -25%
pointwise_native_x86_64 3s 4s -25%
poly_caddq 3s 3s +0%
poly_challenge 3s 5s -40%
poly_invntt_tomont 3s 2s +50%
poly_ntt 3s 4s -25%
poly_ntt_c 3s 3s +0%
poly_shiftl 3s 1s +200%
poly_uniform_gamma1 3s 2s +50%
polyeta_pack 3s 3s +0%
polyt1_unpack 3s 4s -25%
polyveck_pack_eta 3s 4s -25%
polyveck_pack_t0 3s 2s +50%
polyvecl_permute_bitrev_to_custom 3s 3s +0%
polyvecl_uniform_gamma1_serial 3s 3s +0%
polyw1_pack 3s 2s +50%
polyz_pack 3s 3s +0%
polyz_unpack 3s 5s -40%
reduce32 3s 3s +0%
rej_eta 3s 4s -25%
shake128_release 3s 2s +50%
shake128x4_squeezeblocks 3s 2s +50%
shake256 3s 2s +50%
shake256_init 3s 1s +200%
sign_verify_pre_hash_internal 3s 6s -50%
sign_verify_pre_hash_shake256 3s 5s -40%
unpack_pk 3s 4s -25%
decompose 2s 3s -33%
keccak_f1600_x1_native_aarch64 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 3s -33%
keccak_init 2s 3s -33%
keccak_squeeze 2s 5s -60%
keccakf1600_xor_bytes 2s 4s -50%
make_hint 2s 3s -33%
mld_ct_get_optblocker_u8 2s 2s +0%
mld_ct_sel_int32 2s 2s +0%
mld_keccakf1600_extract_bytes 2s 3s -33%
mld_value_barrier_u32 2s 2s +0%
pack_sig_h_poly 2s 5s -60%
pack_sig_z 2s 5s -60%
poly_caddq_native 2s 4s -50%
poly_caddq_native_aarch64 2s 2s +0%
poly_chknorm 2s 3s -33%
poly_decompose 2s 3s -33%
poly_decompose_native 2s 4s -50%
poly_make_hint 2s 3s -33%
poly_pointwise_montgomery 2s 5s -60%
poly_pointwise_montgomery_native 2s 4s -50%
poly_use_hint_native 2s 4s -50%
polyvecl_pack_eta 2s 3s -33%
polyvecl_pointwise_acc_montgomery 2s 2s +0%
power2round 2s 2s +0%
shake128_init 2s 3s -33%
shake128_squeeze 2s 2s +0%
shake128x4_absorb_once 2s 4s -50%
shake256_squeeze 2s 2s +0%
sign_signature_extmu 2s 4s -50%
sys_check_capability 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 1s 3s -67%
keccak_finalize 1s 1s +0%
keccakf1600_extract_bytes (big endian) 1s 4s -75%
mld_value_barrier_i64 1s 2s -50%
pointwise_native_aarch64 1s 4s -75%
poly_chknorm_native 1s 2s -50%
poly_use_hint_c 1s 5s -80%
polyveck_pack_w1 1s 5s -80%
shake128_absorb 1s 3s -67%
shake256x4_squeezeblocks 1s 2s -50%
use_hint 1s 5s -80%

@mkannwischer mkannwischer merged commit 700907b into main Apr 15, 2026
396 checks passed
@mkannwischer mkannwischer deleted the cbmc69 branch April 15, 2026 06:41
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