Defer oversized Strategy replans without stopping proof

autoresearch/prefill/program.md

@@ -49,6 +49,10 @@ Normal iterations use the deterministic host candidate and do not call the
 Strategy model. Invoke Strategy Gemma only after three consecutive
 non-progressing runs, after a falsified branch, or via an explicit CLI/trigger
 file request.
+If an optional Strategy replan exceeds its lossless Prefill budget, defer the
+replan and continue immediately with the deterministic host candidate. Never
+truncate the Strategy prompt and never stop the GAN proof loop for this
+control-plane admission failure.
 An unresolved Critic verdict must isolate one strictly smaller missing lemma;
 the host records that lemma as a deduplicated child obligation. Completed GAN
 runs, transcripts, checkpoints, and ledger updates remain durable even when the

autoresearch/prefill/supervisor.py

@@ -32,6 +32,16 @@
 )
 
 
+class StrategyPrefillBudgetExceeded(ValueError):
+    def __init__(self, token_count: int, max_tokens: int) -> None:
+        self.token_count = int(token_count)
+        self.max_tokens = int(max_tokens)
+        super().__init__(
+            "Strategy Prefill token budget exceeded without truncation: "
+            f"{self.token_count} > {self.max_tokens}",
+        )
+
+
 def _json_request(url: str) -> dict:
     with urllib.request.urlopen(url, timeout=10) as response:
         return json.load(response)
@@ -659,9 +669,9 @@ def propose_candidate(
         enable_thinking=False,
     )
     if len(ids) > max_prefill_tokens:
-        raise ValueError(
-            "Strategy Prefill token budget exceeded without truncation: "
-            f"{len(ids)} > {max_prefill_tokens}",
+        raise StrategyPrefillBudgetExceeded(
+            len(ids),
+            max_prefill_tokens,
         )
     generated: list[int] = []
     print(
@@ -1072,25 +1082,36 @@ def run_iteration(args, iteration: int) -> dict:
                 f"mode=gemma trigger={trigger_reason}",
                 flush=True,
             )
-            proposed = propose_candidate(
-                address=args.address,
-                tokenizer_id=args.tokenizer_id,
-                program=program,
-                current=current,
-                results_text=(
-                    results_path.read_text() if results_path.exists() else ""
-                ),
-                ledger=ledger_data,
-                max_prefill_tokens=args.strategy_max_prefill_tokens,
-            )
-            if proposed["target_obligation_id"] not in _pending_leaf_ids(
-                ledger_data,
-            ):
-                raise ValueError(
-                    "strategy agent targeted a non-leaf proof obligation",
+            try:
+                proposed = propose_candidate(
+                    address=args.address,
+                    tokenizer_id=args.tokenizer_id,
+                    program=program,
+                    current=current,
+                    results_text=(
+                        results_path.read_text()
+                        if results_path.exists() else ""
+                    ),
+                    ledger=ledger_data,
+                    max_prefill_tokens=args.strategy_max_prefill_tokens,
+                )
+                if proposed["target_obligation_id"] not in _pending_leaf_ids(
+                    ledger_data,
+                ):
+                    raise ValueError(
+                        "strategy agent targeted a non-leaf proof obligation",
+                    )
+                if trigger_reason == "manual-trigger-file":
+                    trigger_file.unlink(missing_ok=True)
+            except StrategyPrefillBudgetExceeded as exc:
+                strategy_mode = "host_strategy_deferred"
+                proposed = build_host_candidate(current, ledger_data)
+                print(
+                    "[autoresearch] phase=strategy-deferred-budget "
+                    f"tokens={exc.token_count} max={exc.max_tokens} "
+                    f"fallback=deterministic-host",
+                    flush=True,
                 )
-            if trigger_reason == "manual-trigger-file":
-                trigger_file.unlink(missing_ok=True)
         else:
             strategy_mode = "host"
             proposed = build_host_candidate(current, ledger_data)

tests/inference_engine/bench/test_autoresearch_supervisor.py

@@ -10,6 +10,7 @@
     render_candidate,
     should_keep,
     StrategyPrefillHeartbeat,
+    StrategyPrefillBudgetExceeded,
     strategy_trigger_reason,
     _extract_json,
     _pending_leaf_ids,
@@ -397,6 +398,13 @@ def test_strategy_is_triggered_only_by_events(tmp_path):
     ) == "manual-trigger-file"
 
 
+def test_strategy_budget_error_preserves_exact_admission_counts():
+    error = StrategyPrefillBudgetExceeded(11935, 8448)
+    assert error.token_count == 11935
+    assert error.max_tokens == 8448
+    assert "without truncation: 11935 > 8448" in str(error)
+
+
 def test_strategy_state_keeps_complete_active_ancestry_only():
     ledger = {"obligations": [
         {
@@ -585,6 +593,8 @@ def test_supervisor_preserves_runtime_and_cache_across_iterations():
     assert "phase=runtime-health-check" in body
     assert "phase=deterministic-candidate" in body
     assert "mode=gemma trigger=" in body
+    assert "except StrategyPrefillBudgetExceeded" in body
+    assert "phase=strategy-deferred-budget" in body
     assert "if not gan_completed:" in body
     assert "phase=completed-run-preserved" in body
     assert "deploy_candidate" not in source