Skip to content

Clear ML-KEM Keccak stack scratch#1771

Open
tob-joe wants to merge 2 commits into
mainfrom
ptp/mlkem-clear-keccak-stack-scratch
Open

Clear ML-KEM Keccak stack scratch#1771
tob-joe wants to merge 2 commits into
mainfrom
ptp/mlkem-clear-keccak-stack-scratch

Conversation

@tob-joe

@tob-joe tob-joe commented Jun 30, 2026

Copy link
Copy Markdown

Clear ML-KEM Keccak stack scratch

Summary

  • Clear transient stack scratch in the AVX2, AArch64 scalar-hybrid, and Armv8.1-M MVE x4 Keccak backends.
  • Refresh the corresponding HOL Light proof copies for the changed instruction streams.
  • Keep state-derived stack scratch from surviving past the x4 permutation return path.

Proof Diff Shape

The proof delta follows the changed postambles. The AArch64 x4 Keccak postambles grow from 48 bytes to 108 bytes after adding the zero stores, so the HOL Light proof scripts refresh the embedded bytecode, postamble length constants, and subroutine wrapper step counts. The x86_64 AVX2 proof steps through the additional wipe stores and carries the corresponding event-trace/maychange obligations through the subroutine safety wrapper.

Verification

  • nix develop .#hol_light-cross-aarch64 -c make -B -C proofs/hol_light/aarch64 mlkem/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.correct
  • nix develop .#hol_light-cross-aarch64 -c make -B -C proofs/hol_light/aarch64 mlkem/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.correct
  • nix develop .#hol_light-cross-x86_64 -c make -B -C proofs/hol_light/x86_64 mlkem/keccak_f1600_x4_avx2_asm.correct

Co-authored-by: Codex codex@openai.com
Signed-off-by: Joe Doyle joseph.doyle@trailofbits.com

This work was completed by Trail of Bits as part of the Patch The Planet project in collaboration with OpenAI. The issue was identified primarily by the Codex coding agent, and manually reviewed before submission.

@tob-joe tob-joe requested a review from a team as a code owner June 30, 2026 14:23
@oqs-bot

