From 26a35c9fa24a764b616387c556db1f7d79d60520 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Thu, 1 Oct 2026 16:14:51 +0200
Subject: [PATCH 1/7] misc/lean: add a Lean 4 project, toolchain image, and CI
 step

Add a Lake project in misc/lean for Lean 4 models of Materialize, with a
sample model of update collections that proves consolidation preserves
multiplicities and leaves no zero diffs. warningAsError makes any sorry
fail the build.

The lean mzbuild image installs the toolchain pinned in lean-toolchain
and builds the project's dependencies into the image. It copies only
lean-toolchain, lakefile.toml and lake-manifest.json from misc/lean, so
editing a model reuses the published image. The lean composition copies
the mounted sources next to the baked dependencies and runs lake, and a
new CI step runs it.

Fix the mzbuild copy pre-image, which reported its inputs relative to
the source directory instead of the repository root, so fingerprinting
any image that used it failed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 ci/test/lint-main/checks/check-copyright.sh |   1 +
 ci/test/pipeline.template.yml               |  12 ++
 misc/images/lean/.gitignore                 |   3 +
 misc/images/lean/Dockerfile                 |  64 +++++++++
 misc/images/lean/mz-lake                    |  23 +++
 misc/images/lean/mzbuild.yml                |  26 ++++
 misc/lean/.gitignore                        |   1 +
 misc/lean/Mz.lean                           |  10 ++
 misc/lean/Mz/Collection.lean                | 146 ++++++++++++++++++++
 misc/lean/README.md                         |  32 +++++
 misc/lean/lake-manifest.json                |   5 +
 misc/lean/lakefile.toml                     |  17 +++
 misc/lean/lean-toolchain                    |   1 +
 misc/lean/mzcompose                         |  14 ++
 misc/lean/mzcompose.py                      |  32 +++++
 misc/python/materialize/mzbuild.py          |   8 +-
 16 files changed, 393 insertions(+), 2 deletions(-)
 create mode 100644 misc/images/lean/.gitignore
 create mode 100644 misc/images/lean/Dockerfile
 create mode 100755 misc/images/lean/mz-lake
 create mode 100644 misc/images/lean/mzbuild.yml
 create mode 100644 misc/lean/.gitignore
 create mode 100644 misc/lean/Mz.lean
 create mode 100644 misc/lean/Mz/Collection.lean
 create mode 100644 misc/lean/README.md
 create mode 100644 misc/lean/lake-manifest.json
 create mode 100644 misc/lean/lakefile.toml
 create mode 100644 misc/lean/lean-toolchain
 create mode 100755 misc/lean/mzcompose
 create mode 100644 misc/lean/mzcompose.py

