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