Remove the Mathlib dependency from the Lean packages

.github/workflows/README.md

@@ -141,11 +141,11 @@ Runs Lean verification for the repository, with each package checked in an isola
 All five packages (consensus, common, consistency, disaster-recovery, and kv) run in one matrix.
 Package checks use the `gha-vmss-d16av7-ci` pool and trace replays use `gha-vmss-d16av7-ci-b`, both in Ubuntu 26.04 containers.
 Native trace captures remain on `gha-vmss-d16av7-ci-c` with Azure Linux containers, and the lightweight final gate uses GitHub-hosted Ubuntu.
-Each matrix job caches its third-party dependency checkouts and build outputs, including Mathlib and (where used) leanfmt, using GitHub Actions caching.
+Each matrix job caches its third-party dependency checkouts and build outputs, leanfmt and (for disaster-recovery and kv) Batteries, using GitHub Actions caching.
 Caches are isolated by package and runner architecture and invalidated by changes to the Ubuntu version, Lean toolchain, package and common dependency manifests/configuration, or reusable workflow.
-CCF package and common build outputs are not cached, and all verification steps still run, including Mathlib's upstream cache retrieval.
+CCF package and common build outputs are not cached, and all verification steps still run.
 CCF consensus, KV, and consistency trace captures run in parallel with package checks.
-Three independent trace-validation jobs each restore Mathlib caches, build their own replayer, download the corresponding capture artifacts, and replay the traces without depending on the package matrix.
+Three independent trace-validation jobs each build their own replayer, download the corresponding capture artifacts, and replay the traces without depending on the package matrix.
 Consistency capture reuses the existing `consistency_trace_validation` e2e test, and its replay job also checks the consistency replay fixtures, including election and rollback traces.
 A final summary job requires every package and trace job to succeed.
 
@@ -175,12 +175,23 @@ The KV package job checks `lean/kv/replayer/check-fixtures.sh` against the KV fi
 The dedicated replay job builds `kv-replay` separately to validate the captured traces; no replay executables are transferred between jobs.
 
 After the build, `scripts/lean-format-checks.sh` checks every tracked `.lean` file with the pinned leanfmt dependency.
