verify: Give each function of a Lean project its own goal module, and build only the proofs that changed

clang/lib/Verify/Backend/LeanBackend.cpp

@@ -1087,12 +1087,63 @@ static void emitLeanFunctionBodies(const ObligationModule &Module,
   }
 }
 
+// The definitions every exported goal is stated with: the heap model, the
+// machine comparisons, and C++ division; a project's goals also have the
+// lemmas their readable forms' bridges use.
+void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) {
+  OS << "noncomputable section\n\n";
+  OS << "set_option maxRecDepth 100000\n";
+  OS << "set_option maxHeartbeats 0\n\n";
+  OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n";
+  OS << "  Classical.propDecidable p\n\n";
+  OS << "abbrev CppHeap := Int -> Int\n\n";
+  OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n";
+  OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n";
+  OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n";
+  OS << "  BitVec.ofInt w (h p)\n\n";
+  OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : "
+        "Prop :=\n";
+  OS << "  h' = fun q => if q = p then v else h q\n";
+  OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n";
+  OS << "    (h' : CppHeap) : Prop :=\n";
+  OS << "  h' = fun q => if q = p then\n";
+  OS << "    @ite Int v (Classical.propDecidable v) 1 0 else h q\n";
+  OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n";
+  OS << "    (h' : CppHeap) : Prop :=\n";
+  OS << "  h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n";
+  OS << "opaque validPtr : Int -> Prop\n\n";
+  // Reducible, so instance search sees the Bool comparison and decides it.
+  OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = "
+        "true\n";
+  OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = "
+        "true\n";
+  OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = "
+        "true\n";
+  OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = "
+        "true\n\n";
+  OS << "def cppIntDiv (x y : Int) : Int :=\n";
+  OS << "  if y = 0 then 0 else\n";
+  OS << "    let q := (if x < 0 then -x else x) / "
+        "(if y < 0 then -y else y)\n";
+  OS << "    if (x < 0) ≠ (y < 0) then -q else q\n";
+  OS << "def cppIntRem (x y : Int) : Int :=\n";
+  OS << "  if y = 0 then x else x - cppIntDiv x y * y\n\n";
+  if (Project) {
+    // What the bridges from readable goals use.
+    OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n";
+    OS << "  (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n";
+    OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b "
+          ":=\n";
+    OS << "  (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n";
+  }
+}
+
 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<LeanProjectGoal> *ProjectGoals,
