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

docs/experiments/P0-execution-2026-10-28.md

@@ -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).

docs/experiments/P0-pilot.md

@@ -2,7 +2,22 @@
 
 Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md).
 
-Status: **approved 2026-10-22; labels pending. No detector has been run and no API spend has occurred.**
+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.
+The frozen labels are from one AI annotator, **not human ground truth**. The annotator saw
+the detector implementation and aggregate compile counts before labeling, but did not see
+per-item compiler outcomes or detector outputs. This departs from the original labeling plan;
+any resulting decision is provisional and cannot substitute for an independent human audit.
+Decision thresholds, detector prompts and the concept table remain fixed. Implementation
+repairs before the first paid call restore the complementary-signal PARTIAL rule, exclude
+minor drift from the primary wrong-versus-faithful comparison, enforce the cumulative HTTP
+request budget, and persist run identity and usage. See `experiments/P0-pilot/README.md`.
 Written 2026-10-22. Companion to `docs/research-plan.md` (what and why), `docs/TODO.md` (task list), `docs/acl-2027-bar.md` (bar). Target: ACL 2027 via ARR, deadline 4 Jan 2027 AoE.
 
 ## 1. Decision (approved by the owner on 2026-10-22)

experiments/P0-pilot/README.md

@@ -16,16 +16,50 @@ unfaithful formalizations better than a single LLM judge, compile-only, or stati
 
 ## Steps
 
-    cp runs/p85-110/items.jsonl experiments/P0-pilot/data/items.jsonl
+    # Default exports omit source_text. Restore it from the matching private review.
+    python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \
+        --review runs/p85-110/review.json --out experiments/P0-pilot/data/items.jsonl
     python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
         --out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
     # a person opens data/labelsheet.html, labels all 65 items, downloads labels.json into labels/
     python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
         --out experiments/P0-pilot/data/results.jsonl --dry-run
     python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
-        --out experiments/P0-pilot/data/results.jsonl
+        --out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.json
     python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
         --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json \
         --summary experiments/P0-pilot/results/summary.json
 
 Labeling must be finished before anyone opens `results.jsonl`.
+
+## Execution safeguards
+
+- Every item must have a nonempty source passage. `prepare_items.py` restores passages only
+  when all exported fields match the archived review; the exported cohort and Lean code stay intact.
+- Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant
+  on 2026-10-28. These are **AI labels, not human gold**; see the metadata in `labels/labels.json`.
+- `--max-calls` counts actual HTTP attempts, including transport and JSON retries, cumulatively
+  across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted
+  request may consume a reservation without a known response or token count.
+- 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
+  comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis.
+  The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed
+  by the judge. No threshold, concept table or detector prompt was tuned for these labels.
+- 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.
+
+## Current execution
+
+The 2026-10-28 run was blocked by DashScope `Arrearage`: 42 items are complete, 23 need
+42 detector components, and 131 of the 400 request reservations have been consumed.
+The owner requested fixes and a report now, with paid resumption deferred.
+See `docs/experiments/P0-execution-2026-10-28.md` and `results/execution.json`.
+No gate decision has been issued. Restore provider billing before resuming the same run.

experiments/P0-pilot/labels/labels.json

