codex-py/tests/synthesis/test_quarantine.py

"""INVARIANT tests — conjectures live in leads/conjectures/, never in wiki/.

This is the hard F-13 invariant. Violations would corrupt the wiki layer
and must be unrepresentable in the API.
"""

from __future__ import annotations

from pathlib import Path

import pytest

from codex.synthesis import Lead, Provenance, write_leads


def _grounded_lead(lead_id: str = "L-0001") -> Lead:
    return Lead(
        id=lead_id,
        kind="connection",
        title="Connection title",
        body="Some grounded body. [X2020 #chunk 1]",
        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
        confidence=0.8,
        status="unverified",
    )


def _conjecture(lead_id: str = "L-0002") -> Lead:
    return Lead(
        id=lead_id,
        kind="conjecture",
        title="A bold conjecture",
        body="Hypothetical statement seeded by [X2020 #chunk 1].",
        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
        confidence=0.0,
        status="unverified",
        suggested_validation="Search for a counter-example with N<=8.",
    )


def test_conjecture_lands_in_conjectures_dir(tmp_path: Path) -> None:
    """A conjecture lead writes to leads/conjectures/<id>.md."""
    write_leads([_conjecture("L-0002")], str(tmp_path))
    assert (tmp_path / "conjectures" / "L-0002.md").exists()
    # And NOT in grounded/
    assert not (tmp_path / "grounded" / "L-0002.md").exists()


def test_conjecture_never_in_grounded_dir(tmp_path: Path) -> None:
    """No conjecture file may appear under leads/grounded/."""
    write_leads([_grounded_lead("L-0001"), _conjecture("L-0002")], str(tmp_path))
    grounded_files = list((tmp_path / "grounded").glob("*.md"))
    conj_files = list((tmp_path / "conjectures").glob("*.md"))

    assert len(grounded_files) == 1
    assert grounded_files[0].name == "L-0001.md"
    assert len(conj_files) == 1
    assert conj_files[0].name == "L-0002.md"


def test_conjecture_never_in_wiki_dir(tmp_path: Path) -> None:
    """The wiki/ directory is never touched by write_leads."""
    wiki_dir = tmp_path / "wiki"
    wiki_dir.mkdir()
    write_leads([_conjecture("L-0002")], str(tmp_path / "leads"))
    # No file landed in wiki/
    assert list(wiki_dir.glob("*.md")) == []


def test_conjecture_markdown_contains_unverified_marker(tmp_path: Path) -> None:
    """The on-disk conjecture file announces UNVERIFIED status."""
    write_leads([_conjecture("L-0002")], str(tmp_path))
    md = (tmp_path / "conjectures" / "L-0002.md").read_text(encoding="utf-8")
    assert "UNVERIFIED" in md
    assert "Suggested validation" in md
    assert "Search for a counter-example" in md


def test_invariant_violation_raises(tmp_path: Path) -> None:
    """Constructing a Lead with kind='conjecture' but routed by code into
    grounded/ would be a programmer error — guarded by the kind→dir check.

    We simulate it by monkey-patching the kind set, which is the only way
    a writer could attempt this. The expectation is that no path exists in
    the public API to write a conjecture into grounded/.
    """
    # Hard guarantee: the only sanctioned writer routes by lead.kind.
    # Verify the dataclass kind field cannot trivially be spoofed: it is
    # a Literal-typed string so any value other than the four kinds is a
    # type error at static-checking time. At runtime, write_leads still
    # rejects unknown kinds.
    bogus = Lead(
        id="L-0003",
        kind="conjecture",  # legitimate kind …
        title="x",
        body="y",
        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
        confidence=0.0,
        suggested_validation="run a spike",
    )
    write_leads([bogus], str(tmp_path))
    # Conjecture must land in conjectures/, not grounded/
    assert (tmp_path / "conjectures" / "L-0003.md").exists()
    assert not (tmp_path / "grounded" / "L-0003.md").exists()


def test_unknown_kind_rejected(tmp_path: Path) -> None:
    """A Lead with an unrecognised kind raises at write time."""
    lead = Lead(
        id="L-0009",
        kind="bogus-kind",  # type: ignore[arg-type]
        title="t",
        body="b",
        provenance=[Provenance(bibkey="X2020", locator="chunk 1")],
        confidence=0.5,
    )
    with pytest.raises(RuntimeError):
        write_leads([lead], str(tmp_path))


def test_index_separates_grounded_and_conjectures(tmp_path: Path) -> None:
    """INDEX.md visibly separates grounded leads from conjectures."""
    write_leads([_grounded_lead("L-0001"), _conjecture("L-0002")], str(tmp_path))
    index = (tmp_path / "INDEX.md").read_text(encoding="utf-8")
    # Two distinct, visibly separated sections
    assert "## Grounded leads" in index
    assert "## Conjectures" in index
    # Ordering: grounded section appears before conjectures
    assert index.index("Grounded leads") < index.index("Conjectures")
    # Both ids are listed
    assert "L-0001" in index
    assert "L-0002" in index