CBMC: Functional specs for `make_hint` and hint unpacking by mkannwischer · Pull Request #1287 · pq-code-package/mldsa-native

mkannwischer · 2026-07-15T09:26:23Z

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.

Resolves CBMC: Consider providing functional specs for make_hint and unpack_hint #1099

oqs-bot · 2026-07-15T09:51:33Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sig_unpack_hints`	⚠️	21s	1s	+2000%

Full Results (210 proofs)

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

oqs-bot · 2026-07-15T10:18:53Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`polyeta_unpack`	⚠️	20s	13s	+54%
`sig_unpack_hints`	⚠️	24s	4s	+500%

Full Results (210 proofs)

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

oqs-bot · 2026-07-15T10:18:57Z

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

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sig_unpack_hints`	⚠️	41s	2s	+1950%

Full Results (210 proofs)

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

oqs-bot · 2026-07-15T10:19:29Z

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sig_unpack_hints`	⚠️	30s	3s	+900%
`sign_signature_internal`	⚠️	73s	42s	+74%

Full Results (210 proofs)

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

oqs-bot · 2026-07-15T10:19:34Z

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sig_unpack_hints`	⚠️	41s	2s	+1950%

Full Results (210 proofs)

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

oqs-bot · 2026-07-15T10:20:15Z

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sig_unpack_hints`	⚠️	34s	2s	+1600%

Full Results (210 proofs)

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

hanno-becker · 2026-07-16T05:24:57Z

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 · 2026-07-16T05:48:15Z

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 · 2026-07-16T09:11:34Z

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 · 2026-07-16T10:23:40Z

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 · 2026-07-16T10:27:35Z

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 · 2026-07-16T12:49:34Z

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 · 2026-07-16T16:38:17Z

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?

mkannwischer · 2026-07-17T01:55:10Z

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?

Indeed, that is a valid concern.
Let's change it to an assertion for now and open an issue to discuss how additional function specs can be added that don't affect callees (I went through the CBMC documentation, but didn't find anything that would help with that).

hanno-becker · 2026-07-17T03:38:40Z

Yes, I think that's the right approach.

mkannwischer · 2026-07-17T05:21:45Z

I have opened a follow-up issue: #1292

Strengthen the contracts beyond type/memory safety. Pin mld_make_hint's return value to the exact hint predicate via an ensures clause. Prove mld_sig_unpack_hints sets h->coeffs[p] exactly for the hint indices decoded for a row. This is expressed as an assertion at the end of the function rather than a postcondition, so sign_verify_internal need not assume it (that turned out to blow up the sign_verify_internal proof). - Resolves #1099 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

hanno-becker

Thank you @mkannwischer! I slightly tweaked the comment.

mkannwischer force-pushed the cbmc-hint-functional-specs branch 3 times, most recently from f9cab4d to ae94c4a Compare July 16, 2026 09:06

mkannwischer force-pushed the cbmc-hint-functional-specs branch from ae94c4a to aa5b532 Compare July 17, 2026 05:00

mkannwischer mentioned this pull request Jul 17, 2026

CBMC: find a way to express functional postconditions without imposing them on callers #1292

Open

mkannwischer force-pushed the cbmc-hint-functional-specs branch from aa5b532 to 662d83f Compare July 17, 2026 05:48

mkannwischer marked this pull request as ready for review July 17, 2026 06:18

mkannwischer requested a review from a team as a code owner July 17, 2026 06:18

mkannwischer and others added 2 commits July 20, 2026 07:03

CBMC: Tweak comment on post-condition-as-assert in unpack_hints

74ee4be

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

hanno-becker force-pushed the cbmc-hint-functional-specs branch from 662d83f to 74ee4be Compare July 20, 2026 06:03

hanno-becker approved these changes Jul 20, 2026

View reviewed changes

hanno-becker enabled auto-merge July 20, 2026 06:04

hanno-becker added this pull request to the merge queue Jul 20, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Jul 20, 2026

mkannwischer added this pull request to the merge queue Jul 20, 2026

Merged via the queue into main with commit 90fd070 Jul 20, 2026
389 checks passed

mkannwischer deleted the cbmc-hint-functional-specs branch July 20, 2026 09:22

Uh oh!

Conversation

mkannwischer commented Jul 15, 2026

Uh oh!

oqs-bot commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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

Uh oh!

oqs-bot commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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

Uh oh!

oqs-bot commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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

Uh oh!

oqs-bot commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

oqs-bot commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

hanno-becker commented Jul 16, 2026

Uh oh!

mkannwischer commented Jul 16, 2026

Uh oh!

mkannwischer commented Jul 16, 2026

Uh oh!

hanno-becker commented Jul 16, 2026

Uh oh!

hanno-becker commented Jul 16, 2026

Uh oh!

mkannwischer commented Jul 16, 2026

Uh oh!

hanno-becker commented Jul 16, 2026

Uh oh!

mkannwischer commented Jul 17, 2026

Uh oh!

hanno-becker commented Jul 17, 2026

Uh oh!

mkannwischer commented Jul 17, 2026

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oqs-bot commented Jul 15, 2026 •

edited

Loading

oqs-bot commented Jul 15, 2026 •

edited

Loading

oqs-bot commented Jul 15, 2026 •

edited

Loading

oqs-bot commented Jul 15, 2026 •

edited

Loading

oqs-bot commented Jul 15, 2026 •

edited

Loading

oqs-bot commented Jul 15, 2026 •

edited

Loading