Add Zephyr-based test platform for QEMU MPS boards by mkannwischer · Pull Request #1750 · pq-code-package/mlkem-native

mkannwischer · 2026-06-16T06:46:48Z

No description provided.

oqs-bot · 2026-06-21T04:46:19Z

CBMC Results (ML-KEM-768)

Full Results (191 proofs)

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

oqs-bot · 2026-06-21T04:46:21Z

CBMC Results (ML-KEM-512)

Full Results (191 proofs)

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

oqs-bot · 2026-06-21T04:46:36Z

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)

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

hanno-becker · 2026-06-23T04:06:19Z

+	$$(Q)cp $(ZEPHYR_BUILD_DIR)/$(2)/zephyr/zephyr.elf $$@
+endef
+
+$(eval $(call ZEPHYR_BIN,512,test_mlkem512,test/src/test_mlkem.c))


Why do we need those per-target recipes here? This wasn't needed in previous baremetal platforms, and doesn't scale well as new make targets are added.

hanno-becker

I very much like the consolidation of targets and am generally in favor of introducing Zephyr.

However, I'm not yet happy with how all make targets have to be manually adjusted in the new platform.mk. Can we do better and keep building the test sources in the same way as for other baremetal platforms, but merely add some configurable 'finalize-build' step which bundles the compiled .o files and the Zephyr sources into a Zephyr binary? So rather than having only an EXTRA_SOURCES for a baremetal platform, we generalize this to a more elaborate custom build finalization step -- while still keeping the way the test sources themselves are compiled? Just thinking out loud.

Build the mlkem-native tests as Zephyr applications so they run on QEMU-emulated Arm MPS boards spanning Cortex-M3/M4/M7/M33/M55. This greatly simplifies supporting more hardware without the need for dedicated hardware abstraction layers. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

The Zephyr platform now covers the QEMU MPS boards, so the baremetal m55-an547 and m33-an524 platforms and the pqmx package they used are no longer needed. Also drops the cross-arm-embedded dev shell and the two baremetal.yml jobs. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>

Ordinarily, `main` is exempt from -Wmissing-prototypes. However, if it's re-#define'd, it isn't. To allow -Wmissing-prototypes in baremetal platforms wrapping `main`, this commit adds an explicit prototype for `main` in all test applications. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

The generic test build links each binary from prebuilt objects and the per-scheme library. A platform that builds its binaries differently (e.g. the Zephyr platform, which hands the sources to its own CMake build) had no way to hook into this without per-binary recipes. This commit introduces a CUSTOM_BUILD hook in test/mk/rules.mk: when set, it replaces the default link step, and test/mk/components.mk attaches each binary's sources -- via the new per-binary TEST_SRCS variable -- as its prerequisites rather than prebuilt objects and libraries. TEST_SRCS is the single source of truth for a binary's test sources, so a custom platform needs no per-binary wiring. As part of this, the ADD_SOURCE_UNIT / ADD_SOURCE_ALLOC special cases are folded into ADD_SOURCE (parameterized by a library suffix), and the per-test defines (MLK_STATIC_TESTABLE=, MLK_CONFIG_FILE=...) move from the test object to the test binary. Target-specific CFLAGS propagate to a target's prerequisites, so the object still gets them; attaching to the binary lets a custom build read them off CFLAGS too. No change to the default build: with CUSTOM_BUILD unset, the link step and prerequisites are as before. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

The Zephyr platform previously hand-enumerated every test binary with a per-binary ZEPHYR_BIN recipe. This commit rewrites it on top of the generic CUSTOM_BUILD hook: a single CUSTOM_BUILD recipe drives the CMake build for whichever binary is being made, taking its test sources from the per-binary TEST_SRCS. Adding a test binary now needs no change here. The test binary's full CFLAGS are forwarded to the CMake build and applied to the mlkem amalgamation and the test sources alike, so the firmware is built with the project's own warning/optimization/standard policy and feature defines (including the parameter set) rather than a divergent Zephyr default. Two flags are rewritten for the CMake build dir: -Imlkem is made absolute, and the embedded quotes of -DMLK_CONFIG_FILE="..." are escaped so they survive the recipe shell and CMake's separate_arguments. The QEMU test-tuning defines (smaller iteration counts) are amended onto CFLAGS and forwarded the same way, replacing the separate ZEPHYR_TEST_DEFS / ZEPHYR_LEVEL parameters. The app CMakeLists consumes a ZEPHYR_TEST_SRCS list (entrypoint plus support sources) instead of a single ZEPHYR_TEST_SRC. Also adds a README documenting the platform. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

The Zephyr platform forwards the test binary's full CFLAGS -- including the project's strict, -Werror'd warning set -- to the CMake build. Our own sources are clean under it, but the benchmark cycle HAL (test/hal/hal.c) is the one test source that includes Zephyr SDK headers (<zephyr/kernel.h>), and those are not -Werror-clean (-Wconversion, -Wsign-conversion, -pedantic). This broke the benchmark build on all boards. Drop -Werror for hal.c only, via a per-source COMPILE_OPTIONS property, so the SDK-header warnings no longer fail the build while our own sources stay strict. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

mkannwischer force-pushed the platform-zephyr branch 8 times, most recently from ec37866 to fdf2d86 Compare June 21, 2026 03:52

mkannwischer added the needs-mldsa-native-port label Jun 21, 2026

mkannwischer marked this pull request as ready for review June 21, 2026 04:01

mkannwischer requested a review from a team as a code owner June 21, 2026 04:01

hanno-becker reviewed Jun 23, 2026

View reviewed changes

hanno-becker requested changes Jun 23, 2026

View reviewed changes

hanno-becker force-pushed the platform-zephyr branch 3 times, most recently from ebf9764 to f5160ba Compare June 26, 2026 15:07

mkannwischer and others added 7 commits June 27, 2026 04:36

Armv81M: Remove redundant backend declarations

7c54244

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

hanno-becker force-pushed the platform-zephyr branch from f5160ba to c147080 Compare June 27, 2026 03:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add Zephyr-based test platform for QEMU MPS boards#1750

Add Zephyr-based test platform for QEMU MPS boards#1750
mkannwischer wants to merge 7 commits into
mainfrom
platform-zephyr

mkannwischer commented Jun 16, 2026

Uh oh!

oqs-bot commented Jun 21, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 21, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Jun 21, 2026 •

edited

Loading

Uh oh!

hanno-becker Jun 23, 2026

Uh oh!

hanno-becker left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

mkannwischer commented Jun 16, 2026

Uh oh!

oqs-bot commented Jun 21, 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 Jun 21, 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 Jun 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

hanno-becker Jun 23, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oqs-bot commented Jun 21, 2026 •

edited

Loading

oqs-bot commented Jun 21, 2026 •

edited

Loading

oqs-bot commented Jun 21, 2026 •

edited

Loading