Skip to content

Format: Don't allow tabs#1573

Merged
hanno-becker merged 4 commits intomainfrom
tabs
Mar 13, 2026
Merged

Format: Don't allow tabs#1573
hanno-becker merged 4 commits intomainfrom
tabs

Conversation

@mkannwischer
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer commented Feb 20, 2026

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 20, 2026 •
edited
Loading

CBMC Results (ML-KEM-512)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 20, 2026 •
edited
Loading

CBMC Results (ML-KEM-768)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Feb 20, 2026 •
edited
Loading

CBMC Results (ML-KEM-1024)

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

@mkannwischer mkannwischer marked this pull request as ready for review February 20, 2026 11:27
@mkannwischer mkannwischer requested a review from a team as a code owner February 20, 2026 11:27
@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented Feb 25, 2026

Let's hold this back until we have merged #1543 and #1545.

@mkannwischer mkannwischer marked this pull request as draft February 25, 2026 13:18
@hanno-becker
Copy link
Copy Markdown
Contributor

hanno-becker commented Mar 9, 2026

Let's hold this back until we have merged #1543 and #1545.

Those are merged now. Removing DO-NOT-MERGE.

@mkannwischer mkannwischer marked this pull request as ready for review March 13, 2026 08:57
@mkannwischer
simpasm: Replace tabs with spaces in disassembly output
f3059d2 
objdump uses tabs between mnemonics and operands. Expand them to
spaces so that auto-generated assembly files are tab-free.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
@mkannwischer
Lint/Format: Replace tabs in source files
5f3bec6 
Add an expand-tabs step to scripts/format and a tab-check to
scripts/lint. Makefiles, patches, and assembly (.S) are excluded.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
@mkannwischer
x86_64: Remove tabs from x86_64 dev assembly sources
cfd6dcd 
Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
@mkannwischer
Fix missing .PHONY declarations in Makefiles
43f7cf2 
Add missing .PHONY targets found via checkmake.
checkmake is not added to the lint pipeline due to many false
positives.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
hanno-becker
hanno-becker reviewed Mar 13, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@hanno-becker hanno-becker left a comment

Choose a reason for hiding this comment

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

Should we also set UseTab: Never in .clang-format to prevent formatting-introduced tabs?

@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented Mar 13, 2026

Should we also set UseTab: Never in .clang-format to prevent formatting-introduced tabs?

Isn't that already the case when you do BasedOnStyle: Google?

@hanno-becker
Copy link
Copy Markdown
Contributor

hanno-becker commented Mar 13, 2026

@mkannwischer Good point, you are right.

@hanno-becker hanno-becker merged commit d04cf7a into main Mar 13, 2026
410 checks passed
@hanno-becker hanno-becker deleted the tabs branch March 13, 2026 11:43
mkannwischer added a commit to pq-code-package/mldsa-native that referenced this pull request Apr 6, 2026
@mkannwischer
Port: Replace tabs by spaces
1c3a469 
This commit ports pq-code-package/mlkem-native#1573.
It replaces tabs by spaces in
 - All autogenerated asm via simpasm
 - All handwritten asm
 - All c/h source files

It also extends the format and lint script to enforce the absense of tabs
in source files.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
@mkannwischer mkannwischer mentioned this pull request Apr 6, 2026
Merged
mkannwischer added a commit to pq-code-package/mldsa-native that referenced this pull request Apr 22, 2026
@mkannwischer
Port: Replace tabs by spaces
c22c554 
This commit ports pq-code-package/mlkem-native#1573.
It replaces tabs by spaces in
 - All autogenerated asm via simpasm
 - All handwritten asm
 - All c/h source files

It also extends the format and lint script to enforce the absense of tabs
in source files.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
mkannwischer added a commit to pq-code-package/mldsa-native that referenced this pull request Apr 22, 2026
@mkannwischer
Port: Replace tabs by spaces
7eb2927 
This commit ports pq-code-package/mlkem-native#1573.
It replaces tabs by spaces in
 - All autogenerated asm via simpasm
 - All handwritten asm
 - All c/h source files

It also extends the format and lint script to enforce the absense of tabs
in source files.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
mkannwischer added a commit to pq-code-package/mldsa-native that referenced this pull request Apr 22, 2026
@mkannwischer
Port: Replace tabs by spaces
55c9fb6 
This commit ports pq-code-package/mlkem-native#1573.
It replaces tabs by spaces in
 - All autogenerated asm via simpasm
 - All handwritten asm
 - All c/h source files

It also extends the format and lint script to enforce the absense of tabs
in source files.

Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hanno-becker hanno-becker hanno-becker approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

format: Don't allow tabs

3 participants

@mkannwischer @oqs-bot @hanno-becker