Skip to content

mldsa: Explain packed byte counts via check-magic - #1411

Merged
hanno-becker merged 3 commits into
mainfrom
check-magic-packed-bytes
Sep 2, 2026
Merged

mldsa: Explain packed byte counts via check-magic#1411
hanno-becker merged 3 commits into
mainfrom
check-magic-packed-bytes

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Sep 1, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@mkannwischer
check-magic: Verify annotations for constants below 1000
b686409 
The annotation regexp required at least four digits, so annotations for
smaller constants were silently ignored. Accept any number of digits;
requiring an explanation stays limited to four digits and above.

This revives the 16 and 44 annotations in the native headers. The
3 == 2 + 1 and 5 == 4 + 1 annotations explain nothing and are dropped.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
check-magic: Allow annotations to refer to integer defines
e8ea81a 
Defines were only remembered when the line also carried a magic
constant, so MLDSA_N or a bit width could not be used in an annotation.
Remember integer defines directly instead.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
mldsa: Explain packed byte counts via check-magic
8fae229 
Restore the concrete byte counts and connect them to the packing bit
widths with check-magic annotations.

The parameter set specific annotations spell out the bit width, as
check-magic resolves defines by scan order rather than by preprocessor
branch.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer
mkannwischer force-pushed the check-magic-packed-bytes branch from 96454ba to 8fae229 Compare September 2, 2026 01:19
@mkannwischer
mkannwischer marked this pull request as ready for review September 2, 2026 01:19
@mkannwischer
mkannwischer requested a review from a team as a code owner September 2, 2026 01:19
@oqs-bot

oqs-bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 31s 7s +343%
mld_attempt_signature_generation ⚠️ 121s 31s +290%
sign_keypair_internal ⚠️ 28s 3s +833%
sign_pk_from_sk ⚠️ 49s 5s +880%
sign_verify_internal ⚠️ 159s 71s +124%
Full Results (212 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1213s 1482s -18.2%
sign_verify_internal ⚠️ 159s 71s +124%
mld_attempt_signature_generation ⚠️ 121s 31s +290%
polyvec_matrix_pointwise_montgomery_yvec ✅ 80s 201s -60%
poly_pointwise_montgomery_c ✅ 65s 116s -44%
mld_invntt_layer ✅ 53s 108s -51%
sign_pk_from_sk ⚠️ 49s 5s +880%
compute_pack_t0_t1 ⚠️ 31s 7s +343%
sign_keypair_internal ⚠️ 28s 3s +833%
fqmul ✅ 23s 40s -43%
mld_ntt_layer ✅ 22s 43s -49%
keccakf1600x4_permute_native ✅ 12s 22s -45%
mld_ntt_butterfly_block ✅ 11s 25s -56%
sign_signature_internal ✅ 11s 6s +83%
poly_ntt_c ✅ 10s 22s -55%
rej_uniform_c ✅ 10s 16s -38%
sig_unpack_hints ✅ 10s 1s +900%
polyveck_decompose_pack_w1 ✅ 9s - new
poly_uniform_eta_4x ✅ 8s 13s -38%
polyt0_unpack ✅ 8s 13s -38%
rej_uniform_native_x86_64 ✅ 8s - new
polyveck_chknorm ✅ 7s 36s -81%
sign_signature_pre_hash_shake256 ✅ 7s 7s +0%
mld_check_pct ✅ 6s 12s -50%
poly_chknorm_c ✅ 6s 13s -54%
polyveck_caddq ✅ 6s 7s -14%
polyw1_unpack_32 ✅ 6s - new
polyz_unpack_c ✅ 6s 9s -33%
keccak_absorb_once_x4 ✅ 5s 10s -50%
mld_sample_s1_s2 ✅ 5s 6s -17%
poly_invntt_tomont_c ✅ 5s 10s -50%
poly_use_hint ✅ 5s 3s +67%
polyeta_pack ✅ 5s 1s +400%
polyvecl_chknorm ✅ 5s 43s -88%
sign_keypair ✅ 5s 4s +25%
sign_signature_extmu ✅ 5s 4s +25%
fqscale ✅ 4s 3s +33%
intt_native_x86_64 ✅ 4s 4s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 4s 3s +33%
keccakf1600_permute_native ✅ 4s 2s +100%
keccakf1600x4_extract_bytes ✅ 4s 4s +0%
mld_keccakf1600_permute_c ✅ 4s 7s -43%
montgomery_reduce ✅ 4s 1s +300%
nttunpack_native_x86_64 ✅ 4s 3s +33%
pack_sk_rho_key_tr_s2 ✅ 4s 2s +100%
poly_decompose ✅ 4s 2s +100%
poly_decompose_c ✅ 4s 8s -50%
poly_use_hint_native_aarch64 ✅ 4s 4s +0%
polyt0_pack ✅ 4s 5s -20%
polyvec_matrix_pointwise_montgomery_row ✅ 4s 8s -50%
polyveck_invntt_tomont ✅ 4s 7s -43%
polyveck_reduce ✅ 4s 6s -33%
polyvecl_ntt ✅ 4s 7s -43%
polyvecl_uniform_gamma1 ✅ 4s 4s +0%
polyw1_unpack_88 ✅ 4s - new
unpack_sk_t0hat ✅ 4s 4s +0%
decompose ✅ 3s 4s -25%
keccak_squeeze ✅ 3s 2s +50%
keccakf1600_xor_bytes ✅ 3s 4s -25%
keccakf1600x4_xor_bytes ✅ 3s 2s +50%
mld_compute_pack_z ✅ 3s 5s -40%
mld_ct_cmask_nonzero_u32 ✅ 3s 3s +0%
mld_keccakf1600x4_xor_bytes_c ✅ 3s 2s +50%
mld_polymat_expand_entry ✅ 3s 3s +0%
mld_sign_attempt ✅ 3s - new
mld_sign_finish ✅ 3s - new
mld_sign_resume ✅ 3s - new
mld_value_barrier_i64 ✅ 3s 2s +50%
pack_sig_h ✅ 3s 2s +50%
pointwise_acc_native_aarch64 ✅ 3s 6s -50%
pointwise_native_aarch64 ✅ 3s 3s +0%
pointwise_native_x86_64 ✅ 3s 2s +50%
poly_add ✅ 3s 7s -57%
poly_caddq_c ✅ 3s 5s -40%
poly_chknorm_native ✅ 3s 4s -25%
poly_invntt_tomont_native ✅ 3s 5s -40%
poly_ntt ✅ 3s 2s +50%
poly_pointwise_montgomery_native ✅ 3s 4s -25%
poly_shiftl ✅ 3s 3s +0%
poly_uniform ✅ 3s 2s +50%
poly_uniform_4x ✅ 3s 4s -25%
poly_uniform_gamma1_4x ✅ 3s 3s +0%
poly_use_hint_c ✅ 3s 2s +50%
poly_use_hint_native ✅ 3s 7s -57%
polyt1_pack ✅ 3s 3s +0%
polyt1_unpack ✅ 3s 3s +0%
polyvec_matrix_expand_serial ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery ✅ 3s 3s +0%
polyvecl_pointwise_acc_montgomery_c ✅ 3s 3s +0%
polyvecl_uniform_gamma1_serial ✅ 3s 1s +200%
polyw1_pack ✅ 3s 3s +0%
polyz_unpack_17_native_aarch64 ✅ 3s 2s +50%
polyz_unpack_19_native_aarch64 ✅ 3s 5s -40%
rej_uniform ✅ 3s 7s -57%
rej_uniform_native_aarch64 ✅ 3s 5s -40%
shake128_finalize ✅ 3s 2s +50%
shake128_release ✅ 3s 2s +50%
sign_signature ✅ 3s 5s -40%
sign_signature_pre_hash_internal ✅ 3s 3s +0%
sk_s1hat_get_poly ✅ 3s 3s +0%
unpack_sk_s1hat ✅ 3s 1s +200%
yvec_init ✅ 3s 5s -40%
caddq ✅ 2s 2s +0%
intt_native_aarch64 ✅ 2s 2s +0%
keccak_absorb ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
keccak_finalize ✅ 2s 2s +0%
keccak_init ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) ✅ 2s 3s -33%
keccakf1600_permute ✅ 2s 4s -50%
keccakf1600x4_permute ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native ✅ 2s 2s +0%
make_hint ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 ✅ 2s 2s +0%
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_keccakf1600x4_extract_bytes_c ✅ 2s 2s +0%
mld_prepare_domain_separation_prefix ✅ 2s 4s -50%
mld_value_barrier_u32 ✅ 2s 4s -50%
ntt_native_aarch64 ✅ 2s 3s -33%
ntt_native_x86_64 ✅ 2s 5s -60%
pack_sig_z ✅ 2s 1s +100%
pointwise_acc_native_x86_64 ✅ 2s 5s -60%
poly_caddq ✅ 2s 3s -33%
poly_caddq_native_aarch64 ✅ 2s 2s +0%
poly_challenge ✅ 2s 5s -60%
poly_chknorm ✅ 2s 3s -33%
poly_chknorm_native_aarch64 ✅ 2s 2s +0%
poly_chknorm_native_x86_64 ✅ 2s 4s -50%
poly_decompose_32_native_aarch64 ✅ 2s 4s -50%
poly_decompose_88_native_aarch64 ✅ 2s 2s +0%
poly_decompose_native ✅ 2s 5s -60%
poly_decompose_native_x86_64 ✅ 2s 2s +0%
poly_ntt_native ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional ✅ 2s 3s -33%
poly_pointwise_montgomery ✅ 2s 2s +0%
poly_power2round ✅ 2s 7s -71%
poly_reduce ✅ 2s 4s -50%
poly_sub ✅ 2s 4s -50%
poly_uniform_eta ✅ 2s 5s -60%
poly_use_hint_native_x86_64 ✅ 2s - new
polyeta_unpack ✅ 2s 4s -50%
polyvec_matrix_expand ✅ 2s 6s -67%
polyveck_ntt ✅ 2s 4s -50%
polyveck_pack_eta ✅ 2s 3s -33%
polyvecl_unpack_eta ✅ 2s 2s +0%
polyvecl_unpack_z ✅ 2s 1s +100%
polyw1_pack_32 ✅ 2s 2s +0%
polyw1_pack_88 ✅ 2s 3s -33%
polyz_pack ✅ 2s 3s -33%
polyz_unpack ✅ 2s 3s -33%
polyz_unpack_native_x86_64 ✅ 2s 3s -33%
rej_eta ✅ 2s 5s -60%
rej_eta_native ✅ 2s 3s -33%
rej_uniform_eta_native_aarch64 ✅ 2s 5s -60%
shake128_absorb ✅ 2s 2s +0%
shake128x4_absorb_once ✅ 2s 2s +0%
shake128x4_squeezeblocks ✅ 2s 2s +0%
shake256 ✅ 2s 2s +0%
shake256_finalize ✅ 2s 1s +100%
shake256_release ✅ 2s 3s -33%
shake256x4_absorb_once ✅ 2s 2s +0%
sign_verify_pre_hash_internal ✅ 2s 5s -60%
sign_verify_pre_hash_shake256 ✅ 2s 6s -67%
sk_s2hat_get_poly ✅ 2s 1s +100%
unpack_pk_t1 ✅ 2s 2s +0%
use_hint ✅ 2s 2s +0%
yvec_get_poly ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 2s -50%
keccak_squeezeblocks_x4 ✅ 1s 4s -75%
keccakf1600_xor_bytes (big endian) ✅ 1s 2s -50%
keccakf1600x4_extract_bytes_native ✅ 1s 1s +0%
mld_ct_abs_i32 ✅ 1s 6s -83%
mld_ct_get_optblocker_i64 ✅ 1s 1s +0%
mld_ct_get_optblocker_u8 ✅ 1s 4s -75%
mld_ct_memcmp ✅ 1s 4s -75%
mld_sample_s1_s2_serial ✅ 1s 3s -67%
mld_value_barrier_u8 ✅ 1s 1s +0%
pack_sig_c ✅ 1s 3s -67%
pack_sk_s1 ✅ 1s 3s -67%
poly_caddq_native ✅ 1s 4s -75%
poly_caddq_native_x86_64 ✅ 1s 1s +0%
poly_invntt_tomont ✅ 1s 5s -80%
poly_permute_bitrev_to_custom_optional_native ✅ 1s 3s -67%
poly_uniform_gamma1 ✅ 1s 3s -67%
polyveck_unpack_eta ✅ 1s 3s -67%
polyvecl_pack_eta ✅ 1s 2s -50%
polyvecl_pointwise_acc_montgomery_native ✅ 1s 3s -67%
polyw1_unpack ✅ 1s - new
polyz_unpack_native ✅ 1s 3s -67%
power2round ✅ 1s 2s -50%
reduce32 ✅ 1s 2s -50%
rej_eta_c ✅ 1s 4s -75%
rej_uniform_eta_native_x86_64 ✅ 1s - new
rej_uniform_native ✅ 1s 4s -75%
shake128_init ✅ 1s 6s -83%
shake128_squeeze ✅ 1s 3s -67%
shake256_absorb ✅ 1s 4s -75%
shake256_init ✅ 1s 4s -75%
shake256_squeeze ✅ 1s 4s -75%
shake256x4_squeezeblocks ✅ 1s 2s -50%
sign_verify ✅ 1s 6s -83%
sign_verify_extmu ✅ 1s 2s -50%
sk_t0hat_get_poly ✅ 1s 1s +0%
sys_check_capability ✅ 1s 1s +0%
unpack_sk ✅ 1s 3s -67%
unpack_sk_s2hat ✅ 1s 3s -67%

@oqs-bot

oqs-bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 30s 12s +150%
mld_attempt_signature_generation ⚠️ 137s 19s +621%
sign_keypair_internal ⚠️ 21s 4s +425%
sign_pk_from_sk ⚠️ 36s 5s +620%
sign_verify_internal ⚠️ 180s 49s +267%
Full Results (212 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1234s 1364s -9.5%
sign_verify_internal ⚠️ 180s 49s +267%
mld_attempt_signature_generation ⚠️ 137s 19s +621%
polyvec_matrix_pointwise_montgomery_yvec ✅ 95s 149s -36%
poly_pointwise_montgomery_c ✅ 65s 112s -42%
mld_invntt_layer ✅ 57s 105s -46%
sign_pk_from_sk ⚠️ 36s 5s +620%
compute_pack_t0_t1 ⚠️ 30s 12s +150%
mld_ntt_layer ✅ 23s 41s -44%
fqmul ✅ 22s 39s -44%
sign_keypair_internal ⚠️ 21s 4s +425%
sig_unpack_hints ✅ 16s 2s +700%
keccakf1600x4_permute_native ✅ 12s 22s -45%
sign_signature_internal ✅ 11s 4s +175%
mld_ntt_butterfly_block ✅ 10s 23s -57%
poly_ntt_c ✅ 10s 21s -52%
rej_uniform_native_x86_64 ✅ 9s - new
poly_chknorm_c ✅ 8s 11s -27%
poly_invntt_tomont_c ✅ 8s 11s -27%
rej_uniform_c ✅ 8s 16s -50%
poly_uniform_eta_4x ✅ 7s 12s -42%
polyt0_unpack ✅ 7s 12s -42%
sign_keypair ✅ 7s 5s +40%
keccak_absorb_once_x4 ✅ 6s 8s -25%
pointwise_acc_native_x86_64 ✅ 6s 4s +50%
polyeta_unpack ✅ 6s 14s -57%
polyz_unpack_c ✅ 6s 8s -25%
poly_caddq ✅ 5s 4s +25%
polyvec_matrix_pointwise_montgomery_row ✅ 5s 6s -17%
mld_check_pct ✅ 4s 15s -73%
mld_ct_sel_int32 ✅ 4s 3s +33%
mld_keccakf1600_permute_c ✅ 4s 7s -43%
mld_sample_s1_s2 ✅ 4s 1s +300%
mld_sample_s1_s2_serial ✅ 4s 4s +0%
pack_sk_rho_key_tr_s2 ✅ 4s 5s -20%
poly_decompose_native ✅ 4s 2s +100%
poly_permute_bitrev_to_custom_optional ✅ 4s 5s -20%
poly_pointwise_montgomery ✅ 4s 3s +33%
poly_use_hint_c ✅ 4s 5s -20%
polyeta_pack ✅ 4s 3s +33%
polyveck_chknorm ✅ 4s 67s -94%
polyveck_decompose_pack_w1 ✅ 4s - new
polyw1_unpack_88 ✅ 4s - new
polyz_unpack_17_native_aarch64 ✅ 4s 2s +100%
polyz_unpack_native_x86_64 ✅ 4s 3s +33%
rej_uniform ✅ 4s 8s -50%
shake256_absorb ✅ 4s 2s +100%
sign_signature_pre_hash_shake256 ✅ 4s 4s +0%
caddq ✅ 3s 6s -50%
intt_native_aarch64 ✅ 3s 3s +0%
intt_native_x86_64 ✅ 3s 2s +50%
keccak_absorb ✅ 3s 3s +0%
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_squeezeblocks_x4 ✅ 3s 3s +0%
keccakf1600_permute_native ✅ 3s 3s +0%
keccakf1600x4_permute ✅ 3s 4s -25%
mld_compute_pack_z ✅ 3s 6s -50%
mld_ct_abs_i32 ✅ 3s 3s +0%
mld_ct_cmask_neg_i32 ✅ 3s 2s +50%
mld_ct_cmask_nonzero_u32 ✅ 3s 3s +0%
mld_ct_get_optblocker_u32 ✅ 3s 2s +50%
mld_keccakf1600x4_xor_bytes_c ✅ 3s 4s -25%
ntt_native_aarch64 ✅ 3s 4s -25%
pack_sig_c ✅ 3s 5s -40%
pack_sig_z ✅ 3s 2s +50%
pointwise_acc_native_aarch64 ✅ 3s 6s -50%
poly_add ✅ 3s 7s -57%
poly_caddq_native_x86_64 ✅ 3s 4s -25%
poly_chknorm ✅ 3s 3s +0%
poly_chknorm_native_aarch64 ✅ 3s 2s +50%
poly_decompose_c ✅ 3s 5s -40%
poly_invntt_tomont_native ✅ 3s 3s +0%
poly_ntt_native ✅ 3s 3s +0%
poly_power2round ✅ 3s 4s -25%
poly_reduce ✅ 3s 4s -25%
poly_sub ✅ 3s 3s +0%
poly_uniform ✅ 3s 3s +0%
poly_uniform_4x ✅ 3s 3s +0%
poly_uniform_gamma1_4x ✅ 3s 5s -40%
polyt1_pack ✅ 3s 3s +0%
polyt1_unpack ✅ 3s 2s +50%
polyveck_caddq ✅ 3s 3s +0%
polyveck_invntt_tomont ✅ 3s 5s -40%
polyveck_pack_eta ✅ 3s 4s -25%
polyveck_unpack_eta ✅ 3s 2s +50%
polyvecl_unpack_z ✅ 3s 3s +0%
polyw1_pack ✅ 3s 4s -25%
polyz_unpack ✅ 3s 3s +0%
power2round ✅ 3s 2s +50%
rej_uniform_eta_native_aarch64 ✅ 3s 3s +0%
rej_uniform_eta_native_x86_64 ✅ 3s - new
rej_uniform_native_aarch64 ✅ 3s 3s +0%
shake256_init ✅ 3s 4s -25%
shake256x4_absorb_once ✅ 3s 1s +200%
sign_signature ✅ 3s 6s -50%
sign_signature_extmu ✅ 3s 4s -25%
sign_signature_pre_hash_internal ✅ 3s 4s -25%
sign_verify_pre_hash_shake256 ✅ 3s 5s -40%
sys_check_capability ✅ 3s 2s +50%
unpack_sk ✅ 3s 3s +0%
yvec_init ✅ 3s 1s +200%
decompose ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
keccak_finalize ✅ 2s 2s +0%
keccak_init ✅ 2s 3s -33%
keccak_squeeze ✅ 2s 2s +0%
keccakf1600_extract_bytes (big endian) ✅ 2s 4s -50%
keccakf1600_permute ✅ 2s 2s +0%
keccakf1600_xor_bytes (big endian) ✅ 2s 6s -67%
keccakf1600x4_extract_bytes ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native ✅ 2s 4s -50%
keccakf1600x4_xor_bytes ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u8 ✅ 2s 2s +0%
mld_prepare_domain_separation_prefix ✅ 2s 3s -33%
mld_sign_attempt ✅ 2s - new
mld_sign_finish ✅ 2s - new
mld_sign_resume ✅ 2s - new
mld_value_barrier_u32 ✅ 2s 1s +100%
mld_value_barrier_u8 ✅ 2s 4s -50%
ntt_native_x86_64 ✅ 2s 3s -33%
pack_sig_h ✅ 2s 4s -50%
pack_sk_s1 ✅ 2s 3s -33%
pointwise_native_x86_64 ✅ 2s 4s -50%
poly_caddq_c ✅ 2s 3s -33%
poly_challenge ✅ 2s 6s -67%
poly_chknorm_native ✅ 2s 4s -50%
poly_chknorm_native_x86_64 ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 ✅ 2s 4s -50%
poly_decompose_88_native_aarch64 ✅ 2s 3s -33%
poly_decompose_native_x86_64 ✅ 2s 2s +0%
poly_invntt_tomont ✅ 2s 2s +0%
poly_ntt ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native ✅ 2s 3s -33%
poly_pointwise_montgomery_native ✅ 2s 2s +0%
poly_uniform_gamma1 ✅ 2s 3s -33%
poly_use_hint ✅ 2s 2s +0%
poly_use_hint_native ✅ 2s 3s -33%
poly_use_hint_native_aarch64 ✅ 2s 3s -33%
poly_use_hint_native_x86_64 ✅ 2s - new
polyvec_matrix_expand ✅ 2s 3s -33%
polyvec_matrix_expand_serial ✅ 2s 4s -50%
polyveck_reduce ✅ 2s 4s -50%
polyvecl_chknorm ✅ 2s 11s -82%
polyvecl_ntt ✅ 2s 3s -33%
polyvecl_pack_eta ✅ 2s 2s +0%
polyvecl_pointwise_acc_montgomery ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery_c ✅ 2s 4s -50%
polyvecl_pointwise_acc_montgomery_native ✅ 2s 3s -33%
polyvecl_uniform_gamma1 ✅ 2s 2s +0%
polyvecl_unpack_eta ✅ 2s 4s -50%
polyw1_pack_88 ✅ 2s 2s +0%
polyw1_unpack ✅ 2s - new
polyz_pack ✅ 2s 2s +0%
polyz_unpack_native ✅ 2s 3s -33%
reduce32 ✅ 2s 3s -33%
rej_eta ✅ 2s 5s -60%
shake128_init ✅ 2s 2s +0%
shake128x4_absorb_once ✅ 2s 2s +0%
shake256 ✅ 2s 1s +100%
shake256_release ✅ 2s 1s +100%
shake256x4_squeezeblocks ✅ 2s 2s +0%
sign_verify_extmu ✅ 2s 5s -60%
sign_verify_pre_hash_internal ✅ 2s 5s -60%
sk_s2hat_get_poly ✅ 2s 5s -60%
sk_t0hat_get_poly ✅ 2s 1s +100%
unpack_pk_t1 ✅ 2s 3s -33%
unpack_sk_s1hat ✅ 2s 3s -33%
unpack_sk_s2hat ✅ 2s 4s -50%
unpack_sk_t0hat ✅ 2s 2s +0%
yvec_get_poly ✅ 2s 3s -33%
fqscale ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 2s -50%
keccakf1600_xor_bytes ✅ 1s 3s -67%
keccakf1600x4_xor_bytes_native ✅ 1s 5s -80%
make_hint ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 ✅ 1s 4s -75%
mld_ct_get_optblocker_u8 ✅ 1s 2s -50%
mld_ct_memcmp ✅ 1s 1s +0%
mld_h ✅ 1s 4s -75%
mld_keccakf1600_extract_bytes ✅ 1s 2s -50%
mld_keccakf1600x4_extract_bytes_c ✅ 1s 4s -75%
mld_polymat_expand_entry ✅ 1s 2s -50%
mld_value_barrier_i64 ✅ 1s 3s -67%
montgomery_reduce ✅ 1s 2s -50%
nttunpack_native_x86_64 ✅ 1s 4s -75%
pointwise_native_aarch64 ✅ 1s 2s -50%
poly_caddq_native ✅ 1s 3s -67%
poly_caddq_native_aarch64 ✅ 1s 3s -67%
poly_decompose ✅ 1s 2s -50%
poly_shiftl ✅ 1s 4s -75%
poly_uniform_eta ✅ 1s 2s -50%
polyt0_pack ✅ 1s 4s -75%
polyveck_ntt ✅ 1s 2s -50%
polyvecl_uniform_gamma1_serial ✅ 1s 2s -50%
polyw1_pack_32 ✅ 1s 3s -67%
polyw1_unpack_32 ✅ 1s - new
polyz_unpack_19_native_aarch64 ✅ 1s 4s -75%
rej_eta_c ✅ 1s 4s -75%
rej_eta_native ✅ 1s 3s -67%
rej_uniform_native ✅ 1s 5s -80%
shake128_absorb ✅ 1s 3s -67%
shake128_finalize ✅ 1s 3s -67%
shake128_release ✅ 1s 2s -50%
shake128_squeeze ✅ 1s 2s -50%
shake128x4_squeezeblocks ✅ 1s 2s -50%
shake256_finalize ✅ 1s 2s -50%
shake256_squeeze ✅ 1s 2s -50%
sign_verify ✅ 1s 4s -75%
sk_s1hat_get_poly ✅ 1s 2s -50%
use_hint ✅ 1s 2s -50%

@oqs-bot

oqs-bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 27s 12s +125%
mld_attempt_signature_generation ⚠️ 164s 34s +382%
sign_keypair_internal ⚠️ 49s 6s +717%
sign_pk_from_sk ⚠️ 65s 6s +983%
sign_verify_internal ⚠️ 204s 47s +334%
Full Results (212 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1360s 1436s -5.3%
sign_verify_internal ⚠️ 204s 47s +334%
mld_attempt_signature_generation ⚠️ 164s 34s +382%
polyvec_matrix_pointwise_montgomery_yvec ✅ 119s 196s -39%
poly_pointwise_montgomery_c ✅ 67s 125s -46%
sign_pk_from_sk ⚠️ 65s 6s +983%
mld_invntt_layer ✅ 56s 111s -50%
sign_keypair_internal ⚠️ 49s 6s +717%
compute_pack_t0_t1 ⚠️ 27s 12s +125%
fqmul ✅ 22s 39s -44%
mld_ntt_layer ✅ 21s 44s -52%
sig_unpack_hints ✅ 14s 4s +250%
sign_signature_internal ✅ 13s 3s +333%
keccakf1600x4_permute_native ✅ 12s 25s -52%
poly_ntt_c ✅ 12s 19s -37%
mld_ntt_butterfly_block ✅ 10s 23s -57%
polyeta_unpack ✅ 9s 13s -31%
poly_chknorm_c ✅ 8s 13s -38%
rej_uniform_c ✅ 8s 18s -56%
rej_uniform_native_x86_64 ✅ 8s - new
polyt0_unpack ✅ 7s 14s -50%
polyvecl_ntt ✅ 7s 8s -12%
poly_invntt_tomont_c ✅ 6s 9s -33%
poly_uniform_eta_4x ✅ 6s 12s -50%
polyveck_reduce ✅ 6s 6s +0%
polyz_pack ✅ 6s 4s +50%
intt_native_x86_64 ✅ 5s 4s +25%
keccak_absorb_once_x4 ✅ 5s 8s -38%
keccakf1600_xor_bytes (big endian) ✅ 5s 2s +150%
mld_check_pct ✅ 5s 15s -67%
poly_chknorm_native ✅ 5s 1s +400%
sign_keypair ✅ 5s 4s +25%
sign_signature_pre_hash_shake256 ✅ 5s 3s +67%
keccakf1600_permute ✅ 4s 2s +100%
mld_keccakf1600_permute_c ✅ 4s 8s -50%
mld_sample_s1_s2 ✅ 4s 8s -50%
mld_sign_resume ✅ 4s - new
pack_sig_c ✅ 4s 2s +100%
pack_sig_h ✅ 4s 3s +33%
pointwise_acc_native_aarch64 ✅ 4s 5s -20%
pointwise_acc_native_x86_64 ✅ 4s 8s -50%
poly_power2round ✅ 4s 7s -43%
poly_uniform ✅ 4s 4s +0%
poly_use_hint_c ✅ 4s 4s +0%
polyt1_pack ✅ 4s 5s -20%
polyvec_matrix_pointwise_montgomery_row ✅ 4s 13s -69%
polyveck_caddq ✅ 4s 8s -50%
polyveck_chknorm ✅ 4s 9s -56%
polyveck_invntt_tomont ✅ 4s 4s +0%
polyvecl_pointwise_acc_montgomery_native ✅ 4s 2s +100%
polyz_unpack_native_x86_64 ✅ 4s 3s +33%
rej_eta ✅ 4s 2s +100%
rej_uniform ✅ 4s 7s -43%
shake256x4_absorb_once ✅ 4s 5s -20%
sign_verify_extmu ✅ 4s 4s +0%
unpack_sk ✅ 4s 4s +0%
yvec_get_poly ✅ 4s 2s +100%
caddq ✅ 3s 3s +0%
decompose ✅ 3s 2s +50%
keccak_absorb ✅ 3s 4s -25%
keccakf1600_permute_native ✅ 3s 3s +0%
keccakf1600x4_xor_bytes ✅ 3s 1s +200%
make_hint ✅ 3s 2s +50%
mld_ct_cmask_nonzero_u32 ✅ 3s 5s -40%
mld_ct_get_optblocker_i64 ✅ 3s 2s +50%
mld_ct_memcmp ✅ 3s 1s +200%
mld_h ✅ 3s 2s +50%
mld_prepare_domain_separation_prefix ✅ 3s 3s +0%
mld_sample_s1_s2_serial ✅ 3s 6s -50%
mld_sign_attempt ✅ 3s - new
ntt_native_aarch64 ✅ 3s 4s -25%
pack_sig_z ✅ 3s 3s +0%
poly_caddq ✅ 3s 5s -40%
poly_caddq_native ✅ 3s 3s +0%
poly_chknorm_native_aarch64 ✅ 3s 5s -40%
poly_chknorm_native_x86_64 ✅ 3s 2s +50%
poly_decompose_c ✅ 3s 6s -50%
poly_invntt_tomont_native ✅ 3s 2s +50%
poly_pointwise_montgomery_native ✅ 3s 3s +0%
poly_shiftl ✅ 3s 4s -25%
poly_use_hint_native ✅ 3s 1s +200%
poly_use_hint_native_x86_64 ✅ 3s - new
polyvec_matrix_expand_serial ✅ 3s 3s +0%
polyveck_decompose_pack_w1 ✅ 3s - new
polyveck_pack_eta ✅ 3s 5s -40%
polyvecl_pointwise_acc_montgomery_c ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial ✅ 3s 2s +50%
polyvecl_unpack_eta ✅ 3s 3s +0%
polyw1_pack ✅ 3s 2s +50%
polyw1_unpack ✅ 3s - new
polyz_unpack ✅ 3s 3s +0%
polyz_unpack_c ✅ 3s 7s -57%
reduce32 ✅ 3s 3s +0%
rej_eta_c ✅ 3s 4s -25%
rej_eta_native ✅ 3s 4s -25%
rej_uniform_eta_native_x86_64 ✅ 3s - new
shake128_init ✅ 3s 2s +50%
sign_signature ✅ 3s 4s -25%
sign_signature_pre_hash_internal ✅ 3s 2s +50%
sign_verify_pre_hash_shake256 ✅ 3s 7s -57%
sys_check_capability ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 1s +100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 2s +0%
keccak_init ✅ 2s 1s +100%
keccak_squeezeblocks_x4 ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) ✅ 2s 3s -33%
keccakf1600_xor_bytes ✅ 2s 1s +100%
keccakf1600x4_extract_bytes ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native ✅ 2s 2s +0%
mld_compute_pack_z ✅ 2s 6s -67%
mld_ct_abs_i32 ✅ 2s 1s +100%
mld_ct_cmask_nonzero_u8 ✅ 2s 2s +0%
mld_ct_get_optblocker_u8 ✅ 2s 3s -33%
mld_polymat_expand_entry ✅ 2s 4s -50%
mld_value_barrier_i64 ✅ 2s 2s +0%
ntt_native_x86_64 ✅ 2s 2s +0%
pack_sk_rho_key_tr_s2 ✅ 2s 2s +0%
pack_sk_s1 ✅ 2s 2s +0%
pointwise_native_x86_64 ✅ 2s 5s -60%
poly_add ✅ 2s 8s -75%
poly_caddq_c ✅ 2s 3s -33%
poly_decompose ✅ 2s 2s +0%
poly_decompose_32_native_aarch64 ✅ 2s 3s -33%
poly_decompose_native ✅ 2s 2s +0%
poly_invntt_tomont ✅ 2s 4s -50%
poly_permute_bitrev_to_custom_optional_native ✅ 2s 3s -33%
poly_pointwise_montgomery ✅ 2s 3s -33%
poly_sub ✅ 2s 5s -60%
poly_uniform_eta ✅ 2s 5s -60%
poly_uniform_gamma1 ✅ 2s 3s -33%
poly_use_hint ✅ 2s 4s -50%
polyt0_pack ✅ 2s 3s -33%
polyveck_ntt ✅ 2s 3s -33%
polyvecl_pack_eta ✅ 2s 2s +0%
polyvecl_uniform_gamma1 ✅ 2s 3s -33%
polyw1_pack_32 ✅ 2s 3s -33%
polyw1_pack_88 ✅ 2s 2s +0%
polyw1_unpack_32 ✅ 2s - new
polyw1_unpack_88 ✅ 2s - new
polyz_unpack_native ✅ 2s 1s +100%
power2round ✅ 2s 3s -33%
rej_uniform_eta_native_aarch64 ✅ 2s 3s -33%
rej_uniform_native ✅ 2s 5s -60%
shake128_absorb ✅ 2s 2s +0%
shake128_squeeze ✅ 2s 1s +100%
shake128x4_absorb_once ✅ 2s 4s -50%
shake128x4_squeezeblocks ✅ 2s 1s +100%
shake256 ✅ 2s 3s -33%
shake256_finalize ✅ 2s 3s -33%
shake256_init ✅ 2s 3s -33%
sign_signature_extmu ✅ 2s 4s -50%
sign_verify ✅ 2s 2s +0%
sign_verify_pre_hash_internal ✅ 2s 3s -33%
sk_s2hat_get_poly ✅ 2s 2s +0%
sk_t0hat_get_poly ✅ 2s 3s -33%
unpack_pk_t1 ✅ 2s 2s +0%
unpack_sk_s1hat ✅ 2s 3s -33%
unpack_sk_s2hat ✅ 2s 3s -33%
yvec_init ✅ 2s 4s -50%
fqscale ✅ 1s 1s +0%
intt_native_aarch64 ✅ 1s 4s -75%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 1s 2s -50%
keccak_f1600_x4_native_avx2 ✅ 1s 3s -67%
keccak_finalize ✅ 1s 1s +0%
keccak_squeeze ✅ 1s 5s -80%
keccakf1600x4_extract_bytes_native ✅ 1s 4s -75%
keccakf1600x4_permute ✅ 1s 2s -50%
mld_ct_cmask_neg_i32 ✅ 1s 2s -50%
mld_ct_get_optblocker_u32 ✅ 1s 2s -50%
mld_ct_sel_int32 ✅ 1s 2s -50%
mld_keccakf1600_extract_bytes ✅ 1s 1s +0%
mld_keccakf1600x4_extract_bytes_c ✅ 1s 3s -67%
mld_keccakf1600x4_xor_bytes_c ✅ 1s 1s +0%
mld_sign_finish ✅ 1s - new
mld_value_barrier_u32 ✅ 1s 3s -67%
mld_value_barrier_u8 ✅ 1s 2s -50%
montgomery_reduce ✅ 1s 2s -50%
nttunpack_native_x86_64 ✅ 1s 3s -67%
pointwise_native_aarch64 ✅ 1s 4s -75%
poly_caddq_native_aarch64 ✅ 1s 3s -67%
poly_caddq_native_x86_64 ✅ 1s 3s -67%
poly_challenge ✅ 1s 4s -75%
poly_chknorm ✅ 1s 4s -75%
poly_decompose_88_native_aarch64 ✅ 1s 2s -50%
poly_decompose_native_x86_64 ✅ 1s 3s -67%
poly_ntt ✅ 1s 2s -50%
poly_ntt_native ✅ 1s 4s -75%
poly_permute_bitrev_to_custom_optional ✅ 1s 2s -50%
poly_reduce ✅ 1s 4s -75%
poly_uniform_4x ✅ 1s 3s -67%
poly_uniform_gamma1_4x ✅ 1s 3s -67%
poly_use_hint_native_aarch64 ✅ 1s 3s -67%
polyeta_pack ✅ 1s 3s -67%
polyt1_unpack ✅ 1s 3s -67%
polyvec_matrix_expand ✅ 1s 3s -67%
polyveck_unpack_eta ✅ 1s 3s -67%
polyvecl_chknorm ✅ 1s 38s -97%
polyvecl_pointwise_acc_montgomery ✅ 1s 2s -50%
polyvecl_unpack_z ✅ 1s 3s -67%
polyz_unpack_17_native_aarch64 ✅ 1s 4s -75%
polyz_unpack_19_native_aarch64 ✅ 1s 5s -80%
rej_uniform_native_aarch64 ✅ 1s 3s -67%
shake128_finalize ✅ 1s 2s -50%
shake128_release ✅ 1s 3s -67%
shake256_absorb ✅ 1s 3s -67%
shake256_release ✅ 1s 5s -80%
shake256_squeeze ✅ 1s 2s -50%
shake256x4_squeezeblocks ✅ 1s 4s -75%
sk_s1hat_get_poly ✅ 1s 3s -67%
unpack_sk_t0hat ✅ 1s 4s -75%
use_hint ✅ 1s 3s -67%

@oqs-bot

oqs-bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 94s 50s +88%
mld_attempt_signature_generation ⚠️ 154s 58s +166%
polyveck_chknorm ⚠️ 54s 5s +980%
sign_pk_from_sk ⚠️ 31s 5s +520%
sign_signature_internal ⚠️ 91s 26s +250%
sign_verify_internal ⚠️ 253s 114s +122%
Full Results (212 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1573s 1514s +3.9%
sign_verify_internal ⚠️ 253s 114s +122%
mld_attempt_signature_generation ⚠️ 154s 58s +166%
polyvecl_pointwise_acc_montgomery_c ✅ 144s 131s +10%
compute_pack_t0_t1 ⚠️ 94s 50s +88%
sign_signature_internal ⚠️ 91s 26s +250%
mld_invntt_layer ✅ 58s 107s -46%
polyveck_chknorm ⚠️ 54s 5s +980%
poly_pointwise_montgomery_c ✅ 43s 114s -62%
sign_pk_from_sk ⚠️ 31s 5s +520%
mld_ntt_layer ✅ 22s 42s -48%
fqmul ✅ 21s 39s -46%
sig_unpack_hints ✅ 19s 2s +850%
sign_keypair_internal ✅ 18s 4s +350%
polyvec_matrix_expand ✅ 15s 28s -46%
polyvec_matrix_pointwise_montgomery_yvec ✅ 14s 15s -7%
keccakf1600x4_permute_native ✅ 12s 22s -45%
poly_ntt_c ✅ 11s 19s -42%
rej_uniform ✅ 11s 18s -39%
mld_ntt_butterfly_block ✅ 10s 23s -57%
poly_chknorm_c ✅ 10s 17s -41%
poly_uniform_eta_4x ✅ 8s 11s -27%
rej_uniform_native_x86_64 ✅ 8s - new
rej_uniform_c ✅ 7s 15s -53%
mld_sign_attempt ✅ 6s - new
poly_invntt_tomont_c ✅ 6s 11s -45%
polyt0_unpack ✅ 6s 15s -60%
polyz_unpack_c ✅ 6s 11s -45%
sign_keypair ✅ 6s 4s +50%
keccak_absorb ✅ 5s 5s +0%
mld_check_pct ✅ 5s 14s -64%
poly_uniform_4x ✅ 5s 14s -64%
polyeta_unpack ✅ 5s 14s -64%
polyveck_decompose_pack_w1 ✅ 5s - new
rej_uniform_eta_native_aarch64 ✅ 5s 2s +150%
sign_signature ✅ 5s 3s +67%
unpack_pk_t1 ✅ 5s 5s +0%
keccak_absorb_once_x4 ✅ 4s 9s -56%
keccakf1600_permute ✅ 4s 2s +100%
keccakf1600_xor_bytes (big endian) ✅ 4s 4s +0%
mld_compute_pack_z ✅ 4s 7s -43%
pack_sk_s1 ✅ 4s 2s +100%
poly_chknorm_native ✅ 4s 4s +0%
poly_decompose_88_native_aarch64 ✅ 4s 4s +0%
polyvec_matrix_expand_serial ✅ 4s 8s -50%
polyvec_matrix_pointwise_montgomery_row ✅ 4s 2s +100%
polyveck_caddq ✅ 4s 3s +33%
polyvecl_chknorm ✅ 4s 10s -60%
polyw1_pack ✅ 4s 3s +33%
polyw1_unpack ✅ 4s - new
polyz_unpack_19_native_aarch64 ✅ 4s 5s -20%
rej_uniform_native ✅ 4s 4s +0%
shake128_absorb ✅ 4s 2s +100%
shake256 ✅ 4s 1s +300%
fqscale ✅ 3s 3s +0%
intt_native_aarch64 ✅ 3s 9s -67%
keccak_f1600_x4_native_aarch64_v84a ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 3s 1s +200%
keccak_finalize ✅ 3s 3s +0%
keccak_squeezeblocks_x4 ✅ 3s 4s -25%
keccakf1600x4_extract_bytes ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native ✅ 3s 3s +0%
keccakf1600x4_permute ✅ 3s 4s -25%
mld_ct_get_optblocker_u8 ✅ 3s 1s +200%
mld_h ✅ 3s 4s -25%
mld_keccakf1600_extract_bytes ✅ 3s 2s +50%
mld_keccakf1600_permute_c ✅ 3s 8s -62%
mld_sample_s1_s2 ✅ 3s 4s -25%
montgomery_reduce ✅ 3s 3s +0%
ntt_native_x86_64 ✅ 3s 3s +0%
pack_sig_c ✅ 3s 2s +50%
pointwise_native_aarch64 ✅ 3s 5s -40%
poly_caddq_native ✅ 3s 5s -40%
poly_chknorm_native_x86_64 ✅ 3s 2s +50%
poly_decompose_32_native_aarch64 ✅ 3s 2s +50%
poly_invntt_tomont_native ✅ 3s 4s -25%
poly_ntt_native ✅ 3s 5s -40%
poly_permute_bitrev_to_custom_optional ✅ 3s 2s +50%
poly_reduce ✅ 3s 3s +0%
poly_uniform ✅ 3s 6s -50%
poly_uniform_eta ✅ 3s 5s -40%
poly_uniform_gamma1_4x ✅ 3s 5s -40%
poly_use_hint_c ✅ 3s 3s +0%
poly_use_hint_native ✅ 3s 4s -25%
polyt1_pack ✅ 3s 4s -25%
polyt1_unpack ✅ 3s 5s -40%
polyveck_pack_eta ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery_native ✅ 3s 2s +50%
polyvecl_uniform_gamma1_serial ✅ 3s 2s +50%
polyvecl_unpack_eta ✅ 3s 2s +50%
polyw1_unpack_88 ✅ 3s - new
polyz_unpack_17_native_aarch64 ✅ 3s 5s -40%
polyz_unpack_native ✅ 3s 2s +50%
shake256x4_absorb_once ✅ 3s 3s +0%
sign_signature_extmu ✅ 3s 4s -25%
sign_signature_pre_hash_shake256 ✅ 3s 3s +0%
sign_verify ✅ 3s 4s -25%
sign_verify_extmu ✅ 3s 3s +0%
sign_verify_pre_hash_shake256 ✅ 3s 5s -40%
sk_s1hat_get_poly ✅ 3s 3s +0%
caddq ✅ 2s 2s +0%
decompose ✅ 2s 2s +0%
intt_native_x86_64 ✅ 2s 4s -50%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 ✅ 2s 3s -33%
keccak_squeeze ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native ✅ 2s 3s -33%
make_hint ✅ 2s 3s -33%
mld_ct_cmask_neg_i32 ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 ✅ 2s 2s +0%
mld_ct_cmask_nonzero_u8 ✅ 2s 2s +0%
mld_ct_get_optblocker_i64 ✅ 2s 4s -50%
mld_ct_get_optblocker_u32 ✅ 2s 1s +100%
mld_polymat_expand_entry ✅ 2s 3s -33%
mld_prepare_domain_separation_prefix ✅ 2s 4s -50%
mld_sample_s1_s2_serial ✅ 2s 3s -33%
mld_sign_finish ✅ 2s - new
mld_sign_resume ✅ 2s - new
mld_value_barrier_i64 ✅ 2s 2s +0%
mld_value_barrier_u32 ✅ 2s 2s +0%
mld_value_barrier_u8 ✅ 2s 3s -33%
nttunpack_native_x86_64 ✅ 2s 1s +100%
pack_sig_h ✅ 2s 3s -33%
pack_sig_z ✅ 2s 4s -50%
pointwise_acc_native_aarch64 ✅ 2s 4s -50%
pointwise_acc_native_x86_64 ✅ 2s 7s -71%
poly_add ✅ 2s 7s -71%
poly_caddq_native_aarch64 ✅ 2s 4s -50%
poly_caddq_native_x86_64 ✅ 2s 4s -50%
poly_challenge ✅ 2s 3s -33%
poly_chknorm ✅ 2s 4s -50%
poly_chknorm_native_aarch64 ✅ 2s 4s -50%
poly_decompose ✅ 2s 3s -33%
poly_decompose_c ✅ 2s 4s -50%
poly_decompose_native ✅ 2s 3s -33%
poly_ntt ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native ✅ 2s 4s -50%
poly_pointwise_montgomery ✅ 2s 3s -33%
poly_power2round ✅ 2s 4s -50%
poly_uniform_gamma1 ✅ 2s 4s -50%
poly_use_hint ✅ 2s 4s -50%
poly_use_hint_native_aarch64 ✅ 2s 2s +0%
poly_use_hint_native_x86_64 ✅ 2s - new
polyeta_pack ✅ 2s 3s -33%
polyt0_pack ✅ 2s 2s +0%
polyveck_ntt ✅ 2s 5s -60%
polyveck_reduce ✅ 2s 5s -60%
polyveck_unpack_eta ✅ 2s 2s +0%
polyvecl_ntt ✅ 2s 2s +0%
polyvecl_pack_eta ✅ 2s 3s -33%
polyw1_pack_32 ✅ 2s 2s +0%
polyw1_pack_88 ✅ 2s 1s +100%
polyw1_unpack_32 ✅ 2s - new
polyz_unpack ✅ 2s 3s -33%
polyz_unpack_native_x86_64 ✅ 2s 3s -33%
power2round ✅ 2s 3s -33%
rej_eta ✅ 2s 3s -33%
rej_uniform_eta_native_x86_64 ✅ 2s - new
rej_uniform_native_aarch64 ✅ 2s 5s -60%
shake128_init ✅ 2s 3s -33%
shake128_release ✅ 2s 1s +100%
shake128x4_absorb_once ✅ 2s 3s -33%
shake128x4_squeezeblocks ✅ 2s 1s +100%
shake256_finalize ✅ 2s 2s +0%
shake256_init ✅ 2s 3s -33%
shake256_release ✅ 2s 2s +0%
shake256_squeeze ✅ 2s 2s +0%
shake256x4_squeezeblocks ✅ 2s 4s -50%
sign_signature_pre_hash_internal ✅ 2s 6s -67%
sign_verify_pre_hash_internal ✅ 2s 3s -33%
unpack_sk ✅ 2s 3s -33%
unpack_sk_s1hat ✅ 2s 1s +100%
unpack_sk_s2hat ✅ 2s 4s -50%
unpack_sk_t0hat ✅ 2s 3s -33%
use_hint ✅ 2s 2s +0%
yvec_get_poly ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 1s 3s -67%
keccak_init ✅ 1s 3s -67%
keccakf1600_extract_bytes (big endian) ✅ 1s 2s -50%
keccakf1600_permute_native ✅ 1s 3s -67%
keccakf1600_xor_bytes ✅ 1s 1s +0%
keccakf1600x4_xor_bytes ✅ 1s 2s -50%
mld_ct_abs_i32 ✅ 1s 2s -50%
mld_ct_memcmp ✅ 1s 3s -67%
mld_ct_sel_int32 ✅ 1s 2s -50%
mld_keccakf1600x4_extract_bytes_c ✅ 1s 2s -50%
mld_keccakf1600x4_xor_bytes_c ✅ 1s 2s -50%
ntt_native_aarch64 ✅ 1s 3s -67%
pack_sk_rho_key_tr_s2 ✅ 1s 3s -67%
pointwise_native_x86_64 ✅ 1s 4s -75%
poly_caddq ✅ 1s 2s -50%
poly_caddq_c ✅ 1s 2s -50%
poly_decompose_native_x86_64 ✅ 1s 3s -67%
poly_invntt_tomont ✅ 1s 4s -75%
poly_pointwise_montgomery_native ✅ 1s 2s -50%
poly_shiftl ✅ 1s 3s -67%
poly_sub ✅ 1s 3s -67%
polyveck_invntt_tomont ✅ 1s 5s -80%
polyvecl_pointwise_acc_montgomery ✅ 1s 4s -75%
polyvecl_uniform_gamma1 ✅ 1s 3s -67%
polyvecl_unpack_z ✅ 1s 2s -50%
polyz_pack ✅ 1s 2s -50%
reduce32 ✅ 1s 2s -50%
rej_eta_c ✅ 1s 4s -75%
rej_eta_native ✅ 1s 6s -83%
shake128_finalize ✅ 1s 2s -50%
shake128_squeeze ✅ 1s 1s +0%
shake256_absorb ✅ 1s 3s -67%
sk_s2hat_get_poly ✅ 1s 2s -50%
sk_t0hat_get_poly ✅ 1s 2s -50%
sys_check_capability ✅ 1s 4s -75%
yvec_init ✅ 1s 3s -67%

@oqs-bot

oqs-bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 129s 13s +892%
mld_attempt_signature_generation ⚠️ 227s 63s +260%
sig_unpack_hints ⚠️ 28s 2s +1300%
sign_keypair_internal ⚠️ 26s 5s +420%
sign_pk_from_sk ⚠️ 51s 6s +750%
sign_signature_internal ⚠️ 195s 55s +255%
sign_verify_internal ⚠️ 319s 177s +80%
Full Results (212 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1960s 1784s +9.9%
sign_verify_internal ⚠️ 319s 177s +80%
mld_attempt_signature_generation ⚠️ 227s 63s +260%
sign_signature_internal ⚠️ 195s 55s +255%
polyvecl_pointwise_acc_montgomery_c ✅ 175s 210s -17%
compute_pack_t0_t1 ⚠️ 129s 13s +892%
polyvec_matrix_expand ✅ 78s 110s -29%
mld_invntt_layer ✅ 58s 109s -47%
sign_pk_from_sk ⚠️ 51s 6s +750%
poly_pointwise_montgomery_c ✅ 45s 125s -64%
sig_unpack_hints ⚠️ 28s 2s +1300%
sign_keypair_internal ⚠️ 26s 5s +420%
fqmul ✅ 24s 40s -40%
mld_ntt_layer ✅ 23s 41s -44%
polyvec_matrix_expand_serial ✅ 17s 27s -37%
mld_ntt_butterfly_block ✅ 13s 24s -46%
keccakf1600x4_permute_native ✅ 12s 23s -48%
polyvec_matrix_pointwise_montgomery_yvec ✅ 12s 18s -33%
rej_uniform ✅ 12s 18s -33%
poly_ntt_c ✅ 10s 19s -47%
rej_uniform_c ✅ 10s 14s -29%
poly_chknorm_c ✅ 8s 15s -47%
poly_uniform_4x ✅ 8s 13s -38%
rej_uniform_native_x86_64 ✅ 8s - new
poly_uniform_eta_4x ✅ 7s 14s -50%
poly_invntt_tomont_c ✅ 6s 11s -45%
polyt0_unpack ✅ 6s 16s -62%
polyveck_caddq ✅ 6s 6s +0%
keccak_absorb_once_x4 ✅ 5s 8s -38%
mld_check_pct ✅ 5s 14s -64%
mld_compute_pack_z ✅ 5s 7s -29%
poly_uniform_gamma1 ✅ 5s 3s +67%
polyvecl_chknorm ✅ 5s 7s -29%
polyvecl_uniform_gamma1_serial ✅ 5s 3s +67%
sign_keypair ✅ 5s 3s +67%
sign_signature_pre_hash_shake256 ✅ 5s 3s +67%
keccak_absorb ✅ 4s 3s +33%
keccak_init ✅ 4s 1s +300%
mld_keccakf1600_permute_c ✅ 4s 6s -33%
mld_sample_s1_s2 ✅ 4s 6s -33%
mld_sign_resume ✅ 4s - new
ntt_native_x86_64 ✅ 4s 2s +100%
pack_sig_h ✅ 4s 5s -20%
pack_sk_s1 ✅ 4s 5s -20%
pointwise_acc_native_x86_64 ✅ 4s 8s -50%
poly_decompose_32_native_aarch64 ✅ 4s 3s +33%
poly_invntt_tomont ✅ 4s 3s +33%
poly_power2round ✅ 4s 4s +0%
poly_use_hint ✅ 4s 3s +33%
poly_use_hint_c ✅ 4s 5s -20%
poly_use_hint_native_x86_64 ✅ 4s - new
polyveck_decompose_pack_w1 ✅ 4s - new
polyveck_ntt ✅ 4s 7s -43%
rej_uniform_eta_native_x86_64 ✅ 4s - new
rej_uniform_native_aarch64 ✅ 4s 3s +33%
sign_signature ✅ 4s 6s -33%
caddq ✅ 3s 3s +0%
intt_native_aarch64 ✅ 3s 3s +0%
intt_native_x86_64 ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64 ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 3s +0%
keccak_finalize ✅ 3s 2s +50%
keccak_squeezeblocks_x4 ✅ 3s 5s -40%
keccakf1600_xor_bytes ✅ 3s 2s +50%
mld_ct_abs_i32 ✅ 3s 2s +50%
mld_ct_cmask_neg_i32 ✅ 3s 2s +50%
mld_ct_memcmp ✅ 3s 2s +50%
mld_keccakf1600x4_extract_bytes_c ✅ 3s 3s +0%
mld_prepare_domain_separation_prefix ✅ 3s 2s +50%
mld_sign_finish ✅ 3s - new
montgomery_reduce ✅ 3s 4s -25%
ntt_native_aarch64 ✅ 3s 2s +50%
pack_sig_z ✅ 3s 2s +50%
pointwise_acc_native_aarch64 ✅ 3s 6s -50%
poly_add ✅ 3s 9s -67%
poly_caddq_c ✅ 3s 2s +50%
poly_caddq_native_x86_64 ✅ 3s 3s +0%
poly_chknorm_native_aarch64 ✅ 3s 3s +0%
poly_chknorm_native_x86_64 ✅ 3s 3s +0%
poly_decompose_native_x86_64 ✅ 3s 3s +0%
poly_invntt_tomont_native ✅ 3s 2s +50%
poly_permute_bitrev_to_custom_optional_native ✅ 3s 4s -25%
poly_shiftl ✅ 3s 3s +0%
poly_uniform ✅ 3s 4s -25%
poly_uniform_eta ✅ 3s 4s -25%
polyt0_pack ✅ 3s 3s +0%
polyvecl_ntt ✅ 3s 4s -25%
polyvecl_pack_eta ✅ 3s 3s +0%
polyvecl_uniform_gamma1 ✅ 3s 2s +50%
polyw1_unpack ✅ 3s - new
polyz_unpack_17_native_aarch64 ✅ 3s 3s +0%
polyz_unpack_c ✅ 3s 13s -77%
rej_eta_c ✅ 3s 5s -40%
rej_uniform_native ✅ 3s 4s -25%
shake128_finalize ✅ 3s 1s +200%
shake256_finalize ✅ 3s 1s +200%
shake256x4_squeezeblocks ✅ 3s 2s +50%
sign_verify_extmu ✅ 3s 3s +0%
sign_verify_pre_hash_internal ✅ 3s 5s -40%
sign_verify_pre_hash_shake256 ✅ 3s 5s -40%
sk_s1hat_get_poly ✅ 3s 6s -50%
sk_s2hat_get_poly ✅ 3s 2s +50%
unpack_sk_s1hat ✅ 3s 2s +50%
unpack_sk_t0hat ✅ 3s 5s -40%
yvec_get_poly ✅ 3s 3s +0%
fqscale ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 4s -50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 2s +0%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
keccak_squeeze ✅ 2s 4s -50%
keccakf1600_extract_bytes (big endian) ✅ 2s 2s +0%
keccakf1600_permute ✅ 2s 2s +0%
keccakf1600_permute_native ✅ 2s 3s -33%
keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
keccakf1600x4_extract_bytes ✅ 2s 4s -50%
keccakf1600x4_extract_bytes_native ✅ 2s 4s -50%
keccakf1600x4_permute ✅ 2s 4s -50%
keccakf1600x4_xor_bytes ✅ 2s 1s +100%
keccakf1600x4_xor_bytes_native ✅ 2s 3s -33%
make_hint ✅ 2s 2s +0%
mld_ct_get_optblocker_u8 ✅ 2s 2s +0%
mld_h ✅ 2s 2s +0%
mld_polymat_expand_entry ✅ 2s 4s -50%
mld_sample_s1_s2_serial ✅ 2s 4s -50%
mld_sign_attempt ✅ 2s - new
mld_value_barrier_u32 ✅ 2s 3s -33%
nttunpack_native_x86_64 ✅ 2s 3s -33%
pack_sig_c ✅ 2s 5s -60%
pack_sk_rho_key_tr_s2 ✅ 2s 2s +0%
pointwise_native_x86_64 ✅ 2s 3s -33%
poly_caddq ✅ 2s 2s +0%
poly_caddq_native ✅ 2s 2s +0%
poly_caddq_native_aarch64 ✅ 2s 2s +0%
poly_challenge ✅ 2s 6s -67%
poly_chknorm_native ✅ 2s 2s +0%
poly_decompose ✅ 2s 2s +0%
poly_ntt ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional ✅ 2s 2s +0%
poly_pointwise_montgomery ✅ 2s 3s -33%
poly_pointwise_montgomery_native ✅ 2s 3s -33%
poly_reduce ✅ 2s 3s -33%
poly_use_hint_native ✅ 2s 2s +0%
poly_use_hint_native_aarch64 ✅ 2s 3s -33%
polyeta_pack ✅ 2s 3s -33%
polyeta_unpack ✅ 2s 8s -75%
polyt1_unpack ✅ 2s 5s -60%
polyveck_chknorm ✅ 2s 6s -67%
polyveck_invntt_tomont ✅ 2s 8s -75%
polyveck_pack_eta ✅ 2s 4s -50%
polyveck_reduce ✅ 2s 4s -50%
polyveck_unpack_eta ✅ 2s 6s -67%
polyw1_pack ✅ 2s 4s -50%
polyw1_pack_32 ✅ 2s 4s -50%
polyw1_unpack_32 ✅ 2s - new
polyw1_unpack_88 ✅ 2s - new
polyz_pack ✅ 2s 3s -33%
polyz_unpack ✅ 2s 3s -33%
polyz_unpack_19_native_aarch64 ✅ 2s 3s -33%
polyz_unpack_native ✅ 2s 4s -50%
rej_eta ✅ 2s 2s +0%
shake128_absorb ✅ 2s 2s +0%
shake128_init ✅ 2s 2s +0%
shake128_release ✅ 2s 3s -33%
shake128_squeeze ✅ 2s 2s +0%
shake128x4_squeezeblocks ✅ 2s 3s -33%
shake256 ✅ 2s 2s +0%
shake256_init ✅ 2s 2s +0%
shake256_release ✅ 2s 2s +0%
shake256_squeeze ✅ 2s 3s -33%
shake256x4_absorb_once ✅ 2s 3s -33%
sign_signature_extmu ✅ 2s 2s +0%
sign_signature_pre_hash_internal ✅ 2s 3s -33%
sign_verify ✅ 2s 3s -33%
sk_t0hat_get_poly ✅ 2s 2s +0%
sys_check_capability ✅ 2s 4s -50%
unpack_pk_t1 ✅ 2s 5s -60%
decompose ✅ 1s 1s +0%
mld_ct_cmask_nonzero_u32 ✅ 1s 4s -75%
mld_ct_cmask_nonzero_u8 ✅ 1s 3s -67%
mld_ct_get_optblocker_i64 ✅ 1s 2s -50%
mld_ct_get_optblocker_u32 ✅ 1s 3s -67%
mld_ct_sel_int32 ✅ 1s 3s -67%
mld_keccakf1600_extract_bytes ✅ 1s 1s +0%
mld_keccakf1600x4_xor_bytes_c ✅ 1s 2s -50%
mld_value_barrier_i64 ✅ 1s 2s -50%
mld_value_barrier_u8 ✅ 1s 3s -67%
pointwise_native_aarch64 ✅ 1s 5s -80%
poly_chknorm ✅ 1s 4s -75%
poly_decompose_88_native_aarch64 ✅ 1s 1s +0%
poly_decompose_c ✅ 1s 5s -80%
poly_decompose_native ✅ 1s 3s -67%
poly_ntt_native ✅ 1s 4s -75%
poly_sub ✅ 1s 3s -67%
poly_uniform_gamma1_4x ✅ 1s 4s -75%
polyt1_pack ✅ 1s 3s -67%
polyvec_matrix_pointwise_montgomery_row ✅ 1s 1s +0%
polyvecl_pointwise_acc_montgomery ✅ 1s 3s -67%
polyvecl_pointwise_acc_montgomery_native ✅ 1s 2s -50%
polyvecl_unpack_eta ✅ 1s 3s -67%
polyvecl_unpack_z ✅ 1s 3s -67%
polyw1_pack_88 ✅ 1s 2s -50%
polyz_unpack_native_x86_64 ✅ 1s 3s -67%
power2round ✅ 1s 1s +0%
reduce32 ✅ 1s 3s -67%
rej_eta_native ✅ 1s 3s -67%
rej_uniform_eta_native_aarch64 ✅ 1s 4s -75%
shake128x4_absorb_once ✅ 1s 3s -67%
shake256_absorb ✅ 1s 2s -50%
unpack_sk ✅ 1s 3s -67%
unpack_sk_s2hat ✅ 1s 4s -75%
use_hint ✅ 1s 2s -50%
yvec_init ✅ 1s 3s -67%

@oqs-bot

oqs-bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof Status Current Previous Change
compute_pack_t0_t1 ⚠️ 202s 19s +963%
mld_attempt_signature_generation ⚠️ 270s 55s +391%
sig_unpack_hints ⚠️ 29s 3s +867%
sign_keypair_internal ⚠️ 42s 6s +600%
sign_pk_from_sk ⚠️ 69s 6s +1050%
sign_signature_internal ⚠️ 335s 42s +698%
sign_verify_internal ⚠️ 545s 97s +462%
Full Results (212 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 2574s 2151s +19.7%
sign_verify_internal ⚠️ 545s 97s +462%
sign_signature_internal ⚠️ 335s 42s +698%
mld_attempt_signature_generation ⚠️ 270s 55s +391%
polyvecl_pointwise_acc_montgomery_c ✅ 233s 353s -34%
compute_pack_t0_t1 ⚠️ 202s 19s +963%
polyvec_matrix_expand ✅ 84s 324s -74%
sign_pk_from_sk ⚠️ 69s 6s +1050%
mld_invntt_layer ✅ 60s 115s -48%
poly_pointwise_montgomery_c ✅ 45s 144s -69%
sign_keypair_internal ⚠️ 42s 6s +600%
sig_unpack_hints ⚠️ 29s 3s +867%
mld_ntt_layer ✅ 23s 45s -49%
fqmul ✅ 22s 43s -49%
polyvec_matrix_expand_serial ✅ 22s 38s -42%
keccakf1600x4_permute_native ✅ 14s 23s -39%
poly_ntt_c ✅ 12s 21s -43%
poly_uniform_eta_4x ✅ 12s 11s +9%
rej_uniform ✅ 12s 15s -20%
mld_ntt_butterfly_block ✅ 11s 24s -54%
polyvec_matrix_pointwise_montgomery_yvec ✅ 10s 18s -44%
rej_uniform_c ✅ 9s 19s -53%
poly_invntt_tomont_c ✅ 8s 12s -33%
polyt0_unpack ✅ 8s 14s -43%
rej_uniform_native_x86_64 ✅ 8s - new
poly_chknorm_c ✅ 7s 15s -53%
poly_uniform_4x ✅ 7s 13s -46%
polyveck_caddq ✅ 7s 8s -12%
polyveck_decompose_pack_w1 ✅ 7s - new
poly_add ✅ 6s 6s +0%
polyeta_unpack ✅ 6s 17s -65%
sign_keypair ✅ 6s 4s +50%
mld_compute_pack_z ✅ 5s 8s -38%
poly_decompose_88_native_aarch64 ✅ 5s 2s +150%
poly_power2round ✅ 5s 3s +67%
poly_shiftl ✅ 5s 4s +25%
poly_use_hint_native ✅ 5s 3s +67%
polyveck_invntt_tomont ✅ 5s 9s -44%
polyz_unpack_c ✅ 5s 3s +67%
shake256_absorb ✅ 5s 2s +150%
unpack_sk_s1hat ✅ 5s 2s +150%
keccak_absorb ✅ 4s 3s +33%
keccak_absorb_once_x4 ✅ 4s 9s -56%
keccak_squeeze ✅ 4s 2s +100%
keccak_squeezeblocks_x4 ✅ 4s 4s +0%
keccakf1600_permute ✅ 4s 3s +33%
mld_check_pct ✅ 4s 16s -75%
mld_ct_cmask_neg_i32 ✅ 4s 4s +0%
mld_ct_sel_int32 ✅ 4s 3s +33%
mld_keccakf1600_permute_c ✅ 4s 7s -43%
mld_sample_s1_s2 ✅ 4s 6s -33%
mld_sample_s1_s2_serial ✅ 4s 8s -50%
pointwise_acc_native_aarch64 ✅ 4s 6s -33%
pointwise_acc_native_x86_64 ✅ 4s 6s -33%
poly_challenge ✅ 4s 5s -20%
poly_chknorm_native_aarch64 ✅ 4s 4s +0%
poly_decompose ✅ 4s 3s +33%
poly_invntt_tomont ✅ 4s 1s +300%
poly_reduce ✅ 4s 2s +100%
poly_uniform_gamma1_4x ✅ 4s 3s +33%
poly_use_hint_native_aarch64 ✅ 4s 2s +100%
polyw1_pack ✅ 4s 4s +0%
rej_eta ✅ 4s 4s +0%
rej_eta_native ✅ 4s 6s -33%
sign_signature ✅ 4s 5s -20%
sign_signature_pre_hash_internal ✅ 4s 5s -20%
sign_signature_pre_hash_shake256 ✅ 4s 6s -33%
sign_verify_pre_hash_shake256 ✅ 4s 3s +33%
decompose ✅ 3s 3s +0%
intt_native_aarch64 ✅ 3s 3s +0%
intt_native_x86_64 ✅ 3s 3s +0%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 1s +200%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 3s +0%
keccak_f1600_x4_native_avx2 ✅ 3s 2s +50%
make_hint ✅ 3s 3s +0%
mld_ct_abs_i32 ✅ 3s 3s +0%
mld_ct_get_optblocker_i64 ✅ 3s 3s +0%
mld_prepare_domain_separation_prefix ✅ 3s 4s -25%
mld_sign_finish ✅ 3s - new
mld_sign_resume ✅ 3s - new
mld_value_barrier_i64 ✅ 3s 1s +200%
mld_value_barrier_u32 ✅ 3s 2s +50%
ntt_native_x86_64 ✅ 3s 2s +50%
pack_sig_h ✅ 3s 4s -25%
pointwise_native_aarch64 ✅ 3s 5s -40%
poly_caddq_c ✅ 3s 3s +0%
poly_caddq_native ✅ 3s 4s -25%
poly_decompose_32_native_aarch64 ✅ 3s 5s -40%
poly_pointwise_montgomery ✅ 3s 4s -25%
poly_uniform ✅ 3s 4s -25%
poly_use_hint_c ✅ 3s 2s +50%
polyeta_pack ✅ 3s 4s -25%
polyveck_ntt ✅ 3s 11s -73%
polyveck_unpack_eta ✅ 3s 4s -25%
polyvecl_chknorm ✅ 3s 7s -57%
polyvecl_ntt ✅ 3s 7s -57%
polyw1_pack_32 ✅ 3s 4s -25%
polyw1_unpack ✅ 3s - new
polyz_pack ✅ 3s 5s -40%
polyz_unpack_native ✅ 3s 4s -25%
power2round ✅ 3s 4s -25%
rej_uniform_eta_native_aarch64 ✅ 3s 5s -40%
rej_uniform_eta_native_x86_64 ✅ 3s - new
rej_uniform_native ✅ 3s 8s -62%
shake128_finalize ✅ 3s 2s +50%
shake128_squeeze ✅ 3s 2s +50%
shake128x4_absorb_once ✅ 3s 5s -40%
shake128x4_squeezeblocks ✅ 3s 3s +0%
sign_signature_extmu ✅ 3s 4s -25%
sign_verify ✅ 3s 5s -40%
sk_s2hat_get_poly ✅ 3s 3s +0%
sk_t0hat_get_poly ✅ 3s 4s -25%
unpack_sk_t0hat ✅ 3s 7s -57%
use_hint ✅ 3s 3s +0%
caddq ✅ 2s 4s -50%
fqscale ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 ✅ 2s 1s +100%
keccakf1600_extract_bytes (big endian) ✅ 2s 3s -33%
keccakf1600x4_extract_bytes_native ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native ✅ 2s 3s -33%
mld_ct_get_optblocker_u32 ✅ 2s 2s +0%
mld_ct_memcmp ✅ 2s 3s -33%
mld_h ✅ 2s 3s -33%
mld_keccakf1600_extract_bytes ✅ 2s 4s -50%
mld_polymat_expand_entry ✅ 2s 3s -33%
mld_value_barrier_u8 ✅ 2s 3s -33%
ntt_native_aarch64 ✅ 2s 6s -67%
pack_sk_rho_key_tr_s2 ✅ 2s 3s -33%
pack_sk_s1 ✅ 2s 1s +100%
pointwise_native_x86_64 ✅ 2s 2s +0%
poly_chknorm_native_x86_64 ✅ 2s 2s +0%
poly_decompose_native_x86_64 ✅ 2s 2s +0%
poly_ntt ✅ 2s 3s -33%
poly_ntt_native ✅ 2s 3s -33%
poly_permute_bitrev_to_custom_optional_native ✅ 2s 5s -60%
poly_pointwise_montgomery_native ✅ 2s 5s -60%
poly_uniform_eta ✅ 2s 4s -50%
poly_use_hint ✅ 2s 1s +100%
polyt1_unpack ✅ 2s 4s -50%
polyvec_matrix_pointwise_montgomery_row ✅ 2s 3s -33%
polyveck_chknorm ✅ 2s 3s -33%
polyveck_reduce ✅ 2s 3s -33%
polyvecl_pack_eta ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery ✅ 2s 5s -60%
polyvecl_pointwise_acc_montgomery_native ✅ 2s 3s -33%
polyvecl_uniform_gamma1 ✅ 2s 2s +0%
polyvecl_uniform_gamma1_serial ✅ 2s 4s -50%
polyvecl_unpack_eta ✅ 2s 5s -60%
polyvecl_unpack_z ✅ 2s 4s -50%
polyw1_unpack_32 ✅ 2s - new
polyz_unpack ✅ 2s 2s +0%
polyz_unpack_19_native_aarch64 ✅ 2s 4s -50%
rej_eta_c ✅ 2s 5s -60%
rej_uniform_native_aarch64 ✅ 2s 2s +0%
shake128_absorb ✅ 2s 4s -50%
shake128_release ✅ 2s 4s -50%
shake256_finalize ✅ 2s 2s +0%
shake256_release ✅ 2s 3s -33%
shake256_squeeze ✅ 2s 2s +0%
shake256x4_absorb_once ✅ 2s 2s +0%
shake256x4_squeezeblocks ✅ 2s 1s +100%
sign_verify_extmu ✅ 2s 3s -33%
sign_verify_pre_hash_internal ✅ 2s 3s -33%
sys_check_capability ✅ 2s 3s -33%
unpack_sk_s2hat ✅ 2s 3s -33%
yvec_get_poly ✅ 2s 4s -50%
yvec_init ✅ 2s 4s -50%
keccak_f1600_x4_native_aarch64_v84a ✅ 1s 4s -75%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 1s 4s -75%
keccak_finalize ✅ 1s 1s +0%
keccak_init ✅ 1s 3s -67%
keccakf1600_permute_native ✅ 1s 4s -75%
keccakf1600_xor_bytes ✅ 1s 3s -67%
keccakf1600_xor_bytes (big endian) ✅ 1s 2s -50%
keccakf1600x4_extract_bytes ✅ 1s 2s -50%
keccakf1600x4_permute ✅ 1s 3s -67%
keccakf1600x4_xor_bytes ✅ 1s 3s -67%
mld_ct_cmask_nonzero_u32 ✅ 1s 2s -50%
mld_ct_cmask_nonzero_u8 ✅ 1s 3s -67%
mld_ct_get_optblocker_u8 ✅ 1s 3s -67%
mld_keccakf1600x4_extract_bytes_c ✅ 1s 2s -50%
mld_keccakf1600x4_xor_bytes_c ✅ 1s 4s -75%
mld_sign_attempt ✅ 1s - new
montgomery_reduce ✅ 1s 3s -67%
nttunpack_native_x86_64 ✅ 1s 3s -67%
pack_sig_c ✅ 1s 4s -75%
pack_sig_z ✅ 1s 5s -80%
poly_caddq ✅ 1s 2s -50%
poly_caddq_native_aarch64 ✅ 1s 3s -67%
poly_caddq_native_x86_64 ✅ 1s 2s -50%
poly_chknorm ✅ 1s 3s -67%
poly_chknorm_native ✅ 1s 4s -75%
poly_decompose_c ✅ 1s 5s -80%
poly_decompose_native ✅ 1s 2s -50%
poly_invntt_tomont_native ✅ 1s 5s -80%
poly_permute_bitrev_to_custom_optional ✅ 1s 3s -67%
poly_sub ✅ 1s 3s -67%
poly_uniform_gamma1 ✅ 1s 4s -75%
poly_use_hint_native_x86_64 ✅ 1s - new
polyt0_pack ✅ 1s 4s -75%
polyt1_pack ✅ 1s 3s -67%
polyveck_pack_eta ✅ 1s 6s -83%
polyw1_pack_88 ✅ 1s 3s -67%
polyw1_unpack_88 ✅ 1s - new
polyz_unpack_17_native_aarch64 ✅ 1s 3s -67%
polyz_unpack_native_x86_64 ✅ 1s 3s -67%
reduce32 ✅ 1s 3s -67%
shake128_init ✅ 1s 1s +0%
shake256 ✅ 1s 2s -50%
shake256_init ✅ 1s 2s -50%
sk_s1hat_get_poly ✅ 1s 3s -67%
unpack_pk_t1 ✅ 1s 1s +0%
unpack_sk ✅ 1s 5s -80%

hanno-becker
hanno-becker approved these changes Sep 2, 2026
View reviewed changes

@hanno-becker hanno-becker left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thank you @mkannwischer for getting to the bottom of this. I agree with the fixes and also tested the script locally, confirming that it does break when proposing invalid explanations for small-digit constants.

@hanno-becker
hanno-becker added this pull request to the merge queue Sep 2, 2026
Merged via the queue into main with commit 19d3261 Sep 2, 2026
402 checks passed
@hanno-becker
hanno-becker deleted the check-magic-packed-bytes branch September 2, 2026 05:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hanno-becker hanno-becker hanno-becker approved these changes

Assignees

No one assigned

Labels

needs-mlkem-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkannwischer @oqs-bot @hanno-becker