gioser

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.

⎇ 703ae7023578fabc109ef038063c7351fb3b9f52 T10.md Markdown · 204 siq'ikuna · 11.3 KB Ñawpa willay ch'uya

T10a: presupuesto con procedencia (transferencia CRDT) bd89fbb2d · Sergio ·

1# SDD — Addendum: T10 · Seguridad dinámica del rebalanceo
2
3**Extiende:** `DESIGN.md` + addenda T5–T7, T8, T9.
4**Estado:** Diseño — habilitado por la grieta estático/dinámico del certificado de T9.
5**Precondición:** T9 cerrado. `escrow.rs` (certificado estático) y `router.rs` (`rebalance_to`, `diffuse`)
6existen y pasan tests **secuenciales**.
7**Última edición:** 2026-07-01
8
9---
10
11## A. Qué deja abierto T9 (la grieta estático→dinámico)
12
13T9 probó el certificado para un reparto **congelado**: `Σ bᵢ ≤ S ⟹ valor ≥ K`. Correcto, pero estático.
14El sistema real no está congelado — el presupuesto **se mueve**: se gasta, se rebalancea, se replenishea.
15La conservación `Σ b` bajo `rebalance_to` se testeó **secuencialmente**. Falta lo difícil:
16
17> ¿`Σ b` se conserva cuando los rebalanceos ocurren **concurrentemente**, cuando una **partición** corta
18> una transferencia a la mitad, o cuando una réplica **crashea** sosteniendo presupuesto en tránsito?
19
20Si no, el certificado es de papel: en el instante en que `Σ b > S` (presupuesto fabricado por una carrera),
21`valor ≥ K` deja de estar garantizado y vuelve el sobregiro — el mismo fallo que T9 creía haber cerrado,
22por una puerta distinta.
23
24**Este es el 80% difícil del escrow.** El reparto estático era el 20% fácil. O'Neil (1986) y Balegas et al.
25(2015) gastan su esfuerzo exactamente aquí: en que la **transferencia de derechos** sea segura, no en el
26split. Bounded Counter lo logra con comunicación **pairwise asíncrona** donde las transferencias son
27seguras bajo concurrencia. T10 replica esa garantía y la verifica.
28
29---
30
31## B. El modo de fallo, concreto
32
33Presupuesto `[b_A=0, b_B=30, b_C=0]`. `A` y `C` piden prestado a `B` **a la vez**:
34
35```
36A lee b_B = 30, toma 20  →  quiere dejar b_B = 10
37C lee b_B = 30, toma 20  →  quiere dejar b_B = 10   (leyó el mismo 30)
38merge ingenuo (last-write / max / suma cruda):
39   b_B termina en 10, pero b_A = 20 y b_C = 20
40   Σ b = 10 + 20 + 20 = 50  >  30 original  →  20 de presupuesto FABRICADO
41```
42
43Con `Σ b` inflado, dos réplicas gastan derechos que no existen → `valor < K`. La transferencia leída-y-
44escrita sin cuidado **crea** presupuesto. El dual (perderlo) ocurre si un crash a mitad de transferencia
45deja el débito aplicado en `B` pero el crédito nunca llega a `A`: `Σ b` **baja**, seguro pero con
46disponibilidad estrangulada y presupuesto **stranded**.
47
48---
49
50## C. La cura: transferencia como operación segura (no leída-y-escrita)
51
52La transferencia de presupuesto debe ser **conmutativa y sin fabricación**, igual que el resto del sistema
53es coordination-free. Dos rutas, elige según cuánto quieras acoplar a lo ya hecho:
54
55**C.1 — Presupuesto como par de contadores monótonos (estilo Bounded Counter).**
56En vez de un `b_i` mutable, modela el presupuesto de cada réplica como derechos con **origen**: una matriz
57`granted[from][to]` de derechos transferidos, monótona creciente (solo se añade), más `spent[i]` monótono.
58El presupuesto disponible de `i` es una *función derivada*:
59`avail_i = b0_i + Σ_j granted[j][i] − Σ_j granted[i][j] − spent_i`.
60Como `granted` y `spent` solo crecen y se fusionan por `max`/unión (CRDT), **no hay carrera**: dos
61transferencias concurrentes se suman sin pisarse, y `Σ avail` es invariante por construcción porque cada
62`granted[j][i]` aparece con `+` en `i` y `−` en `j`. Esta es la vía Balegas y la recomendada.
63
64**C.2 — Transferencia como two-phase con reserva (si C.1 es mucho refactor).**
65`B` **reserva** 20 (los descuenta de su `avail` localmente y los marca en tránsito con un id único) antes
66de que `A` los reclame. La reserva es idempotente por id; un crash deja los 20 reservados-no-reclamados,
67recuperables por timeout hacia `B` (nunca hacia ambos). Más frágil que C.1 (necesita timeouts y
68reclamación), pero no reescribe el modelo de datos. Úsala solo si C.1 no cabe en el sprint.
69
70**En ambas: `Σ avail` (o `Σ b`) es invariante bajo cualquier entrelazado.** Ese es el teorema de T10,
71y sube el certificado de T9 de estático a dinámico.
72
73---
74
75## D. El caso sin ruta: fail-safe, no hang (la fila 3 de `COMPARISON.md`)
76
77`try_spend` devuelve `NeedsRebalance{deficit}` correctamente, pero T9 no define el eslabón siguiente cuando
78**no hay ruta** al presupuesto (partición). Reglas:
79
80- `rebalance_to(r, deficit)` sobre un grafo donde `r` no alcanza ningún excedente **debe fallar explícito**
81  (`RebalanceResult::Unreachable`), no bloquear indefinido.
82- Ante `Unreachable`, la operación de gasto **falla-seguro**: se rechaza el retiro de 60, la réplica gasta
83  a lo sumo su presupuesto local (50). Nunca sobregira, nunca cuelga.
84- **Honestidad de disponibilidad (nueva, explícita).** Esto es el costo real del escrow, que hay que
85  nombrar: bajo partición, una réplica está limitada a su presupuesto local. El escrow cambia el
86  falso-verde del detector por un **límite de disponibilidad real y seguro**. No es un bug; es el precio
87  correcto. `diffuse` (ruteo proactivo) lo *mitiga* repartiendo mejor antes de que llegue la partición,
88  pero no lo elimina — ningún mecanismo seguro puede.
89
90---
91
92## E. Modelo de tipos (bocetos, vía C.1)
93
94```rust
95/// Presupuesto con procedencia: todo es monótono creciente ⟹ fusión sin carreras.
96pub struct EscrowState {
97    pub b0: Vec<i64>,                 // reparto inicial (constante)
98    pub granted: Vec<Vec<i64>>,       // granted[from][to], solo crece
99    pub spent: Vec<i64>,              // spent[i], solo crece
100}
101impl EscrowState {
102    pub fn avail(&self, i: usize) -> i64 {
103        self.b0[i]
104          + self.granted.iter().map(|row| row[i]).sum::<i64>()   // recibido
105          - self.granted[i].iter().sum::<i64>()                  // cedido
106          - self.spent[i]
107    }
108    /// Σ avail es invariante: cada granted[j][i] entra +en i, −en j. Solo b0 y −spent lo mueven.
109    pub fn total_avail(&self) -> i64 { /* Σ b0 − Σ spent */ }
110
111    /// Fusión CRDT: max componente a componente en granted y spent. Conmutativa, idempotente.
112    pub fn merge(&mut self, other: &EscrowState) { /* ... */ }
113}
114
115pub enum RebalanceResult {
116    Routed { edges: Vec<(usize, usize, i64)> }, // flujo edge-local que repuso a r
117    Unreachable,                                 // sin ruta (partición): fail-safe arriba
118}
119```
120
121`granted`/`spent` monótonos + `merge` por `max` = las transferencias son un CRDT. Dos `grant` concurrentes
122de `B` a `A` y a `C` se fusionan sumándose, y `total_avail` no puede subir por fusión: **imposible fabricar
123presupuesto**. El crash es seguro: un `grant` a medio propagar, al re-fusionar, o llegó (crédito y débito
124juntos, porque ambos viven en `granted[B][A]`) o no llegó — nunca medio.
125
126---
127
128## F. Tests (el corazón de T10)
129
130Estáticos ya no bastan; T10 es sobre entrelazados.
131
1321. **Conservación bajo concurrencia.** `proptest`: genera N transferencias concurrentes (órdenes de fusión
133   aleatorios) sobre un `EscrowState`; tras fusionar en cualquier orden, `total_avail` == `Σ b0 − Σ spent`.
134   Nunca sube. (Mata el modo de fallo de §B.)
1352. **Idempotencia y conmutatividad de `merge`.** `merge` en cualquier orden y con repeticiones da el mismo
136   estado. (Es la condición CRDT.)
1373. **Crash a mitad de transferencia.** Aplica un `grant` en una réplica, no lo propagues, fusiona el resto,
138   luego propágalo tarde: `total_avail` idéntico; ningún presupuesto fabricado ni perdido.
1394. **Partición sin ruta → fail-safe.** El 60/60 particionado con `b=[50,50]`: `rebalance_to` da
140   `Unreachable`, el gasto de 60 se rechaza, la réplica gasta ≤ 50, `valor ≥ 0` se mantiene. Nunca cuelga.
1415. **Certificado dinámico (el teorema).** `proptest` que entrelaza gastos **y** rebalanceos **y**
142   particiones arbitrarias: en todo momento `valor = inicial − Σ spent ≥ K`. Este subsume el certificado
143   estático de T9 y es la meta de T10.
1446. **No-regresión de disponibilidad honesta.** Documenta (no solo aserta) en `AVAILABILITY.md` el límite:
145   qué retiros bloquean bajo qué particiones, y cuánto los alivia `diffuse`. Sin promesas de liveness que
146   no puedas sostener.
147
148---
149
150## G. Honestidad de T10
151
152- Esto **no** es novedad: transferencia segura de derechos es el núcleo de Bounded Counter (Balegas 2015),
153  y la representación monótona-con-procedencia es CRDT clásico (Shapiro 2011). Lo estás **implementando
154  correctamente**, que es distinto de inventarlo. No lo reclames como aporte.
155- El aporte defendible sigue siendo el de T9 §C: **ruteo/localización por el grafo real** (`diffuse`,
156  `rebalance_to` con flujo mínimo edge-local). T10 le da la base segura sin la cual ese ruteo no significa
157  nada.
158- La honestidad de disponibilidad (§D) es parte del resultado, no una nota al pie: un consejero de
159  coordinación soberano debe decir "bajo esta partición, este nodo puede gastar hasta X y no más", no
160  fingir disponibilidad ilimitada. Esa franqueza es más valiosa que un número inflado.
161
162---
163
164## H. Después de T10: M4 desbloqueado de verdad
165
166Solo con el certificado **dinámico** (F.5) tiene sentido M4. Cablear a Tawasuyu/Hammer un escrow cuya
167conservación solo vale para snapshots congelados sería meter una garantía de papel en una malla de gossip
168donde los rebalanceos **corren de verdad** — el mismo error de "verde estático" que T10 existe para cerrar.
169Con T10 cerrado, M4 congela la API de `verdict`/`escrow` y escribe el adaptador con una base que aguanta
170concurrencia, partición y crash.
171
172---
173
174## I. Tickets
175
176**T10a — Presupuesto con procedencia (transferencia CRDT).**
177"Refactoriza `escrow.rs` a `EscrowState` según §E (vía C.1): `b0` constante, `granted[from][to]` y
178`spent[i]` monótonos, `avail`/`total_avail` derivados, `merge` por max. Sustituye el `b_i` mutable de T9.
179Tests: `merge` conmutativa/idempotente (§F.2); `total_avail` invariante bajo fusión (§F.1). Si C.1 resulta
180inviable, cae a C.2 (two-phase con reserva por id) y dilo en un comentario."
181
182**T10b — Rebalanceo sin ruta + fail-safe.**
183"En `router.rs`, `rebalance_to` devuelve `RebalanceResult::Unreachable` cuando `r` no alcanza excedente en
184el grafo actual (partición), en vez de bloquear. Conecta el veredicto de gasto: ante `Unreachable`, el
185retiro se rechaza y la réplica gasta ≤ su `avail`. Tests §F.4. Escribe `AVAILABILITY.md` (§F.6): el límite
186de disponibilidad bajo partición y cuánto lo alivia `diffuse`, sin prometer liveness."
187
188**T10c — Certificado dinámico (el teorema).**
189"Escribe el `proptest` de §F.5: entrelaza gastos, rebalanceos (`grant`s concurrentes) y particiones
190arbitrarias en órdenes de fusión aleatorios, y verifica `valor = inicial − Σ spent ≥ K` en todo momento,
191más `total_avail` nunca por encima de `Σ b0 − Σ spent`. Incluye el caso de crash a mitad de transferencia
192(§F.3). Este test subsume el certificado estático de T9. Cuando pase, marca en `STRONG_RESULT.md` que la
193evitación de escrow es segura **dinámicamente**, no solo en snapshot, y declara M4 desbloqueado."
194
195---
196
197## J. Referencias
198
199- V. Balegas et al. — *Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants*,
200  IEEE SRDS 2015. (Transferencia de derechos pairwise-asíncrona segura: el modelo de C.1.)
201- P. E. O'Neil — *The Escrow Transactional Method*, ACM TODS 11(4), 1986.
202- M. Shapiro et al. — *A Comprehensive Study of Convergent and Commutative Replicated Data Types*, 2011.
203  (Base CRDT de la representación monótona-con-procedencia.)
204- (De addenda previos) Bailis et al. 2014; Ghrist–Riess 2022; Hansen–Ghrist 2019; Hellerstein–Alvaro.

