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

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.

Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: hanno-becker

mlkem/src/cbmc.h

@@ -80,24 +80,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 */
 
@@ -126,8 +138,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)))                    \
   }
@@ -139,8 +151,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(* (int16_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
   }
 
@@ -150,8 +162,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)] \
   }
 

mlkem/src/verify.h

@@ -376,7 +376,7 @@ __contract__(
 static MLK_INLINE void mlk_ct_cmov_zero(uint8_t *r, const uint8_t *x,
                                         size_t len, uint8_t b)
 __contract__(
-  requires(len <= MLK_MAX_BUFFER_SIZE)
+  requires(len <= UINT32_MAX)
   requires(memory_no_alias(r, len))
   requires(memory_no_alias(x, len))
   assigns(memory_slice(r, len))