diff --git a/KakeyaLeanGate/Prelude.lean b/KakeyaLeanGate/Prelude.lean index a57e3d3..438a280 100644 --- a/KakeyaLeanGate/Prelude.lean +++ b/KakeyaLeanGate/Prelude.lean @@ -3,6 +3,7 @@ import Mathlib.Analysis.Complex.Hadamard import Mathlib.Analysis.Complex.JensenFormula import Mathlib.Analysis.Complex.LocallyUniformLimit import Mathlib.Analysis.Complex.Order +import Mathlib.Analysis.Analytic.Uniqueness /-! Minimal import target for AutoResearch theorem-signature validation. @@ -11,3 +12,31 @@ Generated signatures are compiled in temporary files importing this module. They may use `sorry` while their status is `FORMALIZED`; a proof obligation can only become `PROVED` after a separate no-sorry/no-axiom proof gate. -/ + +open Filter Metric Set + +/- Host-owned semantic atoms used by the typed decomposition registry. These +are definitions, not axioms; generated declarations can mention them, while +proof acceptance still requires the separate no-sorry Lean gate. -/ +def polesOutsideDisk (poles : Set ℂ) (center : ℂ) (radius : ℝ) : Prop := + Disjoint poles (ball center radius) + +def localUniformConvergenceOnDisk + (terms : ℕ → ℂ → ℂ) (sum : ℂ → ℂ) (center : ℂ) (radius : ℝ) : Prop := + TendstoLocallyUniformlyOn terms sum atTop (ball center radius) + +def termsHolomorphicOnDisk + (terms : ℕ → ℂ → ℂ) (center : ℂ) (radius : ℝ) : Prop := + ∀ n, DifferentiableOn ℂ (terms n) (ball center radius) + +def holomorphicSumOnDisk + (sum : ℂ → ℂ) (center : ℂ) (radius : ℝ) : Prop := + DifferentiableOn ℂ sum (ball center radius) + +def agreesWithSimplePoleOnPuncturedDisk + (sum : ℂ → ℂ) (center residue : ℂ) (radius : ℝ) : Prop := + EqOn sum (fun s => residue / (s - center)) (ball center radius \ {center}) + +def nonzeroComplex (z : ℂ) : Prop := z ≠ 0 + +def positiveRadius (radius : ℝ) : Prop := 0 < radius diff --git a/autoresearch/prefill/definition_registry.py b/autoresearch/prefill/definition_registry.py new file mode 100644 index 0000000..886b67d --- /dev/null +++ b/autoresearch/prefill/definition_registry.py @@ -0,0 +1,214 @@ +"""Host-owned definition choices for the active proof obligation.""" +from __future__ import annotations + +import hashlib +import json +from dataclasses import asdict, dataclass +from typing import Mapping + +from autoresearch.prefill.typed_transport import DecodedRoleFields, host_artifact + + +REGISTRY_VERSION = 1 + + +@dataclass(frozen=True) +class DefinitionChoice: + definition_id: str + content_ref: str + label: str + symbol_ids: tuple[str, ...] = () + domain_ids: tuple[str, ...] = () + topology_ids: tuple[str, ...] = () + required_type_id: str = "" + + +@dataclass(frozen=True) +class DefinitionChoiceRegistry: + target_ref: str + symbols: Mapping[str, str] + domains: Mapping[str, str] + topologies: Mapping[str, str] + definitions: Mapping[str, DefinitionChoice] + registry_hash: str + + @property + def registered_output_choices(self) -> dict[str, tuple[str, ...]]: + return { + "target_ref": (self.target_ref,), + "symbol_id": tuple(self.symbols), + "domain_id": tuple(self.domains), + "topology_id": tuple(self.topologies), + "definition_id": tuple(self.definitions), + "missing_definition_id": tuple(self.definitions), + } + + +_SYMBOLS = { + "SYM_EPSILON": "content:symbol:epsilon", + "SYM_GENUS_P": "content:symbol:genus_p", + "SYM_CRITICAL_DENSITY": "content:symbol:critical_density", + "SYM_SEQUENCE": "content:symbol:zero_sequence", + "SYM_SEQUENCE_DENSITY": "content:symbol:sequence_density", + "SYM_COMPLEX_VARIABLE": "content:symbol:complex_variable", + "SYM_POLE_LOCATION": "content:symbol:pole_location", + "SYM_POLE_MULTIPLICITY": "content:symbol:pole_multiplicity", + "SYM_FUNCTION": "content:symbol:entire_function", +} +_DOMAINS = { + "DOM_POSITIVE_REAL": "content:domain:positive_real", + "DOM_NATURAL": "content:domain:natural", + "DOM_COMPLEX": "content:domain:complex", + "DOM_COMPLEX_SEQUENCE": "content:domain:complex_sequence", +} +_TOPOLOGIES = { + "TOP_DELTA_NEIGHBORHOOD": "content:topology:delta_neighborhood", + "TOP_LOCALLY_UNIFORM": "content:topology:locally_uniform", + "TOP_POINTWISE": "content:topology:pointwise", +} +_DEFINITIONS = { + "DEF_EPSILON": DefinitionChoice( + "DEF_EPSILON", "content:definition:epsilon", "Epsilon", + ("SYM_EPSILON",), ("DOM_POSITIVE_REAL",), + ), + "DEF_GENUS": DefinitionChoice( + "DEF_GENUS", "content:definition:genus", "Fixed genus", + ("SYM_GENUS_P",), ("DOM_NATURAL",), + ), + "DEF_CRITICAL_DENSITY": DefinitionChoice( + "DEF_CRITICAL_DENSITY", + "content:definition:critical_density", + "Critical density", + ("SYM_CRITICAL_DENSITY",), ("DOM_POSITIVE_REAL",), + required_type_id="TYPE_DENSITY_THRESHOLD", + ), + "DEF_SEQUENCE_DENSITY": DefinitionChoice( + "DEF_SEQUENCE_DENSITY", + "content:definition:sequence_density", + "Sequence density", + ("SYM_SEQUENCE", "SYM_SEQUENCE_DENSITY"), + ("DOM_COMPLEX_SEQUENCE", "DOM_POSITIVE_REAL"), + required_type_id="TYPE_SEQUENCE_DENSITY", + ), + "DEF_SERIES_CONVERGENCE": DefinitionChoice( + "DEF_SERIES_CONVERGENCE", + "content:definition:series_convergence", + "Series convergence", + ("SYM_SEQUENCE", "SYM_COMPLEX_VARIABLE"), + ("DOM_COMPLEX_SEQUENCE", "DOM_COMPLEX"), + ("TOP_LOCALLY_UNIFORM", "TOP_POINTWISE"), + "TYPE_CONVERGENCE_MODE", + ), + "DEF_POLE_NEIGHBORHOOD": DefinitionChoice( + "DEF_POLE_NEIGHBORHOOD", + "content:definition:pole_neighborhood", + "Pole neighborhood", + ("SYM_POLE_LOCATION", "SYM_POLE_MULTIPLICITY"), + ("DOM_COMPLEX",), + ("TOP_DELTA_NEIGHBORHOOD",), + "TYPE_PUNCTURED_OR_FULL_NEIGHBORHOOD", + ), + "DEF_FUNCTION_BINDING": DefinitionChoice( + "DEF_FUNCTION_BINDING", + "content:definition:function_binding", + "Function binding", + ("SYM_FUNCTION", "SYM_SEQUENCE"), + ("DOM_COMPLEX",), + required_type_id="TYPE_CANONICAL_PRODUCT_BINDING", + ), + "DEF_GROWTH_ORDER": DefinitionChoice( + "DEF_GROWTH_ORDER", + "content:definition:growth_order", + "Growth order", + ("SYM_FUNCTION", "SYM_GENUS_P"), + ("DOM_COMPLEX", "DOM_NATURAL"), + required_type_id="TYPE_ENTIRE_FUNCTION_ORDER", + ), +} + + +def build_definition_choice_registry(target_ref: str) -> DefinitionChoiceRegistry: + """Bind the immutable current-obligation registry to one claim reference.""" + canonical = json.dumps({ + "version": REGISTRY_VERSION, + "target_ref": target_ref, + "symbols": _SYMBOLS, + "domains": _DOMAINS, + "topologies": _TOPOLOGIES, + "definitions": { + key: asdict(value) for key, value in _DEFINITIONS.items() + }, + }, sort_keys=True, separators=(",", ":")).encode() + return DefinitionChoiceRegistry( + target_ref=target_ref, + symbols=dict(_SYMBOLS), + domains=dict(_DOMAINS), + topologies=dict(_TOPOLOGIES), + definitions=dict(_DEFINITIONS), + registry_hash=hashlib.sha256(canonical).hexdigest(), + ) + + +def serialize_definition_audit( + decoded: DecodedRoleFields, + registry: DefinitionChoiceRegistry, + *, + target_obligation_id: str, + parent_statement_hash: str, + root_goal_hash: str, + producer_run_id: str, +) -> tuple[dict[str, object], dict[str, object]]: + """Resolve IDs and serialize the authoritative audit entirely on the Host.""" + values = decoded.values + outcome = str(values["audit_outcome"]) + defined_ids = tuple(dict.fromkeys(values["definition_id"])) + missing_ids = tuple(dict.fromkeys(values["missing_definition_id"])) + + if set(defined_ids) & set(missing_ids): + raise ValueError("definition choice cannot be both defined and missing") + if outcome == "COMPLETE" and missing_ids: + raise ValueError("COMPLETE audit cannot contain missing definitions") + if outcome == "MISSING_DEFINITION" and not missing_ids: + raise ValueError("MISSING_DEFINITION requires a registered missing choice") + if outcome == "REFRAME_REQUIRED" and not missing_ids: + # No invented choice is an intentional semantic reframe, never syntax retry. + missing_ids = tuple(registry.definitions) + + def resolved(choice_id: str, *, missing: bool) -> dict[str, object]: + choice = registry.definitions[choice_id] + return { + "definition_id": choice.definition_id, + "content_ref": choice.content_ref, + "label": choice.label, + "symbol_ids": list(choice.symbol_ids), + "domain_ids": list(choice.domain_ids), + "topology_ids": list(choice.topology_ids), + "required_type_id": choice.required_type_id, + **({"obligation_label": f"D{missing_ids.index(choice_id) + 1}"} + if missing else {}), + } + + payload: dict[str, object] = { + "target_obligation_id": target_obligation_id, + "parent_statement_hash": parent_statement_hash, + "root_goal_hash": root_goal_hash, + "producer_role": "definition_auditor", + "producer_run_id": producer_run_id, + "upstream_artifact_hashes": [], + "definitions": [resolved(item, missing=False) for item in defined_ids], + "missing_definitions": [resolved(item, missing=True) for item in missing_ids], + } + envelope = host_artifact( + decoded, + host_bindings={ + "artifact_kind": "DEFINITION_AUDIT", + "target_obligation_id": target_obligation_id, + "parent_statement_hash": parent_statement_hash, + "root_goal_hash": root_goal_hash, + "producer_run_id": producer_run_id, + "registry_hash": registry.registry_hash, + "audit_outcome": outcome, + }, + dependencies=(), + ) + return payload, envelope diff --git a/autoresearch/prefill/host_compiler.py b/autoresearch/prefill/host_compiler.py new file mode 100644 index 0000000..0b66402 --- /dev/null +++ b/autoresearch/prefill/host_compiler.py @@ -0,0 +1,207 @@ +"""Crash-safe deterministic Typed IR and Lean gate pipeline.""" +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 + +from autoresearch.prefill.math_ir import ( + GateStatus, + LeanCompilation, + MathIR, + TypedIRError, + ValidatedMathIR, + build_lean_declaration, + parse_math_ir, + registry_hash, + validate_math_ir, + verify_proposition_equivalence, +) + + +HOST_COMPILER_VERSION = 2 + + +@dataclass(frozen=True) +class GateEvidence: + stage: str + status: str + input_hash: str + output_hash: str = "" + code: str = "" + message: str = "" + owner: str = "host" + created_at: float = 0.0 + + +@dataclass(frozen=True) +class HostGateResult: + ok: bool + math_ir: MathIR | None + validated_ir: ValidatedMathIR | None + compilation: LeanCompilation | None + evidence: tuple[GateEvidence, ...] + failure_status: str = "" + backjump_owner: 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 _write_atomic(path: Path, payload: dict) -> 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 _classify_elaboration_failure(output: str) -> tuple[GateStatus, str, str]: + lowered = str(output).casefold() + if any(marker in lowered for marker in ( + "unknown identifier", "unknown constant", "unknown namespace", + "failed to synthesize", "declaration uses 'sorry'", + )): + return ( + GateStatus.SEMANTIC_BACKJUMP, + "MISSING_DEFINITION_ENVIRONMENT", + "decomposer", + ) + if any(marker in lowered for marker in ( + "unexpected token", "invalid syntax", "parser", "lexer", + "type mismatch", "application type mismatch", + )): + return GateStatus.INTEGRATION_BLOCKED, "HOST_LEAN_GENERATION_DEFECT", "host" + return GateStatus.INTEGRATION_BLOCKED, "LEAN_ENVIRONMENT_FAILURE", "host" + + +def run_host_gates( + math_ir_lines: Iterable[str], + *, + project_root: Path, + cache_dir: Path, + lean_validator: Callable, +) -> HostGateResult: + """Run all deterministic gates once for a content-addressed input.""" + normalized_lines = tuple(str(item).strip() for item in math_ir_lines if str(item).strip()) + input_hash = _digest({ + "compiler_version": HOST_COMPILER_VERSION, + "registry_hash": registry_hash(), + "lines": normalized_lines, + }) + cache_path = Path(cache_dir).expanduser() / f"{input_hash}.json" + evidence: list[GateEvidence] = [] + math_ir: MathIR | None = None + validated: ValidatedMathIR | None = None + compilation: LeanCompilation | None = None + + def passed(stage: str, output_hash: str) -> None: + evidence.append(GateEvidence( + stage, GateStatus.PASSED.value, input_hash, output_hash, + created_at=time.time(), + )) + + def failed(stage: str, error: TypedIRError) -> HostGateResult: + evidence.append(GateEvidence( + stage, + error.status.value, + input_hash, + code=error.code, + message=str(error), + owner=error.owner, + created_at=time.time(), + )) + _write_atomic(cache_path, { + "schema_version": HOST_COMPILER_VERSION, + "input_hash": input_hash, + "registry_hash": registry_hash(), + "ok": False, + "evidence": [asdict(item) for item in evidence], + }) + return HostGateResult( + False, math_ir, validated, compilation, tuple(evidence), + error.status.value, error.owner, + ) + + try: + math_ir = parse_math_ir( + normalized_lines, + theorem_id=f"typed_{input_hash[:16]}", + ) + passed("TYPED_TRANSPORT_VALIDATION", _digest(asdict(math_ir))) + except TypedIRError as exc: + return failed("TYPED_TRANSPORT_VALIDATION", exc) + try: + validated = validate_math_ir(math_ir) + passed("TYPED_MATH_IR_STRUCTURAL_VALIDATION", validated.content_hash) + passed("SYMBOL_TYPE_OPERATOR_RESOLUTION", registry_hash()) + except TypedIRError as exc: + return failed("TYPED_MATH_IR_STRUCTURAL_VALIDATION", exc) + try: + compilation = build_lean_declaration(validated) + passed("LEAN_AST_SOURCE_GENERATION", compilation.declaration_hash) + except Exception as exc: + return failed("LEAN_AST_SOURCE_GENERATION", TypedIRError( + "HOST_AST_BUILDER_EXCEPTION", + f"{type(exc).__name__}: {exc}", + owner="host", + status=GateStatus.INTEGRATION_BLOCKED, + )) + elaborated = lean_validator( + compilation.declaration_source, + project_root=Path(project_root), + ) + if not elaborated.ok: + status, code, owner = _classify_elaboration_failure( + elaborated.error or elaborated.output, + ) + return failed("LEAN_ELABORATION", TypedIRError( + code, + elaborated.error or elaborated.output, + owner=owner, + status=status, + )) + passed("LEAN_ELABORATION", elaborated.signature_hash) + try: + if elaborated.signature_hash != compilation.declaration_hash: + raise TypedIRError( + "ELABORATED_DECLARATION_HASH_MISMATCH", + "Lean elaborated a declaration different from the host AST", + owner="host", + status=GateStatus.INTEGRATION_BLOCKED, + ) + verify_proposition_equivalence(validated, compilation) + passed("PROPOSITION_HASH_EQUIVALENCE", compilation.proposition_hash) + except TypedIRError as exc: + return failed("PROPOSITION_HASH_EQUIVALENCE", exc) + payload = { + "schema_version": HOST_COMPILER_VERSION, + "input_hash": input_hash, + "registry_hash": registry_hash(), + "ok": True, + "math_ir": asdict(math_ir), + "compilation": asdict(compilation), + "evidence": [asdict(item) for item in evidence], + } + _write_atomic(cache_path, payload) + return HostGateResult( + True, math_ir, validated, compilation, tuple(evidence), + ) diff --git a/autoresearch/prefill/lean_gate.py b/autoresearch/prefill/lean_gate.py index 4773703..733e9ae 100644 --- a/autoresearch/prefill/lean_gate.py +++ b/autoresearch/prefill/lean_gate.py @@ -1,7 +1,8 @@ -"""Fail-closed Lean theorem-signature gate for proof obligations.""" +"""Fail-closed contracts for model-authored Lean declarations.""" from __future__ import annotations import hashlib +import json import os import re import signal @@ -24,6 +25,464 @@ r"\b(?:IO|System|FilePath)\b", re.MULTILINE, ) +_DECLARATION = re.compile( + r"\A(?Ptheorem|lemma)\s+" + r"(?P[A-Za-z_][A-Za-z0-9_']*)" + r"(?P.*?)\Z", + re.DOTALL, +) +_DECLARATION_LINE = re.compile( + r"^\s*(?:theorem|lemma|def|axiom|opaque|abbrev|instance|structure|" + r"inductive|class)\b", + re.MULTILINE, +) +_SCAFFOLD = re.compile(r"\s*:=\s*by\b") +_PLACEHOLDER = re.compile( + r"\b(?:sorry|admit|placeholder|todo)\b|" + r"\.\.\.|…|<[A-Za-z_][A-Za-z0-9_ -]{0,40}>|\?\w*", + re.IGNORECASE, +) +_LATEX_ESCAPE = re.compile(r"\\[A-Za-z]+|[$]") + + +@dataclass(frozen=True) +class LeanDeclaration: + kind: str + name: str + binders: str + proposition: str + source: str + declaration_hash: str + proposition_hash: str + + +@dataclass(frozen=True) +class LeanContractUser: + role: str + file: str + policy: str + contract_id: str + contract_version: int + fixtures: tuple[str, ...] + + +@dataclass(frozen=True) +class LeanContractDefinition: + contract_id: str + version: int + schema_version: int + allowed_kinds: tuple[str, ...] + exact_scaffold: str + forbidden_constructs: tuple[str, ...] + signature_only: bool + content_sha256: str + + +@dataclass(frozen=True) +class LeanSymbol: + name: str + lean_type: str + source_symbol_hash: str + aliases: tuple[str, ...] = () + + +@dataclass(frozen=True) +class LeanSymbolTableDefinition: + symbol_table_id: str + version: int + schema_version: int + parent_statement_hash: str + symbols: tuple[LeanSymbol, ...] + content_sha256: str + + +def _contract_definition( + *, + name: str, + version: int, + signature_only: bool, +) -> LeanContractDefinition: + content = { + "name": name, + "version": version, + "schema_version": 1, + "allowed_kinds": ["theorem", "lemma"], + "exact_scaffold": ":= by", + "forbidden_constructs": [ + "prose", + "markdown_fence", + "commands", + "multiple_declarations", + "placeholders", + "latex_escapes", + "proof_body" if signature_only else "missing_proof_body", + ], + "signature_only": signature_only, + } + digest = hashlib.sha256( + json.dumps(content, sort_keys=True, separators=(",", ":")).encode(), + ).hexdigest() + return LeanContractDefinition( + contract_id=f"{name}-{digest[:16]}", + version=version, + schema_version=1, + allowed_kinds=("theorem", "lemma"), + exact_scaffold=":= by", + forbidden_constructs=tuple(content["forbidden_constructs"]), + signature_only=signature_only, + content_sha256=digest, + ) + + +_SIGNATURE_CONTRACT_DEFINITION = _contract_definition( + name="lean-signature", + version=1, + signature_only=True, +) +_PROOF_CONTRACT_DEFINITION = _contract_definition( + name="lean-proof", + version=1, + signature_only=False, +) +LEAN_CONTRACT_REGISTRY = { + (contract.contract_id, contract.version): contract + for contract in ( + _SIGNATURE_CONTRACT_DEFINITION, + _PROOF_CONTRACT_DEFINITION, + ) +} +LEAN_SYMBOL_TABLE_REGISTRY: dict[ + tuple[str, int], + LeanSymbolTableDefinition, +] = {} + +_AUDITED_SYMBOL_NAMES = { + r"\epsilon": ("epsilon", r"\epsilon"), + "p": ("p",), + r"\rho_c": ("rho_c", r"\rho_c"), + r"\{z_n\}": ("z",), + r"\rho": ("rho", r"\rho"), + "s": ("s",), + "s_0": ("s0",), + r"\delta": ("delta", r"\delta"), + "m": ("m",), + "f(s)": ("f",), + "growth order": ("growthOrder",), +} +_AUDITED_TYPE_MAP = { + "real constant": "ℝ", + "integer (genus)": "ℕ", + "critical density threshold": "ℝ", + "sequence of complex numbers": "ℕ → ℂ", + "density of sequence": "ℝ", + "complex variable": "ℂ", + "singularity point": "ℂ", + "neighborhood radius": "ℝ", + "integer constant": "ℤ", + "meromorphic/analytic function": "ℂ → ℂ", + "order of growth (complex analysis)": "(ℂ → ℂ) → ℝ", +} +_AUDITED_SYMBOL_ID_MAP = { + "SYM_EPSILON": ("epsilon", "ℝ"), + "SYM_GENUS_P": ("p", "ℕ"), + "SYM_CRITICAL_DENSITY": ("rho_c", "ℝ"), + "SYM_SEQUENCE": ("z", "ℕ → ℂ"), + "SYM_SEQUENCE_DENSITY": ("rho", "ℝ"), + "SYM_COMPLEX_VARIABLE": ("s", "ℂ"), + "SYM_POLE_LOCATION": ("s0", "ℂ"), + "SYM_POLE_MULTIPLICITY": ("m", "ℤ"), + "SYM_FUNCTION": ("f", "ℂ → ℂ"), +} +_MISSING_DEFINITION_ID_MAP = { + "DEF_EPSILON": ("positiveEpsilon", "ℝ → Prop"), + "DEF_GENUS": ("fixedGenus", "ℕ → Prop"), + "DEF_CRITICAL_DENSITY": ("criticalDensity", "ℝ"), + "DEF_SEQUENCE_DENSITY": ("density", "(ℕ → ℂ) → ℝ"), + "DEF_SERIES_CONVERGENCE": ( + "localConvergence", + "(ℕ → ℂ) → ℂ → ℤ → ℝ → Prop", + ), + "DEF_POLE_NEIGHBORHOOD": ("poleNeighborhood", "ℂ → ℝ → Prop"), + "DEF_FUNCTION_BINDING": ("canonicalProductBinding", "(ℕ → ℂ) → (ℂ → ℂ) → Prop"), + "DEF_GROWTH_ORDER": ("growthConstraint", "(ℂ → ℂ) → ℕ → Prop"), +} + + +def register_lean_symbol_table( + definitions: list[dict], + *, + parent_statement_hash: str, + missing_definitions: list[dict] | None = None, + version: int = 1, +) -> LeanSymbolTableDefinition: + symbols = [] + seen_symbol_ids = set() + for item in definitions: + symbol_ids = item.get("symbol_ids") + if isinstance(symbol_ids, list): + for symbol_id in symbol_ids: + symbol_id = str(symbol_id) + if symbol_id in seen_symbol_ids: + continue + if symbol_id not in _AUDITED_SYMBOL_ID_MAP: + raise ValueError( + f"unregistered audited symbol ID: {symbol_id}", + ) + name, lean_type = _AUDITED_SYMBOL_ID_MAP[symbol_id] + symbols.append(LeanSymbol( + name=name, + lean_type=lean_type, + source_symbol_hash=hashlib.sha256( + symbol_id.encode(), + ).hexdigest(), + )) + seen_symbol_ids.add(symbol_id) + continue + raw_symbol = str(item.get("symbol", "")) + raw_type = str(item.get("type", "")) + if raw_symbol not in _AUDITED_SYMBOL_NAMES: + raise ValueError(f"unregistered audited symbol: {raw_symbol}") + if raw_type not in _AUDITED_TYPE_MAP: + raise ValueError(f"unregistered audited symbol type: {raw_type}") + names = _AUDITED_SYMBOL_NAMES[raw_symbol] + symbols.append(LeanSymbol( + name=names[0], + lean_type=_AUDITED_TYPE_MAP[raw_type], + source_symbol_hash=hashlib.sha256(raw_symbol.encode()).hexdigest(), + aliases=tuple(names[1:]), + )) + missing_symbol_specs = { + "L1": ("density", "(ℕ → ℂ) → ℝ"), + "L2": ( + "localConvergence", + "(ℕ → ℂ) → ℂ → ℤ → ℝ → Prop", + ), + "L3": ("growthConstraint", "(ℂ → ℂ) → ℕ → Prop"), + } + for item in missing_definitions or []: + definition_id = str(item.get("definition_id", "")) + if definition_id: + if definition_id not in _MISSING_DEFINITION_ID_MAP: + raise ValueError( + f"unregistered missing definition ID: {definition_id}", + ) + name, lean_type = _MISSING_DEFINITION_ID_MAP[definition_id] + symbols.append(LeanSymbol( + name=name, + lean_type=lean_type, + source_symbol_hash=hashlib.sha256( + definition_id.encode(), + ).hexdigest(), + )) + continue + label = str(item.get("obligation_label", "")) + if label not in missing_symbol_specs: + raise ValueError(f"unregistered missing definition label: {label}") + name, lean_type = missing_symbol_specs[label] + symbols.append(LeanSymbol( + name=name, + lean_type=lean_type, + source_symbol_hash=hashlib.sha256( + json.dumps( + item, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode(), + ).hexdigest(), + )) + content = { + "version": version, + "schema_version": 1, + "parent_statement_hash": parent_statement_hash, + "symbols": [ + { + "name": symbol.name, + "lean_type": symbol.lean_type, + "source_symbol_hash": symbol.source_symbol_hash, + "aliases": list(symbol.aliases), + } + for symbol in symbols + ], + } + digest = hashlib.sha256( + json.dumps(content, sort_keys=True, separators=(",", ":")).encode(), + ).hexdigest() + table = LeanSymbolTableDefinition( + symbol_table_id=f"lean-symbols-{digest[:16]}", + version=version, + schema_version=1, + parent_statement_hash=parent_statement_hash, + symbols=tuple(symbols), + content_sha256=digest, + ) + LEAN_SYMBOL_TABLE_REGISTRY[(table.symbol_table_id, table.version)] = table + return table + + +def resolve_lean_symbol_table( + symbol_table_id: str, + version: int, +) -> LeanSymbolTableDefinition: + try: + return LEAN_SYMBOL_TABLE_REGISTRY[ + (str(symbol_table_id), int(version)) + ] + except (KeyError, TypeError, ValueError) as exc: + raise ValueError("unknown or stale Lean symbol table ID/version") from exc + + +def lean_symbol_semantic_hash( + text: str, + table: LeanSymbolTableDefinition, +) -> str: + canonical = str(text) + aliases = sorted( + ( + (alias, symbol.name) + for symbol in table.symbols + for alias in symbol.aliases + ), + key=lambda item: len(item[0]), + reverse=True, + ) + for alias, name in aliases: + canonical = canonical.replace(alias, name) + return hashlib.sha256(canonical.encode()).hexdigest() + + +def normalize_registered_latex_identifiers( + text: str, + table: LeanSymbolTableDefinition, +) -> str: + """Normalize only audited identifier tokens; reject semantic LaTeX.""" + original = str(text) + normalized = original + aliases = sorted( + ( + (alias, symbol.name) + for symbol in table.symbols + for alias in symbol.aliases + ), + key=lambda item: len(item[0]), + reverse=True, + ) + for alias, name in aliases: + pattern = ( + rf"(? None: + for message in messages: + content = str(message.get("content", "")) + escapes = re.findall(r"\\[A-Za-z]+|\\[{}]", content) + if escapes: + raise ValueError( + "Lean-producing prompt contains raw LaTeX: " + + ", ".join(sorted(set(escapes))), + ) + + +def resolve_lean_contract( + contract_id: str, + version: int, + *, + signature_only: bool | None = None, +) -> LeanContractDefinition: + try: + contract = LEAN_CONTRACT_REGISTRY[(str(contract_id), int(version))] + except (KeyError, TypeError, ValueError) as exc: + raise ValueError("unknown or stale Lean contract ID/version") from exc + if signature_only is not None and contract.signature_only != signature_only: + raise ValueError("Lean contract policy mismatch") + return contract + + +def lean_signature_contract_ref() -> dict[str, object]: + return { + "contract_id": _SIGNATURE_CONTRACT_DEFINITION.contract_id, + "version": _SIGNATURE_CONTRACT_DEFINITION.version, + } + + +def lean_proof_contract_ref() -> dict[str, object]: + return { + "contract_id": _PROOF_CONTRACT_DEFINITION.contract_id, + "version": _PROOF_CONTRACT_DEFINITION.version, + } + + +LEAN_SIGNATURE_FIXTURES = ( + "zero_declarations", + "multiple_declarations", + "prose", + "fence", + "def", + "forbidden_command", + "missing_scaffold", + "duplicate_scaffold", + "proof_body", + "placeholder", + "unknown_type", + "changed_theorem_target", + "latex_escape", + "valid_multiline_binders", + "latest_parent_prose", + "latest_child_missing_scaffold", + "latest_reduction_hash", + "latex_identifier_epsilon", + "latex_identifier_rho", + "latex_identifier_delta", + "forbidden_latex_sum", + "forbidden_latex_frac", + "forbidden_latex_set", + "mixed_prose_lean", + "unknown_latex_command", + "escaped_json_backslashes", + "valid_unicode_ascii", +) + +# CI treats this as the exhaustive registry of model roles that may carry Lean. +LEAN_CONTRACT_USER_REGISTRY = { + "formalizer": LeanContractUser( + "formalizer", + "scripts/agent_gan_repl.py", + "signature", + _SIGNATURE_CONTRACT_DEFINITION.contract_id, + _SIGNATURE_CONTRACT_DEFINITION.version, + LEAN_SIGNATURE_FIXTURES, + ), + "prover": LeanContractUser( + "prover", + "scripts/agent_gan_repl.py", + "complete_proof", + _PROOF_CONTRACT_DEFINITION.contract_id, + _PROOF_CONTRACT_DEFINITION.version, + LEAN_SIGNATURE_FIXTURES, + ), + "premise_auditor": LeanContractUser( + "premise_auditor", + "scripts/agent_gan_repl.py", + "reject_unbound_lean", + _PROOF_CONTRACT_DEFINITION.contract_id, + _PROOF_CONTRACT_DEFINITION.version, + LEAN_SIGNATURE_FIXTURES, + ), +} @dataclass(frozen=True) @@ -36,6 +495,11 @@ class LeanSignatureResult: attempts: int = 1 elapsed_s: float = 0.0 output: str = "" + normalized_source: str = "" + declaration_name: str = "" + binders: str = "" + proposition: str = "" + proposition_hash: str = "" @dataclass(frozen=True) @@ -46,6 +510,191 @@ class _LeanRun: output: str +class LeanSignatureContract: + """Syntactic contract shared by every model-authored Lean declaration.""" + + allowed_kinds = ("theorem", "lemma") + exact_scaffold = ":= by" + + @staticmethod + def _split_tail(tail: str) -> tuple[str, str]: + depth = 0 + pairs = {"(": ")", "{": "}", "[": "]"} + closers = set(pairs.values()) + quote = False + escape = False + for index, char in enumerate(tail): + if quote: + if escape: + escape = False + elif char == "\\": + escape = True + elif char == '"': + quote = False + continue + if char == '"': + quote = True + elif char in pairs: + depth += 1 + elif char in closers: + depth -= 1 + if depth < 0: + raise ValueError("unbalanced declaration binders") + elif char == ":" and depth == 0: + return tail[:index].strip(), tail[index + 1:].strip() + raise ValueError("declaration is missing a proposition separator `:`") + + def parse( + self, + source: str, + *, + signature_only: bool, + allow_scaffold_normalization: bool = False, + expected: dict[str, str] | None = None, + ) -> LeanDeclaration: + raw = str(source) + if not raw.strip(): + raise ValueError("empty Lean declaration") + if len(raw) > 12_000: + raise ValueError("Lean declaration is too large") + if "```" in raw: + raise ValueError("Markdown fences are forbidden") + if "--" in raw or "/-" in raw or "-/" in raw: + raise ValueError("comments or prose are forbidden") + if _LATEX_ESCAPE.search(raw): + raise ValueError("LaTeX escapes are forbidden in Lean source") + if _FORBIDDEN.search(raw): + raise ValueError("forbidden Lean command in generated declaration") + if _PLACEHOLDER.search(raw): + raise ValueError("Lean declaration contains a placeholder") + if len(_DECLARATION_LINE.findall(raw)) != 1: + raise ValueError("expected exactly one theorem or lemma declaration") + + text = raw.strip() + match = _DECLARATION.fullmatch(text) + if match is None: + raise ValueError( + "artifact must contain only one theorem or lemma declaration", + ) + scaffold_matches = list(_SCAFFOLD.finditer(match.group("tail"))) + if len(scaffold_matches) > 1: + raise ValueError("duplicate `:= by` proof scaffold") + if not scaffold_matches: + if not allow_scaffold_normalization: + raise ValueError( + "theorem signature must end with `:= by` proof scaffold", + ) + declaration_tail = match.group("tail").rstrip() + proof_body = "" + else: + scaffold = scaffold_matches[0] + declaration_tail = match.group("tail")[:scaffold.start()].rstrip() + proof_body = match.group("tail")[scaffold.end():] + if signature_only and proof_body.strip(): + raise ValueError("signature proof scaffold must have no proof body") + if not signature_only and not proof_body.strip(): + raise ValueError("complete proof must contain a proof body") + + binders, proposition = self._split_tail(declaration_tail) + if not proposition: + raise ValueError("Lean declaration proposition is empty") + kind = match.group("kind") + name = match.group("name") + if expected: + comparisons = { + "kind": kind, + "name": name, + "binders": binders, + "proposition": proposition, + } + for field, actual in comparisons.items(): + if field in expected and str(expected[field]).strip() != actual: + raise ValueError(f"{field} changed during signature transport") + + declaration_core = f"{kind} {name}" + if binders: + declaration_core += f" {binders}" + declaration_core += f" : {proposition}" + normalized = ( + declaration_core + " := by" + if signature_only + else text + ) + declaration_hash = hashlib.sha256( + " ".join(declaration_core.split()).encode(), + ).hexdigest() + proposition_hash = hashlib.sha256(proposition.encode()).hexdigest() + normalized_parsed = _DECLARATION.fullmatch(normalized) + if normalized_parsed is None: + raise ValueError("normalized Lean declaration is malformed") + normalized_tail = normalized_parsed.group("tail") + normalized_scaffold = _SCAFFOLD.search(normalized_tail) + assert normalized_scaffold is not None + normalized_binders, normalized_proposition = self._split_tail( + normalized_tail[:normalized_scaffold.start()].rstrip(), + ) + if ( + normalized_parsed.group("name") != name + or normalized_binders != binders + or normalized_proposition != proposition + or hashlib.sha256(normalized_proposition.encode()).hexdigest() + != proposition_hash + ): + raise ValueError("mechanical normalization changed mathematical content") + return LeanDeclaration( + kind=kind, + name=name, + binders=binders, + proposition=proposition, + source=normalized, + declaration_hash=declaration_hash, + proposition_hash=proposition_hash, + ) + + def normalize_signature( + self, + source: str, + *, + expected: dict[str, str] | None = None, + ) -> LeanDeclaration: + return self.parse( + source, + signature_only=True, + allow_scaffold_normalization=True, + expected=expected, + ) + + def validate_signature( + self, + source: str, + *, + expected: dict[str, str] | None = None, + ) -> LeanDeclaration: + return self.parse( + source, + signature_only=True, + allow_scaffold_normalization=False, + expected=expected, + ) + + def validate_proof(self, source: str) -> LeanDeclaration: + return self.parse(source, signature_only=False) + + def example(self, name: str = "contractExample") -> dict[str, str]: + source = f"theorem {name} (P : Prop) (h : P) : P := by" + parsed = self.validate_signature(source) + return { + "kind": parsed.kind, + "name": parsed.name, + "binders": parsed.binders, + "proposition": parsed.proposition, + "source": parsed.source, + } + + +LEAN_SIGNATURE_CONTRACT = LeanSignatureContract() + + def extract_lean_signature_blocks(text: str) -> list[tuple[str, str]]: return [ ((match.group(1) or "").strip(), match.group("source").strip()) @@ -59,8 +708,26 @@ def _signature_only(source: str) -> str: def lean_theorem_signature_hash(source: str) -> str: - signature = " ".join(_signature_only(source).split()) - return hashlib.sha256(signature.encode()).hexdigest() if signature else "" + try: + return LEAN_SIGNATURE_CONTRACT.normalize_signature( + source, + ).declaration_hash + except ValueError: + signature = " ".join(_signature_only(source).split()) + return hashlib.sha256(signature.encode()).hexdigest() if signature else "" + + +def normalize_lean_signature( + source: str, + *, + expected: dict[str, str] | None = None, +) -> LeanDeclaration: + """Add/canonicalize only the terminal scaffold, never mathematics.""" + return LEAN_SIGNATURE_CONTRACT.normalize_signature(source, expected=expected) + + +def lean_signature_contract_example(name: str = "contractExample") -> dict[str, str]: + return LEAN_SIGNATURE_CONTRACT.example(name) def _run_lean( @@ -182,47 +849,22 @@ def validate_lean_signature( retry_timeout_s: float = 120.0, ) -> LeanSignatureResult: source = source.strip() - if not source: - return LeanSignatureResult( - "", "", False, status="TYPECHECK_FAILED", - error="empty Lean signature", - ) - if len(source) > 12_000: - return LeanSignatureResult( - "", "", False, status="TYPECHECK_FAILED", - error="Lean signature too large", - ) - if _FORBIDDEN.search(source): - return LeanSignatureResult( - source, - "", - False, - status="UNSAFE_REJECTED", - error="forbidden Lean command in generated signature", - ) - declarations = re.findall(r"^\s*theorem\s+([A-Za-z_][\w']*)", source, re.MULTILINE) - if len(declarations) != 1: - return LeanSignatureResult( - source, - "", - False, - status="TYPECHECK_FAILED", - error="expected exactly one theorem declaration", - ) - if not re.search(r"\s*:=\s*by\b", source): + try: + declaration = LEAN_SIGNATURE_CONTRACT.validate_signature(source) + except ValueError as exc: return LeanSignatureResult( source, "", False, - status="TYPECHECK_FAILED", - error="theorem signature must end with `:= by` proof scaffold", + status="CONTRACT_FAILED", + error=str(exc), ) - signature_hash = lean_theorem_signature_hash(source) + signature_hash = declaration.declaration_hash content = ( "import KakeyaLeanGate\n\n" "set_option autoImplicit false\n\n" - + source - + "\n" + + declaration.source + + "\n sorry\n" ) first = _run_lean( content, @@ -250,6 +892,11 @@ def validate_lean_signature( attempts=1, elapsed_s=total_elapsed, output=output, + normalized_source=declaration.source, + declaration_name=declaration.name, + binders=declaration.binders, + proposition=declaration.proposition, + proposition_hash=declaration.proposition_hash, ) run = _run_lean( content, @@ -272,6 +919,11 @@ def validate_lean_signature( attempts=attempts, elapsed_s=total_elapsed, output=output, + normalized_source=declaration.source, + declaration_name=declaration.name, + binders=declaration.binders, + proposition=declaration.proposition, + proposition_hash=declaration.proposition_hash, ) if run.returncode != 0: return LeanSignatureResult( @@ -283,6 +935,11 @@ def validate_lean_signature( attempts=attempts, elapsed_s=total_elapsed, output=output, + normalized_source=declaration.source, + declaration_name=declaration.name, + binders=declaration.binders, + proposition=declaration.proposition, + proposition_hash=declaration.proposition_hash, ) return LeanSignatureResult( source, @@ -292,6 +949,11 @@ def validate_lean_signature( attempts=attempts, elapsed_s=total_elapsed, output=output, + normalized_source=declaration.source, + declaration_name=declaration.name, + binders=declaration.binders, + proposition=declaration.proposition, + proposition_hash=declaration.proposition_hash, ) @@ -303,31 +965,15 @@ def validate_lean_proof( ) -> LeanSignatureResult: """Compile one complete theorem without sorry/admit or added axioms.""" source = source.strip() - if ( - not source - or len(source) > 12_000 - or _FORBIDDEN.search(source) - or re.search(r"\b(?:sorry|admit)\b", source) - ): - return LeanSignatureResult( - source, - "", - False, - status="UNSAFE_REJECTED", - error="Lean proof is empty, unsafe, oversized, or incomplete", - ) - declarations = re.findall( - r"^\s*theorem\s+([A-Za-z_][\w']*)", - source, - re.MULTILINE, - ) - if len(declarations) != 1 or not re.search(r"\s*:=\s*by\b", source): + try: + declaration = LEAN_SIGNATURE_CONTRACT.validate_proof(source) + except ValueError as exc: return LeanSignatureResult( source, "", False, - status="TYPECHECK_FAILED", - error="expected exactly one complete theorem declaration", + status="CONTRACT_FAILED", + error=str(exc), ) proof_hash = hashlib.sha256(source.encode()).hexdigest() run = _run_lean( @@ -346,6 +992,11 @@ def validate_lean_proof( error=f"Lean proof timed out after {timeout_s:.1f}s", elapsed_s=run.elapsed_s, output=run.output, + normalized_source=declaration.source, + declaration_name=declaration.name, + binders=declaration.binders, + proposition=declaration.proposition, + proposition_hash=declaration.proposition_hash, ) if run.returncode != 0: return LeanSignatureResult( @@ -356,6 +1007,11 @@ def validate_lean_proof( error=f"Lean proof failed: {run.output[-2000:]}", elapsed_s=run.elapsed_s, output=run.output, + normalized_source=declaration.source, + declaration_name=declaration.name, + binders=declaration.binders, + proposition=declaration.proposition, + proposition_hash=declaration.proposition_hash, ) return LeanSignatureResult( source, @@ -364,4 +1020,9 @@ def validate_lean_proof( status="PROVED", elapsed_s=run.elapsed_s, output=run.output, + normalized_source=declaration.source, + declaration_name=declaration.name, + binders=declaration.binders, + proposition=declaration.proposition, + proposition_hash=declaration.proposition_hash, ) diff --git a/autoresearch/prefill/live_status.py b/autoresearch/prefill/live_status.py new file mode 100644 index 0000000..395d97b --- /dev/null +++ b/autoresearch/prefill/live_status.py @@ -0,0 +1,492 @@ +"""Atomic, public-safe live execution status for proof orchestration.""" +from __future__ import annotations + +import fcntl +import json +import os +import re +import threading +import time +from pathlib import Path + + +SCHEMA_VERSION = 2 +VALID_STATES = { + "queued", + "prefill", + "decode", + "review", + "completed", + "failed", + "idle", +} +_SAFE_TEXT = re.compile(r"[^A-Za-z0-9_.:@+\- ]") + + +def _safe_text(value, limit: int = 160) -> str: + text = str(value or "") + if "/" in text or re.search( + r"(?i)(?:api[_ -]?key|secret|access[_ -]?token|prompt)\s*[:=]", + text, + ): + return "redacted" + return _SAFE_TEXT.sub("_", text)[:limit] + + +class AtomicLiveStatus: + """Write one status document via locked, permission-restricted replace.""" + + def __init__( + self, + path: Path, + *, + supervisor_pid: int, + iteration: int = 0, + run_id: str = "", + min_interval_s: float = 2.0, + ) -> None: + self.path = Path(path).expanduser() + self.supervisor_pid = int(supervisor_pid) + self.iteration = int(iteration) + self.run_id = _safe_text(run_id) + self.min_interval_s = float(min_interval_s) + self.writer_pid = os.getpid() + self._sequence = 0 + self._last_write = 0.0 + self._last_signature = None + self._lock = threading.Lock() + self._phase_started_at = time.time() + + def set_context( + self, + *, + iteration: int | None = None, + run_id: str | None = None, + ) -> None: + if iteration is not None: + self.iteration = int(iteration) + if run_id is not None: + self.run_id = _safe_text(run_id) + + def emit( + self, + *, + phase: str, + role: str = "", + state: str, + progress_current: int | None = None, + progress_total: int | None = None, + progress_unit: str = "", + active_obligation_id: str = "", + worker: str = "", + source: str = "", + hit_source: str = "", + force: bool = False, + ) -> bool: + if state not in VALID_STATES: + raise ValueError(f"invalid live status state: {state}") + now = time.time() + signature = ( + phase, + role, + state, + progress_current, + progress_total, + progress_unit, + active_obligation_id, + worker, + source, + hit_source, + self.iteration, + self.run_id, + ) + with self._lock: + phase_changed = ( + self._last_signature is None + or self._last_signature[:3] != signature[:3] + ) + if phase_changed: + self._phase_started_at = now + if ( + not force + and signature == self._last_signature + and now - self._last_write < self.min_interval_s + ): + return False + if ( + not force + and not phase_changed + and now - self._last_write < self.min_interval_s + ): + return False + self.path.parent.mkdir(parents=True, exist_ok=True, mode=0o700) + lock_path = self.path.with_suffix(self.path.suffix + ".lock") + with lock_path.open("a+", encoding="utf-8") as lock_handle: + os.chmod(lock_path, 0o600) + fcntl.flock(lock_handle.fileno(), fcntl.LOCK_EX) + try: + try: + existing = json.loads( + self.path.read_text(encoding="utf-8"), + ) + self._sequence = max( + self._sequence, + int(existing.get("sequence", 0)), + ) + except (OSError, ValueError, TypeError, json.JSONDecodeError): + pass + self._sequence += 1 + payload = { + "schema_version": SCHEMA_VERSION, + "supervisor_pid": self.supervisor_pid, + "writer_pid": self.writer_pid, + "run_id": self.run_id, + "iteration": self.iteration, + "phase": _safe_text(phase), + "role": _safe_text(role), + "state": state, + "progress": { + "current": ( + max(0, int(progress_current)) + if progress_current is not None else None + ), + "total": ( + max(0, int(progress_total)) + if progress_total is not None else None + ), + "unit": _safe_text(progress_unit, 32), + }, + "started_at": self._phase_started_at, + "updated_at": now, + "active_obligation_id": _safe_text( + active_obligation_id, + ), + "worker": _safe_text(worker), + "source": _safe_text(source), + "hit_source": _safe_text(hit_source), + "sequence": self._sequence, + } + orchestration_path = os.environ.get( + "KAKEYA_ORCHESTRATION_STATE_PATH", + "", + ) + if orchestration_path: + try: + orchestration = json.loads( + Path(orchestration_path).expanduser().read_text( + encoding="utf-8", + ), + ) + except (OSError, TypeError, ValueError, json.JSONDecodeError): + orchestration = {} + retry_counters = orchestration.get( + "retry_counters", + {}, + ) + current_state = _safe_text( + orchestration.get("state", ""), + ) + critic_ref = orchestration.get( + "validated_artifacts", + {}, + ).get("critic", {}) + resumed = bool( + orchestration.get("strategy_reused", False) + and current_state not in {"GENERATOR", "CRITIC"} + ) + adapter_status = _safe_text( + orchestration.get("adapter_status", ""), + ) + blocked_category = ( + adapter_status + or ( + "PROOF_BLOCKED" + if current_state == "BLOCKED" else "" + ) + ) + payload.update({ + "orchestration_state": current_state, + "active_role": _safe_text( + orchestration.get("current_role", role), + ), + "resume_origin": _safe_text( + orchestration.get("resume_origin", ""), + ), + "transition_reason": _safe_text( + orchestration.get( + "last_transition_reason", + "", + ), + ), + "retry_count": int( + retry_counters.get(current_state, 0), + ), + "decomposition_iteration": int( + orchestration.get( + "decomposition_iteration", + 0, + ), + ), + "viewpoint": _safe_text( + orchestration.get("viewpoint", ""), + ), + "synthesis_iteration": int( + orchestration.get("synthesis_iteration", 0), + ), + "candidate_count": int( + orchestration.get( + "definition_candidate_count", + orchestration.get("candidate_count", 0), + ), + ), + "selected_move": _safe_text( + orchestration.get("selected_move_id", ""), + ), + "candidate_set_hash": _safe_text( + orchestration.get("candidate_set_hash", ""), + ), + "ranking_hash": _safe_text( + orchestration.get("ranking_hash", ""), + ), + "theorem_card_count": len( + orchestration.get("theorem_card_ids", []), + ), + "stagnation_reason": _safe_text( + orchestration.get("stagnation_reason", ""), + ), + "definition_resolution": { + "action": ( + "RESOLVE_ONE_DEFINITION_QUERY" + if orchestration.get( + "current_definition_gap_id", "", + ) else "" + ), + "current_gap": _safe_text(orchestration.get( + "current_definition_gap_id", "", + )), + "candidate_count": int(orchestration.get( + "definition_candidate_count", 0, + )), + "lean_status": _safe_text(orchestration.get( + "lean_definition_status", "", + )), + "store_hash_delta": _safe_text( + orchestration.get( + "definition_store_hash_delta", "", + ), + 160, + ), + "environment_hash_delta": _safe_text( + orchestration.get( + "definition_environment_hash_delta", "", + ), + 160, + ), + "query_hash": _safe_text(orchestration.get( + "definition_query_hash", "", + )), + "source_statuses": { + _safe_text(key, 48): _safe_text(value, 48) + for key, value in orchestration.get( + "definition_source_statuses", {}, + ).items() + }, + "property_statuses": { + _safe_text(key, 80): { + _safe_text(prop, 80): _safe_text( + status, 24, + ) + for prop, status in values.items() + } + for key, values in orchestration.get( + "definition_property_statuses", {}, + ).items() + }, + "branch_count": len(orchestration.get( + "definition_branch_hashes", [], + )), + "exhaustion_hash": _safe_text( + orchestration.get( + "definition_exhaustion_hash", "", + ), + ), + "interface_hash": _safe_text( + orchestration.get( + "definition_interface_hash", "", + ), + ), + "backjump_target": _safe_text( + orchestration.get( + "definition_backjump_target", "", + ), + ), + }, + "mathematical_progress": { + key: int(value) + for key, value in orchestration.get( + "progress_vector", {}, + ).items() + }, + "stagnation_count": int(orchestration.get( + "semantic_stagnation_count", 0, + )), + "semantic_rejection": bool( + orchestration.get("semantic_rejection"), + ), + "novel_proposals": int( + orchestration.get("novel_proposals", 0), + ), + "architecture_version": int( + orchestration.get("architecture_version", 1), + ), + "active_gate": _safe_text( + orchestration.get("active_gate", ""), + ), + "adapter_status": _safe_text( + adapter_status, + ), + "blocked_category": _safe_text(blocked_category), + "blocked_reason": _safe_text( + orchestration.get("blocked_reason", ""), + ), + "resume_role": _safe_text( + orchestration.get("current_role", ""), + ), + "execution_state": state, + "execution_phase": _safe_text(phase), + "typed_ir_hash": _safe_text( + orchestration.get("typed_ir_hash", ""), + ), + "proposition_hash": _safe_text( + orchestration.get("proposition_hash", ""), + ), + "elaborated_theorem_id": _safe_text( + orchestration.get("elaborated_theorem_id", ""), + ), + "lean_contract_id": _safe_text( + orchestration.get("lean_contract_id", ""), + ), + "lean_contract_version": int( + orchestration.get("lean_contract_version", 0), + ), + "lean_symbol_table_id": _safe_text( + orchestration.get("lean_symbol_table_id", ""), + ), + "lean_symbol_table_version": int( + orchestration.get( + "lean_symbol_table_version", + 0, + ), + ), + "validated_formalizer_unit_hashes": { + _safe_text(key, 48): _safe_text(value, 80) + for key, value in orchestration.get( + "formalizer_unit_hashes", + {}, + ).items() + }, + "strategy_reused": bool( + orchestration.get("strategy_reused", False), + ), + "generator_reused": resumed, + "critic_reused": resumed and bool(critic_ref), + "critic_artifact_sha256": _safe_text( + critic_ref.get("sha256", ""), + ), + "critic_source_run_id": _safe_text( + critic_ref.get("source_run_id", ""), + ), + "strategy_tournament": { + "event_type": _safe_text(orchestration.get( + "strategy_event_type", "", + )), + "plans_total": len(orchestration.get( + "strategy_plan_ids", [], + )), + "plans_feasible": len(orchestration.get( + "feasible_strategy_plan_ids", [], + )), + "branches_killed": int(orchestration.get( + "branches_killed", 0, + )), + "selected_plan_id": _safe_text( + orchestration.get( + "selected_strategy_plan_id", "", + ), + ), + }, + "research_contract": { + "contract_id": _safe_text(orchestration.get( + "research_contract_id", "", + )), + "accepted": bool(orchestration.get( + "research_contract_id", "", + )), + "rejection_codes": [ + _safe_text(item, 64) + for item in orchestration.get( + "research_contract_rejection_codes", [], + ) + ], + }, + "proof_search": { + "actions_attempted": int(orchestration.get( + "lean_actions_attempted", 0, + )), + "actions_accepted": int(orchestration.get( + "lean_actions_accepted", 0, + )), + "subgoals_closed": int(orchestration.get( + "subgoals_closed", 0, + )), + "subgoals_remaining": int(orchestration.get( + "subgoals_remaining", 0, + )), + "new_definitions": int(orchestration.get( + "new_elaborated_definitions", 0, + )), + "new_lemmas": int(orchestration.get( + "new_elaborated_lemmas", 0, + )), + "accepted_children": int(orchestration.get( + "accepted_children", 0, + )), + "verified_counterexamples": int( + orchestration.get( + "verified_counterexamples", 0, + ), + ), + "tokens_per_accepted_step": ( + int(orchestration.get( + "proof_tokens_consumed", 0, + )) + / max(1, int(orchestration.get( + "lean_actions_accepted", 0, + ))) + ), + }, + }) + temporary = self.path.with_name( + f".{self.path.name}.{self.writer_pid}." + f"{threading.get_ident()}.tmp", + ) + try: + temporary.write_text( + json.dumps( + payload, + ensure_ascii=True, + separators=(",", ":"), + sort_keys=True, + ), + encoding="utf-8", + ) + os.chmod(temporary, 0o600) + os.replace(temporary, self.path) + os.chmod(self.path, 0o600) + finally: + temporary.unlink(missing_ok=True) + finally: + fcntl.flock(lock_handle.fileno(), fcntl.LOCK_UN) + self._last_signature = signature + self._last_write = now + return True diff --git a/autoresearch/prefill/math_ir.py b/autoresearch/prefill/math_ir.py new file mode 100644 index 0000000..b786b98 --- /dev/null +++ b/autoresearch/prefill/math_ir.py @@ -0,0 +1,871 @@ +"""Typed mathematical IR and deterministic host-owned Lean compiler.""" +from __future__ import annotations + +import hashlib +import json +import re +from dataclasses import asdict, dataclass, field +from enum import Enum +from typing import Iterable, Mapping + + +MATH_IR_VERSION = 3 +REGISTRY_VERSION = 3 +_IDENTIFIER = re.compile(r"[A-Za-z][A-Za-z0-9_]{0,63}\Z") +_RAW_SOURCE = re.compile( + r"```|:=\s*by|(?:^|\s)(?:theorem|lemma|import|axiom)\s+|" + r"\\(?:frac|sum|forall|exists|mathbb|text|begin|end)\b|\$", + re.IGNORECASE, +) + + +class GateStatus(str, Enum): + PASSED = "PASSED" + ADAPTER_BLOCKED = "ADAPTER_BLOCKED" + INTEGRATION_BLOCKED = "INTEGRATION_BLOCKED" + SEMANTIC_BACKJUMP = "SEMANTIC_BACKJUMP" + MATHEMATICAL_REJECTION = "MATHEMATICAL_REJECTION" + + +class TypedIRError(ValueError): + def __init__( + self, + code: str, + message: str, + *, + line: int = 0, + node_id: str = "", + owner: str = "decomposer", + status: GateStatus = GateStatus.INTEGRATION_BLOCKED, + ) -> None: + self.code = str(code) + self.line = int(line) + self.node_id = str(node_id) + self.owner = str(owner) + self.status = status + super().__init__( + f"{status.value}:{code}:owner={owner}:line={line}:" + f"node={node_id}:{message}" + ) + + +@dataclass(frozen=True) +class TypeSpec: + type_id: str + lean_name: str + + +@dataclass(frozen=True) +class SymbolSpec: + symbol_id: str + lean_name: str + argument_types: tuple[str, ...] + result_type: str + + +@dataclass(frozen=True) +class OperatorSpec: + operator_id: str + arity: int + argument_types: tuple[str, ...] + result_type: str + lean_token: str + + +TYPE_REGISTRY: dict[str, TypeSpec] = { + spec.type_id: spec for spec in ( + TypeSpec("Prop", "Prop"), + TypeSpec("Nat", "ℕ"), + TypeSpec("Int", "ℤ"), + TypeSpec("Real", "ℝ"), + TypeSpec("Complex", "ℂ"), + TypeSpec("NatToComplex", "ℕ → ℂ"), + TypeSpec("ComplexToComplex", "ℂ → ℂ"), + TypeSpec("NatToComplexFunction", "ℕ → ℂ → ℂ"), + TypeSpec("SetComplex", "Set ℂ"), + ) +} +SYMBOL_REGISTRY: dict[str, SymbolSpec] = { + spec.symbol_id: spec for spec in ( + SymbolSpec("density", "density", ("NatToComplex",), "Real"), + SymbolSpec( + "localConvergence", + "localConvergence", + ("NatToComplex", "Complex", "Int", "Real"), + "Prop", + ), + SymbolSpec( + "growthConstraint", + "growthConstraint", + ("ComplexToComplex", "Nat"), + "Prop", + ), + SymbolSpec("True", "True", (), "Prop"), + SymbolSpec("False", "False", (), "Prop"), + SymbolSpec( + "polesOutsideDisk", "polesOutsideDisk", + ("SetComplex", "Complex", "Real"), "Prop", + ), + SymbolSpec( + "localUniformConvergenceOnDisk", "localUniformConvergenceOnDisk", + ("NatToComplexFunction", "ComplexToComplex", "Complex", "Real"), + "Prop", + ), + SymbolSpec( + "termsHolomorphicOnDisk", "termsHolomorphicOnDisk", + ("NatToComplexFunction", "Complex", "Real"), "Prop", + ), + SymbolSpec( + "holomorphicSumOnDisk", "holomorphicSumOnDisk", + ("ComplexToComplex", "Complex", "Real"), "Prop", + ), + SymbolSpec( + "agreesWithSimplePoleOnPuncturedDisk", + "agreesWithSimplePoleOnPuncturedDisk", + ("ComplexToComplex", "Complex", "Complex", "Real"), "Prop", + ), + SymbolSpec("nonzeroComplex", "nonzeroComplex", ("Complex",), "Prop"), + SymbolSpec("positiveRadius", "positiveRadius", ("Real",), "Prop"), + ) +} +OPERATOR_REGISTRY: dict[str, OperatorSpec] = { + spec.operator_id: spec for spec in ( + OperatorSpec("not", 1, ("Prop",), "Prop", "¬"), + OperatorSpec("and", 2, ("Prop", "Prop"), "Prop", "∧"), + OperatorSpec("or", 2, ("Prop", "Prop"), "Prop", "∨"), + OperatorSpec("implies", 2, ("Prop", "Prop"), "Prop", "→"), + OperatorSpec("eq_real", 2, ("Real", "Real"), "Prop", "="), + OperatorSpec("gt_real", 2, ("Real", "Real"), "Prop", ">"), + OperatorSpec("lt_real", 2, ("Real", "Real"), "Prop", "<"), + OperatorSpec("ge_real", 2, ("Real", "Real"), "Prop", "≥"), + OperatorSpec("le_real", 2, ("Real", "Real"), "Prop", "≤"), + OperatorSpec("eq_nat", 2, ("Nat", "Nat"), "Prop", "="), + ) +} + + +@dataclass(frozen=True) +class Binder: + binder_id: str + type_id: str + + +@dataclass(frozen=True) +class ExprNode: + node_id: str + kind: str + ref: str + arguments: tuple[str, ...] = () + + +@dataclass(frozen=True) +class MathIR: + theorem_id: str + binders: tuple[Binder, ...] + nodes: tuple[ExprNode, ...] + premises: tuple[str, ...] + conclusion: str + dependency_ids: tuple[str, ...] = () + schema_version: int = MATH_IR_VERSION + registry_version: int = REGISTRY_VERSION + + +@dataclass(frozen=True) +class ValidatedMathIR: + math_ir: MathIR + node_types: Mapping[str, str] + content_hash: str + + +@dataclass(frozen=True) +class LeanCompilation: + theorem_id: str + declaration_source: str + declaration_hash: str + proposition_hash: str + math_ir_hash: str + imports_hash: str + + +@dataclass(frozen=True) +class ProofStep: + tactic_id: str + argument_ids: tuple[str, ...] = () + + +@dataclass(frozen=True) +class ProofPlan: + theorem_id: str + proposition_hash: str + steps: tuple[ProofStep, ...] + schema_version: int = 1 + + +@dataclass(frozen=True) +class TypedIRCandidate: + choice_id: str + transformation_id: str + summary_id: str + typed_payload: tuple[str, ...] + typed_ir_hash: str + candidate_hash: str + + +@dataclass(frozen=True) +class TypedIRCandidateRegistry: + target_ref: str + viewpoint: str + dependency_ids: tuple[str, ...] + candidates: tuple[TypedIRCandidate, ...] + registry_hash: str + + @property + def choices(self) -> tuple[str, ...]: + return tuple(candidate.choice_id for candidate in self.candidates) + + def resolve(self, choice_id: str) -> TypedIRCandidate: + for candidate in self.candidates: + if candidate.choice_id == choice_id: + return candidate + raise TypedIRError( + "INVALID_DECOMPOSITION_CHOICE", + f"choice {choice_id!r} is not in candidate registry {self.registry_hash}", + owner="decomposer", + status=GateStatus.ADAPTER_BLOCKED, + ) + + +TACTIC_REGISTRY: dict[str, tuple[int, str]] = { + "intro": (1, "intro {0}"), + "exact": (1, "exact {0}"), + "apply": (1, "apply {0}"), + "assumption": (0, "assumption"), + "constructor": (0, "constructor"), + "left": (0, "left"), + "right": (0, "right"), + "trivial": (0, "trivial"), + "contradiction": (0, "contradiction"), +} + + +_DECOMPOSITION_TEMPLATES: tuple[ + tuple[str, str, str, tuple[str, ...], tuple[str, ...], tuple[str, ...]], + ..., +] = ( + ( + "A", + "DENSITY_LOWER_BOUND", + "DENSITY_THRESHOLD_MOVE", + ("NatToComplex", "Real"), + ("density",), + ("gt_real",), + ( + "binder sequence NatToComplex", + "binder threshold Real", + "var sequenceNode sequence", + "var thresholdNode threshold", + "symbol densityNode density sequenceNode", + "op resultNode gt_real densityNode thresholdNode", + "conclusion resultNode", + ), + ), + ( + "B", + "LOCAL_CONVERGENCE_OBLIGATION", + "LOCAL_CONVERGENCE_MOVE", + ("NatToComplex", "Complex", "Int", "Real"), + ("localConvergence",), + (), + ( + "binder sequence NatToComplex", + "binder center Complex", + "binder index Int", + "binder radius Real", + "var sequenceNode sequence", + "var centerNode center", + "var indexNode index", + "var radiusNode radius", + "symbol resultNode localConvergence sequenceNode centerNode indexNode radiusNode", + "conclusion resultNode", + ), + ), + ( + "C", + "GROWTH_CONSTRAINT_OBLIGATION", + "GROWTH_CONSTRAINT_MOVE", + ("ComplexToComplex", "Nat"), + ("growthConstraint",), + (), + ( + "binder function ComplexToComplex", + "binder degree Nat", + "var functionNode function", + "var degreeNode degree", + "symbol resultNode growthConstraint functionNode degreeNode", + "conclusion resultNode", + ), + ), + ( + "D", + "LOCAL_TO_GROWTH_BRIDGE", + "REGISTERED_BRIDGE_MOVE", + ( + "NatToComplex", "Complex", "Int", "Real", + "ComplexToComplex", "Nat", + ), + ("localConvergence", "growthConstraint"), + ("implies",), + ( + "binder sequence NatToComplex", + "binder center Complex", + "binder index Int", + "binder radius Real", + "binder function ComplexToComplex", + "binder degree Nat", + "var sequenceNode sequence", + "var centerNode center", + "var indexNode index", + "var radiusNode radius", + "var functionNode function", + "var degreeNode degree", + "symbol localNode localConvergence sequenceNode centerNode indexNode radiusNode", + "symbol growthNode growthConstraint functionNode degreeNode", + "op resultNode implies localNode growthNode", + "conclusion resultNode", + ), + ), + ( + "CASE_SPLIT", + "CASE_SPLIT", + "CASE_PARTITION_MOVE", + (), + ("True", "False"), + ("or",), + ( + "symbol leftCase True", + "symbol rightCase False", + "op partition or leftCase rightCase", + "conclusion partition", + ), + ), + ( + "RESTRICT_DOMAIN", + "RESTRICT_DOMAIN", + "DISK_DOMAIN_RESTRICTION_MOVE", + ("Real",), + ("positiveRadius",), + (), + ( + "binder radius Real", + "var radiusNode radius", + "symbol restricted positiveRadius radiusNode", + "conclusion restricted", + ), + ), + ( + "REMOVE_IRRELEVANT_ASSUMPTION", + "REMOVE_IRRELEVANT_ASSUMPTION", + "ASSUMPTION_PRUNING_MOVE", + (), + ("True",), + (), + ( + "symbol reduced True", + "conclusion reduced", + ), + ), + ( + "HOLOMORPHIC_EXTENSION", + "HOLOMORPHIC_EXTENSION", + "LOCAL_HOLOMORPHIC_SUM_MOVE", + ("ComplexToComplex", "Complex", "Real"), + ("holomorphicSumOnDisk",), + (), + ( + "binder sum ComplexToComplex", + "binder center Complex", + "binder radius Real", + "var sumNode sum", + "var centerNode center", + "var radiusNode radius", + "symbol result holomorphicSumOnDisk sumNode centerNode radiusNode", + "conclusion result", + ), + ), + ( + "SINGULARITY_CONTRADICTION", + "SINGULARITY_CONTRADICTION", + "LOCAL_HOLOMORPHICITY_SPECIAL_CASE_LEMMA", + ( + "NatToComplexFunction", "ComplexToComplex", "SetComplex", + "Complex", "Real", + ), + ( + "polesOutsideDisk", "localUniformConvergenceOnDisk", + "termsHolomorphicOnDisk", "holomorphicSumOnDisk", + "agreesWithSimplePoleOnPuncturedDisk", "nonzeroComplex", + "positiveRadius", "False", + ), + (), + ( + "binder terms NatToComplexFunction", + "binder sum ComplexToComplex", + "binder poles SetComplex", + "binder center Complex", + "binder radius Real", + "binder residue Complex", + "var termsNode terms", + "var sumNode sum", + "var polesNode poles", + "var centerNode center", + "var radiusNode radius", + "var residueNode residue", + "symbol polesOutside polesOutsideDisk polesNode centerNode radiusNode", + "symbol localUniform localUniformConvergenceOnDisk termsNode sumNode centerNode radiusNode", + "symbol termsHolomorphic termsHolomorphicOnDisk termsNode centerNode radiusNode", + "symbol sumHolomorphic holomorphicSumOnDisk sumNode centerNode radiusNode", + "symbol poleAgreement agreesWithSimplePoleOnPuncturedDisk sumNode centerNode residueNode radiusNode", + "symbol residueNonzero nonzeroComplex residueNode", + "symbol radiusPositive positiveRadius radiusNode", + "symbol contradiction False", + "premise polesOutside", + "premise localUniform", + "premise termsHolomorphic", + "premise sumHolomorphic", + "premise poleAgreement", + "premise residueNonzero", + "premise radiusPositive", + "conclusion contradiction", + ), + ), +) + + +def build_decomposer_candidate_registry( + *, + target_ref: str, + viewpoint: str, + dependency_ids: Iterable[str] = (), + allowed_transformations: Iterable[str] | None = None, +) -> TypedIRCandidateRegistry: + """Build a finite host-owned menu; the model emits only one choice code.""" + dependencies = tuple(sorted({str(item) for item in dependency_ids if item})) + allowed = ( + {str(item) for item in allowed_transformations} + if allowed_transformations is not None + else {template[1] for template in _DECOMPOSITION_TEMPLATES} + ) + candidates: list[TypedIRCandidate] = [] + for ( + choice_id, + transformation_id, + summary_id, + required_types, + required_symbols, + required_operators, + body, + ) in _DECOMPOSITION_TEMPLATES: + if transformation_id not in allowed: + continue + if ( + any(item not in TYPE_REGISTRY for item in required_types) + or any(item not in SYMBOL_REGISTRY for item in required_symbols) + or any(item not in OPERATOR_REGISTRY for item in required_operators) + ): + continue + payload = (*body, *(f"dependency {item}" for item in dependencies)) + validated = validate_math_ir(parse_math_ir(payload)) + canonical = { + "choice_id": choice_id, + "transformation_id": transformation_id, + "summary_id": summary_id, + "target_ref": str(target_ref), + "viewpoint": str(viewpoint), + "dependency_ids": dependencies, + "typed_ir": asdict(validated.math_ir), + "typed_ir_hash": validated.content_hash, + } + candidate_hash = hashlib.sha256(json.dumps( + canonical, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + candidates.append(TypedIRCandidate( + choice_id, + transformation_id, + summary_id, + tuple(payload), + validated.content_hash, + candidate_hash, + )) + manifest = { + "target_ref": str(target_ref), + "viewpoint": str(viewpoint), + "dependency_ids": dependencies, + "candidates": [asdict(candidate) for candidate in candidates], + "math_registry_hash": registry_hash(), + } + manifest_hash = hashlib.sha256(json.dumps( + manifest, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + return TypedIRCandidateRegistry( + str(target_ref), + str(viewpoint), + dependencies, + tuple(candidates), + manifest_hash, + ) + + +def registry_hash() -> str: + payload = { + "version": REGISTRY_VERSION, + "types": [asdict(item) for item in TYPE_REGISTRY.values()], + "symbols": [asdict(item) for item in SYMBOL_REGISTRY.values()], + "operators": [asdict(item) for item in OPERATOR_REGISTRY.values()], + "tactics": TACTIC_REGISTRY, + } + return hashlib.sha256(json.dumps( + payload, sort_keys=True, separators=(",", ":"), + ).encode()).hexdigest() + + +def parse_math_ir( + lines: Iterable[str], + *, + theorem_id: str = "hostGeneratedTheorem", +) -> MathIR: + """Parse the registered line DSL; this is adapter work, not proof search.""" + binders: list[Binder] = [] + nodes: list[ExprNode] = [] + premises: list[str] = [] + conclusion = "" + dependencies: list[str] = [] + for line_number, raw in enumerate(lines, 1): + text = str(raw).strip() + if not text: + continue + if _RAW_SOURCE.search(text): + raise TypedIRError( + "RAW_SOURCE_FORBIDDEN", + "Math IR contains source-language or raw LaTeX syntax", + line=line_number, + status=GateStatus.ADAPTER_BLOCKED, + ) + parts = text.split() + command = parts[0] + try: + if command == "binder" and len(parts) == 3: + binders.append(Binder(parts[1], parts[2])) + elif command == "var" and len(parts) == 3: + nodes.append(ExprNode(parts[1], "var", parts[2])) + elif command == "symbol" and len(parts) >= 3: + nodes.append(ExprNode(parts[1], "symbol", parts[2], tuple(parts[3:]))) + elif command == "op" and len(parts) >= 3: + nodes.append(ExprNode(parts[1], "operator", parts[2], tuple(parts[3:]))) + elif command == "premise" and len(parts) == 2: + premises.append(parts[1]) + elif command == "conclusion" and len(parts) == 2: + if conclusion: + raise ValueError("duplicate conclusion") + conclusion = parts[1] + elif command == "dependency" and len(parts) == 2: + dependencies.append(parts[1]) + else: + raise ValueError("unknown command or wrong arity") + except ValueError as exc: + raise TypedIRError( + "MALFORMED_IR_LINE", str(exc), line=line_number, + status=GateStatus.ADAPTER_BLOCKED, + ) from exc + return MathIR( + theorem_id, + tuple(binders), + tuple(nodes), + tuple(premises), + conclusion, + tuple(dependencies), + ) + + +def _canonical_ir(math_ir: MathIR) -> bytes: + return json.dumps( + asdict(math_ir), + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode() + + +def validate_dependency_graph(graph: Mapping[str, Iterable[str]]) -> None: + visiting: set[str] = set() + visited: set[str] = set() + + def visit(item: str) -> None: + if item in visiting: + raise TypedIRError( + "DEPENDENCY_CYCLE", f"dependency cycle at {item}", + owner="decomposer", + status=GateStatus.SEMANTIC_BACKJUMP, + ) + if item in visited: + return + visiting.add(item) + for dependency in graph.get(item, ()): + if dependency not in graph: + raise TypedIRError( + "UNKNOWN_DEPENDENCY", + f"{item} references unknown dependency {dependency}", + owner="decomposer", + status=GateStatus.SEMANTIC_BACKJUMP, + ) + visit(str(dependency)) + visiting.remove(item) + visited.add(item) + + for node in graph: + visit(str(node)) + + +def validate_math_ir(math_ir: MathIR) -> ValidatedMathIR: + if math_ir.schema_version != MATH_IR_VERSION: + raise TypedIRError("STALE_IR_VERSION", "unsupported Math IR version") + if math_ir.registry_version != REGISTRY_VERSION: + raise TypedIRError("STALE_REGISTRY", "unsupported registry version") + if not _IDENTIFIER.fullmatch(math_ir.theorem_id): + raise TypedIRError("INVALID_THEOREM_ID", "invalid theorem ID") + binder_types: dict[str, str] = {} + for binder in math_ir.binders: + if not _IDENTIFIER.fullmatch(binder.binder_id): + raise TypedIRError("INVALID_BINDER", binder.binder_id) + if binder.binder_id in binder_types: + raise TypedIRError("DUPLICATE_BINDER", binder.binder_id) + if binder.type_id not in TYPE_REGISTRY: + raise TypedIRError( + "UNKNOWN_TYPE", binder.type_id, node_id=binder.binder_id, + owner="decomposer", status=GateStatus.SEMANTIC_BACKJUMP, + ) + binder_types[binder.binder_id] = binder.type_id + node_map: dict[str, ExprNode] = {} + for node in math_ir.nodes: + if not _IDENTIFIER.fullmatch(node.node_id) or node.node_id in node_map: + raise TypedIRError("INVALID_OR_DUPLICATE_NODE", node.node_id) + node_map[node.node_id] = node + node_types: dict[str, str] = {} + visiting: set[str] = set() + + def infer(node_id: str) -> str: + if node_id in node_types: + return node_types[node_id] + if node_id in visiting: + raise TypedIRError("EXPRESSION_CYCLE", "cyclic node", node_id=node_id) + try: + node = node_map[node_id] + except KeyError as exc: + raise TypedIRError( + "UNKNOWN_NODE", node_id, node_id=node_id, + owner="decomposer", status=GateStatus.SEMANTIC_BACKJUMP, + ) from exc + visiting.add(node_id) + if node.kind == "var": + if node.arguments or node.ref not in binder_types: + raise TypedIRError( + "BINDER_SCOPE", f"unknown binder {node.ref}", node_id=node_id, + owner="decomposer", status=GateStatus.SEMANTIC_BACKJUMP, + ) + result = binder_types[node.ref] + elif node.kind == "symbol": + try: + symbol = SYMBOL_REGISTRY[node.ref] + except KeyError as exc: + raise TypedIRError( + "UNKNOWN_SYMBOL", node.ref, node_id=node_id, + owner="decomposer", status=GateStatus.SEMANTIC_BACKJUMP, + ) from exc + actual = tuple(infer(argument) for argument in node.arguments) + if actual != symbol.argument_types: + raise TypedIRError( + "SYMBOL_TYPE_MISMATCH", + f"{node.ref} expects {symbol.argument_types}, got {actual}", + node_id=node_id, + owner="decomposer", + status=GateStatus.SEMANTIC_BACKJUMP, + ) + result = symbol.result_type + elif node.kind == "operator": + try: + operator = OPERATOR_REGISTRY[node.ref] + except KeyError as exc: + raise TypedIRError( + "UNKNOWN_OPERATOR", node.ref, node_id=node_id, + owner="decomposer", status=GateStatus.SEMANTIC_BACKJUMP, + ) from exc + if len(node.arguments) != operator.arity: + raise TypedIRError("OPERATOR_ARITY", node.ref, node_id=node_id) + actual = tuple(infer(argument) for argument in node.arguments) + if actual != operator.argument_types: + raise TypedIRError( + "OPERATOR_TYPE_MISMATCH", + f"{node.ref} expects {operator.argument_types}, got {actual}", + node_id=node_id, + owner="decomposer", + status=GateStatus.SEMANTIC_BACKJUMP, + ) + result = operator.result_type + else: + raise TypedIRError("UNKNOWN_NODE_KIND", node.kind, node_id=node_id) + visiting.remove(node_id) + node_types[node_id] = result + return result + + roots = (*math_ir.premises, math_ir.conclusion) + if not math_ir.conclusion: + raise TypedIRError("MISSING_CONCLUSION", "conclusion is required") + for root in roots: + if infer(root) != "Prop": + raise TypedIRError( + "NON_PROPOSITION_ROOT", root, node_id=root, + owner="decomposer", status=GateStatus.SEMANTIC_BACKJUMP, + ) + unreachable = set(node_map) - set(node_types) + if unreachable: + raise TypedIRError( + "UNREACHABLE_NODES", ", ".join(sorted(unreachable)), + owner="decomposer", status=GateStatus.SEMANTIC_BACKJUMP, + ) + return ValidatedMathIR( + math_ir, + node_types, + hashlib.sha256(_canonical_ir(math_ir)).hexdigest(), + ) + + +def _render_expr(node_id: str, node_map: Mapping[str, ExprNode]) -> str: + node = node_map[node_id] + if node.kind == "var": + return node.ref + if node.kind == "symbol": + symbol = SYMBOL_REGISTRY[node.ref] + if not node.arguments: + return symbol.lean_name + arguments = " ".join(f"({_render_expr(arg, node_map)})" for arg in node.arguments) + return f"{symbol.lean_name} {arguments}" + operator = OPERATOR_REGISTRY[node.ref] + rendered = [_render_expr(arg, node_map) for arg in node.arguments] + if operator.arity == 1: + return f"({operator.lean_token} {rendered[0]})" + return f"({rendered[0]} {operator.lean_token} {rendered[1]})" + + +def build_lean_declaration(validated: ValidatedMathIR) -> LeanCompilation: + """Deterministically build Lean; no model-authored source enters here.""" + math_ir = validated.math_ir + node_map = {node.node_id: node for node in math_ir.nodes} + binders = " ".join( + f"({binder.binder_id} : {TYPE_REGISTRY[binder.type_id].lean_name})" + for binder in math_ir.binders + ) + proposition_parts = [ + *(_render_expr(item, node_map) for item in math_ir.premises), + _render_expr(math_ir.conclusion, node_map), + ] + proposition = " → ".join(f"({item})" for item in proposition_parts) + declaration_core = f"theorem {math_ir.theorem_id}" + if binders: + declaration_core += f" {binders}" + declaration_core += f" : {proposition}" + source = declaration_core + " := by" + proposition_hash = hashlib.sha256(proposition.encode()).hexdigest() + declaration_hash = hashlib.sha256(declaration_core.encode()).hexdigest() + imports_hash = hashlib.sha256( + b"import KakeyaLeanGate\nset_option autoImplicit false" + ).hexdigest() + return LeanCompilation( + math_ir.theorem_id, + source, + declaration_hash, + proposition_hash, + validated.content_hash, + imports_hash, + ) + + +def verify_proposition_equivalence( + validated: ValidatedMathIR, + compilation: LeanCompilation, +) -> None: + rebuilt = build_lean_declaration(validated) + if ( + compilation.math_ir_hash != validated.content_hash + or compilation.proposition_hash != rebuilt.proposition_hash + or compilation.declaration_hash != rebuilt.declaration_hash + or compilation.declaration_source != rebuilt.declaration_source + ): + raise TypedIRError( + "PROPOSITION_HASH_MISMATCH", + "Math IR and Lean declaration are not content-equivalent", + status=GateStatus.INTEGRATION_BLOCKED, + owner="host_compiler", + ) + + +def parse_proof_plan( + lines: Iterable[str], + *, + theorem_id: str, + proposition_hash: str, +) -> ProofPlan: + steps: list[ProofStep] = [] + for line_number, raw in enumerate(lines, 1): + text = str(raw).strip() + if not text: + continue + if _RAW_SOURCE.search(text): + raise TypedIRError( + "RAW_PROOF_SOURCE_FORBIDDEN", "proof plan contains source syntax", + line=line_number, owner="proof_search", + status=GateStatus.ADAPTER_BLOCKED, + ) + parts = text.split() + tactic_id = parts[0] + try: + arity, _template = TACTIC_REGISTRY[tactic_id] + except KeyError as exc: + raise TypedIRError( + "UNSUPPORTED_TACTIC", tactic_id, line=line_number, + owner="proof_search", status=GateStatus.MATHEMATICAL_REJECTION, + ) from exc + arguments = tuple(parts[1:]) + if len(arguments) != arity: + raise TypedIRError( + "TACTIC_ARITY", tactic_id, line=line_number, + owner="proof_search", status=GateStatus.MATHEMATICAL_REJECTION, + ) + if any(not _IDENTIFIER.fullmatch(item) for item in arguments): + raise TypedIRError( + "UNSAFE_TACTIC_ARGUMENT", tactic_id, line=line_number, + owner="proof_search", status=GateStatus.ADAPTER_BLOCKED, + ) + steps.append(ProofStep(tactic_id, arguments)) + if not steps: + raise TypedIRError( + "EMPTY_PROOF_PLAN", "proof plan is empty", owner="proof_search", + status=GateStatus.MATHEMATICAL_REJECTION, + ) + return ProofPlan(theorem_id, proposition_hash, tuple(steps)) + + +def render_proof_plan(plan: ProofPlan, compilation: LeanCompilation) -> str: + if ( + plan.theorem_id != compilation.theorem_id + or plan.proposition_hash != compilation.proposition_hash + ): + raise TypedIRError( + "PROOF_TARGET_MISMATCH", "proof plan targets another proposition", + owner="proof_search", status=GateStatus.MATHEMATICAL_REJECTION, + ) + rendered = [] + for step in plan.steps: + arity, template = TACTIC_REGISTRY[step.tactic_id] + if len(step.argument_ids) != arity: + raise TypedIRError("TACTIC_ARITY", step.tactic_id) + rendered.append(" " + template.format(*step.argument_ids)) + return compilation.declaration_source + "\n" + "\n".join(rendered) diff --git a/autoresearch/prefill/orchestration_state.py b/autoresearch/prefill/orchestration_state.py new file mode 100644 index 0000000..4e37554 --- /dev/null +++ b/autoresearch/prefill/orchestration_state.py @@ -0,0 +1,1366 @@ +"""Crash-consistent, event-driven proof orchestration checkpoints.""" +from __future__ import annotations + +import hashlib +import json +import os +import time +from dataclasses import asdict, dataclass, field +from enum import Enum +from pathlib import Path +from typing import Any + + +SCHEMA_VERSION = 10 +ARCHITECTURE_VERSION = 8 +TYPED_ARCHITECTURE_MIN_VERSION = 7 +TYPED_IR_MIGRATION_EVENT = "typed_ir_host_constrained_selector_v2" +CREATIVE_DECOMPOSITION_MIGRATION_EVENT = ( + "creative_decomposition_synthesis_moves_v3" +) +STRATEGY_TOURNAMENT_MIGRATION_EVENT = ( + "strategy_tournament_stepwise_generator_v1" +) +REQUIRED_TYPED_CAPABILITIES = { + "typed_role_transport": True, + "host_owned_public_assumptions": True, + "explicit_restriction_moves": True, + "legacy_model_artifact_execution": False, + "journaled_checkpoint_changes": True, + "strategy_tournament": True, + "research_contract_gate": True, + "stepwise_lean_feedback": True, + "legacy_strategy_generator_execution": False, + "atomic_define_one_concept": True, + "mathematical_progress_invariant": True, + "autonomous_definition_resolution": True, + "legacy_definition_registry_execution": False, + "generic_definition_reframe_execution": False, +} + + +class CheckpointCompatibilityError(ValueError): + """A persisted architecture cannot be executed by this runtime.""" + + +def current_capability_manifest() -> dict[str, Any]: + """Return the authoritative, content-addressed runtime capability set.""" + from autoresearch.prefill.creative_decomposition import MOVE_REGISTRY_VERSION + from autoresearch.prefill.evidence_planner import PLANNER_VERSION + from autoresearch.prefill.host_compiler import HOST_COMPILER_VERSION + from autoresearch.prefill.research_contract import CONTRACT_VERSION + from autoresearch.prefill.stepwise_proof import PROOF_SEARCH_VERSION + from autoresearch.prefill.strategy_tournament import TOURNAMENT_VERSION + from autoresearch.prefill.math_ir import ( + MATH_IR_VERSION, + REGISTRY_VERSION, + registry_hash, + ) + from autoresearch.prefill.typed_transport import ( + TRANSPORT_VERSION, + registry_hash as transport_registry_hash, + ) + from autoresearch.prefill.definition_resolution import PROTOCOL_VERSION + + return { + "typed_transport_version": TRANSPORT_VERSION, + "typed_transport_registry_hash": transport_registry_hash(), + "math_ir_version": MATH_IR_VERSION, + "math_registry_version": REGISTRY_VERSION, + "math_registry_hash": registry_hash(), + "host_compiler_version": HOST_COMPILER_VERSION, + "move_registry_version": MOVE_REGISTRY_VERSION, + "evidence_planner_version": PLANNER_VERSION, + "strategy_tournament_version": TOURNAMENT_VERSION, + "research_contract_version": CONTRACT_VERSION, + "proof_search_version": PROOF_SEARCH_VERSION, + "atomic_definition_version": PROTOCOL_VERSION, + "capability_flags": dict(REQUIRED_TYPED_CAPABILITIES), + } + + +def _manifest_default(name: str): + return current_capability_manifest()[name] + + +class ProofState(str, Enum): + STRATEGY_TOURNAMENT = "STRATEGY_TOURNAMENT" + RESEARCH_CONTRACT_GATE = "RESEARCH_CONTRACT_GATE" + # Legacy names are deserialization markers only. Architecture 7 has no + # transition edges from them and dispatch rejects them. + NEEDS_STRATEGY = "NEEDS_STRATEGY" + GENERATOR = "GENERATOR" + CRITIC = "CRITIC" + DEFINITION_AUDITOR = "DEFINITION_AUDITOR" + COUNTEREXAMPLE_WORKER = "COUNTEREXAMPLE_WORKER" + SYNTHESIS = "SYNTHESIS" + REFRAME = "REFRAME" + DEFINITION_RESOLUTION = "DEFINITION_RESOLUTION" + PARENT_STATEMENT_UNDERSPECIFIED = "PARENT_STATEMENT_UNDERSPECIFIED" + DECOMPOSER = "DECOMPOSER" + MATH_IR_TRANSLATION = "MATH_IR_TRANSLATION" + HOST_TYPED_IR_GATE = "HOST_TYPED_IR_GATE" + LEAN_ELABORATION_GATE = "LEAN_ELABORATION_GATE" + PROOF_SEARCH = "PROOF_SEARCH" + # Source compatibility only; persisted values use the v2 state names. + FORMALIZER = "MATH_IR_TRANSLATION" + PROVER = "PROOF_SEARCH" + ADVERSARIAL_REVIEW = "ADVERSARIAL_REVIEW" + JUDGE = "JUDGE" + COMMIT = "COMMIT" + APPROACH_FAILED = "APPROACH_FAILED" + PREMISE_AUDIT = "PREMISE_AUDIT" + DECOMPOSITION_STAGNATED = "DECOMPOSITION_STAGNATED" + MATHEMATICAL_STAGNATION = "MATHEMATICAL_STAGNATION" + BLOCKED = "BLOCKED" + IDLE = "IDLE" + + +class BlockedEventType(str, Enum): + OPERATOR_UNBLOCK = "OPERATOR_UNBLOCK" + HOST_GATE_DEFECTS_BACKJUMP = "HOST_GATE_DEFECTS_BACKJUMP" + TARGET_BRANCH_CHANGE = "TARGET_BRANCH_CHANGE" + VALIDATED_EVIDENCE_BACKJUMP = "VALIDATED_EVIDENCE_BACKJUMP" + NEW_STRATEGY_TRIGGER = "NEW_STRATEGY_TRIGGER" + + +@dataclass(frozen=True) +class BlockedExitEvent: + event_id: str + event_type: str + reason: str + target_state: str + reset_role: str + metadata: dict[str, Any] = field(default_factory=dict) + created_at: float = field(default_factory=time.time) + schema_version: int = 1 + + @property + def typed_event(self) -> BlockedEventType: + return BlockedEventType(self.event_type) + + +ROLE_ORDER = ( + ProofState.DEFINITION_AUDITOR, + ProofState.COUNTEREXAMPLE_WORKER, + ProofState.DECOMPOSER, + ProofState.MATH_IR_TRANSLATION, + ProofState.HOST_TYPED_IR_GATE, + ProofState.LEAN_ELABORATION_GATE, + ProofState.PROOF_SEARCH, + ProofState.ADVERSARIAL_REVIEW, + ProofState.JUDGE, + ProofState.COMMIT, +) +ROLE_ARTIFACT_KEYS = { + ProofState.STRATEGY_TOURNAMENT: "strategy_tournament", + ProofState.RESEARCH_CONTRACT_GATE: "research_contract", + ProofState.DEFINITION_AUDITOR: "definition_auditor", + ProofState.COUNTEREXAMPLE_WORKER: "counterexample_worker", + ProofState.DECOMPOSER: "decomposer", + ProofState.MATH_IR_TRANSLATION: "math_ir_translator", + ProofState.PROOF_SEARCH: "proof_search", + ProofState.ADVERSARIAL_REVIEW: "adversarial_proponent", + ProofState.JUDGE: "judge", +} +ALLOWED_TRANSITIONS = { + ProofState.STRATEGY_TOURNAMENT: { + ProofState.RESEARCH_CONTRACT_GATE, ProofState.DECOMPOSER, + ProofState.DEFINITION_RESOLUTION, + ProofState.BLOCKED, + }, + ProofState.RESEARCH_CONTRACT_GATE: { + ProofState.DECOMPOSER, ProofState.MATH_IR_TRANSLATION, + ProofState.HOST_TYPED_IR_GATE, ProofState.STRATEGY_TOURNAMENT, + ProofState.PROOF_SEARCH, ProofState.BLOCKED, + }, + # Audit-only legacy states deliberately have no executable outgoing edge. + ProofState.NEEDS_STRATEGY: set(), + ProofState.GENERATOR: set(), + ProofState.CRITIC: set(), + ProofState.DEFINITION_AUDITOR: { + ProofState.DEFINITION_AUDITOR, ProofState.COUNTEREXAMPLE_WORKER, + ProofState.BLOCKED, + }, + ProofState.COUNTEREXAMPLE_WORKER: { + ProofState.COUNTEREXAMPLE_WORKER, ProofState.DECOMPOSER, + ProofState.SYNTHESIS, + ProofState.PREMISE_AUDIT, ProofState.BLOCKED, + }, + ProofState.SYNTHESIS: { + ProofState.SYNTHESIS, ProofState.DEFINITION_RESOLUTION, + ProofState.DECOMPOSER, + ProofState.BLOCKED, + }, + ProofState.REFRAME: set(), + ProofState.DEFINITION_RESOLUTION: { + ProofState.STRATEGY_TOURNAMENT, + ProofState.PARENT_STATEMENT_UNDERSPECIFIED, + ProofState.MATHEMATICAL_STAGNATION, + ProofState.PREMISE_AUDIT, + ProofState.BLOCKED, + }, + ProofState.PARENT_STATEMENT_UNDERSPECIFIED: { + ProofState.STRATEGY_TOURNAMENT, ProofState.PREMISE_AUDIT, + ProofState.BLOCKED, + }, + ProofState.DECOMPOSER: { + ProofState.DECOMPOSER, ProofState.MATH_IR_TRANSLATION, + ProofState.SYNTHESIS, ProofState.DEFINITION_RESOLUTION, + ProofState.DECOMPOSITION_STAGNATED, ProofState.MATHEMATICAL_STAGNATION, + ProofState.BLOCKED, + }, + ProofState.MATH_IR_TRANSLATION: { + ProofState.MATH_IR_TRANSLATION, ProofState.DECOMPOSER, + ProofState.HOST_TYPED_IR_GATE, + # Read-only v1 replay can traverse its recorded downstream edge. + ProofState.PROOF_SEARCH, + ProofState.BLOCKED, + }, + ProofState.HOST_TYPED_IR_GATE: { + ProofState.LEAN_ELABORATION_GATE, ProofState.DECOMPOSER, + ProofState.MATH_IR_TRANSLATION, ProofState.SYNTHESIS, + ProofState.STRATEGY_TOURNAMENT, + ProofState.BLOCKED, + }, + ProofState.LEAN_ELABORATION_GATE: { + ProofState.PROOF_SEARCH, ProofState.DECOMPOSER, + ProofState.MATH_IR_TRANSLATION, ProofState.STRATEGY_TOURNAMENT, + ProofState.BLOCKED, + }, + ProofState.PROOF_SEARCH: { + ProofState.PROOF_SEARCH, ProofState.DECOMPOSER, + ProofState.MATH_IR_TRANSLATION, + ProofState.ADVERSARIAL_REVIEW, ProofState.BLOCKED, + }, + ProofState.ADVERSARIAL_REVIEW: { + ProofState.ADVERSARIAL_REVIEW, ProofState.DECOMPOSER, + ProofState.MATH_IR_TRANSLATION, ProofState.HOST_TYPED_IR_GATE, + ProofState.LEAN_ELABORATION_GATE, ProofState.PROOF_SEARCH, + ProofState.JUDGE, + ProofState.BLOCKED, + }, + ProofState.JUDGE: { + ProofState.JUDGE, ProofState.DEFINITION_AUDITOR, + ProofState.COUNTEREXAMPLE_WORKER, ProofState.DECOMPOSER, + ProofState.MATH_IR_TRANSLATION, ProofState.HOST_TYPED_IR_GATE, + ProofState.LEAN_ELABORATION_GATE, ProofState.PROOF_SEARCH, + ProofState.ADVERSARIAL_REVIEW, ProofState.COMMIT, + ProofState.APPROACH_FAILED, ProofState.PREMISE_AUDIT, + ProofState.BLOCKED, + }, + ProofState.COMMIT: {ProofState.IDLE, ProofState.COMMIT}, + ProofState.APPROACH_FAILED: { + ProofState.STRATEGY_TOURNAMENT, ProofState.BLOCKED, + }, + ProofState.PREMISE_AUDIT: { + ProofState.PREMISE_AUDIT, + ProofState.STRATEGY_TOURNAMENT, ProofState.BLOCKED, + }, + ProofState.DECOMPOSITION_STAGNATED: { + ProofState.SYNTHESIS, ProofState.DEFINITION_RESOLUTION, + ProofState.DECOMPOSER, + ProofState.STRATEGY_TOURNAMENT, ProofState.BLOCKED, + }, + ProofState.MATHEMATICAL_STAGNATION: { + ProofState.DEFINITION_RESOLUTION, ProofState.STRATEGY_TOURNAMENT, + ProofState.BLOCKED, + }, + ProofState.BLOCKED: { + ProofState.BLOCKED, ProofState.STRATEGY_TOURNAMENT, + ProofState.RESEARCH_CONTRACT_GATE, + *ROLE_ORDER[:-1], + }, + ProofState.IDLE: { + ProofState.IDLE, ProofState.STRATEGY_TOURNAMENT, + ProofState.BLOCKED, + }, +} + + +@dataclass +class ArtifactRef: + role: str + sha256: str + schema_version: int + dependencies: list[str] + path: str + source_run_id: str + validated_at: float + + +@dataclass(frozen=True) +class HostGateDefect: + code: str + source_role: str + message: str + hard_invalid: bool = True + + +HOST_GATE_DEFECT_RULES = ( + ( + "UNVERIFIED_COUNTEREXAMPLE", + "counterexample_worker", + "claimed counterexample has no verified evidence", + False, + ), + ( + "REDUCTION_CONCLUSION_MISMATCH", + "formalizer", + "reduction theorem conclusion differs from exact parent proposition", + True, + ), + ( + "PARENT_SIGNATURE_INVALID", + "formalizer", + "parent signature failed:", + True, + ), + ( + "CHILD_SIGNATURE_INVALID", + "formalizer", + "child L1 signature failed:", + True, + ), + ( + "CYCLIC_OR_EQUIVALENT_CHILD", + "decomposer", + "child L1 rejected:", + True, + ), + ( + "REDUCTION_SIGNATURE_INVALID", + "formalizer", + "reduction theorem signature failed or changed", + True, + ), + ( + "REDUCTION_PROOF_INVALID", + "prover", + "complete reduction proof failed or targets another theorem", + True, + ), +) + + +def classify_host_gate_defects(errors: list[str]) -> list[HostGateDefect]: + """Classify exact host errors without collapsing their producer roles.""" + defects = [] + for error in errors: + normalized = " ".join(str(error).split()) + matches = [ + HostGateDefect(code, role, normalized, hard) + for code, role, marker, hard in HOST_GATE_DEFECT_RULES + if marker in normalized + ] + if len(matches) != 1: + raise ValueError(f"unclassified or ambiguous host-gate defect: {error}") + defects.append(matches[0]) + return defects + + +def earliest_invalid_role(defects: list[HostGateDefect]) -> ProofState: + hard_roles = { + state_for_role(defect.source_role) + for defect in defects + if defect.hard_invalid + } + for state in ROLE_ORDER: + if state in hard_roles: + return state + raise ValueError("host-gate recovery requires at least one hard defect") + + +@dataclass +class OrchestrationCheckpoint: + state: str = ProofState.STRATEGY_TOURNAMENT.value + target_obligation_id: str = "" + candidate_sha256: str = "" + strategy_sha256: str = "" + parent_statement_sha256: str = "" + parent_signature_sha256: str = "" + root_goal_sha256: str = "" + current_role: str = "strategy_tournament" + validated_artifacts: dict[str, ArtifactRef] = field(default_factory=dict) + retry_counters: dict[str, int] = field(default_factory=dict) + decomposition_iteration: int = 0 + synthesis_iteration: int = 0 + viewpoint: str = "" + viewpoints_tried: list[str] = field(default_factory=list) + semantic_rejection: dict[str, Any] = field(default_factory=dict) + decomposition_proposals: list[dict[str, Any]] = field(default_factory=list) + novel_proposals: int = 0 + mathematical_retries: int = 0 + formalizer_substate: str = "" + lean_contract_id: str = "" + lean_contract_version: int = 0 + lean_symbol_table_id: str = "" + lean_symbol_table_version: int = 0 + formalizer_unit_hashes: dict[str, str] = field(default_factory=dict) + last_transition_reason: str = "new-checkpoint" + resume_origin: str = "" + strategy_reused: bool = False + source_run_ids: list[str] = field(default_factory=list) + ledger_id: str = "" + ledger_version: int = 0 + orchestration_id: str = "" + commit_key: str = "" + committed: bool = False + blocked_reason: str = "" + last_failure_fingerprint: str = "" + identical_failure_count: int = 0 + last_blocked_event_id: str = "" + invalidated_artifacts: dict[str, dict[str, Any]] = field(default_factory=dict) + advisory_artifacts: dict[str, dict[str, Any]] = field(default_factory=dict) + reuse_map: dict[str, str] = field(default_factory=dict) + recovery_events: list[dict[str, Any]] = field(default_factory=list) + architecture_version: int = ARCHITECTURE_VERSION + typed_transport_version: int = field( + default_factory=lambda: _manifest_default("typed_transport_version"), + ) + typed_transport_registry_hash: str = field( + default_factory=lambda: _manifest_default("typed_transport_registry_hash"), + ) + math_ir_version: int = field( + default_factory=lambda: _manifest_default("math_ir_version"), + ) + math_registry_version: int = field( + default_factory=lambda: _manifest_default("math_registry_version"), + ) + math_registry_hash: str = field( + default_factory=lambda: _manifest_default("math_registry_hash"), + ) + host_compiler_version: int = field( + default_factory=lambda: _manifest_default("host_compiler_version"), + ) + move_registry_version: int = field( + default_factory=lambda: _manifest_default("move_registry_version"), + ) + evidence_planner_version: int = field( + default_factory=lambda: _manifest_default("evidence_planner_version"), + ) + strategy_tournament_version: int = field( + default_factory=lambda: _manifest_default("strategy_tournament_version"), + ) + research_contract_version: int = field( + default_factory=lambda: _manifest_default("research_contract_version"), + ) + proof_search_version: int = field( + default_factory=lambda: _manifest_default("proof_search_version"), + ) + atomic_definition_version: int = field( + default_factory=lambda: _manifest_default("atomic_definition_version"), + ) + capability_flags: dict[str, bool] = field( + default_factory=lambda: dict(REQUIRED_TYPED_CAPABILITIES), + ) + adapter_status: str = "" + typed_ir_hash: str = "" + lean_declaration_hash: str = "" + proposition_hash: str = "" + elaborated_theorem_id: str = "" + active_gate: str = "" + migration_event: str = "" + migration_snapshot: str = "" + scratchpad_refs: list[dict[str, Any]] = field(default_factory=list) + candidate_set_hash: str = "" + candidate_hashes: list[str] = field(default_factory=list) + candidate_count: int = 0 + ranking_hash: str = "" + ranked_candidate_ids: list[str] = field(default_factory=list) + selected_move_id: str = "" + evidence_gap_graph_hash: str = "" + proof_plan_hash: str = "" + proof_plan_id: str = "" + executable_plan_node_id: str = "" + plan_score_explanation: dict[str, int] = field(default_factory=dict) + theorem_card_ids: list[str] = field(default_factory=list) + theorem_card_index_hash: str = "" + stagnation_reason: str = "" + semantic_stagnation_count: int = 0 + protocol_error_count: int = 0 + public_assumptions_hash: str = "" + child_public_assumptions_hash: str = "" + reduction_public_assumptions_hash: str = "" + strategy_event_id: str = "" + strategy_event_type: str = "" + strategy_plan_ids: list[str] = field(default_factory=list) + feasible_strategy_plan_ids: list[str] = field(default_factory=list) + pareto_plan_ids: list[str] = field(default_factory=list) + selected_strategy_plan_id: str = "" + strategy_tournament_hash: str = "" + research_contract_id: str = "" + research_contract_hash: str = "" + research_contract_rejection_codes: list[str] = field(default_factory=list) + branches_killed: int = 0 + branch_history: dict[str, dict[str, Any]] = field(default_factory=dict) + lean_actions_attempted: int = 0 + lean_actions_accepted: int = 0 + subgoals_closed: int = 0 + subgoals_remaining: int = 0 + new_elaborated_definitions: int = 0 + new_elaborated_lemmas: int = 0 + accepted_children: int = 0 + verified_counterexamples: int = 0 + definitions_added: int = 0 + existing_definitions_resolved: int = 0 + lemmas_proved: int = 0 + progress_vector: dict[str, int] = field(default_factory=lambda: { + "definitions_added": 0, + "existing_definitions_resolved": 0, + "lemmas_proved": 0, + "accepted_children": 0, + "subgoals_closed": 0, + "verified_counterexamples": 0, + }) + progress_fingerprint: str = "" + forbidden_semantic_fingerprints: list[str] = field(default_factory=list) + current_definition_gap_id: str = "" + definition_candidate_count: int = 0 + lean_definition_status: str = "" + definition_store_hash: str = "" + definition_environment_hash: str = "" + definition_store_hash_delta: str = "" + definition_environment_hash_delta: str = "" + definition_query_hash: str = "" + definition_source_statuses: dict[str, str] = field(default_factory=dict) + definition_property_statuses: dict[str, dict[str, str]] = field(default_factory=dict) + definition_branch_hashes: list[str] = field(default_factory=list) + definition_exhaustion_hash: str = "" + definition_interface_hash: str = "" + definition_backjump_target: str = "" + proof_tokens_consumed: int = 0 + proof_search_state_path: str = "" + created_at: float = field(default_factory=time.time) + updated_at: float = field(default_factory=time.time) + schema_version: int = SCHEMA_VERSION + + @property + def proof_state(self) -> ProofState: + return ProofState(self.state) + + def transition( + self, + next_state: ProofState, + reason: str, + *, + source_run_id: str = "", + resume_origin: str = "", + strategy_reused: bool | None = None, + blocked_exit_event: BlockedExitEvent | None = None, + ) -> None: + current = self.proof_state + if current in { + ProofState.NEEDS_STRATEGY, + ProofState.GENERATOR, + ProofState.CRITIC, + }: + raise ValueError( + f"legacy architecture state is audit-only: {current.value}", + ) + if ( + current == ProofState.BLOCKED + and next_state != ProofState.BLOCKED + and blocked_exit_event is None + ): + raise ValueError( + "BLOCKED can be exited only by an explicit typed event", + ) + if current == ProofState.BLOCKED and next_state == ProofState.BLOCKED: + return + if next_state not in ALLOWED_TRANSITIONS[current]: + raise ValueError( + f"illegal proof transition {current.value}->{next_state.value}", + ) + self.state = next_state.value + self.current_role = next_state.value.lower() + self.last_transition_reason = str(reason) + self.resume_origin = str(resume_origin) + if blocked_exit_event is not None: + self.last_blocked_event_id = blocked_exit_event.event_id + self.blocked_reason = "" + if strategy_reused is not None: + self.strategy_reused = bool(strategy_reused) + if source_run_id and source_run_id not in self.source_run_ids: + self.source_run_ids.append(source_run_id) + self.updated_at = time.time() + + def retry(self, role: ProofState, reason: str, limit: int) -> bool: + if self.proof_state == ProofState.BLOCKED: + return False + artifact = self.validated_artifacts.get( + ROLE_ARTIFACT_KEYS.get(role, ""), + ) + fingerprint = hashlib.sha256( + json.dumps( + { + "state": role.value, + "artifact": artifact.sha256 if artifact else "", + "error": " ".join(str(reason).split()), + }, + sort_keys=True, + separators=(",", ":"), + ).encode(), + ).hexdigest() + if fingerprint == self.last_failure_fingerprint: + self.identical_failure_count += 1 + else: + self.last_failure_fingerprint = fingerprint + self.identical_failure_count = 1 + if self.identical_failure_count >= 2: + self.blocked_reason = ( + f"{role.value} identical state/artifact/error cycle: {reason}" + ) + self.transition(ProofState.BLOCKED, self.blocked_reason) + return False + count = self.retry_counters.get(role.value, 0) + 1 + self.retry_counters[role.value] = count + if count > limit: + self.blocked_reason = ( + f"{role.value} retry budget exhausted ({limit}): {reason}" + ) + self.transition(ProofState.BLOCKED, self.blocked_reason) + return False + self.transition(role, reason, resume_origin=role.value) + return True + + def adapter_blocked(self, reason: str, *, status: str) -> None: + """Record an out-of-machine adapter/infra stop without proof retries.""" + if status not in { + "ADAPTER_BLOCKED", "INFRASTRUCTURE_BLOCKED", "INTEGRATION_BLOCKED", + }: + raise ValueError("invalid adapter status") + self.adapter_status = status + self.blocked_reason = str(reason) + self.last_transition_reason = f"{status}:{reason}" + self.updated_at = time.time() + + def clear_adapter_blocked(self, reason: str = "adapter-recovered") -> None: + """Resume a quiescent adapter stop without consuming math retries.""" + self.adapter_status = "" + self.blocked_reason = "" + self.last_transition_reason = str(reason) + self.last_failure_fingerprint = "" + self.identical_failure_count = 0 + self.updated_at = time.time() + + def begin_decomposition_iteration( + self, + viewpoint: str, + reason: str, + ) -> None: + """Advance mathematical search without consuming protocol retries.""" + viewpoint = str(viewpoint).strip() + if not viewpoint: + raise ValueError("decomposition viewpoint must be non-empty") + self.decomposition_iteration += 1 + self.viewpoint = viewpoint + if viewpoint not in self.viewpoints_tried: + self.viewpoints_tried.append(viewpoint) + self.transition( + ProofState.DECOMPOSER, + reason, + resume_origin=ProofState.DECOMPOSER.value, + strategy_reused=True, + ) + + +def checkpoint_compatibility_errors( + checkpoint: OrchestrationCheckpoint, +) -> list[str]: + """Compare persisted executable capabilities with the runtime exactly.""" + if checkpoint.architecture_version < TYPED_ARCHITECTURE_MIN_VERSION: + return ["LEGACY_ARCHITECTURE_EXECUTION_DISABLED"] + expected = current_capability_manifest() + errors = [] + if checkpoint.architecture_version != ARCHITECTURE_VERSION: + errors.append( + "ARCHITECTURE_VERSION_MISMATCH:" + f"{checkpoint.architecture_version}!={ARCHITECTURE_VERSION}", + ) + if checkpoint.schema_version != SCHEMA_VERSION: + errors.append( + f"SCHEMA_VERSION_MISMATCH:{checkpoint.schema_version}!={SCHEMA_VERSION}", + ) + for name, value in expected.items(): + actual = getattr(checkpoint, name) + if actual != value: + errors.append(f"{name.upper()}_MISMATCH") + return errors + + +def require_typed_dispatch(checkpoint: OrchestrationCheckpoint) -> None: + """Fail closed unless this checkpoint has the complete typed capability.""" + errors = checkpoint_compatibility_errors(checkpoint) + if checkpoint.proof_state in { + ProofState.NEEDS_STRATEGY, + ProofState.GENERATOR, + ProofState.CRITIC, + }: + errors.append("LEGACY_STRATEGY_GENERATOR_EXECUTION_DISABLED") + if errors: + raise CheckpointCompatibilityError(";".join(errors)) + + +def integration_block_incompatible_checkpoint( + checkpoint: OrchestrationCheckpoint, +) -> bool: + """Persistable fail-closed state used at every runtime dispatch boundary.""" + errors = checkpoint_compatibility_errors(checkpoint) + if not errors: + return False + checkpoint.adapter_blocked( + "checkpoint capability incompatibility: " + ";".join(errors), + status="INTEGRATION_BLOCKED", + ) + return True + + +def apply_blocked_exit_event( + checkpoint: OrchestrationCheckpoint, + event: BlockedExitEvent, +) -> None: + if checkpoint.proof_state != ProofState.BLOCKED: + raise ValueError("blocked exit event requires BLOCKED checkpoint") + if not event.event_id or not event.reason.strip(): + raise ValueError("blocked exit event requires ID and reason") + event_type = event.typed_event + target = ProofState(event.target_state) + reset_role = ProofState(event.reset_role) + if reset_role != target: + raise ValueError("blocked event may reset only its target role") + if target not in ALLOWED_TRANSITIONS[ProofState.BLOCKED]: + raise ValueError("blocked event target is not permitted") + if ( + event_type == BlockedEventType.NEW_STRATEGY_TRIGGER + and target != ProofState.STRATEGY_TOURNAMENT + ): + raise ValueError( + "new strategy trigger must target STRATEGY_TOURNAMENT", + ) + required_metadata = { + BlockedEventType.HOST_GATE_DEFECTS_BACKJUMP: ( + "defects", + "invalidated_artifact_hashes", + "reuse_map", + ), + BlockedEventType.TARGET_BRANCH_CHANGE: ("target_or_branch",), + BlockedEventType.VALIDATED_EVIDENCE_BACKJUMP: ("evidence_sha256",), + BlockedEventType.NEW_STRATEGY_TRIGGER: ("strategy_trigger",), + }.get(event_type, ()) + if any(not event.metadata.get(key) for key in required_metadata): + raise ValueError(f"{event_type.value} missing required metadata") + if event_type == BlockedEventType.HOST_GATE_DEFECTS_BACKJUMP: + defects = classify_host_gate_defects([ + str(item["message"]) for item in event.metadata["defects"] + ]) + if target != earliest_invalid_role(defects): + raise ValueError("host-gate backjump target is not earliest invalid role") + invalidated = event.metadata["invalidated_artifact_hashes"] + for role, digest in invalidated.items(): + ref = checkpoint.validated_artifacts.get(role) + if ref is None or ref.sha256 != digest: + raise ValueError(f"invalidated artifact hash mismatch for {role}") + for role in invalidated: + ref = checkpoint.validated_artifacts.pop(role) + checkpoint.invalidated_artifacts[ref.sha256] = { + **asdict(ref), + "reason_codes": [ + defect.code for defect in defects + if defect.hard_invalid + ], + "event_id": event.event_id, + "audit_only": True, + } + counterexample = checkpoint.validated_artifacts.get( + "counterexample_worker", + ) + if counterexample is not None: + checkpoint.advisory_artifacts[counterexample.sha256] = { + **asdict(counterexample), + "verified": False, + "premise": False, + "public": False, + "certificate_gate": False, + "event_id": event.event_id, + } + checkpoint.reuse_map = { + str(role): str(digest) + for role, digest in event.metadata["reuse_map"].items() + } + checkpoint.recovery_events.append({ + "event_id": event.event_id, + "event_type": event.event_type, + "defect_codes": [defect.code for defect in defects], + "target_state": target.value, + "invalidated_artifact_hashes": dict(invalidated), + "reuse_map": dict(checkpoint.reuse_map), + "created_at": event.created_at, + }) + checkpoint.retry_counters[target.value] = 0 + checkpoint.last_failure_fingerprint = "" + checkpoint.identical_failure_count = 0 + checkpoint.transition( + target, + f"{event_type.value}:{event.reason}", + resume_origin=ProofState.BLOCKED.value, + strategy_reused=target != ProofState.STRATEGY_TOURNAMENT, + blocked_exit_event=event, + ) + + +def append_blocked_event_journal( + path: Path, + event: BlockedExitEvent, + *, + before_state: str, + after_state: str, +) -> None: + path = Path(path).expanduser() + path.parent.mkdir(parents=True, exist_ok=True, mode=0o700) + record = { + "kind": "blocked_exit_event", + "before_state": before_state, + "after_state": after_state, + **asdict(event), + } + encoded = ( + json.dumps(record, ensure_ascii=False, sort_keys=True) + "\n" + ).encode() + descriptor = os.open(path, os.O_APPEND | os.O_CREAT | os.O_WRONLY, 0o600) + try: + os.write(descriptor, encoded) + os.fsync(descriptor) + finally: + os.close(descriptor) + + +def append_checkpoint_change_journal( + path: Path, + checkpoint: OrchestrationCheckpoint, + *, + checkpoint_sha256: str, +) -> None: + """Durably record every attempted checkpoint replacement before commit.""" + path = Path(path).expanduser() + path.parent.mkdir(parents=True, exist_ok=True, mode=0o700) + blocked = bool( + checkpoint.proof_state == ProofState.BLOCKED + or checkpoint.adapter_status + ) + record = { + "kind": "blocked_transition" if blocked else "checkpoint_change", + "checkpoint_sha256": checkpoint_sha256, + "state": checkpoint.state, + "current_role": checkpoint.current_role, + "adapter_status": checkpoint.adapter_status, + "reason": ( + checkpoint.blocked_reason + if blocked else checkpoint.last_transition_reason + ), + "architecture_version": checkpoint.architecture_version, + "schema_version": checkpoint.schema_version, + "typed_transport_version": checkpoint.typed_transport_version, + "host_compiler_version": checkpoint.host_compiler_version, + "updated_at": checkpoint.updated_at, + } + encoded = ( + json.dumps(record, ensure_ascii=False, sort_keys=True) + "\n" + ).encode() + descriptor = os.open(path, os.O_APPEND | os.O_CREAT | os.O_WRONLY, 0o600) + try: + os.write(descriptor, encoded) + os.fsync(descriptor) + finally: + os.close(descriptor) + + +def sha256_text(value: str) -> str: + return hashlib.sha256(str(value).encode()).hexdigest() + + +def _serialize(checkpoint: OrchestrationCheckpoint) -> dict: + return asdict(checkpoint) + + +def save_checkpoint(path: Path, checkpoint: OrchestrationCheckpoint) -> None: + path = Path(path).expanduser() + path.parent.mkdir(parents=True, exist_ok=True, mode=0o700) + checkpoint.updated_at = time.time() + if checkpoint.decomposition_proposals: + persist_decomposition_novelty_manifest(path, checkpoint) + serialized = json.dumps( + _serialize(checkpoint), ensure_ascii=False, indent=2, + ) + checkpoint_hash = hashlib.sha256(serialized.encode()).hexdigest() + append_checkpoint_change_journal( + path.with_name("proof_orchestration.journal.jsonl"), + checkpoint, + checkpoint_sha256=checkpoint_hash, + ) + temporary = path.with_name(f".{path.name}.{os.getpid()}.tmp") + try: + temporary.write_text(serialized, encoding="utf-8") + os.chmod(temporary, 0o600) + os.replace(temporary, path) + os.chmod(path, 0o600) + finally: + temporary.unlink(missing_ok=True) + + +def decomposition_rejection_reason_code(reason: str) -> str: + """Encode repeated rejection prose without losing its semantic class.""" + text = " ".join(str(reason).lower().split()) + for marker, code in ( + ("semantic-signature-duplicate", "SEMANTIC_DUPLICATE"), + ("structural-signature-duplicate", "STRUCTURAL_DUPLICATE"), + ("bidirectionally entails ancestor", "CYCLIC_EQUIVALENT"), + ("not strictly simpler", "NOT_STRICTLY_SIMPLER"), + ("structural delta", "NO_STRUCTURAL_DELTA"), + ("disconnected child", "DISCONNECTED_CHILD"), + ("reduction", "FAILED_REDUCTION"), + ("definition", "DEFINITION_GAP"), + ): + if marker in text: + return code + return "OTHER" + + +def decomposition_novelty_manifest( + checkpoint: OrchestrationCheckpoint, +) -> dict[str, Any]: + """Build the complete deterministic audit index referenced by the prompt.""" + return { + "schema_version": 1, + "records": [{ + "proposal_sha256": str(item.get("proposal_sha256", "")), + "semantic_hash": str(item.get("semantic_hash", "")), + "structural_signature": str( + item.get("structural_signature", ""), + ), + "rejection_reasons": [ + str(reason) for reason in item.get("rejection_reasons", []) + ], + "rejection_reason_codes": [ + decomposition_rejection_reason_code(reason) + for reason in item.get("rejection_reasons", []) + ], + "viewpoint": str(item.get("viewpoint", "")), + "decomposition_iteration": int( + item.get("decomposition_iteration", 0), + ), + "source_run_id": str(item.get("source_run_id", "")), + } for item in checkpoint.decomposition_proposals], + "viewpoints_tried": list(checkpoint.viewpoints_tried), + } + + +def persist_decomposition_novelty_manifest( + checkpoint_path: Path, + checkpoint: OrchestrationCheckpoint, +) -> tuple[str, Path]: + """Persist a content-addressed exact history index for audit/retrieval.""" + payload = decomposition_novelty_manifest(checkpoint) + encoded = json.dumps( + payload, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode() + digest = hashlib.sha256(encoded).hexdigest() + archive_dir = ( + Path(checkpoint_path).expanduser().with_suffix(".semantic-proposals") + / "manifests" + ) + archive_dir.mkdir(parents=True, exist_ok=True, mode=0o700) + path = archive_dir / f"{digest}.json" + 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 digest, path + + +def compact_decomposition_novelty_ledger( + checkpoint: OrchestrationCheckpoint, + *, + max_entries: int = 2, +) -> dict[str, Any]: + """Return a fixed-size model view backed by an exact host-side manifest.""" + proposals = checkpoint.decomposition_proposals + retained = proposals[-max_entries:] + manifest = decomposition_novelty_manifest(checkpoint) + manifest_sha256 = hashlib.sha256(json.dumps( + manifest, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode()).hexdigest() + reason_counts: dict[str, int] = {} + for item in proposals: + for reason in item.get("rejection_reasons", []): + code = decomposition_rejection_reason_code(reason) + reason_counts[code] = reason_counts.get(code, 0) + 1 + return { + "manifest": f"sha256:{manifest_sha256}", + "count": len(proposals), + "novel": checkpoint.novel_proposals, + "reasons": dict(sorted(reason_counts.items())), + "viewpoints": { + "manifest": "sha256:" + hashlib.sha256(json.dumps( + checkpoint.viewpoints_tried, + ensure_ascii=False, + separators=(",", ":"), + ).encode()).hexdigest(), + "count": len(checkpoint.viewpoints_tried), + "base_ids": [ + viewpoint for viewpoint in checkpoint.viewpoints_tried + if not viewpoint.startswith("synthesized_host_failures_") + ][-7:], + "recent_ids": checkpoint.viewpoints_tried[-2:], + }, + "active_viewpoint": checkpoint.viewpoint, + "duplicate_gate": "semantic_hash+structural_signature", + "recent": [{ + "i": item.get("decomposition_iteration", 0), + "v": item.get("viewpoint", ""), + "p": str(item.get("proposal_sha256", ""))[:16], + "s": str(item.get("semantic_hash", ""))[:16], + "d": str(item.get("structural_signature", ""))[:16], + "r": [ + decomposition_rejection_reason_code(reason) + for reason in item.get("rejection_reasons", []) + ], + } for item in retained], + } + + +def archive_decomposition_rejection( + checkpoint_path: Path, + checkpoint: OrchestrationCheckpoint, + *, + proposal: dict[str, Any], + rejection_reasons: list[str], + semantic_hash: str, + structural_signature: str, + source_run_id: str, +) -> dict[str, Any]: + """Persist one rejected mathematical proposal as immutable audit evidence.""" + checkpoint_path = Path(checkpoint_path).expanduser() + encoded = json.dumps( + proposal, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode() + proposal_hash = hashlib.sha256(encoded).hexdigest() + archive_dir = checkpoint_path.with_suffix(".semantic-proposals") + archive_dir.mkdir(parents=True, exist_ok=True, mode=0o700) + archive_path = archive_dir / f"{proposal_hash}.json" + if not archive_path.exists(): + temporary = archive_path.with_name( + f".{archive_path.name}.{os.getpid()}.tmp", + ) + try: + temporary.write_bytes(encoded) + os.chmod(temporary, 0o600) + os.replace(temporary, archive_path) + finally: + temporary.unlink(missing_ok=True) + record = { + "proposal_sha256": proposal_hash, + "semantic_hash": str(semantic_hash), + "structural_signature": str(structural_signature), + "rejection_reasons": [str(item) for item in rejection_reasons], + "viewpoint": checkpoint.viewpoint, + "decomposition_iteration": checkpoint.decomposition_iteration, + "source_run_id": str(source_run_id), + "path": str(archive_path), + "audit_only": True, + "created_at": time.time(), + } + is_novel = not any( + item.get("semantic_hash") == semantic_hash + for item in checkpoint.decomposition_proposals + ) + checkpoint.decomposition_proposals.append(record) + if is_novel: + checkpoint.novel_proposals += 1 + checkpoint.semantic_rejection = dict(record) + checkpoint.updated_at = time.time() + save_checkpoint(checkpoint_path, checkpoint) + return record + + +def load_checkpoint(path: Path) -> OrchestrationCheckpoint | None: + path = Path(path).expanduser() + if not path.exists(): + return None + raw = json.loads(path.read_text(encoding="utf-8")) + if not isinstance(raw, dict): + raise ValueError("orchestration checkpoint must be an object") + legacy_schema = int(raw.get("schema_version", 1)) + legacy_architecture = int(raw.get("architecture_version", 1)) + legacy_state = str(raw.get("state", ProofState.NEEDS_STRATEGY.value)) + capability_fields = set(current_capability_manifest()) + missing_capability_fields = ( + capability_fields.difference(raw) + if ( + legacy_schema >= SCHEMA_VERSION + and int(raw.get("architecture_version", 1)) >= ARCHITECTURE_VERSION + ) + else set() + ) + if legacy_schema < SCHEMA_VERSION: + artifacts = raw.setdefault("validated_artifacts", {}) + invalidated = raw.setdefault("invalidated_artifacts", {}) + for role in ( + "strategy", + "generator", + "critic", + "synthesis", + "decomposer", + "formalizer_parent_signature", + "formalizer_child_signature", + "formalizer_reduction_signature", + "formalizer", + "prover", + "adversarial_proponent", + "judge", + ): + reference = artifacts.pop(role, None) + if reference: + invalidated[str(reference["sha256"])] = { + **reference, + "audit_only": True, + "reason_codes": ["LEGACY_MODEL_JSON_OR_LEAN"], + "migration_event": STRATEGY_TOURNAMENT_MIGRATION_EVENT, + } + if legacy_architecture < ARCHITECTURE_VERSION: + target = ( + ProofState.DEFINITION_RESOLUTION + if legacy_state == ProofState.REFRAME.value + else ProofState.STRATEGY_TOURNAMENT + ) + raw["state"] = target.value + raw["current_role"] = target.value.lower() + raw["resume_origin"] = legacy_state + raw["last_transition_reason"] = ( + "strategy-tournament-v1:legacy-strategy-generator-audit-only" + ) + raw["blocked_reason"] = "" + raw["migration_event"] = STRATEGY_TOURNAMENT_MIGRATION_EVENT + raw["architecture_version"] = ARCHITECTURE_VERSION + raw.update(current_capability_manifest()) + raw["adapter_status"] = "" + raw["formalizer_substate"] = "" + raw["lean_contract_id"] = "" + raw["lean_contract_version"] = 0 + raw["formalizer_unit_hashes"] = {} + raw["retry_counters"] = { + key: value for key, value in raw.get("retry_counters", {}).items() + if key not in {"FORMALIZER", "PROVER"} + } + removed_counter = "protocol_" + "attempt" + if isinstance(raw.get("semantic_rejection"), dict): + raw["semantic_rejection"].pop(removed_counter, None) + for proposal in raw.get("decomposition_proposals", []): + if isinstance(proposal, dict): + proposal.pop(removed_counter, None) + raw.setdefault("recovery_events", []).append({ + "event_type": "OPERATOR_MIGRATION", + "event_id": raw["migration_event"], + "from_schema": legacy_schema, + "to_schema": SCHEMA_VERSION, + "from_state": legacy_state, + "target_state": raw["state"], + "created_at": time.time(), + }) + # Migration defaults for pre-state-machine or early schema documents. + if legacy_schema < SCHEMA_VERSION: + raw["schema_version"] = SCHEMA_VERSION + else: + raw.setdefault("schema_version", SCHEMA_VERSION) + raw.setdefault("validated_artifacts", {}) + raw.setdefault("retry_counters", {}) + raw.setdefault("source_run_ids", []) + raw.setdefault("state", ProofState.STRATEGY_TOURNAMENT.value) + known = set(OrchestrationCheckpoint.__dataclass_fields__) + raw = {key: value for key, value in raw.items() if key in known} + raw["validated_artifacts"] = { + role: ArtifactRef(**value) + for role, value in raw["validated_artifacts"].items() + } + checkpoint = OrchestrationCheckpoint(**raw) + checkpoint.proof_state + if missing_capability_fields: + checkpoint.adapter_blocked( + "checkpoint capability incompatibility: " + "MISSING_CAPABILITY_FIELDS:" + + ",".join(sorted(missing_capability_fields)), + status="INTEGRATION_BLOCKED", + ) + else: + integration_block_incompatible_checkpoint(checkpoint) + return checkpoint + + +def binding_mismatch( + checkpoint: OrchestrationCheckpoint, + *, + target_obligation_id: str, + candidate_sha256: str, + parent_statement_sha256: str, + parent_signature_sha256: str, + root_goal_sha256: str, + ledger_id: str, + ledger_version: int, +) -> str: + expected = { + "target_obligation_id": target_obligation_id, + "candidate_sha256": candidate_sha256, + "parent_statement_sha256": parent_statement_sha256, + "parent_signature_sha256": parent_signature_sha256, + "root_goal_sha256": root_goal_sha256, + "ledger_id": ledger_id, + } + for field_name, value in expected.items(): + saved = str(getattr(checkpoint, field_name)) + if saved and saved != str(value): + return f"{field_name}-mismatch" + if checkpoint.ledger_version and checkpoint.ledger_version != ledger_version: + return "ledger-version-mismatch" + return "" + + +def persist_validated_artifact( + checkpoint_path: Path, + checkpoint: OrchestrationCheckpoint, + *, + role: str, + payload: dict[str, Any], + dependencies: list[str], + source_run_id: str, + artifact_schema_version: int = 1, +) -> ArtifactRef: + encoded = json.dumps( + payload, ensure_ascii=False, sort_keys=True, separators=(",", ":"), + ).encode() + digest = hashlib.sha256(encoded).hexdigest() + artifact_dir = checkpoint_path.with_suffix(".artifacts") + artifact_dir.mkdir(parents=True, exist_ok=True, mode=0o700) + artifact_path = artifact_dir / f"{digest}.json" + if not artifact_path.exists(): + temporary = artifact_path.with_name( + f".{artifact_path.name}.{os.getpid()}.tmp", + ) + try: + temporary.write_bytes(encoded) + os.chmod(temporary, 0o600) + os.replace(temporary, artifact_path) + finally: + temporary.unlink(missing_ok=True) + os.chmod(artifact_path, 0o600) + ref = ArtifactRef( + role=role, + sha256=digest, + schema_version=artifact_schema_version, + dependencies=list(dependencies), + path=str(artifact_path), + source_run_id=source_run_id, + validated_at=time.time(), + ) + checkpoint.validated_artifacts[role] = ref + save_checkpoint(checkpoint_path, checkpoint) + return ref + + +def load_validated_artifacts( + checkpoint: OrchestrationCheckpoint, +) -> dict[str, dict]: + loaded: dict[str, dict] = {} + hashes: dict[str, str] = {} + dependency_roles = { + "definition_auditor": (), + "counterexample_worker": ("definition_auditor",), + "decomposer": ("definition_auditor",), + "math_ir_translator": ("decomposer",), + "proof_search": ("math_ir_translator",), + "adversarial_proponent": ( + "decomposer", "math_ir_translator", "proof_search", + ), + } + for state in ROLE_ORDER: + role = ROLE_ARTIFACT_KEYS.get(state) + if role is None or role not in checkpoint.validated_artifacts: + break + ref = checkpoint.validated_artifacts[role] + dependencies_valid = ( + len(ref.dependencies) == 1 + if role == "judge" + else ref.dependencies == [ + hashes[name] for name in dependency_roles[role] + ] + ) + if ref.schema_version != 1 or not dependencies_valid: + raise ValueError(f"{role} artifact dependency mismatch") + path = Path(ref.path) + encoded = path.read_bytes() + if hashlib.sha256(encoded).hexdigest() != ref.sha256: + raise ValueError(f"{role} artifact hash mismatch") + payload = json.loads(encoded) + if not isinstance(payload, dict): + raise ValueError(f"{role} artifact schema mismatch") + loaded[role] = payload + hashes[role] = ref.sha256 + return loaded + + +def state_for_role(role: str) -> ProofState: + return { + "definition_auditor": ProofState.DEFINITION_AUDITOR, + "counterexample_worker": ProofState.COUNTEREXAMPLE_WORKER, + "decomposer": ProofState.DECOMPOSER, + "formalizer": ProofState.MATH_IR_TRANSLATION, + "math_ir_translator": ProofState.MATH_IR_TRANSLATION, + "prover": ProofState.PROOF_SEARCH, + "proof_search": ProofState.PROOF_SEARCH, + "adversarial_proponent": ProofState.ADVERSARIAL_REVIEW, + "judge": ProofState.JUDGE, + }[role] + + +def classify_failure(role: str, error: str) -> ProofState: + text = str(error).lower() + current = state_for_role(role) + if any(marker in text for marker in ( + "missing definition", "unknown constant", "unknown type", + "unknown symbol", "unknown operator", + )): + return ProofState.DEFINITION_RESOLUTION + if role in {"formalizer", "math_ir_translator"}: + return ProofState.MATH_IR_TRANSLATION + if role in {"prover", "proof_search"}: + if "type mismatch" in text or "signature" in text: + return ProofState.MATH_IR_TRANSLATION + return ProofState.PROOF_SEARCH + if role == "judge": + for marker, state in ( + ("definition", ProofState.DEFINITION_AUDITOR), + ("counterexample", ProofState.COUNTEREXAMPLE_WORKER), + ("decomposition", ProofState.DECOMPOSER), + ("formal", ProofState.MATH_IR_TRANSLATION), + ("proof", ProofState.PROOF_SEARCH), + ("defense", ProofState.ADVERSARIAL_REVIEW), + ): + if marker in text: + return state + if "premise" in text: + return ProofState.PREMISE_AUDIT + if "approach_failed" in text or "mathematical approach" in text: + return ProofState.APPROACH_FAILED + return current diff --git a/autoresearch/prefill/semantic_decompose.py b/autoresearch/prefill/semantic_decompose.py index a8562fa..c152962 100644 --- a/autoresearch/prefill/semantic_decompose.py +++ b/autoresearch/prefill/semantic_decompose.py @@ -3,9 +3,364 @@ import hashlib import json +import re from dataclasses import asdict, dataclass, field +DEFAULT_ARTIFACT_MAX_CHARS = 64 * 1024 + +STRUCTURED_ROLE_MINIMUM_OUTPUT_TOKENS = { + "premise_auditor": 256, + "premise_proponent": 256, + "definition_auditor": 384, + "counterexample_worker": 256, + "decomposer": 512, + "decomposer_scratchpad": 512, + "synthesis_scratchpad": 512, + "synthesis": 256, + "formalizer": 768, + "formalizer_parent_signature": 256, + "formalizer_child_signature": 256, + "formalizer_reduction_signature": 320, + "prover": 384, + "adversarial_proponent": 256, + "judge": 256, +} + + +@dataclass(frozen=True) +class ScannedArtifact: + json_text: str + start: int + end: int + + +def json_syntax_diagnostic(text: str, error: json.JSONDecodeError) -> str: + """Describe a transport-complete syntax failure without echoing full output.""" + radius = 18 + start = max(0, error.pos - radius) + end = min(len(text), error.pos + radius) + context = text[start:end].replace("\r", " ").replace("\n", " ") + context = re.sub(r"[^A-Za-z0-9_.,:{}\[\]\"' $\\:+\-]", "_", context) + return ( + "EOS-complete malformed JSON: " + f"{error.msg} at line {error.lineno} column {error.colno}; " + f"first syntax context {context!r}" + ) + + +@dataclass(frozen=True) +class StructuredArtifactContract: + role: str + heading: str | None + marker: str | None + required_fields: tuple[str, ...] + transport_stop: bool = True + + +STRUCTURED_ARTIFACT_CONTRACTS = { + "strategy": StructuredArtifactContract( + "strategy", + None, + None, + ( + "candidate_id", + "target_obligation_id", + "hypothesis", + "generator_directive", + "critic_directive", + "prefill_compute_chunk_tokens", + ), + ), + "premise_suspicion": StructuredArtifactContract( + "premise_suspicion", + None, + "Evidence artifact:", + ("claim",), + transport_stop=False, + ), + "premise_auditor": StructuredArtifactContract( + "premise_auditor", + "PREMISE_AUDIT", + "Artifact:", + ( + "status", + "evidence_type", + "evidence_source", + "confidence", + "artifact", + "analysis", + ), + ), + "premise_proponent": StructuredArtifactContract( + "premise_proponent", + "PREMISE_DEFENSE", + "Artifact:", + ("status", "correction", "failure_reason", "evidence"), + ), + "definition_auditor": StructuredArtifactContract( + "definition_auditor", + "DEFINITION_AUDIT", + "Artifact:", + ("definitions", "missing_definitions"), + ), + "counterexample_worker": StructuredArtifactContract( + "counterexample_worker", + "COUNTEREXAMPLE_REPORT", + "Artifact:", + ("status", "cases"), + ), + "decomposer": StructuredArtifactContract( + "decomposer", + "DECOMPOSITION_PROPOSAL", + "Artifact:", + ("parent_statement", "child", "public_assumptions", "reduction_contract"), + ), + "formalizer": StructuredArtifactContract( + "formalizer", + "FORMALIZATION_BUNDLE", + "Artifact:", + ( + "parent_signature", + "parent_newly_formalized", + "child_signature", + "reduction_signature", + ), + ), + "formalizer_parent_signature": StructuredArtifactContract( + "formalizer_parent_signature", + "LEAN_SIGNATURE_UNIT", + "Artifact:", + ( + "contract_id", + "contract_version", + "unit", + "kind", + "name", + "binders", + "proposition", + "source", + ), + ), + "formalizer_child_signature": StructuredArtifactContract( + "formalizer_child_signature", + "LEAN_SIGNATURE_UNIT", + "Artifact:", + ( + "contract_id", + "contract_version", + "unit", + "kind", + "name", + "binders", + "proposition", + "source", + ), + ), + "formalizer_reduction_signature": StructuredArtifactContract( + "formalizer_reduction_signature", + "LEAN_SIGNATURE_UNIT", + "Artifact:", + ( + "contract_id", + "contract_version", + "unit", + "kind", + "name", + "binders", + "proposition", + "source", + ), + ), + "prover": StructuredArtifactContract( + "prover", + "PROOF_ATTEMPT", + "Artifact:", + ("status", "reduction_theorem_source"), + ), + "adversarial_proponent": StructuredArtifactContract( + "adversarial_proponent", + "DEFENSE_REPORT", + "Artifact:", + ("status", "issues", "repairs"), + ), + "judge": StructuredArtifactContract( + "judge", + "JUDGE_DECISION", + "Artifact:", + ("decision", "reason"), + ), +} + + +def structured_contract(role: str) -> StructuredArtifactContract: + try: + return STRUCTURED_ARTIFACT_CONTRACTS[role] + except KeyError as exc: + raise ValueError(f"unregistered structured role: {role}") from exc + + +def structured_transport_complete(text: str, role: str) -> bool: + """Return true only at the registered contract's first object boundary.""" + contract = structured_contract(role) + if not contract.transport_stop: + return False + try: + if contract.heading is None: + scanned = scan_artifact_object_prefix(text, marker=contract.marker) + else: + scanned = scan_structured_artifact_prefix(text, contract.heading) + except ValueError: + return False + return bool(scanned is not None and not text[scanned.end:].strip()) + + +def lint_structured_prompt(prompt: str) -> None: + """Fail fast on conversational or syntactically invalid JSON contracts.""" + if ( + re.search(r'"[^"\n]*\|[^"\n]*"', prompt) + or re.search(r"\b[A-Z][A-Z_]*(?:\|[A-Z][A-Z_]*)+\b", prompt) + ): + raise ValueError("structured prompt contains an invalid union placeholder") + forbidden = ( + "prose after json", + "prose after the json", + "continue after the final }", + "follow the json with", + ) + lowered = prompt.casefold() + if any(item in lowered for item in forbidden): + raise ValueError("structured prompt permits prose after JSON") + + +def scan_artifact_object_prefix( + text: str, + *, + marker: str | None = "Artifact:", + max_chars: int = DEFAULT_ARTIFACT_MAX_CHARS, +) -> ScannedArtifact | None: + """Return the first balanced Artifact object, even if more text follows. + + This is a transport-boundary scanner, not an acceptance parser. It is + deliberately string/escape aware and tracks matching object/array + delimiters, but leaves JSON/schema/host validation to the strict parser. + """ + if not isinstance(text, str): + raise ValueError("structured response must be text") + if max_chars <= 0: + raise ValueError("artifact size cap must be > 0") + if marker is None: + start = 0 + else: + marker_index = text.find(marker) + if marker_index < 0: + return None + start = marker_index + len(marker) + while start < len(text) and text[start].isspace(): + start += 1 + if start >= len(text): + return None + if text[start] != "{": + raise ValueError("Artifact must start with a JSON object") + stack: list[str] = [] + in_string = False + escaped = False + matching = {"}": "{", "]": "["} + for index in range(start, len(text)): + if index - start >= max_chars: + raise ValueError("Artifact exceeds size cap") + char = text[index] + if in_string: + if escaped: + escaped = False + elif char == "\\": + escaped = True + elif char == '"': + in_string = False + continue + if char == '"': + in_string = True + elif char in "{[": + stack.append(char) + elif char in "}]": + if not stack or stack[-1] != matching[char]: + raise ValueError("unbalanced Artifact JSON") + stack.pop() + if not stack: + end = index + 1 + return ScannedArtifact(text[start:end], start, end) + if len(text) - start >= max_chars: + raise ValueError("Artifact exceeds size cap") + return None + + +def scan_structured_artifact_prefix( + text: str, + heading: str, + *, + max_chars: int = DEFAULT_ARTIFACT_MAX_CHARS, +) -> ScannedArtifact | None: + """Locate a transport-complete object after one exact heading and marker.""" + match = re.match( + rf"^\s*### {re.escape(heading)}[^\S\r\n]*\r?\n" + r"[^\S\r\n]*Artifact:[^\S\r\n]*", + text, + ) + if match is None: + return None + scanned = scan_artifact_object_prefix( + text[match.end():], + marker=None, + max_chars=max_chars, + ) + if scanned is None: + return None + return ScannedArtifact( + scanned.json_text, + match.end() + scanned.start, + match.end() + scanned.end, + ) + + +def scan_single_artifact_object( + text: str, + *, + marker: str | None = "Artifact:", + max_chars: int = DEFAULT_ARTIFACT_MAX_CHARS, +) -> ScannedArtifact: + """Locate exactly one bounded top-level JSON object after ``marker``. + + The scanner is string/escape aware, so braces in prose or LaTeX strings + do not affect balancing. Any non-whitespace after the object is rejected; + this prevents a second artifact or trailing text from changing meaning. + """ + if marker is not None: + marker_index = text.find(marker) + if marker_index < 0: + raise ValueError("missing Artifact marker") + if text.find(marker, marker_index + len(marker)) >= 0: + raise ValueError("multiple Artifact markers") + scanned = scan_artifact_object_prefix( + text, + marker=marker, + max_chars=max_chars, + ) + if scanned is None: + candidate_start = 0 + if marker is not None: + candidate_start = text.find(marker) + len(marker) + candidate = text[candidate_start:].strip() + if candidate.startswith("{") and candidate.endswith("}"): + try: + json.loads(candidate) + except json.JSONDecodeError as exc: + raise ValueError(json_syntax_diagnostic(candidate, exc)) from exc + raise ValueError("transport-incomplete Artifact JSON") + if text[scanned.end:].strip(): + raise ValueError("trailing text or second Artifact is forbidden") + return scanned + + class SemanticUnitTooLarge(ValueError): status = "SEMANTIC_UNIT_TOO_LARGE" @@ -43,6 +398,71 @@ def __init__( ) +class StructuredResponseBudgetTooSmall(SemanticUnitTooLarge): + status = "STRUCTURED_RESPONSE_BUDGET_TOO_SMALL" + + def __init__( + self, + role: str, + *, + retained_input_tokens: int, + available_tokens: int, + required_tokens: int, + max_retained_tokens: int, + control_reserve_tokens: int, + ) -> None: + self.role = role + self.retained_input_tokens = int(retained_input_tokens) + self.available_tokens = int(available_tokens) + self.required_tokens = int(required_tokens) + self.max_retained_tokens = int(max_retained_tokens) + self.control_reserve_tokens = int(control_reserve_tokens) + self.compaction_tokens_required = max( + 0, + self.required_tokens - self.available_tokens, + ) + ValueError.__init__( + self, + f"{self.status}: {role} retained_input={retained_input_tokens}, " + f"output_available={available_tokens}, " + f"minimum_complete_schema={required_tokens}, " + f"control_reserve={control_reserve_tokens}, " + f"max_retained={max_retained_tokens}; compact whole input fields " + f"by at least {self.compaction_tokens_required} tokens (semantic " + "units must not be truncated)", + ) + + +def repair_json_backslashes(value: str) -> str: + """Make literal model-emitted backslash runs valid JSON losslessly.""" + repaired = [] + index = 0 + while index < len(value): + if value[index] != "\\": + repaired.append(value[index]) + index += 1 + continue + end = index + while end < len(value) and value[end] == "\\": + end += 1 + count = end - index + next_text = value[end:] + valid_single_escape = ( + next_text.startswith('"') + or next_text.startswith("/") + or ( + next_text.startswith("u") + and len(next_text) >= 5 + and all(char in "0123456789abcdefABCDEF" for char in next_text[1:5]) + ) + ) + if count % 2 and not valid_single_escape: + count += 1 + repaired.append("\\" * count) + index = end + return "".join(repaired) + + @dataclass(frozen=True) class ProofStepInterface: root_goal_hash: str @@ -208,3 +628,43 @@ def downstream_output_cap( if configured_output_tokens is None or configured_output_tokens <= 0: return available return min(int(configured_output_tokens), available) + + +def structured_output_cap( + *, + role: str, + max_retained_tokens: int, + retained_input_tokens: int, + minimum_output_tokens: int, + configured_output_tokens: int | None, + control_reserve_tokens: int = 32, +) -> int: + """Budget a complete structured response from actual retained capacity.""" + available = ( + int(max_retained_tokens) + - int(retained_input_tokens) + - int(control_reserve_tokens) + ) + configured = ( + available + if configured_output_tokens is None or configured_output_tokens <= 0 + else min(available, int(configured_output_tokens)) + ) + if available < minimum_output_tokens or configured < minimum_output_tokens: + raise StructuredResponseBudgetTooSmall( + role, + retained_input_tokens=retained_input_tokens, + available_tokens=max(0, configured), + required_tokens=minimum_output_tokens, + max_retained_tokens=max_retained_tokens, + control_reserve_tokens=control_reserve_tokens, + ) + return configured + + +def structured_role_minimum_output_tokens(role: str) -> int: + """Return the reserved tokens for one complete compact role artifact.""" + try: + return STRUCTURED_ROLE_MINIMUM_OUTPUT_TOKENS[str(role)] + except KeyError as exc: + raise ValueError(f"unknown structured role: {role}") from exc diff --git a/autoresearch/prefill/typed_transport.py b/autoresearch/prefill/typed_transport.py new file mode 100644 index 0000000..fb12b69 --- /dev/null +++ b/autoresearch/prefill/typed_transport.py @@ -0,0 +1,524 @@ +"""Bounded, field-typed model transport whose values are wrapped by the host. + +The wire grammar is intentionally not JSON and has no model-visible artifact +metadata. A response is a sequence of registered field blocks: + + parent_claim_ref + + /parent_claim_ref + END + +Fields may repeat only when registered as repeated. Host bindings, versions, +hashes and persistence envelopes are added after this adapter succeeds. +""" +from __future__ import annotations + +import hashlib +import json +import re +from dataclasses import asdict, dataclass +from enum import Enum +from typing import Iterable, Mapping + + +TRANSPORT_VERSION = 4 +MAX_TRANSPORT_CHARS = 64 * 1024 +_FIELD_NAME = re.compile(r"[a-z][a-z0-9_]{0,47}\Z") +_IDENTIFIER = re.compile(r"[A-Za-z][A-Za-z0-9_]{0,63}\Z") +_REFERENCE = re.compile(r"[A-Za-z0-9][A-Za-z0-9_.:-]{0,255}\Z") +_FORBIDDEN_VALUE = re.compile( + r"```|(?:^|\s)(?:Artifact|schema_version)\s*:|" + r"(?:^|\s)(?:theorem|lemma)\s+\w+|:=\s*by|" + r"\\(?:frac|sum|forall|exists|mathbb|text|begin|end)\b|\$", + re.IGNORECASE | re.MULTILINE, +) + + +class AdapterStatus(str, Enum): + ADAPTER_BLOCKED = "ADAPTER_BLOCKED" + INFRASTRUCTURE_BLOCKED = "INFRASTRUCTURE_BLOCKED" + + +class AdapterError(ValueError): + """Transport failure outside the mathematical state machine.""" + + def __init__( + self, + code: str, + message: str, + *, + role: str, + field: str = "", + status: AdapterStatus = AdapterStatus.ADAPTER_BLOCKED, + ) -> None: + self.code = str(code) + self.role = str(role) + self.field = str(field) + self.status = status + super().__init__(f"{status.value}:{code}:{role}:{field}:{message}") + + +@dataclass(frozen=True) +class FieldSpec: + name: str + repeated: bool = False + required: bool = True + max_chars: int = 4096 + choices: tuple[str, ...] = () + value_kind: str = "identifier" + + def __post_init__(self) -> None: + if not _FIELD_NAME.fullmatch(self.name): + raise ValueError(f"invalid transport field name: {self.name}") + if self.max_chars <= 0: + raise ValueError("field max_chars must be positive") + if self.value_kind not in { + "enum", "identifier", "reference", "proof_step", + }: + raise ValueError(f"invalid transport value kind: {self.value_kind}") + if self.value_kind == "enum" and not self.choices: + raise ValueError(f"enum field has no registered choices: {self.name}") + + +@dataclass(frozen=True) +class RoleTransport: + role: str + fields: tuple[FieldSpec, ...] + version: int = TRANSPORT_VERSION + + def __post_init__(self) -> None: + names = [field.name for field in self.fields] + if not self.role or len(names) != len(set(names)): + raise ValueError(f"invalid role transport registry entry: {self.role}") + + +def _ref(name: str, **kwargs) -> FieldSpec: + return FieldSpec(name, value_kind="reference", max_chars=256, **kwargs) + + +def _id(name: str, **kwargs) -> FieldSpec: + return FieldSpec(name, value_kind="identifier", max_chars=64, **kwargs) + + +def _enum(name: str, choices: tuple[str, ...], **kwargs) -> FieldSpec: + return FieldSpec(name, choices=choices, value_kind="enum", max_chars=64, **kwargs) + + +ROLE_TRANSPORT_REGISTRY: dict[str, RoleTransport] = { + "strategy_tournament_selector": RoleTransport( + "strategy_tournament_selector", ( + _id("plan_id", repeated=True), + _enum("reason_code", ( + "MAXIMIZES_INFORMATION_GAIN", + "STRONGEST_THEOREM_SUPPORT", + "LOWEST_COMPLEXITY", + "LOWEST_RISK", + "STRICTEST_REDUCTION", + ), repeated=True), + )), + "strategy_critic_selector": RoleTransport( + "strategy_critic_selector", ( + _id("plan_id", repeated=True), + _enum("reason_code", ( + "MAXIMIZES_INFORMATION_GAIN", + "STRONGEST_THEOREM_SUPPORT", + "LOWEST_COMPLEXITY", + "LOWEST_RISK", + "STRICTEST_REDUCTION", + ), repeated=True), + )), + "synthesis": RoleTransport("synthesis", ( + _enum("choice_code", tuple("ABCDEFGHIJKLMNOPQRSTUVWXYZ")), + _enum("reason_code", ( + "DIRECT_LOCAL_CONTRADICTION", + "SUPPORTED_BY_THEOREM_CARDS", + "STRICTEST_REDUCTION", + "NOVEL_VIEWPOINT", + "LOWEST_COMPLEXITY", + "HIGHEST_GAP_COVERAGE", + "SHALLOWEST_DEPENDENCY_DEPTH", + )), + )), + "premise_suspicion": RoleTransport("premise_suspicion", ( + _ref("target_ref"), + _ref("evidence_ref"), + )), + "premise_auditor": RoleTransport("premise_auditor", ( + _ref("target_ref"), + _ref("evidence_ref", repeated=True), + _id("analysis_code", repeated=True, required=False), + _enum("status", ("CONFIRMED", "NOT_CONFIRMED", "INCONCLUSIVE")), + )), + "premise_proponent": RoleTransport("premise_proponent", ( + _ref("target_ref"), + _ref("correction_ref", required=False), + _ref("evidence_ref"), + _enum("status", ("RESCUED", "NOT_RESCUED", "INCONCLUSIVE")), + )), + "definition_auditor": RoleTransport("definition_auditor", ( + _ref("target_ref"), + _id("symbol_id", repeated=True, required=False), + _id("domain_id", repeated=True, required=False), + _id("topology_id", repeated=True, required=False), + _id("definition_id", repeated=True, required=False), + _id("missing_definition_id", repeated=True, required=False), + _enum("audit_outcome", ( + "COMPLETE", "MISSING_DEFINITION", "REFRAME_REQUIRED", + )), + )), + "counterexample_worker": RoleTransport("counterexample_worker", ( + _ref("target_ref"), + _ref("case_ref", repeated=True, required=False), + _enum("status", ( + "COUNTEREXAMPLE_FOUND", "NO_COUNTEREXAMPLE", "INCONCLUSIVE", + )), + )), + "decomposer": RoleTransport("decomposer", ( + _ref("parent_claim_ref"), + _enum("child_kind", ("DEFINITION", "LEMMA", "COROLLARY")), + _id("definition_id", repeated=True, required=False), + _ref("dependency_id", repeated=True, required=False), + _id("outline_step_id", repeated=True, required=False), + _enum("move_id", ("A", "B", "C", "D")), + )), + "math_ir_translator": RoleTransport("math_ir_translator", ( + _ref("parent_claim_ref"), + _enum("move_id", ("A", "B", "C", "D")), + )), + "proof_action_selector": RoleTransport("proof_action_selector", ( + _id("goal_id"), + _id("action_id"), + _id("operand_id", repeated=True, required=False), + _id("substitution_id", repeated=True, required=False), + )), + "adversarial_proponent": RoleTransport("adversarial_proponent", ( + _ref("target_proposition_ref"), + _id("issue_code", repeated=True, required=False), + _id("repair_step_id", repeated=True, required=False), + _enum("status", ("DEFENDED", "REJECTED", "INCONCLUSIVE")), + )), + "judge": RoleTransport("judge", ( + _ref("target_proposition_ref"), + _enum("decision", ("ACCEPT", "REJECT", "INCONCLUSIVE")), + _id("reason_code"), + )), +} + + +@dataclass(frozen=True) +class DecodedRoleFields: + role: str + values: Mapping[str, str | tuple[str, ...]] + transport_hash: str + + +def transport_prompt( + role: str, + *, + registered_choices: Mapping[str, Iterable[str]] | None = None, +) -> str: + """Return the only model-facing framing contract.""" + contract = resolve_transport(role) + lines = [ + "Return only bounded typed field records.", + "Each record is one line: field_name SPACE field_value SEMICOLON.", + "Repeat only fields marked repeatable. Finish with the exact line END;", + "Do not emit braces, quoted keys, invented metadata, fences, or source code.", + ] + for field in contract.fields: + qualifier = "required" if field.required else "optional" + if field.repeated: + qualifier += ", repeatable" + choice_registry = registered_choices or {} + choices = tuple(choice_registry.get(field.name, field.choices)) + if choices: + qualifier += "; choose exactly " + " or ".join(choices) + elif field.name in choice_registry: + qualifier += "; no registered choices; omit this field" + qualifier += f"; type {field.value_kind}" + lines.append(f"{field.name} ({qualifier})") + return "\n".join(lines) + + +def resolve_transport(role: str) -> RoleTransport: + try: + return ROLE_TRANSPORT_REGISTRY[str(role)] + except KeyError as exc: + raise AdapterError( + "UNREGISTERED_ROLE", + "role has no typed transport", + role=str(role), + ) from exc + + +def _validate_value( + role: str, + spec: FieldSpec, + value: str, + *, + choices: tuple[str, ...] | None = None, +) -> str: + if spec.name == "choice_code" and value != value.strip(): + raise AdapterError( + "INVALID_CHOICE", + "choice code must contain exactly one scoped character", + role=role, + field=spec.name, + ) + normalized = value.strip() + if not normalized: + raise AdapterError("EMPTY_FIELD", "field is empty", role=role, field=spec.name) + if len(normalized) > spec.max_chars: + raise AdapterError( + "FIELD_TOO_LARGE", + f"field exceeds {spec.max_chars} characters", + role=role, + field=spec.name, + ) + if _FORBIDDEN_VALUE.search(normalized): + raise AdapterError( + "MODEL_OWNED_SYNTAX", + "field contains forbidden envelope, Lean, fence, or raw LaTeX syntax", + role=role, + field=spec.name, + ) + allowed = spec.choices if choices is None else choices + if (allowed and normalized not in allowed) or ( + choices is not None and not allowed + ): + raise AdapterError( + "INVALID_CHOICE", + ( + f"expected one of {', '.join(allowed)}" + if allowed else "field has no registered choices and must be omitted" + ), + role=role, + field=spec.name, + ) + if spec.value_kind == "identifier" and not _IDENTIFIER.fullmatch(normalized): + raise AdapterError( + "INVALID_IDENTIFIER", "expected one registered DSL identifier", + role=role, field=spec.name, + ) + if spec.value_kind == "reference" and not _REFERENCE.fullmatch(normalized): + raise AdapterError( + "INVALID_REFERENCE", "expected one host content reference", + role=role, field=spec.name, + ) + if spec.value_kind == "proof_step": + from autoresearch.prefill.math_ir import TACTIC_REGISTRY + parts = normalized.split() + if ( + not parts + or parts[0] not in TACTIC_REGISTRY + or len(parts) - 1 != TACTIC_REGISTRY[parts[0]][0] + or any(not _IDENTIFIER.fullmatch(item) for item in parts[1:]) + ): + raise AdapterError( + "INVALID_PROOF_STEP", "expected registered tactic and identifier IDs", + role=role, field=spec.name, + ) + return normalized + + +def decode_role_fields( + text: str, + role: str, + *, + registered_choices: Mapping[str, Iterable[str]] | None = None, +) -> DecodedRoleFields: + """Decode one complete response without mutating proof state.""" + contract = resolve_transport(role) + if not isinstance(text, str): + raise AdapterError("NOT_TEXT", "response is not text", role=role) + if len(text) > MAX_TRANSPORT_CHARS: + raise AdapterError("RESPONSE_TOO_LARGE", "response exceeds cap", role=role) + lines = text.replace("\r\n", "\n").split("\n") + while lines and not lines[-1]: + lines.pop() + specs = {field.name: field for field in contract.fields} + decoded: dict[str, list[str]] = {} + compact = bool(lines) and all( + not line.strip() + or line.strip() == "END;" + or ( + line.strip().endswith(";") + and len(line.strip().split(maxsplit=1)) == 2 + ) + for line in lines + ) + if compact: + saw_end = False + for index, raw_line in enumerate(lines): + line = raw_line.strip() + if not line: + continue + if line == "END;": + saw_end = True + if any(item.strip() for item in lines[index + 1:]): + raise AdapterError( + "TRAILING_DATA", "tokens follow END", role=role, + ) + break + marker, raw_value = line[:-1].split(maxsplit=1) + if marker not in specs: + raise AdapterError( + "UNKNOWN_FIELD", + f"unknown field {marker!r}", + role=role, + field=marker, + ) + spec = specs[marker] + values = decoded.setdefault(marker, []) + if values and not spec.repeated: + raise AdapterError( + "DUPLICATE_FIELD", + "field is not repeatable", + role=role, + field=marker, + ) + choices = ( + tuple(registered_choices[marker]) + if registered_choices is not None and marker in registered_choices + else None + ) + values.append(_validate_value( + role, spec, raw_value, choices=choices, + )) + if not saw_end: + raise AdapterError("INCOMPLETE", "missing END", role=role) + return _finish_decoded(role, contract, decoded) + index = 0 + saw_end = False + while index < len(lines): + marker = lines[index].strip() + index += 1 + if marker == "END": + saw_end = True + if any(line.strip() for line in lines[index:]): + raise AdapterError( + "TRAILING_DATA", "tokens follow END", role=role, + ) + break + if marker not in specs: + raise AdapterError( + "UNKNOWN_FIELD", f"unknown field {marker!r}", role=role, field=marker, + ) + closing = f"/{marker}" + value_lines: list[str] = [] + while index < len(lines) and lines[index].strip() != closing: + if lines[index].strip() == "END": + raise AdapterError( + "UNCLOSED_FIELD", "END occurred inside field", role=role, + field=marker, + ) + value_lines.append(lines[index]) + index += 1 + if index >= len(lines): + raise AdapterError( + "UNCLOSED_FIELD", f"missing {closing}", role=role, field=marker, + ) + index += 1 + spec = specs[marker] + values = decoded.setdefault(marker, []) + if values and not spec.repeated: + raise AdapterError( + "DUPLICATE_FIELD", "field is not repeatable", role=role, field=marker, + ) + choices = ( + tuple(registered_choices[marker]) + if registered_choices is not None and marker in registered_choices + else None + ) + values.append(_validate_value( + role, spec, "\n".join(value_lines), choices=choices, + )) + if not saw_end: + raise AdapterError("INCOMPLETE", "missing END", role=role) + return _finish_decoded(role, contract, decoded) + + +def _finish_decoded( + role: str, + contract: RoleTransport, + decoded: Mapping[str, list[str]], +) -> DecodedRoleFields: + missing = [ + field.name for field in contract.fields + if field.required and not decoded.get(field.name) + ] + if missing: + raise AdapterError( + "MISSING_FIELDS", ", ".join(missing), role=role, + ) + values: dict[str, str | tuple[str, ...]] = {} + for spec in contract.fields: + items = decoded.get(spec.name, []) + values[spec.name] = tuple(items) if spec.repeated else (items[0] if items else "") + canonical = json.dumps( + {"role": role, "values": values, "transport_version": contract.version}, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode() + return DecodedRoleFields(role, values, hashlib.sha256(canonical).hexdigest()) + + +def typed_transport_complete(text: str, role: str) -> bool: + """Streaming stop predicate; acceptance still requires full decode.""" + if not isinstance(text, str) or len(text) > MAX_TRANSPORT_CHARS: + return False + if not re.search(r"(?:^|\n)END;?\s*\Z", text): + return False + try: + decode_role_fields(text, role) + except AdapterError: + return False + return True + + +def host_artifact( + decoded: DecodedRoleFields, + *, + host_bindings: Mapping[str, object], + dependencies: Iterable[str], +) -> dict[str, object]: + """Create the JSON-persisted envelope exclusively on the host.""" + payload = { + "schema_version": TRANSPORT_VERSION, + "producer_role": decoded.role, + "transport_hash": decoded.transport_hash, + "dependencies": list(dependencies), + "fields": dict(decoded.values), + "bindings": dict(host_bindings), + } + payload["content_hash"] = hashlib.sha256(json.dumps( + payload, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode()).hexdigest() + return payload + + +def registry_manifest() -> dict[str, object]: + return { + role: { + "version": contract.version, + "fields": [asdict(field) for field in contract.fields], + } + for role, contract in sorted(ROLE_TRANSPORT_REGISTRY.items()) + } + + +def registry_hash() -> str: + """Content address the executable typed transport registry.""" + return hashlib.sha256(json.dumps( + { + "transport_version": TRANSPORT_VERSION, + "roles": registry_manifest(), + }, + ensure_ascii=False, + sort_keys=True, + separators=(",", ":"), + ).encode()).hexdigest() diff --git a/tests/inference_engine/bench/test_lean_signature_gate.py b/tests/inference_engine/bench/test_lean_signature_gate.py index ab3566e..443cab5 100644 --- a/tests/inference_engine/bench/test_lean_signature_gate.py +++ b/tests/inference_engine/bench/test_lean_signature_gate.py @@ -1,39 +1,151 @@ from pathlib import Path +import json + +import pytest import autoresearch.prefill.lean_gate as lean_gate from autoresearch.prefill.lean_gate import ( - extract_lean_signature_blocks, + LEAN_CONTRACT_USER_REGISTRY, + LEAN_CONTRACT_REGISTRY, + LEAN_SIGNATURE_CONTRACT, + LEAN_SIGNATURE_FIXTURES, + lean_signature_contract_ref, + lean_symbol_semantic_hash, + lint_lean_model_prompt, + normalize_lean_signature, + normalize_registered_latex_identifiers, + register_lean_symbol_table, + resolve_lean_contract, + resolve_lean_symbol_table, + validate_lean_proof, validate_lean_signature, ) ROOT = Path(__file__).resolve().parents[3] +LATEST_PARENT_FAILURE = ( + "**The Density-Singularity Gap Lemma:** Prove that for a given " + "$\\epsilon$ and a fixed genus $p$, there exists a critical density." +) +LATEST_CHILD_FAILURE = ( + "theorem L1_definition : ∀ (z_n : ℕ → ℂ), True" +) +LATEST_REDUCTION_FAILURE = ( + "ba31be416856d1f975f8f885f54d9babde1aada7ee98d42341c3b58cad91a061" +) +LATEST_LATEX_PARENT_SOURCE = ( + r"theorem parent_537f9def407e " + r"(\epsilon : \mathbb{R}_{>0}) (p : \mathbb{N}) " + r"(\rho_c : \mathbb{R}) (\{z_n\} : \mathbb{N} \to \mathbb{C}) " + r"(s_0 : \mathbb{C}) (m : \mathbb{C}) " + r"(\delta : \mathbb{R}_{>0}) : \rho > \rho_c \implies " + r"\neg (\sum_{n=1}^{\infty} \frac{1}{s-z_n} = " + r"\frac{m}{s-s_0} \text{ in a } \delta\text{-neighborhood of } " + r"s_0 \implies \text{growth_order}(f) \le p) := by" +) + + +@pytest.mark.parametrize( + ("fixture", "source", "error"), + [ + ("zero_declarations", "", "empty Lean declaration"), + ( + "multiple_declarations", + "theorem one : True := by\ntheorem two : True := by", + "exactly one", + ), + ( + "prose", + "Here is Lean:\ntheorem one : True := by", + "only one theorem", + ), + ( + "fence", + "```lean\ntheorem one : True := by\n```", + "fences", + ), + ("def", "def one : Prop := True", "forbidden Lean command"), + ( + "forbidden_command", + "import Mathlib\ntheorem one : True := by", + "forbidden Lean command", + ), + ( + "missing_scaffold", + "theorem one : True", + "must end with `:= by`", + ), + ( + "duplicate_scaffold", + "theorem one : True := by := by", + "duplicate", + ), + ( + "proof_body", + "theorem one : True := by trivial", + "no proof body", + ), + ( + "placeholder", + "theorem one : True := by sorry", + "placeholder", + ), + ( + "latex_escape", + r"theorem one (x : \mathbb{R}) : True := by", + "LaTeX", + ), + ( + "latest_parent_prose", + LATEST_PARENT_FAILURE, + "LaTeX", + ), + ( + "latest_child_missing_scaffold", + LATEST_CHILD_FAILURE, + "must end with `:= by`", + ), + ( + "latest_reduction_hash", + LATEST_REDUCTION_FAILURE, + "exactly one", + ), + ], +) +def test_signature_contract_rejects_required_fixtures(fixture, source, error): + assert fixture in LEAN_SIGNATURE_FIXTURES + result = validate_lean_signature(source, project_root=ROOT) + assert not result.ok + assert result.status == "CONTRACT_FAILED" + assert error.casefold() in result.error.casefold() + -def test_extract_and_typecheck_minimal_mathlib_signature(): - text = """ -### LEAN_SIGNATURE RH-C2-leaf -```lean -theorem local_pole_signature - (f : ℂ → ℂ) - (h : Continuous f) : - Continuous f := by - sorry -``` -""" - blocks = extract_lean_signature_blocks(text) - assert len(blocks) == 1 - target, source = blocks[0] - assert target == "RH-C2-leaf" +def test_valid_multiline_binders_and_lemma_elaborate(): + source = """lemma localPoleSignature + (P : Prop) + (h : P) : + P := by""" result = validate_lean_signature(source, project_root=ROOT) assert result.ok, result.error assert result.status == "FORMALIZED" + assert result.declaration_name == "localPoleSignature" + assert result.proposition == "P" + assert result.normalized_source.endswith(":= by") assert len(result.signature_hash) == 64 -def test_lean_gate_rejects_unknown_type(): +def test_mathematical_inequality_is_not_an_angle_placeholder(): result = validate_lean_signature( - "theorem bad (x : MissingType) : True := by trivial", + "theorem successorStrict (n : Nat) : n < n + 1 := by", + project_root=ROOT, + ) + assert result.ok, result.error + + +def test_lean_gate_rejects_unknown_type_after_contract_validation(): + result = validate_lean_signature( + "theorem bad (x : MissingType) : True := by", project_root=ROOT, ) assert not result.ok @@ -41,16 +153,179 @@ def test_lean_gate_rejects_unknown_type(): assert "unknown" in result.error.lower() -def test_lean_gate_rejects_executable_or_axiomatic_commands(): - for source in ( - "axiom hidden : False", - "def hidden : Nat := 1\ntheorem ok : True := by trivial", - "theorem bad : True := by run_tac do pure ()", - "#eval 1 + 1", - ): - result = validate_lean_signature(source, project_root=ROOT) - assert not result.ok - assert result.status == "UNSAFE_REJECTED" +def test_scaffold_normalization_preserves_all_mathematical_fields_and_hashes(): + original = """theorem normalized + (P : Prop) + (h : P) : + P""" + before = LEAN_SIGNATURE_CONTRACT.normalize_signature(original) + canonical = normalize_lean_signature(original + " := by ") + assert canonical.source.endswith(" := by") + assert canonical.name == before.name + assert canonical.binders == before.binders + assert canonical.proposition == before.proposition + assert canonical.proposition_hash == before.proposition_hash + assert canonical.declaration_hash == before.declaration_hash + + +@pytest.mark.parametrize( + ("source", "expected", "error"), + [ + ( + "theorem changed (P : Prop) : P", + {"name": "immutable", "binders": "(P : Prop)", "proposition": "P"}, + "name changed", + ), + ( + "theorem immutable (P : Prop) : Not P", + {"name": "immutable", "binders": "(P : Prop)", "proposition": "P"}, + "proposition changed", + ), + ( + "theorem immutable (Q : Prop) : Q", + {"name": "immutable", "binders": "(P : Prop)", "proposition": "Q"}, + "binders changed", + ), + ], +) +def test_normalization_never_semantically_repairs(source, expected, error): + with pytest.raises(ValueError, match=error): + normalize_lean_signature(source, expected=expected) + + +def test_prover_uses_same_contract_but_requires_complete_body(): + incomplete = validate_lean_proof( + "theorem proofTarget : True := by", + project_root=ROOT, + ) + assert not incomplete.ok + assert incomplete.status == "CONTRACT_FAILED" + complete = validate_lean_proof( + "theorem proofTarget : True := by\n trivial", + project_root=ROOT, + ) + assert complete.ok, complete.error + assert complete.status == "PROVED" + + +def test_all_lean_producing_roles_are_registered_with_every_fixture(): + assert set(LEAN_CONTRACT_USER_REGISTRY) == { + "formalizer", + "prover", + "premise_auditor", + } + required = set(LEAN_SIGNATURE_FIXTURES) + assert len(required) == 27 + for role, user in LEAN_CONTRACT_USER_REGISTRY.items(): + assert user.role == role + contract = resolve_lean_contract( + user.contract_id, + user.contract_version, + ) + assert contract.content_sha256 + assert set(user.fixtures) == required + source = (ROOT / user.file).read_text() + assert f'"{role}"' in source + if user.policy == "signature": + assert "validate_lean_signature" in source + elif user.policy == "complete_proof": + assert "validate_lean_proof" in source + else: + assert "cannot be safely transformed" in source + + +def test_versioned_content_addressed_contract_ids_fail_closed(): + reference = lean_signature_contract_ref() + contract = resolve_lean_contract( + reference["contract_id"], + reference["version"], + signature_only=True, + ) + assert contract.contract_id.endswith(contract.content_sha256[:16]) + assert (contract.contract_id, contract.version) in LEAN_CONTRACT_REGISTRY + with pytest.raises(ValueError, match="unknown or stale"): + resolve_lean_contract("missing-contract", 1) + with pytest.raises(ValueError, match="unknown or stale"): + resolve_lean_contract(contract.contract_id, contract.version + 1) + with pytest.raises(ValueError, match="policy mismatch"): + resolve_lean_contract( + contract.contract_id, + contract.version, + signature_only=False, + ) + + +def _symbol_table(): + return register_lean_symbol_table( + [ + {"symbol": "\\epsilon", "type": "real constant"}, + {"symbol": "\\rho", "type": "density of sequence"}, + {"symbol": "\\delta", "type": "neighborhood radius"}, + {"symbol": "p", "type": "integer (genus)"}, + ], + parent_statement_hash="parent", + ) + + +def test_registered_identifier_latex_normalization_is_hash_preserving(): + table = _symbol_table() + original = r"(\epsilon : ℝ) (\rho : ℝ) (\delta : ℝ)" + before = lean_symbol_semantic_hash(original, table) + normalized = normalize_registered_latex_identifiers(original, table) + assert normalized == "(epsilon : ℝ) (rho : ℝ) (delta : ℝ)" + assert lean_symbol_semantic_hash(normalized, table) == before + assert resolve_lean_symbol_table( + table.symbol_table_id, + table.version, + ) == table + assert table.symbol_table_id.endswith(table.content_sha256[:16]) + with pytest.raises(ValueError, match="unknown or stale"): + resolve_lean_symbol_table(table.symbol_table_id, table.version + 1) + escaped = json.loads(r'{"binder":"\\\\epsilon"}')["binder"] + with pytest.raises(ValueError, match="unapproved LaTeX"): + normalize_registered_latex_identifiers(escaped, table) + + +@pytest.mark.parametrize( + ("source", "diagnostic"), + [ + (r"\sum n", r"\\sum"), + (r"\frac{1}{x}", r"\\frac"), + (r"\{z_n\}", r"\\\{"), + (r"\unknown x", r"\\unknown"), + ( + r"(\epsilon : \mathbb{R})", + r"\\mathbb", + ), + ], +) +def test_semantic_and_unknown_latex_commands_fail_closed(source, diagnostic): + with pytest.raises(ValueError, match=diagnostic): + normalize_registered_latex_identifiers(source, _symbol_table()) + + +def test_exact_latest_latex_parent_output_rejects_semantic_commands(): + with pytest.raises(ValueError) as caught: + normalize_registered_latex_identifiers( + LATEST_LATEX_PARENT_SOURCE, + _symbol_table(), + ) + message = str(caught.value) + for command in (r"\mathbb", r"\sum", r"\frac", r"\text", r"\{"): + assert command in message + + +def test_lean_prompt_lint_rejects_raw_latex_but_accepts_unicode_ascii(): + with pytest.raises(ValueError, match="raw LaTeX"): + lint_lean_model_prompt([ + {"role": "user", "content": r'{"binder":"\\rho"}'}, + ]) + lint_lean_model_prompt([ + { + "role": "user", + "content": '{"binders":["epsilon : ℝ","rho : ℝ","delta : ℝ"]}', + }, + ]) def test_lean_gate_retries_timeout_after_warmup(monkeypatch): @@ -61,7 +336,7 @@ def test_lean_gate_retries_timeout_after_warmup(monkeypatch): )) monkeypatch.setattr(lean_gate, "_run_lean", lambda *args, **kwargs: next(runs)) result = validate_lean_signature( - "theorem retried : True := by trivial", + "theorem retried : True := by", project_root=ROOT, ) assert result.ok @@ -79,7 +354,7 @@ def test_lean_gate_classifies_second_timeout(monkeypatch): )) monkeypatch.setattr(lean_gate, "_run_lean", lambda *args, **kwargs: next(runs)) result = validate_lean_signature( - "theorem timeout : True := by trivial", + "theorem timeout : True := by", project_root=ROOT, ) assert not result.ok diff --git a/tests/inference_engine/bridge/test_agent_gan_repl.py b/tests/inference_engine/bridge/test_agent_gan_repl.py index fd77308..1a0bbe4 100644 --- a/tests/inference_engine/bridge/test_agent_gan_repl.py +++ b/tests/inference_engine/bridge/test_agent_gan_repl.py @@ -1327,7 +1327,7 @@ def test_lean_proof_without_safe_negation_wrapper_fails_open(tmp_path): project_root=tmp_path, ) assert not rejected.ok - assert rejected.status == "UNSAFE_REJECTED" + assert rejected.status == "CONTRACT_FAILED" def test_complete_minimal_lean_reduction_proof_is_accepted(): diff --git a/tests/inference_engine/bridge/test_structured_output_contract.py b/tests/inference_engine/bridge/test_structured_output_contract.py new file mode 100644 index 0000000..de4b3ca --- /dev/null +++ b/tests/inference_engine/bridge/test_structured_output_contract.py @@ -0,0 +1,106 @@ +import json + +import pytest + +from autoresearch.prefill.semantic_decompose import ( + STRUCTURED_ARTIFACT_CONTRACTS, + lint_structured_prompt, + scan_single_artifact_object, + structured_transport_complete, +) + + +EXPECTED_STRUCTURED_ROLES = { + "strategy", + "premise_suspicion", + "premise_auditor", + "premise_proponent", + "definition_auditor", + "counterexample_worker", + "decomposer", + "formalizer", + "formalizer_parent_signature", + "formalizer_child_signature", + "formalizer_reduction_signature", + "prover", + "adversarial_proponent", + "judge", +} + + +def _value(field): + if field in { + "definitions", + "missing_definitions", + "cases", + "public_assumptions", + "issues", + "repairs", + }: + return [] + if field in {"child", "reduction_contract", "artifact", "claim"}: + return {} + if field in {"parent_newly_formalized"}: + return True + if field in {"confidence"}: + return 0.5 + if field in {"prefill_compute_chunk_tokens"}: + return 256 + return f"value-for-{field}" + + +def _closure_fixture(role): + contract = STRUCTURED_ARTIFACT_CONTRACTS[role] + payload = { + field: _value(field) + for field in contract.required_fields + } + artifact = json.dumps(payload, ensure_ascii=False, separators=(",", ":")) + if contract.heading is None: + if contract.marker: + return f"{contract.marker} {artifact}" + return artifact + return f"### {contract.heading}\n{contract.marker} {artifact}" + + +CLOSURE_FIXTURES = { + role: _closure_fixture(role) + for role in EXPECTED_STRUCTURED_ROLES +} + + +def test_every_structured_role_has_registered_closure_fixture(): + assert set(STRUCTURED_ARTIFACT_CONTRACTS) == EXPECTED_STRUCTURED_ROLES + assert set(CLOSURE_FIXTURES) == EXPECTED_STRUCTURED_ROLES + for role, fixture in CLOSURE_FIXTURES.items(): + contract = STRUCTURED_ARTIFACT_CONTRACTS[role] + if contract.transport_stop: + assert structured_transport_complete(fixture, role) + + +def test_valid_nested_json_handles_latex_braces_quotes_and_backslashes(): + text = ( + '### FORMALIZATION_BUNDLE\nArtifact: {"nested":[{"latex":' + '"\\\\{x\\\\} and } with \\"quote\\" and \\\\\\\\","array":[1,{"x":2}]}]}' + ) + assert structured_transport_complete(text, "formalizer") + scanned = scan_single_artifact_object(text) + assert json.loads(scanned.json_text)["nested"][0]["array"][1] == {"x": 2} + + +def test_markdown_fence_never_becomes_transport_complete(): + fenced = "```json\n" + CLOSURE_FIXTURES["formalizer"] + "\n```" + assert not structured_transport_complete(fenced, "formalizer") + with pytest.raises(ValueError): + scan_single_artifact_object(fenced) + + +def test_prompt_lint_fails_invalid_union_and_post_json_prose(): + with pytest.raises(ValueError, match="union placeholder"): + lint_structured_prompt('Artifact: {"status":"GOOD|BAD"}') + with pytest.raises(ValueError, match="prose after JSON"): + lint_structured_prompt("Follow the JSON with prose after the JSON.") + lint_structured_prompt( + "Return compact JSON. Status must be GOOD or BAD. " + "End immediately after the matching final }." + )