tawasuyu

tawasuyu/hifas

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 Definiciones

⎇ d2514b766a207ec049b26727f541c4d32d2a89c5 STRONG_RESULT.md Markdown · 75 líneas · 4.0 KB Historia crudo

T8c: invariante, I-confluence y la discrepancia buena (versión fuerte) d2514b766 · Sergio · 

1# STRONG_RESULT — ¿el haz supera a CALM, o lo espeja? (T8c)
2
3**Conclusión: VERSIÓN FUERTE PROBADA.** El haz da un veredicto estrictamente más
4fino que el CALM **sintáctico por-programa**, y lo hace por un camino honesto,
5sensible a la instancia y consciente de la topología. Con la salvedad de §F: ese
6veredicto booleano **es** I-confluence (Bailis et al. VLDB 2014) — no algo más
7allá de CALM, sino su refinamiento por-instancia, calculado sobre el grafo real.
8
9## El testigo
10
11Reproducible en `invariant::tests::discrepancia_buena_existe`.
12
13| | Instancia A (el premio) |
14|---|---|
15| Programa | dos réplicas retiran de una cuenta con saldo ≥ 0 |
16| Saldo inicial | `bound = 100` |
17| Retiros | `[10, 10]` (concurrentes) |
18| Grafo | `0 — 1` (comparten) |
19| Merge | `Σ retiros = 20 ≤ 100` ⟹ el invariante sobrevive |
20| **Haz (difusión + `∈ V`)** | **corre libre** |
21| **CALM sintáctico** | **coordina** (el retiro es no monótono en valor) |
22| I-confluence (oráculo indep.) | corre libre |
23
24`haz = libre` mientras `CALM-sintáctico = coordina`, con `I` preservado. Eso es la
25discrepancia buena de §D. Y no es una casualidad: el barrido
26`la_caza_encuentra_muchas_discrepancias` halla >100 testigos solo con dos réplicas
27sobre una cuenta de 100.
28
29## Por qué NO es circular (a diferencia de T5–T7)
30
311. **El orden sale del merge, no de la etiqueta** (T8a): `a ≤ b := merge(a,b)==b`.
32   El haz nunca lee monótono/reset.
332. **La coordinación sale del invariante, no del tipo de dato** (T8c): sin `I`
34   todo CRDT corre libre (T8a/b); la obstrucción aparece solo cuando el merge
35   empuja fuera de `V = {s : I(s)}`.
363. **Dos caminos independientes coinciden** (`haz_iguala_i_confluence`): la
37   difusión de merges y la suma aritmética por componente dan el mismo booleano en
38   toda instancia. Corrección, no definición circular.
394. **Soundness verificada** (`soundness_el_haz_nunca_miente`): el haz jamás dice
40   "libre" con el invariante violado.
41
42## Qué es novedad y qué no (honestidad §F)
43
44- **NO es novedad el sí/no.** El veredicto booleano de la versión fuerte **es**
45  I-confluence (Bailis 2014). Hay incluso una línea "Complete CALM" que muestra
46  `I-confluente ⟺ monótono` bajo el orden dado por la validez del invariante: CALM,
47  I-confluence y esta difusión son la misma moneda con tres órdenes distintos.
48  Reclamar "más preciso que CALM" a secas sería medio cierto: somos más precisos
49  que **CALM sintáctico por-programa**, que es justo lo que I-confluence ya hace.
50- **SÍ es el pitch defendible el *cómo* y la *propina*:** I-confluence sobre el
51  **grafo de comunicación real** (topología-consciente, no un par de estados
52  abstractos: ver `el_mismo_valor_depende_del_grafo` — los mismos retiros 60/60
53  corren libres particionados y coordinan conectados), vía **difusión a punto
54  fijo** que además entrega (a) el **estado reconciliado** y (b) la **localización**
55  de las réplicas/aristas culpables. Un test de I-confluence estándar da un
56  booleano; aquí te llevas el booleano, el merge y el nudo.
57
58## Riesgo aceptado (R-T8b)
59
60El predicado `p ∈ V` es un chequeo **añadido** sobre el punto fijo, no algo
61intrínseco al Laplaciano. No vendemos "la cohomología detecta la violación del
62invariante": la difusión calcula el *merge*; I-confluence es *merge + predicado de
63validez*. Y (R-T8c) el veredicto es por-configuración, no precomputable por
64programa — es la fuente de la precisión y un costo a reevaluar por estado en M4.
65
66## Veredicto final del proyecto
67
68- El MVP lineal medía **topología** (`H¹ = β₁`); útil como detector barato, pero
69  falso-positivo en ciclos.
70- T5–T7 (retículos + Tarski) parecía cerrar la brecha, pero era **circular**:
71  leía la etiqueta (`FLIPS.md`).
72- T8 rederiva todo del merge y ancla la coordinación en un **invariante**. El
73  resultado honesto es un **test de I-confluence constructivo, localizado y
74  consciente de la topología**. Esa es la contribución real y defendible; el
75  camino a M4 (adaptador a sistemas soberanos) queda desbloqueado sobre esta base.

STRONG_RESULT.md

STRONG_RESULT — ¿el haz supera a CALM, o lo espeja? (T8c)

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.

El testigo

Reproducible en invariant::tests::discrepancia_buena_existe.

Instancia A (el premio)
Programados réplicas retiran de una cuenta con saldo ≥ 0
Saldo inicialbound = 100
Retiros[10, 10] (concurrentes)
Grafo0 — 1 (comparten)
MergeΣ retiros = 20 ≤ 100 ⟹ el invariante sobrevive
Haz (difusión + ∈ V)corre libre
CALM sintácticocoordina (el retiro es no monótono en valor)
I-confluence (oráculo indep.)corre libre

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.

Por qué NO es circular (a diferencia de T5–T7)

  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.

Qué es novedad y qué no (honestidad §F)

Riesgo aceptado (R-T8b)

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.

Veredicto final del proyecto