benchmarks.yml

# Nightly / relevant-PR real-world and release-grade benchmarks.
name: benchmarks

on:
  schedule:
    - cron: "0 6 * * *"
  workflow_dispatch:
  pull_request:
    paths:
      - "benchmarks/**"
      - "foundry/**"
      - "scripts/build_foundry_corpus.py"
      - "scripts/validate_foundry_corpus.py"
      - "scripts/run_tool_selection_benchmark.py"
      - "scripts/run_agent_held_out.py"
      - "scripts/run_real_world.py"
      - "scripts/run_property_tests.py"
      - "scripts/run_metamorphic.py"
      - "scripts/run_perf_budgets.py"
      - "scripts/run_differential_backends.py"
      - "scripts/run_leanlink_fuzz_stubs.py"
      - "scripts/run_ideal_membership_benchmark.py"
      - "scripts/smoke_ideal_membership.py"
      - "scripts/generate_exact_ideal_replay_module.py"
      - "scripts/ci/run_cr_exact_lean_e2e.py"
      - "scripts/ci/run_cr_exact_lean_e2e_production.py"
      - "tests/forensic/test_ideal_benchmark_scoring.py"
      - "registry/maturity-inventory.json"
      - "registry/capabilities/**"
      - "adapters/common/exact_replay/**"
      - "MathEvidence/Checkers/IdealMembership/**"
      - "MathEvidence/Core/ExprSerialize.lean"
      - "MathEvidence/Exe/DeclarationIdentity.lean"
      - "adapters/common/ideal_membership.py"
      - "adapters/common/kernel_replay.py"
      - "adapters/common/environment_lock.py"
      - "agent/api/receipt.py"
      - ".github/workflows/benchmarks.yml"
      - ".github/workflows/lean.yml"
      - ".github/workflows/release.yml"

permissions:
  contents: read

concurrency:
  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: true

