[SwayamInSync]

Certification compiled Check.lean, which imports the user's modules, and read the text that its example : G := G_proof and #print axioms G_proof printed. A proof author in bad faith could make it print anything. For this file, where one claims a false postcondition (Z3 finds the counterexample result = 1):

int fine()
  cppverify::post(cppverify::result == 1)
{
  return 1;
}

int one()
  cppverify::post(cppverify::result == 2)
{
  return 1;
}

Proof of one's postcondition	main	Now
theorem …_proof : True := trivial, and in User.lean two macro_rules that turn every example into #eval pure () and every #print axioms into a line saying "does not depend on any axioms"	Certified: one	Unresolved: … the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761_proof proves True, not cppverify_one_99bcee_postcondition_646d2761
a run_cmd that adds the theorem with the goal's type and the value True.intro, under set_option debug.skipKernelTC true, so no kernel checks it	Certified: one	… the kernel rejects CppVerify.Proofs.…: while replaying declaration '…_proof': (kernel) declaration type mismatch, '…_proof' has type True but it is expected to have type …
the same theorem, named cheat, in a module of the project, CppVerify/Lemmas.lean, and theorem …_proof : … := cheat	Certified: one	… the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': …
a proof file that does not import the generated goal and defines its own of the same name, def …_646d2761 : Prop := True, and proves that	Unresolved for both functions (Check.lean imports both definitions)	Certified: fine, and one unresolved: cppverify_one_99bcee_postcondition_646d2761 is not the goal CppVerify.Generated defines
an axiom escape {p : Prop} : p behind a lemma	Unresolved for both functions	Certified: fine, and one unresolved: … depends on the axiom escape, which is not one of Lean's foundations
sorry	Unresolved for both functions	Certified: fine, and one unresolved: … declaration uses 'sorry'

In every case the proofs of fine are sound. They are now certified whatever happens to one's.

Design

Decision 1 of the Lean plan: Certified holds against a proof author in bad faith, so it may rest on nothing the user's Lean source can influence. Vermilion searches its proof files for sorry as text; leanchecker, shipped with the pinned toolchain, replays a module's declarations through the kernel to catch environment hacking. This adds the rest:

• A checker that reads compiled modules (Driver/LeanCertifier.h, written into the project as .cppverify/Certify.lean and run with lake env lean --run). It elaborates none of the user's source, so no macro, notation, or command of theirs changes what it checks. For each goal:

  • it imports the proof's module;
  • the proof G_proof must be a theorem whose type is exactly the constant G, a definition of CppVerify.Generated, declared in that module;
  • its axioms, collected by walking the kernel constants it uses (not a cache a module could carry), must be among propext, Quot.sound, and Classical.choice;
  • every module of the import closure whose .olean is not the pinned toolchain's own is replayed through the kernel against its imports, as leanchecker's replayFromImports does, once per run.

  The checker never frees imported data, because a later import in the same process reads it. Freeing it, as withImportModules does, crashed the second import.

• Per-function results. Each proof file is built on its own (lean -EhasSorry), and a proof that does not build fails only its own goal. Each Lean result records its goals (VerifyResult::LeanGoals), and a function is Certified when every one of them passes. Otherwise it is Unresolved, naming each failing obligation and why.

• Check.lean is still generated, so lake build CppVerify.Check builds every proof at once, but certification no longer reads it.

Tests

• New suite/lean_certifier.test: the six cases in the table, each in its own copy of one project, with fine certified beside each.
• Updated: lean_certify.cpp expects the new message for its axiom case.
• On main and before this PR: the same RUN lines with verify: State each Lean goal as named hypotheses, with a bridge the kernel checks #59's binary print Certified: one [backend=Lean] for the rewritten checks, the theorem past the kernel, and the imported one, and Unresolved for fine with sorry or the axiom.

Mutants of LeanCertifier.h, Verifier.cpp, and VerifyBackend.cpp, each rebuilt and run against the certification tests: 11 of 13 killed.

• no kernel replay; only the toolchain's modules replayed; only the proof's own module replayed;

• the statement unchecked; the goal's module unchecked (killed by the shadowed goal, which I added after this mutant first survived); axioms allowed; the axioms of the lemmas a proof uses missed;

• a function's failed goals ignored; exports recording no goals; a proof that does not build not reported; sorry allowed in proof files.

  Two survive, both equivalent:

  • the check that G_proof is declared in the goal's own proof file. It is not needed for soundness: a proof declared in another module of the project is still replayed by the kernel and has the goal's type. It keeps each goal's proof in its own file, which LM3's moves rely on.
  • treating a goal the checker does not report as failed. The checker reports every goal it is given, so only a bug in the checker could reach this. It stays as a fail-closed default.

Docs

• tooling.rst: the --lean-certify row says what certification checks and that results are per function.
• Book, ch17: "What certification checks", with the rewrite attack and its exact output.
• Release notes: "Lean certification against proofs in bad faith" under wrong results fixed.
• ARCHITECTURE.md: "Certification" under the project goals. DESIGN.md: the certification rules.

Checked

• Lean tests: all 39 Verify tests that use Lean pass on a release build, lean_certifier.test among them.
• VerifyTests: 62 passed, 1 skipped.
• Docs: docs_examples.test and docs_coverage.test pass, with the ch17 example marked as failing one; the site builds with -W.
• clang-format: clean on the changed sources.
• The rest of the Verify suite is left to CI: outside Lean certification, this adds only VerifyResult::LeanGoals.