[SwayamInSync]

Every goal of a Lean project was a stub, each True included, so a project of a few functions needed tens of proofs before it certified. For lean_readable.cpp, 35 goals, all sorry. Now:

$ cpp-verify --backend=lean --lean-project=proof lean_readable.cpp
Exported: lean obligation: next (cppverify_auto proved 3 of 3 goals)
Exported: lean obligation: twice (cppverify_auto proved 4 of 4 goals)
...
Exported: lean obligation: poly (cppverify_auto proved 1 of 3 goals)
$ cpp-verify --backend=lean --lean-project=proof --lean-certify lean_readable.cpp
Certified: next [backend=Lean]
Certified: twice [backend=Lean]
...
Unresolved: lean obligation: poly (Lean certification failed: the proof of fn_…::overflow@102:3: … declaration uses `sorry`)

33 of the 35 goals are proved at export, in 8 s; poly's two are nonlinear, which core Lean does not decide (Mathlib's nlinarith or the native bv_decide tier, both opt-in by the Lean plan's decisions).

Design

As Vermilion, Why3, and Frama-C's WP do, automation runs once, when the goals are generated, and the user sees only what it leaves.

• cppverify_auto (CppVerify/Auto.lean, written with every export from LeanAutomation.h): a ladder of steps, each with a heartbeat budget of its own (cppverify.autoBudget, 50000) and rolled back when it fails, runs out of heartbeats, leaves goals, or proves the goal with an axiom outside Lean's foundations, as Vermilion's vrml_ladder does (rungs, budgets, runtime exceptions caught, a rung counts only when it closes the goal). Steps, cheapest first: grind; the heap step (each heapStore* equation turned into the function it defines and substituted, then the machine normalization, then grind); the machine step (comparisons, constants, and overflow predicates as integer facts, then grind); decide; simp_all. Each first unfolds a goal still in its readable form, as one without binders is after apply G.of_readable.
• Chosen by measurement. A probe tried candidate steps on every goal the suite exports (9830 goals of 375 files, success only on a kernel-accepted theorem without sorryAx). Of the 5740 goals that Z3 proves: grind alone 66.9%, the machine step 77.4%, the heap step 85.6% (681 only it proves), all of them 90.2%; the order was chosen by simulating every order over the measured times (mean 319 ms per goal proved, 1.9 s per goal not). Two more parts were measured and left out: stating the range of every BitVec.toInt term proved nothing more (grind knows the ranges; 5127 against 5129 goals), and removing Int.bmod with an omega discharger proved 32 fewer goals (5129 against 5161) and made the heap step slower (535 ms against 311 ms on average). What remains is nonlinear arithmetic, specs that need induction, and quantified frames.
• The trial (automateLeanProject): every exported goal whose proof file is still the one cpp-verify wrote, and whose header names no attempt by the current LeanAutomationRevision, is tried, with the pinned toolchain if it is installed. A goal it proves gets the step that proved it as its proof (pristine, like a stub); any other gets a stub whose header records the attempt (automation: cppverify_auto 1 did not prove it). It is tried again only when the revision changes, and never once edited.
• Only kernel-accepted proofs count. The probe found grind claiming two false goals (unsafe_i128_negation, unsafe_i128_division) with terms the kernel rejected, and the ladder rejects a step whose proof uses the user's unfinished lemma (an @[grind] theorem proved by sorry), trying the next one.
• Time. Heartbeats do not bound a kernel check: one goal took 260 s under a 200000-heartbeat budget. Each goal therefore has a wall-clock limit (--lean-auto-timeout, 20 s), and the goals after one that exceeds it start again in a new process. The trial runs lean itself, with the LEAN_PATH of lake env, so a stopped process leaves no child, in --jobs chunks.
• Lean reports through a file. Lean writes its messages from a thread of its own, buffered: a slow goal hid the messages of every goal before it, and a stopped process lost them. The ladder and a #cppverify_axioms command append each step and each theorem's axioms (or that the kernel rejected it) to a report file, flushed line by line.
• Certification builds Auto too, builds the proofs --jobs at once, and checks every goal in one environment: all proof modules imported together, and every project module's constants replayed together through the kernel into the environment of the toolchain modules they import. An automatic proof imports Lean, and importing it once per goal took 161 s for 33 goals; now 8 s, and the whole certification 204 s → 12 s. A check reads only kernel constants, so proofs imported together cannot change each other's checks. When the import or replay fails (a proof file that declares a goal's name, a module the kernel rejects), each goal is checked on its own, exactly as before. An equation lemma Lean derives in each module that unfolds a definition is accepted when every copy is the same.
• ChildProcess.{h,cpp}: polling and stopping a process, moved from the cvc5 adapter, which now uses it, and the environment for a child.

--no-lean-auto writes stubs only.

Tests

• New suite/lean_automation.test: an export (an automatic proof and its header, a stub that records the attempt, a goal stopped at a 3 s limit with the goals after it still tried, the counts, JSON lean_automatic); certification of both; a rerun tries nothing; an edited proof is kept and may use cppverify_auto; a stub of no attempt (as before automation) and one of an earlier revision are tried; a step proving a goal with an unfinished @[grind] lemma does not count, and the next step proves it; --no-lean-auto; both options without a project are errors.
• Updated: lean_certify.cpp, lean_dependencies.test, and lean_readable.cpp's stub checks use --no-lean-auto, since they test proofs written over stubs; lean_certifier.test keeps automation and matches the stub's line by pattern; lean_fallback_partial.test's complete export is now Certified, its return check proved by cppverify_auto; lean_toolchain.test exports with --no-lean-auto, so that its certification run under a fake elan tries cppverify_auto first whether or not Lean is installed, and checks that the trial's build runs the pinned Lean too (macOS CI, which has no Lean, tried the goal there and Linux did not, so the log differed).

Mutants, each rebuilt and run against lean_automation.test, lean_certifier.test, and lean_fallback_partial.test: 10 of 13 killed.

• no trial at export; every pristine file tried again; a stub no revision tried never tried; no restart after a goal that stops Lean; the wall-clock limit ignored;
• automatic proofs not recognized as generated; an edited proof taken as generated;
• the ladder accepting a step that uses an unfinished lemma; readable forms not unfolded;
• the checker's fast path keeping its results after a failed replay (killed by lean_certifier.test's theorem past the kernel).

