Architecture 8 runtime integration

autoresearch/prefill/prepare.py

@@ -4,10 +4,225 @@
 
 import argparse
 import csv
+import hashlib
 import importlib.util
 import json
 import time
 from pathlib import Path
+from typing import Any
+
+
+class ReportValidationError(ValueError):
+    """A report/evaluator contract failure, not an infrastructure failure."""
+
+
+class ResumeValidationError(ReportValidationError):
+    """A resumed report could not prove safe reuse of an upstream artifact."""
+
+    def __init__(self, message: str, *, route_state: str = "CRITIC") -> None:
+        super().__init__(message)
+        self.route_state = route_state
+
+
+REPORT_PROVENANCE_SCHEMA_VERSION = 1
+CRITIC_ARTIFACT_SCHEMA_VERSION = 1
+
+
+def _canonical_json(payload: dict[str, Any]) -> bytes:
+    return json.dumps(
+        payload,
+        ensure_ascii=False,
+        sort_keys=True,
+        separators=(",", ":"),
+    ).encode()
+
+
+def critic_artifact_payload(
+    stage: dict,
+    *,
+    source_run_id: str,
+    target_obligation_id: str,
+    candidate_sha256: str,
+    strategy_sha256: str,
+    parent_statement_sha256: str,
+    parent_signature_sha256: str,
+    root_goal_sha256: str,
+    ledger_id: str,
+    ledger_version: int,
+    generator_output_sha256: str,
+) -> dict:
+    """Build the content-addressed evaluation artifact for a physical Critic."""
+    if stage.get("name") != "agent_critic":
+        raise ReportValidationError("Critic artifact requires a physical Critic stage")
+    return {
+        "schema_version": CRITIC_ARTIFACT_SCHEMA_VERSION,
+        "artifact_kind": "critic_evaluation",
+        "source_run_id": source_run_id,
+        "bindings": {
+            "target_obligation_id": target_obligation_id,
+            "candidate_sha256": candidate_sha256,
+            "strategy_sha256": strategy_sha256,
+            "parent_statement_sha256": parent_statement_sha256,
+            "parent_signature_sha256": parent_signature_sha256,
+            "root_goal_sha256": root_goal_sha256,
+            "ledger_id": ledger_id,
+            "ledger_version": int(ledger_version),
+            "generator_output_sha256": generator_output_sha256,
+        },
+        "critic_stage": dict(stage),
+    }
+
+
+def load_critic_artifact(
+    artifact_ref: dict,
+    *,
+    expected_bindings: dict,
+) -> dict:
+    """Verify hash, schema, source identity, and all checkpoint bindings."""
+    required_ref = {
+        "role", "sha256", "schema_version", "dependencies", "path",
+        "source_run_id",
+    }
+    if not isinstance(artifact_ref, dict) or not required_ref.issubset(artifact_ref):
+        raise ResumeValidationError("resumed report has no complete Critic artifact ref")
+    if artifact_ref["role"] != "critic":
+        raise ResumeValidationError("reused artifact role is not critic")
+    if int(artifact_ref["schema_version"]) != CRITIC_ARTIFACT_SCHEMA_VERSION:
+        raise ResumeValidationError("reused Critic artifact schema is incompatible")
+    path = Path(str(artifact_ref["path"])).expanduser()
+    try:
+        encoded = path.read_bytes()
+    except OSError as exc:
+        raise ResumeValidationError(
+            f"reused Critic artifact is unavailable: {exc}",
+        ) from exc
+    digest = hashlib.sha256(encoded).hexdigest()
+    if digest != str(artifact_ref["sha256"]):
+        raise ResumeValidationError("reused Critic artifact hash mismatch")
+    try:
+        payload = json.loads(encoded)
+    except json.JSONDecodeError as exc:
+        raise ResumeValidationError("reused Critic artifact is not JSON") from exc
+    if (
+        not isinstance(payload, dict)
+        or payload.get("schema_version") != CRITIC_ARTIFACT_SCHEMA_VERSION
+        or payload.get("artifact_kind") != "critic_evaluation"
+        or payload.get("source_run_id") != artifact_ref["source_run_id"]
+    ):
+        raise ResumeValidationError("reused Critic artifact provenance mismatch")
+    bindings = payload.get("bindings")
+    if not isinstance(bindings, dict):
+        raise ResumeValidationError("reused Critic artifact has no bindings")
+    for name, expected in expected_bindings.items():
+        actual = bindings.get(name)
+        if name == "ledger_version":
+            actual, expected = int(actual or 0), int(expected or 0)
+        else:
+            actual, expected = str(actual or ""), str(expected or "")
+        if actual != expected:
+            route = "GENERATOR" if name in {
+                "target_obligation_id", "candidate_sha256", "strategy_sha256",
+                "parent_statement_sha256", "parent_signature_sha256",
+                "root_goal_sha256",
+            } else "CRITIC"
+            raise ResumeValidationError(
+                f"reused Critic artifact {name} mismatch",
+                route_state=route,
+            )
+    dependencies = list(artifact_ref.get("dependencies") or [])
+    expected_dependencies = [
+        str(bindings.get("candidate_sha256", "")),
+        str(bindings.get("parent_statement_sha256", "")),
+        str(bindings.get("parent_signature_sha256", "")),
+        str(bindings.get("root_goal_sha256", "")),
+        str(bindings.get("generator_output_sha256", "")),
+    ]
+    if dependencies != expected_dependencies:
+        raise ResumeValidationError("reused Critic artifact dependency mismatch")
+    stage = payload.get("critic_stage")
+    if not isinstance(stage, dict) or stage.get("name") != "agent_critic":
+        raise ResumeValidationError("reused Critic artifact has no physical stage")
+    return payload
+
+
+def _report_provenance(report: dict) -> dict | None:
+    provenance = report.get("provenance")
+    if provenance is None:
+        provenance = report.get("config", {}).get("report_provenance")
+    return provenance if isinstance(provenance, dict) else None
+
+
+def _critic_for_evaluation(report: dict, candidate) -> tuple[dict, dict]:
+    stages = report.get("stages", [])
+    if not isinstance(stages, list):
+        raise ReportValidationError("report stages must be a list")
+    provenance = _report_provenance(report)
+    if not provenance or provenance.get("mode", "fresh") == "fresh":
+        critic = next(
+            (stage for stage in stages if stage.get("name") == "agent_critic"),
+            None,
+        )
+        if critic is None:
+            raise ReportValidationError("fresh report has no physical Critic stage")
+        return critic, {
+            "critic_reused": False,
+            "critic_source_run_id": report.get("id", ""),
+            "critic_artifact_sha256": "",
+        }
+    required = {
+        "schema_version", "mode", "resumed_from_state", "resumed_from_role",
+        "strategy_reused", "generator_reused", "critic_reused",
+        "bindings", "reused_artifacts", "newly_executed_stages",
+    }
+    if (
+        not required.issubset(provenance)
+        or provenance.get("schema_version") != REPORT_PROVENANCE_SCHEMA_VERSION
+        or provenance.get("mode") != "resumed"
+    ):
+        raise ResumeValidationError("resumed report provenance schema is incomplete")
+    if not all(
+        provenance.get(name) is True
+        for name in ("strategy_reused", "generator_reused", "critic_reused")
+    ):
+        raise ResumeValidationError("resumed report does not declare required reuse")
+    actual_stage_names = [str(stage.get("name", "")) for stage in stages]
+    if list(provenance["newly_executed_stages"]) != actual_stage_names:
+        raise ResumeValidationError("resumed report executed-stage provenance mismatch")
+    if "agent_critic" in actual_stage_names:
+        raise ResumeValidationError("resumed report ambiguously reuses and executes Critic")
+    bindings = provenance.get("bindings")
+    if not isinstance(bindings, dict):
+        raise ResumeValidationError("resumed report bindings are missing")
+    expected = {
+        "target_obligation_id": candidate.TARGET_OBLIGATION_ID,
+        "candidate_sha256": str(bindings.get("candidate_sha256", "")),
+        "strategy_sha256": str(bindings.get("strategy_sha256", "")),
+        "parent_statement_sha256": str(
+            bindings.get("parent_statement_sha256", ""),
+        ),
+        "parent_signature_sha256": str(
+            bindings.get("parent_signature_sha256", ""),
+        ),
+        "root_goal_sha256": str(bindings.get("root_goal_sha256", "")),
+        "ledger_id": str(bindings.get("ledger_id", "")),
+        "ledger_version": int(bindings.get("ledger_version", 0)),
+    }
+    candidate_hash = getattr(candidate, "CANDIDATE_SHA256", "")
+    if candidate_hash and candidate_hash != expected["candidate_sha256"]:
+        raise ResumeValidationError(
+            "resumed report candidate hash mismatch",
+            route_state="GENERATOR",
+        )
+    critic_ref = provenance.get("reused_artifacts", {}).get("critic")
+    payload = load_critic_artifact(critic_ref, expected_bindings=expected)
+    return payload["critic_stage"], {
+        "critic_reused": True,
+        "critic_source_run_id": payload["source_run_id"],
+        "critic_artifact_sha256": critic_ref["sha256"],
+        "resumed_from_state": provenance["resumed_from_state"],
+        "resumed_from_role": provenance["resumed_from_role"],
+        "newly_executed_stages": actual_stage_names,
+    }
 
 
 def _load_candidate(path: Path):
