docs(pilot): link the recovery audit to the follow-up PR

fix(pilot): preserve partial results and stop on provider billing errors
2026-10-28 19:08:30 +08:00 · 2026-10-28 19:04:43 +08:00
14 changed files with 341 additions and 2075 deletions
@@ -29,20 +29,3 @@ jobs:
          (find / -maxdepth 4 \( -name 'lake-manifest.json' -o -name '.lake' \) -not -path '/proc/*' 2>/dev/null | head -20) || true
          (docker images 2>&1 | head -20) || true
          (docker ps -a 2>&1 | head -10) || true
      - name: Read-only storage diagnosis
        run: |
          set -eu
          hostname
          lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS
          findmnt -T /var/lib/docker
          df -hT / /var/lib/docker
          docker info --format 'storage={{.Driver}} root={{.DockerRootDir}}'
          docker system df
          docker builder du 2>/dev/null || true
          for dir in /var/lib/docker /var/lib/containerd /opt/lean-cache /var/cache /tmp /var/log; do
            if [ -d "$dir" ]; then du -xhd1 "$dir" 2>/dev/null || true; fi
          done
          for tool in sfdisk growpart resize2fs xfs_growfs; do command -v "$tool" || true; done
          if [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ] && command -v growpart >/dev/null; then
            growpart -N /dev/nvme0n1 3 || true
          fi
@@ -1,49 +0,0 @@
 name: runner-storage-maintenance
 # Manual-only. Never runs on push or pull_request.
 on:
  workflow_dispatch:
    inputs:
      confirm:
        description: Enter EXPAND_RUNNER_ROOT after owner approval
        required: true
        type: string
 jobs:
  expand-root:
    if: ${{ github.event_name == 'workflow_dispatch' && inputs.confirm == 'EXPAND_RUNNER_ROOT' }}
    runs-on: ubuntu24.04-x64-lean4.35
    timeout-minutes: 20
    steps:
      - name: Back up partition table and expand the authorized ext4 root
        run: |
          # Owner-authorized manual-only root partition/filesystem expansion.
          set -euo pipefail
          exec 9>/var/lock/lean-bench-root-maintenance.lock
          flock -n 9
          [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ]
          [ "$(id -u)" = 0 ]
          [ "$(blkid -s PARTUUID -o value /dev/nvme0n1p3 | tr A-Z a-z)" = 9b694bad-5bbb-4485-860f-e5544ae47410 ]
          [ "$(findmnt -n -o SOURCE /)" = /dev/nvme0n1p3 ]
          [ "$(findmnt -n -o FSTYPE /)" = ext4 ]
          [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ]
          [ "$(blockdev --getsize64 /dev/nvme0n1)" -ge 161061273600 ]
          backup_dir="/root/lean-bench-maintenance/$(date -u +%Y%m%dT%H%M%SZ)"
          install -d -m 700 "$backup_dir"
          sfdisk --dump /dev/nvme0n1 > "$backup_dir/nvme0n1.sfdisk"
          sync
          printf 'Partition-table backup: %s\n' "$backup_dir/nvme0n1.sfdisk"
          set +e
          growpart -N /dev/nvme0n1 3 > "$backup_dir/growpart-dry-run.log" 2>&1
          probe_status=$?
          set -e
          if [ "$probe_status" = 0 ]; then
            growpart /dev/nvme0n1 3
          elif ! grep -q '^NOCHANGE:' "$backup_dir/growpart-dry-run.log"; then
            cat "$backup_dir/growpart-dry-run.log"
            exit "$probe_status"
          fi
          resize2fs /dev/nvme0n1p3
          [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ]
          lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS
          df -hT / /var/lib/docker