oqs-bot commented Jun 30, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1575s 1481s +6.3%
mlk_indcpa_enc ✅ 245s 233s +5%
mlk_indcpa_keypair_derand ✅ 211s 193s +9%
mlk_poly_rej_uniform ✅ 141s 125s +13%
mlk_rej_uniform_c ✅ 115s 108s +6%
rej_uniform_native_x86_64 ✅ 58s 55s +5%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 54s 49s +10%
mlk_poly_reduce_native ✅ 37s 33s +12%
poly_ntt_native ✅ 36s 32s +12%
rej_uniform_native_aarch64 ✅ 36s 35s +3%
mlk_ntt_layer ✅ 30s 30s +0%
mlk_keccak_squeezeblocks_x4 ✅ 26s 25s +4%
mlk_indcpa_dec ✅ 17s 15s +13%
mlk_fqmul ✅ 16s 15s +7%
keccakf1600x4_permute_native_x4 ✅ 15s 18s -17%
mlk_poly_decompress_d10_native ✅ 13s 15s -13%
mlk_poly_decompress_d4_native ✅ 13s 14s -7%
mlk_poly_frommsg ✅ 10s 9s +11%
mlk_polyvec_add ✅ 10s 11s -9%
mlk_ntt_butterfly_block ✅ 9s 8s +12%
mlk_poly_frombytes_native ✅ 9s 6s +50%
polyvec_basemul_acc_montgomery_cached_native ✅ 9s 8s +12%
mlk_keccak_squeezeblocks ✅ 8s 7s +14%
mlk_poly_sub ✅ 7s 7s +0%
poly_decompress_d10_native_x86_64 ✅ 7s 4s +75%
kem_dec ✅ 6s 5s +20%
mlk_keccak_squeeze_once ✅ 6s 8s -25%
mlk_keccakf1600_permute_c ✅ 6s 4s +50%
mlk_poly_rej_uniform_x4 ✅ 6s 5s +20%
poly_frombytes_native_x86_64 ✅ 6s 5s +20%
mlk_ct_cmov_zero ✅ 5s 3s +67%
mlk_enc_getnoise_eta1_eta2 ✅ 5s 3s +67%
mlk_keccak_absorb_once_x4 ✅ 5s 6s -17%
mlk_poly_add ✅ 5s 5s +0%
mlk_poly_ntt ✅ 5s 7s -29%
mlk_polymat_permute_bitrev_to_custom ✅ 5s 4s +25%
mlk_scalar_compress_d1 ✅ 5s 2s +150%
poly_decompress_d4_native_x86_64 ✅ 5s 3s +67%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 4s 1s +300%
mlk_ct_cmask_nonzero_u16 ✅ 4s 2s +100%
mlk_invntt_layer ✅ 4s 3s +33%
mlk_keccak_absorb_once ✅ 4s 4s +0%
mlk_matvec_mul ✅ 4s 4s +0%
mlk_poly_compress_d11 ✅ 4s 1s +300%
mlk_poly_compress_d4_c ✅ 4s 2s +100%
mlk_poly_compress_d4_native ✅ 4s 3s +33%
mlk_poly_compress_d5_native ✅ 4s 3s +33%
mlk_poly_compress_dv ✅ 4s 2s +100%
mlk_poly_decompress_d11 ✅ 4s 3s +33%
mlk_poly_decompress_d4_c ✅ 4s 5s -20%
mlk_poly_decompress_dv ✅ 4s 2s +100%
mlk_poly_frombytes ✅ 4s 2s +100%
mlk_poly_frombytes_c ✅ 4s 5s -20%
mlk_poly_getnoise_eta2 ✅ 4s 2s +100%
mlk_poly_invntt_tomont_c ✅ 4s 3s +33%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 4s 3s +33%
mlk_scalar_decompress_d4 ✅ 4s 1s +300%
mlk_shake256x4 ✅ 4s 4s +0%
mlk_value_barrier_i32 ✅ 4s 2s +100%
poly_compress_d10_native_x86_64 ✅ 4s 2s +100%
poly_getnoise_eta1122_4x_native ✅ 4s 3s +33%
poly_mulcache_compute_native_aarch64 ✅ 4s 1s +300%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 4s 4s +0%
intt_native_x86_64 ✅ 3s 3s +0%
kem_check_pk ✅ 3s 5s -40%
kem_enc ✅ 3s 2s +50%
kem_enc_derand ✅ 3s 4s -25%
mlk_check_pct ✅ 3s 2s +50%
mlk_ct_sel_int16 ✅ 3s 2s +50%
mlk_gen_matrix_serial ✅ 3s 2s +50%
mlk_keccakf1600_extract_bytes ✅ 3s 3s +0%
mlk_keccakf1600x4_extract_bytes_c ✅ 3s 1s +200%
mlk_keccakf1600x4_xor_bytes ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes_c ✅ 3s 2s +50%
mlk_keypair_getnoise_eta1 ✅ 3s 3s +0%
mlk_poly_compress_d11_native ✅ 3s 2s +50%
mlk_poly_compress_d4 ✅ 3s 2s +50%
mlk_poly_compress_d5 ✅ 3s 2s +50%
mlk_poly_decompress_d10 ✅ 3s 3s +0%
mlk_poly_decompress_d10_c ✅ 3s 3s +0%
mlk_poly_decompress_d11_native ✅ 3s 2s +50%
mlk_poly_getnoise_eta1122_4x ✅ 3s 3s +0%
mlk_poly_getnoise_eta1_4x_native ✅ 3s 6s -50%
mlk_poly_mulcache_compute_native ✅ 3s 3s +0%
mlk_poly_ntt_c ✅ 3s 3s +0%
mlk_poly_tobytes ✅ 3s 4s -25%
mlk_poly_tobytes_c ✅ 3s 2s +50%
mlk_poly_tomsg ✅ 3s 2s +50%
mlk_polyvec_permute_bitrev_to_custom ✅ 3s 3s +0%
mlk_polyvec_reduce ✅ 3s 1s +200%
mlk_polyvec_tomont ✅ 3s 2s +50%
mlk_rej_uniform ✅ 3s 3s +0%
mlk_scalar_decompress_d11 ✅ 3s 3s +0%
mlk_scalar_decompress_d5 ✅ 3s 2s +50%
mlk_sha3_256 ✅ 3s 2s +50%
mlk_sha3_512 ✅ 3s 2s +50%
mlk_shake128x4_squeezeblocks ✅ 3s 3s +0%
mlk_shake256 ✅ 3s 2s +50%
ntt_native_x86_64 ✅ 3s 2s +50%
poly_compress_d4_native_x86_64 ✅ 3s 2s +50%
poly_decompress_d11_native_x86_64 ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 3s 3s +0%
rej_uniform_native ✅ 3s 4s -25%
sys_check_capability ✅ 3s 2s +50%
intt_native_aarch64 ✅ 2s 1s +100%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 1s +100%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 2s +0%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native ✅ 2s 3s -33%
keccakf1600x4_xor_bytes_native ✅ 2s 2s +0%
kem_check_sk ✅ 2s 2s +0%
mlk_barrett_reduce ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u8 ✅ 2s 1s +100%
mlk_ct_memcmp ✅ 2s 5s -60%
mlk_keccakf1600_permute ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 1s +100%
mlk_keccakf1600x4_extract_bytes ✅ 2s 3s -33%
mlk_keccakf1600x4_permute ✅ 2s 2s +0%
mlk_montgomery_reduce ✅ 2s 1s +100%
mlk_poly_cbd_eta1 ✅ 2s 2s +0%
mlk_poly_cbd_eta2 ✅ 2s 2s +0%
mlk_poly_compress_d10_c ✅ 2s 2s +0%
mlk_poly_compress_d5_c ✅ 2s 1s +100%
mlk_poly_compress_du ✅ 2s 2s +0%
mlk_poly_decompress_d11_c ✅ 2s 1s +100%
mlk_poly_decompress_d4 ✅ 2s 1s +100%
mlk_poly_decompress_d5_native ✅ 2s 2s +0%
mlk_poly_decompress_du ✅ 2s 4s -50%
mlk_poly_getnoise_eta1_4x ✅ 2s 2s +0%
mlk_poly_invntt_tomont ✅ 2s 1s +100%
mlk_poly_mulcache_compute ✅ 2s 2s +0%
mlk_poly_reduce ✅ 2s 1s +100%
mlk_poly_reduce_c ✅ 2s 4s -50%
mlk_poly_tomont ✅ 2s 3s -33%
mlk_poly_tomont_native ✅ 2s 4s -50%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 2s 2s +0%
mlk_polyvec_decompress_du ✅ 2s 3s -33%
mlk_polyvec_frombytes ✅ 2s 2s +0%
mlk_polyvec_invntt_tomont ✅ 2s 2s +0%
mlk_polyvec_mulcache_compute ✅ 2s 2s +0%
mlk_polyvec_tobytes ✅ 2s 2s +0%
mlk_scalar_compress_d10 ✅ 2s 2s +0%
mlk_scalar_compress_d11 ✅ 2s 1s +100%
mlk_scalar_compress_d5 ✅ 2s 3s -33%
mlk_scalar_signed_to_unsigned_q ✅ 2s 3s -33%
mlk_shake128_absorb_once ✅ 2s 1s +100%
mlk_shake128_squeezeblocks ✅ 2s 1s +100%
mlk_shake128x4_absorb_once ✅ 2s 3s -33%
mlk_value_barrier_u32 ✅ 2s 3s -33%
nttunpack_native_x86_64 ✅ 2s 2s +0%
poly_compress_d11_native_x86_64 ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 ✅ 2s 3s -33%
poly_invntt_tomont_native ✅ 2s 2s +0%
poly_mulcache_compute_native_x86_64 ✅ 2s 3s -33%
poly_reduce_native_aarch64 ✅ 2s 1s +100%
poly_reduce_native_x86_64 ✅ 2s 2s +0%
poly_tomont_native_aarch64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 ✅ 1s 3s -67%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 1s +0%
keccakf1600_permute_native ✅ 1s 3s -67%
kem_keypair ✅ 1s 1s +0%
kem_keypair_derand ✅ 1s 3s -67%
mlk_ct_cmask_neg_i16 ✅ 1s 2s -50%
mlk_ct_get_optblocker_i32 ✅ 1s 2s -50%
mlk_ct_get_optblocker_u32 ✅ 1s 3s -67%
mlk_ct_sel_uint8 ✅ 1s 2s -50%
mlk_gen_matrix ✅ 1s 4s -75%
mlk_keccakf1600_extract_bytes (big endian) ✅ 1s 3s -67%
mlk_keccakf1600_xor_bytes ✅ 1s 1s +0%
mlk_poly_compress_d10 ✅ 1s 2s -50%
mlk_poly_compress_d10_native ✅ 1s 2s -50%
mlk_poly_compress_d11_c ✅ 1s 2s -50%
mlk_poly_decompress_d5 ✅ 1s 2s -50%
mlk_poly_decompress_d5_c ✅ 1s 2s -50%
mlk_poly_mulcache_compute_c ✅ 1s 2s -50%
mlk_poly_tobytes_native ✅ 1s 1s +0%
mlk_poly_tomont_c ✅ 1s 4s -75%
mlk_polyvec_compress_du ✅ 1s 3s -67%
mlk_polyvec_ntt ✅ 1s 4s -75%
mlk_scalar_compress_d4 ✅ 1s 3s -67%
mlk_scalar_decompress_d10 ✅ 1s 2s -50%
mlk_value_barrier_u8 ✅ 1s 2s -50%
ntt_native_aarch64 ✅ 1s 3s -67%
poly_decompress_d5_native_x86_64 ✅ 1s 1s +0%
poly_tobytes_native_aarch64 ✅ 1s 2s -50%
poly_tobytes_native_x86_64 ✅ 1s 4s -75%
poly_tomont_native_x86_64 ✅ 1s 2s -50%

