tawasuyu/hifas

1//! `escrow` — evitación de coordinación por presupuestos (T9, §B).
2//!
3//! Método de escrow (O'Neil 1986) como Bounded Counter CRDT (Balegas et al.,
4//! SRDS 2015). Para un invariante global `valor ≥ K`:
5//!
6//! 1. El *slack* `S = valor − K` es lo gastable sin romper `I`.
7//! 2. Se **reparte** `S` en presupuestos por réplica `b_i` con `Σ b_i ≤ S`.
8//! 3. Mientras `r_i` tenga presupuesto, **gasta localmente sin coordinar** — y es
9//!    correcto **incluso particionada**, porque `b_i` es suyo.
10//! 4. La única coordinación es el **rebalanceo edge-local** al agotar `b_i` (T9b).
11//!
12//! **El certificado.** Si `spent_i ≤ b_i` en cada réplica, entonces
13//! `valor = inicial − Σ spent_i ≥ inicial − Σ b_i ≥ inicial − S = K`, para **toda
14//! ejecución, orden y partición**. No se descubre tarde: se garantiza por
15//! construcción. Eso es evitación real, no la detección reactiva de T8 (§A).
16//!
17//! **Honestidad (§B):** escrow no vence a CALM; *transforma* la operación
18//! ("retirar sin límite" → "retirar dentro de presupuesto") para que sea
19//! I-confluente, al costo de un rebalanceo ocasional.
20
21use crate::invariant::GlobalInvariant;
22
23/// El resultado de intentar gastar localmente.
24#[derive(Debug, Clone, Copy, PartialEq, Eq)]
25pub enum SpendResult {
26    /// Dentro de presupuesto: gasto local, **cero coordinación**.
27    Local,
28    /// Presupuesto agotado: hace falta rebalanceo edge-local (T9b).
29    NeedsRebalance {
30        /// Cuánto falta para cubrir el gasto pedido.
31        deficit: i64,
32    },
33}
34
35/// El presupuesto repartido: la 0-cocadena `b` sobre las réplicas.
36#[derive(Debug, Clone, PartialEq, Eq)]
37pub struct Budget {
38    /// Presupuesto restante por réplica.
39    pub per_replica: Vec<i64>,
40}
41
42impl Budget {
43    /// Presupuesto a partir de un reparto explícito.
44    pub fn new(per_replica: Vec<i64>) -> Self {
45        Self { per_replica }
46    }
47
48    /// Reparte el `slack` en `n` presupuestos proporcionales a `weights`, con
49    /// división entera para garantizar `Σ b_i ≤ slack` (reparto siempre válido).
50    pub fn split(inv: &GlobalInvariant, weights: &[u64]) -> Self {
51        let s = inv.slack().max(0) as u128;
52        let total: u128 = weights.iter().map(|&w| w as u128).sum();
53        let per_replica = if total == 0 {
54            vec![0; weights.len()]
55        } else {
56            // ⌊w_i · S / total⌋ ⟹ la suma nunca excede S.
57            weights.iter().map(|&w| ((w as u128 * s) / total) as i64).collect()
58        };
59        Self { per_replica }
60    }
61
62    /// El certificado del reparto (§B): `Σ b_i ≤ slack` y todo `b_i ≥ 0`.
63    pub fn is_valid_split(&self, inv: &GlobalInvariant) -> bool {
64        self.per_replica.iter().all(|&b| b >= 0)
65            && self.per_replica.iter().sum::<i64>() <= inv.slack()
66    }
67
68    /// Presupuesto restante de la réplica `r`.
69    pub fn remaining(&self, r: usize) -> i64 {
70        self.per_replica[r]
71    }
72
73    /// Gasto local de `amount` (≥ 0) en la réplica `r`. Si cabe, descuenta y
74    /// devuelve `Local`; si no, **no gasta** y devuelve `NeedsRebalance` con el
75    /// déficit. Nunca declara "libre global" a ciegas.
76    pub fn try_spend(&mut self, r: usize, amount: i64) -> SpendResult {
77        debug_assert!(amount >= 0, "los gastos son no negativos");
78        if amount <= self.per_replica[r] {
79            self.per_replica[r] -= amount;
80            SpendResult::Local
81        } else {
82            SpendResult::NeedsRebalance {
83                deficit: amount - self.per_replica[r],
84            }
85        }
86    }
87
88    /// El valor del recurso implicado por unos gastos `spent_i` (para el
89    /// certificado): `inicial − Σ spent_i`.
90    pub fn value_after(inv: &GlobalInvariant, spent: &[i64]) -> i64 {
91        inv.initial - spent.iter().sum::<i64>()
92    }
93}
94
95#[cfg(test)]
96mod tests {
97    use super::*;
98    use crate::verdict::Verdict;
99    use proptest::prelude::*;
100
101    /// El caso 60/60 de T8, ahora bien tratado (§F): con presupuestos [50,50]
102    /// (reparto válido de S=100), una réplica **particionada** que intenta retirar
103    /// 60 recibe `NeedsRebalance`, NO `Local`. Muere el falso-verde del detector.
104    #[test]
105    fn t9_particionado_60_es_bloqueado_no_libre() {
106        let inv = GlobalInvariant::new(100, 0); // saldo ≥ 0, slack 100
107        let mut budget = Budget::new(vec![50, 50]);
108        assert!(budget.is_valid_split(&inv));
109
110        // La réplica 0, aislada, intenta retirar 60 (> su presupuesto de 50).
111        let res = budget.try_spend(0, 60);
112        assert_eq!(res, SpendResult::NeedsRebalance { deficit: 10 });
113        // El veredicto de escrow NO es "libre": pide rebalanceo (localizado).
114        assert!(matches!(Verdict::via_escrow(0, &res), Verdict::NeedsCoordination { .. }));
115        // Y no gastó: el presupuesto sigue intacto (el gasto queda pendiente).
116        assert_eq!(budget.remaining(0), 50);
117    }
118
119    /// Gasto dentro de presupuesto: local y descuenta.
120    #[test]
121    fn gasto_dentro_de_presupuesto_es_local() {
122        let mut budget = Budget::new(vec![50, 50]);
123        assert_eq!(budget.try_spend(0, 30), SpendResult::Local);
124        assert_eq!(budget.remaining(0), 20);
125        assert!(matches!(Verdict::via_escrow(0, &SpendResult::Local), Verdict::RunsFree));
126    }
127
128    fn split_valido(inv: &GlobalInvariant, raw: &[u64]) -> Budget {
129        let b = Budget::split(inv, raw);
130        assert!(b.is_valid_split(inv), "split debe ser válido por construcción");
131        b
132    }
133
134    proptest! {
135        /// **EL CERTIFICADO (§F, el corazón de T9a).** Para todo reparto válido y
136        /// TODA combinación de gastos dentro de presupuesto —incluidas particiones
137        /// arbitrarias y todas las réplicas gastando su máximo a la vez— el
138        /// invariante global `valor ≥ K` se preserva. Se cuantifica sobre todos
139        /// los estados alcanzables, no sobre un merge concreto.
140        #[test]
141        fn certificado_valor_nunca_baja_del_piso(
142            initial in 0i64..500,
143            floor in -100i64..100,
144            pesos in prop::collection::vec(0u64..50, 1..6),
145            gasto_raw in prop::collection::vec(0u64..600, 1..6),
146        ) {
147            prop_assume!(initial >= floor);              // slack ≥ 0
148            let inv = GlobalInvariant::new(initial, floor);
149            let budget = split_valido(&inv, &pesos);
150
151            // Gastos arbitrarios pero acotados por el presupuesto de cada réplica.
152            let spent: Vec<i64> = budget
153                .per_replica
154                .iter()
155                .zip(gasto_raw.iter().chain(std::iter::repeat(&0)))
156                .map(|(&b, &g)| (g as i64).min(b))       // spent_i ≤ b_i
157                .collect();
158
159            // El certificado: valor = inicial − Σ spent ≥ floor. Para cualquier
160            // subconjunto que sincronice (partición) el valor es aún mayor.
161            let valor = Budget::value_after(&inv, &spent);
162            prop_assert!(inv.holds(valor), "valor {} < piso {}", valor, inv.floor);
163        }
164    }
165}