Skip to content

CI: lint: output errors#1639

Merged
mkannwischer merged 1 commit intomainfrom
CI-lint-improve
Apr 2, 2026
Merged

CI: lint: output errors#1639
mkannwischer merged 1 commit intomainfrom
CI-lint-improve

Conversation

@L-series
Copy link
Copy Markdown
Contributor

@L-series L-series commented Mar 23, 2026 •
edited by mkannwischer
Loading

@L-series L-series force-pushed the CI-lint-improve branch 8 times, most recently from 66c3c6c to 4fa2a36 Compare March 23, 2026 17:05
@L-series L-series marked this pull request as ready for review March 23, 2026 17:07
@L-series L-series requested a review from a team as a code owner March 23, 2026 17:07
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Mar 23, 2026 •
edited
Loading

CBMC Results (ML-KEM-512)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Mar 23, 2026 •
edited
Loading

CBMC Results (ML-KEM-1024)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Mar 23, 2026 •
edited
Loading

CBMC Results (ML-KEM-768)

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

@L-series L-series mentioned this pull request Mar 25, 2026
Merged
mkannwischer
mkannwischer approved these changes Apr 2, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

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

Thanks @L-series. LGTM!

@L-series @mkannwischer
CI: lint: output errors
86d2035 
This commit accumulates the names of the checks which have failed while
linting and exposes them to the outer context window in order to guide
the user.

Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
@mkannwischer mkannwischer self-assigned this Apr 2, 2026
@mkannwischer mkannwischer merged commit 4165ea0 into main Apr 2, 2026
370 checks passed
@mkannwischer mkannwischer deleted the CI-lint-improve branch April 2, 2026 08:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer approved these changes

Assignees

@mkannwischer mkannwischer

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Improve output of lint script in CI

3 participants

@L-series @oqs-bot @mkannwischer