Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hanno-becker merged 1 commit into from
May 16, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 28 additions & 16 deletions mlkem/src/cbmc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */

Expand Down Expand Up @@ -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))) \
}
Expand All @@ -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)] \
}

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

Expand Down
2 changes: 1 addition & 1 deletion mlkem/src/verify.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
Loading