Skip to content

Add kat test Windows support (C backend only)#1698

Open
willieyz wants to merge 1 commit into
mainfrom
win-sup-kat
Open

Add kat test Windows support (C backend only)#1698
willieyz wants to merge 1 commit into
mainfrom
win-sup-kat

Conversation

@willieyz
Copy link
Copy Markdown
Contributor

@willieyz willieyz commented May 18, 2026 •
edited
Loading

This PR adds Windows support for the C backend KAT tests.

Currently, Unix KAT tests rely on shell pipelines (sha256sum, cut, xargs) not available on Windows.
Introduce test/src/kat_client.py, a Python script that runs gen_KAT binaries, SHA-256-hashes their stdout, and checks against META.yml, replacing the shell one-liner for each security level:

 set -o pipefail; $W $MLKEM512_DIR/bin/gen_KAT512 | $SHA256SUM | \ cut -d " " -f 1 | xargs ./META.sh ML-KEM-512 kat-sha256

Also, refactor gen_KAT{512,768,1024}, gen_KAT, run_kat in Makefile.Microsoft_nmake. now quickcheck align with Unix Makefile.

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 18, 2026 •
edited
Loading

CBMC Results (ML-KEM-768)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 18, 2026 •
edited
Loading

CBMC Results (ML-KEM-512)

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

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented May 18, 2026 •
edited
Loading

CBMC Results (ML-KEM-1024)

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

@willieyz willieyz marked this pull request as ready for review May 19, 2026 03:40
@willieyz willieyz requested a review from a team as a code owner May 19, 2026 03:40
@willieyz willieyz requested a review from mkannwischer May 19, 2026 03:40
mkannwischer
mkannwischer reviewed May 20, 2026
View reviewed changes
Comment thread test/src/kat_client.py
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer May 20, 2026

Choose a reason for hiding this comment

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

I'm not a fan of introducing a second way of running KAT tests.

@hanno-becker, would it be an option to also migrate the other KAT tests to use a Python wrapper?

mkannwischer
mkannwischer requested changes May 22, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer left a comment

Choose a reason for hiding this comment

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

@willieyz, I have discussed this with @hanno-becker: We want to keep KAT checking uniform across platforms. I think the Python approach you have picked is likely the most portable. Could you also switch the Makefile to use that script? Please also clean up all unnecessary files that won't be needed anymore then.

@mkannwischer mkannwischer marked this pull request as draft May 22, 2026 01:03
@willieyz
Add KAT test Windows support (C backend only) and unify across platforms
f07387a 
Unix KAT tests rely on shell pipelines (sha256sum, cut, xargs) not
available on Windows. Introduce test/src/kat_client.py — a portable
Python script that runs gen_KAT binaries, SHA-256-hashes their stdout,
and checks against META.yml, replacing the shell one-liner:
```
 set -o pipefail; $W $MLKEM512_DIR/bin/gen_KAT512 | $SHA256SUM | \
 cut -d " " -f 1 | xargs ./META.sh ML-KEM-512 kat-sha256
```
Add gen_KAT{512,768,1024}, gen_KAT, run_kat, and test targets to
Makefile.Microsoft_nmake. quickcheck now aliases test.

To keep KAT checking uniform across platforms, the Unix Makefile is
migrated to the same Python script. A single mechanism now drives
KAT verification on both Unix and Windows. META.sh and the SHA256SUM
detection block are removed as they are no longer needed.

Signed-off-by: willieyz <willie.zhao@chelpis.com>
@willieyz willieyz force-pushed the win-sup-kat branch 2 times, most recently from 195958f to f07387a Compare May 27, 2026 17:16
@willieyz
Copy link
Copy Markdown
Contributor Author

willieyz commented May 27, 2026

@willieyz, I have discussed this with @hanno-becker: We want to keep KAT checking uniform across platforms. I think the Python approach you have picked is likely the most portable. Could you also switch the Makefile to use that script? Please also clean up all unnecessary files that won't be needed anymore then.

Hello @mkannwischer, thank you for the review and suggestion!
I have addressed your feedback, both the Unix Makefile and Makefile.Microsoft_nmake now use test/src/kat_client.py to run the KAT tests, so KAT checking is uniform across platforms.
META.sh and the SHA256SUM detection block in the Makefile have been removed as they are no longer needed.
Please take another look when you have time, thank you and Hanno again for the suggesions and help!

@willieyz willieyz marked this pull request as ready for review May 27, 2026 18:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mkannwischer mkannwischer mkannwischer requested changes

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@willieyz @oqs-bot @mkannwischer