T10.md

SDD — Addendum: T10 · Seguridad dinámica del rebalanceo

Extiende: DESIGN.md + addenda T5–T7, T8, T9. Estado: Diseño — habilitado por la grieta estático/dinámico del certificado de T9. Precondición: T9 cerrado. escrow.rs (certificado estático) y router.rs (rebalance_to, diffuse) existen y pasan tests secuenciales. Última edición: 2026-07-01


A. Qué deja abierto T9 (la grieta estático→dinámico)

T9 probó el certificado para un reparto congelado: Σ bᵢ ≤ S ⟹ valor ≥ K. Correcto, pero estático. El sistema real no está congelado — el presupuesto se mueve: se gasta, se rebalancea, se replenishea. La conservación Σ b bajo rebalance_to se testeó secuencialmente. Falta lo difícil:

¿Σ b se conserva cuando los rebalanceos ocurren concurrentemente, cuando una partición corta una transferencia a la mitad, o cuando una réplica crashea sosteniendo presupuesto en tránsito?

Si no, el certificado es de papel: en el instante en que Σ b > S (presupuesto fabricado por una carrera), valor ≥ K deja de estar garantizado y vuelve el sobregiro — el mismo fallo que T9 creía haber cerrado, por una puerta distinta.

Este es el 80% difícil del escrow. El reparto estático era el 20% fácil. O'Neil (1986) y Balegas et al. (2015) gastan su esfuerzo exactamente aquí: en que la transferencia de derechos sea segura, no en el split. Bounded Counter lo logra con comunicación pairwise asíncrona donde las transferencias son seguras bajo concurrencia. T10 replica esa garantía y la verifica.


