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//! **Veredicto honesto (§C):** reconcilia por el orden NATIVO (el merge del CRDT)
13//! y `corre libre ⟺ punto_fijo ∈ V`. Es un test de I-confluence **constructivo,
14//! sensible a la instancia y consciente de la topología**: el mismo programa da
15//! distinto veredicto según los valores concretos y según quién sincroniza con
16//! quién. (Riesgo R-T8b: `p ∈ V` es un predicado **añadido** sobre el punto fijo,
17//! no algo intrínseco al Laplaciano. La difusión calcula el *merge*; I-confluence
18//! es *merge + predicado de validez*.)
19
20use std::collections::{BTreeMap, BTreeSet};
21
22use crate::cell::GCounter;
23use crate::native;
24use crate::nerve::ReplicaId;
25use crate::oracle::OracleVerdict;
26use crate::verdict::{Knot, Verdict};
27
28/// Una instancia del programa "retiros sobre una cuenta con saldo ≥ 0".
29#[derive(Debug, Clone)]
30pub struct AccountConfig {
31    /// Nombre del caso.
32    pub name: String,
33    /// Número de réplicas.
34    pub replicas: usize,
35    /// Saldo inicial `B₀` (la cota del invariante).
36    pub bound: u64,
37    /// Retiro concurrente de cada réplica.
38    pub withdrawals: Vec<u64>,
39    /// Grafo de compartición (quién reconcilia con quién).
40    pub edges: Vec<(usize, usize)>,
41}
42
43impl AccountConfig {
44    /// Construye una instancia (con `withdrawals.len() == replicas`).
45    pub fn new(
46        name: impl Into<String>,
47        bound: u64,
48        withdrawals: Vec<u64>,
49        edges: Vec<(usize, usize)>,
50    ) -> Self {
51        Self {
52            name: name.into(),
53            replicas: withdrawals.len(),
54            bound,
55            withdrawals,
56            edges,
57        }
58    }
59
60    /// Estado local de cada réplica: un `GCounter` con su propia casilla puesta a
61    /// su retiro (grow-only; solo incrementa lo suyo).
62    fn seeds(&self) -> Vec<GCounter> {
63        (0..self.replicas)
64            .map(|i| {
65                let mut slots = vec![0u64; self.replicas];
66                slots[i] = self.withdrawals[i];
67                GCounter { slots }
68            })
69            .collect()
70    }
71
72    /// Estado reconciliado por el orden nativo (merge por componente conexa).
73    pub fn reconcile(&self) -> Vec<GCounter> {
74        native::reconcile(&self.edges, &self.seeds())
75    }
76
77    /// Componentes conexas del grafo (union-find). Camino independiente del merge.
78    fn components(&self) -> Vec<usize> {
79        let mut parent: Vec<usize> = (0..self.replicas).collect();
80        fn find(parent: &mut [usize], x: usize) -> usize {
81            let mut r = x;
82            while parent[r] != r {
83                r = parent[r];
84            }
85            r
86        }
87        for &(a, b) in &self.edges {
88            let ra = find(&mut parent, a);
89            let rb = find(&mut parent, b);
90            if ra != rb {
91                parent[ra] = rb;
92            }
93        }
94        (0..self.replicas).map(|i| find(&mut parent, i)).collect()
95    }
96
97    /// **Veredicto del haz (§C):** difunde al punto fijo y comprueba `∈ V`. Corre
98    /// libre si ninguna componente reconciliada sobregira; si alguna lo hace,
99    /// localiza las réplicas culpables (las que retiraron) y sus aristas.
100    pub fn haz_verdict(&self) -> Verdict {
101        let fixpoint = self.reconcile();
102
103        // Vértices cuyo estado reconciliado viola el invariante (sobregiro).
104        let mut malos = BTreeSet::new();
105        for (v, state) in fixpoint.iter().enumerate() {
106            if self.bound < state.value() {
107                malos.insert(v);
108            }
109        }
110
111        if malos.is_empty() {
112            return Verdict::RunsFree;
113        }
114
115        let replicas: Vec<ReplicaId> = malos
116            .iter()
117            .filter(|&&v| self.withdrawals[v] > 0)
118            .map(|&v| ReplicaId(v))
119            .collect();
120        let edges: Vec<usize> = self
121            .edges
122            .iter()
123            .enumerate()
124            .filter(|(_, &(a, b))| malos.contains(&a) || malos.contains(&b))
125            .map(|(i, _)| i)
126            .collect();
127
128        Verdict::NeedsCoordination {
129            knots: vec![Knot { replicas, edges }],
130        }
131    }
132
133    /// El veredicto del haz como `OracleVerdict` (para comparar).
134    pub fn haz_coordination(&self) -> OracleVerdict {
135        match self.haz_verdict() {
136            Verdict::RunsFree => OracleVerdict::CoordinationFree,
137            Verdict::NeedsCoordination { .. } => OracleVerdict::NeedsCoordination,
138        }
139    }
140
141    /// **CALM sintáctico por-programa:** el retiro es una operación no monótona
142    /// (decrementa el saldo), así que el check crudo condena el programa entero,
143    /// sin mirar valores → siempre `coordina`. Es la respuesta a batir (§D).
144    pub fn calm_syntactic(&self) -> OracleVerdict {
145        OracleVerdict::NeedsCoordination
146    }
147
148    /// **Oráculo de I-confluence independiente** (§D): por un camino que NO usa la
149    /// difusión — suma aritmética de los retiros por componente vía union-find — y
150    /// comprueba `Σ ≤ bound`. El haz debe igualarlo en toda instancia (corrección
151    /// y soundness §E.2).
152    pub fn i_confluence_oracle(&self) -> OracleVerdict {
153        let comp = self.components();
154        let mut sums: BTreeMap<usize, u64> = BTreeMap::new();
155        for (&c, &w) in comp.iter().zip(&self.withdrawals) {
156            *sums.entry(c).or_default() += w;
157        }
158        if sums.values().all(|&s| s <= self.bound) {
159            OracleVerdict::CoordinationFree
160        } else {
161            OracleVerdict::NeedsCoordination
162        }
163    }
164
165    /// ¿Es una **discrepancia buena** (versión fuerte, §D instancia A)? El haz
166    /// corre libre mientras el CALM sintáctico coordina — con `I` preservado.
167    pub fn es_discrepancia_buena(&self) -> bool {
168        self.haz_coordination() == OracleVerdict::CoordinationFree
169            && self.calm_syntactic() == OracleVerdict::NeedsCoordination
170    }
171}
172
173#[cfg(test)]
174mod tests {
175    use super::*;
176    use proptest::prelude::*;
177
178    /// **El premio (§D, instancia A):** dos réplicas retiran 10 cada una de una
179    /// cuenta de 100. Los valores caben (20 ≤ 100) → el haz corre libre. Pero el
180    /// retiro es no monótono → CALM sintáctico coordina. Discrepancia buena: el
181    /// haz es más fino que el check por-programa. Testigo para `STRONG_RESULT.md`.
182    #[test]
183    fn discrepancia_buena_existe() {
184        let a = AccountConfig::new("retiros-que-caben", 100, vec![10, 10], vec![(0, 1)]);
185        assert_eq!(a.haz_coordination(), OracleVerdict::CoordinationFree);
186        assert_eq!(a.calm_syntactic(), OracleVerdict::NeedsCoordination);
187        assert_eq!(a.i_confluence_oracle(), OracleVerdict::CoordinationFree);
188        assert!(a.es_discrepancia_buena());
189    }
190
191    /// Instancia B: los retiros sobregiran (60 + 60 > 100) → el haz coordina, y
192    /// coincide con I-confluence. Además localiza a las dos réplicas culpables.
193    #[test]
194    fn sobregiro_coordina_y_localiza() {
195        let a = AccountConfig::new("retiros-que-sobregiran", 100, vec![60, 60], vec![(0, 1)]);
196        assert_eq!(a.haz_coordination(), OracleVerdict::NeedsCoordination);
197        assert_eq!(a.i_confluence_oracle(), OracleVerdict::NeedsCoordination);
198        match a.haz_verdict() {
199            Verdict::NeedsCoordination { knots } => {
200                assert_eq!(knots[0].replicas, vec![ReplicaId(0), ReplicaId(1)]);
201            }
202            Verdict::RunsFree => panic!("debería coordinar"),
203        }
204    }
205
206    /// **La topología importa** (§F, el pitch de novedad): los MISMOS valores
207    /// (60 y 60 sobre 100) corren libres si las réplicas NO comparten (dos
208    /// componentes de 60) y coordinan si comparten (una de 120). I-confluence
209    /// sobre el grafo real, no sobre un par abstracto.
210    #[test]
211    fn el_mismo_valor_depende_del_grafo() {
212        let desconectado = AccountConfig::new("particion", 100, vec![60, 60], vec![]);
213        let conectado = AccountConfig::new("conjunto", 100, vec![60, 60], vec![(0, 1)]);
214        assert_eq!(desconectado.haz_coordination(), OracleVerdict::CoordinationFree);
215        assert_eq!(conectado.haz_coordination(), OracleVerdict::NeedsCoordination);
216    }
217
218    /// Barrido determinista que **caza** discrepancias buenas: hay muchas, no una
219    /// casualidad. Prueba de que la versión fuerte es robusta.
220    #[test]
221    fn la_caza_encuentra_muchas_discrepancias() {
222        let mut encontradas = 0;
223        for total in 0..=90u64 {
224            for w0 in 0..=total {
225                let a = AccountConfig::new("barrido", 100, vec![w0, total - w0], vec![(0, 1)]);
226                if a.es_discrepancia_buena() {
227                    encontradas += 1;
228                }
229            }
230        }
231        assert!(encontradas > 100, "la discrepancia buena es robusta: {encontradas}");
232    }
233
234    fn instancia() -> impl Strategy<Value = AccountConfig> {
235        (2usize..=5, 1u64..=50).prop_flat_map(|(n, bound)| {
236            let ws = prop::collection::vec(0u64..=40, n);
237            let arista = (0..n, 0..n).prop_filter("sin lazos", |(a, b)| a != b);
238            let es = prop::collection::vec(arista, 0..8);
239            (Just(bound), ws, es)
240                .prop_map(|(bound, ws, es)| AccountConfig::new("prop", bound, ws, es))
241        })
242    }
243
244    proptest! {
245        /// **Corrección (§D):** el haz iguala al oráculo de I-confluence en TODA
246        /// instancia. Dos caminos independientes (difusión de merges vs suma por
247        /// componente) que coinciden siempre.
248        #[test]
249        fn haz_iguala_i_confluence(a in instancia()) {
250            prop_assert_eq!(a.haz_coordination(), a.i_confluence_oracle());
251        }
252
253        /// **Soundness (§E.2, no se negocia):** el haz NUNCA dice "corre libre"
254        /// cuando alguna componente reconciliada viola el invariante.
255        #[test]
256        fn soundness_el_haz_nunca_miente(a in instancia()) {
257            if a.haz_coordination() == OracleVerdict::CoordinationFree {
258                for state in a.reconcile() {
259                    prop_assert!(a.bound >= state.value(), "libre ⟹ invariante preservado");
260                }
261            }
262        }
263    }
264}