SergioandClaude Opus 4.8
b666de794e
T8 §A/§B: el acuerdo perfecto de T7 con el oráculo era en parte circular (el encoding leía la etiqueta monótono/reset via 'generación = componente del subgrafo monótono'). T8a deriva el orden MECÁNICAMENTE del merge: - native::Merge (join := merge del CRDT; a ≤ b := merge(a,b)==b) + reconcile (propagación de joins a punto fijo). Impls para GCounter y LWW register. - oracle: tarski_verdict ahora es NATIVO (no lee la etiqueta); el circular de T7 se conserva como tarski_verdict_labeled (control histórico). tarski_reconcile expone el estado reconciliado (la 'propina' del haz). - Bajo el orden nativo el LWW-register es una CADENA → reconcilia al máximo → corre libre. Todo CRDT puro corre libre en cualquier grafo (ciclos incl.). FLIPS.md: 8 casos con reset voltean de 'coordina' (T7 circular) a 'corre libre' (nativo). Cada flip prueba que T5-T7 era circular ahí. DISCREPANCIES.md anota la salvedad. La versión débil (haz colapsa a CALM) no está descartada; se decide en T8c. 39 tests, clippy limpio. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
5.3 KiB
Discrepancias haz ↔ oráculo CALM
Registro de los casos donde el veredicto cohomológico lineal (H¹) no
coincide con el oráculo CRDT/CALM. Como dice el SDD (§8, §11 R1), esto no es un
bug a esconder: es el resultado científico del proyecto — dónde y por qué la
Hipótesis H (§2.2) se rompe bajo la codificación lineal del MVP.
ESTADO (lineal): RESUELTAS por la pista de retículos (M-research). El caso monótono-sobre-ciclo (triángulo/cuadrado) que el motor lineal marcaba como obstrucción corre libre bajo el orden nativo — eso es correcto y sigue en pie.
⚠️ SALVEDAD (T8, ver
FLIPS.md). El acuerdo perfecto de T7 con el oráculo era en parte circular: el encoding leía la etiqueta monótono/reset. T8a rederiva el orden del merge (sin etiqueta) y el veredicto de los casos conresetvoltea a corre libre. La resolución del caso monótono-cíclico es genuina; la de los reset era fabricada. La pregunta abierta (¿el haz supera a CALM o lo espeja?) se decide enSTRONG_RESULT.md(T8c).
Reproducibles con oracle::tests::discrepancias_del_lineal_persisten (el lineal
discrepa) y los casos de oracle::casos_de_discrepancia().
Resumen
| Caso | Oráculo (CALM) | Haz lineal (H¹) |
Difusión de Tarski | Estado |
|---|---|---|---|---|
triangulo-monotono |
corre libre | H¹ = 1 → coordina ❌ |
corre libre ✅ | RESUELTA |
cuadrado-monotono |
corre libre | H¹ = 1 → coordina ❌ |
corre libre ✅ | RESUELTA |
| (general) dato monótono sobre grafo cíclico | corre libre | H¹ = b₁ ≠ 0 ❌ |
corre libre ✅ | RESUELTA |
El MVP lineal coincide con el oráculo en todo el régimen de
oracle::casos_de_acuerdo() (≥20 casos: sharing monótono acíclico y cualquier
configuración no monótona). Tarski coincide en toda la batería, sin excepción,
incluidos los cíclicos monótonos de arriba.
La discrepancia, en detalle
El caso. Tres réplicas comparten un dato monótono (p.ej. un GCounter)
en un triángulo: 0—1, 1—2, 2—0. Todas las operaciones son monótonas.
Qué dice CALM (oráculo). Un GCounter se funde por máximo casilla a casilla;
el join siempre existe y es único. No hay operación que retracte conocimiento,
luego la configuración es coordination-free. El ciclo en el grafo de
compartición es irrelevante: más caminos para difundir la misma información
monótona no crean un conflicto.
Qué dice el haz. La codificación lineal del MVP modela cada dato compartido
como una restricción de acuerdo (identidad). Sobre el triángulo, el haz
constante tiene dim H¹ = b₁ = E − V + C = 3 − 3 + 1 = 1. El motor reporta una
obstrucción y pide coordinar.
Por qué ocurre (§2.3, R1). La cohomología de haces es lineal; los
retículos de los CRDTs son de orden (join-semilattices). Al aplanar el orden
a álgebra lineal, el haz pierde la información de que la fusión monótona siempre
pega las secciones locales. Lo que le queda es la topología pura del grafo, y la
topología de un ciclo tiene H¹ ≠ 0 con independencia de los datos. El haz
"ve" así una obstrucción topológica donde CALM no ve ninguna semántica.
Dicho de otro modo: bajo esta codificación, H¹ = 0 ⟺ el grafo de compartición es acíclico, un enunciado puramente topológico que solo coincide con CALM
cuando el ciclo, de existir, transporta una operación no monótona (y por eso la
codificación honesta añade un segundo enlace en conflicto solo en ese caso).
Consecuencia para la Hipótesis H
En el MVP lineal, la Hipótesis H (H¹ = 0 ⟺ coordination-free) se sostiene
para configuraciones cuyo sharing monótono es acíclico, y falla para datos
monótonos sobre grafos cíclicos. La dirección que falla es conservadora: el haz
pide coordinación de más (falsos positivos), nunca de menos. No se observó el
fallo inverso (haz dice "libre" donde CALM dice "coordina").
Bajo el encoding de retículos con el Laplaciano de Tarski (Addendum), la
Hipótesis H pasa de "se sostiene solo en el caso acíclico" a "se sostiene en
general": la difusión reconcilia el dato monótono alrededor del ciclo sin
colapsar, y solo colapsa a ⊤ ante una operación semánticamente incompatible (un
reset que hace incomparables las generaciones). Verificado además por el
invariante proptest "monótono sobre grafo arbitrario (cíclico incluido) ⟹
corre libre", que el motor lineal no podía satisfacer.
Cómo se cerró (Addendum §B–§F, §2.3 / §11 Q2)
Causa raíz: la resta del coboundary (δx)_e = R·x_u − R·x_v. Un
join-semilattice no tiene inversos; al linealizarlo, δ mide desacuerdo-XOR e
inventa obstrucciones-fantasma alrededor de los ciclos.
La cura fue eliminar la resta: haces valuados en retículos con
restricciones como conexiones de Galois, y el Laplaciano de Tarski
(Ghrist–Riess 2022) difundido a punto fijo (Kleene/Tarski). El punto fijo es la
mejor reconciliación coherente; corre libre si preserva lo local sin colapsar a ⊤.
Ver src/lattice.rs, src/tarski.rs y Verdict::via_tarski.
Residuo abierto
No se ha encontrado ningún caso donde Tarski y el oráculo discrepen. Si apareciera (p.ej. un CRDT que pida ya un quantale, R-L/Q-L1 del Addendum), ese residuo sería el siguiente resultado científico y se anotaría aquí.