SAT back end: asserted forall handed over from an ensures is very expensive #9387

In mldsa-native I am adding CaDiCaL as a second solver for some CBMC proofs. With CBMC 6.11.0, several top-level proofs fail with it on the 32 GB CI machines; for example, the ML-DSA-87 attempt_signature_generation proof needs 50 GB and almost an hour with CaDiCaL. The cause is a common contract pattern: one function's ensures bounds every element of an array, and the next function's requires asks for the same bound.

In CBMC, symex_assert skolemizes every asserted forall (rewrite_quantifiers), while the SAT back end expands assumed foralls over their constant range (eager_quantifier_instantiation). The requires check thus becomes one read at a symbolic index that the solver has to relate to every expanded instance of the ensures.

Reproducer

#include <stdint.h>
typedef int32_t mat[4][4][256];

#define BOUND(m, i, j, k)                                       \
  __CPROVER_forall { uint32_t i; i < 4 ==>                      \
  __CPROVER_forall { uint32_t j; j < 4 ==>                      \
  __CPROVER_forall { uint32_t k; k < 256 ==>                    \
    (0 <= (*m)[i][j][k] && (*m)[i][j][k] < 8380417) } } }

void produce(mat *m)
__CPROVER_requires(__CPROVER_is_fresh(m, sizeof(mat)))
__CPROVER_assigns(__CPROVER_object_whole(m))
__CPROVER_ensures(BOUND(m, i, j, k));

void consume(mat *m)
__CPROVER_requires(__CPROVER_is_fresh(m, sizeof(mat)))
__CPROVER_requires(BOUND(m, x, y, z));

void target(mat *m)
__CPROVER_requires(__CPROVER_is_fresh(m, sizeof(mat)))
__CPROVER_assigns(__CPROVER_object_whole(m))
{
  produce(m);
  consume(m);
}

void harness(void) { mat *m; target(m); }

goto-cc --function harness repro.c -o a.goto
goto-instrument --add-library a.goto b.goto
goto-instrument --dfcc harness --enforce-contract target \
  --replace-call-with-contract produce --replace-call-with-contract consume b.goto c.goto
cbmc c.goto --function harness --object-bits 12 --slice-formula \
  --sat-solver cadical [--no-forall-skolemization]

Patch

no-forall-skolemization.patch

The attached patch (against CBMC 6.11.0, also used in pq-code-package/mldsa-native#1521) adds --no-forall-skolemization: asserted quantifiers are passed to the back end unchanged and expanded like assumed ones. It also treats an empty instantiation range as true (forall) / false (exists) instead of leaving the quantifier unconstrained. With it, I can verify all top-level functions of mldsa-native with CaDiCaL.

I would prefer CBMC to decide this internally rather than through a flag, but I don't quite know how to get that to work.