//! `escrow` — evitación de coordinación por presupuestos (T9, §B). //! //! Método de escrow (O'Neil 1986) como Bounded Counter CRDT (Balegas et al., //! SRDS 2015). Para un invariante global `valor ≥ K`: //! //! 1. El *slack* `S = valor − K` es lo gastable sin romper `I`. //! 2. Se **reparte** `S` en presupuestos por réplica `b_i` con `Σ b_i ≤ S`. //! 3. Mientras `r_i` tenga presupuesto, **gasta localmente sin coordinar** — y es //! correcto **incluso particionada**, porque `b_i` es suyo. //! 4. La única coordinación es el **rebalanceo edge-local** al agotar `b_i` (T9b). //! //! **El certificado.** Si `spent_i ≤ b_i` en cada réplica, entonces //! `valor = inicial − Σ spent_i ≥ inicial − Σ b_i ≥ inicial − S = K`, para **toda //! ejecución, orden y partición**. No se descubre tarde: se garantiza por //! construcción. Eso es evitación real, no la detección reactiva de T8 (§A). //! //! **Honestidad (§B):** escrow no vence a CALM; *transforma* la operación //! ("retirar sin límite" → "retirar dentro de presupuesto") para que sea //! I-confluente, al costo de un rebalanceo ocasional. use crate::invariant::GlobalInvariant; /// El resultado de intentar gastar localmente. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum SpendResult { /// Dentro de presupuesto: gasto local, **cero coordinación**. Local, /// Presupuesto agotado: hace falta rebalanceo edge-local (T9b). NeedsRebalance { /// Cuánto falta para cubrir el gasto pedido. deficit: i64, }, } /// El presupuesto repartido: la 0-cocadena `b` sobre las réplicas. #[derive(Debug, Clone, PartialEq, Eq)] pub struct Budget { /// Presupuesto restante por réplica. pub per_replica: Vec, } impl Budget { /// Presupuesto a partir de un reparto explícito. pub fn new(per_replica: Vec) -> Self { Self { per_replica } } /// Reparte el `slack` en `n` presupuestos proporcionales a `weights`, con /// división entera para garantizar `Σ b_i ≤ slack` (reparto siempre válido). pub fn split(inv: &GlobalInvariant, weights: &[u64]) -> Self { let s = inv.slack().max(0) as u128; let total: u128 = weights.iter().map(|&w| w as u128).sum(); let per_replica = if total == 0 { vec![0; weights.len()] } else { // ⌊w_i · S / total⌋ ⟹ la suma nunca excede S. weights.iter().map(|&w| ((w as u128 * s) / total) as i64).collect() }; Self { per_replica } } /// El certificado del reparto (§B): `Σ b_i ≤ slack` y todo `b_i ≥ 0`. pub fn is_valid_split(&self, inv: &GlobalInvariant) -> bool { self.per_replica.iter().all(|&b| b >= 0) && self.per_replica.iter().sum::() <= inv.slack() } /// Presupuesto restante de la réplica `r`. pub fn remaining(&self, r: usize) -> i64 { self.per_replica[r] } /// Gasto local de `amount` (≥ 0) en la réplica `r`. Si cabe, descuenta y /// devuelve `Local`; si no, **no gasta** y devuelve `NeedsRebalance` con el /// déficit. Nunca declara "libre global" a ciegas. pub fn try_spend(&mut self, r: usize, amount: i64) -> SpendResult { debug_assert!(amount >= 0, "los gastos son no negativos"); if amount <= self.per_replica[r] { self.per_replica[r] -= amount; SpendResult::Local } else { SpendResult::NeedsRebalance { deficit: amount - self.per_replica[r], } } } /// El valor del recurso implicado por unos gastos `spent_i` (para el /// certificado): `inicial − Σ spent_i`. pub fn value_after(inv: &GlobalInvariant, spent: &[i64]) -> i64 { inv.initial - spent.iter().sum::() } } #[cfg(test)] mod tests { use super::*; use crate::verdict::Verdict; use proptest::prelude::*; /// El caso 60/60 de T8, ahora bien tratado (§F): con presupuestos [50,50] /// (reparto válido de S=100), una réplica **particionada** que intenta retirar /// 60 recibe `NeedsRebalance`, NO `Local`. Muere el falso-verde del detector. #[test] fn t9_particionado_60_es_bloqueado_no_libre() { let inv = GlobalInvariant::new(100, 0); // saldo ≥ 0, slack 100 let mut budget = Budget::new(vec![50, 50]); assert!(budget.is_valid_split(&inv)); // La réplica 0, aislada, intenta retirar 60 (> su presupuesto de 50). let res = budget.try_spend(0, 60); assert_eq!(res, SpendResult::NeedsRebalance { deficit: 10 }); // El veredicto de escrow NO es "libre": pide rebalanceo (localizado). assert!(matches!(Verdict::via_escrow(0, &res), Verdict::NeedsCoordination { .. })); // Y no gastó: el presupuesto sigue intacto (el gasto queda pendiente). assert_eq!(budget.remaining(0), 50); } /// Gasto dentro de presupuesto: local y descuenta. #[test] fn gasto_dentro_de_presupuesto_es_local() { let mut budget = Budget::new(vec![50, 50]); assert_eq!(budget.try_spend(0, 30), SpendResult::Local); assert_eq!(budget.remaining(0), 20); assert!(matches!(Verdict::via_escrow(0, &SpendResult::Local), Verdict::RunsFree)); } fn split_valido(inv: &GlobalInvariant, raw: &[u64]) -> Budget { let b = Budget::split(inv, raw); assert!(b.is_valid_split(inv), "split debe ser válido por construcción"); b } proptest! { /// **EL CERTIFICADO (§F, el corazón de T9a).** Para todo reparto válido y /// TODA combinación de gastos dentro de presupuesto —incluidas particiones /// arbitrarias y todas las réplicas gastando su máximo a la vez— el /// invariante global `valor ≥ K` se preserva. Se cuantifica sobre todos /// los estados alcanzables, no sobre un merge concreto. #[test] fn certificado_valor_nunca_baja_del_piso( initial in 0i64..500, floor in -100i64..100, pesos in prop::collection::vec(0u64..50, 1..6), gasto_raw in prop::collection::vec(0u64..600, 1..6), ) { prop_assume!(initial >= floor); // slack ≥ 0 let inv = GlobalInvariant::new(initial, floor); let budget = split_valido(&inv, &pesos); // Gastos arbitrarios pero acotados por el presupuesto de cada réplica. let spent: Vec = budget .per_replica .iter() .zip(gasto_raw.iter().chain(std::iter::repeat(&0))) .map(|(&b, &g)| (g as i64).min(b)) // spent_i ≤ b_i .collect(); // El certificado: valor = inicial − Σ spent ≥ floor. Para cualquier // subconjunto que sincronice (partición) el valor es aún mayor. let valor = Budget::value_after(&inv, &spent); prop_assert!(inv.holds(valor), "valor {} < piso {}", valor, inv.floor); } } }