# SDD — Addendum: T8 · De-circularizar y cazar la discrepancia buena **Extiende:** `DESIGN.md` (SDD v1) + `DESIGN_lattice.md` (pista de retículos, T5–T7). **Estado:** Diseño — habilitado por la duda de circularidad al cierre de T7. **Precondición:** T5–T7 cerrados. `via_tarski` funciona. Batería y `DISCREPANCIES.md` verdes. **Última edición:** 2026-07-01 --- ## A. El problema que T8 resuelve (por qué el verde de T7 no basta) El test maestro de T7 exige que Tarski **coincida con el oráculo en toda la batería**. Pero acuerdo perfecto con CALM es también, exactamente, lo que produce un **encoding circular**. Y la pieza que carga el peso lo delata: `generación = componente del subgrafo monótono`. Eso significa que el encoding *ya lee* la etiqueta monótono/reset — la misma información que CALM usa — y con ella fabrica la incomparabilidad que hace colapsar a los reset. No podemos descartar que Tarski no esté *descubriendo* la frontera de coordinación, sino *reproduciendo* la respuesta de CALM que le metimos disfrazada de retículo. Un espejo, no un teorema. **Dos hipótesis rivales que T8 debe separar:** - **Versión débil.** El haz colapsa a CALM. Su valor no es un veredicto más fino, sino que además de sí/no te entrega el **punto fijo** (el estado global reconciliado) y la **localización** de las aristas del nudo. Real, útil, pero no "más preciso que CALM". - **Versión fuerte.** El haz es sensible a la *instancia*: existe una configuración con una operación no monótona cuyos **valores concretos** sí pegan, donde CALM (regla sintáctica, por-programa) dice `coordina` y una difusión honesta dice `corre libre`. Ese caso — Tarski libre / CALM coordina — es el premio, y es la única evidencia de que tienes un instrumento más fino y no una reimplementación cara. El test de T7, al prohibir la discrepancia, está diseñado para no encontrar nunca la versión fuerte. T8 invierte el criterio: primero mata la circularidad, luego **persigue** la discrepancia buena. **El marco correcto ya tiene nombre:** *invariant confluence* (I-confluence), Bailis et al. VLDB 2014 (arXiv:1402.2237). Un conjunto de transacciones es I-confluente respecto a un invariante `I` si fusionar dos estados I-válidos con ancestro común da un estado I-válido; y esa es condición **necesaria y suficiente** para ejecución libre de coordinación. I-confluence es precisamente el refinamiento *sensible a la instancia* de CALM — coordina solo cuando la fusión *puede* violar el invariante, no cuando el programa *podría* ser no monótono. La versión fuerte de tu proyecto ES un test de I-confluence calculado sobre el grafo real de réplicas. Convendría saberlo antes de reclamar novedad (§F). --- ## B. La cura de raíz: derivar el retículo del merge, no de la etiqueta La circularidad se elimina estructuralmente si el retículo **se deriva mecánicamente de la propia función de fusión del CRDT**, sin tocar jamás la etiqueta monótono/reset: ``` join(a, b) := merge_del_CRDT(a, b) // la fusión que el tipo YA implementa a ≤ b := ( merge(a, b) == b ) // orden inducido por el merge bottom := estado vacío / inicial ``` Con esta regla es **imposible** filtrar la respuesta de CALM: solo usas la semántica de fusión que el dato ya trae. Consecuencias que hay que aceptar con honestidad: - `GCounter` → orden componente-a-componente, `join = max`. Libre de coordinación en cualquier grafo, incluidos ciclos. Correcto: es un CRDT. - **Registro con reset (LWW)** → su merge es "gana el timestamp mayor". El orden inducido es una **cadena** (totalmente ordenada por timestamp). En una cadena la difusión siempre reconcilia al máximo → **corre libre**. Es decir: bajo el orden nativo, el reset **NO colapsa**. Y eso es correcto, porque un LWW-register es un CRDT y los CRDT son libres de coordinación por construcción. **Implicación incómoda pero sana:** el veredicto `coordina` que T5–T7 daba al reset era *fabricado* por la incomparabilidad puesta a mano. Con el orden nativo, ese caso **debe voltearse a `corre libre`** — y si el oráculo aún lo llama `coordina`, el oráculo también estaba mal (usaba monotonía de *valor*, no monotonía en el *retículo de fusión*). La obstrucción real no vive en el tipo de dato; vive en el **invariante** (§C). Ese es el corazón de T8. --- ## C. De dónde sale la coordinación de verdad: el invariante Sin invariante, un CRDT nunca necesita coordinar. La coordinación aparece cuando hay un **invariante global `I`** que ninguna fusión local garantiza. Los estados válidos `V = { s : I(s) }` forman un subconjunto del retículo que **no es cerrado bajo join**: dos estados localmente válidos pueden fundirse en uno inválido. Ejemplo canónico no-CALM (Bailis): saldo ≥ 0, o IDs únicos. Dos réplicas retiran por separado, cada una válida; el join sobregira. O dos réplicas asignan el mismo ID único; el join viola unicidad. **Veredicto del haz, versión honesta:** 1. `harmonize` a punto fijo `p` (el estado fusionado que ya sabes calcular). 2. **corre libre** ⟺ `p ∈ V` (el invariante sobrevive a la fusión). 3. **coordina** ⟺ `p ∉ V` (la fusión rompe `I`; localiza las aristas cuyo aporte empuja fuera de `V`). Esto es, literalmente, un **test de I-confluence constructivo sobre la instancia**, ejecutado sobre el grafo de réplicas. Y es sensible a los valores: el mismo programa da distinto veredicto según qué números concretos tengan las réplicas. Ahí vive la versión fuerte. --- ## D. El experimento: cazar la discrepancia `Tarski=libre / CALM=coordina` Construye pares de instancias con **el mismo programa** (misma operación no monótona, guardada por `I`) y **valores distintos**: | Instancia | Valores | join ∈ V | Haz (Tarski) | CALM sintáctico | Veredicto del par | |---|---|---|---|---|---| | A | retiros que caben en el saldo | sí | **corre libre** | coordina (op no monótona) | **discrepancia buena** ✓ | | B | retiros que sobregiran | no | coordina | coordina | acuerdo | La instancia **A** es el premio: el haz corre libre donde CALM coordina, porque los valores concretos pegan. Si existe, tienes análisis de coordinación sensible a la instancia — estrictamente más que un check sintáctico. **El oráculo correcto ahora es I-confluence, no CALM sintáctico.** El veredicto del haz debe coincidir con "¿el merge cae en `V`?" en *toda* instancia (eso es corrección). La discrepancia que persigues es contra el CALM *por-programa*, y encontrarla es el objetivo, no un fallo. --- ## E. Cambios de criterio de prueba (T8 invierte T7) El test maestro de T7 afirmaba `haz == oráculo` en todo. T8 lo reemplaza por tres aserciones: 1. **De-circularización (T8a/b).** Con el retículo derivado del merge (§B) y el oráculo corregido a monotonía-de-fusión, todos los CRDT puros corren libres en cualquier grafo bajo *ambos* métodos. El acuerdo aquí no es circular: es correcto, y por la razón correcta. 2. **Soundness (sin discrepancia mala).** El haz **nunca** dice `corre libre` cuando el estado fusionado viola `I`. Esta no se negocia. 3. **Existencia de la discrepancia buena (o su imposibilidad).** O bien exhibes una instancia A donde `haz=libre` y `CALM-sintáctico=coordina` con `I` preservado — versión fuerte probada —, o bien demuestras que bajo tu encoding no puede existir — y entonces reportas honestamente que el haz colapsa a CALM y su valor es la localización + el estado reconciliado. `proptest`: genera invariantes lineales simples (saldo ≥ 0, cota superior, unicidad) y busca activamente instancias de tipo A. Un `proptest` que *encuentra* el testigo es más valioso que uno que verifica un invariante. --- ## F. Honestidad sobre la novedad (para no comerte una revisión) - El **veredicto booleano** de la versión fuerte **es** I-confluence (Bailis et al. 2014). No lo estás inventando. Hay incluso un resultado que muestra `I-confluente ⟺ monótono` bajo el orden de resultados dado por la validez del invariante (línea "Complete CALM"), así que CALM, I-confluence y tu difusión son la misma moneda vista con tres órdenes distintos. Reclamar "más preciso que CALM" a secas es medio cierto: eres más preciso que **CALM sintáctico por-programa**, que es exactamente lo que I-confluence ya hace. - El **candidato a novedad** no es el sí/no, es *cómo* lo obtienes y qué te llevas de propina: I-confluence sobre el **grafo de comunicación real** (topología-consciente, no un par de estados abstractos), vía **difusión a punto fijo** que además te entrega (a) el **estado reconciliado** y (b) la **localización** de las aristas culpables. Un test de I-confluence estándar te da un booleano; tú te llevas el booleano, el merge y el nudo. Ese es el pitch defendible. - Si al final es la versión débil, sigue valiendo — pero entonces el pitch honesto es "I-confluence constructivo y localizado sobre topologías arbitrarias", no "supero a CALM". --- ## G. Tickets **T8a — Encoding desde el orden nativo (mata la circularidad).** "Reescribe el encoding de retículo (`lattice.rs`, `tarski_verdict`) para derivar `(L, ≤, join)` MECÁNICAMENTE del merge del CRDT según §B: `join := merge`, `a ≤ b := merge(a,b)==b`. Elimina TODA referencia a la etiqueta monótono/reset y a `generación = componente del subgrafo monótono`. Reejecuta la batería. Documenta en `FLIPS.md` cada veredicto que cambie respecto a T7 — en particular, el registro con reset (LWW) debe voltear de `coordina` a `corre libre`. Un flip = T5–T7 era circular ahí." **T8b — Auditar y corregir el oráculo.** "Revisa `oracle.rs`: si clasifica un CRDT puro (LWW, PN-Counter) como `NeedsCoordination`, estaba usando monotonía de valor, no monotonía en el retículo de fusión. Corrige `oracle_verdict` al criterio CALM real (monótono en el orden en que se hace merge). Test: tras la corrección, todos los CRDT puros son `CoordinationFree` bajo oráculo y haz, sobre grafos cíclicos incluidos. Este acuerdo es correcto, no circular — justifícalo en un comentario." **T8c — Invariante, I-confluence y caza de la discrepancia buena.** "Añade un tipo de operación guardada por invariante `I` (empieza con saldo ≥ 0; añade unicidad de ID como segundo caso — el ejemplo de Bailis). Define `V = {s : I(s)}` y el veredicto por difusión de §C: `corre libre ⟺ punto_fijo ∈ V`, con localización de las aristas que empujan fuera de `V`. Implementa un oráculo de I-confluence independiente (`merge(Di,Dj) ∈ V` sobre estados alcanzables con ancestro común) y exige que el haz lo iguale en toda instancia (soundness §E.2). Luego escribe el test que INVIERTE T7: un `proptest` que **busca** una instancia tipo A (retiros que caben) donde `haz=corre libre` y `CALM-sintáctico=coordina`. Si la encuentra, imprime el testigo y márcala en `STRONG_RESULT.md`. Si demuestras que no puede existir bajo el encoding, documenta en `STRONG_RESULT.md` que el haz colapsa a CALM y por qué. No hagas M4 hasta cerrar este archivo con una de las dos conclusiones." --- ## H. Riesgos de T8 - **R-T8a (orden honesto).** El orden nativo debe salir *del merge*, no de tu conveniencia. La regla `a ≤ b := merge(a,b)==b` lo garantiza mecánicamente; no la puentees "ajustando" el retículo a mano. - **R-T8b (invariante ≠ cohomología).** El check `p ∈ V` es un predicado **añadido** sobre el punto fijo, no algo intrínseco al Laplaciano. No vendas "la cohomología detecta la violación del invariante": la difusión calcula el *merge*; I-confluence es *merge + predicado de validez*. Dilo así. - **R-T8c (costo de la instancia-sensibilidad).** El veredicto pasa a ser por-configuración: no hay respuesta por-programa precomputable. Es la fuente de tu precisión y también un costo en M4 (hay que reevaluar por estado). Anótalo para el adaptador. --- ## I. Referencias añadidas - P. Bailis, A. Fekete, M. J. Franklin, A. Ghodsi, J. M. Hellerstein, I. Stoica — *Coordination Avoidance in Database Systems*, Proc. VLDB Endow. 8(3):185–196 (2014). arXiv:1402.2237. (I-confluence: el marco sensible a la instancia que tu versión fuerte instancia.) - (Contexto) Trabajo que relaciona I-confluence con monotonía bajo el orden de validez del invariante (línea "Complete CALM"). Útil para posicionar el aparato sin sobre-reclamar. - (De addenda previos) Ghrist–Riess 2022 (Tarski); Shapiro et al. 2011 (CRDTs); Hellerstein–Alvaro (CALM); Hansen–Ghrist 2019 (base lineal).