@@ -20,13 +235,7 @@ def _load_candidate(path: Path):
 
 
 def evaluate(report: dict, candidate) -> dict:
-    stages = report.get("stages", [])
-    critic = next(
-        (stage for stage in stages if stage.get("name") == "agent_critic"),
-        None,
-    )
-    if critic is None:
-        raise ValueError("report has no Critic stage")
+    critic, evaluation_provenance = _critic_for_evaluation(report, candidate)
     prefix_tokens = int(critic.get("prefix_tokens", 0))
     warmup_s = float(critic.get("warmup_wall_s", 0))
     measured_tps = prefix_tokens / warmup_s if warmup_s > 0 else 0.0
@@ -77,6 +286,7 @@ def evaluate(report: dict, candidate) -> dict:
             critic.get("proof_obligations_unresolved", 0),
         ),
         "constraints": constraints,
+        "evaluation_provenance": evaluation_provenance,
     }
 
 

autoresearch/prefill/program.md

@@ -61,6 +61,40 @@ creates a child directly. Completed GAN runs, transcripts, checkpoints, and
 ledger updates remain durable even when the candidate strategy is reverted or
 fixed evaluation fails.
 
+## Event-driven orchestration and recovery
+
+The persisted proof machine, not the outer loop counter, selects the next
+role. Its states include `NEEDS_STRATEGY`, `GENERATOR`, `CRITIC`,
+`DEFINITION_AUDITOR`, `COUNTEREXAMPLE_WORKER`, `SYNTHESIS`, `REFRAME`,
+`DECOMPOSER`, the typed Math IR/Host/Lean gates, `PROOF_SEARCH`,
+`ADVERSARIAL_REVIEW`, `JUDGE`, `COMMIT`, `APPROACH_FAILED`, `PREMISE_AUDIT`,
+`BLOCKED`, and `IDLE`. Every committed transition records the
+exact target, candidate/strategy hashes, parent statement/signature hashes,
+root-goal hash, ledger identity/version, validated artifact hashes and
+dependencies, retry counters, source run IDs, transition reason, resume
+origin, timestamps, and whether Strategy was reused. The checkpoint and its
+content-addressed artifacts are atomic private files with mode `0600`.
+
+Protocol, schema, JSON, EOS, output-budget, and transient role failures retry
+the same role within a bounded budget. Decomposer contract failures resume
+Decomposer. Lean signature/elaboration failures resume Formalizer; Prover
+proof failures resume Prover unless the typed error invalidates Formalizer.
+Host/Judge rejection returns to the earliest invalid artifact. Premise
+suspicion enters independent `PREMISE_AUDIT`. Only confirmed approach failure,
+audited premise invalidation or failed rescue, target/branch invalidation,
+explicit operator request, or configured mathematical stagnation may enter
+`NEEDS_STRATEGY`. Infrastructure failures retain the separate circuit breaker
+and never count as mathematical stagnation. Exhausted role budgets enter
+`BLOCKED`; they do not silently burn another Strategy call.
+
+Each validated certified-role artifact is reusable only when its schema/hash,
+ordered dependency hashes, target, candidate, parent statement/signature,
+root goal, and ledger identity/version still match. Partial or rejected
+artifacts are audit-only. A restart resumes the first unresolved role and
+reports its exact state; a candidate remains active until an explicit Strategy
+trigger. `COMMIT` is idempotent: the deterministic child ID and certificate
+hash prevent duplicate ledger children after a crash.
+
 ## Certified decomposition
 
 Certified decomposition is the authoritative and only child-persistence path.
