Skip to content

CBMC: Use instrumented malloc/free for MLD_ALLOC/MLD_FREE#814

Draft
hanno-becker wants to merge 1 commit into
mainfrom
alloc_cbmc
Draft

CBMC: Use instrumented malloc/free for MLD_ALLOC/MLD_FREE#814
hanno-becker wants to merge 1 commit into
mainfrom
alloc_cbmc

Conversation

@hanno-becker
Copy link
Copy Markdown
Contributor

@hanno-becker hanno-becker commented Dec 24, 2025

The default implementation of MLD_ALLOC and MLD_FREE uses stack
allocation, which the compiler can assume not to fail. This means
that CBMC does not exercise the cleanup paths which handle fallible
dynamic allocation -- a significant proof gap.

This commit changes the configuration uses for the CBMC proofs
to use the (instrumented) calls to malloc/free for MLD_ALLOC/MLD_FREE.

Importantly, we set --malloc-may-fail to model allocation as fallible,
and --malloc-fail-null to return NULL in case of allocation failure.

@hanno-becker hanno-becker requested a review from a team as a code owner December 24, 2025 04:40
@hanno-becker hanno-becker force-pushed the alloc_cbmc branch 4 times, most recently from 20a9d4e to f03a619 Compare December 24, 2025 07:21
@mkannwischer mkannwischer self-assigned this Dec 28, 2025
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 @hanno-becker. The changes itself look good to me, but CBMC fails due to timeouts. Marking as draft until we can resolve that.

@mkannwischer mkannwischer marked this pull request as draft December 29, 2025 02:40
@hanno-becker hanno-becker force-pushed the alloc_cbmc branch 2 times, most recently from 428a719 to 9ad59c8 Compare January 2, 2026 04:46
The default implementation of MLD_ALLOC and MLD_FREE uses stack
allocation, which the compiler can assume not to fail. This means
that CBMC does not exercise the cleanup paths which handle fallible
dynamic allocation -- a significant proof gap.

This commit changes the configuration uses for the CBMC proofs
to use the (instrumented) calls to malloc/free for MLD_ALLOC/MLD_FREE.

