tawasuyu/hifas

1//! `oracle` — evaluador CRDT/CALM de referencia, independiente del haz (§8 M3).
2//!
3//! Para cada configuración el oráculo dice, por CALM puro (monotonicidad de las
4//! operaciones compartidas), si es coordination-free — sin mirar el haz. El test
5//! maestro compara ese veredicto con el del haz para validar la Hipótesis H
6//! (§2.2). Donde discrepan (§11 R1) se documenta en `DISCREPANCIES.md`.
7
8use crate::cohomology::compute_with;
9use crate::gf2::Gf2Backend;
10use crate::lattice::{IdentityGalois, ResetVal};
11use crate::sheaf::Sheaf;
12use crate::tarski::LatticeSheaf;
13use crate::verdict::Verdict;
14
15/// Predicción independiente del oráculo para una configuración.
16#[derive(Debug, Clone, Copy, PartialEq, Eq)]
17pub enum OracleVerdict {
18    /// El oráculo cree que la configuración es libre de coordinación.
19    CoordinationFree,
20    /// El oráculo cree que hace falta coordinar.
21    NeedsCoordination,
22}
23
24/// Un dato compartido entre dos réplicas, con la marca CALM de si la operación
25/// que lo toca es monótona.
26#[derive(Debug, Clone, Copy)]
27pub struct Share {
28    /// Primera réplica que comparte.
29    pub a: usize,
30    /// Segunda réplica que comparte.
31    pub b: usize,
32    /// ¿La operación sobre este dato es monótona? (viene de `Cell::is_monotone`).
33    pub monotone: bool,
34}
35
36impl Share {
37    /// Dato compartido monótono (se funde solo).
38    pub fn monotona(a: usize, b: usize) -> Self {
39        Self { a, b, monotone: true }
40    }
41
42    /// Dato compartido no monótono (reset/overwrite → posible conflicto).
43    pub fn no_monotona(a: usize, b: usize) -> Self {
44        Self { a, b, monotone: false }
45    }
46}
47
48/// Una configuración de réplicas con sus datos compartidos.
49#[derive(Debug, Clone)]
50pub struct Config {
51    /// Nombre del caso (para reportes).
52    pub name: String,
53    /// Número de réplicas.
54    pub replicas: usize,
55    /// Datos compartidos.
56    pub shares: Vec<Share>,
57}
58
59impl Config {
60    /// Construye una configuración.
61    pub fn new(name: impl Into<String>, replicas: usize, shares: Vec<Share>) -> Self {
62        Self {
63            name: name.into(),
64            replicas,
65            shares,
66        }
67    }
68
69    /// **Oráculo CALM (independiente del haz).** Coordination-free ⟺ toda
70    /// operación compartida es monótona. En cuanto aparece una no monótona
71    /// compartida, CALM exige coordinación.
72    pub fn oracle_verdict(&self) -> OracleVerdict {
73        if self.shares.iter().all(|s| s.monotone) {
74            OracleVerdict::CoordinationFree
75        } else {
76            OracleVerdict::NeedsCoordination
77        }
78    }
79
80    /// Codificación lineal de la configuración como haz (la codificación honesta
81    /// de la §2.3, sin colapsar ciclos monótonos):
82    /// - cada dato compartido → una arista de acuerdo (restricción identidad);
83    /// - una operación no monótona añade un segundo enlace en conflicto sobre el
84    ///   mismo par → un 2-ciclo localizado (como la Corrida B de M1).
85    pub fn to_sheaf(&self) -> Sheaf {
86        let mut edges = Vec::new();
87        for s in &self.shares {
88            edges.push((s.a, s.b));
89            if !s.monotone {
90                edges.push((s.a, s.b)); // el reset impone un segundo constraint irreconciliable
91            }
92        }
93        Sheaf::constant(self.replicas, &edges, 1)
94    }
95
96    /// **Veredicto del haz lineal.** Coordination-free ⟺ `H¹ = 0`. Usa la
97    /// aritmética exacta `GF(2)`. Es el detector topológico barato del MVP.
98    pub fn sheaf_verdict(&self) -> OracleVerdict {
99        let sheaf = self.to_sheaf();
100        let coho = compute_with(&sheaf, &Gf2Backend).expect("haz bien formado");
101        if coho.dim_h1 == 0 {
102            OracleVerdict::CoordinationFree
103        } else {
104            OracleVerdict::NeedsCoordination
105        }
106    }
107
108    /// Generación de retículo por réplica = componente del **subgrafo monótono**.
109    /// Réplicas ligadas por datos monótonos comparten generación (comparables);
110    /// las separadas por una operación no monótona caen en generaciones distintas
111    /// (incomparables → su reconciliación colapsa a ⊤).
112    fn monotone_generations(&self) -> Vec<u64> {
113        let mut parent: Vec<usize> = (0..self.replicas).collect();
114        fn find(parent: &mut [usize], x: usize) -> usize {
115            let mut r = x;
116            while parent[r] != r {
117                r = parent[r];
118            }
119            r
120        }
121        for s in &self.shares {
122            if s.monotone {
123                let ra = find(&mut parent, s.a);
124                let rb = find(&mut parent, s.b);
125                if ra != rb {
126                    parent[ra] = rb;
127                }
128            }
129        }
130        (0..self.replicas).map(|r| find(&mut parent, r) as u64).collect()
131    }
132
133    /// **Veredicto por difusión de Tarski** (Addendum §C, T7): encoda la config
134    /// como haz de retículos (`ResetVal` uniforme, restricción identidad),
135    /// siembra cada réplica en la generación de su componente monótona, y
136    /// harmoniza. Coordination-free ⟺ el punto fijo no colapsa a ⊤.
137    pub fn tarski_verdict(&self) -> OracleVerdict {
138        let gens = self.monotone_generations();
139        let seed: Vec<ResetVal> = (0..self.replicas)
140            .map(|r| ResetVal::Gen {
141                generation: gens[r],
142                value: r as i64,
143            })
144            .collect();
145        let sheaf = LatticeSheaf::new(
146            self.replicas,
147            self.shares.iter().map(|s| (s.a, s.b)).collect(),
148            IdentityGalois,
149        );
150        match Verdict::via_tarski(&sheaf, &seed) {
151            Verdict::RunsFree => OracleVerdict::CoordinationFree,
152            Verdict::NeedsCoordination { .. } => OracleVerdict::NeedsCoordination,
153        }
154    }
155}
156
157/// Batería de casos donde el haz y el oráculo **coinciden** (§8 M3, ≥20 casos).
158///
159/// Régimen de acuerdo: sharing monótono acíclico (→ ambos "corre libre") y
160/// cualquier configuración con al menos una operación no monótona (→ ambos
161/// "coordina"). El test maestro verifica la coincidencia en todos.
162pub fn casos_de_acuerdo() -> Vec<Config> {
163    let mut casos = Vec::new();
164
165    // --- Monótonos acíclicos → CoordinationFree ---
166    // Caminos de longitud creciente.
167    for k in 2..=10 {
168        let shares = (0..k - 1).map(|i| Share::monotona(i, i + 1)).collect();
169        casos.push(Config::new(format!("camino-monotono-{k}"), k, shares));
170    }
171    // Estrella (centro 0, hojas 1..=4).
172    casos.push(Config::new(
173        "estrella-monotona",
174        5,
175        (1..=4).map(|h| Share::monotona(0, h)).collect(),
176    ));
177    // Árbol binario.
178    casos.push(Config::new(
179        "arbol-binario-monotono",
180        5,
181        vec![
182            Share::monotona(0, 1),
183            Share::monotona(0, 2),
184            Share::monotona(1, 3),
185            Share::monotona(1, 4),
186        ],
187    ));
188    // Bosque desconexo (dos árboles).
189    casos.push(Config::new(
190        "bosque-monotono",
191        5,
192        vec![
193            Share::monotona(0, 1),
194            Share::monotona(1, 2),
195            Share::monotona(3, 4),
196        ],
197    ));
198    // Réplicas sin compartir nada (trivialmente libre).
199    casos.push(Config::new("aislado", 3, vec![]));
200
201    // --- Con operación no monótona → NeedsCoordination ---
202    // Par único con reset.
203    casos.push(Config::new(
204        "par-no-monotono",
205        2,
206        vec![Share::no_monotona(0, 1)],
207    ));
208    // Camino monótono con un reset en un tramo (localiza el nudo ahí).
209    for reset_edge in 0..3 {
210        let mut shares: Vec<Share> = (0..3).map(|i| Share::monotona(i, i + 1)).collect();
211        shares[reset_edge] = Share::no_monotona(reset_edge, reset_edge + 1);
212        casos.push(Config::new(
213            format!("camino-con-reset-en-{reset_edge}"),
214            4,
215            shares,
216        ));
217    }
218    // Dos resets independientes en partes distintas.
219    casos.push(Config::new(
220        "dos-resets-separados",
221        4,
222        vec![Share::no_monotona(0, 1), Share::no_monotona(2, 3)],
223    ));
224    // Estrella monótona con una hoja reseteada.
225    casos.push(Config::new(
226        "estrella-con-reset",
227        5,
228        vec![
229            Share::monotona(0, 1),
230            Share::monotona(0, 2),
231            Share::monotona(0, 3),
232            Share::no_monotona(0, 4),
233        ],
234    ));
235    // Árbol grande con reset en una rama.
236    casos.push(Config::new(
237        "arbol-con-reset",
238        6,
239        vec![
240            Share::monotona(0, 1),
241            Share::monotona(1, 2),
242            Share::monotona(2, 3),
243            Share::monotona(1, 4),
244            Share::no_monotona(4, 5),
245        ],
246    ));
247    // Todo no monótono.
248    casos.push(Config::new(
249        "todo-reset",
250        3,
251        vec![Share::no_monotona(0, 1), Share::no_monotona(1, 2)],
252    ));
253
254    casos
255}
256
257/// Casos donde el haz y el oráculo **discrepan** (§11 R1): dato monótono sobre
258/// un grafo de compartición **cíclico**. CALM dice coordination-free (el join
259/// existe siempre), pero la codificación lineal ve la obstrucción topológica del
260/// ciclo (`H¹ = b₁ ≠ 0`). Documentados en `DISCREPANCIES.md`.
261pub fn casos_de_discrepancia() -> Vec<Config> {
262    vec![
263        Config::new(
264            "triangulo-monotono",
265            3,
266            vec![
267                Share::monotona(0, 1),
268                Share::monotona(1, 2),
269                Share::monotona(2, 0),
270            ],
271        ),
272        Config::new(
273            "cuadrado-monotono",
274            4,
275            vec![
276                Share::monotona(0, 1),
277                Share::monotona(1, 2),
278                Share::monotona(2, 3),
279                Share::monotona(3, 0),
280            ],
281        ),
282    ]
283}
284
285#[cfg(test)]
286mod tests {
287    use super::*;
288
289    /// Test maestro (§8 M3): el veredicto del haz coincide con el del oráculo en
290    /// toda la batería de acuerdo, que tiene ≥20 casos.
291    #[test]
292    fn haz_coincide_con_oraculo() {
293        let casos = casos_de_acuerdo();
294        assert!(casos.len() >= 20, "la batería debe tener ≥20 casos, tiene {}", casos.len());
295        for c in &casos {
296            assert_eq!(
297                c.sheaf_verdict(),
298                c.oracle_verdict(),
299                "discrepancia inesperada en el caso '{}'",
300                c.name
301            );
302        }
303    }
304
305    /// Las discrepancias del MVP **lineal** (R1) son reales y esperadas: el haz
306    /// topológico dice coordinar donde CALM dice libre. Es el control histórico.
307    #[test]
308    fn discrepancias_del_lineal_persisten() {
309        for c in casos_de_discrepancia() {
310            assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
311            assert_eq!(
312                c.sheaf_verdict(),
313                OracleVerdict::NeedsCoordination,
314                "el ciclo monótono '{}' produce una falsa obstrucción topológica",
315                c.name
316            );
317        }
318    }
319
320    /// Test maestro de la pista de retículos (Addendum §F): el veredicto de
321    /// **Tarski** coincide con el oráculo en TODA la batería de acuerdo.
322    #[test]
323    fn tarski_coincide_con_oraculo() {
324        for c in &casos_de_acuerdo() {
325            assert_eq!(
326                c.tarski_verdict(),
327                c.oracle_verdict(),
328                "Tarski discrepa del oráculo en '{}'",
329                c.name
330            );
331        }
332    }
333
334    /// El cierre (Addendum §F): donde el MVP lineal inventaba obstrucción
335    /// (ciclo monótono), Tarski la **disuelve** y coincide con el oráculo. Las
336    /// discrepancias de `DISCREPANCIES.md` quedan RESUELTAS.
337    #[test]
338    fn tarski_resuelve_las_discrepancias_del_lineal() {
339        for c in casos_de_discrepancia() {
340            // El lineal dice coordinar (falso positivo)...
341            assert_eq!(c.sheaf_verdict(), OracleVerdict::NeedsCoordination);
342            // ...pero Tarski corre libre, igualando al oráculo.
343            assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
344            assert_eq!(
345                c.tarski_verdict(),
346                OracleVerdict::CoordinationFree,
347                "Tarski debe disolver la falsa obstrucción de '{}'",
348                c.name
349            );
350        }
351    }
352}