@@ -0,0 +1,427 @@
+{
+  "labeler": "Codex AI assistant (this chat; exact deployed model identifier unavailable)",
+  "labeler_type": "AI; not human gold",
+  "frozen_at": "2026-10-28T10:42:10.032234+00:00",
+  "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+  "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+  "method": "Single-pass semantic annotation in shuffled blind-ID order; per-item compiler outcomes and detector outputs hidden. Pure syntax/proof defects are ignored when meaning is recoverable. No compiler/API-name audit. Full extracted-span coverage is assessed; unspecified design tasks or unresolved contextual references are not formalizable.",
+  "limitations": [
+    "Single AI annotator; no human adjudication or inter-annotator agreement.",
+    "The annotator reviewed detector implementation and aggregate compilation counts before labeling; only per-item outputs were hidden.",
+    "AI labels replace the originally planned human/Kimi labels by explicit owner instruction in this chat; the original human-ground-truth protocol is therefore not fully satisfied."
+  ],
+  "labels": {
+    "P01": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The field axioms and nontriviality match the stated definition."
+    },
+    "P02": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The whole carrier and identity singleton are the two specified subgroups; API spelling is not assessed."
+    },
+    "P03": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Every integer unit is constrained to the two specified values."
+    },
+    "P04": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Generated subgroup is equated with all integer powers; escaped notation is treated as a syntax defect."
+    },
+    "P05": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Existence of a bijective multiplication-preserving map matches the definition."
+    },
+    "P06": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement gives exactly the inverse-of-product identity; proof validity is not assessed."
+    },
+    "P07": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Only already-assumed prime factors are asserted to exist; no recovery from the totient is specified."
+    },
+    "P08": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both identity preservation and inverse preservation are stated under a multiplicative equivalence."
+    },
+    "P09": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The multiplicative ring carrier does not encode the additive cyclic group, and the second extracted exercise is omitted."
+    },
+    "P10": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both left and right equations have unique solutions."
+    },
+    "P11": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The group cardinality is the exponent, with the correct identity and quantification."
+    },
+    "P12": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The extracted design question provides no formal security or authentication specification for a fidelity comparison."
+    },
+    "P13": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended modular identity is retained, but the integer variable is supplied to a natural-number coprimality predicate."
+    },
+    "P14": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "Only existence of a ring structure is stated; the identity and unit characterization are omitted."
+    },
+    "P15": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Unique solvability in both factors expresses the row and column permutation property."
+    },
+    "P16": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Passing to the product representation preserves the order-divisibility claim; capitalization and namespace errors are not semantic changes."
+    },
+    "P17": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "An independent non-field example in the extracted passage is omitted."
+    },
+    "P18": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The norm-one complex carrier and multiplication describe the specified subgroup; bundling/API validity is not assessed."
+    },
+    "P19": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The natural-valued order convention needs an infinite-order convention absent from the cardinality definition."
+    },
+    "P20": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A single left-identity action on one group element forces equality to the identity."
+    },
+    "P21": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended commutativity equivalence is visible, but the left operation lacks the carrier annotation needed to identify G."
+    },
+    "P22": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two quantified unique-solvability claims express the specified table property."
+    },
+    "P23": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Prime factors, modulus, lcm exponent and coprimality reproduce the extracted claim; no unstated distinctness assumption is introduced."
+    },
+    "P24": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "An arbitrary group satisfying an order condition is not identified with the geometric symmetry group."
+    },
+    "P25": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two declarations cover both cancellation directions."
+    },
+    "P26": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis",
+        "missing_hypothesis"
+      ],
+      "notes": "The inserted divisibility assumption does not express the RSA relationship required by the argument."
+    },
+    "P27": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The isomorphism is asserted for a quotient of the ambient group instead of the stabilizer subgroup."
+    },
+    "P28": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Natural exponent division fails to express a square root, and the homomorphism target does not encode the specified automorphism."
+    },
+    "P29": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A bijective homomorphism supplies the isomorphism assumption and both power assertions are retained."
+    },
+    "P30": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "An unordered finite product is used for an arbitrary semigroup, losing the ordered nonempty product required by the exercise."
+    },
+    "P31": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The isolated instruction refers to an earlier map whose definition is absent; the actual proposition cannot be recovered from this span."
+    },
+    "P32": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The result merely supplies an unspecified ring homomorphism and does not constrain it to evaluation at the matrix parameter."
+    },
+    "P33": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The cardinality assumption and the nonidentity involution conclusion match; the missing instance binder is a compilation defect."
+    },
+    "P34": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The contrasting abelian properties encode the reason these specified groups are not isomorphic."
+    },
+    "P35": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "quantifier"
+      ],
+      "notes": "One fixed-arity function is applied at incompatible arities instead of specifying a coherent family of products."
+    },
+    "P36": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The ring carrier replaces the concrete root-of-unity group, and neither its order nor the specified generator is stated."
+    },
+    "P37": {
+      "verdict": "wrong",
+      "errors": [
+        "degenerate",
+        "wrong_conclusion"
+      ],
+      "notes": "The declaration has no defining expression for the requested subgroup."
+    },
+    "P38": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis"
+      ],
+      "notes": "Nonemptiness is missing, so the empty subset satisfies both closure assumptions."
+    },
+    "P39": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Laurent series replace finite Laurent polynomials, and the requested units are not characterized."
+    },
+    "P40": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The supplied structure body fixes the function to the canonical integer residue map."
+    },
+    "P41": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "The cardinality assertion is restricted to the range where noncommutativity holds, dropping the smaller symmetric groups."
+    },
+    "P42": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "wrong_conclusion"
+      ],
+      "notes": "A necessary closure condition is promoted to sufficiency without inverse closure."
+    },
+    "P43": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Any two groups of the specified size are related by a multiplicative equivalence."
+    },
+    "P44": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The defining field is exactly commutativity of the group operation."
+    },
+    "P45": {
+      "verdict": "wrong",
+      "errors": [
+        "quantifier",
+        "wrong_conclusion"
+      ],
+      "notes": "Literal uniqueness of a carrier/structure replaces uniqueness up to group isomorphism."
+    },
+    "P46": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Univariate polynomials over a product ring replace three-variable real polynomials; the units question is omitted."
+    },
+    "P47": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The integer-span equality captures the generated set, but the equality for opposite generators is not explicitly stated."
+    },
+    "P48": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The one-sided inverse hypothesis gives the specified inverse element."
+    },
+    "P49": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement is exactly involutivity of group inversion."
+    },
+    "P50": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The custom structure supplies additive commutative group, associative multiplication and both distributive laws without imposing a unit."
+    },
+    "P51": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The carrier, multiplication and identity encode the specified finite group; existence of the chosen API is not audited."
+    },
+    "P52": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Ring structure and unit-to-constant direction are present, but identity characterization is replaced by reflexivity."
+    },
+    "P53": {
+      "verdict": "minor_drift",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "Cardinality is represented only for finite groups although the definition is not restricted to them."
+    },
+    "P54": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "Multiplicative subgroup closure of a residue is used in place of the additive cyclic subgroup generated by it."
+    },
+    "P55": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The abelian-property equivalence is stated under an isomorphism."
+    },
+    "P56": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The design question does not specify an authenticity predicate or formal adversarial model."
+    },
+    "P57": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The homomorphism criterion is retained but the separate isomorphism definition is absent."
+    },
+    "P58": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "A multiplicative equivalence on the full residue ring does not represent the additive cyclic group in the comparison."
+    },
+    "P59": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The inherited-group criterion is recognizable, but operations on the subset are not specified as restricted operations."
+    },
+    "P60": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "missing_hypothesis"
+      ],
+      "notes": "Global bijections with local differentiability conditions do not specify self-diffeomorphisms of the open subset."
+    },
+    "P61": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The homeomorphism type supplies the intended carrier and group structure under composition; notation validity is not assessed."
+    },
+    "P62": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both least-positive exponent and the bounded-power description are retained, ignoring set-minimum API syntax."
+    },
+    "P63": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both two-sided identity hypotheses and their equality are stated."
+    },
+    "P64": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "extra_hypothesis"
+      ],
+      "notes": "The exponent relation uses the ciphertext modulus where the RSA exponent modulus is required."
+    },
+    "P65": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The arbitrary finite group is unrelated to the requested geometric symmetries, with the classification left in a comment."
+    }
+  }
+}

