▣ gabysql

Fecha: 2026-06-15 Estado: Aceptado Bloque: Segundo nivel de la red de seguridad de hardening (después de M3 sobre planner) Origen: docs/TAREAS_PENDIENTES.md §3 — “proptest sobre Pager” como item independiente de M3. Refina: ADR-0084 (M3 — misma técnica zero-deps aplicada al planner).

Contexto

M3 (ADR-0084) defendió la correctness del planner cost-based: la invariante “el resultado de un SELECT no debe cambiar según si ANALYZE corrió o no”. Eso es la capa de arriba.

La capa de abajo — el Pager, que decide qué páginas leer/escribir y maneja transacciones — también necesita una red de seguridad. Hoy había 3 crash tests sintéticos (puntos elegidos por el dev) y eso es todo. Si una secuencia rara de begin/insert/commit/rollback rompe algo, no nos enteramos hasta que un usuario lo dispara.

Este push agrega property tests al nivel del Pager — mismo enfoque hand-rolled zero-deps que M3.

Decisión

Crear tests/proptest_pager.rs con 3 property tests sobre secuencias random de operaciones DML + tx control. Cada uno verifica una invariante distinta.

Infraestructura compartida con M3

Generador de ops

enum Op {
    Insert(i64, i64),  // (id, v)
    UpdateById(i64),   // SET v=v+1 WHERE id=...
    DeleteById(i64),   // DELETE WHERE id=...
}

IDs del pool 0..30 para garantizar overlap: updates y deletes deben tener chance real de matchear inserts previos. Distribución: 60% inserts, 20% updates, 20% deletes (ajustable).

Modelo de referencia

BTreeMap<i64, i64> en Rust que replica la semántica del engine post-ANSI fix (PK dup ignorada en insert, UPDATE/DELETE sobre fila inexistente devuelve 0 filas). Se compara los IDs del engine vs los del modelo después de cada commit.

Tests

  1. pager_commit_visibility_invariant (40 iters × 50 ops):
    • Aplica ops, commitea, reabre la DB, lee SELECT id FROM t ORDER BY id.
    • Debe matchear los IDs del modelo Rust.
    • Verifica INTEGRITY CHECK clean al final.
  2. pager_rollback_discards_invariant (30 iters × (20 + 30 ops)):
    • Fase 1: commit con 20 ops → snapshot.
    • Fase 2: tx con 30 ops adicionales → ROLLBACK.
    • Reabre y verifica que el estado es EXACTAMENTE el snapshot pre-tx.
    • Verifica INTEGRITY CHECK clean al final.
  3. pager_chained_tx_integrity_invariant (20 iters × 8 tx × 10 ops):
    • Chain de 8 transacciones random; 70% commit, 30% rollback (rng-decidido).
    • Modelo Rust solo aplica los ops de tx commiteadas.
    • Verificación intermedia después de cada tx (no solo al final).
    • INTEGRITY CHECK final.

Total: 40×50 + 30×(20+30) + 20×8×10 = 2000 + 1500 + 1600 = 5100 ops random ejercitados por corrida.

Consecuencias

Positivas

Negativas / deuda

Alternativas consideradas

  1. Usar proptest crate. Mejor shrinking, mejor reporting, ergonomía más pulida. Choca con ADR-0001 (zero-deps core). Misma decisión que en M3.
  2. Incluir CREATE TABLE / DROP TABLE en el generador. Espacio de ops más rico pero requiere modelo más sofisticado. Diferible: focusing first on DML over fixed schema.
  3. Tests separados por tipo de op en vez de mezclados. Rechazado: bugs interesantes emergen de combinaciones (e.g. INSERT seguido de UPDATE seguido de DELETE sobre el mismo PK en la misma tx).

Tests añadidos

Suite total: 813 → 816 (+3 tests, ~5100 ops random adicionales por corrida).

Referencias