tests/test_v113_executable_math.py

from __future__ import annotations

from dataclasses import asdict

import pytest

from pnp_lab.experiment_schemas import (
    EvidenceArtifact,
    EvidenceKind,
    ExecutionModality,
    ExperimentRun,
    ExperimentRunStatus,
    LogicalPolarity,
    VerificationMethod,
    make_experiment_spec,
    validate_experiment_spec,
)
from pnp_lab.research_portfolio import ResearchAction
from pnp_lab.schemas import ExperimentSpec, VerificationTask


def _spec(**overrides):
    data = dict(
        target_obligation_id="OBL-TEST-1",
        scientific_action=ResearchAction.FALSIFY.value,
        execution_modality=ExecutionModality.BUILTIN_EXACT.value,
        question="Does a counterexample exist in the exact finite domain?",
        hypothesis="The universal statement may fail.",
        claim_shape="UNIVERSAL",
        quantifier_structure={"kind": "FORALL", "variable": "x"},
        tested_scope={"kind": "FINITE_COMPLETE", "n": 3},
        domain_definition={"kind": "BOOLEAN_CUBE", "n": 3},
        success_semantics="A checked witness falsifies the exact obligation.",
        falsification_semantics="No witness in a coverage-verified complete domain supports the finite child only.",
        does_not_establish=["No passing bounded run proves an unrestricted parent."],
        instrument_id="builtin.boolean.enumerator",
        instrument_version_constraint="==1",
        input_payload={"predicate": "x0 xor x1"},
        search_strategy={"kind": "lexicographic_complete"},
        checker_plan={"checker_id": "builtin.boolean.direct"},
        reproduction_policy={"required": True},
    )
    data.update(overrides)
    return make_experiment_spec(**data)


def test_action_and_execution_modality_are_separate_axes():
    spec = _spec()
    assert spec.scientific_action == ResearchAction.FALSIFY.value
    assert spec.execution_modality == ExecutionModality.BUILTIN_EXACT.value
    assert "SAT" not in {x.value for x in ResearchAction}
    assert ResearchAction.FALSIFY.value not in {x.value for x in ExecutionModality}


def test_experiment_identity_ignores_transient_creation_metadata():
    a = _spec(created_cycle=1, proposed_by_model="model-a")
    b = _spec(created_cycle=999, proposed_by_model="model-b")
    assert a.id == b.id
    # canonical provenance digest may include proposer, while scientific identity does not.
    assert a.canonical_sha256 != b.canonical_sha256


def test_experiment_identity_changes_when_scientific_scope_changes():
    a = _spec(tested_scope={"kind": "FINITE_COMPLETE", "n": 3}, domain_definition={"kind": "BOOLEAN_CUBE", "n": 3})
    b = _spec(tested_scope={"kind": "FINITE_COMPLETE", "n": 4}, domain_definition={"kind": "BOOLEAN_CUBE", "n": 4})
    assert a.id != b.id


def test_experiment_requires_explicit_seed_when_nondeterministic():
    spec = _spec(determinism="STOCHASTIC", random_seed=None)
    errors = validate_experiment_spec(spec)
    assert "nondeterministic experiment requires explicit random_seed" in errors


def test_invalid_scientific_action_is_rejected():
    with pytest.raises(ValueError):
        _spec(scientific_action="SAT")


def test_core_run_and_evidence_records_keep_operational_and_logical_status_separate():
    run = ExperimentRun(
        run_id="ERUN-1",
        experiment_id="EXP-1",
        run_status=ExperimentRunStatus.WITNESS_FOUND.value,
    )
    ev = EvidenceArtifact(
        evidence_id="EVID-1",
        target_obligation_id="OBL-1",
        experiment_id="EXP-1",
        experiment_run_ids=[run.run_id],
        evidence_kind=EvidenceKind.EXACT_COUNTEREXAMPLE.value,
        verification_method=VerificationMethod.SMALL_INDEPENDENT_CHECKER.value,
        logical_polarity=LogicalPolarity.FALSIFIES.value,
    )
    assert run.run_status == "WITNESS_FOUND"
    assert ev.logical_polarity == "FALSIFIES"
    assert ev.evidence_kind == "EXACT_COUNTEREXAMPLE"
    assert ev.verification_method == "SMALL_INDEPENDENT_CHECKER"


def test_schemas_module_reexports_v113_records_without_breaking_v112_verification_task():
    assert ExperimentSpec.__name__ == "ExperimentSpec"
    legacy = VerificationTask(kind="boolean_equivalence", variables=["x"], lhs="x", rhs="x")
    assert asdict(legacy)["kind"] == "boolean_equivalence"

from pnp_lab.checker_registry import build_core_checker_registry
from pnp_lab.exact_primitives import (
    ExactPrimitiveError,
    evaluate_boolean_circuit,
    evaluate_boolean_polynomial,
    gf2_kernel_basis,
    gf2_kernel_vector_is_valid,
    gf2_rank,
)
from pnp_lab.instrument_registry import build_core_instrument_registry, qualify_core_instruments


def test_boolean_circuit_uses_canonical_dag_and_direct_semantics():
    circuit = {
        "inputs": ["a", "b"],
        "gates": [
            {"id": "p", "op": "AND", "args": ["a", "b"]},
            {"id": "q", "op": "XOR", "args": ["a", "b"]},
            {"id": "o", "op": "OR", "args": ["p", "q"]},
        ],
        "output": "o",
    }
    assert [evaluate_boolean_circuit(circuit, {"a": a, "b": b}) for a, b in [(0,0),(0,1),(1,0),(1,1)]] == [0,1,1,1]
    with pytest.raises(ExactPrimitiveError):
        evaluate_boolean_circuit({"inputs": ["a"], "gates": [{"id": "g", "op": "XOR", "args": ["a", "future"]}], "output": "g"}, {"a": 1})


def test_boolean_polynomial_is_exact_anf_and_duplicate_terms_cancel():
    assert evaluate_boolean_polynomial([[0], [1], [0, 1]], [1, 1]) == 1
    assert evaluate_boolean_polynomial([[0], [0]], [1]) == 0


def test_gf2_rank_and_kernel_basis_are_consistent():
    rows = [0b1101, 0b0110, 0b1011]
    rank = gf2_rank(rows, 4)
    basis = gf2_kernel_basis(rows, 4)
    assert len(basis) == 4 - rank
    assert all(gf2_kernel_vector_is_valid(rows, v, 4) for v in basis)


def test_core_instrument_qualification_passes_differential_and_mutation_checks():
    quals = qualify_core_instruments()
    assert quals
    assert all(q.status == "PASS" for q in quals.values())
    assert quals["builtin.gf2.rank"].differential_tests >= 200
    assert quals["builtin.boolean.circuit.evaluate"].mutation_tests >= 1


def test_unqualified_instrument_cannot_be_used_authoritatively():
    registry = build_core_instrument_registry(qualify=False)
    with pytest.raises(RuntimeError):
        registry.execute("builtin.witness.equality", {"actual": 1, "expected": 1}, authoritative=True)
    assert registry.execute("builtin.witness.equality", {"actual": 1, "expected": 1}, authoritative=False)["status"] == "PASS"


def test_qualified_instrument_and_independent_checker_reject_mutated_witness():
    instruments = build_core_instrument_registry(qualify=True)
    checkers = build_core_checker_registry()
    result = instruments.execute("builtin.gf2.kernel", {"rows": [0b11], "ncols": 2}, authoritative=True)
    vector = result["basis"][0]
    assert checkers.check("checker.gf2.kernel", {"rows": [0b11], "ncols": 2, "vector": vector})["status"] == "PASS"
    assert checkers.check("checker.gf2.kernel", {"rows": [0b11], "ncols": 2, "vector": 0b01})["status"] == "FAIL"

from pnp_lab.exact_primitives import serialize_boolean_circuit


def test_boolean_circuit_serialization_is_canonical():
    circuit = {"output": "g", "gates": [{"args": ["x", "y"], "op": "xor", "id": "g"}], "inputs": ["x", "y"]}
    a = serialize_boolean_circuit(circuit)
    b = serialize_boolean_circuit({"inputs": ["x", "y"], "gates": [{"id": "g", "op": "XOR", "args": ["x", "y"]}], "output": "g"})
    assert a == b
    assert a.endswith(b"\n")


def test_small_rank_checker_is_algorithmically_independent_of_rref_instrument():
    instruments = build_core_instrument_registry(qualify=True)
    checkers = build_core_checker_registry()
    rows = [0b1011, 0b0110, 0b1101]
    result = instruments.execute("builtin.gf2.rank", {"rows": rows, "ncols": 4}, authoritative=True)
    checked = checkers.check("checker.gf2.rank.small", {"rows": rows, "ncols": 4, "expected_rank": result["rank"]})
    assert checked["status"] == "PASS"
    assert checkers.check("checker.gf2.rank.small", {"rows": rows, "ncols": 4, "expected_rank": result["rank"] + 1})["status"] == "FAIL"

import json
from pathlib import Path

from pnp_lab.artifact_store import ArtifactIntegrityError, ArtifactStore
from pnp_lab.experiment_executor import ExperimentExecutor
from pnp_lab.experiment_store import ExperimentStore


def test_content_addressed_blob_store_verifies_hash_and_quarantines_corruption(tmp_path):
    store = ArtifactStore(tmp_path / "scientific_record")
    ref = store.put_bytes(b"proof-carrying-data", role="test")
    assert store.get_bytes(ref.blob_id) == b"proof-carrying-data"
    path = store.path_for_sha256(ref.sha256)
    path.write_bytes(b"corrupt")
    with pytest.raises(ArtifactIntegrityError):
        store.get_bytes(ref.blob_id)
    assert not path.exists()
    assert list(store.quarantine.glob("*.corrupt"))


def test_experiment_store_is_immutable_and_manifest_verified(tmp_path):
    store = ExperimentStore(tmp_path / "scientific_record")
    spec = _spec(instrument_id="builtin.witness.equality", instrument_version_constraint="==1", input_payload={"actual": {"x": 1}, "expected": {"x": 1}})
    store.write_spec(spec)
    assert store.load_spec(spec.id).id == spec.id
    assert store.verify_manifest(spec.id)["status"] == "PASS"

    same_science_new_proposer = _spec(
        instrument_id="builtin.witness.equality", instrument_version_constraint="==1",
        input_payload={"actual": {"x": 1}, "expected": {"x": 1}},
        proposed_by_model="independent-model",
    )
    assert same_science_new_proposer.id == spec.id
    store.write_spec(same_science_new_proposer)
    assert list((store.experiment_dir(spec.id) / "proposals").glob("PROPOSAL-*.json"))
    assert store.verify_manifest(spec.id)["status"] == "PASS"


def test_builtin_experiment_execution_is_replayable_without_llm(tmp_path):
    store = ExperimentStore(tmp_path / "scientific_record")
    spec = _spec(
        instrument_id="builtin.boolean.polynomial.evaluate",
        instrument_version_constraint="==1",
        input_payload={"polynomial": [[0], [1], [0, 1]], "assignment": [1, 1]},
    )
    executor = ExperimentExecutor(store)
    first = executor.execute_builtin(spec)
    assert first.run_status == "PASS"
    assert first.artifact_ids
    assert store.verify_manifest(spec.id)["status"] == "PASS"
    report = executor.replay(spec.id)
    assert report["status"] == "PASS"
    assert report["logical_result_byte_equivalent"] is True
    assert len(store.load_runs(spec.id)) == 2


def test_experiment_manifest_detects_record_tampering(tmp_path):
    store = ExperimentStore(tmp_path / "scientific_record")
    spec = _spec(instrument_id="builtin.witness.equality", instrument_version_constraint="==1", input_payload={"actual": 1, "expected": 1})
    store.write_spec(spec)
    path = store.experiment_dir(spec.id) / "spec.json"
    original = path.read_text(encoding="utf-8")
    path.write_text(original + " ", encoding="utf-8")
    report = store.verify_manifest(spec.id)
    assert report["status"] == "FAIL"
    assert any("spec.json" in error for error in report["errors"])

from pnp_lab.evidence_applicability import assess_applicability
from pnp_lab.obligation_policy import evaluate_obligation_status
from pnp_lab.obligations import normalize_obligation_proposal, obligation_from_proposal
from pnp_lab.schemas import ProofObligation


def _structured_obligation(
    statement: str,
    *,
    claim_shape: str,
    quantifier_structure: dict,
    scope_definition: dict,
    scope: str,
    obligation_type: str = "LEMMA",
    finite_testability: str = "UNKNOWN",
) -> ProofObligation:
    proposal = normalize_obligation_proposal({
        "statement": statement,
        "quantifiers": "structured in v1.13 overlay",
        "scope": scope,
        "claim_shape": claim_shape,
        "quantifier_structure": quantifier_structure,
        "scope_definition": scope_definition,
        "obligation_type": obligation_type,
        "finite_testability": finite_testability,
    })
    return obligation_from_proposal(proposal, cycle=1)


def _checked_counterexample(obl: ProofObligation, *, inner_established: bool | None = None) -> EvidenceArtifact:
    scope = {
        "kind": "INSTANCE",
        "relation_to_obligation": "INSTANCE_IN_OBLIGATION_DOMAIN",
        "target_obligation_id": obl.id,
        "domain_membership_checked": True,
        "assumptions_checked": True,
    }
    if inner_established is not None:
        scope["inner_quantifier_established"] = inner_established
    return EvidenceArtifact(
        evidence_id="EVID-CE-1",
        target_obligation_id=obl.id,
        experiment_id="EXP-CE-1",
        evidence_kind=EvidenceKind.EXACT_COUNTEREXAMPLE.value,
        verification_method=VerificationMethod.SMALL_INDEPENDENT_CHECKER.value,
        logical_polarity=LogicalPolarity.FALSIFIES.value,
        tested_scope=scope,
        witness_ids=["WIT-1"],
        checker_run_ids=["ERUN-CHECK-1"],
    )


def _checked_witness(obl: ProofObligation, *, inner_established: bool | None = None) -> EvidenceArtifact:
    scope = {
        "kind": "INSTANCE",
        "relation_to_obligation": "WITNESS_IN_OBLIGATION_DOMAIN",
        "target_obligation_id": obl.id,
        "domain_membership_checked": True,
        "assumptions_checked": True,
    }
    if inner_established is not None:
        scope["inner_quantifier_established"] = inner_established
    return EvidenceArtifact(
        evidence_id="EVID-WIT-1",
        target_obligation_id=obl.id,
        experiment_id="EXP-WIT-1",
        evidence_kind=EvidenceKind.EXACT_WITNESS.value,
        verification_method=VerificationMethod.DIRECT_CHECKER.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value,
        tested_scope=scope,
        witness_ids=["WIT-1"],
        checker_run_ids=["ERUN-CHECK-1"],
    )


def test_v113_unknown_structured_quantifiers_refuse_to_guess_from_prose():
    legacy = ProofObligation(id="OBL-LEGACY", title="legacy", statement="for all x P(x)", scope="all x", quantifiers="for all x")
    evidence = _checked_counterexample(legacy)
    app = assess_applicability(legacy, evidence)
    assert app.status == "UNKNOWN_SCOPE_COMPATIBILITY"
    assert app.can_falsify is False
    assert evaluate_obligation_status(legacy, evidence=[evidence]).derived_status == "OPEN"


