1# SDD — Addendum: T8 · De-circularizar y cazar la discrepancia buena
2
3**Extiende:** `DESIGN.md` (SDD v1) + `DESIGN_lattice.md` (pista de retículos, T5–T7).
4**Estado:** Diseño — habilitado por la duda de circularidad al cierre de T7.
5**Precondición:** T5–T7 cerrados. `via_tarski` funciona. Batería y `DISCREPANCIES.md` verdes.
6**Última edición:** 2026-07-01
7
8---
9
10## A. El problema que T8 resuelve (por qué el verde de T7 no basta)
11
12El test maestro de T7 exige que Tarski **coincida con el oráculo en toda la batería**. Pero acuerdo
13perfecto con CALM es también, exactamente, lo que produce un **encoding circular**. Y la pieza que carga
14el peso lo delata: `generación = componente del subgrafo monótono`. Eso significa que el encoding *ya lee*
15la etiqueta monótono/reset — la misma información que CALM usa — y con ella fabrica la incomparabilidad que
16hace colapsar a los reset. No podemos descartar que Tarski no esté *descubriendo* la frontera de
17coordinación, sino *reproduciendo* la respuesta de CALM que le metimos disfrazada de retículo. Un espejo,
18no un teorema.
19
20**Dos hipótesis rivales que T8 debe separar:**
21
22- **Versión débil.** El haz colapsa a CALM. Su valor no es un veredicto más fino, sino que además de
23  sí/no te entrega el **punto fijo** (el estado global reconciliado) y la **localización** de las aristas
24  del nudo. Real, útil, pero no "más preciso que CALM".
25- **Versión fuerte.** El haz es sensible a la *instancia*: existe una configuración con una operación
26  no monótona cuyos **valores concretos** sí pegan, donde CALM (regla sintáctica, por-programa) dice
27  `coordina` y una difusión honesta dice `corre libre`. Ese caso — Tarski libre / CALM coordina — es el
28  premio, y es la única evidencia de que tienes un instrumento más fino y no una reimplementación cara.
29
30El test de T7, al prohibir la discrepancia, está diseñado para no encontrar nunca la versión fuerte.
31T8 invierte el criterio: primero mata la circularidad, luego **persigue** la discrepancia buena.
32
33**El marco correcto ya tiene nombre:** *invariant confluence* (I-confluence), Bailis et al. VLDB 2014
34(arXiv:1402.2237). Un conjunto de transacciones es I-confluente respecto a un invariante `I` si fusionar
35dos estados I-válidos con ancestro común da un estado I-válido; y esa es condición **necesaria y
36suficiente** para ejecución libre de coordinación. I-confluence es precisamente el refinamiento
37*sensible a la instancia* de CALM — coordina solo cuando la fusión *puede* violar el invariante, no cuando
38el programa *podría* ser no monótono. La versión fuerte de tu proyecto ES un test de I-confluence
39calculado sobre el grafo real de réplicas. Convendría saberlo antes de reclamar novedad (§F).
40
41---
42
43## B. La cura de raíz: derivar el retículo del merge, no de la etiqueta
44
45La circularidad se elimina estructuralmente si el retículo **se deriva mecánicamente de la propia función
46de fusión del CRDT**, sin tocar jamás la etiqueta monótono/reset:
47
48```
49join(a, b) := merge_del_CRDT(a, b)          // la fusión que el tipo YA implementa
50a ≤ b       := ( merge(a, b) == b )          // orden inducido por el merge
51bottom      := estado vacío / inicial
52```
53
54Con esta regla es **imposible** filtrar la respuesta de CALM: solo usas la semántica de fusión que el dato
55ya trae. Consecuencias que hay que aceptar con honestidad:
56
57- `GCounter` → orden componente-a-componente, `join = max`. Libre de coordinación en cualquier grafo,
58  incluidos ciclos. Correcto: es un CRDT.
59- **Registro con reset (LWW)** → su merge es "gana el timestamp mayor". El orden inducido es una **cadena**
60  (totalmente ordenada por timestamp). En una cadena la difusión siempre reconcilia al máximo → **corre
61  libre**. Es decir: bajo el orden nativo, el reset **NO colapsa**. Y eso es correcto, porque un
62  LWW-register es un CRDT y los CRDT son libres de coordinación por construcción.
63
64**Implicación incómoda pero sana:** el veredicto `coordina` que T5–T7 daba al reset era *fabricado* por la
65incomparabilidad puesta a mano. Con el orden nativo, ese caso **debe voltearse a `corre libre`** — y si el
66oráculo aún lo llama `coordina`, el oráculo también estaba mal (usaba monotonía de *valor*, no monotonía
67en el *retículo de fusión*). La obstrucción real no vive en el tipo de dato; vive en el **invariante**
68(§C). Ese es el corazón de T8.
69
70---
71
72## C. De dónde sale la coordinación de verdad: el invariante
73
74Sin invariante, un CRDT nunca necesita coordinar. La coordinación aparece cuando hay un **invariante
75global `I`** que ninguna fusión local garantiza. Los estados válidos `V = { s : I(s) }` forman un
76subconjunto del retículo que **no es cerrado bajo join**: dos estados localmente válidos pueden fundirse
77en uno inválido.
78
79Ejemplo canónico no-CALM (Bailis): saldo ≥ 0, o IDs únicos. Dos réplicas retiran por separado, cada una
80válida; el join sobregira. O dos réplicas asignan el mismo ID único; el join viola unicidad.
81
82**Veredicto del haz, versión honesta:**
83
841. `harmonize` a punto fijo `p` (el estado fusionado que ya sabes calcular).
852. **corre libre** ⟺ `p ∈ V` (el invariante sobrevive a la fusión).
863. **coordina** ⟺ `p ∉ V` (la fusión rompe `I`; localiza las aristas cuyo aporte empuja fuera de `V`).
87
88Esto es, literalmente, un **test de I-confluence constructivo sobre la instancia**, ejecutado sobre el
89grafo de réplicas. Y es sensible a los valores: el mismo programa da distinto veredicto según qué números
90concretos tengan las réplicas. Ahí vive la versión fuerte.
91
92---
93
94## D. El experimento: cazar la discrepancia `Tarski=libre / CALM=coordina`
95
96Construye pares de instancias con **el mismo programa** (misma operación no monótona, guardada por `I`) y
97**valores distintos**:
98
99| Instancia | Valores | join ∈ V | Haz (Tarski) | CALM sintáctico | Veredicto del par |
100|---|---|---|---|---|---|
101| A | retiros que caben en el saldo | sí | **corre libre** | coordina (op no monótona) | **discrepancia buena** ✓ |
102| B | retiros que sobregiran | no | coordina | coordina | acuerdo |
103
104La instancia **A** es el premio: el haz corre libre donde CALM coordina, porque los valores concretos
105pegan. Si existe, tienes análisis de coordinación sensible a la instancia — estrictamente más que un
106check sintáctico.
107
108**El oráculo correcto ahora es I-confluence, no CALM sintáctico.** El veredicto del haz debe coincidir con
109"¿el merge cae en `V`?" en *toda* instancia (eso es corrección). La discrepancia que persigues es contra
110el CALM *por-programa*, y encontrarla es el objetivo, no un fallo.
111
112---
113
114## E. Cambios de criterio de prueba (T8 invierte T7)
115
116El test maestro de T7 afirmaba `haz == oráculo` en todo. T8 lo reemplaza por tres aserciones:
117
1181. **De-circularización (T8a/b).** Con el retículo derivado del merge (§B) y el oráculo corregido a
119   monotonía-de-fusión, todos los CRDT puros corren libres en cualquier grafo bajo *ambos* métodos. El
120   acuerdo aquí no es circular: es correcto, y por la razón correcta.
1212. **Soundness (sin discrepancia mala).** El haz **nunca** dice `corre libre` cuando el estado fusionado
122   viola `I`. Esta no se negocia.
1233. **Existencia de la discrepancia buena (o su imposibilidad).** O bien exhibes una instancia A donde
124   `haz=libre` y `CALM-sintáctico=coordina` con `I` preservado — versión fuerte probada —, o bien
125   demuestras que bajo tu encoding no puede existir — y entonces reportas honestamente que el haz colapsa
126   a CALM y su valor es la localización + el estado reconciliado.
127
128`proptest`: genera invariantes lineales simples (saldo ≥ 0, cota superior, unicidad) y busca activamente
129instancias de tipo A. Un `proptest` que *encuentra* el testigo es más valioso que uno que verifica un
130invariante.
131
132---
133
134## F. Honestidad sobre la novedad (para no comerte una revisión)
135
136- El **veredicto booleano** de la versión fuerte **es** I-confluence (Bailis et al. 2014). No lo estás
137  inventando. Hay incluso un resultado que muestra `I-confluente ⟺ monótono` bajo el orden de resultados
138  dado por la validez del invariante (línea "Complete CALM"), así que CALM, I-confluence y tu difusión son
139  la misma moneda vista con tres órdenes distintos. Reclamar "más preciso que CALM" a secas es medio
140  cierto: eres más preciso que **CALM sintáctico por-programa**, que es exactamente lo que I-confluence ya
141  hace.
142- El **candidato a novedad** no es el sí/no, es *cómo* lo obtienes y qué te llevas de propina:
143  I-confluence sobre el **grafo de comunicación real** (topología-consciente, no un par de estados
144  abstractos), vía **difusión a punto fijo** que además te entrega (a) el **estado reconciliado** y (b) la
145  **localización** de las aristas culpables. Un test de I-confluence estándar te da un booleano; tú te
146  llevas el booleano, el merge y el nudo. Ese es el pitch defendible.
147- Si al final es la versión débil, sigue valiendo — pero entonces el pitch honesto es "I-confluence
148  constructivo y localizado sobre topologías arbitrarias", no "supero a CALM".
149
150---
151
152## G. Tickets
153
154**T8a — Encoding desde el orden nativo (mata la circularidad).**
155"Reescribe el encoding de retículo (`lattice.rs`, `tarski_verdict`) para derivar `(L, ≤, join)`
156MECÁNICAMENTE del merge del CRDT según §B: `join := merge`, `a ≤ b := merge(a,b)==b`. Elimina TODA
157referencia a la etiqueta monótono/reset y a `generación = componente del subgrafo monótono`. Reejecuta la
158batería. Documenta en `FLIPS.md` cada veredicto que cambie respecto a T7 — en particular, el registro con
159reset (LWW) debe voltear de `coordina` a `corre libre`. Un flip = T5–T7 era circular ahí."
160
161**T8b — Auditar y corregir el oráculo.**
162"Revisa `oracle.rs`: si clasifica un CRDT puro (LWW, PN-Counter) como `NeedsCoordination`, estaba usando
163monotonía de valor, no monotonía en el retículo de fusión. Corrige `oracle_verdict` al criterio CALM real
164(monótono en el orden en que se hace merge). Test: tras la corrección, todos los CRDT puros son
165`CoordinationFree` bajo oráculo y haz, sobre grafos cíclicos incluidos. Este acuerdo es correcto, no
166circular — justifícalo en un comentario."
167
168**T8c — Invariante, I-confluence y caza de la discrepancia buena.**
169"Añade un tipo de operación guardada por invariante `I` (empieza con saldo ≥ 0; añade unicidad de ID como
170segundo caso — el ejemplo de Bailis). Define `V = {s : I(s)}` y el veredicto por difusión de §C: `corre
171libre ⟺ punto_fijo ∈ V`, con localización de las aristas que empujan fuera de `V`. Implementa un oráculo
172de I-confluence independiente (`merge(Di,Dj) ∈ V` sobre estados alcanzables con ancestro común) y exige
173que el haz lo iguale en toda instancia (soundness §E.2). Luego escribe el test que INVIERTE T7: un
174`proptest` que **busca** una instancia tipo A (retiros que caben) donde `haz=corre libre` y
175`CALM-sintáctico=coordina`. Si la encuentra, imprime el testigo y márcala en `STRONG_RESULT.md`. Si
176demuestras que no puede existir bajo el encoding, documenta en `STRONG_RESULT.md` que el haz colapsa a
177CALM y por qué. No hagas M4 hasta cerrar este archivo con una de las dos conclusiones."
178
179---
180
181## H. Riesgos de T8
182
183- **R-T8a (orden honesto).** El orden nativo debe salir *del merge*, no de tu conveniencia. La regla `a ≤ b
184  := merge(a,b)==b` lo garantiza mecánicamente; no la puentees "ajustando" el retículo a mano.
185- **R-T8b (invariante ≠ cohomología).** El check `p ∈ V` es un predicado **añadido** sobre el punto fijo,
186  no algo intrínseco al Laplaciano. No vendas "la cohomología detecta la violación del invariante": la
187  difusión calcula el *merge*; I-confluence es *merge + predicado de validez*. Dilo así.
188- **R-T8c (costo de la instancia-sensibilidad).** El veredicto pasa a ser por-configuración: no hay
189  respuesta por-programa precomputable. Es la fuente de tu precisión y también un costo en M4 (hay que
190  reevaluar por estado). Anótalo para el adaptador.
191
192---
193
194## I. Referencias añadidas
195
196- P. Bailis, A. Fekete, M. J. Franklin, A. Ghodsi, J. M. Hellerstein, I. Stoica — *Coordination Avoidance
197  in Database Systems*, Proc. VLDB Endow. 8(3):185–196 (2014). arXiv:1402.2237. (I-confluence: el marco
198  sensible a la instancia que tu versión fuerte instancia.)
199- (Contexto) Trabajo que relaciona I-confluence con monotonía bajo el orden de validez del invariante
200  (línea "Complete CALM"). Útil para posicionar el aparato sin sobre-reclamar.
201- (De addenda previos) Ghrist–Riess 2022 (Tarski); Shapiro et al. 2011 (CRDTs); Hellerstein–Alvaro (CALM);
202  Hansen–Ghrist 2019 (base lineal).