From a55fb9bdc1a07aa2dd8539f60520317e1923693f Mon Sep 17 00:00:00 2001 From: fluffy314 Date: Wed, 22 Jul 2026 21:21:30 +0800 Subject: [PATCH] feat(autoresearch): certify autonomous proof decomposition Require bounded, isolated proof workers to produce host-validated premise audits and complete Lean reduction certificates so false or irrelevant branches cannot masquerade as mathematical progress. Co-authored-by: Cursor --- autoresearch/prefill/lean_gate.py | 80 +- autoresearch/prefill/program.md | 160 +- autoresearch/prefill/semantic_decompose.py | 210 ++ autoresearch/prefill/supervisor.py | 699 +++- scripts/agent_gan_inference_demo.py | 62 +- scripts/agent_gan_repl.py | 2876 ++++++++++++++++- .../bench/test_autoresearch_supervisor.py | 355 +- .../bridge/test_agent_gan_demo.py | 148 +- .../bridge/test_agent_gan_repl.py | 1415 +++++++- .../distributed/test_mlx_ring.py | 19 + 10 files changed, 5839 insertions(+), 185 deletions(-) create mode 100644 autoresearch/prefill/semantic_decompose.py diff --git a/autoresearch/prefill/lean_gate.py b/autoresearch/prefill/lean_gate.py index 3b01934c..47737033 100644 --- a/autoresearch/prefill/lean_gate.py +++ b/autoresearch/prefill/lean_gate.py @@ -58,6 +58,11 @@ def _signature_only(source: str) -> str: return source[:match.start()].strip() if match else source.strip() +def lean_theorem_signature_hash(source: str) -> str: + signature = " ".join(_signature_only(source).split()) + return hashlib.sha256(signature.encode()).hexdigest() if signature else "" + + def _run_lean( content: str, *, @@ -212,8 +217,7 @@ def validate_lean_signature( status="TYPECHECK_FAILED", error="theorem signature must end with `:= by` proof scaffold", ) - signature = " ".join(_signature_only(source).split()) - signature_hash = hashlib.sha256(signature.encode()).hexdigest() + signature_hash = lean_theorem_signature_hash(source) content = ( "import KakeyaLeanGate\n\n" "set_option autoImplicit false\n\n" @@ -289,3 +293,75 @@ def validate_lean_signature( elapsed_s=total_elapsed, output=output, ) + + +def validate_lean_proof( + source: str, + *, + project_root: Path, + timeout_s: float = 45.0, +) -> LeanSignatureResult: + """Compile one complete theorem without sorry/admit or added axioms.""" + source = source.strip() + if ( + not source + or len(source) > 12_000 + or _FORBIDDEN.search(source) + or re.search(r"\b(?:sorry|admit)\b", source) + ): + return LeanSignatureResult( + source, + "", + False, + status="UNSAFE_REJECTED", + error="Lean proof is empty, unsafe, oversized, or incomplete", + ) + declarations = re.findall( + r"^\s*theorem\s+([A-Za-z_][\w']*)", + source, + re.MULTILINE, + ) + if len(declarations) != 1 or not re.search(r"\s*:=\s*by\b", source): + return LeanSignatureResult( + source, + "", + False, + status="TYPECHECK_FAILED", + error="expected exactly one complete theorem declaration", + ) + proof_hash = hashlib.sha256(source.encode()).hexdigest() + run = _run_lean( + "import KakeyaLeanGate\n\nset_option autoImplicit false\n\n" + + source + + "\n", + project_root=project_root, + timeout_s=timeout_s, + ) + if run.timed_out: + return LeanSignatureResult( + source, + proof_hash, + False, + status="TYPECHECK_TIMEOUT", + error=f"Lean proof timed out after {timeout_s:.1f}s", + elapsed_s=run.elapsed_s, + output=run.output, + ) + if run.returncode != 0: + return LeanSignatureResult( + source, + proof_hash, + False, + status="TYPECHECK_FAILED", + error=f"Lean proof failed: {run.output[-2000:]}", + elapsed_s=run.elapsed_s, + output=run.output, + ) + return LeanSignatureResult( + source, + proof_hash, + True, + status="PROVED", + elapsed_s=run.elapsed_s, + output=run.output, + ) diff --git a/autoresearch/prefill/program.md b/autoresearch/prefill/program.md index c38b6ee9..a6ef45cd 100644 --- a/autoresearch/prefill/program.md +++ b/autoresearch/prefill/program.md @@ -1,6 +1,6 @@ # Prefill AutoResearch Program -You are optimizing the two-Mac full-context RH proof research system. +You are optimizing the two-Mac retained-interface RH proof research system. ## Ownership @@ -36,7 +36,7 @@ Use a lexicographic objective: 3. Modify only `candidate.py`. 4. Verify Primary and allens health without restarting either service. 5. Preserve all KV caches across decomposition iterations. -6. Run the fixed full-context acceptance workload. +6. Run the fixed retained-capacity certified-interface acceptance workload. 7. Run `prepare.py` against the resulting report. 8. Keep the candidate only if every hard constraint passes and it closes an obligation, falsifies a novel hypothesis, or creates a novel smaller @@ -48,15 +48,55 @@ contain a falsifiable hypothesis plus distinct Generator and Critic directives. 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 +file request. A valid premise invalidation is also an immediate event-driven +Strategy trigger. It is informative recovery, but does not reset mathematical +stagnation as proof progress. +If an optional Strategy replan exceeds its exact-interface retained 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 -candidate strategy is reverted or fixed evaluation fails. +that free-form text is only a trigger for certified decomposition and never +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. + +## Certified decomposition + +Certified decomposition is the authoritative and only child-persistence path. +For an unresolved frontier, seven isolated fresh-session workers run in order: +Definition Auditor, Counterexample Worker, Decomposer, Formalizer, Prover, +Adversarial Proponent, and Judge. Every role uses allens Prefill and Primary +decode with no shared session/KV state; only explicit host-packaged artifacts +and hashes flow forward. Raw transcripts and parsed artifacts are persisted in +one private atomic manifest. Any timeout, malformed binding, or role failure +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. + +Formalizer must preserve an existing parent Lean signature/hash exactly, or +propose a new parent signature only for an `UNFORMALIZED` parent. Parent and +all child signatures must pass the pinned signature gate. The reduction +signature may assume the child propositions and declared public assumptions, +but Prover must provide a complete proof of that exact reduction theorem. +`sorry`, `admit`, axioms, unsafe commands, placeholders, signature changes, +disconnected children, semantic duplicates, and vague glossary tasks reject +the entire bundle. Judge receives only the host-generated verification +manifest and cannot override a failed host gate. + +Lean certification proves only that the formal child propositions and public +assumptions suffice for the exact formal parent proposition in the accepted +reduction theorem. The mapping from mathematical prose to Math IR and Lean +propositions remains model-authored semantic translation; host hashes, +typechecking, and adversarial review make that translation explicit but do not +prove it faithfully represents the intended informal mathematics. Worker lifecycle and cache policy belong to the inference serving plane, not the proof experiment. `prefill_compute_chunk_tokens` is immutable during this @@ -65,21 +105,107 @@ 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`. -Prefill budgets are hard admission limits, never truncation instructions. -Strategy input must fit 8448 tokens by carrying the complete active leaf -ancestry and its exact experiment records. Generator and Critic inputs must fit -6144 tokens; the Critic always receives the complete current Generator output. -Repeated Strategy strings are interned once in `text_by_id`; `_ref` fields -losslessly reference that exact text. -If any complete semantic unit exceeds its budget, reject it before remote -Prefill and preserve the checkpoint. Never slice, sample, summarize, or drop -the tail of an over-budget input. +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 +counted before append and must fit `min(configured prefill, +max_retained_tokens)`, including explicit control/decode reserve where needed. +No call may rely on evicted middle tokens. + +Every active model call receives one exact `ProofStepInterface`: immutable root +hash, exact target statement, exact formal target/parent certificate interface, +public assumptions, immediate dependency interface, relevant active no-go +premises, current target evidence, and archive hashes. Eleven-node prose +ancestry and historical evidence are not active context. They remain durable +and hash-addressed; this is state selection, not an LLM summary and not a claim +of arbitrary natural-language full-attention equivalence. + +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. + +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. + +The concise stable `STRATEGY_CONTRACT` in `supervisor.py` is the authoritative +deterministic projection of this human-owned program for Strategy inference. +It includes the objective, event triggers, obligation/no-go/premise recovery +rules, exact-target requirement, immutable candidate/runtime constraints, and +the no-fallback/no-truncation contract. The full program remains authoritative +for host behavior but is not serialized into every Strategy prompt. Obligation IDs are host-owned. Treat IDs emitted by Generator/Critic as untrusted labels and bind verdicts to the exact current target. Never persist a model-invented ID. Reject a proposed child when it duplicates an existing statement or lemma name, is highly similar to an ancestor, or is too vague to -be falsifiable. A rejected cyclic frontier is `INCONCLUSIVE`, not progress. +be falsifiable. Also reject any child that canonically or semantically repeats +a persisted no-go premise. A rejected cyclic frontier is `INCONCLUSIVE`, not +progress. + +Every `DISPROVED` ISSUE_VERDICT distinguishes +`Invalidation: APPROACH|PREMISE_SUSPECTED`. Missing invalidation is legacy +`APPROACH`; legacy transcript value `PREMISE` is only a suspicion. A suspicion +must name `Premise refuted`, identify one evidence type, and provide a concrete +one-line JSON artifact. It never directly closes or quarantines a branch. + +The worker automatically runs two fresh, ordered inference roles for every +structurally valid suspicion. The isolated Premise Auditor returns +`PREMISE_AUDIT` with `CONFIRMED|NOT_CONFIRMED|INCONCLUSIVE`, evidence +type/source, confidence, artifact, and analysis. The isolated Adversarial +Proponent then receives only the immutable goal, host-packaged suspicion, and +complete Auditor output and returns `PREMISE_DEFENSE` with +`RESCUED|NOT_RESCUED|INCONCLUSIVE`, exact correction/failure, and evidence. +Each inference uses a distinct session on allens-prefill/Primary-decode; only +explicit text crosses role boundaries. Both complete outputs and parsed +artifacts are durably persisted. Any timeout, malformed output, or worker +failure is an `INCONCLUSIVE` review and can never invalidate a premise. + +The host upgrades to `PREMISE_INVALIDATED` only on a structurally valid +suspicion, Auditor `CONFIRMED` at confidence >= 0.8, Proponent `NOT_RESCUED`, +and a deterministically verified artifact. Arithmetic evidence uses one +host-normalized `FOR_ALL` claim object (`variables`, domain, lhs, claimed +relation, rhs). The host hashes this exact schema at suspicion time. The +Auditor must preserve the schema/hash, bind every quantified variable exactly +once, and provide a finite witness for which the Critic's claimed relation +evaluates false. Unknown variables, true-but-unrelated arithmetic, missing +bindings, schema changes, or hash changes are rejected. + +Lean evidence is bound to the target's host-recorded `lean_signature_hash` and +must claim `NEGATION_OF_TARGET_SIGNATURE`. The current stored Lean signature +format does not permit the host to safely synthesize an exact negation wrapper, +so Lean artifacts are presently recorded but fail open to `INCONCLUSIVE` even +if their standalone theorem compiles. Pinned theorem references are likewise +untrusted until a local exact-assumption registry exists. + +Before upgrade, descendants retain their statuses and only reversible +`SUSPECTED`/temporary-quarantine metadata is recorded. After upgrade, the host +marks the target `DISPROVED/PREMISE_INVALIDATED`, quarantines descendants, +stores one bound-schema-hash no-go lesson with confidence/evidence/worker-run +provenance, and backjumps to the nearest sound unresolved ancestor. A later +Auditor `NOT_CONFIRMED` or Proponent `RESCUED` deterministically restores prior +statuses and marks quarantine/no-go records `REVERSED`. `APPROACH` failure +never quarantines descendants or siblings. + +After a structurally valid suspicion completes review without verified +upgrade (`NOT_CONFIRMED`, `RESCUED`, or `INCONCLUSIVE`), the host clears all +temporary quarantine, restores descendants, preserves audit provenance, and +closes only the attempted leaf as `DISPROVED/APPROACH_FAILED`. This fallback +is allowed only when the original Critic DISPROVED evidence passed the existing +strong closure gate. It creates no no-go lesson or premise quarantine. + +Only a host-upgraded invalidation triggers supervisor `premise-invalidated`. +Suspicion initiates worker audit but is neither proof progress nor permanent +falsification. The exact Strategy interface carries only active relevant no-go +records. New candidates must not assume, rename, or reconstruct them. Lean +signature typechecking remains merely `FORMALIZED` and does not establish +premise truth; only the separate complete-proof gate can validate Lean +evidence. `DECOMPOSED` is keepable only when the host actually persisted at least one new child that passed the ID, novelty, cycle, and falsifiability gates. diff --git a/autoresearch/prefill/semantic_decompose.py b/autoresearch/prefill/semantic_decompose.py new file mode 100644 index 00000000..a8562fa0 --- /dev/null +++ b/autoresearch/prefill/semantic_decompose.py @@ -0,0 +1,210 @@ +"""Retained-KV admission and exact one-step proof interfaces.""" +from __future__ import annotations + +import hashlib +import json +from dataclasses import asdict, dataclass, field + + +class SemanticUnitTooLarge(ValueError): + status = "SEMANTIC_UNIT_TOO_LARGE" + + def __init__(self, unit: str, token_count: int, max_tokens: int) -> None: + self.unit = unit + self.token_count = int(token_count) + self.max_tokens = int(max_tokens) + super().__init__( + f"{self.status}: {unit} requires {token_count} retained tokens; " + f"limit is {max_tokens}", + ) + + +class SemanticResponseIncomplete(RuntimeError): + """A structured role stopped before EOS; partial output is audit-only.""" + + status = "SEMANTIC_RESPONSE_INCOMPLETE" + + def __init__( + self, + role: str, + *, + token_count: int, + stop_reason: str, + response_cap_exhausted: bool, + ) -> None: + self.role = role + self.token_count = int(token_count) + self.stop_reason = str(stop_reason) + self.response_cap_exhausted = bool(response_cap_exhausted) + super().__init__( + f"{self.status}: {role} stopped before EOS after {token_count} " + f"tokens (stop_reason={stop_reason}, " + f"response_cap_exhausted={response_cap_exhausted})" + ) + + +@dataclass(frozen=True) +class ProofStepInterface: + root_goal_hash: str + target_obligation_id: str + target_statement: str + target_statement_hash: str + target_formal_status: str = "UNFORMALIZED" + target_lean_signature: str = "" + target_lean_signature_hash: str = "" + parent_interface: dict = field(default_factory=dict) + public_assumptions: list[str] = field(default_factory=list) + dependency_interface: dict = field(default_factory=dict) + active_no_go_lessons: list[dict] = field(default_factory=list) + current_target_evidence: str = "" + archive_manifest: dict = field(default_factory=dict) + interface_hash: str = "" + + +def canonical_hash(value) -> str: + encoded = json.dumps( + value, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ) + return hashlib.sha256(encoded.encode()).hexdigest() + + +def build_proof_step_interface( + *, + root_goal_hash: str, + target: dict, + parent: dict | None, + active_no_go_lessons: list[dict], + archive_manifest: dict, +) -> ProofStepInterface: + statement = str(target.get("statement", "")) + parent_interface = {} + if parent is not None: + parent_interface = { + "obligation_id": parent.get("obligation_id", ""), + "statement_hash": hashlib.sha256( + str(parent.get("statement", "")).encode(), + ).hexdigest(), + "formal_status": parent.get("formal_status", "UNFORMALIZED"), + "lean_signature": parent.get("lean_signature", ""), + "lean_signature_hash": parent.get("lean_signature_hash", ""), + "certificate_hash": parent.get( + "decomposition_certificate_hash", + "", + ), + "reduction_theorem_hash": parent.get( + "reduction_theorem_hash", + "", + ), + "dependency_ids": list(parent.get("dependency_ids", [])), + } + payload = { + "root_goal_hash": root_goal_hash, + "target_obligation_id": target.get("obligation_id", ""), + "target_statement": statement, + "target_statement_hash": hashlib.sha256( + statement.encode(), + ).hexdigest(), + "target_formal_status": target.get( + "formal_status", + "UNFORMALIZED", + ), + "target_lean_signature": target.get("lean_signature", ""), + "target_lean_signature_hash": target.get( + "lean_signature_hash", + "", + ), + "parent_interface": parent_interface, + "public_assumptions": list(target.get("public_assumptions", [])), + "dependency_interface": { + "certificate_hash": target.get( + "decomposition_certificate_hash", + "", + ), + "reduction_theorem_hash": target.get( + "reduction_theorem_hash", + "", + ), + "dependency_labels": list(target.get("dependency_labels", [])), + "dependency_ids": list(target.get("dependency_ids", [])), + }, + "active_no_go_lessons": active_no_go_lessons, + "current_target_evidence": target.get("last_evidence", ""), + "archive_manifest": archive_manifest, + } + return ProofStepInterface( + **payload, + interface_hash=canonical_hash(payload), + ) + + +def serialize_proof_step_interface(interface: ProofStepInterface) -> str: + return json.dumps( + asdict(interface), + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ) + + +def effective_input_limit( + configured_prefill_tokens: int, + max_retained_tokens: int, + *, + control_reserve_tokens: int = 0, +) -> int: + if configured_prefill_tokens <= 0 or max_retained_tokens <= 0: + raise ValueError("token limits must be > 0") + if control_reserve_tokens < 0: + raise ValueError("control reserve must be >= 0") + effective = min( + int(configured_prefill_tokens), + int(max_retained_tokens) - int(control_reserve_tokens), + ) + if effective <= 0: + raise ValueError("control reserve consumes retained capacity") + return effective + + +def admit_token_ids( + unit: str, + token_ids, + *, + configured_prefill_tokens: int, + max_retained_tokens: int, + control_reserve_tokens: int = 0, +) -> int: + limit = effective_input_limit( + configured_prefill_tokens, + max_retained_tokens, + control_reserve_tokens=control_reserve_tokens, + ) + token_count = len(token_ids) + if token_count > limit: + raise SemanticUnitTooLarge(unit, token_count, limit) + return token_count + + +def downstream_output_cap( + *, + max_retained_tokens: int, + fixed_downstream_tokens: int, + configured_output_tokens: int | None, + control_reserve_tokens: int = 32, +) -> int: + available = ( + int(max_retained_tokens) + - int(fixed_downstream_tokens) + - int(control_reserve_tokens) + ) + if available <= 0: + raise SemanticUnitTooLarge( + "downstream fixed package", + fixed_downstream_tokens + control_reserve_tokens, + max_retained_tokens, + ) + if configured_output_tokens is None or configured_output_tokens <= 0: + return available + return min(int(configured_output_tokens), available) diff --git a/autoresearch/prefill/supervisor.py b/autoresearch/prefill/supervisor.py index 7c53a81c..dd77d778 100644 --- a/autoresearch/prefill/supervisor.py +++ b/autoresearch/prefill/supervisor.py @@ -16,10 +16,18 @@ import threading import time import urllib.request +from dataclasses import asdict from pathlib import Path from autoresearch.prefill.prepare import _load_candidate, evaluate from autoresearch.prefill.lean_gate import warm_lean_environment +from autoresearch.prefill.semantic_decompose import ( + SemanticResponseIncomplete, + SemanticUnitTooLarge, + admit_token_ids, + build_proof_step_interface, + downstream_output_cap, +) REQUIRED_CANDIDATE_FIELDS = ( @@ -104,12 +112,41 @@ def validate_candidate(candidate: dict) -> None: raise ValueError("candidate must require full context") if candidate.get("allow_fallback", False) is not False: raise ValueError("candidate must forbid fallback") + plan = candidate.get("plan") + if isinstance(plan, dict) and len(plan.get("steps", [])) > 1: + raise ValueError("Strategy candidate must propose exactly one step") def _select_repair_target(current: dict, ledger: dict) -> str: leaves = _pending_leaf_ids(ledger) if not leaves: raise ValueError("proof ledger has no unresolved leaf") + backjump_target = str(ledger.get("backjump_target_id", "")) + if backjump_target: + if backjump_target in leaves: + return backjump_target + parents = { + str(item.get("obligation_id", "")): str(item.get("parent_id", "")) + for item in ledger.get("obligations", []) + } + + def descends_from_backjump(obligation_id: str) -> bool: + cursor = obligation_id + visited = set() + while cursor and cursor not in visited: + if cursor == backjump_target: + return True + visited.add(cursor) + cursor = parents.get(cursor, "") + return False + + backjump_leaves = [ + obligation_id + for obligation_id in leaves + if descends_from_backjump(obligation_id) + ] + if backjump_leaves: + return backjump_leaves[0] current_target = str(current.get("target_obligation_id", "")) if current_target in leaves: return current_target @@ -310,6 +347,18 @@ def _extract_json(text: str) -> dict: stripped, re.DOTALL | re.IGNORECASE, ): + repaired = re.sub( + r'\\(?!(?:["\\/]|u[0-9a-fA-F]{4}))', + r"\\\\", + block.strip(), + ) + try: + value = json.loads(repaired) + except json.JSONDecodeError: + value = None + if isinstance(value, dict): + value["strategy_parse_mode"] = "json-escape-repaired" + return value try: value = ast.literal_eval(block.strip()) except (SyntaxError, ValueError): @@ -388,6 +437,15 @@ def parse_research_verdict(output: str, candidate_id: str) -> dict: "created_obligation_ids": list( fields.get("created_obligation_ids", []), ), + "invalidation_kind": str( + fields.get("invalidation_kind", ""), + ), + "backjump_target_id": str( + fields.get("backjump_target_id", ""), + ), + "no_go_lesson_hashes": list( + fields.get("no_go_lesson_hashes", []), + ), } matches = list(re.finditer( r"^(?:critic>\s*)?### AUTORESEARCH_VERDICT\s*$" @@ -419,45 +477,73 @@ def parse_research_verdict(output: str, candidate_id: str) -> dict: "evidence": fields["Evidence"], "new_frontier": fields["New frontier"], "created_obligation_ids": [], + "invalidation_kind": "", + "backjump_target_id": "", + "no_go_lesson_hashes": [], } def _pending_leaf_ids(ledger: dict) -> list[str]: obligations = ledger.get("obligations", []) + by_id = { + str(item.get("obligation_id", "")): item + for item in obligations + } + + def invalidated_by_ancestor(item: dict) -> bool: + cursor = str(item.get("parent_id", "")) + visited = set() + while cursor and cursor not in visited: + visited.add(cursor) + ancestor = by_id.get(cursor) + if ancestor is None: + break + if ( + ancestor.get("status") == "QUARANTINED" + or ( + ancestor.get("status") == "DISPROVED" + and ancestor.get("invalidation_kind") in { + "PREMISE", + "PREMISE_INVALIDATED", + } + ) + ): + return True + cursor = str(ancestor.get("parent_id", "")) + return False + unresolved = { str(item.get("obligation_id", "")) for item in obligations - if item.get("status") == "UNRESOLVED" + if ( + item.get("status") == "UNRESOLVED" + and not invalidated_by_ancestor(item) + ) } unresolved_parents = { str(item.get("parent_id", "")) for item in obligations if ( - item.get("status") == "UNRESOLVED" + str(item.get("obligation_id", "")) in unresolved and item.get("parent_id") ) } return sorted(unresolved - unresolved_parents) -def build_strategy_research_state( +def _build_legacy_strategy_research_state( *, current: dict, ledger: dict, results_text: str, ) -> dict: text_by_id: dict[str, str] = {} - id_by_text: dict[str, str] = {} def intern(value) -> str: text = str(value or "") if not text: return "" - existing = id_by_text.get(text) - if existing is not None: - return existing - text_id = f"t{len(text_by_id) + 1}" - id_by_text[text] = text_id + text_id = hashlib.sha256(text.encode()).hexdigest()[:20] text_by_id[text_id] = text return text_id @@ -472,20 +558,57 @@ def intern(value) -> str: while cursor and cursor not in visited: visited.add(cursor) item = obligations[cursor] - ancestry.append({ + ancestry_item = { "obligation_id": cursor, "statement_ref": intern(item.get("statement", "")), "status": item.get("status", ""), "parent_id": item.get("parent_id", ""), "last_run_id": item.get("last_run_id", ""), - "last_evidence_ref": intern(item.get("last_evidence", "")), - }) + } + if cursor == target_id: + ancestry_item["last_evidence_ref"] = intern( + item.get("last_evidence", ""), + ) + ancestry.append(ancestry_item) cursor = str(item.get("parent_id", "")) ancestry.reverse() ancestry_ids = { item["obligation_id"] for item in ancestry } - relevant_results = [] + ancestry_refs = { + item["obligation_id"]: f"a{index}" + for index, item in enumerate(ancestry) + } + for item in ancestry: + item["obligation_ref"] = ancestry_refs[item["obligation_id"]] + parent_id = str(item.pop("parent_id", "")) + item["parent_ref"] = ancestry_refs.get(parent_id, "") + if item["obligation_id"] != target_id: + item.pop("obligation_id", None) + item.pop("last_run_id", None) + + def lesson_is_relevant(lesson: dict) -> bool: + cursor = str(lesson.get("source_obligation_id", "")) + visited = set() + while cursor and cursor not in visited: + if cursor in ancestry_ids: + return True + visited.add(cursor) + source = obligations.get(cursor) + if source is None: + break + cursor = str(source.get("parent_id", "")) + return False + + relevant_lessons = [ + lesson + for lesson in ledger.get("no_go_lessons", []) + if ( + lesson.get("reversible_status", "ACTIVE") == "ACTIVE" + and lesson_is_relevant(lesson) + ) + ] + relevant_rows = [] if results_text.strip(): for row in csv.DictReader( io.StringIO(results_text), @@ -493,25 +616,168 @@ def intern(value) -> str: ): if row.get("target_obligation_id") not in ancestry_ids: continue - relevant_results.append({ - "candidate_id": row.get("candidate_id", ""), - "target_obligation_id": row.get( - "target_obligation_id", - "", - ), - "hypothesis_sha256": row.get("hypothesis_sha256", ""), - "research_outcome": row.get("research_outcome", ""), - "research_evidence_ref": intern( - row.get("research_evidence", ""), - ), - "new_frontier_ref": intern(row.get("new_frontier", "")), - "kept": row.get("kept", ""), - "error": row.get("error", ""), - }) + relevant_rows.append(row) + + def exact_record(row: dict) -> dict: + return { + "timestamp": row.get("timestamp", ""), + "experiment_id": row.get("experiment_id", ""), + "run_id": row.get("run_id", ""), + "candidate_id": row.get("candidate_id", ""), + "target_obligation_id": row.get("target_obligation_id", ""), + "hypothesis_sha256": row.get("hypothesis_sha256", ""), + "research_outcome": row.get("research_outcome", ""), + "invalidation_kind": row.get("invalidation_kind", ""), + "research_evidence": row.get("research_evidence", ""), + "new_frontier": row.get("new_frontier", ""), + "kept": row.get("kept", ""), + "error": row.get("error", ""), + } + + def record_hash(row: dict) -> str: + encoded = json.dumps( + exact_record(row), + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ) + return hashlib.sha256(encoded.encode()).hexdigest()[:20] + + def is_kept(row: dict) -> bool: + return row.get("kept") in {True, "True"} + + def is_proof_critical(row: dict) -> bool: + return ( + is_kept(row) + and row.get("research_outcome") in { + "DECOMPOSED", + "SUPPORTED", + "FALSIFIED", + } + ) or row.get("invalidation_kind") == "PREMISE_INVALIDATED" + + grouped: dict[tuple[str, str], list[dict]] = {} + for row in relevant_rows: + key = ( + str(row.get("target_obligation_id", "")), + str(row.get("hypothesis_sha256", "")), + ) + grouped.setdefault(key, []).append(row) + + hypothesis_values = sorted({hypothesis for _, hypothesis in grouped}) + hypothesis_refs = {} + for hypothesis in hypothesis_values: + prefix_size = min(20, len(hypothesis)) + reference = hypothesis[:prefix_size] + while ( + any( + other != hypothesis and other.startswith(reference) + for other in hypothesis_values + ) + and prefix_size < len(hypothesis) + ): + prefix_size += 1 + reference = hypothesis[:prefix_size] + hypothesis_refs[hypothesis] = reference + experiment_groups = [] + latest_record_hashes = set() + for (group_target, hypothesis_hash), rows in sorted(grouped.items()): + latest = rows[-1] + outcome_counts: dict[str, int] = {} + error_counts: dict[str, int] = {} + hashes = [record_hash(row) for row in rows] + for row in rows: + outcome = str(row.get("research_outcome", "") or "(none)") + outcome_counts[outcome] = outcome_counts.get(outcome, 0) + 1 + error = " ".join(str(row.get("error", "")).split()) + if error: + fingerprint = hashlib.sha256( + error.encode(), + ).hexdigest()[:20] + error_counts[fingerprint] = error_counts.get(fingerprint, 0) + 1 + latest_record_hashes.add(hashes[-1]) + experiment_groups.append([ + ancestry_refs[group_target], + hypothesis_refs[hypothesis_hash], + len(rows), + dict(sorted(outcome_counts.items())), + dict(sorted(error_counts.items())), + [ + rows[0].get("timestamp", ""), + ], + [ + latest.get("timestamp", ""), + ], + hashes[:-1], + [ + hashes[-1], + latest.get("research_outcome", ""), + latest.get("invalidation_kind", ""), + intern(latest.get("research_evidence", "")), + intern(latest.get("new_frontier", "")), + intern(latest.get("error", "")), + ], + ]) + + critical_events = [] + for row in relevant_rows: + if not is_proof_critical(row): + continue + item_hash = record_hash(row) + event = [ + item_hash, + ancestry_refs[str(row.get("target_obligation_id", ""))], + hypothesis_refs[str(row.get("hypothesis_sha256", ""))], + row.get("research_outcome", ""), + row.get("invalidation_kind", ""), + ] + if item_hash not in latest_record_hashes: + event.extend([ + intern(row.get("research_evidence", "")), + intern(row.get("new_frontier", "")), + ]) + critical_events.append(event) + + archive_outcomes: dict[str, int] = {} + archive_errors: dict[str, int] = {} + archive_hashes = [] + for row in relevant_rows: + archive_hashes.append(record_hash(row)) + outcome = str(row.get("research_outcome", "") or "(none)") + archive_outcomes[outcome] = archive_outcomes.get(outcome, 0) + 1 + error = " ".join(str(row.get("error", "")).split()) + if error: + fingerprint = hashlib.sha256(error.encode()).hexdigest()[:20] + archive_errors[fingerprint] = archive_errors.get(fingerprint, 0) + 1 state = { "target_leaf_id": target_id, "target_ancestry": ancestry, - "relevant_experiments": relevant_results, + "proof_critical_events": critical_events, + "experiment_groups": experiment_groups, + "event_view_schema": { + "critical_event": ( + "[hash,target_ref,unique_hypothesis_hash_prefix,outcome," + "invalidation,(evidence_ref,frontier_ref if historical)]" + ), + "experiment_group": ( + "[target_ref,hypothesis_hash_prefix,count,outcomes,errors," + "first_ts,last_ts,prior_hashes," + "latest(hash,outcome,invalidation,evidence,frontier,error)]" + ), + }, + "archive_manifest": { + "source": "append-only results.tsv", + "record_count": len(relevant_rows), + "group_count": len(experiment_groups), + "hypothesis_set_sha256": hashlib.sha256( + "".join(hypothesis_values).encode(), + ).hexdigest(), + "ordered_records_sha256": hashlib.sha256( + "".join(archive_hashes).encode(), + ).hexdigest(), + "outcome_counts": dict(sorted(archive_outcomes.items())), + "error_fingerprint_counts": dict(sorted(archive_errors.items())), + }, "current_candidate": { "candidate_id": current.get("candidate_id", ""), "target_obligation_id": current.get( @@ -523,11 +789,170 @@ def intern(value) -> str: "prefill_compute_chunk_tokens", ), }, + "premise_recovery": { + "backjump_target_id": ledger.get("backjump_target_id", ""), + "no_go_lessons": [ + { + "claim_hash": lesson.get("claim_hash", ""), + "refuted_premise_ref": intern( + lesson.get("refuted_premise", ""), + ), + "evidence_ref": intern(lesson.get("evidence", "")), + "source_obligation_id": lesson.get( + "source_obligation_id", + "", + ), + "run_id": lesson.get("run_id", ""), + "confidence": lesson.get("confidence", 0.0), + "evidence_type": lesson.get("evidence_type", ""), + "evidence_source_ref": intern( + lesson.get("evidence_source", ""), + ), + "auditor_run_id": lesson.get("auditor_run_id", ""), + "proponent_run_id": lesson.get( + "proponent_run_id", + "", + ), + "reversible_status": lesson.get( + "reversible_status", + "ACTIVE", + ), + } + for lesson in relevant_lessons + ], + }, } state["text_by_id"] = text_by_id return state +def build_strategy_research_state( + *, + current: dict, + ledger: dict, + results_text: str, +) -> dict: + target_id = _select_repair_target(current, ledger) + obligations = { + str(item.get("obligation_id", "")): item + for item in ledger.get("obligations", []) + } + target = obligations[target_id] + parent = obligations.get(str(target.get("parent_id", ""))) + ancestry_ids = set() + cursor = target_id + while cursor and cursor not in ancestry_ids: + ancestry_ids.add(cursor) + cursor = str(obligations.get(cursor, {}).get("parent_id", "")) + lessons = [] + for lesson in ledger.get("no_go_lessons", []): + if lesson.get("reversible_status", "ACTIVE") != "ACTIVE": + continue + source = str(lesson.get("source_obligation_id", "")) + visited = set() + relevant = False + while source and source not in visited: + if source in ancestry_ids: + relevant = True + break + visited.add(source) + source = str(obligations.get(source, {}).get("parent_id", "")) + if relevant: + lessons.append({ + "claim_hash": lesson.get("claim_hash", ""), + "refuted_premise": lesson.get("refuted_premise", ""), + "evidence": lesson.get("evidence", ""), + "evidence_type": lesson.get("evidence_type", ""), + "confidence": lesson.get("confidence", 0.0), + }) + record_hashes = [] + outcomes: dict[str, int] = {} + latest_failure = {} + if results_text.strip(): + for row in csv.DictReader(io.StringIO(results_text), delimiter="\t"): + encoded = json.dumps( + dict(row), + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ) + record_hashes.append(hashlib.sha256(encoded.encode()).hexdigest()) + outcome = str(row.get("research_outcome", "") or "(none)") + outcomes[outcome] = outcomes.get(outcome, 0) + 1 + error = str(row.get("error", "")) + if "SEMANTIC_RESPONSE_INCOMPLETE" in error: + role_match = re.search( + r"SEMANTIC_RESPONSE_INCOMPLETE:\s+(\w+)\s+stopped", + error, + ) + token_match = re.search(r"after\s+(\d+)\s+tokens", error) + latest_failure = { + "kind": "SEMANTIC_RESPONSE_INCOMPLETE", + "role": ( + role_match.group(1) if role_match else "unknown" + ), + "response_tokens": ( + int(token_match.group(1)) if token_match else 0 + ), + } + archive_manifest = { + "source": "append-only results.tsv", + "record_count": len(record_hashes), + "ordered_records_sha256": hashlib.sha256( + "".join(record_hashes).encode(), + ).hexdigest(), + "outcome_counts": dict(sorted(outcomes.items())), + "latest_failure": latest_failure, + "ledger_version": ledger.get("version", 0), + "ledger_sha256": hashlib.sha256( + json.dumps( + ledger, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode(), + ).hexdigest(), + } + root_goal_hash = str(ledger.get("root_goal_hash", "")) or hashlib.sha256( + str(ledger.get("ledger_id", "")).encode(), + ).hexdigest() + interface = build_proof_step_interface( + root_goal_hash=root_goal_hash, + target=target, + parent=parent, + active_no_go_lessons=lessons, + archive_manifest=archive_manifest, + ) + return { + "proof_step_interface": asdict(interface), + } + + +STRATEGY_CONTRACT = """\ +Propose exactly ONE novel falsifiable step for TARGET_LEAF_ID as the required +JSON fields; never emit a plan. Keep prefill_compute_chunk_tokens unchanged. +target_obligation_id must equal TARGET_LEAF_ID. +Respect the exact ProofStepInterface, active no-go premises, quarantine and +verified backjumps; never repeat a hypothesis or ancestor cycle. +On SEMANTIC_RESPONSE_INCOMPLETE, choose a strictly smaller question, not shorter +wording of the same step. Require retained-capacity, final-only snapshots, +complete Critic review, Primary decode-only, allens prefill-only, <=300s +segments, and no fallback, sampling, slicing, truncation, restart or cache +clearing. Archive hashes carry no mathematical meaning.""" + + +def build_strategy_contract(program: str) -> str: + required_markers = ( + "## Objective", + "## Hard constraints", + "Only a host-upgraded invalidation", + "The concise stable `STRATEGY_CONTRACT`", + ) + if any(marker not in program for marker in required_markers): + raise ValueError("program is missing authoritative Strategy rules") + return STRATEGY_CONTRACT + + def build_strategy_prompt( *, program: str, @@ -540,24 +965,26 @@ def build_strategy_prompt( ledger=ledger, results_text=results_text, ) + contract = build_strategy_contract(program) return ( - "You are the AutoResearch strategy agent. Follow the human-owned " - "program exactly. Attack TARGET_LEAF_ID and propose " - "one falsifiable GAN strategy experiment. Return JSON only with keys: " + "You are the AutoResearch strategy agent. Follow the authoritative " + "human-owned Strategy contract exactly. Attack TARGET_LEAF_ID and propose " + "exactly one falsifiable next proof step. Return JSON only with keys: " + ", ".join(REQUIRED_CANDIDATE_FIELDS) + ". prefill_compute_chunk_tokens is immutable and must equal " f"{current['prefill_compute_chunk_tokens']}. " - "Do not weaken full context, final-only snapshots, or no-fallback rules." - " The hypothesis must not repeat any hypothesis hash in RESEARCH_STATE. " + "Do not weaken retained-capacity, final-only snapshot, or no-fallback " + "rules. The hypothesis must encode one step, not a multi-level plan. " + "It must not assume, rename, or propose any premise recorded in " + "RESEARCH_STATE.proof_step_interface.active_no_go_lessons. " "It must either construct a concrete object or attempt a concrete " "counterexample for the target leaf. target_obligation_id must equal " - "TARGET_LEAF_ID. Every statement and evidence item below is complete; " - "do not infer omitted text from unrelated branches. Fields ending in " - "_ref resolve through text_by_id; this is lossless deduplication, not " - "summary or truncation." - f"\n\nPROGRAM:\n{program}" + "TARGET_LEAF_ID. The interface is complete for this certified step; " + "archived prose is intentionally inactive and represented only by " + "content hashes, never by an LLM summary." + f"\n\nSTRATEGY_CONTRACT:\n{contract}" "\n\nRESEARCH_STATE:\n" - f"{json.dumps(research_state, ensure_ascii=False)}" + f"{json.dumps(research_state, ensure_ascii=False, separators=(',', ':'))}" ) @@ -649,6 +1076,7 @@ def propose_candidate( results_text: str, ledger: dict, max_prefill_tokens: int = 8448, + max_retained_tokens: int = 2052, ) -> dict: from kakeya import Client from transformers import AutoTokenizer @@ -668,11 +1096,25 @@ def propose_candidate( return_dict=False, enable_thinking=False, ) - if len(ids) > max_prefill_tokens: - raise StrategyPrefillBudgetExceeded( - len(ids), - max_prefill_tokens, + try: + admit_token_ids( + "Strategy ProofStepInterface", + ids, + configured_prefill_tokens=max_prefill_tokens, + max_retained_tokens=max_retained_tokens, + control_reserve_tokens=256, ) + except SemanticUnitTooLarge as exc: + raise StrategyPrefillBudgetExceeded( + exc.token_count, + exc.max_tokens, + ) from exc + strategy_output_cap = downstream_output_cap( + max_retained_tokens=max_retained_tokens, + fixed_downstream_tokens=len(ids), + configured_output_tokens=512, + control_reserve_tokens=32, + ) generated: list[int] = [] print( f"[autoresearch] Strategy Prefill: 0/{len(ids)} tokens (0.0%)", @@ -689,9 +1131,17 @@ def propose_candidate( f"[autoresearch] Strategy Prefill complete: {len(ids)} tokens", flush=True, ) - while len(generated) < 2048: + while len(generated) < strategy_output_cap: before = len(generated) - generated.extend(int(token) for token in session.generate(max_tokens=64)) + generated.extend( + int(token) + for token in session.generate( + max_tokens=min( + 64, + strategy_output_cap - len(generated), + ), + ) + ) print( f"[autoresearch] Strategy Decode: {len(generated)} tokens " f"stop_reason={session.last_stop_reason}", @@ -702,8 +1152,13 @@ def propose_candidate( if len(generated) == before: raise RuntimeError("strategy agent made no progress") if session.last_stop_reason != 2: - raise RuntimeError( - f"strategy agent did not reach EOS: {session.last_stop_reason}", + raise SemanticResponseIncomplete( + "Strategy", + token_count=len(generated), + stop_reason=session.last_stop_reason, + response_cap_exhausted=( + len(generated) >= strategy_output_cap + ), ) strategy_output = tokenizer.decode(generated, skip_special_tokens=True) print( @@ -774,12 +1229,14 @@ def run_gan_experiment( candidate_path: Path, state_path: Path, timeout_s: float, + max_retained_tokens: int, ) -> tuple[str, str]: command = [ "bash", str(repo / "scripts/run_agent_gan_repl.sh"), "--skip-ensure", "--no-auto-loop", "--candidate-file", str(candidate_path), "--state-file", str(state_path), + "--max-retained-tokens", str(max_retained_tokens), ] process = subprocess.Popen( command, @@ -828,6 +1285,15 @@ def terminate_on_timeout() -> None: return run_id, output +def extract_gan_failure_reason(output: str) -> str: + matches = re.findall( + r"^\[inference-failed\].*?\berror=(.+)$", + output, + re.MULTILINE, + ) + return matches[-1].strip() if matches else "" + + def read_results(path: Path) -> list[dict]: if not path.exists(): return [] @@ -865,6 +1331,11 @@ def _row_made_progress(row: dict) -> bool: if row.get("kept") not in {True, "True"}: return False outcome = row.get("research_outcome") + if row.get("invalidation_kind") in { + "PREMISE", + "PREMISE_INVALIDATED", + }: + return False if outcome in {"SUPPORTED", "FALSIFIED"}: return True if outcome == "DECOMPOSED": @@ -887,6 +1358,16 @@ def strategy_trigger_reason( return "manual-cli" if trigger_file is not None and trigger_file.exists(): return "manual-trigger-file" + if ( + results + and results[-1].get("invalidation_kind") == "PREMISE_INVALIDATED" + ): + return "premise-invalidated" + if ( + results + and results[-1].get("invalidation_kind") == "APPROACH_FAILED" + ): + return "branch-falsified" if results and results[-1].get("research_outcome") == "FALSIFIED": return "branch-falsified" stagnant = 0 @@ -899,6 +1380,16 @@ def strategy_trigger_reason( return "" +def infrastructure_failure_fingerprint(row: dict) -> str: + """Return a stable fingerprint for a completed failed infrastructure run.""" + if row.get("research_outcome") != "EVALUATION_FAILED": + return "" + error = " ".join(str(row.get("error", "")).lower().split()) + if not error: + return "" + return hashlib.sha256(error.encode()).hexdigest() + + def build_host_candidate(current: dict, ledger: dict) -> dict: target_id = _select_repair_target(current, ledger) target = next( @@ -908,6 +1399,41 @@ def build_host_candidate(current: dict, ledger: dict) -> dict: ) statement = str(target.get("statement", "")).strip() evidence = str(target.get("last_evidence", "")).strip() + obligations = { + str(item.get("obligation_id", "")): item + for item in ledger.get("obligations", []) + } + target_ancestry = set() + cursor = target_id + while cursor and cursor not in target_ancestry: + target_ancestry.add(cursor) + cursor = str(obligations.get(cursor, {}).get("parent_id", "")) + + def lesson_is_relevant(lesson: dict) -> bool: + source_id = str(lesson.get("source_obligation_id", "")) + visited = set() + while source_id and source_id not in visited: + if source_id in target_ancestry: + return True + visited.add(source_id) + source_id = str( + obligations.get(source_id, {}).get("parent_id", ""), + ) + return False + + no_go = "; ".join( + str(lesson.get("refuted_premise", "")).strip() + for lesson in ledger.get("no_go_lessons", []) + if ( + str(lesson.get("refuted_premise", "")).strip() + and lesson.get("reversible_status", "ACTIVE") == "ACTIVE" + and lesson_is_relevant(lesson) + ) + ) + no_go_directive = ( + f" Forbidden refuted premises: {no_go}." + if no_go else "" + ) digest = hashlib.sha256(target_id.encode()).hexdigest()[:12] candidate = { "candidate_id": f"host-leaf-{digest}", @@ -917,7 +1443,7 @@ def build_host_candidate(current: dict, ledger: dict) -> dict: f"Resolve or falsify the exact target leaf {target_id}: " f"{statement} Previous Critic evidence: {evidence or '(none)'}. " "Provide an explicit derivation or counterexample; do not rename " - "the same gap as a new lemma." + f"the same gap as a new lemma.{no_go_directive}" ), "critic_directive": ( f"Adversarially test target leaf {target_id}. Reject unsupported " @@ -965,6 +1491,7 @@ def should_keep(result: dict, baseline: dict | None) -> bool: "candidate_sha256", "report_path", "hypothesis_sha256", "research_outcome", "research_evidence", "new_frontier", "created_obligation_ids", "strategy_mode", + "invalidation_kind", "backjump_target_id", "no_go_lesson_hashes", "transcript_path", "error", ) @@ -1063,6 +1590,13 @@ def run_iteration(args, iteration: int) -> dict: flush=True, ) ledger_data = json.loads(ledger_path.read_text()) + if state_path.exists(): + checkpoint_data = json.loads(state_path.read_text()) + research_goal = str(checkpoint_data.get("research_goal", "")) + if research_goal: + ledger_data["root_goal_hash"] = hashlib.sha256( + research_goal.encode(), + ).hexdigest() trigger_file = Path(args.strategy_trigger_file).expanduser() trigger_reason = strategy_trigger_reason( results, @@ -1070,7 +1604,7 @@ def run_iteration(args, iteration: int) -> dict: force=args.force_strategy and iteration == 0, trigger_file=trigger_file, ) - if baseline is None and iteration == 0: + if baseline is None and iteration == 0 and not trigger_reason: print( "[autoresearch] phase=baseline using current candidate", flush=True, @@ -1094,6 +1628,7 @@ def run_iteration(args, iteration: int) -> dict: ), ledger=ledger_data, max_prefill_tokens=args.strategy_max_prefill_tokens, + max_retained_tokens=args.max_retained_tokens, ) if proposed["target_obligation_id"] not in _pending_leaf_ids( ledger_data, @@ -1112,6 +1647,14 @@ def run_iteration(args, iteration: int) -> dict: f"fallback=deterministic-host", flush=True, ) + except SemanticResponseIncomplete as exc: + strategy_mode = "host_strategy_deferred" + proposed = build_host_candidate(current, ledger_data) + print( + "[autoresearch] phase=strategy-deferred-semantic " + f"reason={exc} fallback=deterministic-host", + flush=True, + ) else: strategy_mode = "host" proposed = build_host_candidate(current, ledger_data) @@ -1158,6 +1701,7 @@ def run_iteration(args, iteration: int) -> dict: candidate_path=candidate_path, state_path=state_path, timeout_s=args.experiment_timeout_s, + max_retained_tokens=args.max_retained_tokens, ) gan_completed = True transcript_path.write_text(gan_output) @@ -1165,8 +1709,13 @@ def run_iteration(args, iteration: int) -> dict: f"http://127.0.0.1:8090/v1/network/benchmarks/{run_id}", ) if report.get("status") != "completed": + failure_reason = extract_gan_failure_reason(gan_output) raise RuntimeError( - f"GAN benchmark is not completed: {report.get('status')}", + f"GAN benchmark is not completed: {report.get('status')}" + + ( + f"; {failure_reason}" + if failure_reason else "" + ), ) report_path.write_text(json.dumps(report, ensure_ascii=False, indent=2)) candidate_module = _load_candidate(candidate_path) @@ -1182,6 +1731,9 @@ def run_iteration(args, iteration: int) -> dict: "created_obligation_ids": verdict["created_obligation_ids"], "transcript_path": str(transcript_path), "hypothesis_novel": hypothesis_novel, + "invalidation_kind": verdict["invalidation_kind"], + "backjump_target_id": verdict["backjump_target_id"], + "no_go_lesson_hashes": verdict["no_go_lesson_hashes"], }) keep = should_keep(result, baseline) print( @@ -1223,6 +1775,11 @@ def run_iteration(args, iteration: int) -> dict: verdict["created_obligation_ids"], ), "strategy_mode": strategy_mode, + "invalidation_kind": verdict["invalidation_kind"], + "backjump_target_id": verdict["backjump_target_id"], + "no_go_lesson_hashes": json.dumps( + verdict["no_go_lesson_hashes"], + ), "transcript_path": str(transcript_path), } append_result(results_path, row) @@ -1293,6 +1850,11 @@ def main() -> int: type=int, default=8448, ) + parser.add_argument( + "--max-retained-tokens", + type=int, + default=2052, + ) parser.add_argument( "--strategy-stagnation-rounds", type=int, @@ -1330,13 +1892,24 @@ def main() -> int: default=str(Path.home() / ".kakeya/agent_gan_proof_ledger.json"), ) parser.add_argument("--experiment-timeout-s", type=float, default=7200) + parser.add_argument( + "--max-consecutive-infrastructure-failures", + type=int, + default=2, + ) args = parser.parse_args() if args.iterations <= 0: raise SystemExit("iterations must be > 0") if args.strategy_max_prefill_tokens <= 0: raise SystemExit("strategy-max-prefill-tokens must be > 0") + if args.max_retained_tokens <= 0: + raise SystemExit("max-retained-tokens must be > 0") if args.strategy_stagnation_rounds <= 0: raise SystemExit("strategy-stagnation-rounds must be > 0") + if args.max_consecutive_infrastructure_failures <= 0: + raise SystemExit( + "max-consecutive-infrastructure-failures must be > 0", + ) lean_warmup = warm_lean_environment( Path(__file__).resolve().parents[2], ) @@ -1349,9 +1922,33 @@ def main() -> int: ) if not lean_warmup.ok: raise SystemExit(lean_warmup.error) + last_failure_fingerprint = "" + consecutive_infrastructure_failures = 0 for iteration in range(args.iterations): row = run_iteration(args, iteration) print(json.dumps(row, indent=2, sort_keys=True)) + fingerprint = infrastructure_failure_fingerprint(row) + if fingerprint: + if fingerprint == last_failure_fingerprint: + consecutive_infrastructure_failures += 1 + else: + last_failure_fingerprint = fingerprint + consecutive_infrastructure_failures = 1 + if ( + consecutive_infrastructure_failures + >= args.max_consecutive_infrastructure_failures + ): + print( + "[autoresearch] phase=infrastructure-circuit-open " + f"consecutive={consecutive_infrastructure_failures} " + f"fingerprint={fingerprint[:12]} " + f"error={row.get('error', '')}", + flush=True, + ) + return 2 + else: + last_failure_fingerprint = "" + consecutive_infrastructure_failures = 0 return 0 diff --git a/scripts/agent_gan_inference_demo.py b/scripts/agent_gan_inference_demo.py index 7f40d834..ce14e6b4 100644 --- a/scripts/agent_gan_inference_demo.py +++ b/scripts/agent_gan_inference_demo.py @@ -14,6 +14,10 @@ _ensure_services, _json_request, ) +from autoresearch.prefill.semantic_decompose import ( + SemanticResponseIncomplete, + SemanticUnitTooLarge, +) def _agent_cache_gate(warm_delta: dict, actual_delta: dict) -> bool: @@ -56,6 +60,26 @@ def build_critic_context( } +def decode_complete_response(tokenizer, role: str, token_ids, metadata: dict) -> str: + """Decode only EOS-terminated structured output. + + A capped/stalled partial response remains available through token-count + metadata and streaming logs for audit, but cannot enter another role, + parser, or proof ledger. + """ + if not metadata.get("complete", False): + raise SemanticResponseIncomplete( + role, + token_count=len(token_ids), + stop_reason=metadata.get("stop_reason", "unknown"), + response_cap_exhausted=metadata.get( + "response_cap_exhausted", + False, + ), + ) + return tokenizer.decode(token_ids, skip_special_tokens=True) + + def _infer( client, eos_ids, @@ -66,12 +90,25 @@ def _infer( max_response_tokens=None, semantic_progress=None, max_semantic_stall_chunks: int = 3, + client_label: str = "agent-gan", + max_retained_tokens: int = 0, ): if max_semantic_stall_chunks <= 0: raise ValueError("max_semantic_stall_chunks must be > 0") + if max_retained_tokens < 0: + raise ValueError("max_retained_tokens must be >= 0") + if max_retained_tokens and len(token_ids) > max_retained_tokens: + raise SemanticUnitTooLarge( + client_label, + len(token_ids), + max_retained_tokens, + ) before = get_stats() started = time.perf_counter() - with client.create_session(eos_token_ids=eos_ids, client_label="agent-gan") as s: + with client.create_session( + eos_token_ids=eos_ids, + client_label=client_label, + ) as s: append_started = time.perf_counter() s.append(token_ids) append_done = time.perf_counter() @@ -123,6 +160,7 @@ def _infer( and stop_reason == "max_tokens" ): stop_reason = "client_safety_limit" + response_cap_exhausted = stop_reason == "client_safety_limit" done = time.perf_counter() after = get_stats() first_at = first_at or done @@ -136,6 +174,8 @@ def _infer( "delta": _delta(before, after), "stop_reason": stop_reason, "complete": stop_reason == "eos", + "eos_reached": stop_reason == "eos", + "response_cap_exhausted": response_cap_exhausted, } @@ -154,6 +194,7 @@ def main() -> int: "reliably; larger values require more worker memory or timeout.", ) parser.add_argument("--output-tokens", type=int, default=64) + parser.add_argument("--max-retained-tokens", type=int, default=2052) parser.add_argument( "--max-response-tokens", type=int, @@ -165,6 +206,8 @@ def main() -> int: args = parser.parse_args() if min(args.rounds, args.output_tokens) <= 0: raise SystemExit("rounds and output-tokens must be > 0") + if args.max_retained_tokens <= 0: + raise SystemExit("max-retained-tokens must be > 0") from kakeya import Client from transformers import AutoTokenizer @@ -247,7 +290,14 @@ def execute_agent(client, name, round_index, history, extra_metrics=None): return_dict=False, enable_thinking=False, ) - warm_tokens, warm = _infer(client, eos_ids, token_ids, 1, get_stats) + warm_tokens, warm = _infer( + client, + eos_ids, + token_ids, + 1, + get_stats, + max_retained_tokens=args.max_retained_tokens, + ) del warm_tokens generated, actual = _infer( client, @@ -256,8 +306,14 @@ def execute_agent(client, name, round_index, history, extra_metrics=None): args.output_tokens, get_stats, max_response_tokens=args.max_response_tokens, + max_retained_tokens=args.max_retained_tokens, + ) + text = decode_complete_response( + tokenizer, + name, + generated, + actual, ) - text = tokenizer.decode(generated, skip_special_tokens=True) delta = actual["delta"] ok = _agent_cache_gate(warm["delta"], delta) stage = { diff --git a/scripts/agent_gan_repl.py b/scripts/agent_gan_repl.py index 9597cc18..61d1d24a 100644 --- a/scripts/agent_gan_repl.py +++ b/scripts/agent_gan_repl.py @@ -3,6 +3,7 @@ from __future__ import annotations import argparse +import ast import atexit import difflib import hashlib @@ -15,7 +16,7 @@ import threading import time import uuid -from dataclasses import asdict, dataclass +from dataclasses import asdict, dataclass, field from datetime import datetime from enum import Enum from pathlib import Path @@ -24,6 +25,7 @@ _agent_cache_gate, _infer, build_critic_context, + decode_complete_response, ) from scripts.benchmark_prefill_architecture import ( _ensure_services, @@ -32,9 +34,17 @@ from inference_engine.bench.prefill_fleet_report import summarize_stages from autoresearch.prefill.lean_gate import ( LeanSignatureResult, - extract_lean_signature_blocks, + lean_theorem_signature_hash, + validate_lean_proof, validate_lean_signature, ) +from autoresearch.prefill.semantic_decompose import ( + SemanticUnitTooLarge, + admit_token_ids, + build_proof_step_interface, + downstream_output_cap, + serialize_proof_step_interface, +) class TimestampedTee: @@ -180,6 +190,204 @@ class ProofObligation: lean_signature: str = "" lean_signature_hash: str = "" formalization_error: str = "" + invalidation_kind: str = "" + quarantine_reason: str = "" + quarantine_root_id: str = "" + quarantine_run_id: str = "" + quarantine_prior_status: str = "" + quarantine_confidence: float = 0.0 + quarantine_evidence_type: str = "" + quarantine_evidence_source: str = "" + quarantine_auditor_run_id: str = "" + quarantine_proponent_run_id: str = "" + quarantine_reversible_status: str = "" + premise_review_status: str = "" + temporary_quarantine_reason: str = "" + temporary_quarantine_root_id: str = "" + temporary_quarantine_run_id: str = "" + invalidation_prior_status: str = "" + premise_audit_confidence: float = 0.0 + premise_audit_evidence_type: str = "" + premise_audit_evidence_source: str = "" + premise_auditor_run_id: str = "" + premise_proponent_run_id: str = "" + premise_review_reason: str = "" + decomposition_certificate_hash: str = "" + reduction_theorem_hash: str = "" + reduction_theorem_status: str = "" + decomposition_role_run_ids: dict = field(default_factory=dict) + dependency_labels: list[str] = field(default_factory=list) + dependency_ids: list[str] = field(default_factory=list) + certificate_reversible_status: str = "" + public_assumptions: list[str] = field(default_factory=list) + + +@dataclass +class NoGoLesson: + claim_hash: str + refuted_premise: str + evidence: str + source_obligation_id: str + run_id: str + confidence: float = 0.0 + evidence_type: str = "" + evidence_source: str = "" + auditor_run_id: str = "" + proponent_run_id: str = "" + reversible_status: str = "ACTIVE" + + +@dataclass(frozen=True) +class PremiseSuspicion: + obligation_id: str + premise: str + evidence_type: str + evidence_artifact: dict + critic_evidence: str + claim_schema: dict = field(default_factory=dict) + claim_hash: str = "" + target_lean_signature_hash: str = "" + + +@dataclass(frozen=True) +class PremiseAudit: + obligation_id: str + status: str + evidence_type: str + evidence_source: str + confidence: float + artifact: dict + analysis: str + run_id: str = "" + + +@dataclass(frozen=True) +class PremiseDefense: + obligation_id: str + status: str + correction: str + failure_reason: str + evidence: str + run_id: str = "" + + +@dataclass(frozen=True) +class PremiseReview: + status: str + verified: bool + confidence: float = 0.0 + evidence_type: str = "" + evidence_source: str = "" + auditor_run_id: str = "" + proponent_run_id: str = "" + reason: str = "" + + +@dataclass(frozen=True) +class DefinitionAudit: + target_obligation_id: str + parent_statement_hash: str + root_goal_hash: str + producer_role: str + producer_run_id: str + upstream_artifact_hashes: list[str] + definitions: list[dict] + missing_definitions: list[dict] + + +@dataclass(frozen=True) +class CounterexampleReport: + target_obligation_id: str + parent_statement_hash: str + root_goal_hash: str + producer_role: str + producer_run_id: str + upstream_artifact_hashes: list[str] + status: str + cases: list[dict] + + +@dataclass(frozen=True) +class DecompositionProposal: + target_obligation_id: str + parent_statement_hash: str + root_goal_hash: str + producer_role: str + producer_run_id: str + upstream_artifact_hashes: list[str] + parent_statement: str + children: list[dict] + dependency_edges: list[list[str]] + public_assumptions: list[str] + reduction_labels: list[str] + reduction_contract: str + + +@dataclass(frozen=True) +class FormalizationBundle: + target_obligation_id: str + parent_statement_hash: str + root_goal_hash: str + producer_role: str + producer_run_id: str + upstream_artifact_hashes: list[str] + math_ir: dict + parent_signature_source: str + parent_signature_hash: str + parent_newly_formalized: bool + children: list[dict] + reduction_theorem_source: str + reduction_signature_hash: str + + +@dataclass(frozen=True) +class ProofAttempt: + target_obligation_id: str + parent_statement_hash: str + root_goal_hash: str + producer_role: str + producer_run_id: str + upstream_artifact_hashes: list[str] + status: str + reduction_theorem_source: str + + +@dataclass(frozen=True) +class DefenseReport: + target_obligation_id: str + parent_statement_hash: str + root_goal_hash: str + producer_role: str + producer_run_id: str + upstream_artifact_hashes: list[str] + status: str + issues: list[str] + repairs: list[str] + + +@dataclass(frozen=True) +class JudgeDecision: + target_obligation_id: str + parent_statement_hash: str + root_goal_hash: str + producer_role: str + producer_run_id: str + upstream_artifact_hashes: list[str] + decision: str + reason: str + + +@dataclass +class DecompositionCertificateResult: + verified: bool + errors: list[str] + artifacts: dict + artifact_hashes: dict + transcripts: dict + role_run_ids: dict + validation: dict + created: list[ProofObligation] = field(default_factory=list) + certificate_hash: str = "" @dataclass @@ -188,6 +396,12 @@ class ProofObligationLedger: obligations: list[ProofObligation] version: int = 1 schema_version: int = 1 + no_go_lessons: list[NoGoLesson] | None = None + backjump_target_id: str = "" + + def __post_init__(self) -> None: + if self.no_go_lessons is None: + self.no_go_lessons = [] def save_proof_ledger(path: Path, ledger: ProofObligationLedger) -> None: @@ -202,6 +416,17 @@ def save_proof_ledger(path: Path, ledger: ProofObligationLedger) -> None: temporary.replace(path) +def save_decomposition_manifest(path: Path, payload: dict) -> None: + path.parent.mkdir(parents=True, exist_ok=True) + temporary = path.with_suffix(path.suffix + ".tmp") + temporary.write_text( + json.dumps(payload, ensure_ascii=False, indent=2), + encoding="utf-8", + ) + os.chmod(temporary, 0o600) + temporary.replace(path) + + def load_proof_ledger(path: Path) -> ProofObligationLedger | None: if not path.exists(): return None @@ -209,7 +434,14 @@ def load_proof_ledger(path: Path) -> ProofObligationLedger | None: obligations = [ ProofObligation(**item) for item in raw.pop("obligations", []) ] - ledger = ProofObligationLedger(obligations=obligations, **raw) + no_go_lessons = [ + NoGoLesson(**item) for item in (raw.pop("no_go_lessons", []) or []) + ] + ledger = ProofObligationLedger( + obligations=obligations, + no_go_lessons=no_go_lessons, + **raw, + ) obligation_ids = { item.obligation_id for item in ledger.obligations } @@ -218,6 +450,9 @@ def load_proof_ledger(path: Path) -> ProofObligationLedger | None: or not ledger.ledger_id or not ledger.obligations or len(obligation_ids) != len(ledger.obligations) + or len({ + lesson.claim_hash for lesson in ledger.no_go_lessons + }) != len(ledger.no_go_lessons) or any( item.parent_id and ( @@ -236,15 +471,46 @@ def pending_obligations( ) -> list[ProofObligation]: if ledger is None: return [] + by_id = { + item.obligation_id: item for item in ledger.obligations + } + + def has_invalid_ancestor(item: ProofObligation) -> bool: + cursor = item.parent_id + visited = set() + while cursor and cursor not in visited: + visited.add(cursor) + ancestor = by_id.get(cursor) + if ancestor is None: + break + if ( + ancestor.status == "QUARANTINED" + or ( + ancestor.status == "DISPROVED" + and ancestor.invalidation_kind in { + "PREMISE", + "PREMISE_INVALIDATED", + } + ) + ): + return True + cursor = ancestor.parent_id + return False + + eligible = { + item.obligation_id + for item in ledger.obligations + if item.status == "UNRESOLVED" and not has_invalid_ancestor(item) + } unresolved_parent_ids = { item.parent_id for item in ledger.obligations - if item.status == "UNRESOLVED" and item.parent_id + if item.obligation_id in eligible and item.parent_id } return [ item for item in ledger.obligations if ( - item.status == "UNRESOLVED" + item.obligation_id in eligible and item.obligation_id not in unresolved_parent_ids ) ] @@ -256,11 +522,11 @@ def format_proof_ledger( ) -> str: selected = obligations if obligations is not None else pending_obligations(ledger) ancestry = [] + by_id = { + item.obligation_id: item + for item in ledger.obligations + } if len(selected) == 1: - by_id = { - item.obligation_id: item - for item in ledger.obligations - } cursor = selected[0].parent_id visited = set() while cursor and cursor not in visited: @@ -275,26 +541,70 @@ def format_proof_ledger( f"- {item.obligation_id}: {item.statement}" for item in ancestry ) + relevant_ids = { + item.obligation_id for item in (*ancestry, *selected) + } + + def lesson_is_relevant(lesson: NoGoLesson) -> bool: + cursor = lesson.source_obligation_id + visited = set() + while cursor and cursor not in visited: + if cursor in relevant_ids: + return True + visited.add(cursor) + source = by_id.get(cursor) + if source is None: + break + cursor = source.parent_id + return False + items = "\n".join( f"- {item.obligation_id}" f"{f' (parent={item.parent_id})' if item.parent_id else ''}: " f"{item.statement}" + f"{f' [lean_signature_hash={item.lean_signature_hash}]' if item.lean_signature_hash else ''}" for item in selected ) + no_go_text = "\n".join( + f"- {lesson.claim_hash}: {lesson.refuted_premise}\n" + f" Evidence: {lesson.evidence}\n" + f" Verification: type={lesson.evidence_type or '(legacy)'} " + f"source={lesson.evidence_source or '(legacy)'} " + f"confidence={lesson.confidence:.2f} " + f"auditor={lesson.auditor_run_id or '(legacy)'} " + f"proponent={lesson.proponent_run_id or '(legacy)'}" + for lesson in ledger.no_go_lessons + if ( + lesson.reversible_status == "ACTIVE" + and lesson_is_relevant(lesson) + ) + ) return ( f"PROOF OBLIGATION LEDGER id={ledger.ledger_id} " f"version={ledger.version}\n" + f"BACKJUMP TARGET: {ledger.backjump_target_id or '(none)'}\n" + "NO-GO PREMISES (never assume, rename, or propose these):\n" + f"{no_go_text or '(none)'}\n" f"COMPLETE ANCESTOR CHAIN:\n{ancestry_text or '(root target)'}\n" f"CURRENT TARGET:\n{items}\n" "Generator requirement: emit `### ISSUE_RESPONSE ` for every " "pending ID, with `Correction:`, `Derivation:`, and `Remaining gap:`. " "Critic requirement: emit `### ISSUE_VERDICT ` for every pending " "ID, with `Status: PROVED|DISPROVED|UNRESOLVED`, `Evidence:`, and " - "`Missing lemma:`. For every UNRESOLVED verdict, immediately emit " - "`### LEAN_SIGNATURE ` followed by one fenced `lean` block. The " - "block must contain exactly one theorem with explicit typed variables, " - "hypotheses, and conclusion, ending in `:= by sorry`. Do not emit " - "imports, axioms, commands, macros, or executable code." + "`Missing lemma:`. A DISPROVED verdict must also emit " + "`Invalidation: APPROACH|PREMISE_SUSPECTED`. A premise suspicion must " + "also emit `Premise refuted:`, `Evidence type: " + "FINITE_COUNTEREXAMPLE|SYMBOLIC_CONTRADICTION|LEAN_PROOF|" + "PINNED_THEOREM`, and one-line JSON `Evidence artifact:` containing " + "exactly `claim`. Arithmetic claim fields are `schema_version:1`, " + "`quantifier:FOR_ALL`, `variables`, `domain`, `lhs`, the claimed " + "`relation`, and `rhs`; do not include a witness. Lean claims must " + "bind `contract:NEGATION_OF_TARGET_SIGNATURE` and the exact host " + "`lean_signature_hash`. Suspicion " + "starts independent audit and defense; it never directly invalidates " + "the premise. Use APPROACH when only the attempted derivation fails. " + "For an UNRESOLVED verdict, request exactly one frontier step. Do not " + "emit Lean; only the certified Formalizer and Prover may introduce Lean." ) @@ -308,43 +618,1686 @@ def format_proof_ledger( re.MULTILINE | re.DOTALL, ) +_PREMISE_AUDIT = re.compile( + r"^### PREMISE_AUDIT\s+(\S+)\s*$" + r"(?P.*?)(?=^### |\Z)", + re.MULTILINE | re.DOTALL, +) +_PREMISE_DEFENSE = re.compile( + r"^### PREMISE_DEFENSE\s+(\S+)\s*$" + r"(?P.*?)(?=^### |\Z)", + re.MULTILINE | re.DOTALL, +) +_VERIFIABLE_EVIDENCE_TYPES = { + "FINITE_COUNTEREXAMPLE", + "SYMBOLIC_CONTRADICTION", + "LEAN_PROOF", + "PINNED_THEOREM", +} + + +def _structured_field(body: str, name: str) -> str: + match = re.search( + rf"^\*{{0,2}}{re.escape(name)}:\*{{0,2}}[ \t]*(.*)$", + body, + re.MULTILINE, + ) + return match.group(1).strip() if match else "" + + +def _json_artifact(value: str) -> dict: + try: + artifact = json.loads(value) + except (TypeError, json.JSONDecodeError): + if not isinstance(value, str): + return {} + repaired = re.sub( + r'\\(?!(?:["\\/]|u[0-9a-fA-F]{4}))', + r"\\\\", + value, + ) + try: + artifact = json.loads(repaired) + except json.JSONDecodeError: + return {} + return artifact if isinstance(artifact, dict) else {} + + +def _normalize_arithmetic_expression( + expression: object, + variables: set[str], +) -> tuple[str, set[str]]: + if not isinstance(expression, str) or not expression.strip(): + raise ValueError("claim expression must be non-empty text") + tree = ast.parse(expression, mode="eval") + names = set() + for node in ast.walk(tree): + if isinstance(node, ast.Name): + if node.id not in variables: + raise ValueError(f"unknown claim variable: {node.id}") + names.add(node.id) + elif isinstance(node, ast.Constant): + if ( + not isinstance(node.value, (int, float)) + or isinstance(node.value, bool) + ): + raise ValueError("claim constants must be finite numbers") + elif isinstance(node, ( + ast.Expression, + ast.Load, + ast.UnaryOp, + ast.UAdd, + ast.USub, + ast.BinOp, + ast.Add, + ast.Sub, + ast.Mult, + ast.Div, + ast.Pow, + )): + continue + else: + raise ValueError("unsafe node in claim expression") + return ast.unparse(tree.body), names + + +def _normalize_claim_schema( + artifact: dict, + evidence_type: str, + *, + target_lean_signature_hash: str = "", +) -> tuple[dict, str]: + if set(artifact) != {"claim"} or not isinstance(artifact["claim"], dict): + raise ValueError("Critic artifact must contain exactly one claim object") + claim = artifact["claim"] + if evidence_type in { + "FINITE_COUNTEREXAMPLE", + "SYMBOLIC_CONTRADICTION", + }: + required = { + "schema_version", + "quantifier", + "variables", + "domain", + "lhs", + "relation", + "rhs", + } + if set(claim) != required: + raise ValueError("arithmetic claim schema fields are not exact") + variables_raw = claim["variables"] + if ( + not isinstance(variables_raw, list) + or not variables_raw + or any( + not isinstance(name, str) + or re.fullmatch(r"[A-Za-z_][A-Za-z0-9_]*", name) is None + for name in variables_raw + ) + or len(set(variables_raw)) != len(variables_raw) + ): + raise ValueError("quantified variables must be unique identifiers") + variables = set(variables_raw) + if ( + claim["schema_version"] != 1 + or claim["quantifier"] != "FOR_ALL" + or claim["domain"] not in {"INTEGER", "RATIONAL", "REAL"} + or claim["relation"] not in {"==", "!=", "<", "<=", ">", ">="} + ): + raise ValueError("unsupported universal arithmetic claim") + lhs, lhs_names = _normalize_arithmetic_expression( + claim["lhs"], + variables, + ) + rhs, rhs_names = _normalize_arithmetic_expression( + claim["rhs"], + variables, + ) + if lhs_names | rhs_names != variables: + raise ValueError("every quantified variable must occur in the claim") + normalized = { + "schema_version": 1, + "quantifier": "FOR_ALL", + "variables": sorted(variables), + "domain": claim["domain"], + "lhs": lhs, + "relation": claim["relation"], + "rhs": rhs, + } + elif evidence_type == "LEAN_PROOF": + required = { + "schema_version", + "contract", + "lean_signature_hash", + } + if set(claim) != required: + raise ValueError("Lean claim schema fields are not exact") + if ( + claim["schema_version"] != 1 + or claim["contract"] != "NEGATION_OF_TARGET_SIGNATURE" + or not target_lean_signature_hash + or claim["lean_signature_hash"] != target_lean_signature_hash + ): + raise ValueError("Lean claim is not bound to the target signature") + normalized = { + "schema_version": 1, + "contract": "NEGATION_OF_TARGET_SIGNATURE", + "lean_signature_hash": target_lean_signature_hash, + } + else: + if evidence_type != "PINNED_THEOREM": + raise ValueError("unsupported evidence type") + if not isinstance(claim, dict) or not claim: + raise ValueError("pinned theorem claim must be explicit") + normalized = json.loads( + json.dumps(claim, ensure_ascii=False, sort_keys=True), + ) + encoded = json.dumps( + normalized, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ) + return normalized, hashlib.sha256(encoded.encode()).hexdigest() + + +def extract_premise_suspicions( + critic_text: str, + allowed_ids: set[str], + target_lean_signature_hashes: dict[str, str] | None = None, +) -> dict[str, PremiseSuspicion]: + target_lean_signature_hashes = target_lean_signature_hashes or {} + suspicions = {} + for match in _ISSUE_VERDICT.finditer(critic_text): + obligation_id = _resolve_model_obligation_id( + match.group(1), + allowed_ids, + ) + if not obligation_id: + continue + body = match.group("body") + invalidation = _structured_field(body, "Invalidation") + if invalidation not in {"PREMISE_SUSPECTED", "PREMISE"}: + continue + premise = _structured_field(body, "Premise refuted") + evidence_type = _structured_field(body, "Evidence type").upper() + artifact = _json_artifact( + _structured_field(body, "Evidence artifact"), + ) + evidence = _structured_field(body, "Evidence") + try: + claim_schema, claim_hash = _normalize_claim_schema( + artifact, + evidence_type, + target_lean_signature_hash=target_lean_signature_hashes.get( + obligation_id, + "", + ), + ) + except ValueError: + claim_schema, claim_hash = {}, "" + if ( + not _canonical_claim(premise) + or evidence_type not in _VERIFIABLE_EVIDENCE_TYPES + or not artifact + or not claim_schema + or not claim_hash + or len(evidence) < 40 + ): + continue + suspicions[obligation_id] = PremiseSuspicion( + obligation_id, + premise, + evidence_type, + {"claim": claim_schema}, + evidence, + claim_schema, + claim_hash, + target_lean_signature_hashes.get(obligation_id, ""), + ) + return suspicions + + +def parse_premise_audit( + text: str, + obligation_id: str, + run_id: str = "", +) -> PremiseAudit | None: + for match in _PREMISE_AUDIT.finditer(text): + if match.group(1) != obligation_id: + continue + body = match.group("body") + status = _structured_field(body, "Status") + evidence_type = _structured_field(body, "Evidence type").upper() + evidence_source = _structured_field(body, "Evidence source") + analysis = _structured_field(body, "Analysis") + artifact = _json_artifact(_structured_field(body, "Artifact")) + try: + confidence = float(_structured_field(body, "Confidence")) + except ValueError: + return None + if ( + status not in {"CONFIRMED", "NOT_CONFIRMED", "INCONCLUSIVE"} + or evidence_type not in _VERIFIABLE_EVIDENCE_TYPES + or not evidence_source + or not 0.0 <= confidence <= 1.0 + or not analysis + ): + return None + return PremiseAudit( + obligation_id, + status, + evidence_type, + evidence_source, + confidence, + artifact, + analysis, + run_id, + ) + return None + + +def parse_premise_defense( + text: str, + obligation_id: str, + run_id: str = "", +) -> PremiseDefense | None: + for match in _PREMISE_DEFENSE.finditer(text): + if match.group(1) != obligation_id: + continue + body = match.group("body") + status = _structured_field(body, "Status") + correction = _structured_field(body, "Correction") + failure_reason = _structured_field(body, "Failure reason") + evidence = _structured_field(body, "Evidence") + if ( + status not in {"RESCUED", "NOT_RESCUED", "INCONCLUSIVE"} + or not evidence + or (status == "RESCUED" and not correction) + or (status == "NOT_RESCUED" and not failure_reason) + ): + return None + return PremiseDefense( + obligation_id, + status, + correction, + failure_reason, + evidence, + run_id, + ) + return None + + +def build_premise_auditor_messages( + goal: str, + suspicion: PremiseSuspicion, +) -> list[dict[str, str]]: + package = json.dumps(asdict(suspicion), ensure_ascii=False, sort_keys=True) + return [{ + "role": "system", + "content": ( + "You are an isolated Premise Auditor. Independently attack the " + "named premise using counterexamples, exact definitions and " + "quantifiers, theorem conflicts, and verifiable Lean, finite, or " + "symbolic evidence. Do not trust the Critic conclusion. Return " + "`### PREMISE_AUDIT ` with `Status: " + "CONFIRMED|NOT_CONFIRMED|INCONCLUSIVE`, `Evidence type:`, " + "`Evidence source:`, `Confidence:` in [0,1], one-line JSON " + "`Artifact:`, and one-line `Analysis:`. For arithmetic, Artifact " + "must contain exactly the host `claim_hash`, unchanged `claim`, " + "and a `witness` binding every quantified variable. The witness " + "must make the Critic's claimed relation false. For Lean, preserve " + "the exact claim/signature hashes and negation contract." + ), + }, { + "role": "user", + "content": ( + f"IMMUTABLE RESEARCH GOAL:\n{goal}\n\n" + f"HOST-PACKAGED CRITIC SUSPICION:\n{package}" + ), + }] + + +def build_premise_proponent_messages( + goal: str, + suspicion: PremiseSuspicion, + auditor_text: str, +) -> list[dict[str, str]]: + package = json.dumps(asdict(suspicion), ensure_ascii=False, sort_keys=True) + return [{ + "role": "system", + "content": ( + "You are an isolated Adversarial Proponent. Attempt to rescue the " + "premise by finding the exact domain, topology, or quantifier " + "correction, or by refuting the Auditor artifact. Return `### " + "PREMISE_DEFENSE ` with `Status: " + "RESCUED|NOT_RESCUED|INCONCLUSIVE`, `Correction:`, `Failure " + "reason:`, and one-line `Evidence:`." + ), + }, { + "role": "user", + "content": ( + f"IMMUTABLE RESEARCH GOAL:\n{goal}\n\n" + f"HOST-PACKAGED CRITIC SUSPICION:\n{package}\n\n" + f"COMPLETE ISOLATED AUDITOR OUTPUT:\n{auditor_text}" + ), + }] + + +def run_isolated_premise_review( + goal: str, + suspicion: PremiseSuspicion, + run_role, +) -> tuple[PremiseAudit | None, PremiseDefense | None, dict]: + transcripts = {"auditor": "", "proponent": ""} + auditor_run_id = "" + try: + auditor_text, auditor_run_id = run_role( + "premise_auditor", + build_premise_auditor_messages(goal, suspicion), + ) + transcripts["auditor"] = auditor_text + except Exception as exc: + transcripts["auditor"] = ( + f"AUDITOR EXECUTION FAILED: {type(exc).__name__}: {exc}" + ) + audit = parse_premise_audit( + transcripts["auditor"], + suspicion.obligation_id, + auditor_run_id, + ) + proponent_run_id = "" + try: + proponent_text, proponent_run_id = run_role( + "adversarial_proponent", + build_premise_proponent_messages( + goal, + suspicion, + transcripts["auditor"], + ), + ) + transcripts["proponent"] = proponent_text + except Exception as exc: + transcripts["proponent"] = ( + f"PROPONENT EXECUTION FAILED: {type(exc).__name__}: {exc}" + ) + defense = parse_premise_defense( + transcripts["proponent"], + suspicion.obligation_id, + proponent_run_id, + ) + transcripts["auditor_run_id"] = auditor_run_id + transcripts["proponent_run_id"] = proponent_run_id + return audit, defense, transcripts + + +def _safe_arithmetic(expression: str, substitutions: dict) -> float: + allowed_names = { + str(key): float(value) + for key, value in substitutions.items() + if isinstance(value, (int, float)) and not isinstance(value, bool) + } + if len(allowed_names) != len(substitutions): + raise ValueError("substitutions must be finite numbers") + tree = ast.parse(expression, mode="eval") + + def evaluate(node) -> float: + if isinstance(node, ast.Expression): + return evaluate(node.body) + if ( + isinstance(node, ast.Constant) + and isinstance(node.value, (int, float)) + and not isinstance(node.value, bool) + ): + return float(node.value) + if isinstance(node, ast.Name) and node.id in allowed_names: + return allowed_names[node.id] + if isinstance(node, ast.UnaryOp) and isinstance( + node.op, + (ast.UAdd, ast.USub), + ): + value = evaluate(node.operand) + return value if isinstance(node.op, ast.UAdd) else -value + if isinstance(node, ast.BinOp) and isinstance( + node.op, + (ast.Add, ast.Sub, ast.Mult, ast.Div, ast.Pow), + ): + left = evaluate(node.left) + right = evaluate(node.right) + if isinstance(node.op, ast.Add): + return left + right + if isinstance(node.op, ast.Sub): + return left - right + if isinstance(node.op, ast.Mult): + return left * right + if isinstance(node.op, ast.Div): + return left / right + if abs(right) > 12: + raise ValueError("exponent is too large") + return left ** right + raise ValueError("unsafe arithmetic expression") + + result = evaluate(tree) + if not (-1e100 < result < 1e100): + raise ValueError("non-finite arithmetic result") + return result + + +def validate_evidence_artifact( + audit: PremiseAudit, + *, + suspicion: PremiseSuspicion, + project_root: Path, + lean_validator=validate_lean_proof, +) -> tuple[bool, str]: + artifact = audit.artifact + if audit.evidence_type != suspicion.evidence_type: + return False, "Auditor evidence type differs from the bound Critic claim" + if audit.evidence_type in { + "FINITE_COUNTEREXAMPLE", + "SYMBOLIC_CONTRADICTION", + }: + try: + if set(artifact) != {"claim_hash", "claim", "witness"}: + raise ValueError("Auditor artifact fields are not exact") + normalized, claim_hash = _normalize_claim_schema( + {"claim": artifact["claim"]}, + audit.evidence_type, + ) + if ( + normalized != suspicion.claim_schema + or claim_hash != suspicion.claim_hash + or artifact["claim_hash"] != suspicion.claim_hash + ): + raise ValueError("Auditor claim or claim hash was tampered") + witness = artifact["witness"] + variables = set(normalized["variables"]) + if not isinstance(witness, dict) or set(witness) != variables: + raise ValueError("witness must bind every quantified variable") + if normalized["domain"] == "INTEGER" and any( + not isinstance(value, int) or isinstance(value, bool) + for value in witness.values() + ): + raise ValueError("integer claim requires integer witnesses") + left = _safe_arithmetic(normalized["lhs"], witness) + right = _safe_arithmetic(normalized["rhs"], witness) + relation = normalized["relation"] + except (KeyError, TypeError, ValueError, ZeroDivisionError) as exc: + return False, f"uncheckable arithmetic artifact: {exc}" + tolerance = 1e-9 * max(1.0, abs(left), abs(right)) + relations = { + "==": abs(left - right) <= tolerance, + "!=": abs(left - right) > tolerance, + "<": left < right, + "<=": left <= right, + ">": left > right, + ">=": left >= right, + } + claimed_relation_holds = relations.get(relation) + if claimed_relation_holds is None: + return False, "unsupported claimed relation" + return ( + not claimed_relation_holds, + "host found counterexample: claimed relation evaluated " + f"{left} {relation} {right} as {claimed_relation_holds}", + ) + if audit.evidence_type == "LEAN_PROOF": + try: + if set(artifact) != { + "claim_hash", + "claim", + "lean_signature_hash", + "contract", + "source", + }: + raise ValueError("Lean Auditor artifact fields are not exact") + normalized, claim_hash = _normalize_claim_schema( + {"claim": artifact["claim"]}, + "LEAN_PROOF", + target_lean_signature_hash=( + suspicion.target_lean_signature_hash + ), + ) + if ( + normalized != suspicion.claim_schema + or claim_hash != suspicion.claim_hash + or artifact["claim_hash"] != suspicion.claim_hash + or artifact["lean_signature_hash"] + != suspicion.target_lean_signature_hash + or artifact["contract"] != "NEGATION_OF_TARGET_SIGNATURE" + ): + raise ValueError("Lean proof contract or hash was tampered") + except (KeyError, TypeError, ValueError) as exc: + return False, f"uncheckable Lean artifact: {exc}" + return False, ( + "target signature hash is bound, but the stored Lean signature " + "cannot be safely transformed into an exact negation wrapper; " + "the complete proof is recorded but not accepted" + ) + return False, ( + "pinned theorem references are recorded but no trusted local theorem " + "registry validates their exact assumptions" + ) + + +def decide_premise_review( + audit: PremiseAudit | None, + defense: PremiseDefense | None, + *, + project_root: Path, + lean_validator=validate_lean_proof, + suspicion: PremiseSuspicion | None = None, +) -> PremiseReview: + if audit is None or defense is None: + return PremiseReview("INCONCLUSIVE", False, reason="missing role output") + common = { + "confidence": audit.confidence, + "evidence_type": audit.evidence_type, + "evidence_source": audit.evidence_source, + "auditor_run_id": audit.run_id, + "proponent_run_id": defense.run_id, + } + if audit.status == "NOT_CONFIRMED": + return PremiseReview( + "NOT_CONFIRMED", + False, + reason=audit.analysis, + **common, + ) + if defense.status == "RESCUED": + return PremiseReview( + "RESCUED", + False, + reason=defense.correction, + **common, + ) + if ( + audit.status != "CONFIRMED" + or defense.status != "NOT_RESCUED" + or audit.confidence < 0.8 + ): + return PremiseReview( + "INCONCLUSIVE", + False, + reason="role agreement or confidence threshold not met", + **common, + ) + if suspicion is None: + return PremiseReview( + "INCONCLUSIVE", + False, + reason="host-bound Critic claim schema is missing", + **common, + ) + if suspicion is not None and ( + audit.obligation_id != suspicion.obligation_id + or defense.obligation_id != suspicion.obligation_id + ): + return PremiseReview( + "INCONCLUSIVE", + False, + reason="artifact is not bound to the exact suspected premise", + **common, + ) + verified, reason = validate_evidence_artifact( + audit, + suspicion=suspicion, + project_root=project_root, + lean_validator=lean_validator, + ) + return PremiseReview( + "PREMISE_INVALIDATED" if verified else "INCONCLUSIVE", + verified, + reason=reason, + **common, + ) + + +_CERTIFIED_ARTIFACT_TYPES = { + "DEFINITION_AUDIT": (DefinitionAudit, "definition_auditor"), + "COUNTEREXAMPLE_REPORT": ( + CounterexampleReport, + "counterexample_worker", + ), + "DECOMPOSITION_PROPOSAL": ( + DecompositionProposal, + "decomposer", + ), + "FORMALIZATION_BUNDLE": ( + FormalizationBundle, + "formalizer", + ), + "PROOF_ATTEMPT": (ProofAttempt, "prover"), + "DEFENSE_REPORT": (DefenseReport, "adversarial_proponent"), + "JUDGE_DECISION": (JudgeDecision, "judge"), +} + + +def _canonical_json_hash(value) -> str: + encoded = json.dumps( + value, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ) + return hashlib.sha256(encoded.encode()).hexdigest() + + +def parse_certified_artifact( + text: str, + heading: str, + *, + target_obligation_id: str, + parent_statement_hash: str, + root_goal_hash: str, + producer_run_id: str, + upstream_artifact_hashes: list[str], +): + artifact_type, producer_role = _CERTIFIED_ARTIFACT_TYPES[heading] + match = re.search( + rf"^### {re.escape(heading)}\s*$" + r"(?P.*?)(?=^### |\Z)", + text, + re.MULTILINE | re.DOTALL, + ) + if match is None: + return None, f"missing {heading}" + payload = _json_artifact(_structured_field(match.group("body"), "Artifact")) + if not payload: + return None, f"malformed {heading} Artifact JSON" + host_bindings = { + "target_obligation_id": target_obligation_id, + "parent_statement_hash": parent_statement_hash, + "root_goal_hash": root_goal_hash, + "producer_role": producer_role, + "producer_run_id": producer_run_id, + "upstream_artifact_hashes": upstream_artifact_hashes, + } + if any( + key in payload and payload[key] != value + for key, value in host_bindings.items() + ): + return None, f"tampered {heading} bindings" + payload = {**host_bindings, **payload} + try: + artifact = artifact_type(**payload) + except (TypeError, ValueError) as exc: + return None, f"invalid {heading} fields: {exc}" + bindings = ( + artifact.target_obligation_id == target_obligation_id + and artifact.parent_statement_hash == parent_statement_hash + and artifact.root_goal_hash == root_goal_hash + and artifact.producer_role == producer_role + and artifact.producer_run_id == producer_run_id + and artifact.upstream_artifact_hashes == upstream_artifact_hashes + ) + if not bindings: + return None, f"tampered {heading} bindings" + if ( + isinstance(artifact, CounterexampleReport) + and artifact.status not in { + "COUNTEREXAMPLE_FOUND", + "NO_COUNTEREXAMPLE", + "INCONCLUSIVE", + } + ) or ( + isinstance(artifact, ProofAttempt) + and artifact.status not in {"PROVED", "FAILED", "INCONCLUSIVE"} + ) or ( + isinstance(artifact, DefenseReport) + and artifact.status not in { + "DEFENDED", + "REJECTED", + "INCONCLUSIVE", + } + ) or ( + isinstance(artifact, JudgeDecision) + and artifact.decision not in { + "ACCEPT", + "REJECT", + "INCONCLUSIVE", + } + ): + return None, f"invalid {heading} status" + return artifact, "" + + +def _certified_role_messages( + role: str, + heading: str, + package: dict, +) -> list[dict[str, str]]: + behavior = { + "definition_auditor": ( + "Inventory every symbol, domain, quantifier, topology, convergence " + "notion, and dependency. Missing definitions become precise " + "definition obligations." + ), + "counterexample_worker": ( + "Attack the exact typed claim with finite, limiting, boundary, " + "and theorem-conflict cases. Unsupported citations are untrusted." + ), + "decomposer": ( + "Propose labeled child propositions, public assumptions, acyclic " + "dependency edges, and an explicit conjunction-to-parent reduction." + ), + "formalizer": ( + "Emit typed Math IR, exact parent and child Lean signatures, and a " + "reduction theorem signature scaffold. Never replace a bound parent." + ), + "prover": ( + "Produce one complete Lean proof of the exact reduction theorem. " + "No sorry, admit, axioms, unsafe commands, or placeholders." + ), + "adversarial_proponent": ( + "Attack circularity, missing definitions, disconnected children, " + "and insufficient reduction; repairs are advisory only." + ), + "judge": ( + "Decide ACCEPT|REJECT|INCONCLUSIVE using only the host-verified " + "manifest. You cannot override a failed host gate." + ), + }[role] + artifact_schema = { + "definition_auditor": ( + '{"definitions":[{"symbol":"...","type":"...","scope":"..."}],' + '"missing_definitions":[{"obligation_label":"L1","symbol":"...",' + '"required_type":"..."}]}' + ), + "counterexample_worker": ( + '{"status":"COUNTEREXAMPLE_FOUND|NO_COUNTEREXAMPLE|INCONCLUSIVE",' + '"cases":[]}' + ), + "decomposer": ( + '{"parent_statement":"","children":[{"label":"L1",' + '"statement":"...","kind":"DEFINITION|LEMMA"}],' + '"dependency_edges":[],"public_assumptions":[],' + '"reduction_labels":["L1"],"reduction_contract":"L1 and A imply P"}' + ), + "formalizer": ( + '{"math_ir":{"parent_signature_hash":"...","parent_proposition_hash":' + '"...","child_labels":["L1"],"public_assumptions":[],' + '"reduction_labels":["L1"]},"parent_signature_source":"...",' + '"parent_signature_hash":"...","parent_newly_formalized":true,' + '"children":[{"label":"L1","statement":"...",' + '"lean_signature":"...","lean_signature_hash":"..."}],' + '"reduction_theorem_source":"...","reduction_signature_hash":"..."}' + ), + "prover": ( + '{"status":"PROVED|FAILED|INCONCLUSIVE",' + '"reduction_theorem_source":"..."}' + ), + "adversarial_proponent": ( + '{"status":"DEFENDED|REJECTED|INCONCLUSIVE",' + '"issues":[],"repairs":[]}' + ), + "judge": ( + '{"decision":"ACCEPT|REJECT|INCONCLUSIVE","reason":"..."}' + ), + }[role] + return [{ + "role": "system", + "content": ( + f"You are the isolated {role}. {behavior} Return exactly `### " + f"{heading}` followed by one-line `Artifact:` JSON. Emit only the " + f"role fields in this schema: {artifact_schema} Host bindings are " + "attached automatically; if emitted, they must match the package." + ), + }, { + "role": "user", + "content": json.dumps(package, ensure_ascii=False, sort_keys=True), + }] + + +def _required_certified_upstream(role: str) -> set[str]: + return { + "definition_auditor": set(), + "counterexample_worker": {"definition_auditor"}, + "decomposer": { + "definition_auditor", + "counterexample_worker", + }, + "formalizer": {"decomposer"}, + "prover": {"formalizer"}, + "adversarial_proponent": { + "decomposer", + "formalizer", + "prover", + }, + }[role] + + +def _validate_dependency_graph( + proposal: DecompositionProposal, +) -> list[str]: + errors = [] + labels = [ + str(child.get("label", "")) + for child in proposal.children + if isinstance(child, dict) + ] + if ( + not labels + or any(not label for label in labels) + or len(set(labels)) != len(labels) + ): + return ["child labels must be non-empty and unique"] + if len(labels) != 1: + return ["one-step decomposition requires exactly one child"] + if set(proposal.reduction_labels) != set(labels): + errors.append("every child must be reachable in the reduction contract") + graph = {label: set() for label in labels} + for edge in proposal.dependency_edges: + if ( + not isinstance(edge, list) + or len(edge) != 2 + or edge[0] not in graph + or edge[1] not in graph + ): + errors.append("dependency edge references an invalid child label") + continue + if edge[0] == edge[1]: + errors.append("child dependency graph must be acyclic") + continue + graph[edge[0]].add(edge[1]) + visiting = set() + visited = set() + + def visit(label: str) -> bool: + if label in visiting: + return False + if label in visited: + return True + visiting.add(label) + if any(not visit(dependency) for dependency in graph[label]): + return False + visiting.remove(label) + visited.add(label) + return True + + if any(not visit(label) for label in labels): + errors.append("child dependency graph must be acyclic") + return errors + + +def _validate_counterexample_report( + report: CounterexampleReport, + *, + project_root: Path, +) -> list[dict]: + validations = [] + for case in report.cases: + if not isinstance(case, dict): + validations.append({"verified": False, "error": "malformed case"}) + continue + evidence_type = str(case.get("evidence_type", "")) + if evidence_type in { + "FINITE_COUNTEREXAMPLE", + "SYMBOLIC_CONTRADICTION", + }: + try: + claim, claim_hash = _normalize_claim_schema( + {"claim": case["claim"]}, + evidence_type, + ) + suspicion = PremiseSuspicion( + report.target_obligation_id, + "Host-bound counterexample case", + evidence_type, + {"claim": claim}, + "Counterexample worker artifact", + claim, + claim_hash, + ) + audit = PremiseAudit( + report.target_obligation_id, + "CONFIRMED", + evidence_type, + str(case.get("evidence_source", "")), + 1.0, + { + "claim_hash": claim_hash, + "claim": claim, + "witness": case["witness"], + }, + "Deterministic counterexample validation.", + ) + verified, error = validate_evidence_artifact( + audit, + suspicion=suspicion, + project_root=project_root, + ) + except (KeyError, TypeError, ValueError) as exc: + verified, error = False, str(exc) + elif evidence_type == "PINNED_THEOREM": + verified, error = ( + False, + "unsupported theorem citation has no trusted local registry", + ) + else: + verified, error = False, "unsupported evidence type" + validations.append({ + "evidence_type": evidence_type, + "verified": verified, + "error": error, + }) + return validations + + +def _validate_decomposition_certificate( + ledger: ProofObligationLedger, + parent: ProofObligation, + definition_audit: DefinitionAudit, + counterexamples: CounterexampleReport, + proposal: DecompositionProposal, + formalization: FormalizationBundle, + proof: ProofAttempt, + defense: DefenseReport, + *, + project_root: Path, + signature_validator=validate_lean_signature, + proof_validator=validate_lean_proof, +) -> tuple[dict, list[str]]: + errors = _validate_dependency_graph(proposal) + validation = { + "graph_valid": not errors, + "parent_signature_valid": False, + "children_valid": False, + "reduction_signature_valid": False, + "reduction_proof_valid": False, + "defense_nonblocking": defense.status in { + "DEFENDED", + "INCONCLUSIVE", + }, + } + validation["definition_inventory_nonempty"] = bool( + definition_audit.definitions + or definition_audit.missing_definitions + ) + if not validation["definition_inventory_nonempty"]: + errors.append("definition inventory is empty") + validation["counterexample_cases"] = _validate_counterexample_report( + counterexamples, + project_root=project_root, + ) + verified_counterexample = ( + counterexamples.status == "COUNTEREXAMPLE_FOUND" + and any( + item["verified"] + for item in validation["counterexample_cases"] + ) + ) + validation["verified_parent_counterexample"] = verified_counterexample + if ( + counterexamples.status == "COUNTEREXAMPLE_FOUND" + and not verified_counterexample + ): + errors.append("claimed counterexample has no verified evidence") + elif verified_counterexample: + errors.append( + "verified counterexample refutes the parent; decomposition is " + "forbidden and premise review is required", + ) + proposal_labels = { + str(child.get("label", "")): child + for child in proposal.children + if isinstance(child, dict) + } + definition_children = { + label + for label, child in proposal_labels.items() + if child.get("kind") == "DEFINITION" + } + required_definition_labels = { + str(item.get("obligation_label", "")) + for item in definition_audit.missing_definitions + if isinstance(item, dict) + } + if ( + "" in required_definition_labels + or not required_definition_labels.issubset(definition_children) + ): + errors.append( + "every missing definition must become a labeled definition child", + ) + formal_children = { + str(child.get("label", "")): child + for child in formalization.children + if isinstance(child, dict) + } + parent_signature_text = " ".join( + formalization.parent_signature_source.split(), + ).split(" := by", 1)[0] + reduction_signature_text = " ".join( + formalization.reduction_theorem_source.split(), + ).split(" := by", 1)[0] + parent_conclusion = ( + parent_signature_text.rsplit(" : ", 1)[-1] + if " : " in parent_signature_text else "" + ) + reduction_conclusion = ( + reduction_signature_text.rsplit(" : ", 1)[-1] + if " : " in reduction_signature_text else "" + ) + parent_proposition_hash = ( + hashlib.sha256(parent_conclusion.encode()).hexdigest() + if parent_conclusion else "" + ) + if set(formal_children) != set(proposal_labels): + errors.append("formalized child labels differ from proposal") + if ( + formalization.math_ir.get("parent_signature_hash") + != formalization.parent_signature_hash + or formalization.math_ir.get("parent_proposition_hash") + != parent_proposition_hash + or set(formalization.math_ir.get("child_labels", [])) + != set(proposal_labels) + or formalization.math_ir.get("public_assumptions") + != proposal.public_assumptions + or set(formalization.math_ir.get("reduction_labels", [])) + != set(proposal.reduction_labels) + ): + errors.append("typed Math IR does not bind the exact reduction contract") + if not parent_conclusion or reduction_conclusion != parent_conclusion: + errors.append( + "reduction theorem conclusion differs from exact parent proposition", + ) + if formalization.parent_signature_hash != parent.lean_signature_hash and ( + parent.formal_status != "UNFORMALIZED" + ): + errors.append("existing parent signature hash mismatch") + parent_result = signature_validator( + formalization.parent_signature_source, + project_root=project_root, + ) + if not parent_result.ok: + errors.append(f"parent signature failed: {parent_result.error}") + elif parent.formal_status == "UNFORMALIZED": + if not formalization.parent_newly_formalized: + errors.append("new parent signature was not declared") + elif parent_result.signature_hash != formalization.parent_signature_hash: + errors.append("new parent signature hash mismatch") + else: + validation["parent_signature_valid"] = True + elif ( + formalization.parent_newly_formalized + or parent_result.signature_hash != parent.lean_signature_hash + or formalization.parent_signature_source != parent.lean_signature + ): + errors.append("existing parent signature cannot be replaced") + else: + validation["parent_signature_valid"] = True + child_results = {} + proposed_items = list(proposal_labels.items()) + for index, (left_label, left_child) in enumerate(proposed_items): + for right_label, right_child in proposed_items[index + 1:]: + equivalent, _score = _semantic_equivalence( + str(left_child.get("statement", "")), + str(right_child.get("statement", "")), + ) + if equivalent: + errors.append( + f"children {left_label} and {right_label} are redundant", + ) + for label, child in formal_children.items(): + source = str(child.get("lean_signature", "")) + result = signature_validator(source, project_root=project_root) + child_results[label] = result + if not result.ok: + errors.append(f"child {label} signature failed: {result.error}") + elif child.get("lean_signature_hash") != result.signature_hash: + errors.append(f"child {label} signature hash mismatch") + if str(child.get("statement", "")) != str( + proposal_labels.get(label, {}).get("statement", ""), + ): + errors.append(f"child {label} statement changed during formalization") + reason = _frontier_rejection_reason( + ledger, + parent.obligation_id, + str(child.get("statement", "")), + ) + if reason: + errors.append(f"child {label} rejected: {reason}") + validation["children_valid"] = bool(child_results) and all( + result.ok for result in child_results.values() + ) + reduction_signature = signature_validator( + formalization.reduction_theorem_source, + project_root=project_root, + ) + if ( + not reduction_signature.ok + or reduction_signature.signature_hash + != formalization.reduction_signature_hash + ): + errors.append("reduction theorem signature failed or changed") + else: + validation["reduction_signature_valid"] = True + proof_result = proof_validator( + proof.reduction_theorem_source, + project_root=project_root, + ) + if ( + proof.status != "PROVED" + or not proof_result.ok + or proof_result.status != "PROVED" + or lean_theorem_signature_hash(proof.reduction_theorem_source) + != formalization.reduction_signature_hash + ): + errors.append("complete reduction proof failed or targets another theorem") + else: + validation["reduction_proof_valid"] = True + if defense.status == "REJECTED": + errors.append("adversarial defense found a blocking defect") + validation["child_signature_hashes"] = { + label: result.signature_hash + for label, result in child_results.items() + if result.ok + } + validation["reduction_proof_hash"] = ( + proof_result.signature_hash if proof_result.ok else "" + ) + validation["host_gates_passed"] = not errors + return validation, errors + + +def run_certified_decomposition( + ledger: ProofObligationLedger, + target_id: str, + root_goal: str, + run_role, + *, + project_root: Path, + orchestration_id: str, + signature_validator=validate_lean_signature, + proof_validator=validate_lean_proof, +) -> DecompositionCertificateResult: + parent = next( + item for item in ledger.obligations + if item.obligation_id == target_id + ) + statement_hash = hashlib.sha256(parent.statement.encode()).hexdigest() + goal_hash = hashlib.sha256(root_goal.encode()).hexdigest() + artifacts = {} + hashes = {} + transcripts = {} + role_run_ids = {} + errors = [] + role_specs = [ + ("definition_auditor", "DEFINITION_AUDIT"), + ("counterexample_worker", "COUNTEREXAMPLE_REPORT"), + ("decomposer", "DECOMPOSITION_PROPOSAL"), + ("formalizer", "FORMALIZATION_BUNDLE"), + ("prover", "PROOF_ATTEMPT"), + ("adversarial_proponent", "DEFENSE_REPORT"), + ] + for role, heading in role_specs: + expected_run_id = f"{orchestration_id}:{role}" + upstream = list(hashes.values()) + package = { + "target_obligation_id": target_id, + "parent_statement": parent.statement, + "parent_statement_hash": statement_hash, + "root_goal": root_goal, + "root_goal_hash": goal_hash, + "producer_role": role, + "producer_run_id": expected_run_id, + "upstream_artifact_hashes": upstream, + "validated_upstream_artifacts": { + name: asdict(value) + for name, value in artifacts.items() + if name in _required_certified_upstream(role) + }, + "parent_formal_status": parent.formal_status, + "parent_lean_signature": parent.lean_signature, + "parent_lean_signature_hash": parent.lean_signature_hash, + } + try: + text, actual_run_id = run_role( + role, + _certified_role_messages(role, heading, package), + expected_run_id, + ) + except Exception as exc: + errors.append(f"{role} failed: {type(exc).__name__}: {exc}") + break + transcripts[role] = text + role_run_ids[role] = actual_run_id + if actual_run_id != expected_run_id: + errors.append(f"{role} run ID mismatch") + break + artifact, error = parse_certified_artifact( + text, + heading, + target_obligation_id=target_id, + parent_statement_hash=statement_hash, + root_goal_hash=goal_hash, + producer_run_id=expected_run_id, + upstream_artifact_hashes=upstream, + ) + if error: + errors.append(error) + break + artifacts[role] = artifact + hashes[role] = _canonical_json_hash(asdict(artifact)) + validation = {"host_gates_passed": False} + if not errors and len(artifacts) == 6: + validation, errors = _validate_decomposition_certificate( + ledger, + parent, + artifacts["definition_auditor"], + artifacts["counterexample_worker"], + artifacts["decomposer"], + artifacts["formalizer"], + artifacts["prover"], + artifacts["adversarial_proponent"], + project_root=project_root, + signature_validator=signature_validator, + proof_validator=proof_validator, + ) + judge_manifest = { + "target_obligation_id": target_id, + "parent_statement": parent.statement, + "parent_statement_hash": statement_hash, + "root_goal_hash": goal_hash, + "artifact_hashes": hashes, + "validation": validation, + "errors": errors, + "retained_child_statements": [ + child.get("statement", "") + for child in ( + artifacts.get("decomposer").children + if artifacts.get("decomposer") else [] + ) + ], + } + manifest_hash = _canonical_json_hash(judge_manifest) + if len(artifacts) == 6: + role = "judge" + heading = "JUDGE_DECISION" + expected_run_id = f"{orchestration_id}:{role}" + package = { + **judge_manifest, + "producer_role": role, + "producer_run_id": expected_run_id, + "upstream_artifact_hashes": [manifest_hash], + } + try: + text, actual_run_id = run_role( + role, + _certified_role_messages(role, heading, package), + expected_run_id, + ) + transcripts[role] = text + role_run_ids[role] = actual_run_id + judge, error = parse_certified_artifact( + text, + heading, + target_obligation_id=target_id, + parent_statement_hash=statement_hash, + root_goal_hash=goal_hash, + producer_run_id=expected_run_id, + upstream_artifact_hashes=[manifest_hash], + ) + if error: + errors.append(error) + else: + artifacts[role] = judge + hashes[role] = _canonical_json_hash(asdict(judge)) + if judge.decision != "ACCEPT": + errors.append(f"Judge decision was {judge.decision}") + except Exception as exc: + errors.append(f"judge failed: {type(exc).__name__}: {exc}") + verified = bool(validation.get("host_gates_passed")) and not errors + certificate_hash = _canonical_json_hash({ + "orchestration_id": orchestration_id, + "artifact_hashes": hashes, + "validation": validation, + }) + return DecompositionCertificateResult( + verified, + errors, + artifacts, + hashes, + transcripts, + role_run_ids, + validation, + certificate_hash=certificate_hash, + ) + + +def persist_verified_decomposition( + ledger: ProofObligationLedger, + target_id: str, + result: DecompositionCertificateResult, + run_id: str, +) -> list[ProofObligation]: + if not result.verified: + return [] + parent = next( + item for item in ledger.obligations + if item.obligation_id == target_id + ) + proposal: DecompositionProposal = result.artifacts["decomposer"] + formalization: FormalizationBundle = result.artifacts["formalizer"] + formal_by_label = { + str(child["label"]): child + for child in formalization.children + } + if parent.formal_status == "UNFORMALIZED": + parent.formal_status = "FORMALIZED" + parent.lean_signature = formalization.parent_signature_source + parent.lean_signature_hash = formalization.parent_signature_hash + label_to_id = { + str(child["label"]): ( + f"{target_id}-" + + hashlib.sha256( + f"{result.certificate_hash}:{child['label']}".encode(), + ).hexdigest()[:10] + ) + for child in proposal.children + } + dependencies = { + label: [] for label in label_to_id + } + for source, dependency in proposal.dependency_edges: + dependencies[source].append(label_to_id[dependency]) + created = [] + for child in proposal.children: + label = str(child["label"]) + formal = formal_by_label[label] + item = ProofObligation( + obligation_id=label_to_id[label], + statement=str(child["statement"]), + parent_id=target_id, + last_run_id=run_id, + last_evidence="Persisted from verified decomposition certificate.", + formal_status="FORMALIZED", + lean_signature=str(formal["lean_signature"]), + lean_signature_hash=result.validation[ + "child_signature_hashes" + ][label], + decomposition_certificate_hash=result.certificate_hash, + reduction_theorem_hash=result.validation[ + "reduction_proof_hash" + ], + reduction_theorem_status="PROVED", + decomposition_role_run_ids=dict(result.role_run_ids), + dependency_labels=[ + edge[1] + for edge in proposal.dependency_edges + if edge[0] == label + ], + dependency_ids=dependencies[label], + certificate_reversible_status="ACTIVE", + ) + ledger.obligations.append(item) + created.append(item) + parent.decomposition_certificate_hash = result.certificate_hash + parent.reduction_theorem_hash = result.validation["reduction_proof_hash"] + parent.reduction_theorem_status = "PROVED" + parent.decomposition_role_run_ids = dict(result.role_run_ids) + parent.certificate_reversible_status = "ACTIVE" + ledger.version += 1 + result.created = created + return created + def generator_issue_coverage( text: str, obligations: list[ProofObligation], ) -> tuple[set[str], set[str]]: required = {item.obligation_id for item in obligations} - covered = set(_ISSUE_RESPONSE.findall(text)) & required + covered = { + resolved + for model_id in _ISSUE_RESPONSE.findall(text) + if (resolved := _resolve_model_obligation_id(model_id, required)) + } return covered, required - covered +def _normalized_obligation_id(value: str) -> str: + return "-".join( + component + for component in re.split(r"[^a-z0-9]+", value.casefold()) + if component + ) + + +def _anchored_obligation_similarity(model_id: str, target_id: str) -> float: + model = _normalized_obligation_id(model_id) + target = _normalized_obligation_id(target_id) + if not model or not target: + return 0.0 + if model == target: + return 1.0 + target_components = target.split("-") + model_components = model.split("-") + if len(target_components) < 2: + return 0.0 + anchor = target_components[:2] + suffixes = [ + "-".join(model_components[index:]) + for index in range(len(model_components) - 1) + if model_components[index:index + 2] == anchor + ] + if not suffixes: + return 0.0 + return max( + difflib.SequenceMatcher(None, suffix, target).ratio() + for suffix in suffixes + ) + + def _resolve_model_obligation_id( model_id: str, allowed_ids: set[str], ) -> str: if model_id in allowed_ids: return model_id - if len(allowed_ids) != 1: + normalized_model = _normalized_obligation_id(model_id) + casefold_matches = [ + target + for target in allowed_ids + if _normalized_obligation_id(target) == normalized_model + ] + if len(casefold_matches) == 1: + return casefold_matches[0] + if not allowed_ids: return "" - target_id = next(iter(allowed_ids)) - common_prefix = os.path.commonprefix((model_id, target_id)) - prefix_ratio = len(common_prefix) / max(1, len(target_id)) - similarity = difflib.SequenceMatcher( - None, - model_id, - target_id, - ).ratio() - if prefix_ratio >= 0.65 or similarity >= 0.75: - return target_id + ranked = sorted( + ( + (_anchored_obligation_similarity(model_id, target), target) + for target in allowed_ids + ), + reverse=True, + ) + best_score, best_target = ranked[0] + if len(allowed_ids) == 1: + return best_target if best_score >= 0.88 else "" + second_score = ranked[1][0] + if best_score >= 0.95 and best_score - second_score >= 0.04: + return best_target return "" +def _descendant_ids( + ledger: ProofObligationLedger, + root_id: str, +) -> set[str]: + descendants = {root_id} + changed = True + while changed: + changed = False + for item in ledger.obligations: + if ( + item.obligation_id not in descendants + and item.parent_id in descendants + ): + descendants.add(item.obligation_id) + changed = True + return descendants - {root_id} + + +def _mark_premise_suspected( + ledger: ProofObligationLedger, + target: ProofObligation, + run_id: str, +) -> None: + target.premise_review_status = "SUSPECTED" + by_id = { + item.obligation_id: item for item in ledger.obligations + } + for descendant_id in _descendant_ids(ledger, target.obligation_id): + descendant = by_id[descendant_id] + descendant.temporary_quarantine_reason = ( + f"Premise {target.obligation_id} awaits independent review." + ) + descendant.temporary_quarantine_root_id = target.obligation_id + descendant.temporary_quarantine_run_id = run_id + + +def _clear_temporary_quarantine( + ledger: ProofObligationLedger, + root_id: str, +) -> None: + for item in ledger.obligations: + if item.temporary_quarantine_root_id != root_id: + continue + item.temporary_quarantine_reason = "" + item.temporary_quarantine_root_id = "" + item.temporary_quarantine_run_id = "" + + +def _reverse_premise_invalidation( + ledger: ProofObligationLedger, + root_id: str, + review: PremiseReview, +) -> None: + by_id = { + item.obligation_id: item for item in ledger.obligations + } + root = by_id.get(root_id) + if root is None: + return + if root.invalidation_kind in {"PREMISE", "PREMISE_INVALIDATED"}: + root.status = root.invalidation_prior_status or "UNRESOLVED" + root.invalidation_kind = "" + root.invalidation_prior_status = "" + root.premise_review_status = review.status + for descendant_id in _descendant_ids(ledger, root_id): + descendant = by_id[descendant_id] + if ( + descendant.status == "QUARANTINED" + and descendant.quarantine_root_id == root_id + ): + descendant.status = ( + descendant.quarantine_prior_status or "UNRESOLVED" + ) + if descendant.quarantine_root_id == root_id: + descendant.quarantine_reason = "" + descendant.quarantine_root_id = "" + descendant.quarantine_run_id = "" + descendant.quarantine_prior_status = "" + descendant.quarantine_confidence = 0.0 + descendant.quarantine_evidence_type = "" + descendant.quarantine_evidence_source = "" + descendant.quarantine_auditor_run_id = "" + descendant.quarantine_proponent_run_id = "" + descendant.quarantine_reversible_status = "REVERSED" + _clear_temporary_quarantine(ledger, root_id) + for lesson in ledger.no_go_lessons: + if ( + lesson.source_obligation_id == root_id + and lesson.reversible_status == "ACTIVE" + ): + lesson.reversible_status = "REVERSED" + ledger.backjump_target_id = "" + + +def _upgrade_premise_invalidation( + ledger: ProofObligationLedger, + target: ProofObligation, + refuted_premise: str, + evidence: str, + run_id: str, + review: PremiseReview | None, + bound_claim_hash: str, +) -> None: + if review is None or not review.verified or not bound_claim_hash: + return + if target.invalidation_kind not in {"PREMISE", "PREMISE_INVALIDATED"}: + target.invalidation_prior_status = target.status + target.status = "DISPROVED" + target.invalidation_kind = "PREMISE_INVALIDATED" + target.premise_review_status = "PREMISE_INVALIDATED" + by_id = { + item.obligation_id: item for item in ledger.obligations + } + for descendant_id in _descendant_ids(ledger, target.obligation_id): + descendant = by_id[descendant_id] + if ( + descendant.status == "QUARANTINED" + and descendant.quarantine_root_id == target.obligation_id + and descendant.quarantine_reversible_status == "ACTIVE" + ): + continue + descendant.quarantine_prior_status = descendant.status + descendant.status = "QUARANTINED" + descendant.quarantine_reason = ( + f"Verified premise invalidation at {target.obligation_id}." + ) + descendant.quarantine_root_id = target.obligation_id + descendant.quarantine_run_id = run_id + descendant.quarantine_confidence = review.confidence + descendant.quarantine_evidence_type = review.evidence_type + descendant.quarantine_evidence_source = review.evidence_source + descendant.quarantine_auditor_run_id = review.auditor_run_id + descendant.quarantine_proponent_run_id = review.proponent_run_id + descendant.quarantine_reversible_status = "ACTIVE" + _clear_temporary_quarantine(ledger, target.obligation_id) + claim_hash = bound_claim_hash + existing = next( + ( + lesson for lesson in ledger.no_go_lessons + if lesson.claim_hash == claim_hash + ), + None, + ) + if existing is None: + ledger.no_go_lessons.append(NoGoLesson( + claim_hash=claim_hash, + refuted_premise=refuted_premise, + evidence=evidence, + source_obligation_id=target.obligation_id, + run_id=run_id, + confidence=review.confidence, + evidence_type=review.evidence_type, + evidence_source=review.evidence_source, + auditor_run_id=review.auditor_run_id, + proponent_run_id=review.proponent_run_id, + reversible_status="ACTIVE", + )) + else: + existing.refuted_premise = refuted_premise + existing.evidence = evidence + existing.source_obligation_id = target.obligation_id + existing.run_id = run_id + existing.confidence = review.confidence + existing.evidence_type = review.evidence_type + existing.evidence_source = review.evidence_source + existing.auditor_run_id = review.auditor_run_id + existing.proponent_run_id = review.proponent_run_id + existing.reversible_status = "ACTIVE" + + def apply_critic_verdicts( ledger: ProofObligationLedger, critic_text: str, run_id: str, obligation_ids: set[str] | None = None, id_repairs: list[tuple[str, str]] | None = None, + premise_reviews: dict[str, PremiseReview] | None = None, ) -> dict[str, str]: pending_ids = ( obligation_ids @@ -353,7 +2306,17 @@ def apply_critic_verdicts( item.obligation_id for item in pending_obligations(ledger) } ) - verdicts: dict[str, tuple[str, str]] = {} + premise_reviews = premise_reviews or {} + suspicions = extract_premise_suspicions( + critic_text, + pending_ids, + { + item.obligation_id: item.lean_signature_hash + for item in ledger.obligations + if item.obligation_id in pending_ids + }, + ) + verdicts: dict[str, tuple[str, str, str, str]] = {} for match in _ISSUE_VERDICT.finditer(critic_text): model_id = match.group(1) obligation_id = _resolve_model_obligation_id( @@ -386,6 +2349,23 @@ def apply_critic_verdicts( status = status_match.group(1) evidence = evidence_match.group(1).strip() missing = missing_match.group(1).strip().lower() + invalidation_match = re.search( + r"^\*{0,2}Invalidation:\*{0,2}\s*" + r"(APPROACH|PREMISE_SUSPECTED|PREMISE)\s*$", + body, + re.MULTILINE, + ) + premise_match = re.search( + r"^\*{0,2}Premise refuted:\*{0,2}[ \t]*(.*)$", + body, + re.MULTILINE, + ) + invalidation_kind = ( + invalidation_match.group(1) if invalidation_match else "APPROACH" + ) + refuted_premise = ( + premise_match.group(1).strip() if premise_match else "" + ) if status in {"PROVED", "DISPROVED"} and ( len(evidence) < 40 or missing not in {"", "none", "(none)"} @@ -395,19 +2375,145 @@ def apply_critic_verdicts( "Closure rejected: proof/counterexample evidence was too " "short or a missing lemma remained." ) - verdicts[obligation_id] = (status, evidence) + invalidation_kind = "" + refuted_premise = "" + if status == "DISPROVED" and invalidation_kind in { + "PREMISE", + "PREMISE_SUSPECTED", + }: + suspicion = suspicions.get(obligation_id) + review = premise_reviews.get(obligation_id) + if suspicion is None: + status = "UNRESOLVED" + evidence = ( + "Premise suspicion rejected: explicit premise, evidence " + "type, concrete JSON artifact, and substantial evidence " + "are required." + ) + invalidation_kind = "" + refuted_premise = "" + elif ( + review is not None + and review.status == "PREMISE_INVALIDATED" + and review.verified + ): + invalidation_kind = "PREMISE_INVALIDATED" + refuted_premise = suspicion.premise + elif ( + review is not None + and review.status in { + "NOT_CONFIRMED", + "RESCUED", + "INCONCLUSIVE", + } + ): + status = "DISPROVED" + invalidation_kind = "APPROACH_FAILED" + refuted_premise = suspicion.premise + else: + status = "UNRESOLVED" + invalidation_kind = "PREMISE_SUSPECTED" + refuted_premise = suspicion.premise + elif status == "DISPROVED": + invalidation_kind = "APPROACH_FAILED" + verdicts[obligation_id] = ( + status, + evidence, + invalidation_kind, + refuted_premise, + ) applied: dict[str, str] = {} + by_id = { + item.obligation_id: item for item in ledger.obligations + } for item in ledger.obligations: - if item.obligation_id not in pending_ids: + if ( + item.obligation_id not in pending_ids + or item.status == "QUARANTINED" + ): continue - status, evidence = verdicts.get( + status, evidence, invalidation_kind, refuted_premise = verdicts.get( item.obligation_id, - ("UNRESOLVED", "Critic supplied no structurally valid verdict."), + ( + "UNRESOLVED", + "Critic supplied no structurally valid verdict.", + "", + "", + ), ) - item.status = status + review = premise_reviews.get(item.obligation_id) + if review is not None: + item.premise_review_status = review.status + item.premise_audit_confidence = review.confidence + item.premise_audit_evidence_type = review.evidence_type + item.premise_audit_evidence_source = review.evidence_source + item.premise_auditor_run_id = review.auditor_run_id + item.premise_proponent_run_id = review.proponent_run_id + item.premise_review_reason = review.reason + if review is not None and review.status in {"NOT_CONFIRMED", "RESCUED"}: + _reverse_premise_invalidation(ledger, item.obligation_id, review) + elif review is not None and review.status == "INCONCLUSIVE": + _clear_temporary_quarantine(ledger, item.obligation_id) + if invalidation_kind == "PREMISE_INVALIDATED": + bound_suspicion = suspicions.get(item.obligation_id) + _upgrade_premise_invalidation( + ledger, + item, + refuted_premise, + evidence, + run_id, + review, + bound_suspicion.claim_hash if bound_suspicion else "", + ) + status = item.status + else: + item.status = status item.last_evidence = evidence item.last_run_id = run_id + item.invalidation_kind = invalidation_kind applied[item.obligation_id] = status + if invalidation_kind == "PREMISE_SUSPECTED": + _mark_premise_suspected(ledger, item, run_id) + if invalidation_kind != "PREMISE_INVALIDATED": + continue + cursor = item.parent_id + visited = set() + ledger.backjump_target_id = "" + + def has_invalid_ancestor(candidate: ProofObligation) -> bool: + ancestor_id = candidate.parent_id + ancestor_visited = set() + while ancestor_id and ancestor_id not in ancestor_visited: + ancestor_visited.add(ancestor_id) + ancestor = by_id.get(ancestor_id) + if ancestor is None: + break + if ( + ancestor.status == "QUARANTINED" + or ( + ancestor.status == "DISPROVED" + and ancestor.invalidation_kind in { + "PREMISE", + "PREMISE_INVALIDATED", + } + ) + ): + return True + ancestor_id = ancestor.parent_id + return False + + while cursor and cursor not in visited: + visited.add(cursor) + ancestor = by_id.get(cursor) + if ancestor is None: + break + if ( + ancestor.status == "UNRESOLVED" + and not has_invalid_ancestor(ancestor) + ): + ledger.backjump_target_id = ancestor.obligation_id + break + cursor = ancestor.parent_id ledger.version += 1 return applied @@ -601,6 +2707,22 @@ def _frontier_rejection_reason( while cursor and cursor not in ancestors: ancestors.add(cursor) cursor = parent_by_id.get(cursor, "") + for lesson in ledger.no_go_lessons: + if lesson.reversible_status != "ACTIVE": + continue + if hashlib.sha256(_canonical_claim(statement).encode()).hexdigest() == ( + lesson.claim_hash + ): + return "repeats quarantined no-go premise" + equivalent, score = _semantic_equivalence( + lesson.refuted_premise, + statement, + ) + if equivalent: + return ( + "semantically repeats quarantined no-go premise " + f"(score={score:.2f})" + ) for item in ledger.obligations: existing_normalized = _normalize_obligation_statement(item.statement) if normalized == existing_normalized: @@ -687,6 +2809,48 @@ def audit_ledger_semantic_duplicates( return rejected +def certified_decomposition_requested( + critic_text: str, + generator_text: str, + target_ids: set[str], +) -> bool: + for match in _ISSUE_VERDICT.finditer(critic_text): + target_id = _resolve_model_obligation_id( + match.group(1), + target_ids, + ) + if not target_id: + continue + body = match.group("body") + if ( + _structured_field(body, "Status") == "UNRESOLVED" + and _normalize_obligation_statement( + _structured_field(body, "Missing lemma"), + ) not in {"", "none", "no missing lemma"} + ): + return True + for match in _ISSUE_RESPONSE.finditer(generator_text): + target_id = _resolve_model_obligation_id( + match.group(1), + target_ids, + ) + if not target_id: + continue + body_start = match.end() + next_match = _ISSUE_RESPONSE.search(generator_text, body_start) + body = generator_text[ + body_start:next_match.start() if next_match else None + ] + remaining = _structured_field(body, "Remaining gap") + if _normalize_obligation_statement(remaining) not in { + "", + "none", + "no remaining gap", + }: + return True + return False + + def create_child_obligations( ledger: ProofObligationLedger, critic_text: str, @@ -697,7 +2861,15 @@ def create_child_obligations( str, LeanSignatureResult | list[LeanSignatureResult], ] | None = None, + certified_only: bool = True, ) -> list[ProofObligation]: + if certified_only: + if rejections is not None: + rejections.append( + "free-form Missing lemma child creation is disabled; " + "a verified decomposition certificate is required", + ) + return [] created: list[ProofObligation] = [] available_signatures = { key: list(value) if isinstance(value, list) else [value] @@ -709,6 +2881,39 @@ def add_child(parent_id: str, statement: str, evidence: str) -> None: normalized = _normalize_obligation_statement(statement) if not normalized or normalized in {"none", "no missing lemma"}: return + parent = next( + item for item in ledger.obligations + if item.obligation_id == parent_id + ) + by_id = { + item.obligation_id: item for item in ledger.obligations + } + cursor = parent + visited = set() + parent_is_sound = parent.status == "UNRESOLVED" + while cursor.parent_id and cursor.parent_id not in visited: + visited.add(cursor.parent_id) + cursor = by_id.get(cursor.parent_id) + if cursor is None: + break + if ( + cursor.status == "QUARANTINED" + or ( + cursor.status == "DISPROVED" + and cursor.invalidation_kind in { + "PREMISE", + "PREMISE_INVALIDATED", + } + ) + ): + parent_is_sound = False + break + if not parent_is_sound: + if rejections is not None: + rejections.append( + f"{statement} :: parent is not a sound unresolved obligation", + ) + return rejection = _frontier_rejection_reason( ledger, parent_id, @@ -834,7 +3039,15 @@ def build_autoresearch_verdict( None, ) status = applied_verdicts.get(target_id, "UNRESOLVED") - target_children = [item for item in created if item.parent_id == target_id] + invalidation_kind = target.invalidation_kind if target is not None else "" + target_children = [ + item for item in created + if ( + item.parent_id == target_id + and item.decomposition_certificate_hash + and item.reduction_theorem_status == "PROVED" + ) + ] if status == "PROVED": outcome = "SUPPORTED" evidence = target.last_evidence if target is not None else ( @@ -844,6 +3057,28 @@ def build_autoresearch_verdict( "Integrate the proved leaf into its parent proof obligation and " "audit every dependency." ) + elif ( + status == "DISPROVED" + and invalidation_kind in {"PREMISE", "PREMISE_INVALIDATED"} + ): + outcome = "FALSIFIED" + evidence = target.last_evidence if target is not None else ( + "The targeted premise was disproved by the Critic." + ) + backjump = next( + ( + item for item in ledger.obligations + if item.obligation_id == ledger.backjump_target_id + ), + None, + ) + frontier = ( + "Backjump to the nearest sound unresolved obligation " + f"{backjump.obligation_id}: {backjump.statement}" + if backjump is not None else + "Restart from a sound unresolved root without assuming the " + "refuted premise or any canonical restatement of it." + ) elif status == "DISPROVED": outcome = "FALSIFIED" evidence = target.last_evidence if target is not None else ( @@ -882,6 +3117,13 @@ def build_autoresearch_verdict( "created_obligation_ids": [ item.obligation_id for item in target_children ], + "invalidation_kind": invalidation_kind, + "backjump_target_id": ledger.backjump_target_id, + "no_go_lesson_hashes": [ + lesson.claim_hash + for lesson in ledger.no_go_lessons + if lesson.reversible_status == "ACTIVE" + ], } @@ -1025,6 +3267,13 @@ def recover_checkpoint_from_log( section = "critic" critic.append(line.removeprefix("critic>").lstrip()) continue + if line.startswith(( + "premise_auditor>", + "adversarial_proponent>", + "[premise-", + )): + section = "" + continue if line.startswith("[metrics]"): break if section == "generator": @@ -1064,7 +3313,36 @@ def build_generator_messages( previous_critic: str = "", proof_ledger: str = "", target_obligation_id: str = "", + proof_step_interface: str = "", ) -> list[dict[str, str]]: + if proof_step_interface: + if not target_obligation_id: + raise ValueError( + "proof-step Generator requires an exact target obligation ID", + ) + return [ + { + "role": "system", + "content": ( + "Resolve exactly one host-bound proof step. Emit exactly " + f"one `### ISSUE_RESPONSE {target_obligation_id}` with " + "Correction, Derivation, and Remaining gap. Use that exact " + "ID. Use at most three concise Derivation steps and keep " + "the complete response within 450 tokens. Do not emit a " + "multi-level plan or Lean." + ), + }, + { + "role": "user", + "content": ( + f"EXACT PROOF_STEP_INTERFACE:\n{proof_step_interface}" + + ( + f"\n\nCURRENT ONE-STEP STRATEGY:\n{steering}" + if steering else "" + ) + ), + }, + ] if target_obligation_id: previous_generator = extract_obligation_history( previous_generator, @@ -1135,7 +3413,35 @@ def build_critic_messages( proof_ledger: str = "", stop_reason: str, complete: bool, + proof_step_interface: str = "", ) -> list[dict[str, str]]: + if proof_step_interface: + return [ + { + "role": "system", + "content": ( + "Audit exactly one certified proof step. Read the complete " + "Generator response and exact ProofStepInterface. Emit one " + "`### ISSUE_VERDICT ` with `Status: " + "PROVED|DISPROVED|UNRESOLVED`, `Evidence:`, and `Missing " + "lemma:`. For DISPROVED also emit `Invalidation: " + "APPROACH|PREMISE_SUSPECTED`; a suspicion must include " + "`Premise refuted:`, `Evidence type:`, and one-line JSON " + "`Evidence artifact:`. Request at most one frontier step. " + "Do not emit Lean, plans, scores, summaries, or blanket " + "approval; certified workers own decomposition and proof." + ), + }, + { + "role": "user", + "content": ( + f"EXACT PROOF_STEP_INTERFACE:\n{proof_step_interface}\n\n" + f"CURRENT CRITIC DIRECTIVE:\n{steering or '(none)'}\n\n" + f"COMPLETE GENERATOR RESPONSE:\n{generator_response}\n\n" + f"Completion: {stop_reason}; complete={complete}" + ), + }, + ] ledger_text = ( f"\n\n{proof_ledger}" if proof_ledger else "" ) @@ -1167,13 +3473,23 @@ def build_critic_messages( "DRIFTED`. If drifted, discard the off-topic branch and restore " "the proof-obligation frontier for the immutable goal. When a " "PROOF OBLIGATION LEDGER is present, adjudicate every pending " - "ID with the exact ISSUE_VERDICT format before any new frontier." + "ID with the exact ISSUE_VERDICT format before any new frontier. " + "You may emit only `Invalidation: APPROACH` or " + "`Invalidation: PREMISE_SUSPECTED`; never claim that one Critic " + "response permanently invalidates a premise. A suspicion must " + "name the premise, evidence type, and a concrete one-line JSON " + "artifact checkable by an independent worker." ), }, { "role": "user", "content": ( - f"IMMUTABLE RESEARCH GOAL:\n{goal}\n\n" + ( + f"EXACT PROOF_STEP_INTERFACE:\n{proof_step_interface}\n\n" + if proof_step_interface else + f"IMMUTABLE RESEARCH GOAL:\n{goal}\n\n" + ) + + f"Current steering:\n{steering or '(none)'}\n\n" f"Complete response:\n{generator_response}\n\n" f"Completion: {stop_reason}; complete={complete}" @@ -1306,6 +3622,12 @@ def main() -> int: default=6144, help="Hard per-stage Prefill budget; over-budget input is rejected.", ) + parser.add_argument( + "--max-retained-tokens", + type=int, + default=2052, + help="Hard sink+window retained-KV capacity for every model call.", + ) parser.add_argument( "--max-response-tokens", type=int, @@ -1333,6 +3655,16 @@ def main() -> int: default="~/.kakeya/agent_gan_proof_ledger.json", help="Private persistent mathematical proof obligations.", ) + parser.add_argument( + "--premise-review-dir", + default="~/.kakeya/premise_reviews", + help="Private durable Auditor/Proponent transcripts and artifacts.", + ) + parser.add_argument( + "--decomposition-review-dir", + default="~/.kakeya/decomposition_reviews", + help="Private atomic seven-role decomposition manifests.", + ) parser.add_argument( "--candidate-file", default="", @@ -1362,6 +3694,8 @@ def main() -> int: raise SystemExit("output-tokens must be > 0") if args.max_prefill_tokens <= 0: raise SystemExit("max-prefill-tokens must be > 0") + if args.max_retained_tokens <= 0: + raise SystemExit("max-retained-tokens must be > 0") if args.auto_loop_boundary_wait_s < 0: raise SystemExit("auto-loop-boundary-wait-s must be >= 0") research_candidate = None @@ -1407,6 +3741,10 @@ def get_stats(): state_path = Path(args.state_file).expanduser() critic_inbox_path = Path(args.critic_inbox).expanduser() proof_ledger_path = Path(args.proof_ledger).expanduser() + premise_review_dir = Path(args.premise_review_dir).expanduser() + decomposition_review_dir = Path( + args.decomposition_review_dir, + ).expanduser() if args.recover_run: recovered = recover_checkpoint_from_log( Path(args.recover_log).expanduser(), @@ -1540,6 +3878,38 @@ def get_stats(): raise ValueError( f"candidate target is not an unresolved leaf: {target_id}", ) + elif len(turn_obligations) > 1: + turn_obligations = turn_obligations[:1] + proof_step_interface_text = "" + if proof_ledger is not None and len(turn_obligations) == 1: + target = turn_obligations[0] + by_id = { + item.obligation_id: item + for item in proof_ledger.obligations + } + parent = by_id.get(target.parent_id) + interface = build_proof_step_interface( + root_goal_hash=hashlib.sha256( + research_goal.encode(), + ).hexdigest(), + target=asdict(target), + parent=asdict(parent) if parent is not None else None, + active_no_go_lessons=[ + asdict(lesson) + for lesson in proof_ledger.no_go_lessons + if lesson.reversible_status == "ACTIVE" + ], + archive_manifest={ + "ledger_id": proof_ledger.ledger_id, + "ledger_version": proof_ledger.version, + "ledger_sha256": _canonical_json_hash( + asdict(proof_ledger), + ), + }, + ) + proof_step_interface_text = ( + serialize_proof_step_interface(interface) + ) proof_ledger_text = ( format_proof_ledger(proof_ledger, turn_obligations) if turn_obligations else "" @@ -1583,7 +3953,18 @@ def get_stats(): "config": { "model_id": "gemma-4-26B-A4B-it-mlx-4bit", "topology": "primary-decode-allens-prefill", - "agents": ["generator", "critic"], + "agents": [ + "generator", + "critic", + "premise_auditor", + "definition_auditor", + "counterexample_worker", + "decomposer", + "formalizer", + "prover", + "adversarial_proponent", + "judge", + ], "rounds": 1, "output_tokens": args.output_tokens, "goal_anchor": hashlib.sha256( @@ -1644,6 +4025,7 @@ def get_stats(): and len(turn_obligations) == 1 else "" ), + proof_step_interface=proof_step_interface_text, ) generator_ids = tokenizer.apply_chat_template( generator_messages, @@ -1652,10 +4034,50 @@ def get_stats(): return_dict=False, enable_thinking=False, ) - enforce_prefill_token_budget( + admit_token_ids( "Generator", generator_ids, - args.max_prefill_tokens, + configured_prefill_tokens=args.max_prefill_tokens, + max_retained_tokens=args.max_retained_tokens, + ) + critic_fixed_messages = build_critic_messages( + research_goal, + "", + steering="\n\n".join(filter(None, ( + steering, + critic_strategy, + critic_issue_injection, + ))), + proof_ledger=( + "" if proof_step_interface_text else proof_ledger_text + ), + stop_reason="eos", + complete=True, + proof_step_interface=proof_step_interface_text, + ) + critic_fixed_ids = tokenizer.apply_chat_template( + critic_fixed_messages, + add_generation_prompt=True, + tokenize=True, + return_dict=False, + enable_thinking=False, + ) + generator_cap = min( + downstream_output_cap( + max_retained_tokens=args.max_retained_tokens, + fixed_downstream_tokens=len(generator_ids), + configured_output_tokens=( + args.max_response_tokens or None + ), + ), + downstream_output_cap( + max_retained_tokens=args.max_retained_tokens, + fixed_downstream_tokens=len(critic_fixed_ids), + configured_output_tokens=( + args.max_response_tokens or None + ), + control_reserve_tokens=384, + ), ) print( f"[allens] Generator Prefill: {len(generator_ids)} tokens...", @@ -1664,6 +4086,7 @@ def get_stats(): with PrefillHeartbeat("Generator", stats_provider=get_stats): _, generator_warm = _infer( client, eos_ids, generator_ids, 1, get_stats, + max_retained_tokens=args.max_retained_tokens, ) generator_printer = TokenPrinter(tokenizer, "generator") generator_tokens, generator_actual = _infer( @@ -1673,18 +4096,21 @@ def get_stats(): args.output_tokens, get_stats, on_token=generator_printer, - max_response_tokens=args.max_response_tokens, + max_response_tokens=generator_cap, semantic_progress=lambda chunk: bool( tokenizer.decode( chunk, skip_special_tokens=True, ).strip() ), + max_retained_tokens=args.max_retained_tokens, ) generator_printer.finish() - generator_text = tokenizer.decode( + generator_text = decode_complete_response( + tokenizer, + "Generator", generator_tokens, - skip_special_tokens=True, + generator_actual, ) covered_issues, missing_issues = generator_issue_coverage( generator_text, @@ -1737,13 +4163,16 @@ def get_stats(): critic_strategy, critic_issue_injection, ))), - proof_ledger=proof_ledger_text + ( + proof_ledger=( + "" if proof_step_interface_text else proof_ledger_text + ) + ( "\nGENERATOR COVERAGE FAILURE: missing " + ", ".join(sorted(missing_issues)) if missing_issues else "" ), stop_reason=generator_actual["stop_reason"], complete=generator_actual["complete"], + proof_step_interface=proof_step_interface_text, ) critic_ids = tokenizer.apply_chat_template( critic_messages, @@ -1752,11 +4181,25 @@ def get_stats(): return_dict=False, enable_thinking=False, ) - enforce_prefill_token_budget( + admit_token_ids( "Critic", critic_ids, - args.max_prefill_tokens, + configured_prefill_tokens=args.max_prefill_tokens, + max_retained_tokens=args.max_retained_tokens, + ) + critic_output_cap = downstream_output_cap( + max_retained_tokens=args.max_retained_tokens, + fixed_downstream_tokens=len(critic_ids), + configured_output_tokens=( + args.max_response_tokens or None + ), ) + if critic_output_cap < 320: + raise SemanticUnitTooLarge( + "Critic structured response reserve", + len(critic_ids) + 320, + args.max_retained_tokens, + ) print( f"[allens] Critic Prefill: {len(critic_ids)} tokens...", flush=True, @@ -1764,6 +4207,7 @@ def get_stats(): with PrefillHeartbeat("Critic", stats_provider=get_stats): _, critic_warm = _infer( client, eos_ids, critic_ids, 1, get_stats, + max_retained_tokens=args.max_retained_tokens, ) critic_printer = TokenPrinter(tokenizer, "critic") critic_tokens, critic_actual = _infer( @@ -1773,60 +4217,248 @@ def get_stats(): args.output_tokens, get_stats, on_token=critic_printer, - max_response_tokens=args.max_response_tokens, + max_response_tokens=critic_output_cap, semantic_progress=lambda chunk: bool( tokenizer.decode( chunk, skip_special_tokens=True, ).strip() ), + max_retained_tokens=args.max_retained_tokens, ) critic_printer.finish() - critic_text = tokenizer.decode( + critic_text = decode_complete_response( + tokenizer, + "Critic", critic_tokens, - skip_special_tokens=True, + critic_actual, ) applied_verdicts = {} created_obligations = [] id_repairs = [] rejected_frontiers = [] + isolated_role_stages = [] + premise_reviews = {} if proof_ledger is not None and turn_obligations: target_ids = { item.obligation_id for item in turn_obligations } - lean_signatures = {} - for model_id, lean_source in extract_lean_signature_blocks( + suspicions = extract_premise_suspicions( critic_text, + target_ids, + { + item.obligation_id: item.lean_signature_hash + for item in turn_obligations + }, + ) + if suspicions: + by_obligation_id = { + item.obligation_id: item + for item in proof_ledger.obligations + } + for suspicion in suspicions.values(): + suspected_target = by_obligation_id[ + suspicion.obligation_id + ] + suspected_target.invalidation_kind = ( + "PREMISE_SUSPECTED" + ) + suspected_target.last_evidence = ( + suspicion.critic_evidence + ) + suspected_target.last_run_id = run_id + _mark_premise_suspected( + proof_ledger, + suspected_target, + run_id, + ) + proof_ledger.version += 1 + save_proof_ledger( + proof_ledger_path, + proof_ledger, + ) + print( + "[premise-suspicion-checkpoint] " + f"count={len(suspicions)} run={run_id}", + flush=True, + ) + + def run_review_role( + role_name, + messages, + expected_run_id="", ): - lean_target = ( - _resolve_model_obligation_id( - model_id, - target_ids, + role_ids = tokenizer.apply_chat_template( + messages, + add_generation_prompt=True, + tokenize=True, + return_dict=False, + enable_thinking=False, + ) + admit_token_ids( + role_name, + role_ids, + configured_prefill_tokens=args.max_prefill_tokens, + max_retained_tokens=args.max_retained_tokens, + ) + role_output_cap = downstream_output_cap( + max_retained_tokens=args.max_retained_tokens, + fixed_downstream_tokens=len(role_ids), + configured_output_tokens=( + args.max_response_tokens or None + ), + control_reserve_tokens=64, + ) + print( + f"[allens] {role_name} Prefill: " + f"{len(role_ids)} tokens...", + flush=True, + ) + with PrefillHeartbeat( + role_name, + stats_provider=get_stats, + ): + _, role_warm = _infer( + client, + eos_ids, + role_ids, + 1, + get_stats, + client_label=f"agent-gan-{role_name}-warm", + max_retained_tokens=args.max_retained_tokens, ) - if model_id else ( - next(iter(target_ids)) - if len(target_ids) == 1 else "" + role_printer = TokenPrinter(tokenizer, role_name) + role_tokens, role_actual = _infer( + client, + eos_ids, + role_ids, + args.output_tokens, + get_stats, + on_token=role_printer, + max_response_tokens=role_output_cap, + semantic_progress=lambda chunk: bool( + tokenizer.decode( + chunk, + skip_special_tokens=True, + ).strip() + ), + client_label=f"agent-gan-{role_name}", + max_retained_tokens=args.max_retained_tokens, + ) + role_printer.finish() + role_text = decode_complete_response( + tokenizer, + role_name, + role_tokens, + role_actual, + ) + role_stage = _stage( + role_name, + role_warm, + role_actual, + role_text, + extra_metrics={ + "isolated_role_session": True, + "explicit_text_handoff_only": True, + }, + ) + if ( + not role_stage["ok"] + and not telemetry_state["degraded"] + ): + raise _gate_failure( + role_name, + role_warm, + role_actual, ) + isolated_role_stages.append(role_stage) + return ( + role_text, + expected_run_id or ( + f"{run_id}:{role_name}:" + f"{next(iter(target_ids))}" + ), ) - if not lean_target: - continue - lean_result = validate_lean_signature( - lean_source, + + for current_suspicion in suspicions.values(): + print( + "[premise-suspected] " + f"id={current_suspicion.obligation_id} " + f"type={current_suspicion.evidence_type}", + flush=True, + ) + audit, defense, transcripts = ( + run_isolated_premise_review( + research_goal, + current_suspicion, + run_review_role, + ) + ) + review = decide_premise_review( + audit, + defense, project_root=Path(__file__).resolve().parents[1], + suspicion=current_suspicion, + ) + if ( + missing_issues + and review.status == "PREMISE_INVALIDATED" + ): + review = PremiseReview( + "INCONCLUSIVE", + False, + confidence=review.confidence, + evidence_type=review.evidence_type, + evidence_source=review.evidence_source, + auditor_run_id=review.auditor_run_id, + proponent_run_id=review.proponent_run_id, + reason=( + "Generator issue coverage was incomplete; " + "permanent invalidation is forbidden." + ), + ) + premise_reviews[ + current_suspicion.obligation_id + ] = review + artifact_payload = { + "schema_version": 1, + "benchmark_run_id": run_id, + "suspicion": asdict(current_suspicion), + "audit": asdict(audit) if audit else None, + "defense": asdict(defense) if defense else None, + "decision": asdict(review), + "transcripts": transcripts, + } + premise_review_dir.mkdir( + parents=True, + exist_ok=True, + ) + review_key = hashlib.sha256( + current_suspicion.obligation_id.encode(), + ).hexdigest()[:16] + artifact_path = premise_review_dir / ( + f"{run_id}-{review_key}.json" + ) + temporary_artifact = artifact_path.with_suffix( + ".json.tmp", + ) + temporary_artifact.write_text( + json.dumps( + artifact_payload, + ensure_ascii=False, + indent=2, + ), + encoding="utf-8", ) - lean_signatures.setdefault( - lean_target, - [], - ).append(lean_result) + os.chmod(temporary_artifact, 0o600) + temporary_artifact.replace(artifact_path) print( - "[lean-signature-gate] " - f"target={lean_target} " - f"status={lean_result.status} " - f"hash={lean_result.signature_hash or '(none)'} " - f"attempts={lean_result.attempts} " - f"elapsed_s={lean_result.elapsed_s:.2f} " - f"error={lean_result.error or '(none)'}", + "[premise-review] " + f"id={current_suspicion.obligation_id} " + f"status={review.status} " + f"verified={review.verified} " + f"artifact={artifact_path}", flush=True, ) applied_verdicts = apply_critic_verdicts( @@ -1838,23 +4470,98 @@ def get_stats(): for item in turn_obligations }, id_repairs, + premise_reviews, ) if missing_issues: rejected_frontiers.append( "Generator coverage incomplete; child creation " f"forbidden for {','.join(sorted(missing_issues))}", ) - else: - created_obligations = create_child_obligations( - proof_ledger, + elif ( + certified_decomposition_requested( critic_text, + generator_text, + target_ids, + ) + and any( + applied_verdicts.get(target_id) == "UNRESOLVED" + for target_id in target_ids + ) + and not any( + item.invalidation_kind == "PREMISE_SUSPECTED" + for item in turn_obligations + ) + ): + decomposition_target = next( + target_id + for target_id in target_ids + if applied_verdicts.get(target_id) == "UNRESOLVED" + ) + orchestration_id = ( + f"{run_id}:decomposition:" + + hashlib.sha256( + decomposition_target.encode(), + ).hexdigest()[:12] + ) + certificate = run_certified_decomposition( + proof_ledger, + decomposition_target, + research_goal, + run_review_role, + project_root=Path(__file__).resolve().parents[1], + orchestration_id=orchestration_id, + ) + created_obligations = persist_verified_decomposition( + proof_ledger, + decomposition_target, + certificate, run_id, - { - item.obligation_id - for item in turn_obligations + ) + manifest_path = decomposition_review_dir / ( + hashlib.sha256( + orchestration_id.encode(), + ).hexdigest()[:20] + + ".json" + ) + manifest_payload = { + "schema_version": 1, + "orchestration_id": orchestration_id, + "target_obligation_id": decomposition_target, + "verified": certificate.verified, + "certificate_hash": certificate.certificate_hash, + "errors": certificate.errors, + "artifact_hashes": certificate.artifact_hashes, + "artifacts": { + role: asdict(artifact) + for role, artifact in ( + certificate.artifacts.items() + ) }, - rejected_frontiers, - lean_signatures, + "validation": certificate.validation, + "role_run_ids": certificate.role_run_ids, + "transcripts": certificate.transcripts, + "created_obligation_ids": [ + item.obligation_id + for item in created_obligations + ], + } + save_decomposition_manifest( + manifest_path, + manifest_payload, + ) + print( + "[decomposition-review] " + f"target={decomposition_target} " + f"verified={certificate.verified} " + f"created={len(created_obligations)} " + f"manifest={manifest_path}", + flush=True, + ) + rejected_frontiers.extend(certificate.errors) + else: + rejected_frontiers.append( + "free-form frontier retained for audit; no child " + "persisted without a certified decomposition", ) for model_id, target_id in id_repairs: print( @@ -1933,7 +4640,10 @@ def get_stats(): api_key=api_key, method="PATCH", body={ - "stages": [critic_stage], + "stages": [ + critic_stage, + *isolated_role_stages, + ], "status": "completed", "finished_at": time.time(), }, @@ -1941,7 +4651,11 @@ def get_stats(): summary = ( completed["summary"] if completed is not None - else summarize_stages([generator_stage, critic_stage]) + else summarize_stages([ + generator_stage, + critic_stage, + *isolated_role_stages, + ]) ) print( "[metrics] " diff --git a/tests/inference_engine/bench/test_autoresearch_supervisor.py b/tests/inference_engine/bench/test_autoresearch_supervisor.py index 7b323f5c..52608123 100644 --- a/tests/inference_engine/bench/test_autoresearch_supervisor.py +++ b/tests/inference_engine/bench/test_autoresearch_supervisor.py @@ -1,9 +1,21 @@ +import json +import pytest + +from autoresearch.prefill.semantic_decompose import ( + SemanticUnitTooLarge, + admit_token_ids, + downstream_output_cap, +) from autoresearch.prefill.supervisor import ( append_result, best_kept, build_host_candidate, + build_strategy_contract, + build_strategy_prompt, build_strategy_research_state, check_runtime_health, + extract_gan_failure_reason, + infrastructure_failure_fingerprint, parse_research_verdict, read_results, repair_candidate_schema, @@ -52,6 +64,45 @@ def test_candidate_render_is_executable_and_strict(tmp_path): raise AssertionError("fallback candidate must be rejected") +def test_infrastructure_failure_fingerprint_is_stable_and_specific(): + failed = { + "research_outcome": "EVALUATION_FAILED", + "error": "RuntimeError: GAN benchmark is not completed: failed", + } + assert infrastructure_failure_fingerprint(failed) + assert infrastructure_failure_fingerprint(failed) == ( + infrastructure_failure_fingerprint({ + **failed, + "error": " RUNTIMEERROR: GAN benchmark is not completed: failed ", + }) + ) + assert infrastructure_failure_fingerprint({ + **failed, + "error": "different failure", + }) != infrastructure_failure_fingerprint(failed) + assert infrastructure_failure_fingerprint({ + **failed, + "research_outcome": "FALSIFIED", + }) == "" + + +def test_gan_failure_reason_preserves_semantic_error(): + output = ( + "[inference-failed] time=now run=br_1 " + "error=SemanticResponseIncomplete: " + "SEMANTIC_RESPONSE_INCOMPLETE: Generator stopped before EOS\n" + ) + assert extract_gan_failure_reason(output) == ( + "SemanticResponseIncomplete: SEMANTIC_RESPONSE_INCOMPLETE: " + "Generator stopped before EOS" + ) + assert extract_gan_failure_reason("no structured failure") == "" + assert infrastructure_failure_fingerprint({ + "research_outcome": "EVALUATION_FAILED", + "error": "", + }) == "" + + def test_strategy_schema_repair_prefers_current_branch_leaf(): current = _candidate() ledger = {"obligations": [ @@ -206,6 +257,16 @@ def test_strategy_parser_accepts_python_literal_candidate(): assert candidate["strategy_parse_mode"] == "python-literal" +def test_strategy_repairs_invalid_json_latex_escapes(): + candidate = _extract_json( + r'''```json +{"candidate_id":"trial","hypothesis":"sequence \{z_n\} has density \rho"} +```''', + ) + assert candidate["hypothesis"] == r"sequence \{z_n\} has density \rho" + assert candidate["strategy_parse_mode"] == "json-escape-repaired" + + def test_keep_requires_novel_mathematical_advancement(): baseline = { "proof_obligations_unresolved": "5", @@ -304,6 +365,28 @@ def test_pending_leaf_ids_excludes_unresolved_parents(): assert _pending_leaf_ids(ledger) == ["RH-C1-child", "RH-C2"] +def test_pending_leaf_ids_excludes_stale_premise_descendants(): + ledger = {"obligations": [ + { + "obligation_id": "ROOT", + "status": "DISPROVED", + "invalidation_kind": "PREMISE", + "parent_id": "", + }, + { + "obligation_id": "ROOT-stale", + "status": "UNRESOLVED", + "parent_id": "ROOT", + }, + { + "obligation_id": "SOUND", + "status": "UNRESOLVED", + "parent_id": "", + }, + ]} + assert _pending_leaf_ids(ledger) == ["SOUND"] + + def test_host_candidate_targets_deepest_current_branch_leaf(): current = {**_candidate(), "target_obligation_id": "RH-C2"} ledger = {"obligations": [ @@ -366,6 +449,43 @@ def test_host_candidate_rolls_back_to_nearest_valid_ancestor(): assert candidate["target_obligation_id"] == "RH-C2-gap" +def test_host_candidate_uses_recorded_premise_backjump_target(): + current = {**_candidate(), "target_obligation_id": "ROOT-bad"} + ledger = { + "backjump_target_id": "ROOT", + "no_go_lessons": [{ + "refuted_premise": "Every admissible kernel is positive.", + "source_obligation_id": "ROOT-bad", + }], + "obligations": [ + { + "obligation_id": "ROOT", + "statement": "Find a sound replacement reduction.", + "status": "UNRESOLVED", + "parent_id": "", + }, + { + "obligation_id": "ROOT-bad", + "statement": "Use universal kernel positivity.", + "status": "DISPROVED", + "invalidation_kind": "PREMISE", + "parent_id": "ROOT", + }, + { + "obligation_id": "UNRELATED", + "statement": "Unrelated unresolved branch.", + "status": "UNRESOLVED", + "parent_id": "", + }, + ], + } + candidate = build_host_candidate(current, ledger) + assert candidate["target_obligation_id"] == "ROOT" + assert "Every admissible kernel is positive" in ( + candidate["generator_directive"] + ) + + def test_strategy_is_triggered_only_by_events(tmp_path): progress = { "kept": "True", @@ -389,6 +509,30 @@ def test_strategy_is_triggered_only_by_events(tmp_path): [{"kept": "True", "research_outcome": "FALSIFIED"}], stagnation_rounds=3, ) == "branch-falsified" + assert strategy_trigger_reason( + [{ + "kept": "True", + "research_outcome": "FALSIFIED", + "invalidation_kind": "PREMISE_INVALIDATED", + }], + stagnation_rounds=3, + ) == "premise-invalidated" + assert strategy_trigger_reason( + [{ + "kept": "False", + "research_outcome": "INCONCLUSIVE", + "invalidation_kind": "PREMISE_SUSPECTED", + }], + stagnation_rounds=3, + ) == "" + assert strategy_trigger_reason( + [{ + "kept": "True", + "research_outcome": "INCONCLUSIVE", + "invalidation_kind": "APPROACH_FAILED", + }], + stagnation_rounds=3, + ) == "branch-falsified" trigger = tmp_path / "request_strategy" trigger.write_text("replan") assert strategy_trigger_reason( @@ -405,7 +549,36 @@ def test_strategy_budget_error_preserves_exact_admission_counts(): assert "without truncation: 11935 > 8448" in str(error) -def test_strategy_state_keeps_complete_active_ancestry_only(): +def test_semantic_admission_and_dynamic_output_reserve_never_slice(): + token_ids = list(range(2053)) + with pytest.raises( + SemanticUnitTooLarge, + match="SEMANTIC_UNIT_TOO_LARGE", + ): + admit_token_ids( + "indivisible target", + token_ids, + configured_prefill_tokens=6144, + max_retained_tokens=2052, + ) + assert token_ids == list(range(2053)) + assert downstream_output_cap( + max_retained_tokens=2052, + fixed_downstream_tokens=1700, + configured_output_tokens=1000, + control_reserve_tokens=32, + ) == 320 + + +def test_strategy_candidate_rejects_multi_step_plan(): + with pytest.raises(ValueError, match="exactly one step"): + validate_candidate({ + **_candidate(), + "plan": {"steps": ["first", "second"]}, + }) + + +def test_strategy_state_keeps_exact_one_step_interface_only(): ledger = {"obligations": [ { "obligation_id": "RH-C1", @@ -441,16 +614,59 @@ def test_strategy_state_keeps_complete_active_ancestry_only(): ledger=ledger, results_text=results, ) - assert state["target_leaf_id"] == "RH-C2-child" + interface = state["proof_step_interface"] + assert interface["target_obligation_id"] == "RH-C2-child" + assert interface["target_statement"] == "exact child statement" + assert interface["current_target_evidence"] == "exact child evidence" + assert interface["parent_interface"]["statement_hash"] serialized = str(state) - assert "exact root statement" in serialized assert "exact child evidence" in serialized - assert "exact result" in serialized + assert "exact root statement" not in serialized + assert "exact root evidence" not in serialized + assert "exact result" not in serialized assert "unrelated root" not in serialized assert "unrelated result" not in serialized -def test_strategy_state_deduplicates_text_losslessly(): +def test_strategy_state_carries_lossless_no_go_lessons(): + premise = "Every admissible kernel is positive." + evidence = ( + "The explicit admissible polynomial kernel changes sign while " + "satisfying every required boundary condition." + ) + ledger = { + "backjump_target_id": "ROOT", + "no_go_lessons": [{ + "claim_hash": "abc123", + "refuted_premise": premise, + "evidence": evidence, + "source_obligation_id": "ROOT-bad", + "run_id": "br_refute", + }], + "obligations": [{ + "obligation_id": "ROOT", + "statement": "Find a replacement reduction.", + "status": "UNRESOLVED", + "parent_id": "", + }, { + "obligation_id": "ROOT-bad", + "statement": premise, + "status": "DISPROVED", + "invalidation_kind": "PREMISE", + "parent_id": "ROOT", + }], + } + state = build_strategy_research_state( + current={**_candidate(), "target_obligation_id": "ROOT-bad"}, + ledger=ledger, + results_text="", + ) + lessons = state["proof_step_interface"]["active_no_go_lessons"] + assert lessons[0]["refuted_premise"] == premise + assert lessons[0]["evidence"] == evidence + + +def test_strategy_state_keeps_target_unit_and_hashes_history(): shared = "Complete exact evidence that must appear once without truncation." ledger = {"obligations": [ { @@ -476,12 +692,117 @@ def test_strategy_state_deduplicates_text_losslessly(): serialized = str(state) assert serialized.count(shared) == 1 assert serialized.count("Root statement.") == 1 - evidence_ref = state["target_ancestry"][0]["last_evidence_ref"] - result_ref = state["relevant_experiments"][0][ - "research_evidence_ref" + interface = state["proof_step_interface"] + assert interface["current_target_evidence"] == shared + archive = interface["archive_manifest"] + assert archive["record_count"] == 1 + assert len(archive["ordered_records_sha256"]) == 64 + + +def test_strategy_state_exposes_latest_semantic_failure_for_smaller_step(): + ledger = {"obligations": [{ + "obligation_id": "RH-C2", + "statement": "Exact current target.", + "status": "UNRESOLVED", + "parent_id": "", + }]} + error = ( + "SemanticResponseIncomplete: SEMANTIC_RESPONSE_INCOMPLETE: " + "Generator stopped before EOS after 320 tokens" + ) + results = ( + "target_obligation_id\thypothesis_sha256\tresearch_outcome\terror\n" + f"RH-C2\thash-1\tEVALUATION_FAILED\t{error}\n" + ) + state = build_strategy_research_state( + current={**_candidate(), "target_obligation_id": "RH-C2"}, + ledger=ledger, + results_text=results, + ) + latest = state["proof_step_interface"]["archive_manifest"][ + "latest_failure" ] - assert evidence_ref == result_ref - assert state["text_by_id"][evidence_ref] == shared + assert latest["kind"] == "SEMANTIC_RESPONSE_INCOMPLETE" + assert latest["role"] == "Generator" + assert latest["response_tokens"] == 320 + assert "error" not in latest + + +def test_strategy_prompt_bounded_interface_for_11_nodes_and_28_runs(): + obligations = [] + for index in range(11): + obligations.append({ + "obligation_id": f"RH-N{index}", + "statement": ( + f"Complete exact ancestry statement {index}: " + + "mathematical condition " * 12 + ), + "status": "UNRESOLVED", + "parent_id": f"RH-N{index - 1}" if index else "", + "last_evidence": ( + f"ancestry evidence {index} " + "detail " * 80 + ), + }) + header = ( + "timestamp\texperiment_id\trun_id\tcandidate_id\t" + "target_obligation_id\thypothesis_sha256\tresearch_outcome\t" + "invalidation_kind\tresearch_evidence\tnew_frontier\tkept\terror\n" + ) + rows = [] + for index in range(28): + critical = index % 7 == 0 + rows.append("\t".join(( + str(index), + f"experiment-{index}", + f"run-{index}", + f"candidate-{index}", + "RH-N10", + f"hypothesis-{index % 4}", + "FALSIFIED" if critical else "INCONCLUSIVE", + "", + f"evidence-{index}-" + "exact mathematical evidence " * 45, + f"frontier-{index}-" + "exact frontier statement " * 30, + "True" if critical else "False", + "" if index % 5 else "worker timeout fingerprint", + ))) + results = header + "\n".join(rows) + "\n" + ledger = {"obligations": obligations} + current = {**_candidate(), "target_obligation_id": "RH-N0"} + state = build_strategy_research_state( + current=current, + ledger=ledger, + results_text=results, + ) + interface = state["proof_step_interface"] + assert interface["target_obligation_id"] == "RH-N10" + assert "Complete exact ancestry statement 10" in ( + interface["target_statement"] + ) + assert "Complete exact ancestry statement 9" not in str(state) + archive = interface["archive_manifest"] + assert archive["record_count"] == 28 + assert len(archive["ordered_records_sha256"]) == 64 + serialized = json.dumps(state, ensure_ascii=False) + assert "evidence-27-" not in serialized + assert "evidence-1-" not in serialized + program = ( + Path(__file__).resolve().parents[3] + / "autoresearch" + / "prefill" + / "program.md" + ).read_text() + contract = build_strategy_contract(program) + assert "target_obligation_id must equal TARGET_LEAF_ID" in contract + assert "no fallback" in contract + prompt = build_strategy_prompt( + program=program, + current=current, + results_text=results, + ledger=ledger, + ) + assert "\n\nPROGRAM:\n" not in prompt + proxy_tokens = (len(prompt.encode("utf-8")) + 3) // 4 + assert proxy_tokens <= 2052 def test_results_are_append_only_and_best_is_selected(tmp_path): @@ -595,6 +916,8 @@ def test_supervisor_preserves_runtime_and_cache_across_iterations(): assert "mode=gemma trigger=" in body assert "except StrategyPrefillBudgetExceeded" in body assert "phase=strategy-deferred-budget" in body + assert "except SemanticResponseIncomplete" in body + assert "phase=strategy-deferred-semantic" in body assert "if not gan_completed:" in body assert "phase=completed-run-preserved" in body assert "deploy_candidate" not in source @@ -602,6 +925,18 @@ def test_supervisor_preserves_runtime_and_cache_across_iterations(): assert "launchctl" not in source assert "bootout" not in source assert "results_text[-" not in source + propose_body = source[ + source.index("def propose_candidate"): + source.index("def check_runtime_health") + ] + assert propose_body.index("admit_token_ids(") < propose_body.index( + "session.append(ids)", + ) + run_body = source[ + source.index("def run_gan_experiment"): + source.index("def read_results") + ] + assert '"--max-retained-tokens"' in run_body def test_gan_subprocess_output_is_streamed_not_captured(): diff --git a/tests/inference_engine/bridge/test_agent_gan_demo.py b/tests/inference_engine/bridge/test_agent_gan_demo.py index dcbd1652..a940b14a 100644 --- a/tests/inference_engine/bridge/test_agent_gan_demo.py +++ b/tests/inference_engine/bridge/test_agent_gan_demo.py @@ -3,7 +3,13 @@ _infer, _output_metadata, build_critic_context, + decode_complete_response, ) +from autoresearch.prefill.semantic_decompose import ( + SemanticResponseIncomplete, + SemanticUnitTooLarge, +) +import pytest def test_agent_gate_accepts_remote_compute_or_exact_remote_cache_hit(): @@ -68,8 +74,10 @@ def generate(self, *, max_tokens): class Client: def __init__(self, session): self.session = session + self.session_kwargs = [] - def create_session(self, **_kwargs): + def create_session(self, **kwargs): + self.session_kwargs.append(kwargs) return self.session @@ -91,6 +99,71 @@ def test_infer_continues_chunks_until_eos(): assert metrics["complete"] is True +def test_infer_uses_explicit_isolated_role_session_label(): + client = Client(Session([([1], 2)])) + _infer( + client, + [2], + [9], + 1, + lambda: {}, + client_label="agent-gan-premise-auditor", + ) + assert client.session_kwargs == [{ + "eos_token_ids": [2], + "client_label": "agent-gan-premise-auditor", + }] + + +def test_infer_rejects_oversized_unit_before_session_append(): + client = Client(Session([([1], 2)])) + with pytest.raises(SemanticUnitTooLarge): + _infer( + client, + [], + list(range(2053)), + 1, + lambda: {}, + max_retained_tokens=2052, + ) + assert client.session_kwargs == [] + + +def test_seven_decomposition_roles_each_get_fresh_session(): + class FreshClient: + def __init__(self): + self.sessions = [] + + def create_session(self, **kwargs): + session = Session([([1], 2)]) + self.sessions.append((kwargs, session)) + return session + + roles = [ + "definition_auditor", + "counterexample_worker", + "decomposer", + "formalizer", + "prover", + "adversarial_proponent", + "judge", + ] + client = FreshClient() + for role in roles: + _infer( + client, + [], + [9], + 1, + lambda: {}, + client_label=f"agent-gan-{role}", + ) + assert [item[0]["client_label"] for item in client.sessions] == [ + f"agent-gan-{role}" for role in roles + ] + assert len({id(item[1]) for item in client.sessions}) == 7 + + def test_infer_reports_explicit_client_safety_limit(): tokens, metrics = _infer( Client(Session([([1, 2], 1)])), @@ -103,6 +176,79 @@ def test_infer_reports_explicit_client_safety_limit(): assert tokens == [1, 2] assert metrics["stop_reason"] == "client_safety_limit" assert metrics["complete"] is False + assert metrics["eos_reached"] is False + assert metrics["response_cap_exhausted"] is True + + +def test_infer_accepts_exact_eos_at_response_cap_without_slicing(): + tokens, metrics = _infer( + Client(Session([([1, 2], 2)])), + [], + [9], + 2, + lambda: {}, + max_response_tokens=2, + ) + assert tokens == [1, 2] + assert metrics["stop_reason"] == "eos" + assert metrics["complete"] is True + assert metrics["eos_reached"] is True + assert metrics["response_cap_exhausted"] is False + + +def test_capped_generator_is_rejected_before_decode_or_critic_construction(): + class CountingTokenizer(CharTokenizer): + def __init__(self): + self.decode_calls = 0 + + def decode(self, token_ids, **kwargs): + self.decode_calls += 1 + return super().decode(token_ids, **kwargs) + + tokenizer = CountingTokenizer() + critic_constructed = False + tokens, metrics = _infer( + Client(Session([([ord("I"), ord("f"), ord(" ")], 1)])), + [], + [9], + 3, + lambda: {}, + max_response_tokens=3, + ) + # Deliberately failing KV metrics prove semantic classification wins. + metrics["delta"] = {"local_hits": 0, "fallbacks": 9} + with pytest.raises( + SemanticResponseIncomplete, + match="SEMANTIC_RESPONSE_INCOMPLETE.*response_cap_exhausted=True", + ) as exc: + generator_text = decode_complete_response( + tokenizer, + "Generator", + tokens, + metrics, + ) + critic_constructed = True + build_critic_context(tokenizer, generator_text) + + assert exc.value.response_cap_exhausted is True + assert exc.value.stop_reason == "client_safety_limit" + assert tokenizer.decode_calls == 0 + assert critic_constructed is False + + +def test_complete_response_decodes_exact_tokens(): + tokenizer = CharTokenizer() + text = decode_complete_response( + tokenizer, + "Generator", + [97, 98, 99], + { + "stop_reason": "eos", + "complete": True, + "response_cap_exhausted": False, + }, + ) + assert text == "abc" def test_infer_stops_repeated_nonsemantic_chunks(): diff --git a/tests/inference_engine/bridge/test_agent_gan_repl.py b/tests/inference_engine/bridge/test_agent_gan_repl.py index ae990371..fd77308b 100644 --- a/tests/inference_engine/bridge/test_agent_gan_repl.py +++ b/tests/inference_engine/bridge/test_agent_gan_repl.py @@ -1,14 +1,32 @@ +import hashlib import io import json +import re import signal import sys import time +from dataclasses import asdict from pathlib import Path -from autoresearch.prefill.lean_gate import LeanSignatureResult +from autoresearch.prefill.lean_gate import ( + LeanSignatureResult, + lean_theorem_signature_hash, + validate_lean_proof, +) +from autoresearch.prefill.semantic_decompose import SemanticUnitTooLarge from scripts.agent_gan_repl import ( PrefillHeartbeat, CriticIssueBatch, + PremiseAudit, + PremiseDefense, + PremiseReview, + DefinitionAudit, + CounterexampleReport, + DecompositionProposal, + FormalizationBundle, + ProofAttempt, + DefenseReport, + JudgeDecision, ProofObligation, ProofObligationLedger, ReplCheckpoint, @@ -16,6 +34,7 @@ TimestampedTee, TokenPrinter, _gate_failure, + _json_artifact, _stage, _telemetry_request, build_critic_messages, @@ -29,21 +48,41 @@ audit_ledger_semantic_duplicates, build_autoresearch_verdict, create_child_obligations, + certified_decomposition_requested, format_critic_issue_injection, format_proof_ledger, generator_issue_coverage, + decide_premise_review, + extract_premise_suspicions, load_checkpoint, load_pending_critic_issues, load_proof_ledger, pending_obligations, parse_repl_command, + parse_premise_audit, + parse_premise_defense, + parse_certified_artifact, recover_checkpoint_from_log, save_critic_issue_batch, + save_decomposition_manifest, save_proof_ledger, save_checkpoint, + run_isolated_premise_review, + run_certified_decomposition, + persist_verified_decomposition, + validate_evidence_artifact, ) +def test_json_artifact_repairs_invalid_latex_escapes_losslessly(): + artifact = _json_artifact( + r'{"statement":"sequence \{z_n\} has density \rho"}', + ) + assert artifact == { + "statement": r"sequence \{z_n\} has density \rho", + } + + class Tokenizer: def decode(self, token_ids, **_kwargs): return "".join(chr(96 + token) for token in token_ids) @@ -57,6 +96,226 @@ def _valid_lean_signature(suffix=""): ) +def _premise_suspicion_text(invalidation="PREMISE_SUSPECTED"): + claim = { + "schema_version": 1, + "quantifier": "FOR_ALL", + "variables": ["x"], + "domain": "REAL", + "lhs": "x*x", + "relation": "==", + "rhs": "x", + } + return f""" +### ISSUE_VERDICT ROOT-A +Status: DISPROVED +Invalidation: {invalidation} +Premise refuted: For every real x, x squared equals x. +Evidence type: FINITE_COUNTEREXAMPLE +Evidence artifact: {json.dumps({"claim": claim}, separators=(",", ":"))} +Evidence: Substitution of the explicit finite value x=2 gives four on the left and two on the right, contradicting universal equality. +Missing lemma: none +""" + + +def _audit_text(status="CONFIRMED", confidence="0.95", evidence_type="FINITE_COUNTEREXAMPLE"): + suspicion = extract_premise_suspicions( + _premise_suspicion_text(), + {"ROOT-A"}, + )["ROOT-A"] + artifact = { + "claim_hash": suspicion.claim_hash, + "claim": suspicion.claim_schema, + "witness": {"x": 2}, + } + return f""" +### PREMISE_AUDIT ROOT-A +Status: {status} +Evidence type: {evidence_type} +Evidence source: host-checkable substitution x=2 +Confidence: {confidence} +Artifact: {json.dumps(artifact, separators=(",", ":"))} +Analysis: The universal quantifier is contradicted by this explicit domain element. +""" + + +def _defense_text(status="NOT_RESCUED"): + return f""" +### PREMISE_DEFENSE ROOT-A +Status: {status} +Correction: Restricting x to zero or one would rescue a different proposition. +Failure reason: The stated universal real-domain premise has no such restriction. +Evidence: The proposed restriction changes the exact domain and therefore cannot rescue the original quantified premise. +""" + + +def _certificate_runner( + *, + child_signature="theorem childReduction : True := by sorry", + proof_source="theorem reduction (h : True) : True := by exact h", + cycle=False, + parent_hash_override="", + judge_decision="ACCEPT", + counterexample_case=None, + multi_child=False, +): + calls = [] + parent_source = "theorem parentTarget : True := by sorry" + reduction_source = "theorem reduction (h : True) : True := by sorry" + child_statement = ( + "For every fixed compact disk, prove an explicit uniform boundary " + "inequality for the analytic approximants." + ) + + def runner(role, messages, expected_run_id): + calls.append((role, messages, expected_run_id)) + package = json.loads(messages[-1]["content"]) + common = { + "target_obligation_id": package["target_obligation_id"], + "parent_statement_hash": package["parent_statement_hash"], + "root_goal_hash": package["root_goal_hash"], + "producer_role": role, + "producer_run_id": expected_run_id, + "upstream_artifact_hashes": package[ + "upstream_artifact_hashes" + ], + } + if role == "definition_auditor": + heading = "DEFINITION_AUDIT" + specific = { + "definitions": [{"symbol": "K", "domain": "compact disks"}], + "missing_definitions": [], + } + elif role == "counterexample_worker": + heading = "COUNTEREXAMPLE_REPORT" + specific = { + "status": ( + "COUNTEREXAMPLE_FOUND" + if counterexample_case else "NO_COUNTEREXAMPLE" + ), + "cases": [counterexample_case] if counterexample_case else [], + } + elif role == "decomposer": + heading = "DECOMPOSITION_PROPOSAL" + children = [{ + "label": "L1", + "statement": child_statement, + "kind": "LEMMA", + }] + if multi_child: + children.append({ + "label": "L2", + "statement": ( + "For every boundary point, prove a separate explicit " + "continuity inequality for the analytic approximants." + ), + "kind": "LEMMA", + }) + specific = { + "parent_statement": package["parent_statement"], + "children": children, + "dependency_edges": [["L1", "L1"]] if cycle else [], + "public_assumptions": [], + "reduction_labels": [ + child["label"] for child in children + ], + "reduction_contract": "L1 implies the exact parent.", + } + elif role == "formalizer": + heading = "FORMALIZATION_BUNDLE" + parent_hash = ( + parent_hash_override + or lean_theorem_signature_hash(parent_source) + ) + specific = { + "math_ir": { + "parent_signature_hash": parent_hash, + "parent_proposition_hash": hashlib.sha256( + b"True", + ).hexdigest(), + "child_labels": ["L1"], + "public_assumptions": [], + "reduction_labels": ["L1"], + }, + "parent_signature_source": parent_source, + "parent_signature_hash": parent_hash, + "parent_newly_formalized": True, + "children": [{ + "label": "L1", + "statement": child_statement, + "lean_signature": child_signature, + "lean_signature_hash": lean_theorem_signature_hash( + child_signature, + ), + }], + "reduction_theorem_source": reduction_source, + "reduction_signature_hash": lean_theorem_signature_hash( + reduction_source, + ), + } + elif role == "prover": + heading = "PROOF_ATTEMPT" + specific = { + "status": "PROVED", + "reduction_theorem_source": proof_source, + } + elif role == "adversarial_proponent": + heading = "DEFENSE_REPORT" + specific = { + "status": "DEFENDED", + "issues": [], + "repairs": [], + } + else: + heading = "JUDGE_DECISION" + specific = { + "decision": judge_decision, + "reason": "Host manifest reviewed.", + } + text = ( + f"### {heading}\nArtifact: " + + json.dumps({**common, **specific}, separators=(",", ":")) + ) + return text, expected_run_id + + return runner, calls + + +def _fake_signature_validator(source, *, project_root): + del project_root + if "badChild" in source: + return LeanSignatureResult( + source, + "", + False, + status="TYPECHECK_FAILED", + error="bad child", + ) + return LeanSignatureResult( + source, + lean_theorem_signature_hash(source), + True, + ) + + +def _fake_proof_validator(source, *, project_root): + del project_root + if re.search(r"\b(?:sorry|admit)\b", source): + return LeanSignatureResult( + source, + "", + False, + status="UNSAFE_REJECTED", + error="incomplete proof", + ) + return LeanSignatureResult( + source, + hashlib.sha256(source.encode()).hexdigest(), + True, + status="PROVED", + ) + + def test_timestamped_tee_preserves_terminal_and_flushes_log(tmp_path): terminal = io.StringIO() timestamps = iter(("t1", "t2", "t3")) @@ -302,6 +561,7 @@ def test_interactive_prompts_are_deterministic_for_kv_reuse(): assert "Ignore prizes, money, prestige" in combined assert "smallest unresolved frontier" in combined assert "sample, summarize, simplify" in combined + assert "LEAN_SIGNATURE" not in combined def test_generator_history_is_scoped_to_target_leaf(): @@ -335,6 +595,95 @@ def test_generator_history_is_scoped_to_target_leaf(): assert "unrelated operator branch" not in prompt +def test_generator_and_critic_share_exact_one_step_interface_and_output(): + interface = json.dumps({ + "root_goal_hash": "root-hash", + "target_obligation_id": "ROOT-L1", + "target_statement": "Exact bounded target statement.", + "interface_hash": "interface-hash", + }, separators=(",", ":")) + generator = build_generator_messages( + "full root prose must not be active", + steering="Attempt exactly one boundary case.", + target_obligation_id="ROOT-L1", + proof_step_interface=interface, + ) + generator_prompt = generator[-1]["content"] + assert interface in generator_prompt + assert "### ISSUE_RESPONSE ROOT-L1" in generator[0]["content"] + assert "### ISSUE_RESPONSE " not in generator[0]["content"] + assert "full root prose" not in generator_prompt + exact_output = ( + "### ISSUE_RESPONSE ROOT-L1\n" + "Correction: exact bytes π.\n" + "Derivation: one bounded step.\n" + "Remaining gap: none" + ) + critic = build_critic_messages( + "full root prose must not be active", + exact_output, + proof_step_interface=interface, + stop_reason="eos", + complete=True, + ) + critic_prompt = critic[-1]["content"] + assert interface in critic_prompt + assert exact_output in critic_prompt + assert critic_prompt.count(exact_output) == 1 + assert "full root prose" not in critic_prompt + assert "Audit exactly one certified proof step" in critic[0]["content"] + assert "Build a proof-obligation tree" not in critic[0]["content"] + + +def test_generator_repairs_real_namespaced_single_target_id(): + target = ( + "RH-C2-0ef53a217d-25557e489d-4f025934ee-3110912e68-" + "763645cd6b-40ef83e052-b80cd1343b-3be9e8e78f-fbee0281ff-" + "e4fff64467" + ) + malformed = ( + "rh-rigorous-obligations-v1-rh-C2-0ef53a217d-25557e489d-" + "4f025934ee-311091268-763645cd6b-40ef83e052-b80cd1343b-" + "3be9e8e78f-fbee0281ff-e4fff64467" + ) + covered, missing = generator_issue_coverage( + f"### ISSUE_RESPONSE {malformed}\nCorrection: repaired", + [ProofObligation(target, "Exact target.")], + ) + assert covered == {target} + assert missing == set() + + +def test_generator_rejects_unrelated_and_ambiguous_ids(): + target = ProofObligation( + "RH-C2-aaaaaaaaaa-bbbbbbbbbb-cccccccccc", + "First target.", + ) + covered, missing = generator_issue_coverage( + "### ISSUE_RESPONSE rh-c2-invented-unrelated-label", + [target], + ) + assert covered == set() + assert missing == {target.obligation_id} + + alternatives = [ + ProofObligation( + "RH-C2-aaaaaaaaaa-bbbbbbbbbb-111111111a", + "Alternative A.", + ), + ProofObligation( + "RH-C2-aaaaaaaaaa-bbbbbbbbbb-111111111b", + "Alternative B.", + ), + ] + covered, missing = generator_issue_coverage( + "### ISSUE_RESPONSE rh-c2-aaaaaaaaaa-bbbbbbbbbb-111111111c", + alternatives, + ) + assert covered == set() + assert missing == {item.obligation_id for item in alternatives} + + def test_prefill_budget_rejects_whole_input_without_truncation(): token_ids = list(range(7)) enforce_prefill_token_budget("Generator", token_ids, 7) @@ -405,6 +754,7 @@ def test_continuous_auto_loop_is_default_and_exception_pauses(): assert "auto_loop_active = False" in source assert "[auto-loop-paused]" in source assert '"--no-auto-loop"' in source + assert "extract_lean_signature_blocks" not in source def test_checkpoint_round_trip_is_private(tmp_path): @@ -466,6 +816,7 @@ def test_proof_ledger_carries_unresolved_and_closes_valid_verdicts(tmp_path): ] rendered = format_proof_ledger(loaded) assert "### ISSUE_RESPONSE " in rendered + assert "LEAN_SIGNATURE" not in rendered covered, missing = generator_issue_coverage( "### ISSUE_RESPONSE RH-C1\nCorrection: fixed", pending_obligations(loaded), @@ -514,7 +865,741 @@ def test_proof_ledger_rejects_weak_or_missing_closure(): assert len(pending_obligations(ledger)) == 2 -def test_missing_lemma_creates_deduplicated_child_and_selects_leaf(): +def test_premise_invalidation_quarantines_subtree_and_backjumps(): + root = ProofObligation("ROOT", "Establish the main reduction.") + target = ProofObligation( + "ROOT-A", + "For every real x, x squared equals x.", + parent_id="ROOT", + ) + descendant = ProofObligation( + "ROOT-A-1", + "Use kernel positivity to derive the bound.", + parent_id="ROOT-A", + ) + alternate = ProofObligation( + "ROOT-B", + "Construct an alternate sign-changing kernel.", + parent_id="ROOT", + ) + ledger = ProofObligationLedger( + ledger_id="premise-recovery", + obligations=[root, target, descendant, alternate], + ) + critic = _premise_suspicion_text() + suspicion = extract_premise_suspicions( + critic, + {"ROOT-A"}, + )["ROOT-A"] + review = decide_premise_review( + parse_premise_audit(_audit_text(), "ROOT-A", "audit-1"), + parse_premise_defense( + _defense_text(), + "ROOT-A", + "defense-1", + ), + project_root=Path(__file__).resolve().parents[3], + suspicion=suspicion, + ) + assert apply_critic_verdicts( + ledger, + critic, + "br_premise", + {"ROOT-A"}, + premise_reviews={"ROOT-A": review}, + ) == {"ROOT-A": "DISPROVED"} + assert target.invalidation_kind == "PREMISE_INVALIDATED" + assert descendant.status == "QUARANTINED" + assert descendant.quarantine_root_id == "ROOT-A" + assert descendant.quarantine_run_id == "br_premise" + assert alternate.status == "UNRESOLVED" + assert ledger.backjump_target_id == "ROOT" + assert len(ledger.no_go_lessons) == 1 + assert ledger.no_go_lessons[0].claim_hash == suspicion.claim_hash + assert ledger.no_go_lessons[0].auditor_run_id == "audit-1" + assert ledger.no_go_lessons[0].reversible_status == "ACTIVE" + assert pending_obligations(ledger) == [alternate] + recovery_prompt = format_proof_ledger(ledger, [alternate]) + assert "For every real x, x squared equals x" in recovery_prompt + assert "never assume, rename, or propose" in recovery_prompt + apply_critic_verdicts( + ledger, + critic, + "br_repeat", + {"ROOT-A"}, + premise_reviews={"ROOT-A": review}, + ) + assert len(ledger.no_go_lessons) == 1 + apply_critic_verdicts( + ledger, + """ +### ISSUE_VERDICT ROOT-A-1 +Status: PROVED +Evidence: This attempted late verdict must not reopen a terminal quarantined descendant under any circumstance. +Missing lemma: none +""", + "br_late", + {"ROOT-A-1"}, + ) + assert descendant.status == "QUARANTINED" + assert descendant.quarantine_run_id == "br_premise" + + +def test_weak_premise_verdict_does_not_cascade(): + target = ProofObligation("ROOT-A", "Assume positivity.") + child = ProofObligation("ROOT-A-1", "Apply positivity.", parent_id="ROOT-A") + ledger = ProofObligationLedger("weak-premise", [target, child]) + critic = """ +### ISSUE_VERDICT ROOT-A +Status: DISPROVED +Invalidation: PREMISE +Premise refuted: +Evidence: This evidence is deliberately long enough, but no explicit premise is named for host validation. +Missing lemma: none +""" + verdicts = apply_critic_verdicts(ledger, critic, "br_weak", {"ROOT-A"}) + assert verdicts == {"ROOT-A": "UNRESOLVED"} + assert target.invalidation_kind == "" + assert child.status == "UNRESOLVED" + assert ledger.no_go_lessons == [] + weak_closure = _premise_suspicion_text().replace( + "Substitution of the explicit finite value x=2 gives four on the left and two on the right, contradicting universal equality.", + "too short", + ) + apply_critic_verdicts( + ledger, + weak_closure, + "br_weak_closure", + {"ROOT-A"}, + premise_reviews={"ROOT-A": PremiseReview( + "INCONCLUSIVE", + False, + reason="workers unavailable", + )}, + ) + assert target.status == "UNRESOLVED" + assert target.invalidation_kind == "" + + +def test_valid_suspicion_is_temporary_until_independent_upgrade(): + target = ProofObligation("ROOT-A", "For every real x, x squared equals x.") + child = ProofObligation("ROOT-A-1", "Use equality.", parent_id="ROOT-A") + ledger = ProofObligationLedger("suspected", [target, child]) + verdicts = apply_critic_verdicts( + ledger, + _premise_suspicion_text(), + "br_suspect", + {"ROOT-A"}, + ) + assert verdicts == {"ROOT-A": "UNRESOLVED"} + assert target.invalidation_kind == "PREMISE_SUSPECTED" + assert target.premise_review_status == "SUSPECTED" + assert child.status == "UNRESOLVED" + assert child.temporary_quarantine_root_id == "ROOT-A" + assert ledger.no_go_lessons == [] + assert pending_obligations(ledger) == [child] + + +def test_old_direct_premise_input_is_only_audited_suspicion(): + suspicions = extract_premise_suspicions( + _premise_suspicion_text("PREMISE"), + {"ROOT-A"}, + ) + assert suspicions["ROOT-A"].evidence_type == "FINITE_COUNTEREXAMPLE" + ledger = ProofObligationLedger( + "legacy-transcript", + [ProofObligation("ROOT-A", "Universal equality.")], + ) + apply_critic_verdicts( + ledger, + _premise_suspicion_text("PREMISE"), + "legacy-run", + {"ROOT-A"}, + ) + assert ledger.obligations[0].status == "UNRESOLVED" + assert ledger.obligations[0].invalidation_kind == "PREMISE_SUSPECTED" + assert ledger.no_go_lessons == [] + + +def test_audit_and_defense_parsers_and_verified_outcome_matrix(tmp_path): + audit = parse_premise_audit(_audit_text(), "ROOT-A", "audit-run") + defense = parse_premise_defense( + _defense_text(), + "ROOT-A", + "defense-run", + ) + assert audit.status == "CONFIRMED" + assert defense.status == "NOT_RESCUED" + suspicion = extract_premise_suspicions( + _premise_suspicion_text(), + {"ROOT-A"}, + )["ROOT-A"] + verified, detail = validate_evidence_artifact( + audit, + suspicion=suspicion, + project_root=tmp_path, + ) + assert verified and "4.0 == 2.0 as False" in detail + decision = decide_premise_review( + audit, + defense, + project_root=tmp_path, + suspicion=suspicion, + ) + assert decision.status == "PREMISE_INVALIDATED" + assert decision.verified + assert decision.auditor_run_id == "audit-run" + mismatched_audit = PremiseAudit( + **{ + **audit.__dict__, + "artifact": { + **audit.artifact, + "claim_hash": "0" * 64, + }, + }, + ) + assert decide_premise_review( + mismatched_audit, + defense, + project_root=tmp_path, + suspicion=suspicion, + ).status == "INCONCLUSIVE" + assert decide_premise_review( + parse_premise_audit( + _audit_text(status="NOT_CONFIRMED"), + "ROOT-A", + ), + defense, + project_root=tmp_path, + ).status == "NOT_CONFIRMED" + assert decide_premise_review( + audit, + parse_premise_defense( + _defense_text(status="RESCUED"), + "ROOT-A", + ), + project_root=tmp_path, + ).status == "RESCUED" + assert decide_premise_review( + parse_premise_audit( + _audit_text(status="INCONCLUSIVE"), + "ROOT-A", + ), + defense, + project_root=tmp_path, + ).status == "INCONCLUSIVE" + assert decide_premise_review( + parse_premise_audit( + _audit_text(confidence="0.5"), + "ROOT-A", + ), + defense, + project_root=tmp_path, + ).status == "INCONCLUSIVE" + assert decide_premise_review( + audit, + parse_premise_defense( + _defense_text(status="INCONCLUSIVE"), + "ROOT-A", + ), + project_root=tmp_path, + ).status == "INCONCLUSIVE" + + symbolic_suspicion = extract_premise_suspicions( + _premise_suspicion_text().replace( + "Evidence type: FINITE_COUNTEREXAMPLE", + "Evidence type: SYMBOLIC_CONTRADICTION", + ), + {"ROOT-A"}, + )["ROOT-A"] + symbolic = PremiseAudit( + "ROOT-A", + "CONFIRMED", + "SYMBOLIC_CONTRADICTION", + "expanded universal identity", + 0.9, + { + "claim_hash": symbolic_suspicion.claim_hash, + "claim": symbolic_suspicion.claim_schema, + "witness": {"x": 2}, + }, + "The claimed symbolic identity fails under the exact witness.", + ) + assert validate_evidence_artifact( + symbolic, + suspicion=symbolic_suspicion, + project_root=tmp_path, + )[0] + + +def test_arbitrary_true_arithmetic_cannot_invalidate_unrelated_premise( + tmp_path, +): + critic = """ +### ISSUE_VERDICT ROOT-A +Status: DISPROVED +Invalidation: PREMISE_SUSPECTED +Premise refuted: An unrelated analytic continuation premise is false. +Evidence type: FINITE_COUNTEREXAMPLE +Evidence artifact: {"claim":{"schema_version":1,"quantifier":"FOR_ALL","variables":["x"],"domain":"INTEGER","lhs":"x","relation":"!=","rhs":"2"}} +Evidence: The model attaches a true arithmetic observation to an unrelated natural-language premise and calls it a counterexample. +Missing lemma: none +""" + suspicion = extract_premise_suspicions( + critic, + {"ROOT-A"}, + )["ROOT-A"] + audit = PremiseAudit( + "ROOT-A", + "CONFIRMED", + "FINITE_COUNTEREXAMPLE", + "unrelated arithmetic", + 0.99, + { + "claim_hash": suspicion.claim_hash, + "claim": suspicion.claim_schema, + "witness": {"x": 1}, + }, + "The attached relation is true, not a counterexample.", + ) + verified, reason = validate_evidence_artifact( + audit, + suspicion=suspicion, + project_root=tmp_path, + ) + assert not verified + assert "as True" in reason + decision = decide_premise_review( + audit, + parse_premise_defense(_defense_text(), "ROOT-A"), + project_root=tmp_path, + suspicion=suspicion, + ) + assert decision.status == "INCONCLUSIVE" + ledger = ProofObligationLedger( + "unrelated-arithmetic", + [ProofObligation("ROOT-A", "Unrelated analytic continuation premise.")], + ) + apply_critic_verdicts( + ledger, + critic, + "unrelated-run", + {"ROOT-A"}, + premise_reviews={"ROOT-A": decision}, + ) + assert ledger.obligations[0].invalidation_kind == "APPROACH_FAILED" + assert ledger.no_go_lessons == [] + tampered = PremiseAudit( + **{ + **audit.__dict__, + "artifact": { + **audit.artifact, + "claim_hash": "tampered", + }, + }, + ) + assert not validate_evidence_artifact( + tampered, + suspicion=suspicion, + project_root=tmp_path, + )[0] + missing_witness = PremiseAudit( + **{ + **audit.__dict__, + "artifact": { + **audit.artifact, + "witness": {}, + }, + }, + ) + assert not validate_evidence_artifact( + missing_witness, + suspicion=suspicion, + project_root=tmp_path, + )[0] + unknown_variable = critic.replace( + '"rhs":"2"', + '"rhs":"y"', + ) + assert extract_premise_suspicions( + unknown_variable, + {"ROOT-A"}, + ) == {} + + +def test_unverified_theorem_reference_fails_open(tmp_path): + pinned_text = """ +### ISSUE_VERDICT ROOT-A +Status: DISPROVED +Invalidation: PREMISE_SUSPECTED +Premise refuted: A cited theorem contradicts the target premise. +Evidence type: PINNED_THEOREM +Evidence artifact: {"claim":{"reference":"Example Theorem 2.1","assumptions":["exact assumption A"]}} +Evidence: The citation purports to conflict with the premise under the exact listed assumption, but requires registry verification. +Missing lemma: none +""" + suspicion = extract_premise_suspicions( + pinned_text, + {"ROOT-A"}, + )["ROOT-A"] + audit = PremiseAudit( + "ROOT-A", + "CONFIRMED", + "PINNED_THEOREM", + "Example Theorem 2.1", + 0.99, + {"claim_hash": suspicion.claim_hash, "claim": suspicion.claim_schema}, + "The cited result appears relevant.", + ) + decision = decide_premise_review( + audit, + parse_premise_defense(_defense_text(), "ROOT-A"), + project_root=tmp_path, + suspicion=suspicion, + ) + assert decision.status == "INCONCLUSIVE" + assert not decision.verified + assert "no trusted local theorem registry" in decision.reason + + +def test_lean_proof_without_safe_negation_wrapper_fails_open(tmp_path): + signature_hash = "lean-target-hash" + lean_text = f""" +### ISSUE_VERDICT ROOT-A +Status: DISPROVED +Invalidation: PREMISE_SUSPECTED +Premise refuted: The formalized target proposition has a constructive negation. +Evidence type: LEAN_PROOF +Evidence artifact: {{"claim":{{"schema_version":1,"contract":"NEGATION_OF_TARGET_SIGNATURE","lean_signature_hash":"{signature_hash}"}}}} +Evidence: A complete Lean proof is proposed against the exact host-recorded target signature, subject to safe wrapper validation. +Missing lemma: none +""" + suspicion = extract_premise_suspicions( + lean_text, + {"ROOT-A"}, + {"ROOT-A": signature_hash}, + )["ROOT-A"] + audit = PremiseAudit( + "ROOT-A", + "CONFIRMED", + "LEAN_PROOF", + "generated Lean theorem", + 0.99, + { + "claim_hash": suspicion.claim_hash, + "claim": suspicion.claim_schema, + "lean_signature_hash": signature_hash, + "contract": "NEGATION_OF_TARGET_SIGNATURE", + "source": "theorem contradiction : False := by trivial", + }, + "Lean artifact supplied.", + "audit-lean", + ) + + verified, reason = validate_evidence_artifact( + audit, + suspicion=suspicion, + project_root=tmp_path, + ) + assert not verified + assert "cannot be safely transformed" in reason + assert extract_premise_suspicions( + lean_text, + {"ROOT-A"}, + {"ROOT-A": "different-host-signature-hash"}, + ) == {} + tampered = PremiseAudit( + **{ + **audit.__dict__, + "artifact": { + **audit.artifact, + "lean_signature_hash": "tampered", + }, + }, + ) + assert not validate_evidence_artifact( + tampered, + suspicion=suspicion, + project_root=tmp_path, + )[0] + rejected = validate_lean_proof( + "theorem incomplete : True := by sorry", + project_root=tmp_path, + ) + assert not rejected.ok + assert rejected.status == "UNSAFE_REJECTED" + + +def test_complete_minimal_lean_reduction_proof_is_accepted(): + result = validate_lean_proof( + "theorem certifiedReduction (h : True) : True := by exact h", + project_root=Path(__file__).resolve().parents[3], + ) + assert result.ok + assert result.status == "PROVED" + + +def test_worker_roles_are_isolated_ordered_and_fail_open(tmp_path): + suspicion = extract_premise_suspicions( + _premise_suspicion_text(), + {"ROOT-A"}, + )["ROOT-A"] + calls = [] + + def runner(role, messages): + calls.append((role, messages)) + if role == "premise_auditor": + return _audit_text(), "audit-run" + assert _audit_text().strip() in messages[-1]["content"] + assert suspicion.claim_hash in messages[-1]["content"] + return _defense_text(), "defense-run" + + audit, defense, transcripts = run_isolated_premise_review( + "prove target", + suspicion, + runner, + ) + assert [role for role, _ in calls] == [ + "premise_auditor", + "adversarial_proponent", + ] + assert calls[0][1] is not calls[1][1] + assert "COMPLETE ISOLATED AUDITOR OUTPUT" not in calls[0][1][-1]["content"] + assert audit.run_id == "audit-run" + assert defense.run_id == "defense-run" + assert transcripts["auditor"] == _audit_text() + + failed_calls = [] + + def failing_runner(role, _messages): + failed_calls.append(role) + raise TimeoutError(f"{role} timed out") + + failed_audit, failed_defense, failed_transcripts = ( + run_isolated_premise_review( + "prove target", + suspicion, + failing_runner, + ) + ) + assert failed_calls == ["premise_auditor", "adversarial_proponent"] + assert failed_audit is None and failed_defense is None + assert "EXECUTION FAILED" in failed_transcripts["auditor"] + failed_decision = decide_premise_review( + failed_audit, + failed_defense, + project_root=tmp_path, + ) + assert failed_decision.status == "INCONCLUSIVE" + failed_ledger = ProofObligationLedger( + "worker-failure", + [ProofObligation("ROOT-A", "Failed attempted approach.")], + ) + apply_critic_verdicts( + failed_ledger, + _premise_suspicion_text(), + "failed-review-run", + {"ROOT-A"}, + premise_reviews={"ROOT-A": failed_decision}, + ) + assert failed_ledger.obligations[0].status == "DISPROVED" + assert failed_ledger.obligations[0].invalidation_kind == "APPROACH_FAILED" + assert failed_ledger.no_go_lessons == [] + + +def test_rescued_review_reverses_quarantine_and_no_go(): + root = ProofObligation("ROOT", "Main unresolved reduction.") + target = ProofObligation("ROOT-A", "Universal equality.", parent_id="ROOT") + child = ProofObligation("ROOT-A-1", "Dependent lemma.", parent_id="ROOT-A") + ledger = ProofObligationLedger("reversible", [root, target, child]) + confirmed = PremiseReview( + "PREMISE_INVALIDATED", + True, + 0.95, + "FINITE_COUNTEREXAMPLE", + "host arithmetic substitution", + "audit-1", + "defense-1", + ) + apply_critic_verdicts( + ledger, + _premise_suspicion_text(), + "br_confirm", + {"ROOT-A"}, + premise_reviews={"ROOT-A": confirmed}, + ) + assert child.status == "QUARANTINED" + rescued = PremiseReview( + "RESCUED", + False, + 0.9, + "FINITE_COUNTEREXAMPLE", + "domain check", + "audit-2", + "defense-2", + "The original domain excluded x=2.", + ) + apply_critic_verdicts( + ledger, + _premise_suspicion_text(), + "br_rescue", + {"ROOT-A"}, + premise_reviews={"ROOT-A": rescued}, + ) + assert target.status == "DISPROVED" + assert target.invalidation_kind == "APPROACH_FAILED" + assert target.premise_review_status == "RESCUED" + assert target.premise_auditor_run_id == "audit-2" + assert child.status == "UNRESOLVED" + assert child.quarantine_reversible_status == "REVERSED" + assert child.temporary_quarantine_root_id == "" + assert ledger.no_go_lessons[0].reversible_status == "REVERSED" + assert ledger.backjump_target_id == "" + + +def test_all_nonupgrade_reviews_close_only_approach_without_no_go(): + for review_status in ("NOT_CONFIRMED", "RESCUED", "INCONCLUSIVE"): + root = ProofObligation("ROOT", "Sound parent.") + target = ProofObligation( + "ROOT-A", + "For every real x, x squared equals x.", + parent_id="ROOT", + ) + child = ProofObligation( + "ROOT-A-1", + "Historical alternate descendant.", + parent_id="ROOT-A", + ) + ledger = ProofObligationLedger( + f"fallback-{review_status}", + [root, target, child], + ) + apply_critic_verdicts( + ledger, + _premise_suspicion_text(), + f"run-{review_status}", + {"ROOT-A"}, + premise_reviews={"ROOT-A": PremiseReview( + review_status, + False, + 0.6, + "FINITE_COUNTEREXAMPLE", + "independent worker result", + f"audit-{review_status}", + f"defense-{review_status}", + f"{review_status} fallback", + )}, + ) + assert target.status == "DISPROVED" + assert target.invalidation_kind == "APPROACH_FAILED" + assert target.premise_review_status == review_status + assert target.premise_review_reason == f"{review_status} fallback" + assert child.status == "UNRESOLVED" + assert child.temporary_quarantine_root_id == "" + assert child.quarantine_root_id == "" + assert ledger.no_go_lessons == [] + assert ledger.backjump_target_id == "" + + +def test_approach_invalidation_does_not_quarantine_descendants_or_siblings(): + target = ProofObligation("ROOT-A", "Try a contour-shift proof.") + child = ProofObligation( + "ROOT-A-1", + "Try a different contour under the same target.", + parent_id="ROOT-A", + ) + sibling = ProofObligation("ROOT-B", "Try a spectral proof.") + ledger = ProofObligationLedger("approach-only", [target, child, sibling]) + critic = """ +### ISSUE_VERDICT ROOT-A +Status: DISPROVED +Evidence: The attempted contour crosses an uncontrolled pole, so this derivation fails even though the target statement may still hold. +Missing lemma: none +""" + apply_critic_verdicts(ledger, critic, "br_approach", {"ROOT-A"}) + assert target.invalidation_kind == "APPROACH_FAILED" + assert child.status == "UNRESOLVED" + assert sibling.status == "UNRESOLVED" + assert {item.obligation_id for item in pending_obligations(ledger)} == { + "ROOT-A-1", + "ROOT-B", + } + + +def test_no_go_lesson_rejects_semantically_repeated_child(): + ledger = ProofObligationLedger( + "no-go", + [ProofObligation("ROOT", "Find a valid replacement argument.")], + ) + premise = "For every real x, x squared equals x." + source = ProofObligation("OLD", premise) + old_ledger = ProofObligationLedger("old", [source]) + apply_critic_verdicts( + old_ledger, + _premise_suspicion_text().replace("ROOT-A", "OLD"), + "br_old", + {"OLD"}, + premise_reviews={"OLD": PremiseReview( + "PREMISE_INVALIDATED", + True, + 0.95, + "FINITE_COUNTEREXAMPLE", + "host arithmetic substitution", + "audit-old", + "defense-old", + )}, + ) + ledger.no_go_lessons = old_ledger.no_go_lessons + rejections = [] + created = create_child_obligations( + ledger, + """ +### ISSUE_VERDICT ROOT +Status: UNRESOLVED +Evidence: A replacement argument is still required. +Missing lemma: Prove that for every real x, x squared equals x. +""", + "br_new", + {"ROOT"}, + rejections, + {"ROOT": _valid_lean_signature()}, + certified_only=False, + ) + assert created == [] + assert "no-go premise" in rejections[0] + + +def test_v1_ledger_loads_without_recovery_metadata(tmp_path): + path = tmp_path / "legacy-ledger.json" + path.write_text(json.dumps({ + "ledger_id": "legacy", + "obligations": [{ + "obligation_id": "ROOT", + "statement": "Legacy unresolved statement.", + "status": "UNRESOLVED", + "parent_id": "", + }], + "no_go_lessons": [{ + "claim_hash": "legacy-hash", + "refuted_premise": "Legacy premise.", + "evidence": "Legacy evidence.", + "source_obligation_id": "ROOT", + "run_id": "legacy-run", + }], + "version": 1, + "schema_version": 1, + })) + ledger = load_proof_ledger(path) + assert ledger.no_go_lessons[0].confidence == 0.0 + assert ledger.no_go_lessons[0].reversible_status == "ACTIVE" + assert ledger.backjump_target_id == "" + assert ledger.obligations[0].invalidation_kind == "" + assert ledger.obligations[0].decomposition_certificate_hash == "" + assert ledger.obligations[0].dependency_ids == [] + assert ledger.obligations[0].public_assumptions == [] + + +def test_free_form_missing_lemma_cannot_persist_child(): ledger = ProofObligationLedger( ledger_id="rh-ledger", obligations=[ProofObligation("RH-C2", "Prove zero convergence.")], @@ -526,27 +1611,308 @@ def test_missing_lemma_creates_deduplicated_child_and_selects_leaf(): **Missing lemma:** Prove locally uniform convergence on every compact subset of the critical strip. """ apply_critic_verdicts(ledger, critic, "br_first") + rejections = [] created = create_child_obligations( ledger, critic, "br_first", {"RH-C2"}, - None, + rejections, {"RH-C2": _valid_lean_signature()}, ) + assert created == [] + assert len(ledger.obligations) == 1 + assert "verified decomposition certificate" in rejections[0] + + +def test_valid_certified_decomposition_runs_seven_roles_and_persists(tmp_path): + parent = ProofObligation( + "ROOT", + "Establish the global convergence theorem for analytic approximants.", + ) + ledger = ProofObligationLedger("certified", [parent]) + runner, calls = _certificate_runner() + result = run_certified_decomposition( + ledger, + "ROOT", + "Immutable root goal", + runner, + project_root=tmp_path, + orchestration_id="orch-1", + signature_validator=_fake_signature_validator, + proof_validator=_fake_proof_validator, + ) + assert [call[0] for call in calls] == [ + "definition_auditor", + "counterexample_worker", + "decomposer", + "formalizer", + "prover", + "adversarial_proponent", + "judge", + ] + assert len({id(call[1]) for call in calls}) == 7 + for index, (_role, messages, expected_run_id) in enumerate(calls): + package = json.loads(messages[-1]["content"]) + assert package["producer_run_id"] == expected_run_id + if index: + assert package["upstream_artifact_hashes"] + packages = { + role: json.loads(messages[-1]["content"]) + for role, messages, _run_id in calls + } + assert set( + packages["formalizer"]["validated_upstream_artifacts"], + ) == {"decomposer"} + assert set( + packages["prover"]["validated_upstream_artifacts"], + ) == {"formalizer"} + assert "definition_auditor" not in ( + packages["prover"]["validated_upstream_artifacts"] + ) + assert result.verified + assert ledger.obligations == [parent] + created = persist_verified_decomposition( + ledger, + "ROOT", + result, + "run-certified", + ) assert len(created) == 1 - assert created[0].parent_id == "RH-C2" - assert created[0].formal_status == "FORMALIZED" - assert created[0].lean_signature_hash == "lean-signature-hash" - assert pending_obligations(ledger) == created - assert create_child_obligations( + assert created[0].obligation_id.startswith("ROOT-") + assert created[0].decomposition_certificate_hash + assert created[0].reduction_theorem_status == "PROVED" + assert created[0].certificate_reversible_status == "ACTIVE" + assert parent.formal_status == "FORMALIZED" + manifest = tmp_path / "reviews" / "manifest.json" + save_decomposition_manifest(manifest, { + "verified": result.verified, + "transcripts": result.transcripts, + "artifact_hashes": result.artifact_hashes, + }) + assert manifest.stat().st_mode & 0o777 == 0o600 + + +def test_certificate_parser_rejects_tampered_bindings_for_every_role( + tmp_path, +): + ledger = ProofObligationLedger( + "bindings", + [ProofObligation( + "ROOT", + "Establish the global convergence theorem for analytic approximants.", + )], + ) + runner, calls = _certificate_runner() + result = run_certified_decomposition( ledger, - critic, - "br_repeat", - {"RH-C2"}, - None, - {"RH-C2": _valid_lean_signature()}, + "ROOT", + "Immutable root goal", + runner, + project_root=tmp_path, + orchestration_id="orch-bind", + signature_validator=_fake_signature_validator, + proof_validator=_fake_proof_validator, + ) + headings = [ + "DEFINITION_AUDIT", + "COUNTEREXAMPLE_REPORT", + "DECOMPOSITION_PROPOSAL", + "FORMALIZATION_BUNDLE", + "PROOF_ATTEMPT", + "DEFENSE_REPORT", + "JUDGE_DECISION", + ] + for heading, (role, messages, expected_run_id) in zip(headings, calls): + package = json.loads(messages[-1]["content"]) + upstream = package["upstream_artifact_hashes"] + artifact, error = parse_certified_artifact( + result.transcripts[role], + heading, + target_obligation_id="ROOT", + parent_statement_hash="tampered", + root_goal_hash=package["root_goal_hash"], + producer_run_id=expected_run_id, + upstream_artifact_hashes=upstream, + ) + assert artifact is None + assert "tampered" in error + + +def test_certificate_timeout_or_malformed_role_never_mutates_ledger(tmp_path): + ledger = ProofObligationLedger( + "fail-open", + [ProofObligation( + "ROOT", + "Establish the global convergence theorem for analytic approximants.", + )], + ) + before = asdict(ledger) + runner, _calls = _certificate_runner() + + def timeout_runner(role, messages, expected_run_id): + if role == "counterexample_worker": + raise TimeoutError("worker timeout") + return runner(role, messages, expected_run_id) + + result = run_certified_decomposition( + ledger, + "ROOT", + "Immutable root goal", + timeout_runner, + project_root=tmp_path, + orchestration_id="orch-timeout", + signature_validator=_fake_signature_validator, + proof_validator=_fake_proof_validator, + ) + assert not result.verified + assert persist_verified_decomposition( + ledger, + "ROOT", + result, + "run-timeout", ) == [] + assert asdict(ledger) == before + + def oversized_runner(_role, _messages, _expected_run_id): + raise SemanticUnitTooLarge("formal artifact", 2053, 2052) + + oversized = run_certified_decomposition( + ledger, + "ROOT", + "Immutable root goal", + oversized_runner, + project_root=tmp_path, + orchestration_id="orch-oversized", + signature_validator=_fake_signature_validator, + proof_validator=_fake_proof_validator, + ) + assert not oversized.verified + assert "SEMANTIC_UNIT_TOO_LARGE" in oversized.errors[0] + assert asdict(ledger) == before + + +def test_certificate_graph_proof_parent_child_and_judge_gates(tmp_path): + cases = [ + ({"cycle": True}, "acyclic"), + ({"proof_source": "theorem reduction (h : True) : True := by sorry"}, "complete reduction proof"), + ({"child_signature": "theorem badChild : True := by sorry"}, "child L1 signature failed"), + ({"judge_decision": "REJECT"}, "Judge decision"), + ({"multi_child": True}, "exactly one child"), + ({ + "counterexample_case": { + "evidence_type": "PINNED_THEOREM", + "reference": "Unsupported Theorem 1", + }, + }, "no verified evidence"), + ({ + "counterexample_case": { + "evidence_type": "FINITE_COUNTEREXAMPLE", + "evidence_source": "host arithmetic evaluator", + "claim": { + "schema_version": 1, + "quantifier": "FOR_ALL", + "variables": ["x"], + "domain": "REAL", + "lhs": "x*x", + "relation": "==", + "rhs": "x", + }, + "witness": {"x": 2}, + }, + }, "verified counterexample refutes the parent"), + ] + for index, (options, expected_error) in enumerate(cases): + ledger = ProofObligationLedger( + f"invalid-{index}", + [ProofObligation( + "ROOT", + "Establish the global convergence theorem for analytic approximants.", + )], + ) + runner, _calls = _certificate_runner(**options) + result = run_certified_decomposition( + ledger, + "ROOT", + "Immutable root goal", + runner, + project_root=tmp_path, + orchestration_id=f"orch-invalid-{index}", + signature_validator=_fake_signature_validator, + proof_validator=_fake_proof_validator, + ) + assert not result.verified + assert any(expected_error in error for error in result.errors) + assert len(ledger.obligations) == 1 + + existing_source = "theorem boundParent : True := by sorry" + existing = ProofObligation( + "ROOT", + "Establish the global convergence theorem for analytic approximants.", + formal_status="FORMALIZED", + lean_signature=existing_source, + lean_signature_hash=lean_theorem_signature_hash(existing_source), + ) + ledger = ProofObligationLedger("parent-mismatch", [existing]) + runner, _calls = _certificate_runner(parent_hash_override="wrong-hash") + result = run_certified_decomposition( + ledger, + "ROOT", + "Immutable root goal", + runner, + project_root=tmp_path, + orchestration_id="orch-parent-mismatch", + signature_validator=_fake_signature_validator, + proof_validator=_fake_proof_validator, + ) + assert not result.verified + assert any("parent signature" in error for error in result.errors) + + +def test_judge_cannot_override_failed_host_graph_gate(tmp_path): + ledger = ProofObligationLedger( + "judge-host", + [ProofObligation( + "ROOT", + "Establish the global convergence theorem for analytic approximants.", + )], + ) + runner, _calls = _certificate_runner(cycle=True, judge_decision="ACCEPT") + result = run_certified_decomposition( + ledger, + "ROOT", + "Immutable root goal", + runner, + project_root=tmp_path, + orchestration_id="orch-judge", + signature_validator=_fake_signature_validator, + proof_validator=_fake_proof_validator, + ) + assert result.artifacts["judge"].decision == "ACCEPT" + assert not result.verified + assert not result.validation["host_gates_passed"] + + +def test_certified_trigger_skips_proved_and_detects_frontiers(): + unresolved = """ +### ISSUE_VERDICT ROOT +Status: UNRESOLVED +Evidence: A precise reduction is still missing from the attempted argument. +Missing lemma: Prove a compact boundary inequality. +""" + proved = """ +### ISSUE_VERDICT ROOT +Status: PROVED +Evidence: This sufficiently detailed complete derivation closes the exact target obligation. +Missing lemma: none +""" + assert certified_decomposition_requested(unresolved, "", {"ROOT"}) + assert not certified_decomposition_requested(proved, "", {"ROOT"}) + assert certified_decomposition_requested( + "", + "### ISSUE_RESPONSE ROOT\nRemaining gap: Define the exact topology.", + {"ROOT"}, + ) def test_host_generated_autoresearch_verdict_uses_new_child_frontier(): @@ -558,6 +1924,8 @@ def test_host_generated_autoresearch_verdict_uses_new_child_frontier(): "RH-C2-child", "Prove locally uniform convergence on compact subsets.", parent_id="RH-C2", + decomposition_certificate_hash="certificate-hash", + reduction_theorem_status="PROVED", ), ], ) @@ -574,9 +1942,16 @@ class Candidate: ) assert verdict["outcome"] == "DECOMPOSED" assert verdict["created_obligation_ids"] == ["RH-C2-child"] + ledger.obligations[1].decomposition_certificate_hash = "" + assert build_autoresearch_verdict( + Candidate, + ledger, + {"RH-C2": "UNRESOLVED"}, + [ledger.obligations[1]], + )["outcome"] == "INCONCLUSIVE" -def test_critic_leaf_table_creates_all_target_children_only(): +def test_critic_leaf_table_cannot_bypass_certificate(): ledger = ProofObligationLedger( ledger_id="rh-ledger", obligations=[ @@ -613,13 +1988,9 @@ def test_critic_leaf_table_creates_all_target_children_only(): }, ) assert applied == {"RH-C2": "UNRESOLVED"} - assert len(created) == 2 - assert all(item.parent_id == "RH-C2" for item in created) + assert created == [] assert ledger.obligations[0].last_run_id == "" - assert pending_obligations(ledger) == [ - ledger.obligations[0], - *created, - ] + assert pending_obligations(ledger) == ledger.obligations def test_corrupted_critic_id_binds_to_single_host_target(): @@ -684,6 +2055,7 @@ def test_cycle_and_invented_ids_cannot_create_children(): "br_cycle", {target.obligation_id}, rejections, + certified_only=False, ) assert created == [] assert len(ledger.obligations) == 2 @@ -740,6 +2112,9 @@ def test_recover_complete_checkpoint_from_timestamped_log(tmp_path): "[t] [allens] Critic Prefill: 100 tokens...", "[t] critic> first critic line", "[t] second critic line", + "[t] [premise-suspected] id=ROOT-A", + "[t] premise_auditor> complete auditor transcript", + "[t] adversarial_proponent> complete defense transcript", "[t] [metrics] run=br_good", )), ) diff --git a/tests/inference_engine/distributed/test_mlx_ring.py b/tests/inference_engine/distributed/test_mlx_ring.py index d44809ee..04af48e4 100644 --- a/tests/inference_engine/distributed/test_mlx_ring.py +++ b/tests/inference_engine/distributed/test_mlx_ring.py @@ -37,6 +37,25 @@ def test_probe_never_raises_and_is_structured(): assert env.world_size == 0 +def test_probe_reports_import_failure_on_every_platform(monkeypatch): + def fail_import(_name): + raise ImportError("synthetic missing mlx") + + monkeypatch.setattr( + "inference_engine.distributed.mlx_ring.importlib.import_module", + fail_import, + ) + env = probe_ring_environment() + assert not env.is_available + assert env.backend == "" + assert env.rank == 0 + assert env.world_size == 0 + assert env.failure_reason == ( + "mlx.core.distributed import failed: " + "ImportError: synthetic missing mlx" + ) + + @pytest.mark.skipif( platform.machine() == "arm64", reason="Linux-gate branch: asserts the mlx-absent probe result",