-The workflow runs on pull requests that change `lean/`, any `.lean` file, the formatter script, or the workflow.
+The workflow runs on pull requests that change `lean/` (except `lean/mathlib-equivalence/`), any `.lean` file, the formatter script, or the workflow.
 It also runs on changes to the C++ sources and trace runners checked against the CCF consensus and KV models: `src/consensus/aft/`, the CCF consensus scenario tests, `src/kv/`, the public KV and transaction headers, and the KV trace runner.
 See the [local formatting commands](../../lean/disaster-recovery/README.md#formatting) to apply fixes.
 
 File: `lean.yml`
-3rd party dependencies: Mathlib and leanfmt (pinned in the Lake package), and elan.
+3rd party dependencies: leanfmt and Batteries (pinned in the Lake packages), and elan.
+
+# Lean Mathlib equivalence
+
+Proves that the local replacements for Mathlib definitions in `lean/common` (`CCF.Seq`, `CCF.Finset` and `CCF.Function`) and the consensus successor ranking are equivalent to the Mathlib definitions they replaced.
+The proofs live in the separate `lean/mathlib-equivalence` package, which is the only Lean package that depends on Mathlib; the main Lean workflow does not schedule it.
+The job restores Mathlib's upstream build cache, runs `lake check --inadvisably-no-sandbox` to build the proofs and replay them through the kernel with only the standard axioms, and checks the package's formatting.
+It caches third-party dependency checkouts and build outputs like the main Lean package jobs.
+The workflow runs only on pull requests that change the replacement definitions, the equivalence package, the Lean toolchain, the formatter script, or the workflow, and can be run manually.
+
+File: `lean-mathlib-equivalence.yml`
+3rd party dependencies: Mathlib (pinned in the Lake package), leanfmt and elan.
 
 # Vendored Dependency Verification
 

.github/workflows/lean-mathlib-equivalence.yml

@@ -0,0 +1,76 @@
+name: "Lean Mathlib equivalence"
+
+# Proves that the local replacements for Mathlib definitions are equivalent to
+# Mathlib's, so this only runs when those definitions or the proofs change.
+on:
+  pull_request:
+    paths:
+      - "lean/common/CCF/Finset.lean"
+      - "lean/common/CCF/Function.lean"
+      - "lean/common/CCF/Seq.lean"
+      - "lean/consensus/Consensus/Model/Node.lean"
+      - "lean/mathlib-equivalence/**"
+      - "lean/lean-toolchain"
+      - "scripts/lean-format-checks.sh"
+      - ".github/workflows/lean-mathlib-equivalence.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  equivalence:
+    name: Prove equivalence with Mathlib
+    runs-on: [gha-vmss-d16av7-ci]
+    container:
+      image: ubuntu:26.04
+      options: --user root
+    timeout-minutes: 90
+    defaults:
+      run:
+        shell: bash
+
+    steps:
+      - name: Install container prerequisites
+        run: |
+          set -euo pipefail
+          apt-get update
+          DEBIAN_FRONTEND=noninteractive apt-get install -y \
+            ca-certificates git curl tar zstd build-essential libgmp-dev elan
+          echo "ELAN_HOME=$RUNNER_TEMP/elan" >> "$GITHUB_ENV"
+
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Install Lean
+        run: |
+          set -euo pipefail
+          git config --global --add safe.directory "$GITHUB_WORKSPACE"
+          echo "TMPDIR=$RUNNER_TEMP" >> "$GITHUB_ENV"
+          elan run --install "$(cat lean/lean-toolchain)" lean --version
+
+      - name: Restore dependency builds
+        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
+        with:
+          path: lean/mathlib-equivalence/.lake/packages
+          key: lean-deps-v2-vmss-ubuntu-26.04-${{ runner.arch }}-mathlib-equivalence-${{ hashFiles('lean/lean-toolchain', 'lean/mathlib-equivalence/lake-manifest.json', 'lean/mathlib-equivalence/lakefile.toml', 'lean/common/lake-manifest.json', 'lean/common/lakefile.toml', 'lean/consensus/lake-manifest.json', 'lean/consensus/lakefile.toml', '.github/workflows/lean-mathlib-equivalence.yml') }}
+
+      - name: Restore Mathlib cache
+        working-directory: lean/mathlib-equivalence
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
+      - name: Build, kernel and axiom check
+        working-directory: lean/mathlib-equivalence
+        run: |
+          set -euo pipefail
+          lake check --inadvisably-no-sandbox
+
+      - name: Check formatting
+        run: |
+          set -euo pipefail
+          ./scripts/lean-format-checks.sh mathlib-equivalence

.github/workflows/lean-package.yml

@@ -62,12 +62,6 @@ jobs:
           path: lean/${{ inputs.package }}/.lake/packages
           key: lean-deps-v2-vmss-ubuntu-26.04-${{ runner.arch }}-${{ inputs.package }}-${{ hashFiles('lean/lean-toolchain', format('lean/{0}/lake-manifest.json', inputs.package), format('lean/{0}/lakefile.toml', inputs.package), 'lean/common/lake-manifest.json', 'lean/common/lakefile.toml', '.github/workflows/lean-package.yml') }}
 
-      - name: Restore Mathlib cache
-        working-directory: lean/${{ inputs.package }}
-        run: |
-          set -euo pipefail
-          lake exe cache get
-
       - name: Build, kernel and axiom check
         working-directory: lean/${{ inputs.package }}
         run: |

.github/workflows/lean.yml

@@ -20,6 +20,8 @@ on:
       - "CMakeLists.txt"
       - ".github/workflows/lean.yml"
       - ".github/workflows/lean-package.yml"
+      # Checked by lean-mathlib-equivalence.yml.
+      - "!lean/mathlib-equivalence/**"
   workflow_dispatch:
 
 concurrency:
@@ -240,12 +242,6 @@ jobs:
           git config --global --add safe.directory "$GITHUB_WORKSPACE"
           elan run --install "$(cat lean/lean-toolchain)" lean --version
 
-      - name: Restore Mathlib cache
-        working-directory: lean/consensus
-        run: |
-          set -euo pipefail
-          lake exe cache get
-
       - name: Build CCF consensus replay
         working-directory: lean/consensus
         run: |
@@ -323,7 +319,9 @@ jobs:
           import pathlib
 
           expected = {"consensus", "common", "consistency", "disaster-recovery", "kv"}
-          actual = {config.parent.name for config in pathlib.Path("lean").glob("*/lakefile.toml")}
+          # Checked by lean-mathlib-equivalence.yml.
+          separate = {"mathlib-equivalence"}
+          actual = {config.parent.name for config in pathlib.Path("lean").glob("*/lakefile.toml")} - separate
           if actual != expected:
               raise SystemExit(
                   f"::error::Lean package inventory changed: expected {sorted(expected)}, got {sorted(actual)}; "
@@ -362,12 +360,6 @@ jobs:
           git config --global --add safe.directory "$GITHUB_WORKSPACE"
           elan run --install "$(cat lean/lean-toolchain)" lean --version
 
-      - name: Restore Mathlib cache
-        working-directory: lean/kv
-        run: |
-          set -euo pipefail
-          lake exe cache get
-
       - name: Build KV replay
         working-directory: lean/kv
         run: |
@@ -421,12 +413,6 @@ jobs:
           git config --global --add safe.directory "$GITHUB_WORKSPACE"
           elan run --install "$(cat lean/lean-toolchain)" lean --version
 
-      - name: Restore Mathlib cache
-        working-directory: lean/consistency
-        run: |
-          set -euo pipefail
-          lake exe cache get
-
       - name: Build consistency replay
         working-directory: lean/consistency
         run: |

doc/architecture/verification.rst

@@ -84,6 +84,8 @@ The :ccf_repo:`Lean workflow <.github/workflows/lean.yml>` runs on pull requests
 
 The disaster recovery traces are replayed by the SNP Genoa job in the main CI workflow instead, since that is where the recovery scenarios run.
 
+A separate ``Lean Mathlib equivalence`` workflow proves that the replacements for Mathlib definitions in ``lean/common`` are equivalent to the Mathlib originals, and runs only when those definitions change; see :ccf_repo:`lean/mathlib-equivalence/README.md`.
+
 Running locally
 ---------------
 
@@ -93,7 +95,6 @@ From a package directory under ``lean/``, the common checks are:
 
 .. code-block:: bash
 
-    lake exe cache get
     lake build --wfail --fail-fast
     lake check --inadvisably-no-sandbox
     lake exe check-imports

doc/build_apps/kv/semantics.rst

@@ -221,7 +221,6 @@ Lean is pinned by ``lean/kv/lean-toolchain`` and is independent of normal CCF bu
 .. code-block:: bash
 
    cd lean/kv
-   lake exe cache get
    lake build --wfail
    cd ../..
    cmake -S . -B build-kv-trace -GNinja \

lean/AGENT.md

@@ -35,7 +35,8 @@ Within a model's library directory, use this layout:
   `Properties.lean` publicly imports the types and helpers needed to understand its statements and privately imports proof implementations.
 
 Write the full logical statement in each public safety theorem and existential witness lemma, rather than defining a separate named proposition.
-Use the `theorem` declaration keyword for public safety claims and `lemma` for their existential `_witness` declarations, including the witness implementations under `Proofs/`.
+Declare public safety claims and their existential witnesses with the `theorem` keyword, since Lean core has no `lemma` command.
+Name each witness after its safety theorem with a `_witness` suffix, including the witness implementations under `Proofs/`.
 Keep each proof body a one-line `by exact Proofs.<implementation>` reference, and place each witness lemma next to its corresponding safety theorem.
 For example:
 

lean/common/CCF.lean

@@ -3,6 +3,11 @@ module  -- shake: keep-all --deprecated_module: ignore
 public import CCF.Architecture
 public import CCF.Capabilities
 public import CCF.Execution
+public import CCF.Finset
+public import CCF.Function
 public import CCF.MultiNodeTransitionSystem
 public import CCF.Parsec
+public import CCF.Proofs.Execution
+public import CCF.Proofs.Finset
+public import CCF.Seq
 public import CCF.TransitionSystem

lean/common/CCF/Architecture.lean

@@ -8,6 +8,15 @@ namespace CCF.Architecture
 
 open Lean
 
+/-- Check an import against the layers of the shared `CCF` modules: only the `CCF` entrypoint
+and other `CCF.Proofs` modules can import `CCF.Proofs`. -/
+def allowedCommonImport (owner dependency : Name) : Bool :=
+  let proofs := `CCF.Proofs
+  !(`CCF).isPrefixOf owner
+  || owner == `CCF
+  || proofs.isPrefixOf owner
+  || !proofs.isPrefixOf dependency
+
 /-- Check an import against the standard layers of the specification rooted at `root`. -/
 def allowedImport (root owner dependency : Name) : Bool :=
   let model := root ++ `Model
@@ -16,7 +25,9 @@ def allowedImport (root owner dependency : Name) : Bool :=
   if (`CCF).isPrefixOf owner then
     !root.isPrefixOf dependency
   else if !root.isPrefixOf dependency then
-    true
+    -- The `CCF` entrypoint reexports `CCF.Proofs`, so models must import definitions directly.
+    !(model.isPrefixOf owner
+      && ((`CCF.Proofs).isPrefixOf dependency || dependency == `CCF))
   else if model.isPrefixOf owner then
     model.isPrefixOf dependency && (owner == model || dependency != model)
   else if owner == properties then
@@ -33,12 +44,14 @@ def allowedImport (root owner dependency : Name) : Bool :=
   else
     true
 
-/-- Reject forbidden imports in an environment, including private transitive imports. -/
+/-- Reject forbidden imports in an environment, including private transitive imports. The
+shared `CCF` root is checked only against the common layers. -/
 def checkImports (root : Name) (environment : Environment) : Except String Unit := do
   let header := environment.header
   for (owner, data) in header.moduleNames.zip header.moduleData do
     for dependency in data.imports do
-      unless allowedImport root owner dependency.module do
+      unless allowedCommonImport owner dependency.module
+              && (root == `CCF || allowedImport root owner dependency.module) do
         throw s!"Forbidden layer dependency: {owner} imports {dependency.module}"
 
 end CCF.Architecture