ci(proofs): gate the Lean 4 verification corpus (verification/proofs/lean4)

.github/workflows/dogfood-proofs-ci.yml

@@ -18,12 +18,14 @@ on:
     branches: [main]
     paths:
       - 'proofs/**'
+      - 'verification/proofs/lean4/**'
       - 'Justfile'
       - '.github/workflows/dogfood-proofs-ci.yml'
   pull_request:
     branches: [main]
     paths:
       - 'proofs/**'
+      - 'verification/proofs/lean4/**'
       - 'Justfile'
       - '.github/workflows/dogfood-proofs-ci.yml'
   workflow_dispatch:
@@ -115,6 +117,56 @@ jobs:
       - name: Build Lean corpus
         run: just proofs-lean
 
+  verif-lean:
+    name: Lean 4 (verification)
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      - name: Install elan + pinned Lean toolchain
+        run: |
+          set -euo pipefail
+          # Mirrors the `lean` job: install the elan shim only, then pre-install the
+          # toolchain pinned by verification/proofs/lean4/lean-toolchain with
+          # retry/backoff so the Build step does not lazily resolve it (elan's release
+          # tag lookup against the GitHub API can transiently fail). This corpus has no
+          # mathlib dependency (lake-manifest packages: []), so it builds fast.
+          curl -fsSL --retry 3 \
+            https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          export PATH="$HOME/.elan/bin:$PATH"
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          toolchain="$(tr -d '[:space:]' < verification/proofs/lean4/lean-toolchain)"
+          for attempt in 1 2 3 4 5; do
+            if elan toolchain install "$toolchain"; then
+              break
+            fi
+            if [ "$attempt" -eq 5 ]; then
+              echo "elan toolchain install failed after 5 attempts" >&2
+              exit 1
+            fi
+            backoff=$((attempt * 5))
+            echo "elan toolchain install failed (attempt $attempt); retrying in ${backoff}s" >&2
+            sleep "$backoff"
+          done
+          elan default "$toolchain"
+          lean --version
+
+      - name: Install just
+        run: |
+          set -euo pipefail
+          curl -fsSL --retry 3 \
+            "https://github.com/casey/just/releases/download/1.51.0/just-1.51.0-x86_64-unknown-linux-musl.tar.gz" \
+            -o /tmp/just.tar.gz
+          mkdir -p "$HOME/.local/bin"
+          tar xzf /tmp/just.tar.gz -C "$HOME/.local/bin" just
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+
+      - name: Build Lean verification corpus
+        run: just proofs-verif-lean
+
   agda:
     name: Agda
     runs-on: ubuntu-latest

Justfile

@@ -250,7 +250,7 @@ test-s4-loop:
 # exact same commands.
 
 # Type-check the whole dogfood proof corpus across every assistant.
-proofs: proofs-coq proofs-lean proofs-agda proofs-idris
+proofs: proofs-coq proofs-lean proofs-agda proofs-idris proofs-verif-lean
 
 # Compile the Coq proof corpus (proofs/coq/**/*.v).
 proofs-coq:
@@ -284,6 +284,14 @@ proofs-agda:
 proofs-idris:
     cd src/idris && idris2 --typecheck echidna-validator.ipkg
 
+# Distinct from proofs-lean: the verification-pipeline *property* proofs
+# (ConfidenceLattice, ParetoMaximality, ParetoStrongMaximality, IntegrityVerification,
+# PortfolioCompleteness) under verification/proofs/lean4, not the dogfood corpus under
+# proofs/lean. No mathlib dependency (lake-manifest packages: []), so the build is light.
+# Build the Lean 4 trust-pipeline property proofs via Lake (verification/proofs/lean4).
+proofs-verif-lean:
+    cd verification/proofs/lean4 && lake build
+
 # Format code
 fmt:
     cargo fmt