From 5e52475e5400bb7e5957dfe2ac1ba0cdbb5da3e2 Mon Sep 17 00:00:00 2001 From: fluffy314 Date: Sun, 26 Jul 2026 16:57:48 +0800 Subject: [PATCH] feat(autoresearch): resolve proof plans autonomously Turn theorem evidence and atomic definition gaps into deterministic, versioned plan candidates so proof search can progress without activating supervisor dispatch yet. Co-authored-by: Cursor --- autoresearch/prefill/architecture_v7.py | 455 +++++++++++ autoresearch/prefill/atomic_definition.py | 554 +++++++++++++ .../prefill/creative_decomposition.py | 649 ++++++++++++++++ autoresearch/prefill/definition_resolution.py | 735 ++++++++++++++++++ autoresearch/prefill/evidence_planner.py | 470 +++++++++++ autoresearch/prefill/research_contract.py | 190 +++++ autoresearch/prefill/stepwise_proof.py | 465 +++++++++++ autoresearch/prefill/strategy_tournament.py | 480 ++++++++++++ autoresearch/prefill/theorem_cards.py | 196 +++++ .../migrate_atomic_define_one_concept_v1.py | 238 ++++++ ...ate_autonomous_definition_resolution_v1.py | 167 ++++ scripts/migrate_creative_decomposition_v3.py | 253 ++++++ .../migrate_research_contract_preproof_v2.py | 194 +++++ scripts/migrate_strategy_tournament_v1.py | 285 +++++++ .../bench/test_atomic_definition.py | 352 +++++++++ .../bench/test_creative_decomposition.py | 501 ++++++++++++ .../bench/test_definition_resolution.py | 231 ++++++ .../test_strategy_tournament_stepwise.py | 535 +++++++++++++ 18 files changed, 6950 insertions(+) create mode 100644 autoresearch/prefill/architecture_v7.py create mode 100644 autoresearch/prefill/atomic_definition.py create mode 100644 autoresearch/prefill/creative_decomposition.py create mode 100644 autoresearch/prefill/definition_resolution.py create mode 100644 autoresearch/prefill/evidence_planner.py create mode 100644 autoresearch/prefill/research_contract.py create mode 100644 autoresearch/prefill/stepwise_proof.py create mode 100644 autoresearch/prefill/strategy_tournament.py create mode 100644 autoresearch/prefill/theorem_cards.py create mode 100644 scripts/migrate_atomic_define_one_concept_v1.py create mode 100644 scripts/migrate_autonomous_definition_resolution_v1.py create mode 100644 scripts/migrate_creative_decomposition_v3.py create mode 100644 scripts/migrate_research_contract_preproof_v2.py create mode 100644 scripts/migrate_strategy_tournament_v1.py create mode 100644 tests/inference_engine/bench/test_atomic_definition.py create mode 100644 tests/inference_engine/bench/test_creative_decomposition.py create mode 100644 tests/inference_engine/bench/test_definition_resolution.py create mode 100644 tests/inference_engine/bench/test_strategy_tournament_stepwise.py diff --git a/autoresearch/prefill/architecture_v7.py b/autoresearch/prefill/architecture_v7.py new file mode 100644 index 0000000..d317608 --- /dev/null +++ b/autoresearch/prefill/architecture_v7.py @@ -0,0 +1,455 @@ +"""Single architecture-7 entry point for tournament and contract routing.""" +from __future__ import annotations + +import json +from dataclasses import asdict +from pathlib import Path +from typing import Mapping + +from autoresearch.prefill.definition_resolution import ( + build_definition_query, + load_resolution_store, + resolve_one_concept, +) +from autoresearch.prefill.orchestration_state import ( + OrchestrationCheckpoint, + ProofState, + persist_validated_artifact, + save_checkpoint, +) +from autoresearch.prefill.research_contract import gate_research_contract +from autoresearch.prefill.strategy_tournament import ( + CriticReason, + StrategyEvent, + build_host_plans, + evaluate_feasibility, + run_tournament, +) +from autoresearch.prefill.theorem_cards import ( + build_theorem_card_index, + pinned_environment_hash, +) + + +def _definition_audit( + checkpoint: OrchestrationCheckpoint, +) -> tuple[tuple[str, ...], tuple[str, ...], tuple[str, ...], str]: + reference = checkpoint.validated_artifacts.get("definition_auditor") + if reference is None: + return (), (), (), "" + try: + payload = json.loads(Path(reference.path).read_text(encoding="utf-8")) + except (OSError, TypeError, ValueError, json.JSONDecodeError): + return (), (), (), reference.sha256 + registered = tuple(sorted({ + str(item.get("definition_id", "")) + for item in payload.get("definitions", ()) + if isinstance(item, Mapping) and item.get("definition_id") + })) + unresolved = tuple(sorted({ + str(item.get("definition_id", "")) + for item in payload.get("missing_definitions", ()) + if isinstance(item, Mapping) and item.get("definition_id") + })) + gaps = tuple(f"gap:definition:{item}" for item in unresolved) + return registered, unresolved, gaps, reference.sha256 + + +def run_host_definition_gate( + checkpoint_path: Path, + checkpoint: OrchestrationCheckpoint, + *, + project_root: Path, +) -> tuple[OrchestrationCheckpoint, str]: + """Execute exactly one Autonomous Definition Resolution transaction.""" + if checkpoint.proof_state not in { + ProofState.DEFINITION_RESOLUTION, + ProofState.DECOMPOSER, + ProofState.STRATEGY_TOURNAMENT, + ProofState.MATHEMATICAL_STAGNATION, + }: + return checkpoint, "" + reference = checkpoint.validated_artifacts.get("definition_auditor") + if reference is None: + return checkpoint, "" + try: + audit = json.loads(Path(reference.path).read_text(encoding="utf-8")) + except (OSError, TypeError, ValueError, json.JSONDecodeError): + return checkpoint, "" + missing = tuple( + item for item in audit.get("missing_definitions", ()) + if isinstance(item, Mapping) and item.get("definition_id") + ) + if not missing: + return checkpoint, "" + base_environment_hash = pinned_environment_hash(project_root) + store_path = checkpoint_path.with_name( + "proof_orchestration.definition_resolution.json", + ) + store = load_resolution_store(store_path, base_environment_hash) + requested = checkpoint.current_definition_gap_id + gap = next( + ( + item for item in missing + if str(item.get("definition_id", "")) == requested + ), + None, + ) if requested else None + if gap is None: + committed = set(store.get("commits", {})) + gap = next( + ( + item for item in missing + if str(item.get("definition_id", "")) not in committed + ), + None, + ) + if gap is None: + checkpoint.current_definition_gap_id = "" + checkpoint.lean_definition_status = "NO_OPEN_DEFINITION_QUERY" + checkpoint.stagnation_reason = "NO_OPEN_DEFINITION_QUERY" + save_checkpoint(checkpoint_path, checkpoint) + return checkpoint, "NO_OPEN_DEFINITION_QUERY" + gap_id = str(gap["definition_id"]) + if checkpoint.proof_state != ProofState.DEFINITION_RESOLUTION: + checkpoint.transition( + ProofState.DEFINITION_RESOLUTION, + "missing-concept:autonomous-definition-resolution", + strategy_reused=True, + ) + evidence_refs = { + role: item.sha256 + for role, item in checkpoint.validated_artifacts.items() + } + query = build_definition_query( + gap, + parent_hash=( + checkpoint.parent_statement_sha256 + or checkpoint.proposition_hash + or checkpoint.target_obligation_id + ), + typed_ir_hash=checkpoint.typed_ir_hash, + auditor_hash=reference.sha256, + critic_evidence_hashes=( + evidence_refs.get("critic", ""), + evidence_refs.get("adversarial_proponent", ""), + ), + counterexample_evidence_hashes=( + evidence_refs.get("counterexample_worker", ""), + ), + theorem_dependencies=checkpoint.theorem_card_ids, + environment_hash=base_environment_hash, + prior_failure_hashes=checkpoint.forbidden_semantic_fingerprints, + ) + history = [ + value for value in store.get("historical_audit", {}).values() + if value.get("semantic_validation") == "VERIFIED" + ] + result = resolve_one_concept( + query=query, + store_path=store_path, + project_root=project_root, + source_context={"validated_history": history}, + ) + checkpoint.current_definition_gap_id = gap_id + checkpoint.definition_query_hash = result.query_hash + checkpoint.definition_candidate_count = len(result.candidate_hashes) + checkpoint.candidate_count = len(result.candidate_hashes) + checkpoint.selected_move_id = "RESOLVE_ONE_DEFINITION_QUERY" + checkpoint.active_gate = "AUTONOMOUS_DEFINITION_RESOLUTION" + checkpoint.lean_definition_status = result.status + checkpoint.definition_store_hash = result.store_hash_after + checkpoint.definition_environment_hash = result.environment_hash_after + checkpoint.definition_store_hash_delta = ( + f"{result.store_hash_before}->{result.store_hash_after}" + ) + checkpoint.definition_environment_hash_delta = ( + f"{result.environment_hash_before}->{result.environment_hash_after}" + ) + checkpoint.definition_source_statuses = { + item.source_id: item.status for item in result.source_statuses + } + checkpoint.definition_property_statuses = { + key: dict(value) for key, value in result.property_statuses.items() + } + checkpoint.definition_branch_hashes = list(result.branch_hashes) + checkpoint.definition_exhaustion_hash = result.exhaustion_hash + checkpoint.definition_interface_hash = result.interface_hash + committed = int(result.status == "COMMITTED") + checkpoint.progress_vector = { + "definitions_added": committed, + "existing_definitions_resolved": 0, + "lemmas_proved": 0, + "accepted_children": 0, + "subgoals_closed": 0, + "verified_counterexamples": 0, + } + checkpoint.definitions_added += committed + checkpoint.new_elaborated_definitions = checkpoint.definitions_added + persist_validated_artifact( + checkpoint_path, + checkpoint, + role="definition_resolution", + payload={"schema_version": 1, **asdict(result)}, + dependencies=[reference.sha256], + source_run_id=f"host:definition-resolution:{gap_id}", + ) + checkpoint.semantic_stagnation_count = 0 + checkpoint.stagnation_reason = result.status + ":" + result.reason + if result.query_hash not in checkpoint.forbidden_semantic_fingerprints: + checkpoint.forbidden_semantic_fingerprints.append(result.query_hash) + if result.status == "COMMITTED": + checkpoint.stagnation_reason = "" + checkpoint.transition( + ProofState.STRATEGY_TOURNAMENT, + "definition-resolution-commit:environment-changed", + strategy_reused=False, + ) + elif result.status == "PARENT_STATEMENT_UNDERSPECIFIED": + checkpoint.transition( + ProofState.PARENT_STATEMENT_UNDERSPECIFIED, + "definition-interpretations-change-parent-truth", + strategy_reused=True, + ) + checkpoint.definition_backjump_target = ( + checkpoint.parent_statement_sha256 or checkpoint.root_goal_sha256 + ) + checkpoint.transition( + ProofState.PREMISE_AUDIT, + "parent-statement-underspecified:premise-audit-and-backjump", + strategy_reused=True, + ) + elif result.status == "INTERFACE_REQUIRED": + checkpoint.definition_backjump_target = ( + checkpoint.parent_statement_sha256 or checkpoint.root_goal_sha256 + ) + checkpoint.transition( + ProofState.PREMISE_AUDIT, + "definition-exhaustion:conditional-interface-axioms-required", + strategy_reused=True, + ) + else: + checkpoint.definition_backjump_target = ( + checkpoint.parent_statement_sha256 or checkpoint.root_goal_sha256 + ) + checkpoint.transition( + ProofState.PARENT_STATEMENT_UNDERSPECIFIED, + "definition-exhaustion:no-viable-interface:typed-backjump", + strategy_reused=True, + ) + save_checkpoint(checkpoint_path, checkpoint) + return checkpoint, result.status + + +def _target_is_quarantined( + checkpoint: OrchestrationCheckpoint, + target_ref: str, +) -> bool: + for review in checkpoint.branch_history.values(): + if str(review.get("status", "")).upper() != "QUARANTINED": + continue + recorded_targets = { + str(item) + for key in ("plan_ids", "evidence_ids") + for item in review.get(key, ()) + } + if target_ref in recorded_targets: + return True + return False + + +def run_architecture_v7_entry( + checkpoint_path: Path, + checkpoint: OrchestrationCheckpoint, + *, + project_root: Path, + target_ref: str, + parent_obligation_ref: str, + parent_complexity: int, + event_type: StrategyEvent, + event_id: str, + elaborated_theorem_id: str = "", + proposition_hash: str = "", +) -> OrchestrationCheckpoint: + """Run exactly once per strategy event; never once per outer iteration.""" + if checkpoint.proof_state != ProofState.STRATEGY_TOURNAMENT: + return checkpoint + cards = build_theorem_card_index(project_root) + card_ids = tuple(card.card_id for card in cards) + environment_hash = pinned_environment_hash(project_root) + ( + definitions, + unresolved_definitions, + definition_gap_ids, + definition_auditor_hash, + ) = _definition_audit(checkpoint) + dependencies = tuple( + reference.sha256 + for role, reference in sorted(checkpoint.validated_artifacts.items()) + if role not in {"strategy", "generator", "critic"} + ) + evidence_refs = (*dependencies, *checkpoint.advisory_artifacts) + plans = build_host_plans( + target_ref=target_ref, + parent_obligation_ref=parent_obligation_ref, + parent_complexity=max(5, int(parent_complexity)), + environment_hash=environment_hash, + registered_definition_ids=definitions, + theorem_card_ids=card_ids, + dependency_ids=dependencies, + evidence_refs=evidence_refs, + unresolved_definition_ids=unresolved_definitions, + definition_gap_ids=definition_gap_ids, + definition_auditor_hash=definition_auditor_hash, + elaborated_theorem_id=elaborated_theorem_id, + proposition_hash=proposition_hash, + ) + decisions = evaluate_feasibility( + plans, + registered_definition_ids=definitions, + resolved_dependency_ids=dependencies, + verified_theorem_card_ids=card_ids, + allowed_assumption_ids=(), + no_go_hashes=tuple(checkpoint.invalidated_artifacts), + ) + tournament = run_tournament( + event_id=event_id, + event_type=event_type, + plans=plans, + decisions=decisions, + critic_ranked_plan_ids=tuple(plan.plan_id for plan in reversed(plans)), + critic_reason_codes=(CriticReason.MAXIMIZES_INFORMATION_GAIN,), + ) + checkpoint.strategy_event_id = event_id + checkpoint.strategy_event_type = event_type.value + checkpoint.strategy_plan_ids = [plan.plan_id for plan in plans] + checkpoint.feasible_strategy_plan_ids = [ + item.plan_id for item in decisions if item.feasible + ] + checkpoint.pareto_plan_ids = list(tournament.pareto_plan_ids) + checkpoint.selected_strategy_plan_id = tournament.selected_plan_id + checkpoint.strategy_tournament_hash = tournament.content_hash + checkpoint.theorem_card_ids = list(card_ids) + persist_validated_artifact( + checkpoint_path, + checkpoint, + role="strategy_tournament", + payload={ + "schema_version": 1, + "event_id": event_id, + "event_type": event_type.value, + "plan_ids": checkpoint.strategy_plan_ids, + "plan_classes": [plan.plan_class for plan in plans], + "plan_hashes": [plan.content_hash for plan in plans], + "plans": [ + { + "plan_id": plan.plan_id, + "required_definition_ids": list( + plan.required_definition_ids + ), + "unresolved_definition_ids": list( + plan.unresolved_definition_ids + ), + "definition_gap_ids": list(plan.definition_gap_ids), + "definition_auditor_hash": plan.definition_auditor_hash, + "proposition_transformation_ref": ( + plan.proposition_transformation_ref + ), + "case_partition_ids": list(plan.case_partition_ids), + "execution_status": plan.execution_status, + } + for plan in plans + ], + "feasibility": [ + { + "plan_id": item.plan_id, + "feasible": item.feasible, + "reason_codes": list(item.reason_codes), + "score_explanation": dict(item.score_explanation), + } + for item in decisions + ], + "pareto_plan_ids": list(tournament.pareto_plan_ids), + "selected_plan_id": tournament.selected_plan_id, + "content_hash": tournament.content_hash, + }, + dependencies=list(dependencies), + source_run_id=f"host:{event_id}", + ) + precontract_reasons = [] + if unresolved_definitions: + precontract_reasons.append("MISSING_DEFINITION") + if not elaborated_theorem_id or not proposition_hash: + precontract_reasons.append("UNELABORATED_TARGET") + if _target_is_quarantined(checkpoint, target_ref): + precontract_reasons.append("QUARANTINED_PARENT_REQUIRES_TYPED_REFRAME") + if precontract_reasons: + checkpoint.research_contract_id = "" + checkpoint.research_contract_hash = "" + checkpoint.research_contract_rejection_codes = [] + checkpoint.transition( + ProofState.DECOMPOSER, + "precontract-semantic-routing:" + ",".join(precontract_reasons), + strategy_reused=True, + ) + save_checkpoint(checkpoint_path, checkpoint) + return checkpoint + selected = next( + (plan for plan in plans if plan.plan_id == tournament.selected_plan_id), + None, + ) + if selected is None: + checkpoint.research_contract_rejection_codes = [] + checkpoint.transition( + ProofState.DECOMPOSER, + "precontract-semantic-routing:NO_EXECUTABLE_PLAN", + strategy_reused=True, + ) + save_checkpoint(checkpoint_path, checkpoint) + return checkpoint + checkpoint.transition( + ProofState.RESEARCH_CONTRACT_GATE, + "strategy-tournament-complete:elaborated-target", + strategy_reused=False, + ) + contract_decision = gate_research_contract( + selected, + elaborated_theorem_id=elaborated_theorem_id, + elaborated_proposition_hash=proposition_hash, + proof_obligation_id=target_ref, + registered_definition_ids=definitions, + resolved_dependency_ids=dependencies, + verified_theorem_card_ids=card_ids, + allowed_assumption_ids=(), + environment_hash=environment_hash, + expected_plan_hash=selected.content_hash, + ) + checkpoint.research_contract_rejection_codes = list( + contract_decision.reason_codes if not contract_decision.accepted else (), + ) + if contract_decision.contract is not None: + contract = contract_decision.contract + checkpoint.research_contract_id = contract.contract_id + checkpoint.research_contract_hash = contract.content_hash + persist_validated_artifact( + checkpoint_path, + checkpoint, + role="research_contract", + payload={ + **contract.__dict__, + "schema_version": 1, + }, + dependencies=[tournament.content_hash], + source_run_id=f"host:{event_id}:contract", + ) + checkpoint.transition( + ProofState(contract_decision.route_state), + ( + "research-contract-accepted" + if contract_decision.accepted + else "research-contract-rejected:" + + ",".join(contract_decision.reason_codes) + ), + ) + save_checkpoint(checkpoint_path, checkpoint) + return checkpoint diff --git a/autoresearch/prefill/atomic_definition.py b/autoresearch/prefill/atomic_definition.py new file mode 100644 index 0000000..5036ea6 --- /dev/null +++ b/autoresearch/prefill/atomic_definition.py @@ -0,0 +1,554 @@ +"""Host-owned atomic definition transactions and mathematical progress.""" +from __future__ import annotations + +import hashlib +import json +import os +import re +import time +from dataclasses import asdict, dataclass +from pathlib import Path +from typing import Any, Iterable, Mapping + +from autoresearch.prefill.lean_gate import _run_lean + + +CAPABILITY_VERSION = 1 +MIGRATION_EVENT = "atomic_define_one_concept_progress_v1" +PROGRESS_FIELDS = ( + "definitions_added", + "existing_definitions_resolved", + "lemmas_proved", + "accepted_children", + "subgoals_closed", + "verified_counterexamples", +) +_PLACEHOLDER = re.compile(r"\b(?:True|sorry|admit|placeholder|todo)\b|\.\.\.|…") + + +@dataclass(frozen=True) +class ProgressVector: + definitions_added: int = 0 + existing_definitions_resolved: int = 0 + lemmas_proved: int = 0 + accepted_children: int = 0 + subgoals_closed: int = 0 + verified_counterexamples: int = 0 + + @property + def total(self) -> int: + return sum(asdict(self).values()) + + +@dataclass(frozen=True) +class TypedDefinitionCandidate: + short_id: str + gap_id: str + declaration_name: str + lean_source: str + dependency_ids: tuple[str, ...] + semantic_bindings: tuple[str, ...] + + @property + def content_hash(self) -> str: + return _digest(asdict(self)) + + +@dataclass(frozen=True) +class GapDecision: + gap_id: str + classification: str + dependencies: tuple[str, ...] + candidates: tuple[TypedDefinitionCandidate, ...] = () + existing_reference: str = "" + typed_entry: str = "" + reason: str = "" + + +@dataclass(frozen=True) +class DefineOneResult: + status: str + gap_id: str + classification: str + candidate_count: int + candidate_id: str + lean_status: str + lean_source: str + artifact_hash: str + registry_hash_before: str + registry_hash_after: str + environment_hash_before: str + environment_hash_after: str + progress: ProgressVector + reason: str = "" + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + default=lambda item: asdict(item), + ).encode()).hexdigest() + + +def _atomic_json(path: Path, payload: Mapping[str, Any]) -> None: + path.parent.mkdir(parents=True, exist_ok=True, mode=0o700) + temporary = path.with_name(f".{path.name}.{os.getpid()}.tmp") + try: + temporary.write_text( + json.dumps(payload, ensure_ascii=False, sort_keys=True, indent=2), + encoding="utf-8", + ) + os.chmod(temporary, 0o600) + os.replace(temporary, path) + os.chmod(path, 0o600) + finally: + temporary.unlink(missing_ok=True) + + +def empty_definition_registry(environment_hash: str) -> dict[str, Any]: + payload: dict[str, Any] = { + "schema_version": CAPABILITY_VERSION, + "definitions": {}, + "resolved_gaps": {}, + "environment_base_hash": environment_hash, + } + payload["registry_hash"] = registry_hash(payload) + payload["environment_hash"] = environment_registry_hash(payload) + return payload + + +def registry_hash(registry: Mapping[str, Any]) -> str: + return _digest({ + "schema_version": registry.get("schema_version", CAPABILITY_VERSION), + "definitions": registry.get("definitions", {}), + "resolved_gaps": registry.get("resolved_gaps", {}), + }) + + +def environment_registry_hash(registry: Mapping[str, Any]) -> str: + return _digest({ + "base": registry.get("environment_base_hash", ""), + "registry": registry_hash(registry), + }) + + +def load_definition_registry(path: Path, environment_hash: str) -> dict[str, Any]: + path = Path(path).expanduser() + if not path.exists(): + return empty_definition_registry(environment_hash) + raw = json.loads(path.read_text(encoding="utf-8")) + if raw.get("schema_version") != CAPABILITY_VERSION: + raise ValueError("definition registry schema mismatch") + if raw.get("registry_hash") != registry_hash(raw): + raise ValueError("definition registry hash mismatch") + if raw.get("environment_hash") != environment_registry_hash(raw): + raise ValueError("definition environment hash mismatch") + return raw + + +def classify_gap( + gap: Mapping[str, Any], + *, + dependency_graph: Mapping[str, Iterable[str]], + theorem_card_ids: Iterable[str], +) -> GapDecision: + """Classify an audited gap without permitting model-authored definitions.""" + gap_id = str(gap.get("definition_id", "")).strip() + dependencies = tuple(sorted(str(item) for item in dependency_graph.get( + gap_id, (), + ))) + if gap_id == "DEF_EPSILON": + return GapDecision( + gap_id, "TYPED_RESTRICTION", dependencies, + typed_entry="epsilon : ℝ; assumption 0 < epsilon", + reason="positivity is a binder assumption, not a definition", + ) + if gap_id == "DEF_GENUS": + return GapDecision( + gap_id, "TYPED_RESTRICTION", dependencies, + typed_entry="genus : ℕ", + reason="genus is a typed Nat binder, not a standalone definition", + ) + if gap_id == "DEF_SERIES_CONVERGENCE": + return GapDecision( + gap_id, "EXISTING_REFERENCE", dependencies, + existing_reference="Mathlib:LocallyUniformly", + reason="use the imported Mathlib convergence notion", + ) + candidates = _candidates_for_gap(gap_id, dependencies) + if not candidates: + return GapDecision( + gap_id, "NO_TYPED_DEFINITION_CANDIDATE", dependencies, + reason="no registered constructor/operator can inhabit the audited type", + ) + return GapDecision(gap_id, "MISSING_CONCEPT", dependencies, candidates) + + +def _candidate( + short_id: str, + gap_id: str, + name: str, + source: str, + dependencies: tuple[str, ...], + bindings: tuple[str, ...], +) -> TypedDefinitionCandidate: + return TypedDefinitionCandidate( + short_id, gap_id, name, source, dependencies, bindings, + ) + + +def _candidates_for_gap( + gap_id: str, + dependencies: tuple[str, ...], +) -> tuple[TypedDefinitionCandidate, ...]: + specs: dict[str, tuple[tuple[str, str, str, tuple[str, ...]], ...]] = { + "DEF_POLE_NEIGHBORHOOD": ( + ("A", "kakeyaPoleNeighborhood", + "def kakeyaPoleNeighborhood (a : ℂ) (ε : ℝ) : Set ℂ := Metric.ball a ε", + ("Metric.ball", "Set", "Complex")), + ("B", "kakeyaPuncturedPoleNeighborhood", + "def kakeyaPuncturedPoleNeighborhood (a : ℂ) (ε : ℝ) : Set ℂ := Metric.ball a ε \\ {a}", + ("Metric.ball", "Set.diff", "Set.singleton", "Complex")), + ), + "DEF_FUNCTION_BINDING": ( + ("A", "kakeyaPartialSum", + "def kakeyaPartialSum (term : ℕ → ℂ → ℂ) (n : ℕ) (z : ℂ) : ℂ := ∑ k ∈ Finset.range n, term k z", + ("Finset.sum", "Finset.range", "Complex")), + ("B", "kakeyaTermFamily", + "abbrev kakeyaTermFamily := ℕ → ℂ → ℂ", + ("Nat", "Complex", "Function")), + ), + "DEF_GROWTH_ORDER": ( + ("A", "kakeyaHasGrowthOrder", + "def kakeyaHasGrowthOrder (f : ℂ → ℂ) (ρ : ℝ) : Prop := ∃ C : ℝ, 0 < C ∧ ∀ z, ‖f z‖ ≤ Real.exp (C * ‖z‖ ^ ρ)", + ("Exists", "Norm.norm", "Real.exp", "Complex")), + ("B", "kakeyaGrowthBound", + "def kakeyaGrowthBound (f : ℂ → ℂ) (p : ℕ) : Prop := ∃ C : ℝ, 0 < C ∧ ∀ z, ‖f z‖ ≤ Real.exp (C * ‖z‖ ^ p)", + ("Exists", "Norm.norm", "Real.exp", "Complex")), + ), + "DEF_CRITICAL_DENSITY": ( + ("A", "kakeyaCriticalDensity", + "def kakeyaCriticalDensity (p : ℕ) : ℝ := (p + 1 : ℕ)", + ("Nat.cast", "Nat.add")), + ), + } + return tuple( + _candidate(short_id, gap_id, name, source, dependencies, bindings) + for short_id, name, source, bindings in specs.get(gap_id, ()) + ) + + +def dependency_graph_for_audit( + missing: Iterable[Mapping[str, Any]], +) -> dict[str, tuple[str, ...]]: + """Derive typed dependencies from symbol/type evidence in the audit.""" + ids = { + str(item.get("definition_id", "")): item for item in missing + if item.get("definition_id") + } + graph: dict[str, tuple[str, ...]] = {} + symbol_owner: dict[str, str] = {} + for gap_id, item in ids.items(): + for symbol in item.get("symbol_ids", ()): + symbol_owner.setdefault(str(symbol), gap_id) + for gap_id, item in ids.items(): + dependencies: set[str] = set() + for symbol in item.get("symbol_ids", ()): + owner = symbol_owner.get(str(symbol)) + if owner and owner != gap_id: + dependencies.add(owner) + # Typed environment evidence refines ambiguous shared-symbol ownership. + required_type = str(item.get("required_type_id", "")) + if required_type == "TYPE_CANONICAL_PRODUCT_BINDING": + dependencies.discard("DEF_SEQUENCE_DENSITY") + dependencies.add("DEF_POLE_NEIGHBORHOOD") + elif required_type == "TYPE_CONVERGENCE_MODE": + dependencies.add("DEF_FUNCTION_BINDING") + dependencies.discard("DEF_SEQUENCE_DENSITY") + elif required_type == "TYPE_ENTIRE_FUNCTION_ORDER": + dependencies.add("DEF_FUNCTION_BINDING") + dependencies.discard("DEF_GENUS") + elif required_type == "TYPE_SEQUENCE_DENSITY": + dependencies.add("DEF_FUNCTION_BINDING") + elif required_type == "TYPE_DENSITY_THRESHOLD": + dependencies.add("DEF_SEQUENCE_DENSITY") + dependencies.discard("DEF_FUNCTION_BINDING") + graph[gap_id] = tuple(sorted(item for item in dependencies if item in ids)) + return graph + + +def first_dependency_closed_gap( + missing: Iterable[Mapping[str, Any]], + *, + dependency_graph: Mapping[str, Iterable[str]], + resolved_gap_ids: Iterable[str], +) -> Mapping[str, Any] | None: + resolved = set(resolved_gap_ids) + candidates = [ + item for item in missing + if str(item.get("definition_id", "")) not in resolved + and set(dependency_graph.get(str(item.get("definition_id", "")), ())) + <= resolved + ] + if not candidates: + return None + order = { + "DEF_EPSILON": 0, + "DEF_GENUS": 1, + "DEF_POLE_NEIGHBORHOOD": 2, + "DEF_FUNCTION_BINDING": 3, + "DEF_SERIES_CONVERGENCE": 4, + "DEF_GROWTH_ORDER": 5, + "DEF_SEQUENCE_DENSITY": 6, + "DEF_CRITICAL_DENSITY": 7, + } + return min(candidates, key=lambda item: ( + order.get(str(item.get("definition_id", "")), 100), + str(item.get("definition_id", "")), + )) + + +def _validate_candidate( + candidate: TypedDefinitionCandidate, + project_root: Path, +) -> tuple[bool, str]: + if _PLACEHOLDER.search(candidate.lean_source): + return False, "PLACEHOLDER_OR_TRIVIAL_DEFINITION" + if re.search( + r"(^|\n)\s*(?:axiom|variable|opaque|unsafe|noncomputable section)\b", + candidate.lean_source, + ): + return False, "HIDDEN_ASSUMPTION_OR_FORBIDDEN_COMMAND" + if len(re.findall(r"\b(?:def|abbrev)\b", candidate.lean_source)) != 1: + return False, "EXPECTED_EXACTLY_ONE_DEFINITION" + if not candidate.semantic_bindings: + return False, "UNBOUND_SEMANTICS" + content = ( + "import Mathlib\n\n" + "set_option autoImplicit false\n\n" + + candidate.lean_source + + "\n" + ) + run = _run_lean(content, project_root=project_root, timeout_s=120.0) + if run.timed_out: + return False, "LEAN_DEFINITION_TIMEOUT" + if run.returncode != 0: + return False, "LEAN_DEFINITION_INVALID:" + run.output[-1000:] + return True, "ELABORATED" + + +def validate_typed_definition_candidate( + candidate: TypedDefinitionCandidate, + *, + project_root: Path, +) -> tuple[bool, str]: + return _validate_candidate(candidate, project_root) + + +def define_one_concept( + *, + gap: Mapping[str, Any], + definition_auditor_hash: str, + dependency_graph: Mapping[str, Iterable[str]], + registry_path: Path, + project_root: Path, + theorem_card_ids: Iterable[str], + current_environment_hash: str, + selected_candidate_id: str = "", +) -> DefineOneResult: + """Resolve exactly one audited gap in one crash-safe idempotent commit.""" + gap_id = str(gap.get("definition_id", "")) + registry = load_definition_registry(registry_path, current_environment_hash) + before_registry = registry_hash(registry) + before_environment = environment_registry_hash(registry) + previous = registry["resolved_gaps"].get(gap_id) + if previous is not None: + return DefineOneResult( + "IDEMPOTENT_REPLAY", gap_id, previous["classification"], + int(previous.get("candidate_count", 0)), + str(previous.get("candidate_id", "")), + str(previous.get("lean_status", "")), + str(previous.get("lean_source", "")), + str(previous["artifact_hash"]), + before_registry, before_registry, before_environment, + before_environment, ProgressVector(), + "gap already resolved by the same content-addressed transaction", + ) + decision = classify_gap( + gap, + dependency_graph=dependency_graph, + theorem_card_ids=theorem_card_ids, + ) + if any( + dependency not in registry["resolved_gaps"] + for dependency in decision.dependencies + ): + return DefineOneResult( + "DEPENDENCY_OPEN", gap_id, decision.classification, + len(decision.candidates), "", "NOT_RUN", "", "", + before_registry, before_registry, before_environment, + before_environment, ProgressVector(), + "typed dependencies are unresolved", + ) + candidate: TypedDefinitionCandidate | None = None + lean_status = "NOT_REQUIRED" + lean_source = "" + progress = ProgressVector(existing_definitions_resolved=1) + if decision.classification == "NO_TYPED_DEFINITION_CANDIDATE": + return DefineOneResult( + "NO_TYPED_DEFINITION_CANDIDATE", gap_id, decision.classification, + 0, "", "NOT_RUN", "", _digest({ + "gap_id": gap_id, "audit": definition_auditor_hash, + "reason": decision.reason, + }), before_registry, before_registry, before_environment, + before_environment, ProgressVector(), decision.reason, + ) + if decision.classification == "MISSING_CONCEPT": + candidate_map = {item.short_id: item for item in decision.candidates} + candidate = ( + candidate_map.get(selected_candidate_id) + if selected_candidate_id else decision.candidates[0] + ) + if candidate is None: + raise ValueError("candidate selection must be a registered short ID") + valid, lean_status = _validate_candidate(candidate, project_root) + lean_source = candidate.lean_source + if not valid: + return DefineOneResult( + "LEAN_DEFINITION_REJECTED", gap_id, decision.classification, + len(decision.candidates), candidate.short_id, lean_status, + lean_source, candidate.content_hash, before_registry, + before_registry, before_environment, before_environment, + ProgressVector(), lean_status, + ) + progress = ProgressVector(definitions_added=1) + artifact = { + "schema_version": CAPABILITY_VERSION, + "action": "DEFINE_ONE_CONCEPT", + "gap_id": gap_id, + "classification": decision.classification, + "definition_auditor_hash": definition_auditor_hash, + "dependencies": list(decision.dependencies), + "candidate_count": len(decision.candidates), + "candidate_id": candidate.short_id if candidate else "", + "candidate_hashes": [ + item.content_hash for item in decision.candidates + ], + "lean_source": lean_source, + "lean_status": lean_status, + "existing_reference": decision.existing_reference, + "typed_entry": decision.typed_entry, + "semantic_bindings": ( + list(candidate.semantic_bindings) if candidate else [] + ), + "environment_hash_before": before_environment, + "created_at": time.time(), + } + artifact_hash = _digest({ + key: value for key, value in artifact.items() if key != "created_at" + }) + artifact["artifact_hash"] = artifact_hash + registry["resolved_gaps"][gap_id] = artifact + if candidate is not None: + registry["definitions"][candidate.declaration_name] = { + "gap_id": gap_id, + "candidate_hash": candidate.content_hash, + "lean_source": candidate.lean_source, + "artifact_hash": artifact_hash, + } + registry["registry_hash"] = registry_hash(registry) + registry["environment_hash"] = environment_registry_hash(registry) + _atomic_json(registry_path, registry) + after_registry = registry["registry_hash"] + after_environment = registry["environment_hash"] + if before_registry == after_registry or before_environment == after_environment: + raise RuntimeError("atomic definition commit did not change environment") + return DefineOneResult( + "RESOLVED", gap_id, decision.classification, + len(decision.candidates), candidate.short_id if candidate else "", + lean_status, lean_source, artifact_hash, before_registry, + after_registry, before_environment, after_environment, progress, + decision.reason, + ) + + +def update_stagnation( + *, + previous_fingerprint: str, + previous_count: int, + obligation_id: str, + environment_hash: str, + move_class: str, + progress: ProgressVector, + completed_semantic_iteration: bool, + infrastructure_failure: bool = False, +) -> tuple[str, int, bool]: + fingerprint = _digest({ + "obligation_id": obligation_id, + "environment_hash": environment_hash, + "move_class": move_class, + }) + if infrastructure_failure or not completed_semantic_iteration: + return previous_fingerprint, previous_count, False + if progress.total: + return fingerprint, 0, False + count = previous_count + 1 if fingerprint == previous_fingerprint else 1 + return fingerprint, count, count >= 3 + + +def record_semantic_iteration( + checkpoint: Any, + progress: ProgressVector, + *, + move_class: str, + completed: bool = True, + infrastructure_failure: bool = False, +) -> bool: + """Apply the hard zero-delta invariant to one completed semantic iteration.""" + checkpoint.progress_vector = asdict(progress) + fingerprint, count, stagnant = update_stagnation( + previous_fingerprint=checkpoint.progress_fingerprint, + previous_count=checkpoint.semantic_stagnation_count, + obligation_id=checkpoint.target_obligation_id, + environment_hash=checkpoint.definition_environment_hash, + move_class=move_class, + progress=progress, + completed_semantic_iteration=completed, + infrastructure_failure=infrastructure_failure, + ) + checkpoint.progress_fingerprint = fingerprint + checkpoint.semantic_stagnation_count = count + if progress.total: + checkpoint.stagnation_reason = "" + elif stagnant: + checkpoint.stagnation_reason = ( + "three completed zero-delta semantic iterations:" + fingerprint + ) + if fingerprint not in checkpoint.forbidden_semantic_fingerprints: + checkpoint.forbidden_semantic_fingerprints.append(fingerprint) + return stagnant + + +def verified_progress_vector( + *, + definitions_added: int = 0, + existing_definitions_resolved: int = 0, + lemmas_proved: int = 0, + accepted_children: int = 0, + subgoals_closed: int = 0, + verified_counterexamples: int = 0, + lean_source: str = "", +) -> ProgressVector: + """Reject registration notes and proposition ``True`` as progress.""" + source = " ".join(str(lean_source).split()) + if re.search(r"\b(?:theorem|lemma)\b[^:]*:\s*\(?True\)?\s*:=", source): + lemmas_proved = 0 + subgoals_closed = 0 + return ProgressVector( + max(0, definitions_added), + max(0, existing_definitions_resolved), + max(0, lemmas_proved), + max(0, accepted_children), + max(0, subgoals_closed), + max(0, verified_counterexamples), + ) diff --git a/autoresearch/prefill/creative_decomposition.py b/autoresearch/prefill/creative_decomposition.py new file mode 100644 index 0000000..64efcf0 --- /dev/null +++ b/autoresearch/prefill/creative_decomposition.py @@ -0,0 +1,649 @@ +"""Host-owned creative decomposition, private reasoning, and synthesis policy.""" +from __future__ import annotations + +import hashlib +import json +import os +import time +from dataclasses import asdict, dataclass +from pathlib import Path +from typing import Callable, Iterable, Mapping + +from autoresearch.prefill.math_ir import ( + TypedIRCandidate, + TypedIRError, + build_decomposer_candidate_registry, + parse_math_ir, + validate_math_ir, +) +from autoresearch.prefill.theorem_cards import TheoremCard + + +MOVE_REGISTRY_VERSION = 5 +MIN_CANDIDATES = 3 +MIGRATION_EVENT = "creative_decomposition_synthesis_moves_v3" +SHORT_CHOICE_CODES = tuple("ABCDEFGHIJKLMNOPQRSTUVWXYZ") +RANK_REASON_CODES = ( + "DIRECT_LOCAL_CONTRADICTION", + "SUPPORTED_BY_THEOREM_CARDS", + "STRICTEST_REDUCTION", + "NOVEL_VIEWPOINT", + "LOWEST_COMPLEXITY", + "HIGHEST_GAP_COVERAGE", + "SHALLOWEST_DEPENDENCY_DEPTH", +) +PREFILTER_REJECTION_CODES = ( + "ANCESTOR_EQUIVALENT", + "DISCONNECTED_TASK", + "UNSUPPORTED_SYMBOL", + "UNVERIFIED_PREMISE", + "NOT_STRICTLY_SIMPLER", + "DUPLICATE_CANDIDATE", + "UNMET_PRECONDITION", + "UNMET_THEOREM_HYPOTHESIS", + "MISSING_DEPENDENCY_ARTIFACT", +) + + +@dataclass(frozen=True) +class ComplexityMetric: + parent: int + child: int + + @property + def strictly_simpler(self) -> bool: + return self.child < self.parent + + +@dataclass(frozen=True) +class HostMoveSpec: + move_id: str + version: int + operand_kinds: tuple[str, ...] + precondition_ids: tuple[str, ...] + structural_delta: str + assumptions_added: tuple[str, ...] + assumptions_removed: tuple[str, ...] + expected_reduction_path: tuple[str, ...] + theorem_card_tags: tuple[str, ...] + metric: ComplexityMetric + result_status: str + requires_parent_case_split: bool = False + resolves_gap_ids: tuple[str, ...] = () + + @property + def content_hash(self) -> str: + return _digest(asdict(self)) + + +MOVE_REGISTRY: dict[str, HostMoveSpec] = { + spec.move_id: spec for spec in ( + HostMoveSpec( + "CASE_SPLIT", 3, ("parent_claim", "case_predicate"), + ("partition_exhaustive",), "partition parent into exhaustive cases", + (), (), ("prove_each_case", "assemble_parent"), + ("identity_principle",), ComplexityMetric(12, 9), + "PARENT_REDUCTION", + ), + HostMoveSpec( + "RESTRICT_DOMAIN", 3, ("domain", "center", "radius"), + ("positive_radius", "subdomain_of_parent"), + "replace global domain by an open disk", (), (), + ("prove_local_lemma", "transport_to_parent"), + ("locally_uniform_limit",), ComplexityMetric(12, 7), "CHILD_LEMMA", + ), + HostMoveSpec( + "REMOVE_IRRELEVANT_ASSUMPTION", 3, ("parent_claim", "assumption_id"), + ("assumption_not_in_dependency_closure",), + "remove one dependency-irrelevant assumption", (), + ("irrelevant_assumption",), ("prove_reduced_claim", "weaken"), + (), ComplexityMetric(12, 10), "CHILD_LEMMA", + ), + HostMoveSpec( + "HOLOMORPHIC_EXTENSION", 3, + ("term_family", "sum", "disk", "pole_set"), + ("poles_outside_disk", "local_uniform_convergence", "term_holomorphicity"), + "derive holomorphicity of the local sum", (), + ("global_growth_conditions",), + ("apply_locally_uniform_limit_card", "obtain_holomorphic_sum"), + ("locally_uniform_limit", "holomorphic_sum"), + ComplexityMetric(12, 5), "CASE_LEMMA", True, + ), + HostMoveSpec( + "SINGULARITY_CONTRADICTION", 3, + ("term_family", "sum", "pole_set", "center", "radius", "residue"), + ( + "poles_outside_disk", "local_uniform_convergence", + "term_holomorphicity", "sum_equals_residue_over_difference", + "nonzero_residue", "positive_radius", + ), + "contrast holomorphic local sum with a nonzero simple pole", (), + ("global_growth_conditions", "unrelated_poles"), + ( + "derive_holomorphic_sum", "show_simple_pole_nonholomorphic", + "derive_local_contradiction", + ), + ( + "locally_uniform_limit", "holomorphic_sum", + "removable_singularity", "identity_principle", + ), + ComplexityMetric(12, 3), "SPECIAL_CASE_LEMMA", True, + ), + HostMoveSpec( + "DENSITY_LOWER_BOUND", 3, ("sequence", "threshold"), + ("density_defined",), "isolate density threshold", (), (), + ("prove_density_bound",), (), ComplexityMetric(12, 8), "CHILD_LEMMA", + ), + HostMoveSpec( + "LOCAL_CONVERGENCE_OBLIGATION", 3, ("sequence", "center", "radius"), + ("positive_radius",), "isolate local convergence", (), (), + ("prove_local_convergence",), ("locally_uniform_limit",), + ComplexityMetric(12, 7), "CHILD_LEMMA", + ), + HostMoveSpec( + "GROWTH_CONSTRAINT_OBLIGATION", 3, ("function", "degree"), + ("growth_notation_defined",), "isolate growth constraint", (), (), + ("prove_growth_bound",), (), ComplexityMetric(12, 8), "CHILD_LEMMA", + ), + HostMoveSpec( + "LOCAL_TO_GROWTH_BRIDGE", 3, ("local_claim", "growth_claim"), + ("both_claims_scoped",), "bridge local and global viewpoints", (), (), + ("prove_bridge",), (), ComplexityMetric(12, 9), "BRIDGE_LEMMA", + ), + ) +} + + +@dataclass(frozen=True) +class MoveCandidate: + candidate_id: str + choice_id: str + move: HostMoveSpec + typed_payload: tuple[str, ...] + typed_ir_hash: str + novelty_hash: str + theorem_card_ids: tuple[str, ...] + connected: bool = True + uses_verified_premises_only: bool = True + satisfied_precondition_ids: tuple[str, ...] = () + dependency_depth: int = 0 + gap_coverage: int = 0 + + @property + def candidate_hash(self) -> str: + return _digest({ + "candidate_id": self.candidate_id, + "choice_id": self.choice_id, + "move_hash": self.move.content_hash, + "typed_ir_hash": self.typed_ir_hash, + "novelty_hash": self.novelty_hash, + "theorem_card_ids": self.theorem_card_ids, + }) + + +@dataclass(frozen=True) +class CandidateSet: + target_ref: str + viewpoint: str + candidates: tuple[MoveCandidate, ...] + rejected: tuple[tuple[str, str], ...] + content_hash: str + ineligible: tuple[tuple[str, tuple[str, ...]], ...] = () + + @property + def choices(self) -> tuple[str, ...]: + return tuple(item.candidate_id for item in self.candidates) + + def resolve(self, candidate_id: str) -> MoveCandidate: + for candidate in self.candidates: + if candidate.candidate_id == candidate_id: + return candidate + raise TypedIRError( + "INVALID_DECOMPOSITION_CHOICE", + f"candidate {candidate_id!r} is outside set {self.content_hash}", + ) + + @property + def short_choice_map(self) -> Mapping[str, MoveCandidate]: + if len(self.candidates) > len(SHORT_CHOICE_CODES): + raise ValueError("TOO_MANY_SHORT_CHOICE_CANDIDATES") + return { + SHORT_CHOICE_CODES[index]: candidate + for index, candidate in enumerate(self.candidates) + } + + @property + def short_choice_codes(self) -> tuple[str, ...]: + return tuple(self.short_choice_map) + + @property + def short_choice_map_hash(self) -> str: + return _digest({ + "candidate_set_hash": self.content_hash, + "mapping": { + code: { + "candidate_id": candidate.candidate_id, + "candidate_hash": candidate.candidate_hash, + } + for code, candidate in self.short_choice_map.items() + }, + }) + + def resolve_short_code( + self, + code: str, + *, + candidate_set_hash: str, + short_choice_map_hash: str, + ) -> MoveCandidate: + if candidate_set_hash != self.content_hash: + raise TypedIRError( + "STALE_CANDIDATE_SET_HASH", + f"candidate set {candidate_set_hash!r} is not current", + ) + if short_choice_map_hash != self.short_choice_map_hash: + raise TypedIRError( + "STALE_SHORT_CHOICE_MAP_HASH", + f"short map {short_choice_map_hash!r} is not current", + ) + try: + return self.short_choice_map[code] + except KeyError as exc: + raise TypedIRError( + "INVALID_SHORT_CHOICE_CODE", + f"choice code {code!r} is outside set {self.content_hash}", + ) from exc + + +@dataclass(frozen=True) +class CandidateRanking: + ordered_candidate_ids: tuple[str, ...] + reason_codes: tuple[str, ...] + selected_candidate_id: str + ranking_hash: str + + +@dataclass(frozen=True) +class ScratchpadRef: + role: str + sha256: str + path: str + token_count: int + audit_only: bool = True + authoritative: bool = False + parse_contract: str = "NEVER_PARSE" + public: bool = False + + +@dataclass(frozen=True) +class SynthesisTrigger: + invoke: bool + reason: str + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +def _cards_for_move( + move: HostMoveSpec, + cards: Iterable[TheoremCard], +) -> tuple[str, ...]: + wanted = set(move.theorem_card_tags) + return tuple(sorted( + card.card_id for card in cards + if wanted.intersection(card.applicability_tags) + )) + + +def _eligibility_reason_codes( + move: HostMoveSpec, + *, + satisfied_precondition_ids: set[str], + available_dependency_artifact_ids: set[str], + required_dependency_artifact_ids: set[str], + cards: tuple[TheoremCard, ...], + satisfied_theorem_hypothesis_ids: set[str], +) -> tuple[str, ...]: + reasons: list[str] = [] + if set(move.precondition_ids).difference(satisfied_precondition_ids): + reasons.append("UNMET_PRECONDITION") + matching_cards = tuple( + card for card in cards + if set(move.theorem_card_tags).intersection(card.applicability_tags) + ) + if any( + set(card.required_hypotheses).difference( + satisfied_theorem_hypothesis_ids, + ) + for card in matching_cards + ): + reasons.append("UNMET_THEOREM_HYPOTHESIS") + if required_dependency_artifact_ids.difference( + available_dependency_artifact_ids, + ): + reasons.append("MISSING_DEPENDENCY_ARTIFACT") + return tuple(dict.fromkeys(reasons)) + + +def build_candidate_set( + *, + target_ref: str, + viewpoint: str, + dependency_ids: Iterable[str] = (), + theorem_cards: Iterable[TheoremCard] = (), + ancestor_hashes: Iterable[str] = (), + disconnected_move_ids: Iterable[str] = (), + unverified_premise_move_ids: Iterable[str] = (), + satisfied_precondition_ids: Iterable[str] = (), + satisfied_theorem_hypothesis_ids: Iterable[str] = (), + available_dependency_artifact_ids: Iterable[str] = (), + required_dependency_artifact_ids: Iterable[str] = (), + minimum: int = MIN_CANDIDATES, +) -> CandidateSet: + """Generate and prefilter a deterministic finite Host-owned candidate set.""" + dependencies = tuple(dependency_ids) + satisfied = set(satisfied_precondition_ids) + raw = build_decomposer_candidate_registry( + target_ref=target_ref, + viewpoint=viewpoint, + dependency_ids=dependencies, + ) + raw_candidates = list(raw.candidates) + ancestors = set(ancestor_hashes) + disconnected = set(disconnected_move_ids) + unverified = set(unverified_premise_move_ids) + cards = tuple(theorem_cards) + satisfied_hypotheses = set(satisfied_theorem_hypothesis_ids) + available_dependencies = set(available_dependency_artifact_ids) + required_dependencies = set(required_dependency_artifact_ids) + accepted: list[MoveCandidate] = [] + rejected: list[tuple[str, str]] = [] + ineligible: list[tuple[str, tuple[str, ...]]] = [] + seen_novelty: set[str] = set() + for item in raw_candidates: + move = MOVE_REGISTRY.get(item.transformation_id) + if move is None: + rejected.append((item.choice_id, "UNSUPPORTED_SYMBOL")) + continue + eligibility_reasons = _eligibility_reason_codes( + move, + satisfied_precondition_ids=satisfied, + available_dependency_artifact_ids=available_dependencies, + required_dependency_artifact_ids=required_dependencies, + cards=cards, + satisfied_theorem_hypothesis_ids=satisfied_hypotheses, + ) + if eligibility_reasons: + ineligible.append((item.transformation_id, eligibility_reasons)) + continue + novelty_hash = _digest({ + "move": move.content_hash, + "typed_ir": item.typed_ir_hash, + "target": target_ref, + "viewpoint": viewpoint, + }) + if item.typed_ir_hash in ancestors or novelty_hash in ancestors: + rejected.append((item.choice_id, "ANCESTOR_EQUIVALENT")) + elif item.transformation_id in disconnected: + rejected.append((item.choice_id, "DISCONNECTED_TASK")) + elif item.transformation_id in unverified: + rejected.append((item.choice_id, "UNVERIFIED_PREMISE")) + elif not move.metric.strictly_simpler: + rejected.append((item.choice_id, "NOT_STRICTLY_SIMPLER")) + elif novelty_hash in seen_novelty: + rejected.append((item.choice_id, "DUPLICATE_CANDIDATE")) + else: + seen_novelty.add(novelty_hash) + accepted.append(MoveCandidate( + candidate_id=f"C{len(accepted) + 1}_{item.transformation_id}", + choice_id=item.choice_id, + move=move, + typed_payload=item.typed_payload, + typed_ir_hash=item.typed_ir_hash, + novelty_hash=novelty_hash, + theorem_card_ids=_cards_for_move(move, cards), + connected=True, + uses_verified_premises_only=True, + satisfied_precondition_ids=tuple(sorted( + set(move.precondition_ids).intersection(satisfied), + )), + dependency_depth=len(required_dependencies), + gap_coverage=max(1, len(move.resolves_gap_ids)), + )) + precondition_eligible_count = len(accepted) + len(rejected) + if raw.candidates and precondition_eligible_count < minimum and not ineligible: + raise ValueError( + f"INSUFFICIENT_DISTINCT_CANDIDATES:{len(accepted)}<{minimum}" + ) + content_hash = _digest({ + "registry_version": MOVE_REGISTRY_VERSION, + "target_ref": target_ref, + "viewpoint": viewpoint, + "candidates": [item.candidate_hash for item in accepted], + "rejected": rejected, + "ineligible": ineligible, + }) + return CandidateSet( + target_ref, viewpoint, tuple(accepted), tuple(rejected), content_hash, + tuple(ineligible), + ) + + +def rank_candidates( + candidate_set: CandidateSet, + *, + ordered_candidate_ids: Iterable[str] | None = None, + reason_codes: Iterable[str] = (), +) -> CandidateRanking: + """Validate constrained ranking IDs or apply deterministic Host ranking.""" + by_id = {item.candidate_id: item for item in candidate_set.candidates} + if ordered_candidate_ids is None: + ordered = tuple(item.candidate_id for item in sorted( + candidate_set.candidates, + key=lambda item: ( + not item.move.requires_parent_case_split, + item.move.metric.child, + -len(item.theorem_card_ids), + item.candidate_id, + ), + )) + reasons = ( + "LOWEST_COMPLEXITY", + "HIGHEST_GAP_COVERAGE", + "SHALLOWEST_DEPENDENCY_DEPTH", + ) + else: + ordered = tuple(ordered_candidate_ids) + reasons = tuple(reason_codes) + if ( + len(ordered) != len(by_id) + or set(ordered) != set(by_id) + or len(ordered) != len(set(ordered)) + ): + raise ValueError("INVALID_CONSTRAINED_CANDIDATE_RANKING") + if not reasons or any(code not in RANK_REASON_CODES for code in reasons): + raise ValueError("INVALID_CONSTRAINED_RANK_REASON") + if not ordered: + raise ValueError("NO_VALID_CANDIDATE") + selected = ordered[0] + selected_candidate = by_id[selected] + for reason in reasons: + if reason in {"LOWEST_COMPLEXITY", "STRICTEST_REDUCTION"} and ( + selected_candidate.move.metric.child + != min(item.move.metric.child for item in by_id.values()) + ): + raise ValueError(f"INVALID_RANK_REASON_METRIC:{reason}") + if reason == "SUPPORTED_BY_THEOREM_CARDS" and ( + not selected_candidate.theorem_card_ids + or len(selected_candidate.theorem_card_ids) + != max(len(item.theorem_card_ids) for item in by_id.values()) + ): + raise ValueError(f"INVALID_RANK_REASON_METRIC:{reason}") + if reason == "HIGHEST_GAP_COVERAGE" and ( + selected_candidate.gap_coverage + != max(item.gap_coverage for item in by_id.values()) + ): + raise ValueError(f"INVALID_RANK_REASON_METRIC:{reason}") + if reason == "SHALLOWEST_DEPENDENCY_DEPTH" and ( + selected_candidate.dependency_depth + != min(item.dependency_depth for item in by_id.values()) + ): + raise ValueError(f"INVALID_RANK_REASON_METRIC:{reason}") + if reason == "DIRECT_LOCAL_CONTRADICTION" and ( + selected_candidate.move.result_status != "SPECIAL_CASE_LEMMA" + ): + raise ValueError(f"INVALID_RANK_REASON_METRIC:{reason}") + ranking_hash = _digest({ + "candidate_set_hash": candidate_set.content_hash, + "ordered": ordered, + "reason_codes": reasons, + "selected": selected, + }) + return CandidateRanking(ordered, reasons, selected, ranking_hash) + + +def rank_short_choice( + candidate_set: CandidateSet, + *, + choice_code: str, + reason_code: str, + candidate_set_hash: str, + short_choice_map_hash: str, +) -> CandidateRanking: + """Map one scoped short code to an immutable candidate and Host ranking.""" + selected = candidate_set.resolve_short_code( + choice_code, + candidate_set_hash=candidate_set_hash, + short_choice_map_hash=short_choice_map_hash, + ) + deterministic = rank_candidates(candidate_set) + ordered = ( + selected.candidate_id, + *( + candidate_id + for candidate_id in deterministic.ordered_candidate_ids + if candidate_id != selected.candidate_id + ), + ) + return rank_candidates( + candidate_set, + ordered_candidate_ids=ordered, + reason_codes=(reason_code,), + ) + + +def persist_private_scratchpad( + directory: Path, + *, + role: str, + transcript: str, + token_count: int, +) -> ScratchpadRef: + """Persist untrusted prose privately, never as a validated role artifact.""" + encoded = str(transcript).encode() + digest = hashlib.sha256(encoded).hexdigest() + directory = Path(directory).expanduser() + directory.mkdir(parents=True, exist_ok=True, mode=0o700) + path = directory / f"{digest}.txt" + if not path.exists(): + temporary = path.with_name(f".{path.name}.{os.getpid()}.tmp") + try: + temporary.write_bytes(encoded) + os.chmod(temporary, 0o600) + os.replace(temporary, path) + finally: + temporary.unlink(missing_ok=True) + return ScratchpadRef(role, digest, str(path), int(token_count)) + + +def run_private_scratchpad( + inference: Callable[[str], tuple[str, int]], + *, + prompt: str, + directory: Path, + role: str = "decomposer_scratchpad", +) -> ScratchpadRef: + transcript, token_count = inference(prompt) + return persist_private_scratchpad( + directory, role=role, transcript=transcript, token_count=token_count, + ) + + +def assert_no_scratchpad_content( + artifact: Mapping[str, object], + scratchpad: ScratchpadRef, +) -> None: + encoded = json.dumps(artifact, ensure_ascii=False, sort_keys=True) + private_text = Path(scratchpad.path).read_text(encoding="utf-8") + + def strings(value: object): + if isinstance(value, str): + yield value + elif isinstance(value, Mapping): + for key, item in value.items(): + yield str(key) + yield from strings(item) + elif isinstance(value, (list, tuple)): + for item in value: + yield from strings(item) + + if private_text and any(private_text in value for value in strings(artifact)): + raise ValueError("SCRATCHPAD_TEXT_CROSSED_ARTIFACT_GATE") + if scratchpad.path in encoded: + raise ValueError("SCRATCHPAD_PATH_CROSSED_ARTIFACT_GATE") + + +def synthesis_trigger( + *, + novel_rejections: int, + repeated_no_move: int, + evidence_roles: Iterable[str], + stagnation_threshold: int = 3, +) -> SynthesisTrigger: + roles = set(evidence_roles) + if novel_rejections >= stagnation_threshold: + return SynthesisTrigger(True, "NOVEL_SEMANTIC_REJECTIONS") + if repeated_no_move >= 2: + return SynthesisTrigger(True, "REPEATED_NO_MOVE") + if len(roles.intersection({ + "critic", "definition_auditor", "counterexample_worker", "theorem_cards", + })) >= 3: + return SynthesisTrigger(True, "MULTI_ROLE_EVIDENCE") + return SynthesisTrigger(False, "NOT_TRIGGERED") + + +def synthesis_manifest( + *, + evidence_hashes: Mapping[str, str], + rejected_reason_codes: Iterable[str], + theorem_card_ids: Iterable[str], + scratchpad_ref: ScratchpadRef, + ranking: CandidateRanking, + short_choice_map_hash: str, + selected_choice_code: str, + counterexample_verified: bool, +) -> dict[str, object]: + """Build a public-safe synthesis artifact containing IDs and hashes only.""" + if "counterexample_worker" in evidence_hashes and not counterexample_verified: + premise_policy = "ADVISORY_ONLY" + else: + premise_policy = "VERIFIED_ONLY" + return { + "schema_version": 1, + "synthesis_version": 3, + "created_at": time.time(), + "evidence_hashes": dict(sorted(evidence_hashes.items())), + "rejected_reason_codes": tuple(rejected_reason_codes), + "theorem_card_ids": tuple(theorem_card_ids), + "scratchpad_ref": scratchpad_ref.sha256, + "scratchpad_audit_only": True, + "ranking_hash": ranking.ranking_hash, + "short_choice_map_hash": short_choice_map_hash, + "selected_choice_code": selected_choice_code, + "ranked_candidate_ids": ranking.ordered_candidate_ids, + "selected_candidate_id": ranking.selected_candidate_id, + "counterexample_premise_policy": premise_policy, + } diff --git a/autoresearch/prefill/definition_resolution.py b/autoresearch/prefill/definition_resolution.py new file mode 100644 index 0000000..b521056 --- /dev/null +++ b/autoresearch/prefill/definition_resolution.py @@ -0,0 +1,735 @@ +"""Host-owned Autonomous Definition Resolution Protocol. + +The protocol resolves exactly one concept per transaction. Every input, +retrieval result, verification decision, branch, and fallback is +content-addressed; models may supply only search tags and rankings of short +candidate IDs. +""" +from __future__ import annotations + +import hashlib +import json +import os +import re +import time +from dataclasses import asdict, dataclass, field, replace +from enum import Enum +from pathlib import Path +from typing import Any, Callable, Iterable, Mapping + +from autoresearch.prefill.lean_gate import _run_lean + + +PROTOCOL_VERSION = 1 +MIGRATION_EVENT = "autonomous_definition_resolution_v1" +STORE_SCHEMA_VERSION = 1 +_FORBIDDEN = re.compile( + r"\b(?:axiom|opaque|unsafe|sorry|admit|placeholder|todo)\b|\.\.\.|…", + re.IGNORECASE, +) + + +def digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + default=lambda item: asdict(item), + ).encode()).hexdigest() + + +def _stable_tuple(values: Iterable[Any]) -> tuple[str, ...]: + return tuple(sorted({" ".join(str(item).split()) for item in values if str(item).strip()})) + + +class PropertyStatus(str, Enum): + VERIFIED = "VERIFIED" + REFUTED = "REFUTED" + UNKNOWN = "UNKNOWN" + + +@dataclass(frozen=True) +class DefinitionQuery: + concept_id: str + use_sites: tuple[str, ...] + parent_hash: str + typed_ir_hash: str + auditor_hash: str + critic_evidence_hashes: tuple[str, ...] + counterexample_evidence_hashes: tuple[str, ...] + domain: str + codomain: str + required_properties: tuple[str, ...] + hard_properties: tuple[str, ...] + theorem_dependencies: tuple[str, ...] + environment_hash: str + prior_failure_hashes: tuple[str, ...] + + @property + def fingerprint(self) -> str: + return digest(asdict(self)) + + +@dataclass(frozen=True) +class SourceProvenance: + source_id: str + source_kind: str + status: str + locator: str + environment_hash: str + evidence_hash: str + detail: str = "" + + +@dataclass(frozen=True) +class TypedDefinitionCandidate: + short_id: str + concept_id: str + branch_id: str + declaration_name: str + domain: str + codomain: str + binders: tuple[str, ...] + typed_expression: str + dependencies: tuple[str, ...] + provenance: SourceProvenance + required_properties: tuple[str, ...] + claimed_properties: tuple[str, ...] + existing_reference: str = "" + declaration_kind: str = "def" + + @property + def content_hash(self) -> str: + payload = asdict(self) + payload.pop("short_id", None) + return digest(payload) + + +@dataclass(frozen=True) +class PropertyEvidence: + property_id: str + status: str + evidence_kind: str + evidence_ref: str + detail: str = "" + + +@dataclass(frozen=True) +class DefinitionInterpretationBranch: + branch_id: str + query_hash: str + candidate_hash: str + rewritten_parent_hash: str + rewritten_typed_ir_hash: str + assumptions: tuple[str, ...] + theorem_dependencies: tuple[str, ...] + falsification_criteria: tuple[str, ...] + success_criteria: tuple[str, ...] + equivalence_obligation_hash: str + + +@dataclass(frozen=True) +class DefinitionInterface: + interface_id: str + query_hash: str + concept_id: str + operator_type: str + minimum_properties: tuple[str, ...] + conditional_parent_hash: str + missing_axiom_obligations: tuple[str, ...] + viable: bool + + +@dataclass(frozen=True) +class ResolutionResult: + status: str + concept_id: str + query_hash: str + source_statuses: tuple[SourceProvenance, ...] + candidate_hashes: tuple[str, ...] + branch_hashes: tuple[str, ...] + property_statuses: Mapping[str, Mapping[str, str]] + exhaustion_hash: str + interface_hash: str + committed_candidate_hash: str + store_hash_before: str + store_hash_after: str + environment_hash_before: str + environment_hash_after: str + reason: str + + +SourceAdapter = Callable[ + [DefinitionQuery, Path, Mapping[str, Any]], + tuple[list[Mapping[str, Any]], SourceProvenance], +] + + +@dataclass +class DefinitionSourceRegistry: + adapters: dict[str, SourceAdapter] = field(default_factory=dict) + + def register(self, source_id: str, adapter: SourceAdapter) -> None: + if not source_id or source_id in self.adapters: + raise ValueError("definition source IDs must be unique and non-empty") + self.adapters[source_id] = adapter + + def retrieve( + self, + query: DefinitionQuery, + project_root: Path, + context: Mapping[str, Any], + ) -> tuple[list[Mapping[str, Any]], tuple[SourceProvenance, ...]]: + raw: list[Mapping[str, Any]] = [] + statuses = [] + for source_id in sorted(self.adapters): + candidates, status = self.adapters[source_id](query, project_root, context) + if status.source_id != source_id: + raise ValueError("source adapter returned mismatched provenance") + raw.extend(candidates) + statuses.append(status) + return raw, tuple(statuses) + + +def build_definition_query( + gap: Mapping[str, Any], + *, + parent_hash: str, + typed_ir_hash: str, + auditor_hash: str, + critic_evidence_hashes: Iterable[str], + counterexample_evidence_hashes: Iterable[str], + theorem_dependencies: Iterable[str], + environment_hash: str, + prior_failure_hashes: Iterable[str] = (), +) -> DefinitionQuery: + concept = str(gap.get("definition_id") or gap.get("concept_id") or "").strip() + if not concept: + raise ValueError("definition query requires exactly one concept ID") + uses = gap.get("use_sites") or gap.get("usage_sites") or gap.get("symbol_ids") or () + required = gap.get("required_properties") or gap.get("properties") or () + hard = gap.get("hard_properties") or required + domain = str(gap.get("domain") or gap.get("required_domain") or "") + codomain = str( + gap.get("codomain") or gap.get("required_codomain") + or gap.get("required_type_id") or "", + ) + return DefinitionQuery( + concept_id=concept, + use_sites=_stable_tuple(uses), + parent_hash=str(parent_hash), + typed_ir_hash=str(typed_ir_hash), + auditor_hash=str(auditor_hash), + critic_evidence_hashes=_stable_tuple(critic_evidence_hashes), + counterexample_evidence_hashes=_stable_tuple(counterexample_evidence_hashes), + domain=" ".join(domain.split()), + codomain=" ".join(codomain.split()), + required_properties=_stable_tuple(required), + hard_properties=_stable_tuple(hard), + theorem_dependencies=_stable_tuple(theorem_dependencies), + environment_hash=str(environment_hash), + prior_failure_hashes=_stable_tuple(prior_failure_hashes), + ) + + +def empty_store(base_environment_hash: str) -> dict[str, Any]: + store = { + "schema_version": STORE_SCHEMA_VERSION, + "protocol_version": PROTOCOL_VERSION, + "environment_base_hash": base_environment_hash, + "queries": {}, + "sources": {}, + "candidates": {}, + "properties": {}, + "branches": {}, + "exhaustions": {}, + "interfaces": {}, + "commits": {}, + "historical_audit": {}, + } + store["store_hash"] = store_hash(store) + store["environment_hash"] = resolution_environment_hash(store) + return store + + +def store_hash(store: Mapping[str, Any]) -> str: + return digest({ + key: store.get(key, {}) + for key in ( + "schema_version", "protocol_version", "queries", "sources", + "candidates", "properties", "branches", "exhaustions", + "interfaces", "commits", "historical_audit", + ) + }) + + +def resolution_environment_hash(store: Mapping[str, Any]) -> str: + return digest({ + "base": store.get("environment_base_hash", ""), + "commits": store.get("commits", {}), + }) + + +def load_resolution_store(path: Path, base_environment_hash: str) -> dict[str, Any]: + path = Path(path).expanduser() + if not path.exists(): + return empty_store(base_environment_hash) + store = json.loads(path.read_text(encoding="utf-8")) + if store.get("schema_version") != STORE_SCHEMA_VERSION: + raise ValueError("definition resolution store schema mismatch") + if store.get("protocol_version") != PROTOCOL_VERSION: + raise ValueError("definition resolution protocol mismatch") + if store.get("store_hash") != store_hash(store): + raise ValueError("definition resolution store hash mismatch") + if store.get("environment_hash") != resolution_environment_hash(store): + raise ValueError("definition resolution environment hash mismatch") + return store + + +def _atomic_write(path: Path, payload: Mapping[str, Any]) -> None: + path.parent.mkdir(parents=True, exist_ok=True, mode=0o700) + temporary = path.with_name(f".{path.name}.{os.getpid()}.tmp") + try: + temporary.write_text( + json.dumps(payload, ensure_ascii=False, sort_keys=True, indent=2), + encoding="utf-8", + ) + os.chmod(temporary, 0o600) + os.replace(temporary, path) + os.chmod(path, 0o600) + finally: + temporary.unlink(missing_ok=True) + + +def _status( + source_id: str, + kind: str, + status: str, + query: DefinitionQuery, + *, + locator: str = "", + evidence: object = (), + detail: str = "", +) -> SourceProvenance: + return SourceProvenance( + source_id, kind, status, locator, query.environment_hash, + digest(evidence), detail, + ) + + +def _mathlib_source(query, project_root, context): + matches = [] + for item in context.get("mathlib_declarations", ()): + if query.concept_id.lower().replace("def_", "") in str(item.get("tags", "")).lower(): + matches.append(item) + return matches, _status( + "mathlib", "LOCAL_MATHLIB", "QUERIED", query, + locator=str(project_root), evidence=matches, + detail=f"{len(matches)} typed declaration matches", + ) + + +def _theorem_cards_source(query, project_root, context): + matches = [ + item for item in context.get("definition_cards", ()) + if query.concept_id in set(map(str, item.get("concept_ids", ()))) + ] + return matches, _status( + "pinned_cards", "PINNED_CARD", "QUERIED", query, + locator="content-addressed-card-index", evidence=matches, + detail=f"{len(matches)} cards matched", + ) + + +def _local_corpus_source(query, project_root, context): + root = Path(os.environ.get("KAKEYA_OPROOFS_ROOT", "")).expanduser() + if not str(os.environ.get("KAKEYA_OPROOFS_ROOT", "")).strip() or not root.exists(): + return [], _status( + "oproofs", "LOCAL_PROOF_CORPUS", "UNAVAILABLE", query, + detail="KAKEYA_OPROOFS_ROOT is not configured or does not exist", + ) + cards = context.get("oproofs_cards", ()) + matches = [ + item for item in cards + if query.concept_id in set(map(str, item.get("concept_ids", ()))) + ] + return matches, _status( + "oproofs", "LOCAL_PROOF_CORPUS", "QUERIED", query, + locator=str(root), evidence=matches, + ) + + +def _local_publication_source(query, project_root, context): + matches = [ + item for item in context.get("publication_cards", ()) + if query.concept_id in set(map(str, item.get("concept_ids", ()))) + ] + return matches, _status( + "publications", "LOCAL_PUBLICATION_CARD", "QUERIED", query, + locator="local-definition-cards", evidence=matches, + detail=f"{len(matches)} cards matched", + ) + + +def _historical_source(query, project_root, context): + matches = [ + item for item in context.get("validated_history", ()) + if item.get("semantic_validation") == "VERIFIED" + and str(item.get("concept_id")) == query.concept_id + ] + return matches, _status( + "validated_history", "VALIDATED_HISTORICAL", "QUERIED", query, + locator="resolution-store:historical_audit", evidence=matches, + detail=f"{len(matches)} semantically validated definitions", + ) + + +def _typed_synthesis_source(query, project_root, context): + operators = context.get("typed_operator_synthesis", ()) + matches = [ + item for item in operators + if str(item.get("concept_id")) == query.concept_id + and (not query.codomain or str(item.get("codomain")) == query.codomain) + ] + return matches, _status( + "typed_synthesis", "HOST_TYPED_SYNTHESIS", "QUERIED", query, + locator="registered-types-and-operators", evidence=matches, + detail=f"{len(matches)} inhabitants constructed", + ) + + +def default_source_registry() -> DefinitionSourceRegistry: + registry = DefinitionSourceRegistry() + registry.register("mathlib", _mathlib_source) + registry.register("oproofs", _local_corpus_source) + registry.register("pinned_cards", _theorem_cards_source) + registry.register("publications", _local_publication_source) + registry.register("typed_synthesis", _typed_synthesis_source) + registry.register("validated_history", _historical_source) + return registry + + +def normalize_candidates( + query: DefinitionQuery, + raw_candidates: Iterable[Mapping[str, Any]], + source_statuses: Iterable[SourceProvenance], +) -> tuple[TypedDefinitionCandidate, ...]: + provenance = {item.source_id: item for item in source_statuses} + normalized = [] + for raw in raw_candidates: + source_id = str(raw.get("source_id", "")) + if source_id not in provenance: + raise ValueError("candidate has no queried source provenance") + expression = " ".join(str(raw.get("typed_expression", "")).split()) + reference = " ".join(str(raw.get("existing_reference", "")).split()) + if not expression and not reference: + continue + candidate = TypedDefinitionCandidate( + short_id="", + concept_id=query.concept_id, + branch_id=str(raw.get("branch_id", "")), + declaration_name=str(raw.get("declaration_name", "")).strip(), + domain=" ".join(str(raw.get("domain", query.domain)).split()), + codomain=" ".join(str(raw.get("codomain", query.codomain)).split()), + binders=_stable_tuple(raw.get("binders", ())), + typed_expression=expression, + dependencies=_stable_tuple(raw.get("dependencies", ())), + provenance=provenance[source_id], + required_properties=query.required_properties, + claimed_properties=_stable_tuple(raw.get("claimed_properties", ())), + existing_reference=reference, + declaration_kind=str(raw.get("declaration_kind", "def")), + ) + normalized.append(candidate) + dedup = {item.content_hash: item for item in normalized} + ordered = [dedup[key] for key in sorted(dedup)] + return tuple( + replace(item, short_id=f"C{index + 1}") + for index, item in enumerate(ordered) + ) + + +def lean_source(candidate: TypedDefinitionCandidate) -> str: + if candidate.existing_reference: + return f"#check {candidate.existing_reference}" + if candidate.declaration_kind not in {"def", "abbrev"}: + raise ValueError("candidate declaration kind must be def or abbrev") + if not candidate.declaration_name: + raise ValueError("generated declaration requires a name") + binders = " ".join(candidate.binders) + result_type = f" : {candidate.codomain}" if candidate.codomain else "" + return ( + f"{candidate.declaration_kind} {candidate.declaration_name}" + f"{(' ' + binders) if binders else ''}{result_type} := " + f"{candidate.typed_expression}" + ) + + +def compile_candidate( + candidate: TypedDefinitionCandidate, + *, + project_root: Path, + environment_hash: str, +) -> tuple[bool, str, str]: + source = lean_source(candidate) + if _FORBIDDEN.search(source) or re.search(r"(^|\n)\s*(?:variable|noncomputable section)\b", source): + return False, "HIDDEN_ASSUMPTION_OR_PLACEHOLDER", digest(source) + content = ( + "import Mathlib\n\nset_option autoImplicit false\n\n" + f"-- environment:{environment_hash}\n{source}\n" + ) + run = _run_lean(content, project_root=project_root, timeout_s=120.0) + if run.timed_out: + return False, "LEAN_TIMEOUT", digest(content) + if run.returncode: + return False, "LEAN_REJECTED:" + run.output[-800:], digest(content) + return True, "ELABORATED", digest(content) + + +def verify_properties( + query: DefinitionQuery, + candidate: TypedDefinitionCandidate, + *, + evidence: Mapping[str, Mapping[str, Any]], +) -> tuple[PropertyEvidence, ...]: + results = [] + for property_id in query.required_properties: + record = evidence.get(property_id, {}) + candidate_hashes = set(map(str, record.get("candidate_hashes", ()))) + applies = not candidate_hashes or candidate.content_hash in candidate_hashes + status = str(record.get("status", "UNKNOWN")).upper() if applies else "UNKNOWN" + if status not in {item.value for item in PropertyStatus}: + status = PropertyStatus.UNKNOWN.value + evidence_ref = str(record.get("evidence_ref", "")) + evidence_kind = str(record.get("evidence_kind", "NONE")) + if status == PropertyStatus.VERIFIED.value and not evidence_ref: + status = PropertyStatus.UNKNOWN.value + results.append(PropertyEvidence( + property_id, status, evidence_kind, evidence_ref, + str(record.get("detail", "")), + )) + return tuple(results) + + +def _branch(query: DefinitionQuery, candidate: TypedDefinitionCandidate) -> DefinitionInterpretationBranch: + candidate_hash = candidate.content_hash + branch_id = "B-" + candidate_hash[:16] + rewritten_parent = digest({ + "parent": query.parent_hash, "concept": query.concept_id, + "candidate": candidate_hash, + }) + rewritten_ir = digest({ + "typed_ir": query.typed_ir_hash, "candidate": candidate_hash, + }) + equivalence = digest({ + "original_parent": query.parent_hash, + "rewritten_parent": rewritten_parent, + "obligation": "semantic_equivalence_or_explicit_reduction", + }) + return DefinitionInterpretationBranch( + branch_id, query.fingerprint, candidate_hash, rewritten_parent, + rewritten_ir, (), query.theorem_dependencies, + tuple(f"refute:{item}" for item in query.hard_properties), + tuple(f"verify:{item}" for item in query.hard_properties), + equivalence, + ) + + +def synthesize_interface(query: DefinitionQuery) -> DefinitionInterface: + operator_type = ( + f"{query.domain} → {query.codomain}" + if query.domain and query.codomain else query.codomain or query.domain + ) + # Auditor ontology IDs constrain search but are not executable Lean types. + # A list of use-site symbols alone cannot justify inventing a signature. + viable = bool( + operator_type + and not re.search(r"(^|[ →])(TYPE|DOM)_[A-Z0-9_]+", operator_type) + ) + obligations = tuple(f"AXIOM_OBLIGATION:{item}" for item in query.hard_properties) + interface_id = digest({ + "query": query.fingerprint, + "operator_type": operator_type, + "minimum_properties": query.hard_properties, + "uses": query.use_sites, + }) + return DefinitionInterface( + interface_id, query.fingerprint, query.concept_id, + operator_type or "USAGE_DERIVED_UNKNOWN_TYPE", + query.hard_properties, + digest({"parent": query.parent_hash, "interface": interface_id}), + obligations, viable, + ) + + +def resolve_one_concept( + *, + query: DefinitionQuery, + store_path: Path, + project_root: Path, + source_registry: DefinitionSourceRegistry | None = None, + source_context: Mapping[str, Any] | None = None, + property_evidence: Mapping[str, Mapping[str, Any]] | None = None, + ranked_short_ids: Iterable[str] = (), +) -> ResolutionResult: + """Run one crash-safe, idempotent definition-resolution transaction.""" + store = load_resolution_store(store_path, query.environment_hash) + before = store_hash(store) + before_environment = resolution_environment_hash(store) + query_hash = query.fingerprint + previous = store["queries"].get(query_hash) + if previous and previous.get("terminal"): + return ResolutionResult( + "IDENTICAL_QUERY_EXHAUSTED" if previous["status"] == "EXHAUSTED" else "IDEMPOTENT_REPLAY", + query.concept_id, query_hash, (), tuple(previous.get("candidate_hashes", ())), + tuple(previous.get("branch_hashes", ())), + previous.get("property_statuses", {}), + str(previous.get("exhaustion_hash", "")), + str(previous.get("interface_hash", "")), + str(previous.get("committed_candidate_hash", "")), + before, before, before_environment, before_environment, + "identical terminal query cannot rerun without semantic input change", + ) + registry = source_registry or default_source_registry() + context = dict(source_context or {}) + raw, statuses = registry.retrieve(query, project_root, context) + candidates = normalize_candidates(query, raw, statuses) + rankings = tuple(ranked_short_ids) + if rankings and ( + len(set(rankings)) != len(rankings) + or not set(rankings) <= {item.short_id for item in candidates} + ): + raise ValueError("model ranking may contain scoped short candidate IDs only") + candidate_order = {item: index for index, item in enumerate(rankings)} + candidates = tuple(sorted( + candidates, key=lambda item: (candidate_order.get(item.short_id, len(rankings)), item.content_hash), + )) + property_map: dict[str, dict[str, str]] = {} + survivors = [] + rejections = {} + for candidate in candidates: + compiled, compile_status, compilation_hash = compile_candidate( + candidate, project_root=project_root, + environment_hash=query.environment_hash, + ) + evidence = verify_properties( + query, candidate, evidence=property_evidence or {}, + ) + statuses_for_candidate = {item.property_id: item.status for item in evidence} + property_map[candidate.content_hash] = statuses_for_candidate + hard_ok = all( + statuses_for_candidate.get(item) == PropertyStatus.VERIFIED.value + for item in query.hard_properties + ) + if compiled and hard_ok: + survivors.append(candidate) + else: + rejections[candidate.content_hash] = { + "compile_status": compile_status, + "compilation_hash": compilation_hash, + "unmet_hard_properties": [ + item for item in query.hard_properties + if statuses_for_candidate.get(item) != PropertyStatus.VERIFIED.value + ], + } + store["candidates"][candidate.content_hash] = asdict(candidate) + store["properties"][candidate.content_hash] = [asdict(item) for item in evidence] + branches = tuple(_branch(query, item) for item in survivors) + branch_hashes = tuple(digest(asdict(item)) for item in branches) + for branch_hash, branch in zip(branch_hashes, branches): + store["branches"][branch_hash] = asdict(branch) + exhaustion_hash = "" + interface_hash = "" + committed_hash = "" + reason = "" + if len(survivors) > 1: + status = "PARENT_STATEMENT_UNDERSPECIFIED" + reason = "multiple hard-feasible interpretations require branch tournament" + elif len(survivors) == 1: + candidate = survivors[0] + committed_hash = candidate.content_hash + store["commits"][query.concept_id] = { + "query_hash": query_hash, + "candidate_hash": committed_hash, + "provenance": asdict(candidate.provenance), + "properties": property_map[committed_hash], + "lean_source_hash": digest(lean_source(candidate)), + "committed_at": time.time(), + } + status = "COMMITTED" + reason = "Lean elaborated, hard properties verified, provenance complete" + else: + interface = synthesize_interface(query) + interface_hash = digest(asdict(interface)) + store["interfaces"][interface_hash] = asdict(interface) + exhaustion = { + "schema_version": 1, + "query_hash": query_hash, + "concept_id": query.concept_id, + "parent_hash": query.parent_hash, + "environment_hash": query.environment_hash, + "sources": [asdict(item) for item in statuses], + "candidate_hashes": [item.content_hash for item in candidates], + "rejections": rejections, + "unmet_properties": list(query.hard_properties), + "interface_hash": interface_hash, + } + exhaustion_hash = digest(exhaustion) + store["exhaustions"][exhaustion_hash] = exhaustion + status = "INTERFACE_REQUIRED" if interface.viable else "PARENT_STATEMENT_UNDERSPECIFIED" + reason = ( + "concrete retrieval exhausted; conditional theorem requires explicit interface axioms" + if interface.viable + else "no concrete definition, viable typed interface, or equivalent rewrite" + ) + store["sources"][query_hash] = [asdict(item) for item in statuses] + query_record = { + **asdict(query), + "query_hash": query_hash, + "status": "EXHAUSTED" if not survivors else status, + "terminal": True, + "candidate_hashes": [item.content_hash for item in candidates], + "branch_hashes": list(branch_hashes), + "property_statuses": property_map, + "exhaustion_hash": exhaustion_hash, + "interface_hash": interface_hash, + "committed_candidate_hash": committed_hash, + "completed_at": time.time(), + } + store["queries"][query_hash] = query_record + store["store_hash"] = store_hash(store) + store["environment_hash"] = resolution_environment_hash(store) + _atomic_write(store_path, store) + return ResolutionResult( + status, query.concept_id, query_hash, statuses, + tuple(item.content_hash for item in candidates), branch_hashes, + property_map, exhaustion_hash, interface_hash, committed_hash, + before, store["store_hash"], before_environment, + store["environment_hash"], reason, + ) + + +def migrate_legacy_registry( + legacy: Mapping[str, Any], + *, + base_environment_hash: str, +) -> dict[str, Any]: + """Import legacy definitions as audit-only pending semantic validation.""" + store = empty_store(base_environment_hash) + for name, record in sorted(legacy.get("definitions", {}).items()): + concept = str(record.get("gap_id", "")) + obligations = { + "DEF_POLE_NEIGHBORHOOD": ("full_vs_punctured_neighborhood",), + "DEF_FUNCTION_BINDING": ("partial_sum_index_binding",), + "DEF_GROWTH_ORDER": ("growth_order_semantics",), + }.get(concept, ("semantic_equivalence_to_actual_use",)) + key = digest({"name": name, "record": record}) + store["historical_audit"][key] = { + "concept_id": concept, + "declaration_name": str(name), + "legacy_record": dict(record), + "semantic_validation": "PENDING", + "property_obligations": list(obligations), + "audit_only": True, + } + store["store_hash"] = store_hash(store) + store["environment_hash"] = resolution_environment_hash(store) + return store diff --git a/autoresearch/prefill/evidence_planner.py b/autoresearch/prefill/evidence_planner.py new file mode 100644 index 0000000..c1a5f45 --- /dev/null +++ b/autoresearch/prefill/evidence_planner.py @@ -0,0 +1,470 @@ +"""Host-owned evidence graph and bounded, non-omniscient proof planning.""" +from __future__ import annotations + +import hashlib +import json +from dataclasses import asdict, dataclass, field, replace +from enum import Enum +from typing import Iterable, Mapping + +from autoresearch.prefill.creative_decomposition import CandidateSet, MoveCandidate +from autoresearch.prefill.theorem_cards import TheoremCard + + +PLANNER_VERSION = 1 +OPERATOR_EVENT = "host_feasibility_evidence_planner_v1" + + +class NodeKind(str, Enum): + GAP = "GAP" + EVIDENCE = "EVIDENCE" + THEOREM_CARD = "THEOREM_CARD" + MOVE = "MOVE" + + +class EdgeKind(str, Enum): + RESOLVES_GAP = "resolves_gap" + REQUIRES = "requires" + SUPPORTS = "supports" + CONTRADICTS = "contradicts" + CASE_OF = "case_of" + REDUCES_TO = "reduces_to" + + +class VerificationStatus(str, Enum): + VERIFIED = "VERIFIED" + ADVISORY = "ADVISORY" + UNRESOLVED = "UNRESOLVED" + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +@dataclass(frozen=True) +class GraphNode: + node_id: str + kind: str + verification_status: str + provenance_refs: tuple[str, ...] + attributes: Mapping[str, object] = field(default_factory=dict) + + +@dataclass(frozen=True) +class GraphEdge: + edge_id: str + kind: str + source_id: str + target_id: str + provenance_refs: tuple[str, ...] + + +@dataclass(frozen=True) +class EvidenceGapGraph: + nodes: tuple[GraphNode, ...] + edges: tuple[GraphEdge, ...] + content_hash: str + + @property + def by_id(self) -> dict[str, GraphNode]: + return {node.node_id: node for node in self.nodes} + + +@dataclass(frozen=True) +class ProofPlanNode: + plan_node_id: str + graph_node_id: str + dependency_node_ids: tuple[str, ...] = () + + +@dataclass(frozen=True) +class PlanScore: + unresolved_gap_coverage: int + verified_theorem_support: int + dependency_depth: int + strict_complexity_reduction: int + novelty_information_gain: int + risk: int + + @property + def ordering_key(self) -> tuple[int, ...]: + return ( + -self.unresolved_gap_coverage, + -self.verified_theorem_support, + self.dependency_depth, + -self.strict_complexity_reduction, + -self.novelty_information_gain, + self.risk, + ) + + +@dataclass(frozen=True) +class ProofPlan: + plan_id: str + nodes: tuple[ProofPlanNode, ...] + resolved_gap_ids: tuple[str, ...] + theorem_card_ids: tuple[str, ...] + case_exhaustiveness_claims: tuple[str, ...] + score: PlanScore + score_explanation: Mapping[str, int] + graph_hash: str + content_hash: str + + +@dataclass(frozen=True) +class HostEvidenceContext: + satisfied_precondition_ids: tuple[str, ...] + satisfied_theorem_hypothesis_ids: tuple[str, ...] + available_dependency_artifact_ids: tuple[str, ...] + unresolved_gap_ids: tuple[str, ...] + + +_DEFINITION_PRECONDITIONS: Mapping[str, tuple[str, ...]] = { + "density_defined": ("DEF_SEQUENCE_DENSITY", "DEF_CRITICAL_DENSITY"), + "growth_notation_defined": ("DEF_GROWTH_ORDER",), + "positive_radius": ("DEF_POLE_NEIGHBORHOOD",), + "registered_definition_gap": (), +} + + +def host_evidence_context( + artifacts: Mapping[str, object], + *, + artifact_hashes: Mapping[str, str], +) -> HostEvidenceContext: + """Derive executable facts only from persisted, verified artifacts.""" + definitions: set[str] = set() + missing: set[str] = set() + hypotheses: set[str] = set() + for artifact in artifacts.values(): + payload = asdict(artifact) if hasattr(artifact, "__dataclass_fields__") else artifact + if not isinstance(payload, Mapping): + continue + for item in payload.get("definitions", ()): + if isinstance(item, Mapping): + definitions.add(str(item.get("definition_id", ""))) + for item in payload.get("missing_definitions", ()): + if isinstance(item, Mapping): + missing.add(str(item.get("definition_id", ""))) + hypotheses.update(str(item) for item in payload.get( + "verified_hypothesis_ids", (), + )) + satisfied = { + precondition + for precondition, requirements in _DEFINITION_PRECONDITIONS.items() + if requirements and set(requirements) <= definitions + } + if missing: + satisfied.add("registered_definition_gap") + return HostEvidenceContext( + tuple(sorted(satisfied)), + tuple(sorted(hypotheses)), + tuple(sorted(artifact_hashes.values())), + tuple(sorted(f"gap:definition:{item}" for item in missing if item)), + ) + + +def _edge( + kind: EdgeKind, + source_id: str, + target_id: str, + provenance_refs: Iterable[str], +) -> GraphEdge: + provenance = tuple(sorted(set(provenance_refs))) + edge_id = "edge:" + _digest((kind.value, source_id, target_id, provenance)) + return GraphEdge(edge_id, kind.value, source_id, target_id, provenance) + + +def build_evidence_gap_graph( + *, + artifacts: Mapping[str, object], + artifact_hashes: Mapping[str, str], + advisory_artifacts: Mapping[str, Mapping[str, object]], + theorem_cards: Iterable[TheoremCard], + candidate_set: CandidateSet, + failure_reason_codes: Iterable[str] = (), +) -> EvidenceGapGraph: + nodes: dict[str, GraphNode] = {} + edges: dict[str, GraphEdge] = {} + missing_ids: list[str] = [] + for role, artifact in sorted(artifacts.items()): + payload = asdict(artifact) if hasattr(artifact, "__dataclass_fields__") else artifact + if not isinstance(payload, Mapping): + continue + provenance = artifact_hashes.get(role, "") + for item in payload.get("missing_definitions", ()): + if not isinstance(item, Mapping): + continue + definition_id = str(item.get("definition_id", "")) + if not definition_id: + continue + gap_id = f"gap:definition:{definition_id}" + missing_ids.append(gap_id) + nodes[gap_id] = GraphNode( + gap_id, NodeKind.GAP.value, VerificationStatus.UNRESOLVED.value, + (provenance,), {"definition_id": definition_id, "source_role": role}, + ) + for item in payload.get("definitions", ()): + if not isinstance(item, Mapping): + continue + definition_id = str(item.get("definition_id", "")) + evidence_id = f"evidence:{provenance}:definition:{definition_id}" + nodes[evidence_id] = GraphNode( + evidence_id, NodeKind.EVIDENCE.value, + VerificationStatus.VERIFIED.value, (provenance,), + {"definition_id": definition_id, "source_role": role}, + ) + gap_id = f"gap:definition:{definition_id}" + nodes.setdefault(gap_id, GraphNode( + gap_id, NodeKind.GAP.value, VerificationStatus.UNRESOLVED.value, + (provenance,), {"definition_id": definition_id}, + )) + support = _edge(EdgeKind.SUPPORTS, evidence_id, gap_id, (provenance,)) + edges[support.edge_id] = support + for digest, payload in sorted(advisory_artifacts.items()): + evidence_id = f"evidence:{digest}:advisory" + nodes[evidence_id] = GraphNode( + evidence_id, NodeKind.EVIDENCE.value, + VerificationStatus.ADVISORY.value, (digest,), + {"premise": False, "source_role": payload.get("role", "")}, + ) + for code in sorted(set(failure_reason_codes)): + gap_id = f"gap:failure:{code}" + nodes[gap_id] = GraphNode( + gap_id, NodeKind.GAP.value, VerificationStatus.UNRESOLVED.value, + (code,), {"reason_code": code}, + ) + for card in sorted(theorem_cards, key=lambda item: item.card_id): + node_id = f"theorem:{card.card_id}" + nodes[node_id] = GraphNode( + node_id, NodeKind.THEOREM_CARD.value, + VerificationStatus.VERIFIED.value, (card.content_hash,), + {"required_hypotheses": card.required_hypotheses}, + ) + for candidate in candidate_set.candidates: + base_id = f"move:{candidate.candidate_id}" + nodes[base_id] = _move_node(base_id, candidate, ()) + for precondition in candidate.move.precondition_ids: + gap_id = f"gap:precondition:{precondition}" + nodes.setdefault(gap_id, GraphNode( + gap_id, NodeKind.GAP.value, VerificationStatus.UNRESOLVED.value, + (), {"precondition_id": precondition}, + )) + required = _edge(EdgeKind.REQUIRES, base_id, gap_id, ()) + edges[required.edge_id] = required + if candidate.move.resolves_gap_ids: + targets = tuple( + f"gap:precondition:{item}" + for item in candidate.move.resolves_gap_ids + ) + for target in targets: + case_id = f"{base_id}:case:{target}" + nodes[case_id] = _move_node(case_id, candidate, (target,)) + case_edge = _edge(EdgeKind.CASE_OF, case_id, base_id, ()) + resolve_edge = _edge( + EdgeKind.RESOLVES_GAP, case_id, target, + nodes[target].provenance_refs if target in nodes else (), + ) + edges[case_edge.edge_id] = case_edge + edges[resolve_edge.edge_id] = resolve_edge + canonical = { + "planner_version": PLANNER_VERSION, + "nodes": [asdict(nodes[key]) for key in sorted(nodes)], + "edges": [asdict(edges[key]) for key in sorted(edges)], + } + return EvidenceGapGraph( + tuple(nodes[key] for key in sorted(nodes)), + tuple(edges[key] for key in sorted(edges)), + _digest(canonical), + ) + + +def _move_node( + node_id: str, + candidate: MoveCandidate, + target_gap_ids: tuple[str, ...], +) -> GraphNode: + return GraphNode( + node_id, NodeKind.MOVE.value, VerificationStatus.VERIFIED.value, + (candidate.candidate_hash,), + { + "candidate_id": candidate.candidate_id, + "candidate_hash": candidate.candidate_hash, + "target_gap_ids": target_gap_ids, + "metric_parent": candidate.move.metric.parent, + "metric_child": candidate.move.metric.child, + "theorem_card_ids": candidate.theorem_card_ids, + "dependency_depth": candidate.dependency_depth, + "requires_parent_case_split": candidate.move.requires_parent_case_split, + }, + ) + + +def generate_proof_plans( + graph: EvidenceGapGraph, + *, + unresolved_gap_ids: Iterable[str], + beam_width: int = 16, +) -> tuple[ProofPlan, ...]: + """Deterministic bounded backward chaining over registered graph edges.""" + unresolved = set(unresolved_gap_ids) + by_id = graph.by_id + resolves: dict[str, set[str]] = {} + for edge in graph.edges: + if edge.kind == EdgeKind.RESOLVES_GAP.value: + resolves.setdefault(edge.source_id, set()).add(edge.target_id) + plans: list[ProofPlan] = [] + for move_id, covered in sorted(resolves.items()): + if move_id not in by_id: + continue + node = by_id[move_id] + actual_coverage = tuple(sorted(covered.intersection(unresolved))) + if not actual_coverage: + continue + attrs = node.attributes + reduction = int(attrs.get("metric_parent", 0)) - int( + attrs.get("metric_child", 0), + ) + theorem_ids = tuple(str(item) for item in attrs.get("theorem_card_ids", ())) + score = PlanScore( + len(actual_coverage), + len(theorem_ids), + int(attrs.get("dependency_depth", 0)), + reduction, + 1, + int(bool(attrs.get("requires_parent_case_split", False))), + ) + plan_node = ProofPlanNode("step:1", move_id, ()) + explanation = { + "unresolved_gap_coverage": score.unresolved_gap_coverage, + "verified_theorem_support": score.verified_theorem_support, + "dependency_depth": score.dependency_depth, + "strict_complexity_reduction": score.strict_complexity_reduction, + "novelty_information_gain": score.novelty_information_gain, + "risk": score.risk, + } + canonical = { + "graph_hash": graph.content_hash, + "nodes": [asdict(plan_node)], + "resolved_gap_ids": actual_coverage, + "theorem_card_ids": theorem_ids, + "case_exhaustiveness_claims": (), + "score": asdict(score), + } + content_hash = _digest(canonical) + plans.append(ProofPlan( + "plan:" + content_hash[:16], (plan_node,), actual_coverage, + theorem_ids, (), score, explanation, graph.content_hash, content_hash, + )) + plans.sort(key=lambda item: (*item.score.ordering_key, item.plan_id)) + return tuple(plans[:beam_width]) + + +def validate_proof_plan(graph: EvidenceGapGraph, plan: ProofPlan) -> None: + if plan.graph_hash != graph.content_hash: + raise ValueError("STALE_PROOF_PLAN_GRAPH_HASH") + graph_nodes = graph.by_id + plan_nodes = {node.plan_node_id: node for node in plan.nodes} + if len(plan_nodes) != len(plan.nodes): + raise ValueError("DUPLICATE_PROOF_PLAN_NODE") + for node in plan.nodes: + if node.graph_node_id not in graph_nodes: + raise ValueError("UNREGISTERED_PROOF_PLAN_GRAPH_NODE") + if any(item not in plan_nodes for item in node.dependency_node_ids): + raise ValueError("PROOF_PLAN_DEPENDENCY_CLOSURE") + visiting: set[str] = set() + visited: set[str] = set() + + def visit(node_id: str) -> None: + if node_id in visiting: + raise ValueError("CYCLIC_PROOF_PLAN") + if node_id in visited: + return + visiting.add(node_id) + for dependency in plan_nodes[node_id].dependency_node_ids: + visit(dependency) + visiting.remove(node_id) + visited.add(node_id) + + for node_id in plan_nodes: + visit(node_id) + if any( + graph_nodes[node.graph_node_id].kind != NodeKind.MOVE.value + for node in plan.nodes + ): + raise ValueError("PROOF_PLAN_NODE_NOT_EXECUTABLE_MOVE") + if any( + graph_nodes[node.graph_node_id].verification_status + != VerificationStatus.VERIFIED.value + for node in plan.nodes + ): + raise ValueError("UNVERIFIED_PROOF_PLAN_NODE") + for claim in plan.case_exhaustiveness_claims: + case_node = graph_nodes.get(claim) + if case_node is None or not bool(case_node.attributes.get("exhaustive", False)): + raise ValueError("CASE_EXHAUSTIVENESS_NOT_VERIFIED") + for node in plan.nodes: + attrs = graph_nodes[node.graph_node_id].attributes + if int(attrs.get("metric_child", 0)) >= int(attrs.get("metric_parent", 0)): + raise ValueError("PROOF_PLAN_NOT_STRICTLY_SIMPLER") + for card_id in attrs.get("theorem_card_ids", ()): + card = graph_nodes.get(f"theorem:{card_id}") + if card is None or card.verification_status != VerificationStatus.VERIFIED.value: + raise ValueError("THEOREM_CARD_NOT_VERIFIED") + + +def first_executable_node(plan: ProofPlan) -> ProofPlanNode: + completed: set[str] = set() + for node in plan.nodes: + if set(node.dependency_node_ids) <= completed: + return node + completed.add(node.plan_node_id) + raise ValueError("NO_EXECUTABLE_PROOF_PLAN_NODE") + + +def replan_after_failure( + graph: EvidenceGapGraph, + *, + failed_plan_node_id: str, + reason_code: str, + unresolved_gap_ids: Iterable[str], +) -> tuple[EvidenceGapGraph, tuple[ProofPlan, ...]]: + evidence_id = f"evidence:failure:{_digest((failed_plan_node_id, reason_code))}" + gap_id = f"gap:failure:{reason_code}" + nodes = (*graph.nodes, GraphNode( + evidence_id, NodeKind.EVIDENCE.value, VerificationStatus.VERIFIED.value, + (failed_plan_node_id,), {"reason_code": reason_code}, + ), GraphNode( + gap_id, NodeKind.GAP.value, VerificationStatus.UNRESOLVED.value, + (evidence_id,), {"reason_code": reason_code}, + )) + contradiction = _edge( + EdgeKind.CONTRADICTS, evidence_id, failed_plan_node_id, + (failed_plan_node_id,), + ) + canonical = { + "planner_version": PLANNER_VERSION, + "nodes": [asdict(item) for item in sorted(nodes, key=lambda item: item.node_id)], + "edges": [asdict(item) for item in sorted( + (*graph.edges, contradiction), key=lambda item: item.edge_id, + )], + } + updated = EvidenceGapGraph( + tuple(sorted(nodes, key=lambda item: item.node_id)), + tuple(sorted((*graph.edges, contradiction), key=lambda item: item.edge_id)), + _digest(canonical), + ) + blocked = { + edge.target_id for edge in updated.edges + if edge.kind == EdgeKind.CONTRADICTS.value + } + filtered = replace( + updated, + nodes=tuple(node for node in updated.nodes if node.node_id not in blocked), + ) + plans = generate_proof_plans( + filtered, unresolved_gap_ids=(*unresolved_gap_ids, gap_id), + ) + return updated, plans diff --git a/autoresearch/prefill/research_contract.py b/autoresearch/prefill/research_contract.py new file mode 100644 index 0000000..c418867 --- /dev/null +++ b/autoresearch/prefill/research_contract.py @@ -0,0 +1,190 @@ +"""Host-owned gate between a strategy tournament and proof search.""" +from __future__ import annotations + +import hashlib +import json +from dataclasses import asdict, dataclass +from enum import Enum +from typing import Iterable, Mapping + +from autoresearch.prefill.strategy_tournament import ( + PlanExecutionStatus, + StrategyPlan, +) + + +CONTRACT_VERSION = 2 + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +class ContractRejection(str, Enum): + MISSING_DEFINITION = "MISSING_DEFINITION" + UNELABORATED_TARGET = "UNELABORATED_TARGET" + PROPOSITION_HASH_MISMATCH = "PROPOSITION_HASH_MISMATCH" + UNRESOLVED_DEPENDENCY = "UNRESOLVED_DEPENDENCY" + UNRESOLVED_THEOREM_CARD = "UNRESOLVED_THEOREM_CARD" + MISSING_SUCCESS_CRITERION = "MISSING_SUCCESS_CRITERION" + MISSING_FAILURE_CRITERION = "MISSING_FAILURE_CRITERION" + MISSING_PROOF_OBLIGATION = "MISSING_PROOF_OBLIGATION" + HIDDEN_ASSUMPTION = "HIDDEN_ASSUMPTION" + NON_REDUCING_TARGET = "NON_REDUCING_TARGET" + ENVIRONMENT_HASH_MISMATCH = "ENVIRONMENT_HASH_MISMATCH" + PLAN_HASH_MISMATCH = "PLAN_HASH_MISMATCH" + PLANNING_ONLY = "PLANNING_ONLY" + + +@dataclass(frozen=True) +class ResearchContract: + contract_version: int + contract_id: str + plan_id: str + plan_hash: str + target_ref: str + theorem_id: str + proposition_hash: str + proof_obligation_id: str + definition_ids: tuple[str, ...] + definition_gap_ids: tuple[str, ...] + definition_auditor_hash: str + dependency_ids: tuple[str, ...] + theorem_card_ids: tuple[str, ...] + assumption_ids: tuple[str, ...] + success_criterion_id: str + failure_criterion_id: str + parent_obligation_ref: str + parent_complexity: int + target_complexity: int + environment_hash: str + content_hash: str + + +@dataclass(frozen=True) +class ContractDecision: + accepted: bool + reason_codes: tuple[str, ...] + route_state: str + contract: ResearchContract | None + + +def gate_research_contract( + plan: StrategyPlan, + *, + elaborated_theorem_id: str, + elaborated_proposition_hash: str, + proof_obligation_id: str, + registered_definition_ids: Iterable[str], + resolved_dependency_ids: Iterable[str], + verified_theorem_card_ids: Iterable[str], + allowed_assumption_ids: Iterable[str], + environment_hash: str, + expected_plan_hash: str, +) -> ContractDecision: + reasons: list[str] = [] + definitions = set(registered_definition_ids) + dependencies = set(resolved_dependency_ids) + cards = set(verified_theorem_card_ids) + assumptions = set(allowed_assumption_ids) + if not set(plan.required_definition_ids) <= definitions: + reasons.append(ContractRejection.MISSING_DEFINITION.value) + if plan.execution_status != PlanExecutionStatus.EXECUTABLE.value: + reasons.append(ContractRejection.PLANNING_ONLY.value) + if ( + plan.plan_class == "REFRAME_DEFINITIONS_OR_REPRESENTATION" + and not ( + plan.proposition_transformation_ref + or plan.case_partition_ids + ) + ): + reasons.append(ContractRejection.PLANNING_ONLY.value) + if not elaborated_theorem_id or not elaborated_proposition_hash: + reasons.append(ContractRejection.UNELABORATED_TARGET.value) + if not set(plan.dependency_ids) <= dependencies: + reasons.append(ContractRejection.UNRESOLVED_DEPENDENCY.value) + if not set(plan.theorem_card_ids) <= cards: + reasons.append(ContractRejection.UNRESOLVED_THEOREM_CARD.value) + if not plan.success_criterion_id: + reasons.append(ContractRejection.MISSING_SUCCESS_CRITERION.value) + if not plan.abandonment_criterion_id: + reasons.append(ContractRejection.MISSING_FAILURE_CRITERION.value) + if not proof_obligation_id: + reasons.append(ContractRejection.MISSING_PROOF_OBLIGATION.value) + if not set(plan.assumption_ids) <= assumptions: + reasons.append(ContractRejection.HIDDEN_ASSUMPTION.value) + if plan.target_complexity >= plan.parent_complexity: + reasons.append(ContractRejection.NON_REDUCING_TARGET.value) + if plan.environment_hash != environment_hash: + reasons.append(ContractRejection.ENVIRONMENT_HASH_MISMATCH.value) + if plan.content_hash != expected_plan_hash: + reasons.append(ContractRejection.PLAN_HASH_MISMATCH.value) + if reasons: + reason_set = set(reasons) + if reason_set & { + ContractRejection.MISSING_DEFINITION.value, + ContractRejection.UNELABORATED_TARGET.value, + ContractRejection.MISSING_PROOF_OBLIGATION.value, + ContractRejection.PLANNING_ONLY.value, + }: + route = "DECOMPOSER" + elif reason_set & { + ContractRejection.PROPOSITION_HASH_MISMATCH.value, + ContractRejection.UNRESOLVED_DEPENDENCY.value, + }: + route = "MATH_IR_TRANSLATION" + elif reason_set & { + ContractRejection.ENVIRONMENT_HASH_MISMATCH.value, + ContractRejection.PLAN_HASH_MISMATCH.value, + }: + route = "HOST_TYPED_IR_GATE" + else: + route = "STRATEGY_TOURNAMENT" + return ContractDecision(False, tuple(dict.fromkeys(reasons)), route, None) + body: Mapping[str, object] = { + "contract_version": CONTRACT_VERSION, + "plan_id": plan.plan_id, + "plan_hash": plan.content_hash, + "target_ref": plan.target_ref, + "theorem_id": elaborated_theorem_id, + "proposition_hash": elaborated_proposition_hash, + "proof_obligation_id": proof_obligation_id, + "definition_ids": plan.required_definition_ids, + "definition_gap_ids": plan.definition_gap_ids, + "definition_auditor_hash": plan.definition_auditor_hash, + "dependency_ids": plan.dependency_ids, + "theorem_card_ids": plan.theorem_card_ids, + "assumption_ids": plan.assumption_ids, + "success_criterion_id": plan.success_criterion_id, + "failure_criterion_id": plan.abandonment_criterion_id, + "parent_obligation_ref": plan.parent_obligation_ref, + "parent_complexity": plan.parent_complexity, + "target_complexity": plan.target_complexity, + "environment_hash": environment_hash, + } + content_hash = _digest(body) + contract = ResearchContract( + contract_id="RC-" + content_hash[:20], + content_hash=content_hash, + **body, # type: ignore[arg-type] + ) + return ContractDecision(True, ("ACCEPTED",), "PROOF_SEARCH", contract) + + +def verify_contract_binding( + contract: ResearchContract, + *, + proposition_hash: str, + environment_hash: str, +) -> None: + if contract.proposition_hash != proposition_hash: + raise ValueError(ContractRejection.PROPOSITION_HASH_MISMATCH.value) + if contract.environment_hash != environment_hash: + raise ValueError(ContractRejection.ENVIRONMENT_HASH_MISMATCH.value) + body = asdict(contract) + content_hash = body.pop("content_hash") + body.pop("contract_id") + if _digest(body) != content_hash: + raise ValueError("RESEARCH_CONTRACT_CONTENT_HASH_MISMATCH") diff --git a/autoresearch/prefill/stepwise_proof.py b/autoresearch/prefill/stepwise_proof.py new file mode 100644 index 0000000..ed9baf6 --- /dev/null +++ b/autoresearch/prefill/stepwise_proof.py @@ -0,0 +1,465 @@ +"""Crash-safe, action-ID-only Lean proof search.""" +from __future__ import annotations + +import hashlib +import json +import os +import re +import subprocess +import tempfile +from dataclasses import asdict, dataclass, field +from enum import Enum +from pathlib import Path +from typing import Callable, Iterable, Mapping + +from autoresearch.prefill.research_contract import ResearchContract + + +PROOF_SEARCH_VERSION = 1 + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +class ActionKind(str, Enum): + INTRO = "INTRO" + EXACT = "EXACT" + APPLY = "APPLY" + ASSUMPTION = "ASSUMPTION" + CONSTRUCTOR = "CONSTRUCTOR" + SIMP = "SIMP" + REWRITE = "REWRITE" + CASES = "CASES" + + +class FeedbackCode(str, Enum): + ACCEPTED = "ACCEPTED" + TYPE_MISMATCH = "TYPE_MISMATCH" + TACTIC_FAILED = "TACTIC_FAILED" + EXPECTED_SUBGOAL_MISMATCH = "EXPECTED_SUBGOAL_MISMATCH" + ADAPTER_ERROR = "ADAPTER_ERROR" + HOST_ERROR = "HOST_ERROR" + SYNTAX_ERROR = "SYNTAX_ERROR" + + +ZERO_BUDGET_CODES = { + FeedbackCode.ADAPTER_ERROR.value, + FeedbackCode.HOST_ERROR.value, + FeedbackCode.SYNTAX_ERROR.value, +} + + +@dataclass(frozen=True) +class ProofGoal: + goal_id: str + proposition_hash: str + local_context_ids: tuple[str, ...] + subgoal_signature: str + + +@dataclass(frozen=True) +class ProofAction: + action_id: str + kind: str + operand_ids: tuple[str, ...] + theorem_card_id: str = "" + novelty: int = 0 + + +@dataclass(frozen=True) +class ActionSelection: + goal_id: str + action_id: str + operand_ids: tuple[str, ...] + substitution_map_ids: tuple[tuple[str, str], ...] + expected_subgoal_signatures: tuple[str, ...] + + +@dataclass(frozen=True) +class ProofStep: + proof_step_id: str + goal_id: str + selected_lemma_or_action_id: str + substitution_map_ids: tuple[tuple[str, str], ...] + expected_subgoal_signatures: tuple[str, ...] + rendered_ast: str + resulting_subgoal_signatures: tuple[str, ...] + lean_feedback_code: str + + +@dataclass(frozen=True) +class LeanStepResult: + accepted: bool + feedback_code: str + subgoal_signatures: tuple[str, ...] + message_ref: str = "" + + +@dataclass +class ProofSearchState: + contract_id: str + theorem_id: str + proposition_hash: str + environment_hash: str + open_goals: list[ProofGoal] + accepted_steps: list[ProofStep] = field(default_factory=list) + rejected_feedback: list[dict[str, object]] = field(default_factory=list) + semantic_failures: int = 0 + proof_budget: int = 32 + tokens_consumed: int = 0 + status: str = "SEARCHING" + schema_version: int = 1 + + +@dataclass(frozen=True) +class LeanExecutionContext: + project_root: Path + declaration_source: str + import_names: tuple[str, ...] = ("KakeyaLeanGate",) + timeout_s: float = 120.0 + + +def new_search_state( + contract: ResearchContract, + goals: Iterable[ProofGoal], + *, + proof_budget: int = 32, +) -> ProofSearchState: + if not contract.theorem_id or not contract.proposition_hash: + raise ValueError("PROOF_SEARCH_REFUSES_UNELABORATED_GOAL") + goals = list(goals) + if not goals or any( + goal.proposition_hash != contract.proposition_hash for goal in goals[:1] + ): + raise ValueError("PROOF_SEARCH_REQUIRES_CURRENT_LEAN_PROOF_STATE") + return ProofSearchState( + contract.contract_id, + contract.theorem_id, + contract.proposition_hash, + contract.environment_hash, + goals, + proof_budget=proof_budget, + ) + + +def enumerate_applicable_actions( + state: ProofSearchState, + *, + local_context_ids: Iterable[str], + theorem_card_to_operand_id: Mapping[str, str], + constructor_ids: Iterable[str] = (), + rewrite_ids: Iterable[str] = (), +) -> tuple[ProofAction, ...]: + if not state.open_goals: + return () + actions = [ + ProofAction("A_INTRO", ActionKind.INTRO.value, ()), + ProofAction("A_ASSUMPTION", ActionKind.ASSUMPTION.value, ()), + ProofAction("A_SIMP", ActionKind.SIMP.value, ()), + ] + for index, operand in enumerate(sorted(set(local_context_ids)), 1): + actions.append(ProofAction( + f"A_EXACT_{index}", ActionKind.EXACT.value, (operand,), novelty=1, + )) + for index, (card_id, operand) in enumerate( + sorted(theorem_card_to_operand_id.items()), 1, + ): + actions.append(ProofAction( + f"A_APPLY_{index}", ActionKind.APPLY.value, (operand,), + theorem_card_id=card_id, novelty=2, + )) + for index, constructor in enumerate(sorted(set(constructor_ids)), 1): + actions.append(ProofAction( + f"A_CONSTRUCTOR_{index}", ActionKind.CONSTRUCTOR.value, + (constructor,), + )) + for index, rewrite in enumerate(sorted(set(rewrite_ids)), 1): + actions.append(ProofAction( + f"A_REWRITE_{index}", ActionKind.REWRITE.value, (rewrite,), + )) + return tuple(actions) + + +def validate_selection( + selection: ActionSelection, + actions: Iterable[ProofAction], + state: ProofSearchState, +) -> ProofAction: + if not state.open_goals or selection.goal_id != state.open_goals[0].goal_id: + raise ValueError("SELECTION_NOT_AT_FIRST_UNPROVED_SUBGOAL") + registry = {action.action_id: action for action in actions} + action = registry.get(selection.action_id) + if action is None: + raise ValueError("UNREGISTERED_PROOF_ACTION_ID") + if tuple(selection.operand_ids) != action.operand_ids: + raise ValueError("UNREGISTERED_ACTION_OPERAND_ID") + substitutions = dict(selection.substitution_map_ids) + if len(substitutions) != len(selection.substitution_map_ids): + raise ValueError("DUPLICATE_SUBSTITUTION_ID") + return action + + +def render_lean_ast( + action: ProofAction, + *, + operand_sources: Mapping[str, str], + substitution_sources: Mapping[str, str], + substitution_map_ids: Iterable[tuple[str, str]] = (), +) -> str: + """Render a tiny registered tactic AST; no model text reaches Lean.""" + operands = [] + for operand_id in action.operand_ids: + if operand_id not in operand_sources: + raise ValueError("UNKNOWN_OPERAND_SOURCE") + operands.append(operand_sources[operand_id]) + substitutions = [] + for variable_id, value_id in substitution_map_ids: + if variable_id not in substitution_sources: + raise ValueError("UNKNOWN_SUBSTITUTION_VARIABLE") + if value_id not in substitution_sources: + raise ValueError("UNKNOWN_SUBSTITUTION_VALUE") + substitutions.append( + f"({substitution_sources[variable_id]} := " + f"{substitution_sources[value_id]})" + ) + suffix = (" " + " ".join(substitutions)) if substitutions else "" + kind = ActionKind(action.kind) + if kind == ActionKind.INTRO: + return "intro" + if kind == ActionKind.ASSUMPTION: + return "assumption" + if kind == ActionKind.SIMP: + return "simp" + if kind == ActionKind.CONSTRUCTOR: + return "constructor" + if kind == ActionKind.EXACT: + return f"exact {operands[0]}{suffix}" + if kind == ActionKind.APPLY: + return f"apply {operands[0]}{suffix}" + if kind == ActionKind.REWRITE: + return f"rw [{operands[0]}]" + if kind == ActionKind.CASES: + return f"cases {operands[0]}" + raise ValueError("UNRENDERABLE_PROOF_ACTION") + + +def attempt_step( + state: ProofSearchState, + selection: ActionSelection, + actions: Iterable[ProofAction], + *, + operand_sources: Mapping[str, str], + substitution_sources: Mapping[str, str], + lean_executor: Callable[[str, ProofSearchState], LeanStepResult], + token_count: int = 0, +) -> LeanStepResult: + action = validate_selection(selection, actions, state) + rendered = render_lean_ast( + action, + operand_sources=operand_sources, + substitution_sources=substitution_sources, + substitution_map_ids=selection.substitution_map_ids, + ) + result = lean_executor(rendered, state) + state.tokens_consumed += max(0, int(token_count)) + if result.accepted: + if ( + selection.expected_subgoal_signatures + and selection.expected_subgoal_signatures + != result.subgoal_signatures + ): + result = LeanStepResult( + False, FeedbackCode.EXPECTED_SUBGOAL_MISMATCH.value, + result.subgoal_signatures, result.message_ref, + ) + else: + canonical = { + "contract_id": state.contract_id, + "prior_steps": [step.proof_step_id for step in state.accepted_steps], + "goal_id": selection.goal_id, + "action_id": action.action_id, + "substitutions": selection.substitution_map_ids, + "expected": selection.expected_subgoal_signatures, + "rendered_ast": rendered, + "resulting": result.subgoal_signatures, + } + step_id = "PS-" + _digest(canonical)[:20] + state.accepted_steps.append(ProofStep( + step_id, selection.goal_id, action.action_id, + selection.substitution_map_ids, + selection.expected_subgoal_signatures, rendered, + result.subgoal_signatures, FeedbackCode.ACCEPTED.value, + )) + # Lean returns the complete current subgoal vector, so it replaces + # (rather than appends to) the host's prior proof-state snapshot. + state.open_goals = [ + ProofGoal( + f"{selection.goal_id}.{index}", + state.proposition_hash, (), + signature, + ) + for index, signature in enumerate(result.subgoal_signatures, 1) + ] + state.status = "PROVED" if not state.open_goals else "SEARCHING" + return result + state.rejected_feedback.append({ + "goal_id": selection.goal_id, + "action_id": selection.action_id, + "feedback_code": result.feedback_code, + "message_ref": result.message_ref, + }) + if result.feedback_code not in ZERO_BUDGET_CODES: + state.semantic_failures += 1 + if state.semantic_failures >= state.proof_budget: + state.status = "BUDGET_EXHAUSTED" + return result + + +def persist_search_state(path: Path, state: ProofSearchState) -> None: + path = Path(path).expanduser() + path.parent.mkdir(parents=True, exist_ok=True, mode=0o700) + durable = asdict(state) + # Rejections are transient typed feedback to the same search state; only + # Lean-accepted formal steps enter the durable proof artifact. + durable["rejected_feedback"] = [] + payload = json.dumps(durable, sort_keys=True, indent=2) + temporary = path.with_name(f".{path.name}.{os.getpid()}.tmp") + try: + temporary.write_text(payload, encoding="utf-8") + os.chmod(temporary, 0o600) + os.replace(temporary, path) + os.chmod(path, 0o600) + finally: + temporary.unlink(missing_ok=True) + + +def load_search_state(path: Path) -> ProofSearchState | None: + path = Path(path).expanduser() + if not path.exists(): + return None + raw = json.loads(path.read_text(encoding="utf-8")) + raw["open_goals"] = [ProofGoal( + goal_id=item["goal_id"], + proposition_hash=item["proposition_hash"], + local_context_ids=tuple(item["local_context_ids"]), + subgoal_signature=item["subgoal_signature"], + ) for item in raw["open_goals"]] + raw["accepted_steps"] = [ProofStep( + proof_step_id=item["proof_step_id"], + goal_id=item["goal_id"], + selected_lemma_or_action_id=item["selected_lemma_or_action_id"], + substitution_map_ids=tuple( + tuple(pair) for pair in item["substitution_map_ids"] + ), + expected_subgoal_signatures=tuple( + item["expected_subgoal_signatures"], + ), + rendered_ast=item["rendered_ast"], + resulting_subgoal_signatures=tuple( + item["resulting_subgoal_signatures"], + ), + lean_feedback_code=item["lean_feedback_code"], + ) for item in raw["accepted_steps"]] + state = ProofSearchState(**raw) + # The ordered open_goals list makes resume deterministic at index zero. + return state + + +def beam_rank( + candidates: Iterable[tuple[ProofSearchState, ProofAction]], + *, + beam_width: int, +) -> tuple[tuple[ProofSearchState, ProofAction], ...]: + return tuple(sorted( + candidates, + key=lambda item: ( + len(item[0].open_goals), + item[0].semantic_failures, + -int(bool(item[1].theorem_card_id)), + -item[1].novelty, + item[1].action_id, + ), + )[:beam_width]) + + +def tokens_per_accepted_step(state: ProofSearchState) -> float: + return ( + state.tokens_consumed / len(state.accepted_steps) + if state.accepted_steps else 0.0 + ) + + +def lean_step_executor( + context: LeanExecutionContext, +) -> Callable[[str, ProofSearchState], LeanStepResult]: + """Build an immediate real-Lean executor for one deterministic AST step.""" + declaration = context.declaration_source.rstrip() + if ":= by" not in declaration or "\n" in declaration: + raise ValueError("LEAN_EXECUTOR_REQUIRES_ELABORATED_DECLARATION_SCAFFOLD") + + def execute(rendered_ast: str, state: ProofSearchState) -> LeanStepResult: + tactics = [ + *(step.rendered_ast for step in state.accepted_steps), + rendered_ast, + ] + source = "\n".join(( + *(f"import {name}" for name in context.import_names), + "", + declaration, + *(f" {tactic}" for tactic in tactics), + "", + )) + root = Path(context.project_root) + with tempfile.NamedTemporaryFile( + mode="w", suffix=".lean", dir=root, encoding="utf-8", delete=False, + ) as handle: + handle.write(source) + path = Path(handle.name) + try: + result = subprocess.run( + ["lake", "env", "lean", str(path)], + cwd=root, + text=True, + capture_output=True, + timeout=context.timeout_s, + check=False, + ) + except (OSError, subprocess.TimeoutExpired) as exc: + return LeanStepResult( + False, FeedbackCode.HOST_ERROR.value, (), + "host:" + _digest(str(exc))[:16], + ) + finally: + path.unlink(missing_ok=True) + output = (result.stderr or "") + "\n" + (result.stdout or "") + if result.returncode == 0: + return LeanStepResult(True, FeedbackCode.ACCEPTED.value, ()) + if "unsolved goals" in output: + goals = tuple( + " ".join(block.split()) + for block in re.findall( + r"(?:case\s+\S+\s*)?(⊢.*?)(?=\n\n|$)", + output, + re.DOTALL, + ) + ) + return LeanStepResult( + True, FeedbackCode.ACCEPTED.value, + goals or ("UNSOLVED_GOAL",), + ) + lowered = output.lower() + code = ( + FeedbackCode.SYNTAX_ERROR.value + if "unexpected token" in lowered or "parser" in lowered + else FeedbackCode.TYPE_MISMATCH.value + if "type mismatch" in lowered + else FeedbackCode.TACTIC_FAILED.value + ) + return LeanStepResult( + False, code, (), "lean:" + _digest(output)[:16], + ) + + return execute diff --git a/autoresearch/prefill/strategy_tournament.py b/autoresearch/prefill/strategy_tournament.py new file mode 100644 index 0000000..5f2df21 --- /dev/null +++ b/autoresearch/prefill/strategy_tournament.py @@ -0,0 +1,480 @@ +"""Evidence-driven, host-owned strategy tournament. + +Models may rank the short IDs produced here, but cannot author plans, syntax, +assumptions, or feasibility decisions. +""" +from __future__ import annotations + +import hashlib +import json +import time +from dataclasses import asdict, dataclass, field +from enum import Enum +from typing import Iterable, Mapping + + +TOURNAMENT_VERSION = 2 +MIGRATION_EVENT = "strategy_tournament_stepwise_generator_v1" + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +class StrategyEvent(str, Enum): + INITIAL_BRANCH = "INITIAL_BRANCH" + CONFIRMED_BRANCH_FAILURE = "CONFIRMED_BRANCH_FAILURE" + PREMISE_INVALIDATION = "PREMISE_INVALIDATION" + TARGET_CHANGE = "TARGET_CHANGE" + MATHEMATICAL_STAGNATION = "MATHEMATICAL_STAGNATION" + + +class PlanClass(str, Enum): + DIRECT_PROOF = "DIRECT_PROOF" + DISPROOF_OR_COUNTEREXAMPLE = "DISPROOF_OR_COUNTEREXAMPLE" + REDUCTION_TO_KNOWN_RESULT = "REDUCTION_TO_KNOWN_RESULT" + REFRAME_DEFINITIONS_OR_REPRESENTATION = ( + "REFRAME_DEFINITIONS_OR_REPRESENTATION" + ) + + +class FeasibilityReason(str, Enum): + FEASIBLE = "FEASIBLE" + UNMET_DEFINITION = "UNMET_DEFINITION" + UNRESOLVED_DEPENDENCY = "UNRESOLVED_DEPENDENCY" + HIDDEN_ASSUMPTION = "HIDDEN_ASSUMPTION" + CIRCULAR_REDUCTION = "CIRCULAR_REDUCTION" + MISSING_FALSIFIER = "MISSING_FALSIFIER" + MISSING_THEOREM_SUPPORT = "MISSING_THEOREM_SUPPORT" + DUPLICATE_ROUTE = "DUPLICATE_ROUTE" + NO_GO_ROUTE = "NO_GO_ROUTE" + NON_REDUCING_TARGET = "NON_REDUCING_TARGET" + PLANNING_ONLY = "PLANNING_ONLY" + + +class CriticReason(str, Enum): + MAXIMIZES_INFORMATION_GAIN = "MAXIMIZES_INFORMATION_GAIN" + STRONGEST_THEOREM_SUPPORT = "STRONGEST_THEOREM_SUPPORT" + LOWEST_COMPLEXITY = "LOWEST_COMPLEXITY" + LOWEST_RISK = "LOWEST_RISK" + STRICTEST_REDUCTION = "STRICTEST_REDUCTION" + + +class PlanExecutionStatus(str, Enum): + EXECUTABLE = "EXECUTABLE" + PLANNING_ONLY = "PLANNING_ONLY" + + +@dataclass(frozen=True) +class LemmaNode: + lemma_id: str + dependency_ids: tuple[str, ...] + target_ref: str + complexity: int + + +@dataclass(frozen=True) +class StrategyPlan: + plan_id: str + plan_class: str + target_ref: str + required_definition_ids: tuple[str, ...] + theorem_card_ids: tuple[str, ...] + dependency_ids: tuple[str, ...] + lemma_graph: tuple[LemmaNode, ...] + falsification_test_id: str + success_criterion_id: str + abandonment_criterion_id: str + expected_information_gain: int + assumption_ids: tuple[str, ...] + restriction_ids: tuple[str, ...] + parent_obligation_ref: str + parent_complexity: int + target_complexity: int + risk: int + source_move_id: str + environment_hash: str + evidence_refs: tuple[str, ...] + unresolved_definition_ids: tuple[str, ...] + definition_gap_ids: tuple[str, ...] + definition_auditor_hash: str + proposition_transformation_ref: str + case_partition_ids: tuple[str, ...] + execution_status: str + content_hash: str + + +@dataclass(frozen=True) +class FeasibilityDecision: + plan_id: str + feasible: bool + reason_codes: tuple[str, ...] + deterministic_score: tuple[int, int, int, int, int] + score_explanation: Mapping[str, int] + + +@dataclass(frozen=True) +class TournamentResult: + event_id: str + event_type: str + plans: tuple[StrategyPlan, ...] + decisions: tuple[FeasibilityDecision, ...] + pareto_plan_ids: tuple[str, ...] + critic_ranked_plan_ids: tuple[str, ...] + critic_reason_codes: tuple[str, ...] + selected_plan_id: str + content_hash: str + + +@dataclass(frozen=True) +class BranchEvidence: + evidence_id: str + event_type: str + accepted_child_delta: int = 0 + lean_theorem_delta: int = 0 + verified_counterexample_delta: int = 0 + semantic_failure_delta: int = 0 + reason_codes: tuple[str, ...] = () + provenance_hash: str = "" + + +@dataclass +class BranchHistory: + branch_id: str + plan_ids: list[str] = field(default_factory=list) + evidence: list[BranchEvidence] = field(default_factory=list) + score: int = 0 + status: str = "ACTIVE" + disposition_reason_codes: list[str] = field(default_factory=list) + + +def strategy_event_due( + event_type: StrategyEvent | None, + *, + rounds_without_verified_progress: int, + stagnation_threshold: int, +) -> bool: + """Events are explicit; outer-loop iteration alone is never a trigger.""" + if event_type is None: + return rounds_without_verified_progress >= stagnation_threshold + return event_type in set(StrategyEvent) + + +def build_host_plans( + *, + target_ref: str, + parent_obligation_ref: str, + parent_complexity: int, + environment_hash: str, + registered_definition_ids: Iterable[str], + theorem_card_ids: Iterable[str], + dependency_ids: Iterable[str], + evidence_refs: Iterable[str], + unresolved_definition_ids: Iterable[str] = (), + definition_gap_ids: Iterable[str] = (), + definition_auditor_hash: str = "", + elaborated_theorem_id: str = "", + proposition_hash: str = "", +) -> tuple[StrategyPlan, ...]: + """Construct one independent host plan per mandatory plan class.""" + registered = tuple(sorted(set(registered_definition_ids))) + unresolved = tuple(sorted(set(unresolved_definition_ids))) + definitions = tuple(sorted(set((*registered, *unresolved)))) + gaps = tuple(sorted(set(definition_gap_ids))) + cards = tuple(sorted(set(theorem_card_ids))) + dependencies = tuple(sorted(set(dependency_ids))) + evidence = tuple(sorted(set(evidence_refs))) + specs = ( + (PlanClass.DIRECT_PROOF, "MOVE_DIRECT", cards[:1], 3, 2), + (PlanClass.DISPROOF_OR_COUNTEREXAMPLE, "MOVE_FALSIFY", (), 5, 2), + (PlanClass.REDUCTION_TO_KNOWN_RESULT, "MOVE_REDUCE", cards[:2], 4, 3), + ( + PlanClass.REFRAME_DEFINITIONS_OR_REPRESENTATION, + "MOVE_REFRAME", (), 5, 1, + ), + ) + plans = [] + for index, (kind, move_id, support, gain, risk) in enumerate(specs, 1): + target_complexity = max(0, parent_complexity - index) + lemma_id = f"L{index}" + transformation_ref = ( + "typed-reframe:" + proposition_hash + if ( + kind == PlanClass.REFRAME_DEFINITIONS_OR_REPRESENTATION + and elaborated_theorem_id + and proposition_hash + ) + else "" + ) + case_partitions = ( + (f"case:{proposition_hash[:20]}",) + if transformation_ref else () + ) + execution_status = ( + PlanExecutionStatus.EXECUTABLE.value + if elaborated_theorem_id and proposition_hash + else PlanExecutionStatus.PLANNING_ONLY.value + ) + canonical = { + "version": TOURNAMENT_VERSION, + "plan_class": kind.value, + "target_ref": target_ref, + "definitions": definitions, + "unresolved_definitions": unresolved, + "definition_gap_ids": gaps, + "definition_auditor_hash": definition_auditor_hash, + "theorem_cards": support, + "dependencies": dependencies, + "lemma_graph": [{ + "lemma_id": lemma_id, + "dependency_ids": dependencies, + "target_ref": target_ref, + "complexity": target_complexity, + }], + "falsification_test_id": f"FALSIFY_{kind.value}", + "success_criterion_id": f"SUCCESS_{kind.value}", + "abandonment_criterion_id": f"ABANDON_{kind.value}", + "information_gain": gain, + "assumptions": (), + "restrictions": (), + "parent": parent_obligation_ref, + "parent_complexity": parent_complexity, + "target_complexity": target_complexity, + "risk": risk, + "source_move_id": move_id, + "environment_hash": environment_hash, + "evidence_refs": evidence, + "proposition_transformation_ref": transformation_ref, + "case_partition_ids": case_partitions, + "execution_status": execution_status, + } + content_hash = _digest(canonical) + plans.append(StrategyPlan( + plan_id=f"P{index}", + plan_class=kind.value, + target_ref=target_ref, + required_definition_ids=definitions, + theorem_card_ids=tuple(support), + dependency_ids=dependencies, + lemma_graph=(LemmaNode( + lemma_id, dependencies, target_ref, target_complexity, + ),), + falsification_test_id=canonical["falsification_test_id"], + success_criterion_id=canonical["success_criterion_id"], + abandonment_criterion_id=canonical["abandonment_criterion_id"], + expected_information_gain=gain, + assumption_ids=(), + restriction_ids=(), + parent_obligation_ref=parent_obligation_ref, + parent_complexity=parent_complexity, + target_complexity=target_complexity, + risk=risk, + source_move_id=move_id, + environment_hash=environment_hash, + evidence_refs=evidence, + unresolved_definition_ids=unresolved, + definition_gap_ids=gaps, + definition_auditor_hash=definition_auditor_hash, + proposition_transformation_ref=transformation_ref, + case_partition_ids=case_partitions, + execution_status=execution_status, + content_hash=content_hash, + )) + return tuple(plans) + + +def evaluate_feasibility( + plans: Iterable[StrategyPlan], + *, + registered_definition_ids: Iterable[str], + resolved_dependency_ids: Iterable[str], + verified_theorem_card_ids: Iterable[str], + allowed_assumption_ids: Iterable[str], + no_go_hashes: Iterable[str] = (), +) -> tuple[FeasibilityDecision, ...]: + definitions = set(registered_definition_ids) + dependencies = set(resolved_dependency_ids) + cards = set(verified_theorem_card_ids) + assumptions = set(allowed_assumption_ids) + no_go = set(no_go_hashes) + seen_routes: set[tuple[str, str, str]] = set() + decisions = [] + for plan in plans: + reasons: list[str] = [] + if not set(plan.required_definition_ids) <= definitions: + reasons.append(FeasibilityReason.UNMET_DEFINITION.value) + if plan.execution_status != PlanExecutionStatus.EXECUTABLE.value: + reasons.append(FeasibilityReason.PLANNING_ONLY.value) + if ( + plan.plan_class + == PlanClass.REFRAME_DEFINITIONS_OR_REPRESENTATION.value + and plan.execution_status == PlanExecutionStatus.EXECUTABLE.value + and not ( + plan.proposition_transformation_ref + or plan.case_partition_ids + ) + ): + reasons.append(FeasibilityReason.PLANNING_ONLY.value) + if not set(plan.dependency_ids) <= dependencies: + reasons.append(FeasibilityReason.UNRESOLVED_DEPENDENCY.value) + if not set(plan.assumption_ids) <= assumptions: + reasons.append(FeasibilityReason.HIDDEN_ASSUMPTION.value) + if not plan.falsification_test_id: + reasons.append(FeasibilityReason.MISSING_FALSIFIER.value) + if ( + plan.plan_class == PlanClass.REDUCTION_TO_KNOWN_RESULT.value + and not plan.theorem_card_ids + ): + reasons.append(FeasibilityReason.MISSING_THEOREM_SUPPORT.value) + if not set(plan.theorem_card_ids) <= cards: + reasons.append(FeasibilityReason.MISSING_THEOREM_SUPPORT.value) + graph_ids = {node.lemma_id for node in plan.lemma_graph} + if plan.parent_obligation_ref in graph_ids: + reasons.append(FeasibilityReason.CIRCULAR_REDUCTION.value) + if plan.target_complexity >= plan.parent_complexity: + reasons.append(FeasibilityReason.NON_REDUCING_TARGET.value) + route = (plan.plan_class, plan.target_ref, plan.source_move_id) + if route in seen_routes: + reasons.append(FeasibilityReason.DUPLICATE_ROUTE.value) + seen_routes.add(route) + if plan.content_hash in no_go: + reasons.append(FeasibilityReason.NO_GO_ROUTE.value) + feasible = not reasons + explanation = { + "information_gain": plan.expected_information_gain, + "theorem_support": len(plan.theorem_card_ids), + "strict_reduction": plan.parent_complexity - plan.target_complexity, + "complexity": plan.target_complexity, + "risk": plan.risk, + } + score = ( + -explanation["information_gain"], + -explanation["theorem_support"], + -explanation["strict_reduction"], + explanation["complexity"], + explanation["risk"], + ) + decisions.append(FeasibilityDecision( + plan.plan_id, feasible, + tuple(reasons or (FeasibilityReason.FEASIBLE.value,)), + score, explanation, + )) + return tuple(decisions) + + +def _dominates(left: FeasibilityDecision, right: FeasibilityDecision) -> bool: + a, b = left.score_explanation, right.score_explanation + maximize = ("information_gain", "theorem_support", "strict_reduction") + minimize = ("complexity", "risk") + no_worse = ( + all(a[key] >= b[key] for key in maximize) + and all(a[key] <= b[key] for key in minimize) + ) + better = ( + any(a[key] > b[key] for key in maximize) + or any(a[key] < b[key] for key in minimize) + ) + return no_worse and better + + +def run_tournament( + *, + event_id: str, + event_type: StrategyEvent, + plans: Iterable[StrategyPlan], + decisions: Iterable[FeasibilityDecision], + critic_ranked_plan_ids: Iterable[str] = (), + critic_reason_codes: Iterable[CriticReason] = (), +) -> TournamentResult: + plans = tuple(plans) + decisions = tuple(decisions) + if {plan.plan_class for plan in plans} != {item.value for item in PlanClass}: + raise ValueError("TOURNAMENT_REQUIRES_FOUR_INDEPENDENT_PLAN_CLASSES") + feasible = tuple(item for item in decisions if item.feasible) + frontier = tuple(sorted( + item.plan_id for item in feasible + if not any(_dominates(other, item) for other in feasible if other != item) + )) + requested = tuple(critic_ranked_plan_ids) + feasible_ids = {item.plan_id for item in feasible} + # Critic ordering is advisory and can never re-admit an infeasible plan. + ranked = tuple(item for item in requested if item in feasible_ids) + ranked += tuple( + item.plan_id for item in sorted( + feasible, key=lambda decision: ( + decision.deterministic_score, decision.plan_id, + ), + ) if item.plan_id not in ranked + ) + selected = next((item for item in ranked if item in frontier), "") + canonical = { + "version": TOURNAMENT_VERSION, + "event_id": event_id, + "event_type": event_type.value, + "plans": [asdict(item) for item in plans], + "decisions": [asdict(item) for item in decisions], + "pareto": frontier, + "critic_ranking": ranked, + "critic_reasons": [item.value for item in critic_reason_codes], + "selected": selected, + } + return TournamentResult( + event_id, event_type.value, plans, decisions, frontier, ranked, + tuple(item.value for item in critic_reason_codes), selected, + _digest(canonical), + ) + + +def review_branch( + history: BranchHistory, + *, + stagnation_threshold: int, + failure_threshold: int, +) -> BranchHistory: + """Review only persisted evidence; callers cannot inject a verdict.""" + progress = sum( + item.accepted_child_delta + item.lean_theorem_delta + + item.verified_counterexample_delta + for item in history.evidence + if item.provenance_hash + ) + failures = sum( + item.semantic_failure_delta for item in history.evidence + if item.provenance_hash + ) + history.score = progress * 10 - failures + if failures >= failure_threshold: + history.status = "QUARANTINED" + history.disposition_reason_codes = ["CONFIRMED_FAILURE_THRESHOLD"] + elif len(history.evidence) >= stagnation_threshold and progress == 0: + history.status = "REFRAME_REQUIRED" + history.disposition_reason_codes = ["OBJECTIVE_MATHEMATICAL_STAGNATION"] + else: + history.status = "ACTIVE" + history.disposition_reason_codes = [] + return history + + +def branch_review_record(history: BranchHistory) -> dict[str, object]: + return { + "schema_version": 1, + "branch_id": history.branch_id, + "reviewed_at": time.time(), + "evidence_ids": [item.evidence_id for item in history.evidence], + "evidence_provenance_hashes": [ + item.provenance_hash for item in history.evidence + ], + "score": history.score, + "status": history.status, + "disposition_reason_codes": list(history.disposition_reason_codes), + "assistant_verdict": None, + "content_hash": _digest({ + "branch_id": history.branch_id, + "evidence": [asdict(item) for item in history.evidence], + "score": history.score, + "status": history.status, + "reasons": history.disposition_reason_codes, + }), + } diff --git a/autoresearch/prefill/theorem_cards.py b/autoresearch/prefill/theorem_cards.py new file mode 100644 index 0000000..2841a93 --- /dev/null +++ b/autoresearch/prefill/theorem_cards.py @@ -0,0 +1,196 @@ +"""Deterministic, bounded theorem cards for the pinned Lean environment.""" +from __future__ import annotations + +import hashlib +import json +import os +import subprocess +import tempfile +from dataclasses import asdict, dataclass +from pathlib import Path +from typing import Iterable + + +CARD_SCHEMA_VERSION = 1 + + +@dataclass(frozen=True) +class TheoremCard: + card_id: str + theorem_name: str + exact_type: str + import_name: str + source_path: str + source_hash: str + environment_hash: str + applicability_tags: tuple[str, ...] + required_hypotheses: tuple[str, ...] + description: str + + @property + def content_hash(self) -> str: + return _digest(asdict(self)) + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +def pinned_environment_hash(project_root: Path) -> str: + root = Path(project_root) + return _digest({ + name: (root / name).read_text(encoding="utf-8") + for name in ("lean-toolchain", "lake-manifest.json", "lakefile.lean") + }) + + +def _source_hash(root: Path, relative: str) -> str: + return hashlib.sha256((root / relative).read_bytes()).hexdigest() + + +_CARD_SPECS = ( + ( + "locally_uniform_limit_holomorphic", + "TendstoLocallyUniformlyOn.differentiableOn", + """{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] +{U : Set ℂ} {φ : Filter ι} {F : ι → ℂ → E} {f : ℂ → E} [CompleteSpace E] [φ.NeBot] +(hf : TendstoLocallyUniformlyOn F f φ U) +(hF : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) : +DifferentiableOn ℂ f U""", + "Mathlib.Analysis.Complex.LocallyUniformLimit", + ".lake/packages/mathlib/Mathlib/Analysis/Complex/LocallyUniformLimit.lean", + ("locally_uniform_limit", "holomorphic_sum", "disk"), + ("filter_nebot", "local_uniform_convergence", "eventual_holomorphicity", "open_domain"), + "A locally uniform limit of holomorphic functions on an open set is holomorphic.", + ), + ( + "holomorphic_tsum_summable_bound", + "Complex.differentiableOn_tsum_of_summable_norm", + """{E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] +{U : Set ℂ} {F : ι → ℂ → E} [CompleteSpace E] {u : ι → ℝ} (hu : Summable u) +(hf : ∀ i, DifferentiableOn ℂ (F i) U) (hU : IsOpen U) +(hF_le : ∀ i w, w ∈ U → ‖F i w‖ ≤ u i) : +DifferentiableOn ℂ (fun w => ∑' i, F i w) U""", + "Mathlib.Analysis.Complex.LocallyUniformLimit", + ".lake/packages/mathlib/Mathlib/Analysis/Complex/LocallyUniformLimit.lean", + ("holomorphic_sum", "tsum", "summable_majorant"), + ("summable_norm_bound", "termwise_holomorphicity", "open_domain"), + "A summably dominated series of holomorphic terms has a holomorphic sum.", + ), + ( + "removable_singularity_continuous", + "Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt", + """{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] +{f : ℂ → E} {c : ℂ} +(hd : ∀ᶠ z in 𝓝[≠] c, DifferentiableAt ℂ f z) +(hc : ContinuousAt f c) : AnalyticAt ℂ f c""", + "Mathlib.Analysis.Complex.RemovableSingularity", + ".lake/packages/mathlib/Mathlib/Analysis/Complex/RemovableSingularity.lean", + ("removable_singularity", "analytic_extension", "punctured_neighborhood"), + ("punctured_holomorphicity", "continuity_at_center"), + "Punctured-neighborhood holomorphicity plus continuity makes the singularity removable.", + ), + ( + "removable_singularity_bounded", + "Complex.differentiableOn_update_limUnder_of_bddAbove", + """{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] +{f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ 𝓝 c) +(hd : DifferentiableOn ℂ f (s \\ {c})) +(hb : BddAbove (norm ∘ f '' (s \\ {c}))) : +DifferentiableOn ℂ (Function.update f c ((𝓝[≠] c).limUnder f)) s""", + "Mathlib.Analysis.Complex.RemovableSingularity", + ".lake/packages/mathlib/Mathlib/Analysis/Complex/RemovableSingularity.lean", + ("removable_singularity", "bounded", "holomorphic_extension"), + ("neighborhood", "punctured_holomorphicity", "bounded_image"), + "A bounded punctured holomorphic function extends differentiably across the center.", + ), + ( + "analytic_identity_principle", + "AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq", + """{𝕜 E F} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] +[NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : E → F} {U : Set E} +(hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) +{z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[𝓝 z₀] g) : Set.EqOn f g U""", + "Mathlib.Analysis.Analytic.Uniqueness", + ".lake/packages/mathlib/Mathlib/Analysis/Analytic/Uniqueness.lean", + ("identity_principle", "analytic_continuation", "preconnected"), + ("both_analytic", "preconnected_domain", "local_eventual_equality"), + "Analytic functions locally equal at one point agree on a preconnected domain.", + ), +) + + +def build_theorem_card_index(project_root: Path) -> tuple[TheoremCard, ...]: + root = Path(project_root) + environment_hash = pinned_environment_hash(root) + cards = tuple(TheoremCard( + card_id=card_id, + theorem_name=name, + exact_type=exact_type, + import_name=import_name, + source_path=source_path, + source_hash=_source_hash(root, source_path), + environment_hash=environment_hash, + applicability_tags=tuple(tags), + required_hypotheses=tuple(hypotheses), + description=description, + ) for ( + card_id, name, exact_type, import_name, source_path, tags, + hypotheses, description, + ) in _CARD_SPECS) + return tuple(sorted(cards, key=lambda item: item.card_id)) + + +def search_theorem_cards( + cards: Iterable[TheoremCard], + tags: Iterable[str], + *, + limit: int = 8, +) -> tuple[TheoremCard, ...]: + wanted = frozenset(str(tag) for tag in tags) + ranked = sorted( + ( + (len(wanted.intersection(card.applicability_tags)), card.card_id, card) + for card in cards + ), + key=lambda item: (-item[0], item[1]), + ) + return tuple(card for score, _card_id, card in ranked if score > 0)[:limit] + + +def validate_theorem_cards( + cards: Iterable[TheoremCard], + *, + project_root: Path, + timeout_s: float = 120.0, +) -> None: + root = Path(project_root) + expected_environment = pinned_environment_hash(root) + cards = tuple(cards) + for card in cards: + if card.environment_hash != expected_environment: + raise ValueError(f"STALE_THEOREM_CARD_ENVIRONMENT:{card.card_id}") + if card.source_hash != _source_hash(root, card.source_path): + raise ValueError(f"STALE_THEOREM_CARD_SOURCE:{card.card_id}") + content = "\n".join( + [*(f"import {name}" for name in sorted({c.import_name for c in cards})), ""], + ) + "\n".join(f"#check {card.theorem_name}" for card in cards) + "\n" + with tempfile.NamedTemporaryFile( + mode="w", suffix=".lean", dir=root, encoding="utf-8", delete=False, + ) as handle: + handle.write(content) + path = Path(handle.name) + try: + result = subprocess.run( + ["lake", "env", "lean", str(path)], + cwd=root, text=True, capture_output=True, timeout=timeout_s, check=False, + ) + finally: + path.unlink(missing_ok=True) + if result.returncode: + raise ValueError( + "THEOREM_CARD_ELABORATION_FAILED:" + + (result.stderr or result.stdout).strip() + ) diff --git a/scripts/migrate_atomic_define_one_concept_v1.py b/scripts/migrate_atomic_define_one_concept_v1.py new file mode 100644 index 0000000..d210011 --- /dev/null +++ b/scripts/migrate_atomic_define_one_concept_v1.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Migrate the active Architecture-7 definition loop crash-safely.""" +from __future__ import annotations + +import argparse +import json +import os +import shutil +import time +from dataclasses import asdict +from pathlib import Path + +from autoresearch.prefill.atomic_definition import ( + MIGRATION_EVENT, + define_one_concept, + dependency_graph_for_audit, + first_dependency_closed_gap, +) +from autoresearch.prefill.orchestration_state import ( + ProofState, + current_capability_manifest, + load_checkpoint, + save_checkpoint, +) +from autoresearch.prefill.theorem_cards import pinned_environment_hash + + +def _snapshot(home: Path, destination: Path, supervisor_pid: int) -> Path: + destination.mkdir(parents=True, exist_ok=False, mode=0o700) + sources = ( + home / "autoresearch/proof_orchestration.json", + home / "autoresearch/proof_orchestration.journal.jsonl", + home / "autoresearch/proof_orchestration.artifacts", + home / "agent_gan_proof_ledger.json", + home / "agent_gan_state.json", + home / "proof_live_status.json", + home / "autoresearch/results.tsv", + ) + records = [] + for source in sources: + if not source.exists(): + continue + target = destination / source.name + if source.is_dir(): + shutil.copytree(source, target) + else: + shutil.copy2(source, target) + records.append({"source": str(source), "snapshot": str(target)}) + manifest = { + "migration_event": MIGRATION_EVENT, + "old_supervisor_pid": supervisor_pid, + "created_at": time.time(), + "files": records, + } + (destination / "manifest.json").write_text( + json.dumps(manifest, indent=2, sort_keys=True), + encoding="utf-8", + ) + return destination + + +def migrate( + *, + home: Path, + project_root: Path, + supervisor_pid: int, + snapshot: Path, +) -> dict: + checkpoint_path = home / "autoresearch/proof_orchestration.json" + raw = json.loads(checkpoint_path.read_text(encoding="utf-8")) + if raw.get("migration_event") == MIGRATION_EVENT: + raw.update(current_capability_manifest()) + raw["adapter_status"] = "" + raw["blocked_reason"] = "" + temporary = checkpoint_path.with_name( + f".{checkpoint_path.name}.{os.getpid()}.tmp", + ) + temporary.write_text( + json.dumps(raw, ensure_ascii=False, indent=2), + encoding="utf-8", + ) + os.replace(temporary, checkpoint_path) + return { + "event": MIGRATION_EVENT, + "status": "IDEMPOTENT_REPLAY", + "snapshot": raw.get("migration_snapshot", ""), + "current_gap": raw.get("current_definition_gap_id", ""), + } + try: + os.kill(supervisor_pid, 0) + except ProcessLookupError: + pass + else: + raise RuntimeError("supervisor must be stopped before migration") + _snapshot(home, snapshot, supervisor_pid) + raw.update(current_capability_manifest()) + raw["capability_flags"] = current_capability_manifest()["capability_flags"] + checkpoint_path.write_text( + json.dumps(raw, ensure_ascii=False, indent=2), + encoding="utf-8", + ) + checkpoint = load_checkpoint(checkpoint_path) + if checkpoint is None: + raise RuntimeError("checkpoint disappeared during migration") + auditor = checkpoint.validated_artifacts.get("definition_auditor") + if auditor is None: + raise RuntimeError("migration requires a validated Definition Auditor") + audit = json.loads(Path(auditor.path).read_text(encoding="utf-8")) + missing = tuple(audit.get("missing_definitions", ())) + graph = dependency_graph_for_audit(missing) + environment_hash = pinned_environment_hash(project_root) + registry_path = checkpoint_path.with_name( + "proof_orchestration.definition_registry.json", + ) + migrated_resolutions = [] + for restriction_id in ("DEF_EPSILON", "DEF_GENUS"): + gap = next( + ( + item for item in missing + if item.get("definition_id") == restriction_id + ), + None, + ) + if gap is None: + continue + result = define_one_concept( + gap=gap, + definition_auditor_hash=auditor.sha256, + dependency_graph=graph, + registry_path=registry_path, + project_root=project_root, + theorem_card_ids=(), + current_environment_hash=environment_hash, + ) + migrated_resolutions.append(asdict(result)) + resolved = { + item["gap_id"] for item in migrated_resolutions + if item["status"] in {"RESOLVED", "IDEMPOTENT_REPLAY"} + } + first_gap = first_dependency_closed_gap( + missing, + dependency_graph=graph, + resolved_gap_ids=resolved, + ) + for role in ( + "decomposer", "synthesis", "math_ir_translator", + "host_typed_ir_gate", "strategy_tournament", "research_contract", + ): + reference = checkpoint.validated_artifacts.pop(role, None) + if reference is not None: + checkpoint.invalidated_artifacts[reference.sha256] = { + **asdict(reference), + "audit_only": True, + "reason_codes": [ + "LEGACY_DEFINITION_REGISTRATION_NOT_PROGRESS", + "PLACEHOLDER_TRUE_NOT_PROGRESS", + ], + "migration_event": MIGRATION_EVENT, + } + checkpoint.state = ProofState.STRATEGY_TOURNAMENT.value + checkpoint.current_role = "strategy_tournament" + checkpoint.adapter_status = "" + checkpoint.blocked_reason = "" + checkpoint.selected_move_id = "DEFINE_ONE_CONCEPT" + checkpoint.active_gate = "HOST_DEFINITION_GATE" + checkpoint.current_definition_gap_id = ( + str(first_gap.get("definition_id", "")) if first_gap else "" + ) + checkpoint.candidate_count = 0 + checkpoint.definition_candidate_count = 0 + checkpoint.typed_ir_hash = "" + checkpoint.lean_declaration_hash = "" + checkpoint.proposition_hash = "" + checkpoint.elaborated_theorem_id = "" + checkpoint.new_elaborated_definitions = 0 + checkpoint.new_elaborated_lemmas = 0 + checkpoint.definitions_added = 0 + checkpoint.lemmas_proved = 0 + checkpoint.progress_vector = { + "definitions_added": 0, + "existing_definitions_resolved": 0, + "lemmas_proved": 0, + "accepted_children": 0, + "subgoals_closed": 0, + "verified_counterexamples": 0, + } + checkpoint.progress_fingerprint = "" + checkpoint.semantic_stagnation_count = 0 + checkpoint.stagnation_reason = "" + checkpoint.forbidden_semantic_fingerprints = [] + checkpoint.strategy_event_id = "" + checkpoint.strategy_event_type = "" + checkpoint.research_contract_id = "" + checkpoint.research_contract_hash = "" + checkpoint.research_contract_rejection_codes = [] + checkpoint.migration_event = MIGRATION_EVENT + checkpoint.migration_snapshot = str(snapshot) + checkpoint.last_transition_reason = ( + "migration:atomic-define-one-concept:first-dependency-closed-gap" + ) + checkpoint.recovery_events.append({ + "event_type": "OPERATOR_MIGRATION", + "event_id": MIGRATION_EVENT, + "from_move": "REGISTER_DEFINITION_OBLIGATION", + "target_state": checkpoint.state, + "current_gap": checkpoint.current_definition_gap_id, + "typed_restrictions_resolved": sorted(resolved), + "created_at": time.time(), + }) + save_checkpoint(checkpoint_path, checkpoint) + return { + "event": MIGRATION_EVENT, + "status": "MIGRATED", + "snapshot": str(snapshot), + "current_gap": checkpoint.current_definition_gap_id, + "typed_restrictions_resolved": sorted(resolved), + } + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--home", type=Path, default=Path.home() / ".kakeya") + parser.add_argument("--project-root", type=Path, required=True) + parser.add_argument("--supervisor-pid", type=int, required=True) + parser.add_argument("--snapshot", type=Path, required=True) + args = parser.parse_args() + result = migrate( + home=args.home.expanduser(), + project_root=args.project_root.expanduser(), + supervisor_pid=args.supervisor_pid, + snapshot=args.snapshot.expanduser(), + ) + print(json.dumps(result, indent=2, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/migrate_autonomous_definition_resolution_v1.py b/scripts/migrate_autonomous_definition_resolution_v1.py new file mode 100644 index 0000000..0d618cd --- /dev/null +++ b/scripts/migrate_autonomous_definition_resolution_v1.py @@ -0,0 +1,167 @@ +#!/usr/bin/env python3 +"""Crash-safe activation migration for definition resolution v1.""" +from __future__ import annotations + +import argparse +import json +import os +import shutil +import time +from dataclasses import asdict +from pathlib import Path + +from autoresearch.prefill.definition_resolution import ( + MIGRATION_EVENT, + migrate_legacy_registry, + store_hash, + resolution_environment_hash, +) +from autoresearch.prefill.orchestration_state import ( + ProofState, + current_capability_manifest, + load_checkpoint, + save_checkpoint, +) +from autoresearch.prefill.theorem_cards import pinned_environment_hash + + +def snapshot_state(home: Path, destination: Path, supervisor_pid: int) -> Path: + destination.mkdir(parents=True, exist_ok=False, mode=0o700) + sources = ( + home / "autoresearch/proof_orchestration.json", + home / "autoresearch/proof_orchestration.journal.jsonl", + home / "autoresearch/proof_orchestration.artifacts", + home / "autoresearch/proof_orchestration.definition_registry.json", + home / "agent_gan_proof_ledger.json", + home / "agent_gan_state.json", + home / "proof_live_status.json", + home / "autoresearch/results.tsv", + ) + copied = [] + for source in sources: + if not source.exists(): + continue + target = destination / source.name + shutil.copytree(source, target) if source.is_dir() else shutil.copy2(source, target) + copied.append({"source": str(source), "snapshot": str(target)}) + manifest = { + "migration_event": MIGRATION_EVENT, + "old_supervisor_pid": supervisor_pid, + "created_at": time.time(), + "files": copied, + } + (destination / "manifest.json").write_text( + json.dumps(manifest, sort_keys=True, indent=2), encoding="utf-8", + ) + return destination + + +def migrate(*, home: Path, project_root: Path, supervisor_pid: int, snapshot: Path) -> dict: + try: + os.kill(supervisor_pid, 0) + except ProcessLookupError: + pass + else: + raise RuntimeError("supervisor must be stopped before migration") + checkpoint_path = home / "autoresearch/proof_orchestration.json" + raw = json.loads(checkpoint_path.read_text(encoding="utf-8")) + if raw.get("migration_event") == MIGRATION_EVENT: + return { + "event": MIGRATION_EVENT, + "status": "IDEMPOTENT_REPLAY", + "snapshot": raw.get("migration_snapshot", ""), + "current_concept": raw.get("current_definition_gap_id", ""), + } + snapshot_state(home, snapshot, supervisor_pid) + legacy_path = checkpoint_path.with_name( + "proof_orchestration.definition_registry.json", + ) + legacy = json.loads(legacy_path.read_text(encoding="utf-8")) if legacy_path.exists() else {} + store = migrate_legacy_registry( + legacy, base_environment_hash=pinned_environment_hash(project_root), + ) + store_path = checkpoint_path.with_name( + "proof_orchestration.definition_resolution.json", + ) + store_path.write_text( + json.dumps(store, ensure_ascii=False, sort_keys=True, indent=2), + encoding="utf-8", + ) + os.chmod(store_path, 0o600) + raw.update(current_capability_manifest()) + raw["schema_version"] = 10 + raw["architecture_version"] = 8 + raw["state"] = ProofState.DEFINITION_RESOLUTION.value + raw["current_role"] = "definition_resolution" + raw["migration_event"] = MIGRATION_EVENT + raw["migration_snapshot"] = str(snapshot) + raw["selected_move_id"] = "RESOLVE_ONE_DEFINITION_QUERY" + raw["active_gate"] = "AUTONOMOUS_DEFINITION_RESOLUTION" + raw["current_definition_gap_id"] = "DEF_SEQUENCE_DENSITY" + raw.pop("definition_registry_hash", None) + raw.pop("definition_registry_hash_delta", None) + raw["definition_store_hash"] = store_hash(store) + raw["definition_environment_hash"] = resolution_environment_hash(store) + raw["definition_store_hash_delta"] = "" + raw["definition_environment_hash_delta"] = "" + raw["definition_query_hash"] = "" + raw["definition_source_statuses"] = {} + raw["definition_property_statuses"] = {} + raw["definition_branch_hashes"] = [] + raw["definition_exhaustion_hash"] = "" + raw["definition_interface_hash"] = "" + raw["definition_backjump_target"] = "" + raw["semantic_stagnation_count"] = 0 + raw["stagnation_reason"] = "" + raw["progress_fingerprint"] = "" + raw["forbidden_semantic_fingerprints"] = [] + raw["typed_ir_hash"] = "" + raw["proposition_hash"] = "" + raw["elaborated_theorem_id"] = "" + raw["adapter_status"] = "" + raw["blocked_reason"] = "" + raw["last_transition_reason"] = "migration:autonomous-definition-resolution-v1" + raw.setdefault("recovery_events", []).append({ + "event_type": "OPERATOR_MIGRATION", + "event_id": MIGRATION_EVENT, + "target_state": ProofState.DEFINITION_RESOLUTION.value, + "current_concept": "DEF_SEQUENCE_DENSITY", + "legacy_definitions": len(store["historical_audit"]), + "legacy_policy": "AUDIT_ONLY_PENDING_SEMANTIC_VALIDATION", + "created_at": time.time(), + }) + checkpoint_path.write_text( + json.dumps(raw, ensure_ascii=False, indent=2), encoding="utf-8", + ) + checkpoint = load_checkpoint(checkpoint_path) + if checkpoint is None: + raise RuntimeError("checkpoint disappeared during migration") + save_checkpoint(checkpoint_path, checkpoint) + return { + "event": MIGRATION_EVENT, + "status": "MIGRATED", + "snapshot": str(snapshot), + "current_concept": checkpoint.current_definition_gap_id, + "legacy_audit_only": len(store["historical_audit"]), + "store_hash": store["store_hash"], + } + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--home", type=Path, default=Path.home() / ".kakeya") + parser.add_argument("--project-root", type=Path, required=True) + parser.add_argument("--supervisor-pid", type=int, required=True) + parser.add_argument("--snapshot", type=Path, required=True) + args = parser.parse_args() + print(json.dumps(migrate( + home=args.home.expanduser(), + project_root=args.project_root.expanduser(), + supervisor_pid=args.supervisor_pid, + snapshot=args.snapshot.expanduser(), + ), indent=2, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/migrate_creative_decomposition_v3.py b/scripts/migrate_creative_decomposition_v3.py new file mode 100644 index 0000000..9739a60 --- /dev/null +++ b/scripts/migrate_creative_decomposition_v3.py @@ -0,0 +1,253 @@ +#!/usr/bin/env python3 +"""Atomically snapshot and migrate a quiescent proof to evidence planning.""" +from __future__ import annotations + +import argparse +import hashlib +import json +import os +import shutil +import time +from pathlib import Path + +from autoresearch.prefill.orchestration_state import ( + ARCHITECTURE_VERSION, + SCHEMA_VERSION, + ProofState, + current_capability_manifest, + load_checkpoint, + save_checkpoint, +) + +MIGRATION_EVENT = "host_feasibility_evidence_planner_v1" + +def _sha256(path: Path) -> str: + digest = hashlib.sha256() + with path.open("rb") as handle: + for chunk in iter(lambda: handle.read(1024 * 1024), b""): + digest.update(chunk) + return digest.hexdigest() + + +def atomic_snapshot( + *, + snapshot_root: Path, + files: tuple[Path, ...], + old_supervisor_pid: int, + ledger_version: int = 87, +) -> Path: + stamp = time.strftime("%Y%m%dT%H%M%SZ", time.gmtime()) + final = snapshot_root / f"evidence-planner-ledger-v{ledger_version}-{stamp}" + temporary = snapshot_root / f".{final.name}.{os.getpid()}.tmp" + snapshot_root.mkdir(parents=True, exist_ok=True, mode=0o700) + if final.exists() or temporary.exists(): + raise FileExistsError(final) + temporary.mkdir(mode=0o700) + manifest_files = [] + try: + used_names: set[str] = set() + for source in files: + if not source.exists(): + continue + snapshot_name = source.name + if snapshot_name in used_names: + snapshot_name = f"{_sha256(source)[:12]}-{snapshot_name}" + used_names.add(snapshot_name) + destination = temporary / snapshot_name + shutil.copy2(source, destination) + os.chmod(destination, 0o600) + manifest_files.append({ + "source": str(source), + "snapshot_name": destination.name, + "sha256": _sha256(destination), + "bytes": destination.stat().st_size, + }) + manifest = { + "schema_version": 1, + "migration_event": MIGRATION_EVENT, + "ledger_version": ledger_version, + "old_supervisor_pid": old_supervisor_pid, + "created_at": time.time(), + "files": manifest_files, + } + manifest_path = temporary / "manifest.json" + manifest_path.write_text( + json.dumps(manifest, sort_keys=True, indent=2), + encoding="utf-8", + ) + os.chmod(manifest_path, 0o600) + directory = os.open(temporary, os.O_RDONLY) + try: + os.fsync(directory) + finally: + os.close(directory) + os.replace(temporary, final) + parent = os.open(snapshot_root, os.O_RDONLY) + try: + os.fsync(parent) + finally: + os.close(parent) + finally: + if temporary.exists(): + shutil.rmtree(temporary) + return final + + +def migrate_checkpoint( + checkpoint_path: Path, + snapshot: Path, + *, + ledger_version: int | None = None, + failed_run_id: str = "", +) -> None: + checkpoint = load_checkpoint(checkpoint_path) + if checkpoint is None: + raise FileNotFoundError(checkpoint_path) + ledger_version = checkpoint.ledger_version if ledger_version is None else ledger_version + prior_checkpoint_ledger_version = checkpoint.ledger_version + if ( + checkpoint.ledger_version != ledger_version + and not ( + checkpoint.ledger_version == ledger_version + 1 + and not checkpoint.committed + ) + ): + raise ValueError( + f"expected ledger v{ledger_version}, found v{checkpoint.ledger_version}" + ) + checkpoint.ledger_version = ledger_version + checkpoint.architecture_version = ARCHITECTURE_VERSION + checkpoint.schema_version = SCHEMA_VERSION + for name, value in current_capability_manifest().items(): + setattr(checkpoint, name, value) + reusable = set(checkpoint.validated_artifacts) + target = ( + ProofState.SYNTHESIS + if "definition_auditor" in reusable + else ProofState.DEFINITION_AUDITOR + ) + checkpoint.state = target.value + checkpoint.current_role = target.value.lower() + checkpoint.resume_origin = "DECOMPOSER" + checkpoint.strategy_reused = True + checkpoint.adapter_status = "" + checkpoint.blocked_reason = "" + checkpoint.migration_event = MIGRATION_EVENT + checkpoint.migration_snapshot = str(snapshot) + checkpoint.stagnation_reason = "LEGACY_DECOMPOSER_OUTPUT_AUDIT_ONLY" + checkpoint.candidate_set_hash = "" + checkpoint.candidate_hashes = [] + checkpoint.candidate_count = 0 + checkpoint.ranking_hash = "" + checkpoint.ranked_candidate_ids = [] + checkpoint.selected_move_id = "" + checkpoint.evidence_gap_graph_hash = "" + checkpoint.proof_plan_hash = "" + checkpoint.proof_plan_id = "" + checkpoint.executable_plan_node_id = "" + checkpoint.plan_score_explanation = {} + checkpoint.last_transition_reason = ( + f"{MIGRATION_EVENT}:resume-{target.value.lower()}" + ) + checkpoint.recovery_events.append({ + "event_type": "OPERATOR_MIGRATION", + "event_id": MIGRATION_EVENT, + "from_ledger_version": ledger_version, + "from_checkpoint_ledger_version": prior_checkpoint_ledger_version, + "target_state": target.value, + "snapshot": str(snapshot), + "failed_run_id": failed_run_id, + "failed_legacy_output": "AUDIT_ONLY_NOT_REUSABLE", + "preserved_validated_artifacts": sorted(reusable), + "created_at": time.time(), + }) + save_checkpoint(checkpoint_path, checkpoint) + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument( + "--home", type=Path, default=Path.home() / ".kakeya", + ) + parser.add_argument("--old-supervisor-pid", type=int, required=True) + parser.add_argument( + "--failed-run-id", default="br_48bdab7c1d75a51f", + ) + parser.add_argument( + "--candidate", + type=Path, + default=Path.cwd() / "autoresearch/prefill/candidate.py", + ) + parser.add_argument( + "--failed-run-artifact", + action="append", + type=Path, + default=[], + ) + parser.add_argument( + "--snapshot", + type=Path, + help="Reuse a quiescent pre-stop snapshot instead of creating one", + ) + args = parser.parse_args() + home = args.home.expanduser() + orchestration = home / "autoresearch/proof_orchestration.json" + ledger = home / "agent_gan_proof_ledger.json" + ledger_payload = json.loads(ledger.read_text(encoding="utf-8")) + ledger_version = int(ledger_payload.get("version", 0)) + if ledger_version <= 0: + raise SystemExit("refusing migration: production ledger has no version") + files = ( + orchestration, + ledger, + args.candidate.expanduser(), + home / "autoresearch/proof_orchestration.journal.jsonl", + home / "agent_gan_state.json", + home / "proof_live_status.json", + *(item.expanduser() for item in args.failed_run_artifact), + ) + snapshot = ( + args.snapshot.expanduser() + if args.snapshot is not None + else atomic_snapshot( + snapshot_root=home / "autoresearch/snapshots", + files=files, + old_supervisor_pid=args.old_supervisor_pid, + ledger_version=ledger_version, + ) + ) + if not snapshot.is_dir(): + raise SystemExit(f"refusing migration: snapshot does not exist: {snapshot}") + migrate_checkpoint( + orchestration, + snapshot, + ledger_version=ledger_version, + failed_run_id=args.failed_run_id, + ) + checkpoint = load_checkpoint(orchestration) + assert checkpoint is not None + journal = orchestration.with_name("proof_orchestration.journal.jsonl") + with journal.open("a", encoding="utf-8") as handle: + handle.write(json.dumps({ + "kind": "operator_event", + "event_id": MIGRATION_EVENT, + "ledger_version": ledger_version, + "old_supervisor_pid": args.old_supervisor_pid, + "snapshot": str(snapshot), + "target_state": checkpoint.state, + "created_at": time.time(), + }, sort_keys=True) + "\n") + handle.flush() + os.fsync(handle.fileno()) + print(json.dumps({ + "migration_event": MIGRATION_EVENT, + "snapshot": str(snapshot), + "ledger_version": ledger_version, + "old_supervisor_pid": args.old_supervisor_pid, + "target_state": checkpoint.state, + }, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/migrate_research_contract_preproof_v2.py b/scripts/migrate_research_contract_preproof_v2.py new file mode 100644 index 0000000..ec59248 --- /dev/null +++ b/scripts/migrate_research_contract_preproof_v2.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +"""Snapshot and migrate a pre-proof Contract deadlock to Decomposer.""" +from __future__ import annotations + +import argparse +import hashlib +import json +import os +import shutil +import time +from dataclasses import asdict +from pathlib import Path + +from autoresearch.prefill.orchestration_state import ( + ProofState, + current_capability_manifest, + load_checkpoint, + save_checkpoint, +) + + +MIGRATION_EVENT = "research_contract_preproof_routing_v2" + + +def snapshot_runtime( + snapshot_root: Path, + sources: tuple[Path, ...], + *, + supervisor_pid: int, + ledger_version: int, +) -> Path: + stamp = time.strftime("%Y%m%dT%H%M%SZ", time.gmtime()) + final = snapshot_root / ( + f"research-contract-preproof-v{ledger_version}-{stamp}" + ) + temporary = snapshot_root / f".{final.name}.{os.getpid()}.tmp" + snapshot_root.mkdir(parents=True, exist_ok=True, mode=0o700) + temporary.mkdir(mode=0o700) + records = [] + try: + for index, source in enumerate(sources): + if not source.exists(): + continue + destination = temporary / f"{index:02d}-{source.name}" + if source.is_dir(): + shutil.copytree(source, destination) + digest = hashlib.sha256(json.dumps(sorted( + str(path.relative_to(destination)) + + ":" + hashlib.sha256(path.read_bytes()).hexdigest() + for path in destination.rglob("*") if path.is_file() + ), separators=(",", ":")).encode()).hexdigest() + else: + shutil.copy2(source, destination) + os.chmod(destination, 0o600) + digest = hashlib.sha256(destination.read_bytes()).hexdigest() + records.append({ + "source": str(source), + "snapshot_name": destination.name, + "sha256": digest, + }) + manifest = { + "schema_version": 1, + "migration_event": MIGRATION_EVENT, + "ledger_version": ledger_version, + "old_supervisor_pid": supervisor_pid, + "created_at": time.time(), + "files": records, + } + manifest_path = temporary / "manifest.json" + manifest_path.write_text( + json.dumps(manifest, sort_keys=True, indent=2), + encoding="utf-8", + ) + os.chmod(manifest_path, 0o600) + descriptor = os.open(temporary, os.O_RDONLY) + try: + os.fsync(descriptor) + finally: + os.close(descriptor) + os.replace(temporary, final) + finally: + if temporary.exists(): + shutil.rmtree(temporary) + return final + + +def migrate( + checkpoint_path: Path, + ledger_path: Path, + snapshot: Path, +) -> dict[str, object]: + checkpoint = load_checkpoint(checkpoint_path) + if checkpoint is None: + raise FileNotFoundError(checkpoint_path) + ledger = json.loads(ledger_path.read_text(encoding="utf-8")) + ledger_version = int(ledger.get("version", 0)) + existing = [ + event for event in checkpoint.recovery_events + if event.get("event_id") == MIGRATION_EVENT + ] + if ( + existing + and checkpoint.proof_state == ProofState.DECOMPOSER + and not checkpoint.research_contract_id + and checkpoint.ledger_version == ledger_version + ): + return existing[-1] + contract_ref = checkpoint.validated_artifacts.pop( + "research_contract", None, + ) + if contract_ref is not None: + checkpoint.invalidated_artifacts[contract_ref.sha256] = { + **asdict(contract_ref), + "audit_only": True, + "read_only": True, + "reason_codes": ["PREPROOF_CONTRACT_INVALID"], + "migration_event": MIGRATION_EVENT, + } + prior_state = checkpoint.state + checkpoint.state = ProofState.DECOMPOSER.value + checkpoint.current_role = "decomposer" + checkpoint.resume_origin = prior_state + checkpoint.strategy_reused = True + checkpoint.ledger_version = ledger_version + checkpoint.adapter_status = "" + checkpoint.blocked_reason = "" + checkpoint.research_contract_id = "" + checkpoint.research_contract_hash = "" + checkpoint.research_contract_rejection_codes = [] + checkpoint.active_gate = "" + checkpoint.migration_event = MIGRATION_EVENT + checkpoint.migration_snapshot = str(snapshot) + checkpoint.last_transition_reason = ( + f"{MIGRATION_EVENT}:resume-at-earliest-semantic-owner" + ) + for name, value in current_capability_manifest().items(): + setattr(checkpoint, name, value) + event = { + "event_type": "OPERATOR_MIGRATION", + "event_id": MIGRATION_EVENT, + "ledger_version": ledger_version, + "from_state": prior_state, + "target_state": ProofState.DECOMPOSER.value, + "snapshot": str(snapshot), + "strategy_tournament_hash": checkpoint.strategy_tournament_hash, + "strategy_plan_ids": list(checkpoint.strategy_plan_ids), + "selected_strategy_plan_id": checkpoint.selected_strategy_plan_id, + "preserved_quarantine_evidence": bool(checkpoint.branch_history), + "created_at": time.time(), + } + checkpoint.recovery_events.append(event) + save_checkpoint(checkpoint_path, checkpoint) + return event + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--home", type=Path, default=Path.home() / ".kakeya") + parser.add_argument("--supervisor-pid", type=int, required=True) + parser.add_argument("--snapshot", type=Path) + args = parser.parse_args() + home = args.home.expanduser() + checkpoint = home / "autoresearch/proof_orchestration.json" + ledger = home / "agent_gan_proof_ledger.json" + payload = json.loads(ledger.read_text(encoding="utf-8")) + checkpoint_payload = json.loads(checkpoint.read_text(encoding="utf-8")) + tournament_value = str( + checkpoint_payload.get("validated_artifacts", {}) + .get("strategy_tournament", {}) + .get("path", "") + ) + sources = [ + checkpoint, + checkpoint.with_name("proof_orchestration.journal.jsonl"), + checkpoint.with_suffix(".artifacts"), + ledger, + home / "proof_live_status.json", + ] + if tournament_value: + sources.insert(2, Path(tournament_value)) + snapshot = ( + args.snapshot.expanduser() if args.snapshot else snapshot_runtime( + home / "autoresearch/snapshots", + tuple(sources), + supervisor_pid=args.supervisor_pid, + ledger_version=int(payload.get("version", 0)), + ) + ) + print(json.dumps(migrate(checkpoint, ledger, snapshot), sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/migrate_strategy_tournament_v1.py b/scripts/migrate_strategy_tournament_v1.py new file mode 100644 index 0000000..f6e3e0a --- /dev/null +++ b/scripts/migrate_strategy_tournament_v1.py @@ -0,0 +1,285 @@ +#!/usr/bin/env python3 +"""Atomically migrate production to architecture 7 and review its branch.""" +from __future__ import annotations + +import argparse +import hashlib +import json +import os +import shutil +import time +from dataclasses import asdict +from pathlib import Path + +from autoresearch.prefill.orchestration_state import ( + ARCHITECTURE_VERSION, + SCHEMA_VERSION, + STRATEGY_TOURNAMENT_MIGRATION_EVENT, + ProofState, + current_capability_manifest, + load_checkpoint, + save_checkpoint, +) +from autoresearch.prefill.strategy_tournament import ( + BranchEvidence, + BranchHistory, + branch_review_record, + review_branch, +) + + +MIGRATION_EVENT = STRATEGY_TOURNAMENT_MIGRATION_EVENT + + +def _digest(value: object) -> str: + return hashlib.sha256(json.dumps( + value, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +def atomic_snapshot( + snapshot_root: Path, + sources: tuple[Path, ...], + *, + supervisor_pid: int, + ledger_version: int, +) -> Path: + stamp = time.strftime("%Y%m%dT%H%M%SZ", time.gmtime()) + final = snapshot_root / f"strategy-tournament-v{ledger_version}-{stamp}" + temporary = snapshot_root / f".{final.name}.{os.getpid()}.tmp" + snapshot_root.mkdir(parents=True, exist_ok=True, mode=0o700) + temporary.mkdir(mode=0o700) + records = [] + try: + for index, source in enumerate(sources): + if not source.exists(): + continue + destination = temporary / f"{index:02d}-{source.name}" + if source.is_dir(): + shutil.copytree(source, destination) + digest = _digest(sorted( + str(path.relative_to(destination)) + + ":" + hashlib.sha256(path.read_bytes()).hexdigest() + for path in destination.rglob("*") if path.is_file() + )) + else: + shutil.copy2(source, destination) + digest = hashlib.sha256(destination.read_bytes()).hexdigest() + os.chmod(destination, 0o600) + records.append({ + "source": str(source), + "snapshot_name": destination.name, + "sha256": digest, + }) + manifest = { + "schema_version": 1, + "migration_event": MIGRATION_EVENT, + "ledger_version": ledger_version, + "old_supervisor_pid": supervisor_pid, + "created_at": time.time(), + "files": records, + } + manifest_path = temporary / "manifest.json" + manifest_path.write_text( + json.dumps(manifest, sort_keys=True, indent=2), + encoding="utf-8", + ) + os.chmod(manifest_path, 0o600) + descriptor = os.open(temporary, os.O_RDONLY) + try: + os.fsync(descriptor) + finally: + os.close(descriptor) + os.replace(temporary, final) + finally: + if temporary.exists(): + shutil.rmtree(temporary) + return final + + +def recorded_density_singularity_review(ledger: dict) -> dict[str, object]: + obligations = [ + item for item in ledger.get("obligations", ()) + if ( + "density" in str(item.get("statement", "")).lower() + or "singular" in str(item.get("statement", "")).lower() + ) + ] + evidence = [] + for item in obligations: + canonical = dict(item) + evidence.append(BranchEvidence( + evidence_id=str(item.get("obligation_id", "")), + event_type="RECORDED_LEDGER_OBLIGATION", + accepted_child_delta=int( + bool(item.get("decomposition_certificate_hash")) + and str(item.get("status", "")) != "REJECTED_DUPLICATE" + ), + lean_theorem_delta=int( + str(item.get("formal_status", "")).upper() == "PROVED" + ), + verified_counterexample_delta=int( + bool(item.get("quarantine_evidence_source")) + and float(item.get("quarantine_confidence", 0.0)) >= 0.8 + ), + semantic_failure_delta=int( + str(item.get("status", "")).upper() + in {"REJECTED", "REJECTED_DUPLICATE", "QUARANTINED"} + ), + reason_codes=tuple(filter(None, ( + str(item.get("status", "")), + str(item.get("formal_status", "")), + str(item.get("invalidation_kind", "")), + ))), + provenance_hash=_digest(canonical), + )) + history = BranchHistory( + branch_id="density-singularity", + plan_ids=[str(item.get("obligation_id", "")) for item in obligations], + evidence=evidence, + ) + review_branch(history, stagnation_threshold=4, failure_threshold=3) + return branch_review_record(history) + + +def migrate( + checkpoint_path: Path, + ledger_path: Path, + snapshot: Path, +) -> dict[str, object]: + checkpoint = load_checkpoint(checkpoint_path) + if checkpoint is None: + raise FileNotFoundError(checkpoint_path) + ledger = json.loads(ledger_path.read_text(encoding="utf-8")) + existing = [ + item for item in checkpoint.recovery_events + if ( + item.get("event_id") == MIGRATION_EVENT + and item.get("branch_review") + and item.get("snapshot") + ) + ] + ledger_version = int(ledger.get("version", 0)) + if ( + existing + and checkpoint.architecture_version == ARCHITECTURE_VERSION + and checkpoint.ledger_version == ledger_version + and set(checkpoint.validated_artifacts) <= {"definition_auditor"} + and checkpoint.migration_snapshot + ): + return existing[-1] + for role in tuple(checkpoint.validated_artifacts): + if role == "definition_auditor": + continue + reference = checkpoint.validated_artifacts.pop(role, None) + if reference is not None: + checkpoint.invalidated_artifacts[reference.sha256] = { + **asdict(reference), + "audit_only": True, + "read_only": True, + "reason_codes": ["LEGACY_PRE_CONTRACT_EXECUTION"], + "migration_event": MIGRATION_EVENT, + } + review = recorded_density_singularity_review(ledger) + review_path = checkpoint_path.with_name( + "density_singularity_branch_review.json", + ) + review_path.write_text( + json.dumps(review, sort_keys=True, indent=2), encoding="utf-8", + ) + os.chmod(review_path, 0o600) + checkpoint.architecture_version = ARCHITECTURE_VERSION + checkpoint.schema_version = SCHEMA_VERSION + for name, value in current_capability_manifest().items(): + setattr(checkpoint, name, value) + prior_state = checkpoint.state + checkpoint.state = ProofState.STRATEGY_TOURNAMENT.value + checkpoint.current_role = "strategy_tournament" + checkpoint.resume_origin = prior_state + checkpoint.ledger_version = ledger_version + checkpoint.strategy_reused = False + checkpoint.adapter_status = "" + checkpoint.blocked_reason = "" + checkpoint.migration_event = MIGRATION_EVENT + checkpoint.migration_snapshot = str(snapshot) + checkpoint.strategy_event_id = "" + checkpoint.strategy_event_type = "" + checkpoint.strategy_plan_ids = [] + checkpoint.feasible_strategy_plan_ids = [] + checkpoint.selected_strategy_plan_id = "" + checkpoint.research_contract_id = "" + checkpoint.research_contract_hash = "" + checkpoint.research_contract_rejection_codes = [] + checkpoint.typed_ir_hash = "" + checkpoint.lean_declaration_hash = "" + checkpoint.proposition_hash = "" + checkpoint.elaborated_theorem_id = "" + checkpoint.active_gate = "" + checkpoint.candidate_set_hash = "" + checkpoint.candidate_hashes = [] + checkpoint.candidate_count = 0 + checkpoint.ranking_hash = "" + checkpoint.ranked_candidate_ids = [] + checkpoint.selected_move_id = "" + checkpoint.evidence_gap_graph_hash = "" + checkpoint.proof_plan_hash = "" + checkpoint.proof_plan_id = "" + checkpoint.executable_plan_node_id = "" + checkpoint.plan_score_explanation = {} + checkpoint.branch_history["density-singularity"] = review + checkpoint.branches_killed = int(review["status"] == "QUARANTINED") + checkpoint.last_transition_reason = f"{MIGRATION_EVENT}:formal-branch-review" + event = { + "event_type": "OPERATOR_MIGRATION", + "event_id": MIGRATION_EVENT, + "ledger_version": ledger_version, + "target_state": checkpoint.state, + "snapshot": str(snapshot), + "branch_review": str(review_path), + "branch_review_hash": review["content_hash"], + "created_at": time.time(), + } + checkpoint.recovery_events.append(event) + save_checkpoint(checkpoint_path, checkpoint) + return event + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--home", type=Path, default=Path.home() / ".kakeya") + parser.add_argument("--supervisor-pid", type=int, required=True) + parser.add_argument("--snapshot", type=Path) + parser.add_argument( + "--candidate", type=Path, + default=Path.cwd() / "autoresearch/prefill/candidate.py", + ) + args = parser.parse_args() + home = args.home.expanduser() + checkpoint = home / "autoresearch/proof_orchestration.json" + ledger = home / "agent_gan_proof_ledger.json" + ledger_payload = json.loads(ledger.read_text(encoding="utf-8")) + sources = ( + checkpoint, + checkpoint.with_name("proof_orchestration.journal.jsonl"), + checkpoint.with_suffix(".artifacts"), + ledger, + home / "agent_gan_state.json", + home / "proof_live_status.json", + args.candidate.expanduser(), + home / "autoresearch" / "runs", + ) + snapshot = ( + args.snapshot.expanduser() if args.snapshot else atomic_snapshot( + home / "autoresearch/snapshots", + sources, + supervisor_pid=args.supervisor_pid, + ledger_version=int(ledger_payload.get("version", 0)), + ) + ) + event = migrate(checkpoint, ledger, snapshot) + print(json.dumps(event, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/inference_engine/bench/test_atomic_definition.py b/tests/inference_engine/bench/test_atomic_definition.py new file mode 100644 index 0000000..013ac9f --- /dev/null +++ b/tests/inference_engine/bench/test_atomic_definition.py @@ -0,0 +1,352 @@ +from __future__ import annotations + +import json +from pathlib import Path +from types import SimpleNamespace + +import pytest + +from autoresearch.prefill.atomic_definition import ( + ProgressVector, + TypedDefinitionCandidate, + classify_gap, + define_one_concept, + dependency_graph_for_audit, + first_dependency_closed_gap, + load_definition_registry, + record_semantic_iteration, + verified_progress_vector, + validate_typed_definition_candidate, +) +from autoresearch.prefill.orchestration_state import ( + OrchestrationCheckpoint, + ProofState, +) +from autoresearch.prefill.orchestration_state import ( + persist_validated_artifact, + save_checkpoint, +) +from scripts.migrate_atomic_define_one_concept_v1 import migrate + + +ROOT = Path(__file__).resolve().parents[3] + + +def _gap(definition_id, *, required_type_id="", symbols=()): + return { + "definition_id": definition_id, + "required_type_id": required_type_id, + "symbol_ids": list(symbols), + } + + +def _lean_ok(*_args, **_kwargs): + return SimpleNamespace(timed_out=False, returncode=0, output="") + + +def test_binder_restrictions_are_typed_entries_not_fake_definitions(): + epsilon = classify_gap( + _gap("DEF_EPSILON"), dependency_graph={}, theorem_card_ids=(), + ) + genus = classify_gap( + _gap("DEF_GENUS"), dependency_graph={}, theorem_card_ids=(), + ) + assert epsilon.classification == "TYPED_RESTRICTION" + assert "0 < epsilon" in epsilon.typed_entry + assert genus.classification == "TYPED_RESTRICTION" + assert "ℕ" in genus.typed_entry + assert not epsilon.candidates and not genus.candidates + + +def test_existing_mathlib_reference_resolves_without_redefinition( + tmp_path, monkeypatch, +): + monkeypatch.setattr( + "autoresearch.prefill.atomic_definition._run_lean", + pytest.fail, + ) + result = define_one_concept( + gap=_gap("DEF_SERIES_CONVERGENCE"), + definition_auditor_hash="a" * 64, + dependency_graph={"DEF_SERIES_CONVERGENCE": ()}, + registry_path=tmp_path / "registry.json", + project_root=ROOT, + theorem_card_ids=("locally_uniform_limit-card",), + current_environment_hash="e" * 64, + ) + assert result.status == "RESOLVED" + assert result.classification == "EXISTING_REFERENCE" + assert result.progress == ProgressVector(existing_definitions_resolved=1) + assert not load_definition_registry( + tmp_path / "registry.json", "e" * 64, + )["definitions"] + + +def test_one_concept_definition_changes_hash_once_and_restart_is_idempotent( + tmp_path, monkeypatch, +): + monkeypatch.setattr( + "autoresearch.prefill.atomic_definition._run_lean", _lean_ok, + ) + kwargs = dict( + gap=_gap("DEF_POLE_NEIGHBORHOOD"), + definition_auditor_hash="a" * 64, + dependency_graph={"DEF_POLE_NEIGHBORHOOD": ()}, + registry_path=tmp_path / "registry.json", + project_root=ROOT, + theorem_card_ids=(), + current_environment_hash="e" * 64, + ) + first = define_one_concept(**kwargs) + second = define_one_concept(**kwargs) + assert first.status == "RESOLVED" + assert first.progress.definitions_added == 1 + assert first.registry_hash_before != first.registry_hash_after + assert first.environment_hash_before != first.environment_hash_after + assert second.status == "IDEMPOTENT_REPLAY" + assert second.registry_hash_before == second.registry_hash_after + assert second.progress.total == 0 + + +def test_invalid_lean_definition_is_rejected_atomically(tmp_path, monkeypatch): + monkeypatch.setattr( + "autoresearch.prefill.atomic_definition._run_lean", + lambda *_args, **_kwargs: SimpleNamespace( + timed_out=False, returncode=1, output="type mismatch", + ), + ) + result = define_one_concept( + gap=_gap("DEF_POLE_NEIGHBORHOOD"), + definition_auditor_hash="a" * 64, + dependency_graph={"DEF_POLE_NEIGHBORHOOD": ()}, + registry_path=tmp_path / "registry.json", + project_root=ROOT, + theorem_card_ids=(), + current_environment_hash="e" * 64, + ) + assert result.status == "LEAN_DEFINITION_REJECTED" + assert result.progress.total == 0 + assert result.registry_hash_before == result.registry_hash_after + assert not (tmp_path / "registry.json").exists() + + +def test_unknown_gap_emits_mathematical_evidence_not_retry(tmp_path): + result = define_one_concept( + gap=_gap("DEF_UNKNOWN"), + definition_auditor_hash="a" * 64, + dependency_graph={"DEF_UNKNOWN": ()}, + registry_path=tmp_path / "registry.json", + project_root=ROOT, + theorem_card_ids=(), + current_environment_hash="e" * 64, + ) + assert result.status == "NO_TYPED_DEFINITION_CANDIDATE" + assert result.artifact_hash + assert result.progress.total == 0 + assert not (tmp_path / "registry.json").exists() + + +def test_dependency_order_is_derived_from_typed_evidence(): + missing = ( + _gap("DEF_EPSILON", symbols=("SYM_EPSILON",)), + _gap("DEF_GENUS", symbols=("SYM_GENUS_P",)), + _gap( + "DEF_POLE_NEIGHBORHOOD", + required_type_id="TYPE_PUNCTURED_OR_FULL_NEIGHBORHOOD", + symbols=("SYM_POLE_LOCATION",), + ), + _gap( + "DEF_FUNCTION_BINDING", + required_type_id="TYPE_CANONICAL_PRODUCT_BINDING", + symbols=("SYM_FUNCTION", "SYM_SEQUENCE"), + ), + _gap( + "DEF_SERIES_CONVERGENCE", + required_type_id="TYPE_CONVERGENCE_MODE", + symbols=("SYM_SEQUENCE",), + ), + _gap( + "DEF_GROWTH_ORDER", + required_type_id="TYPE_ENTIRE_FUNCTION_ORDER", + symbols=("SYM_FUNCTION", "SYM_GENUS_P"), + ), + _gap( + "DEF_SEQUENCE_DENSITY", + required_type_id="TYPE_SEQUENCE_DENSITY", + symbols=("SYM_SEQUENCE",), + ), + ) + graph = dependency_graph_for_audit(missing) + assert graph["DEF_FUNCTION_BINDING"] == ("DEF_POLE_NEIGHBORHOOD",) + assert graph["DEF_SERIES_CONVERGENCE"] == ("DEF_FUNCTION_BINDING",) + assert graph["DEF_GROWTH_ORDER"] == ("DEF_FUNCTION_BINDING",) + assert first_dependency_closed_gap( + missing, + dependency_graph=graph, + resolved_gap_ids=("DEF_EPSILON", "DEF_GENUS"), + )["definition_id"] == "DEF_POLE_NEIGHBORHOOD" + + +def test_true_theorem_and_registration_note_have_zero_progress(): + progress = verified_progress_vector( + lemmas_proved=1, + subgoals_closed=1, + lean_source="theorem fakeProgress : True := by trivial", + ) + assert progress.total == 0 + assert verified_progress_vector().total == 0 + + +def test_three_zero_delta_iterations_stagnate_and_forbid_fingerprint(): + checkpoint = OrchestrationCheckpoint( + target_obligation_id="ROOT", + definition_environment_hash="env", + ) + outcomes = [ + record_semantic_iteration( + checkpoint, + ProgressVector(), + move_class="DEFINE_ONE_CONCEPT:gap", + ) + for _ in range(3) + ] + assert outcomes == [False, False, True] + assert checkpoint.semantic_stagnation_count == 3 + assert checkpoint.progress_fingerprint in ( + checkpoint.forbidden_semantic_fingerprints + ) + assert checkpoint.stagnation_reason.startswith("three completed") + + +def test_infrastructure_failure_does_not_count_and_progress_resets(): + checkpoint = OrchestrationCheckpoint( + target_obligation_id="ROOT", + definition_environment_hash="env", + ) + record_semantic_iteration( + checkpoint, ProgressVector(), move_class="M", + infrastructure_failure=True, + ) + assert checkpoint.semantic_stagnation_count == 0 + + +def test_environment_change_can_replan_from_definition_resolution(): + checkpoint = OrchestrationCheckpoint( + state=ProofState.DEFINITION_RESOLUTION.value, + ) + checkpoint.transition( + ProofState.STRATEGY_TOURNAMENT, + "definition-environment-changed:replan", + ) + assert checkpoint.proof_state == ProofState.STRATEGY_TOURNAMENT + record_semantic_iteration(checkpoint, ProgressVector(), move_class="M") + record_semantic_iteration( + checkpoint, + ProgressVector(verified_counterexamples=1), + move_class="M", + ) + assert checkpoint.semantic_stagnation_count == 0 + + +def test_447_repeated_legacy_actions_cannot_execute_or_make_progress(): + checkpoint = OrchestrationCheckpoint( + target_obligation_id="ROOT", + definition_environment_hash="env", + ) + stopped_at = None + for iteration in range(447): + stagnant = record_semantic_iteration( + checkpoint, ProgressVector(), + move_class="REGISTER_DEFINITION_OBLIGATION", + ) + if stagnant: + stopped_at = iteration + 1 + break + assert stopped_at == 3 + + +def test_architecture_current_contains_no_executable_legacy_registration(): + production = ( + ROOT / "autoresearch/prefill/creative_decomposition.py" + ).read_text(encoding="utf-8") + assert "REGISTER_" + "DEFINITION_OBLIGATION" not in production + + +def test_candidate_selection_accepts_short_ids_only(tmp_path, monkeypatch): + monkeypatch.setattr( + "autoresearch.prefill.atomic_definition._run_lean", _lean_ok, + ) + with pytest.raises(ValueError, match="registered short ID"): + define_one_concept( + gap=_gap("DEF_POLE_NEIGHBORHOOD"), + definition_auditor_hash="a" * 64, + dependency_graph={"DEF_POLE_NEIGHBORHOOD": ()}, + registry_path=tmp_path / "registry.json", + project_root=ROOT, + theorem_card_ids=(), + current_environment_hash="e" * 64, + selected_candidate_id='{"lean":"def injected := True"}', + ) + + +def test_hidden_assumption_is_rejected_before_lean_runs(monkeypatch): + monkeypatch.setattr( + "autoresearch.prefill.atomic_definition._run_lean", + pytest.fail, + ) + candidate = TypedDefinitionCandidate( + "A", + "DEF_BAD", + "bad", + "axiom hidden : Prop\ndef bad : Prop := hidden", + (), + ("Prop",), + ) + assert validate_typed_definition_candidate( + candidate, project_root=ROOT, + ) == (False, "HIDDEN_ASSUMPTION_OR_FORBIDDEN_COMMAND") + + +def test_migration_preserves_audit_and_selects_first_real_gap(tmp_path): + home = tmp_path / "home" + autoresearch = home / "autoresearch" + autoresearch.mkdir(parents=True) + checkpoint_path = autoresearch / "proof_orchestration.json" + checkpoint = OrchestrationCheckpoint( + state="DECOMPOSER", + selected_move_id="REGISTER_DEFINITION_OBLIGATION", + typed_ir_hash="old", + proposition_hash="old-true", + ) + persist_validated_artifact( + checkpoint_path, + checkpoint, + role="definition_auditor", + payload={"missing_definitions": [ + _gap("DEF_EPSILON", symbols=("SYM_EPSILON",)), + _gap("DEF_GENUS", symbols=("SYM_GENUS_P",)), + _gap( + "DEF_POLE_NEIGHBORHOOD", + required_type_id="TYPE_PUNCTURED_OR_FULL_NEIGHBORHOOD", + symbols=("SYM_POLE_LOCATION",), + ), + ]}, + dependencies=[], + source_run_id="audit", + ) + save_checkpoint(checkpoint_path, checkpoint) + (home / "agent_gan_proof_ledger.json").write_text( + json.dumps({"version": 92}), encoding="utf-8", + ) + result = migrate( + home=home, + project_root=ROOT, + supervisor_pid=999999, + snapshot=tmp_path / "snapshot", + ) + assert result["current_gap"] == "DEF_POLE_NEIGHBORHOOD" + raw = json.loads(checkpoint_path.read_text(encoding="utf-8")) + assert raw["migration_event"] == "atomic_define_one_concept_progress_v1" + assert raw["selected_move_id"] == "DEFINE_ONE_CONCEPT" + assert raw["typed_ir_hash"] == "" + assert "definition_auditor" in raw["validated_artifacts"] diff --git a/tests/inference_engine/bench/test_creative_decomposition.py b/tests/inference_engine/bench/test_creative_decomposition.py new file mode 100644 index 0000000..28e51a4 --- /dev/null +++ b/tests/inference_engine/bench/test_creative_decomposition.py @@ -0,0 +1,501 @@ +from dataclasses import replace +from pathlib import Path + +import pytest + +from autoresearch.prefill.creative_decomposition import ( + MIGRATION_EVENT, + MOVE_REGISTRY, + assert_no_scratchpad_content, + build_candidate_set, + persist_private_scratchpad, + rank_candidates, + rank_short_choice, + synthesis_manifest, + synthesis_trigger, +) +from autoresearch.prefill.evidence_planner import ( + EdgeKind, + GraphEdge, + GraphNode, + NodeKind, + ProofPlan, + ProofPlanNode, + VerificationStatus, + build_evidence_gap_graph, + first_executable_node, + generate_proof_plans, + host_evidence_context, + replan_after_failure, + validate_proof_plan, +) +from autoresearch.prefill.host_compiler import run_host_gates +from autoresearch.prefill.lean_gate import validate_lean_signature +from autoresearch.prefill.math_ir import parse_math_ir, validate_math_ir +from autoresearch.prefill.orchestration_state import ( + OrchestrationCheckpoint, + ProofState, +) +from autoresearch.prefill.theorem_cards import ( + build_theorem_card_index, + search_theorem_cards, + validate_theorem_cards, +) +from autoresearch.prefill.typed_transport import ( + AdapterError, + decode_role_fields, + transport_prompt, +) +from scripts.migrate_creative_decomposition_v3 import ( + MIGRATION_EVENT as ARCHITECTURE_MIGRATION_EVENT, + atomic_snapshot, + migrate_checkpoint, +) + + +ROOT = Path(__file__).resolve().parents[3] + + +def _candidate_set(**kwargs): + cards = build_theorem_card_index(ROOT) + preconditions = { + item + for move in MOVE_REGISTRY.values() + for item in move.precondition_ids + if item != "registered_definition_gap" + } + hypotheses = { + item for card in cards for item in card.required_hypotheses + } + return build_candidate_set( + target_ref="claim:" + "a" * 64, + viewpoint="local_holomorphicity", + dependency_ids=("d" * 64,), + theorem_cards=cards, + satisfied_precondition_ids=preconditions, + satisfied_theorem_hypothesis_ids=hypotheses, + available_dependency_artifact_ids=("d" * 64,), + required_dependency_artifact_ids=("d" * 64,), + **kwargs, + ) + + +def test_versioned_move_registry_has_required_scoped_strict_moves(): + required = { + "CASE_SPLIT", "RESTRICT_DOMAIN", "REMOVE_IRRELEVANT_ASSUMPTION", + "HOLOMORPHIC_EXTENSION", "SINGULARITY_CONTRADICTION", + } + assert required <= MOVE_REGISTRY.keys() + for move_id in required: + move = MOVE_REGISTRY[move_id] + assert move.version == 3 + assert move.operand_kinds + assert move.precondition_ids + assert move.metric.strictly_simpler + assert len(move.content_hash) == 64 + + +def test_host_generates_k_distinct_candidates_and_rejects_ancestor(): + first = _candidate_set() + assert len(first.candidates) >= 3 + assert len({item.novelty_hash for item in first.candidates}) == len( + first.candidates, + ) + ancestor = next( + item for item in first.candidates + if item.move.move_id == "SINGULARITY_CONTRADICTION" + ) + second = _candidate_set(ancestor_hashes=(ancestor.typed_ir_hash,)) + assert ( + ancestor.choice_id, "ANCESTOR_EQUIVALENT" + ) in second.rejected + assert all( + item.typed_ir_hash != ancestor.typed_ir_hash + for item in second.candidates + ) + + +def test_local_holomorphicity_candidate_is_honest_special_case_and_elaborates(tmp_path): + candidates = _candidate_set() + candidate = next( + item for item in candidates.candidates + if item.move.move_id == "SINGULARITY_CONTRADICTION" + ) + assert candidate.move.result_status == "SPECIAL_CASE_LEMMA" + assert candidate.move.requires_parent_case_split + assert "locally_uniform_limit_holomorphic" in candidate.theorem_card_ids + validated = validate_math_ir(parse_math_ir(candidate.typed_payload)) + assert validated.content_hash == candidate.typed_ir_hash + assert len(validated.math_ir.premises) == 7 + result = run_host_gates( + candidate.typed_payload, + project_root=ROOT, + cache_dir=tmp_path / "gates", + lean_validator=validate_lean_signature, + ) + assert result.ok + assert result.compilation is not None + assert "polesOutsideDisk" in result.compilation.declaration_source + assert "localUniformConvergenceOnDisk" in result.compilation.declaration_source + assert "agreesWithSimplePoleOnPuncturedDisk" in ( + result.compilation.declaration_source + ) + + +def test_private_scratchpad_is_unparsed_and_cannot_cross_artifact_gate(tmp_path): + private = r"""Untrusted: use $\frac m{s-s_0}$; {"not":"transport"}; theorem X := by""" + ref = persist_private_scratchpad( + tmp_path / "scratchpads", + role="decomposer_scratchpad", + transcript=private, + token_count=19, + ) + assert ref.audit_only and not ref.authoritative and not ref.public + assert ref.parse_contract == "NEVER_PARSE" + safe = {"scratchpad_ref": ref.sha256, "selected_candidate_id": "C1"} + assert_no_scratchpad_content(safe, ref) + with pytest.raises(ValueError, match="SCRATCHPAD_TEXT"): + assert_no_scratchpad_content({"payload": private}, ref) + + +def test_synthesis_trigger_ranking_and_counterexample_advisory(tmp_path): + trigger = synthesis_trigger( + novel_rejections=3, + repeated_no_move=0, + evidence_roles=("critic", "definition_auditor"), + ) + assert trigger.invoke and trigger.reason == "NOVEL_SEMANTIC_REJECTIONS" + candidates = _candidate_set() + ranking = rank_candidates(candidates) + selected = candidates.resolve(ranking.selected_candidate_id) + assert selected.move.move_id == "SINGULARITY_CONTRADICTION" + ref = persist_private_scratchpad( + tmp_path, role="synthesis_scratchpad", + transcript="private comparison", token_count=2, + ) + manifest = synthesis_manifest( + evidence_hashes={"counterexample_worker": "c" * 64}, + rejected_reason_codes=("NOT_STRICTLY_SIMPLER",), + theorem_card_ids=("locally_uniform_limit_holomorphic",), + scratchpad_ref=ref, + ranking=ranking, + short_choice_map_hash=candidates.short_choice_map_hash, + selected_choice_code="I", + counterexample_verified=False, + ) + assert manifest["counterexample_premise_policy"] == "ADVISORY_ONLY" + assert "private comparison" not in str(manifest) + + +def test_synthesis_transport_uses_only_scoped_short_choice_codes(): + candidates = _candidate_set() + assert len(candidates.candidates) == 9 + assert candidates.short_choice_codes == tuple("ABCDEFGHI") + assert candidates.short_choice_map_hash == _candidate_set().short_choice_map_hash + registered = {"choice_code": candidates.short_choice_codes} + decoded = decode_role_fields( + "choice_code I;\nreason_code DIRECT_LOCAL_CONTRADICTION;\nEND;", + "synthesis", + registered_choices=registered, + ) + ranking = rank_short_choice( + candidates, + choice_code=str(decoded.values["choice_code"]), + reason_code=str(decoded.values["reason_code"]), + candidate_set_hash=candidates.content_hash, + short_choice_map_hash=candidates.short_choice_map_hash, + ) + assert candidates.resolve(ranking.selected_candidate_id).move.move_id == ( + "SINGULARITY_CONTRADICTION" + ) + assert candidates.resolve_short_code( + "I", + candidate_set_hash=candidates.content_hash, + short_choice_map_hash=candidates.short_choice_map_hash, + ).candidate_hash == ( + candidates.short_choice_map["I"].candidate_hash + ) + + invalid_codes = ( + "C1_DENSITY_LOWER_BOUND", + "C1_DENSITY_LOWER_BOUN", + "a", + "A ", + "AA", + "J", + ) + for code in invalid_codes: + with pytest.raises(AdapterError): + decode_role_fields( + f"choice_code {code};\nreason_code LOWEST_COMPLEXITY;\nEND;", + "synthesis", + registered_choices=registered, + ) + with pytest.raises(AdapterError, match="DUPLICATE_FIELD"): + decode_role_fields( + "choice_code A;\nchoice_code B;\n" + "reason_code LOWEST_COMPLEXITY;\nEND;", + "synthesis", + registered_choices=registered, + ) + + prompt = transport_prompt("synthesis", registered_choices=registered) + assert "choice_code" in prompt + assert "C1_DENSITY_LOWER_BOUND" not in prompt + assert "candidate_id" not in prompt + assert "ranked_candidate_id" not in prompt + assert "selected_candidate_id" not in prompt + + +def test_semantic_stagnation_changes_decomposition_without_global_strategy(): + checkpoint = OrchestrationCheckpoint( + state=ProofState.DECOMPOSITION_STAGNATED.value, + migration_event=MIGRATION_EVENT, + ) + checkpoint.transition( + ProofState.SYNTHESIS, "novel-rejections-threshold", strategy_reused=True, + ) + checkpoint.transition( + ProofState.DECOMPOSER, "change-case-partition", strategy_reused=True, + ) + assert checkpoint.proof_state == ProofState.DECOMPOSER + assert checkpoint.strategy_reused + + +def test_actual_mathlib_cards_search_elaborate_and_stale_hash_fails(): + cards = build_theorem_card_index(ROOT) + names = {card.theorem_name for card in cards} + assert { + "TendstoLocallyUniformlyOn.differentiableOn", + "Complex.differentiableOn_tsum_of_summable_norm", + "Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt", + "Complex.differentiableOn_update_limUnder_of_bddAbove", + "AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq", + } <= names + retrieved = search_theorem_cards( + cards, ("locally_uniform_limit", "removable_singularity"), + ) + assert retrieved + validate_theorem_cards(retrieved, project_root=ROOT) + with pytest.raises(ValueError, match="STALE_THEOREM_CARD_SOURCE"): + validate_theorem_cards( + (replace(retrieved[0], source_hash="0" * 64),), + project_root=ROOT, + ) + + +def test_atomic_v87_snapshot_and_migration_follows_dependencies(tmp_path): + checkpoint_path = tmp_path / "proof_orchestration.json" + checkpoint = OrchestrationCheckpoint( + state=ProofState.DECOMPOSER.value, + ledger_version=87, + strategy_reused=True, + ) + from autoresearch.prefill.orchestration_state import save_checkpoint + save_checkpoint(checkpoint_path, checkpoint) + ledger = tmp_path / "ledger.json" + ledger.write_text('{"version":87}', encoding="utf-8") + snapshot = atomic_snapshot( + snapshot_root=tmp_path / "snapshots", + files=(checkpoint_path, ledger), + old_supervisor_pid=45556, + ) + assert snapshot.is_dir() + manifest = __import__("json").loads( + (snapshot / "manifest.json").read_text(encoding="utf-8"), + ) + assert manifest["old_supervisor_pid"] == 45556 + assert len(manifest["files"]) == 2 + migrate_checkpoint(checkpoint_path, snapshot) + from autoresearch.prefill.orchestration_state import load_checkpoint + migrated = load_checkpoint(checkpoint_path) + assert migrated.proof_state == ProofState.DEFINITION_AUDITOR + assert migrated.migration_event == ARCHITECTURE_MIGRATION_EVENT + assert migrated.migration_snapshot == str(snapshot) + assert migrated.strategy_reused + + +def _missing_definition_artifact(*definition_ids): + return { + "definitions": [], + "missing_definitions": [ + {"definition_id": item, "obligation_label": f"D{index + 1}"} + for index, item in enumerate(definition_ids) + ], + } + + +def test_production_regression_density_ineligible_reason_checked_and_codes_remap(): + cards = build_theorem_card_index(ROOT) + dependency = "d" * 64 + unfiltered = build_candidate_set( + target_ref="claim:" + "a" * 64, + viewpoint="regression", + dependency_ids=(dependency,), + theorem_cards=cards, + satisfied_precondition_ids={ + item + for move in MOVE_REGISTRY.values() + for item in move.precondition_ids + if item != "registered_definition_gap" + }, + satisfied_theorem_hypothesis_ids={ + item for card in cards for item in card.required_hypotheses + }, + available_dependency_artifact_ids=(dependency,), + required_dependency_artifact_ids=(dependency,), + ) + density = next( + item for item in unfiltered.candidates + if item.move.move_id == "DENSITY_LOWER_BOUND" + ) + density_code = next( + code for code, item in unfiltered.short_choice_map.items() + if item == density + ) + with pytest.raises(ValueError, match="INVALID_RANK_REASON_METRIC"): + rank_short_choice( + unfiltered, + choice_code=density_code, + reason_code="LOWEST_COMPLEXITY", + candidate_set_hash=unfiltered.content_hash, + short_choice_map_hash=unfiltered.short_choice_map_hash, + ) + + filtered = build_candidate_set( + target_ref="claim:" + "a" * 64, + viewpoint="regression", + dependency_ids=(dependency,), + theorem_cards=cards, + satisfied_precondition_ids=("registered_definition_gap",), + available_dependency_artifact_ids=(dependency,), + required_dependency_artifact_ids=(dependency,), + ) + assert filtered.candidates == () + assert any( + move_id == "DENSITY_LOWER_BOUND" + and "UNMET_PRECONDITION" in reasons + for move_id, reasons in filtered.ineligible + ) + assert filtered.short_choice_map == {} + + +def test_evidence_planner_provenance_advisory_exclusion_and_multiple_plans(): + artifact_hash = "a" * 64 + artifact = _missing_definition_artifact( + "DEF_SEQUENCE_DENSITY", "DEF_CRITICAL_DENSITY", + ) + context = host_evidence_context( + {"definition_auditor": artifact}, + artifact_hashes={"definition_auditor": artifact_hash}, + ) + candidates = build_candidate_set( + target_ref="claim:" + "b" * 64, + viewpoint="recorded_gaps", + satisfied_precondition_ids=context.satisfied_precondition_ids, + ) + graph = build_evidence_gap_graph( + artifacts={"definition_auditor": artifact}, + artifact_hashes={"definition_auditor": artifact_hash}, + advisory_artifacts={ + "c" * 64: {"role": "counterexample_worker", "verified": False}, + }, + theorem_cards=(), + candidate_set=candidates, + ) + gaps = [node for node in graph.nodes if node.kind == NodeKind.GAP.value] + assert any(artifact_hash in node.provenance_refs for node in gaps) + advisory_ids = { + node.node_id for node in graph.nodes + if node.verification_status == VerificationStatus.ADVISORY.value + } + assert advisory_ids + assert not any( + edge.kind == EdgeKind.SUPPORTS.value and edge.source_id in advisory_ids + for edge in graph.edges + ) + plans = generate_proof_plans( + graph, unresolved_gap_ids=context.unresolved_gap_ids, + ) + # Definition gaps are completed by Host DEFINE_ONE_CONCEPT before planning. + assert plans == () + assert plans == generate_proof_plans( + graph, unresolved_gap_ids=context.unresolved_gap_ids, + ) + + +def test_plan_dependency_cycle_case_and_restart_fail_closed(): + artifact = _missing_definition_artifact("DEF_A", "DEF_B") + context = host_evidence_context( + {"definition_auditor": artifact}, + artifact_hashes={"definition_auditor": "a" * 64}, + ) + candidates = build_candidate_set( + target_ref="claim:" + "c" * 64, + viewpoint="gaps", + satisfied_precondition_ids=context.satisfied_precondition_ids, + ) + graph = build_evidence_gap_graph( + artifacts={"definition_auditor": artifact}, + artifact_hashes={"definition_auditor": "a" * 64}, + advisory_artifacts={}, + theorem_cards=(), + candidate_set=candidates, + ) + plans = generate_proof_plans( + graph, unresolved_gap_ids=context.unresolved_gap_ids, + ) + assert plans == () + + +def test_theorem_hypothesis_gate_replan_and_generic_scoring_static_guard(): + cards = build_theorem_card_index(ROOT) + preconditions = { + item + for move in MOVE_REGISTRY.values() + for item in move.precondition_ids + if item != "registered_definition_gap" + } + gated = build_candidate_set( + target_ref="claim:" + "d" * 64, + viewpoint="theorem_gate", + theorem_cards=cards, + satisfied_precondition_ids=preconditions, + ) + assert any( + "UNMET_THEOREM_HYPOTHESIS" in reasons + for _move_id, reasons in gated.ineligible + ) + + artifact = _missing_definition_artifact("DEF_A", "DEF_B") + context = host_evidence_context( + {"definition_auditor": artifact}, + artifact_hashes={"definition_auditor": "a" * 64}, + ) + candidates = build_candidate_set( + target_ref="claim:" + "e" * 64, + viewpoint="replan", + satisfied_precondition_ids=context.satisfied_precondition_ids, + ) + graph = build_evidence_gap_graph( + artifacts={"definition_auditor": artifact}, + artifact_hashes={"definition_auditor": "a" * 64}, + advisory_artifacts={}, + theorem_cards=(), + candidate_set=candidates, + ) + plans = generate_proof_plans( + graph, unresolved_gap_ids=context.unresolved_gap_ids, + ) + assert plans == () + + import inspect + from autoresearch.prefill import evidence_planner + scoring_source = inspect.getsource(evidence_planner.generate_proof_plans) + for forbidden in ( + "DENSITY_LOWER_BOUND", + "LOCAL_CONVERGENCE_OBLIGATION", + "HOLOMORPHIC_EXTENSION", + "SINGULARITY_CONTRADICTION", + ): + assert forbidden not in scoring_source diff --git a/tests/inference_engine/bench/test_definition_resolution.py b/tests/inference_engine/bench/test_definition_resolution.py new file mode 100644 index 0000000..f11ad90 --- /dev/null +++ b/tests/inference_engine/bench/test_definition_resolution.py @@ -0,0 +1,231 @@ +from __future__ import annotations + +import json +from pathlib import Path +from types import SimpleNamespace + +import pytest + +from autoresearch.prefill.definition_resolution import ( + DefinitionSourceRegistry, + PropertyStatus, + build_definition_query, + default_source_registry, + load_resolution_store, + migrate_legacy_registry, + normalize_candidates, + resolve_one_concept, +) + + +ROOT = Path(__file__).resolve().parents[3] + + +def query(**overrides): + gap = { + "definition_id": "DEF_TEST", + "domain": "ℕ", + "codomain": "ℕ", + "use_sites": ["u2", "u1"], + "required_properties": ["monotone"], + "hard_properties": ["monotone"], + } + gap.update(overrides.pop("gap", {})) + return build_definition_query( + gap, parent_hash=overrides.pop("parent_hash", "p"), + typed_ir_hash=overrides.pop("typed_ir_hash", "ir"), + auditor_hash="audit", critic_evidence_hashes=(), + counterexample_evidence_hashes=(), theorem_dependencies=(), + environment_hash=overrides.pop("environment_hash", "env"), + prior_failure_hashes=overrides.pop("prior_failure_hashes", ()), + ) + + +def registry(*raw): + result = DefinitionSourceRegistry() + + def adapter(definition_query, _root, _context): + from autoresearch.prefill.definition_resolution import SourceProvenance + return list(raw), SourceProvenance( + "fixture", "FIXTURE", "QUERIED", "test", + definition_query.environment_hash, "evidence", + ) + + result.register("fixture", adapter) + return result + + +def candidate(name="testDef", expression="fun n => n", branch=""): + return { + "source_id": "fixture", + "declaration_name": name, + "domain": "ℕ", + "codomain": "ℕ → ℕ", + "typed_expression": expression, + "branch_id": branch, + "claimed_properties": ["monotone"], + } + + +@pytest.fixture +def lean_ok(monkeypatch): + monkeypatch.setattr( + "autoresearch.prefill.definition_resolution._run_lean", + lambda *_args, **_kwargs: SimpleNamespace( + timed_out=False, returncode=0, output="", + ), + ) + + +def evidence(status="VERIFIED"): + return {"monotone": { + "status": status, + "evidence_kind": "LEAN_THEOREM_CARD", + "evidence_ref": "sha256:proof", + }} + + +def test_query_fingerprint_is_semantic_and_changes_with_evidence(): + first = query() + reordered = query(gap={ + "definition_id": "DEF_TEST", "domain": "ℕ", "codomain": "ℕ", + "use_sites": ["u1", "u2"], "required_properties": ["monotone"], + "hard_properties": ["monotone"], + }) + assert first.fingerprint == reordered.fingerprint + assert first.fingerprint != query(parent_hash="changed").fingerprint + assert first.fingerprint != query(environment_hash="changed").fingerprint + + +def test_unavailable_oproofs_is_reported_honestly(monkeypatch): + monkeypatch.delenv("KAKEYA_OPROOFS_ROOT", raising=False) + _, statuses = default_source_registry().retrieve(query(), ROOT, {}) + status = {item.source_id: item.status for item in statuses} + assert status["oproofs"] == "UNAVAILABLE" + + +def test_candidate_normalization_requires_provenance(): + with pytest.raises(ValueError, match="provenance"): + normalize_candidates(query(), [candidate()], ()) + + +def test_success_compiles_verifies_and_commits(tmp_path, lean_ok): + result = resolve_one_concept( + query=query(), store_path=tmp_path / "resolution.json", + project_root=ROOT, source_registry=registry(candidate()), + property_evidence=evidence(), + ) + assert result.status == "COMMITTED" + assert result.committed_candidate_hash + assert result.environment_hash_before != result.environment_hash_after + store = load_resolution_store(tmp_path / "resolution.json", "env") + assert store["commits"]["DEF_TEST"]["candidate_hash"] == result.committed_candidate_hash + + +def test_unknown_hard_property_cannot_commit(tmp_path, lean_ok): + result = resolve_one_concept( + query=query(), store_path=tmp_path / "resolution.json", + project_root=ROOT, source_registry=registry(candidate()), + property_evidence={}, + ) + assert result.status == "INTERFACE_REQUIRED" + assert result.exhaustion_hash and result.interface_hash + statuses = next(iter(result.property_statuses.values())) + assert statuses["monotone"] == PropertyStatus.UNKNOWN.value + + +def test_ontology_type_id_does_not_fake_a_viable_interface(tmp_path, lean_ok): + abstract = query(gap={ + "definition_id": "DEF_SEQUENCE_DENSITY", + "domain": "", + "codomain": "", + "required_type_id": "TYPE_SEQUENCE_DENSITY", + "symbol_ids": ["SYM_SEQUENCE", "SYM_SEQUENCE_DENSITY"], + }) + result = resolve_one_concept( + query=abstract, store_path=tmp_path / "resolution.json", + project_root=ROOT, source_registry=registry(), + ) + assert result.status == "PARENT_STATEMENT_UNDERSPECIFIED" + assert result.interface_hash and result.exhaustion_hash + + +def test_multiple_survivors_branch_without_silent_choice(tmp_path, lean_ok): + result = resolve_one_concept( + query=query(), store_path=tmp_path / "resolution.json", + project_root=ROOT, + source_registry=registry( + candidate("definitionOne", "fun n => n", "one"), + candidate("definitionTwo", "fun n => n + 1", "two"), + ), + property_evidence=evidence(), + ) + assert result.status == "PARENT_STATEMENT_UNDERSPECIFIED" + assert len(result.branch_hashes) == 2 + assert not result.committed_candidate_hash + store = load_resolution_store(tmp_path / "resolution.json", "env") + for branch_hash in result.branch_hashes: + assert store["branches"][branch_hash]["equivalence_obligation_hash"] + + +def test_identical_exhausted_query_cannot_rerun(tmp_path, lean_ok): + path = tmp_path / "resolution.json" + first = resolve_one_concept( + query=query(), store_path=path, project_root=ROOT, + source_registry=registry(), property_evidence={}, + ) + second = resolve_one_concept( + query=query(), store_path=path, project_root=ROOT, + source_registry=registry(candidate()), property_evidence=evidence(), + ) + assert first.status == "INTERFACE_REQUIRED" + assert second.status == "IDENTICAL_QUERY_EXHAUSTED" + assert second.store_hash_before == second.store_hash_after + + +def test_model_can_rank_short_ids_only(tmp_path, lean_ok): + with pytest.raises(ValueError, match="short candidate IDs"): + resolve_one_concept( + query=query(), store_path=tmp_path / "resolution.json", + project_root=ROOT, source_registry=registry(candidate()), + property_evidence=evidence(), + ranked_short_ids=('{"lean":"axiom injected : False"}',), + ) + + +def test_hidden_assumption_is_rejected_before_lean(tmp_path, monkeypatch): + monkeypatch.setattr( + "autoresearch.prefill.definition_resolution._run_lean", pytest.fail, + ) + bad = candidate(expression="axiom hidden : False") + result = resolve_one_concept( + query=query(), store_path=tmp_path / "resolution.json", + project_root=ROOT, source_registry=registry(bad), + property_evidence=evidence(), + ) + assert result.status == "INTERFACE_REQUIRED" + + +def test_legacy_definitions_are_audit_only_with_property_obligations(): + store = migrate_legacy_registry({ + "definitions": { + "oldNeighborhood": { + "gap_id": "DEF_POLE_NEIGHBORHOOD", + "lean_source": "def oldNeighborhood := 1", + }, + }, + }, base_environment_hash="env") + record = next(iter(store["historical_audit"].values())) + assert record["audit_only"] is True + assert record["semantic_validation"] == "PENDING" + assert record["property_obligations"] == [ + "full_vs_punctured_neighborhood", + ] + assert not store["commits"] + + +def test_static_active_architecture_has_no_legacy_registry_or_reframe_loop(): + source = (ROOT / "autoresearch/prefill/architecture_v7.py").read_text() + assert "definition_" + "registry.json" not in source + assert "NO_TYPED_" + "DEFINITION_CANDIDATE" not in source + assert "ProofState." + "REFRAME" not in source diff --git a/tests/inference_engine/bench/test_strategy_tournament_stepwise.py b/tests/inference_engine/bench/test_strategy_tournament_stepwise.py new file mode 100644 index 0000000..30066a0 --- /dev/null +++ b/tests/inference_engine/bench/test_strategy_tournament_stepwise.py @@ -0,0 +1,535 @@ +import json +import shutil +from dataclasses import replace +from pathlib import Path + +import pytest + +from autoresearch.prefill.architecture_v7 import run_architecture_v7_entry +from autoresearch.prefill.research_contract import gate_research_contract +from autoresearch.prefill.orchestration_state import ( + OrchestrationCheckpoint, + ProofState, + persist_validated_artifact, + save_checkpoint, +) +from autoresearch.prefill.stepwise_proof import ( + ActionSelection, + FeedbackCode, + LeanExecutionContext, + LeanStepResult, + ProofGoal, + attempt_step, + beam_rank, + enumerate_applicable_actions, + load_search_state, + lean_step_executor, + new_search_state, + persist_search_state, + render_lean_ast, +) +from autoresearch.prefill.strategy_tournament import ( + BranchEvidence, + BranchHistory, + CriticReason, + FeasibilityReason, + PlanClass, + PlanExecutionStatus, + StrategyEvent, + build_host_plans, + evaluate_feasibility, + review_branch, + run_tournament, + strategy_event_due, +) +from scripts.migrate_strategy_tournament_v1 import migrate +from scripts.migrate_research_contract_preproof_v2 import ( + MIGRATION_EVENT as PREPROOF_MIGRATION_EVENT, + migrate as migrate_preproof, +) + + +ENV = "e" * 64 + + +def _plans(): + return build_host_plans( + target_ref="target:root", + parent_obligation_ref="ROOT", + parent_complexity=10, + environment_hash=ENV, + registered_definition_ids=("D1",), + theorem_card_ids=("T1", "T2"), + dependency_ids=("E1",), + evidence_refs=("E1",), + elaborated_theorem_id="hostTheorem", + proposition_hash="p" * 64, + ) + + +def _decisions(plans=None): + return evaluate_feasibility( + plans or _plans(), + registered_definition_ids=("D1",), + resolved_dependency_ids=("E1",), + verified_theorem_card_ids=("T1", "T2"), + allowed_assumption_ids=(), + ) + + +def _contract(): + plan = _plans()[0] + decision = gate_research_contract( + plan, + elaborated_theorem_id="hostTheorem", + elaborated_proposition_hash="p" * 64, + proof_obligation_id="O1", + registered_definition_ids=("D1",), + resolved_dependency_ids=("E1",), + verified_theorem_card_ids=("T1", "T2"), + allowed_assumption_ids=(), + environment_hash=ENV, + expected_plan_hash=plan.content_hash, + ) + assert decision.accepted + return decision.contract + + +def test_four_independent_plan_classes_and_event_only_trigger(): + plans = _plans() + assert {item.plan_class for item in plans} == { + item.value for item in PlanClass + } + assert len({item.source_move_id for item in plans}) == 4 + assert all( + item.execution_status == PlanExecutionStatus.EXECUTABLE.value + for item in plans + ) + assert not strategy_event_due( + None, rounds_without_verified_progress=2, stagnation_threshold=3, + ) + assert strategy_event_due( + StrategyEvent.TARGET_CHANGE, + rounds_without_verified_progress=0, + stagnation_threshold=3, + ) + + +def test_hard_feasibility_duplicate_no_go_and_critic_cannot_override(): + plans = _plans() + duplicate = replace( + plans[0], plan_id="P5", content_hash="f" * 64, + ) + decisions = evaluate_feasibility( + (*plans, duplicate), + registered_definition_ids=("D1",), + resolved_dependency_ids=("E1",), + verified_theorem_card_ids=("T1", "T2"), + allowed_assumption_ids=(), + no_go_hashes=(plans[1].content_hash,), + ) + by_id = {item.plan_id: item for item in decisions} + assert FeasibilityReason.NO_GO_ROUTE.value in by_id["P2"].reason_codes + assert FeasibilityReason.DUPLICATE_ROUTE.value in by_id["P5"].reason_codes + tournament = run_tournament( + event_id="event:1", + event_type=StrategyEvent.INITIAL_BRANCH, + plans=plans, + decisions=decisions[:4], + critic_ranked_plan_ids=("P2", "P1"), + critic_reason_codes=(CriticReason.LOWEST_RISK,), + ) + assert "P2" not in tournament.critic_ranked_plan_ids + assert tournament.selected_plan_id in tournament.pareto_plan_ids + + +def test_plan_contract_criteria_and_strict_reduction_rejections(): + plan = _plans()[0] + rejected = gate_research_contract( + replace(plan, target_complexity=plan.parent_complexity), + elaborated_theorem_id="", + elaborated_proposition_hash="", + proof_obligation_id="", + registered_definition_ids=(), + resolved_dependency_ids=(), + verified_theorem_card_ids=(), + allowed_assumption_ids=(), + environment_hash=ENV, + expected_plan_hash=plan.content_hash, + ) + assert not rejected.accepted + assert "UNELABORATED_TARGET" in rejected.reason_codes + assert "NON_REDUCING_TARGET" in rejected.reason_codes + assert rejected.route_state == "DECOMPOSER" + + +def test_production_p4_fixture_keeps_eight_unresolved_definitions_and_is_planning_only(): + missing = tuple(f"DEF_{index}" for index in range(8)) + gaps = tuple(f"gap:definition:{item}" for item in missing) + plans = build_host_plans( + target_ref="production:P4", + parent_obligation_ref="ROOT", + parent_complexity=59, + environment_hash=ENV, + registered_definition_ids=(), + unresolved_definition_ids=missing, + definition_gap_ids=gaps, + definition_auditor_hash="a" * 64, + theorem_card_ids=("T1",), + dependency_ids=("a" * 64,), + evidence_refs=("a" * 64,), + ) + p4 = plans[3] + assert p4.plan_id == "P4" + assert p4.required_definition_ids == missing + assert p4.unresolved_definition_ids == missing + assert p4.definition_gap_ids == gaps + assert p4.definition_auditor_hash == "a" * 64 + assert p4.execution_status == PlanExecutionStatus.PLANNING_ONLY.value + assert not p4.proposition_transformation_ref + decisions = _decisions(plans) + assert FeasibilityReason.PLANNING_ONLY.value in decisions[3].reason_codes + assert FeasibilityReason.UNMET_DEFINITION.value in decisions[3].reason_codes + + +def test_full_preproof_transition_sequence_and_valid_contract(tmp_path, monkeypatch): + checkpoint_path = tmp_path / "proof_orchestration.json" + checkpoint = OrchestrationCheckpoint( + state=ProofState.DECOMPOSER.value, + current_role="decomposer", + target_obligation_id="replacement", + ) + persist_validated_artifact( + checkpoint_path, + checkpoint, + role="definition_auditor", + payload={ + "definitions": [{"definition_id": "D1"}], + "missing_definitions": [], + }, + dependencies=[], + source_run_id="audit", + ) + transitions = [] + original = OrchestrationCheckpoint.transition + + def recording_transition(self, next_state, reason, **kwargs): + transitions.append(next_state) + return original(self, next_state, reason, **kwargs) + + monkeypatch.setattr( + OrchestrationCheckpoint, "transition", recording_transition, + ) + checkpoint.transition(ProofState.MATH_IR_TRANSLATION, "decomposed") + checkpoint.transition(ProofState.HOST_TYPED_IR_GATE, "translated") + checkpoint.transition(ProofState.LEAN_ELABORATION_GATE, "host-gated") + checkpoint.transition(ProofState.STRATEGY_TOURNAMENT, "lean-elaborated") + result = run_architecture_v7_entry( + checkpoint_path, + checkpoint, + project_root=Path(__file__).resolve().parents[3], + target_ref="replacement", + parent_obligation_ref="quarantined-parent", + parent_complexity=20, + event_type=StrategyEvent.TARGET_CHANGE, + event_id="TARGET_CHANGE:typed", + elaborated_theorem_id="hostTheorem", + proposition_hash="p" * 64, + ) + assert transitions == [ + ProofState.MATH_IR_TRANSLATION, + ProofState.HOST_TYPED_IR_GATE, + ProofState.LEAN_ELABORATION_GATE, + ProofState.STRATEGY_TOURNAMENT, + ProofState.RESEARCH_CONTRACT_GATE, + ProofState.PROOF_SEARCH, + ] + assert result.proof_state == ProofState.PROOF_SEARCH + assert result.research_contract_id + contract_payload = json.loads(Path( + result.validated_artifacts["research_contract"].path + ).read_text()) + assert contract_payload["definition_auditor_hash"] + assert contract_payload["definition_gap_ids"] == [] + + +def test_unelaborated_missing_definition_and_quarantine_route_to_decomposer( + tmp_path, +): + checkpoint_path = tmp_path / "proof_orchestration.json" + target = "quarantined-parent" + checkpoint = OrchestrationCheckpoint( + state=ProofState.STRATEGY_TOURNAMENT.value, + current_role="strategy_tournament", + target_obligation_id=target, + branch_history={ + "branch": { + "status": "QUARANTINED", + "evidence_ids": [target], + }, + }, + ) + persist_validated_artifact( + checkpoint_path, + checkpoint, + role="definition_auditor", + payload={ + "definitions": [], + "missing_definitions": [ + {"definition_id": f"DEF_{index}"} for index in range(8) + ], + }, + dependencies=[], + source_run_id="audit", + ) + result = run_architecture_v7_entry( + checkpoint_path, + checkpoint, + project_root=Path(__file__).resolve().parents[3], + target_ref=target, + parent_obligation_ref="ROOT", + parent_complexity=20, + event_type=StrategyEvent.INITIAL_BRANCH, + event_id="INITIAL_BRANCH:fixture", + ) + assert result.proof_state == ProofState.DECOMPOSER + assert result.research_contract_id == "" + assert "research_contract" not in result.validated_artifacts + assert result.research_contract_rejection_codes == [] + assert result.last_transition_reason == ( + "precontract-semantic-routing:MISSING_DEFINITION," + "UNELABORATED_TARGET,QUARANTINED_PARENT_REQUIRES_TYPED_REFRAME" + ) + tournament = json.loads(Path( + result.validated_artifacts["strategy_tournament"].path + ).read_text()) + assert len(tournament["plans"][3]["unresolved_definition_ids"]) == 8 + assert tournament["plans"][3]["execution_status"] == "PLANNING_ONLY" + + +def test_branch_kill_and_reframe_use_recorded_evidence_only(): + failures = BranchHistory("b", evidence=[ + BranchEvidence( + f"E{i}", "FAIL", semantic_failure_delta=1, + provenance_hash=str(i) * 64, + ) + for i in range(3) + ]) + assert review_branch( + failures, stagnation_threshold=4, failure_threshold=3, + ).status == "QUARANTINED" + stagnant = BranchHistory("c", evidence=[ + BranchEvidence(f"E{i}", "NONE", provenance_hash=str(i) * 64) + for i in range(4) + ]) + assert review_branch( + stagnant, stagnation_threshold=4, failure_threshold=3, + ).status == "REFRAME_REQUIRED" + + +def test_proof_search_refuses_free_text_or_unelaborated_goal(): + plan = _plans()[0] + decision = gate_research_contract( + plan, + elaborated_theorem_id="", + elaborated_proposition_hash="", + proof_obligation_id="O1", + registered_definition_ids=("D1",), + resolved_dependency_ids=("E1",), + verified_theorem_card_ids=("T1",), + allowed_assumption_ids=(), + environment_hash=ENV, + expected_plan_hash=plan.content_hash, + ) + assert decision.contract is None + with pytest.raises(AttributeError): + new_search_state(decision.contract, []) # type: ignore[arg-type] + + +def test_action_ids_mapping_deterministic_ast_feedback_budget_and_resume(tmp_path): + contract = _contract() + state = new_search_state(contract, [ + ProofGoal("G1", "p" * 64, ("H1",), "⊢ True"), + ], proof_budget=2) + actions = enumerate_applicable_actions( + state, + local_context_ids=("H1",), + theorem_card_to_operand_id={"T1": "LEMMA1"}, + ) + exact = next(item for item in actions if item.kind == "EXACT") + assert render_lean_ast( + exact, operand_sources={"H1": "h"}, substitution_sources={}, + ) == "exact h" + selection = ActionSelection("G1", exact.action_id, ("H1",), (), ()) + infrastructure = lambda _ast, _state: LeanStepResult( + False, FeedbackCode.HOST_ERROR.value, (), "host:1", + ) + attempt_step( + state, selection, actions, operand_sources={"H1": "h"}, + substitution_sources={}, lean_executor=infrastructure, + ) + assert state.semantic_failures == 0 + semantic = lambda _ast, _state: LeanStepResult( + False, FeedbackCode.TYPE_MISMATCH.value, (), "lean:1", + ) + attempt_step( + state, selection, actions, operand_sources={"H1": "h"}, + substitution_sources={}, lean_executor=semantic, + ) + assert state.semantic_failures == 1 + accepted = lambda _ast, _state: LeanStepResult( + True, FeedbackCode.ACCEPTED.value, (), + ) + attempt_step( + state, selection, actions, operand_sources={"H1": "h"}, + substitution_sources={}, lean_executor=accepted, token_count=7, + ) + assert state.status == "PROVED" and len(state.accepted_steps) == 1 + path = tmp_path / "proof.json" + persist_search_state(path, state) + resumed = load_search_state(path) + assert resumed.accepted_steps == state.accepted_steps + assert resumed.open_goals == state.open_goals + assert resumed.rejected_feedback == [] + assert json.loads(path.read_text())["accepted_steps"][0]["rendered_ast"] == "exact h" + + +def test_beam_ranking_rewards_lean_progress_support_and_novelty(): + contract = _contract() + state = new_search_state(contract, [ + ProofGoal("G1", "p" * 64, (), "g1"), + ProofGoal("G2", "p" * 64, (), "g2"), + ]) + actions = enumerate_applicable_actions( + state, + local_context_ids=(), + theorem_card_to_operand_id={"T1": "L1"}, + ) + ranked = beam_rank(((state, item) for item in actions), beam_width=2) + assert ranked[0][1].theorem_card_id == "T1" + + +@pytest.mark.skipif(shutil.which("lake") is None, reason="Lean unavailable") +def test_real_lean_multistep_acceptance_and_invalid_action_safe_failure(): + root = Path(__file__).resolve().parents[3] + contract = _contract() + state = new_search_state(contract, [ + ProofGoal("G1", "p" * 64, ("HP", "HQ"), "⊢ P ∧ Q"), + ]) + executor = lean_step_executor(LeanExecutionContext( + root, + "theorem stepwiseAnd (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by", + ("Mathlib",), + )) + actions = enumerate_applicable_actions( + state, local_context_ids=("HP", "HQ"), + theorem_card_to_operand_id={}, constructor_ids=("AND",), + ) + constructor = next(item for item in actions if item.kind == "CONSTRUCTOR") + first = attempt_step( + state, + ActionSelection("G1", constructor.action_id, ("AND",), (), ()), + actions, + operand_sources={"AND": "And.intro", "HP": "hP", "HQ": "hQ"}, + substitution_sources={}, + lean_executor=executor, + ) + assert first.accepted and state.open_goals + actions = enumerate_applicable_actions( + state, local_context_ids=("HP", "HQ"), + theorem_card_to_operand_id={}, + ) + hp = next(item for item in actions if item.operand_ids == ("HP",)) + second = attempt_step( + state, + ActionSelection(state.open_goals[0].goal_id, hp.action_id, ("HP",), (), ()), + actions, + operand_sources={"HP": "hP", "HQ": "hQ"}, + substitution_sources={}, + lean_executor=executor, + ) + assert second.accepted + actions = enumerate_applicable_actions( + state, local_context_ids=("HQ",), + theorem_card_to_operand_id={}, + ) + hq = next(item for item in actions if item.operand_ids == ("HQ",)) + final = attempt_step( + state, + ActionSelection(state.open_goals[0].goal_id, hq.action_id, ("HQ",), (), ()), + actions, + operand_sources={"HQ": "hQ"}, + substitution_sources={}, + lean_executor=executor, + ) + assert final.accepted and state.status == "PROVED" + + +def test_migration_branch_review_is_recorded_evidence_only_and_idempotent( + tmp_path, +): + checkpoint_path = tmp_path / "proof_orchestration.json" + ledger_path = tmp_path / "ledger.json" + snapshot = tmp_path / "snapshot" + snapshot.mkdir() + save_checkpoint(checkpoint_path, OrchestrationCheckpoint( + state=ProofState.DECOMPOSER.value, + current_role="decomposer", + ledger_version=91, + )) + ledger_path.write_text(json.dumps({ + "version": 91, + "obligations": [{ + "obligation_id": "density-1", + "statement": "Density Singularity recorded claim", + "status": "UNRESOLVED", + "formal_status": "UNFORMALIZED", + "last_evidence": "recorded only", + }], + })) + first = migrate(checkpoint_path, ledger_path, snapshot) + second = migrate(checkpoint_path, ledger_path, snapshot) + assert first == second + raw = json.loads(checkpoint_path.read_text()) + assert raw["state"] == "STRATEGY_TOURNAMENT" + review = raw["branch_history"]["density-singularity"] + assert review["assistant_verdict"] is None + assert review["evidence_ids"] == ["density-1"] + + +def test_preproof_migration_preserves_tournament_and_quarantine_idempotently( + tmp_path, +): + checkpoint_path = tmp_path / "proof_orchestration.json" + ledger_path = tmp_path / "ledger.json" + snapshot = tmp_path / "snapshot" + snapshot.mkdir() + checkpoint = OrchestrationCheckpoint( + state=ProofState.SYNTHESIS.value, + current_role="synthesis", + ledger_version=91, + strategy_plan_ids=["P1", "P2", "P3", "P4"], + selected_strategy_plan_id="P4", + strategy_tournament_hash="t" * 64, + research_contract_rejection_codes=["UNELABORATED_TARGET"], + branch_history={"branch": {"status": "QUARANTINED"}}, + ) + persist_validated_artifact( + checkpoint_path, + checkpoint, + role="strategy_tournament", + payload={"plan_ids": checkpoint.strategy_plan_ids}, + dependencies=[], + source_run_id="tournament", + ) + ledger_path.write_text(json.dumps({"version": 91})) + first = migrate_preproof(checkpoint_path, ledger_path, snapshot) + second = migrate_preproof(checkpoint_path, ledger_path, snapshot) + assert first == second + raw = json.loads(checkpoint_path.read_text()) + assert raw["state"] == "DECOMPOSER" + assert raw["research_contract_id"] == "" + assert raw["research_contract_rejection_codes"] == [] + assert raw["validated_artifacts"]["strategy_tournament"] + assert raw["branch_history"]["branch"]["status"] == "QUARANTINED" + assert first["event_id"] == PREPROOF_MIGRATION_EVENT