x86_64 + HOL-Light: Replace rej_uniform_eta2/eta4 intrinsics with hand-written assembly and HOL-Light proofs by jakemas · Pull Request #1188 · pq-code-package/mldsa-native

jakemas · 2026-06-16T17:45:44Z

resolves AVX2: Replace intrinsics implementation of rej_uniform_eta with assembly #419
resolves HOL-Light: Prove AVX2 rej_uniform_eta #917
resolves HOL-Light: Prove x86_64 backend correct #912

Summary

Replaces the AVX2 intrinsics implementations of rej_uniform_eta2 and rej_uniform_eta4 with hand-written x86_64 assembly, and adds HOL-Light functional-correctness and memory-safety proofs for both routines. Follows the same approach as #1014:

Table passed as a parameter (consistent with the aarch64 approach), avoiding external symbol references for simpasm compatibility.
All constants constructed from immediates (no .rodata), enabling HOL-Light formal verification.
__contract__ annotations on the asm entry points (CBMC), kept in sync with the HOL-Light specs.
meta.h wires both eta2 and eta4 to the new asm, so the functional test suite exercises both paths.
The x86_64 HOL-Light Makefile and dump_bytecode.ml register the eta2/eta4 bytecode dump targets; ABI-checker tests added for both.
Adds a poly_uniform_eta_4x component benchmark.

s2n-bignum dependency

The proofs use the VPBROADCASTW instruction, added in awslabs/s2n-bignum#421. Until that merges, the nix pin (nix/s2n_bignum/default.nix) is temporarily pointed at the jakemas/s2n-bignum fork branch so CI can decode the instruction; it will be repointed to awslabs main once #421 lands.

oqs-bot · 2026-06-17T00:15:31Z

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

Full Results (210 proofs)

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

oqs-bot · 2026-06-17T00:15:38Z

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

Full Results (210 proofs)

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

oqs-bot · 2026-06-17T00:15:44Z

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

Full Results (210 proofs)

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

oqs-bot · 2026-06-17T00:17:10Z

CBMC Results (ML-DSA-65)

Full Results (210 proofs)

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

oqs-bot · 2026-06-17T00:17:26Z

CBMC Results (ML-DSA-44)

Full Results (210 proofs)

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

oqs-bot · 2026-06-17T00:18:31Z

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`sign_signature_internal`	⚠️	76s	42s	+81%

Full Results (210 proofs)

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

jakemas · 2026-06-17T02:42:09Z

@hanno-becker / @mkannwischer would it be possible to get review on dev/x86_64/src/rej_uniform_eta{2/4}_avx2_asm.S as a preliminary pass, before I start the hol-light proofs. This should help prevent too much proof churn, should any large changes be requested in review. Ideally, the asm would be finalized in review first, and then I'll mark the PR ready once the proofs are complete.

Good idea. Thanks! Will look later today.

Thank you very much!

github-actions