def test_v113_checked_counterexample_falsifies_general_universal_exact_node():
    obl = _structured_obligation(
        "for all x in D, P(x)", claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["x"]},
        scope_definition={"kind": "GENERAL", "domain_id": "D"}, scope="all x in D",
    )
    evidence = _checked_counterexample(obl)
    app = assess_applicability(obl, evidence)
    assert app.can_falsify is True
    assessment = evaluate_obligation_status(obl, evidence=[evidence])
    assert assessment.derived_status == "FALSIFIED"
    assert assessment.contradicting_evidence_ids == ["EVID-CE-1"]


def test_v113_passing_samples_cannot_verify_general_universal():
    obl = _structured_obligation(
        "for all x in D, P(x)", claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["x"]},
        scope_definition={"kind": "GENERAL", "domain_id": "D"}, scope="all x in D",
    )
    sample = EvidenceArtifact(
        evidence_id="EVID-SAMPLE", target_obligation_id=obl.id, experiment_id="EXP-S",
        evidence_kind=EvidenceKind.HEURISTIC_SAMPLE.value,
        verification_method=VerificationMethod.DIRECT_CHECKER.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value,
        tested_scope={"kind": "FINITE_SAMPLE", "domain_id": "D", "sample_count": 1000},
    )
    app = assess_applicability(obl, sample)
    assert app.status == "PARTIAL_SCOPE_ONLY"
    assert app.can_verify is False
    assert evaluate_obligation_status(obl, evidence=[sample]).derived_status == "PARTIALLY_VERIFIED"


def test_v113_complete_finite_enumeration_verifies_exact_child_but_not_general_parent():
    parent = _structured_obligation(
        "for all n P(n)", claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["n"]},
        scope_definition={"kind": "GENERAL", "domain_id": "N"}, scope="all n",
    )
    child_scope = {"kind": "FINITE_COMPLETE", "domain_id": "N", "max_n": 12}
    child = _structured_obligation(
        "for all n <= 12 P(n)", claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["n"]},
        scope_definition=child_scope, scope="n <= 12", obligation_type="FINITE_CHECK", finite_testability="FINITE_COMPLETE",
    )
    def evidence_for(target):
        return EvidenceArtifact(
            evidence_id=f"EVID-FIN-{target.id[-4:]}", target_obligation_id=target.id, experiment_id="EXP-FIN",
            evidence_kind=EvidenceKind.FINITE_EXHAUSTIVE_RESULT.value,
            verification_method=VerificationMethod.COVERAGE_CHECKER.value,
            logical_polarity=LogicalPolarity.SUPPORTS.value,
            tested_scope={**child_scope, "coverage_complete": True, "coverage_checked": True},
            checker_run_ids=["ERUN-COVERAGE-1"],
        )
    child_evidence = evidence_for(child)
    assert assess_applicability(child, child_evidence).can_verify is True
    assert evaluate_obligation_status(child, evidence=[child_evidence]).derived_status == "VERIFIED"

    parent_evidence = evidence_for(parent)
    app = assess_applicability(parent, parent_evidence)
    assert app.status == "PARTIAL_SCOPE_ONLY"
    assert app.restricted_child_required is True
    assert evaluate_obligation_status(parent, evidence=[parent_evidence]).derived_status == "PARTIALLY_VERIFIED"


def test_v113_checked_existential_witness_verifies_exact_existential():
    obl = _structured_obligation(
        "there exists x in D with P(x)", claim_shape="EXISTENTIAL",
        quantifier_structure={"prefix": ["EXISTS"], "variables": ["x"]},
        scope_definition={"kind": "GENERAL", "domain_id": "D"}, scope="x in D",
    )
    evidence = _checked_witness(obl)
    assert assess_applicability(obl, evidence).can_verify is True
    assert evaluate_obligation_status(obl, evidence=[evidence]).derived_status == "VERIFIED"


def test_v113_partial_existential_no_witness_is_not_falsification():
    obl = _structured_obligation(
        "there exists x in D with P(x)", claim_shape="EXISTENTIAL",
        quantifier_structure={"prefix": ["EXISTS"], "variables": ["x"]},
        scope_definition={"kind": "GENERAL", "domain_id": "D"}, scope="x in D",
    )
    evidence = EvidenceArtifact(
        evidence_id="EVID-NONE", target_obligation_id=obl.id, experiment_id="EXP-NONE",
        evidence_kind=EvidenceKind.HEURISTIC_SAMPLE.value,
        verification_method=VerificationMethod.DIRECT_CHECKER.value,
        logical_polarity=LogicalPolarity.NEUTRAL.value,
        tested_scope={"kind": "SEARCHED_SUBSET", "domain_id": "D", "searched_count": 100},
    )
    app = assess_applicability(obl, evidence)
    assert app.can_falsify is False and app.can_verify is False
    assert evaluate_obligation_status(obl, evidence=[evidence]).derived_status == "OPEN"


def test_v113_nested_quantifier_refuses_naive_outer_counterexample_until_inner_is_established():
    obl = _structured_obligation(
        "for all x there exists y P(x,y)", claim_shape="NESTED",
        quantifier_structure={"prefix": ["FORALL", "EXISTS"], "variables": ["x", "y"]},
        scope_definition={"kind": "GENERAL", "domain_id": "D2"}, scope="all x, some y",
    )
    naive = _checked_counterexample(obl, inner_established=False)
    assert assess_applicability(obl, naive).status == "UNKNOWN_SCOPE_COMPATIBILITY"
    assert evaluate_obligation_status(obl, evidence=[naive]).derived_status == "OPEN"
    certified = _checked_counterexample(obl, inner_established=True)
    assert assess_applicability(obl, certified).can_falsify is True


def test_v113_restricted_scope_success_cannot_verify_arbitrary_parent():
    obl = _structured_obligation(
        "P holds for arbitrary circuits", claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["C"]},
        scope_definition={"kind": "GENERAL", "domain_id": "ARBITRARY_CIRCUITS"}, scope="arbitrary circuits",
    )
    evidence = EvidenceArtifact(
        evidence_id="EVID-AFFINE", target_obligation_id=obl.id, experiment_id="EXP-AFFINE",
        evidence_kind=EvidenceKind.FINITE_EXHAUSTIVE_RESULT.value,
        verification_method=VerificationMethod.COVERAGE_CHECKER.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value,
        tested_scope={"kind": "FINITE_COMPLETE", "domain_id": "AFFINE_CIRCUITS", "size": 5, "coverage_complete": True, "coverage_checked": True},
        checker_run_ids=["ERUN-AFFINE-COVERAGE"],
    )
    app = assess_applicability(obl, evidence)
    assert app.status == "PARTIAL_SCOPE_ONLY"
    assert app.can_verify is False


def test_v113_complexity_measurements_never_prove_asymptotic_polynomial_time():
    obl = _structured_obligation(
        "Algorithm A runs in polynomial time", claim_shape="COMPLEXITY",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["n"]},
        scope_definition={"kind": "ASYMPTOTIC", "parameter": "encoded_input_length"}, scope="all input lengths",
    )
    evidence = EvidenceArtifact(
        evidence_id="EVID-TIMING", target_obligation_id=obl.id, experiment_id="EXP-TIMING",
        evidence_kind=EvidenceKind.COMPLEXITY_MEASUREMENT.value,
        verification_method=VerificationMethod.DIRECT_CHECKER.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value,
        tested_scope={"kind": "BOUNDED_MEASUREMENTS", "max_n": 1000},
    )
    app = assess_applicability(obl, evidence)
    assert app.can_verify is False
    assert app.status == "PARTIAL_SCOPE_ONLY"
    assert evaluate_obligation_status(obl, evidence=[evidence]).derived_status != "VERIFIED"


def test_v113_structured_overlay_does_not_change_legacy_obligation_identity():
    base = normalize_obligation_proposal({"statement": "P(n)", "quantifiers": "for all n", "scope": "all n"})
    enriched = normalize_obligation_proposal({
        "statement": "P(n)", "quantifiers": "for all n", "scope": "all n",
        "claim_shape": "UNIVERSAL", "quantifier_structure": {"prefix": ["FORALL"]},
        "scope_definition": {"kind": "GENERAL", "domain_id": "N"},
    })
    assert base["canonical_id"] == enriched["canonical_id"]
    assert obligation_from_proposal(enriched).claim_shape == "UNIVERSAL"


def test_v113_complete_finite_no_witness_can_falsify_exact_finite_existential():
    scope = {"kind": "FINITE_COMPLETE", "domain_id": "D", "size": 16}
    obl = _structured_obligation(
        "there exists x in finite D with P(x)", claim_shape="EXISTENTIAL",
        quantifier_structure={"prefix": ["EXISTS"], "variables": ["x"]},
        scope_definition=scope, scope="finite D", obligation_type="FINITE_CHECK", finite_testability="FINITE_COMPLETE",
    )
    evidence = EvidenceArtifact(
        evidence_id="EVID-FIN-NONE", target_obligation_id=obl.id, experiment_id="EXP-FIN-NONE",
        evidence_kind=EvidenceKind.FINITE_EXHAUSTIVE_RESULT.value,
        verification_method=VerificationMethod.COVERAGE_CHECKER.value,
        logical_polarity=LogicalPolarity.FALSIFIES.value,
        tested_scope={**scope, "coverage_complete": True, "coverage_checked": True},
        checker_run_ids=["ERUN-COVERAGE-2"],
    )
    app = assess_applicability(obl, evidence)
    assert app.can_falsify is True
    assert evaluate_obligation_status(obl, evidence=[evidence]).derived_status == "FALSIFIED"


def test_v113_malformed_structured_overlay_is_safely_treated_as_missing():
    proposal = normalize_obligation_proposal({
        "statement": "P(x)", "quantifiers": "for all x", "scope": "all x",
        "claim_shape": "UNIVERSAL", "quantifier_structure": "not-a-mapping", "scope_definition": ["also", "wrong"],
    })
    obl = obligation_from_proposal(proposal)
    assert obl.quantifier_structure == {}
    assert obl.scope_definition == {}
    assert assess_applicability(obl, _checked_counterexample(obl)).status == "UNKNOWN_SCOPE_COMPATIBILITY"

from pnp_lab.finite_enumerator import audit_boolean_cube_items, exhaustive_boolean_polynomial


def test_v113_finite_enumerator_complete_result_has_explicit_coverage_manifest_and_independent_replay():
    payload = {"n_variables": 4, "polynomial": [[0], [0]], "expected_value": 0}
    instruments = build_core_instrument_registry(qualify=True)
    checkers = build_core_checker_registry()
    result = instruments.execute("builtin.boolean.polynomial.exhaustive", payload, authoritative=True)
    assert result["status"] == "NO_WITNESS_IN_COMPLETE_DOMAIN"
    coverage = result["coverage"]
    assert coverage["expected_count"] == 16
    assert coverage["searched_count"] == 16
    assert coverage["unique_count"] == 16
    assert coverage["duplicate_count"] == 0
    assert coverage["coverage_complete"] is True
    checked = checkers.check("checker.boolean.polynomial.exhaustive", {"input_payload": payload, "producer_result": result})
    assert checked["status"] == "PASS"
    assert checked["coverage_complete"] is True
    assert checked["checked_count"] == 16


def test_v113_finite_enumerator_witness_is_directly_rechecked_by_independent_path():
    payload = {"n_variables": 3, "polynomial": [[0]], "expected_value": 0}
    instruments = build_core_instrument_registry(qualify=True)
    checkers = build_core_checker_registry()
    result = instruments.execute("builtin.boolean.polynomial.exhaustive", payload, authoritative=True)
    assert result["status"] == "WITNESS_FOUND"
    assert result["coverage"]["coverage_complete"] is False
    checked = checkers.check("checker.boolean.polynomial.exhaustive", {"input_payload": payload, "producer_result": result})
    assert checked["status"] == "PASS"
    assert checked["witness_checked"] is True


def test_v113_partial_enumeration_no_witness_has_partial_semantics_only():
    payload = {"n_variables": 6, "polynomial": [], "expected_value": 0, "max_assignments": 5}
    result = exhaustive_boolean_polynomial(payload)
    assert result["status"] == "NO_WITNESS_IN_SEARCHED_SUBSET"
    assert result["coverage"]["searched_count"] == 5
    assert result["coverage"]["expected_count"] == 64
    assert result["coverage"]["coverage_complete"] is False
    checked = build_core_checker_registry().check("checker.boolean.polynomial.exhaustive", {"input_payload": payload, "producer_result": result})
    assert checked["status"] == "PASS"
    assert checked["coverage_complete"] is False


def test_v113_explicit_coverage_audit_catches_skip_and_duplicate_does_not_fake_completeness():
    items = [(0,0), (0,1), (1,0), (1,1)]
    assert audit_boolean_cube_items(items, 2)["status"] == "PASS"
    skipped = audit_boolean_cube_items(items[:-1], 2)
    assert skipped["status"] == "FAIL" and skipped["missing_count"] == 1
    duplicated = audit_boolean_cube_items(items[:-1] + [items[0]], 2)
    assert duplicated["status"] == "FAIL"
    assert duplicated["duplicate_count"] == 1
    assert duplicated["unique_count"] == 3


def test_v113_unqualified_symmetry_reduction_and_filter_can_never_claim_exhaustive():
    reduced = exhaustive_boolean_polynomial({
        "n_variables": 4, "polynomial": [], "expected_value": 0,
        "symmetry_reduction": {"enabled": True, "group": "S4"},
    })
    assert reduced["status"] == "INCONCLUSIVE"
    assert reduced["coverage"]["coverage_status"] == "HEURISTIC_REDUCED_SEARCH"
    assert reduced["coverage"]["coverage_complete"] is False
    filtered = exhaustive_boolean_polynomial({
        "n_variables": 4, "polynomial": [], "expected_value": 0,
        "filter": {"predicate": "x0=0"},
    })
    assert filtered["status"] == "INCONCLUSIVE"
    assert filtered["coverage"]["coverage_status"] == "UNQUALIFIED_FILTER"
    assert filtered["coverage"]["coverage_complete"] is False


def test_v113_independent_exhaustive_checker_rejects_forged_complete_metadata_and_missed_counterexample():
    payload = {"n_variables": 2, "polynomial": [[0]], "expected_value": 0}
    forged = {
        "status": "NO_WITNESS_IN_COMPLETE_DOMAIN",
        "coverage": {"coverage_complete": True, "searched_count": 4, "expected_count": 4},
    }
    checked = build_core_checker_registry().check("checker.boolean.polynomial.exhaustive", {"input_payload": payload, "producer_result": forged})
    assert checked["status"] == "FAIL"
    assert "counterexample" in checked["reason"]


def test_v113_exhaustive_instrument_qualification_includes_coverage_mutation_guards():
    q = qualify_core_instruments()["builtin.boolean.polynomial.exhaustive"]
    assert q.status == "PASS"
    assert q.negative_tests >= 2
    assert q.mutation_tests >= 2
    assert q.details["skipped_case_detected"] is True
    assert q.details["duplicate_cannot_fake_coverage"] is True
    assert q.details["unsafe_symmetry_downgraded"] is True


def test_v113_complete_finite_evidence_needs_recorded_checker_run_not_just_method_label():
    scope = {"kind": "FINITE_COMPLETE", "domain_id": "BOOLEAN_CUBE", "n_variables": 3}
    obl = _structured_obligation(
        "all assignments satisfy P", claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["x"]},
        scope_definition=scope, scope="all 3-bit assignments", obligation_type="FINITE_CHECK", finite_testability="FINITE_COMPLETE",
    )
    unbacked = EvidenceArtifact(
        evidence_id="EVID-UNBACKED-COVERAGE", target_obligation_id=obl.id, experiment_id="EXP-U",
        evidence_kind=EvidenceKind.FINITE_EXHAUSTIVE_RESULT.value,
        verification_method=VerificationMethod.DUAL_IMPLEMENTATION_REPLAY.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value,
        tested_scope={**scope, "coverage_complete": True, "coverage_checked": True},
        checker_run_ids=[],
    )
    assert assess_applicability(obl, unbacked).can_verify is False
    assert evaluate_obligation_status(obl, evidence=[unbacked]).derived_status != "VERIFIED"


def test_v113_actual_exhaustive_producer_and_checker_can_feed_exact_finite_child_policy():
    scope = {"kind": "FINITE_COMPLETE", "domain_id": "BOOLEAN_CUBE", "n_variables": 3}
    obl = _structured_obligation(
        "zero ANF is zero on all 3-bit assignments", claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["assignment"]},
        scope_definition=scope, scope="all 3-bit assignments", obligation_type="FINITE_CHECK", finite_testability="FINITE_COMPLETE",
    )
    payload = {"n_variables": 3, "polynomial": [], "expected_value": 0}
    producer = build_core_instrument_registry(qualify=True).execute("builtin.boolean.polynomial.exhaustive", payload, authoritative=True)
    checker = build_core_checker_registry().check("checker.boolean.polynomial.exhaustive", {"input_payload": payload, "producer_result": producer})
    assert producer["status"] == "NO_WITNESS_IN_COMPLETE_DOMAIN" and checker["status"] == "PASS"
    evidence = EvidenceArtifact(
        evidence_id="EVID-E2E-FINITE", target_obligation_id=obl.id, experiment_id="EXP-E2E-FINITE",
        experiment_run_ids=["ERUN-PRODUCER"],
        evidence_kind=EvidenceKind.FINITE_EXHAUSTIVE_RESULT.value,
        verification_method=VerificationMethod.DUAL_IMPLEMENTATION_REPLAY.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value,
        tested_scope={**scope, "coverage_complete": producer["coverage"]["coverage_complete"], "coverage_checked": checker["coverage_complete"]},
        checker_run_ids=["ERUN-CHECKER"],
    )
    assert assess_applicability(obl, evidence).can_verify is True
    assert evaluate_obligation_status(obl, evidence=[evidence]).derived_status == "VERIFIED"

from pnp_lab.counterexample_lab import CounterexampleLab, CounterexampleLabError
from pnp_lab.counterexamples import CounterexampleStore
from pnp_lab.theorem_graph import TheoremGraph, make_edge


def _boolean_cube_obligation(n: int = 3) -> ProofObligation:
    return _structured_obligation(
        "for every Boolean assignment, polynomial value is zero",
        claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["assignment"]},
        scope_definition={"kind": "FINITE_COMPLETE", "domain_id": "BOOLEAN_CUBE", "n_variables": n},
        scope=f"all {n}-bit assignments",
        obligation_type="FINITE_CHECK",
        finite_testability="FINITE_COMPLETE",
    )


def test_v113_counterexample_lab_end_to_end_binds_checks_minimizes_and_falsifies_exact_obligation(tmp_path):
    obl = _boolean_cube_obligation(3)
    payload = {"n_variables": 3, "polynomial": [[0]], "expected_value": 0}
    producer = build_core_instrument_registry(qualify=True).execute("builtin.boolean.polynomial.exhaustive", payload, authoritative=True)
    assert producer["status"] == "WITNESS_FOUND"
    lab = CounterexampleLab(store=CounterexampleStore(tmp_path / "counterexamples"))
    result = lab.process_boolean_polynomial_witness(
        obligation=obl,
        input_payload=payload,
        producer_result=producer,
        experiment_id="EXP-CX-E2E",
        experiment_run_ids=["ERUN-DISCOVERY"],
        checker_run_id="ERUN-INDEPENDENT-CHECK",
    )
    assert result.counterexample.reproduced is True
    assert result.counterexample.scope == "TARGET"
    assert result.counterexample.target_obligation_id == obl.id
    assert result.counterexample.binding_status == "EXACT_OBLIGATION_BOUND"
    assert result.counterexample.minimality_status == "PROVEN_MINIMAL_WITHIN_FINITE_DOMAIN"
    assert result.evidence.evidence_kind == "EXACT_COUNTEREXAMPLE"
    assert result.applicability["can_falsify"] is True
    assert result.obligation_assessment.derived_status == "FALSIFIED"
    assert result.independent_check["status"] == "PASS"
    assert CounterexampleStore(tmp_path / "counterexamples").latest(result.counterexample.counterexample_id)["binding_status"] == "EXACT_OBLIGATION_BOUND"


def test_v113_counterexample_lab_preserves_original_witness_and_minimizes_nonminimal_discovery():
    obl = _boolean_cube_obligation(3)
    payload = {"n_variables": 3, "polynomial": [[0]], "expected_value": 0}
    producer = {"status": "WITNESS_FOUND", "witness": {"assignment": [1, 1, 1], "actual": 1, "expected": 0}}
    result = CounterexampleLab().process_boolean_polynomial_witness(
        obligation=obl, input_payload=payload, producer_result=producer,
        experiment_id="EXP-CX-NONMIN", experiment_run_ids=["ERUN-D"], checker_run_id="ERUN-C",
    )
    assert result.discovery_witness["assignment"] == [1, 1, 1]
    assert result.minimized_witness["assignment"] == [1, 0, 0]
    assert '"assignment":[1,1,1]' in result.counterexample.original_witness
    assert '"assignment":[1,0,0]' in result.counterexample.minimized_witness
    assert result.counterexample.minimization_trace[0]["operation"] == "FULL_DOMAIN_MINIMIZATION"


def test_v113_counterexample_lab_structural_failing_core_is_machine_readable():
    obl = _boolean_cube_obligation(3)
    payload = {"n_variables": 3, "polynomial": [[0]], "expected_value": 0}
    producer = {"status": "WITNESS_FOUND", "witness": {"assignment": [1, 0, 0], "actual": 1, "expected": 0}}
    result = CounterexampleLab().process_boolean_polynomial_witness(
        obligation=obl, input_payload=payload, producer_result=producer,
        experiment_id="EXP-CX-CORE", experiment_run_ids=["ERUN-D"], checker_run_id="ERUN-C",
    )
    features = result.counterexample.structural_features
    assert features["assignment_support"] == [0]
    assert features["hamming_weight"] == 1
    assert features["single_bit_repair_indices"] == [0]
    assert result.counterexample.repair_seed["status"] == "HYPOTHESIS_SEED_ONLY"


def test_v113_counterexample_lab_rejects_corrupt_or_out_of_domain_witness():
    obl = _boolean_cube_obligation(3)
    payload = {"n_variables": 3, "polynomial": [[0]], "expected_value": 0}
    bad = {"status": "WITNESS_FOUND", "witness": {"assignment": [0, 0, 0], "actual": 1, "expected": 0}}
    with pytest.raises(CounterexampleLabError):
        CounterexampleLab().process_boolean_polynomial_witness(
            obligation=obl, input_payload=payload, producer_result=bad,
            experiment_id="EXP-BAD", experiment_run_ids=["R"], checker_run_id="C",
        )
    wrong_dimension = _boolean_cube_obligation(2)
    good = {"status": "WITNESS_FOUND", "witness": {"assignment": [1, 0, 0], "actual": 1, "expected": 0}}
    with pytest.raises(CounterexampleLabError):
        CounterexampleLab().process_boolean_polynomial_witness(
            obligation=wrong_dimension, input_payload=payload, producer_result=good,
            experiment_id="EXP-BAD-DIM", experiment_run_ids=["R"], checker_run_id="C",
        )


def test_v113_counterexample_lab_does_not_overstate_minimality_for_large_domain():
    n = 13
    obl = _boolean_cube_obligation(n)
    payload = {"n_variables": n, "polynomial": [[0]], "expected_value": 0}
    witness = [1] * n
    producer = {"status": "WITNESS_FOUND", "witness": {"assignment": witness, "actual": 1, "expected": 0}}
    result = CounterexampleLab().process_boolean_polynomial_witness(
        obligation=obl, input_payload=payload, producer_result=producer,
        experiment_id="EXP-CX-LOCAL", experiment_run_ids=["R"], checker_run_id="C",
        full_domain_minimize_n=12,
    )
    assert result.counterexample.minimality_status == "LOCALLY_MINIMIZED"
    assert result.minimized_witness["assignment"] == [1] + [0] * (n - 1)


def test_v113_counterexample_lab_dependency_impact_is_reported_but_not_applied_directly():
    obl = _boolean_cube_obligation(2)
    claim = {"id": "CLM-DEP", "status": "CANDIDATE", "proof_paths": [{"path_id": "P", "required_obligation_ids": [obl.id]}]}
    graph = TheoremGraph.from_state(
        {"claims": {"CLM-DEP": claim}, "obligations": {obl.id: obl.to_dict()}},
        persisted_edges=[make_edge("CLM-DEP", obl.id, "CLAIM_REQUIRES_OBLIGATION", essential=True).to_dict()],
    )
    payload = {"n_variables": 2, "polynomial": [[0]], "expected_value": 0}
    producer = {"status": "WITNESS_FOUND", "witness": {"assignment": [1, 0], "actual": 1, "expected": 0}}
    result = CounterexampleLab().process_boolean_polynomial_witness(
        obligation=obl, input_payload=payload, producer_result=producer,
        experiment_id="EXP-CX-GRAPH", experiment_run_ids=["R"], checker_run_id="C", theorem_graph=graph,
    )
    assert result.dependency_impact["claims_requiring_reaudit"] == ["CLM-DEP"]
    # Graph state remains an input snapshot; CounterexampleLab only reports impact.
    assert graph.nodes[obl.id]["status"] == "OPEN"


def test_v113_counterexample_lab_refuses_unchecked_additional_assumptions():
    obl = _structured_obligation(
        "for all Boolean assignments satisfying A, P",
        claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["assignment"]},
        scope_definition={"kind": "FINITE_COMPLETE", "domain_id": "BOOLEAN_CUBE", "n_variables": 2, "assumptions": ["A(assignment)"]},
        scope="2-bit assignments satisfying A", obligation_type="FINITE_CHECK", finite_testability="FINITE_COMPLETE",
    )
    payload = {"n_variables": 2, "polynomial": [[0]], "expected_value": 0}
    producer = {"status": "WITNESS_FOUND", "witness": {"assignment": [1, 0], "actual": 1, "expected": 0}}
    with pytest.raises(CounterexampleLabError, match="additional structured assumptions"):
        CounterexampleLab().process_boolean_polynomial_witness(
            obligation=obl, input_payload=payload, producer_result=producer,
            experiment_id="EXP-ASSUMPTION", experiment_run_ids=["R"], checker_run_id="C",
        )


def test_v113_counterexample_store_rejects_minimality_downgrade(tmp_path):
    store = CounterexampleStore(tmp_path / "counterexamples")
    from pnp_lab.counterexamples import make_counterexample
    first = make_counterexample(
        "OBL-X", {"assignment": [1]}, reproduced=True, scope="TARGET",
        target_obligation_id="OBL-X", minimality_status="PROVEN_MINIMAL_WITHIN_FINITE_DOMAIN",
    )
    store.put(first)
    downgrade = make_counterexample(
        "OBL-X", {"assignment": [1]}, reproduced=True, scope="TARGET",
        target_obligation_id="OBL-X", minimality_status="LOCALLY_MINIMIZED",
    )
    with pytest.raises(RuntimeError, match="minimality status cannot be downgraded"):
        store.put(downgrade)

# --- v1.13 Checkpoint G: SAT/CNF discovery accelerator ---
import hashlib
import random

from pnp_lab.encoder_registry import (
    EncoderRegistry,
    build_encoder_registry,
    qualify_boolean_circuit_tseitin_encoder,
)
from pnp_lab.sat_backend import (
    SatSolveResult,
    brute_force_cnf_reference,
    discover_sat_capabilities,
    solve_cnf_dpll,
)
from pnp_lab.sat_counterexample import (
    SatCounterexampleEngine,
    SatCounterexampleError,
    validate_circuit_counterexample,
)


def _fixed_circuit_obligation(circuit: dict, expected: int = 0) -> ProofObligation:
    digest = hashlib.sha256(serialize_boolean_circuit(circuit)).hexdigest()
    return _structured_obligation(
        f"for every input to fixed circuit {digest[:12]}, output equals {int(bool(expected))}",
        claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["assignment"]},
        scope_definition={
            "kind": "FINITE_COMPLETE",
            "domain_id": "BOOLEAN_CIRCUIT_INPUTS",
            "circuit_sha256": digest,
        },
        scope=f"all Boolean inputs to fixed circuit {digest}",
        obligation_type="FINITE_CHECK",
        finite_testability="FINITE_COMPLETE",
    )


def test_v113_tseitin_encoder_qualification_is_differential_metamorphic_and_mutation_sensitive():
    q = qualify_boolean_circuit_tseitin_encoder()
    assert q.status == "PASS"
    assert q.golden_tests >= 10
    assert q.differential_tests >= 160
    assert q.metamorphic_tests >= 80
    assert q.mutation_failures_detected >= 2


def test_v113_unqualified_encoder_cannot_generate_authoritative_encoding():
    registry = build_encoder_registry(qualify=False)
    circuit = {"inputs": ["x"], "gates": [{"id": "g", "op": "NOT", "args": ["x"]}], "output": "g"}
    with pytest.raises(RuntimeError, match="not qualified"):
        registry.encode(
            "encoder.boolean.circuit.tseitin.counterexample",
            {"circuit": circuit, "expected_output": 0},
            authoritative=True,
        )
    assert registry.encode(
        "encoder.boolean.circuit.tseitin.counterexample",
        {"circuit": circuit, "expected_output": 0},
        authoritative=False,
    )["clauses"]


def test_v113_builtin_dpll_matches_independent_bruteforce_reference_on_random_small_cnf():
    rng = random.Random(113021)
    checked = 0
    for nvars in range(1, 6):
        for _ in range(60):
            clauses = []
            for _ci in range(rng.randint(0, 8)):
                clause = []
                for _li in range(rng.randint(1, min(4, nvars + 1))):
                    var = rng.randint(1, nvars)
                    clause.append(var if rng.randint(0, 1) else -var)
                clauses.append(clause)
            dpll = solve_cnf_dpll(clauses, nvars, max_nodes=100_000)
            brute = brute_force_cnf_reference(clauses, nvars)
            assert dpll.status in {"SAT", "UNSAT"}
            assert (dpll.status == "SAT") is brute
            checked += 1
    assert checked == 300


