From b29818d4ef23255d9796493c731e5a85b08b7c84 Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Sat, 16 May 2026 04:06:46 +0100 Subject: [PATCH] CBMC: Document and enforce 4 GiB limit of forall/exists quantifiers This commit ports https://github.com/pq-code-package/mlkem-native/pull/1694. 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. mldsa-native does accept arbitrarily large buffers at the top-level API: the message, context, and pre-string passed into mld_sign / mld_sign_verify / mld_H / mld_shake256_absorb are bounded only by MLD_MAX_BUFFER_SIZE = SIZE_MAX >> 12 (~2^52 on 64-bit), and keccak_absorb walks them in a size_t loop. However, those buffers never feed into a quantified predicate -- they appear only as arguments to memory_no_alias / memory_slice and as scalar loop invariants. Hence, the restricted scope of `forall` has no impact on the CBMC safety guarantees for mldsa-native's top-level API. The only size_t-bounded quantifier in the entire tree is mld_ct_memcmp in ct.h, and it already requires len <= UINT16_MAX. 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. - Declare the quantified variable as `uint32_t` (was `unsigned`) as a robustness improvement towards the implementation-defined size of `unsigned`. Note: the upstream PR also tightened mlk_ct_cmov_zero's precondition to UINT32_MAX. mldsa-native has no equivalent function, so no analogous change is needed. 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. Signed-off-by: Hanno Becker --- mldsa/src/cbmc.h | 44 ++++++++++++++++++++++++++++---------------- 1 file changed, 28 insertions(+), 16 deletions(-) diff --git a/mldsa/src/cbmc.h b/mldsa/src/cbmc.h index d1be71971..0a7483a85 100644 --- a/mldsa/src/cbmc.h +++ b/mldsa/src/cbmc.h @@ -93,24 +93,36 @@ * Quantifiers * Note that the range on qvar is _exclusive_ between qvar_lb .. qvar_ub * https://diffblue.github.io/cbmc/contracts-quantifiers.html + * + * The quantified variable is declared as uint32_t, so these macros + * quantify only over indices in [0, UINT32_MAX). Bounds larger than + * UINT32_MAX (4 GiB) are NOT supported: the explicit (uint32_t) casts + * on the bounds will trigger CBMC's conversion check if a wider bound + * (e.g. a size_t > UINT32_MAX) is passed. + * + * Quantifying over size_t (64-bit) was found to blow up SMT proof + * times, so we deliberately keep the index width at 32 bits. Callers + * dealing with size_t-typed buffers must add an explicit + * requires(len <= UINT32_MAX) + * precondition. */ /* * Prevent clang-format from corrupting CBMC's special ==> operator */ /* clang-format off */ -#define forall(qvar, qvar_lb, qvar_ub, predicate) \ - __CPROVER_forall \ - { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \ +#define forall(qvar, qvar_lb, qvar_ub, predicate) \ + __CPROVER_forall \ + { \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> (predicate) \ } -#define exists(qvar, qvar_lb, qvar_ub, predicate) \ - __CPROVER_exists \ - { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate) \ +#define exists(qvar, qvar_lb, qvar_ub, predicate) \ + __CPROVER_exists \ + { \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) && (predicate) \ } /* clang-format on */ @@ -128,8 +140,8 @@ value_lb, value_ub) \ __CPROVER_forall \ { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \ (((int)(value_lb) <= ((array_var)[(qvar)])) && \ (((array_var)[(qvar)]) < (int)(value_ub))) \ } @@ -141,8 +153,8 @@ #define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var) \ __CPROVER_forall \ { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \ ((array_var)[(qvar)]) == (old(* (int32_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ } @@ -152,8 +164,8 @@ #define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var) \ __CPROVER_forall \ { \ - unsigned qvar; \ - ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \ + uint32_t qvar; \ + ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \ ((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \ }