Restore recorded configuration when resuming runs

docs/USAGE.md

@@ -439,9 +439,15 @@ uv run tlaps-bench run --mode proof-completion --backend codex --model gpt-5.5 -
 
 The runner skips benchmarks already recorded as `SKIP` or as a genuine `PASS` in that directory (first-attempt or via a continuation round), and reruns the rest.
 
-For PFS, resume must select the same module tasks as the original run. A default run can resume without selection flags only while Current still resolves to the same tasks. To resume an older full-PFS run, supply a task-list file containing its original module IDs. For an explicit task-list run in either mode, pass the same list again.
+For PFS, resume with the saved configuration and task list:
 
-`--dry-run --resume --output-dir DIR` checks the selected cohort against `task-list.json` without starting a run. Full PFS resume also checks `run-manifest.json`: the canonical corpus, execution sources, pinned proof libraries, verification toolchain, execution limits, and persistent-session policy must still match. If the original run used `--session-dir` or the implicit directory from `--keep-container`, retain that session path. Keep the original checkout and inputs when continuing a historical run.
+```bash
+uv run tlaps-bench run --resume --output-dir results/my-pfs-run
+```
+
+Conflicting options are rejected. Reapply `--jobs`, quota limits, and `--keep-container` if needed. For Proof Completion, repeat the original run options.
+
+Use `--dry-run --resume --output-dir DIR` to preview the selection. Keep the original checkout and inputs when resuming.
 
 Inline infra retries are intentionally short: the default `--infra-retries 3` gives the original attempt plus three retries with brief backoff. If a longer provider or network outage leaves `INFRA_ERROR` / `QUOTA_EXHAUSTED` results, rerun later with the same `--output-dir --resume`; those non-genuine results are not skipped.
 

src/evaluator/backends/claude_code.py

@@ -640,18 +640,21 @@ def check_auth(self) -> str | None:
                 return None
             return "claude_code: Bedrock/Mantle selected but no AWS credentials detected"
         # Fast path: env var present.
-        if os.environ.get("ANTHROPIC_API_KEY"):
+        if not self._needs_claude_credentials():
             return None
         # Slow path: probe the CLI with --no-session-persistence so the
         # probe doesn't pollute the user's resume history. This makes one
         # tiny API call but covers OAuth / subscription auth that env-var
         # checks can't see.
+        # Keep this credential-only probe cheap without changing the experiment's
+        # effort or the parent environment (the model preflight checks those).
         try:
             r = subprocess.run(
                 ["claude", "--print", "--no-session-persistence", "--output-format", "text", "ok"],
                 capture_output=True,
                 text=True,
                 timeout=30,
+                env={**os.environ, "CLAUDE_CODE_EFFORT_LEVEL": "low"},
             )
             if r.returncode == 0:
                 return None

src/evaluator/runner.py