experiments/P0-pilot/make_sheet.py

@@ -154,6 +154,10 @@ def main() -> int:
 
     items = [json.loads(line) for line in args.items.read_text(encoding="utf-8").splitlines()
              if line.strip()]
+    if not items or any(not item.get("source_text", "").strip() for item in items):
+        parser.error("Every item needs nonempty source_text; use a private source-inclusive export.")
+    if len({item["id"] for item in items}) != len(items):
+        parser.error("Item IDs must be unique.")
     order = list(range(len(items)))
     random.Random(args.seed).shuffle(order)
     blind_ids = [f"P{n:02d}" for n in range(1, len(items) + 1)]

experiments/P0-pilot/prepare_items.py

@@ -0,0 +1,45 @@
+"""Restore source passages from a private archived review without changing the cohort."""
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+
+
+def restore(items: list[dict], review: dict) -> list[dict]:
+    archived = review["items"]
+    by_id = {row["id"]: row for row in archived}
+    if len(by_id) != len(archived) or len({row["id"] for row in items}) != len(items):
+        raise ValueError("Duplicate item IDs")
+    restored = []
+    for item in items:
+        original = by_id[item["id"]]
+        comparable = dict(original)
+        if isinstance(comparable.get("imports"), str):
+            comparable["imports"] = json.loads(comparable["imports"])
+        if any(comparable.get(k) != v for k, v in item.items()):
+            raise ValueError(f"Archived review does not match item {item['id']}")
+        passage = original.get("source_text", "")
+        if not passage.strip():
+            raise ValueError(f"Missing archived passage for {item['id']}")
+        restored.append({**item, "source_text": passage})
+    return restored
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--items", required=True, type=Path)
+    parser.add_argument("--review", required=True, type=Path)
+    parser.add_argument("--out", required=True, type=Path)
+    args = parser.parse_args()
+    if args.out.parent.name != "data":
+        parser.error("Source-inclusive output must go in a gitignored data/ directory")
+    items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()]
+    rows = restore(items, json.loads(args.review.read_text()))
+    args.out.parent.mkdir(parents=True, exist_ok=True)
+    args.out.write_text("".join(json.dumps(row, ensure_ascii=False) + "\n" for row in rows))
+    print(f"Restored {len(rows)} passages; all exported fields are unchanged")
+
+
+if __name__ == "__main__":
+    main()