@oqs-bot

oqs-bot commented Jun 30, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1645s 1741s -5.5%
mlk_indcpa_enc ✅ 367s 378s -3%
mlk_indcpa_keypair_derand ✅ 159s 170s -6%
mlk_poly_rej_uniform ✅ 121s 144s -16%
mlk_rej_uniform_c ✅ 119s 125s -5%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 68s 71s -4%
rej_uniform_native_x86_64 ✅ 59s 60s -2%
poly_ntt_native ✅ 39s 40s -3%
mlk_poly_reduce_native ✅ 34s 37s -8%
rej_uniform_native_aarch64 ✅ 33s 38s -13%
mlk_ntt_layer ✅ 29s 34s -15%
polyvec_basemul_acc_montgomery_cached_native ✅ 27s 28s -4%
mlk_keccak_squeezeblocks_x4 ✅ 25s 26s -4%
mlk_polyvec_add ✅ 19s 17s +12%
mlk_fqmul ✅ 16s 16s +0%
keccakf1600x4_permute_native_x4 ✅ 15s 19s -21%
mlk_poly_decompress_d11_native ✅ 12s 15s -20%
mlk_poly_decompress_d5_native ✅ 12s 15s -20%
mlk_indcpa_dec ✅ 11s 12s -8%
mlk_poly_frommsg ✅ 11s 12s -8%
mlk_keccak_squeeze_once ✅ 9s 9s +0%
mlk_poly_sub ✅ 9s 6s +50%
mlk_gen_matrix_serial ✅ 8s 5s +60%
mlk_keccak_squeezeblocks ✅ 8s 9s -11%
mlk_polyvec_ntt ✅ 8s 9s -11%
kem_dec ✅ 7s 6s +17%
mlk_poly_frombytes_native ✅ 7s 7s +0%
mlk_invntt_layer ✅ 6s 5s +20%
mlk_matvec_mul ✅ 6s 3s +100%
mlk_ntt_butterfly_block ✅ 6s 9s -33%
mlk_poly_add ✅ 6s 4s +50%
mlk_gen_matrix ✅ 5s 4s +25%
mlk_keccak_absorb_once ✅ 5s 5s +0%
mlk_keccak_absorb_once_x4 ✅ 5s 7s -29%
mlk_poly_compress_d11 ✅ 5s 2s +150%
mlk_poly_ntt ✅ 5s 7s -29%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 5s 3s +67%
mlk_shake256x4 ✅ 5s 3s +67%
mlk_value_barrier_u32 ✅ 5s 2s +150%
poly_decompress_d11_native_x86_64 ✅ 5s 5s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 4s 2s +100%
kem_enc_derand ✅ 4s 3s +33%
kem_keypair ✅ 4s 4s +0%
mlk_keccakf1600_permute_c ✅ 4s 5s -20%
mlk_keccakf1600_xor_bytes ✅ 4s 3s +33%
mlk_poly_cbd_eta1 ✅ 4s 3s +33%
mlk_poly_compress_d10_c ✅ 4s 3s +33%
mlk_poly_frombytes_c ✅ 4s 5s -20%
mlk_poly_rej_uniform_x4 ✅ 4s 6s -33%
mlk_polymat_permute_bitrev_to_custom ✅ 4s 5s -20%
mlk_polyvec_reduce ✅ 4s 3s +33%
mlk_scalar_compress_d10 ✅ 4s 2s +100%
mlk_scalar_compress_d11 ✅ 4s 3s +33%
mlk_scalar_compress_d5 ✅ 4s 2s +100%
mlk_shake128x4_squeezeblocks ✅ 4s 4s +0%
poly_frombytes_native_x86_64 ✅ 4s 4s +0%
poly_invntt_tomont_native ✅ 4s 4s +0%
poly_tobytes_native_x86_64 ✅ 4s 2s +100%
intt_native_x86_64 ✅ 3s 1s +200%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 4s -25%
keccakf1600_permute_native ✅ 3s 1s +200%
kem_enc ✅ 3s 3s +0%
kem_keypair_derand ✅ 3s 1s +200%
mlk_barrett_reduce ✅ 3s 2s +50%
mlk_check_pct ✅ 3s 3s +0%
mlk_ct_cmask_neg_i16 ✅ 3s 3s +0%
mlk_ct_get_optblocker_u8 ✅ 3s 1s +200%
mlk_keccakf1600_extract_bytes (big endian) ✅ 3s 1s +200%
mlk_keccakf1600x4_xor_bytes ✅ 3s 1s +200%
mlk_poly_decompress_d10_c ✅ 3s 3s +0%
mlk_poly_decompress_d11 ✅ 3s 3s +0%
mlk_poly_decompress_d4_native ✅ 3s 2s +50%
mlk_poly_decompress_d5_c ✅ 3s 1s +200%
mlk_poly_decompress_dv ✅ 3s 2s +50%
mlk_poly_getnoise_eta1_4x ✅ 3s 4s -25%
mlk_poly_getnoise_eta2 ✅ 3s 3s +0%
mlk_poly_invntt_tomont ✅ 3s 2s +50%
mlk_poly_ntt_c ✅ 3s 3s +0%
mlk_poly_reduce_c ✅ 3s 2s +50%
mlk_poly_tobytes ✅ 3s 2s +50%
mlk_poly_tomont_c ✅ 3s 1s +200%
mlk_polyvec_compress_du ✅ 3s 2s +50%
mlk_scalar_compress_d4 ✅ 3s 2s +50%
mlk_scalar_decompress_d10 ✅ 3s 3s +0%
mlk_scalar_decompress_d5 ✅ 3s 2s +50%
mlk_scalar_signed_to_unsigned_q ✅ 3s 2s +50%
ntt_native_aarch64 ✅ 3s 1s +200%
ntt_native_x86_64 ✅ 3s 3s +0%
poly_decompress_d4_native_x86_64 ✅ 3s 3s +0%
poly_decompress_d5_native_x86_64 ✅ 3s 4s -25%
poly_getnoise_eta1122_4x_native ✅ 3s 3s +0%
poly_mulcache_compute_native_x86_64 ✅ 3s 4s -25%
poly_reduce_native_aarch64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 3s 1s +200%
intt_native_aarch64 ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 ✅ 2s 1s +100%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 ✅ 2s 4s -50%
keccakf1600x4_xor_bytes_native ✅ 2s 2s +0%
kem_check_sk ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u16 ✅ 2s 2s +0%
mlk_ct_cmov_zero ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ✅ 2s 2s +0%
mlk_ct_memcmp ✅ 2s 1s +100%
mlk_ct_sel_int16 ✅ 2s 1s +100%
mlk_enc_getnoise_eta1_eta2 ✅ 2s 4s -50%
mlk_keccakf1600_extract_bytes ✅ 2s 4s -50%
mlk_keccakf1600_permute ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 3s -33%
mlk_keccakf1600x4_extract_bytes ✅ 2s 3s -33%
mlk_keccakf1600x4_extract_bytes_c ✅ 2s 3s -33%
mlk_keccakf1600x4_xor_bytes_c ✅ 2s 3s -33%
mlk_keypair_getnoise_eta1 ✅ 2s 5s -60%
mlk_poly_cbd_eta2 ✅ 2s 2s +0%
mlk_poly_compress_d10_native ✅ 2s 2s +0%
mlk_poly_compress_d11_c ✅ 2s 3s -33%
mlk_poly_compress_d11_native ✅ 2s 3s -33%
mlk_poly_compress_d4 ✅ 2s 4s -50%
mlk_poly_compress_d4_c ✅ 2s 2s +0%
mlk_poly_compress_d5_c ✅ 2s 2s +0%
mlk_poly_compress_du ✅ 2s 2s +0%
mlk_poly_decompress_d10 ✅ 2s 2s +0%
mlk_poly_decompress_d10_native ✅ 2s 3s -33%
mlk_poly_decompress_d11_c ✅ 2s 2s +0%
mlk_poly_decompress_d5 ✅ 2s 1s +100%
mlk_poly_frombytes ✅ 2s 2s +0%
mlk_poly_getnoise_eta1122_4x ✅ 2s 2s +0%
mlk_poly_getnoise_eta1_4x_native ✅ 2s 3s -33%
mlk_poly_mulcache_compute ✅ 2s 3s -33%
mlk_poly_mulcache_compute_c ✅ 2s 2s +0%
mlk_poly_mulcache_compute_native ✅ 2s 2s +0%
mlk_poly_reduce ✅ 2s 2s +0%
mlk_poly_tomont ✅ 2s 3s -33%
mlk_poly_tomont_native ✅ 2s 2s +0%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 2s 2s +0%
mlk_polyvec_frombytes ✅ 2s 1s +100%
mlk_polyvec_invntt_tomont ✅ 2s 2s +0%
mlk_polyvec_mulcache_compute ✅ 2s 4s -50%
mlk_polyvec_permute_bitrev_to_custom ✅ 2s 2s +0%
mlk_polyvec_tobytes ✅ 2s 2s +0%
mlk_scalar_compress_d1 ✅ 2s 3s -33%
mlk_scalar_decompress_d11 ✅ 2s 1s +100%
mlk_scalar_decompress_d4 ✅ 2s 2s +0%
mlk_shake128_squeezeblocks ✅ 2s 2s +0%
mlk_shake128x4_absorb_once ✅ 2s 3s -33%
mlk_value_barrier_i32 ✅ 2s 1s +100%
mlk_value_barrier_u8 ✅ 2s 2s +0%
nttunpack_native_x86_64 ✅ 2s 4s -50%
poly_compress_d11_native_x86_64 ✅ 2s 3s -33%
poly_compress_d4_native_x86_64 ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 ✅ 2s 1s +100%
poly_reduce_native_x86_64 ✅ 2s 1s +100%
poly_tomont_native_aarch64 ✅ 2s 2s +0%
poly_tomont_native_x86_64 ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 2s 1s +100%
rej_uniform_native ✅ 2s 5s -60%
sys_check_capability ✅ 2s 2s +0%
keccakf1600x4_extract_bytes_native ✅ 1s 2s -50%
kem_check_pk ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u8 ✅ 1s 3s -67%
mlk_ct_get_optblocker_u32 ✅ 1s 1s +0%
mlk_ct_sel_uint8 ✅ 1s 3s -67%
mlk_keccakf1600x4_permute ✅ 1s 2s -50%
mlk_montgomery_reduce ✅ 1s 1s +0%
mlk_poly_compress_d10 ✅ 1s 1s +0%
mlk_poly_compress_d4_native ✅ 1s 2s -50%
mlk_poly_compress_d5 ✅ 1s 2s -50%
mlk_poly_compress_d5_native ✅ 1s 2s -50%
mlk_poly_compress_dv ✅ 1s 2s -50%
mlk_poly_decompress_d4 ✅ 1s 1s +0%
mlk_poly_decompress_d4_c ✅ 1s 2s -50%
mlk_poly_decompress_du ✅ 1s 3s -67%
mlk_poly_invntt_tomont_c ✅ 1s 2s -50%
mlk_poly_tobytes_c ✅ 1s 1s +0%
mlk_poly_tobytes_native ✅ 1s 2s -50%
mlk_poly_tomsg ✅ 1s 5s -80%
mlk_polyvec_decompress_du ✅ 1s 3s -67%
mlk_polyvec_tomont ✅ 1s 1s +0%
mlk_rej_uniform ✅ 1s 2s -50%
mlk_sha3_256 ✅ 1s 2s -50%
mlk_sha3_512 ✅ 1s 2s -50%
mlk_shake128_absorb_once ✅ 1s 2s -50%
mlk_shake256 ✅ 1s 2s -50%
poly_compress_d10_native_x86_64 ✅ 1s 2s -50%
poly_decompress_d10_native_x86_64 ✅ 1s 3s -67%
poly_mulcache_compute_native_aarch64 ✅ 1s 1s +0%
poly_tobytes_native_aarch64 ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 1s 4s -75%

