From 8e77cf225b20380fc2ad0f9c4043782e6e5b16d4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 18:49:05 +0530 Subject: [PATCH 1/5] verify: Reject the solver options with the Lean backend, which runs no solver. --- clang/tools/cpp-verify/Main.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index dd7f14fd77..56e3ebfa58 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -558,6 +558,13 @@ static bool resolveOptions(bool Replay) { BackendOpt.setValue("bmc"); } const StringRef Backend = BackendOpt.getValue(); + const cl::Option *SolverOption = nullptr; + for (const cl::Option *Option : std::initializer_list{ + &SolverTimeout, &CollectionTimeout, &CertifyTimeout, + &FunctionTimeout, &SolverResourceLimit, &MaxQueryNodes, + &IntEncoding}) + if (!SolverOption && given(*Option)) + SolverOption = Option; std::string Error; if (Backend != "z3" && Backend != "cvc5" && Backend != "portfolio" && Backend != "race" && Backend != "lean" && Backend != "bmc") @@ -581,8 +588,9 @@ static bool resolveOptions(bool Replay) { else if (ProfileQuantifiers && (Backend == "cvc5" || Backend == "lean")) Error = "--profile-quantifiers requires a backend that runs Z3: z3, " "portfolio, race, or bmc"; - else if (given(IntEncoding) && Backend == "lean") - Error = "--int-encoding requires a backend that runs an SMT solver"; + else if (SolverOption && Backend == "lean") + Error = "--" + SolverOption->ArgStr.str() + + " requires a backend that runs an SMT solver"; else if ((given(CheckUB) || given(NoCheckUB)) && Replay) Error = "--check-ub and --no-check-ub apply to source verification; an " "archive keeps the checks it was written with"; From b3b010a45e8601838e705b21e0ccb779c4fc4e4f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 18:49:05 +0530 Subject: [PATCH 2/5] test: Each solver option is an error with Lean export and accepted by the solvers. --- clang/test/Verify/suite/backend_options.cpp | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/backend_options.cpp b/clang/test/Verify/suite/backend_options.cpp index ec0ad21fdd..7ed4bccc33 100644 --- a/clang/test/Verify/suite/backend_options.cpp +++ b/clang/test/Verify/suite/backend_options.cpp @@ -15,9 +15,21 @@ // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --check-ub 2>&1 | FileCheck %s --check-prefix=REPLAY-UB // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --profile-quantifiers 2>&1 | FileCheck %s --check-prefix=REPLAY-PROFILE // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --unroll=1 2>&1 | FileCheck %s --check-prefix=REPLAY-UNROLL +// RUN: not %cpp-verify --lean-out=%t/budget.lean --timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=TIMEOUT +// RUN: not %cpp-verify --lean-project=%t/budget --function-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=FUNCTION +// RUN: not test -e %t/budget +// RUN: not %cpp-verify --backend=lean --collection-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=COLLECTION +// RUN: not %cpp-verify --lean-out=%t/budget.lean --certify-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +// RUN: not %cpp-verify --lean-out=%t/budget.lean --solver-rlimit=100000 %s -- 2>&1 | FileCheck %s --check-prefix=RLIMIT +// RUN: not %cpp-verify --lean-out=%t/budget.lean --max-query-nodes=100000 %s -- 2>&1 | FileCheck %s --check-prefix=NODES +// RUN: not test -e %t/budget.lean +// RUN: not %cpp-verify --obligation-in=%t/goals.cpv --lean-out=%t/budget.lean --timeout=1000 2>&1 | FileCheck %s --check-prefix=TIMEOUT +// RUN: %cpp-verify --timeout=20000 --function-timeout=200000 --solver-rlimit=50000000 --max-query-nodes=1000000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER +// RUN: %cpp-verify --lean-fallback=%t/fallback --timeout=20000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER // // An option one backend alone uses selects it when no backend is named, and -// an option the run would ignore is an error. +// an option the run would ignore is an error: Lean export runs no solver, so +// no solver option applies to it. int count(int n) cppverify::pre(0 <= n && n <= 2) @@ -45,3 +57,10 @@ int count(int n) // REPLAY-UB: error: --check-ub and --no-check-ub apply to source verification // REPLAY-PROFILE: error: --profile-quantifiers applies to source verification // REPLAY-UNROLL: error: --unroll requires a BMC-transformed archive +// TIMEOUT: error: --timeout requires a backend that runs an SMT solver +// FUNCTION: error: --function-timeout requires a backend that runs an SMT solver +// COLLECTION: error: --collection-timeout requires a backend that runs an SMT solver +// CERTIFY: error: --certify-timeout requires a backend that runs an SMT solver +// RLIMIT: error: --solver-rlimit requires a backend that runs an SMT solver +// NODES: error: --max-query-nodes requires a backend that runs an SMT solver +// SOLVER: Verified: count [backend=z3] From 4720cd6213eae738771e485a7133c56feaa3b1fb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 18:49:35 +0530 Subject: [PATCH 3/5] test: Export a false function to Lean without a solver timeout, which Lean rejects. --- clang/test/Verify/suite/lean_backend_failure.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/lean_backend_failure.cpp b/clang/test/Verify/suite/lean_backend_failure.cpp index 0bf555b9d5..ac4452db7e 100644 --- a/clang/test/Verify/suite/lean_backend_failure.cpp +++ b/clang/test/Verify/suite/lean_backend_failure.cpp @@ -1,5 +1,5 @@ // RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s -// RUN: %cpp-verify --backend=lean --timeout=1 --lean-out=%t.lean %s -- 2>&1 | FileCheck %s +// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s -- 2>&1 | FileCheck %s // RUN: grep -q 'unchecked Lean scratch-pad' %t.lean // RUN: grep -Eq 'theorem cppverify_invalid_lean_export_fn_[0-9a-f]+_correct' %t.lean // RUN: grep -Eq 'theorem cppverify_invalid_lean_export_fn_[0-9a-f]+_obligation_[0-9]+' %t.lean From 599d95d8ecbfe33100c7c7ebcae13eac0dda7f26 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 23:08:57 +0530 Subject: [PATCH 4/5] docs: The solver options are errors with Lean, and Lean certification has its own step limit. --- website/source/language/tooling.rst | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index e01e583bb8..c0ad318cfc 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -162,13 +162,20 @@ nothing is verified: - ``error: --cvc5-path requires --backend=cvc5, --backend=portfolio, or --backend=race`` * - ``--backend=cvc5 --profile-quantifiers`` - ``error: --profile-quantifiers requires a backend that runs Z3: z3, portfolio, race, or bmc`` - * - ``--lean-out=FILE --int-encoding=bitvector`` - - ``error: --int-encoding requires a backend that runs an SMT solver`` + * - ``--lean-out=FILE --timeout=60000`` + - ``error: --timeout requires a backend that runs an SMT solver`` * - ``--proof-cache-max-mb=N`` without ``--proof-cache`` - ``error: --proof-cache-max-mb and --proof-cache-max-entries require --proof-cache`` * - ``--lean-fallback-scope=all`` without ``--lean-fallback`` - ``error: --lean-fallback-scope requires --lean-fallback`` +Lean export runs no solver, so every solver option is an error with +``--backend=lean``, ``--lean-out``, or ``--lean-project``, the same way as +``--timeout`` above: ``--timeout``, ``--collection-timeout``, +``--certify-timeout``, ``--function-timeout``, ``--solver-rlimit``, +``--max-query-nodes``, and ``--int-encoding``. ``--lean-fallback`` runs Z3 +first, and accepts all of them. + The same rules hold when replaying an archive: ``--check-ub`` and ``--profile-quantifiers`` are errors there, since an archive keeps the checks it was written with, and ``--unroll`` must match the bound a BMC archive @@ -273,6 +280,7 @@ Backends * - ``--timeout=N`` - Per-query solver timeout in milliseconds (default 30000; ``0`` disables). A query that exceeds it is reported as unresolved instead of hanging. + Not accepted with ``--backend=lean``, which runs no solver. * - ``--certify-timeout=N`` - The milliseconds checking one counterexample against the true definitions may take (default half of the query timeout; ``0`` lets @@ -280,19 +288,23 @@ Backends query's time to other models and later stages; when it is reached the reason says so (``the time one counterexample check may take (N ms, --certify-timeout) was spent``). + Not accepted with ``--backend=lean``, which runs no solver. * - ``--collection-timeout=N`` - Per-query timeout for a function whose queries involve sequences, sets, multisets, or maps, whose theories need more search (default twice ``--timeout``; ``0`` disables). + Not accepted with ``--backend=lean``, which runs no solver. * - ``--solver-rlimit=N`` - Deterministic per-query Z3/cvc5 resource budget (default ``0``, disabled). Exhaustion is ``Unresolved``. Z3 reports ``solver.resource-limit``; cvc5 may report the conservative ``solver.unknown``. + Not accepted with ``--backend=lean``, which runs no solver. * - ``--max-query-nodes=N`` - Reject a solver-backed canonical obligation module larger than ``N`` expression nodes before verification, lower-only encoding, or a requested Z3 dump (default ``0``, disabled). Exhaustion is fail-closed with reason ``query.size-limit``. + Not accepted with ``--backend=lean``, which runs no solver. * - ``--int-encoding=MODE`` - Solver representation of machine integers for Z3, cvc5, portfolio, and BMC: ``auto`` (default; integers reduced modulo ``2^N`` unless a query @@ -308,6 +320,7 @@ Backends * - ``--function-timeout=N`` - Milliseconds all queries of one function may take together (default ten times ``--timeout``; ``0`` disables). See `Time limits`_. + Not accepted with ``--backend=lean``, which runs no solver. * - ``--proof-cache=DIR`` - Persist successful dependency-scoped Z3 or BMC proofs. In portfolio mode this caches only the Z3 component and cvc5 still runs on every query. @@ -409,6 +422,13 @@ The limits are wall-clock times and depend on the machine. For results that must repeat exactly across machines, use ``--solver-rlimit``, a deterministic per-query budget of solver steps. +None of these limits applies to Lean, which runs no solver. Lean +certification (``--lean-certify``) gives each ``lake`` step 300 seconds: +building the generated module, compiling your module, compiling each proof, +and the final check. A step that takes longer leaves every result +``Unresolved`` with reason ``lean.export-failed``, and its message gives the +command's error. + Parallel solving and proof caching ---------------------------------- From 08c6928e1f5e1d2185262a185447d855c5d6dba2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 23:08:58 +0530 Subject: [PATCH 5/5] docs: Solver options with Lean export are errors, in the release notes. --- website/source/release-notes.rst | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b8abf5d90b..ab550229bb 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -124,8 +124,10 @@ function as ``Interrupted``, and exits with status 130 **Options select their backend, and unused options are errors.** ``--lean-out`` and ``--lean-project`` select Lean and ``--unroll`` selects BMC; -an option the run would not use, such as ``--unroll`` with ``--backend=z3``, is -an error that names what it needs, where it was ignored (:doc:`language/tooling`). +an option the run would not use, such as ``--unroll`` with ``--backend=z3``, or +``--timeout`` and the other solver budgets with Lean export, which runs no +solver, is an error that names what it needs, where it was ignored +(:doc:`language/tooling`). **Compiler errors stop their file, and headers are C++.** An error in a command line was printed and then ignored, and a ``.h`` input was compiled as C. Now