experiments/P0-pilot/results/execution.json

@@ -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"
+  }
+}

experiments/P0-pilot/run_pilot.py

@@ -15,8 +15,11 @@ Hard stops: --max-calls bounds API calls; a rerun skips items already in --out.
 from __future__ import annotations
 
 import argparse
+import fcntl
 import hashlib
+import inspect
 import json
+import os
 import sys
 from pathlib import Path
 
@@ -24,7 +27,7 @@ from leanbench import srcsimplex
 from leanbench.align import align
 from leanbench.config import Settings
 from leanbench.lint import lint
-from leanbench.llm import OpenAICompatibleClient
+from leanbench.llm import OpenAICompatibleClient, Usage
 from leanbench.project import project
 
 JUDGE_PROMPT_VERSION = "judge-v1"
@@ -41,69 +44,228 @@ def judge(client, passage: str, lean: str) -> dict:
         {"role": "system", "content": JUDGE_SYSTEM},
         {"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"},
     ])
-    if not isinstance(reply, dict) or "faithful" not in reply:
+    if not isinstance(reply, dict) or type(reply.get("faithful")) is not bool:
         raise ValueError(f"unusable judge reply: {str(reply)[:200]}")
-    return {"faithful": bool(reply["faithful"]), "confidence": reply.get("confidence"),
+    return {"faithful": reply["faithful"], "confidence": reply.get("confidence"),
             "reason": str(reply.get("reason", ""))[:300]}
 
 
-def run_item(client, item: dict) -> dict:
+def provider_blocked(error: Exception) -> bool:
+    text = str(error).lower()
+    return any(code in text for code in ("arrearage", "overdue-payment", "invalid_api_key", "http 401", "http 403"))
+
+
+def complete_row(row: dict) -> bool:
+    return not row.get("errors") and "role" in row and "judge" in row
+
+
+class ProviderBlocked(RuntimeError):
+    """A billing or authentication failure requires external recovery before resuming."""
+
+    def __init__(self, row):
+        super().__init__("Provider billing/authentication blocked; partial results were preserved")
+        self.row = 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 = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
+    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)
-    try:
+    if "role" not in row:
-        src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""),
+        try:
-                                                item.get("label", ""))
+            src = srcsimplex.extract_source_simplex(client, item["source_text"], item.get("label", ""))
-        al = align(src, proj)
+            al = align(src, proj)
-        row["source"] = [r.__dict__ for r in src.roles]
+            row["source"] = [r.__dict__ for r in src.roles]
-        row["role"] = al.as_dict()
+            row["role"] = al.as_dict()
-    except Exception as error:  # a failed extraction is data, not a crash
+            row["errors"].pop("role", None)
-        row["errors"]["role"] = str(error)[:300]
+        except CallBudgetExceeded as error:
-    try:
+            error.row = row
-        row["judge"] = judge(client, item.get("source_text", ""), code)
+            raise
-    except Exception as error:
+        except Exception as error:
-        row["errors"]["judge"] = str(error)[:300]
+            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()
+
+
+def atomic_json(path: Path, value: dict) -> None:
+    temporary = path.with_suffix(path.suffix + ".tmp")
+    temporary.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n", encoding="utf-8")
+    os.replace(temporary, path)
+
+
+class AuditedClient(OpenAICompatibleClient):
+    """Persist reservations before HTTP requests, including transport and JSON retries."""
+
+    def complete(self, *args, **kwargs):
+        try:
+            return super().complete(*args, **kwargs)
+        finally:
+            self.checkpoint()
+
+
+def execute(args, items, settings) -> int:
+    rows = []
+    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}
+    by_id = {row["id"]: row for row in rows}
+    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(),
+        "judge": hashlib.sha256(JUDGE_SYSTEM.encode()).hexdigest(),
+    }
+    identity = {"model": settings.llm.model, "base_url": settings.llm.base_url,
+                "temperature": settings.llm.temperature, "items_sha256": digest(args.items),
+                "prompt_hashes": hashes,
+                "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
+    labels = getattr(args, "labels", None)
+    if labels is not None:
+        identity["labels_sha256"] = digest(labels)
+    meta_path = args.out.with_suffix(".meta.json")
+    meta = {**identity, "request_attempts": 0, "usage": Usage().as_dict(), "status": "ready"}
+    if meta_path.exists():
+        meta = json.loads(meta_path.read_text(encoding="utf-8"))
+        if any(meta.get(k) != v for k, v in identity.items()):
+            raise ValueError("Run identity changed; use a new output path instead of mixing runs")
+    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"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)
+    client.usage = Usage(**meta["usage"])
+
+    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():
+        if meta["request_attempts"] >= args.max_calls:
+            raise CallBudgetExceeded("Cumulative request cap reached; no further HTTP request was sent")
+        meta["request_attempts"] += 1
+        checkpoint()
+
+    client.checkpoint = checkpoint
+    client.request_guard = reserve
+    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:
+        for item in todo:
+            row = run_item(client, item, by_id.get(item["id"]))
+            save_row(row)
+            print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
+        meta["status"] = "complete" if len(done) == len(items) else "detector_errors"
+    except (CallBudgetExceeded, ProviderBlocked) as error:
+        if getattr(error, "row", None) is not None:
+            save_row(error.row)
+        meta["status"] = "provider_blocked" if isinstance(error, ProviderBlocked) else "budget_exhausted"
+        print(str(error), file=sys.stderr)
+    except BaseException:
+        meta["status"] = "interrupted"
+        raise
+    finally:
+        if args.out.exists():
+            meta["results_sha256"] = digest(args.out)
+        checkpoint()
+    print(json.dumps(meta))
+    return 0 if meta["status"] == "complete" else 2
+
+
 def main() -> int:
     ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
     ap.add_argument("--items", required=True, type=Path)
     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:
+        ap.error("P0 requires a request cap between 1 and 400")
     items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()]