B. El modo de fallo, concreto

Presupuesto [b_A=0, b_B=30, b_C=0]. A y C piden prestado a B a la vez:

A lee b_B = 30, toma 20  →  quiere dejar b_B = 10
C lee b_B = 30, toma 20  →  quiere dejar b_B = 10   (leyó el mismo 30)
merge ingenuo (last-write / max / suma cruda):
   b_B termina en 10, pero b_A = 20 y b_C = 20
   Σ b = 10 + 20 + 20 = 50  >  30 original  →  20 de presupuesto FABRICADO

Con Σ b inflado, dos réplicas gastan derechos que no existen → valor < K. La transferencia leída-y- escrita sin cuidado crea presupuesto. El dual (perderlo) ocurre si un crash a mitad de transferencia deja el débito aplicado en B pero el crédito nunca llega a A: Σ b baja, seguro pero con disponibilidad estrangulada y presupuesto stranded.


C. La cura: transferencia como operación segura (no leída-y-escrita)

La transferencia de presupuesto debe ser conmutativa y sin fabricación, igual que el resto del sistema es coordination-free. Dos rutas, elige según cuánto quieras acoplar a lo ya hecho:

C.1 — Presupuesto como par de contadores monótonos (estilo Bounded Counter). En vez de un b_i mutable, modela el presupuesto de cada réplica como derechos con origen: una matriz granted[from][to] de derechos transferidos, monótona creciente (solo se añade), más spent[i] monótono. El presupuesto disponible de i es una función derivada: avail_i = b0_i + Σ_j granted[j][i] − Σ_j granted[i][j] − spent_i. Como granted y spent solo crecen y se fusionan por max/unión (CRDT), no hay carrera: dos transferencias concurrentes se suman sin pisarse, y Σ avail es invariante por construcción porque cada granted[j][i] aparece con + en i y − en j. Esta es la vía Balegas y la recomendada.

