Skip to content

Make ML-DSA SHAKE finalization idempotent#1243

Open
tob-joe wants to merge 2 commits into
mainfrom
ptp/mldsa-make-shake-finalize-idempotent
Open

Make ML-DSA SHAKE finalization idempotent#1243
tob-joe wants to merge 2 commits into
mainfrom
ptp/mldsa-make-shake-finalize-idempotent

Conversation

@tob-joe

@tob-joe tob-joe commented Jun 29, 2026 •
edited
Loading

Copy link
Copy Markdown

Summary

  • make consecutive ML-DSA SHAKE128/SHAKE256 finalize calls harmless before squeezing
  • tighten the internal Keccak finalize precondition and use MLD_MAX_BUFFER_SIZE for XOF proof-contract bounds
  • add regression test coverage for one-finalize versus two-finalize SHAKE output across boundary absorb lengths

Rationale

This is narrow misuse resistance for the built-in incremental FIPS202 implementation. The SHAKE helpers are internal, but they have external linkage by default and sit behind helper boundaries where names such as *_absorb_once already include finalization before later squeezing. A maintainer adding an explicit finalize at such a boundary should not silently corrupt the state by applying the Keccak delimiter twice.

This does not change the intended absorb/finalize/squeeze lifecycle, does not make absorb-after-finalize valid, and does not claim to cover finalizing again after squeezing has begun.

Testing

  • make clean run_unit
  • nix develop --command python3 scripts/autogen --dry-run

Co-authored-by: Codex [email protected]
Signed-off-by: Joe Doyle [email protected]

This work was completed by Trail of Bits as part of the Patch The Planet project in collaboration with OpenAI. The issue was identified primarily by the Codex coding agent, and manually reviewed before submission.

@tob-joe tob-joe requested a review from a team as a code owner June 29, 2026 19:08
@oqs-bot

oqs-bot commented Jun 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