-    done = set()
+    if not items or len({item["id"] for item in items}) != len(items):
-    if args.out.exists():
+        ap.error("Input must contain unique item IDs")
-        done = {json.loads(x)["id"] for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()}
+    if any(not item.get("source_text", "").strip() for item in items):
-    todo = [i for i in items if i["id"] not in done]
+        ap.error("Every item needs nonempty source_text; use a private source-inclusive export")
-    settings = Settings.from_env()
+    if not args.dry_run and args.labels is None:
-    est = len(todo) * 3  # extract (<=2 tries) + judge
+        ap.error("Freeze all blind labels first, then pass --labels")
-    print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
+    if args.labels is not None:
-          f"est_calls<={est} (extract x2 + judge) cap={args.max_calls}")
+        annotation = json.loads(args.labels.read_text(encoding="utf-8"))
-    print("prompts:", srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION,
+        key_path = args.labels.with_name("key.json")
-          hashlib.sha256((srcsimplex.SYSTEM_PROMPT + JUDGE_SYSTEM).encode()).hexdigest()[:12])
+        key = json.loads(key_path.read_text(encoding="utf-8"))["key"]
-    if args.dry_run:
+        verdicts = {"faithful", "minor_drift", "wrong", "not_formalizable"}
-        return 0
+        if (set(key.values()) != {item["id"] for item in items}
-
+                or set(annotation["labels"]) != set(key)
-    client = OpenAICompatibleClient.from_settings(settings.llm)
+                or any(row.get("verdict") not in verdicts for row in annotation["labels"].values())
+                or annotation.get("items_sha256") != digest(args.items)
+                or annotation.get("key_sha256") != digest(key_path)):
+            ap.error("Frozen labels, key and source-inclusive items must be complete and match")
     args.out.parent.mkdir(parents=True, exist_ok=True)