@@ -74,12 +108,15 @@ fails open without ledger mutation.
 
 Every role artifact binds the exact target ID, parent statement hash, immutable
 root-goal hash, producer role/run ID, and all upstream artifact hashes.
-Decomposer labels are temporary: only the host assigns persistent IDs after
-the complete certificate passes. The proposed graph must be acyclic, all
-labels must exist, and the one-step certificate must contain exactly one child
-and reduction label. That child—including a definition obligation—must occur
-in the explicit reduction contract. Deeper graphs are discovered recursively
-across later certified iterations.
+Decomposer labels are temporary: only the host assigns a persistent ID after
+the complete certificate passes. The current artifact schema contains exactly
+one `child` object and one complete `reduction_contract` object; it has no
+`children`, dependency-edge, child-label-list, or reduction-label-list fields.
+The contract binds the exact child label, exact parent statement, exact public
+assumptions, and a substantive child-to-parent derivation. If several missing
+definitions are inseparable, Decomposer must preserve all of them inside one
+bundled `DEFINITION` child and bind every source definition label. Deeper
+graphs are discovered recursively across later certified iterations.
 
 Formalizer must preserve an existing parent Lean signature/hash exactly, or
 propose a new parent signature only for an `UNFORMALIZED` parent. Parent and
@@ -105,6 +142,39 @@ benchmark here. Model/tokenizer/quantization/rope/window/cache-format changes
 must be deployed outside this supervisor. Cold benchmarks are explicit,
 separate invocations of `scripts/benchmark_prefill_architecture.py`.
 
