diff --git a/.github/workflows/proofcheck-agent.yml b/.github/workflows/proofcheck-agent.yml new file mode 100644 index 0000000..f5be16e --- /dev/null +++ b/.github/workflows/proofcheck-agent.yml @@ -0,0 +1,63 @@ +# proofcheck agent evidence (EXPERIMENTAL, opt-in). +# +# When the evidence run finds no proof for a "fixes #N" claim, an LLM agent +# tries to write a reproduction test, and proofcheck runs it on base and head. +# The work is split over separate jobs (separate VMs): +# gate - decides whether to run; reads the API only, runs no PR code +# propose - holds the LLM key; reads the PR as data, never installs or runs it +# verify - runs the candidate tests on base and head; no secrets, read-only token +# comment - re-posts the card with the agent section; never runs PR code +# +# Setup: repository secret PROOFCHECK_LLM_API_KEY, repository variables +# PROOFCHECK_LLM_PROVIDER (anthropic | openai) and PROOFCHECK_LLM_MODEL +# (optional: PROOFCHECK_LLM_BASE_URL). By default the agent only runs for pull +# requests by owners, members and collaborators, or labelled `proofcheck:agent`. +# +# Generated by `proofcheck init --agent`. +name: proofcheck agent + +on: + workflow_run: + workflows: ["proofcheck"] # must match the `name:` of proofcheck.yml + types: [completed] + +permissions: {} + +jobs: + agent: + if: github.event.workflow_run.event == 'pull_request' && github.event.workflow_run.conclusion != 'cancelled' + permissions: + contents: read + actions: read + pull-requests: read + issues: read + uses: bhaskargurram-ai/proofcheck/.github/workflows/agent.yml@v1.0 + with: + proofcheck-ref: v1.0 + llm-provider: ${{ vars.PROOFCHECK_LLM_PROVIDER }} + llm-model: ${{ vars.PROOFCHECK_LLM_MODEL }} + llm-base-url: ${{ vars.PROOFCHECK_LLM_BASE_URL }} + llm-reasoning-effort: ${{ vars.PROOFCHECK_LLM_REASONING_EFFORT }} + python-version: "3.12" + install-command: >- + python -m pip install --quiet --no-deps -e ./adapters/python && + python -m pip install --quiet pytest pytest-asyncio "langgraph>=1.0" "langchain-core>=1.0" "openai-agents>=0.22" "claude-agent-sdk>=0.2" pyyaml + run-for: trusted # or "everyone" (spends API credits on any fork PR) + secrets: + llm-api-key: ${{ secrets.PROOFCHECK_LLM_API_KEY }} + + comment: + needs: agent + if: needs.agent.outputs.verified == 'true' + permissions: + contents: read + actions: read + pull-requests: write + uses: bhaskargurram-ai/proofcheck/.github/workflows/comment.yml@v1.0 + with: + proofcheck-ref: v1.0 + # Trusted values: the PR number comes from the gate job (API data, no PR + # code ran there) and the artifact from this run's verify job. + pr-number: ${{ needs.agent.outputs.pr-number }} + artifact-run-id: ${{ github.run_id }} + labels: true diff --git a/.github/workflows/proofcheck-comment.yml b/.github/workflows/proofcheck-comment.yml new file mode 100644 index 0000000..2cab83b --- /dev/null +++ b/.github/workflows/proofcheck-comment.yml @@ -0,0 +1,29 @@ +# proofcheck, part 2 of 2: post the proof card (PRIVILEGED, never runs PR code). +# +# Triggered when the `proofcheck` workflow completes. `workflow_run` runs with +# a token that can comment, so the reusable workflow never checks out, +# installs or executes anything from the pull request: it downloads the result +# artifact, validates it, re-renders the card, upserts one comment and sets a +# `proofcheck: ` label. Do not use `pull_request_target` instead. +# +# Generated by `proofcheck init`. +name: proofcheck comment + +on: + workflow_run: + workflows: ["proofcheck"] # must match the `name:` of proofcheck.yml + types: [completed] + +permissions: {} + +jobs: + comment: + if: github.event.workflow_run.event == 'pull_request' && github.event.workflow_run.conclusion != 'cancelled' + permissions: + contents: read + actions: read # download the artifact of the triggering run + pull-requests: write # upsert the comment and the verdict label + uses: bhaskargurram-ai/proofcheck/.github/workflows/comment.yml@v1.0 + with: + proofcheck-ref: v1.0 + labels: true diff --git a/.github/workflows/proofcheck.yml b/.github/workflows/proofcheck.yml new file mode 100644 index 0000000..63706d6 --- /dev/null +++ b/.github/workflows/proofcheck.yml @@ -0,0 +1,35 @@ +# proofcheck, part 1 of 2: gather evidence (UNPRIVILEGED). +# +# Runs on `pull_request`, so for pull requests from forks GitHub gives this +# workflow a read-only token and no secrets. Untrusted PR code (tests, issue +# reproducers) only ever runs here. The proof card goes to the job summary and +# into the `proofcheck-result` artifact; proofcheck-comment.yml posts it. +# +# Generated by `proofcheck init`. Pin the reusable workflow to a release tag +# or, stricter, to a full commit SHA, and keep `proofcheck-ref` the same. +name: proofcheck + +on: + pull_request: + types: [opened, synchronize, reopened, edited] + +permissions: + contents: read + issues: read # read linked issues on private repositories (read-only) + +concurrency: + group: proofcheck-${{ github.event.pull_request.number }} + cancel-in-progress: true + +jobs: + evidence: + uses: bhaskargurram-ai/proofcheck/.github/workflows/evidence.yml@v1.0 + with: + proofcheck-ref: v1.0 + python-version: "3.12" + timeout-minutes: 90 # Rust: compiling the workspace for base, head and ablation takes a while + # Installs the project under test; this runs PR code (unprivileged job). + install-command: >- + python -m pip install --quiet --no-deps -e ./adapters/python && + python -m pip install --quiet pytest pytest-asyncio "langgraph>=1.0" "langchain-core>=1.0" "openai-agents>=0.22" "claude-agent-sdk>=0.2" pyyaml + fail-on: never # or "contradicted" / "no-evidence" to fail the check diff --git a/proofcheck.toml b/proofcheck.toml new file mode 100644 index 0000000..b49c7eb --- /dev/null +++ b/proofcheck.toml @@ -0,0 +1,52 @@ +# proofcheck configuration (https://github.com/bhaskargurram-ai/proofcheck). +# +# Read from the pull request's BASE commit, so a PR cannot weaken its own +# check. Every key is optional; the commented values are the defaults. + +# runner = "cargo" # pytest | unittest | jest | cargo +# test_command = "" # custom command; placeholders {junitxml} and {tests} +# setup_command = "" # run once in each worktree before the tests +# timeout = 600 # seconds per test run +# test_env = { PYTHONHASHSEED = "0" } +# benchmark_command = "" # e.g. "python bench.py": lets "2x faster" claims be checked +# benchmark_runs = 5 +# large_diff_threshold = 1000 +# max_issues = 5 + +# [repro] # replay ```python and >>> reproducers from linked issues +# enabled = true +# timeout = 60 + +[ablation] # diff evidence map: revert each changed hunk, re-run the evidence +enabled = true +max_hunks = 12 +time_budget_s = 1200 # Rust: each hunk rebuilds the crate +# exclude = ["*.md", "*.rst", "*.txt", "docs/*", "LICENSE*", "CHANGELOG*", ".github/*"] + +# [llm] # optional LLM claim extraction (off by default) +# enabled = false +# provider = "anthropic" # or "openai" for any OpenAI-compatible endpoint +# model = "" # the key comes from PROOFCHECK_LLM_API_KEY, never from this file + +[agent] # experimental agent evidence (proofcheck-agent.yml) +enabled = true +# variants = 3 +# max_rounds = 2 +# max_tool_calls = 25 +# when = "missing-evidence" # or "always" +# test_dir = "tests/proofcheck_agent" + +# Test projects (detected by `proofcheck init`). Each changed file belongs to the deepest +# project containing it; tests run inside the project's directory. Per-project keys: +# runner, test_command, setup_command, test_paths, timeout, test_env, cargo_target_dir. + +[[project]] +name = "rust" +path = "." +runner = "cargo" +# timeout = 1800 # seconds per run (cargo default: 30 minutes) + +[[project]] +name = "python" +path = "adapters/python" +runner = "pytest"