From 1f5244d270f0de882cb771049a886e1e38b934da Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:20 +0530 Subject: [PATCH 01/22] verify: Add a Lean certifier that checks compiled proofs through the kernel without elaborating user source. --- clang/lib/Verify/Driver/LeanCertifier.h | 132 ++++++++++++++++++++++++ 1 file changed, 132 insertions(+) create mode 100644 clang/lib/Verify/Driver/LeanCertifier.h diff --git a/clang/lib/Verify/Driver/LeanCertifier.h b/clang/lib/Verify/Driver/LeanCertifier.h new file mode 100644 index 0000000000..4b4bbd12ae --- /dev/null +++ b/clang/lib/Verify/Driver/LeanCertifier.h @@ -0,0 +1,132 @@ +//===--- LeanCertifier.h - The checker of Lean project proofs ----------===// +#ifndef LLVM_CLANG_VERIFY_DRIVER_LEANCERTIFIER_H +#define LLVM_CLANG_VERIFY_DRIVER_LEANCERTIFIER_H + +#include "llvm/ADT/StringRef.h" + +namespace clang { +namespace verify { + +/// A Lean program certification runs on a project's compiled modules. It +/// elaborates none of the user's source, so nothing the user writes changes +/// what it checks. +inline constexpr llvm::StringLiteral LeanCertifierSource = R"lean(import Lean +import Lean.Replay +open Lean + +/-- The axioms a constant depends on, through the statements and values of the +constants it uses, read from the kernel's constants. -/ +def axiomsOf (env : Environment) (root : Name) : Except String NameSet := Id.run do + let mut seen : NameSet := {} + let mut axioms : NameSet := {} + let mut work := #[root] + while h : 0 < work.size do + let c := work.back + work := work.pop + if seen.contains c then continue + seen := seen.insert c + let used (e : Expr) := e.getUsedConstants + match env.find? c with + | some (.axiomInfo v) => axioms := axioms.insert c; work := work ++ used v.type + | some (.defnInfo v) => work := work ++ used v.type ++ used v.value + | some (.thmInfo v) => work := work ++ used v.type ++ used v.value + | some (.opaqueInfo v) => work := work ++ used v.type ++ used v.value + | some (.quotInfo _) => pure () + | some (.ctorInfo v) => work := work ++ used v.type + | some (.recInfo v) => work := work ++ used v.type + | some (.inductInfo v) => work := work ++ used v.type ++ v.ctors.toArray + | none => return .error s!"{c} is not in the environment" + return .ok axioms + +/-- Replays a module's own constants into the environment of its imports with +the kernel, as leanchecker does: nothing in it escaped the kernel. -/ +unsafe def replayModule (module : Name) : IO Unit := do + let file ← findOLean module + let mut files := #[file] + let server := OLeanLevel.server.adjustFileName file + if ← server.pathExists then + files := files.push server + let priv := OLeanLevel.private.adjustFileName file + if ← priv.pathExists then + files := files.push priv + let parts ← readModuleDataParts files + if h : parts.size = 0 then throw <| IO.userError "cannot read the module" else + let (data, _) := parts[0] + let (_, s) ← importModulesCore data.imports |>.run + let env ← finalizeImport s data.imports {} 0 false false (isModule := true) + let mut constants := {} + for name in parts[parts.size - 1].1.constNames, info in parts[parts.size - 1].1.constants do + constants := constants.insert name info + discard <| env.toKernelEnv.replay constants + +/-- Whether the proof of a goal states exactly the goal the generated module +defines and depends on no axiom outside the allowed ones. -/ +def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) : + Option String := Id.run do + let generated := `CppVerify.Generated + let moduleOf (c : Name) : Option Name := + (env.getModuleIdxFor? c).bind fun i => env.header.moduleNames[i.toNat]? + let proof := goal.appendAfter "_proof" + match env.find? goal with + | some (.defnInfo _) => + if moduleOf goal != some generated then + return some s!"{goal} is not the goal {generated} defines" + | _ => return some s!"{generated} defines no goal {goal}" + match env.find? proof with + | some (.thmInfo v) => + if moduleOf proof != some module then + return some s!"{proof} is not declared in {module}" + if v.type != .const goal [] then + return some s!"{proof} proves {v.type}, not {goal}" + match axiomsOf env proof with + | .error e => return some e + | .ok axioms => + match axioms.toList.filter (!allowed.contains ·) with + | [] => return none + | [one] => + return some s!"{proof} depends on the axiom {one}, which is not one of Lean's foundations" + | many => + return some s!"{proof} depends on the axioms {", ".intercalate (many.map toString)}, which are not among Lean's foundations" + | some _ => return some s!"{proof} is not a theorem" + | none => return some s!"{module} declares no {proof}" + +/-- A goal is proved when every module of the project its proof imports passes +the kernel (each replayed once in a run), and its proof states exactly the +goal and uses only the allowed axioms. Imported data is never freed: a later +import in the process reads it. -/ +unsafe def checkGoal (goal module : Name) (allowed : NameSet) (toolchain : String) + (replayed : IO.Ref NameSet) : IO (Option String) := do + let env ← importModules #[{ module }] {} + let project ← env.header.moduleNames.filterM fun m => + return !(← findOLean m).toString.startsWith toolchain + let why := checkStatement env goal module allowed + for m in project do + if (← replayed.get).contains m then continue + try replayModule m + catch e => return some s!"the kernel rejects {m}: {e}" + replayed.modify (·.insert m) + return why + +/-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal and its +proof module, separated by a tab, and ALLOWED lists the axioms a proof may +use, separated by commas. Prints one line per goal: `ok` or `fail`, the goal, +and why it failed. -/ +unsafe def main (args : List String) : IO UInt32 := do + let [goals, allowed] := args | throw <| IO.userError "usage: Certify GOALS ALLOWED" + let sysroot ← findSysroot + initSearchPath sysroot + let toolchain := (sysroot / "lib" / "lean").toString + let allowed := (allowed.splitOn ",").foldl (fun s a => s.insert a.toName) ({} : NameSet) + let replayed ← IO.mkRef ({} : NameSet) + for line in ← IO.FS.lines goals do + let [goal, module] := line.splitOn "\t" | continue + match ← checkGoal goal.toName module.toName allowed toolchain replayed with + | none => IO.println s!"ok\t{goal}" + | some why => IO.println s!"fail\t{goal}\t{why.replace "\n" " "}" + return 0 +)lean"; + +} // namespace verify +} // namespace clang + +#endif From 47e1bca013160bc55a6623f7dd0f492267b4f46b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:21 +0530 Subject: [PATCH 02/22] verify: Give each verification result the Lean goals it exported. --- clang/lib/Verify/Backend/VerifyBackend.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 5bec7b6cdd..6159936740 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -152,6 +152,9 @@ struct VerifyResult { /// individually; absent when the backend did not check each one. std::optional> UnprovedObligations; std::optional Evidence; + /// For a module exported to a Lean project: the goals whose proofs prove + /// it, which certification checks. + std::vector LeanGoals; /// For a counterexample: the specs whose postconditions decided a value /// its check needed, so that it rests on them. std::set CertifiedWith; From 040ee379cfcbac06f32e030582ee19bb2cc846e4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:21 +0530 Subject: [PATCH 03/22] verify: Record the goals each Lean export writes on its result. --- clang/lib/Verify/Backend/VerifyBackend.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index 705b9e0864..134495fe9a 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -21,10 +21,15 @@ VerifyResult LeanVerifyBackend::verifyModule(const ObligationModule &Module) { R.Message = "no lean output stream"; return R; } + const size_t Before = ProjectGoals ? ProjectGoals->size() : 0; VerifyResult Result = exportLeanScratchPad( Module, *Out, !PreambleEmitted, EmittedFunctions, EmittedTheorems, ++ModuleIndex, ProjectGoals, Selection ? &*Selection : nullptr); PreambleEmitted = true; + if (ProjectGoals) + for (size_t I = Before; I < ProjectGoals->size(); ++I) + if ((*ProjectGoals)[I].Exported) + Result.LeanGoals.push_back((*ProjectGoals)[I].Name); return Result; } From 6602c131940148c3c98e4f4674d4569b7f0ba633 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:22 +0530 Subject: [PATCH 04/22] verify: Certify each Lean goal with the kernel checker and report the results per function. --- clang/lib/Verify/Driver/Verifier.cpp | 141 ++++++++++++++++----------- 1 file changed, 84 insertions(+), 57 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 6351861a55..331dd7749a 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -22,6 +22,7 @@ #include "../Transform/UBChecks.h" #include "CppVerifyVersion.h" #include "DumpIR.h" +#include "LeanCertifier.h" #include "clang/AST/ASTContext.h" #include "clang/Basic/SourceManager.h" #include "clang/Frontend/TextDiagnostic.h" @@ -1866,7 +1867,11 @@ class Verifier { CheckFile); } - llvm::Error + // Certifies each goal's proof: an error fails every goal; otherwise the + // goals whose proofs fail, each with why. A proof's own module must build + // without `sorry`; then the certifier (LeanCertifier.h) checks the compiled + // modules, which nothing in the user's source can change. + llvm::Expected> certifyLeanProject(const std::vector &ProjectGoals) { if (ProjectGoals.empty()) return llvm::createStringError(llvm::inconvertibleErrorCode(), @@ -1945,6 +1950,8 @@ class Verifier { std::map UniqueGoals; for (const LeanProjectGoal &Goal : ProjectGoals) UniqueGoals.emplace(Goal.Name, &Goal); + std::map Failures; + std::string Built; for (const auto &[Name, Goal] : UniqueGoals) { std::string File; const std::string ProofSource = @@ -1956,54 +1963,52 @@ class Verifier { EC, "cannot create Lean proof build directory"); const std::string ProofObject = leanProjectPath(ObjectDir, {Name + ".olean"}); + llvm::sys::fs::remove(ProofObject); if (auto Proof = runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", ProofObject, ProofSource}, Name); - !Proof) - return Proof.takeError(); + !Proof) { + Failures[Name] = + llvm::StringRef(llvm::toString(Proof.takeError())).rtrim().str(); + continue; + } + Built += Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + "\n"; } + if (Built.empty()) + return Failures; - auto Check = runLake({"env", "lean", "-R", Root, - leanProjectPath(Root, {"CppVerify", "Check.lean"})}, - "check"); - if (!Check) - return Check.takeError(); - - const std::set AllowedAxioms = {"propext", "Quot.sound", - "Classical.choice"}; - unsigned Reports = 0; - llvm::StringRef Report = *Check; - llvm::StringRef NoAxioms = "does not depend on any axioms"; - for (size_t Pos = Report.find(NoAxioms); Pos != llvm::StringRef::npos; - Pos = Report.find(NoAxioms, Pos + NoAxioms.size())) - ++Reports; - llvm::StringRef HasAxioms = "depends on axioms:"; - for (size_t Pos = Report.find(HasAxioms); Pos != llvm::StringRef::npos; - Pos = Report.find(HasAxioms, Pos + HasAxioms.size())) { - ++Reports; - const size_t Open = Report.find('[', Pos + HasAxioms.size()); - const size_t Close = Open == llvm::StringRef::npos - ? llvm::StringRef::npos - : Report.find(']', Open + 1); - if (Open == llvm::StringRef::npos || Close == llvm::StringRef::npos) - return llvm::createStringError( - llvm::inconvertibleErrorCode(), - "malformed Lean axiom-dependency report"); - llvm::SmallVector Axioms; - Report.slice(Open + 1, Close).split(Axioms, ',', -1, false); - for (llvm::StringRef Axiom : Axioms) { - Axiom = Axiom.trim(); - if (!Axiom.empty() && !AllowedAxioms.count(Axiom)) - return llvm::createStringError( - llvm::inconvertibleErrorCode(), - "proof depends on undocumented axiom %s", Axiom.str().c_str()); - } + const std::string Certifier = + leanProjectPath(Root, {".cppverify", "Certify.lean"}); + const std::string GoalList = leanProjectPath(Root, {".cppverify", "goals"}); + if (std::error_code EC = llvm::sys::fs::create_directories( + llvm::sys::path::parent_path(Certifier))) + return llvm::createStringError(EC, "cannot create %s", Certifier.c_str()); + if (llvm::Error Error = writeTextFile(Certifier, LeanCertifierSource)) + return std::move(Error); + if (llvm::Error Error = writeTextFile(GoalList, Built)) + return std::move(Error); + auto Checked = runLake({"env", "lean", "--run", Certifier, GoalList, + "propext,Quot.sound,Classical.choice"}, + "certify"); + if (!Checked) + return Checked.takeError(); + std::set Checks; + for (llvm::StringRef Rest = *Checked; !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + llvm::SmallVector Fields; + Line.split(Fields, '\t', 2); + if (Fields.size() < 2 || (Fields[0] != "ok" && Fields[0] != "fail")) + continue; + Checks.insert(Fields[1].str()); + if (Fields[0] == "fail") + Failures[Fields[1].str()] = + Fields.size() == 3 ? Fields[2].str() : "the certifier failed"; } - if (Reports != UniqueGoals.size()) - return llvm::createStringError( - llvm::inconvertibleErrorCode(), - "Lean did not report axiom dependencies for every proof"); - return llvm::Error::success(); + for (const auto &[Name, Goal] : UniqueGoals) + if (!Failures.count(Name) && !Checks.count(Name)) + Failures[Name] = "the certifier did not check it"; + return Failures; } void checkCalleeRecommendsOnFailure(const VFunction &Caller, @@ -3630,28 +3635,50 @@ class Verifier { if (Finding.FindingOf == Index) Finding.Hidden = true; }; - if (llvm::Error Error = certifyLeanProject(ExportedGoals)) { + auto failed = [&](size_t Index, const std::string &Reason) { AllOk = false; AnyFailed = true; - const std::string Reason = llvm::toString(std::move(Error)); - for (size_t Index = 0; Index != Diags.size(); ++Index) { - VerifyDiagnostic &Diagnostic = Diags[Index]; - if (Diagnostic.K != VerifyDiagnostic::Exported) - continue; - unproved(Index); - Diagnostic.Message += - " (Lean certification failed: " + Reason + ")"; - if (Diagnostic.Result) { - Diagnostic.Result->Status = VerifyStatus::Unresolved; - Diagnostic.Result->Reason = VerifyReason::LeanExportFailure; - Diagnostic.Result->Message = Reason; - } + VerifyDiagnostic &Diagnostic = Diags[Index]; + unproved(Index); + Diagnostic.Message += " (Lean certification failed: " + Reason + ")"; + if (Diagnostic.Result) { + Diagnostic.Result->Status = VerifyStatus::Unresolved; + Diagnostic.Result->Reason = VerifyReason::LeanExportFailure; + Diagnostic.Result->Message = Reason; } + }; + auto Certified = certifyLeanProject(ExportedGoals); + std::map GoalsByName; + for (const LeanProjectGoal &Goal : ExportedGoals) + GoalsByName.emplace(Goal.Name, &Goal); + if (!Certified) { + const std::string Reason = llvm::toString(Certified.takeError()); + for (size_t Index = 0; Index != Diags.size(); ++Index) + if (Diags[Index].K == VerifyDiagnostic::Exported) + failed(Index, Reason); } else { for (size_t Index = 0; Index != Diags.size(); ++Index) { VerifyDiagnostic &Diagnostic = Diags[Index]; if (Diagnostic.K != VerifyDiagnostic::Exported) continue; + // Each goal of the function is certified, or it is not. + std::string Reason; + if (Diagnostic.Result) + for (const std::string &Goal : Diagnostic.Result->LeanGoals) + if (auto Failure = Certified->find(Goal); + Failure != Certified->end()) { + auto Known = GoalsByName.find(Goal); + Reason += + (Reason.empty() ? "" : "; ") + + std::string("the proof of ") + + (Known != GoalsByName.end() ? Known->second->StableId + : Goal) + + ": " + Failure->second; + } + if (!Reason.empty()) { + failed(Index, Reason); + continue; + } const ProofEvidence *Evidence = Diagnostic.Result && Diagnostic.Result->Evidence ? &*Diagnostic.Result->Evidence From d7c7f684399ae6dfff1b6c2b85c95497db10e221 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:23 +0530 Subject: [PATCH 05/22] test: Add a sound and an unsound function for the Lean certifier test. --- clang/test/Verify/suite/Inputs/lean_certifier.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier.cpp diff --git a/clang/test/Verify/suite/Inputs/lean_certifier.cpp b/clang/test/Verify/suite/Inputs/lean_certifier.cpp new file mode 100644 index 0000000000..119573e91a --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier.cpp @@ -0,0 +1,11 @@ +int fine() + cppverify::post(cppverify::result == 1) +{ + return 1; +} + +int one() + cppverify::post(cppverify::result == 2) +{ + return 1; +} From 3c312de697c405789df2dc8ad50ff88ee8c11f56 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:23 +0530 Subject: [PATCH 06/22] test: Add the proof that fine returns for the Lean certifier test. --- .../cppverify_fine_52006a_missing_return_54ae7c80.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean new file mode 100644 index 0000000000..24d917ca90 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +theorem cppverify_fine_52006a_missing_return_54ae7c80_proof : cppverify_fine_52006a_missing_return_54ae7c80 := by + apply cppverify_fine_52006a_missing_return_54ae7c80.of_readable + trivial From e523e971e0bf39f58482526871d1982c0e8c2b0d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:24 +0530 Subject: [PATCH 07/22] test: Add the proof of fine's postcondition for the Lean certifier test. --- .../cppverify_fine_52006a_postcondition_cd6bdfcd.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean new file mode 100644 index 0000000000..2d440f8a0e --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean @@ -0,0 +1,6 @@ +import CppVerify.User + +theorem cppverify_fine_52006a_postcondition_cd6bdfcd_proof : cppverify_fine_52006a_postcondition_cd6bdfcd := by + apply cppverify_fine_52006a_postcondition_cd6bdfcd.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 h_null_1 h_null_2 h_result_1 + exact h_result_1 From 5ae7545c95ffa69318f44f7212c875281f23a666 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:24 +0530 Subject: [PATCH 08/22] test: Add the proof that one returns for the Lean certifier test. --- .../cppverify_one_99bcee_missing_return_54ae7c80.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean new file mode 100644 index 0000000000..f7d3d1a1a7 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : cppverify_one_99bcee_missing_return_54ae7c80 := by + apply cppverify_one_99bcee_missing_return_54ae7c80.of_readable + trivial From c05e794d0162a51bb3933f0786ee4f9cdd39111d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:25 +0530 Subject: [PATCH 09/22] test: Add macros that rewrite the generated checks for the Lean certifier test. --- .../Inputs/lean_certifier_proofs/rewritten/User.lean | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/User.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/User.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/User.lean new file mode 100644 index 0000000000..5f8ac7b7be --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/User.lean @@ -0,0 +1,8 @@ +import CppVerify.Generated + +/- Checks rewritten: every `example` vanishes, and every `#print axioms` + reports none. -/ +macro_rules + | `(command| example : $_ := $_) => `(command| #eval pure ()) +macro_rules + | `(command| #print axioms $_) => `(command| #eval IO.println "does not depend on any axioms") From cc942c373b8ffd1dd2a3bf03ad137899889dd90a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:26 +0530 Subject: [PATCH 10/22] test: Add a proof of True behind rewritten checks for the Lean certifier test. --- .../rewritten/cppverify_one_99bcee_postcondition_646d2761.lean | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean new file mode 100644 index 0000000000..f5ce026671 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean @@ -0,0 +1,3 @@ +import CppVerify.User + +theorem cppverify_one_99bcee_postcondition_646d2761_proof : True := trivial From f5075d1526edb40f6e2d8d136b93837bfc2170a3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:26 +0530 Subject: [PATCH 11/22] test: Add a theorem added past the kernel for the Lean certifier test. --- .../cppverify_one_99bcee_postcondition_646d2761.lean | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean new file mode 100644 index 0000000000..296d7e4797 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean @@ -0,0 +1,9 @@ +import CppVerify.User +import Lean + +/- A theorem of the goal whose value is a proof of True, added without the + kernel. -/ +open Lean Elab Command in +set_option debug.skipKernelTC true in +run_cmd liftTermElabM do + addDecl (.thmDecl { name := `cppverify_one_99bcee_postcondition_646d2761_proof, levelParams := [], type := mkConst `cppverify_one_99bcee_postcondition_646d2761, value := mkConst ``True.intro }) From ee117adbd288f88472cdb0b02272172a1ef82a63 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:27 +0530 Subject: [PATCH 12/22] test: Add a project lemma added past the kernel for the Lean certifier test. --- .../Inputs/lean_certifier_proofs/imported/Lemmas.lean | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean new file mode 100644 index 0000000000..0897c5c20f --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean @@ -0,0 +1,8 @@ +import CppVerify.User +import Lean + +/- The same, in a module of the project the proof imports. -/ +open Lean Elab Command in +set_option debug.skipKernelTC true in +run_cmd liftTermElabM do + addDecl (.thmDecl { name := `cheat, levelParams := [], type := mkConst `cppverify_one_99bcee_postcondition_646d2761, value := mkConst ``True.intro }) From 3cc2a398d57d4bbd5d476b867315d6b077cc1768 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:28 +0530 Subject: [PATCH 13/22] test: Add a proof by an unchecked imported lemma for the Lean certifier test. --- .../imported/cppverify_one_99bcee_postcondition_646d2761.lean | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/cppverify_one_99bcee_postcondition_646d2761.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/cppverify_one_99bcee_postcondition_646d2761.lean new file mode 100644 index 0000000000..0cb5b515d0 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/cppverify_one_99bcee_postcondition_646d2761.lean @@ -0,0 +1,3 @@ +import CppVerify.Lemmas + +theorem cppverify_one_99bcee_postcondition_646d2761_proof : cppverify_one_99bcee_postcondition_646d2761 := cheat From 2fd2e5606b8a9feb8160bd83978226a93e604ad9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:28 +0530 Subject: [PATCH 14/22] test: Add a proof of a goal the proof file defines itself for the Lean certifier test. --- .../cppverify_one_99bcee_postcondition_646d2761.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/shadowed/cppverify_one_99bcee_postcondition_646d2761.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/shadowed/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/shadowed/cppverify_one_99bcee_postcondition_646d2761.lean new file mode 100644 index 0000000000..27221ec931 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/shadowed/cppverify_one_99bcee_postcondition_646d2761.lean @@ -0,0 +1,5 @@ +/- A goal of the same name of its own, true, in place of the generated one, + which this file does not import. -/ +def cppverify_one_99bcee_postcondition_646d2761 : Prop := True + +theorem cppverify_one_99bcee_postcondition_646d2761_proof : cppverify_one_99bcee_postcondition_646d2761 := trivial From c56268e540c5ccd4ab5a0961dddf8eafd51f22ac Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:29 +0530 Subject: [PATCH 15/22] test: Add a proof by an axiom behind a lemma for the Lean certifier test. --- .../cppverify_one_99bcee_postcondition_646d2761.lean | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean new file mode 100644 index 0000000000..823511abad --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean @@ -0,0 +1,8 @@ +import CppVerify.User + +/- An axiom behind a lemma. -/ +axiom escape {p : Prop} : p + +theorem helper : cppverify_one_99bcee_postcondition_646d2761 := escape + +theorem cppverify_one_99bcee_postcondition_646d2761_proof : cppverify_one_99bcee_postcondition_646d2761 := helper From 31bd4c126daf6a6b0d9c6e5322a55aa5d2f9daf4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:29 +0530 Subject: [PATCH 16/22] test: Check that Lean certification resists proofs in bad faith and reports per function. --- clang/test/Verify/suite/lean_certifier.test | 65 +++++++++++++++++++++ 1 file changed, 65 insertions(+) create mode 100644 clang/test/Verify/suite/lean_certifier.test diff --git a/clang/test/Verify/suite/lean_certifier.test b/clang/test/Verify/suite/lean_certifier.test new file mode 100644 index 0000000000..1990b479e6 --- /dev/null +++ b/clang/test/Verify/suite/lean_certifier.test @@ -0,0 +1,65 @@ +# REQUIRES: lean +# +# Certification holds against a proof author in bad faith. It checks the +# compiled modules with a program that elaborates none of the user's source: +# the kernel replays every module of the project a proof imports, the proof +# must state its goal, and it may depend on no axiom but Lean's foundations. +# Each function is certified on its own goals. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/base %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_fine_* %t/base/CppVerify/Proofs/cppverify_fine_52006a/ +# RUN: cp %S/Inputs/lean_certifier_proofs/cppverify_one_* %t/base/CppVerify/Proofs/cppverify_one_99bcee/ +# +# The function whose proofs check is certified, whatever the other's are. +# RUN: cp -r %t/base %t/sorry +# RUN: not %cpp-verify --backend=lean --lean-project=%t/sorry --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=SORRY +# +# Macros of the user's that rewrite the checks of Check.lean, and a proof of +# True for the false postcondition. +# RUN: cp -r %t/base %t/rewritten +# RUN: cp %S/Inputs/lean_certifier_proofs/rewritten/User.lean %t/rewritten/CppVerify/ +# RUN: cp %S/Inputs/lean_certifier_proofs/rewritten/cppverify_one_* %t/rewritten/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: not %cpp-verify --backend=lean --lean-project=%t/rewritten --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=REWRITTEN +# +# A theorem of the goal added without the kernel, in the proof module, then in +# a module of the project the proof imports. +# RUN: cp -r %t/base %t/unchecked +# RUN: cp %S/Inputs/lean_certifier_proofs/unchecked/cppverify_one_* %t/unchecked/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: not %cpp-verify --backend=lean --lean-project=%t/unchecked --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=UNCHECKED +# RUN: cp -r %t/base %t/imported +# RUN: cp %S/Inputs/lean_certifier_proofs/imported/Lemmas.lean %t/imported/CppVerify/ +# RUN: cp %S/Inputs/lean_certifier_proofs/imported/cppverify_one_* %t/imported/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: cd %t/imported && lake build CppVerify.Lemmas +# RUN: not %cpp-verify --backend=lean --lean-project=%t/imported --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=IMPORTED +# +# A goal of the same name defined in the proof's own file. +# RUN: cp -r %t/base %t/shadowed +# RUN: cp %S/Inputs/lean_certifier_proofs/shadowed/cppverify_one_* %t/shadowed/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: not %cpp-verify --backend=lean --lean-project=%t/shadowed --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=SHADOWED +# +# An axiom behind a lemma. +# RUN: cp -r %t/base %t/hidden +# RUN: cp %S/Inputs/lean_certifier_proofs/hidden/cppverify_one_* %t/hidden/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: not %cpp-verify --backend=lean --lean-project=%t/hidden --lean-certify %S/Inputs/lean_certifier.cpp -- 2>&1 | FileCheck %s --check-prefix=HIDDEN + +# EXPORT: Exported: lean obligation: fine +# EXPORT-NEXT: Exported: lean obligation: one + +# SORRY: Certified: fine [backend=Lean] +# SORRY-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: command failed with exit code 1: {{.*}}cppverify_one_99bcee_postcondition_646d2761.lean:11:8: error: declaration uses `sorry`) + +# REWRITTEN: Certified: fine [backend=Lean] +# REWRITTEN-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761_proof proves True, not cppverify_one_99bcee_postcondition_646d2761) + +# UNCHECKED: Certified: fine [backend=Lean] +# UNCHECKED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: the kernel rejects CppVerify.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_postcondition_646d2761: while replaying declaration 'cppverify_one_99bcee_postcondition_646d2761_proof': (kernel) declaration type mismatch, 'cppverify_one_99bcee_postcondition_646d2761_proof' has type True but it is expected to have type cppverify_one_99bcee_postcondition_646d2761) + +# IMPORTED: Certified: fine [backend=Lean] +# IMPORTED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: the kernel rejects CppVerify.Lemmas: while replaying declaration 'cheat': (kernel) declaration type mismatch, 'cheat' has type True but it is expected to have type cppverify_one_99bcee_postcondition_646d2761) + +# SHADOWED: Certified: fine [backend=Lean] +# SHADOWED-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761 is not the goal CppVerify.Generated defines) + +# HIDDEN: Certified: fine [backend=Lean] +# HIDDEN-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761_proof depends on the axiom escape, which is not one of Lean's foundations) From 73842fd12766fbb167adfcbc19190b00ea4e6c7f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:30 +0530 Subject: [PATCH 17/22] test: Expect the certifier's message for a proof that uses an axiom. --- clang/test/Verify/suite/lean_certify.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/lean_certify.cpp b/clang/test/Verify/suite/lean_certify.cpp index 00c6550f43..0a2532b383 100644 --- a/clang/test/Verify/suite/lean_certify.cpp +++ b/clang/test/Verify/suite/lean_certify.cpp @@ -30,5 +30,5 @@ void trivial() // USER-ADMITTED: Unresolved: lean obligation: trivial (Lean certification failed: // USER-ADMITTED-SAME: User.lean // USER-ADMITTED-SAME: declaration uses `sorry` -// AXIOM: Unresolved: lean obligation: trivial (Lean certification failed: proof depends on undocumented axiom escape) +// AXIOM: Unresolved: lean obligation: trivial (Lean certification failed: the proof of {{.*}}::missing-return@synthetic: cppverify_trivial_3e4f5a_missing_return_ba8abb90_proof depends on the axiom escape, which is not one of Lean's foundations; the proof of {{.*}}::postcondition@{{[0-9]+}}:{{[0-9]+}}: cppverify_trivial_3e4f5a_postcondition_ba8abb90_proof depends on the axiom escape, which is not one of Lean's foundations) // STALE: Unresolved: lean obligation: trivial (Lean certification failed: From dc8cc1ad8fcec8ec6fcc029f8ecc2d8fc5808535 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:31 +0530 Subject: [PATCH 18/22] docs: Describe how Lean certification checks compiled proofs. --- docs/ARCHITECTURE.md | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 8391cc3d27..31db136f7f 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1607,7 +1607,29 @@ uses when the source around it changes. stub its `intro` list. On the 375 suite exports, the 351 that built before still build, with every bridge. -`lean_readable.cpp` checks the readable form of each kind of assumption, +- **Certification** (`certifyLeanProject`) builds `Generated` and `User`, + then each proof file with `lean -EhasSorry`, recording the goals whose + proofs do not build, and runs the checker of `LeanCertifier.h`, written + into the project as `.cppverify/Certify.lean`, with `lake env lean --run` + over the goals that built. The checker elaborates none of the user's + source, so their macros and commands cannot change what it checks. For each + goal it imports the proof module (never freeing imported data, which a + later import in the process reads), checks that `G_proof` is a theorem of + type exactly `.const G []` with `G` a definition of `CppVerify.Generated`, + collects its axioms by walking the kernel constants it uses, and replays + through the kernel (as `leanchecker`'s `replayFromImports`) every module of + the import closure whose `.olean` lies outside the toolchain, each once in + a run. It prints `ok` or `fail` with the reason per goal. Each Lean result + records its goals (`VerifyResult::LeanGoals`), and a function is + `Certified` only when all of them pass; a failure names the obligation. + Before 0.2 certification parsed what `Check.lean` printed, which imports + the user's modules: macros there certified proofs of `True`, and so did a + theorem added with `debug.skipKernelTC`. + +`lean_certifier.test` checks each of those attacks, a proof file that defines +a goal of the same name of its own (the type check alone would take it), a +proof that does not build, and an axiom behind a lemma, with a function whose +proofs are sound certified beside each. `lean_readable.cpp` checks the readable form of each kind of assumption, the bridge, the stubs (every one builds), a proof by hypothesis names that certifies, and a readable form that says less than its goal, which fails at its bridge. `lean_identity.test` walks one project through each case (insertion and From f469bca97aac1c9149ba67bcd1a6e471913d5f96 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:31 +0530 Subject: [PATCH 19/22] docs: State the rules Lean certification enforces. --- docs/DESIGN.md | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 124ba4bd64..5f85e263d7 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1904,11 +1904,18 @@ G`, generated and kernel-checked with the generated file: the canonical goal stays what certification checks and identity hashes, and a printer bug in the readable form cannot certify anything. A stub applies the bridge and introduces every name. Initial generation is `Exported`. Certification -compiles the user module and every active proof with `sorry` as an error, then -checks aggregate theorem types and axiom dependencies. Only foundational Lean -axioms are permitted; user `axiom`/`opaque` proof shortcuts, stale proof types, -missing proofs, malformed output, and toolchain failures remain `Unresolved`. -Only complete success is `Certified`. Certification runs the pinned toolchain +holds against a proof author in bad faith. It compiles the user module and each +proof file on its own with `sorry` as an error, then runs a checker +(`LeanCertifier.h`) on the compiled modules, which elaborates none of the +user's source, so no macro, notation, or command of theirs changes what it +checks: the kernel replays every module of the project a proof imports (only +the pinned toolchain's own modules are trusted), as `leanchecker` does, so no +declaration escaped the kernel; the proof's type is exactly the constant of its +goal, which `CppVerify.Generated` defines; and the axioms it depends on, +collected from the constants it uses, are among `propext`, `Quot.sound`, and +`Classical.choice`. A function is `Certified` when every one of its goals +passes, and a failing goal leaves only its own function `Unresolved`, with the +obligation and the reason. Certification runs the pinned toolchain whatever elan's default is, and a project pinned by an earlier release moves to the current pin with a warning; any other pin is an error. From 8eb65262303d59a9095deac2131d77825789dc07 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:32 +0530 Subject: [PATCH 20/22] docs: Say what --lean-certify checks and that its results are per function. --- website/source/language/tooling.rst | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 38d255fdf4..ce68559539 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -289,9 +289,16 @@ Backends ``decide`` evaluates the machine comparisons at constants (:doc:`../book/part-ii/ch17-backends-modular-calls`). * - ``--lean-certify`` - - Build the active project with the pinned Lean 4.35.0, reject ``sorry`` and - undocumented proof axioms, and report ``Certified`` only after every - active proof kernel-checks. Certification runs whatever else failed, + - Build the active project with the pinned Lean 4.35.0, each proof file on + its own and without ``sorry``, then check the compiled modules with a + program that elaborates none of the user's source: the kernel replays + every module of the project a proof imports, the proof must state + exactly its goal, and it may depend on no axiom but ``propext``, + ``Quot.sound``, and ``Classical.choice``. A function whose goals all + pass is ``Certified``; one that has a goal that fails is ``Unresolved``, + with the obligation and why, such as ``the proof of + fn_…::postcondition@8:37: …_proof proves True, not …``, whatever the + other functions' proofs are. Certification runs whatever else failed, before the facts verdicts rest on are settled: a result proved in Lean rests on the callee contracts and spec facts its module uses, as a solver's does, and gets the same qualifiers and vacuity checks (run From 06991f5aabb18586ced04944f0ee8eeab187ff8c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:32 +0530 Subject: [PATCH 21/22] docs: Show what Lean certification checks with a rewrite attack and its output. --- .../part-ii/ch17-backends-modular-calls.rst | 68 +++++++++++++++++-- 1 file changed, 64 insertions(+), 4 deletions(-) diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 4f14e14faa..24765588c7 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -156,16 +156,16 @@ For an explicit interactive proof: # complete proof/CppVerify/Proofs/*/*.lean; put shared lemmas in User.lean cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp -``Generated.lean`` and ``Check.lean`` are machine-owned. +``Generated.lean`` and ``Check.lean`` are machine-owned; ``Check.lean`` imports +every proof, so ``lake build CppVerify.Check`` builds them all at once. ``User.lean`` is never overwritten, and each goal has a proof file of its own, which cpp-verify never rewrites but moves with its goal (see `Proofs that follow their goals`_ below). The project pins ``leanprover/lean4:v4.35.0``, which certification runs whatever elan's default toolchain is; a project 0.1 generated, pinned to ``v4.32.2``, moves to it with a warning. Certification compiles the user -module and every active proof with admissions promoted to errors, checks the -aggregate module, and rejects proof dependencies other than Lean's documented -foundational axioms. +module and each proof file with admissions promoted to errors, then checks the +compiled modules as described in `What certification checks`_ below. Each goal in ``Generated.lean`` is a Lean proposition that means what the obligation means, so a proof of it is a proof of the obligation: @@ -468,6 +468,66 @@ that cpp-verify 0.1 wrote for fn_5f5a3373697876::postcondition@8:37 is now CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean``. A 0.1 proof of a goal the source no longer has is kept in ``Stale/``. +What certification checks +~~~~~~~~~~~~~~~~~~~~~~~~~ + +``Certified`` holds against a proof author in bad faith, so it cannot rest on +anything the user's Lean source does. After the build, a checker that +cpp-verify ships runs on the compiled modules and elaborates none of the +user's source. For each goal: + +- the kernel replays every declaration of every module of the project the + proof imports, as ``leanchecker`` does, so nothing escaped the kernel; only + the pinned toolchain's own modules are trusted; +- the proof ``G_proof`` must be a theorem whose type is exactly the goal + ``G`` that ``CppVerify.Generated`` defines; +- the axioms it depends on, collected from the constants it uses, must be + among ``propext``, ``Quot.sound``, and ``Classical.choice``. + +Each function is certified on its own goals. For this file, where ``one`` +claims a false postcondition: + +.. cppverify-example: fails one + +.. code-block:: cpp + + int fine() + cppverify::post(cppverify::result == 1) + { + return 1; + } + + int one() + cppverify::post(cppverify::result == 2) + { + return 1; + } + +a ``User.lean`` that rewrites what a check file would print, + +.. code-block:: lean4 + + import CppVerify.Generated + + macro_rules + | `(command| example : $_ := $_) => `(command| #eval pure ()) + macro_rules + | `(command| #print axioms $_) => `(command| #eval IO.println "does not depend on any axioms") + +with a proof of ``True`` for the postcondition of ``one`` and true proofs +for the rest, gives: + +.. code-block:: text + + Certified: fine [backend=Lean] + Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761_proof proves True, not cppverify_one_99bcee_postcondition_646d2761) + +A theorem of the goal added by a command with ``debug.skipKernelTC``, which +skips the kernel, is rejected at its replay (``the kernel rejects +CppVerify.Lemmas: while replaying declaration 'cheat': (kernel) declaration +type mismatch``), and a user axiom behind a lemma by its name (``depends on +the axiom escape, which is not one of Lean's foundations``). + Portable obligation archives ---------------------------- From e3b67aa957f063213825d9e9dfa8886fe8903222 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:29:33 +0530 Subject: [PATCH 22/22] docs: Note that Lean certification now holds against proofs in bad faith. --- website/source/release-notes.rst | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index f3cbd5c605..2a61d4bcc1 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -83,6 +83,19 @@ analyzer reported nothing after a ghost block; libclang hid the constructs; and a contract expression in a template's signature produced a malformed symbol. Each now behaves by the construct's meaning (:doc:`language/tooling`). +**Lean certification against proofs in bad faith.** Certification compiled +``Check.lean``, which imports the user's modules, and read the text that its +``example : G := G_proof`` and ``#print axioms`` printed. So a few macros in +``User.lean`` that rewrote those two commands certified proofs of ``True`` for +a false postcondition, and so did a theorem of the goal added by a command +with ``debug.skipKernelTC`` and checked by no kernel, in the proof file or in a +module it imports. Certification now checks the compiled modules with a +program that elaborates none of the user's source: the kernel replays every +module of the project a proof imports, the proof's type must be exactly its +goal, and its axioms are collected from the constants it uses. A failing +proof also no longer fails every function of the project: each function is +certified on its own goals (:doc:`book/part-ii/ch17-backends-modular-calls`). + **Lean goals keep their grouping.** The Lean export placed parentheses by a precedence table of its own, not Lean's, so ``(a ^ b) + 1`` became ``a_0 ^^^ b_0 + 1``, which Lean reads as ``a ^^^ (b + 1)``. With