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

T11a: réplica por dispositivo (cura de F2)

Browse Source 
T11 §C: el supuesto oculto de T10 (spent monótono-durable en la fuente) se
rompe con multi-writer. Cura F2: NO modelar la identidad como una réplica —
una identidad es un CONJUNTO de celdas-dispositivo, cada una réplica del
esquema de T10 con su b0[device] y spent[device].

- escrow::Identity { devices, inv }: total_avail/value/invariant_holds sobre
  las celdas de la identidad. La disciplina single-writer se cumple a nivel
  de celda-dispositivo, no de identidad.

Tests §G.2: dos dispositivos gastan concurrentemente sin pisarse (el gasto de
uno no toca el avail del otro; cada celda un único escritor); rebalanceo entre
dispositivos = grant, conserva total_avail; identidades disjuntas aisladas.

F2 es un no-problema por diseño, coordination-free, sin fencing (eso es solo
la frontera del clon, §D/T11c). 65 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:40:30 +00:00
co-authored by Claude Opus 4.8
parent 4f93b6e871
commit b4bd2e19b4
2 changed files with 302 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
T11.md
+207
View File
@@ -0,0 +1,207 @@
# SDD — Addendum: T11 · Monotonía en la fuente (el supuesto que T10 daba gratis)
**Extiende:** `DESIGN.md` + addenda T5–T7, T8, T9, T10.
**Estado:** Diseño — habilitado por un "no rotundo" a la pregunta de T10:
Tawasuyu/Hammer **no** garantizan réplicas single-writer con estado durable.
**Precondición:** T10 cerrado (`certificado_dinamico` verde bajo el supuesto de fuente monótona-durable).
**Última edición:** 2026-07-01
---
## A. El supuesto oculto de T10, ahora explícito
El teorema de T10 (`total_avail` invariante ⟹ `valor ≥ K`) asume silenciosamente que cada `spent_i` es
**durable y monótono en la fuente**: un escritor nunca olvida ni retrocede lo que ya cometió, y no hay dos
escritores concurrentes sobre la misma celda. La fusión CRDT converge *dado* que cada fuente solo crece.
Si la fuente misma retrocede o se bifurca, la premisa se viola **antes** de fusionar, y el certificado no
aplica.
El "no rotundo" rompe justo eso, por dos vías distintas + una frontera:
| Fallo | Qué pasa | Cura | ¿Coordination-free? |
|---|---|---|---|
| **F1 · Rollback** | un nodo vuelve de snapshot viejo, `spent_i` baja, re-gasta → doble gasto | durabilidad (WAL, persistir antes del ack) | **sí**, local |
| **F2 · Multi-writer** | dos dispositivos = "misma réplica", cada uno gasta su `avail` | réplica-por-dispositivo (identidad = conjunto de réplicas) | **sí**, sin fencing |
| **Frontera · Clon** | un dispositivo clonado a dos copias vivas, misma celda, sin comunicarse | fencing por época: acota + detecta al reconectar | **no del todo** (ver §D) |
Fencing NO es la cura de F1 ni de F2. Es solo la defensa acotada de la frontera del clon.
---
## B. F1 — Durabilidad: `spent` no puede olvidar (coordination-free)
**Contrato:** un gasto se reconoce al usuario (`ack`) **solo después** de que `spent_i` esté persistido
en almacenamiento durable (write-ahead log, fsync). Un crash puede perder gastos *no reconocidos* (nunca
prometidos a nadie), jamás uno reconocido.
Con esto, `spent_i` es monótono en la fuente por construcción: tras cualquier crash, al recuperar desde el
WAL, `spent_i` es ≥ el valor en el último ack. No retrocede por debajo de lo comprometido. Cero
coordinación — cada nodo fsyncea lo suyo.
**Lo que T11 debe verificar (con dientes):** el modelo de crash de T10 era el *benigno* (un `grant` sin
propagar). T11 mete el crash *malo*: una réplica que **revierte su propio `spent_i`** por debajo de un
valor ya reconocido. El test debe demostrar que la capa de durabilidad lo **impide** (la recuperación
restaura `spent_i` desde el WAL), o que se **detecta y rechaza** en el merge (§D). Un `spent_i` que
retrocede sin ser atrapado = certificado roto.
---
## C. F2 — Réplica por dispositivo: la identidad es un conjunto (coordination-free)
**No modeles la identidad como una réplica.** Un usuario/identidad es un **conjunto de réplicas-
dispositivo**, cada una con su propia celda de presupuesto `b0[device]` y su propio `spent[device]`.
Consecuencias:
- Dos dispositivos de una persona son dos réplicas del esquema de T10, sin cambios. Cada uno gasta su
presupuesto local sin serializar con el otro. No hay "dos escritores de la misma celda" → no hay carrera
→ no hace falta fencing para F2.
- Un dispositivo seco rebalancea desde otro dispositivo de la misma identidad: es el rebalanceo edge-local
de T10b, ya construido.
- Un dispositivo offline **estranca** su presupuesto (no lo puede gastar nadie más hasta que vuelva): es el
costo de disponibilidad honesto de `AVAILABILITY.md`, sin novedad.
Esto convierte F2 en un no-problema por diseño, sin coordinación. La disciplina "single-writer" de T10 se
cumple **a nivel de celda-dispositivo**, no a nivel de identidad.
---
## D. La frontera del clon (lo que NINGÚN sistema coordination-free puede cerrar)
F2 resuelve *dos dispositivos distintos*. Queda el caso duro: **una celda con dos escritores vivos** — un
dispositivo restaurado a dos copias (VM snapshot, proceso duplicado) que comparten `device_id` y celda, y
**no se comunican**. Cada clon puede gastar la celda entera → doble gasto de un presupuesto.
**Teorema de imposibilidad (hay que decirlo).** Ningún mecanismo local puede detectar un clon silencioso
antes de que los clones se comuniquen. Es el mismo CAP que el sobregiro particionado, ahora dentro de una
celda: sin comunicación, no hay forma de saber que el presupuesto ya se gastó en otra copia.
**Lo mejor posible — fencing por época device-local, enforced en el merge:**
- Cada instancia viva de un dispositivo tiene una **época** monótona, incrementada y persistida en cada
arranque (`epoch`, en el WAL de §B).
- Cada gasto lleva `(device_id, epoch, seq)`. `spent` se indexa por `(device_id, epoch)`.
- El **merge** es el punto de enforcement (no un servidor central, que no existe): al fusionar, si aparecen
dos linajes con el mismo `device_id` y épocas distintas, el de **época menor es un clon obsoleto** — sus
gastos post-bifurcación se **rechazan/aíslan** y se levanta una alarma (`CloneDetected`).
- Esto **no previene** el doble gasto mientras los clones están aislados; lo **acota** (a una celda por
clon no detectado) y lo **detecta** en cuanto reconectan. Convierte "silencioso e ilimitado" en "acotado
y delatado".
**Honestidad (no repetir el sobre-reclamo).** El fencing token clásico (Kleppmann) asume un recurso
linealizable que rechaza tokens viejos; tu malla no lo tiene, por eso el enforcement vive en el merge y la
garantía es *bounded-detect*, no *prevent*. Y generar épocas *globalmente* monótonas pediría consenso — por
eso son **device-local** (cada dispositivo cuenta sus propios arranques), lo que es coordination-free a
costa de que la detección sea al reconectar, no instantánea.
---
## E. El terminus honesto del proyecto
Tras T11, el enunciado correcto —el que respeta CAP y no promete de más— es:
> **Seguridad coordination-free módulo un supuesto físico nombrado:** cada celda de presupuesto tiene un
> único escritor durable. Bajo ese supuesto (garantizado por §B durabilidad + §C réplica-por-dispositivo),
> el certificado de T10 aplica sin coordinación. Cuando el supuesto se rompe (clon, §D), el daño está
> **acotado a una celda por clon no detectado y se detecta al reconectar** — nunca es silencioso ni
> ilimitado.
Ese es el sitio honesto: no "seguro pase lo que pase", sino "seguro salvo esta condición física, y aquí
está exactamente qué pasa cuando se rompe y cuánto cuesta".
---
## F. Modelo de tipos (bocetos)
```rust
/// spent indexado por (device, epoch): detecta linajes bifurcados en el merge.
pub struct DurableSpent {
pub device_id: DeviceId,
pub epoch: u64, // monótona por dispositivo, persistida al arrancar
pub entries: BTreeMap<u64, i64>, // seq -> monto, solo crece
}
pub struct WriteAheadLog { /* persiste spent+epoch ANTES del ack */ }
impl WriteAheadLog {
pub fn commit_spend(&mut self, seq: u64, amount: i64) -> AckToken { /* fsync, luego ack */ }
pub fn recover(&self) -> DurableSpent { /* spent_i nunca por debajo del último ack */ }
}
pub enum MergeOutcome {
Ok,
CloneDetected { device_id: DeviceId, stale_epoch: u64, live_epoch: u64 },
}
/// EscrowState de T10, ahora con spent durable por (device, epoch) y detección de clon en merge.
impl EscrowState {
pub fn merge(&mut self, other: &EscrowState) -> MergeOutcome { /* ... */ }
}
```
---
## G. Tests (el modelo de crash MALO, no el benigno)
1. **Durabilidad contra rollback (§B).** `proptest`: una réplica gasta y ackea, "crashea" (se descarta su
estado en memoria), recupera desde el WAL, y re-opera. Aserción: `spent_i` recuperado ≥ el del último
ack; nunca re-gasta lo ya comprometido. Incluye el adversario: intentar restaurar un snapshot *por
debajo* del WAL debe ser rechazado, no aceptado.
2. **Réplica-por-dispositivo (§C).** Dos dispositivos de una identidad, cada uno con su celda, gastan
concurrentemente: `total_avail` de la identidad = Σ celdas − Σ spent, invariante. Rebalanceo entre
dispositivos conserva. Ningún gasto de un dispositivo pisa el `avail` del otro.
3. **Detección de clon (§D).** Bifurca un `device_id` en dos épocas, cada clon gasta su celda entera
aislado, luego fusiona: el merge devuelve `CloneDetected`, aísla los gastos de la época menor, y
reporta el daño acotado (≤ una celda). Aserción: tras la detección, el estado reconciliado no propaga el
doble gasto hacia el resto de la malla.
4. **No-regresión del certificado dinámico de T10** bajo el nuevo modelo de `spent` durable-por-época:
sigue verde con fuente monótona; y **falla ruidosamente** (no silenciosamente) cuando se inyecta un
rollback no atrapado — para probar que el test de §G.1 tiene dientes.
---
## H. M4 — el contrato, ahora escribible en piedra
Solo con T11 el adaptador a Tawasuyu/Hammer puede declarar sus precondiciones honestamente:
**Contrato del adaptador (`M4`):**
- **Requiere** WAL durable de `spent` por dispositivo (persistir antes de ack). Sin esto, sin garantía.
- **Requiere** identidad-como-conjunto-de-dispositivos: cada dispositivo es una réplica con su celda.
- **Garantiza** seguridad coordination-free del invariante bajo el supuesto de un-escritor-durable-por-celda.
- **Acota y detecta** (no previene) el doble gasto por clon; expone `CloneDetected` como señal que la capa
de aplicación debe manejar (compensación, alarma). Documentado en `BOUNDARY.md`.
- **Limita** disponibilidad bajo partición al presupuesto local (`AVAILABILITY.md`).
Si Tawasuyu/Hammer no pueden dar durabilidad por dispositivo, el adaptador debe **rehusar** en vez de
prometer seguridad que no tiene. Esa negativa es parte del diseño, no un fallo.
---
## I. Tickets
**T11a — Réplica por dispositivo (F2).**
"Refactoriza el modelo de réplica: `identity = conjunto de device-replicas`, cada una con su `b0[device]` y
`spent[device]`. Ajusta el reparto (`Σ b0 ≤ S` sobre dispositivos) y el rebalanceo (T10b) para operar entre
dispositivos de una identidad. Test §G.2. Ninguna celda tiene más de un escritor lógico."
**T11b — Durabilidad de `spent` (F1).**
"Implementa `WriteAheadLog` (§F): `commit_spend` persiste antes de devolver `AckToken`; `recover`
reconstruye `spent_i` ≥ último ack. Conecta al gasto: no hay ack sin commit durable. Test §G.1, incluido el
adversario que intenta restaurar por debajo del WAL. `spent_i` monótono en la fuente, garantizado."
**T11c — Fencing por época + detección de clon (frontera §D).**
"Indexa `spent` por `(device_id, epoch)`; `epoch` monótona por dispositivo, persistida en el WAL al
arrancar. `merge` devuelve `CloneDetected` cuando halla dos épocas para un `device_id`, aísla la época
menor y acota el daño a una celda. Escribe `BOUNDARY.md`: el teorema de imposibilidad (no hay detección
coordination-free de clon silencioso), la garantía real (bounded + detect-on-reconnect), y por qué las
épocas son device-local (evitar consenso). Tests §G.3 y §G.4. Cuando pase, actualiza `STRONG_RESULT.md`
con el terminus honesto de §E y declara el contrato de M4 (§H) listo para escribir."
---
## J. Referencias
- M. Kleppmann — *How to do distributed locking* (2016) y *Designing Data-Intensive Applications*, cap. 8–9
(fencing tokens; y el punto de que su enforcement clásico necesita un recurso linealizable — de ahí que
aquí viva en el merge).
- P. E. O'Neil 1986; V. Balegas et al. SRDS 2015 (escrow / Bounded Counter, base de T9–T10).
- E. Brewer — CAP (el teorema que §D y §E respetan: safety > availability bajo partición).
- (De addenda previos) Shapiro et al. 2011 (CRDT, base de la representación durable-monótona); Bailis et
al. 2014; Ghrist–Riess 2022; Hansen–Ghrist 2019; Hellerstein–Alvaro.
src/escrow.rs
+95
View File
@@ -190,6 +190,48 @@ impl EscrowState {
}
}
/// Una **identidad** como **conjunto de celdas-dispositivo** (T11a, §C, cura de
/// F2). No se modela la identidad como una réplica: un usuario es un conjunto de
/// dispositivos, cada uno una réplica del esquema de T10 con su propia celda de
/// presupuesto y su propio `spent`. Así la disciplina single-writer se cumple a
/// nivel de **celda-dispositivo**, no de identidad: dos dispositivos gastan sin
/// serializar, sin carrera, sin fencing (F2 es un no-problema por diseño).
///
/// El invariante (el recurso, p.ej. saldo ≥ 0) es de la identidad; su
/// disponibilidad y su certificado se computan sobre SUS dispositivos.
#[derive(Debug, Clone)]
pub struct Identity {
/// Índices de las celdas-dispositivo de esta identidad en el `EscrowState`.
pub devices: Vec<usize>,
/// El invariante del recurso de esta identidad.
pub inv: GlobalInvariant,
}
impl Identity {
/// Crea una identidad con sus dispositivos y su invariante.
pub fn new(devices: Vec<usize>, inv: GlobalInvariant) -> Self {
Self { devices, inv }
}
/// Presupuesto disponible de la identidad = Σ del `avail` de sus dispositivos.
/// Los `grant` **entre** dispositivos de la identidad se cancelan ⟹ solo lo
/// mueven `b0` y `spent`: `total_avail = Σ b0[d] − Σ spent[d]`.
pub fn total_avail(&self, state: &EscrowState) -> i64 {
self.devices.iter().map(|&d| state.avail(d)).sum()
}
/// Valor del recurso de la identidad: `inicial − Σ spent[d]` sobre sus celdas.
pub fn value(&self, state: &EscrowState) -> i64 {
let gastado: i64 = self.devices.iter().map(|&d| state.spent[d]).sum();
self.inv.initial - gastado
}
/// ¿Se preserva el invariante de la identidad?
pub fn invariant_holds(&self, state: &EscrowState) -> bool {
self.inv.holds(self.value(state))
}
}
#[cfg(test)]
mod tests {
use super::*;
@@ -296,6 +338,59 @@ mod tests {
assert_eq!(c2.total_avail(), 30);
}
/// **§G.2 — réplica por dispositivo (F2).** Una identidad con dos
/// dispositivos (celdas `[50,50]`, cuenta 100). Ambos gastan concurrentemente
/// SU celda sin serializar; el gasto de uno **no toca** el `avail` del otro;
/// el `total_avail` de la identidad es `Σ celdas − Σ spent`, invariante.
#[test]
fn t11a_dos_dispositivos_gastan_sin_pisarse() {
let inv = GlobalInvariant::new(100, 0);
let id = Identity::new(vec![0, 1], inv);
let mut state = EscrowState::new(vec![50, 50]);
assert!(state.spend(0, 40));
assert!(state.spend(1, 30));
assert_eq!(state.avail(1), 20, "el gasto de 0 no tocó el avail de 1");
assert_eq!(id.total_avail(&state), 30, "Σ celdas − Σ spent = 100 − 70");
assert!(id.invariant_holds(&state));
// Cada celda tiene un único escritor lógico: 0 no puede gastar la de 1.
assert!(!state.spend(0, 20), "0 ya solo tiene 10 en su propia celda");
}
/// Rebalanceo **entre dispositivos** de una identidad = un `grant`, que
/// conserva el `total_avail` (T10a) — el rebalanceo edge-local de T10b.
#[test]
fn t11a_rebalanceo_entre_dispositivos_conserva() {
let inv = GlobalInvariant::new(100, 0);
let id = Identity::new(vec![0, 1], inv);
let mut state = EscrowState::new(vec![0, 50]);
let antes = id.total_avail(&state);
assert!(state.grant(1, 0, 20), "el dispositivo 1 cede 20 al 0 (seco)");
assert_eq!(state.avail(0), 20);
assert_eq!(state.avail(1), 30);
assert_eq!(id.total_avail(&state), antes, "el rebalanceo conserva");
}
/// Identidades disjuntas no se pisan (F2): la disponibilidad de una identidad
/// depende **solo** de sus dispositivos; la actividad de otra no la afecta.
#[test]
fn t11a_identidades_disjuntas_aisladas() {
let inv = GlobalInvariant::new(100, 0);
let a = Identity::new(vec![0, 1], inv);
let b = Identity::new(vec![2, 3], inv);
let mut state = EscrowState::new(vec![50, 50, 50, 50]);
// Toda la actividad ocurre en la identidad B.
assert!(state.spend(2, 40));
assert!(state.grant(3, 2, 10));
assert_eq!(a.total_avail(&state), 100, "A intacta");
assert!(a.invariant_holds(&state));
assert!(b.invariant_holds(&state));
}
fn escrow_st() -> impl Strategy<Value = EscrowState> {
(1usize..=4).prop_flat_map(|n| {
let b0 = prop::collection::vec(0i64..50, n);