Add ABI checker for AArch64 and x86_64 by hanno-becker · Pull Request #1135 · pq-code-package/mlkem-native

hanno-becker · 2025-07-30T15:17:38Z

Based on FIPS202/AArch64: Unify naming of hybrid assembly routines #1134
Resolves Add ABI checker for AArch64 assembly files #884
Resolves Add ABI checker for x86_64 assembly files #1143

This PR adds ABI checkers for all AArch64 and x86_64 assembly in mlkem-native.

The purpose of an ABI checker is to ensure that assembly files obey the required calling conventions. For AArch64, the AAPCS requires that x19-x30 and d8-d15 are preserved. For x86_64, the System V ABI requires
that rbx, rbp, and r12-r15 are preserved.

It is important to test this since failure to obey the calling convention can lead to rare but fatal bugs depending on the exact compiler and compilation settings.

On a high level, the ABI checker works as follows:

An architecture-specific assembly call stub

  void asm_call_stub(struct register_state *input,
                     struct register_state *output,
                     void (*function_ptr)(void))

is implemented which calls the function specified by function_ptr on the input register state input, and returns the output register state in output. Importantly, it does not assume that function_ptr obeys the
calling convention, so must be implemented in assembly.

Randomized ABI checker

Based on the call stub, we implement an ABI checker which calls the target function with known register inputs and checks that the output register state has retained the callee-saved registers.

Pointer inputs

Most functions read/write memory specified via parameters. Calling those functions with random input would lead to segmentation faults. The ABI checker therefore does not randomize those arguments, but instead sets
up valid aligned buffers of the right size for them.

The ABI checker gets the information about which inputs are pointers from the YAML specification embedded in each assembly file.

Some implementation details:

autogen is extended to generate one test/abicheck/check_FUNCNAME_ARCH.c file per function under test. All tests are declared and enumerated in the autogenerated test/abicheck/checks_all.h.
The handwritten test/abicheck/abicheck.c invokes all per-function ABI checks.
We integrate the abicheck build by extending test/mk/components.mk with specific build rules. This allows us to partly piggy back on existing Makefile infrastructure, such as setting execution wrappers or cross
prefixes. On the other hand, a lot of custom hackery is currently needed to get past the preprocessor directives guarding individual assembly files. This should be improved in the future.
scripts/tests is extended to allow for tests abicheck, and tests all supports --abicheck and --no-abicheck. By default, the abicheck is run with tests all.
YAML metadata is added to all x86_64 dev assembly files (dev/x86_64/src/, dev/fips202/x86_64/src/) and propagated to mlkem/ via simpasm.

oqs-bot · 2026-03-19T13:34:12Z

CBMC Results (ML-KEM-512)

Full Results (187 proofs)

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

oqs-bot · 2026-03-19T13:36:29Z

CBMC Results (ML-KEM-768)

Full Results (187 proofs)

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

oqs-bot · 2026-03-19T13:36:32Z

CBMC Results (ML-KEM-1024)

Full Results (187 proofs)

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

