ci.yml

name: CI

on:
  push:
    branches: ["main", "recovery/**", "feature/**", "fix/**", "test/**", "docs/**", "release/**"]
  pull_request:
    branches: ["main", "master", "recovery/**"]

permissions:
  contents: read

concurrency:
  group: ci-${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  lean-build:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout
        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2

      - name: Lean build
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
          lint: false

  lean-lint:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
          lint: true

  prohibited-tactics:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: actions/setup-python@0b93645e9fea7318ecaed2b359559ac225c90a2b # v5.3.0
        with:
          python-version: "3.11"
      - name: Prohibited tactic scan
        run: python scripts/scan_prohibited_tactics.py

  axiom-audit:
    runs-on: ubuntu-latest
    needs: [lean-build]
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - name: Sync frozen deps
        run: uv sync --frozen --all-extras
      - name: Generate concrete module for axiom audit
        run: |
          OUT_DIR="${RUNNER_TEMP}/lv-axiom-generated"
          mkdir -p "${OUT_DIR}"
          uv run leanverifier generate \
            --model examples/affine_binary/model.json \
            --request examples/affine_binary/request.json \
            --out-dir "${OUT_DIR}"
          echo "GENERATED_DIR=${OUT_DIR}" >> "${GITHUB_ENV}"
          echo "GENERATED_FILE=$(ls "${OUT_DIR}"/GeneratedModel_*.lean | head -n 1)" >> "${GITHUB_ENV}"
      - name: Run axiom audit (library + generated)
        run: |
          uv run python scripts/audit_axioms.py \
            --generated "${GENERATED_FILE}" \
            --report "${RUNNER_TEMP}/axiom-report.txt"
      - name: Upload axiom report
        uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0
        with:
          name: axiom-report
          path: ${{ runner.temp }}/axiom-report.txt

  lean4checker:
    runs-on: ubuntu-latest
    needs: [lean-build]
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
      - name: lean4checker --fresh
        run: |
          chmod +x scripts/run_lean4checker.sh
          scripts/run_lean4checker.sh "${GITHUB_WORKSPACE}" \
            "${RUNNER_TEMP}/axiom-report-lean4checker.txt"
      - name: Upload lean4checker report
        uses: actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08 # v4.6.0
        if: always()
        with:
          name: axiom-report-lean4checker
          path: ${{ runner.temp }}/axiom-report-lean4checker.txt

  python-unit:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - name: Sync frozen deps
        run: uv sync --frozen --all-extras
      - name: Ruff
        run: |
          uv run ruff check src/leanverifier tests scripts
          uv run ruff format --check src/leanverifier tests scripts
      - name: Mypy
        run: uv run mypy src/leanverifier
      - name: Pytest unit + coverage
        # Include security + non-lean integration so CLI/evidence paths count toward
        # the gate; lake-backed verify stays in dedicated jobs.
        run: >
          uv run python -m pytest
          tests/unit tests/schema tests/security tests/integration
          -m "not lean"
          --cov=src/leanverifier --cov-fail-under=70

  schema-negative:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - run: uv run python -m pytest tests/schema -m schema -k negative

  generator-determinism:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - run: uv run python -m pytest tests/unit/test_generator_determinism.py -m unit

  verify-positive:
    runs-on: ubuntu-latest
    needs: [lean-build]
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - name: Warm packaged Lake cache
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
        run: uv run python scripts/warm_packaged_lake.py --seed-from .
      - name: Positive verify + inspect (markers, not -k alone)
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
        run: uv run python -m pytest tests/integration -m "positive and lean" --maxfail=1

  integration-negative:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - run: uv run python -m pytest tests/integration -m "negative"

  mutation:
    runs-on: ubuntu-latest
    needs: [lean-build]
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - name: Warm packaged Lake cache
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
        run: uv run python scripts/warm_packaged_lake.py --seed-from .
      - name: Mutation table (verify/audit/inspect)
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
        run: uv run python -m pytest tests/mutation -m mutation --maxfail=1

  security-tests:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - run: uv run python -m pytest tests/security -m security

  security-windows:
    runs-on: windows-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - name: Security suite on Windows
        run: uv run python -m pytest tests/security -m security

  docs-claims:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - run: uv run python scripts/verify_docs.py --mode claims

  docs-links:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - run: uv run python scripts/verify_docs.py --mode links

  docs-commands:
    runs-on: ubuntu-latest
    needs: [lean-build]
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - run: uv sync --frozen --all-extras
      - name: Warm packaged Lake cache
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
        run: uv run python scripts/warm_packaged_lake.py --seed-from .
      - name: Execute README/user-guide CLI commands
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
        run: uv run python scripts/verify_docs.py --mode commands

  wheel-smoke:
    runs-on: ubuntu-latest
    needs: [lean-build]
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true
      - name: Sync frozen deps
        run: uv sync --frozen --all-extras
      - name: Warm packaged Lake cache
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
        run: uv run python scripts/warm_packaged_lake.py --seed-from .
      - name: Build wheel and sdist
        run: uv build
      - name: Smoke install from /tmp with verify
        env:
          LEANVERIFIER_CACHE: /tmp/lv-pkg-cache
          LEANVERIFIER_VERIFY_TIMEOUT: "1800"
        run: |
          uv run python scripts/smoke_wheel.py --dist dist --artifact both --require-verify

  docker-build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
      - name: Build Lean-only Docker image
        run: docker build -t leanverifier:ci .
      - name: Run formal checks in container
        run: |
          docker run --rm leanverifier:ci lake build
          docker run --rm --entrypoint lake leanverifier:ci env lean LeanVerifier/Audit/PublicAxioms.lean

  clean-worktree:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2

      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
        with:
          build: true
          lint: false

      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
        with:
          python-version: "3.11"
          enable-cache: true

      - name: Sync frozen deps
        run: uv sync --frozen --all-extras

      - name: Pytest (unit + schema subset)
        run: uv run python -m pytest tests/unit tests/schema -q

      - name: Axiom audit
        run: uv run python scripts/audit_axioms.py

      - name: Prohibited tactic scan
        run: python scripts/scan_prohibited_tactics.py

      - name: Docs verify (claims + links)
        run: |
          uv run python scripts/verify_docs.py --mode claims
          uv run python scripts/verify_docs.py --mode links

      - name: Generate outside checkout
        run: |
          OUT_DIR="${RUNNER_TEMP}/lv-clean-worktree-generate"
          mkdir -p "${OUT_DIR}"
          uv run leanverifier generate \
            --model examples/affine_binary/model.json \
            --request examples/affine_binary/request.json \
            --out-dir "${OUT_DIR}"

      - name: Worktree remains clean
        run: test -z "$(git status --porcelain)"