C.2 — Transferencia como two-phase con reserva (si C.1 es mucho refactor). B reserva 20 (los descuenta de su avail localmente y los marca en tránsito con un id único) antes de que A los reclame. La reserva es idempotente por id; un crash deja los 20 reservados-no-reclamados, recuperables por timeout hacia B (nunca hacia ambos). Más frágil que C.1 (necesita timeouts y reclamación), pero no reescribe el modelo de datos. Úsala solo si C.1 no cabe en el sprint.

En ambas: Σ avail (o Σ b) es invariante bajo cualquier entrelazado. Ese es el teorema de T10, y sube el certificado de T9 de estático a dinámico.


D. El caso sin ruta: fail-safe, no hang (la fila 3 de COMPARISON.md)

try_spend devuelve NeedsRebalance{deficit} correctamente, pero T9 no define el eslabón siguiente cuando no hay ruta al presupuesto (partición). Reglas:


E. Modelo de tipos (bocetos, vía C.1)

/// Presupuesto con procedencia: todo es monótono creciente ⟹ fusión sin carreras.
pub struct EscrowState {
    pub b0: Vec<i64>,                 // reparto inicial (constante)
    pub granted: Vec<Vec<i64>>,       // granted[from][to], solo crece
    pub spent: Vec<i64>,              // spent[i], solo crece
}
impl EscrowState {
    pub fn avail(&self, i: usize) -> i64 {
        self.b0[i]
          + self.granted.iter().map(|row| row[i]).sum::<i64>()   // recibido
          - self.granted[i].iter().sum::<i64>()                  // cedido
          - self.spent[i]
    }
    /// Σ avail es invariante: cada granted[j][i] entra +en i, −en j. Solo b0 y −spent lo mueven.
    pub fn total_avail(&self) -> i64 { /* Σ b0 − Σ spent */ }

    /// Fusión CRDT: max componente a componente en granted y spent. Conmutativa, idempotente.
    pub fn merge(&mut self, other: &EscrowState) { /* ... */ }
}

pub enum RebalanceResult {
    Routed { edges: Vec<(usize, usize, i64)> }, // flujo edge-local que repuso a r
    Unreachable,                                 // sin ruta (partición): fail-safe arriba
}

granted/spent monótonos + merge por max = las transferencias son un CRDT. Dos grant concurrentes de B a A y a C se fusionan sumándose, y total_avail no puede subir por fusión: imposible fabricar presupuesto. El crash es seguro: un grant a medio propagar, al re-fusionar, o llegó (crédito y débito juntos, porque ambos viven en granted[B][A]) o no llegó — nunca medio.


F. Tests (el corazón de T10)

Estáticos ya no bastan; T10 es sobre entrelazados.

  1. Conservación bajo concurrencia. proptest: genera N transferencias concurrentes (órdenes de fusión aleatorios) sobre un EscrowState; tras fusionar en cualquier orden, total_avail == Σ b0 − Σ spent. Nunca sube. (Mata el modo de fallo de §B.)
  2. Idempotencia y conmutatividad de merge. merge en cualquier orden y con repeticiones da el mismo estado. (Es la condición CRDT.)
  3. Crash a mitad de transferencia. Aplica un grant en una réplica, no lo propagues, fusiona el resto, luego propágalo tarde: total_avail idéntico; ningún presupuesto fabricado ni perdido.
  4. Partición sin ruta → fail-safe. El 60/60 particionado con b=[50,50]: rebalance_to da Unreachable, el gasto de 60 se rechaza, la réplica gasta ≤ 50, valor ≥ 0 se mantiene. Nunca cuelga.
  5. Certificado dinámico (el teorema). proptest que entrelaza gastos y rebalanceos y particiones arbitrarias: en todo momento valor = inicial − Σ spent ≥ K. Este subsume el certificado estático de T9 y es la meta de T10.
  6. No-regresión de disponibilidad honesta. Documenta (no solo aserta) en AVAILABILITY.md el límite: qué retiros bloquean bajo qué particiones, y cuánto los alivia diffuse. Sin promesas de liveness que no puedas sostener.

