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

This commit ports pq-code-package/mlkem-native#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 <beckphan@amazon.co.uk>

Author: hanno-becker

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)] \
   }