Full Results (205 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1636s 1482s +10.4%
polyvec_matrix_pointwise_montgomery_yvec ✅ 226s 201s +12%
poly_pointwise_montgomery_c ✅ 150s 116s +29%
mld_invntt_layer ✅ 127s 108s +18%
sign_verify_internal ✅ 76s 71s +7%
mld_ntt_layer ✅ 48s 43s +12%
polyvecl_chknorm ✅ 48s 43s +12%
fqmul ✅ 45s 40s +12%
polyveck_chknorm ✅ 37s 36s +3%
mld_attempt_signature_generation ✅ 35s 31s +13%
mld_ntt_butterfly_block ✅ 26s 25s +4%
poly_ntt_c ✅ 26s 22s +18%
keccakf1600x4_permute_native ✅ 23s 22s +5%
rej_uniform_c ✅ 18s 16s +12%
poly_chknorm_c ✅ 15s 13s +15%
mld_check_pct ✅ 13s 12s +8%
poly_invntt_tomont_c ✅ 13s 10s +30%
poly_uniform_eta_4x ✅ 13s 13s +0%
polyt0_unpack ✅ 13s 13s +0%
polyveck_decompose ✅ 12s 14s -14%
keccak_absorb_once_x4 ✅ 11s 10s +10%
polyvec_matrix_pointwise_montgomery_row ✅ 10s 8s +25%
rej_uniform ✅ 10s 7s +43%
polyveck_reduce ✅ 9s 6s +50%
polyvecl_ntt ✅ 9s 7s +29%
compute_pack_t0_t1 ✅ 8s 7s +14%
mld_keccakf1600_permute_c ✅ 8s 7s +14%
poly_decompose_c ✅ 8s 8s +0%
polyveck_invntt_tomont ✅ 8s 7s +14%
polyz_unpack_c ✅ 8s 9s -11%
pointwise_acc_native_x86_64 ✅ 7s 5s +40%
poly_add ✅ 7s 7s +0%
poly_use_hint ✅ 7s 3s +133%
polyveck_caddq ✅ 7s 7s +0%
sign_pk_from_sk ✅ 7s 5s +40%
keccakf1600_permute ✅ 6s 4s +50%
mld_compute_pack_z ✅ 6s 5s +20%
pack_sig_c ✅ 6s 3s +100%
pointwise_acc_native_aarch64 ✅ 6s 6s +0%
poly_reduce ✅ 6s 4s +50%
poly_uniform ✅ 6s 2s +200%
rej_uniform_native ✅ 6s 4s +50%
sign_signature_extmu ✅ 6s 4s +50%
sign_verify_pre_hash_internal ✅ 6s 5s +20%
keccak_absorb ✅ 5s 3s +67%
mld_ct_cmask_neg_i32 ✅ 5s 3s +67%
mld_ct_cmask_nonzero_u8 ✅ 5s 2s +150%
mld_keccakf1600x4_xor_bytes_c ✅ 5s 2s +150%
mld_sample_s1_s2 ✅ 5s 6s -17%
mld_sample_s1_s2_serial ✅ 5s 3s +67%
ntt_native_x86_64 ✅ 5s 5s +0%
poly_permute_bitrev_to_custom_optional ✅ 5s 3s +67%
polyveck_pack_w1 ✅ 5s 4s +25%
polyw1_pack ✅ 5s 3s +67%
polyw1_pack_32 ✅ 5s 2s +150%
sign_keypair ✅ 5s 4s +25%
sign_keypair_internal ✅ 5s 3s +67%
sign_verify ✅ 5s 6s -17%
sign_verify_pre_hash_shake256 ✅ 5s 6s -17%
use_hint ✅ 5s 2s +150%
yvec_get_poly ✅ 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 4s 3s +33%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 4s 3s +33%
keccak_squeezeblocks_x4 ✅ 4s 4s +0%
keccakf1600_extract_bytes (big endian) ✅ 4s 3s +33%
keccakf1600_xor_bytes ✅ 4s 4s +0%
keccakf1600x4_extract_bytes ✅ 4s 4s +0%
keccakf1600x4_permute ✅ 4s 1s +300%
mld_prepare_domain_separation_prefix ✅ 4s 4s +0%
ntt_native_aarch64 ✅ 4s 3s +33%
nttunpack_native_x86_64 ✅ 4s 3s +33%
pack_sk_rho_key_tr_s2 ✅ 4s 2s +100%
pointwise_native_aarch64 ✅ 4s 3s +33%
pointwise_native_x86_64 ✅ 4s 2s +100%
poly_caddq_native_x86_64 ✅ 4s 1s +300%
poly_chknorm ✅ 4s 3s +33%
poly_chknorm_native ✅ 4s 4s +0%
poly_decompose_88_native_aarch64 ✅ 4s 2s +100%
poly_decompose_native_x86_64 ✅ 4s 2s +100%
poly_invntt_tomont ✅ 4s 5s -20%
poly_ntt_native ✅ 4s 2s +100%
poly_shiftl ✅ 4s 3s +33%
poly_uniform_gamma1_4x ✅ 4s 3s +33%
polyt0_pack ✅ 4s 5s -20%
polyt1_pack ✅ 4s 3s +33%
polyvec_matrix_expand_serial ✅ 4s 3s +33%
polyvecl_pointwise_acc_montgomery_native ✅ 4s 3s +33%
polyvecl_unpack_eta ✅ 4s 2s +100%
polyvecl_unpack_z ✅ 4s 1s +300%
polyw1_pack_88 ✅ 4s 3s +33%
polyz_unpack_19_native_aarch64 ✅ 4s 5s -20%
rej_eta_c ✅ 4s 4s +0%
rej_uniform_eta_native_aarch64 ✅ 4s 5s -20%
sign_signature ✅ 4s 5s -20%
sign_signature_internal ✅ 4s 6s -33%
sign_signature_pre_hash_internal ✅ 4s 3s +33%
sign_verify_extmu ✅ 4s 2s +100%
sk_s2hat_get_poly ✅ 4s 1s +300%
sk_t0hat_get_poly ✅ 4s 1s +300%
intt_native_aarch64 ✅ 3s 2s +50%
intt_native_x86_64 ✅ 3s 4s -25%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v84a ✅ 3s 2s +50%
keccak_init ✅ 3s 4s -25%
keccak_squeeze ✅ 3s 2s +50%
keccakf1600x4_xor_bytes_native ✅ 3s 2s +50%
mld_ct_get_optblocker_u32 ✅ 3s 3s +0%
mld_ct_get_optblocker_u8 ✅ 3s 4s -25%
mld_ct_memcmp ✅ 3s 4s -25%
mld_h ✅ 3s 3s +0%
mld_keccakf1600x4_extract_bytes_c ✅ 3s 2s +50%
mld_value_barrier_u32 ✅ 3s 4s -25%
mld_value_barrier_u8 ✅ 3s 1s +200%
montgomery_reduce ✅ 3s 1s +200%
pack_sig_h ✅ 3s 2s +50%
poly_caddq ✅ 3s 3s +0%
poly_caddq_c ✅ 3s 5s -40%
poly_challenge ✅ 3s 5s -40%
poly_decompose_32_native_aarch64 ✅ 3s 4s -25%
poly_decompose_native ✅ 3s 5s -40%
poly_invntt_tomont_native ✅ 3s 5s -40%
poly_power2round ✅ 3s 7s -57%
poly_sub ✅ 3s 4s -25%
poly_use_hint_c ✅ 3s 2s +50%
poly_use_hint_native_aarch64 ✅ 3s 4s -25%
polyeta_unpack ✅ 3s 4s -25%
polyt1_unpack ✅ 3s 3s +0%
polyveck_ntt ✅ 3s 4s -25%
polyveck_unpack_eta ✅ 3s 3s +0%
polyvecl_pack_eta ✅ 3s 2s +50%
polyvecl_pointwise_acc_montgomery_c ✅ 3s 3s +0%
polyvecl_uniform_gamma1 ✅ 3s 4s -25%
polyz_pack ✅ 3s 3s +0%
polyz_unpack_17_native_aarch64 ✅ 3s 2s +50%
rej_eta_native ✅ 3s 3s +0%
rej_uniform_native_aarch64 ✅ 3s 5s -40%
shake128_finalize ✅ 3s 2s +50%
shake128_init ✅ 3s 6s -50%
shake128_squeeze ✅ 3s 3s +0%
shake128x4_absorb_once ✅ 3s 2s +50%
shake256_finalize ✅ 3s 1s +200%
shake256_squeeze ✅ 3s 4s -25%
sign_signature_pre_hash_shake256 ✅ 3s 7s -57%
sk_s1hat_get_poly ✅ 3s 3s +0%
unpack_pk_t1 ✅ 3s 2s +50%
unpack_sk ✅ 3s 3s +0%
unpack_sk_s1hat ✅ 3s 1s +200%
unpack_sk_s2hat ✅ 3s 3s +0%
yvec_init ✅ 3s 5s -40%
caddq ✅ 2s 2s +0%
decompose ✅ 2s 4s -50%
fqscale ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
keccak_finalize ✅ 2s 2s +0%
keccakf1600_permute_native ✅ 2s 2s +0%
keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native ✅ 2s 1s +100%
keccakf1600x4_xor_bytes ✅ 2s 2s +0%
make_hint ✅ 2s 3s -33%
mld_ct_cmask_nonzero_u32 ✅ 2s 3s -33%
mld_ct_get_optblocker_i64 ✅ 2s 1s +100%
mld_keccakf1600_extract_bytes ✅ 2s 2s +0%
mld_polymat_expand_entry ✅ 2s 3s -33%
mld_value_barrier_i64 ✅ 2s 2s +0%
pack_sig_z ✅ 2s 1s +100%
pack_sk_s1 ✅ 2s 3s -33%
poly_caddq_native_aarch64 ✅ 2s 2s +0%
poly_chknorm_native_aarch64 ✅ 2s 2s +0%
poly_chknorm_native_x86_64 ✅ 2s 4s -50%
poly_decompose ✅ 2s 2s +0%
poly_ntt ✅ 2s 2s +0%
poly_permute_bitrev_to_custom_optional_native ✅ 2s 3s -33%
poly_pointwise_montgomery ✅ 2s 2s +0%
poly_pointwise_montgomery_native ✅ 2s 4s -50%
poly_uniform_4x ✅ 2s 4s -50%
poly_uniform_eta ✅ 2s 5s -60%
poly_uniform_gamma1 ✅ 2s 3s -33%
poly_use_hint_native ✅ 2s 7s -71%
poly_use_hint_native_x86_64 ✅ 2s - new
polyvec_matrix_expand ✅ 2s 6s -67%
polyveck_pack_eta ✅ 2s 3s -33%
polyvecl_pointwise_acc_montgomery ✅ 2s 3s -33%
polyvecl_uniform_gamma1_serial ✅ 2s 1s +100%
polyz_unpack_native ✅ 2s 3s -33%
polyz_unpack_native_x86_64 ✅ 2s 3s -33%
power2round ✅ 2s 2s +0%
reduce32 ✅ 2s 2s +0%
rej_eta ✅ 2s 5s -60%
shake128_absorb ✅ 2s 2s +0%
shake128x4_squeezeblocks ✅ 2s 2s +0%
shake256 ✅ 2s 2s +0%
shake256_absorb ✅ 2s 4s -50%
shake256_init ✅ 2s 4s -50%
shake256_release ✅ 2s 3s -33%
shake256x4_absorb_once ✅ 2s 2s +0%
shake256x4_squeezeblocks ✅ 2s 2s +0%
sig_unpack_hints ✅ 2s 1s +100%
unpack_sk_t0hat ✅ 2s 4s -50%
mld_ct_abs_i32 ✅ 1s 6s -83%
mld_ct_sel_int32 ✅ 1s 2s -50%
poly_caddq_native ✅ 1s 4s -75%
polyeta_pack ✅ 1s 1s +0%
polyz_unpack ✅ 1s 3s -67%
shake128_release ✅ 1s 2s -50%
sys_check_capability ✅ 1s 1s +0%

@oqs-bot

oqs-bot commented Jun 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

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

@oqs-bot

oqs-bot commented Jun 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

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

@oqs-bot

oqs-bot commented Jun 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

@oqs-bot

oqs-bot commented Jun 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

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

@oqs-bot

oqs-bot commented Jun 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

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

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

mkannwischer
mkannwischer reviewed Jun 30, 2026
View reviewed changes

@mkannwischer mkannwischer left a comment •
edited
Loading

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.

Thanks @tob-joe. Could you elaborate what is the motivation for this change?
This is an internal function that we are not exposing to consumers.
I'm not convinced that we need to make internal functions misuse resistant.

@tob-joe tob-joe force-pushed the ptp/mldsa-make-shake-finalize-idempotent branch from 4a93f59 to 157f66e Compare July 5, 2026 23:52
tob-joe and others added 2 commits July 7, 2026 17:18
@tob-joe @codex
Make ML-DSA SHAKE finalization idempotent
44bf3f1 
Skip Keccak finalization when SHAKE128 or SHAKE256 state is already finalized,
tighten the internal finalize precondition, and replace arbitrary XOF
proof-contract bounds with MLD_MAX_BUFFER_SIZE.

Add regression test coverage comparing one-finalize and two-finalize
SHAKE128/SHAKE256 output across boundary absorb lengths.

Verification:

- pre-fix targeted test failed with ERROR (test/src/test_unit.c,113)
- make -j1 run_unit_44
- scripts/autogen

Co-authored-by: Codex <[email protected]>
Signed-off-by: Joe Doyle <[email protected]>
@tob-joe @codex
Restore bounded ML-DSA x4 squeeze contracts
1913190 
Keep the idempotent SHAKE finalization change, but restore the prior small CBMC contract bound on the four-way squeeze helpers. The broader symbolic nblocks bound is not needed for this PR and causes the keccak_squeezeblocks_x4 proof to time out across the CBMC matrix.

Verification:

- ./scripts/tests cbmc -kl 44 -p keccak_squeezeblocks_x4 --per-proof-timeout 600 -f -v

- ./scripts/tests cbmc -kl 44 -p keccak_squeezeblocks_x4 --per-proof-timeout 600 -f -v --reduce-ram

- lint

Co-authored-by: Codex <[email protected]>
Signed-off-by: Joe Doyle <[email protected]>
@tob-joe tob-joe force-pushed the ptp/mldsa-make-shake-finalize-idempotent branch from 157f66e to 1913190 Compare July 7, 2026 21:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tob-joe @oqs-bot @mkannwischer