def test_v113_sat_capability_discovery_degrades_gracefully_without_optional_pysat():
    caps = discover_sat_capabilities()
    assert caps["builtin_dpll"]["available"] is True
    assert isinstance(caps["pysat"]["available"], bool)
    assert isinstance(caps["pysat"]["available_backends"], list)
    assert isinstance(caps["pysat"]["errors"], list)


def test_v113_sat_witness_is_only_evidence_after_direct_original_semantics_check():
    circuit = {
        "inputs": ["a", "b"],
        "gates": [{"id": "g", "op": "XOR", "args": ["a", "b"]}],
        "output": "g",
    }
    obl = _fixed_circuit_obligation(circuit, expected=0)
    result = SatCounterexampleEngine().search(
        obligation=obl,
        circuit=circuit,
        expected_output=0,
        experiment_id="EXP-SAT-XOR",
        experiment_run_id="ERUN-SAT-DISCOVERY",
        checker_run_id="ERUN-DIRECT-CHECK",
        solver_backend="builtin.dpll",
    )
    assert result.solver_result.status == "SAT"
    assert result.direct_check["status"] == "PASS"
    assert result.evidence is not None
    assert result.evidence.evidence_kind == EvidenceKind.EXACT_COUNTEREXAMPLE.value
    assert result.evidence.verification_method == VerificationMethod.DIRECT_CHECKER.value
    assert "canonical circuit parser" in result.evidence.trusted_components
    assert any("SAT backend" in x for x in result.evidence.untrusted_components)
    assert result.applicability["can_falsify"] is True
    assert result.obligation_assessment.derived_status == "FALSIFIED"


def test_v113_invalid_or_malformed_sat_model_cannot_become_counterexample_evidence(monkeypatch):
    circuit = {
        "inputs": ["a", "b"],
        "gates": [{"id": "g", "op": "XOR", "args": ["a", "b"]}],
        "output": "g",
    }
    obl = _fixed_circuit_obligation(circuit, expected=0)

    # Pretend a solver/encoding path returns a model whose *input assignment*
    # does not violate the original theorem.  The direct evaluator must veto it.
    def fake_solver(*_args, **_kwargs):
        return SatSolveResult("SAT", "mutated.fake", model=[-1, -2, 3])

    monkeypatch.setattr("pnp_lab.sat_counterexample.solve_cnf", fake_solver)
    result = SatCounterexampleEngine().search(
        obligation=obl,
        circuit=circuit,
        expected_output=0,
        experiment_id="EXP-SAT-BAD-MODEL",
        experiment_run_id="ERUN-BAD",
        checker_run_id="ERUN-DIRECT-CHECK",
        solver_backend="builtin.dpll",
    )
    assert result.solver_result.status == "SAT"
    assert result.direct_check["status"] == "FAIL"
    assert result.evidence is None
    assert result.counterexample is None
    assert result.obligation_assessment.derived_status == "OPEN"


def test_v113_uncertified_sat_unsat_has_no_original_theorem_force():
    circuit = {
        "inputs": [],
        "gates": [{"id": "zero", "op": "CONST", "args": [], "value": 0}],
        "output": "zero",
    }
    obl = _fixed_circuit_obligation(circuit, expected=0)
    result = SatCounterexampleEngine().search(
        obligation=obl,
        circuit=circuit,
        expected_output=0,
        experiment_id="EXP-SAT-UNSAT",
        experiment_run_id="ERUN-SAT-UNSAT",
        checker_run_id="ERUN-NOT-USED",
        solver_backend="builtin.dpll",
    )
    assert result.solver_result.status == "UNSAT"
    assert result.solver_result.certified is False
    assert result.evidence is not None
    assert result.evidence.evidence_kind == EvidenceKind.SAT_RESULT.value
    assert result.evidence.logical_polarity == LogicalPolarity.NEUTRAL.value
    assert result.obligation_assessment.derived_status == "OPEN"


def test_v113_sat_counterexample_binding_rejects_wrong_circuit_or_unchecked_assumptions():
    circuit = {"inputs": ["x"], "gates": [{"id": "g", "op": "NOT", "args": ["x"]}], "output": "g"}
    other = {"inputs": ["x"], "gates": [{"id": "g", "op": "XOR", "args": ["x", "x"]}], "output": "g"}
    obl = _fixed_circuit_obligation(circuit, expected=0)
    with pytest.raises(SatCounterexampleError, match="circuit identity"):
        SatCounterexampleEngine().search(
            obligation=obl, circuit=other, expected_output=0,
            experiment_id="EXP-SAT-WRONG", experiment_run_id="R", checker_run_id="C",
            solver_backend="builtin.dpll",
        )

    digest = hashlib.sha256(serialize_boolean_circuit(circuit)).hexdigest()
    constrained = _structured_obligation(
        "for all fixed-circuit inputs satisfying A, output is zero",
        claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["assignment"]},
        scope_definition={
            "kind": "FINITE_COMPLETE", "domain_id": "BOOLEAN_CIRCUIT_INPUTS",
            "circuit_sha256": digest, "assumptions": ["A(assignment)"],
        },
        scope="fixed circuit inputs satisfying A", obligation_type="FINITE_CHECK", finite_testability="FINITE_COMPLETE",
    )
    with pytest.raises(SatCounterexampleError, match="extra structured assumptions"):
        SatCounterexampleEngine().search(
            obligation=constrained, circuit=circuit, expected_output=0,
            experiment_id="EXP-SAT-ASSUMPTION", experiment_run_id="R", checker_run_id="C",
            solver_backend="builtin.dpll",
        )


def test_v113_direct_circuit_counterexample_checker_rejects_nonviolating_assignment():
    circuit = {"inputs": ["x"], "gates": [{"id": "g", "op": "NOT", "args": ["x"]}], "output": "g"}
    assert validate_circuit_counterexample(circuit, 0, {"x": 0})["status"] == "PASS"
    assert validate_circuit_counterexample(circuit, 0, {"x": 1})["status"] == "FAIL"

from pnp_lab.sat_backend import qualify_builtin_dpll


def test_v113_builtin_dpll_has_explicit_bounded_discovery_qualification_and_no_unsat_authority():
    q = qualify_builtin_dpll()
    assert q.status == "PASS"
    assert q.golden_tests >= 5
    assert q.differential_tests == 300
    assert q.resource_limit_tests == 1
    assert q.maximum_qualified_scope["authoritative_unsat"] is False
    assert q.details["unsat_certificate_checked"] is False

# --- v1.13 Checkpoint H: exact symbolic + optional SMT capability boundary ---
from pnp_lab.symbolic_exact import (
    SymbolicExactError,
    check_rational_polynomial_identity,
    independent_check_rational_polynomial_identity,
    qualify_rational_polynomial_identity,
)
from pnp_lab.smt_backend import (
    ALETHE_EXTERNAL_CHECK_POLICY_THEORIES,
    discover_smt_capabilities,
    run_cvc5_smtlib,
    validate_cvc5_finite_field_scope,
)


def test_v113_exact_symbolic_rational_polynomial_identity_has_coefficient_certificate():
    payload = {
        "variables": ["x", "y"],
        "lhs_terms": [
            {"coefficient": 1, "powers": {"x": 2}},
            {"coefficient": 2, "powers": {"x": 1, "y": 1}},
            {"coefficient": 1, "powers": {"y": 2}},
        ],
        "rhs_terms": [
            {"coefficient": [1, 1], "powers": {"y": 2}},
            {"coefficient": [2, 1], "powers": {"x": 1, "y": 1}},
            {"coefficient": [1, 1], "powers": {"x": 2}},
        ],
    }
    result = check_rational_polynomial_identity(payload)
    assert result["status"] == "PASS"
    assert result["difference_terms"] == []
    assert result["certificate_type"] == "ZERO_SPARSE_COEFFICIENT_MAP"
    assert independent_check_rational_polynomial_identity(payload)["status"] == "PASS"


def test_v113_symbolic_nonidentity_is_detected_exactly_by_both_paths():
    payload = {
        "variables": ["x"],
        "lhs_terms": [{"coefficient": 1, "powers": {"x": 2}}],
        "rhs_terms": [{"coefficient": 1, "powers": {"x": 1}}],
    }
    primary = check_rational_polynomial_identity(payload)
    challenger = independent_check_rational_polynomial_identity(payload)
    assert primary["status"] == "FAIL"
    assert primary["difference_terms"]
    assert challenger["status"] == "FAIL"


def test_v113_symbolic_qualification_crosschecks_with_sympy_and_detects_mutation():
    q = qualify_rational_polynomial_identity()
    assert q.status == "PASS"
    assert q.differential_tests == 100
    assert q.mutation_tests == 1


def test_v113_symbolic_instrument_is_qualified_and_has_independent_checker():
    payload = {
        "variables": ["x"],
        "lhs_terms": [
            {"coefficient": [1, 2], "powers": {"x": 1}},
            {"coefficient": [1, 2], "powers": {"x": 1}},
        ],
        "rhs_terms": [{"coefficient": 1, "powers": {"x": 1}}],
    }
    instruments = build_core_instrument_registry(qualify=True)
    checkers = build_core_checker_registry()
    result = instruments.execute("builtin.symbolic.rational_polynomial.identity", payload, authoritative=True)
    checked = checkers.check("checker.symbolic.rational_polynomial.identity.sympy", payload)
    assert result["status"] == "PASS"
    assert checked["status"] == "PASS"


def test_v113_symbolic_scope_rejects_negative_exponents_and_unknown_variables():
    with pytest.raises(SymbolicExactError, match="nonnegative"):
        check_rational_polynomial_identity({
            "variables": ["x"],
            "lhs_terms": [{"coefficient": 1, "powers": {"x": -1}}],
            "rhs_terms": [],
        })
    with pytest.raises(SymbolicExactError, match="unknown polynomial variable"):
        check_rational_polynomial_identity({
            "variables": ["x"],
            "lhs_terms": [{"coefficient": 1, "powers": {"y": 1}}],
            "rhs_terms": [],
        })


def test_v113_cvc5_finite_field_scope_is_prime_order_only_and_never_silently_extension_field():
    assert validate_cvc5_finite_field_scope(2)["status"] == "SUPPORTED"
    assert validate_cvc5_finite_field_scope(7)["status"] == "SUPPORTED"
    assert validate_cvc5_finite_field_scope(4)["status"] == "UNSUPPORTED"
    assert validate_cvc5_finite_field_scope(4, extension_degree=2)["status"] == "UNSUPPORTED"


def test_v113_smt_capability_discovery_is_optional_and_distinguishes_solver_from_external_proof_checker():
    caps = discover_smt_capabilities()
    assert isinstance(caps["cvc5"]["module_available"], bool)
    assert caps["finite_field"]["prime_order_only"] is True
    assert caps["finite_field"]["extension_fields_supported"] is False
    assert caps["alethe"]["requires_independent_checker_for_certificate_evidence"] is True
    assert "QF_FF" not in ALETHE_EXTERNAL_CHECK_POLICY_THEORIES
    assert caps["alethe"]["finite_field_external_check_supported"] is False


def test_v113_cvc5_run_never_labels_unchecked_alethe_output_certified():
    result = run_cvc5_smtlib("(set-logic QF_LIA)\n(assert false)\n(check-sat)\n", theory="QF_LIA", request_alethe_proof=True)
    assert result.status in {"UNSUPPORTED", "UNSAT", "CRASH", "MALFORMED"}
    assert result.certified is False
    assert result.certification_method in {"NONE", "UNVERIFIED_ALETHE_PROOF"}

# --- v1.13 Checkpoint I: resolution planning + adaptive research regime ---
from pnp_lab.research_regime import assess_research_regime, regime_score_adjustment
from pnp_lab.resolution_planner import plan_resolution
from pnp_lab.experiment_scheduler import ExperimentJobCandidate, rank_experiment_jobs
from pnp_lab.resource_governor import ResourceGovernor
from pnp_lab.adaptive_swarm import plan_next_wave
from pnp_lab.branch_selection import score_branch_kinds
from pnp_lab.prompts_v111 import director_portfolio_prompt
from pnp_lab.adaptive_controller import AdaptiveCycleController
from pnp_lab.contracts_v111 import normalize_director_portfolio, selected_director_from_candidate
from pnp_lab.research_portfolio import ResearchCandidate


def _portfolio_record(cycle: int, candidate: str, program: str = ""):
    payload = {"cycle": cycle, "chosen_candidate_id": candidate}
    if program:
        payload["program_allocation"] = {"chosen_program_id": program}
    return {"decision_id": f"ADEC-{cycle:03d}", "decision_type": "PORTFOLIO_SELECTION", "payload": payload, "created_at_utc": f"2026-08-22T00:{cycle:02d}:00Z"}


def test_v113_research_regime_enters_moonshot_only_from_grounded_cross_cycle_stagnation_and_narrowness():
    state = {"cycle": 10, "consecutive_cycle_failures": 0, "grounded_progress_history": [], "cycle_outcomes": [{"cycle": c} for c in range(6, 10)]}
    recent = [_portfolio_record(i, "OBL-SAME", "PROG-SAME") for i in range(3, 11)]
    regime = assess_research_regime(
        state=state,
        recent_records=recent,
        candidates=[{"id": "OBL-SAME", "failure_concentration": .9, "duplication_score": .85}],
        cycle=10,
    )
    assert regime.mode == "MOONSHOT_ESCAPE"
    assert regime.exploration_fraction >= .75
    assert regime.strategic_distance == "CROSS_PROGRAM_MOONSHOT"
    assert regime.budget_multiplier == 1.0
    assert regime.to_dict()["can_promote_claims"] is False


def test_v113_research_regime_broadens_before_moonshot_when_no_progress_is_already_diverse():
    state = {"cycle": 10, "consecutive_cycle_failures": 0, "grounded_progress_history": [], "cycle_outcomes": [{"cycle": c} for c in range(6, 10)]}
    recent = [_portfolio_record(i, f"OBL-{i}") for i in range(3, 11)]
    regime = assess_research_regime(state=state, recent_records=recent, candidates=[], cycle=10)
    assert regime.mode == "BROADEN"
    assert regime.stagnation_pressure < .72
    assert regime.recent_target_repeat_share <= .2


def test_v113_recent_grounded_decisive_progress_contracts_focus_even_after_older_stagnation():
    state = {
        "cycle": 10,
        "consecutive_cycle_failures": 0,
        "grounded_progress_history": [{"cycle": 10, "delta_units": 1, "grounded_progress_units": 5}],
        "obligations": {"OBL-BREAK": {"status": "FALSIFIED", "updated_cycle": 10}},
    }
    recent = [_portfolio_record(i, "OBL-OLD") for i in range(3, 10)]
    regime = assess_research_regime(state=state, recent_records=recent, candidates=[{"duplication_score": 1.0}], cycle=10)
    assert regime.mode == "EXPLOIT_FOCUS"
    assert regime.convergence_strength >= .85
    assert "OBL-BREAK" in regime.recent_decisive_obligation_ids