@@ -1760,6 +1760,150 @@ def _write_task_list_record(output_dir: str, mode_name: str, task_ids: list[str]
         f.write("\n")
 
 
+def _read_resume_options(output_dir: str) -> tuple[dict[str, object], list[str] | None]:
+    """Recover only recorded CLI inputs; identity validation still runs afterward."""
+
+    def read_record(filename):
+        path = os.path.join(output_dir, filename)
+        try:
+            with open(path, encoding="utf-8") as stream:
+                value = json.load(stream)
+        except FileNotFoundError:
+            return None
+        except (OSError, UnicodeError, json.JSONDecodeError) as exc:
+            raise ValueError(f"cannot read resume record {path!r}: {exc}") from exc
+        if type(value) is not dict:
+            raise ValueError(f"invalid resume record {path!r}: expected an object")
+        return value
+
+    options = {}
+    task_ids = None
+    tasks = read_record(TASK_LIST_RECORD)
+    if tasks is not None:
+        task_ids = tasks.get("tasks")
+        if (
+            set(tasks) != {"mode", "tasks"}
+            or tasks["mode"] not in list_modes()
+            or type(task_ids) is not list
+            or not task_ids
+            or any(type(task_id) is not str or not task_id for task_id in task_ids)
+            or len(set(task_ids)) != len(task_ids)
+        ):
+            raise ValueError(f"invalid recorded task list in {TASK_LIST_RECORD}")
+        options["mode"] = tasks["mode"]
+
+    manifest = read_record(RUN_MANIFEST_RECORD)
+    if manifest is None:
+        return options, task_ids
+    if type(manifest.get("schema_version")) is not int or manifest["schema_version"] != 5:
+        raise ValueError(f"unsupported recorded {RUN_MANIFEST_RECORD} schema; keep the original checkout for this run")
+    if manifest.get("mode") != "proof-from-scratch":
+        raise ValueError(f"invalid recorded mode in {RUN_MANIFEST_RECORD}")
+    if options.get("mode", manifest["mode"]) != manifest["mode"]:
+        raise ValueError("recorded task list and run manifest have different modes")
+    options["mode"] = manifest["mode"]
+    policy = manifest.get("execution_policy")
+    if type(policy) is not dict:
+        raise ValueError("invalid recorded execution policy")
+    for name, types in (
+        ("backend", (str,)),
+        ("model", (str, type(None))),
+        ("reasoning_effort", (str, type(None))),
+        ("max_output_tokens", (int, type(None))),
+        ("timeout", (int,)),
+        ("check_timeout", (int,)),
+        ("infra_retries", (int,)),
+        ("max_continuations", (int,)),
+    ):
+        if name not in policy or type(policy[name]) not in types:
+            raise ValueError(f"invalid recorded execution option {name!r}")
+        value = policy[name]
+        if type(value) is str and not value:
+            raise ValueError(f"empty recorded execution option {name!r}")
+        if type(value) is int and value < (1 if name in {"check_timeout", "max_output_tokens"} else 0):
+            raise ValueError(f"invalid recorded execution option {name!r}")
+        options[name] = value
+    if options["backend"] not in list_backends() or policy.get("environment") not in ("container", "local"):
+        raise ValueError("invalid recorded backend or execution environment")
+    options["no_container"] = policy["environment"] == "local"
+
+    session = policy.get("session")
+    if (
+        type(session) is not dict
+        or type(session.get("persistence")) is not bool
+        or type(session.get("root")) not in {str, type(None)}
+        or session["persistence"] != bool(session["root"])
+        or (session["root"] is not None and not os.path.isabs(session["root"]))
+        or session.get("key_scheme") != SESSION_KEY_SCHEME
+    ):
+        raise ValueError("invalid recorded session policy")
+    options["session_dir"] = session["root"]
+
+    verification = policy.get("verification")
+    if (
+        type(verification) is not dict
+        or verification.get("version") != POLICY_VERSION
+        or type(verification.get("modules")) is not dict
+        or not verification["modules"]
+    ):
+        raise ValueError("invalid recorded verification policy")
+    cpus = set()
+    for value in verification["modules"].values():
+        module_policy = VerificationPolicy.from_dict(value)
+        if module_policy.base_timeout_secs != options["check_timeout"]:
+            raise ValueError("recorded module budget differs from the execution policy")
+        cpus.add(module_policy.cpus)
+    if len(cpus) != 1:
+        raise ValueError("recorded module CPU limits are inconsistent")
+    options["check_cpus"] = cpus.pop()
+    return options, task_ids
+
+
+def _parse_run_args(parser: argparse.ArgumentParser) -> tuple[argparse.Namespace, list[str] | None]:
+    # A sentinel distinguishes omission from explicitly supplying a default
+    # value, including --backend codex, --timeout 28800, and --no-container.
+    names = (
+        "mode",
+        "backend",
+        "model",
+        "reasoning_effort",
+        "max_output_tokens",
+        "timeout",
+        "check_timeout",
+        "check_cpus",
+        "infra_retries",
+        "max_continuations",
+        "no_container",
+        "session_dir",
+    )
+    omitted = object()
+    args = parser.parse_args(namespace=argparse.Namespace(**dict.fromkeys(names, omitted)))
+    recorded_options = {}
+    recorded_tasks = None
+    if args.resume:
+        if not args.output_dir:
+            parser.error("--resume requires --output-dir")
+        try:
+            recorded_options, recorded_tasks = _read_resume_options(args.output_dir)
+        except ValueError as exc:
+            parser.error(str(exc))
+    for name in names:
+        value = getattr(args, name)
+        if value is omitted:
+            setattr(args, name, recorded_options.get(name, parser.get_default(name)))
+        elif name in recorded_options and name != "session_dir" and value != recorded_options[name]:
+            parser.error(
+                f"cannot resume with different --{name.replace('_', '-')}; recorded value is {recorded_options[name]!r}"
+            )
+    if "session_dir" in recorded_options:
+        session_dir = _resolve_session_dir(args.session_dir, args.keep_container, not args.no_container)
+        if session_dir != (recorded_options["session_dir"] or ""):
+            parser.error("cannot resume with a different persistent session directory")
+    if args.filter is not None or args.task_list is not None:
+        recorded_tasks = None
+    return args, recorded_tasks
+
+
 def _update_identity_digest(digest, value: bytes) -> None:
     digest.update(len(value).to_bytes(8, byteorder="big"))
     digest.update(value)
@@ -4080,7 +4224,7 @@ def main():
     parser.add_argument(
         "--resume",
         action="store_true",
-        help="Reuse --output-dir: skip benchmarks already SKIP or genuinely passed there (first-attempt or continuation), run the rest",
+        help="Reuse --output-dir, inherit recorded settings for omitted options, skip benchmarks already SKIP or genuinely passed there, and run the rest",
     )
     parser.add_argument(
         "--min-free-gb",
@@ -4146,7 +4290,7 @@ def main():
         action="store_true",
         help="Continue when public API pricing is unavailable; equivalent_cost_usd will be blank",
     )
-    args = parser.parse_args()
+    args, resume_task_ids = _parse_run_args(parser)
 
     # Container mode is default; --no-container disables it
     use_container = not args.no_container
@@ -4163,7 +4307,11 @@ def main():
     mode = get_mode(args.mode, benchmark_root, checker_binary)
     task_ids = None
     try:
-        if args.filter is not None:
+        if resume_task_ids is not None:
+            task_ids = resume_task_ids
+            benchmark_files = _select_exact_tasks(mode, task_ids)
+            selection_label = f"recorded cohort from {TASK_LIST_RECORD}"
+        elif args.filter is not None:
             if not any(pattern.strip() for pattern in args.filter.split(",")):
                 raise ValueError("--filter requires at least one non-empty pattern")
             benchmark_files = mode.get_benchmark_files(args.filter)

tests/evaluator/test_claude_code_auth.py

@@ -0,0 +1,54 @@
+"""Credential discovery must not inherit expensive experiment effort settings."""
+
+import os
+import subprocess
+from unittest.mock import MagicMock
+
+import pytest
+
+from evaluator.backends.claude_code import ClaudeCodeBackend
+
+
+@pytest.fixture(autouse=True)
+def direct_claude_credentials(monkeypatch):
+    for name in ("CLAUDE_CODE_USE_BEDROCK", "CLAUDE_CODE_USE_MANTLE", "ANTHROPIC_API_KEY", "CLAUDE_CODE_OAUTH_TOKEN"):
+        monkeypatch.delenv(name, raising=False)
+
+
+@pytest.mark.parametrize("name", ["ANTHROPIC_API_KEY", "CLAUDE_CODE_OAUTH_TOKEN"])
+def test_explicit_credentials_skip_host_model_probe(monkeypatch, name):
+    monkeypatch.setenv(name, "test-credential")
+    probe = MagicMock()
+    monkeypatch.setattr(subprocess, "run", probe)
+
+    assert ClaudeCodeBackend().check_auth() is None
+    probe.assert_not_called()
+
+
+def test_cached_credential_probe_overrides_only_its_own_effort(monkeypatch):
+    monkeypatch.setenv("CLAUDE_CODE_EFFORT_LEVEL", "xhigh")
+    probe = MagicMock(return_value=subprocess.CompletedProcess([], 0, "ok", ""))
+    monkeypatch.setattr(subprocess, "run", probe)
+    backend = ClaudeCodeBackend()
+    backend.set_reasoning_effort("max")
+
+    assert backend.check_auth() is None
+    assert probe.call_args.kwargs["env"]["CLAUDE_CODE_EFFORT_LEVEL"] == "low"
+    assert probe.call_args.kwargs["timeout"] == 30
+    assert "--no-session-persistence" in probe.call_args.args[0]
+    assert os.environ["CLAUDE_CODE_EFFORT_LEVEL"] == "xhigh"
+    command = backend.build_command("/workspace", "/results")
+    assert command[command.index("--effort") + 1] == "max"
+
+
+@pytest.mark.parametrize(
+    "outcome,expected",
+    [
+        (subprocess.CompletedProcess([], 1, "", "Invalid bearer token"), "auth probe failed"),
+        (subprocess.TimeoutExpired("claude", 30), "auth probe timed out"),
+    ],
+)
+def test_auth_probe_errors_still_fail(monkeypatch, outcome, expected):
+    probe = MagicMock(**({"side_effect": outcome} if isinstance(outcome, Exception) else {"return_value": outcome}))
+    monkeypatch.setattr(subprocess, "run", probe)
+    assert expected in ClaudeCodeBackend().check_auth()

tests/evaluator/test_problem_sets.py

@@ -179,11 +179,15 @@ def test_default_selection_is_recorded_and_compared_on_resume(pfs_mode, preview_
     runner._write_task_list_record(str(tmp_path), "proof-from-scratch", list(CURRENT))
     arguments = ["run", "--resume", "--output-dir", str(tmp_path), "--dry-run"]
     assert cli.main(arguments) == 0
+    assert set(_selected(capsys.readouterr().out)) == set(CURRENT)
     # An old full-suite run must not silently resume as Current.
     old = list(CURRENT) + ["Walgit/WalgitProof.tla"]
     runner._write_task_list_record(str(tmp_path), "proof-from-scratch", old)
+    assert cli.main(arguments) == 0
+    assert set(_selected(capsys.readouterr().out)) == set(old)
+    # Explicitly requesting Current must still reject a changed cohort.
     with pytest.raises(SystemExit) as exc:
-        cli.main(arguments)
+        cli.main([*arguments, "--task-list", "current"])
     assert exc.value.code == 2
     assert "different task list or mode" in capsys.readouterr().err
     assert json.loads((tmp_path / runner.TASK_LIST_RECORD).read_text())["tasks"] == sorted(old)

tests/evaluator/test_proof_from_scratch_runner.py

@@ -23,6 +23,7 @@
 from evaluator import runner
 from evaluator.backends.agentic import AgenticBackend
 from evaluator.backends.base import BackendCapabilities, SubmissionDisposition, SubmissionPlan
+from evaluator.backends.claude_code import ClaudeCodeBackend
 from evaluator.modes.proof_from_scratch import ProofFromScratch
 
 
@@ -610,3 +611,72 @@ def test_container_proof_from_scratch_uses_image_environment(tmp_path, monkeypat
     assert inspected_images == ["tlaps-bench-base:locked"]
     assert captured_items[0].container_image == "tlaps-bench-base:locked"
     assert captured_items[0].canonical_inputs.proof_library_catalog == _catalog().to_bytes()
+
+
+@pytest.mark.parametrize("changed_sources", [False, True])
+def test_resume_restores_policy_through_dispatch_and_retains_source_gate(tmp_path, monkeypatch, changed_sources):
+    benchmark_root, _suite, task, *_ = _write_fixture(tmp_path)
+    mode = ProofFromScratch(str(benchmark_root), "/checker")
+    backend = ClaudeCodeBackend(model="claude-opus-4-8")
+    backend.set_reasoning_effort("low")
+    policy = VerificationPolicy.create(1200, mode.module_task_spec(str(task)).proof_unit_ids, 4)
+    output = tmp_path / "output"
+    output.mkdir()
+    identity = runner._proof_from_scratch_run_identity(
+        mode,
+        _catalog(),
+        _toolchain(),
+        runner._execution_policy_identity(
+            backend,
+            use_container=True,
+            timeout=0,
+            check_timeout=1200,
+            infra_retries=5,
+            max_continuations=2,
+            session_dir="",
+            verification_policies={MODULE_TASK_ID: policy.as_dict()},
+        ),
+        runner.AgentSkillsSnapshot.capture(backend, runner.SKILLS_DIR),
+    )
+    if changed_sources:
+        identity["execution_source_digest"] = "previous-execution-sources"
+    runner._write_run_manifest(str(output), identity)
+    runner._write_task_list_record(str(output), mode.name, [MODULE_TASK_ID])
+    original_records = {p.name: p.read_bytes() for p in output.iterdir()}
+    items = []
+    model_setup = []
+    monkeypatch.setattr(runner, "get_mode", lambda *args, **kwargs: mode)
+    monkeypatch.setattr(runner, "ensure_image", lambda **kwargs: "test-image")
+    monkeypatch.setattr(runner, "_container_verification_environment", lambda _: (_catalog(), _toolchain()))
+    monkeypatch.setattr(runner, "_run_sany_preflight", lambda **kwargs: None)
+    monkeypatch.setattr(runner, "_confirm_public_pricing", lambda *args, **kwargs: True)
+    monkeypatch.setattr(ClaudeCodeBackend, "check_auth", lambda self: model_setup.append("auth"))
+    monkeypatch.setattr(runner, "_run_preflight", lambda *args: model_setup.append("preflight"))
+    monkeypatch.setattr(runner.quota, "fetch_usage", lambda *args: None)
+    monkeypatch.setattr(runner, "update_summary", lambda *args: None)
+    monkeypatch.setattr(
+        runner,
+        "run_single_benchmark",
+        lambda item: items.append(item) or {"benchmark": MODULE_TASK_ID, "check_verdict": "ERROR", "time_secs": 0},
+    )
+    monkeypatch.setattr(sys, "argv", ["tlaps-bench", "--resume", "--output-dir", str(output)])
+
+    if changed_sources:
+        with pytest.raises(SystemExit, match="2"):
+            runner.main()
+        assert model_setup == []
+        assert items == []
+        assert {p.name: p.read_bytes() for p in output.iterdir()} == original_records
+    else:
+        runner.main()
+        assert model_setup == ["auth", "preflight"]
+        assert len(items) == 1
+        item = items[0]
+        assert item.backend.name == "claude_code"
+        assert item.backend.model == "claude-opus-4-8"
+        assert item.backend.reasoning_effort == "low"
+        assert item.timeout == 0
+        assert item.verification_policy == policy
+        assert item.infra_retries == 5
+        assert item.max_continuations == 2
+        assert (output / runner.RUN_MANIFEST_RECORD).read_bytes() == original_records[runner.RUN_MANIFEST_RECORD]