verify: Certify Lean proofs from their compiled modules, against proofs in bad faith

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;
 }
 

clang/lib/Verify/Backend/VerifyBackend.h

@@ -152,6 +152,9 @@ struct VerifyResult {
   /// individually; absent when the backend did not check each one.
   std::optional<std::vector<std::string>> UnprovedObligations;
   std::optional<ProofEvidence> Evidence;
+  /// For a module exported to a Lean project: the goals whose proofs prove
+  /// it, which certification checks.
+  std::vector<std::string> LeanGoals;
   /// For a counterexample: the specs whose postconditions decided a value
   /// its check needed, so that it rests on them.
   std::set<std::string> CertifiedWith;

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

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<std::map<std::string, std::string>>
   certifyLeanProject(const std::vector<LeanProjectGoal> &ProjectGoals) {
     if (ProjectGoals.empty())
       return llvm::createStringError(llvm::inconvertibleErrorCode(),
@@ -1945,6 +1950,8 @@ class Verifier {
     std::map<std::string, const LeanProjectGoal *> UniqueGoals;
     for (const LeanProjectGoal &Goal : ProjectGoals)
       UniqueGoals.emplace(Goal.Name, &Goal);
+    std::map<std::string, std::string> 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<llvm::StringRef> 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<llvm::StringRef> 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<std::string> Checks;
+    for (llvm::StringRef Rest = *Checked; !Rest.empty();) {
+      auto [Line, Next] = Rest.split('\n');
+      Rest = Next;
+      llvm::SmallVector<llvm::StringRef, 3> 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<std::string, const LeanProjectGoal *> 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

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;
+}

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

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

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

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

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 })