def test_v113_model_confidence_or_rhetoric_does_not_create_convergence_signal():
    state = {"cycle": 3, "strategy_confidence": 1.0, "director_confidence": 1.0, "grounded_progress_history": []}
    regime = assess_research_regime(state=state, recent_records=[], candidates=[], cycle=3)
    assert regime.mode == "BALANCED"
    assert regime.convergence_strength == 0.0


def test_v113_operational_failure_streak_is_not_misread_as_scientific_stagnation():
    state = {"cycle": 5, "consecutive_cycle_failures": 9, "grounded_progress_history": [], "cycle_outcomes": []}
    regime = assess_research_regime(state=state, recent_records=[], candidates=[], cycle=5)
    assert regime.no_progress_streak == 0
    assert regime.mode == "BALANCED"


def test_v113_moonshot_score_penalty_can_be_softened_only_with_explicit_director_override_rationale():
    regime = {
        "mode": "MOONSHOT_ESCAPE",
        "recent_target_ids": ["OLD"],
        "recent_decisive_obligation_ids": [],
    }
    old = ResearchCandidate.from_mapping({"id": "OLD", "novelty_potential": .5, "bridge_potential": .5, "expected_information_gain": .6, "duplication_score": .7})
    override = ResearchCandidate.from_mapping({"id": "OLD", "novelty_potential": .5, "bridge_potential": .5, "expected_information_gain": .6, "duplication_score": .7, "regime_override_rationale": "The new exact counterexample changes the local statement."})
    a, _ = regime_score_adjustment(old, regime)
    b, reasons = regime_score_adjustment(override, regime)
    assert b > a
    assert any("override" in x.lower() for x in reasons)


def test_v113_saturated_swarm_escapes_basin_in_moonshot_regime_without_losing_verification_reserve():
    signals = [
        {"id": f"S{i}", "summary": "same local mechanism repeated", "target_obligation_id": "OBL-X", "verdict": "NO_PROGRESS"}
        for i in range(8)
    ]
    plan = plan_next_wave(
        signals,
        remaining_slots=12,
        previous_cluster_fingerprints=["OBL:OBL-X"],
        verification_debt=.45,
        bridge_priority=.6,
        min_verification_fraction=.30,
        research_regime={"mode": "MOONSHOT_ESCAPE"},
    )
    strategic_distance_slots = sum(plan.allocation.get(k, 0) for k in ("alternative_formalism", "cross_program_transfer", "assumption_inversion", "moonshot"))
    assert strategic_distance_slots >= 4
    assert plan.verification_fraction >= .30
    assert plan.continue_breadth is True


def test_v113_decisive_counterexample_overrides_moonshot_breadth():
    signals = [{"id": "CX", "summary": "exact witness", "verdict": "EXACT_COUNTEREXAMPLE", "counterexample_signature": "w=001"}]
    plan = plan_next_wave(signals, remaining_slots=10, research_regime={"mode": "MOONSHOT_ESCAPE"})
    assert plan.continue_breadth is False
    assert plan.allocation.get("counterexample_reproduce_minimize", 0) > 0
    assert plan.allocation.get("moonshot", 0) == 0


def test_v113_branch_selection_increases_alternative_formalism_and_wildcard_under_moonshot():
    candidate = {"pnp_leverage": .7, "bridge_potential": .6, "falsifiability": .6, "expected_information_gain": .7, "staleness_score": .7}
    balanced = {x.kind: x.score for x in score_branch_kinds(selected_action="EXPLORE", candidate=candidate, research_regime={"mode": "BALANCED"})}
    moonshot = {x.kind: x.score for x in score_branch_kinds(selected_action="EXPLORE", candidate=candidate, research_regime={"mode": "MOONSHOT_ESCAPE"})}
    assert moonshot["ALTERNATIVE_FORMALISM"] > balanced["ALTERNATIVE_FORMALISM"]
    assert moonshot["WILDCARD"] > balanced["WILDCARD"]


def test_v113_director_prompt_exposes_regime_as_advisory_same_cost_and_allows_reasoned_override():
    prompt = director_portfolio_prompt(
        strategy="attack the blocker",
        frontier_context="OBL-X",
        research_regime={
            "mode": "MOONSHOT_ESCAPE", "stagnation_pressure": .9, "convergence_strength": 0,
            "no_progress_streak": 5, "exploration_fraction": .78, "strategic_distance": "CROSS_PROGRAM_MOONSHOT",
            "recommendations": ["change formalism"],
        },
    )
    assert "MOONSHOT_ESCAPE" in prompt
    assert "inference budget multiplier: 1.0" in prompt
    assert "regime_override_rationale" in prompt
    assert "not an order" in prompt


def test_v113_resolution_planner_keeps_scientific_action_separate_and_preempts_for_cheap_exact_circuit_search():
    obligation = {
        "id": "OBL-CIRCUIT",
        "obligation_type": "FINITE_CHECK",
        "claim_shape": "UNIVERSAL",
        "finite_testability": "FINITE_COMPLETE",
        "scope_definition": {"kind": "FINITE_COMPLETE", "domain_id": "BOOLEAN_CIRCUIT_INPUTS", "circuit_sha256": "abc", "variable_count": 8},
    }
    plan = plan_resolution(obligation, scientific_action="FALSIFY")
    assert plan.scientific_action == "FALSIFY"
    assert plan.preferred_modality == "SAT"
    assert plan.cheap_decisive_preemption is True
    assert any(x.execution_modality == "SAT" for x in plan.options)


def test_v113_resolution_planner_positive_bounded_generalization_never_claims_parent_verification():
    obligation = {
        "id": "OBL-GEN",
        "obligation_type": "GENERALIZATION",
        "claim_shape": "UNIVERSAL",
        "finite_testability": "FINITE_BOUNDED_ONLY",
        "scope_definition": {"kind": "GENERAL", "domain_id": "BOOLEAN_CUBE", "n": 12},
    }
    plan = plan_resolution(obligation, scientific_action="EXPLORE")
    enum = next(x for x in plan.options if x.execution_modality == "EXHAUSTIVE_ENUMERATION")
    assert enum.can_falsify_parent is True
    assert enum.can_verify_parent is False
    assert "RESTRICTED" in enum.decisive_scope
    assert plan.cheap_decisive_preemption is False


def test_v113_experiment_scheduler_prioritizes_cheap_decisive_high_fanout_job():
    ranked = rank_experiment_jobs([
        ExperimentJobCandidate("EXP-CHEAP", scientific_leverage=.9, falsification_value=.9, expected_decisiveness=.95, normalized_compute_cost=.05, dependency_fanout=12, exact_scope=True),
        ExperimentJobCandidate("EXP-HUGE", scientific_leverage=.9, falsification_value=.5, expected_decisiveness=.6, normalized_compute_cost=.95, dependency_fanout=2, exact_scope=False),
    ])
    assert ranked[0].experiment_id == "EXP-CHEAP"
    assert ranked[0].preempt_optional_model_breadth is True


def test_v113_experiment_resource_governor_is_separate_from_llm_budget():
    class S:
        max_research_branches = 4
        initial_research_branches = 2
        max_parallel_model_calls = 8
        max_parallel_serious_model_calls = 4
        max_parallel_verifier_processes = 2
        verification_reserve_fraction = .3
        hard_cycle_usd = 10
        experiment_max_parallel_jobs = 3
        experiment_max_cpu_seconds_per_job = 77
        experiment_max_wall_seconds_per_job = 99
        experiment_max_memory_mb_per_job = 512
        experiment_max_artifact_mb_per_job = 12
    gov = ResourceGovernor(S())
    llm_state = {"cycle": 5, "budget": {"hard_limit_usd": 10, "actual_usd": 0, "reserved_usd": 0}}
    llm = gov.snapshot(llm_state)
    exp = gov.experiment_snapshot({"cycle": 5})
    llm_after = gov.snapshot(llm_state)
    assert llm.model_call_limit == llm_after.model_call_limit
    assert exp.max_parallel_jobs <= 3
    assert exp.max_cpu_seconds_per_job == 77
    assert exp.budget_multiplier == 1.0
    assert exp.to_dict()["separate_from_llm_budget"] is True


def test_v113_controller_persists_regime_resolution_and_preemption_without_truth_authority(tmp_path):
    obligation = {
        "id": "OBL-X", "title": "circuit universal", "statement": "for all x output is zero",
        "status": "OPEN", "obligation_type": "FINITE_CHECK", "finite_testability": "FINITE_COMPLETE",
        "claim_shape": "UNIVERSAL", "quantifier_structure": {"prefix": ["FORALL"], "variables": ["x"]},
        "scope_definition": {"kind": "FINITE_COMPLETE", "domain_id": "BOOLEAN_CIRCUIT_INPUTS", "circuit_sha256": "abc", "variable_count": 6},
        "source_run_ids": [], "counterexample_ids": [], "evidence_ids": [], "verification_result_ids": [], "objection_ids": [],
    }
    state = {"cycle": 7, "obligations": {"OBL-X": obligation}, "claims": {}, "counterexamples": {}, "objections": {}, "grounded_progress_history": []}
    controller = AdaptiveCycleController(tmp_path / "decisions", require_sync_receipt=False)
    decision = controller.choose_target(
        candidates=[{"id": "OBL-X", "title": "X", "target": "resolve X", "source_ids": ["OBL-X"], "pnp_leverage": .9, "falsifiability": .9, "expected_information_gain": .9}],
        state=state, branch_revisions=[], recent_records=[], cycle=7,
    )
    assert decision["research_regime"]["can_promote_claims"] is False
    assert decision["resolution_plan"]["scientific_action"] == decision["chosen_action"]
    assert decision["experiment_preemption"]["recommended"] is True
    assert decision["experiment_preemption"]["adds_model_calls"] is False
    assert decision["decision_id"].startswith("ADEC-")


def test_v113_selected_director_carries_regime_and_resolution_metadata_only():
    portfolio = normalize_director_portfolio({
        "candidates": [{"id": "X", "target": "X", "regime_override_rationale": ""}],
        "portfolio_rationale": "", "must_not_repeat": [], "strategy_confidence": .5,
    }, min_candidates=0)
    decision = {
        "chosen_candidate_id": "X", "chosen_action": "EXPLORE", "decision_id": "ADEC-X",
        "research_regime": {"mode": "BROADEN"}, "resolution_plan": {"preferred_modality": "MODEL_REASONING"},
        "experiment_preemption": {"recommended": False},
    }
    selected = selected_director_from_candidate(portfolio["candidates"][0], decision, portfolio)
    assert selected["research_regime"]["mode"] == "BROADEN"
    assert selected["resolution_plan"]["preferred_modality"] == "MODEL_REASONING"
    assert selected["adaptive_metadata_only"] is True

from pnp_lab.experiment_datasets import (
    ExperimentDatasetStore,
    conjecture_to_open_obligation_proposal,
    make_conjecture_proposal,
    mine_simple_exact_patterns,
    test_conjecture_on_holdout as run_conjecture_holdout,
)
from pnp_lab.output_schemas import schema_for
from pnp_lab.prompts import experimental_mathematician_prompt
from pnp_lab.theorem_graph import TheoremGraph


def _dataset(store, *, experiment_id="EXP-0123456789abcdefabcd", rows=None, role="DISCOVERY", seed=None, sampling="EXACT_GENERATED"):
    return store.write_exact_dataset(
        experiment_id=experiment_id,
        rows=rows or [{"n": 1, "rank": 1, "ok": 1}, {"n": 2, "rank": 2, "ok": 1}],
        row_schema={"n": "int", "rank": "int", "ok": "bit"},
        domain_definition={"kind": "FINITE_FAMILY", "n_min": 1, "n_max": 2},
        generator_instrument_id="builtin.test.generator",
        generator_instrument_version="1",
        coverage={"coverage_complete": True},
        sampling_method=sampling,
        random_seed=seed,
        split_role=role,
        source_run_ids=["ERUN-DATA"],
        created_cycle=19,
    )


def test_v113_exact_dataset_is_content_addressed_schema_bound_and_reloads_with_hash_check(tmp_path):
    store = ExperimentDatasetStore(tmp_path / "scientific_record")
    ds = _dataset(store)
    rows = store.load_rows(ds.dataset_id)
    assert ds.dataset_id.startswith("DATASET-")
    assert ds.row_count == 2
    assert rows[1]["rank"] == 2
    assert ds.rows_blob_id.startswith("BLOB-")
    same = _dataset(store)
    assert same.dataset_id == ds.dataset_id


def test_v113_stochastic_dataset_requires_explicit_seed(tmp_path):
    store = ExperimentDatasetStore(tmp_path / "scientific_record")
    with pytest.raises(ValueError):
        _dataset(store, sampling="RANDOM_SAMPLE", seed=None)
    seeded = _dataset(store, sampling="RANDOM_SAMPLE", seed=17)
    assert seeded.random_seed == 17


def test_v113_simple_pattern_miner_outputs_conjecture_only_not_proof(tmp_path):
    store = ExperimentDatasetStore(tmp_path / "scientific_record")
    ds = _dataset(store, rows=[{"a": 0, "b": 0, "ok": 1}, {"a": 1, "b": 1, "ok": 1}])
    patterns = mine_simple_exact_patterns(ds, store.load_rows(ds.dataset_id))
    assert any(p.predicate.get("kind") == "COLUMN_EQUALS_VALUE" and p.predicate.get("column") == "ok" for p in patterns)
    assert any(p.predicate.get("kind") == "COLUMN_EQUALS_COLUMN" and {p.predicate.get("left"), p.predicate.get("right")} == {"a", "b"} for p in patterns)
    assert all(p.can_promote_claims is False and p.epistemic_role == "CONJECTURE_ONLY" for p in patterns)
    assert all("open" in p.generalization_gap.lower() for p in patterns)


def test_v113_heldout_must_be_fresh_and_success_still_cannot_promote(tmp_path):
    store = ExperimentDatasetStore(tmp_path / "scientific_record")
    discovery = _dataset(store, rows=[{"x": 0, "ok": 1}, {"x": 1, "ok": 1}])
    proposal = make_conjecture_proposal(
        title="ok invariant", statement="ok is always 1", predicate={"kind": "COLUMN_EQUALS_VALUE", "column": "ok", "value": 1},
        source_dataset_ids=[discovery.dataset_id], falsification_semantics="find ok != 1", generalization_gap="finite discovery data only",
    )
    with pytest.raises(ValueError):
        run_conjecture_holdout(proposal, discovery, store.load_rows(discovery.dataset_id))
    holdout = store.write_exact_dataset(
        experiment_id="EXP-fedcba9876543210abcd", rows=[{"x": 2, "ok": 1}, {"x": 3, "ok": 1}],
        row_schema={"x": "int", "ok": "bit"}, domain_definition={"kind": "FINITE_FAMILY", "n_min": 3, "n_max": 4},
        generator_instrument_id="builtin.test.generator", generator_instrument_version="1", coverage={"coverage_complete": True}, split_role="HOLDOUT",
    )
    test = run_conjecture_holdout(proposal, holdout, store.load_rows(holdout.dataset_id))
    assert test.status == "HELD_OUT_SUPPORTED"
    assert test.checked_rows == 2
    assert test.can_promote_claims is False
    assert test.epistemic_role == "PRIORITY_FILTER_ONLY"


