[SwayamInSync]

The Lean certifier (LeanCertifier.h, from #60) uses memory that grows with every goal it checks on its own: on main, one certification in lean_certifier.test takes 13.4 GB.

The checker first checks every goal together: all proof modules imported at once, every module of the project replayed into the environment of the toolchain modules they import. When that fails, because one module is rejected (a proof of True added without the kernel) or a proof file declares a goal's name, it checks each goal by itself: it imports that goal's proof module again, and for every module it replays it imports that module's imports again, never freeing what it imported. A proof that imports Lean (every automatic proof does, and a user's tactic lemmas may) brings in Lean's whole environment each time. On main, the imported case of lean_certifier.test (one proof through a module the kernel rejects, four goals) makes one lean --run Certify.lean process take 13.4 GB. The new lean_certifier_memory.test runs that case under Inputs/peak_memory.py, which prints whether the largest process stayed below 6144 MB; with main's binary:

Certified: fine [backend=Lean]
Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': ...)
peak memory 12240 MB, not below 6144 MB

The Linux runners have 16 GB, and lit runs four tests at a time, in name order, so lean_certifier.test runs beside other Lean tests. Since #61 each of those runs cppverify_auto's trial with the pinned Lean, and a Lean test takes about 4.5 GB on main (measured peak PSS, 4 cores).

This is not what stops the Linux release jobs (The runner has received a shutdown signal, exit 143, 18 to 28 minutes into check-clang: main after #61, #62 twice), as this description first said: this branch's own release job was stopped the same way (run 39993647759). The ULEB128 case study takes 14.9 GB by itself on main, and in a run of the Verify suite in lit's order on four workers the whole run peaked at 16.4 GB with it beside lean_semantics.cpp's certifier (1.7 GB on this branch). #64 fixes that (the case study then verifies within 0.9 GB); this change removes the certifier's own share.

Design

One import, one kernel environment, as leanchecker replays a library:

• Read, don't import, the project. The checker reads the compiled files of the generated module, every proof module, and every project module they import (an .olean outside the toolchain): each module's imports and its own constants. It imports only the toolchain modules among those imports, once.
• Replay into one environment. It replays the project's modules through the kernel (Kernel.Environment.replay, Lean's own replay) one at a time, each after the modules it imports, into that environment. A module is left out, with why, when the kernel rejects it, when it imports a module that was left out (so the reason is the first module's, as before: the kernel rejects CppVerify.Lemmas: ...), or when it declares a constant that an earlier module or the toolchain declares otherwise. A constant declared alike twice (an equation lemma Lean derives in each module that unfolds a definition, or a theorem with the same statement, which the kernel's replay itself takes twice) is the same constant.
• The generated module first. So a proof file that defines a goal of its own under the goal's name is the module left out: ...cppverify_one_99bcee_postcondition_646d2761 declares cppverify_one_99bcee_postcondition_646d2761, which CppVerify.Generated declares. Before, the joint import failed on it and the goal was checked by itself, where the proof's type named its own definition (... is not the goal CppVerify.Generated defines); the verdict is the same, and the reason now says what the file did.
• Checks read the kernel's constants. A goal passes when its proof module and the generated module were replayed, G_proof is a theorem of type exactly .const G [], G is a definition that CppVerify.Generated declared (the module is recorded with each constant at its replay), and the axioms its kernel constants reach are allowed. These are the same checks as before; only where they read changed. A bad module now fails only the goals whose proofs import it, with no second path.
• What it no longer does: import a proof module per goal, import any module's imports per module, or fall back. The two paths were one design decision (check together for speed, alone to attribute a failure); one environment with per-module rejection gives both.
• Partial and unsafe constants are skipped by Lean's replay. That is sound here: the kernel rejects a safe declaration that uses one (safe declaration must not contain partial declaration), and checked so in Lean 4.35.0 with a partial constant of a false goal's type added without the kernel.

Measured

Peak memory of each Lean test, run alone on 4 cores (taskset), 8 tests at a time: the PSS of every process of the test summed every 0.2 s (PSS counts each shared page of Lean's .olean files once).

Test	main	this branch
lean_certifier.test	12.41 GB	2.46 GB
lean_semantics.cpp	5.82 GB	2.92 GB
lean_readable.cpp	5.79 GB	5.62 GB
lean_automation.test	4.50 GB	2.56 GB
lean_fallback_partial.test	4.51 GB	2.50 GB
lean_dependencies.test	4.58 GB	2.47 GB

Every Lean test whose proofs import Lean (an automatic proof does) dropped by about 2 GB, since even the joint check imported Lean's environment twice (the proofs, then the replay's toolchain environment). The largest is now lean_readable.cpp's lake build of a project (44 processes), which the checker does not run. The largest of them, lean_readable.cpp, peaks at 5.6 GB, where lean_certifier.test alone took 12.4. The largest process of the imported case, by ru_maxrss: 13360 MB on main, 3576 MB here. The time of lean_certifier.test is 88 s on main and 39 s here.

Tests

• suite/lean_certifier_memory.test (new, Linux): the imported case under Inputs/peak_memory.py, which prints whether the largest process the command ran stayed below 6144 MB (ru_maxrss of the descendants). It fails on main (peak memory 12240 MB, not below 6144 MB) and passes here.

• suite/lean_certifier.test: every case keeps its verdict and reason, except the shadowed proof's reason, above; it fails on main at that line.

• suite/lean_certifier.test also checks the case where the proof that redeclares its goal is the first goal on the list and imports nothing of the project (Inputs/lean_certifier_first.cpp, function early): the next function, fine, is certified. Without replaying the generated module first, CppVerify.Generated is the module left out and fine fails (CppVerify.Generated declares cppverify_early_..., which CppVerify.Proofs... declares).

Mutants, each built and run on lean_certifier.test, lean_certifier_memory.test, and lean_automation.test: 6 of 6 killed on the final code. "The generated module replayed last" survived at first, since a proof that imports it puts it first anyway; the first-goal case above is the one where it matters.

Mutant	Killed by
the generated module replayed last	lean_certifier (the first-goal case)
no check of names declared twice	lean_certifier
a module whose import was left out is replayed anyway	lean_certifier, lean_certifier_memory
a goal whose proof module was left out is checked anyway	lean_certifier, lean_certifier_memory
the toolchain imported again for each module, and the replay into it	all three
the toolchain imported again for each module, the result discarded (only memory changes)	lean_certifier_memory alone

A first version also kept, for each module whose compiled files could not be read, why, so that only the goals importing it would fail; its mutant survived. Only proofs that built reach the checker, and lake builds what they import, so no input reaches it; it is gone, and an unreadable .olean stops the checker, failing every goal with the exception, as on main.

Docs

• ch17 (What certification checks): the toolchain imported once, however many proofs import Lean; names declared twice; the shadowed proof's message.
• Release notes: the certification entry says the replay is into one environment.
• DESIGN.md, ARCHITECTURE.md: the checker as above, the history (a check per goal, the fallback and its 13 GB), and the new test.

Checked

• 42 Lean tests (every Verify test that mentions Lean, outside Inputs/), docs_coverage.test, and docs_examples.test pass; check-doc-examples.py on ch17 and the release notes: 7 examples, 0 failed.
• Partial constants (above): a theorem using a partial constant of a false goal's type, added without the kernel, is rejected by the kernel of Lean 4.35.0 with safe declaration must not contain partial declaration 'cheat'.