lean-proofs.yml

# SPDX-License-Identifier: MPL-2.0
# lean-proofs.yml — machine-checks the Lean 4 formal-verification proofs.
#
# Guards the root cause documented in docs/proofs/verification/AUDIT.md: the
# proofs had bit-rotted because no CI ever ran the prover. This gate keeps the
# "sorry-free, compiles" invariant honest from now on.
name: lean-proofs

on:
  push:
    paths:
      - 'docs/proofs/verification/**'
      - '.github/workflows/lean-proofs.yml'
  pull_request:
    paths:
      - 'docs/proofs/verification/**'
      - '.github/workflows/lean-proofs.yml'

permissions:
  contents: read

jobs:
  lean-check:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

      - name: Install Lean (version pinned by lean-toolchain)
        run: |
          set -euo pipefail
          ver="$(sed -E 's#.*:v##' docs/proofs/verification/lean-toolchain)"
          echo "Installing Lean ${ver}"
          sudo apt-get update
          sudo apt-get install -y zstd
          curl -sSL -o /tmp/lean.tar.zst \
            "https://github.com/leanprover/lean4/releases/download/v${ver}/lean-${ver}-linux.tar.zst"
          sudo mkdir -p /opt/lean
          sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst -C /opt/lean
          echo "/opt/lean/lean-${ver}-linux/bin" >> "$GITHUB_PATH"

      - name: Verify WokeLang.lean (sorry-free; must exit 0 with no errors)
        run: |
          set -euo pipefail
          lean --version
          lean docs/proofs/verification/WokeLang.lean
          echo "✅ WokeLang.lean verified"

      - name: Verify WokeGrammar.lean (grammar proofs; sorry-free; must exit 0)
        run: |
          set -euo pipefail
          lean docs/proofs/verification/WokeGrammar.lean
          echo "✅ WokeGrammar.lean verified"

      - name: Verify WokeGrammarStructure.lean (no-left-recursion + lexer + classification)
        run: |
          set -euo pipefail
          lean docs/proofs/verification/WokeGrammarStructure.lean
          echo "✅ WokeGrammarStructure.lean verified"

      - name: Verify WokeGrammarRegular.lean (§7.1 not-regular: DFA + pigeonhole)
        run: |
          set -euo pipefail
          lean docs/proofs/verification/WokeGrammarRegular.lean
          echo "✅ WokeGrammarRegular.lean verified"

      - name: Verify WokeGrammarCFL.lean (§7.3 CFL closure: union/concat/star)
        run: |
          set -euo pipefail
          lean docs/proofs/verification/WokeGrammarCFL.lean
          echo "✅ WokeGrammarCFL.lean verified"

      - name: Verify WokeGrammarPumping.lean (§7.3 non-closure: pumping foundation)
        run: |
          set -euo pipefail
          lean docs/proofs/verification/WokeGrammarPumping.lean
          echo "✅ WokeGrammarPumping.lean verified"