Wycheproof: Fix incorrect assertion for invalid encaps/decaps tests by mkannwischer · Pull Request #1636 · pq-code-package/mlkem-native

mkannwischer · 2026-03-23T05:45:38Z

The encaps and combined test functions asserted that K should NOT match the expected value for invalid test cases where the binary succeeded. This is wrong: for invalid inputs, the binary should reject the input via input validation, not succeed and produce a different K.

Fix this by restructuring all test functions to branch on tc["result"] first, then verify the binary's behavior:

"invalid": assert the binary rejected the input (_error or decode_error)
"valid": assert outputs match expected values
anything else: fail with unexpected result

Additional changes:

Remove "acceptable" as a result type (not used in any test vectors)
In keygen_seed tests, only "valid" results exist; simplify accordingly
In semi_expanded_decaps tests, assert that invalid tests are rejected rather than silently ignoring errors on valid tests
In combined tests, distinguish keygen decode errors from runtime errors, and always verify ek when keygen succeeds

oqs-bot · 2026-03-23T06:11:08Z

CBMC Results (ML-KEM-512)

Full Results (191 proofs)

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

oqs-bot · 2026-03-23T06:11:55Z

CBMC Results (ML-KEM-768)

Full Results (191 proofs)

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

oqs-bot · 2026-03-23T06:13:28Z

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)

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

hanno-becker

One nit, otherwise it looks good. Thank you very much for catching this!

The encaps and combined test functions asserted that K should NOT match the expected value for invalid test cases where the binary succeeded. This is wrong: for invalid inputs, the binary should reject the input via input validation, not succeed and produce a different K. Fix this by restructuring all test functions to branch on tc["result"] first, then verify the binary's behavior: - "invalid": assert the binary rejected the input (_error or decode_error) - "valid": assert outputs match expected values - anything else: fail with unexpected result Additional changes: - Remove "acceptable" as a result type (not used in any test vectors) - In keygen_seed tests, only "valid" results exist; simplify accordingly - In semi_expanded_decaps tests, assert that invalid tests are rejected rather than silently ignoring errors on valid tests - In combined tests, distinguish keygen decode errors from runtime errors, and always verify ek when keygen succeeds Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

hanno-becker

@mkannwischer LGTM. Please check my edit and feel free to merge then.

mkannwischer force-pushed the fix-wycheproof-test-assertions branch from f2e623f to a87dddf Compare March 23, 2026 05:48

mkannwischer marked this pull request as ready for review March 23, 2026 06:15

mkannwischer requested a review from a team as a code owner March 23, 2026 06:15

mkannwischer force-pushed the fix-wycheproof-test-assertions branch from a87dddf to 9a37576 Compare March 23, 2026 10:32

mkannwischer assigned hanno-becker Apr 2, 2026

hanno-becker reviewed Apr 4, 2026

View reviewed changes

Comment thread test/wycheproof/wycheproof_client.py

hanno-becker reviewed Apr 4, 2026

View reviewed changes

Comment thread test/wycheproof/wycheproof_client.py Outdated

hanno-becker reviewed Apr 4, 2026

View reviewed changes

Comment thread test/wycheproof/wycheproof_client.py Outdated

hanno-becker requested changes Apr 4, 2026

View reviewed changes

hanno-becker force-pushed the fix-wycheproof-test-assertions branch from 9a37576 to b98e73a Compare April 18, 2026 04:39

hanno-becker approved these changes Apr 18, 2026

View reviewed changes

mkannwischer merged commit f5d3230 into main Apr 18, 2026
385 checks passed

mkannwischer deleted the fix-wycheproof-test-assertions branch April 18, 2026 10:00

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Wycheproof: Fix incorrect assertion for invalid encaps/decaps tests#1636

Wycheproof: Fix incorrect assertion for invalid encaps/decaps tests#1636
mkannwischer merged 1 commit intomainfrom
fix-wycheproof-test-assertions

mkannwischer commented Mar 23, 2026

Uh oh!

oqs-bot commented Mar 23, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Mar 23, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Mar 23, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hanno-becker left a comment

Uh oh!

hanno-becker left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

mkannwischer commented Mar 23, 2026

Uh oh!

oqs-bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-512)

Uh oh!

oqs-bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-768)

Uh oh!

oqs-bot commented Mar 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oqs-bot commented Mar 23, 2026 •

edited

Loading

oqs-bot commented Mar 23, 2026 •

edited

Loading

oqs-bot commented Mar 23, 2026 •

edited

Loading