Three survive:

• the trial's own check of a theorem's axioms. The ladder's check catches every case a test can build; the trial's is for a theorem the kernel rejects after the ladder accepted the step, as the probe saw grind do with _inhabitedExprDummy terms, which the ladder now rejects first in every case it reproduced.
• the fast path's comparison of a constant two modules declare. Lean 4.35's import accepts one name declared by two modules even when the proofs differ (tested with theorem foo proved by rfl and by decide: it keeps one), so the fast path falls back when they differ; the kernel replay would catch a mismatched goal anyway.
• the fast path never taken: it changes the time only.

Docs

• tooling.rst: --no-lean-auto, --lean-auto-timeout, automation in --lean-project, parallel builds in --lean-certify and --jobs, the time limits.
• Book, ch17: "Proofs cppverify_auto finds", with the checked example and its exact output; the outputs of the chapter's Lean examples as they are now.
• Release notes: "Lean proofs cppverify_auto finds".
• ARCHITECTURE.md: "Automation" and the checker's two paths. DESIGN.md: the automation rules.

Checked

Rebased onto main at 213a367 (with #57). The one conflict, in tooling.rst's paragraph on jobs, keeps #57's sentence on the work-bounded probe and this PR's on Lean processes. On that tree, an assertions build passes the 41 Verify tests that mention Lean, #57's included. Before that, rebased onto f861d01 (with #46 and #49) without conflicts, and checked on main at 62af455:

• Verify lit suite: 439 passed on a release build, the docs tests included, with llvm_uleb128_decoder_exhaustive.cpp excluded (lit never runs it).
• VerifyTests: 62 passed, 1 skipped.
• The 41 tests that use Lean (every Verify test that mentions it, lean_automation.test and the docs examples among them), and the 22 that use cvc5, whose process loop now uses ChildProcess.
• On main: lean_automation.test fails at its first step: main rejects --lean-auto-timeout, and without it prints Exported: lean obligation: next and writes a sorry stub for every goal.
• Docs: the site builds with -W; docs_examples.test now runs ch17's two Lean examples as Lean exports, in a project of their own ({dir} in cppverify-example: flags), and checks their verdicts.
• clang-format: clean on the changed sources.