Skip to content

CI: Bump EC2 AMIs to Ubuntu 26.04 LTS - #1883

Open
mkannwischer wants to merge 1 commit into
mainfrom
ci-ami-ubuntu-2604
Open

CI: Bump EC2 AMIs to Ubuntu 26.04 LTS#1883
mkannwischer wants to merge 1 commit into
mainfrom
ci-ami-ubuntu-2604

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

The stock AMIs used by the EC2 runners were 24.04 images, the ones for the CI and benchmarking runners built as far back as August 2024. Bump them all to the current 26.04 LTS images in us-east-1 (release 20260819).

Also rename AMI_UBUNTU_LATEST_* to AMI_UBUNTU_* and the AMI selector strings from "ubuntu-latest (...)" to "ubuntu (...)": the AMIs are pinned, so "latest" was never accurate. The Ubuntu version, the architecture and the region are now recorded in a comment next to each AMI ID instead.

The custom AMI in ci.yml (docker images preinstalled) is unchanged.

@mkannwischer
CI: Bump EC2 AMIs to Ubuntu 26.04 LTS
c2691ec 
The stock AMIs used by the EC2 runners were 24.04 images, the ones for
the CI and benchmarking runners built as far back as August 2024. Bump
them all to the current 26.04 LTS images in us-east-1 (release
20260819).

Also rename AMI_UBUNTU_LATEST_* to AMI_UBUNTU_* and the AMI selector
strings from "ubuntu-latest (...)" to "ubuntu (...)": the AMIs are
pinned, so "latest" was never accurate. The Ubuntu version, the
architecture and the region are now recorded in a comment next to each
AMI ID instead.

The custom AMI in ci.yml (docker images preinstalled) is unchanged.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@oqs-bot

oqs-bot commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

⚠️ Attention Required

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

@mkannwischer
mkannwischer marked this pull request as ready for review August 28, 2026 15:21
@mkannwischer
mkannwischer requested a review from a team as a code owner August 28, 2026 15:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mkannwischer @oqs-bot