verify: Replay obligation archives into Lean projects, bounded modules included

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 {
@@ -33,26 +35,55 @@ struct LeanProjectGoal {
   /// 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;
+  /// An unwinding goal of a bounded module: that its loops end within the
+  /// bound.
+  bool Unwinding = false;
 };
 
 /// The group of a module's goals in a project: its function's directory.
 std::string leanProjectGroup(const ObligationModule &Module);
 
+/// A logical function of a Lean project: its opaque declaration and, when it
+/// has a definition Lean may accept, that definition, recursion measured by
+/// its termination measures, with the functions it applies.
+struct LeanSpecDeclaration {
+  /// Its Lean constant.
+  std::string Name;
+  std::string Opaque;
+  std::string Definition;
+  std::set<std::string> Applies;
+};
+
+/// The generated modules of a Lean project: the specs its goals apply, by
+/// identity, which every goal module imports, and each group's spec
+/// definitions and goals.
+struct LeanProjectModules {
+  std::map<std::string, LeanSpecDeclaration> 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.
-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);
+/// the ones left out as not exported. Specs, when given, receives each spec
+/// once, as its project declares it, instead of OS.
+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,
+    std::map<std::string, LeanSpecDeclaration> *Specs = 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,12 +95,13 @@ 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.
-    return {allLogicFeatures() & ~logicFeature(LogicFeature::Sequences) &
-                ~logicFeature(LogicFeature::Collections),
-            false};
+    return {allLogicFeatures(), false};
   }
   /// Restrict later exports to these internal obligation IDs.
   void selectObligations(std::optional<std::set<std::string>> Ids) {

clang/lib/Verify/Backend/Obligation.cpp

@@ -2578,6 +2578,26 @@ verify::validateObligationModule(const ObligationModule &M) {
                                        ValidationError.c_str());
       collectRequiredFeatures(Definition.get(), RequiredFeatures);
     }
+    // A measure only chooses an induction or Lean's termination argument,
+    // so it adds no feature; it must still be an integer over the
+    // parameters.
+    for (const auto &Measure : Declaration.Decreases) {
+      if (!validateLogicExpr(Measure.get(), ValidationError))
+        return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s",
+                                       ValidationError.c_str());
+      if (Measure->Sort.Kind != LogicSortKind::MathematicalInteger &&
+          Measure->Sort.Kind != LogicSortKind::BitVector)
+        return llvm::createStringError(
+            llvm::inconvertibleErrorCode(),
+            "logical function termination measure is not an integer");
+      if (!validateLogicCalls(Measure.get(), M.LogicFunctions,
+                              ValidationError) ||
+          !validateVariableScopes(Measure.get(), ValidationError) ||
+          !validateDefinitionVariables(Measure.get(), Parameters, {},
+                                       ValidationError))
+        return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s",
+                                       ValidationError.c_str());
+    }
   }
   return RequiredFeatures;
 }

clang/lib/Verify/Backend/Obligation.h

