From c2a2a5766890f6367dc15d553c22d6c8a763e793 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:18 +0530 Subject: [PATCH 01/99] verify: Pin Lean 4.35.0, and name the pins earlier releases wrote. --- clang/lib/Verify/Driver/CppVerifyVersion.h | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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"; From c62d0046e058dcdcc69e9159c6667f766813a46c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:19 +0530 Subject: [PATCH 02/99] verify: Move a project an earlier release pinned to the current Lean, and certify with the pinned toolchain. --- clang/lib/Verify/Driver/Verifier.cpp | 64 ++++++++++++++++++++++++---- 1 file changed, 56 insertions(+), 8 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 00611d0595..9fbcb47aa3 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -1430,13 +1430,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); } @@ -1500,14 +1513,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) From 73fb7cf7e9e12a934a3729cab7641d6bdcb13933 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:19 +0530 Subject: [PATCH 03/99] verify: Install Lean 4.35.0 in CI. --- .github/workflows/cppverify-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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: From 3219cf3fa1d45ae277a2f0f1f461a5a1a7bb3064 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:19 +0530 Subject: [PATCH 04/99] test: Expect the Lean 4.35.0 pin in the version report. --- clang/test/Verify/version.test | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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 From 514b7402f23d8700c3083af124d174570f8383b0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:20 +0530 Subject: [PATCH 05/99] test: Check that a project an earlier release pinned moves to the current pin. --- clang/test/Verify/suite/lean_project.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/lean_project.cpp b/clang/test/Verify/suite/lean_project.cpp index 057f39a09a..ae95a61cb6 100644 --- a/clang/test/Verify/suite/lean_project.cpp +++ b/clang/test/Verify/suite/lean_project.cpp @@ -6,7 +6,7 @@ // 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: 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: echo '/- USER_KEEP -/' >> %t.project/CppVerify/User.lean @@ -14,6 +14,13 @@ // 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 +// 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/Goal_583ed320b83a75f8.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 From 00dc8f26a6f38fd4de1e0baefe711548aef568c4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:20 +0530 Subject: [PATCH 06/99] test: Add a function to certify with a given lake. --- clang/test/Verify/suite/Inputs/lean_toolchain.cpp | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_toolchain.cpp 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) +{} From 87fa76abdbf373b5d9576fa523f05ea285f898c0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:21 +0530 Subject: [PATCH 07/99] test: Check that certification runs the pinned Lean. --- clang/test/Verify/suite/lean_toolchain.test | 24 +++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 clang/test/Verify/suite/lean_toolchain.test 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) From 8ef88f4dc4e9ff3af9c3779f8257f6f829c24e8d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:21 +0530 Subject: [PATCH 08/99] docs: Note the Lean 4.35.0 pin in the README. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. From 80b0bd00998a21191e3a49a5ff4f3767cfb4e59a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:21 +0530 Subject: [PATCH 09/99] docs: Describe the Lean pin and its migration in the architecture. --- docs/ARCHITECTURE.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 8585048b55..14e4378054 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1662,6 +1662,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 +2044,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`). From feedc462f16747f154ca823115a41a14eefa9ba7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:22 +0530 Subject: [PATCH 10/99] docs: Note the Lean pin and its migration in the design. --- docs/DESIGN.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 9fd7d50dc7..bca0768874 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1877,14 +1877,16 @@ 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 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 From 9312d84f5eb45ea6be47845de7d5ba91d4c8d977 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:22 +0530 Subject: [PATCH 11/99] docs: Note the Lean 4.35.0 pin in chapter 17. --- website/source/book/part-ii/ch17-backends-modular-calls.rst | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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..559cc98c49 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 @@ -158,7 +158,9 @@ For an explicit interactive proof: ``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 +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. From fb8c11e4992325efd723a5066a84ad98febb12f3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:22 +0530 Subject: [PATCH 12/99] docs: Describe the Lean pin, how certification runs it, and how projects move to it. --- website/source/language/tooling.rst | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 0261fc53a7..fca5de915e 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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -267,7 +272,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 From b695c498142b8469003d77579d5b0e22a8136545 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:23 +0530 Subject: [PATCH 13/99] docs: Note the Lean 4.35.0 pin in the release notes. --- website/source/release-notes.rst | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index ab305ce360..e488f3d6b6 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -279,6 +279,14 @@ queries (:doc:`language/tooling`). which requires extended arrays for constant arrays; such a query now enables them itself (:doc:`language/tooling`). +**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 +296,7 @@ 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``. 0.1.1 ----- From 978e1511968fc5b719ff193c9d434195582972d7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:30 +0530 Subject: [PATCH 14/99] verify: Declare the hash of an obligation's statement, which leaves out its function's identity. --- clang/lib/Verify/Backend/ObligationSerialization.h | 6 ++++++ 1 file changed, 6 insertions(+) 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. From aa0db6ebf7432a154e9ea4eb8c407c3ff0433dd6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:31 +0530 Subject: [PATCH 15/99] verify: Hash an obligation's statement without its function's identity. --- .../Verify/Backend/ObligationSerialization.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) 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); From 6679b539359bc2f473542019d0cdefcc71eb1bdd Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:31 +0530 Subject: [PATCH 16/99] verify: Describe each goal of a Lean project with what identifies it across regenerations. --- clang/lib/Verify/Backend/LeanBackend.h | 37 ++++++++++++++++++++++---- 1 file changed, 32 insertions(+), 5 deletions(-) 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 { From 7f57a546983853025ee06d7da7e008b4302290f4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:31 +0530 Subject: [PATCH 17/99] verify: Name Lean project goals and spec bodies by function and statement, never by position. --- clang/lib/Verify/Backend/LeanBackend.cpp | 88 +++++++++++++++++++++--- 1 file changed, 80 insertions(+), 8 deletions(-) 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); } From b28e26517a4cf0f36e9471c06a194d7b1d08d958 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:32 +0530 Subject: [PATCH 18/99] verify: Pass the Lean backend the goal records of a project. --- clang/lib/Verify/Backend/VerifyBackend.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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, From b6461b6f10cea600fce2573d78965385e3e35f9e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:32 +0530 Subject: [PATCH 19/99] verify: Create the Lean backend with the goal records of a project. --- clang/lib/Verify/Backend/VerifyBackend.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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"); From 51080c30d9ce20082099a7d4b16f6fa5f83bdfea Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:33 +0530 Subject: [PATCH 20/99] verify: Add the option that deletes the proofs a Lean project keeps. --- clang/lib/Verify/Driver/Verifier.h | 2 ++ 1 file changed, 2 insertions(+) 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. From c858715f86f41a3a7b419dab20ec7312b3f3cbc8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:33 +0530 Subject: [PATCH 21/99] verify: Keep each Lean proof with the goal of its statement across regenerations. --- clang/lib/Verify/Driver/Verifier.cpp | 428 +++++++++++++++++++++++++-- 1 file changed, 401 insertions(+), 27 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 9fbcb47aa3..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, @@ -1474,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; + } + 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; - CheckFile += "import CppVerify.Proofs." + Module + "\n"; + 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"); @@ -1576,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(); } @@ -1729,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, @@ -1826,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; @@ -2633,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)) { @@ -2906,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 @@ -3218,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. @@ -3238,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)); From ac5fd41df75b2da5e16233d51bcc8525fd3eeeab Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:33 +0530 Subject: [PATCH 22/99] verify: Add --lean-prune-stale. --- clang/tools/cpp-verify/Main.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) 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"; From 7a1f2390a84b662a6036d2c933b6a7c6de885c6b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:34 +0530 Subject: [PATCH 23/99] test: Prove the statement-named goal in lean_dependencies_impossible.lean. --- .../Verify/suite/Inputs/lean_dependencies_impossible.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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⟩ From fa9357e71f1043c62b917e0e6748a6c9bcc7dd37 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:34 +0530 Subject: [PATCH 24/99] test: Prove the statement-named goal in lean_dependencies_looping.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) ∧ From 994b492614b016f782aca8d1004d58a37ccdbaaa Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:34 +0530 Subject: [PATCH 25/99] test: Prove the statement-named goal in lean_dependencies_mixed.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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) ∧ From e006a33830a30ec5b4c075c4fa106f32f86ed777 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:35 +0530 Subject: [PATCH 26/99] test: Prove the statement-named goal in lean_dependencies_positive.lean. --- .../test/Verify/suite/Inputs/lean_dependencies_positive.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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))) From 87eb170bc79a5fecae5e2424e1226392e063f5bf Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:35 +0530 Subject: [PATCH 27/99] test: Prove the statement-named goal in lean_dependencies_same.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_same.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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)) From 94247f0c28d1a62eb041d554bd7b7fd58499ee24 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:35 +0530 Subject: [PATCH 28/99] test: Prove the statement-named goal in lean_dependencies_seven.lean. --- clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 From a118c22bb3d90d10ae5ad36e99bdbfff1b9273d0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:36 +0530 Subject: [PATCH 29/99] test: Prove the statement-named goal in lean_dependencies_termination.lean. --- .../Verify/suite/Inputs/lean_dependencies_termination.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 From 17da66953338414b3c93052e2fb20468150851ce Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:36 +0530 Subject: [PATCH 30/99] test: Prove the statement-named goal in lean_dependencies_trusting.lean. --- .../test/Verify/suite/Inputs/lean_dependencies_trusting.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 From fdde12a8186f557afd67964ef2221a30134d0709 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:37 +0530 Subject: [PATCH 31/99] test: Prove the statement-named goal in lean_fallback_goal_1.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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] From bda7564d15b07b7b3883141561a9b209d2c9ee02 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:37 +0530 Subject: [PATCH 32/99] test: Prove the statement-named goal in lean_fallback_goal_2.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 From 255b9cb6fd9e2e0f2726232679da6de30528cfef Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:37 +0530 Subject: [PATCH 33/99] test: Prove the statement-named goal in lean_fallback_goal_3.lean. --- clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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] From e9e41eeea883e3feebef1f3b0e5b2b1304361cc4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:38 +0530 Subject: [PATCH 34/99] test: Prove the statement-named goal in lean_fallback_goal_4.lean. --- .../Verify/suite/Inputs/lean_fallback_goal_4.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) 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] From 2fd244c8b68d8582f76cc153d71bc8cb174bfb2f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:38 +0530 Subject: [PATCH 35/99] test: Prove the statement-named goal in lean_fallback_partial_goal_1.lean. --- .../Verify/suite/Inputs/lean_fallback_partial_goal_1.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 From e3cb581f1a348fed8af3780ac4e764d9c1689155 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:38 +0530 Subject: [PATCH 36/99] test: Prove the statement-named goal in lean_fallback_partial_goal_2.lean. --- .../Verify/suite/Inputs/lean_fallback_partial_goal_2.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 From 6828c19ace016e9354567d77f54e4a9527213520 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:39 +0530 Subject: [PATCH 37/99] test: Prove the statement-named goal in lean_semantics_call.lean. --- clang/test/Verify/suite/Inputs/lean_semantics_call.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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⟩)) From a94beff83a9c8fc1c1ee7700221b28c3cc61ba2c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:39 +0530 Subject: [PATCH 38/99] test: Prove the statement-named goal in lean_semantics_mix.lean. --- clang/test/Verify/suite/Inputs/lean_semantics_mix.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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)) From 5abd96b03945e07fce099a6de91274fa47697771 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:39 +0530 Subject: [PATCH 39/99] test: Prove the statement-named goal in lean_semantics_numerals.lean. --- clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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)) From 6984be40da4a1d5a8d6206d08b19e7ab1ba9a544 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:40 +0530 Subject: [PATCH 40/99] test: Check Lean project goals and proof files against the export by obligation. --- .../suite/Inputs/run_backend_fidelity.py | 82 ++++++++++--------- 1 file changed, 45 insertions(+), 37 deletions(-) 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}) From 9e561a3b7e1be8f8dacd39a948478cdc27d19824 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:40 +0530 Subject: [PATCH 41/99] test: Expect statement-named goals and per-function proof files in lean_certify.cpp. --- clang/test/Verify/suite/lean_certify.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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() From 9c97a5bc435472dcc6aa9e0a0062c2cb0f541105 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:41 +0530 Subject: [PATCH 42/99] test: Expect statement-named goals and per-function proof files in lean_dependencies.test. --- clang/test/Verify/suite/lean_dependencies.test | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) 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 From ad38b04d8fd3b08ec119eb0dfac53552cf39900a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:41 +0530 Subject: [PATCH 43/99] test: Expect statement-named goals and per-function proof files in lean_fallback.test. --- clang/test/Verify/suite/lean_fallback.test | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 From c8413afe049f0fe6f4d21d894b1c209d8299f376 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:41 +0530 Subject: [PATCH 44/99] test: Expect statement-named goals and per-function proof files in lean_fallback_fast.cpp. --- clang/test/Verify/suite/lean_fallback_fast.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) { From 736379f3fe23ea4d235592a15e310df1198d564b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:42 +0530 Subject: [PATCH 45/99] test: Expect statement-named goals and per-function proof files in lean_fallback_partial.test. --- .../test/Verify/suite/lean_fallback_partial.test | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) 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 From 8fbb54f0668957e516e9f635ad0e811d8d7594f1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:42 +0530 Subject: [PATCH 46/99] test: Expect statement-named goals and per-function proof files in lean_project.cpp. --- clang/test/Verify/suite/lean_project.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang/test/Verify/suite/lean_project.cpp b/clang/test/Verify/suite/lean_project.cpp index ae95a61cb6..51f4a7c9c6 100644 --- a/clang/test/Verify/suite/lean_project.cpp +++ b/clang/test/Verify/suite/lean_project.cpp @@ -5,21 +5,21 @@ // 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: 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/Goal_583ed320b83a75f8.lean +// 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 From e4506d3b39033becf9f6ce0db76c77d187ee1592 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:42 +0530 Subject: [PATCH 47/99] test: Expect statement-named goals and per-function proof files in lean_semantics.cpp. --- clang/test/Verify/suite/lean_semantics.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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 From 43e634733114b45b2a3c9c53c8c0345157de39a6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:43 +0530 Subject: [PATCH 48/99] test: Add the base source of the Lean proof identity test. --- .../suite/Inputs/lean_identity_base.cpp | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_base.cpp 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; +} From 5ee7f7bd776bbcc3d8336f8cb385dae564de054f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:43 +0530 Subject: [PATCH 49/99] test: Add the inserted source of the Lean proof identity test. --- .../suite/Inputs/lean_identity_inserted.cpp | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_inserted.cpp 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; +} From 8129f71cfe57b8f5a6d9802caa542715dd4cc5dd Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:43 +0530 Subject: [PATCH 50/99] test: Add the renamed source of the Lean proof identity test. --- .../suite/Inputs/lean_identity_renamed.cpp | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_renamed.cpp 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; +} From 3988adb3fab335456b77cd093639575693d31f58 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:44 +0530 Subject: [PATCH 51/99] test: Add the changed source of the Lean proof identity test. --- .../suite/Inputs/lean_identity_changed.cpp | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_changed.cpp 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; +} From d3252a18202140efead32e955b5ff67b7147166d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:44 +0530 Subject: [PATCH 52/99] test: Add the removed source of the Lean proof identity test. --- .../Verify/suite/Inputs/lean_identity_removed.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_removed.cpp 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; +} From 4fe95411ce222fc22414dedb4f70c1378bddc326 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:45 +0530 Subject: [PATCH 53/99] test: Add the proof of cppverify_bump_ce87d1_missing_return_ba8abb90 for the Lean proof identity test. --- .../cppverify_bump_ce87d1_missing_return_ba8abb90.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean 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 From afe389aee73b7b3456f073803fd488de3af4e8c4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:45 +0530 Subject: [PATCH 54/99] test: Add the proof of cppverify_one_99bcee_missing_return_54ae7c80 for the Lean proof identity test. --- .../cppverify_one_99bcee_missing_return_54ae7c80.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean 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 From f5590e4c42bf9e822abfef8366280c320fe2c053 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:45 +0530 Subject: [PATCH 55/99] test: Add the proof of cppverify_one_99bcee_postcondition_cd6bdfcd for the Lean proof identity test. --- .../cppverify_one_99bcee_postcondition_cd6bdfcd.lean | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean 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 From 8129b4bf64dc3be535561d07eaa80845a490211b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:46 +0530 Subject: [PATCH 56/99] test: Add the proof of cppverify_one_99bcee_postcondition_cd6bdfcd_2 for the Lean proof identity test. --- .../cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean 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 From 10b4da9467eefe0ec6593f963cff677b86f99e6f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:46 +0530 Subject: [PATCH 57/99] test: Add the proof of cppverify_one_99bcee_postcondition_ebbe6a6a for the Lean proof identity test. --- .../cppverify_one_99bcee_postcondition_ebbe6a6a.lean | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean 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 From e445a821c87846c4c9007e8ac87d053906bd9ad6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:46 +0530 Subject: [PATCH 58/99] test: Add the proof of cppverify_six_6a2cf3_missing_return_54ae7c80 for the Lean proof identity test. --- .../cppverify_six_6a2cf3_missing_return_54ae7c80.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean 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 From 9808fe9b9cbce47902b4dfa081bf1a50ae13f35a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:47 +0530 Subject: [PATCH 59/99] test: Add the proof of cppverify_six_6a2cf3_postcondition_198bc076 for the Lean proof identity test. --- ...ppverify_six_6a2cf3_postcondition_198bc076.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean 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 From 7073977dcd5ecf29d7751e5ede7f4dcda07d6259 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:47 +0530 Subject: [PATCH 60/99] test: Add the proof of cppverify_tri_decreases_f55d4c_termination_3c6bb93f for the Lean proof identity test. --- ...ppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean 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 From 5214899b3716e4421ad3f33ba7c00e8ba610c07d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:47 +0530 Subject: [PATCH 61/99] test: Add CppVerify/Proofs/Goal_00000000deadbeef.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_00000000deadbeef.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000deadbeef.lean 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 From 75b0652b892453888fb3afc17392196345b815af Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:48 +0530 Subject: [PATCH 62/99] test: Add CppVerify/Proofs/Goal_00000000feedface.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_00000000feedface.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_00000000feedface.lean 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 From bd5634bbb665db51b0768808ad8359ff4ef58953 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:48 +0530 Subject: [PATCH 63/99] test: Add CppVerify/Proofs/Goal_1272763fe029af5c.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_1272763fe029af5c.lean | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_1272763fe029af5c.lean 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 From 911011774baf8c97dbb994b056e51c35764718ae Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:48 +0530 Subject: [PATCH 64/99] test: Add CppVerify/Proofs/Goal_14843fe605ca0dfc.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_14843fe605ca0dfc.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_14843fe605ca0dfc.lean 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 From acbcfa113eabe6fac4f40460ad43b2b473933f3f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:49 +0530 Subject: [PATCH 65/99] test: Add CppVerify/Proofs/Goal_959f92a07e95a169.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_959f92a07e95a169.lean | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_959f92a07e95a169.lean 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 From 76883a78bb66b1c3d67bc60e471f8948f2cdb375 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:49 +0530 Subject: [PATCH 66/99] test: Add CppVerify/Proofs/Goal_9b7aec03175825c9.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_9b7aec03175825c9.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_9b7aec03175825c9.lean 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 From 18a236c70d8e4e930d4a3640d6a2659ef03f57b1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:50 +0530 Subject: [PATCH 67/99] test: Add CppVerify/Proofs/Goal_b054b023e3576f6e.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_b054b023e3576f6e.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b054b023e3576f6e.lean 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 From c3ca848e17130953e9d745f64d2d976473c3171c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:50 +0530 Subject: [PATCH 68/99] test: Add CppVerify/Proofs/Goal_b95e8b7f774dddd4.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_b95e8b7f774dddd4.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_b95e8b7f774dddd4.lean 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 From efe73561e46b87a2581b7fc9893798cf726ea4be Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:50 +0530 Subject: [PATCH 69/99] test: Add CppVerify/Proofs/Goal_f799910065d5f258.lean of the 0.1 project the Lean proof identity test migrates. --- .../CppVerify/Proofs/Goal_f799910065d5f258.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/Proofs/Goal_f799910065d5f258.lean 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 From 782bef8bf208a372f740856787255170462dee8d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:51 +0530 Subject: [PATCH 70/99] test: Add CppVerify/User.lean of the 0.1 project the Lean proof identity test migrates. --- .../Verify/suite/Inputs/lean_identity_v01/CppVerify/User.lean | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/CppVerify/User.lean 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. -/ From 5bd3df40529b1cb10ae1f7ea98dadf275692154e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:51 +0530 Subject: [PATCH 71/99] test: Add lakefile.toml of the 0.1 project the Lean proof identity test migrates. --- .../Verify/suite/Inputs/lean_identity_v01/lakefile.toml | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/lakefile.toml 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" From 07db008c4828db244e9efcca55d8983aa83da387 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:51 +0530 Subject: [PATCH 72/99] test: Add lean-toolchain of the 0.1 project the Lean proof identity test migrates. --- clang/test/Verify/suite/Inputs/lean_identity_v01/lean-toolchain | 1 + 1 file changed, 1 insertion(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_identity_v01/lean-toolchain 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 From e3bde60273efd25205a00d101c3087dfbbc09d10 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:52 +0530 Subject: [PATCH 73/99] test: Check that Lean proofs stay with their goals as the source changes. --- clang/test/Verify/suite/lean_identity.test | 198 +++++++++++++++++++++ 1 file changed, 198 insertions(+) create mode 100644 clang/test/Verify/suite/lean_identity.test 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] From ac1e7f0969df8e6df85f943c2341ab144649c63e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:52 +0530 Subject: [PATCH 74/99] docs: Describe how Lean project goals are named and keep their proofs in the architecture. --- docs/ARCHITECTURE.md | 55 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 54 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 14e4378054..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 @@ -2074,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 From 77e6cc5ce8537765446f5cb95936240c5acce37f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:52 +0530 Subject: [PATCH 75/99] docs: State how Lean project goals are named and regenerated in the design. --- docs/DESIGN.md | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index bca0768874..b8c62faf8f 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1879,7 +1879,25 @@ 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.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, From 1ae8bae526609c5483dd70efc76f8cdca7bbdf43 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:53 +0530 Subject: [PATCH 76/99] docs: Give the Lean proof file path by function in chapter 16. --- website/source/book/part-ii/ch16-when-verification-fails.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 1787839647d2cf197b13d61be1106403c314a517 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:53 +0530 Subject: [PATCH 77/99] docs: Show Lean proofs following their goals in chapter 17. --- .../part-ii/ch17-backends-modular-calls.rst | 74 ++++++++++++++++--- 1 file changed, 64 insertions(+), 10 deletions(-) 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 559cc98c49..2fe0cb898f 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -153,11 +153,13 @@ 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. +``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 @@ -212,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), @@ -223,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⟩)) @@ -267,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 @@ -306,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 ---------------------------- From c84dce250b48e2ad87fa02656fedf5103620f528 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:54 +0530 Subject: [PATCH 78/99] docs: Document Lean goal names, kept proofs, and --lean-prune-stale in the tooling reference. --- website/source/language/tooling.rst | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index fca5de915e..47f4b1caca 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -200,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 @@ -263,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 @@ -292,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, From 78b78453ec64c39b34b2dbc6296aa12e51e47103 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 13:39:54 +0530 Subject: [PATCH 79/99] docs: Note that Lean proofs stay with their goals. --- website/source/release-notes.rst | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index e488f3d6b6..11fd40656e 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -279,6 +279,23 @@ 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 @@ -296,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). Lean projects pin ``leanprover/lean4:v4.35.0``. +(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 ----- From c46381ffaa29db9fa6faa1adaabccb7dc2cd1764 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:40 +0530 Subject: [PATCH 80/99] verify: Let a goal's Or record where the assumption it states comes from. --- clang/lib/Verify/Backend/Obligation.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clang/lib/Verify/Backend/Obligation.h b/clang/lib/Verify/Backend/Obligation.h index ba16118533..e7d74d813f 100644 --- a/clang/lib/Verify/Backend/Obligation.h +++ b/clang/lib/Verify/Backend/Obligation.h @@ -216,6 +216,10 @@ class LogicExpr { /// quantifier, a solver hint outside the term's meaning, its identity, and /// archives. std::vector> Patterns; + /// For an Or that states one assumption of a goal (`!A || rest`): where A + /// comes from (`pre`, `call:f`, `def:x_1`), so a goal can be shown as + /// named hypotheses. Outside the term's meaning, identity, and archives. + std::string Premise; explicit LogicExpr(Kind K) : K(K) {} }; From 10e3432d70b4a8a611e45a5e4d9ef04ab6d6ca2b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:40 +0530 Subject: [PATCH 81/99] verify: Keep where an assumption comes from when a goal is copied. --- clang/lib/Verify/Backend/ObligationSimplify.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/clang/lib/Verify/Backend/ObligationSimplify.cpp b/clang/lib/Verify/Backend/ObligationSimplify.cpp index 48eca39d48..27875e481e 100644 --- a/clang/lib/Verify/Backend/ObligationSimplify.cpp +++ b/clang/lib/Verify/Backend/ObligationSimplify.cpp @@ -28,6 +28,7 @@ std::unique_ptr cloneLogicExpr(const LogicExpr *Expr) { Copy->OverflowOp = Expr->OverflowOp; Copy->CollectionOp = Expr->CollectionOp; Copy->SpecCallee = Expr->SpecCallee; + Copy->Premise = Expr->Premise; for (const auto &Child : Expr->Children) Copy->Children.push_back(cloneLogicExpr(Child.get())); for (const auto &Pattern : Expr->Patterns) @@ -383,6 +384,7 @@ std::unique_ptr substituteVariable(const LogicExpr *Expr, Copy->OverflowOp = Expr->OverflowOp; Copy->CollectionOp = Expr->CollectionOp; Copy->SpecCallee = Expr->SpecCallee; + Copy->Premise = Expr->Premise; for (const auto &Child : Expr->Children) Copy->Children.push_back(substituteVariable(Child.get(), Name, Value)); for (const auto &Pattern : Expr->Patterns) From f90025a96dcb6e638e1edae2f5dfeb2290b8f168 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:41 +0530 Subject: [PATCH 82/99] verify: Record where each passive assumption comes from. --- clang/lib/Verify/Transform/Passivize.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/clang/lib/Verify/Transform/Passivize.h b/clang/lib/Verify/Transform/Passivize.h index b4dcea5c87..0291f72b02 100644 --- a/clang/lib/Verify/Transform/Passivize.h +++ b/clang/lib/Verify/Transform/Passivize.h @@ -31,6 +31,9 @@ struct PassiveStmt { /// postcondition or unfolding, a frame of a spec's reads), not a premise /// of the function's claim. Unmarked assumptions are premises. bool Theorem = false; + /// For an assumption: where it comes from (`pre`, `call:f`, `inv`, ...), + /// which names its hypothesis in a readable goal. + std::string Origin; }; /// A goal checked in the final state. @@ -80,6 +83,8 @@ struct PassiveProgram { std::vector> EntryAssumes; /// How many leading EntryAssumes are the function's own preconditions. size_t PreconditionCount = 0; + /// Where each of EntryAssumes comes from, as PassiveStmt::Origin. + std::vector EntryOrigins; /// Each behavior's assumption in the entry state. std::vector>> BehaviorAssumes; std::vector ExitAsserts; From 17117f9cad29ee6672370d8b50aba231a82c81db Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:41 +0530 Subject: [PATCH 83/99] verify: Name the origin of every assumption the passivizer makes. --- clang/lib/Verify/Transform/Passivize.cpp | 61 ++++++++++++++++++++++-- 1 file changed, 57 insertions(+), 4 deletions(-) diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index dd6f7849b3..b54e616bec 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -9,6 +9,7 @@ #include "llvm/ADT/STLFunctionalExtras.h" #include "llvm/ADT/SmallString.h" #include "llvm/ADT/StringRef.h" +#include "llvm/Support/SaveAndRestore.h" #include #include #include @@ -2915,6 +2916,7 @@ void verify::addChoiceAxioms(std::vector> &Facts, auto Instance = std::make_unique(); Instance->K = PassiveStmt::Assume; Instance->Theorem = Theorem; + Instance->Origin = "choose"; Instance->Cond = std::move(Fact); Facts.push_back(std::move(Instance)); } @@ -3068,6 +3070,7 @@ static void addFrameInstances(PassiveProgram &P, const FunctionMap &FnMap) { Instance->K = PassiveStmt::Assume; Instance->TraceEventCount = P.Stmts[S.Index]->TraceEventCount; Instance->Theorem = true; + Instance->Origin = "reads:" + Spec.Name; Instance->Cond = std::move(Fact); After[S.Index].push_back(std::move(Instance)); Work.push_back(S.Before); @@ -3141,6 +3144,7 @@ addSpecPostInstances(PassiveProgram &P, const FunctionMap &FnMap, auto Instance = std::make_unique(); Instance->K = PassiveStmt::Assume; Instance->Theorem = true; + Instance->Origin = "spec:" + Spec.Name; Instance->Cond = std::move(Fact); if (Spec.Unfolding) Unfolded.push_back(Instance->Cond.get()); @@ -3218,6 +3222,7 @@ addSpecPostInstances(PassiveProgram &P, const FunctionMap &FnMap, std::move(Fact), Call.Loc, (*Q)->BinderType); auto Instance = std::make_unique(); Instance->K = PassiveStmt::Assume; + Instance->Origin = "spec:" + Spec.Name; Instance->Cond = std::move(Fact); Facts.push_back(std::move(Instance)); } @@ -3257,6 +3262,8 @@ class PassivizerImpl { std::string EntryHeap; }; std::vector LoopFrames; + /// Where the assumptions being emitted come from (PassiveStmt::Origin). + std::string Origin; std::vector> ReturnGuards; std::vector OwnedAllocationIdentities; std::map> ReferenceBindings; @@ -3999,6 +4006,8 @@ class PassivizerImpl { PS->K = K; PS->ProofKind = ProofKind; PS->Note = std::move(Note); + if (K == PassiveStmt::Assume) + PS->Origin = Origin; PS->TraceEventCount = TraceEvents.size(); if (Guard) Cond = makeImplies(cloneVExpr(Guard), std::move(Cond), Loc); @@ -4038,6 +4047,7 @@ class PassivizerImpl { !needsInactiveFrame(Guard)) return; auto Inactive = makeNot(cloneVExpr(Guard), Loc); + llvm::SaveAndRestore Kept(Origin, "keep"); emitPassive(P, PassiveStmt::Assume, makeEq(std::make_unique(After.str(), Ty, Loc), std::make_unique(Before.str(), Ty, Loc), Loc), @@ -4109,6 +4119,7 @@ class PassivizerImpl { } std::string ResultName = bump(ResultVar); Renames["result"] = ResultName; + llvm::SaveAndRestore Returned(Origin, "ret"); emitMathBridge(P, Result.get(), nullptr, SourceLocation(), true); emitPassive(P, PassiveStmt::Assume, makeEq(std::make_unique(ResultName, Fn.ReturnType, @@ -4233,13 +4244,12 @@ class PassivizerImpl { for (const SafetyCheck &Check : Checks) emitPassive(P, PassiveStmt::Assert, cloneExpr(Check.Cond.get(), Ctx), Guard, Loc, Check.Kind, Check.Note); - emitPassive(P, PassiveStmt::Assume, - machineMathBridgeForExpr(E, &FnMap, BridgeMachineValue), Guard, - Loc); + emitMathBridge(P, E, Guard, Loc, BridgeMachineValue); } void emitMathBridge(PassiveProgram &P, const VExpr *E, const VExpr *Guard, SourceLocation Loc, bool BridgeMachineValue = false) { + llvm::SaveAndRestore Exact(Origin, "exact"); emitPassive(P, PassiveStmt::Assume, machineMathBridgeForExpr(E, &FnMap, BridgeMachineValue), Guard, Loc); @@ -4577,6 +4587,9 @@ class PassivizerImpl { for (const auto &Pre : Fn.Preconditions) { CloneCtx PCtx{Renames, OldState, false}; + P.EntryOrigins.push_back( + P.EntryAssumes.size() < Fn.ExplicitPreconditionCount ? "pre" + : "entry"); P.EntryAssumes.push_back(cloneExpr(Pre.get(), PCtx)); } P.PreconditionCount = P.EntryAssumes.size(); @@ -4596,12 +4609,15 @@ class PassivizerImpl { std::move(Null), VType::makeBool(), SourceLocation(), Renames[VLivenessHeapName]); P.EntryAssumes.push_back(makeNot(std::move(NullLive), SourceLocation())); + P.EntryOrigins.insert(P.EntryOrigins.end(), 2, "null"); } if (Fn.ObjectModel) { CloneCtx PCtx{Renames, OldState, false}; - for (const AbstractObject &Object : abstractObjects(Fn)) + for (const AbstractObject &Object : abstractObjects(Fn)) { P.EntryAssumes.push_back(cloneExpr( objectPlacement(Object, SourceLocation()).get(), PCtx)); + P.EntryOrigins.push_back("object"); + } } std::unique_ptr Active = makeBoolLiteral(true, SourceLocation()); @@ -5298,6 +5314,7 @@ class PassivizerImpl { for (const auto &Post : Callee->Postconditions) { auto PS = std::make_unique(); PS->K = PassiveStmt::Assume; + PS->Origin = "call:" + Callee->Name; PS->Cond = rebaseSliceBinders(substParams(Post.get(), PostParamMap, Ctx, EntryHeap, "", {}, &ParamMap)); P.Stmts.push_back(std::move(PS)); @@ -5309,9 +5326,41 @@ class PassivizerImpl { } } + // The origin of the assumptions a statement makes, before its parts name + // their own. + static std::string statementOrigin(const VStmt &S) { + switch (S.K) { + case VStmt::Assign: + return "def"; + case VStmt::Store: + return "store"; + case VStmt::Allocate: + case VStmt::EndLifetime: + case VStmt::Free: + return "alloc"; + case VStmt::If: + return "branch"; + case VStmt::Return: + return "ret"; + case VStmt::While: + return "loop"; + case VStmt::Call: + return "call:" + static_cast(S).Callee; + case VStmt::ContractAssert: + return "check"; + case VStmt::Havoc: + return "havoc"; + default: + return "fact"; + } + } + void processStmt(const VStmt &S, PassiveProgram &P, std::map &Renames, std::unique_ptr &Active) { + std::optional> Named; + if (S.K != VStmt::Seq && S.K != VStmt::GhostBlock) + Named.emplace(Origin, statementOrigin(S)); switch (S.K) { case VStmt::Assign: { const auto &A = static_cast(S); @@ -6009,6 +6058,7 @@ class PassivizerImpl { } CloneCtx HeadCtx{Renames, OldState, false}; + llvm::SaveAndRestore Head(Origin, "frame"); if (!LoopEntryHeap.empty()) { // Every iteration starts with the cells outside the declared // footprints unchanged since the loop began. @@ -6018,11 +6068,13 @@ class PassivizerImpl { W.Loc), Active.get(), W.Loc); } + Origin = "inv"; for (const auto &Inv : W.Invariants) { auto BoundInv = cloneExpr(Inv.get(), HeadCtx); emitPassive(P, PassiveStmt::Assume, std::move(BoundInv), Active.get(), W.Loc); } + Origin = "cond"; std::string ChoiceName = bump("__loop_choice"); auto Choice = @@ -6084,6 +6136,7 @@ class PassivizerImpl { } emitTrace(PassiveTraceKind::Loop, "exit", Active.get(), W.Loc); + Origin = "exit"; std::vector Returns; for (size_t I = ReturnsBefore; I != ReturnGuards.size(); ++I) Returns.push_back(ReturnGuards[I].get()); From 534eee5ab91c24873d54f272b74ef565571c7f03 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:41 +0530 Subject: [PATCH 84/99] verify: Mark each assumption of a goal with where it comes from. --- clang/lib/Verify/Backend/Obligation.cpp | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp index 6bebcbc018..0e602c1eba 100644 --- a/clang/lib/Verify/Backend/Obligation.cpp +++ b/clang/lib/Verify/Backend/Obligation.cpp @@ -416,6 +416,7 @@ static std::unique_ptr cloneVCExpr(const VCExpr *E) { Copy->OverflowOp = E->OverflowOp; Copy->CollectionOp = E->CollectionOp; Copy->SpecCallee = E->SpecCallee; + Copy->Premise = E->Premise; for (const auto &Child : E->Children) Copy->Children.push_back(cloneVCExpr(Child.get())); for (const auto &Pattern : E->Patterns) @@ -2230,6 +2231,7 @@ class ObligationBuilder { std::unique_ptr Cond; std::string Note; bool Theorem; + std::string Origin; }; std::vector Stmts; for (const auto &Stmt : P.Stmts) { @@ -2239,7 +2241,7 @@ class ObligationBuilder { } Stmts.push_back({Stmt->K, obligationKind(Stmt->ProofKind), Stmt->TraceEventCount, fromVExpr(Stmt->Cond.get()), - Stmt->Note, Stmt->Theorem}); + Stmt->Note, Stmt->Theorem, Stmt->Origin}); } std::vector< @@ -2272,16 +2274,23 @@ class ObligationBuilder { return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ConstructionError.c_str()); - std::vector Assumptions; - for (const auto &Entry : EntryAssumes) - Assumptions.push_back(Entry.get()); + // Each assumption with where it comes from, which names its hypothesis. + std::vector> Assumptions; + for (size_t I = 0; I != EntryAssumes.size(); ++I) + Assumptions.emplace_back(EntryAssumes[I].get(), I < P.EntryOrigins.size() + ? P.EntryOrigins[I] + : "entry"); for (size_t I = 0; I < P.PreconditionCount && I < EntryAssumes.size(); ++I) M.Preconditions.push_back(cloneVCExpr(EntryAssumes[I].get())); auto makeGoal = [&](const VCExpr *Condition) -> std::unique_ptr { std::unique_ptr ConditionWP = cloneVCExpr(Condition); - for (auto It = Assumptions.rbegin(); It != Assumptions.rend(); ++It) - ConditionWP = vcOr(vcNot(cloneVCExpr(*It)), std::move(ConditionWP)); + for (auto It = Assumptions.rbegin(); It != Assumptions.rend(); ++It) { + ConditionWP = + vcOr(vcNot(cloneVCExpr(It->first)), std::move(ConditionWP)); + if (ConditionWP->K == VCExpr::Or) + ConditionWP->Premise = It->second.empty() ? "fact" : It->second; + } ConditionWP->Loc = Condition->Loc; ConditionWP->EndLoc = Condition->EndLoc; return ConditionWP; @@ -2311,7 +2320,7 @@ class ObligationBuilder { for (const LoweredStmt &Stmt : Stmts) { if (Stmt.Kind == PassiveStmt::Assume) { - Assumptions.push_back(Stmt.Cond.get()); + Assumptions.emplace_back(Stmt.Cond.get(), Stmt.Origin); if (Stmt.Theorem) M.Theorems.push_back(cloneVCExpr(Stmt.Cond.get())); continue; From 7461576c4376de02593dba8b0c3263d499884206 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:42 +0530 Subject: [PATCH 85/99] verify: Give a Lean project goal the names a proof of its readable form introduces. --- clang/lib/Verify/Backend/LeanBackend.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h index 2eb17d5843..7145e8596c 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -23,6 +23,9 @@ struct LeanProjectGoal { std::string Source; /// The prefix of the spec bodies its goal may unfold. std::string BodyPrefix; + /// What a proof of its readable form introduces, in order: the goal's + /// variables, definitions, and named hypotheses. + std::string Intros; /// The names 0.1 gave the goal and its spec bodies, which a project 0.1 /// generated still uses. std::string LegacyName; From 101771e81accbc052051071f4fc9daaab9e5a886 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:42 +0530 Subject: [PATCH 86/99] verify: State each Lean project goal as named hypotheses, with a kernel-checked bridge to the goal. --- clang/lib/Verify/Backend/LeanBackend.cpp | 181 ++++++++++++++++++++++- 1 file changed, 175 insertions(+), 6 deletions(-) diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp index 5cbb3ee19f..f594870e97 100644 --- a/clang/lib/Verify/Backend/LeanBackend.cpp +++ b/clang/lib/Verify/Backend/LeanBackend.cpp @@ -769,8 +769,9 @@ static void collectLeanSpecCalls(const LogicExpr *Expression, // A definition holds at every argument, so the instance at an application // under quantifiers is stated for every value of their binders. -static unsigned emitLeanSpecAxiomBinders(const LogicExpr *Goal, - llvm::raw_ostream &OS) { +static unsigned +emitLeanSpecAxiomBinders(const LogicExpr *Goal, llvm::raw_ostream &OS, + std::vector *Names = nullptr) { std::vector Binders; std::vector Calls; collectLeanSpecCalls(Goal, Binders, Calls); @@ -785,8 +786,12 @@ static unsigned emitLeanSpecAxiomBinders(const LogicExpr *Goal, ++CallIndex; for (unsigned Level = 0; Level < Function->DefinitionFuel; ++Level) { ++BinderCount; - OS << "\n (cppverify_spec_axiom_" << CallIndex << "_" << Level + 1 - << " : "; + const std::string Axiom = "cppverify_spec_axiom_" + + std::to_string(CallIndex) + "_" + + std::to_string(Level + 1); + if (Names) + Names->push_back(Axiom); + OS << "\n (" << Axiom << " : "; if (!Around.empty()) { OS << "∀"; for (const std::string &Binder : Around) { @@ -841,8 +846,162 @@ static void emitLeanTheorem(llvm::StringRef Name, const LogicExpr *Goal, OS << " := by\n sorry\n\n"; } +// A hypothesis of a readable goal: an Or that makeGoal joined to the goal, +// whose left operand negates the assumption. +static const LogicExpr *leanHypothesis(const LogicExpr &Premise) { + const LogicExpr *Left = Premise.Children[0].get(); + return Left->K == LogicExpr::Not && Left->Children.size() == 1 + ? Left->Children[0].get() + : Left; +} + +// Named by where the assumption comes from; a definition by what it defines. +static std::string leanHypothesisName(const LogicExpr &Premise, + std::map &Counts, + std::set &Used) { + auto [Category, Detail] = llvm::StringRef(Premise.Premise).split(':'); + std::string Base = "h_" + leanIdentifierPart(Category); + if (!Detail.empty()) + Base += "_" + leanIdentifierPart(Detail); + bool Numbered = true; + if (llvm::is_contained({"def", "ret", "branch", "loop", "exit", "fact"}, + Category)) { + const LogicExpr *Fact = leanHypothesis(Premise); + if (Fact != Premise.Children[0].get()) + while (Fact->K == LogicExpr::Or && Fact->Children.size() == 2 && + Fact->Children[0]->K == LogicExpr::Not) + Fact = Fact->Children[1].get(); + if (Fact->K == LogicExpr::Eq && Fact->Children.size() == 2 && + Fact->Children[0]->K == LogicExpr::Var) { + Base = "h_" + llvm::StringRef(leanIdentifierPart(Fact->Children[0]->Name)) + .ltrim('_') + .str(); + Numbered = false; + } + } + std::string Name = + Numbered ? Base + "_" + std::to_string(++Counts[Base]) : Base; + while (!Used.insert(Name).second) + Name = Base + "_" + std::to_string(++Counts[Base]); + return Name; +} + +// The goal as named hypotheses and what remains to be shown, and a proof that +// it implies the goal: the bridge the kernel checks, so a proof of this form +// proves the goal whatever this printer did. Intros receives the names a +// proof of it introduces. +static void emitLeanReadableGoal(llvm::StringRef Name, const LogicExpr *Goal, + const std::map &Vars, + bool HasSpecAxioms, std::string &Intros, + llvm::raw_ostream &OS) { + LeanEmitBudget = 500000; + std::vector Premises; + const LogicExpr *Rest = Goal; + while (Rest && Rest->K == LogicExpr::Or && !Rest->Premise.empty() && + Rest->Children.size() == 2) { + Premises.push_back(Rest); + Rest = Rest->Children[1].get(); + } + + std::vector Binders; + for (const auto &[Variable, Sort] : Vars) + Binders.push_back(encodeLeanName(Variable)); + std::string AxiomText; + llvm::raw_string_ostream AxiomOS(AxiomText); + std::vector Axioms; + emitLeanSpecAxiomBinders(Goal, AxiomOS, &Axioms); + Binders.insert(Binders.end(), Axioms.begin(), Axioms.end()); + + LeanTemporaryNames.clear(); + LeanTemporaryRoot = nullptr; + std::vector Temporaries; + for (const LogicExpr *Premise : Premises) + collectLeanTemporaries(Premise->Children[0].get(), Temporaries, true); + collectLeanTemporaries(Rest, Temporaries, true); + std::vector Lets; + for (const LogicExpr *Node : Temporaries) { + LeanTemporaryNames.emplace(Node, Lets.size() + 1); + Lets.push_back("__cppverify_term_" + std::to_string(Lets.size() + 1)); + } + + std::set Used(Binders.begin(), Binders.end()); + Used.insert(Lets.begin(), Lets.end()); + std::map Counts; + std::vector Hypotheses; + for (const LogicExpr *Premise : Premises) + Hypotheses.push_back(leanHypothesisName(*Premise, Counts, Used)); + + OS << "def "; + printLeanName(Name.str(), OS); + OS << ".readable"; + OS << " : Prop :=\n "; + if (!Vars.empty() || HasSpecAxioms) { + OS << "∀"; + emitLeanVariableBinders(Vars, OS); + OS << AxiomText << ",\n "; + } + if (!Lets.empty()) + OS << "("; + for (const LogicExpr *Node : Temporaries) { + OS << "let __cppverify_term_" << LeanTemporaryNames.at(Node) << " : "; + printLeanSort(Node->Sort, OS); + OS << " := "; + LeanTemporaryRoot = Node; + printVCExprLean(Node, OS, LeanTop); + OS << ";\n "; + } + LeanTemporaryRoot = nullptr; + for (size_t I = 0; I != Premises.size(); ++I) { + const LogicExpr *Left = Premises[I]->Children[0].get(); + OS << "(" << Hypotheses[I] << " : "; + if (leanHypothesis(*Premises[I]) != Left) { + printVCExprLean(leanHypothesis(*Premises[I]), OS, LeanTop); + } else { + OS << "¬"; + printVCExprLean(Left, OS, LeanArgument); + } + OS << ") →\n "; + } + printVCExprLean(Rest, OS, Premises.empty() ? LeanTop : LeanArrow); + if (!Lets.empty()) + OS << ")"; + OS << "\n\n"; + LeanTemporaryNames.clear(); + + OS << "theorem "; + printLeanName(Name.str(), OS); + OS << ".of_readable (h : "; + printLeanName(Name.str(), OS); + OS << ".readable) : "; + printLeanName(Name.str(), OS); + OS << " :=\n "; + if (!Binders.empty()) { + OS << "fun"; + for (const std::string &Binder : Binders) + OS << " " << Binder; + OS << " =>\n "; + } + for (size_t I = 0; I != Premises.size(); ++I) + OS << (leanHypothesis(*Premises[I]) != Premises[I]->Children[0].get() + ? "cppverify_imp_or fun " + : "cppverify_not_imp_or fun ") + << Hypotheses[I] << " =>\n "; + OS << "h"; + for (const std::string &Binder : Binders) + OS << " " << Binder; + for (const std::string &Hypothesis : Hypotheses) + OS << " " << Hypothesis; + OS << "\n\n"; + + Intros.clear(); + for (const auto *Part : {&Binders, &Lets, &Hypotheses}) + for (const std::string &Introduced : *Part) + Intros += (Intros.empty() ? "" : " ") + Introduced; +} + static void emitLeanGoalDefinition(llvm::StringRef Name, const LogicExpr *Goal, - llvm::raw_ostream &OS) { + llvm::raw_ostream &OS, + std::string *Intros = nullptr) { LeanEmitBudget = 500000; std::map Variables; collectLeanVariables(Goal, {}, Variables); @@ -868,6 +1027,8 @@ static void emitLeanGoalDefinition(llvm::StringRef Name, const LogicExpr *Goal, } printLeanFlattened(Goal, OS); OS << "\n\n"; + if (Intros) + emitLeanReadableGoal(Name, Goal, Variables, HasSpecAxioms, *Intros, OS); } static void @@ -1004,6 +1165,14 @@ VerifyResult verify::exportLeanScratchPad( OS << " if (x < 0) ≠ (y < 0) then -q else q\n"; OS << "def cppIntRem (x y : Int) : Int :=\n"; OS << " if y = 0 then x else x - cppIntDiv x y * y\n\n"; + if (ProjectGoals) { + // What the bridges from readable goals use. + OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n"; + OS << " (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n"; + OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b " + ":=\n"; + OS << " (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n"; + } } emitLeanFunctionDeclarations(Module, OS, EmittedFunctions); @@ -1080,7 +1249,7 @@ VerifyResult verify::exportLeanScratchPad( } OS << " -/\n"; if (ProjectGoals) { - emitLeanGoalDefinition(Goal.Name, Item.Goal.get(), OS); + emitLeanGoalDefinition(Goal.Name, Item.Goal.get(), OS, &Goal.Intros); ProjectGoals->push_back(std::move(Goal)); } else { emitLeanTheorem(ObligationName, Item.Goal.get(), OS); From e4c8ddb8a8fe2d0b0c2de073a3b5f8661d03d494 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:42 +0530 Subject: [PATCH 87/99] verify: Start each Lean proof stub from the readable form of its goal. --- clang/lib/Verify/Driver/Verifier.cpp | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index e83231923b..6351861a55 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -1298,9 +1298,26 @@ struct LeanProofRecord { bool Pristine = false; }; -static std::string leanProofStub(llvm::StringRef Goal) { +// A stub proves the goal through its readable form, its names introduced. +static std::string leanProofStubHead(llvm::StringRef Goal) { return "import CppVerify.User\n\ntheorem " + Goal.str() + - "_proof : " + Goal.str() + " := by\n sorry\n"; + "_proof : " + Goal.str() + " := by\n apply " + Goal.str() + + ".of_readable\n"; +} + +static std::string leanProofStub(llvm::StringRef Goal, llvm::StringRef Intros) { + std::string Stub = leanProofStubHead(Goal); + if (!Intros.empty()) + Stub += " intro " + Intros.str() + "\n"; + return Stub + " sorry\n"; +} + +static bool isLeanProofStub(llvm::StringRef Body, llvm::StringRef Goal) { + if (!Body.consume_front(leanProofStubHead(Goal)) || + !Body.consume_back(" sorry\n")) + return false; + return Body.empty() || (Body.consume_front(" intro ") && + Body.consume_back("\n") && !Body.contains('\n')); } static std::string leanProofHeader(const LeanProjectGoal &Goal) { @@ -1340,7 +1357,7 @@ static std::optional readLeanProof(llvm::StringRef Path) { return std::nullopt; const size_t End = Text.find("-/\n"); Record.Pristine = End != llvm::StringRef::npos && - Text.substr(End + 3) == leanProofStub(Record.Goal); + isLeanProofStub(Text.substr(End + 3), Record.Goal); return Record; } @@ -1756,7 +1773,8 @@ class Verifier { return llvm::createStringError(EC, "cannot create %s", ProofPath.c_str()); if (llvm::Error Error = writeTextFile( - ProofPath, leanProofHeader(*Goal) + leanProofStub(Goal->Name))) + ProofPath, leanProofHeader(*Goal) + + leanProofStub(Goal->Name, Goal->Intros))) return Error; Taken.insert(ProofPath); } From a0cfe699a72c27f78f351dc4f89605e8e5478416 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:43 +0530 Subject: [PATCH 88/99] test: Prove the True goals of lean_certify.cpp through their readable forms. --- clang/test/Verify/suite/lean_certify.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/clang/test/Verify/suite/lean_certify.cpp b/clang/test/Verify/suite/lean_certify.cpp index c3ce4fd105..00c6550f43 100644 --- a/clang/test/Verify/suite/lean_certify.cpp +++ b/clang/test/Verify/suite/lean_certify.cpp @@ -4,8 +4,8 @@ // 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_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: sed -i.orig 's/ sorry/ trivial/' %t.certified/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.certified/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_postcondition_ba8abb90.lean // RUN: %cpp-verify --backend=lean --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED // RUN: echo 'theorem unfinished : True := by sorry' >> %t.certified/CppVerify/User.lean // RUN: not %cpp-verify --backend=lean --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=USER-ADMITTED @@ -16,8 +16,8 @@ // 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_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: sed -i.orig 's/ sorry/ trivial/' %t.stale/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean +// RUN: sed -i.orig 's/ sorry/ trivial/' %t.stale/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_postcondition_ba8abb90.lean // RUN: not %cpp-verify --backend=lean --lean-project=%t.stale --lean-certify %S/Inputs/lean_certify_stale.cpp -- 2>&1 | FileCheck %s --check-prefix=STALE void trivial() From 375865b22b34b0d50830ac3fbf69d58488ce04aa Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:43 +0530 Subject: [PATCH 89/99] test: Add the source the readable Lean goal test certifies. --- .../Verify/suite/Inputs/lean_readable_certify.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_readable_certify.cpp diff --git a/clang/test/Verify/suite/Inputs/lean_readable_certify.cpp b/clang/test/Verify/suite/Inputs/lean_readable_certify.cpp new file mode 100644 index 0000000000..88f1e5fddb --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_certify.cpp @@ -0,0 +1,12 @@ +[[cppverify::trusted]] int next(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1); + +int twice(int x) + cppverify::pre(x >= 0 && x < 50) + cppverify::post(cppverify::result == x + 2) +{ + int a = next(x); + int b = next(a); + return b; +} From 742558183db6338d41e4fe46a047aa271e21db74 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:43 +0530 Subject: [PATCH 90/99] test: Add the proof of cppverify_twice_edf933_missing_return_54ae7c80 by its named hypotheses. --- .../cppverify_twice_edf933_missing_return_54ae7c80.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean new file mode 100644 index 0000000000..d450f13548 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_missing_return_54ae7c80_proof : cppverify_twice_edf933_missing_return_54ae7c80 := by + apply cppverify_twice_edf933_missing_return_54ae7c80.of_readable + trivial From e9d625d5841f04b6e5e2c37a70e6e5b8315863a2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:44 +0530 Subject: [PATCH 91/99] test: Add the proof of cppverify_twice_edf933_postcondition_28de726e by its named hypotheses. --- ...verify_twice_edf933_postcondition_28de726e.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean new file mode 100644 index 0000000000..e1080ebc94 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean @@ -0,0 +1,14 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by + apply cppverify_twice_edf933_postcondition_28de726e.of_readable + intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 + obtain ⟨_, first⟩ := h_call_next_1 + obtain ⟨_, second⟩ := h_call_next_2 + subst h_result_1 h_b_1 second h_a_1 first + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + refine ⟨by omega, ?_⟩ + rw [BitVec.add_assoc] + rfl From d0ce5c96232e5a2a9426ec829a88bec97f243e36 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:44 +0530 Subject: [PATCH 92/99] test: Add the proof of cppverify_twice_edf933_precondition_51b3c1f0 by its named hypotheses. --- ...pverify_twice_edf933_precondition_51b3c1f0.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean new file mode 100644 index 0000000000..5c6b0e43e4 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean @@ -0,0 +1,14 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_precondition_51b3c1f0_proof : cppverify_twice_edf933_precondition_51b3c1f0 := by + apply cppverify_twice_edf933_precondition_51b3c1f0.of_readable + intro __heap_alloc_0 __heap_live_0 __local_call_1_1 a_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 + obtain ⟨range, called⟩ := h_call_next_1 + subst h_a_1 called + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 ⊢ + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 1).toInt = 1 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + have : (BitVec.ofInt 32 100).toInt = 100 := rfl + rw [BitVec.toInt_add_of_not_saddOverflow (by simp [BitVec.saddOverflow]; omega)] + omega From f86eb0ea97c0827677bed44f7c4a3dd933a0bdf9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:45 +0530 Subject: [PATCH 93/99] test: Add the proof of cppverify_twice_edf933_precondition_f0a3d715 by its named hypotheses. --- .../cppverify_twice_edf933_precondition_f0a3d715.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean new file mode 100644 index 0000000000..2607fff7eb --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean @@ -0,0 +1,10 @@ +import CppVerify.User + +theorem cppverify_twice_edf933_precondition_f0a3d715_proof : cppverify_twice_edf933_precondition_f0a3d715 := by + apply cppverify_twice_edf933_precondition_f0a3d715.of_readable + intro __heap_alloc_0 __heap_live_0 x_0 h_pre_1 h_null_1 h_null_2 + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 ⊢ + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + have : (BitVec.ofInt 32 100).toInt = 100 := rfl + omega From 12650d0bb3c6c5df9f76982d092becddf686c92c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:45 +0530 Subject: [PATCH 94/99] test: Check readable Lean goals, their bridges, and their stubs. --- clang/test/Verify/suite/lean_readable.cpp | 204 ++++++++++++++++++++++ 1 file changed, 204 insertions(+) create mode 100644 clang/test/Verify/suite/lean_readable.cpp diff --git a/clang/test/Verify/suite/lean_readable.cpp b/clang/test/Verify/suite/lean_readable.cpp new file mode 100644 index 0000000000..618ed8feb1 --- /dev/null +++ b/clang/test/Verify/suite/lean_readable.cpp @@ -0,0 +1,204 @@ +// REQUIRES: lean +// +// Each project goal also has a readable form, its assumptions as hypotheses +// named by where they come from, and a bridge from that form to the goal that +// the kernel checks with the generated file. A stub proves the goal through +// it. +// +// RUN: rm -rf %t && mkdir -p %t +// RUN: %cpp-verify --backend=lean --lean-project=%t/p %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT +// RUN: FileCheck %s --input-file=%t/p/CppVerify/Generated.lean +// RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_twice_edf933/cppverify_twice_edf933_postcondition_28de726e.lean --check-prefix=STUB +// RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_poly_c94108/cppverify_poly_c94108_postcondition_fde367c1.lean --check-prefix=LETS +// Every stub's names match its readable form: the project builds, with +// nothing admitted but the stubs. +// RUN: cd %t/p && lake build CppVerify.Check 2>&1 | FileCheck %s --check-prefix=STUBS --implicit-check-not=error +// +// Proofs that use the hypotheses by name certify. +// RUN: %cpp-verify --backend=lean --lean-project=%t/c %S/Inputs/lean_readable_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=TRUSTED +// RUN: cp %S/Inputs/lean_readable_proofs/*.lean %t/c/CppVerify/Proofs/cppverify_twice_edf933/ +// RUN: %cpp-verify --backend=lean --lean-project=%t/c --lean-certify %S/Inputs/lean_readable_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED +// +// A readable form that says less than its goal does not build: here the +// definition of b is replaced by the conclusion it should lead to. +// RUN: sed -i 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Generated.lean +// RUN: cd %t/p && not lake build CppVerify.Generated 2>&1 | FileCheck %s --check-prefix=BRIDGE + +int next(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} + +int twice(int x) + cppverify::pre(x >= 0 && x < 50) + cppverify::post(cppverify::result == x + 2) +{ + int a = next(x); + int b = next(a); + return b; +} + +int count_up(int n) + cppverify::pre(n >= 0 && n < 100) + cppverify::post(cppverify::result == n) +{ + int i = 0; + while (i < n) + cppverify::invariant(0 <= i && i <= n) + cppverify::decreases(n - i) + { + i = i + 1; + } + return i; +} + +void checked(int x) + cppverify::pre(x > 0) +{ + cppverify::check(x != 0); + cppverify::check(x >= 1); +} + +cppverify::spec int count(int n) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 0) +{ + return n <= 0 ? 0 : count(n - 1) + 1; +} + +cppverify::proof void counted(int n) + cppverify::post(count(n) + 1 > 0) +{ +} + +int positive(int x) + cppverify::post(!(x > 0) || cppverify::result > 0) +{ + return x; +} + +int read(const int *p) + cppverify::pre(cppverify::valid(p, 1)) + cppverify::post(cppverify::result == *p) +{ + return *p; +} + +int named(int x) + cppverify::pre(x >= 0 && x < 10) + cppverify::post(cppverify::result == 2 * x + 1) +{ + int h_x = x + 1; + x = x + h_x; + return x; +} + +int poly(int x) + cppverify::pre(x >= 0 && x < 10) + cppverify::post(cppverify::result == ((x + 1) * (x + 2) + (x + 3) * (x + 4)) * ((x + 5) * (x + 6) + (x + 7) * (x + 8))) +{ + return ((x + 1) * (x + 2) + (x + 3) * (x + 4)) * ((x + 5) * (x + 6) + (x + 7) * (x + 8)); +} + +// EXPORT: Exported: lean obligation: next +// EXPORT: Exported: lean obligation: twice +// EXPORT: Exported: lean obligation: count_up +// EXPORT: Exported: lean obligation: checked +// EXPORT: Exported: decreases: count +// EXPORT: Exported: lean obligation: counted +// EXPORT: Exported: lean obligation: positive +// EXPORT: Exported: lean obligation: read +// EXPORT: Exported: lean obligation: named +// EXPORT: Exported: lean obligation: poly + +// CHECK: theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b := +// CHECK-NEXT: (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl +// CHECK-NEXT: theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b := +// CHECK-NEXT: (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha)) + +// Calls of one callee are told apart; a definition is named by what it defines. +// CHECK: def cppverify_twice_edf933_postcondition_28de726e.readable : Prop := +// CHECK: (x_0 : BitVec 32), +// CHECK-NEXT: (h_pre_1 : (cppBvSle (BitVec.ofInt 32 (0)) x_0) ∧ (cppBvSlt x_0 (BitVec.ofInt 32 (50)))) → +// CHECK-NEXT: (h_null_1 : (heapSelectInt __heap_alloc_0 (0 : Int)) = (0 : Int)) → +// CHECK-NEXT: (h_null_2 : ¬(heapSelectBool __heap_live_0 (0 : Int))) → +// CHECK-NEXT: (h_call_next_1 : {{.*}} ∧ __local_call_1_1 = x_0 + (BitVec.ofInt 32 (1))) → +// CHECK-NEXT: (h_a_1 : a_1 = __local_call_1_1) → +// CHECK-NEXT: (h_call_next_2 : {{.*}} ∧ __local_call_2_1 = a_1 + (BitVec.ofInt 32 (1))) → +// CHECK-NEXT: (h_b_1 : b_1 = __local_call_2_1) → +// CHECK-NEXT: (h_result_1 : __result_1 = b_1) → +// CHECK-NEXT: ((x_0).toInt + (2 : Int) ≥ (-2147483648 : Int) ∧ (x_0).toInt + (2 : Int) ≤ (2147483647 : Int)) ∧ __result_1 = x_0 + (BitVec.ofInt 32 (2)) +// CHECK-EMPTY: +// CHECK-NEXT: theorem cppverify_twice_edf933_postcondition_28de726e.of_readable (h : cppverify_twice_edf933_postcondition_28de726e.readable) : cppverify_twice_edf933_postcondition_28de726e := +// CHECK-NEXT: fun __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 => +// CHECK-NEXT: cppverify_imp_or fun h_pre_1 => +// CHECK-NEXT: cppverify_imp_or fun h_null_1 => +// CHECK-NEXT: cppverify_not_imp_or fun h_null_2 => +// CHECK-NEXT: cppverify_imp_or fun h_call_next_1 => +// CHECK-NEXT: cppverify_imp_or fun h_a_1 => +// CHECK-NEXT: cppverify_imp_or fun h_call_next_2 => +// CHECK-NEXT: cppverify_imp_or fun h_b_1 => +// CHECK-NEXT: cppverify_imp_or fun h_result_1 => +// CHECK-NEXT: h __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 + +// A loop: its invariant, the condition of an iteration, the exact value of +// a machine operation, the value a path that skips the body keeps, and the +// exit. +// CHECK: def cppverify_count_up_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_i_1 : i_1 = (BitVec.ofInt 32 (0))) → +// CHECK-NEXT: (h_inv_1 : (cppBvSle (BitVec.ofInt 32 (0)) i_2) ∧ (cppBvSle i_2 n_0)) → +// CHECK-NEXT: (h_cond_1 : ¬__loop_choice_1 ∨ (cppBvSlt i_2 n_0)) → +// CHECK-NEXT: (h_exact_1 : ¬__loop_choice_1 ∨ {{.*}}) → +// CHECK-NEXT: (h_i_3 : ¬__loop_choice_1 ∨ i_3 = i_2 + (BitVec.ofInt 32 (1))) → +// CHECK-NEXT: (h_keep_1 : __loop_choice_1 ∨ i_3 = i_2) → +// CHECK-NEXT: (h_exit_1 : ¬__loop_choice_1) → +// CHECK-NEXT: (h_exit_2 : ¬(cppBvSlt i_2 n_0)) → +// CHECK-NEXT: (h_result_1 : __result_1 = i_2) → +// CHECK-NEXT: __result_1 = n_0 + +// A check proved before is a hypothesis of the next. +// CHECK: def cppverify_checked_{{[0-9a-f]+}}_assertion_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_null_2 : ¬(heapSelectBool __heap_live_0 (0 : Int))) → +// CHECK-NEXT: x_0 ≠ (BitVec.ofInt 32 (0)) +// CHECK: def cppverify_checked_{{[0-9a-f]+}}_assertion_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_check_1 : x_0 ≠ (BitVec.ofInt 32 (0))) → +// CHECK-NEXT: (cppBvSle (BitVec.ofInt 32 (1)) x_0) + +// A spec's proved postcondition at each application. +// CHECK: def cppverify_counted_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_spec_count_1 : (cppSpec_fn_5f5a35636f756e7469 (n_0).toInt) ≥ (0 : Int)) → +// CHECK-NEXT: (h_spec_count_2 : (cppSpec_fn_5f5a35636f756e7469 ((n_0).toInt - (1 : Int))) ≥ (0 : Int)) → + +// The postcondition's own disjunction is what remains to be shown. +// CHECK: def cppverify_positive_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_result_1 : __result_1 = x_0) → +// CHECK-NEXT: ¬(cppBvSlt (BitVec.ofInt 32 (0)) x_0) ∨ (cppBvSlt (BitVec.ofInt 32 (0)) __result_1) + +// Facts the verifier states at entry: an extent's, and where an object lies. +// CHECK: def cppverify_read_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_entry_1 : {{.*}}) → +// CHECK: (h_object_1 : p_0 = (0 : Int) ∨ {{.*}}) → + +// A hypothesis never takes a variable's name. +// CHECK: def cppverify_named_{{[0-9a-f]+}}_postcondition_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_x_1 : BitVec 32) +// CHECK: (h_h_x_1 : h_x_1 = x_0 + (BitVec.ofInt 32 (1))) → +// CHECK: (h_x_1_1 : x_1 = x_0 + h_x_1) → + +// STUB: theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by +// STUB-NEXT: apply cppverify_twice_edf933_postcondition_28de726e.of_readable +// STUB-NEXT: intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 +// STUB-NEXT: sorry + +// A large goal names its parts, which a proof introduces too. +// LETS: intro __heap_alloc_0 __heap_live_0 __result_1 x_0 __cppverify_term_1 {{.*}} h_pre_1 h_null_1 h_null_2 + +// STUBS: Build completed successfully + +// TRUSTED: Trusted: next (contract assumed, not verified) +// TRUSTED: Exported: lean obligation: twice +// CERTIFIED: Certified: twice [backend=Lean] [trusts=next] + +// BRIDGE: Generated.lean:{{[0-9]+}}:{{[0-9]+}}: Application type mismatch: The argument From 88604e626dfb5cc70baf6de3801732f17eb0d4f2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:45 +0530 Subject: [PATCH 95/99] docs: Describe readable Lean goals and their bridges in the architecture. --- docs/ARCHITECTURE.md | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 62c523ef13..8391cc3d27 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1584,7 +1584,33 @@ uses when the source around it changes. 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 +- **Readable goals.** `makeGoal` (`Obligation.cpp`) marks each `Or` it + builds, `!A || rest`, with where `A` comes from (`LogicExpr::Premise`, + like `Patterns` outside the term's meaning, its hash, and archives, and + kept by the clones and the in-place simplifier). The passivizer records + the origin of every assumption it emits (`PassiveStmt::Origin`, from a + current origin each statement kind sets and its parts refine: + `def`, `call:f`, `inv`, `cond`, `exit`, `keep`, `exact`, `check`, + `spec:f`, ...) and of each entry assumption (`PassiveProgram::EntryOrigins`: + `pre` for a written precondition, `entry` for a generated one, `null`, + `object`); spec checks built elsewhere default to `fact`. The Lean adapter + peels the marked chain into `G.readable`: `∀ vars axioms, let …; (h_pre_1 + : A1) → … → C`, a hypothesis being the operand its `Or` negates (or `¬B` + where simplification folded `¬¬B` to `B`), named `h__`, a + definition `h_`, never a binder's name; its `let`s are the large + subterms of the hypotheses and the conclusion. The bridge + `G.of_readable : G.readable → G` is a term, one prelude lemma per + hypothesis (`cppverify_imp_or : (a → b) → ¬a ∨ b`, or + `cppverify_not_imp_or : (¬a → b) → a ∨ b`), so the kernel checks with + `Generated.lean` that the readable form implies the goal: a printer bug in + it fails the build, never certifies. `LeanProjectGoal::Intros` gives the + stub its `intro` list. On the 375 suite exports, the 351 that built + before still build, with every bridge. + +`lean_readable.cpp` checks the readable form of each kind of assumption, +the bridge, the stubs (every one builds), a proof by hypothesis names that +certifies, and a readable form that says less than its goal, which fails at +its bridge. `lean_identity.test` walks one project through each case (insertion and reordering, renames of two functions at once, a changed statement, a removed function and its return, fallback runs, pruning, and a 0.1 project with proofs, stubs, and a proof of a goal that is gone) and certifies it after From 96c1d8d392e1ba66a98a5e7f9e5847daf8c01c4c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:46 +0530 Subject: [PATCH 96/99] docs: State that Lean goals have readable forms checked by a bridge in the design. --- docs/DESIGN.md | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index b8c62faf8f..124ba4bd64 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1896,8 +1896,14 @@ goals (a rename), moved with the generated names it uses; else a 0.1 file 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 +leaves unresolved and leaves every other proof where it is. Each goal `G` +also has a readable form `G.readable`, its assumptions as hypotheses named +by where they come from (as Frama-C's WP labels the steps of a sequent and +Vermilion names its hypotheses), and a bridge `G.of_readable : G.readable → +G`, generated and kernel-checked with the generated file: the canonical goal +stays what certification checks and identity hashes, and a printer bug in +the readable form cannot certify anything. A stub applies the bridge and +introduces every name. Initial generation is `Exported`. Certification compiles the user module and every active proof with `sorry` as an error, then checks aggregate theorem types and axiom dependencies. Only foundational Lean axioms are permitted; user `axiom`/`opaque` proof shortcuts, stale proof types, From db814a4f603e629bcf6345c176c33c3dd3d7bf31 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:46 +0530 Subject: [PATCH 97/99] docs: Show Lean goals as hypotheses in chapter 17. --- .../part-ii/ch17-backends-modular-calls.rst | 108 ++++++++++++++++++ 1 file changed, 108 insertions(+) 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 2fe0cb898f..4f14e14faa 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -309,6 +309,114 @@ one does (``[trusts=f]``, ``[partial]``). It also gets the same vacuity checks, run with Z3: a goal that holds only because no execution reaches it is ``Certified: f [backend=Lean] [vacuous]``, with a warning. +Goals as hypotheses +~~~~~~~~~~~~~~~~~~~ + +Next to each goal, ``Generated.lean`` states it as hypotheses and a +conclusion. Each hypothesis is an assumption the goal makes, named by where +it comes from, and a bridge from that form to the goal is proved in the same +file. For this file: + +.. code-block:: cpp + + [[cppverify::trusted]] int next(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1); + + int twice(int x) + cppverify::pre(x >= 0 && x < 50) + cppverify::post(cppverify::result == x + 2) + { + int a = next(x); + int b = next(a); + return b; + } + +the postcondition of ``twice`` reads: + +.. code-block:: lean4 + + def cppverify_twice_edf933_postcondition_28de726e.readable : Prop := + ∀ + (__heap_alloc_0 : CppHeap) + (__heap_live_0 : CppHeap) + (__local_call_1_1 : BitVec 32) + (__local_call_2_1 : BitVec 32) + (__result_1 : BitVec 32) + (a_1 : BitVec 32) + (b_1 : BitVec 32) + (x_0 : BitVec 32), + (h_pre_1 : (cppBvSle (BitVec.ofInt 32 (0)) x_0) ∧ (cppBvSlt x_0 (BitVec.ofInt 32 (50)))) → + (h_null_1 : (heapSelectInt __heap_alloc_0 (0 : Int)) = (0 : Int)) → + (h_null_2 : ¬(heapSelectBool __heap_live_0 (0 : Int))) → + (h_call_next_1 : ((x_0).toInt + (1 : Int) ≥ (-2147483648 : Int) ∧ (x_0).toInt + (1 : Int) ≤ (2147483647 : Int)) ∧ __local_call_1_1 = x_0 + (BitVec.ofInt 32 (1))) → + (h_a_1 : a_1 = __local_call_1_1) → + (h_call_next_2 : ((a_1).toInt + (1 : Int) ≥ (-2147483648 : Int) ∧ (a_1).toInt + (1 : Int) ≤ (2147483647 : Int)) ∧ __local_call_2_1 = a_1 + (BitVec.ofInt 32 (1))) → + (h_b_1 : b_1 = __local_call_2_1) → + (h_result_1 : __result_1 = b_1) → + ((x_0).toInt + (2 : Int) ≥ (-2147483648 : Int) ∧ (x_0).toInt + (2 : Int) ≤ (2147483647 : Int)) ∧ __result_1 = x_0 + (BitVec.ofInt 32 (2)) + +The names say where each assumption comes from: + +- ``h_pre_``: a precondition the function states; ``h_entry_``: one + the verifier adds, such as an extent's; ``h_null_`` and + ``h_object_``: the null object and where an object lies; +- ``h_``: the definition of that variable, here ``a_1`` and + ``b_1`` and the value returned, ``__result_1``; +- ``h_call__``: what a call of the callee gives, numbered in + order, here both calls of ``next``; +- ``h_inv_``, ``h_cond_``, ``h_exit_``: a loop's invariant, the + condition of an iteration, and how it ended; +- ``h_exact_``: the exact value of a machine operation that does not + overflow; ``h_keep_``: the value of a variable on a path that skips its + assignment; +- ``h_check_``: a ``cppverify::check`` proved before; + ``h_spec__``: a spec's proved postcondition at an application. + +The numbers count within the goal, so a line added to the source renames no +hypothesis. A disjunction the program wrote, such as +``cppverify::post(!(x > 0) || cppverify::result > 0)``, stays in the +conclusion. The bridge, +``cppverify_twice_edf933_postcondition_28de726e.of_readable``, proves the goal +from this form; Lean checks it when it builds the generated file, so a +readable form that said less than its goal would fail there, not certify. A +new proof file starts from it, with every name introduced: + +.. code-block:: lean4 + + import CppVerify.User + + theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by + apply cppverify_twice_edf933_postcondition_28de726e.of_readable + intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 + sorry + +and a proof uses the hypotheses by name: + +.. code-block:: lean4 + + obtain ⟨_, first⟩ := h_call_next_1 + obtain ⟨_, second⟩ := h_call_next_2 + subst h_result_1 h_b_1 second h_a_1 first + simp only [cppBvSle, cppBvSlt, BitVec.sle, BitVec.slt, decide_eq_true_eq] at h_pre_1 + have : (BitVec.ofInt 32 0).toInt = 0 := rfl + have : (BitVec.ofInt 32 50).toInt = 50 := rfl + refine ⟨by omega, ?_⟩ + rw [BitVec.add_assoc] + rfl + +With the two calls' preconditions proved the same way and ``trivial`` for +the return check, +``cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp`` +prints: + +.. code-block:: text + + file.cpp:1:28: Trusted: next (contract assumed, not verified) + Certified: twice [backend=Lean] [trusts=next] + +A proof of the goal itself, as the one for ``small`` above, checks as well. + Proofs that follow their goals ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From 7d7079169d979d556005a8853e8b3512c912aef6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:46 +0530 Subject: [PATCH 98/99] docs: Document readable Lean goals in the tooling reference. --- website/source/language/tooling.rst | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 47f4b1caca..38d255fdf4 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -274,7 +274,13 @@ Backends ``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 + (:doc:`../book/part-ii/ch17-backends-modular-calls`). Each goal + ``G`` also has a readable form, ``G.readable``, its assumptions as + hypotheses named by where they come from (``h_pre_1``, + ``h_call_next_2``, ``h_x_1`` for the definition of ``x_1``), and a + bridge ``G.of_readable : G.readable → G`` that the kernel checks with + the generated file, so a proof of either form proves ``G``. A stub + applies the bridge and introduces every name. Each goal means what its obligation means: every operator keeps its grouping under Lean's precedence, a numeral has its type (``Nat`` would read ``2 - 3`` as 0), a Boolean is a proposition From 0e994eb75051320af1994bc82cc97e2fd61cc37b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 14:22:47 +0530 Subject: [PATCH 99/99] docs: Note that Lean goals read as named hypotheses. --- website/source/release-notes.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 11fd40656e..f3cbd5c605 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -296,6 +296,17 @@ what its solver settles alone. ``--lean-prune-stale`` deletes what ``Stale/`` keeps. A project 0.1 generated is moved to the new names with its proofs (:doc:`book/part-ii/ch17-backends-modular-calls`). +**Lean goals as hypotheses.** A Lean goal was one disjunction, the negation of +every assumption before what it must show, and a proof picked its way to the +conclusion by counting disjuncts (``right; right; right``) with nothing to +say which was the precondition and which a callee's postcondition. Each goal +now also has a readable form, its assumptions as hypotheses named by where +they come from, such as ``h_pre_1``, ``h_call_next_2``, ``h_inv_1``, or +``h_x_1`` for the definition of ``x_1``, and a bridge from that form to the +goal, which the kernel checks with the generated file. A new proof file +starts from the readable form with every name introduced; a proof of the +goal itself still checks (:doc:`book/part-ii/ch17-backends-modular-calls`). + **Lean 4.35.0.** Lean projects pin ``leanprover/lean4:v4.35.0``. A project 0.1 generated, pinned to ``v4.32.2``, moves to the new pin the next time cpp-verify writes it, with a warning; a proof that no longer builds needs updating for that