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 14TOML 1358 Definitions

⎇ 4f93b6e8711fdaea988b0f48b313ef442b28b232 STRONG_RESULT.md Markdown · 103 lines · 6.0 KB History raw

T10c: certificado dinámico (el teorema) — cierra T10 4f93b6e87 · Sergio ·

1# STRONG_RESULT — corregido por T9
2
3> **AVISO (T9 §G).** Este archivo reclamaba una "versión fuerte": que el haz
4> superaba a CALM vía I-confluence sensible a la instancia sobre el grafo real.
5> **Ese reclamo era falso** y está retirado. Lo que el testigo `[10,10]/[60,60]`
6> realmente probó, y el punto ciego que destapó, se documentan abajo. Un error
7> registrado con honestidad vale más que un resultado fuerte reclamado de más.
8
9## Qué se retira (el reclamo de T8, incorrecto)
10
11- ❌ "Versión fuerte probada / el haz es más fino que CALM."
12- ❌ "I-confluence sobre el grafo real como separación respecto a CALM."
13- ❌ "La topología importa: 60/60 particionado corre libre" **como virtud**.
14
15**Por qué era falso (T9 §A):**
16
171. **Detección, no evitación.** El veredicto `libre ⟺ punto_fijo ∈ V` funde dos
18   estados **ya divergidos** y comprueba el merge. Es detección reactiva
19   por-estado. Para un invariante duro llega tarde: si los retiros fueron
20   `[60,60]`, ya se aceptaron, y repararlos es compensación = coordinación.
212. **No hay separación respecto a I-confluence ni a CALM.** "Retirar con saldo ≥ 0"
22   no es I-confluente porque *existe* un `[60,60]` que rompe `I` → coordina,
23   categórico, igual que CALM (`I-confluente ⟺ monótono`, Prop. 3 de Complete
24   CALM). El testigo `[10,10]` no era una cuña más fina: respondía **otra**
25   pregunta (¿este estado concreto ya fusionado es válido?), no la de coordinación.
263. **El "60/60 particionado corre libre" era un BUG, no un refinamiento.** Un
27   invariante **global** codificado por aristas **pares** desaparece del haz al
28   particionar el grafo — justo cuando el acoplamiento sigue intacto. El detector
29   reporta "libre" el caso **más peligroso** porque está **ciego** a él. Ver
30   `COMPARISON.md`, fila 3, y el test `invariant::tests::t9_punto_ciego...`.
31
32## Qué probó de verdad el testigo (lo que sí queda)
33
34Un **detector de conflicto por-estado con localización**: dado un conjunto
35concreto de estados y un grafo, funde por componentes y señala si el merge viola
36el invariante y qué réplicas/aristas lo empujan fuera de `V`. Útil como **alarma
37de reconciliación**, no como consejero de coordinación. No es novedad frente a
38I-confluence; es I-confluence evaluada sobre un estado concreto, con el punto
39ciego de la codificación por aristas.
40
41## Dónde está la evitación real (T9)
42
43La coordinación se **evita** —no se detecta tarde— con **escrow** (O'Neil 1986;
44Bounded Counter, Balegas et al. SRDS 2015):
45
46- Reparto del slack `S` en presupuestos `b_i` con `Σ b_i ≤ S` (`escrow.rs`).
47- Gasto local sin coordinar mientras haya presupuesto — **correcto incluso
48  particionado**, que es justo donde el detector fallaba.
49- **Certificado por construcción:** `spent_i ≤ b_i ⟹ valor ≥ K`, para toda
50  ejecución, orden y partición (`escrow::tests::certificado_...`).
51- Única coordinación: rebalanceo **edge-local** ruteado por el Laplaciano sobre
52  el grafo real, conservando `Σ b` (`router.rs`).
53
54**Honestidad (T9 §B):** escrow **tampoco** vence a CALM. *Transforma* la
55operación —de "retirar sin límite" (no I-confluente → coordina) a "retirar dentro
56de presupuesto" (I-confluente → libre)— al costo de un rebalanceo ocasional. No se
57rompe el teorema; se re-ingeniería la operación para caer del lado bueno.
58
59## El candidato a novedad honesto (T9 §C, R-T9c)
60
61No es el sí/no (eso es I-confluence, Bailis 2014). Es el **ruteo y la
62localización del presupuesto por el grafo de comunicación real**: `diffuse`
63suaviza proactivamente y `rebalance_to` localiza el flujo mínimo, edge-local, que
64repone a una réplica seca. La misma máquina Laplaciana que en el MVP era un
65detector con falso-positivo (`H¹ = β₁`) reaparece aquí como **ruteador legítimo**.
66El reach —múltiples invariantes acoplados vía haces (que Balegas señala como no
67resuelto)— sería nuevo; se reclamará solo si se construye.
68
69## Veredicto del arco
70
71- MVP lineal: medía **topología** (`H¹ = β₁`); detector barato, falso-positivo.
72- T5–T7 (retículos/Tarski): parecía cerrar la brecha, pero era **circular**
73  (`FLIPS.md`).
74- T8: rederivó del merge y ancló en un invariante, pero confundió **detección con
75  evitación** y trató un invariante **global como edge-local** (punto ciego).
76- **T9: evitación real por escrow, con certificado, ruteada por el grafo.** Ahí
77  está la contribución defendible — y las fronteras (R-T9b: recurso divisible;
78  R-T9c: la novedad es el ruteo/localización, no el booleano).
79- **T10: la evitación es segura DINÁMICAMENTE**, no solo en snapshot (§H, §J).
80
81## T10 — certificado dinámico (M4 desbloqueado de verdad)
82
83El certificado de T9 valía para un reparto **congelado**, testeado
84secuencialmente. T10 cierra la grieta estático→dinámico:
85
86- **Transferencia sin carreras** (`EscrowState`, T10a): presupuesto con procedencia
87  (`granted[from][to]`, `spent[i]` monótonos; `avail` derivado). `Σ avail =
88  Σ b0 − Σ spent` es invariante a los `granted` ⟹ **imposible fabricar** por fusión
89  ni **perder** por crash (un `grant` vive entero en su celda).
90- **Fail-safe bajo partición** (`RebalanceResult::Unreachable`, T10b): sin ruta,
91  el gasto se rechaza y la réplica se limita a su presupuesto local; nunca
92  sobregira ni cuelga. El precio honesto está en `AVAILABILITY.md` (CAP: safety
93  sobre availability).
94- **El teorema** (`escrow::tests::certificado_dinamico`, T10c): entrelazando
95  gastos + `grant`s concurrentes + crashes + particiones en órdenes de fusión
96  arbitrarios, `valor = inicial − Σ spent ≥ K` **en todo momento** y `total_avail
97  ≥ 0` siempre. Subsume el certificado estático de T9.
98
99Solo con esta base —conservación bajo concurrencia, partición y crash— tiene
100sentido **M4**: cablear el escrow a una malla de gossip donde los rebalanceos
101corren de verdad. **M4 queda desbloqueado.** Honestidad (T10 §G): T10 no es
102novedad (Bounded Counter/CRDT clásico, Balegas 2015, bien implementado); el aporte
103defendible sigue siendo el ruteo/localización por el grafo real.

STRONG_RESULT.md

STRONG_RESULT — corregido por T9

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.

Qué se retira (el reclamo de T8, incorrecto)

Por qué era falso (T9 §A):

  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....

Qué probó de verdad el testigo (lo que sí queda)

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.

Dónde está la evitación real (T9)

La coordinación se evita —no se detecta tarde— con escrow (O'Neil 1986; Bounded Counter, Balegas et al. SRDS 2015):

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.

El candidato a novedad honesto (T9 §C, R-T9c)

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

T10 — certificado dinámico (M4 desbloqueado de verdad)

El certificado de T9 valía para un reparto congelado, testeado secuencialmente. T10 cierra la grieta estático→dinámico:

Solo con esta base —conservación bajo concurrencia, partición y crash— tiene sentido M4: cablear el escrow a una malla de gossip donde los rebalanceos corren de verdad. M4 queda desbloqueado. Honestidad (T10 §G): T10 no es novedad (Bounded Counter/CRDT clásico, Balegas 2015, bien implementado); el aporte defendible sigue siendo el ruteo/localización por el grafo real.