From c2a2a5766890f6367dc15d553c22d6c8a763e793 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 10:52:18 +0530 Subject: [PATCH 01/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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 -----