-    with args.out.open("a", encoding="utf-8") as fh:
+    with args.out.with_suffix(args.out.suffix + ".lock").open("w") as lock:
-        for item in todo:
+        fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB)
-            if client.usage.calls >= args.max_calls:
+        return execute(args, items, Settings.from_env())
-                print("call cap reached; rerun to resume", file=sys.stderr)
-                break
-            fh.write(json.dumps(run_item(client, item), ensure_ascii=False) + "\n")
-            fh.flush()
-    meta = {"model": settings.llm.model, "usage": client.usage.as_dict(),
-            "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
-    (args.out.parent / "run_meta.json").write_text(json.dumps(meta, indent=2), encoding="utf-8")
-    print(json.dumps(meta))
-    return 0
 
 
 if __name__ == "__main__":

experiments/P0-pilot/score.py

@@ -1,9 +1,9 @@
-"""Score the pilot: detectors vs. the blind human labels, with the pre-registered decision.
+"""Score the pilot against frozen blind labels using the pre-registered decision.
 
     python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
         --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json --summary experiments/P0-pilot/results/summary.json
 
-Positive class = unfaithful. Primary: verdict == "wrong", over ALL labeled items (role alignment and
+Positive class = unfaithful. Primary: wrong versus faithful, excluding minor drift (role alignment and
 the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to
 decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported
 with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before
@@ -19,22 +19,35 @@ With ~65 items every number carries a wide Wilson interval; the pilot checks for
 from __future__ import annotations
 
 import argparse
+import hashlib
 import json
+import math
 from pathlib import Path
 
-from leanbench.evalstats import auc, confusion
+from leanbench.evalstats import auc, confusion, wilson
 
 
 def load(args):
-    results = {json.loads(x)["id"]: json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()}
+    result_rows = [json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()]
+    results = {row["id"]: row for row in result_rows}
     labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"]
     key = json.loads(args.key.read_text(encoding="utf-8"))["key"]
+    if not key or len(set(key.values())) != len(key):
+        raise ValueError("The blind key must contain unique item IDs")
+    if len(results) != len(result_rows) or set(results) != set(key.values()):
+        raise ValueError("Results must cover every keyed item exactly once")
+    if set(labels) != set(key):
+        raise ValueError("Labels must cover every blind ID exactly once")
     rows = []
     for blind, item_id in key.items():
         lab = labels.get(blind) or {}
-        if item_id in results and lab.get("verdict"):
+        if lab.get("verdict") not in {"faithful", "minor_drift", "wrong", "not_formalizable"}:
-            rows.append({**results[item_id], "blind": blind, "verdict": lab["verdict"],
+            raise ValueError(f"Missing or invalid verdict for {blind}")
-                         "human_errors": lab.get("errors", [])})
+        row = results[item_id]
+        if row.get("errors") or "judge" not in row or "role" not in row:
+            raise ValueError(f"Unresolved detector failure for {blind}; no decision can be issued")
+        rows.append({**row, "blind": blind, "verdict": lab["verdict"],
+                     "human_errors": lab.get("errors", [])})
     return rows
 
 
@@ -51,19 +64,24 @@ def report(rows, positive):
     out = {}
     for name in ("compile_only", "lint", "role", "judge"):
         out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict()
+        out[name]["precision_ci"] = wilson(out[name]["tp"], out[name]["tp"] + out[name]["fp"])
     out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows],
                                    [positive(r) for r in rows])
+    out["role"]["complementary_wrong"] = sum(
+        positive(r) and flags(r)["role"] and not flags(r)["judge"] for r in rows
+    )
     return out
 
 
 def decide(sub):
     role, judge = sub["role"], sub["judge"]
-    if role["tp"] + role["fn"] == 0:
+    if role["tp"] + role["fn"] == 0 or role["fp"] + role["tn"] == 0:
-        return "INSUFFICIENT: no wrong items in the labels"
+        return "INSUFFICIENT: both wrong and faithful items are required"
     go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2
           and role["recall"] >= judge["recall"] + 0.10
           and role["false_flag_rate"] <= judge["false_flag_rate"])
