Skip to content

FIPS202: Consolidate backend MLK_USE_NATIVE_* flags - #1775

Open
mkannwischer wants to merge 1 commit into
mainfrom
consolidate-native-flags
Open

FIPS202: Consolidate backend MLK_USE_NATIVE_* flags#1775
mkannwischer wants to merge 1 commit into
mainfrom
consolidate-native-flags

Conversation

@mkannwischer

@mkannwischer mkannwischer commented Jul 1, 2026

Copy link
Copy Markdown
Contributor

Rename the FIPS202 backend function-support flags to the MLK_USE_NATIVE_ convention already used by the arithmetic backend:

MLK_USE_FIPS202_X1_NATIVE -> MLK_USE_NATIVE_FIPS202_X1
MLK_USE_FIPS202_X4_NATIVE -> MLK_USE_NATIVE_FIPS202_X4
MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE -> MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES
MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE -> MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES

Custom backends that set these flags must rename them accordingly.

@mkannwischer
FIPS202: Consolidate backend MLK_USE_NATIVE_* flags
2424b23 
Rename the FIPS202 backend function-support flags to the
MLK_USE_NATIVE_<function> convention already used by the arithmetic
backend:

  MLK_USE_FIPS202_X1_NATIVE               -> MLK_USE_NATIVE_FIPS202_X1
  MLK_USE_FIPS202_X4_NATIVE               -> MLK_USE_NATIVE_FIPS202_X4
  MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE     -> MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES
  MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE -> MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES

Custom backends that set these flags must rename them accordingly.

 - Ports pq-code-package/mldsa-native#1207

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

oqs-bot commented Jul 1, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

⚠️ Attention Required

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

@oqs-bot

oqs-bot commented Jul 1, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

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

@oqs-bot

oqs-bot commented Jul 1, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

⚠️ Attention Required

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

@mkannwischer
mkannwischer marked this pull request as ready for review July 1, 2026 07:09
@mkannwischer
mkannwischer requested a review from a team as a code owner July 1, 2026 07:09
@mkannwischer

mkannwischer commented Jul 2, 2026

Copy link
Copy Markdown
Contributor Author

Thanks for the review @hanno-becker. What's blocking the merge?

@hanno-becker hanno-becker added this to the v2 milestone Jul 6, 2026
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

API-BREAK DO-NOT-MERGE

Projects

None yet

Milestone

v2

Development

Successfully merging this pull request may close these issues.

Consolidate backend MLK_USE_XXX flags indicating function support

3 participants

@mkannwischer @oqs-bot @hanno-becker