@@ -0,0 +1,82 @@
 # P0 execution report: 2026-10-28
 **Status: blocked by provider billing. No GO, PARTIAL or NO-GO decision.**
 The owner requested delivery of the fixes and this report now, with the remaining paid calls deferred.
 ## What ran
 The owner explicitly authorized sending the 65 textbook passages and corresponding Lean code
 through the existing DashScope endpoint to `qwen-max`, at temperature 0 and a cumulative ceiling
 of 400 HTTP requests. The run issued **131 HTTP requests**. Provider responses accounted for
 **37,699 input tokens and 7,790 output tokens**, 45,489 total. These are recorded token counts,
 not an invoice or a monetary cost estimate. The client counted 89 received model responses;
 a received response is not necessarily a usable detector result.
 | Coverage | Count |
 |---|---:|
 | Original cohort | 65 |
 | Items with both detectors complete | 42 |
 | Items with one or both detectors missing | 23 |
 | Successful role-extraction/alignment components | 45 |
 | Successful judge components | 43 |
 | Missing role components | 20 |
 | Missing judge components | 22 |
 | Remaining request reservations | 269 |
 DashScope returned HTTP 400 with error code `Arrearage` and its overdue-payment reference.
 The first runner implementation recorded the failures and continued through the cohort, so
 65 saved rows did not mean 65 successful items. The scorer rejected these incomplete outputs.
 No partial-sample gate decision or performance comparison has been produced.
 ## Inputs and labels
 The default `items.jsonl` export omitted `source_text`. All 65 original passages were recovered
 from the matching detection spans and checked byte-for-byte against the archived private
 `review.json`. Item IDs and Lean code were unchanged. The recovery tool also verifies every
 exported field against the archive, normalizing the archive's JSON-encoded imports field.
 Source-inclusive inputs and the regenerated labeling HTML remain in the ignored data directory.
 The owner replaced the planned Kimi/human labeling with Codex annotation. All 65 labels were
 frozen before the first detector request. They contain 30 faithful, 25 wrong, 7 minor drift and
 3 not-formalizable verdicts. This is one AI annotator, **not human gold**. The annotator saw the
 detector implementation and aggregate compilation counts, but not per-item compiler outcomes
 or detector outputs. Syntax/proof defects were ignored when the intended semantics were recoverable;
 no compiler or API-name audit was performed. Independent human auditing remains necessary before
 using these labels as evidence for paper-level claims.
 ## Execution repairs
 - Empty passages and mismatched frozen inputs/labels are rejected before paid calls.
 - Each HTTP attempt reserves cumulative budget before sending, including transport and JSON retries.
  Model, endpoint, temperature, input/label/prompt hashes and cumulative token usage are persisted.
 - Billing/authentication errors now stop immediately, preserving partial results.
 - Resume keeps every successful detector component and retries only missing components. Existing
  rows are replaced atomically rather than duplicated. A budget stop also preserves completed work
  within the current item. A lock prevents concurrent writers.
 - `--audit-only` reconciles saved metadata without API calls. It confirmed 42 complete items,
  23 incomplete items, 42 missing components and 131 already-consumed request reservations.
 - Scoring requires complete results and unchanged frozen-label/result hashes. It restores the
  preregistered complementary-signal PARTIAL rule and uses wrong versus faithful for primary metrics;
  minor drift is included as positive only in the secondary comparison.
 - Detector prompts, matching thresholds, the concept table and frozen annotations were not tuned
  against these outputs. Recovery changes concern transport, persistence and accounting only.
 The private first-attempt output and metadata were backed up before reconciliation. The results
 hash and the frozen-label hash did not change during the offline audit.
 ## Validation and next action
 149 offline unit tests passed, including billing-stop and partial-resume regressions; repository-wide
 Ruff and diff checks passed. These checks did not compile Lean or build Docker locally.
 The initial PR revision passed Python tests and real Lean validation on
 `ubuntu24.04-x64-lean4.35`, runner 7, in [CI #427](https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427).
 The image job was skipped by the PR workflow. The recovery revision's remote result is reported separately in the PR checks.
 After the owner confirms billing recovery, resume the existing run with the same inputs, frozen
 labels and cumulative budget. There are 42 missing components; retries may consume more requests.
 Do not change model or prompts to work around the provider block. Only after all 65 items have
 successful outputs should the scorer produce the registered decision and disagreement report.
 Phase 1 has not started.
 Tracked audit data: `experiments/P0-pilot/results/execution.json` (counts and hashes only).
 Private raw files: `experiments/P0-pilot/data/` (gitignored).
@@ -1,127 +0,0 @@
 # P0: full-cohort GPT-assisted diagnostic (2026-10-28)
 **All 65 items have a fresh source-role description, a fresh semantic judgment and a
 completed deterministic alignment. This is a same-assistant diagnostic, not an independent
 benchmark or a completion of the preregistered Qwen gate. No gate decision is issued.**
 ## Scope and provenance
 The owner requested that the current GPT assistant reassess the entire cohort after the
 Qwen run was interrupted by provider billing failures. Every item was reviewed again;
 no Qwen detector output was reused, and the incomplete Qwen run was not patched with GPT
 outputs. The earlier labels and Qwen files remain unchanged in the original worktree.
 This branch starts at main `5d531c9` and does not depend on the separate billing-recovery PR.
 The source-role structures and four-way judgments were authored directly by the assistant
 in this chat, frozen before computing the new alignment statistics, and replayed by an
 offline script. They were not responses obtained through a GPT API endpoint. The exact
 deployed model identifier, temperature and chat token usage are unavailable; they are not
 invented. There were **zero new external model API calls** for this diagnostic, and no
 DashScope credential was loaded.
 The assistant had already seen the earlier labels, Lean code, detector implementation and
 aggregate compilation statistics. It also viewed passages and Lean together during this
 review. Thus the source descriptions are **not a blinded source-only extraction** and the
 new judgments are **not independent of the reference labels**. Reading only a passage when
 writing a role does not remove prior context exposure. Syntax and proof defects are
 separated from recoverable semantic meaning; no new Lean compilation or library API audit
 was performed. An independent human review remains necessary for research claims.
 ## Results for all 65 items
 | Fresh semantic judgment | Items |
 |---|---:|
 | Faithful | 25 |
 | Minor drift | 13 |
 | Wrong | 24 |
 | Not formalizable from the extracted specification | 3 |
 | Total | 65 |
 The strict binary assistant judge flags every verdict except faithful. The full four-way
 judgment, error categories and an individual explanation are retained for every item.
 Explanations and role descriptions are private because they paraphrase the source passages.
 The unchanged deterministic role matcher flagged **55/65** items. It flagged all **24**
 items newly judged wrong, but also **16/25** newly judged faithful. These are comparisons
 between dependent components of the same diagnostic, not an independently measured recall
 or false-positive rate. They identify an over-sensitive diagnostic behavior worth auditing.
 Common conflict categories across all items include missing objects (41 items), degenerate
 projections (15), goal mismatch (15), missing hypotheses (14), extra hypotheses (13),
 quantifier conflicts (7) and type conflicts (5). Categories overlap. In particular, a named
 source quantity can be computed inline in Lean, a product representation can replace an
 abstract isomorphic group, and a bundled type can encode conditions without separate
 binders. The current lexical matcher does not establish equivalence of those representations.
 These are hypotheses for a later matcher audit, not measured causal explanations for every flag.
 No matching threshold, concept table or authored assessment was changed after the scores
 were inspected.
 ## Relation to the frozen earlier AI labels
 The fresh four-way judgments agree with **59/65** earlier labels. Six changed:
 | Blind ID | Earlier AI label | Fresh judgment |
 |---|---|---|
 | P02 | Faithful | Minor drift |
 | P18 | Faithful | Minor drift |
 | P23 | Faithful | Minor drift |
 | P34 | Faithful | Minor drift |
 | P51 | Faithful | Minor drift |
 | P57 | Wrong | Minor drift |
 The six changes concern representation, type/scope and coverage judgments. They demonstrate
 annotation instability and should be independently adjudicated, not silently overwritten.
 The 59/65 agreement is **not an accuracy estimate**.
 For debugging continuity, the summary contains confusion counts and Wilson intervals against
 the frozen earlier AI labels. The primary comparison excludes earlier minor-drift and
 not-formalizable labels (55 items); the secondary comparison includes minor drift as positive
 (62 items). These tables are explicitly named `reference_agreement`. They cannot establish
 that GPT or role alignment outperforms Qwen. The Qwen coverage is incomplete and this pass
 has different provenance and no independent ground truth. `decision` is null; no GO,
 PARTIAL or NO-GO is computed.
 ## Artifacts and replay
 Tracked, text-free artifacts:
 - `experiments/P0-pilot/results/gpt-diagnostic-summary.json`: provenance, input/assessment/code
  hashes, distributions, fixed matching thresholds and non-independent agreement statistics.
 - `experiments/P0-pilot/results/gpt-diagnostic-items.json`: all 65 blind IDs, verdicts, error
  categories, compile flags, role scores and conflict categories; no passages or explanations.
 - `experiments/P0-pilot/assistant_diagnostic.py`: validates authored inputs and replays the
  existing projection, lint, alignment and statistics code offline.
 - `tests/test_assistant_diagnostic.py`: completeness, identity, schema, offline replay and
  public-output privacy regressions using synthetic text.
 Private artifacts under the gitignored `experiments/P0-pilot/data/gpt-diagnostic/`:
 - `items.jsonl`: source-inclusive copy of the unchanged cohort.
 - `assistant-assessments.json`: all newly authored source structures and judgments, frozen
  before alignment statistics were inspected.
 - `results.jsonl`: complete replay outputs for the 65 items.
 - `review.html`: local, self-contained per-item source/Lean/reason/role/alignment review.
 - `original-hashes.json`: snapshot of the earlier Qwen files and reference labels for
  verifying that this work did not change them.
 Run from the repository root with the private files present:
 ```sh
 PYTHONPATH=. python3 experiments/P0-pilot/assistant_diagnostic.py \
  --items experiments/P0-pilot/data/gpt-diagnostic/items.jsonl \
  --key experiments/P0-pilot/labels/key.json \
  --assessments experiments/P0-pilot/data/gpt-diagnostic/assistant-assessments.json \
  --labels experiments/P0-pilot/labels/labels.json \
  --private-out experiments/P0-pilot/data/gpt-diagnostic \
  --summary experiments/P0-pilot/results/gpt-diagnostic-summary.json \
  --public-items experiments/P0-pilot/results/gpt-diagnostic-items.json
 ```
 The replay is deterministic; it does not regenerate GPT judgments, call a model, or compile
 Lean. Without the private assessment file, public readers can inspect the categorical
 results but cannot reconstruct the authored descriptions and explanations from hashes.
 152 offline unit tests, repository-wide Ruff and diff checks passed locally without a Lean
 or Docker build. Remote Python and real Lean verification use the owner-confirmed
 `ubuntu24.04-x64-lean4.35` tag; the delivered PR records their current status. The existing
 PR workflow skips the Docker image job. No Phase 1 work has started.
@@ -2,7 +2,11 @@
 Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md).
-Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector execution pending explicit data-transfer approval. No pilot API request has been sent.**
+Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector run blocked by DashScope Arrearage after 131 requests. 42 items are complete, 23 need missing detector components. No gate decision has been issued.**
 The owner explicitly authorized sending the 65 passages and Lean code to DashScope/qwen-max,
 then requested fixes and an execution report now, with paid recovery calls deferred.
 Execution report: [P0 execution, 2026-10-28](P0-execution-2026-10-28.md).
 Owner amendment (2026-10-28, in the execution chat): Codex now handles preparation,
 annotation, detector execution and reporting; Kimi's participation is no longer required.
@@ -3,7 +3,7 @@
 Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label `ubuntu24.04-x64-lean4.35`. Both `lean-bench` and `lean-agent` CI run here; the old `gitea-cicd-server-for-CODEX` label is no longer used.
 ## The host
- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 150 GiB system disk (expanded from 100 GiB on 2026-10-28); the ext4 root filesystem reports about 148 GiB, with 75 GiB available immediately after expansion.
+- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 99 GB disk (88 GB free at setup).
 - Lean 4.35.0 via elan 4.2.4 in `/root/.elan`. Python 3.12.3, git 2.43, gcc 13.3, curl, jq.
 - **No Node**, so `actions/checkout` and other JavaScript actions cannot run. Workflows clone with `git fetch --depth 1 origin $SHA` using `${{ github.token }}`.
 - Docker was not installed; the lean-bench `image` job installs `docker.io` + `docker-buildx` (Docker 29.1.3) if missing.
