[CI] Avoid mismatched comparison and fix error in forall/exists macros

[hanno-becker]

Copy of #1690 to run full CI.

[oqs-bot]

CBMC Results (ML-KEM-512)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
**TOTAL**	⚠️	1841s	1202s	+53.2%
mlk_indcpa_dec	⚠️	81s	15s	+440%
mlk_indcpa_enc	⚠️	343s	158s	+117%
mlk_indcpa_keypair_derand	⚠️	418s	232s	+80%
mlk_keccak_squeeze_once	⚠️	24s	7s	+243%
nttunpack_native_x86_64	⚠️	172s	3s	+5633%

Full Results (191 proofs)

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

[oqs-bot]

CBMC Results (ML-KEM-768)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
**TOTAL**	⚠️	2190s	1303s	+68.1%
mlk_indcpa_dec	⚠️	88s	14s	+529%
mlk_indcpa_enc	⚠️	463s	177s	+162%
mlk_indcpa_keypair_derand	⚠️	575s	202s	+185%
mlk_keccak_squeeze_once	⚠️	26s	7s	+271%
mlk_polyvec_add	⚠️	28s	9s	+211%
nttunpack_native_x86_64	⚠️	180s	4s	+4400%

Full Results (191 proofs)

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

[nmouha]

It's good to see that CI passes for ML-KEM-512 and ML-KEM-768, but I'm surprised to see a failure for ML-KEM-1024.

The failure is after 21m. I am assuming that the proof timeout is the default 30 minutes, so maybe this is an out-of-memory error?

I'm not seeing an error on my side... So it could also be that this is just an unlucky run, in which case maybe you can run the CI again?

@hanno-becker: Thanks for investigating what might have caused the CI failure!

[hanno-becker]

@nmouha NB I think this might be a good time to try to address #1603. If you have bandwidth, would you be interested in having a look (with AIs help, I suppose) how to adjust the CBMC runner scripts so one can configure, for each proof, a set of solvers+options that should be exercised? The results need to disambiguate the solver as well. So I'd imagine that in the proof summaries printed by the CI, we'd have a separate prover column. With that, one could more easily investigate the capabilities of, say, z3 vs bitwuzla vs cvc5 on the different proof workloads.

[hanno-becker]

The failure is after 21m. I am assuming that the proof timeout is the default 30 minutes, so maybe this is an out-of-memory error?

That's my best guess -- the CI logs unfortunately don't give any clue.

We have observed huge differences between CI performance and local performance (mostly AArch64 Mac for us) in the past -- it does not come as a surprise that we see different behavior here.

[nmouha]

I'm not sure I'm the right person to take on #1603. I don't have CI access, and the changes it would require are likely to be contentious: adding solvers (increasing the TCB) and running them in the CI (increasing the CI times).

My time might be better spent on other improvements, such as fixing additional soundness bugs or optimizing the slowest proofs. If there is funding for this kind of work, please let me know.

[hanno-becker]

We can only consider this if we get the CI to pass. @rod-chapman Do you have time to take a look at why the CI fails here?

[hanno-becker]

I'm not sure I'm the right person to take on #1603. I don't have CI access, and the changes it would require are likely to be contentious: adding solvers (increasing the TCB) and running them in the CI (increasing the CI times).
My time might be better spent on other improvements, such as fixing additional soundness bugs or optimizing the slowest proofs. If there is funding for this kind of work, please let me know.

I'll take care of #1603.

[nmouha]

@hanno-becker: Why not just run the CI again, perhaps on a larger EC2 instance (changing ec2_instance_type from r8g.xlarge to r8g.4xlarge in .github/workflows/cbmc.yml)?

Perhaps this was just an unlucky run. But if the problem was the solver ran out of memory, then allocating more memory should do the trick...

[hanno-becker]

@nmouha Larger instances are more expensive, so we avoid scaling up if we can. (NB The nix runtime you observed in the other CI is a one-off because the nix config changed -- after that it's cached). But still, we'll take a look and try to understand why it fails.

[oqs-bot]

CBMC Results (ML-KEM-1024)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
**TOTAL**	⚠️	2157s	1207s	+78.7%
mlk_indcpa_enc	❌	-	141s	-
mlk_indcpa_dec	⚠️	141s	10s	+1310%
mlk_indcpa_keypair_derand	⚠️	975s	118s	+726%
mlk_keccak_squeeze_once	⚠️	24s	10s	+140%
mlk_polyvec_add	⚠️	22s	11s	+100%
nttunpack_native_x86_64	⚠️	173s	3s	+5667%

Full Results (191 proofs)

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

[nmouha]

Looking at the CBMC results, only one proof appears to be failing. I ran it locally: MLKEM_K=4 time ./run-cbmc-proofs.py -p indcpa_enc completes in 16m 46s with ~15 GB peak memory on a single core of an Ultra 7 165H.

The CI run hits the failure at 23m 47s, which is well within the 30-minute timeout. So, this does not seem to be a timeout issue.

This points to an out-of-memory problem in the CI environment. Could we confirm the CI memory limit was reached? If so, we may just need to increase it for this proof, or consider alternative options to reduce the memory footprint.