verify: Define spec functions in Lean when Lean proves they terminate

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,47 @@ struct LeanProjectGoal {
 /// 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 +92,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/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,

clang/lib/Verify/Driver/LeanAutomation.h

@@ -9,23 +9,32 @@ namespace verify {
 
 /// Names this module's tactics: a stub or automatic proof that an earlier
 /// revision wrote is tried again.
-inline constexpr llvm::StringLiteral LeanAutomationRevision = "1";
+inline constexpr llvm::StringLiteral LeanAutomationRevision = "3";
 
 /// The steps of cppverify_auto, each the whole proof of a goal it proves.
 inline constexpr llvm::StringLiteral LeanAutomationSteps[] = {
-    "cppverify_auto_grind", "cppverify_auto_heap", "cppverify_auto_bv",
-    "cppverify_auto_decide", "cppverify_auto_simp"};
+    "cppverify_auto_grind",  "cppverify_auto_heap",   "cppverify_auto_bv",
+    "cppverify_auto_decide", "cppverify_auto_simp",   "cppverify_auto_bveq",
+    "cppverify_auto_ext",    "cppverify_auto_unfold", "cppverify_auto_eval",
+    "cppverify_auto_div"};
 
 /// CppVerify/Auto.lean, written with every export. Its steps were chosen by
 /// what proves the goals of the test suite (heap stores as the functions
 /// they define, machine arithmetic as integers, then grind; stating toInt
 /// ranges and removing Int.bmod first proved nothing more, the latter less),
 /// each with a heartbeat budget of its own, as Vermilion's discharger ladder.
+/// Revision 2 adds the last three, after the others, so that every goal an
+/// earlier step proves keeps its proof: machine equalities and sign
+/// extensions as integer facts, collection equality element by element, and
+/// the definition instances a goal states, by the bodies they name.
+/// Revision 3 adds the last two: the spec functions with Lean definitions
+/// evaluated by their equations, and C++ division and remainder by their
+/// definitions.
 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
@@ -82,6 +91,51 @@ elab "cppverify_unfold_readable" : tactic => withMainContext do
       let unfolded ← deltaExpand target (· == name)
       replaceMainGoal [← (← getMainGoal).change unfolded]
 
+open Lean Elab Tactic Meta in
+/-- Unfolds the definitions of spec bodies that a goal and its hypotheses
+name, so that each definition instance a goal states says what the body
+does. A body names only lower levels of its definition, so this ends. -/
+elab "cppverify_unfold_bodies" : tactic => withMainContext do
+  let isBody : Name → Bool := fun
+    | .str _ s => s.startsWith "cppSpecBody_"
+    | _ => false
+  let rec expand (e : Expr) : Nat → MetaM Expr
+    | 0 => return e
+    | fuel + 1 => do
+      let e' ← deltaExpand e isBody
+      if e' == e then return e else expand e' fuel
+  let mut goal ← getMainGoal
+  goal ← goal.change (← expand (← instantiateMVars (← goal.getType)) 64)
+  for d in ← goal.withContext getLCtx do
+    if d.isImplementationDetail then continue
+    let t ← instantiateMVars d.type
+    let t' ← expand t 64
+    if t' != t then
+      goal ← goal.changeLocalDecl d.fvarId t'
+  replaceMainGoal [goal]
+
+open Lean Elab Tactic Meta in
+/-- Rewrites with the equations of every spec function that Specs.lean
+defines, and C++ division and remainder, so that applications at known
+arguments become values. On unknown arguments it unfolds until its budget
+is spent. -/
+elab "cppverify_eval_specs" : tactic => withMainContext do
+  let env ← getEnv
+  let mut lemmas : Array (TSyntax `Lean.Parser.Tactic.simpLemma) := #[]
+  let some idx := env.getModuleIdx? `CppVerify.Specs
+    | throwError "no spec function has a Lean definition"
+  let some data := env.header.moduleData[idx.toNat]?
+    | throwError "no spec function has a Lean definition"
+  for name in data.constNames do
+    if let .str .anonymous s := name then
+      if s.startsWith "cppSpec_" then
+        if let some (.defnInfo _) := env.find? name then
+          lemmas := lemmas.push
+            (← `(Lean.Parser.Tactic.simpLemma| $(mkIdent name):ident))
+  if lemmas.isEmpty then
+    throwError "no spec function has a Lean definition"
+  evalTactic (← `(tactic| simp [$lemmas,*, cppIntDiv, cppIntRem]))
+
 /-- Machine comparisons, constants, and overflow conditions as facts about
 integers. -/
 macro "cppverify_norm" : tactic => `(tactic| (try simp only [cppBvSlt, cppBvSle,
@@ -118,6 +172,47 @@ macro "cppverify_auto_decide" : tactic =>
 macro "cppverify_auto_simp" : tactic =>
   `(tactic| (cppverify_unfold_readable; simp_all))
 
+/-- Machine equalities, as of `x ≠ y` for distinct keys, and sign extensions
+as facts about integers. -/
+macro "cppverify_bveq" : tactic => `(tactic| (try simp (disch := omega) only
+  [ne_eq, ← BitVec.toInt_inj, BitVec.toInt_signExtend_of_le] at *))
+macro "cppverify_auto_bveq" : tactic => `(tactic| (
+    cppverify_unfold_readable
+    intros
+    cppverify_bveq
+    cppverify_norm
+    all_goals grind))
+/-- Two collections are equal when they agree at every element: equal
+lengths and reads for sequences, membership for sets, counts for
+multisets, and keys and values for maps. -/
+macro "cppverify_auto_ext" : tactic => `(tactic| (
+    cppverify_unfold_readable
+    intros
+    (first | apply cppSeq_ext | apply cppSet_ext | apply cppMultiset_ext
+           | apply cppMap_ext)
+    all_goals (intros; cppverify_norm; all_goals grind)))
+macro "cppverify_auto_unfold" : tactic => `(tactic| (
+    cppverify_unfold_readable
+    intros
+    cppverify_unfold_bodies
+    cppverify_bveq
+    cppverify_norm
+    all_goals grind))
+macro "cppverify_auto_eval" : tactic => `(tactic| (
+    cppverify_unfold_readable
+    intros
+    cppverify_bveq
+    cppverify_eval_specs
+    all_goals grind))
+/-- C++ division and remainder by their definitions, which grind reads by
+constant divisors once the signs are split. -/
+macro "cppverify_auto_div" : tactic => `(tactic| (
+    cppverify_unfold_readable
+    intros
+    cppverify_bveq
+    cppverify_norm
+    all_goals grind [cppIntDiv, cppIntRem]))
+
 open Lean Elab Tactic in
 /-- Tries each step on the goal, each with `cppverify.autoBudget` heartbeats
 of its own, and keeps the first that proves it. A step that runs out of
@@ -132,7 +227,12 @@ elab "cppverify_auto" : tactic => do
     ("cppverify_auto_heap", ← `(tactic| cppverify_auto_heap)),
     ("cppverify_auto_bv", ← `(tactic| cppverify_auto_bv)),
     ("cppverify_auto_decide", ← `(tactic| cppverify_auto_decide)),
-    ("cppverify_auto_simp", ← `(tactic| cppverify_auto_simp))]
+    ("cppverify_auto_simp", ← `(tactic| cppverify_auto_simp)),
+    ("cppverify_auto_bveq", ← `(tactic| cppverify_auto_bveq)),
+    ("cppverify_auto_ext", ← `(tactic| cppverify_auto_ext)),
+    ("cppverify_auto_unfold", ← `(tactic| cppverify_auto_unfold)),
+    ("cppverify_auto_eval", ← `(tactic| cppverify_auto_eval)),
+    ("cppverify_auto_div", ← `(tactic| cppverify_auto_div))]
   for (name, step) in steps do
     let attempt : TacticM Unit := do
       let heartbeats ← IO.getNumHeartbeats