Merge pull request #56 from SwayamInSync/fix/lean-pin

verify: Pin Lean 4.35.0, move projects 0.1 pinned, and certify with the pinned toolchain

Author: SwayamInSync

.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:

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.
 

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";

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<std::string> 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<std::string> Arguments,
                        llvm::StringRef Stage) -> llvm::Expected<std::string> {
-      std::vector<std::string> Command = {"lake", "--dir=" + Root};
+      std::vector<std::string> 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<std::string> 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)

clang/test/Verify/suite/Inputs/lean_toolchain.cpp

@@ -0,0 +1,3 @@
+void trivial()
+  cppverify::post(true)
+{}

clang/test/Verify/suite/lean_project.cpp

@@ -6,14 +6,21 @@
 // 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
 // RUN: echo '/- 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
 // 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

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)

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

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`).
 

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