tawasuyu/hifas

1//! `invariant` — coordinación de verdad: I-confluence sobre el grafo (T8c, §C–§F).
2//!
3//! Sin invariante, un CRDT nunca coordina (T8a/b). La coordinación aparece cuando
4//! hay un **invariante global `I`** que la fusión no preserva: los estados válidos
5//! `V = {s : I(s)}` no son cerrados bajo join. Ejemplo canónico (Bailis et al.,
6//! VLDB 2014): **saldo ≥ 0**.
7//!
8//! Modelo: `bound` = saldo inicial; cada réplica `i` retira `withdrawals[i]`. El
9//! estado es un `GCounter` grow-only de retiros (merge = máximo por casilla). El
10//! invariante sobre un estado reconciliado `s` es `bound ≥ Σ retiros(s)`.
11//!
12//! **`AccountConfig` es un DETECTOR reactivo por-estado** (T8c): funde estados ya
13//! divergidos y comprueba el merge. T9 §A lo degrada de "consejero de
14//! coordinación" a alarma: tiene un **punto ciego** (una restricción global
15//! codificada por aristas desaparece al particionar el grafo — ver `COMPARISON.md`
16//! y el test `t9_punto_ciego...`). La **evitación** real vive en `escrow` sobre la
17//! restricción global `GlobalInvariant` de abajo, no aquí.
18
19use std::collections::{BTreeMap, BTreeSet};
20
21use crate::cell::GCounter;
22use crate::native;
23use crate::nerve::ReplicaId;
24use crate::oracle::OracleVerdict;
25use crate::verdict::{Knot, Verdict};
26
27/// Una **restricción global** `valor ≥ floor` (T9 §D): incide sobre TODAS las
28/// réplicas que tocan el recurso, compartan arista o no. No es edge-local — ese
29/// fue el Error 2 de T8. El escrow reparte su `slack` en presupuestos por réplica.
30#[derive(Debug, Clone, Copy, PartialEq, Eq)]
31pub struct GlobalInvariant {
32    /// `K` en `valor ≥ K`.
33    pub floor: i64,
34    /// Valor inicial del recurso.
35    pub initial: i64,
36}
37
38impl GlobalInvariant {
39    /// Crea la restricción `valor ≥ floor` con valor inicial `initial`.
40    pub fn new(initial: i64, floor: i64) -> Self {
41        Self { floor, initial }
42    }
43
44    /// El *slack* `S = valor − K`: lo que se puede gastar sin romper `I`.
45    pub fn slack(&self) -> i64 {
46        self.initial - self.floor
47    }
48
49    /// ¿El valor dado satisface el invariante?
50    pub fn holds(&self, value: i64) -> bool {
51        value >= self.floor
52    }
53}
54
55/// Una instancia del programa "retiros sobre una cuenta con saldo ≥ 0".
56#[derive(Debug, Clone)]
57pub struct AccountConfig {
58    /// Nombre del caso.
59    pub name: String,
60    /// Número de réplicas.
61    pub replicas: usize,
62    /// Saldo inicial `B₀` (la cota del invariante).
63    pub bound: u64,
64    /// Retiro concurrente de cada réplica.
65    pub withdrawals: Vec<u64>,
66    /// Grafo de compartición (quién reconcilia con quién).
67    pub edges: Vec<(usize, usize)>,
68}
69
70impl AccountConfig {
71    /// Construye una instancia (con `withdrawals.len() == replicas`).
72    pub fn new(
73        name: impl Into<String>,
74        bound: u64,
75        withdrawals: Vec<u64>,
76        edges: Vec<(usize, usize)>,
77    ) -> Self {
78        Self {
79            name: name.into(),
80            replicas: withdrawals.len(),
81            bound,
82            withdrawals,
83            edges,
84        }
85    }
86
87    /// Estado local de cada réplica: un `GCounter` con su propia casilla puesta a
88    /// su retiro (grow-only; solo incrementa lo suyo).
89    fn seeds(&self) -> Vec<GCounter> {
90        (0..self.replicas)
91            .map(|i| {
92                let mut slots = vec![0u64; self.replicas];
93                slots[i] = self.withdrawals[i];
94                GCounter { slots }
95            })
96            .collect()
97    }
98
99    /// Estado reconciliado por el orden nativo (merge por componente conexa).
100    pub fn reconcile(&self) -> Vec<GCounter> {
101        native::reconcile(&self.edges, &self.seeds())
102    }
103
104    /// Componentes conexas del grafo (union-find). Camino independiente del merge.
105    fn components(&self) -> Vec<usize> {
106        let mut parent: Vec<usize> = (0..self.replicas).collect();
107        fn find(parent: &mut [usize], x: usize) -> usize {
108            let mut r = x;
109            while parent[r] != r {
110                r = parent[r];
111            }
112            r
113        }
114        for &(a, b) in &self.edges {
115            let ra = find(&mut parent, a);
116            let rb = find(&mut parent, b);
117            if ra != rb {
118                parent[ra] = rb;
119            }
120        }
121        (0..self.replicas).map(|i| find(&mut parent, i)).collect()
122    }
123
124    /// **Veredicto del haz (§C):** difunde al punto fijo y comprueba `∈ V`. Corre
125    /// libre si ninguna componente reconciliada sobregira; si alguna lo hace,
126    /// localiza las réplicas culpables (las que retiraron) y sus aristas.
127    pub fn haz_verdict(&self) -> Verdict {
128        let fixpoint = self.reconcile();
129
130        // Vértices cuyo estado reconciliado viola el invariante (sobregiro).
131        let mut malos = BTreeSet::new();
132        for (v, state) in fixpoint.iter().enumerate() {
133            if self.bound < state.value() {
134                malos.insert(v);
135            }
136        }
137
138        if malos.is_empty() {
139            return Verdict::RunsFree;
140        }
141
142        let replicas: Vec<ReplicaId> = malos
143            .iter()
144            .filter(|&&v| self.withdrawals[v] > 0)
145            .map(|&v| ReplicaId(v))
146            .collect();
147        let edges: Vec<usize> = self
148            .edges
149            .iter()
150            .enumerate()
151            .filter(|(_, &(a, b))| malos.contains(&a) || malos.contains(&b))
152            .map(|(i, _)| i)
153            .collect();
154
155        Verdict::NeedsCoordination {
156            knots: vec![Knot { replicas, edges }],
157        }
158    }
159
160    /// El veredicto del haz como `OracleVerdict` (para comparar).
161    pub fn haz_coordination(&self) -> OracleVerdict {
162        match self.haz_verdict() {
163            Verdict::RunsFree => OracleVerdict::CoordinationFree,
164            Verdict::NeedsCoordination { .. } => OracleVerdict::NeedsCoordination,
165        }
166    }
167
168    /// **CALM sintáctico por-programa:** el retiro es una operación no monótona
169    /// (decrementa el saldo), así que el check crudo condena el programa entero,
170    /// sin mirar valores → siempre `coordina`. Es la respuesta a batir (§D).
171    pub fn calm_syntactic(&self) -> OracleVerdict {
172        OracleVerdict::NeedsCoordination
173    }
174
175    /// **Oráculo de I-confluence independiente** (§D): por un camino que NO usa la
176    /// difusión — suma aritmética de los retiros por componente vía union-find — y
177    /// comprueba `Σ ≤ bound`. El haz debe igualarlo en toda instancia (corrección
178    /// y soundness §E.2).
179    pub fn i_confluence_oracle(&self) -> OracleVerdict {
180        let comp = self.components();
181        let mut sums: BTreeMap<usize, u64> = BTreeMap::new();
182        for (&c, &w) in comp.iter().zip(&self.withdrawals) {
183            *sums.entry(c).or_default() += w;
184        }
185        if sums.values().all(|&s| s <= self.bound) {
186            OracleVerdict::CoordinationFree
187        } else {
188            OracleVerdict::NeedsCoordination
189        }
190    }
191
192    /// ¿Es una **discrepancia buena** (versión fuerte, §D instancia A)? El haz
193    /// corre libre mientras el CALM sintáctico coordina — con `I` preservado.
194    pub fn es_discrepancia_buena(&self) -> bool {
195        self.haz_coordination() == OracleVerdict::CoordinationFree
196            && self.calm_syntactic() == OracleVerdict::NeedsCoordination
197    }
198}
199
200#[cfg(test)]
201mod tests {
202    use super::*;
203    use proptest::prelude::*;
204
205    /// **El premio (§D, instancia A):** dos réplicas retiran 10 cada una de una
206    /// cuenta de 100. Los valores caben (20 ≤ 100) → el haz corre libre. Pero el
207    /// retiro es no monótono → CALM sintáctico coordina. Discrepancia buena: el
208    /// haz es más fino que el check por-programa. Testigo para `STRONG_RESULT.md`.
209    #[test]
210    fn discrepancia_buena_existe() {
211        let a = AccountConfig::new("retiros-que-caben", 100, vec![10, 10], vec![(0, 1)]);
212        assert_eq!(a.haz_coordination(), OracleVerdict::CoordinationFree);
213        assert_eq!(a.calm_syntactic(), OracleVerdict::NeedsCoordination);
214        assert_eq!(a.i_confluence_oracle(), OracleVerdict::CoordinationFree);
215        assert!(a.es_discrepancia_buena());
216    }
217
218    /// Instancia B: los retiros sobregiran (60 + 60 > 100) → el haz coordina, y
219    /// coincide con I-confluence. Además localiza a las dos réplicas culpables.
220    #[test]
221    fn sobregiro_coordina_y_localiza() {
222        let a = AccountConfig::new("retiros-que-sobregiran", 100, vec![60, 60], vec![(0, 1)]);
223        assert_eq!(a.haz_coordination(), OracleVerdict::NeedsCoordination);
224        assert_eq!(a.i_confluence_oracle(), OracleVerdict::NeedsCoordination);
225        match a.haz_verdict() {
226            Verdict::NeedsCoordination { knots } => {
227                assert_eq!(knots[0].replicas, vec![ReplicaId(0), ReplicaId(1)]);
228            }
229            Verdict::RunsFree => panic!("debería coordinar"),
230        }
231    }
232
233    /// **El PUNTO CIEGO del detector** (T9 §A, Error 2). Lo que T8c celebraba como
234    /// "la topología importa" es en realidad un falso-verde peligroso: con los
235    /// mismos retiros 60/60 sobre 100, el detector dice `libre` al **particionar**
236    /// —el caso MÁS peligroso— porque, sin arista, no ve el acoplamiento del
237    /// invariante GLOBAL. No es que sea seguro; es que el haz está ciego. La cura
238    /// (escrow) bloquea correctamente ese caso: ver `escrow::tests` y `COMPARISON.md`.
239    #[test]
240    fn t9_punto_ciego_del_detector_particionado() {
241        let desconectado = AccountConfig::new("particion", 100, vec![60, 60], vec![]);
242        let conectado = AccountConfig::new("conjunto", 100, vec![60, 60], vec![(0, 1)]);
243        // Conectado detecta el sobregiro...
244        assert_eq!(conectado.haz_coordination(), OracleVerdict::NeedsCoordination);
245        // ...pero particionado lo declara "libre": ESO es el bug que motiva T9.
246        assert_eq!(desconectado.haz_coordination(), OracleVerdict::CoordinationFree);
247    }
248
249    /// Barrido determinista que **caza** discrepancias buenas: hay muchas, no una
250    /// casualidad. Prueba de que la versión fuerte es robusta.
251    #[test]
252    fn la_caza_encuentra_muchas_discrepancias() {
253        let mut encontradas = 0;
254        for total in 0..=90u64 {
255            for w0 in 0..=total {
256                let a = AccountConfig::new("barrido", 100, vec![w0, total - w0], vec![(0, 1)]);
257                if a.es_discrepancia_buena() {
258                    encontradas += 1;
259                }
260            }
261        }
262        assert!(encontradas > 100, "la discrepancia buena es robusta: {encontradas}");
263    }
264
265    fn instancia() -> impl Strategy<Value = AccountConfig> {
266        (2usize..=5, 1u64..=50).prop_flat_map(|(n, bound)| {
267            let ws = prop::collection::vec(0u64..=40, n);
268            let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
269            let es = prop::collection::vec(arista, 0..8);
270            (Just(bound), ws, es)
271                .prop_map(|(bound, ws, es)| AccountConfig::new("prop", bound, ws, es))
272        })
273    }
274
275    proptest! {
276        /// **Corrección (§D):** el haz iguala al oráculo de I-confluence en TODA
277        /// instancia. Dos caminos independientes (difusión de merges vs suma por
278        /// componente) que coinciden siempre.
279        #[test]
280        fn haz_iguala_i_confluence(a in instancia()) {
281            prop_assert_eq!(a.haz_coordination(), a.i_confluence_oracle());
282        }
283
284        /// **Soundness (§E.2, no se negocia):** el haz NUNCA dice "corre libre"
285        /// cuando alguna componente reconciliada viola el invariante.
286        #[test]
287        fn soundness_el_haz_nunca_miente(a in instancia()) {
288            if a.haz_coordination() == OracleVerdict::CoordinationFree {
289                for state in a.reconcile() {
290                    prop_assert!(a.bound >= state.value(), "libre ⟹ invariante preservado");
291                }
292            }
293        }
294    }
295}