[SwayamInSync]

Stacked on #63, whose 10 commits show here until it merges; merge after it. On #63's certifier (one kernel environment, the toolchain imported once), every function's goal module is replayed first, before the proof modules (roots := generated ++ proofs in LeanCertifier.h), so a proof file that declares a goal's name is the module left out, whichever goal module declares it.

A Lean project keeps every goal of every function in CppVerify/Generated.lean, and every proof imports it through User.lean. On main:

	main
a change to one function	every proof builds again, since each imports every goal
certification	deletes every proof's .olean and compiles every proof again, on every run, changed or not
lake build of the project	fails: the CppVerify library has no root module
the export of an unchanged source	rewrites Check.lean with the same text

Design

From Vermilion (read as data): per-function emission is its default, with datatype and spec definitions in one Specs.lean that every unit imports; its writes are change-detecting. Now:

• Layout. CppVerify/Prelude.lean (the fixed prelude), CppVerify/Specs.lean (each spec the run's goals apply, declared once as opaque cppSpec_<identity>), CppVerify/Goals/<function>.lean (a function's goals, readable forms, bridges, and the spec bodies they unfold, under the function's prefix), CppVerify/Generated.lean (imports every goal module), and CppVerify.lean, the library's root, which imports Check. Two goal modules that declared one spec would clash when imported together, and Lean 4.35's import keeps one of two differing declarations without a word, so specs are declared once.
• Imports. A new proof imports its function's goal module, User, and Auto. A new User.lean imports Specs; one of 0.1, which imports Generated, keeps working, with every proof then depending on every goal. Auto imports Prelude.
• Writes are change-detecting, Check.lean included: an export of an unchanged source writes nothing.
• Certification builds Generated, User, and Auto with Lake, then compiles each proof with lean -EhasSorry as before, unless its key is unchanged: SHA-256 of the toolchain, the proof's text, and the .olean bytes of every project module in its import closure (read from the import lines), kept in .cppverify/built/<goal>. Lake cannot do this part: when a dependency fails it names only the dependency (tested: E imports a failing B; lake build E A lists only B), and E's .olean of an earlier build stays, so a proof the user broke would certify from its old .olean.
• User and sorry: User is no longer compiled apart with sorry an error; the checker rejects every goal when a declaration of CppVerify.User depends on sorryAx, as the separate compile did.
• The checker learns each goal's module: G must be a definition of its goal module (the goal list names it), instead of CppVerify.Generated.
• Fallback runs: a run writes the goal modules of the functions it exports and removes every other. Keeping the module of a function the solver settled was the first design, and the new test showed it wrong: the run rewrites Specs with the specs of the modules it exports, and a kept module then failed (Unknown identifier cppSpec_fn_5f5a3374726969). The proofs of such a function stay, as on main, and build again once it is exported; Lake traces sources by content, so a module removed and written again identical builds nothing.

Tests

suite/lean_modules.test, on five functions (two that cppverify_auto proves, two that apply the recursive spec tri, with proofs in Inputs/):

• the layout: Generated imports the goal modules in source order, Specs declares tri once, each goal module imports only Specs and defines tri's body under its own prefix, a proof imports its goal module, User, and Auto, a new User imports Specs, the root imports Check;
• the two goal modules that apply tri are certified together;
• a rerun of the same source writes no file;
• a change to dbl's postcondition compiles again exactly Generated, dbl's goal module, and dbl's three proofs (find -newer);
• lake build builds every proof;
• a deleted function takes its goal module with it;
• a 0.1 User.lean (import CppVerify.Generated) still certifies;
• a fallback run whose solver verifies every function keeps no goal module, every proof, and a project that builds.

Existing Lean tests: proofs in Inputs/ import their goal modules; tests that read Generated.lean read the project's text through Inputs/lean_project_text.py; lean_certify.cpp's admitted User lemma now fails through the checker (unfinished of CppVerify.User uses sorry); lean_certifier.test's shadowing message names the goal module.

Docs

• ch17: a new section, "One module of goals per function", with a checked example, the layout, a proof's imports, User, incremental certification, and fallback runs; the intro, "Goals as hypotheses", the automatic proof's imports, and "What certification checks" (the goal module, User's sorry).
• tooling.rst: --lean-project's modules.
• Release notes: "A Lean module per function".
• DESIGN.md, ARCHITECTURE.md: the design above.

Checked

• Lean tests: the 41 Verify tests that mention Lean, lean_modules.test among them, and the docs tests pass; VerifyTests: 62 passed, 1 skipped.
• Docs: check-doc-examples.py passes on every page this changes (32 examples, 8 against the verdicts their pages show), the new checked export included.
• Mutation: 11 mutants, all killed:
  • a proof imports no goal module; Generated imports none; specs declared in each goal module (the two modules that apply tri then clash);
  • a proof's key leaves out its imports (the change to dbl leaves its unchanged proofs out of the rebuild); every proof compiled again;
  • stale goal modules kept; no root module; a new User imports Generated; generated files always written;
  • the checker takes a goal defined anywhere (lean_certifier.test's shadowing proof); the checker ignores an admitted User lemma (lean_certify.cpp).
• Time. On these projects, compiling proofs is a small part of certification, so skipping unchanged ones saves a few seconds:
  • Inputs/lean_modules.cpp (12 goals): 7.3 s for an unchanged project, 8.7 s with every proof compiled again (its keys removed, which is what every run did before);
  • safe_fib.cpp (64 goals, 36 proved): 31.1 s against 33.6 s. A proof compiles in about 1 s, many at once; the run's time is the export with its solver checks (16 s) and the checker's replay of every project module through the kernel (9.6 s). That replay could be kept by the hash of each .olean too; it is left for later.
• lake --dir: through elan, lake --dir=P runs elan's default toolchain, not P's pin (it picks one by the working directory), so the test runs lake build inside the project.
• lean_toolchain.test: the trial of cppverify_auto builds Generated too, so its line in the log names it.