Add Armv8.1-M Keccak x1 backend by bremoran · Pull Request #1277 · pq-code-package/mldsa-native

bremoran · 2026-07-10T08:11:34Z

Add the unmodified upstream Adomnicai Armv7-M Keccak source under armv81m_clean and the Slothy-generated M7 optimized x1 permutation under armv81m_opt, with a Makefile regeneration path.

Move the Armv8.1-M FIPS202 development sources to armv81m_opt and synchronize the production backend. Route x1 state XOR/extract through the clean-source assembly helpers so the optimized permutation can keep the state in the bit-interleaved native representation.

Keep the test changes focused on representation-aware Keccak x1/x4 unit coverage, including extracted-byte state dumps on x1 failures, and the static ML-DSA-87 unit-test workspace needed for Zephyr stack pressure.

- Port of pq-code-package/mlkem-native#1547 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

- Port of pq-code-package/mlkem-native#1791 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Zephyr's k_cycle_get_32() can wrap during long NUCLEO benchmark windows, producing huge unsigned deltas in the benchmark output. Use k_cycle_get_64() for Zephyr targets. Also make ML-DSA benchmark percentile sorting and formatting robust for large uint64_t cycle values. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Run the NUCLEO-N657X0-Q Zephyr test image as XIP from ITCM and place runtime data/stacks in DTCM after the runner expands FLEXMEM to 256 KiB ITCM and 256 KiB DTCM. Force STM32N6 SystemInit() to use the ITCM vector table address for VTOR. Without this, its fallback derives VTOR from &g_pfnVectors, which moves into DTCM with Zephyr data and points VTOR at RAM data instead of the vector table. Add an early reset hook that scrubs the expanded DTCM window before Zephyr stack, BSS, and MPU setup touch it. Tested: - nix develop .#zephyr --command make run_func EXTRA_MAKEFILE=test/zephyr/platform.mk ZEPHYR_TARGET=mps3-an547 CYCLES=NO -j1 - nix develop .#zephyr --command make run_bench_components EXTRA_MAKEFILE=test/zephyr/platform.mk ZEPHYR_TARGET=nucleo-n657x0-q CYCLES=NO -j1 Signed-off-by: Brendan Moran <brendan.moran@arm.com>

oqs-bot · 2026-07-10T16:09:56Z

CBMC Results (ML-DSA-44)

Full Results (206 proofs)

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

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

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

Full Results (206 proofs)

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

oqs-bot · 2026-07-10T16:10:13Z

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

Full Results (206 proofs)

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

oqs-bot · 2026-07-10T16:10:53Z

CBMC Results (ML-DSA-65)

Full Results (206 proofs)

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

oqs-bot · 2026-07-10T16:11:02Z

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

Full Results (206 proofs)

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

oqs-bot · 2026-07-10T16:14:08Z

CBMC Results (ML-DSA-87)

Full Results (206 proofs)

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

Add the unmodified upstream Adomnicai Armv7-M Keccak source under armv81m_clean and the Slothy-generated M7 optimized x1 permutation under armv81m_opt, with a Makefile regeneration path. Move the Armv8.1-M FIPS202 development sources to armv81m_opt and synchronize the production backend. Route x1 state XOR/extract through the clean-source assembly helpers so the optimized permutation can keep the state in the bit-interleaved native representation. Keep the test changes focused on representation-aware Keccak x1/x4 unit coverage, including extracted-byte state dumps on x1 failures, and the static ML-DSA-87 unit-test workspace needed for Zephyr stack pressure. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Add the clean Armv81-M Keccak permutation source with the project tri-license header and provenance for the public-domain SLOTHY input. Keep the related generated/autogen/test formatting updates staged with the import. Tests: ZEPHYR_TARGET=mps3-an547 nix develop .#zephyr --command ./scripts/tests func --opt=opt Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

bremoran requested a review from a team as a code owner July 10, 2026 08:11

mkannwischer marked this pull request as draft July 10, 2026 08:18

mkannwischer and others added 4 commits July 10, 2026 16:36

Add NUCLEO-N657X0-Q Zephyr hardware platform

001b584

- Port of pq-code-package/mlkem-native#1547 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

zephyr: keep project CFLAGS off Zephyr internals

439cbef

- Port of pq-code-package/mlkem-native#1791 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

bremoran added 3 commits July 10, 2026 17:44

Fix C90 compatibility.

f875a73

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

bremoran force-pushed the armv81m-keccak-x1 branch from 07b9ec4 to f875a73 Compare July 10, 2026 16:45

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add Armv8.1-M Keccak x1 backend#1277

Add Armv8.1-M Keccak x1 backend#1277
bremoran wants to merge 7 commits into
mainfrom
armv81m-keccak-x1

bremoran commented Jul 10, 2026

Uh oh!

oqs-bot commented Jul 10, 2026

Uh oh!

oqs-bot commented Jul 10, 2026

Uh oh!

oqs-bot commented Jul 10, 2026

Uh oh!

oqs-bot commented Jul 10, 2026

Uh oh!

oqs-bot commented Jul 10, 2026

Uh oh!

oqs-bot commented Jul 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

bremoran commented Jul 10, 2026

Uh oh!

oqs-bot commented Jul 10, 2026

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Jul 10, 2026

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

Uh oh!

oqs-bot commented Jul 10, 2026

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

Uh oh!

oqs-bot commented Jul 10, 2026

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Jul 10, 2026

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

Uh oh!

oqs-bot commented Jul 10, 2026

CBMC Results (ML-DSA-87)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants