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.
T10 §F.5: sube el certificado de estático a DINÁMICO. proptest que entrelaza
gastos + grants concurrentes + crashes (grants sin propagar) + particiones
(merges en orden arbitrario) sobre copias por réplica, y verifica en TODO
momento:
- valor = inicial − Σ spent ≥ K (nunca sobregira);
- total_avail ≥ 0 (nunca fabrica presupuesto).
Subsume el certificado estático de T9. Con single-writer por réplica (spend/
grant guardados por el avail local) y merge CRDT, ninguna carrera rompe la
conservación.
STRONG_RESULT.md: marca la evitación de escrow como segura DINÁMICAMENTE (no
solo snapshot) y declara M4 desbloqueado de verdad, con la honestidad §G
(T10 = Bounded Counter/CRDT clásico bien implementado, no novedad; el aporte
sigue siendo el ruteo/localización por el grafo).
62 tests, clippy limpio. Hito T10 cerrado.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
diff --git a/STRONG_RESULT.md b/STRONG_RESULT.md
index 96bc5db..da344cc 100644
--- a/STRONG_RESULT.md
+++ b/STRONG_RESULT.md
@@ -76,3 +76,28 @@ resuelto)— sería nuevo; se reclamará solo si se construye.
- **T9: evitación real por escrow, con certificado, ruteada por el grafo.** Ahí
está la contribución defendible — y las fronteras (R-T9b: recurso divisible;
R-T9c: la novedad es el ruteo/localización, no el booleano).
+- **T10: la evitación es segura DINÁMICAMENTE**, no solo en snapshot (§H, §J).
+
+## T10 — certificado dinámico (M4 desbloqueado de verdad)
+
+El certificado de T9 valía para un reparto **congelado**, testeado
+secuencialmente. T10 cierra la grieta estático→dinámico:
+
+- **Transferencia sin carreras** (`EscrowState`, T10a): presupuesto con procedencia
+ (`granted[from][to]`, `spent[i]` monótonos; `avail` derivado). `Σ avail =
+ Σ b0 − Σ spent` es invariante a los `granted` ⟹ **imposible fabricar** por fusión
+ ni **perder** por crash (un `grant` vive entero en su celda).
+- **Fail-safe bajo partición** (`RebalanceResult::Unreachable`, T10b): sin ruta,
+ el gasto se rechaza y la réplica se limita a su presupuesto local; nunca
+ sobregira ni cuelga. El precio honesto está en `AVAILABILITY.md` (CAP: safety
+ sobre availability).
+- **El teorema** (`escrow::tests::certificado_dinamico`, T10c): entrelazando
+ gastos + `grant`s concurrentes + crashes + particiones en órdenes de fusión
+ arbitrarios, `valor = inicial − Σ spent ≥ K` **en todo momento** y `total_avail
+ ≥ 0` siempre. Subsume el certificado estático de T9.
+
+Solo con esta base —conservación bajo concurrencia, partición y crash— tiene
+sentido **M4**: cablear el escrow a una malla de gossip donde los rebalanceos
+corren de verdad. **M4 queda desbloqueado.** Honestidad (T10 §G): T10 no es
+novedad (Bounded Counter/CRDT clásico, Balegas 2015, bien implementado); el aporte
+defendible sigue siendo el ruteo/localización por el grafo real.
diff --git a/src/escrow.rs b/src/escrow.rs
index 292440a..c6d14f5 100644
--- a/src/escrow.rs
+++ b/src/escrow.rs
@@ -319,7 +319,63 @@ mod tests {
})
}
+ /// Fusiona todas las copias en una vista global (el estado "verdadero").
+ fn merge_all(copies: &[EscrowState], b0: &[i64]) -> EscrowState {
+ let mut g = EscrowState::new(b0.to_vec());
+ for c in copies {
+ g.merge(c);
+ }
+ g
+ }
+
+ /// Escenario dinámico: invariante, reparto por pesos, y una secuencia de
+ /// eventos `(op, x, y, monto)` a interpretar como spend/grant/merge.
+ #[allow(clippy::type_complexity)]
+ fn escenario() -> impl Strategy<Value = (GlobalInvariant, Vec<u64>, Vec<(u8, usize, usize, i64)>)> {
+ (2usize..=4, 0i64..200, -50i64..50).prop_flat_map(|(n, slack, floor)| {
+ let inv = GlobalInvariant::new(floor + slack, floor);
+ let pesos = prop::collection::vec(0u64..20, n);
+ let evento = (0u8..3, 0..n, 0..n, 0i64..80);
+ let eventos = prop::collection::vec(evento, 0..40);
+ (Just(inv), pesos, eventos)
+ })
+ }
+
proptest! {
+ /// **§F.5 — EL CERTIFICADO DINÁMICO (el teorema de T10).** Entrelaza gastos,
+ /// transferencias (`grant`) concurrentes, crashes (grants sin propagar) y
+ /// particiones (merges en orden arbitrario) sobre copias por réplica. En
+ /// **todo momento** `valor = inicial − Σ spent ≥ K`, y el presupuesto total
+ /// nunca se fabrica (`total_avail ≥ 0`). Subsume el certificado estático de
+ /// T9: ya no vale solo para snapshots congelados, sino bajo concurrencia.
+ #[test]
+ fn certificado_dinamico(( inv, pesos, eventos) in escenario()) {
+ let n = pesos.len();
+ // Reparto válido: Σ b0 ≤ slack (mismo split proporcional de T9a).
+ let b0 = Budget::split(&inv, &pesos).per_replica;
+ // Una copia local por réplica (vistas divergibles bajo partición).
+ let mut copies = vec![EscrowState::new(b0.clone()); n];
+
+ for (op, x, y, amount) in eventos {
+ let i = x % n;
+ let j = y % n;
+ match op % 3 {
+ // Gasto local, guardado por el avail local (single-writer índice i).
+ 0 => { copies[i].spend(i, amount); }
+ // Transferencia: la réplica i cede desde SU fila, guardada.
+ 1 => { copies[i].grant(i, j, amount); }
+ // Sincronización: i fusiona la copia de j (orden arbitrario = partición/crash).
+ _ => { let otra = copies[j].clone(); copies[i].merge(&otra); }
+ }
+
+ // El teorema, tras cada evento: la vista global no fabrica ni sobregira.
+ let global = merge_all(&copies, &b0);
+ prop_assert!(global.total_avail() >= 0, "presupuesto fabricado: total_avail < 0");
+ let valor = inv.initial - global.spent.iter().sum::<i64>();
+ prop_assert!(inv.holds(valor), "valor {} < piso {}", valor, inv.floor);
+ }
+ }
+
/// **§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.