Skip to content

CBMC: Functional specs for make_hint and hint unpacking#1287

Draft
mkannwischer wants to merge 1 commit into
mainfrom
cbmc-hint-functional-specs
Draft

CBMC: Functional specs for make_hint and hint unpacking#1287
mkannwischer wants to merge 1 commit into
mainfrom
cbmc-hint-functional-specs

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

Strengthen the contracts beyond type/memory safety: pin mld_make_hint's return value to the exact hint predicate, and prove mld_sig_unpack_hints sets h->coeffs[p] exactly for the hint indices decoded for row i.

@oqs-bot

oqs-bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

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

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-87)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-44)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 15, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-DSA-65)

⚠️ Attention Required

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

@hanno-becker

hanno-becker commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

I support strengthening the functional specification as much as CBMC allows. However, we need to find a way around the unnecessary complexity it imposes on caller that don't care about the added functional properties. Perhaps there is a (clean) way one can mark ensures clauses as "check-only", so they are taken into account when the contract is validated, but ignored when the contract is used. That would be sound.

@mkannwischer

mkannwischer commented Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

I support strengthening the functional specification as much as CBMC allows. However, we need to find a way around the unnecessary complexity it imposes on caller that don't care about the added functional properties. Perhaps there is a (clean) way one can mark ensures clauses as "check-only", so they are taken into account when the contract is validated, but ignored when the contract is used. That would be sound.

Wouldn't that be the same as an assertion at the end of the function?
I'll first check if the sign_verify_internal proof can be rescued through the usual tricks - I had only tested the proofs for the changed contracts locally.

@mkannwischer mkannwischer force-pushed the cbmc-hint-functional-specs branch 2 times, most recently from 064b853 to f9cab4d Compare July 16, 2026 07:51
@mkannwischer
CBMC: Functional specs for make_hint and hint unpacking
ae94c4a 
Strengthen the contracts beyond type/memory safety: pin mld_make_hint's
return value to the exact hint predicate, and prove mld_sig_unpack_hints
sets h->coeffs[p] exactly for the hint indices decoded for row i.

The mld_sig_unpack_hints postcondition is wrapped in functional() so it is
verified in its own proof and discarded by callers that don't rely on
the additional post-condition. Otherwise the sign_verify_internal proof
blows up.

 - Resolves #1099

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer mkannwischer force-pushed the cbmc-hint-functional-specs branch from f9cab4d to ae94c4a Compare July 16, 2026 09:06
@mkannwischer

mkannwischer commented Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

No luck with fixing sign_verify_internal using the usual tricks.
Adding a assertion in the end of the function does work, but I think we want the post-condition to also serve as documentation.
I have added a new macro functional (naming TBD) that can be used to wrap the post-condition so that it is only active for the proof of unpack_hints, but not for the callers. That works for me locally.
We could also define a different variant of ensures.
Any ideas @hanno-becker?

@hanno-becker

hanno-becker commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

Wouldn't that be the same as an assertion at the end of the function?

Yes, functionally it is, but as you say, conceptually it belongs in the contract.

@hanno-becker

hanno-becker commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

I have added a new macro functional (naming TBD) that can be used to wrap the post-condition so that it is only active for the proof of unpack_hints, but not for the callers. That works for me locally. We could also define a different variant of ensures. Any ideas @hanno-becker?

I can't think of anything I like. For the time being, I think we should start with an assertion.

@mkannwischer

mkannwischer commented Jul 16, 2026

Copy link
Copy Markdown
Contributor Author

I have added a new macro functional (naming TBD) that can be used to wrap the post-condition so that it is only active for the proof of unpack_hints, but not for the callers. That works for me locally. We could also define a different variant of ensures. Any ideas @hanno-becker?

I can't think of anything I like. For the time being, I think we should start with an assertion.

As in you do not like what i have right now?

@hanno-becker

hanno-becker commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

Yes, I'm not convinced by the approach yet; you can shoot yourself in the foot by using a functional spec but not proving it. Of course we're doing it the other way around, but nothing enforces it?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

CBMC: Consider providing functional specs for make_hint and unpack_hint

3 participants

@mkannwischer @oqs-bot @hanno-becker