From 2a638fdbe20acfaaa9adc7d51e225808a28b6e4b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E2=88=9A2?= <240895760+sqrt-of-2@users.noreply.github.com>
Date: Mon, 29 Jun 2026 12:19:20 +0000
Subject: [PATCH] feat: add comparator CI to verify theorem `ff`

---
 .github/workflows/comparator.yml | 186 +++++++++++++++++++++++++++++++
 comparator/Challenge.lean        |  22 ++++
 comparator/Solution.lean         |  16 +++
 comparator/config.json           |  10 ++
 comparator/lake-manifest.json    | 123 ++++++++++++++++++++
 comparator/lakefile.toml         |  18 +++
 comparator/lean-toolchain        |   1 +
 comparator/versions.env          |  14 +++
 verify.sh                        | 144 ++++++++++++++++++++++++
 verify_docker.sh                 |  28 +++++
 10 files changed, 562 insertions(+)
 create mode 100644 .github/workflows/comparator.yml
 create mode 100644 comparator/Challenge.lean
 create mode 100644 comparator/Solution.lean
 create mode 100644 comparator/config.json
 create mode 100644 comparator/lake-manifest.json
 create mode 100644 comparator/lakefile.toml
 create mode 100644 comparator/lean-toolchain
 create mode 100644 comparator/versions.env
 create mode 100755 verify.sh
 create mode 100755 verify_docker.sh

