CBMC: Document and enforce 4 GiB limit of forall/exists quantifiers

[hanno-becker]

This is one possible way to approach #1690. We may also consider merging it as a temporary improvement while continuing to deliberate other approaches such as @nmouha's suggestion of switching to size_t bounds and using CVC5.

---

• Resolves Avoid mismatched comparison and fix error in forall/exists macros #1690

---

Acknowledgements: Thanks to @nmouha for identifying this issue.

The forall/exists macros in cbmc.h declared the quantified variable as
unsigned, which on 64-bit platforms is 32 bits wide. When applied to
a size_t bound, this silently truncated the upper bound: the quantifier
only ranged over indices up to UINT32_MAX rather than the full size_t
range, leaving the predicate unchecked for any larger indices.

This was demonstrated by @nmouha in #1690
with a contrived bug in mlk_ct_cmov_zero that corrupts the buffer at
i == 2^32 yet still passes CBMC under the old macros. mlkem-native
itself never operates on buffers that large, so no real bug is masked,
but the quantifier definition is still highly misleading and could mask
real bugs in the future.

For now, make the limitation explicit rather than widening the quantifier:

• Explicitly cast the lower and upper bounds to uint32_t, so
  passing a wider bound triggers CBMC's conversion check rather than
  silently truncating.
• Tighten mlk_ct_cmov_zero's precondition from MLK_MAX_BUFFER_SIZE to
  UINT32_MAX (the only size_t-bounded buffer in mlkem-native that
  participates in a quantified contract).
• Declare the quantified variable as uint32_t (was unsigned)
  as a robustness improvement towards the implementation-defined
  size of unsigned.

We may still want to consider widening the quantifier variable
as a follow-up, but this is a more intrusive change that prior
experiments have proved to significantly impact proof performance.

[oqs-bot]

CBMC Results (ML-KEM-768)

Full Results (191 proofs)

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

[oqs-bot]

CBMC Results (ML-KEM-512)

Full Results (191 proofs)

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

[oqs-bot]

CBMC Results (ML-KEM-1024)

Full Results (191 proofs)

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

[nmouha]

We now have data comparing the two approaches. #1694 (4 GiB limit) runs CBMC proofs in ~13 minutes. #1695 (widening the quantifier without limits) runs them in ~17 minutes. To put this in perspective, the Nix setup test alone in #1695 takes ~28 minutes.

The CBMC proof time increase is modest, and if CI time is a concern, there are more impactful targets, such as reducing the Nix setup test duration.

[mkannwischer]

We now have data comparing the two approaches. #1694 (4 GiB limit) runs CBMC proofs in ~13 minutes. #1695 (widening the quantifier without limits) runs them in ~17 minutes. To put this in perspective, the Nix setup test alone in #1695 takes ~28 minutes.

Thanks for the update! I think we are all in agreement that supporting size_t properly is what we want in the long term. While we get that working, I agree with @hanno-becker that it's a good idea to document the current behavior faithfully and merge #1694 first.

The CBMC proof time increase is modest, and if CI time is a concern, there are more impactful targets, such as reducing the Nix setup test duration.

The Nix setup test only runs in PRs that change the nix files.
Also, the nix setup is cached. Once the change to any nix file gets merged into main, the cache is rebuilt and all PRs use that cache.