misc/lean: add a Lean 4 project, toolchain image, and CI step

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.* ]] \

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$' \

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

misc/images/lean/.gitignore

@@ -0,0 +1,3 @@
+/lean-toolchain
+/lakefile.toml
+/lake-manifest.json

misc/images/lean/Dockerfile

@@ -0,0 +1,75 @@
+# 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 \
+        jq \
+    && apt-get clean \
+    && rm -rf /var/lib/apt/lists/*
+
+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.
+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. 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. 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 \
+    && targets="$(jq -r '.packages[] | "@" + .name' lake-manifest.json)" \
+    && lake build $targets \
+    && rm -rf Mz Mz.lean .lake/build \
+    && chmod -R a+rwX /workspace
+
+COPY mz-lake /usr/local/bin/
+
+ENTRYPOINT ["mz-lake"]
+CMD ["build"]

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 "$@"

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

misc/lean/.gitignore

@@ -0,0 +1 @@
+/.lake

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

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

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 `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.
+
+## 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.

misc/lean/lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "mz",
+ "lakeDir": ".lake"}

misc/lean/lakefile.toml

@@ -0,0 +1,20 @@
+# 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"
+# Builds every module under `Mz/`, not only those `Mz.lean` imports, so an
+# unimported model cannot skip the check.
+globs = ["Mz.*"]

misc/lean/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.34.1