Mac Mini (M1, 2020) benchmarks (opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`46524` cycles	`46501` cycles	`1.00`
`ML-DSA-44 sign`	`131156` cycles	`131159` cycles	`1.00`
`ML-DSA-44 verify`	`47325` cycles	`47327` cycles	`1.00`
`ML-DSA-65 keypair`	`81696` cycles	`81682` cycles	`1.00`
`ML-DSA-65 sign`	`215403` cycles	`215381` cycles	`1.00`
`ML-DSA-65 verify`	`79311` cycles	`79309` cycles	`1.00`
`ML-DSA-87 keypair`	`132415` cycles	`132436` cycles	`1.00`
`ML-DSA-87 sign`	`277406` cycles	`277663` cycles	`1.00`
`ML-DSA-87 verify`	`134055` cycles	`134051` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Mac Mini (M1, 2020) benchmarks (no-opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`113028` cycles	`112820` cycles	`1.00`
`ML-DSA-44 sign`	`402081` cycles	`401084` cycles	`1.00`
`ML-DSA-44 verify`	`119691` cycles	`119458` cycles	`1.00`
`ML-DSA-65 keypair`	`192981` cycles	`192907` cycles	`1.00`
`ML-DSA-65 sign`	`650273` cycles	`649936` cycles	`1.00`
`ML-DSA-65 verify`	`192931` cycles	`192844` cycles	`1.00`
`ML-DSA-87 keypair`	`318799` cycles	`318799` cycles	`1`
`ML-DSA-87 sign`	`828743` cycles	`828921` cycles	`1.00`
`ML-DSA-87 verify`	`326813` cycles	`326734` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`222141` cycles	`223446` cycles	`0.99`
`ML-DSA-44 sign`	`614240` cycles	`634283` cycles	`0.97`
`ML-DSA-44 verify`	`226725` cycles	`223226` cycles	`1.02`
`ML-DSA-65 keypair`	`385352` cycles	`393894` cycles	`0.98`
`ML-DSA-65 sign`	`1003734` cycles	`1022240` cycles	`0.98`
`ML-DSA-65 verify`	`372158` cycles	`378918` cycles	`0.98`
`ML-DSA-87 keypair`	`650198` cycles	`644349` cycles	`1.01`
`ML-DSA-87 sign`	`1362778` cycles	`1332260` cycles	`1.02`
`ML-DSA-87 verify`	`638012` cycles	`627970` cycles	`1.02`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `7c13c63`	Previous: `70fdba0`	Ratio
`ML-DSA-44 keypair`	`227496` cycles	`219616` cycles	`1.04`
`ML-DSA-44 verify`	`235419` cycles	`214195` cycles	`1.10`
`ML-DSA-87 keypair`	`661599` cycles	`635525` cycles	`1.04`
`ML-DSA-87 sign`	`1369715` cycles	`1306530` cycles	`1.05`
`ML-DSA-87 verify`	`645122` cycles	`616298` cycles	`1.05`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 4th gen (c7i)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`43323` cycles	`43311` cycles	`1.00`
`ML-DSA-44 sign`	`129973` cycles	`130234` cycles	`1.00`
`ML-DSA-44 verify`	`45201` cycles	`45328` cycles	`1.00`
`ML-DSA-65 keypair`	`75758` cycles	`75678` cycles	`1.00`
`ML-DSA-65 sign`	`213832` cycles	`214141` cycles	`1.00`
`ML-DSA-65 verify`	`74325` cycles	`74551` cycles	`1.00`
`ML-DSA-87 keypair`	`123264` cycles	`122951` cycles	`1.00`
`ML-DSA-87 sign`	`270347` cycles	`270036` cycles	`1.00`
`ML-DSA-87 verify`	`120938` cycles	`120608` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 4th gen (c7i) (no-opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`91475` cycles	`91650` cycles	`1.00`
`ML-DSA-44 sign`	`352301` cycles	`353391` cycles	`1.00`
`ML-DSA-44 verify`	`99818` cycles	`100249` cycles	`1.00`
`ML-DSA-65 keypair`	`153858` cycles	`153883` cycles	`1.00`
`ML-DSA-65 sign`	`572079` cycles	`571341` cycles	`1.00`
`ML-DSA-65 verify`	`159979` cycles	`159780` cycles	`1.00`
`ML-DSA-87 keypair`	`255344` cycles	`255804` cycles	`1.00`
`ML-DSA-87 sign`	`726579` cycles	`726454` cycles	`1.00`
`ML-DSA-87 verify`	`264184` cycles	`264128` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`55494` cycles	`55575` cycles	`1.00`
`ML-DSA-44 sign`	`158449` cycles	`159176` cycles	`1.00`
`ML-DSA-44 verify`	`57633` cycles	`58038` cycles	`0.99`
`ML-DSA-65 keypair`	`96318` cycles	`95925` cycles	`1.00`
`ML-DSA-65 sign`	`258646` cycles	`259688` cycles	`1.00`
`ML-DSA-65 verify`	`95634` cycles	`96324` cycles	`0.99`
`ML-DSA-87 keypair`	`155356` cycles	`154620` cycles	`1.00`
`ML-DSA-87 sign`	`323135` cycles	`323315` cycles	`1.00`
`ML-DSA-87 verify`	`151250` cycles	`151152` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`298957` cycles	`309045` cycles	`0.97`
`ML-DSA-44 sign`	`1130396` cycles	`1181040` cycles	`0.96`
`ML-DSA-44 verify`	`327888` cycles	`338438` cycles	`0.97`
`ML-DSA-65 keypair`	`557436` cycles	`569427` cycles	`0.98`
`ML-DSA-65 sign`	`1888548` cycles	`1984198` cycles	`0.95`
`ML-DSA-65 verify`	`538964` cycles	`570461` cycles	`0.94`
`ML-DSA-87 keypair`	`861727` cycles	`894629` cycles	`0.96`
`ML-DSA-87 sign`	`2454019` cycles	`2499364` cycles	`0.98`
`ML-DSA-87 verify`	`907684` cycles	`918394` cycles	`0.99`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `7c13c63`	Previous: `70fdba0`	Ratio
`ML-DSA-44 keypair`	`312772` cycles	`294913` cycles	`1.06`
`ML-DSA-44 sign`	`1193382` cycles	`1147432` cycles	`1.04`
`ML-DSA-87 keypair`	`904673` cycles	`847930` cycles	`1.07`
`ML-DSA-87 sign`	`2468732` cycles	`2393137` cycles	`1.03`
`ML-DSA-87 verify`	`906571` cycles	`874118` cycles	`1.04`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a) (no-opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`133692` cycles	`133431` cycles	`1.00`
`ML-DSA-44 sign`	`520225` cycles	`519219` cycles	`1.00`
`ML-DSA-44 verify`	`146942` cycles	`146686` cycles	`1.00`
`ML-DSA-65 keypair`	`223592` cycles	`224467` cycles	`1.00`
`ML-DSA-65 sign`	`841919` cycles	`843782` cycles	`1.00`
`ML-DSA-65 verify`	`233762` cycles	`234011` cycles	`1.00`
`ML-DSA-87 keypair`	`366674` cycles	`367264` cycles	`1.00`
`ML-DSA-87 sign`	`1057851` cycles	`1060362` cycles	`1.00`
`ML-DSA-87 verify`	`380118` cycles	`381078` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`112327` cycles	`112432` cycles	`1.00`
`ML-DSA-44 sign`	`354085` cycles	`353829` cycles	`1.00`
`ML-DSA-44 verify`	`117505` cycles	`117251` cycles	`1.00`
`ML-DSA-65 keypair`	`194501` cycles	`194915` cycles	`1.00`
`ML-DSA-65 sign`	`584403` cycles	`584545` cycles	`1.00`
`ML-DSA-65 verify`	`193506` cycles	`193060` cycles	`1.00`
`ML-DSA-87 keypair`	`320982` cycles	`321247` cycles	`1.00`
`ML-DSA-87 sign`	`747665` cycles	`747767` cycles	`1.00`
`ML-DSA-87 verify`	`318354` cycles	`318871` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton4

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`67271` cycles	`67334` cycles	`1.00`
`ML-DSA-44 sign`	`198182` cycles	`198212` cycles	`1.00`
`ML-DSA-44 verify`	`70155` cycles	`70164` cycles	`1.00`
`ML-DSA-65 keypair`	`119526` cycles	`119314` cycles	`1.00`
`ML-DSA-65 sign`	`326414` cycles	`326337` cycles	`1.00`
`ML-DSA-65 verify`	`116796` cycles	`116812` cycles	`1.00`
`ML-DSA-87 keypair`	`196482` cycles	`196615` cycles	`1.00`
`ML-DSA-87 sign`	`421379` cycles	`421442` cycles	`1.00`
`ML-DSA-87 verify`	`193268` cycles	`192981` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 4th gen (c7a)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`48126` cycles	`46837` cycles	`1.03`
`ML-DSA-44 sign`	`138997` cycles	`140005` cycles	`0.99`
`ML-DSA-44 verify`	`49819` cycles	`49295` cycles	`1.01`
`ML-DSA-65 keypair`	`82346` cycles	`85296` cycles	`0.97`
`ML-DSA-65 sign`	`226618` cycles	`235771` cycles	`0.96`
`ML-DSA-65 verify`	`82230` cycles	`83871` cycles	`0.98`
`ML-DSA-87 keypair`	`130321` cycles	`132099` cycles	`0.99`
`ML-DSA-87 sign`	`281743` cycles	`282238` cycles	`1.00`
`ML-DSA-87 verify`	`129649` cycles	`129367` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton4 (no-opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`127610` cycles	`127745` cycles	`1.00`
`ML-DSA-44 sign`	`441047` cycles	`440937` cycles	`1.00`
`ML-DSA-44 verify`	`136381` cycles	`136447` cycles	`1.00`
`ML-DSA-65 keypair`	`220529` cycles	`220468` cycles	`1.00`
`ML-DSA-65 sign`	`714603` cycles	`714745` cycles	`1.00`
`ML-DSA-65 verify`	`220923` cycles	`221459` cycles	`1.00`
`ML-DSA-87 keypair`	`364675` cycles	`364373` cycles	`1.00`
`ML-DSA-87 sign`	`915835` cycles	`915833` cycles	`1.00`
`ML-DSA-87 verify`	`370946` cycles	`371331` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 3rd gen (c6i)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`61559` cycles	`61513` cycles	`1.00`
`ML-DSA-44 sign`	`188176` cycles	`187961` cycles	`1.00`
`ML-DSA-44 verify`	`66304` cycles	`66502` cycles	`1.00`
`ML-DSA-65 keypair`	`110399` cycles	`108141` cycles	`1.02`
`ML-DSA-65 sign`	`314455` cycles	`311311` cycles	`1.01`
`ML-DSA-65 verify`	`111028` cycles	`108776` cycles	`1.02`
`ML-DSA-87 keypair`	`173234` cycles	`171604` cycles	`1.01`
`ML-DSA-87 sign`	`378684` cycles	`380707` cycles	`0.99`
`ML-DSA-87 verify`	`171059` cycles	`172479` cycles	`0.99`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2 (no-opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`212157` cycles	`211410` cycles	`1.00`
`ML-DSA-44 sign`	`761446` cycles	`758945` cycles	`1.00`
`ML-DSA-44 verify`	`229897` cycles	`228936` cycles	`1.00`
`ML-DSA-65 keypair`	`378864` cycles	`377838` cycles	`1.00`
`ML-DSA-65 sign`	`1248060` cycles	`1248443` cycles	`1.00`
`ML-DSA-65 verify`	`373372` cycles	`372800` cycles	`1.00`
`ML-DSA-87 keypair`	`602524` cycles	`600578` cycles	`1.00`
`ML-DSA-87 sign`	`1584621` cycles	`1583512` cycles	`1.00`
`ML-DSA-87 verify`	`618342` cycles	`616106` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

jakemas · 2026-07-07T01:34:12Z

Ok, ready for review now. The proof files are pretty large, I've thrown claude at them a few times over to try and reduce and streamline the proofs as much as possible, but they are large. This shares some of the sampling table infrastructure with the uniform_rej proof also in PR, so I will rebase once that has landed. Updated the READMEs accordingly as this is the last of the avx2 backend.

oqs-bot

Graviton5

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`51441` cycles	`51442` cycles	`1.00`
`ML-DSA-44 sign`	`162168` cycles	`162042` cycles	`1.00`
`ML-DSA-44 verify`	`54673` cycles	`54768` cycles	`1.00`
`ML-DSA-65 keypair`	`90292` cycles	`90183` cycles	`1.00`
`ML-DSA-65 sign`	`267938` cycles	`268062` cycles	`1.00`
`ML-DSA-65 verify`	`89970` cycles	`89941` cycles	`1.00`
`ML-DSA-87 keypair`	`146017` cycles	`145852` cycles	`1.00`
`ML-DSA-87 sign`	`335274` cycles	`335524` cycles	`1.00`
`ML-DSA-87 verify`	`145278` cycles	`144915` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton5 (no-opt)

Details

Benchmark suite	Current: `237e387`	Previous: `31300ad`	Ratio
`ML-DSA-44 keypair`	`100037` cycles	`100026` cycles	`1.00`
`ML-DSA-44 sign`	`368981` cycles	`369108` cycles	`1.00`
`ML-DSA-44 verify`	`110162` cycles	`110142` cycles	`1.00`
`ML-DSA-65 keypair`	`174279` cycles	`174573` cycles	`1.00`
`ML-DSA-65 sign`	`599035` cycles	`599096` cycles	`1.00`
`ML-DSA-65 verify`	`177906` cycles	`178198` cycles	`1.00`
`ML-DSA-87 keypair`	`285478` cycles	`285839` cycles	`1.00`
`ML-DSA-87 sign`	`760123` cycles	`759674` cycles	`1.00`
`ML-DSA-87 verify`	`296766` cycles	`296320` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

mkannwischer

Many thanks @jakemas for tackling the last two proofs. Looks like a massive amount of work.
The proven specifications are aligned with the aarch64 specs and look good to me!

There are a couple blocking issues:

The CBMC specs are off by one.
There are many dead lemmas that should be trimmed. Can you remove that is not needed here?
There are many comments that don't help the reader understand the proof . Some read like status updates, some are an artifact of how you got there (search for cheat and dates 2026-xx-yy). Can you do a pass though the comments and keep only what is useful?

Could you tackle those please?

mkannwischer · 2026-07-09T05:47:31Z

-  version = "9061e8b76522beafa5ca020f3c8d99b23eba4fbc";
+  # Temporarily pinned to the jakemas/s2n-bignum fork (PR awslabs/s2n-bignum#421,
+  # branch x86-add-vpbroadcastw) so CI picks up the VPBROADCASTW instruction model
+  # needed by the rej_uniform_eta2 AVX2 proof. Repoint to awslabs main once #421 merges.
+  version = "e714d36ddd97ee41cec043f0bc27b87d6f6efd68";
  src = fetchFromGitHub {
-    owner = "awslabs";
+    owner = "jakemas";
    repo = "s2n-bignum";
    rev = "${version}";
-    hash = "sha256-NvtrVfiz5yxfdNvD0P1wSQrn37znuWMbNWxys4jZlU4=";
+    hash = "sha256-hQ7Y+EHua2nMwF1uM/zyxwR3FWfSZCmq4RBwuHGeVGo=";


Marking this so we don't accidentally merge it like this.

mkannwischer · 2026-07-09T05:49:37Z

+  requires(table == mld_rej_uniform_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  ensures(array_bound(r, 0, return_value, -2, 2))


The upper bound is exclusive, so this is wrong.
Use array_abs_bound( ..., 3)

Thanks, fixed!

mkannwischer · 2026-07-09T05:49:47Z

+  requires(table == mld_rej_uniform_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  ensures(array_bound(r, 0, return_value, -4, 4))


Thanks, fixed!

mkannwischer · 2026-07-09T05:50:23Z

+        yield idxs
+
+
+def gen_avx2_rej_uniform_table_rows_c():


This overlaps with the other PR. Please rebase it on top of that one.

Yes, was going to fix this as part of the rebase once uniform_rej landed. fixed now and rebased on tip of main.

mkannwischer · 2026-07-09T05:52:26Z

  MLD_CT_TESTING_DECLASSIFY(buf, buflen);
-  outlen = mld_rej_uniform_eta4_avx2(r, buf);
+  outlen = mld_rej_uniform_eta4_avx2_asm(
+      r, buf, (const uint8_t *)mld_rej_uniform_table);


Can we eliminate the cast here?

mkannwischer · 2026-07-09T06:03:06Z

+            ==> REJ_SAMPLE_ETA4_BYTES [b] =
+                [word_sx(word_sub (word 4:int16) (word(val b MOD 16))):int32;
+                 word_sx(word_sub (word 4:int16) (word(val b DIV 16))):int32]`,
+  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REJ_SAM


mkannwischer · 2026-07-09T06:04:04Z

+            ==> REJ_SAMPLE_ETA4_BYTES [b] =
+                [word_sx(word_sub (word 4:int16) (word(val b MOD 16))):int32;
+                 word_sx(word_sub (word 4:int16) (word(val b DIV 16))):int32]`,
+  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REJ_SAM


CAn we eliminate this extra theorem? it's okay to prove the bound only for the subroutine form.

mkannwischer · 2026-07-09T06:04:55Z

+            ==> REJ_SAMPLE_ETA4_BYTES [b] =
+                [word_sx(word_sub (word 4:int16) (word(val b MOD 16))):int32;
+                 word_sx(word_sub (word 4:int16) (word(val b DIV 16))):int32]`,
+  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REJ_SAM


why skeleton?

removed (skeleton)

mkannwischer · 2026-07-09T06:07:07Z

+            ==> REJ_SAMPLE_ETA4_BYTES [b] =
+                [word_sx(word_sub (word 4:int16) (word(val b MOD 16))):int32;
+                 word_sx(word_sub (word 4:int16) (word(val b DIV 16))):int32]`,
+  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REJ_SAM


these are used

mkannwischer · 2026-07-09T06:31:44Z

+  SUBGOAL_THEN `a MOD 2 EXP 32 = a` (fun th -> REWRITE_TAC[th]) THENL
+   [MATCH_MP_TAC MOD_LT THEN ASM_ARITH_TAC; ASM_ARITH_TAC]);;
+
+let VAL_WORD_GE_9 = prove


This lemma is not used anywhere.
According to Claude, there are a total of 98 dead helpers in this file (plus another 24 in the eta2 file). Could you please do a pass eliminating all lemmas that are unused.

Thank you, I thought I'd already done a pass on this, but you're right. Removed ~114 unused.

jakemas · 2026-07-13T20:25:35Z

ok, all review addressed! @mkannwischer

mkannwischer

Thanks @jakemas, there are still quite a few dead theorems:

  rej_uniform_eta4_avx2_asm.ml (21):
  L424  PSHUFB_TABLE_GATHER          L3011 SUB_LIST_256_FROM_PARTIAL_REJ
  L835  wzx256                       L3030 SCALAR_TAIL_N_EQ_17
  L1198 POPCNT_VPMOVMSKB_LOW8        L3047 LENGTH_OUTLIST0_LE_280
  L1800 REJ_SAMPLE_ETA4_BYTES_16_AS_4 L3128 NIBLEN_BOUND_FROM_WOP
  L2236 POPCNT_NIBBLES_4_BYTES_BRIDGE L3239 REJ_PREFIX_STEP_4
  L2792 SUBITER1_VALUE               L3259 GATHER_WIDE
  L2903 SUBITER_OUTLEN_STEP_4        L3269 MASK_WIDE
  L2965 WORD_SUB_4_NIBBLE_INT32_AS_SX L3296 SIMD2_EXPAND_CONV
  L3307 MASKBIT_PF_TAC               L4018 SI2_GATHER_TO_STORE
  L4286 SI3_GATHER                   L4536 SI4_GATHER
  L7813 DISCARD_OLDSTATE_KEEP_EVENTS_TAC

  rej_uniform_eta2_avx2_asm.ml (12):
  L506  PSHUFB_TABLE_GATHER          L2649 SUBITER_GATHER_NIB_ETA2
  L1278 POPCNT_VPMOVMSKB_LOW8        L2675 SUBITER_MASK_NIB_ETA2
  L1489 SUBITER_STORE_POSTCOND       L2680 MASK_ACCEPT_ETA2
  L2023 POPCNT_NIBBLES_4_BYTES_BRIDGE L2849 REJ_PREFIX_STEP_4
  L2065 ETA_GATHER                   L3244 ETA2_SI1_REDUCE_REFOLD_TAC
  L2086 REDUCE32_LANE_ETA2           L6578 MIDGUARD_NOT_TAKEN_CLEAN_ETA2

(Claude found those, I randomly checked a few)
Could you remove those as well, please?

The comments in the eta4 file are now much cleaner, thank you! In the eta2 files I still see what looks like debugging commentary (particularly the ★CASE4 FIX comments). Could you please clean those up too?

mkannwischer · 2026-07-14T04:32:53Z

+let MOVZBL_R10_CAPTURE_TAC : tactic =
+  RULE_ASSUM_TAC(CONV_RULE(REWRITE_CONV[OP8_R8B_READ] THENC ONCE_DEPTH_CONV COMPONENT_READ_OVER_WRITE_CONV));;
+
+let wzx256 = prove(`!x:int256. word_zx x:int256 = x`, REWRITE_TAC[WORD_ZX_TRIVIAL]);;


mkannwischer · 2026-07-14T04:33:45Z

+(* (per-lane gather). Lane-0 specialisation kept as PSHUFB_TABLE_GATHER for  *)
+(* convenience; the indexed PSHUFB_TABLE_GATHER_8 covers all 8 lanes.        *)
+
+let PSHUFB_TABLE_GATHER = prove


jakemas · 2026-07-14T17:17:02Z

Thanks @mkannwischer! Both addressed in the latest push:

Dead theorems — removed all 21 flagged in eta4 and all 12 in eta2. While doing eta2 I also dropped three now-orphaned private helpers (gen_gather, gen_mask, mask_tac) that only fed the removed SUBITER_GATHER_NIB_ETA2/SUBITER_MASK_NIB_ETA2, so they don't become the next round of dead code.

eta2 debugging commentary — cleaned up all the ★ CASE4 FIX #N markers.

…d-written assembly and HOL-Light proofs Replaces the rej_uniform_eta2 and rej_uniform_eta4 AVX2 intrinsics with hand-written assembly, and adds HOL-Light functional-correctness and memory-safety proofs for both x86_64 routines, plus the CBMC proof for the native wrapper. Both routines are variable-time, so — as for the AArch64 eta proofs — only functional correctness and memory safety are proven, not constant time. The table is passed as a parameter and all constants are built from immediates (no .rodata), following the rej_uniform approach in #1014. The proofs use the VPBROADCASTW instruction, so the s2n-bignum nix pin is temporarily moved to the fork branch of awslabs/s2n-bignum#421 until it lands on main. Signed-off-by: Jake Massimo <[email protected]>

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 5 times, most recently from f789e8d to 1e78719 Compare June 16, 2026 23:56

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from 1e78719 to 7c13c63 Compare June 17, 2026 01:36

jakemas commented Jun 17, 2026

View reviewed changes

mkannwischer added the benchmark label Jun 17, 2026

github-actions Bot reviewed Jun 17, 2026

View reviewed changes

oqs-bot reviewed Jun 17, 2026

View reviewed changes

github-actions Bot reviewed Jun 17, 2026

View reviewed changes

oqs-bot reviewed Jun 17, 2026

View reviewed changes

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from 34a0032 to 5e9bd22 Compare July 6, 2026 21:58

jakemas removed the benchmark label Jul 6, 2026

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 2 times, most recently from 88a47fd to 237e387 Compare July 7, 2026 00:53

jakemas added the benchmark label Jul 7, 2026

jakemas marked this pull request as ready for review July 7, 2026 01:34

jakemas requested a review from a team as a code owner July 7, 2026 01:34

oqs-bot reviewed Jul 7, 2026

View reviewed changes

mkannwischer requested changes Jul 9, 2026

View reviewed changes

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 7 times, most recently from 908d880 to b157440 Compare July 13, 2026 19:33

mkannwischer requested changes Jul 14, 2026

View reviewed changes

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from b157440 to b6fce4e Compare July 14, 2026 17:16

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch 6 times, most recently from 7bce7a5 to df464ba Compare July 14, 2026 22:58

jakemas force-pushed the jakemas/rej-uniform-eta-asm branch from df464ba to 44c3af7 Compare July 14, 2026 23:19

Uh oh!

Conversation

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

Uh oh!

Summary

s2n-bignum dependency

Uh oh!

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

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

jakemas Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

jakemas Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Mac Mini (M1, 2020) benchmarks (opt)

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Mac Mini (M1, 2020) benchmarks (no-opt)

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

⚠️ Performance Alert ⚠️

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i)

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i) (no-opt)

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

AMD EPYC 3rd gen (c6a)

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Uh oh!

github-actions Bot left a comment

jakemas commented Jun 16, 2026 •

edited by mkannwischer

Loading

oqs-bot commented Jun 17, 2026 •

edited

Loading

oqs-bot commented Jun 17, 2026 •

edited

Loading

oqs-bot commented Jun 17, 2026 •

edited

Loading

oqs-bot commented Jun 17, 2026 •

edited

Loading

oqs-bot commented Jun 17, 2026 •

edited

Loading

oqs-bot commented Jun 17, 2026 •

edited

Loading

github-actions Bot left a comment •

edited

Loading

github-actions Bot left a comment •

edited

Loading

github-actions Bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

github-actions Bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

oqs-bot left a comment •

edited

Loading

mkannwischer left a comment •

edited

Loading