diff --git a/ci/test/lint-main/checks/check-copyright.sh b/ci/test/lint-main/checks/check-copyright.sh
index 7ed9a509609a5..d415a11ddfb6a 100755
--- a/ci/test/lint-main/checks/check-copyright.sh
+++ b/ci/test/lint-main/checks/check-copyright.sh
@@ -32,6 +32,7 @@ copyright_files=$(grep -vE \
     -e '(^|/)Cargo\.lock$' \
     -e '(^|/)types\.lock$' \
     -e '(^|/)\.mzprofile$' \
+    -e '(^|/)lean-toolchain$' \
     -e '^src/mz-deploy/src/cli/scaffold/gitignore$' \
     -e '^test/mz-deploy/projects/multi-profile/v1/models/app/core/ambiguous\.sql$' \
     -e '^about\.toml$' \
diff --git a/ci/test/pipeline.template.yml b/ci/test/pipeline.template.yml
index e64cff9510b85..07a48b84b491c 100644
--- a/ci/test/pipeline.template.yml
+++ b/ci/test/pipeline.template.yml
@@ -668,6 +668,18 @@ steps:
     agents:
       queue: hetzner-aarch64-4cpu-8gb
 
+  - id: lean
+    label: Lean models
+    depends_on: build-aarch64
+    timeout_in_minutes: 30
+    plugins:
+      - ./ci/plugins/mzcompose:
+          composition: lean
+    agents:
+      queue: hetzner-aarch64-4cpu-8gb
+    coverage: skip
+    sanitizer: skip
+
   - id: mcp
     label: MCP e2e
     depends_on: build-aarch64
diff --git a/misc/images/lean/.gitignore b/misc/images/lean/.gitignore
new file mode 100644
index 0000000000000..13d97841216ee
--- /dev/null
+++ b/misc/images/lean/.gitignore
@@ -0,0 +1,3 @@
+/lean-toolchain
+/lakefile.toml
+/lake-manifest.json
diff --git a/misc/images/lean/Dockerfile b/misc/images/lean/Dockerfile
new file mode 100644
index 0000000000000..641f31442f8a4
--- /dev/null
+++ b/misc/images/lean/Dockerfile
@@ -0,0 +1,64 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+# Lean 4 toolchain for the Lake project in `misc/lean`. The toolchain comes
+# from that project's `lean-toolchain`, so a local elan install and this image
+# use the same Lean version. The project's dependencies are built into
+# `/workspace/.lake` at image build time.
+
+MZFROM debian-base
+
+ARG ELAN_VERSION=v4.2.4
+
+ENV ELAN_HOME=/opt/elan
+ENV PATH=$ELAN_HOME/bin:$PATH
+
+RUN apt-get update \
+    && TZ=UTC DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends \
+        ca-certificates \
+        curl \
+        git \
+    && apt-get clean \
+    && rm -rf /var/lib/apt/lists/*
+
+COPY lean-toolchain /workspace/
+
+RUN case "$(uname -m)" in \
+        x86_64) triple=x86_64-unknown-linux-gnu; sha256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 ;; \
+        aarch64) triple=aarch64-unknown-linux-gnu; sha256=05febd124d84ebf994b2e7479922a5650b1e950c17ae3bd1ddd776b65bb72bf9 ;; \
+        *) echo "unsupported architecture $(uname -m)" >&2; exit 1 ;; \
+    esac \
+    && curl -fsSL -o /tmp/elan.tar.gz \
+        "https://github.com/leanprover/elan/releases/download/$ELAN_VERSION/elan-$triple.tar.gz" \
+    && echo "$sha256  /tmp/elan.tar.gz" | sha256sum -c - \
+    && tar -C /tmp -xzf /tmp/elan.tar.gz \
+    && /tmp/elan-init -y --no-modify-path --default-toolchain "$(cat /workspace/lean-toolchain)" \
+    && rm /tmp/elan.tar.gz /tmp/elan-init \
+    && chmod -R a+rX "$ELAN_HOME" \
+    && lean --version
+
+# Lake refuses dependency checkouts owned by a different uid than the one
+# running it, and re-clones them instead.
+RUN git config --system --add safe.directory '*'
+
+WORKDIR /workspace
+
+COPY lakefile.toml lake-manifest.json /workspace/
+
+# Builds the dependency closure against an empty placeholder library.
+RUN mkdir Mz \
+    && touch Mz.lean \
+    && lake build \
+    && rm -rf Mz Mz.lean .lake/build \
+    && chmod -R a+rwX /workspace
+
+COPY mz-lake /usr/local/bin/
+
+ENTRYPOINT ["mz-lake"]
+CMD ["build"]
diff --git a/misc/images/lean/mz-lake b/misc/images/lean/mz-lake
new file mode 100755
index 0000000000000..392c9fafcc2be
--- /dev/null
+++ b/misc/images/lean/mz-lake
@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# mz-lake: copy the Lake project mounted at /src into /workspace and run
+# `lake` there with the given arguments.
+
+set -euo pipefail
+
+# Mounting the project over /workspace would hide /workspace/.lake, which
+# holds the dependency closure built into the image. The host's own .lake is
+# skipped for the same reason.
+tar -C /src --exclude=./.lake -cf - . | tar -C /workspace -xf -
+
+cd /workspace
+exec lake "$@"
diff --git a/misc/images/lean/mzbuild.yml b/misc/images/lean/mzbuild.yml
new file mode 100644
index 0000000000000..9c438548ba87d
--- /dev/null
+++ b/misc/images/lean/mzbuild.yml
@@ -0,0 +1,26 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+name: lean
+description: Lean 4 toolchain and dependency closure for the models in misc/lean.
+# Only the files that pin the toolchain and the dependencies are copied, so
+# editing a model does not change the image fingerprint.
+pre-image:
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lean-toolchain
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lakefile.toml
+  - type: copy
+    source: misc/lean
+    destination: .
+    matching: lake-manifest.json
diff --git a/misc/lean/.gitignore b/misc/lean/.gitignore
new file mode 100644
index 0000000000000..bfb30ec8c762c
--- /dev/null
+++ b/misc/lean/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/misc/lean/Mz.lean b/misc/lean/Mz.lean
new file mode 100644
index 0000000000000..d0ffff89084fe
--- /dev/null
+++ b/misc/lean/Mz.lean
@@ -0,0 +1,10 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+
+import Mz.Collection
diff --git a/misc/lean/Mz/Collection.lean b/misc/lean/Mz/Collection.lean
new file mode 100644
index 0000000000000..c8caab8944cee
--- /dev/null
+++ b/misc/lean/Mz/Collection.lean
@@ -0,0 +1,146 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+
+/-!
+# Collections of updates
+
+A collection is a list of `(record, diff)` updates. Its meaning is the
+multiplicity of each record, the sum of that record's diffs. Two collections
+are equivalent when they agree on every multiplicity, regardless of how the
+updates are ordered or split.
+
+`consolidate` merges updates to the same record and drops the ones that cancel.
+It is correct when it preserves every multiplicity and leaves no zero diff.
+-/
+
+namespace Mz
+
+abbrev Collection (α : Type) := List (α × Int)
+
+namespace Collection
+
+variable {α : Type} [DecidableEq α]
+
+/-- The multiplicity of `x` in `c`. -/
+def count : Collection α → α → Int
+  | [], _ => 0
+  | (a, d) :: rest, x => (if a = x then d else 0) + count rest x
+
+/-- Flips the sign of every diff. -/
+def negate (c : Collection α) : Collection α :=
+  c.map fun (a, d) => (a, -d)
+
+/-- Adds `d` to the update for `a`, dropping that update if it cancels. -/
+def insert (a : α) (d : Int) : Collection α → Collection α
+  | [] => if d = 0 then [] else [(a, d)]
+  | (b, e) :: rest =>
+    if b = a then
+      if d + e = 0 then rest else (a, d + e) :: rest
+    else
+      (b, e) :: insert a d rest
+
+/-- Merges updates to the same record and drops the ones that cancel. -/
+def consolidate : Collection α → Collection α
+  | [] => []
+  | (a, d) :: rest => insert a d (consolidate rest)
+
+theorem count_append (c₁ c₂ : Collection α) (x : α) :
+    count (c₁ ++ c₂) x = count c₁ x + count c₂ x := by
+  induction c₁ with
+  | nil => simp [count]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    simp [count, ih, Int.add_assoc]
+
+theorem count_negate (c : Collection α) (x : α) :
+    count (negate c) x = -count c x := by
+  induction c with
+  | nil => simp [negate, count]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    simp only [negate, List.map_cons, count] at ih ⊢
+    rw [ih]
+    split <;> omega
+
+/-- Appending a collection's negation cancels it. -/
+theorem count_append_negate (c : Collection α) (x : α) :
+    count (c ++ negate c) x = 0 := by
+  rw [count_append, count_negate]
+  omega
+
+theorem count_insert (a : α) (d : Int) (c : Collection α) (x : α) :
+    count (insert a d c) x = (if a = x then d else 0) + count c x := by
+  induction c with
+  | nil =>
+    simp only [insert, count]
+    split <;> simp [count, *]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    by_cases hb : b = a
+    · subst hb
+      by_cases hz : d + e = 0
+      · rw [insert, ite_eq_left rfl, ite_eq_left hz, count]
+        by_cases hx : b = x <;> simp [hx] <;> omega
+      · rw [insert, ite_eq_left rfl, ite_eq_right hz, count, count]
+        by_cases hx : b = x <;> simp [hx] <;> omega
+    · rw [insert, ite_eq_right hb, count, count, ih]
+      omega
+
+/-- Consolidation preserves the multiplicity of every record. -/
+theorem count_consolidate (c : Collection α) (x : α) :
+    count (consolidate c) x = count c x := by
+  induction c with
+  | nil => rfl
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    simp only [consolidate, count_insert, ih, count]
+
+/-- Every update has a nonzero diff. -/
+def NoZeros (c : Collection α) : Prop :=
+  ∀ u ∈ c, u.2 ≠ 0
+
+theorem noZeros_insert (a : α) (d : Int) (c : Collection α) (h : NoZeros c) :
+    NoZeros (insert a d c) := by
+  induction c with
+  | nil =>
+    simp only [insert]
+    split
+    · simp [NoZeros]
+    · simp [NoZeros, *]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    have hrest : NoZeros rest := fun v hv => h v (List.mem_cons_of_mem _ hv)
+    have he : e ≠ 0 := h (b, e) List.mem_cons_self
+    simp only [insert]
+    split
+    · split
+      · exact hrest
+      · intro v hv
+        cases List.mem_cons.mp hv with
+        | inl hv => subst hv; assumption
+        | inr hv => exact hrest v hv
+    · intro v hv
+      cases List.mem_cons.mp hv with
+      | inl hv => subst hv; exact he
+      | inr hv => exact ih hrest v hv
+
+/-- Consolidation leaves no update with a zero diff. -/
+theorem noZeros_consolidate (c : Collection α) : NoZeros (consolidate c) := by
+  induction c with
+  | nil => simp [consolidate, NoZeros]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    exact noZeros_insert a d _ ih
+
+example : consolidate ([(1, 2), (2, 1), (1, -2)] : Collection Nat) = [(2, 1)] := by
+  decide
+
+end Collection
+
+end Mz
diff --git a/misc/lean/README.md b/misc/lean/README.md
new file mode 100644
index 0000000000000..2dc4aeae02380
--- /dev/null
+++ b/misc/lean/README.md
@@ -0,0 +1,32 @@
+# Lean models
+
+This directory is a Lake project for Lean 4 models of Materialize.
+Each model lives under `Mz/` and is imported from `Mz.lean`, so `lake build` checks all of them.
+The `lean` CI step runs that build, and `warningAsError` in `lakefile.toml` makes any `sorry` or warning fail it.
+`Mz/Collection.lean` is a sample: it models collections of `(record, diff)` updates and proves that consolidation preserves multiplicities.
+
+## Running
+
+Check all models in Docker, the same way CI does:
+
+```sh
+bin/mzcompose --find lean run default
+```
+
+Arguments replace the default `build` and go to `lake`, for example `bin/mzcompose --find lean run default env lean Mz/Collection.lean`.
+Separate arguments that start with `-` from the workflow's own options with `--`.
+
+For editor support, install [elan](https://github.com/leanprover/elan) and open this directory.
+elan picks the Lean version from `lean-toolchain`.
+
+## Toolchain and dependencies
+
+The `lean` mzbuild image in `misc/images/lean` installs the toolchain named in `lean-toolchain` and builds the dependencies in `lakefile.toml` and `lake-manifest.json` into the image.
+Only those three files are inputs to the image, so editing a model reuses the published image.
+To change the Lean version, edit `lean-toolchain`.
+To add a dependency, add a `[[require]]` to `lakefile.toml`, pin it by `rev`, and commit the `lake-manifest.json` that `lake update` writes.
+
+## Checking a model
+
+A proof only says something about the system if the model can fail.
+Before relying on a model, break it in a way the theorems should catch, for example by removing a guard, and confirm the build fails.
diff --git a/misc/lean/lake-manifest.json b/misc/lean/lake-manifest.json
new file mode 100644
index 0000000000000..255f99002a1e0
--- /dev/null
+++ b/misc/lean/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "mz",
+ "lakeDir": ".lake"}
diff --git a/misc/lean/lakefile.toml b/misc/lean/lakefile.toml
new file mode 100644
index 0000000000000..0637b58e05835
--- /dev/null
+++ b/misc/lean/lakefile.toml
@@ -0,0 +1,17 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+name = "mz"
+defaultTargets = ["Mz"]
+# Makes `sorry` and every other warning fail the build, so an unfinished
+# proof cannot pass CI.
+leanOptions = { warningAsError = true }
+
+[[lean_lib]]
+name = "Mz"
diff --git a/misc/lean/lean-toolchain b/misc/lean/lean-toolchain
new file mode 100644
index 0000000000000..ba8ebf2dbaf6a
--- /dev/null
+++ b/misc/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1
diff --git a/misc/lean/mzcompose b/misc/lean/mzcompose
new file mode 100755
index 0000000000000..1f866645dabc8
--- /dev/null
+++ b/misc/lean/mzcompose
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# mzcompose — runs Docker Compose with Materialize customizations.
+
+exec "$(dirname "$0")"/../../bin/pyactivate -m materialize.cli.mzcompose "$@"
diff --git a/misc/lean/mzcompose.py b/misc/lean/mzcompose.py
new file mode 100644
index 0000000000000..f4cede04fcf3b
--- /dev/null
+++ b/misc/lean/mzcompose.py
@@ -0,0 +1,32 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+
+"""
+Builds and checks the Lean 4 models in this directory.
+"""
+
+from materialize.mzcompose.composition import Composition, WorkflowArgumentParser
+from materialize.mzcompose.service import Service
+
+SERVICES = [
+    Service(
+        name="lean",
+        config={
+            "mzbuild": "lean",
+            "volumes": [".:/src:ro"],
+        },
+    ),
+]
+
+
+def workflow_default(c: Composition, parser: WorkflowArgumentParser) -> None:
+    """Run `lake` with the given arguments, `lake build` by default."""
+    parser.add_argument("lake_args", nargs="*", default=["build"])
+    args = parser.parse_args()
+    c.run("lean", *args.lake_args, rm=True)
diff --git a/misc/python/materialize/mzbuild.py b/misc/python/materialize/mzbuild.py
index b3026b8bc16f5..34f5b5f30a67a 100644
--- a/misc/python/materialize/mzbuild.py
+++ b/misc/python/materialize/mzbuild.py
@@ -602,14 +602,18 @@ def __init__(self, rd: RepositoryDetails, path: Path, config: dict[str, Any]):
 
     def run(self, prep: Any) -> None:
         super().run(prep)
-        for src in self.inputs():
+        for src in self._source_files():
             dst = self.path / self.destination / src
             dst.parent.mkdir(parents=True, exist_ok=True)
             shutil.copy(self.rd.root / self.source / src, dst)
 
-    def inputs(self) -> set[str]:
+    def _source_files(self) -> set[str]:
+        """The files to copy, relative to `source`."""
         return set(git.expand_globs(self.rd.root / self.source, self.matching))
 
+    def inputs(self) -> set[str]:
+        return {str(Path(self.source) / src) for src in self._source_files()}
+
 
 class CargoPreImage(PreImage):
     """A `PreImage` action that uses Cargo."""

From c289f51ce482bdeb364453111a9b1c5a8d9d2de9 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Thu, 1 Oct 2026 18:16:55 +0200
Subject: [PATCH 2/7] misc/lean: check unimported models and bake dependency
 modules

Build every module under Mz/ with globs, so a model that Mz.lean does
not import still fails the build on a sorry. Build each dependency's
default targets in the image, since building the placeholder library
only cloned them.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 misc/images/lean/Dockerfile | 8 +++++++-
 misc/lean/README.md         | 2 +-
 misc/lean/lakefile.toml     | 3 +++
 3 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/misc/images/lean/Dockerfile b/misc/images/lean/Dockerfile
index 641f31442f8a4..164b906434047 100644
--- a/misc/images/lean/Dockerfile
+++ b/misc/images/lean/Dockerfile
@@ -24,6 +24,7 @@ RUN apt-get update \
         ca-certificates \
         curl \
         git \
+        jq \
     && apt-get clean \
     && rm -rf /var/lib/apt/lists/*
 
@@ -51,10 +52,15 @@ WORKDIR /workspace
 
 COPY lakefile.toml lake-manifest.json /workspace/
 
-# Builds the dependency closure against an empty placeholder library.
+# Builds the dependency closure. Building the placeholder library alone only
+# clones the dependencies, because Lake compiles just the modules a target
+# imports, so each package's default targets are built by name. NOTE: a
+# package that declares no default targets builds nothing here and compiles
+# on every run instead.
 RUN mkdir Mz \
     && touch Mz.lean \
     && lake build \
+    && for pkg in $(jq -r '.packages[].name' lake-manifest.json); do lake build "@$pkg"; done \
     && rm -rf Mz Mz.lean .lake/build \
     && chmod -R a+rwX /workspace
 
diff --git a/misc/lean/README.md b/misc/lean/README.md
index 2dc4aeae02380..d45421b167133 100644
--- a/misc/lean/README.md
+++ b/misc/lean/README.md
@@ -1,7 +1,7 @@
 # Lean models
 
 This directory is a Lake project for Lean 4 models of Materialize.
-Each model lives under `Mz/` and is imported from `Mz.lean`, so `lake build` checks all of them.
+Each model lives under `Mz/`, and `lake build` checks every module there, whether or not `Mz.lean` imports it.
 The `lean` CI step runs that build, and `warningAsError` in `lakefile.toml` makes any `sorry` or warning fail it.
 `Mz/Collection.lean` is a sample: it models collections of `(record, diff)` updates and proves that consolidation preserves multiplicities.
 
diff --git a/misc/lean/lakefile.toml b/misc/lean/lakefile.toml
index 0637b58e05835..ece1262e8ac67 100644
--- a/misc/lean/lakefile.toml
+++ b/misc/lean/lakefile.toml
@@ -15,3 +15,6 @@ leanOptions = { warningAsError = true }
 
 [[lean_lib]]
 name = "Mz"
+# Builds every module under `Mz/`, not only those `Mz.lean` imports, so an
+# unimported model cannot skip the check.
+globs = ["Mz.*"]

From a76a4101b32522f54e22c9646954c027fcef0863 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Thu, 1 Oct 2026 19:59:20 +0200
Subject: [PATCH 3/7] misc/images/lean: fail the image build if any dependency
 fails

Build all dependency packages in one lake invocation. A for loop only
reported the last package's status, so an earlier failure produced a
published image without that package's modules.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 misc/images/lean/Dockerfile | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/misc/images/lean/Dockerfile b/misc/images/lean/Dockerfile
index 164b906434047..7d68e92093713 100644
--- a/misc/images/lean/Dockerfile
+++ b/misc/images/lean/Dockerfile
@@ -56,11 +56,12 @@ COPY lakefile.toml lake-manifest.json /workspace/
 # clones the dependencies, because Lake compiles just the modules a target
 # imports, so each package's default targets are built by name. NOTE: a
 # package that declares no default targets builds nothing here and compiles
-# on every run instead.
+# on every run instead. One `lake build` for all packages fails if any of them
+# fails. With no dependencies it builds the placeholder.
 RUN mkdir Mz \
     && touch Mz.lean \
-    && lake build \
-    && for pkg in $(jq -r '.packages[].name' lake-manifest.json); do lake build "@$pkg"; done \
+    && targets="$(jq -r '.packages[] | "@" + .name' lake-manifest.json)" \
+    && lake build $targets \
     && rm -rf Mz Mz.lean .lake/build \
     && chmod -R a+rwX /workspace
 

From 859610021b72634caaee6164aea589d77b79dad2 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Thu, 1 Oct 2026 22:16:31 +0200
Subject: [PATCH 4/7] misc/images/lean: drop toolchain parts proof checking
 does not need

Delete the static libraries, LLVM, .ilean files and sources from the
toolchain, which shrinks it from 3.0 GB to 2.3 GB. Install the toolchain
explicitly first, since elan otherwise downloads it lazily on first use.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 misc/images/lean/Dockerfile | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/misc/images/lean/Dockerfile b/misc/images/lean/Dockerfile
index 7d68e92093713..2571aba5c341c 100644
--- a/misc/images/lean/Dockerfile
+++ b/misc/images/lean/Dockerfile
@@ -30,6 +30,11 @@ RUN apt-get update \
 
 COPY lean-toolchain /workspace/
 
+# Checking proofs needs the `.olean*`, `.ir` and shared libraries. The static
+# libraries, LLVM, `.ilean` files and sources are deleted, which saves 0.7 GB.
+# NOTE: without them nothing can link an executable, so `lean_exe`, `lake exe`
+# (including Mathlib's `lake exe cache get`) and `precompileModules` fail.
+# Keep them if a dependency needs any of these.
 RUN case "$(uname -m)" in \
         x86_64) triple=x86_64-unknown-linux-gnu; sha256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 ;; \
         aarch64) triple=aarch64-unknown-linux-gnu; sha256=05febd124d84ebf994b2e7479922a5650b1e950c17ae3bd1ddd776b65bb72bf9 ;; \
@@ -41,6 +46,10 @@ RUN case "$(uname -m)" in \
     && tar -C /tmp -xzf /tmp/elan.tar.gz \
     && /tmp/elan-init -y --no-modify-path --default-toolchain "$(cat /workspace/lean-toolchain)" \
     && rm /tmp/elan.tar.gz /tmp/elan-init \
+    && elan toolchain install "$(cat /workspace/lean-toolchain)" \
+    && toolchain="$(echo "$ELAN_HOME"/toolchains/*)" \
+    && find "$toolchain" \( -name '*.a' -o -name '*.ilean' \) -delete \
+    && rm -rf "$toolchain/src" "$toolchain"/lib/libLLVM.so.* "$toolchain"/lib/libclang-cpp.so.* \
     && chmod -R a+rX "$ELAN_HOME" \
     && lean --version
 

From 7981677c3dffe77a5818465c5cdd184126101f87 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Thu, 1 Oct 2026 22:52:49 +0200
Subject: [PATCH 5/7] ci: exempt the Lean models step from the empty
 services.log check

The lean composition runs one short-lived container and no long-running
service, so docker compose logs has nothing to collect and the check
failed a passing build.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 ci/plugins/mzcompose/hooks/command | 1 +
 1 file changed, 1 insertion(+)

diff --git a/ci/plugins/mzcompose/hooks/command b/ci/plugins/mzcompose/hooks/command
index 9fd0938b3c561..b0e74df8d7a7e 100644
--- a/ci/plugins/mzcompose/hooks/command
+++ b/ci/plugins/mzcompose/hooks/command
@@ -444,6 +444,7 @@ cleanup() {
     && [ "$BUILDKITE_LABEL" != "Parallel Benchmark against QA Canary Environment" ] \
     && [ "$BUILDKITE_LABEL" != "Parallel Benchmark against QA Benchmarking Staging Environment" ] \
     && [ "$BUILDKITE_LABEL" != ":rust: Miri test (full)" ] \
+    && [ "$BUILDKITE_LABEL" != "Lean models" ] \
     && [[ ! "$BUILDKITE_LABEL" =~ Terraform\ .* ]] \
     && [[ ! "$BUILDKITE_LABEL" =~ Orchestratord\ .* ]] \
     && [[ ! "$BUILDKITE_LABEL" =~ Cluster\ spec\ sheet.* ]] \

From 99fd85f0d41fdb233f7bc36951c863ff66bd0544 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Thu, 1 Oct 2026 23:11:59 +0200
Subject: [PATCH 6/7] misc/images/lean: keep the whole Lean toolchain

Batteries, which Aesop and Mathlib require, lists the runLinter
executable in its default targets. Linking it needs the static libraries
and LLVM, so stripping them breaks the dependency build as soon as any
common library is added.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 misc/images/lean/Dockerfile | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/misc/images/lean/Dockerfile b/misc/images/lean/Dockerfile
index 2571aba5c341c..c5f6ae9a568a9 100644
--- a/misc/images/lean/Dockerfile
+++ b/misc/images/lean/Dockerfile
@@ -30,11 +30,10 @@ RUN apt-get update \
 
 COPY lean-toolchain /workspace/
 
-# Checking proofs needs the `.olean*`, `.ir` and shared libraries. The static
-# libraries, LLVM, `.ilean` files and sources are deleted, which saves 0.7 GB.
-# NOTE: without them nothing can link an executable, so `lean_exe`, `lake exe`
-# (including Mathlib's `lake exe cache get`) and `precompileModules` fail.
-# Keep them if a dependency needs any of these.
+# NOTE: the toolchain is kept whole although checking proofs needs only part of
+# it. The static libraries and LLVM link executables, and Batteries, which
+# Aesop and Mathlib require, lists the `runLinter` executable in its default
+# targets, so the dependency build below fails without them.
 RUN case "$(uname -m)" in \
         x86_64) triple=x86_64-unknown-linux-gnu; sha256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 ;; \
         aarch64) triple=aarch64-unknown-linux-gnu; sha256=05febd124d84ebf994b2e7479922a5650b1e950c17ae3bd1ddd776b65bb72bf9 ;; \
@@ -46,10 +45,6 @@ RUN case "$(uname -m)" in \
     && tar -C /tmp -xzf /tmp/elan.tar.gz \
     && /tmp/elan-init -y --no-modify-path --default-toolchain "$(cat /workspace/lean-toolchain)" \
     && rm /tmp/elan.tar.gz /tmp/elan-init \
-    && elan toolchain install "$(cat /workspace/lean-toolchain)" \
-    && toolchain="$(echo "$ELAN_HOME"/toolchains/*)" \
-    && find "$toolchain" \( -name '*.a' -o -name '*.ilean' \) -delete \
-    && rm -rf "$toolchain/src" "$toolchain"/lib/libLLVM.so.* "$toolchain"/lib/libclang-cpp.so.* \
     && chmod -R a+rX "$ELAN_HOME" \
     && lean --version
 

From 853ed4c444e8ceec3788cc4b24b1ed380249a2f9 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 2 Oct 2026 22:35:33 +0200
Subject: [PATCH 7/7] misc/lean: support non-root runs and prove consolidation
 merges records

mz-lake copied the project with a tar of `.`, which makes a non-root
user change the mode and mtime of the root-owned /workspace and abort.
Copy the entries individually instead. Install the toolchain before the
chmod so every file it downloads is readable by any uid.

Add nodup_consolidate: the existing theorems also hold for a filter that
merges nothing. Fix comments and README claims about image inputs,
lake env, and the git safe.directory rule.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 misc/images/lean/Dockerfile  | 11 +++----
 misc/images/lean/mz-lake     |  7 +++--
 misc/lean/Mz/Collection.lean | 56 +++++++++++++++++++++++++++++++++++-
 misc/lean/README.md          |  3 +-
 4 files changed, 68 insertions(+), 9 deletions(-)

diff --git a/misc/images/lean/Dockerfile b/misc/images/lean/Dockerfile
index c5f6ae9a568a9..1af5e087847e5 100644
--- a/misc/images/lean/Dockerfile
+++ b/misc/images/lean/Dockerfile
@@ -31,9 +31,9 @@ RUN apt-get update \
 COPY lean-toolchain /workspace/
 
 # NOTE: the toolchain is kept whole although checking proofs needs only part of
-# it. The static libraries and LLVM link executables, and Batteries, which
-# Aesop and Mathlib require, lists the `runLinter` executable in its default
-# targets, so the dependency build below fails without them.
+# it. Batteries, a dependency of Aesop and Mathlib, has the `runLinter`
+# executable among its default targets. Linking it needs the toolchain's static
+# libraries and LLVM, so removing them breaks the dependency build below.
 RUN case "$(uname -m)" in \
         x86_64) triple=x86_64-unknown-linux-gnu; sha256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 ;; \
         aarch64) triple=aarch64-unknown-linux-gnu; sha256=05febd124d84ebf994b2e7479922a5650b1e950c17ae3bd1ddd776b65bb72bf9 ;; \
@@ -45,11 +45,12 @@ RUN case "$(uname -m)" in \
     && tar -C /tmp -xzf /tmp/elan.tar.gz \
     && /tmp/elan-init -y --no-modify-path --default-toolchain "$(cat /workspace/lean-toolchain)" \
     && rm /tmp/elan.tar.gz /tmp/elan-init \
+    && elan toolchain install "$(cat /workspace/lean-toolchain)" \
     && chmod -R a+rX "$ELAN_HOME" \
     && lean --version
 
-# Lake refuses dependency checkouts owned by a different uid than the one
-# running it, and re-clones them instead.
+# Git refuses repositories owned by a different uid than the one running it,
+# and Lake then re-clones the baked dependencies.
 RUN git config --system --add safe.directory '*'
 
 WORKDIR /workspace
diff --git a/misc/images/lean/mz-lake b/misc/images/lean/mz-lake
index 392c9fafcc2be..c58d87f97da96 100755
--- a/misc/images/lean/mz-lake
+++ b/misc/images/lean/mz-lake
@@ -16,8 +16,11 @@ set -euo pipefail
 
 # Mounting the project over /workspace would hide /workspace/.lake, which
 # holds the dependency closure built into the image. The host's own .lake is
-# skipped for the same reason.
-tar -C /src --exclude=./.lake -cf - . | tar -C /workspace -xf -
+# skipped for the same reason. The entries are copied one by one because
+# copying `.` itself makes a non-root user try to change the mode and mtime
+# of the root-owned /workspace, which fails.
+cd /src
+find . -mindepth 1 -maxdepth 1 ! -name .lake -exec cp -R -t /workspace {} +
 
 cd /workspace
 exec lake "$@"
diff --git a/misc/lean/Mz/Collection.lean b/misc/lean/Mz/Collection.lean
index c8caab8944cee..4511f4cd8b96e 100644
--- a/misc/lean/Mz/Collection.lean
+++ b/misc/lean/Mz/Collection.lean
@@ -16,7 +16,8 @@ are equivalent when they agree on every multiplicity, regardless of how the
 updates are ordered or split.
 
 `consolidate` merges updates to the same record and drops the ones that cancel.
-It is correct when it preserves every multiplicity and leaves no zero diff.
+It is correct when it preserves every multiplicity, leaves no zero diff, and
+leaves at most one update per record.
 -/
 
 namespace Mz
@@ -138,6 +139,59 @@ theorem noZeros_consolidate (c : Collection α) : NoZeros (consolidate c) := by
     obtain ⟨a, d⟩ := u
     exact noZeros_insert a d _ ih
 
+/-- The records that have an update. -/
+def keys (c : Collection α) : List α :=
+  c.map Prod.fst
+
+theorem mem_keys_insert {a x : α} {d : Int} {c : Collection α}
+    (h : x ∈ keys (insert a d c)) : x = a ∨ x ∈ keys c := by
+  induction c with
+  | nil =>
+    simp only [insert] at h
+    split at h <;> simp_all [keys]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    simp only [insert] at h
+    split at h
+    · split at h <;> simp_all [keys]
+    · simp only [keys, List.map_cons, List.mem_cons] at h ⊢
+      rcases h with h | h
+      · exact Or.inr (Or.inl h)
+      · rcases ih h with h | h
+        · exact Or.inl h
+        · exact Or.inr (Or.inr h)
+
+theorem nodup_insert (a : α) (d : Int) (c : Collection α) (h : (keys c).Nodup) :
+    (keys (insert a d c)).Nodup := by
+  induction c with
+  | nil =>
+    simp only [insert]
+    split <;> simp [keys]
+  | cons u rest ih =>
+    obtain ⟨b, e⟩ := u
+    simp only [keys, List.map_cons, List.nodup_cons] at h
+    obtain ⟨hb, hrest⟩ := h
+    simp only [insert]
+    split
+    · subst_vars
+      split
+      · exact hrest
+      · simp only [keys, List.map_cons, List.nodup_cons]
+        exact ⟨hb, hrest⟩
+    · simp only [keys, List.map_cons, List.nodup_cons]
+      refine ⟨fun hmem => ?_, ih hrest⟩
+      rcases mem_keys_insert hmem with h | h
+      · contradiction
+      · exact hb h
+
+/-- Consolidation leaves at most one update per record. -/
+theorem nodup_consolidate (c : Collection α) : (keys (consolidate c)).Nodup := by
+  induction c with
+  | nil => simp [consolidate, keys]
+  | cons u rest ih =>
+    obtain ⟨a, d⟩ := u
+    exact nodup_insert a d _ ih
+
 example : consolidate ([(1, 2), (2, 1), (1, -2)] : Collection Nat) = [(2, 1)] := by
   decide
 
diff --git a/misc/lean/README.md b/misc/lean/README.md
index d45421b167133..7e7206d40f741 100644
--- a/misc/lean/README.md
+++ b/misc/lean/README.md
@@ -14,6 +14,7 @@ bin/mzcompose --find lean run default
 ```
 
 Arguments replace the default `build` and go to `lake`, for example `bin/mzcompose --find lean run default env lean Mz/Collection.lean`.
+Only `lake build` applies the options in `lakefile.toml`, so `lake env lean` reports a `sorry` as a warning and succeeds.
 Separate arguments that start with `-` from the workflow's own options with `--`.
 
 For editor support, install [elan](https://github.com/leanprover/elan) and open this directory.
@@ -22,7 +23,7 @@ elan picks the Lean version from `lean-toolchain`.
 ## Toolchain and dependencies
 
 The `lean` mzbuild image in `misc/images/lean` installs the toolchain named in `lean-toolchain` and builds the dependencies in `lakefile.toml` and `lake-manifest.json` into the image.
-Only those three files are inputs to the image, so editing a model reuses the published image.
+Those three are the only files from this directory that are inputs to the image, so editing a model reuses the published image.
 To change the Lean version, edit `lean-toolchain`.
 To add a dependency, add a `[[require]]` to `lakefile.toml`, pin it by `rev`, and commit the `lake-manifest.json` that `lake update` writes.