def test_v113_heldout_counterexample_falsifies_pattern_without_touching_theorem_status(tmp_path):
    store = ExperimentDatasetStore(tmp_path / "scientific_record")
    discovery = _dataset(store, rows=[{"x": 0, "ok": 1}, {"x": 1, "ok": 1}])
    proposal = make_conjecture_proposal(
        title="ok invariant", statement="ok is always 1", predicate={"kind": "COLUMN_EQUALS_VALUE", "column": "ok", "value": 1},
        source_dataset_ids=[discovery.dataset_id], falsification_semantics="find ok != 1", generalization_gap="finite discovery data only",
    )
    holdout = store.write_exact_dataset(
        experiment_id="EXP-aaaaaaaaaaaaaaaaaaaa", rows=[{"x": 2, "ok": 1}, {"x": 3, "ok": 0}],
        row_schema={"x": "int", "ok": "bit"}, domain_definition={"kind": "FINITE_FAMILY", "n_min": 3, "n_max": 4},
        generator_instrument_id="builtin.test.generator", generator_instrument_version="1", coverage={"coverage_complete": True}, split_role="HOLDOUT",
    )
    test = run_conjecture_holdout(proposal, holdout, store.load_rows(holdout.dataset_id))
    assert test.status == "HELD_OUT_FALSIFIED"
    assert test.first_counterexample == {"x": 3, "ok": 0}
    assert test.can_promote_claims is False


def test_v113_experimental_conjecture_to_obligation_is_open_and_has_no_inherited_evidence():
    proposal = make_conjecture_proposal(
        title="rank law", statement="For every object in the family, rank equals n.",
        predicate={"kind": "COLUMN_EQUALS_COLUMN", "left": "rank", "right": "n"},
        source_dataset_ids=["DATASET-0123456789abcdefabcd"], falsification_semantics="find rank != n",
        generalization_gap="observed only for bounded generated objects",
    )
    obl = conjecture_to_open_obligation_proposal(
        proposal, scope="arbitrary n", quantifiers="forall n and objects", computational_model="exact finite combinatorial model",
        claim_shape="UNIVERSAL", quantifier_structure={"prefix": ["FORALL"], "variables": ["x"]},
        scope_definition={"kind": "GENERAL", "domain_id": "OBJECT_FAMILY"}, finite_testability="FINITE_BOUNDED_ONLY", cycle=19,
    )
    assert obl.status == "OPEN"
    assert obl.evidence_ids == []
    assert obl.load_bearing is False
    assert "held-out tests do not prove" in obl.status_reason


def test_v113_theorem_graph_can_represent_experiment_dataset_conjecture_without_truth_edge():
    state = {
        "obligations": {"OBL-X": {"id": "OBL-X", "title": "X", "statement": "X", "status": "OPEN"}},
        "experiments": {"EXP-X": {"experiment_id": "EXP-X", "target_obligation_id": "OBL-X"}},
        "experiment_datasets": {"DATASET-X": {"dataset_id": "DATASET-X", "experiment_id": "EXP-X"}},
        "conjectures": {"CONJ-X": {"conjecture_id": "CONJ-X", "source_dataset_ids": ["DATASET-X"], "target_obligation_id": "OBL-X"}},
    }
    graph = TheoremGraph.from_state(state, obligations=[])
    relations = {(e["source_id"], e["target_id"], e["relation"]) for e in graph.edges}
    assert ("EXP-X", "OBL-X", "EXPERIMENT_TESTS_OBLIGATION") in relations
    assert ("EXP-X", "DATASET-X", "EXPERIMENT_GENERATES_DATASET") in relations
    assert ("DATASET-X", "CONJ-X", "DATASET_SUPPORTS_CONJECTURE") in relations
    assert ("EXP-X", "CONJ-X", "EXPERIMENT_GENERATES_CONJECTURE") in relations
    assert ("CONJ-X", "OBL-X", "CONJECTURE_SUGGESTS_OBLIGATION") in relations
    assert ("CONJ-X", "OBL-X", "EVIDENCE_SUPPORTS_OBLIGATION") not in relations


def test_v113_experimental_mathematician_contract_and_prompt_forbid_proof_promotion():
    schema = schema_for("EXPERIMENTAL_MATHEMATICIAN")
    assert schema and "conjectures" in schema["properties"]
    system, user = experimental_mathematician_prompt(
        {"dataset_id": "DATASET-X", "experiment_id": "EXP-X", "row_count": 2, "domain_definition": {"n": 2}},
        [{"rank": 1}, {"rank": 1}],
    )
    assert "CONJECTURE_GENERATION_ONLY" in user
    assert "held-out" in user.lower()
    assert "do not call any pattern a theorem" in user.lower()
    assert "Never claim P=NP" in system

from pnp_lab.formal_bridge import (
    DEFAULT_LEAN_TOOLCHAIN,
    LeanCapabilitySnapshot,
    LeanKernelResult,
    audit_lean_axioms,
    build_formal_proof_evidence,
    canonical_informal_hash,
    check_lean_source_policy,
    discover_lean_capabilities,
    make_fidelity_review,
    make_formalization_record,
    run_lean_kernel_check,
    validate_formalization_binding,
)
from pnp_lab.obligation_policy import evaluate_obligation_status
from pnp_lab.schemas import ProofObligation
from pnp_lab.prompts import formal_fidelity_review_prompt, formalization_prompt


def _formal_obligation(scope=None):
    return ProofObligation(
        id="OBL-FORMAL",
        title="Boolean identity",
        statement="For every Boolean x, x AND false equals false.",
        obligation_type="LEMMA",
        scope="all Boolean x",
        quantifiers="forall x in Bool",
        computational_model="Boolean algebra",
        claim_shape="UNIVERSAL",
        quantifier_structure={"prefix": ["FORALL"], "variables": ["x"]},
        scope_definition=scope or {"kind": "GENERAL", "domain_id": "BOOL", "statement_version": 1},
        status="OPEN",
    )


def _formal_source():
    return """theorem pnp_v113_bool_and_false (x : Bool) : (x && false) = false := by\n  cases x <;> rfl\n"""


def _formal_record(obl=None, source=None):
    obl = obl or _formal_obligation()
    return make_formalization_record(
        obligation=obl,
        formal_statement="∀ x : Bool, x && false = false",
        theorem_name="pnp_v113_bool_and_false",
        definition_mapping={"Boolean": "Bool", "AND": "Bool.and"},
        assumption_mapping={"explicit_assumptions": "none"},
        quantifier_mapping={"forall x in Bool": "(x : Bool)"},
        scope_mapping={"all Boolean x": "Bool"},
        lean_source=source or _formal_source(),
        toolchain_identifier=DEFAULT_LEAN_TOOLCHAIN,
        generator_model_family="deepseek-v4-pro",
        created_cycle=20,
    )


def test_v113_lean_capability_discovery_is_feature_gated_and_pinned():
    cap = discover_lean_capabilities(formal_root="formal")
    assert isinstance(cap.available, bool)
    assert cap.configured_toolchain == "leanprover/lean4:v4.33.0"
    assert len(cap.configured_toolchain_sha256) == 64
    assert open("formal/lean-toolchain", encoding="utf-8").read().strip() == cap.configured_toolchain


def test_v113_lean_source_policy_rejects_sorry_admit_new_axiom_and_unsafe_but_ignores_comments():
    assert check_lean_source_policy(_formal_source()).status == "PASS"
    assert "SORRY_FORBIDDEN" in check_lean_source_policy("theorem t : True := by sorry").violations
    assert "ADMIT_FORBIDDEN" in check_lean_source_policy("theorem t : True := by admit").violations
    assert "NEW_AXIOM_DECLARATION_FORBIDDEN" in check_lean_source_policy("axiom magic : False").violations
    assert "NEW_CONSTANT_DECLARATION_FORBIDDEN" in check_lean_source_policy("constant magic : False").violations
    assert "UNSAFE_DECLARATION_FORBIDDEN" in check_lean_source_policy("unsafe def x := 1").violations
    assert check_lean_source_policy("-- sorry is discussed here\ntheorem t : True := by trivial").status == "PASS"


def test_v113_fidelity_pass_requires_independent_model_family_all_mapping_checks_and_no_mismatch():
    obl = _formal_obligation()
    with pytest.raises(ValueError):
        make_fidelity_review(
            obligation=obl, verdict="PASS", reviewer_model_family="deepseek", generator_model_family="deepseek",
            definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=True, scope_mapping_checked=True,
        )
    with pytest.raises(ValueError):
        make_fidelity_review(
            obligation=obl, verdict="PASS", reviewer_model_family="glm", generator_model_family="deepseek",
            definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=False, scope_mapping_checked=True,
        )
    review = make_fidelity_review(
        obligation=obl, verdict="PASS", reviewer_model_family="glm-5.3", generator_model_family="deepseek-v4-pro",
        definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=True, scope_mapping_checked=True,
    )
    assert review.verdict == "PASS"
    assert review.independent_model_family is True
    assert review.can_promote_claims is False


def test_v113_formalization_binding_is_hash_bound_to_current_canonical_obligation():
    obl = _formal_obligation()
    record = _formal_record(obl)
    assert validate_formalization_binding(obl, record) == []
    record.canonical_informal_statement_sha256 = "0" * 64
    assert "canonical informal statement hash mismatch" in validate_formalization_binding(obl, record)


def test_v113_kernel_runner_returns_unsupported_without_lean_not_false_failure(monkeypatch):
    monkeypatch.setattr("pnp_lab.formal_bridge.discover_lean_capabilities", lambda **_: LeanCapabilitySnapshot(False, configured_toolchain=DEFAULT_LEAN_TOOLCHAIN))
    result = run_lean_kernel_check(_formal_source(), theorem_name="pnp_v113_bool_and_false", formal_root="formal")
    assert result.status == "UNSUPPORTED"
    assert result.axiom_report["reason"] == "Lean binary unavailable"


def test_v113_axiom_audit_allows_only_standard_lean_math_axioms_and_rejects_custom_or_sorry():
    no_axioms = audit_lean_axioms("'t' does not depend on any axioms", theorem_name="t")
    assert no_axioms["status"] == "PASS" and no_axioms["used_axioms"] == []
    standard = audit_lean_axioms("'t' depends on axioms: [propext, Classical.choice, Quot.sound]", theorem_name="t")
    assert standard["status"] == "PASS"
    custom = audit_lean_axioms("'t' depends on axioms: [propext, magic.custom]", theorem_name="t")
    assert custom["status"] == "FAIL" and custom["forbidden_axioms"] == ["magic.custom"]
    sorry = audit_lean_axioms("'t' depends on axioms: [sorryAx]", theorem_name="t")
    assert sorry["status"] == "FAIL"
    unknown = audit_lean_axioms("unexpected printer output", theorem_name="t")
    assert unknown["status"] == "UNKNOWN"


def test_v113_kernel_runner_rejects_runtime_toolchain_mismatch(monkeypatch):
    monkeypatch.setattr("pnp_lab.formal_bridge.discover_lean_capabilities", lambda **_: LeanCapabilitySnapshot(True, "/fake/lean", "Lean 4.32.0", "", DEFAULT_LEAN_TOOLCHAIN, "d" * 64))
    result = run_lean_kernel_check(_formal_source(), theorem_name="pnp_v113_bool_and_false", formal_root="formal")
    assert result.status == "TOOLCHAIN_MISMATCH"


def test_v113_kernel_runner_pass_is_bound_to_exact_source_and_collects_axiom_output(monkeypatch):
    monkeypatch.setattr("pnp_lab.formal_bridge.discover_lean_capabilities", lambda **_: LeanCapabilitySnapshot(True, "/fake/lean", "Lean 4.33.0", "", DEFAULT_LEAN_TOOLCHAIN, "d" * 64))
    class P:
        returncode = 0
        stdout = "'pnp_v113_bool_and_false' depends on axioms: []\n"
        stderr = ""
    monkeypatch.setattr("pnp_lab.formal_bridge.subprocess.run", lambda *a, **k: P())
    result = run_lean_kernel_check(_formal_source(), theorem_name="pnp_v113_bool_and_false", formal_root="formal")
    assert result.status == "PASS"
    assert result.lean_version == "Lean 4.33.0"
    assert result.source_sha256 == check_lean_source_policy(_formal_source()).source_sha256
    assert result.axiom_report["status"] == "PASS"
    assert result.axiom_report["used_axioms"] == []


def test_v113_formal_evidence_requires_fidelity_and_kernel_then_can_verify_exact_matching_obligation():
    obl = _formal_obligation()
    source = _formal_source()
    record = _formal_record(obl, source)
    review = make_fidelity_review(
        obligation=obl, verdict="PASS", reviewer_model_family="glm-5.3", generator_model_family="deepseek-v4-pro",
        definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=True, scope_mapping_checked=True,
    )
    kernel = LeanKernelResult("PASS", record.theorem_name, 0, axiom_report={"status": "PASS", "used_axioms": [], "allowed_axioms": ["Classical.choice", "Quot.sound", "propext"], "forbidden_axioms": []}, source_sha256=record.lean_source_sha256, toolchain=DEFAULT_LEAN_TOOLCHAIN, lean_version="Lean 4.33.0")
    evidence = build_formal_proof_evidence(
        obligation=obl, record=record, fidelity_review=review, kernel_result=kernel,
        experiment_id="EXP-formal0123456789abcd", kernel_run_id="ERUN-LEAN-1",
    )
    assessment = evaluate_obligation_status(obl, evidence=[evidence])
    assert record.kernel_status == "PASS"
    assert record.axiom_report["status"] == "PASS"
    assert review.review_id in record.fidelity_review_ids
    assert record.evidence_id == evidence.evidence_id
    assert evidence.evidence_kind == "FORMAL_PROOF"
    assert evidence.verification_method == "LEAN_KERNEL"
    assert assessment.derived_status == "VERIFIED"
    assert "V113_QUANTIFIER_SCOPE_APPLICABILITY" in assessment.satisfied_gates


def test_v113_formal_kernel_pass_without_fidelity_or_with_scope_mismatch_is_insufficient():
    obl = _formal_obligation()
    record = _formal_record(obl)
    bad_review = make_fidelity_review(
        obligation=obl, verdict="UNCERTAIN", reviewer_model_family="glm-5.3", generator_model_family="deepseek-v4-pro",
        definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=True, scope_mapping_checked=False,
    )
    kernel = LeanKernelResult("PASS", record.theorem_name, 0, axiom_report={"status": "PASS", "used_axioms": [], "allowed_axioms": ["Classical.choice", "Quot.sound", "propext"], "forbidden_axioms": []}, source_sha256=record.lean_source_sha256, toolchain=DEFAULT_LEAN_TOOLCHAIN)
    with pytest.raises(ValueError):
        build_formal_proof_evidence(
            obligation=obl, record=record, fidelity_review=bad_review, kernel_result=kernel,
            experiment_id="EXP-formal0123456789abcd", kernel_run_id="ERUN-LEAN-1",
        )
    good = make_fidelity_review(
        obligation=obl, verdict="PASS", reviewer_model_family="glm-5.3", generator_model_family="deepseek-v4-pro",
        definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=True, scope_mapping_checked=True,
    )
    ev = build_formal_proof_evidence(
        obligation=obl, record=record, fidelity_review=good, kernel_result=kernel,
        experiment_id="EXP-formal0123456789abcd", kernel_run_id="ERUN-LEAN-1",
    )
    ev.tested_scope["domain_id"] = "SMALLER_BOOL_SUBTYPE"
    assert evaluate_obligation_status(obl, evidence=[ev]).derived_status != "VERIFIED"


