diff --git a/.github/workflows/cppverify-ci.yml b/.github/workflows/cppverify-ci.yml index f95b95a2b6..6700656e1b 100644 --- a/.github/workflows/cppverify-ci.yml +++ b/.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: diff --git a/README.md b/README.md index 3091331a30..7b4cb781a3 100644 --- a/README.md +++ b/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. diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp index 5973b55492..f594870e97 100644 --- a/clang/lib/Verify/Backend/LeanBackend.cpp +++ b/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 #include @@ -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(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); } @@ -740,8 +769,9 @@ static void collectLeanSpecCalls(const LogicExpr *Expression, // A definition holds at every argument, so the instance at an application // under quantifiers is stated for every value of their binders. -static unsigned emitLeanSpecAxiomBinders(const LogicExpr *Goal, - llvm::raw_ostream &OS) { +static unsigned +emitLeanSpecAxiomBinders(const LogicExpr *Goal, llvm::raw_ostream &OS, + std::vector *Names = nullptr) { std::vector Binders; std::vector Calls; collectLeanSpecCalls(Goal, Binders, Calls); @@ -756,8 +786,12 @@ static unsigned emitLeanSpecAxiomBinders(const LogicExpr *Goal, ++CallIndex; for (unsigned Level = 0; Level < Function->DefinitionFuel; ++Level) { ++BinderCount; - OS << "\n (cppverify_spec_axiom_" << CallIndex << "_" << Level + 1 - << " : "; + const std::string Axiom = "cppverify_spec_axiom_" + + std::to_string(CallIndex) + "_" + + std::to_string(Level + 1); + if (Names) + Names->push_back(Axiom); + OS << "\n (" << Axiom << " : "; if (!Around.empty()) { OS << "∀"; for (const std::string &Binder : Around) { @@ -812,8 +846,162 @@ static void emitLeanTheorem(llvm::StringRef Name, const LogicExpr *Goal, OS << " := by\n sorry\n\n"; } +// A hypothesis of a readable goal: an Or that makeGoal joined to the goal, +// whose left operand negates the assumption. +static const LogicExpr *leanHypothesis(const LogicExpr &Premise) { + const LogicExpr *Left = Premise.Children[0].get(); + return Left->K == LogicExpr::Not && Left->Children.size() == 1 + ? Left->Children[0].get() + : Left; +} + +// Named by where the assumption comes from; a definition by what it defines. +static std::string leanHypothesisName(const LogicExpr &Premise, + std::map &Counts, + std::set &Used) { + auto [Category, Detail] = llvm::StringRef(Premise.Premise).split(':'); + std::string Base = "h_" + leanIdentifierPart(Category); + if (!Detail.empty()) + Base += "_" + leanIdentifierPart(Detail); + bool Numbered = true; + if (llvm::is_contained({"def", "ret", "branch", "loop", "exit", "fact"}, + Category)) { + const LogicExpr *Fact = leanHypothesis(Premise); + if (Fact != Premise.Children[0].get()) + while (Fact->K == LogicExpr::Or && Fact->Children.size() == 2 && + Fact->Children[0]->K == LogicExpr::Not) + Fact = Fact->Children[1].get(); + if (Fact->K == LogicExpr::Eq && Fact->Children.size() == 2 && + Fact->Children[0]->K == LogicExpr::Var) { + Base = "h_" + llvm::StringRef(leanIdentifierPart(Fact->Children[0]->Name)) + .ltrim('_') + .str(); + Numbered = false; + } + } + std::string Name = + Numbered ? Base + "_" + std::to_string(++Counts[Base]) : Base; + while (!Used.insert(Name).second) + Name = Base + "_" + std::to_string(++Counts[Base]); + return Name; +} + +// The goal as named hypotheses and what remains to be shown, and a proof that +// it implies the goal: the bridge the kernel checks, so a proof of this form +// proves the goal whatever this printer did. Intros receives the names a +// proof of it introduces. +static void emitLeanReadableGoal(llvm::StringRef Name, const LogicExpr *Goal, + const std::map &Vars, + bool HasSpecAxioms, std::string &Intros, + llvm::raw_ostream &OS) { + LeanEmitBudget = 500000; + std::vector Premises; + const LogicExpr *Rest = Goal; + while (Rest && Rest->K == LogicExpr::Or && !Rest->Premise.empty() && + Rest->Children.size() == 2) { + Premises.push_back(Rest); + Rest = Rest->Children[1].get(); + } + + std::vector Binders; + for (const auto &[Variable, Sort] : Vars) + Binders.push_back(encodeLeanName(Variable)); + std::string AxiomText; + llvm::raw_string_ostream AxiomOS(AxiomText); + std::vector Axioms; + emitLeanSpecAxiomBinders(Goal, AxiomOS, &Axioms); + Binders.insert(Binders.end(), Axioms.begin(), Axioms.end()); + + LeanTemporaryNames.clear(); + LeanTemporaryRoot = nullptr; + std::vector Temporaries; + for (const LogicExpr *Premise : Premises) + collectLeanTemporaries(Premise->Children[0].get(), Temporaries, true); + collectLeanTemporaries(Rest, Temporaries, true); + std::vector Lets; + for (const LogicExpr *Node : Temporaries) { + LeanTemporaryNames.emplace(Node, Lets.size() + 1); + Lets.push_back("__cppverify_term_" + std::to_string(Lets.size() + 1)); + } + + std::set Used(Binders.begin(), Binders.end()); + Used.insert(Lets.begin(), Lets.end()); + std::map Counts; + std::vector Hypotheses; + for (const LogicExpr *Premise : Premises) + Hypotheses.push_back(leanHypothesisName(*Premise, Counts, Used)); + + OS << "def "; + printLeanName(Name.str(), OS); + OS << ".readable"; + OS << " : Prop :=\n "; + if (!Vars.empty() || HasSpecAxioms) { + OS << "∀"; + emitLeanVariableBinders(Vars, OS); + OS << AxiomText << ",\n "; + } + if (!Lets.empty()) + OS << "("; + for (const LogicExpr *Node : Temporaries) { + OS << "let __cppverify_term_" << LeanTemporaryNames.at(Node) << " : "; + printLeanSort(Node->Sort, OS); + OS << " := "; + LeanTemporaryRoot = Node; + printVCExprLean(Node, OS, LeanTop); + OS << ";\n "; + } + LeanTemporaryRoot = nullptr; + for (size_t I = 0; I != Premises.size(); ++I) { + const LogicExpr *Left = Premises[I]->Children[0].get(); + OS << "(" << Hypotheses[I] << " : "; + if (leanHypothesis(*Premises[I]) != Left) { + printVCExprLean(leanHypothesis(*Premises[I]), OS, LeanTop); + } else { + OS << "¬"; + printVCExprLean(Left, OS, LeanArgument); + } + OS << ") →\n "; + } + printVCExprLean(Rest, OS, Premises.empty() ? LeanTop : LeanArrow); + if (!Lets.empty()) + OS << ")"; + OS << "\n\n"; + LeanTemporaryNames.clear(); + + OS << "theorem "; + printLeanName(Name.str(), OS); + OS << ".of_readable (h : "; + printLeanName(Name.str(), OS); + OS << ".readable) : "; + printLeanName(Name.str(), OS); + OS << " :=\n "; + if (!Binders.empty()) { + OS << "fun"; + for (const std::string &Binder : Binders) + OS << " " << Binder; + OS << " =>\n "; + } + for (size_t I = 0; I != Premises.size(); ++I) + OS << (leanHypothesis(*Premises[I]) != Premises[I]->Children[0].get() + ? "cppverify_imp_or fun " + : "cppverify_not_imp_or fun ") + << Hypotheses[I] << " =>\n "; + OS << "h"; + for (const std::string &Binder : Binders) + OS << " " << Binder; + for (const std::string &Hypothesis : Hypotheses) + OS << " " << Hypothesis; + OS << "\n\n"; + + Intros.clear(); + for (const auto *Part : {&Binders, &Lets, &Hypotheses}) + for (const std::string &Introduced : *Part) + Intros += (Intros.empty() ? "" : " ") + Introduced; +} + static void emitLeanGoalDefinition(llvm::StringRef Name, const LogicExpr *Goal, - llvm::raw_ostream &OS) { + llvm::raw_ostream &OS, + std::string *Intros = nullptr) { LeanEmitBudget = 500000; std::map Variables; collectLeanVariables(Goal, {}, Variables); @@ -839,6 +1027,8 @@ static void emitLeanGoalDefinition(llvm::StringRef Name, const LogicExpr *Goal, } printLeanFlattened(Goal, OS); OS << "\n\n"; + if (Intros) + emitLeanReadableGoal(Name, Goal, Variables, HasSpecAxioms, *Intros, OS); } static void @@ -899,7 +1089,7 @@ VerifyResult verify::exportLeanScratchPad( const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, std::set &EmittedFunctions, std::set &EmittedTheorems, unsigned ModuleIndex, - std::vector *ProjectGoals, + std::vector *ProjectGoals, const std::set *Selection) { VerifyResult Result; if (!Module.CorrectnessGoal || !Module.CounterexampleQuery) { @@ -911,7 +1101,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) { @@ -959,6 +1165,14 @@ VerifyResult verify::exportLeanScratchPad( 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"; + } } emitLeanFunctionDeclarations(Module, OS, EmittedFunctions); @@ -988,8 +1202,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 +1248,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, &Goal.Intros); + ProjectGoals->push_back(std::move(Goal)); } else { emitLeanTheorem(ObligationName, Item.Goal.get(), OS); } diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h index 815cdeadd6..7145e8596c 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -11,14 +11,44 @@ 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; + /// What a proof of its readable form introduces, in order: the goal's + /// variables, definitions, and named hypotheses. + std::string Intros; + /// 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 &EmittedFunctions, std::set &EmittedTheorems, unsigned ModuleIndex, - std::vector *ProjectGoals, + std::vector *ProjectGoals, const std::set *Selection = nullptr); class LeanVerifyBackend : public VerifyBackend { @@ -27,12 +57,12 @@ class LeanVerifyBackend : public VerifyBackend { std::set EmittedFunctions; std::set EmittedTheorems; unsigned ModuleIndex = 0; - std::vector *ProjectGoals; + std::vector *ProjectGoals; std::optional> Selection; public: LeanVerifyBackend(llvm::raw_ostream *OS, - std::vector *ProjectGoals) + std::vector *ProjectGoals) : Out(OS), ProjectGoals(ProjectGoals) {} llvm::StringRef getName() const override { return "lean"; } BackendCapabilities getCapabilities() const override { diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp index 6bebcbc018..0e602c1eba 100644 --- a/clang/lib/Verify/Backend/Obligation.cpp +++ b/clang/lib/Verify/Backend/Obligation.cpp @@ -416,6 +416,7 @@ static std::unique_ptr cloneVCExpr(const VCExpr *E) { Copy->OverflowOp = E->OverflowOp; Copy->CollectionOp = E->CollectionOp; Copy->SpecCallee = E->SpecCallee; + Copy->Premise = E->Premise; for (const auto &Child : E->Children) Copy->Children.push_back(cloneVCExpr(Child.get())); for (const auto &Pattern : E->Patterns) @@ -2230,6 +2231,7 @@ class ObligationBuilder { std::unique_ptr Cond; std::string Note; bool Theorem; + std::string Origin; }; std::vector Stmts; for (const auto &Stmt : P.Stmts) { @@ -2239,7 +2241,7 @@ class ObligationBuilder { } Stmts.push_back({Stmt->K, obligationKind(Stmt->ProofKind), Stmt->TraceEventCount, fromVExpr(Stmt->Cond.get()), - Stmt->Note, Stmt->Theorem}); + Stmt->Note, Stmt->Theorem, Stmt->Origin}); } std::vector< @@ -2272,16 +2274,23 @@ class ObligationBuilder { return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ConstructionError.c_str()); - std::vector Assumptions; - for (const auto &Entry : EntryAssumes) - Assumptions.push_back(Entry.get()); + // Each assumption with where it comes from, which names its hypothesis. + std::vector> Assumptions; + for (size_t I = 0; I != EntryAssumes.size(); ++I) + Assumptions.emplace_back(EntryAssumes[I].get(), I < P.EntryOrigins.size() + ? P.EntryOrigins[I] + : "entry"); for (size_t I = 0; I < P.PreconditionCount && I < EntryAssumes.size(); ++I) M.Preconditions.push_back(cloneVCExpr(EntryAssumes[I].get())); auto makeGoal = [&](const VCExpr *Condition) -> std::unique_ptr { std::unique_ptr ConditionWP = cloneVCExpr(Condition); - for (auto It = Assumptions.rbegin(); It != Assumptions.rend(); ++It) - ConditionWP = vcOr(vcNot(cloneVCExpr(*It)), std::move(ConditionWP)); + for (auto It = Assumptions.rbegin(); It != Assumptions.rend(); ++It) { + ConditionWP = + vcOr(vcNot(cloneVCExpr(It->first)), std::move(ConditionWP)); + if (ConditionWP->K == VCExpr::Or) + ConditionWP->Premise = It->second.empty() ? "fact" : It->second; + } ConditionWP->Loc = Condition->Loc; ConditionWP->EndLoc = Condition->EndLoc; return ConditionWP; @@ -2311,7 +2320,7 @@ class ObligationBuilder { for (const LoweredStmt &Stmt : Stmts) { if (Stmt.Kind == PassiveStmt::Assume) { - Assumptions.push_back(Stmt.Cond.get()); + Assumptions.emplace_back(Stmt.Cond.get(), Stmt.Origin); if (Stmt.Theorem) M.Theorems.push_back(cloneVCExpr(Stmt.Cond.get())); continue; diff --git a/clang/lib/Verify/Backend/Obligation.h b/clang/lib/Verify/Backend/Obligation.h index ba16118533..e7d74d813f 100644 --- a/clang/lib/Verify/Backend/Obligation.h +++ b/clang/lib/Verify/Backend/Obligation.h @@ -216,6 +216,10 @@ class LogicExpr { /// quantifier, a solver hint outside the term's meaning, its identity, and /// archives. std::vector> 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. + std::string Premise; explicit LogicExpr(Kind K) : K(K) {} }; diff --git a/clang/lib/Verify/Backend/ObligationSerialization.cpp b/clang/lib/Verify/Backend/ObligationSerialization.cpp index f9a12c4b95..547b55818f 100644 --- a/clang/lib/Verify/Backend/ObligationSerialization.cpp +++ b/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); diff --git a/clang/lib/Verify/Backend/ObligationSerialization.h b/clang/lib/Verify/Backend/ObligationSerialization.h index 0c8674bdca..3eb10da883 100644 --- a/clang/lib/Verify/Backend/ObligationSerialization.h +++ b/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. diff --git a/clang/lib/Verify/Backend/ObligationSimplify.cpp b/clang/lib/Verify/Backend/ObligationSimplify.cpp index 48eca39d48..27875e481e 100644 --- a/clang/lib/Verify/Backend/ObligationSimplify.cpp +++ b/clang/lib/Verify/Backend/ObligationSimplify.cpp @@ -28,6 +28,7 @@ std::unique_ptr cloneLogicExpr(const LogicExpr *Expr) { Copy->OverflowOp = Expr->OverflowOp; Copy->CollectionOp = Expr->CollectionOp; Copy->SpecCallee = Expr->SpecCallee; + Copy->Premise = Expr->Premise; for (const auto &Child : Expr->Children) Copy->Children.push_back(cloneLogicExpr(Child.get())); for (const auto &Pattern : Expr->Patterns) @@ -383,6 +384,7 @@ std::unique_ptr substituteVariable(const LogicExpr *Expr, Copy->OverflowOp = Expr->OverflowOp; Copy->CollectionOp = Expr->CollectionOp; Copy->SpecCallee = Expr->SpecCallee; + Copy->Premise = Expr->Premise; for (const auto &Child : Expr->Children) Copy->Children.push_back(substituteVariable(Child.get(), Name, Value)); for (const auto &Pattern : Expr->Patterns) diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index afd6b07247..705b9e0864 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -749,7 +749,7 @@ std::unique_ptr verify::createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut, unsigned BMCUnroll, const BackendExecutionOptions &Execution, - std::vector *LeanProjectGoals) { + std::vector *LeanProjectGoals) { switch (K) { case BackendKind::Z3: return std::make_unique(Execution, "z3"); diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 00e7678705..5bec7b6cdd 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -303,11 +303,13 @@ inline unsigned moduleTimeoutMs(const ObligationModule &Module, : SolverTimeoutMs; } +struct LeanProjectGoal; + std::unique_ptr createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut = nullptr, unsigned BMCUnroll = 10, const BackendExecutionOptions &Execution = {}, - std::vector *LeanProjectGoals = nullptr); + std::vector *LeanProjectGoals = nullptr); VerifyResult lowerObligationModule(const ObligationModule &Module, diff --git a/clang/lib/Verify/Driver/CppVerifyVersion.h b/clang/lib/Verify/Driver/CppVerifyVersion.h index a8d1d7cede..dd759c8e9b 100644 --- a/clang/lib/Verify/Driver/CppVerifyVersion.h +++ b/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"; diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 00611d0595..6351861a55 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -1252,7 +1252,8 @@ static llvm::Error writeTextFileIfMissing(llvm::StringRef Path, return writeTextFile(Path, Contents); } -static std::string leanGoalModuleName(llvm::StringRef Goal) { +// The proof file 0.1 wrote for a goal it named so. +static std::string leanLegacyProofModule(llvm::StringRef Goal) { llvm::MD5 Hasher; llvm::MD5::MD5Result Hash; Hasher.update(Goal); @@ -1262,6 +1263,148 @@ static std::string leanGoalModuleName(llvm::StringRef Goal) { return "Goal_" + llvm::StringRef(Hex).take_front(16).str(); } +static constexpr llvm::StringLiteral LeanLegacyStubNote = + "/- Complete this proof; this file is never regenerated. -/"; + +// Whether a proof file of 0.1 is still the stub 0.1 wrote. +static bool isLeanLegacyStub(llvm::StringRef Path) { + auto Buffer = llvm::MemoryBuffer::getFile(Path); + if (!Buffer) + return false; + llvm::StringRef Text = (*Buffer)->getBuffer(); + const llvm::StringRef Head = + "import CppVerify.User\n\n/- Complete this proof; this file is never " + "regenerated. -/\ntheorem "; + if (!Text.consume_front(Head)) + return false; + llvm::StringRef Goal = Text.take_until([](char C) { return C == ' '; }); + return Goal.consume_back("_proof") && + Text == Goal.str() + "_proof : " + Goal.str() + " := by\n sorry\n"; +} + +static constexpr llvm::StringLiteral LeanProofMark = "/- cppverify proof\n"; +static constexpr llvm::StringLiteral LeanQuarantineNote = + "-- cpp-verify kept this proof here: "; + +// What a proof file proves, from its header: a regeneration finds a proof +// by its goal's semantic hash wherever its function moved. +struct LeanProofRecord { + std::string Path; + std::string Goal; + std::string Hash; + std::string StableId; + std::string BodyPrefix; + /// The stub cpp-verify wrote, never edited: nothing in it is the user's. + bool Pristine = false; +}; + +// A stub proves the goal through its readable form, its names introduced. +static std::string leanProofStubHead(llvm::StringRef Goal) { + return "import CppVerify.User\n\ntheorem " + Goal.str() + + "_proof : " + Goal.str() + " := by\n apply " + Goal.str() + + ".of_readable\n"; +} + +static std::string leanProofStub(llvm::StringRef Goal, llvm::StringRef Intros) { + std::string Stub = leanProofStubHead(Goal); + if (!Intros.empty()) + Stub += " intro " + Intros.str() + "\n"; + return Stub + " sorry\n"; +} + +static bool isLeanProofStub(llvm::StringRef Body, llvm::StringRef Goal) { + if (!Body.consume_front(leanProofStubHead(Goal)) || + !Body.consume_back(" sorry\n")) + return false; + return Body.empty() || (Body.consume_front(" intro ") && + Body.consume_back("\n") && !Body.contains('\n')); +} + +static std::string leanProofHeader(const LeanProjectGoal &Goal) { + return LeanProofMark.str() + " goal: " + Goal.Name + + "\n obligation: " + Goal.StableId + "\n hash: " + Goal.Hash + + "\n bodies: " + Goal.BodyPrefix + + "\n source: " + (Goal.Source.empty() ? "unknown" : Goal.Source) + + "\n Complete this proof. cpp-verify never rewrites it: it moves it " + "with its goal,\n and keeps it in Stale/ when no goal has its " + "statement. -/\n"; +} + +static std::optional readLeanProof(llvm::StringRef Path) { + auto Buffer = llvm::MemoryBuffer::getFile(Path); + if (!Buffer) + return std::nullopt; + llvm::StringRef Text = (*Buffer)->getBuffer(); + if (!Text.consume_front(LeanProofMark)) + return std::nullopt; + LeanProofRecord Record; + Record.Path = Path.str(); + for (llvm::StringRef Rest = Text.take_front(Text.find("-/")); + !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + Line = Line.trim(); + if (Line.consume_front("goal: ")) + Record.Goal = Line.str(); + else if (Line.consume_front("obligation: ")) + Record.StableId = Line.str(); + else if (Line.consume_front("hash: ")) + Record.Hash = Line.str(); + else if (Line.consume_front("bodies: ")) + Record.BodyPrefix = Line.str(); + } + if (Record.Goal.empty() || Record.Hash.empty()) + return std::nullopt; + const size_t End = Text.find("-/\n"); + Record.Pristine = End != llvm::StringRef::npos && + isLeanProofStub(Text.substr(End + 3), Record.Goal); + return Record; +} + +static void replaceAllIn(std::string &Text, llvm::StringRef From, + llvm::StringRef To) { + if (From.empty() || From == To) + return; + for (size_t At = Text.find(From); At != std::string::npos; + At = Text.find(From, At + To.size())) + Text.replace(At, From.size(), To.str()); +} + +// Moves a proof to its goal's file, its generated names renamed with it. +static llvm::Error moveLeanProof(llvm::StringRef From, llvm::StringRef To, + const LeanProjectGoal &Goal, + llvm::StringRef OldGoal, + llvm::StringRef OldBodies) { + auto Buffer = llvm::MemoryBuffer::getFile(From); + if (!Buffer) + return llvm::createStringError( + Buffer.getError(), "cannot read Lean proof %s", From.str().c_str()); + llvm::StringRef Text = (*Buffer)->getBuffer(); + if (Text.consume_front(LeanProofMark)) { + const size_t End = Text.find("-/\n"); + Text = + End == llvm::StringRef::npos ? llvm::StringRef() : Text.substr(End + 3); + } + std::string Body; + for (llvm::StringRef Rest = Text; !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + if (Line.starts_with(LeanQuarantineNote) || Line == LeanLegacyStubNote) + continue; + Body += Line.str() + "\n"; + } + replaceAllIn(Body, OldGoal, Goal.Name); + replaceAllIn(Body, OldBodies, Goal.BodyPrefix); + if (std::error_code EC = + llvm::sys::fs::create_directories(llvm::sys::path::parent_path(To))) + return llvm::createStringError(EC, "cannot create %s", To.str().c_str()); + if (llvm::Error Error = writeTextFile(To, leanProofHeader(Goal) + Body)) + return Error; + if (From != To) + llvm::sys::fs::remove(From); + return llvm::Error::success(); +} + static llvm::Expected executeWithLogs(llvm::StringRef Program, const std::vector &Arguments, @@ -1430,13 +1573,26 @@ class Verifier { if (!Existing) return llvm::createStringError(Existing.getError(), "cannot read Lean toolchain pin"); - if (Existing.get()->getBuffer().trim() != - llvm::StringRef(Toolchain).trim()) - return llvm::createStringError( - llvm::inconvertibleErrorCode(), - "Lean project uses toolchain '%s'; expected '%s'", - Existing.get()->getBuffer().trim().str().c_str(), - llvm::StringRef(Toolchain).trim().str().c_str()); + const std::string Pin = Existing.get()->getBuffer().trim().str(); + if (Pin != LeanToolchain) { + // A pin an earlier release wrote is moved with the release; any + // other is the user's, and the generated semantics need ours. + if (!llvm::is_contained(EarlierLeanToolchains, Pin)) + return llvm::createStringError( + llvm::inconvertibleErrorCode(), + "Lean project uses toolchain '%s'; expected '%s'", Pin.c_str(), + LeanToolchain.str().c_str()); + if (llvm::Error Error = writeTextFile(ToolchainPath, Toolchain)) + return std::move(Error); + Diags.push_back( + {VerifyDiagnostic::Warning, + "the Lean project " + Root + " pinned " + Pin + + ", which an earlier release of cpp-verify wrote; it now " + "pins " + + LeanToolchain.str() + + ", so a proof that no longer builds needs updating for " + "that Lean"}); + } } else if (llvm::Error Error = writeTextFile(ToolchainPath, Toolchain)) { return std::move(Error); } @@ -1461,34 +1617,257 @@ class Verifier { return leanProjectPath(Root, {"CppVerify", "Generated.lean"}); } + static std::vector + leanProofComponents(const LeanProjectGoal &Goal, std::string &File) { + File = Goal.Name + ".lean"; + return {"CppVerify", "Proofs", Goal.Group, File}; + } + + // Each goal gets its proof file: the one recorded with its semantic hash, + // which follows it when its function is renamed or moved; else the one + // 0.1 wrote for it; else a stub. A proof no goal takes is kept in Stale/, + // where a goal with its statement takes it back. A fallback run examines + // only the functions its solver leaves unresolved (RunGroups names the + // groups it gave the solver), so it leaves the proofs of the others alone. llvm::Error - finalizeLeanProject(const std::vector &ProjectGoals) { + finalizeLeanProject(const std::vector &ProjectGoals, + const std::set *RunGroups) { const std::string &Root = leanProjectRoot(); - std::set UniqueGoals(ProjectGoals.begin(), ProjectGoals.end()); + const std::string ProofsDir = + leanProjectPath(Root, {"CppVerify", "Proofs"}); + const std::string StaleDir = leanProjectPath(Root, {"Stale"}); + std::map Goals, Known; + std::set Examined; + std::map StableGoal; + for (const LeanProjectGoal &Goal : ProjectGoals) { + (Goal.Exported ? Goals : Known).emplace(Goal.Name, &Goal); + Examined.insert(Goal.Group); + if (Goal.Exported) + StableGoal.emplace(Goal.StableId, Goal.Name); + } + + // Recorded proofs, live first, then kept ones, each in path order. + std::vector Records; + std::set Legacy; + for (const std::string &Dir : {ProofsDir, StaleDir}) { + std::error_code EC; + std::vector Paths; + for (llvm::sys::fs::recursive_directory_iterator It(Dir, EC), End; + It != End && !EC; It.increment(EC)) + if (llvm::sys::path::extension(It->path()) == ".lean") + Paths.push_back(It->path()); + llvm::sort(Paths); + for (const std::string &Path : Paths) + if (std::optional Record = readLeanProof(Path)) + Records.push_back(std::move(*Record)); + else if (Dir == ProofsDir && + llvm::sys::path::parent_path(Path) == ProofsDir && + llvm::sys::path::filename(Path).starts_with("Goal_")) + Legacy.insert(Path); + } + auto groupOf = [](const LeanProofRecord &Record) { + return llvm::sys::path::filename( + llvm::sys::path::parent_path(Record.Path)) + .str(); + }; + // A proof of a goal this run knows but does not export, or of a + // function it left to the solver, stays where it is. + auto unexamined = [&](const LeanProofRecord &Record) { + auto Goal = Known.find(Record.Goal); + if (Goal != Known.end() && Goal->second->Hash == Record.Hash) + return true; + const std::string Group = groupOf(Record); + return RunGroups && RunGroups->count(Group) && !Examined.count(Group); + }; + std::set Taken; + // Directories a proof left, removed at the end if nothing is left in them. + std::set Emptied; + auto relative = [&](llvm::StringRef Path) { + llvm::StringRef Rel = Path; + Rel.consume_front(Root); + return Rel.ltrim("/\\").str(); + }; + // A renamed function's goals move together: for each goal's group, how + // many of its goals a group that is gone has a proof of. + auto gone = [&](const LeanProofRecord &Record) { + return !Goals.count(Record.Goal) && !unexamined(Record) && + !Record.Pristine; + }; + std::map, unsigned> Affinity; + for (const auto &[Name, Goal] : Goals) { + std::set From; + for (const LeanProofRecord &Record : Records) + if (Record.Hash == Goal->Hash && gone(Record) && + From.insert(groupOf(Record)).second) + ++Affinity[{Goal->Group, groupOf(Record)}]; + } std::string CheckFile; - for (const std::string &Goal : UniqueGoals) { - const std::string Module = leanGoalModuleName(Goal); + for (const auto &[Name, Goal] : Goals) { + std::string File; const std::string ProofPath = - leanProjectPath(Root, {"CppVerify", "Proofs", Module + ".lean"}); - std::string Proof = - "import CppVerify.User\n\n" - "/- Complete this proof; this file is never regenerated. -/\n" - "theorem " + - Goal + "_proof : " + Goal + " := by\n sorry\n"; - if (llvm::Error Error = writeTextFileIfMissing(ProofPath, Proof)) + leanProjectPath(Root, leanProofComponents(*Goal, File)); + auto Here = llvm::find_if(Records, [&](const LeanProofRecord &Record) { + return Record.Path == ProofPath && Record.Hash == Goal->Hash; + }); + // Its own proof first, wherever it is kept; then one written for a + // goal that is gone, from the group with proofs of the most goals of + // this one (the function renamed), in path order within it. + auto Moving = llvm::find_if(Records, [&](const LeanProofRecord &Record) { + return Record.Hash == Goal->Hash && !Taken.count(Record.Path) && + Record.Goal == Name && !Record.Pristine; + }); + auto affinity = [&](const LeanProofRecord &Record) { + return Affinity[{Goal->Group, groupOf(Record)}]; + }; + if (Moving == Records.end()) + for (auto It = Records.begin(); It != Records.end(); ++It) + if (It->Hash == Goal->Hash && !Taken.count(It->Path) && gone(*It) && + (Moving == Records.end() || affinity(*It) > affinity(*Moving))) + Moving = It; + const std::string LegacyPath = leanProjectPath( + Root, {"CppVerify", "Proofs", + leanLegacyProofModule(Goal->LegacyName) + ".lean"}); + if (Here != Records.end()) { + Taken.insert(Here->Path); + } else if (Moving != Records.end() && + (Moving->Path != ProofPath || !Taken.count(ProofPath))) { + const bool WasKept = + llvm::StringRef(Moving->Path).starts_with(StaleDir); + if (llvm::Error Error = moveLeanProof(Moving->Path, ProofPath, *Goal, + Moving->Goal, Moving->BodyPrefix)) + return Error; + Diags.push_back({VerifyDiagnostic::Warning, + "the Lean proof of " + Goal->StableId + + (WasKept ? " came back from " : " moved from ") + + relative(Moving->Path) + " to " + + relative(ProofPath) + + ", the file of the goal with its statement"}); + Taken.insert(Moving->Path); + Taken.insert(ProofPath); + Emptied.insert(llvm::sys::path::parent_path(Moving->Path).str()); + } else if (Legacy.count(LegacyPath)) { + const bool Stub = isLeanLegacyStub(LegacyPath); + if (llvm::Error Error = + moveLeanProof(LegacyPath, ProofPath, *Goal, Goal->LegacyName, + Goal->LegacyBodyPrefix)) + return Error; + if (!Stub) + Diags.push_back({VerifyDiagnostic::Warning, + "the Lean proof " + relative(LegacyPath) + + " that cpp-verify 0.1 wrote for " + + Goal->StableId + " is now " + + relative(ProofPath)}); + Legacy.erase(LegacyPath); + Taken.insert(ProofPath); + } else if (llvm::sys::fs::exists(ProofPath)) { + // A proof written over its stub: its header lets it follow its + // goal from now on. + if (!readLeanProof(ProofPath)) + if (llvm::Error Error = + moveLeanProof(ProofPath, ProofPath, *Goal, Name, "")) + return Error; + Taken.insert(ProofPath); + } else { + if (std::error_code EC = llvm::sys::fs::create_directories( + llvm::sys::path::parent_path(ProofPath))) + return llvm::createStringError(EC, "cannot create %s", + ProofPath.c_str()); + if (llvm::Error Error = writeTextFile( + ProofPath, leanProofHeader(*Goal) + + leanProofStub(Goal->Name, Goal->Intros))) + return Error; + Taken.insert(ProofPath); + } + CheckFile += + "import CppVerify.Proofs." + Goal->Group + "." + Goal->Name + "\n"; + } + + // What no goal took is kept, with why. + auto keep = [&](llvm::StringRef Path, + const std::string &Why) -> llvm::Error { + llvm::SmallString<256> Kept(StaleDir); + llvm::sys::path::append(Kept, llvm::StringRef(relative(Path)) + .drop_front(std::strlen("CppVerify/"))); + std::string Target = std::string(Kept); + for (unsigned Copy = 2; llvm::sys::fs::exists(Target); ++Copy) + Target = std::string(Kept) + "." + std::to_string(Copy); + if (std::error_code EC = llvm::sys::fs::create_directories( + llvm::sys::path::parent_path(Target))) + return llvm::createStringError(EC, "cannot create %s", Target.c_str()); + if (std::error_code EC = llvm::sys::fs::rename(Path, Target)) + return llvm::createStringError(EC, "cannot keep %s", + Path.str().c_str()); + std::error_code EC; + llvm::raw_fd_ostream Note(Target, EC, llvm::sys::fs::OF_Append); + if (!EC) + Note << "\n" << LeanQuarantineNote << Why << "\n"; + Diags.push_back({VerifyDiagnostic::Warning, + "the Lean proof " + relative(Path) + " is kept in " + + relative(Target) + ": " + Why}); + return llvm::Error::success(); + }; + for (const LeanProofRecord &Record : Records) { + if (Taken.count(Record.Path) || + llvm::StringRef(Record.Path).starts_with(StaleDir) || + unexamined(Record)) + continue; + Emptied.insert(llvm::sys::path::parent_path(Record.Path).str()); + if (Record.Pristine) { + llvm::sys::fs::remove(Record.Path); + continue; + } + auto Same = StableGoal.find(Record.StableId); + std::string Why = + Same != StableGoal.end() + ? "the statement of " + Record.StableId + + " changed; its goal is now " + Same->second + : Examined.count(groupOf(Record)) + ? "its function has no obligation with this statement any more" + : "its function is gone, and no goal has its statement"; + if (llvm::Error Error = keep(Record.Path, Why)) return Error; - CheckFile += "import CppVerify.Proofs." + Module + "\n"; } + for (const std::string &Path : Legacy) + if (isLeanLegacyStub(Path)) + llvm::sys::fs::remove(Path); + else if (llvm::Error Error = + keep(Path, "a proof cpp-verify 0.1 wrote for a goal this " + "source no longer has")) + return Error; + for (std::string Dir : Emptied) + while (Dir != ProofsDir && Dir != Root && !llvm::sys::fs::remove(Dir)) + Dir = llvm::sys::path::parent_path(Dir).str(); + + if (Opts.LeanPruneStale && llvm::sys::fs::exists(StaleDir)) { + unsigned Pruned = 0; + std::error_code EC; + for (llvm::sys::fs::recursive_directory_iterator It(StaleDir, EC), End; + It != End && !EC; It.increment(EC)) + if (llvm::sys::path::extension(It->path()) == ".lean" || + llvm::StringRef(It->path()).contains(".lean.")) + ++Pruned; + if (std::error_code EC = llvm::sys::fs::remove_directories(StaleDir)) + return llvm::createStringError(EC, "cannot remove %s", + StaleDir.c_str()); + Diags.push_back({VerifyDiagnostic::Warning, + "removed " + + (Pruned == 1 ? std::string("the Lean proof") + : "the " + std::to_string(Pruned) + + " Lean proofs") + + " kept in Stale/, as --lean-prune-stale asks"}); + } + CheckFile += "\n"; - for (const std::string &Goal : UniqueGoals) { - CheckFile += "example : " + Goal + " := " + Goal + "_proof\n"; - CheckFile += "#print axioms " + Goal + "_proof\n"; + for (const auto &[Name, Goal] : Goals) { + CheckFile += "example : " + Name + " := " + Name + "_proof\n"; + CheckFile += "#print axioms " + Name + "_proof\n"; } return writeTextFile(leanProjectPath(Root, {"CppVerify", "Check.lean"}), CheckFile); } - llvm::Error certifyLeanProject(const std::vector &ProjectGoals) { + llvm::Error + certifyLeanProject(const std::vector &ProjectGoals) { if (ProjectGoals.empty()) return llvm::createStringError(llvm::inconvertibleErrorCode(), "the project has no proof obligations"); @@ -1500,14 +1879,49 @@ class Verifier { const std::string &Root = leanProjectRoot(); const std::string LogBase = leanProjectPath(Root, {".cppverify-certification"}); + // Every step runs the Lean the project pins. elan picks a toolchain by + // the working directory, not by --dir, so its proxy is given the pin; + // and whatever runs, lake must report the pinned Lean. + std::vector Launcher = {"lake"}; + auto Elan = llvm::sys::findProgramByName("elan"); + bool ViaElan = false; + if (!Elan || llvm::sys::fs::equivalent(*Lake, *Elan, ViaElan)) + ViaElan = false; + if (ViaElan) + Launcher.push_back(("+" + LeanToolchain).str()); auto runLake = [&](std::vector Arguments, llvm::StringRef Stage) -> llvm::Expected { - std::vector Command = {"lake", "--dir=" + Root}; + std::vector Command = Launcher; + Command.push_back("--dir=" + Root); Command.insert(Command.end(), std::make_move_iterator(Arguments.begin()), std::make_move_iterator(Arguments.end())); return executeWithLogs(*Lake, Command, LogBase + "-" + Stage.str()); }; + // lake takes --version alone. + std::vector Query = Launcher; + Query.push_back("--version"); + auto Reported = executeWithLogs(*Lake, Query, LogBase + "-version"); + if (!Reported) + return Reported.takeError(); + const llvm::StringRef Pinned = + LeanToolchain.substr(LeanToolchain.find(":v") + 2); + llvm::StringRef Version = *Reported; + if (size_t At = Version.find("Lean version "); At != llvm::StringRef::npos) + Version = + Version.substr(At + std::strlen("Lean version ")) + .take_while([](char C) { return llvm::isDigit(C) || C == '.'; }); + else + Version = ""; + if (Version != Pinned) + return llvm::createStringError( + llvm::inconvertibleErrorCode(), + "the project pins %s, but %s runs Lean %s; install elan " + "(https://github.com/leanprover/elan), which runs the pinned " + "toolchain", + LeanToolchain.str().c_str(), Lake->c_str(), + Version.empty() ? "of an unknown version" : Version.str().c_str()); + if (auto Build = runLake({"build", "CppVerify.Generated", "CppVerify.User"}, "build"); !Build) @@ -1528,16 +1942,23 @@ class Verifier { return llvm::createStringError( EC, "cannot create Lean proof build directory"); - std::set UniqueGoals(ProjectGoals.begin(), ProjectGoals.end()); - for (const std::string &Goal : UniqueGoals) { - const std::string Module = leanGoalModuleName(Goal); + std::map UniqueGoals; + for (const LeanProjectGoal &Goal : ProjectGoals) + UniqueGoals.emplace(Goal.Name, &Goal); + for (const auto &[Name, Goal] : UniqueGoals) { + std::string File; const std::string ProofSource = - leanProjectPath(Root, {"CppVerify", "Proofs", Module + ".lean"}); + leanProjectPath(Root, leanProofComponents(*Goal, File)); + const std::string ObjectDir = + leanProjectPath(ProofBuildDir, {Goal->Group}); + if (std::error_code EC = llvm::sys::fs::create_directories(ObjectDir)) + return llvm::createStringError( + EC, "cannot create Lean proof build directory"); const std::string ProofObject = - leanProjectPath(ProofBuildDir, {Module + ".olean"}); + leanProjectPath(ObjectDir, {Name + ".olean"}); if (auto Proof = runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", ProofObject, ProofSource}, - Module); + Name); !Proof) return Proof.takeError(); } @@ -1681,6 +2102,13 @@ class Verifier { "--lean-fallback"}); return false; } + if (Opts.LeanPruneStale && Opts.LeanProjectPath.empty() && + Opts.LeanFallbackProjectPath.empty()) { + Diags.push_back({VerifyDiagnostic::Error, + "--lean-prune-stale requires --lean-project or " + "--lean-fallback"}); + return false; + } if (Opts.LowerOnly && Opts.Backend == BackendKind::Lean) { Diags.push_back( {VerifyDiagnostic::Error, @@ -1778,7 +2206,10 @@ class Verifier { InterfaceFunctions.push_back(std::move(Interface)); } - std::vector LeanProjectGoals; + std::vector LeanProjectGoals; + // The goal groups of the modules a fallback run gave its solver, which + // it examines in Lean only when the solver leaves them unresolved. + std::set LeanRunGroups; std::unique_ptr LeanFile; llvm::raw_ostream *LeanOut = DumpOS; std::string LeanOutputPath = Opts.LeanOutPath; @@ -2585,6 +3016,8 @@ class Verifier { continue; } } else { + if (LeanFallbackBackend) + LeanRunGroups.insert(leanProjectGroup(DecModule)); VerifyResult R = SpecBackend->verify(DecModule); if (Fn->IsSpec && (R.Reason == VerifyReason::SpecHidden || R.Reason == VerifyReason::SpecFuel)) { @@ -2858,6 +3291,8 @@ class Verifier { continue; } + if (LeanFallbackBackend) + LeanRunGroups.insert(leanProjectGroup(Module)); VerifyResult R = BMCResult ? std::move(*BMCResult) : Backend->verify(Module); // Every unfolding depth gives the solver only proved facts, so the @@ -3170,14 +3605,19 @@ class Verifier { LeanFile->flush(); LeanFile.reset(); } - if (llvm::Error Error = finalizeLeanProject(LeanProjectGoals)) { + std::vector ExportedGoals; + llvm::copy_if(LeanProjectGoals, std::back_inserter(ExportedGoals), + [](const LeanProjectGoal &Goal) { return Goal.Exported; }); + if (llvm::Error Error = finalizeLeanProject( + LeanProjectGoals, + LeanFallbackBackend ? &LeanRunGroups : nullptr)) { AllOk = false; AnyFailed = true; Diags.push_back({VerifyDiagnostic::Error, "cannot finalize Lean project (" + llvm::toString(std::move(Error)) + ")"}); } else if (Opts.LeanCertify && !interruptRequested() && - (!LeanProjectGoals.empty() || + (!ExportedGoals.empty() || Opts.LeanFallbackProjectPath.empty())) { // A verdict certification does not make a proof is reported, and // what its vacuity checks found is not. @@ -3190,7 +3630,7 @@ class Verifier { if (Finding.FindingOf == Index) Finding.Hidden = true; }; - if (llvm::Error Error = certifyLeanProject(LeanProjectGoals)) { + if (llvm::Error Error = certifyLeanProject(ExportedGoals)) { AllOk = false; AnyFailed = true; const std::string Reason = llvm::toString(std::move(Error)); diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 7983a7055a..09bd4dfaf5 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -38,6 +38,8 @@ struct VerifyOptions { std::string LeanFallbackProjectPath; LeanFallbackScope LeanScope = LeanFallbackScope::Unproved; bool LeanCertify = false; + /// Delete the proofs a Lean project keeps in Stale/ once regenerated. + bool LeanPruneStale = false; unsigned BMCUnroll = 10; /// Per-query solver timeout in milliseconds; 0 disables it. Non-terminating /// queries return Unknown instead of hanging the tool. diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index dd6f7849b3..b54e616bec 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -9,6 +9,7 @@ #include "llvm/ADT/STLFunctionalExtras.h" #include "llvm/ADT/SmallString.h" #include "llvm/ADT/StringRef.h" +#include "llvm/Support/SaveAndRestore.h" #include #include #include @@ -2915,6 +2916,7 @@ void verify::addChoiceAxioms(std::vector> &Facts, auto Instance = std::make_unique(); Instance->K = PassiveStmt::Assume; Instance->Theorem = Theorem; + Instance->Origin = "choose"; Instance->Cond = std::move(Fact); Facts.push_back(std::move(Instance)); } @@ -3068,6 +3070,7 @@ static void addFrameInstances(PassiveProgram &P, const FunctionMap &FnMap) { Instance->K = PassiveStmt::Assume; Instance->TraceEventCount = P.Stmts[S.Index]->TraceEventCount; Instance->Theorem = true; + Instance->Origin = "reads:" + Spec.Name; Instance->Cond = std::move(Fact); After[S.Index].push_back(std::move(Instance)); Work.push_back(S.Before); @@ -3141,6 +3144,7 @@ addSpecPostInstances(PassiveProgram &P, const FunctionMap &FnMap, auto Instance = std::make_unique(); Instance->K = PassiveStmt::Assume; Instance->Theorem = true; + Instance->Origin = "spec:" + Spec.Name; Instance->Cond = std::move(Fact); if (Spec.Unfolding) Unfolded.push_back(Instance->Cond.get()); @@ -3218,6 +3222,7 @@ addSpecPostInstances(PassiveProgram &P, const FunctionMap &FnMap, std::move(Fact), Call.Loc, (*Q)->BinderType); auto Instance = std::make_unique(); Instance->K = PassiveStmt::Assume; + Instance->Origin = "spec:" + Spec.Name; Instance->Cond = std::move(Fact); Facts.push_back(std::move(Instance)); } @@ -3257,6 +3262,8 @@ class PassivizerImpl { std::string EntryHeap; }; std::vector LoopFrames; + /// Where the assumptions being emitted come from (PassiveStmt::Origin). + std::string Origin; std::vector> ReturnGuards; std::vector OwnedAllocationIdentities; std::map> ReferenceBindings; @@ -3999,6 +4006,8 @@ class PassivizerImpl { PS->K = K; PS->ProofKind = ProofKind; PS->Note = std::move(Note); + if (K == PassiveStmt::Assume) + PS->Origin = Origin; PS->TraceEventCount = TraceEvents.size(); if (Guard) Cond = makeImplies(cloneVExpr(Guard), std::move(Cond), Loc); @@ -4038,6 +4047,7 @@ class PassivizerImpl { !needsInactiveFrame(Guard)) return; auto Inactive = makeNot(cloneVExpr(Guard), Loc); + llvm::SaveAndRestore Kept(Origin, "keep"); emitPassive(P, PassiveStmt::Assume, makeEq(std::make_unique(After.str(), Ty, Loc), std::make_unique(Before.str(), Ty, Loc), Loc), @@ -4109,6 +4119,7 @@ class PassivizerImpl { } std::string ResultName = bump(ResultVar); Renames["result"] = ResultName; + llvm::SaveAndRestore Returned(Origin, "ret"); emitMathBridge(P, Result.get(), nullptr, SourceLocation(), true); emitPassive(P, PassiveStmt::Assume, makeEq(std::make_unique(ResultName, Fn.ReturnType, @@ -4233,13 +4244,12 @@ class PassivizerImpl { for (const SafetyCheck &Check : Checks) emitPassive(P, PassiveStmt::Assert, cloneExpr(Check.Cond.get(), Ctx), Guard, Loc, Check.Kind, Check.Note); - emitPassive(P, PassiveStmt::Assume, - machineMathBridgeForExpr(E, &FnMap, BridgeMachineValue), Guard, - Loc); + emitMathBridge(P, E, Guard, Loc, BridgeMachineValue); } void emitMathBridge(PassiveProgram &P, const VExpr *E, const VExpr *Guard, SourceLocation Loc, bool BridgeMachineValue = false) { + llvm::SaveAndRestore Exact(Origin, "exact"); emitPassive(P, PassiveStmt::Assume, machineMathBridgeForExpr(E, &FnMap, BridgeMachineValue), Guard, Loc); @@ -4577,6 +4587,9 @@ class PassivizerImpl { for (const auto &Pre : Fn.Preconditions) { CloneCtx PCtx{Renames, OldState, false}; + P.EntryOrigins.push_back( + P.EntryAssumes.size() < Fn.ExplicitPreconditionCount ? "pre" + : "entry"); P.EntryAssumes.push_back(cloneExpr(Pre.get(), PCtx)); } P.PreconditionCount = P.EntryAssumes.size(); @@ -4596,12 +4609,15 @@ class PassivizerImpl { std::move(Null), VType::makeBool(), SourceLocation(), Renames[VLivenessHeapName]); P.EntryAssumes.push_back(makeNot(std::move(NullLive), SourceLocation())); + P.EntryOrigins.insert(P.EntryOrigins.end(), 2, "null"); } if (Fn.ObjectModel) { CloneCtx PCtx{Renames, OldState, false}; - for (const AbstractObject &Object : abstractObjects(Fn)) + for (const AbstractObject &Object : abstractObjects(Fn)) { P.EntryAssumes.push_back(cloneExpr( objectPlacement(Object, SourceLocation()).get(), PCtx)); + P.EntryOrigins.push_back("object"); + } } std::unique_ptr Active = makeBoolLiteral(true, SourceLocation()); @@ -5298,6 +5314,7 @@ class PassivizerImpl { for (const auto &Post : Callee->Postconditions) { auto PS = std::make_unique(); PS->K = PassiveStmt::Assume; + PS->Origin = "call:" + Callee->Name; PS->Cond = rebaseSliceBinders(substParams(Post.get(), PostParamMap, Ctx, EntryHeap, "", {}, &ParamMap)); P.Stmts.push_back(std::move(PS)); @@ -5309,9 +5326,41 @@ class PassivizerImpl { } } + // The origin of the assumptions a statement makes, before its parts name + // their own. + static std::string statementOrigin(const VStmt &S) { + switch (S.K) { + case VStmt::Assign: + return "def"; + case VStmt::Store: + return "store"; + case VStmt::Allocate: + case VStmt::EndLifetime: + case VStmt::Free: + return "alloc"; + case VStmt::If: + return "branch"; + case VStmt::Return: + return "ret"; + case VStmt::While: + return "loop"; + case VStmt::Call: + return "call:" + static_cast(S).Callee; + case VStmt::ContractAssert: + return "check"; + case VStmt::Havoc: + return "havoc"; + default: + return "fact"; + } + } + void processStmt(const VStmt &S, PassiveProgram &P, std::map &Renames, std::unique_ptr &Active) { + std::optional> Named; + if (S.K != VStmt::Seq && S.K != VStmt::GhostBlock) + Named.emplace(Origin, statementOrigin(S)); switch (S.K) { case VStmt::Assign: { const auto &A = static_cast(S); @@ -6009,6 +6058,7 @@ class PassivizerImpl { } CloneCtx HeadCtx{Renames, OldState, false}; + llvm::SaveAndRestore Head(Origin, "frame"); if (!LoopEntryHeap.empty()) { // Every iteration starts with the cells outside the declared // footprints unchanged since the loop began. @@ -6018,11 +6068,13 @@ class PassivizerImpl { W.Loc), Active.get(), W.Loc); } + Origin = "inv"; for (const auto &Inv : W.Invariants) { auto BoundInv = cloneExpr(Inv.get(), HeadCtx); emitPassive(P, PassiveStmt::Assume, std::move(BoundInv), Active.get(), W.Loc); } + Origin = "cond"; std::string ChoiceName = bump("__loop_choice"); auto Choice = @@ -6084,6 +6136,7 @@ class PassivizerImpl { } emitTrace(PassiveTraceKind::Loop, "exit", Active.get(), W.Loc); + Origin = "exit"; std::vector Returns; for (size_t I = ReturnsBefore; I != ReturnGuards.size(); ++I) Returns.push_back(ReturnGuards[I].get()); diff --git a/clang/lib/Verify/Transform/Passivize.h b/clang/lib/Verify/Transform/Passivize.h index b4dcea5c87..0291f72b02 100644 --- a/clang/lib/Verify/Transform/Passivize.h +++ b/clang/lib/Verify/Transform/Passivize.h @@ -31,6 +31,9 @@ struct PassiveStmt { /// postcondition or unfolding, a frame of a spec's reads), not a premise /// of the function's claim. Unmarked assumptions are premises. bool Theorem = false; + /// For an assumption: where it comes from (`pre`, `call:f`, `inv`, ...), + /// which names its hypothesis in a readable goal. + std::string Origin; }; /// A goal checked in the final state. @@ -80,6 +83,8 @@ struct PassiveProgram { std::vector> EntryAssumes; /// How many leading EntryAssumes are the function's own preconditions. size_t PreconditionCount = 0; + /// Where each of EntryAssumes comes from, as PassiveStmt::Origin. + std::vector EntryOrigins; /// Each behavior's assumption in the entry state. std::vector>> BehaviorAssumes; std::vector ExitAsserts; diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean index 25b70cbfbe..391927a090 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppverify_impossible_fn_5f5a3130696d706f737369626c6569_obligation_2_goal_proof : cppverify_impossible_fn_5f5a3130696d706f737369626c6569_obligation_2_goal := by - unfold cppverify_impossible_fn_5f5a3130696d706f737369626c6569_obligation_2_goal +theorem cppverify_impossible_9d6c7c_postcondition_1cd35301_proof : cppverify_impossible_9d6c7c_postcondition_1cd35301 := by + unfold cppverify_impossible_9d6c7c_postcondition_1cd35301 intro _ _ _ x left intro ⟨above, below⟩ diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean index 5660202676..b07ce3c20e 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppverify_looping_fn_5f5a376c6f6f70696e676a6a_obligation_2_goal_proof : cppverify_looping_fn_5f5a376c6f6f70696e676a6a_obligation_2_goal := by - unfold cppverify_looping_fn_5f5a376c6f6f70696e676a6a_obligation_2_goal +theorem cppverify_looping_3f4bd4_postcondition_d06fccd0_proof : cppverify_looping_3f4bd4_postcondition_d06fccd0 := by + unfold cppverify_looping_3f4bd4_postcondition_d06fccd0 intro _ _ _ r a b _ _ _ have thousand : (BitVec.ofInt 32 1000).toNat = 1000 := by decide rcases Classical.em (cppBvUlt a (BitVec.ofInt 32 1000) ∧ diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean index eb5e890c30..9df085a719 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean @@ -1,8 +1,8 @@ import CppVerify.User -theorem cppverify_product_fn_5f5a3770726f647563746a6a_obligation_2_goal_proof : - cppverify_product_fn_5f5a3770726f647563746a6a_obligation_2_goal := by - unfold cppverify_product_fn_5f5a3770726f647563746a6a_obligation_2_goal +theorem cppverify_product_4751c3_postcondition_c4d4674b_proof : + cppverify_product_4751c3_postcondition_c4d4674b := by + unfold cppverify_product_4751c3_postcondition_c4d4674b intro _ _ r c a b have thousand : (BitVec.ofInt 32 1000).toNat = 1000 := by decide rcases Classical.em (cppBvUlt a (BitVec.ofInt 32 1000) ∧ diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean index ec96f2cad6..4a3c213156 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppverify_positive_fn_5f5a38706f73697469766569_obligation_2_goal_proof : cppverify_positive_fn_5f5a38706f73697469766569_obligation_2_goal := by - unfold cppverify_positive_fn_5f5a38706f73697469766569_obligation_2_goal +theorem cppverify_positive_fb6abf_postcondition_78bdd643_proof : cppverify_positive_fb6abf_postcondition_78bdd643 := by + unfold cppverify_positive_fb6abf_postcondition_78bdd643 intro _ _ r x by_cases h : r = x · exact Or.inr (Or.inr (Or.inr (Or.inr h))) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean index 9b031a6292..5a8320c770 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppverify_same_fn_5f5a3473616d6569_obligation_2_goal_proof : cppverify_same_fn_5f5a3473616d6569_obligation_2_goal := by - unfold cppverify_same_fn_5f5a3473616d6569_obligation_2_goal +theorem cppverify_same_9601c2_postcondition_ce92acf8_proof : cppverify_same_9601c2_postcondition_ce92acf8 := by + unfold cppverify_same_9601c2_postcondition_ce92acf8 intro _ _ r x by_cases h : r = x · exact Or.inr (Or.inr (Or.inr h)) diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean index 4c86973e95..ae71525385 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppverify_seven_fn_5f5a35736576656e69_obligation_2_goal_proof : cppverify_seven_fn_5f5a35736576656e69_obligation_2_goal := by - unfold cppverify_seven_fn_5f5a35736576656e69_obligation_2_goal +theorem cppverify_seven_634ea3_postcondition_f0d135e6_proof : cppverify_seven_634ea3_postcondition_f0d135e6 := by + unfold cppverify_seven_634ea3_postcondition_f0d135e6 intro _ _ r c by_cases hc : c = BitVec.ofInt 32 7 · by_cases hr : r = c diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean index 6f865f372d..86ffa0028e 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppEncoded_6370707665726966795f7363616c65642e6465637265617365735f666e5f356635613336373336333631366336353634363936393a3a6465637265617365735f6f626c69676174696f6e5f315f676f616c_proof : cppEncoded_6370707665726966795f7363616c65642e6465637265617365735f666e5f356635613336373336333631366336353634363936393a3a6465637265617365735f6f626c69676174696f6e5f315f676f616c := by - unfold cppEncoded_6370707665726966795f7363616c65642e6465637265617365735f666e5f356635613336373336333631366336353634363936393a3a6465637265617365735f6f626c69676174696f6e5f315f676f616c +theorem cppverify_scaled_decreases_52d363_termination_3164b050_proof : cppverify_scaled_decreases_52d363_termination_3164b050 := by + unfold cppverify_scaled_decreases_52d363_termination_3164b050 intro a b have measure : a ≤ 0 ∨ b ≤ 0 ∨ (a * b ≥ 0 ∧ a * (b - 1) < a * b) := by by_cases ha : a ≤ 0 diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean index 025bfcd81c..3fd338653d 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppverify_trusting_fn_5f5a387472757374696e6769_obligation_2_goal_proof : cppverify_trusting_fn_5f5a387472757374696e6769_obligation_2_goal := by - unfold cppverify_trusting_fn_5f5a387472757374696e6769_obligation_2_goal +theorem cppverify_trusting_b6301a_postcondition_bafafdfb_proof : cppverify_trusting_b6301a_postcondition_bafafdfb := by + unfold cppverify_trusting_b6301a_postcondition_bafafdfb intro _ _ r c by_cases hc : c = BitVec.ofInt 32 7 · by_cases hr : r = c diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean index 5442b6ea2e..8ba810ff34 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean @@ -1,5 +1,5 @@ import CppVerify.User -theorem cppverify_fibo_step_fn_5f5a396669626f5f7374657069_obligation_1_goal_proof : - cppverify_fibo_step_fn_5f5a396669626f5f7374657069_obligation_1_goal := by - simp [cppverify_fibo_step_fn_5f5a396669626f5f7374657069_obligation_1_goal] +theorem cppverify_fibo_step_624f01_missing_return_ba8abb90_proof : + cppverify_fibo_step_624f01_missing_return_ba8abb90 := by + simp [cppverify_fibo_step_624f01_missing_return_ba8abb90] diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean index 3d9cb7b9d2..df65b45915 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean @@ -1,8 +1,8 @@ import CppVerify.User -theorem cppverify_fibo_step_fn_5f5a396669626f5f7374657069_obligation_2_goal_proof : - cppverify_fibo_step_fn_5f5a396669626f5f7374657069_obligation_2_goal := by - unfold cppverify_fibo_step_fn_5f5a396669626f5f7374657069_obligation_2_goal +theorem cppverify_fibo_step_624f01_postcondition_559cb60a_proof : + cppverify_fibo_step_624f01_postcondition_559cb60a := by + unfold cppverify_fibo_step_624f01_postcondition_559cb60a intro __heap_alloc_0 __heap_live_0 i_0 spec1 spec2 spec3 by_cases h : cppBvSle (BitVec.ofInt 32 1) i_0 ∧ @@ -17,7 +17,7 @@ theorem cppverify_fibo_step_fn_5f5a396669626f5f7374657069_obligation_2_goal_proo have minusTwo : i_0.toInt + 1 - 2 = i_0.toInt - 1 := by omega have minusOne : i_0.toInt + 1 - 1 = i_0.toInt := by omega rw [spec1] - unfold cppSpecBody_m1_fn_5f5a346669626f69_1 + unfold cppSpecBody_624f0147_fn_5f5a346669626f69_1 rw [if_neg positive, if_neg notOne, minusTwo, minusOne] exact Int.add_comm _ _ · exact Or.inl h diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean index 004382c179..55b9772bad 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean @@ -1,5 +1,5 @@ import CppVerify.User -theorem cppverify_fibo_six_fn_5f5a386669626f5f73697876_obligation_1_goal_proof : - cppverify_fibo_six_fn_5f5a386669626f5f73697876_obligation_1_goal := by - simp [cppverify_fibo_six_fn_5f5a386669626f5f73697876_obligation_1_goal] +theorem cppverify_fibo_six_ec829a_missing_return_ba8abb90_proof : + cppverify_fibo_six_ec829a_missing_return_ba8abb90 := by + simp [cppverify_fibo_six_ec829a_missing_return_ba8abb90] diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean index eaed431aa1..8ebf102ec4 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean @@ -1,14 +1,14 @@ import CppVerify.User -theorem cppverify_fibo_six_fn_5f5a386669626f5f73697876_obligation_2_goal_proof : - cppverify_fibo_six_fn_5f5a386669626f5f73697876_obligation_2_goal := by - unfold cppverify_fibo_six_fn_5f5a386669626f5f73697876_obligation_2_goal +theorem cppverify_fibo_six_ec829a_postcondition_30cd1b97_proof : + cppverify_fibo_six_ec829a_postcondition_30cd1b97 := by + unfold cppverify_fibo_six_ec829a_postcondition_30cd1b97 intro __heap_alloc_0 __heap_live_0 _ _ _ _ _ _ _ unfolded intros right right have six : (BitVec.ofInt 32 6).toInt = 6 := rfl rw [unfolded, six] - simp [cppSpecBody_m2_fn_5f5a346669626f69_8, cppSpecBody_m2_fn_5f5a346669626f69_7, - cppSpecBody_m2_fn_5f5a346669626f69_6, cppSpecBody_m2_fn_5f5a346669626f69_5, - cppSpecBody_m2_fn_5f5a346669626f69_4, cppSpecBody_m2_fn_5f5a346669626f69_3] + simp [cppSpecBody_ec829a45_fn_5f5a346669626f69_8, cppSpecBody_ec829a45_fn_5f5a346669626f69_7, + cppSpecBody_ec829a45_fn_5f5a346669626f69_6, cppSpecBody_ec829a45_fn_5f5a346669626f69_5, + cppSpecBody_ec829a45_fn_5f5a346669626f69_4, cppSpecBody_ec829a45_fn_5f5a346669626f69_3] diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean index 31bb88d006..aa658e5ebc 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean @@ -1,8 +1,8 @@ import CppVerify.User -theorem cppverify_bump_fn_5f5a3462756d7069_obligation_1_goal_proof : - cppverify_bump_fn_5f5a3462756d7069_obligation_1_goal := by - unfold cppverify_bump_fn_5f5a3462756d7069_obligation_1_goal +theorem cppverify_bump_ce87d1_overflow_f5ee4d20_proof : + cppverify_bump_ce87d1_overflow_f5ee4d20 := by + unfold cppverify_bump_ce87d1_overflow_f5ee4d20 intro _ _ x_0 by_cases pre : cppBvSle (BitVec.ofInt 32 0) x_0 ∧ cppBvSle x_0 (BitVec.ofInt 32 100) · right; right; right diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean index 1dfd0975c6..8d12720c5a 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean @@ -1,8 +1,8 @@ import CppVerify.User -theorem cppverify_bump_fn_5f5a3462756d7069_obligation_2_goal_proof : - cppverify_bump_fn_5f5a3462756d7069_obligation_2_goal := by - unfold cppverify_bump_fn_5f5a3462756d7069_obligation_2_goal +theorem cppverify_bump_ce87d1_assertion_06404a7a_proof : + cppverify_bump_ce87d1_assertion_06404a7a := by + unfold cppverify_bump_ce87d1_assertion_06404a7a intro _ _ x_0 y_1 by_cases pre : cppBvSle (BitVec.ofInt 32 0) x_0 ∧ cppBvSle x_0 (BitVec.ofInt 32 100) · right; right; right; right diff --git a/clang/test/Verify/suite/Inputs/lean_identity_base.cpp b/clang/test/Verify/suite/Inputs/lean_identity_base.cpp new file mode 100644 index 0000000000..796a5d227a --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_base.cpp @@ -0,0 +1,20 @@ +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int six() + cppverify::post(cppverify::result == tri(3)) +{ + cppverify::reveal_with_fuel(tri, 4); + return 6; +} + +int one() + cppverify::post(cppverify::result == 1) + cppverify::post(cppverify::result >= 0) + cppverify::post(cppverify::result == 1) +{ + return 1; +} diff --git a/clang/test/Verify/suite/Inputs/lean_identity_changed.cpp b/clang/test/Verify/suite/Inputs/lean_identity_changed.cpp new file mode 100644 index 0000000000..d33ab7ee63 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_changed.cpp @@ -0,0 +1,20 @@ +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int six_again() + cppverify::post(cppverify::result == tri(3)) +{ + cppverify::reveal_with_fuel(tri, 4); + return 6; +} + +int one_again() + cppverify::post(cppverify::result == 1) + cppverify::post(cppverify::result >= 1) + cppverify::post(cppverify::result == 1) +{ + return 1; +} diff --git a/clang/test/Verify/suite/Inputs/lean_identity_inserted.cpp b/clang/test/Verify/suite/Inputs/lean_identity_inserted.cpp new file mode 100644 index 0000000000..f819906698 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_inserted.cpp @@ -0,0 +1,26 @@ +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int zero() + cppverify::post(cppverify::result == 0) +{ + return 0; +} + +int six() + cppverify::post(cppverify::result == tri(3)) +{ + cppverify::reveal_with_fuel(tri, 4); + return 6; +} + +int one() + cppverify::post(cppverify::result >= 0) + cppverify::post(cppverify::result == 1) + cppverify::post(cppverify::result == 1) +{ + return 1; +} diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean new file mode 100644 index 0000000000..145a149822 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean @@ -0,0 +1,6 @@ +import CppVerify.User + +theorem cppverify_bump_ce87d1_missing_return_ba8abb90_proof : + cppverify_bump_ce87d1_missing_return_ba8abb90 := by + unfold cppverify_bump_ce87d1_missing_return_ba8abb90 + trivial diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean new file mode 100644 index 0000000000..f9024c9662 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -0,0 +1,6 @@ +import CppVerify.User + +theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : + cppverify_one_99bcee_missing_return_54ae7c80 := by + unfold cppverify_one_99bcee_missing_return_54ae7c80 + trivial diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean new file mode 100644 index 0000000000..eee644659e --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean @@ -0,0 +1,9 @@ +import CppVerify.User + +theorem cppverify_one_99bcee_postcondition_cd6bdfcd_proof : + cppverify_one_99bcee_postcondition_cd6bdfcd := by + unfold cppverify_one_99bcee_postcondition_cd6bdfcd + intro _ _ r + by_cases h : r = BitVec.ofInt 32 1 + · right; right; right; exact h + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean new file mode 100644 index 0000000000..7f4b99e6d4 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean @@ -0,0 +1,9 @@ +import CppVerify.User + +theorem cppverify_one_99bcee_postcondition_cd6bdfcd_2_proof : + cppverify_one_99bcee_postcondition_cd6bdfcd_2 := by + unfold cppverify_one_99bcee_postcondition_cd6bdfcd_2 + intro _ _ r + by_cases h : r = BitVec.ofInt 32 1 + · right; right; right; exact h + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean new file mode 100644 index 0000000000..5b4dde2b95 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean @@ -0,0 +1,9 @@ +import CppVerify.User + +theorem cppverify_one_99bcee_postcondition_ebbe6a6a_proof : + cppverify_one_99bcee_postcondition_ebbe6a6a := by + unfold cppverify_one_99bcee_postcondition_ebbe6a6a + intro _ _ r + by_cases h : r = BitVec.ofInt 32 1 + · right; right; right; subst h; decide + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean new file mode 100644 index 0000000000..f3ca2db1f1 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean @@ -0,0 +1,6 @@ +import CppVerify.User + +theorem cppverify_six_6a2cf3_missing_return_54ae7c80_proof : + cppverify_six_6a2cf3_missing_return_54ae7c80 := by + unfold cppverify_six_6a2cf3_missing_return_54ae7c80 + trivial diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean new file mode 100644 index 0000000000..3dae61ac78 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean @@ -0,0 +1,14 @@ +import CppVerify.User + +theorem cppverify_six_6a2cf3_postcondition_198bc076_proof : + cppverify_six_6a2cf3_postcondition_198bc076 := by + unfold cppverify_six_6a2cf3_postcondition_198bc076 + intro _ _ r _ _ _ unfolded + intros + have three : (BitVec.ofInt 32 3).toInt = 3 := rfl + rw [unfolded, three] + by_cases h : r = BitVec.ofInt 32 6 + · right; right; right + simp [cppSpecBody_6a2cf351_fn_5f5a3374726969_4, cppSpecBody_6a2cf351_fn_5f5a3374726969_3, + cppSpecBody_6a2cf351_fn_5f5a3374726969_2, cppSpecBody_6a2cf351_fn_5f5a3374726969_1, h] + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean new file mode 100644 index 0000000000..9f5bed9a7f --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean @@ -0,0 +1,7 @@ +import CppVerify.User + +theorem cppverify_tri_decreases_f55d4c_termination_3c6bb93f_proof : + cppverify_tri_decreases_f55d4c_termination_3c6bb93f := by + unfold cppverify_tri_decreases_f55d4c_termination_3c6bb93f + intro n + omega diff --git a/clang/test/Verify/suite/Inputs/lean_identity_removed.cpp b/clang/test/Verify/suite/Inputs/lean_identity_removed.cpp new file mode 100644 index 0000000000..ae9b8ddf63 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_removed.cpp @@ -0,0 +1,12 @@ +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int six_again() + cppverify::post(cppverify::result == tri(3)) +{ + cppverify::reveal_with_fuel(tri, 4); + return 6; +} diff --git a/clang/test/Verify/suite/Inputs/lean_identity_renamed.cpp b/clang/test/Verify/suite/Inputs/lean_identity_renamed.cpp new file mode 100644 index 0000000000..68a0496a6c --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_renamed.cpp @@ -0,0 +1,20 @@ +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int six_again() + cppverify::post(cppverify::result == tri(3)) +{ + cppverify::reveal_with_fuel(tri, 4); + return 6; +} + +int one_again() + cppverify::post(cppverify::result == 1) + cppverify::post(cppverify::result >= 0) + cppverify::post(cppverify::result == 1) +{ + return 1; +} diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000deadbeef.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000deadbeef.lean new file mode 100644 index 0000000000..baf64b7d11 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000deadbeef.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_gone_fn_5f5a34676f6e6576_obligation_1_goal_proof : cppverify_gone_fn_5f5a34676f6e6576_obligation_1_goal := by + trivial diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000feedface.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000feedface.lean new file mode 100644 index 0000000000..77acef893f --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000feedface.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_gone_fn_5f5a34676f6e6576_obligation_2_goal_proof : cppverify_gone_fn_5f5a34676f6e6576_obligation_2_goal := by + sorry diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_1272763fe029af5c.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_1272763fe029af5c.lean new file mode 100644 index 0000000000..e316810c29 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_1272763fe029af5c.lean @@ -0,0 +1,7 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_six_fn_5f5a3373697876_obligation_1_goal_proof : + cppverify_six_fn_5f5a3373697876_obligation_1_goal := by + unfold cppverify_six_fn_5f5a3373697876_obligation_1_goal + trivial diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_14843fe605ca0dfc.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_14843fe605ca0dfc.lean new file mode 100644 index 0000000000..8f1f2028e5 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_14843fe605ca0dfc.lean @@ -0,0 +1,10 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_one_fn_5f5a336f6e6576_obligation_2_goal_proof : + cppverify_one_fn_5f5a336f6e6576_obligation_2_goal := by + unfold cppverify_one_fn_5f5a336f6e6576_obligation_2_goal + intro _ _ r + by_cases h : r = BitVec.ofInt 32 1 + · right; right; right; exact h + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_959f92a07e95a169.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_959f92a07e95a169.lean new file mode 100644 index 0000000000..e85144ce5c --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_959f92a07e95a169.lean @@ -0,0 +1,8 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppEncoded_6370707665726966795f7472692e6465637265617365735f666e5f35663561333337343732363936393a3a6465637265617365735f6f626c69676174696f6e5f315f676f616c_proof : + cppEncoded_6370707665726966795f7472692e6465637265617365735f666e5f35663561333337343732363936393a3a6465637265617365735f6f626c69676174696f6e5f315f676f616c := by + unfold cppEncoded_6370707665726966795f7472692e6465637265617365735f666e5f35663561333337343732363936393a3a6465637265617365735f6f626c69676174696f6e5f315f676f616c + intro n + omega diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_9b7aec03175825c9.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_9b7aec03175825c9.lean new file mode 100644 index 0000000000..82665dc269 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_9b7aec03175825c9.lean @@ -0,0 +1,10 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_one_fn_5f5a336f6e6576_obligation_4_goal_proof : + cppverify_one_fn_5f5a336f6e6576_obligation_4_goal := by + unfold cppverify_one_fn_5f5a336f6e6576_obligation_4_goal + intro _ _ r + by_cases h : r = BitVec.ofInt 32 1 + · right; right; right; exact h + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b054b023e3576f6e.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b054b023e3576f6e.lean new file mode 100644 index 0000000000..9accd4e683 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b054b023e3576f6e.lean @@ -0,0 +1,15 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_six_fn_5f5a3373697876_obligation_2_goal_proof : + cppverify_six_fn_5f5a3373697876_obligation_2_goal := by + unfold cppverify_six_fn_5f5a3373697876_obligation_2_goal + intro _ _ r _ _ _ unfolded + intros + have three : (BitVec.ofInt 32 3).toInt = 3 := rfl + rw [unfolded, three] + by_cases h : r = BitVec.ofInt 32 6 + · right; right; right + simp [cppSpecBody_m2_fn_5f5a3374726969_4, cppSpecBody_m2_fn_5f5a3374726969_3, + cppSpecBody_m2_fn_5f5a3374726969_2, cppSpecBody_m2_fn_5f5a3374726969_1, h] + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b95e8b7f774dddd4.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b95e8b7f774dddd4.lean new file mode 100644 index 0000000000..c1fd38a764 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b95e8b7f774dddd4.lean @@ -0,0 +1,10 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_one_fn_5f5a336f6e6576_obligation_3_goal_proof : + cppverify_one_fn_5f5a336f6e6576_obligation_3_goal := by + unfold cppverify_one_fn_5f5a336f6e6576_obligation_3_goal + intro _ _ r + by_cases h : r = BitVec.ofInt 32 1 + · right; right; right; subst h; decide + · right; right; left; exact h diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_f799910065d5f258.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_f799910065d5f258.lean new file mode 100644 index 0000000000..3865d7cf0c --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_f799910065d5f258.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +/- Complete this proof; this file is never regenerated. -/ +theorem cppverify_one_fn_5f5a336f6e6576_obligation_1_goal_proof : cppverify_one_fn_5f5a336f6e6576_obligation_1_goal := by + sorry diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/User.lean b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/User.lean new file mode 100644 index 0000000000..acf50c2cf4 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/User.lean @@ -0,0 +1,3 @@ +import CppVerify.Generated + +/- Add reusable lemmas here. This file is never regenerated. -/ diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/lakefile.toml b/clang/test/Verify/suite/Inputs/lean_identity_v01/lakefile.toml new file mode 100644 index 0000000000..cef9515ee9 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/lakefile.toml @@ -0,0 +1,6 @@ +name = "cppverify_proof" +version = "0.1.0" +defaultTargets = ["CppVerify"] + +[[lean_lib]] +name = "CppVerify" diff --git a/clang/test/Verify/suite/Inputs/lean_identity_v01/lean-toolchain b/clang/test/Verify/suite/Inputs/lean_identity_v01/lean-toolchain new file mode 100644 index 0000000000..0ec5999cc0 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_identity_v01/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.32.2 diff --git a/clang/test/Verify/suite/Inputs/lean_readable_certify.cpp b/clang/test/Verify/suite/Inputs/lean_readable_certify.cpp new file mode 100644 index 0000000000..88f1e5fddb --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_certify.cpp @@ -0,0 +1,12 @@ +[[cppverify::trusted]] int next(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1); + +int twice(int x) + cppverify::pre(x >= 0 && x < 50) + cppverify::post(cppverify::result == x + 2) +{ + int a = next(x); + int b = next(a); + return b; +} diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean new file mode 100644 index 0000000000..d450f13548 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_missing_return_54ae7c80_proof : cppverify_twice_edf933_missing_return_54ae7c80 := by + apply cppverify_twice_edf933_missing_return_54ae7c80.of_readable + trivial diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean new file mode 100644 index 0000000000..e1080ebc94 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean @@ -0,0 +1,14 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by + apply cppverify_twice_edf933_postcondition_28de726e.of_readable + intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 + obtain ⟨_, first⟩ := h_call_next_1 + obtain ⟨_, second⟩ := h_call_next_2 + subst h_result_1 h_b_1 second h_a_1 first + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + refine ⟨by omega, ?_⟩ + rw [BitVec.add_assoc] + rfl diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean new file mode 100644 index 0000000000..5c6b0e43e4 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean @@ -0,0 +1,14 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_precondition_51b3c1f0_proof : cppverify_twice_edf933_precondition_51b3c1f0 := by + apply cppverify_twice_edf933_precondition_51b3c1f0.of_readable + intro __heap_alloc_0 __heap_live_0 __local_call_1_1 a_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 + obtain ⟨range, called⟩ := h_call_next_1 + subst h_a_1 called + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 ⊢ + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 1).toInt = 1 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + have : (BitVec.ofInt 32 100).toInt = 100 := rfl + rw [BitVec.toInt_add_of_not_saddOverflow (by simp [BitVec.saddOverflow]; omega)] + omega diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean new file mode 100644 index 0000000000..2607fff7eb --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean @@ -0,0 +1,10 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_precondition_f0a3d715_proof : cppverify_twice_edf933_precondition_f0a3d715 := by + apply cppverify_twice_edf933_precondition_f0a3d715.of_readable + intro __heap_alloc_0 __heap_live_0 x_0 h_pre_1 h_null_1 h_null_2 + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 ⊢ + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + have : (BitVec.ofInt 32 100).toInt = 100 := rfl + omega diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_call.lean b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean index 7d56339ab0..8dc0f46fa3 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_call.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean @@ -1,8 +1,8 @@ import CppVerify.User -theorem cppverify_small_fn_5f5a35736d616c6c76_obligation_1_goal_proof : - cppverify_small_fn_5f5a35736d616c6c76_obligation_1_goal := by - unfold cppverify_small_fn_5f5a35736d616c6c76_obligation_1_goal +theorem cppverify_small_74ff94_precondition_4e324fa2_proof : + cppverify_small_74ff94_precondition_4e324fa2 := by + unfold cppverify_small_74ff94_precondition_4e324fa2 intro _ _ have zero : (BitVec.ofInt 32 0).toInt = 0 := by decide exact Or.inr (Or.inr (Or.inr ⟨fun _ range => by rw [zero] at range; omega, by decide⟩)) diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean index 49b38d981d..4c46c601c2 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean @@ -1,8 +1,8 @@ import CppVerify.User -theorem cppverify_mix_fn_5f5a336d69786a6a_obligation_1_goal_proof : - cppverify_mix_fn_5f5a336d69786a6a_obligation_1_goal := by - unfold cppverify_mix_fn_5f5a336d69786a6a_obligation_1_goal +theorem cppverify_mix_b839ab_assertion_255467f3_proof : + cppverify_mix_b839ab_assertion_255467f3 := by + unfold cppverify_mix_b839ab_assertion_255467f3 intro _ _ a b r s by_cases hr : r = a ^^^ b + (BitVec.ofInt 32 (1)) · by_cases hs : s = a ^^^ b + (BitVec.ofInt 32 (1)) diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean index b4953f1245..5142c33706 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean @@ -1,7 +1,7 @@ import CppVerify.User -theorem cppverify_difference_fn_5f5a3130646966666572656e636576_obligation_1_goal_proof : - cppverify_difference_fn_5f5a3130646966666572656e636576_obligation_1_goal := by - unfold cppverify_difference_fn_5f5a3130646966666572656e636576_obligation_1_goal +theorem cppverify_difference_465d5b_assertion_d7e0e821_proof : + cppverify_difference_465d5b_assertion_d7e0e821 := by + unfold cppverify_difference_465d5b_assertion_d7e0e821 intro _ _ exact Or.inr (Or.inr (by decide)) diff --git a/clang/test/Verify/suite/Inputs/lean_toolchain.cpp b/clang/test/Verify/suite/Inputs/lean_toolchain.cpp new file mode 100644 index 0000000000..ddd0978a3d --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_toolchain.cpp @@ -0,0 +1,3 @@ +void trivial() + cppverify::post(true) +{} diff --git a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py index 46ac53062f..18d97cddca 100644 --- a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py +++ b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py @@ -1,7 +1,6 @@ #!/usr/bin/env python3 import argparse -import hashlib import json import pathlib import re @@ -399,18 +398,28 @@ def check_archive_matrix(cpp_verify, source, work, source_records): return canonical -def goal_names(lean_text): - names = set( +def project_goals(lean_text): + goals = {} + for match in re.finditer( + r"^/- obligation: (\S+)\n kind: (\S+)\n source: ([^\n]*) -/\n" + r"def (cppverify_[A-Za-z0-9_]+) : Prop :=$", + lean_text, + re.MULTILINE, + ): + goals[match.group(4)] = match.group(1, 2, 3) + if not goals: + fail("Lean export contains no named obligation goals") + return goals + + +def obligation_records(lean_text): + return sorted( re.findall( - r"^def ((?:cppverify_[A-Za-z0-9_]+_goal)|" - r"(?:cppEncoded_[0-9a-f]+)) : Prop :=$", + r"^/- obligation: (\S+)\n kind: (\S+)\n source: ([^\n]*) -/$", lean_text, re.MULTILINE, ) ) - if not names: - fail("Lean export contains no named obligation goals") - return names def scratch_theorem_names(lean_text): @@ -427,12 +436,6 @@ def scratch_theorem_names(lean_text): return names -def decode_lean_name(name): - if not name.startswith("cppEncoded_"): - return name - return bytes.fromhex(name.removeprefix("cppEncoded_")).decode("utf-8") - - def check_lean_identity(cpp_verify, source, canonical, work): source_lean = work / "source.lean" replay_lean = work / "replay.lean" @@ -460,7 +463,7 @@ def check_lean_identity(cpp_verify, source, canonical, work): ) if source_lean.read_bytes() != replay_lean.read_bytes(): fail("source and archive replay produced different Lean semantics") - scratch_goals = scratch_theorem_names(source_lean.read_text()) + scratch_theorem_names(source_lean.read_text()) run( [ @@ -478,37 +481,42 @@ def check_lean_identity(cpp_verify, source, canonical, work): if "sorry" in text: fail("generated Lean semantics contains an admitted proof") - goals = goal_names(text) - decoded_scratch_goals = {decode_lean_name(goal) for goal in scratch_goals} - if { - decode_lean_name(goal).removesuffix("_goal") for goal in goals - } - decoded_scratch_goals: + goals = project_goals(text) + if sorted(goals.values()) != obligation_records(source_lean.read_text()): fail("Lean project goal identities differ from scratch/archive export") - proof_files = list((project / "CppVerify" / "Proofs").glob("Goal_*.lean")) + proofs = project / "CppVerify" / "Proofs" + proof_files = sorted(proofs.glob("*/*.lean")) if len(proof_files) != len(goals): fail("Lean project proof-module count does not match generated goals") proof_goals = set() for proof_file in proof_files: - match = re.search( - r"^theorem ((?:cppverify_[A-Za-z0-9_]+_goal)|" - r"(?:cppEncoded_[0-9a-f]+))_proof :", - proof_file.read_text(), - re.MULTILINE, + text = proof_file.read_text() + header = re.match( + r"/- cppverify proof\n goal: (\S+)\n obligation: (\S+)\n" + r" hash: ([0-9a-f]{64})\n", + text, ) - if not match: + if not header: fail("malformed Lean proof module {}".format(proof_file.name)) - goal = match.group(1) - expected_name = "Goal_{}.lean".format( - hashlib.md5(goal.encode("utf-8")).hexdigest()[:16] + goal, obligation, digest = header.groups() + group = proof_file.parent.name + name = re.fullmatch( + re.escape(group) + r"_[a-z0-9_]+_([0-9a-f]{8})(?:_[0-9]+)?", goal ) - if proof_file.name != expected_name: - fail( - "Lean goal hash mismatch: {} should be {}".format( - proof_file.name, expected_name - ) - ) + if proof_file.name != goal + ".lean" or not name: + fail("Lean proof module {} is not named by its goal".format( + proof_file.relative_to(proofs) + )) + if not digest.startswith(name.group(1)): + fail("Lean goal hash mismatch: {} records {}".format(goal, digest)) + if goals.get(goal, (None,))[0] != obligation: + fail("Lean proof module {} names obligation {}".format( + goal, obligation + )) + if "theorem {}_proof :".format(goal) not in text: + fail("malformed Lean proof module {}".format(proof_file.name)) proof_goals.add(goal) - if proof_goals != goals: + if proof_goals != set(goals): fail("Lean proof modules do not cover the generated theorem identities") run(["lake", "--dir={}".format(project), "build", "CppVerify.Generated"], {0}) diff --git a/clang/test/Verify/suite/lean_certify.cpp b/clang/test/Verify/suite/lean_certify.cpp index 87f7c3da6f..00c6550f43 100644 --- a/clang/test/Verify/suite/lean_certify.cpp +++ b/clang/test/Verify/suite/lean_certify.cpp @@ -4,20 +4,20 @@ // RUN: not %cpp-verify --backend=lean --lean-project=%t.admitted --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=ADMITTED // // RUN: %cpp-verify --backend=lean --lean-project=%t.certified %s -- -// RUN: sed -i.orig 's/ sorry/ simp [cppverify_trivial_fn_5f5a377472697669616c76_obligation_1_goal]/' %t.certified/CppVerify/Proofs/Goal_583ed320b83a75f8.lean -// RUN: sed -i.orig 's/ sorry/ simp [cppverify_trivial_fn_5f5a377472697669616c76_obligation_2_goal]/' %t.certified/CppVerify/Proofs/Goal_279b1b0b28d9b239.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.certified/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.certified/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_postcondition_ba8abb90.lean // RUN: %cpp-verify --backend=lean --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED // RUN: echo 'theorem unfinished : True := by sorry' >> %t.certified/CppVerify/User.lean // RUN: not %cpp-verify --backend=lean --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=USER-ADMITTED // // RUN: %cpp-verify --backend=lean --lean-project=%t.axiom %s -- // RUN: echo 'axiom escape {p : Prop} : p' >> %t.axiom/CppVerify/User.lean -// RUN: sed -i.orig 's/ sorry/ exact escape/' %t.axiom/CppVerify/Proofs/*.lean +// RUN: sed -i.orig 's/ sorry/ exact escape/' %t.axiom/CppVerify/Proofs/*/*.lean // RUN: not %cpp-verify --backend=lean --lean-project=%t.axiom --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=AXIOM // // RUN: %cpp-verify --backend=lean --lean-project=%t.stale %s -- -// RUN: sed -i.orig 's/ sorry/ simp [cppverify_trivial_fn_5f5a377472697669616c76_obligation_1_goal]/' %t.stale/CppVerify/Proofs/Goal_583ed320b83a75f8.lean -// RUN: sed -i.orig 's/ sorry/ simp [cppverify_trivial_fn_5f5a377472697669616c76_obligation_2_goal]/' %t.stale/CppVerify/Proofs/Goal_279b1b0b28d9b239.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.stale/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.stale/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_postcondition_ba8abb90.lean // RUN: not %cpp-verify --backend=lean --lean-project=%t.stale --lean-certify %S/Inputs/lean_certify_stale.cpp -- 2>&1 | FileCheck %s --check-prefix=STALE void trivial() diff --git a/clang/test/Verify/suite/lean_dependencies.test b/clang/test/Verify/suite/lean_dependencies.test index d0fc25b318..d238f92634 100644 --- a/clang/test/Verify/suite/lean_dependencies.test +++ b/clang/test/Verify/suite/lean_dependencies.test @@ -10,12 +10,12 @@ # The Lean backend, with every goal proved. An export proves nothing, so it # runs no vacuity check. # RUN: %cpp-verify --backend=lean --lean-project=%t.backend %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND-EXPORT -# RUN: sed -i.orig 's/^ sorry$/ trivial/' %t.backend/CppVerify/Proofs/Goal_*.lean -# RUN: cp %S/Inputs/lean_dependencies_seven.lean %t.backend/CppVerify/Proofs/Goal_dbfc9c3cab47bb98.lean -# RUN: cp %S/Inputs/lean_dependencies_trusting.lean %t.backend/CppVerify/Proofs/Goal_9597ad7a35f15bda.lean -# RUN: cp %S/Inputs/lean_dependencies_impossible.lean %t.backend/CppVerify/Proofs/Goal_5ee9cbcb4bd4ca4c.lean -# RUN: cp %S/Inputs/lean_dependencies_same.lean %t.backend/CppVerify/Proofs/Goal_8f4b3a6a5ff5a52f.lean -# RUN: cp %S/Inputs/lean_dependencies_positive.lean %t.backend/CppVerify/Proofs/Goal_4091f113f9bfaf75.lean +# RUN: sed -i.orig 's/^ sorry$/ trivial/' %t.backend/CppVerify/Proofs/*/*.lean +# RUN: cp %S/Inputs/lean_dependencies_seven.lean %t.backend/CppVerify/Proofs/cppverify_seven_634ea3/cppverify_seven_634ea3_postcondition_f0d135e6.lean +# RUN: cp %S/Inputs/lean_dependencies_trusting.lean %t.backend/CppVerify/Proofs/cppverify_trusting_b6301a/cppverify_trusting_b6301a_postcondition_bafafdfb.lean +# RUN: cp %S/Inputs/lean_dependencies_impossible.lean %t.backend/CppVerify/Proofs/cppverify_impossible_9d6c7c/cppverify_impossible_9d6c7c_postcondition_1cd35301.lean +# RUN: cp %S/Inputs/lean_dependencies_same.lean %t.backend/CppVerify/Proofs/cppverify_same_9601c2/cppverify_same_9601c2_postcondition_ce92acf8.lean +# RUN: cp %S/Inputs/lean_dependencies_positive.lean %t.backend/CppVerify/Proofs/cppverify_positive_fb6abf/cppverify_positive_fb6abf_postcondition_78bdd643.lean # RUN: not %cpp-verify --backend=lean --lean-project=%t.backend --lean-certify %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND # RUN: not %cpp-verify --backend=lean --lean-project=%t.backend --lean-certify --diagnostics-format=json %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND-JSON # @@ -32,14 +32,14 @@ # with the proof left as sorry, then completed. # RUN: not %cpp-verify --solver-rlimit=1000 --lean-fallback=%t.termination %S/Inputs/lean_dependencies_termination.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT # RUN: not %cpp-verify --solver-rlimit=1000 --lean-fallback=%t.termination --lean-certify %S/Inputs/lean_dependencies_termination.cpp -- 2>&1 | FileCheck %s --check-prefix=SORRY -# RUN: cp %S/Inputs/lean_dependencies_termination.lean %t.termination/CppVerify/Proofs/Goal_5225f06eaadb3197.lean +# RUN: cp %S/Inputs/lean_dependencies_termination.lean %t.termination/CppVerify/Proofs/cppverify_scaled_decreases_52d363/cppverify_scaled_decreases_52d363_termination_3164b050.lean # RUN: not %cpp-verify --solver-rlimit=1000 --lean-fallback=%t.termination --lean-certify %S/Inputs/lean_dependencies_termination.cpp -- 2>&1 | FileCheck %s --check-prefix=PROVED # # A function proved by Z3 and Lean together establishes its contract, and # its result is qualified as a solver's is. # RUN: not %cpp-verify --solver-rlimit=300 --lean-fallback=%t.mixed %S/Inputs/lean_dependencies_mixed.cpp -- -# RUN: cp %S/Inputs/lean_dependencies_mixed.lean %t.mixed/CppVerify/Proofs/Goal_7f9f727f06e4d358.lean -# RUN: cp %S/Inputs/lean_dependencies_looping.lean %t.mixed/CppVerify/Proofs/Goal_2f3026c9b1466449.lean +# RUN: cp %S/Inputs/lean_dependencies_mixed.lean %t.mixed/CppVerify/Proofs/cppverify_product_4751c3/cppverify_product_4751c3_postcondition_c4d4674b.lean +# RUN: cp %S/Inputs/lean_dependencies_looping.lean %t.mixed/CppVerify/Proofs/cppverify_looping_3f4bd4/cppverify_looping_3f4bd4_postcondition_d06fccd0.lean # RUN: not %cpp-verify --solver-rlimit=300 --lean-fallback=%t.mixed --lean-certify %S/Inputs/lean_dependencies_mixed.cpp -- 2>&1 | FileCheck %s --check-prefix=MIXED # A contract without a definition establishes nothing, whoever proves the diff --git a/clang/test/Verify/suite/lean_fallback.test b/clang/test/Verify/suite/lean_fallback.test index d3f6c060c3..1aed3ce551 100644 --- a/clang/test/Verify/suite/lean_fallback.test +++ b/clang/test/Verify/suite/lean_fallback.test @@ -4,13 +4,13 @@ // RUN: not %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s // RUN: test -f %t.project/CppVerify/Generated.lean // RUN: test -f %t.project/CppVerify/Check.lean -// RUN: grep -q '^import CppVerify.Proofs.Goal_' %t.project/CppVerify/Check.lean +// RUN: grep -q '^import CppVerify.Proofs.cppverify_' %t.project/CppVerify/Check.lean // RUN: FileCheck %s --input-file=%t.project/CppVerify/Generated.lean --check-prefix=GENERATED // RUN: not %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY -// RUN: cp %S/Inputs/lean_fallback_goal_1.lean %t.project/CppVerify/Proofs/Goal_e255e6a3bdc0555b.lean -// RUN: cp %S/Inputs/lean_fallback_goal_2.lean %t.project/CppVerify/Proofs/Goal_28110d7c20c54bdc.lean -// RUN: cp %S/Inputs/lean_fallback_goal_3.lean %t.project/CppVerify/Proofs/Goal_dcd133d1bd994eee.lean -// RUN: cp %S/Inputs/lean_fallback_goal_4.lean %t.project/CppVerify/Proofs/Goal_157b784bdc2cd4d9.lean +// RUN: cp %S/Inputs/lean_fallback_goal_1.lean %t.project/CppVerify/Proofs/cppverify_fibo_step_624f01/cppverify_fibo_step_624f01_missing_return_ba8abb90.lean +// RUN: cp %S/Inputs/lean_fallback_goal_2.lean %t.project/CppVerify/Proofs/cppverify_fibo_step_624f01/cppverify_fibo_step_624f01_postcondition_559cb60a.lean +// RUN: cp %S/Inputs/lean_fallback_goal_3.lean %t.project/CppVerify/Proofs/cppverify_fibo_six_ec829a/cppverify_fibo_six_ec829a_missing_return_ba8abb90.lean +// RUN: cp %S/Inputs/lean_fallback_goal_4.lean %t.project/CppVerify/Proofs/cppverify_fibo_six_ec829a/cppverify_fibo_six_ec829a_postcondition_30cd1b97.lean // RUN: %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED // RUN: %cpp-verify --solver-rlimit=400 --lean-fallback-scope=all --lean-fallback=%t.project --lean-certify --diagnostics-format=json %S/spec_fuel_recursive_pass.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED-JSON // RUN: rm -rf %t.json-project diff --git a/clang/test/Verify/suite/lean_fallback_fast.cpp b/clang/test/Verify/suite/lean_fallback_fast.cpp index adc107ad16..43fca7ac94 100644 --- a/clang/test/Verify/suite/lean_fallback_fast.cpp +++ b/clang/test/Verify/suite/lean_fallback_fast.cpp @@ -2,7 +2,7 @@ // RUN: not %cpp-verify --solver-rlimit=1 --lean-fallback=%t.project %s -- 2>&1 \ // RUN: | FileCheck %s // RUN: test -f %t.project/CppVerify/Check.lean -// RUN: grep -c '^import CppVerify.Proofs.Goal_' \ +// RUN: grep -c '^import CppVerify.Proofs.cppverify_' \ // RUN: %t.project/CppVerify/Check.lean | FileCheck %s --check-prefix=GOALS cppverify::spec int double_value(int value) { diff --git a/clang/test/Verify/suite/lean_fallback_partial.test b/clang/test/Verify/suite/lean_fallback_partial.test index fe59d0215f..1b7bc677fd 100644 --- a/clang/test/Verify/suite/lean_fallback_partial.test +++ b/clang/test/Verify/suite/lean_fallback_partial.test @@ -1,13 +1,14 @@ # REQUIRES: lean # -# Only obligations Z3 leaves unproved are exported; they keep their positional -# goal names, and certifying them yields a mixed Z3+Lean proof. +# Only obligations Z3 leaves unproved are exported; they keep the goal names +# they have in a complete export, and certifying them yields a mixed Z3+Lean +# proof. # # RUN: rm -rf %t.project # RUN: not %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT -# RUN: FileCheck %s --input-file=%t.project/CppVerify/Check.lean --check-prefix=GOALS -# RUN: cp %S/Inputs/lean_fallback_partial_goal_1.lean %t.project/CppVerify/Proofs/Goal_ea6538a5c8cb138e.lean -# RUN: cp %S/Inputs/lean_fallback_partial_goal_2.lean %t.project/CppVerify/Proofs/Goal_53d4e62b4037d310.lean +# RUN: FileCheck %s --input-file=%t.project/CppVerify/Check.lean --check-prefix=GOALS --implicit-check-not=missing_return +# RUN: cp %S/Inputs/lean_fallback_partial_goal_1.lean %t.project/CppVerify/Proofs/cppverify_bump_ce87d1/cppverify_bump_ce87d1_overflow_f5ee4d20.lean +# RUN: cp %S/Inputs/lean_fallback_partial_goal_2.lean %t.project/CppVerify/Proofs/cppverify_bump_ce87d1/cppverify_bump_ce87d1_assertion_06404a7a.lean # RUN: %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project --lean-certify %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=MIXED # RUN: %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project --lean-certify --diagnostics-format=json %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=MIXED-JSON # RUN: not %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project --lean-fallback-scope=all --lean-certify %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=ALL @@ -15,9 +16,8 @@ # EXPORT: Exported: lean fallback: bump [z3: 1 of 3 proved; lean: 2 exported] # EXPORT: Unresolved: bump [backend=z3] [reason=solver.resource-limit] -# GOALS: obligation_1_goal -# GOALS: obligation_2_goal -# GOALS-NOT: obligation_3_goal +# GOALS: cppverify_bump_ce87d1_assertion_06404a7a +# GOALS: cppverify_bump_ce87d1_overflow_f5ee4d20 # MIXED: Proved (z3+lean): bump [z3: 1 of 3 proved; lean: 2 certified] # MIXED-NOT: Unresolved diff --git a/clang/test/Verify/suite/lean_identity.test b/clang/test/Verify/suite/lean_identity.test new file mode 100644 index 0000000000..d66b654f83 --- /dev/null +++ b/clang/test/Verify/suite/lean_identity.test @@ -0,0 +1,198 @@ +# REQUIRES: lean +# +# A Lean project names a goal by its function and the hash of its statement, +# and each proof file records that hash, so a proof stays with its statement +# as the source around it changes. The sources sit in a directory whose path +# holds `/-`, which a Lean comment must not take as a nested comment. +# +# RUN: rm -rf %t && mkdir -p %t/-src +# RUN: cp %S/Inputs/lean_identity_base.cpp %t/-src/base.cpp +# RUN: cp %S/Inputs/lean_identity_inserted.cpp %t/-src/inserted.cpp +# RUN: cp %S/Inputs/lean_identity_renamed.cpp %t/-src/renamed.cpp +# RUN: cp %S/Inputs/lean_identity_changed.cpp %t/-src/changed.cpp +# RUN: cp %S/Inputs/lean_identity_removed.cpp %t/-src/removed.cpp +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/base.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT --implicit-check-not=warning +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Check.lean --check-prefix=IMPORTS +# +# Proofs written over their stubs get the header that lets them follow their +# goals. +# RUN: cp %S/Inputs/lean_identity_proofs/cppverify_tri_* %t/p/CppVerify/Proofs/cppverify_tri_decreases_f55d4c/ +# RUN: cp %S/Inputs/lean_identity_proofs/cppverify_six_* %t/p/CppVerify/Proofs/cppverify_six_6a2cf3/ +# RUN: cp %S/Inputs/lean_identity_proofs/cppverify_one_* %t/p/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/base.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT --implicit-check-not=warning +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean --check-prefix=HEADER +# +# A function inserted before and postconditions reordered change no +# statement: every proof stays, and so do the spec bodies the proofs unfold. +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/inserted.cpp -- 2>&1 | FileCheck %s --check-prefix=INSERTED --implicit-check-not=warning +# RUN: grep -q 'cppSpecBody_6a2cf351_fn_5f5a3374726969_4,' %t/p/CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean +# RUN: grep -q '^def cppSpecBody_6a2cf351_fn_5f5a3374726969_4$' %t/p/CppVerify/Generated.lean +# RUN: test -f %t/p/CppVerify/Proofs/cppverify_zero_5ece85/cppverify_zero_5ece85_postcondition_36923ed0.lean +# +# Renamed functions take their proofs along, each its own, with the names +# they use; the stubs of the function that is gone are removed. +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/-src/renamed.cpp -- 2>&1 | FileCheck %s --check-prefix=RENAMED --implicit-check-not=warning +# RUN: grep -q 'cppSpecBody_1480fe52_fn_5f5a3374726969_4,' %t/p/CppVerify/Proofs/cppverify_six_again_1480fe/cppverify_six_again_1480fe_postcondition_198bc076.lean +# RUN: not test -e %t/p/CppVerify/Proofs/cppverify_six_6a2cf3 +# RUN: not test -e %t/p/CppVerify/Proofs/cppverify_one_99bcee +# RUN: not test -e %t/p/CppVerify/Proofs/cppverify_zero_5ece85 +# +# A changed statement never gets the old proof: it is kept in Stale/, with +# a note naming the goal of the changed obligation. +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/changed.cpp -- 2>&1 | FileCheck %s --check-prefix=CHANGED --implicit-check-not=warning +# RUN: FileCheck %s --input-file=%t/p/Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean --check-prefix=NOTE +# +# Reverted, the statement takes its proof back, and the stub of the changed +# one is removed. +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/renamed.cpp -- 2>&1 | FileCheck %s --check-prefix=REVERTED --implicit-check-not=warning +# RUN: not test -e %t/p/CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_34c13fbe.lean +# RUN: not grep -q 'cpp-verify kept this proof here' %t/p/CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean +# +# A removed function's proofs are kept; an unedited stub is removed. +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %t/-src/removed.cpp -- 2>&1 | FileCheck %s --check-prefix=REMOVED --implicit-check-not=warning +# RUN: not test -e %t/p/CppVerify/Proofs/cppverify_one_again_52815a +# +# Back under their first names, every proof returns, from Stale/ too, and +# all of them check. +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %t/-src/base.cpp -- 2>&1 | FileCheck %s --check-prefix=BACK --implicit-check-not=warning +# RUN: not test -e %t/p/Stale +# +# A fallback run examines only what its solver leaves unresolved: the proofs +# of the functions the solver settles stay where they are. +# RUN: %cpp-verify --lean-fallback=%t/p %t/-src/base.cpp -- 2>&1 | FileCheck %s --check-prefix=FALLBACK --implicit-check-not=warning +# RUN: test -f %t/p/CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_ebbe6a6a.lean +# RUN: sed '/^int one()/,$d' %t/-src/base.cpp > %t/-src/without_one.cpp +# RUN: %cpp-verify --lean-fallback=%t/p %t/-src/without_one.cpp -- 2>&1 | FileCheck %s --check-prefix=FALLBACK-REMOVED --implicit-check-not=warning +# RUN: test -f %t/p/CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean +# +# Kept proofs are deleted only on request. +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-prune-stale %t/-src/without_one.cpp -- 2>&1 | FileCheck %s --check-prefix=PRUNE --implicit-check-not=warning +# RUN: not test -e %t/p/Stale +# RUN: not %cpp-verify --lean-prune-stale %t/-src/without_one.cpp -- 2>&1 | FileCheck %s --check-prefix=PRUNE-ALONE +# +# The goals of a partly exported function that the solver proved keep their +# proofs. +# RUN: not %cpp-verify --solver-rlimit=100 --lean-fallback=%t/q --lean-fallback-scope=all %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=PARTIAL-ALL +# RUN: cp %S/Inputs/lean_identity_proofs/cppverify_bump_* %t/q/CppVerify/Proofs/cppverify_bump_ce87d1/ +# RUN: not %cpp-verify --solver-rlimit=100 --lean-fallback=%t/q --lean-fallback-scope=all %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=PARTIAL-ALL --implicit-check-not=warning +# RUN: grep -q 'hash: ba8abb90' %t/q/CppVerify/Proofs/cppverify_bump_ce87d1/cppverify_bump_ce87d1_missing_return_ba8abb90.lean +# RUN: not %cpp-verify --solver-rlimit=100 --lean-fallback=%t/q %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=PARTIAL --implicit-check-not=warning +# RUN: grep -q trivial %t/q/CppVerify/Proofs/cppverify_bump_ce87d1/cppverify_bump_ce87d1_missing_return_ba8abb90.lean +# RUN: not grep -q missing_return %t/q/CppVerify/Check.lean +# +# Stubs are not proofs: a function with nothing but stubs, renamed, gets new +# stubs, with no move to report. +# RUN: %cpp-verify --backend=lean --lean-project=%t/s %t/-src/base.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT --implicit-check-not=warning +# RUN: %cpp-verify --backend=lean --lean-project=%t/s %t/-src/renamed.cpp -- 2>&1 | FileCheck %s --check-prefix=STUBS --implicit-check-not=warning +# RUN: not test -e %t/s/Stale +# +# A project of 0.1 moves to its pin and to these names: its proofs move to +# the files of their goals with every generated name they use, its unedited +# stubs silently, and a proof of a goal that is gone is kept. +# RUN: cp -r %S/Inputs/lean_identity_v01 %t/m +# RUN: %cpp-verify --backend=lean --lean-project=%t/m %t/-src/base.cpp -- 2>&1 | FileCheck %s --check-prefix=MIGRATE --implicit-check-not=warning -DPROJECT=%t/m +# RUN: grep -q 'cppSpecBody_6a2cf351_fn_5f5a3374726969_4,' %t/m/CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean +# RUN: grep -q 'cppverify_gone_fn_5f5a34676f6e6576_obligation_1_goal_proof' %t/m/Stale/Proofs/Goal_00000000deadbeef.lean +# RUN: not test -e %t/m/CppVerify/Proofs/Goal_00000000feedface.lean +# RUN: cp %S/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean %t/m/CppVerify/Proofs/cppverify_one_99bcee/ +# RUN: %cpp-verify --backend=lean --lean-project=%t/m --lean-certify %t/-src/base.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED --implicit-check-not=warning + +# EXPORT: Exported: decreases: tri +# EXPORT-NEXT: Exported: lean obligation: six +# EXPORT-NEXT: Exported: lean obligation: one + +# IMPORTS: import CppVerify.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_missing_return_54ae7c80 +# IMPORTS-NEXT: import CppVerify.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_postcondition_cd6bdfcd +# IMPORTS-NEXT: import CppVerify.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_postcondition_cd6bdfcd_2 +# IMPORTS-NEXT: import CppVerify.Proofs.cppverify_one_99bcee.cppverify_one_99bcee_postcondition_ebbe6a6a +# IMPORTS-NEXT: import CppVerify.Proofs.cppverify_six_6a2cf3.cppverify_six_6a2cf3_missing_return_54ae7c80 +# IMPORTS-NEXT: import CppVerify.Proofs.cppverify_six_6a2cf3.cppverify_six_6a2cf3_postcondition_198bc076 +# IMPORTS-NEXT: import CppVerify.Proofs.cppverify_tri_decreases_f55d4c.cppverify_tri_decreases_f55d4c_termination_3c6bb93f +# IMPORTS-EMPTY: + +# HEADER: /- cppverify proof +# HEADER-NEXT: goal: cppverify_six_6a2cf3_postcondition_198bc076 +# HEADER-NEXT: obligation: fn_5f5a3373697876::postcondition@8:37 +# HEADER-NEXT: hash: 198bc0762967df1bfb4e7851125ba87e9761e99c4b6b075ff2d3b06dea679fbe +# HEADER-NEXT: bodies: cppSpecBody_6a2cf351_ +# HEADER-NEXT: source: {{.*}}/ -src/base.cpp:8:37 +# HEADER: -/ +# HEADER-NEXT: import CppVerify.User +# HEADER-EMPTY: +# HEADER-NEXT: theorem cppverify_six_6a2cf3_postcondition_198bc076_proof : + +# INSERTED: Exported: decreases: tri +# INSERTED-NEXT: Exported: lean obligation: zero +# INSERTED-NEXT: Exported: lean obligation: six +# INSERTED-NEXT: Exported: lean obligation: one + +# RENAMED: Certified: decreases: tri [backend=Lean] +# RENAMED-NEXT: Certified: six_again [backend=Lean] +# RENAMED-NEXT: Certified: one_again [backend=Lean] +# RENAMED-NEXT: warning: the Lean proof of fn_5f5a396f6e655f616761696e76::missing-return@synthetic moved from CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_missing_return_54ae7c80.lean to CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_missing_return_54ae7c80.lean, the file of the goal with its statement +# RENAMED-NEXT: warning: the Lean proof of fn_5f5a396f6e655f616761696e76::postcondition@15:37 moved from CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd.lean to CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd.lean, the file of the goal with its statement +# RENAMED-NEXT: warning: the Lean proof of fn_5f5a396f6e655f616761696e76::postcondition@17:37 moved from CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean to CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd_2.lean, the file of the goal with its statement +# RENAMED-NEXT: warning: the Lean proof of fn_5f5a396f6e655f616761696e76::postcondition@16:37 moved from CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_ebbe6a6a.lean to CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean, the file of the goal with its statement +# RENAMED-NEXT: warning: the Lean proof of fn_5f5a397369785f616761696e76::missing-return@synthetic moved from CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_missing_return_54ae7c80.lean to CppVerify/Proofs/cppverify_six_again_1480fe/cppverify_six_again_1480fe_missing_return_54ae7c80.lean, the file of the goal with its statement +# RENAMED-NEXT: warning: the Lean proof of fn_5f5a397369785f616761696e76::postcondition@8:37 moved from CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean to CppVerify/Proofs/cppverify_six_again_1480fe/cppverify_six_again_1480fe_postcondition_198bc076.lean, the file of the goal with its statement + +# CHANGED: Exported: lean obligation: one_again +# CHANGED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean is kept in Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean: the statement of fn_5f5a396f6e655f616761696e76::postcondition@16:37 changed; its goal is now cppverify_one_again_52815a_postcondition_34c13fbe + +# NOTE: theorem cppverify_one_again_52815a_postcondition_ebbe6a6a_proof : +# NOTE: -- cpp-verify kept this proof here: the statement of fn_5f5a396f6e655f616761696e76::postcondition@16:37 changed; its goal is now cppverify_one_again_52815a_postcondition_34c13fbe + +# REVERTED: Exported: lean obligation: one_again +# REVERTED-NEXT: warning: the Lean proof of fn_5f5a396f6e655f616761696e76::postcondition@16:37 came back from Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean to CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean, the file of the goal with its statement + +# REMOVED: Exported: lean obligation: six_again +# REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_missing_return_54ae7c80.lean is kept in Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_missing_return_54ae7c80.lean: its function is gone, and no goal has its statement +# REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd.lean is kept in Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd.lean: its function is gone, and no goal has its statement +# REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd_2.lean is kept in Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd_2.lean: its function is gone, and no goal has its statement +# REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean is kept in Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean: its function is gone, and no goal has its statement + +# BACK: Certified: decreases: tri [backend=Lean] +# BACK-NEXT: Certified: six [backend=Lean] +# BACK-NEXT: Certified: one [backend=Lean] +# BACK-NEXT: warning: the Lean proof of fn_5f5a336f6e6576::missing-return@synthetic came back from Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_missing_return_54ae7c80.lean to CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_missing_return_54ae7c80.lean, the file of the goal with its statement +# BACK-NEXT: warning: the Lean proof of fn_5f5a336f6e6576::postcondition@15:37 came back from Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd.lean to CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd.lean, the file of the goal with its statement +# BACK-NEXT: warning: the Lean proof of fn_5f5a336f6e6576::postcondition@17:37 came back from Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_cd6bdfcd_2.lean to CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean, the file of the goal with its statement +# BACK-NEXT: warning: the Lean proof of fn_5f5a336f6e6576::postcondition@16:37 came back from Stale/Proofs/cppverify_one_again_52815a/cppverify_one_again_52815a_postcondition_ebbe6a6a.lean to CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_ebbe6a6a.lean, the file of the goal with its statement +# BACK-NEXT: warning: the Lean proof of fn_5f5a3373697876::missing-return@synthetic moved from CppVerify/Proofs/cppverify_six_again_1480fe/cppverify_six_again_1480fe_missing_return_54ae7c80.lean to CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_missing_return_54ae7c80.lean, the file of the goal with its statement +# BACK-NEXT: warning: the Lean proof of fn_5f5a3373697876::postcondition@8:37 moved from CppVerify/Proofs/cppverify_six_again_1480fe/cppverify_six_again_1480fe_postcondition_198bc076.lean to CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean, the file of the goal with its statement + +# FALLBACK: Verified: spec decreases: tri +# FALLBACK-NEXT: Verified: six [backend=z3] +# FALLBACK-NEXT: Verified: one [backend=z3] + +# FALLBACK-REMOVED: Verified: six [backend=z3] +# FALLBACK-REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_missing_return_54ae7c80.lean is kept in Stale/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_missing_return_54ae7c80.lean: its function is gone, and no goal has its statement +# FALLBACK-REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd.lean is kept in Stale/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd.lean: its function is gone, and no goal has its statement +# FALLBACK-REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean is kept in Stale/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean: its function is gone, and no goal has its statement +# FALLBACK-REMOVED-NEXT: warning: the Lean proof CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_ebbe6a6a.lean is kept in Stale/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_ebbe6a6a.lean: its function is gone, and no goal has its statement + +# PRUNE: warning: removed the 4 Lean proofs kept in Stale/, as --lean-prune-stale asks +# PRUNE-ALONE: error: --lean-prune-stale requires --lean-project or --lean-fallback + +# PARTIAL-ALL: Exported: lean fallback: bump [z3: 1 of 3 proved; lean: 3 exported] + +# STUBS: Exported: decreases: tri +# STUBS-NEXT: Exported: lean obligation: six_again +# STUBS-NEXT: Exported: lean obligation: one_again +# PARTIAL: Exported: lean fallback: bump [z3: 1 of 3 proved; lean: 2 exported] + +# MIGRATE: warning: the Lean project [[PROJECT]] pinned leanprover/lean4:v4.32.2, which an earlier release of cpp-verify wrote; it now pins leanprover/lean4:v4.35.0, so a proof that no longer builds needs updating for that Lean +# MIGRATE-NEXT: Exported: decreases: tri +# MIGRATE-NEXT: Exported: lean obligation: six +# MIGRATE-NEXT: Exported: lean obligation: one +# MIGRATE-NEXT: warning: the Lean proof CppVerify/Proofs/Goal_14843fe605ca0dfc.lean that cpp-verify 0.1 wrote for fn_5f5a336f6e6576::postcondition@15:37 is now CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd.lean +# MIGRATE-NEXT: warning: the Lean proof CppVerify/Proofs/Goal_9b7aec03175825c9.lean that cpp-verify 0.1 wrote for fn_5f5a336f6e6576::postcondition@17:37 is now CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean +# MIGRATE-NEXT: warning: the Lean proof CppVerify/Proofs/Goal_b95e8b7f774dddd4.lean that cpp-verify 0.1 wrote for fn_5f5a336f6e6576::postcondition@16:37 is now CppVerify/Proofs/cppverify_one_99bcee/cppverify_one_99bcee_postcondition_ebbe6a6a.lean +# MIGRATE-NEXT: warning: the Lean proof CppVerify/Proofs/Goal_1272763fe029af5c.lean that cpp-verify 0.1 wrote for fn_5f5a3373697876::missing-return@synthetic is now CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_missing_return_54ae7c80.lean +# MIGRATE-NEXT: warning: the Lean proof CppVerify/Proofs/Goal_b054b023e3576f6e.lean that cpp-verify 0.1 wrote for fn_5f5a3373697876::postcondition@8:37 is now CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean +# MIGRATE-NEXT: warning: the Lean proof CppVerify/Proofs/Goal_959f92a07e95a169.lean that cpp-verify 0.1 wrote for fn_5f5a3374726969::decreases::termination@4:23 is now CppVerify/Proofs/cppverify_tri_decreases_f55d4c/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean +# MIGRATE-NEXT: warning: the Lean proof CppVerify/Proofs/Goal_00000000deadbeef.lean is kept in Stale/Proofs/Goal_00000000deadbeef.lean: a proof cpp-verify 0.1 wrote for a goal this source no longer has + +# CERTIFIED: Certified: decreases: tri [backend=Lean] +# CERTIFIED-NEXT: Certified: six [backend=Lean] +# CERTIFIED-NEXT: Certified: one [backend=Lean] diff --git a/clang/test/Verify/suite/lean_project.cpp b/clang/test/Verify/suite/lean_project.cpp index 057f39a09a..51f4a7c9c6 100644 --- a/clang/test/Verify/suite/lean_project.cpp +++ b/clang/test/Verify/suite/lean_project.cpp @@ -5,15 +5,22 @@ // RUN: test -f %t.project/CppVerify/Generated.lean // RUN: test -f %t.project/CppVerify/User.lean // RUN: test -f %t.project/CppVerify/Check.lean -// RUN: test -f %t.project/CppVerify/Proofs/Goal_583ed320b83a75f8.lean -// RUN: grep -Fxq 'leanprover/lean4:v4.32.2' %t.project/lean-toolchain +// RUN: test -f %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: grep -Fxq 'leanprover/lean4:v4.35.0' %t.project/lean-toolchain // RUN: FileCheck %s --input-file=%t.project/CppVerify/Generated.lean --check-prefix=GENERATED -// RUN: grep -Fq 'import CppVerify.Proofs.Goal_583ed320b83a75f8' %t.project/CppVerify/Check.lean +// RUN: grep -Fq 'import CppVerify.Proofs.cppverify_trivial_3e4f5a.cppverify_trivial_3e4f5a_missing_return_ba8abb90' %t.project/CppVerify/Check.lean // RUN: echo '/- USER_KEEP -/' >> %t.project/CppVerify/User.lean -// RUN: echo '/- PROOF_KEEP -/' >> %t.project/CppVerify/Proofs/Goal_583ed320b83a75f8.lean +// RUN: echo '/- PROOF_KEEP -/' >> %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean // RUN: %cpp-verify --backend=lean --lean-project=%t.project %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT // RUN: grep -Fq 'USER_KEEP' %t.project/CppVerify/User.lean -// RUN: grep -Fq 'PROOF_KEEP' %t.project/CppVerify/Proofs/Goal_583ed320b83a75f8.lean +// RUN: grep -Fq 'PROOF_KEEP' %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// A project an earlier release generated moves to the current pin, and keeps +// its proofs; a pin no release wrote is the user's, and an error. +// RUN: echo 'leanprover/lean4:v4.32.2' > %t.project/lean-toolchain +// RUN: %cpp-verify --backend=lean --lean-project=%t.project %s -- 2>&1 | FileCheck %s --check-prefix=MOVED +// RUN: grep -Fxq 'leanprover/lean4:v4.35.0' %t.project/lean-toolchain +// RUN: grep -Fq 'PROOF_KEEP' %t.project/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: %cpp-verify --backend=lean --lean-project=%t.project %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT --implicit-check-not=warning // RUN: echo 'leanprover/lean4:v4.31.0' > %t.project/lean-toolchain // RUN: not %cpp-verify --backend=lean --lean-project=%t.project %s -- 2>&1 | FileCheck %s --check-prefix=PIN // RUN: not %cpp-verify --backend=lean --lean-project=%t.empty --lean-certify %S/Inputs/lean_no_obligations.cpp -- 2>&1 | FileCheck %s --check-prefix=EMPTY @@ -27,5 +34,7 @@ void trivial() // GENERATED-NOT: unchecked Lean scratch-pad // GENERATED: function: trivial // GENERATED: source: {{.*}}lean_project.cpp:{{[0-9]+:[0-9]+}} -// PIN: Lean project uses toolchain 'leanprover/lean4:v4.31.0'; expected 'leanprover/lean4:v4.32.2' +// MOVED: warning: the Lean project {{.*}}.project pinned leanprover/lean4:v4.32.2, which an earlier release of cpp-verify wrote; it now pins leanprover/lean4:v4.35.0, so a proof that no longer builds needs updating for that Lean +// MOVED-NEXT: Exported: lean obligation: trivial +// PIN: Lean project uses toolchain 'leanprover/lean4:v4.31.0'; expected 'leanprover/lean4:v4.35.0' // EMPTY: Unresolved: Lean certification requires at least one proof obligation diff --git a/clang/test/Verify/suite/lean_readable.cpp b/clang/test/Verify/suite/lean_readable.cpp new file mode 100644 index 0000000000..618ed8feb1 --- /dev/null +++ b/clang/test/Verify/suite/lean_readable.cpp @@ -0,0 +1,204 @@ +// REQUIRES: lean +// +// Each project goal also has a readable form, its assumptions as hypotheses +// named by where they come from, and a bridge from that form to the goal that +// the kernel checks with the generated file. A stub proves the goal through +// it. +// +// RUN: rm -rf %t && mkdir -p %t +// RUN: %cpp-verify --backend=lean --lean-project=%t/p %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT +// RUN: FileCheck %s --input-file=%t/p/CppVerify/Generated.lean +// RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_twice_edf933/cppverify_twice_edf933_postcondition_28de726e.lean --check-prefix=STUB +// RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_poly_c94108/cppverify_poly_c94108_postcondition_fde367c1.lean --check-prefix=LETS +// Every stub's names match its readable form: the project builds, with +// nothing admitted but the stubs. +// RUN: cd %t/p && lake build CppVerify.Check 2>&1 | FileCheck %s --check-prefix=STUBS --implicit-check-not=error +// +// Proofs that use the hypotheses by name certify. +// RUN: %cpp-verify --backend=lean --lean-project=%t/c %S/Inputs/lean_readable_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=TRUSTED +// RUN: cp %S/Inputs/lean_readable_proofs/*.lean %t/c/CppVerify/Proofs/cppverify_twice_edf933/ +// RUN: %cpp-verify --backend=lean --lean-project=%t/c --lean-certify %S/Inputs/lean_readable_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED +// +// A readable form that says less than its goal does not build: here the +// definition of b is replaced by the conclusion it should lead to. +// RUN: sed -i 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Generated.lean +// RUN: cd %t/p && not lake build CppVerify.Generated 2>&1 | FileCheck %s --check-prefix=BRIDGE + +int next(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} + +int twice(int x) + cppverify::pre(x >= 0 && x < 50) + cppverify::post(cppverify::result == x + 2) +{ + int a = next(x); + int b = next(a); + return b; +} + +int count_up(int n) + cppverify::pre(n >= 0 && n < 100) + cppverify::post(cppverify::result == n) +{ + int i = 0; + while (i < n) + cppverify::invariant(0 <= i && i <= n) + cppverify::decreases(n - i) + { + i = i + 1; + } + return i; +} + +void checked(int x) + cppverify::pre(x > 0) +{ + cppverify::check(x != 0); + cppverify::check(x >= 1); +} + +cppverify::spec int count(int n) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 0) +{ + return n <= 0 ? 0 : count(n - 1) + 1; +} + +cppverify::proof void counted(int n) + cppverify::post(count(n) + 1 > 0) +{ +} + +int positive(int x) + cppverify::post(!(x > 0) || cppverify::result > 0) +{ + return x; +} + +int read(const int *p) + cppverify::pre(cppverify::valid(p, 1)) + cppverify::post(cppverify::result == *p) +{ + return *p; +} + +int named(int x) + cppverify::pre(x >= 0 && x < 10) + cppverify::post(cppverify::result == 2 * x + 1) +{ + int h_x = x + 1; + x = x + h_x; + return x; +} + +int poly(int x) + cppverify::pre(x >= 0 && x < 10) + cppverify::post(cppverify::result == ((x + 1) * (x + 2) + (x + 3) * (x + 4)) * ((x + 5) * (x + 6) + (x + 7) * (x + 8))) +{ + return ((x + 1) * (x + 2) + (x + 3) * (x + 4)) * ((x + 5) * (x + 6) + (x + 7) * (x + 8)); +} + +// EXPORT: Exported: lean obligation: next +// EXPORT: Exported: lean obligation: twice +// EXPORT: Exported: lean obligation: count_up +// EXPORT: Exported: lean obligation: checked +// EXPORT: Exported: decreases: count +// EXPORT: Exported: lean obligation: counted +// EXPORT: Exported: lean obligation: positive +// EXPORT: Exported: lean obligation: read +// EXPORT: Exported: lean obligation: named +// EXPORT: Exported: lean obligation: poly + +// CHECK: theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b := +// CHECK-NEXT: (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl +// CHECK-NEXT: theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b := +// CHECK-NEXT: (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha)) + +// Calls of one callee are told apart; a definition is named by what it defines. +// CHECK: def cppverify_twice_edf933_postcondition_28de726e.readable : Prop := +// CHECK: (x_0 : BitVec 32), +// CHECK-NEXT: (h_pre_1 : (cppBvSle (BitVec.ofInt 32 (0)) x_0) ∧ (cppBvSlt x_0 (BitVec.ofInt 32 (50)))) → +// CHECK-NEXT: (h_null_1 : (heapSelectInt __heap_alloc_0 (0 : Int)) = (0 : Int)) → +// CHECK-NEXT: (h_null_2 : ¬(heapSelectBool __heap_live_0 (0 : Int))) → +// CHECK-NEXT: (h_call_next_1 : {{.*}} ∧ __local_call_1_1 = x_0 + (BitVec.ofInt 32 (1))) → +// CHECK-NEXT: (h_a_1 : a_1 = __local_call_1_1) → +// CHECK-NEXT: (h_call_next_2 : {{.*}} ∧ __local_call_2_1 = a_1 + (BitVec.ofInt 32 (1))) → +// CHECK-NEXT: (h_b_1 : b_1 = __local_call_2_1) → +// CHECK-NEXT: (h_result_1 : __result_1 = b_1) → +// CHECK-NEXT: ((x_0).toInt + (2 : Int) ≥ (-2147483648 : Int) ∧ (x_0).toInt + (2 : Int) ≤ (2147483647 : Int)) ∧ __result_1 = x_0 + (BitVec.ofInt 32 (2)) +// CHECK-EMPTY: +// CHECK-NEXT: theorem cppverify_twice_edf933_postcondition_28de726e.of_readable (h : cppverify_twice_edf933_postcondition_28de726e.readable) : cppverify_twice_edf933_postcondition_28de726e := +// CHECK-NEXT: fun __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 => +// CHECK-NEXT: cppverify_imp_or fun h_pre_1 => +// CHECK-NEXT: cppverify_imp_or fun h_null_1 => +// CHECK-NEXT: cppverify_not_imp_or fun h_null_2 => +// CHECK-NEXT: cppverify_imp_or fun h_call_next_1 => +// CHECK-NEXT: cppverify_imp_or fun h_a_1 => +// CHECK-NEXT: cppverify_imp_or fun h_call_next_2 => +// CHECK-NEXT: cppverify_imp_or fun h_b_1 => +// CHECK-NEXT: cppverify_imp_or fun h_result_1 => +// CHECK-NEXT: h __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 + +// A loop: its invariant, the condition of an iteration, the exact value of +// a machine operation, the value a path that skips the body keeps, and the +// exit. +// CHECK: def cppverify_count_up_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_i_1 : i_1 = (BitVec.ofInt 32 (0))) → +// CHECK-NEXT: (h_inv_1 : (cppBvSle (BitVec.ofInt 32 (0)) i_2) ∧ (cppBvSle i_2 n_0)) → +// CHECK-NEXT: (h_cond_1 : ¬__loop_choice_1 ∨ (cppBvSlt i_2 n_0)) → +// CHECK-NEXT: (h_exact_1 : ¬__loop_choice_1 ∨ {{.*}}) → +// CHECK-NEXT: (h_i_3 : ¬__loop_choice_1 ∨ i_3 = i_2 + (BitVec.ofInt 32 (1))) → +// CHECK-NEXT: (h_keep_1 : __loop_choice_1 ∨ i_3 = i_2) → +// CHECK-NEXT: (h_exit_1 : ¬__loop_choice_1) → +// CHECK-NEXT: (h_exit_2 : ¬(cppBvSlt i_2 n_0)) → +// CHECK-NEXT: (h_result_1 : __result_1 = i_2) → +// CHECK-NEXT: __result_1 = n_0 + +// A check proved before is a hypothesis of the next. +// CHECK: def cppverify_checked_{{[0-9a-f]+}}_assertion_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_null_2 : ¬(heapSelectBool __heap_live_0 (0 : Int))) → +// CHECK-NEXT: x_0 ≠ (BitVec.ofInt 32 (0)) +// CHECK: def cppverify_checked_{{[0-9a-f]+}}_assertion_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_check_1 : x_0 ≠ (BitVec.ofInt 32 (0))) → +// CHECK-NEXT: (cppBvSle (BitVec.ofInt 32 (1)) x_0) + +// A spec's proved postcondition at each application. +// CHECK: def cppverify_counted_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_spec_count_1 : (cppSpec_fn_5f5a35636f756e7469 (n_0).toInt) ≥ (0 : Int)) → +// CHECK-NEXT: (h_spec_count_2 : (cppSpec_fn_5f5a35636f756e7469 ((n_0).toInt - (1 : Int))) ≥ (0 : Int)) → + +// The postcondition's own disjunction is what remains to be shown. +// CHECK: def cppverify_positive_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_result_1 : __result_1 = x_0) → +// CHECK-NEXT: ¬(cppBvSlt (BitVec.ofInt 32 (0)) x_0) ∨ (cppBvSlt (BitVec.ofInt 32 (0)) __result_1) + +// Facts the verifier states at entry: an extent's, and where an object lies. +// CHECK: def cppverify_read_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_entry_1 : {{.*}}) → +// CHECK: (h_object_1 : p_0 = (0 : Int) ∨ {{.*}}) → + +// A hypothesis never takes a variable's name. +// CHECK: def cppverify_named_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_x_1 : BitVec 32) +// CHECK: (h_h_x_1 : h_x_1 = x_0 + (BitVec.ofInt 32 (1))) → +// CHECK: (h_x_1_1 : x_1 = x_0 + h_x_1) → + +// STUB: theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by +// STUB-NEXT: apply cppverify_twice_edf933_postcondition_28de726e.of_readable +// STUB-NEXT: intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 +// STUB-NEXT: sorry + +// A large goal names its parts, which a proof introduces too. +// LETS: intro __heap_alloc_0 __heap_live_0 __result_1 x_0 __cppverify_term_1 {{.*}} h_pre_1 h_null_1 h_null_2 + +// STUBS: Build completed successfully + +// TRUSTED: Trusted: next (contract assumed, not verified) +// TRUSTED: Exported: lean obligation: twice +// CERTIFIED: Certified: twice [backend=Lean] [trusts=next] + +// BRIDGE: Generated.lean:{{[0-9]+}}:{{[0-9]+}}: Application type mismatch: The argument diff --git a/clang/test/Verify/suite/lean_semantics.cpp b/clang/test/Verify/suite/lean_semantics.cpp index d889fb0f48..dcafd92436 100644 --- a/clang/test/Verify/suite/lean_semantics.cpp +++ b/clang/test/Verify/suite/lean_semantics.cpp @@ -20,22 +20,22 @@ // A proof that reads `(a ^ b) + 1` as `a ^ (b + 1)` must not certify the // false check of mix. // RUN: %cpp-verify --backend=lean --lean-project=%t.mix %S/Inputs/lean_semantics_mix.cpp -- -// RUN: cp %S/Inputs/lean_semantics_mix.lean %t.mix/CppVerify/Proofs/Goal_13438fdb5d10430a.lean -// RUN: sed -i.orig 's/ sorry/ trivial/' %t.mix/CppVerify/Proofs/Goal_24c3837769b840de.lean %t.mix/CppVerify/Proofs/Goal_c8f03b2a3781f844.lean +// RUN: cp %S/Inputs/lean_semantics_mix.lean %t.mix/CppVerify/Proofs/cppverify_mix_b839ab/cppverify_mix_b839ab_assertion_255467f3.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.mix/CppVerify/Proofs/cppverify_mix_b839ab/cppverify_mix_b839ab_postcondition_54ae7c80.lean %t.mix/CppVerify/Proofs/cppverify_mix_b839ab/cppverify_mix_b839ab_missing_return_54ae7c80.lean // RUN: not %cpp-verify --backend=lean --lean-project=%t.mix --lean-certify %S/Inputs/lean_semantics_mix.cpp -- 2>&1 | FileCheck %s --check-prefix=MIX // // A proof that reads `2 - 3` in Nat, where it is 0, must not certify the false // check of difference. // RUN: %cpp-verify --backend=lean --lean-project=%t.numerals %S/Inputs/lean_semantics_numerals.cpp -- -// RUN: cp %S/Inputs/lean_semantics_numerals.lean %t.numerals/CppVerify/Proofs/Goal_e9944f7458f737aa.lean -// RUN: sed -i.orig 's/ sorry/ trivial/' %t.numerals/CppVerify/Proofs/Goal_513ce39aed6c9e5f.lean %t.numerals/CppVerify/Proofs/Goal_83df1560b7290408.lean +// RUN: cp %S/Inputs/lean_semantics_numerals.lean %t.numerals/CppVerify/Proofs/cppverify_difference_465d5b/cppverify_difference_465d5b_assertion_d7e0e821.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.numerals/CppVerify/Proofs/cppverify_difference_465d5b/cppverify_difference_465d5b_missing_return_ba8abb90.lean %t.numerals/CppVerify/Proofs/cppverify_difference_465d5b/cppverify_difference_465d5b_postcondition_ba8abb90.lean // RUN: not %cpp-verify --backend=lean --lean-project=%t.numerals --lean-certify %S/Inputs/lean_semantics_numerals.cpp -- 2>&1 | FileCheck %s --check-prefix=NUMERALS // // A precondition with a quantifier, checked at a call, is certified with // `decide` on the machine comparison. // RUN: %cpp-verify --backend=lean --lean-project=%t.call %S/Inputs/lean_semantics_call.cpp -- -// RUN: cp %S/Inputs/lean_semantics_call.lean %t.call/CppVerify/Proofs/Goal_7b984a9483ff5c2f.lean -// RUN: sed -i.orig 's/ sorry/ trivial/' %t.call/CppVerify/Proofs/Goal_ac931ca361dbea89.lean %t.call/CppVerify/Proofs/Goal_e35ba922f1f42a39.lean %t.call/CppVerify/Proofs/Goal_33c547cfb1e2a227.lean +// RUN: cp %S/Inputs/lean_semantics_call.lean %t.call/CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_precondition_4e324fa2.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.call/CppVerify/Proofs/cppverify_nonnegative_5bd01c/cppverify_nonnegative_5bd01c_missing_return_ba8abb90.lean %t.call/CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_missing_return_ba8abb90.lean %t.call/CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_postcondition_ba8abb90.lean // RUN: %cpp-verify --backend=lean --lean-project=%t.call --lean-certify %S/Inputs/lean_semantics_call.cpp -- 2>&1 | FileCheck %s --check-prefix=CALL unsigned mix(unsigned a, unsigned b) @@ -148,7 +148,7 @@ int totals(int n) // LEAN: ∃ ([[K:__quant_[a-z0-9_]+]] : Int), {{.*}} ∧ ((heapSelectBv 32 __heap_0 (p_0 + [[K]] * (4 : Int))) = (BitVec.ofInt 32 (1)) ∨ [[K]] = (2 : Int)) // LEAN: ¬((∀ ({{__quant_[a-z0-9_]+}} : Int), {{.*}} = (BitVec.ofInt 32 (0))) ∧ (cppBvSlt n_0 (BitVec.ofInt 32 (100)))) // LEAN: ∨ (2 : Int) - (3 : Int) < (0 : Int) -// LEAN: (cppverify_spec_axiom_1_1 : ∀ ([[T:__quant_[a-z0-9_]+]] : Int), (cppSpec_fn_{{[0-9a-f]+}} [[T]]) = (cppSpecBody_m{{[0-9]+}}_fn_{{[0-9a-f]+}}_1 [[T]])) +// LEAN: (cppverify_spec_axiom_1_1 : ∀ ([[T:__quant_[a-z0-9_]+]] : Int), (cppSpec_fn_{{[0-9a-f]+}} [[T]]) = (cppSpecBody_{{[0-9a-f]+}}_fn_{{[0-9a-f]+}}_1 [[T]])) // MIX: Unresolved: lean obligation: mix (Lean certification failed: // MIX-NOT: Certified diff --git a/clang/test/Verify/suite/lean_toolchain.test b/clang/test/Verify/suite/lean_toolchain.test new file mode 100644 index 0000000000..d9c30df96e --- /dev/null +++ b/clang/test/Verify/suite/lean_toolchain.test @@ -0,0 +1,24 @@ +# Certification runs the Lean the project pins. Through elan, which picks a +# toolchain by the working directory, every step names the pin; a lake +# outside elan must report the pinned Lean. +# +# UNSUPPORTED: system-windows +# RUN: rm -rf %t %t.project && mkdir -p %t/elan %t/plain +# RUN: %cpp-verify --backend=lean --lean-project=%t.project %S/Inputs/lean_toolchain.cpp -- +# +# A fake elan, with lake as its proxy, records what it is asked. +# RUN: printf '#!/bin/sh\necho "$*" >> %t/elan.log\ncase "$*" in *--version*) echo "Lake version 5.0.0 (Lean version 4.35.0)";; *) exit 1;; esac\n' > %t/elan/elan +# RUN: chmod +x %t/elan/elan && ln -s elan %t/elan/lake +# RUN: not env PATH=%t/elan %cpp-verify --backend=lean --lean-project=%t.project --lean-certify %S/Inputs/lean_toolchain.cpp -- 2>&1 | FileCheck %s --check-prefix=ELAN +# RUN: FileCheck %s --input-file=%t/elan.log --check-prefix=ELAN-LOG +# +# RUN: printf '#!/bin/sh\necho "Lake version 5.0.0 (Lean version 4.1.0)"\n' > %t/plain/lake +# RUN: chmod +x %t/plain/lake +# RUN: not env PATH=%t/plain %cpp-verify --backend=lean --lean-project=%t.project --lean-certify %S/Inputs/lean_toolchain.cpp -- 2>&1 | FileCheck %s --check-prefix=PLAIN -DDIR=%t/plain + +# ELAN: Unresolved: lean obligation: trivial (Lean certification failed: command failed with exit code 1 + +# ELAN-LOG: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} +# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.Generated CppVerify.User{{$}} + +# PLAIN: Unresolved: lean obligation: trivial (Lean certification failed: the project pins leanprover/lean4:v4.35.0, but [[DIR]]/lake runs Lean 4.1.0; install elan (https://github.com/leanprover/elan), which runs the pinned toolchain) diff --git a/clang/test/Verify/version.test b/clang/test/Verify/version.test index 0031ae8249..1163bfcc5d 100644 --- a/clang/test/Verify/version.test +++ b/clang/test/Verify/version.test @@ -8,10 +8,10 @@ # RUN: printf '#!/bin/sh\necho "Lake version 5.0.0 (Lean version 4.1.0)"\n' > %t/plain/lake # RUN: chmod +x %t/plain/cvc5 %t/plain/lake # RUN: env PATH=%t/plain %cpp-verify --version | FileCheck %s --check-prefixes=HEAD,PLAIN -DDIR=%t/plain -# RUN: mkdir -p %t/match && printf '#!/bin/sh\necho "Lake version 5.0.0 (Lean version 4.32.2)"\n' > %t/match/lake +# RUN: mkdir -p %t/match && printf '#!/bin/sh\necho "Lake version 5.0.0 (Lean version 4.35.0)"\n' > %t/match/lake # RUN: chmod +x %t/match/lake # RUN: env PATH=%t/match %cpp-verify --version | FileCheck %s --check-prefixes=HEAD,MATCH -DDIR=%t/match -# RUN: printf '#!/bin/sh\necho "leanprover/lean4:v4.32.2 (default)"\n' > %t/elan/elan +# RUN: printf '#!/bin/sh\necho "leanprover/lean4:v4.35.0 (default)"\n' > %t/elan/elan # RUN: chmod +x %t/elan/elan && ln -s elan %t/elan/lake # RUN: env PATH=%t/elan %cpp-verify --version | FileCheck %s --check-prefixes=HEAD,ELAN -DDIR=%t/elan # RUN: printf '#!/bin/sh\necho "leanprover/lean4:v4.30.0 (default)"\n' > %t/elan/elan @@ -25,18 +25,18 @@ # HEAD-NEXT: {{^}} z3 {{[0-9]+\.[0-9]+\.[0-9]+}} built in ({{vendored|system}}) # NONE-NEXT: {{^}} cvc5 missing not on PATH; --backend=cvc5, portfolio, and race run it (tested with 1.1.2) -# NONE-NEXT: {{^}} lean missing lake is not on PATH; --lean-certify runs it (projects pin leanprover/lean4:v4.32.2) +# NONE-NEXT: {{^}} lean missing lake is not on PATH; --lean-certify runs it (projects pin leanprover/lean4:v4.35.0) # PLAIN-NEXT: {{^}} cvc5 9.8.7 [[DIR]]/cvc5 (tested with 1.1.2) -# PLAIN-NEXT: {{^}} lean 4.1.0 [[DIR]]/lake, but projects pin leanprover/lean4:v4.32.2 +# PLAIN-NEXT: {{^}} lean 4.1.0 [[DIR]]/lake, but projects pin leanprover/lean4:v4.35.0 # MATCH-NEXT: {{^}} cvc5 missing -# MATCH-NEXT: {{^}} lean 4.32.2 [[DIR]]/lake (projects pin leanprover/lean4:v4.32.2) +# MATCH-NEXT: {{^}} lean 4.35.0 [[DIR]]/lake (projects pin leanprover/lean4:v4.35.0) # ELAN-NEXT: {{^}} cvc5 missing -# ELAN-NEXT: {{^}} lean 4.32.2 [[DIR]]/lake (elan; projects pin leanprover/lean4:v4.32.2, installed) +# ELAN-NEXT: {{^}} lean 4.35.0 [[DIR]]/lake (elan; projects pin leanprover/lean4:v4.35.0, installed) # ELAN-MISSING-NEXT: {{^}} cvc5 missing -# ELAN-MISSING-NEXT: {{^}} lean 4.32.2 [[DIR]]/lake (elan; projects pin leanprover/lean4:v4.32.2, which elan installs on first use) +# ELAN-MISSING-NEXT: {{^}} lean 4.35.0 [[DIR]]/lake (elan; projects pin leanprover/lean4:v4.35.0, which elan installs on first use) # HEAD-NEXT: {{^}} bmc uses z3; portfolio and race use z3 and cvc5 diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 56e3ebfa58..d4c6f0b8f2 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -92,6 +92,12 @@ static cl::opt LeanCertify( cl::desc("Kernel-check every proof in --lean-project without admissions"), cl::init(false), cl::cat(CppVerifyCategory)); +static cl::opt LeanPruneStale( + "lean-prune-stale", + cl::desc("Delete the proofs a Lean project keeps in Stale/ because no " + "goal has their statement"), + cl::init(false), cl::cat(CppVerifyCategory)); + static cl::opt BMCUnroll("unroll", cl::desc("Maximum loop unroll bound for --backend=bmc"), cl::init(10), cl::cat(CppVerifyCategory)); @@ -333,6 +339,7 @@ class VerifyConsumer : public ASTConsumer { VOpts.LeanFallbackProjectPath = LeanFallback.getValue(); VOpts.LeanScope = LeanFallbackScope.getValue(); VOpts.LeanCertify = LeanCertify.getValue(); + VOpts.LeanPruneStale = LeanPruneStale.getValue(); VOpts.BMCUnroll = BMCUnroll.getValue(); VOpts.SolverTimeoutMs = SolverTimeout.getValue(); VOpts.CollectionTimeoutMs = collectionTimeoutMs(); @@ -606,7 +613,8 @@ static int replayObligationArchive() { "exclusive\n"; return 1; } - if (!LeanProject.empty() || !LeanFallback.empty() || LeanCertify) { + if (!LeanProject.empty() || !LeanFallback.empty() || LeanCertify || + LeanPruneStale) { llvm::errs() << "error: archive replay supports Lean scratch-pad export " "with --lean-out, not Lean project generation or " "certification\n"; diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 8585048b55..8391cc3d27 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1537,6 +1537,85 @@ as `a ^ (b + 1)` or `2 - 3` in `Nat`, and its probe file (`Inputs/lean_semantics_probe.lean`) states the prelude's values where C++, SMT-LIB, and Lean's own operators differ. +### Project goals and their proofs + +A project names nothing by position, so that a proof keeps every name it +uses when the source around it changes. + +- **Names.** A module's goals form a group, `cppverify__
` + (`leanProjectGroup`), `h6` from the MD5 of the function identity, which + tells overloads apart. A goal is `__`, `h8` the first + eight digits of `obligationStatementHash`: SHA-256 over the obligation's + semantics and the logical declarations it reaches, in the domain + `cppverify-obligation-statement` version 1, without the function identity + that the semantic hash includes, so a renamed function's goals keep their + hashes. Goals of one group with one hash get `_2`, `_3` in source order, + numbered over every obligation of the module whichever are exported. Spec + bodies are `cppSpecBody__...`. Before 0.2 a goal was + `..._obligation_`, its position among the function's obligations, a + body `cppSpecBody_m_...`, and its proof + `Proofs/Goal_.lean`: reordering two postconditions gave + each proof the other's goal, and inserting a function renamed the bodies + every later proof used. +- **Records.** The exporter returns a `LeanProjectGoal` for every + obligation of each module it exports, those a fallback selection leaves to + the solver marked `Exported = false`, with the 0.1 names of the goal and + its bodies. A proof file starts with a header the driver reads back + (`readLeanProof`): the goal, the stable obligation id, the full hash, the + body prefix, and the source, escaped as a Lean comment must be. +- **Regeneration** (`finalizeLeanProject`) reads the records of + `CppVerify/Proofs/` and `Stale/` and gives each exported goal, in name + order: the file at its path; else a record with its name, wherever it is + kept; else a record of the same hash whose goal is gone, from the group + with records of the most of this group's hashes (a renamed function's goals + move together), in path order; else the 0.1 file of its 0.1 name; else a + stub. A move strips the header, the notes, and the 0.1 comment, renames + the goal and the bodies throughout the text, and writes a new header. A + headerless file at a goal's path, a proof written over its stub, gets the + header. A stub never edited (`Pristine`) is never moved and is removed + when its goal is gone, as are unedited 0.1 stubs; any other record no goal + took is renamed into `Stale/` with a note: its statement changed (a goal + has its stable id), its function has no obligation with its statement, or + its function is gone. `--lean-prune-stale` then removes `Stale/`. Emptied + directories are removed, and `Check.lean` imports the exported goals. +- **Fallback runs** examine only the modules their solver leaves + unresolved. The driver records the group of every function and + termination module it gives the solver (`LeanRunGroups`); a record whose + group is among them but has no goal this run, or whose goal the run knows + but does not export, is left where it is and never moved. + +- **Readable goals.** `makeGoal` (`Obligation.cpp`) marks each `Or` it + builds, `!A || rest`, with where `A` comes from (`LogicExpr::Premise`, + like `Patterns` outside the term's meaning, its hash, and archives, and + kept by the clones and the in-place simplifier). The passivizer records + the origin of every assumption it emits (`PassiveStmt::Origin`, from a + current origin each statement kind sets and its parts refine: + `def`, `call:f`, `inv`, `cond`, `exit`, `keep`, `exact`, `check`, + `spec:f`, ...) and of each entry assumption (`PassiveProgram::EntryOrigins`: + `pre` for a written precondition, `entry` for a generated one, `null`, + `object`); spec checks built elsewhere default to `fact`. The Lean adapter + peels the marked chain into `G.readable`: `∀ vars axioms, let …; (h_pre_1 + : A1) → … → C`, a hypothesis being the operand its `Or` negates (or `¬B` + where simplification folded `¬¬B` to `B`), named `h__`, a + definition `h_`, never a binder's name; its `let`s are the large + subterms of the hypotheses and the conclusion. The bridge + `G.of_readable : G.readable → G` is a term, one prelude lemma per + hypothesis (`cppverify_imp_or : (a → b) → ¬a ∨ b`, or + `cppverify_not_imp_or : (¬a → b) → a ∨ b`), so the kernel checks with + `Generated.lean` that the readable form implies the goal: a printer bug in + it fails the build, never certifies. `LeanProjectGoal::Intros` gives the + stub its `intro` list. On the 375 suite exports, the 351 that built + before still build, with every bridge. + +`lean_readable.cpp` checks the readable form of each kind of assumption, +the bridge, the stubs (every one builds), a proof by hypothesis names that +certifies, and a readable form that says less than its goal, which fails at +its bridge. `lean_identity.test` walks one project through each case (insertion and +reordering, renames of two functions at once, a changed statement, a removed +function and its return, fallback runs, pruning, and a 0.1 project with +proofs, stubs, and a proof of a goal that is gone) and certifies it after +the renames and the migration. + ## Counterexample Extraction When Z3 returns SAT, CppVerify evaluates source-attributed SSA variables without @@ -1662,6 +1741,16 @@ The driver selects a backend via `VerifyOptions` (`Verifier.h` / `cpp-verify --b | **BMC** | `LoopUnroll` on VCR, then shared obligation/Z3 path | Source verification grows bounds from zero through `--unroll=N`, stopping on a counterexample, complete unwinding, unresolved query, or the maximum frontier. Safety with failed unwinding is `BoundedSafe(N)`; only proved unwinding is `Verified`. A spec's checks have no loops: the driver solves them with a Z3 backend (`SpecBackend`), as on the default path, and keeps the bound on their archived modules for replay. | | **Lean** | `exportLeanScratchPad` / project certification | Standalone mode emits unchecked theorem stubs. Project mode emits direct source goals, total functional heaps, typed bit-vector/integer operations, and compact finite-fuel spec bodies into generated files while preserving user proofs. Export is `Exported`; only the pinned admission-free kernel/axiom check is `Certified`. Collections are `logic.unsupported` (planned for a future release). | +A Lean project pins `LeanToolchain` (`Driver/CppVerifyVersion.h`) in its +`lean-toolchain` file. A pin in `EarlierLeanToolchains`, which an earlier +release wrote, is rewritten to the current one with a warning; any other pin is +an error, since the generated semantics are written for one Lean. elan picks a +toolchain by the working directory, not by `--dir`, so through elan's proxy +every certification step names the pin (`lake +leanprover/lean4:v4.35.0 +--dir=DIR ...`). Certification first asks `lake --version`, alone, since lake +takes it alone, and refuses a `lake` that reports another Lean. Before 0.2, +certification ran elan's default toolchain. + Each backend declares supported `LogicFeature`s. Central dispatch rejects a module requiring an unavailable feature before backend execution. Spec inlining runs before passivization: `SpecInliner::prepareFunctionAxiomatic` @@ -2034,7 +2123,7 @@ stops before VCR conversion. `CPPVERIFY_PARITY_ARCHIVES` it also compares encodings per archived obligation. - Runner: `scripts/run-verify-tests.sh`. - Backend fidelity gate: `clang/test/Verify/suite/backend_fidelity_gate.test` - requires cvc5 and pinned Lean 4.32.2 and runs the permanent differential + requires cvc5 and pinned Lean 4.35.0 and runs the permanent differential matrix under every machine-integer encoding. - Instrumented coverage: `scripts/coverage-verify.sh` (region target on `clang/lib/Verify`). @@ -2064,7 +2153,7 @@ an unchecked support table: | Quantifiers and finite-fuel specs | Both quantifier kinds, recursive spec calls, and conservative `unknown` rather than false proof | | Frontend-derived semantics | Type invariants and complete-loop Z3/BMC parity | | Portable artifacts | Source-stable obligation IDs, canonical/BMC archive replay, and deterministic parallel results | -| Lean | Source/archive theorem identity, stable proof-module hashes, generated-file kernel build, and bounds instrumentation | +| Lean | Source/archive obligation identity, one proof file per project goal recording its statement hash, generated-file kernel build, and bounds instrumentation | | Advisory checks | `cppverify::recommends` warnings stay source-only and never enter BMC or Lean replay artifacts | An approved valid quantified or inductive query may remain diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 9fd7d50dc7..124ba4bd64 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1877,14 +1877,40 @@ type, a Boolean is a proposition, and machine division by zero is SMT-LIB's, as the certifier (ARCHITECTURE.md, "Lean Encoding"). A unit test checks that Lean's evaluation agrees with the certifier on random ground terms and on every operator at its extreme operands. Standalone output is an unchecked scratch-pad. -Editable project mode pins Lean 4.32.2, overwrites only generated semantics and +Editable project mode pins Lean 4.35.0 (`LeanToolchain`), overwrites only generated semantics and the active check module, and preserves reusable user lemmas and one proof file -per stable obligation goal. Initial generation is `Exported`. Certification +per goal. A goal is named by its function and its statement, never by a +position: `cppverify__
__`, where `h6` hashes the +function's identity (overloads) and `h8` begins the SHA-256 hash of the +obligation's statement, its goal with the logical declarations it uses and +without the function's identity; identical goals of one function get `_2`, +`_3` in source order. Spec bodies are named by the function too. A proof file, +`CppVerify/Proofs//.lean`, records the goal, its obligation, +the full hash, and the prefix of the spec bodies, and every regeneration +gives each goal the proof of its statement, as Frama-C's WP keeps one script +per goal and Vermilion keys a proof by the hash of its statement: the file at +its path; else a proof recorded with its name, from `Stale/` too; else one of +a goal that is gone, from the function with proofs of the most of this one's +goals (a rename), moved with the generated names it uses; else a 0.1 file +`Goal_.lean` of its 0.1 name, migrated the same way; else a stub. A +proof no goal takes is kept in `Stale/` with a note naming why, and an +unedited stub is removed; nothing else is ever deleted unless +`--lean-prune-stale` asks. A fallback run examines only what its solver +leaves unresolved and leaves every other proof where it is. Each goal `G` +also has a readable form `G.readable`, its assumptions as hypotheses named +by where they come from (as Frama-C's WP labels the steps of a sequent and +Vermilion names its hypotheses), and a bridge `G.of_readable : G.readable → +G`, generated and kernel-checked with the generated file: the canonical goal +stays what certification checks and identity hashes, and a printer bug in +the readable form cannot certify anything. A stub applies the bridge and +introduces every name. Initial generation is `Exported`. Certification compiles the user module and every active proof with `sorry` as an error, then checks aggregate theorem types and axiom dependencies. Only foundational Lean axioms are permitted; user `axiom`/`opaque` proof shortcuts, stale proof types, missing proofs, malformed output, and toolchain failures remain `Unresolved`. -Only complete success is `Certified`. +Only complete success is `Certified`. Certification runs the pinned toolchain +whatever elan's default is, and a project pinned by an earlier release moves to +the current pin with a warning; any other pin is an error. `--check-ub` extent instrumentation is applied before all Z3, cvc5, portfolio, BMC, and Lean obligation construction. Direct Lean export and canonical archive diff --git a/website/source/book/part-ii/ch16-when-verification-fails.rst b/website/source/book/part-ii/ch16-when-verification-fails.rst index 60dc3e2c66..40b383dfaa 100644 --- a/website/source/book/part-ii/ch16-when-verification-fails.rst +++ b/website/source/book/part-ii/ch16-when-verification-fails.rst @@ -402,7 +402,7 @@ For automation that remains unresolved, use: .. code-block:: bash cpp-verify --lean-fallback=proof file.cpp - # edit proof/CppVerify/User.lean and proof/CppVerify/Proofs/*.lean + # edit proof/CppVerify/User.lean and proof/CppVerify/Proofs/*/*.lean cpp-verify --lean-fallback=proof --lean-certify file.cpp The first command remains non-success because export is not proof. It exports diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 3222c7f82c..4f14e14faa 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -95,7 +95,7 @@ exist: ninja -C build FileCheck not count split-file llvm-config ./build/bin/llvm-lit -sv clang/test/Verify/suite/backend_fidelity_gate.test -It requires cvc5 and Lean 4.32.2. The gate checks every canonical feature +It requires cvc5 and Lean 4.35.0. The gate checks every canonical feature family through Layer 3 and Z3/cvc5/portfolio/BMC, source-identical failures, deterministic parallel execution, canonical and bounded archive replay, Lean theorem/proof-module identity and generated-file compilation, and that @@ -153,12 +153,16 @@ For an explicit interactive proof: .. code-block:: bash cpp-verify --backend=lean --lean-project=proof file.cpp - # complete proof/CppVerify/Proofs/*.lean; put shared lemmas in User.lean + # complete proof/CppVerify/Proofs/*/*.lean; put shared lemmas in User.lean cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp ``Generated.lean`` and ``Check.lean`` are machine-owned. -``User.lean`` and existing per-obligation proof files are never overwritten. -The project pins ``leanprover/lean4:v4.32.2``. Certification compiles the user +``User.lean`` is never overwritten, and each goal has a proof file of its own, +which cpp-verify never rewrites but moves with its goal (see `Proofs that +follow their goals`_ below). +The project pins ``leanprover/lean4:v4.35.0``, which certification runs whatever +elan's default toolchain is; a project 0.1 generated, pinned to ``v4.32.2``, moves to +it with a warning. Certification compiles the user module and every active proof with admissions promoted to errors, checks the aggregate module, and rejects proof dependencies other than Lean's documented foundational axioms. @@ -210,7 +214,7 @@ goals, three of them ``True``. The one for the call reads: .. code-block:: lean4 - def cppverify_small_fn_5f5a35736d616c6c76_obligation_1_goal : Prop := + def cppverify_small_74ff94_precondition_4e324fa2 : Prop := ∀ (__heap_alloc_0 : CppHeap) (__heap_live_0 : CppHeap), @@ -221,15 +225,16 @@ show. The first two facts describe the null pointer (no object owns address 0, and none is live with identity 0); the third is that evaluating the precondition at ``n = 3`` is defined; the last disjunct is the precondition there, the quantifier for every ``k`` in ``[0, 3)`` and ``3 < 8``. Its proof file, -``proof/CppVerify/Proofs/Goal_7b984a9483ff5c2f.lean``, proves that disjunct: +``proof/CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_precondition_4e324fa2.lean``, +proves that disjunct: .. code-block:: lean4 import CppVerify.User - theorem cppverify_small_fn_5f5a35736d616c6c76_obligation_1_goal_proof : - cppverify_small_fn_5f5a35736d616c6c76_obligation_1_goal := by - unfold cppverify_small_fn_5f5a35736d616c6c76_obligation_1_goal + theorem cppverify_small_74ff94_precondition_4e324fa2_proof : + cppverify_small_74ff94_precondition_4e324fa2 := by + unfold cppverify_small_74ff94_precondition_4e324fa2 intro _ _ have zero : (BitVec.ofInt 32 0).toInt = 0 := by decide exact Or.inr (Or.inr (Or.inr ⟨fun _ range => by rw [zero] at range; omega, by decide⟩)) @@ -265,9 +270,9 @@ proof. When every exported goal kernel-checks the function is ``"status":"mixed-proof"`` with the per-obligation split. When Lean checked every obligation, because ``--lean-fallback-scope=all`` exported them all or the solver proved none on its own, the function is ``Certified``. SAT counterexamples are failures, not -fallback candidates. Regeneration may leave old proof files on disk, but only -the current source obligations are imported and certified; a stale active proof -must type-check against the regenerated goal. +fallback candidates. A fallback run examines in Lean only what its solver +leaves unresolved, so the proofs of the obligations and functions the solver +settles stay where they are until Lean needs them again. A Lean proof proves the goals it covers, and the verdict built from it rests on the same facts as a solver's: the contracts of the functions it calls and @@ -304,6 +309,165 @@ one does (``[trusts=f]``, ``[partial]``). It also gets the same vacuity checks, run with Z3: a goal that holds only because no execution reaches it is ``Certified: f [backend=Lean] [vacuous]``, with a warning. +Goals as hypotheses +~~~~~~~~~~~~~~~~~~~ + +Next to each goal, ``Generated.lean`` states it as hypotheses and a +conclusion. Each hypothesis is an assumption the goal makes, named by where +it comes from, and a bridge from that form to the goal is proved in the same +file. For this file: + +.. code-block:: cpp + + [[cppverify::trusted]] int next(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1); + + int twice(int x) + cppverify::pre(x >= 0 && x < 50) + cppverify::post(cppverify::result == x + 2) + { + int a = next(x); + int b = next(a); + return b; + } + +the postcondition of ``twice`` reads: + +.. code-block:: lean4 + + def cppverify_twice_edf933_postcondition_28de726e.readable : Prop := + ∀ + (__heap_alloc_0 : CppHeap) + (__heap_live_0 : CppHeap) + (__local_call_1_1 : BitVec 32) + (__local_call_2_1 : BitVec 32) + (__result_1 : BitVec 32) + (a_1 : BitVec 32) + (b_1 : BitVec 32) + (x_0 : BitVec 32), + (h_pre_1 : (cppBvSle (BitVec.ofInt 32 (0)) x_0) ∧ (cppBvSlt x_0 (BitVec.ofInt 32 (50)))) → + (h_null_1 : (heapSelectInt __heap_alloc_0 (0 : Int)) = (0 : Int)) → + (h_null_2 : ¬(heapSelectBool __heap_live_0 (0 : Int))) → + (h_call_next_1 : ((x_0).toInt + (1 : Int) ≥ (-2147483648 : Int) ∧ (x_0).toInt + (1 : Int) ≤ (2147483647 : Int)) ∧ __local_call_1_1 = x_0 + (BitVec.ofInt 32 (1))) → + (h_a_1 : a_1 = __local_call_1_1) → + (h_call_next_2 : ((a_1).toInt + (1 : Int) ≥ (-2147483648 : Int) ∧ (a_1).toInt + (1 : Int) ≤ (2147483647 : Int)) ∧ __local_call_2_1 = a_1 + (BitVec.ofInt 32 (1))) → + (h_b_1 : b_1 = __local_call_2_1) → + (h_result_1 : __result_1 = b_1) → + ((x_0).toInt + (2 : Int) ≥ (-2147483648 : Int) ∧ (x_0).toInt + (2 : Int) ≤ (2147483647 : Int)) ∧ __result_1 = x_0 + (BitVec.ofInt 32 (2)) + +The names say where each assumption comes from: + +- ``h_pre_``: a precondition the function states; ``h_entry_``: one + the verifier adds, such as an extent's; ``h_null_`` and + ``h_object_``: the null object and where an object lies; +- ``h_``: the definition of that variable, here ``a_1`` and + ``b_1`` and the value returned, ``__result_1``; +- ``h_call__``: what a call of the callee gives, numbered in + order, here both calls of ``next``; +- ``h_inv_``, ``h_cond_``, ``h_exit_``: a loop's invariant, the + condition of an iteration, and how it ended; +- ``h_exact_``: the exact value of a machine operation that does not + overflow; ``h_keep_``: the value of a variable on a path that skips its + assignment; +- ``h_check_``: a ``cppverify::check`` proved before; + ``h_spec__``: a spec's proved postcondition at an application. + +The numbers count within the goal, so a line added to the source renames no +hypothesis. A disjunction the program wrote, such as +``cppverify::post(!(x > 0) || cppverify::result > 0)``, stays in the +conclusion. The bridge, +``cppverify_twice_edf933_postcondition_28de726e.of_readable``, proves the goal +from this form; Lean checks it when it builds the generated file, so a +readable form that said less than its goal would fail there, not certify. A +new proof file starts from it, with every name introduced: + +.. code-block:: lean4 + + import CppVerify.User + + theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by + apply cppverify_twice_edf933_postcondition_28de726e.of_readable + intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 + sorry + +and a proof uses the hypotheses by name: + +.. code-block:: lean4 + + obtain ⟨_, first⟩ := h_call_next_1 + obtain ⟨_, second⟩ := h_call_next_2 + subst h_result_1 h_b_1 second h_a_1 first + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + refine ⟨by omega, ?_⟩ + rw [BitVec.add_assoc] + rfl + +With the two calls' preconditions proved the same way and ``trivial`` for +the return check, +``cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp`` +prints: + +.. code-block:: text + + file.cpp:1:28: Trusted: next (contract assumed, not verified) + Certified: twice [backend=Lean] [trusts=next] + +A proof of the goal itself, as the one for ``small`` above, checks as well. + +Proofs that follow their goals +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A goal is named by its function and its statement, never by its position: +``cppverify_small_74ff94_precondition_4e324fa2`` is the ``precondition`` +obligation of ``small``, ``74ff94`` from the function's identity (which tells +overloads apart), and ``4e324fa2`` the first digits of the hash of what the +goal states, with the definitions it uses. A goal identical to another of +its function gets ``_2``. Its proof lives in a directory per function, +``CppVerify/Proofs/cppverify_small_74ff94/``, and starts with a header that +records the goal, the obligation, and the full hash. Reordering clauses or +adding functions changes no statement, so every proof stays where it is. + +Each run puts every proof with the goal of its statement. Renaming ``small`` +of the example above to ``tiny`` moves its proofs, with the names they use, +and they certify again: + +.. code-block:: text + + Certified: nonnegative [backend=Lean] + Certified: tiny [backend=Lean] + warning: the Lean proof of fn_5f5a3474696e7976::missing-return@synthetic moved from CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_missing_return_ba8abb90.lean to CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_missing_return_ba8abb90.lean, the file of the goal with its statement + warning: the Lean proof of fn_5f5a3474696e7976::postcondition@7:19 moved from CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_postcondition_ba8abb90.lean to CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_postcondition_ba8abb90.lean, the file of the goal with its statement + warning: the Lean proof of fn_5f5a3474696e7976::precondition@9:3 moved from CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_precondition_4e324fa2.lean to CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_precondition_4e324fa2.lean, the file of the goal with its statement + +A changed statement never gets the old proof. With ``nonnegative(4)`` in +place of ``nonnegative(3)``, the precondition's goal is a new one, which gets +a stub, and the old proof is kept: + +.. code-block:: text + + Exported: lean obligation: nonnegative + Exported: lean obligation: tiny + warning: the Lean proof CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_precondition_4e324fa2.lean is kept in Stale/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_precondition_4e324fa2.lean: the statement of fn_5f5a3474696e7976::precondition@9:3 changed; its goal is now cppverify_tiny_de8a22_precondition_2596f63f + +The kept file ends with that note. The proof comes back by itself once a goal +has its statement again, as it would if the call were ``nonnegative(3)`` +again, and so do the proofs of a function that is removed and later +restored. A stub nobody edited is simply removed. Nothing else is ever +deleted: ``--lean-prune-stale`` deletes what ``Stale/`` keeps, once the run +has taken back what it needs (``warning: removed the 4 Lean proofs kept in +Stale/, as --lean-prune-stale asks``). + +A project 0.1 generated, with its ``Proofs/Goal_*.lean`` files, moves to these +names the next time cpp-verify writes it: each proof moves to the file of its +goal, with the goal and the spec definitions it names renamed, and a warning +such as ``warning: the Lean proof CppVerify/Proofs/Goal_b054b023e3576f6e.lean +that cpp-verify 0.1 wrote for fn_5f5a3373697876::postcondition@8:37 is now +CppVerify/Proofs/cppverify_six_6a2cf3/cppverify_six_6a2cf3_postcondition_198bc076.lean``. +A 0.1 proof of a goal the source no longer has is kept in ``Stale/``. + Portable obligation archives ---------------------------- diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 0261fc53a7..38d255fdf4 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -152,7 +152,12 @@ release it is built on, and each backend: the Z3 linked into it, and the cvc5 an (``lake``) it finds on ``PATH`` with their versions. cvc5 is tested with 1.1.2 and also works with 1.4: a query that needs a constant array, as every one over sets, multisets, and maps does, sets cvc5's ``arrays-exp`` option itself, which 1.4 requires. Every Lean -project pins ``leanprover/lean4:v4.32.2``. +project pins ``leanprover/lean4:v4.35.0``, and certification runs that toolchain whatever +elan's default is: through elan it names the pin, since elan otherwise picks a toolchain +by the working directory, and a ``lake`` outside elan must report the pinned Lean. A +project an earlier release generated, pinned to ``leanprover/lean4:v4.32.2`` by 0.1, is +moved to the current pin the next time cpp-verify writes it, with a warning; a proof that +no longer builds needs updating for the new Lean. Any other pin is an error. Options that select a backend, and options a run would not use ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -195,6 +200,8 @@ nothing is verified: - ``error: --proof-cache-max-mb and --proof-cache-max-entries require --proof-cache`` * - ``--lean-fallback-scope=all`` without ``--lean-fallback`` - ``error: --lean-fallback-scope requires --lean-fallback`` + * - ``--lean-prune-stale`` without ``--lean-project`` or ``--lean-fallback`` + - ``error: --lean-prune-stale requires --lean-project or --lean-fallback`` Lean export runs no solver, so every solver option is an error with ``--backend=lean``, ``--lean-out``, or ``--lean-project``, the same way as @@ -258,7 +265,22 @@ Backends * - ``--lean-project=DIR`` - With ``--backend=lean``, which it selects, generate a pinned editable project. Generated semantics live in ``CppVerify/Generated.lean``; reusable lemmas and - per-obligation proof files are preserved across regeneration. Each + per-obligation proof files are preserved across regeneration. A goal + is named by its function and the hash of its statement + (``cppverify_one_99bcee_postcondition_cd6bdfcd``), and its proof file, + ``CppVerify/Proofs//.lean``, records that hash, so a + proof stays with its statement: it moves with a renamed function, + a proof whose statement changed or whose function is gone is kept in + ``Stale/`` with a note, and it comes back when a goal has its + statement again. A warning names every move. A project 0.1 generated + is moved to these names, with the names its proofs use + (:doc:`../book/part-ii/ch17-backends-modular-calls`). Each goal + ``G`` also has a readable form, ``G.readable``, its assumptions as + hypotheses named by where they come from (``h_pre_1``, + ``h_call_next_2``, ``h_x_1`` for the definition of ``x_1``), and a + bridge ``G.of_readable : G.readable → G`` that the kernel checks with + the generated file, so a proof of either form proves ``G``. A stub + applies the bridge and introduces every name. Each goal means what its obligation means: every operator keeps its grouping under Lean's precedence, a numeral has its type (``Nat`` would read ``2 - 3`` as 0), a Boolean is a proposition @@ -267,7 +289,7 @@ Backends ``decide`` evaluates the machine comparisons at constants (:doc:`../book/part-ii/ch17-backends-modular-calls`). * - ``--lean-certify`` - - Build the active project with Lean 4.32.2, reject ``sorry`` and + - Build the active project with the pinned Lean 4.35.0, reject ``sorry`` and undocumented proof axioms, and report ``Certified`` only after every active proof kernel-checks. Certification runs whatever else failed, before the facts verdicts rest on are settled: a result proved in @@ -287,7 +309,15 @@ Backends - ``unproved`` (default) exports only the obligations the solver did not prove individually; each keeps the goal name it has in a complete export. ``all`` exports every obligation of the function, so success - is ``Certified``. Requires ``--lean-fallback``. + is ``Certified``. Requires ``--lean-fallback``. A fallback run + examines in Lean only what its solver leaves unresolved, so it leaves + the proofs of the other obligations and functions where they are. + * - ``--lean-prune-stale`` + - Delete the proofs a Lean project keeps in ``Stale/``, after the + regeneration has taken back those a goal has the statement of: + ``warning: removed the 4 Lean proofs kept in Stale/, as + --lean-prune-stale asks``. Without it, nothing is ever deleted but an + unedited stub. Requires ``--lean-project`` or ``--lean-fallback``. * - ``--unroll=N`` - Maximum BMC loop bound, which selects ``--backend=bmc``. Source verification explores ``0..N``; lower-only and archive replay retain one exact recorded bound, diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index ab305ce360..f3cbd5c605 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -279,6 +279,42 @@ queries (:doc:`language/tooling`). which requires extended arrays for constant arrays; such a query now enables them itself (:doc:`language/tooling`). +**Lean proofs stay with their goals.** A goal of a Lean project was named by +its function and its position among the function's obligations, and a spec +body by the position of its module in the file. Reordering two +postconditions gave each proof the other's goal, which the kernel rejected, +and a function inserted earlier in the file renamed the spec bodies every +later proof unfolds. A renamed function lost its proofs, and proofs of goals +that were gone stayed among the proof files. A goal is now named by its +function and the hash of its statement, its proof file lives in the +function's directory and records that hash, and every regeneration puts +each proof with the goal of its statement: a renamed function takes its +proofs along with the names they use, a proof whose statement changed or +whose function is gone is kept in ``Stale/`` with a note, and it comes back +when a goal has its statement again. A fallback run leaves the proofs of +what its solver settles alone. ``--lean-prune-stale`` deletes what +``Stale/`` keeps. A project 0.1 generated is moved to the new names with +its proofs (:doc:`book/part-ii/ch17-backends-modular-calls`). + +**Lean goals as hypotheses.** A Lean goal was one disjunction, the negation of +every assumption before what it must show, and a proof picked its way to the +conclusion by counting disjuncts (``right; right; right``) with nothing to +say which was the precondition and which a callee's postcondition. Each goal +now also has a readable form, its assumptions as hypotheses named by where +they come from, such as ``h_pre_1``, ``h_call_next_2``, ``h_inv_1``, or +``h_x_1`` for the definition of ``x_1``, and a bridge from that form to the +goal, which the kernel checks with the generated file. A new proof file +starts from the readable form with every name introduced; a proof of the +goal itself still checks (:doc:`book/part-ii/ch17-backends-modular-calls`). + +**Lean 4.35.0.** Lean projects pin ``leanprover/lean4:v4.35.0``. A project 0.1 +generated, pinned to ``v4.32.2``, moves to the new pin the next time cpp-verify +writes it, with a warning; a proof that no longer builds needs updating for that +Lean. Certification ran elan's default toolchain, which need not be the pin, +since elan picks one by the working directory. It now names the pin, and +refuses a ``lake`` outside elan that reports another Lean +(:doc:`language/tooling`). + **clang-format.** A range footprint is written ``p[lo : n]``, not ``p [lo:n]`` (:doc:`language/tooling`). @@ -288,7 +324,9 @@ Data formats Archives stay ``cppverify.obligation/2`` and JSON diagnostics ``cppverify.diagnostic/1``. JSON records may carry the status ``proved-obligations`` (archive replay) and the reason ``interrupted`` -(Ctrl-C). +(Ctrl-C). Lean projects pin ``leanprover/lean4:v4.35.0``, and each proof +file records the hash of its goal's statement (``cppverify-obligation-statement`` +version 1, which leaves out the function's identity). 0.1.1 -----