jobs:
  # Mathematical/task benchmark behavior (not assurance policy).
  benchmark-task-suite:
    runs-on: ubuntu-latest
    timeout-minutes: 20
    steps:
      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4

      - name: Inventory benchmark trees
        run: |
          find benchmarks -type f | sort
          test -d benchmarks/adversarial/seed
          test -d benchmarks/real_world
          test -d benchmarks/conformance
          test -d benchmarks/agent/held_out
          test -d benchmarks/tool_selection
          test -d foundry/corpus/v0.1
          echo "benchmarks skeleton ok"

      - name: Setup Python
        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5
        with:
          python-version: "3.12"

      - name: Install uv (SHA-pinned)
        uses: astral-sh/setup-uv@d4b2f3b6ecc6e67c4457f6d3e41ec42d3d0fcb86 # v5.4.2
        with:
          enable-cache: true

      - name: Install dependencies (frozen lock required)
        run: |
          set -euo pipefail
          test -f uv.lock
          uv sync --frozen --extra dev --extra sympy
          echo "$PWD/.venv/bin" >> "$GITHUB_PATH"

      - name: Ideal-membership scoring trust regression
        run: python -m pytest tests/forensic/test_ideal_benchmark_scoring.py -q

      - name: Ideal-membership frozen 55-task corpus (candidate/checker tier)
        env:
          MATHEVIDENCE_IDEAL_BACKEND: sympy
        run: |
          set -euo pipefail
          python scripts/run_ideal_membership_benchmark.py --tier candidate | tee /tmp/ideal-candidate.json
          python - <<'PY'
          import json
          from pathlib import Path

          p = json.loads(Path("/tmp/ideal-candidate.json").read_text(encoding="utf-8"))
          manifest = json.loads(
              Path("benchmarks/ideal_membership/manifest.json").read_text(encoding="utf-8")
          )
          expected_scored = int(manifest["passTasks"]) + int(manifest["xfailTasks"])
          assert p.get("tier") == "candidate", p.get("tier")
          assert p.get("taskCount") == manifest.get("taskCount"), (p.get("taskCount"), manifest.get("taskCount"))
          assert p.get("scoredTasks") == expected_scored, (p.get("scoredTasks"), expected_scored)
          assert p.get("skipped") == manifest.get("skipTasks"), (p.get("skipped"), manifest.get("skipTasks"))
          assert p.get("passed") == p.get("scoredTasks"), (p.get("passed"), p.get("scoredTasks"))
          assert p.get("criticalFalseAcceptCount") == 0, p.get("criticalFalseAcceptTasks")
          assert not p.get("criticalFalseAcceptTasks"), p.get("criticalFalseAcceptTasks")
          assert p.get("adapterCheckerDisagreementCount") == 0, p.get("adapterCheckerDisagreementTasks")
          for task in p.get("tasks") or []:
              assert (task.get("lean") or {}).get("resultStatus") is None, task.get("id")
          print(
              "ideal frozen corpus OK:",
              p.get("taskCount"),
              "tasks; scored=", p.get("scoredTasks"),
              "false_accepts=", p.get("criticalFalseAcceptCount"),
          )
          PY

      - name: Agent held-out suite
        run: python scripts/run_agent_held_out.py

      - name: Real-world bottleneck obligations
        run: python scripts/run_real_world.py

      - name: Property tests
        run: python scripts/run_property_tests.py

      - name: Metamorphic suite
        run: python scripts/run_metamorphic.py

      - name: Perf budgets (blocking on regression)
        run: python scripts/run_perf_budgets.py

      - name: Differential backends (skip/fixture without Wolfram)
        run: python scripts/run_differential_backends.py

      - name: Build Foundry corpus (idempotent)
        run: python scripts/build_foundry_corpus.py

      - name: Validate Foundry corpus
        run: python scripts/validate_foundry_corpus.py

      - name: Tool-selection benchmark
        run: python scripts/run_tool_selection_benchmark.py

  # Bounded exact theorem subset: backend-proposed multipliers -> exact Lean
  # theorem -> Lean.Environment identity -> strict Certification Record.
  # The full 55-task corpus runs separately above. Benchmark score never grants
  # CR eligibility.
  ideal-release-grade:
    runs-on: ubuntu-latest
    timeout-minutes: 30
    steps:
      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4

      - name: Install elan (checksum-pinned release asset)
        run: bash scripts/ci/install-elan-pinned.sh

      - name: Restore pinned Mathlib build cache
        run: |
          set -euo pipefail
          lake exe cache get

      - name: Setup Python
        uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5
        with:
          python-version: "3.12"

      - name: Install uv (SHA-pinned)
        uses: astral-sh/setup-uv@d4b2f3b6ecc6e67c4457f6d3e41ec42d3d0fcb86 # v5.4.2
        with:
          enable-cache: true

      - name: Install dependencies (frozen lock required)
        run: |
          set -euo pipefail
          test -f uv.lock
          uv sync --frozen --extra dev --extra sympy
          echo "$PWD/.venv/bin" >> "$GITHUB_PATH"

      - name: Build exact replay dependencies
        run: |
          set -euo pipefail
          echo "::notice title=ideal-release-grade setup::Lake build of exact-replay deps. Failure here is setup/replay, not benchmark scoring."
          lake build MathEvidenceCheckers mathevidence-declaration-identity

      - name: Ideal membership bounded exact theorem subset
        env:
          MATHEVIDENCE_IDEAL_BENCH_TIER: release
          MATHEVIDENCE_IDEAL_BACKEND: sympy
        run: |
          set -euo pipefail
          echo "::notice title=ideal-release-grade bench::Bounded exact-CR subset. The full 55-task candidate/checker corpus is a separate job."
          python scripts/run_ideal_membership_benchmark.py --tier release | tee /tmp/ideal-release.json
          python - <<'PY'
          import json
          p = json.load(open("/tmp/ideal-release.json", encoding="utf-8"))
          tasks = p.get("tasks") or []
          release_tasks = p.get("releaseCertificationTasks") or []
          assert p.get("tier") == "release", p.get("tier")
          assert p.get("taskCount") == len(release_tasks) == len(tasks) and len(tasks) > 0
          assert {t.get("id") for t in tasks} == set(release_tasks)
          assert p.get("passed") == p.get("scoredTasks") and p.get("scoredTasks", 0) > 0
          assert p.get("criticalFalseAcceptCount") == 0, p.get("criticalFalseAcceptTasks")
          assert "OfflineFixtures" not in (p.get("scoringRule") or "")
          for t in tasks:
              lean = t.get("lean") or {}
              assert lean.get("resultStatus") == "soundness_verified", (t.get("id"), lean)
              assert lean.get("certificationRecordDigest"), t.get("id")
              assert lean.get("identityAuthority") == "Lean.Environment ConstantInfo", lean
          assert "crEligible" not in p
          print("ideal bounded exact subset OK:", p.get("passed"), "Certification Records")
          PY