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..5cbb3ee19f 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); } @@ -899,7 +928,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 +940,23 @@ VerifyResult verify::exportLeanScratchPad( LeanEmissionFailed = false; LeanLogicFunctions = &Module.LogicFunctions; - LeanBodyPrefix = "cppSpecBody_m" + std::to_string(ModuleIndex) + "_"; + // A project names everything by identity, never by position, so that a + // proof keeps the names it uses when the source around it changes. + const std::string LegacyBodyPrefix = + "cppSpecBody_m" + std::to_string(ModuleIndex) + "_"; + LeanBodyPrefix = LegacyBodyPrefix; + std::string Group; + if (ProjectGoals) { + Group = leanProjectGroup(Module); + LeanBodyPrefix = + "cppSpecBody_" + leanShortHash(Module.FunctionIdentity, 8) + "_"; + // Modules of one identity (an archive's) are told apart in order. + for (unsigned Copy = 2; !EmittedTheorems.insert(LeanBodyPrefix).second; + ++Copy) + LeanBodyPrefix = "cppSpecBody_" + + leanShortHash(Module.FunctionIdentity, 8) + "_" + + std::to_string(Copy) + "_"; + } if (EmitPreamble) { if (ProjectGoals) { @@ -988,8 +1033,38 @@ VerifyResult verify::exportLeanScratchPad( unsigned Index = 0; for (const Obligation &Item : Module.Obligations) { ++Index; - if (Selection && !Selection->count(Item.Id)) + const bool Selected = !Selection || Selection->count(Item.Id); + if (!Selected && !ProjectGoals) continue; + std::string ObligationName = + TheoremName + "_obligation_" + std::to_string(Index); + LeanProjectGoal Goal; + if (ProjectGoals) { + Goal.Hash = obligationStatementHash(Module, Item); + Goal.Name = Group + "_" + + leanIdentifierPart(obligationKindName(Item.Kind)) + "_" + + Goal.Hash.substr(0, 8); + // Identical obligations of one function, in source order, whichever + // of them are exported. + const std::string Base = Goal.Name; + for (unsigned Copy = 2; !EmittedTheorems.insert(Goal.Name).second; ++Copy) + Goal.Name = Base + "_" + std::to_string(Copy); + Goal.Group = Group; + Goal.StableId = Item.StableId.empty() ? Item.Id : Item.StableId; + if (Item.Source.isValid()) { + llvm::raw_string_ostream SourceOS(Goal.Source); + printLeanCommentText(Item.Source.File, SourceOS); + SourceOS << ":" << Item.Source.Line << ":" << Item.Source.Column; + } + Goal.BodyPrefix = LeanBodyPrefix; + Goal.LegacyName = encodeLeanName(ObligationName + "_goal"); + Goal.LegacyBodyPrefix = LegacyBodyPrefix; + Goal.Exported = Selected; + if (!Selected) { + ProjectGoals->push_back(std::move(Goal)); + continue; + } + } OS << "/- obligation: "; printLeanCommentText(Item.StableId.empty() ? Item.Id : Item.StableId, OS); OS << "\n"; @@ -1004,12 +1079,9 @@ VerifyResult verify::exportLeanScratchPad( OS << "unknown"; } OS << " -/\n"; - std::string ObligationName = - TheoremName + "_obligation_" + std::to_string(Index); if (ProjectGoals) { - ObligationName += "_goal"; - emitLeanGoalDefinition(ObligationName, Item.Goal.get(), OS); - ProjectGoals->push_back(encodeLeanName(ObligationName)); + emitLeanGoalDefinition(Goal.Name, Item.Goal.get(), OS); + ProjectGoals->push_back(std::move(Goal)); } else { emitLeanTheorem(ObligationName, Item.Goal.get(), OS); } diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h index 815cdeadd6..2eb17d5843 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -11,14 +11,41 @@ namespace clang { namespace verify { -/// Selection names the internal IDs to export; an exported goal keeps the -/// positional name it has when every obligation is exported. +/// A goal of an editable Lean project, with what identifies it across +/// regenerations: the semantic hash of its obligation. Its proof file lives in +/// the directory of its function's group. +struct LeanProjectGoal { + std::string Name; + std::string Group; + std::string StableId; + std::string Hash; + /// Where its obligation is, as a Lean comment may hold it. + std::string Source; + /// The prefix of the spec bodies its goal may unfold. + std::string BodyPrefix; + /// The names 0.1 gave the goal and its spec bodies, which a project 0.1 + /// generated still uses. + std::string LegacyName; + std::string LegacyBodyPrefix; + /// False for an obligation of an exported function that a selection left + /// to the solver: its goal is known, but has no definition or proof file. + bool Exported = true; +}; + +/// The group of a module's goals in a project: its function's directory. +std::string leanProjectGroup(const ObligationModule &Module); + +/// Selection names the internal IDs to export; a project goal is named by +/// its function and semantic hash, so it keeps its name whatever else is +/// exported, and a scratch-pad goal keeps the positional name it has when +/// every obligation is exported. A project records every goal of the module, +/// the ones left out as not exported. VerifyResult exportLeanScratchPad(const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, std::set &EmittedFunctions, std::set &EmittedTheorems, unsigned ModuleIndex, - std::vector *ProjectGoals, + std::vector *ProjectGoals, const std::set *Selection = nullptr); class LeanVerifyBackend : public VerifyBackend { @@ -27,12 +54,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/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/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..e83231923b 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,131 @@ 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; +}; + +static std::string leanProofStub(llvm::StringRef Goal) { + return "import CppVerify.User\n\ntheorem " + Goal.str() + + "_proof : " + Goal.str() + " := by\n sorry\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 && + Text.substr(End + 3) == leanProofStub(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 +1556,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 +1600,256 @@ 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))) + 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 +1861,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 +1924,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 +2084,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 +2188,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 +2998,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 +3273,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 +3587,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 +3612,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/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_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..c3ce4fd105 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/ simp [cppverify_trivial_3e4f5a_missing_return_ba8abb90]/' %t.certified/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: sed -i.orig 's/ sorry/ simp [cppverify_trivial_3e4f5a_postcondition_ba8abb90]/' %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/ simp [cppverify_trivial_3e4f5a_missing_return_ba8abb90]/' %t.stale/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: sed -i.orig 's/ sorry/ simp [cppverify_trivial_3e4f5a_postcondition_ba8abb90]/' %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_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..62c523ef13 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1537,6 +1537,59 @@ 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. + +`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 +1715,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 +2097,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 +2127,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..b8c62faf8f 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1877,14 +1877,34 @@ 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. 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..2fe0cb898f 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,57 @@ 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. +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..47f4b1caca 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,16 @@ 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 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 +283,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 +303,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..11fd40656e 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -279,6 +279,31 @@ 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 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 +313,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 -----