Remove siglen from signing and verification APIs by mkannwischer · Pull Request #1240 · pq-code-package/mldsa-native

mkannwischer · 2026-06-29T08:53:49Z

I would like initiate the discussion on the following breaking change to our API. Please share your thoughts if this change should be made prior to releasing v1.0.0. I have updated the AWS-LC, Pavona, and liboqs integrations (see the patches).

ML-DSA signatures have a fixed size, so siglen was redundant: an always-MLDSA_BYTES output for signing and an input used only for a fixed-size check on verification. Drop it from all signing and verification functions (internal, randomized, extmu, and pre-hash variants). Verification now takes the signature as a fixed-size array.

Resolves siglen parameter in crypto_sign_signature is prone to API misuse #789

oqs-bot · 2026-06-29T09:27:46Z

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

Full Results (206 proofs)

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

oqs-bot · 2026-06-29T09:27:49Z

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

Full Results (206 proofs)

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

oqs-bot · 2026-06-29T09:28:04Z

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

Full Results (206 proofs)

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

oqs-bot · 2026-06-29T09:30:45Z

CBMC Results (ML-DSA-65)

Full Results (206 proofs)

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

oqs-bot · 2026-06-29T09:34:32Z

CBMC Results (ML-DSA-44)

Full Results (206 proofs)

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

oqs-bot · 2026-06-29T09:55:14Z

CBMC Results (ML-DSA-87)

Full Results (206 proofs)

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

