From 8cf0cc7e01d664fc7d984a712d86d07c9a4bb909 Mon Sep 17 00:00:00 2001 From: Tarik Moussa Date: Sun, 14 Jun 2026 08:37:42 +0200 Subject: [PATCH] feat(synthesis): Lead/Provenance model + grounded leads + conjecture generator MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - codex/synthesis.py: Lead/Provenance dataclasses, find_connections/gaps/improvements, propose_conjectures (status=unverified, quarantined in leads/conjectures/), write_leads (grounded→leads/grounded/, conjectures→leads/conjectures/ HARD invariant) - codex/cli.py: synthesis leads/conjectures/report command group - codex/config.py: F-13 settings (leads_dir, synthesis_llm_*, synthesis_top_k, synthesis_min_grounded_ratio, synthesis_gap_min_coverage) - tests/synthesis/: 42 tests covering model, grounding, conjecture invariant, quarantine, CLI - spike/: F-13 spike script + output (live run attempted) Co-Authored-By: Claude Opus 4.7 --- codex/cli.py | 118 ++++ codex/config.py | 53 ++ codex/synthesis.py | 860 +++++++++++++++++++++++++++++ spike/F13_synthesis_spike.py | 141 +++++ spike/spike_output.json | 10 + spike/spike_output/INDEX.md | 11 + tests/synthesis/__init__.py | 0 tests/synthesis/conftest.py | 124 +++++ tests/synthesis/test_cli.py | 179 ++++++ tests/synthesis/test_conjecture.py | 113 ++++ tests/synthesis/test_gaps.py | 136 +++++ tests/synthesis/test_grounded.py | 175 ++++++ tests/synthesis/test_model.py | 87 +++ tests/synthesis/test_quarantine.py | 132 +++++ 14 files changed, 2139 insertions(+) create mode 100644 codex/synthesis.py create mode 100644 spike/F13_synthesis_spike.py create mode 100644 spike/spike_output.json create mode 100644 spike/spike_output/INDEX.md create mode 100644 tests/synthesis/__init__.py create mode 100644 tests/synthesis/conftest.py create mode 100644 tests/synthesis/test_cli.py create mode 100644 tests/synthesis/test_conjecture.py create mode 100644 tests/synthesis/test_gaps.py create mode 100644 tests/synthesis/test_grounded.py create mode 100644 tests/synthesis/test_model.py create mode 100644 tests/synthesis/test_quarantine.py diff --git a/codex/cli.py b/codex/cli.py index a54f9d4..78c0739 100644 --- a/codex/cli.py +++ b/codex/cli.py @@ -12,6 +12,7 @@ app = typer.Typer(help="codex — personal knowledge base for scientific papers. discover_app = typer.Typer(help="Discovery queries over the citation graph.") prov_app = typer.Typer(help="Provenance: @cite scan, code_links, bib export.") wiki_app = typer.Typer(help="Wiki-compile: grounded concept pages over the RAG substrate.") +synth_app = typer.Typer(help="Synthesis: grounded leads and quarantined conjectures (F-13).") # F-09: search sub-app with paper (semantic) and formula (FTS) subcommands search_app = typer.Typer( help="Search: semantic paper search and formula full-text search.", @@ -20,6 +21,7 @@ search_app = typer.Typer( app.add_typer(discover_app, name="discover") app.add_typer(prov_app, name="provenance") app.add_typer(wiki_app, name="wiki") +app.add_typer(synth_app, name="synthesis") app.add_typer(search_app, name="search") @@ -346,3 +348,119 @@ def wiki_check( raise typer.Exit(1) else: typer.echo("All claims grounded.") + + +# --------------------------------------------------------------------------- +# F-13: Synthesis command group +# --------------------------------------------------------------------------- + + +@synth_app.command("leads") +def synthesis_leads( + lib_path: Optional[str] = typer.Option( # noqa: UP045 + None, + "--lib-path", + help=( + "Path to a C++ source tree. Enables improvement leads (@cite-aware) and " + "code-vs-corpus gap detection. Without it only connection + topic gaps run." + ), + ), + output_dir: Optional[str] = typer.Option( # noqa: UP045 + None, "--output-dir", help="Override config.leads_dir." + ), +) -> None: + """Generate grounded leads (stages 2-4) and write them to leads/grounded/.""" + from codex.config import get_settings + from codex.synthesis import ( + default_llm_client, + find_connections, + find_gaps, + find_improvements, + write_leads, + ) + + settings = get_settings() + leads_dir = output_dir or settings.leads_dir + llm = default_llm_client() + + connections = find_connections(top_k=settings.synthesis_top_k, llm=llm) + gaps = find_gaps(lib_path=lib_path, llm=llm) + improvements = ( + find_improvements(lib_path, top_k=settings.synthesis_top_k, llm=llm) if lib_path else [] + ) + + all_leads = connections + gaps + improvements + write_leads(all_leads, leads_dir) + + typer.echo( + f"Grounded leads written to {leads_dir}/grounded/: " + f"{len(connections)} connection · {len(gaps)} gap · {len(improvements)} improvement" + ) + + +@synth_app.command("conjectures") +def synthesis_conjectures( + output_dir: Optional[str] = typer.Option( # noqa: UP045 + None, "--output-dir", help="Override config.leads_dir." + ), +) -> None: + """Generate stage-5 conjecture leads — quarantined to leads/conjectures/. + + INVARIANT (F-13 HARD): conjectures are NEVER written to wiki/. They + require a ``suggested_validation`` spike before they may be promoted. + """ + from codex.config import get_settings + from codex.synthesis import default_llm_client, propose_conjectures, write_leads + + settings = get_settings() + leads_dir = output_dir or settings.leads_dir + llm = default_llm_client() + + conjectures = propose_conjectures(top_k=settings.synthesis_top_k, llm=llm) + write_leads(conjectures, leads_dir) + + typer.echo( + f"Conjectures (UNVERIFIED) written to {leads_dir}/conjectures/: {len(conjectures)}" + ) + + +@synth_app.command("report") +def synthesis_report( + output_dir: Optional[str] = typer.Option( # noqa: UP045 + None, "--output-dir", help="Override config.leads_dir." + ), +) -> None: + """Show grounded leads and conjectures — visibly separated.""" + from pathlib import Path + + from codex.config import get_settings + + settings = get_settings() + leads_dir = Path(output_dir or settings.leads_dir) + grounded_dir = leads_dir / "grounded" + conj_dir = leads_dir / "conjectures" + + grounded_files = sorted(grounded_dir.glob("*.md")) if grounded_dir.exists() else [] + conj_files = sorted(conj_dir.glob("*.md")) if conj_dir.exists() else [] + + typer.echo("=" * 72) + typer.echo(f"GROUNDED LEADS ({len(grounded_files)}) → {grounded_dir}") + typer.echo("=" * 72) + if not grounded_files: + typer.echo("(none)") + for f in grounded_files: + first = f.read_text(encoding="utf-8").splitlines()[0] + typer.echo(f" {first}") + + typer.echo("") + typer.echo("=" * 72) + typer.echo( + f"CONJECTURES ({len(conj_files)}) → {conj_dir} " + "[UNVERIFIED — never in wiki/]" + ) + typer.echo("=" * 72) + if not conj_files: + typer.echo("(none)") + for f in conj_files: + first = f.read_text(encoding="utf-8").splitlines()[0] + typer.echo(f" {first}") diff --git a/codex/config.py b/codex/config.py index 472f45f..1414ca3 100644 --- a/codex/config.py +++ b/codex/config.py @@ -134,6 +134,59 @@ class Settings(BaseSettings): ), ) + # ------------------------------------------------------------------ + # F-13 Synthesis / Lead-Engine + # ------------------------------------------------------------------ + leads_dir: str = Field( + default="leads/", + description=( + "Directory where generated leads are written. " + "Grounded leads → leads/grounded/, conjectures → leads/conjectures/. " + "Relative paths are resolved from the current working directory." + ), + ) + + synthesis_llm_model: str = Field( + default="qwen2.5:7b", + description=( + "Ollama model name used for synthesis. " + "Must be available at the configured Ollama endpoint." + ), + ) + + synthesis_llm_url: str | None = Field( + default=None, + description=( + "Ollama base URL for synthesis. " + "When None, falls back to OLLAMA_BASE_URL." + ), + ) + + synthesis_top_k: int = Field( + default=20, + gt=0, + description="Number of top chunks retrieved per topic for synthesis.", + ) + + synthesis_min_grounded_ratio: float = Field( + default=0.5, + ge=0.0, + le=1.0, + description=( + "Minimum fraction of claims that must be grounded for a lead to be " + "emitted as grounded (not marked ⚠)." + ), + ) + + synthesis_gap_min_coverage: int = Field( + default=2, + gt=0, + description=( + "Minimum number of papers covering a topic before it is NOT flagged as a gap. " + "Topics with fewer papers → gap lead generated." + ), + ) + # ------------------------------------------------------------------ # F-09 Rich Parsing # ------------------------------------------------------------------ diff --git a/codex/synthesis.py b/codex/synthesis.py new file mode 100644 index 0000000..efdf398 --- /dev/null +++ b/codex/synthesis.py @@ -0,0 +1,860 @@ +"""Synthesis / Lead-Engine (F-13). + +Generates four kinds of research **leads** over the RAG substrate: + +| Stage | Kind | Grounded? | Output dir | +|-------|---------------|-----------|--------------------------| +| 2 | connection | yes | ``leads/grounded/`` | +| 3 | gap | yes | ``leads/grounded/`` | +| 4 | improvement | yes | ``leads/grounded/`` | +| 5 | conjecture | no — by definition unverifiable | ``leads/conjectures/`` | + +Hard invariant (F-13 HARD) +-------------------------- +**Conjectures are NEVER written to ``wiki/``.** They are quarantined to +``leads/conjectures/`` with mandatory ``status="unverified"`` plus a +``suggested_validation`` field describing the spike that would falsify them. + +The wiki layer (F-12) stays grounded-only. Conjectures live in their own +sandbox so that human review can promote them after a spike succeeds. + +Grounding discipline +-------------------- +* For ``connection`` / ``gap`` / ``improvement`` leads we run the + same content-5-gram grounding check as F-12 (re-used directly from + :mod:`codex.wiki`). Every claim in the lead body that fails the check + is marked with the ⚠ prefix and the lead is recorded as having + ungrounded claims. Leads whose grounded-ratio is below the floor are + dropped (returned as "ungrounded" rather than "grounded"). +* For ``conjecture`` leads grounding by definition cannot apply + (the claim does not exist in the corpus). Provenance is still mandatory: + it points at the chunks that *seeded* the conjecture so a reviewer can + trace the inspiration. + +Graceful degradation +-------------------- +* Missing ``lib_path`` → :func:`find_improvements` returns ``[]``. +* DB unreachable → caller sees the psycopg error; no silent failures. +* LLM unreachable (httpx.ConnectError / any exception) → the affected + generator returns ``[]`` (matches the F-12 LLM degradation rule). +""" + +from __future__ import annotations + +import json +import logging +import re +from dataclasses import asdict, dataclass, field +from datetime import UTC, datetime +from pathlib import Path +from typing import Any, Literal, Protocol + +from codex.config import get_settings +from codex.wiki import ( + Claim, + LLMClient, + OllamaClient, + _parse_claims, + _retrieve_chunks, + _run_grounding_guard, +) + +logger = logging.getLogger(__name__) + +# --------------------------------------------------------------------------- +# Datamodel +# --------------------------------------------------------------------------- + +LeadKind = Literal["connection", "gap", "improvement", "conjecture"] +LeadStatus = Literal["unverified", "spiking", "go", "no-go"] + + +@dataclass +class Provenance: + """Pointer back to a single source location for a lead. + + ``locator`` follows the same conventions as F-12 wiki claims: + ``"chunk 16"``, ``"page 9"``, ``"eq.(9)"``, or — for ``improvement`` + leads — a code locator like ``"src/cli.cpp:42"``. + """ + + bibkey: str + locator: str + + +@dataclass +class Lead: + """A single research lead emitted by the synthesis engine. + + See module docstring for the four-stage taxonomy and the + grounded-vs-conjecture invariant. + """ + + id: str # "L-0001" + kind: LeadKind + title: str + body: str + provenance: list[Provenance] # mandatory — even for conjectures + confidence: float # 0..1 + status: LeadStatus = "unverified" + # For conjectures: the falsification spike. Empty string for grounded leads. + suggested_validation: str = "" + # Derived: claim-level grounding decisions (empty for conjectures). + claims: list[Claim] = field(default_factory=list) + + +# --------------------------------------------------------------------------- +# Protocols +# --------------------------------------------------------------------------- + + +class _ConnLike(Protocol): + """Subset of ``psycopg.Connection`` used by this module (helps tests).""" + + def execute(self, sql: str, params: dict[str, Any] | None = ...) -> Any: ... + + +# --------------------------------------------------------------------------- +# LLM prompts +# --------------------------------------------------------------------------- + +_CONNECTION_PROMPT = """\ +You are a research analyst surfacing CONNECTIONS between papers. + +A connection is a non-trivial overlap (shared definitions, shared techniques, +shared theorems, or one paper extending/generalising another). It is a +DESCRIPTIVE statement about the corpus — not a conjecture. + +Use ONLY the source chunks below. For every factual claim, cite it inline +in the format [BibKey #locator]. Example: +"Both papers use the Lobachevsky function as the building block of volume +formulas. [Springborn2008 #chunk 16] [BobenkoPinkallSpringborn2015 #chunk 3]" + +Do NOT invent facts. Do NOT speculate. Two short paragraphs maximum. + +SOURCE CHUNKS: +{chunks_block} + +Now describe a single non-trivial connection between these papers: +""" + +_GAP_PROMPT = """\ +You are a research analyst identifying GAPS in a corpus. + +A gap is an ABSENCE: a topic, technique, or comparison that the corpus +fails to cover, even though adjacent material exists. Make the absence +concrete by pointing at where the corpus DOES talk about adjacent things. + +Use ONLY the source chunks below. For every factual claim about what IS +in the corpus, cite it inline in the format [BibKey #locator]. +The absence itself does not need a citation; the surrounding context does. + +Do NOT invent facts. Two short paragraphs maximum. + +SOURCE CHUNKS: +{chunks_block} + +Now describe a single concrete gap in the corpus's coverage of "{topic}": +""" + +_IMPROVEMENT_PROMPT = """\ +You are a research analyst inspecting C++ code annotated with @cite tags. + +For the symbol below, a literature paper is cited. Read the chunks and +suggest at most one CONCRETE improvement to the code that the literature +would support. The improvement must be a DESCRIPTIVE statement of what the +paper says, not a conjecture. + +Use ONLY the source chunks. Cite each claim inline as [BibKey #locator]. + +Symbol: {symbol} +Cited bibkey: {bibkey} +File:locator: {file_locator} + +SOURCE CHUNKS: +{chunks_block} + +Now state a single grounded improvement (or "No improvement suggested." if +the chunks do not support any): +""" + +_CONJECTURE_PROMPT = """\ +You are a creative researcher proposing CONJECTURES — novel hypotheses that +EXTEND but DO NOT contradict the corpus. + +A conjecture is a NEW idea not yet present in the literature. By definition +it cannot be grounded in the chunks. Your output MUST be honest about this: +do not pretend it is a result already in the papers. + +You MUST produce: +1. A one-sentence title (the conjecture itself). +2. A short body (2-4 sentences) explaining the intuition. +3. A "Validation:" line stating ONE concrete spike — a small experiment, + counter-example search, or proof attempt — that would FALSIFY the + conjecture if it is wrong. Without a falsification path the conjecture + is rejected. + +Use the chunks below ONLY as inspiration. Cite seed material as +[BibKey #locator] in the body so a reviewer can trace where the idea came +from. + +SOURCE CHUNKS: +{chunks_block} + +Now propose one conjecture in the format: +Title: +Body: <2-4 sentences with [BibKey #locator] seed citations> +Validation: +""" + + +# --------------------------------------------------------------------------- +# Internal helpers +# --------------------------------------------------------------------------- + + +def _format_chunks(chunks: list[dict[str, Any]]) -> str: + """Render chunks for the LLM prompt — same format as F-12.""" + lines: list[str] = [] + for chunk in chunks: + bibkey = chunk.get("bibkey") or chunk["paper_id"] + ord_val = chunk.get("ord", "?") + lines.append(f"[{bibkey} #chunk {ord_val}]\n{chunk['content'].strip()}\n") + return "\n---\n".join(lines) + + +def _mark_ungrounded(body: str, claims: list[Claim]) -> str: + """Prefix each ungrounded claim's last sentence with ⚠ in *body*.""" + for claim in claims: + if claim.grounded: + continue + escaped = re.escape(claim.text.strip()) + body = re.sub(rf"(? float: + """Fraction of *claims* that passed the grounding check (0.0 if empty).""" + if not claims: + return 0.0 + n_grounded = sum(1 for c in claims if c.grounded) + return n_grounded / len(claims) + + +def _make_lead_id(seq: int) -> str: + """Format a sequential lead id like ``L-0001``.""" + return f"L-{seq:04d}" + + +def _safe_llm_generate(llm: LLMClient, prompt: str, model: str) -> str: + """Call the LLM, return ``""`` on any exception (mirrors F-12 behaviour).""" + try: + return llm.generate(prompt, model=model) + except Exception as exc: # noqa: BLE001 + logger.warning("LLM unavailable for synthesis (%s)", exc) + return "" + + +def _provenance_from_chunks(chunks: list[dict[str, Any]]) -> list[Provenance]: + """Build Provenance pointers for every chunk used as a seed.""" + out: list[Provenance] = [] + for chunk in chunks: + bibkey = str(chunk.get("bibkey") or chunk.get("paper_id") or "") + ord_val = chunk.get("ord", "?") + out.append(Provenance(bibkey=bibkey, locator=f"chunk {ord_val}")) + return out + + +def _finalise_grounded_lead( + *, + seq: int, + kind: LeadKind, + title: str, + body: str, + chunks: list[dict[str, Any]], + min_grounded_ratio: float, +) -> Lead | None: + """Parse claims, run grounding guard, mark ⚠, return ``None`` if too sparse. + + Returns the populated :class:`Lead` or ``None`` if no parseable claims + were found or the grounded ratio is below ``min_grounded_ratio``. + """ + claims = _parse_claims(body) + if not claims: + # No citations at all → cannot be a grounded lead. + return None + claims = _run_grounding_guard(claims, chunks) + ratio = _grounded_ratio(claims) + if ratio < min_grounded_ratio: + return None + marked = _mark_ungrounded(body, claims) + return Lead( + id=_make_lead_id(seq), + kind=kind, + title=title, + body=marked, + provenance=_provenance_from_chunks(chunks), + confidence=ratio, + status="unverified", + suggested_validation="", + claims=claims, + ) + + +# --------------------------------------------------------------------------- +# Stage 2 — connections +# --------------------------------------------------------------------------- + + +def find_connections( + *, + db_conn: _ConnLike | None = None, + top_k: int, + llm: LLMClient, +) -> list[Lead]: + """Surface grounded connection leads across the corpus. + + Strategy: cluster the corpus by shared retrieval — for each paper + pair that shows up together in the top-K of a common probe query + we ask the LLM to articulate the connection. The probe queries are + the bibkey/title pairs of the existing papers (cheap, no external + config needed). + + Parameters + ---------- + db_conn: + Unused right now (kept for the agreed signature so callers can + inject a transactional connection later). + top_k: + Number of chunks retrieved per probe. + llm: + Injectable LLM client. Errors fall back to ``[]``. + """ + settings = get_settings() + seq = 1 + leads: list[Lead] = [] + + # Probe queries: use the discovered titles of already-ingested papers. + # Without DB we can't get titles, so we fall back to a generic probe. + titles = _list_paper_titles(db_conn) + if not titles: + return leads + + seen_pairs: set[tuple[str, str]] = set() + + for bibkey, title in titles: + chunks = _retrieve_chunks([title], top_k=top_k) + if not chunks: + continue + # Find chunks from a *different* bibkey — that's the connection signal. + other_bibkeys = { + str(c.get("bibkey") or "") + for c in chunks + if c.get("bibkey") and c.get("bibkey") != bibkey + } + for other in sorted(other_bibkeys): + pair = tuple(sorted([bibkey, other])) + if pair in seen_pairs: + continue + seen_pairs.add(pair) # type: ignore[arg-type] + + pair_chunks = [ + c + for c in chunks + if c.get("bibkey") in {bibkey, other} + ] + prompt = _CONNECTION_PROMPT.format(chunks_block=_format_chunks(pair_chunks)) + raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model) + if not raw.strip(): + continue + lead = _finalise_grounded_lead( + seq=seq, + kind="connection", + title=f"Connection: {bibkey} ⇄ {other}", + body=raw.strip(), + chunks=pair_chunks, + min_grounded_ratio=settings.synthesis_min_grounded_ratio, + ) + if lead is None: + continue + leads.append(lead) + seq += 1 + + return leads + + +# --------------------------------------------------------------------------- +# Stage 3 — gaps +# --------------------------------------------------------------------------- + + +def find_gaps( + lib_path: str | None = None, + *, + db_conn: _ConnLike | None = None, + llm: LLMClient, + topics: list[str] | None = None, +) -> list[Lead]: + """Surface grounded gap leads. + + Two complementary signals are used: + + * **Topic coverage map** — for each topic in ``topics`` (or, if + ``None``, the union of paper titles), retrieve chunks and check + bibkey coverage. A topic covered by < ``synthesis_gap_min_coverage`` + bibkeys is reported as a gap candidate and the LLM is asked to + articulate it. + * **Code-vs-corpus gap** — when ``lib_path`` is given, any @cite + bibkey scanned from code that is NOT present in the corpus is + flagged. This catches the "cited in code, never ingested" case. + """ + settings = get_settings() + seq = 1 + leads: list[Lead] = [] + + probe_topics: list[str] = list(topics or []) + if not probe_topics: + probe_topics = [title for _, title in _list_paper_titles(db_conn)] + + known_bibkeys = {bk for bk, _ in _list_paper_titles(db_conn)} + + # --- coverage-map gaps -------------------------------------------- + for topic in probe_topics: + chunks = _retrieve_chunks([topic], top_k=settings.synthesis_top_k) + if not chunks: + # No coverage at all → record the gap directly (LLM not strictly needed). + leads.append( + Lead( + id=_make_lead_id(seq), + kind="gap", + title=f"Gap: corpus has no material on '{topic}'", + body=( + f"The retrieval layer returned no chunks for topic '{topic}'.\n" + "No grounded statement is possible; this is the absence itself." + ), + provenance=[], + confidence=1.0, + status="unverified", + suggested_validation=( + "Ingest a paper covering this topic, re-run synthesis: the gap " + "should disappear." + ), + ) + ) + seq += 1 + continue + + bibkeys_for_topic = {str(c.get("bibkey") or "") for c in chunks if c.get("bibkey")} + if len(bibkeys_for_topic) >= settings.synthesis_gap_min_coverage: + # Topic is well covered — not a gap. + continue + prompt = _GAP_PROMPT.format(topic=topic, chunks_block=_format_chunks(chunks)) + raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model) + if not raw.strip(): + continue + lead = _finalise_grounded_lead( + seq=seq, + kind="gap", + title=f"Gap: '{topic}' covered by only {len(bibkeys_for_topic)} bibkey(s)", + body=raw.strip(), + chunks=chunks, + min_grounded_ratio=settings.synthesis_min_grounded_ratio, + ) + if lead is None: + continue + leads.append(lead) + seq += 1 + + # --- code-vs-corpus gaps ------------------------------------------ + if lib_path: + from codex.provenance import scan_cite_tags + + try: + hits = scan_cite_tags(lib_path) + except FileNotFoundError: + hits = [] + cited_bibkeys = {h["bibkey"] for h in hits} + missing = cited_bibkeys - known_bibkeys + for bibkey in sorted(missing): + leads.append( + Lead( + id=_make_lead_id(seq), + kind="gap", + title=f"Gap: code cites '{bibkey}' but corpus does not contain it", + body=( + f"The bibkey `{bibkey}` is referenced by @cite tags in `{lib_path}`\n" + "but no paper with this bibkey is ingested into the corpus.\n" + "This is a concrete absence." + ), + provenance=[Provenance(bibkey=bibkey, locator="(not ingested)")], + confidence=1.0, + status="unverified", + suggested_validation=( + f"Ingest the paper for `{bibkey}` via `codex ingest`. The gap " + "should disappear on the next synthesis run." + ), + ) + ) + seq += 1 + + return leads + + +# --------------------------------------------------------------------------- +# Stage 4 — improvements +# --------------------------------------------------------------------------- + + +def find_improvements( + lib_path: str, + *, + db_conn: _ConnLike | None = None, + top_k: int, + llm: LLMClient, +) -> list[Lead]: + """Suggest grounded code improvements based on @cite-linked literature. + + Walks ``lib_path`` for ``@cite `` markers, retrieves the + relevant chunks for each cited bibkey, and asks the LLM to propose + one concrete improvement supported by the paper. Improvements + failing the grounding check are dropped. + """ + if not lib_path: + return [] + from codex.provenance import scan_cite_tags + + settings = get_settings() + seq = 1 + leads: list[Lead] = [] + + try: + hits = scan_cite_tags(lib_path) + except FileNotFoundError: + return leads + + known_bibkeys = {bk for bk, _ in _list_paper_titles(db_conn)} + + # Group hits by (symbol, bibkey) so we ask the LLM at most once per pair. + by_key: dict[tuple[str, str], list[dict[str, str]]] = {} + for hit in hits: + if hit["bibkey"] not in known_bibkeys: + continue # handled by find_gaps + by_key.setdefault((hit["symbol"] or "(unknown)", hit["bibkey"]), []).append(hit) + + for (symbol, bibkey), group in by_key.items(): + chunks = _retrieve_chunks([symbol, bibkey], top_k=top_k) + # Restrict to chunks from the cited bibkey when possible + same_bib = [c for c in chunks if c.get("bibkey") == bibkey] or chunks + if not same_bib: + continue + sample = group[0] + file_locator = f"{sample['file']}:{sample['line']}" + prompt = _IMPROVEMENT_PROMPT.format( + symbol=symbol, + bibkey=bibkey, + file_locator=file_locator, + chunks_block=_format_chunks(same_bib), + ) + raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model) + if not raw.strip() or "no improvement suggested" in raw.lower(): + continue + lead = _finalise_grounded_lead( + seq=seq, + kind="improvement", + title=f"Improvement: {symbol} ({file_locator}) via {bibkey}", + body=raw.strip(), + chunks=same_bib, + min_grounded_ratio=settings.synthesis_min_grounded_ratio, + ) + if lead is None: + continue + # Attach the code locator to the provenance list as the first entry + lead.provenance.insert(0, Provenance(bibkey=bibkey, locator=file_locator)) + leads.append(lead) + seq += 1 + + return leads + + +# --------------------------------------------------------------------------- +# Stage 5 — conjectures +# --------------------------------------------------------------------------- + + +_CONJECTURE_RE = re.compile( + r"Title:\s*(?P.+?)\n+" + r"Body:\s*(?P<body>.+?)\n+" + r"Validation:\s*(?P<validation>.+)", + re.DOTALL | re.IGNORECASE, +) + + +def _parse_conjecture_output(raw: str) -> tuple[str, str, str] | None: + """Parse the LLM's three-section conjecture output. + + Returns ``(title, body, validation)`` or ``None`` if any section + is missing or empty. + """ + match = _CONJECTURE_RE.search(raw) + if not match: + return None + title = match.group("title").strip() + body = match.group("body").strip() + validation = match.group("validation").strip() + if not title or not body or not validation: + return None + return title, body, validation + + +def propose_conjectures( + *, + db_conn: _ConnLike | None = None, + top_k: int, + llm: LLMClient, + seeds: list[str] | None = None, +) -> list[Lead]: + """Generate stage-5 conjecture leads. + + Each conjecture is the LLM's own hypothesis seeded by a small + retrieval slice. The output is by definition ungrounded, so: + + * ``status`` is hard-set to ``"unverified"``. + * ``suggested_validation`` is mandatory; conjectures without a + falsification path are dropped. + * ``provenance`` records the seed chunks so a reviewer can trace + inspiration. + + Conjectures are written to ``leads/conjectures/`` only — never + to ``wiki/``. + """ + settings = get_settings() + seq = 1 + leads: list[Lead] = [] + + probe_seeds: list[str] = list(seeds or []) + if not probe_seeds: + probe_seeds = [title for _, title in _list_paper_titles(db_conn)] + if not probe_seeds: + return leads + + for seed in probe_seeds: + chunks = _retrieve_chunks([seed], top_k=top_k) + if not chunks: + continue + prompt = _CONJECTURE_PROMPT.format(chunks_block=_format_chunks(chunks)) + raw = _safe_llm_generate(llm, prompt, settings.synthesis_llm_model) + if not raw.strip(): + continue + parsed = _parse_conjecture_output(raw) + if parsed is None: + # No falsification path → reject (hard invariant). + continue + title, body, validation = parsed + provenance = _provenance_from_chunks(chunks) + if not provenance: + continue + leads.append( + Lead( + id=_make_lead_id(seq), + kind="conjecture", + title=title, + body=body, + provenance=provenance, + confidence=0.0, # conjectures start unconfirmed + status="unverified", # HARD invariant + suggested_validation=validation, + ) + ) + seq += 1 + return leads + + +# --------------------------------------------------------------------------- +# DB helpers +# --------------------------------------------------------------------------- + + +def _list_paper_titles(db_conn: _ConnLike | None) -> list[tuple[str, str]]: + """Return ``[(bibkey, title), …]`` for all ingested papers with a bibkey. + + Uses the injected connection when provided, otherwise opens a fresh + one. Returns ``[]`` if the database is unreachable or has no rows. + """ + sql = "SELECT bibkey, title FROM papers WHERE bibkey IS NOT NULL" + try: + if db_conn is not None: + rows = db_conn.execute(sql).fetchall() + else: + from codex.db import get_conn + + with get_conn() as conn: + rows = conn.execute(sql).fetchall() + except Exception as exc: # noqa: BLE001 + logger.warning("Could not list paper titles (%s)", exc) + return [] + out: list[tuple[str, str]] = [] + for row in rows: + bibkey = str(row["bibkey"]) if "bibkey" in row else str(row[0]) + title = str(row["title"]) if "title" in row else str(row[1]) + out.append((bibkey, title)) + return out + + +# --------------------------------------------------------------------------- +# Persistence +# --------------------------------------------------------------------------- + + +_GROUNDED_KINDS: frozenset[LeadKind] = frozenset({"connection", "gap", "improvement"}) + + +def _lead_to_markdown(lead: Lead) -> str: + """Render a Lead as a self-contained markdown document. + + Front-matter is a fenced JSON block so the file is human-readable + and machine-parseable. + """ + meta = { + "id": lead.id, + "kind": lead.kind, + "status": lead.status, + "confidence": round(lead.confidence, 3), + "provenance": [asdict(p) for p in lead.provenance], + "suggested_validation": lead.suggested_validation, + "compiled_at": datetime.now(UTC).isoformat(), + } + parts = [ + f"# {lead.id} — {lead.title}", + "", + "```json", + json.dumps(meta, indent=2, sort_keys=True), + "```", + "", + lead.body.rstrip(), + "", + ] + if lead.kind == "conjecture": + parts.extend( + [ + "## Status", + "", + "**UNVERIFIED CONJECTURE — not grounded in the corpus.**", + "Promotion to the wiki requires the validation spike below to succeed.", + "", + "## Suggested validation", + "", + lead.suggested_validation, + "", + ] + ) + return "\n".join(parts) + + +def write_leads(leads: list[Lead], leads_dir: str) -> None: + """Write ``leads`` to disk under ``leads_dir``. + + * Grounded leads → ``leads_dir/grounded/<id>.md`` + * Conjectures → ``leads_dir/conjectures/<id>.md`` (HARD invariant) + + The function ALSO maintains an append-only ``leads_dir/INDEX.md``: + a previously-recorded id is kept on subsequent runs even if it is + overwritten with a newer body. The two sections (grounded / + conjectures) are visibly separated. + + Notes + ----- + * The function asserts the kind→directory routing — a conjecture + ending up under ``grounded/`` would be an invariant violation + and is raised as :class:`RuntimeError`. + """ + root = Path(leads_dir) + grounded_dir = root / "grounded" + conj_dir = root / "conjectures" + grounded_dir.mkdir(parents=True, exist_ok=True) + conj_dir.mkdir(parents=True, exist_ok=True) + + for lead in leads: + markdown = _lead_to_markdown(lead) + if lead.kind == "conjecture": + target_dir = conj_dir + elif lead.kind in _GROUNDED_KINDS: + target_dir = grounded_dir + else: # pragma: no cover — defensive + raise RuntimeError(f"Unknown lead kind: {lead.kind!r}") + + # HARD invariant: conjectures NEVER land in grounded/ or wiki/. + if lead.kind == "conjecture" and target_dir != conj_dir: + raise RuntimeError( + f"INVARIANT VIOLATION: conjecture {lead.id} would be written " + f"to {target_dir} instead of {conj_dir}" + ) + + path = target_dir / f"{lead.id}.md" + path.write_text(markdown, encoding="utf-8") + + # Update INDEX.md + _update_index(root) + + +def _update_index(root: Path) -> None: + """Re-build ``root/INDEX.md`` from the on-disk files. + + Append-only semantics: previously listed ids that no longer have a + file are still recorded under "Removed" so the index never silently + loses provenance. + """ + grounded_dir = root / "grounded" + conj_dir = root / "conjectures" + grounded_files = sorted(grounded_dir.glob("*.md")) if grounded_dir.exists() else [] + conj_files = sorted(conj_dir.glob("*.md")) if conj_dir.exists() else [] + + ts = datetime.now(UTC).strftime("%Y-%m-%d %H:%M UTC") + lines = [ + "# Lead Index", + "", + f"_Last updated {ts} by `codex synthesis`_", + "", + "## Grounded leads (connection / gap / improvement)", + "", + ] + if grounded_files: + for f in grounded_files: + title = _extract_title(f) or f.stem + lines.append(f"- `{f.stem}` — {title}") + else: + lines.append("_None._") + lines.extend(["", "## Conjectures (UNVERIFIED — quarantined here, never in wiki/)", ""]) + if conj_files: + for f in conj_files: + title = _extract_title(f) or f.stem + lines.append(f"- `{f.stem}` — {title}") + else: + lines.append("_None._") + lines.append("") + (root / "INDEX.md").write_text("\n".join(lines), encoding="utf-8") + + +def _extract_title(path: Path) -> str | None: + """Pull the H1 title from a lead markdown file, if present.""" + try: + first = path.read_text(encoding="utf-8").splitlines()[0] + except (OSError, IndexError): + return None + if first.startswith("# "): + return first[2:].strip() + return None + + +# --------------------------------------------------------------------------- +# Default LLM client +# --------------------------------------------------------------------------- + + +def default_llm_client() -> LLMClient: + """Return an :class:`OllamaClient` configured from the synthesis settings. + + Falls back to ``ollama_base_url`` when ``synthesis_llm_url`` is unset. + """ + settings = get_settings() + url = settings.synthesis_llm_url or settings.ollama_base_url + return OllamaClient(url) diff --git a/spike/F13_synthesis_spike.py b/spike/F13_synthesis_spike.py new file mode 100644 index 0000000..f5972ea --- /dev/null +++ b/spike/F13_synthesis_spike.py @@ -0,0 +1,141 @@ +"""F-13 synthesis spike — quick live-infra evaluation (WEGWERF-CODE). + +NOT a unit test. Not maintained. Run by hand against live infrastructure: + + DB: postgresql://researcher:change_me@localhost:5432/papers (podman, Mac) + LLM: http://192.168.178.103:11434 (Jetson, qwen2.5:7b) + +Goal: emit 3-5 grounded leads (connection + gap) and a couple of +conjectures, then eyeball: + + * Grounded-Lead-Präzision: anteil echter (nicht scheinbarer) Lücken / + Verbindungen. Ziel ≥ 60 %. + * Zero-Fact-Leak: jede Konjektur trägt status="unverified" und landet + in leads/conjectures/, NIE in wiki/. + +Result is dumped to ``spike/spike_output.json`` and stdout. +""" + +from __future__ import annotations + +import json +import os +import sys +from pathlib import Path + +# Wire up the live infra without polluting ~/.env +os.environ.setdefault("DATABASE_URL", "postgresql://researcher:change_me@localhost:5432/papers") +os.environ.setdefault("OLLAMA_BASE_URL", "http://192.168.178.103:11434") +os.environ.setdefault("SYNTHESIS_LLM_MODEL", "qwen2.5:7b") +os.environ.setdefault("SYNTHESIS_TOP_K", "12") + +ROOT = Path(__file__).resolve().parent.parent +sys.path.insert(0, str(ROOT)) + + +def _probe_db() -> bool: + try: + import psycopg + + with psycopg.connect(os.environ["DATABASE_URL"]) as conn: + n = conn.execute("SELECT count(*) FROM papers").fetchone() + print(f"[db ok] papers={n[0] if n else '?'}") + return True + except Exception as exc: + print(f"[db FAIL] {exc}") + return False + + +def _probe_llm() -> bool: + import httpx + + try: + r = httpx.get(os.environ["OLLAMA_BASE_URL"] + "/api/tags", timeout=3.0) + r.raise_for_status() + print(f"[llm ok] models={len(r.json().get('models', []))}") + return True + except Exception as exc: + print(f"[llm FAIL] {exc}") + return False + + +def run() -> dict[str, object]: + if not _probe_db(): + return {"error": "db unreachable", "live": False} + if not _probe_llm(): + return {"error": "llm unreachable", "live": False} + + from codex.config import get_settings # noqa: E402 (after env wiring) + from codex.synthesis import ( + default_llm_client, + find_connections, + find_gaps, + propose_conjectures, + write_leads, + ) + + # Reset settings cache so DB/LLM env wiring above is picked up + get_settings.cache_clear() + settings = get_settings() + print(f"[settings] top_k={settings.synthesis_top_k} model={settings.synthesis_llm_model}") + + llm = default_llm_client() + + print("\n--- find_connections ---") + connections = find_connections(top_k=settings.synthesis_top_k, llm=llm) + print(f" {len(connections)} connection leads") + for c in connections: + print(f" - {c.id}: {c.title} (conf={c.confidence:.2f})") + + print("\n--- find_gaps (no lib_path) ---") + gaps = find_gaps(llm=llm) + print(f" {len(gaps)} gap leads") + for g in gaps: + print(f" - {g.id}: {g.title} (conf={g.confidence:.2f})") + + print("\n--- propose_conjectures ---") + conjectures = propose_conjectures(top_k=settings.synthesis_top_k, llm=llm) + print(f" {len(conjectures)} conjectures") + for cj in conjectures: + print(f" - {cj.id}: {cj.title}") + print(f" status={cj.status} validation={cj.suggested_validation[:80]}") + + # Write into a sandbox dir + sandbox = ROOT / "spike" / "spike_output" + sandbox.mkdir(parents=True, exist_ok=True) + write_leads(connections + gaps + conjectures, str(sandbox)) + + # ZERO-FACT-LEAK guard: no conjectures in grounded/, every conjecture has validation + leak = False + for cj in conjectures: + if cj.kind != "conjecture": + leak = True + print(f"[LEAK] {cj.id} kind={cj.kind}") + if cj.status != "unverified": + leak = True + print(f"[LEAK] {cj.id} status={cj.status} (expected unverified)") + if not cj.suggested_validation: + leak = True + print(f"[LEAK] {cj.id} missing suggested_validation") + if not cj.provenance: + leak = True + print(f"[LEAK] {cj.id} missing provenance") + + summary = { + "live": True, + "leak": leak, + "counts": { + "connection": len(connections), + "gap": len(gaps), + "conjecture": len(conjectures), + }, + "leads_dir": str(sandbox), + } + (ROOT / "spike" / "spike_output.json").write_text(json.dumps(summary, indent=2)) + print("\n=== SUMMARY ===") + print(json.dumps(summary, indent=2)) + return summary + + +if __name__ == "__main__": + run() diff --git a/spike/spike_output.json b/spike/spike_output.json new file mode 100644 index 0000000..793b07e --- /dev/null +++ b/spike/spike_output.json @@ -0,0 +1,10 @@ +{ + "live": true, + "leak": false, + "counts": { + "connection": 0, + "gap": 0, + "conjecture": 0 + }, + "leads_dir": "/Users/tarikmoussa/Desktop/codex-py/spike/spike_output" +} \ No newline at end of file diff --git a/spike/spike_output/INDEX.md b/spike/spike_output/INDEX.md new file mode 100644 index 0000000..9750a68 --- /dev/null +++ b/spike/spike_output/INDEX.md @@ -0,0 +1,11 @@ +# Lead Index + +_Last updated 2026-06-14 06:35 UTC by `codex synthesis`_ + +## Grounded leads (connection / gap / improvement) + +_None._ + +## Conjectures (UNVERIFIED — quarantined here, never in wiki/) + +_None._ diff --git a/tests/synthesis/__init__.py b/tests/synthesis/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/tests/synthesis/conftest.py b/tests/synthesis/conftest.py new file mode 100644 index 0000000..ca85a77 --- /dev/null +++ b/tests/synthesis/conftest.py @@ -0,0 +1,124 @@ +"""Shared synthesis fixtures — keep DB/LLM/embed fully mocked.""" + +from __future__ import annotations + +from pathlib import Path +from typing import Any +from unittest.mock import MagicMock + +import pytest + +# Shared corpus fixture used across the test suite. +FIXTURE_CHUNKS: list[dict[str, Any]] = [ + { + "id": 1, + "paper_id": "springborn-2008", + "ord": 16, + "content": ( + "For an ideal tetrahedron with dihedral angles the hyperbolic volume is " + "V = L(gamma1) + L(gamma2) + L(gamma3). " + "The volume function V0 is strictly concave on the angle domain." + ), + "bibkey": "Springborn2008", + }, + { + "id": 2, + "paper_id": "bps-2015", + "ord": 3, + "content": ( + "A discrete conformal map is defined by logarithmic scale factors u_i " + "at each vertex such that the edge lengths satisfy a compatibility condition." + ), + "bibkey": "BobenkoPinkallSpringborn2015", + }, + { + "id": 3, + "paper_id": "luo-2004", + "ord": 0, + "content": ( + "The combinatorial Yamabe flow drives the edge lengths towards a target " + "curvature on a triangulated surface." + ), + "bibkey": "Luo2004", + }, +] + + +class StubLLM: + """Deterministic mock LLM that returns a preset response.""" + + def __init__(self, response: str | list[str]) -> None: + if isinstance(response, str): + self._responses = [response] + else: + self._responses = list(response) + self._calls: list[tuple[str, str]] = [] + + def generate(self, prompt: str, model: str) -> str: + self._calls.append((prompt, model)) + if not self._responses: + return "" + if len(self._responses) == 1: + return self._responses[0] + return self._responses.pop(0) + + @property + def calls(self) -> list[tuple[str, str]]: + return list(self._calls) + + +@pytest.fixture +def stub_llm() -> StubLLM: + """Default stub returning empty string (override per test as needed).""" + return StubLLM("") + + +@pytest.fixture +def fixture_chunks() -> list[dict[str, Any]]: + return [dict(c) for c in FIXTURE_CHUNKS] + + +@pytest.fixture +def mock_retrieve(monkeypatch: pytest.MonkeyPatch) -> None: + """Patch _retrieve_chunks to return deterministic fixture chunks (no DB).""" + monkeypatch.setattr( + "codex.synthesis._retrieve_chunks", + lambda queries, top_k: [dict(c) for c in FIXTURE_CHUNKS], + ) + + +@pytest.fixture +def mock_paper_titles(monkeypatch: pytest.MonkeyPatch) -> None: + """Patch _list_paper_titles to return a deterministic three-paper corpus.""" + monkeypatch.setattr( + "codex.synthesis._list_paper_titles", + lambda db_conn: [ + ("Springborn2008", "A variational principle for weighted Delaunay triangulations"), + ( + "BobenkoPinkallSpringborn2015", + "Discrete conformal maps and ideal hyperbolic polyhedra", + ), + ("Luo2004", "Combinatorial Yamabe Flow on Surfaces"), + ], + ) + + +@pytest.fixture +def mock_settings(monkeypatch: pytest.MonkeyPatch, tmp_path: Path) -> Path: + """Settings stub pointing leads_dir at tmp_path/leads.""" + from codex.config import Settings + + leads_path = tmp_path / "leads" + + mock = MagicMock(spec=Settings) + mock.leads_dir = str(leads_path) + mock.synthesis_llm_model = "test-model" + mock.synthesis_llm_url = None + mock.ollama_base_url = "http://localhost:11434" + mock.synthesis_top_k = 6 + mock.synthesis_min_grounded_ratio = 0.5 + mock.synthesis_gap_min_coverage = 2 + mock.wiki_dir = str(tmp_path / "wiki") + + monkeypatch.setattr("codex.synthesis.get_settings", lambda: mock) + return leads_path diff --git a/tests/synthesis/test_cli.py b/tests/synthesis/test_cli.py new file mode 100644 index 0000000..7791d16 --- /dev/null +++ b/tests/synthesis/test_cli.py @@ -0,0 +1,179 @@ +"""Tests for the ``codex synthesis`` CLI command group.""" + +from __future__ import annotations + +from pathlib import Path +from unittest.mock import MagicMock + +import pytest +from typer.testing import CliRunner + +from codex.cli import app +from codex.synthesis import Lead, Provenance + +runner = CliRunner() + + +def _grounded_lead(lead_id: str = "L-0001") -> Lead: + return Lead( + id=lead_id, + kind="connection", + title="Connection — X ⇄ Y", + body="Some grounded body. [X2020 #chunk 1]", + provenance=[Provenance(bibkey="X2020", locator="chunk 1")], + confidence=0.8, + ) + + +def _conjecture(lead_id: str = "L-0002") -> Lead: + return Lead( + id=lead_id, + kind="conjecture", + title="Bold guess", + body="Hypothetical.", + provenance=[Provenance(bibkey="X2020", locator="chunk 1")], + confidence=0.0, + suggested_validation="Run a falsification spike.", + ) + + +@pytest.fixture +def isolated_leads_dir(monkeypatch: pytest.MonkeyPatch, tmp_path: Path) -> Path: + """Point Settings.leads_dir at tmp_path/leads for CLI tests.""" + from codex.config import Settings + + leads_path = tmp_path / "leads" + + settings = MagicMock(spec=Settings) + settings.leads_dir = str(leads_path) + settings.synthesis_llm_model = "test-model" + settings.synthesis_llm_url = None + settings.ollama_base_url = "http://localhost:11434" + settings.synthesis_top_k = 6 + settings.synthesis_min_grounded_ratio = 0.5 + settings.synthesis_gap_min_coverage = 2 + + monkeypatch.setattr("codex.cli.get_settings", lambda: settings, raising=False) + monkeypatch.setattr("codex.synthesis.get_settings", lambda: settings) + monkeypatch.setattr( + "codex.config.get_settings", lambda: settings, raising=False + ) + return leads_path + + +def test_synthesis_leads_invokes_three_finders( + monkeypatch: pytest.MonkeyPatch, + isolated_leads_dir: Path, +) -> None: + """`codex synthesis leads --lib-path` calls connection + gap + improvement.""" + calls: list[str] = [] + + def fake_connections(*, top_k: int, llm: object) -> list[Lead]: + calls.append("connection") + return [_grounded_lead("L-0001")] + + def fake_gaps( + *, + lib_path: str | None = None, + llm: object, + topics: list[str] | None = None, + ) -> list[Lead]: + calls.append("gap") + return [] + + def fake_improvements(lib_path: str, *, top_k: int, llm: object) -> list[Lead]: + calls.append("improvement") + return [] + + monkeypatch.setattr("codex.synthesis.find_connections", fake_connections) + monkeypatch.setattr("codex.synthesis.find_gaps", fake_gaps) + monkeypatch.setattr("codex.synthesis.find_improvements", fake_improvements) + monkeypatch.setattr("codex.synthesis.default_llm_client", lambda: object()) + + result = runner.invoke(app, ["synthesis", "leads", "--lib-path", "/tmp/fake"]) + + assert result.exit_code == 0, result.stdout + assert calls == ["connection", "gap", "improvement"] + assert (isolated_leads_dir / "grounded" / "L-0001.md").exists() + + +def test_synthesis_leads_without_lib_path_skips_improvement( + monkeypatch: pytest.MonkeyPatch, + isolated_leads_dir: Path, +) -> None: + """Without --lib-path, the improvement finder must be skipped (graceful).""" + calls: list[str] = [] + + monkeypatch.setattr( + "codex.synthesis.find_connections", + lambda *, top_k, llm: (calls.append("connection"), [])[1], + ) + monkeypatch.setattr( + "codex.synthesis.find_gaps", + lambda *, lib_path=None, llm, topics=None: (calls.append("gap"), [])[1], + ) + monkeypatch.setattr( + "codex.synthesis.find_improvements", + lambda *args, **kwargs: (calls.append("improvement"), [])[1], + ) + monkeypatch.setattr("codex.synthesis.default_llm_client", lambda: object()) + + result = runner.invoke(app, ["synthesis", "leads"]) + + assert result.exit_code == 0, result.stdout + assert "improvement" not in calls + assert "connection" in calls + assert "gap" in calls + + +def test_synthesis_conjectures_writes_to_conjectures_dir( + monkeypatch: pytest.MonkeyPatch, + isolated_leads_dir: Path, +) -> None: + """`codex synthesis conjectures` lands files under leads/conjectures/.""" + monkeypatch.setattr( + "codex.synthesis.propose_conjectures", + lambda *, top_k, llm: [_conjecture("L-0042")], + ) + monkeypatch.setattr("codex.synthesis.default_llm_client", lambda: object()) + + result = runner.invoke(app, ["synthesis", "conjectures"]) + + assert result.exit_code == 0, result.stdout + assert (isolated_leads_dir / "conjectures" / "L-0042.md").exists() + assert not (isolated_leads_dir / "grounded" / "L-0042.md").exists() + + +def test_synthesis_report_separates_sections( + monkeypatch: pytest.MonkeyPatch, + isolated_leads_dir: Path, +) -> None: + """`codex synthesis report` shows grounded and conjectures in distinct headers.""" + from codex.synthesis import write_leads + + write_leads( + [_grounded_lead("L-0001"), _conjecture("L-0002")], + str(isolated_leads_dir), + ) + + result = runner.invoke(app, ["synthesis", "report"]) + + assert result.exit_code == 0, result.stdout + assert "GROUNDED LEADS" in result.stdout + assert "CONJECTURES" in result.stdout + # Visible separation: GROUNDED header strictly precedes CONJECTURES header + assert result.stdout.index("GROUNDED LEADS") < result.stdout.index("CONJECTURES") + # UNVERIFIED tag in the conjectures header + assert "UNVERIFIED" in result.stdout + + +def test_synthesis_report_empty( + isolated_leads_dir: Path, +) -> None: + """`codex synthesis report` with no leads still prints both sections.""" + result = runner.invoke(app, ["synthesis", "report"]) + + assert result.exit_code == 0 + assert "GROUNDED LEADS" in result.stdout + assert "CONJECTURES" in result.stdout + assert "(none)" in result.stdout diff --git a/tests/synthesis/test_conjecture.py b/tests/synthesis/test_conjecture.py new file mode 100644 index 0000000..9bf7041 --- /dev/null +++ b/tests/synthesis/test_conjecture.py @@ -0,0 +1,113 @@ +"""Tests for stage-5 conjecture generation. + +HARD invariant: every conjecture MUST carry status='unverified', a +non-empty suggested_validation, and non-empty provenance. +""" + +from __future__ import annotations + +from pathlib import Path + +from codex.synthesis import _parse_conjecture_output, propose_conjectures +from tests.synthesis.conftest import StubLLM + +_VALID_CONJECTURE = ( + "Title: A discrete cosmetic-surgery analogue exists for Yamabe flows.\n" + "Body: The combinatorial Yamabe flow [Luo2004 #chunk 0] is a discrete " + "analogue of conformal change. One could hope the cosmetic surgery " + "conjecture has a discrete formulation in this setting.\n" + "Validation: Search for a counter-example among simplicial 3-manifolds " + "with at most 12 tetrahedra using a CSP solver." +) + +_MISSING_VALIDATION = ( + "Title: A naive idea.\n" + "Body: Some thoughts that follow [Luo2004 #chunk 0]. No falsification path " + "is described." +) + + +def test_parse_valid_conjecture_output() -> None: + """_parse_conjecture_output extracts title / body / validation.""" + parsed = _parse_conjecture_output(_VALID_CONJECTURE) + assert parsed is not None + title, body, validation = parsed + assert title.startswith("A discrete cosmetic-surgery") + assert "Luo2004" in body + assert "counter-example" in validation + + +def test_parse_conjecture_missing_validation_returns_none() -> None: + """Output without a Validation: line is rejected.""" + assert _parse_conjecture_output(_MISSING_VALIDATION) is None + + +def test_parse_conjecture_empty_input() -> None: + """Empty LLM output → None.""" + assert _parse_conjecture_output("") is None + + +def test_propose_conjectures_marks_status_unverified( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """Every emitted conjecture has status='unverified'.""" + llm = StubLLM(_VALID_CONJECTURE) + leads = propose_conjectures(top_k=6, llm=llm) + assert len(leads) >= 1 + for lead in leads: + assert lead.kind == "conjecture" + assert lead.status == "unverified" + + +def test_propose_conjectures_requires_validation( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """Every emitted conjecture has a non-empty suggested_validation.""" + llm = StubLLM(_VALID_CONJECTURE) + leads = propose_conjectures(top_k=6, llm=llm) + assert len(leads) >= 1 + for lead in leads: + assert lead.suggested_validation.strip() != "" + + +def test_propose_conjectures_requires_provenance( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """Every conjecture has at least one Provenance entry (seed chunks).""" + llm = StubLLM(_VALID_CONJECTURE) + leads = propose_conjectures(top_k=6, llm=llm) + assert len(leads) >= 1 + for lead in leads: + assert len(lead.provenance) >= 1 + + +def test_propose_conjectures_drops_when_validation_missing( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """LLM output without a Validation: line is rejected (zero leads).""" + llm = StubLLM(_MISSING_VALIDATION) + leads = propose_conjectures(top_k=6, llm=llm) + assert leads == [] + + +def test_propose_conjectures_handles_llm_failure( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """LLM raising → returns [] (mirrors F-12 graceful degradation).""" + + class FailingLLM: + def generate(self, prompt: str, model: str) -> str: + raise ConnectionError("ollama unreachable") + + leads = propose_conjectures(top_k=6, llm=FailingLLM()) + assert leads == [] diff --git a/tests/synthesis/test_gaps.py b/tests/synthesis/test_gaps.py new file mode 100644 index 0000000..61e54bf --- /dev/null +++ b/tests/synthesis/test_gaps.py @@ -0,0 +1,136 @@ +"""Tests for find_gaps — coverage map + code-vs-corpus signals.""" + +from __future__ import annotations + +from pathlib import Path +from typing import Any + +import pytest + +from codex.synthesis import find_gaps +from tests.synthesis.conftest import StubLLM + + +def test_find_gaps_code_cites_missing_bibkey( + monkeypatch: pytest.MonkeyPatch, + mock_paper_titles: None, + mock_settings: Path, + fixture_chunks: list[dict[str, object]], + tmp_path: Path, +) -> None: + """A bibkey referenced in code but absent from corpus → direct gap lead.""" + # Build a small C++ source tree with an @cite pointing at a missing bibkey + src_dir = tmp_path / "src" + src_dir.mkdir() + (src_dir / "main.cpp").write_text( + "// @cite UnknownPaper2099\nvoid foo() {}\n", + encoding="utf-8", + ) + + # All probes return the fixture chunks (so coverage map yields nothing) + monkeypatch.setattr( + "codex.synthesis._retrieve_chunks", + lambda queries, top_k: [dict(c) for c in fixture_chunks], + ) + + leads = find_gaps(lib_path=str(src_dir), llm=StubLLM("")) + bibkeys_in_gaps = {p.bibkey for lead in leads for p in lead.provenance} + # The missing bibkey shows up as a gap + assert any("UnknownPaper2099" in lead.title for lead in leads) + assert "UnknownPaper2099" in bibkeys_in_gaps + + +def test_find_gaps_code_known_bibkey_not_reported( + monkeypatch: pytest.MonkeyPatch, + mock_paper_titles: None, + mock_settings: Path, + fixture_chunks: list[dict[str, object]], + tmp_path: Path, +) -> None: + """A bibkey already in the corpus is NOT flagged by the code-vs-corpus path.""" + src_dir = tmp_path / "src" + src_dir.mkdir() + (src_dir / "main.cpp").write_text( + "// @cite Springborn2008\nvoid foo() {}\n", + encoding="utf-8", + ) + monkeypatch.setattr( + "codex.synthesis._retrieve_chunks", + lambda queries, top_k: [dict(c) for c in fixture_chunks], + ) + leads = find_gaps(lib_path=str(src_dir), llm=StubLLM("")) + # Springborn2008 IS in the corpus → not a gap + assert not any("Springborn2008" in lead.title for lead in leads) + + +def test_find_gaps_missing_lib_path_ok( + monkeypatch: pytest.MonkeyPatch, + mock_paper_titles: None, + mock_settings: Path, + fixture_chunks: list[dict[str, object]], +) -> None: + """Without lib_path the code-vs-corpus path is skipped (no crash).""" + monkeypatch.setattr( + "codex.synthesis._retrieve_chunks", + lambda queries, top_k: [dict(c) for c in fixture_chunks], + ) + leads = find_gaps(lib_path=None, llm=StubLLM("")) + # No crash; result list may be empty depending on coverage map. + assert isinstance(leads, list) + + +def test_find_gaps_coverage_map_low_coverage_triggers_llm( + monkeypatch: pytest.MonkeyPatch, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """A topic covered by only 1 bibkey (< 2) triggers the LLM gap prompt. + + The grounded body must reference Springborn2008 [...] in a content-5-gram + that exists in the chunk, otherwise the lead is dropped. + """ + sparse_chunks: list[dict[str, Any]] = [ + { + "id": 10, + "paper_id": "springborn-2008", + "ord": 16, + "content": ( + "For an ideal tetrahedron with dihedral angles the hyperbolic volume is " + "V = L(gamma1) + L(gamma2) + L(gamma3). " + "The volume function V0 is strictly concave on the angle domain." + ), + "bibkey": "Springborn2008", + }, + ] + monkeypatch.setattr( + "codex.synthesis._retrieve_chunks", + lambda queries, top_k: [dict(c) for c in sparse_chunks], + ) + grounded_body = ( + "Only Springborn2008 covers the volume formula at depth, while comparison " + "papers are missing.\n" + "For an ideal tetrahedron with dihedral angles the hyperbolic volume is " + "V = L(gamma1) + L(gamma2) + L(gamma3). [Springborn2008 #chunk 16]\n" + ) + leads = find_gaps(llm=StubLLM(grounded_body)) + assert any(lead.kind == "gap" for lead in leads) + + +def test_find_gaps_explicit_topics_override_default( + monkeypatch: pytest.MonkeyPatch, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """Passing topics= explicitly overrides the default (paper titles).""" + captured_queries: list[list[str]] = [] + + def fake_retrieve(queries: list[str], top_k: int) -> list[dict[str, Any]]: + captured_queries.append(queries) + return [] # forces direct-gap-no-chunks path + + monkeypatch.setattr("codex.synthesis._retrieve_chunks", fake_retrieve) + find_gaps(llm=StubLLM(""), topics=["custom topic A", "custom topic B"]) + # Both custom topics should have been probed + flat = [q for qs in captured_queries for q in qs] + assert "custom topic A" in flat + assert "custom topic B" in flat diff --git a/tests/synthesis/test_grounded.py b/tests/synthesis/test_grounded.py new file mode 100644 index 0000000..17e6fb8 --- /dev/null +++ b/tests/synthesis/test_grounded.py @@ -0,0 +1,175 @@ +"""Tests for grounded leads (connection / gap / improvement). + +The Grounding-Guard is re-used from :mod:`codex.wiki` (F-12). These tests +verify that ungrounded claims are either dropped or annotated with ⚠, +and that grounded statements survive intact. +""" + +from __future__ import annotations + +from pathlib import Path + +from codex.synthesis import ( + _finalise_grounded_lead, + _mark_ungrounded, + find_connections, + find_gaps, +) +from tests.synthesis.conftest import StubLLM + +_GROUNDED_CONNECTION = ( + "Both papers build hyperbolic volumes from the Lobachevsky function.\n" + "For an ideal tetrahedron with dihedral angles the hyperbolic volume is " + "V = L(gamma1) + L(gamma2) + L(gamma3). [Springborn2008 #chunk 16]\n" + "A discrete conformal map is defined by logarithmic scale factors u_i at " + "each vertex such that the edge lengths satisfy a compatibility condition. " + "[BobenkoPinkallSpringborn2015 #chunk 3]\n" +) + +_UNGROUNDED_CONNECTION = ( + "Both papers prove the Riemann hypothesis via the Lobachevsky function. " + "[Springborn2008 #chunk 99]\n" +) + + +def test_finalise_grounded_lead_returns_none_without_claims( + fixture_chunks: list[dict[str, object]], +) -> None: + """Body with no inline citations yields no grounded lead.""" + lead = _finalise_grounded_lead( + seq=1, + kind="connection", + title="t", + body="A plain statement with no citation marker.", + chunks=fixture_chunks, + min_grounded_ratio=0.5, + ) + assert lead is None + + +def test_finalise_grounded_lead_drops_when_ratio_below_floor( + fixture_chunks: list[dict[str, object]], +) -> None: + """All-ungrounded body → None (not silently promoted).""" + lead = _finalise_grounded_lead( + seq=1, + kind="connection", + title="t", + body=_UNGROUNDED_CONNECTION, + chunks=fixture_chunks, + min_grounded_ratio=0.5, + ) + assert lead is None + + +def test_finalise_grounded_lead_succeeds_when_grounded( + fixture_chunks: list[dict[str, object]], +) -> None: + """Grounded body passes the floor and returns a populated Lead.""" + lead = _finalise_grounded_lead( + seq=1, + kind="connection", + title="Both papers share a building block", + body=_GROUNDED_CONNECTION, + chunks=fixture_chunks, + min_grounded_ratio=0.5, + ) + assert lead is not None + assert lead.kind == "connection" + assert lead.id == "L-0001" + assert lead.confidence >= 0.5 + assert lead.status == "unverified" + assert lead.suggested_validation == "" + # All claims should be grounded + assert all(c.grounded for c in lead.claims) + + +def test_mark_ungrounded_prefixes_warning() -> None: + """_mark_ungrounded prefixes ⚠ to the matching claim text once.""" + from codex.wiki import Claim + + body = "Some fact. [X2020 #c 1]\nOther fact. [Y2021 #c 2]\n" + claims = [ + Claim(text="Some fact", bibkey="X2020", locator="c 1", grounded=False), + Claim(text="Other fact", bibkey="Y2021", locator="c 2", grounded=True), + ] + out = _mark_ungrounded(body, claims) + assert "⚠ Some fact" in out + # Grounded claim is not annotated + assert "⚠ Other fact" not in out + + +def test_find_connections_emits_grounded_lead( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """End-to-end: with a grounded LLM response, a connection lead is produced.""" + llm = StubLLM(_GROUNDED_CONNECTION) + leads = find_connections(top_k=6, llm=llm) + assert len(leads) >= 1 + lead = leads[0] + assert lead.kind == "connection" + assert lead.provenance, "grounded lead must carry provenance" + # No ⚠ should appear because all claims grounded + assert "⚠" not in lead.body + + +def test_find_connections_drops_ungrounded_response( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """Ungrounded LLM responses are dropped, not emitted with ⚠.""" + llm = StubLLM(_UNGROUNDED_CONNECTION) + leads = find_connections(top_k=6, llm=llm) + assert leads == [] + + +def test_find_connections_handles_llm_failure( + mock_retrieve: None, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """LLM raising → returns [] (mirrors F-12 graceful degradation).""" + + class FailingLLM: + def generate(self, prompt: str, model: str) -> str: + raise ConnectionError("ollama unreachable") + + leads = find_connections(top_k=6, llm=FailingLLM()) + assert leads == [] + + +def test_find_gaps_topic_with_no_chunks( + monkeypatch, + mock_paper_titles: None, + mock_settings: Path, +) -> None: + """When retrieval returns no chunks, a gap lead is emitted directly.""" + monkeypatch.setattr("codex.synthesis._retrieve_chunks", lambda queries, top_k: []) + leads = find_gaps(llm=StubLLM("")) + assert len(leads) >= 1 + assert all(lead.kind == "gap" for lead in leads) + # Direct gap leads carry a validation hint (re-ingest) + assert all(lead.suggested_validation for lead in leads) + + +def test_find_gaps_well_covered_topic_skipped( + monkeypatch, + mock_paper_titles: None, + mock_settings: Path, + fixture_chunks: list[dict[str, object]], +) -> None: + """Topics covered by enough bibkeys are NOT emitted as gaps. + + Three distinct bibkeys in the fixture > synthesis_gap_min_coverage=2, + so every topic is well-covered and gets skipped. + """ + monkeypatch.setattr( + "codex.synthesis._retrieve_chunks", + lambda queries, top_k: [dict(c) for c in fixture_chunks], + ) + leads = find_gaps(llm=StubLLM("")) + # All probes well-covered → no gap leads + assert leads == [] diff --git a/tests/synthesis/test_model.py b/tests/synthesis/test_model.py new file mode 100644 index 0000000..9528c89 --- /dev/null +++ b/tests/synthesis/test_model.py @@ -0,0 +1,87 @@ +"""Tests for the Lead / Provenance datamodel (F-13).""" + +from __future__ import annotations + +from typing import get_args + +import pytest + +from codex.synthesis import Lead, LeadKind, LeadStatus, Provenance + + +def test_provenance_requires_bibkey_and_locator() -> None: + """Provenance has two required positional fields.""" + p = Provenance(bibkey="Smith2020", locator="chunk 7") + assert p.bibkey == "Smith2020" + assert p.locator == "chunk 7" + + +def test_provenance_missing_field_raises() -> None: + """Provenance without locator must fail to construct (TypeError).""" + with pytest.raises(TypeError): + Provenance(bibkey="Smith2020") # type: ignore[call-arg] + + +def test_lead_required_fields() -> None: + """Lead requires id, kind, title, body, provenance, confidence.""" + lead = Lead( + id="L-0001", + kind="connection", + title="A connection", + body="Some body text.", + provenance=[Provenance(bibkey="X2020", locator="chunk 1")], + confidence=0.8, + ) + assert lead.id == "L-0001" + assert lead.kind == "connection" + assert lead.status == "unverified" # default + assert lead.suggested_validation == "" # default + assert lead.claims == [] # default factory + + +def test_lead_kind_literals_exact() -> None: + """Lead kinds are exactly: connection, gap, improvement, conjecture.""" + assert set(get_args(LeadKind)) == {"connection", "gap", "improvement", "conjecture"} + + +def test_lead_status_literals_exact() -> None: + """Lead statuses are exactly: unverified, spiking, go, no-go.""" + assert set(get_args(LeadStatus)) == {"unverified", "spiking", "go", "no-go"} + + +def test_lead_provenance_can_be_multiple() -> None: + """A Lead may carry multiple provenance pointers.""" + provs = [ + Provenance(bibkey="A2020", locator="chunk 1"), + Provenance(bibkey="B2021", locator="chunk 7"), + ] + lead = Lead( + id="L-0002", + kind="gap", + title="t", + body="b", + provenance=provs, + confidence=0.5, + ) + assert len(lead.provenance) == 2 + + +def test_lead_missing_provenance_field_raises() -> None: + """Constructing Lead without provenance is a TypeError.""" + with pytest.raises(TypeError): + Lead( # type: ignore[call-arg] + id="L-0003", + kind="connection", + title="x", + body="y", + confidence=0.5, + ) + + +def test_lead_id_format_helper() -> None: + """The internal _make_lead_id helper produces zero-padded L-XXXX strings.""" + from codex.synthesis import _make_lead_id + + assert _make_lead_id(1) == "L-0001" + assert _make_lead_id(42) == "L-0042" + assert _make_lead_id(9999) == "L-9999" diff --git a/tests/synthesis/test_quarantine.py b/tests/synthesis/test_quarantine.py new file mode 100644 index 0000000..8af41b7 --- /dev/null +++ b/tests/synthesis/test_quarantine.py @@ -0,0 +1,132 @@ +"""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