diff --git a/.github/workflows/comparator.yml b/.github/workflows/comparator.yml
new file mode 100644
index 0000000000..bef9d6f8fc
--- /dev/null
+++ b/.github/workflows/comparator.yml
@@ -0,0 +1,186 @@
+name: Comparator CI (a trustworthy judge for Lean proofs)
+
+permissions:
+  contents: read
+
+on:
+  push:
+    branches: [master]
+  pull_request:
+    paths:
+      - 'comparator/**'
+      - 'APAP/**'
+      - 'APAP.lean'
+      - 'lean-toolchain'
+      - 'verify.sh'
+      - '.github/workflows/comparator.yml'
+  workflow_dispatch:
+
+jobs:
+  comparator:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 90
+
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+
+      - name: Install system dependencies (for act / minimal environments)
+        run: |
+          if ! command -v curl &>/dev/null || ! command -v git &>/dev/null || ! command -v zstd &>/dev/null; then
+            echo "Installing dependencies..."
+            SUDO=""
+            if command -v sudo &>/dev/null; then SUDO="sudo"; fi
+            # Ensure apt is not interactive
+            export DEBIAN_FRONTEND=noninteractive
+            $SUDO apt-get update -y && $SUDO apt-get install -y curl git zstd ca-certificates build-essential
+          fi
+
+      - name: Load version pins from comparator/versions.env
+        run: |
+          grep -v '^#' comparator/versions.env | grep -v '^$' \
+            | while IFS='=' read -r k v; do echo "$k=$v" >> "$GITHUB_ENV"; done
+
+      - name: Free up disk space
+        run: |
+          df -h /
+          SUDO=""
+          if command -v sudo &>/dev/null; then SUDO="sudo"; fi
+          $SUDO rm -rf /usr/local/lib/android /usr/share/dotnet /opt/ghc \
+            /usr/local/.ghcup /opt/hostedtoolcache/CodeQL || true
+          $SUDO apt-get clean || true
+          df -h /
+
+      - name: Install elan and pre-install Lean toolchain
+        run: |
+          curl -fsSL -o /tmp/elan.tar.gz \
+            "https://github.com/leanprover/elan/releases/download/${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz"
+          echo "${ELAN_SHA256}  /tmp/elan.tar.gz" | sha256sum -c
+          tar -xzf /tmp/elan.tar.gz -C /tmp
+          /tmp/elan-init -y --no-modify-path
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+          echo "$HOME/.local/bin" >> $GITHUB_PATH
+          # Install toolchain explicitly so elan doesn't fetch it unverified at build time.
+          TOOLCHAIN_DIR="$HOME/.elan/toolchains/leanprover--lean4---${LEAN_VERSION}"
+          curl -fsSL -o /tmp/lean.tar.zst \
+            "https://releases.lean-lang.org/lean4/${LEAN_VERSION}/lean-${LEAN_VERSION#v}-linux.tar.zst"
+          echo "${LEAN_SHA256}  /tmp/lean.tar.zst" | sha256sum -c
+          mkdir -p "$TOOLCHAIN_DIR"
+          tar --zstd -xf /tmp/lean.tar.zst -C "$TOOLCHAIN_DIR" --strip-components=1
+
+      - name: Cache .lake
+        if: ${{ !env.ACT }}
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        with:
+          path: .lake
+          key: lake-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}-${{ github.run_id }}
+          restore-keys: |
+            lake-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}-
+            lake-
+
+      - name: Build library (warms oleans for comparator)
+        run: |
+          lake exe cache get
+          lake build
+
+      - name: Install landrun
+        run: |
+          mkdir -p "$HOME/.local/bin"
+          curl -fsSL -o "$HOME/.local/bin/landrun" \
+            "https://github.com/Zouuup/landrun/releases/download/${LANDRUN_VERSION}/landrun-linux-amd64"
+          echo "${LANDRUN_SHA256}  $HOME/.local/bin/landrun" | sha256sum -c
+          chmod +x "$HOME/.local/bin/landrun"
+          landrun --version
+
+      - name: Cache lean4export build
+        if: ${{ !env.ACT }}
+        id: cache-lean4export
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        with:
+          path: ~/lean4export
+          key: lean4export-${{ env.LEAN4EXPORT_REF }}-${{ hashFiles('lean-toolchain') }}
+
+      - name: Build lean4export
+        if: steps.cache-lean4export.outputs.cache-hit != 'true'
+        run: |
+          git clone -q --no-checkout https://github.com/leanprover/lean4export ~/lean4export
+          git -C ~/lean4export fetch -q --depth 1 origin "$LEAN4EXPORT_REF"
+          git -C ~/lean4export checkout -q FETCH_HEAD
+          cp lean-toolchain ~/lean4export/lean-toolchain
+          (cd ~/lean4export && lake build)
+
+      - name: Cache comparator build
+        if: ${{ !env.ACT }}
+        id: cache-comparator
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        with:
+          path: ~/comparator
+          key: comparator-${{ env.COMPARATOR_REF }}
+
+      - name: Build comparator
+        if: steps.cache-comparator.outputs.cache-hit != 'true'
+        run: |
+          git clone -q --no-checkout https://github.com/leanprover/comparator ~/comparator
+          git -C ~/comparator fetch -q --depth 1 origin "$COMPARATOR_REF"
+          git -C ~/comparator checkout -q FETCH_HEAD
+          (cd ~/comparator && lake build)
+
+      - name: Cache nanoda build
+        if: ${{ !env.ACT }}
+        id: cache-nanoda
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        with:
+          path: ~/nanoda_lib/target/release/nanoda_bin
+          key: nanoda-${{ env.NANODA_REF }}
+
+      - name: Build nanoda (independent Rust kernel)
+        if: steps.cache-nanoda.outputs.cache-hit != 'true'
+        run: |
+          curl -fsSL -o /tmp/rust.tar.gz \
+            "https://static.rust-lang.org/dist/rust-${RUST_VERSION}-x86_64-unknown-linux-gnu.tar.gz"
+          echo "${RUST_SHA256}  /tmp/rust.tar.gz" | sha256sum -c
+          tar -xzf /tmp/rust.tar.gz -C /tmp
+          /tmp/rust-${RUST_VERSION}-x86_64-unknown-linux-gnu/install.sh --prefix="$HOME/.local" --without=rust-docs
+          git clone -q --no-checkout https://github.com/ammkrn/nanoda_lib ~/nanoda_lib
+          git -C ~/nanoda_lib fetch -q --depth 1 origin "$NANODA_REF"
+          git -C ~/nanoda_lib checkout -q FETCH_HEAD
+          (cd ~/nanoda_lib && "$HOME/.local/bin/cargo" build --release)
+
+      - name: Create landrun wrapper
+        run: |
+          mkdir -p "$HOME/.local/bin"
+          printf '%s\n' \
+            '#!/usr/bin/env bash' \
+            'args=()' \
+            'while [[ $# -gt 0 ]]; do' \
+            '  if [[ "$1" == "--ro" && "$2" == "/" ]]; then' \
+            '    args+=("--rox" "/")' \
+            '    shift 2' \
+            '  else' \
+            '    args+=("$1")' \
+            '    shift' \
+            '  fi' \
+            'done' \
+            'exec LANDRUN_PLACEHOLDER "${args[@]}"' \
+            > "$HOME/.local/bin/landrun-wrapper"
+          sed -i "s|LANDRUN_PLACEHOLDER|$HOME/.local/bin/landrun|g" "$HOME/.local/bin/landrun-wrapper"
+          chmod +x "$HOME/.local/bin/landrun-wrapper"
+
+      - name: Link tools onto PATH
+        run: |
+          ln -sf ~/lean4export/.lake/build/bin/lean4export "$HOME/.local/bin/lean4export"
+          ln -sf ~/comparator/.lake/build/bin/comparator "$HOME/.local/bin/comparator"
+          ln -sf ~/nanoda_lib/target/release/nanoda_bin "$HOME/.local/bin/nanoda_bin"
+          command -v landrun lean4export comparator nanoda_bin
+
+      - name: Build comparator workspace (Challenge + Solution)
+        run: |
+          cd comparator
+          lake exe cache get
+          lake build Challenge Solution
+
+      - name: Run comparator (1 theorem, kernel + axiom-closure re-check)
+        run: |
+          cd comparator
+          COMPARATOR_LANDRUN="$HOME/.local/bin/landrun-wrapper" \
+            COMPARATOR_NANODA="$HOME/nanoda_lib/target/release/nanoda_bin" \
+            lake env comparator config.json
diff --git a/comparator/Challenge.lean b/comparator/Challenge.lean
new file mode 100644
index 0000000000..64c460dd7c
--- /dev/null
+++ b/comparator/Challenge.lean
@@ -0,0 +1,22 @@
+import Mathlib.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.Combinatorics.Additive.AP.Three.Defs
+import Mathlib.Data.Finset.Density
+import Mathlib.LinearAlgebra.Dimension.Finrank
+
+/-!
+# Challenge: human-auditable theorem statements
+
+Imports only Mathlib. To audit: read this file and check that each statement
+says what it claims. A passing comparator run then guarantees the APAP
+library proves these statements using only `{propext, Quot.sound, Classical.choice}`.
+-/
+
+noncomputable section
+
+namespace Comparator
+
+theorem ff {G : Type u} [AddCommGroup G] [Fintype G] {A : Finset G} {q : ℕ} [Module (ZMod q) G]
+    (hq₃ : 3 ≤ q) (hq : Nat.Prime q) (hA₀ : A.Nonempty) (hA : ThreeAPFree (↑A : Set G)) :
+    ↑(Module.finrank (ZMod q) G) ≤ (2 ^ 148 * (1 + Real.log (↑A.dens)⁻¹) ^ 9 : ℝ) := sorry
+
+end Comparator
diff --git a/comparator/Solution.lean b/comparator/Solution.lean
new file mode 100644
index 0000000000..66849a7062
--- /dev/null
+++ b/comparator/Solution.lean
@@ -0,0 +1,16 @@
+import APAP.FiniteField
+
+/-!
+# Solution: bridge from Challenge to the APAP library
+-/
+
+noncomputable section
+
+namespace Comparator
+
+theorem ff {G : Type u} [AddCommGroup G] [Fintype G] {A : Finset G} {q : ℕ} [Module (ZMod q) G]
+    (hq₃ : 3 ≤ q) (hq : Nat.Prime q) (hA₀ : A.Nonempty) (hA : ThreeAPFree (↑A : Set G)) :
+    ↑(Module.finrank (ZMod q) G) ≤ (2 ^ 148 * (1 + Real.log (↑A.dens)⁻¹) ^ 9 : ℝ) :=
+  _root_.ff hq₃ hq hA₀ hA
+
+end Comparator
diff --git a/comparator/config.json b/comparator/config.json
new file mode 100644
index 0000000000..b7a1f21424
--- /dev/null
+++ b/comparator/config.json
@@ -0,0 +1,10 @@
+{
+  "challenge_module": "Challenge",
+  "solution_module": "Solution",
+  "theorem_names": [
+    "Comparator.ff"
+  ],
+  "definition_names": [],
+  "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"],
+  "enable_nanoda": true
+}
diff --git a/comparator/lake-manifest.json b/comparator/lake-manifest.json
new file mode 100644
index 0000000000..11575a80dd
--- /dev/null
+++ b/comparator/lake-manifest.json
@@ -0,0 +1,123 @@
+{"version": "1.2.0",
+ "packagesDir": "../.lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "APAP",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "..",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/add-combi.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "068c06bc90b223b40ef2ed08d7f4de935c3eee13",
+   "name": "AddCombi",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fa08db58b30eb033edcdab331bba000827f9f785",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "APAPComparator",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/comparator/lakefile.toml b/comparator/lakefile.toml
new file mode 100644
index 0000000000..e2aa7b6b57
--- /dev/null
+++ b/comparator/lakefile.toml
@@ -0,0 +1,18 @@
+name = "APAPComparator"
+
+defaultTargets = ["Challenge", "Solution"]
+
+packagesDir = "../.lake/packages"
+
+[leanOptions]
+relaxedAutoImplicit = false
+
+[[require]]
+name = "APAP"
+path = ".."
+
+[[lean_lib]]
+name = "Challenge"
+
+[[lean_lib]]
+name = "Solution"
diff --git a/comparator/lean-toolchain b/comparator/lean-toolchain
new file mode 100644
index 0000000000..18640c8b06
--- /dev/null
+++ b/comparator/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.31.0
diff --git a/comparator/versions.env b/comparator/versions.env
new file mode 100644
index 0000000000..91114e7863
--- /dev/null
+++ b/comparator/versions.env
@@ -0,0 +1,14 @@
+# Single source of truth for all tool versions; sourced by verify.sh and loaded by comparator.yml.
+
+UBUNTU_IMAGE=ubuntu@sha256:786a8b558f7be160c6c8c4a54f9a57274f3b4fb1491cf65146521ae77ff1dc54
+COMPARATOR_REF=1b82ba006811f7e25d53858252372e4d85fd3921
+LEAN4EXPORT_REF=3de59f10bc4b4a0f2de698597aeb1246caa0df0a
+LANDRUN_VERSION=v0.1.14
+LANDRUN_SHA256=645178e3239cd33760560834e50efea0864183a2a8a82faf199760dffee6dd71
+NANODA_REF=f58f2f6d535e189a40fcb02ede8eb95f97a92d37
+ELAN_VERSION=v4.2.3
+ELAN_SHA256=df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2
+LEAN_VERSION=v4.31.0
+LEAN_SHA256=07a633cc8d9151cbc08825ea4cdda50d4b02a2c9cb852c0131b13046f49cad7f
+RUST_VERSION=1.96.0
+RUST_SHA256=c1130e4f7976f230766ab062b105b1fb050d6a78177db2246a5878fd6a589680
diff --git a/verify.sh b/verify.sh
new file mode 100755
index 0000000000..8ac2a73f49
--- /dev/null
+++ b/verify.sh
@@ -0,0 +1,144 @@
+#!/usr/bin/env bash
+
+# Kernel re-check and axiom audit via `leanprover/comparator`.
+# Requires x86_64 Linux; on other platforms use `verify_docker.sh`.
+
+set -euo pipefail
+
+if [[ "$(uname -s)" != "Linux" || "$(uname -m)" != "x86_64" ]]; then
+  echo "error: verify.sh requires x86_64 Linux (all tool downloads are amd64-only)" >&2
+  echo "       On other platforms, use verify_docker.sh instead." >&2
+  exit 1
+fi
+
+HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+WS="$HERE/comparator"
+WORK="${COMPARATOR_WORK:-$HOME/.cache/comparator-verify}"
+
+source "$WS/versions.env"
+
+mkdir -p "$WORK" "$HOME/.local/bin"
+
+verify_sha256() {
+  local file="$1" expected="$2"
+  echo "${expected}  ${file}" | sha256sum -c --status || {
+    echo "error: SHA256 mismatch for $file" >&2
+    exit 1
+  }
+  echo "$file: OK"
+}
+
+if ! command -v elan &>/dev/null; then
+  echo "Installing elan ${ELAN_VERSION}..."
+  curl -fsSL -o /tmp/elan.tar.gz \
+    "https://github.com/leanprover/elan/releases/download/${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz"
+  verify_sha256 /tmp/elan.tar.gz "$ELAN_SHA256"
+  tar -xzf /tmp/elan.tar.gz -C /tmp
+  /tmp/elan-init -y --no-modify-path
+  export PATH="$HOME/.elan/bin:$PATH"
+fi
+
+TOOLCHAIN_DIR="$HOME/.elan/toolchains/leanprover--lean4---${LEAN_VERSION}"
+if [ ! -d "$TOOLCHAIN_DIR" ]; then
+  echo "Installing Lean toolchain ${LEAN_VERSION}..."
+  curl -fsSL -o /tmp/lean.tar.zst \
+    "https://releases.lean-lang.org/lean4/${LEAN_VERSION}/lean-${LEAN_VERSION#v}-linux.tar.zst"
+  verify_sha256 /tmp/lean.tar.zst "$LEAN_SHA256"
+  mkdir -p "$TOOLCHAIN_DIR"
+  tar --zstd -xf /tmp/lean.tar.zst -C "$TOOLCHAIN_DIR" --strip-components=1
+fi
+
+if [ ! -d "$WORK/comparator" ]; then
+  git clone -q --no-checkout https://github.com/leanprover/comparator "$WORK/comparator"
+fi
+git -C "$WORK/comparator" fetch -q --depth 1 origin "$COMPARATOR_REF"
+COMPARATOR_FETCH_SHA="$(git -C "$WORK/comparator" rev-parse FETCH_HEAD)"
+if [ ! -x "$WORK/comparator/.lake/build/bin/comparator" ] || [ "$COMPARATOR_FETCH_SHA" != "$COMPARATOR_REF" ]; then
+  git -C "$WORK/comparator" checkout -q FETCH_HEAD
+  (cd "$WORK/comparator" && lake build)
+else
+  git -C "$WORK/comparator" checkout -q FETCH_HEAD
+fi
+
+if [ ! -d "$WORK/lean4export" ]; then
+  git clone -q --no-checkout https://github.com/leanprover/lean4export "$WORK/lean4export"
+fi
+git -C "$WORK/lean4export" fetch -q --depth 1 origin "$LEAN4EXPORT_REF"
+LEAN4EXPORT_FETCH_SHA="$(git -C "$WORK/lean4export" rev-parse FETCH_HEAD)"
+
+REBUILD_LEAN4EXPORT=false
+if [ ! -x "$WORK/lean4export/.lake/build/bin/lean4export" ] || [ "$LEAN4EXPORT_FETCH_SHA" != "$LEAN4EXPORT_REF" ]; then
+  REBUILD_LEAN4EXPORT=true
+elif ! cmp -s "$HERE/lean-toolchain" "$WORK/lean4export/lean-toolchain"; then
+  REBUILD_LEAN4EXPORT=true
+fi
+
+git -C "$WORK/lean4export" checkout -q FETCH_HEAD
+cp "$HERE/lean-toolchain" "$WORK/lean4export/lean-toolchain"
+
+if [ "$REBUILD_LEAN4EXPORT" = true ]; then
+  echo "Building lean4export with new toolchain..."
+  (cd "$WORK/lean4export" && lake clean && lake build)
+fi
+
+LANDRUN_BIN="$HOME/.local/bin/landrun"
+if [ ! -x "$LANDRUN_BIN" ] || ! echo "${LANDRUN_SHA256}  ${LANDRUN_BIN}" | sha256sum -c --status 2>/dev/null; then
+  echo "Downloading landrun ${LANDRUN_VERSION}..."
+  curl -fsSL -o "$LANDRUN_BIN" \
+    "https://github.com/Zouuup/landrun/releases/download/${LANDRUN_VERSION}/landrun-linux-amd64"
+  verify_sha256 "$LANDRUN_BIN" "$LANDRUN_SHA256"
+  chmod +x "$LANDRUN_BIN"
+fi
+
+LANDRUN_WRAPPER="$HOME/.local/bin/landrun-wrapper"
+cat > "$LANDRUN_WRAPPER" << 'EOF'
+#!/usr/bin/env bash
+args=()
+while [[ $# -gt 0 ]]; do
+  if [[ "$1" == "--ro" && "$2" == "/" ]]; then
+    args+=("--rox" "/")
+    shift 2
+  else
+    args+=("$1")
+    shift
+  fi
+done
+exec "$HOME/.local/bin/landrun" "${args[@]}"
+EOF
+sed -i "s|\$HOME|$HOME|g" "$LANDRUN_WRAPPER"
+chmod +x "$LANDRUN_WRAPPER"
+
+export COMPARATOR_LANDRUN="$LANDRUN_WRAPPER"
+
+NANODA_BIN="$WORK/nanoda_lib/target/release/nanoda_bin"
+
+if [ ! -d "$WORK/nanoda_lib" ]; then
+  git clone -q --no-checkout https://github.com/ammkrn/nanoda_lib "$WORK/nanoda_lib"
+fi
+git -C "$WORK/nanoda_lib" fetch -q --depth 1 origin "$NANODA_REF"
+
+FETCH_SHA="$(git -C "$WORK/nanoda_lib" rev-parse FETCH_HEAD)"
+if [ ! -x "$NANODA_BIN" ] || [ "$FETCH_SHA" != "$NANODA_REF" ]; then
+  git -C "$WORK/nanoda_lib" checkout -q FETCH_HEAD
+  echo "Building nanoda from pinned Rust ${RUST_VERSION}..."
+  curl -fsSL -o /tmp/rust.tar.gz \
+    "https://static.rust-lang.org/dist/rust-${RUST_VERSION}-x86_64-unknown-linux-gnu.tar.gz"
+  verify_sha256 /tmp/rust.tar.gz "$RUST_SHA256"
+  tar -xzf /tmp/rust.tar.gz -C /tmp
+  /tmp/rust-${RUST_VERSION}-x86_64-unknown-linux-gnu/install.sh \
+    --prefix="$HOME/.local" --without=rust-docs
+  (cd "$WORK/nanoda_lib" && PATH="$HOME/.local/bin:$PATH" cargo build --release)
+else
+  git -C "$WORK/nanoda_lib" checkout -q FETCH_HEAD
+fi
+
+export COMPARATOR_NANODA="$NANODA_BIN"
+
+export PATH="$WORK/lean4export/.lake/build/bin:$WORK/comparator/.lake/build/bin:$HOME/.local/bin:$HOME/.elan/bin:$PATH"
+
+cd "$WS"
+lake exe cache get
+CHALLENGE="$(grep -o '"challenge_module"[[:space:]]*:[[:space:]]*"[^"]*"' config.json | grep -o '"[^"]*"$' | tr -d '"')"
+SOLUTION="$(grep -o '"solution_module"[[:space:]]*:[[:space:]]*"[^"]*"' config.json | grep -o '"[^"]*"$' | tr -d '"')"
+lake build "$CHALLENGE" "$SOLUTION"
+exec lake env comparator config.json
diff --git a/verify_docker.sh b/verify_docker.sh
new file mode 100755
index 0000000000..1ffed8a1cc
--- /dev/null
+++ b/verify_docker.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+CACHE="${COMPARATOR_WORK:-$HOME/.cache/comparator-verify}"
+mkdir -p "$CACHE/home" "$CACHE/docker"
+
+source "$HERE/comparator/versions.env"
+
+PLATFORM=()
+if [[ "$(uname -m)" != "x86_64" ]]; then
+  echo "note: non-x86_64 host — using --platform linux/amd64 (requires QEMU, will be slow)"
+  PLATFORM=(--platform linux/amd64)
+fi
+
+exec docker run --rm "${PLATFORM[@]}" \
+  --volume "$HERE:/repo:ro,z" \
+  --volume "$CACHE:/cache:z" \
+  --env "COMPARATOR_WORK=/cache/docker" \
+  --env "HOME=/cache/home" \
+  "$UBUNTU_IMAGE" \
+  bash -c "
+    apt-get update -qq && apt-get install -y -qq curl git zstd ca-certificates build-essential
+    mkdir /work
+    tar -C /repo --exclude='.lake' --exclude='.git' -cf - . | tar -C /work -xf -
+    cd /work
+    bash /work/verify.sh
+  "