# Contratos de interfaz (RNF-4)

Todos los contratos son modelos Pydantic v2; los JSON Schema en `docs/interfaces/*.schema.json` se regeneran con `python scripts/export_schemas.py` y **son derivados del código, no al revés**.

## Módulo RAG (`src/ragsolver/rag/schema.py`, `PLAN_RAG.md` §7-§8)

| Esquema | Uso |
|---|---|
| `Document` | metadatos por fuente (`doc_id`, licencia, `redistributable`, parser) |
| `ChunkBase` / `MathlibChunk` / `InformalChunk` | filas de las tablas LanceDB `mathlib` / `informal` |
| `Figure` | tabla `figures` (recorte, bbox, descripción VLM, `detected_by`) |
| `RetrievalRequest` | entrada del retriever: `queries[1-4]`, `mode`, `corpora`, `k`, `n_candidates`, `filters`, `rerank`, `include_figures`, `context` |
| `RetrievalResult` | `hits[]` (con `figures[]` y `citation`), `citations[]`, `trace` |
| `Citation` | `citation_id` (`M1..`/`I1..`), `locator`, `scores`, `used_in_proof`, `used_in_sketch`, `snippet` |
| `TraceEvent` | evento JSONL por búsqueda/llamada (RNF-5) con `VersionsPin`; en llamadas LLM `request` lleva `model`, `tokens_in`, `tokens_out`, `cost_usd` (exacto, OpenRouter) y `decision` (salida validada) |

## Agentes (`src/ragsolver/agents/schemas.py`, propuesta §6.3)

| Esquema | Agente | Campos clave |
|---|---|---|
| `Problem` | entrada | `informal_statement`, `formal_statement` (`... := by sorry`), `header` (`open ...`), `imports` |
| `PlannerOutput` | Planificador | `strategy`, `subgoals[1-6]` con `statement_nl`, `formal_hint`, `search_queries[≤3]`, `math_area` |
| `GeneratorOutput` | Generador | `sketch`, `used_citations[]` |
| `FormalizerOutput` | Autoformalizador | `proof_tactics` (sólo el bloque tras `:= by`), `notes` |
| `CriticOutput` | Crítico | `error_type`, `action` (retry/replan/abandon), `missing_identifiers[]`, `feedback` |
| `BaselineAOutput` / `BaselineBOutput` | líneas base A / B | A: `proof_tactics` (obligatorio); B: `natural_language_proof` + `self_assessed_correct` (obligatorios) |
| `Verdict` | Verificador | `ok`, `errors[{line,col,message}]`, `uses_sorry`, `axioms[]` (auditoría VER-1: `ok=true` exige subconjunto de `propext`/`Classical.choice`/`Quot.sound`), `seconds` |
| `SolutionReport` | orquestador | estado, intentos, llamadas, tokens, `lean_code`, `citations[]` clasificadas, taxonomía de errores, re-recuperaciones |

## Configuración

- `configs/versions.yaml`: pins (Lean/Mathlib, modelos, proveedor LLM y cadena de modelos, índice).
- `configs/retrieval.yaml`: plantillas de consulta por modo, `rrf_k`, `max_per_module`, flags de ablación del retriever.
- `configs/agents.yaml`: `k_max`, `llm_budget`, recuperación de los agentes, backend Lean, configuraciones de ablación, prompts versionados.
- `configs/ingest.yaml`: filtros de Mathlib, parámetros del PDF, prompts de enriquecimiento (versionados).