Motor en Rust para decidir, con demostración y no a ojo, cuándo un conjunto de réplicas local-first puede operar sin coordinación y cuándo no — y, cuando la respuesta es "sí, dentro de límites", proveer el mecanismo que lo garantiza.
Rust 24Markdown 15TOML 1358 Definitions
T9c: comparación honesta y corrección del registro (cierra T9)
T9 §F/§G. Documentación fundamentada en tests, no a mano:
- tests/comparison.rs: corre detector T8 vs escrow T9 sobre los mismos
escenarios; los veredictos de la tabla son exactamente los aserados.
- COMPARISON.md: tabula detector vs escrow. Fila 3 (particionado 60/60):
detector da FALSO-VERDE (corre libre al caso más peligroso), escrow lo
bloquea con NeedsRebalance — con o sin partición. Rendimiento (reparto)
separado de corrección (certificado).
- STRONG_RESULT.md reescrito (§G): RETIRA el reclamo fuerte de T8
('más fino que CALM / I-confluence sobre el grafo real'). Documenta:
(1) era detección, no evitación; (2) no hay separación vs I-confluence/CALM
(Prop.3); (3) el 60/60-particionado era un BUG (punto ciego), no virtud.
Apunta a escrow+router como la evitación real, con la honestidad §B
(escrow transforma la operación, no vence a CALM).
54 tests, clippy limpio. Hito T9 cerrado: de detección a evitación.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
diff --git a/COMPARISON.md b/COMPARISON.md
new file mode 100644
index 0000000..b3562d1
--- /dev/null
+++ b/COMPARISON.md
@@ -0,0 +1,52 @@
+# COMPARISON — detector (T8) vs escrow (T9)
+
+Los dos mecanismos sobre los **mismos escenarios**, misma cuenta (saldo inicial
+100, invariante `saldo ≥ 0`, slack `S = 100`). Los veredictos de esta tabla son
+exactamente los que verifica `tests/comparison.rs` — ninguno está escrito a mano.
+
+- **Detector (T8):** funde los estados de las réplicas y comprueba el merge
+ (`AccountConfig::haz_coordination`). Detección **reactiva por-estado**.
+- **Escrow (T9):** reparto de presupuestos `[50,50]` (válido: `Σ ≤ 100`); cada
+ réplica gasta local si le cabe (`try_spend`). **Evitación por construcción**.
+
+| # | Escenario | Grafo | Retiros | Detector (T8) | Escrow `[50,50]` (T9) |
+|---|---|---|---|---|---|
+| 1 | conectado, caben | `0—1` | `10,10` | corre libre | **Local** (ambos ≤ 50) |
+| 2 | conectado, sobregiro | `0—1` | `60,60` | coordina | **rebalanceo** (60 > 50) |
+| 3 | **particionado, sobregiro** | `∅` | `60,60` | **corre libre** ⚠️ | **rebalanceo** (60 > 50) |
+| 4 | particionado, caben | `∅` | `10,10` | corre libre | Local |
+
+## La fila 3 es todo el punto de T9
+
+**El detector dice "corre libre" al caso más peligroso.** Con las dos réplicas
+particionadas retirando 60 cada una de una cuenta de 100, el saldo global va a
+`100 − 120 = −20`: viola el invariante. Pero el detector, al codificar una
+restricción **global** por aristas **pares**, se queda sin ninguna arista al
+particionar y no ve el acoplamiento. **Falso-verde: el caso inseguro reportado
+como seguro** — el peor error posible en un consejero de coordinación.
+
+**El escrow lo bloquea correctamente.** El presupuesto de cada réplica es 50; un
+retiro de 60 devuelve `NeedsRebalance{deficit:10}`, **con o sin partición**,
+porque el presupuesto `b_i` es local y su certificado (`Σ b_i ≤ S`) no depende de
+que haya arista. La partición no lo ciega: lo respeta.
+
+## Rendimiento ≠ corrección (R-T9a)
+
+| Reparto | Retiro | Escrow | Nota |
+|---|---|---|---|
+| `[100, 0]` | réplica 1 retira 10 | rebalanceo | reparto malo: la réplica seca coordina de más |
+| `[50, 50]` | réplica 1 retira 10 | Local | reparto equilibrado: cero coordinación |
+
+Ambos repartos son **correctos** (el certificado `valor ≥ K` aguanta los dos); el
+segundo es solo más **eficiente**. La calidad del reparto es un problema de
+optimización sobre el grafo — el trabajo del `BudgetRouter` (`diffuse`) — no de
+corrección. Por eso los tests los separan.
+
+## Lectura
+
+El detector no se borra (sirve como alarma de reconciliación honesta para
+invariantes sin estructura de recurso divisible, R-T9b: unicidad de ID,
+integridad referencial). Pero **deja de ser el consejero de coordinación**: para
+un invariante numérico sobre un recurso conservado, el que evita coordinación de
+verdad —y sin puntos ciegos— es el **escrow** (`escrow.rs`), ruteado por el grafo
+(`router.rs`). Ver `STRONG_RESULT.md` para la corrección del reclamo de T8.
diff --git a/STRONG_RESULT.md b/STRONG_RESULT.md
index 88520ec..96bc5db 100644
--- a/STRONG_RESULT.md
+++ b/STRONG_RESULT.md
@@ -1,75 +1,78 @@
-# STRONG_RESULT — ¿el haz supera a CALM, o lo espeja? (T8c)
+# STRONG_RESULT — corregido por T9
-**Conclusión: VERSIÓN FUERTE PROBADA.** El haz da un veredicto estrictamente más
-fino que el CALM **sintáctico por-programa**, y lo hace por un camino honesto,
-sensible a la instancia y consciente de la topología. Con la salvedad de §F: ese
-veredicto booleano **es** I-confluence (Bailis et al. VLDB 2014) — no algo más
-allá de CALM, sino su refinamiento por-instancia, calculado sobre el grafo real.
+> **AVISO (T9 §G).** Este archivo reclamaba una "versión fuerte": que el haz
+> superaba a CALM vía I-confluence sensible a la instancia sobre el grafo real.
+> **Ese reclamo era falso** y está retirado. Lo que el testigo `[10,10]/[60,60]`
+> realmente probó, y el punto ciego que destapó, se documentan abajo. Un error
+> registrado con honestidad vale más que un resultado fuerte reclamado de más.
-## El testigo
+## Qué se retira (el reclamo de T8, incorrecto)
-Reproducible en `invariant::tests::discrepancia_buena_existe`.
+- ❌ "Versión fuerte probada / el haz es más fino que CALM."
+- ❌ "I-confluence sobre el grafo real como separación respecto a CALM."
+- ❌ "La topología importa: 60/60 particionado corre libre" **como virtud**.
-| | Instancia A (el premio) |
-|---|---|
-| Programa | dos réplicas retiran de una cuenta con saldo ≥ 0 |
-| Saldo inicial | `bound = 100` |
-| Retiros | `[10, 10]` (concurrentes) |
-| Grafo | `0 — 1` (comparten) |
-| Merge | `Σ retiros = 20 ≤ 100` ⟹ el invariante sobrevive |
-| **Haz (difusión + `∈ V`)** | **corre libre** |
-| **CALM sintáctico** | **coordina** (el retiro es no monótono en valor) |
-| I-confluence (oráculo indep.) | corre libre |
+**Por qué era falso (T9 §A):**
-`haz = libre` mientras `CALM-sintáctico = coordina`, con `I` preservado. Eso es la
-discrepancia buena de §D. Y no es una casualidad: el barrido
-`la_caza_encuentra_muchas_discrepancias` halla >100 testigos solo con dos réplicas
-sobre una cuenta de 100.
+1. **Detección, no evitación.** El veredicto `libre ⟺ punto_fijo ∈ V` funde dos
+ estados **ya divergidos** y comprueba el merge. Es detección reactiva
+ por-estado. Para un invariante duro llega tarde: si los retiros fueron
+ `[60,60]`, ya se aceptaron, y repararlos es compensación = coordinación.
+2. **No hay separación respecto a I-confluence ni a CALM.** "Retirar con saldo ≥ 0"
+ no es I-confluente porque *existe* un `[60,60]` que rompe `I` → coordina,
+ categórico, igual que CALM (`I-confluente ⟺ monótono`, Prop. 3 de Complete
+ CALM). El testigo `[10,10]` no era una cuña más fina: respondía **otra**
+ pregunta (¿este estado concreto ya fusionado es válido?), no la de coordinación.
+3. **El "60/60 particionado corre libre" era un BUG, no un refinamiento.** Un
+ invariante **global** codificado por aristas **pares** desaparece del haz al
+ particionar el grafo — justo cuando el acoplamiento sigue intacto. El detector
+ reporta "libre" el caso **más peligroso** porque está **ciego** a él. Ver
+ `COMPARISON.md`, fila 3, y el test `invariant::tests::t9_punto_ciego...`.
-## Por qué NO es circular (a diferencia de T5–T7)
+## Qué probó de verdad el testigo (lo que sí queda)
-1. **El orden sale del merge, no de la etiqueta** (T8a): `a ≤ b := merge(a,b)==b`.
- El haz nunca lee monótono/reset.
-2. **La coordinación sale del invariante, no del tipo de dato** (T8c): sin `I`
- todo CRDT corre libre (T8a/b); la obstrucción aparece solo cuando el merge
- empuja fuera de `V = {s : I(s)}`.
-3. **Dos caminos independientes coinciden** (`haz_iguala_i_confluence`): la
- difusión de merges y la suma aritmética por componente dan el mismo booleano en
- toda instancia. Corrección, no definición circular.
-4. **Soundness verificada** (`soundness_el_haz_nunca_miente`): el haz jamás dice
- "libre" con el invariante violado.
+Un **detector de conflicto por-estado con localización**: dado un conjunto
+concreto de estados y un grafo, funde por componentes y señala si el merge viola
+el invariante y qué réplicas/aristas lo empujan fuera de `V`. Útil como **alarma
+de reconciliación**, no como consejero de coordinación. No es novedad frente a
+I-confluence; es I-confluence evaluada sobre un estado concreto, con el punto
+ciego de la codificación por aristas.
-## Qué es novedad y qué no (honestidad §F)
+## Dónde está la evitación real (T9)
-- **NO es novedad el sí/no.** El veredicto booleano de la versión fuerte **es**
- I-confluence (Bailis 2014). Hay incluso una línea "Complete CALM" que muestra
- `I-confluente ⟺ monótono` bajo el orden dado por la validez del invariante: CALM,
- I-confluence y esta difusión son la misma moneda con tres órdenes distintos.
- Reclamar "más preciso que CALM" a secas sería medio cierto: somos más precisos
- que **CALM sintáctico por-programa**, que es justo lo que I-confluence ya hace.
-- **SÍ es el pitch defendible el *cómo* y la *propina*:** I-confluence sobre el
- **grafo de comunicación real** (topología-consciente, no un par de estados
- abstractos: ver `el_mismo_valor_depende_del_grafo` — los mismos retiros 60/60
- corren libres particionados y coordinan conectados), vía **difusión a punto
- fijo** que además entrega (a) el **estado reconciliado** y (b) la **localización**
- de las réplicas/aristas culpables. Un test de I-confluence estándar da un
- booleano; aquí te llevas el booleano, el merge y el nudo.
+La coordinación se **evita** —no se detecta tarde— con **escrow** (O'Neil 1986;
+Bounded Counter, Balegas et al. SRDS 2015):
-## Riesgo aceptado (R-T8b)
+- Reparto del slack `S` en presupuestos `b_i` con `Σ b_i ≤ S` (`escrow.rs`).
+- Gasto local sin coordinar mientras haya presupuesto — **correcto incluso
+ particionado**, que es justo donde el detector fallaba.
+- **Certificado por construcción:** `spent_i ≤ b_i ⟹ valor ≥ K`, para toda
+ ejecución, orden y partición (`escrow::tests::certificado_...`).
+- Única coordinación: rebalanceo **edge-local** ruteado por el Laplaciano sobre
+ el grafo real, conservando `Σ b` (`router.rs`).
-El predicado `p ∈ V` es un chequeo **añadido** sobre el punto fijo, no algo
-intrínseco al Laplaciano. No vendemos "la cohomología detecta la violación del
-invariante": la difusión calcula el *merge*; I-confluence es *merge + predicado de
-validez*. Y (R-T8c) el veredicto es por-configuración, no precomputable por
-programa — es la fuente de la precisión y un costo a reevaluar por estado en M4.
+**Honestidad (T9 §B):** escrow **tampoco** vence a CALM. *Transforma* la
+operación —de "retirar sin límite" (no I-confluente → coordina) a "retirar dentro
+de presupuesto" (I-confluente → libre)— al costo de un rebalanceo ocasional. No se
+rompe el teorema; se re-ingeniería la operación para caer del lado bueno.
-## Veredicto final del proyecto
+## El candidato a novedad honesto (T9 §C, R-T9c)
-- El MVP lineal medía **topología** (`H¹ = β₁`); útil como detector barato, pero
- falso-positivo en ciclos.
-- T5–T7 (retículos + Tarski) parecía cerrar la brecha, pero era **circular**:
- leía la etiqueta (`FLIPS.md`).
-- T8 rederiva todo del merge y ancla la coordinación en un **invariante**. El
- resultado honesto es un **test de I-confluence constructivo, localizado y
- consciente de la topología**. Esa es la contribución real y defendible; el
- camino a M4 (adaptador a sistemas soberanos) queda desbloqueado sobre esta base.
+No es el sí/no (eso es I-confluence, Bailis 2014). Es el **ruteo y la
+localización del presupuesto por el grafo de comunicación real**: `diffuse`
+suaviza proactivamente y `rebalance_to` localiza el flujo mínimo, edge-local, que
+repone a una réplica seca. La misma máquina Laplaciana que en el MVP era un
+detector con falso-positivo (`H¹ = β₁`) reaparece aquí como **ruteador legítimo**.
+El reach —múltiples invariantes acoplados vía haces (que Balegas señala como no
+resuelto)— sería nuevo; se reclamará solo si se construye.
+
+## Veredicto del arco
+
+- MVP lineal: medía **topología** (`H¹ = β₁`); detector barato, falso-positivo.
+- T5–T7 (retículos/Tarski): parecía cerrar la brecha, pero era **circular**
+ (`FLIPS.md`).
+- T8: rederivó del merge y ancló en un invariante, pero confundió **detección con
+ evitación** y trató un invariante **global como edge-local** (punto ciego).
+- **T9: evitación real por escrow, con certificado, ruteada por el grafo.** Ahí
+ está la contribución defendible — y las fronteras (R-T9b: recurso divisible;
+ R-T9c: la novedad es el ruteo/localización, no el booleano).
diff --git a/tests/comparison.rs b/tests/comparison.rs
new file mode 100644
index 0000000..5a67c60
--- /dev/null
+++ b/tests/comparison.rs
@@ -0,0 +1,50 @@
+//! Respaldo de `COMPARISON.md` (T9c): el detector de T8 y el certificador de
+//! escrow de T9 sobre los mismos escenarios. Los veredictos de la tabla del `.md`
+//! son exactamente los que asertan estos tests — nada escrito a mano.
+//!
+//! Cuenta común: saldo inicial 100, invariante `saldo ≥ 0` (slack 100).
+
+use sheafsync::escrow::{Budget, SpendResult};
+use sheafsync::invariant::AccountConfig;
+use sheafsync::oracle::OracleVerdict;
+
+/// Veredicto del DETECTOR de T8 (funde estados y comprueba el merge).
+fn detector(withdrawals: Vec<u64>, edges: Vec<(usize, usize)>) -> OracleVerdict {
+ AccountConfig::new("cmp", 100, withdrawals, edges).haz_coordination()
+}
+
+/// ¿El ESCROW de T9 permite todos los gastos localmente (sin coordinar) con el
+/// reparto dado? `true` = seguro sin coordinación; `false` = alguien pide rebalanceo.
+fn escrow_todo_local(withdrawals: &[u64], split: Vec<i64>) -> bool {
+ let mut budget = Budget::new(split);
+ withdrawals
+ .iter()
+ .enumerate()
+ .all(|(i, &w)| matches!(budget.try_spend(i, w as i64), SpendResult::Local))
+}
+
+#[test]
+fn escenarios_de_comparison_md() {
+ // 1) Conectado, retiros que caben (10/10).
+ assert_eq!(detector(vec![10, 10], vec![(0, 1)]), OracleVerdict::CoordinationFree);
+ assert!(escrow_todo_local(&[10, 10], vec![50, 50]));
+
+ // 2) Conectado, sobregiro (60/60): ambos detectan el problema.
+ assert_eq!(detector(vec![60, 60], vec![(0, 1)]), OracleVerdict::NeedsCoordination);
+ assert!(!escrow_todo_local(&[60, 60], vec![50, 50]));
+
+ // 3) PARTICIONADO, sobregiro (60/60): el detector da FALSO-VERDE...
+ assert_eq!(detector(vec![60, 60], vec![]), OracleVerdict::CoordinationFree);
+ // ...pero el escrow lo bloquea correctamente (60 > presupuesto de 50).
+ assert!(!escrow_todo_local(&[60, 60], vec![50, 50]));
+
+ // 4) Particionado, retiros que caben (10/10): ambos ok.
+ assert_eq!(detector(vec![10, 10], vec![]), OracleVerdict::CoordinationFree);
+ assert!(escrow_todo_local(&[10, 10], vec![50, 50]));
+
+ // 5) Reparto malo [100,0] (R-T9a): retiro 10 en la réplica seca pide
+ // rebalanceo aunque el slack global sobre — es rendimiento, no corrección.
+ assert!(!escrow_todo_local(&[0, 10], vec![100, 0]));
+ // Con un reparto equilibrado [50,50] el mismo gasto es local.
+ assert!(escrow_todo_local(&[0, 10], vec![50, 50]));
+}