-    const std::set<std::string> *Selection) {
+    const std::set<std::string> *Selection, llvm::raw_ostream *Declarations) {
   VerifyResult Result;
   if (!Module.CorrectnessGoal || !Module.CounterexampleQuery) {
     Result.Status = VerifyStatus::Unresolved;
@@ -1130,54 +1181,11 @@ VerifyResult verify::exportLeanScratchPad(
       OS << "   This file exports canonical obligations but does not certify "
             "them. -/\n\n";
     }
-    OS << "noncomputable section\n\n";
-    OS << "set_option maxRecDepth 100000\n";
-    OS << "set_option maxHeartbeats 0\n\n";
-    OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n";
-    OS << "  Classical.propDecidable p\n\n";
-    OS << "abbrev CppHeap := Int -> Int\n\n";
-    OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n";
-    OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n";
-    OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n";
-    OS << "  BitVec.ofInt w (h p)\n\n";
-    OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : "
-          "Prop :=\n";
-    OS << "  h' = fun q => if q = p then v else h q\n";
-    OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n";
-    OS << "    (h' : CppHeap) : Prop :=\n";
-    OS << "  h' = fun q => if q = p then\n";
-    OS << "    @ite Int v (Classical.propDecidable v) 1 0 else h q\n";
-    OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n";
-    OS << "    (h' : CppHeap) : Prop :=\n";
-    OS << "  h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n";
-    OS << "opaque validPtr : Int -> Prop\n\n";
-    // Reducible, so instance search sees the Bool comparison and decides it.
-    OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = "
-          "true\n";
-    OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = "
-          "true\n";
-    OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = "
-          "true\n";
-    OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = "
-          "true\n\n";
-    OS << "def cppIntDiv (x y : Int) : Int :=\n";
-    OS << "  if y = 0 then 0 else\n";
-    OS << "    let q := (if x < 0 then -x else x) / "
-          "(if y < 0 then -y else y)\n";
-    OS << "    if (x < 0) ≠ (y < 0) then -q else q\n";
-    OS << "def cppIntRem (x y : Int) : Int :=\n";
-    OS << "  if y = 0 then x else x - cppIntDiv x y * y\n\n";
-    if (ProjectGoals) {
-      // What the bridges from readable goals use.
-      OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n";
-      OS << "  (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n";
-      OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b "
-            ":=\n";
-      OS << "  (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n";
-    }
+    emitLeanPrelude(OS, ProjectGoals != nullptr);
   }
 
-  emitLeanFunctionDeclarations(Module, OS, EmittedFunctions);
+  emitLeanFunctionDeclarations(Module, Declarations ? *Declarations : OS,
+                               EmittedFunctions);
   emitLeanFunctionBodies(Module, OS);
   OS << "/- function: ";
   printLeanCommentText(Module.FunctionName, OS);

clang/lib/Verify/Backend/LeanBackend.h

@@ -4,8 +4,10 @@
 
 #include "VerifyBackend.h"
 #include "llvm/Support/raw_ostream.h"
+#include <map>
 #include <optional>
 #include <set>
+#include <string>
 #include <vector>
 
 namespace clang {
@@ -38,21 +40,37 @@ struct LeanProjectGoal {
 /// The group of a module's goals in a project: its function's directory.
 std::string leanProjectGroup(const ObligationModule &Module);
 
+/// The generated modules of a Lean project: the declarations of the specs
+/// its goals apply, which every goal module imports, and each group's spec
+/// definitions and goals.
+struct LeanProjectModules {
+  std::string Specs;
+  std::map<std::string, std::string> Goals;
+  /// The groups in the order their functions were exported: the source's.
+  std::vector<std::string> Order;
+};
+
+/// The definitions every exported goal is stated with.
+void emitLeanPrelude(llvm::raw_ostream &OS, bool Project);
+
 /// 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.
+/// the ones left out as not exported. Declarations, when given, receives
+/// the declarations of the specs, each once.
 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<LeanProjectGoal> *ProjectGoals,
-                     const std::set<std::string> *Selection = nullptr);
+                     const std::set<std::string> *Selection = nullptr,
+                     llvm::raw_ostream *Declarations = nullptr);
 
 class LeanVerifyBackend : public VerifyBackend {
-  llvm::raw_ostream *Out;
+  llvm::raw_ostream *Out = nullptr;
+  LeanProjectModules *Modules = nullptr;
   bool PreambleEmitted = false;
   std::set<std::string> EmittedFunctions;
   std::set<std::string> EmittedTheorems;
@@ -64,6 +82,10 @@ class LeanVerifyBackend : public VerifyBackend {
   LeanVerifyBackend(llvm::raw_ostream *OS,
                     std::vector<LeanProjectGoal> *ProjectGoals)
       : Out(OS), ProjectGoals(ProjectGoals) {}
+  /// A project's export, into its modules.
+  LeanVerifyBackend(LeanProjectModules *Modules,
+                    std::vector<LeanProjectGoal> *ProjectGoals)
+      : Modules(Modules), ProjectGoals(ProjectGoals) {}
   llvm::StringRef getName() const override { return "lean"; }
   BackendCapabilities getCapabilities() const override {
     // Collections have no Lean semantics yet.

clang/lib/Verify/Backend/VerifyBackend.cpp

@@ -15,17 +15,32 @@ using namespace verify;
 
 VerifyResult LeanVerifyBackend::verifyModule(const ObligationModule &Module) {
   VerifyResult R;
-  if (!Out) {
+  if (!Out && !Modules) {
     R.Status = VerifyStatus::Unresolved;
     R.Reason = VerifyReason::LeanExportFailure;
     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;
+  VerifyResult Result;
+  if (Modules) {
+    // A project's goals go to their function's module, and the specs they
+    // apply are declared once, in the module every goal module imports.
+    const std::string Group = leanProjectGroup(Module);
+    if (!Modules->Goals.count(Group))
+      Modules->Order.push_back(Group);
+    llvm::raw_string_ostream Goals(Modules->Goals[Group]);
+    llvm::raw_string_ostream Specs(Modules->Specs);
+    Result = exportLeanScratchPad(Module, Goals, /*EmitPreamble=*/false,
+                                  EmittedFunctions, EmittedTheorems,
+                                  ++ModuleIndex, ProjectGoals,
+                                  Selection ? &*Selection : nullptr, &Specs);
+  } else {
+    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)
@@ -754,11 +769,14 @@ std::unique_ptr<VerifyBackend>
 verify::createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut,
                             unsigned BMCUnroll,
                             const BackendExecutionOptions &Execution,
-                            std::vector<LeanProjectGoal> *LeanProjectGoals) {
+                            std::vector<LeanProjectGoal> *LeanProjectGoals,
+                            LeanProjectModules *LeanModules) {
   switch (K) {
   case BackendKind::Z3:
     return std::make_unique<Z3VerifyBackend>(Execution, "z3");
   case BackendKind::Lean:
+    if (LeanModules)
+      return std::make_unique<LeanVerifyBackend>(LeanModules, LeanProjectGoals);
     return std::make_unique<LeanVerifyBackend>(LeanOut, LeanProjectGoals);
   case BackendKind::BMC:
     return std::make_unique<BMCVerifyBackend>(BMCUnroll, Execution);

clang/lib/Verify/Backend/VerifyBackend.h

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

clang/lib/Verify/Driver/LeanAutomation.h

@@ -25,7 +25,7 @@ inline constexpr llvm::StringLiteral LeanAutomationSource =
     R"lean(/- Generated by CppVerify: the tactics of its automatic proofs, which proof
    files may use too. Regeneration replaces this file. -/
 import Lean
-import CppVerify.Generated
+import CppVerify.Prelude
 
 register_option cppverify.autoBudget : Nat := {
   defValue := 50000