hifas/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:

• rebalance_to(r, deficit) sobre un grafo donde r no alcanza ningún excedente debe fallar explícito (RebalanceResult::Unreachable), no bloquear indefinido.
• Ante Unreachable, la operación de gasto falla-seguro: se rechaza el retiro de 60, la réplica gasta a lo sumo su presupuesto local (50). Nunca sobregira, nunca cuelga.
• Honestidad de disponibilidad (nueva, explícita). Esto es el costo real del escrow, que hay que nombrar: bajo partición, una réplica está limitada a su presupuesto local. El escrow cambia el falso-verde del detector por un límite de disponibilidad real y seguro. No es un bug; es el precio correcto. diffuse (ruteo proactivo) lo mitiga repartiendo mejor antes de que llegue la partición, pero no lo elimina — ningún mecanismo seguro puede.

---

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

• Esto no es novedad: transferencia segura de derechos es el núcleo de Bounded Counter (Balegas 2015), y la representación monótona-con-procedencia es CRDT clásico (Shapiro 2011). Lo estás implementando correctamente, que es distinto de inventarlo. No lo reclames como aporte.
• El aporte defendible sigue siendo el de T9 §C: ruteo/localización por el grafo real (diffuse, rebalance_to con flujo mínimo edge-local). T10 le da la base segura sin la cual ese ruteo no significa nada.
• La honestidad de disponibilidad (§D) es parte del resultado, no una nota al pie: un consejero de coordinación soberano debe decir "bajo esta partición, este nodo puede gastar hasta X y no más", no fingir disponibilidad ilimitada. Esa franqueza es más valiosa que un número inflado.

---

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

• V. Balegas et al. — Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants, IEEE SRDS 2015. (Transferencia de derechos pairwise-asíncrona segura: el modelo de C.1.)
• P. E. O'Neil — The Escrow Transactional Method, ACM TODS 11(4), 1986.
• M. Shapiro et al. — A Comprehensive Study of Convergent and Commutative Replicated Data Types, 2011. (Base CRDT de la representación monótona-con-procedencia.)
• (De addenda previos) Bailis et al. 2014; Ghrist–Riess 2022; Hansen–Ghrist 2019; Hellerstein–Alvaro.