hifas/T11.md

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)

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