-    partial = (role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
+    partial = ((role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
+               or role.get("complementary_wrong", 0) >= 3)
     return "GO" if go else "PARTIAL" if partial else "NO-GO"
 
 
@@ -75,19 +93,51 @@ def main() -> int:
     ap.add_argument("--summary", type=Path, default=None,
                     help="also write the (text-free) summary here, e.g. results/summary.json")
     args = ap.parse_args()
-    rows = [r for r in load(args) if r["verdict"] != "not_formalizable"]
+    meta = json.loads(args.results.with_suffix(".meta.json").read_text(encoding="utf-8"))
-    compiled = [r for r in rows if r["compiled"]]
+    if (meta.get("status") != "complete"
+            or meta.get("labels_sha256") != hashlib.sha256(args.labels.read_bytes()).hexdigest()
+            or meta.get("results_sha256") != hashlib.sha256(args.results.read_bytes()).hexdigest()):
+        ap.error("Scoring requires a complete run with unchanged frozen labels and results")
+    all_rows = load(args)
+    rows = [r for r in all_rows if r["verdict"] != "not_formalizable"]
+    primary = [r for r in rows if r["verdict"] != "minor_drift"]
+    compiled = [r for r in primary if r["compiled"]]
     summary = {
-        "n_labeled": len(rows), "n_compiled": len(compiled),
+        "run_metadata": meta,
+        "n_labeled": len(all_rows), "n_evaluable": len(rows), "n_primary": len(primary),
+        "n_compiled": len(compiled),
         "verdicts": {v: sum(r["verdict"] == v for r in rows) for v in
-                     ("faithful", "minor_drift", "wrong")},
+                     ("faithful", "minor_drift", "wrong", "not_formalizable")},
         "compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled),
-        "primary_all": report(rows, lambda r: r["verdict"] == "wrong"),
+        "primary_all": report(primary, lambda r: r["verdict"] == "wrong"),
         "secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")),
         "compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
     }
+    summary["verdicts"]["not_formalizable"] = len(all_rows) - len(rows)
+    summary["role_recall_by_error"] = {
+        error: {"flagged": sum(flags(r)["role"] for r in rows
+                                if r["verdict"] == "wrong" and error in r["human_errors"]),
+                "total": sum(r["verdict"] == "wrong" and error in r["human_errors"] for r in rows)}
+        for error in sorted({e for r in rows for e in r["human_errors"]})
+    }
+    summary["degenerate_projection"] = {
+        "total": sum(bool(r.get("projection", {}).get("degenerate")) for r in all_rows),
+        "wrong": sum(r["verdict"] == "wrong" and bool(r.get("projection", {}).get("degenerate"))
+                     for r in all_rows),
+    }
+    summary["disagreements"] = [
+        {"blind": r["blind"], "verdict": r["verdict"], "flags": flags(r)}
+        for r in primary if any(f != (r["verdict"] == "wrong") for f in flags(r).values())
+    ]
     summary["decision"] = decide(summary["primary_all"])
-    text = json.dumps(summary, indent=2, default=str)
+    def finite_json(value):
+        if isinstance(value, dict):
+            return {k: finite_json(v) for k, v in value.items()}
+        if isinstance(value, (list, tuple)):
+            return [finite_json(v) for v in value]
+        return None if isinstance(value, float) and not math.isfinite(value) else value
+
+    text = json.dumps(finite_json(summary), indent=2, allow_nan=False)
     if args.summary:
         args.summary.parent.mkdir(parents=True, exist_ok=True)
         args.summary.write_text(text + "\n", encoding="utf-8")

leanbench/llm.py

@@ -14,7 +14,7 @@ import re
 import time
 import urllib.error
 import urllib.request
-from collections.abc import Iterable
+from collections.abc import Callable, Iterable
 from dataclasses import dataclass, field
 from typing import Any, Protocol
 
@@ -66,6 +66,7 @@ class OpenAICompatibleClient:
     max_retries: int = 4
     temperature: float = 0.0
     usage: Usage = field(default_factory=Usage)
+    request_guard: Callable[[], None] | None = field(default=None, repr=False)
 
     @classmethod
     def from_settings(cls, settings: LLMSettings) -> OpenAICompatibleClient:
@@ -97,6 +98,8 @@ class OpenAICompatibleClient:
         }
         last: Exception | None = None
         for attempt in range(self.max_retries + 1):