@@ -20,30 +20,3 @@ Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label `
 - Mathlib's post-update hook runs the cache fetch **inside `lake update`**, so retries placed after it never run. Set `MATHLIB_NO_CACHE_ON_UPDATE=1` for `lake update` and fetch in a retry loop. In the image the archives live in a BuildKit cache mount (`/root/.cache/mathlib`), so a retried build resumes.
 - Cold image build about 19 min; with layers cached about 2 min.
 - Gitea 1.26.1 has no cancel-run API; a person cancels in the web UI, then the API can `DELETE` the finished run. The Actions logs endpoint needs a token; the runs/jobs status endpoints work anonymously on this public repo.
 ## Root capacity expansion (2026-10-28)
 The owner expanded the cloud disk to 150 GiB, but root partition `/dev/nvme0n1p3`
 and its ext4 filesystem still occupied about 100 GiB. CI run number 43 (API run ID 438)
 therefore continued to report 28 GiB available and failed its unchanged 30 GiB preflight.
 Rerunning a failed job retains the same UI run number; its job attempt number increments.
 Read-only probe run number 45 (API run ID 442) confirmed the raw-disk/partition mismatch.
 Its `growpart -N` output showed that partition 3 could extend from 209301471 to
 314159071 sectors while keeping start sector 413696 and its partition UUID unchanged.
 Temporary files and logs were small; Docker/containerd storage and Mathlib were the main
 consumers. No tagged image, build cache or Mathlib cache was deleted for this repair.
 The owner explicitly authorized partition and filesystem expansion in the execution chat.
 Manual maintenance run number 46 (API run ID 443) then backed up the partition table to
 `/root/lean-bench-maintenance/20261028T121919Z/nvme0n1.sfdisk`, expanded partition 3,
 and grew the mounted ext4 filesystem online. The resulting partition is 149.8 GiB;
 `df` reported a 148 GiB filesystem with 75 GiB available. No reboot was required.
 `.gitea/workflows/env-probe.yml` now includes read-only storage and cache diagnostics.
 `.gitea/workflows/runner-storage-maintenance.yml` is manual-only and requires the literal
 confirmation `EXPAND_RUNNER_ROOT`. It validates hostname, root device, ext4 type, partition
 UUID, start sector and disk size, takes a lock, and backs up the partition table before any
 change. Future execution still requires explicit owner authorization for that maintenance.
 It never formats a device or prunes images. The failed image job was retried after expansion;
 its actual build, smoke-test and image-retention outcome is recorded in CI run number 43.
@@ -44,6 +44,9 @@ Labeling must be finished before anyone opens `results.jsonl`.
 - Metadata is stored beside the output as `results.meta.json`. Model, endpoint, temperature,
  input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative.
  A file lock prevents concurrent writers. A budget stop returns exit status 2.
 - Billing/authentication failures stop immediately. Resume retries only missing detector components,
  keeping both complete items and the successful side of partial items. Rows are replaced atomically.
  `--audit-only` reconciles saved completion counts and status without any API request.
 - The nominal successful path uses 130 calls (one source extraction and one judge per item);
  malformed replies and network retries may increase the actual count.
 - Scoring requires complete labels and results and no unresolved detector errors. The primary
@@ -53,15 +56,10 @@ Labeling must be finished before anyone opens `results.jsonl`.
 - Raw passages, labeling HTML and model responses remain in the ignored `data/` directory.
  Only verdicts, abstract annotation notes, hashes and text-free summaries belong in Git.
-## Separate GPT-assisted diagnostic
+## Current execution
-The owner requested a complete 65-item reassessment by the current GPT assistant on
+The 2026-10-28 run was blocked by DashScope `Arrearage`: 42 items are complete, 23 need
-2026-10-28. This is separate from the incomplete Qwen run: no outputs are mixed and
+42 detector components, and 131 of the 400 request reservations have been consumed.
-neither the earlier labels nor Qwen files are overwritten. The assistant had prior
+The owner requested fixes and a report now, with paid resumption deferred.
-exposure to the reference labels and Lean; this is not blind or independent validation.
+See `docs/experiments/P0-execution-2026-10-28.md` and `results/execution.json`.
-No GO/PARTIAL/NO-GO decision is issued.
+No gate decision has been issued. Restore provider billing before resuming the same run.
 See `docs/experiments/P0-gpt-diagnostic.md` for all counts, limitations, artifact locations
 and the offline replay command. The tracked `results/gpt-diagnostic-*.json` files contain
 only categorical/numeric outputs and audit metadata. The authored source structures,
 reasons and full review page stay in the ignored `data/gpt-diagnostic/` directory.
@@ -1,200 +0,0 @@
 """Validate and replay a current-chat assistant review without calling any model.
 Private source schemas and reasons stay in data/. Public summaries contain only
 categories, counts, numeric scores, hashes and an explicit non-independent provenance.
 """
 from __future__ import annotations
 import argparse
 import hashlib
 import html
 import json
 import math
 from collections import Counter
 from pathlib import Path
 from leanbench.align import DEFAULT_THRESHOLD, GOAL_THRESHOLD, align
 from leanbench.evalstats import auc, confusion, wilson
 from leanbench.lint import lint
 from leanbench.project import project
 from leanbench.srcsimplex import parse_source_simplex
 VERDICTS = {"faithful", "minor_drift", "wrong", "not_formalizable"}
 ERRORS = {"missing_hypothesis", "extra_hypothesis", "wrong_type", "quantifier",
          "wrong_conclusion", "degenerate", "hallucinated_api", "other"}
 def digest(path: Path) -> str:
    return hashlib.sha256(path.read_bytes()).hexdigest()
 def finite(value):
    if isinstance(value, dict):
        return {k: finite(v) for k, v in value.items()}
    if isinstance(value, (list, tuple)):
        return [finite(v) for v in value]
    if isinstance(value, float) and not math.isfinite(value):
        return None
    return value
 def unique(rows, field):
    indexed = {row[field]: row for row in rows}
    if len(indexed) != len(rows):
        raise ValueError(f"Duplicate {field}")
    return indexed
 def evaluate(items, key, assessment):
    """Keep model-authored assessments separate from deterministic detector outputs."""
    by_id = unique(items, "id")
    records = unique(assessment["records"], "blind_id")
    if (not key or len(set(key.values())) != len(key) or set(records) != set(key)
            or set(by_id) != set(key.values())):
        raise ValueError("Items, key and assessments must cover the same cohort exactly once")
    output = []
    for blind, item_id in key.items():
        item, record = by_id[item_id], records[blind]
        if record["id"] != item_id or not item.get("source_text", "").strip():
            raise ValueError(f"Missing source text or mismatched item for {blind}")
        judge = record["judge"]
        if (judge.get("verdict") not in VERDICTS or type(judge.get("faithful")) is not bool
                or judge["faithful"] != (judge["verdict"] == "faithful")
                or not isinstance(judge.get("reason"), str) or not judge["reason"].strip()
                or not isinstance(judge.get("errors"), list)
                or not set(judge["errors"]) <= ERRORS):
            raise ValueError(f"Invalid authored judgment for {blind}")
        source = parse_source_simplex(record["source"])
        projection = project(item["lean_code"])
        alignment = align(source, projection)
        output.append({"id": item_id, "blind_id": blind,
                       "source": source.as_dict(), "judge": judge,
                       "projection": projection.as_dict(), "role": alignment.as_dict(),
                       "lint": lint(projection), "compiled": bool(item.get("verified")),
                       "errors": {}})
    return output
 def public_items(rows, labels):
    if set(labels) != {row["blind_id"] for row in rows}:
        raise ValueError("Reference labels must cover the entire cohort")
    out = []
    for row in rows:
        reference = labels[row["blind_id"]]["verdict"]
        if reference not in VERDICTS:
            raise ValueError("Invalid reference verdict")
        out.append({"blind_id": row["blind_id"], "reference_verdict": reference,
                    "assistant_verdict": row["judge"]["verdict"],
                    "assistant_error_types": row["judge"]["errors"],
                    "verdict_agrees": reference == row["judge"]["verdict"],
                    "compiled": row["compiled"], "lint_flagged": bool(row["lint"]),
                    "role_flagged": row["role"]["flagged"],
                    "role_score": row["role"]["score"],
                    "role_conflict_types": row["role"]["errors"],
                    "source_role_count": len(row["source"]["roles"]),
                    "lean_role_count": len(row["projection"]["roles"]),
                    "degenerate_projection": row["projection"]["degenerate"]})
    return out
 def agreement(rows, labels, secondary=False):
    cohort = [r for r in rows if labels[r["blind_id"]]["verdict"] != "not_formalizable"
              and (secondary or labels[r["blind_id"]]["verdict"] != "minor_drift")]
    positives = {"wrong", "minor_drift"} if secondary else {"wrong"}
    target = [labels[r["blind_id"]]["verdict"] in positives for r in cohort]
    out = {}
    for name, flags in {
        "role": [r["role"]["flagged"] for r in cohort],
        "assistant_judge": [not r["judge"]["faithful"] for r in cohort],
        "lint": [bool(r["lint"]) for r in cohort],
        "compile_only": [not r["compiled"] for r in cohort],
    }.items():
        counts = confusion(flags, target)
        out[name] = {**counts.as_dict(), "precision_ci": wilson(counts.tp, counts.tp + counts.fp)}
    out["role"]["auc"] = auc([-r["role"]["score"] for r in cohort], target)
    return {"n": len(cohort), "metrics_are_non_independent_reference_agreement": True,
            "detectors": out}
 def write_review(path, rows, items):
    by_id = {r["id"]: r for r in items}
    sections = []
    for row in rows:
        item = by_id[row["id"]]
        sections.append(
            f'<section id="{html.escape(row["blind_id"])}"><h2>{row["blind_id"]}</h2>'
            f'<h3>Passage</h3><pre>{html.escape(item["source_text"])}</pre>'
            f'<h3>Lean</h3><pre>{html.escape(item["lean_code"])}</pre>'
            f'<h3>Fresh assistant judgment: {row["judge"]["verdict"]}</h3>'
            f'<p>{html.escape(row["judge"]["reason"])}</p>'
            f'<h3>Source roles</h3><pre>{html.escape(json.dumps(row["source"], indent=2, ensure_ascii=False))}</pre>'
            f'<h3>Deterministic alignment</h3><pre>{html.escape(json.dumps(row["role"], indent=2, ensure_ascii=False))}</pre></section>'
        )
    path.write_text('<!doctype html><html lang="en"><meta charset="utf-8">'
                    '<title>P0 GPT-assisted diagnostic</title><style>'
                    'body{font:16px/1.6 system-ui;max-width:1050px;margin:32px auto;padding:0 20px}'
                    'pre{white-space:pre-wrap;overflow-wrap:anywhere;background:#f4f5f6;padding:16px}'
                    'section{border-top:1px solid #ccc;margin:40px 0}</style>'
                    '<h1>P0: 65-item GPT-assisted diagnostic</h1>'
                    '<p>Private review. Same-assistant, non-blind diagnosis; no independent accuracy or gate decision. '
                    'Passages and model-derived descriptions must remain outside Git.</p>'
                    + ''.join(sections) + '</html>', encoding="utf-8")
 def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--items", type=Path, required=True)
    parser.add_argument("--key", type=Path, required=True)
    parser.add_argument("--assessments", type=Path, required=True)
    parser.add_argument("--labels", type=Path, required=True)
    parser.add_argument("--private-out", type=Path, required=True)
    parser.add_argument("--summary", type=Path, required=True)
    parser.add_argument("--public-items", type=Path, required=True)
    args = parser.parse_args()
    if "data" not in args.private_out.parts:
        parser.error("Private output must be under the gitignored data/ directory")
    items = [json.loads(x) for x in args.items.read_text().splitlines() if x.strip()]
    key = json.loads(args.key.read_text())["key"]
    assessment = json.loads(args.assessments.read_text())
    provenance = assessment["provenance"]
    if (provenance["items_sha256"] != digest(args.items)
            or provenance["key_sha256"] != digest(args.key)):
        parser.error("Authored review is bound to different inputs or blind key")
    rows = evaluate(items, key, assessment)
    labels = json.loads(args.labels.read_text())["labels"]
    public = public_items(rows, labels)
    summary = {
        "experiment": "P0-GPT-diagnostic", "status": "complete", "n": len(rows),
        "provenance": provenance, "decision": None,
        "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.",
        "hashes": {"items": digest(args.items), "key": digest(args.key),
                   "assessments": digest(args.assessments), "reference_labels": digest(args.labels),
                   "replay_script": digest(Path(__file__)),
                   **{f"leanbench/{name}.py": digest(Path(__file__).resolve().parents[2] / "leanbench" / f"{name}.py")
                      for name in ("align", "project", "srcsimplex", "lint")}},
        "fixed_thresholds": {"matching": DEFAULT_THRESHOLD, "goal": GOAL_THRESHOLD},
        "verdict_counts": dict(Counter(r["judge"]["verdict"] for r in rows)),
        "role_flagged": sum(r["role"]["flagged"] for r in rows),
        "lint_flagged": sum(bool(r["lint"]) for r in rows),
        "compiled": sum(r["compiled"] for r in rows),
        "degenerate_projection": sum(r["projection"]["degenerate"] for r in rows),
        "exact_verdict_agreement": sum(r["verdict_agrees"] for r in public),
        "changed_verdicts": [r["blind_id"] for r in public if not r["verdict_agrees"]],
        "primary_reference_agreement": agreement(rows, labels),
        "secondary_reference_agreement": agreement(rows, labels, secondary=True),
        "role_flagged_by_new_verdict": {v: {"n": sum(r["judge"]["verdict"] == v for r in rows),
             "flagged": sum(r["judge"]["verdict"] == v and r["role"]["flagged"] for r in rows)}
             for v in sorted(VERDICTS)},
    }
    args.private_out.mkdir(parents=True, exist_ok=True)
    (args.private_out / "results.jsonl").write_text(''.join(json.dumps(r, ensure_ascii=False) + '\n' for r in rows))
    write_review(args.private_out / "review.html", rows, items)
    args.summary.parent.mkdir(parents=True, exist_ok=True)
    args.public_items.parent.mkdir(parents=True, exist_ok=True)
    args.summary.write_text(json.dumps(finite(summary), indent=2, allow_nan=False) + '\n')
    args.public_items.write_text(json.dumps(public, indent=2, allow_nan=False) + '\n')
    print(json.dumps({k: summary[k] for k in ("n", "status", "verdict_counts", "role_flagged", "exact_verdict_agreement", "decision")}))
 if __name__ == "__main__":
    main()
@@ -0,0 +1,71 @@
 {
  "experiment": "P0",
  "status": "provider_blocked",
  "decision": null,
  "decision_withheld_reason": "Incomplete detector outputs after DashScope Arrearage; no GO/PARTIAL/NO-GO is valid.",
  "cohort_size": 65,
  "completed_items": 42,
  "items_with_failures": 23,
  "missing_components": {
    "judge": 22,
    "role": 20
  },
  "request_attempts": 131,
  "max_calls": 400,
  "remaining_request_budget": 269,
  "usage": {
    "calls": 89,
    "prompt_tokens": 37699,
    "completion_tokens": 7790
  },
  "model": "qwen-max",
  "temperature": 0.0,
  "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
  "labels_sha256": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638",
  "results_sha256": "fce402e6eab460a48bb9a8e94140bb23f305843ab46d227bbffa5100d7de69e5",
  "prompt_hashes": {
    "source": "382f9a7b5a0cfb2d50d525f884dc806f45adaa59bcc45e388920c4759db1546f",
    "judge": "7ab92682bd71d78a212471289f0f01db39d6b68f49d44df65d7b1c9e34ebb5e2"
  },
  "labels": {
    "type": "single AI annotator; not human gold",
    "frozen": true,
    "count": 65
  },
  "affected_blind_ids": [
    "P02",
    "P04",
    "P09",
    "P18",
    "P19",
    "P20",
    "P21",
    "P22",
    "P24",
    "P27",
    "P29",
    "P30",
    "P33",
    "P36",
    "P37",
    "P38",
    "P42",
    "P43",
    "P45",
    "P47",
    "P54",
    "P59",
    "P62"
  ],
  "successful_components_preserved": 88,
  "resume_policy": "After owner confirms billing recovery, retry missing components only using the same run files, frozen labels, model, prompts and cumulative 400-request ceiling.",
  "owner_instruction": "2026-10-28: complete fixes and the execution report now; resume paid calls later.",
  "validation": {
    "offline_unit_tests": 149,
    "ruff": "passed",
    "remote_runner_tag": "ubuntu24.04-x64-lean4.35",
    "initial_remote_ci": "https://gitea.entroia.com/Zayden-Jung/lean-bench/actions/runs/427",
    "initial_remote_ci_status": "success; image job skipped for PR",
    "recovery_remote_ci": "See follow-up PR #6 checks for the delivered head revision"
  }
 }
@@ -1,275 +0,0 @@
 {
  "experiment": "P0-GPT-diagnostic",
  "status": "complete",
  "n": 65,
  "provenance": {
    "run_kind": "current-chat assistant-authored diagnostic; not an API benchmark",
    "evaluator": "Codex GPT assistant; exact deployed model identifier unavailable",
    "authored_at": "2026-10-28T11:23:06.275167+00:00",
    "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
    "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
    "reference_labels_seen_in_prior_chat": true,
    "lean_seen_while_authoring_source_roles": true,
    "new_external_api_calls": 0,
    "assistant_token_usage": null,
    "limitations": [
      "Same assistant previously authored the reference labels; agreement is not independent accuracy.",
      "Prior context contains the earlier review and detector code. This is not a blinded source-only extraction or a fresh-model replicate.",
      "All judgments are manually authored in this chat, not responses from a GPT API endpoint.",
      "Semantics are assessed conditionally on recoverable notation. No new Lean compilation or library API audit is performed.",
      "The strict Boolean judge flags all verdicts except faithful, including not_formalizable; four-way verdicts are also retained."
    ]
  },
  "decision": null,
  "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.",
  "hashes": {
    "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
    "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
    "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272",
    "reference_labels": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638",
    "replay_script": "5c02e3d26761ce0b4e38d4be9e65b95bfd8db048c9c7c73edaac17e654e10c0f",
    "leanbench/align.py": "730e44f1158e6e441e4745dff7324e565b89b6e5148017c3fd93f4c69c22c9ce",
    "leanbench/project.py": "8ed76924b463ba418ceb732d0fcb6c572a548d94fe7f23759c67746da24d9430",
    "leanbench/srcsimplex.py": "d10b785299ceb17cadc4e97737eef74183ed390d04b4571a702cd4fd42b069d0",
    "leanbench/lint.py": "4396e879312f370cd70beeffcbd7ffeab8a41ee1704cc1f235dbbcd6e843fd68"
  },
  "fixed_thresholds": {
    "matching": 0.3,
    "goal": 0.2
  },
  "verdict_counts": {
    "faithful": 25,
    "minor_drift": 13,
    "wrong": 24,
    "not_formalizable": 3
  },
  "role_flagged": 55,
  "lint_flagged": 21,
  "compiled": 10,
  "degenerate_projection": 15,
  "exact_verdict_agreement": 59,
  "changed_verdicts": [
    "P02",
    "P18",
    "P23",
    "P34",
    "P51",
    "P57"
  ],
  "primary_reference_agreement": {
    "n": 55,
    "metrics_are_non_independent_reference_agreement": true,
    "detectors": {
      "role": {
        "tp": 25,
        "fp": 21,
        "fn": 0,
        "tn": 9,
        "n": 55,
        "recall": 1.0,
        "precision": 0.5434782608695652,
        "false_flag_rate": 0.7,
        "f1": 0.704225352112676,
        "recall_ci": [
          0.8668035060468213,
          1.0
        ],
        "false_flag_ci": [
          0.5212387898833981,
          0.8333543735604105
        ],
        "precision_ci": [
          0.4017993496608042,
          0.67845489578878
        ],
        "auc": 0.61
      },
      "assistant_judge": {
        "tp": 25,
        "fp": 5,
        "fn": 0,
        "tn": 25,
        "n": 55,
        "recall": 1.0,
        "precision": 0.8333333333333334,
        "false_flag_rate": 0.16666666666666666,
        "f1": 0.9090909090909091,
        "recall_ci": [
          0.8668035060468213,
          1.0
        ],
        "false_flag_ci": [
          0.07336434240351683,
          0.33564705185680177
        ],
        "precision_ci": [
          0.6643529481431982,
          0.9266356575964831
        ]
      },
      "lint": {
        "tp": 12,
        "fp": 5,
        "fn": 13,
        "tn": 25,
        "n": 55,
        "recall": 0.48,
        "precision": 0.7058823529411765,
        "false_flag_rate": 0.16666666666666666,
        "f1": 0.5714285714285713,
        "recall_ci": [
          0.30031003928960015,
          0.6650178204685269
        ],
        "false_flag_ci": [
          0.07336434240351683,
          0.33564705185680177
        ],
        "precision_ci": [
          0.468664666737861,
          0.8672020613444361
        ]
      },
      "compile_only": {
        "tp": 24,
        "fp": 24,
        "fn": 1,
        "tn": 6,
        "n": 55,
        "recall": 0.96,
        "precision": 0.5,
        "false_flag_rate": 0.8,
        "f1": 0.6575342465753424,
        "recall_ci": [
          0.8045552759497747,
          0.9929039496133008
        ],
        "false_flag_ci": [
          0.6269395261897256,
          0.9049502189759876
        ],
        "precision_ci": [
          0.36389098932037767,
          0.6361090106796223
        ]
      }
    }
  },
  "secondary_reference_agreement": {
    "n": 62,
    "metrics_are_non_independent_reference_agreement": true,
    "detectors": {
      "role": {
        "tp": 32,
        "fp": 21,
        "fn": 0,
        "tn": 9,
        "n": 62,
        "recall": 1.0,
        "precision": 0.6037735849056604,
        "false_flag_rate": 0.7,
        "f1": 0.7529411764705882,
        "recall_ci": [
          0.8928172849426366,
          1.0
        ],
        "false_flag_ci": [
          0.5212387898833981,
          0.8333543735604105
        ],
        "precision_ci": [
          0.4694123578888073,
          0.7241078808096105
        ],
        "auc": 0.590625
      },
      "assistant_judge": {
        "tp": 32,
        "fp": 5,
        "fn": 0,
        "tn": 25,
        "n": 62,
        "recall": 1.0,
        "precision": 0.8648648648648649,
        "false_flag_rate": 0.16666666666666666,
        "f1": 0.927536231884058,
        "recall_ci": [
          0.8928172849426366,
          1.0
        ],
        "false_flag_ci": [
          0.07336434240351683,
          0.33564705185680177
        ],
        "precision_ci": [
          0.7202227252929444,
          0.9408679273749238
        ]
      },
      "lint": {
        "tp": 14,
        "fp": 5,
        "fn": 18,
        "tn": 25,
        "n": 62,
        "recall": 0.4375,
        "precision": 0.7368421052631579,
        "false_flag_rate": 0.16666666666666666,
        "f1": 0.5490196078431372,
        "recall_ci": [
          0.2816508596944317,
          0.6067469796877387
        ],
        "false_flag_ci": [
          0.07336434240351683,
          0.33564705185680177
        ],
        "precision_ci": [
          0.5120803155892935,
          0.8819376166045982
        ]
      },
      "compile_only": {
        "tp": 29,
        "fp": 24,
        "fn": 3,
        "tn": 6,
        "n": 62,
        "recall": 0.90625,
        "precision": 0.5471698113207547,
        "false_flag_rate": 0.8,
        "f1": 0.6823529411764705,
        "recall_ci": [
          0.7578150066422116,
          0.9675990373736805
        ],
        "false_flag_ci": [
          0.6269395261897256,
          0.9049502189759876
        ],
        "precision_ci": [
          0.41453742646439184,
          0.6734263183985253
        ]
      }
    }
  },
  "role_flagged_by_new_verdict": {
    "faithful": {
      "n": 25,
      "flagged": 16
    },
    "minor_drift": {
      "n": 13,
      "flagged": 13
    },
    "not_formalizable": {
      "n": 3,
      "flagged": 2
    },
    "wrong": {
      "n": 24,
      "flagged": 24
    }
  }
 }
@@ -50,37 +50,64 @@ def judge(client, passage: str, lean: str) -> dict:
            "reason": str(reply.get("reason", ""))[:300]}
-def run_item(client, item: dict) -> dict:
+def provider_blocked(error: Exception) -> bool:
-    if not item.get("source_text", "").strip():
+    text = str(error).lower()
-        raise ValueError("Missing source_text; use a private source-inclusive export")
+    return any(code in text for code in ("arrearage", "overdue-payment", "invalid_api_key", "http 401", "http 403"))
-    code = item.get("lean_code") or ""
+
-    row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
+
-    proj = project(code)
+def complete_row(row: dict) -> bool:
-    row["projection"] = proj.as_dict()
+    return not row.get("errors") and "role" in row and "judge" in row
-    row["lint"] = lint(proj)
+
-    try:
+
-        src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""),
+class ProviderBlocked(RuntimeError):
-                                                item.get("label", ""))
+    """A billing or authentication failure requires external recovery before resuming."""
-        al = align(src, proj)
+
-        row["source"] = [r.__dict__ for r in src.roles]
+    def __init__(self, row):
-        row["role"] = al.as_dict()
+        super().__init__("Provider billing/authentication blocked; partial results were preserved")
-    except CallBudgetExceeded:
+        self.row = row
        raise
    except Exception as error:  # a failed extraction is data, not a crash
        row["errors"]["role"] = str(error)[:300]
    try:
        row["judge"] = judge(client, item.get("source_text", ""), code)
    except CallBudgetExceeded:
        raise
    except Exception as error:
        row["errors"]["judge"] = str(error)[:300]
    return row
 class CallBudgetExceeded(RuntimeError):
    """Stop before issuing a request that would exceed the cumulative budget."""
 def run_item(client, item: dict, previous: dict | None = None) -> dict:
    if not item.get("source_text", "").strip():
        raise ValueError("Missing source_text; use a private source-inclusive export")
    code = item.get("lean_code") or ""
    row: dict = {**(previous or {}), "id": item["id"], "compiled": bool(item.get("verified"))}
    row["errors"] = dict(row.get("errors", {}))
    proj = project(code)
    row["projection"] = proj.as_dict()
    row["lint"] = lint(proj)
    if "role" not in row:
        try:
            src = srcsimplex.extract_source_simplex(client, item["source_text"], item.get("label", ""))
            al = align(src, proj)
            row["source"] = [r.__dict__ for r in src.roles]
            row["role"] = al.as_dict()
            row["errors"].pop("role", None)
        except CallBudgetExceeded as error:
            error.row = row
            raise
        except Exception as error:
            row["errors"]["role"] = str(error)[:300]
            if provider_blocked(error):
                raise ProviderBlocked(row) from error
    if "judge" not in row:
        try:
            row["judge"] = judge(client, item["source_text"], code)
            row["errors"].pop("judge", None)
        except CallBudgetExceeded as error:
            error.row = row
            raise
        except Exception as error:
            row["errors"]["judge"] = str(error)[:300]
            if provider_blocked(error):
                raise ProviderBlocked(row) from error
    return row
 def digest(path: Path) -> str:
    return hashlib.sha256(path.read_bytes()).hexdigest()
@@ -106,8 +133,9 @@ def execute(args, items, settings) -> int:
    if args.out.exists():
        rows = [json.loads(x) for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()]
    ids = {item["id"] for item in items}
-    done = {row["id"] for row in rows}
+    by_id = {row["id"]: row for row in rows}
-    if len(done) != len(rows) or not done <= ids:
+    done = {row["id"] for row in rows if complete_row(row)}
    if len(by_id) != len(rows) or not set(by_id) <= ids:
        raise ValueError("Results have duplicate or unknown item IDs")
    hashes = {
        "source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(),
@@ -129,11 +157,24 @@ def execute(args, items, settings) -> int:
    elif rows:
        raise ValueError("Cannot resume results without their audit metadata")
    todo = [item for item in items if item["id"] not in done]
    missing = sum(2 - int("role" in by_id.get(i["id"], {}))
                  - int("judge" in by_id.get(i["id"], {})) for i in todo)
    print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
-          f"nominal_calls={len(todo) * 2} request_attempts={meta['request_attempts']} cap={args.max_calls}")
+          f"missing_components={missing} request_attempts={meta['request_attempts']} cap={args.max_calls}")
    print("prompt_hashes:", json.dumps(hashes))
    if args.dry_run:
        return 0
    if getattr(args, "audit_only", False):
        meta["completed_items"] = len(done)
        meta["processed_items"] = len(rows)
        meta["status"] = ("provider_blocked" if any(provider_blocked(RuntimeError(message))
                          for row in rows for message in row.get("errors", {}).values())
                          else "detector_errors" if todo else "complete")
        if args.out.exists():
            meta["results_sha256"] = digest(args.out)
        atomic_json(meta_path, meta)
        print(json.dumps(meta))
        return 0 if meta["status"] == "complete" else 2
    if settings.llm.model != "qwen-max" or settings.llm.temperature != 0:
        raise ValueError("P0 is preregistered for qwen-max at temperature 0")
    client = AuditedClient.from_settings(settings.llm)
@@ -142,6 +183,7 @@ def execute(args, items, settings) -> int:
    def checkpoint():
        meta["usage"] = client.usage.as_dict()
        meta["completed_items"] = len(done)
        meta["processed_items"] = len(by_id)
        atomic_json(meta_path, meta)
    def reserve():
@@ -155,19 +197,30 @@ def execute(args, items, settings) -> int:
    meta["max_calls"] = args.max_calls
    meta["status"] = "running"
    checkpoint()
    def save_row(row):
        by_id[row["id"]] = row
        if complete_row(row):
            done.add(row["id"])
        temporary = args.out.with_suffix(args.out.suffix + ".tmp")
        with temporary.open("w", encoding="utf-8") as stream:
            for item in items:
                if item["id"] in by_id:
                    stream.write(json.dumps(by_id[item["id"]], ensure_ascii=False) + "\n")
            stream.flush()
            os.fsync(stream.fileno())
        os.replace(temporary, args.out)
        checkpoint()
    try:
-        with args.out.open("a", encoding="utf-8") as stream:
+        for item in todo:
-            for item in todo:
+            row = run_item(client, item, by_id.get(item["id"]))
-                row = run_item(client, item)
+            save_row(row)
-                stream.write(json.dumps(row, ensure_ascii=False) + "\n")
+            print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
-                stream.flush()
+        meta["status"] = "complete" if len(done) == len(items) else "detector_errors"
-                os.fsync(stream.fileno())
+    except (CallBudgetExceeded, ProviderBlocked) as error:
-                done.add(item["id"])
+        if getattr(error, "row", None) is not None:
-                checkpoint()
+            save_row(error.row)
-                print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
+        meta["status"] = "provider_blocked" if isinstance(error, ProviderBlocked) else "budget_exhausted"
        meta["status"] = "complete"
    except CallBudgetExceeded as error:
        meta["status"] = "budget_exhausted"
        print(str(error), file=sys.stderr)
    except BaseException:
        meta["status"] = "interrupted"
@@ -186,6 +239,7 @@ def main() -> int:
    ap.add_argument("--out", required=True, type=Path)
    ap.add_argument("--max-calls", type=int, default=400)
    ap.add_argument("--dry-run", action="store_true")
    ap.add_argument("--audit-only", action="store_true", help="Reconcile saved state without making API calls")
    ap.add_argument("--labels", type=Path, help="Frozen labels; their hash is bound to the run")
    args = ap.parse_args()
    if not 1 <= args.max_calls <= 400:
@@ -1,74 +0,0 @@
 """Current-chat review replay is offline, complete and text-free at its public boundary."""
 import copy
 import importlib.util
 from pathlib import Path
 import pytest
 PATH = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/assistant_diagnostic.py"
 SPEC = importlib.util.spec_from_file_location("assistant_diagnostic", PATH)
 DIAG = importlib.util.module_from_spec(SPEC)
 SPEC.loader.exec_module(DIAG)
 ITEM = {"id": "synthetic", "source_text": "Synthetic private prose.",
        "lean_code": "theorem t (n : Nat) : n = n := rfl", "verified": True}
 ASSESSMENT = {"records": [{"id": "synthetic", "blind_id": "P01", "source": {
    "roles": [{"kind": "object", "symbols": ["n"], "description": "Private object wording",
               "keywords": ["natural"]},
              {"kind": "goal", "description": "Private goal wording", "keywords": ["equal"]}],
    "goal_has_exists": False},
    "judge": {"verdict": "faithful", "faithful": True, "errors": [],
              "reason": "Private reviewer explanation"}}]}
 def test_offline_replay_and_text_free_public_output(monkeypatch):
    def no_network(*args, **kwargs):
        raise AssertionError("Replay must not call an API")
    monkeypatch.setattr("urllib.request.urlopen", no_network)
    rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT)
    assert len(rows) == 1 and rows[0]["errors"] == {}
    public = DIAG.public_items(rows, {"P01": {"verdict": "faithful"}})
    assert public[0]["assistant_verdict"] == "faithful"
    assert not any(word in str(public) for word in ["Private", "Synthetic", "explanation"])
    assert all(key not in public[0] for key in ["source", "judge", "reason", "lean_code", "source_text"])
 def test_duplicate_or_missing_assessments_are_rejected():
    assessment = copy.deepcopy(ASSESSMENT)
    assessment["records"] *= 2
    with pytest.raises(ValueError, match="Duplicate"):
        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
    with pytest.raises(ValueError, match="same cohort"):
        DIAG.evaluate([ITEM], {"P01": "synthetic"}, {"records": []})
 def test_mismatched_item_and_missing_source_are_rejected():
    assessment = copy.deepcopy(ASSESSMENT)
    assessment["records"][0]["id"] = "different"
    with pytest.raises(ValueError, match="mismatched"):
        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
    with pytest.raises(ValueError, match="Missing source"):
        DIAG.evaluate([{**ITEM, "source_text": ""}], {"P01": "synthetic"}, ASSESSMENT)
 def test_judge_cannot_disagree_with_its_boolean_flag():
    assessment = copy.deepcopy(ASSESSMENT)
    assessment["records"][0]["judge"]["faithful"] = False
    with pytest.raises(ValueError, match="Invalid authored judgment"):
        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
 def test_invalid_source_schema_is_rejected():
    assessment = copy.deepcopy(ASSESSMENT)
    assessment["records"][0]["source"]["roles"] = []
    with pytest.raises(ValueError, match="goal"):
        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
 def test_agreement_is_explicitly_not_independent_and_has_no_gate():
    rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT)
    result = DIAG.agreement(rows, {"P01": {"verdict": "faithful"}})
    assert result["metrics_are_non_independent_reference_agreement"] is True
    assert "decision" not in result
    assert DIAG.finite(float("nan")) is None
@@ -141,3 +141,82 @@ def test_judge_rejects_string_boolean():
    rp = load("run_pilot")
    with pytest.raises(ValueError, match="unusable judge"):
        rp.judge(ScriptedClient(['{"faithful": "false"}']), "passage", "code")
 def test_partial_resume_keeps_successful_detector_output():
    rp = load("run_pilot")
    row = rp.run_item(Stub(), ITEM)
    expected_role = row["role"]
    row.pop("judge")
    row["errors"]["judge"] = "temporary failure"
    class JudgeOnly:
        calls = 0
        def complete_json(self, messages):
            self.calls += 1
            assert "faithful" in messages[0]["content"]
            return {"faithful": True}
    client = JudgeOnly()
    resumed = rp.run_item(client, ITEM, row)
    assert client.calls == 1
    assert resumed["role"] == expected_role
    assert rp.complete_row(resumed)
    assert row["errors"] == {"judge": "temporary failure"}
 def test_billing_failure_stops_before_next_detector():
    import pytest
    from leanbench.llm import LLMError
    rp = load("run_pilot")
    class Blocked:
        calls = 0
        def complete_json(self, messages):
            self.calls += 1
            raise LLMError("HTTP 400: Arrearage overdue-payment")
    client = Blocked()
    with pytest.raises(rp.ProviderBlocked) as caught:
        rp.run_item(client, ITEM)
    assert client.calls == 1
    assert "role" in caught.value.row["errors"]
    assert "judge" not in caught.value.row["errors"]
 def test_blocked_run_preserves_and_replaces_partial_row(tmp_path, monkeypatch):
    import argparse
    import json
    from leanbench.config import Settings
    rp = load("run_pilot")
    args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl",
                              max_calls=400, dry_run=False)
    args.items.write_text(json.dumps(ITEM) + "\n")
    partial = {"id": "x1", "compiled": True, "role": {"flagged": False},
               "errors": {"judge": "Arrearage"}}
    def blocked(client, item, previous):
        raise rp.ProviderBlocked(partial)
    monkeypatch.setattr(rp, "run_item", blocked)
    assert rp.execute(args, [ITEM], Settings()) == 2
    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
    assert meta["status"] == "provider_blocked"
    assert meta["completed_items"] == 0
    def recover(client, item, previous):
        assert previous["role"] == partial["role"]
        return {**previous, "judge": {"faithful": True}, "errors": {}}
    monkeypatch.setattr(rp, "run_item", recover)
    assert rp.execute(args, [ITEM], Settings()) == 0
    rows = [json.loads(line) for line in args.out.read_text().splitlines()]
    assert len(rows) == 1 and rp.complete_row(rows[0])
    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
    assert meta["completed_items"] == 1 and meta["status"] == "complete"
Author	SHA1	Message	Date
codex-bot	1c265609d5	docs(pilot): link the recovery audit to the follow-up PR ci / python (pull_request) Successful in 13s Details ci / lean (pull_request) Successful in 27s Details ci / image (pull_request) Has been skipped Details	2026-10-28 19:08:30 +08:00
codex-bot	16e49df764	fix(pilot): preserve partial results and stop on provider billing errors ci / python (pull_request) Successful in 17s Details ci / lean (pull_request) Successful in 1m21s Details ci / image (pull_request) Has been skipped Details	2026-10-28 19:04:43 +08:00