+## Creative decomposition v3
+
+Decomposer and Synthesis may first reason in an isolated private scratchpad
+using prose or LaTeX. This consumes research budget but is untrusted,
+audit-only, never parsed, and never enters Math IR, Lean, a gate, or the
+ledger. The Host subsequently generates a finite menu of versioned typed moves
+with scoped operands, preconditions, strict complexity metrics, theorem-card
+support, and content hashes. Model transport contains candidate IDs and typed
+reason codes only.
+
+The registry includes case split, domain restriction, irrelevant-assumption
+removal, holomorphic extension, singularity contradiction, and retained
+definition/local-convergence/growth/bridge moves. Exact or alpha-equivalent
+ancestors, disconnected tasks, unsupported symbols, unverified premises,
+duplicates, and non-simplifying moves are excluded before ranking. Exactly one
+child may continue through the existing Host and Lean gates.
+
+`SYNTHESIS`/`REFRAME` is event-driven after semantic stagnation, repeated no
+move, or sufficiently broad cross-role evidence. Counterexamples remain
+advisory unless independently verified. Reframing may change a case partition
+or viewpoint; only a typed whole-approach failure returns to global Strategy.
+
+The local holomorphicity candidate is explicitly a special-case lemma: poles
+lie outside an open disk, the terms converge locally uniformly there, the sum
+is holomorphic, and agreement with a nonzero simple-pole expression produces
+the proposed contradiction. It never claims to prove the parent; a separate
+parent case-split reduction is mandatory.
+
+Theorem cards are bounded deterministic records from the pinned local Mathlib
+checkout. Each contains an actual declaration name and type, import, source
+and environment hashes, tags, and required hypotheses. CI elaborates all card
+names with `#check` and rejects stale hashes.
+
 Retained KV capacity—not nominal Prefill admission—is the hard model-call
 limit. The deployed default is sink 4 + window 2048 = 2052 tokens. Every
 Strategy, Generator, Critic, premise, and certified-role chat template is
@@ -124,14 +194,39 @@ Strategy proposes exactly one next proof step/question. Generator emits exactly
 one bounded ISSUE_RESPONSE. Before Generator decode, the host reserves enough
 retained capacity for Critic's fixed package plus the complete Generator
 output; Critic receives that output byte-for-byte with the same exact
-ProofStepInterface. Certified Decomposer proposes exactly one child per
-certificate; recursive later iterations perform deeper decomposition.
+ProofStepInterface. Certified Decomposer proposes exactly one structurally
+singular child per certificate; recursive later iterations perform deeper
+decomposition. A complete multi-child response receives one bounded fresh
+protocol-repair call with exact host validation errors and all rejected
+obligations, requiring one bundled child. An output-cap/no-EOS response
+receives one bounded fresh compact retry from the original certified package,
+never a JSON continuation or splice. A second violation fails closed before
+Formalizer, Prover, or Judge.
 
 If an exact statement, structured artifact field, ISSUE block, dependency
 node, or Lean source is indivisible and too large, fail closed with
 `SEMANTIC_UNIT_TOO_LARGE`. Never slice tokens or strings, drop tails, or call a
 model summary lossless. Recursive decomposition preserves exact certified
 interfaces and reduction semantics, not arbitrary prose-history equivalence.
+Structured-role output is budgeted from actual retained availability after the
+tokenized prompt and control reserve. Decomposer must retain at least 512
+output tokens within the 2052-token window; otherwise it fails before decode
+with `STRUCTURED_RESPONSE_BUDGET_TOO_SMALL`. No-EOS and incomplete JSON remain
+audit-only and never enter formal review or persistence.
+
+Structured Artifact closure is a transport contract, not a conversational
+convention. Models commonly append prose, an extra brace, or a second attempted
+Artifact. The former implementation checked role-specific semantic validity
+after tokens had already been generated; a syntactically closed but
+schema-invalid first object therefore failed to stop transport, and divergent
+repair prompts let the same defect recur in later roles. Every structured role
+now uses one registered, string/escape-aware closure scanner. Generation stops
+at the first balanced top-level object after the exact heading/marker with
+`semantic_complete`; normal strict JSON, schema, binding, Lean, and host gates
+then accept or reject that first object. They never scan ahead to a replacement.
+Historical output with an extra brace, prose, Markdown fence, or second object
+remains strictly invalid. The deterministic structured-output contract suite is
+a mandatory local and GitHub CI gate for every registered role.
 
 The concise stable `STRATEGY_CONTRACT` in `supervisor.py` is the authoritative
 deterministic projection of this human-owned program for Strategy inference.