Add minimal GAP reproduction package

8 files changed, 605 insertions, 0 deletions

diff --git a/tests/conftest.py b/tests/conftest.py
new file mode 100644
index 0000000..80ccc2e
--- /dev/null
+++ b/tests/conftest.py
@@ -0,0 +1,126 @@
+from __future__ import annotations
+
+import copy
+
+import pytest
+
+from gap_pipeline.models import CanonicalItem
+
+
+@pytest.fixture
+def item() -> CanonicalItem:
+    return CanonicalItem(
+        item_id="demo-A-1",
+        problem=r"Let \(a>0\). Prove that \(a+1/a\ge 2\).",
+        solution=(
+            r"Since \((a-1)^2\ge0\), expanding gives \(a^2-2a+1\ge0\). "
+            r"Divide by \(a>0\) to obtain \(a+1/a\ge2\)."
+        ),
+        variables=["a"],
+        problem_type="proof",
+    )
+
+
+@pytest.fixture
+def dag_dict() -> dict:
+    return {
+        "nodes": [
+            {
+                "node_id": "n1",
+                "claim": "(a-1)^2 >= 0",
+                "derivation": "a square is nonnegative",
+                "dependencies": [],
+                "source_span": "Since (a-1)^2 >= 0",
+                "mathematical_objects": ["a", "(a-1)^2"],
+            },
+            {
+                "node_id": "n2",
+                "claim": "a+1/a >= 2",
+                "derivation": "expand and divide by positive a",
+                "dependencies": ["n1"],
+                "source_span": "Divide by a>0",
+                "mathematical_objects": ["a"],
+            },
+        ],
+        "terminal_node_id": "n2",
+    }
+
+
+@pytest.fixture
+def plan_dict() -> dict:
+    return {
+        "steps": [
+            {
+                "node_id": "n1",
+                "method_label": "use nonnegativity of a square",
+                "input_roles": ["positive scalar"],
+                "output_role": "nonnegative expression",
+                "invariants": ["scalar is real"],
+            },
+            {
+                "node_id": "n2",
+                "method_label": "expand and divide by a positive quantity",
+                "input_roles": ["nonnegative expression", "positive scalar"],
+                "output_role": "target inequality",
+                "invariants": ["divisor is positive"],
+            },
+        ],
+        "terminal_node_id": "n2",
+    }
+
+
+@pytest.fixture
+def replacement_dict() -> dict:
+    return {
+        "target_node_id": "n1",
+        "original_object": "(a-1)^2",
+        "replacement_object": "(x-2)^2",
+        "guard_conditions": ["x>0"],
+        "guard_evidence": ["choose x in the positive reals"],
+        "expected_downstream_changes": ["expand around 2", "divide by x"],
+        "rationale": "the same square-nonnegativity plan applies",
+    }
+
+
+@pytest.fixture
+def diffused_dict(plan_dict: dict) -> dict:
+    return {
+        "node_instantiations": [
+            {
+                "node_id": "n1",
+                "method_label": plan_dict["steps"][0]["method_label"],
+                "instantiated_claim": "(x-2)^2 >= 0",
+                "instantiated_derivation": "a square is nonnegative",
+                "dependencies": [],
+            },
+            {
+                "node_id": "n2",
+                "method_label": plan_dict["steps"][1]["method_label"],
+                "instantiated_claim": "x+4/x >= 4",
+                "instantiated_derivation": "expand and divide by positive x",
+                "dependencies": ["n1"],
+            },
+        ],
+        "regenerated_proof": (
+            "Since (x-2)^2 >= 0, expand and divide by x>0 to get x+4/x >= 4."
+        ),
+        "terminal_answer": "x+4/x >= 4",
+    }
+
+
+@pytest.fixture
+def candidate_dict(replacement_dict: dict, diffused_dict: dict) -> dict:
+    return {
+        "problem": "Let x>0. Prove that x+4/x >= 4.",
+        "proof": diffused_dict["regenerated_proof"],
+        "terminal_answer": diffused_dict["terminal_answer"],
+        "node_instantiations": diffused_dict["node_instantiations"],
+        "replacement": replacement_dict,
+    }
+
+
+def changed_candidate(candidate: dict, suffix: str) -> dict:
+    value = copy.deepcopy(candidate)
+    value["problem"] = value["problem"] + f" [{suffix}]"
+    value["proof"] = value["proof"] + f" Repair {suffix}."
+    return value
diff --git a/tests/test_e2e.py b/tests/test_e2e.py
new file mode 100644
index 0000000..9da1190
--- /dev/null
+++ b/tests/test_e2e.py
@@ -0,0 +1,30 @@
+from __future__ import annotations
+
+import asyncio
+import json
+from pathlib import Path
+
+from gap_pipeline.e2e import run_offline_smoke
+
+
+def test_offline_end_to_end_smoke(tmp_path: Path) -> None:
+    result = asyncio.run(run_offline_smoke(tmp_path / "e2e"))
+    assert result["mode"] == "offline-smoke"
+    assert result["surface_families"] == [
+        "descriptive_long",
+        "descriptive_long_confusing",
+        "descriptive_long_misleading",
+        "garbled_string",
+    ]
+    assert result["kernel_status"] == "accepted"
+    assert result["verification_rounds"] == 2
+    assert result["export_status"] == "complete"
+    assert result["exported_item_count"] == 1
+    record = json.loads(Path(result["release_record"]).read_text())
+    assert set(record["variants"]) == {
+        "descriptive_long",
+        "descriptive_long_confusing",
+        "descriptive_long_misleading",
+        "garbled_string",
+        "kernel_variant",
+    }
diff --git a/tests/test_models.py b/tests/test_models.py
new file mode 100644
index 0000000..2c678a0
--- /dev/null
+++ b/tests/test_models.py
@@ -0,0 +1,71 @@
+from __future__ import annotations
+
+import pytest
+from pydantic import ValidationError
+
+from gap_pipeline.models import (
+    DiffusedProof,
+    MethodPlan,
+    ProofDAG,
+    ReplacementSpec,
+)
+
+
+def test_valid_dag_and_plan(dag_dict: dict, plan_dict: dict) -> None:
+    dag = ProofDAG.model_validate(dag_dict)
+    assert [node.node_id for node in dag.topological_nodes()] == ["n1", "n2"]
+    assert dag.leaf_node_ids() == ["n1"]
+    plan = MethodPlan.model_validate(plan_dict)
+    plan.validate_against(dag)
+
+
+def test_cycle_is_rejected(dag_dict: dict) -> None:
+    dag_dict["nodes"][0]["dependencies"] = ["n2"]
+    with pytest.raises(ValidationError, match="cycle"):
+        ProofDAG.model_validate(dag_dict)
+
+
+def test_node_disconnected_from_terminal_is_rejected(dag_dict: dict) -> None:
+    dag_dict["nodes"].append(
+        {
+            "node_id": "orphan",
+            "claim": "unused claim",
+            "derivation": "unused derivation",
+            "dependencies": [],
+            "source_span": "",
+            "mathematical_objects": [],
+        }
+    )
+    with pytest.raises(ValidationError, match="disconnected"):
+        ProofDAG.model_validate(dag_dict)
+
+
+def test_method_reordering_is_rejected(dag_dict: dict, plan_dict: dict) -> None:
+    dag = ProofDAG.model_validate(dag_dict)
+    plan_dict["steps"].reverse()
+    plan = MethodPlan.model_validate(plan_dict)
+    with pytest.raises(ValueError, match="topological order"):
+        plan.validate_against(dag)
+
+
+def test_replacement_must_target_leaf(
+    dag_dict: dict, replacement_dict: dict
+) -> None:
+    dag = ProofDAG.model_validate(dag_dict)
+    replacement_dict["target_node_id"] = "n2"
+    replacement = ReplacementSpec.model_validate(replacement_dict)
+    with pytest.raises(ValueError, match="not a DAG leaf"):
+        replacement.validate_against(dag)
+
+
+def test_diffusion_cannot_change_dag_dependencies(
+    dag_dict: dict,
+    plan_dict: dict,
+    diffused_dict: dict,
+) -> None:
+    dag = ProofDAG.model_validate(dag_dict)
+    plan = MethodPlan.model_validate(plan_dict)
+    diffused_dict["node_instantiations"][1]["dependencies"] = []
+    diffused = DiffusedProof.model_validate(diffused_dict)
+    with pytest.raises(ValueError, match="changes dependencies"):
+        diffused.validate_against(dag, plan)
diff --git a/tests/test_offline.py b/tests/test_offline.py
new file mode 100644
index 0000000..04b7f46
--- /dev/null
+++ b/tests/test_offline.py
@@ -0,0 +1,6 @@
+from gap_pipeline.offline import normalize_latex_symbol
+
+
+def test_latex_symbol_aliases_normalize_together() -> None:
+    assert normalize_latex_symbol(r"x_{n}") == normalize_latex_symbol("x_n")
+    assert normalize_latex_symbol(r"\\phi") == normalize_latex_symbol(r"\phi")
diff --git a/tests/test_pipeline.py b/tests/test_pipeline.py
new file mode 100644
index 0000000..ea1077a
--- /dev/null
+++ b/tests/test_pipeline.py
@@ -0,0 +1,236 @@
+from __future__ import annotations
+
+import asyncio
+import json
+
+from gap_pipeline.clients import ScriptedClient
+from gap_pipeline.pipeline import KernelPipeline, PipelineConfig
+from gap_pipeline.store import RunStore
+
+from conftest import changed_candidate
+
+
+def accept_verdict() -> dict:
+    return {
+        "verdict": "accept",
+        "step_by_step_check": "n1 passes; n2 passes",
+        "blocking_issues": "",
+        "patch_suggestion": "",
+    }
+
+
+def reject_verdict(iteration: int) -> dict:
+    return {
+        "verdict": "reject",
+        "step_by_step_check": f"n1 passes; n2 fails at iteration {iteration}",
+        "blocking_issues": "the terminal algebra needs correction",
+        "patch_suggestion": "correct the terminal algebra without changing the plan",
+    }
+
+
+def proposer_responses(
+    item_id: str,
+    dag_dict: dict,
+    plan_dict: dict,
+    replacement_dict: dict,
+    diffused_dict: dict,
+    candidate_dict: dict,
+) -> dict:
+    return {
+        f"{item_id}.stage1": dag_dict,
+        f"{item_id}.stage2": plan_dict,
+        f"{item_id}.stage3": replacement_dict,
+        f"{item_id}.stage4": diffused_dict,
+        f"{item_id}.stage5": candidate_dict,
+    }
+
+
+def test_two_consecutive_unanimous_passes_accept(
+    tmp_path,
+    item,
+    dag_dict,
+    plan_dict,
+    replacement_dict,
+    diffused_dict,
+    candidate_dict,
+) -> None:
+    proposer = ScriptedClient(
+        proposer_responses(
+            item.item_id,
+            dag_dict,
+            plan_dict,
+            replacement_dict,
+            diffused_dict,
+            candidate_dict,
+        )
+    )
+    judges = [
+        ScriptedClient({f"{item.item_id}.verify": [accept_verdict(), accept_verdict()]})
+        for _ in range(5)
+    ]
+    pipeline = KernelPipeline(
+        proposer=proposer,
+        judges=judges,
+        store=RunStore(tmp_path, item.item_id),
+        config=PipelineConfig(proposer_model="scripted", judge_model="scripted"),
+    )
+    result = asyncio.run(pipeline.run(item))
+    assert result.status == "accepted"
+    assert len(result.iterations) == 2
+    assert [row.pass_streak_after for row in result.iterations] == [1, 2]
+    assert not any(row.repaired for row in result.iterations)
+
+    final_path = tmp_path / "items" / item.item_id / "final.json"
+    final = json.loads(final_path.read_text())
+    assert final["human_audit_selected"] in {True, False}
+    assert len(list((final_path.parent / "calls").glob("*.json"))) == 15
+
+
+def test_rejection_resets_streak_and_repairs(
+    tmp_path,
+    item,
+    dag_dict,
+    plan_dict,
+    replacement_dict,
+    diffused_dict,
+    candidate_dict,
+) -> None:
+    repaired = changed_candidate(candidate_dict, "fixed")
+    responses = proposer_responses(
+        item.item_id,
+        dag_dict,
+        plan_dict,
+        replacement_dict,
+        diffused_dict,
+        candidate_dict,
+    )
+    responses[f"{item.item_id}.repair"] = repaired
+    proposer = ScriptedClient(responses)
+    judges = []
+    for judge_id in range(1, 6):
+        first = reject_verdict(1) if judge_id == 1 else accept_verdict()
+        judges.append(
+            ScriptedClient(
+                {
+                    f"{item.item_id}.verify": [
+                        first,
+                        accept_verdict(),
+                        accept_verdict(),
+                    ]
+                }
+            )
+        )
+    pipeline = KernelPipeline(
+        proposer=proposer,
+        judges=judges,
+        store=RunStore(tmp_path, item.item_id),
+        config=PipelineConfig(proposer_model="scripted", judge_model="scripted"),
+    )
+    result = asyncio.run(pipeline.run(item))
+    assert result.status == "accepted"
+    assert len(result.iterations) == 3
+    assert result.iterations[0].repaired
+    assert [row.pass_streak_after for row in result.iterations] == [0, 1, 2]
+    assert (
+        result.iterations[0].repaired_candidate_sha256
+        == result.iterations[1].candidate_sha256
+        == result.iterations[2].candidate_sha256
+    )
+
+
+def test_rejection_after_one_pass_resets_streak_on_new_candidate(
+    tmp_path,
+    item,
+    dag_dict,
+    plan_dict,
+    replacement_dict,
+    diffused_dict,
+    candidate_dict,
+) -> None:
+    repaired = changed_candidate(candidate_dict, "after-broken-streak")
+    responses = proposer_responses(
+        item.item_id,
+        dag_dict,
+        plan_dict,
+        replacement_dict,
+        diffused_dict,
+        candidate_dict,
+    )
+    responses[f"{item.item_id}.repair"] = repaired
+    proposer = ScriptedClient(responses)
+    judges = []
+    for judge_id in range(1, 6):
+        second = reject_verdict(2) if judge_id == 3 else accept_verdict()
+        judges.append(
+            ScriptedClient(
+                {
+                    f"{item.item_id}.verify": [
+                        accept_verdict(),
+                        second,
+                        accept_verdict(),
+                        accept_verdict(),
+                    ]
+                }
+            )
+        )
+    pipeline = KernelPipeline(
+        proposer=proposer,
+        judges=judges,
+        store=RunStore(tmp_path, item.item_id),
+        config=PipelineConfig(proposer_model="scripted", judge_model="scripted"),
+    )
+    result = asyncio.run(pipeline.run(item))
+    assert result.status == "accepted"
+    assert [row.pass_streak_after for row in result.iterations] == [1, 0, 1, 2]
+    assert result.iterations[0].candidate_sha256 == result.iterations[1].candidate_sha256
+    assert result.iterations[1].repaired_candidate_sha256 != result.iterations[1].candidate_sha256
+    assert (
+        result.iterations[1].repaired_candidate_sha256
+        == result.iterations[2].candidate_sha256
+        == result.iterations[3].candidate_sha256
+    )
+
+
+def test_fifteen_failed_rounds_reject(
+    tmp_path,
+    item,
+    dag_dict,
+    plan_dict,
+    replacement_dict,
+    diffused_dict,
+    candidate_dict,
+) -> None:
+    responses = proposer_responses(
+        item.item_id,
+        dag_dict,
+        plan_dict,
+        replacement_dict,
+        diffused_dict,
+        candidate_dict,
+    )
+    responses[f"{item.item_id}.repair"] = [
+        changed_candidate(candidate_dict, f"repair-{iteration}")
+        for iteration in range(1, 15)
+    ]
+    proposer = ScriptedClient(responses)
+    judges = [
+        ScriptedClient(
+            {
+                f"{item.item_id}.verify": [
+                    reject_verdict(iteration) for iteration in range(1, 16)
+                ]
+            }
+        )
+        for _ in range(5)
+    ]
+    pipeline = KernelPipeline(
+        proposer=proposer,
+        judges=judges,
+        store=RunStore(tmp_path, item.item_id),
+        config=PipelineConfig(proposer_model="scripted", judge_model="scripted"),
+    )
+    result = asyncio.run(pipeline.run(item))
+    assert result.status == "rejected"
+    assert len(result.iterations) == 15
+    assert sum(row.repaired for row in result.iterations) == 14
+    assert all(row.pass_streak_after == 0 for row in result.iterations)
diff --git a/tests/test_release.py b/tests/test_release.py
new file mode 100644
index 0000000..3653ff1
--- /dev/null
+++ b/tests/test_release.py
@@ -0,0 +1,80 @@
+from __future__ import annotations
+
+import json
+
+import pytest
+
+from gap_pipeline.models import KernelCandidate
+from gap_pipeline.release import export_release
+from gap_pipeline.store import RunStore, sha256_payload
+from gap_pipeline.surface import SURFACE_FAMILIES
+
+
+def test_offline_release_export_verifies_and_assembles(
+    tmp_path,
+    item,
+    candidate_dict,
+) -> None:
+    source_dir = tmp_path / "source"
+    source_dir.mkdir()
+    source_record = {
+        "index": item.item_id,
+        "question": item.problem,
+        "solution": item.solution,
+        "vars": item.variables,
+        "params": [],
+        "sci_consts": [],
+        "problem_type": "proof",
+        "variants": {},
+    }
+    (source_dir / f"{item.item_id}.json").write_text(
+        json.dumps(source_record),
+        encoding="utf-8",
+    )
+
+    surface_root = tmp_path / "surface-runs"
+    surface_store = RunStore(surface_root, item.item_id)
+    for family in SURFACE_FAMILIES:
+        surface_store.write_stage(
+            f"surface_{family}_variant",
+            {
+                "map": {"a": f"name{family.replace('_', '')}"},
+                "question": f"{family} question",
+                "solution": f"{family} solution",
+            },
+            request_id=None,
+        )
+
+    kernel_root = tmp_path / "kernel-runs"
+    kernel_store = RunStore(kernel_root, item.item_id)
+    candidate = KernelCandidate.model_validate(candidate_dict)
+    kernel_store.write_final(
+        {
+            "item_id": item.item_id,
+            "status": "accepted",
+            "accepted_candidate": candidate.model_dump(mode="json"),
+            "accepted_candidate_sha256": sha256_payload(candidate),
+        }
+    )
+
+    output_root = tmp_path / "release"
+    manifest = export_release(
+        source_dataset=source_dir,
+        surface_run_root=surface_root,
+        kernel_run_root=kernel_root,
+        output_root=output_root,
+    )
+    assert manifest["status"] == "complete"
+    assert manifest["exported_item_count"] == 1
+    output = json.loads(
+        (output_root / "records" / f"{item.item_id}.json").read_text()
+    )
+    assert set(output["variants"]) == {*SURFACE_FAMILIES, "kernel_variant"}
+    assert output["variants"]["kernel_variant"]["question"] == candidate.problem
+    with pytest.raises(FileExistsError):
+        export_release(
+            source_dataset=source_dir,
+            surface_run_root=surface_root,
+            kernel_run_root=kernel_root,
+            output_root=output_root,
+        )
diff --git a/tests/test_store.py b/tests/test_store.py
new file mode 100644
index 0000000..f944130
--- /dev/null
+++ b/tests/test_store.py
@@ -0,0 +1,13 @@
+from __future__ import annotations
+
+import pytest
+
+from gap_pipeline.store import RunStore
+
+
+def test_store_refuses_conflicting_overwrite(tmp_path) -> None:
+    store = RunStore(tmp_path, "item")
+    store.write_json("artifact.json", {"value": 1})
+    store.write_json("artifact.json", {"value": 1})
+    with pytest.raises(FileExistsError, match="refusing to overwrite"):
+        store.write_json("artifact.json", {"value": 2})
diff --git a/tests/test_surface.py b/tests/test_surface.py
new file mode 100644
index 0000000..78c4d5e
--- /dev/null
+++ b/tests/test_surface.py
@@ -0,0 +1,43 @@
+from __future__ import annotations
+
+import pytest
+
+from gap_pipeline.surface import (
+    apply_rename_map,
+    create_surface_variant,
+    validate_rename_map,
+)
+
+
+def test_math_only_rename_preserves_english_article(item) -> None:
+    text = r"Let \(a\) be a randomly chosen value with \(a>0\)."
+    renamed = apply_rename_map(text, {"a": "coefalpha"})
+    assert renamed == (
+        r"Let \(coefalpha\) be a randomly chosen value with \(coefalpha>0\)."
+    )
+
+
+def test_surface_variant_changes_problem_and_solution(item) -> None:
+    variant = create_surface_variant(
+        item,
+        "descriptive_long",
+        {"a": "positiveScalar"},
+    )
+    assert "positiveScalar" in variant.problem
+    assert "positiveScalar" in variant.solution
+    assert "Let positiveScalar" not in variant.problem
+
+
+def test_collision_and_nonbijection_are_rejected(item) -> None:
+    with pytest.raises(ValueError, match="collides"):
+        validate_rename_map(
+            {"a": "a"},
+            existing_identifiers=["a"],
+            scientific_constants=[],
+        )
+    with pytest.raises(ValueError, match="one-to-one"):
+        validate_rename_map(
+            {"a": "sharedName", "b": "sharedName"},
+            existing_identifiers=["a", "b"],
+            scientific_constants=[],
+        )