CI: Add more legacy compiler tests and move to scheduled workflow

[mkannwischer]

Our compiler tests and constant-time tests have been steadily
growing over time which is not sustainable in the medium term.

This commit solves that by splitting the set up of compiler versions
into two

1. Regular compilers - tested as before on every PR. These are compilers
   that are supported by the most recent nixpkgs release.

2. Legacy compilers - tested in a scheduled job or when
   legacy-compiler-tests label is added to the PR. Currently the
   job is scheduled to run daily, but in the long term we may want
   to switch it to weekly.

Legacy compiler shells and overlay overrides live in nix/legacy/, with
their own nixpkgs revisions pinned via fetchTarball.
The main flake.lock therefore stays free of legacy inputs.

This allows us to extend comiler coverage by gcc 6, 8, 9, 10, zig 0.10 +0.11,
and clang 6..13 for both CT and compiler tests.

My expectation is that the legacy compilers only get changed
whenever nixpkgs drops a compiler version.

• Resolves CI: Reconsider nixpkgs for compiler tests and constant-time tests #1557

[mkannwischer]

For a long time I tried many other ways to install such old compilers.
For example, #1688 tries to user Docker for gcc, and https://github.com/KyleMayes/install-llvm-action for LLVM. It seems to be working, but it becomes somewhat hacky and it cannot give us the same coverage as nix can. For example, the gcc4.8/4.9 containers don't work with current docker - and they are not maintained.

The main reason for not using nix was the fear that cache entries in the nix binary cache will eventually disappear forcing our CI to build the compilers from source. So far we have not seen that, so I think we can defer solving this problem until it actually materializes. There is some on going discussion on garbage collecting in the nix binary cache as their S3 bill is apparently quite high, so we may eventually be affected.

[oqs-bot]

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)

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

[oqs-bot]

CBMC Results (ML-KEM-768)

Full Results (191 proofs)

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

[oqs-bot]

CBMC Results (ML-KEM-512)

Full Results (191 proofs)

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