Skip to content

Make tests and examples compatible with reduced-API configurations - #1787

Open
hanno-becker wants to merge 3 commits into
mainfrom
unused_apis
Open

Make tests and examples compatible with reduced-API configurations#1787
hanno-becker wants to merge 3 commits into
mainfrom
unused_apis

Conversation

@hanno-becker

Copy link
Copy Markdown
Contributor
The previous tests and examples assumed all APIs (keygen, encaps,
decaps) were always available: encaps tests generated a keypair as
setup, decaps tests generated a keypair and ciphertext as setup, and
the alloc test required keygen for every test function. This made them
incompatible with reduced-API configurations where some APIs are
disabled via MLK_CONFIG_NO_KEYPAIR_API, MLK_CONFIG_NO_ENCAPS_API, or
MLK_CONFIG_NO_DECAPS_API.

This commit introduces auto-generated test vectors and refactors all
tests and examples so that each operation (keygen, encaps, decaps) can
be tested independently using pre-computed test vectors.

scripts/notrandombytes:
- Add Python implementation of the SURF-based deterministic test PRNG,
  matching the C version in test/notrandombytes/
- Used by autogen --test-vectors to generate reproducible randomness
  for test vector generation

Test vector generation (scripts/autogen --test-vectors):
- Add --test-vectors flag to scripts/autogen that invokes the ACVP
  binaries with randomness from scripts/notrandombytes to generate
  test/test_vectors/expected_test_vectors.h and the multilevel variant
- Generate pk, sk, ct, ss vectors for all three parameter sets
  (512, 768, 1024)
- Include z, d, m byte-arrays in the header so consumers don't need
  to hardcode them
- Array dimensions are explicit in the generated header

Test changes (test_mlkem.c):
- The existing tests (test_keys, test_invalid_pk, etc.) require all
  three APIs and are left unchanged, guarded by
  !MLK_CONFIG_NO_KEYPAIR_API && !MLK_CONFIG_NO_ENCAPS_API &&
  !MLK_CONFIG_NO_DECAPS_API
- Add test_kem_expected() as a new minimal test that works in
  reduced-API configurations: each block (keygen, encaps, decaps) is
  independently guarded and uses test vectors directly, so e.g. the
  decaps block can run without keygen by using test_vector_sk

test_alloc.c and test_rng_fail.c:
- Both files exercise the same 7 API entry points (keypair_derand,
  keypair, enc_derand, enc, check_pk, dec, check_sk), each
  independently guarded by the minimal required API
- Encaps tests use test_vector_pk directly (no keygen dependency)
- Decaps tests use test_vector_sk/ct directly (no keygen or encaps
  dependency)
- main() uses r |= pattern for error accumulation

test_stack.c:
- Guard each test function (keygen/encaps/decaps stack measurement)
  by the matching API config; unavailable modes print SKIPPED

gen_KAT/wycheproof/acvp:
- KAT and Wycheproof stub out to a SKIPPED main() when any API is
  disabled (they inherently need all three)
- ACVP guards each mode (keyGen / encapDecap encapsulation /
  encapDecap decapsulation / encapsulationKeyCheck /
  decapsulationKeyCheck) by the matching API config, so it builds
  and works in any subset

Example refactoring:
- Hoist test logic into static example_xxx() functions with
  #if/#else/#endif guards and SKIPPED stubs for disabled APIs
- main() is a flat sequence of r |= example_xxx() calls
- example_end_to_end runs the full keygen->encaps->decaps flow only
  when all three APIs are enabled; example_expected_vectors runs
  independent keygen/encaps/decaps KAT checks for whichever APIs are
  enabled
- Multilevel examples use per-level static functions (test_expected_512,
  test_expected_768, test_expected_1024) with the same per-API guards
- basic_deterministic uses test_vector_z/d/m from the header instead
  of hardcoded byte arrays
- Add expected_test_vectors.h symlink (single- or multi-level) in each
  example directory pointing to test/test_vectors/

CI (config-variations):
- Add keygen-only, encaps-only, decaps-only, keygen-encaps, keygen-decaps,
  encaps-decaps test configurations, covering all 6 combinations of
  1 or 2 enabled APIs from {keygen, encaps, decaps}

@hanno-becker hanno-becker changed the title Unused apis Make tests and examples compatible with reduced-API configurations Jul 6, 2026
@hanno-becker hanno-becker added this to the v2 milestone Jul 6, 2026
@oqs-bot

oqs-bot commented Jul 6, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-512)

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

@oqs-bot

oqs-bot commented Jul 6, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-768)

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

@oqs-bot

oqs-bot commented Jul 6, 2026

Copy link
Copy Markdown
Contributor

CBMC Results (ML-KEM-1024)

⚠️ Attention Required

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

@hanno-becker
hanno-becker force-pushed the unused_apis branch 5 times, most recently from abfdabf to 8794d26 Compare July 8, 2026 09:40
@hanno-becker
hanno-becker marked this pull request as ready for review July 8, 2026 12:40
@hanno-becker
hanno-becker requested a review from a team as a code owner July 8, 2026 12:40
@hanno-becker
hanno-becker marked this pull request as draft July 8, 2026 12:40
Comment thread test/src/test_mlkem.c Outdated
Comment thread test/src/test_mlkem.c Outdated
Comment thread mlkem/src/kem.c
@hanno-becker
hanno-becker force-pushed the unused_apis branch 3 times, most recently from ef7eb6d to bc56136 Compare July 14, 2026 14:53
@hanno-becker
hanno-becker marked this pull request as ready for review July 23, 2026 04:06
@hanno-becker
hanno-becker force-pushed the unused_apis branch 4 times, most recently from d23daba to 2d30400 Compare July 24, 2026 08:11

@mkannwischer mkannwischer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks @hanno-becker for implementing this feature and aligning with mlkem-native.
CI isn't quite happy yet.

Comment thread test/src/test_mlkem.c
Comment thread test/src/test_mlkem.c Outdated
@hanno-becker
hanno-becker force-pushed the unused_apis branch 2 times, most recently from 4385b2b to bc32bf8 Compare July 25, 2026 08:21
@hanno-becker
hanno-becker force-pushed the unused_apis branch 2 times, most recently from be70cad to a9ebd9a Compare July 27, 2026 05:58
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>
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>
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

Copy link
Copy Markdown
Contributor Author

@mkannwischer Thank you for your review, I believe I have addressed your feedback. Can you re-review?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants