Skip to content

Fix build for MLK_CONFIG_NO_RANDOMIZED_API - #1816

Draft
hanno-becker wants to merge 5 commits into
mainfrom
no-randomized
Draft

Fix build for MLK_CONFIG_NO_RANDOMIZED_API#1816
hanno-becker wants to merge 5 commits into
mainfrom
no-randomized

Conversation

@hanno-becker

@hanno-becker hanno-becker commented Jul 26, 2026

Copy link
Copy Markdown
Contributor

@oqs-bot

oqs-bot commented Jul 26, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

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

@oqs-bot

oqs-bot commented Jul 26, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

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

@oqs-bot

oqs-bot commented Jul 26, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

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

@hanno-becker
hanno-becker force-pushed the no-randomized branch 3 times, most recently from e22e7c3 to bae7641 Compare July 27, 2026 06:30
@hanno-becker
Make tests and examples compatible with reduced-API configurations
7813dd1 
Add MLK_CONFIG_NO_KEYPAIR_API, MLK_CONFIG_NO_ENCAPS_API and
MLK_CONFIG_NO_DECAPS_API, and guard public and internal APIs accordingly.

Generate deterministic KEM vectors so tests and examples can exercise each
enabled operation independently. Adapt ACVP, Wycheproof, allocation, RNG
failure and stack tests to reduced builds; stack analysis measures only
enabled APIs.

Cover all non-empty reduced API combinations in CI.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
ACVP: Filter unsupported functions from test cases
1f3f0cd 
The previous encapDecap-file gate only loaded the file when all four
sub-functions (encapsulation, decapsulation, encapsulationKeyCheck,
decapsulationKeyCheck) were compiled in. Under encaps-only, decaps-only,
keygen-encaps, and keygen-decaps configurations that skipped the entire
prompt file, so ACVP reported OK while driving zero test cases through
the binary.

This commit intead loads the encapDecap file whenever _any_ of its
sub-functions are supported, and drops unsupported test cases via a
filter that mutates both the prompt and the expectedResults data
consistently. This mirrors the filter_test_cases machinery introduced
for the same reason in mldsa-native (PR #1140).

Reduced-API runs also now emit a labelled stderr summary block after
"ALL GOOD!" for both whole-prompt skips and per-test drops, so coverage
gaps aren't buried in scrollback. Full-API runs stay silent.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
AVR: Bump simavr RAM to 63.5K to fix ML-KEM-1024 stack overflow
faa87c7 
The test vectors added in the last commit lead to a stack overflow
on AVR for ML-KEM-1024.

This commit ports the AVR setup from mldsa-native, including its
increase in RAM to nearly 64K.

This fixes the AVR test, and also makes future maintenance of
the AVR backend across mlkem-native and mldsa-native simpler.

- nix/avr: RAMEND 0x81FF -> 0xFFFF, EEPROM E2END 0x3FFF -> 0x7FFF
- platform.mk: __stack=0x81FF -> __DATA_REGION_LENGTH__=0xFC00, so .data/.bss
  grow up from 0x0200 with the stack set at runtime
- avr_wrapper.c / init7.S / exec_wrapper.py: place the argc/argv block at the
  top of RAM and set SP just below it, giving the largest possible stack

Keeping this identical (modulo naming) to mldsa-native lets both projects
share one AVR baremetal harness, so fixes port across as a prefix diff.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
Functional test: Fix build for MLK_CONFIG_NO_RANDOMIZED_API
7a48221 
The reduced-API refactor guarded the randomized round-trip tests in
test_mlkem.c on !NO_KEYPAIR_API && !NO_ENCAPS_API && !NO_DECAPS_API, but
omitted !NO_RANDOMIZED_API. The public header only exposes
crypto_kem_keypair() and crypto_kem_enc() when NO_RANDOMIZED_API is
unset (nested inside the keypair/encaps API guards), so a plain
CFLAGS="-DMLK_CONFIG_NO_RANDOMIZED_API" make failed to compile
test_mlkem.c with implicit-declaration errors.

Add the missing !NO_RANDOMIZED_API term to both guard blocks, matching
the pattern already used in test_stack.c, test_rng_fail.c and
test_alloc.c. The deterministic test_kem_expected_* vectors keep
exercising keygen/encaps/decaps under NO_RANDOMIZED_API; only the
randomized round-trip loop is compiled out.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
@hanno-becker
CI: Add config variation for MLK_CONFIG_NO_RANDOMIZED_API
579cce3 
The deterministic-only build (MLK_CONFIG_NO_RANDOMIZED_API) had no
coverage in the config-variations matrix, which is how the test_mlkem.c
build regression went unnoticed.

Add a "no-randomized" variation that builds and runs func, kat, acvp,
wycheproof, stack and rng_fail under the flag, mirroring the reduced-API
entries. Examples are included except basic_deterministic, which already
sets the flag in its own config and would otherwise trip -Wmacro-redefined.
The alloc test is disabled: its exact high-watermark check assumes the
randomized wrappers, whose coins buffer is absent from the
deterministic-only allocation profile.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
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.

Functional test (test_mlkem.c) fails to build for MLK_CONFIG_NO_RANDOMIZED_API

2 participants

@hanno-becker @oqs-bot