This commit adds an ABI checker for all AArch64 assembly in mlkem-native. The purpose of an ABI checker is to ensure that assembly files obey the required calling conventions. For AArch64 specifically, it is required by the AAPCS that x19-x30 and d8-d15 are unmodified. It is important to test this since failure to obey the AAPCS can lead to rare but fatal bugs depending on the exact compiler and compilation settings. On a high level, the ABI checker works as follows: 1. An assembly callstub void asm_call_stub(struct register_state *input, struct register_state *output, void (*function_ptr)(void)) is implemented which calls the function specified by function_ptr on the input register state input, and returns the output register state in output. Importantly, it does _not_ assume that function_ptr obeys the AAPCS, so must be implemented in assembly. This is done for AArch64 only so far. 2. Randomized ABI checker Based on asm_call_stub, we implement an ABI checker which calls the target function with random register inputs and checks that the output register state has retained the callee saved registers. 3. Pointer inputs Most functions read/write memory specified via parameters. Calling those functions with random input would lead to segmentation faults. The ABI checker therefore does not randomize those arguments, but instead sets up valid pointers of the right size for them. For now, we always align the input pointers via MLK_ALIGN. A future extension should take alignment constraints into account and vary the alignment of the inputs within those constraints. The ABI checker gets the information about which inputs are pointers from the YAML specification of AArch64 assembly. Some implementation details: - autogen is extended to generate one test/abicheck/check_FUNCNAME.c file per function under test. All tests are declared and enumerated in the autogenerated test/abicheck/checks_all.h. - The handwritten test/abicheck/abicheck.c invokes all per-function ABI checks. - We integrate the abicheck build by extending test/mk/components.mk with specific build rules. This allows us to partly piggy back on existing Makefile infrastructure, such as setting execution wrappers or cross prefixes. On the other hand, a lot of custom hackery is currently needed to get past the preprocessor directives guarding individual assembly files. This should be improved in the future. - scripts/tests is extended to allow for tests abicheck, and tests all supports --abicheck and --no-abicheck. By default, the abicheck _is_ run with tests all. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Extend the ABI checker to cover all x86_64 assembly in mlkem-native. The x86_64 System V ABI requires preservation of rbx, rbp, and r12-r15. Unlike AArch64, no SIMD registers are callee-saved. Changes: - Add YAML metadata to all 21 dev x86_64 assembly files (20 arith + 1 keccak), propagated to mlkem/ via simpasm - Add x86_64_callstub.S implementing the register state capture/restore for x86_64 System V - Extend abicheckutil.c/h with x86_64_register_state struct and compliance check - Generalize autogen gen_abicheck() to handle both architectures via an arch_configs table; output filenames are now suffixed with the architecture (e.g. check_ntt_asm_aarch64.c) - Extend components.mk with x86_64 build rules including constant data files (consts.c, compress_consts.c, etc.) Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

hanno-becker force-pushed the abicheck branch 15 times, most recently from 6c254be to 154a194 Compare August 3, 2025 04:21

hanno-becker changed the title ~~[WIP] Add ABI checker~~ AArch64: Add ABI checker Aug 3, 2025

hanno-becker force-pushed the abicheck branch 2 times, most recently from 3584074 to e97840a Compare August 3, 2025 04:33

hanno-becker marked this pull request as ready for review August 3, 2025 04:33

hanno-becker requested a review from a team as a code owner August 3, 2025 04:33

hanno-becker force-pushed the abicheck branch 3 times, most recently from cd2fa2f to 9d8783f Compare August 3, 2025 13:41

hanno-becker marked this pull request as draft August 3, 2025 19:23

hanno-becker force-pushed the abicheck branch 6 times, most recently from 7da9352 to e400cf5 Compare August 11, 2025 03:35

hanno-becker force-pushed the abicheck branch from e400cf5 to 84495ff Compare August 11, 2025 03:55

hanno-becker force-pushed the abicheck branch 3 times, most recently from 46a840e to d56d9c3 Compare September 8, 2025 03:15

hanno-becker mentioned this pull request Sep 9, 2025

Remove backend header import from common.h #1182

Open

3 tasks

hanno-becker added enhancement New feature or request aarch64 labels Oct 10, 2025

hanno-becker force-pushed the abicheck branch 2 times, most recently from 2f89458 to aca3c3d Compare March 19, 2026 13:11

hanno-becker force-pushed the abicheck branch from aca3c3d to 183f494 Compare March 19, 2026 14:51

hanno-becker changed the title ~~AArch64: Add ABI checker~~ Add ABI checker for AArch64 and x86_64 Mar 19, 2026

hanno-becker force-pushed the abicheck branch 4 times, most recently from deb58f5 to b227394 Compare March 20, 2026 05:54

hanno-becker force-pushed the abicheck branch from b227394 to 39ac88f Compare March 20, 2026 08:38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add ABI checker for AArch64 and x86_64#1135

Add ABI checker for AArch64 and x86_64#1135
hanno-becker wants to merge 2 commits intomainfrom
abicheck

hanno-becker commented Jul 30, 2025 •

edited

Loading

Uh oh!

oqs-bot commented Mar 19, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Mar 19, 2026 •

edited

Loading

Uh oh!

oqs-bot commented Mar 19, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

hanno-becker commented Jul 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

CBMC Results (ML-KEM-1024)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

hanno-becker commented Jul 30, 2025 •

edited

Loading

oqs-bot commented Mar 19, 2026 •

edited

Loading

oqs-bot commented Mar 19, 2026 •

edited

Loading

oqs-bot commented Mar 19, 2026 •

edited

Loading