oqs-bot · 2026-06-29T13:50:49Z

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sign_verify_internal`	⚠️	566s	130s	+335%

Full Results (203 proofs)

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

mkannwischer · 2026-06-29T13:51:39Z

@jakemas @bhess @rod-chapman @hanno-becker, WDYT about this proposed change?
My view is that it's a useful simplification for most future consumers, and the required changes for existing consumers are acceptable.

hanno-becker · 2026-07-08T09:06:00Z

+#include <stddef.h>
+#include <stdint.h>
+
+#include "mldsa/src/sign.h"


Why is this working with sign.h and not with mldsa_native.h?

OQS doesn't include any headers at all. I used sign.h here because it's a little easier to use and arguably sig_glue.c itself is internal as well.
But we can switch to mldsa_native.h without much complication.
Pushed.

hanno-becker · 2026-07-08T09:20:50Z

 *
 * @spec{Implements @[FIPS204, Algorithm 7, ML-DSA.Sign_internal].}
 *
 * @param[out] sig        Output signature.


The expected length should be specified here. While at it, the text should also be aligned with the other parameters, e.g. Pointer to buffer to hold the generated signature.

hanno-becker · 2026-07-08T09:21:18Z

@@ -368,7 +365,6 @@ int MLD_API_NAMESPACE(signature_extmu)(
 * @spec{Implements @[FIPS204, Algorithm 8, ML-DSA.Verify_internal].}
 *
 * @param[in] sig        Pointer to input signature.


Similar here, the length should be documented not only in the signature, but also in the documentation.

hanno-becker

Overall I support this change. Two questions/requests:

Ideally, no consumer should work with sign.h, because this is internal. They should be working with the public header mldsa_native.h only. Is there a reason why that's not possible?
Now that the siglen parameter is dropped, the buffer length assumption should be documented.

hanno-becker

This is a welcome simplification, thank you @mkannwischer.

I left some observations for how we can improve documentation at the same time, but they are not blocking.

ML-DSA signatures have a fixed size, so siglen was redundant: an always-MLDSA_BYTES output for signing and an input used only for a fixed-size check on verification. Drop it from all signing and verification functions (internal, randomized, extmu, and pre-hash variants) and the SUPERCOP-named aliases. Verification now takes the signature as a fixed-size array. Update the CBMC contracts and harnesses, tests, and examples to match. Adjust AWS-LC, Pavona, and OQS integrations and their tests accordingly. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

jakemas · 2026-07-11T08:17:02Z

@jakemas @bhess @rod-chapman @hanno-becker, WDYT about this proposed change? My view is that it's a useful simplification for most future consumers, and the required changes for existing consumers are acceptable.

While I can’t argue with the simplification of the API, I do want to put down some thoughts. It kind of goes against aws-LC design guidelines. I believe, across awslc we intend to include len (and length checks) to buffers such as this, so I’m not sure the change is positive for aws-LC. Can’t currently check, but IIRC it’s part of the EVP API so we are always going to have those values as call time. We can of course do anything outside of the mldsa API and within EVP itself, but these are consequences of this change.

I do recall some parts in FIPS204 that says about length checks are a requirement (I’m not sure that extends as far as an API requirement, but perhaps worth a check over FIPS 204 on exact language here).

See perhaps Section 3.6.2:

If an implementation can accept inputs for σ or pk of any other length, it shall return false whenever the lengths … differ from their lengths specified in this standard.

siglen allows the caller to define this exactly, and when accepting buffers from potentially untrusted sources, not a bad call for API security in depth. Are we making the API more or less misuse resistant here, are realistic FIPS callers going to be making this check anyway, do we like the control the caller has to enforce len at call time. Would we have to add a caveat that to have FIPS204 one would need to validate the sig length before calling our API? Does this make usage actually more difficult and confusing?

jakemas

Discussion of comment above of potential downstream consequences and FIPS considerations before my approval.

hanno-becker · 2026-07-12T04:01:13Z

Many thanks @jakemas for chiming in!

I think you raise very good points. For higher level APIs such as provided by AWS-LC, it might make sense to always pair buffers with their lengths, and include lengths-checks as required.

If we look at the lower-level API of mlkem/mldsa-native, however, this is not the case: Where buffers are statically sized by the spec, we pass them as statically sized buffers. Good examples are pk, sk, ss, ct. Dropping siglen and working with fixed-size signature buffers seems to add consistency to the mlx-native API design.

I believe there is no right or wrong here: Each library has an API style to choose and a suitable error checking regime to implement. If you pass buffers + lengths, and the length is subject to constraints, you may want to check them. If you merely pass buffers, you may or may not want to include at least rudimentary != NULL checks -- this is actually still an open question for the mlx-native API, as we currently don't do this. If you decide not to include those checks, I'd argue it's not a bug, it's a choice: So long as you are clear about the assumptions of an API (in our case formally reflected in the CBMC preconditions), it's OK to drop checks in the implementations.

Generally, the higher-level your API gets, the less you want to assume and the more checks you want to include. So, at the level of the EVP API it makes sense to check everything, IMO. But equally I believe that at the lowest level we are looking at here, not passing redundant information, and limiting parameter validation checks, is a defensible choice, and it remains my preference.

Note that there is no need to demand that in stack of APIs, the APIs all follow the same choice -- much the contrary. As you move from one layer to another, you'll discharge the conditions that the higher layer does not assume, but the lower layer does. We see this in @mkannwischer's patch to the LC integration layer: The siglen checks are still present in LC, they have just been hoisted out. There has not been a change in behavior for LC, overall.

Overall, I believe that this is a good change which removes an outlier to what is otherwise a consistent low-level API-style pursued in mlx-native. But Jake is right that lengths checks definitely have a place and the higher levels, and we need to make sure there's no change in behavior for our integrations -- which is the case, as far as I see.

Thanks again @jakemas for joining in and let us know further thoughts 🙏

mkannwischer force-pushed the remove-siglen branch from 12f326f to 20221a6 Compare June 29, 2026 09:09

mkannwischer force-pushed the remove-siglen branch 5 times, most recently from 92392f2 to fe85367 Compare June 29, 2026 13:25

mkannwischer marked this pull request as ready for review June 29, 2026 13:48

mkannwischer requested a review from a team as a code owner June 29, 2026 13:48

mkannwischer commented Jun 29, 2026

View reviewed changes

Comment thread integration/liboqs/ML-DSA-44_META.yml Outdated

mkannwischer force-pushed the remove-siglen branch 2 times, most recently from 0c4d036 to 12c9398 Compare June 30, 2026 08:16

mkannwischer added the API-BREAK label Jun 30, 2026

mkannwischer mentioned this pull request Jun 30, 2026

Remove crypto_sign_* API aliases and MLD_CONFIG_NO_SUPERCOP #1248

Merged

mkannwischer force-pushed the remove-siglen branch from 12c9398 to 09eef61 Compare July 2, 2026 09:58

mkannwischer mentioned this pull request Jul 3, 2026

Consider removing the remaining crypto_sign_* API aliases and MLD_CONFIG_NO_SUPERCOP #1249

Closed

mkannwischer force-pushed the remove-siglen branch 2 times, most recently from d94cfd6 to f34f91f Compare July 8, 2026 06:13

hanno-becker reviewed Jul 8, 2026

View reviewed changes

hanno-becker requested changes Jul 8, 2026

View reviewed changes

mkannwischer force-pushed the remove-siglen branch from f34f91f to af48d97 Compare July 8, 2026 10:35

mkannwischer force-pushed the remove-siglen branch from af48d97 to 6143622 Compare July 9, 2026 03:32

mkannwischer changed the title ~~RFC: Remove siglen from signing and verification APIs~~ Remove siglen from signing and verification APIs Jul 9, 2026

mkannwischer force-pushed the remove-siglen branch from 6143622 to b032a56 Compare July 10, 2026 03:26

mkannwischer mentioned this pull request Jul 10, 2026

CI: Update liboqs to 0.16.0 #1276

Open

hanno-becker reviewed Jul 10, 2026

View reviewed changes

Comment thread mldsa/src/sign.h Outdated

hanno-becker reviewed Jul 10, 2026

View reviewed changes

Comment thread mldsa/src/sign.h

hanno-becker reviewed Jul 10, 2026

View reviewed changes

Comment thread integration/aws-lc/post_import.patch

hanno-becker approved these changes Jul 10, 2026

View reviewed changes

mkannwischer force-pushed the remove-siglen branch from b032a56 to 4bbd6c1 Compare July 10, 2026 10:28

mkannwischer enabled auto-merge July 10, 2026 10:28

hanno-becker force-pushed the remove-siglen branch from 4bbd6c1 to 7a622ca Compare July 11, 2026 03:55

jakemas requested changes Jul 11, 2026

View reviewed changes

mkannwischer disabled auto-merge July 13, 2026 10:48

Uh oh!

Conversation

mkannwischer commented Jun 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot commented Jun 29, 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 Jun 29, 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 Jun 29, 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 Jun 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Jun 29, 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 Jun 29, 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 Jun 29, 2026

CBMC Results (ML-DSA-44)

Uh oh!

mkannwischer commented Jun 29, 2026

Uh oh!

Uh oh!

hanno-becker Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

jakemas commented Jul 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jakemas left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hanno-becker commented Jul 12, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mkannwischer commented Jun 29, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading

oqs-bot commented Jun 29, 2026 •

edited

Loading

jakemas commented Jul 11, 2026 •

edited

Loading

jakemas left a comment •

edited

Loading