@oqs-bot

oqs-bot commented Jun 30, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

Full Results (191 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1839s 1679s +9.5%
mlk_indcpa_keypair_derand ✅ 346s 311s +11%
mlk_indcpa_enc ✅ 264s 252s +5%
mlk_poly_rej_uniform ✅ 157s 138s +14%
mlk_rej_uniform_c ✅ 146s 122s +20%
rej_uniform_native_x86_64 ✅ 61s 60s +2%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 52s 50s +4%
poly_ntt_native ✅ 41s 39s +5%
mlk_ntt_layer ✅ 40s 29s +38%
rej_uniform_native_aarch64 ✅ 40s 34s +18%
mlk_poly_reduce_native ✅ 38s 36s +6%
mlk_keccak_squeezeblocks_x4 ✅ 26s 24s +8%
mlk_fqmul ✅ 19s 19s +0%
keccakf1600x4_permute_native_x4 ✅ 17s 16s +6%
mlk_poly_decompress_d10_native ✅ 16s 15s +7%
polyvec_basemul_acc_montgomery_cached_native ✅ 16s 16s +0%
mlk_poly_decompress_d4_native ✅ 15s 14s +7%
mlk_poly_frommsg ✅ 13s 11s +18%
mlk_poly_frombytes_native ✅ 12s 9s +33%
mlk_polyvec_add ✅ 12s 11s +9%
mlk_indcpa_dec ✅ 11s 12s -8%
mlk_ntt_butterfly_block ✅ 9s 6s +50%
mlk_keccak_squeeze_once ✅ 8s 9s -11%
mlk_keccak_squeezeblocks ✅ 8s 7s +14%
kem_dec ✅ 7s 5s +40%
mlk_poly_ntt ✅ 7s 4s +75%
poly_decompress_d10_native_x86_64 ✅ 7s 4s +75%
mlk_keccak_absorb_once_x4 ✅ 6s 6s +0%
mlk_poly_rej_uniform_x4 ✅ 6s 6s +0%
keccak_f1600_x1_native_aarch64 ✅ 5s 1s +400%
kem_keypair_derand ✅ 5s 4s +25%
mlk_keccakf1600_permute_c ✅ 5s 5s +0%
mlk_keccakf1600x4_extract_bytes_c ✅ 5s 1s +400%
mlk_poly_frombytes_c ✅ 5s 5s +0%
mlk_poly_mulcache_compute_c ✅ 5s 4s +25%
mlk_poly_sub ✅ 5s 6s -17%
mlk_polyvec_decompress_du ✅ 5s 4s +25%
poly_decompress_d4_native_x86_64 ✅ 5s 6s -17%
poly_frombytes_native_x86_64 ✅ 5s 6s -17%
intt_native_aarch64 ✅ 4s 1s +300%
keccakf1600_permute_native ✅ 4s 3s +33%
mlk_check_pct ✅ 4s 3s +33%
mlk_invntt_layer ✅ 4s 6s -33%
mlk_matvec_mul ✅ 4s 4s +0%
mlk_poly_add ✅ 4s 3s +33%
mlk_poly_cbd_eta1 ✅ 4s 3s +33%
mlk_poly_compress_d11_native ✅ 4s 2s +100%
mlk_poly_decompress_d11_c ✅ 4s 2s +100%
mlk_poly_decompress_d4_c ✅ 4s 4s +0%
mlk_poly_getnoise_eta1_4x_native ✅ 4s 1s +300%
mlk_poly_invntt_tomont ✅ 4s 1s +300%
mlk_poly_invntt_tomont_c ✅ 4s 3s +33%
mlk_poly_tobytes ✅ 4s 1s +300%
mlk_poly_tomont ✅ 4s 2s +100%
mlk_poly_tomsg ✅ 4s 2s +100%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 4s 2s +100%
mlk_polyvec_reduce ✅ 4s 2s +100%
mlk_polyvec_tomont ✅ 4s 2s +100%
mlk_scalar_compress_d5 ✅ 4s 3s +33%
mlk_shake256 ✅ 4s 2s +100%
poly_mulcache_compute_native_x86_64 ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 4s 1s +300%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 4s 3s +33%
intt_native_x86_64 ✅ 3s 4s -25%
keccak_f1600_x4_native_aarch64_v84a ✅ 3s 1s +200%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 3s 2s +50%
keccakf1600x4_extract_bytes_native ✅ 3s 3s +0%
kem_check_sk ✅ 3s 4s -25%
kem_keypair ✅ 3s 2s +50%
mlk_barrett_reduce ✅ 3s 1s +200%
mlk_ct_cmask_nonzero_u16 ✅ 3s 2s +50%
mlk_ct_get_optblocker_u32 ✅ 3s 4s -25%
mlk_ct_get_optblocker_u8 ✅ 3s 1s +200%
mlk_ct_sel_uint8 ✅ 3s 4s -25%
mlk_gen_matrix_serial ✅ 3s 3s +0%
mlk_keccakf1600x4_extract_bytes ✅ 3s 1s +200%
mlk_montgomery_reduce ✅ 3s 2s +50%
mlk_poly_cbd_eta2 ✅ 3s 1s +200%
mlk_poly_compress_d10 ✅ 3s 1s +200%
mlk_poly_compress_d10_c ✅ 3s 2s +50%
mlk_poly_compress_d11_c ✅ 3s 3s +0%
mlk_poly_compress_d4_native ✅ 3s 2s +50%
mlk_poly_compress_d5 ✅ 3s 2s +50%
mlk_poly_decompress_d10 ✅ 3s 2s +50%
mlk_poly_decompress_d10_c ✅ 3s 4s -25%
mlk_poly_decompress_d4 ✅ 3s 5s -40%
mlk_poly_decompress_d5_c ✅ 3s 2s +50%
mlk_poly_decompress_du ✅ 3s 3s +0%
mlk_poly_getnoise_eta1122_4x ✅ 3s 3s +0%
mlk_poly_getnoise_eta2 ✅ 3s 2s +50%
mlk_poly_mulcache_compute ✅ 3s 2s +50%
mlk_poly_mulcache_compute_native ✅ 3s 2s +50%
mlk_poly_tobytes_native ✅ 3s 1s +200%
mlk_poly_tomont_native ✅ 3s 1s +200%
mlk_polymat_permute_bitrev_to_custom ✅ 3s 3s +0%
mlk_polyvec_frombytes ✅ 3s 3s +0%
mlk_polyvec_ntt ✅ 3s 2s +50%
mlk_polyvec_permute_bitrev_to_custom ✅ 3s 1s +200%
mlk_rej_uniform ✅ 3s 1s +200%
mlk_scalar_compress_d11 ✅ 3s 2s +50%
mlk_scalar_compress_d4 ✅ 3s 1s +200%
mlk_scalar_decompress_d11 ✅ 3s 2s +50%
mlk_sha3_256 ✅ 3s 1s +200%
mlk_shake128_squeezeblocks ✅ 3s 4s -25%
mlk_shake128x4_absorb_once ✅ 3s 2s +50%
mlk_shake128x4_squeezeblocks ✅ 3s 3s +0%
mlk_shake256x4 ✅ 3s 2s +50%
mlk_value_barrier_i32 ✅ 3s 4s -25%
ntt_native_aarch64 ✅ 3s 2s +50%
poly_compress_d10_native_x86_64 ✅ 3s 3s +0%
poly_compress_d4_native_x86_64 ✅ 3s 2s +50%
poly_decompress_d11_native_x86_64 ✅ 3s 5s -40%
poly_getnoise_eta1122_4x_native ✅ 3s 1s +200%
poly_invntt_tomont_native ✅ 3s 4s -25%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 3s 4s -25%
sys_check_capability ✅ 3s 2s +50%
keccak_f1600_x1_native_aarch64_v84a ✅ 2s 3s -33%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 2s +0%
keccak_f1600_x4_native_avx2 ✅ 2s 1s +100%
kem_enc ✅ 2s 2s +0%
kem_enc_derand ✅ 2s 4s -50%
mlk_ct_cmask_neg_i16 ✅ 2s 5s -60%
mlk_ct_get_optblocker_i32 ✅ 2s 1s +100%
mlk_enc_getnoise_eta1_eta2 ✅ 2s 2s +0%
mlk_gen_matrix ✅ 2s 3s -33%
mlk_keccak_absorb_once ✅ 2s 3s -33%
mlk_keccakf1600_extract_bytes ✅ 2s 1s +100%
mlk_keccakf1600_extract_bytes (big endian) ✅ 2s 2s +0%
mlk_keccakf1600_permute ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
mlk_keccakf1600x4_xor_bytes ✅ 2s 1s +100%
mlk_keccakf1600x4_xor_bytes_c ✅ 2s 2s +0%
mlk_keypair_getnoise_eta1 ✅ 2s 2s +0%
mlk_poly_compress_d4_c ✅ 2s 2s +0%
mlk_poly_compress_d5_native ✅ 2s 1s +100%
mlk_poly_compress_dv ✅ 2s 6s -67%
mlk_poly_decompress_d11 ✅ 2s 3s -33%
mlk_poly_decompress_d11_native ✅ 2s 3s -33%
mlk_poly_decompress_d5_native ✅ 2s 4s -50%
mlk_poly_decompress_dv ✅ 2s 3s -33%
mlk_poly_frombytes ✅ 2s 3s -33%
mlk_poly_getnoise_eta1_4x ✅ 2s 2s +0%
mlk_poly_ntt_c ✅ 2s 3s -33%
mlk_poly_reduce ✅ 2s 1s +100%
mlk_poly_reduce_c ✅ 2s 2s +0%
mlk_poly_tomont_c ✅ 2s 2s +0%
mlk_polyvec_compress_du ✅ 2s 3s -33%
mlk_polyvec_invntt_tomont ✅ 2s 2s +0%
mlk_polyvec_mulcache_compute ✅ 2s 3s -33%
mlk_polyvec_permute_bitrev_to_custom_native ✅ 2s 2s +0%
mlk_polyvec_tobytes ✅ 2s 3s -33%
mlk_scalar_compress_d1 ✅ 2s 2s +0%
mlk_scalar_compress_d10 ✅ 2s 2s +0%
mlk_scalar_decompress_d10 ✅ 2s 4s -50%
mlk_scalar_decompress_d4 ✅ 2s 4s -50%
mlk_sha3_512 ✅ 2s 3s -33%
mlk_value_barrier_u32 ✅ 2s 3s -33%
mlk_value_barrier_u8 ✅ 2s 3s -33%
ntt_native_x86_64 ✅ 2s 4s -50%
nttunpack_native_x86_64 ✅ 2s 3s -33%
poly_compress_d11_native_x86_64 ✅ 2s 2s +0%
poly_compress_d5_native_x86_64 ✅ 2s 2s +0%
poly_mulcache_compute_native_aarch64 ✅ 2s 2s +0%
poly_reduce_native_aarch64 ✅ 2s 3s -33%
poly_reduce_native_x86_64 ✅ 2s 3s -33%
poly_tobytes_native_aarch64 ✅ 2s 1s +100%
poly_tobytes_native_x86_64 ✅ 2s 2s +0%
poly_tomont_native_x86_64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 2s 4s -50%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 2s 2s +0%
rej_uniform_native ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native ✅ 1s 1s +0%
kem_check_pk ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u8 ✅ 1s 4s -75%
mlk_ct_cmov_zero ✅ 1s 3s -67%
mlk_ct_memcmp ✅ 1s 3s -67%
mlk_ct_sel_int16 ✅ 1s 2s -50%
mlk_keccakf1600_xor_bytes ✅ 1s 1s +0%
mlk_keccakf1600x4_permute ✅ 1s 2s -50%
mlk_poly_compress_d10_native ✅ 1s 3s -67%
mlk_poly_compress_d11 ✅ 1s 1s +0%
mlk_poly_compress_d4 ✅ 1s 3s -67%
mlk_poly_compress_d5_c ✅ 1s 2s -50%
mlk_poly_compress_du ✅ 1s 3s -67%
mlk_poly_decompress_d5 ✅ 1s 3s -67%
mlk_poly_tobytes_c ✅ 1s 2s -50%
mlk_scalar_decompress_d5 ✅ 1s 2s -50%
mlk_scalar_signed_to_unsigned_q ✅ 1s 2s -50%
mlk_shake128_absorb_once ✅ 1s 2s -50%
poly_decompress_d5_native_x86_64 ✅ 1s 2s -50%
poly_tomont_native_aarch64 ✅ 1s 3s -67%

@mkannwischer mkannwischer added the benchmark this PR should be benchmarked in CI label Jul 1, 2026
oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mac Mini (M1, 2020) benchmarks

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 12315 cycles 12314 cycles 1.00
ML-KEM-512 encaps 14758 cycles 14757 cycles 1.00
ML-KEM-512 decaps 19314 cycles 19311 cycles 1.00
ML-KEM-768 keypair 21263 cycles 21263 cycles 1
ML-KEM-768 encaps 23505 cycles 23505 cycles 1
ML-KEM-768 decaps 30051 cycles 30050 cycles 1.00
ML-KEM-1024 keypair 30315 cycles 30314 cycles 1.00
ML-KEM-1024 encaps 34080 cycles 34081 cycles 1.00
ML-KEM-1024 decaps 43697 cycles 43696 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ppc64le (POWER10) benchmarks

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 37995 cycles 38031 cycles 1.00
ML-KEM-512 encaps 43524 cycles 43673 cycles 1.00
ML-KEM-512 decaps 53817 cycles 53684 cycles 1.00
ML-KEM-768 keypair 67254 cycles 67972 cycles 0.99
ML-KEM-768 encaps 76024 cycles 76571 cycles 0.99
ML-KEM-768 decaps 90493 cycles 91370 cycles 0.99
ML-KEM-1024 keypair 107962 cycles 107764 cycles 1.00
ML-KEM-1024 encaps 118593 cycles 118422 cycles 1.00
ML-KEM-1024 decaps 137483 cycles 136561 cycles 1.01

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 28298 cycles 28237 cycles 1.00
ML-KEM-512 encaps 34164 cycles 34131 cycles 1.00
ML-KEM-512 decaps 44564 cycles 44522 cycles 1.00
ML-KEM-768 keypair 47658 cycles 47593 cycles 1.00
ML-KEM-768 encaps 53936 cycles 53852 cycles 1.00
ML-KEM-768 decaps 68574 cycles 68523 cycles 1.00
ML-KEM-1024 keypair 70415 cycles 70156 cycles 1.00
ML-KEM-1024 encaps 78713 cycles 78679 cycles 1.00
ML-KEM-1024 decaps 98408 cycles 98306 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 4th gen (c7i)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 11773 cycles 11770 cycles 1.00
ML-KEM-512 encaps 13070 cycles 13061 cycles 1.00
ML-KEM-512 decaps 17069 cycles 17026 cycles 1.00
ML-KEM-768 keypair 19382 cycles 19382 cycles 1
ML-KEM-768 encaps 20645 cycles 20586 cycles 1.00
ML-KEM-768 decaps 26544 cycles 26305 cycles 1.01
ML-KEM-1024 keypair 28072 cycles 28114 cycles 1.00
ML-KEM-1024 encaps 30470 cycles 30365 cycles 1.00
ML-KEM-1024 decaps 37798 cycles 37411 cycles 1.01

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 3rd gen (c6a)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 14557 cycles 14446 cycles 1.01
ML-KEM-512 encaps 16074 cycles 15942 cycles 1.01
ML-KEM-512 decaps 21443 cycles 21333 cycles 1.01
ML-KEM-768 keypair 23963 cycles 23765 cycles 1.01
ML-KEM-768 encaps 25383 cycles 25215 cycles 1.01
ML-KEM-768 decaps 33155 cycles 32939 cycles 1.01
ML-KEM-1024 keypair 33667 cycles 33336 cycles 1.01
ML-KEM-1024 encaps 36141 cycles 35874 cycles 1.01
ML-KEM-1024 decaps 46480 cycles 46176 cycles 1.01

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 3rd gen (c6i)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 17923 cycles 17867 cycles 1.00
ML-KEM-512 encaps 20109 cycles 20058 cycles 1.00
ML-KEM-512 decaps 26671 cycles 26645 cycles 1.00
ML-KEM-768 keypair 31585 cycles 29952 cycles 1.05
ML-KEM-768 encaps 32819 cycles 32078 cycles 1.02
ML-KEM-768 decaps 44082 cycles 41435 cycles 1.06
ML-KEM-1024 keypair 42114 cycles 42375 cycles 0.99
ML-KEM-1024 encaps 44628 cycles 45136 cycles 0.99
ML-KEM-1024 decaps 58195 cycles 58003 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Intel Xeon 3rd gen (c6i)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-768 keypair 31585 cycles 29952 cycles 1.05
ML-KEM-768 decaps 44082 cycles 41435 cycles 1.06

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 4th gen (c7a)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 12859 cycles 12795 cycles 1.01
ML-KEM-512 encaps 14269 cycles 14228 cycles 1.00
ML-KEM-512 decaps 19012 cycles 18974 cycles 1.00
ML-KEM-768 keypair 21638 cycles 21547 cycles 1.00
ML-KEM-768 encaps 22776 cycles 22721 cycles 1.00
ML-KEM-768 decaps 29777 cycles 29718 cycles 1.00
ML-KEM-1024 keypair 30797 cycles 30490 cycles 1.01
ML-KEM-1024 encaps 32720 cycles 32665 cycles 1.00
ML-KEM-1024 decaps 41970 cycles 42061 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 27554 cycles 27644 cycles 1.00
ML-KEM-512 encaps 35623 cycles 35655 cycles 1.00
ML-KEM-512 decaps 44504 cycles 44287 cycles 1.00
ML-KEM-768 keypair 44182 cycles 44256 cycles 1.00
ML-KEM-768 encaps 54978 cycles 55139 cycles 1.00
ML-KEM-768 decaps 68345 cycles 68193 cycles 1.00
ML-KEM-1024 keypair 67648 cycles 67860 cycles 1.00
ML-KEM-1024 encaps 79122 cycles 79004 cycles 1.00
ML-KEM-1024 decaps 95874 cycles 96202 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 40251 cycles 40234 cycles 1.00
ML-KEM-512 encaps 48390 cycles 48398 cycles 1.00
ML-KEM-512 decaps 62212 cycles 62216 cycles 1.00
ML-KEM-768 keypair 62728 cycles 62819 cycles 1.00
ML-KEM-768 encaps 75017 cycles 75293 cycles 1.00
ML-KEM-768 decaps 92545 cycles 92353 cycles 1.00
ML-KEM-1024 keypair 95003 cycles 95045 cycles 1.00
ML-KEM-1024 encaps 110032 cycles 109931 cycles 1.00
ML-KEM-1024 decaps 132753 cycles 132385 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 4th gen (c7a) (no-opt)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 36783 cycles 36774 cycles 1.00
ML-KEM-512 encaps 42828 cycles 42816 cycles 1.00
ML-KEM-512 decaps 55578 cycles 55560 cycles 1.00
ML-KEM-768 keypair 58043 cycles 58004 cycles 1.00
ML-KEM-768 encaps 66972 cycles 66910 cycles 1.00
ML-KEM-768 decaps 83573 cycles 83667 cycles 1.00
ML-KEM-1024 keypair 88578 cycles 88511 cycles 1.00
ML-KEM-1024 encaps 99096 cycles 99027 cycles 1.00
ML-KEM-1024 decaps 120507 cycles 120475 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 3rd gen (c6i) (no-opt)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 46772 cycles 46755 cycles 1.00
ML-KEM-512 encaps 55610 cycles 55553 cycles 1.00
ML-KEM-512 decaps 71200 cycles 71195 cycles 1.00
ML-KEM-768 keypair 74381 cycles 74427 cycles 1.00
ML-KEM-768 encaps 85915 cycles 85925 cycles 1.00
ML-KEM-768 decaps 107081 cycles 107032 cycles 1.00
ML-KEM-1024 keypair 111359 cycles 111559 cycles 1.00
ML-KEM-1024 encaps 126065 cycles 126135 cycles 1.00
ML-KEM-1024 decaps 152142 cycles 152221 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton4

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 17729 cycles 17687 cycles 1.00
ML-KEM-512 encaps 20624 cycles 20598 cycles 1.00
ML-KEM-512 decaps 27020 cycles 27004 cycles 1.00
ML-KEM-768 keypair 29954 cycles 29901 cycles 1.00
ML-KEM-768 encaps 32700 cycles 32633 cycles 1.00
ML-KEM-768 decaps 41966 cycles 41918 cycles 1.00
ML-KEM-1024 keypair 43841 cycles 43725 cycles 1.00
ML-KEM-1024 encaps 48793 cycles 48679 cycles 1.00
ML-KEM-1024 decaps 61484 cycles 61384 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton2

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 28274 cycles 28237 cycles 1.00
ML-KEM-512 encaps 34152 cycles 34120 cycles 1.00
ML-KEM-512 decaps 44494 cycles 44477 cycles 1.00
ML-KEM-768 keypair 47695 cycles 47612 cycles 1.00
ML-KEM-768 encaps 53920 cycles 53869 cycles 1.00
ML-KEM-768 decaps 68578 cycles 68555 cycles 1.00
ML-KEM-1024 keypair 70435 cycles 70258 cycles 1.00
ML-KEM-1024 encaps 78748 cycles 78634 cycles 1.00
ML-KEM-1024 decaps 98581 cycles 98283 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton4 (no-opt)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 35298 cycles 35283 cycles 1.00
ML-KEM-512 encaps 40041 cycles 40023 cycles 1.00
ML-KEM-512 decaps 50626 cycles 50624 cycles 1.00
ML-KEM-768 keypair 56805 cycles 56808 cycles 1.00
ML-KEM-768 encaps 64051 cycles 64053 cycles 1.00
ML-KEM-768 decaps 78491 cycles 78497 cycles 1.00
ML-KEM-1024 keypair 87340 cycles 87387 cycles 1.00
ML-KEM-1024 encaps 96702 cycles 96684 cycles 1.00
ML-KEM-1024 decaps 114724 cycles 114714 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton3

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 18736 cycles 18663 cycles 1.00
ML-KEM-512 encaps 21898 cycles 21857 cycles 1.00
ML-KEM-512 decaps 28867 cycles 28843 cycles 1.00
ML-KEM-768 keypair 31634 cycles 31578 cycles 1.00
ML-KEM-768 encaps 34737 cycles 34670 cycles 1.00
ML-KEM-768 decaps 44835 cycles 44807 cycles 1.00
ML-KEM-1024 keypair 46249 cycles 46139 cycles 1.00
ML-KEM-1024 encaps 51597 cycles 51481 cycles 1.00
ML-KEM-1024 decaps 65090 cycles 64967 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton2 (no-opt)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 58718 cycles 58734 cycles 1.00
ML-KEM-512 encaps 68465 cycles 68440 cycles 1.00
ML-KEM-512 decaps 87331 cycles 87340 cycles 1.00
ML-KEM-768 keypair 94966 cycles 94930 cycles 1.00
ML-KEM-768 encaps 109092 cycles 109078 cycles 1.00
ML-KEM-768 decaps 134063 cycles 134029 cycles 1.00
ML-KEM-1024 keypair 151632 cycles 150888 cycles 1.00
ML-KEM-1024 encaps 165983 cycles 165541 cycles 1.00
ML-KEM-1024 decaps 199536 cycles 198797 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A55 (Snapdragon 888) benchmarks

Details
Benchmark suite Current: e5b3150 Previous: 2c72415 Ratio
ML-KEM-512 keypair 59822 cycles 59790 cycles 1.00
ML-KEM-512 encaps 67496 cycles 67441 cycles 1.00
ML-KEM-512 decaps 86491 cycles 86510 cycles 1.00
ML-KEM-768 keypair 97527 cycles 97515 cycles 1.00
ML-KEM-768 encaps 110905 cycles 110878 cycles 1.00
ML-KEM-768 decaps 138093 cycles 137955 cycles 1.00
ML-KEM-1024 keypair 154701 cycles 154924 cycles 1.00
ML-KEM-1024 encaps 171035 cycles 171448 cycles 1.00
ML-KEM-1024 decaps 208068 cycles 208180 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 1, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton3 (no-opt)

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 38914 cycles 38902 cycles 1.00
ML-KEM-512 encaps 44398 cycles 44388 cycles 1.00
ML-KEM-512 decaps 56208 cycles 56210 cycles 1.00
ML-KEM-768 keypair 62482 cycles 62490 cycles 1.00
ML-KEM-768 encaps 70440 cycles 70446 cycles 1.00
ML-KEM-768 decaps 86366 cycles 86371 cycles 1.00
ML-KEM-1024 keypair 95816 cycles 95879 cycles 1.00
ML-KEM-1024 encaps 106129 cycles 106090 cycles 1.00
ML-KEM-1024 decaps 125761 cycles 125742 cycles 1.00

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

@hanno-becker hanno-becker added benchmark this PR should be benchmarked in CI and removed benchmark this PR should be benchmarked in CI labels Jul 6, 2026
oqs-bot
oqs-bot reviewed Jul 6, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

SpacemiT K1 8 (Banana Pi F3) benchmarks

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 143055 cycles 143022 cycles 1.00
ML-KEM-512 encaps 151409 cycles 151363 cycles 1.00
ML-KEM-512 decaps 189755 cycles 189643 cycles 1.00
ML-KEM-768 keypair 233079 cycles 233081 cycles 1.00
ML-KEM-768 encaps 250313 cycles 250329 cycles 1.00
ML-KEM-768 decaps 304923 cycles 304928 cycles 1.00
ML-KEM-1024 keypair 365633 cycles 365497 cycles 1.00
ML-KEM-1024 encaps 388961 cycles 387803 cycles 1.00
ML-KEM-1024 decaps 459330 cycles 458211 cycles 1.00

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

oqs-bot
oqs-bot reviewed Jul 6, 2026
View reviewed changes

@oqs-bot oqs-bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A72 (Raspberry Pi 4) benchmarks

Details
Benchmark suite Current: e5b3150 Previous: 799592d Ratio
ML-KEM-512 keypair 51160 cycles 50970 cycles 1.00
ML-KEM-512 encaps 59082 cycles 59151 cycles 1.00
ML-KEM-512 decaps 75325 cycles 75254 cycles 1.00
ML-KEM-768 keypair 86678 cycles 86259 cycles 1.00
ML-KEM-768 encaps 96230 cycles 94881 cycles 1.01
ML-KEM-768 decaps 117701 cycles 117239 cycles 1.00
ML-KEM-1024 keypair 131729 cycles 131888 cycles 1.00
ML-KEM-1024 encaps 143492 cycles 142478 cycles 1.01
ML-KEM-1024 decaps 174559 cycles 174909 cycles 1.00

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

@tob-joe @codex
Clear ML-KEM Keccak stack scratch
eaa8092 
Wipe the AVX2, AArch64 scalar-hybrid, and Armv8.1-M MVE x4 Keccak
scratch frames before returning, and refresh the covered HOL Light proof
copies for the changed instruction streams.

This keeps state-derived stack scratch from surviving past the permutation
return path.

Verification:

- nix develop .#hol_light-cross-aarch64 -c make -B -C proofs/hol_light/aarch64 mlkem/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.correct

- nix develop .#hol_light-cross-aarch64 -c make -B -C proofs/hol_light/aarch64 mlkem/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.correct

- nix develop .#hol_light-cross-x86_64 -c make -B -C proofs/hol_light/x86_64 mlkem/keccak_f1600_x4_avx2_asm.correct

Co-authored-by: Codex <codex@openai.com>
Signed-off-by: Joe Doyle <joseph.doyle@trailofbits.com>
@tob-joe @codex
Sync ML-KEM Keccak generated wipes
dec107c 
Regenerate the forced-cross Keccak outputs after adding stack clearing to the shared x4 source. The aarch64 host-local autogen path skipped the x86_64 generated files, but CI regenerates them on x86_64 and with forced cross toolchains.

This expands the generated wipe-store blocks in the checked-in Armv8.1-M and x86_64 outputs so the native autogen and HOL-Light bytecode dry-run checks agree with the source.

Co-authored-by: Codex <codex@openai.com>
Signed-off-by: Joe Doyle <joseph.doyle@trailofbits.com>
@tob-joe tob-joe force-pushed the ptp/mlkem-clear-keccak-stack-scratch branch from e5b3150 to dec107c Compare July 7, 2026 21:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@oqs-bot oqs-bot oqs-bot left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

benchmark this PR should be benchmarked in CI needs-mldsa-native-port

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@tob-joe @oqs-bot @mkannwischer @hanno-becker