+            if self.request_guard is not None:
+                self.request_guard()
             request = urllib.request.Request(url, data=body, headers=headers, method="POST")
             try:
                 with urllib.request.urlopen(request, timeout=self.timeout) as response:

tests/test_pilot_scripts.py

@@ -36,3 +36,187 @@ def test_run_item_and_score(tmp_path):
     out = sc.report(rows, lambda r: r["verdict"] == "wrong")
     assert out["judge"]["n"] == 4
     assert sc.decide(out) in {"GO", "PARTIAL", "NO-GO"}
+
+
+def test_complementary_signal_is_partial():
+    sc = load("score")
+    rows = [
+        {"compiled": True, "lint": [], "role": {"flagged": i < 3, "score": 0.1},
+         "judge": {"faithful": False if 3 <= i < 8 else True}, "verdict": "wrong"}
+        for i in range(10)
+    ] + [
+        {"compiled": True, "lint": [], "role": {"flagged": False, "score": 1},
+         "judge": {"faithful": True}, "verdict": "faithful"}
+    ]
+    summary = sc.report(rows, lambda row: row["verdict"] == "wrong")
+    assert summary["role"]["recall"] == 0.3
+    assert summary["role"]["complementary_wrong"] == 3
+    assert sc.decide(summary) == "PARTIAL"
+
+
+def test_score_rejects_missing_labels_and_detector_failures(tmp_path):
+    import argparse
+    import json
+
+    import pytest
+
+    sc = load("score")
+    args = argparse.Namespace(results=tmp_path / "results.jsonl", labels=tmp_path / "labels.json",
+                              key=tmp_path / "key.json")
+    args.key.write_text(json.dumps({"key": {"P01": "x1"}}))
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": None}}}))
+    args.results.write_text(json.dumps({"id": "x1"}) + "\n")
+    with pytest.raises(ValueError, match="verdict"):
+        sc.load(args)
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": "wrong"}}}))
+    with pytest.raises(ValueError, match="detector failure"):
+        sc.load(args)
+    args.results.write_text("")
+    with pytest.raises(ValueError, match="every keyed item"):
+        sc.load(args)
+
+
+def test_request_budget_survives_resume_and_transport_retries(tmp_path, monkeypatch):
+    import argparse
+    import json
+    import urllib.error
+
+    import pytest
+
+    from leanbench.config import Settings
+
+    rp = load("run_pilot")
+    args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl",
+                              max_calls=2, dry_run=False)
+    args.items.write_text(json.dumps(ITEM) + "\n")
+    monkeypatch.setenv("DASHSCOPE_API_KEY", "test-only")
+    settings = Settings()
+    settings.llm.max_retries = 5
+    requests = []
+
+    def fail(*args, **kwargs):
+        requests.append(1)
+        raise urllib.error.URLError("offline test")
+
+    monkeypatch.setattr("urllib.request.urlopen", fail)
+    monkeypatch.setattr("leanbench.llm.time.sleep", lambda *_: None)
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
+    assert meta["request_attempts"] == 2
+    assert len(meta["prompt_hashes"]["judge"]) == 64
+    assert meta["status"] == "budget_exhausted"
+    settings.llm.model = "other-model"
+    with pytest.raises(ValueError, match="identity changed"):
+        rp.execute(args, [ITEM], settings)
+
+
+def test_run_rejects_missing_source_passage():
+    import pytest
+
+    rp = load("run_pilot")
+    with pytest.raises(ValueError, match="Missing source_text"):
+        rp.run_item(Stub(), {**ITEM, "source_text": ""})
+
+
+def test_restore_passages_checks_cohort_and_normalizes_archived_imports():
+    import pytest
+
+    prepare = load("prepare_items")
+    item = {"id": "x", "lean_code": "example : True := trivial", "imports": ["Mathlib"]}
+    original = {**item, "imports": '["Mathlib"]', "source_text": "A private passage."}
+    restored = prepare.restore([item], {"items": [original]})
+    assert restored == [{**item, "source_text": "A private passage."}]
+    with pytest.raises(ValueError, match="does not match"):
+        prepare.restore([{**item, "lean_code": "changed"}], {"items": [original]})
+
+
+def test_judge_rejects_string_boolean():
+    import pytest
+
+    from leanbench.llm import ScriptedClient
+
+    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"