@@ -230,7 +230,8 @@ class LogicExpr : public llvm::ThreadSafeRefCountedBase<LogicExpr> {
   std::vector<LogicExprRef> Patterns;
   /// For an Or that states one assumption of a goal (`!A || rest`): where A
   /// comes from (`pre`, `call:f`, `def:x_1`), so a goal can be shown as
-  /// named hypotheses. Outside the term's meaning, identity, and archives.
+  /// named hypotheses. Outside the term's meaning and identity; archives
+  /// keep it with their source metadata.
   std::string Premise;
 
   explicit LogicExpr(Kind K) : K(K) {}
@@ -355,7 +356,8 @@ struct LogicFunctionDecl {
   /// value; a verdict that does rests on them. Not archived.
   std::vector<std::unique_ptr<LogicExpr>> Postconditions;
   /// A recursive function's termination measure over the parameters, by
-  /// which an induction over its applications descends. Not archived.
+  /// which an induction over its applications descends and Lean proves its
+  /// definition terminates. Archived, never hashed.
   std::vector<std::unique_ptr<LogicExpr>> Decreases;
   static constexpr const char *ResultVariable = "cppverify.result";
 };

clang/lib/Verify/Backend/ObligationSerialization.cpp

@@ -501,17 +501,24 @@ class ArchiveWriter {
       writeU8(collectionTag(Expr->CollectionOp));
     writeString(Expr->SpecCallee);
     writeSource(Expr->Source);
+    // Where an assumption comes from names its hypothesis in a readable
+    // Lean goal, as source points name a diagnostic's place.
+    if (IncludeSource && Expr->K == LogicExpr::Or)
+      writeString(Expr->Premise);
     writeU64(Expr->Children.size());
     for (const auto &Child : Expr->Children)
       writeExpr(Child.get());
   }
 
+  // A record keeps what a hash leaves out: the display name, and the
+  // termination measures, which change no meaning (Lean checks termination
+  // itself, and an induction descends by a well-founded relation whatever
+  // the measure).
   void writeFunction(const std::string &MapIdentity,
-                     const LogicFunctionDecl &Function,
-                     bool IncludeDisplayName) {
+                     const LogicFunctionDecl &Function, bool Archived) {
     writeString(MapIdentity);
     writeString(Function.Identity);
-    writeString(IncludeDisplayName ? Function.DisplayName : "");
+    writeString(Archived ? Function.DisplayName : "");
     writeU64(Function.Parameters.size());
     for (const LogicFunctionParameter &Parameter : Function.Parameters) {
       writeString(Parameter.Name);
@@ -523,6 +530,11 @@ class ArchiveWriter {
     writeU64(Function.DefinitionLevels.size());
     for (const auto &Definition : Function.DefinitionLevels)
       writeExpr(Definition.get());
+    if (!Archived)
+      return;
+    writeU64(Function.Decreases.size());
+    for (const auto &Measure : Function.Decreases)
+      writeExpr(Measure.get());
   }
 
   void writeFunctionSignature(const std::string &MapIdentity,
@@ -536,10 +548,10 @@ class ArchiveWriter {
   }
 
   void writeFunctions(const std::map<std::string, LogicFunctionDecl> &Functions,
-                      bool IncludeDisplayNames) {
+                      bool Archived) {
     writeU64(Functions.size());
     for (const auto &[Identity, Function] : Functions)
-      writeFunction(Identity, Function, IncludeDisplayNames);
+      writeFunction(Identity, Function, Archived);
   }
 
   void writeModule(const ObligationModule &Module,
@@ -804,6 +816,8 @@ class ArchiveReader {
     }
     Expr->SpecCallee = readString();
     Expr->Source = readSource(IncludeSource);
+    if (Version >= 3 && IncludeSource && Expr->K == LogicExpr::Or)
+      Expr->Premise = readString();
 
     uint64_t Children = readCount();
     if (!Failure.empty())
@@ -839,6 +853,12 @@ class ArchiveReader {
     Function.DefinitionLevels.reserve(Levels);
     for (uint64_t I = 0; I != Levels && Failure.empty(); ++I)
       Function.DefinitionLevels.push_back(readExpr());
+    if (Version >= 3) {
+      uint64_t Measures = readCount();
+      Function.Decreases.reserve(Measures);
+      for (uint64_t I = 0; I != Measures && Failure.empty(); ++I)
+        Function.Decreases.push_back(readExpr());
+    }
     return Function;
   }
 

clang/lib/Verify/Backend/ObligationSerialization.h

@@ -12,7 +12,10 @@
 namespace clang {
 namespace verify {
 
-inline constexpr uint32_t ObligationSerializationVersion = 2;
+/// Version 2 adds the precise obligation kinds; version 3 each logical
+/// function's termination measures and, with source metadata, where each
+/// assumption of a goal comes from. Readers read every earlier version.
+inline constexpr uint32_t ObligationSerializationVersion = 3;
 inline constexpr uint32_t ObligationSemanticHashVersion = 4;
 
 /// Serialize one module as a deterministic, versioned binary record. Records

clang/lib/Verify/Backend/ObligationSimplify.cpp

@@ -363,10 +363,14 @@ void simplifyFunctions(ObligationModule &Module,
     auto Function = Module.LogicFunctions.find(Pending[I]);
     if (Function == Module.LogicFunctions.end())
       continue;
+    // A function's declaration depends on what its definition and its
+    // measures apply.
     std::set<std::string> Dependencies;
     collectCalledFunctions(Function->second.StepDefinition.get(), Dependencies);
     for (const auto &Definition : Function->second.DefinitionLevels)
       collectCalledFunctions(Definition.get(), Dependencies);
+    for (const auto &Measure : Function->second.Decreases)
+      collectCalledFunctions(Measure.get(), Dependencies);
     for (const std::string &Dependency : Dependencies)
       if (Reachable.insert(Dependency).second)
         Pending.push_back(Dependency);

clang/lib/Verify/Backend/VerifyBackend.cpp

@@ -15,17 +15,31 @@ 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]);
+    Result = exportLeanScratchPad(
+        Module, Goals, /*EmitPreamble=*/false, EmittedFunctions,
+        EmittedTheorems, ++ModuleIndex, ProjectGoals,
+        Selection ? &*Selection : nullptr, &Modules->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 +768,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,