tawasuyu/hifas
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

T10a: presupuesto con procedencia (transferencia CRDT)

Browse Source 
T10 §C.1 (vía Balegas): sube el certificado de estático a con-base-dinámica.
El Budget mutable de T9 (b_i leído-y-escrito) era seguro solo en snapshots
secuenciales; una transferencia concurrente podía FABRICAR presupuesto (§B).

- escrow::EscrowState { b0 constante, granted[from][to] monótono, spent[i]
  monótono }. avail derivado; grant/spend guardados por avail local
  (single-writer por fila ⟹ sin conflicto); merge por max (CRDT).
- Teorema §C: Σ avail = Σ b0 − Σ spent, invariante a los granted (se cancelan:
  +en i, −en j). Imposible fabricar por fusión; imposible perder por crash
  (un grant vive entero en granted[from][to]).

Tests: el modo de fallo §B prevenido en el origen (segundo grant de 20 falla);
crash a mitad de transferencia seguro; proptest total_avail_es_invariante
(Σ avail == Σb0−Σspent siempre); merge conmutativo/idempotente; merge nunca
sube el total. Budget de T9 se conserva (router migra en T10b).

59 tests, clippy limpio.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Sergio
2026-07-01 21:04:11 +00:00
co-authored by Claude Opus 4.8
parent 6eff6f1c31
commit bd89fbb2d1
2 changed files with 390 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
T10.md
+204
View File
@@ -0,0 +1,204 @@
# 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)
```rust
/// 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 (`grant`s 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.
src/escrow.rs
+186
View File
@@ -92,6 +92,104 @@ impl Budget {
}
}
/// **Presupuesto con procedencia** (T10, §C.1 — la vía Balegas): todo es monótono
/// creciente, así que la fusión es un CRDT y **no hay carreras**. Sustituye al
/// `Budget` mutable de T9 (`b_i` leído-y-escrito), que era seguro solo en
/// snapshots congelados y secuenciales.
///
/// El presupuesto disponible es una **función derivada** de dos historiales que
/// solo crecen: `granted[from][to]` (derechos cedidos) y `spent[i]` (gasto).
///
/// **El teorema (§C):** `Σ avail = Σ b0 − Σ spent`, invariante bajo cualquier
/// entrelazado, porque cada `granted[j][i]` entra `+` en `i` y `−` en `j` y se
/// cancela. Imposible fabricar presupuesto por fusión; imposible perderlo por un
/// crash a medio propagar (un `grant` vive entero en `granted[from][to]`: al
/// re-fusionar, o llegó completo o no llegó).
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct EscrowState {
/// Reparto inicial (constante); `Σ b0 ≤ slack`.
pub b0: Vec<i64>,
/// `granted[from][to]`: derechos transferidos, solo crece. Fila `from`
/// escrita solo por la réplica `from` (single-writer ⟹ sin conflicto).
pub granted: Vec<Vec<i64>>,
/// `spent[i]`: gasto de la réplica `i`, solo crece.
pub spent: Vec<i64>,
}
impl EscrowState {
/// Estado inicial a partir de un reparto `b0` (sin transferencias ni gasto).
pub fn new(b0: Vec<i64>) -> Self {
let n = b0.len();
Self {
b0,
granted: vec![vec![0; n]; n],
spent: vec![0; n],
}
}
/// Número de réplicas.
pub fn replicas(&self) -> usize {
self.b0.len()
}
/// Presupuesto disponible de `i` = inicial + recibido − cedido − gastado.
pub fn avail(&self, i: usize) -> i64 {
let recibido: i64 = (0..self.replicas()).map(|j| self.granted[j][i]).sum();
let cedido: i64 = self.granted[i].iter().sum();
self.b0[i] + recibido - cedido - self.spent[i]
}
/// Presupuesto total disponible. Por el teorema de §C es exactamente
/// `Σ b0 − Σ spent` — los `granted` se cancelan y **no cambian el total**.
pub fn total_avail(&self) -> i64 {
self.b0.iter().sum::<i64>() - self.spent.iter().sum::<i64>()
}
/// La otra vía de calcular el total (sumando cada `avail`), que DEBE coincidir
/// con `total_avail`: la prueba de la cancelación de `granted`.
pub fn sum_avail(&self) -> i64 {
(0..self.replicas()).map(|i| self.avail(i)).sum()
}
/// La réplica `from` cede `amount` (≥0) a `to`. Guardado por su `avail` local
/// (single-writer): nunca cede más de lo que tiene ⟹ imposible fabricar en el
/// origen. Devuelve `false` si no le alcanza.
pub fn grant(&mut self, from: usize, to: usize, amount: i64) -> bool {
debug_assert!(amount >= 0);
if amount <= self.avail(from) {
self.granted[from][to] += amount;
true
} else {
false
}
}
/// La réplica `i` gasta `amount` (≥0) si le queda `avail`. Monótono.
pub fn spend(&mut self, i: usize, amount: i64) -> bool {
debug_assert!(amount >= 0);
if amount <= self.avail(i) {
self.spent[i] += amount;
true
} else {
false
}
}
/// **Fusión CRDT**: máximo componente a componente en `granted` y `spent`
/// (los historiales solo crecen). Conmutativa, asociativa, idempotente. No
/// puede subir `total_avail`: `Σ spent` solo crece ⟹ el total solo baja.
pub fn merge(&mut self, other: &EscrowState) {
debug_assert_eq!(self.b0, other.b0, "mismo reparto inicial");
let n = self.replicas();
for i in 0..n {
self.spent[i] = self.spent[i].max(other.spent[i]);
for j in 0..n {
self.granted[i][j] = self.granted[i][j].max(other.granted[i][j]);
}
}
}
}
#[cfg(test)]
mod tests {
use super::*;
@@ -162,4 +260,92 @@ mod tests {
prop_assert!(inv.holds(valor), "valor {} < piso {}", valor, inv.floor);
}
}
// ---- T10a: presupuesto con procedencia (EscrowState) ----
/// **El modo de fallo de §B, PREVENIDO en el origen.** `B` tiene 30. Cede 20 a
/// `A`; el segundo intento de ceder 20 a `C` **falla** (solo le quedan 10),
/// porque `grant` está guardado por el `avail` local. Nada de fabricar 20 por
/// una lectura-y-escritura descuidada. `Σ avail` se conserva en 30.
#[test]
fn grant_guardado_previene_la_fabricacion() {
let mut s = EscrowState::new(vec![0, 30, 0]);
assert!(s.grant(1, 0, 20), "B cede 20 a A");
assert!(!s.grant(1, 2, 20), "B ya no puede ceder otros 20 (solo le quedan 10)");
assert!(s.grant(1, 2, 10), "pero sí los 10 restantes");
assert_eq!(s.avail(0), 20);
assert_eq!(s.avail(1), 0);
assert_eq!(s.avail(2), 10);
assert_eq!(s.total_avail(), 30, "Σ avail conservado: cero fabricación");
}
/// Crash a mitad de transferencia: un `grant` aplicado en una copia y no
/// propagado, al re-fusionar tarde da el mismo estado. Ni fabrica ni pierde.
#[test]
fn crash_a_mitad_de_transferencia_es_seguro() {
let base = EscrowState::new(vec![30, 0]);
// Copia 1: B0 concede 20 a la réplica 1 (el "grant en tránsito").
let mut c1 = base.clone();
assert!(c1.grant(0, 1, 20));
// Copia 2 (crashea sin ver el grant): fusiona el resto tal cual.
let mut c2 = base.clone();
c2.merge(&base);
// El grant llega tarde: c2 re-fusiona con c1.
c2.merge(&c1);
assert_eq!(c2, c1, "el grant llega entero o no llega; nunca a medias");
assert_eq!(c2.total_avail(), 30);
}
fn escrow_st() -> impl Strategy<Value = EscrowState> {
(1usize..=4).prop_flat_map(|n| {
let b0 = prop::collection::vec(0i64..50, n);
let granted = prop::collection::vec(prop::collection::vec(0i64..30, n), n);
let spent = prop::collection::vec(0i64..30, n);
(b0, granted, spent).prop_map(|(b0, granted, spent)| EscrowState { b0, granted, spent })
})
}
/// Dos estados con el mismo reparto inicial (para poder fusionarlos).
fn par_de_escrow() -> impl Strategy<Value = (EscrowState, EscrowState)> {
escrow_st().prop_flat_map(|a| {
let n = a.replicas();
let granted = prop::collection::vec(prop::collection::vec(0i64..30, n), n);
let spent = prop::collection::vec(0i64..30, n);
let b0 = a.b0.clone();
(Just(a), (granted, spent)).prop_map(move |(a, (g, s))| {
let b = EscrowState { b0: b0.clone(), granted: g, spent: s };
(a, b)
})
})
}
proptest! {
/// **§F.1 — el total no se puede fabricar.** `Σ avail` (sumando cada réplica)
/// SIEMPRE es igual a `Σ b0 − Σ spent`: los `granted` se cancelan, pase lo
/// que pase con las transferencias. Este es el teorema que mata el §B.
#[test]
fn total_avail_es_invariante_a_los_granted(s in escrow_st()) {
prop_assert_eq!(s.sum_avail(), s.total_avail());
prop_assert_eq!(s.total_avail(), s.b0.iter().sum::<i64>() - s.spent.iter().sum::<i64>());
}
/// **§F.2 — `merge` es un CRDT:** conmutativo e idempotente.
#[test]
fn merge_conmutativo_e_idempotente((a, b) in par_de_escrow()) {
let mut ab = a.clone(); ab.merge(&b);
let mut ba = b.clone(); ba.merge(&a);
prop_assert_eq!(&ab, &ba, "merge conmutativo");
let mut abb = ab.clone(); abb.merge(&b);
prop_assert_eq!(&abb, &ab, "merge idempotente");
}
/// **§F.1 (fusión) — `merge` nunca sube el total.** `Σ spent` solo crece por
/// max ⟹ `total_avail` solo puede bajar. Imposible fabricar por fusión.
#[test]
fn merge_nunca_fabrica_presupuesto((a, b) in par_de_escrow()) {
let mut m = a.clone(); m.merge(&b);
prop_assert!(m.total_avail() <= a.total_avail());
prop_assert!(m.total_avail() <= b.total_avail());
}
}
}