verify: Keep each Lean proof with the goal of its statement

.github/workflows/cppverify-ci.yml

@@ -26,7 +26,7 @@ concurrency:
 
 env:
   CVC5_VERSION: "1.1.2"
-  LEAN_TOOLCHAIN: "leanprover/lean4:v4.32.2"
+  LEAN_TOOLCHAIN: "leanprover/lean4:v4.35.0"
 
 jobs:
   linux:

README.md

@@ -43,7 +43,7 @@ Binaries: `build/bin/cpp-verify`, `build/bin/clang++`, `build/bin/clangd`, and `
 Z3 4.13.4 is built in: from the `third_party/z3` submodule, or, without it, cloned during the first build. See `third_party/README.md`. Two backends are optional and found on `PATH`:
 
 - cvc5, for `--backend=cvc5`, `portfolio`, and `race` (tested with 1.1.2): `apt install cvc5` on Ubuntu 24.04, or a [cvc5 release](https://github.com/cvc5/cvc5/releases/tag/cvc5-1.1.2) for Linux, macOS, or Windows; `--cvc5-path` names another executable.
-- Lean 4, for `--lean-certify` and `--lean-fallback`: install [elan](https://github.com/leanprover/elan); generated projects pin `leanprover/lean4:v4.32.2`.
+- Lean 4, for `--lean-certify` and `--lean-fallback`: install [elan](https://github.com/leanprover/elan); generated projects pin `leanprover/lean4:v4.35.0`.
 
 `cpp-verify --version` shows the cpp-verify release, the LLVM release it is built on, and the Z3, cvc5, and Lean versions it uses.
 

clang/lib/Verify/Backend/LeanBackend.cpp

@@ -1,6 +1,9 @@
 //===--- LeanBackend.cpp --------------------------------------------------===//
 #include "LeanBackend.h"
+#include "ObligationSerialization.h"
 #include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallString.h"
+#include "llvm/Support/MD5.h"
 #include "llvm/Support/raw_ostream.h"
 #include <cctype>
 #include <map>
@@ -59,6 +62,32 @@ static std::string encodeLeanName(llvm::StringRef Name) {
   return Encoded;
 }
 
+// The characters a Lean identifier takes; the others become `_`.
+static std::string leanIdentifierPart(llvm::StringRef Text) {
+  std::string Part;
+  for (char C : Text)
+    Part += std::isalnum(static_cast<unsigned char>(C)) ? C : '_';
+  return Part;
+}
+
+static std::string leanShortHash(llvm::StringRef Text, unsigned Digits) {
+  llvm::MD5 Hasher;
+  llvm::MD5::MD5Result Hash;
+  Hasher.update(Text);
+  Hasher.final(Hash);
+  llvm::SmallString<32> Hex;
+  llvm::MD5::stringifyResult(Hash, Hex);
+  return llvm::StringRef(Hex).take_front(Digits).str();
+}
+
+std::string verify::leanProjectGroup(const ObligationModule &Module) {
+  return "cppverify_" +
+         leanIdentifierPart(Module.FunctionName.empty()
+                                ? llvm::StringRef("goal")
+                                : llvm::StringRef(Module.FunctionName)) +
+         "_" + leanShortHash(Module.FunctionIdentity, 6);
+}
+
 static void printLeanName(llvm::StringRef Name, llvm::raw_ostream &OS) {
   OS << encodeLeanName(Name);
 }
@@ -899,7 +928,7 @@ VerifyResult verify::exportLeanScratchPad(
     const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble,
     std::set<std::string> &EmittedFunctions,
     std::set<std::string> &EmittedTheorems, unsigned ModuleIndex,
-    std::vector<std::string> *ProjectGoals,
+    std::vector<LeanProjectGoal> *ProjectGoals,
     const std::set<std::string> *Selection) {
   VerifyResult Result;
   if (!Module.CorrectnessGoal || !Module.CounterexampleQuery) {
@@ -911,7 +940,23 @@ VerifyResult verify::exportLeanScratchPad(
 
   LeanEmissionFailed = false;
   LeanLogicFunctions = &Module.LogicFunctions;
-  LeanBodyPrefix = "cppSpecBody_m" + std::to_string(ModuleIndex) + "_";
+  // A project names everything by identity, never by position, so that a
+  // proof keeps the names it uses when the source around it changes.
+  const std::string LegacyBodyPrefix =
+      "cppSpecBody_m" + std::to_string(ModuleIndex) + "_";
+  LeanBodyPrefix = LegacyBodyPrefix;
+  std::string Group;
+  if (ProjectGoals) {
+    Group = leanProjectGroup(Module);
+    LeanBodyPrefix =
+        "cppSpecBody_" + leanShortHash(Module.FunctionIdentity, 8) + "_";
+    // Modules of one identity (an archive's) are told apart in order.
+    for (unsigned Copy = 2; !EmittedTheorems.insert(LeanBodyPrefix).second;
+         ++Copy)
+      LeanBodyPrefix = "cppSpecBody_" +
+                       leanShortHash(Module.FunctionIdentity, 8) + "_" +
+                       std::to_string(Copy) + "_";
+  }
 
   if (EmitPreamble) {
     if (ProjectGoals) {
@@ -988,8 +1033,38 @@ VerifyResult verify::exportLeanScratchPad(
   unsigned Index = 0;
   for (const Obligation &Item : Module.Obligations) {
     ++Index;
-    if (Selection && !Selection->count(Item.Id))
+    const bool Selected = !Selection || Selection->count(Item.Id);
+    if (!Selected && !ProjectGoals)
       continue;
+    std::string ObligationName =
+        TheoremName + "_obligation_" + std::to_string(Index);
+    LeanProjectGoal Goal;
+    if (ProjectGoals) {
+      Goal.Hash = obligationStatementHash(Module, Item);
+      Goal.Name = Group + "_" +
+                  leanIdentifierPart(obligationKindName(Item.Kind)) + "_" +
+                  Goal.Hash.substr(0, 8);
+      // Identical obligations of one function, in source order, whichever
+      // of them are exported.
+      const std::string Base = Goal.Name;
+      for (unsigned Copy = 2; !EmittedTheorems.insert(Goal.Name).second; ++Copy)
+        Goal.Name = Base + "_" + std::to_string(Copy);
+      Goal.Group = Group;
+      Goal.StableId = Item.StableId.empty() ? Item.Id : Item.StableId;
+      if (Item.Source.isValid()) {
+        llvm::raw_string_ostream SourceOS(Goal.Source);
+        printLeanCommentText(Item.Source.File, SourceOS);
+        SourceOS << ":" << Item.Source.Line << ":" << Item.Source.Column;
+      }
+      Goal.BodyPrefix = LeanBodyPrefix;
+      Goal.LegacyName = encodeLeanName(ObligationName + "_goal");
+      Goal.LegacyBodyPrefix = LegacyBodyPrefix;
+      Goal.Exported = Selected;
+      if (!Selected) {
+        ProjectGoals->push_back(std::move(Goal));
+        continue;
+      }
+    }
     OS << "/- obligation: ";
     printLeanCommentText(Item.StableId.empty() ? Item.Id : Item.StableId, OS);
     OS << "\n";
@@ -1004,12 +1079,9 @@ VerifyResult verify::exportLeanScratchPad(
       OS << "unknown";
     }
     OS << " -/\n";
-    std::string ObligationName =
-        TheoremName + "_obligation_" + std::to_string(Index);
     if (ProjectGoals) {
-      ObligationName += "_goal";
-      emitLeanGoalDefinition(ObligationName, Item.Goal.get(), OS);
-      ProjectGoals->push_back(encodeLeanName(ObligationName));
+      emitLeanGoalDefinition(Goal.Name, Item.Goal.get(), OS);
+      ProjectGoals->push_back(std::move(Goal));
     } else {
       emitLeanTheorem(ObligationName, Item.Goal.get(), OS);
     }

clang/lib/Verify/Backend/LeanBackend.h

@@ -11,14 +11,41 @@
 namespace clang {
 namespace verify {
 
-/// Selection names the internal IDs to export; an exported goal keeps the
-/// positional name it has when every obligation is exported.
+/// A goal of an editable Lean project, with what identifies it across
+/// regenerations: the semantic hash of its obligation. Its proof file lives in
+/// the directory of its function's group.
+struct LeanProjectGoal {
+  std::string Name;
+  std::string Group;
+  std::string StableId;
+  std::string Hash;
+  /// Where its obligation is, as a Lean comment may hold it.
+  std::string Source;
+  /// The prefix of the spec bodies its goal may unfold.
+  std::string BodyPrefix;
+  /// The names 0.1 gave the goal and its spec bodies, which a project 0.1
+  /// generated still uses.
+  std::string LegacyName;
+  std::string LegacyBodyPrefix;
+  /// False for an obligation of an exported function that a selection left
+  /// to the solver: its goal is known, but has no definition or proof file.
+  bool Exported = true;
+};
+
+/// The group of a module's goals in a project: its function's directory.
+std::string leanProjectGroup(const ObligationModule &Module);
+
+/// Selection names the internal IDs to export; a project goal is named by
+/// its function and semantic hash, so it keeps its name whatever else is
+/// exported, and a scratch-pad goal keeps the positional name it has when
+/// every obligation is exported. A project records every goal of the module,
+/// the ones left out as not exported.
 VerifyResult
 exportLeanScratchPad(const ObligationModule &Module, llvm::raw_ostream &OS,
                      bool EmitPreamble, std::set<std::string> &EmittedFunctions,
                      std::set<std::string> &EmittedTheorems,
                      unsigned ModuleIndex,
-                     std::vector<std::string> *ProjectGoals,
+                     std::vector<LeanProjectGoal> *ProjectGoals,
                      const std::set<std::string> *Selection = nullptr);
 
 class LeanVerifyBackend : public VerifyBackend {
@@ -27,12 +54,12 @@ class LeanVerifyBackend : public VerifyBackend {
   std::set<std::string> EmittedFunctions;
   std::set<std::string> EmittedTheorems;
   unsigned ModuleIndex = 0;
-  std::vector<std::string> *ProjectGoals;
+  std::vector<LeanProjectGoal> *ProjectGoals;
   std::optional<std::set<std::string>> Selection;
 
 public:
   LeanVerifyBackend(llvm::raw_ostream *OS,
-                    std::vector<std::string> *ProjectGoals)
+                    std::vector<LeanProjectGoal> *ProjectGoals)
       : Out(OS), ProjectGoals(ProjectGoals) {}
   llvm::StringRef getName() const override { return "lean"; }
   BackendCapabilities getCapabilities() const override {

clang/lib/Verify/Backend/ObligationSerialization.cpp

@@ -606,10 +606,12 @@ class ArchiveWriter {
       const ObligationModule &Module, const Obligation &Item,
       bool IncludeBMCTransform = true,
       llvm::StringRef Domain = "cppverify-obligation-semantic",
-      uint32_t Version = ObligationSemanticHashVersion) {
+      uint32_t Version = ObligationSemanticHashVersion,
+      bool IncludeIdentity = true) {
     writeString(Domain);
     writeU32(Version);
-    writeString(Module.FunctionIdentity);
+    if (IncludeIdentity)
+      writeString(Module.FunctionIdentity);
     writeString(Module.ResultVarName);
     writeString(Module.HeapPrefix);
     if (IncludeBMCTransform && Module.BMCTransform) {
@@ -1017,6 +1019,15 @@ std::string verify::obligationSemanticHash(const ObligationModule &Module,
   return sha256(Writer.take());
 }
 
+std::string verify::obligationStatementHash(const ObligationModule &Module,
+                                            const Obligation &Item) {
+  ArchiveWriter Writer(false);
+  Writer.writeObligationSemantics(Module, Item, /*IncludeBMCTransform=*/true,
+                                  "cppverify-obligation-statement", 1,
+                                  /*IncludeIdentity=*/false);
+  return sha256(Writer.take());
+}
+
 std::string verify::obligationQuerySemanticHash(const ObligationModule &Module,
                                                 const Obligation &Item) {
   ArchiveWriter Writer(false);

clang/lib/Verify/Backend/ObligationSerialization.h

@@ -34,6 +34,12 @@ std::string obligationSemanticHash(const ObligationModule &Module);
 std::string obligationSemanticHash(const ObligationModule &Module,
                                    const Obligation &Item);
 
+/// SHA-256 for what a proof of an individual goal proves: its semantics
+/// without the identity of the function it comes from, so that a Lean proof
+/// follows its goal when the function is renamed.
+std::string obligationStatementHash(const ObligationModule &Module,
+                                    const Obligation &Item);
+
 /// SHA-256 for exact dependency-scoped query semantics. Unlike the persistent
 /// proof-cache identity, transformed query contents rather than the enclosing
 /// BMC frontier distinguish bounds, permitting in-process prefix-proof reuse.

clang/lib/Verify/Backend/VerifyBackend.cpp

@@ -749,7 +749,7 @@ std::unique_ptr<VerifyBackend>
 verify::createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut,
                             unsigned BMCUnroll,
                             const BackendExecutionOptions &Execution,
-                            std::vector<std::string> *LeanProjectGoals) {
+                            std::vector<LeanProjectGoal> *LeanProjectGoals) {
   switch (K) {
   case BackendKind::Z3:
     return std::make_unique<Z3VerifyBackend>(Execution, "z3");

clang/lib/Verify/Backend/VerifyBackend.h

@@ -303,11 +303,13 @@ inline unsigned moduleTimeoutMs(const ObligationModule &Module,
                                                 : SolverTimeoutMs;
 }
 
+struct LeanProjectGoal;
+
 std::unique_ptr<VerifyBackend>
 createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut = nullptr,
                     unsigned BMCUnroll = 10,
                     const BackendExecutionOptions &Execution = {},
-                    std::vector<std::string> *LeanProjectGoals = nullptr);
+                    std::vector<LeanProjectGoal> *LeanProjectGoals = nullptr);
 
 VerifyResult
 lowerObligationModule(const ObligationModule &Module,

clang/lib/Verify/Driver/CppVerifyVersion.h

@@ -9,7 +9,12 @@ namespace clang {
 namespace verify {
 
 /// The Lean toolchain every generated Lean project pins.
-inline constexpr llvm::StringLiteral LeanToolchain = "leanprover/lean4:v4.32.2";
+inline constexpr llvm::StringLiteral LeanToolchain = "leanprover/lean4:v4.35.0";
+
+/// The toolchains earlier releases pinned. A project that pins one was
+/// generated by such a release, and is moved to the current pin.
+inline constexpr llvm::StringLiteral EarlierLeanToolchains[] = {
+    "leanprover/lean4:v4.32.2"};
 
 /// The cvc5 release the test suite runs with.
 inline constexpr llvm::StringLiteral CVC5TestedVersion = "1.1.2";