Importantly, we set --malloc-may-fail to model allocation as fallible,
and --malloc-fail-null to return NULL in case of allocation failure.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 6, 2026

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 3675s 2446s +50.2%
mld_compute_pack_z - 9s -
sign_pk_from_sk - 27s -
mld_attempt_signature_generation ⚠️ 660s 71s +830%
sign_keypair_internal ⚠️ 164s 58s +183%
sign_signature_internal ⚠️ 107s 48s +123%
sign_verify_internal ⚠️ 887s 52s +1606%
Full Results (198 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 3675s 2446s +50.2%
sign_verify_internal ⚠️ 887s 52s +1606%
mld_attempt_signature_generation ⚠️ 660s 71s +830%
polyvecl_pointwise_acc_montgomery_c 295s 331s -11%
polyvec_matrix_expand 195s 228s -14%
sign_keypair_internal ⚠️ 164s 58s +183%
rej_uniform_native 115s 138s -17%
sign_signature_internal ⚠️ 107s 48s +123%
poly_pointwise_montgomery_c 95s 135s -30%
mld_invntt_layer 94s 118s -20%
mld_ct_memcmp 85s 106s -20%
polyvec_matrix_expand_serial 55s 64s -14%
mld_ntt_layer 42s 53s -21%
fqmul 31s 36s -14%
polyvec_matrix_pointwise_montgomery 26s 25s +4%
keccakf1600x4_permute_native 24s 23s +4%
mld_ntt_butterfly_block 16s 20s -20%
poly_chknorm_c 16s 20s -20%
polyvec_matrix_pointwise_montgomery_yvec 16s 19s -16%
rej_uniform 16s 20s -20%
rej_uniform_c 16s 24s -33%
polyt0_unpack 15s 20s -25%
poly_uniform_eta_4x 13s 16s -19%
polyveck_chknorm 13s 19s -32%
polyeta_unpack 12s 16s -25%
poly_add 11s 15s -27%
polyveck_decompose 11s 14s -21%
poly_uniform_4x 10s 12s -17%
polyveck_power2round 9s 9s +0%
keccak_absorb_once_x4 8s 10s -20%
keccakf1600_permute 8s 7s +14%
mld_check_pct 8s 16s -50%
poly_power2round 8s 10s -20%
polyt0_pack 8s 2s +300%
polyveck_caddq 8s 12s -33%
keccakf1600_permute_native 7s 6s +17%
mld_sample_s1_s2_serial 7s 7s +0%
pointwise_acc_native_aarch64 7s 8s -12%
pointwise_acc_native_x86_64 7s 7s +0%
poly_decompose_c 7s 9s -22%
poly_invntt_tomont_c 7s 11s -36%
poly_uniform_gamma1_4x 7s 3s +133%
polyveck_add 7s 9s -22%
polyveck_invntt_tomont 7s 8s -12%
polyz_unpack_c 7s 6s +17%
sign 7s 9s -22%
sign_keypair 7s 4s +75%
mld_h 6s 5s +20%
mld_prepare_domain_separation_prefix 6s 4s +50%
ntt_native_x86_64 6s 4s +50%
poly_use_hint 6s 5s +20%
poly_use_hint_c 6s 5s +20%
polyveck_reduce 6s 7s -14%
polyvecl_ntt 6s 7s -14%
polyvecl_pointwise_acc_montgomery_native 6s 3s +100%
polyvecl_unpack_eta 6s 4s +50%
sign_verify_pre_hash_internal 6s 4s +50%
sk_s2hat_get_poly 6s 4s +50%
unpack_sk 6s 3s +100%
caddq 5s 3s +67%
keccak_squeezeblocks_x4 5s 6s -17%
keccakf1600_extract_bytes (big endian) 5s 4s +25%
mld_sample_s1_s2 5s 7s -29%
pointwise_native_x86_64 5s 4s +25%
poly_caddq_native 5s 4s +25%
poly_caddq_native_aarch64 5s 3s +67%
poly_decompose 5s 4s +25%
poly_decompose_88_native_aarch64 5s 4s +25%
poly_decompose_native 5s 2s +150%
poly_invntt_tomont 5s 2s +150%
polyveck_ntt 5s 6s -17%
polyvecl_chknorm 5s 8s -38%
polyvecl_uniform_gamma1 5s 2s +150%
polyz_unpack_17_native_aarch64 5s 4s +25%
shake128_finalize 5s 3s +67%
sign_open 5s 6s -17%
sign_verify 5s 6s -17%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 4s 2s +100%
keccak_init 4s 4s +0%
keccakf1600x4_xor_bytes 4s 2s +100%
mld_keccakf1600_extract_bytes 4s 4s +0%
mld_polymat_expand_entry 4s 4s +0%
mld_value_barrier_i64 4s 4s +0%
mld_value_barrier_u8 4s 5s -20%
montgomery_reduce 4s 4s +0%
poly_caddq_c 4s 4s +0%
poly_challenge 4s 4s +0%
poly_make_hint 4s 3s +33%
poly_pointwise_montgomery_native 4s 3s +33%
poly_reduce 4s 3s +33%
poly_shiftl 4s 3s +33%
poly_sub 4s 3s +33%
poly_uniform 4s 6s -33%
polyveck_pack_eta 4s 2s +100%
polyveck_pack_w1 4s 2s +100%
polyveck_unpack_eta 4s 7s -43%
polyveck_unpack_t0 4s 3s +33%
polyz_unpack_19_native_aarch64 4s 10s -60%
rej_eta_c 4s 6s -33%
shake128x4_squeezeblocks 4s 3s +33%
sign_signature 4s 7s -43%
sign_signature_extmu 4s 4s +0%
sign_signature_pre_hash_shake256 4s 4s +0%
sk_s1hat_get_poly 4s 3s +33%
unpack_pk_t1 4s 5s -20%
decompose 3s 4s -25%
fqscale 3s 3s +0%
intt_native_x86_64 3s 3s +0%
keccak_absorb 3s 10s -70%
keccak_f1600_x1_native_aarch64 3s 3s +0%
keccak_f1600_x4_native_aarch64_v84a 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 2s +50%
keccak_f1600_x4_native_avx2 3s 2s +50%
keccak_squeeze 3s 2s +50%
keccakf1600_xor_bytes 3s 4s -25%
mld_ct_abs_i32 3s 3s +0%
mld_ct_cmask_nonzero_u8 3s 5s -40%
mld_ct_get_optblocker_i64 3s 3s +0%
mld_ct_sel_int32 3s 1s +200%
mld_value_barrier_u32 3s 3s +0%
ntt_native_aarch64 3s 5s -40%
nttunpack_native_x86_64 3s 4s -25%
pack_pk 3s 3s +0%
pack_sig_c 3s 3s +0%
pack_sig_h_poly 3s 4s -25%
pointwise_native_aarch64 3s 4s -25%
poly_chknorm_native_aarch64 3s 4s -25%
poly_decompose_32_native_aarch64 3s 3s +0%
poly_invntt_tomont_native 3s 5s -40%
poly_ntt_native 3s 4s -25%
poly_permute_bitrev_to_custom_optional_native 3s 3s +0%
poly_uniform_eta 3s 4s -25%
poly_uniform_gamma1 3s 4s -25%
poly_use_hint_native 3s 5s -40%
polyt1_unpack 3s 3s +0%
polyvec_matrix_pointwise_montgomery_row 3s 3s +0%
polyveck_pack_t0 3s 3s +0%
polyvecl_pack_eta 3s 2s +50%
polyvecl_pointwise_acc_montgomery 3s 5s -40%
polyvecl_uniform_gamma1_serial 3s 4s -25%
reduce32 3s 5s -40%
rej_eta_native 3s 4s -25%
shake128_absorb 3s 4s -25%
shake128_squeeze 3s 3s +0%
shake256_init 3s 4s -25%
shake256_release 3s 2s +50%
shake256x4_absorb_once 3s 3s +0%
shake256x4_squeezeblocks 3s 4s -25%
sig_unpack_hints 3s 5s -40%
sign_signature_pre_hash_internal 3s 7s -57%
sign_verify_extmu 3s 4s -25%
sign_verify_pre_hash_shake256 3s 4s -25%
unpack_sk_t0hat 3s 2s +50%
use_hint 3s 3s +0%
yvec_get_poly 3s 3s +0%
yvec_init 3s 3s +0%
keccak_finalize 2s 4s -50%
keccakf1600_xor_bytes (big endian) 2s 1s +100%
keccakf1600x4_extract_bytes 2s 3s -33%
make_hint 2s 2s +0%
mld_ct_cmask_neg_i32 2s 4s -50%
mld_ct_cmask_nonzero_u32 2s 1s +100%
mld_ct_get_optblocker_u8 2s 1s +100%
pack_sig_z 2s 6s -67%
pack_sk_s1 2s 4s -50%
poly_caddq 2s 5s -60%
poly_chknorm 2s 3s -33%
poly_chknorm_native 2s 3s -33%
poly_ntt 2s 3s -33%
poly_ntt_c 2s 3s -33%
poly_permute_bitrev_to_custom_optional 2s 6s -67%
poly_pointwise_montgomery 2s 2s +0%
polyt1_pack 2s 4s -50%
polyw1_pack 2s 4s -50%
polyz_unpack 2s 1s +100%
polyz_unpack_native 2s 5s -60%
power2round 2s 2s +0%
rej_eta 2s 3s -33%
shake128_init 2s 3s -33%
shake256 2s 2s +0%
shake256_finalize 2s 4s -50%
unpack_sk_s1hat 2s 3s -33%
mld_compute_pack_z - 9s -
sign_pk_from_sk - 27s -
keccak_f1600_x1_native_aarch64_v84a 1s 3s -67%
keccakf1600x4_permute 1s 2s -50%
mld_ct_get_optblocker_u32 1s 2s -50%
pack_sk_rho_key_tr_s2_t0 1s 5s -80%
poly_use_hint_native_aarch64 1s 2s -50%
polyeta_pack 1s 4s -75%
polyvecl_unpack_z 1s 3s -67%
polyz_pack 1s 2s -50%
shake128_release 1s 4s -75%
shake128x4_absorb_once 1s 3s -67%
shake256_absorb 1s 2s -50%
shake256_squeeze 1s 2s -50%
sk_t0hat_get_poly 1s 1s +0%
sys_check_capability 1s 2s -50%
unpack_sk_s2hat 1s 4s -75%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 6, 2026

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 3781s 2220s +70.3%
mld_compute_pack_z - 7s -
sign_pk_from_sk - 23s -
mld_attempt_signature_generation ⚠️ 727s 50s +1354%
sign_keypair_internal ⚠️ 130s 33s +294%
sign_signature_internal ⚠️ 125s 29s +331%
sign_verify_internal ⚠️ 834s 60s +1290%
Full Results (198 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 3781s 2220s +70.3%
sign_verify_internal ⚠️ 834s 60s +1290%
mld_attempt_signature_generation ⚠️ 727s 50s +1354%
polyvecl_pointwise_acc_montgomery_c 472s 508s -7%
sign_keypair_internal ⚠️ 130s 33s +294%
polyvec_matrix_expand 128s 138s -7%
sign_signature_internal ⚠️ 125s 29s +331%
rej_uniform_native 121s 133s -9%
poly_pointwise_montgomery_c 99s 108s -8%
mld_invntt_layer 97s 100s -3%
mld_ct_memcmp 92s 85s +8%
mld_ntt_layer 43s 43s +0%
polyvec_matrix_pointwise_montgomery 35s 35s +0%
fqmul 26s 30s -13%
keccakf1600x4_permute_native 22s 25s -12%
polyvec_matrix_expand_serial 22s 22s +0%
polyveck_power2round 19s 19s +0%
mld_ntt_butterfly_block 17s 16s +6%
poly_add 16s 11s +45%
polyt0_unpack 16s 16s +0%
polyvec_matrix_pointwise_montgomery_yvec 16s 18s -11%
rej_uniform 16s 18s -11%
poly_chknorm_c 15s 14s +7%
rej_uniform_c 15s 18s -17%
polyveck_decompose 13s 11s +18%
poly_power2round 11s 8s +38%
poly_uniform_eta_4x 11s 11s +0%
polyveck_add 11s 10s +10%
polyvecl_chknorm 11s 8s +38%
mld_check_pct 10s 18s -44%
poly_uniform_4x 10s 11s -9%
sign 10s 8s +25%
keccakf1600_permute 9s 5s +80%
pointwise_acc_native_aarch64 9s 5s +80%
pointwise_acc_native_x86_64 9s 6s +50%
poly_invntt_tomont_c 9s 9s +0%
polyvecl_ntt 9s 7s +29%
mld_sample_s1_s2_serial 8s 3s +167%
polyveck_chknorm 8s 9s -11%
sign_keypair 8s 6s +33%
keccak_absorb_once_x4 7s 10s -30%
keccak_squeezeblocks_x4 7s 5s +40%
polyveck_invntt_tomont 7s 8s -12%
polyveck_ntt 7s 9s -22%
keccakf1600_permute_native 6s 6s +0%
mld_keccakf1600_extract_bytes 6s 3s +100%
poly_caddq_native_aarch64 6s 4s +50%
poly_ntt 6s 2s +200%
polyveck_reduce 6s 6s +0%
sign_signature_pre_hash_internal 6s 3s +100%
intt_native_x86_64 5s 2s +150%
make_hint 5s 3s +67%
mld_prepare_domain_separation_prefix 5s 3s +67%
mld_sample_s1_s2 5s 4s +25%
pack_pk 5s 2s +150%
pointwise_native_x86_64 5s 2s +150%
poly_reduce 5s 3s +67%
poly_shiftl 5s 5s +0%
poly_uniform 5s 5s +0%
poly_uniform_eta 5s 4s +25%
poly_uniform_gamma1 5s 4s +25%
poly_use_hint 5s 3s +67%
poly_use_hint_c 5s 4s +25%
poly_use_hint_native 5s 3s +67%
polyvecl_unpack_eta 5s 4s +25%
polyz_unpack_c 5s 6s -17%
shake256x4_squeezeblocks 5s 3s +67%
sign_signature 5s 3s +67%
sign_signature_pre_hash_shake256 5s 7s -29%
sign_verify_pre_hash_internal 5s 4s +25%
sk_t0hat_get_poly 5s 5s +0%
yvec_get_poly 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 4s 2s +100%
mld_ct_cmask_nonzero_u8 4s 3s +33%
mld_ct_get_optblocker_u8 4s 2s +100%
mld_polymat_expand_entry 4s 4s +0%
montgomery_reduce 4s 4s +0%
ntt_native_x86_64 4s 4s +0%
pack_sig_c 4s 3s +33%
pack_sk_s1 4s 4s +0%
poly_challenge 4s 5s -20%
poly_chknorm 4s 3s +33%
poly_chknorm_native_aarch64 4s 2s +100%
poly_decompose_88_native_aarch64 4s 3s +33%
poly_decompose_native 4s 3s +33%
poly_pointwise_montgomery_native 4s 3s +33%
polyeta_pack 4s 2s +100%
polyeta_unpack 4s 4s +0%
polyt1_unpack 4s 1s +300%
polyveck_caddq 4s 7s -43%
polyveck_pack_eta 4s 2s +100%
polyvecl_uniform_gamma1_serial 4s 3s +33%
polyz_pack 4s 5s -20%
sig_unpack_hints 4s 2s +100%
sign_open 4s 4s +0%
sign_signature_extmu 4s 5s -20%
sign_verify_extmu 4s 3s +33%
sign_verify_pre_hash_shake256 4s 4s +0%
sk_s1hat_get_poly 4s 4s +0%
sys_check_capability 4s 3s +33%
unpack_sk 4s 3s +33%
unpack_sk_s2hat 4s 4s +0%
decompose 3s 3s +0%
fqscale 3s 2s +50%
keccak_absorb 3s 8s -62%
keccak_f1600_x1_native_aarch64 3s 4s -25%
keccak_f1600_x1_native_aarch64_v84a 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 2s +50%
keccak_finalize 3s 4s -25%
keccak_squeeze 3s 3s +0%
keccakf1600_xor_bytes 3s 3s +0%
keccakf1600x4_extract_bytes 3s 4s -25%
keccakf1600x4_xor_bytes 3s 3s +0%
mld_ct_get_optblocker_i64 3s 6s -50%
mld_ct_sel_int32 3s 2s +50%
mld_value_barrier_u8 3s 2s +50%
ntt_native_aarch64 3s 2s +50%
pack_sig_z 3s 2s +50%
poly_caddq_native 3s 3s +0%
poly_chknorm_native 3s 3s +0%
poly_decompose_32_native_aarch64 3s 5s -40%
poly_invntt_tomont 3s 2s +50%
poly_invntt_tomont_native 3s 2s +50%
poly_make_hint 3s 3s +0%
poly_ntt_native 3s 3s +0%
poly_permute_bitrev_to_custom_optional 3s 4s -25%
poly_pointwise_montgomery 3s 3s +0%
poly_uniform_gamma1_4x 3s 3s +0%
poly_use_hint_native_aarch64 3s 3s +0%
polyt0_pack 3s 4s -25%
polyvec_matrix_pointwise_montgomery_row 3s 3s +0%
polyveck_pack_w1 3s 5s -40%
polyveck_unpack_eta 3s 3s +0%
polyvecl_pointwise_acc_montgomery 3s 3s +0%
polyvecl_uniform_gamma1 3s 3s +0%
polyvecl_unpack_z 3s 3s +0%
polyz_unpack_17_native_aarch64 3s 2s +50%
polyz_unpack_19_native_aarch64 3s 3s +0%
polyz_unpack_native 3s 2s +50%
rej_eta_native 3s 5s -40%
shake128_init 3s 3s +0%
shake128_release 3s 4s -25%
shake128_squeeze 3s 3s +0%
shake256_squeeze 3s 2s +50%
sign_verify 3s 3s +0%
sk_s2hat_get_poly 3s 2s +50%
unpack_pk_t1 3s 4s -25%
unpack_sk_t0hat 3s 4s -25%
use_hint 3s 3s +0%
yvec_init 3s 3s +0%
caddq 2s 2s +0%
keccak_f1600_x4_native_avx2 2s 4s -50%
keccak_init 2s 2s +0%
keccakf1600_extract_bytes (big endian) 2s 2s +0%
keccakf1600_xor_bytes (big endian) 2s 4s -50%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_cmask_nonzero_u32 2s 2s +0%
mld_ct_get_optblocker_u32 2s 2s +0%
mld_h 2s 5s -60%
mld_value_barrier_u32 2s 1s +100%
nttunpack_native_x86_64 2s 4s -50%
pointwise_native_aarch64 2s 3s -33%
poly_caddq 2s 3s -33%
poly_caddq_c 2s 7s -71%
poly_decompose 2s 3s -33%
poly_decompose_c 2s 2s +0%
poly_ntt_c 2s 4s -50%
poly_permute_bitrev_to_custom_optional_native 2s 3s -33%
poly_sub 2s 5s -60%
polyt1_pack 2s 3s -33%
polyveck_pack_t0 2s 3s -33%
polyveck_unpack_t0 2s 4s -50%
polyvecl_pack_eta 2s 2s +0%
polyvecl_pointwise_acc_montgomery_native 2s 3s -33%
polyz_unpack 2s 2s +0%
reduce32 2s 1s +100%
rej_eta 2s 2s +0%
rej_eta_c 2s 2s +0%
shake128_absorb 2s 4s -50%
shake128_finalize 2s 3s -33%
shake128x4_absorb_once 2s 3s -33%
shake256 2s 3s -33%
shake256_absorb 2s 2s +0%
shake256_init 2s 4s -50%
shake256_release 2s 3s -33%
shake256x4_absorb_once 2s 2s +0%
unpack_sk_s1hat 2s 2s +0%
mld_compute_pack_z - 7s -
sign_pk_from_sk - 23s -
keccak_f1600_x4_native_aarch64_v84a 1s 2s -50%
keccakf1600x4_permute 1s 4s -75%
mld_ct_abs_i32 1s 1s +0%
mld_value_barrier_i64 1s 2s -50%
pack_sig_h_poly 1s 3s -67%
pack_sk_rho_key_tr_s2_t0 1s 2s -50%
polyw1_pack 1s 3s -67%
power2round 1s 3s -67%
shake128x4_squeezeblocks 1s 2s -50%
shake256_finalize 1s 3s -67%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 6, 2026

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

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 3963s 1480s +167.8%
mld_compute_pack_z - 5s -
sign_pk_from_sk - 11s -
mld_attempt_signature_generation ⚠️ 377s 26s +1350%
sign_keypair_internal ⚠️ 142s 30s +373%
sign_signature_internal ⚠️ 1260s 8s +15650%
sign_verify_internal ⚠️ 708s 21s +3271%
Full Results (198 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 3963s 1480s +167.8%
sign_signature_internal ⚠️ 1260s 8s +15650%
sign_verify_internal ⚠️ 708s 21s +3271%
mld_attempt_signature_generation ⚠️ 377s 26s +1350%
poly_pointwise_montgomery_c 197s 158s +25%
sign_keypair_internal ⚠️ 142s 30s +373%
rej_uniform_native 116s 106s +9%
mld_invntt_layer 110s 95s +16%
polyvec_matrix_pointwise_montgomery_yvec 93s 82s +13%
mld_ct_memcmp 90s 71s +27%
mld_ntt_layer 43s 41s +5%
fqmul 29s 27s +7%
keccakf1600x4_permute_native 22s 20s +10%
polyeta_unpack 19s 19s +0%
mld_ntt_butterfly_block 16s 14s +14%
poly_uniform_eta_4x 16s 14s +14%
poly_add 14s 11s +27%
poly_chknorm_c 14s 13s +8%
polyveck_decompose 14s 15s -7%
polyt0_unpack 12s 11s +9%
polyveck_add 12s 11s +9%
rej_uniform 11s 19s -42%
rej_uniform_c 11s 19s -42%
polyveck_invntt_tomont 10s 6s +67%
polyveck_power2round 10s 10s +0%
keccak_absorb_once_x4 9s 10s -10%
keccakf1600_permute_native 9s 9s +0%
polyvec_matrix_pointwise_montgomery_row 9s 9s +0%
keccakf1600_permute 8s 6s +33%
poly_caddq_c 8s 9s -11%
poly_invntt_tomont_c 8s 8s +0%
poly_power2round 8s 6s +33%
polyveck_chknorm 8s 7s +14%
sign_keypair 8s 4s +100%
mld_sample_s1_s2_serial 7s 7s +0%
pointwise_acc_native_aarch64 7s 8s -12%
pointwise_acc_native_x86_64 7s 9s -22%
poly_use_hint_c 7s 5s +40%
polyveck_caddq 7s 5s +40%
polyvecl_ntt 7s 8s -12%
keccak_squeezeblocks_x4 6s 4s +50%
mld_check_pct 6s 13s -54%
mld_sample_s1_s2 6s 5s +20%
poly_make_hint 6s 3s +100%
poly_pointwise_montgomery 6s 4s +50%
polyt1_unpack 6s 3s +100%
polyvec_matrix_pointwise_montgomery 6s 4s +50%
sign 6s 8s -25%
keccak_squeeze 5s 6s -17%
mld_polymat_expand_entry 5s 2s +150%
ntt_native_x86_64 5s 2s +150%
poly_decompose 5s 3s +67%
poly_reduce 5s 4s +25%
poly_shiftl 5s 6s -17%
poly_uniform_gamma1 5s 3s +67%
poly_use_hint_native 5s 3s +67%
polyvecl_chknorm 5s 3s +67%
polyvecl_unpack_eta 5s 3s +67%
polyz_unpack_c 5s 4s +25%
rej_eta_native 5s 2s +150%
sign_signature 5s 3s +67%
sign_signature_extmu 5s 4s +25%
sk_s2hat_get_poly 5s 3s +67%
yvec_get_poly 5s 2s +150%
caddq 4s 4s +0%
fqscale 4s 3s +33%
intt_native_x86_64 4s 1s +300%
mld_ct_cmask_nonzero_u32 4s 3s +33%
mld_h 4s 4s +0%
montgomery_reduce 4s 4s +0%
ntt_native_aarch64 4s 4s +0%
pack_sk_s1 4s 1s +300%
pointwise_native_aarch64 4s 3s +33%
poly_caddq 4s 4s +0%
poly_caddq_native 4s 4s +0%
poly_chknorm_native 4s 6s -33%
poly_decompose_88_native_aarch64 4s 1s +300%
poly_decompose_c 4s 5s -20%
poly_decompose_native 4s 3s +33%
poly_invntt_tomont_native 4s 3s +33%
poly_sub 4s 4s +0%
polyvec_matrix_expand 4s 3s +33%
polyveck_pack_t0 4s 2s +100%
polyveck_reduce 4s 8s -50%
polyveck_unpack_eta 4s 3s +33%
polyvecl_uniform_gamma1_serial 4s 3s +33%
polyz_unpack 4s 3s +33%
polyz_unpack_17_native_aarch64 4s 2s +100%
polyz_unpack_19_native_aarch64 4s 4s +0%
polyz_unpack_native 4s 5s -20%
power2round 4s 4s +0%
rej_eta_c 4s 5s -20%
shake128_finalize 4s 4s +0%
sig_unpack_hints 4s 5s -20%
sign_open 4s 4s +0%
sign_signature_pre_hash_internal 4s 5s -20%
sign_verify_extmu 4s 2s +100%
sign_verify_pre_hash_shake256 4s 5s -20%
unpack_pk_t1 4s 3s +33%
unpack_sk 4s 4s +0%
keccak_absorb 3s 6s -50%
keccak_f1600_x4_native_avx2 3s 2s +50%
keccak_init 3s 4s -25%
keccakf1600_xor_bytes 3s 3s +0%
keccakf1600x4_permute 3s 2s +50%
mld_ct_abs_i32 3s 2s +50%
mld_ct_cmask_neg_i32 3s 1s +200%
mld_prepare_domain_separation_prefix 3s 4s -25%
mld_value_barrier_i64 3s 2s +50%
mld_value_barrier_u32 3s 2s +50%
nttunpack_native_x86_64 3s 2s +50%
pack_sig_h_poly 3s 3s +0%
pack_sig_z 3s 3s +0%
pack_sk_rho_key_tr_s2_t0 3s 2s +50%
pointwise_native_x86_64 3s 3s +0%
poly_challenge 3s 4s -25%
poly_chknorm 3s 4s -25%
poly_chknorm_native_aarch64 3s 3s +0%
poly_invntt_tomont 3s 2s +50%
poly_ntt_c 3s 3s +0%
poly_ntt_native 3s 3s +0%
poly_permute_bitrev_to_custom_optional_native 3s 3s +0%
poly_uniform 3s 4s -25%
poly_uniform_4x 3s 2s +50%
poly_uniform_eta 3s 3s +0%
poly_use_hint_native_aarch64 3s 2s +50%
polyt0_pack 3s 3s +0%
polyt1_pack 3s 3s +0%
polyvec_matrix_expand_serial 3s 5s -40%
polyveck_ntt 3s 4s -25%
polyvecl_pointwise_acc_montgomery_native 3s 4s -25%
polyvecl_uniform_gamma1 3s 5s -40%
polyvecl_unpack_z 3s 2s +50%
polyw1_pack 3s 3s +0%
polyz_pack 3s 2s +50%
shake128_squeeze 3s 3s +0%
shake128x4_squeezeblocks 3s 1s +200%
shake256_absorb 3s 3s +0%
shake256x4_absorb_once 3s 4s -25%
shake256x4_squeezeblocks 3s 2s +50%
sign_signature_pre_hash_shake256 3s 7s -57%
sys_check_capability 3s 4s -25%
unpack_sk_s1hat 3s 4s -25%
unpack_sk_s2hat 3s 2s +50%
unpack_sk_t0hat 3s 2s +50%
decompose 2s 4s -50%
keccak_f1600_x1_native_aarch64_v84a 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 2s 5s -60%
keccak_finalize 2s 2s +0%
keccakf1600_xor_bytes (big endian) 2s 1s +100%
keccakf1600x4_extract_bytes 2s 3s -33%
keccakf1600x4_xor_bytes 2s 2s +0%
make_hint 2s 5s -60%
mld_ct_get_optblocker_i64 2s 1s +100%
mld_ct_get_optblocker_u32 2s 1s +100%
mld_ct_sel_int32 2s 4s -50%
mld_value_barrier_u8 2s 2s +0%
poly_caddq_native_aarch64 2s 2s +0%
poly_decompose_32_native_aarch64 2s 4s -50%
poly_permute_bitrev_to_custom_optional 2s 3s -33%
poly_pointwise_montgomery_native 2s 5s -60%
poly_uniform_gamma1_4x 2s 3s -33%
poly_use_hint 2s 2s +0%
polyeta_pack 2s 2s +0%
polyveck_pack_eta 2s 4s -50%
polyveck_pack_w1 2s 1s +100%
polyveck_unpack_t0 2s 3s -33%
polyvecl_pack_eta 2s 1s +100%
polyvecl_pointwise_acc_montgomery 2s 2s +0%
polyvecl_pointwise_acc_montgomery_c 2s 4s -50%
reduce32 2s 3s -33%
shake128_absorb 2s 3s -33%
shake128_release 2s 4s -50%
shake128x4_absorb_once 2s 2s +0%
shake256 2s 5s -60%
shake256_finalize 2s 1s +100%
shake256_init 2s 4s -50%
shake256_release 2s 2s +0%
shake256_squeeze 2s 3s -33%
sign_verify 2s 4s -50%
sign_verify_pre_hash_internal 2s 3s -33%
sk_s1hat_get_poly 2s 3s -33%
sk_t0hat_get_poly 2s 2s +0%
use_hint 2s 4s -50%
yvec_init 2s 2s +0%
mld_compute_pack_z - 5s -
sign_pk_from_sk - 11s -
keccak_f1600_x1_native_aarch64 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a 1s 1s +0%
keccakf1600_extract_bytes (big endian) 1s 1s +0%
mld_ct_cmask_nonzero_u8 1s 3s -67%
mld_ct_get_optblocker_u8 1s 1s +0%
mld_keccakf1600_extract_bytes 1s 4s -75%
pack_pk 1s 2s -50%
pack_sig_c 1s 3s -67%
poly_ntt 1s 3s -67%
rej_eta 1s 3s -67%
shake128_init 1s 3s -67%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 6, 2026

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

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 3689s 1602s +130.3%
mld_compute_pack_z - 7s -
sign_pk_from_sk - 18s -
mld_attempt_signature_generation ⚠️ 512s 31s +1552%
sign_keypair_internal ⚠️ 112s 22s +409%
sign_signature_internal ⚠️ 927s 8s +11488%
sign_verify_internal ⚠️ 695s 36s +1831%
Full Results (198 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 3689s 1602s +130.3%
sign_signature_internal ⚠️ 927s 8s +11488%
sign_verify_internal ⚠️ 695s 36s +1831%
mld_attempt_signature_generation ⚠️ 512s 31s +1552%
poly_pointwise_montgomery_c 177s 186s -5%
rej_uniform_native 112s 109s +3%
sign_keypair_internal ⚠️ 112s 22s +409%
mld_invntt_layer 110s 109s +1%
mld_ct_memcmp 84s 79s +6%
polyvec_matrix_pointwise_montgomery_yvec 65s 64s +2%
mld_ntt_layer 44s 43s +2%
polyveck_chknorm 35s 40s -12%
fqmul 27s 31s -13%
keccakf1600x4_permute_native 24s 21s +14%
polyveck_invntt_tomont 20s 18s +11%
polyveck_decompose 17s 16s +6%
mld_ntt_butterfly_block 15s 17s -12%
poly_chknorm_c 14s 13s +8%
rej_uniform_c 13s 20s -35%
poly_uniform_eta_4x 12s 12s +0%
polyveck_add 12s 8s +50%
poly_add 11s 11s +0%
polyt0_unpack 11s 13s -15%
polyveck_power2round 11s 12s -8%
poly_invntt_tomont_c 10s 9s +11%
sign_keypair 10s 5s +100%
keccakf1600_permute 9s 7s +29%
polyveck_caddq 9s 12s -25%
rej_uniform 9s 20s -55%
sign 9s 6s +50%
poly_caddq_c 8s 7s +14%
poly_power2round 8s 9s -11%
polyveck_reduce 8s 5s +60%
keccak_absorb_once_x4 7s 12s -42%
rej_eta_c 7s 4s +75%
keccakf1600_permute_native 6s 8s -25%
pack_sig_z 6s 4s +50%
pointwise_acc_native_aarch64 6s 6s +0%
pointwise_acc_native_x86_64 6s 9s -33%
poly_caddq_native_aarch64 6s 2s +200%
polyvecl_ntt 6s 7s -14%
keccak_absorb 5s 5s +0%
keccak_squeezeblocks_x4 5s 4s +25%
keccakf1600x4_permute 5s 3s +67%
mld_check_pct 5s 16s -69%
mld_ct_cmask_nonzero_u8 5s 3s +67%
mld_polymat_expand_entry 5s 3s +67%
mld_sample_s1_s2 5s 3s +67%
mld_value_barrier_i64 5s 2s +150%
pointwise_native_aarch64 5s 2s +150%
poly_challenge 5s 4s +25%
poly_decompose_c 5s 4s +25%
poly_ntt_native 5s 3s +67%
poly_permute_bitrev_to_custom_optional 5s 6s -17%
poly_permute_bitrev_to_custom_optional_native 5s 4s +25%
poly_pointwise_montgomery 5s 3s +67%
poly_shiftl 5s 7s -29%
poly_uniform_gamma1 5s 2s +150%
polyvec_matrix_pointwise_montgomery 5s 4s +25%
polyveck_unpack_t0 5s 5s +0%
polyvecl_chknorm 5s 4s +25%
polyvecl_pointwise_acc_montgomery 5s 5s +0%
polyz_unpack_c 5s 4s +25%
shake128_init 5s 2s +150%
sign_signature 5s 2s +150%
sys_check_capability 5s 3s +67%
caddq 4s 3s +33%
decompose 4s 3s +33%
fqscale 4s 3s +33%
make_hint 4s 4s +0%
mld_ct_sel_int32 4s 1s +300%
mld_prepare_domain_separation_prefix 4s 2s +100%
mld_value_barrier_u32 4s 3s +33%
ntt_native_x86_64 4s 2s +100%
pack_sig_c 4s 2s +100%
pack_sk_s1 4s 5s -20%
poly_make_hint 4s 2s +100%
poly_ntt 4s 3s +33%
poly_uniform_eta 4s 3s +33%
poly_uniform_gamma1_4x 4s 3s +33%
poly_use_hint_c 4s 4s +0%
polyt0_pack 4s 1s +300%
polyvec_matrix_pointwise_montgomery_row 4s 10s -60%
polyveck_pack_t0 4s 3s +33%
polyveck_pack_w1 4s 3s +33%
polyvecl_pointwise_acc_montgomery_c 4s 6s -33%
polyvecl_uniform_gamma1_serial 4s 4s +0%
power2round 4s 4s +0%
shake128_finalize 4s 4s +0%
shake256_finalize 4s 6s -33%
sign_open 4s 3s +33%
sign_signature_extmu 4s 3s +33%
sign_signature_pre_hash_internal 4s 4s +0%
sign_verify 4s 4s +0%
sign_verify_extmu 4s 4s +0%
sign_verify_pre_hash_shake256 4s 5s -20%
unpack_sk_s1hat 4s 3s +33%
use_hint 4s 3s +33%
yvec_get_poly 4s 4s +0%
intt_native_x86_64 3s 3s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 1s +200%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 3s 2s +50%
keccakf1600x4_extract_bytes 3s 4s -25%
keccakf1600x4_xor_bytes 3s 3s +0%
mld_ct_cmask_nonzero_u32 3s 3s +0%
mld_ct_get_optblocker_i64 3s 2s +50%
mld_ct_get_optblocker_u32 3s 1s +200%
mld_ct_get_optblocker_u8 3s 4s -25%
mld_h 3s 5s -40%
mld_keccakf1600_extract_bytes 3s 3s +0%
mld_sample_s1_s2_serial 3s 3s +0%
mld_value_barrier_u8 3s 4s -25%
montgomery_reduce 3s 2s +50%
ntt_native_aarch64 3s 3s +0%
nttunpack_native_x86_64 3s 2s +50%
pack_sig_h_poly 3s 2s +50%
pack_sk_rho_key_tr_s2_t0 3s 3s +0%
poly_caddq 3s 3s +0%
poly_caddq_native 3s 4s -25%
poly_chknorm_native 3s 3s +0%
poly_decompose_32_native_aarch64 3s 3s +0%
poly_decompose_88_native_aarch64 3s 5s -40%
poly_invntt_tomont_native 3s 3s +0%
poly_ntt_c 3s 3s +0%
poly_pointwise_montgomery_native 3s 4s -25%
poly_reduce 3s 4s -25%
poly_sub 3s 4s -25%
poly_uniform 3s 4s -25%
poly_uniform_4x 3s 4s -25%
poly_use_hint 3s 7s -57%
poly_use_hint_native 3s 2s +50%
poly_use_hint_native_aarch64 3s 3s +0%
polyeta_unpack 3s 3s +0%
polyt1_pack 3s 3s +0%
polyt1_unpack 3s 3s +0%
polyveck_ntt 3s 3s +0%
polyveck_pack_eta 3s 1s +200%
polyvecl_uniform_gamma1 3s 4s -25%
polyvecl_unpack_eta 3s 4s -25%
polyw1_pack 3s 4s -25%
polyz_pack 3s 4s -25%
polyz_unpack_17_native_aarch64 3s 3s +0%
reduce32 3s 5s -40%
shake128x4_absorb_once 3s 4s -25%
shake256_absorb 3s 2s +50%
shake256_squeeze 3s 4s -25%
shake256x4_squeezeblocks 3s 2s +50%
sign_verify_pre_hash_internal 3s 5s -40%
yvec_init 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a 2s 2s +0%
keccak_f1600_x4_native_avx2 2s 1s +100%
keccak_finalize 2s 3s -33%
keccak_init 2s 3s -33%
keccak_squeeze 2s 4s -50%
keccakf1600_extract_bytes (big endian) 2s 2s +0%
keccakf1600_xor_bytes 2s 3s -33%
keccakf1600_xor_bytes (big endian) 2s 4s -50%
mld_ct_cmask_neg_i32 2s 3s -33%
pack_pk 2s 3s -33%
pointwise_native_x86_64 2s 4s -50%
poly_chknorm 2s 4s -50%
poly_chknorm_native_aarch64 2s 3s -33%
poly_decompose 2s 4s -50%
poly_decompose_native 2s 5s -60%
poly_invntt_tomont 2s 2s +0%
polyeta_pack 2s 2s +0%
polyvec_matrix_expand 2s 2s +0%
polyvec_matrix_expand_serial 2s 2s +0%
polyveck_unpack_eta 2s 2s +0%
polyvecl_pack_eta 2s 3s -33%
polyvecl_unpack_z 2s 3s -33%
polyz_unpack 2s 2s +0%
polyz_unpack_19_native_aarch64 2s 2s +0%
polyz_unpack_native 2s 4s -50%
rej_eta 2s 2s +0%
rej_eta_native 2s 5s -60%
shake128_absorb 2s 3s -33%
shake128_release 2s 4s -50%
shake128_squeeze 2s 2s +0%
shake128x4_squeezeblocks 2s 2s +0%
shake256 2s 3s -33%
shake256_init 2s 3s -33%
shake256_release 2s 1s +100%
sig_unpack_hints 2s 3s -33%
sign_signature_pre_hash_shake256 2s 3s -33%
sk_s1hat_get_poly 2s 3s -33%
sk_s2hat_get_poly 2s 7s -71%
sk_t0hat_get_poly 2s 4s -50%
unpack_pk_t1 2s 5s -60%
unpack_sk 2s 3s -33%
unpack_sk_s2hat 2s 3s -33%
unpack_sk_t0hat 2s 3s -33%
mld_compute_pack_z - 7s -
sign_pk_from_sk - 18s -
keccak_f1600_x1_native_aarch64 1s 4s -75%
mld_ct_abs_i32 1s 1s +0%
polyvecl_pointwise_acc_montgomery_native 1s 2s -50%
shake256x4_absorb_once 1s 4s -75%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 6, 2026

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 4078s 1724s +136.5%
mld_compute_pack_z - 7s -
sign_pk_from_sk - 20s -
mld_attempt_signature_generation ⚠️ 903s 58s +1457%
sign_keypair_internal ⚠️ 495s 27s +1733%
sign_signature_internal ⚠️ 83s 22s +277%
sign_verify_internal ⚠️ 867s 40s +2068%
Full Results (198 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 4078s 1724s +136.5%
mld_attempt_signature_generation ⚠️ 903s 58s +1457%
sign_verify_internal ⚠️ 867s 40s +2068%
sign_keypair_internal ⚠️ 495s 27s +1733%
polyvecl_pointwise_acc_montgomery_c 278s 226s +23%
rej_uniform_native 134s 124s +8%
poly_pointwise_montgomery_c 114s 92s +24%
mld_invntt_layer 105s 95s +11%
mld_ct_memcmp 101s 78s +29%
sign_signature_internal ⚠️ 83s 22s +277%
mld_ntt_layer 49s 44s +11%
fqmul 31s 29s +7%
polyvec_matrix_pointwise_montgomery_yvec 26s 26s +0%
keccakf1600x4_permute_native 24s 23s +4%
polyvec_matrix_expand 21s 22s -5%
polyvec_matrix_pointwise_montgomery 18s 17s +6%
rej_uniform 18s 17s +6%
poly_chknorm_c 17s 17s +0%
rej_uniform_c 17s 21s -19%
mld_ntt_butterfly_block 16s 16s +0%
polyt0_unpack 16s 15s +7%
poly_uniform_eta_4x 15s 14s +7%
poly_uniform_4x 14s 12s +17%
polyeta_unpack 14s 14s +0%
poly_add 13s 13s +0%
polyz_unpack_c 13s 15s -13%
keccakf1600_permute_native 10s 6s +67%
polyvec_matrix_expand_serial 10s 7s +43%
polyveck_add 10s 8s +25%
sign 10s 7s +43%
keccak_absorb_once_x4 8s 12s -33%
keccakf1600_permute 8s 8s +0%
poly_power2round 8s 9s -11%
polyt0_pack 8s 3s +167%
polyvecl_chknorm 8s 6s +33%
sign_keypair 8s 3s +167%
poly_challenge 7s 8s -12%
poly_invntt_tomont_c 7s 9s -22%
polyveck_decompose 7s 9s -22%
sign_open 7s 8s -12%
sign_signature_pre_hash_shake256 7s 5s +40%
keccak_squeezeblocks_x4 6s 4s +50%
keccakf1600_extract_bytes (big endian) 6s 1s +500%
mld_check_pct 6s 14s -57%
mld_h 6s 2s +200%
pointwise_acc_native_x86_64 6s 6s +0%
poly_caddq 6s 2s +200%
poly_chknorm_native 6s 4s +50%
poly_decompose_c 6s 5s +20%
poly_uniform 6s 5s +20%
polyveck_invntt_tomont 6s 3s +100%
polyveck_pack_eta 6s 2s +200%
polyveck_pack_t0 6s 4s +50%
polyveck_power2round 6s 5s +20%
polyvecl_ntt 6s 4s +50%
polyvecl_pack_eta 6s 3s +100%
shake256x4_squeezeblocks 6s 2s +200%
sign_signature_pre_hash_internal 6s 3s +100%
sign_verify 6s 4s +50%
sign_verify_pre_hash_internal 6s 4s +50%
keccak_absorb 5s 8s -38%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 5s 3s +67%
keccakf1600_xor_bytes (big endian) 5s 2s +150%
mld_sample_s1_s2_serial 5s 3s +67%
ntt_native_aarch64 5s 3s +67%
poly_chknorm 5s 2s +150%
poly_decompose_32_native_aarch64 5s 5s +0%
poly_pointwise_montgomery 5s 4s +25%
poly_shiftl 5s 5s +0%
poly_use_hint_c 5s 5s +0%
polyveck_chknorm 5s 6s -17%
polyvecl_pointwise_acc_montgomery 5s 4s +25%
polyvecl_uniform_gamma1 5s 3s +67%
polyw1_pack 5s 3s +67%
rej_eta_c 5s 4s +25%
shake128_finalize 5s 5s +0%
sign_verify_pre_hash_shake256 5s 4s +25%
unpack_pk_t1 5s 3s +67%
keccak_squeeze 4s 3s +33%
make_hint 4s 2s +100%
mld_ct_abs_i32 4s 2s +100%
mld_prepare_domain_separation_prefix 4s 4s +0%
mld_sample_s1_s2 4s 4s +0%
montgomery_reduce 4s 3s +33%
pack_pk 4s 4s +0%
pack_sig_h_poly 4s 2s +100%
pack_sig_z 4s 3s +33%
pointwise_acc_native_aarch64 4s 4s +0%
pointwise_native_aarch64 4s 3s +33%
poly_caddq_c 4s 4s +0%
poly_caddq_native 4s 4s +0%
poly_caddq_native_aarch64 4s 3s +33%
poly_decompose_88_native_aarch64 4s 3s +33%
poly_invntt_tomont 4s 3s +33%
poly_permute_bitrev_to_custom_optional 4s 3s +33%
poly_sub 4s 2s +100%
poly_uniform_eta 4s 3s +33%
poly_use_hint_native_aarch64 4s 4s +0%
polyeta_pack 4s 2s +100%
polyveck_caddq 4s 4s +0%
polyveck_pack_w1 4s 2s +100%
polyvecl_pointwise_acc_montgomery_native 4s 5s -20%
polyvecl_unpack_eta 4s 2s +100%
polyvecl_unpack_z 4s 1s +300%
polyz_unpack_17_native_aarch64 4s 2s +100%
polyz_unpack_19_native_aarch64 4s 6s -33%
reduce32 4s 7s -43%
rej_eta 4s 3s +33%
shake128_init 4s 3s +33%
shake256_absorb 4s 2s +100%
shake256_squeeze 4s 2s +100%
sign_signature 4s 4s +0%
sign_signature_extmu 4s 5s -20%
sign_verify_extmu 4s 3s +33%
sk_t0hat_get_poly 4s 2s +100%
sys_check_capability 4s 3s +33%
unpack_sk 4s 3s +33%
unpack_sk_s1hat 4s 3s +33%
caddq 3s 2s +50%
decompose 3s 3s +0%
fqscale 3s 5s -40%
keccak_f1600_x1_native_aarch64 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a 3s 3s +0%
keccakf1600_xor_bytes 3s 4s -25%
mld_ct_get_optblocker_i64 3s 3s +0%
mld_ct_sel_int32 3s 2s +50%
mld_polymat_expand_entry 3s 4s -25%
mld_value_barrier_u32 3s 3s +0%
mld_value_barrier_u8 3s 3s +0%
ntt_native_x86_64 3s 3s +0%
pack_sk_rho_key_tr_s2_t0 3s 1s +200%
pack_sk_s1 3s 2s +50%
pointwise_native_x86_64 3s 2s +50%
poly_chknorm_native_aarch64 3s 2s +50%
poly_decompose 3s 4s -25%
poly_decompose_native 3s 4s -25%
poly_make_hint 3s 2s +50%
poly_ntt 3s 2s +50%
poly_ntt_c 3s 4s -25%
poly_pointwise_montgomery_native 3s 7s -57%
poly_reduce 3s 3s +0%
poly_uniform_gamma1 3s 3s +0%
poly_uniform_gamma1_4x 3s 4s -25%
poly_use_hint 3s 2s +50%
polyt1_unpack 3s 2s +50%
polyvec_matrix_pointwise_montgomery_row 3s 3s +0%
polyveck_ntt 3s 4s -25%
polyveck_reduce 3s 7s -57%
polyveck_unpack_t0 3s 5s -40%
polyz_unpack 3s 2s +50%
polyz_unpack_native 3s 2s +50%
rej_eta_native 3s 6s -50%
shake128_squeeze 3s 2s +50%
shake256_init 3s 1s +200%
shake256_release 3s 1s +200%
sk_s1hat_get_poly 3s 3s +0%
use_hint 3s 3s +0%
yvec_get_poly 3s 3s +0%
yvec_init 3s 2s +50%
intt_native_x86_64 2s 4s -50%
keccak_finalize 2s 3s -33%
keccak_init 2s 4s -50%
keccakf1600x4_permute 2s 3s -33%
keccakf1600x4_xor_bytes 2s 2s +0%
mld_ct_cmask_nonzero_u32 2s 4s -50%
mld_ct_cmask_nonzero_u8 2s 4s -50%
mld_ct_get_optblocker_u32 2s 2s +0%
mld_ct_get_optblocker_u8 2s 2s +0%
mld_keccakf1600_extract_bytes 2s 3s -33%
nttunpack_native_x86_64 2s 4s -50%
pack_sig_c 2s 5s -60%
poly_ntt_native 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native 2s 5s -60%
poly_use_hint_native 2s 4s -50%
polyt1_pack 2s 4s -50%
polyveck_unpack_eta 2s 4s -50%
polyvecl_uniform_gamma1_serial 2s 2s +0%
polyz_pack 2s 2s +0%
power2round 2s 4s -50%
shake128_absorb 2s 3s -33%
shake128_release 2s 2s +0%
shake128x4_absorb_once 2s 2s +0%
shake128x4_squeezeblocks 2s 1s +100%
shake256_finalize 2s 1s +100%
shake256x4_absorb_once 2s 2s +0%
sk_s2hat_get_poly 2s 3s -33%
unpack_sk_t0hat 2s 5s -60%
mld_compute_pack_z - 7s -
sign_pk_from_sk - 20s -
keccak_f1600_x1_native_aarch64_v84a 1s 1s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 1s 1s +0%
keccak_f1600_x4_native_avx2 1s 3s -67%
keccakf1600x4_extract_bytes 1s 4s -75%
mld_ct_cmask_neg_i32 1s 2s -50%
mld_value_barrier_i64 1s 1s +0%
poly_invntt_tomont_native 1s 4s -75%
shake256 1s 2s -50%
sig_unpack_hints 1s 2s -50%
unpack_sk_s2hat 1s 4s -75%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 6, 2026

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

⚠️ Attention Required

Proof Status Current Previous Change
**TOTAL** ⚠️ 4414s 1421s +210.6%
mld_compute_pack_z - 5s -
sign_pk_from_sk - 13s -
mld_attempt_signature_generation ⚠️ 466s 25s +1764%
sign_keypair_internal ⚠️ 148s 15s +887%
sign_signature_internal ⚠️ 1621s 5s +32320%
sign_verify_internal ⚠️ 713s 22s +3141%
Full Results (198 proofs)
Proof Status Current Previous Change
**TOTAL** ⚠️ 4414s 1421s +210.6%
sign_signature_internal ⚠️ 1621s 5s +32320%
sign_verify_internal ⚠️ 713s 22s +3141%
mld_attempt_signature_generation ⚠️ 466s 25s +1764%
poly_pointwise_montgomery_c 189s 169s +12%
sign_keypair_internal ⚠️ 148s 15s +887%
rej_uniform_native 116s 103s +13%
mld_invntt_layer 112s 95s +18%
polyvec_matrix_pointwise_montgomery_yvec 96s 88s +9%
mld_ct_memcmp 92s 71s +30%
mld_ntt_layer 44s 42s +5%
fqmul 28s 28s +0%
keccakf1600x4_permute_native 23s 22s +5%
polyveck_power2round 18s 16s +12%
polyeta_unpack 17s 17s +0%
mld_ntt_butterfly_block 15s 17s -12%
poly_uniform_eta_4x 15s 12s +25%
poly_chknorm_c 14s 13s +8%
polyveck_chknorm 12s 8s +50%
rej_uniform_c 12s 15s -20%
poly_invntt_tomont_c 11s 8s +38%
polyt0_unpack 11s 11s +0%
rej_uniform 11s 19s -42%
mld_check_pct 10s 11s -9%
poly_add 10s 10s +0%
poly_caddq_c 10s 7s +43%
poly_decompose_c 9s 6s +50%
polyvec_matrix_pointwise_montgomery_row 9s 7s +29%
keccakf1600_permute 8s 8s +0%
poly_power2round 8s 7s +14%
sign_keypair 8s 4s +100%
keccak_absorb_once_x4 7s 11s -36%
polyw1_pack 7s 3s +133%
sign_verify 7s 3s +133%
keccakf1600_permute_native 6s 6s +0%
mld_sample_s1_s2_serial 6s 3s +100%
pointwise_acc_native_aarch64 6s 5s +20%
poly_decompose_native 6s 2s +200%
poly_shiftl 6s 5s +20%
polyeta_pack 6s 3s +100%
polyveck_add 6s 6s +0%
polyveck_caddq 6s 3s +100%
polyveck_decompose 6s 5s +20%
polyvecl_chknorm 6s 6s +0%
sign 6s 8s -25%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid 5s 3s +67%
keccak_squeezeblocks_x4 5s 3s +67%
ntt_native_x86_64 5s 4s +25%
pack_sig_h_poly 5s 3s +67%
pack_sk_rho_key_tr_s2_t0 5s 2s +150%
pointwise_acc_native_x86_64 5s 5s +0%
poly_caddq_native 5s 3s +67%
poly_challenge 5s 4s +25%
poly_chknorm_native 5s 3s +67%
polyt1_pack 5s 3s +67%
polyveck_pack_w1 5s 4s +25%
polyvecl_ntt 5s 5s +0%
polyvecl_uniform_gamma1_serial 5s 2s +150%
sign_open 5s 4s +25%
sign_signature 5s 3s +67%
sign_signature_pre_hash_internal 5s 3s +67%
sign_verify_extmu 5s 6s -17%
sign_verify_pre_hash_shake256 5s 3s +67%
sk_s1hat_get_poly 5s 2s +150%
unpack_sk_t0hat 5s 4s +25%
keccak_absorb 4s 5s -20%
keccak_f1600_x1_native_aarch64_v84a 4s 3s +33%
keccakf1600_xor_bytes 4s 4s +0%
keccakf1600x4_permute 4s 2s +100%
mld_ct_abs_i32 4s 3s +33%
pack_sig_c 4s 2s +100%
poly_caddq 4s 4s +0%
poly_caddq_native_aarch64 4s 3s +33%
poly_chknorm 4s 2s +100%
poly_make_hint 4s 2s +100%
poly_ntt_native 4s 4s +0%
poly_uniform 4s 5s -20%
poly_uniform_eta 4s 3s +33%
poly_use_hint 4s 4s +0%
poly_use_hint_native_aarch64 4s 2s +100%
polyveck_invntt_tomont 4s 5s -20%
polyveck_ntt 4s 3s +33%
polyveck_pack_eta 4s 1s +300%
polyvecl_pointwise_acc_montgomery_c 4s 3s +33%
polyvecl_pointwise_acc_montgomery_native 4s 3s +33%
polyz_unpack_17_native_aarch64 4s 2s +100%
polyz_unpack_c 4s 4s +0%
rej_eta_c 4s 3s +33%
rej_eta_native 4s 5s -20%
shake256_finalize 4s 2s +100%
shake256_init 4s 2s +100%
shake256x4_absorb_once 4s 3s +33%
sign_signature_pre_hash_shake256 4s 2s +100%
sign_verify_pre_hash_internal 4s 4s +0%
sk_t0hat_get_poly 4s 3s +33%
sys_check_capability 4s 4s +0%
unpack_sk_s1hat 4s 2s +100%
unpack_sk_s2hat 4s 3s +33%
use_hint 4s 4s +0%
yvec_get_poly 4s 2s +100%
caddq 3s 2s +50%
fqscale 3s 3s +0%
intt_native_x86_64 3s 1s +200%
keccak_f1600_x1_native_aarch64 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid 3s 3s +0%
keccakf1600x4_extract_bytes 3s 4s -25%
make_hint 3s 3s +0%
mld_ct_cmask_nonzero_u8 3s 3s +0%
mld_ct_get_optblocker_i64 3s 2s +50%
mld_ct_get_optblocker_u8 3s 3s +0%
mld_prepare_domain_separation_prefix 3s 4s -25%
mld_sample_s1_s2 3s 4s -25%
montgomery_reduce 3s 2s +50%
ntt_native_aarch64 3s 4s -25%
nttunpack_native_x86_64 3s 3s +0%
pack_sk_s1 3s 3s +0%
pointwise_native_x86_64 3s 2s +50%
poly_decompose_88_native_aarch64 3s 2s +50%
poly_invntt_tomont_native 3s 4s -25%
poly_ntt_c 3s 3s +0%
poly_pointwise_montgomery 3s 5s -40%
poly_uniform_gamma1 3s 7s -57%
poly_uniform_gamma1_4x 3s 5s -40%
poly_use_hint_native 3s 4s -25%
polyt0_pack 3s 4s -25%
polyt1_unpack 3s 3s +0%
polyveck_reduce 3s 3s +0%
polyveck_unpack_eta 3s 3s +0%
polyz_unpack 3s 2s +50%
power2round 3s 2s +50%
reduce32 3s 2s +50%
rej_eta 3s 3s +0%
shake128_init 3s 3s +0%
shake128_release 3s 2s +50%
shake128x4_absorb_once 3s 2s +50%
shake128x4_squeezeblocks 3s 4s -25%
sig_unpack_hints 3s 3s +0%
sign_signature_extmu 3s 3s +0%
unpack_sk 3s 4s -25%
decompose 2s 4s -50%
keccak_f1600_x4_native_aarch64_v84a 2s 1s +100%
keccak_f1600_x4_native_avx2 2s 1s +100%
keccak_init 2s 3s -33%
keccak_squeeze 2s 2s +0%
keccakf1600_extract_bytes (big endian) 2s 1s +100%
keccakf1600_xor_bytes (big endian) 2s 3s -33%
keccakf1600x4_xor_bytes 2s 5s -60%
mld_ct_cmask_neg_i32 2s 2s +0%
mld_ct_cmask_nonzero_u32 2s 3s -33%
mld_ct_get_optblocker_u32 2s 3s -33%
mld_ct_sel_int32 2s 2s +0%
mld_h 2s 3s -33%
mld_keccakf1600_extract_bytes 2s 2s +0%
mld_polymat_expand_entry 2s 3s -33%
mld_value_barrier_i64 2s 3s -33%
mld_value_barrier_u8 2s 1s +100%
pack_pk 2s 2s +0%
pack_sig_z 2s 3s -33%
pointwise_native_aarch64 2s 3s -33%
poly_chknorm_native_aarch64 2s 4s -50%
poly_decompose 2s 2s +0%
poly_decompose_32_native_aarch64 2s 3s -33%
poly_invntt_tomont 2s 1s +100%
poly_ntt 2s 3s -33%
poly_permute_bitrev_to_custom_optional 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native 2s 2s +0%
poly_pointwise_montgomery_native 2s 3s -33%
poly_reduce 2s 3s -33%
poly_sub 2s 5s -60%
poly_uniform_4x 2s 2s +0%
poly_use_hint_c 2s 2s +0%
polyvec_matrix_expand 2s 4s -50%
polyvec_matrix_expand_serial 2s 2s +0%
polyvec_matrix_pointwise_montgomery 2s 2s +0%
polyveck_pack_t0 2s 3s -33%
polyveck_unpack_t0 2s 2s +0%
polyvecl_pack_eta 2s 4s -50%
polyvecl_pointwise_acc_montgomery 2s 4s -50%
polyvecl_uniform_gamma1 2s 2s +0%
polyvecl_unpack_eta 2s 4s -50%
polyvecl_unpack_z 2s 2s +0%
polyz_pack 2s 3s -33%
polyz_unpack_19_native_aarch64 2s 3s -33%
polyz_unpack_native 2s 5s -60%
shake128_absorb 2s 6s -67%
shake128_finalize 2s 1s +100%
shake128_squeeze 2s 4s -50%
shake256 2s 3s -33%
shake256_absorb 2s 2s +0%
shake256_release 2s 3s -33%
shake256_squeeze 2s 1s +100%
shake256x4_squeezeblocks 2s 1s +100%
sk_s2hat_get_poly 2s 3s -33%
unpack_pk_t1 2s 2s +0%
yvec_init 2s 2s +0%
mld_compute_pack_z - 5s -
sign_pk_from_sk - 13s -
keccak_finalize 1s 3s -67%
mld_value_barrier_u32 1s 2s -50%

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