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.

⎇ main STRONG_RESULT.md Markdown · 142 lines · 8.1 KB History raw

T11c: fencing por época + detección de clon (frontera §D) — cierra T11 a8a39a67f · 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. Honestidad (T10 §G): T10 no es novedad (Bounded Counter/CRDT
102clásico, Balegas 2015, bien implementado); el aporte defendible sigue siendo el
103ruteo/localización por el grafo real.
104
105## T11 — el terminus honesto (el supuesto físico nombrado)
106
107El teorema de T10 daba gratis un supuesto: `spent_i` **durable y monótono en la
108fuente**. T11 lo nombra y lo defiende, respetando CAP:
109
110- **F1 · Durabilidad** (`durable.rs`): un gasto se ackea solo tras persistir en el
111  WAL; `recover` restaura `spent ≥ último ack`; un rollback por debajo del WAL se
112  rechaza. `spent` no puede olvidar.
113- **F2 · Réplica-por-dispositivo** (`escrow::Identity`): la identidad es un
114  **conjunto de celdas-dispositivo**, cada una single-writer. Dos dispositivos
115  gastan sin serializar, sin fencing. F2 es un no-problema por diseño.
116- **Frontera · Clon** (`fencing.rs`, `BOUNDARY.md`): una celda con dos escritores
117  vivos que no se comunican es **imposible** de resolver coordination-free (CAP
118  dentro de la celda). El fencing por época **acota** el daño a una celda y lo
119  **detecta** al reconectar (`CloneDetected`) — *bounded + detect*, no *prevent*.
120
121**El enunciado correcto, que no promete de más:**
122
123> **Seguridad coordination-free módulo un supuesto físico nombrado:** cada celda de
124> presupuesto tiene un único escritor durable. Bajo él (§B durabilidad + §C
125> réplica-por-dispositivo) el certificado de T10 aplica sin coordinación. Roto el
126> supuesto (clon, §D), el daño está acotado a una celda por clon no detectado y se
127> detecta al reconectar — nunca silencioso ni ilimitado.
128
129## Contrato de M4 (listo para escribir en piedra)
130
131El adaptador a Tawasuyu/Hammer puede ahora declarar precondiciones honestas:
132
133- **Requiere** WAL durable de `spent` por dispositivo (persistir antes del ack).
134- **Requiere** identidad-como-conjunto-de-dispositivos (una celda por dispositivo).
135- **Garantiza** seguridad coordination-free del invariante bajo un-escritor-durable-
136  por-celda.
137- **Acota y detecta** (no previene) el doble gasto por clon; expone `CloneDetected`
138  para que la aplicación compense (`BOUNDARY.md`).
139- **Limita** la disponibilidad bajo partición al presupuesto local (`AVAILABILITY.md`).
140
141Si Tawasuyu/Hammer no pueden dar durabilidad por dispositivo, el adaptador **rehúsa**
142en vez de prometer seguridad que no tiene. Esa negativa es parte del diseño.

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

T11 — el terminus honesto (el supuesto físico nombrado)

El teorema de T10 daba gratis un supuesto: spent_i durable y monótono en la fuente. T11 lo nombra y lo defiende, respetando CAP:

El enunciado correcto, que no promete de más:

Seguridad coordination-free módulo un supuesto físico nombrado: cada celda de presupuesto tiene un único escritor durable. Bajo él (§B durabilidad + §C réplica-por-dispositivo) el certificado de T10 aplica sin coordinación. Roto el supuesto (clon, §D), el daño está acotado a una celda por clon no detectado y se detecta al reconectar — nunca silencioso ni ilimitado.

Contrato de M4 (listo para escribir en piedra)

El adaptador a Tawasuyu/Hammer puede ahora declarar precondiciones honestas:

Si Tawasuyu/Hammer no pueden dar durabilidad por dispositivo, el adaptador rehúsa en vez de prometer seguridad que no tiene. Esa negativa es parte del diseño.