def test_v113_formal_evidence_rejects_kernel_pass_without_axiom_audit_or_wrong_toolchain():
    obl = _formal_obligation()
    record = _formal_record(obl)
    review = make_fidelity_review(
        obligation=obl, verdict="PASS", reviewer_model_family="glm", generator_model_family="deepseek-v4-pro",
        definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=True, scope_mapping_checked=True,
    )
    no_audit = LeanKernelResult("PASS", record.theorem_name, 0, source_sha256=record.lean_source_sha256, toolchain=DEFAULT_LEAN_TOOLCHAIN)
    with pytest.raises(ValueError, match="axioms audit"):
        build_formal_proof_evidence(obligation=obl, record=record, fidelity_review=review, kernel_result=no_audit, experiment_id="EXP-formal0123456789abcd", kernel_run_id="ERUN-LEAN-X")
    wrong_toolchain = LeanKernelResult("PASS", record.theorem_name, 0, axiom_report={"status": "PASS"}, source_sha256=record.lean_source_sha256, toolchain="leanprover/lean4:v4.32.0")
    with pytest.raises(ValueError, match="exact recorded Lean toolchain"):
        build_formal_proof_evidence(obligation=obl, record=record, fidelity_review=review, kernel_result=wrong_toolchain, experiment_id="EXP-formal0123456789abcd", kernel_run_id="ERUN-LEAN-X")


def test_v113_source_policy_failure_blocks_formal_evidence_even_with_fake_kernel_pass():
    obl = _formal_obligation()
    record = _formal_record(obl, "theorem pnp_v113_bool_and_false : True := by sorry\n")
    assert record.source_policy_status == "FAIL"
    review = make_fidelity_review(
        obligation=obl, verdict="PASS", reviewer_model_family="glm", generator_model_family="deepseek-v4-pro",
        definition_mapping_checked=True, assumption_mapping_checked=True, quantifier_mapping_checked=True, scope_mapping_checked=True,
    )
    kernel = LeanKernelResult("PASS", record.theorem_name, 0, axiom_report={"status": "PASS", "used_axioms": [], "allowed_axioms": ["Classical.choice", "Quot.sound", "propext"], "forbidden_axioms": []}, source_sha256=record.lean_source_sha256, toolchain=DEFAULT_LEAN_TOOLCHAIN)
    with pytest.raises(ValueError):
        build_formal_proof_evidence(
            obligation=obl, record=record, fidelity_review=review, kernel_result=kernel,
            experiment_id="EXP-formal0123456789abcd", kernel_run_id="ERUN-LEAN-1",
        )


def test_v113_formalization_graph_edges_are_contextual_and_evidence_support_is_explicit():
    state = {
        "obligations": {"OBL-X": {"id": "OBL-X", "title": "X", "statement": "X", "status": "OPEN"}},
        "formalizations": {"FORM-X": {"formalization_id": "FORM-X", "target_obligation_id": "OBL-X", "evidence_id": "EVID-FORMAL", "created_cycle": 20}},
    }
    graph = TheoremGraph.from_state(state, obligations=[])
    relations = {(e["source_id"], e["target_id"], e["relation"]) for e in graph.edges}
    assert ("FORM-X", "OBL-X", "FORMALIZATION_ENCODES_OBLIGATION") in relations
    assert ("EVID-FORMAL", "OBL-X", "FORMAL_PROOF_SUPPORTS_OBLIGATION") in relations


def test_v113_formal_prompts_force_mapping_fidelity_and_no_sorry():
    obl = _formal_obligation().to_dict()
    _, formal_user = formalization_prompt(obl, "definitions")
    _, fidelity_user = formal_fidelity_review_prompt(obl, {"formal_statement": "..."}, "glm-5.3", "deepseek-v4-pro")
    assert "sorry/admit" in formal_user
    assert "map every informal definition" in formal_user.lower()
    assert "proof of the wrong theorem" in fidelity_user.lower()
    assert schema_for("FORMALIZER") is not None
    assert schema_for("FORMAL_FIDELITY_REVIEW") is not None

from pathlib import Path
import hashlib
import json
import shutil
import zipfile

from pnp_lab.config import Settings
from pnp_lab.experiment_datasets import ExperimentDatasetStore
from pnp_lab.experiment_schemas import CertificateArtifact
from pnp_lab.handoff import create_research_handoff_bundle
from pnp_lab.persistence import MarkdownBrain
from pnp_lab.scientific_handoff import (
    build_scientific_record_index,
    build_toolchain_capability_snapshot,
    collect_scientific_record_members,
    select_scientific_handoff_files,
    verify_handoff_manifest,
    restore_scientific_record_snapshot,
)
from pnp_lab.state import StateStore


def _v113_temp_settings(tmp_path: Path) -> Settings:
    settings = Settings()
    settings.version = "1.13"
    settings.persistent_root = tmp_path
    settings.brain_dir = tmp_path / "brain"
    settings.runtime_dir = tmp_path / "runtime"
    settings.hf_token = ""
    settings.operator_token = ""
    settings.require_operator_token = False
    settings.integrity_check_on_boot = False
    settings.run_inference_preflight = False
    settings.auto_start = False
    settings.handoff_bundle_max_file_bytes = 8_000_000
    settings.handoff_bundle_max_total_bytes = 64_000_000
    settings.handoff_import_max_files = 128
    settings.ensure_dirs()
    return settings


def test_v113_experiment_store_persists_certificate_and_formalization_with_manifest_roles(tmp_path):
    root = tmp_path / "scientific-record"
    store = ExperimentStore(root)
    spec = _spec(target_obligation_id="OBL-FORMAL")
    store.write_spec(spec)
    blob = store.put_artifact(b"checked-proof-certificate", role="solver_certificate", media_type="application/octet-stream")
    cert = CertificateArtifact(
        certificate_id="CERT-TEST-1",
        certificate_type="TEST_CERTIFICATE",
        producer_instrument="builtin.test",
        target_experiment=spec.id,
        target_obligation="OBL-FORMAL",
        artifact_path=blob.relative_path,
        sha256=blob.sha256,
        checker_id="checker.test",
        checker_result="PASS",
    )
    store.write_certificate(cert)
    record = _formal_record(_formal_obligation())
    store.write_formalization(spec.id, record)
    manifest = store.rebuild_manifest(spec.id)
    roles = {row["role"] for row in manifest["files"]}
    assert "certificate" in roles
    assert "formalization" in roles
    assert store.verify_manifest(spec.id)["status"] == "PASS"
    bad = CertificateArtifact(
        certificate_id="CERT-BAD",
        certificate_type="TEST",
        producer_instrument="builtin.test",
        target_experiment=spec.id,
        target_obligation="OBL-WRONG",
        artifact_path=blob.relative_path,
        sha256=blob.sha256,
    )
    with pytest.raises(ValueError, match="target obligation"):
        store.write_certificate(bad)


def test_v113_scientific_handoff_selects_typed_records_and_only_small_referenced_blobs(tmp_path):
    root = tmp_path / "scientific-record"
    dataset_store = ExperimentDatasetStore(root)
    record = dataset_store.write_exact_dataset(
        experiment_id="EXP-0123456789abcdefghij",
        rows=[{"x": 0, "rank": 0}, {"x": 1, "rank": 1}],
        row_schema={"x": "bit", "rank": "int"},
        domain_definition={"kind": "FINITE_COMPLETE", "n": 1},
        generator_instrument_id="builtin.dataset",
        generator_instrument_version="1",
        coverage={"coverage_complete": True},
    )
    # An unreferenced historical blob must not be recursively swept into handoff.
    unreferenced = dataset_store.artifacts.put_bytes(b"orphan", role="orphan")
    selected, report = select_scientific_handoff_files(root, max_files=50, max_file_bytes=1_000_000, small_blob_max_bytes=1_000_000)
    rels = {p.relative_to(root).as_posix() for p in selected}
    assert f"datasets/{record.dataset_id}.json" in rels
    assert record.rows_blob_id in report["embedded_blob_ids"]
    assert unreferenced.blob_id not in report["embedded_blob_ids"]
    assert f"blobs/sha256/{record.rows_sha256[:2]}/{record.rows_sha256[2:]}" in rels
    assert report["large_blobs_recursive_embedding"] is False


def test_v113_scientific_handoff_fails_closed_on_missing_referenced_blob(tmp_path):
    root = tmp_path / "scientific-record"
    dataset_store = ExperimentDatasetStore(root)
    record = dataset_store.write_exact_dataset(
        experiment_id="EXP-0123456789abcdefghij", rows=[{"x": 0}],
        row_schema={"x": "bit"}, domain_definition={"kind": "FINITE_COMPLETE", "n": 0},
        generator_instrument_id="builtin.dataset", generator_instrument_version="1",
    )
    blob_path = dataset_store.artifacts.path_for_sha256(record.rows_sha256)
    blob_path.unlink()
    with pytest.raises(RuntimeError, match="missing/corrupt referenced blobs"):
        collect_scientific_record_members(root)


def test_v113_scientific_record_index_reports_experiment_manifest_integrity(tmp_path):
    root = tmp_path / "scientific-record"
    store = ExperimentStore(root)
    spec = _spec()
    store.write_spec(spec)
    index = build_scientific_record_index(root)
    row = next(x for x in index["experiments"] if x["experiment_id"] == spec.id)
    assert row["integrity"]["status"] == "PASS"
    (store.experiment_dir(spec.id) / "spec.json").write_text("{}\n", encoding="utf-8")
    broken = build_scientific_record_index(root)
    row2 = next(x for x in broken["experiments"] if x["experiment_id"] == spec.id)
    assert row2["integrity"]["status"] == "FAIL"


def test_v113_toolchain_snapshot_is_descriptive_and_contains_pinned_lean_without_secrets():
    snapshot = build_toolchain_capability_snapshot(Path.cwd())
    assert snapshot["secrets_included"] is False
    assert snapshot["runtime_google_credentials_required"] is False
    assert snapshot["lean"]["configured_toolchain"] == DEFAULT_LEAN_TOOLCHAIN
    assert "sat" in snapshot and "smt" in snapshot and "instrument_registry" in snapshot and "checker_registry" in snapshot


def test_v113_whole_lab_handoff_carries_scientific_records_hashes_and_readback_verification(tmp_path):
    settings = _v113_temp_settings(tmp_path)
    brain = MarkdownBrain(settings)
    brain.initialize()
    state_store = StateStore(settings)
    spec = _spec()
    exp_store = ExperimentStore(settings.scientific_record_dir)
    exp_store.write_spec(spec)
    path = create_research_handoff_bundle(settings, state_store.snapshot(), brain)
    assert verify_handoff_manifest(path)["status"] == "PASS"
    sidecar = path.with_name(path.name + ".sha256")
    assert sidecar.is_file()
    expected = sidecar.read_text(encoding="utf-8").split()[0]
    assert expected == hashlib.sha256(path.read_bytes()).hexdigest()
    latest = settings.handoff_dir / "pnp-lab-research-handoff-latest.zip"
    latest_sha = latest.with_name(latest.name + ".sha256")
    assert latest.is_file() and latest_sha.is_file()
    with zipfile.ZipFile(path) as archive:
        names = set(archive.namelist())
        assert "11_V113_SCIENTIFIC_RECORD_INDEX.json" in names
        assert "12_V113_TOOLCHAIN_CAPABILITIES.json" in names
        assert f"scientific_record/experiments/{spec.id}/spec.json" in names
        manifest = json.loads(archive.read("MANIFEST.json"))
        assert manifest["scientific_record_selection"]["large_blobs_recursive_embedding"] is False


def test_v113_scientific_handoff_restore_is_hash_checked_idempotent_and_collision_safe(tmp_path):
    settings = _v113_temp_settings(tmp_path / "source")
    brain = MarkdownBrain(settings)
    brain.initialize()
    spec = _spec()
    exp_store = ExperimentStore(settings.scientific_record_dir)
    spec_path = exp_store.write_spec(spec)
    original = spec_path.read_bytes()
    bundle = create_research_handoff_bundle(settings, StateStore(settings).snapshot(), brain)

    restored_root = tmp_path / "restored" / "scientific-record"
    report = restore_scientific_record_snapshot(bundle, restored_root)
    assert report["status"] == "PASS" and report["restored_count"] > 0
    restored_spec = restored_root / "experiments" / spec.id / "spec.json"
    assert restored_spec.read_bytes() == original
    again = restore_scientific_record_snapshot(bundle, restored_root)
    assert again["status"] == "PASS" and again["restored_count"] == 0 and again["reused_count"] == again["file_count"]

    restored_spec.write_text("{}\n", encoding="utf-8")
    with pytest.raises(RuntimeError, match="collision"):
        restore_scientific_record_snapshot(bundle, restored_root)


def test_v113_handoff_manifest_readback_detects_corruption(tmp_path):
    path = tmp_path / "bad.zip"
    with zipfile.ZipFile(path, "w") as archive:
        payload = b"hello"
        archive.writestr("x.txt", payload)
        archive.writestr("MANIFEST.json", json.dumps({"files": [{"path": "x.txt", "bytes": 5, "sha256": "0" * 64}]}))
    report = verify_handoff_manifest(path)
    assert report["status"] == "FAIL"
    assert any("sha256 mismatch" in x for x in report["errors"])


def test_v113_state_schema_initializes_scientific_entity_reference_maps(tmp_path):
    settings = _v113_temp_settings(tmp_path)
    state = StateStore(settings).snapshot()
    for key in ("experiments", "evidence_artifacts", "experiment_datasets", "conjectures", "certificates", "formalizations", "counterexamples"):
        assert key in state and state[key] == {}


