Tests: Add AVR baremetal tests by mkannwischer · Pull Request #1158 · pq-code-package/mldsa-native

mkannwischer · 2026-06-07T02:37:59Z

Resolves Consider AVR baremetal tests #1157

mkannwischer · 2026-06-07T07:28:20Z

The ACVP tests for verification require the return value of the main function to properly test invalid signatures. Currently the AVR harness does not propagate the return codes. That needs to be fixed first.

oqs-bot · 2026-06-10T14:07:06Z

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

Full Results (205 proofs)

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

oqs-bot · 2026-06-10T14:07:14Z

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

Full Results (205 proofs)

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

oqs-bot · 2026-06-10T14:07:14Z

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

Full Results (205 proofs)

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

oqs-bot · 2026-06-10T14:08:34Z

CBMC Results (ML-DSA-44)

Full Results (205 proofs)

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

oqs-bot · 2026-06-10T14:09:02Z

CBMC Results (ML-DSA-65)

Full Results (205 proofs)

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

oqs-bot · 2026-06-10T14:09:44Z

CBMC Results (ML-DSA-87)

Full Results (205 proofs)

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

mkannwischer · 2026-06-10T15:00:47Z

The ACVP tests for verification require the return value of the main function to properly test invalid signatures. Currently the AVR harness does not propagate the return codes. That needs to be fixed first.

That is now added in. Also the UBSan tests were ported from mlkem-native

On platforms with 16-bit int, several shift and conversion idioms relied on int being at least 32 bits: - Shift constants exceeding 16-bit int need explicit int32_t (reduce.h, rounding.h, MLDSA_GAMMA1 in params.h) - The ghost bound parameter of mld_ntt_butterfly_block reaches up to 9 * MLD_FQMUL_BOUND and does not fit unsigned int; use uint32_t - Use unsigned for the Keccak rate in fips202x4.c (as in mlkem-native) - Keep the nonce computation in mld_yvec_get_poly_lazy unsigned to avoid signed/unsigned conversion when uint16_t does not promote to int Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Decode the hex values of ACVP command line arguments in place inside the argument strings instead of into separate stack buffers. This reduces peak RAM usage by up to ~13KB, which is required to fit ML-DSA-87 sigGen into the 64KB data address space of AVR. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Port the AVR baremetal build and test environment from mlkem-native, using avr-gcc and a patched simavr (ATmega128rfr2 with RAM bumped to the maximal 63.5K of the 16-bit data address space, 32K EEPROM). Unlike mlkem-native, the argc/argv block is placed at the top of RAM at a per-invocation address chosen by the exec wrapper and passed via EEPROM; startup code points the stack directly below it. This is needed because ML-DSA test binaries have conflicting demands: the functional and RNG-failure tests carry up to ~24K of .data test vectors, while the ACVP binaries receive up to ~31K of hex-encoded arguments. Test exit codes are propagated through simavr's exit-code commands (buserror/simavr@c9354b3, not yet in a release, backported as a patch): the firmware declares a command register via AVR_MCU_SIMAVR_COMMAND, and an exit() override forwards the return value of main(). The .mmcu section holding the register declaration must be placed outside the flash address range: the linker otherwise places it between the .text and .data load segments, and simavr then loads .data at the wrong address, breaking the firmware. The tests are built with -fno-wrapv -fsanitize=undefined -fsanitize-trap=undefined to detect UB (such as signed-shift overflow on 16-bit int) at runtime; avr-gcc otherwise defaults to -fwrapv, hiding such UB. On a trap, the abort() override in the test wrapper prints an error and exits nonzero. Builds use MLD_CONFIG_REDUCE_RAM and a single test iteration. Functional, RNG-failure, and ACVP tests pass in simavr for all parameter sets. Unit tests exceed avr-gcc's per-function stack frame limit and are disabled. In CI, only the ACVP tests are run to keep the runtime manageable. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

mkannwischer force-pushed the avr branch 3 times, most recently from 971c25c to 346b78d Compare June 10, 2026 13:27

mkannwischer marked this pull request as ready for review June 10, 2026 15:00

mkannwischer requested a review from a team as a code owner June 10, 2026 15:00

hanno-becker self-assigned this Jun 13, 2026

hanno-becker self-requested a review June 13, 2026 05:38

hanno-becker reviewed Jun 13, 2026

View reviewed changes

Comment thread mldsa/src/poly.c Outdated

mkannwischer force-pushed the avr branch 2 times, most recently from b706360 to 76b822c Compare June 17, 2026 08:31

hanno-becker force-pushed the avr branch from 76b822c to 69b18e5 Compare June 20, 2026 04:09

mkannwischer added 3 commits June 20, 2026 12:58

mkannwischer force-pushed the avr branch from 69b18e5 to 505fc93 Compare June 20, 2026 04:58

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Tests: Add AVR baremetal tests#1158

Tests: Add AVR baremetal tests#1158
mkannwischer wants to merge 3 commits into
mainfrom
avr

mkannwischer commented Jun 7, 2026 •

edited

Loading

Uh oh!

mkannwischer commented Jun 7, 2026

Uh oh!

oqs-bot commented Jun 10, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 10, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 10, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 10, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 10, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 10, 2026 •

edited

Loading

Uh oh!

mkannwischer commented Jun 10, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

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

Uh oh!

Uh oh!

mkannwischer commented Jun 7, 2026

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

mkannwischer commented Jun 10, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mkannwischer commented Jun 7, 2026 •

edited

Loading

oqs-bot commented Jun 10, 2026 •

edited

Loading

oqs-bot commented Jun 10, 2026 •

edited

Loading

oqs-bot commented Jun 10, 2026 •

edited

Loading

oqs-bot commented Jun 10, 2026 •

edited

Loading

oqs-bot commented Jun 10, 2026 •

edited

Loading

oqs-bot commented Jun 10, 2026 •

edited

Loading