G. Honestidad de T10


H. Después de T10: M4 desbloqueado de verdad

Solo con el certificado dinámico (F.5) tiene sentido M4. Cablear a Tawasuyu/Hammer un escrow cuya conservación solo vale para snapshots congelados sería meter una garantía de papel en una malla de gossip donde los rebalanceos corren de verdad — el mismo error de "verde estático" que T10 existe para cerrar. Con T10 cerrado, M4 congela la API de verdict/escrow y escribe el adaptador con una base que aguanta concurrencia, partición y crash.


I. Tickets

T10a — Presupuesto con procedencia (transferencia CRDT). "Refactoriza escrow.rs a EscrowState según §E (vía C.1): b0 constante, granted[from][to] y spent[i] monótonos, avail/total_avail derivados, merge por max. Sustituye el b_i mutable de T9. Tests: merge conmutativa/idempotente (§F.2); total_avail invariante bajo fusión (§F.1). Si C.1 resulta inviable, cae a C.2 (two-phase con reserva por id) y dilo en un comentario."

T10b — Rebalanceo sin ruta + fail-safe. "En router.rs, rebalance_to devuelve RebalanceResult::Unreachable cuando r no alcanza excedente en el grafo actual (partición), en vez de bloquear. Conecta el veredicto de gasto: ante Unreachable, el retiro se rechaza y la réplica gasta ≤ su avail. Tests §F.4. Escribe AVAILABILITY.md (§F.6): el límite de disponibilidad bajo partición y cuánto lo alivia diffuse, sin prometer liveness."

T10c — Certificado dinámico (el teorema). "Escribe el proptest de §F.5: entrelaza gastos, rebalanceos (grants concurrentes) y particiones arbitrarias en órdenes de fusión aleatorios, y verifica valor = inicial − Σ spent ≥ K en todo momento, más total_avail nunca por encima de Σ b0 − Σ spent. Incluye el caso de crash a mitad de transferencia (§F.3). Este test subsume el certificado estático de T9. Cuando pase, marca en STRONG_RESULT.md que la evitación de escrow es segura dinámicamente, no solo en snapshot, y declara M4 desbloqueado."


J. Referencias