def test_v113_scientific_subbundle_restore_is_hash_checked_idempotent_and_nonpromoting(tmp_path):
    import zipfile
    from pnp_lab.scientific_handoff import collect_scientific_record_members, restore_scientific_record_snapshot, MANIFEST_NAME
    source = tmp_path / "source"
    exp = ExperimentStore(source)
    spec = _spec()
    exp.write_spec(spec)
    blob = exp.put_artifact({"witness": [1, 0]}, role="checked_witness")
    exp.write_artifact_ref(spec.id, blob)
    bundle = collect_scientific_record_members(source)
    archive = tmp_path / "handoff.zip"
    with zipfile.ZipFile(archive, "w") as z:
        rows = []
        for rel, raw in bundle.members:
            name = "scientific_record/" + rel
            z.writestr(name, raw)
            rows.append({"path": name, "bytes": len(raw), "sha256": hashlib.sha256(raw).hexdigest(), "source": "fixture"})
        manifest_raw = json.dumps(bundle.manifest, indent=2, sort_keys=True).encode()
        z.writestr("scientific_record/" + MANIFEST_NAME, manifest_raw)
        rows.append({"path": "scientific_record/" + MANIFEST_NAME, "bytes": len(manifest_raw), "sha256": hashlib.sha256(manifest_raw).hexdigest(), "source": "fixture"})
        z.writestr("MANIFEST.json", json.dumps({"files": rows}))
    dest = tmp_path / "dest"
    first = restore_scientific_record_snapshot(archive, dest)
    second = restore_scientific_record_snapshot(archive, dest)
    assert first["status"] == "PASS" and first["restored_count"] > 0
    assert second["restored_count"] == 0 and second["reused_count"] == first["file_count"]
    assert "canonical theorem state unchanged" in first["authority"]
    assert (dest / "experiments" / spec.id / "spec.json").is_file()


def test_v113_scientific_restore_collision_aborts_before_writing_other_records(tmp_path):
    import zipfile
    from pnp_lab.scientific_handoff import collect_scientific_record_members, restore_scientific_record_snapshot, MANIFEST_NAME
    source = tmp_path / "source"
    exp = ExperimentStore(source); spec = _spec(); exp.write_spec(spec)
    bundle = collect_scientific_record_members(source)
    archive = tmp_path / "handoff.zip"
    with zipfile.ZipFile(archive, "w") as z:
        for rel, raw in bundle.members:
            z.writestr("scientific_record/" + rel, raw)
        z.writestr("scientific_record/" + MANIFEST_NAME, json.dumps(bundle.manifest))
    dest = tmp_path / "dest"
    collision = dest / "experiments" / spec.id / "spec.json"
    collision.parent.mkdir(parents=True)
    collision.write_text("corrupt", encoding="utf-8")
    before = {p.relative_to(dest).as_posix() for p in dest.rglob("*") if p.is_file()}
    with pytest.raises(RuntimeError, match="collision"):
        restore_scientific_record_snapshot(archive, dest)
    after = {p.relative_to(dest).as_posix() for p in dest.rglob("*") if p.is_file()}
    assert after == before


def test_v113_missing_referenced_blob_is_explicitly_incomplete_and_blocks_whole_handoff(tmp_path):
    settings = _v113_temp_settings(tmp_path)
    brain = MarkdownBrain(settings); brain.initialize()
    exp = ExperimentStore(settings.scientific_record_dir)
    spec = _spec(); exp.write_spec(spec)
    ref = exp.put_artifact({"witness": [1]}, role="checked_witness")
    exp.write_artifact_ref(spec.id, ref)
    (settings.scientific_record_dir / ref.relative_path).unlink()
    selected, report = select_scientific_handoff_files(settings.scientific_record_dir)
    assert report["status"] == "INCOMPLETE"
    assert any(row["reason"] == "MISSING_LOCAL_BLOB" for row in report["critical_omissions"])
    with pytest.raises(RuntimeError, match="missing/corrupt referenced blobs"):
        create_research_handoff_bundle(settings, StateStore(settings).snapshot(), brain)

# ---- Checkpoint M release-hardening gaps ---------------------------------
from pnp_lab.experiment_cache import ExperimentCache, build_experiment_cache_key
from pnp_lab.custom_code_policy import custom_code_capability, lint_custom_code, require_custom_code_execution
from pnp_lab.certificate_policy import assess_certificate_checker_result, invalidate_evidence_for_checker_failure
from pnp_lab.evidence_headers import collect_evidence_scope_headers, evidence_scope_header


def test_v113_exact_cache_is_toolchain_aware_and_never_counts_as_reproduction(tmp_path):
    root = tmp_path / "scientific"
    store = ExperimentStore(root)
    executor = ExperimentExecutor(store)
    cache = ExperimentCache(root)
    spec = make_experiment_spec(
        target_obligation_id="OBL-CACHE", scientific_action="VERIFY", execution_modality="BUILTIN_EXACT",
        question="evaluate", claim_shape="EXISTENTIAL", quantifier_structure={"prefix": ["EXISTS"]},
        tested_scope={"kind": "FINITE_COMPLETE", "n": 1}, domain_definition={"kind": "BOOLEAN_CUBE", "n": 1},
        success_semantics="exact output", falsification_semantics="mismatch", instrument_id="builtin.boolean.polynomial.evaluate",
        instrument_version_constraint="==1", input_payload={"polynomial": [[0]], "assignment": [1]},
        checker_plan={"checker_id": "checker.boolean.polynomial.output"}, reproduction_policy={"required": False},
    )
    first = executor.execute_with_cache(spec, cache, encoder_version="enc-1", encoder_sha256="a" * 64)
    assert first["status"] == "EXECUTED" and first["creates_new_run"] is True
    before = len(store.load_runs(spec.id))
    second = executor.execute_with_cache(spec, cache, encoder_version="enc-1", encoder_sha256="a" * 64)
    assert second["status"] == "CACHE_HIT"
    assert second["independent_reproduction_credit"] is False and second["creates_new_run"] is False
    assert len(store.load_runs(spec.id)) == before
    # Scientifically relevant encoder change is a cache miss/new execution.
    third = executor.execute_with_cache(spec, cache, encoder_version="enc-2", encoder_sha256="b" * 64)
    assert third["status"] == "EXECUTED"
    assert len(store.load_runs(spec.id)) == before + 1


def test_v113_cache_key_changes_with_seed_and_toolchain():
    a = _spec(instrument_id="builtin.boolean.polynomial.evaluate", instrument_version_constraint="==1", input_payload={"polynomial": [], "assignment": []})
    k1 = build_experiment_cache_key(a, instrument_version="1", instrument_binary_sha256="a"*64, toolchain_digest="tool-A")
    k2 = build_experiment_cache_key(a, instrument_version="1", instrument_binary_sha256="a"*64, toolchain_digest="tool-B")
    assert k1.cache_key != k2.cache_key
    b = _spec(instrument_id="builtin.boolean.polynomial.evaluate", instrument_version_constraint="==1", input_payload={"polynomial": [], "assignment": []}, determinism="STOCHASTIC", random_seed=7)
    c = _spec(instrument_id="builtin.boolean.polynomial.evaluate", instrument_version_constraint="==1", input_payload={"polynomial": [], "assignment": []}, determinism="STOCHASTIC", random_seed=8)
    kb = build_experiment_cache_key(b, instrument_version="1", instrument_binary_sha256="a"*64, toolchain_digest="tool-A")
    kc = build_experiment_cache_key(c, instrument_version="1", instrument_binary_sha256="a"*64, toolchain_digest="tool-A")
    assert kb.cache_key != kc.cache_key


def test_v113_custom_generated_code_is_disabled_without_strong_sandbox(monkeypatch):
    monkeypatch.delenv("PNP_STRONG_SANDBOX_BACKEND", raising=False)
    cap = custom_code_capability(requested_enabled=True, require_strong_sandbox=True)
    assert cap.execution_allowed is False and cap.authoritative_evidence_allowed is False
    with pytest.raises(RuntimeError, match="strong sandbox unavailable"):
        require_custom_code_execution(requested_enabled=True, require_strong_sandbox=True)
    disabled = custom_code_capability(requested_enabled=False)
    assert disabled.execution_allowed is False


def test_v113_custom_code_lint_rejects_network_process_file_and_dynamic_execution():
    bad = lint_custom_code("import subprocess\nopen('x','w')\neval('1+1')\n")
    assert bad.status == "FAIL"
    assert any("subprocess" in x for x in bad.violations)
    assert any("forbidden call: open" in x for x in bad.violations)
    assert any("forbidden call: eval" in x for x in bad.violations)
    good = lint_custom_code("from fractions import Fraction\nx = Fraction(1, 3)\n")
    assert good.status == "PASS"
    assert "not a security boundary" in good.note


def test_v113_failed_certificate_checker_invalidates_and_quarantines_evidence():
    cert = CertificateArtifact(
        certificate_id="CERT-X", certificate_type="UNSAT_PROOF", producer_instrument="solver-x",
        target_experiment="EXP-X", target_obligation="OBL-X", artifact_path="certificates/x.proof",
        sha256="a"*64, checker_id="checker-x", checker_version="1", checker_result="FAIL", checker_run_id="ERUN-CHECK-X",
    )
    decision = assess_certificate_checker_result(cert)
    assert decision.status == "QUARANTINED" and decision.evidence_valid is False
    assert decision.quarantine_required and decision.instrument_incident_required
    ev = EvidenceArtifact(
        evidence_id="EVID-X", target_obligation_id="OBL-X", experiment_id="EXP-X",
        evidence_kind=EvidenceKind.SOLVER_CERTIFIED_RESULT.value, verification_method=VerificationMethod.PROOF_CHECKER.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value, tested_scope={"kind":"FINITE_COMPLETE","n":1,"coverage_complete":True,"coverage_checked":True},
        certificate_ids=["CERT-X"], checker_run_ids=["ERUN-CHECK-X"],
    )
    invalid = invalidate_evidence_for_checker_failure(ev, decision)
    assert invalid.applicability_status == "INVALID"
    assert "must not carry proof force" in invalid.applicability_reason


def test_v113_applicability_honors_upstream_invalid_evidence():
    from pnp_lab.evidence_applicability import assess_applicability
    from pnp_lab.schemas import ProofObligation
    obl = ProofObligation(
        id="OBL-X", title="finite", statement="forall x", status="OPEN", obligation_type="LEMMA",
        claim_shape="UNIVERSAL", quantifier_structure={"prefix":["FORALL"]}, scope_definition={"kind":"FINITE_COMPLETE","n":1},
    )
    ev = EvidenceArtifact(
        evidence_id="EVID-X", target_obligation_id="OBL-X", experiment_id="EXP-X",
        evidence_kind=EvidenceKind.FINITE_EXHAUSTIVE_RESULT.value, verification_method=VerificationMethod.PROOF_CHECKER.value,
        logical_polarity=LogicalPolarity.SUPPORTS.value, tested_scope={"kind":"FINITE_COMPLETE","n":1,"coverage_complete":True,"coverage_checked":True},
        checker_run_ids=["ERUN-CHECK"], applicability_status="INVALID", applicability_reason="checker failed",
    )
    app = assess_applicability(obl, ev)
    assert app.status == "INVALID" and not app.can_verify and not app.can_falsify


def test_v113_machine_evidence_headers_make_scope_and_trust_explicit():
    ev = EvidenceArtifact(
        evidence_id="EVID-H", target_obligation_id="OBL-H", experiment_id="EXP-H",
        evidence_kind=EvidenceKind.EXACT_COUNTEREXAMPLE.value, verification_method=VerificationMethod.SMALL_INDEPENDENT_CHECKER.value,
        logical_polarity=LogicalPolarity.FALSIFIES.value, tested_scope={"kind":"INSTANCE"},
        does_establish=["falsifies exact universal"], does_not_establish=["no broader theorem"],
        trusted_components=["tiny checker"], untrusted_components=["SAT discovery"], independent_reproduction_status="CHECKED",
    )
    h = evidence_scope_header(ev)
    assert h["RESULT_TYPE"] == "EXACT_COUNTEREXAMPLE"
    assert h["TARGET_OBLIGATION"] == "OBL-H"
    assert h["DOES_NOT_ESTABLISH"] == ["no broader theorem"]
    assert h["TRUSTED_COMPONENTS"] == ["tiny checker"]
    assert collect_evidence_scope_headers({"nested": [ev.to_dict()]})[0]["EVIDENCE_ID"] == "EVID-H"


def test_v113_settings_default_custom_code_closed_and_cache_enabled(monkeypatch):
    for name in ("CUSTOM_EXPERIMENT_CODE_ENABLED", "CUSTOM_EXPERIMENT_REQUIRE_STRONG_SANDBOX", "EXPERIMENT_CACHE_ENABLED"):
        monkeypatch.delenv(name, raising=False)
    settings = Settings()
    assert settings.custom_experiment_code_enabled is False
    assert settings.custom_experiment_require_strong_sandbox is True
    assert settings.experiment_cache_enabled is True


def test_v113_cache_hit_refuses_missing_or_corrupt_result_blob(tmp_path):
    root = tmp_path / "scientific"
    store = ExperimentStore(root); cache = ExperimentCache(root); executor = ExperimentExecutor(store)
    spec = make_experiment_spec(
        target_obligation_id="OBL-CACHE-INTEGRITY", scientific_action="VERIFY", execution_modality="BUILTIN_EXACT",
        question="evaluate", claim_shape="EXISTENTIAL", quantifier_structure={"prefix":["EXISTS"]},
        tested_scope={"kind":"FINITE_COMPLETE","n":1}, domain_definition={"kind":"BOOLEAN_CUBE","n":1},
        success_semantics="exact", falsification_semantics="mismatch", instrument_id="builtin.boolean.polynomial.evaluate",
        instrument_version_constraint="==1", input_payload={"polynomial":[],"assignment":[0]},
        checker_plan={"checker_id":"checker.boolean.polynomial.output"}, reproduction_policy={"required":False},
    )
    first = executor.execute_with_cache(spec, cache)
    blob = store.artifacts.path_for_sha256(first["result_blob_id"].removeprefix("BLOB-"))
    blob.unlink()
    with pytest.raises(RuntimeError, match="result blob failed integrity"):
        executor.execute_with_cache(spec, cache)


def test_v113_sandbox_binary_presence_is_not_qualification(monkeypatch):
    import pnp_lab.custom_code_policy as ccp
    monkeypatch.setenv("PNP_STRONG_SANDBOX_BACKEND", "bubblewrap")
    monkeypatch.delenv("PNP_STRONG_SANDBOX_QUALIFIED", raising=False)
    monkeypatch.setattr(ccp.shutil, "which", lambda name: "/usr/bin/bwrap" if name == "bwrap" else None)
    cap = ccp.custom_code_capability(requested_enabled=True, require_strong_sandbox=True)
    assert cap.execution_allowed is False and cap.strong_sandbox_available is False
    monkeypatch.setenv("PNP_STRONG_SANDBOX_QUALIFIED", "true")
    cap2 = ccp.custom_code_capability(requested_enabled=True, require_strong_sandbox=True)
    assert cap2.execution_allowed is True and cap2.authoritative_evidence_allowed is False


def test_v113_certificate_pass_without_checker_qualification_is_inconclusive():
    cert = CertificateArtifact(
        certificate_id="CERT-PASS", certificate_type="UNSAT_PROOF", producer_instrument="solver-x",
        target_experiment="EXP-X", target_obligation="OBL-X", artifact_path="x.proof", sha256="a"*64,
        checker_id="unknown-checker", checker_version="9", checker_result="PASS", checker_run_id="ERUN-CHECK-X",
    )
    unknown = assess_certificate_checker_result(cert)
    assert unknown.status == "INCONCLUSIVE" and not unknown.evidence_valid
    attested = assess_certificate_checker_result(cert, checker_qualified=True)
    assert attested.status == "PASS" and attested.evidence_valid